%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWC426_1 : TPTP v9.3.1. Bugfixed v9.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % Computer : n004.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:03:56 PM UTC 2026 % Result : Timeout 291.48s 42.16s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWC426_1 : TPTP v9.3.1. Bugfixed v9.1.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.11/0.21 % Computer : n004.cluster.edu % 0.11/0.21 % Model : x86_64 x86_64 % 0.11/0.21 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.21 % Memory : 8046.5625MB % 0.11/0.21 % OS : Linux 6.8.0-71-generic % 0.11/0.21 % CPULimit : 300 % 0.11/0.21 % WCLimit : 300 % 0.11/0.21 % DateTime : Mon Sep 28 09:36:37 UTC 2026 % 0.11/0.21 % CPUTime : % 0.11/0.21 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.11/0.24 Running first-order theorem proving % 0.11/0.24 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 4.19/1.34 % (233301)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule. % 4.19/1.34 % (233307)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=209781551:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi) % 4.19/1.34 % (233307)Refutation not found, incomplete strategy % 4.19/1.34 % (233307)------------------------------ % 4.19/1.34 % (233307)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.19/1.34 % (233307)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.19/1.34 % (233307)CaDiCaL version: 2.1.3 % 4.19/1.34 % (233307)Termination reason: Refutation not found, incomplete strategy % 4.19/1.34 % (233307)Time elapsed: 0.032 s % 4.19/1.34 % (233307)Peak memory usage: 116 MB % 4.19/1.34 % (233307)Instructions burned: 39 (million) % 4.19/1.34 % (233309)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=3550205436:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi) % 4.19/1.34 % (233312)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=644331553:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi) % 4.19/1.34 % (233306)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=3345967880:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi) % 4.19/1.34 % (233308)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=27968527:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi) % 4.19/1.34 % (233310)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=3400854307:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi) % 4.19/1.34 % (233311)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=1714821465:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi) % 4.19/1.34 % (233310)Instruction limit reached! % 4.19/1.34 % (233310)------------------------------ % 4.19/1.34 % (233310)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.19/1.34 % (233310)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.19/1.34 % (233310)CaDiCaL version: 2.1.3 % 4.19/1.34 % (233310)Termination reason: Instruction limit % 4.19/1.34 % (233310)Termination phase: Saturation % 4.19/1.34 % (233310)Time elapsed: 0.003 s % 4.19/1.34 % (233310)Peak memory usage: 88 MB % 4.19/1.34 % (233310)Instructions burned: 4 (million) % 4.19/1.34 % (233309)Instruction limit reached! % 4.19/1.34 % (233309)------------------------------ % 4.19/1.34 % (233309)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.19/1.34 % (233309)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.19/1.34 % (233309)CaDiCaL version: 2.1.3 % 4.19/1.34 % (233309)Termination reason: Instruction limit % 4.19/1.34 % (233309)Termination phase: Saturation % 4.19/1.34 % (233309)Time elapsed: 0.004 s % 4.19/1.34 % (233309)Peak memory usage: 88 MB % 4.19/1.34 % (233309)Instructions burned: 7 (million) % 4.19/1.34 % (233311)Refutation not found, incomplete strategy % 4.19/1.34 % (233311)------------------------------ % 4.19/1.34 % (233311)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.19/1.34 % (233311)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.19/1.34 % (233311)CaDiCaL version: 2.1.3 % 4.19/1.34 % (233311)Termination reason: Refutation not found, incomplete strategy % 4.19/1.34 % (233311)Time elapsed: 0.031 s % 4.19/1.34 % (233311)Peak memory usage: 115 MB % 4.19/1.34 % (233311)Instructions burned: 8 (million) % 4.19/1.34 % (233306)Instruction limit reached! % 4.19/1.34 % (233306)------------------------------ % 4.19/1.34 % (233306)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.19/1.34 % (233306)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.19/1.34 % (233306)CaDiCaL version: 2.1.3 % 4.19/1.34 % (233306)Termination reason: Instruction limit % 4.19/1.34 % (233306)Termination phase: Saturation % 4.19/1.34 % (233306)Time elapsed: 0.032 s % 4.19/1.34 % (233306)Peak memory usage: 115 MB % 4.19/1.34 % (233306)Instructions burned: 13 (million) % 4.19/1.34 % (233312)Instruction limit reached! % 4.19/1.34 % (233312)------------------------------ % 4.19/1.34 % (233312)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.19/1.34 % (233312)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.19/1.34 % (233312)CaDiCaL version: 2.1.3 % 4.19/1.34 % (233312)Termination reason: Instruction limit % 4.84/1.49 % (233312)Termination phase: Saturation % 4.84/1.49 % (233312)Time elapsed: 0.046 s % 4.84/1.49 % (233312)Peak memory usage: 116 MB % 4.84/1.49 % (233312)Instructions burned: 34 (million) % 4.84/1.49 % (233307)------------------------------ % 4.84/1.49 % (233307)------------------------------ % 4.84/1.49 % (233320)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=2039393169:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2998 on theBenchmark for (2998ds/14Mi) % 4.84/1.49 % (233320)Refutation not found, incomplete strategy % 4.84/1.49 % (233320)------------------------------ % 4.84/1.49 % (233320)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.84/1.49 % (233320)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.84/1.49 % (233320)CaDiCaL version: 2.1.3 % 4.84/1.49 % (233320)Termination reason: Refutation not found, incomplete strategy % 4.84/1.49 % (233320)Time elapsed: 0.002 s % 4.84/1.49 % (233320)Peak memory usage: 89 MB % 4.84/1.49 % (233320)Instructions burned: 1 (million) % 4.84/1.49 % (233308)Instruction limit reached! % 4.84/1.49 % (233308)------------------------------ % 4.84/1.49 % (233308)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.84/1.49 % (233308)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.84/1.49 % (233321)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=1646973167:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2998 on theBenchmark for (2998ds/29Mi) % 4.84/1.49 % (233308)CaDiCaL version: 2.1.3 % 4.84/1.49 % (233308)Termination reason: Instruction limit % 4.84/1.49 % (233308)Termination phase: Saturation % 4.84/1.49 % (233308)Time elapsed: 0.172 s % 4.84/1.49 % (233308)Peak memory usage: 117 MB % 4.84/1.49 % (233308)Instructions burned: 202 (million) % 4.84/1.49 % (233321)Instruction limit reached! % 4.84/1.49 % (233321)------------------------------ % 4.84/1.49 % (233321)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.84/1.49 % (233321)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.84/1.49 % (233321)CaDiCaL version: 2.1.3 % 4.84/1.49 % (233321)Termination reason: Instruction limit % 4.84/1.49 % (233321)Termination phase: Saturation % 4.84/1.49 % (233321)Time elapsed: 0.020 s % 4.84/1.49 % (233321)Peak memory usage: 88 MB % 4.84/1.49 % (233321)Instructions burned: 31 (million) % 4.84/1.49 % (233323)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=1304295338:i=24:canc=force:rtra=on_2997 on theBenchmark for (2997ds/24Mi) % 4.84/1.49 % (233322)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=2672165078:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2997 on theBenchmark for (2997ds/16Mi) % 4.84/1.49 % (233322)Instruction limit reached! % 4.84/1.49 % (233322)------------------------------ % 4.84/1.49 % (233322)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.84/1.49 % (233322)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.84/1.49 % (233322)CaDiCaL version: 2.1.3 % 4.84/1.49 % (233322)Termination reason: Instruction limit % 4.84/1.49 % (233322)Termination phase: Saturation % 4.84/1.49 % (233322)Time elapsed: 0.010 s % 4.84/1.49 % (233322)Peak memory usage: 90 MB % 4.84/1.49 % (233322)Instructions burned: 17 (million) % 4.84/1.49 % (233323)Instruction limit reached! % 4.84/1.49 % (233323)------------------------------ % 4.84/1.49 % (233323)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.84/1.49 % (233323)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.84/1.49 % (233323)CaDiCaL version: 2.1.3 % 4.84/1.49 % (233323)Termination reason: Instruction limit % 4.84/1.49 % (233323)Termination phase: Saturation % 4.84/1.49 % (233323)Time elapsed: 0.018 s % 4.84/1.49 % (233323)Peak memory usage: 89 MB % 4.84/1.49 % (233323)Instructions burned: 25 (million) % 4.84/1.49 % (233324)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=4050337331:i=27:canc=cautious:fsr=off:rtra=on_2996 on theBenchmark for (2996ds/27Mi) % 4.84/1.49 % (233324)Instruction limit reached! % 4.84/1.49 % (233324)------------------------------ % 4.84/1.49 % (233324)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.84/1.49 % (233324)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.84/1.49 % (233324)CaDiCaL version: 2.1.3 % 6.10/1.66 % (233324)Termination reason: Instruction limit % 6.10/1.66 % (233324)Termination phase: Saturation % 6.10/1.66 % (233324)Time elapsed: 0.008 s % 6.10/1.66 % (233324)Peak memory usage: 89 MB % 6.10/1.66 % (233324)Instructions burned: 28 (million) % 6.10/1.66 % (233311)------------------------------ % 6.10/1.66 % (233311)------------------------------ % 6.10/1.66 % (233327)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=1319887218:i=85:gtgl=4:rtra=on:gtg=exists_sym_2996 on theBenchmark for (2996ds/85Mi) % 6.10/1.66 % (233328)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=2710684974:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2996 on theBenchmark for (2996ds/2Mi) % 6.10/1.66 % (233328)Instruction limit reached! % 6.10/1.66 % (233328)------------------------------ % 6.10/1.66 % (233328)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.10/1.66 % (233328)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.10/1.66 % (233328)CaDiCaL version: 2.1.3 % 6.10/1.66 % (233328)Termination reason: Instruction limit % 6.10/1.66 % (233328)Termination phase: Saturation % 6.10/1.66 % (233328)Time elapsed: 0.003 s % 6.10/1.66 % (233328)Peak memory usage: 88 MB % 6.10/1.66 % (233328)Instructions burned: 4 (million) % 6.10/1.66 % (233331)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=2807444767:i=181:rtra=on:ss=axioms:ev=cautious_2996 on theBenchmark for (2996ds/181Mi) % 6.10/1.66 % (233331)Refutation not found, incomplete strategy % 6.10/1.66 % (233331)------------------------------ % 6.10/1.66 % (233331)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.10/1.66 % (233331)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.10/1.66 % (233331)CaDiCaL version: 2.1.3 % 6.10/1.66 % (233331)Termination reason: Refutation not found, incomplete strategy % 6.10/1.66 % (233331)Time elapsed: 0.003 s % 6.10/1.66 % (233331)Peak memory usage: 89 MB % 6.10/1.66 % (233331)Instructions burned: 2 (million) % 6.10/1.66 % (233334)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=8008816:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2995 on theBenchmark for (2995ds/66Mi) % 6.10/1.66 % (233332)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=2557886880:i=4:ep=RST:ins=2:rtra=on_2996 on theBenchmark for (2996ds/4Mi) % 6.10/1.66 % (233332)Instruction limit reached! % 6.10/1.66 % (233332)------------------------------ % 6.10/1.66 % (233332)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.10/1.66 % (233332)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.10/1.66 % (233332)CaDiCaL version: 2.1.3 % 6.10/1.66 % (233332)Termination reason: Instruction limit % 6.10/1.66 % (233332)Termination phase: Saturation % 6.10/1.66 % (233332)Time elapsed: 0.004 s % 6.10/1.66 % (233332)Peak memory usage: 89 MB % 6.10/1.66 % (233332)Instructions burned: 5 (million) % 6.10/1.66 % (233327)Instruction limit reached! % 6.10/1.66 % (233327)------------------------------ % 6.10/1.66 % (233327)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.10/1.66 % (233327)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.10/1.66 % (233327)CaDiCaL version: 2.1.3 % 6.10/1.66 % (233327)Termination reason: Instruction limit % 6.10/1.66 % (233327)Termination phase: Saturation % 6.10/1.66 % (233327)Time elapsed: 0.057 s % 6.10/1.66 % (233327)Peak memory usage: 89 MB % 6.10/1.66 % (233327)Instructions burned: 85 (million) % 6.10/1.66 % (233320)------------------------------ % 6.10/1.66 % (233320)------------------------------ % 6.10/1.66 % (233334)Instruction limit reached! % 6.10/1.66 % (233334)------------------------------ % 6.10/1.66 % (233334)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.10/1.66 % (233334)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.10/1.66 % (233334)CaDiCaL version: 2.1.3 % 6.10/1.66 % (233334)Termination reason: Instruction limit % 6.10/1.66 % (233334)Termination phase: Saturation % 6.10/1.66 % (233334)Time elapsed: 0.053 s % 6.10/1.66 % (233334)Peak memory usage: 134 MB % 6.10/1.66 % (233334)Instructions burned: 67 (million) % 6.10/1.66 % (233335)lrs+10_1_thi=all:si=on:fd=off:random_seed=3879266245:i=53:rtra=on:gtg=all_2995 on theBenchmark for (2995ds/53Mi) % 6.10/1.66 % (233338)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=440968354:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2994 on theBenchmark for (2994ds/8Mi) % 7.15/1.92 % (233335)Instruction limit reached! % 7.15/1.92 % (233335)------------------------------ % 7.15/1.92 % (233335)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.15/1.92 % (233338)Instruction limit reached! % 7.15/1.92 % (233338)------------------------------ % 7.15/1.92 % (233338)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.15/1.92 % (233338)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.15/1.92 % (233338)CaDiCaL version: 2.1.3 % 7.15/1.92 % (233338)Termination reason: Instruction limit % 7.15/1.92 % (233338)Termination phase: Saturation % 7.15/1.92 % (233338)Time elapsed: 0.007 s % 7.15/1.92 % (233338)Peak memory usage: 88 MB % 7.15/1.92 % (233338)Instructions burned: 9 (million) % 7.15/1.92 % (233335)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.15/1.92 % (233335)CaDiCaL version: 2.1.3 % 7.15/1.92 % (233335)Termination reason: Instruction limit % 7.15/1.92 % (233335)Termination phase: Saturation % 7.15/1.92 % (233335)Time elapsed: 0.063 s % 7.15/1.92 % (233335)Peak memory usage: 116 MB % 7.15/1.92 % (233335)Instructions burned: 53 (million) % 7.15/1.92 % (233342)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=1483451057:st=3:i=2:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/2Mi) % 7.15/1.92 % (233342)Instruction limit reached! % 7.15/1.92 % (233342)------------------------------ % 7.15/1.92 % (233342)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.15/1.92 % (233342)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.15/1.92 % (233342)CaDiCaL version: 2.1.3 % 7.15/1.92 % (233342)Termination reason: Instruction limit % 7.15/1.92 % (233342)Termination phase: Saturation % 7.15/1.92 % (233342)Time elapsed: 0.003 s % 7.15/1.92 % (233342)Peak memory usage: 90 MB % 7.15/1.92 % (233342)Instructions burned: 3 (million) % 7.15/1.92 % (233343)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=246357689:i=2:doe=on:canc=force:asg=cautious:rtra=on_2994 on theBenchmark for (2994ds/2Mi) % 7.15/1.92 % (233343)Instruction limit reached! % 7.15/1.92 % (233343)------------------------------ % 7.15/1.92 % (233343)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.15/1.92 % (233343)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.15/1.92 % (233343)CaDiCaL version: 2.1.3 % 7.15/1.92 % (233343)Termination reason: Instruction limit % 7.15/1.92 % (233343)Termination phase: Saturation % 7.15/1.92 % (233343)Time elapsed: 0.003 s % 7.15/1.92 % (233343)Peak memory usage: 89 MB % 7.15/1.92 % (233343)Instructions burned: 3 (million) % 7.15/1.92 % (233344)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=2647490126:i=127:doe=on:rtra=on_2994 on theBenchmark for (2994ds/127Mi) % 7.15/1.92 % (233345)dis+10_1_si=on:random_seed=4188422971:i=10:ep=R:rtra=on_2994 on theBenchmark for (2994ds/10Mi) % 7.15/1.92 % (233345)Instruction limit reached! % 7.15/1.92 % (233345)------------------------------ % 7.15/1.92 % (233345)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.15/1.92 % (233345)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.15/1.92 % (233345)CaDiCaL version: 2.1.3 % 7.15/1.92 % (233345)Termination reason: Instruction limit % 7.15/1.92 % (233345)Termination phase: Saturation % 7.15/1.92 % (233345)Time elapsed: 0.007 s % 7.15/1.92 % (233345)Peak memory usage: 88 MB % 7.15/1.92 % (233345)Instructions burned: 11 (million) % 7.15/1.92 % (233331)------------------------------ % 7.15/1.92 % (233331)------------------------------ % 7.15/1.92 % (233344)Instruction limit reached! % 7.15/1.92 % (233344)------------------------------ % 7.15/1.92 % (233344)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.15/1.92 % (233344)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.15/1.92 % (233344)CaDiCaL version: 2.1.3 % 7.15/1.92 % (233344)Termination reason: Instruction limit % 7.15/1.92 % (233344)Termination phase: Saturation % 7.15/1.92 % (233344)Time elapsed: 0.092 s % 7.15/1.92 % (233344)Peak memory usage: 116 MB % 7.15/1.92 % (233344)Instructions burned: 128 (million) % 7.15/1.92 % (233348)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=3169040142:i=26:canc=cautious:av=off:rtra=on_2993 on theBenchmark for (2993ds/26Mi) % 7.15/1.92 % (233349)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=3069359704:avsq=on:i=35:doe=on:thsqd=64:nm=64:fsr=off:thsqc=32:rtra=on:tac=light:ss=included:thsq=on:ev=off:sgt=32_2993 on theBenchmark for (2993ds/35Mi) % 10.66/2.17 % (233348)Refutation not found, incomplete strategy % 10.66/2.17 % (233348)------------------------------ % 10.66/2.17 % (233348)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.66/2.17 % (233348)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.66/2.17 % (233348)CaDiCaL version: 2.1.3 % 10.66/2.17 % (233348)Termination reason: Refutation not found, incomplete strategy % 10.66/2.17 % (233348)Time elapsed: 0.003 s % 10.66/2.17 % (233348)Peak memory usage: 89 MB % 10.66/2.17 % (233348)Instructions burned: 2 (million) % 10.66/2.17 % (233351)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=1350924706:i=2:fsr=off:rtra=on:inst=on_2993 on theBenchmark for (2993ds/2Mi) % 10.66/2.17 % (233351)Instruction limit reached! % 10.66/2.17 % (233351)------------------------------ % 10.66/2.17 % (233351)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.66/2.17 % (233351)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.66/2.17 % (233351)CaDiCaL version: 2.1.3 % 10.66/2.17 % (233351)Termination reason: Instruction limit % 10.66/2.17 % (233351)Termination phase: Saturation % 10.66/2.17 % (233351)Time elapsed: 0.003 s % 10.66/2.17 % (233351)Peak memory usage: 89 MB % 10.66/2.17 % (233351)Instructions burned: 4 (million) % 10.66/2.17 % (233353)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=4060111532:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2993 on theBenchmark for (2993ds/8Mi) % 10.66/2.17 % (233349)Instruction limit reached! % 10.66/2.17 % (233349)------------------------------ % 10.66/2.17 % (233349)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.66/2.17 % (233349)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.66/2.17 % (233349)CaDiCaL version: 2.1.3 % 10.66/2.17 % (233349)Termination reason: Instruction limit % 10.66/2.17 % (233349)Termination phase: Saturation % 10.66/2.17 % (233349)Time elapsed: 0.026 s % 10.66/2.17 % (233349)Peak memory usage: 89 MB % 10.66/2.17 % (233349)Instructions burned: 35 (million) % 10.66/2.17 % (233353)Instruction limit reached! % 10.66/2.17 % (233353)------------------------------ % 10.66/2.17 % (233353)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.66/2.17 % (233353)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.66/2.17 % (233353)CaDiCaL version: 2.1.3 % 10.66/2.17 % (233353)Termination reason: Instruction limit % 10.66/2.17 % (233353)Termination phase: Saturation % 10.66/2.17 % (233353)Time elapsed: 0.006 s % 10.66/2.17 % (233353)Peak memory usage: 89 MB % 10.66/2.17 % (233353)Instructions burned: 8 (million) % 10.66/2.17 % (233356)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=2248471869:i=370:ep=RS:fsr=off:rtra=on_2992 on theBenchmark for (2992ds/370Mi) % 10.66/2.17 % (233357)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=2463198021:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2992 on theBenchmark for (2992ds/13Mi) % 10.66/2.17 % (233360)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=896003847:i=226:rtra=on:gtg=position:ss=axioms_2991 on theBenchmark for (2991ds/226Mi) % 10.66/2.17 % (233357)Instruction limit reached! % 10.66/2.17 % (233357)------------------------------ % 10.66/2.17 % (233357)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.66/2.17 % (233357)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.66/2.17 % (233357)CaDiCaL version: 2.1.3 % 10.66/2.17 % (233357)Termination reason: Instruction limit % 10.66/2.17 % (233357)Termination phase: Saturation % 10.66/2.17 % (233357)Time elapsed: 0.034 s % 10.66/2.17 % (233357)Peak memory usage: 116 MB % 10.66/2.17 % (233357)Instructions burned: 14 (million) % 10.66/2.17 % (233362)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=955913063:i=10:rtra=on_2991 on theBenchmark for (2991ds/10Mi) % 10.66/2.17 % (233362)Refutation not found, incomplete strategy % 10.66/2.17 % (233362)------------------------------ % 10.66/2.17 % (233362)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.66/2.17 % (233362)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.66/2.17 % (233362)CaDiCaL version: 2.1.3 % 10.66/2.17 % (233362)Termination reason: Refutation not found, incomplete strategy % 10.66/2.17 % (233362)Time elapsed: 0.002 s % 10.66/2.17 % (233362)Peak memory usage: 88 MB % 10.66/2.17 % (233364)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=3822239610:i=71:rtra=on:gtg=exists_top_2991 on theBenchmark for (2991ds/71Mi) % 11.83/2.50 % (233360)Refutation not found, incomplete strategy % 11.83/2.50 % (233360)------------------------------ % 11.83/2.50 % (233360)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.83/2.50 % (233360)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.83/2.50 % (233360)CaDiCaL version: 2.1.3 % 11.83/2.50 % (233360)Termination reason: Refutation not found, incomplete strategy % 11.83/2.50 % (233360)Time elapsed: 0.030 s % 11.83/2.50 % (233360)Peak memory usage: 116 MB % 11.83/2.50 % (233360)Instructions burned: 7 (million) % 11.83/2.50 % (233356)Instruction limit reached! % 11.83/2.50 % (233356)------------------------------ % 11.83/2.50 % (233356)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.83/2.50 % (233356)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.83/2.50 % (233356)CaDiCaL version: 2.1.3 % 11.83/2.50 % (233356)Termination reason: Instruction limit % 11.83/2.50 % (233356)Termination phase: Saturation % 11.83/2.50 % (233356)Time elapsed: 0.097 s % 11.83/2.50 % (233356)Peak memory usage: 89 MB % 11.83/2.50 % (233356)Instructions burned: 372 (million) % 11.83/2.50 % (233365)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=1661940402:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2991 on theBenchmark for (2991ds/75Mi) % 11.83/2.50 % (233364)Refutation not found, incomplete strategy % 11.83/2.50 % (233364)------------------------------ % 11.83/2.50 % (233364)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.83/2.50 % (233364)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.83/2.50 % (233364)CaDiCaL version: 2.1.3 % 11.83/2.50 % (233364)Termination reason: Refutation not found, incomplete strategy % 11.83/2.50 % (233364)Time elapsed: 0.054 s % 11.83/2.50 % (233364)Peak memory usage: 132 MB % 11.83/2.50 % (233364)Instructions burned: 12 (million) % 11.83/2.50 % (233365)Instruction limit reached! % 11.83/2.50 % (233365)------------------------------ % 11.83/2.50 % (233365)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.83/2.50 % (233365)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.83/2.50 % (233365)CaDiCaL version: 2.1.3 % 11.83/2.50 % (233365)Termination reason: Instruction limit % 11.83/2.50 % (233365)Termination phase: Saturation % 11.83/2.50 % (233365)Time elapsed: 0.038 s % 11.83/2.50 % (233365)Peak memory usage: 89 MB % 11.83/2.50 % (233365)Instructions burned: 75 (million) % 11.83/2.50 % (233348)------------------------------ % 11.83/2.50 % (233348)------------------------------ % 11.83/2.50 % (233369)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=4175345717:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2990 on theBenchmark for (2990ds/294Mi) % 11.83/2.50 % (233373)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=3731933940:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2990 on theBenchmark for (2990ds/130Mi) % 11.83/2.50 % (233373)Refutation not found, incomplete strategy % 11.83/2.50 % (233373)------------------------------ % 11.83/2.50 % (233373)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.83/2.50 % (233373)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.83/2.50 % (233373)CaDiCaL version: 2.1.3 % 11.83/2.50 % (233373)Termination reason: Refutation not found, incomplete strategy % 11.83/2.50 % (233373)Time elapsed: 0.026 s % 11.83/2.50 % (233373)Peak memory usage: 117 MB % 11.83/2.50 % (233373)Instructions burned: 28 (million) % 11.83/2.50 % (233374)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=633986204:i=131:rtra=on_2989 on theBenchmark for (2989ds/131Mi) % 11.83/2.50 % (233362)------------------------------ % 11.83/2.50 % (233362)------------------------------ % 11.83/2.50 % (233360)------------------------------ % 11.83/2.50 % (233360)------------------------------ % 11.83/2.50 % (233375)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=3229665672:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2989 on theBenchmark for (2989ds/40Mi) % 11.83/2.50 % (233369)Instruction limit reached! % 11.83/2.50 % (233369)------------------------------ % 11.83/2.50 % (233369)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.83/2.50 % (233369)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.48/2.74 % (233369)CaDiCaL version: 2.1.3 % 13.48/2.74 % (233369)Termination reason: Instruction limit % 13.48/2.74 % (233369)Termination phase: Saturation % 13.48/2.74 % (233369)Time elapsed: 0.127 s % 13.48/2.74 % (233369)Peak memory usage: 88 MB % 13.48/2.74 % (233369)Instructions burned: 297 (million) % 13.48/2.74 % (233374)Refutation not found, incomplete strategy % 13.48/2.74 % (233374)------------------------------ % 13.48/2.74 % (233374)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.48/2.74 % (233374)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.48/2.74 % (233374)CaDiCaL version: 2.1.3 % 13.48/2.74 % (233374)Termination reason: Refutation not found, incomplete strategy % 13.48/2.74 % (233374)Time elapsed: 0.055 s % 13.48/2.74 % (233374)Peak memory usage: 132 MB % 13.48/2.74 % (233374)Instructions burned: 12 (million) % 13.48/2.74 % (233364)------------------------------ % 13.48/2.74 % (233364)------------------------------ % 13.48/2.74 % (233373)------------------------------ % 13.48/2.74 % (233373)------------------------------ % 13.48/2.74 % (233375)Instruction limit reached! % 13.48/2.74 % (233375)------------------------------ % 13.48/2.74 % (233375)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.48/2.74 % (233375)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.48/2.74 % (233375)CaDiCaL version: 2.1.3 % 13.48/2.74 % (233375)Termination reason: Instruction limit % 13.48/2.74 % (233375)Termination phase: Saturation % 13.48/2.74 % (233375)Time elapsed: 0.073 s % 13.48/2.74 % (233375)Peak memory usage: 133 MB % 13.48/2.74 % (233375)Instructions burned: 40 (million) % 13.48/2.74 % (233380)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=3129228209:i=307:rtra=on:gtg=exists_top_2987 on theBenchmark for (2987ds/307Mi) % 13.48/2.74 % (233381)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=1198746463:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2987 on theBenchmark for (2987ds/598Mi) % 13.48/2.74 % (233382)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=1065304777:i=131:canc=cautious:fsr=off:rtra=on_2987 on theBenchmark for (2987ds/131Mi) % 13.48/2.74 % (233384)dis+10_1_si=on:random_seed=145616390:s2a=on:i=1000:rtra=on:gtg=exists_all_2987 on theBenchmark for (2987ds/1000Mi) % 13.48/2.74 % (233381)Refutation not found, incomplete strategy % 13.48/2.74 % (233381)------------------------------ % 13.48/2.74 % (233381)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.48/2.74 % (233381)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.48/2.74 % (233381)CaDiCaL version: 2.1.3 % 13.48/2.74 % (233381)Termination reason: Refutation not found, incomplete strategy % 13.48/2.74 % (233381)Time elapsed: 0.056 s % 13.48/2.74 % (233381)Peak memory usage: 133 MB % 13.48/2.74 % (233381)Instructions burned: 14 (million) % 13.48/2.74 % (233383)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=631892865:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2987 on theBenchmark for (2987ds/259Mi) % 13.48/2.74 % (233385)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=2362905840:i=383:fsr=off:rtra=on:ev=force_2986 on theBenchmark for (2986ds/383Mi) % 13.48/2.74 % (233385)Refutation not found, incomplete strategy % 13.48/2.74 % (233385)------------------------------ % 13.48/2.74 % (233385)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.48/2.74 % (233385)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.48/2.74 % (233385)CaDiCaL version: 2.1.3 % 13.48/2.74 % (233385)Termination reason: Refutation not found, incomplete strategy % 13.48/2.74 % (233385)Time elapsed: 0.004 s % 13.48/2.74 % (233385)Peak memory usage: 89 MB % 13.48/2.74 % (233385)Instructions burned: 4 (million) % 13.48/2.74 % (233382)Instruction limit reached! % 13.48/2.74 % (233382)------------------------------ % 13.48/2.74 % (233382)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.48/2.74 % (233382)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.48/2.74 % (233382)CaDiCaL version: 2.1.3 % 13.48/2.74 % (233382)Termination reason: Instruction limit % 13.48/2.74 % (233382)Termination phase: Saturation % 13.48/2.74 % (233382)Time elapsed: 0.091 s % 13.48/2.74 % (233382)Peak memory usage: 116 MB % 13.48/2.74 % (233382)Instructions burned: 131 (million) % 13.48/2.74 % (233374)------------------------------ % 16.97/3.06 % (233374)------------------------------ % 16.97/3.06 % (233380)Instruction limit reached! % 16.97/3.06 % (233380)------------------------------ % 16.97/3.06 % (233380)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.97/3.06 % (233380)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.97/3.06 % (233380)CaDiCaL version: 2.1.3 % 16.97/3.06 % (233380)Termination reason: Instruction limit % 16.97/3.06 % (233380)Termination phase: Saturation % 16.97/3.06 % (233380)Time elapsed: 0.155 s % 16.97/3.06 % (233380)Peak memory usage: 91 MB % 16.97/3.06 % (233380)Instructions burned: 307 (million) % 16.97/3.06 % (233383)Instruction limit reached! % 16.97/3.06 % (233383)------------------------------ % 16.97/3.06 % (233383)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.97/3.06 % (233383)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.97/3.06 % (233383)CaDiCaL version: 2.1.3 % 16.97/3.06 % (233383)Termination reason: Instruction limit % 16.97/3.06 % (233383)Termination phase: Saturation % 16.97/3.06 % (233383)Time elapsed: 0.168 s % 16.97/3.06 % (233383)Peak memory usage: 116 MB % 16.97/3.06 % (233383)Instructions burned: 259 (million) % 16.97/3.06 % (233392)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=2658113094:i=141:doe=on:rtra=on_2985 on theBenchmark for (2985ds/141Mi) % 16.97/3.06 % (233393)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=647715197:i=65:nm=16:rtra=on_2985 on theBenchmark for (2985ds/65Mi) % 16.97/3.06 % (233381)------------------------------ % 16.97/3.06 % (233381)------------------------------ % 16.97/3.06 % (233394)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=3087473606:i=121:nm=16:rtra=on_2984 on theBenchmark for (2984ds/121Mi) % 16.97/3.06 % (233393)Refutation not found, incomplete strategy % 16.97/3.06 % (233393)------------------------------ % 16.97/3.06 % (233393)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.97/3.06 % (233393)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.97/3.06 % (233393)CaDiCaL version: 2.1.3 % 16.97/3.06 % (233393)Termination reason: Refutation not found, incomplete strategy % 16.97/3.06 % (233393)Time elapsed: 0.029 s % 16.97/3.06 % (233393)Peak memory usage: 115 MB % 16.97/3.06 % (233393)Instructions burned: 6 (million) % 16.97/3.06 % (233385)------------------------------ % 16.97/3.06 % (233385)------------------------------ % 16.97/3.06 % (233392)Instruction limit reached! % 16.97/3.06 % (233392)------------------------------ % 16.97/3.06 % (233392)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.97/3.06 % (233392)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.97/3.06 % (233392)CaDiCaL version: 2.1.3 % 16.97/3.06 % (233392)Termination reason: Instruction limit % 16.97/3.06 % (233392)Termination phase: Saturation % 16.97/3.06 % (233392)Time elapsed: 0.091 s % 16.97/3.06 % (233392)Peak memory usage: 90 MB % 16.97/3.06 % (233392)Instructions burned: 141 (million) % 16.97/3.06 % (233384)Instruction limit reached! % 16.97/3.06 % (233384)------------------------------ % 16.97/3.06 % (233384)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.97/3.06 % (233384)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.97/3.06 % (233384)CaDiCaL version: 2.1.3 % 16.97/3.06 % (233384)Termination reason: Instruction limit % 16.97/3.06 % (233384)Termination phase: Saturation % 16.97/3.06 % (233384)Time elapsed: 0.324 s % 16.97/3.06 % (233384)Peak memory usage: 95 MB % 16.97/3.06 % (233384)Instructions burned: 1002 (million) % 16.97/3.06 % (233394)Instruction limit reached! % 16.97/3.06 % (233394)------------------------------ % 16.97/3.06 % (233394)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.97/3.06 % (233394)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.97/3.06 % (233394)CaDiCaL version: 2.1.3 % 16.97/3.06 % (233394)Termination reason: Instruction limit % 16.97/3.06 % (233394)Termination phase: Saturation % 16.97/3.06 % (233394)Time elapsed: 0.053 s % 16.97/3.06 % (233394)Peak memory usage: 88 MB % 16.97/3.06 % (233394)Instructions burned: 123 (million) % 16.97/3.06 % (233395)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=455185731:s2a=on:i=128:s2at=5:ins=3:rtra=on_2983 on theBenchmark for (2983ds/128Mi) % 16.97/3.06 % (233399)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=541571467:i=39:ins=3:rtra=on_2983 on theBenchmark for (2983ds/39Mi) % 18.13/3.32 % (233402)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=4022547070:s2a=on:i=483:doe=on:nm=32:rtra=on_2982 on theBenchmark for (2982ds/483Mi) % 18.13/3.32 % (233400)dis+1010_1_to=kbo:si=on:random_seed=4173893645:i=175:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2982 on theBenchmark for (2982ds/175Mi) % 18.13/3.32 % (233402)Refutation not found, incomplete strategy % 18.13/3.32 % (233402)------------------------------ % 18.13/3.32 % (233402)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.13/3.32 % (233402)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.13/3.32 % (233402)CaDiCaL version: 2.1.3 % 18.13/3.32 % (233402)Termination reason: Refutation not found, incomplete strategy % 18.13/3.32 % (233402)Time elapsed: 0.033 s % 18.13/3.32 % (233402)Peak memory usage: 132 MB % 18.13/3.32 % (233402)Instructions burned: 12 (million) % 18.13/3.32 % (233395)Instruction limit reached! % 18.13/3.32 % (233395)------------------------------ % 18.13/3.32 % (233395)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.13/3.32 % (233395)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.13/3.32 % (233395)CaDiCaL version: 2.1.3 % 18.13/3.32 % (233395)Termination reason: Instruction limit % 18.13/3.32 % (233395)Termination phase: Saturation % 18.13/3.32 % (233395)Time elapsed: 0.111 s % 18.13/3.32 % (233395)Peak memory usage: 118 MB % 18.13/3.32 % (233395)Instructions burned: 130 (million) % 18.13/3.32 % (233399)Instruction limit reached! % 18.13/3.32 % (233399)------------------------------ % 18.13/3.32 % (233399)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.13/3.32 % (233399)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.13/3.32 % (233399)CaDiCaL version: 2.1.3 % 18.13/3.32 % (233399)Termination reason: Instruction limit % 18.13/3.32 % (233399)Termination phase: Saturation % 18.13/3.32 % (233399)Time elapsed: 0.051 s % 18.13/3.32 % (233399)Peak memory usage: 116 MB % 18.13/3.32 % (233399)Instructions burned: 40 (million) % 18.13/3.32 % (233401)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=1829743915:i=329:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2982 on theBenchmark for (2982ds/329Mi) % 18.13/3.32 % (233403)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=2315485705:thitd=on:i=215:nm=0:rtra=on:ev=force_2982 on theBenchmark for (2982ds/215Mi) % 18.13/3.32 % (233393)------------------------------ % 18.13/3.32 % (233393)------------------------------ % 18.13/3.32 % (233403)Refutation not found, incomplete strategy % 18.13/3.32 % (233403)------------------------------ % 18.13/3.32 % (233403)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.13/3.32 % (233403)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.13/3.32 % (233403)CaDiCaL version: 2.1.3 % 18.13/3.32 % (233403)Termination reason: Refutation not found, incomplete strategy % 18.13/3.32 % (233403)Time elapsed: 0.073 s % 18.13/3.32 % (233403)Peak memory usage: 134 MB % 18.13/3.32 % (233403)Instructions burned: 39 (million) % 18.13/3.32 % (233400)Instruction limit reached! % 18.13/3.32 % (233400)------------------------------ % 18.13/3.32 % (233400)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.13/3.32 % (233400)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.13/3.32 % (233400)CaDiCaL version: 2.1.3 % 18.13/3.32 % (233400)Termination reason: Instruction limit % 18.13/3.32 % (233400)Termination phase: Saturation % 18.13/3.32 % (233400)Time elapsed: 0.129 s % 18.13/3.32 % (233400)Peak memory usage: 91 MB % 18.13/3.32 % (233400)Instructions burned: 175 (million) % 18.13/3.32 % (233402)------------------------------ % 18.13/3.32 % (233402)------------------------------ % 18.13/3.32 % (233408)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=4059534826:i=349:rtra=on_2981 on theBenchmark for (2981ds/349Mi) % 18.13/3.32 % (233409)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=595656172:st=2:i=295:rtra=on:ss=axioms_2981 on theBenchmark for (2981ds/295Mi) % 18.13/3.32 % (233408)Refutation not found, incomplete strategy % 18.13/3.32 % (233408)------------------------------ % 18.13/3.32 % (233408)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.13/3.32 % (233408)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.62/3.63 % (233408)CaDiCaL version: 2.1.3 % 19.62/3.63 % (233408)Termination reason: Refutation not found, incomplete strategy % 19.62/3.63 % (233408)Time elapsed: 0.029 s % 19.62/3.63 % (233408)Peak memory usage: 116 MB % 19.62/3.63 % (233408)Instructions burned: 7 (million) % 19.62/3.63 % (233412)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=2942283260:i=328:kws=inv_frequency:nm=20:rtra=on_2980 on theBenchmark for (2980ds/328Mi) % 19.62/3.63 % (233413)dis+1010_1_to=lpo:sil=128000:sas=z3:si=on:nwc=5:random_seed=1877106700:i=281:gtgl=2:rtra=on:gtg=all_2980 on theBenchmark for (2980ds/281Mi) % 19.62/3.63 % (233414)lrs+1010_1_to=kbo:sil=128000:si=on:sos=on:urr=on:uwa=alasca_main:random_seed=2700299932:i=484:doe=on:nm=0:av=off:rtra=on:ss=axioms_2979 on theBenchmark for (2979ds/484Mi) % 19.62/3.63 % (233401)Instruction limit reached! % 19.62/3.63 % (233401)------------------------------ % 19.62/3.63 % (233401)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.62/3.63 % (233401)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.62/3.63 % (233401)CaDiCaL version: 2.1.3 % 19.62/3.63 % (233401)Termination reason: Instruction limit % 19.62/3.63 % (233401)Termination phase: Saturation % 19.62/3.63 % (233401)Time elapsed: 0.263 s % 19.62/3.63 % (233401)Peak memory usage: 118 MB % 19.62/3.63 % (233401)Instructions burned: 330 (million) % 19.62/3.63 % (233409)Instruction limit reached! % 19.62/3.63 % (233409)------------------------------ % 19.62/3.63 % (233409)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.62/3.63 % (233409)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.62/3.63 % (233409)CaDiCaL version: 2.1.3 % 19.62/3.63 % (233409)Termination reason: Instruction limit % 19.62/3.63 % (233409)Termination phase: Saturation % 19.62/3.63 % (233409)Time elapsed: 0.166 s % 19.62/3.63 % (233409)Peak memory usage: 90 MB % 19.62/3.63 % (233409)Instructions burned: 297 (million) % 19.62/3.63 % (233403)------------------------------ % 19.62/3.63 % (233403)------------------------------ % 19.62/3.63 % (233414)Instruction limit reached! % 19.62/3.63 % (233414)------------------------------ % 19.62/3.63 % (233414)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.62/3.63 % (233414)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.62/3.63 % (233414)CaDiCaL version: 2.1.3 % 19.62/3.63 % (233414)Termination reason: Instruction limit % 19.62/3.63 % (233414)Termination phase: Saturation % 19.62/3.63 % (233414)Time elapsed: 0.125 s % 19.62/3.63 % (233414)Peak memory usage: 90 MB % 19.62/3.63 % (233414)Instructions burned: 486 (million) % 19.62/3.63 % (233408)------------------------------ % 19.62/3.63 % (233408)------------------------------ % 19.62/3.63 % (233420)lrs+21_1_to=kbo:sil=128000:thi=neg_eq:si=on:random_seed=207917296:i=321:canc=force:rtra=on:tac=axiom:ss=axioms:ev=force_2978 on theBenchmark for (2978ds/321Mi) % 19.62/3.63 % (233413)Instruction limit reached! % 19.62/3.63 % (233413)------------------------------ % 19.62/3.63 % (233413)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.62/3.63 % (233413)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.62/3.63 % (233413)CaDiCaL version: 2.1.3 % 19.62/3.63 % (233413)Termination reason: Instruction limit % 19.62/3.63 % (233413)Termination phase: Saturation % 19.62/3.63 % (233413)Time elapsed: 0.193 s % 19.62/3.63 % (233413)Peak memory usage: 117 MB % 19.62/3.63 % (233413)Instructions burned: 281 (million) % 19.62/3.63 % (233412)Instruction limit reached! % 19.62/3.63 % (233412)------------------------------ % 19.62/3.63 % (233412)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.62/3.63 % (233412)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.62/3.63 % (233412)CaDiCaL version: 2.1.3 % 19.62/3.63 % (233412)Termination reason: Instruction limit % 19.62/3.63 % (233412)Termination phase: Saturation % 19.62/3.63 % (233412)Time elapsed: 0.237 s % 19.62/3.63 % (233412)Peak memory usage: 119 MB % 19.62/3.63 % (233412)Instructions burned: 328 (million) % 19.62/3.63 % (233421)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=285864937:i=416:rtra=on:gtg=position:ss=axioms_2978 on theBenchmark for (2978ds/416Mi) % 19.62/3.63 % (233422)lrs+1010_1_to=kbo:tgt=ground:fde=unused:sas=z3:si=on:sp=unary_frequency:gve=force:spb=goal:tha=off:random_seed=3026036198:i=471:thf=on:kws=precedence:rtra=on_2977 on theBenchmark for (2977ds/471Mi) % 19.62/3.63 % (233423)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=3049006574:avsq=on:i=276:avsqr=1,2:rtra=on_2977 on theBenchmark for (2977ds/276Mi) % 21.73/3.93 % (233421)Refutation not found, incomplete strategy % 21.73/3.93 % (233421)------------------------------ % 21.73/3.93 % (233421)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.73/3.93 % (233421)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.73/3.93 % (233421)CaDiCaL version: 2.1.3 % 21.73/3.93 % (233421)Termination reason: Refutation not found, incomplete strategy % 21.73/3.93 % (233421)Time elapsed: 0.030 s % 21.73/3.93 % (233421)Peak memory usage: 116 MB % 21.73/3.93 % (233421)Instructions burned: 7 (million) % 21.73/3.93 % (233422)Refutation not found, incomplete strategy % 21.73/3.93 % (233422)------------------------------ % 21.73/3.93 % (233422)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.73/3.93 % (233422)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.73/3.93 % (233422)CaDiCaL version: 2.1.3 % 21.73/3.93 % (233422)Termination reason: Refutation not found, incomplete strategy % 21.73/3.93 % (233422)Time elapsed: 0.030 s % 21.73/3.93 % (233422)Peak memory usage: 116 MB % 21.73/3.93 % (233422)Instructions burned: 8 (million) % 21.73/3.93 % (233424)lrs+1010_2_to=kbo:sil=128000:tgt=ground:fde=unused:sas=z3:si=on:uwa=off:tha=off:nwc=1:random_seed=2264227690:i=375:kws=inv_arity_squared:rtra=on_2976 on theBenchmark for (2976ds/375Mi) % 21.73/3.93 % (233423)Instruction limit reached! % 21.73/3.93 % (233423)------------------------------ % 21.73/3.93 % (233423)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.73/3.93 % (233423)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.73/3.93 % (233423)CaDiCaL version: 2.1.3 % 21.73/3.93 % (233423)Termination reason: Instruction limit % 21.73/3.93 % (233423)Termination phase: Saturation % 21.73/3.93 % (233423)Time elapsed: 0.087 s % 21.73/3.93 % (233423)Peak memory usage: 133 MB % 21.73/3.93 % (233423)Instructions burned: 279 (million) % 21.73/3.93 % (233426)lrs+10_1_to=kbo:sil=128000:tgt=full:sas=z3:si=on:uwa=func_ext:slsqc=1:flr=on:slsq=on:random_seed=3198968021:i=387:bd=preordered:rtra=on:ss=axioms:sgt=8_2976 on theBenchmark for (2976ds/387Mi) % 21.73/3.93 % (233424)Refutation not found, incomplete strategy % 21.73/3.93 % (233424)------------------------------ % 21.73/3.93 % (233424)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.73/3.93 % (233424)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.73/3.93 % (233424)CaDiCaL version: 2.1.3 % 21.73/3.93 % (233424)Termination reason: Refutation not found, incomplete strategy % 21.73/3.93 % (233424)Time elapsed: 0.029 s % 21.73/3.93 % (233424)Peak memory usage: 115 MB % 21.73/3.93 % (233424)Instructions burned: 7 (million) % 21.73/3.93 % (233427)lrs+10_1_to=kbo:sil=128000:fde=none:si=on:norm_ineq=on:urr=on:nwc=0.5:random_seed=1731211248:i=513:kws=frequency:bd=all:rtra=on:gtg=exists_all:ss=axioms:sgt=4_2976 on theBenchmark for (2976ds/513Mi) % 21.73/3.93 % (233420)Instruction limit reached! % 21.73/3.93 % (233420)------------------------------ % 21.73/3.93 % (233420)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.73/3.93 % (233420)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.73/3.93 % (233420)CaDiCaL version: 2.1.3 % 21.73/3.93 % (233420)Termination reason: Instruction limit % 21.73/3.93 % (233420)Termination phase: Saturation % 21.73/3.93 % (233420)Time elapsed: 0.210 s % 21.73/3.93 % (233420)Peak memory usage: 115 MB % 21.73/3.93 % (233420)Instructions burned: 321 (million) % 21.73/3.93 % (233433)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=1985982976:i=334:rtra=on_2975 on theBenchmark for (2975ds/334Mi) % 21.73/3.93 % (233433)Refutation not found, incomplete strategy % 21.73/3.93 % (233433)------------------------------ % 21.73/3.93 % (233433)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.73/3.93 % (233433)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.73/3.93 % (233433)CaDiCaL version: 2.1.3 % 21.73/3.93 % (233433)Termination reason: Refutation not found, incomplete strategy % 21.73/3.93 % (233433)Time elapsed: 0.033 s % 21.73/3.93 % (233433)Peak memory usage: 132 MB % 21.73/3.93 % (233433)Instructions burned: 12 (million) % 21.73/3.93 % (233421)------------------------------ % 21.73/3.93 % (233421)------------------------------ % 21.73/3.93 % (233422)------------------------------ % 21.73/3.93 % (233422)------------------------------ % 25.54/4.30 % (233435)lrs+1010_1_to=kbo:sil=64000:sas=cadical:si=on:sos=on:bce=on:random_seed=2470284479:i=359:rtra=on:gtg=exists_top:ss=axioms_2974 on theBenchmark for (2974ds/359Mi) % 25.54/4.30 % (233435)Refutation not found, incomplete strategy % 25.54/4.30 % (233435)------------------------------ % 25.54/4.30 % (233435)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.54/4.30 % (233435)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.54/4.30 % (233435)CaDiCaL version: 2.1.3 % 25.54/4.30 % (233435)Termination reason: Refutation not found, incomplete strategy % 25.54/4.30 % (233435)Time elapsed: 0.003 s % 25.54/4.30 % (233435)Peak memory usage: 89 MB % 25.54/4.30 % (233435)Instructions burned: 2 (million) % 25.54/4.30 % (233424)------------------------------ % 25.54/4.30 % (233424)------------------------------ % 25.54/4.30 % (233426)Instruction limit reached! % 25.54/4.30 % (233426)------------------------------ % 25.54/4.30 % (233426)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.54/4.30 % (233426)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.54/4.30 % (233426)CaDiCaL version: 2.1.3 % 25.54/4.30 % (233426)Termination reason: Instruction limit % 25.54/4.30 % (233426)Termination phase: Saturation % 25.54/4.30 % (233426)Time elapsed: 0.300 s % 25.54/4.30 % (233426)Peak memory usage: 119 MB % 25.54/4.30 % (233426)Instructions burned: 387 (million) % 25.54/4.30 % (233433)------------------------------ % 25.54/4.30 % (233433)------------------------------ % 25.54/4.30 % (233437)dis+1010_1_to=lpo:sil=128000:thi=all:fde=unused:si=on:sp=reverse_arity:tha=off:random_seed=4003990:i=341:gtgl=2:rtra=on:gtg=exists_sym:ev=force:fsd=on:fsdmm=1_2973 on theBenchmark for (2973ds/341Mi) % 25.54/4.30 % (233427)Instruction limit reached! % 25.54/4.30 % (233427)------------------------------ % 25.54/4.30 % (233427)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.54/4.30 % (233427)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.54/4.30 % (233427)CaDiCaL version: 2.1.3 % 25.54/4.30 % (233427)Termination reason: Instruction limit % 25.54/4.30 % (233427)Termination phase: Saturation % 25.54/4.30 % (233427)Time elapsed: 0.327 s % 25.54/4.30 % (233427)Peak memory usage: 94 MB % 25.54/4.30 % (233427)Instructions burned: 514 (million) % 25.54/4.30 % (233438)lrs-2_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_max:tha=off:random_seed=305762348:st=1.5:i=261:sd=1:kws=precedence:rtra=on:ss=axioms_2973 on theBenchmark for (2973ds/261Mi) % 25.54/4.30 % (233437)Refutation not found, incomplete strategy % 25.54/4.30 % (233437)------------------------------ % 25.54/4.30 % (233437)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.54/4.30 % (233437)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.54/4.30 % (233437)CaDiCaL version: 2.1.3 % 25.54/4.30 % (233437)Termination reason: Refutation not found, incomplete strategy % 25.54/4.30 % (233437)Time elapsed: 0.028 s % 25.54/4.30 % (233437)Peak memory usage: 113 MB % 25.54/4.30 % (233437)Instructions burned: 6 (million) % 25.54/4.30 % (233438)Refutation not found, incomplete strategy % 25.54/4.30 % (233438)------------------------------ % 25.54/4.30 % (233438)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.54/4.30 % (233438)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.54/4.30 % (233438)CaDiCaL version: 2.1.3 % 25.54/4.30 % (233438)Termination reason: Refutation not found, incomplete strategy % 25.54/4.30 % (233438)Time elapsed: 0.038 s % 25.54/4.30 % (233438)Peak memory usage: 116 MB % 25.54/4.30 % (233438)Instructions burned: 17 (million) % 25.54/4.30 % (233440)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=1156003679:s2pl=no:i=235:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2972 on theBenchmark for (2972ds/235Mi) % 25.54/4.30 % (233442)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=3493548015:i=146:doe=on:rtra=on_2972 on theBenchmark for (2972ds/146Mi) % 25.54/4.30 % (233441)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=4142400822:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2972 on theBenchmark for (2972ds/273Mi) % 25.54/4.30 % (233435)------------------------------ % 25.54/4.30 % (233435)------------------------------ % 25.54/4.30 % (233442)Instruction limit reached! % 25.54/4.30 % (233442)------------------------------ % 25.54/4.30 % (233442)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.58/4.73 % (233442)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.58/4.73 % (233442)CaDiCaL version: 2.1.3 % 27.58/4.73 % (233442)Termination reason: Instruction limit % 27.58/4.73 % (233442)Termination phase: Saturation % 27.58/4.73 % (233442)Time elapsed: 0.051 s % 27.58/4.73 % (233442)Peak memory usage: 90 MB % 27.58/4.73 % (233442)Instructions burned: 149 (million) % 27.58/4.73 % (233445)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=3027256518:i=4428:doe=on:fsr=off:rtra=on_2971 on theBenchmark for (2971ds/4428Mi) % 27.58/4.73 % (233440)Instruction limit reached! % 27.58/4.73 % (233440)------------------------------ % 27.58/4.73 % (233440)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.58/4.73 % (233440)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.58/4.73 % (233440)CaDiCaL version: 2.1.3 % 27.58/4.73 % (233440)Termination reason: Instruction limit % 27.58/4.73 % (233440)Termination phase: Saturation % 27.58/4.73 % (233440)Time elapsed: 0.160 s % 27.58/4.73 % (233440)Peak memory usage: 116 MB % 27.58/4.73 % (233440)Instructions burned: 236 (million) % 27.58/4.73 % (233437)------------------------------ % 27.58/4.73 % (233437)------------------------------ % 27.58/4.73 % (233450)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=1777183917:i=1052:rtra=on_2970 on theBenchmark for (2970ds/1052Mi) % 27.58/4.73 % (233438)------------------------------ % 27.58/4.73 % (233438)------------------------------ % 27.58/4.73 % (233441)Instruction limit reached! % 27.58/4.73 % (233441)------------------------------ % 27.58/4.73 % (233441)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.58/4.73 % (233441)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.58/4.73 % (233441)CaDiCaL version: 2.1.3 % 27.58/4.73 % (233441)Termination reason: Instruction limit % 27.58/4.73 % (233441)Termination phase: Saturation % 27.58/4.73 % (233441)Time elapsed: 0.167 s % 27.58/4.73 % (233441)Peak memory usage: 92 MB % 27.58/4.73 % (233441)Instructions burned: 274 (million) % 27.58/4.73 % (233449)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=1016449813:avsq=on:i=276:avsqr=1,2:rtra=on_2970 on theBenchmark for (2970ds/276Mi) % 27.58/4.73 % (233452)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=2078385320:i=655:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2969 on theBenchmark for (2969ds/655Mi) % 27.58/4.73 % (233452)Refutation not found, incomplete strategy % 27.58/4.73 % (233452)------------------------------ % 27.58/4.73 % (233452)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.58/4.73 % (233452)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.58/4.73 % (233452)CaDiCaL version: 2.1.3 % 27.58/4.73 % (233452)Termination reason: Refutation not found, incomplete strategy % 27.58/4.73 % (233452)Time elapsed: 0.004 s % 27.58/4.73 % (233452)Peak memory usage: 89 MB % 27.58/4.73 % (233452)Instructions burned: 4 (million) % 27.58/4.73 % (233454)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=1749569883:st=5:i=1054:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2969 on theBenchmark for (2969ds/1054Mi) % 27.58/4.73 % (233454)Refutation not found, incomplete strategy % 27.58/4.73 % (233454)------------------------------ % 27.58/4.73 % (233454)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.58/4.73 % (233454)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.58/4.73 % (233454)CaDiCaL version: 2.1.3 % 27.58/4.73 % (233454)Termination reason: Refutation not found, incomplete strategy % 27.58/4.73 % (233454)Time elapsed: 0.003 s % 27.58/4.73 % (233454)Peak memory usage: 89 MB % 27.58/4.73 % (233454)Instructions burned: 2 (million) % 27.58/4.73 % (233457)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=2554956018:s2a=on:i=450:doe=on:nm=32:rtra=on_2969 on theBenchmark for (2969ds/450Mi) % 27.58/4.73 % (233456)lrs-1002_1_to=kbo:sas=z3:si=on:norm_ineq=on:sos=on:tha=some:random_seed=31767060:i=107:rtra=on_2969 on theBenchmark for (2969ds/107Mi) % 27.58/4.73 % (233449)Instruction limit reached! % 27.58/4.73 % (233449)------------------------------ % 27.58/4.73 % (233449)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.58/4.73 % (233449)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.14/5.12 % (233449)CaDiCaL version: 2.1.3 % 31.14/5.12 % (233449)Termination reason: Instruction limit % 31.14/5.12 % (233449)Termination phase: Saturation % 31.14/5.12 % (233449)Time elapsed: 0.155 s % 31.14/5.12 % (233449)Peak memory usage: 133 MB % 31.14/5.12 % (233449)Instructions burned: 277 (million) % 31.14/5.12 % (233456)Refutation not found, incomplete strategy % 31.14/5.12 % (233456)------------------------------ % 31.14/5.12 % (233456)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.14/5.12 % (233456)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.14/5.12 % (233456)CaDiCaL version: 2.1.3 % 31.14/5.12 % (233456)Termination reason: Refutation not found, incomplete strategy % 31.14/5.12 % (233456)Time elapsed: 0.030 s % 31.14/5.12 % (233456)Peak memory usage: 115 MB % 31.14/5.12 % (233456)Instructions burned: 8 (million) % 31.14/5.12 % (233457)Refutation not found, incomplete strategy % 31.14/5.12 % (233457)------------------------------ % 31.14/5.12 % (233457)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.14/5.12 % (233457)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.14/5.12 % (233457)CaDiCaL version: 2.1.3 % 31.14/5.12 % (233457)Termination reason: Refutation not found, incomplete strategy % 31.14/5.12 % (233457)Time elapsed: 0.054 s % 31.14/5.12 % (233457)Peak memory usage: 132 MB % 31.14/5.12 % (233457)Instructions burned: 12 (million) % 31.14/5.12 % (233450)Instruction limit reached! % 31.14/5.12 % (233450)------------------------------ % 31.14/5.12 % (233450)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.14/5.12 % (233450)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.14/5.12 % (233450)CaDiCaL version: 2.1.3 % 31.14/5.12 % (233450)Termination reason: Instruction limit % 31.14/5.12 % (233450)Termination phase: Saturation % 31.14/5.12 % (233450)Time elapsed: 0.238 s % 31.14/5.12 % (233450)Peak memory usage: 89 MB % 31.14/5.12 % (233450)Instructions burned: 1054 (million) % 31.14/5.12 % (233462)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 % 31.14/5.12 % (233462)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=937995369:i=1090:aac=none:nm=0:rtra=on:rawr=on_2967 on theBenchmark for (2967ds/1090Mi) % 31.14/5.12 % (233463)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=46628877:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2966 on theBenchmark for (2966ds/130Mi) % 31.14/5.12 % (233452)------------------------------ % 31.14/5.12 % (233452)------------------------------ % 31.14/5.12 % (233454)------------------------------ % 31.14/5.12 % (233454)------------------------------ % 31.14/5.12 % (233463)Refutation not found, incomplete strategy % 31.14/5.12 % (233463)------------------------------ % 31.14/5.12 % (233463)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.14/5.12 % (233462)Refutation not found, incomplete strategy % 31.14/5.12 % (233462)------------------------------ % 31.14/5.12 % (233462)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.14/5.12 % (233463)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.14/5.12 % (233462)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.14/5.12 % (233463)CaDiCaL version: 2.1.3 % 31.14/5.12 % (233463)Termination reason: Refutation not found, incomplete strategy % 31.14/5.12 % (233463)Time elapsed: 0.024 s % 31.14/5.12 % (233462)CaDiCaL version: 2.1.3 % 31.14/5.12 % (233463)Peak memory usage: 116 MB % 31.14/5.12 % (233463)Instructions burned: 24 (million) % 31.14/5.12 % (233462)Termination reason: Refutation not found, incomplete strategy % 31.14/5.12 % (233462)Time elapsed: 0.029 s % 31.14/5.12 % (233462)Peak memory usage: 116 MB % 31.14/5.12 % (233462)Instructions burned: 7 (million) % 31.14/5.12 % (233456)------------------------------ % 31.14/5.12 % (233456)------------------------------ % 31.14/5.12 % (233457)------------------------------ % 31.14/5.12 % (233457)------------------------------ % 31.14/5.12 % (233466)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=1540779757:i=312:kws=inv_frequency:nm=20:rtra=on_2965 on theBenchmark for (2965ds/312Mi) % 31.14/5.12 % (233463)------------------------------ % 31.14/5.12 % (233463)------------------------------ % 31.14/5.12 % (233467)ott+10_1_to=kbo:sil=64000:si=on:sp=reverse_frequency:sos=on:random_seed=2984151840:i=491:doe=on:rtra=on:gtg=position_2965 on theBenchmark for (2965ds/491Mi) % 33.53/5.68 % (233467)Refutation not found, incomplete strategy % 33.53/5.68 % (233467)------------------------------ % 33.53/5.68 % (233467)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.53/5.68 % (233467)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.53/5.68 % (233467)CaDiCaL version: 2.1.3 % 33.53/5.68 % (233467)Termination reason: Refutation not found, incomplete strategy % 33.53/5.68 % (233467)Time elapsed: 0.003 s % 33.53/5.68 % (233467)Peak memory usage: 89 MB % 33.53/5.68 % (233467)Instructions burned: 2 (million) % 33.53/5.68 % (233468)ott+1011_4:1_to=lpo:sil=64000:si=on:spb=intro:random_seed=490312335:s2a=on:i=835:s2at=2:rtra=on_2964 on theBenchmark for (2964ds/835Mi) % 33.53/5.68 % (233462)------------------------------ % 33.53/5.68 % (233462)------------------------------ % 33.53/5.68 % (233469)ott+1011_2_to=lpo:sil=128000:si=on:sos=on:random_seed=3159442411:i=307:bd=preordered:av=off:rtra=on:ev=cautious_2964 on theBenchmark for (2964ds/307Mi) % 33.53/5.68 % (233471)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=2925650686:i=776:doe=on:rtra=on_2963 on theBenchmark for (2963ds/776Mi) % 33.53/5.68 % (233466)Instruction limit reached! % 33.53/5.68 % (233466)------------------------------ % 33.53/5.68 % (233466)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.53/5.68 % (233466)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.53/5.68 % (233466)CaDiCaL version: 2.1.3 % 33.53/5.68 % (233466)Termination reason: Instruction limit % 33.53/5.68 % (233466)Termination phase: Saturation % 33.53/5.68 % (233466)Time elapsed: 0.221 s % 33.53/5.68 % (233466)Peak memory usage: 118 MB % 33.53/5.68 % (233466)Instructions burned: 313 (million) % 33.53/5.68 % (233475)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=2920361327:s2a=on:i=646:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2962 on theBenchmark for (2962ds/646Mi) % 33.53/5.68 % (233467)------------------------------ % 33.53/5.68 % (233467)------------------------------ % 33.53/5.68 % (233475)Refutation not found, incomplete strategy % 33.53/5.68 % (233475)------------------------------ % 33.53/5.68 % (233475)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.53/5.68 % (233475)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.53/5.68 % (233475)CaDiCaL version: 2.1.3 % 33.53/5.68 % (233475)Termination reason: Refutation not found, incomplete strategy % 33.53/5.68 % (233475)Time elapsed: 0.055 s % 33.53/5.68 % (233475)Peak memory usage: 133 MB % 33.53/5.68 % (233475)Instructions burned: 14 (million) % 33.53/5.68 % (233469)Instruction limit reached! % 33.53/5.68 % (233469)------------------------------ % 33.53/5.68 % (233469)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.53/5.68 % (233469)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.53/5.68 % (233469)CaDiCaL version: 2.1.3 % 33.53/5.68 % (233469)Termination reason: Instruction limit % 33.53/5.68 % (233469)Termination phase: Saturation % 33.53/5.68 % (233469)Time elapsed: 0.217 s % 33.53/5.68 % (233469)Peak memory usage: 92 MB % 33.53/5.68 % (233469)Instructions burned: 308 (million) % 33.53/5.68 % (233471)Instruction limit reached! % 33.53/5.68 % (233471)------------------------------ % 33.53/5.68 % (233471)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.53/5.68 % (233471)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.53/5.68 % (233471)CaDiCaL version: 2.1.3 % 33.53/5.68 % (233471)Termination reason: Instruction limit % 33.53/5.68 % (233471)Termination phase: Saturation % 33.53/5.68 % (233471)Time elapsed: 0.211 s % 33.53/5.68 % (233471)Peak memory usage: 121 MB % 33.53/5.68 % (233471)Instructions burned: 781 (million) % 33.53/5.68 % (233477)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=3541360999:thitd=on:cond=fast:i=784:nm=30:rtra=on:gtg=all:tac=axiom_2961 on theBenchmark for (2961ds/784Mi) % 33.53/5.68 % (233479)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=3576690328:thitd=on:s2a=on:i=1131:add=on:canc=force:bd=all:rtra=on:tac=axiom:ev=off_2961 on theBenchmark for (2961ds/1131Mi) % 33.53/5.68 % (233481)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=1893861287:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2960 on theBenchmark for (2960ds/775Mi) % 38.20/6.10 % (233480)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=1641294528:s2pl=no:i=246:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2960 on theBenchmark for (2960ds/246Mi) % 38.20/6.10 % (233468)Instruction limit reached! % 38.20/6.10 % (233468)------------------------------ % 38.20/6.10 % (233468)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 38.20/6.10 % (233468)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.20/6.10 % (233468)CaDiCaL version: 2.1.3 % 38.20/6.10 % (233468)Termination reason: Instruction limit % 38.20/6.10 % (233468)Termination phase: Saturation % 38.20/6.10 % (233468)Time elapsed: 0.460 s % 38.20/6.10 % (233468)Peak memory usage: 93 MB % 38.20/6.10 % (233468)Instructions burned: 835 (million) % 38.20/6.10 % (233475)------------------------------ % 38.20/6.10 % (233475)------------------------------ % 38.20/6.10 % (233480)Instruction limit reached! % 38.20/6.10 % (233480)------------------------------ % 38.20/6.10 % (233480)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 38.20/6.10 % (233480)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.20/6.10 % (233480)CaDiCaL version: 2.1.3 % 38.20/6.10 % (233480)Termination reason: Instruction limit % 38.20/6.10 % (233480)Termination phase: Saturation % 38.20/6.10 % (233480)Time elapsed: 0.159 s % 38.20/6.10 % (233480)Peak memory usage: 116 MB % 38.20/6.10 % (233480)Instructions burned: 247 (million) % 38.20/6.10 % (233486)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=2599852386:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2958 on theBenchmark for (2958ds/273Mi) % 38.20/6.10 % (233487)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=2883556208:i=102:nm=16:rtra=on_2958 on theBenchmark for (2958ds/102Mi) % 38.20/6.10 % (233481)Instruction limit reached! % 38.20/6.10 % (233481)------------------------------ % 38.20/6.10 % (233481)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 38.20/6.10 % (233481)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.20/6.10 % (233481)CaDiCaL version: 2.1.3 % 38.20/6.10 % (233481)Termination reason: Instruction limit % 38.20/6.10 % (233481)Termination phase: Saturation % 38.20/6.10 % (233481)Time elapsed: 0.276 s % 38.20/6.10 % (233481)Peak memory usage: 96 MB % 38.20/6.10 % (233481)Instructions burned: 776 (million) % 38.20/6.10 % (233487)Instruction limit reached! % 38.20/6.10 % (233487)------------------------------ % 38.20/6.10 % (233487)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 38.20/6.10 % (233487)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.20/6.10 % (233487)CaDiCaL version: 2.1.3 % 38.20/6.10 % (233487)Termination reason: Instruction limit % 38.20/6.10 % (233487)Termination phase: Saturation % 38.20/6.10 % (233487)Time elapsed: 0.051 s % 38.20/6.10 % (233487)Peak memory usage: 88 MB % 38.20/6.10 % (233487)Instructions burned: 103 (million) % 38.20/6.10 % (233477)Instruction limit reached! % 38.20/6.10 % (233477)------------------------------ % 38.20/6.10 % (233477)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 38.20/6.10 % (233477)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.20/6.10 % (233477)CaDiCaL version: 2.1.3 % 38.20/6.10 % (233477)Termination reason: Instruction limit % 38.20/6.10 % (233477)Termination phase: Saturation % 38.20/6.10 % (233477)Time elapsed: 0.405 s % 38.20/6.10 % (233477)Peak memory usage: 120 MB % 38.20/6.10 % (233477)Instructions burned: 785 (million) % 38.20/6.10 % (233488)lrs+10_1_to=lpo:sil=128000:si=on:bsr=unit_only:tha=off:random_seed=512296577:avsq=on:s2a=on:i=1094:s2at=5:avsqr=4463,131072:rtra=on_2957 on theBenchmark for (2957ds/1094Mi) % 38.20/6.10 % (233488)Refutation not found, incomplete strategy % 38.20/6.10 % (233488)------------------------------ % 38.20/6.10 % (233488)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 38.20/6.10 % (233488)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.20/6.10 % (233488)CaDiCaL version: 2.1.3 % 38.20/6.10 % (233488)Termination reason: Refutation not found, incomplete strategy % 38.20/6.10 % (233488)Time elapsed: 0.002 s % 38.20/6.10 % (233488)Peak memory usage: 88 MB % 38.20/6.10 % (233491)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=905733543:i=6400:doe=on:fsr=off:rtra=on_2956 on theBenchmark for (2956ds/6400Mi) % 47.05/7.31 % (233486)Instruction limit reached! % 47.05/7.31 % (233486)------------------------------ % 47.05/7.31 % (233486)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 47.05/7.31 % (233486)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.05/7.31 % (233486)CaDiCaL version: 2.1.3 % 47.05/7.31 % (233486)Termination reason: Instruction limit % 47.05/7.31 % (233486)Termination phase: Saturation % 47.05/7.31 % (233486)Time elapsed: 0.161 s % 47.05/7.31 % (233486)Peak memory usage: 92 MB % 47.05/7.31 % (233486)Instructions burned: 275 (million) % 47.05/7.31 % (233492)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=1327303056:i=868:doe=on:nm=0:rtra=on:gtg=exists_sym_2956 on theBenchmark for (2956ds/868Mi) % 47.05/7.31 % (233493)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=3150407719:i=1846:canc=cautious:fsr=off:rtra=on_2956 on theBenchmark for (2956ds/1846Mi) % 47.05/7.31 % (233492)Refutation not found, incomplete strategy % 47.05/7.31 % (233492)------------------------------ % 47.05/7.31 % (233492)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 47.05/7.31 % (233492)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.05/7.31 % (233492)CaDiCaL version: 2.1.3 % 47.05/7.31 % (233492)Termination reason: Refutation not found, incomplete strategy % 47.05/7.31 % (233492)Time elapsed: 0.052 s % 47.05/7.31 % (233492)Peak memory usage: 116 MB % 47.05/7.31 % (233492)Instructions burned: 40 (million) % 47.05/7.31 % (233496)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=189338111:s2a=on:i=36816:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2955 on theBenchmark for (2955ds/36816Mi) % 47.05/7.31 % (233496)Refutation not found, incomplete strategy % 47.05/7.31 % (233496)------------------------------ % 47.05/7.31 % (233496)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 47.05/7.31 % (233496)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.05/7.31 % (233496)CaDiCaL version: 2.1.3 % 47.05/7.31 % (233496)Termination reason: Refutation not found, incomplete strategy % 47.05/7.31 % (233496)Time elapsed: 0.002 s % 47.05/7.31 % (233496)Peak memory usage: 88 MB % 47.05/7.31 % (233496)Instructions burned: 1 (million) % 47.05/7.31 % (233488)------------------------------ % 47.05/7.31 % (233488)------------------------------ % 47.05/7.31 % (233479)Instruction limit reached! % 47.05/7.31 % (233479)------------------------------ % 47.05/7.31 % (233479)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 47.05/7.31 % (233479)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.05/7.31 % (233479)CaDiCaL version: 2.1.3 % 47.05/7.31 % (233479)Termination reason: Instruction limit % 47.05/7.31 % (233479)Termination phase: Saturation % 47.05/7.31 % (233479)Time elapsed: 0.720 s % 47.05/7.31 % (233479)Peak memory usage: 124 MB % 47.05/7.31 % (233479)Instructions burned: 1131 (million) % 47.05/7.31 % (233492)------------------------------ % 47.05/7.31 % (233492)------------------------------ % 47.05/7.31 % (233500)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=1731061088:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2953 on theBenchmark for (2953ds/273Mi) % 47.05/7.31 % (233496)------------------------------ % 47.05/7.31 % (233496)------------------------------ % 47.05/7.31 % (233501)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=4047705099:i=863:doe=on:nm=0:rtra=on:gtg=exists_sym_2952 on theBenchmark for (2952ds/863Mi) % 47.05/7.31 % (233502)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=1947696831:i=5811:kws=precedence:nm=0:rtra=on_2951 on theBenchmark for (2951ds/5811Mi) % 47.05/7.31 % (233501)Refutation not found, incomplete strategy % 47.05/7.31 % (233501)------------------------------ % 47.05/7.31 % (233501)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 47.05/7.31 % (233501)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.05/7.31 % (233501)CaDiCaL version: 2.1.3 % 47.05/7.31 % (233501)Termination reason: Refutation not found, incomplete strategy % 47.05/7.31 % (233501)Time elapsed: 0.052 s % 47.05/7.31 % (233501)Peak memory usage: 116 MB % 47.05/7.31 % (233501)Instructions burned: 39 (million) % 47.05/7.31 % (233500)Instruction limit reached! % 57.84/9.09 % (233500)------------------------------ % 57.84/9.09 % (233500)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 57.84/9.09 % (233500)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 57.84/9.09 % (233500)CaDiCaL version: 2.1.3 % 57.84/9.09 % (233500)Termination reason: Instruction limit % 57.84/9.09 % (233500)Termination phase: Saturation % 57.84/9.09 % (233500)Time elapsed: 0.177 s % 57.84/9.09 % (233500)Peak memory usage: 91 MB % 57.84/9.09 % (233500)Instructions burned: 274 (million) % 57.84/9.09 % (233502)Refutation not found, incomplete strategy % 57.84/9.09 % (233502)------------------------------ % 57.84/9.09 % (233502)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 57.84/9.09 % (233502)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 57.84/9.09 % (233502)CaDiCaL version: 2.1.3 % 57.84/9.09 % (233502)Termination reason: Refutation not found, incomplete strategy % 57.84/9.09 % (233502)Time elapsed: 0.052 s % 57.84/9.09 % (233502)Peak memory usage: 116 MB % 57.84/9.09 % (233502)Instructions burned: 41 (million) % 57.84/9.09 % (233504)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=2772232120:i=2216:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2951 on theBenchmark for (2951ds/2216Mi) % 57.84/9.09 % (233507)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=134653025:i=801:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2950 on theBenchmark for (2950ds/801Mi) % 57.84/9.09 % (233507)Refutation not found, incomplete strategy % 57.84/9.09 % (233507)------------------------------ % 57.84/9.09 % (233507)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 57.84/9.09 % (233507)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 57.84/9.09 % (233507)CaDiCaL version: 2.1.3 % 57.84/9.09 % (233507)Termination reason: Refutation not found, incomplete strategy % 57.84/9.09 % (233507)Time elapsed: 0.004 s % 57.84/9.09 % (233507)Peak memory usage: 89 MB % 57.84/9.09 % (233507)Instructions burned: 4 (million) % 57.84/9.09 % (233501)------------------------------ % 57.84/9.09 % (233501)------------------------------ % 57.84/9.09 % (233445)Instruction limit reached! % 57.84/9.09 % (233445)------------------------------ % 60.79/9.53 % (233445)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 60.79/9.53 % (233445)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.79/9.53 % (233445)CaDiCaL version: 2.1.3 % 60.79/9.53 % (233445)Termination reason: Instruction limit % 60.79/9.53 % (233445)Termination phase: Saturation % 60.79/9.53 % (233445)Time elapsed: 2.264 s % 60.79/9.53 % (233445)Peak memory usage: 106 MB % 60.79/9.53 % (233445)Instructions burned: 4429 (million) % 60.79/9.53 % (233502)------------------------------ % 60.79/9.53 % (233502)------------------------------ % 60.79/9.53 % (233493)Instruction limit reached! % 60.79/9.53 % (233493)------------------------------ % 60.79/9.53 % (233493)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 60.79/9.53 % (233493)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.79/9.53 % (233493)CaDiCaL version: 2.1.3 % 60.79/9.53 % (233493)Termination reason: Instruction limit % 60.79/9.53 % (233493)Termination phase: Saturation % 60.79/9.53 % (233493)Time elapsed: 0.775 s % 60.79/9.53 % (233493)Peak memory usage: 99 MB % 60.79/9.53 % (233493)Instructions burned: 1847 (million) % 60.79/9.53 % (233510)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=3201252646:st=5:i=1026:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2947 on theBenchmark for (2947ds/1026Mi) % 60.79/9.53 % (233510)Refutation not found, incomplete strategy % 60.79/9.53 % (233510)------------------------------ % 60.79/9.53 % (233510)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 60.79/9.53 % (233510)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.79/9.53 % (233510)CaDiCaL version: 2.1.3 % 60.79/9.53 % (233510)Termination reason: Refutation not found, incomplete strategy % 60.79/9.53 % (233510)Time elapsed: 0.003 s % 60.79/9.53 % (233510)Peak memory usage: 89 MB % 60.79/9.53 % (233510)Instructions burned: 2 (million) % 60.79/9.53 % (233511)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=2208731075:i=3509:rtra=on_2947 on theBenchmark for (2947ds/3509Mi) % 60.79/9.53 % (233512)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=3207816825:st=2:i=2127:sd=12:ep=R:rtra=on:ss=axioms_2947 on theBenchmark for (2947ds/2127Mi) % 80.28/12.27 % (233507)------------------------------ % 80.28/12.27 % (233507)------------------------------ % 80.28/12.27 % (233513)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=13233456:i=1959:rtra=on:fsd=on:proc=on_2946 on theBenchmark for (2946ds/1959Mi) % 80.28/12.27 % (233513)Refutation not found, incomplete strategy % 80.28/12.27 % (233513)------------------------------ % 80.28/12.27 % (233513)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 80.28/12.27 % (233513)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 80.28/12.27 % (233513)CaDiCaL version: 2.1.3 % 80.28/12.27 % (233513)Termination reason: Refutation not found, incomplete strategy % 80.28/12.27 % (233513)Time elapsed: 0.030 s % 80.28/12.27 % (233513)Peak memory usage: 116 MB % 80.28/12.27 % (233513)Instructions burned: 7 (million) % 80.28/12.27 % (233510)------------------------------ % 80.28/12.27 % (233510)------------------------------ % 80.28/12.27 % (233517)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=635723478:s2a=on:i=3553:nm=0:rtra=on_2945 on theBenchmark for (2945ds/3553Mi) % 80.28/12.27 % (233513)------------------------------ % 80.28/12.27 % (233513)------------------------------ % 80.28/12.27 % (233519)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=738325165:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2943 on theBenchmark for (2943ds/3201Mi) % 80.28/12.27 % (233521)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=3853649751:thitd=on:cond=on:i=4093:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2942 on theBenchmark for (2942ds/4093Mi) % 80.28/12.27 % (233491)Instruction limit reached! % 80.28/12.27 % (233491)------------------------------ % 80.28/12.27 % (233491)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 80.28/12.27 % (233491)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 80.28/12.27 % (233491)CaDiCaL version: 2.1.3 % 80.28/12.27 % (233491)Termination reason: Instruction limit % 80.28/12.27 % (233491)Termination phase: Saturation % 80.28/12.27 % (233491)Time elapsed: 1.731 s % 80.28/12.27 % (233491)Peak memory usage: 115 MB % 80.28/12.27 % (233491)Instructions burned: 6403 (million) % 80.28/12.27 % (233504)Instruction limit reached! % 80.28/12.27 % (233504)------------------------------ % 80.28/12.27 % (233504)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 80.28/12.27 % (233504)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 80.28/12.27 % (233504)CaDiCaL version: 2.1.3 % 80.28/12.27 % (233504)Termination reason: Instruction limit % 80.28/12.27 % (233504)Termination phase: Saturation % 80.28/12.27 % (233504)Time elapsed: 1.185 s % 80.28/12.27 % (233504)Peak memory usage: 131 MB % 80.28/12.27 % (233504)Instructions burned: 2216 (million) % 80.28/12.27 % (233524)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=1255342915:cond=fast:i=21173:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2938 on theBenchmark for (2938ds/21173Mi) % 80.28/12.27 % (233525)lrs+11_1_to=lpo:thi=all:sas=z3:si=on:fd=off:sac=on:slsq=on:random_seed=4203583503:avsq=on:i=10544:avsqr=17,4:canc=force:rtra=on:gtg=exists_top:er=filter_2937 on theBenchmark for (2937ds/10544Mi) % 80.28/12.27 % (233512)Instruction limit reached! % 80.28/12.27 % (233512)------------------------------ % 80.28/12.27 % (233512)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 80.28/12.27 % (233512)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 80.28/12.27 % (233512)CaDiCaL version: 2.1.3 % 80.28/12.27 % (233512)Termination reason: Instruction limit % 80.28/12.27 % (233512)Termination phase: Saturation % 80.28/12.27 % (233512)Time elapsed: 1.010 s % 80.28/12.27 % (233512)Peak memory usage: 101 MB % 80.28/12.27 % (233512)Instructions burned: 2128 (million) % 80.28/12.27 % (233528)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=4057067988:avsq=on:i=1262:avsqr=1,16:rtra=on:rawr=on_2935 on theBenchmark for (2935ds/1262Mi) % 80.28/12.27 % (233528)Refutation not found, incomplete strategy % 80.28/12.27 % (233528)------------------------------ % 80.28/12.27 % (233528)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 80.28/12.27 % (233528)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 80.28/12.27 % (233528)CaDiCaL version: 2.1.3 % 80.28/12.27 % (233528)Termination reason: Refutation not found, incomplete strategy % 95.25/14.33 % (233528)Time elapsed: 0.029 s % 95.25/14.33 % (233528)Peak memory usage: 116 MB % 95.25/14.33 % (233528)Instructions burned: 8 (million) % 95.25/14.33 % (233519)Refutation not found, incomplete strategy % 95.25/14.33 % (233519)------------------------------ % 95.25/14.33 % (233519)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 95.25/14.33 % (233519)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 95.25/14.33 % (233519)CaDiCaL version: 2.1.3 % 95.25/14.33 % (233519)Termination reason: Refutation not found, incomplete strategy % 95.25/14.33 % (233519)Time elapsed: 0.929 s % 95.25/14.33 % (233519)Peak memory usage: 95 MB % 95.25/14.33 % (233519)Instructions burned: 2168 (million) % 95.25/14.33 % (233519)------------------------------ % 95.25/14.33 % (233519)------------------------------ % 95.25/14.33 % (233528)------------------------------ % 95.25/14.33 % (233528)------------------------------ % 95.25/14.33 % (233511)Instruction limit reached! % 95.25/14.33 % (233511)------------------------------ % 95.25/14.33 % (233511)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 95.25/14.33 % (233511)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 95.25/14.33 % (233511)CaDiCaL version: 2.1.3 % 95.25/14.33 % (233511)Termination reason: Instruction limit % 95.25/14.33 % (233511)Termination phase: Saturation % 95.25/14.33 % (233511)Time elapsed: 2.398 s % 95.25/14.33 % (233511)Peak memory usage: 106 MB % 95.25/14.33 % (233511)Instructions burned: 3510 (million) % 95.25/14.33 % (233530)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=314365490:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2927 on theBenchmark for (2927ds/775Mi) % 95.25/14.33 % (233531)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=206819392:i=270:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2927 on theBenchmark for (2927ds/270Mi) % 95.25/14.33 % (233532)ott+10_128_isp=bottom:to=lpo:sil=128000:si=on:urr=on:uwa=alasca_main:sac=on:slsq=on:random_seed=2128546918:i=17165:aac=none:doe=on:rtra=on:gtg=exists_all_2922 on theBenchmark for (2922ds/17165Mi) % 95.25/14.33 % (233531)Instruction limit reached! % 95.25/14.33 % (233531)------------------------------ % 95.25/14.33 % (233531)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 95.25/14.33 % (233531)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 95.25/14.33 % (233531)CaDiCaL version: 2.1.3 % 95.25/14.33 % (233531)Termination reason: Instruction limit % 95.25/14.33 % (233531)Termination phase: Saturation % 95.25/14.33 % (233531)Time elapsed: 0.165 s % 95.25/14.33 % (233531)Peak memory usage: 91 MB % 95.25/14.33 % (233531)Instructions burned: 271 (million) % 95.25/14.33 % (233517)Instruction limit reached! % 95.25/14.33 % (233517)------------------------------ % 95.25/14.33 % (233517)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 95.25/14.33 % (233517)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 95.25/14.33 % (233517)CaDiCaL version: 2.1.3 % 95.25/14.33 % (233517)Termination reason: Instruction limit % 95.25/14.33 % (233517)Termination phase: Saturation % 95.25/14.33 % (233517)Time elapsed: 2.513 s % 95.25/14.33 % (233517)Peak memory usage: 105 MB % 95.25/14.33 % (233517)Instructions burned: 3553 (million) % 95.25/14.33 % (233521)Instruction limit reached! % 95.25/14.33 % (233521)------------------------------ % 95.25/14.33 % (233521)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 95.25/14.33 % (233521)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 95.25/14.33 % (233521)CaDiCaL version: 2.1.3 % 95.25/14.33 % (233521)Termination reason: Instruction limit % 95.25/14.33 % (233521)Termination phase: Saturation % 95.25/14.33 % (233521)Time elapsed: 2.287 s % 95.25/14.33 % (233521)Peak memory usage: 151 MB % 95.25/14.33 % (233521)Instructions burned: 4093 (million) % 95.25/14.33 % (233536)lrs+2_10_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_main:tha=some:random_seed=1775273750:s2a=on:i=13094:s2at=-1:rtra=on_2919 on theBenchmark for (2919ds/13094Mi) % 95.25/14.33 % (233537)lrs+10_1_to=lpo:sil=128000:si=on:sp=occurrence:random_seed=911647308:st=2:i=12633:rtra=on:ss=axioms_2918 on theBenchmark for (2918ds/12633Mi) % 95.25/14.33 % (233538)dis+1011_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_frequency:lsd=20:nwc=3:random_seed=30293792:i=1783:rtra=on:gtg=position_2918 on theBenchmark for (2918ds/1783Mi) % 95.25/14.33 % (233530)Instruction limit reached! % 95.25/14.33 % (233530)------------------------------ % 114.89/17.08 % (233530)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 114.89/17.08 % (233530)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.89/17.08 % (233530)CaDiCaL version: 2.1.3 % 114.89/17.08 % (233530)Termination reason: Instruction limit % 114.89/17.08 % (233530)Termination phase: Saturation % 114.89/17.08 % (233530)Time elapsed: 0.514 s % 114.89/17.08 % (233530)Peak memory usage: 96 MB % 114.89/17.08 % (233530)Instructions burned: 776 (million) % 114.89/17.08 % (233542)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=1347538989:i=5451:aac=none:doe=on:nm=0:rtra=on:amm=off:gtg=position_2915 on theBenchmark for (2915ds/5451Mi) % 114.89/17.08 % (233538)Instruction limit reached! % 114.89/17.08 % (233538)------------------------------ % 114.89/17.08 % (233538)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 114.89/17.08 % (233538)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.89/17.08 % (233538)CaDiCaL version: 2.1.3 % 114.89/17.08 % (233538)Termination reason: Instruction limit % 114.89/17.08 % (233538)Termination phase: Saturation % 114.89/17.08 % (233538)Time elapsed: 1.018 s % 114.89/17.08 % (233538)Peak memory usage: 122 MB % 114.89/17.08 % (233538)Instructions burned: 1783 (million) % 114.89/17.08 % (233544)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=1559250154:i=4975:doe=on:nm=0:rtra=on:gtg=exists_sym_2906 on theBenchmark for (2906ds/4975Mi) % 114.89/17.08 % (233544)Refutation not found, incomplete strategy % 114.89/17.08 % (233544)------------------------------ % 114.89/17.08 % (233544)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 114.89/17.08 % (233544)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.89/17.08 % (233544)CaDiCaL version: 2.1.3 % 114.89/17.08 % (233544)Termination reason: Refutation not found, incomplete strategy % 114.89/17.08 % (233544)Time elapsed: 0.051 s % 114.89/17.08 % (233544)Peak memory usage: 117 MB % 114.89/17.08 % (233544)Instructions burned: 39 (million) % 114.89/17.08 % (233544)------------------------------ % 114.89/17.08 % (233544)------------------------------ % 114.89/17.08 % (233546)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=2690861562:i=2076:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2901 on theBenchmark for (2901ds/2076Mi) % 114.89/17.08 % (233524)Instruction limit reached! % 114.89/17.08 % (233524)------------------------------ % 114.89/17.08 % (233524)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 114.89/17.08 % (233524)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.89/17.08 % (233524)CaDiCaL version: 2.1.3 % 114.89/17.08 % (233524)Termination reason: Instruction limit % 114.89/17.08 % (233524)Termination phase: Saturation % 114.89/17.08 % (233524)Time elapsed: 4.577 s % 114.89/17.08 % (233524)Peak memory usage: 139 MB % 114.89/17.08 % (233524)Instructions burned: 21179 (million) % 114.89/17.08 % (233548)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=324541221:i=5145:rtra=on_2891 on theBenchmark for (2891ds/5145Mi) % 114.89/17.08 % (233546)Instruction limit reached! % 114.89/17.08 % (233546)------------------------------ % 114.89/17.08 % (233546)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 114.89/17.08 % (233546)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.89/17.08 % (233546)CaDiCaL version: 2.1.3 % 114.89/17.08 % (233546)Termination reason: Instruction limit % 114.89/17.08 % (233546)Termination phase: Saturation % 114.89/17.08 % (233546)Time elapsed: 1.121 s % 114.89/17.08 % (233546)Peak memory usage: 124 MB % 114.89/17.08 % (233546)Instructions burned: 2076 (million) % 114.89/17.08 % (233550)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=1981239381:i=3509:rtra=on_2888 on theBenchmark for (2888ds/3509Mi) % 114.89/17.08 % (233542)Instruction limit reached! % 114.89/17.08 % (233542)------------------------------ % 114.89/17.08 % (233542)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 114.89/17.08 % (233542)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.89/17.08 % (233542)CaDiCaL version: 2.1.3 % 114.89/17.08 % (233542)Termination reason: Instruction limit % 114.89/17.08 % (233542)Termination phase: Saturation % 114.89/17.08 % (233542)Time elapsed: 2.843 s % 114.89/17.08 % (233542)Peak memory usage: 128 MB % 114.89/17.08 % (233542)Instructions burned: 5452 (million) % 114.89/17.08 % (233552)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=3676780960:st=2:i=13800:sd=12:ep=R:rtra=on:ss=axioms_2885 on theBenchmark for (2885ds/13800Mi) % 136.94/20.18 % (233548)Instruction limit reached! % 136.94/20.18 % (233548)------------------------------ % 136.94/20.18 % (233548)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 136.94/20.18 % (233548)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.94/20.18 % (233548)CaDiCaL version: 2.1.3 % 136.94/20.18 % (233548)Termination reason: Instruction limit % 136.94/20.18 % (233548)Termination phase: Saturation % 136.94/20.18 % (233548)Time elapsed: 1.052 s % 136.94/20.18 % (233548)Peak memory usage: 90 MB % 136.94/20.18 % (233548)Instructions burned: 5149 (million) % 136.94/20.18 % (233554)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=2699884951:i=1412:rtra=on:fsd=on:proc=on_2879 on theBenchmark for (2879ds/1412Mi) % 136.94/20.18 % (233554)Refutation not found, incomplete strategy % 136.94/20.18 % (233554)------------------------------ % 136.94/20.18 % (233554)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 136.94/20.18 % (233554)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.94/20.18 % (233554)CaDiCaL version: 2.1.3 % 136.94/20.18 % (233554)Termination reason: Refutation not found, incomplete strategy % 136.94/20.18 % (233554)Time elapsed: 0.018 s % 136.94/20.18 % (233554)Peak memory usage: 116 MB % 136.94/20.18 % (233554)Instructions burned: 8 (million) % 136.94/20.18 % (233554)------------------------------ % 136.94/20.18 % (233554)------------------------------ % 136.94/20.18 % (233556)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 % 136.94/20.18 % (233556)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=3799138694:i=11747:aac=none:nm=0:rtra=on:rawr=on_2876 on theBenchmark for (2876ds/11747Mi) % 136.94/20.18 % (233556)Refutation not found, incomplete strategy % 136.94/20.18 % (233556)------------------------------ % 136.94/20.18 % (233556)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 136.94/20.18 % (233556)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.94/20.18 % (233556)CaDiCaL version: 2.1.3 % 136.94/20.18 % (233556)Termination reason: Refutation not found, incomplete strategy % 136.94/20.18 % (233556)Time elapsed: 0.018 s % 136.94/20.18 % (233556)Peak memory usage: 116 MB % 136.94/20.18 % (233556)Instructions burned: 7 (million) % 136.94/20.18 % (233556)------------------------------ % 136.94/20.18 % (233556)------------------------------ % 136.94/20.18 % (233558)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=768686764:s2a=on:i=3553:nm=0:rtra=on_2873 on theBenchmark for (2873ds/3553Mi) % 136.94/20.18 % (233536)Instruction limit reached! % 136.94/20.18 % (233536)------------------------------ % 136.94/20.18 % (233536)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 136.94/20.18 % (233536)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.94/20.18 % (233536)CaDiCaL version: 2.1.3 % 136.94/20.18 % (233536)Termination reason: Instruction limit % 136.94/20.18 % (233536)Termination phase: Saturation % 136.94/20.18 % (233536)Time elapsed: 4.875 s % 136.94/20.18 % (233536)Peak memory usage: 91 MB % 136.94/20.18 % (233536)Instructions burned: 13096 (million) % 136.94/20.18 % (233562)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=31957072:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2868 on theBenchmark for (2868ds/3201Mi) % 136.94/20.18 % (233525)Instruction limit reached! % 136.94/20.18 % (233525)------------------------------ % 136.94/20.18 % (233525)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 136.94/20.18 % (233525)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.94/20.18 % (233525)CaDiCaL version: 2.1.3 % 136.94/20.18 % (233525)Termination reason: Instruction limit % 136.94/20.18 % (233525)Termination phase: Saturation % 136.94/20.18 % (233525)Time elapsed: 6.903 s % 136.94/20.18 % (233525)Peak memory usage: 194 MB % 136.94/20.18 % (233525)Instructions burned: 10545 (million) % 136.94/20.18 % (233625)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=2522771314:thitd=on:cond=on:i=4081:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2867 on theBenchmark for (2867ds/4081Mi) % 136.94/20.18 % (233550)Instruction limit reached! % 175.37/25.64 % (233550)------------------------------ % 175.37/25.64 % (233550)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 175.37/25.64 % (233550)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 175.37/25.64 % (233550)CaDiCaL version: 2.1.3 % 175.37/25.64 % (233550)Termination reason: Instruction limit % 175.37/25.64 % (233550)Termination phase: Saturation % 175.37/25.64 % (233550)Time elapsed: 2.361 s % 175.37/25.64 % (233550)Peak memory usage: 107 MB % 175.37/25.64 % (233550)Instructions burned: 3510 (million) % 175.37/25.64 % (233680)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=546111254:cond=fast:i=20260:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2863 on theBenchmark for (2863ds/20260Mi) % 175.37/25.64 % (233562)Refutation not found, incomplete strategy % 175.37/25.64 % (233562)------------------------------ % 175.37/25.64 % (233562)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 175.37/25.64 % (233562)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 175.37/25.64 % (233562)CaDiCaL version: 2.1.3 % 175.37/25.64 % (233562)Termination reason: Refutation not found, incomplete strategy % 175.37/25.64 % (233562)Time elapsed: 0.831 s % 175.37/25.64 % (233562)Peak memory usage: 95 MB % 175.37/25.64 % (233562)Instructions burned: 1933 (million) % 175.37/25.64 % (233558)Instruction limit reached! % 175.37/25.64 % (233558)------------------------------ % 175.37/25.64 % (233558)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 175.37/25.64 % (233558)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 175.37/25.64 % (233558)CaDiCaL version: 2.1.3 % 175.37/25.64 % (233558)Termination reason: Instruction limit % 175.37/25.64 % (233558)Termination phase: Saturation % 175.37/25.64 % (233558)Time elapsed: 1.400 s % 175.37/25.64 % (233558)Peak memory usage: 107 MB % 175.37/25.64 % (233558)Instructions burned: 3553 (million) % 175.37/25.64 % (233808)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=2881064791:s2a=on:i=58627:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2858 on theBenchmark for (2858ds/58627Mi) % 175.37/25.64 % (233808)Refutation not found, incomplete strategy % 175.37/25.64 % (233808)------------------------------ % 175.37/25.64 % (233808)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 175.37/25.64 % (233808)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 175.37/25.64 % (233808)CaDiCaL version: 2.1.3 % 175.37/25.64 % (233808)Termination reason: Refutation not found, incomplete strategy % 175.37/25.64 % (233808)Time elapsed: 0.001 s % 175.37/25.64 % (233808)Peak memory usage: 88 MB % 175.37/25.64 % (233808)Instructions burned: 1 (million) % 175.37/25.64 % (233562)------------------------------ % 175.37/25.64 % (233562)------------------------------ % 175.37/25.64 % (233808)------------------------------ % 175.37/25.64 % (233808)------------------------------ % 175.37/25.64 % (233814)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=2225973921:avsq=on:i=6258:avsqr=1,16:rtra=on:rawr=on_2856 on theBenchmark for (2856ds/6258Mi) % 175.37/25.64 % (233814)Refutation not found, incomplete strategy % 175.37/25.64 % (233814)------------------------------ % 175.37/25.64 % (233814)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 175.37/25.64 % (233814)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 175.37/25.64 % (233814)CaDiCaL version: 2.1.3 % 175.37/25.64 % (233814)Termination reason: Refutation not found, incomplete strategy % 175.37/25.64 % (233814)Time elapsed: 0.030 s % 175.37/25.64 % (233814)Peak memory usage: 116 MB % 175.37/25.64 % (233814)Instructions burned: 8 (million) % 175.37/25.64 % (233815)ott+10_128_isp=bottom:to=lpo:sil=128000:si=on:urr=on:uwa=alasca_main:sac=on:slsq=on:random_seed=3382861375:i=34001:aac=none:doe=on:rtra=on:gtg=exists_all_2855 on theBenchmark for (2855ds/34001Mi) % 175.37/25.64 % (233814)------------------------------ % 175.37/25.64 % (233814)------------------------------ % 175.37/25.64 % (233826)lrs+2_10_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_main:tha=some:random_seed=1225348984:s2a=on:i=71622:s2at=-1:rtra=on_2852 on theBenchmark for (2852ds/71622Mi) % 175.37/25.64 % (233625)Instruction limit reached! % 175.37/25.64 % (233625)------------------------------ % 175.37/25.64 % (233625)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 175.37/25.64 % (233625)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 175.37/25.64 % (233625)CaDiCaL version: 2.1.3 % 175.37/25.64 % (233625)Termination reason: Instruction limit % 204.07/29.71 % (233625)Termination phase: Saturation % 204.07/29.71 % (233625)Time elapsed: 2.962 s % 204.07/29.71 % (233625)Peak memory usage: 152 MB % 204.07/29.71 % (233625)Instructions burned: 4081 (million) % 204.07/29.71 % (233894)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=4073810087:i=24001:kws=precedence:nm=0:rtra=on_2835 on theBenchmark for (2835ds/24001Mi) % 204.07/29.71 % (233894)Refutation not found, incomplete strategy % 204.07/29.71 % (233894)------------------------------ % 204.07/29.71 % (233894)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 204.07/29.71 % (233894)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 204.07/29.71 % (233894)CaDiCaL version: 2.1.3 % 204.07/29.71 % (233894)Termination reason: Refutation not found, incomplete strategy % 204.07/29.71 % (233894)Time elapsed: 0.073 s % 204.07/29.71 % (233894)Peak memory usage: 116 MB % 204.07/29.71 % (233894)Instructions burned: 36 (million) % 204.07/29.71 % (233894)------------------------------ % 204.07/29.71 % (233894)------------------------------ % 204.07/29.71 % (233537)Instruction limit reached! % 204.07/29.71 % (233537)------------------------------ % 204.07/29.71 % (233537)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 204.07/29.71 % (233537)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 204.07/29.71 % (233537)CaDiCaL version: 2.1.3 % 204.07/29.71 % (233537)Termination reason: Instruction limit % 204.07/29.71 % (233537)Termination phase: Saturation % 204.07/29.71 % (233537)Time elapsed: 9.192 s % 204.07/29.71 % (233537)Peak memory usage: 133 MB % 204.07/29.71 % (233537)Instructions burned: 12633 (million) % 204.07/29.71 % (233917)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=143188537:i=2076:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2828 on theBenchmark for (2828ds/2076Mi) % 204.07/29.71 % (233929)dis+21_20_to=lakbo:si=on:alasca=on:sp=const_max:uwa=alasca_main:sac=on:random_seed=4058985362:s2a=on:i=83971:s2at=4:bd=all:ins=1:rtra=on_2825 on theBenchmark for (2825ds/83971Mi) % 204.07/29.71 % (233532)Instruction limit reached! % 204.07/29.71 % (233532)------------------------------ % 204.07/29.71 % (233532)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 204.07/29.71 % (233532)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 204.07/29.71 % (233532)CaDiCaL version: 2.1.3 % 204.07/29.71 % (233532)Termination reason: Instruction limit % 204.07/29.71 % (233532)Termination phase: Saturation % 204.07/29.71 % (233532)Time elapsed: 10.454 s % 204.07/29.71 % (233532)Peak memory usage: 157 MB % 204.07/29.71 % (233532)Instructions burned: 17166 (million) % 204.07/29.71 % (233952)lrs+1011_5:1_to=lpo:sil=128000:sas=z3:si=on:norm_ineq=on:tha=some:random_seed=3124253591:i=83944:rtra=on_2815 on theBenchmark for (2815ds/83944Mi) % 204.07/29.71 % (233952)Refutation not found, incomplete strategy % 204.07/29.71 % (233952)------------------------------ % 204.07/29.71 % (233952)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 204.07/29.71 % (233952)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 204.07/29.71 % (233952)CaDiCaL version: 2.1.3 % 204.07/29.71 % (233952)Termination reason: Refutation not found, incomplete strategy % 204.07/29.71 % (233952)Time elapsed: 0.044 s % 204.07/29.71 % (233952)Peak memory usage: 116 MB % 204.07/29.71 % (233952)Instructions burned: 8 (million) % 204.07/29.71 % (233952)------------------------------ % 204.07/29.71 % (233952)------------------------------ % 204.07/29.71 % (233917)Instruction limit reached! % 204.07/29.71 % (233917)------------------------------ % 204.07/29.71 % (233917)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 204.07/29.71 % (233917)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 204.07/29.71 % (233917)CaDiCaL version: 2.1.3 % 204.07/29.71 % (233917)Termination reason: Instruction limit % 204.07/29.71 % (233917)Termination phase: Saturation % 204.07/29.71 % (233917)Time elapsed: 1.776 s % 204.07/29.71 % (233917)Peak memory usage: 125 MB % 204.07/29.71 % (233917)Instructions burned: 2076 (million) % 204.07/29.71 % (233968)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=3244215663:i=9201:rtra=on_2808 on theBenchmark for (2808ds/9201Mi) % 204.07/29.71 % (233974)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 % 204.07/29.71 % (233974)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=2049490216:i=6806:aac=none:nm=0:rtra=on:rawr=on_2807 on theBenchmark for (2807ds/6806Mi) % 209.97/31.13 % (233974)Refutation not found, incomplete strategy % 209.97/31.13 % (233974)------------------------------ % 209.97/31.13 % (233974)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 209.97/31.13 % (233974)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 209.97/31.13 % (233974)CaDiCaL version: 2.1.3 % 209.97/31.13 % (233974)Termination reason: Refutation not found, incomplete strategy % 209.97/31.13 % (233974)Time elapsed: 0.038 s % 209.97/31.13 % (233974)Peak memory usage: 116 MB % 209.97/31.13 % (233974)Instructions burned: 7 (million) % 209.97/31.13 % (233974)------------------------------ % 209.97/31.13 % (233974)------------------------------ % 209.97/31.13 % (233552)Instruction limit reached! % 209.97/31.13 % (233552)------------------------------ % 209.97/31.13 % (233552)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 209.97/31.13 % (233552)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 209.97/31.13 % (233552)CaDiCaL version: 2.1.3 % 209.97/31.14 % (233552)Termination reason: Instruction limit % 209.97/31.14 % (233552)Termination phase: Saturation % 209.97/31.14 % (233552)Time elapsed: 8.476 s % 209.97/31.14 % (233552)Peak memory usage: 133 MB % 209.97/31.14 % (233552)Instructions burned: 13800 (million) % 209.97/31.14 % (233991)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=4189926300:s2a=on:i=3553:nm=0:rtra=on_2800 on theBenchmark for (2800ds/3553Mi) % 209.97/31.14 % (233994)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=3631370102:thitd=on:cond=on:i=2064:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2799 on theBenchmark for (2799ds/2064Mi) % 209.97/31.14 % (233994)Instruction limit reached! % 209.97/31.14 % (233994)------------------------------ % 209.97/31.14 % (233994)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 209.97/31.14 % (233994)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 209.97/31.14 % (233994)CaDiCaL version: 2.1.3 % 209.97/31.14 % (233994)Termination reason: Instruction limit % 209.97/31.14 % (233994)Termination phase: Saturation % 209.97/31.14 % (233994)Time elapsed: 2.122 s % 209.97/31.14 % (233994)Peak memory usage: 144 MB % 209.97/31.14 % (233994)Instructions burned: 2064 (million) % 209.97/31.14 % (234032)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=3819692583:cond=fast:i=20260:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2774 on theBenchmark for (2774ds/20260Mi) % 209.97/31.14 % (233991)Instruction limit reached! % 209.97/31.14 % (233991)------------------------------ % 209.97/31.14 % (233991)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 209.97/31.14 % (233991)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 209.97/31.14 % (233991)CaDiCaL version: 2.1.3 % 209.97/31.14 % (233991)Termination reason: Instruction limit % 209.97/31.14 % (233991)Termination phase: Saturation % 209.97/31.14 % (233991)Time elapsed: 3.658 s % 209.97/31.14 % (233991)Peak memory usage: 107 MB % 209.97/31.14 % (233991)Instructions burned: 3553 (million) % 209.97/31.14 % (234050)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=52814178:avsq=on:i=1244:avsqr=1,16:rtra=on:rawr=on_2761 on theBenchmark for (2761ds/1244Mi) % 209.97/31.14 % (234050)Refutation not found, incomplete strategy % 209.97/31.14 % (234050)------------------------------ % 209.97/31.14 % (234050)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 209.97/31.14 % (234050)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 209.97/31.14 % (234050)CaDiCaL version: 2.1.3 % 209.97/31.14 % (234050)Termination reason: Refutation not found, incomplete strategy % 209.97/31.14 % (234050)Time elapsed: 0.043 s % 209.97/31.14 % (234050)Peak memory usage: 116 MB % 209.97/31.14 % (234050)Instructions burned: 8 (million) % 209.97/31.14 % (234050)------------------------------ % 209.97/31.14 % (234050)------------------------------ % 209.97/31.14 % (234056)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=920125798:i=58261:doe=on:nm=0:rtra=on:gtg=exists_sym_2753 on theBenchmark for (2753ds/58261Mi) % 209.97/31.14 % (234056)Refutation not found, incomplete strategy % 209.97/31.14 % (234056)------------------------------ % 209.97/31.14 % (234056)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 221.33/32.04 % (234056)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 221.33/32.04 % (234056)CaDiCaL version: 2.1.3 % 221.33/32.04 % (234056)Termination reason: Refutation not found, incomplete strategy % 221.33/32.04 % (234056)Time elapsed: 0.074 s % 221.33/32.04 % (234056)Peak memory usage: 116 MB % 221.33/32.04 % (234056)Instructions burned: 36 (million) % 221.33/32.04 % (234056)------------------------------ % 221.33/32.04 % (234056)------------------------------ % 221.33/32.04 % (234062)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 % 221.33/32.04 % (234062)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=4164913934:i=6806:aac=none:nm=0:rtra=on:rawr=on_2746 on theBenchmark for (2746ds/6806Mi) % 221.33/32.04 % (234062)Refutation not found, incomplete strategy % 221.33/32.04 % (234062)------------------------------ % 221.33/32.04 % (234062)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 221.33/32.04 % (234062)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 221.33/32.04 % (234062)CaDiCaL version: 2.1.3 % 221.33/32.04 % (234062)Termination reason: Refutation not found, incomplete strategy % 221.33/32.04 % (234062)Time elapsed: 0.043 s % 221.33/32.04 % (234062)Peak memory usage: 116 MB % 221.33/32.04 % (234062)Instructions burned: 8 (million) % 221.33/32.04 % (234062)------------------------------ % 221.33/32.04 % (234062)------------------------------ % 221.33/32.04 % (234067)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=3293342955:thitd=on:cond=on:i=4081:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2739 on theBenchmark for (2739ds/4081Mi) % 221.33/32.04 % (233680)Instruction limit reached! % 221.33/32.04 % (233680)------------------------------ % 221.33/32.04 % (233680)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 221.33/32.04 % (233680)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 221.33/32.04 % (233680)CaDiCaL version: 2.1.3 % 221.33/32.04 % (233680)Termination reason: Instruction limit % 221.33/32.04 % (233680)Termination phase: Saturation % 221.33/32.04 % (233680)Time elapsed: 13.778 s % 221.33/32.04 % (233680)Peak memory usage: 135 MB % 221.33/32.04 % (233680)Instructions burned: 20260 (million) % 221.33/32.04 % (234071)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=181856712:avsq=on:i=1701:avsqr=1,16:rtra=on:rawr=on_2723 on theBenchmark for (2723ds/1701Mi) % 221.33/32.04 % (234071)Refutation not found, incomplete strategy % 221.33/32.04 % (234071)------------------------------ % 221.33/32.04 % (234071)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 221.33/32.04 % (234071)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 221.33/32.04 % (234071)CaDiCaL version: 2.1.3 % 221.33/32.04 % (234071)Termination reason: Refutation not found, incomplete strategy % 221.33/32.04 % (234071)Time elapsed: 0.030 s % 221.33/32.04 % (234071)Peak memory usage: 116 MB % 221.33/32.04 % (234071)Instructions burned: 8 (million) % 221.33/32.04 % (234071)------------------------------ % 221.33/32.04 % (234071)------------------------------ % 221.33/32.04 % (234079)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=4168884400:i=57001:doe=on:nm=0:rtra=on:gtg=exists_sym_2717 on theBenchmark for (2717ds/57001Mi) % 221.33/32.04 % (234079)Refutation not found, incomplete strategy % 221.33/32.04 % (234079)------------------------------ % 221.33/32.04 % (234079)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 221.33/32.04 % (234079)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 221.33/32.04 % (234079)CaDiCaL version: 2.1.3 % 221.33/32.04 % (234079)Termination reason: Refutation not found, incomplete strategy % 221.33/32.04 % (234079)Time elapsed: 0.071 s % 221.33/32.04 % (234079)Peak memory usage: 117 MB % 221.33/32.04 % (234079)Instructions burned: 42 (million) % 221.33/32.04 % (234079)------------------------------ % 221.33/32.04 % (234079)------------------------------ % 221.33/32.04 % (233968)Instruction limit reached! % 221.33/32.04 % (233968)------------------------------ % 221.33/32.04 % (233968)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 221.33/32.04 % (233968)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 221.33/32.04 % (233968)CaDiCaL version: 2.1.3 % 225.12/32.72 % (233968)Termination reason: Instruction limit % 225.12/32.72 % (233968)Termination phase: Saturation % 225.12/32.72 % (233968)Time elapsed: 9.630 s % 225.12/32.72 % (233968)Peak memory usage: 128 MB % 225.12/32.72 % (233968)Instructions burned: 9203 (million) % 225.12/32.72 % (234088)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=859441937:i=24:doe=on:rtra=on:gtg=exists_top:ss=axioms_2709 on theBenchmark for (2709ds/24Mi) % 225.12/32.72 % (234087)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 % 225.12/32.72 % (234087)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=1990405204:i=8622:aac=none:nm=0:rtra=on:rawr=on_2709 on theBenchmark for (2709ds/8622Mi) % 225.12/32.72 % (234088)Instruction limit reached! % 225.12/32.72 % (234088)------------------------------ % 225.12/32.72 % (234088)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 225.12/32.72 % (234088)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 225.12/32.72 % (234088)CaDiCaL version: 2.1.3 % 225.12/32.72 % (234088)Termination reason: Instruction limit % 225.12/32.72 % (234088)Termination phase: Saturation % 225.12/32.72 % (234088)Time elapsed: 0.056 s % 225.12/32.72 % (234088)Peak memory usage: 116 MB % 225.12/32.72 % (234088)Instructions burned: 25 (million) % 225.12/32.72 % (234087)Refutation not found, incomplete strategy % 225.12/32.72 % (234087)------------------------------ % 225.12/32.72 % (234087)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 225.12/32.72 % (234087)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 225.12/32.72 % (234087)CaDiCaL version: 2.1.3 % 225.12/32.72 % (234087)Termination reason: Refutation not found, incomplete strategy % 225.12/32.72 % (234087)Time elapsed: 0.042 s % 225.12/32.72 % (234087)Peak memory usage: 116 MB % 225.12/32.72 % (234087)Instructions burned: 8 (million) % 225.12/32.72 % (234092)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=72796401:i=614:kws=precedence:nm=0:rtra=on_2706 on theBenchmark for (2706ds/614Mi) % 225.12/32.72 % (234092)Refutation not found, incomplete strategy % 225.12/32.72 % (234092)------------------------------ % 225.12/32.72 % (234092)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 225.12/32.72 % (234092)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 225.12/32.72 % (234092)CaDiCaL version: 2.1.3 % 225.12/32.72 % (234092)Termination reason: Refutation not found, incomplete strategy % 225.12/32.72 % (234092)Time elapsed: 0.081 s % 225.12/32.72 % (234092)Peak memory usage: 117 MB % 225.12/32.72 % (234092)Instructions burned: 40 (million) % 225.12/32.72 % (234087)------------------------------ % 225.12/32.72 % (234087)------------------------------ % 225.12/32.72 % (234095)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=3882755281:i=402:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2702 on theBenchmark for (2702ds/402Mi) % 225.12/32.72 % (234092)------------------------------ % 225.12/32.72 % (234092)------------------------------ % 225.12/32.72 % (234067)Instruction limit reached! % 225.12/32.72 % (234067)------------------------------ % 225.12/32.72 % (234067)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 225.12/32.72 % (234067)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 225.12/32.72 % (234067)CaDiCaL version: 2.1.3 % 225.12/32.72 % (234067)Termination reason: Instruction limit % 225.12/32.72 % (234067)Termination phase: Saturation % 225.12/32.72 % (234067)Time elapsed: 3.978 s % 225.12/32.72 % (234067)Peak memory usage: 151 MB % 225.12/32.72 % (234067)Instructions burned: 4081 (million) % 225.12/32.72 % (234097)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=833005438:s2a=on:i=14:rtra=on:inst=on_2698 on theBenchmark for (2698ds/14Mi) % 225.12/32.72 % (234097)Instruction limit reached! % 225.12/32.72 % (234097)------------------------------ % 225.12/32.72 % (234097)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 225.12/32.72 % (234097)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 225.12/32.72 % (234097)CaDiCaL version: 2.1.3 % 225.12/32.72 % (234097)Termination reason: Instruction limit % 225.12/32.72 % (234097)Termination phase: Saturation % 225.12/32.72 % (234097)Time elapsed: 0.014 s % 225.12/32.72 % (234097)Peak memory usage: 88 MB % 225.12/32.72 % (234097)Instructions burned: 14 (million) % 230.03/33.40 % (234095)Instruction limit reached! % 230.03/33.40 % (234095)------------------------------ % 230.03/33.40 % (234095)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 230.03/33.40 % (234095)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 230.03/33.40 % (234095)CaDiCaL version: 2.1.3 % 230.03/33.40 % (234095)Termination reason: Instruction limit % 230.03/33.40 % (234095)Termination phase: Saturation % 230.03/33.40 % (234095)Time elapsed: 0.462 s % 230.03/33.40 % (234095)Peak memory usage: 119 MB % 230.03/33.40 % (234095)Instructions burned: 402 (million) % 230.03/33.40 % (234098)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=1392600975:i=8:rtra=on_2696 on theBenchmark for (2696ds/8Mi) % 230.03/33.40 % (234098)Instruction limit reached! % 230.03/33.40 % (234098)------------------------------ % 230.03/33.40 % (234098)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 230.03/33.40 % (234098)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 230.03/33.40 % (234098)CaDiCaL version: 2.1.3 % 230.03/33.40 % (234098)Termination reason: Instruction limit % 230.03/33.40 % (234098)Termination phase: Saturation % 230.03/33.40 % (234098)Time elapsed: 0.007 s % 230.03/33.40 % (234098)Peak memory usage: 89 MB % 230.03/33.40 % (234098)Instructions burned: 9 (million) % 230.03/33.40 % (234101)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=4082289594:i=92:rtra=on_2695 on theBenchmark for (2695ds/92Mi) % 230.03/33.40 % (234104)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=2304346597:st=5:i=28:sd=10:rtra=on:ss=axioms:rawr=on_2694 on theBenchmark for (2694ds/28Mi) % 230.03/33.40 % (234104)Refutation not found, incomplete strategy % 230.03/33.40 % (234104)------------------------------ % 230.03/33.40 % (234104)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 230.03/33.40 % (234104)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 230.03/33.40 % (234104)CaDiCaL version: 2.1.3 % 230.03/33.40 % (234104)Termination reason: Refutation not found, incomplete strategy % 230.03/33.40 % (234104)Time elapsed: 0.002 s % 230.03/33.40 % (234104)Peak memory usage: 88 MB % 230.03/33.40 % (234104)Instructions burned: 1 (million) % 230.03/33.40 % (234102)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=2998692418:i=66:rtra=on_2694 on theBenchmark for (2694ds/66Mi) % 230.03/33.40 % (234101)Refutation not found, incomplete strategy % 230.03/33.40 % (234101)------------------------------ % 230.03/33.40 % (234101)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 230.03/33.40 % (234101)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 230.03/33.40 % (234101)CaDiCaL version: 2.1.3 % 230.03/33.40 % (234101)Termination reason: Refutation not found, incomplete strategy % 230.03/33.40 % (234101)Time elapsed: 0.043 s % 230.03/33.40 % (234101)Peak memory usage: 116 MB % 230.03/33.40 % (234101)Instructions burned: 8 (million) % 230.03/33.40 % (234102)Instruction limit reached! % 230.03/33.40 % (234102)------------------------------ % 230.03/33.40 % (234102)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 230.03/33.40 % (234102)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 230.03/33.40 % (234102)CaDiCaL version: 2.1.3 % 230.03/33.40 % (234102)Termination reason: Instruction limit % 230.03/33.40 % (234102)Termination phase: Saturation % 230.03/33.40 % (234102)Time elapsed: 0.104 s % 230.03/33.40 % (234102)Peak memory usage: 116 MB % 230.03/33.40 % (234102)Instructions burned: 66 (million) % 230.03/33.40 % (234104)------------------------------ % 230.03/33.40 % (234104)------------------------------ % 230.03/33.40 % (234109)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=1599675626:i=58:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2691 on theBenchmark for (2691ds/58Mi) % 230.03/33.40 % (234101)------------------------------ % 230.03/33.40 % (234101)------------------------------ % 230.03/33.40 % (234109)Instruction limit reached! % 230.03/33.40 % (234109)------------------------------ % 230.03/33.40 % (234109)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 230.03/33.40 % (234109)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 230.03/33.40 % (234109)CaDiCaL version: 2.1.3 % 230.03/33.40 % (234109)Termination reason: Instruction limit % 230.03/33.40 % (234109)Termination phase: Saturation % 230.03/33.40 % (234109)Time elapsed: 0.046 s % 230.03/33.40 % (234109)Peak memory usage: 88 MB % 230.03/33.40 % (234109)Instructions burned: 59 (million) % 230.03/33.40 % (234110)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=1525504662:cond=on:i=32:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2688 on theBenchmark for (2688ds/32Mi) % 235.10/34.08 % (234110)Instruction limit reached! % 235.10/34.08 % (234110)------------------------------ % 235.10/34.08 % (234110)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 235.10/34.08 % (234110)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.10/34.08 % (234110)CaDiCaL version: 2.1.3 % 235.10/34.08 % (234110)Termination reason: Instruction limit % 235.10/34.08 % (234110)Termination phase: Saturation % 235.10/34.08 % (234110)Time elapsed: 0.030 s % 235.10/34.08 % (234110)Peak memory usage: 90 MB % 235.10/34.08 % (234110)Instructions burned: 32 (million) % 235.10/34.08 % (234112)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=1677709336:i=48:canc=force:rtra=on_2688 on theBenchmark for (2688ds/48Mi) % 235.10/34.08 % (234113)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=848721062:i=54:canc=cautious:fsr=off:rtra=on_2688 on theBenchmark for (2688ds/54Mi) % 235.10/34.08 % (234113)Instruction limit reached! % 235.10/34.08 % (234113)------------------------------ % 235.10/34.08 % (234113)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 235.10/34.08 % (234113)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.10/34.08 % (234113)CaDiCaL version: 2.1.3 % 235.10/34.08 % (234113)Termination reason: Instruction limit % 235.10/34.08 % (234113)Termination phase: Saturation % 235.10/34.08 % (234113)Time elapsed: 0.047 s % 235.10/34.08 % (234113)Peak memory usage: 89 MB % 235.10/34.08 % (234113)Instructions burned: 55 (million) % 235.10/34.08 % (234112)Instruction limit reached! % 235.10/34.08 % (234112)------------------------------ % 235.10/34.08 % (234112)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 235.10/34.08 % (234112)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.10/34.08 % (234112)CaDiCaL version: 2.1.3 % 235.10/34.08 % (234112)Termination reason: Instruction limit % 235.10/34.08 % (234112)Termination phase: Saturation % 235.10/34.08 % (234112)Time elapsed: 0.050 s % 235.10/34.08 % (234112)Peak memory usage: 89 MB % 235.10/34.08 % (234112)Instructions burned: 48 (million) % 235.10/34.08 % (234115)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=2503993924:i=170:gtgl=4:rtra=on:gtg=exists_sym_2686 on theBenchmark for (2686ds/170Mi) % 235.10/34.08 % (234118)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=2006673857:i=4:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2685 on theBenchmark for (2685ds/4Mi) % 235.10/34.08 % (234119)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=1056190759:i=362:rtra=on:ss=axioms:ev=cautious_2685 on theBenchmark for (2685ds/362Mi) % 235.10/34.08 % (234119)Refutation not found, incomplete strategy % 235.10/34.08 % (234119)------------------------------ % 235.10/34.08 % (234119)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 235.10/34.08 % (234119)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.10/34.08 % (234119)CaDiCaL version: 2.1.3 % 235.10/34.08 % (234119)Termination reason: Refutation not found, incomplete strategy % 235.10/34.08 % (234119)Time elapsed: 0.005 s % 235.10/34.08 % (234119)Peak memory usage: 89 MB % 235.10/34.08 % (234118)Instruction limit reached! % 235.10/34.08 % (234118)------------------------------ % 235.10/34.08 % (234118)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 235.10/34.08 % (234118)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.10/34.08 % (234119)Instructions burned: 2 (million) % 235.10/34.08 % (234118)CaDiCaL version: 2.1.3 % 235.10/34.08 % (234118)Termination reason: Instruction limit % 235.10/34.08 % (234118)Termination phase: Saturation % 235.10/34.08 % (234118)Time elapsed: 0.005 s % 235.10/34.08 % (234118)Peak memory usage: 88 MB % 235.10/34.08 % (234118)Instructions burned: 4 (million) % 235.10/34.08 % (234115)Instruction limit reached! % 235.10/34.08 % (234115)------------------------------ % 235.10/34.08 % (234115)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 235.10/34.08 % (234115)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.10/34.08 % (234115)CaDiCaL version: 2.1.3 % 235.10/34.08 % (234115)Termination reason: Instruction limit % 235.10/34.08 % (234115)Termination phase: Saturation % 235.10/34.08 % (234115)Time elapsed: 0.183 s % 235.10/34.08 % (234115)Peak memory usage: 90 MB % 235.10/34.08 % (234115)Instructions burned: 170 (million) % 235.10/34.08 % (234123)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=3868089936:i=8:ep=RST:ins=2:rtra=on_2682 on theBenchmark for (2682ds/8Mi) % 239.56/34.89 % (234123)Instruction limit reached! % 239.56/34.89 % (234123)------------------------------ % 239.56/34.89 % (234123)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 239.56/34.89 % (234123)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 239.56/34.89 % (234123)CaDiCaL version: 2.1.3 % 239.56/34.89 % (234123)Termination reason: Instruction limit % 239.56/34.89 % (234123)Termination phase: Saturation % 239.56/34.89 % (234123)Time elapsed: 0.011 s % 239.56/34.89 % (234123)Peak memory usage: 88 MB % 239.56/34.89 % (234123)Instructions burned: 9 (million) % 239.56/34.89 % (234124)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=2905906358:i=132:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2681 on theBenchmark for (2681ds/132Mi) % 239.56/34.89 % (234119)------------------------------ % 239.56/34.89 % (234119)------------------------------ % 239.56/34.89 % (234126)lrs+10_1_thi=all:si=on:fd=off:random_seed=4047281729:i=106:rtra=on:gtg=all_2679 on theBenchmark for (2679ds/106Mi) % 239.56/34.89 % (234124)Instruction limit reached! % 239.56/34.89 % (234124)------------------------------ % 239.56/34.89 % (234124)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 239.56/34.89 % (234124)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 239.56/34.89 % (234124)CaDiCaL version: 2.1.3 % 239.56/34.89 % (234124)Termination reason: Instruction limit % 239.56/34.89 % (234124)Termination phase: Saturation % 239.56/34.89 % (234124)Time elapsed: 0.216 s % 239.56/34.89 % (234124)Peak memory usage: 134 MB % 239.56/34.89 % (234124)Instructions burned: 132 (million) % 239.56/34.89 % (234126)Instruction limit reached! % 239.56/34.89 % (234126)------------------------------ % 239.56/34.89 % (234126)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 239.56/34.89 % (234126)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 239.56/34.89 % (234126)CaDiCaL version: 2.1.3 % 239.56/34.89 % (234126)Termination reason: Instruction limit % 239.56/34.89 % (234126)Termination phase: Saturation % 239.56/34.89 % (234126)Time elapsed: 0.148 s % 239.56/34.89 % (234126)Peak memory usage: 117 MB % 239.56/34.89 % (234126)Instructions burned: 107 (million) % 239.56/34.89 % (234128)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=4222720076:i=16:ep=RST:nm=16:rtra=on:gtg=exists_top_2678 on theBenchmark for (2678ds/16Mi) % 239.56/34.89 % (234128)Instruction limit reached! % 239.56/34.89 % (234128)------------------------------ % 239.56/34.89 % (234128)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 239.56/34.89 % (234128)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 239.56/34.89 % (234128)CaDiCaL version: 2.1.3 % 239.56/34.89 % (234128)Termination reason: Instruction limit % 239.56/34.89 % (234128)Termination phase: Saturation % 239.56/34.89 % (234128)Time elapsed: 0.019 s % 239.56/34.89 % (234128)Peak memory usage: 88 MB % 239.56/34.89 % (234128)Instructions burned: 16 (million) % 239.56/34.89 % (234130)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=3487726219:st=3:i=4:rtra=on:ss=axioms_2676 on theBenchmark for (2676ds/4Mi) % 239.56/34.89 % (234130)Instruction limit reached! % 239.56/34.89 % (234130)------------------------------ % 239.56/34.89 % (234130)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 239.56/34.89 % (234130)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 239.56/34.89 % (234130)CaDiCaL version: 2.1.3 % 239.56/34.89 % (234130)Termination reason: Instruction limit % 239.56/34.89 % (234130)Termination phase: Saturation % 239.56/34.89 % (234130)Time elapsed: 0.006 s % 239.56/34.89 % (234130)Peak memory usage: 90 MB % 239.56/34.89 % (234130)Instructions burned: 4 (million) % 239.56/34.89 % (234132)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=60812385:i=4:doe=on:canc=force:asg=cautious:rtra=on_2675 on theBenchmark for (2675ds/4Mi) % 239.56/34.89 % (234132)Instruction limit reached! % 239.56/34.89 % (234132)------------------------------ % 239.56/34.89 % (234132)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 239.56/34.89 % (234132)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 239.56/34.89 % (234132)CaDiCaL version: 2.1.3 % 239.56/34.89 % (234132)Termination reason: Instruction limit % 239.56/34.89 % (234132)Termination phase: Saturation % 239.56/34.89 % (234132)Time elapsed: 0.007 s % 239.56/34.89 % (234132)Peak memory usage: 89 MB % 239.56/34.89 % (234132)Instructions burned: 4 (million) % 246.44/35.75 % (234133)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=2881701946:i=254:doe=on:rtra=on_2675 on theBenchmark for (2675ds/254Mi) % 246.44/35.75 % (234135)dis+10_1_si=on:random_seed=2370156504:i=20:ep=R:rtra=on_2673 on theBenchmark for (2673ds/20Mi) % 246.44/35.75 % (234135)Instruction limit reached! % 246.44/35.75 % (234135)------------------------------ % 246.44/35.75 % (234135)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 246.44/35.75 % (234135)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 246.44/35.75 % (234135)CaDiCaL version: 2.1.3 % 246.44/35.75 % (234135)Termination reason: Instruction limit % 246.44/35.75 % (234135)Termination phase: Saturation % 246.44/35.75 % (234135)Time elapsed: 0.021 s % 246.44/35.75 % (234135)Peak memory usage: 88 MB % 246.44/35.75 % (234135)Instructions burned: 20 (million) % 246.44/35.75 % (234137)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=785648674:i=52:canc=cautious:av=off:rtra=on_2672 on theBenchmark for (2672ds/52Mi) % 246.44/35.75 % (234137)Refutation not found, incomplete strategy % 246.44/35.75 % (234137)------------------------------ % 246.44/35.75 % (234137)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 246.44/35.75 % (234137)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 246.44/35.75 % (234137)CaDiCaL version: 2.1.3 % 246.44/35.75 % (234137)Termination reason: Refutation not found, incomplete strategy % 246.44/35.75 % (234137)Time elapsed: 0.005 s % 246.44/35.75 % (234137)Peak memory usage: 89 MB % 246.44/35.75 % (234137)Instructions burned: 2 (million) % 246.44/35.75 % (234133)Instruction limit reached! % 246.44/35.75 % (234133)------------------------------ % 246.44/35.75 % (234133)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 246.44/35.75 % (234133)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 246.44/35.75 % (234133)CaDiCaL version: 2.1.3 % 246.44/35.75 % (234133)Termination reason: Instruction limit % 246.44/35.75 % (234133)Termination phase: Saturation % 246.44/35.75 % (234133)Time elapsed: 0.270 s % 246.44/35.75 % (234133)Peak memory usage: 118 MB % 246.44/35.75 % (234133)Instructions burned: 254 (million) % 246.44/35.75 % (234140)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=3254073931:avsq=on:i=70:doe=on:thsqd=64:nm=64:fsr=off:thsqc=32:rtra=on:tac=light:ss=included:thsq=on:ev=off:sgt=32_2671 on theBenchmark for (2671ds/70Mi) % 246.44/35.75 % (234140)Instruction limit reached! % 246.44/35.75 % (234140)------------------------------ % 246.44/35.75 % (234140)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 246.44/35.75 % (234140)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 246.44/35.75 % (234140)CaDiCaL version: 2.1.3 % 246.44/35.75 % (234140)Termination reason: Instruction limit % 246.44/35.75 % (234140)Termination phase: Saturation % 246.44/35.75 % (234140)Time elapsed: 0.063 s % 246.44/35.75 % (234140)Peak memory usage: 90 MB % 246.44/35.75 % (234140)Instructions burned: 70 (million) % 246.44/35.75 % (234142)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=1060651358:i=4:fsr=off:rtra=on:inst=on_2669 on theBenchmark for (2669ds/4Mi) % 246.44/35.75 % (234142)Instruction limit reached! % 246.44/35.75 % (234142)------------------------------ % 246.44/35.75 % (234142)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 246.44/35.75 % (234142)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 246.44/35.75 % (234142)CaDiCaL version: 2.1.3 % 246.44/35.75 % (234142)Termination reason: Instruction limit % 246.44/35.75 % (234142)Termination phase: Saturation % 246.44/35.75 % (234142)Time elapsed: 0.006 s % 246.44/35.75 % (234142)Peak memory usage: 88 MB % 246.44/35.75 % (234142)Instructions burned: 4 (million) % 246.44/35.75 % (234144)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=920099696:s2a=on:i=16:kws=inv_precedence:doe=on:rtra=on_2668 on theBenchmark for (2668ds/16Mi) % 246.44/35.75 % (234137)------------------------------ % 246.44/35.75 % (234137)------------------------------ % 246.44/35.75 % (234144)Instruction limit reached! % 246.44/35.75 % (234144)------------------------------ % 246.44/35.75 % (234144)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 246.44/35.75 % (234144)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 246.44/35.75 % (234144)CaDiCaL version: 2.1.3 % 246.44/35.75 % (234144)Termination reason: Instruction limit % 246.44/35.75 % (234144)Termination phase: Saturation % 246.44/35.75 % (234144)Time elapsed: 0.021 s % 252.46/36.64 % (234144)Peak memory usage: 89 MB % 252.46/36.64 % (234144)Instructions burned: 17 (million) % 252.46/36.64 % (233815)Instruction limit reached! % 252.46/36.64 % (233815)------------------------------ % 252.46/36.64 % (233815)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 252.46/36.64 % (233815)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.46/36.64 % (233815)CaDiCaL version: 2.1.3 % 252.46/36.64 % (233815)Termination reason: Instruction limit % 252.46/36.64 % (233815)Termination phase: Saturation % 252.46/36.64 % (233815)Time elapsed: 18.858 s % 252.46/36.64 % (233815)Peak memory usage: 688 MB % 252.46/36.64 % (233815)Instructions burned: 34001 (million) % 252.46/36.64 % (234148)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=4201887644:i=26:av=off:rtra=on:gtg=exists_sym:ev=force_2666 on theBenchmark for (2666ds/26Mi) % 252.46/36.64 % (234146)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=2888395329:i=740:ep=RS:fsr=off:rtra=on_2666 on theBenchmark for (2666ds/740Mi) % 252.46/36.64 % (234149)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=2535418326:i=452:rtra=on:gtg=position:ss=axioms_2665 on theBenchmark for (2665ds/452Mi) % 252.46/36.64 % (234148)Instruction limit reached! % 252.46/36.64 % (234148)------------------------------ % 252.46/36.64 % (234148)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 252.46/36.64 % (234148)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.46/36.64 % (234148)CaDiCaL version: 2.1.3 % 252.46/36.64 % (234148)Termination reason: Instruction limit % 252.46/36.64 % (234148)Termination phase: Saturation % 252.46/36.64 % (234148)Time elapsed: 0.062 s % 252.46/36.64 % (234148)Peak memory usage: 116 MB % 252.46/36.64 % (234148)Instructions burned: 26 (million) % 252.46/36.64 % (234149)Refutation not found, incomplete strategy % 252.46/36.64 % (234149)------------------------------ % 252.46/36.64 % (234149)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 252.46/36.64 % (234149)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.46/36.64 % (234149)CaDiCaL version: 2.1.3 % 252.46/36.64 % (234149)Termination reason: Refutation not found, incomplete strategy % 252.46/36.64 % (234149)Time elapsed: 0.042 s % 252.46/36.64 % (234149)Peak memory usage: 116 MB % 252.46/36.64 % (234149)Instructions burned: 7 (million) % 252.46/36.64 % (234150)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=3592298119:i=20:rtra=on_2664 on theBenchmark for (2664ds/20Mi) % 252.46/36.64 % (234150)Refutation not found, incomplete strategy % 252.46/36.64 % (234150)------------------------------ % 252.46/36.64 % (234150)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 252.46/36.64 % (234150)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.46/36.64 % (234150)CaDiCaL version: 2.1.3 % 252.46/36.64 % (234150)Termination reason: Refutation not found, incomplete strategy % 252.46/36.64 % (234150)Time elapsed: 0.002 s % 252.46/36.64 % (234150)Peak memory usage: 88 MB % 252.46/36.64 % (234154)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=2075341255:i=142:rtra=on:gtg=exists_top_2663 on theBenchmark for (2663ds/142Mi) % 252.46/36.64 % (234154)Refutation not found, incomplete strategy % 252.46/36.64 % (234154)------------------------------ % 252.46/36.64 % (234154)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 252.46/36.64 % (234154)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.46/36.64 % (234154)CaDiCaL version: 2.1.3 % 252.46/36.64 % (234154)Termination reason: Refutation not found, incomplete strategy % 252.46/36.64 % (234154)Time elapsed: 0.043 s % 252.46/36.64 % (234154)Peak memory usage: 133 MB % 252.46/36.64 % (234154)Instructions burned: 12 (million) % 252.46/36.64 % (234150)------------------------------ % 252.46/36.64 % (234150)------------------------------ % 252.46/36.64 % (234149)------------------------------ % 252.46/36.64 % (234149)------------------------------ % 252.46/36.64 % (234154)------------------------------ % 252.46/36.64 % (234154)------------------------------ % 252.46/36.64 % (234146)Instruction limit reached! % 252.46/36.64 % (234146)------------------------------ % 252.46/36.64 % (234146)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 252.46/36.64 % (234146)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.46/36.64 % (234146)CaDiCaL version: 2.1.3 % 252.46/36.64 % (234146)Termination reason: Instruction limit % 252.46/36.64 % (234146)Termination phase: Saturation % 252.46/36.64 % (234146)Time elapsed: 0.601 s % 258.35/37.45 % (234146)Peak memory usage: 91 MB % 258.35/37.45 % (234146)Instructions burned: 741 (million) % 258.35/37.45 % (234158)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=660371686:i=150:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2659 on theBenchmark for (2659ds/150Mi) % 258.35/37.45 % (234159)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=4130749836:i=588:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2659 on theBenchmark for (2659ds/588Mi) % 258.35/37.45 % (234162)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=3263800438:i=260:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2658 on theBenchmark for (2658ds/260Mi) % 258.35/37.45 % (234162)Refutation not found, incomplete strategy % 258.35/37.45 % (234162)------------------------------ % 258.35/37.45 % (234162)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 258.35/37.45 % (234162)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 258.35/37.45 % (234162)CaDiCaL version: 2.1.3 % 258.35/37.45 % (234162)Termination reason: Refutation not found, incomplete strategy % 258.35/37.45 % (234162)Time elapsed: 0.035 s % 258.35/37.45 % (234162)Peak memory usage: 116 MB % 258.35/37.45 % (234162)Instructions burned: 23 (million) % 258.35/37.45 % (234158)Instruction limit reached! % 258.35/37.45 % (234158)------------------------------ % 258.35/37.45 % (234158)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 258.35/37.45 % (234158)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 258.35/37.45 % (234158)CaDiCaL version: 2.1.3 % 258.35/37.45 % (234158)Termination reason: Instruction limit % 258.35/37.45 % (234158)Termination phase: Saturation % 258.35/37.45 % (234158)Time elapsed: 0.118 s % 258.35/37.45 % (234158)Peak memory usage: 89 MB % 258.35/37.45 % (234158)Instructions burned: 150 (million) % 258.35/37.45 % (234163)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=587696417:i=262:rtra=on_2657 on theBenchmark for (2657ds/262Mi) % 258.35/37.45 % (234163)Refutation not found, incomplete strategy % 258.35/37.45 % (234163)------------------------------ % 258.35/37.45 % (234163)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 258.35/37.46 % (234163)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 258.35/37.46 % (234163)CaDiCaL version: 2.1.3 % 258.35/37.46 % (234163)Termination reason: Refutation not found, incomplete strategy % 258.35/37.46 % (234163)Time elapsed: 0.068 s % 258.35/37.46 % (234163)Peak memory usage: 132 MB % 258.35/37.46 % (234163)Instructions burned: 12 (million) % 258.35/37.46 % (234162)------------------------------ % 258.35/37.46 % (234162)------------------------------ % 258.35/37.46 % (234168)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=1832017889:i=80:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2655 on theBenchmark for (2655ds/80Mi) % 258.35/37.46 % (234159)Instruction limit reached! % 258.35/37.46 % (234159)------------------------------ % 258.35/37.46 % (234159)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 258.35/37.46 % (234159)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 258.35/37.46 % (234159)CaDiCaL version: 2.1.3 % 258.35/37.46 % (234159)Termination reason: Instruction limit % 258.35/37.46 % (234159)Termination phase: Saturation % 258.35/37.46 % (234159)Time elapsed: 0.449 s % 258.35/37.46 % (234159)Peak memory usage: 89 MB % 258.35/37.46 % (234159)Instructions burned: 588 (million) % 258.35/37.46 % (234168)Instruction limit reached! % 258.35/37.46 % (234168)------------------------------ % 258.35/37.46 % (234168)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 258.35/37.46 % (234168)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 258.35/37.46 % (234168)CaDiCaL version: 2.1.3 % 258.35/37.46 % (234168)Termination reason: Instruction limit % 258.35/37.46 % (234168)Termination phase: Saturation % 258.35/37.46 % (234168)Time elapsed: 0.143 s % 258.35/37.46 % (234168)Peak memory usage: 134 MB % 258.35/37.46 % (234168)Instructions burned: 80 (million) % 258.35/37.46 % (234172)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=3090380022:i=614:rtra=on:gtg=exists_top_2653 on theBenchmark for (2653ds/614Mi) % 258.35/37.46 % (234163)------------------------------ % 258.35/37.46 % (234163)------------------------------ % 258.35/37.46 % (234174)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=1890150229:s2a=on:i=1196:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2651 on theBenchmark for (2651ds/1196Mi) % 266.97/38.69 % (234172)Instruction limit reached! % 266.97/38.69 % (234172)------------------------------ % 266.97/38.69 % (234172)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 266.97/38.69 % (234172)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 266.97/38.69 % (234172)CaDiCaL version: 2.1.3 % 266.97/38.69 % (234172)Termination reason: Instruction limit % 266.97/38.69 % (234172)Termination phase: Saturation % 266.97/38.69 % (234172)Time elapsed: 0.261 s % 266.97/38.69 % (234172)Peak memory usage: 93 MB % 266.97/38.69 % (234172)Instructions burned: 617 (million) % 266.97/38.69 % (234176)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=14517806:i=262:canc=cautious:fsr=off:rtra=on_2651 on theBenchmark for (2651ds/262Mi) % 266.97/38.69 % (234177)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=3440028417:s2pl=no:i=518:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2650 on theBenchmark for (2650ds/518Mi) % 266.97/38.69 % (234174)Refutation not found, incomplete strategy % 266.97/38.69 % (234174)------------------------------ % 266.97/38.69 % (234174)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 266.97/38.69 % (234174)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 266.97/38.69 % (234174)CaDiCaL version: 2.1.3 % 266.97/38.69 % (234174)Termination reason: Refutation not found, incomplete strategy % 266.97/38.69 % (234174)Time elapsed: 0.080 s % 266.97/38.69 % (234174)Peak memory usage: 133 MB % 266.97/38.69 % (234174)Instructions burned: 14 (million) % 266.97/38.69 % (234180)dis+10_1_si=on:random_seed=513545739:s2a=on:i=2000:rtra=on:gtg=exists_all_2648 on theBenchmark for (2648ds/2000Mi) % 266.97/38.69 % (234176)Instruction limit reached! % 266.97/38.69 % (234176)------------------------------ % 266.97/38.69 % (234176)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 266.97/38.69 % (234176)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 266.97/38.69 % (234176)CaDiCaL version: 2.1.3 % 266.97/38.69 % (234176)Termination reason: Instruction limit % 266.97/38.69 % (234176)Termination phase: Saturation % 266.97/38.69 % (234176)Time elapsed: 0.272 s % 266.97/38.69 % (234176)Peak memory usage: 119 MB % 266.97/38.69 % (234176)Instructions burned: 263 (million) % 266.97/38.69 % (234174)------------------------------ % 266.97/38.69 % (234174)------------------------------ % 266.97/38.69 % (234177)Instruction limit reached! % 266.97/38.69 % (234177)------------------------------ % 266.97/38.69 % (234177)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 266.97/38.69 % (234177)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 266.97/38.69 % (234177)CaDiCaL version: 2.1.3 % 266.97/38.69 % (234177)Termination reason: Instruction limit % 266.97/38.69 % (234177)Termination phase: Saturation % 266.97/38.69 % (234177)Time elapsed: 0.474 s % 266.97/38.69 % (234177)Peak memory usage: 117 MB % 266.97/38.69 % (234177)Instructions burned: 518 (million) % 266.97/38.69 % (234185)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=3002346844:i=766:fsr=off:rtra=on:ev=force_2645 on theBenchmark for (2645ds/766Mi) % 266.97/38.69 % (234185)Refutation not found, incomplete strategy % 266.97/38.69 % (234185)------------------------------ % 266.97/38.69 % (234185)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 266.97/38.69 % (234185)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 266.97/38.69 % (234185)CaDiCaL version: 2.1.3 % 266.97/38.69 % (234185)Termination reason: Refutation not found, incomplete strategy % 266.97/38.69 % (234185)Time elapsed: 0.006 s % 266.97/38.69 % (234185)Peak memory usage: 89 MB % 266.97/38.69 % (234185)Instructions burned: 4 (million) % 266.97/38.69 % (234187)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=934177154:i=282:doe=on:rtra=on_2644 on theBenchmark for (2644ds/282Mi) % 266.97/38.69 % (234188)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=469758723:i=130:nm=16:rtra=on_2643 on theBenchmark for (2643ds/130Mi) % 266.97/38.69 % (234188)Refutation not found, incomplete strategy % 266.97/38.69 % (234188)------------------------------ % 266.97/38.69 % (234188)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 266.97/38.69 % (234188)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 266.97/38.69 % (234188)CaDiCaL version: 2.1.3 % 266.97/38.69 % (234188)Termination reason: Refutation not found, incomplete strategy % 272.02/39.30 % (234188)Time elapsed: 0.041 s % 272.02/39.30 % (234188)Peak memory usage: 115 MB % 272.02/39.30 % (234188)Instructions burned: 6 (million) % 272.02/39.30 % (234185)------------------------------ % 272.02/39.30 % (234185)------------------------------ % 272.02/39.30 % (234187)Instruction limit reached! % 272.02/39.30 % (234187)------------------------------ % 272.02/39.30 % (234187)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 272.02/39.30 % (234187)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 272.02/39.30 % (234187)CaDiCaL version: 2.1.3 % 272.02/39.30 % (234187)Termination reason: Instruction limit % 272.02/39.30 % (234187)Termination phase: Saturation % 272.02/39.30 % (234187)Time elapsed: 0.285 s % 272.02/39.30 % (234187)Peak memory usage: 91 MB % 272.02/39.30 % (234187)Instructions burned: 283 (million) % 272.02/39.30 % (234188)------------------------------ % 272.02/39.30 % (234188)------------------------------ % 272.02/39.30 % (234193)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=1453552251:i=242:nm=16:rtra=on_2638 on theBenchmark for (2638ds/242Mi) % 272.02/39.30 % (234194)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=2943594862:s2a=on:i=256:s2at=5:ins=3:rtra=on_2638 on theBenchmark for (2638ds/256Mi) % 272.02/39.30 % (234180)Instruction limit reached! % 272.02/39.30 % (234180)------------------------------ % 272.02/39.30 % (234180)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 272.02/39.30 % (234180)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 272.02/39.30 % (234180)CaDiCaL version: 2.1.3 % 272.02/39.30 % (234180)Termination reason: Instruction limit % 272.02/39.30 % (234180)Termination phase: Saturation % 272.02/39.30 % (234180)Time elapsed: 1.012 s % 272.02/39.30 % (234180)Peak memory usage: 101 MB % 272.02/39.30 % (234180)Instructions burned: 2001 (million) % 272.02/39.30 % (234193)Instruction limit reached! % 272.02/39.30 % (234193)------------------------------ % 272.02/39.30 % (234193)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 272.02/39.30 % (234193)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 272.02/39.30 % (234193)CaDiCaL version: 2.1.3 % 272.02/39.30 % (234193)Termination reason: Instruction limit % 272.02/39.30 % (234193)Termination phase: Saturation % 272.02/39.30 % (234193)Time elapsed: 0.177 s % 272.02/39.30 % (234193)Peak memory usage: 88 MB % 272.02/39.30 % (234193)Instructions burned: 242 (million) % 272.02/39.30 % (234199)dis+1010_1_to=kbo:si=on:random_seed=3795078675:i=350:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2636 on theBenchmark for (2636ds/350Mi) % 272.02/39.30 % (234198)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=82546247:i=78:ins=3:rtra=on_2636 on theBenchmark for (2636ds/78Mi) % 272.02/39.30 % (234194)Instruction limit reached! % 272.02/39.30 % (234194)------------------------------ % 272.02/39.30 % (234194)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 272.02/39.30 % (234194)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 272.02/39.30 % (234194)CaDiCaL version: 2.1.3 % 272.02/39.30 % (234194)Termination reason: Instruction limit % 272.02/39.30 % (234194)Termination phase: Saturation % 272.02/39.30 % (234194)Time elapsed: 0.288 s % 272.02/39.30 % (234194)Peak memory usage: 118 MB % 272.02/39.30 % (234194)Instructions burned: 256 (million) % 272.02/39.30 % (234198)Instruction limit reached! % 272.02/39.30 % (234198)------------------------------ % 272.02/39.30 % (234198)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 272.02/39.30 % (234198)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 272.02/39.30 % (234198)CaDiCaL version: 2.1.3 % 272.02/39.30 % (234198)Termination reason: Instruction limit % 272.02/39.30 % (234198)Termination phase: Saturation % 272.02/39.30 % (234198)Time elapsed: 0.117 s % 272.02/39.30 % (234198)Peak memory usage: 116 MB % 272.02/39.30 % (234198)Instructions burned: 78 (million) % 272.02/39.30 % (234201)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=4165461512:i=658:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2634 on theBenchmark for (2634ds/658Mi) % 272.02/39.30 % (234199)Instruction limit reached! % 272.02/39.30 % (234199)------------------------------ % 272.02/39.30 % (234199)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 272.02/39.30 % (234199)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 272.02/39.30 % (234199)CaDiCaL version: 2.1.3 % 272.02/39.30 % (234199)Termination reason: Instruction limit % 278.00/40.18 % (234199)Termination phase: Saturation % 278.00/40.18 % (234199)Time elapsed: 0.198 s % 278.00/40.18 % (234199)Peak memory usage: 93 MB % 278.00/40.18 % (234199)Instructions burned: 351 (million) % 278.00/40.18 % (234204)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=1867915791:s2a=on:i=966:doe=on:nm=32:rtra=on_2633 on theBenchmark for (2633ds/966Mi) % 278.00/40.18 % (234204)Refutation not found, incomplete strategy % 278.00/40.18 % (234204)------------------------------ % 278.00/40.18 % (234204)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 278.00/40.18 % (234204)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 278.00/40.18 % (234204)CaDiCaL version: 2.1.3 % 278.00/40.18 % (234204)Termination reason: Refutation not found, incomplete strategy % 278.00/40.18 % (234204)Time elapsed: 0.059 s % 278.00/40.18 % (234204)Peak memory usage: 132 MB % 278.00/40.18 % (234204)Instructions burned: 12 (million) % 278.00/40.18 % (234207)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=3234048663:i=698:rtra=on_2632 on theBenchmark for (2632ds/698Mi) % 278.00/40.18 % (234207)Refutation not found, incomplete strategy % 278.00/40.18 % (234207)------------------------------ % 278.00/40.18 % (234207)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 278.00/40.18 % (234207)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 278.00/40.18 % (234207)CaDiCaL version: 2.1.3 % 278.00/40.18 % (234207)Termination reason: Refutation not found, incomplete strategy % 278.00/40.18 % (234207)Time elapsed: 0.024 s % 278.00/40.18 % (234207)Peak memory usage: 116 MB % 278.00/40.18 % (234207)Instructions burned: 7 (million) % 278.00/40.18 % (234206)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=1245046549:thitd=on:i=430:nm=0:rtra=on:ev=force_2632 on theBenchmark for (2632ds/430Mi) % 278.00/40.18 % (234207)------------------------------ % 278.00/40.18 % (234207)------------------------------ % 278.00/40.18 % (234204)------------------------------ % 278.00/40.18 % (234204)------------------------------ % 278.00/40.18 % (234211)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=2666826413:st=2:i=590:rtra=on:ss=axioms_2627 on theBenchmark for (2627ds/590Mi) % 278.00/40.18 % (234201)Instruction limit reached! % 278.00/40.18 % (234201)------------------------------ % 278.00/40.18 % (234201)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 278.00/40.18 % (234201)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 278.00/40.18 % (234201)CaDiCaL version: 2.1.3 % 278.00/40.18 % (234201)Termination reason: Instruction limit % 278.00/40.18 % (234201)Termination phase: Saturation % 278.00/40.18 % (234201)Time elapsed: 0.742 s % 278.00/40.18 % (234201)Peak memory usage: 120 MB % 278.00/40.18 % (234201)Instructions burned: 658 (million) % 278.00/40.18 % (234206)Instruction limit reached! % 278.00/40.18 % (234206)------------------------------ % 278.00/40.18 % (234206)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 278.00/40.18 % (234206)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 278.00/40.18 % (234206)CaDiCaL version: 2.1.3 % 278.00/40.18 % (234206)Termination reason: Instruction limit % 278.00/40.18 % (234206)Termination phase: Saturation % 278.00/40.18 % (234206)Time elapsed: 0.491 s % 278.00/40.18 % (234206)Peak memory usage: 138 MB % 278.00/40.18 % (234206)Instructions burned: 430 (million) % 278.00/40.18 % (234212)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=673405921:i=656:kws=inv_frequency:nm=20:rtra=on_2626 on theBenchmark for (2626ds/656Mi) % 278.00/40.18 % (234217)lrs+1010_1_to=kbo:sil=128000:si=on:sos=on:urr=on:uwa=alasca_main:random_seed=1674230165:i=968:doe=on:nm=0:av=off:rtra=on:ss=axioms_2624 on theBenchmark for (2624ds/968Mi) % 278.00/40.18 % (234215)dis+1010_1_to=lpo:sil=128000:sas=z3:si=on:nwc=5:random_seed=3680379228:i=562:gtgl=2:rtra=on:gtg=all_2624 on theBenchmark for (2624ds/562Mi) % 278.00/40.18 % (234212)Instruction limit reached! % 278.00/40.18 % (234212)------------------------------ % 278.00/40.18 % (234212)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 278.00/40.18 % (234212)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 278.00/40.18 % (234212)CaDiCaL version: 2.1.3 % 278.00/40.18 % (234212)Termination reason: Instruction limit % 278.00/40.18 % (234212)Termination phase: Saturation % 278.00/40.18 % (234212)Time elapsed: 0.365 s % 278.00/40.18 % (234212)Peak memory usage: 121 MB % 278.00/40.18 % (234212)Instructions burned: 656 (million) % 278.00/40.18 % (234211)Instruction limit reached! % 285.52/41.16 % (234211)------------------------------ % 285.52/41.16 % (234211)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 285.52/41.16 % (234211)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 285.52/41.16 % (234211)CaDiCaL version: 2.1.3 % 285.52/41.16 % (234211)Termination reason: Instruction limit % 285.52/41.16 % (234211)Termination phase: Saturation % 285.52/41.16 % (234211)Time elapsed: 0.525 s % 285.52/41.16 % (234211)Peak memory usage: 92 MB % 285.52/41.16 % (234211)Instructions burned: 591 (million) % 285.52/41.16 % (234221)lrs+21_1_to=kbo:sil=128000:thi=neg_eq:si=on:random_seed=4158896248:i=642:canc=force:rtra=on:tac=axiom:ss=axioms:ev=force_2620 on theBenchmark for (2620ds/642Mi) % 285.52/41.16 % (234032)Instruction limit reached! % 285.52/41.16 % (234032)------------------------------ % 285.52/41.16 % (234032)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 285.52/41.16 % (234032)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 285.52/41.16 % (234032)CaDiCaL version: 2.1.3 % 285.52/41.16 % (234032)Termination reason: Instruction limit % 285.52/41.16 % (234032)Termination phase: Saturation % 285.52/41.16 % (234032)Time elapsed: 15.389 s % 285.52/41.16 % (234032)Peak memory usage: 132 MB % 285.52/41.16 % (234032)Instructions burned: 20260 (million) % 285.52/41.16 % (234222)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=3920827839:i=832:rtra=on:gtg=position:ss=axioms_2619 on theBenchmark for (2619ds/832Mi) % 285.52/41.16 % (234215)Instruction limit reached! % 285.52/41.16 % (234215)------------------------------ % 285.52/41.16 % (234215)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 285.52/41.16 % (234215)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 285.52/41.16 % (234215)CaDiCaL version: 2.1.3 % 285.52/41.16 % (234215)Termination reason: Instruction limit % 285.52/41.16 % (234215)Termination phase: Saturation % 285.52/41.16 % (234215)Time elapsed: 0.586 s % 285.52/41.16 % (234215)Peak memory usage: 119 MB % 285.52/41.16 % (234215)Instructions burned: 563 (million) % 285.52/41.16 % (234222)Refutation not found, incomplete strategy % 285.52/41.16 % (234222)------------------------------ % 285.52/41.16 % (234222)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 285.52/41.16 % (234222)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 285.52/41.16 % (234222)CaDiCaL version: 2.1.3 % 285.52/41.16 % (234222)Termination reason: Refutation not found, incomplete strategy % 285.52/41.16 % (234222)Time elapsed: 0.042 s % 285.52/41.16 % (234222)Peak memory usage: 116 MB % 285.52/41.16 % (234222)Instructions burned: 7 (million) % 285.52/41.16 % (234221)Instruction limit reached! % 285.52/41.16 % (234221)------------------------------ % 285.52/41.16 % (234221)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 285.52/41.16 % (234221)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 285.52/41.16 % (234221)CaDiCaL version: 2.1.3 % 285.52/41.16 % (234221)Termination reason: Instruction limit % 285.52/41.16 % (234221)Termination phase: Saturation % 285.52/41.16 % (234221)Time elapsed: 0.310 s % 285.52/41.16 % (234221)Peak memory usage: 116 MB % 285.52/41.16 % (234221)Instructions burned: 643 (million) % 285.52/41.16 % (234217)Instruction limit reached! % 285.52/41.16 % (234217)------------------------------ % 285.52/41.16 % (234217)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 285.52/41.16 % (234217)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 285.52/41.16 % (234217)CaDiCaL version: 2.1.3 % 285.52/41.16 % (234217)Termination reason: Instruction limit % 285.52/41.16 % (234217)Termination phase: Saturation % 285.52/41.16 % (234217)Time elapsed: 0.729 s % 285.52/41.16 % (234217)Peak memory usage: 92 MB % 285.52/41.16 % (234217)Instructions burned: 969 (million) % 285.52/41.16 % (234225)lrs+1010_1_to=kbo:tgt=ground:fde=unused:sas=z3:si=on:sp=unary_frequency:gve=force:spb=goal:tha=off:random_seed=1810174356:i=942:thf=on:kws=precedence:rtra=on_2617 on theBenchmark for (2617ds/942Mi) % 285.52/41.16 % (234225)Refutation not found, incomplete strategy % 285.52/41.16 % (234225)------------------------------ % 285.52/41.16 % (234225)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 285.52/41.16 % (234225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 285.52/41.16 % (234225)CaDiCaL version: 2.1.3 % 285.52/41.16 % (234225)Termination reason: Refutation not found, incomplete strategy % 285.52/41.16 % (234225)Time elapsed: 0.033 s % 285.52/41.16 % (234225)Peak memory usage: 116 MB % 285.52/41.16 % (234225)Instructions burned: 7 (million) % 285.52/41.16 % (234228)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=3531328156:avsq=on:i=552:avsqr=1,2:rtra=on_2616 on theBenchmark for (2616ds/552Mi) % 291.48/42.16 % (234229)lrs+1010_2_to=kbo:sil=128000:tgt=ground:fde=unused:sas=z3:si=on:uwa=off:tha=off:nwc=1:random_seed=1390428422:i=750:kws=inv_arity_squared:rtra=on_2615 on theBenchmark for (2615ds/750Mi) % 291.48/42.16 % (234230)lrs+10_1_to=kbo:sil=128000:tgt=full:sas=z3:si=on:uwa=func_ext:slsqc=1:flr=on:slsq=on:random_seed=3347350410:i=774:bd=preordered:rtra=on:ss=axioms:sgt=8_2615 on theBenchmark for (2615ds/774Mi) % 291.48/42.16 % (234229)Refutation not found, incomplete strategy % 291.48/42.16 % (234229)------------------------------ % 291.48/42.16 % (234229)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 291.48/42.16 % (234229)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 291.48/42.16 % (234229)CaDiCaL version: 2.1.3 % 291.48/42.16 % (234229)Termination reason: Refutation not found, incomplete strategy % 291.48/42.16 % (234229)Time elapsed: 0.031 s % 291.48/42.16 % (234229)Peak memory usage: 115 MB % 291.48/42.16 % (234229)Instructions burned: 7 (million) % 291.48/42.16 % (234222)------------------------------ % 291.48/42.16 % (234222)------------------------------ % 291.48/42.16 % (234225)------------------------------ % 291.48/42.16 % (234225)------------------------------ % 291.48/42.16 % (234229)------------------------------ % 291.48/42.16 % (234229)------------------------------ % 291.48/42.16 % (234237)lrs+10_1_to=kbo:sil=128000:fde=none:si=on:norm_ineq=on:urr=on:nwc=0.5:random_seed=3483235370:i=1026:kws=frequency:bd=all:rtra=on:gtg=exists_all:ss=axioms:sgt=4_2612 on theBenchmark for (2612ds/1026Mi) % 291.48/42.16 % (234228)Instruction limit reached! % 291.48/42.16 % (234228)------------------------------ % 291.48/42.16 % (234228)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 291.48/42.16 % (234228)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 291.48/42.16 % (234228)CaDiCaL version: 2.1.3 % 291.48/42.16 % (234228)Termination reason: Instruction limit % 291.48/42.16 % (234228)Termination phase: Saturation % 291.48/42.16 % (234228)Time elapsed: 0.534 s % 291.48/42.16 % (234228)Peak memory usage: 134 MB % 291.48/42.16 % (234228)Instructions burned: 552 (million) % 291.48/42.16 % (234239)lrs+1010_1_to=kbo:sil=64000:sas=cadical:si=on:sos=on:bce=on:random_seed=2500716598:i=718:rtra=on:gtg=exists_top:ss=axioms_2610 on theBenchmark for (2610ds/718Mi) % 291.48/42.16 % (234238)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=1290606714:i=668:rtra=on_2610 on theBenchmark for (2610ds/668Mi) % 291.48/42.16 % (234238)Refutation not found, incomplete strategy % 291.48/42.16 % (234238)------------------------------ % 291.48/42.16 % (234238)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 291.48/42.16 % (234238)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 291.48/42.16 % (234238)CaDiCaL version: 2.1.3 % 291.48/42.16 % (234238)Termination reason: Refutation not found, incomplete strategy % 291.48/42.16 % (234238)Time elapsed: 0.075 s % 291.48/42.16 % (234238)Peak memory usage: 132 MB % 291.48/42.16 % (234238)Instructions burned: 12 (million) % 291.48/42.16 % (234243)dis+1010_1_to=lpo:sil=128000:thi=all:fde=unused:si=on:sp=reverse_arity:tha=off:random_seed=256744158:i=682:gtgl=2:rtra=on:gtg=exists_sym:ev=force:fsd=on:fsdmm=1_2608 on theBenchmark for (2608ds/682Mi) % 291.48/42.16 % (234243)Refutation not found, incomplete strategy % 291.48/42.16 % (234243)------------------------------ % 291.48/42.16 % (234243)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 291.48/42.16 % (234243)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 291.48/42.16 % (234243)CaDiCaL version: 2.1.3 % 291.48/42.16 % (234243)Termination reason: Refutation not found, incomplete strategy % 291.48/42.16 % (234243)Time elapsed: 0.034 s % 291.48/42.16 % (234243)Peak memory usage: 113 MB % 291.48/42.16 % (234243)Instructions burned: 6 (million) % 291.48/42.16 % (234239)Instruction limit reached! % 291.48/42.16 % (234239)------------------------------ % 291.48/42.16 % (234239)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 291.48/42.16 % (234239)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 291.48/42.16 % (234239)CaDiCaL version: 2.1.3 % 291.48/42.16 % (234239)Termination reason: Instruction limit % 291.48/42.16 % (234239)Termination phase: Saturation % 291.48/42.16 % (234239)Time elapsed: 0.343 s % 291.48/42.16 % (234239)Peak memory usaTerminated %------------------------------------------------------------------------------