%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWX126_1 : TPTP v9.3.1. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % Computer : n013.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:45:56 PM UTC 2026 % Result : Timeout 300.01s 43.19s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.04 % Problem : SWX126_1 : TPTP v9.3.1. Released v9.3.0. % 0.00/0.08 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.11/0.27 % Computer : n013.cluster.edu % 0.11/0.27 % Model : x86_64 x86_64 % 0.11/0.27 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.27 % Memory : 8046.5625MB % 0.11/0.27 % OS : Linux 6.8.0-71-generic % 0.11/0.27 % CPULimit : 300 % 0.11/0.27 % WCLimit : 300 % 0.11/0.27 % DateTime : Mon Sep 28 15:02:21 UTC 2026 % 0.25/0.27 % CPUTime : % 0.25/0.27 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.25/0.31 Running first-order theorem proving % 0.25/0.31 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 5.19/1.87 % (1249758)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule. % 5.19/1.87 % (1249763)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=8031606:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi) % 5.19/1.87 % (1249763)Instruction limit reached! % 5.19/1.87 % (1249763)------------------------------ % 5.19/1.87 % (1249763)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.19/1.87 % (1249763)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.19/1.87 % (1249763)CaDiCaL version: 2.1.3 % 5.19/1.87 % (1249763)Termination reason: Instruction limit % 5.19/1.87 % (1249763)Termination phase: Saturation % 5.19/1.87 % (1249763)Time elapsed: 0.006 s % 5.19/1.87 % (1249763)Peak memory usage: 86 MB % 5.19/1.87 % (1249763)Instructions burned: 15 (million) % 5.19/1.87 % (1249768)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=3699729799:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi) % 5.19/1.87 % (1249765)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=1273444861:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi) % 5.19/1.87 % (1249764)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=2501572612:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi) % 5.19/1.87 % (1249769)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=2581371836:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi) % 5.19/1.87 % (1249767)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=1335250340:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi) % 5.19/1.87 % (1249766)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=214793135:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi) % 5.19/1.87 % (1249767)Instruction limit reached! % 5.19/1.87 % (1249767)------------------------------ % 5.19/1.87 % (1249767)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.19/1.87 % (1249767)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.19/1.87 % (1249767)CaDiCaL version: 2.1.3 % 5.19/1.87 % (1249767)Termination reason: Instruction limit % 5.19/1.87 % (1249767)Termination phase: Property scanning % 5.19/1.87 % (1249767)Time elapsed: 0.004 s % 5.19/1.87 % (1249767)Peak memory usage: 85 MB % 5.19/1.87 % (1249767)Instructions burned: 5 (million) % 5.19/1.87 % (1249766)Instruction limit reached! % 5.19/1.87 % (1249766)------------------------------ % 5.19/1.87 % (1249766)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.19/1.87 % (1249766)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.19/1.87 % (1249766)CaDiCaL version: 2.1.3 % 5.19/1.87 % (1249766)Termination reason: Instruction limit % 5.19/1.87 % (1249766)Termination phase: Property scanning % 5.19/1.87 % (1249766)Time elapsed: 0.007 s % 5.19/1.87 % (1249766)Peak memory usage: 85 MB % 5.19/1.87 % (1249766)Instructions burned: 7 (million) % 5.19/1.87 % (1249768)Instruction limit reached! % 5.19/1.87 % (1249768)------------------------------ % 5.19/1.87 % (1249768)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.19/1.87 % (1249768)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.19/1.87 % (1249768)CaDiCaL version: 2.1.3 % 5.19/1.87 % (1249768)Termination reason: Instruction limit % 5.19/1.87 % (1249768)Termination phase: Saturation % 5.19/1.87 % (1249768)Time elapsed: 0.066 s % 5.19/1.87 % (1249768)Peak memory usage: 112 MB % 5.19/1.87 % (1249768)Instructions burned: 46 (million) % 5.19/1.87 % (1249769)Instruction limit reached! % 5.19/1.87 % (1249769)------------------------------ % 5.19/1.87 % (1249769)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.19/1.87 % (1249769)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.19/1.87 % (1249769)CaDiCaL version: 2.1.3 % 5.19/1.87 % (1249769)Termination reason: Instruction limit % 5.19/1.87 % (1249769)Termination phase: Saturation % 5.19/1.87 % (1249769)Time elapsed: 0.054 s % 5.19/1.87 % (1249769)Peak memory usage: 111 MB % 5.19/1.87 % (1249769)Instructions burned: 33 (million) % 5.19/1.87 % (1249771)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=2417352102:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2997 on theBenchmark for (2997ds/14Mi) % 5.19/1.87 % (1249771)Refutation not found, incomplete strategy % 5.19/1.87 % (1249771)------------------------------ % 8.27/2.12 % (1249771)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.27/2.12 % (1249771)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.27/2.12 % (1249771)CaDiCaL version: 2.1.3 % 8.27/2.12 % (1249771)Termination reason: Refutation not found, incomplete strategy % 8.27/2.12 % (1249771)Time elapsed: 0.004 s % 8.27/2.12 % (1249771)Peak memory usage: 88 MB % 8.27/2.12 % (1249771)Instructions burned: 8 (million) % 8.27/2.12 % (1249765)Instruction limit reached! % 8.27/2.12 % (1249765)------------------------------ % 8.27/2.12 % (1249765)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.27/2.12 % (1249765)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.27/2.12 % (1249765)CaDiCaL version: 2.1.3 % 8.27/2.12 % (1249765)Termination reason: Instruction limit % 8.27/2.12 % (1249765)Termination phase: Saturation % 8.27/2.12 % (1249765)Time elapsed: 0.184 s % 8.27/2.12 % (1249765)Peak memory usage: 117 MB % 8.27/2.12 % (1249765)Instructions burned: 201 (million) % 8.27/2.12 % (1249778)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=54082860:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2997 on theBenchmark for (2997ds/29Mi) % 8.27/2.12 % (1249778)Instruction limit reached! % 8.27/2.12 % (1249778)------------------------------ % 8.27/2.12 % (1249778)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.27/2.12 % (1249778)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.27/2.12 % (1249778)CaDiCaL version: 2.1.3 % 8.27/2.12 % (1249778)Termination reason: Instruction limit % 8.27/2.12 % (1249778)Termination phase: Saturation % 8.27/2.12 % (1249778)Time elapsed: 0.025 s % 8.27/2.12 % (1249778)Peak memory usage: 89 MB % 8.27/2.12 % (1249778)Instructions burned: 29 (million) % 8.27/2.12 % (1249779)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=3452750291:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2997 on theBenchmark for (2997ds/16Mi) % 8.27/2.12 % (1249764)Instruction limit reached! % 8.27/2.12 % (1249764)------------------------------ % 8.27/2.12 % (1249764)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.27/2.12 % (1249764)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.27/2.12 % (1249764)CaDiCaL version: 2.1.3 % 8.27/2.12 % (1249764)Termination reason: Instruction limit % 8.27/2.12 % (1249764)Termination phase: Saturation % 8.27/2.12 % (1249764)Time elapsed: 0.268 s % 8.27/2.12 % (1249764)Peak memory usage: 116 MB % 8.27/2.12 % (1249764)Instructions burned: 308 (million) % 8.27/2.12 % (1249779)Instruction limit reached! % 8.27/2.12 % (1249779)------------------------------ % 8.27/2.12 % (1249779)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.27/2.12 % (1249779)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.27/2.12 % (1249779)CaDiCaL version: 2.1.3 % 8.27/2.12 % (1249779)Termination reason: Instruction limit % 8.27/2.12 % (1249779)Termination phase: Saturation % 8.27/2.12 % (1249779)Time elapsed: 0.014 s % 8.27/2.12 % (1249779)Peak memory usage: 89 MB % 8.27/2.12 % (1249779)Instructions burned: 16 (million) % 8.27/2.12 % (1249781)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=1749585847:i=27:canc=cautious:fsr=off:rtra=on_2996 on theBenchmark for (2996ds/27Mi) % 8.27/2.12 % (1249780)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=439054321:i=24:canc=force:rtra=on_2996 on theBenchmark for (2996ds/24Mi) % 8.27/2.12 % (1249780)Instruction limit reached! % 8.27/2.12 % (1249780)------------------------------ % 8.27/2.12 % (1249780)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.27/2.12 % (1249780)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.27/2.12 % (1249780)CaDiCaL version: 2.1.3 % 8.27/2.12 % (1249780)Termination reason: Instruction limit % 8.27/2.12 % (1249780)Termination phase: Saturation % 8.27/2.12 % (1249780)Time elapsed: 0.021 s % 8.27/2.12 % (1249780)Peak memory usage: 88 MB % 8.27/2.12 % (1249780)Instructions burned: 25 (million) % 8.27/2.12 % (1249781)Refutation not found, incomplete strategy % 8.27/2.12 % (1249781)------------------------------ % 8.27/2.12 % (1249781)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.27/2.12 % (1249781)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.19/2.34 % (1249781)CaDiCaL version: 2.1.3 % 9.19/2.34 % (1249781)Termination reason: Refutation not found, incomplete strategy % 9.19/2.34 % (1249781)Time elapsed: 0.023 s % 9.19/2.34 % (1249781)Peak memory usage: 88 MB % 9.19/2.34 % (1249781)Instructions burned: 27 (million) % 9.19/2.34 % (1249771)------------------------------ % 9.19/2.34 % (1249771)------------------------------ % 9.19/2.34 % (1249783)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=2125848375:i=85:gtgl=4:rtra=on:gtg=exists_sym_2995 on theBenchmark for (2995ds/85Mi) % 9.19/2.34 % (1249783)Instruction limit reached! % 9.19/2.34 % (1249783)------------------------------ % 9.19/2.34 % (1249783)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.19/2.34 % (1249783)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.19/2.34 % (1249783)CaDiCaL version: 2.1.3 % 9.19/2.34 % (1249783)Termination reason: Instruction limit % 9.19/2.34 % (1249783)Termination phase: Saturation % 9.19/2.34 % (1249783)Time elapsed: 0.079 s % 9.19/2.34 % (1249783)Peak memory usage: 89 MB % 9.19/2.34 % (1249783)Instructions burned: 85 (million) % 9.19/2.34 % (1249786)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=3336939977:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2994 on theBenchmark for (2994ds/2Mi) % 9.19/2.34 % (1249786)Instruction limit reached! % 9.19/2.34 % (1249786)------------------------------ % 9.19/2.34 % (1249786)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.19/2.34 % (1249786)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.19/2.34 % (1249786)CaDiCaL version: 2.1.3 % 9.19/2.34 % (1249786)Termination reason: Instruction limit % 9.19/2.34 % (1249786)Termination phase: Property scanning % 9.19/2.34 % (1249786)Time elapsed: 0.002 s % 9.19/2.34 % (1249786)Peak memory usage: 85 MB % 9.19/2.34 % (1249786)Instructions burned: 2 (million) % 9.19/2.34 % (1249787)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=3229133413:i=181:rtra=on:ss=axioms:ev=cautious_2994 on theBenchmark for (2994ds/181Mi) % 9.19/2.34 % (1249787)Refutation not found, incomplete strategy % 9.19/2.34 % (1249787)------------------------------ % 9.19/2.34 % (1249787)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.19/2.34 % (1249787)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.19/2.34 % (1249787)CaDiCaL version: 2.1.3 % 9.19/2.34 % (1249787)Termination reason: Refutation not found, incomplete strategy % 9.19/2.34 % (1249787)Time elapsed: 0.006 s % 9.19/2.34 % (1249787)Peak memory usage: 87 MB % 9.19/2.34 % (1249787)Instructions burned: 7 (million) % 9.19/2.34 % (1249788)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=1971797815:i=4:ep=RST:ins=2:rtra=on_2994 on theBenchmark for (2994ds/4Mi) % 9.19/2.34 % (1249788)Instruction limit reached! % 9.19/2.34 % (1249788)------------------------------ % 9.19/2.34 % (1249788)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.19/2.34 % (1249788)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.19/2.34 % (1249788)CaDiCaL version: 2.1.3 % 9.19/2.34 % (1249788)Termination reason: Instruction limit % 9.19/2.34 % (1249788)Termination phase: Property scanning % 9.19/2.34 % (1249788)Time elapsed: 0.004 s % 9.19/2.34 % (1249788)Peak memory usage: 85 MB % 9.19/2.34 % (1249788)Instructions burned: 4 (million) % 9.19/2.34 % (1249792)lrs+10_1_thi=all:si=on:fd=off:random_seed=1741428066:i=53:rtra=on:gtg=all_2993 on theBenchmark for (2993ds/53Mi) % 9.19/2.34 % (1249791)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=1969374019:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2993 on theBenchmark for (2993ds/66Mi) % 9.19/2.34 % (1249792)Instruction limit reached! % 9.19/2.34 % (1249792)------------------------------ % 9.19/2.34 % (1249792)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.19/2.34 % (1249792)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.19/2.34 % (1249792)CaDiCaL version: 2.1.3 % 9.19/2.34 % (1249792)Termination reason: Instruction limit % 9.19/2.34 % (1249792)Termination phase: Saturation % 9.19/2.34 % (1249792)Time elapsed: 0.043 s % 9.19/2.34 % (1249792)Peak memory usage: 116 MB % 9.19/2.34 % (1249792)Instructions burned: 54 (million) % 9.19/2.34 % (1249781)------------------------------ % 9.19/2.34 % (1249781)------------------------------ % 9.19/2.34 % (1249791)Instruction limit reached! % 9.19/2.34 % (1249791)------------------------------ % 10.74/2.66 % (1249791)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.74/2.66 % (1249791)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.74/2.66 % (1249791)CaDiCaL version: 2.1.3 % 10.74/2.66 % (1249791)Termination reason: Instruction limit % 10.74/2.66 % (1249791)Termination phase: Saturation % 10.74/2.66 % (1249791)Time elapsed: 0.107 s % 10.74/2.66 % (1249791)Peak memory usage: 129 MB % 10.74/2.66 % (1249791)Instructions burned: 66 (million) % 10.74/2.66 % (1249794)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=3113491811:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2992 on theBenchmark for (2992ds/8Mi) % 10.74/2.66 % (1249794)Instruction limit reached! % 10.74/2.66 % (1249794)------------------------------ % 10.74/2.66 % (1249794)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.74/2.66 % (1249794)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.74/2.66 % (1249794)CaDiCaL version: 2.1.3 % 10.74/2.66 % (1249794)Termination reason: Instruction limit % 10.74/2.66 % (1249794)Termination phase: Property scanning % 10.74/2.66 % (1249794)Time elapsed: 0.007 s % 10.74/2.66 % (1249794)Peak memory usage: 85 MB % 10.74/2.66 % (1249794)Instructions burned: 9 (million) % 10.74/2.66 % (1249796)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=954497703:st=3:i=2:rtra=on:ss=axioms_2992 on theBenchmark for (2992ds/2Mi) % 10.74/2.66 % (1249796)Instruction limit reached! % 10.74/2.66 % (1249796)------------------------------ % 10.74/2.66 % (1249796)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.74/2.66 % (1249796)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.74/2.66 % (1249796)CaDiCaL version: 2.1.3 % 10.74/2.66 % (1249796)Termination reason: Instruction limit % 10.74/2.66 % (1249796)Termination phase: Property scanning % 10.74/2.66 % (1249796)Time elapsed: 0.003 s % 10.74/2.66 % (1249796)Peak memory usage: 85 MB % 10.74/2.66 % (1249796)Instructions burned: 3 (million) % 10.74/2.66 % (1249799)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=656350447:i=2:doe=on:canc=force:asg=cautious:rtra=on_2991 on theBenchmark for (2991ds/2Mi) % 10.74/2.66 % (1249799)Instruction limit reached! % 10.74/2.66 % (1249799)------------------------------ % 10.74/2.66 % (1249799)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.74/2.66 % (1249799)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.74/2.66 % (1249799)CaDiCaL version: 2.1.3 % 10.74/2.66 % (1249799)Termination reason: Instruction limit % 10.74/2.66 % (1249799)Termination phase: Property scanning % 10.74/2.66 % (1249799)Time elapsed: 0.002 s % 10.74/2.66 % (1249799)Peak memory usage: 85 MB % 10.74/2.66 % (1249799)Instructions burned: 2 (million) % 10.74/2.66 % (1249802)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=2016762429:i=127:doe=on:rtra=on_2991 on theBenchmark for (2991ds/127Mi) % 10.74/2.66 % (1249802)Instruction limit reached! % 10.74/2.66 % (1249802)------------------------------ % 10.74/2.66 % (1249802)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.74/2.66 % (1249802)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.74/2.66 % (1249802)CaDiCaL version: 2.1.3 % 10.74/2.66 % (1249802)Termination reason: Instruction limit % 10.74/2.66 % (1249802)Termination phase: Saturation % 10.74/2.66 % (1249802)Time elapsed: 0.068 s % 10.74/2.66 % (1249802)Peak memory usage: 113 MB % 10.74/2.66 % (1249802)Instructions burned: 128 (million) % 10.74/2.66 % (1249803)dis+10_1_si=on:random_seed=1613057168:i=10:ep=R:rtra=on_2990 on theBenchmark for (2990ds/10Mi) % 10.74/2.66 % (1249803)Instruction limit reached! % 10.74/2.66 % (1249803)------------------------------ % 10.74/2.66 % (1249803)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.74/2.66 % (1249803)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.74/2.66 % (1249803)CaDiCaL version: 2.1.3 % 10.74/2.66 % (1249803)Termination reason: Instruction limit % 10.74/2.66 % (1249803)Termination phase: Property scanning % 10.74/2.66 % (1249803)Time elapsed: 0.010 s % 10.74/2.66 % (1249803)Peak memory usage: 86 MB % 10.74/2.66 % (1249803)Instructions burned: 11 (million) % 10.74/2.66 % (1249787)------------------------------ % 10.74/2.66 % (1249787)------------------------------ % 10.74/2.66 % (1249804)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=1395279770:i=26:canc=cautious:av=off:rtra=on_2990 on theBenchmark for (2990ds/26Mi) % 13.02/3.02 % (1249806)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=282999962:avsq=on:i=35:doe=on:thsqd=64:nm=64:fsr=off:thsqc=32:rtra=on:tac=light:ss=included:thsq=on:ev=off:sgt=32_2990 on theBenchmark for (2990ds/35Mi) % 13.02/3.02 % (1249804)Instruction limit reached! % 13.02/3.02 % (1249804)------------------------------ % 13.02/3.02 % (1249804)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.02/3.02 % (1249804)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.02/3.02 % (1249804)CaDiCaL version: 2.1.3 % 13.02/3.02 % (1249804)Termination reason: Instruction limit % 13.02/3.02 % (1249804)Termination phase: Saturation % 13.02/3.02 % (1249804)Time elapsed: 0.022 s % 13.02/3.02 % (1249804)Peak memory usage: 88 MB % 13.02/3.02 % (1249804)Instructions burned: 26 (million) % 13.02/3.02 % (1249806)Instruction limit reached! % 13.02/3.02 % (1249806)------------------------------ % 13.02/3.02 % (1249806)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.02/3.02 % (1249806)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.02/3.02 % (1249806)CaDiCaL version: 2.1.3 % 13.02/3.02 % (1249806)Termination reason: Instruction limit % 13.02/3.02 % (1249806)Termination phase: Saturation % 13.02/3.02 % (1249806)Time elapsed: 0.030 s % 13.02/3.02 % (1249806)Peak memory usage: 89 MB % 13.02/3.02 % (1249806)Instructions burned: 35 (million) % 13.02/3.02 % (1249808)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=896408271:i=2:fsr=off:rtra=on:inst=on_2989 on theBenchmark for (2989ds/2Mi) % 13.02/3.02 % (1249808)Instruction limit reached! % 13.02/3.02 % (1249808)------------------------------ % 13.02/3.02 % (1249808)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.02/3.02 % (1249808)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.02/3.02 % (1249808)CaDiCaL version: 2.1.3 % 13.02/3.02 % (1249808)Termination reason: Instruction limit % 13.02/3.02 % (1249808)Termination phase: Property scanning % 13.02/3.02 % (1249808)Time elapsed: 0.003 s % 13.02/3.02 % (1249808)Peak memory usage: 85 MB % 13.02/3.02 % (1249808)Instructions burned: 2 (million) % 13.02/3.02 % (1249811)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=651851658:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2989 on theBenchmark for (2989ds/8Mi) % 13.02/3.02 % (1249811)Instruction limit reached! % 13.02/3.02 % (1249811)------------------------------ % 13.02/3.02 % (1249811)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.02/3.02 % (1249811)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.02/3.02 % (1249811)CaDiCaL version: 2.1.3 % 13.02/3.02 % (1249811)Termination reason: Instruction limit % 13.02/3.02 % (1249811)Termination phase: SInE selection % 13.02/3.02 % (1249811)Time elapsed: 0.007 s % 13.02/3.02 % (1249811)Peak memory usage: 85 MB % 13.02/3.02 % (1249811)Instructions burned: 8 (million) % 13.02/3.02 % (1249812)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=2544264552:i=370:ep=RS:fsr=off:rtra=on_2988 on theBenchmark for (2988ds/370Mi) % 13.02/3.02 % (1249812)Refutation not found, incomplete strategy % 13.02/3.02 % (1249812)------------------------------ % 13.02/3.02 % (1249812)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.02/3.02 % (1249812)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.02/3.02 % (1249812)CaDiCaL version: 2.1.3 % 13.02/3.02 % (1249812)Termination reason: Refutation not found, incomplete strategy % 13.02/3.02 % (1249812)Time elapsed: 0.011 s % 13.02/3.02 % (1249812)Peak memory usage: 89 MB % 13.02/3.02 % (1249812)Instructions burned: 25 (million) % 13.02/3.02 % (1249814)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=2649152380:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2988 on theBenchmark for (2988ds/13Mi) % 13.02/3.02 % (1249814)Instruction limit reached! % 13.02/3.02 % (1249814)------------------------------ % 13.02/3.02 % (1249814)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.02/3.02 % (1249814)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.02/3.02 % (1249814)CaDiCaL version: 2.1.3 % 13.02/3.02 % (1249814)Termination reason: Instruction limit % 13.02/3.02 % (1249814)Termination phase: Property scanning % 13.02/3.02 % (1249814)Time elapsed: 0.011 s % 13.02/3.02 % (1249814)Peak memory usage: 85 MB % 13.02/3.02 % (1249814)Instructions burned: 13 (million) % 16.92/3.40 % (1249818)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=3818812657:i=10:rtra=on_2987 on theBenchmark for (2987ds/10Mi) % 16.92/3.40 % (1249818)Instruction limit reached! % 16.92/3.40 % (1249818)------------------------------ % 16.92/3.40 % (1249818)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.92/3.40 % (1249818)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.92/3.40 % (1249818)CaDiCaL version: 2.1.3 % 16.92/3.40 % (1249818)Termination reason: Instruction limit % 16.92/3.40 % (1249818)Termination phase: Saturation % 16.92/3.40 % (1249818)Time elapsed: 0.009 s % 16.92/3.40 % (1249818)Peak memory usage: 87 MB % 16.92/3.40 % (1249818)Instructions burned: 10 (million) % 16.92/3.40 % (1249817)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=3586420950:i=226:rtra=on:gtg=position:ss=axioms_2988 on theBenchmark for (2988ds/226Mi) % 16.92/3.40 % (1249819)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=1721137199:i=71:rtra=on:gtg=exists_top_2987 on theBenchmark for (2987ds/71Mi) % 16.92/3.40 % (1249817)Refutation not found, incomplete strategy % 16.92/3.40 % (1249817)------------------------------ % 16.92/3.40 % (1249817)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.92/3.40 % (1249817)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.92/3.40 % (1249817)CaDiCaL version: 2.1.3 % 16.92/3.40 % (1249817)Termination reason: Refutation not found, incomplete strategy % 16.92/3.40 % (1249817)Time elapsed: 0.045 s % 16.92/3.40 % (1249817)Peak memory usage: 111 MB % 16.92/3.40 % (1249817)Instructions burned: 16 (million) % 16.92/3.40 % (1249823)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=1520040462:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2987 on theBenchmark for (2987ds/294Mi) % 16.92/3.40 % (1249821)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=3981416182:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2987 on theBenchmark for (2987ds/75Mi) % 16.92/3.40 % (1249821)Instruction limit reached! % 16.92/3.40 % (1249821)------------------------------ % 16.92/3.40 % (1249821)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.92/3.40 % (1249821)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.92/3.40 % (1249821)CaDiCaL version: 2.1.3 % 16.92/3.40 % (1249821)Termination reason: Instruction limit % 16.92/3.40 % (1249821)Termination phase: Saturation % 16.92/3.40 % (1249821)Time elapsed: 0.062 s % 16.92/3.40 % (1249821)Peak memory usage: 90 MB % 16.92/3.40 % (1249821)Instructions burned: 76 (million) % 16.92/3.40 % (1249812)------------------------------ % 16.92/3.40 % (1249812)------------------------------ % 16.92/3.40 % (1249819)Instruction limit reached! % 16.92/3.40 % (1249819)------------------------------ % 16.92/3.40 % (1249819)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.92/3.40 % (1249819)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.92/3.40 % (1249819)CaDiCaL version: 2.1.3 % 16.92/3.40 % (1249819)Termination reason: Instruction limit % 16.92/3.40 % (1249819)Termination phase: Saturation % 16.92/3.40 % (1249819)Time elapsed: 0.112 s % 16.92/3.40 % (1249819)Peak memory usage: 129 MB % 16.92/3.40 % (1249819)Instructions burned: 71 (million) % 16.92/3.40 % (1249826)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=4029547835:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2986 on theBenchmark for (2986ds/130Mi) % 16.92/3.40 % (1249829)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=2598164326:i=131:rtra=on_2985 on theBenchmark for (2985ds/131Mi) % 16.92/3.40 % (1249823)Instruction limit reached! % 16.92/3.40 % (1249823)------------------------------ % 16.92/3.40 % (1249823)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.92/3.40 % (1249823)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.92/3.40 % (1249823)CaDiCaL version: 2.1.3 % 16.92/3.40 % (1249823)Termination reason: Instruction limit % 16.92/3.40 % (1249823)Termination phase: Saturation % 16.92/3.40 % (1249823)Time elapsed: 0.228 s % 16.92/3.40 % (1249823)Peak memory usage: 89 MB % 16.92/3.40 % (1249823)Instructions burned: 295 (million) % 16.92/3.40 % (1249834)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=1690007759:i=307:rtra=on:gtg=exists_top_2984 on theBenchmark for (2984ds/307Mi) % 18.36/3.86 % (1249834)Refutation not found, incomplete strategy % 18.36/3.86 % (1249834)------------------------------ % 18.36/3.86 % (1249834)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.36/3.86 % (1249834)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.36/3.86 % (1249834)CaDiCaL version: 2.1.3 % 18.36/3.86 % (1249834)Termination reason: Refutation not found, incomplete strategy % 18.36/3.86 % (1249834)Time elapsed: 0.016 s % 18.36/3.86 % (1249834)Peak memory usage: 89 MB % 18.36/3.86 % (1249834)Instructions burned: 35 (million) % 18.36/3.86 % (1249835)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=298881052:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2984 on theBenchmark for (2984ds/598Mi) % 18.36/3.86 % (1249833)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=3611910916:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2984 on theBenchmark for (2984ds/40Mi) % 18.36/3.86 % (1249826)Instruction limit reached! % 18.36/3.86 % (1249826)------------------------------ % 18.36/3.86 % (1249826)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.36/3.86 % (1249826)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.36/3.86 % (1249826)CaDiCaL version: 2.1.3 % 18.36/3.86 % (1249826)Termination reason: Instruction limit % 18.36/3.86 % (1249826)Termination phase: Saturation % 18.36/3.86 % (1249826)Time elapsed: 0.143 s % 18.36/3.86 % (1249826)Peak memory usage: 116 MB % 18.36/3.86 % (1249826)Instructions burned: 130 (million) % 18.36/3.86 % (1249829)Instruction limit reached! % 18.36/3.86 % (1249829)------------------------------ % 18.36/3.86 % (1249829)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.36/3.86 % (1249829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.36/3.86 % (1249829)CaDiCaL version: 2.1.3 % 18.36/3.86 % (1249829)Termination reason: Instruction limit % 18.36/3.86 % (1249829)Termination phase: Saturation % 18.36/3.86 % (1249829)Time elapsed: 0.164 s % 18.36/3.86 % (1249829)Peak memory usage: 133 MB % 18.36/3.86 % (1249829)Instructions burned: 131 (million) % 18.36/3.86 % (1249833)Instruction limit reached! % 18.36/3.86 % (1249833)------------------------------ % 18.36/3.86 % (1249833)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.36/3.86 % (1249833)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.36/3.86 % (1249833)CaDiCaL version: 2.1.3 % 18.36/3.86 % (1249833)Termination reason: Instruction limit % 18.36/3.86 % (1249833)Termination phase: Saturation % 18.36/3.86 % (1249833)Time elapsed: 0.086 s % 18.36/3.86 % (1249833)Peak memory usage: 128 MB % 18.36/3.86 % (1249833)Instructions burned: 40 (million) % 18.36/3.86 % (1249817)------------------------------ % 18.36/3.86 % (1249817)------------------------------ % 18.36/3.86 % (1249839)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=4066858078:i=131:canc=cautious:fsr=off:rtra=on_2982 on theBenchmark for (2982ds/131Mi) % 18.36/3.86 % (1249843)dis+10_1_si=on:random_seed=80832088:s2a=on:i=1000:rtra=on:gtg=exists_all_2981 on theBenchmark for (2981ds/1000Mi) % 18.36/3.86 % (1249842)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=2406496910:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2981 on theBenchmark for (2981ds/259Mi) % 18.36/3.86 % (1249835)Instruction limit reached! % 18.36/3.86 % (1249835)------------------------------ % 18.36/3.86 % (1249835)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.36/3.86 % (1249835)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.36/3.86 % (1249835)CaDiCaL version: 2.1.3 % 18.36/3.86 % (1249835)Termination reason: Instruction limit % 18.36/3.86 % (1249835)Termination phase: Saturation % 18.36/3.86 % (1249835)Time elapsed: 0.283 s % 18.36/3.86 % (1249835)Peak memory usage: 135 MB % 18.36/3.86 % (1249835)Instructions burned: 600 (million) % 18.36/3.86 % (1249842)Refutation not found, incomplete strategy % 18.36/3.86 % (1249842)------------------------------ % 18.36/3.86 % (1249842)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.36/3.86 % (1249842)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.36/3.86 % (1249842)CaDiCaL version: 2.1.3 % 18.36/3.86 % (1249842)Termination reason: Refutation not found, incomplete strategy % 18.36/3.86 % (1249842)Time elapsed: 0.045 s % 18.36/3.86 % (1249842)Peak memory usage: 111 MB % 23.26/4.25 % (1249842)Instructions burned: 17 (million) % 23.26/4.25 % (1249839)Instruction limit reached! % 23.26/4.25 % (1249839)------------------------------ % 23.26/4.25 % (1249839)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.26/4.25 % (1249839)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.26/4.25 % (1249839)CaDiCaL version: 2.1.3 % 23.26/4.25 % (1249839)Termination reason: Instruction limit % 23.26/4.25 % (1249839)Termination phase: Saturation % 23.26/4.25 % (1249839)Time elapsed: 0.124 s % 23.26/4.25 % (1249839)Peak memory usage: 112 MB % 23.26/4.25 % (1249839)Instructions burned: 132 (million) % 23.26/4.25 % (1249845)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=1697964935:i=141:doe=on:rtra=on_2981 on theBenchmark for (2981ds/141Mi) % 23.26/4.25 % (1249844)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=3108331298:i=383:fsr=off:rtra=on:ev=force_2981 on theBenchmark for (2981ds/383Mi) % 23.26/4.25 % (1249834)------------------------------ % 23.26/4.25 % (1249834)------------------------------ % 23.26/4.25 % (1249845)Instruction limit reached! % 23.26/4.25 % (1249845)------------------------------ % 23.26/4.25 % (1249845)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.26/4.25 % (1249845)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.26/4.25 % (1249845)CaDiCaL version: 2.1.3 % 23.26/4.25 % (1249845)Termination reason: Instruction limit % 23.26/4.25 % (1249845)Termination phase: Saturation % 23.26/4.25 % (1249845)Time elapsed: 0.103 s % 23.26/4.25 % (1249845)Peak memory usage: 88 MB % 23.26/4.25 % (1249845)Instructions burned: 142 (million) % 23.26/4.25 % (1249849)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=3559064976:i=65:nm=16:rtra=on_2979 on theBenchmark for (2979ds/65Mi) % 23.26/4.25 % (1249849)Refutation not found, incomplete strategy % 23.26/4.25 % (1249849)------------------------------ % 23.26/4.25 % (1249849)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.26/4.25 % (1249849)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.26/4.25 % (1249849)CaDiCaL version: 2.1.3 % 23.26/4.25 % (1249849)Termination reason: Refutation not found, incomplete strategy % 23.26/4.25 % (1249849)Time elapsed: 0.036 s % 23.26/4.25 % (1249849)Peak memory usage: 112 MB % 23.26/4.25 % (1249849)Instructions burned: 36 (million) % 23.26/4.25 % (1249852)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=2809595739:i=121:nm=16:rtra=on_2978 on theBenchmark for (2978ds/121Mi) % 23.26/4.25 % (1249853)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=7571675:s2a=on:i=128:s2at=5:ins=3:rtra=on_2978 on theBenchmark for (2978ds/128Mi) % 23.26/4.25 % (1249844)Instruction limit reached! % 23.26/4.25 % (1249844)------------------------------ % 23.26/4.25 % (1249844)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.26/4.25 % (1249844)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.26/4.25 % (1249844)CaDiCaL version: 2.1.3 % 23.26/4.25 % (1249844)Termination reason: Instruction limit % 23.26/4.25 % (1249844)Termination phase: Saturation % 23.26/4.25 % (1249844)Time elapsed: 0.292 s % 23.26/4.25 % (1249844)Peak memory usage: 90 MB % 23.26/4.25 % (1249844)Instructions burned: 384 (million) % 23.26/4.25 % (1249852)Instruction limit reached! % 23.26/4.25 % (1249852)------------------------------ % 23.26/4.25 % (1249852)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.26/4.25 % (1249852)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.26/4.25 % (1249852)CaDiCaL version: 2.1.3 % 23.26/4.25 % (1249852)Termination reason: Instruction limit % 23.26/4.25 % (1249852)Termination phase: Saturation % 23.26/4.25 % (1249852)Time elapsed: 0.092 s % 23.26/4.25 % (1249852)Peak memory usage: 89 MB % 23.26/4.25 % (1249852)Instructions burned: 121 (million) % 23.26/4.25 % (1249853)Refutation not found, incomplete strategy % 23.26/4.25 % (1249853)------------------------------ % 23.26/4.25 % (1249853)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.26/4.25 % (1249853)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.26/4.25 % (1249853)CaDiCaL version: 2.1.3 % 23.26/4.25 % (1249853)Termination reason: Refutation not found, incomplete strategy % 23.26/4.25 % (1249853)Time elapsed: 0.071 s % 23.26/4.25 % (1249853)Peak memory usage: 113 MB % 23.26/4.25 % (1249853)Instructions burned: 46 (million) % 25.45/4.79 % (1249842)------------------------------ % 25.45/4.79 % (1249842)------------------------------ % 25.45/4.79 % (1249854)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=1664295772:i=39:ins=3:rtra=on_2977 on theBenchmark for (2977ds/39Mi) % 25.45/4.79 % (1249854)Instruction limit reached! % 25.45/4.79 % (1249854)------------------------------ % 25.45/4.79 % (1249854)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.45/4.79 % (1249854)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.45/4.79 % (1249854)CaDiCaL version: 2.1.3 % 25.45/4.79 % (1249854)Termination reason: Instruction limit % 25.45/4.79 % (1249854)Termination phase: Saturation % 25.45/4.79 % (1249854)Time elapsed: 0.032 s % 25.45/4.79 % (1249854)Peak memory usage: 88 MB % 25.45/4.79 % (1249854)Instructions burned: 39 (million) % 25.45/4.79 % (1249849)------------------------------ % 25.45/4.79 % (1249849)------------------------------ % 25.45/4.79 % (1249858)dis+1010_1_to=kbo:si=on:random_seed=846520609:i=175:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2975 on theBenchmark for (2975ds/175Mi) % 25.45/4.79 % (1249861)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=2843441418:s2a=on:i=483:doe=on:nm=32:rtra=on_2975 on theBenchmark for (2975ds/483Mi) % 25.45/4.79 % (1249859)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=3867606818:i=329:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2975 on theBenchmark for (2975ds/329Mi) % 25.45/4.79 % (1249843)Instruction limit reached! % 25.45/4.79 % (1249843)------------------------------ % 25.45/4.79 % (1249843)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.45/4.79 % (1249843)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.45/4.79 % (1249843)CaDiCaL version: 2.1.3 % 25.45/4.79 % (1249843)Termination reason: Instruction limit % 25.45/4.79 % (1249843)Termination phase: Saturation % 25.45/4.79 % (1249843)Time elapsed: 0.674 s % 25.45/4.79 % (1249843)Peak memory usage: 89 MB % 25.45/4.79 % (1249843)Instructions burned: 1000 (million) % 25.45/4.79 % (1249862)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=2420139650:thitd=on:i=215:nm=0:rtra=on:ev=force_2974 on theBenchmark for (2974ds/215Mi) % 25.45/4.79 % (1249863)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=3441842793:i=349:rtra=on_2974 on theBenchmark for (2974ds/349Mi) % 25.45/4.79 % (1249858)Instruction limit reached! % 25.45/4.79 % (1249858)------------------------------ % 25.45/4.79 % (1249858)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.45/4.79 % (1249858)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.45/4.79 % (1249858)CaDiCaL version: 2.1.3 % 25.45/4.79 % (1249858)Termination reason: Instruction limit % 25.45/4.79 % (1249858)Termination phase: Saturation % 25.45/4.79 % (1249858)Time elapsed: 0.137 s % 25.45/4.79 % (1249858)Peak memory usage: 90 MB % 25.45/4.79 % (1249858)Instructions burned: 175 (million) % 25.45/4.79 % (1249853)------------------------------ % 25.45/4.79 % (1249853)------------------------------ % 25.45/4.79 % (1249861)Instruction limit reached! % 25.45/4.79 % (1249861)------------------------------ % 25.45/4.79 % (1249861)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.45/4.79 % (1249861)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.45/4.79 % (1249861)CaDiCaL version: 2.1.3 % 25.45/4.79 % (1249861)Termination reason: Instruction limit % 25.45/4.79 % (1249861)Termination phase: Saturation % 25.45/4.79 % (1249861)Time elapsed: 0.230 s % 25.45/4.79 % (1249861)Peak memory usage: 134 MB % 25.45/4.79 % (1249861)Instructions burned: 485 (million) % 25.45/4.79 % (1249867)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=3827611018:st=2:i=295:rtra=on:ss=axioms_2973 on theBenchmark for (2973ds/295Mi) % 25.45/4.79 % (1249867)Refutation not found, incomplete strategy % 25.45/4.79 % (1249867)------------------------------ % 25.45/4.79 % (1249867)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.45/4.79 % (1249867)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.45/4.79 % (1249867)CaDiCaL version: 2.1.3 % 25.45/4.79 % (1249867)Termination reason: Refutation not found, incomplete strategy % 25.45/4.79 % (1249867)Time elapsed: 0.010 s % 25.45/4.79 % (1249867)Peak memory usage: 88 MB % 25.45/4.79 % (1249867)Instructions burned: 12 (million) % 29.34/5.12 % (1249859)Instruction limit reached! % 29.34/5.12 % (1249859)------------------------------ % 29.34/5.12 % (1249859)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.34/5.12 % (1249859)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.34/5.12 % (1249859)CaDiCaL version: 2.1.3 % 29.34/5.12 % (1249859)Termination reason: Instruction limit % 29.34/5.12 % (1249859)Termination phase: Saturation % 29.34/5.12 % (1249859)Time elapsed: 0.272 s % 29.34/5.12 % (1249859)Peak memory usage: 117 MB % 29.34/5.12 % (1249859)Instructions burned: 330 (million) % 29.34/5.12 % (1249862)Instruction limit reached! % 29.34/5.12 % (1249862)------------------------------ % 29.34/5.12 % (1249862)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.34/5.12 % (1249862)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.34/5.12 % (1249862)CaDiCaL version: 2.1.3 % 29.34/5.12 % (1249862)Termination reason: Instruction limit % 29.34/5.12 % (1249862)Termination phase: Saturation % 29.34/5.12 % (1249862)Time elapsed: 0.240 s % 29.34/5.12 % (1249862)Peak memory usage: 135 MB % 29.34/5.12 % (1249862)Instructions burned: 215 (million) % 29.34/5.12 % (1249870)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=418084142:i=328:kws=inv_frequency:nm=20:rtra=on_2972 on theBenchmark for (2972ds/328Mi) % 29.34/5.12 % (1249872)lrs+1010_1_to=kbo:sil=128000:si=on:sos=on:urr=on:uwa=alasca_main:random_seed=1106895989:i=484:doe=on:nm=0:av=off:rtra=on:ss=axioms_2971 on theBenchmark for (2971ds/484Mi) % 29.34/5.12 % (1249871)dis+1010_1_to=lpo:sil=128000:sas=z3:si=on:nwc=5:random_seed=3914190755:i=281:gtgl=2:rtra=on:gtg=all_2971 on theBenchmark for (2971ds/281Mi) % 29.34/5.12 % (1249872)Refutation not found, incomplete strategy % 29.34/5.12 % (1249872)------------------------------ % 29.34/5.12 % (1249872)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.34/5.12 % (1249872)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.34/5.12 % (1249872)CaDiCaL version: 2.1.3 % 29.34/5.12 % (1249872)Termination reason: Refutation not found, incomplete strategy % 29.34/5.12 % (1249872)Time elapsed: 0.005 s % 29.34/5.12 % (1249872)Peak memory usage: 88 MB % 29.34/5.12 % (1249872)Instructions burned: 11 (million) % 29.34/5.12 % (1249863)Instruction limit reached! % 29.34/5.12 % (1249863)------------------------------ % 29.34/5.12 % (1249863)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.34/5.12 % (1249863)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.34/5.12 % (1249863)CaDiCaL version: 2.1.3 % 29.34/5.12 % (1249863)Termination reason: Instruction limit % 29.34/5.12 % (1249863)Termination phase: Saturation % 29.34/5.12 % (1249863)Time elapsed: 0.296 s % 29.34/5.12 % (1249863)Peak memory usage: 117 MB % 29.34/5.12 % (1249863)Instructions burned: 350 (million) % 29.34/5.12 % (1249874)lrs+21_1_to=kbo:sil=128000:thi=neg_eq:si=on:random_seed=1048041823:i=321:canc=force:rtra=on:tac=axiom:ss=axioms:ev=force_2970 on theBenchmark for (2970ds/321Mi) % 29.34/5.12 % (1249874)Refutation not found, incomplete strategy % 29.34/5.12 % (1249874)------------------------------ % 29.34/5.12 % (1249874)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.34/5.12 % (1249874)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.34/5.12 % (1249874)CaDiCaL version: 2.1.3 % 29.34/5.12 % (1249874)Termination reason: Refutation not found, incomplete strategy % 29.34/5.12 % (1249874)Time elapsed: 0.046 s % 29.34/5.12 % (1249874)Peak memory usage: 112 MB % 29.34/5.12 % (1249874)Instructions burned: 16 (million) % 29.34/5.12 % (1249875)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=3237431362:i=416:rtra=on:gtg=position:ss=axioms_2969 on theBenchmark for (2969ds/416Mi) % 29.34/5.12 % (1249872)------------------------------ % 29.34/5.12 % (1249872)------------------------------ % 29.34/5.12 % (1249870)Instruction limit reached! % 29.34/5.12 % (1249870)------------------------------ % 29.34/5.12 % (1249870)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.34/5.12 % (1249870)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.34/5.12 % (1249870)CaDiCaL version: 2.1.3 % 29.34/5.12 % (1249870)Termination reason: Instruction limit % 29.34/5.12 % (1249870)Termination phase: Saturation % 29.34/5.12 % (1249870)Time elapsed: 0.279 s % 29.34/5.12 % (1249870)Peak memory usage: 117 MB % 29.34/5.12 % (1249870)Instructions burned: 328 (million) % 29.34/5.12 % (1249867)------------------------------ % 30.90/5.63 % (1249867)------------------------------ % 30.90/5.63 % (1249871)Instruction limit reached! % 30.90/5.63 % (1249871)------------------------------ % 30.90/5.63 % (1249871)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 30.90/5.63 % (1249871)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.90/5.63 % (1249871)CaDiCaL version: 2.1.3 % 30.90/5.63 % (1249871)Termination reason: Instruction limit % 30.90/5.63 % (1249871)Termination phase: Saturation % 30.90/5.63 % (1249871)Time elapsed: 0.256 s % 30.90/5.63 % (1249871)Peak memory usage: 116 MB % 30.90/5.63 % (1249871)Instructions burned: 281 (million) % 30.90/5.63 % (1249875)Refutation not found, incomplete strategy % 30.90/5.63 % (1249875)------------------------------ % 30.90/5.63 % (1249875)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 30.90/5.63 % (1249875)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.90/5.63 % (1249875)CaDiCaL version: 2.1.3 % 30.90/5.63 % (1249875)Termination reason: Refutation not found, incomplete strategy % 30.90/5.63 % (1249875)Time elapsed: 0.046 s % 30.90/5.63 % (1249875)Peak memory usage: 111 MB % 30.90/5.63 % (1249875)Instructions burned: 16 (million) % 30.90/5.63 % (1249879)lrs+1010_1_to=kbo:tgt=ground:fde=unused:sas=z3:si=on:sp=unary_frequency:gve=force:spb=goal:tha=off:random_seed=845794734:i=471:thf=on:kws=precedence:rtra=on_2969 on theBenchmark for (2969ds/471Mi) % 30.90/5.63 % (1249882)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=3983745954:avsq=on:i=276:avsqr=1,2:rtra=on_2967 on theBenchmark for (2967ds/276Mi) % 30.90/5.63 % (1249885)lrs+10_1_to=kbo:sil=128000:tgt=full:sas=z3:si=on:uwa=func_ext:slsqc=1:flr=on:slsq=on:random_seed=3838977183:i=387:bd=preordered:rtra=on:ss=axioms:sgt=8_2966 on theBenchmark for (2966ds/387Mi) % 30.90/5.63 % (1249886)lrs+10_1_to=kbo:sil=128000:fde=none:si=on:norm_ineq=on:urr=on:nwc=0.5:random_seed=1814362698:i=513:kws=frequency:bd=all:rtra=on:gtg=exists_all:ss=axioms:sgt=4_2966 on theBenchmark for (2966ds/513Mi) % 30.90/5.63 % (1249883)lrs+1010_2_to=kbo:sil=128000:tgt=ground:fde=unused:sas=z3:si=on:uwa=off:tha=off:nwc=1:random_seed=3487651121:i=375:kws=inv_arity_squared:rtra=on_2966 on theBenchmark for (2966ds/375Mi) % 30.90/5.63 % (1249885)Refutation not found, incomplete strategy % 30.90/5.63 % (1249885)------------------------------ % 30.90/5.63 % (1249885)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 30.90/5.63 % (1249885)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.90/5.63 % (1249885)CaDiCaL version: 2.1.3 % 30.90/5.63 % (1249885)Termination reason: Refutation not found, incomplete strategy % 30.90/5.63 % (1249885)Time elapsed: 0.045 s % 30.90/5.63 % (1249885)Peak memory usage: 111 MB % 30.90/5.63 % (1249885)Instructions burned: 17 (million) % 30.90/5.63 % (1249874)------------------------------ % 30.90/5.63 % (1249874)------------------------------ % 30.90/5.63 % (1249882)Instruction limit reached! % 30.90/5.63 % (1249882)------------------------------ % 30.90/5.63 % (1249882)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 30.90/5.63 % (1249882)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.90/5.63 % (1249882)CaDiCaL version: 2.1.3 % 30.90/5.63 % (1249882)Termination reason: Instruction limit % 30.90/5.63 % (1249882)Termination phase: Saturation % 30.90/5.63 % (1249882)Time elapsed: 0.164 s % 30.90/5.63 % (1249882)Peak memory usage: 134 MB % 30.90/5.63 % (1249882)Instructions burned: 278 (million) % 30.90/5.63 % (1249879)Instruction limit reached! % 30.90/5.63 % (1249879)------------------------------ % 30.90/5.63 % (1249879)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 30.90/5.63 % (1249879)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.90/5.63 % (1249879)CaDiCaL version: 2.1.3 % 30.90/5.63 % (1249879)Termination reason: Instruction limit % 30.90/5.63 % (1249879)Termination phase: Saturation % 30.90/5.63 % (1249879)Time elapsed: 0.354 s % 30.90/5.63 % (1249879)Peak memory usage: 112 MB % 30.90/5.63 % (1249879)Instructions burned: 471 (million) % 30.90/5.63 % (1249875)------------------------------ % 30.90/5.63 % (1249875)------------------------------ % 30.90/5.63 % (1249893)lrs+1010_1_to=kbo:sil=64000:sas=cadical:si=on:sos=on:bce=on:random_seed=1092332607:i=359:rtra=on:gtg=exists_top:ss=axioms_2963 on theBenchmark for (2963ds/359Mi) % 30.90/5.63 % (1249892)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=2296135390:i=334:rtra=on_2963 on theBenchmark for (2963ds/334Mi) % 37.38/6.29 % (1249893)Refutation not found, incomplete strategy % 37.38/6.29 % (1249893)------------------------------ % 37.38/6.29 % (1249893)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 37.38/6.29 % (1249893)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.38/6.29 % (1249893)CaDiCaL version: 2.1.3 % 37.38/6.29 % (1249893)Termination reason: Refutation not found, incomplete strategy % 37.38/6.29 % (1249893)Time elapsed: 0.007 s % 37.38/6.29 % (1249893)Peak memory usage: 88 MB % 37.38/6.29 % (1249893)Instructions burned: 15 (million) % 37.38/6.29 % (1249894)dis+1010_1_to=lpo:sil=128000:thi=all:fde=unused:si=on:sp=reverse_arity:tha=off:random_seed=2702897499:i=341:gtgl=2:rtra=on:gtg=exists_sym:ev=force:fsd=on:fsdmm=1_2963 on theBenchmark for (2963ds/341Mi) % 37.38/6.29 % (1249883)Instruction limit reached! % 37.38/6.29 % (1249883)------------------------------ % 37.38/6.29 % (1249883)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 37.38/6.29 % (1249883)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.38/6.29 % (1249883)CaDiCaL version: 2.1.3 % 37.38/6.29 % (1249883)Termination reason: Instruction limit % 37.38/6.29 % (1249883)Termination phase: Saturation % 37.38/6.29 % (1249883)Time elapsed: 0.316 s % 37.38/6.29 % (1249883)Peak memory usage: 117 MB % 37.38/6.29 % (1249883)Instructions burned: 375 (million) % 37.38/6.29 % (1249886)Instruction limit reached! % 37.38/6.29 % (1249886)------------------------------ % 37.38/6.29 % (1249886)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 37.38/6.29 % (1249886)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.38/6.29 % (1249886)CaDiCaL version: 2.1.3 % 37.38/6.29 % (1249886)Termination reason: Instruction limit % 37.38/6.29 % (1249886)Termination phase: Saturation % 37.38/6.29 % (1249886)Time elapsed: 0.364 s % 37.38/6.29 % (1249886)Peak memory usage: 89 MB % 37.38/6.29 % (1249886)Instructions burned: 513 (million) % 37.38/6.29 % (1249895)lrs-2_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_max:tha=off:random_seed=3376141538:st=1.5:i=261:sd=1:kws=precedence:rtra=on:ss=axioms_2962 on theBenchmark for (2962ds/261Mi) % 37.38/6.29 % (1249885)------------------------------ % 37.38/6.29 % (1249885)------------------------------ % 37.38/6.29 % (1249895)Refutation not found, incomplete strategy % 37.38/6.29 % (1249895)------------------------------ % 37.38/6.29 % (1249895)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 37.38/6.29 % (1249895)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.38/6.29 % (1249895)CaDiCaL version: 2.1.3 % 37.38/6.29 % (1249895)Termination reason: Refutation not found, incomplete strategy % 37.38/6.29 % (1249895)Time elapsed: 0.042 s % 37.38/6.29 % (1249895)Peak memory usage: 111 MB % 37.38/6.29 % (1249895)Instructions burned: 13 (million) % 37.38/6.29 % (1249893)------------------------------ % 37.38/6.29 % (1249893)------------------------------ % 37.38/6.29 % (1249900)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=3037715813:s2pl=no:i=235:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2961 on theBenchmark for (2961ds/235Mi) % 37.38/6.29 % (1249894)Instruction limit reached! % 37.38/6.29 % (1249894)------------------------------ % 37.38/6.29 % (1249894)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 37.38/6.29 % (1249894)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.38/6.29 % (1249894)CaDiCaL version: 2.1.3 % 37.38/6.29 % (1249894)Termination reason: Instruction limit % 37.38/6.29 % (1249894)Termination phase: Saturation % 37.38/6.29 % (1249894)Time elapsed: 0.270 s % 37.38/6.29 % (1249894)Peak memory usage: 117 MB % 37.38/6.29 % (1249894)Instructions burned: 341 (million) % 37.38/6.29 % (1249900)Refutation not found, incomplete strategy % 37.38/6.29 % (1249900)------------------------------ % 37.38/6.29 % (1249900)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 37.38/6.29 % (1249900)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.38/6.29 % (1249900)CaDiCaL version: 2.1.3 % 37.38/6.29 % (1249900)Termination reason: Refutation not found, incomplete strategy % 37.38/6.29 % (1249900)Time elapsed: 0.047 s % 37.38/6.29 % (1249900)Peak memory usage: 111 MB % 37.38/6.29 % (1249900)Instructions burned: 17 (million) % 37.38/6.29 % (1249892)Instruction limit reached! % 37.38/6.29 % (1249892)------------------------------ % 40.09/7.02 % (1249892)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 40.09/7.02 % (1249892)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.09/7.02 % (1249892)CaDiCaL version: 2.1.3 % 40.09/7.02 % (1249892)Termination reason: Instruction limit % 40.09/7.02 % (1249892)Termination phase: Saturation % 40.09/7.02 % (1249892)Time elapsed: 0.326 s % 40.09/7.02 % (1249892)Peak memory usage: 134 MB % 40.09/7.02 % (1249892)Instructions burned: 335 (million) % 40.09/7.02 % (1249901)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=2810459643:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2960 on theBenchmark for (2960ds/273Mi) % 40.09/7.02 % (1249903)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=3475328260:i=146:doe=on:rtra=on_2959 on theBenchmark for (2959ds/146Mi) % 40.09/7.02 % (1249901)Instruction limit reached! % 40.09/7.02 % (1249901)------------------------------ % 40.09/7.02 % (1249901)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 40.09/7.02 % (1249901)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.09/7.02 % (1249901)CaDiCaL version: 2.1.3 % 40.09/7.02 % (1249901)Termination reason: Instruction limit % 40.09/7.02 % (1249901)Termination phase: Saturation % 40.09/7.02 % (1249901)Time elapsed: 0.112 s % 40.09/7.02 % (1249901)Peak memory usage: 90 MB % 40.09/7.02 % (1249901)Instructions burned: 275 (million) % 40.09/7.02 % (1249905)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=3432813194:i=4428:doe=on:fsr=off:rtra=on_2959 on theBenchmark for (2959ds/4428Mi) % 40.09/7.02 % (1249903)Instruction limit reached! % 40.09/7.02 % (1249903)------------------------------ % 40.09/7.02 % (1249903)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 40.09/7.02 % (1249903)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.09/7.02 % (1249903)CaDiCaL version: 2.1.3 % 40.09/7.02 % (1249903)Termination reason: Instruction limit % 40.09/7.02 % (1249903)Termination phase: Saturation % 40.09/7.02 % (1249903)Time elapsed: 0.108 s % 40.09/7.02 % (1249903)Peak memory usage: 89 MB % 40.09/7.02 % (1249903)Instructions burned: 147 (million) % 40.09/7.02 % (1249906)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=1023938965:avsq=on:i=276:avsqr=1,2:rtra=on_2958 on theBenchmark for (2958ds/276Mi) % 40.09/7.02 % (1249895)------------------------------ % 40.09/7.02 % (1249895)------------------------------ % 40.09/7.02 % (1249908)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=3689111751:i=1052:rtra=on_2958 on theBenchmark for (2958ds/1052Mi) % 40.09/7.02 % (1249910)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=1751599309:i=655:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2956 on theBenchmark for (2956ds/655Mi) % 40.09/7.02 % (1249900)------------------------------ % 40.09/7.02 % (1249900)------------------------------ % 40.09/7.02 % (1249912)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=2180430383:st=5:i=1054:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2956 on theBenchmark for (2956ds/1054Mi) % 40.09/7.02 % (1249912)Refutation not found, incomplete strategy % 40.09/7.02 % (1249912)------------------------------ % 40.09/7.02 % (1249912)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 40.09/7.02 % (1249912)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.09/7.02 % (1249912)CaDiCaL version: 2.1.3 % 40.09/7.02 % (1249912)Termination reason: Refutation not found, incomplete strategy % 40.09/7.02 % (1249912)Time elapsed: 0.004 s % 40.09/7.02 % (1249912)Peak memory usage: 87 MB % 40.09/7.02 % (1249912)Instructions burned: 8 (million) % 40.09/7.02 % (1249910)Refutation not found, incomplete strategy % 40.09/7.02 % (1249910)------------------------------ % 40.09/7.02 % (1249910)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 40.09/7.02 % (1249910)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.09/7.02 % (1249910)CaDiCaL version: 2.1.3 % 40.09/7.02 % (1249910)Termination reason: Refutation not found, incomplete strategy % 40.09/7.02 % (1249910)Time elapsed: 0.127 s % 40.09/7.02 % (1249910)Peak memory usage: 93 MB % 40.09/7.02 % (1249910)Instructions burned: 235 (million) % 40.09/7.02 % (1249906)Instruction limit reached! % 40.09/7.02 % (1249906)------------------------------ % 45.49/7.47 % (1249906)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 45.49/7.47 % (1249906)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.49/7.47 % (1249906)CaDiCaL version: 2.1.3 % 45.49/7.47 % (1249906)Termination reason: Instruction limit % 45.49/7.47 % (1249906)Termination phase: Saturation % 45.49/7.47 % (1249906)Time elapsed: 0.296 s % 45.49/7.47 % (1249906)Peak memory usage: 134 MB % 45.49/7.47 % (1249906)Instructions burned: 276 (million) % 45.49/7.47 % (1249915)lrs-1002_1_to=kbo:sas=z3:si=on:norm_ineq=on:sos=on:tha=some:random_seed=2212349743:i=107:rtra=on_2955 on theBenchmark for (2955ds/107Mi) % 45.49/7.47 % (1249915)Refutation not found, incomplete strategy % 45.49/7.47 % (1249915)------------------------------ % 45.49/7.47 % (1249915)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 45.49/7.47 % (1249915)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.49/7.47 % (1249915)CaDiCaL version: 2.1.3 % 45.49/7.47 % (1249915)Termination reason: Refutation not found, incomplete strategy % 45.49/7.47 % (1249915)Time elapsed: 0.066 s % 45.49/7.47 % (1249915)Peak memory usage: 113 MB % 45.49/7.47 % (1249915)Instructions burned: 41 (million) % 45.49/7.47 % (1249917)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=3690537072:s2a=on:i=450:doe=on:nm=32:rtra=on_2954 on theBenchmark for (2954ds/450Mi) % 45.49/7.47 % (1249910)------------------------------ % 45.49/7.47 % (1249910)------------------------------ % 45.49/7.47 % (1249912)------------------------------ % 45.49/7.47 % (1249912)------------------------------ % 45.49/7.47 % (1249919)WARNING Broken Constraint: if demodulation_redundancy_check(ordering) has been set then forward_demodulation(off) is not equal to off or backward_demodulation(off) is not equal to off or partial_redundancy_check(off) is not equal to off % 45.49/7.47 % (1249919)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=2774269769:i=1090:aac=none:nm=0:rtra=on:rawr=on_2953 on theBenchmark for (2953ds/1090Mi) % 45.49/7.47 % (1249922)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=3049234913:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2951 on theBenchmark for (2951ds/130Mi) % 45.49/7.47 % (1249922)Instruction limit reached! % 45.49/7.47 % (1249922)------------------------------ % 45.49/7.47 % (1249922)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 45.49/7.47 % (1249922)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.49/7.47 % (1249922)CaDiCaL version: 2.1.3 % 45.49/7.47 % (1249922)Termination reason: Instruction limit % 45.49/7.47 % (1249922)Termination phase: Saturation % 45.49/7.47 % (1249922)Time elapsed: 0.080 s % 45.49/7.47 % (1249922)Peak memory usage: 116 MB % 45.49/7.47 % (1249922)Instructions burned: 130 (million) % 45.49/7.47 % (1249915)------------------------------ % 45.49/7.47 % (1249915)------------------------------ % 45.49/7.47 % (1249924)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=1852850243:i=312:kws=inv_frequency:nm=20:rtra=on_2950 on theBenchmark for (2950ds/312Mi) % 45.49/7.47 % (1249917)Instruction limit reached! % 45.49/7.47 % (1249917)------------------------------ % 45.49/7.47 % (1249917)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 45.49/7.47 % (1249917)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.49/7.47 % (1249917)CaDiCaL version: 2.1.3 % 45.49/7.47 % (1249917)Termination reason: Instruction limit % 45.49/7.47 % (1249917)Termination phase: Saturation % 45.49/7.47 % (1249917)Time elapsed: 0.403 s % 45.49/7.47 % (1249917)Peak memory usage: 134 MB % 45.49/7.47 % (1249917)Instructions burned: 451 (million) % 45.49/7.47 % (1249908)Instruction limit reached! % 45.49/7.47 % (1249908)------------------------------ % 45.49/7.47 % (1249908)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 45.49/7.47 % (1249908)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.49/7.47 % (1249908)CaDiCaL version: 2.1.3 % 45.49/7.47 % (1249908)Termination reason: Instruction limit % 45.49/7.47 % (1249908)Termination phase: Saturation % 45.49/7.47 % (1249908)Time elapsed: 0.784 s % 45.49/7.47 % (1249908)Peak memory usage: 91 MB % 45.49/7.47 % (1249908)Instructions burned: 1052 (million) % 45.49/7.47 % (1249926)ott+10_1_to=kbo:sil=64000:si=on:sp=reverse_frequency:sos=on:random_seed=1700044383:i=491:doe=on:rtra=on:gtg=position_2948 on theBenchmark for (2948ds/491Mi) % 45.49/7.47 % (1249926)Refutation not found, incomplete strategy % 52.26/8.38 % (1249926)------------------------------ % 52.26/8.38 % (1249926)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 52.26/8.38 % (1249926)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 52.26/8.38 % (1249926)CaDiCaL version: 2.1.3 % 52.26/8.38 % (1249926)Termination reason: Refutation not found, incomplete strategy % 52.26/8.38 % (1249926)Time elapsed: 0.019 s % 52.26/8.38 % (1249926)Peak memory usage: 89 MB % 52.26/8.38 % (1249926)Instructions burned: 43 (million) % 52.26/8.38 % (1249927)ott+1011_4:1_to=lpo:sil=64000:si=on:spb=intro:random_seed=2202243411:s2a=on:i=835:s2at=2:rtra=on_2948 on theBenchmark for (2948ds/835Mi) % 52.26/8.38 % (1249929)ott+1011_2_to=lpo:sil=128000:si=on:sos=on:random_seed=137443608:i=307:bd=preordered:av=off:rtra=on:ev=cautious_2947 on theBenchmark for (2947ds/307Mi) % 52.26/8.38 % (1249930)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=2214258795:i=776:doe=on:rtra=on_2947 on theBenchmark for (2947ds/776Mi) % 52.26/8.38 % (1249924)Instruction limit reached! % 52.26/8.38 % (1249924)------------------------------ % 52.26/8.38 % (1249924)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 52.26/8.38 % (1249924)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 52.26/8.38 % (1249924)CaDiCaL version: 2.1.3 % 52.26/8.38 % (1249924)Termination reason: Instruction limit % 52.26/8.38 % (1249924)Termination phase: Saturation % 52.26/8.38 % (1249924)Time elapsed: 0.267 s % 52.26/8.38 % (1249924)Peak memory usage: 117 MB % 52.26/8.38 % (1249924)Instructions burned: 312 (million) % 52.26/8.38 % (1249929)Refutation not found, incomplete strategy % 52.26/8.38 % (1249929)------------------------------ % 52.26/8.38 % (1249929)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 52.26/8.38 % (1249929)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 52.26/8.38 % (1249929)CaDiCaL version: 2.1.3 % 52.26/8.38 % (1249929)Termination reason: Refutation not found, incomplete strategy % 52.26/8.38 % (1249929)Time elapsed: 0.038 s % 52.26/8.38 % (1249929)Peak memory usage: 89 MB % 52.26/8.38 % (1249929)Instructions burned: 46 (million) % 52.26/8.38 % (1249926)------------------------------ % 52.26/8.39 % (1249926)------------------------------ % 52.26/8.39 % (1249935)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=2955170382:s2a=on:i=646:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2945 on theBenchmark for (2945ds/646Mi) % 52.26/8.39 % (1249936)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=249954410:thitd=on:cond=fast:i=784:nm=30:rtra=on:gtg=all:tac=axiom_2944 on theBenchmark for (2944ds/784Mi) % 52.26/8.39 % (1249919)Instruction limit reached! % 52.26/8.39 % (1249919)------------------------------ % 52.26/8.39 % (1249919)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 52.26/8.39 % (1249919)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 52.26/8.39 % (1249919)CaDiCaL version: 2.1.3 % 52.26/8.39 % (1249919)Termination reason: Instruction limit % 52.26/8.39 % (1249919)Termination phase: Saturation % 52.26/8.39 % (1249919)Time elapsed: 0.873 s % 52.26/8.39 % (1249919)Peak memory usage: 117 MB % 52.26/8.39 % (1249919)Instructions burned: 1090 (million) % 52.26/8.39 % (1249929)------------------------------ % 52.26/8.39 % (1249929)------------------------------ % 52.26/8.39 % (1249927)Instruction limit reached! % 52.26/8.39 % (1249927)------------------------------ % 52.26/8.39 % (1249927)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 52.26/8.39 % (1249927)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 52.26/8.39 % (1249927)CaDiCaL version: 2.1.3 % 52.26/8.39 % (1249927)Termination reason: Instruction limit % 52.26/8.39 % (1249927)Termination phase: Saturation % 52.26/8.39 % (1249927)Time elapsed: 0.584 s % 52.26/8.39 % (1249927)Peak memory usage: 88 MB % 52.26/8.39 % (1249927)Instructions burned: 836 (million) % 52.26/8.39 % (1249930)Instruction limit reached! % 52.26/8.39 % (1249930)------------------------------ % 52.26/8.39 % (1249930)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 52.26/8.39 % (1249930)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 52.26/8.39 % (1249930)CaDiCaL version: 2.1.3 % 52.26/8.39 % (1249930)Termination reason: Instruction limit % 52.26/8.39 % (1249930)Termination phase: Saturation % 52.26/8.39 % (1249930)Time elapsed: 0.586 s % 59.47/9.40 % (1249930)Peak memory usage: 113 MB % 59.47/9.40 % (1249930)Instructions burned: 777 (million) % 59.47/9.40 % (1249939)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=3468238006:thitd=on:s2a=on:i=1131:add=on:canc=force:bd=all:rtra=on:tac=axiom:ev=off_2941 on theBenchmark for (2941ds/1131Mi) % 59.47/9.40 % (1249936)Instruction limit reached! % 59.47/9.40 % (1249936)------------------------------ % 59.47/9.40 % (1249936)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 59.47/9.40 % (1249936)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 59.47/9.40 % (1249936)CaDiCaL version: 2.1.3 % 59.47/9.40 % (1249936)Termination reason: Instruction limit % 59.47/9.40 % (1249936)Termination phase: Saturation % 59.47/9.40 % (1249936)Time elapsed: 0.309 s % 59.47/9.40 % (1249936)Peak memory usage: 113 MB % 59.47/9.40 % (1249936)Instructions burned: 785 (million) % 59.47/9.40 % (1249940)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=1619329073:s2pl=no:i=246:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2940 on theBenchmark for (2940ds/246Mi) % 59.47/9.40 % (1249940)Refutation not found, incomplete strategy % 59.47/9.40 % (1249940)------------------------------ % 59.47/9.40 % (1249940)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 59.47/9.40 % (1249940)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 59.47/9.40 % (1249940)CaDiCaL version: 2.1.3 % 59.47/9.40 % (1249940)Termination reason: Refutation not found, incomplete strategy % 59.47/9.40 % (1249940)Time elapsed: 0.046 s % 59.47/9.40 % (1249940)Peak memory usage: 111 MB % 59.47/9.40 % (1249940)Instructions burned: 17 (million) % 59.47/9.40 % (1249941)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=1665986068:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2939 on theBenchmark for (2939ds/775Mi) % 59.47/9.40 % (1249941)Refutation not found, incomplete strategy % 59.47/9.40 % (1249941)------------------------------ % 59.47/9.40 % (1249941)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 59.47/9.40 % (1249941)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 59.47/9.40 % (1249941)CaDiCaL version: 2.1.3 % 59.47/9.40 % (1249941)Termination reason: Refutation not found, incomplete strategy % 59.47/9.40 % (1249941)Time elapsed: 0.011 s % 59.47/9.40 % (1249941)Peak memory usage: 88 MB % 59.47/9.40 % (1249941)Instructions burned: 12 (million) % 59.47/9.40 % (1249944)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=3017181708:i=102:nm=16:rtra=on_2938 on theBenchmark for (2938ds/102Mi) % 59.47/9.40 % (1249935)Instruction limit reached! % 59.47/9.40 % (1249935)------------------------------ % 59.47/9.40 % (1249935)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 59.47/9.40 % (1249935)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 59.47/9.40 % (1249935)CaDiCaL version: 2.1.3 % 59.47/9.40 % (1249935)Termination reason: Instruction limit % 59.47/9.40 % (1249935)Termination phase: Saturation % 59.47/9.40 % (1249935)Time elapsed: 0.574 s % 59.47/9.40 % (1249935)Peak memory usage: 135 MB % 59.47/9.40 % (1249935)Instructions burned: 646 (million) % 59.47/9.40 % (1249942)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=1704671098:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2939 on theBenchmark for (2939ds/273Mi) % 59.47/9.40 % (1249944)Instruction limit reached! % 59.47/9.40 % (1249944)------------------------------ % 59.47/9.40 % (1249944)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 59.47/9.40 % (1249944)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 59.47/9.40 % (1249944)CaDiCaL version: 2.1.3 % 59.47/9.40 % (1249944)Termination reason: Instruction limit % 59.47/9.40 % (1249944)Termination phase: Saturation % 59.47/9.40 % (1249944)Time elapsed: 0.042 s % 59.47/9.40 % (1249944)Peak memory usage: 89 MB % 59.47/9.40 % (1249944)Instructions burned: 104 (million) % 59.47/9.40 % (1249942)Instruction limit reached! % 59.47/9.40 % (1249942)------------------------------ % 59.47/9.40 % (1249942)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 59.47/9.40 % (1249942)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 59.47/9.40 % (1249942)CaDiCaL version: 2.1.3 % 59.47/9.40 % (1249942)Termination reason: Instruction limit % 59.47/9.40 % (1249942)Termination phase: Saturation % 71.79/11.06 % (1249942)Time elapsed: 0.206 s % 71.79/11.06 % (1249942)Peak memory usage: 90 MB % 71.79/11.06 % (1249942)Instructions burned: 274 (million) % 71.79/11.06 % (1249950)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=3332700547:i=6400:doe=on:fsr=off:rtra=on_2936 on theBenchmark for (2936ds/6400Mi) % 71.79/11.06 % (1249949)lrs+10_1_to=lpo:sil=128000:si=on:bsr=unit_only:tha=off:random_seed=4192874797:avsq=on:s2a=on:i=1094:s2at=5:avsqr=4463,131072:rtra=on_2936 on theBenchmark for (2936ds/1094Mi) % 71.79/11.06 % (1249940)------------------------------ % 71.79/11.06 % (1249940)------------------------------ % 71.79/11.06 % (1249941)------------------------------ % 71.79/11.06 % (1249941)------------------------------ % 71.79/11.06 % (1249951)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=3412425987:i=868:doe=on:nm=0:rtra=on:gtg=exists_sym_2934 on theBenchmark for (2934ds/868Mi) % 71.79/11.06 % (1249954)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=3841109121:i=1846:canc=cautious:fsr=off:rtra=on_2934 on theBenchmark for (2934ds/1846Mi) % 71.79/11.06 % (1249954)Refutation not found, incomplete strategy % 71.79/11.06 % (1249954)------------------------------ % 71.79/11.06 % (1249954)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 71.79/11.06 % (1249954)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 71.79/11.06 % (1249954)CaDiCaL version: 2.1.3 % 71.79/11.06 % (1249954)Termination reason: Refutation not found, incomplete strategy % 71.79/11.06 % (1249954)Time elapsed: 0.022 s % 71.79/11.06 % (1249954)Peak memory usage: 89 MB % 71.79/11.06 % (1249954)Instructions burned: 27 (million) % 71.79/11.06 % (1249955)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=473248512:s2a=on:i=36816:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2933 on theBenchmark for (2933ds/36816Mi) % 71.79/11.06 % (1249939)Instruction limit reached! % 71.79/11.06 % (1249939)------------------------------ % 71.79/11.06 % (1249939)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 71.79/11.06 % (1249939)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 71.79/11.06 % (1249939)CaDiCaL version: 2.1.3 % 71.79/11.06 % (1249939)Termination reason: Instruction limit % 71.79/11.06 % (1249939)Termination phase: Saturation % 71.79/11.06 % (1249939)Time elapsed: 0.881 s % 71.79/11.06 % (1249939)Peak memory usage: 113 MB % 71.79/11.06 % (1249939)Instructions burned: 1131 (million) % 71.79/11.06 % (1249959)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=1747815937:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2930 on theBenchmark for (2930ds/273Mi) % 71.79/11.06 % (1249954)------------------------------ % 71.79/11.06 % (1249954)------------------------------ % 71.79/11.06 % (1249949)Instruction limit reached! % 71.79/11.06 % (1249949)------------------------------ % 71.79/11.06 % (1249949)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 71.79/11.06 % (1249949)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 71.79/11.06 % (1249949)CaDiCaL version: 2.1.3 % 71.79/11.06 % (1249949)Termination reason: Instruction limit % 71.79/11.06 % (1249949)Termination phase: Saturation % 71.79/11.06 % (1249949)Time elapsed: 0.777 s % 71.79/11.06 % (1249949)Peak memory usage: 90 MB % 71.79/11.06 % (1249949)Instructions burned: 1094 (million) % 71.79/11.06 % (1249905)Instruction limit reached! % 71.79/11.06 % (1249905)------------------------------ % 71.79/11.06 % (1249905)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 71.79/11.06 % (1249905)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 71.79/11.06 % (1249905)CaDiCaL version: 2.1.3 % 71.79/11.06 % (1249905)Termination reason: Instruction limit % 71.79/11.06 % (1249905)Termination phase: Saturation % 71.79/11.06 % (1249905)Time elapsed: 3.059 s % 71.79/11.06 % (1249905)Peak memory usage: 91 MB % 71.79/11.06 % (1249905)Instructions burned: 4429 (million) % 71.79/11.06 % (1249959)Instruction limit reached! % 71.79/11.06 % (1249959)------------------------------ % 71.79/11.06 % (1249959)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 71.79/11.06 % (1249959)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 71.79/11.06 % (1249959)CaDiCaL version: 2.1.3 % 71.79/11.06 % (1249959)Termination reason: Instruction limit % 71.79/11.06 % (1249959)Termination phase: Saturation % 80.44/12.38 % (1249959)Time elapsed: 0.205 s % 80.44/12.38 % (1249959)Peak memory usage: 90 MB % 80.44/12.38 % (1249959)Instructions burned: 275 (million) % 80.44/12.38 % (1249961)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=3900779685:i=863:doe=on:nm=0:rtra=on:gtg=exists_sym_2927 on theBenchmark for (2927ds/863Mi) % 80.44/12.38 % (1249951)Instruction limit reached! % 80.44/12.38 % (1249951)------------------------------ % 80.44/12.38 % (1249951)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 80.44/12.38 % (1249951)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 80.44/12.38 % (1249951)CaDiCaL version: 2.1.3 % 80.44/12.38 % (1249951)Termination reason: Instruction limit % 80.44/12.38 % (1249951)Termination phase: Saturation % 80.44/12.38 % (1249951)Time elapsed: 0.744 s % 80.44/12.38 % (1249951)Peak memory usage: 125 MB % 80.44/12.38 % (1249951)Instructions burned: 869 (million) % 80.44/12.38 % (1249962)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=975521684:i=5811:kws=precedence:nm=0:rtra=on_2926 on theBenchmark for (2926ds/5811Mi) % 80.44/12.38 % (1249963)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=71181273:i=2216:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2926 on theBenchmark for (2926ds/2216Mi) % 80.44/12.38 % (1249964)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=132494603:i=801:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2925 on theBenchmark for (2925ds/801Mi) % 80.44/12.38 % (1249966)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=736051781:st=5:i=1026:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2924 on theBenchmark for (2924ds/1026Mi) % 80.44/12.38 % (1249966)Refutation not found, incomplete strategy % 80.44/12.38 % (1249966)------------------------------ % 80.44/12.38 % (1249966)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 80.44/12.38 % (1249966)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 80.44/12.38 % (1249966)CaDiCaL version: 2.1.3 % 80.44/12.38 % (1249966)Termination reason: Refutation not found, incomplete strategy % 80.44/12.38 % (1249966)Time elapsed: 0.007 s % 80.44/12.38 % (1249966)Peak memory usage: 87 MB % 80.44/12.38 % (1249966)Instructions burned: 8 (million) % 80.44/12.38 % (1249964)Refutation not found, incomplete strategy % 80.44/12.38 % (1249964)------------------------------ % 80.44/12.38 % (1249964)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 80.44/12.38 % (1249964)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 80.44/12.38 % (1249964)CaDiCaL version: 2.1.3 % 80.44/12.38 % (1249964)Termination reason: Refutation not found, incomplete strategy % 80.44/12.38 % (1249964)Time elapsed: 0.203 s % 80.44/12.38 % (1249964)Peak memory usage: 93 MB % 80.44/12.38 % (1249964)Instructions burned: 212 (million) % 80.44/12.38 % (1249966)------------------------------ % 80.44/12.38 % (1249966)------------------------------ % 80.44/12.38 % (1249961)Instruction limit reached! % 80.44/12.38 % (1249961)------------------------------ % 80.44/12.38 % (1249961)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 80.44/12.38 % (1249961)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 80.44/12.38 % (1249961)CaDiCaL version: 2.1.3 % 80.44/12.38 % (1249961)Termination reason: Instruction limit % 80.44/12.38 % (1249961)Termination phase: Saturation % 80.44/12.38 % (1249961)Time elapsed: 0.719 s % 80.44/12.38 % (1249961)Peak memory usage: 123 MB % 80.44/12.38 % (1249961)Instructions burned: 863 (million) % 80.44/12.38 % (1249964)------------------------------ % 80.44/12.38 % (1249964)------------------------------ % 80.44/12.38 % (1249971)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=3488964863:i=3509:rtra=on_2918 on theBenchmark for (2918ds/3509Mi) % 80.44/12.38 % (1249972)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=3927713968:st=2:i=2127:sd=12:ep=R:rtra=on:ss=axioms_2917 on theBenchmark for (2917ds/2127Mi) % 80.44/12.38 % (1249972)Refutation not found, incomplete strategy % 80.44/12.38 % (1249972)------------------------------ % 80.44/12.38 % (1249972)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 80.44/12.38 % (1249972)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 80.44/12.38 % (1249972)CaDiCaL version: 2.1.3 % 80.44/12.38 % (1249972)Termination reason: Refutation not found, incomplete strategy % 80.44/12.38 % (1249972)Time elapsed: 0.010 s % 95.39/14.41 % (1249972)Peak memory usage: 88 MB % 95.39/14.41 % (1249972)Instructions burned: 12 (million) % 95.39/14.41 % (1249973)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=1603254766:i=1959:rtra=on:fsd=on:proc=on_2917 on theBenchmark for (2917ds/1959Mi) % 95.39/14.41 % (1249972)------------------------------ % 95.39/14.41 % (1249972)------------------------------ % 95.39/14.41 % (1249950)Instruction limit reached! % 95.39/14.41 % (1249950)------------------------------ % 95.39/14.41 % (1249950)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 95.39/14.41 % (1249950)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 95.39/14.41 % (1249950)CaDiCaL version: 2.1.3 % 95.39/14.41 % (1249950)Termination reason: Instruction limit % 95.39/14.41 % (1249950)Termination phase: Saturation % 95.39/14.41 % (1249950)Time elapsed: 2.373 s % 95.39/14.41 % (1249950)Peak memory usage: 92 MB % 95.39/14.41 % (1249950)Instructions burned: 6401 (million) % 95.39/14.41 % (1249978)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=3132812105:s2a=on:i=3553:nm=0:rtra=on_2911 on theBenchmark for (2911ds/3553Mi) % 95.39/14.41 % (1249980)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=2508031293:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2910 on theBenchmark for (2910ds/3201Mi) % 95.39/14.41 % (1249980)Refutation not found, incomplete strategy % 95.39/14.41 % (1249980)------------------------------ % 95.39/14.41 % (1249980)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 95.39/14.41 % (1249980)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 95.39/14.41 % (1249980)CaDiCaL version: 2.1.3 % 95.39/14.41 % (1249980)Termination reason: Refutation not found, incomplete strategy % 95.39/14.41 % (1249980)Time elapsed: 0.126 s % 95.39/14.41 % (1249980)Peak memory usage: 92 MB % 95.39/14.41 % (1249980)Instructions burned: 309 (million) % 95.39/14.41 % (1249963)Instruction limit reached! % 95.39/14.41 % (1249963)------------------------------ % 95.39/14.41 % (1249963)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 95.39/14.41 % (1249963)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 95.39/14.41 % (1249963)CaDiCaL version: 2.1.3 % 95.39/14.41 % (1249963)Termination reason: Instruction limit % 95.39/14.41 % (1249963)Termination phase: Saturation % 95.39/14.41 % (1249963)Time elapsed: 1.737 s % 95.39/14.41 % (1249963)Peak memory usage: 118 MB % 95.39/14.41 % (1249963)Instructions burned: 2216 (million) % 95.39/14.41 % (1249980)------------------------------ % 95.39/14.41 % (1249980)------------------------------ % 95.39/14.41 % (1249983)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=808599427:thitd=on:cond=on:i=4093:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2906 on theBenchmark for (2906ds/4093Mi) % 95.39/14.41 % (1249984)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=92100448:cond=fast:i=21173:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2905 on theBenchmark for (2905ds/21173Mi) % 95.39/14.41 % (1249984)Refutation not found, incomplete strategy % 95.39/14.41 % (1249984)------------------------------ % 95.39/14.41 % (1249984)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 95.39/14.42 % (1249984)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 95.39/14.42 % (1249984)CaDiCaL version: 2.1.3 % 95.39/14.42 % (1249984)Termination reason: Refutation not found, incomplete strategy % 95.39/14.42 % (1249984)Time elapsed: 0.025 s % 95.39/14.42 % (1249984)Peak memory usage: 112 MB % 95.39/14.42 % (1249984)Instructions burned: 10 (million) % 95.39/14.42 % (1249984)------------------------------ % 95.39/14.42 % (1249984)------------------------------ % 95.39/14.42 % (1249973)Instruction limit reached! % 95.39/14.42 % (1249973)------------------------------ % 95.39/14.42 % (1249973)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 95.39/14.42 % (1249973)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 95.39/14.42 % (1249973)CaDiCaL version: 2.1.3 % 95.39/14.42 % (1249973)Termination reason: Instruction limit % 95.39/14.42 % (1249973)Termination phase: Saturation % 95.39/14.42 % (1249973)Time elapsed: 1.530 s % 95.39/14.42 % (1249973)Peak memory usage: 118 MB % 95.39/14.42 % (1249973)Instructions burned: 1960 (million) % 95.39/14.42 % (1249987)lrs+11_1_to=lpo:thi=all:sas=z3:si=on:fd=off:sac=on:slsq=on:random_seed=33624088:avsq=on:i=10544:avsqr=17,4:canc=force:rtra=on:gtg=exists_top:er=filter_2900 on theBenchmark for (2900ds/10544Mi) % 110.37/16.59 % (1249988)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=2113899609:avsq=on:i=1262:avsqr=1,16:rtra=on:rawr=on_2899 on theBenchmark for (2899ds/1262Mi) % 110.37/16.59 % (1249971)Instruction limit reached! % 110.37/16.59 % (1249971)------------------------------ % 110.37/16.59 % (1249971)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 110.37/16.59 % (1249971)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 110.37/16.59 % (1249971)CaDiCaL version: 2.1.3 % 110.37/16.59 % (1249971)Termination reason: Instruction limit % 110.37/16.59 % (1249971)Termination phase: Saturation % 110.37/16.59 % (1249971)Time elapsed: 2.316 s % 110.37/16.59 % (1249971)Peak memory usage: 90 MB % 110.37/16.59 % (1249971)Instructions burned: 3509 (million) % 110.37/16.59 % (1249991)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=4152061498:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2892 on theBenchmark for (2892ds/775Mi) % 110.37/16.59 % (1249991)Refutation not found, incomplete strategy % 110.37/16.59 % (1249991)------------------------------ % 110.37/16.59 % (1249991)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 110.37/16.59 % (1249991)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 110.37/16.59 % (1249991)CaDiCaL version: 2.1.3 % 110.37/16.59 % (1249991)Termination reason: Refutation not found, incomplete strategy % 110.37/16.59 % (1249991)Time elapsed: 0.006 s % 110.37/16.59 % (1249991)Peak memory usage: 88 MB % 110.37/16.59 % (1249991)Instructions burned: 12 (million) % 110.37/16.59 % (1249988)Instruction limit reached! % 110.37/16.59 % (1249988)------------------------------ % 110.37/16.59 % (1249988)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 110.37/16.59 % (1249988)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 110.37/16.59 % (1249988)CaDiCaL version: 2.1.3 % 110.37/16.59 % (1249988)Termination reason: Instruction limit % 110.37/16.59 % (1249988)Termination phase: Saturation % 110.37/16.59 % (1249988)Time elapsed: 0.705 s % 110.37/16.59 % (1249988)Peak memory usage: 117 MB % 110.37/16.59 % (1249988)Instructions burned: 1263 (million) % 110.37/16.59 % (1249991)------------------------------ % 110.37/16.59 % (1249991)------------------------------ % 110.37/16.59 % (1249993)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=3173558831:i=270:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2889 on theBenchmark for (2889ds/270Mi) % 110.37/16.59 % (1249993)Instruction limit reached! % 110.37/16.59 % (1249993)------------------------------ % 110.37/16.59 % (1249993)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 110.37/16.59 % (1249993)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 110.37/16.59 % (1249993)CaDiCaL version: 2.1.3 % 110.37/16.59 % (1249993)Termination reason: Instruction limit % 110.37/16.59 % (1249993)Termination phase: Saturation % 110.37/16.59 % (1249993)Time elapsed: 0.109 s % 110.37/16.59 % (1249993)Peak memory usage: 90 MB % 110.37/16.59 % (1249993)Instructions burned: 272 (million) % 110.37/16.59 % (1249978)Instruction limit reached! % 110.37/16.59 % (1249978)------------------------------ % 110.37/16.59 % (1249978)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 110.37/16.59 % (1249978)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 110.37/16.59 % (1249978)CaDiCaL version: 2.1.3 % 110.37/16.59 % (1249978)Termination reason: Instruction limit % 110.37/16.59 % (1249978)Termination phase: Saturation % 110.37/16.59 % (1249978)Time elapsed: 2.187 s % 110.37/16.59 % (1249978)Peak memory usage: 91 MB % 110.37/16.59 % (1249978)Instructions burned: 3553 (million) % 110.37/16.59 % (1249994)ott+10_128_isp=bottom:to=lpo:sil=128000:si=on:urr=on:uwa=alasca_main:sac=on:slsq=on:random_seed=3938537257:i=17165:aac=none:doe=on:rtra=on:gtg=exists_all_2888 on theBenchmark for (2888ds/17165Mi) % 110.37/16.59 % (1249996)lrs+2_10_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_main:tha=some:random_seed=512613187:s2a=on:i=13094:s2at=-1:rtra=on_2887 on theBenchmark for (2887ds/13094Mi) % 110.37/16.59 % (1249997)lrs+10_1_to=lpo:sil=128000:si=on:sp=occurrence:random_seed=799940508:st=2:i=12633:rtra=on:ss=axioms_2887 on theBenchmark for (2887ds/12633Mi) % 110.37/16.59 % (1249997)Refutation not found, incomplete strategy % 110.37/16.59 % (1249997)------------------------------ % 110.37/16.59 % (1249997)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 126.62/18.99 % (1249997)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.62/18.99 % (1249997)CaDiCaL version: 2.1.3 % 126.62/18.99 % (1249997)Termination reason: Refutation not found, incomplete strategy % 126.62/18.99 % (1249997)Time elapsed: 0.005 s % 126.62/18.99 % (1249997)Peak memory usage: 87 MB % 126.62/18.99 % (1249997)Instructions burned: 9 (million) % 126.62/18.99 % (1249962)Instruction limit reached! % 126.62/18.99 % (1249962)------------------------------ % 126.62/18.99 % (1249962)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 126.62/18.99 % (1249962)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.62/18.99 % (1249962)CaDiCaL version: 2.1.3 % 126.62/18.99 % (1249962)Termination reason: Instruction limit % 126.62/18.99 % (1249962)Termination phase: Saturation % 126.62/18.99 % (1249962)Time elapsed: 3.991 s % 126.62/18.99 % (1249962)Peak memory usage: 118 MB % 126.62/18.99 % (1249962)Instructions burned: 5813 (million) % 126.62/18.99 % (1249997)------------------------------ % 126.62/18.99 % (1249997)------------------------------ % 126.62/18.99 % (1249983)Instruction limit reached! % 126.62/18.99 % (1249983)------------------------------ % 126.62/18.99 % (1249983)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 126.62/18.99 % (1249983)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.62/18.99 % (1249983)CaDiCaL version: 2.1.3 % 126.62/18.99 % (1249983)Termination reason: Instruction limit % 126.62/18.99 % (1249983)Termination phase: Saturation % 126.62/18.99 % (1249983)Time elapsed: 2.102 s % 126.62/18.99 % (1249983)Peak memory usage: 138 MB % 126.62/18.99 % (1249983)Instructions burned: 4095 (million) % 126.62/18.99 % (1250028)dis+1011_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_frequency:lsd=20:nwc=3:random_seed=332555444:i=1783:rtra=on:gtg=position_2884 on theBenchmark for (2884ds/1783Mi) % 126.62/18.99 % (1250070)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=4190691993:i=5451:aac=none:doe=on:nm=0:rtra=on:amm=off:gtg=position_2883 on theBenchmark for (2883ds/5451Mi) % 126.62/18.99 % (1250084)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=2469183370:i=4975:doe=on:nm=0:rtra=on:gtg=exists_sym_2882 on theBenchmark for (2882ds/4975Mi) % 126.62/18.99 % (1250028)Instruction limit reached! % 126.62/18.99 % (1250028)------------------------------ % 126.62/18.99 % (1250028)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 126.62/18.99 % (1250028)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.62/18.99 % (1250028)CaDiCaL version: 2.1.3 % 126.62/18.99 % (1250028)Termination reason: Instruction limit % 126.62/18.99 % (1250028)Termination phase: Saturation % 126.62/18.99 % (1250028)Time elapsed: 0.723 s % 126.62/18.99 % (1250028)Peak memory usage: 119 MB % 126.62/18.99 % (1250028)Instructions burned: 1784 (million) % 126.62/18.99 % (1250160)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=426885224:i=2076:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2875 on theBenchmark for (2875ds/2076Mi) % 126.62/18.99 % (1249987)Instruction limit reached! % 126.62/18.99 % (1249987)------------------------------ % 126.62/18.99 % (1249987)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 126.62/18.99 % (1249987)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.62/18.99 % (1249987)CaDiCaL version: 2.1.3 % 126.62/18.99 % (1249987)Termination reason: Instruction limit % 126.62/18.99 % (1249987)Termination phase: Saturation % 126.62/18.99 % (1249987)Time elapsed: 3.043 s % 126.62/18.99 % (1249987)Peak memory usage: 188 MB % 126.62/18.99 % (1249987)Instructions burned: 10546 (million) % 126.62/18.99 % (1250219)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=2433571396:i=5145:rtra=on_2868 on theBenchmark for (2868ds/5145Mi) % 126.62/18.99 % (1250160)Instruction limit reached! % 126.62/18.99 % (1250160)------------------------------ % 126.62/18.99 % (1250160)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 126.62/18.99 % (1250160)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.62/18.99 % (1250160)CaDiCaL version: 2.1.3 % 126.62/18.99 % (1250160)Termination reason: Instruction limit % 126.62/18.99 % (1250160)Termination phase: Saturation % 126.62/18.99 % (1250160)Time elapsed: 0.846 s % 126.62/18.99 % (1250160)Peak memory usage: 118 MB % 126.62/18.99 % (1250160)Instructions burned: 2078 (million) % 205.11/29.87 % (1250296)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=2667064582:i=3509:rtra=on_2865 on theBenchmark for (2865ds/3509Mi) % 205.11/29.87 % (1250084)Instruction limit reached! % 205.11/29.87 % (1250084)------------------------------ % 205.11/29.87 % (1250084)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 205.11/29.87 % (1250084)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 205.11/29.87 % (1250084)CaDiCaL version: 2.1.3 % 205.11/29.87 % (1250084)Termination reason: Instruction limit % 205.11/29.87 % (1250084)Termination phase: Saturation % 205.11/29.87 % (1250084)Time elapsed: 2.126 s % 205.11/29.87 % (1250084)Peak memory usage: 127 MB % 205.11/29.87 % (1250084)Instructions burned: 4975 (million) % 205.11/29.87 % (1250380)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=1311104096:st=2:i=13800:sd=12:ep=R:rtra=on:ss=axioms_2859 on theBenchmark for (2859ds/13800Mi) % 205.11/29.87 % (1250380)Refutation not found, incomplete strategy % 205.11/29.87 % (1250380)------------------------------ % 205.11/29.87 % (1250380)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 205.11/29.87 % (1250380)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 205.11/29.87 % (1250380)CaDiCaL version: 2.1.3 % 205.11/29.87 % (1250380)Termination reason: Refutation not found, incomplete strategy % 205.11/29.87 % (1250380)Time elapsed: 0.006 s % 205.11/29.87 % (1250380)Peak memory usage: 88 MB % 205.11/29.87 % (1250380)Instructions burned: 12 (million) % 205.11/29.87 % (1250070)Instruction limit reached! % 205.11/29.87 % (1250070)------------------------------ % 205.11/29.87 % (1250070)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 205.11/29.87 % (1250070)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 205.11/29.87 % (1250070)CaDiCaL version: 2.1.3 % 205.11/29.87 % (1250070)Termination reason: Instruction limit % 205.11/29.87 % (1250070)Termination phase: Saturation % 205.11/29.87 % (1250070)Time elapsed: 2.412 s % 205.11/29.87 % (1250070)Peak memory usage: 123 MB % 205.11/29.87 % (1250070)Instructions burned: 5453 (million) % 205.11/29.87 % (1250219)Instruction limit reached! % 205.11/29.87 % (1250219)------------------------------ % 205.11/29.87 % (1250219)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 205.11/29.87 % (1250219)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 205.11/29.87 % (1250219)CaDiCaL version: 2.1.3 % 205.11/29.87 % (1250219)Termination reason: Instruction limit % 205.11/29.87 % (1250219)Termination phase: Saturation % 205.11/29.87 % (1250219)Time elapsed: 1.045 s % 205.11/29.87 % (1250219)Peak memory usage: 95 MB % 205.11/29.87 % (1250219)Instructions burned: 5150 (million) % 205.11/29.87 % (1250380)------------------------------ % 205.11/29.87 % (1250380)------------------------------ % 205.11/29.87 % (1250431)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 % 205.11/29.87 % (1250431)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=1241655007:i=11747:aac=none:nm=0:rtra=on:rawr=on_2856 on theBenchmark for (2856ds/11747Mi) % 205.11/29.87 % (1250430)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=3658959608:i=1412:rtra=on:fsd=on:proc=on_2857 on theBenchmark for (2857ds/1412Mi) % 205.11/29.87 % (1250446)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=4145685729:s2a=on:i=3553:nm=0:rtra=on_2855 on theBenchmark for (2855ds/3553Mi) % 205.11/29.87 % (1250296)Instruction limit reached! % 205.11/29.87 % (1250296)------------------------------ % 205.11/29.87 % (1250296)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 205.11/29.87 % (1250296)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 205.11/29.87 % (1250296)CaDiCaL version: 2.1.3 % 205.11/29.87 % (1250296)Termination reason: Instruction limit % 205.11/29.87 % (1250296)Termination phase: Saturation % 205.11/29.87 % (1250296)Time elapsed: 1.712 s % 205.11/29.87 % (1250296)Peak memory usage: 90 MB % 205.11/29.87 % (1250296)Instructions burned: 3511 (million) % 205.11/29.87 % (1250482)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=1093521619:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2846 on theBenchmark for (2846ds/3201Mi) % 205.11/29.87 % (1250430)Instruction limit reached! % 205.11/29.87 % (1250430)------------------------------ % 205.11/29.87 % (1250430)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 235.30/34.10 % (1250430)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.30/34.10 % (1250430)CaDiCaL version: 2.1.3 % 235.30/34.10 % (1250430)Termination reason: Instruction limit % 235.30/34.10 % (1250430)Termination phase: Saturation % 235.30/34.10 % (1250430)Time elapsed: 1.147 s % 235.30/34.10 % (1250430)Peak memory usage: 118 MB % 235.30/34.10 % (1250430)Instructions burned: 1413 (million) % 235.30/34.10 % (1250482)Refutation not found, incomplete strategy % 235.30/34.10 % (1250482)------------------------------ % 235.30/34.10 % (1250482)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 235.30/34.10 % (1250482)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.30/34.10 % (1250482)CaDiCaL version: 2.1.3 % 235.30/34.10 % (1250482)Termination reason: Refutation not found, incomplete strategy % 235.30/34.10 % (1250482)Time elapsed: 0.237 s % 235.30/34.10 % (1250482)Peak memory usage: 92 MB % 235.30/34.10 % (1250482)Instructions burned: 309 (million) % 235.30/34.10 % (1250494)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=994360341:thitd=on:cond=on:i=4081:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2843 on theBenchmark for (2843ds/4081Mi) % 235.30/34.10 % (1250482)------------------------------ % 235.30/34.10 % (1250482)------------------------------ % 235.30/34.10 % (1250496)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=2179120722:cond=fast:i=20260:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2837 on theBenchmark for (2837ds/20260Mi) % 235.30/34.10 % (1250496)Refutation not found, incomplete strategy % 235.30/34.10 % (1250496)------------------------------ % 235.30/34.10 % (1250496)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 235.30/34.10 % (1250496)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.30/34.10 % (1250496)CaDiCaL version: 2.1.3 % 235.30/34.10 % (1250496)Termination reason: Refutation not found, incomplete strategy % 235.30/34.10 % (1250496)Time elapsed: 0.042 s % 235.30/34.10 % (1250496)Peak memory usage: 112 MB % 235.30/34.10 % (1250496)Instructions burned: 10 (million) % 235.30/34.10 % (1250496)------------------------------ % 235.30/34.10 % (1250496)------------------------------ % 235.30/34.10 % (1250502)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=3620804537:s2a=on:i=58627:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2830 on theBenchmark for (2830ds/58627Mi) % 235.30/34.10 % (1250446)Instruction limit reached! % 235.30/34.10 % (1250446)------------------------------ % 235.30/34.10 % (1250446)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 235.30/34.10 % (1250446)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.30/34.10 % (1250446)CaDiCaL version: 2.1.3 % 235.30/34.10 % (1250446)Termination reason: Instruction limit % 235.30/34.10 % (1250446)Termination phase: Saturation % 235.30/34.10 % (1250446)Time elapsed: 2.551 s % 235.30/34.10 % (1250446)Peak memory usage: 91 MB % 235.30/34.10 % (1250446)Instructions burned: 3554 (million) % 235.30/34.10 % (1250504)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=1760123355:avsq=on:i=6258:avsqr=1,16:rtra=on:rawr=on_2827 on theBenchmark for (2827ds/6258Mi) % 235.30/34.10 % (1249996)Instruction limit reached! % 235.30/34.10 % (1249996)------------------------------ % 235.30/34.10 % (1249996)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 235.30/34.10 % (1249996)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.30/34.10 % (1249996)CaDiCaL version: 2.1.3 % 235.30/34.10 % (1249996)Termination reason: Instruction limit % 235.30/34.10 % (1249996)Termination phase: Saturation % 235.30/34.10 % (1249996)Time elapsed: 6.158 s % 235.30/34.10 % (1249996)Peak memory usage: 101 MB % 235.30/34.10 % (1249996)Instructions burned: 13094 (million) % 235.30/34.10 % (1250506)ott+10_128_isp=bottom:to=lpo:sil=128000:si=on:urr=on:uwa=alasca_main:sac=on:slsq=on:random_seed=2253205162:i=34001:aac=none:doe=on:rtra=on:gtg=exists_all_2824 on theBenchmark for (2824ds/34001Mi) % 235.30/34.10 % (1250502)Refutation not found, incomplete strategy % 235.30/34.10 % (1250502)------------------------------ % 235.30/34.10 % (1250502)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 235.30/34.10 % (1250502)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.30/34.10 % (1250502)CaDiCaL version: 2.1.3 % 235.30/34.10 % (1250502)Termination reason: Refutation not found, incomplete strategy % 280.13/40.41 % (1250502)Time elapsed: 0.810 s % 280.13/40.41 % (1250502)Peak memory usage: 91 MB % 280.13/40.41 % (1250502)Instructions burned: 1296 (million) % 280.13/40.41 % (1250502)------------------------------ % 280.13/40.41 % (1250502)------------------------------ % 280.13/40.41 % (1250514)lrs+2_10_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_main:tha=some:random_seed=675879895:s2a=on:i=71622:s2at=-1:rtra=on_2815 on theBenchmark for (2815ds/71622Mi) % 280.13/40.41 % (1250494)Instruction limit reached! % 280.13/40.41 % (1250494)------------------------------ % 280.13/40.41 % (1250494)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 280.13/40.41 % (1250494)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 280.13/40.41 % (1250494)CaDiCaL version: 2.1.3 % 280.13/40.41 % (1250494)Termination reason: Instruction limit % 280.13/40.41 % (1250494)Termination phase: Saturation % 280.13/40.41 % (1250494)Time elapsed: 3.031 s % 280.13/40.41 % (1250494)Peak memory usage: 137 MB % 280.13/40.41 % (1250494)Instructions burned: 4081 (million) % 280.13/40.41 % (1250519)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=600493692:i=24001:kws=precedence:nm=0:rtra=on_2810 on theBenchmark for (2810ds/24001Mi) % 280.13/40.41 % (1250431)Instruction limit reached! % 280.13/40.41 % (1250431)------------------------------ % 280.13/40.41 % (1250431)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 280.13/40.41 % (1250431)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 280.13/40.41 % (1250431)CaDiCaL version: 2.1.3 % 280.13/40.41 % (1250431)Termination reason: Instruction limit % 280.13/40.41 % (1250431)Termination phase: Saturation % 280.13/40.41 % (1250431)Time elapsed: 4.874 s % 280.13/40.41 % (1250431)Peak memory usage: 122 MB % 280.13/40.41 % (1250431)Instructions burned: 11747 (million) % 280.13/40.41 % (1250530)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=937642992:i=2076:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2806 on theBenchmark for (2806ds/2076Mi) % 280.13/40.41 % (1249994)Instruction limit reached! % 280.13/40.41 % (1249994)------------------------------ % 280.13/40.41 % (1249994)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 280.13/40.41 % (1249994)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 280.13/40.41 % (1249994)CaDiCaL version: 2.1.3 % 280.13/40.41 % (1249994)Termination reason: Instruction limit % 280.13/40.41 % (1249994)Termination phase: Saturation % 280.13/40.41 % (1249994)Time elapsed: 8.930 s % 280.13/40.41 % (1249994)Peak memory usage: 94 MB % 280.13/40.41 % (1249994)Instructions burned: 17166 (million) % 280.13/40.41 % (1250530)Instruction limit reached! % 280.13/40.41 % (1250530)------------------------------ % 280.13/40.41 % (1250530)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 280.13/40.41 % (1250530)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 280.13/40.41 % (1250530)CaDiCaL version: 2.1.3 % 280.13/40.41 % (1250530)Termination reason: Instruction limit % 280.13/40.41 % (1250530)Termination phase: Saturation % 280.13/40.41 % (1250530)Time elapsed: 0.856 s % 280.13/40.41 % (1250530)Peak memory usage: 118 MB % 280.13/40.41 % (1250530)Instructions burned: 2078 (million) % 280.13/40.41 % (1250532)dis+21_20_to=lakbo:si=on:alasca=on:sp=const_max:uwa=alasca_main:sac=on:random_seed=3345936096:s2a=on:i=83971:s2at=4:bd=all:ins=1:rtra=on_2797 on theBenchmark for (2797ds/83971Mi) % 280.13/40.41 % (1250533)lrs+1011_5:1_to=lpo:sil=128000:sas=z3:si=on:norm_ineq=on:tha=some:random_seed=3150441899:i=83944:rtra=on_2795 on theBenchmark for (2795ds/83944Mi) % 280.13/40.41 % (1250504)Instruction limit reached! % 280.13/40.41 % (1250504)------------------------------ % 280.13/40.41 % (1250504)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 280.13/40.41 % (1250504)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 280.13/40.41 % (1250504)CaDiCaL version: 2.1.3 % 280.13/40.41 % (1250504)Termination reason: Instruction limit % 280.13/40.41 % (1250504)Termination phase: Saturation % 280.13/40.41 % (1250504)Time elapsed: 4.829 s % 280.13/40.41 % (1250504)Peak memory usage: 118 MB % 280.13/40.41 % (1250504)Instructions burned: 6259 (million) % 280.13/40.41 % (1250538)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=3886576390:i=9201:rtra=on_2776 on theBenchmark for (2776ds/9201Mi) % 280.13/40.41 % (1250538)Instruction limit reached! % 280.13/40.41 % (1250538)------------------------------ % 280.13/40.41 % (1250538)Version: Vampire 5.0.1 (Release build, commit eaTerminated %------------------------------------------------------------------------------