%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWC481_1 : TPTP v9.3.1. Released v9.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % Computer : n014.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:04:01 PM UTC 2026 % Result : Timeout 300.50s 42.84s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWC481_1 : TPTP v9.3.1. Released v9.0.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.07/0.20 % Computer : n014.cluster.edu % 0.07/0.20 % Model : x86_64 x86_64 % 0.07/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.07/0.20 % Memory : 8046.5625MB % 0.07/0.20 % OS : Linux 6.8.0-71-generic % 0.07/0.20 % CPULimit : 300 % 0.07/0.20 % WCLimit : 300 % 0.07/0.20 % DateTime : Mon Sep 28 09:40:01 UTC 2026 % 0.07/0.20 % CPUTime : % 0.07/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.07/0.23 Running first-order theorem proving % 0.07/0.23 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 % 4.54/1.28 % (1665316)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule. % 4.54/1.28 % (1665393)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=908360058:i=33:rtra=on_3000 on theBenchmark for (3000ds/33Mi) % 4.54/1.28 % (1665393)Instruction limit reached! % 4.54/1.28 % (1665393)------------------------------ % 4.54/1.28 % (1665393)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.54/1.28 % (1665393)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.54/1.28 % (1665393)CaDiCaL version: 2.1.3 % 4.54/1.28 % (1665393)Termination reason: Instruction limit % 4.54/1.28 % (1665393)Termination phase: Saturation % 4.54/1.28 % (1665393)Time elapsed: 0.038 s % 4.54/1.28 % (1665393)Peak memory usage: 117 MB % 4.54/1.28 % (1665393)Instructions burned: 34 (million) % 4.54/1.28 % (1665389)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=3874651081:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_3000 on theBenchmark for (3000ds/201Mi) % 4.54/1.28 % (1665388)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=1811708592:i=307:kws=precedence:nm=0:rtra=on_3000 on theBenchmark for (3000ds/307Mi) % 4.54/1.28 % (1665392)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=1733796960:i=46:rtra=on_3000 on theBenchmark for (3000ds/46Mi) % 4.54/1.28 % (1665390)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=899720300:s2a=on:i=7:rtra=on:inst=on_3000 on theBenchmark for (3000ds/7Mi) % 4.54/1.28 % (1665391)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=3981599247:i=4:rtra=on_3000 on theBenchmark for (3000ds/4Mi) % 4.54/1.28 % (1665387)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=3103426861:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_3000 on theBenchmark for (3000ds/12Mi) % 4.54/1.28 % (1665391)Instruction limit reached! % 4.54/1.28 % (1665391)------------------------------ % 4.54/1.28 % (1665391)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.54/1.28 % (1665391)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.54/1.28 % (1665391)CaDiCaL version: 2.1.3 % 4.54/1.28 % (1665391)Termination reason: Instruction limit % 4.54/1.28 % (1665391)Termination phase: Saturation % 4.54/1.28 % (1665391)Time elapsed: 0.006 s % 4.54/1.28 % (1665391)Peak memory usage: 89 MB % 4.54/1.28 % (1665391)Instructions burned: 4 (million) % 4.54/1.28 % (1665390)Instruction limit reached! % 4.54/1.28 % (1665390)------------------------------ % 4.54/1.28 % (1665390)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.54/1.28 % (1665390)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.54/1.28 % (1665390)CaDiCaL version: 2.1.3 % 4.54/1.28 % (1665390)Termination reason: Instruction limit % 4.54/1.28 % (1665390)Termination phase: Saturation % 4.54/1.28 % (1665390)Time elapsed: 0.008 s % 4.54/1.28 % (1665390)Peak memory usage: 88 MB % 4.54/1.28 % (1665390)Instructions burned: 7 (million) % 4.54/1.28 % (1665387)Instruction limit reached! % 4.54/1.28 % (1665387)------------------------------ % 4.54/1.28 % (1665387)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.54/1.28 % (1665387)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.54/1.28 % (1665387)CaDiCaL version: 2.1.3 % 4.54/1.28 % (1665387)Termination reason: Instruction limit % 4.54/1.28 % (1665387)Termination phase: Saturation % 4.54/1.28 % (1665387)Time elapsed: 0.043 s % 4.54/1.28 % (1665387)Peak memory usage: 116 MB % 4.54/1.28 % (1665387)Instructions burned: 12 (million) % 4.54/1.28 % (1665392)Instruction limit reached! % 4.54/1.28 % (1665392)------------------------------ % 4.54/1.28 % (1665392)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.54/1.28 % (1665392)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.54/1.28 % (1665392)CaDiCaL version: 2.1.3 % 4.54/1.28 % (1665392)Termination reason: Instruction limit % 4.54/1.28 % (1665392)Termination phase: Saturation % 4.54/1.28 % (1665392)Time elapsed: 0.073 s % 4.54/1.28 % (1665392)Peak memory usage: 116 MB % 4.54/1.28 % (1665392)Instructions burned: 47 (million) % 4.54/1.28 % (1665404)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=1934504014:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2998 on theBenchmark for (2998ds/14Mi) % 4.54/1.28 % (1665404)Instruction limit reached! % 4.54/1.28 % (1665404)------------------------------ % 6.25/1.53 % (1665404)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.25/1.53 % (1665404)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.25/1.53 % (1665404)CaDiCaL version: 2.1.3 % 6.25/1.53 % (1665404)Termination reason: Instruction limit % 6.25/1.53 % (1665404)Termination phase: Saturation % 6.25/1.53 % (1665404)Time elapsed: 0.008 s % 6.25/1.53 % (1665404)Peak memory usage: 88 MB % 6.25/1.53 % (1665404)Instructions burned: 15 (million) % 6.25/1.53 % (1665389)Instruction limit reached! % 6.25/1.53 % (1665389)------------------------------ % 6.25/1.53 % (1665389)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.25/1.53 % (1665389)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.25/1.53 % (1665389)CaDiCaL version: 2.1.3 % 6.25/1.53 % (1665389)Termination reason: Instruction limit % 6.25/1.53 % (1665389)Termination phase: Saturation % 6.25/1.53 % (1665389)Time elapsed: 0.257 s % 6.25/1.53 % (1665389)Peak memory usage: 118 MB % 6.25/1.53 % (1665389)Instructions burned: 201 (million) % 6.25/1.53 % (1665422)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=537532027:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2997 on theBenchmark for (2997ds/16Mi) % 6.25/1.53 % (1665421)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=1863943446:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2997 on theBenchmark for (2997ds/29Mi) % 6.25/1.53 % (1665422)Instruction limit reached! % 6.25/1.53 % (1665422)------------------------------ % 6.25/1.53 % (1665422)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.25/1.53 % (1665422)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.25/1.53 % (1665422)CaDiCaL version: 2.1.3 % 6.25/1.53 % (1665422)Termination reason: Instruction limit % 6.25/1.53 % (1665422)Termination phase: Saturation % 6.25/1.53 % (1665422)Time elapsed: 0.018 s % 6.25/1.53 % (1665422)Peak memory usage: 90 MB % 6.25/1.53 % (1665422)Instructions burned: 16 (million) % 6.25/1.53 % (1665425)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=273027423:i=24:canc=force:rtra=on_2996 on theBenchmark for (2996ds/24Mi) % 6.25/1.53 % (1665426)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=3556585530:i=27:canc=cautious:fsr=off:rtra=on_2996 on theBenchmark for (2996ds/27Mi) % 6.25/1.53 % (1665431)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=3643437877:i=85:gtgl=4:rtra=on:gtg=exists_sym_2995 on theBenchmark for (2995ds/85Mi) % 6.25/1.53 % (1665421)Instruction limit reached! % 6.25/1.53 % (1665421)------------------------------ % 6.25/1.53 % (1665421)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.25/1.53 % (1665421)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.25/1.53 % (1665421)CaDiCaL version: 2.1.3 % 6.25/1.53 % (1665421)Termination reason: Instruction limit % 6.25/1.53 % (1665421)Termination phase: Saturation % 6.25/1.53 % (1665421)Time elapsed: 0.032 s % 6.25/1.53 % (1665421)Peak memory usage: 88 MB % 6.25/1.53 % (1665421)Instructions burned: 30 (million) % 6.25/1.53 % (1665388)Instruction limit reached! % 6.25/1.53 % (1665388)------------------------------ % 6.25/1.53 % (1665388)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.25/1.53 % (1665388)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.25/1.53 % (1665388)CaDiCaL version: 2.1.3 % 6.25/1.53 % (1665388)Termination reason: Instruction limit % 6.25/1.53 % (1665388)Termination phase: Saturation % 6.25/1.53 % (1665388)Time elapsed: 0.298 s % 6.25/1.53 % (1665388)Peak memory usage: 116 MB % 6.25/1.53 % (1665388)Instructions burned: 308 (million) % 6.25/1.53 % (1665426)Instruction limit reached! % 6.25/1.53 % (1665426)------------------------------ % 6.25/1.53 % (1665426)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.25/1.53 % (1665426)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.25/1.53 % (1665426)CaDiCaL version: 2.1.3 % 6.25/1.53 % (1665426)Termination reason: Instruction limit % 6.25/1.53 % (1665426)Termination phase: Saturation % 6.25/1.53 % (1665426)Time elapsed: 0.028 s % 6.25/1.53 % (1665426)Peak memory usage: 89 MB % 6.25/1.53 % (1665426)Instructions burned: 28 (million) % 6.25/1.53 % (1665425)Instruction limit reached! % 6.25/1.53 % (1665425)------------------------------ % 6.25/1.53 % (1665425)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.44/1.90 % (1665425)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.44/1.90 % (1665425)CaDiCaL version: 2.1.3 % 8.44/1.90 % (1665425)Termination reason: Instruction limit % 8.44/1.90 % (1665425)Termination phase: Saturation % 8.44/1.90 % (1665425)Time elapsed: 0.029 s % 8.44/1.90 % (1665425)Peak memory usage: 89 MB % 8.44/1.90 % (1665425)Instructions burned: 24 (million) % 8.44/1.90 % (1665431)Instruction limit reached! % 8.44/1.90 % (1665431)------------------------------ % 8.44/1.90 % (1665431)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.44/1.90 % (1665431)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.44/1.90 % (1665431)CaDiCaL version: 2.1.3 % 8.44/1.90 % (1665431)Termination reason: Instruction limit % 8.44/1.90 % (1665431)Termination phase: Saturation % 8.44/1.90 % (1665431)Time elapsed: 0.041 s % 8.44/1.90 % (1665431)Peak memory usage: 89 MB % 8.44/1.90 % (1665431)Instructions burned: 86 (million) % 8.44/1.90 % (1665437)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=3647896637:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2995 on theBenchmark for (2995ds/2Mi) % 8.44/1.90 % (1665437)Instruction limit reached! % 8.44/1.90 % (1665437)------------------------------ % 8.44/1.90 % (1665437)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.44/1.90 % (1665437)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.44/1.90 % (1665437)CaDiCaL version: 2.1.3 % 8.44/1.90 % (1665437)Termination reason: Instruction limit % 8.44/1.90 % (1665437)Termination phase: Saturation % 8.44/1.90 % (1665437)Time elapsed: 0.004 s % 8.44/1.90 % (1665437)Peak memory usage: 88 MB % 8.44/1.90 % (1665437)Instructions burned: 2 (million) % 8.44/1.90 % (1665448)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=1459386082:st=3:i=2:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/2Mi) % 8.44/1.90 % (1665448)Instruction limit reached! % 8.44/1.90 % (1665448)------------------------------ % 8.44/1.90 % (1665448)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.44/1.90 % (1665448)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.44/1.90 % (1665448)CaDiCaL version: 2.1.3 % 8.44/1.90 % (1665448)Termination reason: Instruction limit % 8.44/1.90 % (1665448)Termination phase: Saturation % 8.44/1.90 % (1665448)Time elapsed: 0.003 s % 8.44/1.90 % (1665448)Peak memory usage: 89 MB % 8.44/1.90 % (1665448)Instructions burned: 3 (million) % 8.44/1.90 % (1665444)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=447951337:i=4:ep=RST:ins=2:rtra=on_2994 on theBenchmark for (2994ds/4Mi) % 8.44/1.90 % (1665440)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=3474631992:i=181:rtra=on:ss=axioms:ev=cautious_2994 on theBenchmark for (2994ds/181Mi) % 8.44/1.90 % (1665440)Refutation not found, incomplete strategy % 8.44/1.90 % (1665440)------------------------------ % 8.44/1.90 % (1665440)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.44/1.90 % (1665440)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.44/1.90 % (1665440)CaDiCaL version: 2.1.3 % 8.44/1.90 % (1665440)Termination reason: Refutation not found, incomplete strategy % 8.44/1.90 % (1665440)Time elapsed: 0.003 s % 8.44/1.90 % (1665440)Peak memory usage: 89 MB % 8.44/1.90 % (1665440)Instructions burned: 1 (million) % 8.44/1.90 % (1665444)Instruction limit reached! % 8.44/1.90 % (1665444)------------------------------ % 8.44/1.90 % (1665444)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.44/1.90 % (1665444)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.44/1.90 % (1665444)CaDiCaL version: 2.1.3 % 8.44/1.90 % (1665444)Termination reason: Instruction limit % 8.44/1.90 % (1665444)Termination phase: Saturation % 8.44/1.90 % (1665444)Time elapsed: 0.006 s % 8.44/1.90 % (1665444)Peak memory usage: 88 MB % 8.44/1.90 % (1665444)Instructions burned: 4 (million) % 8.44/1.90 % (1665445)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=1950508471:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2994 on theBenchmark for (2994ds/66Mi) % 8.44/1.90 % (1665446)lrs+10_1_thi=all:si=on:fd=off:random_seed=3939692284:i=53:rtra=on:gtg=all_2994 on theBenchmark for (2994ds/53Mi) % 8.44/1.90 % (1665447)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=43770124:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2994 on theBenchmark for (2994ds/8Mi) % 12.05/2.29 % (1665447)Instruction limit reached! % 12.05/2.29 % (1665447)------------------------------ % 12.05/2.29 % (1665447)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.05/2.29 % (1665447)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.05/2.29 % (1665447)CaDiCaL version: 2.1.3 % 12.05/2.29 % (1665447)Termination reason: Instruction limit % 12.05/2.29 % (1665447)Termination phase: Saturation % 12.05/2.29 % (1665447)Time elapsed: 0.011 s % 12.05/2.29 % (1665447)Peak memory usage: 89 MB % 12.05/2.29 % (1665447)Instructions burned: 9 (million) % 12.05/2.29 % (1665446)Instruction limit reached! % 12.05/2.29 % (1665446)------------------------------ % 12.05/2.29 % (1665446)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.05/2.29 % (1665446)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.05/2.29 % (1665446)CaDiCaL version: 2.1.3 % 12.05/2.29 % (1665446)Termination reason: Instruction limit % 12.05/2.29 % (1665446)Termination phase: Saturation % 12.05/2.29 % (1665446)Time elapsed: 0.091 s % 12.05/2.29 % (1665446)Peak memory usage: 115 MB % 12.05/2.29 % (1665446)Instructions burned: 53 (million) % 12.05/2.29 % (1665445)Instruction limit reached! % 12.05/2.29 % (1665445)------------------------------ % 12.05/2.29 % (1665445)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.05/2.29 % (1665445)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.05/2.29 % (1665445)CaDiCaL version: 2.1.3 % 12.05/2.29 % (1665445)Termination reason: Instruction limit % 12.05/2.29 % (1665445)Termination phase: Saturation % 12.05/2.29 % (1665445)Time elapsed: 0.138 s % 12.05/2.29 % (1665445)Peak memory usage: 134 MB % 12.05/2.29 % (1665445)Instructions burned: 67 (million) % 12.05/2.29 % (1665456)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=2630219458:i=127:doe=on:rtra=on_2992 on theBenchmark for (2992ds/127Mi) % 12.05/2.29 % (1665451)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=3588315116:i=2:doe=on:canc=force:asg=cautious:rtra=on_2992 on theBenchmark for (2992ds/2Mi) % 12.05/2.29 % (1665451)Instruction limit reached! % 12.05/2.29 % (1665451)------------------------------ % 12.05/2.29 % (1665451)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.05/2.29 % (1665451)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.05/2.29 % (1665451)CaDiCaL version: 2.1.3 % 12.05/2.29 % (1665451)Termination reason: Instruction limit % 12.05/2.29 % (1665451)Termination phase: Saturation % 12.05/2.29 % (1665451)Time elapsed: 0.004 s % 12.05/2.29 % (1665451)Peak memory usage: 89 MB % 12.05/2.29 % (1665451)Instructions burned: 2 (million) % 12.05/2.29 % (1665457)dis+10_1_si=on:random_seed=3025838121:i=10:ep=R:rtra=on_2992 on theBenchmark for (2992ds/10Mi) % 12.05/2.29 % (1665457)Instruction limit reached! % 12.05/2.29 % (1665457)------------------------------ % 12.05/2.29 % (1665457)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.05/2.29 % (1665457)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.05/2.29 % (1665457)CaDiCaL version: 2.1.3 % 12.05/2.29 % (1665457)Termination reason: Instruction limit % 12.05/2.29 % (1665457)Termination phase: Saturation % 12.05/2.29 % (1665457)Time elapsed: 0.013 s % 12.05/2.29 % (1665457)Peak memory usage: 88 MB % 12.05/2.29 % (1665457)Instructions burned: 10 (million) % 12.05/2.29 % (1665456)Instruction limit reached! % 12.05/2.29 % (1665456)------------------------------ % 12.05/2.29 % (1665456)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.05/2.29 % (1665456)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.05/2.29 % (1665456)CaDiCaL version: 2.1.3 % 12.05/2.29 % (1665456)Termination reason: Instruction limit % 12.05/2.29 % (1665456)Termination phase: Saturation % 12.05/2.29 % (1665456)Time elapsed: 0.097 s % 12.05/2.29 % (1665456)Peak memory usage: 117 MB % 12.05/2.29 % (1665456)Instructions burned: 129 (million) % 12.05/2.29 % (1665461)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=1746165616:i=26:canc=cautious:av=off:rtra=on_2991 on theBenchmark for (2991ds/26Mi) % 12.05/2.29 % (1665461)Refutation not found, incomplete strategy % 12.05/2.29 % (1665461)------------------------------ % 12.05/2.29 % (1665461)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.05/2.29 % (1665461)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.75/2.72 % (1665461)CaDiCaL version: 2.1.3 % 13.75/2.72 % (1665461)Termination reason: Refutation not found, incomplete strategy % 13.75/2.72 % (1665461)Time elapsed: 0.004 s % 13.75/2.72 % (1665461)Peak memory usage: 89 MB % 13.75/2.72 % (1665461)Instructions burned: 2 (million) % 13.75/2.72 % (1665440)------------------------------ % 13.75/2.72 % (1665440)------------------------------ % 13.75/2.72 % (1665462)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=4101014124: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_2990 on theBenchmark for (2990ds/35Mi) % 13.75/2.72 % (1665464)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=24906960:i=2:fsr=off:rtra=on:inst=on_2990 on theBenchmark for (2990ds/2Mi) % 13.75/2.72 % (1665462)Instruction limit reached! % 13.75/2.72 % (1665462)------------------------------ % 13.75/2.72 % (1665462)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.75/2.72 % (1665462)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.75/2.72 % (1665462)CaDiCaL version: 2.1.3 % 13.75/2.72 % (1665462)Termination reason: Instruction limit % 13.75/2.72 % (1665462)Termination phase: Saturation % 13.75/2.72 % (1665462)Time elapsed: 0.039 s % 13.75/2.72 % (1665462)Peak memory usage: 89 MB % 13.75/2.72 % (1665462)Instructions burned: 35 (million) % 13.75/2.72 % (1665464)Instruction limit reached! % 13.75/2.72 % (1665464)------------------------------ % 13.75/2.72 % (1665464)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.75/2.72 % (1665464)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.75/2.72 % (1665464)CaDiCaL version: 2.1.3 % 13.75/2.72 % (1665464)Termination reason: Instruction limit % 13.75/2.72 % (1665464)Termination phase: Saturation % 13.75/2.72 % (1665464)Time elapsed: 0.004 s % 13.75/2.72 % (1665464)Peak memory usage: 88 MB % 13.75/2.72 % (1665464)Instructions burned: 2 (million) % 13.75/2.72 % (1665469)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=1333667988:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2989 on theBenchmark for (2989ds/8Mi) % 13.75/2.72 % (1665469)Instruction limit reached! % 13.75/2.72 % (1665469)------------------------------ % 13.75/2.72 % (1665469)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.75/2.72 % (1665469)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.75/2.72 % (1665469)CaDiCaL version: 2.1.3 % 13.75/2.72 % (1665469)Termination reason: Instruction limit % 13.75/2.72 % (1665469)Termination phase: Saturation % 13.75/2.72 % (1665469)Time elapsed: 0.012 s % 13.75/2.72 % (1665469)Peak memory usage: 89 MB % 13.75/2.72 % (1665469)Instructions burned: 8 (million) % 13.75/2.72 % (1665476)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=2788888405:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2989 on theBenchmark for (2989ds/13Mi) % 13.75/2.72 % (1665476)Instruction limit reached! % 13.75/2.72 % (1665476)------------------------------ % 13.75/2.72 % (1665476)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.75/2.72 % (1665476)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.75/2.72 % (1665476)CaDiCaL version: 2.1.3 % 13.75/2.72 % (1665476)Termination reason: Instruction limit % 13.75/2.72 % (1665476)Termination phase: Saturation % 13.75/2.72 % (1665476)Time elapsed: 0.028 s % 13.75/2.72 % (1665476)Peak memory usage: 116 MB % 13.75/2.72 % (1665476)Instructions burned: 13 (million) % 13.75/2.72 % (1665473)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=3473643078:i=370:ep=RS:fsr=off:rtra=on_2989 on theBenchmark for (2989ds/370Mi) % 13.75/2.72 % (1665479)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=1370027130:i=226:rtra=on:gtg=position:ss=axioms_2988 on theBenchmark for (2988ds/226Mi) % 13.75/2.72 % (1665483)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=2326877195:i=71:rtra=on:gtg=exists_top_2987 on theBenchmark for (2987ds/71Mi) % 13.75/2.72 % (1665482)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=3531392377:i=10:rtra=on_2987 on theBenchmark for (2987ds/10Mi) % 13.75/2.72 % (1665479)Refutation not found, incomplete strategy % 13.75/2.72 % (1665479)------------------------------ % 13.75/2.72 % (1665479)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.75/2.72 % (1665479)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.99/3.16 % (1665479)CaDiCaL version: 2.1.3 % 18.99/3.16 % (1665479)Termination reason: Refutation not found, incomplete strategy % 18.99/3.16 % (1665479)Time elapsed: 0.041 s % 18.99/3.16 % (1665479)Peak memory usage: 116 MB % 18.99/3.16 % (1665479)Instructions burned: 6 (million) % 18.99/3.16 % (1665482)Instruction limit reached! % 18.99/3.16 % (1665482)------------------------------ % 18.99/3.16 % (1665482)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.99/3.16 % (1665482)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.99/3.16 % (1665482)CaDiCaL version: 2.1.3 % 18.99/3.16 % (1665482)Termination reason: Instruction limit % 18.99/3.16 % (1665482)Termination phase: Saturation % 18.99/3.16 % (1665482)Time elapsed: 0.013 s % 18.99/3.16 % (1665482)Peak memory usage: 88 MB % 18.99/3.16 % (1665482)Instructions burned: 11 (million) % 18.99/3.16 % (1665461)------------------------------ % 18.99/3.16 % (1665461)------------------------------ % 18.99/3.16 % (1665487)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=828966462:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2987 on theBenchmark for (2987ds/75Mi) % 18.99/3.16 % (1665483)Instruction limit reached! % 18.99/3.16 % (1665483)------------------------------ % 18.99/3.16 % (1665483)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.99/3.16 % (1665483)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.99/3.16 % (1665483)CaDiCaL version: 2.1.3 % 18.99/3.16 % (1665483)Termination reason: Instruction limit % 18.99/3.16 % (1665483)Termination phase: Saturation % 18.99/3.16 % (1665483)Time elapsed: 0.129 s % 18.99/3.16 % (1665483)Peak memory usage: 134 MB % 18.99/3.16 % (1665483)Instructions burned: 71 (million) % 18.99/3.16 % (1665487)Instruction limit reached! % 18.99/3.16 % (1665487)------------------------------ % 18.99/3.16 % (1665487)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.99/3.16 % (1665487)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.99/3.16 % (1665487)CaDiCaL version: 2.1.3 % 18.99/3.16 % (1665487)Termination reason: Instruction limit % 18.99/3.16 % (1665487)Termination phase: Saturation % 18.99/3.16 % (1665487)Time elapsed: 0.061 s % 18.99/3.16 % (1665487)Peak memory usage: 89 MB % 18.99/3.16 % (1665487)Instructions burned: 75 (million) % 18.99/3.16 % (1665490)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=1529599165:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2987 on theBenchmark for (2987ds/294Mi) % 18.99/3.16 % (1665473)Instruction limit reached! % 18.99/3.16 % (1665473)------------------------------ % 18.99/3.16 % (1665473)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.99/3.16 % (1665473)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.99/3.16 % (1665473)CaDiCaL version: 2.1.3 % 18.99/3.16 % (1665473)Termination reason: Instruction limit % 18.99/3.16 % (1665473)Termination phase: Saturation % 18.99/3.16 % (1665473)Time elapsed: 0.314 s % 18.99/3.16 % (1665473)Peak memory usage: 90 MB % 18.99/3.16 % (1665473)Instructions burned: 370 (million) % 18.99/3.16 % (1665496)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=498577419:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2985 on theBenchmark for (2985ds/130Mi) % 18.99/3.16 % (1665497)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=3720343496:i=131:rtra=on_2985 on theBenchmark for (2985ds/131Mi) % 18.99/3.16 % (1665496)Instruction limit reached! % 18.99/3.16 % (1665496)------------------------------ % 18.99/3.16 % (1665496)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.99/3.16 % (1665496)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.99/3.16 % (1665496)CaDiCaL version: 2.1.3 % 18.99/3.16 % (1665496)Termination reason: Instruction limit % 18.99/3.16 % (1665496)Termination phase: Saturation % 18.99/3.16 % (1665496)Time elapsed: 0.092 s % 18.99/3.16 % (1665496)Peak memory usage: 116 MB % 18.99/3.16 % (1665496)Instructions burned: 131 (million) % 18.99/3.16 % (1665499)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=1091616003:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2984 on theBenchmark for (2984ds/40Mi) % 18.99/3.16 % (1665479)------------------------------ % 18.99/3.16 % (1665479)------------------------------ % 18.99/3.16 % (1665501)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=100269419:i=307:rtra=on:gtg=exists_top_2984 on theBenchmark for (2984ds/307Mi) % 20.38/3.54 % (1665490)Instruction limit reached! % 20.38/3.54 % (1665490)------------------------------ % 20.38/3.54 % (1665490)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.38/3.54 % (1665490)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.38/3.54 % (1665490)CaDiCaL version: 2.1.3 % 20.38/3.54 % (1665490)Termination reason: Instruction limit % 20.38/3.54 % (1665490)Termination phase: Saturation % 20.38/3.54 % (1665490)Time elapsed: 0.276 s % 20.38/3.54 % (1665490)Peak memory usage: 89 MB % 20.38/3.54 % (1665490)Instructions burned: 295 (million) % 20.38/3.54 % (1665502)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=2883623341:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2983 on theBenchmark for (2983ds/598Mi) % 20.38/3.54 % (1665497)Instruction limit reached! % 20.38/3.54 % (1665497)------------------------------ % 20.38/3.54 % (1665497)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.38/3.54 % (1665497)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.38/3.54 % (1665497)CaDiCaL version: 2.1.3 % 20.38/3.54 % (1665497)Termination reason: Instruction limit % 20.38/3.54 % (1665497)Termination phase: Saturation % 20.38/3.54 % (1665497)Time elapsed: 0.196 s % 20.38/3.54 % (1665497)Peak memory usage: 135 MB % 20.38/3.54 % (1665497)Instructions burned: 132 (million) % 20.38/3.54 % (1665499)Instruction limit reached! % 20.38/3.54 % (1665499)------------------------------ % 20.38/3.54 % (1665499)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.38/3.54 % (1665499)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.38/3.54 % (1665499)CaDiCaL version: 2.1.3 % 20.38/3.54 % (1665499)Termination reason: Instruction limit % 20.38/3.54 % (1665499)Termination phase: Saturation % 20.38/3.54 % (1665499)Time elapsed: 0.103 s % 20.38/3.54 % (1665499)Peak memory usage: 134 MB % 20.38/3.54 % (1665499)Instructions burned: 40 (million) % 20.38/3.54 % (1665505)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=1228795128:i=131:canc=cautious:fsr=off:rtra=on_2982 on theBenchmark for (2982ds/131Mi) % 20.38/3.54 % (1665508)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=500042793:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2981 on theBenchmark for (2981ds/259Mi) % 20.38/3.54 % (1665505)Instruction limit reached! % 20.38/3.54 % (1665505)------------------------------ % 20.38/3.54 % (1665505)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.38/3.54 % (1665505)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.38/3.54 % (1665505)CaDiCaL version: 2.1.3 % 20.38/3.54 % (1665505)Termination reason: Instruction limit % 20.38/3.54 % (1665505)Termination phase: Saturation % 20.38/3.54 % (1665505)Time elapsed: 0.089 s % 20.38/3.54 % (1665505)Peak memory usage: 118 MB % 20.38/3.54 % (1665505)Instructions burned: 132 (million) % 20.38/3.54 % (1665501)Instruction limit reached! % 20.38/3.54 % (1665501)------------------------------ % 20.38/3.54 % (1665501)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.38/3.54 % (1665501)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.38/3.54 % (1665501)CaDiCaL version: 2.1.3 % 20.38/3.54 % (1665501)Termination reason: Instruction limit % 20.38/3.54 % (1665501)Termination phase: Saturation % 20.38/3.54 % (1665501)Time elapsed: 0.246 s % 20.38/3.54 % (1665501)Peak memory usage: 91 MB % 20.38/3.54 % (1665501)Instructions burned: 307 (million) % 20.38/3.54 % (1665509)dis+10_1_si=on:random_seed=3392346653:s2a=on:i=1000:rtra=on:gtg=exists_all_2981 on theBenchmark for (2981ds/1000Mi) % 20.38/3.54 % (1665514)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=266926660:i=141:doe=on:rtra=on_2980 on theBenchmark for (2980ds/141Mi) % 20.38/3.54 % (1665513)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=1683216705:i=383:fsr=off:rtra=on:ev=force_2980 on theBenchmark for (2980ds/383Mi) % 20.38/3.54 % (1665517)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=860900446:i=65:nm=16:rtra=on_2979 on theBenchmark for (2979ds/65Mi) % 20.38/3.54 % (1665508)Instruction limit reached! % 20.38/3.54 % (1665508)------------------------------ % 20.38/3.54 % (1665508)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.43/4.13 % (1665508)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.43/4.13 % (1665508)CaDiCaL version: 2.1.3 % 25.43/4.13 % (1665508)Termination reason: Instruction limit % 25.43/4.13 % (1665508)Termination phase: Saturation % 25.43/4.13 % (1665508)Time elapsed: 0.239 s % 25.43/4.13 % (1665508)Peak memory usage: 116 MB % 25.43/4.13 % (1665508)Instructions burned: 259 (million) % 25.43/4.13 % (1665517)Refutation not found, incomplete strategy % 25.43/4.13 % (1665517)------------------------------ % 25.43/4.13 % (1665517)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.43/4.13 % (1665517)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.43/4.13 % (1665517)CaDiCaL version: 2.1.3 % 25.43/4.13 % (1665517)Termination reason: Refutation not found, incomplete strategy % 25.43/4.13 % (1665517)Time elapsed: 0.024 s % 25.43/4.13 % (1665517)Peak memory usage: 115 MB % 25.43/4.13 % (1665517)Instructions burned: 6 (million) % 25.43/4.13 % (1665518)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=1273516474:i=121:nm=16:rtra=on_2979 on theBenchmark for (2979ds/121Mi) % 25.43/4.13 % (1665514)Instruction limit reached! % 25.43/4.13 % (1665514)------------------------------ % 25.43/4.13 % (1665514)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.43/4.13 % (1665514)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.43/4.13 % (1665514)CaDiCaL version: 2.1.3 % 25.43/4.13 % (1665514)Termination reason: Instruction limit % 25.43/4.13 % (1665514)Termination phase: Saturation % 25.43/4.13 % (1665514)Time elapsed: 0.148 s % 25.43/4.13 % (1665514)Peak memory usage: 90 MB % 25.43/4.13 % (1665514)Instructions burned: 141 (million) % 25.43/4.13 % (1665518)Instruction limit reached! % 25.43/4.13 % (1665518)------------------------------ % 25.43/4.13 % (1665518)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.43/4.13 % (1665518)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.43/4.13 % (1665518)CaDiCaL version: 2.1.3 % 25.43/4.13 % (1665518)Termination reason: Instruction limit % 25.43/4.13 % (1665518)Termination phase: Saturation % 25.43/4.13 % (1665518)Time elapsed: 0.109 s % 25.43/4.13 % (1665518)Peak memory usage: 89 MB % 25.43/4.13 % (1665518)Instructions burned: 122 (million) % 25.43/4.13 % (1665502)Instruction limit reached! % 25.43/4.13 % (1665502)------------------------------ % 25.43/4.13 % (1665502)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.43/4.13 % (1665502)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.43/4.13 % (1665502)CaDiCaL version: 2.1.3 % 25.43/4.13 % (1665502)Termination reason: Instruction limit % 25.43/4.13 % (1665502)Termination phase: Saturation % 25.43/4.13 % (1665502)Time elapsed: 0.594 s % 25.43/4.13 % (1665502)Peak memory usage: 138 MB % 25.43/4.13 % (1665502)Instructions burned: 598 (million) % 25.43/4.13 % (1665517)------------------------------ % 25.43/4.13 % (1665517)------------------------------ % 25.43/4.13 % (1665525)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=2481391647:s2a=on:i=128:s2at=5:ins=3:rtra=on_2977 on theBenchmark for (2977ds/128Mi) % 25.43/4.13 % (1665513)Instruction limit reached! % 25.43/4.13 % (1665513)------------------------------ % 25.43/4.13 % (1665513)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.43/4.13 % (1665513)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.43/4.13 % (1665513)CaDiCaL version: 2.1.3 % 25.43/4.13 % (1665513)Termination reason: Instruction limit % 25.43/4.13 % (1665513)Termination phase: Saturation % 25.43/4.13 % (1665513)Time elapsed: 0.341 s % 25.43/4.13 % (1665513)Peak memory usage: 92 MB % 25.43/4.13 % (1665513)Instructions burned: 384 (million) % 25.43/4.13 % (1665527)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=181232906:i=39:ins=3:rtra=on_2976 on theBenchmark for (2976ds/39Mi) % 25.43/4.13 % (1665528)dis+1010_1_to=kbo:si=on:random_seed=948210897:i=175:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2975 on theBenchmark for (2975ds/175Mi) % 25.43/4.13 % (1665525)Instruction limit reached! % 25.43/4.13 % (1665525)------------------------------ % 25.43/4.13 % (1665525)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.43/4.13 % (1665525)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.43/4.13 % (1665525)CaDiCaL version: 2.1.3 % 25.43/4.13 % (1665525)Termination reason: Instruction limit % 25.43/4.13 % (1665525)Termination phase: Saturation % 27.28/4.48 % (1665525)Time elapsed: 0.161 s % 27.28/4.48 % (1665525)Peak memory usage: 118 MB % 27.28/4.48 % (1665525)Instructions burned: 129 (million) % 27.28/4.48 % (1665527)Instruction limit reached! % 27.28/4.48 % (1665527)------------------------------ % 27.28/4.48 % (1665527)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.28/4.48 % (1665527)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.28/4.48 % (1665527)CaDiCaL version: 2.1.3 % 27.28/4.48 % (1665527)Termination reason: Instruction limit % 27.28/4.48 % (1665527)Termination phase: Saturation % 27.28/4.48 % (1665527)Time elapsed: 0.079 s % 27.28/4.48 % (1665527)Peak memory usage: 117 MB % 27.28/4.48 % (1665527)Instructions burned: 39 (million) % 27.28/4.48 % (1665530)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=2180513292:s2a=on:i=483:doe=on:nm=32:rtra=on_2974 on theBenchmark for (2974ds/483Mi) % 27.28/4.48 % (1665529)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=1085120124:i=329:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2974 on theBenchmark for (2974ds/329Mi) % 27.28/4.48 % (1665532)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=2996580975:thitd=on:i=215:nm=0:rtra=on:ev=force_2974 on theBenchmark for (2974ds/215Mi) % 27.28/4.48 % (1665528)Instruction limit reached! % 27.28/4.48 % (1665528)------------------------------ % 27.28/4.48 % (1665528)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.28/4.48 % (1665528)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.28/4.48 % (1665528)CaDiCaL version: 2.1.3 % 27.28/4.48 % (1665528)Termination reason: Instruction limit % 27.28/4.48 % (1665528)Termination phase: Saturation % 27.28/4.48 % (1665528)Time elapsed: 0.207 s % 27.28/4.48 % (1665528)Peak memory usage: 91 MB % 27.28/4.48 % (1665528)Instructions burned: 175 (million) % 27.28/4.48 % (1665535)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=2827214346:i=349:rtra=on_2972 on theBenchmark for (2972ds/349Mi) % 27.28/4.48 % (1665530)Instruction limit reached! % 27.28/4.48 % (1665530)------------------------------ % 27.28/4.48 % (1665530)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.28/4.48 % (1665530)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.28/4.48 % (1665530)CaDiCaL version: 2.1.3 % 27.28/4.48 % (1665530)Termination reason: Instruction limit % 27.28/4.48 % (1665530)Termination phase: Saturation % 27.28/4.48 % (1665530)Time elapsed: 0.266 s % 27.28/4.48 % (1665530)Peak memory usage: 134 MB % 27.28/4.48 % (1665530)Instructions burned: 484 (million) % 27.28/4.48 % (1665537)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=1483411203:st=2:i=295:rtra=on:ss=axioms_2972 on theBenchmark for (2972ds/295Mi) % 27.28/4.48 % (1665535)Refutation not found, incomplete strategy % 27.28/4.48 % (1665535)------------------------------ % 27.28/4.48 % (1665535)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.28/4.48 % (1665535)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.28/4.48 % (1665535)CaDiCaL version: 2.1.3 % 27.28/4.48 % (1665535)Termination reason: Refutation not found, incomplete strategy % 27.28/4.48 % (1665535)Time elapsed: 0.041 s % 27.28/4.48 % (1665535)Peak memory usage: 116 MB % 27.28/4.48 % (1665535)Instructions burned: 7 (million) % 27.28/4.48 % (1665509)Instruction limit reached! % 27.28/4.48 % (1665509)------------------------------ % 27.28/4.48 % (1665509)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.28/4.48 % (1665509)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.28/4.48 % (1665509)CaDiCaL version: 2.1.3 % 27.28/4.48 % (1665509)Termination reason: Instruction limit % 27.28/4.48 % (1665509)Termination phase: Saturation % 27.28/4.48 % (1665509)Time elapsed: 0.911 s % 27.28/4.48 % (1665509)Peak memory usage: 94 MB % 27.28/4.48 % (1665509)Instructions burned: 1000 (million) % 27.28/4.48 % (1665532)Instruction limit reached! % 27.28/4.48 % (1665532)------------------------------ % 27.28/4.48 % (1665532)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.28/4.48 % (1665532)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.28/4.48 % (1665532)CaDiCaL version: 2.1.3 % 27.28/4.48 % (1665532)Termination reason: Instruction limit % 27.28/4.48 % (1665532)Termination phase: Saturation % 27.28/4.48 % (1665532)Time elapsed: 0.277 s % 27.28/4.48 % (1665532)Peak memory usage: 137 MB % 29.29/4.97 % (1665532)Instructions burned: 215 (million) % 29.29/4.97 % (1665544)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=588067149:i=328:kws=inv_frequency:nm=20:rtra=on_2970 on theBenchmark for (2970ds/328Mi) % 29.29/4.97 % (1665529)Instruction limit reached! % 29.29/4.97 % (1665529)------------------------------ % 29.29/4.97 % (1665529)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.29/4.97 % (1665529)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.29/4.97 % (1665529)CaDiCaL version: 2.1.3 % 29.29/4.97 % (1665529)Termination reason: Instruction limit % 29.29/4.97 % (1665529)Termination phase: Saturation % 29.29/4.97 % (1665529)Time elapsed: 0.375 s % 29.29/4.97 % (1665529)Peak memory usage: 120 MB % 29.29/4.97 % (1665529)Instructions burned: 329 (million) % 29.29/4.97 % (1665547)dis+1010_1_to=lpo:sil=128000:sas=z3:si=on:nwc=5:random_seed=1784713541:i=281:gtgl=2:rtra=on:gtg=all_2970 on theBenchmark for (2970ds/281Mi) % 29.29/4.97 % (1665537)Instruction limit reached! % 29.29/4.97 % (1665537)------------------------------ % 29.29/4.97 % (1665537)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.29/4.97 % (1665537)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.29/4.97 % (1665537)CaDiCaL version: 2.1.3 % 29.29/4.97 % (1665537)Termination reason: Instruction limit % 29.29/4.97 % (1665537)Termination phase: Saturation % 29.29/4.97 % (1665537)Time elapsed: 0.279 s % 29.29/4.97 % (1665537)Peak memory usage: 90 MB % 29.29/4.97 % (1665537)Instructions burned: 296 (million) % 29.29/4.97 % (1665548)lrs+1010_1_to=kbo:sil=128000:si=on:sos=on:urr=on:uwa=alasca_main:random_seed=1448680660:i=484:doe=on:nm=0:av=off:rtra=on:ss=axioms_2969 on theBenchmark for (2969ds/484Mi) % 29.29/4.97 % (1665551)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=1066965007:i=416:rtra=on:gtg=position:ss=axioms_2968 on theBenchmark for (2968ds/416Mi) % 29.29/4.97 % (1665550)lrs+21_1_to=kbo:sil=128000:thi=neg_eq:si=on:random_seed=4034192729:i=321:canc=force:rtra=on:tac=axiom:ss=axioms:ev=force_2969 on theBenchmark for (2969ds/321Mi) % 29.29/4.97 % (1665551)Refutation not found, incomplete strategy % 29.29/4.97 % (1665551)------------------------------ % 29.29/4.97 % (1665551)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.29/4.97 % (1665551)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.29/4.97 % (1665551)CaDiCaL version: 2.1.3 % 29.29/4.97 % (1665551)Termination reason: Refutation not found, incomplete strategy % 29.29/4.97 % (1665551)Time elapsed: 0.037 s % 29.29/4.97 % (1665551)Peak memory usage: 116 MB % 29.29/4.97 % (1665551)Instructions burned: 6 (million) % 29.29/4.97 % (1665547)Instruction limit reached! % 29.29/4.97 % (1665547)------------------------------ % 29.29/4.97 % (1665547)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.29/4.97 % (1665547)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.29/4.97 % (1665547)CaDiCaL version: 2.1.3 % 29.29/4.97 % (1665547)Termination reason: Instruction limit % 29.29/4.97 % (1665547)Termination phase: Saturation % 29.29/4.97 % (1665547)Time elapsed: 0.173 s % 29.29/4.97 % (1665547)Peak memory usage: 118 MB % 29.29/4.97 % (1665547)Instructions burned: 281 (million) % 29.29/4.97 % (1665535)------------------------------ % 29.29/4.97 % (1665535)------------------------------ % 29.29/4.97 % (1665544)Instruction limit reached! % 29.29/4.97 % (1665544)------------------------------ % 29.29/4.97 % (1665544)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.29/4.97 % (1665544)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.29/4.97 % (1665544)CaDiCaL version: 2.1.3 % 29.29/4.97 % (1665544)Termination reason: Instruction limit % 29.29/4.97 % (1665544)Termination phase: Saturation % 29.29/4.97 % (1665544)Time elapsed: 0.366 s % 29.29/4.97 % (1665544)Peak memory usage: 119 MB % 29.29/4.97 % (1665544)Instructions burned: 328 (million) % 29.29/4.97 % (1665553)lrs+1010_1_to=kbo:tgt=ground:fde=unused:sas=z3:si=on:sp=unary_frequency:gve=force:spb=goal:tha=off:random_seed=3032658767:i=471:thf=on:kws=precedence:rtra=on_2967 on theBenchmark for (2967ds/471Mi) % 29.29/4.97 % (1665557)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=3701576019:avsq=on:i=276:avsqr=1,2:rtra=on_2966 on theBenchmark for (2966ds/276Mi) % 29.29/4.97 % (1665558)lrs+1010_2_to=kbo:sil=128000:tgt=ground:fde=unused:sas=z3:si=on:uwa=off:tha=off:nwc=1:random_seed=447674167:i=375:kws=inv_arity_squared:rtra=on_2966 on theBenchmark for (2966ds/375Mi) % 34.15/5.44 % (1665550)Instruction limit reached! % 34.15/5.44 % (1665550)------------------------------ % 34.15/5.44 % (1665550)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.15/5.44 % (1665550)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.15/5.44 % (1665550)CaDiCaL version: 2.1.3 % 34.15/5.44 % (1665550)Termination reason: Instruction limit % 34.15/5.44 % (1665550)Termination phase: Saturation % 34.15/5.44 % (1665550)Time elapsed: 0.346 s % 34.15/5.44 % (1665550)Peak memory usage: 115 MB % 34.15/5.44 % (1665550)Instructions burned: 322 (million) % 34.15/5.44 % (1665559)lrs+10_1_to=kbo:sil=128000:tgt=full:sas=z3:si=on:uwa=func_ext:slsqc=1:flr=on:slsq=on:random_seed=3721327679:i=387:bd=preordered:rtra=on:ss=axioms:sgt=8_2965 on theBenchmark for (2965ds/387Mi) % 34.15/5.44 % (1665551)------------------------------ % 34.15/5.44 % (1665551)------------------------------ % 34.15/5.44 % (1665548)Instruction limit reached! % 34.15/5.44 % (1665548)------------------------------ % 34.15/5.44 % (1665548)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.15/5.44 % (1665548)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.15/5.44 % (1665548)CaDiCaL version: 2.1.3 % 34.15/5.44 % (1665548)Termination reason: Instruction limit % 34.15/5.44 % (1665548)Termination phase: Saturation % 34.15/5.44 % (1665548)Time elapsed: 0.469 s % 34.15/5.44 % (1665548)Peak memory usage: 91 MB % 34.15/5.44 % (1665548)Instructions burned: 484 (million) % 34.15/5.44 % (1665557)Instruction limit reached! % 34.15/5.44 % (1665557)------------------------------ % 34.15/5.44 % (1665557)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.15/5.44 % (1665557)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.15/5.44 % (1665557)CaDiCaL version: 2.1.3 % 34.15/5.44 % (1665557)Termination reason: Instruction limit % 34.15/5.44 % (1665557)Termination phase: Saturation % 34.15/5.44 % (1665557)Time elapsed: 0.190 s % 34.15/5.44 % (1665557)Peak memory usage: 135 MB % 34.15/5.44 % (1665557)Instructions burned: 276 (million) % 34.15/5.44 % (1665566)lrs+1010_1_to=kbo:sil=64000:sas=cadical:si=on:sos=on:bce=on:random_seed=2190576493:i=359:rtra=on:gtg=exists_top:ss=axioms_2962 on theBenchmark for (2962ds/359Mi) % 34.15/5.45 % (1665566)Refutation not found, incomplete strategy % 34.15/5.45 % (1665566)------------------------------ % 34.15/5.45 % (1665566)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.15/5.45 % (1665566)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.15/5.45 % (1665566)CaDiCaL version: 2.1.3 % 34.15/5.45 % (1665566)Termination reason: Refutation not found, incomplete strategy % 34.15/5.45 % (1665566)Time elapsed: 0.002 s % 34.15/5.45 % (1665566)Peak memory usage: 89 MB % 34.15/5.45 % (1665566)Instructions burned: 2 (million) % 34.15/5.45 % (1665563)lrs+10_1_to=kbo:sil=128000:fde=none:si=on:norm_ineq=on:urr=on:nwc=0.5:random_seed=3149200732:i=513:kws=frequency:bd=all:rtra=on:gtg=exists_all:ss=axioms:sgt=4_2962 on theBenchmark for (2962ds/513Mi) % 34.15/5.45 % (1665553)Instruction limit reached! % 34.15/5.45 % (1665553)------------------------------ % 34.15/5.45 % (1665553)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.15/5.45 % (1665553)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.15/5.45 % (1665553)CaDiCaL version: 2.1.3 % 34.15/5.45 % (1665553)Termination reason: Instruction limit % 34.15/5.45 % (1665553)Termination phase: Saturation % 34.15/5.45 % (1665553)Time elapsed: 0.424 s % 34.15/5.45 % (1665553)Peak memory usage: 119 MB % 34.15/5.45 % (1665553)Instructions burned: 473 (million) % 34.15/5.45 % (1665558)Instruction limit reached! % 34.15/5.45 % (1665558)------------------------------ % 34.15/5.45 % (1665558)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.15/5.45 % (1665558)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.15/5.45 % (1665558)CaDiCaL version: 2.1.3 % 34.15/5.45 % (1665558)Termination reason: Instruction limit % 34.15/5.45 % (1665558)Termination phase: Saturation % 34.15/5.45 % (1665558)Time elapsed: 0.350 s % 34.15/5.45 % (1665558)Peak memory usage: 116 MB % 34.15/5.45 % (1665558)Instructions burned: 376 (million) % 34.15/5.45 % (1665567)dis+1010_1_to=lpo:sil=128000:thi=all:fde=unused:si=on:sp=reverse_arity:tha=off:random_seed=582254233:i=341:gtgl=2:rtra=on:gtg=exists_sym:ev=force:fsd=on:fsdmm=1_2962 on theBenchmark for (2962ds/341Mi) % 40.69/6.21 % (1665565)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=152341404:i=334:rtra=on_2962 on theBenchmark for (2962ds/334Mi) % 40.69/6.21 % (1665566)------------------------------ % 40.69/6.21 % (1665566)------------------------------ % 40.69/6.21 % (1665559)Instruction limit reached! % 40.69/6.21 % (1665559)------------------------------ % 40.69/6.21 % (1665559)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 40.69/6.21 % (1665559)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.69/6.21 % (1665559)CaDiCaL version: 2.1.3 % 40.69/6.21 % (1665559)Termination reason: Instruction limit % 40.69/6.21 % (1665559)Termination phase: Saturation % 40.69/6.21 % (1665559)Time elapsed: 0.497 s % 40.69/6.21 % (1665559)Peak memory usage: 121 MB % 40.69/6.21 % (1665559)Instructions burned: 388 (million) % 40.69/6.21 % (1665570)lrs-2_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_max:tha=off:random_seed=4277874717:st=1.5:i=261:sd=1:kws=precedence:rtra=on:ss=axioms_2960 on theBenchmark for (2960ds/261Mi) % 40.69/6.21 % (1665575)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=3130133790:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2959 on theBenchmark for (2959ds/273Mi) % 40.69/6.21 % (1665573)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=150915287:s2pl=no:i=235:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2959 on theBenchmark for (2959ds/235Mi) % 40.69/6.21 % (1665570)Refutation not found, incomplete strategy % 40.69/6.21 % (1665570)------------------------------ % 40.69/6.21 % (1665570)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 40.69/6.21 % (1665570)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.69/6.21 % (1665570)CaDiCaL version: 2.1.3 % 40.69/6.21 % (1665570)Termination reason: Refutation not found, incomplete strategy % 40.69/6.21 % (1665570)Time elapsed: 0.041 s % 40.69/6.21 % (1665570)Peak memory usage: 115 MB % 40.69/6.21 % (1665570)Instructions burned: 7 (million) % 40.69/6.21 % (1665567)Instruction limit reached! % 40.69/6.21 % (1665567)------------------------------ % 40.69/6.21 % (1665567)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 40.69/6.21 % (1665567)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.69/6.21 % (1665567)CaDiCaL version: 2.1.3 % 40.69/6.21 % (1665567)Termination reason: Instruction limit % 40.69/6.21 % (1665567)Termination phase: Saturation % 40.69/6.21 % (1665567)Time elapsed: 0.320 s % 40.69/6.21 % (1665567)Peak memory usage: 117 MB % 40.69/6.21 % (1665567)Instructions burned: 342 (million) % 40.69/6.21 % (1665565)Instruction limit reached! % 40.69/6.21 % (1665565)------------------------------ % 40.69/6.21 % (1665565)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 40.69/6.21 % (1665565)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.69/6.21 % (1665565)CaDiCaL version: 2.1.3 % 40.69/6.21 % (1665565)Termination reason: Instruction limit % 40.69/6.21 % (1665565)Termination phase: Saturation % 40.69/6.21 % (1665565)Time elapsed: 0.348 s % 40.69/6.21 % (1665565)Peak memory usage: 135 MB % 40.69/6.21 % (1665565)Instructions burned: 334 (million) % 40.69/6.21 % (1665575)Instruction limit reached! % 40.69/6.21 % (1665575)------------------------------ % 40.69/6.21 % (1665575)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 40.69/6.21 % (1665575)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.69/6.21 % (1665575)CaDiCaL version: 2.1.3 % 40.69/6.21 % (1665575)Termination reason: Instruction limit % 40.69/6.21 % (1665575)Termination phase: Saturation % 40.69/6.21 % (1665575)Time elapsed: 0.155 s % 40.69/6.21 % (1665575)Peak memory usage: 92 MB % 40.69/6.21 % (1665575)Instructions burned: 275 (million) % 40.69/6.21 % (1665563)Instruction limit reached! % 40.69/6.21 % (1665563)------------------------------ % 40.69/6.21 % (1665563)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 40.69/6.21 % (1665563)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.69/6.21 % (1665563)CaDiCaL version: 2.1.3 % 40.69/6.21 % (1665563)Termination reason: Instruction limit % 40.69/6.21 % (1665563)Termination phase: Saturation % 40.69/6.21 % (1665563)Time elapsed: 0.547 s % 40.69/6.21 % (1665563)Peak memory usage: 93 MB % 40.69/6.21 % (1665563)Instructions burned: 514 (million) % 40.69/6.21 % (1665579)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=4076298278:i=146:doe=on:rtra=on_2957 on theBenchmark for (2957ds/146Mi) % 42.62/6.93 % (1665573)Instruction limit reached! % 42.62/6.93 % (1665573)------------------------------ % 42.62/6.93 % (1665573)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 42.62/6.93 % (1665573)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.62/6.93 % (1665573)CaDiCaL version: 2.1.3 % 42.62/6.93 % (1665573)Termination reason: Instruction limit % 42.62/6.93 % (1665573)Termination phase: Saturation % 42.62/6.93 % (1665573)Time elapsed: 0.247 s % 42.62/6.93 % (1665573)Peak memory usage: 116 MB % 42.62/6.93 % (1665573)Instructions burned: 235 (million) % 42.62/6.93 % (1665584)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=1869004827:avsq=on:i=276:avsqr=1,2:rtra=on_2956 on theBenchmark for (2956ds/276Mi) % 42.62/6.93 % (1665583)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=68812826:i=4428:doe=on:fsr=off:rtra=on_2956 on theBenchmark for (2956ds/4428Mi) % 42.62/6.93 % (1665585)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=103584385:i=1052:rtra=on_2955 on theBenchmark for (2955ds/1052Mi) % 42.62/6.93 % (1665579)Instruction limit reached! % 42.62/6.93 % (1665579)------------------------------ % 42.62/6.93 % (1665579)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 42.62/6.93 % (1665579)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.62/6.93 % (1665579)CaDiCaL version: 2.1.3 % 42.62/6.93 % (1665579)Termination reason: Instruction limit % 42.62/6.93 % (1665579)Termination phase: Saturation % 42.62/6.93 % (1665579)Time elapsed: 0.155 s % 42.62/6.93 % (1665579)Peak memory usage: 90 MB % 42.62/6.93 % (1665579)Instructions burned: 146 (million) % 42.62/6.93 % (1665570)------------------------------ % 42.62/6.93 % (1665570)------------------------------ % 42.62/6.93 % (1665586)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=644170430:i=655:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2955 on theBenchmark for (2955ds/655Mi) % 42.62/6.93 % (1665586)Refutation not found, incomplete strategy % 42.62/6.93 % (1665586)------------------------------ % 42.62/6.93 % (1665586)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 42.62/6.93 % (1665586)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.62/6.93 % (1665586)CaDiCaL version: 2.1.3 % 42.62/6.93 % (1665586)Termination reason: Refutation not found, incomplete strategy % 42.62/6.93 % (1665586)Time elapsed: 0.005 s % 42.62/6.93 % (1665586)Peak memory usage: 89 MB % 42.62/6.93 % (1665586)Instructions burned: 3 (million) % 42.62/6.93 % (1665588)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=1187187151:st=5:i=1054:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2954 on theBenchmark for (2954ds/1054Mi) % 42.62/6.93 % (1665588)Refutation not found, incomplete strategy % 42.62/6.93 % (1665588)------------------------------ % 42.62/6.93 % (1665588)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 42.62/6.93 % (1665588)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.62/6.93 % (1665588)CaDiCaL version: 2.1.3 % 42.62/6.93 % (1665588)Termination reason: Refutation not found, incomplete strategy % 42.62/6.93 % (1665588)Time elapsed: 0.008 s % 42.62/6.93 % (1665588)Peak memory usage: 89 MB % 42.62/6.93 % (1665588)Instructions burned: 5 (million) % 42.62/6.93 % (1665592)lrs-1002_1_to=kbo:sas=z3:si=on:norm_ineq=on:sos=on:tha=some:random_seed=307914621:i=107:rtra=on_2953 on theBenchmark for (2953ds/107Mi) % 42.62/6.93 % (1665584)Instruction limit reached! % 42.62/6.93 % (1665584)------------------------------ % 42.62/6.93 % (1665584)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 42.62/6.93 % (1665584)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.62/6.93 % (1665584)CaDiCaL version: 2.1.3 % 42.62/6.93 % (1665584)Termination reason: Instruction limit % 42.62/6.93 % (1665584)Termination phase: Saturation % 42.62/6.93 % (1665584)Time elapsed: 0.349 s % 42.62/6.93 % (1665584)Peak memory usage: 135 MB % 42.62/6.93 % (1665584)Instructions burned: 276 (million) % 42.62/6.93 % (1665593)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=1704356575:s2a=on:i=450:doe=on:nm=32:rtra=on_2953 on theBenchmark for (2953ds/450Mi) % 42.62/6.93 % (1665592)Refutation not found, incomplete strategy % 49.21/7.61 % (1665592)------------------------------ % 49.21/7.61 % (1665592)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 49.21/7.61 % (1665592)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 49.21/7.61 % (1665592)CaDiCaL version: 2.1.3 % 49.21/7.61 % (1665592)Termination reason: Refutation not found, incomplete strategy % 49.21/7.61 % (1665592)Time elapsed: 0.044 s % 49.21/7.61 % (1665592)Peak memory usage: 116 MB % 49.21/7.61 % (1665592)Instructions burned: 8 (million) % 49.21/7.61 % (1665585)Instruction limit reached! % 49.21/7.61 % (1665585)------------------------------ % 49.21/7.61 % (1665585)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 49.21/7.61 % (1665585)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 49.21/7.61 % (1665585)CaDiCaL version: 2.1.3 % 49.21/7.61 % (1665585)Termination reason: Instruction limit % 49.21/7.61 % (1665585)Termination phase: Saturation % 49.21/7.61 % (1665585)Time elapsed: 0.446 s % 49.21/7.61 % (1665585)Peak memory usage: 90 MB % 49.21/7.61 % (1665585)Instructions burned: 1053 (million) % 49.21/7.61 % (1665586)------------------------------ % 49.21/7.61 % (1665586)------------------------------ % 49.21/7.61 % (1665588)------------------------------ % 49.21/7.61 % (1665588)------------------------------ % 49.21/7.61 % (1665598)WARNING Broken Constraint: if demodulation_redundancy_check(ordering) has been set then forward_demodulation(off) is not equal to off or backward_demodulation(off) is not equal to off or partial_redundancy_check(off) is not equal to off % 49.21/7.61 % (1665598)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=2655276401:i=1090:aac=none:nm=0:rtra=on:rawr=on_2950 on theBenchmark for (2950ds/1090Mi) % 49.21/7.61 % (1665599)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=2094839327:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2949 on theBenchmark for (2949ds/130Mi) % 49.21/7.61 % (1665592)------------------------------ % 49.21/7.61 % (1665592)------------------------------ % 49.21/7.61 % (1665599)Instruction limit reached! % 49.21/7.61 % (1665599)------------------------------ % 49.21/7.61 % (1665599)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 49.21/7.61 % (1665599)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 49.21/7.61 % (1665599)CaDiCaL version: 2.1.3 % 49.21/7.61 % (1665599)Termination reason: Instruction limit % 49.21/7.61 % (1665599)Termination phase: Saturation % 49.21/7.61 % (1665599)Time elapsed: 0.115 s % 49.21/7.61 % (1665599)Peak memory usage: 117 MB % 49.21/7.61 % (1665599)Instructions burned: 131 (million) % 49.21/7.61 % (1665593)Instruction limit reached! % 49.21/7.61 % (1665593)------------------------------ % 49.21/7.61 % (1665593)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 49.21/7.61 % (1665593)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 49.21/7.61 % (1665593)CaDiCaL version: 2.1.3 % 49.21/7.61 % (1665593)Termination reason: Instruction limit % 49.21/7.61 % (1665593)Termination phase: Saturation % 49.21/7.61 % (1665593)Time elapsed: 0.465 s % 49.21/7.61 % (1665593)Peak memory usage: 134 MB % 49.21/7.61 % (1665593)Instructions burned: 450 (million) % 49.21/7.61 % (1665610)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=3434154398:i=312:kws=inv_frequency:nm=20:rtra=on_2948 on theBenchmark for (2948ds/312Mi) % 49.21/7.61 % (1665611)ott+10_1_to=kbo:sil=64000:si=on:sp=reverse_frequency:sos=on:random_seed=2824006083:i=491:doe=on:rtra=on:gtg=position_2947 on theBenchmark for (2947ds/491Mi) % 49.21/7.61 % (1665614)ott+1011_4:1_to=lpo:sil=64000:si=on:spb=intro:random_seed=483302076:s2a=on:i=835:s2at=2:rtra=on_2946 on theBenchmark for (2946ds/835Mi) % 49.21/7.61 % (1665615)ott+1011_2_to=lpo:sil=128000:si=on:sos=on:random_seed=245635654:i=307:bd=preordered:av=off:rtra=on:ev=cautious_2945 on theBenchmark for (2945ds/307Mi) % 49.21/7.61 % (1665617)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=3693948760:i=776:doe=on:rtra=on_2945 on theBenchmark for (2945ds/776Mi) % 49.21/7.61 % (1665615)Instruction limit reached! % 49.21/7.61 % (1665615)------------------------------ % 49.21/7.61 % (1665615)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 49.21/7.61 % (1665615)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 49.21/7.61 % (1665615)CaDiCaL version: 2.1.3 % 49.21/7.61 % (1665615)Termination reason: Instruction limit % 55.72/8.47 % (1665615)Termination phase: Saturation % 55.72/8.47 % (1665615)Time elapsed: 0.155 s % 55.72/8.47 % (1665615)Peak memory usage: 91 MB % 55.72/8.47 % (1665615)Instructions burned: 307 (million) % 55.72/8.47 % (1665610)Instruction limit reached! % 55.72/8.47 % (1665610)------------------------------ % 55.72/8.47 % (1665610)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 55.72/8.47 % (1665610)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 55.72/8.47 % (1665610)CaDiCaL version: 2.1.3 % 55.72/8.47 % (1665610)Termination reason: Instruction limit % 55.72/8.47 % (1665610)Termination phase: Saturation % 55.72/8.47 % (1665610)Time elapsed: 0.362 s % 55.72/8.47 % (1665610)Peak memory usage: 119 MB % 55.72/8.47 % (1665610)Instructions burned: 312 (million) % 55.72/8.47 % (1665622)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=1703414529:s2a=on:i=646:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2942 on theBenchmark for (2942ds/646Mi) % 55.72/8.47 % (1665611)Instruction limit reached! % 55.72/8.47 % (1665611)------------------------------ % 55.72/8.47 % (1665611)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 55.72/8.47 % (1665611)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 55.72/8.47 % (1665611)CaDiCaL version: 2.1.3 % 55.72/8.47 % (1665611)Termination reason: Instruction limit % 55.72/8.47 % (1665611)Termination phase: Saturation % 55.72/8.47 % (1665611)Time elapsed: 0.519 s % 55.72/8.47 % (1665611)Peak memory usage: 94 MB % 55.72/8.47 % (1665611)Instructions burned: 491 (million) % 55.72/8.47 % (1665623)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=3171372460:thitd=on:cond=fast:i=784:nm=30:rtra=on:gtg=all:tac=axiom_2941 on theBenchmark for (2941ds/784Mi) % 55.72/8.47 % (1665598)Instruction limit reached! % 55.72/8.47 % (1665598)------------------------------ % 55.72/8.47 % (1665598)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 55.72/8.47 % (1665598)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 55.72/8.47 % (1665598)CaDiCaL version: 2.1.3 % 55.72/8.47 % (1665598)Termination reason: Instruction limit % 55.72/8.47 % (1665598)Termination phase: Saturation % 55.72/8.47 % (1665598)Time elapsed: 0.899 s % 55.72/8.47 % (1665598)Peak memory usage: 122 MB % 55.72/8.47 % (1665598)Instructions burned: 1090 (million) % 55.72/8.47 % (1665626)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=3947715026:thitd=on:s2a=on:i=1131:add=on:canc=force:bd=all:rtra=on:tac=axiom:ev=off_2939 on theBenchmark for (2939ds/1131Mi) % 55.72/8.47 % (1665614)Instruction limit reached! % 55.72/8.47 % (1665614)------------------------------ % 55.72/8.47 % (1665614)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 55.72/8.47 % (1665614)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 55.72/8.47 % (1665614)CaDiCaL version: 2.1.3 % 55.72/8.47 % (1665614)Termination reason: Instruction limit % 55.72/8.47 % (1665614)Termination phase: Saturation % 55.72/8.47 % (1665614)Time elapsed: 0.778 s % 55.72/8.47 % (1665614)Peak memory usage: 93 MB % 55.72/8.47 % (1665614)Instructions burned: 835 (million) % 55.72/8.47 % (1665617)Instruction limit reached! % 55.72/8.47 % (1665617)------------------------------ % 55.72/8.47 % (1665617)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 55.72/8.47 % (1665617)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 55.72/8.47 % (1665617)CaDiCaL version: 2.1.3 % 55.72/8.47 % (1665617)Termination reason: Instruction limit % 55.72/8.47 % (1665617)Termination phase: Saturation % 55.72/8.47 % (1665617)Time elapsed: 0.716 s % 55.72/8.47 % (1665617)Peak memory usage: 121 MB % 55.72/8.47 % (1665617)Instructions burned: 777 (million) % 55.72/8.47 % (1665627)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=3038094675:s2pl=no:i=246:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2938 on theBenchmark for (2938ds/246Mi) % 55.72/8.47 % (1665623)Instruction limit reached! % 55.72/8.47 % (1665623)------------------------------ % 55.72/8.47 % (1665623)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 55.72/8.47 % (1665623)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 55.72/8.47 % (1665623)CaDiCaL version: 2.1.3 % 55.72/8.47 % (1665623)Termination reason: Instruction limit % 55.72/8.47 % (1665623)Termination phase: Saturation % 63.99/9.90 % (1665623)Time elapsed: 0.454 s % 63.99/9.90 % (1665623)Peak memory usage: 120 MB % 63.99/9.90 % (1665623)Instructions burned: 785 (million) % 63.99/9.90 % (1665631)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=1437455289:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2936 on theBenchmark for (2936ds/775Mi) % 63.99/9.90 % (1665633)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=2380170531:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2935 on theBenchmark for (2935ds/273Mi) % 63.99/9.90 % (1665627)Instruction limit reached! % 63.99/9.90 % (1665627)------------------------------ % 63.99/9.90 % (1665627)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 63.99/9.90 % (1665627)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 63.99/9.90 % (1665627)CaDiCaL version: 2.1.3 % 63.99/9.90 % (1665627)Termination reason: Instruction limit % 63.99/9.90 % (1665627)Termination phase: Saturation % 63.99/9.90 % (1665627)Time elapsed: 0.238 s % 63.99/9.90 % (1665627)Peak memory usage: 116 MB % 63.99/9.90 % (1665627)Instructions burned: 246 (million) % 63.99/9.90 % (1665634)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=3487694992:i=102:nm=16:rtra=on_2935 on theBenchmark for (2935ds/102Mi) % 63.99/9.90 % (1665622)Instruction limit reached! % 63.99/9.90 % (1665622)------------------------------ % 63.99/9.90 % (1665622)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 63.99/9.90 % (1665622)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 63.99/9.90 % (1665622)CaDiCaL version: 2.1.3 % 63.99/9.90 % (1665622)Termination reason: Instruction limit % 63.99/9.90 % (1665622)Termination phase: Saturation % 63.99/9.90 % (1665622)Time elapsed: 0.737 s % 63.99/9.90 % (1665622)Peak memory usage: 138 MB % 63.99/9.90 % (1665622)Instructions burned: 646 (million) % 63.99/9.90 % (1665634)Instruction limit reached! % 63.99/9.90 % (1665634)------------------------------ % 63.99/9.90 % (1665634)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 63.99/9.90 % (1665634)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 63.99/9.90 % (1665634)CaDiCaL version: 2.1.3 % 63.99/9.90 % (1665634)Termination reason: Instruction limit % 63.99/9.90 % (1665634)Termination phase: Saturation % 63.99/9.90 % (1665634)Time elapsed: 0.051 s % 63.99/9.90 % (1665634)Peak memory usage: 89 MB % 63.99/9.90 % (1665634)Instructions burned: 102 (million) % 63.99/9.90 % (1665637)lrs+10_1_to=lpo:sil=128000:si=on:bsr=unit_only:tha=off:random_seed=1329582041:avsq=on:s2a=on:i=1094:s2at=5:avsqr=4463,131072:rtra=on_2933 on theBenchmark for (2933ds/1094Mi) % 63.99/9.90 % (1665640)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=740689395:i=868:doe=on:nm=0:rtra=on:gtg=exists_sym_2932 on theBenchmark for (2932ds/868Mi) % 63.99/9.90 % (1665633)Instruction limit reached! % 63.99/9.90 % (1665633)------------------------------ % 63.99/9.90 % (1665633)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 63.99/9.90 % (1665633)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 63.99/9.90 % (1665633)CaDiCaL version: 2.1.3 % 63.99/9.90 % (1665633)Termination reason: Instruction limit % 63.99/9.90 % (1665633)Termination phase: Saturation % 63.99/9.90 % (1665633)Time elapsed: 0.281 s % 63.99/9.90 % (1665633)Peak memory usage: 92 MB % 63.99/9.90 % (1665633)Instructions burned: 273 (million) % 63.99/9.90 % (1665640)Refutation not found, incomplete strategy % 63.99/9.90 % (1665640)------------------------------ % 63.99/9.90 % (1665640)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 63.99/9.90 % (1665640)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 63.99/9.90 % (1665640)CaDiCaL version: 2.1.3 % 63.99/9.90 % (1665640)Termination reason: Refutation not found, incomplete strategy % 63.99/9.90 % (1665640)Time elapsed: 0.034 s % 63.99/9.90 % (1665640)Peak memory usage: 116 MB % 63.99/9.90 % (1665640)Instructions burned: 20 (million) % 63.99/9.90 % (1665639)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=1433929186:i=6400:doe=on:fsr=off:rtra=on_2932 on theBenchmark for (2932ds/6400Mi) % 63.99/9.90 % (1665643)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=2458085836:i=1846:canc=cautious:fsr=off:rtra=on_2930 on theBenchmark for (2930ds/1846Mi) % 83.06/12.27 % (1665640)------------------------------ % 83.06/12.27 % (1665640)------------------------------ % 83.06/12.27 % (1665626)Instruction limit reached! % 83.06/12.27 % (1665626)------------------------------ % 83.06/12.27 % (1665626)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 83.06/12.27 % (1665626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.06/12.27 % (1665626)CaDiCaL version: 2.1.3 % 83.06/12.27 % (1665626)Termination reason: Instruction limit % 83.06/12.27 % (1665626)Termination phase: Saturation % 83.06/12.27 % (1665626)Time elapsed: 1.175 s % 83.06/12.27 % (1665626)Peak memory usage: 122 MB % 83.06/12.27 % (1665626)Instructions burned: 1131 (million) % 83.06/12.27 % (1665631)Instruction limit reached! % 83.06/12.27 % (1665631)------------------------------ % 83.06/12.27 % (1665631)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 83.06/12.27 % (1665631)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.06/12.27 % (1665631)CaDiCaL version: 2.1.3 % 83.06/12.27 % (1665631)Termination reason: Instruction limit % 83.06/12.27 % (1665631)Termination phase: Saturation % 83.06/12.27 % (1665631)Time elapsed: 0.833 s % 83.06/12.27 % (1665631)Peak memory usage: 95 MB % 83.06/12.27 % (1665631)Instructions burned: 775 (million) % 83.06/12.27 % (1665646)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=1506588761:s2a=on:i=36816:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2927 on theBenchmark for (2927ds/36816Mi) % 83.06/12.27 % (1665646)Refutation not found, incomplete strategy % 83.06/12.27 % (1665646)------------------------------ % 83.06/12.27 % (1665646)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 83.06/12.27 % (1665646)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.06/12.27 % (1665646)CaDiCaL version: 2.1.3 % 83.06/12.27 % (1665646)Termination reason: Refutation not found, incomplete strategy % 83.06/12.27 % (1665646)Time elapsed: 0.002 s % 83.06/12.27 % (1665646)Peak memory usage: 88 MB % 83.06/12.27 % (1665646)Instructions burned: 1 (million) % 83.06/12.27 % (1665647)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=2732143014:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2925 on theBenchmark for (2925ds/273Mi) % 83.06/12.27 % (1665646)------------------------------ % 83.06/12.27 % (1665646)------------------------------ % 83.06/12.27 % (1665648)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=4040670942:i=863:doe=on:nm=0:rtra=on:gtg=exists_sym_2925 on theBenchmark for (2925ds/863Mi) % 83.06/12.27 % (1665637)Instruction limit reached! % 83.06/12.27 % (1665637)------------------------------ % 83.06/12.27 % (1665637)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 83.06/12.27 % (1665637)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.06/12.27 % (1665637)CaDiCaL version: 2.1.3 % 83.06/12.27 % (1665637)Termination reason: Instruction limit % 83.06/12.27 % (1665637)Termination phase: Saturation % 83.06/12.27 % (1665637)Time elapsed: 0.838 s % 83.06/12.27 % (1665637)Peak memory usage: 89 MB % 83.06/12.27 % (1665637)Instructions burned: 1094 (million) % 83.06/12.27 % (1665648)Refutation not found, incomplete strategy % 83.06/12.27 % (1665648)------------------------------ % 83.06/12.27 % (1665648)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 83.06/12.27 % (1665648)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.06/12.27 % (1665648)CaDiCaL version: 2.1.3 % 83.06/12.27 % (1665648)Termination reason: Refutation not found, incomplete strategy % 83.06/12.27 % (1665648)Time elapsed: 0.056 s % 83.06/12.27 % (1665648)Peak memory usage: 117 MB % 83.06/12.27 % (1665648)Instructions burned: 19 (million) % 83.06/12.27 % (1665651)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=2126066255:i=5811:kws=precedence:nm=0:rtra=on_2923 on theBenchmark for (2923ds/5811Mi) % 83.06/12.27 % (1665647)Instruction limit reached! % 83.06/12.27 % (1665647)------------------------------ % 83.06/12.27 % (1665647)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 83.06/12.27 % (1665647)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.06/12.27 % (1665647)CaDiCaL version: 2.1.3 % 83.06/12.27 % (1665647)Termination reason: Instruction limit % 83.06/12.27 % (1665647)Termination phase: Saturation % 83.06/12.27 % (1665647)Time elapsed: 0.301 s % 83.06/12.27 % (1665647)Peak memory usage: 91 MB % 83.06/12.27 % (1665647)Instructions burned: 273 (million) % 83.06/12.27 % (1665653)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=1057867697:i=2216:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2922 on theBenchmark for (2922ds/2216Mi) % 97.91/14.38 % (1665648)------------------------------ % 97.91/14.38 % (1665648)------------------------------ % 97.91/14.38 % (1665655)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=1531102168:i=801:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2920 on theBenchmark for (2920ds/801Mi) % 97.91/14.38 % (1665655)Refutation not found, incomplete strategy % 97.91/14.38 % (1665655)------------------------------ % 97.91/14.38 % (1665655)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 97.91/14.38 % (1665655)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 97.91/14.38 % (1665655)CaDiCaL version: 2.1.3 % 97.91/14.38 % (1665655)Termination reason: Refutation not found, incomplete strategy % 97.91/14.38 % (1665655)Time elapsed: 0.005 s % 97.91/14.38 % (1665655)Peak memory usage: 89 MB % 97.91/14.38 % (1665655)Instructions burned: 3 (million) % 97.91/14.38 % (1665657)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=3270629174:st=5:i=1026:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2918 on theBenchmark for (2918ds/1026Mi) % 97.91/14.38 % (1665657)Refutation not found, incomplete strategy % 97.91/14.38 % (1665657)------------------------------ % 97.91/14.38 % (1665657)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 97.91/14.38 % (1665657)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 97.91/14.38 % (1665657)CaDiCaL version: 2.1.3 % 97.91/14.38 % (1665657)Termination reason: Refutation not found, incomplete strategy % 97.91/14.38 % (1665657)Time elapsed: 0.008 s % 97.91/14.38 % (1665657)Peak memory usage: 89 MB % 97.91/14.38 % (1665657)Instructions burned: 5 (million) % 97.91/14.38 % (1665655)------------------------------ % 97.91/14.38 % (1665655)------------------------------ % 97.91/14.38 % (1665583)Instruction limit reached! % 97.91/14.38 % (1665583)------------------------------ % 97.91/14.38 % (1665583)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 97.91/14.38 % (1665583)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 97.91/14.38 % (1665583)CaDiCaL version: 2.1.3 % 97.91/14.38 % (1665583)Termination reason: Instruction limit % 97.91/14.38 % (1665583)Termination phase: Saturation % 97.91/14.38 % (1665583)Time elapsed: 4.048 s % 97.91/14.38 % (1665583)Peak memory usage: 114 MB % 97.91/14.38 % (1665583)Instructions burned: 4429 (million) % 97.91/14.38 % (1665643)Instruction limit reached! % 97.91/14.38 % (1665643)------------------------------ % 97.91/14.38 % (1665643)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 97.91/14.38 % (1665643)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 97.91/14.38 % (1665643)CaDiCaL version: 2.1.3 % 97.91/14.38 % (1665643)Termination reason: Instruction limit % 97.91/14.38 % (1665643)Termination phase: Saturation % 97.91/14.38 % (1665643)Time elapsed: 1.582 s % 97.91/14.38 % (1665643)Peak memory usage: 96 MB % 97.91/14.38 % (1665643)Instructions burned: 1846 (million) % 97.91/14.38 % (1665657)------------------------------ % 97.91/14.38 % (1665657)------------------------------ % 97.91/14.38 % (1665661)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=1394338648:i=3509:rtra=on_2913 on theBenchmark for (2913ds/3509Mi) % 97.91/14.38 % (1665663)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=2774222656:st=2:i=2127:sd=12:ep=R:rtra=on:ss=axioms_2913 on theBenchmark for (2913ds/2127Mi) % 97.91/14.38 % (1665664)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=1903783867:i=1959:rtra=on:fsd=on:proc=on_2912 on theBenchmark for (2912ds/1959Mi) % 97.91/14.38 % (1665664)Refutation not found, incomplete strategy % 97.91/14.38 % (1665664)------------------------------ % 97.91/14.38 % (1665664)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 97.91/14.38 % (1665664)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 97.91/14.38 % (1665664)CaDiCaL version: 2.1.3 % 97.91/14.38 % (1665664)Termination reason: Refutation not found, incomplete strategy % 97.91/14.38 % (1665664)Time elapsed: 0.050 s % 97.91/14.38 % (1665664)Peak memory usage: 117 MB % 97.91/14.38 % (1665664)Instructions burned: 13 (million) % 97.91/14.38 % (1665665)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=361830702:s2a=on:i=3553:nm=0:rtra=on_2911 on theBenchmark for (2911ds/3553Mi) % 97.91/14.38 % (1665664)------------------------------ % 150.51/21.72 % (1665664)------------------------------ % 150.51/21.72 % (1665670)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=1895253605:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2905 on theBenchmark for (2905ds/3201Mi) % 150.51/21.72 % (1665653)Instruction limit reached! % 150.51/21.72 % (1665653)------------------------------ % 150.51/21.72 % (1665653)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 150.51/21.72 % (1665653)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 150.51/21.72 % (1665653)CaDiCaL version: 2.1.3 % 150.51/21.72 % (1665653)Termination reason: Instruction limit % 150.51/21.72 % (1665653)Termination phase: Saturation % 150.51/21.72 % (1665653)Time elapsed: 2.034 s % 150.51/21.72 % (1665653)Peak memory usage: 129 MB % 150.51/21.72 % (1665653)Instructions burned: 2217 (million) % 150.51/21.72 % (1665651)Instruction limit reached! % 150.51/21.72 % (1665651)------------------------------ % 150.51/21.72 % (1665651)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 150.51/21.72 % (1665651)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 150.51/21.72 % (1665651)CaDiCaL version: 2.1.3 % 150.51/21.72 % (1665651)Termination reason: Instruction limit % 150.51/21.72 % (1665651)Termination phase: Saturation % 150.51/21.72 % (1665651)Time elapsed: 2.359 s % 150.51/21.72 % (1665651)Peak memory usage: 124 MB % 150.51/21.72 % (1665651)Instructions burned: 5814 (million) % 150.51/21.72 % (1665672)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=1620447074:thitd=on:cond=on:i=4093:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2899 on theBenchmark for (2899ds/4093Mi) % 150.51/21.72 % (1665673)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=1830656473:cond=fast:i=21173:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2897 on theBenchmark for (2897ds/21173Mi) % 150.51/21.72 % (1665663)Instruction limit reached! % 150.51/21.72 % (1665663)------------------------------ % 150.51/21.72 % (1665663)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 150.51/21.72 % (1665663)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 150.51/21.72 % (1665663)CaDiCaL version: 2.1.3 % 150.51/21.72 % (1665663)Termination reason: Instruction limit % 150.51/21.72 % (1665663)Termination phase: Saturation % 150.51/21.72 % (1665663)Time elapsed: 1.778 s % 150.51/21.72 % (1665663)Peak memory usage: 102 MB % 150.51/21.72 % (1665663)Instructions burned: 2127 (million) % 150.51/21.72 % (1665680)lrs+11_1_to=lpo:thi=all:sas=z3:si=on:fd=off:sac=on:slsq=on:random_seed=3926116962:avsq=on:i=10544:avsqr=17,4:canc=force:rtra=on:gtg=exists_top:er=filter_2892 on theBenchmark for (2892ds/10544Mi) % 150.51/21.72 % (1665670)Refutation not found, incomplete strategy % 150.51/21.72 % (1665670)------------------------------ % 150.51/21.72 % (1665670)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 150.51/21.72 % (1665670)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 150.51/21.72 % (1665670)CaDiCaL version: 2.1.3 % 150.51/21.72 % (1665670)Termination reason: Refutation not found, incomplete strategy % 150.51/21.72 % (1665670)Time elapsed: 1.330 s % 150.51/21.72 % (1665670)Peak memory usage: 94 MB % 150.51/21.72 % (1665670)Instructions burned: 1704 (million) % 150.51/21.72 % (1665670)------------------------------ % 150.51/21.72 % (1665670)------------------------------ % 150.51/21.72 % (1665682)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=1601716431:avsq=on:i=1262:avsqr=1,16:rtra=on:rawr=on_2885 on theBenchmark for (2885ds/1262Mi) % 150.51/21.72 % (1665682)Refutation not found, incomplete strategy % 150.51/21.72 % (1665682)------------------------------ % 150.51/21.72 % (1665682)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 150.51/21.72 % (1665682)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 150.51/21.72 % (1665682)CaDiCaL version: 2.1.3 % 150.51/21.72 % (1665682)Termination reason: Refutation not found, incomplete strategy % 150.51/21.72 % (1665682)Time elapsed: 0.047 s % 150.51/21.72 % (1665682)Peak memory usage: 116 MB % 150.51/21.72 % (1665682)Instructions burned: 7 (million) % 150.51/21.72 % (1665661)Instruction limit reached! % 150.51/21.72 % (1665661)------------------------------ % 150.51/21.72 % (1665661)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 150.51/21.72 % (1665661)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 171.01/24.62 % (1665661)CaDiCaL version: 2.1.3 % 171.01/24.62 % (1665661)Termination reason: Instruction limit % 171.01/24.62 % (1665661)Termination phase: Saturation % 171.01/24.62 % (1665661)Time elapsed: 2.926 s % 171.01/24.62 % (1665661)Peak memory usage: 107 MB % 171.01/24.62 % (1665661)Instructions burned: 3509 (million) % 171.01/24.62 % (1665684)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=3420685350:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2881 on theBenchmark for (2881ds/775Mi) % 171.01/24.62 % (1665682)------------------------------ % 171.01/24.62 % (1665682)------------------------------ % 171.01/24.62 % (1665686)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=1275445899:i=270:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2878 on theBenchmark for (2878ds/270Mi) % 171.01/24.62 % (1665665)Instruction limit reached! % 171.01/24.62 % (1665665)------------------------------ % 171.01/24.62 % (1665665)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 171.01/24.62 % (1665665)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 171.01/24.62 % (1665665)CaDiCaL version: 2.1.3 % 171.01/24.62 % (1665665)Termination reason: Instruction limit % 171.01/24.62 % (1665665)Termination phase: Saturation % 171.01/24.62 % (1665665)Time elapsed: 3.429 s % 171.01/24.62 % (1665665)Peak memory usage: 105 MB % 171.01/24.62 % (1665665)Instructions burned: 3553 (million) % 171.01/24.62 % (1665686)Instruction limit reached! % 171.01/24.62 % (1665686)------------------------------ % 171.01/24.62 % (1665686)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 171.01/24.62 % (1665686)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 171.01/24.62 % (1665686)CaDiCaL version: 2.1.3 % 171.01/24.62 % (1665686)Termination reason: Instruction limit % 171.01/24.62 % (1665686)Termination phase: Saturation % 171.01/24.62 % (1665686)Time elapsed: 0.230 s % 171.01/24.62 % (1665686)Peak memory usage: 92 MB % 171.01/24.62 % (1665686)Instructions burned: 272 (million) % 171.01/24.62 % (1665688)ott+10_128_isp=bottom:to=lpo:sil=128000:si=on:urr=on:uwa=alasca_main:sac=on:slsq=on:random_seed=4048782841:i=17165:aac=none:doe=on:rtra=on:gtg=exists_all_2875 on theBenchmark for (2875ds/17165Mi) % 171.01/24.62 % (1665689)lrs+2_10_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_main:tha=some:random_seed=404818192:s2a=on:i=13094:s2at=-1:rtra=on_2873 on theBenchmark for (2873ds/13094Mi) % 171.01/24.62 % (1665684)Instruction limit reached! % 171.01/24.62 % (1665684)------------------------------ % 171.01/24.62 % (1665684)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 171.01/24.62 % (1665684)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 171.01/24.62 % (1665684)CaDiCaL version: 2.1.3 % 171.01/24.62 % (1665684)Termination reason: Instruction limit % 171.01/24.62 % (1665684)Termination phase: Saturation % 171.01/24.62 % (1665684)Time elapsed: 0.826 s % 171.01/24.62 % (1665684)Peak memory usage: 95 MB % 171.01/24.62 % (1665684)Instructions burned: 775 (million) % 171.01/24.62 % (1665639)Instruction limit reached! % 171.01/24.62 % (1665639)------------------------------ % 171.01/24.62 % (1665639)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 171.01/24.62 % (1665639)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 171.01/24.62 % (1665639)CaDiCaL version: 2.1.3 % 171.01/24.62 % (1665639)Termination reason: Instruction limit % 171.01/24.62 % (1665639)Termination phase: Saturation % 171.01/24.62 % (1665639)Time elapsed: 5.995 s % 171.01/24.62 % (1665639)Peak memory usage: 125 MB % 171.01/24.62 % (1665639)Instructions burned: 6401 (million) % 171.01/24.62 % (1665692)lrs+10_1_to=lpo:sil=128000:si=on:sp=occurrence:random_seed=1127935969:st=2:i=12633:rtra=on:ss=axioms_2870 on theBenchmark for (2870ds/12633Mi) % 171.01/24.62 % (1665693)dis+1011_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_frequency:lsd=20:nwc=3:random_seed=1478368851:i=1783:rtra=on:gtg=position_2869 on theBenchmark for (2869ds/1783Mi) % 171.01/24.62 % (1665672)Instruction limit reached! % 171.01/24.62 % (1665672)------------------------------ % 171.01/24.62 % (1665672)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 171.01/24.62 % (1665672)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 171.01/24.62 % (1665672)CaDiCaL version: 2.1.3 % 171.01/24.62 % (1665672)Termination reason: Instruction limit % 171.01/24.62 % (1665672)Termination phase: Saturation % 171.01/24.62 % (1665672)Time elapsed: 3.574 s % 171.01/24.62 % (1665672)Peak memory usage: 141 MB % 185.68/26.83 % (1665672)Instructions burned: 4094 (million) % 185.68/26.83 % (1665698)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=3422026156:i=5451:aac=none:doe=on:nm=0:rtra=on:amm=off:gtg=position_2860 on theBenchmark for (2860ds/5451Mi) % 185.68/26.83 % (1665693)Instruction limit reached! % 185.68/26.83 % (1665693)------------------------------ % 185.68/26.83 % (1665693)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 185.68/26.83 % (1665693)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 185.68/26.83 % (1665693)CaDiCaL version: 2.1.3 % 185.68/26.83 % (1665693)Termination reason: Instruction limit % 185.68/26.83 % (1665693)Termination phase: Saturation % 185.68/26.83 % (1665693)Time elapsed: 1.769 s % 185.68/26.83 % (1665693)Peak memory usage: 124 MB % 185.68/26.83 % (1665693)Instructions burned: 1783 (million) % 185.68/26.83 % (1665700)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=347623924:i=4975:doe=on:nm=0:rtra=on:gtg=exists_sym_2848 on theBenchmark for (2848ds/4975Mi) % 185.68/26.83 % (1665700)Refutation not found, incomplete strategy % 185.68/26.83 % (1665700)------------------------------ % 185.68/26.83 % (1665700)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 185.68/26.83 % (1665700)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 185.68/26.83 % (1665700)CaDiCaL version: 2.1.3 % 185.68/26.83 % (1665700)Termination reason: Refutation not found, incomplete strategy % 185.68/26.83 % (1665700)Time elapsed: 0.056 s % 185.68/26.83 % (1665700)Peak memory usage: 116 MB % 185.68/26.83 % (1665700)Instructions burned: 19 (million) % 185.68/26.83 % (1665700)------------------------------ % 185.68/26.83 % (1665700)------------------------------ % 185.68/26.83 % (1665702)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=4016987579:i=2076:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2841 on theBenchmark for (2841ds/2076Mi) % 185.68/26.83 % (1665702)Instruction limit reached! % 185.68/26.83 % (1665702)------------------------------ % 185.68/26.83 % (1665702)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 185.68/26.83 % (1665702)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 185.68/26.83 % (1665702)CaDiCaL version: 2.1.3 % 185.68/26.83 % (1665702)Termination reason: Instruction limit % 185.68/26.83 % (1665702)Termination phase: Saturation % 185.68/26.83 % (1665702)Time elapsed: 1.954 s % 185.68/26.83 % (1665702)Peak memory usage: 126 MB % 185.68/26.83 % (1665702)Instructions burned: 2076 (million) % 185.68/26.83 % (1665706)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=2733582375:i=5145:rtra=on_2819 on theBenchmark for (2819ds/5145Mi) % 185.68/26.83 % (1665673)Instruction limit reached! % 185.68/26.83 % (1665673)------------------------------ % 185.68/26.83 % (1665673)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 185.68/26.83 % (1665673)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 185.68/26.83 % (1665673)CaDiCaL version: 2.1.3 % 185.68/26.83 % (1665673)Termination reason: Instruction limit % 185.68/26.83 % (1665673)Termination phase: Saturation % 185.68/26.83 % (1665673)Time elapsed: 8.684 s % 185.68/26.83 % (1665673)Peak memory usage: 138 MB % 185.68/26.83 % (1665673)Instructions burned: 21175 (million) % 185.68/26.83 % (1665698)Instruction limit reached! % 185.68/26.83 % (1665698)------------------------------ % 185.68/26.83 % (1665698)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 185.68/26.83 % (1665698)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 185.68/26.83 % (1665698)CaDiCaL version: 2.1.3 % 185.68/26.83 % (1665698)Termination reason: Instruction limit % 185.68/26.83 % (1665698)Termination phase: Saturation % 185.68/26.83 % (1665698)Time elapsed: 5.201 s % 185.68/26.83 % (1665698)Peak memory usage: 144 MB % 185.68/26.83 % (1665698)Instructions burned: 5451 (million) % 185.68/26.83 % (1665710)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=271948869:i=3509:rtra=on_2807 on theBenchmark for (2807ds/3509Mi) % 185.68/26.83 % (1665711)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=2956473680:st=2:i=13800:sd=12:ep=R:rtra=on:ss=axioms_2805 on theBenchmark for (2805ds/13800Mi) % 185.68/26.83 % (1665710)Instruction limit reached! % 185.68/26.83 % (1665710)------------------------------ % 185.68/26.83 % (1665710)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 185.68/26.83 % (1665710)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 232.85/33.33 % (1665710)CaDiCaL version: 2.1.3 % 232.85/33.33 % (1665710)Termination reason: Instruction limit % 232.85/33.33 % (1665710)Termination phase: Saturation % 232.85/33.33 % (1665710)Time elapsed: 1.802 s % 232.85/33.33 % (1665710)Peak memory usage: 104 MB % 232.85/33.33 % (1665710)Instructions burned: 3509 (million) % 232.85/33.33 % (1665714)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=2105988077:i=1412:rtra=on:fsd=on:proc=on_2787 on theBenchmark for (2787ds/1412Mi) % 232.85/33.33 % (1665714)Refutation not found, incomplete strategy % 232.85/33.33 % (1665714)------------------------------ % 232.85/33.33 % (1665714)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 232.85/33.33 % (1665714)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 232.85/33.33 % (1665714)CaDiCaL version: 2.1.3 % 232.85/33.33 % (1665714)Termination reason: Refutation not found, incomplete strategy % 232.85/33.33 % (1665714)Time elapsed: 0.029 s % 232.85/33.33 % (1665714)Peak memory usage: 117 MB % 232.85/33.33 % (1665714)Instructions burned: 14 (million) % 232.85/33.33 % (1665714)------------------------------ % 232.85/33.33 % (1665714)------------------------------ % 232.85/33.33 % (1665716)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 % 232.85/33.33 % (1665716)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=2598081421:i=11747:aac=none:nm=0:rtra=on:rawr=on_2782 on theBenchmark for (2782ds/11747Mi) % 232.85/33.33 % (1665706)Instruction limit reached! % 232.85/33.33 % (1665706)------------------------------ % 232.85/33.33 % (1665706)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 232.85/33.33 % (1665706)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 232.85/33.33 % (1665706)CaDiCaL version: 2.1.3 % 232.85/33.33 % (1665706)Termination reason: Instruction limit % 232.85/33.33 % (1665706)Termination phase: Saturation % 232.85/33.33 % (1665706)Time elapsed: 4.087 s % 232.85/33.33 % (1665706)Peak memory usage: 94 MB % 232.85/33.33 % (1665706)Instructions burned: 5146 (million) % 232.85/33.33 % (1665680)Instruction limit reached! % 232.85/33.33 % (1665680)------------------------------ % 232.85/33.33 % (1665680)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 232.85/33.33 % (1665680)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 232.85/33.33 % (1665680)CaDiCaL version: 2.1.3 % 232.85/33.33 % (1665680)Termination reason: Instruction limit % 232.85/33.33 % (1665680)Termination phase: Saturation % 232.85/33.33 % (1665680)Time elapsed: 11.407 s % 232.85/33.33 % (1665680)Peak memory usage: 199 MB % 232.85/33.33 % (1665680)Instructions burned: 10544 (million) % 232.85/33.33 % (1665718)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=1537959611:s2a=on:i=3553:nm=0:rtra=on_2776 on theBenchmark for (2776ds/3553Mi) % 232.85/33.33 % (1665719)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=2354679374:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2775 on theBenchmark for (2775ds/3201Mi) % 232.85/33.33 % (1665689)Instruction limit reached! % 232.85/33.33 % (1665689)------------------------------ % 232.85/33.33 % (1665689)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 232.85/33.33 % (1665689)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 232.85/33.33 % (1665689)CaDiCaL version: 2.1.3 % 232.85/33.33 % (1665689)Termination reason: Instruction limit % 232.85/33.33 % (1665689)Termination phase: Saturation % 232.85/33.33 % (1665689)Time elapsed: 10.599 s % 232.85/33.33 % (1665689)Peak memory usage: 129 MB % 232.85/33.33 % (1665689)Instructions burned: 13094 (million) % 232.85/33.33 % (1665724)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=1758161381:thitd=on:cond=on:i=4081:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2764 on theBenchmark for (2764ds/4081Mi) % 232.85/33.33 % (1665719)Refutation not found, incomplete strategy % 232.85/33.33 % (1665719)------------------------------ % 232.85/33.33 % (1665719)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 232.85/33.33 % (1665719)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 232.85/33.33 % (1665719)CaDiCaL version: 2.1.3 % 232.85/33.33 % (1665719)Termination reason: Refutation not found, incomplete strategy % 269.59/38.58 % (1665719)Time elapsed: 1.409 s % 269.59/38.58 % (1665719)Peak memory usage: 94 MB % 269.59/38.58 % (1665719)Instructions burned: 1824 (million) % 269.59/38.58 % (1665688)Instruction limit reached! % 269.59/38.58 % (1665688)------------------------------ % 269.59/38.58 % (1665688)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 269.59/38.58 % (1665688)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.59/38.58 % (1665688)CaDiCaL version: 2.1.3 % 269.59/38.58 % (1665688)Termination reason: Instruction limit % 269.59/38.58 % (1665688)Termination phase: Saturation % 269.59/38.58 % (1665688)Time elapsed: 11.771 s % 269.59/38.58 % (1665688)Peak memory usage: 147 MB % 269.59/38.58 % (1665688)Instructions burned: 17168 (million) % 269.59/38.58 % (1665719)------------------------------ % 269.59/38.58 % (1665719)------------------------------ % 269.59/38.58 % (1665726)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=1750191527:cond=fast:i=20260:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2754 on theBenchmark for (2754ds/20260Mi) % 269.59/38.58 % (1665727)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=913639244:s2a=on:i=58627:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2754 on theBenchmark for (2754ds/58627Mi) % 269.59/38.58 % (1665727)Refutation not found, incomplete strategy % 269.59/38.58 % (1665727)------------------------------ % 269.59/38.58 % (1665727)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 269.59/38.58 % (1665727)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.59/38.58 % (1665727)CaDiCaL version: 2.1.3 % 269.59/38.58 % (1665727)Termination reason: Refutation not found, incomplete strategy % 269.59/38.58 % (1665727)Time elapsed: 0.003 s % 269.59/38.58 % (1665727)Peak memory usage: 88 MB % 269.59/38.58 % (1665727)Instructions burned: 1 (million) % 269.59/38.58 % (1665727)------------------------------ % 269.59/38.58 % (1665727)------------------------------ % 269.59/38.58 % (1665730)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=2187212815:avsq=on:i=6258:avsqr=1,16:rtra=on:rawr=on_2747 on theBenchmark for (2747ds/6258Mi) % 269.59/38.58 % (1665730)Refutation not found, incomplete strategy % 269.59/38.58 % (1665730)------------------------------ % 269.59/38.58 % (1665730)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 269.59/38.58 % (1665730)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.59/38.58 % (1665730)CaDiCaL version: 2.1.3 % 269.59/38.58 % (1665730)Termination reason: Refutation not found, incomplete strategy % 269.59/38.58 % (1665730)Time elapsed: 0.037 s % 269.59/38.58 % (1665730)Peak memory usage: 116 MB % 269.59/38.58 % (1665730)Instructions burned: 8 (million) % 269.59/38.58 % (1665692)Instruction limit reached! % 269.59/38.58 % (1665692)------------------------------ % 269.59/38.58 % (1665692)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 269.59/38.58 % (1665692)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.59/38.58 % (1665692)CaDiCaL version: 2.1.3 % 269.59/38.58 % (1665692)Termination reason: Instruction limit % 269.59/38.58 % (1665692)Termination phase: Saturation % 269.59/38.58 % (1665692)Time elapsed: 12.759 s % 269.59/38.58 % (1665692)Peak memory usage: 132 MB % 269.59/38.58 % (1665692)Instructions burned: 12633 (million) % 269.59/38.58 % (1665730)------------------------------ % 269.59/38.58 % (1665730)------------------------------ % 269.59/38.58 % (1665732)ott+10_128_isp=bottom:to=lpo:sil=128000:si=on:urr=on:uwa=alasca_main:sac=on:slsq=on:random_seed=1211001773:i=34001:aac=none:doe=on:rtra=on:gtg=exists_all_2740 on theBenchmark for (2740ds/34001Mi) % 269.59/38.58 % (1665718)Instruction limit reached! % 269.59/38.58 % (1665718)------------------------------ % 269.59/38.58 % (1665718)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 269.59/38.58 % (1665718)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.59/38.58 % (1665718)CaDiCaL version: 2.1.3 % 269.59/38.58 % (1665718)Termination reason: Instruction limit % 269.59/38.58 % (1665718)Termination phase: Saturation % 269.59/38.58 % (1665718)Time elapsed: 3.510 s % 269.59/38.58 % (1665718)Peak memory usage: 105 MB % 269.59/38.58 % (1665718)Instructions burned: 3553 (million) % 269.59/38.58 % (1665733)lrs+2_10_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_main:tha=some:random_seed=459818221:s2a=on:i=71622:s2at=-1:rtra=on_2740 on theBenchmark for (2740ds/71622Mi) % 269.59/38.58 % (1665735)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:sTerminated %------------------------------------------------------------------------------