%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWW001_1 : TPTP v9.3.1. Released v5.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % Computer : n018.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:27:55 PM UTC 2026 % Result : Timeout 290.30s 41.58s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : SWW001_1 : TPTP v9.3.1. Released v5.0.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.09/0.19 % Computer : n018.cluster.edu % 0.09/0.19 % Model : x86_64 x86_64 % 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.19 % Memory : 8046.5625MB % 0.09/0.19 % OS : Linux 6.8.0-71-generic % 0.09/0.19 % CPULimit : 300 % 0.09/0.19 % WCLimit : 300 % 0.09/0.20 % DateTime : Mon Sep 28 13:10:09 UTC 2026 % 0.09/0.20 % CPUTime : % 0.09/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.09/0.23 Running first-order theorem proving % 0.09/0.23 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 4.78/1.15 % (3370140)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule. % 4.78/1.15 % (3370167)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=1166791354:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi) % 4.78/1.15 % (3370161)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=2263320030:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi) % 4.78/1.15 % (3370162)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=543080346:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi) % 4.78/1.15 % (3370164)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=3869025261:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi) % 4.78/1.15 % (3370165)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=448297439:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi) % 4.78/1.15 % (3370166)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=931528602:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi) % 4.78/1.15 % (3370166)Instruction limit reached! % 4.78/1.15 % (3370166)------------------------------ % 4.78/1.15 % (3370166)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.78/1.15 % (3370166)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.78/1.15 % (3370166)CaDiCaL version: 2.1.3 % 4.78/1.15 % (3370166)Termination reason: Instruction limit % 4.78/1.15 % (3370166)Termination phase: Preprocessing 1 % 4.78/1.15 % (3370166)Time elapsed: 0.001 s % 4.78/1.15 % (3370166)Peak memory usage: 85 MB % 4.78/1.15 % (3370166)Instructions burned: 5 (million) % 4.78/1.15 % (3370165)Instruction limit reached! % 4.78/1.15 % (3370165)------------------------------ % 4.78/1.15 % (3370165)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.78/1.15 % (3370165)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.78/1.15 % (3370165)CaDiCaL version: 2.1.3 % 4.78/1.15 % (3370165)Termination reason: Instruction limit % 4.78/1.15 % (3370165)Termination phase: Preprocessing 3 % 4.78/1.15 % (3370165)Time elapsed: 0.005 s % 4.78/1.15 % (3370165)Peak memory usage: 86 MB % 4.78/1.15 % (3370165)Instructions burned: 8 (million) % 4.78/1.15 % (3370168)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=1523457324:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi) % 4.78/1.15 % (3370161)Instruction limit reached! % 4.78/1.15 % (3370161)------------------------------ % 4.78/1.15 % (3370161)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.78/1.15 % (3370161)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.78/1.15 % (3370161)CaDiCaL version: 2.1.3 % 4.78/1.15 % (3370161)Termination reason: Instruction limit % 4.78/1.15 % (3370161)Termination phase: Property scanning % 4.78/1.15 % (3370161)Time elapsed: 0.006 s % 4.78/1.15 % (3370161)Peak memory usage: 86 MB % 4.78/1.15 % (3370161)Instructions burned: 13 (million) % 4.78/1.15 % (3370168)Instruction limit reached! % 4.78/1.15 % (3370168)------------------------------ % 4.78/1.15 % (3370168)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.78/1.15 % (3370168)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.78/1.15 % (3370168)CaDiCaL version: 2.1.3 % 4.78/1.15 % (3370168)Termination reason: Instruction limit % 4.78/1.15 % (3370168)Termination phase: Saturation % 4.78/1.15 % (3370168)Time elapsed: 0.038 s % 4.78/1.15 % (3370168)Peak memory usage: 112 MB % 4.78/1.15 % (3370168)Instructions burned: 34 (million) % 4.78/1.15 % (3370167)Instruction limit reached! % 4.78/1.15 % (3370167)------------------------------ % 4.78/1.15 % (3370167)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.78/1.15 % (3370167)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.78/1.15 % (3370167)CaDiCaL version: 2.1.3 % 4.78/1.15 % (3370167)Termination reason: Instruction limit % 4.78/1.15 % (3370167)Termination phase: Saturation % 4.78/1.15 % (3370167)Time elapsed: 0.048 s % 4.78/1.15 % (3370167)Peak memory usage: 116 MB % 4.78/1.15 % (3370167)Instructions burned: 47 (million) % 4.78/1.15 % (3370162)Refutation not found, incomplete strategy % 4.78/1.15 % (3370162)------------------------------ % 4.78/1.15 % (3370162)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.78/1.15 % (3370162)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.45/1.40 % (3370162)CaDiCaL version: 2.1.3 % 5.45/1.40 % (3370162)Termination reason: Refutation not found, incomplete strategy % 5.45/1.40 % (3370162)Time elapsed: 0.107 s % 5.45/1.40 % (3370162)Peak memory usage: 117 MB % 5.45/1.40 % (3370162)Instructions burned: 103 (million) % 5.45/1.40 % (3370232)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=783218151:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2998 on theBenchmark for (2998ds/14Mi) % 5.45/1.40 % (3370232)Instruction limit reached! % 5.45/1.40 % (3370232)------------------------------ % 5.45/1.40 % (3370232)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.45/1.40 % (3370232)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.45/1.40 % (3370232)CaDiCaL version: 2.1.3 % 5.45/1.40 % (3370232)Termination reason: Instruction limit % 5.45/1.40 % (3370232)Termination phase: Saturation % 5.45/1.40 % (3370232)Time elapsed: 0.005 s % 5.45/1.40 % (3370232)Peak memory usage: 88 MB % 5.45/1.40 % (3370232)Instructions burned: 15 (million) % 5.45/1.40 % (3370235)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=955827764:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/16Mi) % 5.45/1.40 % (3370234)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=4181763434:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2998 on theBenchmark for (2998ds/29Mi) % 5.45/1.40 % (3370164)Instruction limit reached! % 5.45/1.40 % (3370164)------------------------------ % 5.45/1.40 % (3370164)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.45/1.40 % (3370164)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.45/1.40 % (3370164)CaDiCaL version: 2.1.3 % 5.45/1.40 % (3370164)Termination reason: Instruction limit % 5.45/1.40 % (3370164)Termination phase: Saturation % 5.45/1.40 % (3370164)Time elapsed: 0.160 s % 5.45/1.40 % (3370164)Peak memory usage: 118 MB % 5.45/1.40 % (3370164)Instructions burned: 201 (million) % 5.45/1.40 % (3370235)Instruction limit reached! % 5.45/1.40 % (3370235)------------------------------ % 5.45/1.40 % (3370235)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.45/1.40 % (3370235)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.45/1.40 % (3370235)CaDiCaL version: 2.1.3 % 5.45/1.40 % (3370235)Termination reason: Instruction limit % 5.45/1.40 % (3370235)Termination phase: Saturation % 5.45/1.40 % (3370235)Time elapsed: 0.010 s % 5.45/1.40 % (3370235)Peak memory usage: 89 MB % 5.45/1.40 % (3370235)Instructions burned: 18 (million) % 5.45/1.40 % (3370234)Instruction limit reached! % 5.45/1.40 % (3370234)------------------------------ % 5.45/1.40 % (3370234)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.45/1.40 % (3370234)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.45/1.40 % (3370234)CaDiCaL version: 2.1.3 % 5.45/1.40 % (3370234)Termination reason: Instruction limit % 5.45/1.40 % (3370234)Termination phase: Saturation % 5.45/1.40 % (3370234)Time elapsed: 0.017 s % 5.45/1.40 % (3370234)Peak memory usage: 89 MB % 5.45/1.40 % (3370234)Instructions burned: 29 (million) % 5.45/1.40 % (3370245)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=1201568824:i=24:canc=force:rtra=on_2997 on theBenchmark for (2997ds/24Mi) % 5.45/1.40 % (3370246)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=2215724896:i=27:canc=cautious:fsr=off:rtra=on_2997 on theBenchmark for (2997ds/27Mi) % 5.45/1.40 % (3370245)Instruction limit reached! % 5.45/1.40 % (3370245)------------------------------ % 5.45/1.40 % (3370245)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.45/1.40 % (3370245)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.45/1.40 % (3370245)CaDiCaL version: 2.1.3 % 5.45/1.40 % (3370245)Termination reason: Instruction limit % 5.45/1.40 % (3370245)Termination phase: Saturation % 5.45/1.40 % (3370245)Time elapsed: 0.014 s % 5.45/1.40 % (3370245)Peak memory usage: 90 MB % 5.45/1.40 % (3370245)Instructions burned: 24 (million) % 5.45/1.40 % (3370246)Instruction limit reached! % 5.45/1.40 % (3370246)------------------------------ % 5.45/1.40 % (3370246)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.45/1.40 % (3370246)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.91/1.59 % (3370246)CaDiCaL version: 2.1.3 % 6.91/1.59 % (3370246)Termination reason: Instruction limit % 6.91/1.59 % (3370246)Termination phase: Saturation % 6.91/1.59 % (3370246)Time elapsed: 0.014 s % 6.91/1.59 % (3370246)Peak memory usage: 89 MB % 6.91/1.59 % (3370246)Instructions burned: 27 (million) % 6.91/1.59 % (3370263)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=1230433958:i=85:gtgl=4:rtra=on:gtg=exists_sym_2997 on theBenchmark for (2997ds/85Mi) % 6.91/1.59 % (3370263)Instruction limit reached! % 6.91/1.59 % (3370263)------------------------------ % 6.91/1.59 % (3370263)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.91/1.59 % (3370263)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.91/1.59 % (3370263)CaDiCaL version: 2.1.3 % 6.91/1.59 % (3370263)Termination reason: Instruction limit % 6.91/1.59 % (3370263)Termination phase: Saturation % 6.91/1.59 % (3370263)Time elapsed: 0.026 s % 6.91/1.59 % (3370263)Peak memory usage: 89 MB % 6.91/1.59 % (3370263)Instructions burned: 86 (million) % 6.91/1.59 % (3370277)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=2875564172:i=181:rtra=on:ss=axioms:ev=cautious_2996 on theBenchmark for (2996ds/181Mi) % 6.91/1.59 % (3370275)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=13514731:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2996 on theBenchmark for (2996ds/2Mi) % 6.91/1.59 % (3370275)Instruction limit reached! % 6.91/1.59 % (3370275)------------------------------ % 6.91/1.59 % (3370275)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.91/1.59 % (3370275)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.91/1.59 % (3370275)CaDiCaL version: 2.1.3 % 6.91/1.59 % (3370275)Termination reason: Instruction limit % 6.91/1.59 % (3370275)Termination phase: Property scanning % 6.91/1.59 % (3370275)Time elapsed: 0.003 s % 6.91/1.59 % (3370275)Peak memory usage: 85 MB % 6.91/1.59 % (3370275)Instructions burned: 2 (million) % 6.91/1.59 % (3370279)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=2823737191:i=4:ep=RST:ins=2:rtra=on_2996 on theBenchmark for (2996ds/4Mi) % 6.91/1.59 % (3370279)Instruction limit reached! % 6.91/1.59 % (3370279)------------------------------ % 6.91/1.59 % (3370279)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.91/1.59 % (3370279)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.91/1.59 % (3370279)CaDiCaL version: 2.1.3 % 6.91/1.59 % (3370279)Termination reason: Instruction limit % 6.91/1.59 % (3370279)Termination phase: Preprocessing 1 % 6.91/1.59 % (3370279)Time elapsed: 0.004 s % 6.91/1.59 % (3370279)Peak memory usage: 85 MB % 6.91/1.59 % (3370279)Instructions burned: 4 (million) % 6.91/1.59 % (3370277)Refutation not found, incomplete strategy % 6.91/1.59 % (3370277)------------------------------ % 6.91/1.59 % (3370277)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.91/1.59 % (3370277)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.91/1.59 % (3370277)CaDiCaL version: 2.1.3 % 6.91/1.59 % (3370277)Termination reason: Refutation not found, incomplete strategy % 6.91/1.59 % (3370277)Time elapsed: 0.075 s % 6.91/1.59 % (3370277)Peak memory usage: 92 MB % 6.91/1.59 % (3370277)Instructions burned: 101 (million) % 6.91/1.59 % (3370162)------------------------------ % 6.91/1.59 % (3370162)------------------------------ % 6.91/1.59 % (3370291)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=2056138699:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2996 on theBenchmark for (2996ds/66Mi) % 6.91/1.59 % (3370293)lrs+10_1_thi=all:si=on:fd=off:random_seed=70434995:i=53:rtra=on:gtg=all_2996 on theBenchmark for (2996ds/53Mi) % 6.91/1.59 % (3370293)Instruction limit reached! % 6.91/1.59 % (3370293)------------------------------ % 6.91/1.59 % (3370293)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.91/1.59 % (3370293)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.91/1.59 % (3370293)CaDiCaL version: 2.1.3 % 6.91/1.59 % (3370293)Termination reason: Instruction limit % 6.91/1.59 % (3370293)Termination phase: Saturation % 6.91/1.59 % (3370293)Time elapsed: 0.047 s % 6.91/1.59 % (3370293)Peak memory usage: 116 MB % 6.91/1.59 % (3370293)Instructions burned: 53 (million) % 6.91/1.59 % (3370305)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=849020875:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2995 on theBenchmark for (2995ds/8Mi) % 8.38/2.03 % (3370291)Instruction limit reached! % 8.38/2.03 % (3370291)------------------------------ % 8.38/2.03 % (3370291)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.38/2.03 % (3370291)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.38/2.03 % (3370291)CaDiCaL version: 2.1.3 % 8.38/2.03 % (3370291)Termination reason: Instruction limit % 8.38/2.03 % (3370291)Termination phase: Saturation % 8.38/2.03 % (3370291)Time elapsed: 0.108 s % 8.38/2.03 % (3370291)Peak memory usage: 135 MB % 8.38/2.03 % (3370291)Instructions burned: 66 (million) % 8.38/2.03 % (3370305)Instruction limit reached! % 8.38/2.03 % (3370305)------------------------------ % 8.38/2.03 % (3370305)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.38/2.03 % (3370305)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.38/2.03 % (3370305)CaDiCaL version: 2.1.3 % 8.38/2.03 % (3370305)Termination reason: Instruction limit % 8.38/2.03 % (3370305)Termination phase: Preprocessing 2 % 8.38/2.03 % (3370305)Time elapsed: 0.007 s % 8.38/2.03 % (3370305)Peak memory usage: 86 MB % 8.38/2.03 % (3370305)Instructions burned: 8 (million) % 8.38/2.03 % (3370324)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=529054703:st=3:i=2:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/2Mi) % 8.38/2.03 % (3370324)Instruction limit reached! % 8.38/2.03 % (3370324)------------------------------ % 8.38/2.03 % (3370324)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.38/2.03 % (3370324)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.38/2.03 % (3370324)CaDiCaL version: 2.1.3 % 8.38/2.03 % (3370324)Termination reason: Instruction limit % 8.38/2.03 % (3370324)Termination phase: Preprocessing 1 % 8.38/2.03 % (3370324)Time elapsed: 0.003 s % 8.38/2.03 % (3370324)Peak memory usage: 85 MB % 8.38/2.03 % (3370324)Instructions burned: 3 (million) % 8.38/2.03 % (3370330)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=149425643:i=2:doe=on:canc=force:asg=cautious:rtra=on_2994 on theBenchmark for (2994ds/2Mi) % 8.38/2.03 % (3370330)Instruction limit reached! % 8.38/2.03 % (3370330)------------------------------ % 8.38/2.03 % (3370330)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.38/2.03 % (3370330)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.38/2.03 % (3370330)CaDiCaL version: 2.1.3 % 8.38/2.03 % (3370330)Termination reason: Instruction limit % 8.38/2.03 % (3370330)Termination phase: Property scanning % 8.38/2.03 % (3370330)Time elapsed: 0.003 s % 8.38/2.03 % (3370330)Peak memory usage: 85 MB % 8.38/2.03 % (3370330)Instructions burned: 2 (million) % 8.38/2.03 % (3370337)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=3455088829:i=127:doe=on:rtra=on_2993 on theBenchmark for (2993ds/127Mi) % 8.38/2.03 % (3370341)dis+10_1_si=on:random_seed=2834275994:i=10:ep=R:rtra=on_2993 on theBenchmark for (2993ds/10Mi) % 8.38/2.03 % (3370337)Instruction limit reached! % 8.38/2.03 % (3370337)------------------------------ % 8.38/2.03 % (3370337)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.38/2.03 % (3370337)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.38/2.03 % (3370337)CaDiCaL version: 2.1.3 % 8.38/2.03 % (3370337)Termination reason: Instruction limit % 8.38/2.03 % (3370337)Termination phase: Saturation % 8.38/2.03 % (3370337)Time elapsed: 0.105 s % 8.38/2.03 % (3370337)Peak memory usage: 117 MB % 8.38/2.03 % (3370337)Instructions burned: 128 (million) % 8.38/2.03 % (3370341)Instruction limit reached! % 8.38/2.03 % (3370341)------------------------------ % 8.38/2.03 % (3370341)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.38/2.03 % (3370341)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.38/2.03 % (3370341)CaDiCaL version: 2.1.3 % 8.38/2.03 % (3370341)Termination reason: Instruction limit % 8.38/2.03 % (3370341)Termination phase: Clausification % 8.38/2.03 % (3370341)Time elapsed: 0.009 s % 8.38/2.03 % (3370341)Peak memory usage: 86 MB % 8.38/2.03 % (3370341)Instructions burned: 10 (million) % 8.38/2.03 % (3370277)------------------------------ % 8.38/2.03 % (3370277)------------------------------ % 8.38/2.03 % (3370348)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=3248066903: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_2992 on theBenchmark for (2992ds/35Mi) % 12.44/2.47 % (3370347)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=3363213092:i=26:canc=cautious:av=off:rtra=on_2992 on theBenchmark for (2992ds/26Mi) % 12.44/2.47 % (3370348)Instruction limit reached! % 12.44/2.47 % (3370348)------------------------------ % 12.44/2.47 % (3370348)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.44/2.47 % (3370348)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.44/2.47 % (3370348)CaDiCaL version: 2.1.3 % 12.44/2.47 % (3370348)Termination reason: Instruction limit % 12.44/2.47 % (3370348)Termination phase: Saturation % 12.44/2.47 % (3370348)Time elapsed: 0.035 s % 12.44/2.47 % (3370348)Peak memory usage: 89 MB % 12.44/2.47 % (3370348)Instructions burned: 35 (million) % 12.44/2.47 % (3370347)Instruction limit reached! % 12.44/2.47 % (3370347)------------------------------ % 12.44/2.47 % (3370347)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.44/2.47 % (3370347)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.44/2.47 % (3370347)CaDiCaL version: 2.1.3 % 12.44/2.47 % (3370347)Termination reason: Instruction limit % 12.44/2.47 % (3370347)Termination phase: Saturation % 12.44/2.47 % (3370347)Time elapsed: 0.024 s % 12.44/2.47 % (3370347)Peak memory usage: 88 MB % 12.44/2.47 % (3370347)Instructions burned: 27 (million) % 12.44/2.47 % (3370354)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=1639533089:i=2:fsr=off:rtra=on:inst=on_2992 on theBenchmark for (2992ds/2Mi) % 12.44/2.47 % (3370354)Instruction limit reached! % 12.44/2.47 % (3370354)------------------------------ % 12.44/2.47 % (3370354)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.44/2.47 % (3370354)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.44/2.47 % (3370354)CaDiCaL version: 2.1.3 % 12.44/2.47 % (3370354)Termination reason: Instruction limit % 12.44/2.47 % (3370354)Termination phase: Property scanning % 12.44/2.47 % (3370354)Time elapsed: 0.002 s % 12.44/2.47 % (3370354)Peak memory usage: 85 MB % 12.44/2.47 % (3370354)Instructions burned: 2 (million) % 12.44/2.47 % (3370357)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=2088058910:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2991 on theBenchmark for (2991ds/8Mi) % 12.44/2.47 % (3370357)Instruction limit reached! % 12.44/2.47 % (3370357)------------------------------ % 12.44/2.47 % (3370357)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.44/2.47 % (3370357)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.44/2.47 % (3370357)CaDiCaL version: 2.1.3 % 12.44/2.47 % (3370357)Termination reason: Instruction limit % 12.44/2.47 % (3370357)Termination phase: Preprocessing 3 % 12.44/2.47 % (3370357)Time elapsed: 0.009 s % 12.44/2.47 % (3370357)Peak memory usage: 86 MB % 12.44/2.47 % (3370357)Instructions burned: 9 (million) % 12.44/2.47 % (3370362)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=1346900663:i=226:rtra=on:gtg=position:ss=axioms_2990 on theBenchmark for (2990ds/226Mi) % 12.44/2.47 % (3370359)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=3303275446:i=370:ep=RS:fsr=off:rtra=on_2990 on theBenchmark for (2990ds/370Mi) % 12.44/2.47 % (3370360)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=1157297146:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2990 on theBenchmark for (2990ds/13Mi) % 12.44/2.47 % (3370359)Refutation not found, incomplete strategy % 12.44/2.47 % (3370359)------------------------------ % 12.44/2.47 % (3370359)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.44/2.47 % (3370359)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.44/2.47 % (3370359)CaDiCaL version: 2.1.3 % 12.44/2.47 % (3370359)Termination reason: Refutation not found, incomplete strategy % 12.44/2.47 % (3370359)Time elapsed: 0.020 s % 12.44/2.47 % (3370359)Peak memory usage: 89 MB % 12.44/2.47 % (3370359)Instructions burned: 21 (million) % 12.44/2.47 % (3370360)Instruction limit reached! % 12.44/2.47 % (3370360)------------------------------ % 12.44/2.47 % (3370360)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.44/2.47 % (3370360)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.44/2.47 % (3370360)CaDiCaL version: 2.1.3 % 12.44/2.47 % (3370360)Termination reason: Instruction limit % 12.44/2.47 % (3370360)Termination phase: Preprocessing 3 % 12.44/2.47 % (3370360)Time elapsed: 0.012 s % 15.77/2.95 % (3370360)Peak memory usage: 86 MB % 15.77/2.95 % (3370360)Instructions burned: 13 (million) % 15.77/2.95 % (3370365)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=1836597796:i=71:rtra=on:gtg=exists_top_2990 on theBenchmark for (2990ds/71Mi) % 15.77/2.95 % (3370362)Refutation not found, incomplete strategy % 15.77/2.95 % (3370362)------------------------------ % 15.77/2.95 % (3370362)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.77/2.95 % (3370362)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.77/2.95 % (3370362)CaDiCaL version: 2.1.3 % 15.77/2.95 % (3370362)Termination reason: Refutation not found, incomplete strategy % 15.77/2.95 % (3370362)Time elapsed: 0.126 s % 15.77/2.95 % (3370362)Peak memory usage: 117 MB % 15.77/2.95 % (3370362)Instructions burned: 206 (million) % 15.77/2.95 % (3370364)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=4203239965:i=10:rtra=on_2990 on theBenchmark for (2990ds/10Mi) % 15.77/2.95 % (3370364)Instruction limit reached! % 15.77/2.95 % (3370364)------------------------------ % 15.77/2.95 % (3370364)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.77/2.95 % (3370364)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.77/2.95 % (3370364)CaDiCaL version: 2.1.3 % 15.77/2.95 % (3370364)Termination reason: Instruction limit % 15.77/2.95 % (3370364)Termination phase: Saturation % 15.77/2.95 % (3370364)Time elapsed: 0.010 s % 15.77/2.95 % (3370364)Peak memory usage: 86 MB % 15.77/2.95 % (3370364)Instructions burned: 10 (million) % 15.77/2.95 % (3370372)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=463329695:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2989 on theBenchmark for (2989ds/294Mi) % 15.77/2.95 % (3370368)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=3130629940:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2989 on theBenchmark for (2989ds/75Mi) % 15.77/2.95 % (3370368)Instruction limit reached! % 15.77/2.95 % (3370368)------------------------------ % 15.77/2.95 % (3370368)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.77/2.95 % (3370368)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.77/2.95 % (3370368)CaDiCaL version: 2.1.3 % 15.77/2.95 % (3370368)Termination reason: Instruction limit % 15.77/2.95 % (3370368)Termination phase: Saturation % 15.77/2.95 % (3370368)Time elapsed: 0.055 s % 15.77/2.95 % (3370368)Peak memory usage: 91 MB % 15.77/2.95 % (3370368)Instructions burned: 76 (million) % 15.77/2.95 % (3370365)Instruction limit reached! % 15.77/2.95 % (3370365)------------------------------ % 15.77/2.95 % (3370365)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.77/2.95 % (3370365)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.77/2.95 % (3370365)CaDiCaL version: 2.1.3 % 15.77/2.95 % (3370365)Termination reason: Instruction limit % 15.77/2.95 % (3370365)Termination phase: Saturation % 15.77/2.95 % (3370365)Time elapsed: 0.134 s % 15.77/2.95 % (3370365)Peak memory usage: 133 MB % 15.77/2.95 % (3370365)Instructions burned: 71 (million) % 15.77/2.95 % (3370381)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=934652681:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2988 on theBenchmark for (2988ds/130Mi) % 15.77/2.95 % (3370362)------------------------------ % 15.77/2.95 % (3370362)------------------------------ % 15.77/2.95 % (3370359)------------------------------ % 15.77/2.95 % (3370359)------------------------------ % 15.77/2.95 % (3370386)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=3024591493:i=131:rtra=on_2987 on theBenchmark for (2987ds/131Mi) % 15.77/2.95 % (3370372)Instruction limit reached! % 15.77/2.95 % (3370372)------------------------------ % 15.77/2.95 % (3370372)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.77/2.95 % (3370372)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.77/2.95 % (3370372)CaDiCaL version: 2.1.3 % 15.77/2.95 % (3370372)Termination reason: Instruction limit % 15.77/2.95 % (3370372)Termination phase: Saturation % 15.77/2.95 % (3370372)Time elapsed: 0.285 s % 15.77/2.95 % (3370372)Peak memory usage: 90 MB % 15.77/2.95 % (3370372)Instructions burned: 295 (million) % 15.77/2.95 % (3370394)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=821049785:i=307:rtra=on:gtg=exists_top_2986 on theBenchmark for (2986ds/307Mi) % 19.43/3.34 % (3370381)Refutation not found, incomplete strategy % 19.43/3.34 % (3370381)------------------------------ % 19.43/3.34 % (3370381)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.43/3.34 % (3370381)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.43/3.34 % (3370381)CaDiCaL version: 2.1.3 % 19.43/3.34 % (3370381)Termination reason: Refutation not found, incomplete strategy % 19.43/3.34 % (3370381)Time elapsed: 0.159 s % 19.43/3.34 % (3370381)Peak memory usage: 117 MB % 19.43/3.34 % (3370381)Instructions burned: 127 (million) % 19.43/3.34 % (3370392)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=637310868:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2986 on theBenchmark for (2986ds/40Mi) % 19.43/3.34 % (3370392)Instruction limit reached! % 19.43/3.34 % (3370392)------------------------------ % 19.43/3.34 % (3370392)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.43/3.34 % (3370392)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.43/3.34 % (3370392)CaDiCaL version: 2.1.3 % 19.43/3.34 % (3370392)Termination reason: Instruction limit % 19.43/3.34 % (3370392)Termination phase: Saturation % 19.43/3.34 % (3370392)Time elapsed: 0.093 s % 19.43/3.34 % (3370392)Peak memory usage: 130 MB % 19.43/3.34 % (3370392)Instructions burned: 40 (million) % 19.43/3.34 % (3370394)Instruction limit reached! % 19.43/3.34 % (3370394)------------------------------ % 19.43/3.34 % (3370394)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.43/3.34 % (3370394)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.43/3.34 % (3370394)CaDiCaL version: 2.1.3 % 19.43/3.34 % (3370394)Termination reason: Instruction limit % 19.43/3.34 % (3370394)Termination phase: Saturation % 19.43/3.34 % (3370394)Time elapsed: 0.149 s % 19.43/3.34 % (3370394)Peak memory usage: 90 MB % 19.43/3.34 % (3370394)Instructions burned: 308 (million) % 19.43/3.34 % (3370386)Instruction limit reached! % 19.43/3.34 % (3370386)------------------------------ % 19.43/3.34 % (3370386)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.43/3.34 % (3370386)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.43/3.34 % (3370386)CaDiCaL version: 2.1.3 % 19.43/3.34 % (3370386)Termination reason: Instruction limit % 19.43/3.34 % (3370386)Termination phase: Saturation % 19.43/3.34 % (3370386)Time elapsed: 0.199 s % 19.43/3.34 % (3370386)Peak memory usage: 133 MB % 19.43/3.34 % (3370386)Instructions burned: 131 (million) % 19.43/3.34 % (3370398)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=2015903979:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2985 on theBenchmark for (2985ds/598Mi) % 19.43/3.34 % (3370400)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=3990617822:i=131:canc=cautious:fsr=off:rtra=on_2984 on theBenchmark for (2984ds/131Mi) % 19.43/3.34 % (3370403)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=3873360181:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2984 on theBenchmark for (2984ds/259Mi) % 19.43/3.34 % (3370408)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=950183686:i=383:fsr=off:rtra=on:ev=force_2982 on theBenchmark for (2982ds/383Mi) % 19.43/3.34 % (3370406)dis+10_1_si=on:random_seed=551165225:s2a=on:i=1000:rtra=on:gtg=exists_all_2983 on theBenchmark for (2983ds/1000Mi) % 19.43/3.34 % (3370381)------------------------------ % 19.43/3.34 % (3370381)------------------------------ % 19.43/3.34 % (3370400)Instruction limit reached! % 19.43/3.34 % (3370400)------------------------------ % 19.43/3.34 % (3370400)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.43/3.34 % (3370400)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.43/3.34 % (3370400)CaDiCaL version: 2.1.3 % 19.43/3.34 % (3370400)Termination reason: Instruction limit % 19.43/3.34 % (3370400)Termination phase: Saturation % 19.43/3.34 % (3370400)Time elapsed: 0.171 s % 19.43/3.34 % (3370400)Peak memory usage: 117 MB % 19.43/3.34 % (3370400)Instructions burned: 132 (million) % 19.43/3.34 % (3370408)Refutation not found, incomplete strategy % 19.43/3.34 % (3370408)------------------------------ % 19.43/3.34 % (3370408)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.43/3.34 % (3370408)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.96/3.89 % (3370408)CaDiCaL version: 2.1.3 % 21.96/3.89 % (3370408)Termination reason: Refutation not found, incomplete strategy % 21.96/3.89 % (3370408)Time elapsed: 0.054 s % 21.96/3.89 % (3370408)Peak memory usage: 91 MB % 21.96/3.89 % (3370408)Instructions burned: 89 (million) % 21.96/3.89 % (3370411)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=3284800312:i=141:doe=on:rtra=on_2982 on theBenchmark for (2982ds/141Mi) % 21.96/3.89 % (3370403)Instruction limit reached! % 21.96/3.89 % (3370403)------------------------------ % 21.96/3.89 % (3370403)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.96/3.89 % (3370403)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.96/3.89 % (3370403)CaDiCaL version: 2.1.3 % 21.96/3.89 % (3370403)Termination reason: Instruction limit % 21.96/3.89 % (3370403)Termination phase: Saturation % 21.96/3.89 % (3370403)Time elapsed: 0.308 s % 21.96/3.89 % (3370403)Peak memory usage: 118 MB % 21.96/3.89 % (3370403)Instructions burned: 259 (million) % 21.96/3.89 % (3370411)Instruction limit reached! % 21.96/3.89 % (3370411)------------------------------ % 21.96/3.89 % (3370411)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.96/3.89 % (3370411)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.96/3.89 % (3370411)CaDiCaL version: 2.1.3 % 21.96/3.89 % (3370411)Termination reason: Instruction limit % 21.96/3.89 % (3370411)Termination phase: Saturation % 21.96/3.89 % (3370411)Time elapsed: 0.143 s % 21.96/3.89 % (3370411)Peak memory usage: 90 MB % 21.96/3.89 % (3370411)Instructions burned: 142 (million) % 21.96/3.89 % (3370398)Refutation not found, incomplete strategy % 21.96/3.89 % (3370398)------------------------------ % 21.96/3.89 % (3370398)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.96/3.89 % (3370398)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.96/3.89 % (3370398)CaDiCaL version: 2.1.3 % 21.96/3.89 % (3370398)Termination reason: Refutation not found, incomplete strategy % 21.96/3.89 % (3370398)Time elapsed: 0.447 s % 21.96/3.89 % (3370398)Peak memory usage: 136 MB % 21.96/3.89 % (3370398)Instructions burned: 408 (million) % 21.96/3.89 % (3370419)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=181578751:i=121:nm=16:rtra=on_2980 on theBenchmark for (2980ds/121Mi) % 21.96/3.89 % (3370418)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=2791799295:i=65:nm=16:rtra=on_2980 on theBenchmark for (2980ds/65Mi) % 21.96/3.89 % (3370408)------------------------------ % 21.96/3.89 % (3370408)------------------------------ % 21.96/3.89 % (3370418)Instruction limit reached! % 21.96/3.89 % (3370418)------------------------------ % 21.96/3.89 % (3370418)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.96/3.89 % (3370418)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.96/3.89 % (3370418)CaDiCaL version: 2.1.3 % 21.96/3.89 % (3370418)Termination reason: Instruction limit % 21.96/3.89 % (3370418)Termination phase: Saturation % 21.96/3.89 % (3370418)Time elapsed: 0.098 s % 21.96/3.89 % (3370418)Peak memory usage: 116 MB % 21.96/3.89 % (3370418)Instructions burned: 65 (million) % 21.96/3.89 % (3370419)Instruction limit reached! % 21.96/3.89 % (3370419)------------------------------ % 21.96/3.89 % (3370419)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.96/3.89 % (3370419)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.96/3.89 % (3370419)CaDiCaL version: 2.1.3 % 21.96/3.89 % (3370419)Termination reason: Instruction limit % 21.96/3.89 % (3370419)Termination phase: Saturation % 21.96/3.89 % (3370419)Time elapsed: 0.111 s % 21.96/3.89 % (3370419)Peak memory usage: 89 MB % 21.96/3.89 % (3370419)Instructions burned: 121 (million) % 21.96/3.89 % (3370421)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=1950383200:s2a=on:i=128:s2at=5:ins=3:rtra=on_2978 on theBenchmark for (2978ds/128Mi) % 21.96/3.89 % (3370422)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=615708814:i=39:ins=3:rtra=on_2978 on theBenchmark for (2978ds/39Mi) % 21.96/3.89 % (3370422)Instruction limit reached! % 21.96/3.89 % (3370422)------------------------------ % 21.96/3.89 % (3370422)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.96/3.89 % (3370422)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.96/3.89 % (3370422)CaDiCaL version: 2.1.3 % 27.17/4.41 % (3370422)Termination reason: Instruction limit % 27.17/4.41 % (3370422)Termination phase: Saturation % 27.17/4.41 % (3370422)Time elapsed: 0.063 s % 27.17/4.41 % (3370422)Peak memory usage: 112 MB % 27.17/4.41 % (3370422)Instructions burned: 39 (million) % 27.17/4.41 % (3370426)dis+1010_1_to=kbo:si=on:random_seed=300576152:i=175:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2976 on theBenchmark for (2976ds/175Mi) % 27.17/4.41 % (3370429)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=1510506491:s2a=on:i=483:doe=on:nm=32:rtra=on_2976 on theBenchmark for (2976ds/483Mi) % 27.17/4.41 % (3370398)------------------------------ % 27.17/4.41 % (3370398)------------------------------ % 27.17/4.41 % (3370421)Instruction limit reached! % 27.17/4.41 % (3370421)------------------------------ % 27.17/4.41 % (3370421)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.17/4.41 % (3370421)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.17/4.41 % (3370421)CaDiCaL version: 2.1.3 % 27.17/4.41 % (3370421)Termination reason: Instruction limit % 27.17/4.41 % (3370421)Termination phase: Saturation % 27.17/4.41 % (3370421)Time elapsed: 0.165 s % 27.17/4.41 % (3370421)Peak memory usage: 117 MB % 27.17/4.41 % (3370421)Instructions burned: 129 (million) % 27.17/4.41 % (3370426)Instruction limit reached! % 27.17/4.41 % (3370426)------------------------------ % 27.17/4.41 % (3370426)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.17/4.41 % (3370426)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.17/4.41 % (3370426)CaDiCaL version: 2.1.3 % 27.17/4.41 % (3370426)Termination reason: Instruction limit % 27.17/4.41 % (3370426)Termination phase: Saturation % 27.17/4.41 % (3370426)Time elapsed: 0.101 s % 27.17/4.41 % (3370426)Peak memory usage: 92 MB % 27.17/4.41 % (3370426)Instructions burned: 176 (million) % 27.17/4.41 % (3370428)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=916230494:i=329:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2976 on theBenchmark for (2976ds/329Mi) % 27.17/4.41 % (3370433)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=3924706680:thitd=on:i=215:nm=0:rtra=on:ev=force_2974 on theBenchmark for (2974ds/215Mi) % 27.17/4.41 % (3370437)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=2215464174:i=349:rtra=on_2973 on theBenchmark for (2973ds/349Mi) % 27.17/4.41 % (3370438)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=2921256140:st=2:i=295:rtra=on:ss=axioms_2973 on theBenchmark for (2973ds/295Mi) % 27.17/4.41 % (3370437)Refutation not found, incomplete strategy % 27.17/4.41 % (3370437)------------------------------ % 27.17/4.41 % (3370437)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.17/4.41 % (3370437)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.17/4.41 % (3370437)CaDiCaL version: 2.1.3 % 27.17/4.41 % (3370437)Termination reason: Refutation not found, incomplete strategy % 27.17/4.41 % (3370437)Time elapsed: 0.049 s % 27.17/4.41 % (3370437)Peak memory usage: 116 MB % 27.17/4.41 % (3370437)Instructions burned: 57 (million) % 27.17/4.41 % (3370429)Refutation not found, incomplete strategy % 27.17/4.41 % (3370429)------------------------------ % 27.17/4.41 % (3370429)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.17/4.41 % (3370429)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.17/4.41 % (3370429)CaDiCaL version: 2.1.3 % 27.17/4.41 % (3370429)Termination reason: Refutation not found, incomplete strategy % 27.17/4.41 % (3370429)Time elapsed: 0.339 s % 27.17/4.41 % (3370429)Peak memory usage: 134 MB % 27.17/4.41 % (3370429)Instructions burned: 245 (million) % 27.17/4.41 % (3370406)Instruction limit reached! % 27.17/4.41 % (3370406)------------------------------ % 27.17/4.41 % (3370406)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.17/4.41 % (3370406)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.17/4.41 % (3370406)CaDiCaL version: 2.1.3 % 27.17/4.41 % (3370406)Termination reason: Instruction limit % 27.17/4.41 % (3370406)Termination phase: Saturation % 27.17/4.41 % (3370406)Time elapsed: 0.920 s % 27.17/4.41 % (3370406)Peak memory usage: 94 MB % 27.17/4.41 % (3370406)Instructions burned: 1000 (million) % 27.17/4.41 % (3370439)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=1198357261:i=328:kws=inv_frequency:nm=20:rtra=on_2973 on theBenchmark for (2973ds/328Mi) % 29.21/4.92 % (3370438)Instruction limit reached! % 29.21/4.92 % (3370438)------------------------------ % 29.21/4.92 % (3370438)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.21/4.92 % (3370438)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.21/4.92 % (3370438)CaDiCaL version: 2.1.3 % 29.21/4.92 % (3370438)Termination reason: Instruction limit % 29.21/4.92 % (3370438)Termination phase: Saturation % 29.21/4.92 % (3370438)Time elapsed: 0.242 s % 29.21/4.92 % (3370438)Peak memory usage: 90 MB % 29.21/4.92 % (3370438)Instructions burned: 295 (million) % 29.21/4.92 % (3370428)Instruction limit reached! % 29.21/4.92 % (3370428)------------------------------ % 29.21/4.92 % (3370428)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.21/4.92 % (3370428)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.21/4.92 % (3370428)CaDiCaL version: 2.1.3 % 29.21/4.92 % (3370428)Termination reason: Instruction limit % 29.21/4.92 % (3370428)Termination phase: Saturation % 29.21/4.92 % (3370428)Time elapsed: 0.402 s % 29.21/4.92 % (3370428)Peak memory usage: 119 MB % 29.21/4.92 % (3370428)Instructions burned: 329 (million) % 29.21/4.92 % (3370433)Instruction limit reached! % 29.21/4.92 % (3370433)------------------------------ % 29.21/4.92 % (3370433)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.21/4.92 % (3370433)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.21/4.92 % (3370433)CaDiCaL version: 2.1.3 % 29.21/4.92 % (3370433)Termination reason: Instruction limit % 29.21/4.92 % (3370433)Termination phase: Saturation % 29.21/4.92 % (3370433)Time elapsed: 0.289 s % 29.21/4.92 % (3370433)Peak memory usage: 136 MB % 29.21/4.92 % (3370433)Instructions burned: 215 (million) % 29.21/4.92 % (3370437)------------------------------ % 29.21/4.92 % (3370437)------------------------------ % 29.21/4.92 % (3370445)dis+1010_1_to=lpo:sil=128000:sas=z3:si=on:nwc=5:random_seed=3042972525:i=281:gtgl=2:rtra=on:gtg=all_2971 on theBenchmark for (2971ds/281Mi) % 29.21/4.92 % (3370447)lrs+21_1_to=kbo:sil=128000:thi=neg_eq:si=on:random_seed=3337300506:i=321:canc=force:rtra=on:tac=axiom:ss=axioms:ev=force_2969 on theBenchmark for (2969ds/321Mi) % 29.21/4.92 % (3370439)Instruction limit reached! % 29.21/4.92 % (3370439)------------------------------ % 29.21/4.92 % (3370439)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.21/4.92 % (3370439)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.21/4.92 % (3370439)CaDiCaL version: 2.1.3 % 29.21/4.92 % (3370439)Termination reason: Instruction limit % 29.21/4.92 % (3370439)Termination phase: Saturation % 29.21/4.92 % (3370439)Time elapsed: 0.362 s % 29.21/4.92 % (3370439)Peak memory usage: 118 MB % 29.21/4.92 % (3370439)Instructions burned: 328 (million) % 29.21/4.92 % (3370429)------------------------------ % 29.21/4.92 % (3370429)------------------------------ % 29.21/4.92 % (3370449)lrs+1010_1_to=kbo:tgt=ground:fde=unused:sas=z3:si=on:sp=unary_frequency:gve=force:spb=goal:tha=off:random_seed=4152175321:i=471:thf=on:kws=precedence:rtra=on_2969 on theBenchmark for (2969ds/471Mi) % 29.21/4.92 % (3370446)lrs+1010_1_to=kbo:sil=128000:si=on:sos=on:urr=on:uwa=alasca_main:random_seed=304355372:i=484:doe=on:nm=0:av=off:rtra=on:ss=axioms_2969 on theBenchmark for (2969ds/484Mi) % 29.21/4.92 % (3370448)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=333590610:i=416:rtra=on:gtg=position:ss=axioms_2969 on theBenchmark for (2969ds/416Mi) % 29.21/4.92 % (3370449)Refutation not found, incomplete strategy % 29.21/4.92 % (3370449)------------------------------ % 29.21/4.92 % (3370449)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.21/4.92 % (3370449)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.21/4.92 % (3370449)CaDiCaL version: 2.1.3 % 29.21/4.92 % (3370449)Termination reason: Refutation not found, incomplete strategy % 29.21/4.92 % (3370449)Time elapsed: 0.079 s % 29.21/4.92 % (3370449)Peak memory usage: 117 MB % 29.21/4.92 % (3370449)Instructions burned: 125 (million) % 29.21/4.92 % (3370447)Instruction limit reached! % 29.21/4.92 % (3370447)------------------------------ % 29.21/4.92 % (3370447)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.21/4.92 % (3370447)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.21/4.92 % (3370447)CaDiCaL version: 2.1.3 % 29.21/4.92 % (3370447)Termination reason: Instruction limit % 29.21/4.92 % (3370447)Termination phase: Saturation % 34.21/5.52 % (3370447)Time elapsed: 0.200 s % 34.21/5.52 % (3370447)Peak memory usage: 116 MB % 34.21/5.52 % (3370447)Instructions burned: 322 (million) % 34.21/5.52 % (3370445)Instruction limit reached! % 34.21/5.52 % (3370445)------------------------------ % 34.21/5.52 % (3370445)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.21/5.52 % (3370445)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.21/5.52 % (3370445)CaDiCaL version: 2.1.3 % 34.21/5.52 % (3370445)Termination reason: Instruction limit % 34.21/5.52 % (3370445)Termination phase: Saturation % 34.21/5.52 % (3370445)Time elapsed: 0.322 s % 34.21/5.52 % (3370445)Peak memory usage: 118 MB % 34.21/5.52 % (3370445)Instructions burned: 281 (million) % 34.21/5.52 % (3370452)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=1164045023:avsq=on:i=276:avsqr=1,2:rtra=on_2967 on theBenchmark for (2967ds/276Mi) % 34.21/5.52 % (3370455)lrs+1010_2_to=kbo:sil=128000:tgt=ground:fde=unused:sas=z3:si=on:uwa=off:tha=off:nwc=1:random_seed=801084702:i=375:kws=inv_arity_squared:rtra=on_2967 on theBenchmark for (2967ds/375Mi) % 34.21/5.52 % (3370449)------------------------------ % 34.21/5.52 % (3370449)------------------------------ % 34.21/5.52 % (3370448)Refutation not found, incomplete strategy % 34.21/5.52 % (3370448)------------------------------ % 34.21/5.52 % (3370448)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.21/5.52 % (3370448)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.21/5.52 % (3370448)CaDiCaL version: 2.1.3 % 34.21/5.52 % (3370448)Termination reason: Refutation not found, incomplete strategy % 34.21/5.52 % (3370448)Time elapsed: 0.250 s % 34.21/5.52 % (3370448)Peak memory usage: 117 MB % 34.21/5.52 % (3370448)Instructions burned: 239 (million) % 34.21/5.52 % (3370457)lrs+10_1_to=kbo:sil=128000:tgt=full:sas=z3:si=on:uwa=func_ext:slsqc=1:flr=on:slsq=on:random_seed=3844132355:i=387:bd=preordered:rtra=on:ss=axioms:sgt=8_2965 on theBenchmark for (2965ds/387Mi) % 34.21/5.52 % (3370455)Refutation not found, incomplete strategy % 34.21/5.52 % (3370455)------------------------------ % 34.21/5.52 % (3370455)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.21/5.52 % (3370455)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.21/5.52 % (3370455)CaDiCaL version: 2.1.3 % 34.21/5.52 % (3370455)Termination reason: Refutation not found, incomplete strategy % 34.21/5.52 % (3370455)Time elapsed: 0.130 s % 34.21/5.52 % (3370455)Peak memory usage: 117 MB % 34.21/5.52 % (3370455)Instructions burned: 102 (million) % 34.21/5.52 % (3370446)Instruction limit reached! % 34.21/5.52 % (3370446)------------------------------ % 34.21/5.52 % (3370446)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.21/5.52 % (3370446)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.21/5.52 % (3370446)CaDiCaL version: 2.1.3 % 34.21/5.52 % (3370446)Termination reason: Instruction limit % 34.21/5.52 % (3370446)Termination phase: Saturation % 34.21/5.52 % (3370446)Time elapsed: 0.443 s % 34.21/5.52 % (3370446)Peak memory usage: 90 MB % 34.21/5.52 % (3370446)Instructions burned: 484 (million) % 34.21/5.52 % (3370458)lrs+10_1_to=kbo:sil=128000:fde=none:si=on:norm_ineq=on:urr=on:nwc=0.5:random_seed=3407103840:i=513:kws=frequency:bd=all:rtra=on:gtg=exists_all:ss=axioms:sgt=4_2965 on theBenchmark for (2965ds/513Mi) % 34.21/5.52 % (3370461)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=3108813113:i=334:rtra=on_2964 on theBenchmark for (2964ds/334Mi) % 34.21/5.52 % (3370452)Instruction limit reached! % 34.21/5.52 % (3370452)------------------------------ % 34.21/5.52 % (3370452)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.21/5.52 % (3370452)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.21/5.52 % (3370452)CaDiCaL version: 2.1.3 % 34.21/5.52 % (3370452)Termination reason: Instruction limit % 34.21/5.52 % (3370452)Termination phase: Saturation % 34.21/5.52 % (3370452)Time elapsed: 0.356 s % 34.21/5.52 % (3370452)Peak memory usage: 134 MB % 34.21/5.52 % (3370452)Instructions burned: 276 (million) % 34.21/5.52 % (3370461)Refutation not found, incomplete strategy % 34.21/5.52 % (3370461)------------------------------ % 34.21/5.52 % (3370461)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.21/5.52 % (3370461)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.21/5.52 % (3370461)CaDiCaL version: 2.1.3 % 39.25/6.09 % (3370461)Termination reason: Refutation not found, incomplete strategy % 39.25/6.09 % (3370461)Time elapsed: 0.163 s % 39.25/6.09 % (3370461)Peak memory usage: 134 MB % 39.25/6.09 % (3370461)Instructions burned: 213 (million) % 39.25/6.09 % (3370448)------------------------------ % 39.25/6.09 % (3370448)------------------------------ % 39.25/6.09 % (3370464)lrs+1010_1_to=kbo:sil=64000:sas=cadical:si=on:sos=on:bce=on:random_seed=2430796829:i=359:rtra=on:gtg=exists_top:ss=axioms_2962 on theBenchmark for (2962ds/359Mi) % 39.25/6.09 % (3370455)------------------------------ % 39.25/6.09 % (3370455)------------------------------ % 39.25/6.09 % (3370457)Instruction limit reached! % 39.25/6.09 % (3370457)------------------------------ % 39.25/6.09 % (3370457)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.25/6.09 % (3370457)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.25/6.09 % (3370457)CaDiCaL version: 2.1.3 % 39.25/6.09 % (3370457)Termination reason: Instruction limit % 39.25/6.09 % (3370457)Termination phase: Saturation % 39.25/6.09 % (3370457)Time elapsed: 0.506 s % 39.25/6.09 % (3370457)Peak memory usage: 119 MB % 39.25/6.09 % (3370457)Instructions burned: 387 (million) % 39.25/6.09 % (3370467)dis+1010_1_to=lpo:sil=128000:thi=all:fde=unused:si=on:sp=reverse_arity:tha=off:random_seed=2301569079:i=341:gtgl=2:rtra=on:gtg=exists_sym:ev=force:fsd=on:fsdmm=1_2960 on theBenchmark for (2960ds/341Mi) % 39.25/6.09 % (3370461)------------------------------ % 39.25/6.09 % (3370461)------------------------------ % 39.25/6.09 % (3370458)Instruction limit reached! % 39.25/6.09 % (3370458)------------------------------ % 39.25/6.09 % (3370458)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.25/6.09 % (3370458)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.25/6.09 % (3370458)CaDiCaL version: 2.1.3 % 39.25/6.09 % (3370458)Termination reason: Instruction limit % 39.25/6.09 % (3370458)Termination phase: Saturation % 39.25/6.09 % (3370458)Time elapsed: 0.472 s % 39.25/6.09 % (3370458)Peak memory usage: 92 MB % 39.25/6.09 % (3370458)Instructions burned: 513 (million) % 39.25/6.09 % (3370468)lrs-2_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_max:tha=off:random_seed=2891220090:st=1.5:i=261:sd=1:kws=precedence:rtra=on:ss=axioms_2960 on theBenchmark for (2960ds/261Mi) % 39.25/6.09 % (3370464)Instruction limit reached! % 39.25/6.09 % (3370464)------------------------------ % 39.25/6.09 % (3370464)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.25/6.09 % (3370464)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.25/6.09 % (3370464)CaDiCaL version: 2.1.3 % 39.25/6.09 % (3370464)Termination reason: Instruction limit % 39.25/6.09 % (3370464)Termination phase: Saturation % 39.25/6.09 % (3370464)Time elapsed: 0.351 s % 39.25/6.09 % (3370464)Peak memory usage: 92 MB % 39.25/6.09 % (3370464)Instructions burned: 360 (million) % 39.25/6.09 % (3370470)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=3091566340:s2pl=no:i=235:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2959 on theBenchmark for (2959ds/235Mi) % 39.25/6.09 % (3370468)Refutation not found, incomplete strategy % 39.25/6.09 % (3370468)------------------------------ % 39.25/6.09 % (3370468)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.25/6.09 % (3370468)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.25/6.09 % (3370468)CaDiCaL version: 2.1.3 % 39.25/6.09 % (3370468)Termination reason: Refutation not found, incomplete strategy % 39.25/6.09 % (3370468)Time elapsed: 0.125 s % 39.25/6.09 % (3370468)Peak memory usage: 117 MB % 39.25/6.09 % (3370468)Instructions burned: 98 (million) % 39.25/6.09 % (3370473)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=2194986512:i=146:doe=on:rtra=on_2957 on theBenchmark for (2957ds/146Mi) % 39.25/6.09 % (3370471)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=2479517343:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2958 on theBenchmark for (2958ds/273Mi) % 39.25/6.09 % (3370474)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=4163802589:i=4428:doe=on:fsr=off:rtra=on_2957 on theBenchmark for (2957ds/4428Mi) % 39.25/6.09 % (3370467)Refutation not found, incomplete strategy % 39.25/6.09 % (3370467)------------------------------ % 39.25/6.09 % (3370467)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 43.16/6.88 % (3370467)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.16/6.88 % (3370467)CaDiCaL version: 2.1.3 % 43.16/6.88 % (3370467)Termination reason: Refutation not found, incomplete strategy % 43.16/6.88 % (3370467)Time elapsed: 0.287 s % 43.16/6.88 % (3370467)Peak memory usage: 119 MB % 43.16/6.88 % (3370467)Instructions burned: 230 (million) % 43.16/6.88 % (3370473)Instruction limit reached! % 43.16/6.88 % (3370473)------------------------------ % 43.16/6.88 % (3370473)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 43.16/6.88 % (3370473)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.16/6.88 % (3370473)CaDiCaL version: 2.1.3 % 43.16/6.88 % (3370473)Termination reason: Instruction limit % 43.16/6.88 % (3370473)Termination phase: Saturation % 43.16/6.88 % (3370473)Time elapsed: 0.079 s % 43.16/6.88 % (3370473)Peak memory usage: 90 MB % 43.16/6.88 % (3370473)Instructions burned: 147 (million) % 43.16/6.88 % (3370470)Instruction limit reached! % 43.16/6.88 % (3370470)------------------------------ % 43.16/6.88 % (3370470)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 43.16/6.88 % (3370470)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.16/6.88 % (3370470)CaDiCaL version: 2.1.3 % 43.16/6.88 % (3370470)Termination reason: Instruction limit % 43.16/6.88 % (3370470)Termination phase: Saturation % 43.16/6.88 % (3370470)Time elapsed: 0.284 s % 43.16/6.88 % (3370470)Peak memory usage: 118 MB % 43.16/6.88 % (3370470)Instructions burned: 235 (million) % 43.16/6.88 % (3370477)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=938202768:avsq=on:i=276:avsqr=1,2:rtra=on_2956 on theBenchmark for (2956ds/276Mi) % 43.16/6.88 % (3370468)------------------------------ % 43.16/6.88 % (3370468)------------------------------ % 43.16/6.88 % (3370471)Instruction limit reached! % 43.16/6.88 % (3370471)------------------------------ % 43.16/6.88 % (3370471)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 43.16/6.88 % (3370471)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.16/6.88 % (3370471)CaDiCaL version: 2.1.3 % 43.16/6.88 % (3370471)Termination reason: Instruction limit % 43.16/6.88 % (3370471)Termination phase: Saturation % 43.16/6.88 % (3370471)Time elapsed: 0.283 s % 43.16/6.88 % (3370471)Peak memory usage: 92 MB % 43.16/6.88 % (3370471)Instructions burned: 273 (million) % 43.16/6.88 % (3370481)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=4201831536:i=1052:rtra=on_2955 on theBenchmark for (2955ds/1052Mi) % 43.16/6.88 % (3370467)------------------------------ % 43.16/6.88 % (3370467)------------------------------ % 43.16/6.88 % (3370488)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=4129861209:st=5:i=1054:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2953 on theBenchmark for (2953ds/1054Mi) % 43.16/6.88 % (3370487)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=2076026417:i=655:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2953 on theBenchmark for (2953ds/655Mi) % 43.16/6.88 % (3370477)Instruction limit reached! % 43.16/6.88 % (3370477)------------------------------ % 43.16/6.88 % (3370477)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 43.16/6.88 % (3370477)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.16/6.88 % (3370477)CaDiCaL version: 2.1.3 % 43.16/6.88 % (3370477)Termination reason: Instruction limit % 43.16/6.88 % (3370477)Termination phase: Saturation % 43.16/6.88 % (3370477)Time elapsed: 0.297 s % 43.16/6.88 % (3370477)Peak memory usage: 134 MB % 43.16/6.88 % (3370477)Instructions burned: 276 (million) % 43.16/6.88 % (3370490)lrs-1002_1_to=kbo:sas=z3:si=on:norm_ineq=on:sos=on:tha=some:random_seed=2578033698:i=107:rtra=on_2952 on theBenchmark for (2952ds/107Mi) % 43.16/6.88 % (3370487)Refutation not found, incomplete strategy % 43.16/6.88 % (3370487)------------------------------ % 43.16/6.88 % (3370487)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 43.16/6.88 % (3370487)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.16/6.88 % (3370487)CaDiCaL version: 2.1.3 % 43.16/6.88 % (3370487)Termination reason: Refutation not found, incomplete strategy % 43.16/6.88 % (3370487)Time elapsed: 0.081 s % 43.16/6.88 % (3370487)Peak memory usage: 90 MB % 43.16/6.88 % (3370487)Instructions burned: 86 (million) % 43.16/6.88 % (3370490)Refutation not found, incomplete strategy % 43.16/6.88 % (3370490)------------------------------ % 49.33/7.53 % (3370490)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 49.33/7.53 % (3370490)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 49.33/7.53 % (3370490)CaDiCaL version: 2.1.3 % 49.33/7.53 % (3370490)Termination reason: Refutation not found, incomplete strategy % 49.33/7.53 % (3370490)Time elapsed: 0.087 s % 49.33/7.53 % (3370490)Peak memory usage: 116 MB % 49.33/7.53 % (3370490)Instructions burned: 56 (million) % 49.33/7.53 % (3370488)Refutation not found, incomplete strategy % 49.33/7.53 % (3370488)------------------------------ % 49.33/7.53 % (3370488)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 49.33/7.53 % (3370488)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 49.33/7.53 % (3370488)CaDiCaL version: 2.1.3 % 49.33/7.53 % (3370488)Termination reason: Refutation not found, incomplete strategy % 49.33/7.53 % (3370488)Time elapsed: 0.147 s % 49.33/7.53 % (3370488)Peak memory usage: 91 MB % 49.33/7.53 % (3370488)Instructions burned: 154 (million) % 49.33/7.53 % (3370494)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=2123713628:s2a=on:i=450:doe=on:nm=32:rtra=on_2951 on theBenchmark for (2951ds/450Mi) % 49.33/7.53 % (3370498)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 % 49.33/7.53 % (3370498)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=3230012462:i=1090:aac=none:nm=0:rtra=on:rawr=on_2950 on theBenchmark for (2950ds/1090Mi) % 49.33/7.53 % (3370481)Instruction limit reached! % 49.33/7.53 % (3370481)------------------------------ % 49.33/7.53 % (3370481)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 49.33/7.53 % (3370481)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 49.33/7.53 % (3370481)CaDiCaL version: 2.1.3 % 49.33/7.53 % (3370481)Termination reason: Instruction limit % 49.33/7.53 % (3370481)Termination phase: Saturation % 49.33/7.53 % (3370481)Time elapsed: 0.527 s % 49.33/7.53 % (3370481)Peak memory usage: 93 MB % 49.33/7.53 % (3370481)Instructions burned: 1053 (million) % 49.33/7.53 % (3370498)Refutation not found, incomplete strategy % 49.33/7.53 % (3370498)------------------------------ % 49.33/7.53 % (3370498)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 49.33/7.53 % (3370498)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 49.33/7.53 % (3370498)CaDiCaL version: 2.1.3 % 49.33/7.53 % (3370498)Termination reason: Refutation not found, incomplete strategy % 49.33/7.53 % (3370498)Time elapsed: 0.108 s % 49.33/7.53 % (3370498)Peak memory usage: 116 MB % 49.33/7.53 % (3370498)Instructions burned: 76 (million) % 49.33/7.53 % (3370487)------------------------------ % 49.33/7.53 % (3370487)------------------------------ % 49.33/7.53 % (3370490)------------------------------ % 49.33/7.53 % (3370490)------------------------------ % 49.33/7.53 % (3370488)------------------------------ % 49.33/7.53 % (3370488)------------------------------ % 49.33/7.53 % (3370494)Refutation not found, incomplete strategy % 49.33/7.53 % (3370494)------------------------------ % 49.33/7.53 % (3370494)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 49.33/7.53 % (3370494)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 49.33/7.53 % (3370494)CaDiCaL version: 2.1.3 % 49.33/7.53 % (3370494)Termination reason: Refutation not found, incomplete strategy % 49.33/7.53 % (3370494)Time elapsed: 0.375 s % 49.33/7.53 % (3370494)Peak memory usage: 134 MB % 49.33/7.53 % (3370494)Instructions burned: 281 (million) % 49.33/7.53 % (3370502)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=4148021625:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2947 on theBenchmark for (2947ds/130Mi) % 49.33/7.53 % (3370502)Refutation not found, incomplete strategy % 49.33/7.53 % (3370502)------------------------------ % 49.33/7.53 % (3370502)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 49.33/7.53 % (3370502)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 49.33/7.53 % (3370502)CaDiCaL version: 2.1.3 % 49.33/7.53 % (3370502)Termination reason: Refutation not found, incomplete strategy % 49.33/7.53 % (3370502)Time elapsed: 0.076 s % 49.33/7.53 % (3370502)Peak memory usage: 117 MB % 49.33/7.53 % (3370502)Instructions burned: 105 (million) % 49.33/7.53 % (3370503)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=3877511559:i=312:kws=inv_frequency:nm=20:rtra=on_2945 on theBenchmark for (2945ds/312Mi) % 55.42/8.41 % (3370498)------------------------------ % 55.42/8.41 % (3370498)------------------------------ % 55.42/8.41 % (3370505)ott+10_1_to=kbo:sil=64000:si=on:sp=reverse_frequency:sos=on:random_seed=943695342:i=491:doe=on:rtra=on:gtg=position_2945 on theBenchmark for (2945ds/491Mi) % 55.42/8.41 % (3370506)ott+1011_4:1_to=lpo:sil=64000:si=on:spb=intro:random_seed=3264885561:s2a=on:i=835:s2at=2:rtra=on_2945 on theBenchmark for (2945ds/835Mi) % 55.42/8.41 % (3370502)------------------------------ % 55.42/8.41 % (3370502)------------------------------ % 55.42/8.41 % (3370494)------------------------------ % 55.42/8.41 % (3370494)------------------------------ % 55.42/8.41 % (3370503)Instruction limit reached! % 55.42/8.41 % (3370503)------------------------------ % 55.42/8.41 % (3370503)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 55.42/8.41 % (3370503)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 55.42/8.41 % (3370503)CaDiCaL version: 2.1.3 % 55.42/8.41 % (3370503)Termination reason: Instruction limit % 55.42/8.41 % (3370503)Termination phase: Saturation % 55.42/8.41 % (3370503)Time elapsed: 0.304 s % 55.42/8.41 % (3370503)Peak memory usage: 118 MB % 55.42/8.41 % (3370503)Instructions burned: 312 (million) % 55.42/8.41 % (3370516)ott+1011_2_to=lpo:sil=128000:si=on:sos=on:random_seed=2332606577:i=307:bd=preordered:av=off:rtra=on:ev=cautious_2942 on theBenchmark for (2942ds/307Mi) % 55.42/8.41 % (3370519)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=3092809075:i=776:doe=on:rtra=on_2942 on theBenchmark for (2942ds/776Mi) % 55.42/8.41 % (3370520)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=562457238:s2a=on:i=646:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2941 on theBenchmark for (2941ds/646Mi) % 55.42/8.41 % (3370505)Instruction limit reached! % 55.42/8.41 % (3370505)------------------------------ % 55.42/8.41 % (3370505)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 55.42/8.41 % (3370505)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 55.42/8.41 % (3370505)CaDiCaL version: 2.1.3 % 55.42/8.41 % (3370505)Termination reason: Instruction limit % 55.42/8.41 % (3370505)Termination phase: Saturation % 55.42/8.41 % (3370505)Time elapsed: 0.467 s % 55.42/8.41 % (3370505)Peak memory usage: 91 MB % 55.42/8.41 % (3370505)Instructions burned: 491 (million) % 55.42/8.41 % (3370521)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=2387306042:thitd=on:cond=fast:i=784:nm=30:rtra=on:gtg=all:tac=axiom_2940 on theBenchmark for (2940ds/784Mi) % 55.42/8.41 % (3370516)Instruction limit reached! % 55.42/8.41 % (3370516)------------------------------ % 55.42/8.41 % (3370516)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 55.42/8.41 % (3370516)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 55.42/8.41 % (3370516)CaDiCaL version: 2.1.3 % 55.42/8.41 % (3370516)Termination reason: Instruction limit % 55.42/8.41 % (3370516)Termination phase: Saturation % 55.42/8.41 % (3370516)Time elapsed: 0.344 s % 55.42/8.41 % (3370516)Peak memory usage: 93 MB % 55.42/8.41 % (3370516)Instructions burned: 307 (million) % 55.42/8.41 % (3370519)Instruction limit reached! % 55.42/8.41 % (3370519)------------------------------ % 55.42/8.41 % (3370519)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 55.42/8.41 % (3370519)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 55.42/8.41 % (3370519)CaDiCaL version: 2.1.3 % 55.42/8.41 % (3370519)Termination reason: Instruction limit % 55.42/8.41 % (3370519)Termination phase: Saturation % 55.42/8.41 % (3370519)Time elapsed: 0.400 s % 55.42/8.41 % (3370519)Peak memory usage: 118 MB % 55.42/8.41 % (3370519)Instructions burned: 777 (million) % 55.42/8.41 % (3370520)Refutation not found, incomplete strategy % 55.42/8.41 % (3370520)------------------------------ % 55.42/8.41 % (3370520)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 55.42/8.41 % (3370520)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 55.42/8.41 % (3370520)CaDiCaL version: 2.1.3 % 55.42/8.41 % (3370520)Termination reason: Refutation not found, incomplete strategy % 55.42/8.41 % (3370520)Time elapsed: 0.396 s % 55.42/8.41 % (3370520)Peak memory usage: 136 MB % 55.42/8.41 % (3370520)Instructions burned: 388 (million) % 61.01/9.17 % (3370525)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=4173951402:thitd=on:s2a=on:i=1131:add=on:canc=force:bd=all:rtra=on:tac=axiom:ev=off_2937 on theBenchmark for (2937ds/1131Mi) % 61.01/9.17 % (3370527)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=881169577:s2pl=no:i=246:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2936 on theBenchmark for (2936ds/246Mi) % 61.01/9.17 % (3370506)Instruction limit reached! % 61.01/9.17 % (3370506)------------------------------ % 61.01/9.17 % (3370506)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 61.01/9.17 % (3370506)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.01/9.17 % (3370506)CaDiCaL version: 2.1.3 % 61.01/9.17 % (3370506)Termination reason: Instruction limit % 61.01/9.17 % (3370506)Termination phase: Saturation % 61.01/9.17 % (3370506)Time elapsed: 0.766 s % 61.01/9.17 % (3370506)Peak memory usage: 93 MB % 61.01/9.17 % (3370506)Instructions burned: 835 (million) % 61.01/9.17 % (3370528)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=52238905:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2936 on theBenchmark for (2936ds/775Mi) % 61.01/9.17 % (3370527)Instruction limit reached! % 61.01/9.17 % (3370527)------------------------------ % 61.01/9.17 % (3370527)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 61.01/9.17 % (3370527)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.01/9.17 % (3370527)CaDiCaL version: 2.1.3 % 61.01/9.17 % (3370527)Termination reason: Instruction limit % 61.01/9.17 % (3370527)Termination phase: Saturation % 61.01/9.17 % (3370527)Time elapsed: 0.181 s % 61.01/9.17 % (3370527)Peak memory usage: 118 MB % 61.01/9.17 % (3370527)Instructions burned: 246 (million) % 61.01/9.17 % (3370531)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=4218118850:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2934 on theBenchmark for (2934ds/273Mi) % 61.01/9.17 % (3370520)------------------------------ % 61.01/9.17 % (3370520)------------------------------ % 61.01/9.17 % (3370535)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=2166724928:i=102:nm=16:rtra=on_2933 on theBenchmark for (2933ds/102Mi) % 61.01/9.17 % (3370535)Instruction limit reached! % 61.01/9.17 % (3370535)------------------------------ % 61.01/9.17 % (3370535)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 61.01/9.17 % (3370535)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.01/9.17 % (3370535)CaDiCaL version: 2.1.3 % 61.01/9.17 % (3370535)Termination reason: Instruction limit % 61.01/9.17 % (3370535)Termination phase: Saturation % 61.01/9.17 % (3370535)Time elapsed: 0.052 s % 61.01/9.17 % (3370535)Peak memory usage: 90 MB % 61.01/9.17 % (3370535)Instructions burned: 102 (million) % 61.01/9.17 % (3370537)lrs+10_1_to=lpo:sil=128000:si=on:bsr=unit_only:tha=off:random_seed=3923920935:avsq=on:s2a=on:i=1094:s2at=5:avsqr=4463,131072:rtra=on_2931 on theBenchmark for (2931ds/1094Mi) % 61.01/9.17 % (3370537)Refutation not found, incomplete strategy % 61.01/9.17 % (3370537)------------------------------ % 61.01/9.17 % (3370537)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 61.01/9.17 % (3370537)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.01/9.17 % (3370537)CaDiCaL version: 2.1.3 % 61.01/9.17 % (3370537)Termination reason: Refutation not found, incomplete strategy % 61.01/9.17 % (3370537)Time elapsed: 0.027 s % 61.01/9.17 % (3370537)Peak memory usage: 89 MB % 61.01/9.17 % (3370537)Instructions burned: 51 (million) % 61.01/9.17 % (3370521)Instruction limit reached! % 61.01/9.17 % (3370521)------------------------------ % 61.01/9.17 % (3370521)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 61.01/9.17 % (3370521)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.01/9.17 % (3370521)CaDiCaL version: 2.1.3 % 61.01/9.17 % (3370521)Termination reason: Instruction limit % 61.01/9.17 % (3370521)Termination phase: Saturation % 61.01/9.17 % (3370521)Time elapsed: 0.814 s % 61.01/9.17 % (3370521)Peak memory usage: 120 MB % 61.01/9.17 % (3370521)Instructions burned: 784 (million) % 61.01/9.17 % (3370531)Instruction limit reached! % 61.01/9.17 % (3370531)------------------------------ % 61.01/9.17 % (3370531)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 76.85/11.45 % (3370531)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 76.85/11.45 % (3370531)CaDiCaL version: 2.1.3 % 76.85/11.45 % (3370531)Termination reason: Instruction limit % 76.85/11.45 % (3370531)Termination phase: Saturation % 76.85/11.45 % (3370531)Time elapsed: 0.281 s % 76.85/11.45 % (3370531)Peak memory usage: 92 MB % 76.85/11.45 % (3370531)Instructions burned: 273 (million) % 76.85/11.45 % (3370539)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=1617289533:i=6400:doe=on:fsr=off:rtra=on_2930 on theBenchmark for (2930ds/6400Mi) % 76.85/11.45 % (3370537)------------------------------ % 76.85/11.45 % (3370537)------------------------------ % 76.85/11.45 % (3370542)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=72388266:i=1846:canc=cautious:fsr=off:rtra=on_2929 on theBenchmark for (2929ds/1846Mi) % 76.85/11.45 % (3370541)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=598384226:i=868:doe=on:nm=0:rtra=on:gtg=exists_sym_2929 on theBenchmark for (2929ds/868Mi) % 76.85/11.45 % (3370528)Instruction limit reached! % 76.85/11.45 % (3370528)------------------------------ % 76.85/11.45 % (3370528)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 76.85/11.45 % (3370528)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 76.85/11.45 % (3370528)CaDiCaL version: 2.1.3 % 76.85/11.45 % (3370528)Termination reason: Instruction limit % 76.85/11.45 % (3370528)Termination phase: Saturation % 76.85/11.45 % (3370528)Time elapsed: 0.705 s % 76.85/11.45 % (3370528)Peak memory usage: 92 MB % 76.85/11.45 % (3370528)Instructions burned: 776 (million) % 76.85/11.45 % (3370544)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=3838801369:s2a=on:i=36816:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2926 on theBenchmark for (2926ds/36816Mi) % 76.85/11.45 % (3370541)Refutation not found, incomplete strategy % 76.85/11.45 % (3370541)------------------------------ % 76.85/11.45 % (3370541)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 76.85/11.45 % (3370541)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 76.85/11.45 % (3370541)CaDiCaL version: 2.1.3 % 76.85/11.45 % (3370541)Termination reason: Refutation not found, incomplete strategy % 76.85/11.45 % (3370541)Time elapsed: 0.131 s % 76.85/11.45 % (3370541)Peak memory usage: 117 MB % 76.85/11.45 % (3370541)Instructions burned: 104 (million) % 76.85/11.45 % (3370544)Refutation not found, incomplete strategy % 76.85/11.45 % (3370544)------------------------------ % 76.85/11.45 % (3370544)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 76.85/11.45 % (3370544)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 76.85/11.45 % (3370544)CaDiCaL version: 2.1.3 % 76.85/11.45 % (3370544)Termination reason: Refutation not found, incomplete strategy % 76.85/11.45 % (3370544)Time elapsed: 0.031 s % 76.85/11.45 % (3370544)Peak memory usage: 89 MB % 76.85/11.45 % (3370544)Instructions burned: 53 (million) % 76.85/11.45 % (3370525)Instruction limit reached! % 76.85/11.45 % (3370525)------------------------------ % 76.85/11.45 % (3370525)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 76.85/11.45 % (3370525)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 76.85/11.45 % (3370525)CaDiCaL version: 2.1.3 % 76.85/11.45 % (3370525)Termination reason: Instruction limit % 76.85/11.45 % (3370525)Termination phase: Saturation % 76.85/11.45 % (3370525)Time elapsed: 1.140 s % 76.85/11.45 % (3370525)Peak memory usage: 120 MB % 76.85/11.45 % (3370525)Instructions burned: 1131 (million) % 76.85/11.45 % (3370547)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=3679132836:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2926 on theBenchmark for (2926ds/273Mi) % 76.85/11.45 % (3370544)------------------------------ % 76.85/11.45 % (3370544)------------------------------ % 76.85/11.45 % (3370541)------------------------------ % 76.85/11.45 % (3370541)------------------------------ % 76.85/11.45 % (3370549)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=3761648336:i=863:doe=on:nm=0:rtra=on:gtg=exists_sym_2923 on theBenchmark for (2923ds/863Mi) % 76.85/11.45 % (3370547)Instruction limit reached! % 76.85/11.45 % (3370547)------------------------------ % 76.85/11.45 % (3370547)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 76.85/11.45 % (3370547)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.02/13.43 % (3370547)CaDiCaL version: 2.1.3 % 91.02/13.43 % (3370547)Termination reason: Instruction limit % 91.02/13.43 % (3370547)Termination phase: Saturation % 91.02/13.43 % (3370547)Time elapsed: 0.280 s % 91.02/13.43 % (3370547)Peak memory usage: 92 MB % 91.02/13.43 % (3370547)Instructions burned: 274 (million) % 91.02/13.43 % (3370551)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=2990556304:i=5811:kws=precedence:nm=0:rtra=on_2922 on theBenchmark for (2922ds/5811Mi) % 91.02/13.43 % (3370549)Refutation not found, incomplete strategy % 91.02/13.43 % (3370549)------------------------------ % 91.02/13.43 % (3370549)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 91.02/13.43 % (3370549)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.02/13.43 % (3370549)CaDiCaL version: 2.1.3 % 91.02/13.43 % (3370549)Termination reason: Refutation not found, incomplete strategy % 91.02/13.43 % (3370549)Time elapsed: 0.139 s % 91.02/13.43 % (3370549)Peak memory usage: 117 MB % 91.02/13.43 % (3370549)Instructions burned: 107 (million) % 91.02/13.43 % (3370551)Refutation not found, incomplete strategy % 91.02/13.43 % (3370551)------------------------------ % 91.02/13.43 % (3370551)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 91.02/13.43 % (3370551)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.02/13.43 % (3370551)CaDiCaL version: 2.1.3 % 91.02/13.43 % (3370551)Termination reason: Refutation not found, incomplete strategy % 91.02/13.43 % (3370551)Time elapsed: 0.073 s % 91.02/13.43 % (3370551)Peak memory usage: 117 MB % 91.02/13.43 % (3370551)Instructions burned: 102 (million) % 91.02/13.43 % (3370552)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=3740069222:i=2216:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2920 on theBenchmark for (2920ds/2216Mi) % 91.02/13.43 % (3370554)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=2514218149:i=801:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2920 on theBenchmark for (2920ds/801Mi) % 91.02/13.43 % (3370554)Refutation not found, incomplete strategy % 91.02/13.43 % (3370554)------------------------------ % 91.02/13.43 % (3370554)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 91.02/13.43 % (3370554)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.02/13.43 % (3370554)CaDiCaL version: 2.1.3 % 91.02/13.43 % (3370554)Termination reason: Refutation not found, incomplete strategy % 91.02/13.43 % (3370554)Time elapsed: 0.085 s % 91.02/13.43 % (3370554)Peak memory usage: 90 MB % 91.02/13.43 % (3370554)Instructions burned: 112 (million) % 91.02/13.43 % (3370551)------------------------------ % 91.02/13.43 % (3370551)------------------------------ % 91.02/13.43 % (3370549)------------------------------ % 91.02/13.43 % (3370549)------------------------------ % 91.02/13.43 % (3370558)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=67339805:st=5:i=1026:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2917 on theBenchmark for (2917ds/1026Mi) % 91.02/13.43 % (3370474)Instruction limit reached! % 91.02/13.43 % (3370474)------------------------------ % 91.02/13.43 % (3370474)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 91.02/13.43 % (3370474)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.02/13.43 % (3370474)CaDiCaL version: 2.1.3 % 91.02/13.43 % (3370474)Termination reason: Instruction limit % 91.02/13.43 % (3370474)Termination phase: Saturation % 91.02/13.43 % (3370474)Time elapsed: 4.157 s % 91.02/13.43 % (3370474)Peak memory usage: 113 MB % 91.02/13.43 % (3370474)Instructions burned: 4428 (million) % 91.02/13.43 % (3370558)Refutation not found, incomplete strategy % 91.02/13.43 % (3370558)------------------------------ % 91.02/13.43 % (3370558)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 91.02/13.43 % (3370558)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.02/13.43 % (3370558)CaDiCaL version: 2.1.3 % 91.02/13.43 % (3370558)Termination reason: Refutation not found, incomplete strategy % 91.02/13.43 % (3370558)Time elapsed: 0.090 s % 91.02/13.43 % (3370558)Peak memory usage: 91 MB % 91.02/13.43 % (3370558)Instructions burned: 148 (million) % 91.02/13.43 % (3370554)------------------------------ % 91.02/13.43 % (3370554)------------------------------ % 91.02/13.43 % (3370561)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=1836196972:i=3509:rtra=on_2915 on theBenchmark for (2915ds/3509Mi) % 137.53/20.00 % (3370563)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=2024098275:st=2:i=2127:sd=12:ep=R:rtra=on:ss=axioms_2914 on theBenchmark for (2914ds/2127Mi) % 137.53/20.00 % (3370558)------------------------------ % 137.53/20.00 % (3370558)------------------------------ % 137.53/20.00 % (3370564)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=550671723:i=1959:rtra=on:fsd=on:proc=on_2913 on theBenchmark for (2913ds/1959Mi) % 137.53/20.00 % (3370567)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=1839529016:s2a=on:i=3553:nm=0:rtra=on_2911 on theBenchmark for (2911ds/3553Mi) % 137.53/20.00 % (3370564)Refutation not found, incomplete strategy % 137.53/20.00 % (3370564)------------------------------ % 137.53/20.00 % (3370564)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 137.53/20.00 % (3370564)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 137.53/20.00 % (3370564)CaDiCaL version: 2.1.3 % 137.53/20.00 % (3370564)Termination reason: Refutation not found, incomplete strategy % 137.53/20.00 % (3370564)Time elapsed: 0.149 s % 137.53/20.00 % (3370564)Peak memory usage: 118 MB % 137.53/20.00 % (3370564)Instructions burned: 106 (million) % 137.53/20.00 % (3370542)Instruction limit reached! % 137.53/20.00 % (3370542)------------------------------ % 137.53/20.00 % (3370542)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 137.53/20.00 % (3370542)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 137.53/20.00 % (3370542)CaDiCaL version: 2.1.3 % 137.53/20.00 % (3370542)Termination reason: Instruction limit % 137.53/20.00 % (3370542)Termination phase: Saturation % 137.53/20.00 % (3370542)Time elapsed: 1.896 s % 137.53/20.00 % (3370542)Peak memory usage: 105 MB % 137.53/20.00 % (3370542)Instructions burned: 1846 (million) % 137.53/20.00 % (3370564)------------------------------ % 137.53/20.00 % (3370564)------------------------------ % 137.53/20.00 % (3370570)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=725815312:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2907 on theBenchmark for (2907ds/3201Mi) % 137.53/20.00 % (3370572)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=1624500794:thitd=on:cond=on:i=4093:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2905 on theBenchmark for (2905ds/4093Mi) % 137.53/20.00 % (3370552)Instruction limit reached! % 137.53/20.00 % (3370552)------------------------------ % 137.53/20.00 % (3370552)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 137.53/20.00 % (3370552)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 137.53/20.00 % (3370552)CaDiCaL version: 2.1.3 % 137.53/20.00 % (3370552)Termination reason: Instruction limit % 137.53/20.00 % (3370552)Termination phase: Saturation % 137.53/20.00 % (3370552)Time elapsed: 2.039 s % 137.53/20.00 % (3370552)Peak memory usage: 128 MB % 137.53/20.00 % (3370552)Instructions burned: 2216 (million) % 137.53/20.00 % (3370576)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=1844250541:cond=fast:i=21173:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2897 on theBenchmark for (2897ds/21173Mi) % 137.53/20.00 % (3370563)Instruction limit reached! % 137.53/20.00 % (3370563)------------------------------ % 137.53/20.00 % (3370563)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 137.53/20.00 % (3370563)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 137.53/20.00 % (3370563)CaDiCaL version: 2.1.3 % 137.53/20.00 % (3370563)Termination reason: Instruction limit % 137.53/20.00 % (3370563)Termination phase: Saturation % 137.53/20.00 % (3370563)Time elapsed: 1.767 s % 137.53/20.00 % (3370563)Peak memory usage: 100 MB % 137.53/20.00 % (3370563)Instructions burned: 2128 (million) % 137.53/20.00 % (3370578)lrs+11_1_to=lpo:thi=all:sas=z3:si=on:fd=off:sac=on:slsq=on:random_seed=2579831743:avsq=on:i=10544:avsqr=17,4:canc=force:rtra=on:gtg=exists_top:er=filter_2894 on theBenchmark for (2894ds/10544Mi) % 137.53/20.00 % (3370567)Instruction limit reached! % 137.53/20.00 % (3370567)------------------------------ % 137.53/20.00 % (3370567)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 137.53/20.00 % (3370567)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 137.53/20.00 % (3370567)CaDiCaL version: 2.1.3 % 137.53/20.00 % (3370567)Termination reason: Instruction limit % 137.53/20.00 % (3370567)Termination phase: Saturation % 167.68/24.17 % (3370567)Time elapsed: 1.940 s % 167.68/24.17 % (3370567)Peak memory usage: 99 MB % 167.68/24.17 % (3370567)Instructions burned: 3553 (million) % 167.68/24.17 % (3370580)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=3749670852:avsq=on:i=1262:avsqr=1,16:rtra=on:rawr=on_2889 on theBenchmark for (2889ds/1262Mi) % 167.68/24.17 % (3370580)Refutation not found, incomplete strategy % 167.68/24.17 % (3370580)------------------------------ % 167.68/24.17 % (3370580)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 167.68/24.17 % (3370580)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 167.68/24.17 % (3370580)CaDiCaL version: 2.1.3 % 167.68/24.17 % (3370580)Termination reason: Refutation not found, incomplete strategy % 167.68/24.17 % (3370580)Time elapsed: 0.130 s % 167.68/24.17 % (3370580)Peak memory usage: 117 MB % 167.68/24.17 % (3370580)Instructions burned: 228 (million) % 167.68/24.17 % (3370580)------------------------------ % 167.68/24.17 % (3370580)------------------------------ % 167.68/24.17 % (3370582)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=2352930209:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2883 on theBenchmark for (2883ds/775Mi) % 167.68/24.17 % (3370582)Instruction limit reached! % 167.68/24.17 % (3370582)------------------------------ % 167.68/24.17 % (3370582)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 167.68/24.17 % (3370582)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 167.68/24.17 % (3370582)CaDiCaL version: 2.1.3 % 167.68/24.17 % (3370582)Termination reason: Instruction limit % 167.68/24.17 % (3370582)Termination phase: Saturation % 167.68/24.17 % (3370582)Time elapsed: 0.365 s % 167.68/24.17 % (3370582)Peak memory usage: 92 MB % 167.68/24.17 % (3370582)Instructions burned: 775 (million) % 167.68/24.17 % (3370570)Instruction limit reached! % 167.68/24.17 % (3370570)------------------------------ % 167.68/24.17 % (3370570)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 167.68/24.17 % (3370570)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 167.68/24.17 % (3370570)CaDiCaL version: 2.1.3 % 167.68/24.17 % (3370570)Termination reason: Instruction limit % 167.68/24.17 % (3370570)Termination phase: Saturation % 167.68/24.17 % (3370570)Time elapsed: 2.759 s % 167.68/24.17 % (3370570)Peak memory usage: 101 MB % 167.68/24.17 % (3370570)Instructions burned: 3202 (million) % 167.68/24.17 % (3370584)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=70124101:i=270:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2878 on theBenchmark for (2878ds/270Mi) % 167.68/24.17 % (3370561)Instruction limit reached! % 167.68/24.17 % (3370561)------------------------------ % 167.68/24.17 % (3370561)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 167.68/24.17 % (3370561)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 167.68/24.17 % (3370561)CaDiCaL version: 2.1.3 % 167.68/24.17 % (3370561)Termination reason: Instruction limit % 167.68/24.17 % (3370561)Termination phase: Saturation % 167.68/24.17 % (3370561)Time elapsed: 3.720 s % 167.68/24.17 % (3370561)Peak memory usage: 102 MB % 167.68/24.17 % (3370561)Instructions burned: 3509 (million) % 167.68/24.17 % (3370585)ott+10_128_isp=bottom:to=lpo:sil=128000:si=on:urr=on:uwa=alasca_main:sac=on:slsq=on:random_seed=2604262300:i=17165:aac=none:doe=on:rtra=on:gtg=exists_all_2876 on theBenchmark for (2876ds/17165Mi) % 167.68/24.17 % (3370584)Instruction limit reached! % 167.68/24.17 % (3370584)------------------------------ % 167.68/24.17 % (3370584)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 167.68/24.17 % (3370584)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 167.68/24.17 % (3370584)CaDiCaL version: 2.1.3 % 167.68/24.17 % (3370584)Termination reason: Instruction limit % 167.68/24.17 % (3370584)Termination phase: Saturation % 167.68/24.17 % (3370584)Time elapsed: 0.176 s % 167.68/24.17 % (3370584)Peak memory usage: 92 MB % 167.68/24.17 % (3370584)Instructions burned: 270 (million) % 167.68/24.17 % (3370587)lrs+2_10_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_main:tha=some:random_seed=3002597783:s2a=on:i=13094:s2at=-1:rtra=on_2875 on theBenchmark for (2875ds/13094Mi) % 167.68/24.17 % (3370589)lrs+10_1_to=lpo:sil=128000:si=on:sp=occurrence:random_seed=972284463:st=2:i=12633:rtra=on:ss=axioms_2874 on theBenchmark for (2874ds/12633Mi) % 167.68/24.17 % (3370539)Instruction limit reached! % 167.68/24.17 % (3370539)------------------------------ % 167.68/24.17 % (3370539)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 185.16/26.76 % (3370539)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 185.16/26.76 % (3370539)CaDiCaL version: 2.1.3 % 185.16/26.76 % (3370539)Termination reason: Instruction limit % 185.16/26.76 % (3370539)Termination phase: Saturation % 185.16/26.76 % (3370539)Time elapsed: 5.778 s % 185.16/26.76 % (3370539)Peak memory usage: 123 MB % 185.16/26.76 % (3370539)Instructions burned: 6401 (million) % 185.16/26.76 % (3370592)dis+1011_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_frequency:lsd=20:nwc=3:random_seed=2631587885:i=1783:rtra=on:gtg=position_2870 on theBenchmark for (2870ds/1783Mi) % 185.16/26.76 % (3370572)Instruction limit reached! % 185.16/26.76 % (3370572)------------------------------ % 185.16/26.76 % (3370572)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 185.16/26.76 % (3370572)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 185.16/26.76 % (3370572)CaDiCaL version: 2.1.3 % 185.16/26.76 % (3370572)Termination reason: Instruction limit % 185.16/26.76 % (3370572)Termination phase: Saturation % 185.16/26.76 % (3370572)Time elapsed: 4.274 s % 185.16/26.76 % (3370572)Peak memory usage: 150 MB % 185.16/26.76 % (3370572)Instructions burned: 4094 (million) % 185.16/26.76 % (3370594)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=806122270:i=5451:aac=none:doe=on:nm=0:rtra=on:amm=off:gtg=position_2859 on theBenchmark for (2859ds/5451Mi) % 185.16/26.76 % (3370592)Instruction limit reached! % 185.16/26.76 % (3370592)------------------------------ % 185.16/26.76 % (3370592)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 185.16/26.76 % (3370592)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 185.16/26.76 % (3370592)CaDiCaL version: 2.1.3 % 185.16/26.76 % (3370592)Termination reason: Instruction limit % 185.16/26.76 % (3370592)Termination phase: Saturation % 185.16/26.76 % (3370592)Time elapsed: 1.704 s % 185.16/26.76 % (3370592)Peak memory usage: 126 MB % 185.16/26.76 % (3370592)Instructions burned: 1783 (million) % 185.16/26.76 % (3370600)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=1768925408:i=4975:doe=on:nm=0:rtra=on:gtg=exists_sym_2849 on theBenchmark for (2849ds/4975Mi) % 185.16/26.76 % (3370600)Refutation not found, incomplete strategy % 185.16/26.76 % (3370600)------------------------------ % 185.16/26.76 % (3370600)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 185.16/26.76 % (3370600)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 185.16/26.76 % (3370600)CaDiCaL version: 2.1.3 % 185.16/26.76 % (3370600)Termination reason: Refutation not found, incomplete strategy % 185.16/26.76 % (3370600)Time elapsed: 0.134 s % 185.16/26.76 % (3370600)Peak memory usage: 117 MB % 185.16/26.76 % (3370600)Instructions burned: 105 (million) % 185.16/26.76 % (3370600)------------------------------ % 185.16/26.76 % (3370600)------------------------------ % 185.16/26.76 % (3370602)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=2874899527:i=2076:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2841 on theBenchmark for (2841ds/2076Mi) % 185.16/26.76 % (3370602)Instruction limit reached! % 185.16/26.76 % (3370602)------------------------------ % 185.16/26.76 % (3370602)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 185.16/26.76 % (3370602)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 185.16/26.76 % (3370602)CaDiCaL version: 2.1.3 % 185.16/26.76 % (3370602)Termination reason: Instruction limit % 185.16/26.76 % (3370602)Termination phase: Saturation % 185.16/26.76 % (3370602)Time elapsed: 1.916 s % 185.16/26.76 % (3370602)Peak memory usage: 125 MB % 185.16/26.76 % (3370602)Instructions burned: 2076 (million) % 185.16/26.76 % (3370606)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=3559162576:i=5145:rtra=on_2819 on theBenchmark for (2819ds/5145Mi) % 185.16/26.76 % (3370594)Instruction limit reached! % 185.16/26.76 % (3370594)------------------------------ % 185.16/26.76 % (3370594)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 185.16/26.76 % (3370594)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 185.16/26.76 % (3370594)CaDiCaL version: 2.1.3 % 185.16/26.76 % (3370594)Termination reason: Instruction limit % 185.16/26.76 % (3370594)Termination phase: Saturation % 185.16/26.76 % (3370594)Time elapsed: 5.196 s % 185.16/26.76 % (3370594)Peak memory usage: 148 MB % 185.16/26.76 % (3370594)Instructions burned: 5451 (million) % 197.47/28.55 % (3370608)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=2667502719:i=3509:rtra=on_2804 on theBenchmark for (2804ds/3509Mi) % 197.47/28.55 % (3370589)Instruction limit reached! % 197.47/28.55 % (3370589)------------------------------ % 197.47/28.55 % (3370589)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 197.47/28.55 % (3370589)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 197.47/28.55 % (3370589)CaDiCaL version: 2.1.3 % 197.47/28.55 % (3370589)Termination reason: Instruction limit % 197.47/28.55 % (3370589)Termination phase: Saturation % 197.47/28.55 % (3370589)Time elapsed: 7.463 s % 197.47/28.55 % (3370589)Peak memory usage: 117 MB % 197.47/28.55 % (3370589)Instructions burned: 12634 (million) % 197.47/28.55 % (3370610)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=415308737:st=2:i=13800:sd=12:ep=R:rtra=on:ss=axioms_2797 on theBenchmark for (2797ds/13800Mi) % 197.47/28.55 % (3370578)Instruction limit reached! % 197.47/28.55 % (3370578)------------------------------ % 197.47/28.55 % (3370578)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 197.47/28.55 % (3370578)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 197.47/28.55 % (3370578)CaDiCaL version: 2.1.3 % 197.47/28.55 % (3370578)Termination reason: Instruction limit % 197.47/28.55 % (3370578)Termination phase: Saturation % 197.47/28.55 % (3370578)Time elapsed: 9.998 s % 197.47/28.55 % (3370578)Peak memory usage: 174 MB % 197.47/28.55 % (3370578)Instructions burned: 10544 (million) % 197.47/28.55 % (3370612)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=250239984:i=1412:rtra=on:fsd=on:proc=on_2790 on theBenchmark for (2790ds/1412Mi) % 197.47/28.55 % (3370612)Refutation not found, incomplete strategy % 197.47/28.55 % (3370612)------------------------------ % 197.47/28.55 % (3370612)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 197.47/28.55 % (3370612)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 197.47/28.55 % (3370612)CaDiCaL version: 2.1.3 % 197.47/28.55 % (3370612)Termination reason: Refutation not found, incomplete strategy % 197.47/28.55 % (3370612)Time elapsed: 0.139 s % 197.47/28.55 % (3370612)Peak memory usage: 118 MB % 197.47/28.55 % (3370612)Instructions burned: 96 (million) % 197.47/28.55 % (3370612)------------------------------ % 197.47/28.55 % (3370612)------------------------------ % 197.47/28.55 % (3370616)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 % 197.47/28.55 % (3370616)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=1226669095:i=11747:aac=none:nm=0:rtra=on:rawr=on_2782 on theBenchmark for (2782ds/11747Mi) % 197.47/28.55 % (3370616)Refutation not found, incomplete strategy % 197.47/28.55 % (3370616)------------------------------ % 197.47/28.55 % (3370616)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 197.47/28.55 % (3370616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 197.47/28.55 % (3370616)CaDiCaL version: 2.1.3 % 197.47/28.55 % (3370616)Termination reason: Refutation not found, incomplete strategy % 197.47/28.55 % (3370616)Time elapsed: 0.110 s % 197.47/28.55 % (3370616)Peak memory usage: 117 MB % 197.47/28.55 % (3370616)Instructions burned: 80 (million) % 197.47/28.55 % (3370616)------------------------------ % 197.47/28.55 % (3370616)------------------------------ % 197.47/28.55 % (3370618)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=4127677522:s2a=on:i=3553:nm=0:rtra=on_2774 on theBenchmark for (2774ds/3553Mi) % 197.47/28.55 % (3370606)Instruction limit reached! % 197.47/28.55 % (3370606)------------------------------ % 197.47/28.55 % (3370606)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 197.47/28.55 % (3370606)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 197.47/28.55 % (3370606)CaDiCaL version: 2.1.3 % 197.47/28.55 % (3370606)Termination reason: Instruction limit % 197.47/28.55 % (3370606)Termination phase: Saturation % 197.47/28.55 % (3370606)Time elapsed: 4.550 s % 197.47/28.55 % (3370606)Peak memory usage: 101 MB % 197.47/28.55 % (3370606)Instructions burned: 5145 (million) % 197.47/28.55 % (3370620)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=1102849882:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2771 on theBenchmark for (2771ds/3201Mi) % 197.47/28.55 % (3370608)Instruction limit reached! % 225.43/32.34 % (3370608)------------------------------ % 225.43/32.34 % (3370608)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 225.43/32.34 % (3370608)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 225.43/32.34 % (3370608)CaDiCaL version: 2.1.3 % 225.43/32.34 % (3370608)Termination reason: Instruction limit % 225.43/32.34 % (3370608)Termination phase: Saturation % 225.43/32.34 % (3370608)Time elapsed: 3.849 s % 225.43/32.34 % (3370608)Peak memory usage: 102 MB % 225.43/32.34 % (3370608)Instructions burned: 3509 (million) % 225.43/32.34 % (3370587)Instruction limit reached! % 225.43/32.34 % (3370587)------------------------------ % 225.43/32.34 % (3370587)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 225.43/32.34 % (3370587)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 225.43/32.34 % (3370587)CaDiCaL version: 2.1.3 % 225.43/32.34 % (3370587)Termination reason: Instruction limit % 225.43/32.34 % (3370587)Termination phase: Saturation % 225.43/32.34 % (3370587)Time elapsed: 11.059 s % 225.43/32.34 % (3370587)Peak memory usage: 119 MB % 225.43/32.34 % (3370587)Instructions burned: 13095 (million) % 225.43/32.34 % (3370623)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=3351137762:cond=fast:i=20260:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2762 on theBenchmark for (2762ds/20260Mi) % 225.43/32.34 % (3370622)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=3591273846:thitd=on:cond=on:i=4081:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2762 on theBenchmark for (2762ds/4081Mi) % 225.43/32.34 % (3370618)Instruction limit reached! % 225.43/32.34 % (3370618)------------------------------ % 225.43/32.34 % (3370618)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 225.43/32.34 % (3370618)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 225.43/32.34 % (3370618)CaDiCaL version: 2.1.3 % 225.43/32.34 % (3370618)Termination reason: Instruction limit % 225.43/32.34 % (3370618)Termination phase: Saturation % 225.43/32.34 % (3370618)Time elapsed: 2.769 s % 225.43/32.34 % (3370618)Peak memory usage: 100 MB % 225.43/32.34 % (3370618)Instructions burned: 3554 (million) % 225.43/32.34 % (3370620)Instruction limit reached! % 225.43/32.34 % (3370620)------------------------------ % 225.43/32.34 % (3370620)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 225.43/32.34 % (3370620)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 225.43/32.34 % (3370620)CaDiCaL version: 2.1.3 % 225.43/32.34 % (3370620)Termination reason: Instruction limit % 225.43/32.34 % (3370620)Termination phase: Saturation % 225.43/32.34 % (3370620)Time elapsed: 2.671 s % 225.43/32.34 % (3370620)Peak memory usage: 97 MB % 225.43/32.34 % (3370620)Instructions burned: 3202 (million) % 225.43/32.34 % (3370626)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=3333723135:s2a=on:i=58627:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2744 on theBenchmark for (2744ds/58627Mi) % 225.43/32.34 % (3370626)Refutation not found, incomplete strategy % 225.43/32.34 % (3370626)------------------------------ % 225.43/32.34 % (3370626)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 225.43/32.34 % (3370626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 225.43/32.34 % (3370626)CaDiCaL version: 2.1.3 % 225.43/32.34 % (3370626)Termination reason: Refutation not found, incomplete strategy % 225.43/32.34 % (3370626)Time elapsed: 0.027 s % 225.43/32.34 % (3370626)Peak memory usage: 90 MB % 225.43/32.34 % (3370626)Instructions burned: 55 (million) % 225.43/32.34 % (3370627)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=2982975289:avsq=on:i=6258:avsqr=1,16:rtra=on:rawr=on_2742 on theBenchmark for (2742ds/6258Mi) % 225.43/32.34 % (3370626)------------------------------ % 225.43/32.34 % (3370626)------------------------------ % 225.43/32.34 % (3370627)Refutation not found, incomplete strategy % 225.43/32.34 % (3370627)------------------------------ % 225.43/32.34 % (3370627)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 225.43/32.34 % (3370627)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 225.43/32.34 % (3370627)CaDiCaL version: 2.1.3 % 225.43/32.34 % (3370627)Termination reason: Refutation not found, incomplete strategy % 225.43/32.34 % (3370627)Time elapsed: 0.228 s % 225.43/32.34 % (3370627)Peak memory usage: 117 MB % 225.43/32.34 % (3370627)Instructions burned: 211 (million) % 225.43/32.34 % (3370630)ott+10_128_isp=bottom:to=lpo:sil=128000:si=on:urr=on:uwa=alasca_main:sac=on:slsq=on:random_seed=1409751880:i=34001:aac=none:doe=on:rtra=on:gtg=exists_all_2739 on theBenchmark for (2739ds/34001Mi) % 243.87/34.90 % (3370627)------------------------------ % 243.87/34.90 % (3370627)------------------------------ % 243.87/34.90 % (3370632)lrs+2_10_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_main:tha=some:random_seed=2394873265:s2a=on:i=71622:s2at=-1:rtra=on_2733 on theBenchmark for (2733ds/71622Mi) % 243.87/34.90 % (3370576)Instruction limit reached! % 243.87/34.90 % (3370576)------------------------------ % 243.87/34.90 % (3370576)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 243.87/34.90 % (3370576)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 243.87/34.90 % (3370576)CaDiCaL version: 2.1.3 % 243.87/34.90 % (3370576)Termination reason: Instruction limit % 243.87/34.90 % (3370576)Termination phase: Saturation % 243.87/34.90 % (3370576)Time elapsed: 16.425 s % 243.87/34.90 % (3370576)Peak memory usage: 137 MB % 243.87/34.90 % (3370576)Instructions burned: 21174 (million) % 243.87/34.90 % (3370636)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=2459569422:i=24001:kws=precedence:nm=0:rtra=on_2730 on theBenchmark for (2730ds/24001Mi) % 243.87/34.90 % (3370636)Refutation not found, incomplete strategy % 243.87/34.90 % (3370636)------------------------------ % 243.87/34.90 % (3370636)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 243.87/34.90 % (3370636)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 243.87/34.90 % (3370636)CaDiCaL version: 2.1.3 % 243.87/34.90 % (3370636)Termination reason: Refutation not found, incomplete strategy % 243.87/34.90 % (3370636)Time elapsed: 0.139 s % 243.87/34.90 % (3370636)Peak memory usage: 117 MB % 243.87/34.90 % (3370636)Instructions burned: 112 (million) % 243.87/34.90 % (3370610)Instruction limit reached! % 243.87/34.90 % (3370610)------------------------------ % 243.87/34.90 % (3370610)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 243.87/34.90 % (3370610)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 243.87/34.90 % (3370610)CaDiCaL version: 2.1.3 % 243.87/34.90 % (3370610)Termination reason: Instruction limit % 243.87/34.90 % (3370610)Termination phase: Saturation % 243.87/34.90 % (3370610)Time elapsed: 7.070 s % 243.87/34.90 % (3370610)Peak memory usage: 134 MB % 243.87/34.90 % (3370610)Instructions burned: 13800 (million) % 243.87/34.90 % (3370585)Instruction limit reached! % 243.87/34.90 % (3370585)------------------------------ % 243.87/34.90 % (3370585)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 243.87/34.90 % (3370585)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 243.87/34.90 % (3370585)CaDiCaL version: 2.1.3 % 243.87/34.90 % (3370585)Termination reason: Instruction limit % 243.87/34.90 % (3370585)Termination phase: Saturation % 243.87/34.90 % (3370585)Time elapsed: 14.992 s % 243.87/34.90 % (3370585)Peak memory usage: 125 MB % 243.87/34.90 % (3370585)Instructions burned: 17166 (million) % 243.87/34.90 % (3370636)------------------------------ % 243.87/34.90 % (3370636)------------------------------ % 243.87/34.90 % (3370639)dis+21_20_to=lakbo:si=on:alasca=on:sp=const_max:uwa=alasca_main:sac=on:random_seed=1806303666:s2a=on:i=83971:s2at=4:bd=all:ins=1:rtra=on_2724 on theBenchmark for (2724ds/83971Mi) % 243.87/34.90 % (3370638)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=1088034717:i=2076:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2724 on theBenchmark for (2724ds/2076Mi) % 243.87/34.90 % (3370640)lrs+1011_5:1_to=lpo:sil=128000:sas=z3:si=on:norm_ineq=on:tha=some:random_seed=3424468719:i=83944:rtra=on_2722 on theBenchmark for (2722ds/83944Mi) % 243.87/34.90 % (3370640)Refutation not found, incomplete strategy % 243.87/34.90 % (3370640)------------------------------ % 243.87/34.90 % (3370640)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 243.87/34.90 % (3370640)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 243.87/34.90 % (3370640)CaDiCaL version: 2.1.3 % 243.87/34.90 % (3370640)Termination reason: Refutation not found, incomplete strategy % 243.87/34.90 % (3370640)Time elapsed: 0.077 s % 243.87/34.90 % (3370640)Peak memory usage: 116 MB % 243.87/34.90 % (3370640)Instructions burned: 48 (million) % 243.87/34.90 % (3370622)Instruction limit reached! % 243.87/34.90 % (3370622)------------------------------ % 243.87/34.90 % (3370622)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 243.87/34.90 % (3370622)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 266.50/38.10 % (3370622)CaDiCaL version: 2.1.3 % 266.50/38.10 % (3370622)Termination reason: Instruction limit % 266.50/38.10 % (3370622)Termination phase: Saturation % 266.50/38.10 % (3370622)Time elapsed: 4.093 s % 266.50/38.10 % (3370622)Peak memory usage: 148 MB % 266.50/38.10 % (3370622)Instructions burned: 4081 (million) % 266.50/38.10 % (3370639)Refutation not found, incomplete strategy % 266.50/38.10 % (3370639)------------------------------ % 266.50/38.10 % (3370639)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 266.50/38.10 % (3370639)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 266.50/38.10 % (3370639)CaDiCaL version: 2.1.3 % 266.50/38.10 % (3370639)Termination reason: Refutation not found, incomplete strategy % 266.50/38.10 % (3370639)Time elapsed: 0.380 s % 266.50/38.10 % (3370639)Peak memory usage: 94 MB % 266.50/38.10 % (3370639)Instructions burned: 443 (million) % 266.50/38.10 % (3370644)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=1312129830:i=9201:rtra=on_2718 on theBenchmark for (2718ds/9201Mi) % 266.50/38.10 % (3370640)------------------------------ % 266.50/38.10 % (3370640)------------------------------ % 266.50/38.10 % (3370639)------------------------------ % 266.50/38.10 % (3370639)------------------------------ % 266.50/38.10 % (3370646)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 % 266.50/38.10 % (3370646)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=3539479011:i=6806:aac=none:nm=0:rtra=on:rawr=on_2715 on theBenchmark for (2715ds/6806Mi) % 266.50/38.10 % (3370646)Refutation not found, incomplete strategy % 266.50/38.10 % (3370646)------------------------------ % 266.50/38.10 % (3370646)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 266.50/38.10 % (3370646)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 266.50/38.10 % (3370646)CaDiCaL version: 2.1.3 % 266.50/38.10 % (3370646)Termination reason: Refutation not found, incomplete strategy % 266.50/38.10 % (3370646)Time elapsed: 0.097 s % 266.50/38.10 % (3370646)Peak memory usage: 117 MB % 266.50/38.10 % (3370646)Instructions burned: 65 (million) % 266.50/38.10 % (3370647)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=2892952775:s2a=on:i=3553:nm=0:rtra=on_2713 on theBenchmark for (2713ds/3553Mi) % 266.50/38.10 % (3370646)------------------------------ % 266.50/38.10 % (3370646)------------------------------ % 266.50/38.10 % (3370650)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=1292152737:thitd=on:cond=on:i=2064:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2707 on theBenchmark for (2707ds/2064Mi) % 266.50/38.10 % (3370638)Instruction limit reached! % 266.50/38.10 % (3370638)------------------------------ % 266.50/38.10 % (3370638)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 266.50/38.10 % (3370638)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 266.50/38.10 % (3370638)CaDiCaL version: 2.1.3 % 266.50/38.10 % (3370638)Termination reason: Instruction limit % 266.50/38.10 % (3370638)Termination phase: Saturation % 266.50/38.10 % (3370638)Time elapsed: 1.893 s % 266.50/38.10 % (3370638)Peak memory usage: 124 MB % 266.50/38.10 % (3370638)Instructions burned: 2076 (million) % 266.50/38.10 % (3370654)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=862364917:cond=fast:i=20260:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2702 on theBenchmark for (2702ds/20260Mi) % 266.50/38.10 % (3370650)Instruction limit reached! % 266.50/38.10 % (3370650)------------------------------ % 266.50/38.10 % (3370650)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 266.50/38.10 % (3370650)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 266.50/38.10 % (3370650)CaDiCaL version: 2.1.3 % 266.50/38.10 % (3370650)Termination reason: Instruction limit % 266.50/38.10 % (3370650)Termination phase: Saturation % 266.50/38.10 % (3370650)Time elapsed: 2.041 s % 266.50/38.10 % (3370650)Peak memory usage: 143 MB % 266.50/38.10 % (3370650)Instructions burned: 2064 (million) % 266.50/38.10 % (3370661)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=3909967365:avsq=on:i=1244:avsqr=1,16:rtra=on:rawr=on_2684 on theBenchmark for (2684ds/1244Mi) % 271.93/39.05 % (3370661)Refutation not found, incomplete strategy % 271.93/39.05 % (3370661)------------------------------ % 271.93/39.05 % (3370661)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 271.93/39.05 % (3370661)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 271.93/39.05 % (3370661)CaDiCaL version: 2.1.3 % 271.93/39.05 % (3370661)Termination reason: Refutation not found, incomplete strategy % 271.93/39.05 % (3370661)Time elapsed: 0.236 s % 271.93/39.05 % (3370661)Peak memory usage: 117 MB % 271.93/39.05 % (3370661)Instructions burned: 229 (million) % 271.93/39.05 % (3370647)Instruction limit reached! % 271.93/39.05 % (3370647)------------------------------ % 271.93/39.05 % (3370647)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 271.93/39.05 % (3370647)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 271.93/39.05 % (3370647)CaDiCaL version: 2.1.3 % 271.93/39.05 % (3370647)Termination reason: Instruction limit % 271.93/39.05 % (3370647)Termination phase: Saturation % 271.93/39.05 % (3370647)Time elapsed: 3.481 s % 271.93/39.05 % (3370647)Peak memory usage: 100 MB % 271.93/39.05 % (3370647)Instructions burned: 3554 (million) % 271.93/39.05 % (3370661)------------------------------ % 271.93/39.05 % (3370661)------------------------------ % 271.93/39.05 % (3370676)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=3935582470:i=58261:doe=on:nm=0:rtra=on:gtg=exists_sym_2676 on theBenchmark for (2676ds/58261Mi) % 271.93/39.05 % (3370677)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 % 271.93/39.05 % (3370676)Refutation not found, incomplete strategy % 271.93/39.05 % (3370676)------------------------------ % 271.93/39.05 % (3370676)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 271.93/39.05 % (3370676)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 271.93/39.05 % (3370676)CaDiCaL version: 2.1.3 % 271.93/39.05 % (3370676)Termination reason: Refutation not found, incomplete strategy % 271.93/39.05 % (3370676)Time elapsed: 0.140 s % 271.93/39.05 % (3370676)Peak memory usage: 117 MB % 271.93/39.05 % (3370676)Instructions burned: 108 (million) % 271.93/39.05 % (3370677)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=2689783683:i=6806:aac=none:nm=0:rtra=on:rawr=on_2674 on theBenchmark for (2674ds/6806Mi) % 271.93/39.05 % (3370677)Refutation not found, incomplete strategy % 271.93/39.05 % (3370677)------------------------------ % 271.93/39.05 % (3370677)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 271.93/39.05 % (3370677)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 271.93/39.05 % (3370677)CaDiCaL version: 2.1.3 % 271.93/39.05 % (3370677)Termination reason: Refutation not found, incomplete strategy % 271.93/39.05 % (3370677)Time elapsed: 0.102 s % 271.93/39.05 % (3370677)Peak memory usage: 117 MB % 271.93/39.05 % (3370677)Instructions burned: 71 (million) % 271.93/39.05 % (3370676)------------------------------ % 271.93/39.05 % (3370676)------------------------------ % 271.93/39.05 % (3370677)------------------------------ % 271.93/39.05 % (3370677)------------------------------ % 271.93/39.05 % (3370680)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=3014952694:thitd=on:cond=on:i=4081:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2667 on theBenchmark for (2667ds/4081Mi) % 271.93/39.05 % (3370681)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=748164924:avsq=on:i=1701:avsqr=1,16:rtra=on:rawr=on_2666 on theBenchmark for (2666ds/1701Mi) % 271.93/39.05 % (3370681)Refutation not found, incomplete strategy % 271.93/39.05 % (3370681)------------------------------ % 271.93/39.05 % (3370681)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 271.93/39.05 % (3370681)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 271.93/39.05 % (3370681)CaDiCaL version: 2.1.3 % 271.93/39.05 % (3370681)Termination reason: Refutation not found, incomplete strategy % 271.93/39.05 % (3370681)Time elapsed: 0.163 s % 271.93/39.05 % (3370681)Peak memory usage: 117 MB % 271.93/39.05 % (3370681)Instructions burned: 142 (million) % 271.93/39.05 % (3370681)------------------------------ % 271.93/39.05 % (3370681)------------------------------ % 271.93/39.05 % (3370686)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=931945330:i=57001:doe=on:nm=0:rtra=on:gtg=exists_sym_2658 on theBenchmark for (2658ds/57001Mi) % 277.77/39.77 % (3370686)Refutation not found, incomplete strategy % 277.77/39.77 % (3370686)------------------------------ % 277.77/39.77 % (3370686)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 277.77/39.77 % (3370686)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 277.77/39.77 % (3370686)CaDiCaL version: 2.1.3 % 277.77/39.77 % (3370686)Termination reason: Refutation not found, incomplete strategy % 277.77/39.77 % (3370686)Time elapsed: 0.136 s % 277.77/39.77 % (3370686)Peak memory usage: 117 MB % 277.77/39.77 % (3370686)Instructions burned: 108 (million) % 277.77/39.77 % (3370686)------------------------------ % 277.77/39.77 % (3370686)------------------------------ % 277.77/39.77 % (3370688)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 % 277.77/39.77 % (3370688)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=1156013829:i=8622:aac=none:nm=0:rtra=on:rawr=on_2650 on theBenchmark for (2650ds/8622Mi) % 277.77/39.77 % (3370688)Refutation not found, incomplete strategy % 277.77/39.77 % (3370688)------------------------------ % 277.77/39.77 % (3370688)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 277.77/39.77 % (3370688)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 277.77/39.77 % (3370688)CaDiCaL version: 2.1.3 % 277.77/39.77 % (3370688)Termination reason: Refutation not found, incomplete strategy % 277.77/39.77 % (3370688)Time elapsed: 0.098 s % 277.77/39.77 % (3370688)Peak memory usage: 117 MB % 277.77/39.77 % (3370688)Instructions burned: 68 (million) % 277.77/39.77 % (3370688)------------------------------ % 277.77/39.77 % (3370688)------------------------------ % 277.77/39.77 % (3370690)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=2243689839:i=24:doe=on:rtra=on:gtg=exists_top:ss=axioms_2642 on theBenchmark for (2642ds/24Mi) % 277.77/39.77 % (3370690)Instruction limit reached! % 277.77/39.77 % (3370690)------------------------------ % 277.77/39.77 % (3370690)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 277.77/39.77 % (3370690)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 277.77/39.77 % (3370690)CaDiCaL version: 2.1.3 % 277.77/39.77 % (3370690)Termination reason: Instruction limit % 277.77/39.77 % (3370690)Termination phase: Saturation % 277.77/39.77 % (3370690)Time elapsed: 0.049 s % 277.77/39.77 % (3370690)Peak memory usage: 112 MB % 277.77/39.77 % (3370690)Instructions burned: 24 (million) % 277.77/39.77 % (3370692)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=1286706323:i=614:kws=precedence:nm=0:rtra=on_2639 on theBenchmark for (2639ds/614Mi) % 277.77/39.77 % (3370692)Refutation not found, incomplete strategy % 277.77/39.77 % (3370692)------------------------------ % 277.77/39.77 % (3370692)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 277.77/39.77 % (3370692)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 277.77/39.77 % (3370692)CaDiCaL version: 2.1.3 % 277.77/39.77 % (3370692)Termination reason: Refutation not found, incomplete strategy % 277.77/39.77 % (3370692)Time elapsed: 0.131 s % 277.77/39.77 % (3370692)Peak memory usage: 117 MB % 277.77/39.77 % (3370692)Instructions burned: 104 (million) % 277.77/39.77 % (3370692)------------------------------ % 277.77/39.77 % (3370692)------------------------------ % 277.77/39.77 % (3370694)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=1598170762:i=402:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2631 on theBenchmark for (2631ds/402Mi) % 277.77/39.77 % (3370680)Instruction limit reached! % 277.77/39.77 % (3370680)------------------------------ % 277.77/39.77 % (3370680)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 277.77/39.77 % (3370680)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 277.77/39.77 % (3370680)CaDiCaL version: 2.1.3 % 277.77/39.77 % (3370680)Termination reason: Instruction limit % 277.77/39.77 % (3370680)Termination phase: Saturation % 277.77/39.77 % (3370680)Time elapsed: 4.116 s % 277.77/39.77 % (3370680)Peak memory usage: 150 MB % 277.77/39.77 % (3370680)Instructions burned: 4081 (million) % 277.77/39.77 % (3370694)Instruction limit reached! % 277.77/39.77 % (3370694)------------------------------ % 282.89/40.45 % (3370694)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 282.89/40.45 % (3370694)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.89/40.45 % (3370694)CaDiCaL version: 2.1.3 % 282.89/40.45 % (3370694)Termination reason: Instruction limit % 282.89/40.45 % (3370694)Termination phase: Saturation % 282.89/40.45 % (3370694)Time elapsed: 0.460 s % 282.89/40.45 % (3370694)Peak memory usage: 119 MB % 282.89/40.45 % (3370694)Instructions burned: 402 (million) % 282.89/40.45 % (3370696)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=1009230432:s2a=on:i=14:rtra=on:inst=on_2623 on theBenchmark for (2623ds/14Mi) % 282.89/40.45 % (3370696)Instruction limit reached! % 282.89/40.45 % (3370696)------------------------------ % 282.89/40.45 % (3370696)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 282.89/40.45 % (3370696)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.89/40.45 % (3370696)CaDiCaL version: 2.1.3 % 282.89/40.45 % (3370696)Termination reason: Instruction limit % 282.89/40.45 % (3370696)Termination phase: Saturation % 282.89/40.45 % (3370696)Time elapsed: 0.014 s % 282.89/40.45 % (3370696)Peak memory usage: 88 MB % 282.89/40.45 % (3370696)Instructions burned: 14 (million) % 282.89/40.45 % (3370697)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=3848701848:i=8:rtra=on_2623 on theBenchmark for (2623ds/8Mi) % 282.89/40.45 % (3370697)Instruction limit reached! % 282.89/40.45 % (3370697)------------------------------ % 282.89/40.45 % (3370697)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 282.89/40.45 % (3370697)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.89/40.45 % (3370697)CaDiCaL version: 2.1.3 % 282.89/40.45 % (3370697)Termination reason: Instruction limit % 282.89/40.45 % (3370697)Termination phase: Preprocessing 3 % 282.89/40.45 % (3370697)Time elapsed: 0.007 s % 282.89/40.45 % (3370697)Peak memory usage: 86 MB % 282.89/40.45 % (3370697)Instructions burned: 8 (million) % 282.89/40.45 % (3370701)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=712117326:i=66:rtra=on_2620 on theBenchmark for (2620ds/66Mi) % 282.89/40.45 % (3370699)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=4272999540:i=92:rtra=on_2620 on theBenchmark for (2620ds/92Mi) % 282.89/40.45 % (3370701)Instruction limit reached! % 282.89/40.45 % (3370701)------------------------------ % 282.89/40.45 % (3370701)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 282.89/40.45 % (3370701)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.89/40.45 % (3370701)CaDiCaL version: 2.1.3 % 282.89/40.45 % (3370701)Termination reason: Instruction limit % 282.89/40.45 % (3370701)Termination phase: Saturation % 282.89/40.45 % (3370701)Time elapsed: 0.087 s % 282.89/40.45 % (3370701)Peak memory usage: 116 MB % 282.89/40.45 % (3370701)Instructions burned: 66 (million) % 282.89/40.45 % (3370699)Refutation not found, incomplete strategy % 282.89/40.45 % (3370699)------------------------------ % 282.89/40.45 % (3370699)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 282.89/40.45 % (3370699)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.89/40.45 % (3370699)CaDiCaL version: 2.1.3 % 282.89/40.45 % (3370699)Termination reason: Refutation not found, incomplete strategy % 282.89/40.45 % (3370699)Time elapsed: 0.107 s % 282.89/40.45 % (3370699)Peak memory usage: 117 MB % 282.89/40.45 % (3370699)Instructions burned: 75 (million) % 282.89/40.45 % (3370644)Instruction limit reached! % 282.89/40.45 % (3370644)------------------------------ % 282.89/40.45 % (3370644)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 282.89/40.45 % (3370644)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.89/40.45 % (3370644)CaDiCaL version: 2.1.3 % 282.89/40.45 % (3370644)Termination reason: Instruction limit % 282.89/40.45 % (3370644)Termination phase: Saturation % 282.89/40.45 % (3370644)Time elapsed: 10.160 s % 282.89/40.45 % (3370644)Peak memory usage: 113 MB % 282.89/40.45 % (3370644)Instructions burned: 9201 (million) % 282.89/40.45 % (3370704)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=815595087:st=5:i=28:sd=10:rtra=on:ss=axioms:rawr=on_2617 on theBenchmark for (2617ds/28Mi) % 282.89/40.45 % (3370704)Instruction limit reached! % 282.89/40.45 % (3370704)------------------------------ % 282.89/40.45 % (3370704)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 282.89/40.45 % (3370704)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.89/40.45 % (3370704)CaDiCaL version: 2.1.3 % 285.46/40.96 % (3370704)Termination reason: Instruction limit % 285.46/40.96 % (3370704)Termination phase: Saturation % 285.46/40.96 % (3370704)Time elapsed: 0.027 s % 285.46/40.96 % (3370704)Peak memory usage: 89 MB % 285.46/40.96 % (3370704)Instructions burned: 28 (million) % 285.46/40.96 % (3370699)------------------------------ % 285.46/40.96 % (3370699)------------------------------ % 285.46/40.96 % (3370707)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=1977847812:cond=on:i=32:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2613 on theBenchmark for (2613ds/32Mi) % 285.46/40.96 % (3370705)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=3462453964:i=58:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2614 on theBenchmark for (2614ds/58Mi) % 285.46/40.96 % (3370707)Instruction limit reached! % 285.46/40.96 % (3370707)------------------------------ % 285.46/40.96 % (3370707)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 285.46/40.96 % (3370707)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 285.46/40.96 % (3370707)CaDiCaL version: 2.1.3 % 285.46/40.96 % (3370707)Termination reason: Instruction limit % 285.46/40.96 % (3370707)Termination phase: Saturation % 285.46/40.96 % (3370707)Time elapsed: 0.030 s % 285.46/40.96 % (3370707)Peak memory usage: 89 MB % 285.46/40.96 % (3370707)Instructions burned: 32 (million) % 285.46/40.96 % (3370705)Instruction limit reached! % 285.46/40.96 % (3370705)------------------------------ % 285.46/40.96 % (3370705)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 285.46/40.96 % (3370705)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 285.46/40.96 % (3370705)CaDiCaL version: 2.1.3 % 285.46/40.96 % (3370705)Termination reason: Instruction limit % 285.46/40.96 % (3370705)Termination phase: Saturation % 285.46/40.96 % (3370705)Time elapsed: 0.058 s % 285.46/40.96 % (3370705)Peak memory usage: 89 MB % 285.46/40.96 % (3370705)Instructions burned: 58 (million) % 285.46/40.96 % (3370708)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=131802792:i=48:canc=force:rtra=on_2613 on theBenchmark for (2613ds/48Mi) % 285.46/40.96 % (3370708)Instruction limit reached! % 285.46/40.96 % (3370708)------------------------------ % 285.46/40.96 % (3370708)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 285.46/40.96 % (3370708)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 285.46/40.96 % (3370708)CaDiCaL version: 2.1.3 % 285.46/40.96 % (3370708)Termination reason: Instruction limit % 285.46/40.96 % (3370708)Termination phase: Saturation % 285.46/40.96 % (3370708)Time elapsed: 0.034 s % 285.46/40.96 % (3370708)Peak memory usage: 90 MB % 285.46/40.96 % (3370708)Instructions burned: 49 (million) % 285.46/40.96 % (3370711)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=4099079686:i=54:canc=cautious:fsr=off:rtra=on_2611 on theBenchmark for (2611ds/54Mi) % 285.46/40.96 % (3370712)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=840524542:i=170:gtgl=4:rtra=on:gtg=exists_sym_2611 on theBenchmark for (2611ds/170Mi) % 285.46/40.96 % (3370711)Instruction limit reached! % 285.46/40.96 % (3370711)------------------------------ % 285.46/40.96 % (3370711)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 285.46/40.96 % (3370711)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 285.46/40.96 % (3370711)CaDiCaL version: 2.1.3 % 285.46/40.96 % (3370711)Termination reason: Instruction limit % 285.46/40.96 % (3370711)Termination phase: Saturation % 285.46/40.96 % (3370711)Time elapsed: 0.055 s % 285.46/40.96 % (3370711)Peak memory usage: 90 MB % 285.46/40.96 % (3370711)Instructions burned: 55 (million) % 285.46/40.96 % (3370714)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=4141162983:i=4:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2610 on theBenchmark for (2610ds/4Mi) % 285.46/40.96 % (3370714)Instruction limit reached! % 285.46/40.96 % (3370714)------------------------------ % 285.46/40.96 % (3370714)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 285.46/40.96 % (3370714)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 285.46/40.96 % (3370714)CaDiCaL version: 2.1.3 % 285.46/40.96 % (3370714)Termination reason: Instruction limit % 285.46/40.96 % (3370714)Termination phase: Preprocessing 1 % 285.46/40.96 % (3370714)Time elapsed: 0.005 s % 285.46/40.96 % (3370714)Peak memory usage: 85 MB % 285.46/40.96 % (3370714)Instructions burned: 5 (million) % 285.46/40.96 % (3370712)Instruction limit reached! % 285.46/40.96 % (3370712)------------------------------ % 290.30/41.58 % (3370712)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 290.30/41.58 % (3370712)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 290.30/41.58 % (3370712)CaDiCaL version: 2.1.3 % 290.30/41.58 % (3370712)Termination reason: Instruction limit % 290.30/41.58 % (3370712)Termination phase: Saturation % 290.30/41.58 % (3370712)Time elapsed: 0.171 s % 290.30/41.58 % (3370712)Peak memory usage: 90 MB % 290.30/41.58 % (3370712)Instructions burned: 170 (million) % 290.30/41.58 % (3370717)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=1380770837:i=362:rtra=on:ss=axioms:ev=cautious_2608 on theBenchmark for (2608ds/362Mi) % 290.30/41.58 % (3370719)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=3529578693:i=8:ep=RST:ins=2:rtra=on_2607 on theBenchmark for (2607ds/8Mi) % 290.30/41.58 % (3370719)Instruction limit reached! % 290.30/41.58 % (3370719)------------------------------ % 290.30/41.58 % (3370719)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 290.30/41.58 % (3370719)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 290.30/41.58 % (3370719)CaDiCaL version: 2.1.3 % 290.30/41.58 % (3370719)Termination reason: Instruction limit % 290.30/41.58 % (3370719)Termination phase: Preprocessing 3 % 290.30/41.58 % (3370719)Time elapsed: 0.008 s % 290.30/41.58 % (3370719)Peak memory usage: 86 MB % 290.30/41.58 % (3370719)Instructions burned: 8 (million) % 290.30/41.58 % (3370717)Refutation not found, incomplete strategy % 290.30/41.58 % (3370717)------------------------------ % 290.30/41.58 % (3370717)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 290.30/41.58 % (3370717)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 290.30/41.58 % (3370717)CaDiCaL version: 2.1.3 % 290.30/41.58 % (3370717)Termination reason: Refutation not found, incomplete strategy % 290.30/41.58 % (3370717)Time elapsed: 0.104 s % 290.30/41.58 % (3370717)Peak memory usage: 92 MB % 290.30/41.58 % (3370717)Instructions burned: 105 (million) % 290.30/41.58 % (3370720)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=3826615344:i=132:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2606 on theBenchmark for (2606ds/132Mi) % 290.30/41.58 % (3370723)lrs+10_1_thi=all:si=on:fd=off:random_seed=2082491094:i=106:rtra=on:gtg=all_2605 on theBenchmark for (2605ds/106Mi) % 290.30/41.58 % (3370720)Instruction limit reached! % 290.30/41.58 % (3370720)------------------------------ % 290.30/41.58 % (3370720)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 290.30/41.58 % (3370720)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 290.30/41.58 % (3370720)CaDiCaL version: 2.1.3 % 290.30/41.58 % (3370720)Termination reason: Instruction limit % 290.30/41.58 % (3370720)Termination phase: Saturation % 290.30/41.58 % (3370720)Time elapsed: 0.198 s % 290.30/41.58 % (3370720)Peak memory usage: 135 MB % 290.30/41.58 % (3370720)Instructions burned: 132 (million) % 290.30/41.58 % (3370723)Instruction limit reached! % 290.30/41.58 % (3370723)------------------------------ % 290.30/41.58 % (3370723)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 290.30/41.58 % (3370723)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 290.30/41.58 % (3370723)CaDiCaL version: 2.1.3 % 290.30/41.58 % (3370723)Termination reason: Instruction limit % 290.30/41.58 % (3370723)Termination phase: Saturation % 290.30/41.58 % (3370723)Time elapsed: 0.144 s % 290.30/41.58 % (3370723)Peak memory usage: 116 MB % 290.30/41.58 % (3370723)Instructions burned: 106 (million) % 290.30/41.58 % (3370623)Instruction limit reached! % 290.30/41.58 % (3370623)------------------------------ % 290.30/41.58 % (3370623)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 290.30/41.58 % (3370623)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 290.30/41.58 % (3370623)CaDiCaL version: 2.1.3 % 290.30/41.58 % (3370623)Termination reason: Instruction limit % 290.30/41.58 % (3370623)Termination phase: Saturation % 290.30/41.58 % (3370623)Time elapsed: 15.886 s % 290.30/41.58 % (3370623)Peak memory usage: 132 MB % 290.30/41.58 % (3370623)Instructions burned: 20261 (million) % 290.30/41.58 % (3370717)------------------------------ % 290.30/41.58 % (3370717)------------------------------ % 290.30/41.58 % (3370726)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=2541291862:i=16:ep=RST:nm=16:rtra=on:gtg=exists_top_2602 on theBenchmark for (2602ds/16Mi) % 290.30/41.58 % (3370726)Instruction limit reached! % 290.30/41.58 % (3370726)------------------------------ % 297.58/42.50 % (3370726)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 297.58/42.50 % (3370726)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 297.58/42.50 % (3370726)CaDiCaL version: 2.1.3 % 297.58/42.50 % (3370726)Termination reason: Instruction limit % 297.58/42.50 % (3370726)Termination phase: Saturation % 297.58/42.50 % (3370726)Time elapsed: 0.015 s % 297.58/42.50 % (3370726)Peak memory usage: 88 MB % 297.58/42.50 % (3370726)Instructions burned: 16 (million) % 297.58/42.50 % (3370727)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=287921737:st=3:i=4:rtra=on:ss=axioms_2601 on theBenchmark for (2601ds/4Mi) % 297.58/42.50 % (3370727)Instruction limit reached! % 297.58/42.50 % (3370727)------------------------------ % 297.58/42.50 % (3370727)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 297.58/42.50 % (3370727)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 297.58/42.50 % (3370727)CaDiCaL version: 2.1.3 % 297.58/42.50 % (3370727)Termination reason: Instruction limit % 297.58/42.50 % (3370727)Termination phase: Preprocessing 1 % 297.58/42.50 % (3370727)Time elapsed: 0.004 s % 297.58/42.50 % (3370727)Peak memory usage: 85 MB % 297.58/42.50 % (3370727)Instructions burned: 4 (million) % 297.58/42.50 % (3370728)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=3234909125:i=4:doe=on:canc=force:asg=cautious:rtra=on_2600 on theBenchmark for (2600ds/4Mi) % 297.58/42.50 % (3370728)Instruction limit reached! % 297.58/42.50 % (3370728)------------------------------ % 297.58/42.50 % (3370728)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 297.58/42.50 % (3370728)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 297.58/42.50 % (3370728)CaDiCaL version: 2.1.3 % 297.58/42.50 % (3370728)Termination reason: Instruction limit % 297.58/42.50 % (3370728)Termination phase: Preprocessing 1 % 297.58/42.50 % (3370728)Time elapsed: 0.004 s % 297.58/42.50 % (3370728)Peak memory usage: 85 MB % 297.58/42.50 % (3370728)Instructions burned: 4 (million) % 297.58/42.50 % (3370729)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=3580519597:i=254:doe=on:rtra=on_2600 on theBenchmark for (2600ds/254Mi) % 297.58/42.50 % (3370731)dis+10_1_si=on:random_seed=1691559892:i=20:ep=R:rtra=on_2599 on theBenchmark for (2599ds/20Mi) % 297.58/42.50 % (3370731)Instruction limit reached! % 297.58/42.50 % (3370731)------------------------------ % 297.58/42.50 % (3370731)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 297.58/42.50 % (3370731)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 297.58/42.50 % (3370731)CaDiCaL version: 2.1.3 % 297.58/42.50 % (3370731)Termination reason: Instruction limit % 297.58/42.50 % (3370731)Termination phase: Saturation % 297.58/42.50 % (3370731)Time elapsed: 0.020 s % 297.58/42.50 % (3370731)Peak memory usage: 89 MB % 297.58/42.50 % (3370731)Instructions burned: 20 (million) % 297.58/42.50 % (3370733)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=3196207138:i=52:canc=cautious:av=off:rtra=on_2599 on theBenchmark for (2599ds/52Mi) % 297.58/42.50 % (3370733)Refutation not found, incomplete strategy % 297.58/42.50 % (3370733)------------------------------ % 297.58/42.50 % (3370733)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 297.58/42.50 % (3370733)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 297.58/42.50 % (3370733)CaDiCaL version: 2.1.3 % 297.58/42.50 % (3370733)Termination reason: Refutation not found, incomplete strategy % 297.58/42.50 % (3370733)Time elapsed: 0.048 s % 297.58/42.50 % (3370733)Peak memory usage: 90 MB % 297.58/42.50 % (3370733)Instructions burned: 50 (million) % 297.58/42.50 % (3370735)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=3116047242: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_2598 on theBenchmark for (2598ds/70Mi) % 297.58/42.50 % (3370729)Instruction limit reached! % 297.58/42.50 % (3370729)------------------------------ % 297.58/42.50 % (3370729)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 297.58/42.50 % (3370729)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 297.58/42.50 % (3370729)CaDiCaL version: 2.1.3 % 297.58/42.50 % (3370729)Termination reason: Instruction limit % 297.58/42.50 % (3370729)Termination phase: Saturation % 297.58/42.50 % (3370729)Time elapsed: 0.264 s % 297.58/42.50 % (3370729)Peak memory usage: 117 MB % 297.58/42.50 % (3370729)Instructions burned: 254 (million) % 297.58/42.50 % (3370735)Instruction limit reached!Terminated %------------------------------------------------------------------------------