%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWX135_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 : n017.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:45:57 PM UTC 2026 % Result : Timeout 289.43s 41.70s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWX135_1 : TPTP v9.3.1. Released v9.3.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.09/0.22 % Computer : n017.cluster.edu % 0.09/0.22 % Model : x86_64 x86_64 % 0.09/0.22 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.22 % Memory : 8046.5625MB % 0.09/0.22 % OS : Linux 6.8.0-71-generic % 0.09/0.22 % CPULimit : 300 % 0.09/0.22 % WCLimit : 300 % 0.09/0.22 % DateTime : Mon Sep 28 14:58:36 UTC 2026 % 0.09/0.22 % CPUTime : % 0.09/0.23 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.23/0.28 Running first-order theorem proving % 0.23/0.28 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 4.88/1.61 % (3616160)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule. % 4.88/1.61 % (3616165)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=749544069:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2998 on theBenchmark for (2998ds/12Mi) % 4.88/1.61 % (3616170)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=986216469:i=46:rtra=on_2998 on theBenchmark for (2998ds/46Mi) % 4.88/1.61 % (3616165)Instruction limit reached! % 4.88/1.61 % (3616165)------------------------------ % 4.88/1.61 % (3616165)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.88/1.61 % (3616165)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.88/1.61 % (3616165)CaDiCaL version: 2.1.3 % 4.88/1.61 % (3616165)Termination reason: Instruction limit % 4.88/1.61 % (3616165)Termination phase: Property scanning % 4.88/1.61 % (3616165)Time elapsed: 0.005 s % 4.88/1.61 % (3616165)Peak memory usage: 85 MB % 4.88/1.61 % (3616165)Instructions burned: 12 (million) % 4.88/1.61 % (3616170)Instruction limit reached! % 4.88/1.61 % (3616170)------------------------------ % 4.88/1.61 % (3616170)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.88/1.61 % (3616170)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.88/1.61 % (3616170)CaDiCaL version: 2.1.3 % 4.88/1.61 % (3616170)Termination reason: Instruction limit % 4.88/1.61 % (3616170)Termination phase: Property scanning % 4.88/1.61 % (3616170)Time elapsed: 0.020 s % 4.88/1.61 % (3616170)Peak memory usage: 85 MB % 4.88/1.61 % (3616170)Instructions burned: 47 (million) % 4.88/1.61 % (3616166)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=650471426:i=307:kws=precedence:nm=0:rtra=on_2998 on theBenchmark for (2998ds/307Mi) % 4.88/1.61 % (3616168)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=2271035850:s2a=on:i=7:rtra=on:inst=on_2998 on theBenchmark for (2998ds/7Mi) % 4.88/1.61 % (3616169)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=2443743920:i=4:rtra=on_2998 on theBenchmark for (2998ds/4Mi) % 4.88/1.61 % (3616167)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=4042899371:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/201Mi) % 4.88/1.61 % (3616169)Instruction limit reached! % 4.88/1.61 % (3616169)------------------------------ % 4.88/1.61 % (3616169)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.88/1.61 % (3616169)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.88/1.61 % (3616169)CaDiCaL version: 2.1.3 % 4.88/1.61 % (3616169)Termination reason: Instruction limit % 4.88/1.61 % (3616169)Termination phase: shuffling % 4.88/1.61 % (3616169)Time elapsed: 0.003 s % 4.88/1.61 % (3616169)Peak memory usage: 84 MB % 4.88/1.61 % (3616169)Instructions burned: 4 (million) % 4.88/1.61 % (3616168)Instruction limit reached! % 4.88/1.61 % (3616168)------------------------------ % 4.88/1.61 % (3616168)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.88/1.61 % (3616168)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.88/1.61 % (3616168)CaDiCaL version: 2.1.3 % 4.88/1.61 % (3616168)Termination reason: Instruction limit % 4.88/1.61 % (3616168)Termination phase: Property scanning % 4.88/1.61 % (3616168)Time elapsed: 0.006 s % 4.88/1.61 % (3616168)Peak memory usage: 85 MB % 4.88/1.61 % (3616168)Instructions burned: 7 (million) % 4.88/1.61 % (3616171)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=1419985055:i=33:rtra=on_2998 on theBenchmark for (2998ds/33Mi) % 4.88/1.61 % (3616171)Instruction limit reached! % 4.88/1.61 % (3616171)------------------------------ % 4.88/1.61 % (3616171)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.88/1.61 % (3616171)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.88/1.61 % (3616171)CaDiCaL version: 2.1.3 % 4.88/1.61 % (3616171)Termination reason: Instruction limit % 4.88/1.61 % (3616171)Termination phase: Property scanning % 4.88/1.61 % (3616171)Time elapsed: 0.025 s % 4.88/1.61 % (3616171)Peak memory usage: 85 MB % 4.88/1.61 % (3616171)Instructions burned: 33 (million) % 4.88/1.61 % (3616175)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=263065799:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2997 on theBenchmark for (2997ds/29Mi) % 4.88/1.61 % (3616175)Instruction limit reached! % 5.84/1.79 % (3616175)------------------------------ % 5.84/1.79 % (3616175)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.84/1.79 % (3616175)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.84/1.79 % (3616175)CaDiCaL version: 2.1.3 % 5.84/1.79 % (3616175)Termination reason: Instruction limit % 5.84/1.79 % (3616175)Termination phase: Property scanning % 5.84/1.79 % (3616175)Time elapsed: 0.013 s % 5.84/1.79 % (3616175)Peak memory usage: 85 MB % 5.84/1.79 % (3616175)Instructions burned: 31 (million) % 5.84/1.79 % (3616174)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=1681268156:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2997 on theBenchmark for (2997ds/14Mi) % 5.84/1.79 % (3616174)Instruction limit reached! % 5.84/1.79 % (3616174)------------------------------ % 5.84/1.79 % (3616174)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.84/1.79 % (3616174)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.84/1.79 % (3616174)CaDiCaL version: 2.1.3 % 5.84/1.79 % (3616174)Termination reason: Instruction limit % 5.84/1.79 % (3616174)Termination phase: Property scanning % 5.84/1.79 % (3616174)Time elapsed: 0.011 s % 5.84/1.79 % (3616174)Peak memory usage: 85 MB % 5.84/1.79 % (3616174)Instructions burned: 14 (million) % 5.84/1.79 % (3616167)Instruction limit reached! % 5.84/1.79 % (3616167)------------------------------ % 5.84/1.79 % (3616167)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.84/1.79 % (3616167)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.84/1.79 % (3616167)CaDiCaL version: 2.1.3 % 5.84/1.79 % (3616167)Termination reason: Instruction limit % 5.84/1.79 % (3616167)Termination phase: Saturation % 5.84/1.79 % (3616167)Time elapsed: 0.183 s % 5.84/1.79 % (3616167)Peak memory usage: 111 MB % 5.84/1.79 % (3616167)Instructions burned: 202 (million) % 5.84/1.79 % (3616181)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=2825089016:i=24:canc=force:rtra=on_2996 on theBenchmark for (2996ds/24Mi) % 5.84/1.79 % (3616181)Instruction limit reached! % 5.84/1.79 % (3616181)------------------------------ % 5.84/1.79 % (3616181)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.84/1.79 % (3616181)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.84/1.79 % (3616181)CaDiCaL version: 2.1.3 % 5.84/1.79 % (3616181)Termination reason: Instruction limit % 5.84/1.79 % (3616181)Termination phase: Property scanning % 5.84/1.79 % (3616181)Time elapsed: 0.019 s % 5.84/1.79 % (3616181)Peak memory usage: 85 MB % 5.84/1.79 % (3616181)Instructions burned: 25 (million) % 5.84/1.79 % (3616180)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=1170008649:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2996 on theBenchmark for (2996ds/16Mi) % 5.84/1.79 % (3616180)Instruction limit reached! % 5.84/1.79 % (3616180)------------------------------ % 5.84/1.79 % (3616180)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.84/1.79 % (3616180)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.84/1.79 % (3616180)CaDiCaL version: 2.1.3 % 5.84/1.79 % (3616180)Termination reason: Instruction limit % 5.84/1.79 % (3616180)Termination phase: Property scanning % 5.84/1.79 % (3616180)Time elapsed: 0.013 s % 5.84/1.79 % (3616180)Peak memory usage: 85 MB % 5.84/1.79 % (3616180)Instructions burned: 17 (million) % 5.84/1.79 % (3616166)Instruction limit reached! % 5.84/1.79 % (3616166)------------------------------ % 5.84/1.79 % (3616166)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.84/1.79 % (3616166)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.84/1.79 % (3616166)CaDiCaL version: 2.1.3 % 5.84/1.79 % (3616166)Termination reason: Instruction limit % 5.84/1.79 % (3616166)Termination phase: Saturation % 5.84/1.79 % (3616166)Time elapsed: 0.256 s % 5.84/1.79 % (3616166)Peak memory usage: 112 MB % 5.84/1.79 % (3616166)Instructions burned: 307 (million) % 5.84/1.79 % (3616183)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=3173561038:i=27:canc=cautious:fsr=off:rtra=on_2996 on theBenchmark for (2996ds/27Mi) % 5.84/1.79 % (3616183)Instruction limit reached! % 5.84/1.79 % (3616183)------------------------------ % 5.84/1.79 % (3616183)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.84/1.79 % (3616183)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.03/2.03 % (3616183)CaDiCaL version: 2.1.3 % 7.03/2.03 % (3616183)Termination reason: Instruction limit % 7.03/2.03 % (3616183)Termination phase: Property scanning % 7.03/2.03 % (3616183)Time elapsed: 0.021 s % 7.03/2.03 % (3616183)Peak memory usage: 85 MB % 7.03/2.03 % (3616183)Instructions burned: 27 (million) % 7.03/2.03 % (3616185)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=2823311069:i=85:gtgl=4:rtra=on:gtg=exists_sym_2995 on theBenchmark for (2995ds/85Mi) % 7.03/2.03 % (3616193)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=1503750344:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2993 on theBenchmark for (2993ds/66Mi) % 7.03/2.03 % (3616185)Instruction limit reached! % 7.03/2.03 % (3616185)------------------------------ % 7.03/2.03 % (3616185)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.03/2.03 % (3616185)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.03/2.03 % (3616185)CaDiCaL version: 2.1.3 % 7.03/2.03 % (3616185)Termination reason: Instruction limit % 7.03/2.03 % (3616185)Termination phase: Property scanning % 7.03/2.03 % (3616185)Time elapsed: 0.065 s % 7.03/2.03 % (3616185)Peak memory usage: 85 MB % 7.03/2.03 % (3616185)Instructions burned: 85 (million) % 7.03/2.03 % (3616193)Instruction limit reached! % 7.03/2.03 % (3616193)------------------------------ % 7.03/2.03 % (3616193)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.03/2.03 % (3616193)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.03/2.03 % (3616193)CaDiCaL version: 2.1.3 % 7.03/2.03 % (3616193)Termination reason: Instruction limit % 7.03/2.03 % (3616193)Termination phase: Property scanning % 7.03/2.03 % (3616193)Time elapsed: 0.014 s % 7.03/2.03 % (3616193)Peak memory usage: 86 MB % 7.03/2.03 % (3616193)Instructions burned: 69 (million) % 7.03/2.03 % (3616188)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=2261815148:i=181:rtra=on:ss=axioms:ev=cautious_2994 on theBenchmark for (2994ds/181Mi) % 7.03/2.03 % (3616187)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=1610127687:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2994 on theBenchmark for (2994ds/2Mi) % 7.03/2.03 % (3616187)Instruction limit reached! % 7.03/2.03 % (3616187)------------------------------ % 7.03/2.03 % (3616187)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.03/2.03 % (3616187)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.03/2.03 % (3616187)CaDiCaL version: 2.1.3 % 7.03/2.03 % (3616187)Termination reason: Instruction limit % 7.03/2.03 % (3616187)Termination phase: shuffling % 7.03/2.03 % (3616187)Time elapsed: 0.002 s % 7.03/2.03 % (3616187)Peak memory usage: 84 MB % 7.03/2.03 % (3616187)Instructions burned: 3 (million) % 7.03/2.03 % (3616188)Refutation not found, incomplete strategy % 7.03/2.03 % (3616188)------------------------------ % 7.03/2.03 % (3616188)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.03/2.03 % (3616188)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.03/2.03 % (3616188)CaDiCaL version: 2.1.3 % 7.03/2.03 % (3616188)Termination reason: Refutation not found, incomplete strategy % 7.03/2.03 % (3616188)Time elapsed: 0.031 s % 7.03/2.03 % (3616188)Peak memory usage: 87 MB % 7.03/2.03 % (3616188)Instructions burned: 40 (million) % 7.03/2.03 % (3616191)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=2707810244:i=4:ep=RST:ins=2:rtra=on_2994 on theBenchmark for (2994ds/4Mi) % 7.03/2.03 % (3616191)Instruction limit reached! % 7.03/2.03 % (3616191)------------------------------ % 7.03/2.03 % (3616191)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.03/2.03 % (3616191)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.03/2.03 % (3616191)CaDiCaL version: 2.1.3 % 7.03/2.03 % (3616191)Termination reason: Instruction limit % 7.03/2.03 % (3616191)Termination phase: shuffling % 7.03/2.03 % (3616191)Time elapsed: 0.003 s % 7.03/2.03 % (3616191)Peak memory usage: 85 MB % 7.03/2.03 % (3616191)Instructions burned: 4 (million) % 7.03/2.03 % (3616194)lrs+10_1_thi=all:si=on:fd=off:random_seed=2621593488:i=53:rtra=on:gtg=all_2993 on theBenchmark for (2993ds/53Mi) % 7.03/2.03 % (3616194)Instruction limit reached! % 7.03/2.03 % (3616194)------------------------------ % 7.03/2.03 % (3616194)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.03/2.03 % (3616194)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.46/2.35 % (3616194)CaDiCaL version: 2.1.3 % 10.46/2.35 % (3616194)Termination reason: Instruction limit % 10.46/2.35 % (3616194)Termination phase: Property scanning % 10.46/2.35 % (3616194)Time elapsed: 0.041 s % 10.46/2.35 % (3616194)Peak memory usage: 85 MB % 10.46/2.35 % (3616194)Instructions burned: 53 (million) % 10.46/2.35 % (3616201)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=2860357738:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2993 on theBenchmark for (2993ds/8Mi) % 10.46/2.35 % (3616201)Instruction limit reached! % 10.46/2.35 % (3616201)------------------------------ % 10.46/2.35 % (3616201)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.46/2.35 % (3616201)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.46/2.35 % (3616201)CaDiCaL version: 2.1.3 % 10.46/2.35 % (3616201)Termination reason: Instruction limit % 10.46/2.35 % (3616201)Termination phase: Property scanning % 10.46/2.35 % (3616201)Time elapsed: 0.007 s % 10.46/2.35 % (3616201)Peak memory usage: 85 MB % 10.46/2.35 % (3616201)Instructions burned: 9 (million) % 10.46/2.35 % (3616207)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=825503782:i=2:doe=on:canc=force:asg=cautious:rtra=on_2992 on theBenchmark for (2992ds/2Mi) % 10.46/2.35 % (3616207)Instruction limit reached! % 10.46/2.35 % (3616207)------------------------------ % 10.46/2.35 % (3616207)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.46/2.35 % (3616207)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.46/2.35 % (3616207)CaDiCaL version: 2.1.3 % 10.46/2.35 % (3616207)Termination reason: Instruction limit % 10.46/2.35 % (3616207)Termination phase: shuffling % 10.46/2.35 % (3616207)Time elapsed: 0.001 s % 10.46/2.35 % (3616207)Peak memory usage: 85 MB % 10.46/2.35 % (3616207)Instructions burned: 2 (million) % 10.46/2.35 % (3616206)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=961114340:st=3:i=2:rtra=on:ss=axioms_2992 on theBenchmark for (2992ds/2Mi) % 10.46/2.35 % (3616206)Instruction limit reached! % 10.46/2.35 % (3616206)------------------------------ % 10.46/2.35 % (3616206)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.46/2.35 % (3616206)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.46/2.35 % (3616206)CaDiCaL version: 2.1.3 % 10.46/2.35 % (3616206)Termination reason: Instruction limit % 10.46/2.35 % (3616206)Termination phase: shuffling % 10.46/2.35 % (3616206)Time elapsed: 0.002 s % 10.46/2.35 % (3616206)Peak memory usage: 84 MB % 10.46/2.35 % (3616206)Instructions burned: 2 (million) % 10.46/2.35 % (3616210)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=3603613651:i=127:doe=on:rtra=on_2992 on theBenchmark for (2992ds/127Mi) % 10.46/2.35 % (3616212)dis+10_1_si=on:random_seed=2453521334:i=10:ep=R:rtra=on_2991 on theBenchmark for (2991ds/10Mi) % 10.46/2.35 % (3616217)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=2330539395:avsq=on:i=35:doe=on:thsqd=64:nm=64:fsr=off:thsqc=32:rtra=on:tac=light:ss=included:thsq=on:ev=off:sgt=32_2990 on theBenchmark for (2990ds/35Mi) % 10.46/2.35 % (3616218)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=3806941864:i=2:fsr=off:rtra=on:inst=on_2990 on theBenchmark for (2990ds/2Mi) % 10.46/2.35 % (3616212)Instruction limit reached! % 10.46/2.35 % (3616212)------------------------------ % 10.46/2.35 % (3616212)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.46/2.35 % (3616212)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.46/2.35 % (3616212)CaDiCaL version: 2.1.3 % 10.46/2.35 % (3616212)Termination reason: Instruction limit % 10.46/2.35 % (3616212)Termination phase: Property scanning % 10.46/2.35 % (3616212)Time elapsed: 0.008 s % 10.46/2.35 % (3616212)Peak memory usage: 85 MB % 10.46/2.35 % (3616212)Instructions burned: 11 (million) % 10.46/2.35 % (3616218)Instruction limit reached! % 10.46/2.35 % (3616218)------------------------------ % 10.46/2.35 % (3616218)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.46/2.35 % (3616218)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.46/2.35 % (3616218)CaDiCaL version: 2.1.3 % 10.46/2.35 % (3616218)Termination reason: Instruction limit % 10.46/2.35 % (3616218)Termination phase: shuffling % 10.46/2.35 % (3616218)Time elapsed: 0.002 s % 11.65/2.74 % (3616218)Peak memory usage: 85 MB % 11.65/2.74 % (3616218)Instructions burned: 4 (million) % 11.65/2.74 % (3616217)Instruction limit reached! % 11.65/2.74 % (3616217)------------------------------ % 11.65/2.74 % (3616217)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.65/2.74 % (3616217)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.65/2.74 % (3616217)CaDiCaL version: 2.1.3 % 11.65/2.74 % (3616217)Termination reason: Instruction limit % 11.65/2.74 % (3616217)Termination phase: Property scanning % 11.65/2.74 % (3616217)Time elapsed: 0.014 s % 11.65/2.74 % (3616217)Peak memory usage: 85 MB % 11.65/2.74 % (3616217)Instructions burned: 35 (million) % 11.65/2.74 % (3616214)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=2139444658:i=26:canc=cautious:av=off:rtra=on_2991 on theBenchmark for (2991ds/26Mi) % 11.65/2.74 % (3616214)Instruction limit reached! % 11.65/2.74 % (3616214)------------------------------ % 11.65/2.74 % (3616214)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.65/2.74 % (3616214)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.65/2.74 % (3616214)CaDiCaL version: 2.1.3 % 11.65/2.74 % (3616214)Termination reason: Instruction limit % 11.65/2.74 % (3616214)Termination phase: Property scanning % 11.65/2.74 % (3616214)Time elapsed: 0.020 s % 11.65/2.74 % (3616214)Peak memory usage: 85 MB % 11.65/2.74 % (3616214)Instructions burned: 26 (million) % 11.65/2.74 % (3616210)Instruction limit reached! % 11.65/2.74 % (3616210)------------------------------ % 11.65/2.74 % (3616210)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.65/2.74 % (3616210)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.65/2.74 % (3616210)CaDiCaL version: 2.1.3 % 11.65/2.74 % (3616210)Termination reason: Instruction limit % 11.65/2.74 % (3616210)Termination phase: Saturation % 11.65/2.74 % (3616210)Time elapsed: 0.125 s % 11.65/2.74 % (3616210)Peak memory usage: 112 MB % 11.65/2.74 % (3616210)Instructions burned: 127 (million) % 11.65/2.74 % (3616188)------------------------------ % 11.65/2.74 % (3616188)------------------------------ % 11.65/2.74 % (3616220)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=34568354:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2990 on theBenchmark for (2990ds/8Mi) % 11.65/2.74 % (3616220)Instruction limit reached! % 11.65/2.74 % (3616220)------------------------------ % 11.65/2.74 % (3616220)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.65/2.74 % (3616220)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.65/2.74 % (3616220)CaDiCaL version: 2.1.3 % 11.65/2.74 % (3616220)Termination reason: Instruction limit % 11.65/2.74 % (3616220)Termination phase: Property scanning % 11.65/2.74 % (3616220)Time elapsed: 0.006 s % 11.65/2.74 % (3616220)Peak memory usage: 85 MB % 11.65/2.74 % (3616220)Instructions burned: 8 (million) % 11.65/2.74 % (3616225)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=4121274679:i=370:ep=RS:fsr=off:rtra=on_2989 on theBenchmark for (2989ds/370Mi) % 11.65/2.74 % (3616229)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=2681886465:i=10:rtra=on_2988 on theBenchmark for (2988ds/10Mi) % 11.65/2.74 % (3616229)Instruction limit reached! % 11.65/2.74 % (3616229)------------------------------ % 11.65/2.74 % (3616229)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.65/2.74 % (3616229)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.65/2.74 % (3616229)CaDiCaL version: 2.1.3 % 11.65/2.74 % (3616229)Termination reason: Instruction limit % 11.65/2.74 % (3616229)Termination phase: Property scanning % 11.65/2.74 % (3616229)Time elapsed: 0.005 s % 11.65/2.74 % (3616229)Peak memory usage: 85 MB % 11.65/2.74 % (3616229)Instructions burned: 13 (million) % 11.65/2.74 % (3616227)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=1130818730:i=226:rtra=on:gtg=position:ss=axioms_2989 on theBenchmark for (2989ds/226Mi) % 11.65/2.74 % (3616226)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=1743028689:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2989 on theBenchmark for (2989ds/13Mi) % 11.65/2.74 % (3616226)Instruction limit reached! % 11.65/2.74 % (3616226)------------------------------ % 11.65/2.74 % (3616226)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.65/2.74 % (3616226)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.72/3.14 % (3616226)CaDiCaL version: 2.1.3 % 16.72/3.14 % (3616226)Termination reason: Instruction limit % 16.72/3.14 % (3616226)Termination phase: Property scanning % 16.72/3.14 % (3616226)Time elapsed: 0.011 s % 16.72/3.14 % (3616226)Peak memory usage: 85 MB % 16.72/3.14 % (3616226)Instructions burned: 13 (million) % 16.72/3.14 % (3616230)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=2013614328:i=71:rtra=on:gtg=exists_top_2988 on theBenchmark for (2988ds/71Mi) % 16.72/3.14 % (3616227)Refutation not found, incomplete strategy % 16.72/3.14 % (3616227)------------------------------ % 16.72/3.14 % (3616227)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.72/3.14 % (3616227)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.72/3.14 % (3616227)CaDiCaL version: 2.1.3 % 16.72/3.14 % (3616227)Termination reason: Refutation not found, incomplete strategy % 16.72/3.14 % (3616227)Time elapsed: 0.088 s % 16.72/3.14 % (3616227)Peak memory usage: 111 MB % 16.72/3.14 % (3616227)Instructions burned: 72 (million) % 16.72/3.14 % (3616225)Refutation not found, incomplete strategy % 16.72/3.14 % (3616225)------------------------------ % 16.72/3.14 % (3616225)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.72/3.14 % (3616225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.72/3.14 % (3616225)CaDiCaL version: 2.1.3 % 16.72/3.14 % (3616225)Termination reason: Refutation not found, incomplete strategy % 16.72/3.14 % (3616225)Time elapsed: 0.118 s % 16.72/3.14 % (3616225)Peak memory usage: 89 MB % 16.72/3.14 % (3616225)Instructions burned: 161 (million) % 16.72/3.14 % (3616231)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=1605474583:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2988 on theBenchmark for (2988ds/75Mi) % 16.72/3.14 % (3616230)Instruction limit reached! % 16.72/3.14 % (3616230)------------------------------ % 16.72/3.14 % (3616230)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.72/3.14 % (3616230)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.72/3.14 % (3616230)CaDiCaL version: 2.1.3 % 16.72/3.14 % (3616230)Termination reason: Instruction limit % 16.72/3.14 % (3616230)Termination phase: Property scanning % 16.72/3.14 % (3616230)Time elapsed: 0.055 s % 16.72/3.14 % (3616230)Peak memory usage: 85 MB % 16.72/3.14 % (3616230)Instructions burned: 71 (million) % 16.72/3.14 % (3616233)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=1988670119:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2987 on theBenchmark for (2987ds/294Mi) % 16.72/3.14 % (3616238)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=172520864:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2986 on theBenchmark for (2986ds/130Mi) % 16.72/3.14 % (3616231)Instruction limit reached! % 16.72/3.14 % (3616231)------------------------------ % 16.72/3.14 % (3616231)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.72/3.14 % (3616231)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.72/3.14 % (3616231)CaDiCaL version: 2.1.3 % 16.72/3.14 % (3616231)Termination reason: Instruction limit % 16.72/3.14 % (3616231)Termination phase: Property scanning % 16.72/3.14 % (3616231)Time elapsed: 0.058 s % 16.72/3.14 % (3616231)Peak memory usage: 86 MB % 16.72/3.14 % (3616231)Instructions burned: 75 (million) % 16.72/3.14 % (3616239)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=2262050308:i=131:rtra=on_2986 on theBenchmark for (2986ds/131Mi) % 16.72/3.14 % (3616238)Instruction limit reached! % 16.72/3.14 % (3616238)------------------------------ % 16.72/3.14 % (3616238)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.72/3.14 % (3616238)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.72/3.14 % (3616238)CaDiCaL version: 2.1.3 % 16.72/3.14 % (3616238)Termination reason: Instruction limit % 16.72/3.14 % (3616238)Termination phase: Twee Goal Transformation % 16.72/3.14 % (3616238)Time elapsed: 0.053 s % 16.72/3.14 % (3616238)Peak memory usage: 87 MB % 16.72/3.14 % (3616238)Instructions burned: 132 (million) % 16.72/3.14 % (3616239)Instruction limit reached! % 16.72/3.14 % (3616239)------------------------------ % 16.72/3.14 % (3616239)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.72/3.14 % (3616239)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.94/3.47 % (3616239)CaDiCaL version: 2.1.3 % 16.94/3.47 % (3616239)Termination reason: Instruction limit % 16.94/3.47 % (3616239)Termination phase: Saturation % 16.94/3.47 % (3616239)Time elapsed: 0.155 s % 16.94/3.47 % (3616239)Peak memory usage: 128 MB % 16.94/3.47 % (3616239)Instructions burned: 132 (million) % 16.94/3.47 % (3616246)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=2509936569:i=307:rtra=on:gtg=exists_top_2985 on theBenchmark for (2985ds/307Mi) % 16.94/3.47 % (3616242)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=2879253874:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2985 on theBenchmark for (2985ds/40Mi) % 16.94/3.47 % (3616233)Instruction limit reached! % 16.94/3.47 % (3616233)------------------------------ % 16.94/3.47 % (3616233)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.94/3.47 % (3616233)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.94/3.47 % (3616233)CaDiCaL version: 2.1.3 % 16.94/3.47 % (3616233)Termination reason: Instruction limit % 16.94/3.47 % (3616233)Termination phase: Saturation % 16.94/3.47 % (3616233)Time elapsed: 0.222 s % 16.94/3.47 % (3616233)Peak memory usage: 90 MB % 16.94/3.47 % (3616233)Instructions burned: 294 (million) % 16.94/3.47 % (3616242)Instruction limit reached! % 16.94/3.47 % (3616242)------------------------------ % 16.94/3.47 % (3616242)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.94/3.47 % (3616242)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.94/3.47 % (3616242)CaDiCaL version: 2.1.3 % 16.94/3.47 % (3616242)Termination reason: Instruction limit % 16.94/3.47 % (3616242)Termination phase: Property scanning % 16.94/3.47 % (3616242)Time elapsed: 0.031 s % 16.94/3.47 % (3616242)Peak memory usage: 85 MB % 16.94/3.47 % (3616242)Instructions burned: 40 (million) % 16.94/3.47 % (3616246)Refutation not found, incomplete strategy % 16.94/3.47 % (3616246)------------------------------ % 16.94/3.47 % (3616246)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.94/3.47 % (3616246)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.94/3.47 % (3616246)CaDiCaL version: 2.1.3 % 16.94/3.47 % (3616246)Termination reason: Refutation not found, incomplete strategy % 16.94/3.47 % (3616246)Time elapsed: 0.088 s % 16.94/3.47 % (3616246)Peak memory usage: 89 MB % 16.94/3.47 % (3616246)Instructions burned: 226 (million) % 16.94/3.47 % (3616227)------------------------------ % 16.94/3.47 % (3616227)------------------------------ % 16.94/3.47 % (3616225)------------------------------ % 16.94/3.47 % (3616225)------------------------------ % 16.94/3.47 % (3616247)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=1846756789:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2984 on theBenchmark for (2984ds/598Mi) % 16.94/3.47 % (3616248)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=2167751460:i=131:canc=cautious:fsr=off:rtra=on_2983 on theBenchmark for (2983ds/131Mi) % 16.94/3.47 % (3616252)dis+10_1_si=on:random_seed=3354774982:s2a=on:i=1000:rtra=on:gtg=exists_all_2982 on theBenchmark for (2982ds/1000Mi) % 16.94/3.47 % (3616251)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=2157585138:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2983 on theBenchmark for (2983ds/259Mi) % 16.94/3.47 % (3616246)------------------------------ % 16.94/3.47 % (3616246)------------------------------ % 16.94/3.47 % (3616251)Refutation not found, incomplete strategy % 16.94/3.47 % (3616251)------------------------------ % 16.94/3.47 % (3616251)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.94/3.47 % (3616251)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.94/3.47 % (3616251)CaDiCaL version: 2.1.3 % 16.94/3.47 % (3616251)Termination reason: Refutation not found, incomplete strategy % 16.94/3.47 % (3616251)Time elapsed: 0.089 s % 16.94/3.47 % (3616251)Peak memory usage: 111 MB % 16.94/3.47 % (3616251)Instructions burned: 76 (million) % 16.94/3.47 % (3616248)Instruction limit reached! % 16.94/3.47 % (3616248)------------------------------ % 16.94/3.47 % (3616248)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.94/3.47 % (3616248)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.94/3.47 % (3616248)CaDiCaL version: 2.1.3 % 16.94/3.47 % (3616248)Termination reason: Instruction limit % 16.94/3.47 % (3616248)Termination phase: Saturation % 16.94/3.47 % (3616248)Time elapsed: 0.128 s % 16.94/3.47 % (3616248)Peak memory usage: 111 MB % 19.65/3.87 % (3616248)Instructions burned: 132 (million) % 19.65/3.87 % (3616255)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=294933502:i=141:doe=on:rtra=on_2982 on theBenchmark for (2982ds/141Mi) % 19.65/3.87 % (3616254)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=2293203123:i=383:fsr=off:rtra=on:ev=force_2982 on theBenchmark for (2982ds/383Mi) % 19.65/3.87 % (3616255)Instruction limit reached! % 19.65/3.87 % (3616255)------------------------------ % 19.65/3.87 % (3616255)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.65/3.87 % (3616255)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.65/3.87 % (3616255)CaDiCaL version: 2.1.3 % 19.65/3.87 % (3616255)Termination reason: Instruction limit % 19.65/3.87 % (3616255)Termination phase: Saturation % 19.65/3.87 % (3616255)Time elapsed: 0.105 s % 19.65/3.87 % (3616255)Peak memory usage: 88 MB % 19.65/3.87 % (3616255)Instructions burned: 142 (million) % 19.65/3.87 % (3616259)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=3641637283:i=65:nm=16:rtra=on_2980 on theBenchmark for (2980ds/65Mi) % 19.65/3.87 % (3616259)Instruction limit reached! % 19.65/3.87 % (3616259)------------------------------ % 19.65/3.87 % (3616259)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.65/3.87 % (3616259)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.65/3.87 % (3616259)CaDiCaL version: 2.1.3 % 19.65/3.87 % (3616259)Termination reason: Instruction limit % 19.65/3.87 % (3616259)Termination phase: Saturation % 19.65/3.87 % (3616259)Time elapsed: 0.026 s % 19.65/3.87 % (3616259)Peak memory usage: 88 MB % 19.65/3.87 % (3616259)Instructions burned: 67 (million) % 19.65/3.87 % (3616260)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=689484265:i=121:nm=16:rtra=on_2979 on theBenchmark for (2979ds/121Mi) % 19.65/3.87 % (3616247)Instruction limit reached! % 19.65/3.87 % (3616247)------------------------------ % 19.65/3.87 % (3616247)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.65/3.87 % (3616247)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.65/3.87 % (3616247)CaDiCaL version: 2.1.3 % 19.65/3.87 % (3616247)Termination reason: Instruction limit % 19.65/3.87 % (3616247)Termination phase: Saturation % 19.65/3.87 % (3616247)Time elapsed: 0.521 s % 19.65/3.87 % (3616247)Peak memory usage: 136 MB % 19.65/3.87 % (3616247)Instructions burned: 599 (million) % 19.65/3.87 % (3616254)Instruction limit reached! % 19.65/3.87 % (3616254)------------------------------ % 19.65/3.87 % (3616254)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.65/3.87 % (3616254)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.65/3.87 % (3616254)CaDiCaL version: 2.1.3 % 19.65/3.87 % (3616254)Termination reason: Instruction limit % 19.65/3.87 % (3616254)Termination phase: Saturation % 19.65/3.87 % (3616254)Time elapsed: 0.287 s % 19.65/3.87 % (3616254)Peak memory usage: 90 MB % 19.65/3.87 % (3616254)Instructions burned: 384 (million) % 19.65/3.87 % (3616263)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=3073210645:s2a=on:i=128:s2at=5:ins=3:rtra=on_2978 on theBenchmark for (2978ds/128Mi) % 19.65/3.87 % (3616260)Instruction limit reached! % 19.65/3.87 % (3616260)------------------------------ % 19.65/3.87 % (3616260)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.65/3.87 % (3616260)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.65/3.87 % (3616260)CaDiCaL version: 2.1.3 % 19.65/3.87 % (3616260)Termination reason: Instruction limit % 19.65/3.87 % (3616260)Termination phase: Saturation % 19.65/3.87 % (3616260)Time elapsed: 0.093 s % 19.65/3.87 % (3616260)Peak memory usage: 88 MB % 19.65/3.87 % (3616260)Instructions burned: 122 (million) % 19.65/3.87 % (3616251)------------------------------ % 19.65/3.87 % (3616251)------------------------------ % 19.65/3.87 % (3616265)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=790170621:i=39:ins=3:rtra=on_2977 on theBenchmark for (2977ds/39Mi) % 19.65/3.87 % (3616265)Instruction limit reached! % 19.65/3.87 % (3616265)------------------------------ % 19.65/3.87 % (3616265)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.65/3.87 % (3616265)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.65/3.87 % (3616265)CaDiCaL version: 2.1.3 % 23.69/4.28 % (3616265)Termination reason: Instruction limit % 23.69/4.28 % (3616265)Termination phase: Property scanning % 23.69/4.28 % (3616265)Time elapsed: 0.016 s % 23.69/4.28 % (3616265)Peak memory usage: 85 MB % 23.69/4.28 % (3616265)Instructions burned: 41 (million) % 23.69/4.28 % (3616263)Instruction limit reached! % 23.69/4.28 % (3616263)------------------------------ % 23.69/4.28 % (3616263)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.69/4.28 % (3616263)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.69/4.28 % (3616263)CaDiCaL version: 2.1.3 % 23.69/4.28 % (3616263)Termination reason: Instruction limit % 23.69/4.28 % (3616263)Termination phase: Saturation % 23.69/4.28 % (3616263)Time elapsed: 0.097 s % 23.69/4.28 % (3616263)Peak memory usage: 88 MB % 23.69/4.28 % (3616263)Instructions burned: 128 (million) % 23.69/4.28 % (3616252)Instruction limit reached! % 23.69/4.28 % (3616252)------------------------------ % 23.69/4.28 % (3616252)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.69/4.28 % (3616252)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.69/4.28 % (3616252)CaDiCaL version: 2.1.3 % 23.69/4.28 % (3616252)Termination reason: Instruction limit % 23.69/4.28 % (3616252)Termination phase: Saturation % 23.69/4.28 % (3616252)Time elapsed: 0.627 s % 23.69/4.28 % (3616252)Peak memory usage: 90 MB % 23.69/4.28 % (3616252)Instructions burned: 1000 (million) % 23.69/4.28 % (3616267)dis+1010_1_to=kbo:si=on:random_seed=1654696599:i=175:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2976 on theBenchmark for (2976ds/175Mi) % 23.69/4.28 % (3616268)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=3719329115:i=329:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2976 on theBenchmark for (2976ds/329Mi) % 23.69/4.28 % (3616273)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=3365127634:i=349:rtra=on_2975 on theBenchmark for (2975ds/349Mi) % 23.69/4.28 % (3616270)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=1689253848:s2a=on:i=483:doe=on:nm=32:rtra=on_2976 on theBenchmark for (2976ds/483Mi) % 23.69/4.28 % (3616272)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=3341628602:thitd=on:i=215:nm=0:rtra=on:ev=force_2975 on theBenchmark for (2975ds/215Mi) % 23.69/4.28 % (3616267)Instruction limit reached! % 23.69/4.28 % (3616267)------------------------------ % 23.69/4.28 % (3616267)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.69/4.28 % (3616267)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.69/4.28 % (3616267)CaDiCaL version: 2.1.3 % 23.69/4.28 % (3616267)Termination reason: Instruction limit % 23.69/4.28 % (3616267)Termination phase: Property scanning % 23.69/4.28 % (3616267)Time elapsed: 0.133 s % 23.69/4.28 % (3616267)Peak memory usage: 86 MB % 23.69/4.28 % (3616267)Instructions burned: 176 (million) % 23.69/4.28 % (3616274)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=2889502346:st=2:i=295:rtra=on:ss=axioms_2975 on theBenchmark for (2975ds/295Mi) % 23.69/4.28 % (3616275)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=1896506954:i=328:kws=inv_frequency:nm=20:rtra=on_2974 on theBenchmark for (2974ds/328Mi) % 23.69/4.28 % (3616274)Refutation not found, incomplete strategy % 23.69/4.28 % (3616274)------------------------------ % 23.69/4.28 % (3616274)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.69/4.28 % (3616274)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.69/4.28 % (3616274)CaDiCaL version: 2.1.3 % 23.69/4.28 % (3616274)Termination reason: Refutation not found, incomplete strategy % 23.69/4.28 % (3616274)Time elapsed: 0.054 s % 23.69/4.28 % (3616274)Peak memory usage: 88 MB % 23.69/4.28 % (3616274)Instructions burned: 70 (million) % 23.69/4.28 % (3616273)Instruction limit reached! % 23.69/4.28 % (3616273)------------------------------ % 23.69/4.28 % (3616273)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.69/4.28 % (3616273)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.69/4.28 % (3616273)CaDiCaL version: 2.1.3 % 23.69/4.28 % (3616273)Termination reason: Instruction limit % 23.69/4.28 % (3616273)Termination phase: Saturation % 23.69/4.28 % (3616273)Time elapsed: 0.151 s % 23.69/4.28 % (3616273)Peak memory usage: 113 MB % 23.69/4.28 % (3616273)Instructions burned: 352 (million) % 25.38/4.74 % (3616272)Instruction limit reached! % 25.38/4.74 % (3616272)------------------------------ % 25.38/4.74 % (3616272)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.38/4.74 % (3616272)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.38/4.74 % (3616272)CaDiCaL version: 2.1.3 % 25.38/4.74 % (3616272)Termination reason: Instruction limit % 25.38/4.74 % (3616272)Termination phase: Saturation % 25.38/4.74 % (3616272)Time elapsed: 0.217 s % 25.38/4.74 % (3616272)Peak memory usage: 129 MB % 25.38/4.74 % (3616272)Instructions burned: 215 (million) % 25.38/4.74 % (3616268)Instruction limit reached! % 25.38/4.74 % (3616268)------------------------------ % 25.38/4.74 % (3616268)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.38/4.74 % (3616268)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.38/4.74 % (3616268)CaDiCaL version: 2.1.3 % 25.38/4.74 % (3616268)Termination reason: Instruction limit % 25.38/4.74 % (3616268)Termination phase: Saturation % 25.38/4.74 % (3616268)Time elapsed: 0.276 s % 25.38/4.74 % (3616268)Peak memory usage: 117 MB % 25.38/4.74 % (3616268)Instructions burned: 329 (million) % 25.38/4.74 % (3616282)dis+1010_1_to=lpo:sil=128000:sas=z3:si=on:nwc=5:random_seed=3840594073:i=281:gtgl=2:rtra=on:gtg=all_2973 on theBenchmark for (2973ds/281Mi) % 25.38/4.74 % (3616284)lrs+1010_1_to=kbo:sil=128000:si=on:sos=on:urr=on:uwa=alasca_main:random_seed=782452085:i=484:doe=on:nm=0:av=off:rtra=on:ss=axioms_2972 on theBenchmark for (2972ds/484Mi) % 25.38/4.74 % (3616284)Refutation not found, incomplete strategy % 25.38/4.74 % (3616284)------------------------------ % 25.38/4.74 % (3616284)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.38/4.74 % (3616284)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.38/4.74 % (3616284)CaDiCaL version: 2.1.3 % 25.38/4.74 % (3616284)Termination reason: Refutation not found, incomplete strategy % 25.38/4.74 % (3616284)Time elapsed: 0.026 s % 25.38/4.74 % (3616284)Peak memory usage: 87 MB % 25.38/4.74 % (3616284)Instructions burned: 68 (million) % 25.38/4.74 % (3616275)Instruction limit reached! % 25.38/4.74 % (3616275)------------------------------ % 25.38/4.74 % (3616275)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.38/4.74 % (3616275)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.38/4.74 % (3616275)CaDiCaL version: 2.1.3 % 25.38/4.74 % (3616275)Termination reason: Instruction limit % 25.38/4.74 % (3616275)Termination phase: Saturation % 25.38/4.74 % (3616275)Time elapsed: 0.267 s % 25.38/4.74 % (3616275)Peak memory usage: 112 MB % 25.38/4.74 % (3616275)Instructions burned: 328 (million) % 25.38/4.74 % (3616285)lrs+21_1_to=kbo:sil=128000:thi=neg_eq:si=on:random_seed=3918331788:i=321:canc=force:rtra=on:tac=axiom:ss=axioms:ev=force_2971 on theBenchmark for (2971ds/321Mi) % 25.38/4.74 % (3616270)Instruction limit reached! % 25.38/4.74 % (3616270)------------------------------ % 25.38/4.74 % (3616270)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.38/4.74 % (3616270)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.38/4.74 % (3616270)CaDiCaL version: 2.1.3 % 25.38/4.74 % (3616270)Termination reason: Instruction limit % 25.38/4.74 % (3616270)Termination phase: Saturation % 25.38/4.74 % (3616270)Time elapsed: 0.419 s % 25.38/4.74 % (3616270)Peak memory usage: 133 MB % 25.38/4.74 % (3616270)Instructions burned: 483 (million) % 25.38/4.74 % (3616286)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=2771472033:i=416:rtra=on:gtg=position:ss=axioms_2971 on theBenchmark for (2971ds/416Mi) % 25.38/4.74 % (3616285)Refutation not found, incomplete strategy % 25.38/4.74 % (3616285)------------------------------ % 25.38/4.74 % (3616285)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.38/4.74 % (3616285)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.38/4.74 % (3616285)CaDiCaL version: 2.1.3 % 25.38/4.74 % (3616285)Termination reason: Refutation not found, incomplete strategy % 25.38/4.74 % (3616285)Time elapsed: 0.087 s % 25.38/4.74 % (3616285)Peak memory usage: 112 MB % 25.38/4.74 % (3616285)Instructions burned: 73 (million) % 25.38/4.74 % (3616274)------------------------------ % 25.38/4.74 % (3616274)------------------------------ % 25.38/4.74 % (3616282)Instruction limit reached! % 25.38/4.74 % (3616282)------------------------------ % 25.38/4.74 % (3616282)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.38/4.74 % (3616282)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.54/5.29 % (3616282)CaDiCaL version: 2.1.3 % 31.54/5.29 % (3616282)Termination reason: Instruction limit % 31.54/5.29 % (3616282)Termination phase: Saturation % 31.54/5.29 % (3616282)Time elapsed: 0.241 s % 31.54/5.29 % (3616282)Peak memory usage: 112 MB % 31.54/5.29 % (3616282)Instructions burned: 282 (million) % 31.54/5.29 % (3616286)Refutation not found, incomplete strategy % 31.54/5.29 % (3616286)------------------------------ % 31.54/5.29 % (3616286)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.54/5.29 % (3616286)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.54/5.29 % (3616286)CaDiCaL version: 2.1.3 % 31.54/5.29 % (3616286)Termination reason: Refutation not found, incomplete strategy % 31.54/5.29 % (3616286)Time elapsed: 0.086 s % 31.54/5.29 % (3616286)Peak memory usage: 111 MB % 31.54/5.29 % (3616286)Instructions burned: 73 (million) % 31.54/5.29 % (3616289)lrs+1010_1_to=kbo:tgt=ground:fde=unused:sas=z3:si=on:sp=unary_frequency:gve=force:spb=goal:tha=off:random_seed=3591728751:i=471:thf=on:kws=precedence:rtra=on_2970 on theBenchmark for (2970ds/471Mi) % 31.54/5.29 % (3616284)------------------------------ % 31.54/5.29 % (3616284)------------------------------ % 31.54/5.29 % (3616294)lrs+1010_2_to=kbo:sil=128000:tgt=ground:fde=unused:sas=z3:si=on:uwa=off:tha=off:nwc=1:random_seed=3701091389:i=375:kws=inv_arity_squared:rtra=on_2968 on theBenchmark for (2968ds/375Mi) % 31.54/5.29 % (3616291)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=2255363443:avsq=on:i=276:avsqr=1,2:rtra=on_2969 on theBenchmark for (2969ds/276Mi) % 31.54/5.29 % (3616296)lrs+10_1_to=kbo:sil=128000:tgt=full:sas=z3:si=on:uwa=func_ext:slsqc=1:flr=on:slsq=on:random_seed=2123893122:i=387:bd=preordered:rtra=on:ss=axioms:sgt=8_2968 on theBenchmark for (2968ds/387Mi) % 31.54/5.29 % (3616285)------------------------------ % 31.54/5.29 % (3616285)------------------------------ % 31.54/5.29 % (3616294)Instruction limit reached! % 31.54/5.29 % (3616294)------------------------------ % 31.54/5.29 % (3616294)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.54/5.29 % (3616294)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.54/5.29 % (3616294)CaDiCaL version: 2.1.3 % 31.54/5.29 % (3616294)Termination reason: Instruction limit % 31.54/5.29 % (3616294)Termination phase: Saturation % 31.54/5.29 % (3616294)Time elapsed: 0.192 s % 31.54/5.29 % (3616294)Peak memory usage: 113 MB % 31.54/5.29 % (3616294)Instructions burned: 375 (million) % 31.54/5.29 % (3616298)lrs+10_1_to=kbo:sil=128000:fde=none:si=on:norm_ineq=on:urr=on:nwc=0.5:random_seed=3363274320:i=513:kws=frequency:bd=all:rtra=on:gtg=exists_all:ss=axioms:sgt=4_2967 on theBenchmark for (2967ds/513Mi) % 31.54/5.29 % (3616296)Refutation not found, incomplete strategy % 31.54/5.29 % (3616296)------------------------------ % 31.54/5.29 % (3616296)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.54/5.29 % (3616296)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.54/5.29 % (3616296)CaDiCaL version: 2.1.3 % 31.54/5.29 % (3616296)Termination reason: Refutation not found, incomplete strategy % 31.54/5.29 % (3616296)Time elapsed: 0.091 s % 31.54/5.29 % (3616296)Peak memory usage: 111 MB % 31.54/5.29 % (3616296)Instructions burned: 77 (million) % 31.54/5.29 % (3616291)Instruction limit reached! % 31.54/5.29 % (3616291)------------------------------ % 31.54/5.29 % (3616291)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.54/5.29 % (3616291)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.54/5.29 % (3616291)CaDiCaL version: 2.1.3 % 31.54/5.29 % (3616291)Termination reason: Instruction limit % 31.54/5.29 % (3616291)Termination phase: Saturation % 31.54/5.29 % (3616291)Time elapsed: 0.253 s % 31.54/5.29 % (3616291)Peak memory usage: 129 MB % 31.54/5.29 % (3616291)Instructions burned: 277 (million) % 31.54/5.29 % (3616286)------------------------------ % 31.54/5.29 % (3616286)------------------------------ % 31.54/5.29 % (3616289)Instruction limit reached! % 31.54/5.29 % (3616289)------------------------------ % 31.54/5.29 % (3616289)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.54/5.29 % (3616289)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.54/5.29 % (3616289)CaDiCaL version: 2.1.3 % 31.54/5.29 % (3616289)Termination reason: Instruction limit % 31.54/5.29 % (3616289)Termination phase: Saturation % 31.54/5.29 % (3616289)Time elapsed: 0.375 s % 31.54/5.29 % (3616289)Peak memory usage: 113 MB % 35.97/6.12 % (3616289)Instructions burned: 471 (million) % 35.97/6.12 % (3616298)Instruction limit reached! % 35.97/6.12 % (3616298)------------------------------ % 35.97/6.12 % (3616298)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 35.97/6.12 % (3616298)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.97/6.12 % (3616298)CaDiCaL version: 2.1.3 % 35.97/6.12 % (3616298)Termination reason: Instruction limit % 35.97/6.12 % (3616298)Termination phase: Saturation % 35.97/6.12 % (3616298)Time elapsed: 0.194 s % 35.97/6.12 % (3616298)Peak memory usage: 89 MB % 35.97/6.12 % (3616298)Instructions burned: 514 (million) % 35.97/6.12 % (3616302)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=1237133041:i=334:rtra=on_2964 on theBenchmark for (2964ds/334Mi) % 35.97/6.12 % (3616303)lrs+1010_1_to=kbo:sil=64000:sas=cadical:si=on:sos=on:bce=on:random_seed=898285981:i=359:rtra=on:gtg=exists_top:ss=axioms_2964 on theBenchmark for (2964ds/359Mi) % 35.97/6.12 % (3616307)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=60842810:s2pl=no:i=235:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2964 on theBenchmark for (2964ds/235Mi) % 35.97/6.12 % (3616306)lrs-2_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_max:tha=off:random_seed=1039955809:st=1.5:i=261:sd=1:kws=precedence:rtra=on:ss=axioms_2964 on theBenchmark for (2964ds/261Mi) % 35.97/6.12 % (3616305)dis+1010_1_to=lpo:sil=128000:thi=all:fde=unused:si=on:sp=reverse_arity:tha=off:random_seed=1096271704:i=341:gtgl=2:rtra=on:gtg=exists_sym:ev=force:fsd=on:fsdmm=1_2964 on theBenchmark for (2964ds/341Mi) % 35.97/6.12 % (3616303)Refutation not found, incomplete strategy % 35.97/6.12 % (3616303)------------------------------ % 35.97/6.12 % (3616303)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 35.97/6.12 % (3616303)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.97/6.12 % (3616303)CaDiCaL version: 2.1.3 % 35.97/6.12 % (3616303)Termination reason: Refutation not found, incomplete strategy % 35.97/6.12 % (3616303)Time elapsed: 0.074 s % 35.97/6.12 % (3616303)Peak memory usage: 88 MB % 35.97/6.12 % (3616303)Instructions burned: 97 (million) % 35.97/6.12 % (3616306)Refutation not found, incomplete strategy % 35.97/6.12 % (3616306)------------------------------ % 35.97/6.12 % (3616306)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 35.97/6.12 % (3616306)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.97/6.12 % (3616306)CaDiCaL version: 2.1.3 % 35.97/6.12 % (3616306)Termination reason: Refutation not found, incomplete strategy % 35.97/6.12 % (3616306)Time elapsed: 0.069 s % 35.97/6.12 % (3616306)Peak memory usage: 111 MB % 35.97/6.12 % (3616306)Instructions burned: 48 (million) % 35.97/6.12 % (3616308)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=2658759913:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2962 on theBenchmark for (2962ds/273Mi) % 35.97/6.12 % (3616307)Refutation not found, incomplete strategy % 35.97/6.12 % (3616307)------------------------------ % 35.97/6.12 % (3616307)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 35.97/6.12 % (3616307)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.97/6.12 % (3616307)CaDiCaL version: 2.1.3 % 35.97/6.12 % (3616307)Termination reason: Refutation not found, incomplete strategy % 35.97/6.12 % (3616307)Time elapsed: 0.090 s % 35.97/6.12 % (3616307)Peak memory usage: 111 MB % 35.97/6.12 % (3616307)Instructions burned: 76 (million) % 35.97/6.12 % (3616296)------------------------------ % 35.97/6.12 % (3616296)------------------------------ % 35.97/6.12 % (3616308)Instruction limit reached! % 35.97/6.12 % (3616308)------------------------------ % 35.97/6.12 % (3616308)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 35.97/6.12 % (3616308)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.97/6.12 % (3616308)CaDiCaL version: 2.1.3 % 35.97/6.12 % (3616308)Termination reason: Instruction limit % 35.97/6.12 % (3616308)Termination phase: Saturation % 35.97/6.12 % (3616308)Time elapsed: 0.109 s % 35.97/6.12 % (3616308)Peak memory usage: 91 MB % 35.97/6.12 % (3616308)Instructions burned: 273 (million) % 35.97/6.12 % (3616302)Instruction limit reached! % 35.97/6.12 % (3616302)------------------------------ % 35.97/6.12 % (3616302)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 40.10/6.68 % (3616302)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.10/6.68 % (3616302)CaDiCaL version: 2.1.3 % 40.10/6.68 % (3616302)Termination reason: Instruction limit % 40.10/6.68 % (3616302)Termination phase: Saturation % 40.10/6.68 % (3616302)Time elapsed: 0.308 s % 40.10/6.68 % (3616302)Peak memory usage: 129 MB % 40.10/6.68 % (3616302)Instructions burned: 335 (million) % 40.10/6.68 % (3616305)Instruction limit reached! % 40.10/6.68 % (3616305)------------------------------ % 40.10/6.68 % (3616305)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 40.10/6.68 % (3616305)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.10/6.68 % (3616305)CaDiCaL version: 2.1.3 % 40.10/6.68 % (3616305)Termination reason: Instruction limit % 40.10/6.68 % (3616305)Termination phase: Saturation % 40.10/6.68 % (3616305)Time elapsed: 0.291 s % 40.10/6.68 % (3616305)Peak memory usage: 117 MB % 40.10/6.68 % (3616305)Instructions burned: 342 (million) % 40.10/6.68 % (3616315)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=4612030:i=146:doe=on:rtra=on_2960 on theBenchmark for (2960ds/146Mi) % 40.10/6.68 % (3616316)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=485625736:i=4428:doe=on:fsr=off:rtra=on_2959 on theBenchmark for (2959ds/4428Mi) % 40.10/6.68 % (3616317)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=193527786:avsq=on:i=276:avsqr=1,2:rtra=on_2959 on theBenchmark for (2959ds/276Mi) % 40.10/6.68 % (3616303)------------------------------ % 40.10/6.68 % (3616303)------------------------------ % 40.10/6.68 % (3616306)------------------------------ % 40.10/6.68 % (3616306)------------------------------ % 40.10/6.68 % (3616307)------------------------------ % 40.10/6.68 % (3616307)------------------------------ % 40.10/6.68 % (3616315)Instruction limit reached! % 40.10/6.68 % (3616315)------------------------------ % 40.10/6.68 % (3616315)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 40.10/6.68 % (3616315)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.10/6.68 % (3616315)CaDiCaL version: 2.1.3 % 40.10/6.68 % (3616315)Termination reason: Instruction limit % 40.10/6.68 % (3616315)Termination phase: Saturation % 40.10/6.68 % (3616315)Time elapsed: 0.111 s % 40.10/6.68 % (3616315)Peak memory usage: 88 MB % 40.10/6.68 % (3616315)Instructions burned: 147 (million) % 40.10/6.68 % (3616317)Instruction limit reached! % 40.10/6.68 % (3616317)------------------------------ % 40.10/6.68 % (3616317)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 40.10/6.68 % (3616317)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.10/6.68 % (3616317)CaDiCaL version: 2.1.3 % 40.10/6.68 % (3616317)Termination reason: Instruction limit % 40.10/6.68 % (3616317)Termination phase: Saturation % 40.10/6.68 % (3616317)Time elapsed: 0.164 s % 40.10/6.68 % (3616317)Peak memory usage: 129 MB % 40.10/6.68 % (3616317)Instructions burned: 278 (million) % 40.10/6.68 % (3616318)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=1462221548:i=1052:rtra=on_2958 on theBenchmark for (2958ds/1052Mi) % 40.10/6.68 % (3616322)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=3653363585:i=655:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2957 on theBenchmark for (2957ds/655Mi) % 40.10/6.68 % (3616323)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=1609308144:st=5:i=1054:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2956 on theBenchmark for (2956ds/1054Mi) % 40.10/6.68 % (3616324)lrs-1002_1_to=kbo:sas=z3:si=on:norm_ineq=on:sos=on:tha=some:random_seed=3976312048:i=107:rtra=on_2956 on theBenchmark for (2956ds/107Mi) % 40.10/6.68 % (3616323)Refutation not found, incomplete strategy % 40.10/6.68 % (3616323)------------------------------ % 40.10/6.68 % (3616323)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 40.10/6.68 % (3616323)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.10/6.68 % (3616323)CaDiCaL version: 2.1.3 % 40.10/6.68 % (3616323)Termination reason: Refutation not found, incomplete strategy % 40.10/6.68 % (3616323)Time elapsed: 0.032 s % 40.10/6.68 % (3616323)Peak memory usage: 87 MB % 40.10/6.68 % (3616323)Instructions burned: 42 (million) % 40.10/6.68 % (3616325)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=3119618549:s2a=on:i=450:doe=on:nm=32:rtra=on_2956 on theBenchmark for (2956ds/450Mi) % 44.87/7.15 % (3616324)Instruction limit reached! % 44.87/7.15 % (3616324)------------------------------ % 44.87/7.15 % (3616324)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 44.87/7.15 % (3616324)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 44.87/7.15 % (3616324)CaDiCaL version: 2.1.3 % 44.87/7.15 % (3616324)Termination reason: Instruction limit % 44.87/7.15 % (3616324)Termination phase: Saturation % 44.87/7.15 % (3616324)Time elapsed: 0.082 s % 44.87/7.15 % (3616324)Peak memory usage: 88 MB % 44.87/7.15 % (3616324)Instructions burned: 107 (million) % 44.87/7.15 % (3616326)WARNING Broken Constraint: if demodulation_redundancy_check(ordering) has been set then forward_demodulation(off) is not equal to off or backward_demodulation(off) is not equal to off or partial_redundancy_check(off) is not equal to off % 44.87/7.15 % (3616326)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=482157221:i=1090:aac=none:nm=0:rtra=on:rawr=on_2956 on theBenchmark for (2956ds/1090Mi) % 44.87/7.15 % (3616332)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=656763982:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2953 on theBenchmark for (2953ds/130Mi) % 44.87/7.15 % (3616325)Instruction limit reached! % 44.87/7.15 % (3616325)------------------------------ % 44.87/7.15 % (3616325)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 44.87/7.15 % (3616325)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 44.87/7.15 % (3616325)CaDiCaL version: 2.1.3 % 44.87/7.15 % (3616325)Termination reason: Instruction limit % 44.87/7.15 % (3616325)Termination phase: Saturation % 44.87/7.15 % (3616325)Time elapsed: 0.379 s % 44.87/7.15 % (3616325)Peak memory usage: 129 MB % 44.87/7.15 % (3616325)Instructions burned: 450 (million) % 44.87/7.15 % (3616323)------------------------------ % 44.87/7.15 % (3616323)------------------------------ % 44.87/7.15 % (3616322)Refutation not found, incomplete strategy % 44.87/7.15 % (3616322)------------------------------ % 44.87/7.15 % (3616322)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 44.87/7.15 % (3616322)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 44.87/7.15 % (3616322)CaDiCaL version: 2.1.3 % 44.87/7.15 % (3616322)Termination reason: Refutation not found, incomplete strategy % 44.87/7.15 % (3616322)Time elapsed: 0.499 s % 44.87/7.15 % (3616322)Peak memory usage: 96 MB % 44.87/7.15 % (3616322)Instructions burned: 539 (million) % 44.87/7.15 % (3616332)Instruction limit reached! % 44.87/7.15 % (3616332)------------------------------ % 44.87/7.15 % (3616332)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 44.87/7.15 % (3616332)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 44.87/7.15 % (3616332)CaDiCaL version: 2.1.3 % 44.87/7.15 % (3616332)Termination reason: Instruction limit % 44.87/7.15 % (3616332)Termination phase: Twee Goal Transformation % 44.87/7.15 % (3616332)Time elapsed: 0.101 s % 44.87/7.15 % (3616332)Peak memory usage: 87 MB % 44.87/7.15 % (3616332)Instructions burned: 130 (million) % 44.87/7.15 % (3616318)Instruction limit reached! % 44.87/7.15 % (3616318)------------------------------ % 44.87/7.15 % (3616318)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 44.87/7.15 % (3616318)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 44.87/7.15 % (3616318)CaDiCaL version: 2.1.3 % 44.87/7.15 % (3616318)Termination reason: Instruction limit % 44.87/7.15 % (3616318)Termination phase: Saturation % 44.87/7.15 % (3616318)Time elapsed: 0.731 s % 44.87/7.15 % (3616318)Peak memory usage: 91 MB % 44.87/7.15 % (3616318)Instructions burned: 1053 (million) % 44.87/7.15 % (3616335)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=392008886:i=312:kws=inv_frequency:nm=20:rtra=on_2950 on theBenchmark for (2950ds/312Mi) % 44.87/7.15 % (3616337)ott+1011_4:1_to=lpo:sil=64000:si=on:spb=intro:random_seed=2704182625:s2a=on:i=835:s2at=2:rtra=on_2949 on theBenchmark for (2949ds/835Mi) % 44.87/7.15 % (3616336)ott+10_1_to=kbo:sil=64000:si=on:sp=reverse_frequency:sos=on:random_seed=1020129725:i=491:doe=on:rtra=on:gtg=position_2950 on theBenchmark for (2950ds/491Mi) % 44.87/7.15 % (3616322)------------------------------ % 44.87/7.15 % (3616322)------------------------------ % 44.87/7.15 % (3616338)ott+1011_2_to=lpo:sil=128000:si=on:sos=on:random_seed=3096132488:i=307:bd=preordered:av=off:rtra=on:ev=cautious_2948 on theBenchmark for (2948ds/307Mi) % 47.66/7.85 % (3616336)Refutation not found, incomplete strategy % 47.66/7.85 % (3616336)------------------------------ % 47.66/7.85 % (3616336)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 47.66/7.85 % (3616336)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.66/7.85 % (3616336)CaDiCaL version: 2.1.3 % 47.66/7.85 % (3616336)Termination reason: Refutation not found, incomplete strategy % 47.66/7.85 % (3616336)Time elapsed: 0.191 s % 47.66/7.85 % (3616336)Peak memory usage: 90 MB % 47.66/7.85 % (3616336)Instructions burned: 251 (million) % 47.66/7.85 % (3616326)Instruction limit reached! % 47.66/7.85 % (3616326)------------------------------ % 47.66/7.85 % (3616326)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 47.66/7.85 % (3616326)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.66/7.85 % (3616326)CaDiCaL version: 2.1.3 % 47.66/7.85 % (3616326)Termination reason: Instruction limit % 47.66/7.85 % (3616326)Termination phase: Saturation % 47.66/7.85 % (3616326)Time elapsed: 0.805 s % 47.66/7.85 % (3616326)Peak memory usage: 118 MB % 47.66/7.85 % (3616326)Instructions burned: 1090 (million) % 47.66/7.85 % (3616335)Instruction limit reached! % 47.66/7.85 % (3616335)------------------------------ % 47.66/7.85 % (3616335)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 47.66/7.85 % (3616335)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.66/7.85 % (3616335)CaDiCaL version: 2.1.3 % 47.66/7.85 % (3616335)Termination reason: Instruction limit % 47.66/7.85 % (3616335)Termination phase: Saturation % 47.66/7.85 % (3616335)Time elapsed: 0.264 s % 47.66/7.85 % (3616335)Peak memory usage: 112 MB % 47.66/7.85 % (3616335)Instructions burned: 313 (million) % 47.66/7.85 % (3616338)Refutation not found, incomplete strategy % 47.66/7.85 % (3616338)------------------------------ % 47.66/7.85 % (3616338)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 47.66/7.85 % (3616338)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.66/7.85 % (3616338)CaDiCaL version: 2.1.3 % 47.66/7.85 % (3616338)Termination reason: Refutation not found, incomplete strategy % 47.66/7.85 % (3616338)Time elapsed: 0.156 s % 47.66/7.85 % (3616338)Peak memory usage: 90 MB % 47.66/7.85 % (3616338)Instructions burned: 207 (million) % 47.66/7.85 % (3616344)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=3306247666:s2a=on:i=646:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2945 on theBenchmark for (2945ds/646Mi) % 47.66/7.85 % (3616342)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=2141940660:i=776:doe=on:rtra=on_2946 on theBenchmark for (2946ds/776Mi) % 47.66/7.85 % (3616337)Instruction limit reached! % 47.66/7.85 % (3616337)------------------------------ % 47.66/7.85 % (3616337)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 47.66/7.85 % (3616337)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.66/7.85 % (3616337)CaDiCaL version: 2.1.3 % 47.66/7.85 % (3616337)Termination reason: Instruction limit % 47.66/7.85 % (3616337)Termination phase: Saturation % 47.66/7.85 % (3616337)Time elapsed: 0.543 s % 47.66/7.85 % (3616337)Peak memory usage: 90 MB % 47.66/7.85 % (3616337)Instructions burned: 835 (million) % 47.66/7.85 % (3616345)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=81204281:thitd=on:cond=fast:i=784:nm=30:rtra=on:gtg=all:tac=axiom_2945 on theBenchmark for (2945ds/784Mi) % 47.66/7.85 % (3616316)Instruction limit reached! % 47.66/7.85 % (3616316)------------------------------ % 47.66/7.85 % (3616316)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 47.66/7.85 % (3616316)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.66/7.85 % (3616316)CaDiCaL version: 2.1.3 % 47.66/7.85 % (3616316)Termination reason: Instruction limit % 47.66/7.85 % (3616316)Termination phase: Saturation % 47.66/7.85 % (3616316)Time elapsed: 1.586 s % 47.66/7.85 % (3616316)Peak memory usage: 90 MB % 47.66/7.85 % (3616316)Instructions burned: 4431 (million) % 47.66/7.85 % (3616336)------------------------------ % 47.66/7.85 % (3616336)------------------------------ % 47.66/7.85 % (3616338)------------------------------ % 47.66/7.85 % (3616338)------------------------------ % 47.66/7.85 % (3616350)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=3925981130:s2pl=no:i=246:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2942 on theBenchmark for (2942ds/246Mi) % 56.04/8.88 % (3616351)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=259345387:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2941 on theBenchmark for (2941ds/775Mi) % 56.04/8.88 % (3616348)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=3147594527:thitd=on:s2a=on:i=1131:add=on:canc=force:bd=all:rtra=on:tac=axiom:ev=off_2942 on theBenchmark for (2942ds/1131Mi) % 56.04/8.88 % (3616350)Refutation not found, incomplete strategy % 56.04/8.88 % (3616350)------------------------------ % 56.04/8.88 % (3616350)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 56.04/8.88 % (3616350)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.04/8.88 % (3616350)CaDiCaL version: 2.1.3 % 56.04/8.88 % (3616350)Termination reason: Refutation not found, incomplete strategy % 56.04/8.88 % (3616350)Time elapsed: 0.051 s % 56.04/8.88 % (3616350)Peak memory usage: 111 MB % 56.04/8.88 % (3616350)Instructions burned: 76 (million) % 56.04/8.88 % (3616351)Refutation not found, incomplete strategy % 56.04/8.88 % (3616351)------------------------------ % 56.04/8.88 % (3616351)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 56.04/8.88 % (3616351)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.04/8.88 % (3616351)CaDiCaL version: 2.1.3 % 56.04/8.88 % (3616351)Termination reason: Refutation not found, incomplete strategy % 56.04/8.88 % (3616351)Time elapsed: 0.057 s % 56.04/8.88 % (3616351)Peak memory usage: 88 MB % 56.04/8.88 % (3616351)Instructions burned: 74 (million) % 56.04/8.88 % (3616344)Instruction limit reached! % 56.04/8.88 % (3616344)------------------------------ % 56.04/8.88 % (3616344)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 56.04/8.88 % (3616344)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.04/8.88 % (3616344)CaDiCaL version: 2.1.3 % 56.04/8.88 % (3616344)Termination reason: Instruction limit % 56.04/8.88 % (3616344)Termination phase: Saturation % 56.04/8.88 % (3616344)Time elapsed: 0.534 s % 56.04/8.88 % (3616344)Peak memory usage: 136 MB % 56.04/8.88 % (3616344)Instructions burned: 647 (million) % 56.04/8.88 % (3616342)Instruction limit reached! % 56.04/8.88 % (3616342)------------------------------ % 56.04/8.88 % (3616342)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 56.04/8.88 % (3616342)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.04/8.88 % (3616342)CaDiCaL version: 2.1.3 % 56.04/8.88 % (3616342)Termination reason: Instruction limit % 56.04/8.88 % (3616342)Termination phase: Saturation % 56.04/8.88 % (3616342)Time elapsed: 0.568 s % 56.04/8.88 % (3616342)Peak memory usage: 113 MB % 56.04/8.88 % (3616342)Instructions burned: 776 (million) % 56.04/8.88 % (3616352)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=3765705393:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2940 on theBenchmark for (2940ds/273Mi) % 56.04/8.88 % (3616350)------------------------------ % 56.04/8.88 % (3616350)------------------------------ % 56.04/8.88 % (3616356)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=2048993264:i=102:nm=16:rtra=on_2938 on theBenchmark for (2938ds/102Mi) % 56.04/8.88 % (3616345)Instruction limit reached! % 56.04/8.88 % (3616345)------------------------------ % 56.04/8.88 % (3616345)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 56.04/8.88 % (3616345)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.04/8.88 % (3616345)CaDiCaL version: 2.1.3 % 56.04/8.88 % (3616345)Termination reason: Instruction limit % 56.04/8.88 % (3616345)Termination phase: Saturation % 56.04/8.88 % (3616345)Time elapsed: 0.573 s % 56.04/8.88 % (3616345)Peak memory usage: 114 MB % 56.04/8.88 % (3616345)Instructions burned: 784 (million) % 56.04/8.88 % (3616356)Instruction limit reached! % 56.04/8.88 % (3616356)------------------------------ % 56.04/8.88 % (3616356)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 56.04/8.88 % (3616356)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.04/8.88 % (3616356)CaDiCaL version: 2.1.3 % 56.04/8.88 % (3616356)Termination reason: Instruction limit % 56.04/8.88 % (3616356)Termination phase: Saturation % 56.04/8.88 % (3616356)Time elapsed: 0.048 s % 56.04/8.88 % (3616356)Peak memory usage: 88 MB % 56.04/8.88 % (3616356)Instructions burned: 102 (million) % 56.04/8.88 % (3616352)Instruction limit reached! % 56.04/8.88 % (3616352)------------------------------ % 74.17/11.39 % (3616352)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 74.17/11.39 % (3616352)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.17/11.39 % (3616352)CaDiCaL version: 2.1.3 % 74.17/11.39 % (3616352)Termination reason: Instruction limit % 74.17/11.39 % (3616352)Termination phase: Saturation % 74.17/11.39 % (3616352)Time elapsed: 0.205 s % 74.17/11.39 % (3616352)Peak memory usage: 90 MB % 74.17/11.39 % (3616352)Instructions burned: 274 (million) % 74.17/11.39 % (3616351)------------------------------ % 74.17/11.39 % (3616351)------------------------------ % 74.17/11.39 % (3616357)lrs+10_1_to=lpo:sil=128000:si=on:bsr=unit_only:tha=off:random_seed=2548493019:avsq=on:s2a=on:i=1094:s2at=5:avsqr=4463,131072:rtra=on_2937 on theBenchmark for (2937ds/1094Mi) % 74.17/11.39 % (3616359)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=4106778589:i=6400:doe=on:fsr=off:rtra=on_2937 on theBenchmark for (2937ds/6400Mi) % 74.17/11.39 % (3616361)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=1827430760:i=868:doe=on:nm=0:rtra=on:gtg=exists_sym_2936 on theBenchmark for (2936ds/868Mi) % 74.17/11.39 % (3616365)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=2373614541:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2935 on theBenchmark for (2935ds/273Mi) % 74.17/11.39 % (3616362)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=1247007:i=1846:canc=cautious:fsr=off:rtra=on_2936 on theBenchmark for (2936ds/1846Mi) % 74.17/11.39 % (3616363)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=2675566292:s2a=on:i=36816:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2935 on theBenchmark for (2935ds/36816Mi) % 74.17/11.39 % (3616362)Refutation not found, incomplete strategy % 74.17/11.39 % (3616362)------------------------------ % 74.17/11.39 % (3616362)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 74.17/11.39 % (3616362)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.17/11.39 % (3616362)CaDiCaL version: 2.1.3 % 74.17/11.39 % (3616362)Termination reason: Refutation not found, incomplete strategy % 74.17/11.39 % (3616362)Time elapsed: 0.123 s % 74.17/11.39 % (3616362)Peak memory usage: 89 MB % 74.17/11.39 % (3616362)Instructions burned: 170 (million) % 74.17/11.39 % (3616365)Instruction limit reached! % 74.17/11.39 % (3616365)------------------------------ % 74.17/11.39 % (3616365)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 74.17/11.39 % (3616365)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.17/11.39 % (3616365)CaDiCaL version: 2.1.3 % 74.17/11.39 % (3616365)Termination reason: Instruction limit % 74.17/11.39 % (3616365)Termination phase: Saturation % 74.17/11.39 % (3616365)Time elapsed: 0.155 s % 74.17/11.39 % (3616365)Peak memory usage: 90 MB % 74.17/11.39 % (3616365)Instructions burned: 274 (million) % 74.17/11.39 % (3616348)Instruction limit reached! % 74.17/11.39 % (3616348)------------------------------ % 74.17/11.39 % (3616348)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 74.17/11.39 % (3616348)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.17/11.39 % (3616348)CaDiCaL version: 2.1.3 % 74.17/11.39 % (3616348)Termination reason: Instruction limit % 74.17/11.39 % (3616348)Termination phase: Saturation % 74.17/11.39 % (3616348)Time elapsed: 0.884 s % 74.17/11.39 % (3616348)Peak memory usage: 113 MB % 74.17/11.39 % (3616348)Instructions burned: 1131 (million) % 74.17/11.39 % (3616361)Instruction limit reached! % 74.17/11.39 % (3616361)------------------------------ % 74.17/11.39 % (3616361)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 74.17/11.39 % (3616361)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.17/11.39 % (3616361)CaDiCaL version: 2.1.3 % 74.17/11.39 % (3616361)Termination reason: Instruction limit % 74.17/11.39 % (3616361)Termination phase: Saturation % 74.17/11.39 % (3616361)Time elapsed: 0.394 s % 74.17/11.39 % (3616361)Peak memory usage: 128 MB % 74.17/11.39 % (3616361)Instructions burned: 869 (million) % 74.17/11.39 % (3616371)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=2655676901:i=863:doe=on:nm=0:rtra=on:gtg=exists_sym_2932 on theBenchmark for (2932ds/863Mi) % 74.17/11.39 % (3616373)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=2678493895:i=2216:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2930 on theBenchmark for (2930ds/2216Mi) % 80.37/12.18 % (3616372)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=2455400549:i=5811:kws=precedence:nm=0:rtra=on_2930 on theBenchmark for (2930ds/5811Mi) % 80.37/12.18 % (3616362)------------------------------ % 80.37/12.18 % (3616362)------------------------------ % 80.37/12.18 % (3616357)Instruction limit reached! % 80.37/12.18 % (3616357)------------------------------ % 80.37/12.18 % (3616357)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 80.37/12.18 % (3616357)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 80.37/12.18 % (3616357)CaDiCaL version: 2.1.3 % 80.37/12.18 % (3616357)Termination reason: Instruction limit % 80.37/12.18 % (3616357)Termination phase: Saturation % 80.37/12.18 % (3616357)Time elapsed: 0.755 s % 80.37/12.18 % (3616357)Peak memory usage: 91 MB % 80.37/12.18 % (3616357)Instructions burned: 1095 (million) % 80.37/12.18 % (3616377)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=2309953763:i=801:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2928 on theBenchmark for (2928ds/801Mi) % 80.37/12.18 % (3616378)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=3714983169:st=5:i=1026:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2927 on theBenchmark for (2927ds/1026Mi) % 80.37/12.18 % (3616378)Refutation not found, incomplete strategy % 80.37/12.18 % (3616378)------------------------------ % 80.37/12.18 % (3616378)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 80.37/12.18 % (3616378)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 80.37/12.18 % (3616378)CaDiCaL version: 2.1.3 % 80.37/12.18 % (3616378)Termination reason: Refutation not found, incomplete strategy % 80.37/12.18 % (3616378)Time elapsed: 0.037 s % 80.37/12.18 % (3616378)Peak memory usage: 87 MB % 80.37/12.18 % (3616378)Instructions burned: 42 (million) % 80.37/12.18 % (3616371)Instruction limit reached! % 80.37/12.18 % (3616371)------------------------------ % 80.37/12.18 % (3616371)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 80.37/12.18 % (3616371)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 80.37/12.18 % (3616371)CaDiCaL version: 2.1.3 % 80.37/12.18 % (3616371)Termination reason: Instruction limit % 80.37/12.18 % (3616371)Termination phase: Saturation % 80.37/12.18 % (3616371)Time elapsed: 0.739 s % 80.37/12.18 % (3616371)Peak memory usage: 128 MB % 80.37/12.18 % (3616371)Instructions burned: 863 (million) % 80.37/12.18 % (3616378)------------------------------ % 80.37/12.18 % (3616378)------------------------------ % 80.37/12.18 % (3616377)Refutation not found, incomplete strategy % 80.37/12.18 % (3616377)------------------------------ % 80.37/12.18 % (3616377)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 80.37/12.18 % (3616377)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 80.37/12.18 % (3616377)CaDiCaL version: 2.1.3 % 80.37/12.18 % (3616377)Termination reason: Refutation not found, incomplete strategy % 80.37/12.18 % (3616377)Time elapsed: 0.477 s % 80.37/12.18 % (3616377)Peak memory usage: 95 MB % 80.37/12.18 % (3616377)Instructions burned: 524 (million) % 80.37/12.18 % (3616373)Instruction limit reached! % 80.37/12.18 % (3616373)------------------------------ % 80.37/12.18 % (3616373)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 80.37/12.18 % (3616373)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 80.37/12.18 % (3616373)CaDiCaL version: 2.1.3 % 80.37/12.18 % (3616373)Termination reason: Instruction limit % 80.37/12.18 % (3616373)Termination phase: Saturation % 80.37/12.18 % (3616373)Time elapsed: 0.839 s % 80.37/12.18 % (3616373)Peak memory usage: 119 MB % 80.37/12.18 % (3616373)Instructions burned: 2218 (million) % 80.37/12.18 % (3616381)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=83758101:i=3509:rtra=on_2922 on theBenchmark for (2922ds/3509Mi) % 80.37/12.18 % (3616382)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=3330845367:st=2:i=2127:sd=12:ep=R:rtra=on:ss=axioms_2921 on theBenchmark for (2921ds/2127Mi) % 80.37/12.18 % (3616382)Refutation not found, incomplete strategy % 80.37/12.18 % (3616382)------------------------------ % 80.37/12.18 % (3616382)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 80.37/12.18 % (3616382)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 98.69/14.84 % (3616382)CaDiCaL version: 2.1.3 % 98.69/14.84 % (3616382)Termination reason: Refutation not found, incomplete strategy % 98.69/14.84 % (3616382)Time elapsed: 0.054 s % 98.69/14.84 % (3616382)Peak memory usage: 88 MB % 98.69/14.84 % (3616382)Instructions burned: 70 (million) % 98.69/14.84 % (3616383)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=3407333100:i=1959:rtra=on:fsd=on:proc=on_2920 on theBenchmark for (2920ds/1959Mi) % 98.69/14.84 % (3616377)------------------------------ % 98.69/14.84 % (3616377)------------------------------ % 98.69/14.84 % (3616382)------------------------------ % 98.69/14.84 % (3616382)------------------------------ % 98.69/14.84 % (3616387)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=3155897080:s2a=on:i=3553:nm=0:rtra=on_2917 on theBenchmark for (2917ds/3553Mi) % 98.69/14.84 % (3616389)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=2857406738:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2914 on theBenchmark for (2914ds/3201Mi) % 98.69/14.84 % (3616383)Instruction limit reached! % 98.69/14.84 % (3616383)------------------------------ % 98.69/14.84 % (3616383)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 98.69/14.84 % (3616383)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 98.69/14.84 % (3616383)CaDiCaL version: 2.1.3 % 98.69/14.84 % (3616383)Termination reason: Instruction limit % 98.69/14.84 % (3616383)Termination phase: Saturation % 98.69/14.84 % (3616383)Time elapsed: 0.760 s % 98.69/14.84 % (3616383)Peak memory usage: 119 MB % 98.69/14.84 % (3616383)Instructions burned: 1961 (million) % 98.69/14.84 % (3616391)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=3840984417:thitd=on:cond=on:i=4093:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2910 on theBenchmark for (2910ds/4093Mi) % 98.69/14.84 % (3616389)Refutation not found, incomplete strategy % 98.69/14.84 % (3616389)------------------------------ % 98.69/14.84 % (3616389)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 98.69/14.84 % (3616389)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 98.69/14.84 % (3616389)CaDiCaL version: 2.1.3 % 98.69/14.84 % (3616389)Termination reason: Refutation not found, incomplete strategy % 98.69/14.84 % (3616389)Time elapsed: 0.458 s % 98.69/14.84 % (3616389)Peak memory usage: 93 MB % 98.69/14.84 % (3616389)Instructions burned: 607 (million) % 98.69/14.84 % (3616389)------------------------------ % 98.69/14.84 % (3616389)------------------------------ % 98.69/14.84 % (3616393)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=13191331:cond=fast:i=21173:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2903 on theBenchmark for (2903ds/21173Mi) % 98.69/14.84 % (3616393)Refutation not found, incomplete strategy % 98.69/14.84 % (3616393)------------------------------ % 98.69/14.84 % (3616393)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 98.69/14.84 % (3616393)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 98.69/14.84 % (3616393)CaDiCaL version: 2.1.3 % 98.69/14.84 % (3616393)Termination reason: Refutation not found, incomplete strategy % 98.69/14.84 % (3616393)Time elapsed: 0.064 s % 98.69/14.84 % (3616393)Peak memory usage: 112 MB % 98.69/14.84 % (3616393)Instructions burned: 41 (million) % 98.69/14.84 % (3616393)------------------------------ % 98.69/14.84 % (3616393)------------------------------ % 98.69/14.84 % (3616381)Instruction limit reached! % 98.69/14.84 % (3616381)------------------------------ % 98.69/14.84 % (3616381)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 98.69/14.84 % (3616381)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 98.69/14.84 % (3616381)CaDiCaL version: 2.1.3 % 98.69/14.84 % (3616381)Termination reason: Instruction limit % 98.69/14.84 % (3616381)Termination phase: Saturation % 98.69/14.84 % (3616381)Time elapsed: 2.397 s % 98.69/14.84 % (3616381)Peak memory usage: 90 MB % 98.69/14.84 % (3616381)Instructions burned: 3509 (million) % 98.69/14.84 % (3616396)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=1737840631:avsq=on:i=1262:avsqr=1,16:rtra=on:rawr=on_2895 on theBenchmark for (2895ds/1262Mi) % 98.69/14.84 % (3616391)Instruction limit reached! % 98.69/14.84 % (3616391)------------------------------ % 98.69/14.84 % (3616391)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 106.32/16.08 % (3616391)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 106.32/16.08 % (3616391)CaDiCaL version: 2.1.3 % 106.32/16.08 % (3616391)Termination reason: Instruction limit % 106.32/16.08 % (3616391)Termination phase: Saturation % 106.32/16.08 % (3616391)Time elapsed: 1.513 s % 106.32/16.08 % (3616391)Peak memory usage: 136 MB % 106.32/16.08 % (3616391)Instructions burned: 4095 (million) % 106.32/16.08 % (3616395)lrs+11_1_to=lpo:thi=all:sas=z3:si=on:fd=off:sac=on:slsq=on:random_seed=1723679162:avsq=on:i=10544:avsqr=17,4:canc=force:rtra=on:gtg=exists_top:er=filter_2895 on theBenchmark for (2895ds/10544Mi) % 106.32/16.08 % (3616398)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=415739288:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2893 on theBenchmark for (2893ds/775Mi) % 106.32/16.08 % (3616398)Refutation not found, incomplete strategy % 106.32/16.08 % (3616398)------------------------------ % 106.32/16.08 % (3616398)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 106.32/16.08 % (3616398)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 106.32/16.08 % (3616398)CaDiCaL version: 2.1.3 % 106.32/16.08 % (3616398)Termination reason: Refutation not found, incomplete strategy % 106.32/16.08 % (3616398)Time elapsed: 0.030 s % 106.32/16.08 % (3616398)Peak memory usage: 88 MB % 106.32/16.08 % (3616398)Instructions burned: 74 (million) % 106.32/16.08 % (3616387)Instruction limit reached! % 106.32/16.08 % (3616387)------------------------------ % 106.32/16.08 % (3616387)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 106.32/16.08 % (3616387)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 106.32/16.08 % (3616387)CaDiCaL version: 2.1.3 % 106.32/16.08 % (3616387)Termination reason: Instruction limit % 106.32/16.08 % (3616387)Termination phase: Saturation % 106.32/16.08 % (3616387)Time elapsed: 2.422 s % 106.32/16.08 % (3616387)Peak memory usage: 91 MB % 106.32/16.08 % (3616387)Instructions burned: 3554 (million) % 106.32/16.08 % (3616359)Instruction limit reached! % 106.32/16.08 % (3616359)------------------------------ % 106.32/16.08 % (3616359)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 106.32/16.08 % (3616359)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 106.32/16.08 % (3616359)CaDiCaL version: 2.1.3 % 106.32/16.08 % (3616359)Termination reason: Instruction limit % 106.32/16.08 % (3616359)Termination phase: Saturation % 106.32/16.08 % (3616359)Time elapsed: 4.487 s % 106.32/16.08 % (3616359)Peak memory usage: 90 MB % 106.32/16.08 % (3616359)Instructions burned: 6400 (million) % 106.32/16.08 % (3616398)------------------------------ % 106.32/16.08 % (3616398)------------------------------ % 106.32/16.08 % (3616401)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=2827580375:i=270:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2890 on theBenchmark for (2890ds/270Mi) % 106.32/16.08 % (3616401)Instruction limit reached! % 106.32/16.08 % (3616401)------------------------------ % 106.32/16.08 % (3616401)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 106.32/16.08 % (3616401)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 106.32/16.08 % (3616401)CaDiCaL version: 2.1.3 % 106.32/16.08 % (3616401)Termination reason: Instruction limit % 106.32/16.08 % (3616401)Termination phase: Saturation % 106.32/16.08 % (3616401)Time elapsed: 0.109 s % 106.32/16.08 % (3616401)Peak memory usage: 91 MB % 106.32/16.08 % (3616401)Instructions burned: 272 (million) % 106.32/16.08 % (3616402)ott+10_128_isp=bottom:to=lpo:sil=128000:si=on:urr=on:uwa=alasca_main:sac=on:slsq=on:random_seed=945004821:i=17165:aac=none:doe=on:rtra=on:gtg=exists_all_2889 on theBenchmark for (2889ds/17165Mi) % 106.32/16.08 % (3616372)Instruction limit reached! % 106.32/16.08 % (3616372)------------------------------ % 106.32/16.08 % (3616372)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 106.32/16.08 % (3616372)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 106.32/16.08 % (3616372)CaDiCaL version: 2.1.3 % 106.32/16.08 % (3616372)Termination reason: Instruction limit % 106.32/16.08 % (3616372)Termination phase: Saturation % 106.32/16.08 % (3616372)Time elapsed: 4.194 s % 106.32/16.08 % (3616372)Peak memory usage: 119 MB % 106.32/16.08 % (3616372)Instructions burned: 5812 (million) % 106.32/16.08 % (3616405)lrs+2_10_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_main:tha=some:random_seed=806416092:s2a=on:i=13094:s2at=-1:rtra=on_2888 on theBenchmark for (2888ds/13094Mi) % 106.32/16.08 % (3616408)lrs+10_1_to=lpo:sil=128000:si=on:sp=occurrence:random_seed=1658799628:st=2:i=12633:rtra=on:ss=axioms_2887 on theBenchmark for (2887ds/12633Mi) % 122.85/18.15 % (3616408)Refutation not found, incomplete strategy % 122.85/18.15 % (3616408)------------------------------ % 122.85/18.15 % (3616408)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 122.85/18.15 % (3616408)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 122.85/18.15 % (3616408)CaDiCaL version: 2.1.3 % 122.85/18.15 % (3616408)Termination reason: Refutation not found, incomplete strategy % 122.85/18.15 % (3616408)Time elapsed: 0.026 s % 122.85/18.15 % (3616408)Peak memory usage: 87 MB % 122.85/18.15 % (3616408)Instructions burned: 65 (million) % 122.85/18.15 % (3616396)Instruction limit reached! % 122.85/18.15 % (3616396)------------------------------ % 122.85/18.15 % (3616396)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 122.85/18.15 % (3616396)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 122.85/18.15 % (3616396)CaDiCaL version: 2.1.3 % 122.85/18.15 % (3616396)Termination reason: Instruction limit % 122.85/18.15 % (3616396)Termination phase: Saturation % 122.85/18.15 % (3616396)Time elapsed: 0.928 s % 122.85/18.15 % (3616396)Peak memory usage: 119 MB % 122.85/18.15 % (3616396)Instructions burned: 1262 (million) % 122.85/18.15 % (3616409)dis+1011_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_frequency:lsd=20:nwc=3:random_seed=1995916369:i=1783:rtra=on:gtg=position_2886 on theBenchmark for (2886ds/1783Mi) % 122.85/18.15 % (3616408)------------------------------ % 122.85/18.15 % (3616408)------------------------------ % 122.85/18.15 % (3616412)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=1072742006:i=5451:aac=none:doe=on:nm=0:rtra=on:amm=off:gtg=position_2884 on theBenchmark for (2884ds/5451Mi) % 122.85/18.15 % (3616414)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=3185583654:i=4975:doe=on:nm=0:rtra=on:gtg=exists_sym_2882 on theBenchmark for (2882ds/4975Mi) % 122.85/18.15 % (3616409)Instruction limit reached! % 122.85/18.15 % (3616409)------------------------------ % 122.85/18.15 % (3616409)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 122.85/18.15 % (3616409)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 122.85/18.15 % (3616409)CaDiCaL version: 2.1.3 % 122.85/18.15 % (3616409)Termination reason: Instruction limit % 122.85/18.15 % (3616409)Termination phase: Saturation % 122.85/18.15 % (3616409)Time elapsed: 0.997 s % 122.85/18.15 % (3616409)Peak memory usage: 119 MB % 122.85/18.15 % (3616409)Instructions burned: 1784 (million) % 122.85/18.15 % (3616452)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=3351481246:i=2076:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2873 on theBenchmark for (2873ds/2076Mi) % 122.85/18.15 % (3616414)Instruction limit reached! % 122.85/18.15 % (3616414)------------------------------ % 122.85/18.15 % (3616414)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 122.85/18.15 % (3616414)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 122.85/18.15 % (3616414)CaDiCaL version: 2.1.3 % 122.85/18.15 % (3616414)Termination reason: Instruction limit % 122.85/18.15 % (3616414)Termination phase: Saturation % 122.85/18.15 % (3616414)Time elapsed: 1.375 s % 122.85/18.15 % (3616414)Peak memory usage: 130 MB % 122.85/18.15 % (3616414)Instructions burned: 4977 (million) % 122.85/18.15 % (3616466)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=504908881:i=5145:rtra=on_2866 on theBenchmark for (2866ds/5145Mi) % 122.85/18.15 % (3616452)Instruction limit reached! % 122.85/18.15 % (3616452)------------------------------ % 122.85/18.15 % (3616452)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 122.85/18.15 % (3616452)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 122.85/18.15 % (3616452)CaDiCaL version: 2.1.3 % 122.85/18.15 % (3616452)Termination reason: Instruction limit % 122.85/18.15 % (3616452)Termination phase: Saturation % 122.85/18.15 % (3616452)Time elapsed: 0.770 s % 122.85/18.15 % (3616452)Peak memory usage: 119 MB % 122.85/18.15 % (3616452)Instructions burned: 2078 (million) % 122.85/18.15 % (3616468)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=3411871364:i=3509:rtra=on_2864 on theBenchmark for (2864ds/3509Mi) % 122.85/18.15 % (3616412)Instruction limit reached! % 122.85/18.15 % (3616412)------------------------------ % 122.85/18.15 % (3616412)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 185.82/27.05 % (3616412)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 185.82/27.05 % (3616412)CaDiCaL version: 2.1.3 % 185.82/27.05 % (3616412)Termination reason: Instruction limit % 185.82/27.05 % (3616412)Termination phase: Saturation % 185.82/27.05 % (3616412)Time elapsed: 2.313 s % 185.82/27.05 % (3616412)Peak memory usage: 120 MB % 185.82/27.05 % (3616412)Instructions burned: 5452 (million) % 185.82/27.05 % (3616470)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=3985997638:st=2:i=13800:sd=12:ep=R:rtra=on:ss=axioms_2858 on theBenchmark for (2858ds/13800Mi) % 185.82/27.05 % (3616470)Refutation not found, incomplete strategy % 185.82/27.05 % (3616470)------------------------------ % 185.82/27.05 % (3616470)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 185.82/27.05 % (3616470)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 185.82/27.05 % (3616470)CaDiCaL version: 2.1.3 % 185.82/27.05 % (3616470)Termination reason: Refutation not found, incomplete strategy % 185.82/27.05 % (3616470)Time elapsed: 0.026 s % 185.82/27.05 % (3616470)Peak memory usage: 87 MB % 185.82/27.05 % (3616470)Instructions burned: 70 (million) % 185.82/27.05 % (3616466)Instruction limit reached! % 185.82/27.05 % (3616466)------------------------------ % 185.82/27.05 % (3616466)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 185.82/27.05 % (3616466)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 185.82/27.05 % (3616466)CaDiCaL version: 2.1.3 % 185.82/27.05 % (3616466)Termination reason: Instruction limit % 185.82/27.05 % (3616466)Termination phase: Saturation % 185.82/27.05 % (3616466)Time elapsed: 1.005 s % 185.82/27.05 % (3616466)Peak memory usage: 94 MB % 185.82/27.05 % (3616466)Instructions burned: 5151 (million) % 185.82/27.05 % (3616472)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=2828551784:i=1412:rtra=on:fsd=on:proc=on_2855 on theBenchmark for (2855ds/1412Mi) % 185.82/27.05 % (3616470)------------------------------ % 185.82/27.05 % (3616470)------------------------------ % 185.82/27.05 % (3616474)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 % 185.82/27.05 % (3616474)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=1668406795:i=11747:aac=none:nm=0:rtra=on:rawr=on_2854 on theBenchmark for (2854ds/11747Mi) % 185.82/27.05 % (3616472)Instruction limit reached! % 185.82/27.05 % (3616472)------------------------------ % 185.82/27.05 % (3616472)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 185.82/27.05 % (3616472)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 185.82/27.05 % (3616472)CaDiCaL version: 2.1.3 % 185.82/27.05 % (3616472)Termination reason: Instruction limit % 185.82/27.05 % (3616472)Termination phase: Saturation % 185.82/27.05 % (3616472)Time elapsed: 0.293 s % 185.82/27.05 % (3616472)Peak memory usage: 119 MB % 185.82/27.05 % (3616472)Instructions burned: 1415 (million) % 185.82/27.05 % (3616476)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=2666459863:s2a=on:i=3553:nm=0:rtra=on_2851 on theBenchmark for (2851ds/3553Mi) % 185.82/27.05 % (3616468)Instruction limit reached! % 185.82/27.05 % (3616468)------------------------------ % 185.82/27.05 % (3616468)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 185.82/27.05 % (3616468)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 185.82/27.05 % (3616468)CaDiCaL version: 2.1.3 % 185.82/27.05 % (3616468)Termination reason: Instruction limit % 185.82/27.05 % (3616468)Termination phase: Saturation % 185.82/27.05 % (3616468)Time elapsed: 1.286 s % 185.82/27.05 % (3616468)Peak memory usage: 89 MB % 185.82/27.05 % (3616468)Instructions burned: 3512 (million) % 185.82/27.05 % (3616478)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=1119479488:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2850 on theBenchmark for (2850ds/3201Mi) % 185.82/27.05 % (3616478)Refutation not found, incomplete strategy % 185.82/27.05 % (3616478)------------------------------ % 185.82/27.05 % (3616478)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 185.82/27.05 % (3616478)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 185.82/27.05 % (3616478)CaDiCaL version: 2.1.3 % 185.82/27.05 % (3616478)Termination reason: Refutation not found, incomplete strategy % 185.82/27.05 % (3616478)Time elapsed: 0.229 s % 203.22/29.51 % (3616478)Peak memory usage: 93 MB % 203.22/29.51 % (3616478)Instructions burned: 606 (million) % 203.22/29.51 % (3616478)------------------------------ % 203.22/29.51 % (3616478)------------------------------ % 203.22/29.51 % (3616476)Instruction limit reached! % 203.22/29.51 % (3616476)------------------------------ % 203.22/29.51 % (3616476)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 203.22/29.51 % (3616476)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 203.22/29.51 % (3616476)CaDiCaL version: 2.1.3 % 203.22/29.51 % (3616476)Termination reason: Instruction limit % 203.22/29.51 % (3616476)Termination phase: Saturation % 203.22/29.51 % (3616476)Time elapsed: 0.682 s % 203.22/29.51 % (3616476)Peak memory usage: 91 MB % 203.22/29.51 % (3616476)Instructions burned: 3556 (million) % 203.22/29.51 % (3616480)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=4218224173:thitd=on:cond=on:i=4081:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2843 on theBenchmark for (2843ds/4081Mi) % 203.22/29.51 % (3616481)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=1492433781:cond=fast:i=20260:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2843 on theBenchmark for (2843ds/20260Mi) % 203.22/29.51 % (3616481)Refutation not found, incomplete strategy % 203.22/29.51 % (3616481)------------------------------ % 203.22/29.51 % (3616481)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 203.22/29.51 % (3616481)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 203.22/29.51 % (3616481)CaDiCaL version: 2.1.3 % 203.22/29.51 % (3616481)Termination reason: Refutation not found, incomplete strategy % 203.22/29.51 % (3616481)Time elapsed: 0.023 s % 203.22/29.51 % (3616481)Peak memory usage: 112 MB % 203.22/29.51 % (3616481)Instructions burned: 41 (million) % 203.22/29.51 % (3616481)------------------------------ % 203.22/29.51 % (3616481)------------------------------ % 203.22/29.51 % (3616484)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=1580780274:s2a=on:i=58627:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2840 on theBenchmark for (2840ds/58627Mi) % 203.22/29.51 % (3616395)Instruction limit reached! % 203.22/29.51 % (3616395)------------------------------ % 203.22/29.51 % (3616395)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 203.22/29.51 % (3616395)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 203.22/29.51 % (3616395)CaDiCaL version: 2.1.3 % 203.22/29.51 % (3616395)Termination reason: Instruction limit % 203.22/29.51 % (3616395)Termination phase: Saturation % 203.22/29.51 % (3616395)Time elapsed: 5.407 s % 203.22/29.51 % (3616395)Peak memory usage: 166 MB % 203.22/29.51 % (3616395)Instructions burned: 10544 (million) % 203.22/29.51 % (3616486)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=4269539884:avsq=on:i=6258:avsqr=1,16:rtra=on:rawr=on_2838 on theBenchmark for (2838ds/6258Mi) % 203.22/29.51 % (3616405)Instruction limit reached! % 203.22/29.51 % (3616405)------------------------------ % 203.22/29.51 % (3616405)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 203.22/29.51 % (3616405)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 203.22/29.51 % (3616405)CaDiCaL version: 2.1.3 % 203.22/29.51 % (3616405)Termination reason: Instruction limit % 203.22/29.51 % (3616405)Termination phase: Saturation % 203.22/29.51 % (3616405)Time elapsed: 5.139 s % 203.22/29.51 % (3616405)Peak memory usage: 107 MB % 203.22/29.51 % (3616405)Instructions burned: 13095 (million) % 203.22/29.51 % (3616488)ott+10_128_isp=bottom:to=lpo:sil=128000:si=on:urr=on:uwa=alasca_main:sac=on:slsq=on:random_seed=2932150630:i=34001:aac=none:doe=on:rtra=on:gtg=exists_all_2834 on theBenchmark for (2834ds/34001Mi) % 203.22/29.51 % (3616480)Instruction limit reached! % 203.22/29.51 % (3616480)------------------------------ % 203.22/29.51 % (3616480)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 203.22/29.51 % (3616480)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 203.22/29.51 % (3616480)CaDiCaL version: 2.1.3 % 203.22/29.51 % (3616480)Termination reason: Instruction limit % 203.22/29.51 % (3616480)Termination phase: Saturation % 203.22/29.51 % (3616480)Time elapsed: 1.511 s % 203.22/29.51 % (3616480)Peak memory usage: 132 MB % 203.22/29.51 % (3616480)Instructions burned: 4082 (million) % 203.22/29.51 % (3616491)lrs+2_10_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_main:tha=some:random_seed=4026782233:s2a=on:i=71622:s2at=-1:rtra=on_2827 on theBenchmark for (2827ds/71622Mi) % 213.73/31.06 % (3616402)Instruction limit reached! % 213.73/31.06 % (3616402)------------------------------ % 213.73/31.06 % (3616402)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 213.73/31.06 % (3616402)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.73/31.06 % (3616402)CaDiCaL version: 2.1.3 % 213.73/31.06 % (3616402)Termination reason: Instruction limit % 213.73/31.06 % (3616402)Termination phase: Saturation % 213.73/31.06 % (3616402)Time elapsed: 6.802 s % 213.73/31.06 % (3616402)Peak memory usage: 90 MB % 213.73/31.06 % (3616402)Instructions burned: 17165 (million) % 213.73/31.06 % (3616493)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=3776925828:i=24001:kws=precedence:nm=0:rtra=on_2819 on theBenchmark for (2819ds/24001Mi) % 213.73/31.06 % (3616486)Instruction limit reached! % 213.73/31.06 % (3616486)------------------------------ % 213.73/31.06 % (3616486)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 213.73/31.06 % (3616486)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.73/31.06 % (3616486)CaDiCaL version: 2.1.3 % 213.73/31.06 % (3616486)Termination reason: Instruction limit % 213.73/31.06 % (3616486)Termination phase: Saturation % 213.73/31.06 % (3616486)Time elapsed: 2.268 s % 213.73/31.06 % (3616486)Peak memory usage: 120 MB % 213.73/31.06 % (3616486)Instructions burned: 6260 (million) % 213.73/31.06 % (3616495)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=2542154481:i=2076:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2814 on theBenchmark for (2814ds/2076Mi) % 213.73/31.06 % (3616474)Instruction limit reached! % 213.73/31.06 % (3616474)------------------------------ % 213.73/31.06 % (3616474)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 213.73/31.06 % (3616474)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.73/31.06 % (3616474)CaDiCaL version: 2.1.3 % 213.73/31.06 % (3616474)Termination reason: Instruction limit % 213.73/31.06 % (3616474)Termination phase: Saturation % 213.73/31.06 % (3616474)Time elapsed: 4.475 s % 213.73/31.06 % (3616474)Peak memory usage: 123 MB % 213.73/31.06 % (3616474)Instructions burned: 11747 (million) % 213.73/31.06 % (3616497)dis+21_20_to=lakbo:si=on:alasca=on:sp=const_max:uwa=alasca_main:sac=on:random_seed=553393207:s2a=on:i=83971:s2at=4:bd=all:ins=1:rtra=on_2807 on theBenchmark for (2807ds/83971Mi) % 213.73/31.06 % (3616495)Instruction limit reached! % 213.73/31.06 % (3616495)------------------------------ % 213.73/31.06 % (3616495)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 213.73/31.06 % (3616495)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.73/31.06 % (3616495)CaDiCaL version: 2.1.3 % 213.73/31.06 % (3616495)Termination reason: Instruction limit % 213.73/31.06 % (3616495)Termination phase: Saturation % 213.73/31.06 % (3616495)Time elapsed: 0.765 s % 213.73/31.06 % (3616495)Peak memory usage: 119 MB % 213.73/31.06 % (3616495)Instructions burned: 2076 (million) % 213.73/31.06 % (3616499)lrs+1011_5:1_to=lpo:sil=128000:sas=z3:si=on:norm_ineq=on:tha=some:random_seed=2881172100:i=83944:rtra=on_2805 on theBenchmark for (2805ds/83944Mi) % 213.73/31.06 % (3616363)Instruction limit reached! % 213.73/31.06 % (3616363)------------------------------ % 213.73/31.06 % (3616363)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 213.73/31.06 % (3616363)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.73/31.06 % (3616363)CaDiCaL version: 2.1.3 % 213.73/31.06 % (3616363)Termination reason: Instruction limit % 213.73/31.06 % (3616363)Termination phase: Saturation % 213.73/31.06 % (3616363)Time elapsed: 16.114 s % 213.73/31.06 % (3616363)Peak memory usage: 103 MB % 213.73/31.06 % (3616363)Instructions burned: 36817 (million) % 213.73/31.06 % (3616501)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=1673489254:i=9201:rtra=on_2771 on theBenchmark for (2771ds/9201Mi) % 213.73/31.06 % (3616501)Instruction limit reached! % 213.73/31.06 % (3616501)------------------------------ % 213.73/31.06 % (3616501)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 213.73/31.06 % (3616501)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.73/31.06 % (3616501)CaDiCaL version: 2.1.3 % 213.73/31.06 % (3616501)Termination reason: Instruction limit % 213.73/31.06 % (3616501)Termination phase: Saturation % 213.73/31.06 % (3616501)Time elapsed: 3.356 s % 213.73/31.06 % (3616501)Peak memory usage: 90 MB % 213.73/31.06 % (3616501)Instructions burned: 9201 (million) % 226.62/32.84 % (3616503)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 % 226.62/32.84 % (3616503)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=220285168:i=6806:aac=none:nm=0:rtra=on:rawr=on_2736 on theBenchmark for (2736ds/6806Mi) % 226.62/32.84 % (3616484)Instruction limit reached! % 226.62/32.84 % (3616484)------------------------------ % 226.62/32.84 % (3616484)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 226.62/32.84 % (3616484)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 226.62/32.84 % (3616484)CaDiCaL version: 2.1.3 % 226.62/32.84 % (3616484)Termination reason: Instruction limit % 226.62/32.84 % (3616484)Termination phase: Saturation % 226.62/32.84 % (3616484)Time elapsed: 11.264 s % 226.62/32.84 % (3616484)Peak memory usage: 128 MB % 226.62/32.84 % (3616484)Instructions burned: 58631 (million) % 226.62/32.84 % (3616505)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=2323643204:s2a=on:i=3553:nm=0:rtra=on_2726 on theBenchmark for (2726ds/3553Mi) % 226.62/32.84 % (3616493)Instruction limit reached! % 226.62/32.84 % (3616493)------------------------------ % 226.62/32.84 % (3616493)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 226.62/32.84 % (3616493)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 226.62/32.84 % (3616493)CaDiCaL version: 2.1.3 % 226.62/32.84 % (3616493)Termination reason: Instruction limit % 226.62/32.84 % (3616493)Termination phase: Saturation % 226.62/32.84 % (3616493)Time elapsed: 9.591 s % 226.62/32.84 % (3616493)Peak memory usage: 125 MB % 226.62/32.84 % (3616493)Instructions burned: 24002 (million) % 226.62/32.84 % (3616507)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=1567848465:thitd=on:cond=on:i=2064:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2721 on theBenchmark for (2721ds/2064Mi) % 226.62/32.84 % (3616505)Instruction limit reached! % 226.62/32.84 % (3616505)------------------------------ % 226.62/32.84 % (3616505)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 226.62/32.84 % (3616505)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 226.62/32.84 % (3616505)CaDiCaL version: 2.1.3 % 226.62/32.84 % (3616505)Termination reason: Instruction limit % 226.62/32.84 % (3616505)Termination phase: Saturation % 226.62/32.84 % (3616505)Time elapsed: 0.681 s % 226.62/32.84 % (3616505)Peak memory usage: 91 MB % 226.62/32.84 % (3616505)Instructions burned: 3554 (million) % 226.62/32.84 % (3616509)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=767701185:cond=fast:i=20260:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2718 on theBenchmark for (2718ds/20260Mi) % 226.62/32.84 % (3616509)Refutation not found, incomplete strategy % 226.62/32.84 % (3616509)------------------------------ % 226.62/32.84 % (3616509)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 226.62/32.84 % (3616509)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 226.62/32.84 % (3616509)CaDiCaL version: 2.1.3 % 226.62/32.84 % (3616509)Termination reason: Refutation not found, incomplete strategy % 226.62/32.84 % (3616509)Time elapsed: 0.023 s % 226.62/32.84 % (3616509)Peak memory usage: 112 MB % 226.62/32.84 % (3616509)Instructions burned: 41 (million) % 226.62/32.84 % (3616509)------------------------------ % 226.62/32.84 % (3616509)------------------------------ % 226.62/32.84 % (3616511)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=79444012:avsq=on:i=1244:avsqr=1,16:rtra=on:rawr=on_2715 on theBenchmark for (2715ds/1244Mi) % 226.62/32.84 % (3616507)Instruction limit reached! % 226.62/32.84 % (3616507)------------------------------ % 226.62/32.84 % (3616507)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 226.62/32.84 % (3616507)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 226.62/32.84 % (3616507)CaDiCaL version: 2.1.3 % 226.62/32.84 % (3616507)Termination reason: Instruction limit % 226.62/32.84 % (3616507)Termination phase: Saturation % 226.62/32.84 % (3616507)Time elapsed: 0.792 s % 226.62/32.84 % (3616507)Peak memory usage: 132 MB % 226.62/32.84 % (3616507)Instructions burned: 2066 (million) % 226.62/32.84 % (3616511)Instruction limit reached! % 226.62/32.84 % (3616511)------------------------------ % 226.62/32.84 % (3616511)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 229.16/33.19 % (3616511)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 229.16/33.19 % (3616511)CaDiCaL version: 2.1.3 % 229.16/33.19 % (3616511)Termination reason: Instruction limit % 229.16/33.19 % (3616511)Termination phase: Saturation % 229.16/33.19 % (3616511)Time elapsed: 0.255 s % 229.16/33.19 % (3616511)Peak memory usage: 119 MB % 229.16/33.19 % (3616511)Instructions burned: 1245 (million) % 229.16/33.19 % (3616514)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 % 229.16/33.19 % (3616514)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=1021613143:i=6806:aac=none:nm=0:rtra=on:rawr=on_2711 on theBenchmark for (2711ds/6806Mi) % 229.16/33.19 % (3616513)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=573871219:i=58261:doe=on:nm=0:rtra=on:gtg=exists_sym_2712 on theBenchmark for (2712ds/58261Mi) % 229.16/33.19 % (3616503)Instruction limit reached! % 229.16/33.19 % (3616503)------------------------------ % 229.16/33.19 % (3616503)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 229.16/33.19 % (3616503)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 229.16/33.19 % (3616503)CaDiCaL version: 2.1.3 % 229.16/33.19 % (3616503)Termination reason: Instruction limit % 229.16/33.19 % (3616503)Termination phase: Saturation % 229.16/33.19 % (3616503)Time elapsed: 2.480 s % 229.16/33.19 % (3616503)Peak memory usage: 119 MB % 229.16/33.19 % (3616503)Instructions burned: 6806 (million) % 229.16/33.19 % (3616488)Instruction limit reached! % 229.16/33.19 % (3616488)------------------------------ % 229.16/33.19 % (3616488)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 229.16/33.19 % (3616488)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 229.16/33.19 % (3616488)CaDiCaL version: 2.1.3 % 229.16/33.19 % (3616488)Termination reason: Instruction limit % 229.16/33.19 % (3616488)Termination phase: Saturation % 229.16/33.19 % (3616488)Time elapsed: 12.376 s % 229.16/33.19 % (3616488)Peak memory usage: 91 MB % 229.16/33.19 % (3616488)Instructions burned: 34026 (million) % 229.16/33.19 % (3616517)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=369920450:thitd=on:cond=on:i=4081:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2710 on theBenchmark for (2710ds/4081Mi) % 229.16/33.19 % (3616518)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=3715093395:avsq=on:i=1701:avsqr=1,16:rtra=on:rawr=on_2709 on theBenchmark for (2709ds/1701Mi) % 229.16/33.19 % (3616518)Instruction limit reached! % 229.16/33.19 % (3616518)------------------------------ % 229.16/33.19 % (3616518)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 229.16/33.19 % (3616518)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 229.16/33.19 % (3616518)CaDiCaL version: 2.1.3 % 229.16/33.19 % (3616518)Termination reason: Instruction limit % 229.16/33.19 % (3616518)Termination phase: Saturation % 229.16/33.19 % (3616518)Time elapsed: 0.637 s % 229.16/33.19 % (3616518)Peak memory usage: 120 MB % 229.16/33.19 % (3616518)Instructions burned: 1701 (million) % 229.16/33.19 % (3616521)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=1158470080:i=57001:doe=on:nm=0:rtra=on:gtg=exists_sym_2701 on theBenchmark for (2701ds/57001Mi) % 229.16/33.19 % (3616514)Instruction limit reached! % 229.16/33.19 % (3616514)------------------------------ % 229.16/33.19 % (3616514)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 229.16/33.19 % (3616514)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 229.16/33.19 % (3616514)CaDiCaL version: 2.1.3 % 229.16/33.19 % (3616514)Termination reason: Instruction limit % 229.16/33.19 % (3616514)Termination phase: Saturation % 229.16/33.19 % (3616514)Time elapsed: 1.312 s % 229.16/33.19 % (3616514)Peak memory usage: 119 MB % 229.16/33.19 % (3616514)Instructions burned: 6808 (million) % 229.16/33.19 % (3616523)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 % 229.16/33.19 % (3616523)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=3070821852:i=8622:aac=none:nm=0:rtra=on:rawr=on_2697 on theBenchmark for (2697ds/8622Mi) % 232.19/33.66 % (3616517)Instruction limit reached! % 232.19/33.66 % (3616517)------------------------------ % 232.19/33.66 % (3616517)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 232.19/33.66 % (3616517)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 232.19/33.66 % (3616517)CaDiCaL version: 2.1.3 % 232.19/33.66 % (3616517)Termination reason: Instruction limit % 232.19/33.66 % (3616517)Termination phase: Saturation % 232.19/33.66 % (3616517)Time elapsed: 1.535 s % 232.19/33.66 % (3616517)Peak memory usage: 136 MB % 232.19/33.66 % (3616517)Instructions burned: 4082 (million) % 232.19/33.66 % (3616525)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=4244838709:i=24:doe=on:rtra=on:gtg=exists_top:ss=axioms_2693 on theBenchmark for (2693ds/24Mi) % 232.19/33.66 % (3616525)Instruction limit reached! % 232.19/33.66 % (3616525)------------------------------ % 232.19/33.66 % (3616525)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 232.19/33.66 % (3616525)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 232.19/33.66 % (3616525)CaDiCaL version: 2.1.3 % 232.19/33.66 % (3616525)Termination reason: Instruction limit % 232.19/33.66 % (3616525)Termination phase: Property scanning % 232.19/33.66 % (3616525)Time elapsed: 0.010 s % 232.19/33.66 % (3616525)Peak memory usage: 85 MB % 232.19/33.66 % (3616525)Instructions burned: 26 (million) % 232.19/33.66 % (3616527)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=61292576:i=614:kws=precedence:nm=0:rtra=on_2691 on theBenchmark for (2691ds/614Mi) % 232.19/33.66 % (3616527)Instruction limit reached! % 232.19/33.66 % (3616527)------------------------------ % 232.19/33.66 % (3616527)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 232.19/33.66 % (3616527)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 232.19/33.66 % (3616527)CaDiCaL version: 2.1.3 % 232.19/33.66 % (3616527)Termination reason: Instruction limit % 232.19/33.66 % (3616527)Termination phase: Saturation % 232.19/33.66 % (3616527)Time elapsed: 0.250 s % 232.19/33.66 % (3616527)Peak memory usage: 118 MB % 232.19/33.66 % (3616527)Instructions burned: 617 (million) % 232.19/33.66 % (3616529)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=1377602697:i=402:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2687 on theBenchmark for (2687ds/402Mi) % 232.19/33.66 % (3616529)Instruction limit reached! % 232.19/33.66 % (3616529)------------------------------ % 232.19/33.66 % (3616529)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 232.19/33.66 % (3616529)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 232.19/33.66 % (3616529)CaDiCaL version: 2.1.3 % 232.19/33.66 % (3616529)Termination reason: Instruction limit % 232.19/33.66 % (3616529)Termination phase: Saturation % 232.19/33.66 % (3616529)Time elapsed: 0.175 s % 232.19/33.66 % (3616529)Peak memory usage: 117 MB % 232.19/33.66 % (3616529)Instructions burned: 402 (million) % 232.19/33.66 % (3616531)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=142489967:s2a=on:i=14:rtra=on:inst=on_2683 on theBenchmark for (2683ds/14Mi) % 232.19/33.66 % (3616531)Instruction limit reached! % 232.19/33.66 % (3616531)------------------------------ % 232.19/33.66 % (3616531)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 232.19/33.66 % (3616531)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 232.19/33.66 % (3616531)CaDiCaL version: 2.1.3 % 232.19/33.66 % (3616531)Termination reason: Instruction limit % 232.19/33.66 % (3616531)Termination phase: Property scanning % 232.19/33.66 % (3616531)Time elapsed: 0.006 s % 232.19/33.66 % (3616531)Peak memory usage: 85 MB % 232.19/33.66 % (3616531)Instructions burned: 16 (million) % 232.19/33.66 % (3616523)Instruction limit reached! % 232.19/33.66 % (3616523)------------------------------ % 232.19/33.66 % (3616523)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 232.19/33.66 % (3616523)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 232.19/33.66 % (3616523)CaDiCaL version: 2.1.3 % 232.19/33.66 % (3616523)Termination reason: Instruction limit % 232.19/33.66 % (3616523)Termination phase: Saturation % 232.19/33.66 % (3616523)Time elapsed: 1.679 s % 232.19/33.66 % (3616523)Peak memory usage: 123 MB % 232.19/33.66 % (3616523)Instructions burned: 8623 (million) % 232.19/33.66 % (3616533)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=2167499905:i=8:rtra=on_2680 on theBenchmark for (2680ds/8Mi) % 236.22/34.18 % (3616533)Instruction limit reached! % 236.22/34.18 % (3616533)------------------------------ % 236.22/34.18 % (3616533)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 236.22/34.18 % (3616533)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 236.22/34.18 % (3616533)CaDiCaL version: 2.1.3 % 236.22/34.18 % (3616533)Termination reason: Instruction limit % 236.22/34.18 % (3616533)Termination phase: Property scanning % 236.22/34.18 % (3616533)Time elapsed: 0.004 s % 236.22/34.18 % (3616533)Peak memory usage: 85 MB % 236.22/34.18 % (3616533)Instructions burned: 8 (million) % 236.22/34.18 % (3616534)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=2130051951:i=92:rtra=on_2679 on theBenchmark for (2679ds/92Mi) % 236.22/34.18 % (3616534)Instruction limit reached! % 236.22/34.18 % (3616534)------------------------------ % 236.22/34.18 % (3616534)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 236.22/34.18 % (3616534)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 236.22/34.18 % (3616534)CaDiCaL version: 2.1.3 % 236.22/34.18 % (3616534)Termination reason: Instruction limit % 236.22/34.18 % (3616534)Termination phase: Saturation % 236.22/34.18 % (3616534)Time elapsed: 0.032 s % 236.22/34.18 % (3616534)Peak memory usage: 111 MB % 236.22/34.18 % (3616534)Instructions burned: 93 (million) % 236.22/34.18 % (3616538)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=1832446741:st=5:i=28:sd=10:rtra=on:ss=axioms:rawr=on_2678 on theBenchmark for (2678ds/28Mi) % 236.22/34.18 % (3616536)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=2162517891:i=66:rtra=on_2678 on theBenchmark for (2678ds/66Mi) % 236.22/34.18 % (3616538)Instruction limit reached! % 236.22/34.18 % (3616538)------------------------------ % 236.22/34.18 % (3616538)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 236.22/34.18 % (3616538)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 236.22/34.18 % (3616538)CaDiCaL version: 2.1.3 % 236.22/34.18 % (3616538)Termination reason: Instruction limit % 236.22/34.18 % (3616538)Termination phase: SInE selection % 236.22/34.18 % (3616538)Time elapsed: 0.006 s % 236.22/34.18 % (3616538)Peak memory usage: 85 MB % 236.22/34.18 % (3616538)Instructions burned: 32 (million) % 236.22/34.18 % (3616536)Instruction limit reached! % 236.22/34.18 % (3616536)------------------------------ % 236.22/34.18 % (3616536)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 236.22/34.18 % (3616536)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 236.22/34.18 % (3616536)CaDiCaL version: 2.1.3 % 236.22/34.18 % (3616536)Termination reason: Instruction limit % 236.22/34.18 % (3616536)Termination phase: Property scanning % 236.22/34.18 % (3616536)Time elapsed: 0.025 s % 236.22/34.18 % (3616536)Peak memory usage: 86 MB % 236.22/34.18 % (3616536)Instructions burned: 68 (million) % 236.22/34.18 % (3616541)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=2375902173:i=58:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2677 on theBenchmark for (2677ds/58Mi) % 236.22/34.18 % (3616541)Instruction limit reached! % 236.22/34.18 % (3616541)------------------------------ % 236.22/34.18 % (3616541)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 236.22/34.18 % (3616541)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 236.22/34.18 % (3616541)CaDiCaL version: 2.1.3 % 236.22/34.18 % (3616541)Termination reason: Instruction limit % 236.22/34.18 % (3616541)Termination phase: Property scanning % 236.22/34.18 % (3616541)Time elapsed: 0.011 s % 236.22/34.18 % (3616541)Peak memory usage: 85 MB % 236.22/34.18 % (3616541)Instructions burned: 59 (million) % 236.22/34.18 % (3616542)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=151589338:cond=on:i=32:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2676 on theBenchmark for (2676ds/32Mi) % 236.22/34.18 % (3616542)Instruction limit reached! % 236.22/34.18 % (3616542)------------------------------ % 236.22/34.18 % (3616542)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 236.22/34.18 % (3616542)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 236.22/34.18 % (3616542)CaDiCaL version: 2.1.3 % 236.22/34.18 % (3616542)Termination reason: Instruction limit % 236.22/34.18 % (3616542)Termination phase: Property scanning % 236.22/34.18 % (3616542)Time elapsed: 0.013 s % 236.22/34.18 % (3616542)Peak memory usage: 86 MB % 236.22/34.18 % (3616542)Instructions burned: 34 (million) % 239.37/34.67 % (3616544)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=1166170046:i=48:canc=force:rtra=on_2675 on theBenchmark for (2675ds/48Mi) % 239.37/34.67 % (3616544)Instruction limit reached! % 239.37/34.67 % (3616544)------------------------------ % 239.37/34.67 % (3616544)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 239.37/34.67 % (3616544)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 239.37/34.67 % (3616544)CaDiCaL version: 2.1.3 % 239.37/34.67 % (3616544)Termination reason: Instruction limit % 239.37/34.67 % (3616544)Termination phase: Property scanning % 239.37/34.67 % (3616544)Time elapsed: 0.010 s % 239.37/34.67 % (3616544)Peak memory usage: 85 MB % 239.37/34.67 % (3616544)Instructions burned: 50 (million) % 239.37/34.67 % (3616546)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=2763009955:i=54:canc=cautious:fsr=off:rtra=on_2675 on theBenchmark for (2675ds/54Mi) % 239.37/34.67 % (3616546)Instruction limit reached! % 239.37/34.67 % (3616546)------------------------------ % 239.37/34.67 % (3616546)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 239.37/34.67 % (3616546)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 239.37/34.67 % (3616546)CaDiCaL version: 2.1.3 % 239.37/34.67 % (3616546)Termination reason: Instruction limit % 239.37/34.67 % (3616546)Termination phase: Property scanning % 239.37/34.67 % (3616546)Time elapsed: 0.021 s % 239.37/34.67 % (3616546)Peak memory usage: 85 MB % 239.37/34.67 % (3616546)Instructions burned: 56 (million) % 239.37/34.67 % (3616548)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=446188645:i=170:gtgl=4:rtra=on:gtg=exists_sym_2674 on theBenchmark for (2674ds/170Mi) % 239.37/34.67 % (3616548)Instruction limit reached! % 239.37/34.67 % (3616548)------------------------------ % 239.37/34.67 % (3616548)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 239.37/34.67 % (3616548)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 239.37/34.67 % (3616548)CaDiCaL version: 2.1.3 % 239.37/34.67 % (3616548)Termination reason: Instruction limit % 239.37/34.67 % (3616548)Termination phase: Saturation % 239.37/34.67 % (3616548)Time elapsed: 0.033 s % 239.37/34.67 % (3616548)Peak memory usage: 86 MB % 239.37/34.67 % (3616548)Instructions burned: 175 (million) % 239.37/34.67 % (3616550)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=4116208318:i=4:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2673 on theBenchmark for (2673ds/4Mi) % 239.37/34.67 % (3616550)Instruction limit reached! % 239.37/34.67 % (3616550)------------------------------ % 239.37/34.67 % (3616550)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 239.37/34.67 % (3616550)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 239.37/34.67 % (3616550)CaDiCaL version: 2.1.3 % 239.37/34.67 % (3616550)Termination reason: Instruction limit % 239.37/34.67 % (3616550)Termination phase: Property scanning % 239.37/34.67 % (3616550)Time elapsed: 0.002 s % 239.37/34.67 % (3616550)Peak memory usage: 85 MB % 239.37/34.67 % (3616550)Instructions burned: 5 (million) % 239.37/34.67 % (3616552)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=2498444938:i=362:rtra=on:ss=axioms:ev=cautious_2673 on theBenchmark for (2673ds/362Mi) % 239.37/34.67 % (3616552)Refutation not found, incomplete strategy % 239.37/34.67 % (3616552)------------------------------ % 239.37/34.67 % (3616552)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 239.37/34.67 % (3616552)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 239.37/34.67 % (3616552)CaDiCaL version: 2.1.3 % 239.37/34.67 % (3616552)Termination reason: Refutation not found, incomplete strategy % 239.37/34.67 % (3616552)Time elapsed: 0.008 s % 239.37/34.67 % (3616552)Peak memory usage: 87 MB % 239.37/34.67 % (3616552)Instructions burned: 40 (million) % 239.37/34.67 % (3616552)------------------------------ % 239.37/34.67 % (3616552)------------------------------ % 239.37/34.67 % (3616555)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=1041314864:i=8:ep=RST:ins=2:rtra=on_2672 on theBenchmark for (2672ds/8Mi) % 239.37/34.67 % (3616555)Instruction limit reached! % 239.37/34.67 % (3616555)------------------------------ % 239.37/34.67 % (3616555)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 239.37/34.67 % (3616555)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 239.37/34.67 % (3616555)CaDiCaL version: 2.1.3 % 239.37/34.67 % (3616555)Termination reason: Instruction limit % 243.96/35.29 % (3616555)Termination phase: Property scanning % 243.96/35.29 % (3616555)Time elapsed: 0.004 s % 243.96/35.29 % (3616555)Peak memory usage: 85 MB % 243.96/35.29 % (3616555)Instructions burned: 10 (million) % 243.96/35.29 % (3616557)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=387049645:i=132:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2670 on theBenchmark for (2670ds/132Mi) % 243.96/35.29 % (3616557)Instruction limit reached! % 243.96/35.29 % (3616557)------------------------------ % 243.96/35.29 % (3616557)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 243.96/35.29 % (3616557)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 243.96/35.29 % (3616557)CaDiCaL version: 2.1.3 % 243.96/35.29 % (3616557)Termination reason: Instruction limit % 243.96/35.29 % (3616557)Termination phase: Saturation % 243.96/35.29 % (3616557)Time elapsed: 0.053 s % 243.96/35.29 % (3616557)Peak memory usage: 128 MB % 243.96/35.29 % (3616557)Instructions burned: 136 (million) % 243.96/35.29 % (3616558)lrs+10_1_thi=all:si=on:fd=off:random_seed=3760393258:i=106:rtra=on:gtg=all_2670 on theBenchmark for (2670ds/106Mi) % 243.96/35.29 % (3616558)Instruction limit reached! % 243.96/35.29 % (3616558)------------------------------ % 243.96/35.29 % (3616558)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 243.96/35.29 % (3616558)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 243.96/35.29 % (3616558)CaDiCaL version: 2.1.3 % 243.96/35.29 % (3616558)Termination reason: Instruction limit % 243.96/35.29 % (3616558)Termination phase: Property scanning % 243.96/35.29 % (3616558)Time elapsed: 0.039 s % 243.96/35.29 % (3616558)Peak memory usage: 85 MB % 243.96/35.29 % (3616558)Instructions burned: 107 (million) % 243.96/35.29 % (3616561)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=2750743603:i=16:ep=RST:nm=16:rtra=on:gtg=exists_top_2668 on theBenchmark for (2668ds/16Mi) % 243.96/35.29 % (3616561)Instruction limit reached! % 243.96/35.29 % (3616561)------------------------------ % 243.96/35.29 % (3616561)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 243.96/35.29 % (3616561)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 243.96/35.29 % (3616561)CaDiCaL version: 2.1.3 % 243.96/35.29 % (3616561)Termination reason: Instruction limit % 243.96/35.29 % (3616561)Termination phase: Property scanning % 243.96/35.29 % (3616561)Time elapsed: 0.003 s % 243.96/35.29 % (3616561)Peak memory usage: 85 MB % 243.96/35.29 % (3616561)Instructions burned: 16 (million) % 243.96/35.29 % (3616562)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=1489184037:st=3:i=4:rtra=on:ss=axioms_2668 on theBenchmark for (2668ds/4Mi) % 243.96/35.29 % (3616562)Instruction limit reached! % 243.96/35.29 % (3616562)------------------------------ % 243.96/35.29 % (3616562)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 243.96/35.29 % (3616562)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 243.96/35.29 % (3616562)CaDiCaL version: 2.1.3 % 243.96/35.29 % (3616562)Termination reason: Instruction limit % 243.96/35.29 % (3616562)Termination phase: shuffling % 243.96/35.29 % (3616562)Time elapsed: 0.002 s % 243.96/35.29 % (3616562)Peak memory usage: 85 MB % 243.96/35.29 % (3616562)Instructions burned: 4 (million) % 243.96/35.29 % (3616564)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=3841775836:i=4:doe=on:canc=force:asg=cautious:rtra=on_2667 on theBenchmark for (2667ds/4Mi) % 243.96/35.29 % (3616564)Instruction limit reached! % 243.96/35.29 % (3616564)------------------------------ % 243.96/35.29 % (3616564)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 243.96/35.29 % (3616564)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 243.96/35.29 % (3616564)CaDiCaL version: 2.1.3 % 243.96/35.29 % (3616564)Termination reason: Instruction limit % 243.96/35.29 % (3616564)Termination phase: Property scanning % 243.96/35.29 % (3616564)Time elapsed: 0.002 s % 243.96/35.29 % (3616564)Peak memory usage: 85 MB % 243.96/35.29 % (3616564)Instructions burned: 9 (million) % 243.96/35.29 % (3616568)dis+10_1_si=on:random_seed=1624074827:i=20:ep=R:rtra=on_2666 on theBenchmark for (2666ds/20Mi) % 243.96/35.29 % (3616566)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=1273087292:i=254:doe=on:rtra=on_2666 on theBenchmark for (2666ds/254Mi) % 243.96/35.29 % (3616568)Instruction limit reached! % 243.96/35.29 % (3616568)------------------------------ % 243.96/35.29 % (3616568)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 249.17/36.13 % (3616568)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 249.17/36.13 % (3616568)CaDiCaL version: 2.1.3 % 249.17/36.13 % (3616568)Termination reason: Instruction limit % 249.17/36.13 % (3616568)Termination phase: Property scanning % 249.17/36.13 % (3616568)Time elapsed: 0.004 s % 249.17/36.13 % (3616568)Peak memory usage: 85 MB % 249.17/36.13 % (3616568)Instructions burned: 21 (million) % 249.17/36.13 % (3616566)Instruction limit reached! % 249.17/36.13 % (3616566)------------------------------ % 249.17/36.13 % (3616566)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 249.17/36.13 % (3616566)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 249.17/36.13 % (3616566)CaDiCaL version: 2.1.3 % 249.17/36.13 % (3616566)Termination reason: Instruction limit % 249.17/36.13 % (3616566)Termination phase: Saturation % 249.17/36.13 % (3616566)Time elapsed: 0.118 s % 249.17/36.13 % (3616566)Peak memory usage: 113 MB % 249.17/36.13 % (3616566)Instructions burned: 255 (million) % 249.17/36.13 % (3616571)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=1014090194:i=52:canc=cautious:av=off:rtra=on_2665 on theBenchmark for (2665ds/52Mi) % 249.17/36.13 % (3616571)Instruction limit reached! % 249.17/36.13 % (3616571)------------------------------ % 249.17/36.13 % (3616571)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 249.17/36.13 % (3616571)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 249.17/36.13 % (3616571)CaDiCaL version: 2.1.3 % 249.17/36.13 % (3616571)Termination reason: Instruction limit % 249.17/36.13 % (3616571)Termination phase: Property scanning % 249.17/36.13 % (3616571)Time elapsed: 0.011 s % 249.17/36.13 % (3616571)Peak memory usage: 85 MB % 249.17/36.13 % (3616571)Instructions burned: 58 (million) % 249.17/36.13 % (3616574)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=2104278025:i=4:fsr=off:rtra=on:inst=on_2664 on theBenchmark for (2664ds/4Mi) % 249.17/36.13 % (3616573)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=3697794891:avsq=on:i=70:doe=on:thsqd=64:nm=64:fsr=off:thsqc=32:rtra=on:tac=light:ss=included:thsq=on:ev=off:sgt=32_2664 on theBenchmark for (2664ds/70Mi) % 249.17/36.13 % (3616574)Instruction limit reached! % 249.17/36.13 % (3616574)------------------------------ % 249.17/36.13 % (3616574)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 249.17/36.13 % (3616574)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 249.17/36.13 % (3616574)CaDiCaL version: 2.1.3 % 249.17/36.13 % (3616574)Termination reason: Instruction limit % 249.17/36.13 % (3616574)Termination phase: Property scanning % 249.17/36.13 % (3616574)Time elapsed: 0.002 s % 249.17/36.13 % (3616574)Peak memory usage: 85 MB % 249.17/36.13 % (3616574)Instructions burned: 9 (million) % 249.17/36.13 % (3616573)Instruction limit reached! % 249.17/36.13 % (3616573)------------------------------ % 249.17/36.13 % (3616573)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 249.17/36.13 % (3616573)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 249.17/36.13 % (3616573)CaDiCaL version: 2.1.3 % 249.17/36.13 % (3616573)Termination reason: Instruction limit % 249.17/36.13 % (3616573)Termination phase: Property scanning % 249.17/36.13 % (3616573)Time elapsed: 0.026 s % 249.17/36.13 % (3616573)Peak memory usage: 86 MB % 249.17/36.13 % (3616573)Instructions burned: 70 (million) % 249.17/36.13 % (3616577)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=3336693321:s2a=on:i=16:kws=inv_precedence:doe=on:rtra=on_2662 on theBenchmark for (2662ds/16Mi) % 250.41/36.13 % (3616577)Instruction limit reached! % 250.41/36.13 % (3616577)------------------------------ % 250.41/36.13 % (3616577)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 250.41/36.13 % (3616577)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 250.41/36.13 % (3616577)CaDiCaL version: 2.1.3 % 250.41/36.13 % (3616577)Termination reason: Instruction limit % 250.41/36.13 % (3616577)Termination phase: Property scanning % 250.41/36.13 % (3616577)Time elapsed: 0.004 s % 250.41/36.13 % (3616577)Peak memory usage: 85 MB % 250.41/36.13 % (3616577)Instructions burned: 21 (million) % 250.41/36.13 % (3616578)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=1116916123:i=740:ep=RS:fsr=off:rtra=on_2662 on theBenchmark for (2662ds/740Mi) % 250.41/36.13 % (3616580)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=348036365:i=26:av=off:rtra=on:gtg=exists_sym:ev=force_2661 on theBenchmark for (2661ds/26Mi) % 256.39/37.13 % (3616578)Refutation not found, incomplete strategy % 256.39/37.13 % (3616578)------------------------------ % 256.39/37.13 % (3616578)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 256.39/37.13 % (3616578)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 256.39/37.13 % (3616578)CaDiCaL version: 2.1.3 % 256.39/37.13 % (3616578)Termination reason: Refutation not found, incomplete strategy % 256.39/37.13 % (3616578)Time elapsed: 0.060 s % 256.39/37.13 % (3616578)Peak memory usage: 89 MB % 256.39/37.13 % (3616578)Instructions burned: 161 (million) % 256.39/37.13 % (3616580)Instruction limit reached! % 256.39/37.13 % (3616580)------------------------------ % 256.39/37.13 % (3616580)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 256.39/37.13 % (3616580)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 256.39/37.13 % (3616580)CaDiCaL version: 2.1.3 % 256.39/37.13 % (3616580)Termination reason: Instruction limit % 256.39/37.13 % (3616580)Termination phase: shuffling % 256.39/37.13 % (3616580)Time elapsed: 0.005 s % 256.39/37.13 % (3616580)Peak memory usage: 85 MB % 256.39/37.13 % (3616580)Instructions burned: 29 (million) % 256.39/37.13 % (3616583)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=439665705:i=452:rtra=on:gtg=position:ss=axioms_2660 on theBenchmark for (2660ds/452Mi) % 256.39/37.13 % (3616583)Refutation not found, incomplete strategy % 256.39/37.13 % (3616583)------------------------------ % 256.39/37.13 % (3616583)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 256.39/37.13 % (3616583)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 256.39/37.13 % (3616583)CaDiCaL version: 2.1.3 % 256.39/37.13 % (3616583)Termination reason: Refutation not found, incomplete strategy % 256.39/37.13 % (3616583)Time elapsed: 0.029 s % 256.39/37.13 % (3616583)Peak memory usage: 111 MB % 256.39/37.13 % (3616583)Instructions burned: 72 (million) % 256.39/37.13 % (3616578)------------------------------ % 256.39/37.13 % (3616578)------------------------------ % 256.39/37.13 % (3616583)------------------------------ % 256.39/37.13 % (3616583)------------------------------ % 256.39/37.13 % (3616585)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=2127253420:i=20:rtra=on_2658 on theBenchmark for (2658ds/20Mi) % 256.39/37.13 % (3616585)Instruction limit reached! % 256.39/37.13 % (3616585)------------------------------ % 256.39/37.13 % (3616585)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 256.39/37.13 % (3616585)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 256.39/37.13 % (3616585)CaDiCaL version: 2.1.3 % 256.39/37.13 % (3616585)Termination reason: Instruction limit % 256.39/37.13 % (3616585)Termination phase: Property scanning % 256.39/37.13 % (3616585)Time elapsed: 0.009 s % 256.39/37.13 % (3616585)Peak memory usage: 85 MB % 256.39/37.13 % (3616585)Instructions burned: 23 (million) % 256.39/37.13 % (3616586)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=3293256410:i=142:rtra=on:gtg=exists_top_2657 on theBenchmark for (2657ds/142Mi) % 256.39/37.13 % (3616586)Instruction limit reached! % 256.39/37.13 % (3616586)------------------------------ % 256.39/37.13 % (3616586)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 256.39/37.13 % (3616586)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 256.39/37.13 % (3616586)CaDiCaL version: 2.1.3 % 256.39/37.13 % (3616586)Termination reason: Instruction limit % 256.39/37.13 % (3616586)Termination phase: Saturation % 256.39/37.13 % (3616586)Time elapsed: 0.055 s % 256.39/37.13 % (3616586)Peak memory usage: 128 MB % 256.39/37.13 % (3616586)Instructions burned: 149 (million) % 256.39/37.13 % (3616588)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=138204977:i=150:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2656 on theBenchmark for (2656ds/150Mi) % 256.39/37.13 % (3616590)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=3557564108:i=588:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2655 on theBenchmark for (2655ds/588Mi) % 256.39/37.13 % (3616588)Instruction limit reached! % 256.39/37.13 % (3616588)------------------------------ % 256.39/37.13 % (3616588)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 256.39/37.13 % (3616588)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 256.39/37.13 % (3616588)CaDiCaL version: 2.1.3 % 256.39/37.13 % (3616588)Termination reason: Instruction limit % 262.59/37.94 % (3616588)Termination phase: Saturation % 262.59/37.94 % (3616588)Time elapsed: 0.056 s % 262.59/37.94 % (3616588)Peak memory usage: 88 MB % 262.59/37.94 % (3616588)Instructions burned: 151 (million) % 262.59/37.94 % (3616590)Instruction limit reached! % 262.59/37.94 % (3616590)------------------------------ % 262.59/37.94 % (3616590)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 262.59/37.94 % (3616590)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 262.59/37.94 % (3616590)CaDiCaL version: 2.1.3 % 262.59/37.94 % (3616590)Termination reason: Instruction limit % 262.59/37.94 % (3616590)Termination phase: Saturation % 262.59/37.94 % (3616590)Time elapsed: 0.131 s % 262.59/37.94 % (3616590)Peak memory usage: 92 MB % 262.59/37.94 % (3616590)Instructions burned: 591 (million) % 262.59/37.94 % (3616593)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=1604231957:i=260:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2654 on theBenchmark for (2654ds/260Mi) % 262.59/37.94 % (3616594)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=3840955265:i=262:rtra=on_2652 on theBenchmark for (2652ds/262Mi) % 262.59/37.94 % (3616593)Instruction limit reached! % 262.59/37.94 % (3616593)------------------------------ % 262.59/37.94 % (3616593)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 262.59/37.94 % (3616593)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 262.59/37.94 % (3616593)CaDiCaL version: 2.1.3 % 262.59/37.94 % (3616593)Termination reason: Instruction limit % 262.59/37.94 % (3616593)Termination phase: Saturation % 262.59/37.94 % (3616593)Time elapsed: 0.137 s % 262.59/37.94 % (3616593)Peak memory usage: 115 MB % 262.59/37.94 % (3616593)Instructions burned: 261 (million) % 262.59/37.94 % (3616594)Instruction limit reached! % 262.59/37.94 % (3616594)------------------------------ % 262.59/37.94 % (3616594)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 262.59/37.94 % (3616594)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 262.59/37.94 % (3616594)CaDiCaL version: 2.1.3 % 262.59/37.94 % (3616594)Termination reason: Instruction limit % 262.59/37.94 % (3616594)Termination phase: Saturation % 262.59/37.94 % (3616594)Time elapsed: 0.079 s % 262.59/37.94 % (3616594)Peak memory usage: 129 MB % 262.59/37.94 % (3616594)Instructions burned: 267 (million) % 262.59/37.94 % (3616597)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=2351778723:i=80:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2651 on theBenchmark for (2651ds/80Mi) % 262.59/37.94 % (3616598)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=1798993766:i=614:rtra=on:gtg=exists_top_2650 on theBenchmark for (2650ds/614Mi) % 262.59/37.94 % (3616597)Instruction limit reached! % 262.59/37.94 % (3616597)------------------------------ % 262.59/37.94 % (3616597)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 262.59/37.94 % (3616597)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 262.59/37.94 % (3616597)CaDiCaL version: 2.1.3 % 262.59/37.94 % (3616597)Termination reason: Instruction limit % 262.59/37.94 % (3616597)Termination phase: Property scanning % 262.59/37.94 % (3616597)Time elapsed: 0.030 s % 262.59/37.94 % (3616597)Peak memory usage: 85 MB % 262.59/37.94 % (3616597)Instructions burned: 81 (million) % 262.59/37.94 % (3616598)Refutation not found, incomplete strategy % 262.59/37.94 % (3616598)------------------------------ % 262.59/37.94 % (3616598)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 262.59/37.94 % (3616598)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 262.59/37.94 % (3616598)CaDiCaL version: 2.1.3 % 262.59/37.94 % (3616598)Termination reason: Refutation not found, incomplete strategy % 262.59/37.94 % (3616598)Time elapsed: 0.044 s % 262.59/37.94 % (3616598)Peak memory usage: 89 MB % 262.59/37.94 % (3616598)Instructions burned: 226 (million) % 262.59/37.94 % (3616598)------------------------------ % 262.59/37.94 % (3616598)------------------------------ % 262.59/37.94 % (3616601)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=219545850:s2a=on:i=1196:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2649 on theBenchmark for (2649ds/1196Mi) % 262.59/37.94 % (3616603)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=3470494194:i=262:canc=cautious:fsr=off:rtra=on_2647 on theBenchmark for (2647ds/262Mi) % 262.59/37.94 % (3616603)Instruction limit reached! % 262.59/37.94 % (3616603)------------------------------ % 262.59/37.94 % (3616603)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 262.59/37.94 % (3616603)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.00/38.83 % (3616603)CaDiCaL version: 2.1.3 % 269.00/38.83 % (3616603)Termination reason: Instruction limit % 269.00/38.83 % (3616603)Termination phase: Saturation % 269.00/38.83 % (3616603)Time elapsed: 0.069 s % 269.00/38.83 % (3616603)Peak memory usage: 118 MB % 269.00/38.83 % (3616603)Instructions burned: 264 (million) % 269.00/38.83 % (3616605)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=3475989549:s2pl=no:i=518:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2645 on theBenchmark for (2645ds/518Mi) % 269.00/38.83 % (3616605)Refutation not found, incomplete strategy % 269.00/38.83 % (3616605)------------------------------ % 269.00/38.83 % (3616605)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 269.00/38.83 % (3616605)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.00/38.83 % (3616605)CaDiCaL version: 2.1.3 % 269.00/38.83 % (3616605)Termination reason: Refutation not found, incomplete strategy % 269.00/38.83 % (3616605)Time elapsed: 0.030 s % 269.00/38.83 % (3616605)Peak memory usage: 111 MB % 269.00/38.83 % (3616605)Instructions burned: 76 (million) % 269.00/38.83 % (3616605)------------------------------ % 269.00/38.83 % (3616605)------------------------------ % 269.00/38.83 % (3616601)Instruction limit reached! % 269.00/38.83 % (3616601)------------------------------ % 269.00/38.83 % (3616601)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 269.00/38.83 % (3616601)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.00/38.83 % (3616601)CaDiCaL version: 2.1.3 % 269.00/38.83 % (3616601)Termination reason: Instruction limit % 269.00/38.83 % (3616601)Termination phase: Saturation % 269.00/38.83 % (3616601)Time elapsed: 0.500 s % 269.00/38.83 % (3616601)Peak memory usage: 137 MB % 269.00/38.83 % (3616601)Instructions burned: 1196 (million) % 269.00/38.83 % (3616607)dis+10_1_si=on:random_seed=3310981543:s2a=on:i=2000:rtra=on:gtg=exists_all_2642 on theBenchmark for (2642ds/2000Mi) % 269.00/38.83 % (3616608)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=67927683:i=766:fsr=off:rtra=on:ev=force_2642 on theBenchmark for (2642ds/766Mi) % 269.00/38.83 % (3616608)Instruction limit reached! % 269.00/38.83 % (3616608)------------------------------ % 269.00/38.83 % (3616608)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 269.00/38.83 % (3616608)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.00/38.83 % (3616608)CaDiCaL version: 2.1.3 % 269.00/38.83 % (3616608)Termination reason: Instruction limit % 269.00/38.83 % (3616608)Termination phase: Saturation % 269.00/38.83 % (3616608)Time elapsed: 0.293 s % 269.00/38.83 % (3616608)Peak memory usage: 91 MB % 269.00/38.83 % (3616608)Instructions burned: 769 (million) % 269.00/38.83 % (3616607)Instruction limit reached! % 269.00/38.83 % (3616607)------------------------------ % 269.00/38.83 % (3616607)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 269.00/38.83 % (3616607)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.00/38.83 % (3616607)CaDiCaL version: 2.1.3 % 269.00/38.83 % (3616607)Termination reason: Instruction limit % 269.00/38.83 % (3616607)Termination phase: Saturation % 269.00/38.83 % (3616607)Time elapsed: 0.375 s % 269.00/38.83 % (3616607)Peak memory usage: 91 MB % 269.00/38.83 % (3616607)Instructions burned: 2005 (million) % 269.00/38.83 % (3616612)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=495250000:i=130:nm=16:rtra=on_2637 on theBenchmark for (2637ds/130Mi) % 269.00/38.83 % (3616611)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=1105056417:i=282:doe=on:rtra=on_2638 on theBenchmark for (2638ds/282Mi) % 269.00/38.83 % (3616612)Instruction limit reached! % 269.00/38.83 % (3616612)------------------------------ % 269.00/38.83 % (3616612)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 269.00/38.83 % (3616612)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.00/38.83 % (3616612)CaDiCaL version: 2.1.3 % 269.00/38.83 % (3616612)Termination reason: Instruction limit % 269.00/38.83 % (3616612)Termination phase: Saturation % 269.00/38.83 % (3616612)Time elapsed: 0.027 s % 269.00/38.83 % (3616612)Peak memory usage: 89 MB % 269.00/38.83 % (3616612)Instructions burned: 135 (million) % 269.00/38.83 % (3616611)Instruction limit reached! % 269.00/38.83 % (3616611)------------------------------ % 269.00/38.83 % (3616611)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 269.00/38.83 % (3616611)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 276.11/39.86 % (3616611)CaDiCaL version: 2.1.3 % 276.11/39.86 % (3616611)Termination reason: Instruction limit % 276.11/39.86 % (3616611)Termination phase: Saturation % 276.11/39.86 % (3616611)Time elapsed: 0.105 s % 276.11/39.86 % (3616611)Peak memory usage: 89 MB % 276.11/39.86 % (3616611)Instructions burned: 283 (million) % 276.11/39.86 % (3616615)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=2758125907:i=242:nm=16:rtra=on_2636 on theBenchmark for (2636ds/242Mi) % 276.11/39.86 % (3616615)Instruction limit reached! % 276.11/39.86 % (3616615)------------------------------ % 276.11/39.86 % (3616615)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 276.11/39.86 % (3616615)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 276.11/39.86 % (3616615)CaDiCaL version: 2.1.3 % 276.11/39.86 % (3616615)Termination reason: Instruction limit % 276.11/39.86 % (3616615)Termination phase: Saturation % 276.11/39.86 % (3616615)Time elapsed: 0.052 s % 276.11/39.86 % (3616615)Peak memory usage: 90 MB % 276.11/39.86 % (3616615)Instructions burned: 246 (million) % 276.11/39.86 % (3616616)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=3176897522:s2a=on:i=256:s2at=5:ins=3:rtra=on_2635 on theBenchmark for (2635ds/256Mi) % 276.11/39.86 % (3616618)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=301888344:i=78:ins=3:rtra=on_2634 on theBenchmark for (2634ds/78Mi) % 276.11/39.86 % (3616618)Instruction limit reached! % 276.11/39.86 % (3616618)------------------------------ % 276.11/39.86 % (3616618)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 276.11/39.86 % (3616618)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 276.11/39.86 % (3616618)CaDiCaL version: 2.1.3 % 276.11/39.86 % (3616618)Termination reason: Instruction limit % 276.11/39.86 % (3616618)Termination phase: Property scanning % 276.11/39.86 % (3616618)Time elapsed: 0.015 s % 276.11/39.86 % (3616618)Peak memory usage: 86 MB % 276.11/39.86 % (3616618)Instructions burned: 79 (million) % 276.11/39.86 % (3616616)Refutation not found, incomplete strategy % 276.11/39.86 % (3616616)------------------------------ % 276.11/39.86 % (3616616)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 276.11/39.86 % (3616616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 276.11/39.86 % (3616616)CaDiCaL version: 2.1.3 % 276.11/39.86 % (3616616)Termination reason: Refutation not found, incomplete strategy % 276.11/39.86 % (3616616)Time elapsed: 0.114 s % 276.11/39.86 % (3616616)Peak memory usage: 114 MB % 276.11/39.86 % (3616616)Instructions burned: 238 (million) % 276.11/39.86 % (3616621)dis+1010_1_to=kbo:si=on:random_seed=2087604770:i=350:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2633 on theBenchmark for (2633ds/350Mi) % 276.11/39.86 % (3616621)Instruction limit reached! % 276.11/39.86 % (3616621)------------------------------ % 276.11/39.86 % (3616621)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 276.11/39.86 % (3616621)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 276.11/39.86 % (3616621)CaDiCaL version: 2.1.3 % 276.11/39.86 % (3616621)Termination reason: Instruction limit % 276.11/39.86 % (3616621)Termination phase: Saturation % 276.11/39.86 % (3616621)Time elapsed: 0.078 s % 276.11/39.86 % (3616621)Peak memory usage: 91 MB % 276.11/39.86 % (3616621)Instructions burned: 354 (million) % 276.11/39.86 % (3616616)------------------------------ % 276.11/39.86 % (3616616)------------------------------ % 276.11/39.86 % (3616623)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=3600849315:i=658:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2631 on theBenchmark for (2631ds/658Mi) % 276.11/39.86 % (3616624)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=3852595720:s2a=on:i=966:doe=on:nm=32:rtra=on_2630 on theBenchmark for (2630ds/966Mi) % 276.11/39.86 % (3616623)Instruction limit reached! % 276.11/39.86 % (3616623)------------------------------ % 276.11/39.86 % (3616623)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 276.11/39.86 % (3616623)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 276.11/39.86 % (3616623)CaDiCaL version: 2.1.3 % 276.11/39.86 % (3616623)Termination reason: Instruction limit % 276.11/39.86 % (3616623)Termination phase: Saturation % 276.11/39.86 % (3616623)Time elapsed: 0.146 s % 276.11/39.86 % (3616623)Peak memory usage: 117 MB % 276.11/39.86 % (3616623)Instructions burned: 659 (million) % 282.54/40.72 % (3616627)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=931014612:thitd=on:i=430:nm=0:rtra=on:ev=force_2628 on theBenchmark for (2628ds/430Mi) % 282.54/40.72 % (3616627)Instruction limit reached! % 282.54/40.72 % (3616627)------------------------------ % 282.54/40.72 % (3616627)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 282.54/40.72 % (3616627)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.54/40.72 % (3616627)CaDiCaL version: 2.1.3 % 282.54/40.72 % (3616627)Termination reason: Instruction limit % 282.54/40.72 % (3616627)Termination phase: Saturation % 282.54/40.72 % (3616627)Time elapsed: 0.110 s % 282.54/40.72 % (3616627)Peak memory usage: 130 MB % 282.54/40.72 % (3616627)Instructions burned: 431 (million) % 282.54/40.72 % (3616629)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=178267788:i=698:rtra=on_2626 on theBenchmark for (2626ds/698Mi) % 282.54/40.72 % (3616624)Instruction limit reached! % 282.54/40.72 % (3616624)------------------------------ % 282.54/40.72 % (3616624)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 282.54/40.72 % (3616624)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.54/40.72 % (3616624)CaDiCaL version: 2.1.3 % 282.54/40.72 % (3616624)Termination reason: Instruction limit % 282.54/40.72 % (3616624)Termination phase: Saturation % 282.54/40.72 % (3616624)Time elapsed: 0.409 s % 282.54/40.72 % (3616624)Peak memory usage: 136 MB % 282.54/40.72 % (3616624)Instructions burned: 967 (million) % 282.54/40.72 % (3616629)Instruction limit reached! % 282.54/40.72 % (3616629)------------------------------ % 282.54/40.72 % (3616629)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 282.54/40.72 % (3616629)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.54/40.72 % (3616629)CaDiCaL version: 2.1.3 % 282.54/40.72 % (3616629)Termination reason: Instruction limit % 282.54/40.72 % (3616629)Termination phase: Saturation % 282.54/40.72 % (3616629)Time elapsed: 0.154 s % 282.54/40.72 % (3616629)Peak memory usage: 118 MB % 282.54/40.72 % (3616629)Instructions burned: 700 (million) % 282.54/40.72 % (3616631)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=3560760794:st=2:i=590:rtra=on:ss=axioms_2625 on theBenchmark for (2625ds/590Mi) % 282.54/40.72 % (3616631)Refutation not found, incomplete strategy % 282.54/40.72 % (3616631)------------------------------ % 282.54/40.72 % (3616631)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 282.54/40.72 % (3616631)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.54/40.72 % (3616631)CaDiCaL version: 2.1.3 % 282.54/40.72 % (3616631)Termination reason: Refutation not found, incomplete strategy % 282.54/40.72 % (3616631)Time elapsed: 0.026 s % 282.54/40.72 % (3616631)Peak memory usage: 88 MB % 282.54/40.72 % (3616631)Instructions burned: 70 (million) % 282.54/40.72 % (3616632)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=1198080122:i=656:kws=inv_frequency:nm=20:rtra=on_2623 on theBenchmark for (2623ds/656Mi) % 282.54/40.72 % (3616632)Instruction limit reached! % 282.54/40.72 % (3616632)------------------------------ % 282.54/40.72 % (3616632)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 282.54/40.72 % (3616632)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.54/40.72 % (3616632)CaDiCaL version: 2.1.3 % 282.54/40.72 % (3616632)Termination reason: Instruction limit % 282.54/40.72 % (3616632)Termination phase: Saturation % 282.54/40.72 % (3616632)Time elapsed: 0.146 s % 282.54/40.72 % (3616632)Peak memory usage: 117 MB % 282.54/40.72 % (3616632)Instructions burned: 659 (million) % 282.54/40.72 % (3616631)------------------------------ % 282.54/40.72 % (3616631)------------------------------ % 282.54/40.72 % (3616635)dis+1010_1_to=lpo:sil=128000:sas=z3:si=on:nwc=5:random_seed=3303347253:i=562:gtgl=2:rtra=on:gtg=all_2620 on theBenchmark for (2620ds/562Mi) % 282.54/40.72 % (3616636)lrs+1010_1_to=kbo:sil=128000:si=on:sos=on:urr=on:uwa=alasca_main:random_seed=3121763323:i=968:doe=on:nm=0:av=off:rtra=on:ss=axioms_2620 on theBenchmark for (2620ds/968Mi) % 282.54/40.72 % (3616636)Refutation not found, incomplete strategy % 282.54/40.72 % (3616636)------------------------------ % 282.54/40.72 % (3616636)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 282.54/40.72 % (3616636)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.54/40.72 % (3616636)CaDiCaL version: 2.1.3 % 282.54/40.72 % (3616636)Termination reason: Refutation not found, incomplete strategy % 289.43/41.70 % (3616636)Time elapsed: 0.025 s % 289.43/41.70 % (3616636)Peak memory usage: 87 MB % 289.43/41.70 % (3616636)Instructions burned: 68 (million) % 289.43/41.70 % (3616635)Instruction limit reached! % 289.43/41.70 % (3616635)------------------------------ % 289.43/41.70 % (3616635)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 289.43/41.70 % (3616635)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.43/41.70 % (3616635)CaDiCaL version: 2.1.3 % 289.43/41.70 % (3616635)Termination reason: Instruction limit % 289.43/41.70 % (3616635)Termination phase: Saturation % 289.43/41.70 % (3616635)Time elapsed: 0.123 s % 289.43/41.70 % (3616635)Peak memory usage: 115 MB % 289.43/41.70 % (3616635)Instructions burned: 562 (million) % 289.43/41.70 % (3616639)lrs+21_1_to=kbo:sil=128000:thi=neg_eq:si=on:random_seed=1757696452:i=642:canc=force:rtra=on:tac=axiom:ss=axioms:ev=force_2618 on theBenchmark for (2618ds/642Mi) % 289.43/41.70 % (3616639)Refutation not found, incomplete strategy % 289.43/41.70 % (3616639)------------------------------ % 289.43/41.70 % (3616639)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 289.43/41.70 % (3616639)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.43/41.70 % (3616639)CaDiCaL version: 2.1.3 % 289.43/41.70 % (3616639)Termination reason: Refutation not found, incomplete strategy % 289.43/41.70 % (3616639)Time elapsed: 0.029 s % 289.43/41.70 % (3616639)Peak memory usage: 112 MB % 289.43/41.70 % (3616639)Instructions burned: 73 (million) % 289.43/41.70 % (3616636)------------------------------ % 289.43/41.70 % (3616636)------------------------------ % 289.43/41.70 % (3616639)------------------------------ % 289.43/41.70 % (3616639)------------------------------ % 289.43/41.70 % (3616641)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=2402578469:i=832:rtra=on:gtg=position:ss=axioms_2616 on theBenchmark for (2616ds/832Mi) % 289.43/41.70 % (3616642)lrs+1010_1_to=kbo:tgt=ground:fde=unused:sas=z3:si=on:sp=unary_frequency:gve=force:spb=goal:tha=off:random_seed=316083533:i=942:thf=on:kws=precedence:rtra=on_2615 on theBenchmark for (2615ds/942Mi) % 289.43/41.70 % (3616641)Refutation not found, incomplete strategy % 289.43/41.70 % (3616641)------------------------------ % 289.43/41.70 % (3616641)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 289.43/41.70 % (3616641)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.43/41.70 % (3616641)CaDiCaL version: 2.1.3 % 289.43/41.70 % (3616641)Termination reason: Refutation not found, incomplete strategy % 289.43/41.70 % (3616641)Time elapsed: 0.050 s % 289.43/41.70 % (3616641)Peak memory usage: 111 MB % 289.43/41.70 % (3616641)Instructions burned: 72 (million) % 289.43/41.70 % (3616642)Instruction limit reached! % 289.43/41.70 % (3616642)------------------------------ % 289.43/41.70 % (3616642)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 289.43/41.70 % (3616642)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.43/41.70 % (3616642)CaDiCaL version: 2.1.3 % 289.43/41.70 % (3616642)Termination reason: Instruction limit % 289.43/41.70 % (3616642)Termination phase: Saturation % 289.43/41.70 % (3616642)Time elapsed: 0.211 s % 289.43/41.70 % (3616642)Peak memory usage: 113 MB % 289.43/41.70 % (3616642)Instructions burned: 945 (million) % 289.43/41.70 % (3616641)------------------------------ % 289.43/41.70 % (3616641)------------------------------ % 289.43/41.70 % (3616645)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=3385116307:avsq=on:i=552:avsqr=1,2:rtra=on_2612 on theBenchmark for (2612ds/552Mi) % 289.43/41.70 % (3616646)lrs+1010_2_to=kbo:sil=128000:tgt=ground:fde=unused:sas=z3:si=on:uwa=off:tha=off:nwc=1:random_seed=2740865241:i=750:kws=inv_arity_squared:rtra=on_2611 on theBenchmark for (2611ds/750Mi) % 289.43/41.70 % (3616645)Instruction limit reached! % 289.43/41.70 % (3616645)------------------------------ % 289.43/41.70 % (3616645)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 289.43/41.70 % (3616645)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.43/41.70 % (3616645)CaDiCaL version: 2.1.3 % 289.43/41.70 % (3616645)Termination reason: Instruction limit % 289.43/41.70 % (3616645)Termination phase: Saturation % 289.43/41.70 % (3616645)Time elapsed: 0.138 s % 289.43/41.70 % (3616645)Peak memory usage: 133 MB % 289.43/41.70 % (3616645)Instructions burned: 556 (million) % 289.43/41.70 % (3616649)lrs+10_1_to=kbo:sil=128000:tgt=full:sas=z3:si=on:uwa=func_ext:slsqc=1:flr=on:slsq=on:random_seed=1925116791:i=774:bd=preordered:rtra=on:ss=axioms:sgt=8_2609 on theBenchmark for (2609ds/774Mi) % 300.09/43.17 % (3616649)Refutation not found, incomplete strategy % 300.09/43.17 % (3616649)------------------------------ % 300.09/43.17 % (3616649)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.09/43.17 % (3616649)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.09/43.17 % (3616649)CaDiCaL version: 2.1.3 % 300.09/43.17 % (3616649)Termination reason: Refutation not found, incomplete strategy % 300.09/43.17 % (3616649)Time elapsed: 0.029 s % 300.09/43.17 % (3616649)Peak memory usage: 111 MB % 300.09/43.17 % (3616649)Instructions burned: 77 (million) % 300.09/43.17 % (3616646)Instruction limit reached! % 300.09/43.17 % (3616646)------------------------------ % 300.09/43.17 % (3616646)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.09/43.17 % (3616646)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.09/43.17 % (3616646)CaDiCaL version: 2.1.3 % 300.09/43.17 % (3616646)Termination reason: Instruction limit % 300.09/43.17 % (3616646)Termination phase: Saturation % 300.09/43.17 % (3616646)Time elapsed: 0.305 s % 300.09/43.17 % (3616646)Peak memory usage: 118 MB % 300.09/43.17 % (3616646)Instructions burned: 751 (million) % 300.09/43.17 % (3616649)------------------------------ % 300.09/43.17 % (3616649)------------------------------ % 300.09/43.17 % (3616651)lrs+10_1_to=kbo:sil=128000:fde=none:si=on:norm_ineq=on:urr=on:nwc=0.5:random_seed=1393365590:i=1026:kws=frequency:bd=all:rtra=on:gtg=exists_all:ss=axioms:sgt=4_2607 on theBenchmark for (2607ds/1026Mi) % 300.09/43.17 % (3616652)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=340084309:i=668:rtra=on_2606 on theBenchmark for (2606ds/668Mi) % 300.09/43.17 % (3616652)Instruction limit reached! % 300.09/43.17 % (3616652)------------------------------ % 300.09/43.17 % (3616652)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.09/43.17 % (3616652)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.09/43.17 % (3616652)CaDiCaL version: 2.1.3 % 300.09/43.17 % (3616652)Termination reason: Instruction limit % 300.09/43.17 % (3616652)Termination phase: Saturation % 300.09/43.17 % (3616652)Time elapsed: 0.166 s % 300.09/43.17 % (3616652)Peak memory usage: 136 MB % 300.09/43.17 % (3616652)Instructions burned: 672 (million) % 300.09/43.17 % (3616655)lrs+1010_1_to=kbo:sil=64000:sas=cadical:si=on:sos=on:bce=on:random_seed=2998620072:i=718:rtra=on:gtg=exists_top:ss=axioms_2603 on theBenchmark for (2603ds/718Mi) % 300.09/43.17 % (3616655)Refutation not found, incomplete strategy % 300.09/43.17 % (3616655)------------------------------ % 300.09/43.17 % (3616655)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.09/43.17 % (3616655)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.09/43.17 % (3616655)CaDiCaL version: 2.1.3 % 300.09/43.17 % (3616655)Termination reason: Refutation not found, incomplete strategy % 300.09/43.17 % (3616655)Time elapsed: 0.019 s % 300.09/43.17 % (3616655)Peak memory usage: 88 MB % 300.09/43.17 % (3616655)Instructions burned: 97 (million) % 300.09/43.17 % (3616651)Instruction limit reached! % 300.09/43.17 % (3616651)------------------------------ % 300.09/43.17 % (3616651)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.09/43.17 % (3616651)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.09/43.17 % (3616651)CaDiCaL version: 2.1.3 % 300.09/43.17 % (3616651)Termination reason: Instruction limit % 300.09/43.17 % (3616651)Termination phase: Saturation % 300.09/43.17 % (3616651)Time elapsed: 0.374 s % 300.09/43.17 % (3616651)Peak memory usage: 90 MB % 300.09/43.17 % (3616651)Instructions burned: 1026 (million) % 300.09/43.17 % (3616655)------------------------------ % 300.09/43.17 % (3616655)------------------------------ % 300.09/43.17 % (3616657)dis+1010_1_to=lpo:sil=128000:thi=all:fde=unused:si=on:sp=reverse_arity:tha=off:random_seed=72131208:i=682:gtgl=2:rtra=on:gtg=exists_sym:ev=force:fsd=on:fsdmm=1_2602 on theBenchmark for (2602ds/682Mi) % 300.09/43.17 % (3616658)lrs-2_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_max:tha=off:random_seed=2094673774:st=1.5:i=522:sd=1:kws=precedence:rtra=on:ss=axioms_2601 on theBenchmark for (2601ds/522Mi) % 300.09/43.17 % (3616658)Refutation not found, incomplete strategy % 300.09/43.17 % (3616658)------------------------------ % 300.09/43.17 % (3616658)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.09/43.17 % (3616658)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.09/43.17 % (3616658)CaDiCaL version: 2.1.3 % 300.09/43.17 % (36166 % 300.09/43.18 Terminated %------------------------------------------------------------------------------