%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWX144_1 : TPTP v9.3.1. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % Computer : 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:45:58 PM UTC 2026 % Result : Timeout 300.54s 43.34s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWX144_1 : TPTP v9.3.1. Released v9.3.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.10/0.20 % Computer : n004.cluster.edu % 0.10/0.20 % Model : x86_64 x86_64 % 0.10/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.20 % Memory : 8046.5625MB % 0.10/0.20 % OS : Linux 6.8.0-71-generic % 0.10/0.20 % CPULimit : 300 % 0.10/0.20 % WCLimit : 300 % 0.10/0.20 % DateTime : Mon Sep 28 15:04:23 UTC 2026 % 0.10/0.21 % CPUTime : % 0.10/0.21 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.10/0.24 Running first-order theorem proving % 0.10/0.24 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 2.94/1.48 % (441403)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule. % 2.94/1.48 % (441411)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=1149966394:s2a=on:i=7:rtra=on:inst=on_2996 on theBenchmark for (2996ds/7Mi) % 2.94/1.48 % (441411)Instruction limit reached! % 2.94/1.48 % (441411)------------------------------ % 2.94/1.48 % (441411)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 2.94/1.48 % (441411)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.94/1.48 % (441411)CaDiCaL version: 2.1.3 % 2.94/1.48 % (441411)Termination reason: Instruction limit % 2.94/1.48 % (441411)Termination phase: shuffling % 2.94/1.48 % (441411)Time elapsed: 0.002 s % 2.94/1.48 % (441411)Peak memory usage: 85 MB % 2.94/1.48 % (441411)Instructions burned: 8 (million) % 2.94/1.48 % (441413)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=318967186:i=46:rtra=on_2996 on theBenchmark for (2996ds/46Mi) % 2.94/1.48 % (441409)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=2123957991:i=307:kws=precedence:nm=0:rtra=on_2996 on theBenchmark for (2996ds/307Mi) % 2.94/1.48 % (441414)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=2678401398:i=33:rtra=on_2996 on theBenchmark for (2996ds/33Mi) % 2.94/1.48 % (441408)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=1434331283:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2996 on theBenchmark for (2996ds/12Mi) % 2.94/1.48 % (441410)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=1009643633:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2996 on theBenchmark for (2996ds/201Mi) % 2.94/1.48 % (441408)Instruction limit reached! % 2.94/1.48 % (441408)------------------------------ % 2.94/1.48 % (441408)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 2.94/1.48 % (441408)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.94/1.48 % (441408)CaDiCaL version: 2.1.3 % 2.94/1.48 % (441408)Termination reason: Instruction limit % 2.94/1.48 % (441408)Termination phase: Property scanning % 2.94/1.48 % (441408)Time elapsed: 0.005 s % 2.94/1.48 % (441408)Peak memory usage: 85 MB % 2.94/1.48 % (441408)Instructions burned: 13 (million) % 2.94/1.48 % (441412)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=154809731:i=4:rtra=on_2996 on theBenchmark for (2996ds/4Mi) % 2.94/1.48 % (441412)Instruction limit reached! % 2.94/1.48 % (441412)------------------------------ % 2.94/1.48 % (441412)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 2.94/1.48 % (441412)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.94/1.48 % (441412)CaDiCaL version: 2.1.3 % 2.94/1.48 % (441412)Termination reason: Instruction limit % 2.94/1.48 % (441412)Termination phase: shuffling % 2.94/1.48 % (441412)Time elapsed: 0.002 s % 2.94/1.48 % (441412)Peak memory usage: 85 MB % 2.94/1.48 % (441412)Instructions burned: 5 (million) % 2.94/1.48 % (441414)Instruction limit reached! % 2.94/1.48 % (441414)------------------------------ % 2.94/1.48 % (441414)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 2.94/1.48 % (441414)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.94/1.48 % (441414)CaDiCaL version: 2.1.3 % 2.94/1.48 % (441414)Termination reason: Instruction limit % 2.94/1.48 % (441414)Termination phase: Property scanning % 2.94/1.48 % (441414)Time elapsed: 0.014 s % 2.94/1.48 % (441414)Peak memory usage: 85 MB % 2.94/1.48 % (441414)Instructions burned: 34 (million) % 2.94/1.48 % (441413)Instruction limit reached! % 2.94/1.48 % (441413)------------------------------ % 2.94/1.48 % (441413)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 2.94/1.48 % (441413)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.94/1.48 % (441413)CaDiCaL version: 2.1.3 % 2.94/1.48 % (441413)Termination reason: Instruction limit % 2.94/1.48 % (441413)Termination phase: Property scanning % 2.94/1.48 % (441413)Time elapsed: 0.019 s % 2.94/1.48 % (441413)Peak memory usage: 85 MB % 2.94/1.48 % (441413)Instructions burned: 49 (million) % 2.94/1.48 % (441416)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=350951043:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2995 on theBenchmark for (2995ds/14Mi) % 2.94/1.48 % (441416)Instruction limit reached! % 2.94/1.48 % (441416)------------------------------ % 2.94/1.48 % (441416)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.10/1.62 % (441416)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.10/1.62 % (441416)CaDiCaL version: 2.1.3 % 4.10/1.62 % (441416)Termination reason: Instruction limit % 4.10/1.62 % (441416)Termination phase: shuffling % 4.10/1.62 % (441416)Time elapsed: 0.004 s % 4.10/1.62 % (441416)Peak memory usage: 85 MB % 4.10/1.62 % (441416)Instructions burned: 19 (million) % 4.10/1.62 % (441410)Instruction limit reached! % 4.10/1.62 % (441410)------------------------------ % 4.10/1.62 % (441410)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.10/1.62 % (441410)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.10/1.62 % (441410)CaDiCaL version: 2.1.3 % 4.10/1.62 % (441410)Termination reason: Instruction limit % 4.10/1.62 % (441410)Termination phase: Property scanning % 4.10/1.62 % (441410)Time elapsed: 0.076 s % 4.10/1.62 % (441410)Peak memory usage: 85 MB % 4.10/1.62 % (441410)Instructions burned: 204 (million) % 4.10/1.62 % (441424)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=2951319561:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2994 on theBenchmark for (2994ds/16Mi) % 4.10/1.62 % (441423)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=2872958835:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2994 on theBenchmark for (2994ds/29Mi) % 4.10/1.62 % (441424)Instruction limit reached! % 4.10/1.62 % (441424)------------------------------ % 4.10/1.62 % (441424)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.10/1.62 % (441424)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.10/1.62 % (441424)CaDiCaL version: 2.1.3 % 4.10/1.62 % (441424)Termination reason: Instruction limit % 4.10/1.62 % (441424)Termination phase: shuffling % 4.10/1.62 % (441424)Time elapsed: 0.007 s % 4.10/1.62 % (441424)Peak memory usage: 85 MB % 4.10/1.62 % (441424)Instructions burned: 18 (million) % 4.10/1.62 % (441423)Instruction limit reached! % 4.10/1.62 % (441423)------------------------------ % 4.10/1.62 % (441423)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.10/1.62 % (441423)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.10/1.62 % (441423)CaDiCaL version: 2.1.3 % 4.10/1.62 % (441423)Termination reason: Instruction limit % 4.10/1.62 % (441423)Termination phase: Property scanning % 4.10/1.62 % (441423)Time elapsed: 0.013 s % 4.10/1.62 % (441423)Peak memory usage: 85 MB % 4.10/1.62 % (441423)Instructions burned: 31 (million) % 4.10/1.62 % (441426)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=3412566323:i=27:canc=cautious:fsr=off:rtra=on_2994 on theBenchmark for (2994ds/27Mi) % 4.10/1.62 % (441409)Instruction limit reached! % 4.10/1.62 % (441409)------------------------------ % 4.10/1.62 % (441409)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.10/1.62 % (441409)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.10/1.62 % (441409)CaDiCaL version: 2.1.3 % 4.10/1.62 % (441409)Termination reason: Instruction limit % 4.10/1.62 % (441409)Termination phase: Saturation % 4.10/1.62 % (441409)Time elapsed: 0.139 s % 4.10/1.62 % (441409)Peak memory usage: 112 MB % 4.10/1.62 % (441409)Instructions burned: 307 (million) % 4.10/1.62 % (441425)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=1274259749:i=24:canc=force:rtra=on_2994 on theBenchmark for (2994ds/24Mi) % 4.10/1.62 % (441426)Instruction limit reached! % 4.10/1.62 % (441426)------------------------------ % 4.10/1.62 % (441426)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.10/1.62 % (441426)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.10/1.62 % (441426)CaDiCaL version: 2.1.3 % 4.10/1.62 % (441426)Termination reason: Instruction limit % 4.10/1.62 % (441426)Termination phase: Property scanning % 4.10/1.62 % (441426)Time elapsed: 0.012 s % 4.10/1.62 % (441426)Peak memory usage: 86 MB % 4.10/1.62 % (441426)Instructions burned: 27 (million) % 4.10/1.62 % (441428)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=1255117348:i=85:gtgl=4:rtra=on:gtg=exists_sym_2994 on theBenchmark for (2994ds/85Mi) % 4.10/1.62 % (441425)Instruction limit reached! % 4.10/1.62 % (441425)------------------------------ % 4.10/1.62 % (441425)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.10/1.62 % (441425)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.65/1.76 % (441425)CaDiCaL version: 2.1.3 % 4.65/1.76 % (441425)Termination reason: Instruction limit % 4.65/1.76 % (441425)Termination phase: Property scanning % 4.65/1.76 % (441425)Time elapsed: 0.011 s % 4.65/1.76 % (441425)Peak memory usage: 86 MB % 4.65/1.76 % (441425)Instructions burned: 25 (million) % 4.65/1.76 % (441428)Instruction limit reached! % 4.65/1.76 % (441428)------------------------------ % 4.65/1.76 % (441428)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.65/1.76 % (441428)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.65/1.76 % (441428)CaDiCaL version: 2.1.3 % 4.65/1.76 % (441428)Termination reason: Instruction limit % 4.65/1.76 % (441428)Termination phase: Property scanning % 4.65/1.76 % (441428)Time elapsed: 0.017 s % 4.65/1.76 % (441428)Peak memory usage: 85 MB % 4.65/1.76 % (441428)Instructions burned: 89 (million) % 4.65/1.76 % (441429)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=2814107791:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2994 on theBenchmark for (2994ds/2Mi) % 4.65/1.76 % (441429)Instruction limit reached! % 4.65/1.76 % (441429)------------------------------ % 4.65/1.76 % (441429)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.65/1.76 % (441429)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.65/1.76 % (441429)CaDiCaL version: 2.1.3 % 4.65/1.76 % (441429)Termination reason: Instruction limit % 4.65/1.76 % (441429)Termination phase: shuffling % 4.65/1.76 % (441429)Time elapsed: 0.002 s % 4.65/1.76 % (441429)Peak memory usage: 85 MB % 4.65/1.76 % (441429)Instructions burned: 4 (million) % 4.65/1.76 % (441432)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=2223741153:i=181:rtra=on:ss=axioms:ev=cautious_2993 on theBenchmark for (2993ds/181Mi) % 4.65/1.76 % (441440)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=1122125048:st=3:i=2:rtra=on:ss=axioms_2993 on theBenchmark for (2993ds/2Mi) % 4.65/1.76 % (441440)Instruction limit reached! % 4.65/1.76 % (441440)------------------------------ % 4.65/1.76 % (441440)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.65/1.76 % (441440)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.65/1.76 % (441440)CaDiCaL version: 2.1.3 % 4.65/1.76 % (441440)Termination reason: Instruction limit % 4.65/1.76 % (441440)Termination phase: shuffling % 4.65/1.76 % (441440)Time elapsed: 0.001 s % 4.65/1.76 % (441440)Peak memory usage: 85 MB % 4.65/1.76 % (441440)Instructions burned: 4 (million) % 4.65/1.76 % (441438)lrs+10_1_thi=all:si=on:fd=off:random_seed=1924108938:i=53:rtra=on:gtg=all_2993 on theBenchmark for (2993ds/53Mi) % 4.65/1.76 % (441434)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=3440941257:i=4:ep=RST:ins=2:rtra=on_2993 on theBenchmark for (2993ds/4Mi) % 4.65/1.76 % (441434)Instruction limit reached! % 4.65/1.76 % (441434)------------------------------ % 4.65/1.76 % (441434)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.65/1.76 % (441434)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.65/1.76 % (441434)CaDiCaL version: 2.1.3 % 4.65/1.76 % (441434)Termination reason: Instruction limit % 4.65/1.76 % (441434)Termination phase: shuffling % 4.65/1.76 % (441434)Time elapsed: 0.002 s % 4.65/1.76 % (441434)Peak memory usage: 85 MB % 4.65/1.76 % (441434)Instructions burned: 4 (million) % 4.65/1.76 % (441436)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=2987558808:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2993 on theBenchmark for (2993ds/66Mi) % 4.65/1.76 % (441439)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=2950580882:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2993 on theBenchmark for (2993ds/8Mi) % 4.65/1.76 % (441438)Instruction limit reached! % 4.65/1.76 % (441438)------------------------------ % 4.65/1.76 % (441438)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.65/1.76 % (441438)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.65/1.76 % (441438)CaDiCaL version: 2.1.3 % 4.65/1.76 % (441438)Termination reason: Instruction limit % 4.65/1.76 % (441438)Termination phase: Property scanning % 4.65/1.76 % (441438)Time elapsed: 0.020 s % 4.65/1.76 % (441438)Peak memory usage: 85 MB % 4.65/1.76 % (441438)Instructions burned: 54 (million) % 4.65/1.76 % (441439)Instruction limit reached! % 5.69/1.89 % (441439)------------------------------ % 5.69/1.89 % (441439)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.69/1.89 % (441439)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.69/1.89 % (441439)CaDiCaL version: 2.1.3 % 5.69/1.89 % (441439)Termination reason: Instruction limit % 5.69/1.89 % (441439)Termination phase: Property scanning % 5.69/1.89 % (441439)Time elapsed: 0.004 s % 5.69/1.89 % (441439)Peak memory usage: 85 MB % 5.69/1.89 % (441439)Instructions burned: 9 (million) % 5.69/1.89 % (441436)Instruction limit reached! % 5.69/1.89 % (441436)------------------------------ % 5.69/1.89 % (441436)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.69/1.89 % (441436)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.69/1.89 % (441436)CaDiCaL version: 2.1.3 % 5.69/1.89 % (441436)Termination reason: Instruction limit % 5.69/1.89 % (441436)Termination phase: Property scanning % 5.69/1.89 % (441436)Time elapsed: 0.026 s % 5.69/1.89 % (441436)Peak memory usage: 86 MB % 5.69/1.89 % (441436)Instructions burned: 67 (million) % 5.69/1.89 % (441432)Refutation not found, incomplete strategy % 5.69/1.89 % (441432)------------------------------ % 5.69/1.89 % (441432)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.69/1.89 % (441432)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.69/1.89 % (441432)CaDiCaL version: 2.1.3 % 5.69/1.89 % (441432)Termination reason: Refutation not found, incomplete strategy % 5.69/1.89 % (441432)Time elapsed: 0.063 s % 5.69/1.89 % (441432)Peak memory usage: 88 MB % 5.69/1.89 % (441432)Instructions burned: 173 (million) % 5.69/1.89 % (441442)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=2248382160:i=2:doe=on:canc=force:asg=cautious:rtra=on_2992 on theBenchmark for (2992ds/2Mi) % 5.69/1.89 % (441442)Instruction limit reached! % 5.69/1.89 % (441442)------------------------------ % 5.69/1.89 % (441442)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.69/1.89 % (441442)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.69/1.89 % (441442)CaDiCaL version: 2.1.3 % 5.69/1.89 % (441442)Termination reason: Instruction limit % 5.69/1.89 % (441442)Termination phase: shuffling % 5.69/1.89 % (441442)Time elapsed: 0.002 s % 5.69/1.89 % (441442)Peak memory usage: 85 MB % 5.69/1.89 % (441442)Instructions burned: 4 (million) % 5.69/1.89 % (441445)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=4055721008:i=127:doe=on:rtra=on_2992 on theBenchmark for (2992ds/127Mi) % 5.69/1.89 % (441445)Instruction limit reached! % 5.69/1.89 % (441445)------------------------------ % 5.69/1.89 % (441445)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.69/1.89 % (441445)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.69/1.89 % (441445)CaDiCaL version: 2.1.3 % 5.69/1.89 % (441445)Termination reason: Instruction limit % 5.69/1.89 % (441445)Termination phase: Property scanning % 5.69/1.89 % (441445)Time elapsed: 0.026 s % 5.69/1.89 % (441445)Peak memory usage: 86 MB % 5.69/1.89 % (441445)Instructions burned: 132 (million) % 5.69/1.89 % (441449)dis+10_1_si=on:random_seed=1748483603:i=10:ep=R:rtra=on_2992 on theBenchmark for (2992ds/10Mi) % 5.69/1.89 % (441449)Instruction limit reached! % 5.69/1.89 % (441449)------------------------------ % 5.69/1.89 % (441449)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.69/1.89 % (441449)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.69/1.89 % (441449)CaDiCaL version: 2.1.3 % 5.69/1.89 % (441449)Termination reason: Instruction limit % 5.69/1.89 % (441449)Termination phase: shuffling % 5.69/1.89 % (441449)Time elapsed: 0.005 s % 5.69/1.89 % (441449)Peak memory usage: 85 MB % 5.69/1.89 % (441449)Instructions burned: 12 (million) % 5.69/1.89 % (441452)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=2305955122:avsq=on:i=35:doe=on:thsqd=64:nm=64:fsr=off:thsqc=32:rtra=on:tac=light:ss=included:thsq=on:ev=off:sgt=32_2991 on theBenchmark for (2991ds/35Mi) % 5.69/1.89 % (441451)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=3660336065:i=26:canc=cautious:av=off:rtra=on_2992 on theBenchmark for (2992ds/26Mi) % 5.69/1.89 % (441451)Instruction limit reached! % 5.69/1.89 % (441451)------------------------------ % 5.69/1.89 % (441451)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.69/1.89 % (441451)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.53/2.09 % (441451)CaDiCaL version: 2.1.3 % 7.53/2.09 % (441451)Termination reason: Instruction limit % 7.53/2.09 % (441451)Termination phase: Property scanning % 7.53/2.09 % (441451)Time elapsed: 0.012 s % 7.53/2.09 % (441451)Peak memory usage: 85 MB % 7.53/2.09 % (441451)Instructions burned: 28 (million) % 7.53/2.09 % (441452)Instruction limit reached! % 7.53/2.09 % (441452)------------------------------ % 7.53/2.09 % (441452)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.53/2.09 % (441452)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.53/2.09 % (441452)CaDiCaL version: 2.1.3 % 7.53/2.09 % (441452)Termination reason: Instruction limit % 7.53/2.09 % (441452)Termination phase: Property scanning % 7.53/2.09 % (441452)Time elapsed: 0.015 s % 7.53/2.09 % (441452)Peak memory usage: 85 MB % 7.53/2.09 % (441452)Instructions burned: 38 (million) % 7.53/2.09 % (441453)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=1276137746:i=2:fsr=off:rtra=on:inst=on_2991 on theBenchmark for (2991ds/2Mi) % 7.53/2.09 % (441453)Instruction limit reached! % 7.53/2.09 % (441453)------------------------------ % 7.53/2.09 % (441453)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.53/2.09 % (441453)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.53/2.09 % (441453)CaDiCaL version: 2.1.3 % 7.53/2.09 % (441453)Termination reason: Instruction limit % 7.53/2.09 % (441453)Termination phase: shuffling % 7.53/2.09 % (441453)Time elapsed: 0.002 s % 7.53/2.09 % (441453)Peak memory usage: 85 MB % 7.53/2.09 % (441453)Instructions burned: 4 (million) % 7.53/2.09 % (441457)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=534491071:i=370:ep=RS:fsr=off:rtra=on_2991 on theBenchmark for (2991ds/370Mi) % 7.53/2.09 % (441455)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=2126842595:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2991 on theBenchmark for (2991ds/8Mi) % 7.53/2.09 % (441455)Instruction limit reached! % 7.53/2.09 % (441455)------------------------------ % 7.53/2.09 % (441455)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.53/2.09 % (441455)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.53/2.09 % (441455)CaDiCaL version: 2.1.3 % 7.53/2.09 % (441455)Termination reason: Instruction limit % 7.53/2.09 % (441455)Termination phase: shuffling % 7.53/2.09 % (441455)Time elapsed: 0.004 s % 7.53/2.09 % (441455)Peak memory usage: 85 MB % 7.53/2.09 % (441455)Instructions burned: 9 (million) % 7.53/2.09 % (441459)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=2045377209:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2990 on theBenchmark for (2990ds/13Mi) % 7.53/2.09 % (441459)Instruction limit reached! % 7.53/2.09 % (441459)------------------------------ % 7.53/2.09 % (441459)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.53/2.09 % (441459)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.53/2.09 % (441459)CaDiCaL version: 2.1.3 % 7.53/2.09 % (441459)Termination reason: Instruction limit % 7.53/2.09 % (441459)Termination phase: Property scanning % 7.53/2.09 % (441459)Time elapsed: 0.006 s % 7.53/2.09 % (441459)Peak memory usage: 85 MB % 7.53/2.09 % (441459)Instructions burned: 16 (million) % 7.53/2.09 % (441457)Instruction limit reached! % 7.53/2.09 % (441457)------------------------------ % 7.53/2.09 % (441457)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.53/2.09 % (441457)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.53/2.09 % (441457)CaDiCaL version: 2.1.3 % 7.53/2.09 % (441457)Termination reason: Instruction limit % 7.53/2.09 % (441457)Termination phase: Saturation % 7.53/2.09 % (441457)Time elapsed: 0.072 s % 7.53/2.09 % (441457)Peak memory usage: 88 MB % 7.53/2.09 % (441457)Instructions burned: 374 (million) % 7.53/2.09 % (441462)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=1708677058:i=226:rtra=on:gtg=position:ss=axioms_2990 on theBenchmark for (2990ds/226Mi) % 7.53/2.09 % (441432)------------------------------ % 7.53/2.09 % (441432)------------------------------ % 7.53/2.09 % (441463)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=1423586897:i=10:rtra=on_2990 on theBenchmark for (2990ds/10Mi) % 7.53/2.09 % (441463)Instruction limit reached! % 7.53/2.09 % (441463)------------------------------ % 7.53/2.09 % (441463)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.92/2.27 % (441463)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.92/2.27 % (441463)CaDiCaL version: 2.1.3 % 8.92/2.27 % (441463)Termination reason: Instruction limit % 8.92/2.27 % (441463)Termination phase: shuffling % 8.92/2.27 % (441463)Time elapsed: 0.005 s % 8.92/2.27 % (441463)Peak memory usage: 85 MB % 8.92/2.27 % (441463)Instructions burned: 12 (million) % 8.92/2.27 % (441465)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=1137860061:i=71:rtra=on:gtg=exists_top_2990 on theBenchmark for (2990ds/71Mi) % 8.92/2.27 % (441465)Instruction limit reached! % 8.92/2.27 % (441465)------------------------------ % 8.92/2.27 % (441465)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.92/2.27 % (441465)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.92/2.27 % (441465)CaDiCaL version: 2.1.3 % 8.92/2.27 % (441465)Termination reason: Instruction limit % 8.92/2.27 % (441465)Termination phase: Property scanning % 8.92/2.27 % (441465)Time elapsed: 0.027 s % 8.92/2.27 % (441465)Peak memory usage: 85 MB % 8.92/2.27 % (441465)Instructions burned: 73 (million) % 8.92/2.27 % (441468)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=3118227740:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2990 on theBenchmark for (2990ds/75Mi) % 8.92/2.27 % (441471)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=1884846186:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2989 on theBenchmark for (2989ds/130Mi) % 8.92/2.27 % (441462)Instruction limit reached! % 8.92/2.27 % (441462)------------------------------ % 8.92/2.27 % (441462)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.92/2.27 % (441462)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.92/2.27 % (441462)CaDiCaL version: 2.1.3 % 8.92/2.27 % (441462)Termination reason: Instruction limit % 8.92/2.27 % (441462)Termination phase: Property scanning % 8.92/2.27 % (441462)Time elapsed: 0.085 s % 8.92/2.27 % (441462)Peak memory usage: 86 MB % 8.92/2.27 % (441462)Instructions burned: 228 (million) % 8.92/2.27 % (441468)Instruction limit reached! % 8.92/2.27 % (441468)------------------------------ % 8.92/2.27 % (441468)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.92/2.27 % (441468)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.92/2.27 % (441468)CaDiCaL version: 2.1.3 % 8.92/2.27 % (441468)Termination reason: Instruction limit % 8.92/2.27 % (441468)Termination phase: Property scanning % 8.92/2.27 % (441468)Time elapsed: 0.030 s % 8.92/2.27 % (441468)Peak memory usage: 86 MB % 8.92/2.27 % (441468)Instructions burned: 76 (million) % 8.92/2.27 % (441471)Instruction limit reached! % 8.92/2.27 % (441471)------------------------------ % 8.92/2.27 % (441471)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.92/2.27 % (441471)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.92/2.27 % (441471)CaDiCaL version: 2.1.3 % 8.92/2.27 % (441471)Termination reason: Instruction limit % 8.92/2.27 % (441471)Termination phase: Property scanning % 8.92/2.27 % (441471)Time elapsed: 0.026 s % 8.92/2.27 % (441471)Peak memory usage: 85 MB % 8.92/2.27 % (441471)Instructions burned: 134 (million) % 8.92/2.27 % (441470)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=1679331574:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2989 on theBenchmark for (2989ds/294Mi) % 8.92/2.27 % (441475)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=1057180144:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2989 on theBenchmark for (2989ds/40Mi) % 8.92/2.27 % (441474)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=3573448920:i=131:rtra=on_2989 on theBenchmark for (2989ds/131Mi) % 8.92/2.27 % (441475)Instruction limit reached! % 8.92/2.27 % (441475)------------------------------ % 8.92/2.27 % (441475)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.92/2.27 % (441475)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.92/2.27 % (441475)CaDiCaL version: 2.1.3 % 8.92/2.27 % (441475)Termination reason: Instruction limit % 8.92/2.27 % (441475)Termination phase: Property scanning % 8.92/2.27 % (441475)Time elapsed: 0.016 s % 8.92/2.27 % (441475)Peak memory usage: 85 MB % 8.92/2.27 % (441475)Instructions burned: 43 (million) % 9.75/2.48 % (441477)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=3928199764:i=307:rtra=on:gtg=exists_top_2988 on theBenchmark for (2988ds/307Mi) % 9.75/2.48 % (441483)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=4132703714:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2988 on theBenchmark for (2988ds/259Mi) % 9.75/2.48 % (441474)Instruction limit reached! % 9.75/2.48 % (441474)------------------------------ % 9.75/2.48 % (441474)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.75/2.48 % (441474)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.75/2.48 % (441474)CaDiCaL version: 2.1.3 % 9.75/2.48 % (441474)Termination reason: Instruction limit % 9.75/2.48 % (441474)Termination phase: Property scanning % 9.75/2.48 % (441474)Time elapsed: 0.050 s % 9.75/2.48 % (441474)Peak memory usage: 86 MB % 9.75/2.48 % (441474)Instructions burned: 132 (million) % 9.75/2.48 % (441480)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=2173991793:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2988 on theBenchmark for (2988ds/598Mi) % 9.75/2.48 % (441470)Instruction limit reached! % 9.75/2.48 % (441470)------------------------------ % 9.75/2.48 % (441470)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.75/2.48 % (441470)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.75/2.48 % (441470)CaDiCaL version: 2.1.3 % 9.75/2.48 % (441470)Termination reason: Instruction limit % 9.75/2.48 % (441470)Termination phase: Property scanning % 9.75/2.48 % (441470)Time elapsed: 0.109 s % 9.75/2.48 % (441470)Peak memory usage: 86 MB % 9.75/2.48 % (441470)Instructions burned: 295 (million) % 9.75/2.48 % (441481)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=3105061572:i=131:canc=cautious:fsr=off:rtra=on_2988 on theBenchmark for (2988ds/131Mi) % 9.75/2.48 % (441483)Instruction limit reached! % 9.75/2.48 % (441483)------------------------------ % 9.75/2.48 % (441483)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.75/2.48 % (441483)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.75/2.48 % (441483)CaDiCaL version: 2.1.3 % 9.75/2.48 % (441483)Termination reason: Instruction limit % 9.75/2.48 % (441483)Termination phase: SInE selection % 9.75/2.48 % (441483)Time elapsed: 0.051 s % 9.75/2.48 % (441483)Peak memory usage: 86 MB % 9.75/2.48 % (441483)Instructions burned: 262 (million) % 9.75/2.48 % (441481)Instruction limit reached! % 9.75/2.48 % (441481)------------------------------ % 9.75/2.48 % (441481)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.75/2.48 % (441481)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.75/2.48 % (441481)CaDiCaL version: 2.1.3 % 9.75/2.48 % (441481)Termination reason: Instruction limit % 9.75/2.48 % (441481)Termination phase: Property scanning % 9.75/2.48 % (441481)Time elapsed: 0.050 s % 9.75/2.48 % (441481)Peak memory usage: 86 MB % 9.75/2.48 % (441481)Instructions burned: 133 (million) % 9.75/2.48 % (441477)Instruction limit reached! % 9.75/2.48 % (441477)------------------------------ % 9.75/2.48 % (441477)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.75/2.48 % (441477)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.75/2.48 % (441477)CaDiCaL version: 2.1.3 % 9.75/2.48 % (441477)Termination reason: Instruction limit % 9.75/2.48 % (441477)Termination phase: Property scanning % 9.75/2.48 % (441477)Time elapsed: 0.114 s % 9.75/2.48 % (441477)Peak memory usage: 86 MB % 9.75/2.48 % (441477)Instructions burned: 310 (million) % 9.75/2.48 % (441486)dis+10_1_si=on:random_seed=2665414429:s2a=on:i=1000:rtra=on:gtg=exists_all_2987 on theBenchmark for (2987ds/1000Mi) % 9.75/2.48 % (441490)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=3169175393:i=383:fsr=off:rtra=on:ev=force_2987 on theBenchmark for (2987ds/383Mi) % 9.75/2.48 % (441493)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=1370156047:i=65:nm=16:rtra=on_2987 on theBenchmark for (2987ds/65Mi) % 9.75/2.48 % (441493)Instruction limit reached! % 9.75/2.48 % (441493)------------------------------ % 9.75/2.48 % (441493)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.75/2.48 % (441493)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.81/2.67 % (441493)CaDiCaL version: 2.1.3 % 10.81/2.67 % (441493)Termination reason: Instruction limit % 10.81/2.67 % (441493)Termination phase: Property scanning % 10.81/2.67 % (441493)Time elapsed: 0.014 s % 10.81/2.67 % (441493)Peak memory usage: 86 MB % 10.81/2.67 % (441493)Instructions burned: 70 (million) % 10.81/2.67 % (441491)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=3786350971:i=141:doe=on:rtra=on_2987 on theBenchmark for (2987ds/141Mi) % 10.81/2.67 % (441494)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=2883982220:i=121:nm=16:rtra=on_2986 on theBenchmark for (2986ds/121Mi) % 10.81/2.67 % (441496)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=1394305559:s2a=on:i=128:s2at=5:ins=3:rtra=on_2986 on theBenchmark for (2986ds/128Mi) % 10.81/2.67 % (441491)Instruction limit reached! % 10.81/2.67 % (441491)------------------------------ % 10.81/2.67 % (441491)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.81/2.67 % (441491)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.81/2.67 % (441491)CaDiCaL version: 2.1.3 % 10.81/2.67 % (441491)Termination reason: Instruction limit % 10.81/2.67 % (441491)Termination phase: Property scanning % 10.81/2.67 % (441491)Time elapsed: 0.054 s % 10.81/2.67 % (441491)Peak memory usage: 86 MB % 10.81/2.67 % (441491)Instructions burned: 144 (million) % 10.81/2.67 % (441499)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=236979572:i=39:ins=3:rtra=on_2985 on theBenchmark for (2985ds/39Mi) % 10.81/2.67 % (441499)Instruction limit reached! % 10.81/2.67 % (441499)------------------------------ % 10.81/2.67 % (441499)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.81/2.67 % (441499)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.81/2.67 % (441499)CaDiCaL version: 2.1.3 % 10.81/2.67 % (441499)Termination reason: Instruction limit % 10.81/2.67 % (441499)Termination phase: Property scanning % 10.81/2.67 % (441499)Time elapsed: 0.009 s % 10.81/2.67 % (441499)Peak memory usage: 86 MB % 10.81/2.67 % (441499)Instructions burned: 42 (million) % 10.81/2.67 % (441494)Instruction limit reached! % 10.81/2.67 % (441494)------------------------------ % 10.81/2.67 % (441494)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.81/2.67 % (441494)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.81/2.67 % (441494)CaDiCaL version: 2.1.3 % 10.81/2.67 % (441494)Termination reason: Instruction limit % 10.81/2.67 % (441494)Termination phase: Property scanning % 10.81/2.67 % (441494)Time elapsed: 0.045 s % 10.81/2.67 % (441494)Peak memory usage: 86 MB % 10.81/2.67 % (441494)Instructions burned: 121 (million) % 10.81/2.67 % (441496)Instruction limit reached! % 10.81/2.67 % (441496)------------------------------ % 10.81/2.67 % (441496)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.81/2.67 % (441496)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.81/2.67 % (441496)CaDiCaL version: 2.1.3 % 10.81/2.67 % (441496)Termination reason: Instruction limit % 10.81/2.67 % (441496)Termination phase: Property scanning % 10.81/2.67 % (441496)Time elapsed: 0.048 s % 10.81/2.67 % (441496)Peak memory usage: 86 MB % 10.81/2.67 % (441496)Instructions burned: 129 (million) % 10.81/2.67 % (441480)Instruction limit reached! % 10.81/2.67 % (441480)------------------------------ % 10.81/2.67 % (441480)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.81/2.67 % (441480)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.81/2.67 % (441480)CaDiCaL version: 2.1.3 % 10.81/2.67 % (441480)Termination reason: Instruction limit % 10.81/2.67 % (441480)Termination phase: Saturation % 10.81/2.67 % (441480)Time elapsed: 0.272 s % 10.81/2.67 % (441480)Peak memory usage: 130 MB % 10.81/2.67 % (441480)Instructions burned: 599 (million) % 10.81/2.67 % (441490)Instruction limit reached! % 10.81/2.67 % (441490)------------------------------ % 10.81/2.67 % (441490)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.81/2.67 % (441490)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.81/2.67 % (441490)CaDiCaL version: 2.1.3 % 10.81/2.67 % (441490)Termination reason: Instruction limit % 10.81/2.67 % (441490)Termination phase: Saturation % 10.81/2.67 % (441490)Time elapsed: 0.142 s % 10.81/2.67 % (441490)Peak memory usage: 88 MB % 10.81/2.67 % (441490)Instructions burned: 384 (million) % 10.81/2.67 % (441518)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=2585261485:i=329:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2985 on theBenchmark for (2985ds/329Mi) % 12.94/2.99 % (441506)dis+1010_1_to=kbo:si=on:random_seed=2030873958:i=175:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2985 on theBenchmark for (2985ds/175Mi) % 12.94/2.99 % (441528)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=2765377092:thitd=on:i=215:nm=0:rtra=on:ev=force_2984 on theBenchmark for (2984ds/215Mi) % 12.94/2.99 % (441524)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=3331199713:s2a=on:i=483:doe=on:nm=32:rtra=on_2984 on theBenchmark for (2984ds/483Mi) % 12.94/2.99 % (441518)Instruction limit reached! % 12.94/2.99 % (441518)------------------------------ % 12.94/2.99 % (441518)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.94/2.99 % (441518)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.94/2.99 % (441518)CaDiCaL version: 2.1.3 % 12.94/2.99 % (441518)Termination reason: Instruction limit % 12.94/2.99 % (441518)Termination phase: Property scanning % 12.94/2.99 % (441518)Time elapsed: 0.064 s % 12.94/2.99 % (441518)Peak memory usage: 86 MB % 12.94/2.99 % (441518)Instructions burned: 335 (million) % 12.94/2.99 % (441542)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=2532585727:st=2:i=295:rtra=on:ss=axioms_2984 on theBenchmark for (2984ds/295Mi) % 12.94/2.99 % (441539)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=2354581041:i=349:rtra=on_2984 on theBenchmark for (2984ds/349Mi) % 12.94/2.99 % (441506)Instruction limit reached! % 12.94/2.99 % (441506)------------------------------ % 12.94/2.99 % (441506)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.94/2.99 % (441506)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.94/2.99 % (441506)CaDiCaL version: 2.1.3 % 12.94/2.99 % (441506)Termination reason: Instruction limit % 12.94/2.99 % (441506)Termination phase: Property scanning % 12.94/2.99 % (441506)Time elapsed: 0.066 s % 12.94/2.99 % (441506)Peak memory usage: 85 MB % 12.94/2.99 % (441506)Instructions burned: 177 (million) % 12.94/2.99 % (441528)Instruction limit reached! % 12.94/2.99 % (441528)------------------------------ % 12.94/2.99 % (441528)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.94/2.99 % (441528)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.94/2.99 % (441528)CaDiCaL version: 2.1.3 % 12.94/2.99 % (441528)Termination reason: Instruction limit % 12.94/2.99 % (441528)Termination phase: Property scanning % 12.94/2.99 % (441528)Time elapsed: 0.079 s % 12.94/2.99 % (441528)Peak memory usage: 86 MB % 12.94/2.99 % (441528)Instructions burned: 215 (million) % 12.94/2.99 % (441486)Instruction limit reached! % 12.94/2.99 % (441486)------------------------------ % 12.94/2.99 % (441486)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.94/2.99 % (441486)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.94/2.99 % (441486)CaDiCaL version: 2.1.3 % 12.94/2.99 % (441486)Termination reason: Instruction limit % 12.94/2.99 % (441486)Termination phase: Saturation % 12.94/2.99 % (441486)Time elapsed: 0.377 s % 12.94/2.99 % (441486)Peak memory usage: 89 MB % 12.94/2.99 % (441486)Instructions burned: 1002 (million) % 12.94/2.99 % (441578)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=715774100:i=328:kws=inv_frequency:nm=20:rtra=on_2983 on theBenchmark for (2983ds/328Mi) % 12.94/2.99 % (441542)Refutation not found, incomplete strategy % 12.94/2.99 % (441542)------------------------------ % 12.94/2.99 % (441542)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.94/2.99 % (441542)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.94/2.99 % (441542)CaDiCaL version: 2.1.3 % 12.94/2.99 % (441542)Termination reason: Refutation not found, incomplete strategy % 12.94/2.99 % (441542)Time elapsed: 0.105 s % 12.94/2.99 % (441542)Peak memory usage: 88 MB % 12.94/2.99 % (441542)Instructions burned: 289 (million) % 12.94/2.99 % (441581)dis+1010_1_to=lpo:sil=128000:sas=z3:si=on:nwc=5:random_seed=597465482:i=281:gtgl=2:rtra=on:gtg=all_2983 on theBenchmark for (2983ds/281Mi) % 12.94/2.99 % (441578)Instruction limit reached! % 12.94/2.99 % (441578)------------------------------ % 12.94/2.99 % (441578)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.94/2.99 % (441578)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.27/3.19 % (441578)CaDiCaL version: 2.1.3 % 15.27/3.19 % (441578)Termination reason: Instruction limit % 15.27/3.19 % (441578)Termination phase: Property scanning % 15.27/3.19 % (441578)Time elapsed: 0.064 s % 15.27/3.19 % (441578)Peak memory usage: 86 MB % 15.27/3.19 % (441578)Instructions burned: 333 (million) % 15.27/3.19 % (441539)Instruction limit reached! % 15.27/3.19 % (441539)------------------------------ % 15.27/3.19 % (441539)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.27/3.19 % (441539)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.27/3.19 % (441539)CaDiCaL version: 2.1.3 % 15.27/3.19 % (441539)Termination reason: Instruction limit % 15.27/3.19 % (441539)Termination phase: Saturation % 15.27/3.19 % (441539)Time elapsed: 0.150 s % 15.27/3.19 % (441539)Peak memory usage: 112 MB % 15.27/3.19 % (441539)Instructions burned: 350 (million) % 15.27/3.19 % (441592)lrs+1010_1_to=kbo:sil=128000:si=on:sos=on:urr=on:uwa=alasca_main:random_seed=4139537168:i=484:doe=on:nm=0:av=off:rtra=on:ss=axioms_2982 on theBenchmark for (2982ds/484Mi) % 15.27/3.19 % (441593)lrs+21_1_to=kbo:sil=128000:thi=neg_eq:si=on:random_seed=1469205320:i=321:canc=force:rtra=on:tac=axiom:ss=axioms:ev=force_2982 on theBenchmark for (2982ds/321Mi) % 15.27/3.19 % (441524)Instruction limit reached! % 15.27/3.19 % (441524)------------------------------ % 15.27/3.19 % (441524)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.27/3.19 % (441524)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.27/3.19 % (441524)CaDiCaL version: 2.1.3 % 15.27/3.19 % (441524)Termination reason: Instruction limit % 15.27/3.19 % (441524)Termination phase: Saturation % 15.27/3.19 % (441524)Time elapsed: 0.228 s % 15.27/3.19 % (441524)Peak memory usage: 129 MB % 15.27/3.19 % (441524)Instructions burned: 483 (million) % 15.27/3.19 % (441596)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=4076649643:i=416:rtra=on:gtg=position:ss=axioms_2982 on theBenchmark for (2982ds/416Mi) % 15.27/3.19 % (441581)Instruction limit reached! % 15.27/3.19 % (441581)------------------------------ % 15.27/3.19 % (441581)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.27/3.19 % (441581)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.27/3.19 % (441581)CaDiCaL version: 2.1.3 % 15.27/3.19 % (441581)Termination reason: Instruction limit % 15.27/3.19 % (441581)Termination phase: Property scanning % 15.27/3.19 % (441581)Time elapsed: 0.105 s % 15.27/3.19 % (441581)Peak memory usage: 86 MB % 15.27/3.19 % (441581)Instructions burned: 282 (million) % 15.27/3.19 % (441598)lrs+1010_1_to=kbo:tgt=ground:fde=unused:sas=z3:si=on:sp=unary_frequency:gve=force:spb=goal:tha=off:random_seed=977916657:i=471:thf=on:kws=precedence:rtra=on_2981 on theBenchmark for (2981ds/471Mi) % 15.27/3.19 % (441592)Refutation not found, incomplete strategy % 15.27/3.19 % (441592)------------------------------ % 15.27/3.19 % (441592)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.27/3.19 % (441592)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.27/3.19 % (441592)CaDiCaL version: 2.1.3 % 15.27/3.19 % (441592)Termination reason: Refutation not found, incomplete strategy % 15.27/3.19 % (441592)Time elapsed: 0.102 s % 15.27/3.19 % (441592)Peak memory usage: 88 MB % 15.27/3.19 % (441592)Instructions burned: 282 (million) % 15.27/3.19 % (441596)Refutation not found, incomplete strategy % 15.27/3.19 % (441596)------------------------------ % 15.27/3.19 % (441596)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.27/3.19 % (441596)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.27/3.19 % (441596)CaDiCaL version: 2.1.3 % 15.27/3.19 % (441596)Termination reason: Refutation not found, incomplete strategy % 15.27/3.19 % (441596)Time elapsed: 0.068 s % 15.27/3.19 % (441596)Peak memory usage: 112 MB % 15.27/3.19 % (441596)Instructions burned: 285 (million) % 15.27/3.19 % (441593)Refutation not found, incomplete strategy % 15.27/3.19 % (441593)------------------------------ % 15.27/3.19 % (441593)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.27/3.19 % (441593)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.27/3.19 % (441593)CaDiCaL version: 2.1.3 % 15.27/3.19 % (441593)Termination reason: Refutation not found, incomplete strategy % 15.27/3.19 % (441593)Time elapsed: 0.130 s % 15.27/3.19 % (441593)Peak memory usage: 112 MB % 15.27/3.19 % (441593)Instructions burned: 287 (million) % 16.22/3.47 % (441630)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=3202556376:avsq=on:i=276:avsqr=1,2:rtra=on_2981 on theBenchmark for (2981ds/276Mi) % 16.22/3.47 % (441542)------------------------------ % 16.22/3.47 % (441542)------------------------------ % 16.22/3.47 % (441645)lrs+1010_2_to=kbo:sil=128000:tgt=ground:fde=unused:sas=z3:si=on:uwa=off:tha=off:nwc=1:random_seed=1972076115:i=375:kws=inv_arity_squared:rtra=on_2980 on theBenchmark for (2980ds/375Mi) % 16.22/3.47 % (441596)------------------------------ % 16.22/3.47 % (441596)------------------------------ % 16.22/3.47 % (441630)Instruction limit reached! % 16.22/3.47 % (441630)------------------------------ % 16.22/3.47 % (441630)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.22/3.47 % (441630)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.22/3.47 % (441630)CaDiCaL version: 2.1.3 % 16.22/3.47 % (441630)Termination reason: Instruction limit % 16.22/3.47 % (441630)Termination phase: Property scanning % 16.22/3.47 % (441630)Time elapsed: 0.101 s % 16.22/3.47 % (441630)Peak memory usage: 86 MB % 16.22/3.47 % (441630)Instructions burned: 277 (million) % 16.22/3.47 % (441652)lrs+10_1_to=kbo:sil=128000:tgt=full:sas=z3:si=on:uwa=func_ext:slsqc=1:flr=on:slsq=on:random_seed=2473887541:i=387:bd=preordered:rtra=on:ss=axioms:sgt=8_2979 on theBenchmark for (2979ds/387Mi) % 16.22/3.47 % (441598)Instruction limit reached! % 16.22/3.47 % (441598)------------------------------ % 16.22/3.47 % (441598)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.22/3.47 % (441598)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.22/3.47 % (441598)CaDiCaL version: 2.1.3 % 16.22/3.47 % (441598)Termination reason: Instruction limit % 16.22/3.47 % (441598)Termination phase: Saturation % 16.22/3.47 % (441598)Time elapsed: 0.203 s % 16.22/3.47 % (441598)Peak memory usage: 114 MB % 16.22/3.47 % (441598)Instructions burned: 472 (million) % 16.22/3.47 % (441592)------------------------------ % 16.22/3.47 % (441592)------------------------------ % 16.22/3.47 % (441654)lrs+10_1_to=kbo:sil=128000:fde=none:si=on:norm_ineq=on:urr=on:nwc=0.5:random_seed=1251391676:i=513:kws=frequency:bd=all:rtra=on:gtg=exists_all:ss=axioms:sgt=4_2979 on theBenchmark for (2979ds/513Mi) % 16.22/3.47 % (441645)Instruction limit reached! % 16.22/3.47 % (441645)------------------------------ % 16.22/3.47 % (441645)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.22/3.47 % (441645)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.22/3.47 % (441645)CaDiCaL version: 2.1.3 % 16.22/3.47 % (441645)Termination reason: Instruction limit % 16.22/3.47 % (441645)Termination phase: Saturation % 16.22/3.47 % (441645)Time elapsed: 0.161 s % 16.22/3.47 % (441645)Peak memory usage: 112 MB % 16.22/3.47 % (441645)Instructions burned: 375 (million) % 16.22/3.47 % (441655)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=4026628567:i=334:rtra=on_2979 on theBenchmark for (2979ds/334Mi) % 16.22/3.47 % (441593)------------------------------ % 16.22/3.47 % (441593)------------------------------ % 16.22/3.47 % (441652)Refutation not found, incomplete strategy % 16.22/3.47 % (441652)------------------------------ % 16.22/3.47 % (441652)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.22/3.47 % (441652)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.22/3.47 % (441652)CaDiCaL version: 2.1.3 % 16.22/3.47 % (441652)Termination reason: Refutation not found, incomplete strategy % 16.22/3.47 % (441652)Time elapsed: 0.136 s % 16.22/3.47 % (441652)Peak memory usage: 112 MB % 16.22/3.47 % (441652)Instructions burned: 301 (million) % 16.22/3.47 % (441657)lrs+1010_1_to=kbo:sil=64000:sas=cadical:si=on:sos=on:bce=on:random_seed=3429076832:i=359:rtra=on:gtg=exists_top:ss=axioms_2978 on theBenchmark for (2978ds/359Mi) % 16.22/3.47 % (441654)Instruction limit reached! % 16.22/3.47 % (441654)------------------------------ % 16.22/3.47 % (441654)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.22/3.47 % (441654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.22/3.47 % (441654)CaDiCaL version: 2.1.3 % 16.22/3.47 % (441654)Termination reason: Instruction limit % 16.22/3.47 % (441654)Termination phase: Property scanning % 16.22/3.47 % (441654)Time elapsed: 0.100 s % 16.22/3.47 % (441654)Peak memory usage: 86 MB % 16.22/3.47 % (441654)Instructions burned: 517 (million) % 16.22/3.47 % (441659)dis+1010_1_to=lpo:sil=128000:thi=all:fde=unused:si=on:sp=reverse_arity:tha=off:random_seed=2676537915:i=341:gtgl=2:rtra=on:gtg=exists_sym:ev=force:fsd=on:fsdmm=1_2978 on theBenchmark for (2978ds/341Mi) % 18.22/3.78 % (441660)lrs-2_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_max:tha=off:random_seed=3991217140:st=1.5:i=261:sd=1:kws=precedence:rtra=on:ss=axioms_2978 on theBenchmark for (2978ds/261Mi) % 18.22/3.78 % (441662)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=1136047130:s2pl=no:i=235:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2977 on theBenchmark for (2977ds/235Mi) % 18.22/3.78 % (441664)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=3831865930:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2977 on theBenchmark for (2977ds/273Mi) % 18.22/3.78 % (441655)Instruction limit reached! % 18.22/3.78 % (441655)------------------------------ % 18.22/3.78 % (441655)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.22/3.78 % (441655)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.22/3.78 % (441655)CaDiCaL version: 2.1.3 % 18.22/3.78 % (441655)Termination reason: Instruction limit % 18.22/3.78 % (441655)Termination phase: Saturation % 18.22/3.78 % (441655)Time elapsed: 0.165 s % 18.22/3.78 % (441655)Peak memory usage: 129 MB % 18.22/3.78 % (441655)Instructions burned: 336 (million) % 18.22/3.78 % (441657)Instruction limit reached! % 18.22/3.78 % (441657)------------------------------ % 18.22/3.78 % (441657)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.22/3.78 % (441657)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.22/3.78 % (441657)CaDiCaL version: 2.1.3 % 18.22/3.78 % (441657)Termination reason: Instruction limit % 18.22/3.78 % (441657)Termination phase: SInE selection % 18.22/3.78 % (441657)Time elapsed: 0.132 s % 18.22/3.78 % (441657)Peak memory usage: 86 MB % 18.22/3.78 % (441657)Instructions burned: 361 (million) % 18.22/3.78 % (441660)Refutation not found, incomplete strategy % 18.22/3.78 % (441660)------------------------------ % 18.22/3.78 % (441660)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.22/3.78 % (441660)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.22/3.78 % (441660)CaDiCaL version: 2.1.3 % 18.22/3.78 % (441660)Termination reason: Refutation not found, incomplete strategy % 18.22/3.78 % (441660)Time elapsed: 0.092 s % 18.22/3.78 % (441660)Peak memory usage: 112 MB % 18.22/3.78 % (441660)Instructions burned: 193 (million) % 18.22/3.78 % (441664)Instruction limit reached! % 18.22/3.78 % (441664)------------------------------ % 18.22/3.78 % (441664)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.22/3.78 % (441664)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.22/3.78 % (441664)CaDiCaL version: 2.1.3 % 18.22/3.78 % (441664)Termination reason: Instruction limit % 18.22/3.78 % (441664)Termination phase: Property scanning % 18.22/3.78 % (441664)Time elapsed: 0.053 s % 18.22/3.78 % (441664)Peak memory usage: 86 MB % 18.22/3.78 % (441664)Instructions burned: 279 (million) % 18.22/3.78 % (441659)Instruction limit reached! % 18.22/3.78 % (441659)------------------------------ % 18.22/3.78 % (441659)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.22/3.78 % (441659)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.22/3.78 % (441659)CaDiCaL version: 2.1.3 % 18.22/3.78 % (441659)Termination reason: Instruction limit % 18.22/3.78 % (441659)Termination phase: Property scanning % 18.22/3.78 % (441659)Time elapsed: 0.124 s % 18.22/3.78 % (441659)Peak memory usage: 86 MB % 18.22/3.78 % (441659)Instructions burned: 341 (million) % 18.22/3.78 % (441662)Instruction limit reached! % 18.22/3.78 % (441662)------------------------------ % 18.22/3.78 % (441662)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.22/3.78 % (441662)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.22/3.78 % (441662)CaDiCaL version: 2.1.3 % 18.22/3.78 % (441662)Termination reason: Instruction limit % 18.22/3.78 % (441662)Termination phase: SInE selection % 18.22/3.78 % (441662)Time elapsed: 0.087 s % 18.22/3.78 % (441662)Peak memory usage: 86 MB % 18.22/3.78 % (441662)Instructions burned: 235 (million) % 18.22/3.78 % (441671)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=255963380:avsq=on:i=276:avsqr=1,2:rtra=on_2975 on theBenchmark for (2975ds/276Mi) % 21.65/4.12 % (441652)------------------------------ % 21.65/4.12 % (441652)------------------------------ % 21.65/4.12 % (441669)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=1438832828:i=146:doe=on:rtra=on_2976 on theBenchmark for (2976ds/146Mi) % 21.65/4.12 % (441670)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=2910687993:i=4428:doe=on:fsr=off:rtra=on_2975 on theBenchmark for (2975ds/4428Mi) % 21.65/4.12 % (441671)Instruction limit reached! % 21.65/4.12 % (441671)------------------------------ % 21.65/4.12 % (441671)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.65/4.12 % (441671)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.65/4.12 % (441671)CaDiCaL version: 2.1.3 % 21.65/4.12 % (441671)Termination reason: Instruction limit % 21.65/4.12 % (441671)Termination phase: Property scanning % 21.65/4.12 % (441671)Time elapsed: 0.054 s % 21.65/4.12 % (441671)Peak memory usage: 86 MB % 21.65/4.12 % (441671)Instructions burned: 279 (million) % 21.65/4.12 % (441672)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=693920944:i=1052:rtra=on_2975 on theBenchmark for (2975ds/1052Mi) % 21.65/4.12 % (441669)Instruction limit reached! % 21.65/4.12 % (441669)------------------------------ % 21.65/4.12 % (441669)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.65/4.12 % (441669)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.65/4.12 % (441669)CaDiCaL version: 2.1.3 % 21.65/4.12 % (441669)Termination reason: Instruction limit % 21.65/4.12 % (441669)Termination phase: Property scanning % 21.65/4.12 % (441669)Time elapsed: 0.055 s % 21.65/4.12 % (441669)Peak memory usage: 86 MB % 21.65/4.12 % (441669)Instructions burned: 147 (million) % 21.65/4.12 % (441673)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=1654169530:i=655:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2975 on theBenchmark for (2975ds/655Mi) % 21.65/4.12 % (441660)------------------------------ % 21.65/4.12 % (441660)------------------------------ % 21.65/4.12 % (441676)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=1420223784:st=5:i=1054:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2974 on theBenchmark for (2974ds/1054Mi) % 21.65/4.12 % (441678)lrs-1002_1_to=kbo:sas=z3:si=on:norm_ineq=on:sos=on:tha=some:random_seed=2514820905:i=107:rtra=on_2974 on theBenchmark for (2974ds/107Mi) % 21.65/4.12 % (441678)Instruction limit reached! % 21.65/4.12 % (441678)------------------------------ % 21.65/4.12 % (441678)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.65/4.12 % (441678)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.65/4.12 % (441678)CaDiCaL version: 2.1.3 % 21.65/4.12 % (441678)Termination reason: Instruction limit % 21.65/4.12 % (441678)Termination phase: Property scanning % 21.65/4.12 % (441678)Time elapsed: 0.021 s % 21.65/4.12 % (441678)Peak memory usage: 86 MB % 21.65/4.12 % (441678)Instructions burned: 108 (million) % 21.65/4.12 % (441680)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=2968475220:s2a=on:i=450:doe=on:nm=32:rtra=on_2974 on theBenchmark for (2974ds/450Mi) % 21.65/4.12 % (441676)Refutation not found, incomplete strategy % 21.65/4.12 % (441676)------------------------------ % 21.65/4.12 % (441676)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.65/4.12 % (441676)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.65/4.12 % (441676)CaDiCaL version: 2.1.3 % 21.65/4.12 % (441676)Termination reason: Refutation not found, incomplete strategy % 21.65/4.12 % (441676)Time elapsed: 0.066 s % 21.65/4.12 % (441676)Peak memory usage: 88 MB % 21.65/4.12 % (441676)Instructions burned: 180 (million) % 21.65/4.12 % (441685)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=991215638:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2973 on theBenchmark for (2973ds/130Mi) % 21.65/4.12 % (441684)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 % 21.65/4.12 % (441684)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=408528203:i=1090:aac=none:nm=0:rtra=on:rawr=on_2973 on theBenchmark for (2973ds/1090Mi) % 21.65/4.12 % (441685)Instruction limit reached! % 23.74/4.51 % (441685)------------------------------ % 23.74/4.51 % (441685)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.74/4.51 % (441685)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.74/4.51 % (441685)CaDiCaL version: 2.1.3 % 23.74/4.51 % (441685)Termination reason: Instruction limit % 23.74/4.51 % (441685)Termination phase: Property scanning % 23.74/4.51 % (441685)Time elapsed: 0.026 s % 23.74/4.51 % (441685)Peak memory usage: 85 MB % 23.74/4.51 % (441685)Instructions burned: 134 (million) % 23.74/4.51 % (441673)Instruction limit reached! % 23.74/4.51 % (441673)------------------------------ % 23.74/4.51 % (441673)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.74/4.51 % (441673)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.74/4.51 % (441673)CaDiCaL version: 2.1.3 % 23.74/4.51 % (441673)Termination reason: Instruction limit % 23.74/4.51 % (441673)Termination phase: Saturation % 23.74/4.51 % (441673)Time elapsed: 0.242 s % 23.74/4.51 % (441673)Peak memory usage: 89 MB % 23.74/4.51 % (441673)Instructions burned: 656 (million) % 23.74/4.51 % (441689)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=502584457:i=312:kws=inv_frequency:nm=20:rtra=on_2972 on theBenchmark for (2972ds/312Mi) % 23.74/4.51 % (441680)Instruction limit reached! % 23.74/4.51 % (441680)------------------------------ % 23.74/4.51 % (441680)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.74/4.51 % (441680)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.74/4.51 % (441680)CaDiCaL version: 2.1.3 % 23.74/4.51 % (441680)Termination reason: Instruction limit % 23.74/4.51 % (441680)Termination phase: Saturation % 23.74/4.51 % (441680)Time elapsed: 0.211 s % 23.74/4.51 % (441680)Peak memory usage: 129 MB % 23.74/4.51 % (441680)Instructions burned: 451 (million) % 23.74/4.51 % (441689)Instruction limit reached! % 23.74/4.51 % (441689)------------------------------ % 23.74/4.51 % (441689)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.74/4.51 % (441689)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.74/4.51 % (441689)CaDiCaL version: 2.1.3 % 23.74/4.51 % (441689)Termination reason: Instruction limit % 23.74/4.51 % (441689)Termination phase: Property scanning % 23.74/4.51 % (441689)Time elapsed: 0.060 s % 23.74/4.51 % (441689)Peak memory usage: 86 MB % 23.74/4.51 % (441689)Instructions burned: 315 (million) % 23.74/4.51 % (441690)ott+10_1_to=kbo:sil=64000:si=on:sp=reverse_frequency:sos=on:random_seed=2732546114:i=491:doe=on:rtra=on:gtg=position_2971 on theBenchmark for (2971ds/491Mi) % 23.74/4.51 % (441676)------------------------------ % 23.74/4.51 % (441676)------------------------------ % 23.74/4.51 % (441672)Instruction limit reached! % 23.74/4.51 % (441672)------------------------------ % 23.74/4.51 % (441672)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.74/4.51 % (441672)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.74/4.51 % (441672)CaDiCaL version: 2.1.3 % 23.74/4.51 % (441672)Termination reason: Instruction limit % 23.74/4.51 % (441672)Termination phase: Saturation % 23.74/4.51 % (441672)Time elapsed: 0.396 s % 23.74/4.51 % (441672)Peak memory usage: 95 MB % 23.74/4.51 % (441672)Instructions burned: 1053 (million) % 23.74/4.51 % (441692)ott+1011_4:1_to=lpo:sil=64000:si=on:spb=intro:random_seed=717755222:s2a=on:i=835:s2at=2:rtra=on_2970 on theBenchmark for (2970ds/835Mi) % 23.74/4.51 % (441693)ott+1011_2_to=lpo:sil=128000:si=on:sos=on:random_seed=3864424588:i=307:bd=preordered:av=off:rtra=on:ev=cautious_2970 on theBenchmark for (2970ds/307Mi) % 23.74/4.51 % (441696)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=4131849576:s2a=on:i=646:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2970 on theBenchmark for (2970ds/646Mi) % 23.74/4.51 % (441695)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=1867218809:i=776:doe=on:rtra=on_2970 on theBenchmark for (2970ds/776Mi) % 23.74/4.51 % (441693)Instruction limit reached! % 23.74/4.51 % (441693)------------------------------ % 23.74/4.51 % (441693)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.74/4.51 % (441693)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.74/4.51 % (441693)CaDiCaL version: 2.1.3 % 23.74/4.51 % (441693)Termination reason: Instruction limit % 23.74/4.51 % (441693)Termination phase: Property scanning % 23.74/4.51 % (441693)Time elapsed: 0.059 s % 28.96/5.06 % (441693)Peak memory usage: 86 MB % 28.96/5.06 % (441693)Instructions burned: 310 (million) % 28.96/5.06 % (441690)Instruction limit reached! % 28.96/5.06 % (441690)------------------------------ % 28.96/5.06 % (441690)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 28.96/5.06 % (441690)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.96/5.06 % (441690)CaDiCaL version: 2.1.3 % 28.96/5.06 % (441690)Termination reason: Instruction limit % 28.96/5.06 % (441690)Termination phase: Property scanning % 28.96/5.06 % (441690)Time elapsed: 0.178 s % 28.96/5.06 % (441690)Peak memory usage: 87 MB % 28.96/5.06 % (441690)Instructions burned: 492 (million) % 28.96/5.06 % (441701)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=3990000713:thitd=on:cond=fast:i=784:nm=30:rtra=on:gtg=all:tac=axiom_2969 on theBenchmark for (2969ds/784Mi) % 28.96/5.06 % (441684)Instruction limit reached! % 28.96/5.06 % (441684)------------------------------ % 28.96/5.06 % (441684)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 28.96/5.06 % (441684)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.96/5.06 % (441684)CaDiCaL version: 2.1.3 % 28.96/5.06 % (441684)Termination reason: Instruction limit % 28.96/5.06 % (441684)Termination phase: Saturation % 28.96/5.06 % (441684)Time elapsed: 0.433 s % 28.96/5.06 % (441684)Peak memory usage: 113 MB % 28.96/5.06 % (441684)Instructions burned: 1091 (million) % 28.96/5.06 % (441702)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=1508956838:thitd=on:s2a=on:i=1131:add=on:canc=force:bd=all:rtra=on:tac=axiom:ev=off_2968 on theBenchmark for (2968ds/1131Mi) % 28.96/5.06 % (441701)Instruction limit reached! % 28.96/5.06 % (441701)------------------------------ % 28.96/5.06 % (441701)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 28.96/5.06 % (441701)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.96/5.06 % (441701)CaDiCaL version: 2.1.3 % 28.96/5.06 % (441701)Termination reason: Instruction limit % 28.96/5.06 % (441701)Termination phase: Saturation % 28.96/5.06 % (441701)Time elapsed: 0.161 s % 28.96/5.06 % (441701)Peak memory usage: 112 MB % 28.96/5.06 % (441701)Instructions burned: 784 (million) % 28.96/5.06 % (441704)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=2648562004:s2pl=no:i=246:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2967 on theBenchmark for (2967ds/246Mi) % 28.96/5.06 % (441692)Instruction limit reached! % 28.96/5.06 % (441692)------------------------------ % 28.96/5.06 % (441692)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 28.96/5.06 % (441692)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.96/5.06 % (441692)CaDiCaL version: 2.1.3 % 28.96/5.06 % (441692)Termination reason: Instruction limit % 28.96/5.06 % (441692)Termination phase: Saturation % 28.96/5.06 % (441692)Time elapsed: 0.314 s % 28.96/5.06 % (441692)Peak memory usage: 92 MB % 28.96/5.06 % (441692)Instructions burned: 835 (million) % 28.96/5.06 % (441696)Instruction limit reached! % 28.96/5.06 % (441696)------------------------------ % 28.96/5.06 % (441696)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 28.96/5.06 % (441696)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.96/5.06 % (441696)CaDiCaL version: 2.1.3 % 28.96/5.06 % (441696)Termination reason: Instruction limit % 28.96/5.06 % (441696)Termination phase: Saturation % 28.96/5.06 % (441696)Time elapsed: 0.287 s % 28.96/5.06 % (441696)Peak memory usage: 130 MB % 28.96/5.06 % (441696)Instructions burned: 648 (million) % 28.96/5.06 % (441695)Instruction limit reached! % 28.96/5.06 % (441695)------------------------------ % 28.96/5.06 % (441695)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 28.96/5.06 % (441695)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.96/5.06 % (441695)CaDiCaL version: 2.1.3 % 28.96/5.06 % (441695)Termination reason: Instruction limit % 28.96/5.06 % (441695)Termination phase: Saturation % 28.96/5.06 % (441695)Time elapsed: 0.319 s % 28.96/5.06 % (441695)Peak memory usage: 117 MB % 28.96/5.06 % (441695)Instructions burned: 778 (million) % 28.96/5.06 % (441707)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=4028632456:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2966 on theBenchmark for (2966ds/775Mi) % 28.96/5.06 % (441704)Instruction limit reached! % 28.96/5.06 % (441704)------------------------------ % 39.17/6.51 % (441704)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.17/6.51 % (441704)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.17/6.51 % (441704)CaDiCaL version: 2.1.3 % 39.17/6.51 % (441704)Termination reason: Instruction limit % 39.17/6.51 % (441704)Termination phase: SInE selection % 39.17/6.51 % (441704)Time elapsed: 0.092 s % 39.17/6.51 % (441704)Peak memory usage: 86 MB % 39.17/6.51 % (441704)Instructions burned: 246 (million) % 39.17/6.51 % (441708)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=2491993320:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2966 on theBenchmark for (2966ds/273Mi) % 39.17/6.51 % (441707)Refutation not found, incomplete strategy % 39.17/6.51 % (441707)------------------------------ % 39.17/6.51 % (441707)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.17/6.51 % (441707)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.17/6.51 % (441707)CaDiCaL version: 2.1.3 % 39.17/6.51 % (441707)Termination reason: Refutation not found, incomplete strategy % 39.17/6.51 % (441707)Time elapsed: 0.058 s % 39.17/6.51 % (441707)Peak memory usage: 88 MB % 39.17/6.51 % (441707)Instructions burned: 304 (million) % 39.17/6.51 % (441709)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=2905937823:i=102:nm=16:rtra=on_2966 on theBenchmark for (2966ds/102Mi) % 39.17/6.51 % (441710)lrs+10_1_to=lpo:sil=128000:si=on:bsr=unit_only:tha=off:random_seed=1885889412:avsq=on:s2a=on:i=1094:s2at=5:avsqr=4463,131072:rtra=on_2965 on theBenchmark for (2965ds/1094Mi) % 39.17/6.51 % (441709)Instruction limit reached! % 39.17/6.51 % (441709)------------------------------ % 39.17/6.51 % (441709)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.17/6.51 % (441709)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.17/6.51 % (441709)CaDiCaL version: 2.1.3 % 39.17/6.51 % (441709)Termination reason: Instruction limit % 39.17/6.51 % (441709)Termination phase: Property scanning % 39.17/6.51 % (441709)Time elapsed: 0.040 s % 39.17/6.51 % (441709)Peak memory usage: 86 MB % 39.17/6.51 % (441709)Instructions burned: 105 (million) % 39.17/6.51 % (441708)Instruction limit reached! % 39.17/6.51 % (441708)------------------------------ % 39.17/6.51 % (441708)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.17/6.51 % (441708)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.17/6.51 % (441708)CaDiCaL version: 2.1.3 % 39.17/6.51 % (441708)Termination reason: Instruction limit % 39.17/6.51 % (441708)Termination phase: Property scanning % 39.17/6.51 % (441708)Time elapsed: 0.100 s % 39.17/6.51 % (441708)Peak memory usage: 86 MB % 39.17/6.51 % (441708)Instructions burned: 274 (million) % 39.17/6.51 % (441712)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=939474776:i=6400:doe=on:fsr=off:rtra=on_2965 on theBenchmark for (2965ds/6400Mi) % 39.17/6.51 % (441707)------------------------------ % 39.17/6.51 % (441707)------------------------------ % 39.17/6.51 % (441716)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=703511100:i=868:doe=on:nm=0:rtra=on:gtg=exists_sym_2964 on theBenchmark for (2964ds/868Mi) % 39.17/6.51 % (441718)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=2911376452:i=1846:canc=cautious:fsr=off:rtra=on_2964 on theBenchmark for (2964ds/1846Mi) % 39.17/6.51 % (441702)Instruction limit reached! % 39.17/6.51 % (441702)------------------------------ % 39.17/6.51 % (441702)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.17/6.51 % (441702)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.17/6.51 % (441702)CaDiCaL version: 2.1.3 % 39.17/6.51 % (441702)Termination reason: Instruction limit % 39.17/6.51 % (441702)Termination phase: Saturation % 39.17/6.51 % (441702)Time elapsed: 0.450 s % 39.17/6.51 % (441702)Peak memory usage: 122 MB % 39.17/6.51 % (441702)Instructions burned: 1132 (million) % 39.17/6.51 % (441719)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=3393330750:s2a=on:i=36816:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2963 on theBenchmark for (2963ds/36816Mi) % 39.17/6.51 % (441722)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=831375738:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2962 on theBenchmark for (2962ds/273Mi) % 43.91/7.15 % (441722)Instruction limit reached! % 43.91/7.15 % (441722)------------------------------ % 43.91/7.15 % (441722)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 43.91/7.15 % (441722)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.91/7.15 % (441722)CaDiCaL version: 2.1.3 % 43.91/7.15 % (441722)Termination reason: Instruction limit % 43.91/7.15 % (441722)Termination phase: Property scanning % 43.91/7.15 % (441722)Time elapsed: 0.099 s % 43.91/7.15 % (441722)Peak memory usage: 86 MB % 43.91/7.15 % (441722)Instructions burned: 276 (million) % 43.91/7.15 % (441718)Refutation not found, incomplete strategy % 43.91/7.15 % (441718)------------------------------ % 43.91/7.15 % (441718)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 43.91/7.15 % (441718)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.91/7.15 % (441718)CaDiCaL version: 2.1.3 % 43.91/7.15 % (441718)Termination reason: Refutation not found, incomplete strategy % 43.91/7.15 % (441718)Time elapsed: 0.249 s % 43.91/7.15 % (441718)Peak memory usage: 91 MB % 43.91/7.15 % (441718)Instructions burned: 676 (million) % 43.91/7.15 % (441710)Instruction limit reached! % 43.91/7.15 % (441710)------------------------------ % 43.91/7.15 % (441710)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 43.91/7.15 % (441710)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.91/7.15 % (441710)CaDiCaL version: 2.1.3 % 43.91/7.15 % (441710)Termination reason: Instruction limit % 43.91/7.15 % (441710)Termination phase: Saturation % 43.91/7.15 % (441710)Time elapsed: 0.418 s % 43.91/7.15 % (441710)Peak memory usage: 95 MB % 43.91/7.15 % (441710)Instructions burned: 1095 (million) % 43.91/7.15 % (441716)Instruction limit reached! % 43.91/7.15 % (441716)------------------------------ % 43.91/7.15 % (441716)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 43.91/7.15 % (441716)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.91/7.15 % (441716)CaDiCaL version: 2.1.3 % 43.91/7.15 % (441716)Termination reason: Instruction limit % 43.91/7.15 % (441716)Termination phase: Saturation % 43.91/7.15 % (441716)Time elapsed: 0.330 s % 43.91/7.15 % (441716)Peak memory usage: 116 MB % 43.91/7.15 % (441716)Instructions burned: 870 (million) % 43.91/7.15 % (441725)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=544038752:i=863:doe=on:nm=0:rtra=on:gtg=exists_sym_2960 on theBenchmark for (2960ds/863Mi) % 43.91/7.15 % (441726)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=422362571:i=5811:kws=precedence:nm=0:rtra=on_2960 on theBenchmark for (2960ds/5811Mi) % 43.91/7.15 % (441727)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=2210874027:i=2216:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2959 on theBenchmark for (2959ds/2216Mi) % 43.91/7.15 % (441718)------------------------------ % 43.91/7.15 % (441718)------------------------------ % 43.91/7.15 % (441670)Instruction limit reached! % 43.91/7.15 % (441670)------------------------------ % 43.91/7.15 % (441670)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 43.91/7.15 % (441670)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.91/7.15 % (441670)CaDiCaL version: 2.1.3 % 43.91/7.15 % (441670)Termination reason: Instruction limit % 43.91/7.15 % (441670)Termination phase: Saturation % 43.91/7.15 % (441670)Time elapsed: 1.694 s % 43.91/7.15 % (441670)Peak memory usage: 92 MB % 43.91/7.15 % (441670)Instructions burned: 4430 (million) % 43.91/7.15 % (441731)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=1935435683:i=801:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2958 on theBenchmark for (2958ds/801Mi) % 43.91/7.15 % (441732)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=4166856007:st=5:i=1026:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2957 on theBenchmark for (2957ds/1026Mi) % 43.91/7.15 % (441725)Instruction limit reached! % 43.91/7.15 % (441725)------------------------------ % 43.91/7.15 % (441725)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 43.91/7.15 % (441725)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.91/7.15 % (441725)CaDiCaL version: 2.1.3 % 43.91/7.15 % (441725)Termination reason: Instruction limit % 51.43/8.26 % (441725)Termination phase: Saturation % 51.43/8.26 % (441725)Time elapsed: 0.327 s % 51.43/8.26 % (441725)Peak memory usage: 116 MB % 51.43/8.26 % (441725)Instructions burned: 863 (million) % 51.43/8.26 % (441732)Refutation not found, incomplete strategy % 51.43/8.26 % (441732)------------------------------ % 51.43/8.26 % (441732)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 51.43/8.26 % (441732)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 51.43/8.26 % (441732)CaDiCaL version: 2.1.3 % 51.43/8.26 % (441732)Termination reason: Refutation not found, incomplete strategy % 51.43/8.26 % (441732)Time elapsed: 0.065 s % 51.43/8.26 % (441732)Peak memory usage: 88 MB % 51.43/8.26 % (441732)Instructions burned: 180 (million) % 51.43/8.26 % (441735)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=468594390:i=3509:rtra=on_2956 on theBenchmark for (2956ds/3509Mi) % 51.43/8.26 % (441731)Instruction limit reached! % 51.43/8.26 % (441731)------------------------------ % 51.43/8.26 % (441731)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 51.43/8.26 % (441731)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 51.43/8.26 % (441731)CaDiCaL version: 2.1.3 % 51.43/8.26 % (441731)Termination reason: Instruction limit % 51.43/8.26 % (441731)Termination phase: Saturation % 51.43/8.26 % (441731)Time elapsed: 0.287 s % 51.43/8.26 % (441731)Peak memory usage: 93 MB % 51.43/8.26 % (441731)Instructions burned: 802 (million) % 51.43/8.26 % (441732)------------------------------ % 51.43/8.26 % (441732)------------------------------ % 51.43/8.26 % (441737)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=423481066:st=2:i=2127:sd=12:ep=R:rtra=on:ss=axioms_2954 on theBenchmark for (2954ds/2127Mi) % 51.43/8.26 % (441738)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=283318375:i=1959:rtra=on:fsd=on:proc=on_2953 on theBenchmark for (2953ds/1959Mi) % 51.43/8.26 % (441737)Refutation not found, incomplete strategy % 51.43/8.26 % (441737)------------------------------ % 51.43/8.26 % (441737)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 51.43/8.26 % (441737)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 51.43/8.26 % (441737)CaDiCaL version: 2.1.3 % 51.43/8.26 % (441737)Termination reason: Refutation not found, incomplete strategy % 51.43/8.26 % (441737)Time elapsed: 0.104 s % 51.43/8.26 % (441737)Peak memory usage: 88 MB % 51.43/8.26 % (441737)Instructions burned: 289 (million) % 51.43/8.26 % (441727)Instruction limit reached! % 51.43/8.26 % (441727)------------------------------ % 51.43/8.26 % (441727)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 51.43/8.26 % (441727)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 51.43/8.26 % (441727)CaDiCaL version: 2.1.3 % 51.43/8.26 % (441727)Termination reason: Instruction limit % 51.43/8.26 % (441727)Termination phase: Saturation % 51.43/8.26 % (441727)Time elapsed: 0.854 s % 51.43/8.26 % (441727)Peak memory usage: 119 MB % 51.43/8.26 % (441727)Instructions burned: 2218 (million) % 51.43/8.26 % (441737)------------------------------ % 51.43/8.26 % (441737)------------------------------ % 51.43/8.26 % (441741)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=475388232:s2a=on:i=3553:nm=0:rtra=on_2949 on theBenchmark for (2949ds/3553Mi) % 51.43/8.26 % (441742)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=1784331733:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2949 on theBenchmark for (2949ds/3201Mi) % 51.43/8.26 % (441738)Instruction limit reached! % 51.43/8.26 % (441738)------------------------------ % 51.43/8.26 % (441738)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 51.43/8.26 % (441738)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 51.43/8.26 % (441738)CaDiCaL version: 2.1.3 % 51.43/8.26 % (441738)Termination reason: Instruction limit % 51.43/8.26 % (441738)Termination phase: Saturation % 51.43/8.26 % (441738)Time elapsed: 0.756 s % 51.43/8.26 % (441738)Peak memory usage: 122 MB % 51.43/8.26 % (441738)Instructions burned: 1961 (million) % 51.43/8.26 % (441745)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=1701963567:thitd=on:cond=on:i=4093:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2944 on theBenchmark for (2944ds/4093Mi) % 51.43/8.26 % (441735)Instruction limit reached! % 51.43/8.26 % (441735)------------------------------ % 51.43/8.26 % (441735)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 72.72/11.29 % (441735)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.72/11.29 % (441735)CaDiCaL version: 2.1.3 % 72.72/11.29 % (441735)Termination reason: Instruction limit % 72.72/11.29 % (441735)Termination phase: Saturation % 72.72/11.29 % (441735)Time elapsed: 1.315 s % 72.72/11.29 % (441735)Peak memory usage: 92 MB % 72.72/11.29 % (441735)Instructions burned: 3510 (million) % 72.72/11.29 % (441742)Refutation not found, incomplete strategy % 72.72/11.29 % (441742)------------------------------ % 72.72/11.29 % (441742)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 72.72/11.29 % (441742)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.72/11.29 % (441742)CaDiCaL version: 2.1.3 % 72.72/11.29 % (441742)Termination reason: Refutation not found, incomplete strategy % 72.72/11.29 % (441742)Time elapsed: 0.684 s % 72.72/11.29 % (441742)Peak memory usage: 99 MB % 72.72/11.29 % (441742)Instructions burned: 1822 (million) % 72.72/11.29 % (441747)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=24868368:cond=fast:i=21173:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2941 on theBenchmark for (2941ds/21173Mi) % 72.72/11.29 % (441712)Instruction limit reached! % 72.72/11.29 % (441712)------------------------------ % 72.72/11.29 % (441712)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 72.72/11.29 % (441712)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.72/11.29 % (441712)CaDiCaL version: 2.1.3 % 72.72/11.29 % (441712)Termination reason: Instruction limit % 72.72/11.29 % (441712)Termination phase: Saturation % 72.72/11.29 % (441712)Time elapsed: 2.429 s % 72.72/11.29 % (441712)Peak memory usage: 92 MB % 72.72/11.29 % (441712)Instructions burned: 6402 (million) % 72.72/11.29 % (441747)Refutation not found, incomplete strategy % 72.72/11.29 % (441747)------------------------------ % 72.72/11.29 % (441747)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 72.72/11.29 % (441747)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.72/11.29 % (441747)CaDiCaL version: 2.1.3 % 72.72/11.29 % (441747)Termination reason: Refutation not found, incomplete strategy % 72.72/11.29 % (441747)Time elapsed: 0.079 s % 72.72/11.29 % (441747)Peak memory usage: 113 MB % 72.72/11.29 % (441747)Instructions burned: 147 (million) % 72.72/11.29 % (441742)------------------------------ % 72.72/11.29 % (441742)------------------------------ % 72.72/11.29 % (441749)lrs+11_1_to=lpo:thi=all:sas=z3:si=on:fd=off:sac=on:slsq=on:random_seed=3807991715:avsq=on:i=10544:avsqr=17,4:canc=force:rtra=on:gtg=exists_top:er=filter_2939 on theBenchmark for (2939ds/10544Mi) % 72.72/11.29 % (441750)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=1685796780:avsq=on:i=1262:avsqr=1,16:rtra=on:rawr=on_2938 on theBenchmark for (2938ds/1262Mi) % 72.72/11.29 % (441747)------------------------------ % 72.72/11.29 % (441747)------------------------------ % 72.72/11.29 % (441726)Instruction limit reached! % 72.72/11.29 % (441726)------------------------------ % 72.72/11.29 % (441726)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 72.72/11.29 % (441726)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.72/11.29 % (441726)CaDiCaL version: 2.1.3 % 72.72/11.29 % (441726)Termination reason: Instruction limit % 72.72/11.29 % (441726)Termination phase: Saturation % 72.72/11.29 % (441726)Time elapsed: 2.179 s % 72.72/11.29 % (441726)Peak memory usage: 124 MB % 72.72/11.29 % (441726)Instructions burned: 5812 (million) % 72.72/11.29 % (441753)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=2738598585:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2937 on theBenchmark for (2937ds/775Mi) % 72.72/11.29 % (441754)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=2251386194:i=270:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2937 on theBenchmark for (2937ds/270Mi) % 72.72/11.29 % (441741)Instruction limit reached! % 72.72/11.29 % (441741)------------------------------ % 72.72/11.29 % (441741)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 72.72/11.29 % (441741)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.72/11.29 % (441741)CaDiCaL version: 2.1.3 % 72.72/11.29 % (441741)Termination reason: Instruction limit % 72.72/11.29 % (441741)Termination phase: Saturation % 72.72/11.29 % (441741)Time elapsed: 1.330 s % 72.72/11.29 % (441741)Peak memory usage: 95 MB % 76.04/12.02 % (441741)Instructions burned: 3554 (million) % 76.04/12.02 % (441754)Instruction limit reached! % 76.04/12.02 % (441754)------------------------------ % 76.04/12.02 % (441754)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 76.04/12.02 % (441754)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 76.04/12.02 % (441754)CaDiCaL version: 2.1.3 % 76.04/12.02 % (441754)Termination reason: Instruction limit % 76.04/12.02 % (441754)Termination phase: Property scanning % 76.04/12.02 % (441754)Time elapsed: 0.098 s % 76.04/12.02 % (441754)Peak memory usage: 86 MB % 76.04/12.02 % (441754)Instructions burned: 272 (million) % 76.04/12.02 % (441753)Refutation not found, incomplete strategy % 76.04/12.02 % (441753)------------------------------ % 76.04/12.02 % (441753)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 76.04/12.02 % (441753)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 76.04/12.02 % (441753)CaDiCaL version: 2.1.3 % 76.04/12.02 % (441753)Termination reason: Refutation not found, incomplete strategy % 76.04/12.02 % (441753)Time elapsed: 0.109 s % 76.04/12.02 % (441753)Peak memory usage: 88 MB % 76.04/12.02 % (441753)Instructions burned: 304 (million) % 76.04/12.02 % (441757)ott+10_128_isp=bottom:to=lpo:sil=128000:si=on:urr=on:uwa=alasca_main:sac=on:slsq=on:random_seed=4070137713:i=17165:aac=none:doe=on:rtra=on:gtg=exists_all_2935 on theBenchmark for (2935ds/17165Mi) % 76.04/12.02 % (441758)lrs+2_10_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_main:tha=some:random_seed=3633750102:s2a=on:i=13094:s2at=-1:rtra=on_2934 on theBenchmark for (2934ds/13094Mi) % 76.04/12.02 % (441753)------------------------------ % 76.04/12.02 % (441753)------------------------------ % 76.04/12.02 % (441750)Instruction limit reached! % 76.04/12.02 % (441750)------------------------------ % 76.04/12.02 % (441750)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 76.04/12.02 % (441750)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 76.04/12.02 % (441750)CaDiCaL version: 2.1.3 % 76.04/12.02 % (441750)Termination reason: Instruction limit % 76.04/12.02 % (441750)Termination phase: Saturation % 76.04/12.02 % (441750)Time elapsed: 0.499 s % 76.04/12.02 % (441750)Peak memory usage: 116 MB % 76.04/12.02 % (441750)Instructions burned: 1265 (million) % 76.04/12.02 % (441762)dis+1011_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_frequency:lsd=20:nwc=3:random_seed=3775460334:i=1783:rtra=on:gtg=position_2932 on theBenchmark for (2932ds/1783Mi) % 76.04/12.02 % (441761)lrs+10_1_to=lpo:sil=128000:si=on:sp=occurrence:random_seed=4077700546:st=2:i=12633:rtra=on:ss=axioms_2932 on theBenchmark for (2932ds/12633Mi) % 76.04/12.02 % (441761)Refutation not found, incomplete strategy % 76.04/12.02 % (441761)------------------------------ % 76.04/12.02 % (441761)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 76.04/12.02 % (441761)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 76.04/12.02 % (441761)CaDiCaL version: 2.1.3 % 76.04/12.02 % (441761)Termination reason: Refutation not found, incomplete strategy % 76.04/12.02 % (441761)Time elapsed: 0.095 s % 76.04/12.02 % (441761)Peak memory usage: 88 MB % 76.04/12.02 % (441761)Instructions burned: 257 (million) % 76.04/12.02 % (441761)------------------------------ % 76.04/12.02 % (441761)------------------------------ % 76.04/12.02 % (441745)Instruction limit reached! % 76.04/12.02 % (441745)------------------------------ % 76.04/12.02 % (441745)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 76.04/12.02 % (441745)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 76.04/12.02 % (441745)CaDiCaL version: 2.1.3 % 76.04/12.02 % (441745)Termination reason: Instruction limit % 76.04/12.02 % (441745)Termination phase: Saturation % 76.04/12.02 % (441745)Time elapsed: 1.570 s % 76.04/12.02 % (441745)Peak memory usage: 134 MB % 76.04/12.02 % (441745)Instructions burned: 4093 (million) % 76.04/12.02 % (441765)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=1350542600:i=5451:aac=none:doe=on:nm=0:rtra=on:amm=off:gtg=position_2927 on theBenchmark for (2927ds/5451Mi) % 76.04/12.02 % (441766)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=3861613488:i=4975:doe=on:nm=0:rtra=on:gtg=exists_sym_2927 on theBenchmark for (2927ds/4975Mi) % 76.04/12.02 % (441762)Instruction limit reached! % 76.04/12.02 % (441762)------------------------------ % 76.04/12.02 % (441762)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 96.17/14.56 % (441762)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 96.17/14.56 % (441762)CaDiCaL version: 2.1.3 % 96.17/14.56 % (441762)Termination reason: Instruction limit % 96.17/14.56 % (441762)Termination phase: Saturation % 96.17/14.56 % (441762)Time elapsed: 0.670 s % 96.17/14.56 % (441762)Peak memory usage: 114 MB % 96.17/14.56 % (441762)Instructions burned: 1785 (million) % 96.17/14.56 % (441769)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=675097954:i=2076:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2924 on theBenchmark for (2924ds/2076Mi) % 96.17/14.56 % (441769)Instruction limit reached! % 96.17/14.56 % (441769)------------------------------ % 96.17/14.56 % (441769)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 96.17/14.56 % (441769)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 96.17/14.56 % (441769)CaDiCaL version: 2.1.3 % 96.17/14.56 % (441769)Termination reason: Instruction limit % 96.17/14.56 % (441769)Termination phase: Saturation % 96.17/14.56 % (441769)Time elapsed: 0.777 s % 96.17/14.56 % (441769)Peak memory usage: 116 MB % 96.17/14.56 % (441769)Instructions burned: 2076 (million) % 96.17/14.56 % (441771)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=3139263044:i=5145:rtra=on_2915 on theBenchmark for (2915ds/5145Mi) % 96.17/14.56 % (441765)Instruction limit reached! % 96.17/14.56 % (441765)------------------------------ % 96.17/14.56 % (441765)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 96.17/14.56 % (441765)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 96.17/14.56 % (441765)CaDiCaL version: 2.1.3 % 96.17/14.56 % (441765)Termination reason: Instruction limit % 96.17/14.56 % (441765)Termination phase: Saturation % 96.17/14.56 % (441765)Time elapsed: 2.087 s % 96.17/14.56 % (441765)Peak memory usage: 125 MB % 96.17/14.56 % (441765)Instructions burned: 5453 (million) % 96.17/14.56 % (441773)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=2728878610:i=3509:rtra=on_2905 on theBenchmark for (2905ds/3509Mi) % 96.17/14.56 % (441766)Instruction limit reached! % 96.17/14.56 % (441766)------------------------------ % 96.17/14.56 % (441766)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 96.17/14.56 % (441766)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 96.17/14.56 % (441766)CaDiCaL version: 2.1.3 % 96.17/14.56 % (441766)Termination reason: Instruction limit % 96.17/14.56 % (441766)Termination phase: Saturation % 96.17/14.56 % (441766)Time elapsed: 2.361 s % 96.17/14.56 % (441766)Peak memory usage: 165 MB % 96.17/14.56 % (441766)Instructions burned: 4975 (million) % 96.17/14.56 % (441775)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=423084680:st=2:i=13800:sd=12:ep=R:rtra=on:ss=axioms_2902 on theBenchmark for (2902ds/13800Mi) % 96.17/14.56 % (441775)Refutation not found, incomplete strategy % 96.17/14.56 % (441775)------------------------------ % 96.17/14.56 % (441775)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 96.17/14.56 % (441775)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 96.17/14.56 % (441775)CaDiCaL version: 2.1.3 % 96.17/14.56 % (441775)Termination reason: Refutation not found, incomplete strategy % 96.17/14.56 % (441775)Time elapsed: 0.103 s % 96.17/14.56 % (441775)Peak memory usage: 88 MB % 96.17/14.56 % (441775)Instructions burned: 289 (million) % 96.17/14.56 % (441775)------------------------------ % 96.17/14.56 % (441775)------------------------------ % 96.17/14.56 % (441777)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=87002294:i=1412:rtra=on:fsd=on:proc=on_2897 on theBenchmark for (2897ds/1412Mi) % 96.17/14.56 % (441771)Instruction limit reached! % 96.17/14.56 % (441771)------------------------------ % 96.17/14.56 % (441771)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 96.17/14.56 % (441771)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 96.17/14.56 % (441771)CaDiCaL version: 2.1.3 % 96.17/14.56 % (441771)Termination reason: Instruction limit % 96.17/14.56 % (441771)Termination phase: Saturation % 96.17/14.56 % (441771)Time elapsed: 1.875 s % 96.17/14.56 % (441771)Peak memory usage: 95 MB % 96.17/14.56 % (441771)Instructions burned: 5148 (million) % 96.17/14.56 % (441779)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 % 157.44/23.14 % (441779)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=3184484180:i=11747:aac=none:nm=0:rtra=on:rawr=on_2895 on theBenchmark for (2895ds/11747Mi) % 157.44/23.14 % (441777)Instruction limit reached! % 157.44/23.14 % (441777)------------------------------ % 157.44/23.14 % (441777)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 157.44/23.14 % (441777)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.44/23.14 % (441777)CaDiCaL version: 2.1.3 % 157.44/23.14 % (441777)Termination reason: Instruction limit % 157.44/23.14 % (441777)Termination phase: Saturation % 157.44/23.14 % (441777)Time elapsed: 0.543 s % 157.44/23.14 % (441777)Peak memory usage: 117 MB % 157.44/23.14 % (441777)Instructions burned: 1413 (million) % 157.44/23.14 % (441773)Instruction limit reached! % 157.44/23.14 % (441773)------------------------------ % 157.44/23.14 % (441773)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 157.44/23.14 % (441773)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.44/23.14 % (441773)CaDiCaL version: 2.1.3 % 157.44/23.14 % (441773)Termination reason: Instruction limit % 157.44/23.14 % (441773)Termination phase: Saturation % 157.44/23.14 % (441773)Time elapsed: 1.297 s % 157.44/23.14 % (441773)Peak memory usage: 94 MB % 157.44/23.14 % (441773)Instructions burned: 3511 (million) % 157.44/23.14 % (441749)Instruction limit reached! % 157.44/23.14 % (441749)------------------------------ % 157.44/23.14 % (441749)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 157.44/23.14 % (441749)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.44/23.14 % (441749)CaDiCaL version: 2.1.3 % 157.44/23.14 % (441749)Termination reason: Instruction limit % 157.44/23.14 % (441749)Termination phase: Saturation % 157.44/23.14 % (441749)Time elapsed: 4.842 s % 157.44/23.14 % (441749)Peak memory usage: 171 MB % 157.44/23.14 % (441749)Instructions burned: 10546 (million) % 157.44/23.14 % (441782)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=2780859451:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2890 on theBenchmark for (2890ds/3201Mi) % 157.44/23.14 % (441781)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=1193360702:s2a=on:i=3553:nm=0:rtra=on_2890 on theBenchmark for (2890ds/3553Mi) % 157.44/23.14 % (441719)Instruction limit reached! % 157.44/23.14 % (441719)------------------------------ % 157.44/23.14 % (441719)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 157.44/23.14 % (441719)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.44/23.14 % (441719)CaDiCaL version: 2.1.3 % 157.44/23.14 % (441719)Termination reason: Instruction limit % 157.44/23.14 % (441719)Termination phase: Saturation % 157.44/23.14 % (441719)Time elapsed: 7.347 s % 157.44/23.14 % (441719)Peak memory usage: 116 MB % 157.44/23.14 % (441719)Instructions burned: 36817 (million) % 157.44/23.14 % (441783)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=2106226553:thitd=on:cond=on:i=4081:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2890 on theBenchmark for (2890ds/4081Mi) % 157.44/23.14 % (441786)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=1372755000:cond=fast:i=20260:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2889 on theBenchmark for (2889ds/20260Mi) % 157.44/23.14 % (441786)Refutation not found, incomplete strategy % 157.44/23.14 % (441786)------------------------------ % 157.44/23.14 % (441786)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 157.44/23.14 % (441786)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.44/23.14 % (441786)CaDiCaL version: 2.1.3 % 157.44/23.14 % (441786)Termination reason: Refutation not found, incomplete strategy % 157.44/23.14 % (441786)Time elapsed: 0.043 s % 157.44/23.14 % (441786)Peak memory usage: 113 MB % 157.44/23.14 % (441786)Instructions burned: 147 (million) % 157.44/23.14 % (441786)------------------------------ % 157.44/23.14 % (441786)------------------------------ % 157.44/23.14 % (441758)Instruction limit reached! % 157.44/23.14 % (441758)------------------------------ % 157.44/23.14 % (441758)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 157.44/23.14 % (441758)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.44/23.14 % (441758)CaDiCaL version: 2.1.3 % 157.44/23.14 % (441758)Termination reason: Instruction limit % 171.66/25.13 % (441758)Termination phase: Saturation % 171.66/25.13 % (441758)Time elapsed: 4.700 s % 171.66/25.13 % (441758)Peak memory usage: 97 MB % 171.66/25.13 % (441758)Instructions burned: 13095 (million) % 171.66/25.13 % (441789)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=622841727:s2a=on:i=58627:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2886 on theBenchmark for (2886ds/58627Mi) % 171.66/25.13 % (441790)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=1289773897:avsq=on:i=6258:avsqr=1,16:rtra=on:rawr=on_2886 on theBenchmark for (2886ds/6258Mi) % 171.66/25.13 % (441782)Refutation not found, incomplete strategy % 171.66/25.13 % (441782)------------------------------ % 171.66/25.13 % (441782)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 171.66/25.13 % (441782)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 171.66/25.13 % (441782)CaDiCaL version: 2.1.3 % 171.66/25.13 % (441782)Termination reason: Refutation not found, incomplete strategy % 171.66/25.13 % (441782)Time elapsed: 0.688 s % 171.66/25.13 % (441782)Peak memory usage: 99 MB % 171.66/25.13 % (441782)Instructions burned: 1823 (million) % 171.66/25.13 % (441782)------------------------------ % 171.66/25.13 % (441782)------------------------------ % 171.66/25.13 % (441793)ott+10_128_isp=bottom:to=lpo:sil=128000:si=on:urr=on:uwa=alasca_main:sac=on:slsq=on:random_seed=2821198977:i=34001:aac=none:doe=on:rtra=on:gtg=exists_all_2880 on theBenchmark for (2880ds/34001Mi) % 171.66/25.13 % (441781)Instruction limit reached! % 171.66/25.13 % (441781)------------------------------ % 171.66/25.13 % (441781)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 171.66/25.13 % (441781)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 171.66/25.13 % (441781)CaDiCaL version: 2.1.3 % 171.66/25.13 % (441781)Termination reason: Instruction limit % 171.66/25.13 % (441781)Termination phase: Saturation % 171.66/25.13 % (441781)Time elapsed: 1.318 s % 171.66/25.13 % (441781)Peak memory usage: 95 MB % 171.66/25.13 % (441781)Instructions burned: 3553 (million) % 171.66/25.13 % (441796)lrs+2_10_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_main:tha=some:random_seed=2468397443:s2a=on:i=71622:s2at=-1:rtra=on_2876 on theBenchmark for (2876ds/71622Mi) % 171.66/25.13 % (441783)Instruction limit reached! % 171.66/25.13 % (441783)------------------------------ % 171.66/25.13 % (441783)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 171.66/25.13 % (441783)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 171.66/25.13 % (441783)CaDiCaL version: 2.1.3 % 171.66/25.13 % (441783)Termination reason: Instruction limit % 171.66/25.13 % (441783)Termination phase: Saturation % 171.66/25.13 % (441783)Time elapsed: 1.548 s % 171.66/25.13 % (441783)Peak memory usage: 136 MB % 171.66/25.13 % (441783)Instructions burned: 4082 (million) % 171.66/25.13 % (441888)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=2713538329:i=24001:kws=precedence:nm=0:rtra=on_2873 on theBenchmark for (2873ds/24001Mi) % 171.66/25.13 % (441757)Instruction limit reached! % 171.66/25.13 % (441757)------------------------------ % 171.66/25.13 % (441757)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 171.66/25.13 % (441757)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 171.66/25.13 % (441757)CaDiCaL version: 2.1.3 % 171.66/25.13 % (441757)Termination reason: Instruction limit % 171.66/25.13 % (441757)Termination phase: Saturation % 171.66/25.13 % (441757)Time elapsed: 6.365 s % 171.66/25.13 % (441757)Peak memory usage: 93 MB % 171.66/25.13 % (441757)Instructions burned: 17166 (million) % 171.66/25.13 % (441974)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=2968996586:i=2076:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2870 on theBenchmark for (2870ds/2076Mi) % 171.66/25.13 % (441790)Instruction limit reached! % 171.66/25.13 % (441790)------------------------------ % 171.66/25.13 % (441790)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 171.66/25.13 % (441790)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 171.66/25.13 % (441790)CaDiCaL version: 2.1.3 % 171.66/25.13 % (441790)Termination reason: Instruction limit % 171.66/25.13 % (441790)Termination phase: Saturation % 171.66/25.13 % (441790)Time elapsed: 2.330 s % 171.66/25.13 % (441790)Peak memory usage: 128 MB % 171.66/25.13 % (441790)Instructions burned: 6260 (million) % 171.66/25.13 % (441974)Instruction limit reached! % 171.66/25.13 % (441974)------------------------------ % 171.66/25.13 % (441974)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 178.00/26.06 % (441974)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 178.00/26.06 % (441974)CaDiCaL version: 2.1.3 % 178.00/26.06 % (441974)Termination reason: Instruction limit % 178.00/26.06 % (441974)Termination phase: Saturation % 178.00/26.06 % (441974)Time elapsed: 0.777 s % 178.00/26.06 % (441974)Peak memory usage: 116 MB % 178.00/26.06 % (441974)Instructions burned: 2077 (million) % 178.00/26.06 % (442160)dis+21_20_to=lakbo:si=on:alasca=on:sp=const_max:uwa=alasca_main:sac=on:random_seed=2638776644:s2a=on:i=83971:s2at=4:bd=all:ins=1:rtra=on_2861 on theBenchmark for (2861ds/83971Mi) % 178.00/26.06 % (442161)lrs+1011_5:1_to=lpo:sil=128000:sas=z3:si=on:norm_ineq=on:tha=some:random_seed=1045801740:i=83944:rtra=on_2861 on theBenchmark for (2861ds/83944Mi) % 178.00/26.06 % (441779)Instruction limit reached! % 178.00/26.06 % (441779)------------------------------ % 178.00/26.06 % (441779)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 178.00/26.06 % (441779)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 178.00/26.06 % (441779)CaDiCaL version: 2.1.3 % 178.00/26.06 % (441779)Termination reason: Instruction limit % 178.00/26.06 % (441779)Termination phase: Saturation % 178.00/26.06 % (441779)Time elapsed: 4.350 s % 178.00/26.06 % (441779)Peak memory usage: 126 MB % 178.00/26.06 % (441779)Instructions burned: 11747 (million) % 178.00/26.06 % (442164)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=3971283150:i=9201:rtra=on_2850 on theBenchmark for (2850ds/9201Mi) % 178.00/26.06 % (442164)Instruction limit reached! % 178.00/26.06 % (442164)------------------------------ % 178.00/26.06 % (442164)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 178.00/26.06 % (442164)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 178.00/26.06 % (442164)CaDiCaL version: 2.1.3 % 178.00/26.06 % (442164)Termination reason: Instruction limit % 178.00/26.06 % (442164)Termination phase: Saturation % 178.00/26.06 % (442164)Time elapsed: 3.371 s % 178.00/26.06 % (442164)Peak memory usage: 94 MB % 178.00/26.06 % (442164)Instructions burned: 9202 (million) % 178.00/26.06 % (442166)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 % 178.00/26.06 % (442166)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=1695181071:i=6806:aac=none:nm=0:rtra=on:rawr=on_2815 on theBenchmark for (2815ds/6806Mi) % 178.00/26.06 % (442166)Instruction limit reached! % 178.00/26.06 % (442166)------------------------------ % 178.00/26.06 % (442166)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 178.00/26.06 % (442166)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 178.00/26.06 % (442166)CaDiCaL version: 2.1.3 % 178.00/26.06 % (442166)Termination reason: Instruction limit % 178.00/26.06 % (442166)Termination phase: Saturation % 178.00/26.06 % (442166)Time elapsed: 2.501 s % 178.00/26.06 % (442166)Peak memory usage: 125 MB % 178.00/26.06 % (442166)Instructions burned: 6806 (million) % 178.00/26.06 % (442168)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=884209600:s2a=on:i=3553:nm=0:rtra=on_2789 on theBenchmark for (2789ds/3553Mi) % 178.00/26.06 % (441888)Instruction limit reached! % 178.00/26.06 % (441888)------------------------------ % 178.00/26.06 % (441888)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 178.00/26.06 % (441888)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 178.00/26.06 % (441888)CaDiCaL version: 2.1.3 % 178.00/26.06 % (441888)Termination reason: Instruction limit % 178.00/26.06 % (441888)Termination phase: Saturation % 178.00/26.06 % (441888)Time elapsed: 8.698 s % 178.00/26.06 % (441888)Peak memory usage: 144 MB % 178.00/26.06 % (441888)Instructions burned: 24001 (million) % 178.00/26.06 % (442170)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=1813064861:thitd=on:cond=on:i=2064:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2784 on theBenchmark for (2784ds/2064Mi) % 178.00/26.06 % (442170)Instruction limit reached! % 178.00/26.06 % (442170)------------------------------ % 178.00/26.06 % (442170)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 178.00/26.06 % (442170)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 178.00/26.06 % (442170)CaDiCaL version: 2.1.3 % 178.00/26.06 % (442170)Termination reason: Instruction limit % 182.00/26.65 % (442170)Termination phase: Saturation % 182.00/26.65 % (442170)Time elapsed: 0.795 s % 182.00/26.65 % (442170)Peak memory usage: 134 MB % 182.00/26.65 % (442170)Instructions burned: 2064 (million) % 182.00/26.65 % (442168)Instruction limit reached! % 182.00/26.65 % (442168)------------------------------ % 182.00/26.65 % (442168)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 182.00/26.65 % (442168)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 182.00/26.65 % (442168)CaDiCaL version: 2.1.3 % 182.00/26.65 % (442168)Termination reason: Instruction limit % 182.00/26.65 % (442168)Termination phase: Saturation % 182.00/26.65 % (442168)Time elapsed: 1.297 s % 182.00/26.65 % (442168)Peak memory usage: 93 MB % 182.00/26.65 % (442168)Instructions burned: 3555 (million) % 182.00/26.65 % (442172)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=1071348147:cond=fast:i=20260:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2775 on theBenchmark for (2775ds/20260Mi) % 182.00/26.65 % (442173)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=2620878800:avsq=on:i=1244:avsqr=1,16:rtra=on:rawr=on_2774 on theBenchmark for (2774ds/1244Mi) % 182.00/26.65 % (442172)Refutation not found, incomplete strategy % 182.00/26.65 % (442172)------------------------------ % 182.00/26.65 % (442172)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 182.00/26.65 % (442172)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 182.00/26.65 % (442172)CaDiCaL version: 2.1.3 % 182.00/26.65 % (442172)Termination reason: Refutation not found, incomplete strategy % 182.00/26.65 % (442172)Time elapsed: 0.080 s % 182.00/26.65 % (442172)Peak memory usage: 113 MB % 182.00/26.65 % (442172)Instructions burned: 147 (million) % 182.00/26.65 % (442172)------------------------------ % 182.00/26.65 % (442172)------------------------------ % 182.00/26.65 % (441789)Instruction limit reached! % 182.00/26.65 % (441789)------------------------------ % 182.00/26.65 % (441789)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 182.00/26.65 % (441789)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 182.00/26.65 % (441789)CaDiCaL version: 2.1.3 % 182.00/26.65 % (441789)Termination reason: Instruction limit % 182.00/26.65 % (441789)Termination phase: Saturation % 182.00/26.65 % (441789)Time elapsed: 11.612 s % 182.00/26.65 % (441789)Peak memory usage: 120 MB % 182.00/26.65 % (441789)Instructions burned: 58630 (million) % 182.00/26.65 % (442176)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=2562438324:i=58261:doe=on:nm=0:rtra=on:gtg=exists_sym_2770 on theBenchmark for (2770ds/58261Mi) % 182.00/26.65 % (442177)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 % 182.00/26.65 % (442177)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=3161316394:i=6806:aac=none:nm=0:rtra=on:rawr=on_2769 on theBenchmark for (2769ds/6806Mi) % 182.00/26.65 % (442173)Instruction limit reached! % 182.00/26.65 % (442173)------------------------------ % 182.00/26.65 % (442173)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 182.00/26.65 % (442173)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 182.00/26.65 % (442173)CaDiCaL version: 2.1.3 % 182.00/26.65 % (442173)Termination reason: Instruction limit % 182.00/26.65 % (442173)Termination phase: Saturation % 182.00/26.65 % (442173)Time elapsed: 0.482 s % 182.00/26.65 % (442173)Peak memory usage: 114 MB % 182.00/26.65 % (442173)Instructions burned: 1244 (million) % 182.00/26.65 % (442180)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=1345125411:thitd=on:cond=on:i=4081:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2768 on theBenchmark for (2768ds/4081Mi) % 182.00/26.65 % (442177)Instruction limit reached! % 182.00/26.65 % (442177)------------------------------ % 182.00/26.65 % (442177)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 182.00/26.65 % (442177)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 182.00/26.65 % (442177)CaDiCaL version: 2.1.3 % 182.00/26.65 % (442177)Termination reason: Instruction limit % 182.00/26.65 % (442177)Termination phase: Saturation % 182.00/26.65 % (442177)Time elapsed: 1.332 s % 186.27/27.28 % (442177)Peak memory usage: 125 MB % 186.27/27.28 % (442177)Instructions burned: 6810 (million) % 186.27/27.28 % (442182)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=3317781298:avsq=on:i=1701:avsqr=1,16:rtra=on:rawr=on_2755 on theBenchmark for (2755ds/1701Mi) % 186.27/27.28 % (442180)Instruction limit reached! % 186.27/27.28 % (442180)------------------------------ % 186.27/27.28 % (442180)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 186.27/27.28 % (442180)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 186.27/27.28 % (442180)CaDiCaL version: 2.1.3 % 186.27/27.28 % (442180)Termination reason: Instruction limit % 186.27/27.28 % (442180)Termination phase: Saturation % 186.27/27.28 % (442180)Time elapsed: 1.536 s % 186.27/27.28 % (442180)Peak memory usage: 135 MB % 186.27/27.28 % (442180)Instructions burned: 4082 (million) % 186.27/27.28 % (441793)Instruction limit reached! % 186.27/27.28 % (441793)------------------------------ % 186.27/27.28 % (441793)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 186.27/27.28 % (441793)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 186.27/27.28 % (441793)CaDiCaL version: 2.1.3 % 186.27/27.28 % (441793)Termination reason: Instruction limit % 186.27/27.28 % (441793)Termination phase: Saturation % 186.27/27.28 % (441793)Time elapsed: 12.717 s % 186.27/27.28 % (441793)Peak memory usage: 93 MB % 186.27/27.28 % (441793)Instructions burned: 34001 (million) % 186.27/27.28 % (442182)Instruction limit reached! % 186.27/27.28 % (442182)------------------------------ % 186.27/27.28 % (442182)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 186.27/27.28 % (442182)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 186.27/27.28 % (442182)CaDiCaL version: 2.1.3 % 186.27/27.28 % (442182)Termination reason: Instruction limit % 186.27/27.28 % (442182)Termination phase: Saturation % 186.27/27.28 % (442182)Time elapsed: 0.343 s % 186.27/27.28 % (442182)Peak memory usage: 114 MB % 186.27/27.28 % (442182)Instructions burned: 1705 (million) % 186.27/27.28 % (442185)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 % 186.27/27.28 % (442185)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=2964346367:i=8622:aac=none:nm=0:rtra=on:rawr=on_2751 on theBenchmark for (2751ds/8622Mi) % 186.27/27.28 % (442184)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=276883723:i=57001:doe=on:nm=0:rtra=on:gtg=exists_sym_2751 on theBenchmark for (2751ds/57001Mi) % 186.27/27.28 % (442186)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=981269345:i=24:doe=on:rtra=on:gtg=exists_top:ss=axioms_2751 on theBenchmark for (2751ds/24Mi) % 186.27/27.28 % (442186)Instruction limit reached! % 186.27/27.28 % (442186)------------------------------ % 186.27/27.28 % (442186)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 186.27/27.28 % (442186)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 186.27/27.28 % (442186)CaDiCaL version: 2.1.3 % 186.27/27.28 % (442186)Termination reason: Instruction limit % 186.27/27.28 % (442186)Termination phase: Property scanning % 186.27/27.28 % (442186)Time elapsed: 0.005 s % 186.27/27.28 % (442186)Peak memory usage: 85 MB % 186.27/27.28 % (442186)Instructions burned: 28 (million) % 186.27/27.28 % (442190)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=781368622:i=614:kws=precedence:nm=0:rtra=on_2750 on theBenchmark for (2750ds/614Mi) % 186.27/27.28 % (442190)Instruction limit reached! % 186.27/27.28 % (442190)------------------------------ % 186.27/27.28 % (442190)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 186.27/27.28 % (442190)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 186.27/27.28 % (442190)CaDiCaL version: 2.1.3 % 186.27/27.28 % (442190)Termination reason: Instruction limit % 186.27/27.28 % (442190)Termination phase: Saturation % 186.27/27.28 % (442190)Time elapsed: 0.134 s % 186.27/27.28 % (442190)Peak memory usage: 113 MB % 186.27/27.28 % (442190)Instructions burned: 620 (million) % 186.27/27.28 % (442192)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=722379927:i=402:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2747 on theBenchmark for (2747ds/402Mi) % 186.27/27.28 % (442192)Instruction limit reached! % 191.22/28.02 % (442192)------------------------------ % 191.22/28.02 % (442192)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 191.22/28.02 % (442192)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 191.22/28.02 % (442192)CaDiCaL version: 2.1.3 % 191.22/28.02 % (442192)Termination reason: Instruction limit % 191.22/28.02 % (442192)Termination phase: Property scanning % 191.22/28.02 % (442192)Time elapsed: 0.076 s % 191.22/28.02 % (442192)Peak memory usage: 86 MB % 191.22/28.02 % (442192)Instructions burned: 402 (million) % 191.22/28.02 % (442194)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=1254773721:s2a=on:i=14:rtra=on:inst=on_2746 on theBenchmark for (2746ds/14Mi) % 191.22/28.02 % (442194)Instruction limit reached! % 191.22/28.02 % (442194)------------------------------ % 191.22/28.02 % (442194)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 191.22/28.02 % (442194)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 191.22/28.02 % (442194)CaDiCaL version: 2.1.3 % 191.22/28.02 % (442194)Termination reason: Instruction limit % 191.22/28.02 % (442194)Termination phase: shuffling % 191.22/28.02 % (442194)Time elapsed: 0.004 s % 191.22/28.02 % (442194)Peak memory usage: 85 MB % 191.22/28.02 % (442194)Instructions burned: 19 (million) % 191.22/28.02 % (442196)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=4246628389:i=8:rtra=on_2745 on theBenchmark for (2745ds/8Mi) % 191.22/28.02 % (442196)Instruction limit reached! % 191.22/28.02 % (442196)------------------------------ % 191.22/28.02 % (442196)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 191.22/28.02 % (442196)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 191.22/28.02 % (442196)CaDiCaL version: 2.1.3 % 191.22/28.02 % (442196)Termination reason: Instruction limit % 191.22/28.02 % (442196)Termination phase: shuffling % 191.22/28.02 % (442196)Time elapsed: 0.002 s % 191.22/28.02 % (442196)Peak memory usage: 85 MB % 191.22/28.02 % (442196)Instructions burned: 8 (million) % 191.22/28.02 % (442198)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=3173138646:i=92:rtra=on_2744 on theBenchmark for (2744ds/92Mi) % 191.22/28.02 % (442198)Instruction limit reached! % 191.22/28.02 % (442198)------------------------------ % 191.22/28.02 % (442198)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 191.22/28.02 % (442198)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 191.22/28.02 % (442198)CaDiCaL version: 2.1.3 % 191.22/28.02 % (442198)Termination reason: Instruction limit % 191.22/28.02 % (442198)Termination phase: Property scanning % 191.22/28.02 % (442198)Time elapsed: 0.018 s % 191.22/28.02 % (442198)Peak memory usage: 86 MB % 191.22/28.02 % (442198)Instructions burned: 92 (million) % 191.22/28.02 % (442200)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=1641554305:i=66:rtra=on_2743 on theBenchmark for (2743ds/66Mi) % 191.22/28.02 % (442200)Instruction limit reached! % 191.22/28.02 % (442200)------------------------------ % 191.22/28.02 % (442200)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 191.22/28.02 % (442200)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 191.22/28.02 % (442200)CaDiCaL version: 2.1.3 % 191.22/28.02 % (442200)Termination reason: Instruction limit % 191.22/28.02 % (442200)Termination phase: Property scanning % 191.22/28.02 % (442200)Time elapsed: 0.014 s % 191.22/28.02 % (442200)Peak memory usage: 86 MB % 191.22/28.02 % (442200)Instructions burned: 72 (million) % 191.22/28.02 % (442202)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=1843785619:st=5:i=28:sd=10:rtra=on:ss=axioms:rawr=on_2742 on theBenchmark for (2742ds/28Mi) % 191.22/28.02 % (442202)Instruction limit reached! % 191.22/28.02 % (442202)------------------------------ % 191.22/28.02 % (442202)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 191.22/28.02 % (442202)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 191.22/28.02 % (442202)CaDiCaL version: 2.1.3 % 191.22/28.02 % (442202)Termination reason: Instruction limit % 191.22/28.02 % (442202)Termination phase: Property scanning % 191.22/28.02 % (442202)Time elapsed: 0.006 s % 191.22/28.02 % (442202)Peak memory usage: 86 MB % 191.22/28.02 % (442202)Instructions burned: 29 (million) % 191.22/28.02 % (442204)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=1212379093:i=58:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2741 on theBenchmark for (2741ds/58Mi) % 191.22/28.02 % (442204)Instruction limit reached! % 191.22/28.02 % (442204)------------------------------ % 196.13/28.68 % (442204)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 196.13/28.68 % (442204)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 196.13/28.68 % (442204)CaDiCaL version: 2.1.3 % 196.13/28.68 % (442204)Termination reason: Instruction limit % 196.13/28.68 % (442204)Termination phase: Property scanning % 196.13/28.68 % (442204)Time elapsed: 0.013 s % 196.13/28.68 % (442204)Peak memory usage: 86 MB % 196.13/28.68 % (442204)Instructions burned: 63 (million) % 196.13/28.68 % (442206)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=2881150371:cond=on:i=32:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2740 on theBenchmark for (2740ds/32Mi) % 196.13/28.68 % (442206)Instruction limit reached! % 196.13/28.68 % (442206)------------------------------ % 196.13/28.68 % (442206)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 196.13/28.68 % (442206)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 196.13/28.68 % (442206)CaDiCaL version: 2.1.3 % 196.13/28.68 % (442206)Termination reason: Instruction limit % 196.13/28.68 % (442206)Termination phase: Property scanning % 196.13/28.68 % (442206)Time elapsed: 0.007 s % 196.13/28.68 % (442206)Peak memory usage: 86 MB % 196.13/28.68 % (442206)Instructions burned: 35 (million) % 196.13/28.68 % (442208)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=373144688:i=48:canc=force:rtra=on_2739 on theBenchmark for (2739ds/48Mi) % 196.13/28.68 % (442208)Instruction limit reached! % 196.13/28.68 % (442208)------------------------------ % 196.13/28.68 % (442208)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 196.13/28.68 % (442208)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 196.13/28.68 % (442208)CaDiCaL version: 2.1.3 % 196.13/28.68 % (442208)Termination reason: Instruction limit % 196.13/28.68 % (442208)Termination phase: Property scanning % 196.13/28.68 % (442208)Time elapsed: 0.011 s % 196.13/28.68 % (442208)Peak memory usage: 86 MB % 196.13/28.68 % (442208)Instructions burned: 53 (million) % 196.13/28.68 % (442210)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=319990391:i=54:canc=cautious:fsr=off:rtra=on_2738 on theBenchmark for (2738ds/54Mi) % 196.13/28.68 % (442210)Instruction limit reached! % 196.13/28.68 % (442210)------------------------------ % 196.13/28.68 % (442210)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 196.13/28.68 % (442210)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 196.13/28.68 % (442210)CaDiCaL version: 2.1.3 % 196.13/28.68 % (442210)Termination reason: Instruction limit % 196.13/28.68 % (442210)Termination phase: Property scanning % 196.13/28.68 % (442210)Time elapsed: 0.012 s % 196.13/28.68 % (442210)Peak memory usage: 86 MB % 196.13/28.68 % (442210)Instructions burned: 57 (million) % 196.13/28.68 % (442212)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=3166691556:i=170:gtgl=4:rtra=on:gtg=exists_sym_2737 on theBenchmark for (2737ds/170Mi) % 196.13/28.68 % (442212)Instruction limit reached! % 196.13/28.68 % (442212)------------------------------ % 196.13/28.68 % (442212)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 196.13/28.68 % (442212)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 196.13/28.68 % (442212)CaDiCaL version: 2.1.3 % 196.13/28.68 % (442212)Termination reason: Instruction limit % 196.13/28.68 % (442212)Termination phase: Property scanning % 196.13/28.68 % (442212)Time elapsed: 0.033 s % 196.13/28.68 % (442212)Peak memory usage: 85 MB % 196.13/28.68 % (442212)Instructions burned: 176 (million) % 196.13/28.68 % (442214)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=4238953854:i=4:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2736 on theBenchmark for (2736ds/4Mi) % 196.13/28.68 % (442214)Instruction limit reached! % 196.13/28.68 % (442214)------------------------------ % 196.13/28.68 % (442214)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 196.13/28.68 % (442214)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 196.13/28.68 % (442214)CaDiCaL version: 2.1.3 % 196.13/28.68 % (442214)Termination reason: Instruction limit % 196.13/28.68 % (442214)Termination phase: shuffling % 196.13/28.68 % (442214)Time elapsed: 0.002 s % 196.13/28.68 % (442214)Peak memory usage: 85 MB % 196.13/28.68 % (442214)Instructions burned: 9 (million) % 196.13/28.68 % (442216)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=445620032:i=362:rtra=on:ss=axioms:ev=cautious_2735 on theBenchmark for (2735ds/362Mi) % 196.13/28.68 % (442216)Refutation not found, incomplete strategy % 200.28/29.28 % (442216)------------------------------ % 200.28/29.28 % (442216)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 200.28/29.28 % (442216)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 200.28/29.28 % (442216)CaDiCaL version: 2.1.3 % 200.28/29.28 % (442216)Termination reason: Refutation not found, incomplete strategy % 200.28/29.28 % (442216)Time elapsed: 0.033 s % 200.28/29.28 % (442216)Peak memory usage: 88 MB % 200.28/29.28 % (442216)Instructions burned: 173 (million) % 200.28/29.28 % (442216)------------------------------ % 200.28/29.28 % (442216)------------------------------ % 200.28/29.28 % (442218)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=70536786:i=8:ep=RST:ins=2:rtra=on_2732 on theBenchmark for (2732ds/8Mi) % 200.28/29.28 % (442218)Instruction limit reached! % 200.28/29.28 % (442218)------------------------------ % 200.28/29.28 % (442218)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 200.28/29.28 % (442218)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 200.28/29.28 % (442218)CaDiCaL version: 2.1.3 % 200.28/29.28 % (442218)Termination reason: Instruction limit % 200.28/29.28 % (442218)Termination phase: shuffling % 200.28/29.28 % (442218)Time elapsed: 0.002 s % 200.28/29.28 % (442218)Peak memory usage: 85 MB % 200.28/29.28 % (442218)Instructions burned: 9 (million) % 200.28/29.28 % (442220)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=2480656239:i=132:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2731 on theBenchmark for (2731ds/132Mi) % 200.28/29.28 % (442220)Instruction limit reached! % 200.28/29.28 % (442220)------------------------------ % 200.28/29.28 % (442220)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 200.28/29.28 % (442220)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 200.28/29.28 % (442220)CaDiCaL version: 2.1.3 % 200.28/29.28 % (442220)Termination reason: Instruction limit % 200.28/29.28 % (442220)Termination phase: Property scanning % 200.28/29.28 % (442220)Time elapsed: 0.027 s % 200.28/29.28 % (442220)Peak memory usage: 86 MB % 200.28/29.28 % (442220)Instructions burned: 136 (million) % 200.28/29.28 % (442222)lrs+10_1_thi=all:si=on:fd=off:random_seed=3280779271:i=106:rtra=on:gtg=all_2730 on theBenchmark for (2730ds/106Mi) % 200.28/29.28 % (442222)Instruction limit reached! % 200.28/29.28 % (442222)------------------------------ % 200.28/29.28 % (442222)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 200.28/29.28 % (442222)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 200.28/29.28 % (442222)CaDiCaL version: 2.1.3 % 200.28/29.28 % (442222)Termination reason: Instruction limit % 200.28/29.28 % (442222)Termination phase: shuffling % 200.28/29.28 % (442222)Time elapsed: 0.020 s % 200.28/29.28 % (442222)Peak memory usage: 85 MB % 200.28/29.28 % (442222)Instructions burned: 108 (million) % 200.28/29.28 % (442224)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=1692145267:i=16:ep=RST:nm=16:rtra=on:gtg=exists_top_2729 on theBenchmark for (2729ds/16Mi) % 200.28/29.28 % (442224)Instruction limit reached! % 200.28/29.28 % (442224)------------------------------ % 200.28/29.28 % (442224)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 200.28/29.28 % (442224)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 200.28/29.28 % (442224)CaDiCaL version: 2.1.3 % 200.28/29.28 % (442224)Termination reason: Instruction limit % 200.28/29.28 % (442224)Termination phase: Property scanning % 200.28/29.28 % (442224)Time elapsed: 0.004 s % 200.28/29.28 % (442224)Peak memory usage: 85 MB % 200.28/29.28 % (442224)Instructions burned: 20 (million) % 200.28/29.28 % (442226)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=2189361389:st=3:i=4:rtra=on:ss=axioms_2728 on theBenchmark for (2728ds/4Mi) % 200.28/29.28 % (442226)Instruction limit reached! % 200.28/29.28 % (442226)------------------------------ % 200.28/29.28 % (442226)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 200.28/29.28 % (442226)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 200.28/29.28 % (442226)CaDiCaL version: 2.1.3 % 200.28/29.28 % (442226)Termination reason: Instruction limit % 200.28/29.28 % (442226)Termination phase: shuffling % 200.28/29.28 % (442226)Time elapsed: 0.002 s % 200.28/29.28 % (442226)Peak memory usage: 85 MB % 200.28/29.28 % (442226)Instructions burned: 9 (million) % 200.28/29.28 % (442228)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=278746224:i=4:doe=on:canc=force:asg=cautious:rtra=on_2727 on theBenchmark for (2727ds/4Mi) % 205.44/30.03 % (442228)Instruction limit reached! % 205.44/30.03 % (442228)------------------------------ % 205.44/30.03 % (442228)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 205.44/30.03 % (442228)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 205.44/30.03 % (442228)CaDiCaL version: 2.1.3 % 205.44/30.03 % (442228)Termination reason: Instruction limit % 205.44/30.03 % (442228)Termination phase: shuffling % 205.44/30.03 % (442228)Time elapsed: 0.001 s % 205.44/30.03 % (442228)Peak memory usage: 85 MB % 205.44/30.03 % (442228)Instructions burned: 6 (million) % 205.44/30.03 % (442230)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=3763770823:i=254:doe=on:rtra=on_2726 on theBenchmark for (2726ds/254Mi) % 205.44/30.03 % (442230)Instruction limit reached! % 205.44/30.03 % (442230)------------------------------ % 205.44/30.03 % (442230)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 205.44/30.03 % (442230)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 205.44/30.03 % (442230)CaDiCaL version: 2.1.3 % 205.44/30.03 % (442230)Termination reason: Instruction limit % 205.44/30.03 % (442230)Termination phase: Property scanning % 205.44/30.03 % (442230)Time elapsed: 0.049 s % 205.44/30.03 % (442230)Peak memory usage: 86 MB % 205.44/30.03 % (442230)Instructions burned: 259 (million) % 205.44/30.03 % (442232)dis+10_1_si=on:random_seed=4289132110:i=20:ep=R:rtra=on_2725 on theBenchmark for (2725ds/20Mi) % 205.44/30.03 % (442232)Instruction limit reached! % 205.44/30.03 % (442232)------------------------------ % 205.44/30.03 % (442232)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 205.44/30.03 % (442232)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 205.44/30.03 % (442232)CaDiCaL version: 2.1.3 % 205.44/30.03 % (442232)Termination reason: Instruction limit % 205.44/30.03 % (442232)Termination phase: Property scanning % 205.44/30.03 % (442232)Time elapsed: 0.005 s % 205.44/30.03 % (442232)Peak memory usage: 86 MB % 205.44/30.03 % (442232)Instructions burned: 23 (million) % 205.44/30.03 % (442236)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=1824283674:i=52:canc=cautious:av=off:rtra=on_2724 on theBenchmark for (2724ds/52Mi) % 205.44/30.03 % (442236)Instruction limit reached! % 205.44/30.03 % (442236)------------------------------ % 205.44/30.03 % (442236)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 205.44/30.03 % (442236)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 205.44/30.03 % (442236)CaDiCaL version: 2.1.3 % 205.44/30.03 % (442236)Termination reason: Instruction limit % 205.44/30.03 % (442236)Termination phase: Property scanning % 205.44/30.03 % (442236)Time elapsed: 0.012 s % 205.44/30.03 % (442236)Peak memory usage: 85 MB % 205.44/30.03 % (442236)Instructions burned: 56 (million) % 205.44/30.03 % (442266)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=2860694246: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_2722 on theBenchmark for (2722ds/70Mi) % 205.44/30.03 % (442266)Instruction limit reached! % 205.44/30.03 % (442266)------------------------------ % 205.44/30.03 % (442266)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 205.44/30.03 % (442266)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 205.44/30.03 % (442266)CaDiCaL version: 2.1.3 % 205.44/30.03 % (442266)Termination reason: Instruction limit % 205.44/30.03 % (442266)Termination phase: Property scanning % 205.44/30.03 % (442266)Time elapsed: 0.015 s % 205.44/30.03 % (442266)Peak memory usage: 86 MB % 205.44/30.03 % (442266)Instructions burned: 73 (million) % 205.44/30.03 % (442302)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=1391966101:i=4:fsr=off:rtra=on:inst=on_2721 on theBenchmark for (2721ds/4Mi) % 205.44/30.03 % (442302)Instruction limit reached! % 205.44/30.03 % (442302)------------------------------ % 205.44/30.03 % (442302)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 205.44/30.03 % (442302)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 205.44/30.03 % (442302)CaDiCaL version: 2.1.3 % 205.44/30.03 % (442302)Termination reason: Instruction limit % 205.44/30.03 % (442302)Termination phase: shuffling % 205.44/30.03 % (442302)Time elapsed: 0.002 s % 205.44/30.03 % (442302)Peak memory usage: 85 MB % 205.44/30.03 % (442302)Instructions burned: 9 (million) % 205.44/30.03 % (442349)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=3063218131:s2a=on:i=16:kws=inv_precedence:doe=on:rtra=on_2720 on theBenchmark for (2720ds/16Mi) % 216.00/31.41 % (442349)Instruction limit reached! % 216.00/31.41 % (442349)------------------------------ % 216.00/31.41 % (442349)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 216.00/31.41 % (442349)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 216.00/31.41 % (442349)CaDiCaL version: 2.1.3 % 216.00/31.41 % (442349)Termination reason: Instruction limit % 216.00/31.41 % (442349)Termination phase: shuffling % 216.00/31.41 % (442349)Time elapsed: 0.004 s % 216.00/31.41 % (442349)Peak memory usage: 85 MB % 216.00/31.41 % (442349)Instructions burned: 17 (million) % 216.00/31.41 % (442374)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=2259154466:i=740:ep=RS:fsr=off:rtra=on_2719 on theBenchmark for (2719ds/740Mi) % 216.00/31.41 % (442185)Instruction limit reached! % 216.00/31.41 % (442185)------------------------------ % 216.00/31.41 % (442185)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 216.00/31.41 % (442185)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 216.00/31.41 % (442185)CaDiCaL version: 2.1.3 % 216.00/31.41 % (442185)Termination reason: Instruction limit % 216.00/31.41 % (442185)Termination phase: Saturation % 216.00/31.41 % (442185)Time elapsed: 3.264 s % 216.00/31.41 % (442185)Peak memory usage: 126 MB % 216.00/31.41 % (442185)Instructions burned: 8625 (million) % 216.00/31.41 % (442374)Refutation not found, incomplete strategy % 216.00/31.41 % (442374)------------------------------ % 216.00/31.41 % (442374)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 216.00/31.41 % (442374)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 216.00/31.41 % (442374)CaDiCaL version: 2.1.3 % 216.00/31.41 % (442374)Termination reason: Refutation not found, incomplete strategy % 216.00/31.41 % (442374)Time elapsed: 0.124 s % 216.00/31.41 % (442374)Peak memory usage: 89 MB % 216.00/31.41 % (442374)Instructions burned: 640 (million) % 216.00/31.41 % (442376)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=231519466:i=26:av=off:rtra=on:gtg=exists_sym:ev=force_2718 on theBenchmark for (2718ds/26Mi) % 216.00/31.41 % (442376)Instruction limit reached! % 216.00/31.41 % (442376)------------------------------ % 216.00/31.41 % (442376)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 216.00/31.41 % (442376)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 216.00/31.41 % (442376)CaDiCaL version: 2.1.3 % 216.00/31.41 % (442376)Termination reason: Instruction limit % 216.00/31.41 % (442376)Termination phase: Property scanning % 216.00/31.41 % (442376)Time elapsed: 0.011 s % 216.00/31.41 % (442376)Peak memory usage: 85 MB % 216.00/31.41 % (442376)Instructions burned: 26 (million) % 216.00/31.41 % (442374)------------------------------ % 216.00/31.41 % (442374)------------------------------ % 216.00/31.41 % (442384)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=3351840049:i=20:rtra=on_2716 on theBenchmark for (2716ds/20Mi) % 216.00/31.41 % (442384)Instruction limit reached! % 216.00/31.41 % (442384)------------------------------ % 216.00/31.41 % (442384)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 216.00/31.41 % (442384)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 216.00/31.41 % (442384)CaDiCaL version: 2.1.3 % 216.00/31.41 % (442384)Termination reason: Instruction limit % 216.00/31.41 % (442384)Termination phase: Property scanning % 216.00/31.41 % (442384)Time elapsed: 0.005 s % 216.00/31.41 % (442384)Peak memory usage: 86 MB % 216.00/31.41 % (442384)Instructions burned: 22 (million) % 216.00/31.41 % (442378)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=3280947675:i=452:rtra=on:gtg=position:ss=axioms_2716 on theBenchmark for (2716ds/452Mi) % 216.00/31.41 % (442418)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=85666954:i=142:rtra=on:gtg=exists_top_2715 on theBenchmark for (2715ds/142Mi) % 216.00/31.41 % (442418)Instruction limit reached! % 216.00/31.41 % (442418)------------------------------ % 216.00/31.41 % (442418)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 216.00/31.41 % (442418)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 216.00/31.41 % (442418)CaDiCaL version: 2.1.3 % 216.00/31.41 % (442418)Termination reason: Instruction limit % 216.00/31.41 % (442418)Termination phase: Property scanning % 216.00/31.41 % (442418)Time elapsed: 0.030 s % 216.00/31.41 % (442418)Peak memory usage: 86 MB % 216.00/31.41 % (442418)Instructions burned: 145 (million) % 216.00/31.41 % (442378)Refutation not found, incomplete strategy % 219.47/31.94 % (442378)------------------------------ % 219.47/31.94 % (442378)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 219.47/31.94 % (442378)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 219.47/31.94 % (442378)CaDiCaL version: 2.1.3 % 219.47/31.94 % (442378)Termination reason: Refutation not found, incomplete strategy % 219.47/31.94 % (442378)Time elapsed: 0.127 s % 219.47/31.94 % (442378)Peak memory usage: 112 MB % 219.47/31.94 % (442378)Instructions burned: 286 (million) % 219.47/31.94 % (442464)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=929514029:i=150:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2714 on theBenchmark for (2714ds/150Mi) % 219.47/31.94 % (442464)Instruction limit reached! % 219.47/31.94 % (442464)------------------------------ % 219.47/31.94 % (442464)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 219.47/31.94 % (442464)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 219.47/31.94 % (442464)CaDiCaL version: 2.1.3 % 219.47/31.94 % (442464)Termination reason: Instruction limit % 219.47/31.94 % (442464)Termination phase: Property scanning % 219.47/31.94 % (442464)Time elapsed: 0.031 s % 219.47/31.94 % (442464)Peak memory usage: 86 MB % 219.47/31.94 % (442464)Instructions burned: 157 (million) % 219.47/31.94 % (442491)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=2721763093:i=588:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2712 on theBenchmark for (2712ds/588Mi) % 219.47/31.94 % (442378)------------------------------ % 219.47/31.94 % (442378)------------------------------ % 219.47/31.94 % (442491)Instruction limit reached! % 219.47/31.94 % (442491)------------------------------ % 219.47/31.94 % (442491)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 219.47/31.94 % (442491)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 219.47/31.94 % (442491)CaDiCaL version: 2.1.3 % 219.47/31.94 % (442491)Termination reason: Instruction limit % 219.47/31.94 % (442491)Termination phase: Saturation % 219.47/31.94 % (442491)Time elapsed: 0.120 s % 219.47/31.94 % (442491)Peak memory usage: 96 MB % 219.47/31.94 % (442491)Instructions burned: 589 (million) % 219.47/31.94 % (442515)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=2805680773:i=260:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2711 on theBenchmark for (2711ds/260Mi) % 219.47/31.94 % (442529)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=248474807:i=262:rtra=on_2710 on theBenchmark for (2710ds/262Mi) % 219.47/31.94 % (442529)Instruction limit reached! % 219.47/31.94 % (442529)------------------------------ % 219.47/31.94 % (442529)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 219.47/31.94 % (442529)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 219.47/31.94 % (442529)CaDiCaL version: 2.1.3 % 219.47/31.94 % (442529)Termination reason: Instruction limit % 219.47/31.94 % (442529)Termination phase: Saturation % 219.47/31.94 % (442529)Time elapsed: 0.130 s % 219.47/31.94 % (442529)Peak memory usage: 128 MB % 219.47/31.94 % (442529)Instructions burned: 262 (million) % 219.47/31.94 % (442515)Instruction limit reached! % 219.47/31.94 % (442515)------------------------------ % 219.47/31.94 % (442515)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 219.47/31.94 % (442515)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 219.47/31.94 % (442515)CaDiCaL version: 2.1.3 % 219.47/31.94 % (442515)Termination reason: Instruction limit % 219.47/31.94 % (442515)Termination phase: Property scanning % 219.47/31.94 % (442515)Time elapsed: 0.188 s % 219.47/31.94 % (442515)Peak memory usage: 86 MB % 219.47/31.94 % (442515)Instructions burned: 260 (million) % 219.47/31.94 % (442586)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=1844668666:i=80:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2708 on theBenchmark for (2708ds/80Mi) % 219.47/31.94 % (442586)Instruction limit reached! % 219.47/31.94 % (442586)------------------------------ % 219.47/31.94 % (442586)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 219.47/31.94 % (442586)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 219.47/31.94 % (442586)CaDiCaL version: 2.1.3 % 219.47/31.94 % (442586)Termination reason: Instruction limit % 219.47/31.94 % (442586)Termination phase: Property scanning % 219.47/31.94 % (442586)Time elapsed: 0.031 s % 219.47/31.94 % (442586)Peak memory usage: 85 MB % 219.47/31.94 % (442586)Instructions burned: 80 (million) % 226.37/32.91 % (442592)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=2209764960:i=614:rtra=on:gtg=exists_top_2707 on theBenchmark for (2707ds/614Mi) % 226.37/32.91 % (442613)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=2724551118:s2a=on:i=1196:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2706 on theBenchmark for (2706ds/1196Mi) % 226.37/32.91 % (442592)Instruction limit reached! % 226.37/32.91 % (442592)------------------------------ % 226.37/32.91 % (442592)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 226.37/32.91 % (442592)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 226.37/32.91 % (442592)CaDiCaL version: 2.1.3 % 226.37/32.91 % (442592)Termination reason: Instruction limit % 226.37/32.91 % (442592)Termination phase: Saturation % 226.37/32.91 % (442592)Time elapsed: 0.460 s % 226.37/32.91 % (442592)Peak memory usage: 89 MB % 226.37/32.91 % (442592)Instructions burned: 614 (million) % 226.37/32.91 % (442613)Instruction limit reached! % 226.37/32.91 % (442613)------------------------------ % 226.37/32.91 % (442613)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 226.37/32.91 % (442613)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 226.37/32.91 % (442613)CaDiCaL version: 2.1.3 % 226.37/32.91 % (442613)Termination reason: Instruction limit % 226.37/32.91 % (442613)Termination phase: Saturation % 226.37/32.91 % (442613)Time elapsed: 0.455 s % 226.37/32.91 % (442613)Peak memory usage: 130 MB % 226.37/32.91 % (442613)Instructions burned: 1196 (million) % 226.37/32.91 % (442660)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=763230627:i=262:canc=cautious:fsr=off:rtra=on_2701 on theBenchmark for (2701ds/262Mi) % 226.37/32.91 % (442666)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=3089893929:s2pl=no:i=518:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2700 on theBenchmark for (2700ds/518Mi) % 226.37/32.91 % (442666)Refutation not found, incomplete strategy % 226.37/32.91 % (442666)------------------------------ % 226.37/32.91 % (442666)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 226.37/32.91 % (442666)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 226.37/32.91 % (442666)CaDiCaL version: 2.1.3 % 226.37/32.91 % (442666)Termination reason: Refutation not found, incomplete strategy % 226.37/32.91 % (442666)Time elapsed: 0.078 s % 226.37/32.91 % (442666)Peak memory usage: 112 MB % 226.37/32.91 % (442666)Instructions burned: 300 (million) % 226.37/32.91 % (442660)Instruction limit reached! % 226.37/32.91 % (442660)------------------------------ % 226.37/32.91 % (442660)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 226.37/32.91 % (442660)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 226.37/32.91 % (442660)CaDiCaL version: 2.1.3 % 226.37/32.91 % (442660)Termination reason: Instruction limit % 226.37/32.91 % (442660)Termination phase: Property scanning % 226.37/32.91 % (442660)Time elapsed: 0.156 s % 226.37/32.91 % (442660)Peak memory usage: 86 MB % 226.37/32.91 % (442660)Instructions burned: 265 (million) % 226.37/32.91 % (442666)------------------------------ % 226.37/32.91 % (442666)------------------------------ % 226.37/32.91 % (442688)dis+10_1_si=on:random_seed=3688297369:s2a=on:i=2000:rtra=on:gtg=exists_all_2697 on theBenchmark for (2697ds/2000Mi) % 226.37/32.91 % (442689)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=2819488191:i=766:fsr=off:rtra=on:ev=force_2696 on theBenchmark for (2696ds/766Mi) % 226.37/32.91 % (442689)Instruction limit reached! % 226.37/32.91 % (442689)------------------------------ % 226.37/32.91 % (442689)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 226.37/32.91 % (442689)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 226.37/32.91 % (442689)CaDiCaL version: 2.1.3 % 226.37/32.91 % (442689)Termination reason: Instruction limit % 226.37/32.91 % (442689)Termination phase: Saturation % 226.37/32.91 % (442689)Time elapsed: 0.152 s % 226.37/32.91 % (442689)Peak memory usage: 89 MB % 226.37/32.91 % (442689)Instructions burned: 767 (million) % 226.37/32.91 % (442759)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=4233033433:i=282:doe=on:rtra=on_2694 on theBenchmark for (2694ds/282Mi) % 226.37/32.91 % (442759)Instruction limit reached! % 226.37/32.91 % (442759)------------------------------ % 226.37/32.91 % (442759)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 226.37/32.91 % (442759)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 232.62/33.80 % (442759)CaDiCaL version: 2.1.3 % 232.62/33.80 % (442759)Termination reason: Instruction limit % 232.62/33.80 % (442759)Termination phase: Property scanning % 232.62/33.80 % (442759)Time elapsed: 0.054 s % 232.62/33.80 % (442759)Peak memory usage: 86 MB % 232.62/33.80 % (442759)Instructions burned: 287 (million) % 232.62/33.80 % (442795)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=1333759576:i=130:nm=16:rtra=on_2692 on theBenchmark for (2692ds/130Mi) % 232.62/33.80 % (442795)Instruction limit reached! % 232.62/33.80 % (442795)------------------------------ % 232.62/33.80 % (442795)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 232.62/33.80 % (442795)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 232.62/33.80 % (442795)CaDiCaL version: 2.1.3 % 232.62/33.80 % (442795)Termination reason: Instruction limit % 232.62/33.80 % (442795)Termination phase: Property scanning % 232.62/33.80 % (442795)Time elapsed: 0.026 s % 232.62/33.80 % (442795)Peak memory usage: 86 MB % 232.62/33.80 % (442795)Instructions burned: 133 (million) % 232.62/33.80 % (442801)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=684000332:i=242:nm=16:rtra=on_2691 on theBenchmark for (2691ds/242Mi) % 232.62/33.80 % (442801)Instruction limit reached! % 232.62/33.80 % (442801)------------------------------ % 232.62/33.80 % (442801)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 232.62/33.80 % (442801)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 232.62/33.80 % (442801)CaDiCaL version: 2.1.3 % 232.62/33.80 % (442801)Termination reason: Instruction limit % 232.62/33.80 % (442801)Termination phase: Property scanning % 232.62/33.80 % (442801)Time elapsed: 0.047 s % 232.62/33.80 % (442801)Peak memory usage: 86 MB % 232.62/33.80 % (442801)Instructions burned: 247 (million) % 232.62/33.80 % (442850)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=133120600:s2a=on:i=256:s2at=5:ins=3:rtra=on_2690 on theBenchmark for (2690ds/256Mi) % 232.62/33.80 % (442688)Instruction limit reached! % 232.62/33.80 % (442688)------------------------------ % 232.62/33.80 % (442688)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 232.62/33.80 % (442688)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 232.62/33.80 % (442688)CaDiCaL version: 2.1.3 % 232.62/33.80 % (442688)Termination reason: Instruction limit % 232.62/33.80 % (442688)Termination phase: Saturation % 232.62/33.80 % (442688)Time elapsed: 0.730 s % 232.62/33.80 % (442688)Peak memory usage: 96 MB % 232.62/33.80 % (442688)Instructions burned: 2003 (million) % 232.62/33.80 % (442850)Instruction limit reached! % 232.62/33.80 % (442850)------------------------------ % 232.62/33.80 % (442850)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 232.62/33.80 % (442850)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 232.62/33.80 % (442850)CaDiCaL version: 2.1.3 % 232.62/33.80 % (442850)Termination reason: Instruction limit % 232.62/33.80 % (442850)Termination phase: SInE selection % 232.62/33.80 % (442850)Time elapsed: 0.049 s % 232.62/33.80 % (442850)Peak memory usage: 86 MB % 232.62/33.80 % (442850)Instructions burned: 256 (million) % 232.62/33.80 % (442853)dis+1010_1_to=kbo:si=on:random_seed=2905105177:i=350:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2688 on theBenchmark for (2688ds/350Mi) % 232.62/33.80 % (442852)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=2823355949:i=78:ins=3:rtra=on_2688 on theBenchmark for (2688ds/78Mi) % 232.62/33.80 % (442852)Instruction limit reached! % 232.62/33.80 % (442852)------------------------------ % 232.62/33.80 % (442852)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 232.62/33.80 % (442852)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 232.62/33.80 % (442852)CaDiCaL version: 2.1.3 % 232.62/33.80 % (442852)Termination reason: Instruction limit % 232.62/33.80 % (442852)Termination phase: Property scanning % 232.62/33.80 % (442852)Time elapsed: 0.029 s % 232.62/33.80 % (442852)Peak memory usage: 86 MB % 232.62/33.80 % (442852)Instructions burned: 79 (million) % 232.62/33.80 % (442853)Instruction limit reached! % 232.62/33.80 % (442853)------------------------------ % 232.62/33.80 % (442853)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 232.62/33.80 % (442853)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 232.62/33.80 % (442853)CaDiCaL version: 2.1.3 % 232.62/33.80 % (442853)Termination reason: Instruction limit % 232.62/33.80 % (442853)Termination phase: Property scanning % 238.64/34.67 % (442853)Time elapsed: 0.067 s % 238.64/34.67 % (442853)Peak memory usage: 86 MB % 238.64/34.67 % (442853)Instructions burned: 356 (million) % 238.64/34.67 % (442857)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=1915528016:s2a=on:i=966:doe=on:nm=32:rtra=on_2687 on theBenchmark for (2687ds/966Mi) % 238.64/34.67 % (442856)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=2184362016:i=658:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2687 on theBenchmark for (2687ds/658Mi) % 238.64/34.67 % (442857)Instruction limit reached! % 238.64/34.67 % (442857)------------------------------ % 238.64/34.67 % (442857)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 238.64/34.67 % (442857)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.64/34.67 % (442857)CaDiCaL version: 2.1.3 % 238.64/34.67 % (442857)Termination reason: Instruction limit % 238.64/34.67 % (442857)Termination phase: Saturation % 238.64/34.67 % (442857)Time elapsed: 0.216 s % 238.64/34.67 % (442857)Peak memory usage: 132 MB % 238.64/34.67 % (442857)Instructions burned: 968 (million) % 238.64/34.67 % (442856)Instruction limit reached! % 238.64/34.67 % (442856)------------------------------ % 238.64/34.67 % (442856)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 238.64/34.67 % (442856)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.64/34.67 % (442856)CaDiCaL version: 2.1.3 % 238.64/34.67 % (442856)Termination reason: Instruction limit % 238.64/34.67 % (442856)Termination phase: Property scanning % 238.64/34.67 % (442856)Time elapsed: 0.238 s % 238.64/34.67 % (442856)Peak memory usage: 87 MB % 238.64/34.67 % (442856)Instructions burned: 659 (million) % 238.64/34.67 % (442860)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=529072135:thitd=on:i=430:nm=0:rtra=on:ev=force_2684 on theBenchmark for (2684ds/430Mi) % 238.64/34.67 % (442860)Instruction limit reached! % 238.64/34.67 % (442860)------------------------------ % 238.64/34.67 % (442860)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 238.64/34.67 % (442860)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.64/34.67 % (442860)CaDiCaL version: 2.1.3 % 238.64/34.67 % (442860)Termination reason: Instruction limit % 238.64/34.67 % (442860)Termination phase: Property scanning % 238.64/34.67 % (442860)Time elapsed: 0.081 s % 238.64/34.67 % (442860)Peak memory usage: 87 MB % 238.64/34.67 % (442860)Instructions burned: 435 (million) % 238.64/34.67 % (442861)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=472730739:i=698:rtra=on_2683 on theBenchmark for (2683ds/698Mi) % 238.64/34.67 % (442863)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=4193223864:st=2:i=590:rtra=on:ss=axioms_2682 on theBenchmark for (2682ds/590Mi) % 238.64/34.67 % (442863)Refutation not found, incomplete strategy % 238.64/34.67 % (442863)------------------------------ % 238.64/34.67 % (442863)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 238.64/34.67 % (442863)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.64/34.67 % (442863)CaDiCaL version: 2.1.3 % 238.64/34.67 % (442863)Termination reason: Refutation not found, incomplete strategy % 238.64/34.67 % (442863)Time elapsed: 0.054 s % 238.64/34.67 % (442863)Peak memory usage: 88 MB % 238.64/34.67 % (442863)Instructions burned: 289 (million) % 238.64/34.67 % (442863)------------------------------ % 238.64/34.67 % (442863)------------------------------ % 238.64/34.67 % (442861)Instruction limit reached! % 238.64/34.67 % (442861)------------------------------ % 238.64/34.67 % (442861)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 238.64/34.67 % (442861)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.64/34.67 % (442861)CaDiCaL version: 2.1.3 % 238.64/34.67 % (442861)Termination reason: Instruction limit % 238.64/34.67 % (442861)Termination phase: Saturation % 238.64/34.67 % (442861)Time elapsed: 0.282 s % 238.64/34.67 % (442861)Peak memory usage: 113 MB % 238.64/34.67 % (442861)Instructions burned: 699 (million) % 238.64/34.67 % (442866)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=3429994172:i=656:kws=inv_frequency:nm=20:rtra=on_2679 on theBenchmark for (2679ds/656Mi) % 238.64/34.67 % (442867)dis+1010_1_to=lpo:sil=128000:sas=z3:si=on:nwc=5:random_seed=1801988914:i=562:gtgl=2:rtra=on:gtg=all_2679 on theBenchmark for (2679ds/562Mi) % 238.64/34.67 % (442866)Instruction limit reached! % 238.64/34.67 % (442866)------------------------------ % 245.05/35.53 % (442866)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 245.05/35.53 % (442866)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 245.05/35.53 % (442866)CaDiCaL version: 2.1.3 % 245.05/35.53 % (442866)Termination reason: Instruction limit % 245.05/35.53 % (442866)Termination phase: Saturation % 245.05/35.53 % (442866)Time elapsed: 0.139 s % 245.05/35.53 % (442866)Peak memory usage: 112 MB % 245.05/35.53 % (442866)Instructions burned: 661 (million) % 245.05/35.53 % (442870)lrs+1010_1_to=kbo:sil=128000:si=on:sos=on:urr=on:uwa=alasca_main:random_seed=2376763134:i=968:doe=on:nm=0:av=off:rtra=on:ss=axioms_2677 on theBenchmark for (2677ds/968Mi) % 245.05/35.53 % (442867)Instruction limit reached! % 245.05/35.53 % (442867)------------------------------ % 245.05/35.53 % (442867)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 245.05/35.53 % (442867)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 245.05/35.53 % (442867)CaDiCaL version: 2.1.3 % 245.05/35.53 % (442867)Termination reason: Instruction limit % 245.05/35.53 % (442867)Termination phase: Property scanning % 245.05/35.53 % (442867)Time elapsed: 0.201 s % 245.05/35.53 % (442867)Peak memory usage: 86 MB % 245.05/35.53 % (442867)Instructions burned: 565 (million) % 245.05/35.53 % (442870)Refutation not found, incomplete strategy % 245.05/35.53 % (442870)------------------------------ % 245.05/35.53 % (442870)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 245.05/35.53 % (442870)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 245.05/35.53 % (442870)CaDiCaL version: 2.1.3 % 245.05/35.53 % (442870)Termination reason: Refutation not found, incomplete strategy % 245.05/35.53 % (442870)Time elapsed: 0.054 s % 245.05/35.53 % (442870)Peak memory usage: 88 MB % 245.05/35.53 % (442870)Instructions burned: 282 (million) % 245.05/35.53 % (442872)lrs+21_1_to=kbo:sil=128000:thi=neg_eq:si=on:random_seed=1521119830:i=642:canc=force:rtra=on:tac=axiom:ss=axioms:ev=force_2676 on theBenchmark for (2676ds/642Mi) % 245.05/35.53 % (442870)------------------------------ % 245.05/35.53 % (442870)------------------------------ % 245.05/35.53 % (442874)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=2945675963:i=832:rtra=on:gtg=position:ss=axioms_2674 on theBenchmark for (2674ds/832Mi) % 245.05/35.53 % (442872)Refutation not found, incomplete strategy % 245.05/35.53 % (442872)------------------------------ % 245.05/35.53 % (442872)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 245.05/35.53 % (442872)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 245.05/35.53 % (442872)CaDiCaL version: 2.1.3 % 245.05/35.53 % (442872)Termination reason: Refutation not found, incomplete strategy % 245.05/35.53 % (442872)Time elapsed: 0.125 s % 245.05/35.53 % (442872)Peak memory usage: 112 MB % 245.05/35.53 % (442872)Instructions burned: 286 (million) % 245.05/35.53 % (442874)Refutation not found, incomplete strategy % 245.05/35.53 % (442874)------------------------------ % 245.05/35.53 % (442874)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 245.05/35.53 % (442874)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 245.05/35.53 % (442874)CaDiCaL version: 2.1.3 % 245.05/35.53 % (442874)Termination reason: Refutation not found, incomplete strategy % 245.05/35.53 % (442874)Time elapsed: 0.067 s % 245.05/35.53 % (442874)Peak memory usage: 112 MB % 245.05/35.53 % (442874)Instructions burned: 286 (million) % 245.05/35.53 % (442874)------------------------------ % 245.05/35.53 % (442874)------------------------------ % 245.05/35.53 % (442872)------------------------------ % 245.05/35.53 % (442872)------------------------------ % 245.05/35.53 % (442876)lrs+1010_1_to=kbo:tgt=ground:fde=unused:sas=z3:si=on:sp=unary_frequency:gve=force:spb=goal:tha=off:random_seed=1190869213:i=942:thf=on:kws=precedence:rtra=on_2671 on theBenchmark for (2671ds/942Mi) % 245.05/35.53 % (442877)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=775750470:avsq=on:i=552:avsqr=1,2:rtra=on_2671 on theBenchmark for (2671ds/552Mi) % 245.05/35.53 % (442876)Instruction limit reached! % 245.05/35.53 % (442876)------------------------------ % 245.05/35.53 % (442876)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 245.05/35.53 % (442876)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 245.05/35.53 % (442876)CaDiCaL version: 2.1.3 % 245.05/35.53 % (442876)Termination reason: Instruction limit % 245.05/35.53 % (442876)Termination phase: Saturation % 245.05/35.53 % (442876)Time elapsed: 0.208 s % 257.23/37.26 % (442876)Peak memory usage: 115 MB % 257.23/37.26 % (442876)Instructions burned: 950 (million) % 257.23/37.26 % (442880)lrs+1010_2_to=kbo:sil=128000:tgt=ground:fde=unused:sas=z3:si=on:uwa=off:tha=off:nwc=1:random_seed=2469766270:i=750:kws=inv_arity_squared:rtra=on_2668 on theBenchmark for (2668ds/750Mi) % 257.23/37.26 % (442877)Instruction limit reached! % 257.23/37.26 % (442877)------------------------------ % 257.23/37.26 % (442877)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 257.23/37.26 % (442877)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 257.23/37.26 % (442877)CaDiCaL version: 2.1.3 % 257.23/37.26 % (442877)Termination reason: Instruction limit % 257.23/37.26 % (442877)Termination phase: Saturation % 257.23/37.26 % (442877)Time elapsed: 0.241 s % 257.23/37.26 % (442877)Peak memory usage: 129 MB % 257.23/37.26 % (442877)Instructions burned: 554 (million) % 257.23/37.26 % (442882)lrs+10_1_to=kbo:sil=128000:tgt=full:sas=z3:si=on:uwa=func_ext:slsqc=1:flr=on:slsq=on:random_seed=3835862974:i=774:bd=preordered:rtra=on:ss=axioms:sgt=8_2667 on theBenchmark for (2667ds/774Mi) % 257.23/37.26 % (442880)Instruction limit reached! % 257.23/37.26 % (442880)------------------------------ % 257.23/37.26 % (442880)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 257.23/37.26 % (442880)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 257.23/37.26 % (442880)CaDiCaL version: 2.1.3 % 257.23/37.26 % (442880)Termination reason: Instruction limit % 257.23/37.26 % (442880)Termination phase: Saturation % 257.23/37.26 % (442880)Time elapsed: 0.163 s % 257.23/37.26 % (442880)Peak memory usage: 115 MB % 257.23/37.26 % (442880)Instructions burned: 756 (million) % 257.23/37.26 % (442884)lrs+10_1_to=kbo:sil=128000:fde=none:si=on:norm_ineq=on:urr=on:nwc=0.5:random_seed=3866942189:i=1026:kws=frequency:bd=all:rtra=on:gtg=exists_all:ss=axioms:sgt=4_2666 on theBenchmark for (2666ds/1026Mi) % 257.23/37.26 % (442882)Refutation not found, incomplete strategy % 257.23/37.26 % (442882)------------------------------ % 257.23/37.26 % (442882)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 257.23/37.26 % (442882)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 257.23/37.26 % (442882)CaDiCaL version: 2.1.3 % 257.23/37.26 % (442882)Termination reason: Refutation not found, incomplete strategy % 257.23/37.26 % (442882)Time elapsed: 0.131 s % 257.23/37.26 % (442882)Peak memory usage: 112 MB % 257.23/37.26 % (442882)Instructions burned: 301 (million) % 257.23/37.26 % (442884)Instruction limit reached! % 257.23/37.26 % (442884)------------------------------ % 257.23/37.26 % (442884)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 257.23/37.26 % (442884)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 257.23/37.26 % (442884)CaDiCaL version: 2.1.3 % 257.23/37.26 % (442884)Termination reason: Instruction limit % 257.23/37.26 % (442884)Termination phase: Saturation % 257.23/37.26 % (442884)Time elapsed: 0.199 s % 257.23/37.26 % (442884)Peak memory usage: 92 MB % 257.23/37.26 % (442884)Instructions burned: 1028 (million) % 257.23/37.26 % (442882)------------------------------ % 257.23/37.26 % (442882)------------------------------ % 257.23/37.26 % (442886)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=166416878:i=668:rtra=on_2663 on theBenchmark for (2663ds/668Mi) % 257.23/37.26 % (442887)lrs+1010_1_to=kbo:sil=64000:sas=cadical:si=on:sos=on:bce=on:random_seed=4221235179:i=718:rtra=on:gtg=exists_top:ss=axioms_2662 on theBenchmark for (2662ds/718Mi) % 257.23/37.26 % (442886)Instruction limit reached! % 257.23/37.26 % (442886)------------------------------ % 257.23/37.26 % (442886)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 257.23/37.26 % (442886)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 257.23/37.26 % (442886)CaDiCaL version: 2.1.3 % 257.23/37.26 % (442886)Termination reason: Instruction limit % 257.23/37.26 % (442886)Termination phase: Saturation % 257.23/37.26 % (442886)Time elapsed: 0.159 s % 257.23/37.26 % (442886)Peak memory usage: 132 MB % 257.23/37.26 % (442886)Instructions burned: 674 (million) % 257.23/37.26 % (442887)Refutation not found, incomplete strategy % 257.23/37.26 % (442887)------------------------------ % 257.23/37.26 % (442887)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 257.23/37.26 % (442887)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 257.23/37.26 % (442887)CaDiCaL version: 2.1.3 % 257.23/37.26 % (442887)Termination reason: Refutation not found, incomplete strategy % 257.23/37.26 % (442887)Time elapsed: 0.141 s % 268.19/38.82 % (442887)Peak memory usage: 89 MB % 268.19/38.82 % (442887)Instructions burned: 396 (million) % 268.19/38.82 % (442890)dis+1010_1_to=lpo:sil=128000:thi=all:fde=unused:si=on:sp=reverse_arity:tha=off:random_seed=4066704034:i=682:gtgl=2:rtra=on:gtg=exists_sym:ev=force:fsd=on:fsdmm=1_2661 on theBenchmark for (2661ds/682Mi) % 268.19/38.82 % (442890)Instruction limit reached! % 268.19/38.82 % (442890)------------------------------ % 268.19/38.82 % (442890)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 268.19/38.82 % (442890)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 268.19/38.82 % (442890)CaDiCaL version: 2.1.3 % 268.19/38.82 % (442890)Termination reason: Instruction limit % 268.19/38.82 % (442890)Termination phase: Saturation % 268.19/38.82 % (442890)Time elapsed: 0.146 s % 268.19/38.82 % (442890)Peak memory usage: 113 MB % 268.19/38.82 % (442890)Instructions burned: 686 (million) % 268.19/38.82 % (442887)------------------------------ % 268.19/38.82 % (442887)------------------------------ % 268.19/38.82 % (442892)lrs-2_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_max:tha=off:random_seed=916319576:st=1.5:i=522:sd=1:kws=precedence:rtra=on:ss=axioms_2658 on theBenchmark for (2658ds/522Mi) % 268.19/38.82 % (442892)Refutation not found, incomplete strategy % 268.19/38.82 % (442892)------------------------------ % 268.19/38.82 % (442892)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 268.19/38.82 % (442892)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 268.19/38.82 % (442892)CaDiCaL version: 2.1.3 % 268.19/38.82 % (442892)Termination reason: Refutation not found, incomplete strategy % 268.19/38.82 % (442892)Time elapsed: 0.050 s % 268.19/38.82 % (442892)Peak memory usage: 112 MB % 268.19/38.82 % (442892)Instructions burned: 193 (million) % 268.19/38.82 % (442893)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=1594894104:s2pl=no:i=470:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2657 on theBenchmark for (2657ds/470Mi) % 268.19/38.82 % (442892)------------------------------ % 268.19/38.82 % (442892)------------------------------ % 268.19/38.82 % (442893)Refutation not found, incomplete strategy % 268.19/38.82 % (442893)------------------------------ % 268.19/38.82 % (442893)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 268.19/38.82 % (442893)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 268.19/38.82 % (442893)CaDiCaL version: 2.1.3 % 268.19/38.82 % (442893)Termination reason: Refutation not found, incomplete strategy % 268.19/38.82 % (442893)Time elapsed: 0.131 s % 268.19/38.82 % (442893)Peak memory usage: 112 MB % 268.19/38.82 % (442893)Instructions burned: 300 (million) % 268.19/38.82 % (442896)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=3215606365:i=546:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2655 on theBenchmark for (2655ds/546Mi) % 268.19/38.82 % (442896)Instruction limit reached! % 268.19/38.82 % (442896)------------------------------ % 268.19/38.82 % (442896)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 268.19/38.82 % (442896)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 268.19/38.82 % (442896)CaDiCaL version: 2.1.3 % 268.19/38.82 % (442896)Termination reason: Instruction limit % 268.19/38.82 % (442896)Termination phase: Saturation % 268.19/38.82 % (442896)Time elapsed: 0.103 s % 268.19/38.82 % (442896)Peak memory usage: 89 MB % 268.19/38.82 % (442896)Instructions burned: 547 (million) % 268.19/38.82 % (442898)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=1381933438:i=292:doe=on:rtra=on_2653 on theBenchmark for (2653ds/292Mi) % 268.19/38.82 % (442893)------------------------------ % 268.19/38.82 % (442893)------------------------------ % 268.19/38.82 % (442898)Instruction limit reached! % 268.19/38.82 % (442898)------------------------------ % 268.19/38.82 % (442898)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 268.19/38.82 % (442898)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 268.19/38.82 % (442898)CaDiCaL version: 2.1.3 % 268.19/38.82 % (442898)Termination reason: Instruction limit % 268.19/38.82 % (442898)Termination phase: Property scanning % 268.19/38.82 % (442898)Time elapsed: 0.056 s % 268.19/38.82 % (442898)Peak memory usage: 86 MB % 268.19/38.82 % (442898)Instructions burned: 294 (million) % 268.19/38.82 % (442901)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=360017150:avsq=on:i=552:avsqr=1,2:rtra=on_2652 on theBenchmark for (2652ds/552Mi) % 274.77/39.84 % (442900)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=243570794:i=8856:doe=on:fsr=off:rtra=on_2652 on theBenchmark for (2652ds/8856Mi) % 274.77/39.84 % (442901)Instruction limit reached! % 274.77/39.84 % (442901)------------------------------ % 274.77/39.84 % (442901)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 274.77/39.84 % (442901)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 274.77/39.84 % (442901)CaDiCaL version: 2.1.3 % 274.77/39.84 % (442901)Termination reason: Instruction limit % 274.77/39.84 % (442901)Termination phase: Saturation % 274.77/39.84 % (442901)Time elapsed: 0.131 s % 274.77/39.84 % (442901)Peak memory usage: 129 MB % 274.77/39.84 % (442901)Instructions burned: 555 (million) % 274.77/39.84 % (442904)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=2059650729:i=2104:rtra=on_2650 on theBenchmark for (2650ds/2104Mi) % 274.77/39.84 % (442904)Instruction limit reached! % 274.77/39.84 % (442904)------------------------------ % 274.77/39.84 % (442904)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 274.77/39.84 % (442904)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 274.77/39.84 % (442904)CaDiCaL version: 2.1.3 % 274.77/39.84 % (442904)Termination reason: Instruction limit % 274.77/39.84 % (442904)Termination phase: Saturation % 274.77/39.84 % (442904)Time elapsed: 0.408 s % 274.77/39.84 % (442904)Peak memory usage: 95 MB % 274.77/39.84 % (442904)Instructions burned: 2107 (million) % 274.77/39.84 % (442906)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=610961778:i=1310:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2645 on theBenchmark for (2645ds/1310Mi) % 274.77/39.84 % (442906)Instruction limit reached! % 274.77/39.84 % (442906)------------------------------ % 274.77/39.84 % (442906)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 274.77/39.84 % (442906)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 274.77/39.84 % (442906)CaDiCaL version: 2.1.3 % 274.77/39.84 % (442906)Termination reason: Instruction limit % 274.77/39.84 % (442906)Termination phase: Saturation % 274.77/39.84 % (442906)Time elapsed: 0.347 s % 274.77/39.84 % (442906)Peak memory usage: 102 MB % 274.77/39.84 % (442906)Instructions burned: 1312 (million) % 274.77/39.84 % (442908)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=2139645898:st=5:i=2108:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2640 on theBenchmark for (2640ds/2108Mi) % 274.77/39.84 % (442908)Refutation not found, incomplete strategy % 274.77/39.84 % (442908)------------------------------ % 274.77/39.84 % (442908)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 274.77/39.84 % (442908)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 274.77/39.84 % (442908)CaDiCaL version: 2.1.3 % 274.77/39.84 % (442908)Termination reason: Refutation not found, incomplete strategy % 274.77/39.84 % (442908)Time elapsed: 0.034 s % 274.77/39.84 % (442908)Peak memory usage: 88 MB % 274.77/39.84 % (442908)Instructions burned: 181 (million) % 274.77/39.84 % (442908)------------------------------ % 274.77/39.84 % (442908)------------------------------ % 274.77/39.84 % (442910)lrs-1002_1_to=kbo:sas=z3:si=on:norm_ineq=on:sos=on:tha=some:random_seed=2338513065:i=214:rtra=on_2638 on theBenchmark for (2638ds/214Mi) % 274.77/39.84 % (442910)Instruction limit reached! % 274.77/39.84 % (442910)------------------------------ % 274.77/39.84 % (442910)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 274.77/39.84 % (442910)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 274.77/39.84 % (442910)CaDiCaL version: 2.1.3 % 274.77/39.84 % (442910)Termination reason: Instruction limit % 274.77/39.84 % (442910)Termination phase: Property scanning % 274.77/39.84 % (442910)Time elapsed: 0.042 s % 274.77/39.84 % (442910)Peak memory usage: 86 MB % 274.77/39.84 % (442910)Instructions burned: 220 (million) % 274.77/39.84 % (442912)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=4233683983:s2a=on:i=900:doe=on:nm=32:rtra=on_2637 on theBenchmark for (2637ds/900Mi) % 274.77/39.84 % (442912)Instruction limit reached! % 274.77/39.84 % (442912)------------------------------ % 274.77/39.84 % (442912)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 274.77/39.84 % (442912)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 274.77/39.84 % (442912)CaDiCaL version: 2.1.3 % 274.77/39.84 % (442912)Termination reason: Instruction limit % 274.77/39.84 % (442912)Termination phase: Saturation % 281.18/40.78 % (442912)Time elapsed: 0.200 s % 281.18/40.78 % (442912)Peak memory usage: 130 MB % 281.18/40.78 % (442912)Instructions burned: 901 (million) % 281.18/40.78 % (442914)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 % 281.18/40.78 % (442914)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=270347480:i=2180:aac=none:nm=0:rtra=on:rawr=on_2634 on theBenchmark for (2634ds/2180Mi) % 281.18/40.78 % (442914)Instruction limit reached! % 281.18/40.78 % (442914)------------------------------ % 281.18/40.78 % (442914)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 281.18/40.78 % (442914)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 281.18/40.78 % (442914)CaDiCaL version: 2.1.3 % 281.18/40.78 % (442914)Termination reason: Instruction limit % 281.18/40.78 % (442914)Termination phase: Saturation % 281.18/40.78 % (442914)Time elapsed: 0.437 s % 281.18/40.78 % (442914)Peak memory usage: 122 MB % 281.18/40.78 % (442914)Instructions burned: 2183 (million) % 281.18/40.78 % (442916)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=3248486750:i=260:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2629 on theBenchmark for (2629ds/260Mi) % 281.18/40.78 % (442916)Instruction limit reached! % 281.18/40.78 % (442916)------------------------------ % 281.18/40.78 % (442916)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 281.18/40.78 % (442916)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 281.18/40.78 % (442916)CaDiCaL version: 2.1.3 % 281.18/40.78 % (442916)Termination reason: Instruction limit % 281.18/40.78 % (442916)Termination phase: Property scanning % 281.18/40.78 % (442916)Time elapsed: 0.050 s % 281.18/40.78 % (442916)Peak memory usage: 86 MB % 281.18/40.78 % (442916)Instructions burned: 260 (million) % 281.18/40.78 % (442918)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=2334124299:i=624:kws=inv_frequency:nm=20:rtra=on_2627 on theBenchmark for (2627ds/624Mi) % 281.18/40.78 % (442918)Instruction limit reached! % 281.18/40.78 % (442918)------------------------------ % 281.18/40.78 % (442918)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 281.18/40.78 % (442918)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 281.18/40.78 % (442918)CaDiCaL version: 2.1.3 % 281.18/40.78 % (442918)Termination reason: Instruction limit % 281.18/40.78 % (442918)Termination phase: Saturation % 281.18/40.78 % (442918)Time elapsed: 0.133 s % 281.18/40.78 % (442918)Peak memory usage: 112 MB % 281.18/40.78 % (442918)Instructions burned: 628 (million) % 281.18/40.78 % (442920)ott+10_1_to=kbo:sil=64000:si=on:sp=reverse_frequency:sos=on:random_seed=1353405621:i=982:doe=on:rtra=on:gtg=position_2625 on theBenchmark for (2625ds/982Mi) % 281.18/40.78 % (442920)Instruction limit reached! % 281.18/40.78 % (442920)------------------------------ % 281.18/40.78 % (442920)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 281.18/40.78 % (442920)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 281.18/40.78 % (442920)CaDiCaL version: 2.1.3 % 281.18/40.78 % (442920)Termination reason: Instruction limit % 281.18/40.78 % (442920)Termination phase: Saturation % 281.18/40.78 % (442920)Time elapsed: 0.192 s % 281.18/40.78 % (442920)Peak memory usage: 92 MB % 281.18/40.78 % (442920)Instructions burned: 985 (million) % 281.18/40.78 % (442922)ott+1011_4:1_to=lpo:sil=64000:si=on:spb=intro:random_seed=1278141026:s2a=on:i=1670:s2at=2:rtra=on_2622 on theBenchmark for (2622ds/1670Mi) % 281.18/40.78 % (442922)Instruction limit reached! % 281.18/40.78 % (442922)------------------------------ % 281.18/40.78 % (442922)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 281.18/40.78 % (442922)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 281.18/40.78 % (442922)CaDiCaL version: 2.1.3 % 281.18/40.78 % (442922)Termination reason: Instruction limit % 281.18/40.78 % (442922)Termination phase: Saturation % 281.18/40.78 % (442922)Time elapsed: 0.329 s % 281.18/40.78 % (442922)Peak memory usage: 93 MB % 281.18/40.78 % (442922)Instructions burned: 1675 (million) % 281.18/40.78 % (442900)Instruction limit reached! % 281.18/40.78 % (442900)------------------------------ % 281.18/40.78 % (442900)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 281.18/40.78 % (442900)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 281.18/40.78 % (442900)CaDiCaTerminated % 300.54/43.34 % Vampire exiting % 300.54/43.35 Terminated %------------------------------------------------------------------------------