%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWW590_2 : TPTP v9.3.1. Released v6.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % Computer : n016.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:30:52 PM UTC 2026 % Result : Timeout 296.57s 42.24s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWW590_2 : TPTP v9.3.1. Released v6.1.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.09/0.18 % Computer : n016.cluster.edu % 0.09/0.18 % Model : x86_64 x86_64 % 0.09/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.18 % Memory : 8046.5625MB % 0.09/0.18 % OS : Linux 6.8.0-71-generic % 0.09/0.18 % CPULimit : 300 % 0.09/0.18 % WCLimit : 300 % 0.09/0.18 % DateTime : Mon Sep 28 14:26:03 UTC 2026 % 0.09/0.19 % CPUTime : % 0.09/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.09/0.22 Running first-order theorem proving % 0.09/0.22 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 2.92/0.91 % (3656520)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule. % 2.92/0.91 % (3656530)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=568720135:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi) % 2.92/0.91 % (3656531)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=2800467331:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi) % 2.92/0.91 % (3656529)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=2772181250:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi) % 2.92/0.91 % (3656525)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=2462587521:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi) % 2.92/0.91 % (3656526)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=2697707982:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi) % 2.92/0.91 % (3656528)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=609906101:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi) % 2.92/0.91 % (3656527)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=3694454820:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi) % 2.92/0.91 % (3656529)Instruction limit reached! % 2.92/0.91 % (3656529)------------------------------ % 2.92/0.91 % (3656529)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 2.92/0.91 % (3656529)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.92/0.91 % (3656529)CaDiCaL version: 2.1.3 % 2.92/0.91 % (3656529)Termination reason: Instruction limit % 2.92/0.91 % (3656529)Termination phase: Saturation % 2.92/0.91 % (3656529)Time elapsed: 0.003 s % 2.92/0.91 % (3656529)Peak memory usage: 87 MB % 2.92/0.91 % (3656529)Instructions burned: 4 (million) % 2.92/0.91 % (3656530)Instruction limit reached! % 2.92/0.91 % (3656530)------------------------------ % 2.92/0.91 % (3656530)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 2.92/0.91 % (3656530)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.92/0.91 % (3656530)CaDiCaL version: 2.1.3 % 2.92/0.91 % (3656530)Termination reason: Instruction limit % 2.92/0.91 % (3656530)Termination phase: Saturation % 2.92/0.91 % (3656530)Time elapsed: 0.032 s % 2.92/0.91 % (3656530)Peak memory usage: 116 MB % 2.92/0.91 % (3656530)Instructions burned: 48 (million) % 2.92/0.91 % (3656528)Instruction limit reached! % 2.92/0.91 % (3656528)------------------------------ % 2.92/0.91 % (3656528)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 2.92/0.91 % (3656528)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.92/0.91 % (3656528)CaDiCaL version: 2.1.3 % 2.92/0.91 % (3656528)Termination reason: Instruction limit % 2.92/0.91 % (3656528)Termination phase: Saturation % 2.92/0.91 % (3656528)Time elapsed: 0.005 s % 2.92/0.91 % (3656528)Peak memory usage: 88 MB % 2.92/0.91 % (3656528)Instructions burned: 7 (million) % 2.92/0.91 % (3656525)Instruction limit reached! % 2.92/0.91 % (3656525)------------------------------ % 2.92/0.91 % (3656525)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 2.92/0.91 % (3656525)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.92/0.91 % (3656525)CaDiCaL version: 2.1.3 % 2.92/0.91 % (3656525)Termination reason: Instruction limit % 2.92/0.91 % (3656525)Termination phase: Saturation % 2.92/0.91 % (3656525)Time elapsed: 0.030 s % 2.92/0.91 % (3656525)Peak memory usage: 115 MB % 2.92/0.91 % (3656525)Instructions burned: 13 (million) % 2.92/0.91 % (3656531)Instruction limit reached! % 2.92/0.91 % (3656531)------------------------------ % 2.92/0.91 % (3656531)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 2.92/0.91 % (3656531)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.92/0.91 % (3656531)CaDiCaL version: 2.1.3 % 2.92/0.91 % (3656531)Termination reason: Instruction limit % 2.92/0.91 % (3656531)Termination phase: Saturation % 2.92/0.91 % (3656531)Time elapsed: 0.046 s % 2.92/0.91 % (3656531)Peak memory usage: 116 MB % 2.92/0.91 % (3656531)Instructions burned: 33 (million) % 2.92/0.91 % (3656541)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=2449700162:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/16Mi) % 2.92/0.91 % (3656541)Instruction limit reached! % 2.92/0.91 % (3656541)------------------------------ % 4.56/1.07 % (3656541)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.56/1.07 % (3656541)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.56/1.07 % (3656541)CaDiCaL version: 2.1.3 % 4.56/1.07 % (3656541)Termination reason: Instruction limit % 4.56/1.07 % (3656541)Termination phase: Saturation % 4.56/1.07 % (3656541)Time elapsed: 0.005 s % 4.56/1.07 % (3656541)Peak memory usage: 89 MB % 4.56/1.07 % (3656541)Instructions burned: 16 (million) % 4.56/1.07 % (3656540)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=1979036535:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2998 on theBenchmark for (2998ds/29Mi) % 4.56/1.07 % (3656539)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=1338485638:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2998 on theBenchmark for (2998ds/14Mi) % 4.56/1.07 % (3656539)Instruction limit reached! % 4.56/1.07 % (3656539)------------------------------ % 4.56/1.07 % (3656539)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.56/1.07 % (3656539)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.56/1.07 % (3656539)CaDiCaL version: 2.1.3 % 4.56/1.07 % (3656539)Termination reason: Instruction limit % 4.56/1.07 % (3656539)Termination phase: Saturation % 4.56/1.07 % (3656539)Time elapsed: 0.011 s % 4.56/1.07 % (3656539)Peak memory usage: 88 MB % 4.56/1.07 % (3656539)Instructions burned: 14 (million) % 4.56/1.07 % (3656540)Instruction limit reached! % 4.56/1.07 % (3656540)------------------------------ % 4.56/1.07 % (3656540)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.56/1.07 % (3656540)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.56/1.07 % (3656540)CaDiCaL version: 2.1.3 % 4.56/1.07 % (3656540)Termination reason: Instruction limit % 4.56/1.07 % (3656540)Termination phase: Saturation % 4.56/1.07 % (3656540)Time elapsed: 0.023 s % 4.56/1.07 % (3656540)Peak memory usage: 88 MB % 4.56/1.07 % (3656540)Instructions burned: 30 (million) % 4.56/1.07 % (3656527)Instruction limit reached! % 4.56/1.07 % (3656527)------------------------------ % 4.56/1.07 % (3656527)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.56/1.07 % (3656527)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.56/1.07 % (3656527)CaDiCaL version: 2.1.3 % 4.56/1.07 % (3656527)Termination reason: Instruction limit % 4.56/1.07 % (3656527)Termination phase: Saturation % 4.56/1.07 % (3656527)Time elapsed: 0.166 s % 4.56/1.07 % (3656527)Peak memory usage: 119 MB % 4.56/1.07 % (3656527)Instructions burned: 202 (million) % 4.56/1.07 % (3656542)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=3859697761:i=24:canc=force:rtra=on_2998 on theBenchmark for (2998ds/24Mi) % 4.56/1.07 % (3656543)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=3457156171:i=27:canc=cautious:fsr=off:rtra=on_2998 on theBenchmark for (2998ds/27Mi) % 4.56/1.07 % (3656542)Instruction limit reached! % 4.56/1.07 % (3656542)------------------------------ % 4.56/1.07 % (3656542)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.56/1.07 % (3656542)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.56/1.07 % (3656542)CaDiCaL version: 2.1.3 % 4.56/1.07 % (3656542)Termination reason: Instruction limit % 4.56/1.07 % (3656542)Termination phase: Saturation % 4.56/1.07 % (3656542)Time elapsed: 0.018 s % 4.56/1.07 % (3656542)Peak memory usage: 89 MB % 4.56/1.07 % (3656542)Instructions burned: 24 (million) % 4.56/1.07 % (3656543)Instruction limit reached! % 4.56/1.07 % (3656543)------------------------------ % 4.56/1.07 % (3656543)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.56/1.07 % (3656543)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.56/1.07 % (3656543)CaDiCaL version: 2.1.3 % 4.56/1.07 % (3656543)Termination reason: Instruction limit % 4.56/1.07 % (3656543)Termination phase: Saturation % 4.56/1.07 % (3656543)Time elapsed: 0.018 s % 4.56/1.07 % (3656543)Peak memory usage: 90 MB % 4.56/1.07 % (3656543)Instructions burned: 27 (million) % 4.56/1.07 % (3656545)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=3231910556:i=85:gtgl=4:rtra=on:gtg=exists_sym_2997 on theBenchmark for (2997ds/85Mi) % 4.56/1.07 % (3656526)Instruction limit reached! % 4.56/1.07 % (3656526)------------------------------ % 4.56/1.07 % (3656526)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.12/1.21 % (3656526)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.12/1.21 % (3656526)CaDiCaL version: 2.1.3 % 5.12/1.21 % (3656526)Termination reason: Instruction limit % 5.12/1.21 % (3656526)Termination phase: Saturation % 5.12/1.21 % (3656526)Time elapsed: 0.226 s % 5.12/1.21 % (3656526)Peak memory usage: 117 MB % 5.12/1.21 % (3656526)Instructions burned: 307 (million) % 5.12/1.21 % (3656545)Instruction limit reached! % 5.12/1.21 % (3656545)------------------------------ % 5.12/1.21 % (3656545)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.12/1.21 % (3656545)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.12/1.21 % (3656545)CaDiCaL version: 2.1.3 % 5.12/1.21 % (3656545)Termination reason: Instruction limit % 5.12/1.21 % (3656545)Termination phase: Saturation % 5.12/1.21 % (3656545)Time elapsed: 0.031 s % 5.12/1.21 % (3656545)Peak memory usage: 89 MB % 5.12/1.21 % (3656545)Instructions burned: 88 (million) % 5.12/1.21 % (3656548)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=3549154471:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2997 on theBenchmark for (2997ds/2Mi) % 5.12/1.21 % (3656548)Instruction limit reached! % 5.12/1.21 % (3656548)------------------------------ % 5.12/1.21 % (3656548)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.12/1.21 % (3656548)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.12/1.21 % (3656548)CaDiCaL version: 2.1.3 % 5.12/1.21 % (3656548)Termination reason: Instruction limit % 5.12/1.21 % (3656548)Termination phase: Property scanning % 5.12/1.21 % (3656548)Time elapsed: 0.002 s % 5.12/1.21 % (3656548)Peak memory usage: 86 MB % 5.12/1.21 % (3656548)Instructions burned: 3 (million) % 5.12/1.21 % (3656549)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=1086238120:i=181:rtra=on:ss=axioms:ev=cautious_2997 on theBenchmark for (2997ds/181Mi) % 5.12/1.21 % (3656552)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=3870060367:i=4:ep=RST:ins=2:rtra=on_2996 on theBenchmark for (2996ds/4Mi) % 5.12/1.21 % (3656552)Instruction limit reached! % 5.12/1.21 % (3656552)------------------------------ % 5.12/1.21 % (3656552)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.12/1.21 % (3656552)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.12/1.21 % (3656552)CaDiCaL version: 2.1.3 % 5.12/1.21 % (3656552)Termination reason: Instruction limit % 5.12/1.21 % (3656552)Termination phase: Property scanning % 5.12/1.21 % (3656552)Time elapsed: 0.003 s % 5.12/1.21 % (3656552)Peak memory usage: 87 MB % 5.12/1.21 % (3656552)Instructions burned: 5 (million) % 5.12/1.21 % (3656554)lrs+10_1_thi=all:si=on:fd=off:random_seed=1189778302:i=53:rtra=on:gtg=all_2996 on theBenchmark for (2996ds/53Mi) % 5.12/1.21 % (3656549)Refutation not found, incomplete strategy % 5.12/1.21 % (3656549)------------------------------ % 5.12/1.21 % (3656549)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.12/1.21 % (3656549)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.12/1.21 % (3656549)CaDiCaL version: 2.1.3 % 5.12/1.21 % (3656549)Termination reason: Refutation not found, incomplete strategy % 5.12/1.21 % (3656549)Time elapsed: 0.034 s % 5.12/1.21 % (3656549)Peak memory usage: 90 MB % 5.12/1.21 % (3656549)Instructions burned: 45 (million) % 5.12/1.21 % (3656553)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=2643813915:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2996 on theBenchmark for (2996ds/66Mi) % 5.12/1.21 % (3656557)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=3712447576:st=3:i=2:rtra=on:ss=axioms_2996 on theBenchmark for (2996ds/2Mi) % 5.12/1.21 % (3656557)Instruction limit reached! % 5.12/1.21 % (3656557)------------------------------ % 5.12/1.21 % (3656557)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.12/1.21 % (3656557)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.12/1.21 % (3656557)CaDiCaL version: 2.1.3 % 5.12/1.21 % (3656557)Termination reason: Instruction limit % 5.12/1.21 % (3656557)Termination phase: Clausification % 5.12/1.21 % (3656557)Time elapsed: 0.001 s % 5.12/1.21 % (3656557)Peak memory usage: 86 MB % 5.12/1.21 % (3656557)Instructions burned: 2 (million) % 5.12/1.21 % (3656556)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=1434234653:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2996 on theBenchmark for (2996ds/8Mi) % 6.25/1.40 % (3656556)Instruction limit reached! % 6.25/1.40 % (3656556)------------------------------ % 6.25/1.40 % (3656556)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.25/1.40 % (3656556)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.25/1.40 % (3656556)CaDiCaL version: 2.1.3 % 6.25/1.40 % (3656556)Termination reason: Instruction limit % 6.25/1.40 % (3656556)Termination phase: Saturation % 6.25/1.40 % (3656556)Time elapsed: 0.006 s % 6.25/1.40 % (3656556)Peak memory usage: 88 MB % 6.25/1.40 % (3656556)Instructions burned: 9 (million) % 6.25/1.40 % (3656554)Instruction limit reached! % 6.25/1.40 % (3656554)------------------------------ % 6.25/1.40 % (3656554)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.25/1.40 % (3656554)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.25/1.40 % (3656554)CaDiCaL version: 2.1.3 % 6.25/1.40 % (3656554)Termination reason: Instruction limit % 6.25/1.40 % (3656554)Termination phase: Saturation % 6.25/1.40 % (3656554)Time elapsed: 0.064 s % 6.25/1.40 % (3656554)Peak memory usage: 116 MB % 6.25/1.40 % (3656554)Instructions burned: 53 (million) % 6.25/1.40 % (3656559)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=2386878216:i=2:doe=on:canc=force:asg=cautious:rtra=on_2996 on theBenchmark for (2996ds/2Mi) % 6.25/1.40 % (3656559)Instruction limit reached! % 6.25/1.40 % (3656559)------------------------------ % 6.25/1.40 % (3656559)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.25/1.40 % (3656559)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.25/1.40 % (3656559)CaDiCaL version: 2.1.3 % 6.25/1.40 % (3656559)Termination reason: Instruction limit % 6.25/1.40 % (3656559)Termination phase: Property scanning % 6.25/1.40 % (3656559)Time elapsed: 0.002 s % 6.25/1.40 % (3656559)Peak memory usage: 86 MB % 6.25/1.40 % (3656559)Instructions burned: 3 (million) % 6.25/1.40 % (3656553)Instruction limit reached! % 6.25/1.40 % (3656553)------------------------------ % 6.25/1.40 % (3656553)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.25/1.40 % (3656553)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.25/1.40 % (3656553)CaDiCaL version: 2.1.3 % 6.25/1.40 % (3656553)Termination reason: Instruction limit % 6.25/1.40 % (3656553)Termination phase: Saturation % 6.25/1.40 % (3656553)Time elapsed: 0.092 s % 6.25/1.40 % (3656553)Peak memory usage: 134 MB % 6.25/1.40 % (3656553)Instructions burned: 66 (million) % 6.25/1.40 % (3656562)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=1702243955:i=127:doe=on:rtra=on_2995 on theBenchmark for (2995ds/127Mi) % 6.25/1.40 % (3656566)dis+10_1_si=on:random_seed=3790473692:i=10:ep=R:rtra=on_2995 on theBenchmark for (2995ds/10Mi) % 6.25/1.40 % (3656566)Instruction limit reached! % 6.25/1.40 % (3656566)------------------------------ % 6.25/1.40 % (3656566)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.25/1.40 % (3656566)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.25/1.40 % (3656566)CaDiCaL version: 2.1.3 % 6.25/1.40 % (3656566)Termination reason: Instruction limit % 6.25/1.40 % (3656566)Termination phase: Saturation % 6.25/1.40 % (3656566)Time elapsed: 0.004 s % 6.25/1.40 % (3656566)Peak memory usage: 88 MB % 6.25/1.40 % (3656566)Instructions burned: 12 (million) % 6.25/1.40 % (3656569)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=1257981333:avsq=on:i=35:doe=on:thsqd=64:nm=64:fsr=off:thsqc=32:rtra=on:tac=light:ss=included:thsq=on:ev=off:sgt=32_2994 on theBenchmark for (2994ds/35Mi) % 6.25/1.40 % (3656568)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=3687676456:i=26:canc=cautious:av=off:rtra=on_2994 on theBenchmark for (2994ds/26Mi) % 6.25/1.40 % (3656575)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=3194740851:i=370:ep=RS:fsr=off:rtra=on_2994 on theBenchmark for (2994ds/370Mi) % 6.25/1.40 % (3656569)Instruction limit reached! % 6.25/1.40 % (3656569)------------------------------ % 6.25/1.40 % (3656569)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.25/1.40 % (3656569)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.25/1.40 % (3656569)CaDiCaL version: 2.1.3 % 6.25/1.40 % (3656569)Termination reason: Instruction limit % 7.56/1.64 % (3656569)Termination phase: Saturation % 7.56/1.64 % (3656569)Time elapsed: 0.023 s % 7.56/1.64 % (3656569)Peak memory usage: 89 MB % 7.56/1.64 % (3656569)Instructions burned: 35 (million) % 7.56/1.64 % (3656568)Instruction limit reached! % 7.56/1.64 % (3656568)------------------------------ % 7.56/1.64 % (3656568)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.56/1.64 % (3656568)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.56/1.64 % (3656568)CaDiCaL version: 2.1.3 % 7.56/1.64 % (3656568)Termination reason: Instruction limit % 7.56/1.64 % (3656568)Termination phase: Saturation % 7.56/1.64 % (3656568)Time elapsed: 0.017 s % 7.56/1.64 % (3656568)Peak memory usage: 89 MB % 7.56/1.64 % (3656568)Instructions burned: 26 (million) % 7.56/1.64 % (3656571)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=3127369231:i=2:fsr=off:rtra=on:inst=on_2994 on theBenchmark for (2994ds/2Mi) % 7.56/1.64 % (3656571)Instruction limit reached! % 7.56/1.64 % (3656571)------------------------------ % 7.56/1.64 % (3656571)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.56/1.64 % (3656571)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.56/1.64 % (3656571)CaDiCaL version: 2.1.3 % 7.56/1.64 % (3656571)Termination reason: Instruction limit % 7.56/1.64 % (3656571)Termination phase: Property scanning % 7.56/1.64 % (3656571)Time elapsed: 0.002 s % 7.56/1.64 % (3656571)Peak memory usage: 86 MB % 7.56/1.64 % (3656571)Instructions burned: 3 (million) % 7.56/1.64 % (3656562)Instruction limit reached! % 7.56/1.64 % (3656562)------------------------------ % 7.56/1.64 % (3656562)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.56/1.64 % (3656562)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.56/1.64 % (3656562)CaDiCaL version: 2.1.3 % 7.56/1.64 % (3656562)Termination reason: Instruction limit % 7.56/1.64 % (3656562)Termination phase: Saturation % 7.56/1.64 % (3656562)Time elapsed: 0.115 s % 7.56/1.64 % (3656562)Peak memory usage: 118 MB % 7.56/1.64 % (3656562)Instructions burned: 127 (million) % 7.56/1.64 % (3656574)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=3882936740:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2994 on theBenchmark for (2994ds/8Mi) % 7.56/1.64 % (3656574)Instruction limit reached! % 7.56/1.64 % (3656574)------------------------------ % 7.56/1.64 % (3656574)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.56/1.64 % (3656574)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.56/1.64 % (3656574)CaDiCaL version: 2.1.3 % 7.56/1.64 % (3656574)Termination reason: Instruction limit % 7.56/1.64 % (3656574)Termination phase: Saturation % 7.56/1.64 % (3656574)Time elapsed: 0.006 s % 7.56/1.64 % (3656574)Peak memory usage: 88 MB % 7.56/1.64 % (3656574)Instructions burned: 9 (million) % 7.56/1.64 % (3656549)------------------------------ % 7.56/1.64 % (3656549)------------------------------ % 7.56/1.64 % (3656575)Instruction limit reached! % 7.56/1.64 % (3656575)------------------------------ % 7.56/1.64 % (3656575)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.56/1.64 % (3656575)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.56/1.64 % (3656575)CaDiCaL version: 2.1.3 % 7.56/1.64 % (3656575)Termination reason: Instruction limit % 7.56/1.64 % (3656575)Termination phase: Saturation % 7.56/1.64 % (3656575)Time elapsed: 0.087 s % 7.56/1.64 % (3656575)Peak memory usage: 89 MB % 7.56/1.64 % (3656575)Instructions burned: 373 (million) % 7.56/1.64 % (3656581)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=1906440851:i=226:rtra=on:gtg=position:ss=axioms_2993 on theBenchmark for (2993ds/226Mi) % 7.56/1.64 % (3656580)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=2807830350:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2993 on theBenchmark for (2993ds/13Mi) % 7.56/1.64 % (3656583)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=799324163:i=71:rtra=on:gtg=exists_top_2993 on theBenchmark for (2993ds/71Mi) % 7.56/1.64 % (3656582)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=293178856:i=10:rtra=on_2993 on theBenchmark for (2993ds/10Mi) % 7.56/1.64 % (3656585)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=2098305417:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2993 on theBenchmark for (2993ds/75Mi) % 8.41/1.86 % (3656582)Instruction limit reached! % 8.41/1.86 % (3656582)------------------------------ % 8.41/1.86 % (3656582)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.41/1.86 % (3656582)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.41/1.86 % (3656582)CaDiCaL version: 2.1.3 % 8.41/1.86 % (3656582)Termination reason: Instruction limit % 8.41/1.86 % (3656582)Termination phase: Saturation % 8.41/1.86 % (3656582)Time elapsed: 0.008 s % 8.41/1.86 % (3656582)Peak memory usage: 88 MB % 8.41/1.86 % (3656582)Instructions burned: 10 (million) % 8.41/1.86 % (3656580)Instruction limit reached! % 8.41/1.86 % (3656580)------------------------------ % 8.41/1.86 % (3656580)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.41/1.86 % (3656580)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.41/1.86 % (3656580)CaDiCaL version: 2.1.3 % 8.41/1.86 % (3656580)Termination reason: Instruction limit % 8.41/1.86 % (3656580)Termination phase: Saturation % 8.41/1.86 % (3656580)Time elapsed: 0.028 s % 8.41/1.86 % (3656580)Peak memory usage: 112 MB % 8.41/1.86 % (3656580)Instructions burned: 13 (million) % 8.41/1.86 % (3656587)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=2662947583:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2992 on theBenchmark for (2992ds/130Mi) % 8.41/1.86 % (3656586)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=2716219075:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2992 on theBenchmark for (2992ds/294Mi) % 8.41/1.86 % (3656585)Instruction limit reached! % 8.41/1.86 % (3656585)------------------------------ % 8.41/1.86 % (3656585)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.41/1.86 % (3656585)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.41/1.86 % (3656585)CaDiCaL version: 2.1.3 % 8.41/1.86 % (3656585)Termination reason: Instruction limit % 8.41/1.86 % (3656585)Termination phase: Saturation % 8.41/1.86 % (3656585)Time elapsed: 0.053 s % 8.41/1.86 % (3656585)Peak memory usage: 90 MB % 8.41/1.86 % (3656585)Instructions burned: 76 (million) % 8.41/1.86 % (3656583)Instruction limit reached! % 8.41/1.86 % (3656583)------------------------------ % 8.41/1.86 % (3656583)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.41/1.86 % (3656583)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.41/1.86 % (3656583)CaDiCaL version: 2.1.3 % 8.41/1.86 % (3656583)Termination reason: Instruction limit % 8.41/1.86 % (3656583)Termination phase: Saturation % 8.41/1.86 % (3656583)Time elapsed: 0.094 s % 8.41/1.86 % (3656583)Peak memory usage: 133 MB % 8.41/1.86 % (3656583)Instructions burned: 71 (million) % 8.41/1.86 % (3656587)Instruction limit reached! % 8.41/1.86 % (3656587)------------------------------ % 8.41/1.86 % (3656587)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.41/1.86 % (3656587)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.41/1.86 % (3656587)CaDiCaL version: 2.1.3 % 8.41/1.86 % (3656587)Termination reason: Instruction limit % 8.41/1.86 % (3656587)Termination phase: Saturation % 8.41/1.86 % (3656587)Time elapsed: 0.062 s % 8.41/1.86 % (3656587)Peak memory usage: 118 MB % 8.41/1.86 % (3656587)Instructions burned: 132 (million) % 8.41/1.86 % (3656593)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=942151361:i=131:rtra=on_2991 on theBenchmark for (2991ds/131Mi) % 8.41/1.86 % (3656581)Instruction limit reached! % 8.41/1.86 % (3656581)------------------------------ % 8.41/1.86 % (3656581)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.41/1.86 % (3656581)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.41/1.86 % (3656581)CaDiCaL version: 2.1.3 % 8.41/1.86 % (3656581)Termination reason: Instruction limit % 8.41/1.86 % (3656581)Termination phase: Saturation % 8.41/1.86 % (3656581)Time elapsed: 0.148 s % 8.41/1.86 % (3656581)Peak memory usage: 118 MB % 8.41/1.86 % (3656581)Instructions burned: 227 (million) % 8.41/1.86 % (3656594)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=3803810564:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2991 on theBenchmark for (2991ds/40Mi) % 8.41/1.86 % (3656599)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=4161305012:i=131:canc=cautious:fsr=off:rtra=on_2991 on theBenchmark for (2991ds/131Mi) % 8.41/1.86 % (3656597)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=1586686268:i=307:rtra=on:gtg=exists_top_2991 on theBenchmark for (2991ds/307Mi) % 12.21/2.19 % (3656598)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=3745321084:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2991 on theBenchmark for (2991ds/598Mi) % 12.21/2.19 % (3656594)Instruction limit reached! % 12.21/2.19 % (3656594)------------------------------ % 12.21/2.19 % (3656594)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.21/2.19 % (3656594)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.21/2.19 % (3656594)CaDiCaL version: 2.1.3 % 12.21/2.19 % (3656594)Termination reason: Instruction limit % 12.21/2.19 % (3656594)Termination phase: Saturation % 12.21/2.19 % (3656594)Time elapsed: 0.068 s % 12.21/2.19 % (3656594)Peak memory usage: 134 MB % 12.21/2.19 % (3656594)Instructions burned: 40 (million) % 12.21/2.19 % (3656599)Instruction limit reached! % 12.21/2.19 % (3656599)------------------------------ % 12.21/2.19 % (3656599)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.21/2.19 % (3656599)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.21/2.19 % (3656599)CaDiCaL version: 2.1.3 % 12.21/2.19 % (3656599)Termination reason: Instruction limit % 12.21/2.19 % (3656599)Termination phase: Saturation % 12.21/2.19 % (3656599)Time elapsed: 0.059 s % 12.21/2.19 % (3656599)Peak memory usage: 118 MB % 12.21/2.19 % (3656599)Instructions burned: 133 (million) % 12.21/2.19 % (3656586)Instruction limit reached! % 12.21/2.19 % (3656586)------------------------------ % 12.21/2.19 % (3656586)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.21/2.19 % (3656586)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.21/2.19 % (3656586)CaDiCaL version: 2.1.3 % 12.21/2.19 % (3656586)Termination reason: Instruction limit % 12.21/2.19 % (3656586)Termination phase: Saturation % 12.21/2.19 % (3656586)Time elapsed: 0.206 s % 12.21/2.19 % (3656586)Peak memory usage: 91 MB % 12.21/2.19 % (3656586)Instructions burned: 295 (million) % 12.21/2.19 % (3656601)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=423419580:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2990 on theBenchmark for (2990ds/259Mi) % 12.21/2.19 % (3656593)Instruction limit reached! % 12.21/2.19 % (3656593)------------------------------ % 12.21/2.19 % (3656593)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.21/2.19 % (3656593)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.21/2.19 % (3656593)CaDiCaL version: 2.1.3 % 12.21/2.19 % (3656593)Termination reason: Instruction limit % 12.21/2.19 % (3656593)Termination phase: Saturation % 12.21/2.19 % (3656593)Time elapsed: 0.136 s % 12.21/2.19 % (3656593)Peak memory usage: 135 MB % 12.21/2.19 % (3656593)Instructions burned: 132 (million) % 12.21/2.19 % (3656607)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=3253981894:i=383:fsr=off:rtra=on:ev=force_2989 on theBenchmark for (2989ds/383Mi) % 12.21/2.19 % (3656606)dis+10_1_si=on:random_seed=828673439:s2a=on:i=1000:rtra=on:gtg=exists_all_2989 on theBenchmark for (2989ds/1000Mi) % 12.21/2.19 % (3656597)Instruction limit reached! % 12.21/2.19 % (3656597)------------------------------ % 12.21/2.19 % (3656597)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.21/2.19 % (3656597)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.21/2.19 % (3656597)CaDiCaL version: 2.1.3 % 12.21/2.19 % (3656597)Termination reason: Instruction limit % 12.21/2.19 % (3656597)Termination phase: Saturation % 12.21/2.19 % (3656597)Time elapsed: 0.181 s % 12.21/2.19 % (3656597)Peak memory usage: 92 MB % 12.21/2.19 % (3656597)Instructions burned: 309 (million) % 12.21/2.19 % (3656608)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=2546836801:i=141:doe=on:rtra=on_2989 on theBenchmark for (2989ds/141Mi) % 12.21/2.19 % (3656610)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=3909803681:i=65:nm=16:rtra=on_2989 on theBenchmark for (2989ds/65Mi) % 12.21/2.19 % (3656601)Instruction limit reached! % 12.21/2.19 % (3656601)------------------------------ % 12.21/2.19 % (3656601)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.21/2.19 % (3656601)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.21/2.19 % (3656601)CaDiCaL version: 2.1.3 % 13.10/2.47 % (3656601)Termination reason: Instruction limit % 13.10/2.47 % (3656601)Termination phase: Saturation % 13.10/2.47 % (3656601)Time elapsed: 0.167 s % 13.10/2.47 % (3656601)Peak memory usage: 119 MB % 13.10/2.47 % (3656601)Instructions burned: 260 (million) % 13.10/2.47 % (3656610)Refutation not found, incomplete strategy % 13.10/2.47 % (3656610)------------------------------ % 13.10/2.47 % (3656610)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.10/2.47 % (3656610)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.10/2.47 % (3656610)CaDiCaL version: 2.1.3 % 13.10/2.47 % (3656610)Termination reason: Refutation not found, incomplete strategy % 13.10/2.47 % (3656610)Time elapsed: 0.046 s % 13.10/2.47 % (3656610)Peak memory usage: 116 MB % 13.10/2.47 % (3656610)Instructions burned: 33 (million) % 13.10/2.47 % (3656607)Instruction limit reached! % 13.10/2.47 % (3656607)------------------------------ % 13.10/2.47 % (3656607)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.10/2.47 % (3656607)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.10/2.47 % (3656607)CaDiCaL version: 2.1.3 % 13.10/2.47 % (3656607)Termination reason: Instruction limit % 13.10/2.47 % (3656607)Termination phase: Saturation % 13.10/2.47 % (3656607)Time elapsed: 0.121 s % 13.10/2.47 % (3656607)Peak memory usage: 93 MB % 13.10/2.47 % (3656607)Instructions burned: 386 (million) % 13.10/2.47 % (3656608)Instruction limit reached! % 13.10/2.47 % (3656608)------------------------------ % 13.10/2.47 % (3656608)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.10/2.47 % (3656608)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.10/2.47 % (3656608)CaDiCaL version: 2.1.3 % 13.10/2.47 % (3656608)Termination reason: Instruction limit % 13.10/2.47 % (3656608)Termination phase: Saturation % 13.10/2.47 % (3656608)Time elapsed: 0.095 s % 13.10/2.47 % (3656608)Peak memory usage: 90 MB % 13.10/2.47 % (3656608)Instructions burned: 142 (million) % 13.10/2.47 % (3656613)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=3648146210:i=121:nm=16:rtra=on_2988 on theBenchmark for (2988ds/121Mi) % 13.10/2.47 % (3656617)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=463071227:i=39:ins=3:rtra=on_2987 on theBenchmark for (2987ds/39Mi) % 13.10/2.47 % (3656616)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=1506028627:s2a=on:i=128:s2at=5:ins=3:rtra=on_2987 on theBenchmark for (2987ds/128Mi) % 13.10/2.47 % (3656617)Instruction limit reached! % 13.10/2.47 % (3656617)------------------------------ % 13.10/2.47 % (3656617)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.10/2.47 % (3656617)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.10/2.47 % (3656617)CaDiCaL version: 2.1.3 % 13.10/2.47 % (3656617)Termination reason: Instruction limit % 13.10/2.47 % (3656617)Termination phase: Saturation % 13.10/2.47 % (3656617)Time elapsed: 0.028 s % 13.10/2.47 % (3656617)Peak memory usage: 117 MB % 13.10/2.47 % (3656617)Instructions burned: 41 (million) % 13.10/2.47 % (3656613)Instruction limit reached! % 13.10/2.47 % (3656613)------------------------------ % 13.10/2.47 % (3656613)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.10/2.47 % (3656613)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.10/2.47 % (3656613)CaDiCaL version: 2.1.3 % 13.10/2.47 % (3656613)Termination reason: Instruction limit % 13.10/2.47 % (3656613)Termination phase: Saturation % 13.10/2.47 % (3656613)Time elapsed: 0.079 s % 13.10/2.47 % (3656613)Peak memory usage: 89 MB % 13.10/2.47 % (3656613)Instructions burned: 122 (million) % 13.10/2.47 % (3656598)Instruction limit reached! % 13.10/2.47 % (3656598)------------------------------ % 13.10/2.47 % (3656598)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.10/2.47 % (3656598)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.10/2.47 % (3656598)CaDiCaL version: 2.1.3 % 13.10/2.47 % (3656598)Termination reason: Instruction limit % 13.10/2.47 % (3656598)Termination phase: Saturation % 13.10/2.47 % (3656598)Time elapsed: 0.377 s % 13.10/2.47 % (3656598)Peak memory usage: 140 MB % 13.10/2.47 % (3656598)Instructions burned: 598 (million) % 13.10/2.47 % (3656618)dis+1010_1_to=kbo:si=on:random_seed=503780857:i=175:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2987 on theBenchmark for (2987ds/175Mi) % 13.10/2.47 % (3656622)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=2576550496:i=329:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2986 on theBenchmark for (2986ds/329Mi) % 15.50/2.72 % (3656616)Instruction limit reached! % 15.50/2.72 % (3656616)------------------------------ % 15.50/2.72 % (3656616)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.50/2.72 % (3656616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.50/2.72 % (3656616)CaDiCaL version: 2.1.3 % 15.50/2.72 % (3656616)Termination reason: Instruction limit % 15.50/2.72 % (3656616)Termination phase: Saturation % 15.50/2.72 % (3656616)Time elapsed: 0.105 s % 15.50/2.72 % (3656616)Peak memory usage: 119 MB % 15.50/2.72 % (3656616)Instructions burned: 129 (million) % 15.50/2.72 % (3656610)------------------------------ % 15.50/2.72 % (3656610)------------------------------ % 15.50/2.72 % (3656623)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=1943978915:s2a=on:i=483:doe=on:nm=32:rtra=on_2986 on theBenchmark for (2986ds/483Mi) % 15.50/2.72 % (3656624)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=1360899465:thitd=on:i=215:nm=0:rtra=on:ev=force_2985 on theBenchmark for (2985ds/215Mi) % 15.50/2.72 % (3656618)Instruction limit reached! % 15.50/2.72 % (3656618)------------------------------ % 15.50/2.72 % (3656618)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.50/2.72 % (3656618)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.50/2.72 % (3656618)CaDiCaL version: 2.1.3 % 15.50/2.72 % (3656618)Termination reason: Instruction limit % 15.50/2.72 % (3656618)Termination phase: Saturation % 15.50/2.72 % (3656618)Time elapsed: 0.126 s % 15.50/2.72 % (3656618)Peak memory usage: 91 MB % 15.50/2.72 % (3656618)Instructions burned: 176 (million) % 15.50/2.72 % (3656627)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=3648252918:i=349:rtra=on_2985 on theBenchmark for (2985ds/349Mi) % 15.50/2.72 % (3656622)Instruction limit reached! % 15.50/2.72 % (3656622)------------------------------ % 15.50/2.72 % (3656622)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.50/2.72 % (3656622)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.50/2.72 % (3656622)CaDiCaL version: 2.1.3 % 15.50/2.72 % (3656622)Termination reason: Instruction limit % 15.50/2.72 % (3656622)Termination phase: Saturation % 15.50/2.72 % (3656622)Time elapsed: 0.135 s % 15.50/2.72 % (3656622)Peak memory usage: 120 MB % 15.50/2.72 % (3656622)Instructions burned: 329 (million) % 15.50/2.72 % (3656628)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=3150454372:st=2:i=295:rtra=on:ss=axioms_2985 on theBenchmark for (2985ds/295Mi) % 15.50/2.72 % (3656633)dis+1010_1_to=lpo:sil=128000:sas=z3:si=on:nwc=5:random_seed=3456772858:i=281:gtgl=2:rtra=on:gtg=all_2984 on theBenchmark for (2984ds/281Mi) % 15.50/2.72 % (3656631)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=1643355739:i=328:kws=inv_frequency:nm=20:rtra=on_2984 on theBenchmark for (2984ds/328Mi) % 15.50/2.72 % (3656624)Instruction limit reached! % 15.50/2.72 % (3656624)------------------------------ % 15.50/2.72 % (3656624)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.50/2.72 % (3656624)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.50/2.72 % (3656624)CaDiCaL version: 2.1.3 % 15.50/2.72 % (3656624)Termination reason: Instruction limit % 15.50/2.72 % (3656624)Termination phase: Saturation % 15.50/2.72 % (3656624)Time elapsed: 0.176 s % 15.50/2.72 % (3656624)Peak memory usage: 135 MB % 15.50/2.72 % (3656624)Instructions burned: 216 (million) % 15.50/2.72 % (3656606)Instruction limit reached! % 15.50/2.72 % (3656606)------------------------------ % 15.50/2.72 % (3656606)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.50/2.72 % (3656606)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.50/2.72 % (3656606)CaDiCaL version: 2.1.3 % 15.50/2.72 % (3656606)Termination reason: Instruction limit % 15.50/2.72 % (3656606)Termination phase: Saturation % 15.50/2.72 % (3656606)Time elapsed: 0.621 s % 15.50/2.72 % (3656606)Peak memory usage: 94 MB % 15.50/2.72 % (3656606)Instructions burned: 1001 (million) % 15.50/2.72 % (3656633)Instruction limit reached! % 15.50/2.72 % (3656633)------------------------------ % 15.50/2.72 % (3656633)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.50/2.72 % (3656633)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.48/2.96 % (3656633)CaDiCaL version: 2.1.3 % 16.48/2.96 % (3656633)Termination reason: Instruction limit % 16.48/2.96 % (3656633)Termination phase: Saturation % 16.48/2.96 % (3656633)Time elapsed: 0.110 s % 16.48/2.96 % (3656633)Peak memory usage: 118 MB % 16.48/2.96 % (3656633)Instructions burned: 283 (million) % 16.48/2.96 % (3656628)Instruction limit reached! % 16.48/2.96 % (3656628)------------------------------ % 16.48/2.96 % (3656628)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.48/2.96 % (3656628)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.48/2.96 % (3656628)CaDiCaL version: 2.1.3 % 16.48/2.96 % (3656628)Termination reason: Instruction limit % 16.48/2.96 % (3656628)Termination phase: Saturation % 16.48/2.96 % (3656628)Time elapsed: 0.170 s % 16.48/2.96 % (3656628)Peak memory usage: 91 MB % 16.48/2.96 % (3656628)Instructions burned: 296 (million) % 16.48/2.96 % (3656627)Instruction limit reached! % 16.48/2.96 % (3656627)------------------------------ % 16.48/2.96 % (3656627)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.48/2.96 % (3656627)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.48/2.96 % (3656627)CaDiCaL version: 2.1.3 % 16.48/2.96 % (3656627)Termination reason: Instruction limit % 16.48/2.96 % (3656627)Termination phase: Saturation % 16.48/2.96 % (3656627)Time elapsed: 0.232 s % 16.48/2.96 % (3656627)Peak memory usage: 120 MB % 16.48/2.96 % (3656627)Instructions burned: 350 (million) % 16.48/2.96 % (3656637)lrs+1010_1_to=kbo:sil=128000:si=on:sos=on:urr=on:uwa=alasca_main:random_seed=379289198:i=484:doe=on:nm=0:av=off:rtra=on:ss=axioms_2982 on theBenchmark for (2982ds/484Mi) % 16.48/2.96 % (3656623)Instruction limit reached! % 16.48/2.96 % (3656623)------------------------------ % 16.48/2.96 % (3656623)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.48/2.96 % (3656623)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.48/2.96 % (3656623)CaDiCaL version: 2.1.3 % 16.48/2.96 % (3656623)Termination reason: Instruction limit % 16.48/2.96 % (3656623)Termination phase: Saturation % 16.48/2.96 % (3656623)Time elapsed: 0.356 s % 16.48/2.96 % (3656623)Peak memory usage: 135 MB % 16.48/2.96 % (3656623)Instructions burned: 484 (million) % 16.48/2.96 % (3656639)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=2292600222:i=416:rtra=on:gtg=position:ss=axioms_2982 on theBenchmark for (2982ds/416Mi) % 16.48/2.96 % (3656638)lrs+21_1_to=kbo:sil=128000:thi=neg_eq:si=on:random_seed=1541479968:i=321:canc=force:rtra=on:tac=axiom:ss=axioms:ev=force_2982 on theBenchmark for (2982ds/321Mi) % 16.48/2.96 % (3656640)lrs+1010_1_to=kbo:tgt=ground:fde=unused:sas=z3:si=on:sp=unary_frequency:gve=force:spb=goal:tha=off:random_seed=2786211108:i=471:thf=on:kws=precedence:rtra=on_2982 on theBenchmark for (2982ds/471Mi) % 16.48/2.96 % (3656631)Instruction limit reached! % 16.48/2.96 % (3656631)------------------------------ % 16.48/2.96 % (3656631)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.48/2.96 % (3656631)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.48/2.96 % (3656631)CaDiCaL version: 2.1.3 % 16.48/2.96 % (3656631)Termination reason: Instruction limit % 16.48/2.96 % (3656631)Termination phase: Saturation % 16.48/2.96 % (3656631)Time elapsed: 0.237 s % 16.48/2.96 % (3656631)Peak memory usage: 119 MB % 16.48/2.96 % (3656631)Instructions burned: 330 (million) % 16.48/2.96 % (3656641)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=490041061:avsq=on:i=276:avsqr=1,2:rtra=on_2981 on theBenchmark for (2981ds/276Mi) % 16.48/2.96 % (3656644)lrs+1010_2_to=kbo:sil=128000:tgt=ground:fde=unused:sas=z3:si=on:uwa=off:tha=off:nwc=1:random_seed=4035656609:i=375:kws=inv_arity_squared:rtra=on_2981 on theBenchmark for (2981ds/375Mi) % 16.48/2.96 % (3656639)Instruction limit reached! % 16.48/2.96 % (3656639)------------------------------ % 16.48/2.96 % (3656639)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.48/2.96 % (3656639)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.48/2.96 % (3656639)CaDiCaL version: 2.1.3 % 16.48/2.96 % (3656639)Termination reason: Instruction limit % 16.48/2.96 % (3656639)Termination phase: Saturation % 16.48/2.96 % (3656639)Time elapsed: 0.145 s % 16.48/2.96 % (3656639)Peak memory usage: 122 MB % 16.48/2.96 % (3656639)Instructions burned: 419 (million) % 16.48/2.96 % (3656638)Instruction limit reached! % 20.82/3.41 % (3656638)------------------------------ % 20.82/3.41 % (3656638)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.82/3.41 % (3656638)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.82/3.41 % (3656638)CaDiCaL version: 2.1.3 % 20.82/3.41 % (3656638)Termination reason: Instruction limit % 20.82/3.41 % (3656638)Termination phase: Saturation % 20.82/3.41 % (3656638)Time elapsed: 0.159 s % 20.82/3.41 % (3656638)Peak memory usage: 114 MB % 20.82/3.41 % (3656638)Instructions burned: 322 (million) % 20.82/3.41 % (3656647)lrs+10_1_to=kbo:sil=128000:tgt=full:sas=z3:si=on:uwa=func_ext:slsqc=1:flr=on:slsq=on:random_seed=3391266548:i=387:bd=preordered:rtra=on:ss=axioms:sgt=8_2980 on theBenchmark for (2980ds/387Mi) % 20.82/3.41 % (3656650)lrs+10_1_to=kbo:sil=128000:fde=none:si=on:norm_ineq=on:urr=on:nwc=0.5:random_seed=2755830001:i=513:kws=frequency:bd=all:rtra=on:gtg=exists_all:ss=axioms:sgt=4_2979 on theBenchmark for (2979ds/513Mi) % 20.82/3.41 % (3656637)Instruction limit reached! % 20.82/3.41 % (3656637)------------------------------ % 20.82/3.41 % (3656637)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.82/3.41 % (3656637)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.82/3.41 % (3656637)CaDiCaL version: 2.1.3 % 20.82/3.41 % (3656637)Termination reason: Instruction limit % 20.82/3.41 % (3656637)Termination phase: Saturation % 20.82/3.41 % (3656637)Time elapsed: 0.297 s % 20.82/3.41 % (3656637)Peak memory usage: 93 MB % 20.82/3.41 % (3656637)Instructions burned: 484 (million) % 20.82/3.41 % (3656641)Instruction limit reached! % 20.82/3.41 % (3656641)------------------------------ % 20.82/3.41 % (3656641)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.82/3.41 % (3656641)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.82/3.41 % (3656641)CaDiCaL version: 2.1.3 % 20.82/3.41 % (3656641)Termination reason: Instruction limit % 20.82/3.41 % (3656641)Termination phase: Saturation % 20.82/3.41 % (3656641)Time elapsed: 0.230 s % 20.82/3.41 % (3656641)Peak memory usage: 136 MB % 20.82/3.41 % (3656641)Instructions burned: 276 (million) % 20.82/3.41 % (3656651)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=968656159:i=334:rtra=on_2979 on theBenchmark for (2979ds/334Mi) % 20.82/3.41 % (3656640)Instruction limit reached! % 20.82/3.41 % (3656640)------------------------------ % 20.82/3.41 % (3656640)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.82/3.41 % (3656640)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.82/3.41 % (3656640)CaDiCaL version: 2.1.3 % 20.82/3.41 % (3656640)Termination reason: Instruction limit % 20.82/3.41 % (3656640)Termination phase: Saturation % 20.82/3.41 % (3656640)Time elapsed: 0.300 s % 20.82/3.41 % (3656640)Peak memory usage: 121 MB % 20.82/3.41 % (3656640)Instructions burned: 471 (million) % 20.82/3.41 % (3656644)Instruction limit reached! % 20.82/3.41 % (3656644)------------------------------ % 20.82/3.41 % (3656644)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.82/3.41 % (3656644)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.82/3.41 % (3656644)CaDiCaL version: 2.1.3 % 20.82/3.41 % (3656644)Termination reason: Instruction limit % 20.82/3.41 % (3656644)Termination phase: Saturation % 20.82/3.41 % (3656644)Time elapsed: 0.244 s % 20.82/3.41 % (3656644)Peak memory usage: 118 MB % 20.82/3.41 % (3656644)Instructions burned: 376 (million) % 20.82/3.41 % (3656654)lrs+1010_1_to=kbo:sil=64000:sas=cadical:si=on:sos=on:bce=on:random_seed=1179189576:i=359:rtra=on:gtg=exists_top:ss=axioms_2978 on theBenchmark for (2978ds/359Mi) % 20.82/3.41 % (3656650)Instruction limit reached! % 20.82/3.41 % (3656650)------------------------------ % 20.82/3.41 % (3656650)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.82/3.41 % (3656650)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.82/3.41 % (3656650)CaDiCaL version: 2.1.3 % 20.82/3.41 % (3656650)Termination reason: Instruction limit % 20.82/3.41 % (3656650)Termination phase: Saturation % 20.82/3.41 % (3656650)Time elapsed: 0.172 s % 20.82/3.41 % (3656650)Peak memory usage: 92 MB % 20.82/3.41 % (3656650)Instructions burned: 513 (million) % 20.82/3.41 % (3656655)dis+1010_1_to=lpo:sil=128000:thi=all:fde=unused:si=on:sp=reverse_arity:tha=off:random_seed=2071719936:i=341:gtgl=2:rtra=on:gtg=exists_sym:ev=force:fsd=on:fsdmm=1_2978 on theBenchmark for (2978ds/341Mi) % 20.82/3.41 % (3656647)Instruction limit reached! % 20.82/3.41 % (3656647)------------------------------ % 22.62/3.76 % (3656647)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 22.62/3.76 % (3656647)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.62/3.76 % (3656647)CaDiCaL version: 2.1.3 % 22.62/3.76 % (3656647)Termination reason: Instruction limit % 22.62/3.76 % (3656647)Termination phase: Saturation % 22.62/3.76 % (3656647)Time elapsed: 0.244 s % 22.62/3.76 % (3656647)Peak memory usage: 120 MB % 22.62/3.76 % (3656647)Instructions burned: 388 (million) % 22.62/3.76 % (3656660)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=2676195211:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2977 on theBenchmark for (2977ds/273Mi) % 22.62/3.76 % (3656657)lrs-2_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_max:tha=off:random_seed=197525091:st=1.5:i=261:sd=1:kws=precedence:rtra=on:ss=axioms_2977 on theBenchmark for (2977ds/261Mi) % 22.62/3.76 % (3656658)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=351792410:s2pl=no:i=235:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2977 on theBenchmark for (2977ds/235Mi) % 22.62/3.76 % (3656651)Instruction limit reached! % 22.62/3.76 % (3656651)------------------------------ % 22.62/3.76 % (3656651)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 22.62/3.76 % (3656651)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.62/3.76 % (3656651)CaDiCaL version: 2.1.3 % 22.62/3.76 % (3656651)Termination reason: Instruction limit % 22.62/3.76 % (3656651)Termination phase: Saturation % 22.62/3.76 % (3656651)Time elapsed: 0.253 s % 22.62/3.76 % (3656651)Peak memory usage: 136 MB % 22.62/3.76 % (3656651)Instructions burned: 336 (million) % 22.62/3.76 % (3656662)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=4151611540:i=146:doe=on:rtra=on_2976 on theBenchmark for (2976ds/146Mi) % 22.62/3.76 % (3656660)Instruction limit reached! % 22.62/3.76 % (3656660)------------------------------ % 22.62/3.76 % (3656660)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 22.62/3.76 % (3656660)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.62/3.76 % (3656660)CaDiCaL version: 2.1.3 % 22.62/3.76 % (3656660)Termination reason: Instruction limit % 22.62/3.76 % (3656660)Termination phase: Saturation % 22.62/3.76 % (3656660)Time elapsed: 0.104 s % 22.62/3.76 % (3656660)Peak memory usage: 92 MB % 22.62/3.76 % (3656660)Instructions burned: 276 (million) % 22.62/3.76 % (3656654)Instruction limit reached! % 22.62/3.76 % (3656654)------------------------------ % 22.62/3.76 % (3656654)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 22.62/3.76 % (3656654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.62/3.76 % (3656654)CaDiCaL version: 2.1.3 % 22.62/3.76 % (3656654)Termination reason: Instruction limit % 22.62/3.76 % (3656654)Termination phase: Saturation % 22.62/3.76 % (3656654)Time elapsed: 0.236 s % 22.62/3.76 % (3656654)Peak memory usage: 91 MB % 22.62/3.76 % (3656654)Instructions burned: 360 (million) % 22.62/3.76 % (3656657)Instruction limit reached! % 22.62/3.76 % (3656657)------------------------------ % 22.62/3.76 % (3656657)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 22.62/3.76 % (3656657)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.62/3.76 % (3656657)CaDiCaL version: 2.1.3 % 22.62/3.76 % (3656657)Termination reason: Instruction limit % 22.62/3.76 % (3656657)Termination phase: Saturation % 22.62/3.76 % (3656657)Time elapsed: 0.155 s % 22.62/3.76 % (3656657)Peak memory usage: 117 MB % 22.62/3.76 % (3656657)Instructions burned: 261 (million) % 22.62/3.76 % (3656655)Instruction limit reached! % 22.62/3.76 % (3656655)------------------------------ % 22.62/3.76 % (3656655)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 22.62/3.76 % (3656655)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.62/3.76 % (3656655)CaDiCaL version: 2.1.3 % 22.62/3.76 % (3656655)Termination reason: Instruction limit % 22.62/3.76 % (3656655)Termination phase: Saturation % 22.62/3.76 % (3656655)Time elapsed: 0.231 s % 22.62/3.76 % (3656655)Peak memory usage: 120 MB % 22.62/3.76 % (3656655)Instructions burned: 342 (million) % 22.62/3.76 % (3656658)Instruction limit reached! % 22.62/3.76 % (3656658)------------------------------ % 22.62/3.76 % (3656658)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 22.62/3.76 % (3656658)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.84/4.24 % (3656658)CaDiCaL version: 2.1.3 % 26.84/4.24 % (3656658)Termination reason: Instruction limit % 26.84/4.24 % (3656658)Termination phase: Saturation % 26.84/4.24 % (3656658)Time elapsed: 0.149 s % 26.84/4.24 % (3656658)Peak memory usage: 118 MB % 26.84/4.24 % (3656658)Instructions burned: 235 (million) % 26.84/4.24 % (3656662)Instruction limit reached! % 26.84/4.24 % (3656662)------------------------------ % 26.84/4.24 % (3656662)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.84/4.24 % (3656662)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.84/4.24 % (3656662)CaDiCaL version: 2.1.3 % 26.84/4.24 % (3656662)Termination reason: Instruction limit % 26.84/4.24 % (3656662)Termination phase: Saturation % 26.84/4.24 % (3656662)Time elapsed: 0.099 s % 26.84/4.24 % (3656662)Peak memory usage: 90 MB % 26.84/4.24 % (3656662)Instructions burned: 147 (million) % 26.84/4.24 % (3656668)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=1068493873:avsq=on:i=276:avsqr=1,2:rtra=on_2975 on theBenchmark for (2975ds/276Mi) % 26.84/4.24 % (3656667)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=4165542906:i=4428:doe=on:fsr=off:rtra=on_2975 on theBenchmark for (2975ds/4428Mi) % 26.84/4.24 % (3656669)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=650381664:i=1052:rtra=on_2974 on theBenchmark for (2974ds/1052Mi) % 26.84/4.24 % (3656670)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=3381169376:i=655:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2974 on theBenchmark for (2974ds/655Mi) % 26.84/4.24 % (3656671)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=3232247949:st=5:i=1054:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2974 on theBenchmark for (2974ds/1054Mi) % 26.84/4.24 % (3656673)lrs-1002_1_to=kbo:sas=z3:si=on:norm_ineq=on:sos=on:tha=some:random_seed=1740329715:i=107:rtra=on_2974 on theBenchmark for (2974ds/107Mi) % 26.84/4.24 % (3656674)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=1531374741:s2a=on:i=450:doe=on:nm=32:rtra=on_2974 on theBenchmark for (2974ds/450Mi) % 26.84/4.24 % (3656668)Instruction limit reached! % 26.84/4.24 % (3656668)------------------------------ % 26.84/4.24 % (3656668)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.84/4.24 % (3656668)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.84/4.24 % (3656668)CaDiCaL version: 2.1.3 % 26.84/4.24 % (3656668)Termination reason: Instruction limit % 26.84/4.24 % (3656668)Termination phase: Saturation % 26.84/4.24 % (3656668)Time elapsed: 0.131 s % 26.84/4.24 % (3656668)Peak memory usage: 137 MB % 26.84/4.24 % (3656668)Instructions burned: 277 (million) % 26.84/4.24 % (3656673)Instruction limit reached! % 26.84/4.24 % (3656673)------------------------------ % 26.84/4.24 % (3656673)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.84/4.24 % (3656673)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.84/4.24 % (3656673)CaDiCaL version: 2.1.3 % 26.84/4.24 % (3656673)Termination reason: Instruction limit % 26.84/4.24 % (3656673)Termination phase: Saturation % 26.84/4.24 % (3656673)Time elapsed: 0.090 s % 26.84/4.24 % (3656673)Peak memory usage: 117 MB % 26.84/4.24 % (3656673)Instructions burned: 107 (million) % 26.84/4.24 % (3656681)WARNING Broken Constraint: if demodulation_redundancy_check(ordering) has been set then forward_demodulation(off) is not equal to off or backward_demodulation(off) is not equal to off or partial_redundancy_check(off) is not equal to off % 26.84/4.24 % (3656681)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=2161631313:i=1090:aac=none:nm=0:rtra=on:rawr=on_2973 on theBenchmark for (2973ds/1090Mi) % 26.84/4.24 % (3656682)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=3820796685:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2972 on theBenchmark for (2972ds/130Mi) % 26.84/4.24 % (3656682)Instruction limit reached! % 26.84/4.24 % (3656682)------------------------------ % 26.84/4.24 % (3656682)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.84/4.24 % (3656682)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.84/4.24 % (3656682)CaDiCaL version: 2.1.3 % 26.84/4.24 % (3656682)Termination reason: Instruction limit % 29.26/4.80 % (3656682)Termination phase: Saturation % 29.26/4.80 % (3656682)Time elapsed: 0.107 s % 29.26/4.80 % (3656682)Peak memory usage: 118 MB % 29.26/4.80 % (3656682)Instructions burned: 131 (million) % 29.26/4.80 % (3656674)Instruction limit reached! % 29.26/4.80 % (3656674)------------------------------ % 29.26/4.80 % (3656674)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.26/4.80 % (3656674)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.26/4.80 % (3656674)CaDiCaL version: 2.1.3 % 29.26/4.80 % (3656674)Termination reason: Instruction limit % 29.26/4.80 % (3656674)Termination phase: Saturation % 29.26/4.80 % (3656674)Time elapsed: 0.327 s % 29.26/4.80 % (3656674)Peak memory usage: 135 MB % 29.26/4.80 % (3656674)Instructions burned: 450 (million) % 29.26/4.80 % (3656670)Instruction limit reached! % 29.26/4.80 % (3656670)------------------------------ % 29.26/4.80 % (3656670)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.26/4.80 % (3656670)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.26/4.80 % (3656670)CaDiCaL version: 2.1.3 % 29.26/4.80 % (3656670)Termination reason: Instruction limit % 29.26/4.80 % (3656670)Termination phase: Saturation % 29.26/4.80 % (3656670)Time elapsed: 0.453 s % 29.26/4.80 % (3656670)Peak memory usage: 95 MB % 29.26/4.80 % (3656670)Instructions burned: 655 (million) % 29.26/4.80 % (3656686)ott+10_1_to=kbo:sil=64000:si=on:sp=reverse_frequency:sos=on:random_seed=3572858658:i=491:doe=on:rtra=on:gtg=position_2969 on theBenchmark for (2969ds/491Mi) % 29.26/4.80 % (3656685)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=891180252:i=312:kws=inv_frequency:nm=20:rtra=on_2969 on theBenchmark for (2969ds/312Mi) % 29.26/4.80 % (3656681)Instruction limit reached! % 29.26/4.80 % (3656681)------------------------------ % 29.26/4.80 % (3656681)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.26/4.80 % (3656681)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.26/4.80 % (3656681)CaDiCaL version: 2.1.3 % 29.26/4.80 % (3656681)Termination reason: Instruction limit % 29.26/4.80 % (3656681)Termination phase: Saturation % 29.26/4.80 % (3656681)Time elapsed: 0.373 s % 29.26/4.80 % (3656681)Peak memory usage: 124 MB % 29.26/4.80 % (3656681)Instructions burned: 1091 (million) % 29.26/4.80 % (3656687)ott+1011_4:1_to=lpo:sil=64000:si=on:spb=intro:random_seed=1597814233:s2a=on:i=835:s2at=2:rtra=on_2968 on theBenchmark for (2968ds/835Mi) % 29.26/4.80 % (3656690)ott+1011_2_to=lpo:sil=128000:si=on:sos=on:random_seed=1780226658:i=307:bd=preordered:av=off:rtra=on:ev=cautious_2968 on theBenchmark for (2968ds/307Mi) % 29.26/4.80 % (3656671)Instruction limit reached! % 29.26/4.80 % (3656671)------------------------------ % 29.26/4.80 % (3656671)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.26/4.80 % (3656671)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.26/4.80 % (3656671)CaDiCaL version: 2.1.3 % 29.26/4.80 % (3656671)Termination reason: Instruction limit % 29.26/4.80 % (3656671)Termination phase: Saturation % 29.26/4.80 % (3656671)Time elapsed: 0.631 s % 29.26/4.80 % (3656671)Peak memory usage: 96 MB % 29.26/4.80 % (3656671)Instructions burned: 1055 (million) % 29.26/4.80 % (3656669)Instruction limit reached! % 29.26/4.80 % (3656669)------------------------------ % 29.26/4.80 % (3656669)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.26/4.80 % (3656669)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.26/4.80 % (3656669)CaDiCaL version: 2.1.3 % 29.26/4.80 % (3656669)Termination reason: Instruction limit % 29.26/4.80 % (3656669)Termination phase: Saturation % 29.26/4.80 % (3656669)Time elapsed: 0.675 s % 29.26/4.80 % (3656669)Peak memory usage: 95 MB % 29.26/4.80 % (3656669)Instructions burned: 1052 (million) % 29.26/4.80 % (3656690)Instruction limit reached! % 29.26/4.80 % (3656690)------------------------------ % 29.26/4.80 % (3656690)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.26/4.80 % (3656690)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.26/4.80 % (3656690)CaDiCaL version: 2.1.3 % 29.26/4.80 % (3656690)Termination reason: Instruction limit % 29.26/4.80 % (3656690)Termination phase: Saturation % 29.26/4.80 % (3656690)Time elapsed: 0.094 s % 29.26/4.80 % (3656690)Peak memory usage: 91 MB % 29.26/4.80 % (3656690)Instructions burned: 308 (million) % 29.26/4.80 % (3656685)Instruction limit reached! % 29.26/4.80 % (3656685)------------------------------ % 29.26/4.80 % (3656685)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 35.72/5.66 % (3656685)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.72/5.66 % (3656685)CaDiCaL version: 2.1.3 % 35.72/5.66 % (3656685)Termination reason: Instruction limit % 35.72/5.66 % (3656685)Termination phase: Saturation % 35.72/5.66 % (3656685)Time elapsed: 0.223 s % 35.72/5.66 % (3656685)Peak memory usage: 119 MB % 35.72/5.66 % (3656685)Instructions burned: 313 (million) % 35.72/5.66 % (3656693)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=1277885755:i=776:doe=on:rtra=on_2967 on theBenchmark for (2967ds/776Mi) % 35.72/5.66 % (3656695)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=1895614084:thitd=on:cond=fast:i=784:nm=30:rtra=on:gtg=all:tac=axiom_2966 on theBenchmark for (2966ds/784Mi) % 35.72/5.66 % (3656686)Instruction limit reached! % 35.72/5.66 % (3656686)------------------------------ % 35.72/5.66 % (3656686)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 35.72/5.66 % (3656686)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.72/5.66 % (3656686)CaDiCaL version: 2.1.3 % 35.72/5.66 % (3656686)Termination reason: Instruction limit % 35.72/5.66 % (3656686)Termination phase: Saturation % 35.72/5.66 % (3656686)Time elapsed: 0.306 s % 35.72/5.66 % (3656686)Peak memory usage: 93 MB % 35.72/5.66 % (3656686)Instructions burned: 492 (million) % 35.72/5.66 % (3656694)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=1618275858:s2a=on:i=646:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2966 on theBenchmark for (2966ds/646Mi) % 35.72/5.66 % (3656696)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=3766499759:thitd=on:s2a=on:i=1131:add=on:canc=force:bd=all:rtra=on:tac=axiom:ev=off_2966 on theBenchmark for (2966ds/1131Mi) % 35.72/5.66 % (3656699)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=607325277:s2pl=no:i=246:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2965 on theBenchmark for (2965ds/246Mi) % 35.72/5.66 % (3656687)Instruction limit reached! % 35.72/5.66 % (3656687)------------------------------ % 35.72/5.66 % (3656687)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 35.72/5.66 % (3656687)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.72/5.66 % (3656687)CaDiCaL version: 2.1.3 % 35.72/5.66 % (3656687)Termination reason: Instruction limit % 35.72/5.66 % (3656687)Termination phase: Saturation % 35.72/5.66 % (3656687)Time elapsed: 0.483 s % 35.72/5.66 % (3656687)Peak memory usage: 95 MB % 35.72/5.66 % (3656687)Instructions burned: 837 (million) % 35.72/5.66 % (3656699)Instruction limit reached! % 35.72/5.66 % (3656699)------------------------------ % 35.72/5.66 % (3656699)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 35.72/5.66 % (3656699)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.72/5.66 % (3656699)CaDiCaL version: 2.1.3 % 35.72/5.66 % (3656699)Termination reason: Instruction limit % 35.72/5.66 % (3656699)Termination phase: Saturation % 35.72/5.66 % (3656699)Time elapsed: 0.152 s % 35.72/5.66 % (3656699)Peak memory usage: 119 MB % 35.72/5.66 % (3656699)Instructions burned: 247 (million) % 35.72/5.66 % (3656695)Instruction limit reached! % 35.72/5.66 % (3656695)------------------------------ % 35.72/5.66 % (3656695)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 35.72/5.66 % (3656695)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.72/5.66 % (3656695)CaDiCaL version: 2.1.3 % 35.72/5.66 % (3656695)Termination reason: Instruction limit % 35.72/5.66 % (3656695)Termination phase: Saturation % 35.72/5.66 % (3656695)Time elapsed: 0.318 s % 35.72/5.66 % (3656695)Peak memory usage: 123 MB % 35.72/5.66 % (3656695)Instructions burned: 785 (million) % 35.72/5.66 % (3656705)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=3916985348:i=102:nm=16:rtra=on_2962 on theBenchmark for (2962ds/102Mi) % 35.72/5.66 % (3656694)Instruction limit reached! % 35.72/5.66 % (3656694)------------------------------ % 35.72/5.66 % (3656694)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 35.72/5.66 % (3656694)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.72/5.66 % (3656694)CaDiCaL version: 2.1.3 % 35.72/5.66 % (3656694)Termination reason: Instruction limit % 35.72/5.66 % (3656694)Termination phase: Saturation % 48.84/7.37 % (3656694)Time elapsed: 0.385 s % 48.84/7.37 % (3656694)Peak memory usage: 139 MB % 48.84/7.37 % (3656694)Instructions burned: 648 (million) % 48.84/7.37 % (3656704)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=2894669162:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2962 on theBenchmark for (2962ds/273Mi) % 48.84/7.37 % (3656703)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=1951922068:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2962 on theBenchmark for (2962ds/775Mi) % 48.84/7.37 % (3656705)Instruction limit reached! % 48.84/7.37 % (3656705)------------------------------ % 48.84/7.37 % (3656705)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.84/7.37 % (3656705)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.84/7.37 % (3656705)CaDiCaL version: 2.1.3 % 48.84/7.37 % (3656705)Termination reason: Instruction limit % 48.84/7.37 % (3656705)Termination phase: Saturation % 48.84/7.37 % (3656705)Time elapsed: 0.036 s % 48.84/7.37 % (3656705)Peak memory usage: 89 MB % 48.84/7.37 % (3656705)Instructions burned: 104 (million) % 48.84/7.37 % (3656693)Instruction limit reached! % 48.84/7.37 % (3656693)------------------------------ % 48.84/7.37 % (3656693)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.84/7.37 % (3656693)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.84/7.37 % (3656693)CaDiCaL version: 2.1.3 % 48.84/7.37 % (3656693)Termination reason: Instruction limit % 48.84/7.37 % (3656693)Termination phase: Saturation % 48.84/7.37 % (3656693)Time elapsed: 0.507 s % 48.84/7.37 % (3656693)Peak memory usage: 124 MB % 48.84/7.37 % (3656693)Instructions burned: 777 (million) % 48.84/7.37 % (3656710)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=1188639048:i=6400:doe=on:fsr=off:rtra=on_2961 on theBenchmark for (2961ds/6400Mi) % 48.84/7.37 % (3656707)lrs+10_1_to=lpo:sil=128000:si=on:bsr=unit_only:tha=off:random_seed=1367679037:avsq=on:s2a=on:i=1094:s2at=5:avsqr=4463,131072:rtra=on_2961 on theBenchmark for (2961ds/1094Mi) % 48.84/7.37 % (3656704)Instruction limit reached! % 48.84/7.37 % (3656704)------------------------------ % 48.84/7.37 % (3656704)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.84/7.37 % (3656704)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.84/7.37 % (3656704)CaDiCaL version: 2.1.3 % 48.84/7.37 % (3656704)Termination reason: Instruction limit % 48.84/7.37 % (3656704)Termination phase: Saturation % 48.84/7.37 % (3656704)Time elapsed: 0.184 s % 48.84/7.37 % (3656704)Peak memory usage: 92 MB % 48.84/7.37 % (3656704)Instructions burned: 273 (million) % 48.84/7.37 % (3656711)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=3442495777:i=868:doe=on:nm=0:rtra=on:gtg=exists_sym_2960 on theBenchmark for (2960ds/868Mi) % 48.84/7.37 % (3656714)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=2588440954:i=1846:canc=cautious:fsr=off:rtra=on_2959 on theBenchmark for (2959ds/1846Mi) % 48.84/7.37 % (3656696)Instruction limit reached! % 48.84/7.37 % (3656696)------------------------------ % 48.84/7.37 % (3656696)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.84/7.37 % (3656696)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.84/7.37 % (3656696)CaDiCaL version: 2.1.3 % 48.84/7.37 % (3656696)Termination reason: Instruction limit % 48.84/7.37 % (3656696)Termination phase: Saturation % 48.84/7.37 % (3656696)Time elapsed: 0.753 s % 48.84/7.37 % (3656696)Peak memory usage: 123 MB % 48.84/7.37 % (3656696)Instructions burned: 1132 (million) % 48.84/7.37 % (3656703)Instruction limit reached! % 48.84/7.37 % (3656703)------------------------------ % 48.84/7.37 % (3656703)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.84/7.37 % (3656703)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.84/7.37 % (3656703)CaDiCaL version: 2.1.3 % 48.84/7.37 % (3656703)Termination reason: Instruction limit % 48.84/7.37 % (3656703)Termination phase: Saturation % 48.84/7.37 % (3656703)Time elapsed: 0.515 s % 48.84/7.37 % (3656703)Peak memory usage: 95 MB % 48.84/7.37 % (3656703)Instructions burned: 775 (million) % 48.84/7.37 % (3656717)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=891497432:s2a=on:i=36816:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2957 on theBenchmark for (2957ds/36816Mi) % 56.76/8.53 % (3656711)Instruction limit reached! % 56.76/8.53 % (3656711)------------------------------ % 56.76/8.53 % (3656711)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 56.76/8.53 % (3656711)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.76/8.53 % (3656711)CaDiCaL version: 2.1.3 % 56.76/8.53 % (3656711)Termination reason: Instruction limit % 56.76/8.53 % (3656711)Termination phase: Saturation % 56.76/8.53 % (3656711)Time elapsed: 0.439 s % 56.76/8.53 % (3656711)Peak memory usage: 120 MB % 56.76/8.53 % (3656711)Instructions burned: 870 (million) % 56.76/8.53 % (3656718)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=23594947:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2956 on theBenchmark for (2956ds/273Mi) % 56.76/8.53 % (3656707)Instruction limit reached! % 56.76/8.53 % (3656707)------------------------------ % 56.76/8.53 % (3656707)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 56.76/8.53 % (3656707)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.76/8.53 % (3656707)CaDiCaL version: 2.1.3 % 56.76/8.53 % (3656707)Termination reason: Instruction limit % 56.76/8.53 % (3656707)Termination phase: Saturation % 56.76/8.53 % (3656707)Time elapsed: 0.622 s % 56.76/8.53 % (3656707)Peak memory usage: 94 MB % 56.76/8.53 % (3656707)Instructions burned: 1094 (million) % 56.76/8.53 % (3656720)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=3591646495:i=863:doe=on:nm=0:rtra=on:gtg=exists_sym_2955 on theBenchmark for (2955ds/863Mi) % 56.76/8.53 % (3656718)Instruction limit reached! % 56.76/8.53 % (3656718)------------------------------ % 56.76/8.53 % (3656718)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 56.76/8.53 % (3656718)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.76/8.53 % (3656718)CaDiCaL version: 2.1.3 % 56.76/8.53 % (3656718)Termination reason: Instruction limit % 56.76/8.53 % (3656718)Termination phase: Saturation % 56.76/8.53 % (3656718)Time elapsed: 0.213 s % 56.76/8.53 % (3656718)Peak memory usage: 92 MB % 56.76/8.53 % (3656718)Instructions burned: 275 (million) % 56.76/8.53 % (3656722)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=466397614:i=5811:kws=precedence:nm=0:rtra=on_2954 on theBenchmark for (2954ds/5811Mi) % 56.76/8.53 % (3656724)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=1567584880:i=2216:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2952 on theBenchmark for (2952ds/2216Mi) % 56.76/8.53 % (3656720)Instruction limit reached! % 56.76/8.53 % (3656720)------------------------------ % 56.76/8.53 % (3656720)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 56.76/8.53 % (3656720)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.76/8.53 % (3656720)CaDiCaL version: 2.1.3 % 56.76/8.53 % (3656720)Termination reason: Instruction limit % 56.76/8.53 % (3656720)Termination phase: Saturation % 56.76/8.53 % (3656720)Time elapsed: 0.415 s % 56.76/8.53 % (3656720)Peak memory usage: 119 MB % 56.76/8.53 % (3656720)Instructions burned: 865 (million) % 56.76/8.53 % (3656667)Instruction limit reached! % 56.76/8.53 % (3656667)------------------------------ % 56.76/8.53 % (3656667)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 56.76/8.53 % (3656667)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.76/8.53 % (3656667)CaDiCaL version: 2.1.3 % 56.76/8.53 % (3656667)Termination reason: Instruction limit % 56.76/8.53 % (3656667)Termination phase: Saturation % 56.76/8.53 % (3656667)Time elapsed: 2.573 s % 56.76/8.53 % (3656667)Peak memory usage: 115 MB % 56.76/8.53 % (3656667)Instructions burned: 4429 (million) % 56.76/8.53 % (3656727)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=1102521213:i=801:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2949 on theBenchmark for (2949ds/801Mi) % 56.76/8.53 % (3656714)Instruction limit reached! % 56.76/8.53 % (3656714)------------------------------ % 56.76/8.53 % (3656714)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 56.76/8.53 % (3656714)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.76/8.53 % (3656714)CaDiCaL version: 2.1.3 % 56.76/8.53 % (3656714)Termination reason: Instruction limit % 56.76/8.53 % (3656714)Termination phase: Saturation % 56.76/8.53 % (3656714)Time elapsed: 1.077 s % 94.39/13.74 % (3656714)Peak memory usage: 99 MB % 94.39/13.74 % (3656714)Instructions burned: 1846 (million) % 94.39/13.74 % (3656729)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=231594542:st=5:i=1026:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2948 on theBenchmark for (2948ds/1026Mi) % 94.39/13.74 % (3656730)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=3342854348:i=3509:rtra=on_2947 on theBenchmark for (2947ds/3509Mi) % 94.39/13.74 % (3656727)Instruction limit reached! % 94.39/13.74 % (3656727)------------------------------ % 94.39/13.74 % (3656727)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 94.39/13.74 % (3656727)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 94.39/13.74 % (3656727)CaDiCaL version: 2.1.3 % 94.39/13.74 % (3656727)Termination reason: Instruction limit % 94.39/13.74 % (3656727)Termination phase: Saturation % 94.39/13.74 % (3656727)Time elapsed: 0.570 s % 94.39/13.74 % (3656727)Peak memory usage: 98 MB % 94.39/13.74 % (3656727)Instructions burned: 802 (million) % 94.39/13.74 % (3656733)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=2649028026:st=2:i=2127:sd=12:ep=R:rtra=on:ss=axioms_2942 on theBenchmark for (2942ds/2127Mi) % 94.39/13.74 % (3656724)Instruction limit reached! % 94.39/13.74 % (3656724)------------------------------ % 94.39/13.74 % (3656724)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 94.39/13.74 % (3656724)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 94.39/13.74 % (3656724)CaDiCaL version: 2.1.3 % 94.39/13.74 % (3656724)Termination reason: Instruction limit % 94.39/13.74 % (3656724)Termination phase: Saturation % 94.39/13.74 % (3656724)Time elapsed: 1.038 s % 94.39/13.74 % (3656724)Peak memory usage: 121 MB % 94.39/13.74 % (3656724)Instructions burned: 2217 (million) % 94.39/13.74 % (3656729)Instruction limit reached! % 94.39/13.74 % (3656729)------------------------------ % 94.39/13.74 % (3656729)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 94.39/13.74 % (3656729)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 94.39/13.74 % (3656729)CaDiCaL version: 2.1.3 % 94.39/13.74 % (3656729)Termination reason: Instruction limit % 94.39/13.74 % (3656729)Termination phase: Saturation % 94.39/13.74 % (3656729)Time elapsed: 0.614 s % 94.39/13.74 % (3656729)Peak memory usage: 96 MB % 94.39/13.74 % (3656729)Instructions burned: 1026 (million) % 94.39/13.74 % (3656710)Instruction limit reached! % 94.39/13.74 % (3656710)------------------------------ % 94.39/13.74 % (3656710)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 94.39/13.74 % (3656710)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 94.39/13.74 % (3656710)CaDiCaL version: 2.1.3 % 94.39/13.74 % (3656710)Termination reason: Instruction limit % 94.39/13.74 % (3656710)Termination phase: Saturation % 94.39/13.74 % (3656710)Time elapsed: 2.018 s % 94.39/13.74 % (3656710)Peak memory usage: 126 MB % 94.39/13.74 % (3656710)Instructions burned: 6402 (million) % 94.39/13.74 % (3656735)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=1592446319:i=1959:rtra=on:fsd=on:proc=on_2941 on theBenchmark for (2941ds/1959Mi) % 94.39/13.74 % (3656736)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=1145272168:s2a=on:i=3553:nm=0:rtra=on_2940 on theBenchmark for (2940ds/3553Mi) % 94.39/13.74 % (3656737)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=3299315570:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2940 on theBenchmark for (2940ds/3201Mi) % 94.39/13.74 % (3656737)Instruction limit reached! % 94.39/13.74 % (3656737)------------------------------ % 94.39/13.74 % (3656737)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 94.39/13.74 % (3656737)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 94.39/13.74 % (3656737)CaDiCaL version: 2.1.3 % 94.39/13.74 % (3656737)Termination reason: Instruction limit % 94.39/13.74 % (3656737)Termination phase: Saturation % 94.39/13.74 % (3656737)Time elapsed: 0.723 s % 94.39/13.74 % (3656737)Peak memory usage: 93 MB % 94.39/13.74 % (3656737)Instructions burned: 3206 (million) % 94.39/13.74 % (3656741)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=2898977296:thitd=on:cond=on:i=4093:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2932 on theBenchmark for (2932ds/4093Mi) % 94.39/13.74 % (3656735)Instruction limit reached! % 94.39/13.74 % (3656735)------------------------------ % 112.85/16.34 % (3656735)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 112.85/16.34 % (3656735)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.85/16.34 % (3656735)CaDiCaL version: 2.1.3 % 112.85/16.34 % (3656735)Termination reason: Instruction limit % 112.85/16.34 % (3656735)Termination phase: Saturation % 112.85/16.34 % (3656735)Time elapsed: 0.928 s % 112.85/16.34 % (3656735)Peak memory usage: 121 MB % 112.85/16.34 % (3656735)Instructions burned: 1961 (million) % 112.85/16.34 % (3656733)Instruction limit reached! % 112.85/16.34 % (3656733)------------------------------ % 112.85/16.34 % (3656733)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 112.85/16.34 % (3656733)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.85/16.34 % (3656733)CaDiCaL version: 2.1.3 % 112.85/16.34 % (3656733)Termination reason: Instruction limit % 112.85/16.34 % (3656733)Termination phase: Saturation % 112.85/16.34 % (3656733)Time elapsed: 1.124 s % 112.85/16.34 % (3656733)Peak memory usage: 103 MB % 112.85/16.34 % (3656733)Instructions burned: 2128 (million) % 112.85/16.34 % (3656743)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=270963623:cond=fast:i=21173:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2930 on theBenchmark for (2930ds/21173Mi) % 112.85/16.34 % (3656744)lrs+11_1_to=lpo:thi=all:sas=z3:si=on:fd=off:sac=on:slsq=on:random_seed=3076359963:avsq=on:i=10544:avsqr=17,4:canc=force:rtra=on:gtg=exists_top:er=filter_2930 on theBenchmark for (2930ds/10544Mi) % 112.85/16.34 % (3656730)Instruction limit reached! % 112.85/16.34 % (3656730)------------------------------ % 112.85/16.34 % (3656730)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 112.85/16.34 % (3656730)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.85/16.34 % (3656730)CaDiCaL version: 2.1.3 % 112.85/16.34 % (3656730)Termination reason: Instruction limit % 112.85/16.34 % (3656730)Termination phase: Saturation % 112.85/16.34 % (3656730)Time elapsed: 2.306 s % 112.85/16.34 % (3656730)Peak memory usage: 110 MB % 112.85/16.34 % (3656730)Instructions burned: 3510 (million) % 112.85/16.34 % (3656747)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=3243751616:avsq=on:i=1262:avsqr=1,16:rtra=on:rawr=on_2923 on theBenchmark for (2923ds/1262Mi) % 112.85/16.34 % (3656722)Instruction limit reached! % 112.85/16.34 % (3656722)------------------------------ % 112.85/16.34 % (3656722)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 112.85/16.34 % (3656722)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.85/16.34 % (3656722)CaDiCaL version: 2.1.3 % 112.85/16.34 % (3656722)Termination reason: Instruction limit % 112.85/16.34 % (3656722)Termination phase: Saturation % 112.85/16.34 % (3656722)Time elapsed: 3.173 s % 112.85/16.34 % (3656722)Peak memory usage: 133 MB % 112.85/16.34 % (3656722)Instructions burned: 5812 (million) % 112.85/16.34 % (3656741)Instruction limit reached! % 112.85/16.34 % (3656741)------------------------------ % 112.85/16.34 % (3656741)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 112.85/16.34 % (3656741)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.85/16.34 % (3656741)CaDiCaL version: 2.1.3 % 112.85/16.34 % (3656741)Termination reason: Instruction limit % 112.85/16.34 % (3656741)Termination phase: Saturation % 112.85/16.34 % (3656741)Time elapsed: 1.061 s % 112.85/16.34 % (3656741)Peak memory usage: 141 MB % 112.85/16.34 % (3656741)Instructions burned: 4097 (million) % 112.85/16.34 % (3656750)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=1110312832:i=270:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2920 on theBenchmark for (2920ds/270Mi) % 112.85/16.34 % (3656749)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=1835720824:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2920 on theBenchmark for (2920ds/775Mi) % 112.85/16.34 % (3656750)Instruction limit reached! % 112.85/16.34 % (3656750)------------------------------ % 112.85/16.34 % (3656750)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 112.85/16.34 % (3656750)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.85/16.34 % (3656750)CaDiCaL version: 2.1.3 % 112.85/16.34 % (3656750)Termination reason: Instruction limit % 112.85/16.34 % (3656750)Termination phase: Saturation % 112.85/16.34 % (3656750)Time elapsed: 0.102 s % 112.85/16.34 % (3656750)Peak memory usage: 92 MB % 112.85/16.34 % (3656750)Instructions burned: 272 (million) % 134.89/19.41 % (3656753)ott+10_128_isp=bottom:to=lpo:sil=128000:si=on:urr=on:uwa=alasca_main:sac=on:slsq=on:random_seed=869475229:i=17165:aac=none:doe=on:rtra=on:gtg=exists_all_2918 on theBenchmark for (2918ds/17165Mi) % 134.89/19.41 % (3656747)Instruction limit reached! % 134.89/19.41 % (3656747)------------------------------ % 134.89/19.41 % (3656747)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 134.89/19.41 % (3656747)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 134.89/19.41 % (3656747)CaDiCaL version: 2.1.3 % 134.89/19.41 % (3656747)Termination reason: Instruction limit % 134.89/19.41 % (3656747)Termination phase: Saturation % 134.89/19.41 % (3656747)Time elapsed: 0.666 s % 134.89/19.41 % (3656747)Peak memory usage: 123 MB % 134.89/19.41 % (3656747)Instructions burned: 1263 (million) % 134.89/19.41 % (3656736)Instruction limit reached! % 134.89/19.41 % (3656736)------------------------------ % 134.89/19.41 % (3656736)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 134.89/19.41 % (3656736)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 134.89/19.41 % (3656736)CaDiCaL version: 2.1.3 % 134.89/19.41 % (3656736)Termination reason: Instruction limit % 134.89/19.41 % (3656736)Termination phase: Saturation % 134.89/19.41 % (3656736)Time elapsed: 2.456 s % 134.89/19.41 % (3656736)Peak memory usage: 106 MB % 134.89/19.41 % (3656736)Instructions burned: 3553 (million) % 134.89/19.41 % (3656749)Instruction limit reached! % 134.89/19.41 % (3656749)------------------------------ % 134.89/19.41 % (3656749)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 134.89/19.41 % (3656749)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 134.89/19.41 % (3656749)CaDiCaL version: 2.1.3 % 134.89/19.41 % (3656749)Termination reason: Instruction limit % 134.89/19.41 % (3656749)Termination phase: Saturation % 134.89/19.41 % (3656749)Time elapsed: 0.513 s % 134.89/19.41 % (3656749)Peak memory usage: 95 MB % 134.89/19.41 % (3656749)Instructions burned: 775 (million) % 134.89/19.41 % (3656755)lrs+2_10_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_main:tha=some:random_seed=2121623402:s2a=on:i=13094:s2at=-1:rtra=on_2915 on theBenchmark for (2915ds/13094Mi) % 134.89/19.41 % (3656756)lrs+10_1_to=lpo:sil=128000:si=on:sp=occurrence:random_seed=1986770466:st=2:i=12633:rtra=on:ss=axioms_2914 on theBenchmark for (2914ds/12633Mi) % 134.89/19.41 % (3656757)dis+1011_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_frequency:lsd=20:nwc=3:random_seed=2068721365:i=1783:rtra=on:gtg=position_2914 on theBenchmark for (2914ds/1783Mi) % 134.89/19.41 % (3656757)Instruction limit reached! % 134.89/19.41 % (3656757)------------------------------ % 134.89/19.41 % (3656757)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 134.89/19.41 % (3656757)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 134.89/19.41 % (3656757)CaDiCaL version: 2.1.3 % 134.89/19.41 % (3656757)Termination reason: Instruction limit % 134.89/19.41 % (3656757)Termination phase: Saturation % 134.89/19.41 % (3656757)Time elapsed: 0.963 s % 134.89/19.41 % (3656757)Peak memory usage: 124 MB % 134.89/19.41 % (3656757)Instructions burned: 1783 (million) % 134.89/19.41 % (3656761)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=3098467026:i=5451:aac=none:doe=on:nm=0:rtra=on:amm=off:gtg=position_2903 on theBenchmark for (2903ds/5451Mi) % 134.89/19.41 % (3656761)Instruction limit reached! % 134.89/19.41 % (3656761)------------------------------ % 134.89/19.41 % (3656761)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 134.89/19.41 % (3656761)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 134.89/19.41 % (3656761)CaDiCaL version: 2.1.3 % 134.89/19.41 % (3656761)Termination reason: Instruction limit % 134.89/19.41 % (3656761)Termination phase: Saturation % 134.89/19.41 % (3656761)Time elapsed: 2.656 s % 134.89/19.41 % (3656761)Peak memory usage: 127 MB % 134.89/19.41 % (3656761)Instructions burned: 5451 (million) % 134.89/19.41 % (3656763)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=3418935600:i=4975:doe=on:nm=0:rtra=on:gtg=exists_sym_2875 on theBenchmark for (2875ds/4975Mi) % 134.89/19.41 % (3656753)Instruction limit reached! % 134.89/19.41 % (3656753)------------------------------ % 134.89/19.41 % (3656753)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 134.89/19.41 % (3656753)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 134.89/19.41 % (3656753)CaDiCaL version: 2.1.3 % 180.35/25.87 % (3656753)Termination reason: Instruction limit % 180.35/25.87 % (3656753)Termination phase: Saturation % 180.35/25.87 % (3656753)Time elapsed: 5.123 s % 180.35/25.87 % (3656753)Peak memory usage: 198 MB % 180.35/25.87 % (3656753)Instructions burned: 17168 (million) % 180.35/25.87 % (3656765)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=2665131549:i=2076:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2866 on theBenchmark for (2866ds/2076Mi) % 180.35/25.87 % (3656744)Instruction limit reached! % 180.35/25.87 % (3656744)------------------------------ % 180.35/25.87 % (3656744)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 180.35/25.87 % (3656744)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.35/25.87 % (3656744)CaDiCaL version: 2.1.3 % 180.35/25.87 % (3656744)Termination reason: Instruction limit % 180.35/25.87 % (3656744)Termination phase: Saturation % 180.35/25.87 % (3656744)Time elapsed: 6.573 s % 180.35/25.87 % (3656744)Peak memory usage: 201 MB % 180.35/25.87 % (3656744)Instructions burned: 10545 (million) % 180.35/25.87 % (3656769)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=3042128362:i=5145:rtra=on_2862 on theBenchmark for (2862ds/5145Mi) % 180.35/25.87 % (3656765)Instruction limit reached! % 180.35/25.87 % (3656765)------------------------------ % 180.35/25.87 % (3656765)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 180.35/25.87 % (3656765)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.35/25.87 % (3656765)CaDiCaL version: 2.1.3 % 180.35/25.87 % (3656765)Termination reason: Instruction limit % 180.35/25.87 % (3656765)Termination phase: Saturation % 180.35/25.87 % (3656765)Time elapsed: 0.521 s % 180.35/25.87 % (3656765)Peak memory usage: 121 MB % 180.35/25.87 % (3656765)Instructions burned: 2077 (million) % 180.35/25.87 % (3656771)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=267113809:i=3509:rtra=on_2860 on theBenchmark for (2860ds/3509Mi) % 180.35/25.87 % (3656763)Instruction limit reached! % 180.35/25.87 % (3656763)------------------------------ % 180.35/25.87 % (3656763)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 180.35/25.87 % (3656763)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.35/25.87 % (3656763)CaDiCaL version: 2.1.3 % 180.35/25.87 % (3656763)Termination reason: Instruction limit % 180.35/25.87 % (3656763)Termination phase: Saturation % 180.35/25.87 % (3656763)Time elapsed: 2.330 s % 180.35/25.87 % (3656763)Peak memory usage: 124 MB % 180.35/25.87 % (3656763)Instructions burned: 4975 (million) % 180.35/25.87 % (3656833)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=501058050:st=2:i=13800:sd=12:ep=R:rtra=on:ss=axioms_2850 on theBenchmark for (2850ds/13800Mi) % 180.35/25.87 % (3656771)Instruction limit reached! % 180.35/25.87 % (3656771)------------------------------ % 180.35/25.87 % (3656771)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 180.35/25.87 % (3656771)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.35/25.87 % (3656771)CaDiCaL version: 2.1.3 % 180.35/25.87 % (3656771)Termination reason: Instruction limit % 180.35/25.87 % (3656771)Termination phase: Saturation % 180.35/25.87 % (3656771)Time elapsed: 1.224 s % 180.35/25.87 % (3656771)Peak memory usage: 108 MB % 180.35/25.87 % (3656771)Instructions burned: 3511 (million) % 180.35/25.87 % (3656835)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=1500263353:i=1412:rtra=on:fsd=on:proc=on_2847 on theBenchmark for (2847ds/1412Mi) % 180.35/25.87 % (3656835)Instruction limit reached! % 180.35/25.87 % (3656835)------------------------------ % 180.35/25.87 % (3656835)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 180.35/25.87 % (3656835)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.35/25.87 % (3656835)CaDiCaL version: 2.1.3 % 180.35/25.87 % (3656835)Termination reason: Instruction limit % 180.35/25.87 % (3656835)Termination phase: Saturation % 180.35/25.87 % (3656835)Time elapsed: 0.469 s % 180.35/25.87 % (3656835)Peak memory usage: 126 MB % 180.35/25.87 % (3656835)Instructions burned: 1413 (million) % 180.35/25.87 % (3656837)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 % 180.35/25.87 % (3656837)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=2436177347:i=11747:aac=none:nm=0:rtra=on:rawr=on_2841 on theBenchmark for (2841ds/11747Mi) % 223.42/31.94 % (3656755)Instruction limit reached! % 223.42/31.94 % (3656755)------------------------------ % 223.42/31.94 % (3656755)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 223.42/31.94 % (3656755)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 223.42/31.94 % (3656755)CaDiCaL version: 2.1.3 % 223.42/31.94 % (3656755)Termination reason: Instruction limit % 223.42/31.94 % (3656755)Termination phase: Saturation % 223.42/31.94 % (3656755)Time elapsed: 7.979 s % 223.42/31.94 % (3656755)Peak memory usage: 152 MB % 223.42/31.94 % (3656755)Instructions burned: 13095 (million) % 223.42/31.94 % (3656839)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=665163423:s2a=on:i=3553:nm=0:rtra=on_2834 on theBenchmark for (2834ds/3553Mi) % 223.42/31.94 % (3656756)Instruction limit reached! % 223.42/31.94 % (3656756)------------------------------ % 223.42/31.94 % (3656756)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 223.42/31.94 % (3656756)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 223.42/31.94 % (3656756)CaDiCaL version: 2.1.3 % 223.42/31.94 % (3656756)Termination reason: Instruction limit % 223.42/31.94 % (3656756)Termination phase: Saturation % 223.42/31.94 % (3656756)Time elapsed: 8.162 s % 223.42/31.94 % (3656756)Peak memory usage: 138 MB % 223.42/31.94 % (3656756)Instructions burned: 12635 (million) % 223.42/31.94 % (3656841)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=1352401649:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2832 on theBenchmark for (2832ds/3201Mi) % 223.42/31.94 % (3656769)Instruction limit reached! % 223.42/31.94 % (3656769)------------------------------ % 223.42/31.94 % (3656769)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 223.42/31.94 % (3656769)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 223.42/31.94 % (3656769)CaDiCaL version: 2.1.3 % 223.42/31.94 % (3656769)Termination reason: Instruction limit % 223.42/31.94 % (3656769)Termination phase: Saturation % 223.42/31.94 % (3656769)Time elapsed: 3.162 s % 223.42/31.94 % (3656769)Peak memory usage: 114 MB % 223.42/31.94 % (3656769)Instructions burned: 5146 (million) % 223.42/31.94 % (3656843)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=1983417170:thitd=on:cond=on:i=4081:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2830 on theBenchmark for (2830ds/4081Mi) % 223.42/31.94 % (3656743)Instruction limit reached! % 223.42/31.94 % (3656743)------------------------------ % 223.42/31.94 % (3656743)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 223.42/31.94 % (3656743)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 223.42/31.94 % (3656743)CaDiCaL version: 2.1.3 % 223.42/31.94 % (3656743)Termination reason: Instruction limit % 223.42/31.94 % (3656743)Termination phase: Saturation % 223.42/31.94 % (3656743)Time elapsed: 10.490 s % 223.42/31.94 % (3656743)Peak memory usage: 177 MB % 223.42/31.94 % (3656743)Instructions burned: 21181 (million) % 223.42/31.94 % (3656845)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=3350374540:cond=fast:i=20260:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2823 on theBenchmark for (2823ds/20260Mi) % 223.42/31.94 % (3656841)Instruction limit reached! % 223.42/31.94 % (3656841)------------------------------ % 223.42/31.94 % (3656841)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 223.42/31.94 % (3656841)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 223.42/31.94 % (3656841)CaDiCaL version: 2.1.3 % 223.42/31.94 % (3656841)Termination reason: Instruction limit % 223.42/31.94 % (3656841)Termination phase: Saturation % 223.42/31.94 % (3656841)Time elapsed: 1.377 s % 223.42/31.94 % (3656841)Peak memory usage: 93 MB % 223.42/31.94 % (3656841)Instructions burned: 3202 (million) % 223.42/31.94 % (3656848)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=2629346501:s2a=on:i=58627:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2817 on theBenchmark for (2817ds/58627Mi) % 223.42/31.94 % (3656837)Instruction limit reached! % 223.42/31.94 % (3656837)------------------------------ % 223.42/31.94 % (3656837)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 223.42/31.94 % (3656837)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 223.42/31.94 % (3656837)CaDiCaL version: 2.1.3 % 223.42/31.94 % (3656837)Termination reason: Instruction limit % 296.57/42.24 % (3656837)Termination phase: Saturation % 296.57/42.24 % (3656837)Time elapsed: 3.061 s % 296.57/42.24 % (3656837)Peak memory usage: 143 MB % 296.57/42.24 % (3656837)Instructions burned: 11749 (million) % 296.57/42.24 % (3656843)Instruction limit reached! % 296.57/42.24 % (3656843)------------------------------ % 296.57/42.24 % (3656843)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 296.57/42.24 % (3656843)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 296.57/42.24 % (3656843)CaDiCaL version: 2.1.3 % 296.57/42.24 % (3656843)Termination reason: Instruction limit % 296.57/42.24 % (3656843)Termination phase: Saturation % 296.57/42.24 % (3656843)Time elapsed: 1.922 s % 296.57/42.24 % (3656843)Peak memory usage: 141 MB % 296.57/42.24 % (3656843)Instructions burned: 4082 (million) % 296.57/42.24 % (3656850)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=4172458383:avsq=on:i=6258:avsqr=1,16:rtra=on:rawr=on_2810 on theBenchmark for (2810ds/6258Mi) % 296.57/42.24 % (3656851)ott+10_128_isp=bottom:to=lpo:sil=128000:si=on:urr=on:uwa=alasca_main:sac=on:slsq=on:random_seed=2496654209:i=34001:aac=none:doe=on:rtra=on:gtg=exists_all_2809 on theBenchmark for (2809ds/34001Mi) % 296.57/42.24 % (3656839)Instruction limit reached! % 296.57/42.24 % (3656839)------------------------------ % 296.57/42.24 % (3656839)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 296.57/42.24 % (3656839)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 296.57/42.24 % (3656839)CaDiCaL version: 2.1.3 % 296.57/42.24 % (3656839)Termination reason: Instruction limit % 296.57/42.24 % (3656839)Termination phase: Saturation % 296.57/42.24 % (3656839)Time elapsed: 2.469 s % 296.57/42.24 % (3656839)Peak memory usage: 105 MB % 296.57/42.24 % (3656839)Instructions burned: 3553 (million) % 296.57/42.24 % (3656854)lrs+2_10_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_main:tha=some:random_seed=842126665:s2a=on:i=71622:s2at=-1:rtra=on_2808 on theBenchmark for (2808ds/71622Mi) % 296.57/42.24 % (3656850)Instruction limit reached! % 296.57/42.24 % (3656850)------------------------------ % 296.57/42.24 % (3656850)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 296.57/42.24 % (3656850)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 296.57/42.24 % (3656850)CaDiCaL version: 2.1.3 % 296.57/42.24 % (3656850)Termination reason: Instruction limit % 296.57/42.24 % (3656850)Termination phase: Saturation % 296.57/42.24 % (3656850)Time elapsed: 1.500 s % 296.57/42.24 % (3656850)Peak memory usage: 126 MB % 296.57/42.24 % (3656850)Instructions burned: 6261 (million) % 296.57/42.24 % (3656856)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=636648475:i=24001:kws=precedence:nm=0:rtra=on_2794 on theBenchmark for (2794ds/24001Mi) % 296.57/42.24 % (3656833)Instruction limit reached! % 296.57/42.24 % (3656833)------------------------------ % 296.57/42.24 % (3656833)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 296.57/42.24 % (3656833)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 296.57/42.24 % (3656833)CaDiCaL version: 2.1.3 % 296.57/42.24 % (3656833)Termination reason: Instruction limit % 296.57/42.24 % (3656833)Termination phase: Saturation % 296.57/42.24 % (3656833)Time elapsed: 7.687 s % 296.57/42.24 % (3656833)Peak memory usage: 164 MB % 296.57/42.24 % (3656833)Instructions burned: 13801 (million) % 296.57/42.24 % (3656858)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=2359456093:i=2076:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2772 on theBenchmark for (2772ds/2076Mi) % 296.57/42.24 % (3656858)Instruction limit reached! % 296.57/42.24 % (3656858)------------------------------ % 296.57/42.24 % (3656858)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 296.57/42.24 % (3656858)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 296.57/42.24 % (3656858)CaDiCaL version: 2.1.3 % 296.57/42.24 % (3656858)Termination reason: Instruction limit % 296.57/42.24 % (3656858)Termination phase: Saturation % 296.57/42.24 % (3656858)Time elapsed: 1.001 s % 296.57/42.24 % (3656858)Peak memory usage: 121 MB % 296.57/42.24 % (3656858)Instructions burned: 2078 (million) % 296.57/42.24 % (3656860)dis+21_20_to=lakbo:si=on:alasca=on:sp=const_max:uwa=alasca_main:sac=on:random_seed=385047318:s2a=on:i=83971:s2at=4:bd=all:ins=1:rtra=on_2761 on theBenchmark for (2761ds/83971Mi) % 296.57/42.24 % (3656717)Instruction limit reached! % 296.57/42.24 % (3656717)------------------------------ % 296.57/42.24 % (3656717)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.14/42.93 % (3656717)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.14/42.93 % (3656717)CaDiCaL version: 2.1.3 % 300.14/42.93 % (3656717)Termination reason: Instruction limit % 300.14/42.93 % (3656717)Termination phase: Saturation % 300.14/42.93 % (3656717)Time elapsed: 21.067 s % 300.14/42.93 % (3656717)Peak memory usage: 207 MB % 300.14/42.93 % (3656717)Instructions burned: 36818 (million) % 300.14/42.93 % (3656862)lrs+1011_5:1_to=lpo:sil=128000:sas=z3:si=on:norm_ineq=on:tha=some:random_seed=173532899:i=83944:rtra=on_2745 on theBenchmark for (2745ds/83944Mi) % 300.14/42.93 % (3656856)Instruction limit reached! % 300.14/42.93 % (3656856)------------------------------ % 300.14/42.93 % (3656856)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.14/42.93 % (3656856)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.14/42.93 % (3656856)CaDiCaL version: 2.1.3 % 300.14/42.93 % (3656856)Termination reason: Instruction limit % 300.14/42.93 % (3656856)Termination phase: Saturation % 300.14/42.93 % (3656856)Time elapsed: 5.855 s % 300.14/42.93 % (3656856)Peak memory usage: 135 MB % 300.14/42.93 % (3656856)Instructions burned: 24006 (million) % 300.14/42.93 % (3656864)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=226180801:i=9201:rtra=on_2734 on theBenchmark for (2734ds/9201Mi) % 300.14/42.93 % (3656845)Instruction limit reached! % 300.14/42.93 % (3656845)------------------------------ % 300.14/42.93 % (3656845)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.14/42.93 % (3656845)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.14/42.93 % (3656845)CaDiCaL version: 2.1.3 % 300.14/42.93 % (3656845)Termination reason: Instruction limit % 300.14/42.93 % (3656845)Termination phase: Saturation % 300.14/42.93 % (3656845)Time elapsed: 10.035 s % 300.14/42.93 % (3656845)Peak memory usage: 174 MB % 300.14/42.93 % (3656845)Instructions burned: 20263 (million) % 300.14/42.93 % (3656866)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 % 300.14/42.93 % (3656866)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=1006834054:i=6806:aac=none:nm=0:rtra=on:rawr=on_2722 on theBenchmark for (2722ds/6806Mi) % 300.14/42.93 % (3656864)Instruction limit reached! % 300.14/42.93 % (3656864)------------------------------ % 300.14/42.93 % (3656864)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.14/42.93 % (3656864)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.14/42.93 % (3656864)CaDiCaL version: 2.1.3 % 300.14/42.93 % (3656864)Termination reason: Instruction limit % 300.14/42.93 % (3656864)Termination phase: Saturation % 300.14/42.93 % (3656864)Time elapsed: 3.234 s % 300.14/42.93 % (3656864)Peak memory usage: 128 MB % 300.14/42.93 % (3656864)Instructions burned: 9202 (million) % 300.14/42.93 % (3656870)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=4293015163:s2a=on:i=3553:nm=0:rtra=on_2701 on theBenchmark for (2701ds/3553Mi) % 300.14/42.93 % (3656870)Instruction limit reached! % 300.14/42.93 % (3656870)------------------------------ % 300.14/42.93 % (3656870)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.14/42.93 % (3656870)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.14/42.93 % (3656870)CaDiCaL version: 2.1.3 % 300.14/42.93 % (3656870)Termination reason: Instruction limit % 300.14/42.93 % (3656870)Termination phase: Saturation % 300.14/42.93 % (3656870)Time elapsed: 1.318 s % 300.14/42.93 % (3656870)Peak memory usage: 105 MB % 300.14/42.93 % (3656870)Instructions burned: 3554 (million) % 300.14/42.93 % (3656872)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=537237264:thitd=on:cond=on:i=2064:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2687 on theBenchmark for (2687ds/2064Mi) % 300.14/42.93 % (3656866)Instruction limit reached! % 300.14/42.93 % (3656866)------------------------------ % 300.14/42.93 % (3656866)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.14/42.93 % (3656866)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.14/42.93 % (3656866)CaDiCaL version: 2.1.3 % 300.14/42.93 % (3656866)Termination reason: Instruction limit % 300.14/42.93 % (3656866)Termination phase: Saturation % 300.14/42.93 % (3656866)Time elapsed: 3.622 s % 300.14/42.93 % (3656866)P % 300.14/42.93 Terminated %------------------------------------------------------------------------------