%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWX114_1 : TPTP v9.3.1. Released v9.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/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:55 PM UTC 2026 % Result : Timeout 289.12s 41.38s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWX114_1 : TPTP v9.3.1. Released v9.1.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.10/0.18 % Computer : n006.cluster.edu % 0.10/0.18 % Model : x86_64 x86_64 % 0.10/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.18 % Memory : 8046.5625MB % 0.10/0.18 % OS : Linux 6.8.0-71-generic % 0.10/0.18 % CPULimit : 300 % 0.10/0.18 % WCLimit : 300 % 0.10/0.18 % DateTime : Mon Sep 28 15:01:40 UTC 2026 % 0.10/0.19 % CPUTime : % 0.10/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.10/0.22 Running first-order theorem proving % 0.10/0.22 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 3.56/1.16 % (4032180)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule. % 3.56/1.16 % (4032187)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=2104474172:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi) % 3.56/1.16 % (4032190)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=1908158665:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi) % 3.56/1.16 % (4032186)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=492042413:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi) % 3.56/1.16 % (4032188)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=1403023159:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi) % 3.56/1.16 % (4032191)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=2293486464:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi) % 3.56/1.16 % (4032189)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=3839184216:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi) % 3.56/1.16 % (4032185)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=3302413244:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi) % 3.56/1.16 % (4032189)Instruction limit reached! % 3.56/1.16 % (4032189)------------------------------ % 3.56/1.16 % (4032189)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.56/1.16 % (4032189)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.56/1.16 % (4032189)CaDiCaL version: 2.1.3 % 3.56/1.16 % (4032189)Termination reason: Instruction limit % 3.56/1.16 % (4032189)Termination phase: Property scanning % 3.56/1.16 % (4032189)Time elapsed: 0.003 s % 3.56/1.16 % (4032189)Peak memory usage: 86 MB % 3.56/1.16 % (4032189)Instructions burned: 4 (million) % 3.56/1.16 % (4032188)Instruction limit reached! % 3.56/1.16 % (4032188)------------------------------ % 3.56/1.16 % (4032188)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.56/1.16 % (4032188)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.56/1.16 % (4032188)CaDiCaL version: 2.1.3 % 3.56/1.16 % (4032188)Termination reason: Instruction limit % 3.56/1.16 % (4032188)Termination phase: Saturation % 3.56/1.16 % (4032188)Time elapsed: 0.005 s % 3.56/1.16 % (4032188)Peak memory usage: 88 MB % 3.56/1.16 % (4032188)Instructions burned: 9 (million) % 3.56/1.16 % (4032185)Instruction limit reached! % 3.56/1.16 % (4032185)------------------------------ % 3.56/1.16 % (4032185)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.56/1.16 % (4032185)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.56/1.16 % (4032185)CaDiCaL version: 2.1.3 % 3.56/1.16 % (4032185)Termination reason: Instruction limit % 3.56/1.16 % (4032185)Termination phase: Saturation % 3.56/1.16 % (4032185)Time elapsed: 0.027 s % 3.56/1.16 % (4032185)Peak memory usage: 110 MB % 3.56/1.16 % (4032185)Instructions burned: 12 (million) % 3.56/1.16 % (4032187)Instruction limit reached! % 3.56/1.16 % (4032187)------------------------------ % 3.56/1.16 % (4032187)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.56/1.16 % (4032187)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.56/1.16 % (4032187)CaDiCaL version: 2.1.3 % 3.56/1.16 % (4032187)Termination reason: Instruction limit % 3.56/1.16 % (4032187)Termination phase: Saturation % 3.56/1.16 % (4032187)Time elapsed: 0.083 s % 3.56/1.16 % (4032187)Peak memory usage: 118 MB % 3.56/1.16 % (4032187)Instructions burned: 203 (million) % 3.56/1.16 % (4032191)Instruction limit reached! % 3.56/1.16 % (4032191)------------------------------ % 3.56/1.16 % (4032191)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.56/1.16 % (4032191)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.56/1.16 % (4032191)CaDiCaL version: 2.1.3 % 3.56/1.16 % (4032191)Termination reason: Instruction limit % 3.56/1.16 % (4032191)Termination phase: Saturation % 3.56/1.16 % (4032191)Time elapsed: 0.045 s % 3.56/1.16 % (4032191)Peak memory usage: 116 MB % 3.56/1.16 % (4032191)Instructions burned: 34 (million) % 3.56/1.16 % (4032190)Instruction limit reached! % 3.56/1.16 % (4032190)------------------------------ % 3.56/1.16 % (4032190)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.56/1.16 % (4032190)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.93/1.28 % (4032190)CaDiCaL version: 2.1.3 % 3.93/1.28 % (4032190)Termination reason: Instruction limit % 3.93/1.28 % (4032190)Termination phase: Saturation % 3.93/1.28 % (4032190)Time elapsed: 0.055 s % 3.93/1.28 % (4032190)Peak memory usage: 116 MB % 3.93/1.28 % (4032190)Instructions burned: 47 (million) % 3.93/1.28 % (4032202)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=2066324336:i=24:canc=force:rtra=on_2998 on theBenchmark for (2998ds/24Mi) % 3.93/1.28 % (4032202)Instruction limit reached! % 3.93/1.28 % (4032202)------------------------------ % 3.93/1.28 % (4032202)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.93/1.28 % (4032202)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.93/1.28 % (4032202)CaDiCaL version: 2.1.3 % 3.93/1.28 % (4032202)Termination reason: Instruction limit % 3.93/1.28 % (4032202)Termination phase: Saturation % 3.93/1.28 % (4032202)Time elapsed: 0.010 s % 3.93/1.28 % (4032202)Peak memory usage: 89 MB % 3.93/1.28 % (4032202)Instructions burned: 26 (million) % 3.93/1.28 % (4032199)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=3686237508:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2998 on theBenchmark for (2998ds/14Mi) % 3.93/1.28 % (4032200)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=3759970868:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2998 on theBenchmark for (2998ds/29Mi) % 3.93/1.28 % (4032199)Instruction limit reached! % 3.93/1.28 % (4032199)------------------------------ % 3.93/1.28 % (4032199)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.93/1.28 % (4032199)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.93/1.28 % (4032199)CaDiCaL version: 2.1.3 % 3.93/1.28 % (4032199)Termination reason: Instruction limit % 3.93/1.28 % (4032199)Termination phase: Saturation % 3.93/1.28 % (4032199)Time elapsed: 0.009 s % 3.93/1.28 % (4032199)Peak memory usage: 89 MB % 3.93/1.28 % (4032199)Instructions burned: 14 (million) % 3.93/1.28 % (4032200)Instruction limit reached! % 3.93/1.28 % (4032200)------------------------------ % 3.93/1.28 % (4032200)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.93/1.28 % (4032200)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.93/1.28 % (4032200)CaDiCaL version: 2.1.3 % 3.93/1.28 % (4032200)Termination reason: Instruction limit % 3.93/1.28 % (4032200)Termination phase: Saturation % 3.93/1.28 % (4032200)Time elapsed: 0.020 s % 3.93/1.28 % (4032200)Peak memory usage: 89 MB % 3.93/1.28 % (4032200)Instructions burned: 30 (million) % 3.93/1.28 % (4032201)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=3910901475:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/16Mi) % 3.93/1.28 % (4032204)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=43663930:i=85:gtgl=4:rtra=on:gtg=exists_sym_2997 on theBenchmark for (2997ds/85Mi) % 3.93/1.28 % (4032203)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=371298468:i=27:canc=cautious:fsr=off:rtra=on_2998 on theBenchmark for (2998ds/27Mi) % 3.93/1.28 % (4032201)Instruction limit reached! % 3.93/1.28 % (4032201)------------------------------ % 3.93/1.28 % (4032201)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.93/1.28 % (4032201)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.93/1.28 % (4032201)CaDiCaL version: 2.1.3 % 3.93/1.28 % (4032201)Termination reason: Instruction limit % 3.93/1.28 % (4032201)Termination phase: Saturation % 3.93/1.28 % (4032201)Time elapsed: 0.011 s % 3.93/1.28 % (4032201)Peak memory usage: 89 MB % 3.93/1.28 % (4032201)Instructions burned: 18 (million) % 3.93/1.28 % (4032203)Instruction limit reached! % 3.93/1.28 % (4032203)------------------------------ % 3.93/1.28 % (4032203)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.93/1.28 % (4032203)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.93/1.28 % (4032203)CaDiCaL version: 2.1.3 % 3.93/1.28 % (4032203)Termination reason: Instruction limit % 3.93/1.28 % (4032203)Termination phase: Saturation % 3.93/1.28 % (4032203)Time elapsed: 0.016 s % 3.93/1.28 % (4032203)Peak memory usage: 90 MB % 3.93/1.28 % (4032203)Instructions burned: 28 (million) % 3.93/1.28 % (4032206)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=2064508180:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2997 on theBenchmark for (2997ds/2Mi) % 5.00/1.43 % (4032206)Instruction limit reached! % 5.00/1.43 % (4032206)------------------------------ % 5.00/1.43 % (4032206)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.00/1.43 % (4032206)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.00/1.43 % (4032206)CaDiCaL version: 2.1.3 % 5.00/1.43 % (4032206)Termination reason: Instruction limit % 5.00/1.43 % (4032206)Termination phase: Saturation % 5.00/1.43 % (4032206)Time elapsed: 0.003 s % 5.00/1.43 % (4032206)Peak memory usage: 89 MB % 5.00/1.43 % (4032206)Instructions burned: 10 (million) % 5.00/1.43 % (4032186)Instruction limit reached! % 5.00/1.43 % (4032186)------------------------------ % 5.00/1.43 % (4032186)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.00/1.43 % (4032186)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.00/1.43 % (4032186)CaDiCaL version: 2.1.3 % 5.00/1.43 % (4032186)Termination reason: Instruction limit % 5.00/1.43 % (4032186)Termination phase: Saturation % 5.00/1.43 % (4032186)Time elapsed: 0.220 s % 5.00/1.43 % (4032186)Peak memory usage: 117 MB % 5.00/1.43 % (4032186)Instructions burned: 308 (million) % 5.00/1.43 % (4032204)Instruction limit reached! % 5.00/1.43 % (4032204)------------------------------ % 5.00/1.43 % (4032204)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.00/1.43 % (4032204)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.00/1.43 % (4032204)CaDiCaL version: 2.1.3 % 5.00/1.43 % (4032204)Termination reason: Instruction limit % 5.00/1.43 % (4032204)Termination phase: Saturation % 5.00/1.43 % (4032204)Time elapsed: 0.056 s % 5.00/1.43 % (4032204)Peak memory usage: 89 MB % 5.00/1.43 % (4032204)Instructions burned: 88 (million) % 5.00/1.43 % (4032211)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=3466295229:i=4:ep=RST:ins=2:rtra=on_2996 on theBenchmark for (2996ds/4Mi) % 5.00/1.43 % (4032209)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=1141792224:i=181:rtra=on:ss=axioms:ev=cautious_2997 on theBenchmark for (2997ds/181Mi) % 5.00/1.43 % (4032211)Instruction limit reached! % 5.00/1.43 % (4032211)------------------------------ % 5.00/1.43 % (4032211)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.00/1.43 % (4032211)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.00/1.43 % (4032211)CaDiCaL version: 2.1.3 % 5.00/1.43 % (4032211)Termination reason: Instruction limit % 5.00/1.43 % (4032211)Termination phase: Property scanning % 5.00/1.43 % (4032211)Time elapsed: 0.003 s % 5.00/1.43 % (4032211)Peak memory usage: 86 MB % 5.00/1.43 % (4032211)Instructions burned: 4 (million) % 5.00/1.43 % (4032217)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=2074919455:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2996 on theBenchmark for (2996ds/8Mi) % 5.00/1.43 % (4032217)Instruction limit reached! % 5.00/1.43 % (4032217)------------------------------ % 5.00/1.43 % (4032217)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.00/1.43 % (4032217)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.00/1.43 % (4032217)CaDiCaL version: 2.1.3 % 5.00/1.43 % (4032217)Termination reason: Instruction limit % 5.00/1.43 % (4032217)Termination phase: Saturation % 5.00/1.43 % (4032217)Time elapsed: 0.003 s % 5.00/1.43 % (4032217)Peak memory usage: 87 MB % 5.00/1.43 % (4032217)Instructions burned: 10 (million) % 5.00/1.43 % (4032215)lrs+10_1_thi=all:si=on:fd=off:random_seed=3450965326:i=53:rtra=on:gtg=all_2996 on theBenchmark for (2996ds/53Mi) % 5.00/1.43 % (4032214)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=3034205241:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2996 on theBenchmark for (2996ds/66Mi) % 5.00/1.43 % (4032219)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=2262798310:i=2:doe=on:canc=force:asg=cautious:rtra=on_2996 on theBenchmark for (2996ds/2Mi) % 5.00/1.43 % (4032218)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=3110917312:st=3:i=2:rtra=on:ss=axioms_2996 on theBenchmark for (2996ds/2Mi) % 5.00/1.43 % (4032215)Instruction limit reached! % 5.00/1.43 % (4032215)------------------------------ % 5.00/1.43 % (4032215)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.00/1.43 % (4032215)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.32/1.66 % (4032215)CaDiCaL version: 2.1.3 % 6.32/1.66 % (4032215)Termination reason: Instruction limit % 6.32/1.66 % (4032215)Termination phase: Saturation % 6.32/1.66 % (4032215)Time elapsed: 0.059 s % 6.32/1.66 % (4032215)Peak memory usage: 116 MB % 6.32/1.66 % (4032215)Instructions burned: 54 (million) % 6.32/1.66 % (4032219)Instruction limit reached! % 6.32/1.66 % (4032219)------------------------------ % 6.32/1.66 % (4032219)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.32/1.66 % (4032218)Instruction limit reached! % 6.32/1.66 % (4032218)------------------------------ % 6.32/1.66 % (4032218)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.32/1.66 % (4032218)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.32/1.66 % (4032219)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.32/1.66 % (4032218)CaDiCaL version: 2.1.3 % 6.32/1.66 % (4032219)CaDiCaL version: 2.1.3 % 6.32/1.66 % (4032219)Termination reason: Instruction limit % 6.32/1.66 % (4032219)Termination phase: Clausification % 6.32/1.66 % (4032218)Termination reason: Instruction limit % 6.32/1.66 % (4032218)Termination phase: Clausification % 6.32/1.66 % (4032219)Time elapsed: 0.003 s % 6.32/1.66 % (4032218)Time elapsed: 0.003 s % 6.32/1.66 % (4032219)Peak memory usage: 86 MB % 6.32/1.66 % (4032218)Peak memory usage: 86 MB % 6.32/1.66 % (4032219)Instructions burned: 4 (million) % 6.32/1.66 % (4032218)Instructions burned: 4 (million) % 6.32/1.66 % (4032209)Instruction limit reached! % 6.32/1.66 % (4032209)------------------------------ % 6.32/1.66 % (4032209)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.32/1.66 % (4032209)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.32/1.66 % (4032209)CaDiCaL version: 2.1.3 % 6.32/1.66 % (4032209)Termination reason: Instruction limit % 6.32/1.66 % (4032209)Termination phase: Saturation % 6.32/1.66 % (4032209)Time elapsed: 0.104 s % 6.32/1.66 % (4032209)Peak memory usage: 91 MB % 6.32/1.66 % (4032209)Instructions burned: 182 (million) % 6.32/1.66 % (4032225)dis+10_1_si=on:random_seed=316939668:i=10:ep=R:rtra=on_2995 on theBenchmark for (2995ds/10Mi) % 6.32/1.66 % (4032225)Instruction limit reached! % 6.32/1.66 % (4032225)------------------------------ % 6.32/1.66 % (4032225)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.32/1.66 % (4032225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.32/1.66 % (4032225)CaDiCaL version: 2.1.3 % 6.32/1.66 % (4032225)Termination reason: Instruction limit % 6.32/1.66 % (4032225)Termination phase: Saturation % 6.32/1.66 % (4032225)Time elapsed: 0.003 s % 6.32/1.66 % (4032225)Peak memory usage: 88 MB % 6.32/1.66 % (4032225)Instructions burned: 10 (million) % 6.32/1.66 % (4032214)Instruction limit reached! % 6.32/1.66 % (4032214)------------------------------ % 6.32/1.66 % (4032214)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.32/1.66 % (4032214)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.32/1.66 % (4032214)CaDiCaL version: 2.1.3 % 6.32/1.66 % (4032214)Termination reason: Instruction limit % 6.32/1.66 % (4032214)Termination phase: Saturation % 6.32/1.66 % (4032214)Time elapsed: 0.090 s % 6.32/1.66 % (4032214)Peak memory usage: 134 MB % 6.32/1.66 % (4032214)Instructions burned: 66 (million) % 6.32/1.66 % (4032222)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=1413521134:i=127:doe=on:rtra=on_2995 on theBenchmark for (2995ds/127Mi) % 6.32/1.66 % (4032234)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=1774927572:i=370:ep=RS:fsr=off:rtra=on_2994 on theBenchmark for (2994ds/370Mi) % 6.32/1.66 % (4032234)Refutation not found, incomplete strategy % 6.32/1.66 % (4032234)------------------------------ % 6.32/1.66 % (4032234)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.32/1.66 % (4032234)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.32/1.66 % (4032234)CaDiCaL version: 2.1.3 % 6.32/1.66 % (4032234)Termination reason: Refutation not found, incomplete strategy % 6.32/1.66 % (4032234)Time elapsed: 0.005 s % 6.32/1.66 % (4032234)Peak memory usage: 89 MB % 6.32/1.66 % (4032234)Instructions burned: 13 (million) % 6.32/1.66 % (4032229)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=2244199598:i=26:canc=cautious:av=off:rtra=on_2994 on theBenchmark for (2994ds/26Mi) % 6.32/1.66 % (4032230)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=3091180100: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) % 7.54/1.85 % (4032229)Refutation not found, incomplete strategy % 7.54/1.85 % (4032229)------------------------------ % 7.54/1.85 % (4032229)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.54/1.85 % (4032229)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.54/1.85 % (4032229)CaDiCaL version: 2.1.3 % 7.54/1.85 % (4032229)Termination reason: Refutation not found, incomplete strategy % 7.54/1.85 % (4032229)Time elapsed: 0.008 s % 7.54/1.85 % (4032229)Peak memory usage: 89 MB % 7.54/1.85 % (4032229)Instructions burned: 12 (million) % 7.54/1.85 % (4032231)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=3457937748:i=2:fsr=off:rtra=on:inst=on_2994 on theBenchmark for (2994ds/2Mi) % 7.54/1.85 % (4032231)Instruction limit reached! % 7.54/1.85 % (4032231)------------------------------ % 7.54/1.85 % (4032231)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.54/1.85 % (4032231)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.54/1.85 % (4032231)CaDiCaL version: 2.1.3 % 7.54/1.85 % (4032231)Termination reason: Instruction limit % 7.54/1.85 % (4032231)Termination phase: Preprocessing 3 % 7.54/1.85 % (4032231)Time elapsed: 0.002 s % 7.54/1.85 % (4032231)Peak memory usage: 86 MB % 7.54/1.85 % (4032231)Instructions burned: 2 (million) % 7.54/1.85 % (4032230)Instruction limit reached! % 7.54/1.85 % (4032230)------------------------------ % 7.54/1.85 % (4032230)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.54/1.85 % (4032230)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.54/1.85 % (4032230)CaDiCaL version: 2.1.3 % 7.54/1.85 % (4032230)Termination reason: Instruction limit % 7.54/1.85 % (4032230)Termination phase: Saturation % 7.54/1.85 % (4032230)Time elapsed: 0.028 s % 7.54/1.85 % (4032230)Peak memory usage: 89 MB % 7.54/1.85 % (4032230)Instructions burned: 37 (million) % 7.54/1.85 % (4032233)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=3069872539:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2994 on theBenchmark for (2994ds/8Mi) % 7.54/1.85 % (4032233)Instruction limit reached! % 7.54/1.85 % (4032233)------------------------------ % 7.54/1.85 % (4032233)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.54/1.85 % (4032233)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.54/1.85 % (4032233)CaDiCaL version: 2.1.3 % 7.54/1.85 % (4032233)Termination reason: Instruction limit % 7.54/1.85 % (4032233)Termination phase: Saturation % 7.54/1.85 % (4032233)Time elapsed: 0.005 s % 7.54/1.85 % (4032233)Peak memory usage: 88 MB % 7.54/1.85 % (4032233)Instructions burned: 8 (million) % 7.54/1.85 % (4032222)Instruction limit reached! % 7.54/1.85 % (4032222)------------------------------ % 7.54/1.85 % (4032222)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.54/1.85 % (4032222)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.54/1.85 % (4032222)CaDiCaL version: 2.1.3 % 7.54/1.85 % (4032222)Termination reason: Instruction limit % 7.54/1.85 % (4032222)Termination phase: Saturation % 7.54/1.85 % (4032222)Time elapsed: 0.109 s % 7.54/1.85 % (4032222)Peak memory usage: 117 MB % 7.54/1.85 % (4032222)Instructions burned: 128 (million) % 7.54/1.85 % (4032235)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=1062751847:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2994 on theBenchmark for (2994ds/13Mi) % 7.54/1.85 % (4032235)Instruction limit reached! % 7.54/1.85 % (4032235)------------------------------ % 7.54/1.85 % (4032235)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.54/1.85 % (4032235)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.54/1.85 % (4032235)CaDiCaL version: 2.1.3 % 7.54/1.85 % (4032235)Termination reason: Instruction limit % 7.54/1.85 % (4032235)Termination phase: Saturation % 7.54/1.85 % (4032235)Time elapsed: 0.029 s % 7.54/1.85 % (4032235)Peak memory usage: 112 MB % 7.54/1.85 % (4032235)Instructions burned: 14 (million) % 7.54/1.85 % (4032241)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=3150689246:i=226:rtra=on:gtg=position:ss=axioms_2993 on theBenchmark for (2993ds/226Mi) % 7.54/1.85 % (4032234)------------------------------ % 7.54/1.85 % (4032234)------------------------------ % 10.16/2.08 % (4032244)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=2787397224:i=71:rtra=on:gtg=exists_top_2993 on theBenchmark for (2993ds/71Mi) % 10.16/2.08 % (4032243)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=111362151:i=10:rtra=on_2993 on theBenchmark for (2993ds/10Mi) % 10.16/2.08 % (4032243)Instruction limit reached! % 10.16/2.08 % (4032243)------------------------------ % 10.16/2.08 % (4032243)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.16/2.08 % (4032243)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.16/2.08 % (4032243)CaDiCaL version: 2.1.3 % 10.16/2.08 % (4032243)Termination reason: Instruction limit % 10.16/2.08 % (4032243)Termination phase: Saturation % 10.16/2.08 % (4032243)Time elapsed: 0.006 s % 10.16/2.08 % (4032243)Peak memory usage: 88 MB % 10.16/2.08 % (4032243)Instructions burned: 10 (million) % 10.16/2.08 % (4032245)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=536689247:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2993 on theBenchmark for (2993ds/75Mi) % 10.16/2.08 % (4032245)Instruction limit reached! % 10.16/2.08 % (4032245)------------------------------ % 10.16/2.08 % (4032245)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.16/2.08 % (4032245)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.16/2.08 % (4032245)CaDiCaL version: 2.1.3 % 10.16/2.08 % (4032245)Termination reason: Instruction limit % 10.16/2.08 % (4032245)Termination phase: Saturation % 10.16/2.08 % (4032245)Time elapsed: 0.053 s % 10.16/2.08 % (4032245)Peak memory usage: 91 MB % 10.16/2.08 % (4032245)Instructions burned: 76 (million) % 10.16/2.08 % (4032247)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=2848799941:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2992 on theBenchmark for (2992ds/294Mi) % 10.16/2.08 % (4032249)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=894240089:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2992 on theBenchmark for (2992ds/130Mi) % 10.16/2.08 % (4032244)Instruction limit reached! % 10.16/2.08 % (4032244)------------------------------ % 10.16/2.08 % (4032244)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.16/2.08 % (4032244)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.16/2.08 % (4032244)CaDiCaL version: 2.1.3 % 10.16/2.08 % (4032244)Termination reason: Instruction limit % 10.16/2.08 % (4032244)Termination phase: Saturation % 10.16/2.08 % (4032244)Time elapsed: 0.089 s % 10.16/2.08 % (4032244)Peak memory usage: 133 MB % 10.16/2.08 % (4032244)Instructions burned: 71 (million) % 10.16/2.08 % (4032229)------------------------------ % 10.16/2.08 % (4032229)------------------------------ % 10.16/2.08 % (4032249)Instruction limit reached! % 10.16/2.08 % (4032249)------------------------------ % 10.16/2.08 % (4032249)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.16/2.08 % (4032249)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.16/2.08 % (4032249)CaDiCaL version: 2.1.3 % 10.16/2.08 % (4032249)Termination reason: Instruction limit % 10.16/2.08 % (4032249)Termination phase: Saturation % 10.16/2.08 % (4032249)Time elapsed: 0.059 s % 10.16/2.08 % (4032249)Peak memory usage: 118 MB % 10.16/2.08 % (4032249)Instructions burned: 132 (million) % 10.16/2.08 % (4032253)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=2137212356:i=131:rtra=on_2991 on theBenchmark for (2991ds/131Mi) % 10.16/2.08 % (4032241)Instruction limit reached! % 10.16/2.08 % (4032241)------------------------------ % 10.16/2.08 % (4032241)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.16/2.08 % (4032241)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.16/2.08 % (4032241)CaDiCaL version: 2.1.3 % 10.16/2.08 % (4032241)Termination reason: Instruction limit % 10.16/2.08 % (4032241)Termination phase: Saturation % 10.16/2.08 % (4032241)Time elapsed: 0.172 s % 10.16/2.08 % (4032241)Peak memory usage: 119 MB % 10.16/2.08 % (4032241)Instructions burned: 226 (million) % 10.16/2.08 % (4032254)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=3079905140:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2991 on theBenchmark for (2991ds/40Mi) % 10.16/2.08 % (4032257)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=169197517:i=307:rtra=on:gtg=exists_top_2991 on theBenchmark for (2991ds/307Mi) % 10.97/2.36 % (4032260)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=531915348:i=131:canc=cautious:fsr=off:rtra=on_2990 on theBenchmark for (2990ds/131Mi) % 10.97/2.36 % (4032258)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=1329909263:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2991 on theBenchmark for (2991ds/598Mi) % 10.97/2.36 % (4032247)Instruction limit reached! % 10.97/2.36 % (4032247)------------------------------ % 10.97/2.36 % (4032247)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.97/2.36 % (4032247)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.97/2.36 % (4032247)CaDiCaL version: 2.1.3 % 10.97/2.36 % (4032247)Termination reason: Instruction limit % 10.97/2.36 % (4032247)Termination phase: Saturation % 10.97/2.36 % (4032247)Time elapsed: 0.182 s % 10.97/2.36 % (4032247)Peak memory usage: 91 MB % 10.97/2.36 % (4032247)Instructions burned: 295 (million) % 10.97/2.36 % (4032254)Instruction limit reached! % 10.97/2.36 % (4032254)------------------------------ % 10.97/2.36 % (4032254)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.97/2.36 % (4032254)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.97/2.36 % (4032254)CaDiCaL version: 2.1.3 % 10.97/2.36 % (4032254)Termination reason: Instruction limit % 10.97/2.36 % (4032254)Termination phase: Saturation % 10.97/2.36 % (4032254)Time elapsed: 0.067 s % 10.97/2.36 % (4032254)Peak memory usage: 134 MB % 10.97/2.36 % (4032254)Instructions burned: 40 (million) % 10.97/2.36 % (4032253)Instruction limit reached! % 10.97/2.36 % (4032253)------------------------------ % 10.97/2.36 % (4032253)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.97/2.36 % (4032253)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.97/2.36 % (4032253)CaDiCaL version: 2.1.3 % 10.97/2.36 % (4032253)Termination reason: Instruction limit % 10.97/2.36 % (4032253)Termination phase: Saturation % 10.97/2.36 % (4032253)Time elapsed: 0.131 s % 10.97/2.36 % (4032253)Peak memory usage: 136 MB % 10.97/2.36 % (4032253)Instructions burned: 132 (million) % 10.97/2.36 % (4032260)Instruction limit reached! % 10.97/2.36 % (4032260)------------------------------ % 10.97/2.36 % (4032260)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.97/2.36 % (4032260)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.97/2.36 % (4032260)CaDiCaL version: 2.1.3 % 10.97/2.36 % (4032260)Termination reason: Instruction limit % 10.97/2.36 % (4032260)Termination phase: Saturation % 10.97/2.36 % (4032260)Time elapsed: 0.056 s % 10.97/2.36 % (4032260)Peak memory usage: 117 MB % 10.97/2.36 % (4032260)Instructions burned: 131 (million) % 10.97/2.36 % (4032261)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=3713455775:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2990 on theBenchmark for (2990ds/259Mi) % 10.97/2.36 % (4032269)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=1611288441:i=65:nm=16:rtra=on_2989 on theBenchmark for (2989ds/65Mi) % 10.97/2.36 % (4032266)dis+10_1_si=on:random_seed=24240986:s2a=on:i=1000:rtra=on:gtg=exists_all_2989 on theBenchmark for (2989ds/1000Mi) % 10.97/2.36 % (4032267)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=171377265:i=383:fsr=off:rtra=on:ev=force_2989 on theBenchmark for (2989ds/383Mi) % 10.97/2.36 % (4032269)Instruction limit reached! % 10.97/2.36 % (4032269)------------------------------ % 10.97/2.36 % (4032269)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.97/2.36 % (4032269)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.97/2.36 % (4032269)CaDiCaL version: 2.1.3 % 10.97/2.36 % (4032269)Termination reason: Instruction limit % 10.97/2.36 % (4032269)Termination phase: Saturation % 10.97/2.36 % (4032269)Time elapsed: 0.037 s % 10.97/2.36 % (4032269)Peak memory usage: 118 MB % 10.97/2.36 % (4032269)Instructions burned: 65 (million) % 10.97/2.36 % (4032257)Instruction limit reached! % 10.97/2.36 % (4032257)------------------------------ % 10.97/2.36 % (4032257)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.97/2.36 % (4032257)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.97/2.36 % (4032257)CaDiCaL version: 2.1.3 % 10.97/2.36 % (4032257)Termination reason: Instruction limit % 10.97/2.36 % (4032257)Termination phase: Saturation % 13.16/2.65 % (4032257)Time elapsed: 0.192 s % 13.16/2.65 % (4032257)Peak memory usage: 91 MB % 13.16/2.65 % (4032257)Instructions burned: 308 (million) % 13.16/2.65 % (4032268)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=975972846:i=141:doe=on:rtra=on_2989 on theBenchmark for (2989ds/141Mi) % 13.16/2.65 % (4032274)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=2474223427:i=121:nm=16:rtra=on_2988 on theBenchmark for (2988ds/121Mi) % 13.16/2.65 % (4032261)Instruction limit reached! % 13.16/2.65 % (4032261)------------------------------ % 13.16/2.65 % (4032261)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.16/2.65 % (4032261)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.16/2.65 % (4032261)CaDiCaL version: 2.1.3 % 13.16/2.65 % (4032261)Termination reason: Instruction limit % 13.16/2.65 % (4032261)Termination phase: Saturation % 13.16/2.65 % (4032261)Time elapsed: 0.194 s % 13.16/2.65 % (4032261)Peak memory usage: 118 MB % 13.16/2.65 % (4032261)Instructions burned: 259 (million) % 13.16/2.65 % (4032268)Instruction limit reached! % 13.16/2.65 % (4032268)------------------------------ % 13.16/2.65 % (4032268)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.16/2.65 % (4032268)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.16/2.65 % (4032268)CaDiCaL version: 2.1.3 % 13.16/2.65 % (4032268)Termination reason: Instruction limit % 13.16/2.65 % (4032268)Termination phase: Saturation % 13.16/2.65 % (4032268)Time elapsed: 0.086 s % 13.16/2.65 % (4032268)Peak memory usage: 90 MB % 13.16/2.65 % (4032268)Instructions burned: 142 (million) % 13.16/2.65 % (4032274)Instruction limit reached! % 13.16/2.65 % (4032274)------------------------------ % 13.16/2.65 % (4032274)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.16/2.65 % (4032274)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.16/2.65 % (4032274)CaDiCaL version: 2.1.3 % 13.16/2.65 % (4032274)Termination reason: Instruction limit % 13.16/2.65 % (4032274)Termination phase: Saturation % 13.16/2.65 % (4032274)Time elapsed: 0.038 s % 13.16/2.65 % (4032274)Peak memory usage: 89 MB % 13.16/2.65 % (4032274)Instructions burned: 125 (million) % 13.16/2.65 % (4032275)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=1501880184:s2a=on:i=128:s2at=5:ins=3:rtra=on_2987 on theBenchmark for (2987ds/128Mi) % 13.16/2.65 % (4032267)Instruction limit reached! % 13.16/2.65 % (4032267)------------------------------ % 13.16/2.65 % (4032267)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.16/2.65 % (4032267)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.16/2.65 % (4032267)CaDiCaL version: 2.1.3 % 13.16/2.65 % (4032267)Termination reason: Instruction limit % 13.16/2.65 % (4032267)Termination phase: Saturation % 13.16/2.65 % (4032267)Time elapsed: 0.206 s % 13.16/2.65 % (4032267)Peak memory usage: 92 MB % 13.16/2.65 % (4032267)Instructions burned: 384 (million) % 13.16/2.65 % (4032258)Instruction limit reached! % 13.16/2.65 % (4032258)------------------------------ % 13.16/2.65 % (4032258)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.16/2.65 % (4032258)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.16/2.65 % (4032258)CaDiCaL version: 2.1.3 % 13.16/2.65 % (4032258)Termination reason: Instruction limit % 13.16/2.65 % (4032258)Termination phase: Saturation % 13.16/2.65 % (4032258)Time elapsed: 0.373 s % 13.16/2.65 % (4032258)Peak memory usage: 137 MB % 13.16/2.65 % (4032258)Instructions burned: 598 (million) % 13.16/2.65 % (4032281)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=912938416:i=329:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2986 on theBenchmark for (2986ds/329Mi) % 13.16/2.65 % (4032275)Instruction limit reached! % 13.16/2.65 % (4032275)------------------------------ % 13.16/2.65 % (4032275)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.16/2.65 % (4032275)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.16/2.65 % (4032275)CaDiCaL version: 2.1.3 % 13.16/2.65 % (4032275)Termination reason: Instruction limit % 13.16/2.65 % (4032275)Termination phase: Saturation % 13.16/2.65 % (4032275)Time elapsed: 0.104 s % 13.16/2.65 % (4032275)Peak memory usage: 117 MB % 13.16/2.65 % (4032275)Instructions burned: 128 (million) % 13.16/2.65 % (4032279)dis+1010_1_to=kbo:si=on:random_seed=135018709:i=175:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2987 on theBenchmark for (2987ds/175Mi) % 13.86/2.86 % (4032278)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=4230748954:i=39:ins=3:rtra=on_2987 on theBenchmark for (2987ds/39Mi) % 13.86/2.86 % (4032278)Instruction limit reached! % 13.86/2.86 % (4032278)------------------------------ % 13.86/2.86 % (4032278)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.86/2.86 % (4032278)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.86/2.86 % (4032278)CaDiCaL version: 2.1.3 % 13.86/2.86 % (4032278)Termination reason: Instruction limit % 13.86/2.86 % (4032278)Termination phase: Saturation % 13.86/2.86 % (4032278)Time elapsed: 0.049 s % 13.86/2.86 % (4032278)Peak memory usage: 116 MB % 13.86/2.86 % (4032278)Instructions burned: 39 (million) % 13.86/2.86 % (4032282)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=3242615471:s2a=on:i=483:doe=on:nm=32:rtra=on_2986 on theBenchmark for (2986ds/483Mi) % 13.86/2.86 % (4032281)Instruction limit reached! % 13.86/2.86 % (4032281)------------------------------ % 13.86/2.86 % (4032281)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.86/2.86 % (4032281)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.86/2.86 % (4032281)CaDiCaL version: 2.1.3 % 13.86/2.86 % (4032281)Termination reason: Instruction limit % 13.86/2.86 % (4032281)Termination phase: Saturation % 13.86/2.86 % (4032281)Time elapsed: 0.119 s % 13.86/2.86 % (4032281)Peak memory usage: 115 MB % 13.86/2.86 % (4032281)Instructions burned: 331 (million) % 13.86/2.86 % (4032279)Instruction limit reached! % 13.86/2.86 % (4032279)------------------------------ % 13.86/2.86 % (4032279)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.86/2.86 % (4032279)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.86/2.86 % (4032279)CaDiCaL version: 2.1.3 % 13.86/2.86 % (4032279)Termination reason: Instruction limit % 13.86/2.86 % (4032279)Termination phase: Saturation % 13.86/2.86 % (4032279)Time elapsed: 0.096 s % 13.86/2.86 % (4032279)Peak memory usage: 90 MB % 13.86/2.86 % (4032279)Instructions burned: 175 (million) % 13.86/2.86 % (4032284)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=3655462117:thitd=on:i=215:nm=0:rtra=on:ev=force_2985 on theBenchmark for (2985ds/215Mi) % 13.86/2.86 % (4032287)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=3112508086:i=349:rtra=on_2985 on theBenchmark for (2985ds/349Mi) % 13.86/2.86 % (4032291)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=2263929720:i=328:kws=inv_frequency:nm=20:rtra=on_2984 on theBenchmark for (2984ds/328Mi) % 13.86/2.86 % (4032288)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=2625920848:st=2:i=295:rtra=on:ss=axioms_2985 on theBenchmark for (2985ds/295Mi) % 13.86/2.86 % (4032266)Instruction limit reached! % 13.86/2.86 % (4032266)------------------------------ % 13.86/2.86 % (4032266)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.86/2.86 % (4032266)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.86/2.86 % (4032266)CaDiCaL version: 2.1.3 % 13.86/2.86 % (4032266)Termination reason: Instruction limit % 13.86/2.86 % (4032266)Termination phase: Saturation % 13.86/2.86 % (4032266)Time elapsed: 0.452 s % 13.86/2.86 % (4032266)Peak memory usage: 91 MB % 13.86/2.86 % (4032266)Instructions burned: 1000 (million) % 13.86/2.86 % (4032292)dis+1010_1_to=lpo:sil=128000:sas=z3:si=on:nwc=5:random_seed=2582793633:i=281:gtgl=2:rtra=on:gtg=all_2984 on theBenchmark for (2984ds/281Mi) % 13.86/2.86 % (4032284)Instruction limit reached! % 13.86/2.86 % (4032284)------------------------------ % 13.86/2.86 % (4032284)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.86/2.86 % (4032284)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.86/2.86 % (4032284)CaDiCaL version: 2.1.3 % 13.86/2.86 % (4032284)Termination reason: Instruction limit % 13.86/2.86 % (4032284)Termination phase: Saturation % 13.86/2.86 % (4032284)Time elapsed: 0.161 s % 13.86/2.86 % (4032284)Peak memory usage: 135 MB % 13.86/2.86 % (4032284)Instructions burned: 215 (million) % 13.86/2.86 % (4032291)Instruction limit reached! % 13.86/2.86 % (4032291)------------------------------ % 13.86/2.86 % (4032291)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.86/2.86 % (4032291)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.56/3.15 % (4032291)CaDiCaL version: 2.1.3 % 17.56/3.15 % (4032291)Termination reason: Instruction limit % 17.56/3.15 % (4032291)Termination phase: Saturation % 17.56/3.15 % (4032291)Time elapsed: 0.101 s % 17.56/3.15 % (4032291)Peak memory usage: 118 MB % 17.56/3.15 % (4032291)Instructions burned: 328 (million) % 17.56/3.15 % (4032296)lrs+1010_1_to=kbo:sil=128000:si=on:sos=on:urr=on:uwa=alasca_main:random_seed=3209546322:i=484:doe=on:nm=0:av=off:rtra=on:ss=axioms_2983 on theBenchmark for (2983ds/484Mi) % 17.56/3.15 % (4032288)Instruction limit reached! % 17.56/3.15 % (4032288)------------------------------ % 17.56/3.15 % (4032288)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.56/3.15 % (4032288)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.56/3.15 % (4032288)CaDiCaL version: 2.1.3 % 17.56/3.15 % (4032288)Termination reason: Instruction limit % 17.56/3.15 % (4032288)Termination phase: Saturation % 17.56/3.15 % (4032288)Time elapsed: 0.155 s % 17.56/3.15 % (4032288)Peak memory usage: 90 MB % 17.56/3.15 % (4032288)Instructions burned: 297 (million) % 17.56/3.15 % (4032287)Instruction limit reached! % 17.56/3.15 % (4032287)------------------------------ % 17.56/3.15 % (4032287)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.56/3.15 % (4032287)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.56/3.15 % (4032287)CaDiCaL version: 2.1.3 % 17.56/3.15 % (4032287)Termination reason: Instruction limit % 17.56/3.15 % (4032287)Termination phase: Saturation % 17.56/3.15 % (4032287)Time elapsed: 0.232 s % 17.56/3.15 % (4032287)Peak memory usage: 117 MB % 17.56/3.15 % (4032287)Instructions burned: 349 (million) % 17.56/3.15 % (4032299)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=3144996304:i=416:rtra=on:gtg=position:ss=axioms_2982 on theBenchmark for (2982ds/416Mi) % 17.56/3.15 % (4032298)lrs+21_1_to=kbo:sil=128000:thi=neg_eq:si=on:random_seed=2974973438:i=321:canc=force:rtra=on:tac=axiom:ss=axioms:ev=force_2983 on theBenchmark for (2983ds/321Mi) % 17.56/3.15 % (4032292)Instruction limit reached! % 17.56/3.15 % (4032292)------------------------------ % 17.56/3.15 % (4032292)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.56/3.15 % (4032292)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.56/3.15 % (4032292)CaDiCaL version: 2.1.3 % 17.56/3.15 % (4032292)Termination reason: Instruction limit % 17.56/3.15 % (4032292)Termination phase: Saturation % 17.56/3.15 % (4032292)Time elapsed: 0.182 s % 17.56/3.15 % (4032292)Peak memory usage: 118 MB % 17.56/3.15 % (4032292)Instructions burned: 282 (million) % 17.56/3.15 % (4032282)Instruction limit reached! % 17.56/3.15 % (4032282)------------------------------ % 17.56/3.15 % (4032282)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.56/3.15 % (4032282)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.56/3.15 % (4032282)CaDiCaL version: 2.1.3 % 17.56/3.15 % (4032282)Termination reason: Instruction limit % 17.56/3.15 % (4032282)Termination phase: Saturation % 17.56/3.15 % (4032282)Time elapsed: 0.359 s % 17.56/3.15 % (4032282)Peak memory usage: 137 MB % 17.56/3.15 % (4032282)Instructions burned: 483 (million) % 17.56/3.15 % (4032301)lrs+1010_1_to=kbo:tgt=ground:fde=unused:sas=z3:si=on:sp=unary_frequency:gve=force:spb=goal:tha=off:random_seed=3023517367:i=471:thf=on:kws=precedence:rtra=on_2982 on theBenchmark for (2982ds/471Mi) % 17.56/3.15 % (4032302)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=2064245280:avsq=on:i=276:avsqr=1,2:rtra=on_2982 on theBenchmark for (2982ds/276Mi) % 17.56/3.15 % (4032299)Instruction limit reached! % 17.56/3.15 % (4032299)------------------------------ % 17.56/3.15 % (4032299)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.56/3.15 % (4032299)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.56/3.15 % (4032299)CaDiCaL version: 2.1.3 % 17.56/3.15 % (4032299)Termination reason: Instruction limit % 17.56/3.15 % (4032299)Termination phase: Saturation % 17.56/3.15 % (4032299)Time elapsed: 0.142 s % 17.56/3.15 % (4032299)Peak memory usage: 120 MB % 17.56/3.15 % (4032299)Instructions burned: 419 (million) % 17.56/3.15 % (4032305)lrs+1010_2_to=kbo:sil=128000:tgt=ground:fde=unused:sas=z3:si=on:uwa=off:tha=off:nwc=1:random_seed=803213693:i=375:kws=inv_arity_squared:rtra=on_2981 on theBenchmark for (2981ds/375Mi) % 17.56/3.15 % (4032298)Instruction limit reached! % 17.56/3.15 % (4032298)------------------------------ % 18.69/3.62 % (4032298)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.69/3.62 % (4032298)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.69/3.62 % (4032298)CaDiCaL version: 2.1.3 % 18.69/3.62 % (4032298)Termination reason: Instruction limit % 18.69/3.62 % (4032298)Termination phase: Saturation % 18.69/3.62 % (4032298)Time elapsed: 0.165 s % 18.69/3.62 % (4032298)Peak memory usage: 114 MB % 18.69/3.62 % (4032298)Instructions burned: 323 (million) % 18.69/3.62 % (4032306)lrs+10_1_to=kbo:sil=128000:tgt=full:sas=z3:si=on:uwa=func_ext:slsqc=1:flr=on:slsq=on:random_seed=1992840187:i=387:bd=preordered:rtra=on:ss=axioms:sgt=8_2981 on theBenchmark for (2981ds/387Mi) % 18.69/3.62 % (4032296)Instruction limit reached! % 18.69/3.62 % (4032296)------------------------------ % 18.69/3.62 % (4032296)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.69/3.62 % (4032296)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.69/3.62 % (4032296)CaDiCaL version: 2.1.3 % 18.69/3.62 % (4032296)Termination reason: Instruction limit % 18.69/3.62 % (4032296)Termination phase: Saturation % 18.69/3.62 % (4032296)Time elapsed: 0.267 s % 18.69/3.62 % (4032296)Peak memory usage: 94 MB % 18.69/3.62 % (4032296)Instructions burned: 485 (million) % 18.69/3.62 % (4032309)lrs+10_1_to=kbo:sil=128000:fde=none:si=on:norm_ineq=on:urr=on:nwc=0.5:random_seed=526566003:i=513:kws=frequency:bd=all:rtra=on:gtg=exists_all:ss=axioms:sgt=4_2980 on theBenchmark for (2980ds/513Mi) % 18.69/3.62 % (4032312)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=2121602691:i=334:rtra=on_2979 on theBenchmark for (2979ds/334Mi) % 18.69/3.62 % (4032302)Instruction limit reached! % 18.69/3.62 % (4032302)------------------------------ % 18.69/3.62 % (4032302)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.69/3.62 % (4032302)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.69/3.62 % (4032302)CaDiCaL version: 2.1.3 % 18.69/3.62 % (4032302)Termination reason: Instruction limit % 18.69/3.62 % (4032302)Termination phase: Saturation % 18.69/3.62 % (4032302)Time elapsed: 0.221 s % 18.69/3.62 % (4032302)Peak memory usage: 137 MB % 18.69/3.62 % (4032302)Instructions burned: 276 (million) % 18.69/3.62 % (4032313)lrs+1010_1_to=kbo:sil=64000:sas=cadical:si=on:sos=on:bce=on:random_seed=83137984:i=359:rtra=on:gtg=exists_top:ss=axioms_2979 on theBenchmark for (2979ds/359Mi) % 18.69/3.62 % (4032313)Refutation not found, incomplete strategy % 18.69/3.62 % (4032313)------------------------------ % 18.69/3.62 % (4032313)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.69/3.62 % (4032313)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.69/3.62 % (4032313)CaDiCaL version: 2.1.3 % 18.69/3.62 % (4032313)Termination reason: Refutation not found, incomplete strategy % 18.69/3.62 % (4032313)Time elapsed: 0.010 s % 18.69/3.62 % (4032313)Peak memory usage: 90 MB % 18.69/3.62 % (4032313)Instructions burned: 16 (million) % 18.69/3.62 % (4032309)Instruction limit reached! % 18.69/3.62 % (4032309)------------------------------ % 18.69/3.62 % (4032309)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.69/3.62 % (4032309)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.69/3.62 % (4032309)CaDiCaL version: 2.1.3 % 18.69/3.62 % (4032309)Termination reason: Instruction limit % 18.69/3.62 % (4032309)Termination phase: Saturation % 18.69/3.62 % (4032309)Time elapsed: 0.153 s % 18.69/3.62 % (4032309)Peak memory usage: 93 MB % 18.69/3.62 % (4032309)Instructions burned: 514 (million) % 18.69/3.62 % (4032305)Instruction limit reached! % 18.69/3.62 % (4032305)------------------------------ % 18.69/3.62 % (4032305)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.69/3.62 % (4032305)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.69/3.62 % (4032305)CaDiCaL version: 2.1.3 % 18.69/3.62 % (4032305)Termination reason: Instruction limit % 18.69/3.62 % (4032305)Termination phase: Saturation % 18.69/3.62 % (4032305)Time elapsed: 0.234 s % 18.69/3.62 % (4032305)Peak memory usage: 119 MB % 18.69/3.62 % (4032305)Instructions burned: 376 (million) % 18.69/3.62 % (4032301)Instruction limit reached! % 18.69/3.62 % (4032301)------------------------------ % 18.69/3.62 % (4032301)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.69/3.62 % (4032301)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.69/3.62 % (4032301)CaDiCaL version: 2.1.3 % 24.97/4.15 % (4032301)Termination reason: Instruction limit % 24.97/4.15 % (4032301)Termination phase: Saturation % 24.97/4.15 % (4032301)Time elapsed: 0.297 s % 24.97/4.15 % (4032301)Peak memory usage: 121 MB % 24.97/4.15 % (4032301)Instructions burned: 472 (million) % 24.97/4.15 % (4032306)Instruction limit reached! % 24.97/4.15 % (4032306)------------------------------ % 24.97/4.15 % (4032306)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.97/4.15 % (4032306)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.97/4.15 % (4032306)CaDiCaL version: 2.1.3 % 24.97/4.15 % (4032306)Termination reason: Instruction limit % 24.97/4.15 % (4032306)Termination phase: Saturation % 24.97/4.15 % (4032306)Time elapsed: 0.256 s % 24.97/4.15 % (4032306)Peak memory usage: 120 MB % 24.97/4.15 % (4032306)Instructions burned: 387 (million) % 24.97/4.15 % (4032317)dis+1010_1_to=lpo:sil=128000:thi=all:fde=unused:si=on:sp=reverse_arity:tha=off:random_seed=178632894:i=341:gtgl=2:rtra=on:gtg=exists_sym:ev=force:fsd=on:fsdmm=1_2978 on theBenchmark for (2978ds/341Mi) % 24.97/4.15 % (4032318)lrs-2_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_max:tha=off:random_seed=2653335644:st=1.5:i=261:sd=1:kws=precedence:rtra=on:ss=axioms_2978 on theBenchmark for (2978ds/261Mi) % 24.97/4.15 % (4032320)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=3382213400:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2977 on theBenchmark for (2977ds/273Mi) % 24.97/4.15 % (4032319)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=1420972312:s2pl=no:i=235:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2978 on theBenchmark for (2978ds/235Mi) % 24.97/4.15 % (4032312)Instruction limit reached! % 24.97/4.15 % (4032312)------------------------------ % 24.97/4.15 % (4032312)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.97/4.15 % (4032312)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.97/4.15 % (4032312)CaDiCaL version: 2.1.3 % 24.97/4.15 % (4032312)Termination reason: Instruction limit % 24.97/4.15 % (4032312)Termination phase: Saturation % 24.97/4.15 % (4032312)Time elapsed: 0.240 s % 24.97/4.15 % (4032312)Peak memory usage: 137 MB % 24.97/4.15 % (4032312)Instructions burned: 337 (million) % 24.97/4.15 % (4032321)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=3840487239:i=146:doe=on:rtra=on_2977 on theBenchmark for (2977ds/146Mi) % 24.97/4.15 % (4032313)------------------------------ % 24.97/4.15 % (4032313)------------------------------ % 24.97/4.15 % (4032317)Instruction limit reached! % 24.97/4.15 % (4032317)------------------------------ % 24.97/4.15 % (4032317)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.97/4.15 % (4032317)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.97/4.15 % (4032317)CaDiCaL version: 2.1.3 % 24.97/4.15 % (4032317)Termination reason: Instruction limit % 24.97/4.15 % (4032317)Termination phase: Saturation % 24.97/4.15 % (4032317)Time elapsed: 0.183 s % 24.97/4.15 % (4032317)Peak memory usage: 117 MB % 24.97/4.15 % (4032317)Instructions burned: 342 (million) % 24.97/4.15 % (4032321)Instruction limit reached! % 24.97/4.15 % (4032321)------------------------------ % 24.97/4.15 % (4032321)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.97/4.15 % (4032321)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.97/4.15 % (4032321)CaDiCaL version: 2.1.3 % 24.97/4.15 % (4032321)Termination reason: Instruction limit % 24.97/4.15 % (4032321)Termination phase: Saturation % 24.97/4.15 % (4032321)Time elapsed: 0.085 s % 24.97/4.15 % (4032321)Peak memory usage: 90 MB % 24.97/4.15 % (4032321)Instructions burned: 148 (million) % 24.97/4.15 % (4032318)Instruction limit reached! % 24.97/4.15 % (4032318)------------------------------ % 24.97/4.15 % (4032318)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.97/4.15 % (4032318)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.97/4.15 % (4032318)CaDiCaL version: 2.1.3 % 24.97/4.15 % (4032318)Termination reason: Instruction limit % 24.97/4.15 % (4032318)Termination phase: Saturation % 24.97/4.15 % (4032318)Time elapsed: 0.174 s % 24.97/4.15 % (4032318)Peak memory usage: 119 MB % 24.97/4.15 % (4032318)Instructions burned: 262 (million) % 24.97/4.15 % (4032326)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=739941516:i=4428:doe=on:fsr=off:rtra=on_2976 on theBenchmark for (2976ds/4428Mi) % 26.44/4.51 % (4032320)Instruction limit reached! % 26.44/4.51 % (4032320)------------------------------ % 26.44/4.51 % (4032320)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.44/4.51 % (4032320)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.44/4.51 % (4032320)CaDiCaL version: 2.1.3 % 26.44/4.51 % (4032320)Termination reason: Instruction limit % 26.44/4.51 % (4032320)Termination phase: Saturation % 26.44/4.51 % (4032320)Time elapsed: 0.172 s % 26.44/4.51 % (4032320)Peak memory usage: 92 MB % 26.44/4.51 % (4032320)Instructions burned: 275 (million) % 26.44/4.51 % (4032319)Instruction limit reached! % 26.44/4.51 % (4032319)------------------------------ % 26.44/4.51 % (4032319)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.44/4.51 % (4032319)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.44/4.51 % (4032319)CaDiCaL version: 2.1.3 % 26.44/4.51 % (4032319)Termination reason: Instruction limit % 26.44/4.51 % (4032319)Termination phase: Saturation % 26.44/4.51 % (4032319)Time elapsed: 0.181 s % 26.44/4.51 % (4032319)Peak memory usage: 120 MB % 26.44/4.51 % (4032319)Instructions burned: 238 (million) % 26.44/4.51 % (4032328)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=440855698:avsq=on:i=276:avsqr=1,2:rtra=on_2975 on theBenchmark for (2975ds/276Mi) % 26.44/4.51 % (4032329)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=3474840347:i=1052:rtra=on_2975 on theBenchmark for (2975ds/1052Mi) % 26.44/4.51 % (4032330)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=2151818943:i=655:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2975 on theBenchmark for (2975ds/655Mi) % 26.44/4.51 % (4032331)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=816245930:st=5:i=1054:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2975 on theBenchmark for (2975ds/1054Mi) % 26.44/4.51 % (4032333)lrs-1002_1_to=kbo:sas=z3:si=on:norm_ineq=on:sos=on:tha=some:random_seed=3445335937:i=107:rtra=on_2974 on theBenchmark for (2974ds/107Mi) % 26.44/4.51 % (4032334)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=1296020214:s2a=on:i=450:doe=on:nm=32:rtra=on_2974 on theBenchmark for (2974ds/450Mi) % 26.44/4.51 % (4032333)Refutation not found, incomplete strategy % 26.44/4.51 % (4032333)------------------------------ % 26.44/4.51 % (4032333)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.44/4.51 % (4032333)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.44/4.51 % (4032333)CaDiCaL version: 2.1.3 % 26.44/4.51 % (4032333)Termination reason: Refutation not found, incomplete strategy % 26.44/4.51 % (4032333)Time elapsed: 0.036 s % 26.44/4.51 % (4032333)Peak memory usage: 116 MB % 26.44/4.51 % (4032333)Instructions burned: 20 (million) % 26.44/4.51 % (4032328)Instruction limit reached! % 26.44/4.51 % (4032328)------------------------------ % 26.44/4.51 % (4032328)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.44/4.51 % (4032328)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.44/4.51 % (4032328)CaDiCaL version: 2.1.3 % 26.44/4.51 % (4032328)Termination reason: Instruction limit % 26.44/4.51 % (4032328)Termination phase: Saturation % 26.44/4.51 % (4032328)Time elapsed: 0.214 s % 26.44/4.51 % (4032328)Peak memory usage: 136 MB % 26.44/4.51 % (4032328)Instructions burned: 277 (million) % 26.44/4.51 % (4032341)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.44/4.51 % (4032341)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=3712905487:i=1090:aac=none:nm=0:rtra=on:rawr=on_2972 on theBenchmark for (2972ds/1090Mi) % 26.44/4.51 % (4032333)------------------------------ % 26.44/4.51 % (4032333)------------------------------ % 26.44/4.51 % (4032334)Instruction limit reached! % 26.44/4.51 % (4032334)------------------------------ % 26.44/4.51 % (4032334)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.44/4.51 % (4032334)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.44/4.51 % (4032334)CaDiCaL version: 2.1.3 % 26.44/4.51 % (4032334)Termination reason: Instruction limit % 26.44/4.51 % (4032334)Termination phase: Saturation % 27.82/4.90 % (4032334)Time elapsed: 0.319 s % 27.82/4.90 % (4032334)Peak memory usage: 136 MB % 27.82/4.90 % (4032334)Instructions burned: 451 (million) % 27.82/4.90 % (4032343)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=1185014797:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2970 on theBenchmark for (2970ds/130Mi) % 27.82/4.90 % (4032330)Instruction limit reached! % 27.82/4.90 % (4032330)------------------------------ % 27.82/4.90 % (4032330)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.82/4.90 % (4032330)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.82/4.90 % (4032330)CaDiCaL version: 2.1.3 % 27.82/4.90 % (4032330)Termination reason: Instruction limit % 27.82/4.90 % (4032330)Termination phase: Saturation % 27.82/4.90 % (4032330)Time elapsed: 0.436 s % 27.82/4.90 % (4032330)Peak memory usage: 96 MB % 27.82/4.90 % (4032330)Instructions burned: 657 (million) % 27.82/4.90 % (4032344)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=835161057:i=312:kws=inv_frequency:nm=20:rtra=on_2970 on theBenchmark for (2970ds/312Mi) % 27.82/4.90 % (4032343)Instruction limit reached! % 27.82/4.90 % (4032343)------------------------------ % 27.82/4.90 % (4032343)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.82/4.90 % (4032343)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.82/4.90 % (4032343)CaDiCaL version: 2.1.3 % 27.82/4.90 % (4032343)Termination reason: Instruction limit % 27.82/4.90 % (4032343)Termination phase: Saturation % 27.82/4.90 % (4032343)Time elapsed: 0.105 s % 27.82/4.90 % (4032343)Peak memory usage: 118 MB % 27.82/4.90 % (4032343)Instructions burned: 130 (million) % 27.82/4.90 % (4032346)ott+10_1_to=kbo:sil=64000:si=on:sp=reverse_frequency:sos=on:random_seed=4186223091:i=491:doe=on:rtra=on:gtg=position_2969 on theBenchmark for (2969ds/491Mi) % 27.82/4.90 % (4032329)Instruction limit reached! % 27.82/4.90 % (4032329)------------------------------ % 27.82/4.90 % (4032329)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.82/4.90 % (4032329)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.82/4.90 % (4032329)CaDiCaL version: 2.1.3 % 27.82/4.90 % (4032329)Termination reason: Instruction limit % 27.82/4.90 % (4032329)Termination phase: Saturation % 27.82/4.90 % (4032329)Time elapsed: 0.618 s % 27.82/4.90 % (4032329)Peak memory usage: 95 MB % 27.82/4.90 % (4032329)Instructions burned: 1053 (million) % 27.82/4.90 % (4032331)Instruction limit reached! % 27.82/4.90 % (4032331)------------------------------ % 27.82/4.90 % (4032331)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.82/4.90 % (4032331)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.82/4.90 % (4032331)CaDiCaL version: 2.1.3 % 27.82/4.90 % (4032331)Termination reason: Instruction limit % 27.82/4.90 % (4032331)Termination phase: Saturation % 27.82/4.90 % (4032331)Time elapsed: 0.591 s % 27.82/4.90 % (4032331)Peak memory usage: 93 MB % 27.82/4.90 % (4032331)Instructions burned: 1055 (million) % 27.82/4.90 % (4032348)ott+1011_4:1_to=lpo:sil=64000:si=on:spb=intro:random_seed=1090893485:s2a=on:i=835:s2at=2:rtra=on_2968 on theBenchmark for (2968ds/835Mi) % 27.82/4.90 % (4032344)Instruction limit reached! % 27.82/4.90 % (4032344)------------------------------ % 27.82/4.90 % (4032344)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.82/4.90 % (4032344)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.82/4.90 % (4032344)CaDiCaL version: 2.1.3 % 27.82/4.90 % (4032344)Termination reason: Instruction limit % 27.82/4.90 % (4032344)Termination phase: Saturation % 27.82/4.90 % (4032344)Time elapsed: 0.191 s % 27.82/4.90 % (4032344)Peak memory usage: 119 MB % 27.82/4.90 % (4032344)Instructions burned: 313 (million) % 27.82/4.90 % (4032350)ott+1011_2_to=lpo:sil=128000:si=on:sos=on:random_seed=3854760942:i=307:bd=preordered:av=off:rtra=on:ev=cautious_2967 on theBenchmark for (2967ds/307Mi) % 27.82/4.90 % (4032351)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=4244037564:i=776:doe=on:rtra=on_2967 on theBenchmark for (2967ds/776Mi) % 27.82/4.90 % (4032353)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=144184981:s2a=on:i=646:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2966 on theBenchmark for (2966ds/646Mi) % 27.82/4.90 % (4032346)Instruction limit reached! % 27.82/4.90 % (4032346)------------------------------ % 27.82/4.90 % (4032346)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.30/5.72 % (4032346)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.30/5.72 % (4032346)CaDiCaL version: 2.1.3 % 34.30/5.72 % (4032346)Termination reason: Instruction limit % 34.30/5.72 % (4032346)Termination phase: Saturation % 34.30/5.72 % (4032346)Time elapsed: 0.304 s % 34.30/5.72 % (4032346)Peak memory usage: 94 MB % 34.30/5.72 % (4032346)Instructions burned: 491 (million) % 34.30/5.72 % (4032341)Instruction limit reached! % 34.30/5.72 % (4032341)------------------------------ % 34.30/5.72 % (4032341)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.30/5.72 % (4032341)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.30/5.72 % (4032341)CaDiCaL version: 2.1.3 % 34.30/5.72 % (4032341)Termination reason: Instruction limit % 34.30/5.72 % (4032341)Termination phase: Saturation % 34.30/5.72 % (4032341)Time elapsed: 0.635 s % 34.30/5.72 % (4032341)Peak memory usage: 124 MB % 34.30/5.72 % (4032341)Instructions burned: 1091 (million) % 34.30/5.72 % (4032350)Instruction limit reached! % 34.30/5.72 % (4032350)------------------------------ % 34.30/5.72 % (4032350)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.30/5.72 % (4032350)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.30/5.72 % (4032350)CaDiCaL version: 2.1.3 % 34.30/5.72 % (4032350)Termination reason: Instruction limit % 34.30/5.72 % (4032350)Termination phase: Saturation % 34.30/5.72 % (4032350)Time elapsed: 0.213 s % 34.30/5.72 % (4032350)Peak memory usage: 92 MB % 34.30/5.72 % (4032350)Instructions burned: 308 (million) % 34.30/5.72 % (4032357)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=2663539138:thitd=on:cond=fast:i=784:nm=30:rtra=on:gtg=all:tac=axiom_2965 on theBenchmark for (2965ds/784Mi) % 34.30/5.72 % (4032358)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=3726952890:thitd=on:s2a=on:i=1131:add=on:canc=force:bd=all:rtra=on:tac=axiom:ev=off_2964 on theBenchmark for (2964ds/1131Mi) % 34.30/5.72 % (4032359)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=656362546:s2pl=no:i=246:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2964 on theBenchmark for (2964ds/246Mi) % 34.30/5.72 % (4032348)Instruction limit reached! % 34.30/5.72 % (4032348)------------------------------ % 34.30/5.72 % (4032348)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.30/5.72 % (4032348)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.30/5.72 % (4032348)CaDiCaL version: 2.1.3 % 34.30/5.72 % (4032348)Termination reason: Instruction limit % 34.30/5.72 % (4032348)Termination phase: Saturation % 34.30/5.72 % (4032348)Time elapsed: 0.429 s % 34.30/5.72 % (4032348)Peak memory usage: 93 MB % 34.30/5.72 % (4032348)Instructions burned: 836 (million) % 34.30/5.72 % (4032351)Instruction limit reached! % 34.30/5.72 % (4032351)------------------------------ % 34.30/5.72 % (4032351)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.30/5.72 % (4032351)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.30/5.72 % (4032351)CaDiCaL version: 2.1.3 % 34.30/5.72 % (4032351)Termination reason: Instruction limit % 34.30/5.72 % (4032351)Termination phase: Saturation % 34.30/5.72 % (4032351)Time elapsed: 0.388 s % 34.30/5.72 % (4032351)Peak memory usage: 118 MB % 34.30/5.72 % (4032351)Instructions burned: 777 (million) % 34.30/5.72 % (4032326)Instruction limit reached! % 34.30/5.72 % (4032326)------------------------------ % 34.30/5.72 % (4032326)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.30/5.72 % (4032326)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.30/5.72 % (4032326)CaDiCaL version: 2.1.3 % 34.30/5.72 % (4032326)Termination reason: Instruction limit % 34.30/5.72 % (4032326)Termination phase: Saturation % 34.30/5.72 % (4032326)Time elapsed: 1.303 s % 34.30/5.72 % (4032326)Peak memory usage: 112 MB % 34.30/5.72 % (4032326)Instructions burned: 4430 (million) % 34.30/5.72 % (4032363)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=1680564130:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2962 on theBenchmark for (2962ds/775Mi) % 34.30/5.72 % (4032353)Instruction limit reached! % 34.30/5.72 % (4032353)------------------------------ % 34.30/5.72 % (4032353)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.30/5.72 % (4032353)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 46.22/7.16 % (4032353)CaDiCaL version: 2.1.3 % 46.22/7.16 % (4032353)Termination reason: Instruction limit % 46.22/7.16 % (4032353)Termination phase: Saturation % 46.22/7.16 % (4032353)Time elapsed: 0.412 s % 46.22/7.16 % (4032353)Peak memory usage: 138 MB % 46.22/7.16 % (4032353)Instructions burned: 647 (million) % 46.22/7.16 % (4032359)Instruction limit reached! % 46.22/7.16 % (4032359)------------------------------ % 46.22/7.16 % (4032359)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 46.22/7.16 % (4032359)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 46.22/7.16 % (4032359)CaDiCaL version: 2.1.3 % 46.22/7.16 % (4032359)Termination reason: Instruction limit % 46.22/7.16 % (4032359)Termination phase: Saturation % 46.22/7.16 % (4032359)Time elapsed: 0.182 s % 46.22/7.16 % (4032359)Peak memory usage: 118 MB % 46.22/7.16 % (4032359)Instructions burned: 247 (million) % 46.22/7.16 % (4032364)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=491091116:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2962 on theBenchmark for (2962ds/273Mi) % 46.22/7.16 % (4032365)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=1141469826:i=102:nm=16:rtra=on_2961 on theBenchmark for (2961ds/102Mi) % 46.22/7.16 % (4032365)Instruction limit reached! % 46.22/7.16 % (4032365)------------------------------ % 46.22/7.16 % (4032365)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 46.22/7.16 % (4032365)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 46.22/7.16 % (4032365)CaDiCaL version: 2.1.3 % 46.22/7.16 % (4032365)Termination reason: Instruction limit % 46.22/7.16 % (4032365)Termination phase: Saturation % 46.22/7.16 % (4032365)Time elapsed: 0.032 s % 46.22/7.16 % (4032365)Peak memory usage: 89 MB % 46.22/7.16 % (4032365)Instructions burned: 102 (million) % 46.22/7.16 % (4032368)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=1482686973:i=6400:doe=on:fsr=off:rtra=on_2961 on theBenchmark for (2961ds/6400Mi) % 46.22/7.16 % (4032367)lrs+10_1_to=lpo:sil=128000:si=on:bsr=unit_only:tha=off:random_seed=2664501086:avsq=on:s2a=on:i=1094:s2at=5:avsqr=4463,131072:rtra=on_2961 on theBenchmark for (2961ds/1094Mi) % 46.22/7.16 % (4032371)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=3771276356:i=868:doe=on:nm=0:rtra=on:gtg=exists_sym_2960 on theBenchmark for (2960ds/868Mi) % 46.22/7.16 % (4032364)Instruction limit reached! % 46.22/7.16 % (4032364)------------------------------ % 46.22/7.16 % (4032364)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 46.22/7.16 % (4032364)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 46.22/7.16 % (4032364)CaDiCaL version: 2.1.3 % 46.22/7.16 % (4032364)Termination reason: Instruction limit % 46.22/7.16 % (4032364)Termination phase: Saturation % 46.22/7.16 % (4032364)Time elapsed: 0.176 s % 46.22/7.16 % (4032364)Peak memory usage: 92 MB % 46.22/7.16 % (4032364)Instructions burned: 273 (million) % 46.22/7.16 % (4032357)Instruction limit reached! % 46.22/7.16 % (4032357)------------------------------ % 46.22/7.16 % (4032357)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 46.22/7.16 % (4032357)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 46.22/7.16 % (4032357)CaDiCaL version: 2.1.3 % 46.22/7.16 % (4032357)Termination reason: Instruction limit % 46.22/7.16 % (4032357)Termination phase: Saturation % 46.22/7.16 % (4032357)Time elapsed: 0.455 s % 46.22/7.16 % (4032357)Peak memory usage: 119 MB % 46.22/7.16 % (4032357)Instructions burned: 785 (million) % 46.22/7.16 % (4032375)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=1381482493:i=1846:canc=cautious:fsr=off:rtra=on_2959 on theBenchmark for (2959ds/1846Mi) % 46.22/7.16 % (4032376)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=3969463810:s2a=on:i=36816:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2959 on theBenchmark for (2959ds/36816Mi) % 46.22/7.16 % (4032371)Instruction limit reached! % 46.22/7.16 % (4032371)------------------------------ % 46.22/7.16 % (4032371)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 46.22/7.16 % (4032371)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 46.22/7.16 % (4032371)CaDiCaL version: 2.1.3 % 46.22/7.16 % (4032371)Termination reason: Instruction limit % 54.86/8.48 % (4032371)Termination phase: Saturation % 54.86/8.48 % (4032371)Time elapsed: 0.237 s % 54.86/8.48 % (4032371)Peak memory usage: 120 MB % 54.86/8.48 % (4032371)Instructions burned: 872 (million) % 54.86/8.48 % (4032363)Instruction limit reached! % 54.86/8.48 % (4032363)------------------------------ % 54.86/8.48 % (4032363)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 54.86/8.48 % (4032363)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 54.86/8.48 % (4032363)CaDiCaL version: 2.1.3 % 54.86/8.48 % (4032363)Termination reason: Instruction limit % 54.86/8.48 % (4032363)Termination phase: Saturation % 54.86/8.48 % (4032363)Time elapsed: 0.452 s % 54.86/8.48 % (4032363)Peak memory usage: 98 MB % 54.86/8.48 % (4032363)Instructions burned: 775 (million) % 54.86/8.48 % (4032379)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=1562415883:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2957 on theBenchmark for (2957ds/273Mi) % 54.86/8.48 % (4032358)Instruction limit reached! % 54.86/8.48 % (4032358)------------------------------ % 54.86/8.48 % (4032358)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 54.86/8.48 % (4032358)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 54.86/8.48 % (4032358)CaDiCaL version: 2.1.3 % 54.86/8.48 % (4032358)Termination reason: Instruction limit % 54.86/8.48 % (4032358)Termination phase: Saturation % 54.86/8.48 % (4032358)Time elapsed: 0.707 s % 54.86/8.48 % (4032358)Peak memory usage: 123 MB % 54.86/8.48 % (4032358)Instructions burned: 1132 (million) % 54.86/8.48 % (4032379)Instruction limit reached! % 54.86/8.48 % (4032379)------------------------------ % 54.86/8.48 % (4032379)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 54.86/8.48 % (4032379)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 54.86/8.48 % (4032379)CaDiCaL version: 2.1.3 % 54.86/8.48 % (4032379)Termination reason: Instruction limit % 54.86/8.48 % (4032379)Termination phase: Saturation % 54.86/8.48 % (4032379)Time elapsed: 0.096 s % 54.86/8.48 % (4032379)Peak memory usage: 93 MB % 54.86/8.48 % (4032379)Instructions burned: 274 (million) % 54.86/8.48 % (4032380)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=3374414838:i=863:doe=on:nm=0:rtra=on:gtg=exists_sym_2956 on theBenchmark for (2956ds/863Mi) % 54.86/8.48 % (4032382)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=386978569:i=5811:kws=precedence:nm=0:rtra=on_2956 on theBenchmark for (2956ds/5811Mi) % 54.86/8.48 % (4032383)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=3382790095:i=2216:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2955 on theBenchmark for (2955ds/2216Mi) % 54.86/8.48 % (4032367)Instruction limit reached! % 54.86/8.48 % (4032367)------------------------------ % 54.86/8.48 % (4032367)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 54.86/8.48 % (4032367)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 54.86/8.48 % (4032367)CaDiCaL version: 2.1.3 % 54.86/8.48 % (4032367)Termination reason: Instruction limit % 54.86/8.48 % (4032367)Termination phase: Saturation % 54.86/8.48 % (4032367)Time elapsed: 0.657 s % 54.86/8.48 % (4032367)Peak memory usage: 98 MB % 54.86/8.48 % (4032367)Instructions burned: 1095 (million) % 54.86/8.48 % (4032387)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=3993680714:i=801:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2953 on theBenchmark for (2953ds/801Mi) % 54.86/8.48 % (4032380)Instruction limit reached! % 54.86/8.48 % (4032380)------------------------------ % 54.86/8.48 % (4032380)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 54.86/8.48 % (4032380)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 54.86/8.48 % (4032380)CaDiCaL version: 2.1.3 % 54.86/8.48 % (4032380)Termination reason: Instruction limit % 54.86/8.48 % (4032380)Termination phase: Saturation % 54.86/8.48 % (4032380)Time elapsed: 0.432 s % 54.86/8.48 % (4032380)Peak memory usage: 120 MB % 54.86/8.48 % (4032380)Instructions burned: 864 (million) % 54.86/8.48 % (4032389)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=2557254285:st=5:i=1026:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2951 on theBenchmark for (2951ds/1026Mi) % 54.86/8.48 % (4032383)Instruction limit reached! % 54.86/8.48 % (4032383)------------------------------ % 82.96/12.30 % (4032383)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 82.96/12.30 % (4032383)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 82.96/12.30 % (4032383)CaDiCaL version: 2.1.3 % 82.96/12.30 % (4032383)Termination reason: Instruction limit % 82.96/12.30 % (4032383)Termination phase: Saturation % 82.96/12.30 % (4032383)Time elapsed: 0.558 s % 82.96/12.30 % (4032383)Peak memory usage: 122 MB % 82.96/12.30 % (4032383)Instructions burned: 2218 (million) % 82.96/12.30 % (4032391)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=1417541991:i=3509:rtra=on_2949 on theBenchmark for (2949ds/3509Mi) % 82.96/12.30 % (4032375)Instruction limit reached! % 82.96/12.30 % (4032375)------------------------------ % 82.96/12.30 % (4032375)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 82.96/12.30 % (4032375)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 82.96/12.30 % (4032375)CaDiCaL version: 2.1.3 % 82.96/12.30 % (4032375)Termination reason: Instruction limit % 82.96/12.30 % (4032375)Termination phase: Saturation % 82.96/12.30 % (4032375)Time elapsed: 0.996 s % 82.96/12.30 % (4032375)Peak memory usage: 101 MB % 82.96/12.30 % (4032375)Instructions burned: 1846 (million) % 82.96/12.30 % (4032387)Instruction limit reached! % 82.96/12.30 % (4032387)------------------------------ % 82.96/12.30 % (4032387)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 82.96/12.30 % (4032387)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 82.96/12.30 % (4032387)CaDiCaL version: 2.1.3 % 82.96/12.30 % (4032387)Termination reason: Instruction limit % 82.96/12.30 % (4032387)Termination phase: Saturation % 82.96/12.30 % (4032387)Time elapsed: 0.498 s % 82.96/12.30 % (4032387)Peak memory usage: 96 MB % 82.96/12.30 % (4032387)Instructions burned: 802 (million) % 82.96/12.30 % (4032393)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=4251809687:st=2:i=2127:sd=12:ep=R:rtra=on:ss=axioms_2948 on theBenchmark for (2948ds/2127Mi) % 82.96/12.30 % (4032394)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=3383188197:i=1959:rtra=on:fsd=on:proc=on_2947 on theBenchmark for (2947ds/1959Mi) % 82.96/12.30 % (4032389)Instruction limit reached! % 82.96/12.30 % (4032389)------------------------------ % 82.96/12.30 % (4032389)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 82.96/12.30 % (4032389)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 82.96/12.30 % (4032389)CaDiCaL version: 2.1.3 % 82.96/12.30 % (4032389)Termination reason: Instruction limit % 82.96/12.30 % (4032389)Termination phase: Saturation % 82.96/12.30 % (4032389)Time elapsed: 0.534 s % 82.96/12.30 % (4032389)Peak memory usage: 93 MB % 82.96/12.30 % (4032389)Instructions burned: 1026 (million) % 82.96/12.30 % (4032397)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=3191397814:s2a=on:i=3553:nm=0:rtra=on_2944 on theBenchmark for (2944ds/3553Mi) % 82.96/12.30 % (4032391)Instruction limit reached! % 82.96/12.30 % (4032391)------------------------------ % 82.96/12.30 % (4032391)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 82.96/12.30 % (4032391)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 82.96/12.30 % (4032391)CaDiCaL version: 2.1.3 % 82.96/12.30 % (4032391)Termination reason: Instruction limit % 82.96/12.30 % (4032391)Termination phase: Saturation % 82.96/12.30 % (4032391)Time elapsed: 0.771 s % 82.96/12.30 % (4032391)Peak memory usage: 96 MB % 82.96/12.30 % (4032391)Instructions burned: 3512 (million) % 82.96/12.30 % (4032399)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=693639180:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2940 on theBenchmark for (2940ds/3201Mi) % 82.96/12.30 % (4032393)Instruction limit reached! % 82.96/12.30 % (4032393)------------------------------ % 82.96/12.30 % (4032393)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 82.96/12.30 % (4032393)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 82.96/12.30 % (4032393)CaDiCaL version: 2.1.3 % 82.96/12.30 % (4032393)Termination reason: Instruction limit % 82.96/12.30 % (4032393)Termination phase: Saturation % 82.96/12.30 % (4032393)Time elapsed: 1.062 s % 82.96/12.30 % (4032393)Peak memory usage: 94 MB % 82.96/12.30 % (4032393)Instructions burned: 2128 (million) % 82.96/12.30 % (4032401)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=3844619285:thitd=on:cond=on:i=4093:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2936 on theBenchmark for (2936ds/4093Mi) % 99.66/14.73 % (4032394)Instruction limit reached! % 99.66/14.73 % (4032394)------------------------------ % 99.66/14.73 % (4032394)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 99.66/14.73 % (4032394)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.66/14.73 % (4032394)CaDiCaL version: 2.1.3 % 99.66/14.73 % (4032394)Termination reason: Instruction limit % 99.66/14.73 % (4032394)Termination phase: Saturation % 99.66/14.73 % (4032394)Time elapsed: 1.115 s % 99.66/14.73 % (4032394)Peak memory usage: 126 MB % 99.66/14.73 % (4032394)Instructions burned: 1959 (million) % 99.66/14.73 % (4032403)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=308876410:cond=fast:i=21173:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2934 on theBenchmark for (2934ds/21173Mi) % 99.66/14.73 % (4032399)Instruction limit reached! % 99.66/14.73 % (4032399)------------------------------ % 99.66/14.73 % (4032399)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 99.66/14.73 % (4032399)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.66/14.73 % (4032399)CaDiCaL version: 2.1.3 % 99.66/14.73 % (4032399)Termination reason: Instruction limit % 99.66/14.73 % (4032399)Termination phase: Saturation % 99.66/14.73 % (4032399)Time elapsed: 0.825 s % 99.66/14.73 % (4032399)Peak memory usage: 94 MB % 99.66/14.73 % (4032399)Instructions burned: 3203 (million) % 99.66/14.73 % (4032405)lrs+11_1_to=lpo:thi=all:sas=z3:si=on:fd=off:sac=on:slsq=on:random_seed=4034921408:avsq=on:i=10544:avsqr=17,4:canc=force:rtra=on:gtg=exists_top:er=filter_2931 on theBenchmark for (2931ds/10544Mi) % 99.66/14.73 % (4032397)Instruction limit reached! % 99.66/14.73 % (4032397)------------------------------ % 99.66/14.73 % (4032397)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 99.66/14.73 % (4032397)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.66/14.73 % (4032397)CaDiCaL version: 2.1.3 % 99.66/14.73 % (4032397)Termination reason: Instruction limit % 99.66/14.73 % (4032397)Termination phase: Saturation % 99.66/14.73 % (4032397)Time elapsed: 1.598 s % 99.66/14.73 % (4032397)Peak memory usage: 106 MB % 99.66/14.73 % (4032397)Instructions burned: 3553 (million) % 99.66/14.73 % (4032407)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=2257835054:avsq=on:i=1262:avsqr=1,16:rtra=on:rawr=on_2927 on theBenchmark for (2927ds/1262Mi) % 99.66/14.73 % (4032382)Instruction limit reached! % 99.66/14.73 % (4032382)------------------------------ % 99.66/14.73 % (4032382)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 99.66/14.73 % (4032382)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.66/14.73 % (4032382)CaDiCaL version: 2.1.3 % 99.66/14.73 % (4032382)Termination reason: Instruction limit % 99.66/14.73 % (4032382)Termination phase: Saturation % 99.66/14.73 % (4032382)Time elapsed: 2.984 s % 99.66/14.73 % (4032382)Peak memory usage: 131 MB % 99.66/14.73 % (4032382)Instructions burned: 5812 (million) % 99.66/14.73 % (4032368)Instruction limit reached! % 99.66/14.73 % (4032368)------------------------------ % 99.66/14.73 % (4032368)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 99.66/14.73 % (4032368)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.66/14.73 % (4032368)CaDiCaL version: 2.1.3 % 99.66/14.73 % (4032368)Termination reason: Instruction limit % 99.66/14.73 % (4032368)Termination phase: Saturation % 99.66/14.73 % (4032368)Time elapsed: 3.543 s % 99.66/14.73 % (4032368)Peak memory usage: 121 MB % 99.66/14.73 % (4032368)Instructions burned: 6401 (million) % 99.66/14.73 % (4032409)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=1291785368:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2924 on theBenchmark for (2924ds/775Mi) % 99.66/14.73 % (4032410)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=1519519023:i=270:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2924 on theBenchmark for (2924ds/270Mi) % 99.66/14.73 % (4032410)Instruction limit reached! % 99.66/14.73 % (4032410)------------------------------ % 99.66/14.73 % (4032410)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 99.66/14.73 % (4032410)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.66/14.73 % (4032410)CaDiCaL version: 2.1.3 % 99.66/14.73 % (4032410)Termination reason: Instruction limit % 117.66/17.24 % (4032410)Termination phase: Saturation % 117.66/17.24 % (4032410)Time elapsed: 0.161 s % 117.66/17.24 % (4032410)Peak memory usage: 92 MB % 117.66/17.24 % (4032410)Instructions burned: 271 (million) % 117.66/17.24 % (4032413)ott+10_128_isp=bottom:to=lpo:sil=128000:si=on:urr=on:uwa=alasca_main:sac=on:slsq=on:random_seed=508988382:i=17165:aac=none:doe=on:rtra=on:gtg=exists_all_2921 on theBenchmark for (2921ds/17165Mi) % 117.66/17.24 % (4032409)Instruction limit reached! % 117.66/17.24 % (4032409)------------------------------ % 117.66/17.24 % (4032409)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 117.66/17.24 % (4032409)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.66/17.24 % (4032409)CaDiCaL version: 2.1.3 % 117.66/17.24 % (4032409)Termination reason: Instruction limit % 117.66/17.24 % (4032409)Termination phase: Saturation % 117.66/17.24 % (4032409)Time elapsed: 0.349 s % 117.66/17.24 % (4032409)Peak memory usage: 93 MB % 117.66/17.24 % (4032409)Instructions burned: 775 (million) % 117.66/17.24 % (4032407)Instruction limit reached! % 117.66/17.24 % (4032407)------------------------------ % 117.66/17.24 % (4032407)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 117.66/17.24 % (4032407)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.66/17.24 % (4032407)CaDiCaL version: 2.1.3 % 117.66/17.24 % (4032407)Termination reason: Instruction limit % 117.66/17.24 % (4032407)Termination phase: Saturation % 117.66/17.24 % (4032407)Time elapsed: 0.613 s % 117.66/17.24 % (4032407)Peak memory usage: 120 MB % 117.66/17.24 % (4032407)Instructions burned: 1263 (million) % 117.66/17.24 % (4032415)lrs+2_10_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_main:tha=some:random_seed=1242632265:s2a=on:i=13094:s2at=-1:rtra=on_2920 on theBenchmark for (2920ds/13094Mi) % 117.66/17.24 % (4032416)lrs+10_1_to=lpo:sil=128000:si=on:sp=occurrence:random_seed=1200385666:st=2:i=12633:rtra=on:ss=axioms_2919 on theBenchmark for (2919ds/12633Mi) % 117.66/17.24 % (4032401)Instruction limit reached! % 117.66/17.24 % (4032401)------------------------------ % 117.66/17.24 % (4032401)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 117.66/17.24 % (4032401)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.66/17.24 % (4032401)CaDiCaL version: 2.1.3 % 117.66/17.24 % (4032401)Termination reason: Instruction limit % 117.66/17.24 % (4032401)Termination phase: Saturation % 117.66/17.24 % (4032401)Time elapsed: 1.970 s % 117.66/17.24 % (4032401)Peak memory usage: 139 MB % 117.66/17.24 % (4032401)Instructions burned: 4094 (million) % 117.66/17.24 % (4032419)dis+1011_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_frequency:lsd=20:nwc=3:random_seed=2851262685:i=1783:rtra=on:gtg=position_2915 on theBenchmark for (2915ds/1783Mi) % 117.66/17.24 % (4032419)Instruction limit reached! % 117.66/17.24 % (4032419)------------------------------ % 117.66/17.24 % (4032419)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 117.66/17.24 % (4032419)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.66/17.24 % (4032419)CaDiCaL version: 2.1.3 % 117.66/17.24 % (4032419)Termination reason: Instruction limit % 117.66/17.24 % (4032419)Termination phase: Saturation % 117.66/17.24 % (4032419)Time elapsed: 1.051 s % 117.66/17.24 % (4032419)Peak memory usage: 126 MB % 117.66/17.24 % (4032419)Instructions burned: 1784 (million) % 117.66/17.24 % (4032421)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=3687577387:i=5451:aac=none:doe=on:nm=0:rtra=on:amm=off:gtg=position_2903 on theBenchmark for (2903ds/5451Mi) % 117.66/17.24 % (4032405)Instruction limit reached! % 117.66/17.24 % (4032405)------------------------------ % 117.66/17.24 % (4032405)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 117.66/17.24 % (4032405)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.66/17.24 % (4032405)CaDiCaL version: 2.1.3 % 117.66/17.24 % (4032405)Termination reason: Instruction limit % 117.66/17.24 % (4032405)Termination phase: Saturation % 117.66/17.24 % (4032405)Time elapsed: 3.371 s % 117.66/17.24 % (4032405)Peak memory usage: 180 MB % 117.66/17.24 % (4032405)Instructions burned: 10544 (million) % 117.66/17.24 % (4032423)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=1220245896:i=4975:doe=on:nm=0:rtra=on:gtg=exists_sym_2896 on theBenchmark for (2896ds/4975Mi) % 117.66/17.24 % (4032423)Instruction limit reached! % 117.66/17.24 % (4032423)------------------------------ % 117.66/17.24 % (4032423)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 155.39/22.60 % (4032423)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.39/22.60 % (4032423)CaDiCaL version: 2.1.3 % 155.39/22.60 % (4032423)Termination reason: Instruction limit % 155.39/22.60 % (4032423)Termination phase: Saturation % 155.39/22.60 % (4032423)Time elapsed: 1.260 s % 155.39/22.60 % (4032423)Peak memory usage: 122 MB % 155.39/22.60 % (4032423)Instructions burned: 4980 (million) % 155.39/22.60 % (4032425)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=806980796:i=2076:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2883 on theBenchmark for (2883ds/2076Mi) % 155.39/22.60 % (4032425)Instruction limit reached! % 155.39/22.60 % (4032425)------------------------------ % 155.39/22.60 % (4032425)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 155.39/22.60 % (4032425)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.39/22.60 % (4032425)CaDiCaL version: 2.1.3 % 155.39/22.60 % (4032425)Termination reason: Instruction limit % 155.39/22.60 % (4032425)Termination phase: Saturation % 155.39/22.60 % (4032425)Time elapsed: 0.534 s % 155.39/22.60 % (4032425)Peak memory usage: 122 MB % 155.39/22.60 % (4032425)Instructions burned: 2077 (million) % 155.39/22.60 % (4032427)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=1949782605:i=5145:rtra=on_2877 on theBenchmark for (2877ds/5145Mi) % 155.39/22.60 % (4032421)Instruction limit reached! % 155.39/22.60 % (4032421)------------------------------ % 155.39/22.60 % (4032421)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 155.39/22.60 % (4032421)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.39/22.60 % (4032421)CaDiCaL version: 2.1.3 % 155.39/22.60 % (4032421)Termination reason: Instruction limit % 155.39/22.60 % (4032421)Termination phase: Saturation % 155.39/22.60 % (4032421)Time elapsed: 2.627 s % 155.39/22.60 % (4032421)Peak memory usage: 123 MB % 155.39/22.60 % (4032421)Instructions burned: 5454 (million) % 155.39/22.60 % (4032429)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=2326207685:i=3509:rtra=on_2875 on theBenchmark for (2875ds/3509Mi) % 155.39/22.60 % (4032416)Instruction limit reached! % 155.39/22.60 % (4032416)------------------------------ % 155.39/22.60 % (4032416)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 155.39/22.60 % (4032416)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.39/22.60 % (4032416)CaDiCaL version: 2.1.3 % 155.39/22.60 % (4032416)Termination reason: Instruction limit % 155.39/22.60 % (4032416)Termination phase: Saturation % 155.39/22.60 % (4032416)Time elapsed: 4.538 s % 155.39/22.60 % (4032416)Peak memory usage: 95 MB % 155.39/22.60 % (4032416)Instructions burned: 12636 (million) % 155.39/22.60 % (4032431)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=2903824368:st=2:i=13800:sd=12:ep=R:rtra=on:ss=axioms_2873 on theBenchmark for (2873ds/13800Mi) % 155.39/22.60 % (4032427)Instruction limit reached! % 155.39/22.60 % (4032427)------------------------------ % 155.39/22.60 % (4032427)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 155.39/22.60 % (4032427)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.39/22.60 % (4032427)CaDiCaL version: 2.1.3 % 155.39/22.60 % (4032427)Termination reason: Instruction limit % 155.39/22.60 % (4032427)Termination phase: Saturation % 155.39/22.60 % (4032427)Time elapsed: 1.397 s % 155.39/22.60 % (4032427)Peak memory usage: 102 MB % 155.39/22.60 % (4032427)Instructions burned: 5147 (million) % 155.39/22.60 % (4032739)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=830532585:i=1412:rtra=on:fsd=on:proc=on_2862 on theBenchmark for (2862ds/1412Mi) % 155.39/22.60 % (4032429)Instruction limit reached! % 155.39/22.60 % (4032429)------------------------------ % 155.39/22.60 % (4032429)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 155.39/22.60 % (4032429)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.39/22.60 % (4032429)CaDiCaL version: 2.1.3 % 155.39/22.60 % (4032429)Termination reason: Instruction limit % 155.39/22.60 % (4032429)Termination phase: Saturation % 155.39/22.60 % (4032429)Time elapsed: 1.387 s % 155.39/22.60 % (4032429)Peak memory usage: 93 MB % 155.39/22.60 % (4032429)Instructions burned: 3511 (million) % 155.39/22.60 % (4032784)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 % 242.12/34.75 % (4032784)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=1639630793:i=11747:aac=none:nm=0:rtra=on:rawr=on_2860 on theBenchmark for (2860ds/11747Mi) % 242.12/34.75 % (4032739)Instruction limit reached! % 242.12/34.75 % (4032739)------------------------------ % 242.12/34.75 % (4032739)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 242.12/34.75 % (4032739)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 242.12/34.75 % (4032739)CaDiCaL version: 2.1.3 % 242.12/34.75 % (4032739)Termination reason: Instruction limit % 242.12/34.75 % (4032739)Termination phase: Saturation % 242.12/34.75 % (4032739)Time elapsed: 0.433 s % 242.12/34.75 % (4032739)Peak memory usage: 124 MB % 242.12/34.75 % (4032739)Instructions burned: 1413 (million) % 242.12/34.75 % (4032786)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=669092523:s2a=on:i=3553:nm=0:rtra=on_2857 on theBenchmark for (2857ds/3553Mi) % 242.12/34.75 % (4032415)Instruction limit reached! % 242.12/34.75 % (4032415)------------------------------ % 242.12/34.75 % (4032415)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 242.12/34.75 % (4032415)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 242.12/34.75 % (4032415)CaDiCaL version: 2.1.3 % 242.12/34.75 % (4032415)Termination reason: Instruction limit % 242.12/34.75 % (4032415)Termination phase: Saturation % 242.12/34.75 % (4032415)Time elapsed: 6.804 s % 242.12/34.75 % (4032415)Peak memory usage: 150 MB % 242.12/34.75 % (4032415)Instructions burned: 13095 (million) % 242.12/34.75 % (4032788)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=3898814817:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2850 on theBenchmark for (2850ds/3201Mi) % 242.12/34.75 % (4032786)Instruction limit reached! % 242.12/34.75 % (4032786)------------------------------ % 242.12/34.75 % (4032786)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 242.12/34.75 % (4032786)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 242.12/34.75 % (4032786)CaDiCaL version: 2.1.3 % 242.12/34.75 % (4032786)Termination reason: Instruction limit % 242.12/34.75 % (4032786)Termination phase: Saturation % 242.12/34.75 % (4032786)Time elapsed: 0.838 s % 242.12/34.75 % (4032786)Peak memory usage: 106 MB % 242.12/34.75 % (4032786)Instructions burned: 3556 (million) % 242.12/34.75 % (4032790)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=1552094603:thitd=on:cond=on:i=4081:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2847 on theBenchmark for (2847ds/4081Mi) % 242.12/34.75 % (4032403)Instruction limit reached! % 242.12/34.75 % (4032403)------------------------------ % 242.12/34.75 % (4032403)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 242.12/34.75 % (4032403)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 242.12/34.75 % (4032403)CaDiCaL version: 2.1.3 % 242.12/34.75 % (4032403)Termination reason: Instruction limit % 242.12/34.75 % (4032403)Termination phase: Saturation % 242.12/34.75 % (4032403)Time elapsed: 9.409 s % 242.12/34.75 % (4032403)Peak memory usage: 154 MB % 242.12/34.75 % (4032403)Instructions burned: 21175 (million) % 242.12/34.75 % (4032792)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=2998001988:cond=fast:i=20260:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2839 on theBenchmark for (2839ds/20260Mi) % 242.12/34.75 % (4032790)Instruction limit reached! % 242.12/34.75 % (4032790)------------------------------ % 242.12/34.75 % (4032790)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 242.12/34.75 % (4032790)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 242.12/34.75 % (4032790)CaDiCaL version: 2.1.3 % 242.12/34.75 % (4032790)Termination reason: Instruction limit % 242.12/34.75 % (4032790)Termination phase: Saturation % 242.12/34.75 % (4032790)Time elapsed: 1.126 s % 242.12/34.75 % (4032790)Peak memory usage: 144 MB % 242.12/34.75 % (4032790)Instructions burned: 4084 (million) % 242.12/34.75 % (4032794)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=1537417886:s2a=on:i=58627:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2835 on theBenchmark for (2835ds/58627Mi) % 242.12/34.75 % (4032788)Instruction limit reached! % 242.12/34.75 % (4032788)------------------------------ % 242.12/34.75 % (4032788)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 242.12/34.75 % (4032788)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.12/41.38 % (4032788)CaDiCaL version: 2.1.3 % 289.12/41.38 % (4032788)Termination reason: Instruction limit % 289.12/41.38 % (4032788)Termination phase: Saturation % 289.12/41.38 % (4032788)Time elapsed: 1.531 s % 289.12/41.38 % (4032788)Peak memory usage: 94 MB % 289.12/41.38 % (4032788)Instructions burned: 3202 (million) % 289.12/41.38 % (4032796)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=967444694:avsq=on:i=6258:avsqr=1,16:rtra=on:rawr=on_2834 on theBenchmark for (2834ds/6258Mi) % 289.12/41.38 % (4032413)Instruction limit reached! % 289.12/41.38 % (4032413)------------------------------ % 289.12/41.38 % (4032413)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 289.12/41.38 % (4032413)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.12/41.38 % (4032413)CaDiCaL version: 2.1.3 % 289.12/41.38 % (4032413)Termination reason: Instruction limit % 289.12/41.38 % (4032413)Termination phase: Saturation % 289.12/41.38 % (4032413)Time elapsed: 8.844 s % 289.12/41.38 % (4032413)Peak memory usage: 157 MB % 289.12/41.38 % (4032413)Instructions burned: 17166 (million) % 289.12/41.38 % (4032798)ott+10_128_isp=bottom:to=lpo:sil=128000:si=on:urr=on:uwa=alasca_main:sac=on:slsq=on:random_seed=3521796150:i=34001:aac=none:doe=on:rtra=on:gtg=exists_all_2831 on theBenchmark for (2831ds/34001Mi) % 289.12/41.38 % (4032431)Instruction limit reached! % 289.12/41.38 % (4032431)------------------------------ % 289.12/41.38 % (4032431)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 289.12/41.38 % (4032431)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.12/41.38 % (4032431)CaDiCaL version: 2.1.3 % 289.12/41.38 % (4032431)Termination reason: Instruction limit % 289.12/41.38 % (4032431)Termination phase: Saturation % 289.12/41.38 % (4032431)Time elapsed: 6.441 s % 289.12/41.38 % (4032431)Peak memory usage: 103 MB % 289.12/41.38 % (4032431)Instructions burned: 13800 (million) % 289.12/41.38 % (4032800)lrs+2_10_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_main:tha=some:random_seed=1809187746:s2a=on:i=71622:s2at=-1:rtra=on_2807 on theBenchmark for (2807ds/71622Mi) % 289.12/41.38 % (4032796)Instruction limit reached! % 289.12/41.38 % (4032796)------------------------------ % 289.12/41.38 % (4032796)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 289.12/41.38 % (4032796)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.12/41.38 % (4032796)CaDiCaL version: 2.1.3 % 289.12/41.38 % (4032796)Termination reason: Instruction limit % 289.12/41.38 % (4032796)Termination phase: Saturation % 289.12/41.38 % (4032796)Time elapsed: 2.856 s % 289.12/41.38 % (4032796)Peak memory usage: 123 MB % 289.12/41.38 % (4032796)Instructions burned: 6260 (million) % 289.12/41.38 % (4032802)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=2920019516:i=24001:kws=precedence:nm=0:rtra=on_2804 on theBenchmark for (2804ds/24001Mi) % 289.12/41.38 % (4032784)Instruction limit reached! % 289.12/41.38 % (4032784)------------------------------ % 289.12/41.38 % (4032784)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 289.12/41.38 % (4032784)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.12/41.38 % (4032784)CaDiCaL version: 2.1.3 % 289.12/41.38 % (4032784)Termination reason: Instruction limit % 289.12/41.38 % (4032784)Termination phase: Saturation % 289.12/41.38 % (4032784)Time elapsed: 6.599 s % 289.12/41.38 % (4032784)Peak memory usage: 177 MB % 289.12/41.38 % (4032784)Instructions burned: 11747 (million) % 289.12/41.38 % (4032804)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=3341505169:i=2076:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2793 on theBenchmark for (2793ds/2076Mi) % 289.12/41.38 % (4032804)Instruction limit reached! % 289.12/41.38 % (4032804)------------------------------ % 289.12/41.38 % (4032804)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 289.12/41.38 % (4032804)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.12/41.38 % (4032804)CaDiCaL version: 2.1.3 % 289.12/41.38 % (4032804)Termination reason: Instruction limit % 289.12/41.38 % (4032804)Termination phase: Saturation % 289.12/41.38 % (4032804)Time elapsed: 0.988 s % 289.12/41.38 % (4032804)Peak memory usage: 121 MB % 289.12/41.38 % (4032804)Instructions burned: 2078 (million) % 289.12/41.38 % (4032806)dis+21_20_to=lakbo:si=on:alasca=on:sp=const_max:uwa=alasca_main:sac=on:random_seed=2246852664:s2a=on:i=83971:s2at=4:bd=all:ins=1:rtra=on_27Terminated %------------------------------------------------------------------------------