%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWX150_1 : TPTP v9.3.1. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % Computer : n006.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:45:58 PM UTC 2026 % Result : Timeout 293.53s 42.28s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.04 % Problem : SWX150_1 : TPTP v9.3.1. Released v9.3.0. % 0.00/0.08 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.09/0.25 % Computer : n006.cluster.edu % 0.09/0.25 % Model : x86_64 x86_64 % 0.09/0.25 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.25 % Memory : 8046.5625MB % 0.09/0.25 % OS : Linux 6.8.0-71-generic % 0.09/0.25 % CPULimit : 300 % 0.09/0.25 % WCLimit : 300 % 0.09/0.25 % DateTime : Mon Sep 28 15:04:25 UTC 2026 % 0.09/0.26 % CPUTime : % 0.09/0.26 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.25/0.30 Running first-order theorem proving % 0.25/0.30 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 5.21/1.70 % (4035631)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule. % 5.21/1.70 % (4035645)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=4114132480:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi) % 5.21/1.70 % (4035645)Instruction limit reached! % 5.21/1.70 % (4035645)------------------------------ % 5.21/1.70 % (4035645)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.21/1.70 % (4035645)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.21/1.70 % (4035645)CaDiCaL version: 2.1.3 % 5.21/1.70 % (4035645)Termination reason: Instruction limit % 5.21/1.70 % (4035645)Termination phase: shuffling % 5.21/1.70 % (4035645)Time elapsed: 0.006 s % 5.21/1.70 % (4035645)Peak memory usage: 85 MB % 5.21/1.70 % (4035645)Instructions burned: 14 (million) % 5.21/1.70 % (4035651)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=1918843626:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi) % 5.21/1.70 % (4035651)Instruction limit reached! % 5.21/1.70 % (4035651)------------------------------ % 5.21/1.70 % (4035651)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.21/1.70 % (4035651)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.21/1.70 % (4035651)CaDiCaL version: 2.1.3 % 5.21/1.70 % (4035651)Termination reason: Instruction limit % 5.21/1.70 % (4035651)Termination phase: Property scanning % 5.21/1.70 % (4035651)Time elapsed: 0.028 s % 5.21/1.70 % (4035651)Peak memory usage: 86 MB % 5.21/1.70 % (4035651)Instructions burned: 34 (million) % 5.21/1.70 % (4035647)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=340741441:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi) % 5.21/1.70 % (4035646)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=2654261592:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi) % 5.21/1.70 % (4035650)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=2143199376:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi) % 5.21/1.70 % (4035648)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=696001530:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi) % 5.21/1.70 % (4035649)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=3452496102:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi) % 5.21/1.70 % (4035649)Instruction limit reached! % 5.21/1.70 % (4035649)------------------------------ % 5.21/1.70 % (4035649)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.21/1.70 % (4035649)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.21/1.70 % (4035649)CaDiCaL version: 2.1.3 % 5.21/1.70 % (4035649)Termination reason: Instruction limit % 5.21/1.70 % (4035649)Termination phase: Property scanning % 5.21/1.70 % (4035649)Time elapsed: 0.004 s % 5.21/1.70 % (4035649)Peak memory usage: 85 MB % 5.21/1.70 % (4035649)Instructions burned: 4 (million) % 5.21/1.70 % (4035648)Instruction limit reached! % 5.21/1.70 % (4035648)------------------------------ % 5.21/1.70 % (4035648)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.21/1.70 % (4035648)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.21/1.70 % (4035648)CaDiCaL version: 2.1.3 % 5.21/1.70 % (4035648)Termination reason: Instruction limit % 5.21/1.70 % (4035648)Termination phase: Property scanning % 5.21/1.70 % (4035648)Time elapsed: 0.007 s % 5.21/1.70 % (4035648)Peak memory usage: 85 MB % 5.21/1.70 % (4035648)Instructions burned: 8 (million) % 5.21/1.70 % (4035650)Instruction limit reached! % 5.21/1.70 % (4035650)------------------------------ % 5.21/1.70 % (4035650)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.21/1.70 % (4035650)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.21/1.70 % (4035650)CaDiCaL version: 2.1.3 % 5.21/1.70 % (4035650)Termination reason: Instruction limit % 5.21/1.70 % (4035650)Termination phase: Saturation % 5.21/1.70 % (4035650)Time elapsed: 0.032 s % 5.21/1.70 % (4035650)Peak memory usage: 86 MB % 5.21/1.70 % (4035650)Instructions burned: 46 (million) % 5.21/1.70 % (4035654)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=3900597373:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2997 on theBenchmark for (2997ds/14Mi) % 5.21/1.70 % (4035654)Instruction limit reached! % 5.21/1.70 % (4035654)------------------------------ % 6.51/1.97 % (4035654)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.51/1.97 % (4035654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.51/1.97 % (4035654)CaDiCaL version: 2.1.3 % 6.51/1.97 % (4035654)Termination reason: Instruction limit % 6.51/1.97 % (4035654)Termination phase: Property scanning % 6.51/1.97 % (4035654)Time elapsed: 0.007 s % 6.51/1.97 % (4035654)Peak memory usage: 85 MB % 6.51/1.97 % (4035654)Instructions burned: 15 (million) % 6.51/1.97 % (4035647)Instruction limit reached! % 6.51/1.97 % (4035647)------------------------------ % 6.51/1.97 % (4035647)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.51/1.97 % (4035647)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.51/1.97 % (4035647)CaDiCaL version: 2.1.3 % 6.51/1.97 % (4035647)Termination reason: Instruction limit % 6.51/1.97 % (4035647)Termination phase: Saturation % 6.51/1.97 % (4035647)Time elapsed: 0.190 s % 6.51/1.97 % (4035647)Peak memory usage: 118 MB % 6.51/1.97 % (4035647)Instructions burned: 201 (million) % 6.51/1.97 % (4035661)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=967477752:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2996 on theBenchmark for (2996ds/29Mi) % 6.51/1.97 % (4035661)Instruction limit reached! % 6.51/1.97 % (4035661)------------------------------ % 6.51/1.97 % (4035661)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.51/1.97 % (4035661)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.51/1.97 % (4035661)CaDiCaL version: 2.1.3 % 6.51/1.97 % (4035661)Termination reason: Instruction limit % 6.51/1.97 % (4035661)Termination phase: Property scanning % 6.51/1.97 % (4035661)Time elapsed: 0.024 s % 6.51/1.97 % (4035661)Peak memory usage: 86 MB % 6.51/1.97 % (4035661)Instructions burned: 29 (million) % 6.51/1.97 % (4035663)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=1410786271:i=24:canc=force:rtra=on_2996 on theBenchmark for (2996ds/24Mi) % 6.51/1.97 % (4035662)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=3546972454:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2996 on theBenchmark for (2996ds/16Mi) % 6.51/1.97 % (4035662)Instruction limit reached! % 6.51/1.97 % (4035662)------------------------------ % 6.51/1.97 % (4035662)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.51/1.97 % (4035662)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.51/1.97 % (4035662)CaDiCaL version: 2.1.3 % 6.51/1.97 % (4035662)Termination reason: Instruction limit % 6.51/1.97 % (4035662)Termination phase: Preprocessing 1 % 6.51/1.97 % (4035662)Time elapsed: 0.014 s % 6.51/1.97 % (4035662)Peak memory usage: 86 MB % 6.51/1.97 % (4035662)Instructions burned: 16 (million) % 6.51/1.97 % (4035646)Instruction limit reached! % 6.51/1.97 % (4035646)------------------------------ % 6.51/1.97 % (4035646)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.51/1.97 % (4035646)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.51/1.97 % (4035646)CaDiCaL version: 2.1.3 % 6.51/1.97 % (4035646)Termination reason: Instruction limit % 6.51/1.97 % (4035646)Termination phase: Saturation % 6.51/1.97 % (4035646)Time elapsed: 0.270 s % 6.51/1.97 % (4035646)Peak memory usage: 116 MB % 6.51/1.97 % (4035646)Instructions burned: 307 (million) % 6.51/1.97 % (4035663)Instruction limit reached! % 6.51/1.97 % (4035663)------------------------------ % 6.51/1.97 % (4035663)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.51/1.97 % (4035663)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.51/1.97 % (4035663)CaDiCaL version: 2.1.3 % 6.51/1.97 % (4035663)Termination reason: Instruction limit % 6.51/1.97 % (4035663)Termination phase: Property scanning % 6.51/1.97 % (4035663)Time elapsed: 0.022 s % 6.51/1.97 % (4035663)Peak memory usage: 86 MB % 6.51/1.97 % (4035663)Instructions burned: 27 (million) % 6.51/1.97 % (4035664)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=3850321646:i=27:canc=cautious:fsr=off:rtra=on_2996 on theBenchmark for (2996ds/27Mi) % 6.51/1.97 % (4035666)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=1941398189:i=85:gtgl=4:rtra=on:gtg=exists_sym_2995 on theBenchmark for (2995ds/85Mi) % 6.51/1.97 % (4035664)Instruction limit reached! % 6.51/1.97 % (4035664)------------------------------ % 9.35/2.24 % (4035664)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.35/2.24 % (4035664)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.35/2.24 % (4035664)CaDiCaL version: 2.1.3 % 9.35/2.24 % (4035664)Termination reason: Instruction limit % 9.35/2.24 % (4035664)Termination phase: Property scanning % 9.35/2.24 % (4035664)Time elapsed: 0.023 s % 9.35/2.24 % (4035664)Peak memory usage: 86 MB % 9.35/2.24 % (4035664)Instructions burned: 27 (million) % 9.35/2.24 % (4035666)Instruction limit reached! % 9.35/2.24 % (4035666)------------------------------ % 9.35/2.24 % (4035666)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.35/2.24 % (4035666)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.35/2.24 % (4035666)CaDiCaL version: 2.1.3 % 9.35/2.24 % (4035666)Termination reason: Instruction limit % 9.35/2.24 % (4035666)Termination phase: Property scanning % 9.35/2.24 % (4035666)Time elapsed: 0.034 s % 9.35/2.24 % (4035666)Peak memory usage: 87 MB % 9.35/2.24 % (4035666)Instructions burned: 87 (million) % 9.35/2.24 % (4035673)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=2108409401:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2994 on theBenchmark for (2994ds/66Mi) % 9.35/2.24 % (4035667)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=2465828792:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2994 on theBenchmark for (2994ds/2Mi) % 9.35/2.24 % (4035667)Instruction limit reached! % 9.35/2.24 % (4035667)------------------------------ % 9.35/2.24 % (4035667)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.35/2.24 % (4035667)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.35/2.24 % (4035667)CaDiCaL version: 2.1.3 % 9.35/2.24 % (4035667)Termination reason: Instruction limit % 9.35/2.24 % (4035667)Termination phase: shuffling % 9.35/2.24 % (4035667)Time elapsed: 0.002 s % 9.35/2.24 % (4035667)Peak memory usage: 85 MB % 9.35/2.24 % (4035667)Instructions burned: 2 (million) % 9.35/2.24 % (4035673)Instruction limit reached! % 9.35/2.24 % (4035673)------------------------------ % 9.35/2.24 % (4035673)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.35/2.24 % (4035673)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.35/2.24 % (4035673)CaDiCaL version: 2.1.3 % 9.35/2.24 % (4035673)Termination reason: Instruction limit % 9.35/2.24 % (4035673)Termination phase: Saturation % 9.35/2.24 % (4035673)Time elapsed: 0.028 s % 9.35/2.24 % (4035673)Peak memory usage: 87 MB % 9.35/2.24 % (4035673)Instructions burned: 67 (million) % 9.35/2.24 % (4035671)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=2823732396:i=181:rtra=on:ss=axioms:ev=cautious_2994 on theBenchmark for (2994ds/181Mi) % 9.35/2.24 % (4035672)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=3984809767:i=4:ep=RST:ins=2:rtra=on_2994 on theBenchmark for (2994ds/4Mi) % 9.35/2.24 % (4035672)Instruction limit reached! % 9.35/2.24 % (4035672)------------------------------ % 9.35/2.24 % (4035672)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.35/2.24 % (4035672)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.35/2.24 % (4035672)CaDiCaL version: 2.1.3 % 9.35/2.24 % (4035672)Termination reason: Instruction limit % 9.35/2.24 % (4035672)Termination phase: Property scanning % 9.35/2.24 % (4035672)Time elapsed: 0.005 s % 9.35/2.24 % (4035672)Peak memory usage: 85 MB % 9.35/2.24 % (4035672)Instructions burned: 5 (million) % 9.35/2.24 % (4035671)Refutation not found, incomplete strategy % 9.35/2.24 % (4035671)------------------------------ % 9.35/2.24 % (4035671)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.35/2.24 % (4035671)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.35/2.24 % (4035671)CaDiCaL version: 2.1.3 % 9.35/2.24 % (4035671)Termination reason: Refutation not found, incomplete strategy % 9.35/2.24 % (4035671)Time elapsed: 0.031 s % 9.35/2.24 % (4035671)Peak memory usage: 88 MB % 9.35/2.24 % (4035671)Instructions burned: 47 (million) % 9.35/2.24 % (4035675)lrs+10_1_thi=all:si=on:fd=off:random_seed=3595796054:i=53:rtra=on:gtg=all_2994 on theBenchmark for (2994ds/53Mi) % 9.35/2.24 % (4035677)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=2320945442:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2993 on theBenchmark for (2993ds/8Mi) % 10.44/2.49 % (4035677)Instruction limit reached! % 10.44/2.49 % (4035677)------------------------------ % 10.44/2.49 % (4035677)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.44/2.49 % (4035677)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.44/2.49 % (4035677)CaDiCaL version: 2.1.3 % 10.44/2.49 % (4035677)Termination reason: Instruction limit % 10.44/2.49 % (4035677)Termination phase: Property scanning % 10.44/2.49 % (4035677)Time elapsed: 0.007 s % 10.44/2.49 % (4035677)Peak memory usage: 85 MB % 10.44/2.49 % (4035677)Instructions burned: 8 (million) % 10.44/2.49 % (4035675)Instruction limit reached! % 10.44/2.49 % (4035675)------------------------------ % 10.44/2.49 % (4035675)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.44/2.49 % (4035675)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.44/2.49 % (4035675)CaDiCaL version: 2.1.3 % 10.44/2.49 % (4035675)Termination reason: Instruction limit % 10.44/2.49 % (4035675)Termination phase: Property scanning % 10.44/2.49 % (4035675)Time elapsed: 0.043 s % 10.44/2.49 % (4035675)Peak memory usage: 86 MB % 10.44/2.49 % (4035675)Instructions burned: 54 (million) % 10.44/2.49 % (4035678)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=3709453787:st=3:i=2:rtra=on:ss=axioms_2993 on theBenchmark for (2993ds/2Mi) % 10.44/2.49 % (4035678)Instruction limit reached! % 10.44/2.49 % (4035678)------------------------------ % 10.44/2.49 % (4035678)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.44/2.49 % (4035678)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.44/2.49 % (4035678)CaDiCaL version: 2.1.3 % 10.44/2.49 % (4035678)Termination reason: Instruction limit % 10.44/2.49 % (4035678)Termination phase: shuffling % 10.44/2.49 % (4035678)Time elapsed: 0.002 s % 10.44/2.49 % (4035678)Peak memory usage: 85 MB % 10.44/2.49 % (4035678)Instructions burned: 2 (million) % 10.44/2.49 % (4035682)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=2422635243:i=127:doe=on:rtra=on_2992 on theBenchmark for (2992ds/127Mi) % 10.44/2.49 % (4035681)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=3181407758:i=2:doe=on:canc=force:asg=cautious:rtra=on_2992 on theBenchmark for (2992ds/2Mi) % 10.44/2.49 % (4035681)Instruction limit reached! % 10.44/2.49 % (4035681)------------------------------ % 10.44/2.49 % (4035681)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.44/2.49 % (4035681)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.44/2.49 % (4035681)CaDiCaL version: 2.1.3 % 10.44/2.49 % (4035681)Termination reason: Instruction limit % 10.44/2.49 % (4035681)Termination phase: shuffling % 10.44/2.49 % (4035681)Time elapsed: 0.002 s % 10.44/2.49 % (4035681)Peak memory usage: 85 MB % 10.44/2.49 % (4035681)Instructions burned: 2 (million) % 10.44/2.49 % (4035682)Instruction limit reached! % 10.44/2.49 % (4035682)------------------------------ % 10.44/2.49 % (4035682)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.44/2.49 % (4035682)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.44/2.49 % (4035682)CaDiCaL version: 2.1.3 % 10.44/2.49 % (4035682)Termination reason: Instruction limit % 10.44/2.49 % (4035682)Termination phase: Saturation % 10.44/2.49 % (4035682)Time elapsed: 0.069 s % 10.44/2.49 % (4035682)Peak memory usage: 113 MB % 10.44/2.49 % (4035682)Instructions burned: 127 (million) % 10.44/2.49 % (4035686)dis+10_1_si=on:random_seed=4200890187:i=10:ep=R:rtra=on_2991 on theBenchmark for (2991ds/10Mi) % 10.44/2.49 % (4035686)Instruction limit reached! % 10.44/2.49 % (4035686)------------------------------ % 10.44/2.49 % (4035686)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.44/2.49 % (4035686)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.44/2.49 % (4035686)CaDiCaL version: 2.1.3 % 10.44/2.49 % (4035686)Termination reason: Instruction limit % 10.44/2.49 % (4035686)Termination phase: Property scanning % 10.44/2.49 % (4035686)Time elapsed: 0.009 s % 10.44/2.49 % (4035686)Peak memory usage: 85 MB % 10.44/2.49 % (4035686)Instructions burned: 10 (million) % 10.44/2.49 % (4035689)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=259744061: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_2991 on theBenchmark for (2991ds/35Mi) % 10.44/2.49 % (4035688)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=1665478866:i=26:canc=cautious:av=off:rtra=on_2991 on theBenchmark for (2991ds/26Mi) % 12.65/2.93 % (4035691)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=2759525340:i=2:fsr=off:rtra=on:inst=on_2990 on theBenchmark for (2990ds/2Mi) % 12.65/2.93 % (4035691)Instruction limit reached! % 12.65/2.93 % (4035691)------------------------------ % 12.65/2.93 % (4035691)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.65/2.93 % (4035691)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.65/2.93 % (4035691)CaDiCaL version: 2.1.3 % 12.65/2.93 % (4035691)Termination reason: Instruction limit % 12.65/2.93 % (4035691)Termination phase: shuffling % 12.65/2.93 % (4035691)Time elapsed: 0.002 s % 12.65/2.93 % (4035691)Peak memory usage: 85 MB % 12.65/2.93 % (4035691)Instructions burned: 2 (million) % 12.65/2.93 % (4035689)Instruction limit reached! % 12.65/2.93 % (4035689)------------------------------ % 12.65/2.93 % (4035689)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.65/2.93 % (4035689)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.65/2.93 % (4035689)CaDiCaL version: 2.1.3 % 12.65/2.93 % (4035689)Termination reason: Instruction limit % 12.65/2.93 % (4035689)Termination phase: Property scanning % 12.65/2.93 % (4035689)Time elapsed: 0.030 s % 12.65/2.93 % (4035689)Peak memory usage: 86 MB % 12.65/2.93 % (4035689)Instructions burned: 36 (million) % 12.65/2.93 % (4035688)Instruction limit reached! % 12.65/2.93 % (4035688)------------------------------ % 12.65/2.93 % (4035688)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.65/2.93 % (4035688)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.65/2.93 % (4035688)CaDiCaL version: 2.1.3 % 12.65/2.93 % (4035688)Termination reason: Instruction limit % 12.65/2.93 % (4035688)Termination phase: Property scanning % 12.65/2.93 % (4035688)Time elapsed: 0.021 s % 12.65/2.93 % (4035688)Peak memory usage: 86 MB % 12.65/2.93 % (4035688)Instructions burned: 26 (million) % 12.65/2.93 % (4035671)------------------------------ % 12.65/2.93 % (4035671)------------------------------ % 12.65/2.93 % (4035696)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=2616502585:i=370:ep=RS:fsr=off:rtra=on_2989 on theBenchmark for (2989ds/370Mi) % 12.65/2.93 % (4035695)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=3846728851:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2989 on theBenchmark for (2989ds/8Mi) % 12.65/2.93 % (4035695)Instruction limit reached! % 12.65/2.93 % (4035695)------------------------------ % 12.65/2.93 % (4035695)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.65/2.93 % (4035695)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.65/2.93 % (4035695)CaDiCaL version: 2.1.3 % 12.65/2.93 % (4035695)Termination reason: Instruction limit % 12.65/2.93 % (4035695)Termination phase: Property scanning % 12.65/2.93 % (4035695)Time elapsed: 0.008 s % 12.65/2.93 % (4035695)Peak memory usage: 85 MB % 12.65/2.93 % (4035695)Instructions burned: 8 (million) % 12.65/2.93 % (4035698)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=655165475:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2989 on theBenchmark for (2989ds/13Mi) % 12.65/2.93 % (4035698)Instruction limit reached! % 12.65/2.93 % (4035698)------------------------------ % 12.65/2.93 % (4035698)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.65/2.93 % (4035698)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.65/2.93 % (4035698)CaDiCaL version: 2.1.3 % 12.65/2.93 % (4035698)Termination reason: Instruction limit % 12.65/2.93 % (4035698)Termination phase: shuffling % 12.65/2.93 % (4035698)Time elapsed: 0.006 s % 12.65/2.93 % (4035698)Peak memory usage: 85 MB % 12.65/2.93 % (4035698)Instructions burned: 15 (million) % 12.65/2.93 % (4035696)Refutation not found, incomplete strategy % 12.65/2.93 % (4035696)------------------------------ % 12.65/2.93 % (4035696)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.65/2.93 % (4035696)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.65/2.93 % (4035696)CaDiCaL version: 2.1.3 % 12.65/2.93 % (4035696)Termination reason: Refutation not found, incomplete strategy % 12.65/2.93 % (4035696)Time elapsed: 0.079 s % 12.65/2.93 % (4035696)Peak memory usage: 89 MB % 12.65/2.93 % (4035696)Instructions burned: 104 (million) % 12.65/2.93 % (4035703)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=212889166:i=10:rtra=on_2988 on theBenchmark for (2988ds/10Mi) % 16.74/3.32 % (4035702)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=3947708307:i=226:rtra=on:gtg=position:ss=axioms_2988 on theBenchmark for (2988ds/226Mi) % 16.74/3.32 % (4035704)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=2878558431:i=71:rtra=on:gtg=exists_top_2988 on theBenchmark for (2988ds/71Mi) % 16.74/3.32 % (4035705)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=2558553803:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2988 on theBenchmark for (2988ds/75Mi) % 16.74/3.32 % (4035703)Instruction limit reached! % 16.74/3.32 % (4035703)------------------------------ % 16.74/3.32 % (4035703)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.74/3.32 % (4035703)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.74/3.32 % (4035703)CaDiCaL version: 2.1.3 % 16.74/3.32 % (4035703)Termination reason: Instruction limit % 16.74/3.32 % (4035703)Termination phase: Property scanning % 16.74/3.32 % (4035703)Time elapsed: 0.009 s % 16.74/3.32 % (4035703)Peak memory usage: 85 MB % 16.74/3.32 % (4035703)Instructions burned: 10 (million) % 16.74/3.32 % (4035705)Instruction limit reached! % 16.74/3.32 % (4035705)------------------------------ % 16.74/3.32 % (4035705)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.74/3.32 % (4035705)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.74/3.32 % (4035705)CaDiCaL version: 2.1.3 % 16.74/3.32 % (4035705)Termination reason: Instruction limit % 16.74/3.32 % (4035705)Termination phase: Saturation % 16.74/3.32 % (4035705)Time elapsed: 0.051 s % 16.74/3.32 % (4035705)Peak memory usage: 86 MB % 16.74/3.32 % (4035705)Instructions burned: 76 (million) % 16.74/3.32 % (4035708)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=962843526:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2987 on theBenchmark for (2987ds/294Mi) % 16.74/3.32 % (4035702)Refutation not found, incomplete strategy % 16.74/3.32 % (4035702)------------------------------ % 16.74/3.32 % (4035702)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.74/3.32 % (4035702)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.74/3.32 % (4035702)CaDiCaL version: 2.1.3 % 16.74/3.32 % (4035702)Termination reason: Refutation not found, incomplete strategy % 16.74/3.32 % (4035702)Time elapsed: 0.078 s % 16.74/3.32 % (4035702)Peak memory usage: 112 MB % 16.74/3.32 % (4035702)Instructions burned: 65 (million) % 16.74/3.32 % (4035704)Instruction limit reached! % 16.74/3.32 % (4035704)------------------------------ % 16.74/3.32 % (4035704)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.74/3.32 % (4035704)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.74/3.32 % (4035704)CaDiCaL version: 2.1.3 % 16.74/3.32 % (4035704)Termination reason: Instruction limit % 16.74/3.32 % (4035704)Termination phase: Saturation % 16.74/3.32 % (4035704)Time elapsed: 0.079 s % 16.74/3.32 % (4035704)Peak memory usage: 112 MB % 16.74/3.32 % (4035704)Instructions burned: 71 (million) % 16.74/3.32 % (4035710)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=3900839746:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2987 on theBenchmark for (2987ds/130Mi) % 16.74/3.32 % (4035708)Instruction limit reached! % 16.74/3.32 % (4035708)------------------------------ % 16.74/3.32 % (4035708)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.74/3.32 % (4035708)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.74/3.32 % (4035708)CaDiCaL version: 2.1.3 % 16.74/3.32 % (4035708)Termination reason: Instruction limit % 16.74/3.32 % (4035708)Termination phase: Saturation % 16.74/3.32 % (4035708)Time elapsed: 0.113 s % 16.74/3.32 % (4035708)Peak memory usage: 91 MB % 16.74/3.32 % (4035708)Instructions burned: 295 (million) % 16.74/3.32 % (4035717)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=1274067985:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2985 on theBenchmark for (2985ds/40Mi) % 16.74/3.32 % (4035716)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=1379318259:i=131:rtra=on_2985 on theBenchmark for (2985ds/131Mi) % 16.74/3.32 % (4035717)Instruction limit reached! % 16.74/3.32 % (4035717)------------------------------ % 16.74/3.32 % (4035717)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.65/3.63 % (4035717)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.65/3.63 % (4035717)CaDiCaL version: 2.1.3 % 18.65/3.63 % (4035717)Termination reason: Instruction limit % 18.65/3.63 % (4035717)Termination phase: Property scanning % 18.65/3.63 % (4035717)Time elapsed: 0.019 s % 18.65/3.63 % (4035717)Peak memory usage: 86 MB % 18.65/3.63 % (4035717)Instructions burned: 42 (million) % 18.65/3.63 % (4035710)Instruction limit reached! % 18.65/3.63 % (4035710)------------------------------ % 18.65/3.63 % (4035710)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.65/3.63 % (4035710)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.65/3.63 % (4035710)CaDiCaL version: 2.1.3 % 18.65/3.63 % (4035710)Termination reason: Instruction limit % 18.65/3.63 % (4035710)Termination phase: Property scanning % 18.65/3.63 % (4035710)Time elapsed: 0.096 s % 18.65/3.63 % (4035710)Peak memory usage: 88 MB % 18.65/3.63 % (4035710)Instructions burned: 130 (million) % 18.65/3.63 % (4035696)------------------------------ % 18.65/3.63 % (4035696)------------------------------ % 18.65/3.63 % (4035719)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=1145993590:i=307:rtra=on:gtg=exists_top_2985 on theBenchmark for (2985ds/307Mi) % 18.65/3.63 % (4035719)Refutation not found, incomplete strategy % 18.65/3.63 % (4035719)------------------------------ % 18.65/3.63 % (4035719)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.65/3.63 % (4035719)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.65/3.63 % (4035719)CaDiCaL version: 2.1.3 % 18.65/3.63 % (4035719)Termination reason: Refutation not found, incomplete strategy % 18.65/3.63 % (4035719)Time elapsed: 0.062 s % 18.65/3.63 % (4035719)Peak memory usage: 90 MB % 18.65/3.63 % (4035719)Instructions burned: 138 (million) % 18.65/3.63 % (4035716)Instruction limit reached! % 18.65/3.63 % (4035716)------------------------------ % 18.65/3.63 % (4035716)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.65/3.63 % (4035716)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.65/3.63 % (4035716)CaDiCaL version: 2.1.3 % 18.65/3.63 % (4035716)Termination reason: Instruction limit % 18.65/3.63 % (4035716)Termination phase: Saturation % 18.65/3.63 % (4035716)Time elapsed: 0.152 s % 18.65/3.63 % (4035716)Peak memory usage: 130 MB % 18.65/3.63 % (4035716)Instructions burned: 131 (million) % 18.65/3.63 % (4035721)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=2013004521:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2984 on theBenchmark for (2984ds/598Mi) % 18.65/3.63 % (4035725)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=3800043630:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2983 on theBenchmark for (2983ds/259Mi) % 18.65/3.63 % (4035702)------------------------------ % 18.65/3.63 % (4035702)------------------------------ % 18.65/3.63 % (4035725)Refutation not found, incomplete strategy % 18.65/3.63 % (4035725)------------------------------ % 18.65/3.63 % (4035725)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.65/3.63 % (4035725)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.65/3.63 % (4035725)CaDiCaL version: 2.1.3 % 18.65/3.63 % (4035725)Termination reason: Refutation not found, incomplete strategy % 18.65/3.64 % (4035725)Time elapsed: 0.045 s % 18.65/3.64 % (4035725)Peak memory usage: 112 MB % 18.65/3.64 % (4035725)Instructions burned: 68 (million) % 18.65/3.64 % (4035724)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=952541352:i=131:canc=cautious:fsr=off:rtra=on_2983 on theBenchmark for (2983ds/131Mi) % 18.65/3.64 % (4035727)dis+10_1_si=on:random_seed=476502503:s2a=on:i=1000:rtra=on:gtg=exists_all_2982 on theBenchmark for (2982ds/1000Mi) % 18.65/3.64 % (4035724)Instruction limit reached! % 18.65/3.64 % (4035724)------------------------------ % 18.65/3.64 % (4035724)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.65/3.64 % (4035724)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.65/3.64 % (4035724)CaDiCaL version: 2.1.3 % 18.65/3.64 % (4035724)Termination reason: Instruction limit % 18.65/3.64 % (4035724)Termination phase: Saturation % 18.65/3.64 % (4035724)Time elapsed: 0.129 s % 18.65/3.64 % (4035724)Peak memory usage: 113 MB % 18.65/3.64 % (4035724)Instructions burned: 132 (million) % 18.65/3.64 % (4035728)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=182002954:i=383:fsr=off:rtra=on:ev=force_2981 on theBenchmark for (2981ds/383Mi) % 19.00/4.07 % (4035725)------------------------------ % 19.00/4.07 % (4035725)------------------------------ % 19.00/4.07 % (4035731)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=2937863158:i=141:doe=on:rtra=on_2981 on theBenchmark for (2981ds/141Mi) % 19.00/4.07 % (4035719)------------------------------ % 19.00/4.07 % (4035719)------------------------------ % 19.00/4.07 % (4035731)Instruction limit reached! % 19.00/4.07 % (4035731)------------------------------ % 19.00/4.07 % (4035731)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.00/4.07 % (4035731)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.00/4.07 % (4035731)CaDiCaL version: 2.1.3 % 19.00/4.07 % (4035731)Termination reason: Instruction limit % 19.00/4.07 % (4035731)Termination phase: Saturation % 19.00/4.07 % (4035731)Time elapsed: 0.105 s % 19.00/4.07 % (4035731)Peak memory usage: 89 MB % 19.00/4.07 % (4035731)Instructions burned: 141 (million) % 19.00/4.07 % (4035735)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=4177174100:i=65:nm=16:rtra=on_2979 on theBenchmark for (2979ds/65Mi) % 19.00/4.07 % (4035738)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=271647495:i=121:nm=16:rtra=on_2978 on theBenchmark for (2978ds/121Mi) % 19.00/4.07 % (4035735)Instruction limit reached! % 19.00/4.07 % (4035735)------------------------------ % 19.00/4.07 % (4035735)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.00/4.07 % (4035735)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.00/4.07 % (4035735)CaDiCaL version: 2.1.3 % 19.00/4.07 % (4035735)Termination reason: Instruction limit % 19.00/4.07 % (4035735)Termination phase: Saturation % 19.00/4.07 % (4035735)Time elapsed: 0.049 s % 19.00/4.07 % (4035735)Peak memory usage: 88 MB % 19.00/4.07 % (4035735)Instructions burned: 66 (million) % 19.00/4.07 % (4035738)Instruction limit reached! % 19.00/4.07 % (4035738)------------------------------ % 19.00/4.07 % (4035738)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.00/4.07 % (4035738)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.00/4.07 % (4035738)CaDiCaL version: 2.1.3 % 19.00/4.07 % (4035738)Termination reason: Instruction limit % 19.00/4.07 % (4035738)Termination phase: Saturation % 19.00/4.07 % (4035738)Time elapsed: 0.049 s % 19.00/4.07 % (4035738)Peak memory usage: 90 MB % 19.00/4.07 % (4035738)Instructions burned: 123 (million) % 19.00/4.07 % (4035728)Instruction limit reached! % 19.00/4.07 % (4035728)------------------------------ % 19.00/4.07 % (4035728)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.00/4.07 % (4035728)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.00/4.07 % (4035728)CaDiCaL version: 2.1.3 % 19.00/4.07 % (4035728)Termination reason: Instruction limit % 19.00/4.07 % (4035728)Termination phase: Saturation % 19.00/4.07 % (4035728)Time elapsed: 0.287 s % 19.00/4.07 % (4035728)Peak memory usage: 91 MB % 19.00/4.07 % (4035728)Instructions burned: 383 (million) % 19.00/4.07 % (4035721)Instruction limit reached! % 19.00/4.07 % (4035721)------------------------------ % 19.00/4.07 % (4035721)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.00/4.07 % (4035721)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.00/4.07 % (4035721)CaDiCaL version: 2.1.3 % 19.00/4.07 % (4035721)Termination reason: Instruction limit % 19.00/4.07 % (4035721)Termination phase: Saturation % 19.00/4.07 % (4035721)Time elapsed: 0.536 s % 19.00/4.07 % (4035721)Peak memory usage: 138 MB % 19.00/4.07 % (4035721)Instructions burned: 598 (million) % 19.00/4.07 % (4035739)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=3572360938:s2a=on:i=128:s2at=5:ins=3:rtra=on_2978 on theBenchmark for (2978ds/128Mi) % 19.00/4.07 % (4035741)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=2421455306:i=39:ins=3:rtra=on_2977 on theBenchmark for (2977ds/39Mi) % 19.00/4.07 % (4035741)Instruction limit reached! % 19.00/4.07 % (4035741)------------------------------ % 19.00/4.07 % (4035741)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.00/4.07 % (4035741)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.00/4.07 % (4035741)CaDiCaL version: 2.1.3 % 19.00/4.07 % (4035741)Termination reason: Instruction limit % 23.91/4.62 % (4035741)Termination phase: Property scanning % 23.91/4.62 % (4035741)Time elapsed: 0.031 s % 23.91/4.62 % (4035741)Peak memory usage: 86 MB % 23.91/4.62 % (4035741)Instructions burned: 39 (million) % 23.91/4.62 % (4035739)Instruction limit reached! % 23.91/4.62 % (4035739)------------------------------ % 23.91/4.62 % (4035739)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.91/4.62 % (4035739)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.91/4.62 % (4035739)CaDiCaL version: 2.1.3 % 23.91/4.62 % (4035739)Termination reason: Instruction limit % 23.91/4.62 % (4035739)Termination phase: Saturation % 23.91/4.62 % (4035739)Time elapsed: 0.078 s % 23.91/4.62 % (4035739)Peak memory usage: 90 MB % 23.91/4.62 % (4035739)Instructions burned: 128 (million) % 23.91/4.62 % (4035746)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=2617233502:i=329:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2976 on theBenchmark for (2976ds/329Mi) % 23.91/4.62 % (4035748)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=1674240202:thitd=on:i=215:nm=0:rtra=on:ev=force_2976 on theBenchmark for (2976ds/215Mi) % 23.91/4.62 % (4035745)dis+1010_1_to=kbo:si=on:random_seed=2987631341:i=175:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2976 on theBenchmark for (2976ds/175Mi) % 23.91/4.62 % (4035747)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=6247160:s2a=on:i=483:doe=on:nm=32:rtra=on_2976 on theBenchmark for (2976ds/483Mi) % 23.91/4.62 % (4035746)Instruction limit reached! % 23.91/4.62 % (4035746)------------------------------ % 23.91/4.62 % (4035746)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.91/4.62 % (4035746)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.91/4.62 % (4035746)CaDiCaL version: 2.1.3 % 23.91/4.62 % (4035746)Termination reason: Instruction limit % 23.91/4.62 % (4035746)Termination phase: Saturation % 23.91/4.62 % (4035746)Time elapsed: 0.150 s % 23.91/4.62 % (4035746)Peak memory usage: 118 MB % 23.91/4.62 % (4035746)Instructions burned: 332 (million) % 23.91/4.62 % (4035727)Instruction limit reached! % 23.91/4.62 % (4035727)------------------------------ % 23.91/4.62 % (4035727)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.91/4.62 % (4035727)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.91/4.62 % (4035727)CaDiCaL version: 2.1.3 % 23.91/4.62 % (4035727)Termination reason: Instruction limit % 23.91/4.62 % (4035727)Termination phase: Saturation % 23.91/4.62 % (4035727)Time elapsed: 0.712 s % 23.91/4.62 % (4035727)Peak memory usage: 92 MB % 23.91/4.62 % (4035727)Instructions burned: 1001 (million) % 23.91/4.62 % (4035745)Instruction limit reached! % 23.91/4.62 % (4035745)------------------------------ % 23.91/4.62 % (4035745)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.91/4.62 % (4035745)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.91/4.62 % (4035745)CaDiCaL version: 2.1.3 % 23.91/4.62 % (4035745)Termination reason: Instruction limit % 23.91/4.62 % (4035745)Termination phase: Saturation % 23.91/4.62 % (4035745)Time elapsed: 0.138 s % 23.91/4.62 % (4035745)Peak memory usage: 91 MB % 23.91/4.62 % (4035745)Instructions burned: 176 (million) % 23.91/4.62 % (4035748)Instruction limit reached! % 23.91/4.62 % (4035748)------------------------------ % 23.91/4.62 % (4035748)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.91/4.62 % (4035748)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.91/4.62 % (4035748)CaDiCaL version: 2.1.3 % 23.91/4.62 % (4035748)Termination reason: Instruction limit % 23.91/4.62 % (4035748)Termination phase: Saturation % 23.91/4.62 % (4035748)Time elapsed: 0.185 s % 23.91/4.62 % (4035748)Peak memory usage: 131 MB % 23.91/4.62 % (4035748)Instructions burned: 217 (million) % 23.91/4.62 % (4035752)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=4268954935:st=2:i=295:rtra=on:ss=axioms_2974 on theBenchmark for (2974ds/295Mi) % 23.91/4.62 % (4035751)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=119963332:i=349:rtra=on_2975 on theBenchmark for (2975ds/349Mi) % 23.91/4.62 % (4035752)Refutation not found, incomplete strategy % 23.91/4.62 % (4035752)------------------------------ % 23.91/4.62 % (4035752)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.91/4.62 % (4035752)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.33/4.98 % (4035752)CaDiCaL version: 2.1.3 % 26.33/4.98 % (4035752)Termination reason: Refutation not found, incomplete strategy % 26.33/4.98 % (4035752)Time elapsed: 0.045 s % 26.33/4.98 % (4035752)Peak memory usage: 88 MB % 26.33/4.98 % (4035752)Instructions burned: 63 (million) % 26.33/4.98 % (4035758)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=2554669092:i=328:kws=inv_frequency:nm=20:rtra=on_2973 on theBenchmark for (2973ds/328Mi) % 26.33/4.98 % (4035759)dis+1010_1_to=lpo:sil=128000:sas=z3:si=on:nwc=5:random_seed=678919503:i=281:gtgl=2:rtra=on:gtg=all_2972 on theBenchmark for (2972ds/281Mi) % 26.33/4.98 % (4035760)lrs+1010_1_to=kbo:sil=128000:si=on:sos=on:urr=on:uwa=alasca_main:random_seed=1559836388:i=484:doe=on:nm=0:av=off:rtra=on:ss=axioms_2972 on theBenchmark for (2972ds/484Mi) % 26.33/4.98 % (4035761)lrs+21_1_to=kbo:sil=128000:thi=neg_eq:si=on:random_seed=1169369383:i=321:canc=force:rtra=on:tac=axiom:ss=axioms:ev=force_2972 on theBenchmark for (2972ds/321Mi) % 26.33/4.98 % (4035760)Refutation not found, incomplete strategy % 26.33/4.98 % (4035760)------------------------------ % 26.33/4.98 % (4035760)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.33/4.98 % (4035760)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.33/4.98 % (4035760)CaDiCaL version: 2.1.3 % 26.33/4.98 % (4035760)Termination reason: Refutation not found, incomplete strategy % 26.33/4.98 % (4035760)Time elapsed: 0.042 s % 26.33/4.98 % (4035760)Peak memory usage: 88 MB % 26.33/4.98 % (4035760)Instructions burned: 61 (million) % 26.33/4.98 % (4035758)Instruction limit reached! % 26.33/4.98 % (4035758)------------------------------ % 26.33/4.98 % (4035758)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.33/4.98 % (4035758)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.33/4.98 % (4035758)CaDiCaL version: 2.1.3 % 26.33/4.98 % (4035758)Termination reason: Instruction limit % 26.33/4.98 % (4035758)Termination phase: Saturation % 26.33/4.98 % (4035758)Time elapsed: 0.153 s % 26.33/4.98 % (4035758)Peak memory usage: 115 MB % 26.33/4.98 % (4035758)Instructions burned: 330 (million) % 26.33/4.98 % (4035751)Instruction limit reached! % 26.33/4.98 % (4035751)------------------------------ % 26.33/4.98 % (4035751)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.33/4.98 % (4035751)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.33/4.98 % (4035751)CaDiCaL version: 2.1.3 % 26.33/4.98 % (4035751)Termination reason: Instruction limit % 26.33/4.98 % (4035751)Termination phase: Saturation % 26.33/4.98 % (4035751)Time elapsed: 0.302 s % 26.33/4.98 % (4035751)Peak memory usage: 117 MB % 26.33/4.98 % (4035751)Instructions burned: 349 (million) % 26.33/4.98 % (4035747)Instruction limit reached! % 26.33/4.98 % (4035747)------------------------------ % 26.33/4.98 % (4035747)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.33/4.98 % (4035747)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.33/4.98 % (4035747)CaDiCaL version: 2.1.3 % 26.33/4.98 % (4035747)Termination reason: Instruction limit % 26.33/4.98 % (4035747)Termination phase: Saturation % 26.33/4.98 % (4035747)Time elapsed: 0.444 s % 26.33/4.98 % (4035747)Peak memory usage: 137 MB % 26.33/4.98 % (4035747)Instructions burned: 484 (million) % 26.33/4.98 % (4035761)Refutation not found, incomplete strategy % 26.33/4.98 % (4035761)------------------------------ % 26.33/4.98 % (4035761)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.33/4.98 % (4035761)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.33/4.98 % (4035761)CaDiCaL version: 2.1.3 % 26.33/4.98 % (4035761)Termination reason: Refutation not found, incomplete strategy % 26.33/4.98 % (4035761)Time elapsed: 0.078 s % 26.33/4.98 % (4035761)Peak memory usage: 112 MB % 26.33/4.98 % (4035761)Instructions burned: 66 (million) % 26.33/4.98 % (4035752)------------------------------ % 26.33/4.98 % (4035752)------------------------------ % 26.33/4.98 % (4035759)Instruction limit reached! % 26.33/4.98 % (4035759)------------------------------ % 26.33/4.98 % (4035759)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.33/4.98 % (4035759)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.33/4.98 % (4035759)CaDiCaL version: 2.1.3 % 26.33/4.98 % (4035759)Termination reason: Instruction limit % 26.33/4.98 % (4035759)Termination phase: Saturation % 26.33/4.98 % (4035759)Time elapsed: 0.245 s % 26.33/4.98 % (4035759)Peak memory usage: 113 MB % 31.24/5.50 % (4035759)Instructions burned: 282 (million) % 31.24/5.50 % (4035768)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=2658627467:i=416:rtra=on:gtg=position:ss=axioms_2969 on theBenchmark for (2969ds/416Mi) % 31.24/5.50 % (4035770)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=1499037115:avsq=on:i=276:avsqr=1,2:rtra=on_2969 on theBenchmark for (2969ds/276Mi) % 31.24/5.50 % (4035769)lrs+1010_1_to=kbo:tgt=ground:fde=unused:sas=z3:si=on:sp=unary_frequency:gve=force:spb=goal:tha=off:random_seed=3930577131:i=471:thf=on:kws=precedence:rtra=on_2969 on theBenchmark for (2969ds/471Mi) % 31.24/5.50 % (4035768)Refutation not found, incomplete strategy % 31.24/5.50 % (4035768)------------------------------ % 31.24/5.50 % (4035768)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.24/5.50 % (4035768)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.24/5.50 % (4035768)CaDiCaL version: 2.1.3 % 31.24/5.50 % (4035768)Termination reason: Refutation not found, incomplete strategy % 31.24/5.50 % (4035768)Time elapsed: 0.077 s % 31.24/5.50 % (4035768)Peak memory usage: 111 MB % 31.24/5.50 % (4035768)Instructions burned: 65 (million) % 31.24/5.50 % (4035760)------------------------------ % 31.24/5.50 % (4035760)------------------------------ % 31.24/5.50 % (4035770)Instruction limit reached! % 31.24/5.50 % (4035770)------------------------------ % 31.24/5.50 % (4035770)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.24/5.50 % (4035770)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.24/5.50 % (4035770)CaDiCaL version: 2.1.3 % 31.24/5.50 % (4035770)Termination reason: Instruction limit % 31.24/5.50 % (4035770)Termination phase: Saturation % 31.24/5.50 % (4035770)Time elapsed: 0.143 s % 31.24/5.50 % (4035770)Peak memory usage: 131 MB % 31.24/5.50 % (4035770)Instructions burned: 276 (million) % 31.24/5.50 % (4035772)lrs+1010_2_to=kbo:sil=128000:tgt=ground:fde=unused:sas=z3:si=on:uwa=off:tha=off:nwc=1:random_seed=2774971489:i=375:kws=inv_arity_squared:rtra=on_2967 on theBenchmark for (2967ds/375Mi) % 31.24/5.50 % (4035773)lrs+10_1_to=kbo:sil=128000:tgt=full:sas=z3:si=on:uwa=func_ext:slsqc=1:flr=on:slsq=on:random_seed=2200731423:i=387:bd=preordered:rtra=on:ss=axioms:sgt=8_2967 on theBenchmark for (2967ds/387Mi) % 31.24/5.50 % (4035761)------------------------------ % 31.24/5.50 % (4035761)------------------------------ % 31.24/5.50 % (4035773)Refutation not found, incomplete strategy % 31.24/5.50 % (4035773)------------------------------ % 31.24/5.50 % (4035773)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.24/5.50 % (4035773)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.24/5.50 % (4035773)CaDiCaL version: 2.1.3 % 31.24/5.50 % (4035773)Termination reason: Refutation not found, incomplete strategy % 31.24/5.50 % (4035773)Time elapsed: 0.081 s % 31.24/5.50 % (4035773)Peak memory usage: 112 MB % 31.24/5.50 % (4035773)Instructions burned: 69 (million) % 31.24/5.50 % (4035769)Instruction limit reached! % 31.24/5.50 % (4035769)------------------------------ % 31.24/5.50 % (4035769)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.24/5.50 % (4035769)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.24/5.50 % (4035769)CaDiCaL version: 2.1.3 % 31.24/5.50 % (4035769)Termination reason: Instruction limit % 31.24/5.50 % (4035769)Termination phase: Saturation % 31.24/5.50 % (4035769)Time elapsed: 0.338 s % 31.24/5.50 % (4035769)Peak memory usage: 113 MB % 31.24/5.50 % (4035769)Instructions burned: 471 (million) % 31.24/5.50 % (4035778)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=1172658592:i=334:rtra=on_2965 on theBenchmark for (2965ds/334Mi) % 31.24/5.50 % (4035777)lrs+10_1_to=kbo:sil=128000:fde=none:si=on:norm_ineq=on:urr=on:nwc=0.5:random_seed=3565216176:i=513:kws=frequency:bd=all:rtra=on:gtg=exists_all:ss=axioms:sgt=4_2965 on theBenchmark for (2965ds/513Mi) % 31.24/5.50 % (4035768)------------------------------ % 31.24/5.50 % (4035768)------------------------------ % 31.24/5.50 % (4035782)lrs+1010_1_to=kbo:sil=64000:sas=cadical:si=on:sos=on:bce=on:random_seed=1158774703:i=359:rtra=on:gtg=exists_top:ss=axioms_2965 on theBenchmark for (2965ds/359Mi) % 31.24/5.50 % (4035772)Instruction limit reached! % 31.24/5.50 % (4035772)------------------------------ % 31.24/5.50 % (4035772)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 37.57/6.17 % (4035772)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.57/6.17 % (4035772)CaDiCaL version: 2.1.3 % 37.57/6.17 % (4035772)Termination reason: Instruction limit % 37.57/6.17 % (4035772)Termination phase: Saturation % 37.57/6.17 % (4035772)Time elapsed: 0.325 s % 37.57/6.17 % (4035772)Peak memory usage: 118 MB % 37.57/6.17 % (4035772)Instructions burned: 375 (million) % 37.57/6.17 % (4035778)Instruction limit reached! % 37.57/6.17 % (4035778)------------------------------ % 37.57/6.17 % (4035778)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 37.57/6.17 % (4035778)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.57/6.17 % (4035778)CaDiCaL version: 2.1.3 % 37.57/6.17 % (4035778)Termination reason: Instruction limit % 37.57/6.17 % (4035778)Termination phase: Saturation % 37.57/6.17 % (4035778)Time elapsed: 0.173 s % 37.57/6.17 % (4035778)Peak memory usage: 134 MB % 37.57/6.17 % (4035778)Instructions burned: 336 (million) % 37.57/6.17 % (4035782)Refutation not found, incomplete strategy % 37.57/6.17 % (4035782)------------------------------ % 37.57/6.17 % (4035782)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 37.57/6.17 % (4035782)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.57/6.17 % (4035782)CaDiCaL version: 2.1.3 % 37.57/6.17 % (4035782)Termination reason: Refutation not found, incomplete strategy % 37.57/6.17 % (4035782)Time elapsed: 0.052 s % 37.57/6.17 % (4035782)Peak memory usage: 89 MB % 37.57/6.17 % (4035782)Instructions burned: 76 (million) % 37.57/6.17 % (4035784)dis+1010_1_to=lpo:sil=128000:thi=all:fde=unused:si=on:sp=reverse_arity:tha=off:random_seed=2414740305:i=341:gtgl=2:rtra=on:gtg=exists_sym:ev=force:fsd=on:fsdmm=1_2963 on theBenchmark for (2963ds/341Mi) % 37.57/6.17 % (4035786)lrs-2_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_max:tha=off:random_seed=2898738892:st=1.5:i=261:sd=1:kws=precedence:rtra=on:ss=axioms_2962 on theBenchmark for (2962ds/261Mi) % 37.57/6.17 % (4035773)------------------------------ % 37.57/6.17 % (4035773)------------------------------ % 37.57/6.17 % (4035786)Refutation not found, incomplete strategy % 37.57/6.17 % (4035786)------------------------------ % 37.57/6.17 % (4035786)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 37.57/6.17 % (4035786)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.57/6.17 % (4035786)CaDiCaL version: 2.1.3 % 37.57/6.17 % (4035786)Termination reason: Refutation not found, incomplete strategy % 37.57/6.17 % (4035786)Time elapsed: 0.057 s % 37.57/6.17 % (4035786)Peak memory usage: 111 MB % 37.57/6.17 % (4035786)Instructions burned: 59 (million) % 37.57/6.17 % (4035789)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=1291600612:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2961 on theBenchmark for (2961ds/273Mi) % 37.57/6.17 % (4035788)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=1105273942:s2pl=no:i=235:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2962 on theBenchmark for (2962ds/235Mi) % 37.57/6.17 % (4035777)Instruction limit reached! % 37.57/6.17 % (4035777)------------------------------ % 37.57/6.17 % (4035777)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 37.57/6.17 % (4035777)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.57/6.17 % (4035777)CaDiCaL version: 2.1.3 % 37.57/6.17 % (4035777)Termination reason: Instruction limit % 37.57/6.17 % (4035777)Termination phase: Saturation % 37.57/6.17 % (4035777)Time elapsed: 0.378 s % 37.57/6.17 % (4035777)Peak memory usage: 90 MB % 37.57/6.17 % (4035777)Instructions burned: 514 (million) % 37.57/6.17 % (4035789)Instruction limit reached! % 37.57/6.17 % (4035789)------------------------------ % 37.57/6.17 % (4035789)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 37.57/6.17 % (4035789)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.57/6.17 % (4035789)CaDiCaL version: 2.1.3 % 37.57/6.17 % (4035789)Termination reason: Instruction limit % 37.57/6.17 % (4035789)Termination phase: Saturation % 37.57/6.17 % (4035789)Time elapsed: 0.109 s % 37.57/6.17 % (4035789)Peak memory usage: 92 MB % 37.57/6.17 % (4035789)Instructions burned: 274 (million) % 37.57/6.17 % (4035788)Refutation not found, incomplete strategy % 37.57/6.17 % (4035788)------------------------------ % 37.57/6.17 % (4035788)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 40.55/6.83 % (4035788)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.55/6.83 % (4035788)CaDiCaL version: 2.1.3 % 40.55/6.83 % (4035788)Termination reason: Refutation not found, incomplete strategy % 40.55/6.83 % (4035788)Time elapsed: 0.080 s % 40.55/6.83 % (4035788)Peak memory usage: 112 MB % 40.55/6.83 % (4035788)Instructions burned: 68 (million) % 40.55/6.83 % (4035784)Instruction limit reached! % 40.55/6.83 % (4035784)------------------------------ % 40.55/6.83 % (4035784)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 40.55/6.83 % (4035784)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.55/6.83 % (4035784)CaDiCaL version: 2.1.3 % 40.55/6.83 % (4035784)Termination reason: Instruction limit % 40.55/6.83 % (4035784)Termination phase: Saturation % 40.55/6.83 % (4035784)Time elapsed: 0.283 s % 40.55/6.83 % (4035784)Peak memory usage: 119 MB % 40.55/6.83 % (4035784)Instructions burned: 341 (million) % 40.55/6.83 % (4035782)------------------------------ % 40.55/6.83 % (4035782)------------------------------ % 40.55/6.83 % (4035792)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=1856245737:i=146:doe=on:rtra=on_2960 on theBenchmark for (2960ds/146Mi) % 40.55/6.83 % (4035796)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=1125792761:avsq=on:i=276:avsqr=1,2:rtra=on_2958 on theBenchmark for (2958ds/276Mi) % 40.55/6.83 % (4035792)Instruction limit reached! % 40.55/6.83 % (4035792)------------------------------ % 40.55/6.83 % (4035792)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 40.55/6.83 % (4035792)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.55/6.83 % (4035792)CaDiCaL version: 2.1.3 % 40.55/6.83 % (4035792)Termination reason: Instruction limit % 40.55/6.83 % (4035792)Termination phase: Saturation % 40.55/6.83 % (4035792)Time elapsed: 0.111 s % 40.55/6.83 % (4035792)Peak memory usage: 90 MB % 40.55/6.83 % (4035792)Instructions burned: 147 (million) % 40.55/6.83 % (4035795)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=3453465140:i=4428:doe=on:fsr=off:rtra=on_2959 on theBenchmark for (2959ds/4428Mi) % 40.55/6.83 % (4035786)------------------------------ % 40.55/6.83 % (4035786)------------------------------ % 40.55/6.83 % (4035799)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=302084407:i=655:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2957 on theBenchmark for (2957ds/655Mi) % 40.55/6.83 % (4035797)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=668705966:i=1052:rtra=on_2958 on theBenchmark for (2958ds/1052Mi) % 40.55/6.83 % (4035796)Instruction limit reached! % 40.55/6.83 % (4035796)------------------------------ % 40.55/6.83 % (4035796)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 40.55/6.83 % (4035796)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.55/6.83 % (4035796)CaDiCaL version: 2.1.3 % 40.55/6.83 % (4035796)Termination reason: Instruction limit % 40.55/6.83 % (4035796)Termination phase: Saturation % 40.55/6.83 % (4035796)Time elapsed: 0.141 s % 40.55/6.83 % (4035796)Peak memory usage: 130 MB % 40.55/6.83 % (4035796)Instructions burned: 278 (million) % 40.55/6.83 % (4035788)------------------------------ % 40.55/6.83 % (4035788)------------------------------ % 40.55/6.83 % (4035802)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=2382289950:st=5:i=1054:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2956 on theBenchmark for (2956ds/1054Mi) % 40.55/6.83 % (4035802)Refutation not found, incomplete strategy % 40.55/6.83 % (4035802)------------------------------ % 40.55/6.83 % (4035802)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 40.55/6.83 % (4035802)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.55/6.83 % (4035802)CaDiCaL version: 2.1.3 % 40.55/6.83 % (4035802)Termination reason: Refutation not found, incomplete strategy % 40.55/6.83 % (4035802)Time elapsed: 0.032 s % 40.55/6.83 % (4035802)Peak memory usage: 88 MB % 40.55/6.83 % (4035802)Instructions burned: 48 (million) % 40.55/6.83 % (4035803)lrs-1002_1_to=kbo:sas=z3:si=on:norm_ineq=on:sos=on:tha=some:random_seed=3037281756:i=107:rtra=on_2956 on theBenchmark for (2956ds/107Mi) % 40.55/6.83 % (4035806)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=3415486862:s2a=on:i=450:doe=on:nm=32:rtra=on_2955 on theBenchmark for (2955ds/450Mi) % 45.18/7.36 % (4035803)Instruction limit reached! % 45.18/7.36 % (4035803)------------------------------ % 45.18/7.36 % (4035803)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 45.18/7.36 % (4035803)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.18/7.36 % (4035803)CaDiCaL version: 2.1.3 % 45.18/7.36 % (4035803)Termination reason: Instruction limit % 45.18/7.36 % (4035803)Termination phase: Saturation % 45.18/7.36 % (4035803)Time elapsed: 0.083 s % 45.18/7.36 % (4035803)Peak memory usage: 89 MB % 45.18/7.36 % (4035803)Instructions burned: 108 (million) % 45.18/7.36 % (4035807)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 % 45.18/7.36 % (4035807)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=4058935927:i=1090:aac=none:nm=0:rtra=on:rawr=on_2954 on theBenchmark for (2954ds/1090Mi) % 45.18/7.36 % (4035806)Instruction limit reached! % 45.18/7.36 % (4035806)------------------------------ % 45.18/7.36 % (4035806)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 45.18/7.36 % (4035806)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.18/7.36 % (4035806)CaDiCaL version: 2.1.3 % 45.18/7.36 % (4035806)Termination reason: Instruction limit % 45.18/7.36 % (4035806)Termination phase: Saturation % 45.18/7.36 % (4035806)Time elapsed: 0.222 s % 45.18/7.36 % (4035806)Peak memory usage: 137 MB % 45.18/7.36 % (4035806)Instructions burned: 450 (million) % 45.18/7.36 % (4035811)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=65606830:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2952 on theBenchmark for (2952ds/130Mi) % 45.18/7.36 % (4035811)Instruction limit reached! % 45.18/7.36 % (4035811)------------------------------ % 45.18/7.36 % (4035811)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 45.18/7.36 % (4035811)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.18/7.36 % (4035811)CaDiCaL version: 2.1.3 % 45.18/7.36 % (4035811)Termination reason: Instruction limit % 45.18/7.36 % (4035811)Termination phase: Saturation % 45.18/7.36 % (4035811)Time elapsed: 0.058 s % 45.18/7.36 % (4035811)Peak memory usage: 88 MB % 45.18/7.36 % (4035811)Instructions burned: 132 (million) % 45.18/7.36 % (4035799)Instruction limit reached! % 45.18/7.36 % (4035799)------------------------------ % 45.18/7.36 % (4035799)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 45.18/7.36 % (4035799)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.18/7.36 % (4035799)CaDiCaL version: 2.1.3 % 45.18/7.36 % (4035799)Termination reason: Instruction limit % 45.18/7.36 % (4035799)Termination phase: Saturation % 45.18/7.36 % (4035799)Time elapsed: 0.559 s % 45.18/7.36 % (4035799)Peak memory usage: 100 MB % 45.18/7.36 % (4035799)Instructions burned: 655 (million) % 45.18/7.36 % (4035802)------------------------------ % 45.18/7.36 % (4035802)------------------------------ % 45.18/7.36 % (4035797)Instruction limit reached! % 45.18/7.36 % (4035797)------------------------------ % 45.18/7.36 % (4035797)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 45.18/7.36 % (4035797)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.18/7.36 % (4035797)CaDiCaL version: 2.1.3 % 45.18/7.36 % (4035797)Termination reason: Instruction limit % 45.18/7.36 % (4035797)Termination phase: Saturation % 45.18/7.36 % (4035797)Time elapsed: 0.713 s % 45.18/7.36 % (4035797)Peak memory usage: 91 MB % 45.18/7.36 % (4035797)Instructions burned: 1053 (million) % 45.18/7.36 % (4035813)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=2915974779:i=312:kws=inv_frequency:nm=20:rtra=on_2951 on theBenchmark for (2951ds/312Mi) % 45.18/7.36 % (4035816)ott+10_1_to=kbo:sil=64000:si=on:sp=reverse_frequency:sos=on:random_seed=293734737:i=491:doe=on:rtra=on:gtg=position_2950 on theBenchmark for (2950ds/491Mi) % 45.18/7.36 % (4035817)ott+1011_4:1_to=lpo:sil=64000:si=on:spb=intro:random_seed=1889024952:s2a=on:i=835:s2at=2:rtra=on_2949 on theBenchmark for (2949ds/835Mi) % 45.18/7.36 % (4035818)ott+1011_2_to=lpo:sil=128000:si=on:sos=on:random_seed=1755883898:i=307:bd=preordered:av=off:rtra=on:ev=cautious_2949 on theBenchmark for (2949ds/307Mi) % 45.18/7.36 % (4035816)Refutation not found, incomplete strategy % 45.18/7.36 % (4035816)------------------------------ % 45.18/7.36 % (4035816)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 51.49/8.18 % (4035816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 51.49/8.18 % (4035816)CaDiCaL version: 2.1.3 % 51.49/8.18 % (4035816)Termination reason: Refutation not found, incomplete strategy % 51.49/8.18 % (4035816)Time elapsed: 0.156 s % 51.49/8.18 % (4035816)Peak memory usage: 91 MB % 51.49/8.18 % (4035816)Instructions burned: 175 (million) % 51.49/8.18 % (4035813)Instruction limit reached! % 51.49/8.18 % (4035813)------------------------------ % 51.49/8.18 % (4035813)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 51.49/8.18 % (4035813)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 51.49/8.18 % (4035813)CaDiCaL version: 2.1.3 % 51.49/8.18 % (4035813)Termination reason: Instruction limit % 51.49/8.18 % (4035813)Termination phase: Saturation % 51.49/8.18 % (4035813)Time elapsed: 0.253 s % 51.49/8.18 % (4035813)Peak memory usage: 113 MB % 51.49/8.18 % (4035813)Instructions burned: 312 (million) % 51.49/8.18 % (4035819)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=3380626404:i=776:doe=on:rtra=on_2948 on theBenchmark for (2948ds/776Mi) % 51.49/8.18 % (4035818)Refutation not found, incomplete strategy % 51.49/8.18 % (4035818)------------------------------ % 51.49/8.18 % (4035818)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 51.49/8.18 % (4035818)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 51.49/8.18 % (4035818)CaDiCaL version: 2.1.3 % 51.49/8.18 % (4035818)Termination reason: Refutation not found, incomplete strategy % 51.49/8.18 % (4035818)Time elapsed: 0.151 s % 51.49/8.18 % (4035818)Peak memory usage: 95 MB % 51.49/8.18 % (4035818)Instructions burned: 247 (million) % 51.49/8.18 % (4035817)Instruction limit reached! % 51.49/8.18 % (4035817)------------------------------ % 51.49/8.18 % (4035817)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 51.49/8.18 % (4035817)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 51.49/8.18 % (4035817)CaDiCaL version: 2.1.3 % 51.49/8.18 % (4035817)Termination reason: Instruction limit % 51.49/8.18 % (4035817)Termination phase: Saturation % 51.49/8.18 % (4035817)Time elapsed: 0.312 s % 51.49/8.18 % (4035817)Peak memory usage: 90 MB % 51.49/8.18 % (4035817)Instructions burned: 835 (million) % 51.49/8.18 % (4035826)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=1065126718:s2a=on:i=646:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2945 on theBenchmark for (2945ds/646Mi) % 51.49/8.18 % (4035807)Instruction limit reached! % 51.49/8.18 % (4035807)------------------------------ % 51.49/8.18 % (4035807)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 51.49/8.18 % (4035807)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 51.49/8.18 % (4035807)CaDiCaL version: 2.1.3 % 51.49/8.18 % (4035807)Termination reason: Instruction limit % 51.49/8.18 % (4035807)Termination phase: Saturation % 51.49/8.18 % (4035807)Time elapsed: 0.842 s % 51.49/8.18 % (4035807)Peak memory usage: 120 MB % 51.49/8.18 % (4035807)Instructions burned: 1091 (million) % 51.49/8.18 % (4035816)------------------------------ % 51.49/8.18 % (4035816)------------------------------ % 51.49/8.18 % (4035829)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=1633053390:thitd=on:cond=fast:i=784:nm=30:rtra=on:gtg=all:tac=axiom_2944 on theBenchmark for (2944ds/784Mi) % 51.49/8.18 % (4035818)------------------------------ % 51.49/8.18 % (4035818)------------------------------ % 51.49/8.18 % (4035831)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=1126128502:thitd=on:s2a=on:i=1131:add=on:canc=force:bd=all:rtra=on:tac=axiom:ev=off_2943 on theBenchmark for (2943ds/1131Mi) % 51.49/8.18 % (4035833)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=1228369786:s2pl=no:i=246:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2942 on theBenchmark for (2942ds/246Mi) % 51.49/8.18 % (4035833)Refutation not found, incomplete strategy % 51.49/8.18 % (4035833)------------------------------ % 51.49/8.18 % (4035833)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 51.49/8.18 % (4035833)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 51.49/8.18 % (4035833)CaDiCaL version: 2.1.3 % 51.49/8.18 % (4035833)Termination reason: Refutation not found, incomplete strategy % 58.73/9.70 % (4035833)Time elapsed: 0.053 s % 58.73/9.70 % (4035833)Peak memory usage: 112 MB % 58.73/9.70 % (4035833)Instructions burned: 68 (million) % 58.73/9.70 % (4035819)Instruction limit reached! % 58.73/9.70 % (4035819)------------------------------ % 58.73/9.70 % (4035819)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 58.73/9.70 % (4035819)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 58.73/9.70 % (4035819)CaDiCaL version: 2.1.3 % 58.73/9.70 % (4035819)Termination reason: Instruction limit % 58.73/9.70 % (4035819)Termination phase: Saturation % 58.73/9.70 % (4035819)Time elapsed: 0.585 s % 58.73/9.70 % (4035819)Peak memory usage: 114 MB % 58.73/9.70 % (4035819)Instructions burned: 777 (million) % 58.73/9.70 % (4035829)Instruction limit reached! % 58.73/9.70 % (4035829)------------------------------ % 58.73/9.70 % (4035829)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 58.73/9.70 % (4035829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 58.73/9.70 % (4035829)CaDiCaL version: 2.1.3 % 58.73/9.70 % (4035829)Termination reason: Instruction limit % 58.73/9.70 % (4035829)Termination phase: Saturation % 58.73/9.70 % (4035829)Time elapsed: 0.310 s % 58.73/9.70 % (4035829)Peak memory usage: 114 MB % 58.73/9.70 % (4035829)Instructions burned: 784 (million) % 58.73/9.70 % (4035834)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=2022365037:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2941 on theBenchmark for (2941ds/775Mi) % 58.73/9.70 % (4035834)Refutation not found, incomplete strategy % 58.73/9.70 % (4035834)------------------------------ % 58.73/9.70 % (4035834)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 58.73/9.70 % (4035834)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 58.73/9.70 % (4035834)CaDiCaL version: 2.1.3 % 58.73/9.70 % (4035834)Termination reason: Refutation not found, incomplete strategy % 58.73/9.70 % (4035834)Time elapsed: 0.045 s % 58.73/9.70 % (4035834)Peak memory usage: 88 MB % 58.73/9.70 % (4035834)Instructions burned: 66 (million) % 58.73/9.70 % (4035826)Instruction limit reached! % 58.73/9.70 % (4035826)------------------------------ % 58.73/9.70 % (4035826)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 58.73/9.70 % (4035826)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 58.73/9.70 % (4035826)CaDiCaL version: 2.1.3 % 58.73/9.70 % (4035826)Termination reason: Instruction limit % 58.73/9.70 % (4035826)Termination phase: Saturation % 58.73/9.70 % (4035826)Time elapsed: 0.580 s % 58.73/9.70 % (4035826)Peak memory usage: 137 MB % 58.73/9.70 % (4035826)Instructions burned: 646 (million) % 58.73/9.70 % (4035838)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=3017689242:i=102:nm=16:rtra=on_2939 on theBenchmark for (2939ds/102Mi) % 58.73/9.70 % (4035838)Instruction limit reached! % 58.73/9.70 % (4035838)------------------------------ % 58.73/9.70 % (4035838)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 58.73/9.70 % (4035838)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 58.73/9.70 % (4035838)CaDiCaL version: 2.1.3 % 58.73/9.70 % (4035838)Termination reason: Instruction limit % 58.73/9.70 % (4035838)Termination phase: Saturation % 58.73/9.70 % (4035838)Time elapsed: 0.039 s % 58.73/9.70 % (4035838)Peak memory usage: 88 MB % 58.73/9.70 % (4035838)Instructions burned: 103 (million) % 58.73/9.70 % (4035837)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=1815070102:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2939 on theBenchmark for (2939ds/273Mi) % 58.73/9.70 % (4035833)------------------------------ % 58.73/9.70 % (4035833)------------------------------ % 58.73/9.70 % (4035840)lrs+10_1_to=lpo:sil=128000:si=on:bsr=unit_only:tha=off:random_seed=3696470674:avsq=on:s2a=on:i=1094:s2at=5:avsqr=4463,131072:rtra=on_2937 on theBenchmark for (2937ds/1094Mi) % 58.73/9.70 % (4035842)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=3531231317:i=6400:doe=on:fsr=off:rtra=on_2937 on theBenchmark for (2937ds/6400Mi) % 58.73/9.70 % (4035837)Instruction limit reached! % 58.73/9.70 % (4035837)------------------------------ % 58.73/9.70 % (4035837)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 58.73/9.70 % (4035837)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 58.73/9.70 % (4035837)CaDiCaL version: 2.1.3 % 58.73/9.70 % (4035837)Termination reason: Instruction limit % 73.23/11.22 % (4035837)Termination phase: Saturation % 73.23/11.22 % (4035837)Time elapsed: 0.207 s % 73.23/11.22 % (4035837)Peak memory usage: 91 MB % 73.23/11.22 % (4035837)Instructions burned: 273 (million) % 73.23/11.22 % (4035844)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=1485420863:i=868:doe=on:nm=0:rtra=on:gtg=exists_sym_2936 on theBenchmark for (2936ds/868Mi) % 73.23/11.22 % (4035834)------------------------------ % 73.23/11.22 % (4035834)------------------------------ % 73.23/11.22 % (4035847)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=113584535:i=1846:canc=cautious:fsr=off:rtra=on_2934 on theBenchmark for (2934ds/1846Mi) % 73.23/11.22 % (4035831)Instruction limit reached! % 73.23/11.22 % (4035831)------------------------------ % 73.23/11.22 % (4035831)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 73.23/11.22 % (4035831)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 73.23/11.22 % (4035831)CaDiCaL version: 2.1.3 % 73.23/11.22 % (4035831)Termination reason: Instruction limit % 73.23/11.22 % (4035831)Termination phase: Saturation % 73.23/11.22 % (4035831)Time elapsed: 0.895 s % 73.23/11.22 % (4035831)Peak memory usage: 114 MB % 73.23/11.22 % (4035831)Instructions burned: 1131 (million) % 73.23/11.22 % (4035849)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=1808567232:s2a=on:i=36816:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2934 on theBenchmark for (2934ds/36816Mi) % 73.23/11.22 % (4035847)Refutation not found, incomplete strategy % 73.23/11.22 % (4035847)------------------------------ % 73.23/11.22 % (4035847)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 73.23/11.22 % (4035847)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 73.23/11.22 % (4035847)CaDiCaL version: 2.1.3 % 73.23/11.22 % (4035847)Termination reason: Refutation not found, incomplete strategy % 73.23/11.22 % (4035847)Time elapsed: 0.083 s % 73.23/11.22 % (4035847)Peak memory usage: 89 MB % 73.23/11.22 % (4035847)Instructions burned: 115 (million) % 73.23/11.22 % (4035851)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=2463760274:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2931 on theBenchmark for (2931ds/273Mi) % 73.23/11.22 % (4035851)Instruction limit reached! % 73.23/11.22 % (4035851)------------------------------ % 73.23/11.22 % (4035851)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 73.23/11.22 % (4035851)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 73.23/11.22 % (4035851)CaDiCaL version: 2.1.3 % 73.23/11.22 % (4035851)Termination reason: Instruction limit % 73.23/11.22 % (4035851)Termination phase: Saturation % 73.23/11.22 % (4035851)Time elapsed: 0.202 s % 73.23/11.22 % (4035851)Peak memory usage: 91 MB % 73.23/11.22 % (4035851)Instructions burned: 273 (million) % 73.23/11.22 % (4035840)Instruction limit reached! % 73.23/11.22 % (4035840)------------------------------ % 73.23/11.22 % (4035840)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 73.23/11.22 % (4035840)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 73.23/11.22 % (4035840)CaDiCaL version: 2.1.3 % 73.23/11.22 % (4035840)Termination reason: Instruction limit % 73.23/11.22 % (4035840)Termination phase: Saturation % 73.23/11.22 % (4035840)Time elapsed: 0.770 s % 73.23/11.22 % (4035840)Peak memory usage: 91 MB % 73.23/11.22 % (4035840)Instructions burned: 1095 (million) % 73.23/11.22 % (4035847)------------------------------ % 73.23/11.22 % (4035847)------------------------------ % 73.23/11.22 % (4035844)Instruction limit reached! % 73.23/11.22 % (4035844)------------------------------ % 73.23/11.22 % (4035844)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 73.23/11.22 % (4035844)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 73.23/11.22 % (4035844)CaDiCaL version: 2.1.3 % 73.23/11.22 % (4035844)Termination reason: Instruction limit % 73.23/11.22 % (4035844)Termination phase: Saturation % 73.23/11.22 % (4035844)Time elapsed: 0.730 s % 73.23/11.22 % (4035844)Peak memory usage: 137 MB % 73.23/11.22 % (4035844)Instructions burned: 868 (million) % 73.23/11.22 % (4035795)Instruction limit reached! % 73.23/11.22 % (4035795)------------------------------ % 73.23/11.22 % (4035795)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 73.23/11.22 % (4035795)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 73.23/11.22 % (4035795)CaDiCaL version: 2.1.3 % 82.83/12.74 % (4035795)Termination reason: Instruction limit % 82.83/12.74 % (4035795)Termination phase: Saturation % 82.83/12.74 % (4035795)Time elapsed: 3.012 s % 82.83/12.74 % (4035795)Peak memory usage: 92 MB % 82.83/12.74 % (4035795)Instructions burned: 4429 (million) % 82.83/12.74 % (4035854)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=668687186:i=863:doe=on:nm=0:rtra=on:gtg=exists_sym_2927 on theBenchmark for (2927ds/863Mi) % 82.83/12.74 % (4035855)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=3409347772:i=5811:kws=precedence:nm=0:rtra=on_2927 on theBenchmark for (2927ds/5811Mi) % 82.83/12.74 % (4035856)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=3093650107:i=2216:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2927 on theBenchmark for (2927ds/2216Mi) % 82.83/12.74 % (4035857)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=2703847701:i=801:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2927 on theBenchmark for (2927ds/801Mi) % 82.83/12.74 % (4035858)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=3493493024:st=5:i=1026:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2926 on theBenchmark for (2926ds/1026Mi) % 82.83/12.74 % (4035858)Refutation not found, incomplete strategy % 82.83/12.74 % (4035858)------------------------------ % 82.83/12.74 % (4035858)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 82.83/12.74 % (4035858)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 82.83/12.74 % (4035858)CaDiCaL version: 2.1.3 % 82.83/12.74 % (4035858)Termination reason: Refutation not found, incomplete strategy % 82.83/12.74 % (4035858)Time elapsed: 0.032 s % 82.83/12.74 % (4035858)Peak memory usage: 88 MB % 82.83/12.74 % (4035858)Instructions burned: 48 (million) % 82.83/12.74 % (4035858)------------------------------ % 82.83/12.74 % (4035858)------------------------------ % 82.83/12.74 % (4035857)Instruction limit reached! % 82.83/12.74 % (4035857)------------------------------ % 82.83/12.74 % (4035857)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 82.83/12.74 % (4035857)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 82.83/12.74 % (4035857)CaDiCaL version: 2.1.3 % 82.83/12.74 % (4035857)Termination reason: Instruction limit % 82.83/12.74 % (4035857)Termination phase: Saturation % 82.83/12.74 % (4035857)Time elapsed: 0.673 s % 82.83/12.74 % (4035857)Peak memory usage: 101 MB % 82.83/12.74 % (4035857)Instructions burned: 801 (million) % 82.83/12.74 % (4035854)Instruction limit reached! % 82.83/12.74 % (4035854)------------------------------ % 82.83/12.74 % (4035854)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 82.83/12.74 % (4035854)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 82.83/12.74 % (4035854)CaDiCaL version: 2.1.3 % 82.83/12.74 % (4035854)Termination reason: Instruction limit % 82.83/12.74 % (4035854)Termination phase: Saturation % 82.83/12.74 % (4035854)Time elapsed: 0.752 s % 82.83/12.74 % (4035854)Peak memory usage: 137 MB % 82.83/12.74 % (4035854)Instructions burned: 863 (million) % 82.83/12.74 % (4035864)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=1459525707:i=3509:rtra=on_2919 on theBenchmark for (2919ds/3509Mi) % 82.83/12.74 % (4035865)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=4042539499:st=2:i=2127:sd=12:ep=R:rtra=on:ss=axioms_2917 on theBenchmark for (2917ds/2127Mi) % 82.83/12.74 % (4035866)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=2505799961:i=1959:rtra=on:fsd=on:proc=on_2917 on theBenchmark for (2917ds/1959Mi) % 82.83/12.74 % (4035865)Refutation not found, incomplete strategy % 82.83/12.74 % (4035865)------------------------------ % 82.83/12.74 % (4035865)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 82.83/12.74 % (4035865)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 82.83/12.74 % (4035865)CaDiCaL version: 2.1.3 % 82.83/12.74 % (4035865)Termination reason: Refutation not found, incomplete strategy % 82.83/12.74 % (4035865)Time elapsed: 0.043 s % 82.83/12.74 % (4035865)Peak memory usage: 88 MB % 82.83/12.74 % (4035865)Instructions burned: 63 (million) % 82.83/12.74 % (4035842)Instruction limit reached! % 82.83/12.74 % (4035842)------------------------------ % 82.83/12.74 % (4035842)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 82.83/12.74 % (4035842)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.19/17.92 % (4035842)CaDiCaL version: 2.1.3 % 120.19/17.92 % (4035842)Termination reason: Instruction limit % 120.19/17.92 % (4035842)Termination phase: Saturation % 120.19/17.92 % (4035842)Time elapsed: 2.368 s % 120.19/17.92 % (4035842)Peak memory usage: 93 MB % 120.19/17.92 % (4035842)Instructions burned: 6400 (million) % 120.19/17.92 % (4035865)------------------------------ % 120.19/17.92 % (4035865)------------------------------ % 120.19/17.92 % (4035870)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=3417489914:s2a=on:i=3553:nm=0:rtra=on_2911 on theBenchmark for (2911ds/3553Mi) % 120.19/17.92 % (4035856)Instruction limit reached! % 120.19/17.92 % (4035856)------------------------------ % 120.19/17.92 % (4035856)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 120.19/17.92 % (4035856)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.19/17.92 % (4035856)CaDiCaL version: 2.1.3 % 120.19/17.92 % (4035856)Termination reason: Instruction limit % 120.19/17.92 % (4035856)Termination phase: Saturation % 120.19/17.92 % (4035856)Time elapsed: 1.649 s % 120.19/17.92 % (4035856)Peak memory usage: 122 MB % 120.19/17.92 % (4035856)Instructions burned: 2218 (million) % 120.19/17.92 % (4035871)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=3276408635:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2910 on theBenchmark for (2910ds/3201Mi) % 120.19/17.92 % (4035874)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=375555270:thitd=on:cond=on:i=4093:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2908 on theBenchmark for (2908ds/4093Mi) % 120.19/17.92 % (4035871)Refutation not found, incomplete strategy % 120.19/17.92 % (4035871)------------------------------ % 120.19/17.92 % (4035871)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 120.19/17.92 % (4035871)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.19/17.92 % (4035871)CaDiCaL version: 2.1.3 % 120.19/17.92 % (4035871)Termination reason: Refutation not found, incomplete strategy % 120.19/17.92 % (4035871)Time elapsed: 0.327 s % 120.19/17.92 % (4035871)Peak memory usage: 93 MB % 120.19/17.92 % (4035871)Instructions burned: 432 (million) % 120.19/17.92 % (4035871)------------------------------ % 120.19/17.92 % (4035871)------------------------------ % 120.19/17.92 % (4035866)Instruction limit reached! % 120.19/17.92 % (4035866)------------------------------ % 120.19/17.92 % (4035866)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 120.19/17.92 % (4035866)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.19/17.92 % (4035866)CaDiCaL version: 2.1.3 % 120.19/17.92 % (4035866)Termination reason: Instruction limit % 120.19/17.92 % (4035866)Termination phase: Saturation % 120.19/17.92 % (4035866)Time elapsed: 1.515 s % 120.19/17.92 % (4035866)Peak memory usage: 121 MB % 120.19/17.92 % (4035866)Instructions burned: 1960 (million) % 120.19/17.92 % (4035876)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=1870339181:cond=fast:i=21173:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2900 on theBenchmark for (2900ds/21173Mi) % 120.19/17.92 % (4035876)Refutation not found, incomplete strategy % 120.19/17.92 % (4035876)------------------------------ % 120.19/17.92 % (4035876)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 120.19/17.92 % (4035876)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.19/17.92 % (4035876)CaDiCaL version: 2.1.3 % 120.19/17.92 % (4035876)Termination reason: Refutation not found, incomplete strategy % 120.19/17.92 % (4035876)Time elapsed: 0.054 s % 120.19/17.92 % (4035876)Peak memory usage: 113 MB % 120.19/17.92 % (4035876)Instructions burned: 24 (million) % 120.19/17.92 % (4035877)lrs+11_1_to=lpo:thi=all:sas=z3:si=on:fd=off:sac=on:slsq=on:random_seed=2591668982:avsq=on:i=10544:avsqr=17,4:canc=force:rtra=on:gtg=exists_top:er=filter_2899 on theBenchmark for (2899ds/10544Mi) % 120.19/17.92 % (4035870)Instruction limit reached! % 120.19/17.92 % (4035870)------------------------------ % 120.19/17.92 % (4035870)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 120.19/17.92 % (4035870)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.19/17.92 % (4035870)CaDiCaL version: 2.1.3 % 120.19/17.92 % (4035870)Termination reason: Instruction limit % 120.19/17.92 % (4035870)Termination phase: Saturation % 120.19/17.92 % (4035870)Time elapsed: 1.324 s % 120.19/17.92 % (4035870)Peak memory usage: 93 MB % 136.12/20.12 % (4035870)Instructions burned: 3556 (million) % 136.12/20.12 % (4035876)------------------------------ % 136.12/20.12 % (4035876)------------------------------ % 136.12/20.12 % (4035880)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=2349304876:avsq=on:i=1262:avsqr=1,16:rtra=on:rawr=on_2896 on theBenchmark for (2896ds/1262Mi) % 136.12/20.12 % (4035864)Instruction limit reached! % 136.12/20.12 % (4035864)------------------------------ % 136.12/20.12 % (4035864)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 136.12/20.12 % (4035864)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.12/20.12 % (4035864)CaDiCaL version: 2.1.3 % 136.12/20.12 % (4035864)Termination reason: Instruction limit % 136.12/20.12 % (4035864)Termination phase: Saturation % 136.12/20.12 % (4035864)Time elapsed: 2.485 s % 136.12/20.12 % (4035864)Peak memory usage: 91 MB % 136.12/20.12 % (4035864)Instructions burned: 3509 (million) % 136.12/20.12 % (4035882)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=3082619132:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2893 on theBenchmark for (2893ds/775Mi) % 136.12/20.12 % (4035882)Refutation not found, incomplete strategy % 136.12/20.12 % (4035882)------------------------------ % 136.12/20.12 % (4035882)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 136.12/20.12 % (4035882)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.12/20.12 % (4035882)CaDiCaL version: 2.1.3 % 136.12/20.12 % (4035882)Termination reason: Refutation not found, incomplete strategy % 136.12/20.12 % (4035882)Time elapsed: 0.046 s % 136.12/20.12 % (4035882)Peak memory usage: 88 MB % 136.12/20.12 % (4035882)Instructions burned: 66 (million) % 136.12/20.12 % (4035883)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=4248752475:i=270:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2891 on theBenchmark for (2891ds/270Mi) % 136.12/20.12 % (4035880)Instruction limit reached! % 136.12/20.12 % (4035880)------------------------------ % 136.12/20.12 % (4035880)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 136.12/20.12 % (4035880)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.12/20.12 % (4035880)CaDiCaL version: 2.1.3 % 136.12/20.12 % (4035880)Termination reason: Instruction limit % 136.12/20.12 % (4035880)Termination phase: Saturation % 136.12/20.12 % (4035880)Time elapsed: 0.509 s % 136.12/20.12 % (4035880)Peak memory usage: 121 MB % 136.12/20.12 % (4035880)Instructions burned: 1264 (million) % 136.12/20.12 % (4035883)Instruction limit reached! % 136.12/20.12 % (4035883)------------------------------ % 136.12/20.12 % (4035883)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 136.12/20.12 % (4035883)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.12/20.12 % (4035883)CaDiCaL version: 2.1.3 % 136.12/20.12 % (4035883)Termination reason: Instruction limit % 136.12/20.12 % (4035883)Termination phase: Saturation % 136.12/20.12 % (4035883)Time elapsed: 0.203 s % 136.12/20.12 % (4035883)Peak memory usage: 92 MB % 136.12/20.12 % (4035883)Instructions burned: 270 (million) % 136.12/20.12 % (4035886)ott+10_128_isp=bottom:to=lpo:sil=128000:si=on:urr=on:uwa=alasca_main:sac=on:slsq=on:random_seed=1333981056:i=17165:aac=none:doe=on:rtra=on:gtg=exists_all_2888 on theBenchmark for (2888ds/17165Mi) % 136.12/20.12 % (4035882)------------------------------ % 136.12/20.12 % (4035882)------------------------------ % 136.12/20.12 % (4035887)lrs+2_10_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_main:tha=some:random_seed=158509460:s2a=on:i=13094:s2at=-1:rtra=on_2886 on theBenchmark for (2886ds/13094Mi) % 136.12/20.12 % (4035889)lrs+10_1_to=lpo:sil=128000:si=on:sp=occurrence:random_seed=1410701535:st=2:i=12633:rtra=on:ss=axioms_2886 on theBenchmark for (2886ds/12633Mi) % 136.12/20.12 % (4035889)Refutation not found, incomplete strategy % 136.12/20.12 % (4035889)------------------------------ % 136.12/20.12 % (4035889)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 136.12/20.12 % (4035889)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.12/20.12 % (4035889)CaDiCaL version: 2.1.3 % 136.12/20.12 % (4035889)Termination reason: Refutation not found, incomplete strategy % 136.12/20.12 % (4035889)Time elapsed: 0.029 s % 136.12/20.12 % (4035889)Peak memory usage: 88 MB % 136.12/20.12 % (4035889)Instructions burned: 35 (million) % 136.12/20.12 % (4035855)Instruction limit reached! % 136.12/20.12 % (4035855)------------------------------ % 136.12/20.12 % (4035855)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 159.26/23.34 % (4035855)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 159.26/23.34 % (4035855)CaDiCaL version: 2.1.3 % 159.26/23.34 % (4035855)Termination reason: Instruction limit % 159.26/23.34 % (4035855)Termination phase: Saturation % 159.26/23.34 % (4035855)Time elapsed: 4.418 s % 159.26/23.34 % (4035855)Peak memory usage: 121 MB % 159.26/23.34 % (4035855)Instructions burned: 5812 (million) % 159.26/23.34 % (4035889)------------------------------ % 159.26/23.34 % (4035889)------------------------------ % 159.26/23.34 % (4035892)dis+1011_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_frequency:lsd=20:nwc=3:random_seed=345325536:i=1783:rtra=on:gtg=position_2880 on theBenchmark for (2880ds/1783Mi) % 159.26/23.34 % (4035894)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=1934306466:i=5451:aac=none:doe=on:nm=0:rtra=on:amm=off:gtg=position_2879 on theBenchmark for (2879ds/5451Mi) % 159.26/23.34 % (4035874)Instruction limit reached! % 159.26/23.34 % (4035874)------------------------------ % 159.26/23.34 % (4035874)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 159.26/23.34 % (4035874)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 159.26/23.34 % (4035874)CaDiCaL version: 2.1.3 % 159.26/23.34 % (4035874)Termination reason: Instruction limit % 159.26/23.34 % (4035874)Termination phase: Saturation % 159.26/23.34 % (4035874)Time elapsed: 3.003 s % 159.26/23.34 % (4035874)Peak memory usage: 134 MB % 159.26/23.34 % (4035874)Instructions burned: 4094 (million) % 159.26/23.34 % (4035898)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=3294804906:i=4975:doe=on:nm=0:rtra=on:gtg=exists_sym_2875 on theBenchmark for (2875ds/4975Mi) % 159.26/23.34 % (4035892)Instruction limit reached! % 159.26/23.34 % (4035892)------------------------------ % 159.26/23.34 % (4035892)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 159.26/23.34 % (4035892)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 159.26/23.34 % (4035892)CaDiCaL version: 2.1.3 % 159.26/23.34 % (4035892)Termination reason: Instruction limit % 159.26/23.34 % (4035892)Termination phase: Saturation % 159.26/23.34 % (4035892)Time elapsed: 1.342 s % 159.26/23.34 % (4035892)Peak memory usage: 121 MB % 159.26/23.34 % (4035892)Instructions burned: 1784 (million) % 159.26/23.34 % (4035900)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=1565478608:i=2076:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2864 on theBenchmark for (2864ds/2076Mi) % 159.26/23.34 % (4035900)Instruction limit reached! % 159.26/23.34 % (4035900)------------------------------ % 159.26/23.34 % (4035900)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 159.26/23.34 % (4035900)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 159.26/23.34 % (4035900)CaDiCaL version: 2.1.3 % 159.26/23.34 % (4035900)Termination reason: Instruction limit % 159.26/23.34 % (4035900)Termination phase: Saturation % 159.26/23.34 % (4035900)Time elapsed: 1.528 s % 159.26/23.34 % (4035900)Peak memory usage: 122 MB % 159.26/23.34 % (4035900)Instructions burned: 2077 (million) % 159.26/23.34 % (4035902)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=2869336961:i=5145:rtra=on_2846 on theBenchmark for (2846ds/5145Mi) % 159.26/23.34 % (4035894)Instruction limit reached! % 159.26/23.34 % (4035894)------------------------------ % 159.26/23.34 % (4035894)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 159.26/23.34 % (4035894)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 159.26/23.34 % (4035894)CaDiCaL version: 2.1.3 % 159.26/23.34 % (4035894)Termination reason: Instruction limit % 159.26/23.34 % (4035894)Termination phase: Saturation % 159.26/23.34 % (4035894)Time elapsed: 3.999 s % 159.26/23.34 % (4035894)Peak memory usage: 122 MB % 159.26/23.34 % (4035894)Instructions burned: 5452 (million) % 159.26/23.34 % (4035904)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=3938990016:i=3509:rtra=on_2836 on theBenchmark for (2836ds/3509Mi) % 159.26/23.34 % (4035898)Instruction limit reached! % 159.26/23.34 % (4035898)------------------------------ % 159.26/23.34 % (4035898)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 159.26/23.34 % (4035898)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 159.26/23.34 % (4035898)CaDiCaL version: 2.1.3 % 159.26/23.34 % (4035898)Termination reason: Instruction limit % 233.20/33.77 % (4035898)Termination phase: Saturation % 233.20/33.77 % (4035898)Time elapsed: 4.320 s % 233.20/33.77 % (4035898)Peak memory usage: 161 MB % 233.20/33.77 % (4035898)Instructions burned: 4975 (million) % 233.20/33.77 % (4035906)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=1423575666:st=2:i=13800:sd=12:ep=R:rtra=on:ss=axioms_2828 on theBenchmark for (2828ds/13800Mi) % 233.20/33.77 % (4035906)Refutation not found, incomplete strategy % 233.20/33.77 % (4035906)------------------------------ % 233.20/33.77 % (4035906)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 233.20/33.77 % (4035906)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 233.20/33.77 % (4035906)CaDiCaL version: 2.1.3 % 233.20/33.77 % (4035906)Termination reason: Refutation not found, incomplete strategy % 233.20/33.77 % (4035906)Time elapsed: 0.043 s % 233.20/33.77 % (4035906)Peak memory usage: 88 MB % 233.20/33.77 % (4035906)Instructions burned: 63 (million) % 233.20/33.77 % (4035886)Instruction limit reached! % 233.20/33.77 % (4035886)------------------------------ % 233.20/33.77 % (4035886)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 233.20/33.77 % (4035886)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 233.20/33.77 % (4035886)CaDiCaL version: 2.1.3 % 233.20/33.77 % (4035886)Termination reason: Instruction limit % 233.20/33.77 % (4035886)Termination phase: Saturation % 233.20/33.77 % (4035886)Time elapsed: 6.406 s % 233.20/33.77 % (4035886)Peak memory usage: 97 MB % 233.20/33.77 % (4035886)Instructions burned: 17165 (million) % 233.20/33.77 % (4035906)------------------------------ % 233.20/33.77 % (4035906)------------------------------ % 233.20/33.77 % (4035908)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=2996113820:i=1412:rtra=on:fsd=on:proc=on_2822 on theBenchmark for (2822ds/1412Mi) % 233.20/33.77 % (4035909)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 % 233.20/33.77 % (4035909)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=3091062601:i=11747:aac=none:nm=0:rtra=on:rawr=on_2821 on theBenchmark for (2821ds/11747Mi) % 233.20/33.77 % (4035908)Instruction limit reached! % 233.20/33.77 % (4035908)------------------------------ % 233.20/33.77 % (4035908)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 233.20/33.77 % (4035908)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 233.20/33.77 % (4035908)CaDiCaL version: 2.1.3 % 233.20/33.77 % (4035908)Termination reason: Instruction limit % 233.20/33.77 % (4035908)Termination phase: Saturation % 233.20/33.77 % (4035908)Time elapsed: 0.579 s % 233.20/33.77 % (4035908)Peak memory usage: 121 MB % 233.20/33.77 % (4035908)Instructions burned: 1412 (million) % 233.20/33.77 % (4035912)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=2756004061:s2a=on:i=3553:nm=0:rtra=on_2814 on theBenchmark for (2814ds/3553Mi) % 233.20/33.77 % (4035904)Instruction limit reached! % 233.20/33.77 % (4035904)------------------------------ % 233.20/33.77 % (4035904)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 233.20/33.77 % (4035904)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 233.20/33.77 % (4035904)CaDiCaL version: 2.1.3 % 233.20/33.77 % (4035904)Termination reason: Instruction limit % 233.20/33.77 % (4035904)Termination phase: Saturation % 233.20/33.77 % (4035904)Time elapsed: 2.466 s % 233.20/33.77 % (4035904)Peak memory usage: 91 MB % 233.20/33.77 % (4035904)Instructions burned: 3510 (million) % 233.20/33.77 % (4035877)Instruction limit reached! % 233.20/33.77 % (4035877)------------------------------ % 233.20/33.77 % (4035877)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 233.20/33.77 % (4035877)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 233.20/33.77 % (4035877)CaDiCaL version: 2.1.3 % 233.20/33.77 % (4035877)Termination reason: Instruction limit % 233.20/33.77 % (4035877)Termination phase: Saturation % 233.20/33.77 % (4035877)Time elapsed: 8.995 s % 233.20/33.77 % (4035877)Peak memory usage: 172 MB % 233.20/33.77 % (4035877)Instructions burned: 10545 (million) % 233.20/33.77 % (4035902)Instruction limit reached! % 233.20/33.77 % (4035902)------------------------------ % 233.20/33.77 % (4035902)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 233.20/33.77 % (4035902)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 233.20/33.77 % (4035902)CaDiCaL version: 2.1.3 % 266.94/38.57 % (4035902)Termination reason: Instruction limit % 266.94/38.57 % (4035902)Termination phase: Saturation % 266.94/38.57 % (4035902)Time elapsed: 3.674 s % 266.94/38.57 % (4035902)Peak memory usage: 96 MB % 266.94/38.57 % (4035902)Instructions burned: 5146 (million) % 266.94/38.57 % (4035916)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=1616359010:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2808 on theBenchmark for (2808ds/3201Mi) % 266.94/38.57 % (4035917)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=1199880310:thitd=on:cond=on:i=4081:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2807 on theBenchmark for (2807ds/4081Mi) % 266.94/38.57 % (4035918)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=1031597264:cond=fast:i=20260:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2806 on theBenchmark for (2806ds/20260Mi) % 266.94/38.57 % (4035918)Refutation not found, incomplete strategy % 266.94/38.57 % (4035918)------------------------------ % 266.94/38.57 % (4035918)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 266.94/38.57 % (4035918)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 266.94/38.57 % (4035918)CaDiCaL version: 2.1.3 % 266.94/38.57 % (4035918)Termination reason: Refutation not found, incomplete strategy % 266.94/38.57 % (4035918)Time elapsed: 0.053 s % 266.94/38.57 % (4035918)Peak memory usage: 113 MB % 266.94/38.57 % (4035918)Instructions burned: 24 (million) % 266.94/38.57 % (4035916)Refutation not found, incomplete strategy % 266.94/38.57 % (4035916)------------------------------ % 266.94/38.57 % (4035916)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 266.94/38.57 % (4035916)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 266.94/38.57 % (4035916)CaDiCaL version: 2.1.3 % 266.94/38.57 % (4035916)Termination reason: Refutation not found, incomplete strategy % 266.94/38.57 % (4035916)Time elapsed: 0.376 s % 266.94/38.57 % (4035916)Peak memory usage: 93 MB % 266.94/38.57 % (4035916)Instructions burned: 493 (million) % 266.94/38.57 % (4035918)------------------------------ % 266.94/38.57 % (4035918)------------------------------ % 266.94/38.57 % (4035912)Instruction limit reached! % 266.94/38.57 % (4035912)------------------------------ % 266.94/38.57 % (4035912)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 266.94/38.57 % (4035912)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 266.94/38.57 % (4035912)CaDiCaL version: 2.1.3 % 266.94/38.57 % (4035912)Termination reason: Instruction limit % 266.94/38.57 % (4035912)Termination phase: Saturation % 266.94/38.57 % (4035912)Time elapsed: 1.320 s % 266.94/38.57 % (4035912)Peak memory usage: 93 MB % 266.94/38.57 % (4035912)Instructions burned: 3553 (million) % 266.94/38.57 % (4035916)------------------------------ % 266.94/38.57 % (4035916)------------------------------ % 266.94/38.57 % (4035925)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=3391460425:avsq=on:i=6258:avsqr=1,16:rtra=on:rawr=on_2799 on theBenchmark for (2799ds/6258Mi) % 266.94/38.57 % (4035924)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=3992502693:s2a=on:i=58627:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2799 on theBenchmark for (2799ds/58627Mi) % 266.94/38.57 % (4035926)ott+10_128_isp=bottom:to=lpo:sil=128000:si=on:urr=on:uwa=alasca_main:sac=on:slsq=on:random_seed=1497421465:i=34001:aac=none:doe=on:rtra=on:gtg=exists_all_2798 on theBenchmark for (2798ds/34001Mi) % 266.94/38.57 % (4035887)Instruction limit reached! % 266.94/38.57 % (4035887)------------------------------ % 266.94/38.57 % (4035887)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 266.94/38.57 % (4035887)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 266.94/38.57 % (4035887)CaDiCaL version: 2.1.3 % 266.94/38.57 % (4035887)Termination reason: Instruction limit % 266.94/38.57 % (4035887)Termination phase: Saturation % 266.94/38.57 % (4035887)Time elapsed: 9.388 s % 266.94/38.57 % (4035887)Peak memory usage: 118 MB % 266.94/38.57 % (4035887)Instructions burned: 13095 (million) % 266.94/38.57 % (4035930)lrs+2_10_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_main:tha=some:random_seed=1410691397:s2a=on:i=71622:s2at=-1:rtra=on_2790 on theBenchmark for (2790ds/71622Mi) % 266.94/38.57 % (4035917)Instruction limit reached! % 266.94/38.57 % (4035917)------------------------------ % 266.94/38.57 % (4035917)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 293.53/42.28 % (4035917)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 293.53/42.28 % (4035917)CaDiCaL version: 2.1.3 % 293.53/42.28 % (4035917)Termination reason: Instruction limit % 293.53/42.28 % (4035917)Termination phase: Saturation % 293.53/42.28 % (4035917)Time elapsed: 2.933 s % 293.53/42.28 % (4035917)Peak memory usage: 134 MB % 293.53/42.28 % (4035917)Instructions burned: 4081 (million) % 293.53/42.28 % (4035925)Instruction limit reached! % 293.53/42.28 % (4035925)------------------------------ % 293.53/42.28 % (4035925)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 293.53/42.28 % (4035925)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 293.53/42.28 % (4035925)CaDiCaL version: 2.1.3 % 293.53/42.28 % (4035925)Termination reason: Instruction limit % 293.53/42.28 % (4035925)Termination phase: Saturation % 293.53/42.28 % (4035925)Time elapsed: 2.499 s % 293.53/42.28 % (4035925)Peak memory usage: 123 MB % 293.53/42.28 % (4035925)Instructions burned: 6260 (million) % 293.53/42.28 % (4035934)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=2342136997:i=24001:kws=precedence:nm=0:rtra=on_2774 on theBenchmark for (2774ds/24001Mi) % 293.53/42.28 % (4035935)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=2854194140:i=2076:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2772 on theBenchmark for (2772ds/2076Mi) % 293.53/42.28 % (4035935)Instruction limit reached! % 293.53/42.28 % (4035935)------------------------------ % 293.53/42.28 % (4035935)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 293.53/42.28 % (4035935)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 293.53/42.28 % (4035935)CaDiCaL version: 2.1.3 % 293.53/42.28 % (4035935)Termination reason: Instruction limit % 293.53/42.28 % (4035935)Termination phase: Saturation % 293.53/42.28 % (4035935)Time elapsed: 0.807 s % 293.53/42.28 % (4035935)Peak memory usage: 122 MB % 293.53/42.28 % (4035935)Instructions burned: 2078 (million) % 293.53/42.28 % (4035938)dis+21_20_to=lakbo:si=on:alasca=on:sp=const_max:uwa=alasca_main:sac=on:random_seed=2718177924:s2a=on:i=83971:s2at=4:bd=all:ins=1:rtra=on_2762 on theBenchmark for (2762ds/83971Mi) % 293.53/42.28 % (4035849)Refutation not found, non-redundant clauses discarded % 293.53/42.28 % (4035849)------------------------------ % 293.53/42.28 % (4035849)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 293.53/42.28 % (4035849)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 293.53/42.28 % (4035849)CaDiCaL version: 2.1.3 % 293.53/42.28 % (4035849)Termination reason: Refutation not found, non-redundant clauses discarded % 293.53/42.28 % (4035849)Time elapsed: 18.801 s % 293.53/42.28 % (4035849)Peak memory usage: 107 MB % 293.53/42.28 % (4035849)Instructions burned: 26911 (million) % 293.53/42.28 % (4035849)------------------------------ % 293.53/42.28 % (4035849)------------------------------ % 293.53/42.28 % (4035950)lrs+1011_5:1_to=lpo:sil=128000:sas=z3:si=on:norm_ineq=on:tha=some:random_seed=1506792404:i=83944:rtra=on_2739 on theBenchmark for (2739ds/83944Mi) % 293.53/42.28 % (4035909)Instruction limit reached! % 293.53/42.28 % (4035909)------------------------------ % 293.53/42.28 % (4035909)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 293.53/42.28 % (4035909)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 293.53/42.28 % (4035909)CaDiCaL version: 2.1.3 % 293.53/42.28 % (4035909)Termination reason: Instruction limit % 293.53/42.28 % (4035909)Termination phase: Saturation % 293.53/42.28 % (4035909)Time elapsed: 8.943 s % 293.53/42.28 % (4035909)Peak memory usage: 138 MB % 293.53/42.28 % (4035909)Instructions burned: 11747 (million) % 293.53/42.28 % (4035952)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=2227289481:i=9201:rtra=on_2729 on theBenchmark for (2729ds/9201Mi) % 293.53/42.28 % (4035952)Instruction limit reached! % 293.53/42.28 % (4035952)------------------------------ % 293.53/42.28 % (4035952)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 293.53/42.28 % (4035952)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 293.53/42.28 % (4035952)CaDiCaL version: 2.1.3 % 293.53/42.28 % (4035952)Termination reason: Instruction limit % 293.53/42.28 % (4035952)Termination phase: Saturation % 293.53/42.28 % (4035952)Time elapsed: 5.376 s % 293.53/42.28 % (4035952)Peak memory usage: 93 MB % 293.53/42.28 % (4035952)Instructions burned: 9203 (million) % 293.53/42.28 % (4036006)WARNING Broken Constraint: if demodulation_redundancy_check(ordering) haTerminated %------------------------------------------------------------------------------