%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWX101_1 : TPTP v9.3.1. Released v9.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % Computer : n006.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:45:53 PM UTC 2026 % Result : Timeout 300.34s 42.94s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWX101_1 : TPTP v9.3.1. Released v9.1.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.08/0.18 % Computer : n006.cluster.edu % 0.08/0.18 % Model : x86_64 x86_64 % 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.18 % Memory : 8046.5625MB % 0.08/0.18 % OS : Linux 6.8.0-71-generic % 0.08/0.18 % CPULimit : 300 % 0.08/0.18 % WCLimit : 300 % 0.08/0.18 % DateTime : Mon Sep 28 15:00:55 UTC 2026 % 0.08/0.19 % CPUTime : % 0.08/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.08/0.21 Running first-order theorem proving % 0.08/0.21 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 % 3.29/1.16 % (4030595)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule. % 3.29/1.16 % (4030603)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=3827570212:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi) % 3.29/1.16 % (4030603)Instruction limit reached! % 3.29/1.16 % (4030603)------------------------------ % 3.29/1.16 % (4030603)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.29/1.16 % (4030603)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.29/1.16 % (4030603)CaDiCaL version: 2.1.3 % 3.29/1.16 % (4030603)Termination reason: Instruction limit % 3.29/1.16 % (4030603)Termination phase: Saturation % 3.29/1.16 % (4030603)Time elapsed: 0.003 s % 3.29/1.16 % (4030603)Peak memory usage: 88 MB % 3.29/1.16 % (4030603)Instructions burned: 8 (million) % 3.29/1.16 % (4030601)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=3753378395:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi) % 3.29/1.16 % (4030602)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=2797952674:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi) % 3.29/1.16 % (4030600)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=3342109338:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi) % 3.29/1.16 % (4030604)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=1851234756:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi) % 3.29/1.16 % (4030606)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=3157991903:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi) % 3.29/1.16 % (4030605)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=1563489135:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi) % 3.29/1.16 % (4030604)Instruction limit reached! % 3.29/1.16 % (4030604)------------------------------ % 3.29/1.16 % (4030604)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.29/1.16 % (4030604)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.29/1.16 % (4030604)CaDiCaL version: 2.1.3 % 3.29/1.16 % (4030604)Termination reason: Instruction limit % 3.29/1.16 % (4030604)Termination phase: Property scanning % 3.29/1.16 % (4030604)Time elapsed: 0.003 s % 3.29/1.16 % (4030604)Peak memory usage: 86 MB % 3.29/1.16 % (4030604)Instructions burned: 4 (million) % 3.29/1.16 % (4030600)Instruction limit reached! % 3.29/1.16 % (4030600)------------------------------ % 3.29/1.16 % (4030600)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.29/1.16 % (4030600)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.29/1.16 % (4030600)CaDiCaL version: 2.1.3 % 3.29/1.16 % (4030600)Termination reason: Instruction limit % 3.29/1.16 % (4030600)Termination phase: Saturation % 3.29/1.16 % (4030600)Time elapsed: 0.030 s % 3.29/1.16 % (4030600)Peak memory usage: 115 MB % 3.29/1.16 % (4030600)Instructions burned: 13 (million) % 3.29/1.16 % (4030606)Instruction limit reached! % 3.29/1.16 % (4030606)------------------------------ % 3.29/1.16 % (4030606)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.29/1.16 % (4030606)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.29/1.16 % (4030606)CaDiCaL version: 2.1.3 % 3.29/1.16 % (4030606)Termination reason: Instruction limit % 3.29/1.16 % (4030606)Termination phase: Saturation % 3.29/1.16 % (4030606)Time elapsed: 0.046 s % 3.29/1.16 % (4030606)Peak memory usage: 116 MB % 3.29/1.16 % (4030606)Instructions burned: 33 (million) % 3.29/1.16 % (4030605)Instruction limit reached! % 3.29/1.16 % (4030605)------------------------------ % 3.29/1.16 % (4030605)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.29/1.16 % (4030605)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.29/1.16 % (4030605)CaDiCaL version: 2.1.3 % 3.29/1.16 % (4030605)Termination reason: Instruction limit % 3.29/1.16 % (4030605)Termination phase: Saturation % 3.29/1.16 % (4030605)Time elapsed: 0.055 s % 3.29/1.16 % (4030605)Peak memory usage: 116 MB % 3.29/1.16 % (4030605)Instructions burned: 46 (million) % 3.29/1.16 % (4030608)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=2488660276:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2998 on theBenchmark for (2998ds/14Mi) % 3.29/1.16 % (4030608)Instruction limit reached! % 3.29/1.16 % (4030608)------------------------------ % 3.95/1.30 % (4030608)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.95/1.30 % (4030608)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.95/1.30 % (4030608)CaDiCaL version: 2.1.3 % 3.95/1.30 % (4030608)Termination reason: Instruction limit % 3.95/1.30 % (4030608)Termination phase: Saturation % 3.95/1.30 % (4030608)Time elapsed: 0.006 s % 3.95/1.30 % (4030608)Peak memory usage: 89 MB % 3.95/1.30 % (4030608)Instructions burned: 16 (million) % 3.95/1.30 % (4030602)Instruction limit reached! % 3.95/1.30 % (4030602)------------------------------ % 3.95/1.30 % (4030602)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.95/1.30 % (4030602)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.95/1.30 % (4030602)CaDiCaL version: 2.1.3 % 3.95/1.30 % (4030602)Termination reason: Instruction limit % 3.95/1.30 % (4030602)Termination phase: Saturation % 3.95/1.30 % (4030602)Time elapsed: 0.115 s % 3.95/1.30 % (4030602)Peak memory usage: 114 MB % 3.95/1.30 % (4030602)Instructions burned: 203 (million) % 3.95/1.30 % (4030615)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=2297557273:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2998 on theBenchmark for (2998ds/29Mi) % 3.95/1.30 % (4030616)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=4173647737:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/16Mi) % 3.95/1.30 % (4030615)Instruction limit reached! % 3.95/1.30 % (4030615)------------------------------ % 3.95/1.30 % (4030615)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.95/1.30 % (4030615)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.95/1.30 % (4030615)CaDiCaL version: 2.1.3 % 3.95/1.30 % (4030615)Termination reason: Instruction limit % 3.95/1.30 % (4030615)Termination phase: Saturation % 3.95/1.30 % (4030615)Time elapsed: 0.023 s % 3.95/1.30 % (4030615)Peak memory usage: 89 MB % 3.95/1.30 % (4030615)Instructions burned: 29 (million) % 3.95/1.30 % (4030620)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=2691424668:i=85:gtgl=4:rtra=on:gtg=exists_sym_2997 on theBenchmark for (2997ds/85Mi) % 3.95/1.30 % (4030616)Instruction limit reached! % 3.95/1.30 % (4030616)------------------------------ % 3.95/1.30 % (4030616)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.95/1.30 % (4030616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.95/1.30 % (4030616)CaDiCaL version: 2.1.3 % 3.95/1.30 % (4030616)Termination reason: Instruction limit % 3.95/1.30 % (4030616)Termination phase: Saturation % 3.95/1.30 % (4030616)Time elapsed: 0.011 s % 3.95/1.30 % (4030616)Peak memory usage: 89 MB % 3.95/1.30 % (4030616)Instructions burned: 17 (million) % 3.95/1.30 % (4030617)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=4222827478:i=24:canc=force:rtra=on_2997 on theBenchmark for (2997ds/24Mi) % 3.95/1.30 % (4030620)Instruction limit reached! % 3.95/1.30 % (4030620)------------------------------ % 3.95/1.30 % (4030620)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.95/1.30 % (4030620)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.95/1.30 % (4030620)CaDiCaL version: 2.1.3 % 3.95/1.30 % (4030620)Termination reason: Instruction limit % 3.95/1.30 % (4030620)Termination phase: Saturation % 3.95/1.30 % (4030620)Time elapsed: 0.027 s % 3.95/1.30 % (4030620)Peak memory usage: 89 MB % 3.95/1.30 % (4030620)Instructions burned: 88 (million) % 3.95/1.30 % (4030617)Instruction limit reached! % 3.95/1.30 % (4030617)------------------------------ % 3.95/1.30 % (4030617)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.95/1.30 % (4030617)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.95/1.30 % (4030617)CaDiCaL version: 2.1.3 % 3.95/1.30 % (4030617)Termination reason: Instruction limit % 3.95/1.30 % (4030617)Termination phase: Saturation % 3.95/1.30 % (4030617)Time elapsed: 0.019 s % 3.95/1.30 % (4030617)Peak memory usage: 89 MB % 3.95/1.30 % (4030617)Instructions burned: 25 (million) % 3.95/1.30 % (4030619)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=4202704192:i=27:canc=cautious:fsr=off:rtra=on_2997 on theBenchmark for (2997ds/27Mi) % 3.95/1.30 % (4030619)Instruction limit reached! % 3.95/1.30 % (4030619)------------------------------ % 3.95/1.30 % (4030619)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.85/1.44 % (4030619)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.85/1.44 % (4030619)CaDiCaL version: 2.1.3 % 4.85/1.44 % (4030619)Termination reason: Instruction limit % 4.85/1.44 % (4030619)Termination phase: Saturation % 4.85/1.44 % (4030619)Time elapsed: 0.018 s % 4.85/1.44 % (4030619)Peak memory usage: 89 MB % 4.85/1.44 % (4030619)Instructions burned: 28 (million) % 4.85/1.44 % (4030601)Instruction limit reached! % 4.85/1.44 % (4030601)------------------------------ % 4.85/1.44 % (4030601)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.85/1.44 % (4030601)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.85/1.44 % (4030601)CaDiCaL version: 2.1.3 % 4.85/1.44 % (4030601)Termination reason: Instruction limit % 4.85/1.44 % (4030601)Termination phase: Saturation % 4.85/1.44 % (4030601)Time elapsed: 0.223 s % 4.85/1.44 % (4030601)Peak memory usage: 118 MB % 4.85/1.44 % (4030601)Instructions burned: 308 (million) % 4.85/1.44 % (4030621)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=1306739934:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2997 on theBenchmark for (2997ds/2Mi) % 4.85/1.44 % (4030621)Instruction limit reached! % 4.85/1.44 % (4030621)------------------------------ % 4.85/1.44 % (4030621)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.85/1.44 % (4030621)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.85/1.44 % (4030621)CaDiCaL version: 2.1.3 % 4.85/1.44 % (4030621)Termination reason: Instruction limit % 4.85/1.44 % (4030621)Termination phase: Preprocessing 3 % 4.85/1.44 % (4030621)Time elapsed: 0.002 s % 4.85/1.44 % (4030621)Peak memory usage: 86 MB % 4.85/1.44 % (4030621)Instructions burned: 2 (million) % 4.85/1.44 % (4030628)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=788224591:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2996 on theBenchmark for (2996ds/66Mi) % 4.85/1.44 % (4030624)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=1555347146:i=181:rtra=on:ss=axioms:ev=cautious_2996 on theBenchmark for (2996ds/181Mi) % 4.85/1.44 % (4030626)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=423483673:i=4:ep=RST:ins=2:rtra=on_2996 on theBenchmark for (2996ds/4Mi) % 4.85/1.44 % (4030626)Instruction limit reached! % 4.85/1.44 % (4030626)------------------------------ % 4.85/1.44 % (4030626)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.85/1.44 % (4030626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.85/1.44 % (4030626)CaDiCaL version: 2.1.3 % 4.85/1.44 % (4030626)Termination reason: Instruction limit % 4.85/1.44 % (4030626)Termination phase: Property scanning % 4.85/1.44 % (4030626)Time elapsed: 0.003 s % 4.85/1.44 % (4030626)Peak memory usage: 86 MB % 4.85/1.44 % (4030626)Instructions burned: 4 (million) % 4.85/1.44 % (4030629)lrs+10_1_thi=all:si=on:fd=off:random_seed=3977383447:i=53:rtra=on:gtg=all_2996 on theBenchmark for (2996ds/53Mi) % 4.85/1.44 % (4030628)Instruction limit reached! % 4.85/1.44 % (4030628)------------------------------ % 4.85/1.44 % (4030628)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.85/1.44 % (4030628)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.85/1.44 % (4030628)CaDiCaL version: 2.1.3 % 4.85/1.44 % (4030628)Termination reason: Instruction limit % 4.85/1.44 % (4030628)Termination phase: Saturation % 4.85/1.44 % (4030628)Time elapsed: 0.054 s % 4.85/1.44 % (4030628)Peak memory usage: 134 MB % 4.85/1.44 % (4030628)Instructions burned: 67 (million) % 4.85/1.44 % (4030631)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=496523961:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2996 on theBenchmark for (2996ds/8Mi) % 4.85/1.44 % (4030632)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=3623836114:st=3:i=2:rtra=on:ss=axioms_2996 on theBenchmark for (2996ds/2Mi) % 4.85/1.44 % (4030632)Instruction limit reached! % 4.85/1.44 % (4030632)------------------------------ % 4.85/1.44 % (4030632)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.85/1.44 % (4030632)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.85/1.44 % (4030632)CaDiCaL version: 2.1.3 % 4.85/1.44 % (4030632)Termination reason: Instruction limit % 4.85/1.44 % (4030632)Termination phase: Preprocessing 3 % 6.23/1.67 % (4030632)Time elapsed: 0.002 s % 6.23/1.67 % (4030632)Peak memory usage: 86 MB % 6.23/1.67 % (4030632)Instructions burned: 2 (million) % 6.23/1.67 % (4030631)Instruction limit reached! % 6.23/1.67 % (4030631)------------------------------ % 6.23/1.67 % (4030631)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.23/1.67 % (4030631)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.23/1.67 % (4030631)CaDiCaL version: 2.1.3 % 6.23/1.67 % (4030631)Termination reason: Instruction limit % 6.23/1.67 % (4030631)Termination phase: Saturation % 6.23/1.67 % (4030631)Time elapsed: 0.006 s % 6.23/1.67 % (4030631)Peak memory usage: 89 MB % 6.23/1.67 % (4030631)Instructions burned: 9 (million) % 6.23/1.67 % (4030624)Instruction limit reached! % 6.23/1.67 % (4030624)------------------------------ % 6.23/1.67 % (4030624)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.23/1.67 % (4030624)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.23/1.67 % (4030624)CaDiCaL version: 2.1.3 % 6.23/1.67 % (4030624)Termination reason: Instruction limit % 6.23/1.67 % (4030624)Termination phase: Saturation % 6.23/1.67 % (4030624)Time elapsed: 0.105 s % 6.23/1.67 % (4030624)Peak memory usage: 90 MB % 6.23/1.67 % (4030624)Instructions burned: 183 (million) % 6.23/1.67 % (4030629)Instruction limit reached! % 6.23/1.67 % (4030629)------------------------------ % 6.23/1.67 % (4030629)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.23/1.67 % (4030629)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.23/1.67 % (4030629)CaDiCaL version: 2.1.3 % 6.23/1.67 % (4030629)Termination reason: Instruction limit % 6.23/1.67 % (4030629)Termination phase: Saturation % 6.23/1.67 % (4030629)Time elapsed: 0.063 s % 6.23/1.67 % (4030629)Peak memory usage: 117 MB % 6.23/1.67 % (4030629)Instructions burned: 53 (million) % 6.23/1.67 % (4030634)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=3728131552:i=2:doe=on:canc=force:asg=cautious:rtra=on_2995 on theBenchmark for (2995ds/2Mi) % 6.23/1.67 % (4030634)Instruction limit reached! % 6.23/1.67 % (4030634)------------------------------ % 6.23/1.67 % (4030634)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.23/1.67 % (4030634)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.23/1.67 % (4030634)CaDiCaL version: 2.1.3 % 6.23/1.67 % (4030634)Termination reason: Instruction limit % 6.23/1.67 % (4030634)Termination phase: Preprocessing 3 % 6.23/1.67 % (4030634)Time elapsed: 0.002 s % 6.23/1.67 % (4030634)Peak memory usage: 86 MB % 6.23/1.67 % (4030634)Instructions burned: 2 (million) % 6.23/1.67 % (4030638)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=761719479:i=127:doe=on:rtra=on_2995 on theBenchmark for (2995ds/127Mi) % 6.23/1.67 % (4030640)dis+10_1_si=on:random_seed=919913318:i=10:ep=R:rtra=on_2995 on theBenchmark for (2995ds/10Mi) % 6.23/1.67 % (4030640)Instruction limit reached! % 6.23/1.67 % (4030640)------------------------------ % 6.23/1.67 % (4030640)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.23/1.67 % (4030640)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.23/1.67 % (4030640)CaDiCaL version: 2.1.3 % 6.23/1.67 % (4030640)Termination reason: Instruction limit % 6.23/1.67 % (4030640)Termination phase: Saturation % 6.23/1.67 % (4030640)Time elapsed: 0.004 s % 6.23/1.67 % (4030640)Peak memory usage: 88 MB % 6.23/1.67 % (4030640)Instructions burned: 11 (million) % 6.23/1.67 % (4030643)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=271124885:i=26:canc=cautious:av=off:rtra=on_2994 on theBenchmark for (2994ds/26Mi) % 6.23/1.67 % (4030643)Refutation not found, incomplete strategy % 6.23/1.67 % (4030643)------------------------------ % 6.23/1.67 % (4030643)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.23/1.67 % (4030643)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.23/1.67 % (4030643)CaDiCaL version: 2.1.3 % 6.23/1.67 % (4030643)Termination reason: Refutation not found, incomplete strategy % 6.23/1.67 % (4030643)Time elapsed: 0.006 s % 6.23/1.67 % (4030643)Peak memory usage: 89 MB % 6.23/1.67 % (4030643)Instructions burned: 8 (million) % 6.23/1.67 % (4030644)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=194888915: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) % 8.30/1.90 % (4030646)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=2553371044:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2994 on theBenchmark for (2994ds/8Mi) % 8.30/1.90 % (4030646)Instruction limit reached! % 8.30/1.90 % (4030646)------------------------------ % 8.30/1.90 % (4030646)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.30/1.90 % (4030646)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.30/1.90 % (4030646)CaDiCaL version: 2.1.3 % 8.30/1.90 % (4030646)Termination reason: Instruction limit % 8.30/1.90 % (4030646)Termination phase: Saturation % 8.30/1.90 % (4030646)Time elapsed: 0.006 s % 8.30/1.90 % (4030646)Peak memory usage: 88 MB % 8.30/1.90 % (4030646)Instructions burned: 9 (million) % 8.30/1.90 % (4030645)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=3892119975:i=2:fsr=off:rtra=on:inst=on_2994 on theBenchmark for (2994ds/2Mi) % 8.30/1.90 % (4030645)Instruction limit reached! % 8.30/1.90 % (4030645)------------------------------ % 8.30/1.90 % (4030645)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.30/1.91 % (4030645)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.30/1.91 % (4030645)CaDiCaL version: 2.1.3 % 8.30/1.91 % (4030645)Termination reason: Instruction limit % 8.30/1.91 % (4030645)Termination phase: Preprocessing 3 % 8.30/1.91 % (4030645)Time elapsed: 0.002 s % 8.30/1.91 % (4030645)Peak memory usage: 86 MB % 8.30/1.91 % (4030645)Instructions burned: 2 (million) % 8.30/1.91 % (4030648)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=3290464666:i=370:ep=RS:fsr=off:rtra=on_2994 on theBenchmark for (2994ds/370Mi) % 8.30/1.91 % (4030638)Instruction limit reached! % 8.30/1.91 % (4030638)------------------------------ % 8.30/1.91 % (4030638)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.30/1.91 % (4030638)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.30/1.91 % (4030638)CaDiCaL version: 2.1.3 % 8.30/1.91 % (4030638)Termination reason: Instruction limit % 8.30/1.91 % (4030638)Termination phase: Saturation % 8.30/1.91 % (4030638)Time elapsed: 0.110 s % 8.30/1.91 % (4030638)Peak memory usage: 117 MB % 8.30/1.91 % (4030638)Instructions burned: 127 (million) % 8.30/1.91 % (4030644)Instruction limit reached! % 8.30/1.91 % (4030644)------------------------------ % 8.30/1.91 % (4030644)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.30/1.91 % (4030644)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.30/1.91 % (4030644)CaDiCaL version: 2.1.3 % 8.30/1.91 % (4030644)Termination reason: Instruction limit % 8.30/1.91 % (4030644)Termination phase: Saturation % 8.30/1.91 % (4030644)Time elapsed: 0.028 s % 8.30/1.91 % (4030644)Peak memory usage: 89 MB % 8.30/1.91 % (4030644)Instructions burned: 36 (million) % 8.30/1.91 % (4030651)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=3615905604:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2994 on theBenchmark for (2994ds/13Mi) % 8.30/1.91 % (4030651)Instruction limit reached! % 8.30/1.91 % (4030651)------------------------------ % 8.30/1.91 % (4030651)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.30/1.91 % (4030651)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.30/1.91 % (4030651)CaDiCaL version: 2.1.3 % 8.30/1.91 % (4030651)Termination reason: Instruction limit % 8.30/1.91 % (4030651)Termination phase: Saturation % 8.30/1.91 % (4030651)Time elapsed: 0.029 s % 8.30/1.91 % (4030651)Peak memory usage: 112 MB % 8.30/1.91 % (4030651)Instructions burned: 13 (million) % 8.30/1.91 % (4030658)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=3122476873:i=10:rtra=on_2993 on theBenchmark for (2993ds/10Mi) % 8.30/1.91 % (4030658)Instruction limit reached! % 8.30/1.91 % (4030658)------------------------------ % 8.30/1.91 % (4030658)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.30/1.91 % (4030658)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.30/1.91 % (4030658)CaDiCaL version: 2.1.3 % 8.30/1.91 % (4030658)Termination reason: Instruction limit % 8.30/1.91 % (4030658)Termination phase: Saturation % 8.30/1.91 % (4030658)Time elapsed: 0.007 s % 8.30/1.91 % (4030658)Peak memory usage: 88 MB % 8.30/1.91 % (4030658)Instructions burned: 10 (million) % 8.30/1.91 % (4030656)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=1037467997:i=226:rtra=on:gtg=position:ss=axioms_2993 on theBenchmark for (2993ds/226Mi) % 10.14/2.10 % (4030659)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=3206161446:i=71:rtra=on:gtg=exists_top_2993 on theBenchmark for (2993ds/71Mi) % 10.14/2.10 % (4030660)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=889411029:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2993 on theBenchmark for (2993ds/75Mi) % 10.14/2.10 % (4030660)Instruction limit reached! % 10.14/2.10 % (4030660)------------------------------ % 10.14/2.10 % (4030660)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.14/2.10 % (4030660)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.14/2.10 % (4030660)CaDiCaL version: 2.1.3 % 10.14/2.10 % (4030660)Termination reason: Instruction limit % 10.14/2.10 % (4030660)Termination phase: Saturation % 10.14/2.10 % (4030660)Time elapsed: 0.050 s % 10.14/2.10 % (4030660)Peak memory usage: 91 MB % 10.14/2.10 % (4030660)Instructions burned: 76 (million) % 10.14/2.10 % (4030648)Instruction limit reached! % 10.14/2.10 % (4030648)------------------------------ % 10.14/2.10 % (4030648)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.14/2.10 % (4030648)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.14/2.10 % (4030648)CaDiCaL version: 2.1.3 % 10.14/2.10 % (4030648)Termination reason: Instruction limit % 10.14/2.10 % (4030648)Termination phase: Saturation % 10.14/2.10 % (4030648)Time elapsed: 0.204 s % 10.14/2.10 % (4030648)Peak memory usage: 94 MB % 10.14/2.10 % (4030648)Instructions burned: 371 (million) % 10.14/2.10 % (4030643)------------------------------ % 10.14/2.10 % (4030643)------------------------------ % 10.14/2.10 % (4030662)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=3700121041:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2992 on theBenchmark for (2992ds/294Mi) % 10.14/2.10 % (4030659)Instruction limit reached! % 10.14/2.10 % (4030659)------------------------------ % 10.14/2.10 % (4030659)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.14/2.10 % (4030659)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.14/2.10 % (4030659)CaDiCaL version: 2.1.3 % 10.14/2.10 % (4030659)Termination reason: Instruction limit % 10.14/2.10 % (4030659)Termination phase: Saturation % 10.14/2.10 % (4030659)Time elapsed: 0.093 s % 10.14/2.10 % (4030659)Peak memory usage: 134 MB % 10.14/2.10 % (4030659)Instructions burned: 72 (million) % 10.14/2.10 % (4030665)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=2151824742:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2992 on theBenchmark for (2992ds/130Mi) % 10.14/2.10 % (4030656)Instruction limit reached! % 10.14/2.10 % (4030656)------------------------------ % 10.14/2.10 % (4030656)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.14/2.10 % (4030656)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.14/2.10 % (4030656)CaDiCaL version: 2.1.3 % 10.14/2.10 % (4030656)Termination reason: Instruction limit % 10.14/2.10 % (4030656)Termination phase: Saturation % 10.14/2.10 % (4030656)Time elapsed: 0.169 s % 10.14/2.10 % (4030656)Peak memory usage: 120 MB % 10.14/2.10 % (4030656)Instructions burned: 227 (million) % 10.14/2.10 % (4030668)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=894768464:i=131:rtra=on_2991 on theBenchmark for (2991ds/131Mi) % 10.14/2.10 % (4030662)Instruction limit reached! % 10.14/2.10 % (4030662)------------------------------ % 10.14/2.10 % (4030662)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.14/2.10 % (4030662)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.14/2.10 % (4030662)CaDiCaL version: 2.1.3 % 10.14/2.10 % (4030662)Termination reason: Instruction limit % 10.14/2.10 % (4030662)Termination phase: Saturation % 10.14/2.10 % (4030662)Time elapsed: 0.109 s % 10.14/2.10 % (4030662)Peak memory usage: 91 MB % 10.14/2.10 % (4030662)Instructions burned: 296 (million) % 10.14/2.10 % (4030670)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=1249343252:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2991 on theBenchmark for (2991ds/40Mi) % 10.14/2.10 % (4030671)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=1833084831:i=307:rtra=on:gtg=exists_top_2991 on theBenchmark for (2991ds/307Mi) % 10.14/2.10 % (4030665)Instruction limit reached! % 10.14/2.10 % (4030665)------------------------------ % 11.90/2.43 % (4030665)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.90/2.43 % (4030665)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.90/2.43 % (4030665)CaDiCaL version: 2.1.3 % 11.90/2.43 % (4030665)Termination reason: Instruction limit % 11.90/2.43 % (4030665)Termination phase: Saturation % 11.90/2.43 % (4030665)Time elapsed: 0.111 s % 11.90/2.43 % (4030665)Peak memory usage: 119 MB % 11.90/2.43 % (4030665)Instructions burned: 130 (million) % 11.90/2.43 % (4030672)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=455575670:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2991 on theBenchmark for (2991ds/598Mi) % 11.90/2.43 % (4030676)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=1007418150:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2990 on theBenchmark for (2990ds/259Mi) % 11.90/2.43 % (4030670)Instruction limit reached! % 11.90/2.43 % (4030670)------------------------------ % 11.90/2.43 % (4030670)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.90/2.43 % (4030670)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.90/2.43 % (4030670)CaDiCaL version: 2.1.3 % 11.90/2.43 % (4030670)Termination reason: Instruction limit % 11.90/2.43 % (4030670)Termination phase: Saturation % 11.90/2.43 % (4030670)Time elapsed: 0.070 s % 11.90/2.43 % (4030670)Peak memory usage: 134 MB % 11.90/2.43 % (4030670)Instructions burned: 41 (million) % 11.90/2.43 % (4030674)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=2844920109:i=131:canc=cautious:fsr=off:rtra=on_2990 on theBenchmark for (2990ds/131Mi) % 11.90/2.43 % (4030668)Instruction limit reached! % 11.90/2.43 % (4030668)------------------------------ % 11.90/2.43 % (4030668)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.90/2.43 % (4030668)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.90/2.43 % (4030668)CaDiCaL version: 2.1.3 % 11.90/2.43 % (4030668)Termination reason: Instruction limit % 11.90/2.43 % (4030668)Termination phase: Saturation % 11.90/2.43 % (4030668)Time elapsed: 0.134 s % 11.90/2.43 % (4030668)Peak memory usage: 135 MB % 11.90/2.43 % (4030668)Instructions burned: 131 (million) % 11.90/2.43 % (4030680)dis+10_1_si=on:random_seed=1145339621:s2a=on:i=1000:rtra=on:gtg=exists_all_2989 on theBenchmark for (2989ds/1000Mi) % 11.90/2.43 % (4030676)Instruction limit reached! % 11.90/2.43 % (4030676)------------------------------ % 11.90/2.43 % (4030676)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.90/2.43 % (4030676)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.90/2.43 % (4030676)CaDiCaL version: 2.1.3 % 11.90/2.43 % (4030676)Termination reason: Instruction limit % 11.90/2.43 % (4030676)Termination phase: Saturation % 11.90/2.43 % (4030676)Time elapsed: 0.106 s % 11.90/2.43 % (4030676)Peak memory usage: 119 MB % 11.90/2.43 % (4030676)Instructions burned: 259 (million) % 11.90/2.43 % (4030674)Instruction limit reached! % 11.90/2.43 % (4030674)------------------------------ % 11.90/2.43 % (4030674)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.90/2.43 % (4030674)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.90/2.43 % (4030674)CaDiCaL version: 2.1.3 % 11.90/2.43 % (4030674)Termination reason: Instruction limit % 11.90/2.43 % (4030674)Termination phase: Saturation % 11.90/2.43 % (4030674)Time elapsed: 0.103 s % 11.90/2.43 % (4030674)Peak memory usage: 118 MB % 11.90/2.43 % (4030674)Instructions burned: 132 (million) % 11.90/2.43 % (4030671)Instruction limit reached! % 11.90/2.43 % (4030671)------------------------------ % 11.90/2.43 % (4030671)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.90/2.43 % (4030671)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.90/2.43 % (4030671)CaDiCaL version: 2.1.3 % 11.90/2.43 % (4030671)Termination reason: Instruction limit % 11.90/2.43 % (4030671)Termination phase: Saturation % 11.90/2.43 % (4030671)Time elapsed: 0.204 s % 11.90/2.43 % (4030671)Peak memory usage: 92 MB % 11.90/2.43 % (4030671)Instructions burned: 308 (million) % 11.90/2.43 % (4030682)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=3131496564:i=383:fsr=off:rtra=on:ev=force_2989 on theBenchmark for (2989ds/383Mi) % 11.90/2.43 % (4030684)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=1020342562:i=141:doe=on:rtra=on_2988 on theBenchmark for (2988ds/141Mi) % 13.65/2.73 % (4030686)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=3119253047:i=65:nm=16:rtra=on_2988 on theBenchmark for (2988ds/65Mi) % 13.65/2.73 % (4030686)Instruction limit reached! % 13.65/2.73 % (4030686)------------------------------ % 13.65/2.73 % (4030686)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.65/2.73 % (4030686)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.65/2.73 % (4030686)CaDiCaL version: 2.1.3 % 13.65/2.73 % (4030686)Termination reason: Instruction limit % 13.65/2.73 % (4030686)Termination phase: Saturation % 13.65/2.73 % (4030686)Time elapsed: 0.038 s % 13.65/2.73 % (4030686)Peak memory usage: 118 MB % 13.65/2.73 % (4030686)Instructions burned: 67 (million) % 13.65/2.73 % (4030687)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=3813430446:i=121:nm=16:rtra=on_2987 on theBenchmark for (2987ds/121Mi) % 13.65/2.73 % (4030688)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=219077478:s2a=on:i=128:s2at=5:ins=3:rtra=on_2987 on theBenchmark for (2987ds/128Mi) % 13.65/2.73 % (4030684)Instruction limit reached! % 13.65/2.73 % (4030684)------------------------------ % 13.65/2.73 % (4030684)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.65/2.73 % (4030684)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.65/2.73 % (4030684)CaDiCaL version: 2.1.3 % 13.65/2.73 % (4030684)Termination reason: Instruction limit % 13.65/2.73 % (4030684)Termination phase: Saturation % 13.65/2.73 % (4030684)Time elapsed: 0.097 s % 13.65/2.73 % (4030684)Peak memory usage: 90 MB % 13.65/2.73 % (4030684)Instructions burned: 142 (million) % 13.65/2.73 % (4030687)Instruction limit reached! % 13.65/2.73 % (4030687)------------------------------ % 13.65/2.73 % (4030687)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.65/2.73 % (4030687)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.65/2.73 % (4030687)CaDiCaL version: 2.1.3 % 13.65/2.73 % (4030687)Termination reason: Instruction limit % 13.65/2.73 % (4030687)Termination phase: Saturation % 13.65/2.73 % (4030687)Time elapsed: 0.077 s % 13.65/2.73 % (4030687)Peak memory usage: 90 MB % 13.65/2.73 % (4030687)Instructions burned: 121 (million) % 13.65/2.73 % (4030692)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=3284510991:i=39:ins=3:rtra=on_2986 on theBenchmark for (2986ds/39Mi) % 13.65/2.73 % (4030682)Instruction limit reached! % 13.65/2.73 % (4030682)------------------------------ % 13.65/2.73 % (4030682)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.65/2.73 % (4030682)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.65/2.73 % (4030682)CaDiCaL version: 2.1.3 % 13.65/2.73 % (4030682)Termination reason: Instruction limit % 13.65/2.73 % (4030682)Termination phase: Saturation % 13.65/2.73 % (4030682)Time elapsed: 0.211 s % 13.65/2.73 % (4030682)Peak memory usage: 92 MB % 13.65/2.73 % (4030682)Instructions burned: 383 (million) % 13.65/2.73 % (4030672)Instruction limit reached! % 13.65/2.73 % (4030672)------------------------------ % 13.65/2.73 % (4030672)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.65/2.73 % (4030672)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.65/2.73 % (4030672)CaDiCaL version: 2.1.3 % 13.65/2.73 % (4030672)Termination reason: Instruction limit % 13.65/2.73 % (4030672)Termination phase: Saturation % 13.65/2.73 % (4030672)Time elapsed: 0.411 s % 13.65/2.73 % (4030672)Peak memory usage: 138 MB % 13.65/2.73 % (4030672)Instructions burned: 599 (million) % 13.65/2.73 % (4030692)Instruction limit reached! % 13.65/2.73 % (4030692)------------------------------ % 13.65/2.73 % (4030692)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.65/2.73 % (4030692)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.65/2.73 % (4030692)CaDiCaL version: 2.1.3 % 13.65/2.73 % (4030692)Termination reason: Instruction limit % 13.65/2.73 % (4030692)Termination phase: Saturation % 13.65/2.73 % (4030692)Time elapsed: 0.028 s % 13.65/2.73 % (4030692)Peak memory usage: 116 MB % 13.65/2.73 % (4030692)Instructions burned: 39 (million) % 13.65/2.73 % (4030688)Instruction limit reached! % 13.65/2.73 % (4030688)------------------------------ % 13.65/2.73 % (4030688)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.65/2.73 % (4030688)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.12/2.97 % (4030688)CaDiCaL version: 2.1.3 % 15.12/2.97 % (4030688)Termination reason: Instruction limit % 15.12/2.97 % (4030688)Termination phase: Saturation % 15.12/2.97 % (4030688)Time elapsed: 0.109 s % 15.12/2.97 % (4030688)Peak memory usage: 119 MB % 15.12/2.97 % (4030688)Instructions burned: 129 (million) % 15.12/2.97 % (4030695)dis+1010_1_to=kbo:si=on:random_seed=1310881901:i=175:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2986 on theBenchmark for (2986ds/175Mi) % 15.12/2.97 % (4030699)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=1851702939:thitd=on:i=215:nm=0:rtra=on:ev=force_2985 on theBenchmark for (2985ds/215Mi) % 15.12/2.97 % (4030696)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=4173753507:i=329:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2985 on theBenchmark for (2985ds/329Mi) % 15.12/2.97 % (4030698)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=3010866548:s2a=on:i=483:doe=on:nm=32:rtra=on_2985 on theBenchmark for (2985ds/483Mi) % 15.12/2.97 % (4030701)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=96093552:st=2:i=295:rtra=on:ss=axioms_2985 on theBenchmark for (2985ds/295Mi) % 15.12/2.97 % (4030700)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=3508212149:i=349:rtra=on_2985 on theBenchmark for (2985ds/349Mi) % 15.12/2.97 % (4030695)Instruction limit reached! % 15.12/2.97 % (4030695)------------------------------ % 15.12/2.97 % (4030695)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.12/2.97 % (4030695)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.12/2.97 % (4030695)CaDiCaL version: 2.1.3 % 15.12/2.97 % (4030695)Termination reason: Instruction limit % 15.12/2.97 % (4030695)Termination phase: Saturation % 15.12/2.97 % (4030695)Time elapsed: 0.118 s % 15.12/2.97 % (4030695)Peak memory usage: 91 MB % 15.12/2.97 % (4030695)Instructions burned: 176 (million) % 15.12/2.97 % (4030699)Instruction limit reached! % 15.12/2.97 % (4030699)------------------------------ % 15.12/2.97 % (4030699)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.12/2.97 % (4030699)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.12/2.97 % (4030699)CaDiCaL version: 2.1.3 % 15.12/2.97 % (4030699)Termination reason: Instruction limit % 15.12/2.97 % (4030699)Termination phase: Saturation % 15.12/2.97 % (4030699)Time elapsed: 0.093 s % 15.12/2.97 % (4030699)Peak memory usage: 135 MB % 15.12/2.97 % (4030699)Instructions burned: 218 (million) % 15.12/2.97 % (4030696)Instruction limit reached! % 15.12/2.97 % (4030696)------------------------------ % 15.12/2.97 % (4030696)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.12/2.97 % (4030696)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.12/2.97 % (4030696)CaDiCaL version: 2.1.3 % 15.12/2.97 % (4030696)Termination reason: Instruction limit % 15.12/2.97 % (4030696)Termination phase: Saturation % 15.12/2.97 % (4030696)Time elapsed: 0.164 s % 15.12/2.97 % (4030696)Peak memory usage: 114 MB % 15.12/2.97 % (4030696)Instructions burned: 331 (million) % 15.12/2.97 % (4030709)dis+1010_1_to=lpo:sil=128000:sas=z3:si=on:nwc=5:random_seed=3787600560:i=281:gtgl=2:rtra=on:gtg=all_2983 on theBenchmark for (2983ds/281Mi) % 15.12/2.97 % (4030708)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=3091280787:i=328:kws=inv_frequency:nm=20:rtra=on_2983 on theBenchmark for (2983ds/328Mi) % 15.12/2.97 % (4030701)Instruction limit reached! % 15.12/2.97 % (4030701)------------------------------ % 15.12/2.97 % (4030701)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.12/2.97 % (4030701)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.12/2.97 % (4030701)CaDiCaL version: 2.1.3 % 15.12/2.97 % (4030701)Termination reason: Instruction limit % 15.12/2.97 % (4030701)Termination phase: Saturation % 15.12/2.97 % (4030701)Time elapsed: 0.166 s % 15.12/2.97 % (4030701)Peak memory usage: 91 MB % 15.12/2.97 % (4030701)Instructions burned: 296 (million) % 15.12/2.97 % (4030680)Instruction limit reached! % 15.12/2.97 % (4030680)------------------------------ % 15.12/2.97 % (4030680)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.12/2.97 % (4030680)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.12/2.97 % (4030680)CaDiCaL version: 2.1.3 % 17.93/3.20 % (4030680)Termination reason: Instruction limit % 17.93/3.20 % (4030680)Termination phase: Saturation % 17.93/3.20 % (4030680)Time elapsed: 0.626 s % 17.93/3.20 % (4030680)Peak memory usage: 97 MB % 17.93/3.20 % (4030680)Instructions burned: 1001 (million) % 17.93/3.20 % (4030709)Instruction limit reached! % 17.93/3.20 % (4030709)------------------------------ % 17.93/3.20 % (4030709)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.93/3.20 % (4030709)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.93/3.20 % (4030709)CaDiCaL version: 2.1.3 % 17.93/3.20 % (4030709)Termination reason: Instruction limit % 17.93/3.20 % (4030709)Termination phase: Saturation % 17.93/3.20 % (4030709)Time elapsed: 0.109 s % 17.93/3.20 % (4030709)Peak memory usage: 118 MB % 17.93/3.20 % (4030709)Instructions burned: 281 (million) % 17.93/3.20 % (4030710)lrs+1010_1_to=kbo:sil=128000:si=on:sos=on:urr=on:uwa=alasca_main:random_seed=2511776563:i=484:doe=on:nm=0:av=off:rtra=on:ss=axioms_2983 on theBenchmark for (2983ds/484Mi) % 17.93/3.20 % (4030700)Instruction limit reached! % 17.93/3.20 % (4030700)------------------------------ % 17.93/3.20 % (4030700)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.93/3.20 % (4030700)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.93/3.20 % (4030700)CaDiCaL version: 2.1.3 % 17.93/3.20 % (4030700)Termination reason: Instruction limit % 17.93/3.20 % (4030700)Termination phase: Saturation % 17.93/3.20 % (4030700)Time elapsed: 0.258 s % 17.93/3.20 % (4030700)Peak memory usage: 120 MB % 17.93/3.20 % (4030700)Instructions burned: 350 (million) % 17.93/3.20 % (4030713)lrs+21_1_to=kbo:sil=128000:thi=neg_eq:si=on:random_seed=3019943146:i=321:canc=force:rtra=on:tac=axiom:ss=axioms:ev=force_2982 on theBenchmark for (2982ds/321Mi) % 17.93/3.20 % (4030698)Instruction limit reached! % 17.93/3.20 % (4030698)------------------------------ % 17.93/3.20 % (4030698)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.93/3.20 % (4030698)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.93/3.20 % (4030698)CaDiCaL version: 2.1.3 % 17.93/3.20 % (4030698)Termination reason: Instruction limit % 17.93/3.20 % (4030698)Termination phase: Saturation % 17.93/3.20 % (4030698)Time elapsed: 0.332 s % 17.93/3.20 % (4030698)Peak memory usage: 137 MB % 17.93/3.20 % (4030698)Instructions burned: 483 (million) % 17.93/3.20 % (4030715)lrs+1010_1_to=kbo:tgt=ground:fde=unused:sas=z3:si=on:sp=unary_frequency:gve=force:spb=goal:tha=off:random_seed=270444485:i=471:thf=on:kws=precedence:rtra=on_2981 on theBenchmark for (2981ds/471Mi) % 17.93/3.20 % (4030714)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=2303266983:i=416:rtra=on:gtg=position:ss=axioms_2982 on theBenchmark for (2982ds/416Mi) % 17.93/3.20 % (4030708)Instruction limit reached! % 17.93/3.20 % (4030708)------------------------------ % 17.93/3.20 % (4030708)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.93/3.20 % (4030708)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.93/3.20 % (4030708)CaDiCaL version: 2.1.3 % 17.93/3.20 % (4030708)Termination reason: Instruction limit % 17.93/3.20 % (4030708)Termination phase: Saturation % 17.93/3.20 % (4030708)Time elapsed: 0.221 s % 17.93/3.20 % (4030708)Peak memory usage: 119 MB % 17.93/3.20 % (4030708)Instructions burned: 328 (million) % 17.93/3.20 % (4030717)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=1026825252:avsq=on:i=276:avsqr=1,2:rtra=on_2981 on theBenchmark for (2981ds/276Mi) % 17.93/3.20 % (4030713)Instruction limit reached! % 17.93/3.20 % (4030713)------------------------------ % 17.93/3.20 % (4030713)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.93/3.20 % (4030713)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.93/3.20 % (4030713)CaDiCaL version: 2.1.3 % 17.93/3.20 % (4030713)Termination reason: Instruction limit % 17.93/3.20 % (4030713)Termination phase: Saturation % 17.93/3.20 % (4030713)Time elapsed: 0.157 s % 17.93/3.20 % (4030713)Peak memory usage: 114 MB % 17.93/3.20 % (4030713)Instructions burned: 321 (million) % 17.93/3.20 % (4030719)lrs+1010_2_to=kbo:sil=128000:tgt=ground:fde=unused:sas=z3:si=on:uwa=off:tha=off:nwc=1:random_seed=2198168693:i=375:kws=inv_arity_squared:rtra=on_2980 on theBenchmark for (2980ds/375Mi) % 17.93/3.20 % (4030722)lrs+10_1_to=kbo:sil=128000:tgt=full:sas=z3:si=on:uwa=func_ext:slsqc=1:flr=on:slsq=on:random_seed=641097414:i=387:bd=preordered:rtra=on:ss=axioms:sgt=8_2980 on theBenchmark for (2980ds/387Mi) % 19.15/3.66 % (4030715)Instruction limit reached! % 19.15/3.66 % (4030715)------------------------------ % 19.15/3.66 % (4030715)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.15/3.66 % (4030715)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.15/3.66 % (4030715)CaDiCaL version: 2.1.3 % 19.15/3.66 % (4030715)Termination reason: Instruction limit % 19.15/3.66 % (4030715)Termination phase: Saturation % 19.15/3.66 % (4030715)Time elapsed: 0.177 s % 19.15/3.66 % (4030715)Peak memory usage: 121 MB % 19.15/3.66 % (4030715)Instructions burned: 472 (million) % 19.15/3.66 % (4030710)Instruction limit reached! % 19.15/3.66 % (4030710)------------------------------ % 19.15/3.66 % (4030710)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.15/3.66 % (4030710)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.15/3.66 % (4030710)CaDiCaL version: 2.1.3 % 19.15/3.66 % (4030710)Termination reason: Instruction limit % 19.15/3.66 % (4030710)Termination phase: Saturation % 19.15/3.66 % (4030710)Time elapsed: 0.266 s % 19.15/3.66 % (4030710)Peak memory usage: 92 MB % 19.15/3.66 % (4030710)Instructions burned: 485 (million) % 19.15/3.66 % (4030724)lrs+10_1_to=kbo:sil=128000:fde=none:si=on:norm_ineq=on:urr=on:nwc=0.5:random_seed=3688566449:i=513:kws=frequency:bd=all:rtra=on:gtg=exists_all:ss=axioms:sgt=4_2979 on theBenchmark for (2979ds/513Mi) % 19.15/3.66 % (4030727)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=1619122269:i=334:rtra=on_2979 on theBenchmark for (2979ds/334Mi) % 19.15/3.66 % (4030714)Instruction limit reached! % 19.15/3.66 % (4030714)------------------------------ % 19.15/3.66 % (4030714)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.15/3.66 % (4030714)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.15/3.66 % (4030714)CaDiCaL version: 2.1.3 % 19.15/3.66 % (4030714)Termination reason: Instruction limit % 19.15/3.66 % (4030714)Termination phase: Saturation % 19.15/3.66 % (4030714)Time elapsed: 0.277 s % 19.15/3.66 % (4030714)Peak memory usage: 120 MB % 19.15/3.66 % (4030714)Instructions burned: 417 (million) % 19.15/3.66 % (4030717)Instruction limit reached! % 19.15/3.66 % (4030717)------------------------------ % 19.15/3.66 % (4030717)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.15/3.66 % (4030717)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.15/3.66 % (4030717)CaDiCaL version: 2.1.3 % 19.15/3.66 % (4030717)Termination reason: Instruction limit % 19.15/3.66 % (4030717)Termination phase: Saturation % 19.15/3.66 % (4030717)Time elapsed: 0.215 s % 19.15/3.66 % (4030717)Peak memory usage: 136 MB % 19.15/3.66 % (4030717)Instructions burned: 277 (million) % 19.15/3.66 % (4030728)lrs+1010_1_to=kbo:sil=64000:sas=cadical:si=on:sos=on:bce=on:random_seed=306292013:i=359:rtra=on:gtg=exists_top:ss=axioms_2978 on theBenchmark for (2978ds/359Mi) % 19.15/3.66 % (4030727)Instruction limit reached! % 19.15/3.66 % (4030727)------------------------------ % 19.15/3.66 % (4030727)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.15/3.66 % (4030727)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.15/3.66 % (4030727)CaDiCaL version: 2.1.3 % 19.15/3.66 % (4030727)Termination reason: Instruction limit % 19.15/3.66 % (4030727)Termination phase: Saturation % 19.15/3.66 % (4030727)Time elapsed: 0.127 s % 19.15/3.66 % (4030727)Peak memory usage: 136 MB % 19.15/3.66 % (4030727)Instructions burned: 335 (million) % 19.15/3.66 % (4030719)Instruction limit reached! % 19.15/3.66 % (4030719)------------------------------ % 19.15/3.66 % (4030719)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.15/3.66 % (4030719)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.15/3.66 % (4030719)CaDiCaL version: 2.1.3 % 19.15/3.66 % (4030719)Termination reason: Instruction limit % 19.15/3.66 % (4030719)Termination phase: Saturation % 19.15/3.66 % (4030719)Time elapsed: 0.269 s % 19.15/3.66 % (4030719)Peak memory usage: 119 MB % 19.15/3.66 % (4030719)Instructions burned: 376 (million) % 19.15/3.66 % (4030732)lrs-2_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_max:tha=off:random_seed=1969232174:st=1.5:i=261:sd=1:kws=precedence:rtra=on:ss=axioms_2977 on theBenchmark for (2977ds/261Mi) % 19.15/3.66 % (4030731)dis+1010_1_to=lpo:sil=128000:thi=all:fde=unused:si=on:sp=reverse_arity:tha=off:random_seed=131753540:i=341:gtgl=2:rtra=on:gtg=exists_sym:ev=force:fsd=on:fsdmm=1_2978 on theBenchmark for (2978ds/341Mi) % 24.32/4.06 % (4030722)Instruction limit reached! % 24.32/4.06 % (4030722)------------------------------ % 24.32/4.06 % (4030722)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.32/4.06 % (4030722)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.32/4.06 % (4030722)CaDiCaL version: 2.1.3 % 24.32/4.06 % (4030722)Termination reason: Instruction limit % 24.32/4.06 % (4030722)Termination phase: Saturation % 24.32/4.06 % (4030722)Time elapsed: 0.237 s % 24.32/4.06 % (4030722)Peak memory usage: 119 MB % 24.32/4.06 % (4030722)Instructions burned: 387 (million) % 24.32/4.06 % (4030734)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=1630649014:s2pl=no:i=235:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2976 on theBenchmark for (2976ds/235Mi) % 24.32/4.06 % (4030737)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=3462984000:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2976 on theBenchmark for (2976ds/273Mi) % 24.32/4.06 % (4030728)Instruction limit reached! % 24.32/4.06 % (4030728)------------------------------ % 24.32/4.06 % (4030728)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.32/4.06 % (4030728)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.32/4.06 % (4030728)CaDiCaL version: 2.1.3 % 24.32/4.06 % (4030728)Termination reason: Instruction limit % 24.32/4.06 % (4030728)Termination phase: Saturation % 24.32/4.06 % (4030728)Time elapsed: 0.220 s % 24.32/4.06 % (4030728)Peak memory usage: 92 MB % 24.32/4.06 % (4030728)Instructions burned: 360 (million) % 24.32/4.06 % (4030738)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=2293545641:i=146:doe=on:rtra=on_2976 on theBenchmark for (2976ds/146Mi) % 24.32/4.06 % (4030724)Instruction limit reached! % 24.32/4.06 % (4030724)------------------------------ % 24.32/4.06 % (4030724)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.32/4.06 % (4030724)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.32/4.06 % (4030724)CaDiCaL version: 2.1.3 % 24.32/4.06 % (4030724)Termination reason: Instruction limit % 24.32/4.06 % (4030724)Termination phase: Saturation % 24.32/4.06 % (4030724)Time elapsed: 0.321 s % 24.32/4.06 % (4030724)Peak memory usage: 93 MB % 24.32/4.06 % (4030724)Instructions burned: 514 (million) % 24.32/4.06 % (4030734)Instruction limit reached! % 24.32/4.06 % (4030734)------------------------------ % 24.32/4.06 % (4030734)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.32/4.06 % (4030734)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.32/4.06 % (4030734)CaDiCaL version: 2.1.3 % 24.32/4.06 % (4030734)Termination reason: Instruction limit % 24.32/4.06 % (4030734)Termination phase: Saturation % 24.32/4.06 % (4030734)Time elapsed: 0.097 s % 24.32/4.06 % (4030734)Peak memory usage: 118 MB % 24.32/4.06 % (4030734)Instructions burned: 235 (million) % 24.32/4.06 % (4030732)Instruction limit reached! % 24.32/4.06 % (4030732)------------------------------ % 24.32/4.06 % (4030732)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.32/4.06 % (4030732)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.32/4.06 % (4030732)CaDiCaL version: 2.1.3 % 24.32/4.06 % (4030732)Termination reason: Instruction limit % 24.32/4.06 % (4030732)Termination phase: Saturation % 24.32/4.06 % (4030732)Time elapsed: 0.193 s % 24.32/4.06 % (4030732)Peak memory usage: 119 MB % 24.32/4.06 % (4030732)Instructions burned: 261 (million) % 24.32/4.06 % (4030731)Instruction limit reached! % 24.32/4.06 % (4030731)------------------------------ % 24.32/4.06 % (4030731)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.32/4.06 % (4030731)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.32/4.06 % (4030731)CaDiCaL version: 2.1.3 % 24.32/4.06 % (4030731)Termination reason: Instruction limit % 24.32/4.06 % (4030731)Termination phase: Saturation % 24.32/4.06 % (4030731)Time elapsed: 0.220 s % 24.32/4.06 % (4030731)Peak memory usage: 119 MB % 24.32/4.06 % (4030731)Instructions burned: 342 (million) % 24.32/4.06 % (4030738)Instruction limit reached! % 24.32/4.06 % (4030738)------------------------------ % 24.32/4.06 % (4030738)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.32/4.06 % (4030738)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.32/4.06 % (4030738)CaDiCaL version: 2.1.3 % 26.56/4.49 % (4030738)Termination reason: Instruction limit % 26.56/4.49 % (4030738)Termination phase: Saturation % 26.56/4.49 % (4030738)Time elapsed: 0.099 s % 26.56/4.49 % (4030738)Peak memory usage: 90 MB % 26.56/4.49 % (4030738)Instructions burned: 146 (million) % 26.56/4.49 % (4030742)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=1803980110:i=4428:doe=on:fsr=off:rtra=on_2975 on theBenchmark for (2975ds/4428Mi) % 26.56/4.49 % (4030744)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=3532942837:i=1052:rtra=on_2975 on theBenchmark for (2975ds/1052Mi) % 26.56/4.49 % (4030743)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=1648312761:avsq=on:i=276:avsqr=1,2:rtra=on_2975 on theBenchmark for (2975ds/276Mi) % 26.56/4.49 % (4030737)Instruction limit reached! % 26.56/4.49 % (4030737)------------------------------ % 26.56/4.49 % (4030737)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.56/4.49 % (4030737)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.56/4.49 % (4030737)CaDiCaL version: 2.1.3 % 26.56/4.49 % (4030737)Termination reason: Instruction limit % 26.56/4.49 % (4030737)Termination phase: Saturation % 26.56/4.49 % (4030737)Time elapsed: 0.198 s % 26.56/4.49 % (4030737)Peak memory usage: 93 MB % 26.56/4.49 % (4030737)Instructions burned: 273 (million) % 26.56/4.49 % (4030745)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=1189021991:i=655:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2974 on theBenchmark for (2974ds/655Mi) % 26.56/4.49 % (4030746)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=1212613064:st=5:i=1054:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2974 on theBenchmark for (2974ds/1054Mi) % 26.56/4.49 % (4030747)lrs-1002_1_to=kbo:sas=z3:si=on:norm_ineq=on:sos=on:tha=some:random_seed=4177679104:i=107:rtra=on_2974 on theBenchmark for (2974ds/107Mi) % 26.56/4.49 % (4030747)Refutation not found, incomplete strategy % 26.56/4.49 % (4030747)------------------------------ % 26.56/4.49 % (4030747)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.56/4.49 % (4030747)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.56/4.49 % (4030747)CaDiCaL version: 2.1.3 % 26.56/4.49 % (4030747)Termination reason: Refutation not found, incomplete strategy % 26.56/4.49 % (4030747)Time elapsed: 0.041 s % 26.56/4.49 % (4030747)Peak memory usage: 116 MB % 26.56/4.49 % (4030747)Instructions burned: 25 (million) % 26.56/4.49 % (4030751)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=2406058031:s2a=on:i=450:doe=on:nm=32:rtra=on_2973 on theBenchmark for (2973ds/450Mi) % 26.56/4.49 % (4030743)Instruction limit reached! % 26.56/4.49 % (4030743)------------------------------ % 26.56/4.49 % (4030743)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.56/4.49 % (4030743)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.56/4.49 % (4030743)CaDiCaL version: 2.1.3 % 26.56/4.49 % (4030743)Termination reason: Instruction limit % 26.56/4.49 % (4030743)Termination phase: Saturation % 26.56/4.49 % (4030743)Time elapsed: 0.223 s % 26.56/4.49 % (4030743)Peak memory usage: 136 MB % 26.56/4.49 % (4030743)Instructions burned: 277 (million) % 26.56/4.49 % (4030744)Instruction limit reached! % 26.56/4.49 % (4030744)------------------------------ % 26.56/4.49 % (4030744)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.56/4.49 % (4030744)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.56/4.49 % (4030744)CaDiCaL version: 2.1.3 % 26.56/4.49 % (4030744)Termination reason: Instruction limit % 26.56/4.49 % (4030744)Termination phase: Saturation % 26.56/4.49 % (4030744)Time elapsed: 0.352 s % 26.56/4.49 % (4030744)Peak memory usage: 94 MB % 26.56/4.49 % (4030744)Instructions burned: 1055 (million) % 26.56/4.49 % (4030747)------------------------------ % 26.56/4.49 % (4030747)------------------------------ % 26.56/4.49 % (4030756)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.56/4.49 % (4030756)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=491004051:i=1090:aac=none:nm=0:rtra=on:rawr=on_2971 on theBenchmark for (2971ds/1090Mi) % 26.56/4.49 % (4030757)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=136369688:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2970 on theBenchmark for (2970ds/130Mi) % 31.40/5.05 % (4030757)Instruction limit reached! % 31.40/5.05 % (4030757)------------------------------ % 31.40/5.05 % (4030757)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.40/5.05 % (4030757)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.40/5.05 % (4030757)CaDiCaL version: 2.1.3 % 31.40/5.05 % (4030757)Termination reason: Instruction limit % 31.40/5.05 % (4030757)Termination phase: Saturation % 31.40/5.05 % (4030757)Time elapsed: 0.061 s % 31.40/5.05 % (4030757)Peak memory usage: 119 MB % 31.40/5.05 % (4030757)Instructions burned: 130 (million) % 31.40/5.05 % (4030758)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=3685621304:i=312:kws=inv_frequency:nm=20:rtra=on_2970 on theBenchmark for (2970ds/312Mi) % 31.40/5.05 % (4030745)Instruction limit reached! % 31.40/5.05 % (4030745)------------------------------ % 31.40/5.05 % (4030745)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.40/5.05 % (4030745)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.40/5.05 % (4030745)CaDiCaL version: 2.1.3 % 31.40/5.05 % (4030745)Termination reason: Instruction limit % 31.40/5.05 % (4030745)Termination phase: Saturation % 31.40/5.05 % (4030745)Time elapsed: 0.461 s % 31.40/5.05 % (4030745)Peak memory usage: 96 MB % 31.40/5.05 % (4030745)Instructions burned: 655 (million) % 31.40/5.05 % (4030751)Instruction limit reached! % 31.40/5.05 % (4030751)------------------------------ % 31.40/5.05 % (4030751)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.40/5.05 % (4030751)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.40/5.05 % (4030751)CaDiCaL version: 2.1.3 % 31.40/5.05 % (4030751)Termination reason: Instruction limit % 31.40/5.05 % (4030751)Termination phase: Saturation % 31.40/5.05 % (4030751)Time elapsed: 0.347 s % 31.40/5.05 % (4030751)Peak memory usage: 136 MB % 31.40/5.05 % (4030751)Instructions burned: 451 (million) % 31.40/5.05 % (4030761)ott+10_1_to=kbo:sil=64000:si=on:sp=reverse_frequency:sos=on:random_seed=688323595:i=491:doe=on:rtra=on:gtg=position_2969 on theBenchmark for (2969ds/491Mi) % 31.40/5.05 % (4030763)ott+1011_4:1_to=lpo:sil=64000:si=on:spb=intro:random_seed=3171841719:s2a=on:i=835:s2at=2:rtra=on_2968 on theBenchmark for (2968ds/835Mi) % 31.40/5.05 % (4030764)ott+1011_2_to=lpo:sil=128000:si=on:sos=on:random_seed=3386628372:i=307:bd=preordered:av=off:rtra=on:ev=cautious_2968 on theBenchmark for (2968ds/307Mi) % 31.40/5.05 % (4030758)Instruction limit reached! % 31.40/5.05 % (4030758)------------------------------ % 31.40/5.05 % (4030758)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.40/5.05 % (4030758)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.40/5.05 % (4030758)CaDiCaL version: 2.1.3 % 31.40/5.05 % (4030758)Termination reason: Instruction limit % 31.40/5.05 % (4030758)Termination phase: Saturation % 31.40/5.05 % (4030758)Time elapsed: 0.210 s % 31.40/5.05 % (4030758)Peak memory usage: 120 MB % 31.40/5.05 % (4030758)Instructions burned: 312 (million) % 31.40/5.05 % (4030746)Instruction limit reached! % 31.40/5.05 % (4030746)------------------------------ % 31.40/5.05 % (4030746)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.40/5.05 % (4030746)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.40/5.05 % (4030746)CaDiCaL version: 2.1.3 % 31.40/5.05 % (4030746)Termination reason: Instruction limit % 31.40/5.05 % (4030746)Termination phase: Saturation % 31.40/5.05 % (4030746)Time elapsed: 0.633 s % 31.40/5.05 % (4030746)Peak memory usage: 93 MB % 31.40/5.05 % (4030746)Instructions burned: 1055 (million) % 31.40/5.05 % (4030761)Instruction limit reached! % 31.40/5.05 % (4030761)------------------------------ % 31.40/5.05 % (4030761)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.40/5.05 % (4030761)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.40/5.05 % (4030761)CaDiCaL version: 2.1.3 % 31.40/5.05 % (4030761)Termination reason: Instruction limit % 31.40/5.05 % (4030761)Termination phase: Saturation % 31.40/5.05 % (4030761)Time elapsed: 0.167 s % 31.40/5.05 % (4030761)Peak memory usage: 94 MB % 31.40/5.05 % (4030761)Instructions burned: 491 (million) % 31.40/5.05 % (4030770)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=2112388409:thitd=on:cond=fast:i=784:nm=30:rtra=on:gtg=all:tac=axiom_2966 on theBenchmark for (2966ds/784Mi) % 34.41/5.68 % (4030768)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=873881910:i=776:doe=on:rtra=on_2966 on theBenchmark for (2966ds/776Mi) % 34.41/5.68 % (4030769)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=2007898592:s2a=on:i=646:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2966 on theBenchmark for (2966ds/646Mi) % 34.41/5.68 % (4030764)Instruction limit reached! % 34.41/5.68 % (4030764)------------------------------ % 34.41/5.68 % (4030764)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.41/5.68 % (4030764)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.41/5.68 % (4030764)CaDiCaL version: 2.1.3 % 34.41/5.68 % (4030764)Termination reason: Instruction limit % 34.41/5.68 % (4030764)Termination phase: Saturation % 34.41/5.68 % (4030764)Time elapsed: 0.207 s % 34.41/5.68 % (4030764)Peak memory usage: 92 MB % 34.41/5.68 % (4030764)Instructions burned: 308 (million) % 34.41/5.68 % (4030774)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=2255541714:thitd=on:s2a=on:i=1131:add=on:canc=force:bd=all:rtra=on:tac=axiom:ev=off_2965 on theBenchmark for (2965ds/1131Mi) % 34.41/5.68 % (4030756)Instruction limit reached! % 34.41/5.68 % (4030756)------------------------------ % 34.41/5.68 % (4030756)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.41/5.68 % (4030756)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.41/5.68 % (4030756)CaDiCaL version: 2.1.3 % 34.41/5.68 % (4030756)Termination reason: Instruction limit % 34.41/5.68 % (4030756)Termination phase: Saturation % 34.41/5.68 % (4030756)Time elapsed: 0.694 s % 34.41/5.68 % (4030756)Peak memory usage: 127 MB % 34.41/5.68 % (4030756)Instructions burned: 1091 (million) % 34.41/5.68 % (4030770)Instruction limit reached! % 34.41/5.68 % (4030770)------------------------------ % 34.41/5.68 % (4030770)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.41/5.68 % (4030770)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.41/5.68 % (4030770)CaDiCaL version: 2.1.3 % 34.41/5.68 % (4030770)Termination reason: Instruction limit % 34.41/5.68 % (4030770)Termination phase: Saturation % 34.41/5.68 % (4030770)Time elapsed: 0.289 s % 34.41/5.68 % (4030770)Peak memory usage: 124 MB % 34.41/5.68 % (4030770)Instructions burned: 784 (million) % 34.41/5.68 % (4030777)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=2297185357:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2962 on theBenchmark for (2962ds/775Mi) % 34.41/5.68 % (4030776)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=169854541:s2pl=no:i=246:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2963 on theBenchmark for (2963ds/246Mi) % 34.41/5.68 % (4030769)Instruction limit reached! % 34.41/5.68 % (4030769)------------------------------ % 34.41/5.68 % (4030769)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.41/5.68 % (4030769)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.41/5.68 % (4030769)CaDiCaL version: 2.1.3 % 34.41/5.68 % (4030769)Termination reason: Instruction limit % 34.41/5.68 % (4030769)Termination phase: Saturation % 34.41/5.68 % (4030769)Time elapsed: 0.380 s % 34.41/5.68 % (4030769)Peak memory usage: 137 MB % 34.41/5.68 % (4030769)Instructions burned: 646 (million) % 34.41/5.68 % (4030763)Instruction limit reached! % 34.41/5.68 % (4030763)------------------------------ % 34.41/5.68 % (4030763)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.41/5.68 % (4030763)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.41/5.68 % (4030763)CaDiCaL version: 2.1.3 % 34.41/5.68 % (4030763)Termination reason: Instruction limit % 34.41/5.68 % (4030763)Termination phase: Saturation % 34.41/5.68 % (4030763)Time elapsed: 0.568 s % 34.41/5.68 % (4030763)Peak memory usage: 95 MB % 34.41/5.68 % (4030763)Instructions burned: 835 (million) % 34.41/5.68 % (4030768)Instruction limit reached! % 34.41/5.68 % (4030768)------------------------------ % 34.41/5.68 % (4030768)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.41/5.68 % (4030768)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.41/5.68 % (4030768)CaDiCaL version: 2.1.3 % 34.41/5.68 % (4030768)Termination reason: Instruction limit % 34.41/5.68 % (4030768)Termination phase: Saturation % 49.21/7.62 % (4030768)Time elapsed: 0.427 s % 49.21/7.62 % (4030768)Peak memory usage: 119 MB % 49.21/7.62 % (4030768)Instructions burned: 776 (million) % 49.21/7.62 % (4030780)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=1531458846:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2961 on theBenchmark for (2961ds/273Mi) % 49.21/7.62 % (4030781)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=3799651228:i=102:nm=16:rtra=on_2961 on theBenchmark for (2961ds/102Mi) % 49.21/7.62 % (4030782)lrs+10_1_to=lpo:sil=128000:si=on:bsr=unit_only:tha=off:random_seed=2638083318:avsq=on:s2a=on:i=1094:s2at=5:avsqr=4463,131072:rtra=on_2961 on theBenchmark for (2961ds/1094Mi) % 49.21/7.62 % (4030776)Instruction limit reached! % 49.21/7.62 % (4030776)------------------------------ % 49.21/7.62 % (4030776)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 49.21/7.62 % (4030776)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 49.21/7.62 % (4030776)CaDiCaL version: 2.1.3 % 49.21/7.62 % (4030776)Termination reason: Instruction limit % 49.21/7.62 % (4030776)Termination phase: Saturation % 49.21/7.62 % (4030776)Time elapsed: 0.190 s % 49.21/7.62 % (4030776)Peak memory usage: 119 MB % 49.21/7.62 % (4030776)Instructions burned: 248 (million) % 49.21/7.62 % (4030781)Instruction limit reached! % 49.21/7.62 % (4030781)------------------------------ % 49.21/7.62 % (4030781)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 49.21/7.62 % (4030781)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 49.21/7.62 % (4030781)CaDiCaL version: 2.1.3 % 49.21/7.62 % (4030781)Termination reason: Instruction limit % 49.21/7.62 % (4030781)Termination phase: Saturation % 49.21/7.62 % (4030781)Time elapsed: 0.067 s % 49.21/7.62 % (4030781)Peak memory usage: 89 MB % 49.21/7.62 % (4030781)Instructions burned: 103 (million) % 49.21/7.62 % (4030777)Instruction limit reached! % 49.21/7.62 % (4030777)------------------------------ % 49.21/7.62 % (4030777)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 49.21/7.62 % (4030777)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 49.21/7.62 % (4030777)CaDiCaL version: 2.1.3 % 49.21/7.62 % (4030777)Termination reason: Instruction limit % 49.21/7.62 % (4030777)Termination phase: Saturation % 49.21/7.62 % (4030777)Time elapsed: 0.264 s % 49.21/7.62 % (4030777)Peak memory usage: 95 MB % 49.21/7.62 % (4030777)Instructions burned: 776 (million) % 49.21/7.62 % (4030786)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=3070589696:i=6400:doe=on:fsr=off:rtra=on_2960 on theBenchmark for (2960ds/6400Mi) % 49.21/7.62 % (4030780)Instruction limit reached! % 49.21/7.62 % (4030780)------------------------------ % 49.21/7.62 % (4030780)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 49.21/7.62 % (4030780)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 49.21/7.62 % (4030780)CaDiCaL version: 2.1.3 % 49.21/7.62 % (4030780)Termination reason: Instruction limit % 49.21/7.62 % (4030780)Termination phase: Saturation % 49.21/7.62 % (4030780)Time elapsed: 0.196 s % 49.21/7.62 % (4030780)Peak memory usage: 93 MB % 49.21/7.62 % (4030780)Instructions burned: 273 (million) % 49.21/7.62 % (4030788)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=2280160568:i=1846:canc=cautious:fsr=off:rtra=on_2959 on theBenchmark for (2959ds/1846Mi) % 49.21/7.62 % (4030787)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=1349478895:i=868:doe=on:nm=0:rtra=on:gtg=exists_sym_2959 on theBenchmark for (2959ds/868Mi) % 49.21/7.62 % (4030790)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=2749416256:s2a=on:i=36816:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2958 on theBenchmark for (2958ds/36816Mi) % 49.21/7.62 % (4030774)Instruction limit reached! % 49.21/7.62 % (4030774)------------------------------ % 49.21/7.62 % (4030774)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 49.21/7.62 % (4030774)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 49.21/7.62 % (4030774)CaDiCaL version: 2.1.3 % 49.21/7.62 % (4030774)Termination reason: Instruction limit % 49.21/7.62 % (4030774)Termination phase: Saturation % 49.21/7.62 % (4030774)Time elapsed: 0.785 s % 49.21/7.62 % (4030774)Peak memory usage: 123 MB % 49.21/7.62 % (4030774)Instructions burned: 1132 (million) % 59.81/9.04 % (4030794)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=3463612472:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2955 on theBenchmark for (2955ds/273Mi) % 59.81/9.04 % (4030788)Instruction limit reached! % 59.81/9.04 % (4030788)------------------------------ % 59.81/9.04 % (4030788)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 59.81/9.04 % (4030788)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 59.81/9.04 % (4030788)CaDiCaL version: 2.1.3 % 59.81/9.04 % (4030788)Termination reason: Instruction limit % 59.81/9.04 % (4030788)Termination phase: Saturation % 59.81/9.04 % (4030788)Time elapsed: 0.489 s % 59.81/9.04 % (4030788)Peak memory usage: 96 MB % 59.81/9.04 % (4030788)Instructions burned: 1846 (million) % 59.81/9.04 % (4030782)Instruction limit reached! % 59.81/9.04 % (4030782)------------------------------ % 59.81/9.04 % (4030782)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 59.81/9.04 % (4030782)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 59.81/9.04 % (4030782)CaDiCaL version: 2.1.3 % 59.81/9.04 % (4030782)Termination reason: Instruction limit % 59.81/9.04 % (4030782)Termination phase: Saturation % 59.81/9.04 % (4030782)Time elapsed: 0.669 s % 59.81/9.04 % (4030782)Peak memory usage: 98 MB % 59.81/9.04 % (4030782)Instructions burned: 1094 (million) % 59.81/9.04 % (4030787)Instruction limit reached! % 59.81/9.04 % (4030787)------------------------------ % 59.81/9.04 % (4030787)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 59.81/9.04 % (4030787)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 59.81/9.04 % (4030787)CaDiCaL version: 2.1.3 % 59.81/9.04 % (4030787)Termination reason: Instruction limit % 59.81/9.04 % (4030787)Termination phase: Saturation % 59.81/9.04 % (4030787)Time elapsed: 0.531 s % 59.81/9.04 % (4030787)Peak memory usage: 121 MB % 59.81/9.04 % (4030787)Instructions burned: 868 (million) % 59.81/9.04 % (4030796)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=886830043:i=863:doe=on:nm=0:rtra=on:gtg=exists_sym_2953 on theBenchmark for (2953ds/863Mi) % 59.81/9.04 % (4030794)Instruction limit reached! % 59.81/9.04 % (4030794)------------------------------ % 59.81/9.04 % (4030794)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 59.81/9.04 % (4030794)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 59.81/9.04 % (4030794)CaDiCaL version: 2.1.3 % 59.81/9.04 % (4030794)Termination reason: Instruction limit % 59.81/9.04 % (4030794)Termination phase: Saturation % 59.81/9.04 % (4030794)Time elapsed: 0.194 s % 59.81/9.04 % (4030794)Peak memory usage: 93 MB % 59.81/9.04 % (4030794)Instructions burned: 274 (million) % 59.81/9.04 % (4030797)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=3776060079:i=5811:kws=precedence:nm=0:rtra=on_2953 on theBenchmark for (2953ds/5811Mi) % 59.81/9.04 % (4030798)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=931703192:i=2216:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2953 on theBenchmark for (2953ds/2216Mi) % 59.81/9.04 % (4030800)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=4114218521:i=801:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2952 on theBenchmark for (2952ds/801Mi) % 59.81/9.04 % (4030796)Instruction limit reached! % 59.81/9.04 % (4030796)------------------------------ % 59.81/9.04 % (4030796)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 59.81/9.04 % (4030796)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 59.81/9.04 % (4030796)CaDiCaL version: 2.1.3 % 59.81/9.04 % (4030796)Termination reason: Instruction limit % 59.81/9.04 % (4030796)Termination phase: Saturation % 59.81/9.04 % (4030796)Time elapsed: 0.267 s % 59.81/9.04 % (4030796)Peak memory usage: 120 MB % 59.81/9.04 % (4030796)Instructions burned: 864 (million) % 59.81/9.04 % (4030742)Instruction limit reached! % 59.81/9.04 % (4030742)------------------------------ % 59.81/9.04 % (4030742)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 59.81/9.04 % (4030742)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 59.81/9.04 % (4030742)CaDiCaL version: 2.1.3 % 59.81/9.04 % (4030742)Termination reason: Instruction limit % 59.81/9.04 % (4030742)Termination phase: Saturation % 59.81/9.04 % (4030742)Time elapsed: 2.459 s % 92.04/13.67 % (4030742)Peak memory usage: 111 MB % 92.04/13.67 % (4030742)Instructions burned: 4429 (million) % 92.04/13.67 % (4030804)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=1897088180:st=5:i=1026:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2950 on theBenchmark for (2950ds/1026Mi) % 92.04/13.67 % (4030805)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=987998783:i=3509:rtra=on_2949 on theBenchmark for (2949ds/3509Mi) % 92.04/13.67 % (4030804)Instruction limit reached! % 92.04/13.67 % (4030804)------------------------------ % 92.04/13.67 % (4030804)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 92.04/13.67 % (4030804)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 92.04/13.67 % (4030804)CaDiCaL version: 2.1.3 % 92.04/13.67 % (4030804)Termination reason: Instruction limit % 92.04/13.67 % (4030804)Termination phase: Saturation % 92.04/13.67 % (4030804)Time elapsed: 0.322 s % 92.04/13.67 % (4030804)Peak memory usage: 93 MB % 92.04/13.67 % (4030804)Instructions burned: 1026 (million) % 92.04/13.67 % (4030800)Instruction limit reached! % 92.04/13.67 % (4030800)------------------------------ % 92.04/13.67 % (4030800)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 92.04/13.67 % (4030800)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 92.04/13.67 % (4030800)CaDiCaL version: 2.1.3 % 92.04/13.67 % (4030800)Termination reason: Instruction limit % 92.04/13.67 % (4030800)Termination phase: Saturation % 92.04/13.67 % (4030800)Time elapsed: 0.548 s % 92.04/13.67 % (4030800)Peak memory usage: 96 MB % 92.04/13.67 % (4030800)Instructions burned: 801 (million) % 92.04/13.67 % (4030808)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=2486512086:st=2:i=2127:sd=12:ep=R:rtra=on:ss=axioms_2945 on theBenchmark for (2945ds/2127Mi) % 92.04/13.67 % (4030809)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=2001499142:i=1959:rtra=on:fsd=on:proc=on_2945 on theBenchmark for (2945ds/1959Mi) % 92.04/13.67 % (4030798)Instruction limit reached! % 92.04/13.67 % (4030798)------------------------------ % 92.04/13.67 % (4030798)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 92.04/13.67 % (4030798)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 92.04/13.67 % (4030798)CaDiCaL version: 2.1.3 % 92.04/13.67 % (4030798)Termination reason: Instruction limit % 92.04/13.67 % (4030798)Termination phase: Saturation % 92.04/13.67 % (4030798)Time elapsed: 1.087 s % 92.04/13.67 % (4030798)Peak memory usage: 121 MB % 92.04/13.67 % (4030798)Instructions burned: 2217 (million) % 92.04/13.67 % (4030812)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=3656454310:s2a=on:i=3553:nm=0:rtra=on_2940 on theBenchmark for (2940ds/3553Mi) % 92.04/13.67 % (4030808)Instruction limit reached! % 92.04/13.67 % (4030808)------------------------------ % 92.04/13.67 % (4030808)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 92.04/13.67 % (4030808)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 92.04/13.67 % (4030808)CaDiCaL version: 2.1.3 % 92.04/13.67 % (4030808)Termination reason: Instruction limit % 92.04/13.67 % (4030808)Termination phase: Saturation % 92.04/13.67 % (4030808)Time elapsed: 0.585 s % 92.04/13.67 % (4030808)Peak memory usage: 93 MB % 92.04/13.67 % (4030808)Instructions burned: 2129 (million) % 92.04/13.67 % (4030814)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=936270926:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2939 on theBenchmark for (2939ds/3201Mi) % 92.04/13.67 % (4030809)Instruction limit reached! % 92.04/13.67 % (4030809)------------------------------ % 92.04/13.67 % (4030809)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 92.04/13.67 % (4030809)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 92.04/13.67 % (4030809)CaDiCaL version: 2.1.3 % 92.04/13.67 % (4030809)Termination reason: Instruction limit % 92.04/13.67 % (4030809)Termination phase: Saturation % 92.04/13.67 % (4030809)Time elapsed: 0.979 s % 92.04/13.67 % (4030809)Peak memory usage: 120 MB % 92.04/13.67 % (4030809)Instructions burned: 1960 (million) % 92.04/13.67 % (4030816)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=1579024079:thitd=on:cond=on:i=4093:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2934 on theBenchmark for (2934ds/4093Mi) % 92.04/13.67 % (4030814)Instruction limit reached! % 92.04/13.67 % (4030814)------------------------------ % 112.44/16.56 % (4030814)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 112.44/16.56 % (4030814)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.44/16.56 % (4030814)CaDiCaL version: 2.1.3 % 112.44/16.56 % (4030814)Termination reason: Instruction limit % 112.44/16.56 % (4030814)Termination phase: Saturation % 112.44/16.56 % (4030814)Time elapsed: 0.812 s % 112.44/16.56 % (4030814)Peak memory usage: 93 MB % 112.44/16.56 % (4030814)Instructions burned: 3204 (million) % 112.44/16.56 % (4030818)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=3771887410:cond=fast:i=21173:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2930 on theBenchmark for (2930ds/21173Mi) % 112.44/16.56 % (4030805)Instruction limit reached! % 112.44/16.56 % (4030805)------------------------------ % 112.44/16.56 % (4030805)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 112.44/16.56 % (4030805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.44/16.56 % (4030805)CaDiCaL version: 2.1.3 % 112.44/16.56 % (4030805)Termination reason: Instruction limit % 112.44/16.56 % (4030805)Termination phase: Saturation % 112.44/16.56 % (4030805)Time elapsed: 2.112 s % 112.44/16.56 % (4030805)Peak memory usage: 110 MB % 112.44/16.56 % (4030805)Instructions burned: 3510 (million) % 112.44/16.56 % (4030820)lrs+11_1_to=lpo:thi=all:sas=z3:si=on:fd=off:sac=on:slsq=on:random_seed=3783461306:avsq=on:i=10544:avsqr=17,4:canc=force:rtra=on:gtg=exists_top:er=filter_2927 on theBenchmark for (2927ds/10544Mi) % 112.44/16.56 % (4030786)Instruction limit reached! % 112.44/16.56 % (4030786)------------------------------ % 112.44/16.56 % (4030786)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 112.44/16.56 % (4030786)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.44/16.56 % (4030786)CaDiCaL version: 2.1.3 % 112.44/16.56 % (4030786)Termination reason: Instruction limit % 112.44/16.56 % (4030786)Termination phase: Saturation % 112.44/16.56 % (4030786)Time elapsed: 3.517 s % 112.44/16.56 % (4030786)Peak memory usage: 118 MB % 112.44/16.56 % (4030786)Instructions burned: 6401 (million) % 112.44/16.56 % (4030822)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=2905027624:avsq=on:i=1262:avsqr=1,16:rtra=on:rawr=on_2923 on theBenchmark for (2923ds/1262Mi) % 112.44/16.56 % (4030797)Instruction limit reached! % 112.44/16.56 % (4030797)------------------------------ % 112.44/16.56 % (4030797)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 112.44/16.56 % (4030797)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.44/16.56 % (4030797)CaDiCaL version: 2.1.3 % 112.44/16.56 % (4030797)Termination reason: Instruction limit % 112.44/16.56 % (4030797)Termination phase: Saturation % 112.44/16.56 % (4030797)Time elapsed: 3.271 s % 112.44/16.56 % (4030797)Peak memory usage: 132 MB % 112.44/16.56 % (4030797)Instructions burned: 5813 (million) % 112.44/16.56 % (4030812)Instruction limit reached! % 112.44/16.56 % (4030812)------------------------------ % 112.44/16.56 % (4030812)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 112.44/16.56 % (4030812)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.44/16.56 % (4030812)CaDiCaL version: 2.1.3 % 112.44/16.56 % (4030812)Termination reason: Instruction limit % 112.44/16.56 % (4030812)Termination phase: Saturation % 112.44/16.56 % (4030812)Time elapsed: 2.076 s % 112.44/16.56 % (4030812)Peak memory usage: 104 MB % 112.44/16.56 % (4030812)Instructions burned: 3553 (million) % 112.44/16.56 % (4030824)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=354699303:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2919 on theBenchmark for (2919ds/775Mi) % 112.44/16.56 % (4030825)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=4140384342:i=270:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2918 on theBenchmark for (2918ds/270Mi) % 112.44/16.56 % (4030822)Instruction limit reached! % 112.44/16.56 % (4030822)------------------------------ % 112.44/16.56 % (4030822)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 112.44/16.56 % (4030822)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.44/16.56 % (4030822)CaDiCaL version: 2.1.3 % 112.44/16.56 % (4030822)Termination reason: Instruction limit % 112.44/16.56 % (4030822)Termination phase: Saturation % 112.44/16.56 % (4030822)Time elapsed: 0.613 s % 112.44/16.56 % (4030822)Peak memory usage: 121 MB % 112.44/16.56 % (4030822)Instructions burned: 1264 (million) % 133.60/19.52 % (4030825)Instruction limit reached! % 133.60/19.52 % (4030825)------------------------------ % 133.60/19.52 % (4030825)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 133.60/19.52 % (4030825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 133.60/19.52 % (4030825)CaDiCaL version: 2.1.3 % 133.60/19.52 % (4030825)Termination reason: Instruction limit % 133.60/19.52 % (4030825)Termination phase: Saturation % 133.60/19.52 % (4030825)Time elapsed: 0.188 s % 133.60/19.52 % (4030825)Peak memory usage: 92 MB % 133.60/19.52 % (4030825)Instructions burned: 270 (million) % 133.60/19.52 % (4030828)ott+10_128_isp=bottom:to=lpo:sil=128000:si=on:urr=on:uwa=alasca_main:sac=on:slsq=on:random_seed=55887537:i=17165:aac=none:doe=on:rtra=on:gtg=exists_all_2916 on theBenchmark for (2916ds/17165Mi) % 133.60/19.52 % (4030829)lrs+2_10_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_main:tha=some:random_seed=4140484546:s2a=on:i=13094:s2at=-1:rtra=on_2915 on theBenchmark for (2915ds/13094Mi) % 133.60/19.52 % (4030824)Instruction limit reached! % 133.60/19.52 % (4030824)------------------------------ % 133.60/19.52 % (4030824)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 133.60/19.52 % (4030824)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 133.60/19.52 % (4030824)CaDiCaL version: 2.1.3 % 133.60/19.52 % (4030824)Termination reason: Instruction limit % 133.60/19.52 % (4030824)Termination phase: Saturation % 133.60/19.52 % (4030824)Time elapsed: 0.483 s % 133.60/19.52 % (4030824)Peak memory usage: 94 MB % 133.60/19.52 % (4030824)Instructions burned: 776 (million) % 133.60/19.52 % (4030816)Instruction limit reached! % 133.60/19.52 % (4030816)------------------------------ % 133.60/19.52 % (4030816)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 133.60/19.52 % (4030816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 133.60/19.52 % (4030816)CaDiCaL version: 2.1.3 % 133.60/19.52 % (4030816)Termination reason: Instruction limit % 133.60/19.52 % (4030816)Termination phase: Saturation % 133.60/19.52 % (4030816)Time elapsed: 2.057 s % 133.60/19.52 % (4030816)Peak memory usage: 140 MB % 133.60/19.52 % (4030816)Instructions burned: 4094 (million) % 133.60/19.52 % (4030832)lrs+10_1_to=lpo:sil=128000:si=on:sp=occurrence:random_seed=670026880:st=2:i=12633:rtra=on:ss=axioms_2913 on theBenchmark for (2913ds/12633Mi) % 133.60/19.52 % (4030833)dis+1011_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_frequency:lsd=20:nwc=3:random_seed=1507071929:i=1783:rtra=on:gtg=position_2912 on theBenchmark for (2912ds/1783Mi) % 133.60/19.52 % (4030833)Instruction limit reached! % 133.60/19.52 % (4030833)------------------------------ % 133.60/19.52 % (4030833)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 133.60/19.52 % (4030833)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 133.60/19.52 % (4030833)CaDiCaL version: 2.1.3 % 133.60/19.52 % (4030833)Termination reason: Instruction limit % 133.60/19.52 % (4030833)Termination phase: Saturation % 133.60/19.52 % (4030833)Time elapsed: 1.042 s % 133.60/19.52 % (4030833)Peak memory usage: 123 MB % 133.60/19.52 % (4030833)Instructions burned: 1783 (million) % 133.60/19.52 % (4030836)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=3035751639:i=5451:aac=none:doe=on:nm=0:rtra=on:amm=off:gtg=position_2900 on theBenchmark for (2900ds/5451Mi) % 133.60/19.52 % (4030836)Instruction limit reached! % 133.60/19.52 % (4030836)------------------------------ % 133.60/19.52 % (4030836)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 133.60/19.52 % (4030836)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 133.60/19.52 % (4030836)CaDiCaL version: 2.1.3 % 133.60/19.52 % (4030836)Termination reason: Instruction limit % 133.60/19.52 % (4030836)Termination phase: Saturation % 133.60/19.52 % (4030836)Time elapsed: 2.691 s % 133.60/19.52 % (4030836)Peak memory usage: 126 MB % 133.60/19.52 % (4030836)Instructions burned: 5452 (million) % 133.60/19.52 % (4030838)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=518533983:i=4975:doe=on:nm=0:rtra=on:gtg=exists_sym_2872 on theBenchmark for (2872ds/4975Mi) % 133.60/19.52 % (4030818)Instruction limit reached! % 133.60/19.52 % (4030818)------------------------------ % 133.60/19.52 % (4030818)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 133.60/19.52 % (4030818)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 133.60/19.52 % (4030818)CaDiCaL version: 2.1.3 % 180.56/26.11 % (4030818)Termination reason: Instruction limit % 180.56/26.11 % (4030818)Termination phase: Saturation % 180.56/26.11 % (4030818)Time elapsed: 5.957 s % 180.56/26.11 % (4030818)Peak memory usage: 155 MB % 180.56/26.11 % (4030818)Instructions burned: 21175 (million) % 180.56/26.11 % (4030905)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=2371612184:i=2076:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2869 on theBenchmark for (2869ds/2076Mi) % 180.56/26.11 % (4030905)Instruction limit reached! % 180.56/26.11 % (4030905)------------------------------ % 180.56/26.11 % (4030905)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 180.56/26.11 % (4030905)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.56/26.11 % (4030905)CaDiCaL version: 2.1.3 % 180.56/26.11 % (4030905)Termination reason: Instruction limit % 180.56/26.11 % (4030905)Termination phase: Saturation % 180.56/26.11 % (4030905)Time elapsed: 0.540 s % 180.56/26.11 % (4030905)Peak memory usage: 121 MB % 180.56/26.11 % (4030905)Instructions burned: 2079 (million) % 180.56/26.11 % (4031009)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=1451502835:i=5145:rtra=on_2863 on theBenchmark for (2863ds/5145Mi) % 180.56/26.11 % (4030820)Instruction limit reached! % 180.56/26.11 % (4030820)------------------------------ % 180.56/26.11 % (4030820)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 180.56/26.11 % (4030820)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.56/26.11 % (4030820)CaDiCaL version: 2.1.3 % 180.56/26.11 % (4030820)Termination reason: Instruction limit % 180.56/26.11 % (4030820)Termination phase: Saturation % 180.56/26.11 % (4030820)Time elapsed: 6.401 s % 180.56/26.11 % (4030820)Peak memory usage: 184 MB % 180.56/26.11 % (4030820)Instructions burned: 10546 (million) % 180.56/26.11 % (4031069)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=69300532:i=3509:rtra=on_2861 on theBenchmark for (2861ds/3509Mi) % 180.56/26.11 % (4030832)Instruction limit reached! % 180.56/26.11 % (4030832)------------------------------ % 180.56/26.11 % (4030832)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 180.56/26.11 % (4030832)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.56/26.11 % (4030832)CaDiCaL version: 2.1.3 % 180.56/26.11 % (4030832)Termination reason: Instruction limit % 180.56/26.11 % (4030832)Termination phase: Saturation % 180.56/26.11 % (4030832)Time elapsed: 6.151 s % 180.56/26.11 % (4030832)Peak memory usage: 146 MB % 180.56/26.11 % (4030832)Instructions burned: 12635 (million) % 180.56/26.11 % (4031135)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=95858233:st=2:i=13800:sd=12:ep=R:rtra=on:ss=axioms_2850 on theBenchmark for (2850ds/13800Mi) % 180.56/26.11 % (4030838)Instruction limit reached! % 180.56/26.11 % (4030838)------------------------------ % 180.56/26.11 % (4030838)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 180.56/26.11 % (4030838)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.56/26.11 % (4030838)CaDiCaL version: 2.1.3 % 180.56/26.11 % (4030838)Termination reason: Instruction limit % 180.56/26.11 % (4030838)Termination phase: Saturation % 180.56/26.11 % (4030838)Time elapsed: 2.634 s % 180.56/26.11 % (4030838)Peak memory usage: 123 MB % 180.56/26.11 % (4030838)Instructions burned: 4976 (million) % 180.56/26.11 % (4031163)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=1933791365:i=1412:rtra=on:fsd=on:proc=on_2844 on theBenchmark for (2844ds/1412Mi) % 180.56/26.11 % (4031009)Instruction limit reached! % 180.56/26.11 % (4031009)------------------------------ % 180.56/26.11 % (4031009)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 180.56/26.11 % (4031009)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.56/26.11 % (4031009)CaDiCaL version: 2.1.3 % 180.56/26.11 % (4031009)Termination reason: Instruction limit % 180.56/26.11 % (4031009)Termination phase: Saturation % 180.56/26.11 % (4031009)Time elapsed: 2.012 s % 180.56/26.11 % (4031009)Peak memory usage: 115 MB % 180.56/26.11 % (4031009)Instructions burned: 5148 (million) % 180.56/26.11 % (4031177)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.56/26.11 % (4031177)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=2319764376:i=11747:aac=none:nm=0:rtra=on:rawr=on_2842 on theBenchmark for (2842ds/11747Mi) % 268.32/38.45 % (4031069)Instruction limit reached! % 268.32/38.45 % (4031069)------------------------------ % 268.32/38.45 % (4031069)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 268.32/38.45 % (4031069)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 268.32/38.45 % (4031069)CaDiCaL version: 2.1.3 % 268.32/38.45 % (4031069)Termination reason: Instruction limit % 268.32/38.45 % (4031069)Termination phase: Saturation % 268.32/38.45 % (4031069)Time elapsed: 2.457 s % 268.32/38.45 % (4031069)Peak memory usage: 108 MB % 268.32/38.45 % (4031069)Instructions burned: 3510 (million) % 268.32/38.45 % (4031199)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=1629558115:s2a=on:i=3553:nm=0:rtra=on_2835 on theBenchmark for (2835ds/3553Mi) % 268.32/38.45 % (4031163)Instruction limit reached! % 268.32/38.45 % (4031163)------------------------------ % 268.32/38.45 % (4031163)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 268.32/38.45 % (4031163)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 268.32/38.45 % (4031163)CaDiCaL version: 2.1.3 % 268.32/38.45 % (4031163)Termination reason: Instruction limit % 268.32/38.45 % (4031163)Termination phase: Saturation % 268.32/38.45 % (4031163)Time elapsed: 1.105 s % 268.32/38.45 % (4031163)Peak memory usage: 122 MB % 268.32/38.45 % (4031163)Instructions burned: 1414 (million) % 268.32/38.45 % (4031201)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=3038628225:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2832 on theBenchmark for (2832ds/3201Mi) % 268.32/38.45 % (4030829)Instruction limit reached! % 268.32/38.45 % (4030829)------------------------------ % 268.32/38.45 % (4030829)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 268.32/38.45 % (4030829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 268.32/38.45 % (4030829)CaDiCaL version: 2.1.3 % 268.32/38.45 % (4030829)Termination reason: Instruction limit % 268.32/38.45 % (4030829)Termination phase: Saturation % 268.32/38.45 % (4030829)Time elapsed: 8.414 s % 268.32/38.45 % (4030829)Peak memory usage: 163 MB % 268.32/38.45 % (4030829)Instructions burned: 13094 (million) % 268.32/38.45 % (4031203)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=905719986:thitd=on:cond=on:i=4081:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2830 on theBenchmark for (2830ds/4081Mi) % 268.32/38.45 % (4031201)Instruction limit reached! % 268.32/38.45 % (4031201)------------------------------ % 268.32/38.45 % (4031201)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 268.32/38.45 % (4031201)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 268.32/38.45 % (4031201)CaDiCaL version: 2.1.3 % 268.32/38.45 % (4031201)Termination reason: Instruction limit % 268.32/38.45 % (4031201)Termination phase: Saturation % 268.32/38.45 % (4031201)Time elapsed: 1.545 s % 268.32/38.45 % (4031201)Peak memory usage: 93 MB % 268.32/38.45 % (4031201)Instructions burned: 3203 (million) % 268.32/38.45 % (4031358)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=889026451:cond=fast:i=20260:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2815 on theBenchmark for (2815ds/20260Mi) % 268.32/38.45 % (4031199)Instruction limit reached! % 268.32/38.45 % (4031199)------------------------------ % 268.32/38.45 % (4031199)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 268.32/38.45 % (4031199)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 268.32/38.45 % (4031199)CaDiCaL version: 2.1.3 % 268.32/38.45 % (4031199)Termination reason: Instruction limit % 268.32/38.45 % (4031199)Termination phase: Saturation % 268.32/38.45 % (4031199)Time elapsed: 2.176 s % 268.32/38.45 % (4031199)Peak memory usage: 109 MB % 268.32/38.45 % (4031199)Instructions burned: 3554 (million) % 268.32/38.45 % (4030828)Instruction limit reached! % 268.32/38.45 % (4030828)------------------------------ % 268.32/38.45 % (4030828)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 268.32/38.45 % (4030828)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 268.32/38.45 % (4030828)CaDiCaL version: 2.1.3 % 268.32/38.45 % (4030828)Termination reason: Instruction limit % 268.32/38.45 % (4030828)Termination phase: Saturation % 268.32/38.45 % (4030828)Time elapsed: 10.258 s % 268.32/38.45 % (4030828)Peak memory usage: 168 MB % 268.32/38.45 % (4030828)Instructions burned: 17165 (million) % 268.32/38.45 % (403Terminated %------------------------------------------------------------------------------