%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWW086_1 : TPTP v9.3.1. Released v5.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/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:29:23 PM UTC 2026 % Result : Timeout 287.76s 41.08s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWW086_1 : TPTP v9.3.1. Released v5.0.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.08/0.18 % Computer : n017.cluster.edu % 0.08/0.18 % Model : x86_64 x86_64 % 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.18 % Memory : 8046.5625MB % 0.08/0.18 % OS : Linux 6.8.0-71-generic % 0.08/0.19 % CPULimit : 300 % 0.08/0.19 % WCLimit : 300 % 0.08/0.19 % DateTime : Mon Sep 28 13:06:51 UTC 2026 % 0.08/0.19 % CPUTime : % 0.08/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.08/0.22 Running first-order theorem proving % 0.08/0.22 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 2.84/0.94 % (3539190)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule. % 2.84/0.94 % (3539201)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=2144889473:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi) % 2.84/0.94 % (3539201)Instruction limit reached! % 2.84/0.94 % (3539201)------------------------------ % 2.84/0.94 % (3539201)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 2.84/0.94 % (3539201)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.84/0.94 % (3539201)CaDiCaL version: 2.1.3 % 2.84/0.94 % (3539201)Termination reason: Instruction limit % 2.84/0.94 % (3539201)Termination phase: Preprocessing 1 % 2.84/0.94 % (3539201)Time elapsed: 0.009 s % 2.84/0.94 % (3539201)Peak memory usage: 87 MB % 2.84/0.94 % (3539201)Instructions burned: 37 (million) % 2.84/0.94 % (3539199)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=3237930152:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi) % 2.84/0.94 % (3539195)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=531873928:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi) % 2.84/0.94 % (3539197)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=104194982:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi) % 2.84/0.94 % (3539200)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=3682798094:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi) % 2.84/0.94 % (3539198)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=3311239762:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi) % 2.84/0.94 % (3539196)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=3609272944:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi) % 2.84/0.94 % (3539199)Instruction limit reached! % 2.84/0.94 % (3539199)------------------------------ % 2.84/0.94 % (3539199)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 2.84/0.94 % (3539199)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.84/0.94 % (3539199)CaDiCaL version: 2.1.3 % 2.84/0.94 % (3539199)Termination reason: Instruction limit % 2.84/0.94 % (3539199)Termination phase: shuffling % 2.84/0.94 % (3539199)Time elapsed: 0.003 s % 2.84/0.94 % (3539199)Peak memory usage: 85 MB % 2.84/0.94 % (3539199)Instructions burned: 4 (million) % 2.84/0.94 % (3539198)Instruction limit reached! % 2.84/0.94 % (3539198)------------------------------ % 2.84/0.94 % (3539198)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 2.84/0.94 % (3539198)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.84/0.94 % (3539198)CaDiCaL version: 2.1.3 % 2.84/0.94 % (3539198)Termination reason: Instruction limit % 2.84/0.94 % (3539198)Termination phase: shuffling % 2.84/0.94 % (3539198)Time elapsed: 0.004 s % 2.84/0.94 % (3539198)Peak memory usage: 85 MB % 2.84/0.94 % (3539198)Instructions burned: 7 (million) % 2.84/0.94 % (3539195)Instruction limit reached! % 2.84/0.94 % (3539195)------------------------------ % 2.84/0.94 % (3539195)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 2.84/0.94 % (3539195)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.84/0.94 % (3539195)CaDiCaL version: 2.1.3 % 2.84/0.94 % (3539195)Termination reason: Instruction limit % 2.84/0.94 % (3539195)Termination phase: Property scanning % 2.84/0.94 % (3539195)Time elapsed: 0.007 s % 2.84/0.94 % (3539195)Peak memory usage: 85 MB % 2.84/0.94 % (3539195)Instructions burned: 14 (million) % 2.84/0.94 % (3539200)Instruction limit reached! % 2.84/0.94 % (3539200)------------------------------ % 2.84/0.94 % (3539200)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 2.84/0.94 % (3539200)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.84/0.94 % (3539200)CaDiCaL version: 2.1.3 % 2.84/0.94 % (3539200)Termination reason: Instruction limit % 2.84/0.94 % (3539200)Termination phase: Preprocessing 2 % 2.84/0.94 % (3539200)Time elapsed: 0.024 s % 2.84/0.94 % (3539200)Peak memory usage: 88 MB % 2.84/0.94 % (3539200)Instructions burned: 46 (million) % 2.84/0.94 % (3539203)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=466911706:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2998 on theBenchmark for (2998ds/14Mi) % 2.84/0.94 % (3539203)Instruction limit reached! % 2.84/0.94 % (3539203)------------------------------ % 4.19/1.09 % (3539203)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.19/1.09 % (3539203)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.19/1.09 % (3539203)CaDiCaL version: 2.1.3 % 4.19/1.09 % (3539203)Termination reason: Instruction limit % 4.19/1.09 % (3539203)Termination phase: Property scanning % 4.19/1.09 % (3539203)Time elapsed: 0.004 s % 4.19/1.09 % (3539203)Peak memory usage: 86 MB % 4.19/1.09 % (3539203)Instructions burned: 15 (million) % 4.19/1.09 % (3539197)Instruction limit reached! % 4.19/1.09 % (3539197)------------------------------ % 4.19/1.09 % (3539197)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.19/1.09 % (3539197)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.19/1.09 % (3539197)CaDiCaL version: 2.1.3 % 4.19/1.09 % (3539197)Termination reason: Instruction limit % 4.19/1.09 % (3539197)Termination phase: Saturation % 4.19/1.09 % (3539197)Time elapsed: 0.131 s % 4.19/1.09 % (3539197)Peak memory usage: 122 MB % 4.19/1.09 % (3539197)Instructions burned: 202 (million) % 4.19/1.09 % (3539212)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=4002140625:i=24:canc=force:rtra=on_2998 on theBenchmark for (2998ds/24Mi) % 4.19/1.09 % (3539211)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=868343274:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/16Mi) % 4.19/1.09 % (3539210)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=276125640:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2998 on theBenchmark for (2998ds/29Mi) % 4.19/1.09 % (3539211)Instruction limit reached! % 4.19/1.09 % (3539211)------------------------------ % 4.19/1.09 % (3539211)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.19/1.09 % (3539211)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.19/1.09 % (3539211)CaDiCaL version: 2.1.3 % 4.19/1.09 % (3539211)Termination reason: Instruction limit % 4.19/1.09 % (3539211)Termination phase: Property scanning % 4.19/1.09 % (3539211)Time elapsed: 0.008 s % 4.19/1.09 % (3539211)Peak memory usage: 85 MB % 4.19/1.09 % (3539211)Instructions burned: 18 (million) % 4.19/1.09 % (3539212)Instruction limit reached! % 4.19/1.09 % (3539212)------------------------------ % 4.19/1.09 % (3539212)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.19/1.09 % (3539212)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.19/1.09 % (3539212)CaDiCaL version: 2.1.3 % 4.19/1.09 % (3539212)Termination reason: Instruction limit % 4.19/1.09 % (3539212)Termination phase: Property scanning % 4.19/1.09 % (3539212)Time elapsed: 0.012 s % 4.19/1.09 % (3539212)Peak memory usage: 86 MB % 4.19/1.09 % (3539212)Instructions burned: 26 (million) % 4.19/1.09 % (3539210)Instruction limit reached! % 4.19/1.09 % (3539210)------------------------------ % 4.19/1.09 % (3539210)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.19/1.09 % (3539210)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.19/1.09 % (3539210)CaDiCaL version: 2.1.3 % 4.19/1.09 % (3539210)Termination reason: Instruction limit % 4.19/1.09 % (3539210)Termination phase: Property scanning % 4.19/1.09 % (3539210)Time elapsed: 0.013 s % 4.19/1.09 % (3539210)Peak memory usage: 86 MB % 4.19/1.09 % (3539210)Instructions burned: 30 (million) % 4.19/1.09 % (3539213)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=350204054:i=27:canc=cautious:fsr=off:rtra=on_2997 on theBenchmark for (2997ds/27Mi) % 4.19/1.09 % (3539213)Instruction limit reached! % 4.19/1.09 % (3539213)------------------------------ % 4.19/1.09 % (3539213)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.19/1.09 % (3539213)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.19/1.09 % (3539213)CaDiCaL version: 2.1.3 % 4.19/1.09 % (3539213)Termination reason: Instruction limit % 4.19/1.09 % (3539213)Termination phase: Property scanning % 4.19/1.09 % (3539213)Time elapsed: 0.013 s % 4.19/1.09 % (3539213)Peak memory usage: 86 MB % 4.19/1.09 % (3539213)Instructions burned: 27 (million) % 4.19/1.09 % (3539215)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=2525078193:i=85:gtgl=4:rtra=on:gtg=exists_sym_2997 on theBenchmark for (2997ds/85Mi) % 4.19/1.09 % (3539196)Instruction limit reached! % 4.19/1.09 % (3539196)------------------------------ % 5.10/1.25 % (3539196)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.10/1.25 % (3539196)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.10/1.25 % (3539196)CaDiCaL version: 2.1.3 % 5.10/1.25 % (3539196)Termination reason: Instruction limit % 5.10/1.25 % (3539196)Termination phase: Saturation % 5.10/1.25 % (3539196)Time elapsed: 0.202 s % 5.10/1.25 % (3539196)Peak memory usage: 122 MB % 5.10/1.25 % (3539196)Instructions burned: 307 (million) % 5.10/1.25 % (3539215)Instruction limit reached! % 5.10/1.25 % (3539215)------------------------------ % 5.10/1.25 % (3539215)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.10/1.25 % (3539215)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.10/1.25 % (3539215)CaDiCaL version: 2.1.3 % 5.10/1.25 % (3539215)Termination reason: Instruction limit % 5.10/1.25 % (3539215)Termination phase: Unused predicate definition removal % 5.10/1.25 % (3539215)Time elapsed: 0.022 s % 5.10/1.25 % (3539215)Peak memory usage: 88 MB % 5.10/1.25 % (3539215)Instructions burned: 86 (million) % 5.10/1.25 % (3539217)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=2755463102:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2996 on theBenchmark for (2996ds/2Mi) % 5.10/1.25 % (3539217)Instruction limit reached! % 5.10/1.25 % (3539217)------------------------------ % 5.10/1.25 % (3539217)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.10/1.25 % (3539217)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.10/1.25 % (3539217)CaDiCaL version: 2.1.3 % 5.10/1.25 % (3539217)Termination reason: Instruction limit % 5.10/1.25 % (3539217)Termination phase: shuffling % 5.10/1.25 % (3539217)Time elapsed: 0.003 s % 5.10/1.25 % (3539217)Peak memory usage: 85 MB % 5.10/1.25 % (3539217)Instructions burned: 4 (million) % 5.10/1.25 % (3539222)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=1843425879:i=4:ep=RST:ins=2:rtra=on_2996 on theBenchmark for (2996ds/4Mi) % 5.10/1.25 % (3539223)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=1818783161:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2996 on theBenchmark for (2996ds/66Mi) % 5.10/1.25 % (3539221)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=1262644866:i=181:rtra=on:ss=axioms:ev=cautious_2996 on theBenchmark for (2996ds/181Mi) % 5.10/1.25 % (3539222)Instruction limit reached! % 5.10/1.25 % (3539222)------------------------------ % 5.10/1.25 % (3539222)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.10/1.25 % (3539222)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.10/1.25 % (3539222)CaDiCaL version: 2.1.3 % 5.10/1.25 % (3539222)Termination reason: Instruction limit % 5.10/1.25 % (3539222)Termination phase: shuffling % 5.10/1.25 % (3539222)Time elapsed: 0.003 s % 5.10/1.25 % (3539222)Peak memory usage: 85 MB % 5.10/1.25 % (3539222)Instructions burned: 4 (million) % 5.10/1.25 % (3539225)lrs+10_1_thi=all:si=on:fd=off:random_seed=4286995277:i=53:rtra=on:gtg=all_2996 on theBenchmark for (2996ds/53Mi) % 5.10/1.25 % (3539228)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=4266590435:st=3:i=2:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/2Mi) % 5.10/1.25 % (3539228)Instruction limit reached! % 5.10/1.25 % (3539228)------------------------------ % 5.10/1.25 % (3539228)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.10/1.25 % (3539228)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.10/1.25 % (3539228)CaDiCaL version: 2.1.3 % 5.10/1.25 % (3539228)Termination reason: Instruction limit % 5.10/1.25 % (3539228)Termination phase: shuffling % 5.10/1.25 % (3539228)Time elapsed: 0.002 s % 5.10/1.25 % (3539228)Peak memory usage: 85 MB % 5.10/1.25 % (3539228)Instructions burned: 5 (million) % 5.10/1.25 % (3539223)Instruction limit reached! % 5.10/1.25 % (3539223)------------------------------ % 5.10/1.25 % (3539223)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.10/1.25 % (3539223)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.10/1.25 % (3539223)CaDiCaL version: 2.1.3 % 5.10/1.25 % (3539223)Termination reason: Instruction limit % 5.10/1.25 % (3539223)Termination phase: Preprocessing 2 % 5.10/1.25 % (3539223)Time elapsed: 0.035 s % 5.10/1.25 % (3539223)Peak memory usage: 89 MB % 5.10/1.25 % (3539223)Instructions burned: 67 (million) % 5.10/1.25 % (3539225)Instruction limit reached! % 6.10/1.44 % (3539225)------------------------------ % 6.10/1.44 % (3539225)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.10/1.44 % (3539225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.10/1.44 % (3539225)CaDiCaL version: 2.1.3 % 6.10/1.44 % (3539225)Termination reason: Instruction limit % 6.10/1.44 % (3539225)Termination phase: Property scanning % 6.10/1.44 % (3539225)Time elapsed: 0.023 s % 6.10/1.44 % (3539225)Peak memory usage: 86 MB % 6.10/1.44 % (3539225)Instructions burned: 54 (million) % 6.10/1.44 % (3539227)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=1035287560:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2996 on theBenchmark for (2996ds/8Mi) % 6.10/1.44 % (3539227)Instruction limit reached! % 6.10/1.44 % (3539227)------------------------------ % 6.10/1.44 % (3539227)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.10/1.44 % (3539227)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.10/1.44 % (3539227)CaDiCaL version: 2.1.3 % 6.10/1.44 % (3539227)Termination reason: Instruction limit % 6.10/1.44 % (3539227)Termination phase: Property scanning % 6.10/1.44 % (3539227)Time elapsed: 0.005 s % 6.10/1.44 % (3539227)Peak memory usage: 85 MB % 6.10/1.44 % (3539227)Instructions burned: 10 (million) % 6.10/1.44 % (3539221)Instruction limit reached! % 6.10/1.44 % (3539221)------------------------------ % 6.10/1.44 % (3539221)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.10/1.44 % (3539221)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.10/1.44 % (3539221)CaDiCaL version: 2.1.3 % 6.10/1.44 % (3539221)Termination reason: Instruction limit % 6.10/1.44 % (3539221)Termination phase: Saturation % 6.10/1.44 % (3539221)Time elapsed: 0.098 s % 6.10/1.44 % (3539221)Peak memory usage: 95 MB % 6.10/1.44 % (3539221)Instructions burned: 181 (million) % 6.10/1.44 % (3539237)dis+10_1_si=on:random_seed=1213717202:i=10:ep=R:rtra=on_2994 on theBenchmark for (2994ds/10Mi) % 6.10/1.44 % (3539230)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=2423692175:i=2:doe=on:canc=force:asg=cautious:rtra=on_2995 on theBenchmark for (2995ds/2Mi) % 6.10/1.44 % (3539237)Instruction limit reached! % 6.10/1.44 % (3539237)------------------------------ % 6.10/1.44 % (3539237)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.10/1.44 % (3539237)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.10/1.44 % (3539237)CaDiCaL version: 2.1.3 % 6.10/1.44 % (3539237)Termination reason: Instruction limit % 6.10/1.44 % (3539237)Termination phase: Property scanning % 6.10/1.44 % (3539237)Time elapsed: 0.004 s % 6.10/1.44 % (3539230)Instruction limit reached! % 6.10/1.44 % (3539230)------------------------------ % 6.10/1.44 % (3539230)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.10/1.44 % (3539237)Peak memory usage: 86 MB % 6.10/1.44 % (3539237)Instructions burned: 14 (million) % 6.10/1.44 % (3539230)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.10/1.44 % (3539230)CaDiCaL version: 2.1.3 % 6.10/1.44 % (3539230)Termination reason: Instruction limit % 6.10/1.44 % (3539230)Termination phase: shuffling % 6.10/1.44 % (3539230)Time elapsed: 0.003 s % 6.10/1.44 % (3539230)Peak memory usage: 85 MB % 6.10/1.44 % (3539230)Instructions burned: 4 (million) % 6.10/1.44 % (3539234)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=1454047814:i=127:doe=on:rtra=on_2995 on theBenchmark for (2995ds/127Mi) % 6.10/1.44 % (3539238)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=1635306895:i=26:canc=cautious:av=off:rtra=on_2994 on theBenchmark for (2994ds/26Mi) % 6.10/1.44 % (3539240)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=712961427: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_2994 on theBenchmark for (2994ds/35Mi) % 6.10/1.44 % (3539238)Instruction limit reached! % 6.10/1.44 % (3539238)------------------------------ % 6.10/1.44 % (3539238)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.10/1.44 % (3539238)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.10/1.44 % (3539238)CaDiCaL version: 2.1.3 % 6.10/1.44 % (3539238)Termination reason: Instruction limit % 6.10/1.44 % (3539238)Termination phase: Property scanning % 6.10/1.44 % (3539238)Time elapsed: 0.013 s % 7.52/1.68 % (3539238)Peak memory usage: 86 MB % 7.52/1.68 % (3539238)Instructions burned: 27 (million) % 7.52/1.68 % (3539241)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=2679767558:i=2:fsr=off:rtra=on:inst=on_2994 on theBenchmark for (2994ds/2Mi) % 7.52/1.68 % (3539240)Instruction limit reached! % 7.52/1.68 % (3539240)------------------------------ % 7.52/1.68 % (3539240)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.52/1.68 % (3539240)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.52/1.68 % (3539240)CaDiCaL version: 2.1.3 % 7.52/1.68 % (3539240)Termination reason: Instruction limit % 7.52/1.68 % (3539240)Termination phase: SInE selection % 7.52/1.68 % (3539240)Time elapsed: 0.015 s % 7.52/1.68 % (3539240)Peak memory usage: 86 MB % 7.52/1.68 % (3539240)Instructions burned: 35 (million) % 7.52/1.68 % (3539241)Instruction limit reached! % 7.52/1.68 % (3539241)------------------------------ % 7.52/1.68 % (3539241)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.52/1.68 % (3539241)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.52/1.68 % (3539241)CaDiCaL version: 2.1.3 % 7.52/1.68 % (3539241)Termination reason: Instruction limit % 7.52/1.68 % (3539241)Termination phase: shuffling % 7.52/1.68 % (3539241)Time elapsed: 0.003 s % 7.52/1.68 % (3539241)Peak memory usage: 85 MB % 7.52/1.68 % (3539241)Instructions burned: 4 (million) % 7.52/1.68 % (3539234)Instruction limit reached! % 7.52/1.68 % (3539234)------------------------------ % 7.52/1.68 % (3539234)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.52/1.68 % (3539234)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.52/1.68 % (3539234)CaDiCaL version: 2.1.3 % 7.52/1.68 % (3539234)Termination reason: Instruction limit % 7.52/1.68 % (3539234)Termination phase: Saturation % 7.52/1.68 % (3539234)Time elapsed: 0.091 s % 7.52/1.68 % (3539234)Peak memory usage: 118 MB % 7.52/1.68 % (3539234)Instructions burned: 128 (million) % 7.52/1.68 % (3539242)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=3703259317:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2994 on theBenchmark for (2994ds/8Mi) % 7.52/1.68 % (3539242)Instruction limit reached! % 7.52/1.68 % (3539242)------------------------------ % 7.52/1.69 % (3539242)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.52/1.69 % (3539242)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.52/1.69 % (3539242)CaDiCaL version: 2.1.3 % 7.52/1.69 % (3539242)Termination reason: Instruction limit % 7.52/1.69 % (3539242)Termination phase: Property scanning % 7.52/1.69 % (3539242)Time elapsed: 0.005 s % 7.52/1.69 % (3539242)Peak memory usage: 85 MB % 7.52/1.69 % (3539242)Instructions burned: 8 (million) % 7.52/1.69 % (3539245)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=501124784:i=370:ep=RS:fsr=off:rtra=on_2993 on theBenchmark for (2993ds/370Mi) % 7.52/1.69 % (3539246)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=418151766:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2993 on theBenchmark for (2993ds/13Mi) % 7.52/1.69 % (3539246)Instruction limit reached! % 7.52/1.69 % (3539246)------------------------------ % 7.52/1.69 % (3539246)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.52/1.69 % (3539246)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.52/1.69 % (3539246)CaDiCaL version: 2.1.3 % 7.52/1.69 % (3539246)Termination reason: Instruction limit % 7.52/1.69 % (3539246)Termination phase: Property scanning % 7.52/1.69 % (3539246)Time elapsed: 0.006 s % 7.52/1.69 % (3539246)Peak memory usage: 85 MB % 7.52/1.69 % (3539246)Instructions burned: 13 (million) % 7.52/1.69 % (3539253)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=2571133845:i=71:rtra=on:gtg=exists_top_2993 on theBenchmark for (2993ds/71Mi) % 7.52/1.69 % (3539252)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=4286637407:i=10:rtra=on_2993 on theBenchmark for (2993ds/10Mi) % 7.52/1.69 % (3539250)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=431919157:i=226:rtra=on:gtg=position:ss=axioms_2993 on theBenchmark for (2993ds/226Mi) % 7.52/1.69 % (3539252)Instruction limit reached! % 7.52/1.69 % (3539252)------------------------------ % 7.52/1.69 % (3539252)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.52/1.69 % (3539252)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.77/1.90 % (3539252)CaDiCaL version: 2.1.3 % 9.77/1.90 % (3539252)Termination reason: Instruction limit % 9.77/1.90 % (3539252)Termination phase: Property scanning % 9.77/1.90 % (3539252)Time elapsed: 0.006 s % 9.77/1.90 % (3539252)Peak memory usage: 85 MB % 9.77/1.90 % (3539252)Instructions burned: 12 (million) % 9.77/1.90 % (3539245)Refutation not found, incomplete strategy % 9.77/1.90 % (3539245)------------------------------ % 9.77/1.90 % (3539245)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.77/1.90 % (3539245)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.77/1.90 % (3539245)CaDiCaL version: 2.1.3 % 9.77/1.90 % (3539245)Termination reason: Refutation not found, incomplete strategy % 9.77/1.90 % (3539245)Time elapsed: 0.101 s % 9.77/1.90 % (3539245)Peak memory usage: 96 MB % 9.77/1.90 % (3539245)Instructions burned: 187 (million) % 9.77/1.90 % (3539253)Instruction limit reached! % 9.77/1.90 % (3539253)------------------------------ % 9.77/1.90 % (3539253)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.77/1.90 % (3539253)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.77/1.90 % (3539253)CaDiCaL version: 2.1.3 % 9.77/1.90 % (3539253)Termination reason: Instruction limit % 9.77/1.90 % (3539253)Termination phase: shuffling % 9.77/1.90 % (3539253)Time elapsed: 0.036 s % 9.77/1.90 % (3539253)Peak memory usage: 89 MB % 9.77/1.90 % (3539253)Instructions burned: 72 (million) % 9.77/1.90 % (3539255)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=3950248253:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2992 on theBenchmark for (2992ds/75Mi) % 9.77/1.90 % (3539256)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=3821981379:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2992 on theBenchmark for (2992ds/294Mi) % 9.77/1.90 % (3539255)Instruction limit reached! % 9.77/1.90 % (3539255)------------------------------ % 9.77/1.90 % (3539255)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.77/1.90 % (3539255)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.77/1.90 % (3539255)CaDiCaL version: 2.1.3 % 9.77/1.90 % (3539255)Termination reason: Instruction limit % 9.77/1.90 % (3539255)Termination phase: Preprocessing 3 % 9.77/1.90 % (3539255)Time elapsed: 0.039 s % 9.77/1.90 % (3539255)Peak memory usage: 90 MB % 9.77/1.90 % (3539255)Instructions burned: 76 (million) % 9.77/1.90 % (3539259)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=1196207155:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2992 on theBenchmark for (2992ds/130Mi) % 9.77/1.90 % (3539250)Instruction limit reached! % 9.77/1.90 % (3539250)------------------------------ % 9.77/1.90 % (3539250)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.77/1.90 % (3539250)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.77/1.90 % (3539250)CaDiCaL version: 2.1.3 % 9.77/1.90 % (3539250)Termination reason: Instruction limit % 9.77/1.90 % (3539250)Termination phase: Saturation % 9.77/1.90 % (3539250)Time elapsed: 0.131 s % 9.77/1.90 % (3539250)Peak memory usage: 118 MB % 9.77/1.90 % (3539250)Instructions burned: 227 (million) % 9.77/1.90 % (3539259)Instruction limit reached! % 9.77/1.90 % (3539259)------------------------------ % 9.77/1.90 % (3539259)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.77/1.90 % (3539259)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.77/1.90 % (3539259)CaDiCaL version: 2.1.3 % 9.77/1.90 % (3539259)Termination reason: Instruction limit % 9.77/1.90 % (3539259)Termination phase: Twee Goal Transformation % 9.77/1.90 % (3539259)Time elapsed: 0.063 s % 9.77/1.90 % (3539259)Peak memory usage: 91 MB % 9.77/1.90 % (3539259)Instructions burned: 131 (million) % 9.77/1.90 % (3539263)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=558507994:i=131:rtra=on_2991 on theBenchmark for (2991ds/131Mi) % 9.77/1.90 % (3539265)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=2678994864:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2991 on theBenchmark for (2991ds/40Mi) % 9.77/1.90 % (3539265)Instruction limit reached! % 9.77/1.90 % (3539265)------------------------------ % 9.77/1.90 % (3539265)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.84/2.19 % (3539265)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.84/2.19 % (3539265)CaDiCaL version: 2.1.3 % 11.84/2.19 % (3539265)Termination reason: Instruction limit % 11.84/2.19 % (3539265)Termination phase: shuffling % 11.84/2.19 % (3539265)Time elapsed: 0.017 s % 11.84/2.19 % (3539265)Peak memory usage: 86 MB % 11.84/2.19 % (3539265)Instructions burned: 40 (million) % 11.84/2.19 % (3539256)Instruction limit reached! % 11.84/2.19 % (3539256)------------------------------ % 11.84/2.19 % (3539256)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.84/2.19 % (3539256)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.84/2.19 % (3539256)CaDiCaL version: 2.1.3 % 11.84/2.19 % (3539256)Termination reason: Instruction limit % 11.84/2.19 % (3539256)Termination phase: Saturation % 11.84/2.19 % (3539256)Time elapsed: 0.155 s % 11.84/2.19 % (3539256)Peak memory usage: 95 MB % 11.84/2.19 % (3539256)Instructions burned: 296 (million) % 11.84/2.19 % (3539268)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=2895627055:i=307:rtra=on:gtg=exists_top_2990 on theBenchmark for (2990ds/307Mi) % 11.84/2.19 % (3539270)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=2438091093:i=131:canc=cautious:fsr=off:rtra=on_2990 on theBenchmark for (2990ds/131Mi) % 11.84/2.19 % (3539245)------------------------------ % 11.84/2.19 % (3539245)------------------------------ % 11.84/2.19 % (3539263)Instruction limit reached! % 11.84/2.19 % (3539263)------------------------------ % 11.84/2.19 % (3539263)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.84/2.19 % (3539263)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.84/2.19 % (3539263)CaDiCaL version: 2.1.3 % 11.84/2.19 % (3539263)Termination reason: Instruction limit % 11.84/2.19 % (3539263)Termination phase: Saturation % 11.84/2.19 % (3539263)Time elapsed: 0.113 s % 11.84/2.19 % (3539263)Peak memory usage: 134 MB % 11.84/2.19 % (3539263)Instructions burned: 131 (million) % 11.84/2.19 % (3539269)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=225735013:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2990 on theBenchmark for (2990ds/598Mi) % 11.84/2.19 % (3539270)Instruction limit reached! % 11.84/2.19 % (3539270)------------------------------ % 11.84/2.19 % (3539270)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.84/2.19 % (3539270)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.84/2.19 % (3539270)CaDiCaL version: 2.1.3 % 11.84/2.19 % (3539270)Termination reason: Instruction limit % 11.84/2.19 % (3539270)Termination phase: Saturation % 11.84/2.19 % (3539270)Time elapsed: 0.051 s % 11.84/2.19 % (3539270)Peak memory usage: 117 MB % 11.84/2.19 % (3539270)Instructions burned: 133 (million) % 11.84/2.19 % (3539273)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=760960178:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2989 on theBenchmark for (2989ds/259Mi) % 11.84/2.19 % (3539268)Instruction limit reached! % 11.84/2.19 % (3539268)------------------------------ % 11.84/2.19 % (3539268)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.84/2.19 % (3539268)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.84/2.19 % (3539268)CaDiCaL version: 2.1.3 % 11.84/2.19 % (3539268)Termination reason: Instruction limit % 11.84/2.19 % (3539268)Termination phase: Saturation % 11.84/2.19 % (3539268)Time elapsed: 0.153 s % 11.84/2.19 % (3539268)Peak memory usage: 95 MB % 11.84/2.19 % (3539268)Instructions burned: 309 (million) % 11.84/2.19 % (3539275)dis+10_1_si=on:random_seed=3465201719:s2a=on:i=1000:rtra=on:gtg=exists_all_2989 on theBenchmark for (2989ds/1000Mi) % 11.84/2.19 % (3539278)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=1940463344:i=141:doe=on:rtra=on_2988 on theBenchmark for (2988ds/141Mi) % 11.84/2.19 % (3539277)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=974405837:i=383:fsr=off:rtra=on:ev=force_2988 on theBenchmark for (2988ds/383Mi) % 11.84/2.19 % (3539280)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=2595956994:i=65:nm=16:rtra=on_2988 on theBenchmark for (2988ds/65Mi) % 11.84/2.19 % (3539280)Instruction limit reached! % 11.84/2.19 % (3539280)------------------------------ % 11.84/2.19 % (3539280)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.84/2.19 % (3539280)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.15/2.50 % (3539280)CaDiCaL version: 2.1.3 % 13.15/2.50 % (3539280)Termination reason: Instruction limit % 13.15/2.50 % (3539280)Termination phase: Preprocessing 3 % 13.15/2.50 % (3539280)Time elapsed: 0.019 s % 13.15/2.50 % (3539280)Peak memory usage: 90 MB % 13.15/2.50 % (3539280)Instructions burned: 65 (million) % 13.15/2.50 % (3539278)Instruction limit reached! % 13.15/2.50 % (3539278)------------------------------ % 13.15/2.50 % (3539278)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.15/2.50 % (3539278)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.15/2.50 % (3539278)CaDiCaL version: 2.1.3 % 13.15/2.50 % (3539278)Termination reason: Instruction limit % 13.15/2.50 % (3539278)Termination phase: Saturation % 13.15/2.50 % (3539278)Time elapsed: 0.071 s % 13.15/2.50 % (3539278)Peak memory usage: 93 MB % 13.15/2.50 % (3539278)Instructions burned: 141 (million) % 13.15/2.50 % (3539283)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=3687967553:i=121:nm=16:rtra=on_2987 on theBenchmark for (2987ds/121Mi) % 13.15/2.50 % (3539273)Instruction limit reached! % 13.15/2.50 % (3539273)------------------------------ % 13.15/2.50 % (3539273)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.15/2.50 % (3539273)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.15/2.50 % (3539273)CaDiCaL version: 2.1.3 % 13.15/2.50 % (3539273)Termination reason: Instruction limit % 13.15/2.50 % (3539273)Termination phase: Saturation % 13.15/2.50 % (3539273)Time elapsed: 0.174 s % 13.15/2.50 % (3539273)Peak memory usage: 123 MB % 13.15/2.50 % (3539273)Instructions burned: 260 (million) % 13.15/2.50 % (3539287)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=1745894135:s2a=on:i=128:s2at=5:ins=3:rtra=on_2987 on theBenchmark for (2987ds/128Mi) % 13.15/2.50 % (3539283)Instruction limit reached! % 13.15/2.50 % (3539283)------------------------------ % 13.15/2.50 % (3539283)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.15/2.50 % (3539283)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.15/2.50 % (3539283)CaDiCaL version: 2.1.3 % 13.15/2.50 % (3539283)Termination reason: Instruction limit % 13.15/2.50 % (3539283)Termination phase: Twee Goal Transformation % 13.15/2.50 % (3539283)Time elapsed: 0.061 s % 13.15/2.50 % (3539283)Peak memory usage: 91 MB % 13.15/2.50 % (3539283)Instructions burned: 122 (million) % 13.15/2.50 % (3539287)Instruction limit reached! % 13.15/2.50 % (3539287)------------------------------ % 13.15/2.50 % (3539287)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.15/2.50 % (3539287)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.15/2.50 % (3539287)CaDiCaL version: 2.1.3 % 13.15/2.50 % (3539287)Termination reason: Instruction limit % 13.15/2.50 % (3539287)Termination phase: Saturation % 13.15/2.50 % (3539287)Time elapsed: 0.049 s % 13.15/2.50 % (3539287)Peak memory usage: 117 MB % 13.15/2.50 % (3539287)Instructions burned: 131 (million) % 13.15/2.50 % (3539277)Instruction limit reached! % 13.15/2.50 % (3539277)------------------------------ % 13.15/2.50 % (3539277)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.15/2.50 % (3539277)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.15/2.50 % (3539277)CaDiCaL version: 2.1.3 % 13.15/2.50 % (3539277)Termination reason: Instruction limit % 13.15/2.50 % (3539277)Termination phase: Saturation % 13.15/2.50 % (3539277)Time elapsed: 0.203 s % 13.15/2.50 % (3539277)Peak memory usage: 106 MB % 13.15/2.50 % (3539277)Instructions burned: 384 (million) % 13.15/2.50 % (3539269)Instruction limit reached! % 13.15/2.50 % (3539269)------------------------------ % 13.15/2.50 % (3539269)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.15/2.50 % (3539269)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.15/2.50 % (3539269)CaDiCaL version: 2.1.3 % 13.15/2.50 % (3539269)Termination reason: Instruction limit % 13.15/2.50 % (3539269)Termination phase: Saturation % 13.15/2.50 % (3539269)Time elapsed: 0.337 s % 13.15/2.50 % (3539269)Peak memory usage: 136 MB % 13.15/2.50 % (3539269)Instructions burned: 600 (million) % 13.15/2.50 % (3539288)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=2454435684:i=39:ins=3:rtra=on_2986 on theBenchmark for (2986ds/39Mi) % 13.15/2.50 % (3539288)Instruction limit reached! % 13.15/2.50 % (3539288)------------------------------ % 13.15/2.50 % (3539288)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.23/2.76 % (3539288)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.23/2.76 % (3539288)CaDiCaL version: 2.1.3 % 15.23/2.76 % (3539288)Termination reason: Instruction limit % 15.23/2.76 % (3539288)Termination phase: Preprocessing 1 % 15.23/2.76 % (3539288)Time elapsed: 0.019 s % 15.23/2.76 % (3539288)Peak memory usage: 87 MB % 15.23/2.76 % (3539288)Instructions burned: 40 (million) % 15.23/2.76 % (3539290)dis+1010_1_to=kbo:si=on:random_seed=3630487978:i=175:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2986 on theBenchmark for (2986ds/175Mi) % 15.23/2.76 % (3539293)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=1894246438:s2a=on:i=483:doe=on:nm=32:rtra=on_2985 on theBenchmark for (2985ds/483Mi) % 15.23/2.76 % (3539292)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=1588144382:i=329:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2985 on theBenchmark for (2985ds/329Mi) % 15.23/2.76 % (3539290)Instruction limit reached! % 15.23/2.76 % (3539290)------------------------------ % 15.23/2.76 % (3539290)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.23/2.76 % (3539290)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.23/2.76 % (3539290)CaDiCaL version: 2.1.3 % 15.23/2.76 % (3539290)Termination reason: Instruction limit % 15.23/2.76 % (3539290)Termination phase: Saturation % 15.23/2.76 % (3539290)Time elapsed: 0.089 s % 15.23/2.76 % (3539290)Peak memory usage: 95 MB % 15.23/2.76 % (3539290)Instructions burned: 175 (million) % 15.23/2.76 % (3539294)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=3489939642:thitd=on:i=215:nm=0:rtra=on:ev=force_2985 on theBenchmark for (2985ds/215Mi) % 15.23/2.76 % (3539295)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=900058715:i=349:rtra=on_2985 on theBenchmark for (2985ds/349Mi) % 15.23/2.76 % (3539297)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=3395544648:st=2:i=295:rtra=on:ss=axioms_2985 on theBenchmark for (2985ds/295Mi) % 15.23/2.76 % (3539293)Instruction limit reached! % 15.23/2.76 % (3539293)------------------------------ % 15.23/2.76 % (3539293)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.23/2.76 % (3539293)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.23/2.76 % (3539293)CaDiCaL version: 2.1.3 % 15.23/2.76 % (3539293)Termination reason: Instruction limit % 15.23/2.76 % (3539293)Termination phase: Saturation % 15.23/2.76 % (3539293)Time elapsed: 0.169 s % 15.23/2.76 % (3539293)Peak memory usage: 142 MB % 15.23/2.76 % (3539293)Instructions burned: 485 (million) % 15.23/2.76 % (3539294)Instruction limit reached! % 15.23/2.76 % (3539294)------------------------------ % 15.23/2.76 % (3539294)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.23/2.76 % (3539294)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.23/2.76 % (3539294)CaDiCaL version: 2.1.3 % 15.23/2.76 % (3539294)Termination reason: Instruction limit % 15.23/2.76 % (3539294)Termination phase: Saturation % 15.23/2.76 % (3539294)Time elapsed: 0.151 s % 15.23/2.76 % (3539294)Peak memory usage: 139 MB % 15.23/2.76 % (3539294)Instructions burned: 215 (million) % 15.23/2.76 % (3539301)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=1222256134:i=328:kws=inv_frequency:nm=20:rtra=on_2983 on theBenchmark for (2983ds/328Mi) % 15.23/2.76 % (3539275)Instruction limit reached! % 15.23/2.76 % (3539275)------------------------------ % 15.23/2.76 % (3539275)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.23/2.76 % (3539275)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.23/2.76 % (3539275)CaDiCaL version: 2.1.3 % 15.23/2.76 % (3539275)Termination reason: Instruction limit % 15.23/2.76 % (3539275)Termination phase: Saturation % 15.23/2.76 % (3539275)Time elapsed: 0.563 s % 15.23/2.76 % (3539275)Peak memory usage: 100 MB % 15.23/2.76 % (3539275)Instructions burned: 1001 (million) % 15.23/2.76 % (3539292)Instruction limit reached! % 15.23/2.76 % (3539292)------------------------------ % 15.23/2.76 % (3539292)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.23/2.76 % (3539292)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.23/2.76 % (3539292)CaDiCaL version: 2.1.3 % 15.23/2.76 % (3539292)Termination reason: Instruction limit % 16.12/2.95 % (3539292)Termination phase: Saturation % 16.12/2.95 % (3539292)Time elapsed: 0.214 s % 16.12/2.95 % (3539292)Peak memory usage: 123 MB % 16.12/2.95 % (3539292)Instructions burned: 329 (million) % 16.12/2.95 % (3539297)Instruction limit reached! % 16.12/2.95 % (3539297)------------------------------ % 16.12/2.95 % (3539297)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.12/2.95 % (3539297)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.12/2.95 % (3539297)CaDiCaL version: 2.1.3 % 16.12/2.95 % (3539297)Termination reason: Instruction limit % 16.12/2.95 % (3539297)Termination phase: Saturation % 16.12/2.95 % (3539297)Time elapsed: 0.151 s % 16.12/2.95 % (3539297)Peak memory usage: 95 MB % 16.12/2.95 % (3539297)Instructions burned: 296 (million) % 16.12/2.95 % (3539295)Instruction limit reached! % 16.12/2.95 % (3539295)------------------------------ % 16.12/2.95 % (3539295)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.12/2.95 % (3539295)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.12/2.95 % (3539295)CaDiCaL version: 2.1.3 % 16.12/2.95 % (3539295)Termination reason: Instruction limit % 16.12/2.95 % (3539295)Termination phase: Saturation % 16.12/2.95 % (3539295)Time elapsed: 0.196 s % 16.12/2.95 % (3539295)Peak memory usage: 120 MB % 16.12/2.95 % (3539295)Instructions burned: 350 (million) % 16.12/2.95 % (3539305)dis+1010_1_to=lpo:sil=128000:sas=z3:si=on:nwc=5:random_seed=1816128562:i=281:gtgl=2:rtra=on:gtg=all_2982 on theBenchmark for (2982ds/281Mi) % 16.12/2.95 % (3539307)lrs+1010_1_to=kbo:sil=128000:si=on:sos=on:urr=on:uwa=alasca_main:random_seed=902652596:i=484:doe=on:nm=0:av=off:rtra=on:ss=axioms_2982 on theBenchmark for (2982ds/484Mi) % 16.12/2.95 % (3539308)lrs+21_1_to=kbo:sil=128000:thi=neg_eq:si=on:random_seed=1624771999:i=321:canc=force:rtra=on:tac=axiom:ss=axioms:ev=force_2982 on theBenchmark for (2982ds/321Mi) % 16.12/2.95 % (3539309)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=312465474:i=416:rtra=on:gtg=position:ss=axioms_2982 on theBenchmark for (2982ds/416Mi) % 16.12/2.95 % (3539305)Instruction limit reached! % 16.12/2.95 % (3539305)------------------------------ % 16.12/2.95 % (3539305)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.12/2.95 % (3539305)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.12/2.95 % (3539305)CaDiCaL version: 2.1.3 % 16.12/2.95 % (3539305)Termination reason: Instruction limit % 16.12/2.95 % (3539305)Termination phase: Saturation % 16.12/2.95 % (3539305)Time elapsed: 0.098 s % 16.12/2.95 % (3539305)Peak memory usage: 122 MB % 16.12/2.95 % (3539305)Instructions burned: 283 (million) % 16.12/2.95 % (3539310)lrs+1010_1_to=kbo:tgt=ground:fde=unused:sas=z3:si=on:sp=unary_frequency:gve=force:spb=goal:tha=off:random_seed=2544119387:i=471:thf=on:kws=precedence:rtra=on_2981 on theBenchmark for (2981ds/471Mi) % 16.12/2.95 % (3539311)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=4165922995:avsq=on:i=276:avsqr=1,2:rtra=on_2981 on theBenchmark for (2981ds/276Mi) % 16.12/2.95 % (3539301)Instruction limit reached! % 16.12/2.95 % (3539301)------------------------------ % 16.12/2.95 % (3539301)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.12/2.95 % (3539301)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.12/2.95 % (3539301)CaDiCaL version: 2.1.3 % 16.12/2.95 % (3539301)Termination reason: Instruction limit % 16.12/2.95 % (3539301)Termination phase: Saturation % 16.12/2.95 % (3539301)Time elapsed: 0.208 s % 16.12/2.95 % (3539301)Peak memory usage: 123 MB % 16.12/2.95 % (3539301)Instructions burned: 329 (million) % 16.12/2.95 % (3539316)lrs+1010_2_to=kbo:sil=128000:tgt=ground:fde=unused:sas=z3:si=on:uwa=off:tha=off:nwc=1:random_seed=2250125598:i=375:kws=inv_arity_squared:rtra=on_2980 on theBenchmark for (2980ds/375Mi) % 16.12/2.95 % (3539308)Instruction limit reached! % 16.12/2.95 % (3539308)------------------------------ % 16.12/2.95 % (3539308)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.12/2.95 % (3539308)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.12/2.95 % (3539308)CaDiCaL version: 2.1.3 % 16.12/2.95 % (3539308)Termination reason: Instruction limit % 16.12/2.95 % (3539308)Termination phase: Saturation % 16.12/2.95 % (3539308)Time elapsed: 0.182 s % 16.12/2.95 % (3539308)Peak memory usage: 127 MB % 16.12/2.95 % (3539308)Instructions burned: 323 (million) % 19.60/3.29 % (3539319)lrs+10_1_to=kbo:sil=128000:tgt=full:sas=z3:si=on:uwa=func_ext:slsqc=1:flr=on:slsq=on:random_seed=3293639270:i=387:bd=preordered:rtra=on:ss=axioms:sgt=8_2980 on theBenchmark for (2980ds/387Mi) % 19.60/3.29 % (3539311)Instruction limit reached! % 19.60/3.29 % (3539311)------------------------------ % 19.60/3.29 % (3539311)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.60/3.29 % (3539311)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.60/3.29 % (3539311)CaDiCaL version: 2.1.3 % 19.60/3.29 % (3539311)Termination reason: Instruction limit % 19.60/3.29 % (3539311)Termination phase: Saturation % 19.60/3.29 % (3539311)Time elapsed: 0.170 s % 19.60/3.29 % (3539311)Peak memory usage: 134 MB % 19.60/3.29 % (3539311)Instructions burned: 277 (million) % 19.60/3.29 % (3539309)Instruction limit reached! % 19.60/3.29 % (3539309)------------------------------ % 19.60/3.29 % (3539309)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.60/3.29 % (3539309)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.60/3.29 % (3539309)CaDiCaL version: 2.1.3 % 19.60/3.29 % (3539309)Termination reason: Instruction limit % 19.60/3.29 % (3539309)Termination phase: Saturation % 19.60/3.29 % (3539309)Time elapsed: 0.227 s % 19.60/3.29 % (3539309)Peak memory usage: 124 MB % 19.60/3.29 % (3539309)Instructions burned: 417 (million) % 19.60/3.29 % (3539307)Instruction limit reached! % 19.60/3.29 % (3539307)------------------------------ % 19.60/3.29 % (3539307)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.60/3.29 % (3539307)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.60/3.29 % (3539307)CaDiCaL version: 2.1.3 % 19.60/3.29 % (3539307)Termination reason: Instruction limit % 19.60/3.29 % (3539307)Termination phase: Saturation % 19.60/3.29 % (3539307)Time elapsed: 0.250 s % 19.60/3.29 % (3539307)Peak memory usage: 97 MB % 19.60/3.29 % (3539307)Instructions burned: 485 (million) % 19.60/3.29 % (3539316)Instruction limit reached! % 19.60/3.29 % (3539316)------------------------------ % 19.60/3.29 % (3539316)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.60/3.29 % (3539316)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.60/3.29 % (3539316)CaDiCaL version: 2.1.3 % 19.60/3.29 % (3539316)Termination reason: Instruction limit % 19.60/3.29 % (3539316)Termination phase: Saturation % 19.60/3.29 % (3539316)Time elapsed: 0.108 s % 19.60/3.29 % (3539316)Peak memory usage: 119 MB % 19.60/3.29 % (3539316)Instructions burned: 376 (million) % 19.60/3.29 % (3539310)Instruction limit reached! % 19.60/3.29 % (3539310)------------------------------ % 19.60/3.29 % (3539310)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.60/3.29 % (3539310)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.60/3.29 % (3539310)CaDiCaL version: 2.1.3 % 19.60/3.29 % (3539310)Termination reason: Instruction limit % 19.60/3.29 % (3539310)Termination phase: Saturation % 19.60/3.29 % (3539310)Time elapsed: 0.263 s % 19.60/3.29 % (3539310)Peak memory usage: 125 MB % 19.60/3.29 % (3539310)Instructions burned: 473 (million) % 19.60/3.29 % (3539321)lrs+10_1_to=kbo:sil=128000:fde=none:si=on:norm_ineq=on:urr=on:nwc=0.5:random_seed=2216515590:i=513:kws=frequency:bd=all:rtra=on:gtg=exists_all:ss=axioms:sgt=4_2979 on theBenchmark for (2979ds/513Mi) % 19.60/3.29 % (3539326)lrs-2_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_max:tha=off:random_seed=3221076535:st=1.5:i=261:sd=1:kws=precedence:rtra=on:ss=axioms_2978 on theBenchmark for (2978ds/261Mi) % 19.60/3.29 % (3539323)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=2413452808:i=334:rtra=on_2978 on theBenchmark for (2978ds/334Mi) % 19.60/3.29 % (3539324)lrs+1010_1_to=kbo:sil=64000:sas=cadical:si=on:sos=on:bce=on:random_seed=762103330:i=359:rtra=on:gtg=exists_top:ss=axioms_2978 on theBenchmark for (2978ds/359Mi) % 19.60/3.29 % (3539325)dis+1010_1_to=lpo:sil=128000:thi=all:fde=unused:si=on:sp=reverse_arity:tha=off:random_seed=1484124703:i=341:gtgl=2:rtra=on:gtg=exists_sym:ev=force:fsd=on:fsdmm=1_2978 on theBenchmark for (2978ds/341Mi) % 19.60/3.29 % (3539319)Instruction limit reached! % 19.60/3.29 % (3539319)------------------------------ % 19.60/3.29 % (3539319)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.60/3.29 % (3539319)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.60/3.29 % (3539319)CaDiCaL version: 2.1.3 % 19.60/3.29 % (3539319)Termination reason: Instruction limit % 21.75/3.66 % (3539319)Termination phase: Saturation % 21.75/3.66 % (3539319)Time elapsed: 0.210 s % 21.75/3.66 % (3539319)Peak memory usage: 119 MB % 21.75/3.66 % (3539319)Instructions burned: 387 (million) % 21.75/3.66 % (3539326)Instruction limit reached! % 21.75/3.66 % (3539326)------------------------------ % 21.75/3.66 % (3539326)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.75/3.66 % (3539326)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.75/3.66 % (3539326)CaDiCaL version: 2.1.3 % 21.75/3.66 % (3539326)Termination reason: Instruction limit % 21.75/3.66 % (3539326)Termination phase: Saturation % 21.75/3.66 % (3539326)Time elapsed: 0.081 s % 21.75/3.66 % (3539326)Peak memory usage: 118 MB % 21.75/3.66 % (3539326)Instructions burned: 261 (million) % 21.75/3.66 % (3539327)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=1894175447:s2pl=no:i=235:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2977 on theBenchmark for (2977ds/235Mi) % 21.75/3.66 % (3539334)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=3571416043:i=146:doe=on:rtra=on_2976 on theBenchmark for (2976ds/146Mi) % 21.75/3.66 % (3539324)Instruction limit reached! % 21.75/3.66 % (3539324)------------------------------ % 21.75/3.66 % (3539324)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.75/3.66 % (3539324)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.75/3.66 % (3539324)CaDiCaL version: 2.1.3 % 21.75/3.66 % (3539324)Termination reason: Instruction limit % 21.75/3.66 % (3539324)Termination phase: Saturation % 21.75/3.66 % (3539324)Time elapsed: 0.174 s % 21.75/3.66 % (3539324)Peak memory usage: 96 MB % 21.75/3.66 % (3539324)Instructions burned: 359 (million) % 21.75/3.66 % (3539323)Instruction limit reached! % 21.75/3.66 % (3539323)------------------------------ % 21.75/3.66 % (3539323)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.75/3.66 % (3539323)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.75/3.66 % (3539323)CaDiCaL version: 2.1.3 % 21.75/3.66 % (3539323)Termination reason: Instruction limit % 21.75/3.66 % (3539323)Termination phase: Saturation % 21.75/3.66 % (3539323)Time elapsed: 0.210 s % 21.75/3.66 % (3539323)Peak memory usage: 137 MB % 21.75/3.66 % (3539323)Instructions burned: 335 (million) % 21.75/3.66 % (3539321)Instruction limit reached! % 21.75/3.66 % (3539321)------------------------------ % 21.75/3.66 % (3539321)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.75/3.66 % (3539321)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.75/3.66 % (3539321)CaDiCaL version: 2.1.3 % 21.75/3.66 % (3539321)Termination reason: Instruction limit % 21.75/3.66 % (3539321)Termination phase: Saturation % 21.75/3.66 % (3539321)Time elapsed: 0.256 s % 21.75/3.66 % (3539321)Peak memory usage: 97 MB % 21.75/3.66 % (3539321)Instructions burned: 513 (million) % 21.75/3.66 % (3539325)Instruction limit reached! % 21.75/3.66 % (3539325)------------------------------ % 21.75/3.66 % (3539325)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.75/3.66 % (3539325)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.75/3.66 % (3539325)CaDiCaL version: 2.1.3 % 21.75/3.66 % (3539325)Termination reason: Instruction limit % 21.75/3.66 % (3539325)Termination phase: Saturation % 21.75/3.66 % (3539325)Time elapsed: 0.199 s % 21.75/3.66 % (3539325)Peak memory usage: 133 MB % 21.75/3.66 % (3539325)Instructions burned: 341 (million) % 21.75/3.66 % (3539333)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=1760424793:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2976 on theBenchmark for (2976ds/273Mi) % 21.75/3.66 % (3539334)Instruction limit reached! % 21.75/3.66 % (3539334)------------------------------ % 21.75/3.66 % (3539334)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.75/3.66 % (3539334)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.75/3.66 % (3539334)CaDiCaL version: 2.1.3 % 21.75/3.66 % (3539334)Termination reason: Instruction limit % 21.75/3.66 % (3539334)Termination phase: Saturation % 21.75/3.66 % (3539334)Time elapsed: 0.041 s % 21.75/3.66 % (3539334)Peak memory usage: 93 MB % 21.75/3.66 % (3539334)Instructions burned: 149 (million) % 21.75/3.66 % (3539327)Instruction limit reached! % 21.75/3.66 % (3539327)------------------------------ % 21.75/3.66 % (3539327)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.33/4.15 % (3539327)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.33/4.15 % (3539327)CaDiCaL version: 2.1.3 % 26.33/4.15 % (3539327)Termination reason: Instruction limit % 26.33/4.15 % (3539327)Termination phase: Saturation % 26.33/4.15 % (3539327)Time elapsed: 0.153 s % 26.33/4.15 % (3539327)Peak memory usage: 122 MB % 26.33/4.15 % (3539327)Instructions burned: 235 (million) % 26.33/4.15 % (3539341)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=2839050440:i=655:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2974 on theBenchmark for (2974ds/655Mi) % 26.33/4.15 % (3539337)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=1611402888:i=4428:doe=on:fsr=off:rtra=on_2975 on theBenchmark for (2975ds/4428Mi) % 26.33/4.15 % (3539338)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=699750520:avsq=on:i=276:avsqr=1,2:rtra=on_2975 on theBenchmark for (2975ds/276Mi) % 26.33/4.15 % (3539340)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=2151336266:i=1052:rtra=on_2974 on theBenchmark for (2974ds/1052Mi) % 26.33/4.15 % (3539333)Instruction limit reached! % 26.33/4.15 % (3539333)------------------------------ % 26.33/4.15 % (3539333)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.33/4.15 % (3539333)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.33/4.15 % (3539333)CaDiCaL version: 2.1.3 % 26.33/4.15 % (3539333)Termination reason: Instruction limit % 26.33/4.15 % (3539333)Termination phase: Saturation % 26.33/4.15 % (3539333)Time elapsed: 0.151 s % 26.33/4.15 % (3539333)Peak memory usage: 96 MB % 26.33/4.15 % (3539333)Instructions burned: 273 (million) % 26.33/4.15 % (3539342)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=1555381899:st=5:i=1054:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2974 on theBenchmark for (2974ds/1054Mi) % 26.33/4.15 % (3539343)lrs-1002_1_to=kbo:sas=z3:si=on:norm_ineq=on:sos=on:tha=some:random_seed=2924643402:i=107:rtra=on_2974 on theBenchmark for (2974ds/107Mi) % 26.33/4.15 % (3539343)Instruction limit reached! % 26.33/4.15 % (3539343)------------------------------ % 26.33/4.15 % (3539343)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.33/4.15 % (3539343)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.33/4.15 % (3539343)CaDiCaL version: 2.1.3 % 26.33/4.15 % (3539343)Termination reason: Instruction limit % 26.33/4.15 % (3539343)Termination phase: Saturation % 26.33/4.15 % (3539343)Time elapsed: 0.054 s % 26.33/4.15 % (3539343)Peak memory usage: 93 MB % 26.33/4.15 % (3539343)Instructions burned: 108 (million) % 26.33/4.15 % (3539341)Instruction limit reached! % 26.33/4.15 % (3539341)------------------------------ % 26.33/4.15 % (3539341)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.33/4.15 % (3539341)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.33/4.15 % (3539341)CaDiCaL version: 2.1.3 % 26.33/4.15 % (3539341)Termination reason: Instruction limit % 26.33/4.15 % (3539341)Termination phase: Saturation % 26.33/4.15 % (3539341)Time elapsed: 0.160 s % 26.33/4.15 % (3539341)Peak memory usage: 96 MB % 26.33/4.15 % (3539341)Instructions burned: 658 (million) % 26.33/4.15 % (3539349)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=2982151556:s2a=on:i=450:doe=on:nm=32:rtra=on_2973 on theBenchmark for (2973ds/450Mi) % 26.33/4.15 % (3539338)Instruction limit reached! % 26.33/4.15 % (3539338)------------------------------ % 26.33/4.15 % (3539338)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.33/4.15 % (3539338)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.33/4.15 % (3539338)CaDiCaL version: 2.1.3 % 26.33/4.15 % (3539338)Termination reason: Instruction limit % 26.33/4.15 % (3539338)Termination phase: Saturation % 26.33/4.15 % (3539338)Time elapsed: 0.178 s % 26.33/4.15 % (3539338)Peak memory usage: 135 MB % 26.33/4.15 % (3539338)Instructions burned: 278 (million) % 26.33/4.15 % (3539351)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 % 26.33/4.15 % (3539352)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=2557885770:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2972 on theBenchmark for (2972ds/130Mi) % 27.68/4.59 % (3539351)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=726430042:i=1090:aac=none:nm=0:rtra=on:rawr=on_2972 on theBenchmark for (2972ds/1090Mi) % 27.68/4.59 % (3539352)Instruction limit reached! % 27.68/4.59 % (3539352)------------------------------ % 27.68/4.59 % (3539352)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.68/4.59 % (3539352)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.68/4.59 % (3539352)CaDiCaL version: 2.1.3 % 27.68/4.59 % (3539352)Termination reason: Instruction limit % 27.68/4.59 % (3539352)Termination phase: Twee Goal Transformation % 27.68/4.59 % (3539352)Time elapsed: 0.033 s % 27.68/4.59 % (3539352)Peak memory usage: 91 MB % 27.68/4.59 % (3539352)Instructions burned: 131 (million) % 27.68/4.59 % (3539354)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=2384418089:i=312:kws=inv_frequency:nm=20:rtra=on_2971 on theBenchmark for (2971ds/312Mi) % 27.68/4.59 % (3539357)ott+10_1_to=kbo:sil=64000:si=on:sp=reverse_frequency:sos=on:random_seed=79164536:i=491:doe=on:rtra=on:gtg=position_2970 on theBenchmark for (2970ds/491Mi) % 27.68/4.59 % (3539349)Instruction limit reached! % 27.68/4.59 % (3539349)------------------------------ % 27.68/4.59 % (3539349)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.68/4.59 % (3539349)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.68/4.59 % (3539349)CaDiCaL version: 2.1.3 % 27.68/4.59 % (3539349)Termination reason: Instruction limit % 27.68/4.59 % (3539349)Termination phase: Saturation % 27.68/4.59 % (3539349)Time elapsed: 0.298 s % 27.68/4.59 % (3539349)Peak memory usage: 142 MB % 27.68/4.59 % (3539349)Instructions burned: 450 (million) % 27.68/4.59 % (3539351)Refutation not found, incomplete strategy % 27.68/4.59 % (3539351)------------------------------ % 27.68/4.59 % (3539351)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.68/4.59 % (3539351)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.68/4.59 % (3539351)CaDiCaL version: 2.1.3 % 27.68/4.59 % (3539351)Termination reason: Refutation not found, incomplete strategy % 27.68/4.59 % (3539351)Time elapsed: 0.247 s % 27.68/4.59 % (3539351)Peak memory usage: 125 MB % 27.68/4.59 % (3539351)Instructions burned: 423 (million) % 27.68/4.59 % (3539357)Instruction limit reached! % 27.68/4.59 % (3539357)------------------------------ % 27.68/4.59 % (3539357)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.68/4.59 % (3539357)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.68/4.59 % (3539357)CaDiCaL version: 2.1.3 % 27.68/4.59 % (3539357)Termination reason: Instruction limit % 27.68/4.59 % (3539357)Termination phase: Saturation % 27.68/4.59 % (3539357)Time elapsed: 0.122 s % 27.68/4.59 % (3539357)Peak memory usage: 96 MB % 27.68/4.59 % (3539357)Instructions burned: 493 (million) % 27.68/4.59 % (3539354)Instruction limit reached! % 27.68/4.59 % (3539354)------------------------------ % 27.68/4.59 % (3539354)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.68/4.59 % (3539354)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.68/4.59 % (3539354)CaDiCaL version: 2.1.3 % 27.68/4.59 % (3539354)Termination reason: Instruction limit % 27.68/4.59 % (3539354)Termination phase: Saturation % 27.68/4.59 % (3539354)Time elapsed: 0.194 s % 27.68/4.59 % (3539354)Peak memory usage: 122 MB % 27.68/4.59 % (3539354)Instructions burned: 313 (million) % 27.68/4.59 % (3539340)Instruction limit reached! % 27.68/4.59 % (3539340)------------------------------ % 27.68/4.59 % (3539340)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.68/4.59 % (3539340)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.68/4.59 % (3539340)CaDiCaL version: 2.1.3 % 27.68/4.59 % (3539340)Termination reason: Instruction limit % 27.68/4.59 % (3539340)Termination phase: Saturation % 27.68/4.59 % (3539340)Time elapsed: 0.576 s % 27.68/4.59 % (3539340)Peak memory usage: 99 MB % 27.68/4.59 % (3539340)Instructions burned: 1052 (million) % 27.68/4.59 % (3539342)Instruction limit reached! % 27.68/4.59 % (3539342)------------------------------ % 27.68/4.59 % (3539342)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.68/4.59 % (3539342)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.68/4.59 % (3539342)CaDiCaL version: 2.1.3 % 27.68/4.59 % (3539342)Termination reason: Instruction limit % 27.68/4.59 % (3539342)Termination phase: Saturation % 35.18/5.54 % (3539342)Time elapsed: 0.584 s % 35.18/5.54 % (3539342)Peak memory usage: 103 MB % 35.18/5.54 % (3539342)Instructions burned: 1055 (million) % 35.18/5.54 % (3539360)ott+1011_4:1_to=lpo:sil=64000:si=on:spb=intro:random_seed=651571487:s2a=on:i=835:s2at=2:rtra=on_2968 on theBenchmark for (2968ds/835Mi) % 35.18/5.54 % (3539361)ott+1011_2_to=lpo:sil=128000:si=on:sos=on:random_seed=2880946932:i=307:bd=preordered:av=off:rtra=on:ev=cautious_2968 on theBenchmark for (2968ds/307Mi) % 35.18/5.54 % (3539362)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=1252601225:i=776:doe=on:rtra=on_2968 on theBenchmark for (2968ds/776Mi) % 35.18/5.54 % (3539351)------------------------------ % 35.18/5.54 % (3539351)------------------------------ % 35.18/5.54 % (3539361)Instruction limit reached! % 35.18/5.54 % (3539361)------------------------------ % 35.18/5.54 % (3539361)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 35.18/5.54 % (3539361)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.18/5.54 % (3539361)CaDiCaL version: 2.1.3 % 35.18/5.54 % (3539361)Termination reason: Instruction limit % 35.18/5.54 % (3539361)Termination phase: Saturation % 35.18/5.54 % (3539361)Time elapsed: 0.082 s % 35.18/5.54 % (3539361)Peak memory usage: 96 MB % 35.18/5.54 % (3539361)Instructions burned: 308 (million) % 35.18/5.54 % (3539363)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=1234193985:s2a=on:i=646:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2967 on theBenchmark for (2967ds/646Mi) % 35.18/5.54 % (3539364)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=3276729768:thitd=on:cond=fast:i=784:nm=30:rtra=on:gtg=all:tac=axiom_2967 on theBenchmark for (2967ds/784Mi) % 35.18/5.54 % (3539368)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=4156237775:thitd=on:s2a=on:i=1131:add=on:canc=force:bd=all:rtra=on:tac=axiom:ev=off_2966 on theBenchmark for (2966ds/1131Mi) % 35.18/5.54 % (3539369)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=1251540246:s2pl=no:i=246:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2966 on theBenchmark for (2966ds/246Mi) % 35.18/5.54 % (3539369)Instruction limit reached! % 35.18/5.54 % (3539369)------------------------------ % 35.18/5.54 % (3539369)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 35.18/5.54 % (3539369)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.18/5.54 % (3539369)CaDiCaL version: 2.1.3 % 35.18/5.54 % (3539369)Termination reason: Instruction limit % 35.18/5.54 % (3539369)Termination phase: Saturation % 35.18/5.54 % (3539369)Time elapsed: 0.154 s % 35.18/5.54 % (3539369)Peak memory usage: 123 MB % 35.18/5.54 % (3539369)Instructions burned: 247 (million) % 35.18/5.54 % (3539360)Instruction limit reached! % 35.18/5.54 % (3539360)------------------------------ % 35.18/5.54 % (3539360)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 35.18/5.54 % (3539360)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.18/5.54 % (3539360)CaDiCaL version: 2.1.3 % 35.18/5.54 % (3539360)Termination reason: Instruction limit % 35.18/5.54 % (3539360)Termination phase: Saturation % 35.18/5.54 % (3539360)Time elapsed: 0.431 s % 35.18/5.54 % (3539360)Peak memory usage: 100 MB % 35.18/5.54 % (3539360)Instructions burned: 836 (million) % 35.18/5.54 % (3539363)Instruction limit reached! % 35.18/5.54 % (3539363)------------------------------ % 35.18/5.54 % (3539363)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 35.18/5.54 % (3539363)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.18/5.54 % (3539363)CaDiCaL version: 2.1.3 % 35.18/5.54 % (3539363)Termination reason: Instruction limit % 35.18/5.54 % (3539363)Termination phase: Saturation % 35.18/5.54 % (3539363)Time elapsed: 0.342 s % 35.18/5.54 % (3539363)Peak memory usage: 136 MB % 35.18/5.54 % (3539363)Instructions burned: 647 (million) % 35.18/5.54 % (3539362)Instruction limit reached! % 35.18/5.54 % (3539362)------------------------------ % 35.18/5.54 % (3539362)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 35.18/5.54 % (3539362)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.18/5.54 % (3539362)CaDiCaL version: 2.1.3 % 35.18/5.54 % (3539362)Termination reason: Instruction limit % 35.18/5.54 % (3539362)Termination phase: Saturation % 35.18/5.54 % (3539362)Time elapsed: 0.407 s % 42.17/6.41 % (3539362)Peak memory usage: 125 MB % 42.17/6.41 % (3539362)Instructions burned: 777 (million) % 42.17/6.41 % (3539374)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=884762037:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2962 on theBenchmark for (2962ds/775Mi) % 42.17/6.41 % (3539375)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=4027153711:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2962 on theBenchmark for (2962ds/273Mi) % 42.17/6.41 % (3539368)Instruction limit reached! % 42.17/6.41 % (3539368)------------------------------ % 42.17/6.41 % (3539368)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 42.17/6.41 % (3539368)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.17/6.41 % (3539368)CaDiCaL version: 2.1.3 % 42.17/6.41 % (3539368)Termination reason: Instruction limit % 42.17/6.41 % (3539368)Termination phase: Saturation % 42.17/6.41 % (3539368)Time elapsed: 0.386 s % 42.17/6.41 % (3539368)Peak memory usage: 134 MB % 42.17/6.41 % (3539368)Instructions burned: 1133 (million) % 42.17/6.41 % (3539377)lrs+10_1_to=lpo:sil=128000:si=on:bsr=unit_only:tha=off:random_seed=1227028443:avsq=on:s2a=on:i=1094:s2at=5:avsqr=4463,131072:rtra=on_2962 on theBenchmark for (2962ds/1094Mi) % 42.17/6.41 % (3539376)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=161600426:i=102:nm=16:rtra=on_2962 on theBenchmark for (2962ds/102Mi) % 42.17/6.41 % (3539364)Instruction limit reached! % 42.17/6.41 % (3539364)------------------------------ % 42.17/6.41 % (3539364)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 42.17/6.41 % (3539364)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.17/6.41 % (3539364)CaDiCaL version: 2.1.3 % 42.17/6.41 % (3539364)Termination reason: Instruction limit % 42.17/6.41 % (3539364)Termination phase: Saturation % 42.17/6.41 % (3539364)Time elapsed: 0.503 s % 42.17/6.41 % (3539364)Peak memory usage: 125 MB % 42.17/6.41 % (3539364)Instructions burned: 785 (million) % 42.17/6.41 % (3539376)Instruction limit reached! % 42.17/6.41 % (3539376)------------------------------ % 42.17/6.41 % (3539376)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 42.17/6.41 % (3539376)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.17/6.41 % (3539376)CaDiCaL version: 2.1.3 % 42.17/6.41 % (3539376)Termination reason: Instruction limit % 42.17/6.41 % (3539376)Termination phase: Property scanning % 42.17/6.41 % (3539376)Time elapsed: 0.052 s % 42.17/6.41 % (3539376)Peak memory usage: 91 MB % 42.17/6.41 % (3539376)Instructions burned: 102 (million) % 42.17/6.41 % (3539375)Instruction limit reached! % 42.17/6.41 % (3539375)------------------------------ % 42.17/6.41 % (3539375)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 42.17/6.41 % (3539375)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.17/6.41 % (3539375)CaDiCaL version: 2.1.3 % 42.17/6.41 % (3539375)Termination reason: Instruction limit % 42.17/6.41 % (3539375)Termination phase: Saturation % 42.17/6.41 % (3539375)Time elapsed: 0.145 s % 42.17/6.41 % (3539375)Peak memory usage: 96 MB % 42.17/6.41 % (3539375)Instructions burned: 273 (million) % 42.17/6.41 % (3539380)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=3074392677:i=6400:doe=on:fsr=off:rtra=on_2961 on theBenchmark for (2961ds/6400Mi) % 42.17/6.41 % (3539383)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=3889652933:i=868:doe=on:nm=0:rtra=on:gtg=exists_sym_2960 on theBenchmark for (2960ds/868Mi) % 42.17/6.41 % (3539384)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=396281908:i=1846:canc=cautious:fsr=off:rtra=on_2960 on theBenchmark for (2960ds/1846Mi) % 42.17/6.41 % (3539385)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=444846901:s2a=on:i=36816:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2960 on theBenchmark for (2960ds/36816Mi) % 42.17/6.41 % (3539377)Refutation not found, incomplete strategy % 42.17/6.41 % (3539377)------------------------------ % 42.17/6.41 % (3539377)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 42.17/6.41 % (3539377)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.17/6.41 % (3539377)CaDiCaL version: 2.1.3 % 42.17/6.41 % (3539377)Termination reason: Refutation not found, incomplete strategy % 52.05/7.97 % (3539377)Time elapsed: 0.282 s % 52.05/7.97 % (3539377)Peak memory usage: 98 MB % 52.05/7.97 % (3539377)Instructions burned: 521 (million) % 52.05/7.97 % (3539374)Instruction limit reached! % 52.05/7.97 % (3539374)------------------------------ % 52.05/7.97 % (3539374)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 52.05/7.97 % (3539374)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 52.05/7.97 % (3539374)CaDiCaL version: 2.1.3 % 52.05/7.97 % (3539374)Termination reason: Instruction limit % 52.05/7.97 % (3539374)Termination phase: Saturation % 52.05/7.97 % (3539374)Time elapsed: 0.394 s % 52.05/7.97 % (3539374)Peak memory usage: 97 MB % 52.05/7.97 % (3539374)Instructions burned: 775 (million) % 52.05/7.97 % (3539390)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=1746669775:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2957 on theBenchmark for (2957ds/273Mi) % 52.05/7.97 % (3539377)------------------------------ % 52.05/7.97 % (3539377)------------------------------ % 52.05/7.97 % (3539385)Refutation not found, incomplete strategy % 52.05/7.97 % (3539385)------------------------------ % 52.05/7.97 % (3539385)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 52.05/7.97 % (3539385)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 52.05/7.97 % (3539385)CaDiCaL version: 2.1.3 % 52.05/7.97 % (3539385)Termination reason: Refutation not found, incomplete strategy % 52.05/7.97 % (3539385)Time elapsed: 0.313 s % 52.05/7.97 % (3539385)Peak memory usage: 98 MB % 52.05/7.97 % (3539385)Instructions burned: 604 (million) % 52.05/7.97 % (3539390)Instruction limit reached! % 52.05/7.97 % (3539390)------------------------------ % 52.05/7.97 % (3539390)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 52.05/7.97 % (3539390)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 52.05/7.97 % (3539390)CaDiCaL version: 2.1.3 % 52.05/7.97 % (3539390)Termination reason: Instruction limit % 52.05/7.97 % (3539390)Termination phase: Saturation % 52.05/7.97 % (3539390)Time elapsed: 0.146 s % 52.05/7.97 % (3539390)Peak memory usage: 96 MB % 52.05/7.97 % (3539390)Instructions burned: 274 (million) % 52.05/7.97 % (3539383)Instruction limit reached! % 52.05/7.97 % (3539383)------------------------------ % 52.05/7.97 % (3539383)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 52.05/7.97 % (3539383)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 52.05/7.97 % (3539383)CaDiCaL version: 2.1.3 % 52.05/7.97 % (3539383)Termination reason: Instruction limit % 52.05/7.97 % (3539383)Termination phase: Saturation % 52.05/7.97 % (3539383)Time elapsed: 0.511 s % 52.05/7.97 % (3539383)Peak memory usage: 126 MB % 52.05/7.97 % (3539383)Instructions burned: 869 (million) % 52.05/7.97 % (3539392)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=56056523:i=863:doe=on:nm=0:rtra=on:gtg=exists_sym_2955 on theBenchmark for (2955ds/863Mi) % 52.05/7.97 % (3539385)------------------------------ % 52.05/7.97 % (3539385)------------------------------ % 52.05/7.97 % (3539393)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=3231348258:i=5811:kws=precedence:nm=0:rtra=on_2954 on theBenchmark for (2954ds/5811Mi) % 52.05/7.97 % (3539394)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=2749125709:i=2216:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2954 on theBenchmark for (2954ds/2216Mi) % 52.05/7.97 % (3539397)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=1972243271:i=801:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2952 on theBenchmark for (2952ds/801Mi) % 52.05/7.97 % (3539392)Instruction limit reached! % 52.05/7.97 % (3539392)------------------------------ % 52.05/7.97 % (3539392)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 52.05/7.97 % (3539392)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 52.05/7.97 % (3539392)CaDiCaL version: 2.1.3 % 52.05/7.97 % (3539392)Termination reason: Instruction limit % 52.05/7.97 % (3539392)Termination phase: Saturation % 52.05/7.97 % (3539392)Time elapsed: 0.507 s % 52.05/7.97 % (3539392)Peak memory usage: 126 MB % 52.05/7.97 % (3539392)Instructions burned: 863 (million) % 52.05/7.97 % (3539384)Instruction limit reached! % 52.05/7.97 % (3539384)------------------------------ % 52.05/7.97 % (3539384)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 64.42/9.60 % (3539384)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 64.42/9.60 % (3539384)CaDiCaL version: 2.1.3 % 64.42/9.60 % (3539384)Termination reason: Instruction limit % 64.42/9.60 % (3539384)Termination phase: Saturation % 64.42/9.60 % (3539384)Time elapsed: 1.036 s % 64.42/9.60 % (3539384)Peak memory usage: 112 MB % 64.42/9.60 % (3539384)Instructions burned: 1846 (million) % 64.42/9.60 % (3539337)Instruction limit reached! % 64.42/9.60 % (3539337)------------------------------ % 64.42/9.60 % (3539337)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 64.42/9.60 % (3539337)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 64.42/9.60 % (3539337)CaDiCaL version: 2.1.3 % 64.42/9.60 % (3539337)Termination reason: Instruction limit % 64.42/9.60 % (3539337)Termination phase: Saturation % 64.42/9.60 % (3539337)Time elapsed: 2.579 s % 64.42/9.60 % (3539337)Peak memory usage: 120 MB % 64.42/9.60 % (3539337)Instructions burned: 4429 (million) % 64.42/9.60 % (3539393)Refutation not found, incomplete strategy % 64.42/9.60 % (3539393)------------------------------ % 64.42/9.60 % (3539393)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 64.42/9.60 % (3539393)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 64.42/9.60 % (3539393)CaDiCaL version: 2.1.3 % 64.42/9.60 % (3539393)Termination reason: Refutation not found, incomplete strategy % 64.42/9.60 % (3539393)Time elapsed: 0.488 s % 64.42/9.60 % (3539393)Peak memory usage: 126 MB % 64.42/9.60 % (3539393)Instructions burned: 853 (million) % 64.42/9.60 % (3539397)Instruction limit reached! % 64.42/9.60 % (3539397)------------------------------ % 64.42/9.60 % (3539397)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 64.42/9.60 % (3539397)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 64.42/9.60 % (3539397)CaDiCaL version: 2.1.3 % 64.42/9.60 % (3539397)Termination reason: Instruction limit % 64.42/9.60 % (3539397)Termination phase: Saturation % 64.42/9.60 % (3539397)Time elapsed: 0.369 s % 64.42/9.60 % (3539397)Peak memory usage: 98 MB % 64.42/9.60 % (3539397)Instructions burned: 801 (million) % 64.42/9.60 % (3539400)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=3830069327:st=5:i=1026:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2948 on theBenchmark for (2948ds/1026Mi) % 64.42/9.60 % (3539401)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=3076509681:i=3509:rtra=on_2948 on theBenchmark for (2948ds/3509Mi) % 64.42/9.60 % (3539402)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=907103225:st=2:i=2127:sd=12:ep=R:rtra=on:ss=axioms_2948 on theBenchmark for (2948ds/2127Mi) % 64.42/9.60 % (3539403)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=3105661281:i=1959:rtra=on:fsd=on:proc=on_2947 on theBenchmark for (2947ds/1959Mi) % 64.42/9.60 % (3539393)------------------------------ % 64.42/9.60 % (3539393)------------------------------ % 64.42/9.60 % (3539408)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=617253660:s2a=on:i=3553:nm=0:rtra=on_2945 on theBenchmark for (2945ds/3553Mi) % 64.42/9.60 % (3539400)Instruction limit reached! % 64.42/9.60 % (3539400)------------------------------ % 64.42/9.60 % (3539400)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 64.42/9.60 % (3539400)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 64.42/9.60 % (3539400)CaDiCaL version: 2.1.3 % 64.42/9.60 % (3539400)Termination reason: Instruction limit % 64.42/9.60 % (3539400)Termination phase: Saturation % 64.42/9.60 % (3539400)Time elapsed: 0.566 s % 64.42/9.60 % (3539400)Peak memory usage: 103 MB % 64.42/9.60 % (3539400)Instructions burned: 1026 (million) % 64.42/9.60 % (3539394)Instruction limit reached! % 64.42/9.60 % (3539394)------------------------------ % 64.42/9.60 % (3539394)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 64.42/9.60 % (3539394)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 64.42/9.60 % (3539394)CaDiCaL version: 2.1.3 % 64.42/9.60 % (3539394)Termination reason: Instruction limit % 64.42/9.60 % (3539394)Termination phase: Saturation % 64.42/9.60 % (3539394)Time elapsed: 1.141 s % 64.42/9.60 % (3539394)Peak memory usage: 129 MB % 64.42/9.60 % (3539394)Instructions burned: 2217 (million) % 64.42/9.60 % (3539410)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=1314509958:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2941 on theBenchmark for (2941ds/3201Mi) % 90.68/13.29 % (3539411)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=2245931164:thitd=on:cond=on:i=4093:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2941 on theBenchmark for (2941ds/4093Mi) % 90.68/13.29 % (3539403)Refutation not found, incomplete strategy % 90.68/13.29 % (3539403)------------------------------ % 90.68/13.29 % (3539403)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 90.68/13.29 % (3539403)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 90.68/13.29 % (3539403)CaDiCaL version: 2.1.3 % 90.68/13.29 % (3539403)Termination reason: Refutation not found, incomplete strategy % 90.68/13.29 % (3539403)Time elapsed: 0.672 s % 90.68/13.29 % (3539403)Peak memory usage: 130 MB % 90.68/13.29 % (3539403)Instructions burned: 1272 (million) % 90.68/13.29 % (3539380)Instruction limit reached! % 90.68/13.29 % (3539380)------------------------------ % 90.68/13.29 % (3539380)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 90.68/13.29 % (3539380)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 90.68/13.30 % (3539380)CaDiCaL version: 2.1.3 % 90.68/13.30 % (3539380)Termination reason: Instruction limit % 90.68/13.30 % (3539380)Termination phase: Saturation % 90.68/13.30 % (3539380)Time elapsed: 2.090 s % 90.68/13.30 % (3539380)Peak memory usage: 127 MB % 90.68/13.30 % (3539380)Instructions burned: 6401 (million) % 90.68/13.30 % (3539414)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=3795663034:cond=fast:i=21173:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2938 on theBenchmark for (2938ds/21173Mi) % 90.68/13.30 % (3539403)------------------------------ % 90.68/13.30 % (3539403)------------------------------ % 90.68/13.30 % (3539402)Instruction limit reached! % 90.68/13.30 % (3539402)------------------------------ % 90.68/13.30 % (3539402)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 90.68/13.30 % (3539402)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 90.68/13.30 % (3539402)CaDiCaL version: 2.1.3 % 90.68/13.30 % (3539402)Termination reason: Instruction limit % 90.68/13.30 % (3539402)Termination phase: Saturation % 90.68/13.30 % (3539402)Time elapsed: 1.098 s % 90.68/13.30 % (3539402)Peak memory usage: 108 MB % 90.68/13.30 % (3539402)Instructions burned: 2128 (million) % 90.68/13.30 % (3539416)lrs+11_1_to=lpo:thi=all:sas=z3:si=on:fd=off:sac=on:slsq=on:random_seed=3346309050:avsq=on:i=10544:avsqr=17,4:canc=force:rtra=on:gtg=exists_top:er=filter_2936 on theBenchmark for (2936ds/10544Mi) % 90.68/13.30 % (3539417)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=1867556948:avsq=on:i=1262:avsqr=1,16:rtra=on:rawr=on_2935 on theBenchmark for (2935ds/1262Mi) % 90.68/13.30 % (3539417)Refutation not found, incomplete strategy % 90.68/13.30 % (3539417)------------------------------ % 90.68/13.30 % (3539417)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 90.68/13.30 % (3539417)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 90.68/13.30 % (3539417)CaDiCaL version: 2.1.3 % 90.68/13.30 % (3539417)Termination reason: Refutation not found, incomplete strategy % 90.68/13.30 % (3539417)Time elapsed: 0.606 s % 90.68/13.30 % (3539417)Peak memory usage: 127 MB % 90.68/13.30 % (3539417)Instructions burned: 1091 (million) % 90.68/13.30 % (3539410)Instruction limit reached! % 90.68/13.30 % (3539410)------------------------------ % 90.68/13.30 % (3539410)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 90.68/13.30 % (3539410)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 90.68/13.30 % (3539410)CaDiCaL version: 2.1.3 % 90.68/13.30 % (3539410)Termination reason: Instruction limit % 90.68/13.30 % (3539410)Termination phase: Saturation % 90.68/13.30 % (3539410)Time elapsed: 1.477 s % 90.68/13.30 % (3539410)Peak memory usage: 117 MB % 90.68/13.30 % (3539410)Instructions burned: 3202 (million) % 90.68/13.30 % (3539417)------------------------------ % 90.68/13.30 % (3539417)------------------------------ % 90.68/13.30 % (3539401)Instruction limit reached! % 90.68/13.30 % (3539401)------------------------------ % 90.68/13.30 % (3539401)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 90.68/13.30 % (3539401)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 90.68/13.30 % (3539401)CaDiCaL version: 2.1.3 % 90.68/13.30 % (3539401)Termination reason: Instruction limit % 101.22/14.94 % (3539401)Termination phase: Saturation % 101.22/14.94 % (3539401)Time elapsed: 2.270 s % 101.22/14.94 % (3539401)Peak memory usage: 109 MB % 101.22/14.94 % (3539401)Instructions burned: 3510 (million) % 101.22/14.94 % (3539421)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=2207729231:i=270:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2925 on theBenchmark for (2925ds/270Mi) % 101.22/14.94 % (3539420)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=3273039549:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2925 on theBenchmark for (2925ds/775Mi) % 101.22/14.94 % (3539422)ott+10_128_isp=bottom:to=lpo:sil=128000:si=on:urr=on:uwa=alasca_main:sac=on:slsq=on:random_seed=2382270358:i=17165:aac=none:doe=on:rtra=on:gtg=exists_all_2924 on theBenchmark for (2924ds/17165Mi) % 101.22/14.94 % (3539408)Instruction limit reached! % 101.22/14.94 % (3539408)------------------------------ % 101.22/14.94 % (3539408)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 101.22/14.94 % (3539408)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 101.22/14.94 % (3539408)CaDiCaL version: 2.1.3 % 101.22/14.94 % (3539408)Termination reason: Instruction limit % 101.22/14.94 % (3539408)Termination phase: Saturation % 101.22/14.94 % (3539408)Time elapsed: 2.140 s % 101.22/14.94 % (3539408)Peak memory usage: 105 MB % 101.22/14.94 % (3539408)Instructions burned: 3553 (million) % 101.22/14.94 % (3539421)Instruction limit reached! % 101.22/14.94 % (3539421)------------------------------ % 101.22/14.94 % (3539421)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 101.22/14.94 % (3539421)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 101.22/14.94 % (3539421)CaDiCaL version: 2.1.3 % 101.22/14.94 % (3539421)Termination reason: Instruction limit % 101.22/14.94 % (3539421)Termination phase: Saturation % 101.22/14.94 % (3539421)Time elapsed: 0.142 s % 101.22/14.94 % (3539421)Peak memory usage: 96 MB % 101.22/14.94 % (3539421)Instructions burned: 270 (million) % 101.22/14.94 % (3539426)lrs+2_10_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_main:tha=some:random_seed=1602612000:s2a=on:i=13094:s2at=-1:rtra=on_2922 on theBenchmark for (2922ds/13094Mi) % 101.22/14.94 % (3539427)lrs+10_1_to=lpo:sil=128000:si=on:sp=occurrence:random_seed=327715991:st=2:i=12633:rtra=on:ss=axioms_2922 on theBenchmark for (2922ds/12633Mi) % 101.22/14.94 % (3539420)Instruction limit reached! % 101.22/14.94 % (3539420)------------------------------ % 101.22/14.94 % (3539420)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 101.22/14.94 % (3539420)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 101.22/14.94 % (3539420)CaDiCaL version: 2.1.3 % 101.22/14.94 % (3539420)Termination reason: Instruction limit % 101.22/14.94 % (3539420)Termination phase: Saturation % 101.22/14.94 % (3539420)Time elapsed: 0.393 s % 101.22/14.94 % (3539420)Peak memory usage: 97 MB % 101.22/14.94 % (3539420)Instructions burned: 775 (million) % 101.22/14.94 % (3539411)Instruction limit reached! % 101.22/14.94 % (3539411)------------------------------ % 101.22/14.94 % (3539411)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 101.22/14.94 % (3539411)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 101.22/14.94 % (3539411)CaDiCaL version: 2.1.3 % 101.22/14.94 % (3539411)Termination reason: Instruction limit % 101.22/14.94 % (3539411)Termination phase: Saturation % 101.22/14.94 % (3539411)Time elapsed: 2.092 s % 101.22/14.94 % (3539411)Peak memory usage: 148 MB % 101.22/14.94 % (3539411)Instructions burned: 4094 (million) % 101.22/14.94 % (3539430)dis+1011_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_frequency:lsd=20:nwc=3:random_seed=2358697591:i=1783:rtra=on:gtg=position_2919 on theBenchmark for (2919ds/1783Mi) % 101.22/14.94 % (3539431)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=608152399:i=5451:aac=none:doe=on:nm=0:rtra=on:amm=off:gtg=position_2918 on theBenchmark for (2918ds/5451Mi) % 101.22/14.94 % (3539430)Instruction limit reached! % 101.22/14.94 % (3539430)------------------------------ % 101.22/14.94 % (3539430)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 101.22/14.94 % (3539430)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 101.22/14.94 % (3539430)CaDiCaL version: 2.1.3 % 101.22/14.94 % (3539430)Termination reason: Instruction limit % 101.22/14.94 % (3539430)Termination phase: Saturation % 101.22/14.94 % (3539430)Time elapsed: 0.996 s % 101.22/14.94 % (3539430)Peak memory usage: 128 MB % 101.22/14.94 % (3539430)Instructions burned: 1784 (million) % 121.90/17.75 % (3539434)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=722045336:i=4975:doe=on:nm=0:rtra=on:gtg=exists_sym_2908 on theBenchmark for (2908ds/4975Mi) % 121.90/17.75 % (3539434)Refutation not found, incomplete strategy % 121.90/17.75 % (3539434)------------------------------ % 121.90/17.75 % (3539434)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 121.90/17.75 % (3539434)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.90/17.75 % (3539434)CaDiCaL version: 2.1.3 % 121.90/17.75 % (3539434)Termination reason: Refutation not found, incomplete strategy % 121.90/17.75 % (3539434)Time elapsed: 0.542 s % 121.90/17.75 % (3539434)Peak memory usage: 127 MB % 121.90/17.75 % (3539434)Instructions burned: 947 (million) % 121.90/17.75 % (3539434)------------------------------ % 121.90/17.75 % (3539434)------------------------------ % 121.90/17.75 % (3539436)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=1461103295:i=2076:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2898 on theBenchmark for (2898ds/2076Mi) % 121.90/17.75 % (3539414)Instruction limit reached! % 121.90/17.75 % (3539414)------------------------------ % 121.90/17.75 % (3539414)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 121.90/17.75 % (3539414)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.90/17.75 % (3539414)CaDiCaL version: 2.1.3 % 121.90/17.75 % (3539414)Termination reason: Instruction limit % 121.90/17.75 % (3539414)Termination phase: Saturation % 121.90/17.75 % (3539414)Time elapsed: 5.119 s % 121.90/17.75 % (3539414)Peak memory usage: 153 MB % 121.90/17.75 % (3539414)Instructions burned: 21174 (million) % 121.90/17.75 % (3539436)Instruction limit reached! % 121.90/17.75 % (3539436)------------------------------ % 121.90/17.75 % (3539436)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 121.90/17.75 % (3539436)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.90/17.75 % (3539436)CaDiCaL version: 2.1.3 % 121.90/17.75 % (3539436)Termination reason: Instruction limit % 121.90/17.75 % (3539436)Termination phase: Saturation % 121.90/17.75 % (3539436)Time elapsed: 1.081 s % 121.90/17.75 % (3539436)Peak memory usage: 129 MB % 121.90/17.75 % (3539436)Instructions burned: 2077 (million) % 121.90/17.75 % (3539438)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=312555480:i=5145:rtra=on_2886 on theBenchmark for (2886ds/5145Mi) % 121.90/17.75 % (3539431)Instruction limit reached! % 121.90/17.75 % (3539431)------------------------------ % 121.90/17.75 % (3539431)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 121.90/17.75 % (3539431)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.90/17.75 % (3539431)CaDiCaL version: 2.1.3 % 121.90/17.75 % (3539431)Termination reason: Instruction limit % 121.90/17.75 % (3539431)Termination phase: Saturation % 121.90/17.75 % (3539431)Time elapsed: 3.188 s % 121.90/17.75 % (3539431)Peak memory usage: 161 MB % 121.90/17.75 % (3539431)Instructions burned: 5451 (million) % 121.90/17.75 % (3539439)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=2798027559:i=3509:rtra=on_2886 on theBenchmark for (2886ds/3509Mi) % 121.90/17.75 % (3539441)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=4237393058:st=2:i=13800:sd=12:ep=R:rtra=on:ss=axioms_2884 on theBenchmark for (2884ds/13800Mi) % 121.90/17.75 % (3539416)Instruction limit reached! % 121.90/17.75 % (3539416)------------------------------ % 121.90/17.75 % (3539416)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 121.90/17.75 % (3539416)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.90/17.75 % (3539416)CaDiCaL version: 2.1.3 % 121.90/17.75 % (3539416)Termination reason: Instruction limit % 121.90/17.75 % (3539416)Termination phase: Saturation % 121.90/17.75 % (3539416)Time elapsed: 6.027 s % 121.90/17.75 % (3539416)Peak memory usage: 182 MB % 121.90/17.75 % (3539416)Instructions burned: 10544 (million) % 121.90/17.75 % (3539444)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=3554042441:i=1412:rtra=on:fsd=on:proc=on_2874 on theBenchmark for (2874ds/1412Mi) % 121.90/17.75 % (3539438)Instruction limit reached! % 121.90/17.75 % (3539438)------------------------------ % 121.90/17.75 % (3539438)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 121.90/17.75 % (3539438)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.63/21.49 % (3539438)CaDiCaL version: 2.1.3 % 148.63/21.49 % (3539438)Termination reason: Instruction limit % 148.63/21.49 % (3539438)Termination phase: Saturation % 148.63/21.49 % (3539438)Time elapsed: 1.396 s % 148.63/21.49 % (3539438)Peak memory usage: 105 MB % 148.63/21.49 % (3539438)Instructions burned: 5147 (million) % 148.63/21.49 % (3539446)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 % 148.63/21.49 % (3539446)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=3230512489:i=11747:aac=none:nm=0:rtra=on:rawr=on_2871 on theBenchmark for (2871ds/11747Mi) % 148.63/21.49 % (3539446)Refutation not found, incomplete strategy % 148.63/21.49 % (3539446)------------------------------ % 148.63/21.49 % (3539446)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 148.63/21.49 % (3539446)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.63/21.49 % (3539446)CaDiCaL version: 2.1.3 % 148.63/21.49 % (3539446)Termination reason: Refutation not found, incomplete strategy % 148.63/21.49 % (3539446)Time elapsed: 0.140 s % 148.63/21.49 % (3539446)Peak memory usage: 125 MB % 148.63/21.49 % (3539446)Instructions burned: 442 (million) % 148.63/21.49 % (3539446)------------------------------ % 148.63/21.49 % (3539446)------------------------------ % 148.63/21.49 % (3539444)Refutation not found, incomplete strategy % 148.63/21.49 % (3539444)------------------------------ % 148.63/21.49 % (3539444)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 148.63/21.49 % (3539444)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.63/21.49 % (3539444)CaDiCaL version: 2.1.3 % 148.63/21.49 % (3539444)Termination reason: Refutation not found, incomplete strategy % 148.63/21.49 % (3539444)Time elapsed: 0.686 s % 148.63/21.49 % (3539444)Peak memory usage: 129 MB % 148.63/21.49 % (3539444)Instructions burned: 1300 (million) % 148.63/21.49 % (3539449)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=508995446:s2a=on:i=3553:nm=0:rtra=on_2867 on theBenchmark for (2867ds/3553Mi) % 148.63/21.49 % (3539444)------------------------------ % 148.63/21.49 % (3539444)------------------------------ % 148.63/21.50 % (3539468)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=166958506:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2863 on theBenchmark for (2863ds/3201Mi) % 148.63/21.50 % (3539439)Instruction limit reached! % 148.63/21.50 % (3539439)------------------------------ % 148.63/21.50 % (3539439)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 148.63/21.50 % (3539439)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.63/21.50 % (3539439)CaDiCaL version: 2.1.3 % 148.63/21.50 % (3539439)Termination reason: Instruction limit % 148.63/21.50 % (3539439)Termination phase: Saturation % 148.63/21.50 % (3539439)Time elapsed: 2.309 s % 148.63/21.50 % (3539439)Peak memory usage: 109 MB % 148.63/21.50 % (3539439)Instructions burned: 3510 (million) % 148.63/21.50 % (3539561)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=2518790990:thitd=on:cond=on:i=4081:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2861 on theBenchmark for (2861ds/4081Mi) % 148.63/21.50 % (3539426)Instruction limit reached! % 148.63/21.50 % (3539426)------------------------------ % 148.63/21.50 % (3539426)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 148.63/21.50 % (3539426)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.63/21.50 % (3539426)CaDiCaL version: 2.1.3 % 148.63/21.50 % (3539426)Termination reason: Instruction limit % 148.63/21.50 % (3539426)Termination phase: Saturation % 148.63/21.50 % (3539426)Time elapsed: 6.512 s % 148.63/21.50 % (3539426)Peak memory usage: 121 MB % 148.63/21.50 % (3539426)Instructions burned: 13095 (million) % 148.63/21.50 % (3539449)Instruction limit reached! % 148.63/21.50 % (3539449)------------------------------ % 148.63/21.50 % (3539449)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 148.63/21.50 % (3539449)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.63/21.50 % (3539449)CaDiCaL version: 2.1.3 % 148.63/21.50 % (3539449)Termination reason: Instruction limit % 148.63/21.50 % (3539449)Termination phase: Saturation % 148.63/21.50 % (3539449)Time elapsed: 1.103 s % 148.63/21.50 % (3539449)Peak memory usage: 104 MB % 148.63/21.50 % (3539449)Instructions burned: 3554 (million) % 180.18/25.97 % (3539618)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=45902202:cond=fast:i=20260:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2855 on theBenchmark for (2855ds/20260Mi) % 180.18/25.97 % (3539650)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=449482687:s2a=on:i=58627:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2854 on theBenchmark for (2854ds/58627Mi) % 180.18/25.97 % (3539650)Refutation not found, incomplete strategy % 180.18/25.97 % (3539650)------------------------------ % 180.18/25.97 % (3539650)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 180.18/25.97 % (3539650)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.18/25.97 % (3539650)CaDiCaL version: 2.1.3 % 180.18/25.97 % (3539650)Termination reason: Refutation not found, incomplete strategy % 180.18/25.97 % (3539650)Time elapsed: 0.217 s % 180.18/25.97 % (3539650)Peak memory usage: 98 MB % 180.18/25.97 % (3539650)Instructions burned: 767 (million) % 180.18/25.97 % (3539650)------------------------------ % 180.18/25.97 % (3539650)------------------------------ % 180.18/25.97 % (3539727)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=1184842332:avsq=on:i=6258:avsqr=1,16:rtra=on:rawr=on_2848 on theBenchmark for (2848ds/6258Mi) % 180.18/25.97 % (3539468)Instruction limit reached! % 180.18/25.97 % (3539468)------------------------------ % 180.18/25.97 % (3539468)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 180.18/25.97 % (3539468)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.18/25.97 % (3539468)CaDiCaL version: 2.1.3 % 180.18/25.97 % (3539468)Termination reason: Instruction limit % 180.18/25.97 % (3539468)Termination phase: Saturation % 180.18/25.97 % (3539468)Time elapsed: 1.833 s % 180.18/25.97 % (3539468)Peak memory usage: 117 MB % 180.18/25.97 % (3539468)Instructions burned: 3201 (million) % 180.18/25.97 % (3539734)ott+10_128_isp=bottom:to=lpo:sil=128000:si=on:urr=on:uwa=alasca_main:sac=on:slsq=on:random_seed=254516810:i=34001:aac=none:doe=on:rtra=on:gtg=exists_all_2843 on theBenchmark for (2843ds/34001Mi) % 180.18/25.97 % (3539727)Refutation not found, incomplete strategy % 180.18/25.97 % (3539727)------------------------------ % 180.18/25.97 % (3539727)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 180.18/25.97 % (3539727)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.18/25.97 % (3539727)CaDiCaL version: 2.1.3 % 180.18/25.97 % (3539727)Termination reason: Refutation not found, incomplete strategy % 180.18/25.97 % (3539727)Time elapsed: 0.632 s % 180.18/25.97 % (3539727)Peak memory usage: 127 MB % 180.18/25.97 % (3539727)Instructions burned: 1324 (million) % 180.18/25.97 % (3539727)------------------------------ % 180.18/25.97 % (3539727)------------------------------ % 180.18/25.97 % (3539744)lrs+2_10_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_main:tha=some:random_seed=4069371796:s2a=on:i=71622:s2at=-1:rtra=on_2837 on theBenchmark for (2837ds/71622Mi) % 180.18/25.97 % (3539422)Instruction limit reached! % 180.18/25.97 % (3539422)------------------------------ % 180.18/25.97 % (3539422)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 180.18/25.97 % (3539422)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.18/25.97 % (3539422)CaDiCaL version: 2.1.3 % 180.18/25.97 % (3539422)Termination reason: Instruction limit % 180.18/25.97 % (3539422)Termination phase: Saturation % 180.18/25.97 % (3539422)Time elapsed: 9.080 s % 180.18/25.97 % (3539422)Peak memory usage: 100 MB % 180.18/25.97 % (3539422)Instructions burned: 17165 (million) % 180.18/25.97 % (3539561)Instruction limit reached! % 180.18/25.97 % (3539561)------------------------------ % 180.18/25.97 % (3539561)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 180.18/25.97 % (3539561)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.18/25.97 % (3539561)CaDiCaL version: 2.1.3 % 180.18/25.97 % (3539561)Termination reason: Instruction limit % 180.18/25.97 % (3539561)Termination phase: Saturation % 180.18/25.97 % (3539561)Time elapsed: 3.047 s % 180.18/25.97 % (3539561)Peak memory usage: 150 MB % 180.18/25.97 % (3539561)Instructions burned: 4082 (million) % 180.18/25.97 % (3539752)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=2091981609:i=24001:kws=precedence:nm=0:rtra=on_2831 on theBenchmark for (2831ds/24001Mi) % 180.18/25.97 % (3539427)Instruction limit reached! % 180.18/25.97 % (3539427)------------------------------ % 180.18/25.97 % (3539427)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 208.25/29.84 % (3539427)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 208.25/29.84 % (3539427)CaDiCaL version: 2.1.3 % 208.25/29.84 % (3539427)Termination reason: Instruction limit % 208.25/29.84 % (3539427)Termination phase: Saturation % 208.25/29.84 % (3539427)Time elapsed: 9.395 s % 208.25/29.84 % (3539427)Peak memory usage: 125 MB % 208.25/29.84 % (3539427)Instructions burned: 12633 (million) % 208.25/29.84 % (3539753)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=1790267899:i=2076:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2829 on theBenchmark for (2829ds/2076Mi) % 208.25/29.84 % (3539757)dis+21_20_to=lakbo:si=on:alasca=on:sp=const_max:uwa=alasca_main:sac=on:random_seed=1571409503:s2a=on:i=83971:s2at=4:bd=all:ins=1:rtra=on_2826 on theBenchmark for (2826ds/83971Mi) % 208.25/29.84 % (3539752)Refutation not found, incomplete strategy % 208.25/29.84 % (3539752)------------------------------ % 208.25/29.84 % (3539752)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 208.25/29.84 % (3539752)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 208.25/29.84 % (3539752)CaDiCaL version: 2.1.3 % 208.25/29.84 % (3539752)Termination reason: Refutation not found, incomplete strategy % 208.25/29.84 % (3539752)Time elapsed: 0.928 s % 208.25/29.84 % (3539752)Peak memory usage: 127 MB % 208.25/29.84 % (3539752)Instructions burned: 1041 (million) % 208.25/29.84 % (3539752)------------------------------ % 208.25/29.84 % (3539752)------------------------------ % 208.25/29.84 % (3539760)lrs+1011_5:1_to=lpo:sil=128000:sas=z3:si=on:norm_ineq=on:tha=some:random_seed=3168997678:i=83944:rtra=on_2815 on theBenchmark for (2815ds/83944Mi) % 208.25/29.84 % (3539753)Instruction limit reached! % 208.25/29.84 % (3539753)------------------------------ % 208.25/29.84 % (3539753)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 208.25/29.84 % (3539753)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 208.25/29.84 % (3539753)CaDiCaL version: 2.1.3 % 208.25/29.84 % (3539753)Termination reason: Instruction limit % 208.25/29.84 % (3539753)Termination phase: Saturation % 208.25/29.84 % (3539753)Time elapsed: 1.897 s % 208.25/29.84 % (3539753)Peak memory usage: 128 MB % 208.25/29.84 % (3539753)Instructions burned: 2076 (million) % 208.25/29.84 % (3539760)Refutation not found, incomplete strategy % 208.25/29.84 % (3539760)------------------------------ % 208.25/29.84 % (3539760)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 208.25/29.84 % (3539760)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 208.25/29.84 % (3539760)CaDiCaL version: 2.1.3 % 208.25/29.84 % (3539760)Termination reason: Refutation not found, incomplete strategy % 208.25/29.84 % (3539760)Time elapsed: 0.658 s % 208.25/29.84 % (3539760)Peak memory usage: 125 MB % 208.25/29.84 % (3539760)Instructions burned: 813 (million) % 208.25/29.84 % (3539764)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=4039952800:i=9201:rtra=on_2807 on theBenchmark for (2807ds/9201Mi) % 208.25/29.84 % (3539760)------------------------------ % 208.25/29.84 % (3539760)------------------------------ % 208.25/29.84 % (3539768)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 % 208.25/29.84 % (3539768)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=4192804588:i=6806:aac=none:nm=0:rtra=on:rawr=on_2802 on theBenchmark for (2802ds/6806Mi) % 208.25/29.84 % (3539768)Refutation not found, incomplete strategy % 208.25/29.84 % (3539768)------------------------------ % 208.25/29.84 % (3539768)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 208.25/29.84 % (3539768)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 208.25/29.84 % (3539768)CaDiCaL version: 2.1.3 % 208.25/29.84 % (3539768)Termination reason: Refutation not found, incomplete strategy % 208.25/29.84 % (3539768)Time elapsed: 0.424 s % 208.25/29.84 % (3539768)Peak memory usage: 125 MB % 208.25/29.84 % (3539768)Instructions burned: 462 (million) % 208.25/29.84 % (3539768)------------------------------ % 208.25/29.84 % (3539768)------------------------------ % 208.25/29.84 % (3539441)Instruction limit reached! % 208.25/29.84 % (3539441)------------------------------ % 208.25/29.84 % (3539441)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 208.25/29.84 % (3539441)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 214.22/30.72 % (3539441)CaDiCaL version: 2.1.3 % 214.22/30.72 % (3539441)Termination reason: Instruction limit % 214.22/30.72 % (3539441)Termination phase: Saturation % 214.22/30.72 % (3539441)Time elapsed: 9.419 s % 214.22/30.72 % (3539441)Peak memory usage: 146 MB % 214.22/30.72 % (3539441)Instructions burned: 13800 (million) % 214.22/30.72 % (3539774)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=582985002:s2a=on:i=3553:nm=0:rtra=on_2791 on theBenchmark for (2791ds/3553Mi) % 214.22/30.72 % (3539775)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=1439058484:thitd=on:cond=on:i=2064:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2788 on theBenchmark for (2788ds/2064Mi) % 214.22/30.72 % (3539757)Refutation not found, incomplete strategy % 214.22/30.72 % (3539757)------------------------------ % 214.22/30.72 % (3539757)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 214.22/30.72 % (3539757)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 214.22/30.72 % (3539757)CaDiCaL version: 2.1.3 % 214.22/30.72 % (3539757)Termination reason: Refutation not found, incomplete strategy % 214.22/30.72 % (3539757)Time elapsed: 5.312 s % 214.22/30.72 % (3539757)Peak memory usage: 123 MB % 214.22/30.72 % (3539757)Instructions burned: 6818 (million) % 214.22/30.72 % (3539775)Instruction limit reached! % 214.22/30.72 % (3539775)------------------------------ % 214.22/30.72 % (3539775)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 214.22/30.72 % (3539775)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 214.22/30.72 % (3539775)CaDiCaL version: 2.1.3 % 214.22/30.72 % (3539775)Termination reason: Instruction limit % 214.22/30.72 % (3539775)Termination phase: Saturation % 214.22/30.72 % (3539775)Time elapsed: 1.890 s % 214.22/30.72 % (3539775)Peak memory usage: 145 MB % 214.22/30.72 % (3539775)Instructions burned: 2064 (million) % 214.22/30.72 % (3539757)------------------------------ % 214.22/30.72 % (3539757)------------------------------ % 214.22/30.72 % (3539782)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=1108062607:cond=fast:i=20260:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2766 on theBenchmark for (2766ds/20260Mi) % 214.22/30.72 % (3539783)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=2851132733:avsq=on:i=1244:avsqr=1,16:rtra=on:rawr=on_2765 on theBenchmark for (2765ds/1244Mi) % 214.22/30.72 % (3539774)Instruction limit reached! % 214.22/30.72 % (3539774)------------------------------ % 214.22/30.72 % (3539774)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 214.22/30.72 % (3539774)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 214.22/30.72 % (3539774)CaDiCaL version: 2.1.3 % 214.22/30.72 % (3539774)Termination reason: Instruction limit % 214.22/30.72 % (3539774)Termination phase: Saturation % 214.22/30.72 % (3539774)Time elapsed: 3.258 s % 214.22/30.72 % (3539774)Peak memory usage: 104 MB % 214.22/30.72 % (3539774)Instructions burned: 3553 (million) % 214.22/30.72 % (3539788)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=3288405061:i=58261:doe=on:nm=0:rtra=on:gtg=exists_sym_2755 on theBenchmark for (2755ds/58261Mi) % 214.22/30.72 % (3539783)Instruction limit reached! % 214.22/30.72 % (3539783)------------------------------ % 214.22/30.72 % (3539783)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 214.22/30.72 % (3539783)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 214.22/30.72 % (3539783)CaDiCaL version: 2.1.3 % 214.22/30.72 % (3539783)Termination reason: Instruction limit % 214.22/30.72 % (3539783)Termination phase: Saturation % 214.22/30.72 % (3539783)Time elapsed: 1.140 s % 214.22/30.72 % (3539783)Peak memory usage: 126 MB % 214.22/30.72 % (3539783)Instructions burned: 1244 (million) % 214.22/30.72 % (3539790)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 % 214.22/30.72 % (3539790)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=3702657355:i=6806:aac=none:nm=0:rtra=on:rawr=on_2751 on theBenchmark for (2751ds/6806Mi) % 214.22/30.72 % (3539790)Refutation not found, incomplete strategy % 214.22/30.72 % (3539790)------------------------------ % 214.22/30.72 % (3539790)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 218.47/31.36 % (3539790)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 218.47/31.36 % (3539790)CaDiCaL version: 2.1.3 % 218.47/31.36 % (3539790)Termination reason: Refutation not found, incomplete strategy % 218.47/31.36 % (3539790)Time elapsed: 0.435 s % 218.47/31.36 % (3539790)Peak memory usage: 125 MB % 218.47/31.36 % (3539790)Instructions burned: 444 (million) % 218.47/31.36 % (3539788)Refutation not found, incomplete strategy % 218.47/31.36 % (3539788)------------------------------ % 218.47/31.36 % (3539788)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 218.47/31.36 % (3539788)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 218.47/31.36 % (3539788)CaDiCaL version: 2.1.3 % 218.47/31.36 % (3539788)Termination reason: Refutation not found, incomplete strategy % 218.47/31.36 % (3539788)Time elapsed: 0.923 s % 218.47/31.36 % (3539788)Peak memory usage: 128 MB % 218.47/31.36 % (3539788)Instructions burned: 1001 (million) % 218.47/31.36 % (3539790)------------------------------ % 218.47/31.36 % (3539790)------------------------------ % 218.47/31.36 % (3539788)------------------------------ % 218.47/31.36 % (3539788)------------------------------ % 218.47/31.36 % (3539795)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=3294575877:avsq=on:i=1701:avsqr=1,16:rtra=on:rawr=on_2739 on theBenchmark for (2739ds/1701Mi) % 218.47/31.36 % (3539794)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=1212793644:thitd=on:cond=on:i=4081:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2740 on theBenchmark for (2740ds/4081Mi) % 218.47/31.36 % (3539795)Refutation not found, incomplete strategy % 218.47/31.36 % (3539795)------------------------------ % 218.47/31.36 % (3539795)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 218.47/31.36 % (3539795)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 218.47/31.36 % (3539795)CaDiCaL version: 2.1.3 % 218.47/31.36 % (3539795)Termination reason: Refutation not found, incomplete strategy % 218.47/31.36 % (3539795)Time elapsed: 1.019 s % 218.47/31.36 % (3539795)Peak memory usage: 127 MB % 218.47/31.36 % (3539795)Instructions burned: 1145 (million) % 218.47/31.36 % (3539795)------------------------------ % 218.47/31.36 % (3539795)------------------------------ % 218.47/31.36 % (3539802)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=410488170:i=57001:doe=on:nm=0:rtra=on:gtg=exists_sym_2723 on theBenchmark for (2723ds/57001Mi) % 218.47/31.36 % (3539802)Refutation not found, incomplete strategy % 218.47/31.36 % (3539802)------------------------------ % 218.47/31.36 % (3539802)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 218.47/31.36 % (3539802)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 218.47/31.36 % (3539802)CaDiCaL version: 2.1.3 % 218.47/31.36 % (3539802)Termination reason: Refutation not found, incomplete strategy % 218.47/31.36 % (3539802)Time elapsed: 0.916 s % 218.47/31.36 % (3539802)Peak memory usage: 127 MB % 218.47/31.36 % (3539802)Instructions burned: 968 (million) % 218.47/31.36 % (3539764)Instruction limit reached! % 218.47/31.36 % (3539764)------------------------------ % 218.47/31.36 % (3539764)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 218.47/31.36 % (3539764)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 218.47/31.36 % (3539764)CaDiCaL version: 2.1.3 % 218.47/31.36 % (3539764)Termination reason: Instruction limit % 218.47/31.36 % (3539764)Termination phase: Saturation % 218.47/31.36 % (3539764)Time elapsed: 9.562 s % 218.47/31.36 % (3539764)Peak memory usage: 119 MB % 218.47/31.36 % (3539764)Instructions burned: 9201 (million) % 218.47/31.36 % (3539802)------------------------------ % 218.47/31.36 % (3539802)------------------------------ % 218.47/31.36 % (3539794)Instruction limit reached! % 218.47/31.36 % (3539794)------------------------------ % 218.47/31.36 % (3539794)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 218.47/31.36 % (3539794)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 218.47/31.36 % (3539794)CaDiCaL version: 2.1.3 % 218.47/31.36 % (3539794)Termination reason: Instruction limit % 218.47/31.36 % (3539794)Termination phase: Saturation % 218.47/31.36 % (3539794)Time elapsed: 3.173 s % 218.47/31.36 % (3539794)Peak memory usage: 145 MB % 218.47/31.36 % (3539794)Instructions burned: 4082 (million) % 218.47/31.36 % (3539804)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 % 220.87/31.75 % (3539804)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=3642141121:i=8622:aac=none:nm=0:rtra=on:rawr=on_2708 on theBenchmark for (2708ds/8622Mi) % 220.87/31.75 % (3539805)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=2092003375:i=24:doe=on:rtra=on:gtg=exists_top:ss=axioms_2706 on theBenchmark for (2706ds/24Mi) % 220.87/31.75 % (3539805)Instruction limit reached! % 220.87/31.75 % (3539805)------------------------------ % 220.87/31.75 % (3539805)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 220.87/31.75 % (3539805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 220.87/31.75 % (3539805)CaDiCaL version: 2.1.3 % 220.87/31.75 % (3539805)Termination reason: Instruction limit % 220.87/31.75 % (3539805)Termination phase: Property scanning % 220.87/31.75 % (3539805)Time elapsed: 0.025 s % 220.87/31.75 % (3539805)Peak memory usage: 86 MB % 220.87/31.75 % (3539805)Instructions burned: 29 (million) % 220.87/31.75 % (3539807)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=2199771714:i=614:kws=precedence:nm=0:rtra=on_2705 on theBenchmark for (2705ds/614Mi) % 220.87/31.75 % (3539809)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=852161716:i=402:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2704 on theBenchmark for (2704ds/402Mi) % 220.87/31.75 % (3539804)Refutation not found, incomplete strategy % 220.87/31.75 % (3539804)------------------------------ % 220.87/31.75 % (3539804)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 220.87/31.75 % (3539804)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 220.87/31.75 % (3539804)CaDiCaL version: 2.1.3 % 220.87/31.75 % (3539804)Termination reason: Refutation not found, incomplete strategy % 220.87/31.75 % (3539804)Time elapsed: 0.508 s % 220.87/31.75 % (3539804)Peak memory usage: 125 MB % 220.87/31.75 % (3539804)Instructions burned: 591 (million) % 220.87/31.75 % (3539618)Instruction limit reached! % 220.87/31.75 % (3539618)------------------------------ % 220.87/31.75 % (3539618)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 220.87/31.75 % (3539618)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 220.87/31.75 % (3539618)CaDiCaL version: 2.1.3 % 220.87/31.75 % (3539618)Termination reason: Instruction limit % 220.87/31.75 % (3539618)Termination phase: Saturation % 220.87/31.75 % (3539618)Time elapsed: 15.391 s % 220.87/31.75 % (3539618)Peak memory usage: 153 MB % 220.87/31.75 % (3539618)Instructions burned: 20260 (million) % 220.87/31.75 % (3539812)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=2928866196:s2a=on:i=14:rtra=on:inst=on_2699 on theBenchmark for (2699ds/14Mi) % 220.87/31.75 % (3539812)Instruction limit reached! % 220.87/31.75 % (3539812)------------------------------ % 220.87/31.75 % (3539812)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 220.87/31.75 % (3539812)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 220.87/31.75 % (3539812)CaDiCaL version: 2.1.3 % 220.87/31.75 % (3539812)Termination reason: Instruction limit % 220.87/31.75 % (3539812)Termination phase: Property scanning % 220.87/31.75 % (3539812)Time elapsed: 0.014 s % 220.87/31.75 % (3539812)Peak memory usage: 85 MB % 220.87/31.75 % (3539812)Instructions burned: 15 (million) % 220.87/31.75 % (3539807)Instruction limit reached! % 220.87/31.75 % (3539807)------------------------------ % 220.87/31.75 % (3539807)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 220.87/31.75 % (3539807)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 220.87/31.75 % (3539807)CaDiCaL version: 2.1.3 % 220.87/31.75 % (3539807)Termination reason: Instruction limit % 220.87/31.75 % (3539807)Termination phase: Saturation % 220.87/31.75 % (3539807)Time elapsed: 0.579 s % 220.87/31.75 % (3539807)Peak memory usage: 124 MB % 220.87/31.75 % (3539807)Instructions burned: 615 (million) % 220.87/31.75 % (3539809)Instruction limit reached! % 220.87/31.75 % (3539809)------------------------------ % 220.87/31.75 % (3539809)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 220.87/31.75 % (3539809)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 220.87/31.75 % (3539809)CaDiCaL version: 2.1.3 % 220.87/31.75 % (3539809)Termination reason: Instruction limit % 220.87/31.75 % (3539809)Termination phase: Saturation % 225.35/32.31 % (3539809)Time elapsed: 0.419 s % 225.35/32.31 % (3539809)Peak memory usage: 124 MB % 225.35/32.31 % (3539809)Instructions burned: 402 (million) % 225.35/32.31 % (3539804)------------------------------ % 225.35/32.31 % (3539804)------------------------------ % 225.35/32.31 % (3539814)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=247922145:i=8:rtra=on_2697 on theBenchmark for (2697ds/8Mi) % 225.35/32.31 % (3539814)Instruction limit reached! % 225.35/32.31 % (3539814)------------------------------ % 225.35/32.31 % (3539814)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 225.35/32.31 % (3539814)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 225.35/32.31 % (3539814)CaDiCaL version: 2.1.3 % 225.35/32.31 % (3539814)Termination reason: Instruction limit % 225.35/32.31 % (3539814)Termination phase: Property scanning % 225.35/32.31 % (3539814)Time elapsed: 0.009 s % 225.35/32.31 % (3539814)Peak memory usage: 86 MB % 225.35/32.31 % (3539814)Instructions burned: 8 (million) % 225.35/32.31 % (3539815)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=620352054:i=92:rtra=on_2696 on theBenchmark for (2696ds/92Mi) % 225.35/32.31 % (3539817)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=315661008:st=5:i=28:sd=10:rtra=on:ss=axioms:rawr=on_2696 on theBenchmark for (2696ds/28Mi) % 225.35/32.31 % (3539816)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=3669640610:i=66:rtra=on_2696 on theBenchmark for (2696ds/66Mi) % 225.35/32.31 % (3539817)Instruction limit reached! % 225.35/32.31 % (3539817)------------------------------ % 225.35/32.31 % (3539817)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 225.35/32.31 % (3539817)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 225.35/32.31 % (3539817)CaDiCaL version: 2.1.3 % 225.35/32.31 % (3539817)Termination reason: Instruction limit % 225.35/32.31 % (3539817)Termination phase: Preprocessing 1 % 225.35/32.31 % (3539817)Time elapsed: 0.024 s % 225.35/32.31 % (3539817)Peak memory usage: 86 MB % 225.35/32.31 % (3539817)Instructions burned: 28 (million) % 225.35/32.31 % (3539815)Instruction limit reached! % 225.35/32.31 % (3539815)------------------------------ % 225.35/32.31 % (3539815)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 225.35/32.31 % (3539815)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 225.35/32.31 % (3539815)CaDiCaL version: 2.1.3 % 225.35/32.31 % (3539815)Termination reason: Instruction limit % 225.35/32.31 % (3539815)Termination phase: Property scanning % 225.35/32.31 % (3539815)Time elapsed: 0.086 s % 225.35/32.31 % (3539815)Peak memory usage: 91 MB % 225.35/32.31 % (3539815)Instructions burned: 93 (million) % 225.35/32.31 % (3539816)Instruction limit reached! % 225.35/32.31 % (3539816)------------------------------ % 225.35/32.31 % (3539816)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 225.35/32.31 % (3539816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 225.35/32.31 % (3539816)CaDiCaL version: 2.1.3 % 225.35/32.31 % (3539816)Termination reason: Instruction limit % 225.35/32.31 % (3539816)Termination phase: Preprocessing 2 % 225.35/32.31 % (3539816)Time elapsed: 0.058 s % 225.35/32.31 % (3539816)Peak memory usage: 90 MB % 225.35/32.31 % (3539816)Instructions burned: 66 (million) % 225.35/32.31 % (3539819)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=1898485231:i=58:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2694 on theBenchmark for (2694ds/58Mi) % 225.35/32.31 % (3539819)Instruction limit reached! % 225.35/32.31 % (3539819)------------------------------ % 225.35/32.31 % (3539819)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 225.35/32.31 % (3539819)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 225.35/32.31 % (3539819)CaDiCaL version: 2.1.3 % 225.35/32.31 % (3539819)Termination reason: Instruction limit % 225.35/32.31 % (3539819)Termination phase: Preprocessing 2 % 225.35/32.31 % (3539819)Time elapsed: 0.053 s % 225.35/32.31 % (3539819)Peak memory usage: 89 MB % 225.35/32.31 % (3539819)Instructions burned: 58 (million) % 225.35/32.31 % (3539823)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=2306059386:cond=on:i=32:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2693 on theBenchmark for (2693ds/32Mi) % 225.35/32.31 % (3539824)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=2174896599:i=48:canc=force:rtra=on_2693 on theBenchmark for (2693ds/48Mi) % 225.35/32.31 % (3539823)Instruction limit reached! % 225.35/32.31 % (3539823)------------------------------ % 225.35/32.31 % (3539823)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 228.44/32.78 % (3539823)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 228.44/32.78 % (3539823)CaDiCaL version: 2.1.3 % 228.44/32.78 % (3539823)Termination reason: Instruction limit % 228.44/32.78 % (3539823)Termination phase: Preprocessing 1 % 228.44/32.78 % (3539823)Time elapsed: 0.030 s % 228.44/32.78 % (3539823)Peak memory usage: 87 MB % 228.44/32.78 % (3539823)Instructions burned: 33 (million) % 228.44/32.78 % (3539825)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=3508787759:i=54:canc=cautious:fsr=off:rtra=on_2693 on theBenchmark for (2693ds/54Mi) % 228.44/32.78 % (3539824)Instruction limit reached! % 228.44/32.78 % (3539824)------------------------------ % 228.44/32.78 % (3539824)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 228.44/32.78 % (3539824)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 228.44/32.78 % (3539824)CaDiCaL version: 2.1.3 % 228.44/32.78 % (3539824)Termination reason: Instruction limit % 228.44/32.78 % (3539824)Termination phase: Preprocessing 1 % 228.44/32.78 % (3539824)Time elapsed: 0.044 s % 228.44/32.78 % (3539824)Peak memory usage: 88 MB % 228.44/32.78 % (3539824)Instructions burned: 48 (million) % 228.44/32.78 % (3539825)Instruction limit reached! % 228.44/32.78 % (3539825)------------------------------ % 228.44/32.78 % (3539825)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 228.44/32.78 % (3539825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 228.44/32.78 % (3539825)CaDiCaL version: 2.1.3 % 228.44/32.78 % (3539825)Termination reason: Instruction limit % 228.44/32.78 % (3539825)Termination phase: Unused predicate definition removal % 228.44/32.78 % (3539825)Time elapsed: 0.044 s % 228.44/32.78 % (3539825)Peak memory usage: 88 MB % 228.44/32.78 % (3539825)Instructions burned: 54 (million) % 228.44/32.78 % (3539830)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=1685344046:i=4:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2690 on theBenchmark for (2690ds/4Mi) % 228.44/32.78 % (3539827)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=3003990992:i=170:gtgl=4:rtra=on:gtg=exists_sym_2691 on theBenchmark for (2691ds/170Mi) % 228.44/32.78 % (3539830)Instruction limit reached! % 228.44/32.78 % (3539830)------------------------------ % 228.44/32.78 % (3539830)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 228.44/32.78 % (3539830)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 228.44/32.78 % (3539830)CaDiCaL version: 2.1.3 % 228.44/32.78 % (3539830)Termination reason: Instruction limit % 228.44/32.78 % (3539830)Termination phase: shuffling % 228.44/32.78 % (3539830)Time elapsed: 0.003 s % 228.44/32.78 % (3539830)Peak memory usage: 86 MB % 228.44/32.78 % (3539830)Instructions burned: 4 (million) % 228.44/32.78 % (3539832)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=1581298175:i=362:rtra=on:ss=axioms:ev=cautious_2690 on theBenchmark for (2690ds/362Mi) % 228.44/32.78 % (3539827)Instruction limit reached! % 228.44/32.78 % (3539827)------------------------------ % 228.44/32.78 % (3539827)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 228.44/32.78 % (3539827)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 228.44/32.78 % (3539827)CaDiCaL version: 2.1.3 % 228.44/32.78 % (3539827)Termination reason: Instruction limit % 228.44/32.78 % (3539827)Termination phase: Saturation % 228.44/32.78 % (3539827)Time elapsed: 0.150 s % 228.44/32.78 % (3539827)Peak memory usage: 94 MB % 228.44/32.78 % (3539827)Instructions burned: 171 (million) % 228.44/32.78 % (3539833)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=955064464:i=8:ep=RST:ins=2:rtra=on_2689 on theBenchmark for (2689ds/8Mi) % 228.44/32.78 % (3539833)Instruction limit reached! % 228.44/32.78 % (3539833)------------------------------ % 228.44/32.78 % (3539833)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 228.44/32.78 % (3539833)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 228.44/32.78 % (3539833)CaDiCaL version: 2.1.3 % 228.44/32.78 % (3539833)Termination reason: Instruction limit % 228.44/32.78 % (3539833)Termination phase: Property scanning % 228.44/32.78 % (3539833)Time elapsed: 0.009 s % 228.44/32.78 % (3539833)Peak memory usage: 86 MB % 228.44/32.78 % (3539833)Instructions burned: 9 (million) % 228.44/32.78 % (3539836)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=2261845933:i=132:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2688 on theBenchmark for (2688ds/132Mi) % 232.86/33.35 % (3539839)lrs+10_1_thi=all:si=on:fd=off:random_seed=1205654300:i=106:rtra=on:gtg=all_2687 on theBenchmark for (2687ds/106Mi) % 232.86/33.35 % (3539836)Instruction limit reached! % 232.86/33.35 % (3539836)------------------------------ % 232.86/33.35 % (3539836)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 232.86/33.35 % (3539836)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 232.86/33.35 % (3539836)CaDiCaL version: 2.1.3 % 232.86/33.35 % (3539836)Termination reason: Instruction limit % 232.86/33.35 % (3539836)Termination phase: Saturation % 232.86/33.35 % (3539836)Time elapsed: 0.181 s % 232.86/33.35 % (3539836)Peak memory usage: 135 MB % 232.86/33.35 % (3539836)Instructions burned: 133 (million) % 232.86/33.35 % (3539841)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=846276789:i=16:ep=RST:nm=16:rtra=on:gtg=exists_top_2686 on theBenchmark for (2686ds/16Mi) % 232.86/33.35 % (3539832)Instruction limit reached! % 232.86/33.35 % (3539832)------------------------------ % 232.86/33.35 % (3539832)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 232.86/33.35 % (3539832)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 232.86/33.35 % (3539832)CaDiCaL version: 2.1.3 % 232.86/33.35 % (3539832)Termination reason: Instruction limit % 232.86/33.35 % (3539832)Termination phase: Saturation % 232.86/33.35 % (3539832)Time elapsed: 0.327 s % 232.86/33.35 % (3539832)Peak memory usage: 99 MB % 232.86/33.35 % (3539832)Instructions burned: 362 (million) % 232.86/33.35 % (3539841)Instruction limit reached! % 232.86/33.35 % (3539841)------------------------------ % 232.86/33.35 % (3539841)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 232.86/33.35 % (3539841)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 232.86/33.35 % (3539841)CaDiCaL version: 2.1.3 % 232.86/33.35 % (3539841)Termination reason: Instruction limit % 232.86/33.35 % (3539841)Termination phase: shuffling % 232.86/33.35 % (3539841)Time elapsed: 0.015 s % 232.86/33.35 % (3539841)Peak memory usage: 86 MB % 232.86/33.35 % (3539841)Instructions burned: 16 (million) % 232.86/33.35 % (3539839)Instruction limit reached! % 232.86/33.35 % (3539839)------------------------------ % 232.86/33.35 % (3539839)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 232.86/33.35 % (3539839)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 232.86/33.35 % (3539839)CaDiCaL version: 2.1.3 % 232.86/33.35 % (3539839)Termination reason: Instruction limit % 232.86/33.35 % (3539839)Termination phase: Preprocessing 3 % 232.86/33.35 % (3539839)Time elapsed: 0.092 s % 232.86/33.35 % (3539839)Peak memory usage: 90 MB % 232.86/33.35 % (3539839)Instructions burned: 107 (million) % 232.86/33.35 % (3539845)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=1068949234:st=3:i=4:rtra=on:ss=axioms_2684 on theBenchmark for (2684ds/4Mi) % 232.86/33.35 % (3539845)Instruction limit reached! % 232.86/33.35 % (3539845)------------------------------ % 232.86/33.35 % (3539845)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 232.86/33.35 % (3539845)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 232.86/33.35 % (3539845)CaDiCaL version: 2.1.3 % 232.86/33.35 % (3539845)Termination reason: Instruction limit % 232.86/33.35 % (3539845)Termination phase: shuffling % 232.86/33.35 % (3539845)Time elapsed: 0.005 s % 232.86/33.35 % (3539845)Peak memory usage: 85 MB % 232.86/33.35 % (3539845)Instructions burned: 4 (million) % 232.86/33.35 % (3539848)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=3784691498:i=254:doe=on:rtra=on_2683 on theBenchmark for (2683ds/254Mi) % 232.86/33.35 % (3539847)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=979805526:i=4:doe=on:canc=force:asg=cautious:rtra=on_2684 on theBenchmark for (2684ds/4Mi) % 232.86/33.35 % (3539847)Instruction limit reached! % 232.86/33.35 % (3539847)------------------------------ % 232.86/33.35 % (3539847)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 232.86/33.35 % (3539847)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 232.86/33.35 % (3539847)CaDiCaL version: 2.1.3 % 232.86/33.35 % (3539847)Termination reason: Instruction limit % 232.86/33.35 % (3539847)Termination phase: shuffling % 232.86/33.35 % (3539847)Time elapsed: 0.005 s % 232.86/33.35 % (3539847)Peak memory usage: 85 MB % 232.86/33.35 % (3539847)Instructions burned: 4 (million) % 232.86/33.35 % (3539849)dis+10_1_si=on:random_seed=3949745866:i=20:ep=R:rtra=on_2683 on theBenchmark for (2683ds/20Mi) % 239.60/34.28 % (3539849)Instruction limit reached! % 239.60/34.28 % (3539849)------------------------------ % 239.60/34.28 % (3539849)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 239.60/34.28 % (3539849)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 239.60/34.28 % (3539849)CaDiCaL version: 2.1.3 % 239.60/34.28 % (3539849)Termination reason: Instruction limit % 239.60/34.28 % (3539849)Termination phase: Property scanning % 239.60/34.28 % (3539849)Time elapsed: 0.018 s % 239.60/34.28 % (3539849)Peak memory usage: 86 MB % 239.60/34.28 % (3539849)Instructions burned: 20 (million) % 239.60/34.28 % (3539851)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=3594577977:i=52:canc=cautious:av=off:rtra=on_2681 on theBenchmark for (2681ds/52Mi) % 239.60/34.28 % (3539857)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=2606597535:i=4:fsr=off:rtra=on:inst=on_2680 on theBenchmark for (2680ds/4Mi) % 239.60/34.28 % (3539857)Instruction limit reached! % 239.60/34.28 % (3539857)------------------------------ % 239.60/34.28 % (3539857)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 239.60/34.28 % (3539857)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 239.60/34.28 % (3539857)CaDiCaL version: 2.1.3 % 239.60/34.28 % (3539857)Termination reason: Instruction limit % 239.60/34.28 % (3539857)Termination phase: shuffling % 239.60/34.28 % (3539857)Time elapsed: 0.004 s % 239.60/34.28 % (3539857)Peak memory usage: 86 MB % 239.60/34.28 % (3539857)Instructions burned: 4 (million) % 239.60/34.28 % (3539848)Instruction limit reached! % 239.60/34.28 % (3539848)------------------------------ % 239.60/34.28 % (3539848)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 239.60/34.28 % (3539848)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 239.60/34.28 % (3539848)CaDiCaL version: 2.1.3 % 239.60/34.28 % (3539848)Termination reason: Instruction limit % 239.60/34.28 % (3539848)Termination phase: Saturation % 239.60/34.28 % (3539848)Time elapsed: 0.230 s % 239.60/34.28 % (3539848)Peak memory usage: 119 MB % 239.60/34.28 % (3539848)Instructions burned: 254 (million) % 239.60/34.28 % (3539851)Instruction limit reached! % 239.60/34.28 % (3539851)------------------------------ % 239.60/34.28 % (3539851)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 239.60/34.28 % (3539851)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 239.60/34.28 % (3539851)CaDiCaL version: 2.1.3 % 239.60/34.28 % (3539851)Termination reason: Instruction limit % 239.60/34.28 % (3539851)Termination phase: shuffling % 239.60/34.28 % (3539851)Time elapsed: 0.045 s % 239.60/34.28 % (3539851)Peak memory usage: 88 MB % 239.60/34.28 % (3539851)Instructions burned: 52 (million) % 239.60/34.28 % (3539854)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=119303664: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_2681 on theBenchmark for (2681ds/70Mi) % 239.60/34.28 % (3539854)Instruction limit reached! % 239.60/34.28 % (3539854)------------------------------ % 239.60/34.28 % (3539854)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 239.60/34.28 % (3539854)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 239.60/34.28 % (3539854)CaDiCaL version: 2.1.3 % 239.60/34.28 % (3539854)Termination reason: Instruction limit % 239.60/34.28 % (3539854)Termination phase: Preprocessing 2 % 239.60/34.28 % (3539854)Time elapsed: 0.062 s % 239.60/34.28 % (3539854)Peak memory usage: 90 MB % 239.60/34.28 % (3539854)Instructions burned: 70 (million) % 239.60/34.28 % (3539861)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=936123731:s2a=on:i=16:kws=inv_precedence:doe=on:rtra=on_2679 on theBenchmark for (2679ds/16Mi) % 239.60/34.28 % (3539861)Instruction limit reached! % 239.60/34.28 % (3539861)------------------------------ % 239.60/34.28 % (3539861)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 239.60/34.28 % (3539861)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 239.60/34.28 % (3539861)CaDiCaL version: 2.1.3 % 239.60/34.28 % (3539861)Termination reason: Instruction limit % 239.60/34.28 % (3539861)Termination phase: Property scanning % 239.60/34.28 % (3539861)Time elapsed: 0.015 s % 239.60/34.28 % (3539861)Peak memory usage: 86 MB % 239.60/34.28 % (3539861)Instructions burned: 17 (million) % 239.60/34.28 % (3539864)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=1493584168:i=26:av=off:rtra=on:gtg=exists_sym:ev=force_2678 on theBenchmark for (2678ds/26Mi) % 248.98/35.67 % (3539864)Instruction limit reached! % 248.98/35.67 % (3539864)------------------------------ % 248.98/35.67 % (3539864)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 248.98/35.67 % (3539864)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 248.98/35.67 % (3539864)CaDiCaL version: 2.1.3 % 248.98/35.67 % (3539864)Termination reason: Instruction limit % 248.98/35.67 % (3539864)Termination phase: Property scanning % 248.98/35.67 % (3539864)Time elapsed: 0.014 s % 248.98/35.67 % (3539864)Peak memory usage: 85 MB % 248.98/35.67 % (3539864)Instructions burned: 28 (million) % 248.98/35.67 % (3539863)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=3962410426:i=740:ep=RS:fsr=off:rtra=on_2678 on theBenchmark for (2678ds/740Mi) % 248.98/35.67 % (3539865)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=921600875:i=452:rtra=on:gtg=position:ss=axioms_2678 on theBenchmark for (2678ds/452Mi) % 248.98/35.67 % (3539863)Refutation not found, incomplete strategy % 248.98/35.67 % (3539863)------------------------------ % 248.98/35.67 % (3539863)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 248.98/35.67 % (3539863)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 248.98/35.67 % (3539863)CaDiCaL version: 2.1.3 % 248.98/35.67 % (3539863)Termination reason: Refutation not found, incomplete strategy % 248.98/35.67 % (3539863)Time elapsed: 0.168 s % 248.98/35.67 % (3539863)Peak memory usage: 96 MB % 248.98/35.67 % (3539863)Instructions burned: 187 (million) % 248.98/35.67 % (3539870)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=990696109:i=142:rtra=on:gtg=exists_top_2676 on theBenchmark for (2676ds/142Mi) % 248.98/35.67 % (3539867)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=3101050666:i=20:rtra=on_2676 on theBenchmark for (2676ds/20Mi) % 248.98/35.67 % (3539867)Instruction limit reached! % 248.98/35.67 % (3539867)------------------------------ % 248.98/35.67 % (3539867)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 248.98/35.67 % (3539867)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 248.98/35.67 % (3539867)CaDiCaL version: 2.1.3 % 248.98/35.67 % (3539867)Termination reason: Instruction limit % 248.98/35.67 % (3539867)Termination phase: Property scanning % 248.98/35.67 % (3539867)Time elapsed: 0.017 s % 248.98/35.67 % (3539867)Peak memory usage: 86 MB % 248.98/35.67 % (3539867)Instructions burned: 20 (million) % 248.98/35.67 % (3539870)Instruction limit reached! % 248.98/35.67 % (3539870)------------------------------ % 248.98/35.67 % (3539870)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 248.98/35.67 % (3539870)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 248.98/35.67 % (3539870)CaDiCaL version: 2.1.3 % 248.98/35.67 % (3539870)Termination reason: Instruction limit % 248.98/35.67 % (3539870)Termination phase: Saturation % 248.98/35.67 % (3539870)Time elapsed: 0.207 s % 248.98/35.67 % (3539870)Peak memory usage: 134 MB % 248.98/35.67 % (3539870)Instructions burned: 142 (million) % 248.98/35.67 % (3539865)Instruction limit reached! % 248.98/35.67 % (3539865)------------------------------ % 248.98/35.67 % (3539865)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 248.98/35.67 % (3539865)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 248.98/35.67 % (3539865)CaDiCaL version: 2.1.3 % 248.98/35.67 % (3539865)Termination reason: Instruction limit % 248.98/35.67 % (3539865)Termination phase: Saturation % 248.98/35.67 % (3539865)Time elapsed: 0.382 s % 248.98/35.67 % (3539865)Peak memory usage: 124 MB % 248.98/35.67 % (3539865)Instructions burned: 452 (million) % 248.98/35.67 % (3539874)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=2206973205:i=150:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2673 on theBenchmark for (2673ds/150Mi) % 248.98/35.67 % (3539874)Instruction limit reached! % 248.98/35.67 % (3539874)------------------------------ % 248.98/35.67 % (3539874)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 248.98/35.67 % (3539874)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 248.98/35.67 % (3539874)CaDiCaL version: 2.1.3 % 248.98/35.67 % (3539874)Termination reason: Instruction limit % 248.98/35.67 % (3539874)Termination phase: Saturation % 248.98/35.67 % (3539874)Time elapsed: 0.096 s % 248.98/35.67 % (3539874)Peak memory usage: 96 MB % 248.98/35.67 % (3539874)Instructions burned: 150 (million) % 248.98/35.67 % (3539863)------------------------------ % 248.98/35.67 % (3539863)------------------------------ % 256.97/36.89 % (3539875)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=3319980585:i=588:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2671 on theBenchmark for (2671ds/588Mi) % 256.97/36.89 % (3539876)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=17015272:i=260:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2671 on theBenchmark for (2671ds/260Mi) % 256.97/36.89 % (3539878)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=2657379109:i=262:rtra=on_2670 on theBenchmark for (2670ds/262Mi) % 256.97/36.89 % (3539879)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=948152432:i=80:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2670 on theBenchmark for (2670ds/80Mi) % 256.97/36.89 % (3539878)Instruction limit reached! % 256.97/36.89 % (3539878)------------------------------ % 256.97/36.89 % (3539878)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 256.97/36.89 % (3539878)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 256.97/36.89 % (3539878)CaDiCaL version: 2.1.3 % 256.97/36.89 % (3539878)Termination reason: Instruction limit % 256.97/36.89 % (3539878)Termination phase: Saturation % 256.97/36.89 % (3539878)Time elapsed: 0.195 s % 256.97/36.89 % (3539878)Peak memory usage: 136 MB % 256.97/36.89 % (3539878)Instructions burned: 265 (million) % 256.97/36.89 % (3539876)Instruction limit reached! % 256.97/36.89 % (3539876)------------------------------ % 256.97/36.89 % (3539876)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 256.97/36.89 % (3539876)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 256.97/36.89 % (3539876)CaDiCaL version: 2.1.3 % 256.97/36.89 % (3539876)Termination reason: Instruction limit % 256.97/36.89 % (3539876)Termination phase: Saturation % 256.97/36.89 % (3539876)Time elapsed: 0.236 s % 256.97/36.89 % (3539876)Peak memory usage: 118 MB % 256.97/36.89 % (3539876)Instructions burned: 260 (million) % 256.97/36.89 % (3539879)Instruction limit reached! % 256.97/36.89 % (3539879)------------------------------ % 256.97/36.89 % (3539879)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 256.97/36.89 % (3539879)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 256.97/36.89 % (3539879)CaDiCaL version: 2.1.3 % 256.97/36.89 % (3539879)Termination reason: Instruction limit % 256.97/36.89 % (3539879)Termination phase: Preprocessing 1 % 256.97/36.89 % (3539879)Time elapsed: 0.068 s % 256.97/36.89 % (3539879)Peak memory usage: 88 MB % 256.97/36.89 % (3539879)Instructions burned: 80 (million) % 256.97/36.89 % (3539886)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=4067491708:i=262:canc=cautious:fsr=off:rtra=on_2666 on theBenchmark for (2666ds/262Mi) % 256.97/36.89 % (3539884)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=2534856284:i=614:rtra=on:gtg=exists_top_2666 on theBenchmark for (2666ds/614Mi) % 256.97/36.89 % (3539875)Instruction limit reached! % 256.97/36.89 % (3539875)------------------------------ % 256.97/36.89 % (3539875)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 256.97/36.89 % (3539875)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 256.97/36.89 % (3539875)CaDiCaL version: 2.1.3 % 256.97/36.89 % (3539875)Termination reason: Instruction limit % 256.97/36.89 % (3539875)Termination phase: Saturation % 256.97/36.89 % (3539875)Time elapsed: 0.501 s % 256.97/36.89 % (3539875)Peak memory usage: 96 MB % 256.97/36.89 % (3539875)Instructions burned: 588 (million) % 256.97/36.89 % (3539885)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=1757154027:s2a=on:i=1196:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2666 on theBenchmark for (2666ds/1196Mi) % 256.97/36.89 % (3539886)Instruction limit reached! % 256.97/36.89 % (3539886)------------------------------ % 256.97/36.89 % (3539886)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 256.97/36.89 % (3539886)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 256.97/36.89 % (3539886)CaDiCaL version: 2.1.3 % 256.97/36.89 % (3539886)Termination reason: Instruction limit % 256.97/36.89 % (3539886)Termination phase: Saturation % 256.97/36.89 % (3539886)Time elapsed: 0.238 s % 256.97/36.89 % (3539886)Peak memory usage: 118 MB % 256.97/36.89 % (3539886)Instructions burned: 263 (million) % 256.97/36.89 % (3539889)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=3716215290:s2pl=no:i=518:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2664 on theBenchmark for (2664ds/518Mi) % 263.51/37.98 % (3539884)Instruction limit reached! % 263.51/37.98 % (3539884)------------------------------ % 263.51/37.98 % (3539884)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 263.51/37.98 % (3539884)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 263.51/37.98 % (3539884)CaDiCaL version: 2.1.3 % 263.51/37.98 % (3539884)Termination reason: Instruction limit % 263.51/37.98 % (3539884)Termination phase: Saturation % 263.51/37.98 % (3539884)Time elapsed: 0.520 s % 263.51/37.98 % (3539884)Peak memory usage: 97 MB % 263.51/37.98 % (3539884)Instructions burned: 614 (million) % 263.51/37.98 % (3539891)dis+10_1_si=on:random_seed=2920918909:s2a=on:i=2000:rtra=on:gtg=exists_all_2662 on theBenchmark for (2662ds/2000Mi) % 263.51/37.98 % (3539893)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=674031717:i=766:fsr=off:rtra=on:ev=force_2659 on theBenchmark for (2659ds/766Mi) % 263.51/37.98 % (3539889)Instruction limit reached! % 263.51/37.98 % (3539889)------------------------------ % 263.51/37.98 % (3539889)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 263.51/37.98 % (3539889)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 263.51/37.98 % (3539889)CaDiCaL version: 2.1.3 % 263.51/37.98 % (3539889)Termination reason: Instruction limit % 263.51/37.98 % (3539889)Termination phase: Saturation % 263.51/37.98 % (3539889)Time elapsed: 0.506 s % 263.51/37.98 % (3539889)Peak memory usage: 124 MB % 263.51/37.98 % (3539889)Instructions burned: 519 (million) % 263.51/37.98 % (3539896)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=3349944627:i=282:doe=on:rtra=on_2656 on theBenchmark for (2656ds/282Mi) % 263.51/37.98 % (3539885)Instruction limit reached! % 263.51/37.98 % (3539885)------------------------------ % 263.51/37.98 % (3539885)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 263.51/37.98 % (3539885)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 263.51/37.98 % (3539885)CaDiCaL version: 2.1.3 % 263.51/37.98 % (3539885)Termination reason: Instruction limit % 263.51/37.98 % (3539885)Termination phase: Saturation % 263.51/37.98 % (3539885)Time elapsed: 1.064 s % 263.51/37.98 % (3539885)Peak memory usage: 142 MB % 263.51/37.98 % (3539885)Instructions burned: 1197 (million) % 263.51/37.98 % (3539893)Refutation not found, incomplete strategy % 263.51/37.98 % (3539893)------------------------------ % 263.51/37.98 % (3539893)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 263.51/37.98 % (3539893)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 263.51/37.98 % (3539893)CaDiCaL version: 2.1.3 % 263.51/37.98 % (3539893)Termination reason: Refutation not found, incomplete strategy % 263.51/37.98 % (3539893)Time elapsed: 0.591 s % 263.51/37.98 % (3539893)Peak memory usage: 108 MB % 263.51/37.98 % (3539893)Instructions burned: 740 (million) % 263.51/37.98 % (3539898)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=1310870847:i=130:nm=16:rtra=on_2653 on theBenchmark for (2653ds/130Mi) % 263.51/37.98 % (3539896)Instruction limit reached! % 263.51/37.98 % (3539896)------------------------------ % 263.51/37.98 % (3539896)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 263.51/37.98 % (3539896)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 263.51/37.98 % (3539896)CaDiCaL version: 2.1.3 % 263.51/37.98 % (3539896)Termination reason: Instruction limit % 263.51/37.98 % (3539896)Termination phase: Saturation % 263.51/37.98 % (3539896)Time elapsed: 0.242 s % 263.51/37.98 % (3539896)Peak memory usage: 96 MB % 263.51/37.98 % (3539896)Instructions burned: 283 (million) % 263.51/37.98 % (3539898)Instruction limit reached! % 263.51/37.98 % (3539898)------------------------------ % 263.51/37.98 % (3539898)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 263.51/37.98 % (3539898)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 263.51/37.98 % (3539898)CaDiCaL version: 2.1.3 % 263.51/37.98 % (3539898)Termination reason: Instruction limit % 263.51/37.98 % (3539898)Termination phase: Saturation % 263.51/37.98 % (3539898)Time elapsed: 0.104 s % 263.51/37.98 % (3539898)Peak memory usage: 117 MB % 263.51/37.98 % (3539898)Instructions burned: 130 (million) % 263.51/37.98 % (3539900)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=227044714:i=242:nm=16:rtra=on_2650 on theBenchmark for (2650ds/242Mi) % 263.51/37.98 % (3539893)------------------------------ % 263.51/37.98 % (3539893)------------------------------ % 263.51/37.98 % (3539901)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=1513363353:s2a=on:i=256:s2at=5:ins=3:rtra=on_2649 on theBenchmark for (2649ds/256Mi) % 275.77/39.48 % (3539900)Instruction limit reached! % 275.77/39.48 % (3539900)------------------------------ % 275.77/39.48 % (3539900)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 275.77/39.48 % (3539900)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 275.77/39.48 % (3539900)CaDiCaL version: 2.1.3 % 275.77/39.48 % (3539900)Termination reason: Instruction limit % 275.77/39.48 % (3539900)Termination phase: Saturation % 275.77/39.48 % (3539900)Time elapsed: 0.215 s % 275.77/39.48 % (3539900)Peak memory usage: 95 MB % 275.77/39.48 % (3539900)Instructions burned: 242 (million) % 275.77/39.48 % (3539904)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=2980515635:i=78:ins=3:rtra=on_2647 on theBenchmark for (2647ds/78Mi) % 275.77/39.48 % (3539901)Instruction limit reached! % 275.77/39.48 % (3539901)------------------------------ % 275.77/39.48 % (3539901)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 275.77/39.48 % (3539901)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 275.77/39.48 % (3539901)CaDiCaL version: 2.1.3 % 275.77/39.48 % (3539901)Termination reason: Instruction limit % 275.77/39.48 % (3539901)Termination phase: Saturation % 275.77/39.48 % (3539901)Time elapsed: 0.266 s % 275.77/39.48 % (3539901)Peak memory usage: 123 MB % 275.77/39.48 % (3539901)Instructions burned: 256 (million) % 275.77/39.48 % (3539904)Instruction limit reached! % 275.77/39.48 % (3539904)------------------------------ % 275.77/39.48 % (3539904)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 275.77/39.48 % (3539904)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 275.77/39.48 % (3539904)CaDiCaL version: 2.1.3 % 275.77/39.48 % (3539904)Termination reason: Instruction limit % 275.77/39.48 % (3539904)Termination phase: Preprocessing 3 % 275.77/39.48 % (3539904)Time elapsed: 0.071 s % 275.77/39.48 % (3539904)Peak memory usage: 90 MB % 275.77/39.48 % (3539904)Instructions burned: 79 (million) % 275.77/39.48 % (3539905)dis+1010_1_to=kbo:si=on:random_seed=1819672062:i=350:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2645 on theBenchmark for (2645ds/350Mi) % 275.77/39.48 % (3539907)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=2272362941:i=658:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2644 on theBenchmark for (2644ds/658Mi) % 275.77/39.48 % (3539891)Instruction limit reached! % 275.77/39.48 % (3539891)------------------------------ % 275.77/39.48 % (3539891)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 275.77/39.48 % (3539891)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 275.77/39.48 % (3539891)CaDiCaL version: 2.1.3 % 275.77/39.48 % (3539891)Termination reason: Instruction limit % 275.77/39.48 % (3539891)Termination phase: Saturation % 275.77/39.48 % (3539891)Time elapsed: 1.752 s % 275.77/39.48 % (3539891)Peak memory usage: 105 MB % 275.77/39.48 % (3539891)Instructions burned: 2001 (million) % 275.77/39.48 % (3539908)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=1794536071:s2a=on:i=966:doe=on:nm=32:rtra=on_2644 on theBenchmark for (2644ds/966Mi) % 275.77/39.48 % (3539905)Instruction limit reached! % 275.77/39.48 % (3539905)------------------------------ % 275.77/39.48 % (3539905)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 275.77/39.48 % (3539905)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 275.77/39.48 % (3539905)CaDiCaL version: 2.1.3 % 275.77/39.48 % (3539905)Termination reason: Instruction limit % 275.77/39.48 % (3539905)Termination phase: Saturation % 275.77/39.48 % (3539905)Time elapsed: 0.315 s % 275.77/39.48 % (3539905)Peak memory usage: 99 MB % 275.77/39.48 % (3539905)Instructions burned: 351 (million) % 275.77/39.48 % (3539912)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=773218920:thitd=on:i=430:nm=0:rtra=on:ev=force_2641 on theBenchmark for (2641ds/430Mi) % 275.77/39.48 % (3539915)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=3550356768:i=698:rtra=on_2640 on theBenchmark for (2640ds/698Mi) % 275.77/39.48 % (3539907)Instruction limit reached! % 275.77/39.48 % (3539907)------------------------------ % 275.77/39.48 % (3539907)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 275.77/39.48 % (3539907)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.31/40.35 % (3539907)CaDiCaL version: 2.1.3 % 282.31/40.35 % (3539907)Termination reason: Instruction limit % 282.31/40.35 % (3539907)Termination phase: Saturation % 282.31/40.35 % (3539907)Time elapsed: 0.673 s % 282.31/40.35 % (3539907)Peak memory usage: 125 MB % 282.31/40.35 % (3539907)Instructions burned: 658 (million) % 282.31/40.35 % (3539912)Instruction limit reached! % 282.31/40.35 % (3539912)------------------------------ % 282.31/40.35 % (3539912)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 282.31/40.35 % (3539912)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.31/40.35 % (3539912)CaDiCaL version: 2.1.3 % 282.31/40.35 % (3539912)Termination reason: Instruction limit % 282.31/40.35 % (3539912)Termination phase: Saturation % 282.31/40.35 % (3539912)Time elapsed: 0.444 s % 282.31/40.35 % (3539912)Peak memory usage: 151 MB % 282.31/40.35 % (3539912)Instructions burned: 431 (million) % 282.31/40.35 % (3539915)Refutation not found, incomplete strategy % 282.31/40.35 % (3539915)------------------------------ % 282.31/40.35 % (3539915)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 282.31/40.35 % (3539915)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.31/40.35 % (3539915)CaDiCaL version: 2.1.3 % 282.31/40.35 % (3539915)Termination reason: Refutation not found, incomplete strategy % 282.31/40.35 % (3539915)Time elapsed: 0.434 s % 282.31/40.35 % (3539915)Peak memory usage: 125 MB % 282.31/40.35 % (3539915)Instructions burned: 497 (million) % 282.31/40.35 % (3539918)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=3266183446:st=2:i=590:rtra=on:ss=axioms_2635 on theBenchmark for (2635ds/590Mi) % 282.31/40.35 % (3539919)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=664360015:i=656:kws=inv_frequency:nm=20:rtra=on_2634 on theBenchmark for (2634ds/656Mi) % 282.31/40.35 % (3539908)Instruction limit reached! % 282.31/40.35 % (3539908)------------------------------ % 282.31/40.35 % (3539908)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 282.31/40.35 % (3539908)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.31/40.35 % (3539908)CaDiCaL version: 2.1.3 % 282.31/40.35 % (3539908)Termination reason: Instruction limit % 282.31/40.35 % (3539908)Termination phase: Saturation % 282.31/40.35 % (3539908)Time elapsed: 1.009 s % 282.31/40.35 % (3539908)Peak memory usage: 143 MB % 282.31/40.35 % (3539908)Instructions burned: 966 (million) % 282.31/40.35 % (3539915)------------------------------ % 282.31/40.35 % (3539915)------------------------------ % 282.31/40.35 % (3539922)dis+1010_1_to=lpo:sil=128000:sas=z3:si=on:nwc=5:random_seed=1931273481:i=562:gtgl=2:rtra=on:gtg=all_2631 on theBenchmark for (2631ds/562Mi) % 282.31/40.35 % (3539918)Instruction limit reached! % 282.31/40.35 % (3539918)------------------------------ % 282.31/40.35 % (3539918)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 282.31/40.35 % (3539918)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.31/40.35 % (3539918)CaDiCaL version: 2.1.3 % 282.31/40.35 % (3539918)Termination reason: Instruction limit % 282.31/40.35 % (3539918)Termination phase: Saturation % 282.31/40.35 % (3539918)Time elapsed: 0.492 s % 282.31/40.35 % (3539918)Peak memory usage: 98 MB % 282.31/40.35 % (3539918)Instructions burned: 591 (million) % 282.31/40.35 % (3539923)lrs+1010_1_to=kbo:sil=128000:si=on:sos=on:urr=on:uwa=alasca_main:random_seed=3895536660:i=968:doe=on:nm=0:av=off:rtra=on:ss=axioms_2629 on theBenchmark for (2629ds/968Mi) % 282.31/40.35 % (3539919)Instruction limit reached! % 282.31/40.35 % (3539919)------------------------------ % 282.31/40.35 % (3539919)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 282.31/40.35 % (3539919)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.31/40.35 % (3539919)CaDiCaL version: 2.1.3 % 282.31/40.35 % (3539919)Termination reason: Instruction limit % 282.31/40.35 % (3539919)Termination phase: Saturation % 282.31/40.35 % (3539919)Time elapsed: 0.617 s % 282.31/40.35 % (3539919)Peak memory usage: 125 MB % 282.31/40.35 % (3539919)Instructions burned: 656 (million) % 282.31/40.35 % (3539925)lrs+21_1_to=kbo:sil=128000:thi=neg_eq:si=on:random_seed=2509354502:i=642:canc=force:rtra=on:tac=axiom:ss=axioms:ev=force_2627 on theBenchmark for (2627ds/642Mi) % 282.31/40.35 % (3539922)Instruction limit reached! % 282.31/40.35 % (3539922)------------------------------ % 282.31/40.35 % (3539922)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 282.31/40.35 % (3539922)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.31/40.35 % (3539922)CaDiCaL version: 2.1.3 % 287.76/41.08 % (3539922)Termination reason: Instruction limit % 287.76/41.08 % (3539922)Termination phase: Saturation % 287.76/41.08 % (3539922)Time elapsed: 0.472 s % 287.76/41.08 % (3539922)Peak memory usage: 125 MB % 287.76/41.08 % (3539922)Instructions burned: 562 (million) % 287.76/41.08 % (3539927)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=3067170669:i=832:rtra=on:gtg=position:ss=axioms_2624 on theBenchmark for (2624ds/832Mi) % 287.76/41.08 % (3539929)lrs+1010_1_to=kbo:tgt=ground:fde=unused:sas=z3:si=on:sp=unary_frequency:gve=force:spb=goal:tha=off:random_seed=1516770379:i=942:thf=on:kws=precedence:rtra=on_2624 on theBenchmark for (2624ds/942Mi) % 287.76/41.08 % (3539925)Instruction limit reached! % 287.76/41.08 % (3539925)------------------------------ % 287.76/41.08 % (3539925)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 287.76/41.08 % (3539925)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 287.76/41.08 % (3539925)CaDiCaL version: 2.1.3 % 287.76/41.08 % (3539925)Termination reason: Instruction limit % 287.76/41.08 % (3539925)Termination phase: Saturation % 287.76/41.08 % (3539925)Time elapsed: 0.545 s % 287.76/41.08 % (3539925)Peak memory usage: 130 MB % 287.76/41.08 % (3539925)Instructions burned: 642 (million) % 287.76/41.08 % (3539923)Instruction limit reached! % 287.76/41.08 % (3539923)------------------------------ % 287.76/41.08 % (3539923)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 287.76/41.08 % (3539923)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 287.76/41.08 % (3539923)CaDiCaL version: 2.1.3 % 287.76/41.08 % (3539923)Termination reason: Instruction limit % 287.76/41.08 % (3539923)Termination phase: Saturation % 287.76/41.08 % (3539923)Time elapsed: 0.818 s % 287.76/41.08 % (3539923)Peak memory usage: 98 MB % 287.76/41.08 % (3539923)Instructions burned: 968 (million) % 287.76/41.08 % (3539932)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=3240783369:avsq=on:i=552:avsqr=1,2:rtra=on_2618 on theBenchmark for (2618ds/552Mi) % 287.76/41.08 % (3539933)lrs+1010_2_to=kbo:sil=128000:tgt=ground:fde=unused:sas=z3:si=on:uwa=off:tha=off:nwc=1:random_seed=94189453:i=750:kws=inv_arity_squared:rtra=on_2618 on theBenchmark for (2618ds/750Mi) % 287.76/41.08 % (3539927)Instruction limit reached! % 287.76/41.08 % (3539927)------------------------------ % 287.76/41.08 % (3539927)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 287.76/41.08 % (3539927)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 287.76/41.08 % (3539927)CaDiCaL version: 2.1.3 % 287.76/41.08 % (3539927)Termination reason: Instruction limit % 287.76/41.08 % (3539927)Termination phase: Saturation % 287.76/41.08 % (3539927)Time elapsed: 0.705 s % 287.76/41.08 % (3539927)Peak memory usage: 125 MB % 287.76/41.08 % (3539927)Instructions burned: 832 (million) % 287.76/41.08 % (3539929)Instruction limit reached! % 287.76/41.08 % (3539929)------------------------------ % 287.76/41.08 % (3539929)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 287.76/41.08 % (3539929)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 287.76/41.08 % (3539929)CaDiCaL version: 2.1.3 % 287.76/41.08 % (3539929)Termination reason: Instruction limit % 287.76/41.08 % (3539929)Termination phase: Saturation % 287.76/41.08 % (3539929)Time elapsed: 0.724 s % 287.76/41.08 % (3539929)Peak memory usage: 125 MB % 287.76/41.08 % (3539929)Instructions burned: 946 (million) % 287.76/41.08 % (3539936)lrs+10_1_to=kbo:sil=128000:tgt=full:sas=z3:si=on:uwa=func_ext:slsqc=1:flr=on:slsq=on:random_seed=2794392437:i=774:bd=preordered:rtra=on:ss=axioms:sgt=8_2615 on theBenchmark for (2615ds/774Mi) % 287.76/41.08 % (3539932)Instruction limit reached! % 287.76/41.08 % (3539932)------------------------------ % 287.76/41.08 % (3539932)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 287.76/41.08 % (3539932)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 287.76/41.08 % (3539932)CaDiCaL version: 2.1.3 % 287.76/41.08 % (3539932)Termination reason: Instruction limit % 287.76/41.08 % (3539932)Termination phase: Saturation % 287.76/41.08 % (3539932)Time elapsed: 0.476 s % 287.76/41.08 % (3539932)Peak memory usage: 136 MB % 287.76/41.08 % (3539932)Instructions burned: 552 (million) % 287.76/41.08 % (3539937)lrs+10_1_to=kbo:sil=128000:fde=none:si=on:norm_ineq=on:urr=on:nwc=0.5:random_seed=1227672624:i=1026:kws=frequency:bd=all:rtra=on:gtg=exists_all:ss=axioms:sgt=4_2613 on theBenchmark for (2613ds/1026Mi) % 287.76/41.08 % (3539939)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=1407819517:i=668:rtra=on_2611 on theBenchmark for (2611ds/668Mi) % 299.19/42.75 % (3539933)Instruction limit reached! % 299.19/42.75 % (3539933)------------------------------ % 299.19/42.75 % (3539933)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 299.19/42.75 % (3539933)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 299.19/42.75 % (3539933)CaDiCaL version: 2.1.3 % 299.19/42.75 % (3539933)Termination reason: Instruction limit % 299.19/42.75 % (3539933)Termination phase: Saturation % 299.19/42.75 % (3539933)Time elapsed: 0.641 s % 299.19/42.75 % (3539933)Peak memory usage: 125 MB % 299.19/42.75 % (3539933)Instructions burned: 750 (million) % 299.19/42.75 % (3539782)Instruction limit reached! % 299.19/42.75 % (3539782)------------------------------ % 299.19/42.75 % (3539782)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 299.19/42.75 % (3539782)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 299.19/42.75 % (3539782)CaDiCaL version: 2.1.3 % 299.19/42.75 % (3539782)Termination reason: Instruction limit % 299.19/42.75 % (3539782)Termination phase: Saturation % 299.19/42.76 % (3539782)Time elapsed: 15.550 s % 299.19/42.76 % (3539782)Peak memory usage: 148 MB % 299.19/42.76 % (3539782)Instructions burned: 20260 (million) % 299.19/42.76 % (3539942)lrs+1010_1_to=kbo:sil=64000:sas=cadical:si=on:sos=on:bce=on:random_seed=1975526159:i=718:rtra=on:gtg=exists_top:ss=axioms_2609 on theBenchmark for (2609ds/718Mi) % 299.19/42.76 % (3539936)Instruction limit reached! % 299.19/42.76 % (3539936)------------------------------ % 299.19/42.76 % (3539936)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 299.19/42.76 % (3539936)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 299.19/42.76 % (3539936)CaDiCaL version: 2.1.3 % 299.19/42.76 % (3539936)Termination reason: Instruction limit % 299.19/42.76 % (3539936)Termination phase: Saturation % 299.19/42.76 % (3539936)Time elapsed: 0.634 s % 299.19/42.76 % (3539936)Peak memory usage: 125 MB % 299.19/42.76 % (3539936)Instructions burned: 774 (million) % 299.19/42.76 % (3539943)dis+1010_1_to=lpo:sil=128000:thi=all:fde=unused:si=on:sp=reverse_arity:tha=off:random_seed=533199262:i=682:gtgl=2:rtra=on:gtg=exists_sym:ev=force:fsd=on:fsdmm=1_2608 on theBenchmark for (2608ds/682Mi) % 299.19/42.76 % (3539946)lrs-2_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_max:tha=off:random_seed=743629245:st=1.5:i=522:sd=1:kws=precedence:rtra=on:ss=axioms_2605 on theBenchmark for (2605ds/522Mi) % 299.19/42.76 % (3539937)Instruction limit reached! % 299.19/42.76 % (3539937)------------------------------ % 299.19/42.76 % (3539937)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 299.19/42.76 % (3539937)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 299.19/42.76 % (3539937)CaDiCaL version: 2.1.3 % 299.19/42.76 % (3539937)Termination reason: Instruction limit % 299.19/42.76 % (3539937)Termination phase: Saturation % 299.19/42.76 % (3539937)Time elapsed: 0.828 s % 299.19/42.76 % (3539937)Peak memory usage: 99 MB % 299.19/42.76 % (3539937)Instructions burned: 1027 (million) % 299.19/42.76 % (3539939)Instruction limit reached! % 299.19/42.76 % (3539939)------------------------------ % 299.19/42.76 % (3539939)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 299.19/42.76 % (3539939)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 299.19/42.76 % (3539939)CaDiCaL version: 2.1.3 % 299.19/42.76 % (3539939)Termination reason: Instruction limit % 299.19/42.76 % (3539939)Termination phase: Saturation % 299.19/42.76 % (3539939)Time elapsed: 0.676 s % 299.19/42.76 % (3539939)Peak memory usage: 142 MB % 299.19/42.76 % (3539939)Instructions burned: 668 (million) % 299.19/42.76 % (3539946)Instruction limit reached! % 299.19/42.76 % (3539946)------------------------------ % 299.19/42.76 % (3539946)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 299.19/42.76 % (3539946)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 299.19/42.76 % (3539946)CaDiCaL version: 2.1.3 % 299.19/42.76 % (3539946)Termination reason: Instruction limit % 299.19/42.76 % (3539946)Termination phase: Saturation % 299.19/42.76 % (3539946)Time elapsed: 0.221 s % 299.19/42.76 % (3539946)Peak memory usage: 125 MB % 299.19/42.76 % (3539946)Instructions burned: 524 (million) % 299.19/42.76 % (3539942)Instruction limit reached! % 299.19/42.76 % (3539942)------------------------------ % 299.19/42.76 % (3539942)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 299.19/42.76 % (3539942)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 299.19/42.76 % (3Terminated %------------------------------------------------------------------------------