%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : NUM922_1 : TPTP v9.3.1. Released v5.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % Computer : n008.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 12:17:27 PM UTC 2026 % Result : Timeout 293.91s 42.29s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : NUM922_1 : TPTP v9.3.1. Released v5.0.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.12/0.38 % Computer : n008.cluster.edu % 0.12/0.38 % Model : x86_64 x86_64 % 0.12/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.38 % Memory : 8046.5625MB % 0.12/0.38 % OS : Linux 6.8.0-71-generic % 0.12/0.38 % CPULimit : 300 % 0.12/0.38 % WCLimit : 300 % 0.12/0.38 % DateTime : Sun Sep 27 21:40:09 UTC 2026 % 0.12/0.39 % CPUTime : % 0.12/0.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.12/0.42 Running first-order theorem proving % 0.12/0.42 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 3.29/1.46 % (1626867)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule. % 3.29/1.46 % (1626874)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=2358703400:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi) % 3.29/1.46 % (1626878)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=4026077787:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi) % 3.29/1.46 % (1626873)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=54995011:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi) % 3.29/1.46 % (1626875)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=3490228595:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi) % 3.29/1.46 % (1626872)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=1979689681:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi) % 3.29/1.46 % (1626876)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=2155083719:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi) % 3.29/1.46 % (1626877)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=4081458211:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi) % 3.29/1.46 % (1626876)Instruction limit reached! % 3.29/1.46 % (1626876)------------------------------ % 3.29/1.46 % (1626876)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.29/1.46 % (1626876)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.29/1.46 % (1626876)CaDiCaL version: 2.1.3 % 3.29/1.46 % (1626876)Termination reason: Instruction limit % 3.29/1.46 % (1626876)Termination phase: Saturation % 3.29/1.46 % (1626876)Time elapsed: 0.004 s % 3.29/1.46 % (1626876)Peak memory usage: 88 MB % 3.29/1.46 % (1626876)Instructions burned: 5 (million) % 3.29/1.46 % (1626875)Instruction limit reached! % 3.29/1.46 % (1626875)------------------------------ % 3.29/1.46 % (1626875)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.29/1.46 % (1626875)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.29/1.46 % (1626875)CaDiCaL version: 2.1.3 % 3.29/1.46 % (1626875)Termination reason: Instruction limit % 3.29/1.46 % (1626875)Termination phase: Saturation % 3.29/1.46 % (1626875)Time elapsed: 0.006 s % 3.29/1.46 % (1626875)Peak memory usage: 88 MB % 3.29/1.46 % (1626875)Instructions burned: 7 (million) % 3.29/1.46 % (1626874)Instruction limit reached! % 3.29/1.46 % (1626874)------------------------------ % 3.29/1.46 % (1626874)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.29/1.46 % (1626874)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.29/1.46 % (1626874)CaDiCaL version: 2.1.3 % 3.29/1.46 % (1626874)Termination reason: Instruction limit % 3.29/1.46 % (1626874)Termination phase: Saturation % 3.29/1.46 % (1626874)Time elapsed: 0.059 s % 3.29/1.46 % (1626874)Peak memory usage: 113 MB % 3.29/1.46 % (1626874)Instructions burned: 204 (million) % 3.29/1.46 % (1626877)Refutation not found, incomplete strategy % 3.29/1.46 % (1626877)------------------------------ % 3.29/1.46 % (1626877)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.29/1.46 % (1626873)Refutation not found, incomplete strategy % 3.29/1.46 % (1626873)------------------------------ % 3.29/1.46 % (1626873)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.29/1.46 % (1626873)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.29/1.46 % (1626873)CaDiCaL version: 2.1.3 % 3.29/1.46 % (1626877)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.29/1.46 % (1626873)Termination reason: Refutation not found, incomplete strategy % 3.29/1.46 % (1626873)Time elapsed: 0.029 s % 3.29/1.46 % (1626873)Peak memory usage: 115 MB % 3.29/1.46 % (1626877)CaDiCaL version: 2.1.3 % 3.29/1.46 % (1626873)Instructions burned: 6 (million) % 3.29/1.46 % (1626877)Termination reason: Refutation not found, incomplete strategy % 3.29/1.46 % (1626877)Time elapsed: 0.029 s % 3.29/1.46 % (1626877)Peak memory usage: 114 MB % 3.29/1.46 % (1626877)Instructions burned: 6 (million) % 3.29/1.46 % (1626872)Instruction limit reached! % 3.29/1.46 % (1626872)------------------------------ % 3.29/1.46 % (1626872)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.29/1.46 % (1626872)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.90/1.67 % (1626872)CaDiCaL version: 2.1.3 % 4.90/1.67 % (1626872)Termination reason: Instruction limit % 4.90/1.67 % (1626872)Termination phase: Saturation % 4.90/1.67 % (1626872)Time elapsed: 0.030 s % 4.90/1.67 % (1626872)Peak memory usage: 115 MB % 4.90/1.67 % (1626872)Instructions burned: 12 (million) % 4.90/1.67 % (1626878)Instruction limit reached! % 4.90/1.67 % (1626878)------------------------------ % 4.90/1.67 % (1626878)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.90/1.67 % (1626878)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.90/1.67 % (1626878)CaDiCaL version: 2.1.3 % 4.90/1.67 % (1626878)Termination reason: Instruction limit % 4.90/1.67 % (1626878)Termination phase: Saturation % 4.90/1.67 % (1626878)Time elapsed: 0.047 s % 4.90/1.67 % (1626878)Peak memory usage: 115 MB % 4.90/1.67 % (1626878)Instructions burned: 34 (million) % 4.90/1.67 % (1626888)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=84476799:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/16Mi) % 4.90/1.67 % (1626887)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=3948071641:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2998 on theBenchmark for (2998ds/29Mi) % 4.90/1.67 % (1626886)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=2407401767:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2998 on theBenchmark for (2998ds/14Mi) % 4.90/1.67 % (1626886)Refutation not found, incomplete strategy % 4.90/1.67 % (1626886)------------------------------ % 4.90/1.67 % (1626886)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.90/1.67 % (1626886)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.90/1.67 % (1626886)CaDiCaL version: 2.1.3 % 4.90/1.67 % (1626886)Termination reason: Refutation not found, incomplete strategy % 4.90/1.67 % (1626886)Time elapsed: 0.001 s % 4.90/1.67 % (1626886)Peak memory usage: 88 MB % 4.90/1.67 % (1626888)Instruction limit reached! % 4.90/1.67 % (1626888)------------------------------ % 4.90/1.67 % (1626888)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.90/1.67 % (1626888)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.90/1.67 % (1626888)CaDiCaL version: 2.1.3 % 4.90/1.67 % (1626888)Termination reason: Instruction limit % 4.90/1.67 % (1626888)Termination phase: Saturation % 4.90/1.67 % (1626888)Time elapsed: 0.007 s % 4.90/1.67 % (1626888)Peak memory usage: 90 MB % 4.90/1.67 % (1626888)Instructions burned: 16 (million) % 4.90/1.67 % (1626887)Instruction limit reached! % 4.90/1.67 % (1626887)------------------------------ % 4.90/1.67 % (1626887)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.90/1.67 % (1626887)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.90/1.67 % (1626887)CaDiCaL version: 2.1.3 % 4.90/1.67 % (1626887)Termination reason: Instruction limit % 4.90/1.67 % (1626887)Termination phase: Saturation % 4.90/1.67 % (1626887)Time elapsed: 0.015 s % 4.90/1.67 % (1626887)Peak memory usage: 88 MB % 4.90/1.67 % (1626887)Instructions burned: 30 (million) % 4.90/1.67 % (1626889)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=565983130:i=24:canc=force:rtra=on_2998 on theBenchmark for (2998ds/24Mi) % 4.90/1.67 % (1626889)Instruction limit reached! % 4.90/1.67 % (1626889)------------------------------ % 4.90/1.67 % (1626889)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.90/1.67 % (1626889)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.90/1.67 % (1626889)CaDiCaL version: 2.1.3 % 4.90/1.67 % (1626889)Termination reason: Instruction limit % 4.90/1.67 % (1626889)Termination phase: Saturation % 4.90/1.67 % (1626889)Time elapsed: 0.017 s % 4.90/1.67 % (1626889)Peak memory usage: 89 MB % 4.90/1.67 % (1626889)Instructions burned: 25 (million) % 4.90/1.67 % (1626890)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=692648400:i=27:canc=cautious:fsr=off:rtra=on_2997 on theBenchmark for (2997ds/27Mi) % 4.90/1.67 % (1626890)Instruction limit reached! % 4.90/1.67 % (1626890)------------------------------ % 4.90/1.67 % (1626890)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.90/1.67 % (1626890)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.90/1.67 % (1626890)CaDiCaL version: 2.1.3 % 6.17/1.81 % (1626890)Termination reason: Instruction limit % 6.17/1.81 % (1626890)Termination phase: Saturation % 6.17/1.81 % (1626890)Time elapsed: 0.017 s % 6.17/1.81 % (1626890)Peak memory usage: 89 MB % 6.17/1.81 % (1626890)Instructions burned: 29 (million) % 6.17/1.81 % (1626894)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=466333142:i=85:gtgl=4:rtra=on:gtg=exists_sym_2996 on theBenchmark for (2996ds/85Mi) % 6.17/1.81 % (1626873)------------------------------ % 6.17/1.81 % (1626873)------------------------------ % 6.17/1.81 % (1626877)------------------------------ % 6.17/1.81 % (1626877)------------------------------ % 6.17/1.81 % (1626894)Instruction limit reached! % 6.17/1.81 % (1626894)------------------------------ % 6.17/1.81 % (1626894)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.17/1.81 % (1626894)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.17/1.81 % (1626894)CaDiCaL version: 2.1.3 % 6.17/1.81 % (1626894)Termination reason: Instruction limit % 6.17/1.81 % (1626894)Termination phase: Saturation % 6.17/1.81 % (1626894)Time elapsed: 0.029 s % 6.17/1.81 % (1626894)Peak memory usage: 88 MB % 6.17/1.81 % (1626894)Instructions burned: 87 (million) % 6.17/1.81 % (1626895)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=3009261173:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2996 on theBenchmark for (2996ds/2Mi) % 6.17/1.81 % (1626895)Instruction limit reached! % 6.17/1.81 % (1626895)------------------------------ % 6.17/1.81 % (1626895)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.17/1.81 % (1626895)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.17/1.81 % (1626895)CaDiCaL version: 2.1.3 % 6.17/1.81 % (1626895)Termination reason: Instruction limit % 6.17/1.81 % (1626895)Termination phase: Saturation % 6.17/1.81 % (1626895)Time elapsed: 0.003 s % 6.17/1.81 % (1626895)Peak memory usage: 89 MB % 6.17/1.81 % (1626895)Instructions burned: 2 (million) % 6.17/1.81 % (1626897)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=2423029553:i=181:rtra=on:ss=axioms:ev=cautious_2996 on theBenchmark for (2996ds/181Mi) % 6.17/1.81 % (1626897)Refutation not found, incomplete strategy % 6.17/1.81 % (1626897)------------------------------ % 6.17/1.81 % (1626897)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.17/1.81 % (1626897)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.17/1.81 % (1626897)CaDiCaL version: 2.1.3 % 6.17/1.81 % (1626897)Termination reason: Refutation not found, incomplete strategy % 6.17/1.81 % (1626897)Time elapsed: 0.003 s % 6.17/1.81 % (1626897)Peak memory usage: 89 MB % 6.17/1.81 % (1626897)Instructions burned: 1 (million) % 6.17/1.81 % (1626886)------------------------------ % 6.17/1.81 % (1626886)------------------------------ % 6.17/1.81 % (1626899)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=2926169391:i=4:ep=RST:ins=2:rtra=on_2996 on theBenchmark for (2996ds/4Mi) % 6.17/1.81 % (1626899)Instruction limit reached! % 6.17/1.81 % (1626899)------------------------------ % 6.17/1.81 % (1626899)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.17/1.81 % (1626899)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.17/1.81 % (1626899)CaDiCaL version: 2.1.3 % 6.17/1.81 % (1626899)Termination reason: Instruction limit % 6.17/1.81 % (1626899)Termination phase: Saturation % 6.17/1.81 % (1626899)Time elapsed: 0.003 s % 6.17/1.81 % (1626899)Peak memory usage: 88 MB % 6.17/1.81 % (1626899)Instructions burned: 4 (million) % 6.17/1.81 % (1626903)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=4266579793:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2995 on theBenchmark for (2995ds/8Mi) % 6.17/1.81 % (1626903)Refutation not found, incomplete strategy % 6.17/1.81 % (1626903)------------------------------ % 6.17/1.81 % (1626903)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.17/1.81 % (1626903)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.17/1.81 % (1626903)CaDiCaL version: 2.1.3 % 6.17/1.81 % (1626903)Termination reason: Refutation not found, incomplete strategy % 6.17/1.81 % (1626903)Time elapsed: 0.001 s % 6.17/1.81 % (1626903)Peak memory usage: 89 MB % 6.17/1.81 % (1626903)Instructions burned: 1 (million) % 6.17/1.81 % (1626902)lrs+10_1_thi=all:si=on:fd=off:random_seed=969656573:i=53:rtra=on:gtg=all_2995 on theBenchmark for (2995ds/53Mi) % 6.17/1.81 % (1626901)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=1057135833:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2995 on theBenchmark for (2995ds/66Mi) % 8.58/2.10 % (1626905)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=2625639410:st=3:i=2:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/2Mi) % 8.58/2.10 % (1626905)Instruction limit reached! % 8.58/2.10 % (1626905)------------------------------ % 8.58/2.10 % (1626905)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.58/2.10 % (1626905)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.58/2.10 % (1626905)CaDiCaL version: 2.1.3 % 8.58/2.10 % (1626905)Termination reason: Instruction limit % 8.58/2.10 % (1626905)Termination phase: Saturation % 8.58/2.10 % (1626905)Time elapsed: 0.003 s % 8.58/2.10 % (1626905)Peak memory usage: 90 MB % 8.58/2.10 % (1626905)Instructions burned: 2 (million) % 8.58/2.10 % (1626902)Instruction limit reached! % 8.58/2.10 % (1626902)------------------------------ % 8.58/2.10 % (1626902)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.58/2.10 % (1626902)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.58/2.10 % (1626902)CaDiCaL version: 2.1.3 % 8.58/2.10 % (1626902)Termination reason: Instruction limit % 8.58/2.10 % (1626902)Termination phase: Saturation % 8.58/2.10 % (1626902)Time elapsed: 0.059 s % 8.58/2.10 % (1626902)Peak memory usage: 111 MB % 8.58/2.10 % (1626902)Instructions burned: 54 (million) % 8.58/2.10 % (1626901)Instruction limit reached! % 8.58/2.10 % (1626901)------------------------------ % 8.58/2.10 % (1626901)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.58/2.10 % (1626901)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.58/2.10 % (1626901)CaDiCaL version: 2.1.3 % 8.58/2.10 % (1626901)Termination reason: Instruction limit % 8.58/2.10 % (1626901)Termination phase: Saturation % 8.58/2.10 % (1626901)Time elapsed: 0.086 s % 8.58/2.10 % (1626901)Peak memory usage: 132 MB % 8.58/2.10 % (1626901)Instructions burned: 66 (million) % 8.58/2.10 % (1626903)------------------------------ % 8.58/2.10 % (1626903)------------------------------ % 8.58/2.10 % (1626910)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=1387067778:i=127:doe=on:rtra=on_2994 on theBenchmark for (2994ds/127Mi) % 8.58/2.10 % (1626909)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=1349914489:i=2:doe=on:canc=force:asg=cautious:rtra=on_2994 on theBenchmark for (2994ds/2Mi) % 8.58/2.10 % (1626909)Instruction limit reached! % 8.58/2.10 % (1626909)------------------------------ % 8.58/2.10 % (1626909)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.58/2.10 % (1626909)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.58/2.10 % (1626909)CaDiCaL version: 2.1.3 % 8.58/2.10 % (1626909)Termination reason: Instruction limit % 8.58/2.10 % (1626909)Termination phase: Saturation % 8.58/2.10 % (1626909)Time elapsed: 0.003 s % 8.58/2.10 % (1626909)Peak memory usage: 88 MB % 8.58/2.10 % (1626909)Instructions burned: 2 (million) % 8.58/2.10 % (1626897)------------------------------ % 8.58/2.10 % (1626897)------------------------------ % 8.58/2.10 % (1626914)dis+10_1_si=on:random_seed=1136941142:i=10:ep=R:rtra=on_2993 on theBenchmark for (2993ds/10Mi) % 8.58/2.10 % (1626914)Instruction limit reached! % 8.58/2.10 % (1626914)------------------------------ % 8.58/2.10 % (1626914)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.58/2.10 % (1626914)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.58/2.10 % (1626914)CaDiCaL version: 2.1.3 % 8.58/2.10 % (1626914)Termination reason: Instruction limit % 8.58/2.10 % (1626914)Termination phase: Saturation % 8.58/2.10 % (1626914)Time elapsed: 0.007 s % 8.58/2.10 % (1626914)Peak memory usage: 88 MB % 8.58/2.10 % (1626914)Instructions burned: 11 (million) % 8.58/2.10 % (1626915)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=2014622267:i=26:canc=cautious:av=off:rtra=on_2993 on theBenchmark for (2993ds/26Mi) % 8.58/2.10 % (1626915)Refutation not found, incomplete strategy % 8.58/2.10 % (1626915)------------------------------ % 8.58/2.10 % (1626915)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.58/2.10 % (1626915)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.58/2.10 % (1626915)CaDiCaL version: 2.1.3 % 8.58/2.10 % (1626915)Termination reason: Refutation not found, incomplete strategy % 8.58/2.10 % (1626915)Time elapsed: 0.002 s % 8.58/2.10 % (1626915)Peak memory usage: 88 MB % 9.74/2.33 % (1626910)Instruction limit reached! % 9.74/2.33 % (1626910)------------------------------ % 9.74/2.33 % (1626910)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.74/2.33 % (1626910)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.74/2.33 % (1626910)CaDiCaL version: 2.1.3 % 9.74/2.33 % (1626910)Termination reason: Instruction limit % 9.74/2.33 % (1626910)Termination phase: Saturation % 9.74/2.33 % (1626910)Time elapsed: 0.105 s % 9.74/2.33 % (1626910)Peak memory usage: 115 MB % 9.74/2.33 % (1626910)Instructions burned: 128 (million) % 9.74/2.33 % (1626919)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=3612163739:i=2:fsr=off:rtra=on:inst=on_2992 on theBenchmark for (2992ds/2Mi) % 9.74/2.33 % (1626919)Instruction limit reached! % 9.74/2.33 % (1626919)------------------------------ % 9.74/2.33 % (1626919)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.74/2.33 % (1626919)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.74/2.33 % (1626919)CaDiCaL version: 2.1.3 % 9.74/2.33 % (1626919)Termination reason: Instruction limit % 9.74/2.33 % (1626919)Termination phase: Saturation % 9.74/2.33 % (1626919)Time elapsed: 0.002 s % 9.74/2.33 % (1626919)Peak memory usage: 89 MB % 9.74/2.33 % (1626919)Instructions burned: 3 (million) % 9.74/2.33 % (1626916)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=4018466689: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_2993 on theBenchmark for (2993ds/35Mi) % 9.74/2.33 % (1626916)Instruction limit reached! % 9.74/2.33 % (1626916)------------------------------ % 9.74/2.33 % (1626916)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.74/2.33 % (1626916)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.74/2.33 % (1626916)CaDiCaL version: 2.1.3 % 9.74/2.33 % (1626916)Termination reason: Instruction limit % 9.74/2.33 % (1626916)Termination phase: Saturation % 9.74/2.33 % (1626916)Time elapsed: 0.027 s % 9.74/2.33 % (1626916)Peak memory usage: 89 MB % 9.74/2.33 % (1626916)Instructions burned: 35 (million) % 9.74/2.33 % (1626920)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=194870022:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2992 on theBenchmark for (2992ds/8Mi) % 9.74/2.33 % (1626920)Instruction limit reached! % 9.74/2.33 % (1626920)------------------------------ % 9.74/2.33 % (1626920)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.74/2.33 % (1626920)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.74/2.33 % (1626920)CaDiCaL version: 2.1.3 % 9.74/2.33 % (1626920)Termination reason: Instruction limit % 9.74/2.33 % (1626920)Termination phase: Saturation % 9.74/2.33 % (1626920)Time elapsed: 0.007 s % 9.74/2.33 % (1626920)Peak memory usage: 88 MB % 9.74/2.33 % (1626920)Instructions burned: 9 (million) % 9.74/2.33 % (1626921)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=189546158:i=370:ep=RS:fsr=off:rtra=on_2992 on theBenchmark for (2992ds/370Mi) % 9.74/2.33 % (1626921)Refutation not found, incomplete strategy % 9.74/2.33 % (1626921)------------------------------ % 9.74/2.33 % (1626921)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.74/2.33 % (1626921)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.74/2.33 % (1626921)CaDiCaL version: 2.1.3 % 9.74/2.33 % (1626921)Termination reason: Refutation not found, incomplete strategy % 9.74/2.33 % (1626921)Time elapsed: 0.001 s % 9.74/2.33 % (1626921)Peak memory usage: 88 MB % 9.74/2.33 % (1626928)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=1971235543:i=10:rtra=on_2991 on theBenchmark for (2991ds/10Mi) % 9.74/2.33 % (1626928)Refutation not found, incomplete strategy % 9.74/2.33 % (1626928)------------------------------ % 9.74/2.33 % (1626928)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.74/2.33 % (1626928)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.74/2.33 % (1626928)CaDiCaL version: 2.1.3 % 9.74/2.33 % (1626928)Termination reason: Refutation not found, incomplete strategy % 9.74/2.33 % (1626928)Time elapsed: 0.001 s % 9.74/2.33 % (1626928)Peak memory usage: 88 MB % 9.74/2.33 % (1626924)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=834157858:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2991 on theBenchmark for (2991ds/13Mi) % 11.96/2.71 % (1626927)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=1921449516:i=226:rtra=on:gtg=position:ss=axioms_2991 on theBenchmark for (2991ds/226Mi) % 11.96/2.71 % (1626924)Instruction limit reached! % 11.96/2.71 % (1626924)------------------------------ % 11.96/2.71 % (1626924)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.96/2.71 % (1626924)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.96/2.71 % (1626924)CaDiCaL version: 2.1.3 % 11.96/2.71 % (1626924)Termination reason: Instruction limit % 11.96/2.71 % (1626924)Termination phase: Saturation % 11.96/2.71 % (1626924)Time elapsed: 0.029 s % 11.96/2.71 % (1626924)Peak memory usage: 112 MB % 11.96/2.71 % (1626924)Instructions burned: 14 (million) % 11.96/2.71 % (1626929)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=607200730:i=71:rtra=on:gtg=exists_top_2991 on theBenchmark for (2991ds/71Mi) % 11.96/2.71 % (1626931)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=622287940:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2991 on theBenchmark for (2991ds/75Mi) % 11.96/2.71 % (1626915)------------------------------ % 11.96/2.71 % (1626915)------------------------------ % 11.96/2.71 % (1626929)Refutation not found, incomplete strategy % 11.96/2.71 % (1626929)------------------------------ % 11.96/2.71 % (1626929)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.96/2.71 % (1626929)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.96/2.71 % (1626929)CaDiCaL version: 2.1.3 % 11.96/2.71 % (1626929)Termination reason: Refutation not found, incomplete strategy % 11.96/2.71 % (1626929)Time elapsed: 0.052 s % 11.96/2.71 % (1626929)Peak memory usage: 132 MB % 11.96/2.71 % (1626929)Instructions burned: 10 (million) % 11.96/2.71 % (1626931)Instruction limit reached! % 11.96/2.71 % (1626931)------------------------------ % 11.96/2.71 % (1626931)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.96/2.71 % (1626931)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.96/2.71 % (1626931)CaDiCaL version: 2.1.3 % 11.96/2.71 % (1626931)Termination reason: Instruction limit % 11.96/2.71 % (1626931)Termination phase: Saturation % 11.96/2.71 % (1626931)Time elapsed: 0.032 s % 11.96/2.71 % (1626931)Peak memory usage: 89 MB % 11.96/2.71 % (1626931)Instructions burned: 77 (million) % 11.96/2.71 % (1626928)------------------------------ % 11.96/2.71 % (1626928)------------------------------ % 11.96/2.71 % (1626927)Instruction limit reached! % 11.96/2.71 % (1626927)------------------------------ % 11.96/2.71 % (1626927)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.96/2.71 % (1626927)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.96/2.71 % (1626927)CaDiCaL version: 2.1.3 % 11.96/2.71 % (1626927)Termination reason: Instruction limit % 11.96/2.71 % (1626927)Termination phase: Saturation % 11.96/2.71 % (1626927)Time elapsed: 0.154 s % 11.96/2.71 % (1626927)Peak memory usage: 115 MB % 11.96/2.71 % (1626927)Instructions burned: 226 (million) % 11.96/2.71 % (1626936)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=2421924154:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2990 on theBenchmark for (2990ds/294Mi) % 11.96/2.71 % (1626921)------------------------------ % 11.96/2.71 % (1626921)------------------------------ % 11.96/2.71 % (1626939)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=2588968547:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2989 on theBenchmark for (2989ds/130Mi) % 11.96/2.71 % (1626941)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=3436396521:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2989 on theBenchmark for (2989ds/40Mi) % 11.96/2.71 % (1626939)Refutation not found, incomplete strategy % 11.96/2.71 % (1626939)------------------------------ % 11.96/2.71 % (1626939)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.96/2.71 % (1626939)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.96/2.71 % (1626939)CaDiCaL version: 2.1.3 % 11.96/2.71 % (1626939)Termination reason: Refutation not found, incomplete strategy % 11.96/2.71 % (1626939)Time elapsed: 0.029 s % 11.96/2.71 % (1626939)Peak memory usage: 115 MB % 11.96/2.71 % (1626939)Instructions burned: 6 (million) % 11.96/2.71 % (1626940)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=3875035988:i=131:rtra=on_2989 on theBenchmark for (2989ds/131Mi) % 13.35/2.93 % (1626941)Instruction limit reached! % 13.35/2.93 % (1626941)------------------------------ % 13.35/2.93 % (1626941)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.35/2.93 % (1626941)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.35/2.93 % (1626941)CaDiCaL version: 2.1.3 % 13.35/2.93 % (1626941)Termination reason: Instruction limit % 13.35/2.93 % (1626941)Termination phase: Saturation % 13.35/2.93 % (1626941)Time elapsed: 0.042 s % 13.35/2.93 % (1626941)Peak memory usage: 133 MB % 13.35/2.93 % (1626941)Instructions burned: 41 (million) % 13.35/2.93 % (1626936)Instruction limit reached! % 13.35/2.93 % (1626936)------------------------------ % 13.35/2.93 % (1626936)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.35/2.93 % (1626936)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.35/2.93 % (1626936)CaDiCaL version: 2.1.3 % 13.35/2.93 % (1626936)Termination reason: Instruction limit % 13.35/2.93 % (1626936)Termination phase: Saturation % 13.35/2.93 % (1626936)Time elapsed: 0.125 s % 13.35/2.93 % (1626936)Peak memory usage: 88 MB % 13.35/2.93 % (1626936)Instructions burned: 294 (million) % 13.35/2.93 % (1626940)Refutation not found, incomplete strategy % 13.35/2.93 % (1626940)------------------------------ % 13.35/2.93 % (1626940)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.35/2.93 % (1626940)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.35/2.93 % (1626940)CaDiCaL version: 2.1.3 % 13.35/2.93 % (1626940)Termination reason: Refutation not found, incomplete strategy % 13.35/2.93 % (1626940)Time elapsed: 0.053 s % 13.35/2.93 % (1626940)Peak memory usage: 132 MB % 13.35/2.93 % (1626940)Instructions burned: 10 (million) % 13.35/2.93 % (1626942)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=1414507435:i=307:rtra=on:gtg=exists_top_2988 on theBenchmark for (2988ds/307Mi) % 13.35/2.93 % (1626929)------------------------------ % 13.35/2.93 % (1626929)------------------------------ % 13.35/2.93 % (1626944)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=1735317724:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2988 on theBenchmark for (2988ds/598Mi) % 13.35/2.93 % (1626948)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=4064602422:i=131:canc=cautious:fsr=off:rtra=on_2987 on theBenchmark for (2987ds/131Mi) % 13.35/2.93 % (1626948)Instruction limit reached! % 13.35/2.93 % (1626948)------------------------------ % 13.35/2.93 % (1626948)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.35/2.93 % (1626948)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.35/2.93 % (1626948)CaDiCaL version: 2.1.3 % 13.35/2.93 % (1626948)Termination reason: Instruction limit % 13.35/2.93 % (1626948)Termination phase: Saturation % 13.35/2.93 % (1626948)Time elapsed: 0.048 s % 13.35/2.93 % (1626948)Peak memory usage: 116 MB % 13.35/2.93 % (1626948)Instructions burned: 134 (million) % 13.35/2.93 % (1626949)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=1258138710:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2987 on theBenchmark for (2987ds/259Mi) % 13.35/2.93 % (1626942)Instruction limit reached! % 13.35/2.93 % (1626942)------------------------------ % 13.35/2.93 % (1626942)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.35/2.93 % (1626942)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.35/2.93 % (1626942)CaDiCaL version: 2.1.3 % 13.35/2.93 % (1626942)Termination reason: Instruction limit % 13.35/2.93 % (1626942)Termination phase: Saturation % 13.35/2.93 % (1626942)Time elapsed: 0.158 s % 13.35/2.93 % (1626942)Peak memory usage: 91 MB % 13.35/2.93 % (1626942)Instructions burned: 308 (million) % 13.35/2.93 % (1626949)Refutation not found, incomplete strategy % 13.35/2.93 % (1626949)------------------------------ % 13.35/2.93 % (1626949)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.35/2.93 % (1626949)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.35/2.93 % (1626949)CaDiCaL version: 2.1.3 % 13.35/2.93 % (1626949)Termination reason: Refutation not found, incomplete strategy % 13.35/2.93 % (1626949)Time elapsed: 0.028 s % 13.35/2.93 % (1626949)Peak memory usage: 115 MB % 13.35/2.93 % (1626949)Instructions burned: 6 (million) % 13.35/2.93 % (1626939)------------------------------ % 16.53/3.23 % (1626939)------------------------------ % 16.53/3.23 % (1626951)dis+10_1_si=on:random_seed=2899688479:s2a=on:i=1000:rtra=on:gtg=exists_all_2986 on theBenchmark for (2986ds/1000Mi) % 16.53/3.23 % (1626940)------------------------------ % 16.53/3.23 % (1626940)------------------------------ % 16.53/3.23 % (1626954)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=1041739307:i=383:fsr=off:rtra=on:ev=force_2985 on theBenchmark for (2985ds/383Mi) % 16.53/3.23 % (1626954)Refutation not found, incomplete strategy % 16.53/3.23 % (1626954)------------------------------ % 16.53/3.23 % (1626954)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.53/3.23 % (1626954)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.53/3.23 % (1626954)CaDiCaL version: 2.1.3 % 16.53/3.23 % (1626954)Termination reason: Refutation not found, incomplete strategy % 16.53/3.23 % (1626954)Time elapsed: 0.001 s % 16.53/3.23 % (1626954)Peak memory usage: 89 MB % 16.53/3.23 % (1626956)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=1850463573:i=141:doe=on:rtra=on_2985 on theBenchmark for (2985ds/141Mi) % 16.53/3.23 % (1626957)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=2587839439:i=65:nm=16:rtra=on_2985 on theBenchmark for (2985ds/65Mi) % 16.53/3.23 % (1626957)Refutation not found, incomplete strategy % 16.53/3.23 % (1626957)------------------------------ % 16.53/3.23 % (1626957)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.53/3.23 % (1626957)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.53/3.23 % (1626957)CaDiCaL version: 2.1.3 % 16.53/3.23 % (1626957)Termination reason: Refutation not found, incomplete strategy % 16.53/3.23 % (1626957)Time elapsed: 0.028 s % 16.53/3.23 % (1626957)Peak memory usage: 115 MB % 16.53/3.23 % (1626957)Instructions burned: 6 (million) % 16.53/3.23 % (1626954)------------------------------ % 16.53/3.23 % (1626954)------------------------------ % 16.53/3.23 % (1626956)Instruction limit reached! % 16.53/3.23 % (1626956)------------------------------ % 16.53/3.23 % (1626956)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.53/3.23 % (1626956)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.53/3.23 % (1626956)CaDiCaL version: 2.1.3 % 16.53/3.23 % (1626956)Termination reason: Instruction limit % 16.53/3.23 % (1626956)Termination phase: Saturation % 16.53/3.23 % (1626956)Time elapsed: 0.092 s % 16.53/3.23 % (1626956)Peak memory usage: 89 MB % 16.53/3.23 % (1626956)Instructions burned: 142 (million) % 16.53/3.23 % (1626949)------------------------------ % 16.53/3.23 % (1626949)------------------------------ % 16.53/3.23 % (1626944)Instruction limit reached! % 16.53/3.23 % (1626944)------------------------------ % 16.53/3.23 % (1626944)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.53/3.23 % (1626944)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.53/3.23 % (1626944)CaDiCaL version: 2.1.3 % 16.53/3.23 % (1626944)Termination reason: Instruction limit % 16.53/3.23 % (1626944)Termination phase: Saturation % 16.53/3.23 % (1626944)Time elapsed: 0.357 s % 16.53/3.23 % (1626944)Peak memory usage: 133 MB % 16.53/3.23 % (1626944)Instructions burned: 599 (million) % 16.53/3.23 % (1626960)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=1582244537:i=121:nm=16:rtra=on_2984 on theBenchmark for (2984ds/121Mi) % 16.53/3.23 % (1626960)Instruction limit reached! % 16.53/3.23 % (1626960)------------------------------ % 16.53/3.23 % (1626960)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.53/3.23 % (1626960)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.53/3.23 % (1626960)CaDiCaL version: 2.1.3 % 16.53/3.23 % (1626960)Termination reason: Instruction limit % 16.53/3.23 % (1626960)Termination phase: Saturation % 16.53/3.23 % (1626960)Time elapsed: 0.054 s % 16.53/3.23 % (1626960)Peak memory usage: 88 MB % 16.53/3.23 % (1626960)Instructions burned: 122 (million) % 16.53/3.23 % (1626963)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=3366043232:s2a=on:i=128:s2at=5:ins=3:rtra=on_2983 on theBenchmark for (2983ds/128Mi) % 16.53/3.23 % (1626964)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=2499257271:i=39:ins=3:rtra=on_2983 on theBenchmark for (2983ds/39Mi) % 16.53/3.23 % (1626966)dis+1010_1_to=kbo:si=on:random_seed=762628000:i=175:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2982 on theBenchmark for (2982ds/175Mi) % 17.09/3.51 % (1626967)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=2566944724:i=329:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2982 on theBenchmark for (2982ds/329Mi) % 17.09/3.51 % (1626963)Instruction limit reached! % 17.09/3.51 % (1626963)------------------------------ % 17.09/3.51 % (1626963)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.09/3.51 % (1626963)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.09/3.51 % (1626963)CaDiCaL version: 2.1.3 % 17.09/3.51 % (1626963)Termination reason: Instruction limit % 17.09/3.51 % (1626963)Termination phase: Saturation % 17.09/3.51 % (1626963)Time elapsed: 0.059 s % 17.09/3.51 % (1626963)Peak memory usage: 117 MB % 17.09/3.51 % (1626963)Instructions burned: 131 (million) % 17.09/3.51 % (1626964)Instruction limit reached! % 17.09/3.51 % (1626964)------------------------------ % 17.09/3.51 % (1626964)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.09/3.51 % (1626964)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.09/3.51 % (1626964)CaDiCaL version: 2.1.3 % 17.09/3.51 % (1626964)Termination reason: Instruction limit % 17.09/3.51 % (1626964)Termination phase: Saturation % 17.09/3.51 % (1626964)Time elapsed: 0.047 s % 17.09/3.51 % (1626964)Peak memory usage: 115 MB % 17.09/3.51 % (1626964)Instructions burned: 40 (million) % 17.09/3.51 % (1626957)------------------------------ % 17.09/3.51 % (1626957)------------------------------ % 17.09/3.51 % (1626968)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=2980127165:s2a=on:i=483:doe=on:nm=32:rtra=on_2982 on theBenchmark for (2982ds/483Mi) % 17.09/3.51 % (1626973)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=925437630:thitd=on:i=215:nm=0:rtra=on:ev=force_2981 on theBenchmark for (2981ds/215Mi) % 17.09/3.51 % (1626968)Refutation not found, incomplete strategy % 17.09/3.51 % (1626968)------------------------------ % 17.09/3.51 % (1626968)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.09/3.51 % (1626968)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.09/3.51 % (1626968)CaDiCaL version: 2.1.3 % 17.09/3.51 % (1626968)Termination reason: Refutation not found, incomplete strategy % 17.09/3.51 % (1626968)Time elapsed: 0.052 s % 17.09/3.51 % (1626968)Peak memory usage: 132 MB % 17.09/3.51 % (1626968)Instructions burned: 10 (million) % 17.09/3.51 % (1626966)Instruction limit reached! % 17.09/3.51 % (1626966)------------------------------ % 17.09/3.51 % (1626966)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.09/3.51 % (1626966)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.09/3.51 % (1626966)CaDiCaL version: 2.1.3 % 17.09/3.51 % (1626966)Termination reason: Instruction limit % 17.09/3.51 % (1626966)Termination phase: Saturation % 17.09/3.51 % (1626966)Time elapsed: 0.132 s % 17.09/3.51 % (1626966)Peak memory usage: 90 MB % 17.09/3.51 % (1626966)Instructions burned: 175 (million) % 17.09/3.51 % (1626967)Instruction limit reached! % 17.09/3.51 % (1626967)------------------------------ % 17.09/3.51 % (1626967)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.09/3.51 % (1626967)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.09/3.51 % (1626967)CaDiCaL version: 2.1.3 % 17.09/3.51 % (1626967)Termination reason: Instruction limit % 17.09/3.51 % (1626967)Termination phase: Saturation % 17.09/3.51 % (1626967)Time elapsed: 0.156 s % 17.09/3.51 % (1626967)Peak memory usage: 112 MB % 17.09/3.51 % (1626967)Instructions burned: 329 (million) % 17.09/3.51 % (1626973)Refutation not found, incomplete strategy % 17.09/3.51 % (1626973)------------------------------ % 17.09/3.51 % (1626973)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.09/3.51 % (1626973)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.09/3.51 % (1626973)CaDiCaL version: 2.1.3 % 17.09/3.51 % (1626973)Termination reason: Refutation not found, incomplete strategy % 17.09/3.51 % (1626973)Time elapsed: 0.036 s % 17.09/3.51 % (1626973)Peak memory usage: 133 MB % 17.09/3.51 % (1626973)Instructions burned: 16 (million) % 17.09/3.51 % (1626974)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=941896126:i=349:rtra=on_2981 on theBenchmark for (2981ds/349Mi) % 17.09/3.51 % (1626974)Refutation not found, incomplete strategy % 19.43/3.80 % (1626974)------------------------------ % 19.43/3.80 % (1626974)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.43/3.80 % (1626974)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.43/3.80 % (1626974)CaDiCaL version: 2.1.3 % 19.43/3.80 % (1626974)Termination reason: Refutation not found, incomplete strategy % 19.43/3.80 % (1626974)Time elapsed: 0.028 s % 19.43/3.80 % (1626974)Peak memory usage: 115 MB % 19.43/3.80 % (1626974)Instructions burned: 6 (million) % 19.43/3.80 % (1626975)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=3958274029:st=2:i=295:rtra=on:ss=axioms_2980 on theBenchmark for (2980ds/295Mi) % 19.43/3.80 % (1626951)Instruction limit reached! % 19.43/3.80 % (1626951)------------------------------ % 19.43/3.80 % (1626951)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.43/3.80 % (1626951)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.43/3.80 % (1626951)CaDiCaL version: 2.1.3 % 19.43/3.80 % (1626951)Termination reason: Instruction limit % 19.43/3.80 % (1626951)Termination phase: Saturation % 19.43/3.80 % (1626951)Time elapsed: 0.613 s % 19.43/3.80 % (1626951)Peak memory usage: 94 MB % 19.43/3.80 % (1626951)Instructions burned: 1001 (million) % 19.43/3.80 % (1626978)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=706824988:i=328:kws=inv_frequency:nm=20:rtra=on_2980 on theBenchmark for (2980ds/328Mi) % 19.43/3.80 % (1626973)------------------------------ % 19.43/3.80 % (1626973)------------------------------ % 19.43/3.80 % (1626979)dis+1010_1_to=lpo:sil=128000:sas=z3:si=on:nwc=5:random_seed=2325670019:i=281:gtgl=2:rtra=on:gtg=all_2979 on theBenchmark for (2979ds/281Mi) % 19.43/3.80 % (1626968)------------------------------ % 19.43/3.80 % (1626968)------------------------------ % 19.43/3.80 % (1626975)Instruction limit reached! % 19.43/3.80 % (1626975)------------------------------ % 19.43/3.80 % (1626975)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.43/3.80 % (1626975)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.43/3.80 % (1626975)CaDiCaL version: 2.1.3 % 19.43/3.80 % (1626975)Termination reason: Instruction limit % 19.43/3.80 % (1626975)Termination phase: Saturation % 19.43/3.80 % (1626975)Time elapsed: 0.166 s % 19.43/3.80 % (1626975)Peak memory usage: 90 MB % 19.43/3.80 % (1626975)Instructions burned: 296 (million) % 19.43/3.80 % (1626982)lrs+1010_1_to=kbo:sil=128000:si=on:sos=on:urr=on:uwa=alasca_main:random_seed=288554435:i=484:doe=on:nm=0:av=off:rtra=on:ss=axioms_2978 on theBenchmark for (2978ds/484Mi) % 19.43/3.80 % (1626984)lrs+21_1_to=kbo:sil=128000:thi=neg_eq:si=on:random_seed=2414987197:i=321:canc=force:rtra=on:tac=axiom:ss=axioms:ev=force_2978 on theBenchmark for (2978ds/321Mi) % 19.43/3.80 % (1626974)------------------------------ % 19.43/3.80 % (1626974)------------------------------ % 19.43/3.80 % (1626978)Instruction limit reached! % 19.43/3.80 % (1626978)------------------------------ % 19.43/3.80 % (1626978)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.43/3.80 % (1626978)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.43/3.80 % (1626978)CaDiCaL version: 2.1.3 % 19.43/3.80 % (1626978)Termination reason: Instruction limit % 19.43/3.80 % (1626978)Termination phase: Saturation % 19.43/3.80 % (1626978)Time elapsed: 0.222 s % 19.43/3.80 % (1626978)Peak memory usage: 117 MB % 19.43/3.80 % (1626978)Instructions burned: 328 (million) % 19.43/3.80 % (1626979)Instruction limit reached! % 19.43/3.80 % (1626979)------------------------------ % 19.43/3.80 % (1626979)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.43/3.80 % (1626979)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.43/3.80 % (1626979)CaDiCaL version: 2.1.3 % 19.43/3.80 % (1626979)Termination reason: Instruction limit % 19.43/3.80 % (1626979)Termination phase: Saturation % 19.43/3.80 % (1626979)Time elapsed: 0.196 s % 19.43/3.80 % (1626979)Peak memory usage: 117 MB % 19.43/3.80 % (1626979)Instructions burned: 282 (million) % 19.43/3.80 % (1626984)Instruction limit reached! % 19.43/3.80 % (1626984)------------------------------ % 19.43/3.80 % (1626984)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.43/3.80 % (1626984)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.43/3.80 % (1626984)CaDiCaL version: 2.1.3 % 19.43/3.80 % (1626984)Termination reason: Instruction limit % 19.43/3.80 % (1626984)Termination phase: Saturation % 19.43/3.80 % (1626984)Time elapsed: 0.085 s % 22.72/4.05 % (1626984)Peak memory usage: 114 MB % 22.72/4.05 % (1626984)Instructions burned: 323 (million) % 22.72/4.05 % (1626986)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=1153957364:i=416:rtra=on:gtg=position:ss=axioms_2977 on theBenchmark for (2977ds/416Mi) % 22.72/4.05 % (1626987)lrs+1010_1_to=kbo:tgt=ground:fde=unused:sas=z3:si=on:sp=unary_frequency:gve=force:spb=goal:tha=off:random_seed=2545910298:i=471:thf=on:kws=precedence:rtra=on_2977 on theBenchmark for (2977ds/471Mi) % 22.72/4.05 % (1626987)Refutation not found, incomplete strategy % 22.72/4.05 % (1626987)------------------------------ % 22.72/4.05 % (1626987)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 22.72/4.05 % (1626987)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.72/4.05 % (1626987)CaDiCaL version: 2.1.3 % 22.72/4.05 % (1626987)Termination reason: Refutation not found, incomplete strategy % 22.72/4.05 % (1626987)Time elapsed: 0.029 s % 22.72/4.05 % (1626987)Peak memory usage: 116 MB % 22.72/4.05 % (1626987)Instructions burned: 6 (million) % 22.72/4.05 % (1626990)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=2614583815:avsq=on:i=276:avsqr=1,2:rtra=on_2976 on theBenchmark for (2976ds/276Mi) % 22.72/4.05 % (1626993)lrs+10_1_to=kbo:sil=128000:fde=none:si=on:norm_ineq=on:urr=on:nwc=0.5:random_seed=3690538965:i=513:kws=frequency:bd=all:rtra=on:gtg=exists_all:ss=axioms:sgt=4_2976 on theBenchmark for (2976ds/513Mi) % 22.72/4.05 % (1626991)lrs+1010_2_to=kbo:sil=128000:tgt=ground:fde=unused:sas=z3:si=on:uwa=off:tha=off:nwc=1:random_seed=2808238787:i=375:kws=inv_arity_squared:rtra=on_2976 on theBenchmark for (2976ds/375Mi) % 22.72/4.05 % (1626992)lrs+10_1_to=kbo:sil=128000:tgt=full:sas=z3:si=on:uwa=func_ext:slsqc=1:flr=on:slsq=on:random_seed=2121321754:i=387:bd=preordered:rtra=on:ss=axioms:sgt=8_2976 on theBenchmark for (2976ds/387Mi) % 22.72/4.05 % (1626991)Refutation not found, incomplete strategy % 22.72/4.05 % (1626991)------------------------------ % 22.72/4.05 % (1626991)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 22.72/4.05 % (1626991)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.72/4.05 % (1626991)CaDiCaL version: 2.1.3 % 22.72/4.05 % (1626991)Termination reason: Refutation not found, incomplete strategy % 22.72/4.05 % (1626991)Time elapsed: 0.028 s % 22.72/4.05 % (1626991)Peak memory usage: 115 MB % 22.72/4.05 % (1626991)Instructions burned: 6 (million) % 22.72/4.05 % (1626982)Instruction limit reached! % 22.72/4.05 % (1626982)------------------------------ % 22.72/4.05 % (1626982)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 22.72/4.05 % (1626982)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.72/4.05 % (1626982)CaDiCaL version: 2.1.3 % 22.72/4.05 % (1626982)Termination reason: Instruction limit % 22.72/4.05 % (1626982)Termination phase: Saturation % 22.72/4.05 % (1626982)Time elapsed: 0.292 s % 22.72/4.05 % (1626982)Peak memory usage: 94 MB % 22.72/4.05 % (1626982)Instructions burned: 484 (million) % 22.72/4.05 % (1626986)Instruction limit reached! % 22.72/4.05 % (1626986)------------------------------ % 22.72/4.05 % (1626986)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 22.72/4.05 % (1626986)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.72/4.05 % (1626986)CaDiCaL version: 2.1.3 % 22.72/4.05 % (1626986)Termination reason: Instruction limit % 22.72/4.05 % (1626986)Termination phase: Saturation % 22.72/4.05 % (1626986)Time elapsed: 0.244 s % 22.72/4.05 % (1626986)Peak memory usage: 116 MB % 22.72/4.05 % (1626986)Instructions burned: 416 (million) % 22.72/4.05 % (1626990)Instruction limit reached! % 22.72/4.05 % (1626990)------------------------------ % 22.72/4.05 % (1626990)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 22.72/4.05 % (1626990)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.72/4.05 % (1626990)CaDiCaL version: 2.1.3 % 22.72/4.05 % (1626990)Termination reason: Instruction limit % 22.72/4.05 % (1626990)Termination phase: Saturation % 22.72/4.05 % (1626990)Time elapsed: 0.159 s % 22.72/4.05 % (1626990)Peak memory usage: 132 MB % 22.72/4.05 % (1626990)Instructions burned: 276 (million) % 22.72/4.05 % (1626993)Instruction limit reached! % 22.72/4.05 % (1626993)------------------------------ % 22.72/4.05 % (1626993)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 22.72/4.05 % (1626993)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.82/4.40 % (1626993)CaDiCaL version: 2.1.3 % 24.82/4.40 % (1626993)Termination reason: Instruction limit % 24.82/4.40 % (1626993)Termination phase: Saturation % 24.82/4.40 % (1626993)Time elapsed: 0.166 s % 24.82/4.40 % (1626993)Peak memory usage: 92 MB % 24.82/4.40 % (1626993)Instructions burned: 515 (million) % 24.82/4.40 % (1626987)------------------------------ % 24.82/4.40 % (1626987)------------------------------ % 24.82/4.40 % (1627000)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=3602566219:i=334:rtra=on_2974 on theBenchmark for (2974ds/334Mi) % 24.82/4.40 % (1627003)lrs-2_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_max:tha=off:random_seed=266394435:st=1.5:i=261:sd=1:kws=precedence:rtra=on:ss=axioms_2973 on theBenchmark for (2973ds/261Mi) % 24.82/4.40 % (1627001)lrs+1010_1_to=kbo:sil=64000:sas=cadical:si=on:sos=on:bce=on:random_seed=901672975:i=359:rtra=on:gtg=exists_top:ss=axioms_2973 on theBenchmark for (2973ds/359Mi) % 24.82/4.40 % (1627002)dis+1010_1_to=lpo:sil=128000:thi=all:fde=unused:si=on:sp=reverse_arity:tha=off:random_seed=399102779:i=341:gtgl=2:rtra=on:gtg=exists_sym:ev=force:fsd=on:fsdmm=1_2973 on theBenchmark for (2973ds/341Mi) % 24.82/4.40 % (1627000)Refutation not found, incomplete strategy % 24.82/4.40 % (1627000)------------------------------ % 24.82/4.40 % (1627000)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.82/4.40 % (1627000)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.82/4.40 % (1627000)CaDiCaL version: 2.1.3 % 24.82/4.40 % (1627000)Termination reason: Refutation not found, incomplete strategy % 24.82/4.40 % (1627000)Time elapsed: 0.053 s % 24.82/4.40 % (1627000)Peak memory usage: 132 MB % 24.82/4.40 % (1627000)Instructions burned: 10 (million) % 24.82/4.40 % (1627003)Refutation not found, incomplete strategy % 24.82/4.40 % (1627003)------------------------------ % 24.82/4.40 % (1627003)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.82/4.40 % (1627003)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.82/4.40 % (1627003)CaDiCaL version: 2.1.3 % 24.82/4.40 % (1627003)Termination reason: Refutation not found, incomplete strategy % 24.82/4.40 % (1627003)Time elapsed: 0.018 s % 24.82/4.40 % (1627003)Peak memory usage: 115 MB % 24.82/4.40 % (1627003)Instructions burned: 6 (million) % 24.82/4.40 % (1627002)Refutation not found, incomplete strategy % 24.82/4.40 % (1627002)------------------------------ % 24.82/4.40 % (1627002)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.82/4.40 % (1627002)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.82/4.40 % (1627002)CaDiCaL version: 2.1.3 % 24.82/4.40 % (1627002)Termination reason: Refutation not found, incomplete strategy % 24.82/4.40 % (1627002)Time elapsed: 0.027 s % 24.82/4.40 % (1627002)Peak memory usage: 112 MB % 24.82/4.40 % (1627002)Instructions burned: 5 (million) % 24.82/4.40 % (1626991)------------------------------ % 24.82/4.40 % (1626991)------------------------------ % 24.82/4.40 % (1626992)Instruction limit reached! % 24.82/4.40 % (1626992)------------------------------ % 24.82/4.40 % (1626992)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.82/4.40 % (1626992)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.82/4.40 % (1626992)CaDiCaL version: 2.1.3 % 24.82/4.40 % (1626992)Termination reason: Instruction limit % 24.82/4.40 % (1626992)Termination phase: Saturation % 24.82/4.40 % (1626992)Time elapsed: 0.274 s % 24.82/4.40 % (1626992)Peak memory usage: 118 MB % 24.82/4.40 % (1626992)Instructions burned: 387 (million) % 24.82/4.40 % (1627004)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=939862622:s2pl=no:i=235:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2973 on theBenchmark for (2973ds/235Mi) % 24.82/4.40 % (1627004)Refutation not found, incomplete strategy % 24.82/4.40 % (1627004)------------------------------ % 24.82/4.40 % (1627004)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.82/4.40 % (1627004)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.82/4.40 % (1627004)CaDiCaL version: 2.1.3 % 24.82/4.40 % (1627004)Termination reason: Refutation not found, incomplete strategy % 24.82/4.40 % (1627004)Time elapsed: 0.028 s % 24.82/4.40 % (1627004)Peak memory usage: 115 MB % 24.82/4.40 % (1627004)Instructions burned: 6 (million) % 24.82/4.40 % (1627003)------------------------------ % 24.82/4.40 % (1627003)------------------------------ % 27.65/4.93 % (1627009)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=1688275889:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2971 on theBenchmark for (2971ds/273Mi) % 27.65/4.93 % (1627010)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=1623017256:i=146:doe=on:rtra=on_2971 on theBenchmark for (2971ds/146Mi) % 27.65/4.93 % (1627001)Instruction limit reached! % 27.65/4.93 % (1627001)------------------------------ % 27.65/4.93 % (1627001)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.65/4.93 % (1627001)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.65/4.93 % (1627001)CaDiCaL version: 2.1.3 % 27.65/4.93 % (1627001)Termination reason: Instruction limit % 27.65/4.93 % (1627001)Termination phase: Saturation % 27.65/4.93 % (1627001)Time elapsed: 0.195 s % 27.65/4.93 % (1627001)Peak memory usage: 90 MB % 27.65/4.93 % (1627001)Instructions burned: 360 (million) % 27.65/4.93 % (1627000)------------------------------ % 27.65/4.93 % (1627000)------------------------------ % 27.65/4.93 % (1627002)------------------------------ % 27.65/4.93 % (1627002)------------------------------ % 27.65/4.93 % (1627009)Instruction limit reached! % 27.65/4.93 % (1627009)------------------------------ % 27.65/4.93 % (1627009)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.65/4.93 % (1627009)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.65/4.93 % (1627009)CaDiCaL version: 2.1.3 % 27.65/4.93 % (1627009)Termination reason: Instruction limit % 27.65/4.93 % (1627009)Termination phase: Saturation % 27.65/4.93 % (1627009)Time elapsed: 0.090 s % 27.65/4.93 % (1627009)Peak memory usage: 91 MB % 27.65/4.93 % (1627009)Instructions burned: 274 (million) % 27.65/4.93 % (1627010)Instruction limit reached! % 27.65/4.93 % (1627010)------------------------------ % 27.65/4.93 % (1627010)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.65/4.93 % (1627010)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.65/4.93 % (1627010)CaDiCaL version: 2.1.3 % 27.65/4.93 % (1627010)Termination reason: Instruction limit % 27.65/4.93 % (1627010)Termination phase: Saturation % 27.65/4.93 % (1627010)Time elapsed: 0.094 s % 27.65/4.93 % (1627010)Peak memory usage: 89 MB % 27.65/4.93 % (1627010)Instructions burned: 147 (million) % 27.65/4.93 % (1627012)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=244339709:i=4428:doe=on:fsr=off:rtra=on_2970 on theBenchmark for (2970ds/4428Mi) % 27.65/4.93 % (1627004)------------------------------ % 27.65/4.93 % (1627004)------------------------------ % 27.65/4.93 % (1627015)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=2827190391:avsq=on:i=276:avsqr=1,2:rtra=on_2970 on theBenchmark for (2970ds/276Mi) % 27.65/4.93 % (1627018)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=1984879971:st=5:i=1054:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2969 on theBenchmark for (2969ds/1054Mi) % 27.65/4.93 % (1627018)Refutation not found, incomplete strategy % 27.65/4.93 % (1627018)------------------------------ % 27.65/4.93 % (1627018)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.65/4.93 % (1627018)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.65/4.93 % (1627018)CaDiCaL version: 2.1.3 % 27.65/4.93 % (1627018)Termination reason: Refutation not found, incomplete strategy % 27.65/4.93 % (1627018)Time elapsed: 0.001 s % 27.65/4.93 % (1627018)Peak memory usage: 89 MB % 27.65/4.93 % (1627016)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=2726881225:i=1052:rtra=on_2969 on theBenchmark for (2969ds/1052Mi) % 27.65/4.93 % (1627017)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=538985018:i=655:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2969 on theBenchmark for (2969ds/655Mi) % 27.65/4.93 % (1627017)Refutation not found, incomplete strategy % 27.65/4.93 % (1627017)------------------------------ % 27.65/4.93 % (1627017)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.65/4.93 % (1627017)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.65/4.93 % (1627017)CaDiCaL version: 2.1.3 % 27.65/4.93 % (1627017)Termination reason: Refutation not found, incomplete strategy % 27.65/4.93 % (1627017)Time elapsed: 0.002 s % 27.65/4.93 % (1627017)Peak memory usage: 89 MB % 30.51/5.32 % (1627019)lrs-1002_1_to=kbo:sas=z3:si=on:norm_ineq=on:sos=on:tha=some:random_seed=754699083:i=107:rtra=on_2969 on theBenchmark for (2969ds/107Mi) % 30.51/5.32 % (1627019)Refutation not found, incomplete strategy % 30.51/5.32 % (1627019)------------------------------ % 30.51/5.32 % (1627019)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 30.51/5.32 % (1627019)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.51/5.32 % (1627019)CaDiCaL version: 2.1.3 % 30.51/5.32 % (1627019)Termination reason: Refutation not found, incomplete strategy % 30.51/5.32 % (1627019)Time elapsed: 0.029 s % 30.51/5.32 % (1627019)Peak memory usage: 115 MB % 30.51/5.32 % (1627019)Instructions burned: 6 (million) % 30.51/5.32 % (1627021)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=1769607294:s2a=on:i=450:doe=on:nm=32:rtra=on_2968 on theBenchmark for (2968ds/450Mi) % 30.51/5.32 % (1627015)Instruction limit reached! % 30.51/5.32 % (1627015)------------------------------ % 30.51/5.32 % (1627015)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 30.51/5.32 % (1627015)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.51/5.32 % (1627015)CaDiCaL version: 2.1.3 % 30.51/5.32 % (1627015)Termination reason: Instruction limit % 30.51/5.32 % (1627015)Termination phase: Saturation % 30.51/5.32 % (1627015)Time elapsed: 0.161 s % 30.51/5.32 % (1627015)Peak memory usage: 132 MB % 30.51/5.32 % (1627015)Instructions burned: 278 (million) % 30.51/5.32 % (1627018)------------------------------ % 30.51/5.32 % (1627018)------------------------------ % 30.51/5.32 % (1627021)Refutation not found, incomplete strategy % 30.51/5.32 % (1627021)------------------------------ % 30.51/5.32 % (1627021)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 30.51/5.32 % (1627021)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.51/5.32 % (1627021)CaDiCaL version: 2.1.3 % 30.51/5.32 % (1627021)Termination reason: Refutation not found, incomplete strategy % 30.51/5.32 % (1627021)Time elapsed: 0.053 s % 30.51/5.32 % (1627021)Peak memory usage: 132 MB % 30.51/5.32 % (1627021)Instructions burned: 10 (million) % 30.51/5.32 % (1627017)------------------------------ % 30.51/5.32 % (1627017)------------------------------ % 30.51/5.32 % (1627028)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 % 30.51/5.32 % (1627029)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=3458793074:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2966 on theBenchmark for (2966ds/130Mi) % 30.51/5.32 % (1627028)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=322525090:i=1090:aac=none:nm=0:rtra=on:rawr=on_2967 on theBenchmark for (2967ds/1090Mi) % 30.51/5.32 % (1627029)Refutation not found, incomplete strategy % 30.51/5.32 % (1627029)------------------------------ % 30.51/5.32 % (1627029)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 30.51/5.32 % (1627029)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.51/5.32 % (1627029)CaDiCaL version: 2.1.3 % 30.51/5.32 % (1627029)Termination reason: Refutation not found, incomplete strategy % 30.51/5.32 % (1627029)Time elapsed: 0.018 s % 30.51/5.32 % (1627029)Peak memory usage: 115 MB % 30.51/5.32 % (1627029)Instructions burned: 6 (million) % 30.51/5.32 % (1627028)Refutation not found, incomplete strategy % 30.51/5.32 % (1627028)------------------------------ % 30.51/5.32 % (1627028)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 30.51/5.32 % (1627028)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.51/5.32 % (1627028)CaDiCaL version: 2.1.3 % 30.51/5.32 % (1627028)Termination reason: Refutation not found, incomplete strategy % 30.51/5.32 % (1627028)Time elapsed: 0.028 s % 30.51/5.32 % (1627028)Peak memory usage: 115 MB % 30.51/5.32 % (1627028)Instructions burned: 6 (million) % 30.51/5.32 % (1627019)------------------------------ % 30.51/5.32 % (1627019)------------------------------ % 30.51/5.32 % (1627016)Instruction limit reached! % 30.51/5.32 % (1627016)------------------------------ % 30.51/5.32 % (1627016)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 30.51/5.32 % (1627016)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.51/5.32 % (1627016)CaDiCaL version: 2.1.3 % 32.90/5.79 % (1627016)Termination reason: Instruction limit % 32.90/5.79 % (1627016)Termination phase: Saturation % 32.90/5.79 % (1627016)Time elapsed: 0.377 s % 32.90/5.79 % (1627016)Peak memory usage: 88 MB % 32.90/5.79 % (1627016)Instructions burned: 1054 (million) % 32.90/5.79 % (1627021)------------------------------ % 32.90/5.79 % (1627021)------------------------------ % 32.90/5.79 % (1627032)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=668432077:i=312:kws=inv_frequency:nm=20:rtra=on_2965 on theBenchmark for (2965ds/312Mi) % 32.90/5.79 % (1627029)------------------------------ % 32.90/5.79 % (1627029)------------------------------ % 32.90/5.79 % (1627033)ott+10_1_to=kbo:sil=64000:si=on:sp=reverse_frequency:sos=on:random_seed=175569508:i=491:doe=on:rtra=on:gtg=position_2964 on theBenchmark for (2964ds/491Mi) % 32.90/5.79 % (1627034)ott+1011_4:1_to=lpo:sil=64000:si=on:spb=intro:random_seed=771088264:s2a=on:i=835:s2at=2:rtra=on_2964 on theBenchmark for (2964ds/835Mi) % 32.90/5.79 % (1627028)------------------------------ % 32.90/5.79 % (1627028)------------------------------ % 32.90/5.79 % (1627037)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=3925758484:i=776:doe=on:rtra=on_2963 on theBenchmark for (2963ds/776Mi) % 32.90/5.79 % (1627036)ott+1011_2_to=lpo:sil=128000:si=on:sos=on:random_seed=3318354743:i=307:bd=preordered:av=off:rtra=on:ev=cautious_2964 on theBenchmark for (2964ds/307Mi) % 32.90/5.79 % (1627032)Instruction limit reached! % 32.90/5.79 % (1627032)------------------------------ % 32.90/5.79 % (1627032)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.90/5.79 % (1627032)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.90/5.79 % (1627032)CaDiCaL version: 2.1.3 % 32.90/5.79 % (1627032)Termination reason: Instruction limit % 32.90/5.79 % (1627032)Termination phase: Saturation % 32.90/5.79 % (1627032)Time elapsed: 0.209 s % 32.90/5.79 % (1627032)Peak memory usage: 117 MB % 32.90/5.79 % (1627032)Instructions burned: 312 (million) % 32.90/5.79 % (1627040)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=148958394:s2a=on:i=646:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2962 on theBenchmark for (2962ds/646Mi) % 32.90/5.79 % (1627036)Instruction limit reached! % 32.90/5.79 % (1627036)------------------------------ % 32.90/5.79 % (1627036)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.90/5.79 % (1627036)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.90/5.79 % (1627036)CaDiCaL version: 2.1.3 % 32.90/5.79 % (1627036)Termination reason: Instruction limit % 32.90/5.79 % (1627036)Termination phase: Saturation % 32.90/5.79 % (1627036)Time elapsed: 0.195 s % 32.90/5.79 % (1627036)Peak memory usage: 94 MB % 32.90/5.79 % (1627036)Instructions burned: 309 (million) % 32.90/5.79 % (1627033)Instruction limit reached! % 32.90/5.79 % (1627033)------------------------------ % 32.90/5.79 % (1627033)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.90/5.79 % (1627033)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.90/5.79 % (1627033)CaDiCaL version: 2.1.3 % 32.90/5.79 % (1627033)Termination reason: Instruction limit % 32.90/5.79 % (1627033)Termination phase: Saturation % 32.90/5.79 % (1627033)Time elapsed: 0.288 s % 32.90/5.79 % (1627033)Peak memory usage: 92 MB % 32.90/5.79 % (1627033)Instructions burned: 493 (million) % 32.90/5.79 % (1627037)Instruction limit reached! % 32.90/5.79 % (1627037)------------------------------ % 32.90/5.79 % (1627037)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.90/5.79 % (1627037)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.90/5.79 % (1627037)CaDiCaL version: 2.1.3 % 32.90/5.79 % (1627037)Termination reason: Instruction limit % 32.90/5.79 % (1627037)Termination phase: Saturation % 32.90/5.79 % (1627037)Time elapsed: 0.227 s % 32.90/5.79 % (1627037)Peak memory usage: 117 MB % 32.90/5.79 % (1627037)Instructions burned: 776 (million) % 32.90/5.79 % (1627043)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=740052920:thitd=on:cond=fast:i=784:nm=30:rtra=on:gtg=all:tac=axiom_2961 on theBenchmark for (2961ds/784Mi) % 32.90/5.79 % (1627045)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=3085754383:thitd=on:s2a=on:i=1131:add=on:canc=force:bd=all:rtra=on:tac=axiom:ev=off_2960 on theBenchmark for (2960ds/1131Mi) % 32.90/5.79 % (1627047)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=1852128566:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2960 on theBenchmark for (2960ds/775Mi) % 39.95/6.51 % (1627046)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=1137335614:s2pl=no:i=246:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2960 on theBenchmark for (2960ds/246Mi) % 39.95/6.51 % (1627046)Refutation not found, incomplete strategy % 39.95/6.51 % (1627046)------------------------------ % 39.95/6.51 % (1627046)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.95/6.51 % (1627046)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.95/6.51 % (1627046)CaDiCaL version: 2.1.3 % 39.95/6.51 % (1627046)Termination reason: Refutation not found, incomplete strategy % 39.95/6.51 % (1627046)Time elapsed: 0.027 s % 39.95/6.51 % (1627046)Peak memory usage: 115 MB % 39.95/6.51 % (1627046)Instructions burned: 6 (million) % 39.95/6.51 % (1627034)Instruction limit reached! % 39.95/6.51 % (1627034)------------------------------ % 39.95/6.51 % (1627034)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.95/6.51 % (1627034)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.95/6.51 % (1627034)CaDiCaL version: 2.1.3 % 39.95/6.51 % (1627034)Termination reason: Instruction limit % 39.95/6.51 % (1627034)Termination phase: Saturation % 39.95/6.51 % (1627034)Time elapsed: 0.435 s % 39.95/6.51 % (1627034)Peak memory usage: 92 MB % 39.95/6.51 % (1627034)Instructions burned: 835 (million) % 39.95/6.51 % (1627040)Instruction limit reached! % 39.95/6.51 % (1627040)------------------------------ % 39.95/6.51 % (1627040)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.95/6.51 % (1627040)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.95/6.51 % (1627040)CaDiCaL version: 2.1.3 % 39.95/6.51 % (1627040)Termination reason: Instruction limit % 39.95/6.51 % (1627040)Termination phase: Saturation % 39.95/6.51 % (1627040)Time elapsed: 0.376 s % 39.95/6.51 % (1627040)Peak memory usage: 133 MB % 39.95/6.51 % (1627040)Instructions burned: 648 (million) % 39.95/6.51 % (1627052)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=394331051:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2958 on theBenchmark for (2958ds/273Mi) % 39.95/6.51 % (1627046)------------------------------ % 39.95/6.51 % (1627046)------------------------------ % 39.95/6.51 % (1627047)Instruction limit reached! % 39.95/6.51 % (1627047)------------------------------ % 39.95/6.51 % (1627047)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.95/6.51 % (1627047)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.95/6.51 % (1627047)CaDiCaL version: 2.1.3 % 39.95/6.51 % (1627047)Termination reason: Instruction limit % 39.95/6.51 % (1627047)Termination phase: Saturation % 39.95/6.51 % (1627047)Time elapsed: 0.270 s % 39.95/6.51 % (1627047)Peak memory usage: 95 MB % 39.95/6.51 % (1627047)Instructions burned: 775 (million) % 39.95/6.51 % (1627053)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=799762222:i=102:nm=16:rtra=on_2957 on theBenchmark for (2957ds/102Mi) % 39.95/6.51 % (1627043)Instruction limit reached! % 39.95/6.51 % (1627043)------------------------------ % 39.95/6.51 % (1627043)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.95/6.51 % (1627043)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.95/6.51 % (1627043)CaDiCaL version: 2.1.3 % 39.95/6.51 % (1627043)Termination reason: Instruction limit % 39.95/6.51 % (1627043)Termination phase: Saturation % 39.95/6.51 % (1627043)Time elapsed: 0.451 s % 39.95/6.51 % (1627043)Peak memory usage: 115 MB % 39.95/6.51 % (1627043)Instructions burned: 785 (million) % 39.95/6.51 % (1627055)lrs+10_1_to=lpo:sil=128000:si=on:bsr=unit_only:tha=off:random_seed=30005737:avsq=on:s2a=on:i=1094:s2at=5:avsqr=4463,131072:rtra=on_2956 on theBenchmark for (2956ds/1094Mi) % 39.95/6.51 % (1627055)Refutation not found, incomplete strategy % 39.95/6.51 % (1627055)------------------------------ % 39.95/6.51 % (1627055)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.95/6.51 % (1627055)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.95/6.51 % (1627055)CaDiCaL version: 2.1.3 % 39.95/6.51 % (1627055)Termination reason: Refutation not found, incomplete strategy % 39.95/6.51 % (1627055)Time elapsed: 0.001 s % 39.95/6.51 % (1627055)Peak memory usage: 88 MB % 48.03/7.79 % (1627053)Instruction limit reached! % 48.03/7.79 % (1627053)------------------------------ % 48.03/7.79 % (1627053)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.03/7.79 % (1627053)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.03/7.79 % (1627053)CaDiCaL version: 2.1.3 % 48.03/7.79 % (1627053)Termination reason: Instruction limit % 48.03/7.79 % (1627053)Termination phase: Saturation % 48.03/7.79 % (1627053)Time elapsed: 0.045 s % 48.03/7.79 % (1627053)Peak memory usage: 88 MB % 48.03/7.79 % (1627053)Instructions burned: 102 (million) % 48.03/7.79 % (1627052)Instruction limit reached! % 48.03/7.79 % (1627052)------------------------------ % 48.03/7.79 % (1627052)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.03/7.79 % (1627052)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.03/7.79 % (1627052)CaDiCaL version: 2.1.3 % 48.03/7.79 % (1627052)Termination reason: Instruction limit % 48.03/7.79 % (1627052)Termination phase: Saturation % 48.03/7.79 % (1627052)Time elapsed: 0.171 s % 48.03/7.79 % (1627052)Peak memory usage: 92 MB % 48.03/7.79 % (1627052)Instructions burned: 274 (million) % 48.03/7.79 % (1627056)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=132753075:i=6400:doe=on:fsr=off:rtra=on_2956 on theBenchmark for (2956ds/6400Mi) % 48.03/7.79 % (1627058)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=3842266389:i=868:doe=on:nm=0:rtra=on:gtg=exists_sym_2955 on theBenchmark for (2955ds/868Mi) % 48.03/7.79 % (1627055)------------------------------ % 48.03/7.79 % (1627055)------------------------------ % 48.03/7.79 % (1627058)Refutation not found, incomplete strategy % 48.03/7.79 % (1627058)------------------------------ % 48.03/7.79 % (1627058)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.03/7.79 % (1627058)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.03/7.79 % (1627058)CaDiCaL version: 2.1.3 % 48.03/7.79 % (1627058)Termination reason: Refutation not found, incomplete strategy % 48.03/7.79 % (1627058)Time elapsed: 0.029 s % 48.03/7.79 % (1627058)Peak memory usage: 116 MB % 48.03/7.79 % (1627058)Instructions burned: 6 (million) % 48.03/7.79 % (1627060)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=1423413221:i=1846:canc=cautious:fsr=off:rtra=on_2955 on theBenchmark for (2955ds/1846Mi) % 48.03/7.79 % (1627061)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=886732505:s2a=on:i=36816:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2955 on theBenchmark for (2955ds/36816Mi) % 48.03/7.79 % (1627045)Instruction limit reached! % 48.03/7.79 % (1627045)------------------------------ % 48.03/7.79 % (1627045)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.03/7.79 % (1627045)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.03/7.79 % (1627045)CaDiCaL version: 2.1.3 % 48.03/7.79 % (1627045)Termination reason: Instruction limit % 48.03/7.79 % (1627045)Termination phase: Saturation % 48.03/7.79 % (1627045)Time elapsed: 0.671 s % 48.03/7.79 % (1627045)Peak memory usage: 123 MB % 48.03/7.79 % (1627045)Instructions burned: 1132 (million) % 48.03/7.79 % (1627064)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=2187213686:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2953 on theBenchmark for (2953ds/273Mi) % 48.03/7.79 % (1627064)Instruction limit reached! % 48.03/7.79 % (1627064)------------------------------ % 48.03/7.79 % (1627064)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.03/7.79 % (1627064)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.03/7.79 % (1627064)CaDiCaL version: 2.1.3 % 48.03/7.79 % (1627064)Termination reason: Instruction limit % 48.03/7.79 % (1627064)Termination phase: Saturation % 48.03/7.79 % (1627064)Time elapsed: 0.090 s % 48.03/7.79 % (1627064)Peak memory usage: 91 MB % 48.03/7.79 % (1627064)Instructions burned: 275 (million) % 48.03/7.79 % (1627058)------------------------------ % 48.03/7.79 % (1627058)------------------------------ % 48.03/7.79 % (1627068)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=3812683623:i=863:doe=on:nm=0:rtra=on:gtg=exists_sym_2952 on theBenchmark for (2952ds/863Mi) % 48.03/7.79 % (1627068)Refutation not found, incomplete strategy % 48.03/7.79 % (1627068)------------------------------ % 58.21/9.08 % (1627068)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 58.21/9.08 % (1627068)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 58.21/9.08 % (1627068)CaDiCaL version: 2.1.3 % 58.21/9.08 % (1627068)Termination reason: Refutation not found, incomplete strategy % 58.21/9.08 % (1627068)Time elapsed: 0.029 s % 58.21/9.08 % (1627068)Peak memory usage: 116 MB % 58.21/9.08 % (1627068)Instructions burned: 6 (million) % 58.21/9.08 % (1627069)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=396081997:i=5811:kws=precedence:nm=0:rtra=on_2951 on theBenchmark for (2951ds/5811Mi) % 58.21/9.08 % (1627069)Refutation not found, incomplete strategy % 58.21/9.08 % (1627069)------------------------------ % 58.21/9.08 % (1627069)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 58.21/9.08 % (1627069)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 58.21/9.08 % (1627069)CaDiCaL version: 2.1.3 % 58.21/9.08 % (1627069)Termination reason: Refutation not found, incomplete strategy % 58.21/9.08 % (1627069)Time elapsed: 0.018 s % 58.21/9.08 % (1627069)Peak memory usage: 115 MB % 58.21/9.08 % (1627069)Instructions burned: 6 (million) % 58.21/9.08 % (1627070)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=4004929329:i=2216:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2951 on theBenchmark for (2951ds/2216Mi) % 58.21/9.08 % (1627069)------------------------------ % 58.21/9.08 % (1627069)------------------------------ % 58.21/9.08 % (1627068)------------------------------ % 58.21/9.08 % (1627068)------------------------------ % 58.21/9.08 % (1627074)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=1999724715:i=801:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2948 on theBenchmark for (2948ds/801Mi) % 58.21/9.08 % (1627074)Refutation not found, incomplete strategy % 58.21/9.08 % (1627074)------------------------------ % 58.21/9.08 % (1627074)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 58.21/9.08 % (1627074)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 58.21/9.08 % (1627074)CaDiCaL version: 2.1.3 % 58.21/9.08 % (1627074)Termination reason: Refutation not found, incomplete strategy % 58.21/9.08 % (1627074)Time elapsed: 0.001 s % 58.21/9.08 % (1627074)Peak memory usage: 89 MB % 58.21/9.08 % (1627075)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=749967100:st=5:i=1026:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2948 on theBenchmark for (2948ds/1026Mi) % 58.21/9.08 % (1627075)Refutation not found, incomplete strategy % 58.21/9.08 % (1627075)------------------------------ % 58.21/9.08 % (1627075)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 58.21/9.08 % (1627075)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 58.21/9.08 % (1627075)CaDiCaL version: 2.1.3 % 58.21/9.08 % (1627075)Termination reason: Refutation not found, incomplete strategy % 58.21/9.08 % (1627075)Time elapsed: 0.002 s % 58.21/9.08 % (1627075)Peak memory usage: 89 MB % 58.21/9.08 % (1627074)------------------------------ % 58.21/9.08 % (1627074)------------------------------ % 58.21/9.08 % (1627078)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=597369877:i=3509:rtra=on_2946 on theBenchmark for (2946ds/3509Mi) % 58.21/9.08 % (1627075)------------------------------ % 58.21/9.08 % (1627075)------------------------------ % 58.21/9.08 % (1627060)Instruction limit reached! % 58.21/9.08 % (1627060)------------------------------ % 58.21/9.08 % (1627060)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 58.21/9.08 % (1627060)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 58.21/9.08 % (1627060)CaDiCaL version: 2.1.3 % 58.21/9.08 % (1627060)Termination reason: Instruction limit % 58.21/9.08 % (1627060)Termination phase: Saturation % 58.21/9.08 % (1627060)Time elapsed: 1.017 s % 58.21/9.08 % (1627060)Peak memory usage: 112 MB % 58.21/9.08 % (1627060)Instructions burned: 1847 (million) % 58.21/9.08 % (1627012)Instruction limit reached! % 58.21/9.08 % (1627012)------------------------------ % 58.21/9.08 % (1627012)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 58.21/9.08 % (1627012)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 58.21/9.08 % (1627012)CaDiCaL version: 2.1.3 % 58.21/9.08 % (1627012)Termination reason: Instruction limit % 58.21/9.08 % (1627012)Termination phase: Saturation % 82.81/12.54 % (1627012)Time elapsed: 2.547 s % 82.81/12.54 % (1627012)Peak memory usage: 117 MB % 82.81/12.54 % (1627012)Instructions burned: 4428 (million) % 82.81/12.54 % (1627080)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=2116792837:st=2:i=2127:sd=12:ep=R:rtra=on:ss=axioms_2944 on theBenchmark for (2944ds/2127Mi) % 82.81/12.54 % (1627081)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=1220308230:i=1959:rtra=on:fsd=on:proc=on_2943 on theBenchmark for (2943ds/1959Mi) % 82.81/12.54 % (1627082)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=3313848920:s2a=on:i=3553:nm=0:rtra=on_2943 on theBenchmark for (2943ds/3553Mi) % 82.81/12.54 % (1627081)Refutation not found, incomplete strategy % 82.81/12.54 % (1627081)------------------------------ % 82.81/12.54 % (1627081)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 82.81/12.54 % (1627081)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 82.81/12.54 % (1627081)CaDiCaL version: 2.1.3 % 82.81/12.54 % (1627081)Termination reason: Refutation not found, incomplete strategy % 82.81/12.54 % (1627081)Time elapsed: 0.027 s % 82.81/12.54 % (1627081)Peak memory usage: 115 MB % 82.81/12.54 % (1627081)Instructions burned: 6 (million) % 82.81/12.54 % (1627081)------------------------------ % 82.81/12.54 % (1627081)------------------------------ % 82.81/12.54 % (1627086)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=222131979:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2939 on theBenchmark for (2939ds/3201Mi) % 82.81/12.54 % (1627070)Instruction limit reached! % 82.81/12.54 % (1627070)------------------------------ % 82.81/12.54 % (1627070)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 82.81/12.54 % (1627070)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 82.81/12.54 % (1627070)CaDiCaL version: 2.1.3 % 82.81/12.54 % (1627070)Termination reason: Instruction limit % 82.81/12.54 % (1627070)Termination phase: Saturation % 82.81/12.54 % (1627070)Time elapsed: 1.241 s % 82.81/12.54 % (1627070)Peak memory usage: 124 MB % 82.81/12.54 % (1627070)Instructions burned: 2218 (million) % 82.81/12.54 % (1627088)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=837090703:thitd=on:cond=on:i=4093:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2937 on theBenchmark for (2937ds/4093Mi) % 82.81/12.54 % (1627078)Instruction limit reached! % 82.81/12.54 % (1627078)------------------------------ % 82.81/12.54 % (1627078)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 82.81/12.54 % (1627078)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 82.81/12.54 % (1627078)CaDiCaL version: 2.1.3 % 82.81/12.54 % (1627078)Termination reason: Instruction limit % 82.81/12.54 % (1627078)Termination phase: Saturation % 82.81/12.54 % (1627078)Time elapsed: 1.232 s % 82.81/12.54 % (1627078)Peak memory usage: 100 MB % 82.81/12.54 % (1627078)Instructions burned: 3512 (million) % 82.81/12.54 % (1627080)Instruction limit reached! % 82.81/12.54 % (1627080)------------------------------ % 82.81/12.54 % (1627080)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 82.81/12.54 % (1627080)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 82.81/12.54 % (1627080)CaDiCaL version: 2.1.3 % 82.81/12.54 % (1627080)Termination reason: Instruction limit % 82.81/12.54 % (1627080)Termination phase: Saturation % 82.81/12.54 % (1627080)Time elapsed: 1.019 s % 82.81/12.54 % (1627080)Peak memory usage: 103 MB % 82.81/12.54 % (1627080)Instructions burned: 2129 (million) % 82.81/12.54 % (1627090)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=521445176:cond=fast:i=21173:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2932 on theBenchmark for (2932ds/21173Mi) % 82.81/12.54 % (1627090)Refutation not found, incomplete strategy % 82.81/12.54 % (1627090)------------------------------ % 82.81/12.54 % (1627090)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 82.81/12.54 % (1627090)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 82.81/12.54 % (1627090)CaDiCaL version: 2.1.3 % 82.81/12.54 % (1627090)Termination reason: Refutation not found, incomplete strategy % 82.81/12.54 % (1627090)Time elapsed: 0.017 s % 82.81/12.54 % (1627090)Peak memory usage: 114 MB % 82.81/12.54 % (1627090)Instructions burned: 6 (million) % 82.81/12.54 % (1627091)lrs+11_1_to=lpo:thi=all:sas=z3:si=on:fd=off:sac=on:slsq=on:random_seed=2280019428:avsq=on:i=10544:avsqr=17,4:canc=force:rtra=on:gtg=exists_top:er=filter_2932 on theBenchmark for (2932ds/10544Mi) % 99.42/14.93 % (1627090)------------------------------ % 99.42/14.93 % (1627090)------------------------------ % 99.42/14.93 % (1627094)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=821217947:avsq=on:i=1262:avsqr=1,16:rtra=on:rawr=on_2929 on theBenchmark for (2929ds/1262Mi) % 99.42/14.93 % (1627094)Instruction limit reached! % 99.42/14.93 % (1627094)------------------------------ % 99.42/14.93 % (1627094)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 99.42/14.93 % (1627094)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.42/14.93 % (1627094)CaDiCaL version: 2.1.3 % 99.42/14.93 % (1627094)Termination reason: Instruction limit % 99.42/14.93 % (1627094)Termination phase: Saturation % 99.42/14.93 % (1627094)Time elapsed: 0.341 s % 99.42/14.93 % (1627094)Peak memory usage: 117 MB % 99.42/14.93 % (1627094)Instructions burned: 1267 (million) % 99.42/14.93 % (1627096)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=2245733182:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2925 on theBenchmark for (2925ds/775Mi) % 99.42/14.93 % (1627096)Instruction limit reached! % 99.42/14.93 % (1627096)------------------------------ % 99.42/14.93 % (1627096)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 99.42/14.93 % (1627096)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.42/14.93 % (1627096)CaDiCaL version: 2.1.3 % 99.42/14.93 % (1627096)Termination reason: Instruction limit % 99.42/14.93 % (1627096)Termination phase: Saturation % 99.42/14.93 % (1627096)Time elapsed: 0.267 s % 99.42/14.93 % (1627096)Peak memory usage: 95 MB % 99.42/14.93 % (1627096)Instructions burned: 779 (million) % 99.42/14.93 % (1627098)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=3214338380:i=270:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2921 on theBenchmark for (2921ds/270Mi) % 99.42/14.93 % (1627098)Instruction limit reached! % 99.42/14.93 % (1627098)------------------------------ % 99.42/14.93 % (1627098)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 99.42/14.93 % (1627098)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.42/14.93 % (1627098)CaDiCaL version: 2.1.3 % 99.42/14.93 % (1627098)Termination reason: Instruction limit % 99.42/14.93 % (1627098)Termination phase: Saturation % 99.42/14.93 % (1627098)Time elapsed: 0.089 s % 99.42/14.93 % (1627098)Peak memory usage: 91 MB % 99.42/14.93 % (1627098)Instructions burned: 271 (million) % 99.42/14.93 % (1627056)Instruction limit reached! % 99.42/14.93 % (1627056)------------------------------ % 99.42/14.93 % (1627056)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 99.42/14.93 % (1627056)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.42/14.93 % (1627056)CaDiCaL version: 2.1.3 % 99.42/14.93 % (1627056)Termination reason: Instruction limit % 99.42/14.93 % (1627056)Termination phase: Saturation % 99.42/14.93 % (1627056)Time elapsed: 3.634 s % 99.42/14.93 % (1627056)Peak memory usage: 129 MB % 99.42/14.93 % (1627056)Instructions burned: 6400 (million) % 99.42/14.93 % (1627082)Instruction limit reached! % 99.42/14.93 % (1627082)------------------------------ % 99.42/14.93 % (1627082)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 99.42/14.93 % (1627082)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.42/14.93 % (1627082)CaDiCaL version: 2.1.3 % 99.42/14.93 % (1627082)Termination reason: Instruction limit % 99.42/14.93 % (1627082)Termination phase: Saturation % 99.42/14.93 % (1627082)Time elapsed: 2.355 s % 99.42/14.93 % (1627082)Peak memory usage: 103 MB % 99.42/14.93 % (1627082)Instructions burned: 3554 (million) % 99.42/14.93 % (1627086)Instruction limit reached! % 99.42/14.93 % (1627086)------------------------------ % 99.42/14.93 % (1627086)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 99.42/14.93 % (1627086)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.42/14.93 % (1627086)CaDiCaL version: 2.1.3 % 99.42/14.93 % (1627086)Termination reason: Instruction limit % 99.42/14.93 % (1627086)Termination phase: Saturation % 99.42/14.93 % (1627086)Time elapsed: 1.948 s % 99.42/14.93 % (1627086)Peak memory usage: 133 MB % 99.42/14.93 % (1627086)Instructions burned: 3202 (million) % 99.42/14.93 % (1627100)ott+10_128_isp=bottom:to=lpo:sil=128000:si=on:urr=on:uwa=alasca_main:sac=on:slsq=on:random_seed=2851561789:i=17165:aac=none:doe=on:rtra=on:gtg=exists_all_2919 on theBenchmark for (2919ds/17165Mi) % 120.82/17.95 % (1627101)lrs+2_10_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_main:tha=some:random_seed=2260726528:s2a=on:i=13094:s2at=-1:rtra=on_2918 on theBenchmark for (2918ds/13094Mi) % 120.82/17.95 % (1627102)lrs+10_1_to=lpo:sil=128000:si=on:sp=occurrence:random_seed=728691359:st=2:i=12633:rtra=on:ss=axioms_2918 on theBenchmark for (2918ds/12633Mi) % 120.82/17.95 % (1627103)dis+1011_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_frequency:lsd=20:nwc=3:random_seed=559359737:i=1783:rtra=on:gtg=position_2918 on theBenchmark for (2918ds/1783Mi) % 120.82/17.95 % (1627088)Instruction limit reached! % 120.82/17.95 % (1627088)------------------------------ % 120.82/17.95 % (1627088)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 120.82/17.95 % (1627088)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.82/17.95 % (1627088)CaDiCaL version: 2.1.3 % 120.82/17.95 % (1627088)Termination reason: Instruction limit % 120.82/17.95 % (1627088)Termination phase: Saturation % 120.82/17.95 % (1627088)Time elapsed: 1.971 s % 120.82/17.95 % (1627088)Peak memory usage: 140 MB % 120.82/17.95 % (1627088)Instructions burned: 4095 (million) % 120.82/17.95 % (1627108)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=3432979631:i=5451:aac=none:doe=on:nm=0:rtra=on:amm=off:gtg=position_2915 on theBenchmark for (2915ds/5451Mi) % 120.82/17.95 % (1627103)Instruction limit reached! % 120.82/17.95 % (1627103)------------------------------ % 120.82/17.95 % (1627103)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 120.82/17.95 % (1627103)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.82/17.95 % (1627103)CaDiCaL version: 2.1.3 % 120.82/17.95 % (1627103)Termination reason: Instruction limit % 120.82/17.95 % (1627103)Termination phase: Saturation % 120.82/17.95 % (1627103)Time elapsed: 1.011 s % 120.82/17.95 % (1627103)Peak memory usage: 126 MB % 120.82/17.95 % (1627103)Instructions burned: 1784 (million) % 120.82/17.95 % (1627110)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=1390501749:i=4975:doe=on:nm=0:rtra=on:gtg=exists_sym_2906 on theBenchmark for (2906ds/4975Mi) % 120.82/17.95 % (1627110)Refutation not found, incomplete strategy % 120.82/17.95 % (1627110)------------------------------ % 120.82/17.95 % (1627110)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 120.82/17.95 % (1627110)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.82/17.95 % (1627110)CaDiCaL version: 2.1.3 % 120.82/17.95 % (1627110)Termination reason: Refutation not found, incomplete strategy % 120.82/17.95 % (1627110)Time elapsed: 0.029 s % 120.82/17.95 % (1627110)Peak memory usage: 116 MB % 120.82/17.95 % (1627110)Instructions burned: 6 (million) % 120.82/17.95 % (1627110)------------------------------ % 120.82/17.95 % (1627110)------------------------------ % 120.82/17.95 % (1627112)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=478931128:i=2076:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2901 on theBenchmark for (2901ds/2076Mi) % 120.82/17.95 % (1627112)Instruction limit reached! % 120.82/17.95 % (1627112)------------------------------ % 120.82/17.95 % (1627112)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 120.82/17.95 % (1627112)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.82/17.95 % (1627112)CaDiCaL version: 2.1.3 % 120.82/17.95 % (1627112)Termination reason: Instruction limit % 120.82/17.95 % (1627112)Termination phase: Saturation % 120.82/17.95 % (1627112)Time elapsed: 0.850 s % 120.82/17.95 % (1627112)Peak memory usage: 126 MB % 120.82/17.95 % (1627112)Instructions burned: 2076 (million) % 120.82/17.95 % (1627114)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=4169389407:i=5145:rtra=on_2891 on theBenchmark for (2891ds/5145Mi) % 120.82/17.95 % (1627108)Instruction limit reached! % 120.82/17.95 % (1627108)------------------------------ % 120.82/17.95 % (1627108)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 120.82/17.95 % (1627108)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.82/17.95 % (1627108)CaDiCaL version: 2.1.3 % 120.82/17.95 % (1627108)Termination reason: Instruction limit % 120.82/17.95 % (1627108)Termination phase: Saturation % 120.82/17.95 % (1627108)Time elapsed: 3.111 s % 120.82/17.95 % (1627108)Peak memory usage: 146 MB % 120.82/17.95 % (1627108)Instructions burned: 5451 (million) % 230.09/33.24 % (1627116)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=680007542:i=3509:rtra=on_2883 on theBenchmark for (2883ds/3509Mi) % 230.09/33.24 % (1627114)Instruction limit reached! % 230.09/33.24 % (1627114)------------------------------ % 230.09/33.24 % (1627114)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 230.09/33.24 % (1627114)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 230.09/33.24 % (1627114)CaDiCaL version: 2.1.3 % 230.09/33.24 % (1627114)Termination reason: Instruction limit % 230.09/33.24 % (1627114)Termination phase: Saturation % 230.09/33.24 % (1627114)Time elapsed: 1.792 s % 230.09/33.24 % (1627114)Peak memory usage: 89 MB % 230.09/33.24 % (1627114)Instructions burned: 5147 (million) % 230.09/33.24 % (1627118)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=2736978022:st=2:i=13800:sd=12:ep=R:rtra=on:ss=axioms_2872 on theBenchmark for (2872ds/13800Mi) % 230.09/33.24 % (1627101)Instruction limit reached! % 230.09/33.24 % (1627101)------------------------------ % 230.09/33.24 % (1627101)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 230.09/33.24 % (1627101)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 230.09/33.24 % (1627101)CaDiCaL version: 2.1.3 % 230.09/33.24 % (1627101)Termination reason: Instruction limit % 230.09/33.24 % (1627101)Termination phase: Saturation % 230.09/33.24 % (1627101)Time elapsed: 4.942 s % 230.09/33.24 % (1627101)Peak memory usage: 93 MB % 230.09/33.24 % (1627101)Instructions burned: 13096 (million) % 230.09/33.24 % (1627175)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=1925581767:i=1412:rtra=on:fsd=on:proc=on_2867 on theBenchmark for (2867ds/1412Mi) % 230.09/33.24 % (1627175)Refutation not found, incomplete strategy % 230.09/33.24 % (1627175)------------------------------ % 230.09/33.24 % (1627175)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 230.09/33.24 % (1627175)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 230.09/33.24 % (1627175)CaDiCaL version: 2.1.3 % 230.09/33.24 % (1627175)Termination reason: Refutation not found, incomplete strategy % 230.09/33.24 % (1627175)Time elapsed: 0.027 s % 230.09/33.24 % (1627175)Peak memory usage: 115 MB % 230.09/33.24 % (1627175)Instructions burned: 6 (million) % 230.09/33.24 % (1627091)Instruction limit reached! % 230.09/33.24 % (1627091)------------------------------ % 230.09/33.24 % (1627091)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 230.09/33.24 % (1627091)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 230.09/33.24 % (1627091)CaDiCaL version: 2.1.3 % 230.09/33.24 % (1627091)Termination reason: Instruction limit % 230.09/33.24 % (1627091)Termination phase: Saturation % 230.09/33.24 % (1627091)Time elapsed: 6.598 s % 230.09/33.24 % (1627091)Peak memory usage: 257 MB % 230.09/33.24 % (1627091)Instructions burned: 10544 (million) % 230.09/33.24 % (1627175)------------------------------ % 230.09/33.24 % (1627175)------------------------------ % 230.09/33.24 % (1627238)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 % 230.09/33.24 % (1627238)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=3214249474:i=11747:aac=none:nm=0:rtra=on:rawr=on_2864 on theBenchmark for (2864ds/11747Mi) % 230.09/33.24 % (1627238)Refutation not found, incomplete strategy % 230.09/33.24 % (1627238)------------------------------ % 230.09/33.24 % (1627238)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 230.09/33.24 % (1627238)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 230.09/33.24 % (1627238)CaDiCaL version: 2.1.3 % 230.09/33.24 % (1627238)Termination reason: Refutation not found, incomplete strategy % 230.09/33.24 % (1627238)Time elapsed: 0.028 s % 230.09/33.24 % (1627238)Peak memory usage: 115 MB % 230.09/33.24 % (1627238)Instructions burned: 6 (million) % 230.09/33.24 % (1627239)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=4237867566:s2a=on:i=3553:nm=0:rtra=on_2863 on theBenchmark for (2863ds/3553Mi) % 230.09/33.24 % (1627238)------------------------------ % 230.09/33.24 % (1627238)------------------------------ % 230.09/33.24 % (1627100)Instruction limit reached! % 230.09/33.24 % (1627100)------------------------------ % 230.09/33.24 % (1627100)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 230.09/33.24 % (1627100)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 281.62/40.51 % (1627100)CaDiCaL version: 2.1.3 % 281.62/40.51 % (1627100)Termination reason: Instruction limit % 281.62/40.51 % (1627100)Termination phase: Saturation % 281.62/40.51 % (1627100)Time elapsed: 5.852 s % 281.62/40.51 % (1627100)Peak memory usage: 358 MB % 281.62/40.51 % (1627100)Instructions burned: 17169 (million) % 281.62/40.51 % (1627325)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=1431950983:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2860 on theBenchmark for (2860ds/3201Mi) % 281.62/40.51 % (1627116)Instruction limit reached! % 281.62/40.51 % (1627116)------------------------------ % 281.62/40.51 % (1627116)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 281.62/40.51 % (1627116)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 281.62/40.51 % (1627116)CaDiCaL version: 2.1.3 % 281.62/40.51 % (1627116)Termination reason: Instruction limit % 281.62/40.51 % (1627116)Termination phase: Saturation % 281.62/40.51 % (1627116)Time elapsed: 2.308 s % 281.62/40.51 % (1627116)Peak memory usage: 100 MB % 281.62/40.51 % (1627116)Instructions burned: 3510 (million) % 281.62/40.51 % (1627341)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=1340075068:thitd=on:cond=on:i=4081:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2859 on theBenchmark for (2859ds/4081Mi) % 281.62/40.51 % (1627346)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=3417258127:cond=fast:i=20260:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2858 on theBenchmark for (2858ds/20260Mi) % 281.62/40.51 % (1627346)Refutation not found, incomplete strategy % 281.62/40.51 % (1627346)------------------------------ % 281.62/40.51 % (1627346)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 281.62/40.51 % (1627346)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 281.62/40.51 % (1627346)CaDiCaL version: 2.1.3 % 281.62/40.51 % (1627346)Termination reason: Refutation not found, incomplete strategy % 281.62/40.51 % (1627346)Time elapsed: 0.027 s % 281.62/40.51 % (1627346)Peak memory usage: 114 MB % 281.62/40.51 % (1627346)Instructions burned: 6 (million) % 281.62/40.51 % (1627346)------------------------------ % 281.62/40.51 % (1627346)------------------------------ % 281.62/40.51 % (1627362)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=4184788265:s2a=on:i=58627:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2854 on theBenchmark for (2854ds/58627Mi) % 281.62/40.51 % (1627102)Instruction limit reached! % 281.62/40.51 % (1627102)------------------------------ % 281.62/40.51 % (1627102)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 281.62/40.51 % (1627102)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 281.62/40.51 % (1627102)CaDiCaL version: 2.1.3 % 281.62/40.51 % (1627102)Termination reason: Instruction limit % 281.62/40.51 % (1627102)Termination phase: Saturation % 281.62/40.51 % (1627102)Time elapsed: 7.388 s % 281.62/40.51 % (1627102)Peak memory usage: 115 MB % 281.62/40.51 % (1627102)Instructions burned: 12635 (million) % 281.62/40.51 % (1627387)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=1932960944:avsq=on:i=6258:avsqr=1,16:rtra=on:rawr=on_2842 on theBenchmark for (2842ds/6258Mi) % 281.62/40.51 % (1627325)Instruction limit reached! % 281.62/40.51 % (1627325)------------------------------ % 281.62/40.51 % (1627325)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 281.62/40.51 % (1627325)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 281.62/40.51 % (1627325)CaDiCaL version: 2.1.3 % 281.62/40.51 % (1627325)Termination reason: Instruction limit % 281.62/40.51 % (1627325)Termination phase: Saturation % 281.62/40.51 % (1627325)Time elapsed: 2.623 s % 281.62/40.51 % (1627325)Peak memory usage: 133 MB % 281.62/40.51 % (1627325)Instructions burned: 3201 (million) % 281.62/40.51 % (1627239)Instruction limit reached! % 281.62/40.51 % (1627239)------------------------------ % 281.62/40.51 % (1627239)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 281.62/40.51 % (1627239)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 281.62/40.51 % (1627239)CaDiCaL version: 2.1.3 % 281.62/40.51 % (1627239)Termination reason: Instruction limit % 281.62/40.51 % (1627239)Termination phase: Saturation % 281.62/40.51 % (1627239)Time elapsed: 3.092 s % 281.62/40.51 % (1627239)Peak memory usage: 103 MB % 281.62/40.51 % (1627239)Instructions burned: 3553 (million) % 281.62/40.51 % (1627404)ott+10_128_isp=bottom:to=lpo:sil=128000:si=on:urr=on:uwa=alasca_main:sac=on:slsq=on:random_seed=904604839:i=34001:aac=none:doe=on:rtra=on:gtg=exists_all_2832 on theBenchmark for (2832ds/34001Mi) % 293.91/42.29 % (1627407)lrs+2_10_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_main:tha=some:random_seed=3413220626:s2a=on:i=71622:s2at=-1:rtra=on_2830 on theBenchmark for (2830ds/71622Mi) % 293.91/42.29 % (1627341)Instruction limit reached! % 293.91/42.29 % (1627341)------------------------------ % 293.91/42.29 % (1627341)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 293.91/42.29 % (1627341)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 293.91/42.29 % (1627341)CaDiCaL version: 2.1.3 % 293.91/42.29 % (1627341)Termination reason: Instruction limit % 293.91/42.29 % (1627341)Termination phase: Saturation % 293.91/42.29 % (1627341)Time elapsed: 3.005 s % 293.91/42.29 % (1627341)Peak memory usage: 140 MB % 293.91/42.29 % (1627341)Instructions burned: 4082 (million) % 293.91/42.29 % (1627410)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=3413629077:i=24001:kws=precedence:nm=0:rtra=on_2827 on theBenchmark for (2827ds/24001Mi) % 293.91/42.29 % (1627410)Refutation not found, incomplete strategy % 293.91/42.29 % (1627410)------------------------------ % 293.91/42.29 % (1627410)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 293.91/42.29 % (1627410)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 293.91/42.29 % (1627410)CaDiCaL version: 2.1.3 % 293.91/42.29 % (1627410)Termination reason: Refutation not found, incomplete strategy % 293.91/42.29 % (1627410)Time elapsed: 0.040 s % 293.91/42.29 % (1627410)Peak memory usage: 115 MB % 293.91/42.29 % (1627410)Instructions burned: 6 (million) % 293.91/42.29 % (1627410)------------------------------ % 293.91/42.29 % (1627410)------------------------------ % 293.91/42.29 % (1627417)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=835454684:i=2076:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2820 on theBenchmark for (2820ds/2076Mi) % 293.91/42.29 % (1627387)Instruction limit reached! % 293.91/42.29 % (1627387)------------------------------ % 293.91/42.29 % (1627387)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 293.91/42.29 % (1627387)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 293.91/42.29 % (1627387)CaDiCaL version: 2.1.3 % 293.91/42.29 % (1627387)Termination reason: Instruction limit % 293.91/42.29 % (1627387)Termination phase: Saturation % 293.91/42.29 % (1627387)Time elapsed: 2.598 s % 293.91/42.29 % (1627387)Peak memory usage: 119 MB % 293.91/42.29 % (1627387)Instructions burned: 6260 (million) % 293.91/42.29 % (1627424)dis+21_20_to=lakbo:si=on:alasca=on:sp=const_max:uwa=alasca_main:sac=on:random_seed=4172220517:s2a=on:i=83971:s2at=4:bd=all:ins=1:rtra=on_2814 on theBenchmark for (2814ds/83971Mi) % 293.91/42.29 % (1627417)Instruction limit reached! % 293.91/42.29 % (1627417)------------------------------ % 293.91/42.29 % (1627417)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 293.91/42.29 % (1627417)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 293.91/42.29 % (1627417)CaDiCaL version: 2.1.3 % 293.91/42.29 % (1627417)Termination reason: Instruction limit % 293.91/42.29 % (1627417)Termination phase: Saturation % 293.91/42.29 % (1627417)Time elapsed: 1.866 s % 293.91/42.29 % (1627417)Peak memory usage: 125 MB % 293.91/42.29 % (1627417)Instructions burned: 2076 (million) % 293.91/42.29 % (1627439)lrs+1011_5:1_to=lpo:sil=128000:sas=z3:si=on:norm_ineq=on:tha=some:random_seed=562203509:i=83944:rtra=on_2798 on theBenchmark for (2798ds/83944Mi) % 293.91/42.29 % (1627118)Instruction limit reached! % 293.91/42.29 % (1627118)------------------------------ % 293.91/42.29 % (1627118)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 293.91/42.29 % (1627118)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 293.91/42.29 % (1627118)CaDiCaL version: 2.1.3 % 293.91/42.29 % (1627118)Termination reason: Instruction limit % 293.91/42.29 % (1627118)Termination phase: Saturation % 293.91/42.29 % (1627118)Time elapsed: 9.402 s % 293.91/42.29 % (1627118)Peak memory usage: 187 MB % 293.91/42.29 % (1627118)Instructions burned: 13800 (million) % 293.91/42.29 % (1627449)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=490665699:i=9201:rtra=on_2776 on theBenchmark for (2776ds/9201Mi) % 293.91/42.29 % (1627449)Instruction limit reached! % 293.91/42.29 % (1627449)------------------------------ % 293.91/42.29 % (1627449)Version: Vampire 5.0.1 (ReleaTerminated %------------------------------------------------------------------------------