%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWW837_1 : TPTP v9.3.1. Released v7.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/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:37:55 PM UTC 2026 % Result : Timeout 286.93s 41.04s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWW837_1 : TPTP v9.3.1. Released v7.0.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.07/0.18 % Computer : n018.cluster.edu % 0.07/0.18 % Model : x86_64 x86_64 % 0.07/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.07/0.18 % Memory : 8046.5625MB % 0.07/0.18 % OS : Linux 6.8.0-71-generic % 0.07/0.18 % CPULimit : 300 % 0.07/0.18 % WCLimit : 300 % 0.07/0.18 % DateTime : Mon Sep 28 14:33:25 UTC 2026 % 0.07/0.18 % CPUTime : % 0.07/0.18 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.07/0.22 Running first-order theorem proving % 0.07/0.22 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 3.74/1.22 % (3436150)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule. % 3.74/1.22 % (3436161)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=1969364470:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi) % 3.74/1.22 % (3436161)Instruction limit reached! % 3.74/1.22 % (3436161)------------------------------ % 3.74/1.22 % (3436161)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.74/1.22 % (3436161)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.74/1.22 % (3436161)CaDiCaL version: 2.1.3 % 3.74/1.22 % (3436161)Termination reason: Instruction limit % 3.74/1.22 % (3436161)Termination phase: Saturation % 3.74/1.22 % (3436161)Time elapsed: 0.027 s % 3.74/1.22 % (3436161)Peak memory usage: 117 MB % 3.74/1.22 % (3436161)Instructions burned: 34 (million) % 3.74/1.22 % (3436158)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=1011846766:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi) % 3.74/1.22 % (3436159)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=2238129012:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi) % 3.74/1.22 % (3436157)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=261606657:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi) % 3.74/1.22 % (3436156)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=2233772116:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi) % 3.74/1.22 % (3436155)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=3497416263:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi) % 3.74/1.22 % (3436160)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=1269112243:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi) % 3.74/1.22 % (3436159)Instruction limit reached! % 3.74/1.22 % (3436159)------------------------------ % 3.74/1.22 % (3436159)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.74/1.22 % (3436159)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.74/1.22 % (3436159)CaDiCaL version: 2.1.3 % 3.74/1.22 % (3436159)Termination reason: Instruction limit % 3.74/1.22 % (3436159)Termination phase: shuffling % 3.74/1.22 % (3436159)Time elapsed: 0.003 s % 3.74/1.22 % (3436159)Peak memory usage: 86 MB % 3.74/1.22 % (3436159)Instructions burned: 5 (million) % 3.74/1.22 % (3436158)Instruction limit reached! % 3.74/1.22 % (3436158)------------------------------ % 3.74/1.22 % (3436158)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.74/1.22 % (3436158)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.74/1.22 % (3436158)CaDiCaL version: 2.1.3 % 3.74/1.22 % (3436158)Termination reason: Instruction limit % 3.74/1.22 % (3436158)Termination phase: Saturation % 3.74/1.22 % (3436158)Time elapsed: 0.004 s % 3.74/1.22 % (3436158)Peak memory usage: 87 MB % 3.74/1.22 % (3436158)Instructions burned: 7 (million) % 3.74/1.22 % (3436155)Instruction limit reached! % 3.74/1.22 % (3436155)------------------------------ % 3.74/1.22 % (3436155)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.74/1.22 % (3436155)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.74/1.22 % (3436155)CaDiCaL version: 2.1.3 % 3.74/1.22 % (3436155)Termination reason: Instruction limit % 3.74/1.22 % (3436155)Termination phase: Saturation % 3.74/1.22 % (3436155)Time elapsed: 0.027 s % 3.74/1.22 % (3436155)Peak memory usage: 110 MB % 3.74/1.22 % (3436155)Instructions burned: 12 (million) % 3.74/1.22 % (3436160)Instruction limit reached! % 3.74/1.22 % (3436160)------------------------------ % 3.74/1.22 % (3436160)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.74/1.22 % (3436160)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.74/1.22 % (3436160)CaDiCaL version: 2.1.3 % 3.74/1.22 % (3436160)Termination reason: Instruction limit % 3.74/1.22 % (3436160)Termination phase: Saturation % 3.74/1.22 % (3436160)Time elapsed: 0.055 s % 3.74/1.22 % (3436160)Peak memory usage: 117 MB % 3.74/1.22 % (3436160)Instructions burned: 46 (million) % 3.74/1.22 % (3436163)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=1224633107:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2998 on theBenchmark for (2998ds/14Mi) % 3.74/1.22 % (3436163)Refutation not found, incomplete strategy % 3.74/1.22 % (3436163)------------------------------ % 4.58/1.38 % (3436163)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.58/1.38 % (3436163)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.58/1.38 % (3436163)CaDiCaL version: 2.1.3 % 4.58/1.38 % (3436163)Termination reason: Refutation not found, incomplete strategy % 4.58/1.38 % (3436163)Time elapsed: 0.001 s % 4.58/1.38 % (3436163)Peak memory usage: 88 MB % 4.58/1.38 % (3436163)Instructions burned: 1 (million) % 4.58/1.38 % (3436170)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=4130097812:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2998 on theBenchmark for (2998ds/29Mi) % 4.58/1.38 % (3436171)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=2108433106:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/16Mi) % 4.58/1.38 % (3436171)Instruction limit reached! % 4.58/1.38 % (3436171)------------------------------ % 4.58/1.38 % (3436171)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.58/1.38 % (3436171)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.58/1.38 % (3436171)CaDiCaL version: 2.1.3 % 4.58/1.38 % (3436171)Termination reason: Instruction limit % 4.58/1.38 % (3436171)Termination phase: Saturation % 4.58/1.38 % (3436171)Time elapsed: 0.010 s % 4.58/1.38 % (3436171)Peak memory usage: 88 MB % 4.58/1.38 % (3436171)Instructions burned: 18 (million) % 4.58/1.38 % (3436157)Instruction limit reached! % 4.58/1.38 % (3436157)------------------------------ % 4.58/1.38 % (3436157)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.58/1.38 % (3436157)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.58/1.38 % (3436157)CaDiCaL version: 2.1.3 % 4.58/1.38 % (3436157)Termination reason: Instruction limit % 4.58/1.38 % (3436157)Termination phase: Saturation % 4.58/1.38 % (3436157)Time elapsed: 0.147 s % 4.58/1.38 % (3436157)Peak memory usage: 117 MB % 4.58/1.38 % (3436157)Instructions burned: 201 (million) % 4.58/1.38 % (3436170)Instruction limit reached! % 4.58/1.38 % (3436170)------------------------------ % 4.58/1.38 % (3436170)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.58/1.38 % (3436170)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.58/1.38 % (3436170)CaDiCaL version: 2.1.3 % 4.58/1.38 % (3436170)Termination reason: Instruction limit % 4.58/1.38 % (3436170)Termination phase: Saturation % 4.58/1.38 % (3436170)Time elapsed: 0.021 s % 4.58/1.38 % (3436170)Peak memory usage: 88 MB % 4.58/1.38 % (3436170)Instructions burned: 30 (million) % 4.58/1.38 % (3436172)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=1873545862:i=24:canc=force:rtra=on_2998 on theBenchmark for (2998ds/24Mi) % 4.58/1.38 % (3436172)Instruction limit reached! % 4.58/1.38 % (3436172)------------------------------ % 4.58/1.38 % (3436172)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.58/1.38 % (3436172)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.58/1.38 % (3436172)CaDiCaL version: 2.1.3 % 4.58/1.38 % (3436172)Termination reason: Instruction limit % 4.58/1.38 % (3436172)Termination phase: Saturation % 4.58/1.38 % (3436172)Time elapsed: 0.017 s % 4.58/1.38 % (3436172)Peak memory usage: 89 MB % 4.58/1.38 % (3436172)Instructions burned: 24 (million) % 4.58/1.38 % (3436173)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=2268620689:i=27:canc=cautious:fsr=off:rtra=on_2997 on theBenchmark for (2997ds/27Mi) % 4.58/1.38 % (3436173)Refutation not found, incomplete strategy % 4.58/1.38 % (3436173)------------------------------ % 4.58/1.38 % (3436173)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.58/1.38 % (3436173)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.58/1.38 % (3436173)CaDiCaL version: 2.1.3 % 4.58/1.38 % (3436173)Termination reason: Refutation not found, incomplete strategy % 4.58/1.38 % (3436173)Time elapsed: 0.007 s % 4.58/1.38 % (3436173)Peak memory usage: 89 MB % 4.58/1.38 % (3436173)Instructions burned: 9 (million) % 4.58/1.38 % (3436156)Instruction limit reached! % 4.58/1.38 % (3436156)------------------------------ % 4.58/1.38 % (3436156)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.58/1.38 % (3436156)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.83/1.56 % (3436156)CaDiCaL version: 2.1.3 % 5.83/1.56 % (3436156)Termination reason: Instruction limit % 5.83/1.56 % (3436156)Termination phase: Saturation % 5.83/1.56 % (3436156)Time elapsed: 0.212 s % 5.83/1.56 % (3436156)Peak memory usage: 119 MB % 5.83/1.56 % (3436156)Instructions burned: 309 (million) % 5.83/1.56 % (3436163)------------------------------ % 5.83/1.56 % (3436163)------------------------------ % 5.83/1.56 % (3436177)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=851385971:i=85:gtgl=4:rtra=on:gtg=exists_sym_2997 on theBenchmark for (2997ds/85Mi) % 5.83/1.56 % (3436179)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=2090292591:i=181:rtra=on:ss=axioms:ev=cautious_2996 on theBenchmark for (2996ds/181Mi) % 5.83/1.56 % (3436178)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=1057829754:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2996 on theBenchmark for (2996ds/2Mi) % 5.83/1.56 % (3436179)Refutation not found, incomplete strategy % 5.83/1.56 % (3436179)------------------------------ % 5.83/1.56 % (3436179)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.83/1.56 % (3436179)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.83/1.56 % (3436179)CaDiCaL version: 2.1.3 % 5.83/1.56 % (3436179)Termination reason: Refutation not found, incomplete strategy % 5.83/1.56 % (3436179)Time elapsed: 0.001 s % 5.83/1.56 % (3436179)Peak memory usage: 87 MB % 5.83/1.56 % (3436179)Instructions burned: 1 (million) % 5.83/1.56 % (3436178)Instruction limit reached! % 5.83/1.56 % (3436178)------------------------------ % 5.83/1.56 % (3436178)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.83/1.56 % (3436178)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.83/1.56 % (3436178)CaDiCaL version: 2.1.3 % 5.83/1.56 % (3436178)Termination reason: Instruction limit % 5.83/1.56 % (3436178)Termination phase: Preprocessing 3 % 5.83/1.56 % (3436178)Time elapsed: 0.002 s % 5.83/1.56 % (3436178)Peak memory usage: 86 MB % 5.83/1.56 % (3436178)Instructions burned: 3 (million) % 5.83/1.56 % (3436181)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=1643867097:i=4:ep=RST:ins=2:rtra=on_2996 on theBenchmark for (2996ds/4Mi) % 5.83/1.56 % (3436181)Instruction limit reached! % 5.83/1.56 % (3436181)------------------------------ % 5.83/1.56 % (3436181)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.83/1.56 % (3436181)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.83/1.56 % (3436181)CaDiCaL version: 2.1.3 % 5.83/1.56 % (3436181)Termination reason: Instruction limit % 5.83/1.56 % (3436181)Termination phase: Equality resolution with deletion % 5.83/1.56 % (3436181)Time elapsed: 0.003 s % 5.83/1.56 % (3436181)Peak memory usage: 86 MB % 5.83/1.56 % (3436181)Instructions burned: 5 (million) % 5.83/1.56 % (3436177)Instruction limit reached! % 5.83/1.56 % (3436177)------------------------------ % 5.83/1.56 % (3436177)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.83/1.56 % (3436177)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.83/1.56 % (3436177)CaDiCaL version: 2.1.3 % 5.83/1.56 % (3436177)Termination reason: Instruction limit % 5.83/1.56 % (3436177)Termination phase: Saturation % 5.83/1.56 % (3436177)Time elapsed: 0.052 s % 5.83/1.56 % (3436177)Peak memory usage: 89 MB % 5.83/1.56 % (3436177)Instructions burned: 86 (million) % 5.83/1.56 % (3436183)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=2357382073:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2996 on theBenchmark for (2996ds/66Mi) % 5.83/1.56 % (3436184)lrs+10_1_thi=all:si=on:fd=off:random_seed=3453511193:i=53:rtra=on:gtg=all_2996 on theBenchmark for (2996ds/53Mi) % 5.83/1.56 % (3436184)Instruction limit reached! % 5.83/1.56 % (3436184)------------------------------ % 5.83/1.56 % (3436184)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.83/1.56 % (3436184)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.83/1.56 % (3436184)CaDiCaL version: 2.1.3 % 5.83/1.56 % (3436184)Termination reason: Instruction limit % 5.83/1.56 % (3436184)Termination phase: Saturation % 5.83/1.56 % (3436184)Time elapsed: 0.051 s % 5.83/1.56 % (3436184)Peak memory usage: 116 MB % 5.83/1.56 % (3436184)Instructions burned: 54 (million) % 5.83/1.56 % (3436183)Instruction limit reached! % 5.83/1.56 % (3436183)------------------------------ % 5.83/1.56 % (3436183)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.83/1.76 % (3436183)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.83/1.76 % (3436183)CaDiCaL version: 2.1.3 % 6.83/1.76 % (3436183)Termination reason: Instruction limit % 6.83/1.76 % (3436183)Termination phase: Saturation % 6.83/1.76 % (3436183)Time elapsed: 0.082 s % 6.83/1.76 % (3436183)Peak memory usage: 135 MB % 6.83/1.76 % (3436183)Instructions burned: 67 (million) % 6.83/1.76 % (3436188)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=3660521051:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2995 on theBenchmark for (2995ds/8Mi) % 6.83/1.76 % (3436188)Instruction limit reached! % 6.83/1.76 % (3436188)------------------------------ % 6.83/1.76 % (3436188)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.83/1.76 % (3436188)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.83/1.76 % (3436188)CaDiCaL version: 2.1.3 % 6.83/1.76 % (3436188)Termination reason: Instruction limit % 6.83/1.76 % (3436188)Termination phase: Saturation % 6.83/1.76 % (3436188)Time elapsed: 0.005 s % 6.83/1.76 % (3436188)Peak memory usage: 87 MB % 6.83/1.76 % (3436188)Instructions burned: 9 (million) % 6.83/1.76 % (3436190)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=2792083670:st=3:i=2:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/2Mi) % 6.83/1.76 % (3436190)Refutation not found, incomplete strategy % 6.83/1.76 % (3436190)------------------------------ % 6.83/1.76 % (3436190)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.83/1.76 % (3436190)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.83/1.76 % (3436190)CaDiCaL version: 2.1.3 % 6.83/1.76 % (3436190)Termination reason: Refutation not found, incomplete strategy % 6.83/1.76 % (3436190)Time elapsed: 0.002 s % 6.83/1.76 % (3436190)Peak memory usage: 88 MB % 6.83/1.76 % (3436190)Instructions burned: 1 (million) % 6.83/1.76 % (3436191)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=1476912599:i=2:doe=on:canc=force:asg=cautious:rtra=on_2995 on theBenchmark for (2995ds/2Mi) % 6.83/1.76 % (3436191)Instruction limit reached! % 6.83/1.76 % (3436191)------------------------------ % 6.83/1.76 % (3436191)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.83/1.76 % (3436191)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.83/1.76 % (3436191)CaDiCaL version: 2.1.3 % 6.83/1.76 % (3436191)Termination reason: Instruction limit % 6.83/1.76 % (3436191)Termination phase: Preprocessing 3 % 6.83/1.76 % (3436191)Time elapsed: 0.002 s % 6.83/1.76 % (3436191)Peak memory usage: 86 MB % 6.83/1.76 % (3436191)Instructions burned: 3 (million) % 6.83/1.76 % (3436173)------------------------------ % 6.83/1.76 % (3436173)------------------------------ % 6.83/1.76 % (3436194)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=1429120144:i=127:doe=on:rtra=on_2994 on theBenchmark for (2994ds/127Mi) % 6.83/1.76 % (3436179)------------------------------ % 6.83/1.76 % (3436179)------------------------------ % 6.83/1.76 % (3436196)dis+10_1_si=on:random_seed=238809805:i=10:ep=R:rtra=on_2994 on theBenchmark for (2994ds/10Mi) % 6.83/1.76 % (3436196)Instruction limit reached! % 6.83/1.76 % (3436196)------------------------------ % 6.83/1.76 % (3436196)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.83/1.76 % (3436196)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.83/1.76 % (3436196)CaDiCaL version: 2.1.3 % 6.83/1.76 % (3436196)Termination reason: Instruction limit % 6.83/1.76 % (3436196)Termination phase: Saturation % 6.83/1.76 % (3436196)Time elapsed: 0.006 s % 6.83/1.76 % (3436196)Peak memory usage: 88 MB % 6.83/1.76 % (3436196)Instructions burned: 10 (million) % 6.83/1.76 % (3436194)Instruction limit reached! % 6.83/1.76 % (3436194)------------------------------ % 6.83/1.76 % (3436194)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.83/1.76 % (3436194)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.83/1.76 % (3436194)CaDiCaL version: 2.1.3 % 6.83/1.76 % (3436194)Termination reason: Instruction limit % 6.83/1.76 % (3436194)Termination phase: Saturation % 6.83/1.76 % (3436194)Time elapsed: 0.056 s % 6.83/1.76 % (3436194)Peak memory usage: 118 MB % 6.83/1.76 % (3436194)Instructions burned: 130 (million) % 6.83/1.76 % (3436198)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=3855553784:i=26:canc=cautious:av=off:rtra=on_2994 on theBenchmark for (2994ds/26Mi) % 6.83/1.76 % (3436200)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=2394655125: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_2993 on theBenchmark for (2993ds/35Mi) % 8.41/1.98 % (3436198)Refutation not found, incomplete strategy % 8.41/1.98 % (3436198)------------------------------ % 8.41/1.98 % (3436198)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.41/1.98 % (3436198)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.41/1.98 % (3436198)CaDiCaL version: 2.1.3 % 8.41/1.98 % (3436198)Termination reason: Refutation not found, incomplete strategy % 8.41/1.98 % (3436198)Time elapsed: 0.007 s % 8.41/1.98 % (3436198)Peak memory usage: 88 MB % 8.41/1.98 % (3436198)Instructions burned: 10 (million) % 8.41/1.98 % (3436200)Instruction limit reached! % 8.41/1.98 % (3436200)------------------------------ % 8.41/1.98 % (3436200)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.41/1.98 % (3436200)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.41/1.98 % (3436200)CaDiCaL version: 2.1.3 % 8.41/1.98 % (3436200)Termination reason: Instruction limit % 8.41/1.98 % (3436200)Termination phase: Saturation % 8.41/1.98 % (3436200)Time elapsed: 0.027 s % 8.41/1.98 % (3436200)Peak memory usage: 89 MB % 8.41/1.98 % (3436200)Instructions burned: 35 (million) % 8.41/1.98 % (3436201)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=4144641058:i=2:fsr=off:rtra=on:inst=on_2993 on theBenchmark for (2993ds/2Mi) % 8.41/1.98 % (3436201)Instruction limit reached! % 8.41/1.98 % (3436201)------------------------------ % 8.41/1.98 % (3436201)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.41/1.98 % (3436201)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.41/1.98 % (3436201)CaDiCaL version: 2.1.3 % 8.41/1.98 % (3436201)Termination reason: Instruction limit % 8.41/1.98 % (3436201)Termination phase: Preprocessing 3 % 8.41/1.98 % (3436201)Time elapsed: 0.002 s % 8.41/1.98 % (3436201)Peak memory usage: 86 MB % 8.41/1.98 % (3436201)Instructions burned: 3 (million) % 8.41/1.98 % (3436207)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=1101834052:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2992 on theBenchmark for (2992ds/13Mi) % 8.41/1.98 % (3436203)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=1879897728:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2993 on theBenchmark for (2993ds/8Mi) % 8.41/1.98 % (3436203)Instruction limit reached! % 8.41/1.98 % (3436203)------------------------------ % 8.41/1.98 % (3436203)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.41/1.98 % (3436203)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.41/1.98 % (3436203)CaDiCaL version: 2.1.3 % 8.41/1.98 % (3436203)Termination reason: Instruction limit % 8.41/1.98 % (3436203)Termination phase: Saturation % 8.41/1.98 % (3436203)Time elapsed: 0.005 s % 8.41/1.98 % (3436203)Peak memory usage: 88 MB % 8.41/1.98 % (3436203)Instructions burned: 8 (million) % 8.41/1.98 % (3436207)Instruction limit reached! % 8.41/1.98 % (3436207)------------------------------ % 8.41/1.98 % (3436207)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.41/1.98 % (3436207)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.41/1.99 % (3436207)CaDiCaL version: 2.1.3 % 8.41/1.99 % (3436207)Termination reason: Instruction limit % 8.41/1.99 % (3436207)Termination phase: Saturation % 8.41/1.99 % (3436207)Time elapsed: 0.018 s % 8.41/1.99 % (3436207)Peak memory usage: 112 MB % 8.41/1.99 % (3436207)Instructions burned: 16 (million) % 8.41/1.99 % (3436190)------------------------------ % 8.41/1.99 % (3436190)------------------------------ % 8.41/1.99 % (3436205)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=2616261954:i=370:ep=RS:fsr=off:rtra=on_2992 on theBenchmark for (2992ds/370Mi) % 8.41/1.99 % (3436210)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=1180493212:i=226:rtra=on:gtg=position:ss=axioms_2992 on theBenchmark for (2992ds/226Mi) % 8.41/1.99 % (3436211)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=1884467659:i=10:rtra=on_2992 on theBenchmark for (2992ds/10Mi) % 8.41/1.99 % (3436211)Instruction limit reached! % 8.41/1.99 % (3436211)------------------------------ % 8.41/1.99 % (3436211)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.55/2.28 % (3436211)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.55/2.28 % (3436211)CaDiCaL version: 2.1.3 % 10.55/2.28 % (3436211)Termination reason: Instruction limit % 10.55/2.28 % (3436211)Termination phase: Saturation % 10.55/2.28 % (3436211)Time elapsed: 0.007 s % 10.55/2.28 % (3436211)Peak memory usage: 88 MB % 10.55/2.28 % (3436211)Instructions burned: 11 (million) % 10.55/2.28 % (3436210)Refutation not found, incomplete strategy % 10.55/2.28 % (3436210)------------------------------ % 10.55/2.28 % (3436210)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.55/2.28 % (3436210)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.55/2.28 % (3436210)CaDiCaL version: 2.1.3 % 10.55/2.28 % (3436210)Termination reason: Refutation not found, incomplete strategy % 10.55/2.28 % (3436210)Time elapsed: 0.027 s % 10.55/2.28 % (3436210)Peak memory usage: 111 MB % 10.55/2.28 % (3436210)Instructions burned: 7 (million) % 10.55/2.28 % (3436215)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=2077002068:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2991 on theBenchmark for (2991ds/75Mi) % 10.55/2.28 % (3436215)Instruction limit reached! % 10.55/2.28 % (3436215)------------------------------ % 10.55/2.28 % (3436215)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.55/2.28 % (3436215)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.55/2.28 % (3436215)CaDiCaL version: 2.1.3 % 10.55/2.28 % (3436215)Termination reason: Instruction limit % 10.55/2.28 % (3436215)Termination phase: Saturation % 10.55/2.28 % (3436215)Time elapsed: 0.027 s % 10.55/2.28 % (3436215)Peak memory usage: 90 MB % 10.55/2.28 % (3436215)Instructions burned: 78 (million) % 10.55/2.28 % (3436214)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=1606717519:i=71:rtra=on:gtg=exists_top_2991 on theBenchmark for (2991ds/71Mi) % 10.55/2.28 % (3436217)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=645012553:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2991 on theBenchmark for (2991ds/294Mi) % 10.55/2.28 % (3436198)------------------------------ % 10.55/2.28 % (3436198)------------------------------ % 10.55/2.28 % (3436222)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=3298544423:i=131:rtra=on_2990 on theBenchmark for (2990ds/131Mi) % 10.55/2.28 % (3436205)Instruction limit reached! % 10.55/2.28 % (3436205)------------------------------ % 10.55/2.28 % (3436205)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.55/2.28 % (3436205)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.55/2.28 % (3436205)CaDiCaL version: 2.1.3 % 10.55/2.28 % (3436205)Termination reason: Instruction limit % 10.55/2.28 % (3436205)Termination phase: Saturation % 10.55/2.28 % (3436205)Time elapsed: 0.200 s % 10.55/2.28 % (3436205)Peak memory usage: 91 MB % 10.55/2.28 % (3436205)Instructions burned: 370 (million) % 10.55/2.28 % (3436221)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=1942072355:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2990 on theBenchmark for (2990ds/130Mi) % 10.55/2.28 % (3436214)Instruction limit reached! % 10.55/2.28 % (3436214)------------------------------ % 10.55/2.28 % (3436214)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.55/2.28 % (3436214)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.55/2.28 % (3436214)CaDiCaL version: 2.1.3 % 10.55/2.28 % (3436214)Termination reason: Instruction limit % 10.55/2.28 % (3436214)Termination phase: Saturation % 10.55/2.28 % (3436214)Time elapsed: 0.091 s % 10.55/2.28 % (3436214)Peak memory usage: 135 MB % 10.55/2.28 % (3436214)Instructions burned: 71 (million) % 10.55/2.28 % (3436222)Instruction limit reached! % 10.55/2.28 % (3436222)------------------------------ % 10.55/2.28 % (3436222)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.55/2.28 % (3436222)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.55/2.28 % (3436222)CaDiCaL version: 2.1.3 % 10.55/2.28 % (3436222)Termination reason: Instruction limit % 10.55/2.28 % (3436222)Termination phase: Saturation % 10.55/2.28 % (3436222)Time elapsed: 0.074 s % 10.55/2.28 % (3436222)Peak memory usage: 135 MB % 10.55/2.28 % (3436222)Instructions burned: 132 (million) % 10.55/2.28 % (3436225)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=1003089117:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2990 on theBenchmark for (2990ds/40Mi) % 13.19/2.60 % (3436210)------------------------------ % 13.19/2.60 % (3436210)------------------------------ % 13.19/2.60 % (3436217)Instruction limit reached! % 13.19/2.60 % (3436217)------------------------------ % 13.19/2.60 % (3436217)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.19/2.60 % (3436217)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.19/2.60 % (3436217)CaDiCaL version: 2.1.3 % 13.19/2.60 % (3436217)Termination reason: Instruction limit % 13.19/2.60 % (3436217)Termination phase: Saturation % 13.19/2.60 % (3436217)Time elapsed: 0.176 s % 13.19/2.60 % (3436217)Peak memory usage: 91 MB % 13.19/2.60 % (3436217)Instructions burned: 295 (million) % 13.19/2.60 % (3436221)Instruction limit reached! % 13.19/2.60 % (3436221)------------------------------ % 13.19/2.60 % (3436221)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.19/2.60 % (3436221)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.19/2.60 % (3436221)CaDiCaL version: 2.1.3 % 13.19/2.60 % (3436221)Termination reason: Instruction limit % 13.19/2.60 % (3436221)Termination phase: Saturation % 13.19/2.60 % (3436221)Time elapsed: 0.109 s % 13.19/2.60 % (3436221)Peak memory usage: 118 MB % 13.19/2.60 % (3436221)Instructions burned: 130 (million) % 13.19/2.60 % (3436227)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=2431784834:i=307:rtra=on:gtg=exists_top_2989 on theBenchmark for (2989ds/307Mi) % 13.19/2.60 % (3436225)Instruction limit reached! % 13.19/2.60 % (3436225)------------------------------ % 13.19/2.60 % (3436225)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.19/2.60 % (3436225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.19/2.60 % (3436225)CaDiCaL version: 2.1.3 % 13.19/2.60 % (3436225)Termination reason: Instruction limit % 13.19/2.60 % (3436225)Termination phase: Saturation % 13.19/2.60 % (3436225)Time elapsed: 0.067 s % 13.19/2.60 % (3436225)Peak memory usage: 135 MB % 13.19/2.60 % (3436225)Instructions burned: 40 (million) % 13.19/2.60 % (3436230)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=2271954873:i=131:canc=cautious:fsr=off:rtra=on_2988 on theBenchmark for (2988ds/131Mi) % 13.19/2.60 % (3436229)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=3262954297:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2989 on theBenchmark for (2989ds/598Mi) % 13.19/2.60 % (3436230)Instruction limit reached! % 13.19/2.60 % (3436230)------------------------------ % 13.19/2.60 % (3436230)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.19/2.60 % (3436230)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.19/2.60 % (3436230)CaDiCaL version: 2.1.3 % 13.19/2.60 % (3436230)Termination reason: Instruction limit % 13.19/2.60 % (3436230)Termination phase: Saturation % 13.19/2.60 % (3436230)Time elapsed: 0.054 s % 13.19/2.60 % (3436230)Peak memory usage: 117 MB % 13.19/2.60 % (3436230)Instructions burned: 134 (million) % 13.19/2.60 % (3436234)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=354103385:i=383:fsr=off:rtra=on:ev=force_2988 on theBenchmark for (2988ds/383Mi) % 13.19/2.60 % (3436233)dis+10_1_si=on:random_seed=1128975278:s2a=on:i=1000:rtra=on:gtg=exists_all_2988 on theBenchmark for (2988ds/1000Mi) % 13.19/2.60 % (3436232)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=2974588615:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2988 on theBenchmark for (2988ds/259Mi) % 13.19/2.60 % (3436232)Refutation not found, incomplete strategy % 13.19/2.60 % (3436232)------------------------------ % 13.19/2.60 % (3436232)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.19/2.60 % (3436232)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.19/2.60 % (3436232)CaDiCaL version: 2.1.3 % 13.19/2.60 % (3436232)Termination reason: Refutation not found, incomplete strategy % 13.19/2.60 % (3436232)Time elapsed: 0.027 s % 13.19/2.60 % (3436232)Peak memory usage: 111 MB % 13.19/2.60 % (3436232)Instructions burned: 7 (million) % 13.19/2.60 % (3436236)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=1784137717:i=141:doe=on:rtra=on_2988 on theBenchmark for (2988ds/141Mi) % 13.19/2.60 % (3436239)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=55451509:i=65:nm=16:rtra=on_2987 on theBenchmark for (2987ds/65Mi) % 13.51/2.77 % (3436239)Refutation not found, incomplete strategy % 13.51/2.77 % (3436239)------------------------------ % 13.51/2.77 % (3436239)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.51/2.77 % (3436239)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.51/2.77 % (3436239)CaDiCaL version: 2.1.3 % 13.51/2.77 % (3436239)Termination reason: Refutation not found, incomplete strategy % 13.51/2.77 % (3436239)Time elapsed: 0.018 s % 13.51/2.77 % (3436239)Peak memory usage: 112 MB % 13.51/2.77 % (3436239)Instructions burned: 13 (million) % 13.51/2.77 % (3436227)Instruction limit reached! % 13.51/2.77 % (3436227)------------------------------ % 13.51/2.77 % (3436227)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.51/2.77 % (3436227)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.51/2.77 % (3436227)CaDiCaL version: 2.1.3 % 13.51/2.77 % (3436227)Termination reason: Instruction limit % 13.51/2.77 % (3436227)Termination phase: Saturation % 13.51/2.77 % (3436227)Time elapsed: 0.190 s % 13.51/2.77 % (3436227)Peak memory usage: 91 MB % 13.51/2.77 % (3436227)Instructions burned: 310 (million) % 13.51/2.77 % (3436236)Instruction limit reached! % 13.51/2.77 % (3436236)------------------------------ % 13.51/2.77 % (3436236)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.51/2.77 % (3436236)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.51/2.77 % (3436236)CaDiCaL version: 2.1.3 % 13.51/2.77 % (3436236)Termination reason: Instruction limit % 13.51/2.77 % (3436236)Termination phase: Saturation % 13.51/2.77 % (3436236)Time elapsed: 0.087 s % 13.51/2.77 % (3436236)Peak memory usage: 90 MB % 13.51/2.77 % (3436236)Instructions burned: 142 (million) % 13.51/2.77 % (3436234)Instruction limit reached! % 13.51/2.77 % (3436234)------------------------------ % 13.51/2.77 % (3436234)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.51/2.77 % (3436234)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.51/2.77 % (3436234)CaDiCaL version: 2.1.3 % 13.51/2.77 % (3436234)Termination reason: Instruction limit % 13.51/2.77 % (3436234)Termination phase: Saturation % 13.51/2.77 % (3436234)Time elapsed: 0.201 s % 13.51/2.77 % (3436234)Peak memory usage: 93 MB % 13.51/2.77 % (3436234)Instructions burned: 383 (million) % 13.51/2.77 % (3436245)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=1633691478:i=121:nm=16:rtra=on_2986 on theBenchmark for (2986ds/121Mi) % 13.51/2.77 % (3436239)------------------------------ % 13.51/2.77 % (3436239)------------------------------ % 13.51/2.77 % (3436232)------------------------------ % 13.51/2.77 % (3436232)------------------------------ % 13.51/2.77 % (3436246)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=655766927:s2a=on:i=128:s2at=5:ins=3:rtra=on_2985 on theBenchmark for (2985ds/128Mi) % 13.51/2.77 % (3436245)Instruction limit reached! % 13.51/2.77 % (3436245)------------------------------ % 13.51/2.77 % (3436245)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.51/2.77 % (3436245)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.51/2.77 % (3436245)CaDiCaL version: 2.1.3 % 13.51/2.77 % (3436245)Termination reason: Instruction limit % 13.51/2.77 % (3436245)Termination phase: Saturation % 13.51/2.77 % (3436245)Time elapsed: 0.070 s % 13.51/2.77 % (3436245)Peak memory usage: 90 MB % 13.51/2.77 % (3436245)Instructions burned: 121 (million) % 13.51/2.77 % (3436246)Refutation not found, incomplete strategy % 13.51/2.77 % (3436246)------------------------------ % 13.51/2.77 % (3436246)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.51/2.77 % (3436246)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.51/2.77 % (3436246)CaDiCaL version: 2.1.3 % 13.51/2.77 % (3436246)Termination reason: Refutation not found, incomplete strategy % 13.51/2.77 % (3436246)Time elapsed: 0.033 s % 13.51/2.77 % (3436246)Peak memory usage: 113 MB % 13.51/2.77 % (3436246)Instructions burned: 16 (million) % 13.51/2.77 % (3436249)dis+1010_1_to=kbo:si=on:random_seed=909769296:i=175:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2984 on theBenchmark for (2984ds/175Mi) % 13.51/2.77 % (3436248)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=2796654454:i=39:ins=3:rtra=on_2985 on theBenchmark for (2985ds/39Mi) % 13.51/2.77 % (3436248)Refutation not found, incomplete strategy % 17.19/3.13 % (3436248)------------------------------ % 17.19/3.13 % (3436248)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.19/3.13 % (3436248)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.19/3.13 % (3436248)CaDiCaL version: 2.1.3 % 17.19/3.13 % (3436248)Termination reason: Refutation not found, incomplete strategy % 17.19/3.13 % (3436248)Time elapsed: 0.032 s % 17.19/3.13 % (3436248)Peak memory usage: 113 MB % 17.19/3.13 % (3436248)Instructions burned: 15 (million) % 17.19/3.13 % (3436229)Instruction limit reached! % 17.19/3.13 % (3436229)------------------------------ % 17.19/3.13 % (3436229)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.19/3.13 % (3436229)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.19/3.13 % (3436229)CaDiCaL version: 2.1.3 % 17.19/3.13 % (3436229)Termination reason: Instruction limit % 17.19/3.13 % (3436229)Termination phase: Saturation % 17.19/3.13 % (3436229)Time elapsed: 0.441 s % 17.19/3.13 % (3436229)Peak memory usage: 139 MB % 17.19/3.13 % (3436229)Instructions burned: 599 (million) % 17.19/3.13 % (3436249)Instruction limit reached! % 17.19/3.13 % (3436249)------------------------------ % 17.19/3.13 % (3436249)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.19/3.13 % (3436249)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.19/3.13 % (3436249)CaDiCaL version: 2.1.3 % 17.19/3.13 % (3436249)Termination reason: Instruction limit % 17.19/3.13 % (3436249)Termination phase: Saturation % 17.19/3.13 % (3436249)Time elapsed: 0.062 s % 17.19/3.13 % (3436249)Peak memory usage: 91 MB % 17.19/3.13 % (3436249)Instructions burned: 175 (million) % 17.19/3.13 % (3436251)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=390017836:i=329:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2984 on theBenchmark for (2984ds/329Mi) % 17.19/3.13 % (3436252)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=3536131017:s2a=on:i=483:doe=on:nm=32:rtra=on_2984 on theBenchmark for (2984ds/483Mi) % 17.19/3.13 % (3436256)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=341925548:i=349:rtra=on_2983 on theBenchmark for (2983ds/349Mi) % 17.19/3.13 % (3436255)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=1510126215:thitd=on:i=215:nm=0:rtra=on:ev=force_2983 on theBenchmark for (2983ds/215Mi) % 17.19/3.13 % (3436246)------------------------------ % 17.19/3.13 % (3436246)------------------------------ % 17.19/3.13 % (3436256)Instruction limit reached! % 17.19/3.13 % (3436256)------------------------------ % 17.19/3.13 % (3436256)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.19/3.13 % (3436256)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.19/3.13 % (3436256)CaDiCaL version: 2.1.3 % 17.19/3.13 % (3436256)Termination reason: Instruction limit % 17.19/3.13 % (3436256)Termination phase: Saturation % 17.19/3.13 % (3436256)Time elapsed: 0.125 s % 17.19/3.13 % (3436256)Peak memory usage: 119 MB % 17.19/3.13 % (3436256)Instructions burned: 351 (million) % 17.19/3.13 % (3436248)------------------------------ % 17.19/3.13 % (3436248)------------------------------ % 17.19/3.13 % (3436233)Instruction limit reached! % 17.19/3.13 % (3436233)------------------------------ % 17.19/3.13 % (3436233)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.19/3.13 % (3436233)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.19/3.13 % (3436233)CaDiCaL version: 2.1.3 % 17.19/3.13 % (3436233)Termination reason: Instruction limit % 17.19/3.13 % (3436233)Termination phase: Saturation % 17.19/3.13 % (3436233)Time elapsed: 0.597 s % 17.19/3.13 % (3436233)Peak memory usage: 96 MB % 17.19/3.13 % (3436233)Instructions burned: 1000 (million) % 17.19/3.13 % (3436251)Instruction limit reached! % 17.19/3.13 % (3436251)------------------------------ % 17.19/3.13 % (3436251)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.19/3.13 % (3436251)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.19/3.13 % (3436251)CaDiCaL version: 2.1.3 % 17.19/3.13 % (3436251)Termination reason: Instruction limit % 17.19/3.13 % (3436251)Termination phase: Saturation % 17.19/3.13 % (3436251)Time elapsed: 0.236 s % 17.19/3.13 % (3436251)Peak memory usage: 118 MB % 17.19/3.13 % (3436251)Instructions burned: 330 (million) % 17.19/3.13 % (3436255)Instruction limit reached! % 17.19/3.13 % (3436255)------------------------------ % 18.49/3.35 % (3436255)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.49/3.35 % (3436255)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.49/3.35 % (3436255)CaDiCaL version: 2.1.3 % 18.49/3.35 % (3436255)Termination reason: Instruction limit % 18.49/3.35 % (3436255)Termination phase: Saturation % 18.49/3.35 % (3436255)Time elapsed: 0.181 s % 18.49/3.35 % (3436255)Peak memory usage: 137 MB % 18.49/3.35 % (3436255)Instructions burned: 216 (million) % 18.49/3.35 % (3436262)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=1773757656:i=328:kws=inv_frequency:nm=20:rtra=on_2981 on theBenchmark for (2981ds/328Mi) % 18.49/3.35 % (3436261)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=4065876645:st=2:i=295:rtra=on:ss=axioms_2981 on theBenchmark for (2981ds/295Mi) % 18.49/3.35 % (3436261)Refutation not found, incomplete strategy % 18.49/3.35 % (3436261)------------------------------ % 18.49/3.35 % (3436261)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.49/3.35 % (3436261)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.49/3.35 % (3436261)CaDiCaL version: 2.1.3 % 18.49/3.35 % (3436261)Termination reason: Refutation not found, incomplete strategy % 18.49/3.35 % (3436261)Time elapsed: 0.002 s % 18.49/3.35 % (3436261)Peak memory usage: 88 MB % 18.49/3.35 % (3436261)Instructions burned: 3 (million) % 18.49/3.35 % (3436263)dis+1010_1_to=lpo:sil=128000:sas=z3:si=on:nwc=5:random_seed=1333322872:i=281:gtgl=2:rtra=on:gtg=all_2981 on theBenchmark for (2981ds/281Mi) % 18.49/3.35 % (3436264)lrs+1010_1_to=kbo:sil=128000:si=on:sos=on:urr=on:uwa=alasca_main:random_seed=3751188609:i=484:doe=on:nm=0:av=off:rtra=on:ss=axioms_2981 on theBenchmark for (2981ds/484Mi) % 18.49/3.35 % (3436264)Refutation not found, incomplete strategy % 18.49/3.35 % (3436264)------------------------------ % 18.49/3.35 % (3436264)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.49/3.35 % (3436264)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.49/3.35 % (3436264)CaDiCaL version: 2.1.3 % 18.49/3.35 % (3436264)Termination reason: Refutation not found, incomplete strategy % 18.49/3.35 % (3436264)Time elapsed: 0.002 s % 18.49/3.35 % (3436264)Peak memory usage: 87 MB % 18.49/3.35 % (3436264)Instructions burned: 2 (million) % 18.49/3.35 % (3436252)Instruction limit reached! % 18.49/3.35 % (3436252)------------------------------ % 18.49/3.35 % (3436252)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.49/3.35 % (3436252)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.49/3.35 % (3436252)CaDiCaL version: 2.1.3 % 18.49/3.35 % (3436252)Termination reason: Instruction limit % 18.49/3.35 % (3436252)Termination phase: Saturation % 18.49/3.35 % (3436252)Time elapsed: 0.354 s % 18.49/3.35 % (3436252)Peak memory usage: 137 MB % 18.49/3.35 % (3436252)Instructions burned: 484 (million) % 18.49/3.35 % (3436265)lrs+21_1_to=kbo:sil=128000:thi=neg_eq:si=on:random_seed=2112498891:i=321:canc=force:rtra=on:tac=axiom:ss=axioms:ev=force_2980 on theBenchmark for (2980ds/321Mi) % 18.49/3.35 % (3436262)Instruction limit reached! % 18.49/3.35 % (3436262)------------------------------ % 18.49/3.35 % (3436262)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.49/3.35 % (3436262)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.49/3.35 % (3436262)CaDiCaL version: 2.1.3 % 18.49/3.35 % (3436262)Termination reason: Instruction limit % 18.49/3.35 % (3436262)Termination phase: Saturation % 18.49/3.35 % (3436262)Time elapsed: 0.123 s % 18.49/3.35 % (3436262)Peak memory usage: 119 MB % 18.49/3.35 % (3436262)Instructions burned: 331 (million) % 18.49/3.35 % (3436265)Refutation not found, incomplete strategy % 18.49/3.35 % (3436265)------------------------------ % 18.49/3.35 % (3436265)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.49/3.35 % (3436265)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.49/3.35 % (3436265)CaDiCaL version: 2.1.3 % 18.49/3.35 % (3436265)Termination reason: Refutation not found, incomplete strategy % 18.49/3.35 % (3436265)Time elapsed: 0.027 s % 18.49/3.35 % (3436265)Peak memory usage: 111 MB % 18.49/3.35 % (3436265)Instructions burned: 7 (million) % 18.49/3.35 % (3436268)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=3060282948:i=416:rtra=on:gtg=position:ss=axioms_2980 on theBenchmark for (2980ds/416Mi) % 18.49/3.35 % (3436268)Refutation not found, incomplete strategy % 20.17/3.70 % (3436268)------------------------------ % 20.17/3.70 % (3436268)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.17/3.70 % (3436268)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.17/3.70 % (3436268)CaDiCaL version: 2.1.3 % 20.17/3.70 % (3436268)Termination reason: Refutation not found, incomplete strategy % 20.17/3.70 % (3436268)Time elapsed: 0.027 s % 20.17/3.70 % (3436268)Peak memory usage: 111 MB % 20.17/3.70 % (3436268)Instructions burned: 7 (million) % 20.17/3.70 % (3436273)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=3077354821:avsq=on:i=276:avsqr=1,2:rtra=on_2979 on theBenchmark for (2979ds/276Mi) % 20.17/3.70 % (3436272)lrs+1010_1_to=kbo:tgt=ground:fde=unused:sas=z3:si=on:sp=unary_frequency:gve=force:spb=goal:tha=off:random_seed=2682208729:i=471:thf=on:kws=precedence:rtra=on_2979 on theBenchmark for (2979ds/471Mi) % 20.17/3.70 % (3436263)Instruction limit reached! % 20.17/3.70 % (3436263)------------------------------ % 20.17/3.70 % (3436263)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.17/3.70 % (3436263)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.17/3.70 % (3436263)CaDiCaL version: 2.1.3 % 20.17/3.70 % (3436263)Termination reason: Instruction limit % 20.17/3.70 % (3436263)Termination phase: Saturation % 20.17/3.70 % (3436263)Time elapsed: 0.183 s % 20.17/3.70 % (3436263)Peak memory usage: 118 MB % 20.17/3.70 % (3436263)Instructions burned: 282 (million) % 20.17/3.70 % (3436261)------------------------------ % 20.17/3.70 % (3436261)------------------------------ % 20.17/3.70 % (3436264)------------------------------ % 20.17/3.70 % (3436264)------------------------------ % 20.17/3.70 % (3436273)Instruction limit reached! % 20.17/3.70 % (3436273)------------------------------ % 20.17/3.70 % (3436273)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.17/3.70 % (3436273)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.17/3.70 % (3436273)CaDiCaL version: 2.1.3 % 20.17/3.70 % (3436273)Termination reason: Instruction limit % 20.17/3.70 % (3436273)Termination phase: Saturation % 20.17/3.70 % (3436273)Time elapsed: 0.123 s % 20.17/3.70 % (3436273)Peak memory usage: 136 MB % 20.17/3.70 % (3436273)Instructions burned: 277 (million) % 20.17/3.70 % (3436277)lrs+1010_2_to=kbo:sil=128000:tgt=ground:fde=unused:sas=z3:si=on:uwa=off:tha=off:nwc=1:random_seed=77044885:i=375:kws=inv_arity_squared:rtra=on_2978 on theBenchmark for (2978ds/375Mi) % 20.17/3.70 % (3436265)------------------------------ % 20.17/3.70 % (3436265)------------------------------ % 20.17/3.70 % (3436278)lrs+10_1_to=kbo:sil=128000:tgt=full:sas=z3:si=on:uwa=func_ext:slsqc=1:flr=on:slsq=on:random_seed=527296583:i=387:bd=preordered:rtra=on:ss=axioms:sgt=8_2977 on theBenchmark for (2977ds/387Mi) % 20.17/3.70 % (3436268)------------------------------ % 20.17/3.70 % (3436268)------------------------------ % 20.17/3.70 % (3436278)Refutation not found, incomplete strategy % 20.17/3.70 % (3436278)------------------------------ % 20.17/3.70 % (3436278)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.17/3.70 % (3436278)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.17/3.70 % (3436278)CaDiCaL version: 2.1.3 % 20.17/3.70 % (3436278)Termination reason: Refutation not found, incomplete strategy % 20.17/3.70 % (3436278)Time elapsed: 0.029 s % 20.17/3.70 % (3436278)Peak memory usage: 111 MB % 20.17/3.70 % (3436278)Instructions burned: 8 (million) % 20.17/3.70 % (3436280)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=1182315393:i=334:rtra=on_2976 on theBenchmark for (2976ds/334Mi) % 20.17/3.70 % (3436279)lrs+10_1_to=kbo:sil=128000:fde=none:si=on:norm_ineq=on:urr=on:nwc=0.5:random_seed=4240491672:i=513:kws=frequency:bd=all:rtra=on:gtg=exists_all:ss=axioms:sgt=4_2977 on theBenchmark for (2977ds/513Mi) % 20.17/3.70 % (3436272)Instruction limit reached! % 20.17/3.70 % (3436272)------------------------------ % 20.17/3.70 % (3436272)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.17/3.70 % (3436272)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.17/3.70 % (3436272)CaDiCaL version: 2.1.3 % 20.17/3.70 % (3436272)Termination reason: Instruction limit % 20.17/3.70 % (3436272)Termination phase: Saturation % 20.17/3.70 % (3436272)Time elapsed: 0.288 s % 20.17/3.70 % (3436272)Peak memory usage: 119 MB % 20.17/3.70 % (3436272)Instructions burned: 472 (million) % 20.17/3.70 % (3436282)lrs+1010_1_to=kbo:sil=64000:sas=cadical:si=on:sos=on:bce=on:random_seed=1404461112:i=359:rtra=on:gtg=exists_top:ss=axioms_2976 on theBenchmark for (2976ds/359Mi) % 24.24/4.04 % (3436284)dis+1010_1_to=lpo:sil=128000:thi=all:fde=unused:si=on:sp=reverse_arity:tha=off:random_seed=2702059878:i=341:gtgl=2:rtra=on:gtg=exists_sym:ev=force:fsd=on:fsdmm=1_2976 on theBenchmark for (2976ds/341Mi) % 24.24/4.04 % (3436280)Instruction limit reached! % 24.24/4.04 % (3436280)------------------------------ % 24.24/4.04 % (3436280)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.24/4.04 % (3436280)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.24/4.04 % (3436280)CaDiCaL version: 2.1.3 % 24.24/4.04 % (3436280)Termination reason: Instruction limit % 24.24/4.04 % (3436280)Termination phase: Saturation % 24.24/4.04 % (3436280)Time elapsed: 0.143 s % 24.24/4.04 % (3436280)Peak memory usage: 137 MB % 24.24/4.04 % (3436280)Instructions burned: 336 (million) % 24.24/4.04 % (3436277)Instruction limit reached! % 24.24/4.04 % (3436277)------------------------------ % 24.24/4.04 % (3436277)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.24/4.04 % (3436277)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.24/4.04 % (3436277)CaDiCaL version: 2.1.3 % 24.24/4.04 % (3436277)Termination reason: Instruction limit % 24.24/4.04 % (3436277)Termination phase: Saturation % 24.24/4.04 % (3436277)Time elapsed: 0.253 s % 24.24/4.04 % (3436277)Peak memory usage: 121 MB % 24.24/4.04 % (3436277)Instructions burned: 377 (million) % 24.24/4.04 % (3436288)lrs-2_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_max:tha=off:random_seed=1305817750:st=1.5:i=261:sd=1:kws=precedence:rtra=on:ss=axioms_2975 on theBenchmark for (2975ds/261Mi) % 24.24/4.04 % (3436290)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=2102343732:s2pl=no:i=235:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2974 on theBenchmark for (2974ds/235Mi) % 24.24/4.04 % (3436278)------------------------------ % 24.24/4.04 % (3436278)------------------------------ % 24.24/4.04 % (3436290)Refutation not found, incomplete strategy % 24.24/4.04 % (3436290)------------------------------ % 24.24/4.04 % (3436290)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.24/4.04 % (3436290)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.24/4.04 % (3436290)CaDiCaL version: 2.1.3 % 24.24/4.04 % (3436290)Termination reason: Refutation not found, incomplete strategy % 24.24/4.04 % (3436290)Time elapsed: 0.017 s % 24.24/4.04 % (3436290)Peak memory usage: 111 MB % 24.24/4.04 % (3436290)Instructions burned: 7 (million) % 24.24/4.04 % (3436288)Refutation not found, incomplete strategy % 24.24/4.04 % (3436288)------------------------------ % 24.24/4.04 % (3436288)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.24/4.04 % (3436288)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.24/4.04 % (3436288)CaDiCaL version: 2.1.3 % 24.24/4.04 % (3436288)Termination reason: Refutation not found, incomplete strategy % 24.24/4.04 % (3436288)Time elapsed: 0.027 s % 24.24/4.04 % (3436288)Peak memory usage: 111 MB % 24.24/4.04 % (3436288)Instructions burned: 6 (million) % 24.24/4.04 % (3436279)Instruction limit reached! % 24.24/4.04 % (3436279)------------------------------ % 24.24/4.04 % (3436279)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.24/4.04 % (3436279)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.24/4.04 % (3436279)CaDiCaL version: 2.1.3 % 24.24/4.04 % (3436279)Termination reason: Instruction limit % 24.24/4.04 % (3436279)Termination phase: Saturation % 24.24/4.04 % (3436279)Time elapsed: 0.286 s % 24.24/4.04 % (3436279)Peak memory usage: 94 MB % 24.24/4.04 % (3436279)Instructions burned: 514 (million) % 24.24/4.04 % (3436284)Instruction limit reached! % 24.24/4.04 % (3436284)------------------------------ % 24.24/4.04 % (3436284)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.24/4.04 % (3436284)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.24/4.04 % (3436284)CaDiCaL version: 2.1.3 % 24.24/4.04 % (3436284)Termination reason: Instruction limit % 24.24/4.04 % (3436284)Termination phase: Saturation % 24.24/4.04 % (3436284)Time elapsed: 0.194 s % 24.24/4.04 % (3436284)Peak memory usage: 120 MB % 24.24/4.04 % (3436284)Instructions burned: 341 (million) % 24.24/4.04 % (3436282)Instruction limit reached! % 24.24/4.04 % (3436282)------------------------------ % 24.24/4.04 % (3436282)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.62/4.50 % (3436282)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.62/4.50 % (3436282)CaDiCaL version: 2.1.3 % 26.62/4.50 % (3436282)Termination reason: Instruction limit % 26.62/4.50 % (3436282)Termination phase: Saturation % 26.62/4.50 % (3436282)Time elapsed: 0.220 s % 26.62/4.50 % (3436282)Peak memory usage: 92 MB % 26.62/4.50 % (3436282)Instructions burned: 360 (million) % 26.62/4.50 % (3436291)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=3904524157:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2974 on theBenchmark for (2974ds/273Mi) % 26.62/4.50 % (3436294)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=3031293235:i=146:doe=on:rtra=on_2973 on theBenchmark for (2973ds/146Mi) % 26.62/4.50 % (3436290)------------------------------ % 26.62/4.50 % (3436290)------------------------------ % 26.62/4.50 % (3436295)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=10194842:i=4428:doe=on:fsr=off:rtra=on_2973 on theBenchmark for (2973ds/4428Mi) % 26.62/4.50 % (3436297)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=3730220297:i=1052:rtra=on_2972 on theBenchmark for (2972ds/1052Mi) % 26.62/4.50 % (3436296)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=2632830060:avsq=on:i=276:avsqr=1,2:rtra=on_2972 on theBenchmark for (2972ds/276Mi) % 26.62/4.50 % (3436294)Instruction limit reached! % 26.62/4.50 % (3436294)------------------------------ % 26.62/4.50 % (3436294)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.62/4.50 % (3436294)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.62/4.50 % (3436294)CaDiCaL version: 2.1.3 % 26.62/4.50 % (3436294)Termination reason: Instruction limit % 26.62/4.50 % (3436294)Termination phase: Saturation % 26.62/4.50 % (3436294)Time elapsed: 0.091 s % 26.62/4.50 % (3436294)Peak memory usage: 90 MB % 26.62/4.50 % (3436294)Instructions burned: 147 (million) % 26.62/4.50 % (3436300)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=4065857383:i=655:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2972 on theBenchmark for (2972ds/655Mi) % 26.62/4.50 % (3436291)Instruction limit reached! % 26.62/4.50 % (3436291)------------------------------ % 26.62/4.50 % (3436291)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.62/4.50 % (3436291)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.62/4.50 % (3436291)CaDiCaL version: 2.1.3 % 26.62/4.50 % (3436291)Termination reason: Instruction limit % 26.62/4.50 % (3436291)Termination phase: Saturation % 26.62/4.50 % (3436291)Time elapsed: 0.170 s % 26.62/4.50 % (3436291)Peak memory usage: 92 MB % 26.62/4.50 % (3436291)Instructions burned: 274 (million) % 26.62/4.50 % (3436288)------------------------------ % 26.62/4.50 % (3436288)------------------------------ % 26.62/4.50 % (3436304)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=1460036826:st=5:i=1054:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2971 on theBenchmark for (2971ds/1054Mi) % 26.62/4.50 % (3436304)Refutation not found, incomplete strategy % 26.62/4.50 % (3436304)------------------------------ % 26.62/4.50 % (3436304)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.62/4.50 % (3436304)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.62/4.50 % (3436304)CaDiCaL version: 2.1.3 % 26.62/4.50 % (3436304)Termination reason: Refutation not found, incomplete strategy % 26.62/4.50 % (3436304)Time elapsed: 0.002 s % 26.62/4.50 % (3436304)Peak memory usage: 87 MB % 26.62/4.50 % (3436304)Instructions burned: 1 (million) % 26.62/4.50 % (3436307)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=775710315:s2a=on:i=450:doe=on:nm=32:rtra=on_2971 on theBenchmark for (2971ds/450Mi) % 26.62/4.50 % (3436306)lrs-1002_1_to=kbo:sas=z3:si=on:norm_ineq=on:sos=on:tha=some:random_seed=1203941557:i=107:rtra=on_2971 on theBenchmark for (2971ds/107Mi) % 26.62/4.50 % (3436296)Instruction limit reached! % 26.62/4.50 % (3436296)------------------------------ % 26.62/4.50 % (3436296)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.62/4.50 % (3436296)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.84/4.83 % (3436296)CaDiCaL version: 2.1.3 % 27.84/4.83 % (3436296)Termination reason: Instruction limit % 27.84/4.83 % (3436296)Termination phase: Saturation % 27.84/4.83 % (3436296)Time elapsed: 0.222 s % 27.84/4.83 % (3436296)Peak memory usage: 137 MB % 27.84/4.83 % (3436296)Instructions burned: 277 (million) % 27.84/4.83 % (3436306)Refutation not found, incomplete strategy % 27.84/4.83 % (3436306)------------------------------ % 27.84/4.83 % (3436306)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.84/4.83 % (3436306)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.84/4.83 % (3436306)CaDiCaL version: 2.1.3 % 27.84/4.83 % (3436306)Termination reason: Refutation not found, incomplete strategy % 27.84/4.83 % (3436306)Time elapsed: 0.032 s % 27.84/4.83 % (3436306)Peak memory usage: 113 MB % 27.84/4.83 % (3436306)Instructions burned: 14 (million) % 27.84/4.83 % (3436300)Instruction limit reached! % 27.84/4.83 % (3436300)------------------------------ % 27.84/4.83 % (3436300)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.84/4.83 % (3436300)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.84/4.83 % (3436300)CaDiCaL version: 2.1.3 % 27.84/4.83 % (3436300)Termination reason: Instruction limit % 27.84/4.83 % (3436300)Termination phase: Saturation % 27.84/4.83 % (3436300)Time elapsed: 0.193 s % 27.84/4.83 % (3436300)Peak memory usage: 96 MB % 27.84/4.83 % (3436300)Instructions burned: 656 (million) % 27.84/4.83 % (3436312)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=1574477602:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2969 on theBenchmark for (2969ds/130Mi) % 27.84/4.83 % (3436311)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 % 27.84/4.83 % (3436311)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=3330294620:i=1090:aac=none:nm=0:rtra=on:rawr=on_2969 on theBenchmark for (2969ds/1090Mi) % 27.84/4.83 % (3436304)------------------------------ % 27.84/4.83 % (3436304)------------------------------ % 27.84/4.83 % (3436312)Instruction limit reached! % 27.84/4.83 % (3436312)------------------------------ % 27.84/4.83 % (3436312)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.84/4.83 % (3436312)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.84/4.83 % (3436312)CaDiCaL version: 2.1.3 % 27.84/4.83 % (3436312)Termination reason: Instruction limit % 27.84/4.83 % (3436312)Termination phase: Saturation % 27.84/4.83 % (3436312)Time elapsed: 0.059 s % 27.84/4.83 % (3436312)Peak memory usage: 119 MB % 27.84/4.83 % (3436312)Instructions burned: 130 (million) % 27.84/4.83 % (3436306)------------------------------ % 27.84/4.83 % (3436306)------------------------------ % 27.84/4.83 % (3436316)ott+10_1_to=kbo:sil=64000:si=on:sp=reverse_frequency:sos=on:random_seed=3713870823:i=491:doe=on:rtra=on:gtg=position_2967 on theBenchmark for (2967ds/491Mi) % 27.84/4.83 % (3436316)Refutation not found, incomplete strategy % 27.84/4.83 % (3436316)------------------------------ % 27.84/4.83 % (3436316)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.84/4.83 % (3436316)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.84/4.83 % (3436316)CaDiCaL version: 2.1.3 % 27.84/4.83 % (3436316)Termination reason: Refutation not found, incomplete strategy % 27.84/4.83 % (3436316)Time elapsed: 0.004 s % 27.84/4.83 % (3436316)Peak memory usage: 89 MB % 27.84/4.83 % (3436316)Instructions burned: 10 (million) % 27.84/4.83 % (3436307)Instruction limit reached! % 27.84/4.83 % (3436307)------------------------------ % 27.84/4.83 % (3436307)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.84/4.83 % (3436307)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.84/4.83 % (3436307)CaDiCaL version: 2.1.3 % 27.84/4.83 % (3436307)Termination reason: Instruction limit % 27.84/4.83 % (3436307)Termination phase: Saturation % 27.84/4.83 % (3436307)Time elapsed: 0.327 s % 27.84/4.83 % (3436307)Peak memory usage: 137 MB % 27.84/4.83 % (3436307)Instructions burned: 451 (million) % 27.84/4.83 % (3436315)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=696369059:i=312:kws=inv_frequency:nm=20:rtra=on_2967 on theBenchmark for (2967ds/312Mi) % 27.84/4.83 % (3436297)Instruction limit reached! % 27.84/4.83 % (3436297)------------------------------ % 27.84/4.83 % (3436297)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.45/5.48 % (3436297)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.45/5.48 % (3436297)CaDiCaL version: 2.1.3 % 33.45/5.48 % (3436297)Termination reason: Instruction limit % 33.45/5.48 % (3436297)Termination phase: Saturation % 33.45/5.48 % (3436297)Time elapsed: 0.564 s % 33.45/5.48 % (3436297)Peak memory usage: 95 MB % 33.45/5.48 % (3436297)Instructions burned: 1053 (million) % 33.45/5.48 % (3436317)ott+1011_4:1_to=lpo:sil=64000:si=on:spb=intro:random_seed=2914158391:s2a=on:i=835:s2at=2:rtra=on_2966 on theBenchmark for (2966ds/835Mi) % 33.45/5.48 % (3436316)------------------------------ % 33.45/5.48 % (3436316)------------------------------ % 33.45/5.48 % (3436319)ott+1011_2_to=lpo:sil=128000:si=on:sos=on:random_seed=347853330:i=307:bd=preordered:av=off:rtra=on:ev=cautious_2966 on theBenchmark for (2966ds/307Mi) % 33.45/5.48 % (3436319)Refutation not found, incomplete strategy % 33.45/5.48 % (3436319)------------------------------ % 33.45/5.48 % (3436319)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.45/5.48 % (3436319)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.45/5.49 % (3436319)CaDiCaL version: 2.1.3 % 33.45/5.49 % (3436319)Termination reason: Refutation not found, incomplete strategy % 33.45/5.49 % (3436319)Time elapsed: 0.008 s % 33.45/5.49 % (3436319)Peak memory usage: 89 MB % 33.45/5.49 % (3436319)Instructions burned: 13 (million) % 33.45/5.49 % (3436321)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=3506552821:i=776:doe=on:rtra=on_2966 on theBenchmark for (2966ds/776Mi) % 33.45/5.49 % (3436323)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=3906119304:s2a=on:i=646:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2965 on theBenchmark for (2965ds/646Mi) % 33.45/5.49 % (3436315)Instruction limit reached! % 33.45/5.49 % (3436315)------------------------------ % 33.45/5.49 % (3436315)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.45/5.49 % (3436315)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.45/5.49 % (3436315)CaDiCaL version: 2.1.3 % 33.45/5.49 % (3436315)Termination reason: Instruction limit % 33.45/5.49 % (3436315)Termination phase: Saturation % 33.45/5.49 % (3436315)Time elapsed: 0.215 s % 33.45/5.49 % (3436315)Peak memory usage: 120 MB % 33.45/5.49 % (3436315)Instructions burned: 312 (million) % 33.45/5.49 % (3436327)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=3556104453:thitd=on:cond=fast:i=784:nm=30:rtra=on:gtg=all:tac=axiom_2964 on theBenchmark for (2964ds/784Mi) % 33.45/5.49 % (3436319)------------------------------ % 33.45/5.49 % (3436319)------------------------------ % 33.45/5.49 % (3436311)Instruction limit reached! % 33.45/5.49 % (3436311)------------------------------ % 33.45/5.49 % (3436311)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.45/5.49 % (3436311)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.45/5.49 % (3436311)CaDiCaL version: 2.1.3 % 33.45/5.49 % (3436311)Termination reason: Instruction limit % 33.45/5.49 % (3436311)Termination phase: Saturation % 33.45/5.49 % (3436311)Time elapsed: 0.576 s % 33.45/5.49 % (3436311)Peak memory usage: 120 MB % 33.45/5.49 % (3436311)Instructions burned: 1092 (million) % 33.45/5.49 % (3436317)Instruction limit reached! % 33.45/5.49 % (3436317)------------------------------ % 33.45/5.49 % (3436317)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.45/5.49 % (3436317)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.45/5.49 % (3436317)CaDiCaL version: 2.1.3 % 33.45/5.49 % (3436317)Termination reason: Instruction limit % 33.45/5.49 % (3436317)Termination phase: Saturation % 33.45/5.49 % (3436317)Time elapsed: 0.331 s % 33.45/5.49 % (3436317)Peak memory usage: 90 MB % 33.45/5.49 % (3436317)Instructions burned: 837 (million) % 33.45/5.49 % (3436323)Instruction limit reached! % 33.45/5.49 % (3436323)------------------------------ % 33.45/5.49 % (3436323)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.45/5.49 % (3436323)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.45/5.49 % (3436323)CaDiCaL version: 2.1.3 % 33.45/5.49 % (3436323)Termination reason: Instruction limit % 33.45/5.49 % (3436323)Termination phase: Saturation % 33.45/5.49 % (3436323)Time elapsed: 0.237 s % 33.45/5.49 % (3436323)Peak memory usage: 139 MB % 33.45/5.49 % (3436323)Instructions burned: 649 (million) % 33.45/5.49 % (3436329)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=2741236656:thitd=on:s2a=on:i=1131:add=on:canc=force:bd=all:rtra=on:tac=axiom:ev=off_2962 on theBenchmark for (2962ds/1131Mi) % 39.43/6.24 % (3436332)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=448493495:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2961 on theBenchmark for (2961ds/273Mi) % 39.43/6.24 % (3436330)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=170056403:s2pl=no:i=246:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2962 on theBenchmark for (2962ds/246Mi) % 39.43/6.24 % (3436330)Refutation not found, incomplete strategy % 39.43/6.24 % (3436330)------------------------------ % 39.43/6.24 % (3436330)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.43/6.24 % (3436330)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.43/6.24 % (3436330)CaDiCaL version: 2.1.3 % 39.43/6.24 % (3436330)Termination reason: Refutation not found, incomplete strategy % 39.43/6.24 % (3436330)Time elapsed: 0.027 s % 39.43/6.24 % (3436330)Peak memory usage: 111 MB % 39.43/6.24 % (3436330)Instructions burned: 7 (million) % 39.43/6.24 % (3436331)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=1082725057:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2962 on theBenchmark for (2962ds/775Mi) % 39.43/6.24 % (3436331)Refutation not found, incomplete strategy % 39.43/6.24 % (3436331)------------------------------ % 39.43/6.24 % (3436331)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.43/6.24 % (3436331)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.43/6.24 % (3436331)CaDiCaL version: 2.1.3 % 39.43/6.24 % (3436331)Termination reason: Refutation not found, incomplete strategy % 39.43/6.24 % (3436331)Time elapsed: 0.002 s % 39.43/6.24 % (3436331)Peak memory usage: 88 MB % 39.43/6.24 % (3436331)Instructions burned: 3 (million) % 39.43/6.24 % (3436332)Instruction limit reached! % 39.43/6.24 % (3436332)------------------------------ % 39.43/6.24 % (3436332)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.43/6.24 % (3436332)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.43/6.24 % (3436332)CaDiCaL version: 2.1.3 % 39.43/6.24 % (3436332)Termination reason: Instruction limit % 39.43/6.24 % (3436332)Termination phase: Saturation % 39.43/6.24 % (3436332)Time elapsed: 0.089 s % 39.43/6.24 % (3436332)Peak memory usage: 92 MB % 39.43/6.24 % (3436332)Instructions burned: 275 (million) % 39.43/6.24 % (3436321)Instruction limit reached! % 39.43/6.24 % (3436321)------------------------------ % 39.43/6.24 % (3436321)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.43/6.24 % (3436321)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.43/6.24 % (3436321)CaDiCaL version: 2.1.3 % 39.43/6.24 % (3436321)Termination reason: Instruction limit % 39.43/6.24 % (3436321)Termination phase: Saturation % 39.43/6.24 % (3436321)Time elapsed: 0.478 s % 39.43/6.24 % (3436321)Peak memory usage: 122 MB % 39.43/6.24 % (3436321)Instructions burned: 777 (million) % 39.43/6.24 % (3436337)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=2045421:i=102:nm=16:rtra=on_2960 on theBenchmark for (2960ds/102Mi) % 39.43/6.24 % (3436337)Instruction limit reached! % 39.43/6.24 % (3436337)------------------------------ % 39.43/6.24 % (3436337)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.43/6.24 % (3436337)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.43/6.24 % (3436337)CaDiCaL version: 2.1.3 % 39.43/6.24 % (3436337)Termination reason: Instruction limit % 39.43/6.24 % (3436337)Termination phase: Saturation % 39.43/6.24 % (3436337)Time elapsed: 0.032 s % 39.43/6.24 % (3436337)Peak memory usage: 89 MB % 39.43/6.24 % (3436337)Instructions burned: 104 (million) % 39.43/6.24 % (3436338)lrs+10_1_to=lpo:sil=128000:si=on:bsr=unit_only:tha=off:random_seed=2473650560:avsq=on:s2a=on:i=1094:s2at=5:avsqr=4463,131072:rtra=on_2959 on theBenchmark for (2959ds/1094Mi) % 39.43/6.24 % (3436330)------------------------------ % 39.43/6.24 % (3436330)------------------------------ % 39.43/6.24 % (3436331)------------------------------ % 39.43/6.24 % (3436331)------------------------------ % 39.43/6.24 % (3436327)Instruction limit reached! % 39.43/6.24 % (3436327)------------------------------ % 39.43/6.24 % (3436327)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 45.73/7.31 % (3436327)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.73/7.31 % (3436327)CaDiCaL version: 2.1.3 % 45.73/7.31 % (3436327)Termination reason: Instruction limit % 45.73/7.31 % (3436327)Termination phase: Saturation % 45.73/7.31 % (3436327)Time elapsed: 0.456 s % 45.73/7.31 % (3436327)Peak memory usage: 120 MB % 45.73/7.31 % (3436327)Instructions burned: 785 (million) % 45.73/7.31 % (3436340)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=1806420592:i=6400:doe=on:fsr=off:rtra=on_2958 on theBenchmark for (2958ds/6400Mi) % 45.73/7.31 % (3436342)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=680271075:i=868:doe=on:nm=0:rtra=on:gtg=exists_sym_2958 on theBenchmark for (2958ds/868Mi) % 45.73/7.31 % (3436343)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=3992871089:i=1846:canc=cautious:fsr=off:rtra=on_2958 on theBenchmark for (2958ds/1846Mi) % 45.73/7.31 % (3436343)Refutation not found, incomplete strategy % 45.73/7.31 % (3436343)------------------------------ % 45.73/7.31 % (3436343)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 45.73/7.31 % (3436343)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.73/7.31 % (3436343)CaDiCaL version: 2.1.3 % 45.73/7.31 % (3436343)Termination reason: Refutation not found, incomplete strategy % 45.73/7.31 % (3436343)Time elapsed: 0.006 s % 45.73/7.31 % (3436343)Peak memory usage: 89 MB % 45.73/7.31 % (3436343)Instructions burned: 9 (million) % 45.73/7.31 % (3436344)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=3414372383:s2a=on:i=36816:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2958 on theBenchmark for (2958ds/36816Mi) % 45.73/7.31 % (3436329)Instruction limit reached! % 45.73/7.31 % (3436329)------------------------------ % 45.73/7.31 % (3436329)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 45.73/7.31 % (3436329)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.73/7.31 % (3436329)CaDiCaL version: 2.1.3 % 45.73/7.31 % (3436329)Termination reason: Instruction limit % 45.73/7.31 % (3436329)Termination phase: Saturation % 45.73/7.31 % (3436329)Time elapsed: 0.682 s % 45.73/7.31 % (3436329)Peak memory usage: 124 MB % 45.73/7.31 % (3436329)Instructions burned: 1132 (million) % 45.73/7.31 % (3436343)------------------------------ % 45.73/7.31 % (3436343)------------------------------ % 45.73/7.31 % (3436338)Instruction limit reached! % 45.73/7.31 % (3436338)------------------------------ % 45.73/7.31 % (3436338)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 45.73/7.31 % (3436338)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.73/7.31 % (3436338)CaDiCaL version: 2.1.3 % 45.73/7.31 % (3436338)Termination reason: Instruction limit % 45.73/7.31 % (3436338)Termination phase: Saturation % 45.73/7.31 % (3436338)Time elapsed: 0.482 s % 45.73/7.31 % (3436338)Peak memory usage: 92 MB % 45.73/7.31 % (3436338)Instructions burned: 1094 (million) % 45.73/7.31 % (3436350)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=1553122335:i=863:doe=on:nm=0:rtra=on:gtg=exists_sym_2954 on theBenchmark for (2954ds/863Mi) % 45.73/7.31 % (3436349)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=1714162689:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2954 on theBenchmark for (2954ds/273Mi) % 45.73/7.31 % (3436351)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=2171666712:i=5811:kws=precedence:nm=0:rtra=on_2953 on theBenchmark for (2953ds/5811Mi) % 45.73/7.31 % (3436342)Instruction limit reached! % 45.73/7.31 % (3436342)------------------------------ % 45.73/7.31 % (3436342)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 45.73/7.31 % (3436342)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.73/7.31 % (3436342)CaDiCaL version: 2.1.3 % 45.73/7.31 % (3436342)Termination reason: Instruction limit % 45.73/7.31 % (3436342)Termination phase: Saturation % 45.73/7.31 % (3436342)Time elapsed: 0.459 s % 45.73/7.31 % (3436342)Peak memory usage: 120 MB % 45.73/7.31 % (3436342)Instructions burned: 868 (million) % 45.73/7.31 % (3436349)Instruction limit reached! % 45.73/7.31 % (3436349)------------------------------ % 45.73/7.31 % (3436349)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 53.24/8.17 % (3436349)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.24/8.17 % (3436349)CaDiCaL version: 2.1.3 % 53.24/8.17 % (3436349)Termination reason: Instruction limit % 53.24/8.17 % (3436349)Termination phase: Saturation % 53.24/8.17 % (3436349)Time elapsed: 0.168 s % 53.24/8.17 % (3436349)Peak memory usage: 92 MB % 53.24/8.17 % (3436349)Instructions burned: 273 (million) % 53.24/8.17 % (3436355)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=4120267126:i=2216:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2952 on theBenchmark for (2952ds/2216Mi) % 53.24/8.17 % (3436356)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=2158072802:i=801:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2951 on theBenchmark for (2951ds/801Mi) % 53.24/8.17 % (3436295)Instruction limit reached! % 53.24/8.17 % (3436295)------------------------------ % 53.24/8.17 % (3436295)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 53.24/8.17 % (3436295)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.24/8.17 % (3436295)CaDiCaL version: 2.1.3 % 53.24/8.17 % (3436295)Termination reason: Instruction limit % 53.24/8.17 % (3436295)Termination phase: Saturation % 53.24/8.17 % (3436295)Time elapsed: 2.281 s % 53.24/8.17 % (3436295)Peak memory usage: 108 MB % 53.24/8.17 % (3436295)Instructions burned: 4428 (million) % 53.24/8.17 % (3436350)Instruction limit reached! % 53.24/8.17 % (3436350)------------------------------ % 53.24/8.17 % (3436350)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 53.24/8.17 % (3436350)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.24/8.17 % (3436350)CaDiCaL version: 2.1.3 % 53.24/8.17 % (3436350)Termination reason: Instruction limit % 53.24/8.17 % (3436350)Termination phase: Saturation % 53.24/8.17 % (3436350)Time elapsed: 0.457 s % 53.24/8.17 % (3436350)Peak memory usage: 120 MB % 53.24/8.17 % (3436350)Instructions burned: 863 (million) % 53.24/8.17 % (3436359)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=3159441380:st=5:i=1026:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2949 on theBenchmark for (2949ds/1026Mi) % 53.24/8.17 % (3436359)Refutation not found, incomplete strategy % 53.24/8.17 % (3436359)------------------------------ % 53.24/8.17 % (3436359)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 53.24/8.17 % (3436359)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.24/8.17 % (3436359)CaDiCaL version: 2.1.3 % 53.24/8.17 % (3436359)Termination reason: Refutation not found, incomplete strategy % 53.24/8.17 % (3436359)Time elapsed: 0.001 s % 53.24/8.17 % (3436359)Peak memory usage: 87 MB % 53.24/8.17 % (3436359)Instructions burned: 1 (million) % 53.24/8.17 % (3436360)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=3473621479:i=3509:rtra=on_2948 on theBenchmark for (2948ds/3509Mi) % 53.24/8.17 % (3436356)Instruction limit reached! % 53.24/8.17 % (3436356)------------------------------ % 53.24/8.17 % (3436356)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 53.24/8.17 % (3436356)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.24/8.17 % (3436356)CaDiCaL version: 2.1.3 % 53.24/8.17 % (3436356)Termination reason: Instruction limit % 53.24/8.17 % (3436356)Termination phase: Saturation % 53.24/8.17 % (3436356)Time elapsed: 0.417 s % 53.24/8.17 % (3436356)Peak memory usage: 96 MB % 53.24/8.17 % (3436356)Instructions burned: 802 (million) % 53.24/8.17 % (3436359)------------------------------ % 53.24/8.17 % (3436359)------------------------------ % 53.24/8.17 % (3436363)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=1145903879:st=2:i=2127:sd=12:ep=R:rtra=on:ss=axioms_2946 on theBenchmark for (2946ds/2127Mi) % 53.24/8.17 % (3436363)Refutation not found, incomplete strategy % 53.24/8.17 % (3436363)------------------------------ % 53.24/8.17 % (3436363)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 53.24/8.17 % (3436363)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.24/8.17 % (3436363)CaDiCaL version: 2.1.3 % 53.24/8.17 % (3436363)Termination reason: Refutation not found, incomplete strategy % 53.24/8.17 % (3436363)Time elapsed: 0.002 s % 53.24/8.17 % (3436363)Peak memory usage: 88 MB % 53.24/8.17 % (3436363)Instructions burned: 3 (million) % 53.24/8.17 % (3436364)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=916231847:i=1959:rtra=on:fsd=on:proc=on_2945 on theBenchmark for (2945ds/1959Mi) % 75.81/11.30 % (3436363)------------------------------ % 75.81/11.30 % (3436363)------------------------------ % 75.81/11.30 % (3436340)Instruction limit reached! % 75.81/11.30 % (3436340)------------------------------ % 75.81/11.30 % (3436340)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 75.81/11.30 % (3436340)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 75.81/11.30 % (3436340)CaDiCaL version: 2.1.3 % 75.81/11.30 % (3436340)Termination reason: Instruction limit % 75.81/11.30 % (3436340)Termination phase: Saturation % 75.81/11.30 % (3436340)Time elapsed: 1.697 s % 75.81/11.30 % (3436340)Peak memory usage: 112 MB % 75.81/11.30 % (3436340)Instructions burned: 6405 (million) % 75.81/11.30 % (3436367)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=1075758106:s2a=on:i=3553:nm=0:rtra=on_2942 on theBenchmark for (2942ds/3553Mi) % 75.81/11.30 % (3436355)Instruction limit reached! % 75.81/11.30 % (3436355)------------------------------ % 75.81/11.30 % (3436355)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 75.81/11.30 % (3436355)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 75.81/11.30 % (3436355)CaDiCaL version: 2.1.3 % 75.81/11.30 % (3436355)Termination reason: Instruction limit % 75.81/11.30 % (3436355)Termination phase: Saturation % 75.81/11.30 % (3436355)Time elapsed: 1.066 s % 75.81/11.30 % (3436355)Peak memory usage: 122 MB % 75.81/11.30 % (3436355)Instructions burned: 2216 (million) % 75.81/11.30 % (3436368)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=3215451749:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2941 on theBenchmark for (2941ds/3201Mi) % 75.81/11.30 % (3436370)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=1936464539:thitd=on:cond=on:i=4093:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2940 on theBenchmark for (2940ds/4093Mi) % 75.81/11.30 % (3436364)Instruction limit reached! % 75.81/11.30 % (3436364)------------------------------ % 75.81/11.30 % (3436364)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 75.81/11.30 % (3436364)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 75.81/11.30 % (3436364)CaDiCaL version: 2.1.3 % 75.81/11.30 % (3436364)Termination reason: Instruction limit % 75.81/11.30 % (3436364)Termination phase: Saturation % 75.81/11.30 % (3436364)Time elapsed: 0.835 s % 75.81/11.30 % (3436364)Peak memory usage: 121 MB % 75.81/11.30 % (3436364)Instructions burned: 1959 (million) % 75.81/11.30 % (3436373)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=3473989687:cond=fast:i=21173:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2935 on theBenchmark for (2935ds/21173Mi) % 75.81/11.30 % (3436373)Refutation not found, incomplete strategy % 75.81/11.30 % (3436373)------------------------------ % 75.81/11.30 % (3436373)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 75.81/11.30 % (3436373)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 75.81/11.30 % (3436373)CaDiCaL version: 2.1.3 % 75.81/11.30 % (3436373)Termination reason: Refutation not found, incomplete strategy % 75.81/11.30 % (3436373)Time elapsed: 0.026 s % 75.81/11.30 % (3436373)Peak memory usage: 112 MB % 75.81/11.30 % (3436373)Instructions burned: 6 (million) % 75.81/11.30 % (3436360)Instruction limit reached! % 75.81/11.30 % (3436360)------------------------------ % 75.81/11.30 % (3436360)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 75.81/11.30 % (3436360)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 75.81/11.30 % (3436360)CaDiCaL version: 2.1.3 % 75.81/11.30 % (3436360)Termination reason: Instruction limit % 75.81/11.30 % (3436360)Termination phase: Saturation % 75.81/11.30 % (3436360)Time elapsed: 1.392 s % 75.81/11.30 % (3436360)Peak memory usage: 91 MB % 75.81/11.30 % (3436360)Instructions burned: 3510 (million) % 75.81/11.30 % (3436368)Instruction limit reached! % 75.81/11.30 % (3436368)------------------------------ % 75.81/11.30 % (3436368)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 75.81/11.30 % (3436368)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 75.81/11.30 % (3436368)CaDiCaL version: 2.1.3 % 75.81/11.30 % (3436368)Termination reason: Instruction limit % 75.81/11.30 % (3436368)Termination phase: Saturation % 75.81/11.30 % (3436368)Time elapsed: 0.688 s % 75.81/11.30 % (3436368)Peak memory usage: 93 MB % 89.33/13.29 % (3436368)Instructions burned: 3202 (million) % 89.33/13.29 % (3436376)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=1475966115:avsq=on:i=1262:avsqr=1,16:rtra=on:rawr=on_2933 on theBenchmark for (2933ds/1262Mi) % 89.33/13.29 % (3436375)lrs+11_1_to=lpo:thi=all:sas=z3:si=on:fd=off:sac=on:slsq=on:random_seed=4105751817:avsq=on:i=10544:avsqr=17,4:canc=force:rtra=on:gtg=exists_top:er=filter_2933 on theBenchmark for (2933ds/10544Mi) % 89.33/13.29 % (3436373)------------------------------ % 89.33/13.29 % (3436373)------------------------------ % 89.33/13.29 % (3436379)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=3470553719:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2931 on theBenchmark for (2931ds/775Mi) % 89.33/13.29 % (3436379)Refutation not found, incomplete strategy % 89.33/13.29 % (3436379)------------------------------ % 89.33/13.29 % (3436379)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 89.33/13.29 % (3436379)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 89.33/13.29 % (3436379)CaDiCaL version: 2.1.3 % 89.33/13.29 % (3436379)Termination reason: Refutation not found, incomplete strategy % 89.33/13.29 % (3436379)Time elapsed: 0.002 s % 89.33/13.29 % (3436379)Peak memory usage: 88 MB % 89.33/13.29 % (3436379)Instructions burned: 3 (million) % 89.33/13.29 % (3436376)Instruction limit reached! % 89.33/13.29 % (3436376)------------------------------ % 89.33/13.29 % (3436376)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 89.33/13.29 % (3436376)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 89.33/13.29 % (3436376)CaDiCaL version: 2.1.3 % 89.33/13.29 % (3436376)Termination reason: Instruction limit % 89.33/13.29 % (3436376)Termination phase: Saturation % 89.33/13.29 % (3436376)Time elapsed: 0.359 s % 89.33/13.29 % (3436376)Peak memory usage: 122 MB % 89.33/13.29 % (3436376)Instructions burned: 1265 (million) % 89.33/13.29 % (3436381)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=630515515:i=270:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2928 on theBenchmark for (2928ds/270Mi) % 89.33/13.29 % (3436379)------------------------------ % 89.33/13.29 % (3436379)------------------------------ % 89.33/13.29 % (3436381)Instruction limit reached! % 89.33/13.29 % (3436381)------------------------------ % 89.33/13.29 % (3436381)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 89.33/13.29 % (3436381)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 89.33/13.29 % (3436381)CaDiCaL version: 2.1.3 % 89.33/13.29 % (3436381)Termination reason: Instruction limit % 89.33/13.29 % (3436381)Termination phase: Saturation % 89.33/13.29 % (3436381)Time elapsed: 0.083 s % 89.33/13.29 % (3436381)Peak memory usage: 92 MB % 89.33/13.29 % (3436381)Instructions burned: 273 (million) % 89.33/13.29 % (3436383)ott+10_128_isp=bottom:to=lpo:sil=128000:si=on:urr=on:uwa=alasca_main:sac=on:slsq=on:random_seed=3502532400:i=17165:aac=none:doe=on:rtra=on:gtg=exists_all_2927 on theBenchmark for (2927ds/17165Mi) % 89.33/13.29 % (3436351)Instruction limit reached! % 89.33/13.29 % (3436351)------------------------------ % 89.33/13.29 % (3436351)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 89.33/13.29 % (3436351)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 89.33/13.29 % (3436351)CaDiCaL version: 2.1.3 % 89.33/13.29 % (3436351)Termination reason: Instruction limit % 89.33/13.29 % (3436351)Termination phase: Saturation % 89.33/13.29 % (3436351)Time elapsed: 2.623 s % 89.33/13.29 % (3436351)Peak memory usage: 121 MB % 89.33/13.29 % (3436351)Instructions burned: 5811 (million) % 89.33/13.29 % (3436384)lrs+2_10_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_main:tha=some:random_seed=789793563:s2a=on:i=13094:s2at=-1:rtra=on_2927 on theBenchmark for (2927ds/13094Mi) % 89.33/13.29 % (3436386)lrs+10_1_to=lpo:sil=128000:si=on:sp=occurrence:random_seed=580896857:st=2:i=12633:rtra=on:ss=axioms_2926 on theBenchmark for (2926ds/12633Mi) % 89.33/13.29 % (3436386)Refutation not found, incomplete strategy % 89.33/13.29 % (3436386)------------------------------ % 89.33/13.29 % (3436386)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 89.33/13.29 % (3436386)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 89.33/13.29 % (3436386)CaDiCaL version: 2.1.3 % 89.33/13.29 % (3436386)Termination reason: Refutation not found, incomplete strategy % 89.33/13.29 % (3436386)Time elapsed: 0.002 s % 99.98/14.76 % (3436386)Peak memory usage: 88 MB % 99.98/14.76 % (3436386)Instructions burned: 3 (million) % 99.98/14.76 % (3436386)------------------------------ % 99.98/14.76 % (3436386)------------------------------ % 99.98/14.76 % (3436389)dis+1011_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_frequency:lsd=20:nwc=3:random_seed=1026583047:i=1783:rtra=on:gtg=position_2922 on theBenchmark for (2922ds/1783Mi) % 99.98/14.76 % (3436367)Instruction limit reached! % 99.98/14.76 % (3436367)------------------------------ % 99.98/14.76 % (3436367)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 99.98/14.76 % (3436367)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.98/14.76 % (3436367)CaDiCaL version: 2.1.3 % 99.98/14.76 % (3436367)Termination reason: Instruction limit % 99.98/14.76 % (3436367)Termination phase: Saturation % 99.98/14.76 % (3436367)Time elapsed: 2.137 s % 99.98/14.76 % (3436367)Peak memory usage: 109 MB % 99.98/14.76 % (3436367)Instructions burned: 3554 (million) % 99.98/14.76 % (3436391)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=3210376371:i=5451:aac=none:doe=on:nm=0:rtra=on:amm=off:gtg=position_2919 on theBenchmark for (2919ds/5451Mi) % 99.98/14.76 % (3436370)Instruction limit reached! % 99.98/14.76 % (3436370)------------------------------ % 99.98/14.76 % (3436370)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 99.98/14.76 % (3436370)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.98/14.76 % (3436370)CaDiCaL version: 2.1.3 % 99.98/14.76 % (3436370)Termination reason: Instruction limit % 99.98/14.76 % (3436370)Termination phase: Saturation % 99.98/14.76 % (3436370)Time elapsed: 2.282 s % 99.98/14.76 % (3436370)Peak memory usage: 146 MB % 99.98/14.76 % (3436370)Instructions burned: 4094 (million) % 99.98/14.76 % (3436393)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=1321813159:i=4975:doe=on:nm=0:rtra=on:gtg=exists_sym_2916 on theBenchmark for (2916ds/4975Mi) % 99.98/14.76 % (3436389)Instruction limit reached! % 99.98/14.76 % (3436389)------------------------------ % 99.98/14.76 % (3436389)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 99.98/14.76 % (3436389)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.98/14.76 % (3436389)CaDiCaL version: 2.1.3 % 99.98/14.76 % (3436389)Termination reason: Instruction limit % 99.98/14.76 % (3436389)Termination phase: Saturation % 99.98/14.76 % (3436389)Time elapsed: 1.006 s % 99.98/14.76 % (3436389)Peak memory usage: 121 MB % 99.98/14.76 % (3436389)Instructions burned: 1783 (million) % 99.98/14.76 % (3436395)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=1644212895:i=2076:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2910 on theBenchmark for (2910ds/2076Mi) % 99.98/14.76 % (3436395)Instruction limit reached! % 99.98/14.76 % (3436395)------------------------------ % 99.98/14.76 % (3436395)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 99.98/14.76 % (3436395)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.98/14.76 % (3436395)CaDiCaL version: 2.1.3 % 99.98/14.76 % (3436395)Termination reason: Instruction limit % 99.98/14.76 % (3436395)Termination phase: Saturation % 99.98/14.76 % (3436395)Time elapsed: 0.985 s % 99.98/14.76 % (3436395)Peak memory usage: 122 MB % 99.98/14.76 % (3436395)Instructions burned: 2078 (million) % 99.98/14.76 % (3436397)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=1110032183:i=5145:rtra=on_2899 on theBenchmark for (2899ds/5145Mi) % 99.98/14.76 % (3436384)Instruction limit reached! % 99.98/14.76 % (3436384)------------------------------ % 99.98/14.76 % (3436384)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 99.98/14.76 % (3436384)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.98/14.76 % (3436384)CaDiCaL version: 2.1.3 % 99.98/14.76 % (3436384)Termination reason: Instruction limit % 99.98/14.76 % (3436384)Termination phase: Saturation % 99.98/14.76 % (3436384)Time elapsed: 3.218 s % 99.98/14.76 % (3436384)Peak memory usage: 147 MB % 99.98/14.76 % (3436384)Instructions burned: 13098 (million) % 99.98/14.76 % (3436393)Instruction limit reached! % 99.98/14.76 % (3436393)------------------------------ % 99.98/14.76 % (3436393)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 99.98/14.76 % (3436393)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.31/27.79 % (3436393)CaDiCaL version: 2.1.3 % 192.31/27.79 % (3436393)Termination reason: Instruction limit % 192.31/27.79 % (3436393)Termination phase: Saturation % 192.31/27.79 % (3436393)Time elapsed: 2.151 s % 192.31/27.79 % (3436393)Peak memory usage: 122 MB % 192.31/27.79 % (3436393)Instructions burned: 4979 (million) % 192.31/27.79 % (3436399)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=1085845196:i=3509:rtra=on_2893 on theBenchmark for (2893ds/3509Mi) % 192.31/27.79 % (3436400)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=3943765995:st=2:i=13800:sd=12:ep=R:rtra=on:ss=axioms_2893 on theBenchmark for (2893ds/13800Mi) % 192.31/27.79 % (3436400)Refutation not found, incomplete strategy % 192.31/27.79 % (3436400)------------------------------ % 192.31/27.79 % (3436400)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 192.31/27.79 % (3436400)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.31/27.79 % (3436400)CaDiCaL version: 2.1.3 % 192.31/27.79 % (3436400)Termination reason: Refutation not found, incomplete strategy % 192.31/27.79 % (3436400)Time elapsed: 0.002 s % 192.31/27.79 % (3436400)Peak memory usage: 88 MB % 192.31/27.79 % (3436400)Instructions burned: 3 (million) % 192.31/27.79 % (3436391)Instruction limit reached! % 192.31/27.79 % (3436391)------------------------------ % 192.31/27.79 % (3436391)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 192.31/27.79 % (3436391)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.31/27.79 % (3436391)CaDiCaL version: 2.1.3 % 192.31/27.79 % (3436391)Termination reason: Instruction limit % 192.31/27.79 % (3436391)Termination phase: Saturation % 192.31/27.79 % (3436391)Time elapsed: 2.764 s % 192.31/27.79 % (3436391)Peak memory usage: 126 MB % 192.31/27.79 % (3436391)Instructions burned: 5452 (million) % 192.31/27.79 % (3436400)------------------------------ % 192.31/27.79 % (3436400)------------------------------ % 192.31/27.79 % (3436403)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=1825671043:i=1412:rtra=on:fsd=on:proc=on_2890 on theBenchmark for (2890ds/1412Mi) % 192.31/27.79 % (3436404)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 % 192.31/27.79 % (3436404)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=1287521497:i=11747:aac=none:nm=0:rtra=on:rawr=on_2889 on theBenchmark for (2889ds/11747Mi) % 192.31/27.79 % (3436399)Instruction limit reached! % 192.31/27.79 % (3436399)------------------------------ % 192.31/27.79 % (3436399)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 192.31/27.79 % (3436399)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.31/27.79 % (3436399)CaDiCaL version: 2.1.3 % 192.31/27.79 % (3436399)Termination reason: Instruction limit % 192.31/27.79 % (3436399)Termination phase: Saturation % 192.31/27.79 % (3436399)Time elapsed: 0.706 s % 192.31/27.79 % (3436399)Peak memory usage: 91 MB % 192.31/27.79 % (3436399)Instructions burned: 3514 (million) % 192.31/27.79 % (3436407)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=3674691536:s2a=on:i=3553:nm=0:rtra=on_2885 on theBenchmark for (2885ds/3553Mi) % 192.31/27.79 % (3436403)Instruction limit reached! % 192.31/27.79 % (3436403)------------------------------ % 192.31/27.79 % (3436403)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 192.31/27.79 % (3436403)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.31/27.79 % (3436403)CaDiCaL version: 2.1.3 % 192.31/27.79 % (3436403)Termination reason: Instruction limit % 192.31/27.79 % (3436403)Termination phase: Saturation % 192.31/27.79 % (3436403)Time elapsed: 0.730 s % 192.31/27.79 % (3436403)Peak memory usage: 120 MB % 192.31/27.79 % (3436403)Instructions burned: 1413 (million) % 192.31/27.79 % (3436409)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=2205012870:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2881 on theBenchmark for (2881ds/3201Mi) % 192.31/27.79 % (3436407)Instruction limit reached! % 192.31/27.79 % (3436407)------------------------------ % 192.31/27.79 % (3436407)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 192.31/27.79 % (3436407)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.31/27.79 % (3436407)CaDiCaL version: 2.1.3 % 192.31/27.79 % (3436407)Termination reason: Instruction limit % 192.31/27.79 % (3436407)Termination phase: Saturation % 224.93/32.35 % (3436407)Time elapsed: 1.135 s % 224.93/32.35 % (3436407)Peak memory usage: 108 MB % 224.93/32.35 % (3436407)Instructions burned: 3554 (million) % 224.93/32.35 % (3436375)Instruction limit reached! % 224.93/32.35 % (3436375)------------------------------ % 224.93/32.35 % (3436375)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 224.93/32.35 % (3436375)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 224.93/32.35 % (3436375)CaDiCaL version: 2.1.3 % 224.93/32.35 % (3436375)Termination reason: Instruction limit % 224.93/32.35 % (3436375)Termination phase: Saturation % 224.93/32.35 % (3436375)Time elapsed: 5.905 s % 224.93/32.35 % (3436375)Peak memory usage: 207 MB % 224.93/32.35 % (3436375)Instructions burned: 10545 (million) % 224.93/32.35 % (3436397)Instruction limit reached! % 224.93/32.35 % (3436397)------------------------------ % 224.93/32.35 % (3436397)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 224.93/32.35 % (3436397)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 224.93/32.35 % (3436397)CaDiCaL version: 2.1.3 % 224.93/32.35 % (3436397)Termination reason: Instruction limit % 224.93/32.35 % (3436397)Termination phase: Saturation % 224.93/32.35 % (3436397)Time elapsed: 2.536 s % 224.93/32.35 % (3436397)Peak memory usage: 128 MB % 224.93/32.35 % (3436397)Instructions burned: 5147 (million) % 224.93/32.35 % (3436411)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=1247491713:thitd=on:cond=on:i=4081:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2873 on theBenchmark for (2873ds/4081Mi) % 224.93/32.35 % (3436413)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=1630266499:cond=fast:i=20260:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2873 on theBenchmark for (2873ds/20260Mi) % 224.93/32.35 % (3436414)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=2413758397:s2a=on:i=58627:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2873 on theBenchmark for (2873ds/58627Mi) % 224.93/32.35 % (3436413)Refutation not found, incomplete strategy % 224.93/32.35 % (3436413)------------------------------ % 224.93/32.35 % (3436413)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 224.93/32.35 % (3436413)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 224.93/32.35 % (3436413)CaDiCaL version: 2.1.3 % 224.93/32.35 % (3436413)Termination reason: Refutation not found, incomplete strategy % 224.93/32.35 % (3436413)Time elapsed: 0.027 s % 224.93/32.35 % (3436413)Peak memory usage: 112 MB % 224.93/32.35 % (3436413)Instructions burned: 6 (million) % 224.93/32.35 % (3436413)------------------------------ % 224.93/32.35 % (3436413)------------------------------ % 224.93/32.35 % (3436496)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=4050673246:avsq=on:i=6258:avsqr=1,16:rtra=on:rawr=on_2869 on theBenchmark for (2869ds/6258Mi) % 224.93/32.35 % (3436409)Instruction limit reached! % 224.93/32.35 % (3436409)------------------------------ % 224.93/32.35 % (3436409)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 224.93/32.35 % (3436409)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 224.93/32.35 % (3436409)CaDiCaL version: 2.1.3 % 224.93/32.35 % (3436409)Termination reason: Instruction limit % 224.93/32.35 % (3436409)Termination phase: Saturation % 224.93/32.35 % (3436409)Time elapsed: 1.301 s % 224.93/32.35 % (3436409)Peak memory usage: 93 MB % 224.93/32.35 % (3436409)Instructions burned: 3203 (million) % 224.93/32.35 % (3436549)ott+10_128_isp=bottom:to=lpo:sil=128000:si=on:urr=on:uwa=alasca_main:sac=on:slsq=on:random_seed=1320343282:i=34001:aac=none:doe=on:rtra=on:gtg=exists_all_2867 on theBenchmark for (2867ds/34001Mi) % 224.93/32.35 % (3436411)Instruction limit reached! % 224.93/32.35 % (3436411)------------------------------ % 224.93/32.35 % (3436411)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 224.93/32.35 % (3436411)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 224.93/32.35 % (3436411)CaDiCaL version: 2.1.3 % 224.93/32.35 % (3436411)Termination reason: Instruction limit % 224.93/32.35 % (3436411)Termination phase: Saturation % 224.93/32.35 % (3436411)Time elapsed: 1.294 s % 224.93/32.35 % (3436411)Peak memory usage: 146 MB % 224.93/32.35 % (3436411)Instructions burned: 4084 (million) % 224.93/32.35 % (3436680)lrs+2_10_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_main:tha=some:random_seed=1251482309:s2a=on:i=71622:s2at=-1:rtra=on_2859 on theBenchmark for (2859ds/71622Mi) % 250.49/35.97 % (3436496)Instruction limit reached! % 250.49/35.97 % (3436496)------------------------------ % 250.49/35.97 % (3436496)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 250.49/35.97 % (3436496)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 250.49/35.97 % (3436496)CaDiCaL version: 2.1.3 % 250.49/35.97 % (3436496)Termination reason: Instruction limit % 250.49/35.97 % (3436496)Termination phase: Saturation % 250.49/35.97 % (3436496)Time elapsed: 2.865 s % 250.49/35.97 % (3436496)Peak memory usage: 123 MB % 250.49/35.97 % (3436496)Instructions burned: 6259 (million) % 250.49/35.97 % (3436682)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=1528858273:i=24001:kws=precedence:nm=0:rtra=on_2839 on theBenchmark for (2839ds/24001Mi) % 250.49/35.97 % (3436404)Instruction limit reached! % 250.49/35.97 % (3436404)------------------------------ % 250.49/35.97 % (3436404)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 250.49/35.97 % (3436404)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 250.49/35.97 % (3436404)CaDiCaL version: 2.1.3 % 250.49/35.97 % (3436404)Termination reason: Instruction limit % 250.49/35.97 % (3436404)Termination phase: Saturation % 250.49/35.97 % (3436404)Time elapsed: 5.115 s % 250.49/35.97 % (3436404)Peak memory usage: 123 MB % 250.49/35.97 % (3436404)Instructions burned: 11748 (million) % 250.49/35.97 % (3436684)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=861499834:i=2076:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2837 on theBenchmark for (2837ds/2076Mi) % 250.49/35.97 % (3436383)Instruction limit reached! % 250.49/35.97 % (3436383)------------------------------ % 250.49/35.97 % (3436383)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 250.49/35.97 % (3436383)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 250.49/35.97 % (3436383)CaDiCaL version: 2.1.3 % 250.49/35.97 % (3436383)Termination reason: Instruction limit % 250.49/35.97 % (3436383)Termination phase: Saturation % 250.49/35.97 % (3436383)Time elapsed: 9.709 s % 250.49/35.97 % (3436383)Peak memory usage: 205 MB % 250.49/35.97 % (3436383)Instructions burned: 17167 (million) % 250.49/35.97 % (3436686)dis+21_20_to=lakbo:si=on:alasca=on:sp=const_max:uwa=alasca_main:sac=on:random_seed=977966565:s2a=on:i=83971:s2at=4:bd=all:ins=1:rtra=on_2829 on theBenchmark for (2829ds/83971Mi) % 250.49/35.97 % (3436684)Instruction limit reached! % 250.49/35.97 % (3436684)------------------------------ % 250.49/35.97 % (3436684)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 250.49/35.97 % (3436684)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 250.49/35.97 % (3436684)CaDiCaL version: 2.1.3 % 250.49/35.97 % (3436684)Termination reason: Instruction limit % 250.49/35.97 % (3436684)Termination phase: Saturation % 250.49/35.97 % (3436684)Time elapsed: 0.980 s % 250.49/35.97 % (3436684)Peak memory usage: 122 MB % 250.49/35.97 % (3436684)Instructions burned: 2076 (million) % 250.49/35.97 % (3436688)lrs+1011_5:1_to=lpo:sil=128000:sas=z3:si=on:norm_ineq=on:tha=some:random_seed=2853551192:i=83944:rtra=on_2826 on theBenchmark for (2826ds/83944Mi) % 250.49/35.97 % (3436344)Instruction limit reached! % 250.49/35.97 % (3436344)------------------------------ % 250.49/35.97 % (3436344)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 250.49/35.97 % (3436344)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 250.49/35.97 % (3436344)CaDiCaL version: 2.1.3 % 250.49/35.97 % (3436344)Termination reason: Instruction limit % 250.49/35.97 % (3436344)Termination phase: Saturation % 250.49/35.97 % (3436344)Time elapsed: 20.640 s % 250.49/35.97 % (3436344)Peak memory usage: 250 MB % 250.49/35.97 % (3436344)Instructions burned: 36817 (million) % 250.49/35.97 % (3436690)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=750973681:i=9201:rtra=on_2750 on theBenchmark for (2750ds/9201Mi) % 250.49/35.97 % (3436682)Instruction limit reached! % 250.49/35.97 % (3436682)------------------------------ % 250.49/35.97 % (3436682)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 250.49/35.97 % (3436682)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 250.49/35.97 % (3436682)CaDiCaL version: 2.1.3 % 250.49/35.97 % (3436682)Termination reason: Instruction limit % 250.49/35.97 % (3436682)Termination phase: Saturation % 250.49/35.97 % (3436682)Time elapsed: 10.810 s % 250.49/35.97 % (3436682)Peak memory usage: 126 MB % 250.49/35.97 % (3436682)Instructions burned: 24003 (million) % 250.49/35.97 % (3436692)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 % 260.40/37.36 % (3436692)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=2096308268:i=6806:aac=none:nm=0:rtra=on:rawr=on_2729 on theBenchmark for (2729ds/6806Mi) % 260.40/37.36 % (3436690)Instruction limit reached! % 260.40/37.36 % (3436690)------------------------------ % 260.40/37.36 % (3436690)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 260.40/37.36 % (3436690)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 260.40/37.36 % (3436690)CaDiCaL version: 2.1.3 % 260.40/37.36 % (3436690)Termination reason: Instruction limit % 260.40/37.36 % (3436690)Termination phase: Saturation % 260.40/37.36 % (3436690)Time elapsed: 3.532 s % 260.40/37.36 % (3436690)Peak memory usage: 92 MB % 260.40/37.36 % (3436690)Instructions burned: 9201 (million) % 260.40/37.36 % (3436694)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=2662384021:s2a=on:i=3553:nm=0:rtra=on_2713 on theBenchmark for (2713ds/3553Mi) % 260.40/37.36 % (3436692)Instruction limit reached! % 260.40/37.36 % (3436692)------------------------------ % 260.40/37.36 % (3436692)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 260.40/37.36 % (3436692)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 260.40/37.36 % (3436692)CaDiCaL version: 2.1.3 % 260.40/37.36 % (3436692)Termination reason: Instruction limit % 260.40/37.36 % (3436692)Termination phase: Saturation % 260.40/37.36 % (3436692)Time elapsed: 3.021 s % 260.40/37.36 % (3436692)Peak memory usage: 122 MB % 260.40/37.36 % (3436692)Instructions burned: 6807 (million) % 260.40/37.36 % (3436696)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=4258692026:thitd=on:cond=on:i=2064:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2698 on theBenchmark for (2698ds/2064Mi) % 260.40/37.36 % (3436694)Instruction limit reached! % 260.40/37.36 % (3436694)------------------------------ % 260.40/37.36 % (3436694)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 260.40/37.36 % (3436694)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 260.40/37.36 % (3436694)CaDiCaL version: 2.1.3 % 260.40/37.36 % (3436694)Termination reason: Instruction limit % 260.40/37.36 % (3436694)Termination phase: Saturation % 260.40/37.36 % (3436694)Time elapsed: 2.125 s % 260.40/37.36 % (3436694)Peak memory usage: 109 MB % 260.40/37.36 % (3436694)Instructions burned: 3554 (million) % 260.40/37.36 % (3436698)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=2201868187:cond=fast:i=20260:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2690 on theBenchmark for (2690ds/20260Mi) % 260.40/37.36 % (3436698)Refutation not found, incomplete strategy % 260.40/37.36 % (3436698)------------------------------ % 260.40/37.36 % (3436698)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 260.40/37.36 % (3436698)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 260.40/37.36 % (3436698)CaDiCaL version: 2.1.3 % 260.40/37.36 % (3436698)Termination reason: Refutation not found, incomplete strategy % 260.40/37.36 % (3436698)Time elapsed: 0.026 s % 260.40/37.36 % (3436698)Peak memory usage: 112 MB % 260.40/37.36 % (3436698)Instructions burned: 6 (million) % 260.40/37.36 % (3436698)------------------------------ % 260.40/37.36 % (3436698)------------------------------ % 260.40/37.36 % (3436700)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=3917908111:avsq=on:i=1244:avsqr=1,16:rtra=on:rawr=on_2687 on theBenchmark for (2687ds/1244Mi) % 260.40/37.36 % (3436696)Instruction limit reached! % 260.40/37.36 % (3436696)------------------------------ % 260.40/37.36 % (3436696)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 260.40/37.36 % (3436696)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 260.40/37.36 % (3436696)CaDiCaL version: 2.1.3 % 260.40/37.36 % (3436696)Termination reason: Instruction limit % 260.40/37.36 % (3436696)Termination phase: Saturation % 260.40/37.36 % (3436696)Time elapsed: 1.257 s % 260.40/37.36 % (3436696)Peak memory usage: 142 MB % 260.40/37.36 % (3436696)Instructions burned: 2064 (million) % 260.40/37.36 % (3436702)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=3465073587:i=58261:doe=on:nm=0:rtra=on:gtg=exists_sym_2684 on theBenchmark for (2684ds/58261Mi) % 268.89/38.59 % (3436700)Instruction limit reached! % 268.89/38.59 % (3436700)------------------------------ % 268.89/38.59 % (3436700)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 268.89/38.59 % (3436700)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 268.89/38.59 % (3436700)CaDiCaL version: 2.1.3 % 268.89/38.59 % (3436700)Termination reason: Instruction limit % 268.89/38.59 % (3436700)Termination phase: Saturation % 268.89/38.59 % (3436700)Time elapsed: 0.641 s % 268.89/38.59 % (3436700)Peak memory usage: 120 MB % 268.89/38.59 % (3436700)Instructions burned: 1245 (million) % 268.89/38.59 % (3436704)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 % 268.89/38.59 % (3436704)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=849860491:i=6806:aac=none:nm=0:rtra=on:rawr=on_2679 on theBenchmark for (2679ds/6806Mi) % 268.89/38.59 % (3436549)Instruction limit reached! % 268.89/38.59 % (3436549)------------------------------ % 268.89/38.59 % (3436549)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 268.89/38.59 % (3436549)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 268.89/38.59 % (3436549)CaDiCaL version: 2.1.3 % 268.89/38.59 % (3436549)Termination reason: Instruction limit % 268.89/38.59 % (3436549)Termination phase: Saturation % 268.89/38.59 % (3436549)Time elapsed: 19.485 s % 268.89/38.59 % (3436549)Peak memory usage: 586 MB % 268.89/38.59 % (3436549)Instructions burned: 34001 (million) % 268.89/38.59 % (3436707)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=810523080:thitd=on:cond=on:i=4081:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2670 on theBenchmark for (2670ds/4081Mi) % 268.89/38.59 % (3436680)Instruction limit reached! % 268.89/38.59 % (3436680)------------------------------ % 268.89/38.59 % (3436680)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 268.89/38.59 % (3436680)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 268.89/38.59 % (3436680)CaDiCaL version: 2.1.3 % 268.89/38.59 % (3436680)Termination reason: Instruction limit % 268.89/38.59 % (3436680)Termination phase: Saturation % 268.89/38.59 % (3436680)Time elapsed: 19.393 s % 268.89/38.59 % (3436680)Peak memory usage: 353 MB % 268.89/38.59 % (3436680)Instructions burned: 71623 (million) % 268.89/38.59 % (3436709)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=1749449508:avsq=on:i=1701:avsqr=1,16:rtra=on:rawr=on_2664 on theBenchmark for (2664ds/1701Mi) % 268.89/38.59 % (3436709)Instruction limit reached! % 268.89/38.59 % (3436709)------------------------------ % 268.89/38.59 % (3436709)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 268.89/38.59 % (3436709)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 268.89/38.59 % (3436709)CaDiCaL version: 2.1.3 % 268.89/38.59 % (3436709)Termination reason: Instruction limit % 268.89/38.59 % (3436709)Termination phase: Saturation % 268.89/38.59 % (3436709)Time elapsed: 0.453 s % 268.89/38.59 % (3436709)Peak memory usage: 121 MB % 268.89/38.59 % (3436709)Instructions burned: 1702 (million) % 268.89/38.59 % (3436711)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=2212375010:i=57001:doe=on:nm=0:rtra=on:gtg=exists_sym_2659 on theBenchmark for (2659ds/57001Mi) % 268.89/38.59 % (3436704)Instruction limit reached! % 268.89/38.59 % (3436704)------------------------------ % 268.89/38.59 % (3436704)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 268.89/38.59 % (3436704)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 268.89/38.59 % (3436704)CaDiCaL version: 2.1.3 % 268.89/38.59 % (3436704)Termination reason: Instruction limit % 268.89/38.59 % (3436704)Termination phase: Saturation % 268.89/38.59 % (3436704)Time elapsed: 2.969 s % 268.89/38.59 % (3436704)Peak memory usage: 124 MB % 268.89/38.59 % (3436704)Instructions burned: 6807 (million) % 268.89/38.59 % (3436713)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 % 268.89/38.59 % (3436713)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=4143757475:i=8622:aac=none:nm=0:rtra=on:rawr=on_2648 on theBenchmark for (2648ds/8622Mi) % 278.00/39.81 % (3436707)Instruction limit reached! % 278.00/39.81 % (3436707)------------------------------ % 278.00/39.81 % (3436707)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 278.00/39.81 % (3436707)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 278.00/39.81 % (3436707)CaDiCaL version: 2.1.3 % 278.00/39.81 % (3436707)Termination reason: Instruction limit % 278.00/39.81 % (3436707)Termination phase: Saturation % 278.00/39.81 % (3436707)Time elapsed: 2.287 s % 278.00/39.81 % (3436707)Peak memory usage: 145 MB % 278.00/39.81 % (3436707)Instructions burned: 4081 (million) % 278.00/39.81 % (3436715)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=3712747262:i=24:doe=on:rtra=on:gtg=exists_top:ss=axioms_2646 on theBenchmark for (2646ds/24Mi) % 278.00/39.81 % (3436715)Instruction limit reached! % 278.00/39.81 % (3436715)------------------------------ % 278.00/39.81 % (3436715)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 278.00/39.81 % (3436715)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 278.00/39.81 % (3436715)CaDiCaL version: 2.1.3 % 278.00/39.81 % (3436715)Termination reason: Instruction limit % 278.00/39.81 % (3436715)Termination phase: Saturation % 278.00/39.81 % (3436715)Time elapsed: 0.036 s % 278.00/39.81 % (3436715)Peak memory usage: 118 MB % 278.00/39.81 % (3436715)Instructions burned: 24 (million) % 278.00/39.81 % (3436717)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=2004050318:i=614:kws=precedence:nm=0:rtra=on_2644 on theBenchmark for (2644ds/614Mi) % 278.00/39.81 % (3436717)Instruction limit reached! % 278.00/39.81 % (3436717)------------------------------ % 278.00/39.81 % (3436717)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 278.00/39.81 % (3436717)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 278.00/39.81 % (3436717)CaDiCaL version: 2.1.3 % 278.00/39.81 % (3436717)Termination reason: Instruction limit % 278.00/39.81 % (3436717)Termination phase: Saturation % 278.00/39.81 % (3436717)Time elapsed: 0.350 s % 278.00/39.81 % (3436717)Peak memory usage: 120 MB % 278.00/39.81 % (3436717)Instructions burned: 614 (million) % 278.00/39.81 % (3436719)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=1362836484:i=402:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2639 on theBenchmark for (2639ds/402Mi) % 278.00/39.81 % (3436719)Instruction limit reached! % 278.00/39.81 % (3436719)------------------------------ % 278.00/39.81 % (3436719)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 278.00/39.81 % (3436719)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 278.00/39.81 % (3436719)CaDiCaL version: 2.1.3 % 278.00/39.81 % (3436719)Termination reason: Instruction limit % 278.00/39.81 % (3436719)Termination phase: Saturation % 278.00/39.81 % (3436719)Time elapsed: 0.273 s % 278.00/39.81 % (3436719)Peak memory usage: 119 MB % 278.00/39.81 % (3436719)Instructions burned: 403 (million) % 278.00/39.81 % (3436721)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=3485199880:s2a=on:i=14:rtra=on:inst=on_2635 on theBenchmark for (2635ds/14Mi) % 278.00/39.81 % (3436721)Instruction limit reached! % 278.00/39.81 % (3436721)------------------------------ % 278.00/39.81 % (3436721)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 278.00/39.81 % (3436721)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 278.00/39.81 % (3436721)CaDiCaL version: 2.1.3 % 278.00/39.81 % (3436721)Termination reason: Instruction limit % 278.00/39.81 % (3436721)Termination phase: Saturation % 278.00/39.81 % (3436721)Time elapsed: 0.008 s % 278.00/39.81 % (3436721)Peak memory usage: 89 MB % 278.00/39.81 % (3436721)Instructions burned: 14 (million) % 278.00/39.81 % (3436723)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=1195703068:i=8:rtra=on_2634 on theBenchmark for (2634ds/8Mi) % 278.00/39.81 % (3436723)Instruction limit reached! % 278.00/39.81 % (3436723)------------------------------ % 278.00/39.81 % (3436723)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 278.00/39.81 % (3436723)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 278.00/39.81 % (3436723)CaDiCaL version: 2.1.3 % 278.00/39.81 % (3436723)Termination reason: Instruction limit % 278.00/39.81 % (3436723)Termination phase: Saturation % 278.00/39.81 % (3436723)Time elapsed: 0.005 s % 278.00/39.81 % (3436723)Peak memory usage: 89 MB % 278.00/39.81 % (3436723)Instructions burned: 8 (million) % 282.84/40.54 % (3436725)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=4289603636:i=92:rtra=on_2632 on theBenchmark for (2632ds/92Mi) % 282.84/40.54 % (3436725)Instruction limit reached! % 282.84/40.54 % (3436725)------------------------------ % 282.84/40.54 % (3436725)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 282.84/40.54 % (3436725)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.84/40.54 % (3436725)CaDiCaL version: 2.1.3 % 282.84/40.54 % (3436725)Termination reason: Instruction limit % 282.84/40.54 % (3436725)Termination phase: Saturation % 282.84/40.54 % (3436725)Time elapsed: 0.075 s % 282.84/40.54 % (3436725)Peak memory usage: 118 MB % 282.84/40.54 % (3436725)Instructions burned: 92 (million) % 282.84/40.54 % (3436727)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=472836839:i=66:rtra=on_2630 on theBenchmark for (2630ds/66Mi) % 282.84/40.54 % (3436727)Instruction limit reached! % 282.84/40.54 % (3436727)------------------------------ % 282.84/40.54 % (3436727)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 282.84/40.54 % (3436727)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.84/40.54 % (3436727)CaDiCaL version: 2.1.3 % 282.84/40.54 % (3436727)Termination reason: Instruction limit % 282.84/40.54 % (3436727)Termination phase: Saturation % 282.84/40.54 % (3436727)Time elapsed: 0.067 s % 282.84/40.54 % (3436727)Peak memory usage: 119 MB % 282.84/40.54 % (3436727)Instructions burned: 67 (million) % 282.84/40.54 % (3436729)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=2015805953:st=5:i=28:sd=10:rtra=on:ss=axioms:rawr=on_2628 on theBenchmark for (2628ds/28Mi) % 282.84/40.54 % (3436729)Refutation not found, incomplete strategy % 282.84/40.54 % (3436729)------------------------------ % 282.84/40.54 % (3436729)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 282.84/40.54 % (3436729)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.84/40.54 % (3436729)CaDiCaL version: 2.1.3 % 282.84/40.54 % (3436729)Termination reason: Refutation not found, incomplete strategy % 282.84/40.54 % (3436729)Time elapsed: 0.002 s % 282.84/40.54 % (3436729)Peak memory usage: 88 MB % 282.84/40.54 % (3436729)Instructions burned: 1 (million) % 282.84/40.54 % (3436729)------------------------------ % 282.84/40.54 % (3436729)------------------------------ % 282.84/40.54 % (3436731)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=2484079884:i=58:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2625 on theBenchmark for (2625ds/58Mi) % 282.84/40.54 % (3436731)Instruction limit reached! % 282.84/40.54 % (3436731)------------------------------ % 282.84/40.54 % (3436731)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 282.84/40.54 % (3436731)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.84/40.54 % (3436731)CaDiCaL version: 2.1.3 % 282.84/40.54 % (3436731)Termination reason: Instruction limit % 282.84/40.54 % (3436731)Termination phase: Saturation % 282.84/40.54 % (3436731)Time elapsed: 0.036 s % 282.84/40.54 % (3436731)Peak memory usage: 89 MB % 282.84/40.54 % (3436731)Instructions burned: 59 (million) % 282.84/40.54 % (3436733)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=1277143831:cond=on:i=32:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2623 on theBenchmark for (2623ds/32Mi) % 282.84/40.54 % (3436733)Instruction limit reached! % 282.84/40.54 % (3436733)------------------------------ % 282.84/40.54 % (3436733)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 282.84/40.54 % (3436733)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.84/40.54 % (3436733)CaDiCaL version: 2.1.3 % 282.84/40.54 % (3436733)Termination reason: Instruction limit % 282.84/40.54 % (3436733)Termination phase: Saturation % 282.84/40.54 % (3436733)Time elapsed: 0.017 s % 282.84/40.54 % (3436733)Peak memory usage: 90 MB % 282.84/40.54 % (3436733)Instructions burned: 33 (million) % 282.84/40.54 % (3436735)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=1623278026:i=48:canc=force:rtra=on_2622 on theBenchmark for (2622ds/48Mi) % 282.84/40.54 % (3436735)Instruction limit reached! % 282.84/40.54 % (3436735)------------------------------ % 282.84/40.54 % (3436735)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 282.84/40.54 % (3436735)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.84/40.54 % (3436735)CaDiCaL version: 2.1.3 % 282.84/40.54 % (3436735)Termination reason: Instruction limit % 282.84/40.54 % (3436735)Termination phase: Saturation % 286.93/41.04 % (3436735)Time elapsed: 0.034 s % 286.93/41.04 % (3436735)Peak memory usage: 90 MB % 286.93/41.04 % (3436735)Instructions burned: 49 (million) % 286.93/41.04 % (3436737)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=4081836852:i=54:canc=cautious:fsr=off:rtra=on_2620 on theBenchmark for (2620ds/54Mi) % 286.93/41.04 % (3436737)Refutation not found, incomplete strategy % 286.93/41.04 % (3436737)------------------------------ % 286.93/41.04 % (3436737)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 286.93/41.04 % (3436737)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 286.93/41.04 % (3436737)CaDiCaL version: 2.1.3 % 286.93/41.04 % (3436737)Termination reason: Refutation not found, incomplete strategy % 286.93/41.04 % (3436737)Time elapsed: 0.006 s % 286.93/41.04 % (3436737)Peak memory usage: 89 MB % 286.93/41.04 % (3436737)Instructions burned: 9 (million) % 286.93/41.04 % (3436737)------------------------------ % 286.93/41.04 % (3436737)------------------------------ % 286.93/41.04 % (3436739)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=865254163:i=170:gtgl=4:rtra=on:gtg=exists_sym_2616 on theBenchmark for (2616ds/170Mi) % 286.93/41.04 % (3436739)Instruction limit reached! % 286.93/41.04 % (3436739)------------------------------ % 286.93/41.04 % (3436739)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 286.93/41.04 % (3436739)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 286.93/41.04 % (3436739)CaDiCaL version: 2.1.3 % 286.93/41.04 % (3436739)Termination reason: Instruction limit % 286.93/41.04 % (3436739)Termination phase: Saturation % 286.93/41.04 % (3436739)Time elapsed: 0.102 s % 286.93/41.04 % (3436739)Peak memory usage: 90 MB % 286.93/41.04 % (3436739)Instructions burned: 172 (million) % 286.93/41.04 % (3436741)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=341974286:i=4:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2614 on theBenchmark for (2614ds/4Mi) % 286.93/41.04 % (3436741)Instruction limit reached! % 286.93/41.04 % (3436741)------------------------------ % 286.93/41.04 % (3436741)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 286.93/41.04 % (3436741)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 286.93/41.04 % (3436741)CaDiCaL version: 2.1.3 % 286.93/41.04 % (3436741)Termination reason: Instruction limit % 286.93/41.04 % (3436741)Termination phase: Function definition elimination % 286.93/41.04 % (3436741)Time elapsed: 0.003 s % 286.93/41.04 % (3436741)Peak memory usage: 86 MB % 286.93/41.04 % (3436741)Instructions burned: 5 (million) % 286.93/41.04 % (3436743)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=1874555327:i=362:rtra=on:ss=axioms:ev=cautious_2613 on theBenchmark for (2613ds/362Mi) % 286.93/41.04 % (3436743)Refutation not found, incomplete strategy % 286.93/41.04 % (3436743)------------------------------ % 286.93/41.04 % (3436743)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 286.93/41.04 % (3436743)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 286.93/41.04 % (3436743)CaDiCaL version: 2.1.3 % 286.93/41.04 % (3436743)Termination reason: Refutation not found, incomplete strategy % 286.93/41.04 % (3436743)Time elapsed: 0.001 s % 286.93/41.04 % (3436743)Peak memory usage: 87 MB % 286.93/41.04 % (3436743)Instructions burned: 1 (million) % 286.93/41.04 % (3436743)------------------------------ % 286.93/41.04 % (3436743)------------------------------ % 286.93/41.04 % (3436713)Instruction limit reached! % 286.93/41.04 % (3436713)------------------------------ % 286.93/41.04 % (3436713)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 286.93/41.04 % (3436713)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 286.93/41.04 % (3436713)CaDiCaL version: 2.1.3 % 286.93/41.04 % (3436713)Termination reason: Instruction limit % 286.93/41.04 % (3436713)Termination phase: Saturation % 286.93/41.04 % (3436713)Time elapsed: 3.732 s % 286.93/41.04 % (3436713)Peak memory usage: 123 MB % 286.93/41.04 % (3436713)Instructions burned: 8623 (million) % 286.93/41.04 % (3436745)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=3766797045:i=8:ep=RST:ins=2:rtra=on_2609 on theBenchmark for (2609ds/8Mi) % 286.93/41.04 % (3436745)Instruction limit reached! % 286.93/41.04 % (3436745)------------------------------ % 286.93/41.04 % (3436745)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 286.93/41.04 % (3436745)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 286.93/41.04 % (3436745)CaDiCaL version: 2.1.3 % 291.94/41.82 % (3436745)Termination reason: Instruction limit % 291.94/41.82 % (3436745)Termination phase: Saturation % 291.94/41.82 % (3436745)Time elapsed: 0.005 s % 291.94/41.82 % (3436745)Peak memory usage: 88 MB % 291.94/41.82 % (3436745)Instructions burned: 8 (million) % 291.94/41.82 % (3436746)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=4245912062:i=132:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2609 on theBenchmark for (2609ds/132Mi) % 291.94/41.82 % (3436748)lrs+10_1_thi=all:si=on:fd=off:random_seed=1750301665:i=106:rtra=on:gtg=all_2608 on theBenchmark for (2608ds/106Mi) % 291.94/41.82 % (3436746)Instruction limit reached! % 291.94/41.82 % (3436746)------------------------------ % 291.94/41.82 % (3436746)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 291.94/41.82 % (3436746)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 291.94/41.82 % (3436746)CaDiCaL version: 2.1.3 % 291.94/41.82 % (3436746)Termination reason: Instruction limit % 291.94/41.82 % (3436746)Termination phase: Saturation % 291.94/41.82 % (3436746)Time elapsed: 0.131 s % 291.94/41.82 % (3436746)Peak memory usage: 137 MB % 291.94/41.82 % (3436746)Instructions burned: 132 (million) % 291.94/41.82 % (3436748)Instruction limit reached! % 291.94/41.82 % (3436748)------------------------------ % 291.94/41.82 % (3436748)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 291.94/41.82 % (3436748)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 291.94/41.82 % (3436748)CaDiCaL version: 2.1.3 % 291.94/41.82 % (3436748)Termination reason: Instruction limit % 291.94/41.82 % (3436748)Termination phase: Saturation % 291.94/41.82 % (3436748)Time elapsed: 0.092 s % 291.94/41.82 % (3436748)Peak memory usage: 117 MB % 291.94/41.82 % (3436748)Instructions burned: 107 (million) % 291.94/41.82 % (3436751)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=3513490813:i=16:ep=RST:nm=16:rtra=on:gtg=exists_top_2606 on theBenchmark for (2606ds/16Mi) % 291.94/41.82 % (3436751)Instruction limit reached! % 291.94/41.82 % (3436751)------------------------------ % 291.94/41.82 % (3436751)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 291.94/41.82 % (3436751)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 291.94/41.82 % (3436751)CaDiCaL version: 2.1.3 % 291.94/41.82 % (3436751)Termination reason: Instruction limit % 291.94/41.82 % (3436751)Termination phase: Saturation % 291.94/41.82 % (3436751)Time elapsed: 0.010 s % 291.94/41.82 % (3436751)Peak memory usage: 89 MB % 291.94/41.82 % (3436751)Instructions burned: 17 (million) % 291.94/41.82 % (3436752)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=3766652526:st=3:i=4:rtra=on:ss=axioms_2606 on theBenchmark for (2606ds/4Mi) % 291.94/41.82 % (3436752)Refutation not found, incomplete strategy % 291.94/41.82 % (3436752)------------------------------ % 291.94/41.82 % (3436752)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 291.94/41.82 % (3436752)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 291.94/41.82 % (3436752)CaDiCaL version: 2.1.3 % 291.94/41.82 % (3436752)Termination reason: Refutation not found, incomplete strategy % 291.94/41.82 % (3436752)Time elapsed: 0.002 s % 291.94/41.82 % (3436752)Peak memory usage: 88 MB % 291.94/41.82 % (3436752)Instructions burned: 1 (million) % 291.94/41.82 % (3436754)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=3045743325:i=4:doe=on:canc=force:asg=cautious:rtra=on_2605 on theBenchmark for (2605ds/4Mi) % 291.94/41.82 % (3436754)Instruction limit reached! % 291.94/41.82 % (3436754)------------------------------ % 291.94/41.82 % (3436754)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 291.94/41.82 % (3436754)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 291.94/41.82 % (3436754)CaDiCaL version: 2.1.3 % 291.94/41.82 % (3436754)Termination reason: Instruction limit % 291.94/41.82 % (3436754)Termination phase: Function definition elimination % 291.94/41.82 % (3436754)Time elapsed: 0.003 s % 291.94/41.82 % (3436754)Peak memory usage: 86 MB % 291.94/41.82 % (3436754)Instructions burned: 5 (million) % 291.94/41.82 % (3436752)------------------------------ % 291.94/41.82 % (3436752)------------------------------ % 291.94/41.82 % (3436757)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=3933018068:i=254:doe=on:rtra=on_2603 on theBenchmark for (2603ds/254Mi) % 291.94/41.82 % (3436758)dis+10_1_si=on:random_seed=2870595804:i=20:ep=R:rtra=on_2602 on theBenchmark for (2602ds/20Mi) % 291.94/41.82 % (3436758)Instruction limit reachTerminated %------------------------------------------------------------------------------