%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWX142_1 : TPTP v9.3.1. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % Computer : n018.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:45:58 PM UTC 2026 % Result : Timeout 292.08s 42.29s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.04 % Problem : SWX142_1 : TPTP v9.3.1. Released v9.3.0. % 0.00/0.08 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.10/0.25 % Computer : n018.cluster.edu % 0.10/0.25 % Model : x86_64 x86_64 % 0.10/0.25 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.25 % Memory : 8046.5625MB % 0.10/0.25 % OS : Linux 6.8.0-71-generic % 0.10/0.25 % CPULimit : 300 % 0.10/0.25 % WCLimit : 300 % 0.10/0.25 % DateTime : Mon Sep 28 15:06:55 UTC 2026 % 0.10/0.25 % CPUTime : % 0.10/0.25 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.24/0.31 Running first-order theorem proving % 0.24/0.31 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 5.32/1.91 % (3468201)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule. % 5.32/1.91 % (3468212)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=1374583161:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2995 on theBenchmark for (2995ds/12Mi) % 5.32/1.91 % (3468213)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=2382159075:i=307:kws=precedence:nm=0:rtra=on_2995 on theBenchmark for (2995ds/307Mi) % 5.32/1.91 % (3468212)Instruction limit reached! % 5.32/1.91 % (3468212)------------------------------ % 5.32/1.91 % (3468212)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.32/1.91 % (3468212)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.32/1.91 % (3468212)CaDiCaL version: 2.1.3 % 5.32/1.91 % (3468212)Termination reason: Instruction limit % 5.32/1.91 % (3468212)Termination phase: Property scanning % 5.32/1.91 % (3468212)Time elapsed: 0.006 s % 5.32/1.91 % (3468212)Peak memory usage: 85 MB % 5.32/1.91 % (3468212)Instructions burned: 13 (million) % 5.32/1.91 % (3468218)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=3393580594:i=33:rtra=on_2995 on theBenchmark for (2995ds/33Mi) % 5.32/1.91 % (3468217)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=1275684716:i=46:rtra=on_2995 on theBenchmark for (2995ds/46Mi) % 5.32/1.91 % (3468216)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=3734774465:i=4:rtra=on_2995 on theBenchmark for (2995ds/4Mi) % 5.32/1.91 % (3468215)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=3059460238:s2a=on:i=7:rtra=on:inst=on_2995 on theBenchmark for (2995ds/7Mi) % 5.32/1.91 % (3468214)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=674230987:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2995 on theBenchmark for (2995ds/201Mi) % 5.32/1.91 % (3468216)Instruction limit reached! % 5.32/1.91 % (3468216)------------------------------ % 5.32/1.91 % (3468216)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.32/1.91 % (3468216)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.32/1.91 % (3468216)CaDiCaL version: 2.1.3 % 5.32/1.91 % (3468216)Termination reason: Instruction limit % 5.32/1.91 % (3468216)Termination phase: shuffling % 5.32/1.91 % (3468216)Time elapsed: 0.003 s % 5.32/1.91 % (3468216)Peak memory usage: 85 MB % 5.32/1.91 % (3468216)Instructions burned: 4 (million) % 5.32/1.91 % (3468215)Instruction limit reached! % 5.32/1.91 % (3468215)------------------------------ % 5.32/1.91 % (3468215)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.32/1.91 % (3468215)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.32/1.91 % (3468215)CaDiCaL version: 2.1.3 % 5.32/1.91 % (3468215)Termination reason: Instruction limit % 5.32/1.91 % (3468215)Termination phase: shuffling % 5.32/1.91 % (3468215)Time elapsed: 0.005 s % 5.32/1.91 % (3468215)Peak memory usage: 85 MB % 5.32/1.91 % (3468215)Instructions burned: 8 (million) % 5.32/1.91 % (3468218)Instruction limit reached! % 5.32/1.91 % (3468218)------------------------------ % 5.32/1.91 % (3468218)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.32/1.91 % (3468218)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.32/1.91 % (3468218)CaDiCaL version: 2.1.3 % 5.32/1.91 % (3468218)Termination reason: Instruction limit % 5.32/1.91 % (3468218)Termination phase: Property scanning % 5.32/1.91 % (3468218)Time elapsed: 0.013 s % 5.32/1.91 % (3468218)Peak memory usage: 85 MB % 5.32/1.91 % (3468218)Instructions burned: 34 (million) % 5.32/1.91 % (3468217)Instruction limit reached! % 5.32/1.91 % (3468217)------------------------------ % 5.32/1.91 % (3468217)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.32/1.91 % (3468217)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.32/1.91 % (3468217)CaDiCaL version: 2.1.3 % 5.32/1.91 % (3468217)Termination reason: Instruction limit % 5.32/1.91 % (3468217)Termination phase: Property scanning % 5.32/1.91 % (3468217)Time elapsed: 0.035 s % 5.32/1.91 % (3468217)Peak memory usage: 86 MB % 5.32/1.91 % (3468217)Instructions burned: 47 (million) % 5.32/1.91 % (3468213)Instruction limit reached! % 5.32/1.91 % (3468213)------------------------------ % 5.32/1.91 % (3468213)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.32/1.91 % (3468213)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.09/2.13 % (3468213)CaDiCaL version: 2.1.3 % 7.09/2.13 % (3468213)Termination reason: Instruction limit % 7.09/2.13 % (3468213)Termination phase: Saturation % 7.09/2.13 % (3468213)Time elapsed: 0.181 s % 7.09/2.13 % (3468213)Peak memory usage: 112 MB % 7.09/2.13 % (3468213)Instructions burned: 307 (million) % 7.09/2.13 % (3468214)Instruction limit reached! % 7.09/2.13 % (3468214)------------------------------ % 7.09/2.13 % (3468214)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.09/2.13 % (3468214)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.09/2.13 % (3468214)CaDiCaL version: 2.1.3 % 7.09/2.13 % (3468214)Termination reason: Instruction limit % 7.09/2.13 % (3468214)Termination phase: Property scanning % 7.09/2.13 % (3468214)Time elapsed: 0.152 s % 7.09/2.13 % (3468214)Peak memory usage: 85 MB % 7.09/2.13 % (3468214)Instructions burned: 202 (million) % 7.09/2.13 % (3468221)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=4250204141:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2993 on theBenchmark for (2993ds/14Mi) % 7.09/2.13 % (3468221)Instruction limit reached! % 7.09/2.13 % (3468221)------------------------------ % 7.09/2.13 % (3468221)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.09/2.13 % (3468221)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.09/2.13 % (3468221)CaDiCaL version: 2.1.3 % 7.09/2.13 % (3468221)Termination reason: Instruction limit % 7.09/2.13 % (3468221)Termination phase: shuffling % 7.09/2.13 % (3468221)Time elapsed: 0.011 s % 7.09/2.13 % (3468221)Peak memory usage: 85 MB % 7.09/2.13 % (3468221)Instructions burned: 15 (million) % 7.09/2.13 % (3468228)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=2477348774:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2992 on theBenchmark for (2992ds/16Mi) % 7.09/2.13 % (3468227)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=3500587999:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2992 on theBenchmark for (2992ds/29Mi) % 7.09/2.13 % (3468228)Instruction limit reached! % 7.09/2.13 % (3468228)------------------------------ % 7.09/2.13 % (3468228)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.09/2.13 % (3468228)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.09/2.13 % (3468228)CaDiCaL version: 2.1.3 % 7.09/2.13 % (3468228)Termination reason: Instruction limit % 7.09/2.13 % (3468228)Termination phase: shuffling % 7.09/2.13 % (3468228)Time elapsed: 0.006 s % 7.09/2.13 % (3468228)Peak memory usage: 85 MB % 7.09/2.13 % (3468228)Instructions burned: 16 (million) % 7.09/2.13 % (3468227)Instruction limit reached! % 7.09/2.13 % (3468227)------------------------------ % 7.09/2.13 % (3468227)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.09/2.13 % (3468227)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.09/2.13 % (3468227)CaDiCaL version: 2.1.3 % 7.09/2.13 % (3468227)Termination reason: Instruction limit % 7.09/2.13 % (3468227)Termination phase: Property scanning % 7.09/2.13 % (3468227)Time elapsed: 0.021 s % 7.09/2.13 % (3468227)Peak memory usage: 85 MB % 7.09/2.13 % (3468227)Instructions burned: 29 (million) % 7.09/2.13 % (3468229)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=2625260715:i=24:canc=force:rtra=on_2992 on theBenchmark for (2992ds/24Mi) % 7.09/2.13 % (3468229)Instruction limit reached! % 7.09/2.13 % (3468229)------------------------------ % 7.09/2.13 % (3468229)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.09/2.13 % (3468229)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.09/2.13 % (3468229)CaDiCaL version: 2.1.3 % 7.09/2.13 % (3468229)Termination reason: Instruction limit % 7.09/2.13 % (3468229)Termination phase: Property scanning % 7.09/2.13 % (3468229)Time elapsed: 0.018 s % 7.09/2.13 % (3468229)Peak memory usage: 86 MB % 7.09/2.13 % (3468229)Instructions burned: 25 (million) % 7.09/2.13 % (3468230)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=725763578:i=27:canc=cautious:fsr=off:rtra=on_2992 on theBenchmark for (2992ds/27Mi) % 7.09/2.13 % (3468231)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=2792289640:i=85:gtgl=4:rtra=on:gtg=exists_sym_2991 on theBenchmark for (2991ds/85Mi) % 7.09/2.13 % (3468230)Instruction limit reached! % 7.09/2.13 % (3468230)------------------------------ % 8.19/2.40 % (3468230)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.19/2.40 % (3468230)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.19/2.40 % (3468230)CaDiCaL version: 2.1.3 % 8.19/2.40 % (3468230)Termination reason: Instruction limit % 8.19/2.40 % (3468230)Termination phase: Property scanning % 8.19/2.40 % (3468230)Time elapsed: 0.020 s % 8.19/2.40 % (3468230)Peak memory usage: 86 MB % 8.19/2.40 % (3468230)Instructions burned: 27 (million) % 8.19/2.40 % (3468231)Instruction limit reached! % 8.19/2.40 % (3468231)------------------------------ % 8.19/2.40 % (3468231)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.19/2.40 % (3468231)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.19/2.40 % (3468231)CaDiCaL version: 2.1.3 % 8.19/2.40 % (3468231)Termination reason: Instruction limit % 8.19/2.40 % (3468231)Termination phase: Property scanning % 8.19/2.40 % (3468231)Time elapsed: 0.033 s % 8.19/2.40 % (3468231)Peak memory usage: 85 MB % 8.19/2.40 % (3468231)Instructions burned: 85 (million) % 8.19/2.40 % (3468232)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=4198033460:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2991 on theBenchmark for (2991ds/2Mi) % 8.19/2.40 % (3468232)Instruction limit reached! % 8.19/2.40 % (3468232)------------------------------ % 8.19/2.40 % (3468232)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.19/2.40 % (3468232)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.19/2.40 % (3468232)CaDiCaL version: 2.1.3 % 8.19/2.40 % (3468232)Termination reason: Instruction limit % 8.19/2.40 % (3468232)Termination phase: shuffling % 8.19/2.40 % (3468232)Time elapsed: 0.002 s % 8.19/2.40 % (3468232)Peak memory usage: 85 MB % 8.19/2.40 % (3468232)Instructions burned: 2 (million) % 8.19/2.40 % (3468236)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=2601377906:i=181:rtra=on:ss=axioms:ev=cautious_2991 on theBenchmark for (2991ds/181Mi) % 8.19/2.40 % (3468237)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=490745424:i=4:ep=RST:ins=2:rtra=on_2990 on theBenchmark for (2990ds/4Mi) % 8.19/2.40 % (3468237)Instruction limit reached! % 8.19/2.40 % (3468237)------------------------------ % 8.19/2.40 % (3468237)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.19/2.40 % (3468237)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.19/2.40 % (3468237)CaDiCaL version: 2.1.3 % 8.19/2.40 % (3468237)Termination reason: Instruction limit % 8.19/2.40 % (3468237)Termination phase: shuffling % 8.19/2.40 % (3468237)Time elapsed: 0.003 s % 8.19/2.40 % (3468237)Peak memory usage: 85 MB % 8.19/2.40 % (3468237)Instructions burned: 4 (million) % 8.19/2.40 % (3468238)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=1838686073:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2990 on theBenchmark for (2990ds/66Mi) % 8.19/2.40 % (3468240)lrs+10_1_thi=all:si=on:fd=off:random_seed=2488893962:i=53:rtra=on:gtg=all_2990 on theBenchmark for (2990ds/53Mi) % 8.19/2.40 % (3468238)Instruction limit reached! % 8.19/2.40 % (3468238)------------------------------ % 8.19/2.40 % (3468238)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.19/2.40 % (3468238)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.19/2.40 % (3468238)CaDiCaL version: 2.1.3 % 8.19/2.40 % (3468238)Termination reason: Instruction limit % 8.19/2.40 % (3468238)Termination phase: Property scanning % 8.19/2.40 % (3468238)Time elapsed: 0.044 s % 8.19/2.40 % (3468238)Peak memory usage: 86 MB % 8.19/2.40 % (3468238)Instructions burned: 66 (million) % 8.19/2.40 % (3468244)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=3112759497:st=3:i=2:rtra=on:ss=axioms_2989 on theBenchmark for (2989ds/2Mi) % 8.19/2.40 % (3468244)Instruction limit reached! % 8.19/2.40 % (3468244)------------------------------ % 8.19/2.40 % (3468244)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.19/2.40 % (3468244)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.19/2.40 % (3468244)CaDiCaL version: 2.1.3 % 8.19/2.40 % (3468244)Termination reason: Instruction limit % 8.19/2.40 % (3468244)Termination phase: shuffling % 8.19/2.40 % (3468244)Time elapsed: 0.005 s % 8.19/2.40 % (3468244)Peak memory usage: 85 MB % 8.19/2.40 % (3468244)Instructions burned: 10 (million) % 8.19/2.40 % (3468240)Instruction limit reached! % 8.19/2.40 % (3468240)------------------------------ % 9.98/2.65 % (3468240)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.98/2.65 % (3468240)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.98/2.65 % (3468240)CaDiCaL version: 2.1.3 % 9.98/2.65 % (3468240)Termination reason: Instruction limit % 9.98/2.65 % (3468240)Termination phase: Property scanning % 9.98/2.65 % (3468240)Time elapsed: 0.042 s % 9.98/2.65 % (3468240)Peak memory usage: 85 MB % 9.98/2.65 % (3468240)Instructions burned: 54 (million) % 9.98/2.65 % (3468243)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=2598384021:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2989 on theBenchmark for (2989ds/8Mi) % 9.98/2.65 % (3468243)Instruction limit reached! % 9.98/2.65 % (3468243)------------------------------ % 9.98/2.65 % (3468243)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.98/2.65 % (3468243)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.98/2.65 % (3468243)CaDiCaL version: 2.1.3 % 9.98/2.65 % (3468243)Termination reason: Instruction limit % 9.98/2.65 % (3468243)Termination phase: Property scanning % 9.98/2.65 % (3468243)Time elapsed: 0.007 s % 9.98/2.65 % (3468243)Peak memory usage: 85 MB % 9.98/2.65 % (3468243)Instructions burned: 8 (million) % 9.98/2.65 % (3468236)Refutation not found, incomplete strategy % 9.98/2.65 % (3468236)------------------------------ % 9.98/2.65 % (3468236)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.98/2.65 % (3468236)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.98/2.65 % (3468236)CaDiCaL version: 2.1.3 % 9.98/2.65 % (3468236)Termination reason: Refutation not found, incomplete strategy % 9.98/2.65 % (3468236)Time elapsed: 0.122 s % 9.98/2.65 % (3468236)Peak memory usage: 88 MB % 9.98/2.65 % (3468236)Instructions burned: 174 (million) % 9.98/2.65 % (3468246)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=2967393630:i=2:doe=on:canc=force:asg=cautious:rtra=on_2989 on theBenchmark for (2989ds/2Mi) % 9.98/2.65 % (3468246)Instruction limit reached! % 9.98/2.65 % (3468246)------------------------------ % 9.98/2.65 % (3468246)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.98/2.65 % (3468246)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.98/2.65 % (3468246)CaDiCaL version: 2.1.3 % 9.98/2.65 % (3468246)Termination reason: Instruction limit % 9.98/2.65 % (3468246)Termination phase: shuffling % 9.98/2.65 % (3468246)Time elapsed: 0.002 s % 9.98/2.65 % (3468246)Peak memory usage: 85 MB % 9.98/2.65 % (3468246)Instructions burned: 2 (million) % 9.98/2.65 % (3468250)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=3279237380:i=127:doe=on:rtra=on_2988 on theBenchmark for (2988ds/127Mi) % 9.98/2.65 % (3468250)Instruction limit reached! % 9.98/2.65 % (3468250)------------------------------ % 9.98/2.65 % (3468250)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.98/2.65 % (3468250)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.98/2.65 % (3468250)CaDiCaL version: 2.1.3 % 9.98/2.65 % (3468250)Termination reason: Instruction limit % 9.98/2.65 % (3468250)Termination phase: Property scanning % 9.98/2.65 % (3468250)Time elapsed: 0.050 s % 9.98/2.65 % (3468250)Peak memory usage: 86 MB % 9.98/2.65 % (3468250)Instructions burned: 128 (million) % 9.98/2.65 % (3468255)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=3079612948:i=26:canc=cautious:av=off:rtra=on_2987 on theBenchmark for (2987ds/26Mi) % 9.98/2.65 % (3468255)Instruction limit reached! % 9.98/2.65 % (3468255)------------------------------ % 9.98/2.65 % (3468255)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.98/2.65 % (3468255)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.98/2.65 % (3468255)CaDiCaL version: 2.1.3 % 9.98/2.65 % (3468255)Termination reason: Instruction limit % 9.98/2.65 % (3468255)Termination phase: Property scanning % 9.98/2.65 % (3468255)Time elapsed: 0.019 s % 9.98/2.65 % (3468255)Peak memory usage: 85 MB % 9.98/2.65 % (3468255)Instructions burned: 26 (million) % 9.98/2.65 % (3468254)dis+10_1_si=on:random_seed=1085471072:i=10:ep=R:rtra=on_2987 on theBenchmark for (2987ds/10Mi) % 9.98/2.65 % (3468254)Instruction limit reached! % 9.98/2.65 % (3468254)------------------------------ % 9.98/2.65 % (3468254)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.98/2.65 % (3468254)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.88/3.01 % (3468254)CaDiCaL version: 2.1.3 % 11.88/3.01 % (3468254)Termination reason: Instruction limit % 11.88/3.01 % (3468254)Termination phase: shuffling % 11.88/3.01 % (3468254)Time elapsed: 0.007 s % 11.88/3.01 % (3468254)Peak memory usage: 85 MB % 11.88/3.01 % (3468254)Instructions burned: 11 (million) % 11.88/3.01 % (3468257)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=494989580: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_2987 on theBenchmark for (2987ds/35Mi) % 11.88/3.01 % (3468258)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=3074852858:i=2:fsr=off:rtra=on:inst=on_2987 on theBenchmark for (2987ds/2Mi) % 11.88/3.01 % (3468258)Instruction limit reached! % 11.88/3.01 % (3468258)------------------------------ % 11.88/3.01 % (3468258)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.88/3.01 % (3468258)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.88/3.01 % (3468258)CaDiCaL version: 2.1.3 % 11.88/3.01 % (3468258)Termination reason: Instruction limit % 11.88/3.01 % (3468258)Termination phase: shuffling % 11.88/3.01 % (3468258)Time elapsed: 0.002 s % 11.88/3.01 % (3468258)Peak memory usage: 85 MB % 11.88/3.01 % (3468258)Instructions burned: 3 (million) % 11.88/3.01 % (3468257)Instruction limit reached! % 11.88/3.01 % (3468257)------------------------------ % 11.88/3.01 % (3468257)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.88/3.01 % (3468257)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.88/3.01 % (3468257)CaDiCaL version: 2.1.3 % 11.88/3.01 % (3468257)Termination reason: Instruction limit % 11.88/3.01 % (3468257)Termination phase: Property scanning % 11.88/3.01 % (3468257)Time elapsed: 0.026 s % 11.88/3.01 % (3468257)Peak memory usage: 86 MB % 11.88/3.01 % (3468257)Instructions burned: 36 (million) % 11.88/3.01 % (3468260)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=853110892:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2986 on theBenchmark for (2986ds/8Mi) % 11.88/3.01 % (3468260)Instruction limit reached! % 11.88/3.01 % (3468260)------------------------------ % 11.88/3.01 % (3468260)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.88/3.01 % (3468260)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.88/3.01 % (3468260)CaDiCaL version: 2.1.3 % 11.88/3.01 % (3468260)Termination reason: Instruction limit % 11.88/3.01 % (3468260)Termination phase: shuffling % 11.88/3.01 % (3468260)Time elapsed: 0.004 s % 11.88/3.01 % (3468260)Peak memory usage: 85 MB % 11.88/3.01 % (3468260)Instructions burned: 10 (million) % 11.88/3.01 % (3468262)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=2582987510:i=370:ep=RS:fsr=off:rtra=on_2986 on theBenchmark for (2986ds/370Mi) % 11.88/3.01 % (3468236)------------------------------ % 11.88/3.01 % (3468236)------------------------------ % 11.88/3.01 % (3468267)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=4258971827:i=226:rtra=on:gtg=position:ss=axioms_2985 on theBenchmark for (2985ds/226Mi) % 11.88/3.01 % (3468265)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=1852447113:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2985 on theBenchmark for (2985ds/13Mi) % 11.88/3.01 % (3468272)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=3601230399:i=71:rtra=on:gtg=exists_top_2984 on theBenchmark for (2984ds/71Mi) % 11.88/3.01 % (3468265)Instruction limit reached! % 11.88/3.01 % (3468265)------------------------------ % 11.88/3.01 % (3468265)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.88/3.01 % (3468265)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.88/3.01 % (3468265)CaDiCaL version: 2.1.3 % 11.88/3.01 % (3468265)Termination reason: Instruction limit % 11.88/3.01 % (3468265)Termination phase: Property scanning % 11.88/3.01 % (3468265)Time elapsed: 0.012 s % 11.88/3.01 % (3468265)Peak memory usage: 85 MB % 11.88/3.01 % (3468265)Instructions burned: 14 (million) % 11.88/3.01 % (3468271)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=1138325981:i=10:rtra=on_2985 on theBenchmark for (2985ds/10Mi) % 11.88/3.01 % (3468271)Instruction limit reached! % 11.88/3.01 % (3468271)------------------------------ % 11.88/3.01 % (3468271)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.10/3.32 % (3468271)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.10/3.32 % (3468271)CaDiCaL version: 2.1.3 % 15.10/3.32 % (3468271)Termination reason: Instruction limit % 15.10/3.32 % (3468271)Termination phase: shuffling % 15.10/3.32 % (3468271)Time elapsed: 0.007 s % 15.10/3.32 % (3468271)Peak memory usage: 85 MB % 15.10/3.32 % (3468271)Instructions burned: 11 (million) % 15.10/3.32 % (3468272)Instruction limit reached! % 15.10/3.32 % (3468272)------------------------------ % 15.10/3.32 % (3468272)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.10/3.32 % (3468272)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.10/3.32 % (3468272)CaDiCaL version: 2.1.3 % 15.10/3.32 % (3468272)Termination reason: Instruction limit % 15.10/3.32 % (3468272)Termination phase: Property scanning % 15.10/3.32 % (3468272)Time elapsed: 0.030 s % 15.10/3.32 % (3468272)Peak memory usage: 85 MB % 15.10/3.32 % (3468272)Instructions burned: 72 (million) % 15.10/3.32 % (3468262)Instruction limit reached! % 15.10/3.32 % (3468262)------------------------------ % 15.10/3.32 % (3468262)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.10/3.32 % (3468262)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.10/3.32 % (3468262)CaDiCaL version: 2.1.3 % 15.10/3.32 % (3468262)Termination reason: Instruction limit % 15.10/3.32 % (3468262)Termination phase: Saturation % 15.10/3.32 % (3468262)Time elapsed: 0.141 s % 15.10/3.32 % (3468262)Peak memory usage: 88 MB % 15.10/3.32 % (3468262)Instructions burned: 372 (million) % 15.10/3.32 % (3468274)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=2521386011:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2984 on theBenchmark for (2984ds/75Mi) % 15.10/3.32 % (3468267)Instruction limit reached! % 15.10/3.32 % (3468267)------------------------------ % 15.10/3.32 % (3468267)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.10/3.32 % (3468267)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.10/3.32 % (3468267)CaDiCaL version: 2.1.3 % 15.10/3.32 % (3468267)Termination reason: Instruction limit % 15.10/3.32 % (3468267)Termination phase: Property scanning % 15.10/3.32 % (3468267)Time elapsed: 0.171 s % 15.10/3.32 % (3468267)Peak memory usage: 85 MB % 15.10/3.32 % (3468267)Instructions burned: 227 (million) % 15.10/3.32 % (3468274)Instruction limit reached! % 15.10/3.32 % (3468274)------------------------------ % 15.10/3.32 % (3468274)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.10/3.32 % (3468274)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.10/3.32 % (3468274)CaDiCaL version: 2.1.3 % 15.10/3.32 % (3468274)Termination reason: Instruction limit % 15.10/3.32 % (3468274)Termination phase: Property scanning % 15.10/3.32 % (3468274)Time elapsed: 0.056 s % 15.10/3.32 % (3468274)Peak memory usage: 85 MB % 15.10/3.32 % (3468274)Instructions burned: 76 (million) % 15.10/3.32 % (3468276)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=845730566:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2983 on theBenchmark for (2983ds/294Mi) % 15.10/3.32 % (3468283)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=4220245437:i=131:rtra=on_2982 on theBenchmark for (2982ds/131Mi) % 15.10/3.32 % (3468281)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=4134813949:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2982 on theBenchmark for (2982ds/130Mi) % 15.10/3.32 % (3468285)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=775626851:i=307:rtra=on:gtg=exists_top_2982 on theBenchmark for (2982ds/307Mi) % 15.10/3.32 % (3468284)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=1325328121:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2982 on theBenchmark for (2982ds/40Mi) % 15.10/3.32 % (3468284)Instruction limit reached! % 15.10/3.32 % (3468284)------------------------------ % 15.10/3.32 % (3468284)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.10/3.32 % (3468284)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.10/3.32 % (3468284)CaDiCaL version: 2.1.3 % 15.10/3.32 % (3468284)Termination reason: Instruction limit % 15.10/3.32 % (3468284)Termination phase: Property scanning % 15.10/3.32 % (3468284)Time elapsed: 0.031 s % 15.10/3.32 % (3468284)Peak memory usage: 85 MB % 15.10/3.32 % (3468284)Instructions burned: 40 (million) % 16.85/3.63 % (3468283)Instruction limit reached! % 16.85/3.63 % (3468283)------------------------------ % 16.85/3.63 % (3468283)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.85/3.63 % (3468283)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.85/3.63 % (3468283)CaDiCaL version: 2.1.3 % 16.85/3.63 % (3468283)Termination reason: Instruction limit % 16.85/3.63 % (3468283)Termination phase: Property scanning % 16.85/3.63 % (3468283)Time elapsed: 0.096 s % 16.85/3.63 % (3468283)Peak memory usage: 85 MB % 16.85/3.63 % (3468283)Instructions burned: 133 (million) % 16.85/3.63 % (3468281)Instruction limit reached! % 16.85/3.63 % (3468281)------------------------------ % 16.85/3.63 % (3468281)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.85/3.63 % (3468281)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.85/3.63 % (3468281)CaDiCaL version: 2.1.3 % 16.85/3.63 % (3468281)Termination reason: Instruction limit % 16.85/3.63 % (3468281)Termination phase: Property scanning % 16.85/3.63 % (3468281)Time elapsed: 0.096 s % 16.85/3.63 % (3468281)Peak memory usage: 85 MB % 16.85/3.63 % (3468281)Instructions burned: 131 (million) % 16.85/3.63 % (3468288)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=2784695773:i=131:canc=cautious:fsr=off:rtra=on_2981 on theBenchmark for (2981ds/131Mi) % 16.85/3.63 % (3468287)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=2251654226:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2981 on theBenchmark for (2981ds/598Mi) % 16.85/3.63 % (3468288)Instruction limit reached! % 16.85/3.63 % (3468288)------------------------------ % 16.85/3.63 % (3468288)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.85/3.63 % (3468288)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.85/3.63 % (3468288)CaDiCaL version: 2.1.3 % 16.85/3.63 % (3468288)Termination reason: Instruction limit % 16.85/3.63 % (3468288)Termination phase: Property scanning % 16.85/3.63 % (3468288)Time elapsed: 0.056 s % 16.85/3.63 % (3468288)Peak memory usage: 86 MB % 16.85/3.63 % (3468288)Instructions burned: 132 (million) % 16.85/3.63 % (3468276)Instruction limit reached! % 16.85/3.63 % (3468276)------------------------------ % 16.85/3.63 % (3468276)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.85/3.63 % (3468276)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.85/3.63 % (3468276)CaDiCaL version: 2.1.3 % 16.85/3.63 % (3468276)Termination reason: Instruction limit % 16.85/3.63 % (3468276)Termination phase: Property scanning % 16.85/3.63 % (3468276)Time elapsed: 0.222 s % 16.85/3.63 % (3468276)Peak memory usage: 86 MB % 16.85/3.63 % (3468276)Instructions burned: 295 (million) % 16.85/3.63 % (3468285)Instruction limit reached! % 16.85/3.63 % (3468285)------------------------------ % 16.85/3.63 % (3468285)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.85/3.63 % (3468285)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.85/3.63 % (3468285)CaDiCaL version: 2.1.3 % 16.85/3.63 % (3468285)Termination reason: Instruction limit % 16.85/3.63 % (3468285)Termination phase: Property scanning % 16.85/3.63 % (3468285)Time elapsed: 0.196 s % 16.85/3.63 % (3468285)Peak memory usage: 86 MB % 16.85/3.63 % (3468285)Instructions burned: 308 (million) % 16.85/3.63 % (3468294)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=3825432271:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2980 on theBenchmark for (2980ds/259Mi) % 16.85/3.63 % (3468296)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=2873839199:i=383:fsr=off:rtra=on:ev=force_2979 on theBenchmark for (2979ds/383Mi) % 16.85/3.63 % (3468295)dis+10_1_si=on:random_seed=3855026417:s2a=on:i=1000:rtra=on:gtg=exists_all_2980 on theBenchmark for (2980ds/1000Mi) % 16.85/3.63 % (3468301)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=1997422:i=121:nm=16:rtra=on_2978 on theBenchmark for (2978ds/121Mi) % 16.85/3.63 % (3468299)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=2569563231:i=141:doe=on:rtra=on_2979 on theBenchmark for (2979ds/141Mi) % 16.85/3.63 % (3468296)Instruction limit reached! % 16.85/3.63 % (3468296)------------------------------ % 16.85/3.63 % (3468296)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.85/3.63 % (3468296)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.92/4.00 % (3468296)CaDiCaL version: 2.1.3 % 17.92/4.00 % (3468296)Termination reason: Instruction limit % 17.92/4.00 % (3468296)Termination phase: Saturation % 17.92/4.00 % (3468296)Time elapsed: 0.128 s % 17.92/4.00 % (3468296)Peak memory usage: 88 MB % 17.92/4.00 % (3468296)Instructions burned: 384 (million) % 17.92/4.00 % (3468300)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=1081978135:i=65:nm=16:rtra=on_2978 on theBenchmark for (2978ds/65Mi) % 17.92/4.00 % (3468294)Instruction limit reached! % 17.92/4.00 % (3468294)------------------------------ % 17.92/4.00 % (3468294)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.92/4.00 % (3468294)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.92/4.00 % (3468294)CaDiCaL version: 2.1.3 % 17.92/4.00 % (3468294)Termination reason: Instruction limit % 17.92/4.00 % (3468294)Termination phase: SInE selection % 17.92/4.00 % (3468294)Time elapsed: 0.194 s % 17.92/4.00 % (3468294)Peak memory usage: 86 MB % 17.92/4.00 % (3468294)Instructions burned: 259 (million) % 17.92/4.00 % (3468301)Instruction limit reached! % 17.92/4.00 % (3468301)------------------------------ % 17.92/4.00 % (3468301)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.92/4.00 % (3468301)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.92/4.00 % (3468301)CaDiCaL version: 2.1.3 % 17.92/4.00 % (3468301)Termination reason: Instruction limit % 17.92/4.00 % (3468301)Termination phase: Property scanning % 17.92/4.00 % (3468301)Time elapsed: 0.097 s % 17.92/4.00 % (3468301)Peak memory usage: 86 MB % 17.92/4.00 % (3468301)Instructions burned: 122 (million) % 17.92/4.00 % (3468300)Instruction limit reached! % 17.92/4.00 % (3468300)------------------------------ % 17.92/4.00 % (3468300)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.92/4.00 % (3468300)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.92/4.00 % (3468300)CaDiCaL version: 2.1.3 % 17.92/4.00 % (3468300)Termination reason: Instruction limit % 17.92/4.00 % (3468300)Termination phase: Property scanning % 17.92/4.00 % (3468300)Time elapsed: 0.048 s % 17.92/4.00 % (3468300)Peak memory usage: 86 MB % 17.92/4.00 % (3468300)Instructions burned: 66 (million) % 17.92/4.00 % (3468299)Instruction limit reached! % 17.92/4.00 % (3468299)------------------------------ % 17.92/4.00 % (3468299)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.92/4.00 % (3468299)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.92/4.00 % (3468299)CaDiCaL version: 2.1.3 % 17.92/4.00 % (3468299)Termination reason: Instruction limit % 17.92/4.00 % (3468299)Termination phase: Property scanning % 17.92/4.00 % (3468299)Time elapsed: 0.106 s % 17.92/4.00 % (3468299)Peak memory usage: 86 MB % 17.92/4.00 % (3468299)Instructions burned: 142 (million) % 17.92/4.00 % (3468308)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=1906199800:s2a=on:i=128:s2at=5:ins=3:rtra=on_2976 on theBenchmark for (2976ds/128Mi) % 17.92/4.00 % (3468287)Instruction limit reached! % 17.92/4.00 % (3468287)------------------------------ % 17.92/4.00 % (3468287)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.92/4.00 % (3468287)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.92/4.00 % (3468287)CaDiCaL version: 2.1.3 % 17.92/4.00 % (3468287)Termination reason: Instruction limit % 17.92/4.00 % (3468287)Termination phase: Saturation % 17.92/4.00 % (3468287)Time elapsed: 0.491 s % 17.92/4.00 % (3468287)Peak memory usage: 130 MB % 17.92/4.00 % (3468287)Instructions burned: 599 (million) % 17.92/4.00 % (3468308)Instruction limit reached! % 17.92/4.00 % (3468308)------------------------------ % 17.92/4.00 % (3468308)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.92/4.00 % (3468308)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.92/4.00 % (3468308)CaDiCaL version: 2.1.3 % 17.92/4.00 % (3468308)Termination reason: Instruction limit % 17.92/4.00 % (3468308)Termination phase: Property scanning % 17.92/4.00 % (3468308)Time elapsed: 0.050 s % 17.92/4.00 % (3468308)Peak memory usage: 86 MB % 17.92/4.00 % (3468308)Instructions burned: 128 (million) % 17.92/4.00 % (3468310)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=306840479:i=39:ins=3:rtra=on_2976 on theBenchmark for (2976ds/39Mi) % 17.92/4.00 % (3468311)dis+1010_1_to=kbo:si=on:random_seed=89360704:i=175:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2975 on theBenchmark for (2975ds/175Mi) % 22.89/4.59 % (3468312)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=3520567115:i=329:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2975 on theBenchmark for (2975ds/329Mi) % 22.89/4.59 % (3468310)Instruction limit reached! % 22.89/4.59 % (3468310)------------------------------ % 22.89/4.59 % (3468310)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 22.89/4.59 % (3468310)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.89/4.59 % (3468310)CaDiCaL version: 2.1.3 % 22.89/4.59 % (3468310)Termination reason: Instruction limit % 22.89/4.59 % (3468310)Termination phase: Property scanning % 22.89/4.59 % (3468310)Time elapsed: 0.029 s % 22.89/4.59 % (3468310)Peak memory usage: 85 MB % 22.89/4.59 % (3468310)Instructions burned: 40 (million) % 22.89/4.59 % (3468313)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=2817438134:s2a=on:i=483:doe=on:nm=32:rtra=on_2975 on theBenchmark for (2975ds/483Mi) % 22.89/4.59 % (3468316)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=4131474670:thitd=on:i=215:nm=0:rtra=on:ev=force_2974 on theBenchmark for (2974ds/215Mi) % 22.89/4.59 % (3468317)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=3376375118:i=349:rtra=on_2974 on theBenchmark for (2974ds/349Mi) % 22.89/4.59 % (3468311)Instruction limit reached! % 22.89/4.59 % (3468311)------------------------------ % 22.89/4.59 % (3468311)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 22.89/4.59 % (3468311)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.89/4.59 % (3468311)CaDiCaL version: 2.1.3 % 22.89/4.59 % (3468311)Termination reason: Instruction limit % 22.89/4.59 % (3468311)Termination phase: Property scanning % 22.89/4.59 % (3468311)Time elapsed: 0.133 s % 22.89/4.59 % (3468311)Peak memory usage: 85 MB % 22.89/4.59 % (3468311)Instructions burned: 176 (million) % 22.89/4.59 % (3468312)Instruction limit reached! % 22.89/4.59 % (3468312)------------------------------ % 22.89/4.59 % (3468312)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 22.89/4.59 % (3468312)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.89/4.59 % (3468312)CaDiCaL version: 2.1.3 % 22.89/4.59 % (3468312)Termination reason: Instruction limit % 22.89/4.59 % (3468312)Termination phase: Property scanning % 22.89/4.59 % (3468312)Time elapsed: 0.241 s % 22.89/4.59 % (3468312)Peak memory usage: 85 MB % 22.89/4.59 % (3468312)Instructions burned: 329 (million) % 22.89/4.59 % (3468316)Instruction limit reached! % 22.89/4.59 % (3468316)------------------------------ % 22.89/4.59 % (3468316)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 22.89/4.59 % (3468316)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.89/4.59 % (3468316)CaDiCaL version: 2.1.3 % 22.89/4.59 % (3468316)Termination reason: Instruction limit % 22.89/4.59 % (3468316)Termination phase: Property scanning % 22.89/4.59 % (3468316)Time elapsed: 0.165 s % 22.89/4.59 % (3468316)Peak memory usage: 86 MB % 22.89/4.59 % (3468316)Instructions burned: 215 (million) % 22.89/4.59 % (3468317)Instruction limit reached! % 22.89/4.59 % (3468317)------------------------------ % 22.89/4.59 % (3468317)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 22.89/4.59 % (3468317)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.89/4.59 % (3468317)CaDiCaL version: 2.1.3 % 22.89/4.59 % (3468317)Termination reason: Instruction limit % 22.89/4.59 % (3468317)Termination phase: Saturation % 22.89/4.59 % (3468317)Time elapsed: 0.153 s % 22.89/4.59 % (3468317)Peak memory usage: 112 MB % 22.89/4.59 % (3468317)Instructions burned: 350 (million) % 22.89/4.59 % (3468322)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=362979893:st=2:i=295:rtra=on:ss=axioms_2973 on theBenchmark for (2973ds/295Mi) % 22.89/4.59 % (3468295)Instruction limit reached! % 22.89/4.59 % (3468295)------------------------------ % 22.89/4.59 % (3468295)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 22.89/4.59 % (3468295)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.89/4.59 % (3468295)CaDiCaL version: 2.1.3 % 22.89/4.59 % (3468295)Termination reason: Instruction limit % 22.89/4.59 % (3468295)Termination phase: Saturation % 22.89/4.59 % (3468295)Time elapsed: 0.735 s % 22.89/4.59 % (3468295)Peak memory usage: 89 MB % 22.89/4.59 % (3468295)Instructions burned: 1000 (million) % 26.17/5.00 % (3468325)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=4163466725:i=328:kws=inv_frequency:nm=20:rtra=on_2972 on theBenchmark for (2972ds/328Mi) % 26.17/5.00 % (3468313)Instruction limit reached! % 26.17/5.00 % (3468313)------------------------------ % 26.17/5.00 % (3468313)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.17/5.00 % (3468313)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.17/5.00 % (3468313)CaDiCaL version: 2.1.3 % 26.17/5.00 % (3468313)Termination reason: Instruction limit % 26.17/5.00 % (3468313)Termination phase: Saturation % 26.17/5.00 % (3468313)Time elapsed: 0.408 s % 26.17/5.00 % (3468313)Peak memory usage: 129 MB % 26.17/5.00 % (3468313)Instructions burned: 483 (million) % 26.17/5.00 % (3468328)lrs+21_1_to=kbo:sil=128000:thi=neg_eq:si=on:random_seed=3691809032:i=321:canc=force:rtra=on:tac=axiom:ss=axioms:ev=force_2970 on theBenchmark for (2970ds/321Mi) % 26.17/5.00 % (3468326)dis+1010_1_to=lpo:sil=128000:sas=z3:si=on:nwc=5:random_seed=3495479934:i=281:gtgl=2:rtra=on:gtg=all_2971 on theBenchmark for (2971ds/281Mi) % 26.17/5.00 % (3468327)lrs+1010_1_to=kbo:sil=128000:si=on:sos=on:urr=on:uwa=alasca_main:random_seed=3724841940:i=484:doe=on:nm=0:av=off:rtra=on:ss=axioms_2971 on theBenchmark for (2971ds/484Mi) % 26.17/5.00 % (3468322)Refutation not found, incomplete strategy % 26.17/5.00 % (3468322)------------------------------ % 26.17/5.00 % (3468322)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.17/5.00 % (3468322)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.17/5.00 % (3468322)CaDiCaL version: 2.1.3 % 26.17/5.00 % (3468322)Termination reason: Refutation not found, incomplete strategy % 26.17/5.00 % (3468322)Time elapsed: 0.210 s % 26.17/5.00 % (3468322)Peak memory usage: 88 MB % 26.17/5.00 % (3468322)Instructions burned: 289 (million) % 26.17/5.00 % (3468330)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=993652615:i=416:rtra=on:gtg=position:ss=axioms_2970 on theBenchmark for (2970ds/416Mi) % 26.17/5.00 % (3468328)Refutation not found, incomplete strategy % 26.17/5.00 % (3468328)------------------------------ % 26.17/5.00 % (3468328)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.17/5.00 % (3468328)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.17/5.00 % (3468328)CaDiCaL version: 2.1.3 % 26.17/5.00 % (3468328)Termination reason: Refutation not found, incomplete strategy % 26.17/5.00 % (3468328)Time elapsed: 0.153 s % 26.17/5.00 % (3468328)Peak memory usage: 112 MB % 26.17/5.00 % (3468328)Instructions burned: 286 (million) % 26.17/5.00 % (3468330)Refutation not found, incomplete strategy % 26.17/5.00 % (3468330)------------------------------ % 26.17/5.00 % (3468330)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.17/5.00 % (3468330)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.17/5.00 % (3468330)CaDiCaL version: 2.1.3 % 26.17/5.00 % (3468330)Termination reason: Refutation not found, incomplete strategy % 26.17/5.00 % (3468330)Time elapsed: 0.126 s % 26.17/5.00 % (3468330)Peak memory usage: 112 MB % 26.17/5.00 % (3468330)Instructions burned: 286 (million) % 26.17/5.00 % (3468325)Instruction limit reached! % 26.17/5.00 % (3468325)------------------------------ % 26.17/5.00 % (3468325)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.17/5.00 % (3468325)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.17/5.00 % (3468325)CaDiCaL version: 2.1.3 % 26.17/5.00 % (3468325)Termination reason: Instruction limit % 26.17/5.00 % (3468325)Termination phase: Property scanning % 26.17/5.00 % (3468325)Time elapsed: 0.249 s % 26.17/5.00 % (3468325)Peak memory usage: 86 MB % 26.17/5.00 % (3468325)Instructions burned: 328 (million) % 26.17/5.00 % (3468327)Refutation not found, incomplete strategy % 26.17/5.00 % (3468327)------------------------------ % 26.17/5.00 % (3468327)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.17/5.00 % (3468327)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.17/5.00 % (3468327)CaDiCaL version: 2.1.3 % 26.17/5.00 % (3468327)Termination reason: Refutation not found, incomplete strategy % 26.17/5.00 % (3468327)Time elapsed: 0.206 s % 26.17/5.00 % (3468327)Peak memory usage: 88 MB % 26.17/5.00 % (3468327)Instructions burned: 282 (million) % 26.17/5.00 % (3468326)Instruction limit reached! % 26.17/5.00 % (3468326)------------------------------ % 29.73/5.52 % (3468326)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.73/5.52 % (3468326)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.73/5.52 % (3468326)CaDiCaL version: 2.1.3 % 29.73/5.52 % (3468326)Termination reason: Instruction limit % 29.73/5.52 % (3468326)Termination phase: Property scanning % 29.73/5.52 % (3468326)Time elapsed: 0.207 s % 29.73/5.52 % (3468326)Peak memory usage: 86 MB % 29.73/5.52 % (3468326)Instructions burned: 282 (million) % 29.73/5.52 % (3468333)lrs+1010_1_to=kbo:tgt=ground:fde=unused:sas=z3:si=on:sp=unary_frequency:gve=force:spb=goal:tha=off:random_seed=4065943435:i=471:thf=on:kws=precedence:rtra=on_2969 on theBenchmark for (2969ds/471Mi) % 29.73/5.52 % (3468330)------------------------------ % 29.73/5.52 % (3468330)------------------------------ % 29.73/5.52 % (3468322)------------------------------ % 29.73/5.52 % (3468322)------------------------------ % 29.73/5.52 % (3468337)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=1416205233:avsq=on:i=276:avsqr=1,2:rtra=on_2967 on theBenchmark for (2967ds/276Mi) % 29.73/5.52 % (3468338)lrs+1010_2_to=kbo:sil=128000:tgt=ground:fde=unused:sas=z3:si=on:uwa=off:tha=off:nwc=1:random_seed=1594575178:i=375:kws=inv_arity_squared:rtra=on_2966 on theBenchmark for (2966ds/375Mi) % 29.73/5.52 % (3468328)------------------------------ % 29.73/5.52 % (3468328)------------------------------ % 29.73/5.52 % (3468337)Instruction limit reached! % 29.73/5.52 % (3468337)------------------------------ % 29.73/5.52 % (3468337)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.73/5.52 % (3468337)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.73/5.52 % (3468337)CaDiCaL version: 2.1.3 % 29.73/5.52 % (3468337)Termination reason: Instruction limit % 29.73/5.52 % (3468337)Termination phase: Property scanning % 29.73/5.52 % (3468337)Time elapsed: 0.118 s % 29.73/5.52 % (3468337)Peak memory usage: 87 MB % 29.73/5.52 % (3468337)Instructions burned: 278 (million) % 29.73/5.52 % (3468340)lrs+10_1_to=kbo:sil=128000:tgt=full:sas=z3:si=on:uwa=func_ext:slsqc=1:flr=on:slsq=on:random_seed=4013251540:i=387:bd=preordered:rtra=on:ss=axioms:sgt=8_2964 on theBenchmark for (2964ds/387Mi) % 29.73/5.52 % (3468327)------------------------------ % 29.73/5.52 % (3468327)------------------------------ % 29.73/5.52 % (3468333)Instruction limit reached! % 29.73/5.52 % (3468333)------------------------------ % 29.73/5.52 % (3468333)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.73/5.52 % (3468333)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.73/5.52 % (3468333)CaDiCaL version: 2.1.3 % 29.73/5.52 % (3468333)Termination reason: Instruction limit % 29.73/5.52 % (3468333)Termination phase: Saturation % 29.73/5.52 % (3468333)Time elapsed: 0.385 s % 29.73/5.52 % (3468333)Peak memory usage: 114 MB % 29.73/5.52 % (3468333)Instructions burned: 472 (million) % 29.73/5.52 % (3468342)lrs+10_1_to=kbo:sil=128000:fde=none:si=on:norm_ineq=on:urr=on:nwc=0.5:random_seed=3379007046:i=513:kws=frequency:bd=all:rtra=on:gtg=exists_all:ss=axioms:sgt=4_2964 on theBenchmark for (2964ds/513Mi) % 29.73/5.52 % (3468340)Refutation not found, incomplete strategy % 29.73/5.52 % (3468340)------------------------------ % 29.73/5.52 % (3468340)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.73/5.52 % (3468340)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.73/5.52 % (3468340)CaDiCaL version: 2.1.3 % 29.73/5.52 % (3468340)Termination reason: Refutation not found, incomplete strategy % 29.73/5.52 % (3468340)Time elapsed: 0.131 s % 29.73/5.52 % (3468340)Peak memory usage: 112 MB % 29.73/5.52 % (3468340)Instructions burned: 301 (million) % 29.73/5.52 % (3468347)dis+1010_1_to=lpo:sil=128000:thi=all:fde=unused:si=on:sp=reverse_arity:tha=off:random_seed=2816506831:i=341:gtgl=2:rtra=on:gtg=exists_sym:ev=force:fsd=on:fsdmm=1_2962 on theBenchmark for (2962ds/341Mi) % 29.73/5.52 % (3468344)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=122708302:i=334:rtra=on_2963 on theBenchmark for (2963ds/334Mi) % 29.73/5.52 % (3468345)lrs+1010_1_to=kbo:sil=64000:sas=cadical:si=on:sos=on:bce=on:random_seed=227621557:i=359:rtra=on:gtg=exists_top:ss=axioms_2963 on theBenchmark for (2963ds/359Mi) % 29.73/5.52 % (3468338)Instruction limit reached! % 29.73/5.52 % (3468338)------------------------------ % 29.73/5.52 % (3468338)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 35.07/6.06 % (3468338)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.07/6.06 % (3468338)CaDiCaL version: 2.1.3 % 35.07/6.06 % (3468338)Termination reason: Instruction limit % 35.07/6.06 % (3468338)Termination phase: Saturation % 35.07/6.06 % (3468338)Time elapsed: 0.302 s % 35.07/6.06 % (3468338)Peak memory usage: 112 MB % 35.07/6.06 % (3468338)Instructions burned: 376 (million) % 35.07/6.06 % (3468349)lrs-2_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_max:tha=off:random_seed=3137391565:st=1.5:i=261:sd=1:kws=precedence:rtra=on:ss=axioms_2962 on theBenchmark for (2962ds/261Mi) % 35.07/6.06 % (3468340)------------------------------ % 35.07/6.06 % (3468340)------------------------------ % 35.07/6.06 % (3468347)Instruction limit reached! % 35.07/6.06 % (3468347)------------------------------ % 35.07/6.06 % (3468347)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 35.07/6.06 % (3468347)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.07/6.06 % (3468347)CaDiCaL version: 2.1.3 % 35.07/6.06 % (3468347)Termination reason: Instruction limit % 35.07/6.06 % (3468347)Termination phase: Property scanning % 35.07/6.07 % (3468347)Time elapsed: 0.243 s % 35.07/6.07 % (3468347)Peak memory usage: 86 MB % 35.07/6.07 % (3468347)Instructions burned: 342 (million) % 35.07/6.07 % (3468354)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=2660006535:s2pl=no:i=235:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2960 on theBenchmark for (2960ds/235Mi) % 35.07/6.07 % (3468345)Instruction limit reached! % 35.07/6.07 % (3468345)------------------------------ % 35.07/6.07 % (3468345)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 35.07/6.07 % (3468345)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.07/6.07 % (3468345)CaDiCaL version: 2.1.3 % 35.07/6.07 % (3468345)Termination reason: Instruction limit % 35.07/6.07 % (3468345)Termination phase: SInE selection % 35.07/6.07 % (3468345)Time elapsed: 0.272 s % 35.07/6.07 % (3468345)Peak memory usage: 86 MB % 35.07/6.07 % (3468345)Instructions burned: 360 (million) % 35.07/6.07 % (3468342)Instruction limit reached! % 35.07/6.07 % (3468342)------------------------------ % 35.07/6.07 % (3468342)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 35.07/6.07 % (3468342)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.07/6.07 % (3468342)CaDiCaL version: 2.1.3 % 35.07/6.07 % (3468342)Termination reason: Instruction limit % 35.07/6.07 % (3468342)Termination phase: Property scanning % 35.07/6.07 % (3468342)Time elapsed: 0.386 s % 35.07/6.07 % (3468342)Peak memory usage: 86 MB % 35.07/6.07 % (3468342)Instructions burned: 514 (million) % 35.07/6.07 % (3468344)Instruction limit reached! % 35.07/6.07 % (3468344)------------------------------ % 35.07/6.07 % (3468344)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 35.07/6.07 % (3468344)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.07/6.07 % (3468344)CaDiCaL version: 2.1.3 % 35.07/6.07 % (3468344)Termination reason: Instruction limit % 35.07/6.07 % (3468344)Termination phase: Saturation % 35.07/6.07 % (3468344)Time elapsed: 0.300 s % 35.07/6.07 % (3468344)Peak memory usage: 129 MB % 35.07/6.07 % (3468344)Instructions burned: 335 (million) % 35.07/6.07 % (3468349)Refutation not found, incomplete strategy % 35.07/6.07 % (3468349)------------------------------ % 35.07/6.07 % (3468349)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 35.07/6.07 % (3468349)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.07/6.07 % (3468349)CaDiCaL version: 2.1.3 % 35.07/6.07 % (3468349)Termination reason: Refutation not found, incomplete strategy % 35.07/6.07 % (3468349)Time elapsed: 0.167 s % 35.07/6.07 % (3468349)Peak memory usage: 112 MB % 35.07/6.07 % (3468349)Instructions burned: 193 (million) % 35.07/6.07 % (3468357)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=2238925393:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2959 on theBenchmark for (2959ds/273Mi) % 35.07/6.07 % (3468354)Instruction limit reached! % 35.07/6.07 % (3468354)------------------------------ % 35.07/6.07 % (3468354)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 35.07/6.07 % (3468354)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.07/6.07 % (3468354)CaDiCaL version: 2.1.3 % 35.07/6.07 % (3468354)Termination reason: Instruction limit % 35.07/6.07 % (3468354)Termination phase: SInE selection % 38.55/6.72 % (3468354)Time elapsed: 0.176 s % 38.55/6.72 % (3468354)Peak memory usage: 86 MB % 38.55/6.72 % (3468354)Instructions burned: 236 (million) % 38.55/6.72 % (3468357)Instruction limit reached! % 38.55/6.72 % (3468357)------------------------------ % 38.55/6.72 % (3468357)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 38.55/6.72 % (3468357)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.55/6.72 % (3468357)CaDiCaL version: 2.1.3 % 38.55/6.72 % (3468357)Termination reason: Instruction limit % 38.55/6.72 % (3468357)Termination phase: Property scanning % 38.55/6.72 % (3468357)Time elapsed: 0.106 s % 38.55/6.72 % (3468357)Peak memory usage: 86 MB % 38.55/6.72 % (3468357)Instructions burned: 275 (million) % 38.55/6.72 % (3468359)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=327361515:i=146:doe=on:rtra=on_2958 on theBenchmark for (2958ds/146Mi) % 38.55/6.72 % (3468360)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=2272085462:i=4428:doe=on:fsr=off:rtra=on_2958 on theBenchmark for (2958ds/4428Mi) % 38.55/6.72 % (3468361)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=3201976603:avsq=on:i=276:avsqr=1,2:rtra=on_2958 on theBenchmark for (2958ds/276Mi) % 38.55/6.72 % (3468362)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=4285517451:i=1052:rtra=on_2957 on theBenchmark for (2957ds/1052Mi) % 38.55/6.72 % (3468359)Instruction limit reached! % 38.55/6.72 % (3468359)------------------------------ % 38.55/6.72 % (3468359)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 38.55/6.72 % (3468359)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.55/6.72 % (3468359)CaDiCaL version: 2.1.3 % 38.55/6.72 % (3468359)Termination reason: Instruction limit % 38.55/6.72 % (3468359)Termination phase: Property scanning % 38.55/6.72 % (3468359)Time elapsed: 0.111 s % 38.55/6.72 % (3468359)Peak memory usage: 86 MB % 38.55/6.72 % (3468359)Instructions burned: 147 (million) % 38.55/6.72 % (3468364)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=3352909815:i=655:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2956 on theBenchmark for (2956ds/655Mi) % 38.55/6.72 % (3468349)------------------------------ % 38.55/6.72 % (3468349)------------------------------ % 38.55/6.72 % (3468361)Instruction limit reached! % 38.55/6.72 % (3468361)------------------------------ % 38.55/6.72 % (3468361)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 38.55/6.72 % (3468361)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.55/6.72 % (3468361)CaDiCaL version: 2.1.3 % 38.55/6.72 % (3468361)Termination reason: Instruction limit % 38.55/6.72 % (3468361)Termination phase: Property scanning % 38.55/6.72 % (3468361)Time elapsed: 0.206 s % 38.55/6.72 % (3468361)Peak memory usage: 86 MB % 38.55/6.72 % (3468361)Instructions burned: 276 (million) % 38.55/6.72 % (3468368)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=271748972:st=5:i=1054:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2956 on theBenchmark for (2956ds/1054Mi) % 38.55/6.72 % (3468368)Refutation not found, incomplete strategy % 38.55/6.72 % (3468368)------------------------------ % 38.55/6.72 % (3468368)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 38.55/6.72 % (3468368)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.55/6.72 % (3468368)CaDiCaL version: 2.1.3 % 38.55/6.72 % (3468368)Termination reason: Refutation not found, incomplete strategy % 38.55/6.72 % (3468368)Time elapsed: 0.065 s % 38.55/6.72 % (3468368)Peak memory usage: 88 MB % 38.55/6.72 % (3468368)Instructions burned: 181 (million) % 38.55/6.72 % (3468370)lrs-1002_1_to=kbo:sas=z3:si=on:norm_ineq=on:sos=on:tha=some:random_seed=3535540772:i=107:rtra=on_2954 on theBenchmark for (2954ds/107Mi) % 38.55/6.72 % (3468374)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 % 38.55/6.72 % (3468374)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=2088333707:i=1090:aac=none:nm=0:rtra=on:rawr=on_2953 on theBenchmark for (2953ds/1090Mi) % 38.55/6.72 % (3468370)Instruction limit reached! % 38.55/6.72 % (3468370)------------------------------ % 38.55/6.72 % (3468370)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 43.87/7.39 % (3468370)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.87/7.39 % (3468370)CaDiCaL version: 2.1.3 % 43.87/7.39 % (3468370)Termination reason: Instruction limit % 43.87/7.39 % (3468370)Termination phase: Property scanning % 43.87/7.39 % (3468370)Time elapsed: 0.083 s % 43.87/7.39 % (3468370)Peak memory usage: 86 MB % 43.87/7.39 % (3468370)Instructions burned: 108 (million) % 43.87/7.39 % (3468372)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=4137108574:s2a=on:i=450:doe=on:nm=32:rtra=on_2954 on theBenchmark for (2954ds/450Mi) % 43.87/7.39 % (3468368)------------------------------ % 43.87/7.39 % (3468368)------------------------------ % 43.87/7.39 % (3468377)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=3793218134:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2951 on theBenchmark for (2951ds/130Mi) % 43.87/7.39 % (3468364)Instruction limit reached! % 43.87/7.39 % (3468364)------------------------------ % 43.87/7.39 % (3468364)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 43.87/7.39 % (3468364)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.87/7.39 % (3468364)CaDiCaL version: 2.1.3 % 43.87/7.39 % (3468364)Termination reason: Instruction limit % 43.87/7.39 % (3468364)Termination phase: Saturation % 43.87/7.39 % (3468364)Time elapsed: 0.475 s % 43.87/7.39 % (3468364)Peak memory usage: 89 MB % 43.87/7.39 % (3468364)Instructions burned: 655 (million) % 43.87/7.39 % (3468377)Instruction limit reached! % 43.87/7.39 % (3468377)------------------------------ % 43.87/7.39 % (3468377)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 43.87/7.39 % (3468377)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.87/7.39 % (3468377)CaDiCaL version: 2.1.3 % 43.87/7.39 % (3468377)Termination reason: Instruction limit % 43.87/7.39 % (3468377)Termination phase: Property scanning % 43.87/7.39 % (3468377)Time elapsed: 0.054 s % 43.87/7.39 % (3468377)Peak memory usage: 85 MB % 43.87/7.39 % (3468377)Instructions burned: 132 (million) % 43.87/7.39 % (3468379)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=223257894:i=312:kws=inv_frequency:nm=20:rtra=on_2950 on theBenchmark for (2950ds/312Mi) % 43.87/7.39 % (3468362)Instruction limit reached! % 43.87/7.39 % (3468362)------------------------------ % 43.87/7.39 % (3468362)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 43.87/7.39 % (3468362)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.87/7.39 % (3468362)CaDiCaL version: 2.1.3 % 43.87/7.39 % (3468362)Termination reason: Instruction limit % 43.87/7.39 % (3468362)Termination phase: Saturation % 43.87/7.39 % (3468362)Time elapsed: 0.739 s % 43.87/7.39 % (3468362)Peak memory usage: 95 MB % 43.87/7.39 % (3468362)Instructions burned: 1053 (million) % 43.87/7.39 % (3468379)Instruction limit reached! % 43.87/7.39 % (3468379)------------------------------ % 43.87/7.39 % (3468379)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 43.87/7.39 % (3468379)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.87/7.39 % (3468379)CaDiCaL version: 2.1.3 % 43.87/7.39 % (3468379)Termination reason: Instruction limit % 43.87/7.39 % (3468379)Termination phase: Property scanning % 43.87/7.39 % (3468379)Time elapsed: 0.122 s % 43.87/7.39 % (3468379)Peak memory usage: 86 MB % 43.87/7.39 % (3468379)Instructions burned: 313 (million) % 43.87/7.39 % (3468372)Instruction limit reached! % 43.87/7.39 % (3468372)------------------------------ % 43.87/7.39 % (3468372)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 43.87/7.39 % (3468372)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.87/7.39 % (3468372)CaDiCaL version: 2.1.3 % 43.87/7.39 % (3468372)Termination reason: Instruction limit % 43.87/7.39 % (3468372)Termination phase: Saturation % 43.87/7.39 % (3468372)Time elapsed: 0.383 s % 43.87/7.39 % (3468372)Peak memory usage: 129 MB % 43.87/7.39 % (3468372)Instructions burned: 450 (million) % 43.87/7.39 % (3468381)ott+10_1_to=kbo:sil=64000:si=on:sp=reverse_frequency:sos=on:random_seed=256561660:i=491:doe=on:rtra=on:gtg=position_2949 on theBenchmark for (2949ds/491Mi) % 43.87/7.39 % (3468382)ott+1011_4:1_to=lpo:sil=64000:si=on:spb=intro:random_seed=4155785863:s2a=on:i=835:s2at=2:rtra=on_2949 on theBenchmark for (2949ds/835Mi) % 43.87/7.39 % (3468384)ott+1011_2_to=lpo:sil=128000:si=on:sos=on:random_seed=451725427:i=307:bd=preordered:av=off:rtra=on:ev=cautious_2947 on theBenchmark for (2947ds/307Mi) % 50.42/8.26 % (3468385)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=2226393543:i=776:doe=on:rtra=on_2947 on theBenchmark for (2947ds/776Mi) % 50.42/8.26 % (3468386)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=4221745946:s2a=on:i=646:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2947 on theBenchmark for (2947ds/646Mi) % 50.42/8.26 % (3468384)Instruction limit reached! % 50.42/8.26 % (3468384)------------------------------ % 50.42/8.26 % (3468384)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 50.42/8.26 % (3468384)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 50.42/8.26 % (3468384)CaDiCaL version: 2.1.3 % 50.42/8.26 % (3468384)Termination reason: Instruction limit % 50.42/8.26 % (3468384)Termination phase: Property scanning % 50.42/8.26 % (3468384)Time elapsed: 0.123 s % 50.42/8.26 % (3468384)Peak memory usage: 86 MB % 50.42/8.26 % (3468384)Instructions burned: 309 (million) % 50.42/8.26 % (3468374)Instruction limit reached! % 50.42/8.26 % (3468374)------------------------------ % 50.42/8.26 % (3468374)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 50.42/8.26 % (3468374)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 50.42/8.26 % (3468374)CaDiCaL version: 2.1.3 % 50.42/8.26 % (3468374)Termination reason: Instruction limit % 50.42/8.26 % (3468374)Termination phase: Saturation % 50.42/8.26 % (3468374)Time elapsed: 0.808 s % 50.42/8.26 % (3468374)Peak memory usage: 116 MB % 50.42/8.26 % (3468374)Instructions burned: 1090 (million) % 50.42/8.26 % (3468381)Instruction limit reached! % 50.42/8.26 % (3468381)------------------------------ % 50.42/8.26 % (3468381)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 50.42/8.26 % (3468381)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 50.42/8.26 % (3468381)CaDiCaL version: 2.1.3 % 50.42/8.26 % (3468381)Termination reason: Instruction limit % 50.42/8.26 % (3468381)Termination phase: Property scanning % 50.42/8.26 % (3468381)Time elapsed: 0.372 s % 50.42/8.26 % (3468381)Peak memory usage: 87 MB % 50.42/8.26 % (3468381)Instructions burned: 491 (million) % 50.42/8.26 % (3468393)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=3950864458:thitd=on:cond=fast:i=784:nm=30:rtra=on:gtg=all:tac=axiom_2944 on theBenchmark for (2944ds/784Mi) % 50.42/8.26 % (3468394)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=2610576991:thitd=on:s2a=on:i=1131:add=on:canc=force:bd=all:rtra=on:tac=axiom:ev=off_2943 on theBenchmark for (2943ds/1131Mi) % 50.42/8.26 % (3468382)Instruction limit reached! % 50.42/8.26 % (3468382)------------------------------ % 50.42/8.26 % (3468382)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 50.42/8.26 % (3468382)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 50.42/8.26 % (3468382)CaDiCaL version: 2.1.3 % 50.42/8.26 % (3468382)Termination reason: Instruction limit % 50.42/8.26 % (3468382)Termination phase: Saturation % 50.42/8.26 % (3468382)Time elapsed: 0.622 s % 50.42/8.26 % (3468382)Peak memory usage: 92 MB % 50.42/8.26 % (3468382)Instructions burned: 835 (million) % 50.42/8.26 % (3468386)Instruction limit reached! % 50.42/8.26 % (3468386)------------------------------ % 50.42/8.26 % (3468386)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 50.42/8.26 % (3468386)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 50.42/8.26 % (3468386)CaDiCaL version: 2.1.3 % 50.42/8.26 % (3468386)Termination reason: Instruction limit % 50.42/8.26 % (3468386)Termination phase: Saturation % 50.42/8.26 % (3468386)Time elapsed: 0.463 s % 50.42/8.26 % (3468386)Peak memory usage: 131 MB % 50.42/8.26 % (3468386)Instructions burned: 646 (million) % 50.42/8.26 % (3468396)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=1800782633:s2pl=no:i=246:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2942 on theBenchmark for (2942ds/246Mi) % 50.42/8.26 % (3468393)Instruction limit reached! % 50.42/8.26 % (3468393)------------------------------ % 50.42/8.26 % (3468393)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 50.42/8.26 % (3468393)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 50.42/8.26 % (3468393)CaDiCaL version: 2.1.3 % 50.42/8.26 % (3468393)Termination reason: Instruction limit % 60.73/10.01 % (3468393)Termination phase: Saturation % 60.73/10.01 % (3468393)Time elapsed: 0.315 s % 60.73/10.01 % (3468393)Peak memory usage: 112 MB % 60.73/10.01 % (3468393)Instructions burned: 784 (million) % 60.73/10.01 % (3468385)Instruction limit reached! % 60.73/10.01 % (3468385)------------------------------ % 60.73/10.01 % (3468385)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 60.73/10.01 % (3468385)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.73/10.01 % (3468385)CaDiCaL version: 2.1.3 % 60.73/10.01 % (3468385)Termination reason: Instruction limit % 60.73/10.01 % (3468385)Termination phase: Saturation % 60.73/10.01 % (3468385)Time elapsed: 0.604 s % 60.73/10.01 % (3468385)Peak memory usage: 117 MB % 60.73/10.01 % (3468385)Instructions burned: 777 (million) % 60.73/10.01 % (3468396)Instruction limit reached! % 60.73/10.01 % (3468396)------------------------------ % 60.73/10.01 % (3468396)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 60.73/10.01 % (3468396)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.73/10.01 % (3468396)CaDiCaL version: 2.1.3 % 60.73/10.01 % (3468396)Termination reason: Instruction limit % 60.73/10.01 % (3468396)Termination phase: SInE selection % 60.73/10.01 % (3468396)Time elapsed: 0.187 s % 60.73/10.01 % (3468396)Peak memory usage: 86 MB % 60.73/10.01 % (3468396)Instructions burned: 247 (million) % 60.73/10.01 % (3468400)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=2498474063:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2940 on theBenchmark for (2940ds/775Mi) % 60.73/10.01 % (3468402)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=2540188133:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2940 on theBenchmark for (2940ds/273Mi) % 60.73/10.01 % (3468404)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=4034974437:i=102:nm=16:rtra=on_2939 on theBenchmark for (2939ds/102Mi) % 60.73/10.01 % (3468404)Instruction limit reached! % 60.73/10.01 % (3468404)------------------------------ % 60.73/10.01 % (3468404)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 60.73/10.01 % (3468404)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.73/10.01 % (3468404)CaDiCaL version: 2.1.3 % 60.73/10.01 % (3468404)Termination reason: Instruction limit % 60.73/10.01 % (3468404)Termination phase: Property scanning % 60.73/10.01 % (3468404)Time elapsed: 0.041 s % 60.73/10.01 % (3468404)Peak memory usage: 86 MB % 60.73/10.01 % (3468404)Instructions burned: 104 (million) % 60.73/10.01 % (3468405)lrs+10_1_to=lpo:sil=128000:si=on:bsr=unit_only:tha=off:random_seed=2775933040:avsq=on:s2a=on:i=1094:s2at=5:avsqr=4463,131072:rtra=on_2939 on theBenchmark for (2939ds/1094Mi) % 60.73/10.01 % (3468402)Instruction limit reached! % 60.73/10.01 % (3468402)------------------------------ % 60.73/10.01 % (3468402)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 60.73/10.01 % (3468402)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.73/10.01 % (3468402)CaDiCaL version: 2.1.3 % 60.73/10.01 % (3468402)Termination reason: Instruction limit % 60.73/10.01 % (3468402)Termination phase: Property scanning % 60.73/10.01 % (3468402)Time elapsed: 0.206 s % 60.73/10.01 % (3468402)Peak memory usage: 86 MB % 60.73/10.01 % (3468402)Instructions burned: 274 (million) % 60.73/10.01 % (3468406)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=722891839:i=6400:doe=on:fsr=off:rtra=on_2938 on theBenchmark for (2938ds/6400Mi) % 60.73/10.01 % (3468400)Refutation not found, incomplete strategy % 60.73/10.01 % (3468400)------------------------------ % 60.73/10.01 % (3468400)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 60.73/10.01 % (3468400)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.73/10.01 % (3468400)CaDiCaL version: 2.1.3 % 60.73/10.01 % (3468400)Termination reason: Refutation not found, incomplete strategy % 60.73/10.01 % (3468400)Time elapsed: 0.223 s % 60.73/10.01 % (3468400)Peak memory usage: 88 MB % 60.73/10.01 % (3468400)Instructions burned: 304 (million) % 60.73/10.01 % (3468410)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=788797759:i=868:doe=on:nm=0:rtra=on:gtg=exists_sym_2937 on theBenchmark for (2937ds/868Mi) % 60.73/10.01 % (3468413)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=2383696700:i=1846:canc=cautious:fsr=off:rtra=on_2935 on theBenchmark for (2935ds/1846Mi) % 74.05/11.66 % (3468394)Instruction limit reached! % 74.05/11.66 % (3468394)------------------------------ % 74.05/11.66 % (3468394)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 74.05/11.66 % (3468394)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.05/11.66 % (3468394)CaDiCaL version: 2.1.3 % 74.05/11.66 % (3468394)Termination reason: Instruction limit % 74.05/11.66 % (3468394)Termination phase: Saturation % 74.05/11.66 % (3468394)Time elapsed: 0.886 s % 74.05/11.66 % (3468394)Peak memory usage: 117 MB % 74.05/11.66 % (3468394)Instructions burned: 1131 (million) % 74.05/11.66 % (3468410)Instruction limit reached! % 74.05/11.66 % (3468410)------------------------------ % 74.05/11.66 % (3468410)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 74.05/11.66 % (3468410)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.05/11.66 % (3468410)CaDiCaL version: 2.1.3 % 74.05/11.66 % (3468410)Termination reason: Instruction limit % 74.05/11.66 % (3468410)Termination phase: Saturation % 74.05/11.66 % (3468410)Time elapsed: 0.335 s % 74.05/11.66 % (3468410)Peak memory usage: 116 MB % 74.05/11.66 % (3468410)Instructions burned: 869 (million) % 74.05/11.66 % (3468400)------------------------------ % 74.05/11.66 % (3468400)------------------------------ % 74.05/11.66 % (3468417)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=3672671237:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2931 on theBenchmark for (2931ds/273Mi) % 74.05/11.66 % (3468416)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=938990082:s2a=on:i=36816:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2932 on theBenchmark for (2932ds/36816Mi) % 74.05/11.66 % (3468418)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=1736972367:i=863:doe=on:nm=0:rtra=on:gtg=exists_sym_2931 on theBenchmark for (2931ds/863Mi) % 74.05/11.66 % (3468417)Instruction limit reached! % 74.05/11.66 % (3468417)------------------------------ % 74.05/11.66 % (3468417)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 74.05/11.66 % (3468417)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.05/11.66 % (3468417)CaDiCaL version: 2.1.3 % 74.05/11.66 % (3468417)Termination reason: Instruction limit % 74.05/11.66 % (3468417)Termination phase: Property scanning % 74.05/11.66 % (3468417)Time elapsed: 0.109 s % 74.05/11.66 % (3468417)Peak memory usage: 86 MB % 74.05/11.66 % (3468417)Instructions burned: 275 (million) % 74.05/11.66 % (3468405)Instruction limit reached! % 74.05/11.66 % (3468405)------------------------------ % 74.05/11.66 % (3468405)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 74.05/11.66 % (3468405)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.05/11.66 % (3468405)CaDiCaL version: 2.1.3 % 74.05/11.66 % (3468405)Termination reason: Instruction limit % 74.05/11.66 % (3468405)Termination phase: Saturation % 74.05/11.66 % (3468405)Time elapsed: 0.786 s % 74.05/11.66 % (3468405)Peak memory usage: 94 MB % 74.05/11.66 % (3468405)Instructions burned: 1095 (million) % 74.05/11.66 % (3468413)Refutation not found, incomplete strategy % 74.05/11.66 % (3468413)------------------------------ % 74.05/11.66 % (3468413)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 74.05/11.66 % (3468413)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.05/11.66 % (3468413)CaDiCaL version: 2.1.3 % 74.05/11.66 % (3468413)Termination reason: Refutation not found, incomplete strategy % 74.05/11.66 % (3468413)Time elapsed: 0.498 s % 74.05/11.66 % (3468413)Peak memory usage: 91 MB % 74.05/11.66 % (3468413)Instructions burned: 676 (million) % 74.05/11.66 % (3468422)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=116908646:i=5811:kws=precedence:nm=0:rtra=on_2929 on theBenchmark for (2929ds/5811Mi) % 74.05/11.66 % (3468423)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=1209938860:i=2216:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2928 on theBenchmark for (2928ds/2216Mi) % 74.05/11.66 % (3468360)Instruction limit reached! % 74.05/11.66 % (3468360)------------------------------ % 74.05/11.66 % (3468360)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 74.05/11.66 % (3468360)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 81.27/12.85 % (3468360)CaDiCaL version: 2.1.3 % 81.27/12.85 % (3468360)Termination reason: Instruction limit % 81.27/12.85 % (3468360)Termination phase: Saturation % 81.27/12.85 % (3468360)Time elapsed: 3.190 s % 81.27/12.85 % (3468360)Peak memory usage: 91 MB % 81.27/12.85 % (3468360)Instructions burned: 4429 (million) % 81.27/12.85 % (3468413)------------------------------ % 81.27/12.85 % (3468413)------------------------------ % 81.27/12.85 % (3468418)Instruction limit reached! % 81.27/12.85 % (3468418)------------------------------ % 81.27/12.85 % (3468418)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 81.27/12.85 % (3468418)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 81.27/12.85 % (3468418)CaDiCaL version: 2.1.3 % 81.27/12.85 % (3468418)Termination reason: Instruction limit % 81.27/12.85 % (3468418)Termination phase: Saturation % 81.27/12.85 % (3468418)Time elapsed: 0.628 s % 81.27/12.85 % (3468418)Peak memory usage: 115 MB % 81.27/12.85 % (3468418)Instructions burned: 863 (million) % 81.27/12.85 % (3468426)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=171865400:i=801:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2924 on theBenchmark for (2924ds/801Mi) % 81.27/12.85 % (3468427)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=1093297088:st=5:i=1026:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2923 on theBenchmark for (2923ds/1026Mi) % 81.27/12.85 % (3468428)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=3544186087:i=3509:rtra=on_2923 on theBenchmark for (2923ds/3509Mi) % 81.27/12.85 % (3468427)Refutation not found, incomplete strategy % 81.27/12.85 % (3468427)------------------------------ % 81.27/12.85 % (3468427)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 81.27/12.85 % (3468427)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 81.27/12.85 % (3468427)CaDiCaL version: 2.1.3 % 81.27/12.85 % (3468427)Termination reason: Refutation not found, incomplete strategy % 81.27/12.85 % (3468427)Time elapsed: 0.127 s % 81.27/12.85 % (3468427)Peak memory usage: 88 MB % 81.27/12.85 % (3468427)Instructions burned: 181 (million) % 81.27/12.85 % (3468427)------------------------------ % 81.27/12.85 % (3468427)------------------------------ % 81.27/12.85 % (3468426)Instruction limit reached! % 81.27/12.85 % (3468426)------------------------------ % 81.27/12.85 % (3468426)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 81.27/12.85 % (3468426)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 81.27/12.85 % (3468426)CaDiCaL version: 2.1.3 % 81.27/12.85 % (3468426)Termination reason: Instruction limit % 81.27/12.85 % (3468426)Termination phase: Saturation % 81.27/12.85 % (3468426)Time elapsed: 0.569 s % 81.27/12.85 % (3468426)Peak memory usage: 93 MB % 81.27/12.85 % (3468426)Instructions burned: 802 (million) % 81.27/12.85 % (3468432)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=2677722042:st=2:i=2127:sd=12:ep=R:rtra=on:ss=axioms_2916 on theBenchmark for (2916ds/2127Mi) % 81.27/12.85 % (3468433)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=3517364927:i=1959:rtra=on:fsd=on:proc=on_2915 on theBenchmark for (2915ds/1959Mi) % 81.27/12.85 % (3468432)Refutation not found, incomplete strategy % 81.27/12.85 % (3468432)------------------------------ % 81.27/12.85 % (3468432)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 81.27/12.85 % (3468432)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 81.27/12.85 % (3468432)CaDiCaL version: 2.1.3 % 81.27/12.85 % (3468432)Termination reason: Refutation not found, incomplete strategy % 81.27/12.85 % (3468432)Time elapsed: 0.209 s % 81.27/12.85 % (3468432)Peak memory usage: 88 MB % 81.27/12.85 % (3468432)Instructions burned: 289 (million) % 81.27/12.85 % (3468423)Instruction limit reached! % 81.27/12.85 % (3468423)------------------------------ % 81.27/12.85 % (3468423)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 81.27/12.85 % (3468423)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 81.27/12.85 % (3468423)CaDiCaL version: 2.1.3 % 81.27/12.85 % (3468423)Termination reason: Instruction limit % 81.27/12.85 % (3468423)Termination phase: Saturation % 81.27/12.85 % (3468423)Time elapsed: 1.666 s % 81.27/12.85 % (3468423)Peak memory usage: 119 MB % 81.27/12.85 % (3468423)Instructions burned: 2216 (million) % 81.27/12.85 % (3468432)------------------------------ % 81.27/12.85 % (3468432)------------------------------ % 81.27/12.85 % (3468436)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=869966275:s2a=on:i=3553:nm=0:rtra=on_2909 on theBenchmark for (2909ds/3553Mi) % 115.76/17.41 % (3468422)Instruction limit reached! % 115.76/17.41 % (3468422)------------------------------ % 115.76/17.41 % (3468422)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 115.76/17.41 % (3468422)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 115.76/17.41 % (3468422)CaDiCaL version: 2.1.3 % 115.76/17.41 % (3468422)Termination reason: Instruction limit % 115.76/17.41 % (3468422)Termination phase: Saturation % 115.76/17.41 % (3468422)Time elapsed: 2.187 s % 115.76/17.41 % (3468422)Peak memory usage: 124 MB % 115.76/17.41 % (3468422)Instructions burned: 5812 (million) % 115.76/17.41 % (3468438)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=3418407180:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2907 on theBenchmark for (2907ds/3201Mi) % 115.76/17.41 % (3468440)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=3268139330:thitd=on:cond=on:i=4093:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2905 on theBenchmark for (2905ds/4093Mi) % 115.76/17.41 % (3468433)Instruction limit reached! % 115.76/17.41 % (3468433)------------------------------ % 115.76/17.41 % (3468433)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 115.76/17.41 % (3468433)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 115.76/17.41 % (3468433)CaDiCaL version: 2.1.3 % 115.76/17.41 % (3468433)Termination reason: Instruction limit % 115.76/17.41 % (3468433)Termination phase: Saturation % 115.76/17.41 % (3468433)Time elapsed: 1.488 s % 115.76/17.41 % (3468433)Peak memory usage: 123 MB % 115.76/17.41 % (3468433)Instructions burned: 1959 (million) % 115.76/17.41 % (3468428)Instruction limit reached! % 115.76/17.41 % (3468428)------------------------------ % 115.76/17.41 % (3468428)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 115.76/17.41 % (3468428)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 115.76/17.41 % (3468428)CaDiCaL version: 2.1.3 % 115.76/17.41 % (3468428)Termination reason: Instruction limit % 115.76/17.41 % (3468428)Termination phase: Saturation % 115.76/17.41 % (3468428)Time elapsed: 2.400 s % 115.76/17.41 % (3468428)Peak memory usage: 96 MB % 115.76/17.41 % (3468428)Instructions burned: 3509 (million) % 115.76/17.41 % (3468444)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=1795689088:cond=fast:i=21173:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2898 on theBenchmark for (2898ds/21173Mi) % 115.76/17.41 % (3468444)Refutation not found, incomplete strategy % 115.76/17.41 % (3468444)------------------------------ % 115.76/17.41 % (3468444)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 115.76/17.41 % (3468444)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 115.76/17.41 % (3468444)CaDiCaL version: 2.1.3 % 115.76/17.41 % (3468444)Termination reason: Refutation not found, incomplete strategy % 115.76/17.41 % (3468444)Time elapsed: 0.145 s % 115.76/17.41 % (3468444)Peak memory usage: 113 MB % 115.76/17.41 % (3468444)Instructions burned: 147 (million) % 115.76/17.41 % (3468445)lrs+11_1_to=lpo:thi=all:sas=z3:si=on:fd=off:sac=on:slsq=on:random_seed=4053322265:avsq=on:i=10544:avsqr=17,4:canc=force:rtra=on:gtg=exists_top:er=filter_2896 on theBenchmark for (2896ds/10544Mi) % 115.76/17.41 % (3468438)Refutation not found, incomplete strategy % 115.76/17.41 % (3468438)------------------------------ % 115.76/17.41 % (3468438)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 115.76/17.41 % (3468438)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 115.76/17.41 % (3468438)CaDiCaL version: 2.1.3 % 115.76/17.41 % (3468438)Termination reason: Refutation not found, incomplete strategy % 115.76/17.41 % (3468438)Time elapsed: 1.355 s % 115.76/17.41 % (3468438)Peak memory usage: 99 MB % 115.76/17.41 % (3468438)Instructions burned: 1826 (million) % 115.76/17.41 % (3468406)Instruction limit reached! % 115.76/17.41 % (3468406)------------------------------ % 115.76/17.41 % (3468406)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 115.76/17.41 % (3468406)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 115.76/17.41 % (3468406)CaDiCaL version: 2.1.3 % 115.76/17.41 % (3468406)Termination reason: Instruction limit % 115.76/17.41 % (3468406)Termination phase: Saturation % 115.76/17.41 % (3468406)Time elapsed: 4.528 s % 115.76/17.41 % (3468406)Peak memory usage: 92 MB % 115.76/17.41 % (3468406)Instructions burned: 6401 (million) % 115.76/17.41 % (3468444)------------------------------ % 131.82/19.71 % (3468444)------------------------------ % 131.82/19.71 % (3468440)Instruction limit reached! % 131.82/19.71 % (3468440)------------------------------ % 131.82/19.71 % (3468440)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 131.82/19.71 % (3468440)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.82/19.71 % (3468440)CaDiCaL version: 2.1.3 % 131.82/19.71 % (3468440)Termination reason: Instruction limit % 131.82/19.71 % (3468440)Termination phase: Saturation % 131.82/19.71 % (3468440)Time elapsed: 1.552 s % 131.82/19.71 % (3468440)Peak memory usage: 134 MB % 131.82/19.71 % (3468440)Instructions burned: 4095 (million) % 131.82/19.71 % (3468448)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=1502214718:avsq=on:i=1262:avsqr=1,16:rtra=on:rawr=on_2890 on theBenchmark for (2890ds/1262Mi) % 131.82/19.71 % (3468449)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=105093568:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2890 on theBenchmark for (2890ds/775Mi) % 131.82/19.71 % (3468438)------------------------------ % 131.82/19.71 % (3468438)------------------------------ % 131.82/19.71 % (3468436)Instruction limit reached! % 131.82/19.71 % (3468436)------------------------------ % 131.82/19.71 % (3468436)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 131.82/19.71 % (3468436)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.82/19.71 % (3468436)CaDiCaL version: 2.1.3 % 131.82/19.71 % (3468436)Termination reason: Instruction limit % 131.82/19.71 % (3468436)Termination phase: Saturation % 131.82/19.71 % (3468436)Time elapsed: 2.010 s % 131.82/19.71 % (3468436)Peak memory usage: 101 MB % 131.82/19.71 % (3468436)Instructions burned: 3554 (million) % 131.82/19.71 % (3468450)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=2428167973:i=270:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2887 on theBenchmark for (2887ds/270Mi) % 131.82/19.71 % (3468449)Refutation not found, incomplete strategy % 131.82/19.71 % (3468449)------------------------------ % 131.82/19.71 % (3468449)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 131.82/19.71 % (3468449)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.82/19.71 % (3468449)CaDiCaL version: 2.1.3 % 131.82/19.71 % (3468449)Termination reason: Refutation not found, incomplete strategy % 131.82/19.71 % (3468449)Time elapsed: 0.221 s % 131.82/19.71 % (3468449)Peak memory usage: 88 MB % 131.82/19.71 % (3468449)Instructions burned: 304 (million) % 131.82/19.71 % (3468450)Instruction limit reached! % 131.82/19.71 % (3468450)------------------------------ % 131.82/19.71 % (3468450)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 131.82/19.71 % (3468450)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.82/19.71 % (3468450)CaDiCaL version: 2.1.3 % 131.82/19.71 % (3468450)Termination reason: Instruction limit % 131.82/19.71 % (3468450)Termination phase: Property scanning % 131.82/19.71 % (3468450)Time elapsed: 0.107 s % 131.82/19.71 % (3468450)Peak memory usage: 86 MB % 131.82/19.71 % (3468450)Instructions burned: 272 (million) % 131.82/19.71 % (3468453)ott+10_128_isp=bottom:to=lpo:sil=128000:si=on:urr=on:uwa=alasca_main:sac=on:slsq=on:random_seed=519006772:i=17165:aac=none:doe=on:rtra=on:gtg=exists_all_2886 on theBenchmark for (2886ds/17165Mi) % 131.82/19.71 % (3468454)lrs+2_10_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_main:tha=some:random_seed=2261199397:s2a=on:i=13094:s2at=-1:rtra=on_2886 on theBenchmark for (2886ds/13094Mi) % 131.82/19.71 % (3468456)lrs+10_1_to=lpo:sil=128000:si=on:sp=occurrence:random_seed=2094809920:st=2:i=12633:rtra=on:ss=axioms_2884 on theBenchmark for (2884ds/12633Mi) % 131.82/19.71 % (3468456)Refutation not found, incomplete strategy % 131.82/19.71 % (3468456)------------------------------ % 131.82/19.71 % (3468456)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 131.82/19.71 % (3468456)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.82/19.71 % (3468456)CaDiCaL version: 2.1.3 % 131.82/19.71 % (3468456)Termination reason: Refutation not found, incomplete strategy % 131.82/19.71 % (3468456)Time elapsed: 0.102 s % 131.82/19.71 % (3468456)Peak memory usage: 88 MB % 131.82/19.71 % (3468456)Instructions burned: 257 (million) % 131.82/19.71 % (3468449)------------------------------ % 131.82/19.71 % (3468449)------------------------------ % 131.82/19.71 % (3468456)------------------------------ % 131.82/19.71 % (3468456)------------------------------ % 131.82/19.71 % (3468462)dis+1011_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_frequency:lsd=20:nwc=3:random_seed=3546488671:i=1783:rtra=on:gtg=position_2881 on theBenchmark for (2881ds/1783Mi) % 168.26/24.87 % (3468448)Instruction limit reached! % 168.26/24.87 % (3468448)------------------------------ % 168.26/24.87 % (3468448)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 168.26/24.87 % (3468448)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 168.26/24.87 % (3468448)CaDiCaL version: 2.1.3 % 168.26/24.87 % (3468448)Termination reason: Instruction limit % 168.26/24.87 % (3468448)Termination phase: Saturation % 168.26/24.87 % (3468448)Time elapsed: 0.971 s % 168.26/24.87 % (3468448)Peak memory usage: 116 MB % 168.26/24.87 % (3468448)Instructions burned: 1262 (million) % 168.26/24.87 % (3468463)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=1827475555:i=5451:aac=none:doe=on:nm=0:rtra=on:amm=off:gtg=position_2879 on theBenchmark for (2879ds/5451Mi) % 168.26/24.87 % (3468465)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=3861796158:i=4975:doe=on:nm=0:rtra=on:gtg=exists_sym_2877 on theBenchmark for (2877ds/4975Mi) % 168.26/24.87 % (3468462)Instruction limit reached! % 168.26/24.87 % (3468462)------------------------------ % 168.26/24.87 % (3468462)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 168.26/24.87 % (3468462)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 168.26/24.87 % (3468462)CaDiCaL version: 2.1.3 % 168.26/24.87 % (3468462)Termination reason: Instruction limit % 168.26/24.87 % (3468462)Termination phase: Saturation % 168.26/24.87 % (3468462)Time elapsed: 1.349 s % 168.26/24.87 % (3468462)Peak memory usage: 114 MB % 168.26/24.87 % (3468462)Instructions burned: 1783 (million) % 168.26/24.87 % (3468468)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=3545761267:i=2076:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2864 on theBenchmark for (2864ds/2076Mi) % 168.26/24.87 % (3468465)Instruction limit reached! % 168.26/24.87 % (3468465)------------------------------ % 168.26/24.87 % (3468465)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 168.26/24.87 % (3468465)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 168.26/24.87 % (3468465)CaDiCaL version: 2.1.3 % 168.26/24.87 % (3468465)Termination reason: Instruction limit % 168.26/24.87 % (3468465)Termination phase: Saturation % 168.26/24.87 % (3468465)Time elapsed: 2.292 s % 168.26/24.87 % (3468465)Peak memory usage: 164 MB % 168.26/24.87 % (3468465)Instructions burned: 4975 (million) % 168.26/24.87 % (3468472)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=3479903248:i=5145:rtra=on_2852 on theBenchmark for (2852ds/5145Mi) % 168.26/24.87 % (3468468)Instruction limit reached! % 168.26/24.87 % (3468468)------------------------------ % 168.26/24.87 % (3468468)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 168.26/24.87 % (3468468)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 168.26/24.87 % (3468468)CaDiCaL version: 2.1.3 % 168.26/24.87 % (3468468)Termination reason: Instruction limit % 168.26/24.87 % (3468468)Termination phase: Saturation % 168.26/24.87 % (3468468)Time elapsed: 1.575 s % 168.26/24.87 % (3468468)Peak memory usage: 117 MB % 168.26/24.87 % (3468468)Instructions burned: 2076 (million) % 168.26/24.87 % (3468474)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=2130473768:i=3509:rtra=on_2846 on theBenchmark for (2846ds/3509Mi) % 168.26/24.87 % (3468463)Instruction limit reached! % 168.26/24.87 % (3468463)------------------------------ % 168.26/24.87 % (3468463)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 168.26/24.87 % (3468463)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 168.26/24.87 % (3468463)CaDiCaL version: 2.1.3 % 168.26/24.87 % (3468463)Termination reason: Instruction limit % 168.26/24.87 % (3468463)Termination phase: Saturation % 168.26/24.87 % (3468463)Time elapsed: 4.018 s % 168.26/24.87 % (3468463)Peak memory usage: 125 MB % 168.26/24.87 % (3468463)Instructions burned: 5452 (million) % 168.26/24.87 % (3468480)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=619229918:st=2:i=13800:sd=12:ep=R:rtra=on:ss=axioms_2836 on theBenchmark for (2836ds/13800Mi) % 168.26/24.87 % (3468472)Instruction limit reached! % 168.26/24.87 % (3468472)------------------------------ % 168.26/24.87 % (3468472)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 235.31/34.24 % (3468472)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.31/34.24 % (3468472)CaDiCaL version: 2.1.3 % 235.31/34.24 % (3468472)Termination reason: Instruction limit % 235.31/34.24 % (3468472)Termination phase: Saturation % 235.31/34.24 % (3468472)Time elapsed: 1.780 s % 235.31/34.24 % (3468472)Peak memory usage: 95 MB % 235.31/34.24 % (3468472)Instructions burned: 5148 (million) % 235.31/34.24 % (3468480)Refutation not found, incomplete strategy % 235.31/34.24 % (3468480)------------------------------ % 235.31/34.24 % (3468480)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 235.31/34.24 % (3468480)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.31/34.24 % (3468480)CaDiCaL version: 2.1.3 % 235.31/34.24 % (3468480)Termination reason: Refutation not found, incomplete strategy % 235.31/34.24 % (3468480)Time elapsed: 0.213 s % 235.31/34.24 % (3468480)Peak memory usage: 88 MB % 235.31/34.24 % (3468480)Instructions burned: 289 (million) % 235.31/34.24 % (3468484)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=44115259:i=1412:rtra=on:fsd=on:proc=on_2832 on theBenchmark for (2832ds/1412Mi) % 235.31/34.24 % (3468480)------------------------------ % 235.31/34.24 % (3468480)------------------------------ % 235.31/34.24 % (3468484)Instruction limit reached! % 235.31/34.24 % (3468484)------------------------------ % 235.31/34.24 % (3468484)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 235.31/34.24 % (3468484)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.31/34.24 % (3468484)CaDiCaL version: 2.1.3 % 235.31/34.24 % (3468484)Termination reason: Instruction limit % 235.31/34.24 % (3468484)Termination phase: Saturation % 235.31/34.24 % (3468484)Time elapsed: 0.463 s % 235.31/34.24 % (3468484)Peak memory usage: 117 MB % 235.31/34.24 % (3468484)Instructions burned: 1416 (million) % 235.31/34.24 % (3468489)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 % 235.31/34.24 % (3468489)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=1959715028:i=11747:aac=none:nm=0:rtra=on:rawr=on_2827 on theBenchmark for (2827ds/11747Mi) % 235.31/34.24 % (3468490)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=3432915679:s2a=on:i=3553:nm=0:rtra=on_2825 on theBenchmark for (2825ds/3553Mi) % 235.31/34.24 % (3468474)Instruction limit reached! % 235.31/34.24 % (3468474)------------------------------ % 235.31/34.24 % (3468474)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 235.31/34.24 % (3468474)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.31/34.24 % (3468474)CaDiCaL version: 2.1.3 % 235.31/34.24 % (3468474)Termination reason: Instruction limit % 235.31/34.24 % (3468474)Termination phase: Saturation % 235.31/34.24 % (3468474)Time elapsed: 2.498 s % 235.31/34.24 % (3468474)Peak memory usage: 92 MB % 235.31/34.24 % (3468474)Instructions burned: 3510 (million) % 235.31/34.24 % (3468494)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=4117109217:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2818 on theBenchmark for (2818ds/3201Mi) % 235.31/34.24 % (3468490)Instruction limit reached! % 235.31/34.24 % (3468490)------------------------------ % 235.31/34.24 % (3468490)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 235.31/34.24 % (3468490)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.31/34.24 % (3468490)CaDiCaL version: 2.1.3 % 235.31/34.24 % (3468490)Termination reason: Instruction limit % 235.31/34.24 % (3468490)Termination phase: Saturation % 235.31/34.24 % (3468490)Time elapsed: 1.060 s % 235.31/34.24 % (3468490)Peak memory usage: 101 MB % 235.31/34.24 % (3468490)Instructions burned: 3554 (million) % 235.31/34.24 % (3468496)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=782698740:thitd=on:cond=on:i=4081:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2812 on theBenchmark for (2812ds/4081Mi) % 235.31/34.24 % (3468445)Instruction limit reached! % 235.31/34.24 % (3468445)------------------------------ % 235.31/34.24 % (3468445)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 235.31/34.24 % (3468445)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.31/34.24 % (3468445)CaDiCaL version: 2.1.3 % 235.31/34.24 % (3468445)Termination reason: Instruction limit % 246.91/36.00 % (3468445)Termination phase: Saturation % 246.91/36.00 % (3468445)Time elapsed: 8.401 s % 246.91/36.00 % (3468445)Peak memory usage: 168 MB % 246.91/36.00 % (3468445)Instructions burned: 10545 (million) % 246.91/36.00 % (3468498)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=33470568:cond=fast:i=20260:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2809 on theBenchmark for (2809ds/20260Mi) % 246.91/36.00 % (3468498)Refutation not found, incomplete strategy % 246.91/36.00 % (3468498)------------------------------ % 246.91/36.00 % (3468498)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 246.91/36.00 % (3468498)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 246.91/36.00 % (3468498)CaDiCaL version: 2.1.3 % 246.91/36.00 % (3468498)Termination reason: Refutation not found, incomplete strategy % 246.91/36.00 % (3468498)Time elapsed: 0.141 s % 246.91/36.00 % (3468498)Peak memory usage: 113 MB % 246.91/36.00 % (3468498)Instructions burned: 147 (million) % 246.91/36.00 % (3468494)Refutation not found, incomplete strategy % 246.91/36.00 % (3468494)------------------------------ % 246.91/36.00 % (3468494)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 246.91/36.00 % (3468494)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 246.91/36.00 % (3468494)CaDiCaL version: 2.1.3 % 246.91/36.00 % (3468494)Termination reason: Refutation not found, incomplete strategy % 246.91/36.00 % (3468494)Time elapsed: 1.359 s % 246.91/36.00 % (3468494)Peak memory usage: 99 MB % 246.91/36.00 % (3468494)Instructions burned: 1828 (million) % 246.91/36.00 % (3468498)------------------------------ % 246.91/36.00 % (3468498)------------------------------ % 246.91/36.00 % (3468500)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=4165530515:s2a=on:i=58627:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2801 on theBenchmark for (2801ds/58627Mi) % 246.91/36.00 % (3468494)------------------------------ % 246.91/36.00 % (3468494)------------------------------ % 246.91/36.00 % (3468496)Instruction limit reached! % 246.91/36.00 % (3468496)------------------------------ % 246.91/36.00 % (3468496)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 246.91/36.00 % (3468496)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 246.91/36.00 % (3468496)CaDiCaL version: 2.1.3 % 246.91/36.00 % (3468496)Termination reason: Instruction limit % 246.91/36.00 % (3468496)Termination phase: Saturation % 246.91/36.00 % (3468496)Time elapsed: 1.523 s % 246.91/36.00 % (3468496)Peak memory usage: 136 MB % 246.91/36.00 % (3468496)Instructions burned: 4081 (million) % 246.91/36.00 % (3468503)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=1861220908:avsq=on:i=6258:avsqr=1,16:rtra=on:rawr=on_2798 on theBenchmark for (2798ds/6258Mi) % 246.91/36.00 % (3468506)ott+10_128_isp=bottom:to=lpo:sil=128000:si=on:urr=on:uwa=alasca_main:sac=on:slsq=on:random_seed=86194753:i=34001:aac=none:doe=on:rtra=on:gtg=exists_all_2795 on theBenchmark for (2795ds/34001Mi) % 246.91/36.00 % (3468454)Instruction limit reached! % 246.91/36.00 % (3468454)------------------------------ % 246.91/36.00 % (3468454)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 246.91/36.00 % (3468454)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 246.91/36.00 % (3468454)CaDiCaL version: 2.1.3 % 246.91/36.00 % (3468454)Termination reason: Instruction limit % 246.91/36.00 % (3468454)Termination phase: Saturation % 246.91/36.00 % (3468454)Time elapsed: 9.185 s % 246.91/36.00 % (3468454)Peak memory usage: 97 MB % 246.91/36.00 % (3468454)Instructions burned: 13094 (million) % 246.91/36.00 % (3468508)lrs+2_10_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_main:tha=some:random_seed=1206774349:s2a=on:i=71622:s2at=-1:rtra=on_2791 on theBenchmark for (2791ds/71622Mi) % 246.91/36.00 % (3468453)Instruction limit reached! % 246.91/36.00 % (3468453)------------------------------ % 246.91/36.00 % (3468453)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 246.91/36.00 % (3468453)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 246.91/36.00 % (3468453)CaDiCaL version: 2.1.3 % 246.91/36.00 % (3468453)Termination reason: Instruction limit % 246.91/36.00 % (3468453)Termination phase: Saturation % 246.91/36.00 % (3468453)Time elapsed: 12.361 s % 246.91/36.00 % (3468453)Peak memory usage: 95 MB % 246.91/36.00 % (3468453)Instructions burned: 17166 (million) % 246.91/36.00 % (3468514)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=2732472832:i=24001:kws=precedence:nm=0:rtra=on_2760 on theBenchmark for (2760ds/24001Mi) % 292.08/42.29 % (3468503)Instruction limit reached! % 292.08/42.29 % (3468503)------------------------------ % 292.08/42.29 % (3468503)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 292.08/42.29 % (3468503)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 292.08/42.29 % (3468503)CaDiCaL version: 2.1.3 % 292.08/42.29 % (3468503)Termination reason: Instruction limit % 292.08/42.29 % (3468503)Termination phase: Saturation % 292.08/42.29 % (3468503)Time elapsed: 4.601 s % 292.08/42.29 % (3468503)Peak memory usage: 128 MB % 292.08/42.29 % (3468503)Instructions burned: 6259 (million) % 292.08/42.29 % (3468518)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=1391511208:i=2076:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2749 on theBenchmark for (2749ds/2076Mi) % 292.08/42.29 % (3468489)Instruction limit reached! % 292.08/42.29 % (3468489)------------------------------ % 292.08/42.29 % (3468489)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 292.08/42.29 % (3468489)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 292.08/42.29 % (3468489)CaDiCaL version: 2.1.3 % 292.08/42.29 % (3468489)Termination reason: Instruction limit % 292.08/42.29 % (3468489)Termination phase: Saturation % 292.08/42.29 % (3468489)Time elapsed: 8.494 s % 292.08/42.29 % (3468489)Peak memory usage: 126 MB % 292.08/42.29 % (3468489)Instructions burned: 11748 (million) % 292.08/42.29 % (3468520)dis+21_20_to=lakbo:si=on:alasca=on:sp=const_max:uwa=alasca_main:sac=on:random_seed=589711200:s2a=on:i=83971:s2at=4:bd=all:ins=1:rtra=on_2739 on theBenchmark for (2739ds/83971Mi) % 292.08/42.29 % (3468518)Instruction limit reached! % 292.08/42.29 % (3468518)------------------------------ % 292.08/42.29 % (3468518)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 292.08/42.29 % (3468518)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 292.08/42.29 % (3468518)CaDiCaL version: 2.1.3 % 292.08/42.29 % (3468518)Termination reason: Instruction limit % 292.08/42.29 % (3468518)Termination phase: Saturation % 292.08/42.29 % (3468518)Time elapsed: 1.575 s % 292.08/42.29 % (3468518)Peak memory usage: 116 MB % 292.08/42.29 % (3468518)Instructions burned: 2077 (million) % 292.08/42.29 % (3468522)lrs+1011_5:1_to=lpo:sil=128000:sas=z3:si=on:norm_ineq=on:tha=some:random_seed=629830626:i=83944:rtra=on_2730 on theBenchmark for (2730ds/83944Mi) % 292.08/42.29 % (3468416)Refutation not found, non-redundant clauses discarded % 292.08/42.29 % (3468416)------------------------------ % 292.08/42.29 % (3468416)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 292.08/42.29 % (3468416)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 292.08/42.29 % (3468416)CaDiCaL version: 2.1.3 % 292.08/42.29 % (3468416)Termination reason: Refutation not found, non-redundant clauses discarded % 292.08/42.29 % (3468416)Time elapsed: 23.151 s % 292.08/42.29 % (3468416)Peak memory usage: 130 MB % 292.08/42.29 % (3468416)Instructions burned: 32738 (million) % 292.08/42.29 % (3468416)------------------------------ % 292.08/42.29 % (3468416)------------------------------ % 292.08/42.29 % (3468524)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=2918206101:i=9201:rtra=on_2694 on theBenchmark for (2694ds/9201Mi) % 292.08/42.29 % (3468506)Instruction limit reached! % 292.08/42.29 % (3468506)------------------------------ % 292.08/42.29 % (3468506)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 292.08/42.29 % (3468506)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 292.08/42.29 % (3468506)CaDiCaL version: 2.1.3 % 292.08/42.29 % (3468506)Termination reason: Instruction limit % 292.08/42.29 % (3468506)Termination phase: Saturation % 292.08/42.29 % (3468506)Time elapsed: 11.448 s % 292.08/42.29 % (3468506)Peak memory usage: 93 MB % 292.08/42.29 % (3468506)Instructions burned: 34004 (million) % 292.08/42.29 % (3468569)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 % 292.08/42.29 % (3468569)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=4022730043:i=6806:aac=none:nm=0:rtra=on:rawr=on_2678 on theBenchmark for (2678ds/6806Mi) % 292.08/42.29 % (3468569)Instruction limit reached! % 292.08/42.29 % (3468569)------------------------------ % 292.08/42.29 % (3468569)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.58/43.43 % (3468569)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.58/43.43 % (3468569)CaDiCaL version: 2.1.3 % 300.58/43.43 % (3468569)Termination reason: Instruction limit % 300.58/43.43 % (3468569)Termination phase: Saturation % 300.58/43.43 % (3468569)Time elapsed: 1.338 s % 300.58/43.43 % (3468569)Peak memory usage: 125 MB % 300.58/43.43 % (3468569)Instructions burned: 6810 (million) % 300.58/43.43 % (3468571)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=281976221:s2a=on:i=3553:nm=0:rtra=on_2664 on theBenchmark for (2664ds/3553Mi) % 300.58/43.43 % (3468571)Instruction limit reached! % 300.58/43.43 % (3468571)------------------------------ % 300.58/43.43 % (3468571)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.58/43.43 % (3468571)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.58/43.43 % (3468571)CaDiCaL version: 2.1.3 % 300.58/43.43 % (3468571)Termination reason: Instruction limit % 300.58/43.43 % (3468571)Termination phase: Saturation % 300.58/43.43 % (3468571)Time elapsed: 0.691 s % 300.58/43.43 % (3468571)Peak memory usage: 93 MB % 300.58/43.43 % (3468571)Instructions burned: 3557 (million) % 300.58/43.43 % (3468573)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=62377820:thitd=on:cond=on:i=2064:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2656 on theBenchmark for (2656ds/2064Mi) % 300.58/43.43 % (3468524)Instruction limit reached! % 300.58/43.43 % (3468524)------------------------------ % 300.58/43.43 % (3468524)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.58/43.43 % (3468524)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.58/43.43 % (3468524)CaDiCaL version: 2.1.3 % 300.58/43.43 % (3468524)Termination reason: Instruction limit % 300.58/43.43 % (3468524)Termination phase: Saturation % 300.58/43.43 % (3468524)Time elapsed: 3.767 s % 300.58/43.43 % (3468524)Peak memory usage: 92 MB % 300.58/43.43 % (3468524)Instructions burned: 9202 (million) % 300.58/43.43 % (3468575)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=1430122924:cond=fast:i=20260:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2654 on theBenchmark for (2654ds/20260Mi) % 300.58/43.43 % (3468575)Refutation not found, incomplete strategy % 300.58/43.43 % (3468575)------------------------------ % 300.58/43.43 % (3468575)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.58/43.43 % (3468575)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.58/43.43 % (3468575)CaDiCaL version: 2.1.3 % 300.58/43.43 % (3468575)Termination reason: Refutation not found, incomplete strategy % 300.58/43.43 % (3468575)Time elapsed: 0.078 s % 300.58/43.43 % (3468575)Peak memory usage: 113 MB % 300.58/43.43 % (3468575)Instructions burned: 147 (million) % 300.58/43.43 % (3468573)Instruction limit reached! % 300.58/43.43 % (3468573)------------------------------ % 300.58/43.43 % (3468573)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.58/43.43 % (3468573)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.58/43.43 % (3468573)CaDiCaL version: 2.1.3 % 300.58/43.43 % (3468573)Termination reason: Instruction limit % 300.58/43.43 % (3468573)Termination phase: Saturation % 300.58/43.43 % (3468573)Time elapsed: 0.431 s % 300.58/43.43 % (3468573)Peak memory usage: 134 MB % 300.58/43.43 % (3468573)Instructions burned: 2069 (million) % 300.58/43.43 % (3468575)------------------------------ % 300.58/43.43 % (3468575)------------------------------ % 300.58/43.43 % (3468577)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=3346128443:avsq=on:i=1244:avsqr=1,16:rtra=on:rawr=on_2650 on theBenchmark for (2650ds/1244Mi) % 300.58/43.43 % (3468578)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=2087443964:i=58261:doe=on:nm=0:rtra=on:gtg=exists_sym_2649 on theBenchmark for (2649ds/58261Mi) % 300.58/43.43 % (3468577)Instruction limit reached! % 300.58/43.43 % (3468577)------------------------------ % 300.58/43.43 % (3468577)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.58/43.43 % (3468577)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.58/43.43 % (3468577)CaDiCaL version: 2.1.3 % 300.58/43.43 % (3468577)Termination reason: Instruction limit % 300.58/43.43 % (3468577)Termination phase: Saturation % 300.58/43.43 % (3468577)Time elapsed: 0.261 s % 300.58/43.43 % (3468577)Peak memory usage: 116 MB % 300.58/43.43 % (3468577)Instructions % 300.58/43.44 Terminated %------------------------------------------------------------------------------