%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWW622_2 : TPTP v9.3.1. Released v6.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % Computer : n002.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:30:58 PM UTC 2026 % Result : Timeout 300.55s 43.10s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWW622_2 : TPTP v9.3.1. Released v6.1.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.08/0.20 % Computer : n002.cluster.edu % 0.08/0.20 % Model : x86_64 x86_64 % 0.08/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.20 % Memory : 8046.5625MB % 0.08/0.20 % OS : Linux 6.8.0-71-generic % 0.08/0.20 % CPULimit : 300 % 0.08/0.20 % WCLimit : 300 % 0.08/0.20 % DateTime : Mon Sep 28 14:25:37 UTC 2026 % 0.08/0.20 % CPUTime : % 0.08/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.08/0.24 Running first-order theorem proving % 0.08/0.24 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 5.13/1.56 % (384304)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule. % 5.13/1.56 % (384434)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=1570898538:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi) % 5.13/1.56 % (384431)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=3172092788:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi) % 5.13/1.56 % (384431)Instruction limit reached! % 5.13/1.56 % (384431)------------------------------ % 5.13/1.56 % (384431)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.13/1.56 % (384431)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.13/1.56 % (384431)CaDiCaL version: 2.1.3 % 5.13/1.56 % (384431)Termination reason: Instruction limit % 5.13/1.56 % (384431)Termination phase: Preprocessing 2 % 5.13/1.56 % (384431)Time elapsed: 0.003 s % 5.13/1.56 % (384431)Peak memory usage: 86 MB % 5.13/1.56 % (384431)Instructions burned: 4 (million) % 5.13/1.56 % (384427)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=407183340:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi) % 5.13/1.56 % (384430)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=3993770711:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi) % 5.13/1.56 % (384428)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=551068717:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi) % 5.13/1.56 % (384429)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=3088923711:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi) % 5.13/1.56 % (384433)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=3583512982:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi) % 5.13/1.56 % (384430)Instruction limit reached! % 5.13/1.56 % (384430)------------------------------ % 5.13/1.56 % (384430)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.13/1.56 % (384430)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.13/1.56 % (384430)CaDiCaL version: 2.1.3 % 5.13/1.56 % (384430)Termination reason: Instruction limit % 5.13/1.56 % (384430)Termination phase: Preprocessing 3 % 5.13/1.56 % (384430)Time elapsed: 0.007 s % 5.13/1.56 % (384430)Peak memory usage: 86 MB % 5.13/1.56 % (384430)Instructions burned: 7 (million) % 5.13/1.56 % (384434)Instruction limit reached! % 5.13/1.56 % (384434)------------------------------ % 5.13/1.56 % (384434)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.13/1.56 % (384434)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.13/1.56 % (384434)CaDiCaL version: 2.1.3 % 5.13/1.56 % (384434)Termination reason: Instruction limit % 5.13/1.56 % (384434)Termination phase: Saturation % 5.13/1.56 % (384434)Time elapsed: 0.039 s % 5.13/1.56 % (384434)Peak memory usage: 117 MB % 5.13/1.56 % (384434)Instructions burned: 34 (million) % 5.13/1.56 % (384427)Instruction limit reached! % 5.13/1.56 % (384427)------------------------------ % 5.13/1.56 % (384427)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.13/1.56 % (384427)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.13/1.56 % (384427)CaDiCaL version: 2.1.3 % 5.13/1.56 % (384427)Termination reason: Instruction limit % 5.13/1.56 % (384427)Termination phase: Saturation % 5.13/1.56 % (384427)Time elapsed: 0.018 s % 5.13/1.56 % (384427)Peak memory usage: 92 MB % 5.13/1.56 % (384427)Instructions burned: 12 (million) % 5.13/1.56 % (384433)Instruction limit reached! % 5.13/1.56 % (384433)------------------------------ % 5.13/1.56 % (384433)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.13/1.56 % (384433)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.13/1.56 % (384433)CaDiCaL version: 2.1.3 % 5.13/1.56 % (384433)Termination reason: Instruction limit % 5.13/1.56 % (384433)Termination phase: Saturation % 5.13/1.56 % (384433)Time elapsed: 0.081 s % 5.13/1.56 % (384433)Peak memory usage: 116 MB % 5.13/1.56 % (384433)Instructions burned: 46 (million) % 5.13/1.56 % (384457)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=617666213:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2997 on theBenchmark for (2997ds/16Mi) % 5.13/1.56 % (384450)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=2603882731:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2997 on theBenchmark for (2997ds/14Mi) % 6.70/1.79 % (384457)Instruction limit reached! % 6.70/1.79 % (384457)------------------------------ % 6.70/1.79 % (384457)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.70/1.79 % (384457)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.70/1.79 % (384457)CaDiCaL version: 2.1.3 % 6.70/1.79 % (384457)Termination reason: Instruction limit % 6.70/1.79 % (384457)Termination phase: Saturation % 6.70/1.79 % (384457)Time elapsed: 0.010 s % 6.70/1.79 % (384457)Peak memory usage: 89 MB % 6.70/1.79 % (384457)Instructions burned: 17 (million) % 6.70/1.79 % (384450)Instruction limit reached! % 6.70/1.79 % (384450)------------------------------ % 6.70/1.79 % (384450)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.70/1.79 % (384450)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.70/1.79 % (384450)CaDiCaL version: 2.1.3 % 6.70/1.79 % (384450)Termination reason: Instruction limit % 6.70/1.79 % (384450)Termination phase: Saturation % 6.70/1.79 % (384450)Time elapsed: 0.016 s % 6.70/1.79 % (384450)Peak memory usage: 88 MB % 6.70/1.79 % (384450)Instructions burned: 14 (million) % 6.70/1.79 % (384429)Instruction limit reached! % 6.70/1.79 % (384429)------------------------------ % 6.70/1.79 % (384429)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.70/1.79 % (384429)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.70/1.79 % (384429)CaDiCaL version: 2.1.3 % 6.70/1.79 % (384429)Termination reason: Instruction limit % 6.70/1.79 % (384429)Termination phase: Saturation % 6.70/1.79 % (384429)Time elapsed: 0.258 s % 6.70/1.79 % (384429)Peak memory usage: 119 MB % 6.70/1.79 % (384429)Instructions burned: 201 (million) % 6.70/1.79 % (384456)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=1399212038:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2997 on theBenchmark for (2997ds/29Mi) % 6.70/1.79 % (384458)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=1993801617:i=24:canc=force:rtra=on_2997 on theBenchmark for (2997ds/24Mi) % 6.70/1.79 % (384458)Instruction limit reached! % 6.70/1.79 % (384458)------------------------------ % 6.70/1.79 % (384458)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.70/1.79 % (384458)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.70/1.79 % (384458)CaDiCaL version: 2.1.3 % 6.70/1.79 % (384458)Termination reason: Instruction limit % 6.70/1.79 % (384458)Termination phase: Saturation % 6.70/1.79 % (384458)Time elapsed: 0.026 s % 6.70/1.79 % (384458)Peak memory usage: 89 MB % 6.70/1.79 % (384458)Instructions burned: 24 (million) % 6.70/1.79 % (384456)Instruction limit reached! % 6.70/1.79 % (384456)------------------------------ % 6.70/1.79 % (384456)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.70/1.79 % (384456)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.70/1.79 % (384456)CaDiCaL version: 2.1.3 % 6.70/1.79 % (384456)Termination reason: Instruction limit % 6.70/1.79 % (384456)Termination phase: Saturation % 6.70/1.79 % (384456)Time elapsed: 0.035 s % 6.70/1.79 % (384456)Peak memory usage: 89 MB % 6.70/1.79 % (384456)Instructions burned: 29 (million) % 6.70/1.79 % (384428)Instruction limit reached! % 6.70/1.79 % (384428)------------------------------ % 6.70/1.79 % (384428)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.70/1.79 % (384428)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.70/1.79 % (384428)CaDiCaL version: 2.1.3 % 6.70/1.79 % (384428)Termination reason: Instruction limit % 6.70/1.79 % (384428)Termination phase: Saturation % 6.70/1.79 % (384428)Time elapsed: 0.332 s % 6.70/1.79 % (384428)Peak memory usage: 117 MB % 6.70/1.79 % (384428)Instructions burned: 307 (million) % 6.70/1.79 % (384459)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=568631264:i=27:canc=cautious:fsr=off:rtra=on_2996 on theBenchmark for (2996ds/27Mi) % 6.70/1.79 % (384459)Instruction limit reached! % 6.70/1.79 % (384459)------------------------------ % 6.70/1.79 % (384459)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.70/1.79 % (384459)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.70/1.79 % (384459)CaDiCaL version: 2.1.3 % 6.70/1.79 % (384459)Termination reason: Instruction limit % 6.70/1.79 % (384459)Termination phase: Saturation % 10.11/2.13 % (384459)Time elapsed: 0.029 s % 10.11/2.13 % (384459)Peak memory usage: 89 MB % 10.11/2.13 % (384459)Instructions burned: 28 (million) % 10.11/2.13 % (384462)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=3896404835:i=85:gtgl=4:rtra=on:gtg=exists_sym_2995 on theBenchmark for (2995ds/85Mi) % 10.11/2.13 % (384462)Instruction limit reached! % 10.11/2.13 % (384462)------------------------------ % 10.11/2.13 % (384462)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.11/2.13 % (384462)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.11/2.13 % (384462)CaDiCaL version: 2.1.3 % 10.11/2.13 % (384462)Termination reason: Instruction limit % 10.11/2.13 % (384462)Termination phase: Saturation % 10.11/2.13 % (384462)Time elapsed: 0.042 s % 10.11/2.13 % (384462)Peak memory usage: 89 MB % 10.11/2.13 % (384462)Instructions burned: 87 (million) % 10.11/2.13 % (384463)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=1428052872:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2995 on theBenchmark for (2995ds/2Mi) % 10.11/2.13 % (384463)Instruction limit reached! % 10.11/2.13 % (384463)------------------------------ % 10.11/2.13 % (384463)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.11/2.13 % (384463)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.11/2.13 % (384463)CaDiCaL version: 2.1.3 % 10.11/2.13 % (384463)Termination reason: Instruction limit % 10.11/2.13 % (384463)Termination phase: Property scanning % 10.11/2.13 % (384463)Time elapsed: 0.003 s % 10.11/2.13 % (384463)Peak memory usage: 85 MB % 10.11/2.13 % (384463)Instructions burned: 3 (million) % 10.11/2.13 % (384465)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=2043269300:i=181:rtra=on:ss=axioms:ev=cautious_2995 on theBenchmark for (2995ds/181Mi) % 10.11/2.13 % (384471)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=1343125187:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2994 on theBenchmark for (2994ds/66Mi) % 10.11/2.13 % (384477)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=1645748360:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2994 on theBenchmark for (2994ds/8Mi) % 10.11/2.13 % (384470)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=2266016024:i=4:ep=RST:ins=2:rtra=on_2994 on theBenchmark for (2994ds/4Mi) % 10.11/2.13 % (384470)Instruction limit reached! % 10.11/2.13 % (384470)------------------------------ % 10.11/2.13 % (384470)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.11/2.13 % (384470)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.11/2.13 % (384470)CaDiCaL version: 2.1.3 % 10.11/2.13 % (384470)Termination reason: Instruction limit % 10.11/2.13 % (384470)Termination phase: Preprocessing 2 % 10.11/2.13 % (384470)Time elapsed: 0.004 s % 10.11/2.13 % (384470)Peak memory usage: 86 MB % 10.11/2.13 % (384470)Instructions burned: 4 (million) % 10.11/2.13 % (384477)Instruction limit reached! % 10.11/2.13 % (384477)------------------------------ % 10.11/2.13 % (384477)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.11/2.13 % (384477)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.11/2.13 % (384477)CaDiCaL version: 2.1.3 % 10.11/2.13 % (384477)Termination reason: Instruction limit % 10.11/2.13 % (384477)Termination phase: Preprocessing 3 % 10.11/2.13 % (384477)Time elapsed: 0.007 s % 10.11/2.13 % (384477)Peak memory usage: 86 MB % 10.11/2.13 % (384477)Instructions burned: 8 (million) % 10.11/2.13 % (384474)lrs+10_1_thi=all:si=on:fd=off:random_seed=3291638576:i=53:rtra=on:gtg=all_2994 on theBenchmark for (2994ds/53Mi) % 10.11/2.13 % (384471)Instruction limit reached! % 10.11/2.13 % (384471)------------------------------ % 10.11/2.13 % (384471)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.11/2.13 % (384471)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.11/2.13 % (384471)CaDiCaL version: 2.1.3 % 10.11/2.13 % (384471)Termination reason: Instruction limit % 10.11/2.13 % (384471)Termination phase: Saturation % 10.11/2.13 % (384471)Time elapsed: 0.123 s % 10.11/2.13 % (384471)Peak memory usage: 134 MB % 10.11/2.13 % (384471)Instructions burned: 66 (million) % 10.11/2.13 % (384474)Instruction limit reached! % 10.11/2.13 % (384474)------------------------------ % 10.11/2.13 % (384474)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.11/2.13 % (384474)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.49/2.50 % (384474)CaDiCaL version: 2.1.3 % 11.49/2.50 % (384474)Termination reason: Instruction limit % 11.49/2.50 % (384474)Termination phase: Saturation % 11.49/2.50 % (384474)Time elapsed: 0.075 s % 11.49/2.50 % (384474)Peak memory usage: 117 MB % 11.49/2.50 % (384474)Instructions burned: 53 (million) % 11.49/2.50 % (384483)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=2976525788:st=3:i=2:rtra=on:ss=axioms_2993 on theBenchmark for (2993ds/2Mi) % 11.49/2.50 % (384483)Instruction limit reached! % 11.49/2.50 % (384483)------------------------------ % 11.49/2.50 % (384483)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.49/2.50 % (384483)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.49/2.50 % (384483)CaDiCaL version: 2.1.3 % 11.49/2.50 % (384483)Termination reason: Instruction limit % 11.49/2.50 % (384483)Termination phase: Property scanning % 11.49/2.50 % (384483)Time elapsed: 0.004 s % 11.49/2.50 % (384483)Peak memory usage: 86 MB % 11.49/2.50 % (384483)Instructions burned: 7 (million) % 11.49/2.50 % (384465)Instruction limit reached! % 11.49/2.50 % (384465)------------------------------ % 11.49/2.50 % (384465)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.49/2.50 % (384465)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.49/2.50 % (384465)CaDiCaL version: 2.1.3 % 11.49/2.50 % (384465)Termination reason: Instruction limit % 11.49/2.50 % (384465)Termination phase: Saturation % 11.49/2.50 % (384465)Time elapsed: 0.201 s % 11.49/2.50 % (384465)Peak memory usage: 91 MB % 11.49/2.50 % (384465)Instructions burned: 181 (million) % 11.49/2.50 % (384485)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=3561540019:i=2:doe=on:canc=force:asg=cautious:rtra=on_2992 on theBenchmark for (2992ds/2Mi) % 11.49/2.50 % (384485)Instruction limit reached! % 11.49/2.50 % (384485)------------------------------ % 11.49/2.50 % (384485)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.49/2.50 % (384485)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.49/2.50 % (384485)CaDiCaL version: 2.1.3 % 11.49/2.50 % (384485)Termination reason: Instruction limit % 11.49/2.50 % (384485)Termination phase: Preprocessing 3 % 11.49/2.50 % (384485)Time elapsed: 0.003 s % 11.49/2.50 % (384485)Peak memory usage: 86 MB % 11.49/2.50 % (384485)Instructions burned: 5 (million) % 11.49/2.50 % (384490)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=4050115313:i=127:doe=on:rtra=on_2992 on theBenchmark for (2992ds/127Mi) % 11.49/2.50 % (384491)dis+10_1_si=on:random_seed=2620545650:i=10:ep=R:rtra=on_2992 on theBenchmark for (2992ds/10Mi) % 11.49/2.50 % (384491)Instruction limit reached! % 11.49/2.50 % (384491)------------------------------ % 11.49/2.50 % (384491)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.49/2.50 % (384491)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.49/2.50 % (384491)CaDiCaL version: 2.1.3 % 11.49/2.50 % (384491)Termination reason: Instruction limit % 11.49/2.50 % (384491)Termination phase: Equality proxy % 11.49/2.50 % (384491)Time elapsed: 0.011 s % 11.49/2.50 % (384491)Peak memory usage: 86 MB % 11.49/2.50 % (384491)Instructions burned: 11 (million) % 11.49/2.50 % (384498)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=2686745351: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) % 11.49/2.50 % (384494)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=1256398367:i=26:canc=cautious:av=off:rtra=on_2991 on theBenchmark for (2991ds/26Mi) % 11.49/2.50 % (384498)Instruction limit reached! % 11.49/2.50 % (384498)------------------------------ % 11.49/2.50 % (384498)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.49/2.50 % (384498)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.49/2.50 % (384498)CaDiCaL version: 2.1.3 % 11.49/2.50 % (384498)Termination reason: Instruction limit % 11.49/2.50 % (384498)Termination phase: Saturation % 11.49/2.50 % (384498)Time elapsed: 0.022 s % 11.49/2.50 % (384498)Peak memory usage: 89 MB % 11.49/2.50 % (384498)Instructions burned: 35 (million) % 11.49/2.50 % (384494)Refutation not found, incomplete strategy % 11.49/2.50 % (384494)------------------------------ % 11.49/2.50 % (384494)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.49/2.50 % (384494)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.53/2.96 % (384494)CaDiCaL version: 2.1.3 % 13.53/2.96 % (384494)Termination reason: Refutation not found, incomplete strategy % 13.53/2.96 % (384494)Time elapsed: 0.021 s % 13.53/2.96 % (384494)Peak memory usage: 89 MB % 13.53/2.96 % (384494)Instructions burned: 19 (million) % 13.53/2.96 % (384499)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=2221117637:i=2:fsr=off:rtra=on:inst=on_2991 on theBenchmark for (2991ds/2Mi) % 13.53/2.96 % (384499)Instruction limit reached! % 13.53/2.96 % (384499)------------------------------ % 13.53/2.96 % (384499)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.53/2.96 % (384499)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.53/2.96 % (384499)CaDiCaL version: 2.1.3 % 13.53/2.96 % (384499)Termination reason: Instruction limit % 13.53/2.96 % (384499)Termination phase: Property scanning % 13.53/2.96 % (384499)Time elapsed: 0.003 s % 13.53/2.96 % (384499)Peak memory usage: 85 MB % 13.53/2.96 % (384499)Instructions burned: 3 (million) % 13.53/2.96 % (384502)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=979242231:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2990 on theBenchmark for (2990ds/8Mi) % 13.53/2.96 % (384506)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=4199988715:i=370:ep=RS:fsr=off:rtra=on_2990 on theBenchmark for (2990ds/370Mi) % 13.53/2.96 % (384502)Instruction limit reached! % 13.53/2.96 % (384502)------------------------------ % 13.53/2.96 % (384502)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.53/2.96 % (384502)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.53/2.96 % (384502)CaDiCaL version: 2.1.3 % 13.53/2.96 % (384502)Termination reason: Instruction limit % 13.53/2.96 % (384502)Termination phase: Property scanning % 13.53/2.96 % (384502)Time elapsed: 0.008 s % 13.53/2.96 % (384502)Peak memory usage: 86 MB % 13.53/2.96 % (384502)Instructions burned: 8 (million) % 13.53/2.96 % (384490)Instruction limit reached! % 13.53/2.96 % (384490)------------------------------ % 13.53/2.96 % (384490)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.53/2.96 % (384490)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.53/2.96 % (384490)CaDiCaL version: 2.1.3 % 13.53/2.96 % (384490)Termination reason: Instruction limit % 13.53/2.96 % (384490)Termination phase: Saturation % 13.53/2.96 % (384490)Time elapsed: 0.179 s % 13.53/2.96 % (384490)Peak memory usage: 117 MB % 13.53/2.96 % (384490)Instructions burned: 127 (million) % 13.53/2.96 % (384510)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=2230693943:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2989 on theBenchmark for (2989ds/13Mi) % 13.53/2.96 % (384510)Instruction limit reached! % 13.53/2.96 % (384510)------------------------------ % 13.53/2.96 % (384510)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.53/2.96 % (384510)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.53/2.96 % (384510)CaDiCaL version: 2.1.3 % 13.53/2.96 % (384510)Termination reason: Instruction limit % 13.53/2.96 % (384510)Termination phase: Saturation % 13.53/2.96 % (384510)Time elapsed: 0.007 s % 13.53/2.96 % (384510)Peak memory usage: 88 MB % 13.53/2.96 % (384510)Instructions burned: 13 (million) % 13.53/2.96 % (384513)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=4064845029:i=226:rtra=on:gtg=position:ss=axioms_2988 on theBenchmark for (2988ds/226Mi) % 13.53/2.96 % (384515)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=3684417679:i=10:rtra=on_2988 on theBenchmark for (2988ds/10Mi) % 13.53/2.96 % (384515)Instruction limit reached! % 13.53/2.96 % (384515)------------------------------ % 13.53/2.96 % (384515)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.53/2.96 % (384515)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.53/2.96 % (384515)CaDiCaL version: 2.1.3 % 13.53/2.96 % (384515)Termination reason: Instruction limit % 13.53/2.96 % (384515)Termination phase: Saturation % 13.53/2.96 % (384515)Time elapsed: 0.012 s % 13.53/2.96 % (384515)Peak memory usage: 88 MB % 13.53/2.96 % (384515)Instructions burned: 11 (million) % 13.53/2.96 % (384518)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=1379973806:i=71:rtra=on:gtg=exists_top_2987 on theBenchmark for (2987ds/71Mi) % 13.53/2.96 % (384521)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=1247324254:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2987 on theBenchmark for (2987ds/294Mi) % 18.16/3.37 % (384518)Instruction limit reached! % 18.16/3.37 % (384518)------------------------------ % 18.16/3.37 % (384518)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.16/3.37 % (384518)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.16/3.37 % (384518)CaDiCaL version: 2.1.3 % 18.16/3.37 % (384518)Termination reason: Instruction limit % 18.16/3.37 % (384518)Termination phase: Saturation % 18.16/3.37 % (384518)Time elapsed: 0.078 s % 18.16/3.37 % (384518)Peak memory usage: 133 MB % 18.16/3.37 % (384518)Instructions burned: 71 (million) % 18.16/3.37 % (384494)------------------------------ % 18.16/3.37 % (384494)------------------------------ % 18.16/3.37 % (384520)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=2584562607:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2987 on theBenchmark for (2987ds/75Mi) % 18.16/3.37 % (384506)Instruction limit reached! % 18.16/3.37 % (384506)------------------------------ % 18.16/3.37 % (384506)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.16/3.37 % (384506)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.16/3.37 % (384506)CaDiCaL version: 2.1.3 % 18.16/3.37 % (384506)Termination reason: Instruction limit % 18.16/3.37 % (384506)Termination phase: Saturation % 18.16/3.37 % (384506)Time elapsed: 0.365 s % 18.16/3.37 % (384506)Peak memory usage: 92 MB % 18.16/3.37 % (384506)Instructions burned: 370 (million) % 18.16/3.37 % (384520)Instruction limit reached! % 18.16/3.37 % (384520)------------------------------ % 18.16/3.37 % (384520)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.16/3.37 % (384520)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.16/3.37 % (384520)CaDiCaL version: 2.1.3 % 18.16/3.37 % (384520)Termination reason: Instruction limit % 18.16/3.37 % (384520)Termination phase: Saturation % 18.16/3.37 % (384520)Time elapsed: 0.088 s % 18.16/3.37 % (384520)Peak memory usage: 90 MB % 18.16/3.37 % (384520)Instructions burned: 76 (million) % 18.16/3.37 % (384529)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=2185882490:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2985 on theBenchmark for (2985ds/130Mi) % 18.16/3.37 % (384513)Instruction limit reached! % 18.16/3.37 % (384513)------------------------------ % 18.16/3.37 % (384513)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.16/3.37 % (384513)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.16/3.37 % (384513)CaDiCaL version: 2.1.3 % 18.16/3.37 % (384513)Termination reason: Instruction limit % 18.16/3.37 % (384513)Termination phase: Saturation % 18.16/3.37 % (384513)Time elapsed: 0.286 s % 18.16/3.37 % (384513)Peak memory usage: 118 MB % 18.16/3.37 % (384513)Instructions burned: 227 (million) % 18.16/3.37 % (384521)Instruction limit reached! % 18.16/3.37 % (384521)------------------------------ % 18.16/3.37 % (384521)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.16/3.37 % (384521)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.16/3.37 % (384521)CaDiCaL version: 2.1.3 % 18.16/3.37 % (384521)Termination reason: Instruction limit % 18.16/3.37 % (384521)Termination phase: Saturation % 18.16/3.37 % (384521)Time elapsed: 0.264 s % 18.16/3.37 % (384521)Peak memory usage: 91 MB % 18.16/3.37 % (384521)Instructions burned: 295 (million) % 18.16/3.37 % (384533)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=1783094939:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2984 on theBenchmark for (2984ds/40Mi) % 18.16/3.37 % (384531)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=1305371997:i=131:rtra=on_2985 on theBenchmark for (2985ds/131Mi) % 18.16/3.37 % (384534)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=2977180331:i=307:rtra=on:gtg=exists_top_2984 on theBenchmark for (2984ds/307Mi) % 18.16/3.37 % (384529)Instruction limit reached! % 18.16/3.37 % (384529)------------------------------ % 18.16/3.37 % (384529)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.16/3.37 % (384529)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.16/3.37 % (384529)CaDiCaL version: 2.1.3 % 18.16/3.37 % (384529)Termination reason: Instruction limit % 18.16/3.37 % (384529)Termination phase: Saturation % 18.16/3.37 % (384529)Time elapsed: 0.179 s % 19.38/3.87 % (384529)Peak memory usage: 117 MB % 19.38/3.87 % (384529)Instructions burned: 130 (million) % 19.38/3.87 % (384533)Instruction limit reached! % 19.38/3.87 % (384533)------------------------------ % 19.38/3.87 % (384533)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.38/3.87 % (384533)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.38/3.87 % (384533)CaDiCaL version: 2.1.3 % 19.38/3.87 % (384533)Termination reason: Instruction limit % 19.38/3.87 % (384533)Termination phase: Saturation % 19.38/3.87 % (384533)Time elapsed: 0.078 s % 19.38/3.87 % (384533)Peak memory usage: 134 MB % 19.38/3.87 % (384533)Instructions burned: 40 (million) % 19.38/3.87 % (384535)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=1808732674:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2984 on theBenchmark for (2984ds/598Mi) % 19.38/3.87 % (384534)Instruction limit reached! % 19.38/3.87 % (384534)------------------------------ % 19.38/3.87 % (384534)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.38/3.87 % (384534)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.38/3.87 % (384534)CaDiCaL version: 2.1.3 % 19.38/3.87 % (384534)Termination reason: Instruction limit % 19.38/3.87 % (384534)Termination phase: Saturation % 19.38/3.87 % (384534)Time elapsed: 0.163 s % 19.38/3.87 % (384534)Peak memory usage: 92 MB % 19.38/3.87 % (384534)Instructions burned: 308 (million) % 19.38/3.87 % (384537)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=1201020362:i=131:canc=cautious:fsr=off:rtra=on_2983 on theBenchmark for (2983ds/131Mi) % 19.38/3.87 % (384531)Instruction limit reached! % 19.38/3.87 % (384531)------------------------------ % 19.38/3.87 % (384531)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.38/3.87 % (384531)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.38/3.87 % (384531)CaDiCaL version: 2.1.3 % 19.38/3.87 % (384531)Termination reason: Instruction limit % 19.38/3.87 % (384531)Termination phase: Saturation % 19.38/3.87 % (384531)Time elapsed: 0.207 s % 19.38/3.87 % (384531)Peak memory usage: 134 MB % 19.38/3.87 % (384531)Instructions burned: 131 (million) % 19.38/3.87 % (384538)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=3641450200:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2982 on theBenchmark for (2982ds/259Mi) % 19.38/3.87 % (384545)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=2421854867:i=383:fsr=off:rtra=on:ev=force_2981 on theBenchmark for (2981ds/383Mi) % 19.38/3.87 % (384544)dis+10_1_si=on:random_seed=3227723402:s2a=on:i=1000:rtra=on:gtg=exists_all_2981 on theBenchmark for (2981ds/1000Mi) % 19.38/3.87 % (384537)Instruction limit reached! % 19.38/3.87 % (384537)------------------------------ % 19.38/3.87 % (384537)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.38/3.87 % (384537)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.38/3.87 % (384537)CaDiCaL version: 2.1.3 % 19.38/3.87 % (384537)Termination reason: Instruction limit % 19.38/3.87 % (384537)Termination phase: Saturation % 19.38/3.87 % (384537)Time elapsed: 0.168 s % 19.38/3.87 % (384537)Peak memory usage: 118 MB % 19.38/3.87 % (384537)Instructions burned: 131 (million) % 19.38/3.87 % (384547)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=737557991:i=141:doe=on:rtra=on_2980 on theBenchmark for (2980ds/141Mi) % 19.38/3.87 % (384549)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=3965385136:i=65:nm=16:rtra=on_2980 on theBenchmark for (2980ds/65Mi) % 19.38/3.87 % (384547)Instruction limit reached! % 19.38/3.87 % (384547)------------------------------ % 19.38/3.87 % (384547)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.38/3.87 % (384547)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.38/3.87 % (384547)CaDiCaL version: 2.1.3 % 19.38/3.87 % (384547)Termination reason: Instruction limit % 19.38/3.87 % (384547)Termination phase: Saturation % 19.38/3.87 % (384547)Time elapsed: 0.105 s % 19.38/3.87 % (384547)Peak memory usage: 91 MB % 19.38/3.87 % (384547)Instructions burned: 141 (million) % 19.38/3.87 % (384538)Instruction limit reached! % 19.38/3.87 % (384538)------------------------------ % 19.38/3.87 % (384538)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.38/3.87 % (384538)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.60/4.47 % (384538)CaDiCaL version: 2.1.3 % 25.60/4.47 % (384538)Termination reason: Instruction limit % 25.60/4.47 % (384538)Termination phase: Saturation % 25.60/4.47 % (384538)Time elapsed: 0.298 s % 25.60/4.47 % (384538)Peak memory usage: 118 MB % 25.60/4.47 % (384538)Instructions burned: 259 (million) % 25.60/4.47 % (384549)Instruction limit reached! % 25.60/4.47 % (384549)------------------------------ % 25.60/4.47 % (384549)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.60/4.47 % (384549)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.60/4.47 % (384549)CaDiCaL version: 2.1.3 % 25.60/4.47 % (384549)Termination reason: Instruction limit % 25.60/4.47 % (384549)Termination phase: Saturation % 25.60/4.47 % (384549)Time elapsed: 0.099 s % 25.60/4.47 % (384549)Peak memory usage: 116 MB % 25.60/4.47 % (384549)Instructions burned: 65 (million) % 25.60/4.47 % (384555)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=2093163554:i=121:nm=16:rtra=on_2978 on theBenchmark for (2978ds/121Mi) % 25.60/4.47 % (384545)Instruction limit reached! % 25.60/4.47 % (384545)------------------------------ % 25.60/4.47 % (384545)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.60/4.47 % (384545)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.60/4.47 % (384545)CaDiCaL version: 2.1.3 % 25.60/4.47 % (384545)Termination reason: Instruction limit % 25.60/4.47 % (384545)Termination phase: Saturation % 25.60/4.47 % (384545)Time elapsed: 0.365 s % 25.60/4.47 % (384545)Peak memory usage: 92 MB % 25.60/4.47 % (384545)Instructions burned: 383 (million) % 25.60/4.47 % (384535)Instruction limit reached! % 25.60/4.47 % (384535)------------------------------ % 25.60/4.47 % (384535)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.60/4.47 % (384535)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.60/4.47 % (384535)CaDiCaL version: 2.1.3 % 25.60/4.47 % (384535)Termination reason: Instruction limit % 25.60/4.47 % (384535)Termination phase: Saturation % 25.60/4.47 % (384535)Time elapsed: 0.597 s % 25.60/4.47 % (384535)Peak memory usage: 143 MB % 25.60/4.47 % (384535)Instructions burned: 598 (million) % 25.60/4.47 % (384558)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=3456121766:s2a=on:i=128:s2at=5:ins=3:rtra=on_2977 on theBenchmark for (2977ds/128Mi) % 25.60/4.47 % (384555)Instruction limit reached! % 25.60/4.47 % (384555)------------------------------ % 25.60/4.47 % (384555)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.60/4.47 % (384555)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.60/4.47 % (384555)CaDiCaL version: 2.1.3 % 25.60/4.47 % (384555)Termination reason: Instruction limit % 25.60/4.47 % (384555)Termination phase: Saturation % 25.60/4.47 % (384555)Time elapsed: 0.131 s % 25.60/4.47 % (384555)Peak memory usage: 90 MB % 25.60/4.47 % (384555)Instructions burned: 121 (million) % 25.60/4.47 % (384559)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=1413483832:i=39:ins=3:rtra=on_2977 on theBenchmark for (2977ds/39Mi) % 25.60/4.47 % (384558)Instruction limit reached! % 25.60/4.47 % (384558)------------------------------ % 25.60/4.47 % (384558)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.60/4.47 % (384558)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.60/4.47 % (384558)CaDiCaL version: 2.1.3 % 25.60/4.47 % (384558)Termination reason: Instruction limit % 25.60/4.47 % (384558)Termination phase: Saturation % 25.60/4.47 % (384558)Time elapsed: 0.095 s % 25.60/4.47 % (384558)Peak memory usage: 119 MB % 25.60/4.47 % (384558)Instructions burned: 128 (million) % 25.60/4.47 % (384559)Instruction limit reached! % 25.60/4.47 % (384559)------------------------------ % 25.60/4.47 % (384559)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.60/4.47 % (384559)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.60/4.47 % (384559)CaDiCaL version: 2.1.3 % 25.60/4.47 % (384559)Termination reason: Instruction limit % 25.60/4.47 % (384559)Termination phase: Saturation % 25.60/4.47 % (384559)Time elapsed: 0.073 s % 25.60/4.47 % (384559)Peak memory usage: 117 MB % 25.60/4.47 % (384559)Instructions burned: 39 (million) % 25.60/4.47 % (384560)dis+1010_1_to=kbo:si=on:random_seed=870340558:i=175:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2976 on theBenchmark for (2976ds/175Mi) % 25.60/4.47 % (384562)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=234820176:i=329:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2975 on theBenchmark for (2975ds/329Mi) % 27.56/4.97 % (384565)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=2389804561:thitd=on:i=215:nm=0:rtra=on:ev=force_2974 on theBenchmark for (2974ds/215Mi) % 27.56/4.97 % (384564)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=3554972101:s2a=on:i=483:doe=on:nm=32:rtra=on_2975 on theBenchmark for (2975ds/483Mi) % 27.56/4.97 % (384560)Instruction limit reached! % 27.56/4.97 % (384560)------------------------------ % 27.56/4.97 % (384560)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.56/4.97 % (384560)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.56/4.97 % (384560)CaDiCaL version: 2.1.3 % 27.56/4.97 % (384560)Termination reason: Instruction limit % 27.56/4.97 % (384560)Termination phase: Saturation % 27.56/4.97 % (384560)Time elapsed: 0.202 s % 27.56/4.97 % (384560)Peak memory usage: 91 MB % 27.56/4.97 % (384560)Instructions burned: 175 (million) % 27.56/4.97 % (384565)Instruction limit reached! % 27.56/4.97 % (384565)------------------------------ % 27.56/4.97 % (384565)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.56/4.97 % (384565)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.56/4.97 % (384565)CaDiCaL version: 2.1.3 % 27.56/4.97 % (384565)Termination reason: Instruction limit % 27.56/4.97 % (384565)Termination phase: Saturation % 27.56/4.97 % (384565)Time elapsed: 0.148 s % 27.56/4.97 % (384565)Peak memory usage: 135 MB % 27.56/4.97 % (384565)Instructions burned: 215 (million) % 27.56/4.97 % (384567)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=1806677553:i=349:rtra=on_2974 on theBenchmark for (2974ds/349Mi) % 27.56/4.97 % (384569)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=623176808:st=2:i=295:rtra=on:ss=axioms_2973 on theBenchmark for (2973ds/295Mi) % 27.56/4.97 % (384567)Instruction limit reached! % 27.56/4.97 % (384567)------------------------------ % 27.56/4.97 % (384567)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.56/4.97 % (384567)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.56/4.97 % (384562)Instruction limit reached! % 27.56/4.97 % (384562)------------------------------ % 27.56/4.97 % (384562)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.56/4.97 % (384562)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.56/4.97 % (384562)CaDiCaL version: 2.1.3 % 27.56/4.97 % (384562)Termination reason: Instruction limit % 27.56/4.97 % (384562)Termination phase: Saturation % 27.56/4.97 % (384562)Time elapsed: 0.387 s % 27.56/4.97 % (384562)Peak memory usage: 119 MB % 27.56/4.97 % (384562)Instructions burned: 329 (million) % 27.56/4.97 % (384567)CaDiCaL version: 2.1.3 % 27.56/4.97 % (384567)Termination reason: Instruction limit % 27.56/4.97 % (384567)Termination phase: Saturation % 27.56/4.97 % (384567)Time elapsed: 0.223 s % 27.56/4.97 % (384567)Peak memory usage: 116 MB % 27.56/4.97 % (384567)Instructions burned: 349 (million) % 27.56/4.97 % (384575)dis+1010_1_to=lpo:sil=128000:sas=z3:si=on:nwc=5:random_seed=2109673288:i=281:gtgl=2:rtra=on:gtg=all_2971 on theBenchmark for (2971ds/281Mi) % 27.56/4.97 % (384573)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=1762990192:i=328:kws=inv_frequency:nm=20:rtra=on_2971 on theBenchmark for (2971ds/328Mi) % 27.56/4.97 % (384544)Instruction limit reached! % 27.56/4.97 % (384544)------------------------------ % 27.56/4.97 % (384544)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.56/4.97 % (384544)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.56/4.97 % (384544)CaDiCaL version: 2.1.3 % 27.56/4.97 % (384544)Termination reason: Instruction limit % 27.56/4.97 % (384544)Termination phase: Saturation % 27.56/4.97 % (384544)Time elapsed: 1.016 s % 27.56/4.97 % (384544)Peak memory usage: 95 MB % 27.56/4.97 % (384544)Instructions burned: 1000 (million) % 27.56/4.97 % (384569)Instruction limit reached! % 27.56/4.97 % (384569)------------------------------ % 27.56/4.97 % (384569)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.56/4.97 % (384569)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.56/4.97 % (384569)CaDiCaL version: 2.1.3 % 27.56/4.97 % (384569)Termination reason: Instruction limit % 32.41/5.37 % (384569)Termination phase: Saturation % 32.41/5.37 % (384569)Time elapsed: 0.279 s % 32.41/5.37 % (384569)Peak memory usage: 91 MB % 32.41/5.37 % (384569)Instructions burned: 297 (million) % 32.41/5.37 % (384580)lrs+21_1_to=kbo:sil=128000:thi=neg_eq:si=on:random_seed=1030402566:i=321:canc=force:rtra=on:tac=axiom:ss=axioms:ev=force_2969 on theBenchmark for (2969ds/321Mi) % 32.41/5.37 % (384564)Instruction limit reached! % 32.41/5.37 % (384564)------------------------------ % 32.41/5.37 % (384564)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.41/5.37 % (384564)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.41/5.37 % (384564)CaDiCaL version: 2.1.3 % 32.41/5.37 % (384564)Termination reason: Instruction limit % 32.41/5.37 % (384564)Termination phase: Saturation % 32.41/5.37 % (384564)Time elapsed: 0.572 s % 32.41/5.37 % (384564)Peak memory usage: 135 MB % 32.41/5.37 % (384564)Instructions burned: 483 (million) % 32.41/5.37 % (384575)Instruction limit reached! % 32.41/5.37 % (384575)------------------------------ % 32.41/5.37 % (384575)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.41/5.37 % (384575)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.41/5.37 % (384575)CaDiCaL version: 2.1.3 % 32.41/5.37 % (384575)Termination reason: Instruction limit % 32.41/5.37 % (384575)Termination phase: Saturation % 32.41/5.37 % (384575)Time elapsed: 0.241 s % 32.41/5.37 % (384575)Peak memory usage: 118 MB % 32.41/5.37 % (384575)Instructions burned: 281 (million) % 32.41/5.37 % (384579)lrs+1010_1_to=kbo:sil=128000:si=on:sos=on:urr=on:uwa=alasca_main:random_seed=226864071:i=484:doe=on:nm=0:av=off:rtra=on:ss=axioms_2969 on theBenchmark for (2969ds/484Mi) % 32.41/5.37 % (384581)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=3972556240:i=416:rtra=on:gtg=position:ss=axioms_2968 on theBenchmark for (2968ds/416Mi) % 32.41/5.37 % (384580)Instruction limit reached! % 32.41/5.37 % (384580)------------------------------ % 32.41/5.37 % (384580)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.41/5.37 % (384580)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.41/5.37 % (384580)CaDiCaL version: 2.1.3 % 32.41/5.37 % (384580)Termination reason: Instruction limit % 32.41/5.37 % (384580)Termination phase: Saturation % 32.41/5.37 % (384580)Time elapsed: 0.154 s % 32.41/5.37 % (384580)Peak memory usage: 115 MB % 32.41/5.37 % (384580)Instructions burned: 322 (million) % 32.41/5.37 % (384573)Instruction limit reached! % 32.41/5.37 % (384573)------------------------------ % 32.41/5.37 % (384573)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.41/5.37 % (384573)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.41/5.37 % (384573)CaDiCaL version: 2.1.3 % 32.41/5.37 % (384573)Termination reason: Instruction limit % 32.41/5.37 % (384573)Termination phase: Saturation % 32.41/5.37 % (384573)Time elapsed: 0.355 s % 32.41/5.37 % (384573)Peak memory usage: 118 MB % 32.41/5.37 % (384573)Instructions burned: 328 (million) % 32.41/5.37 % (384582)lrs+1010_1_to=kbo:tgt=ground:fde=unused:sas=z3:si=on:sp=unary_frequency:gve=force:spb=goal:tha=off:random_seed=3909422615:i=471:thf=on:kws=precedence:rtra=on_2968 on theBenchmark for (2968ds/471Mi) % 32.41/5.37 % (384584)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=707322526:avsq=on:i=276:avsqr=1,2:rtra=on_2966 on theBenchmark for (2966ds/276Mi) % 32.41/5.37 % (384585)lrs+1010_2_to=kbo:sil=128000:tgt=ground:fde=unused:sas=z3:si=on:uwa=off:tha=off:nwc=1:random_seed=2305488888:i=375:kws=inv_arity_squared:rtra=on_2966 on theBenchmark for (2966ds/375Mi) % 32.41/5.37 % (384588)lrs+10_1_to=kbo:sil=128000:tgt=full:sas=z3:si=on:uwa=func_ext:slsqc=1:flr=on:slsq=on:random_seed=2984301295:i=387:bd=preordered:rtra=on:ss=axioms:sgt=8_2965 on theBenchmark for (2965ds/387Mi) % 32.41/5.37 % (384590)lrs+10_1_to=kbo:sil=128000:fde=none:si=on:norm_ineq=on:urr=on:nwc=0.5:random_seed=1169087336:i=513:kws=frequency:bd=all:rtra=on:gtg=exists_all:ss=axioms:sgt=4_2965 on theBenchmark for (2965ds/513Mi) % 32.41/5.37 % (384579)Instruction limit reached! % 32.41/5.37 % (384579)------------------------------ % 32.41/5.37 % (384579)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.41/5.37 % (384579)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.41/5.37 % (384579)CaDiCaL version: 2.1.3 % 32.41/5.37 % (384579)Termination reason: Instruction limit % 39.15/6.22 % (384579)Termination phase: Saturation % 39.15/6.22 % (384579)Time elapsed: 0.430 s % 39.15/6.22 % (384579)Peak memory usage: 94 MB % 39.15/6.22 % (384579)Instructions burned: 484 (million) % 39.15/6.22 % (384581)Instruction limit reached! % 39.15/6.22 % (384581)------------------------------ % 39.15/6.22 % (384581)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.15/6.22 % (384581)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.15/6.22 % (384581)CaDiCaL version: 2.1.3 % 39.15/6.22 % (384581)Termination reason: Instruction limit % 39.15/6.22 % (384581)Termination phase: Saturation % 39.15/6.22 % (384581)Time elapsed: 0.476 s % 39.15/6.22 % (384581)Peak memory usage: 120 MB % 39.15/6.22 % (384581)Instructions burned: 416 (million) % 39.15/6.22 % (384588)Instruction limit reached! % 39.15/6.22 % (384588)------------------------------ % 39.15/6.22 % (384588)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.15/6.22 % (384588)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.15/6.22 % (384588)CaDiCaL version: 2.1.3 % 39.15/6.22 % (384588)Termination reason: Instruction limit % 39.15/6.22 % (384588)Termination phase: Saturation % 39.15/6.22 % (384588)Time elapsed: 0.238 s % 39.15/6.22 % (384588)Peak memory usage: 118 MB % 39.15/6.22 % (384588)Instructions burned: 388 (million) % 39.15/6.22 % (384584)Instruction limit reached! % 39.15/6.22 % (384584)------------------------------ % 39.15/6.22 % (384584)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.15/6.22 % (384584)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.15/6.22 % (384584)CaDiCaL version: 2.1.3 % 39.15/6.22 % (384584)Termination reason: Instruction limit % 39.15/6.22 % (384584)Termination phase: Saturation % 39.15/6.22 % (384584)Time elapsed: 0.364 s % 39.15/6.22 % (384584)Peak memory usage: 135 MB % 39.15/6.22 % (384584)Instructions burned: 276 (million) % 39.15/6.22 % (384582)Instruction limit reached! % 39.15/6.22 % (384582)------------------------------ % 39.15/6.22 % (384582)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.15/6.22 % (384582)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.15/6.22 % (384582)CaDiCaL version: 2.1.3 % 39.15/6.22 % (384582)Termination reason: Instruction limit % 39.15/6.22 % (384582)Termination phase: Saturation % 39.15/6.22 % (384582)Time elapsed: 0.496 s % 39.15/6.22 % (384582)Peak memory usage: 119 MB % 39.15/6.22 % (384582)Instructions burned: 471 (million) % 39.15/6.22 % (384585)Instruction limit reached! % 39.15/6.22 % (384585)------------------------------ % 39.15/6.22 % (384585)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.15/6.22 % (384585)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.15/6.22 % (384585)CaDiCaL version: 2.1.3 % 39.15/6.22 % (384585)Termination reason: Instruction limit % 39.15/6.22 % (384585)Termination phase: Saturation % 39.15/6.22 % (384585)Time elapsed: 0.427 s % 39.15/6.22 % (384585)Peak memory usage: 119 MB % 39.15/6.22 % (384585)Instructions burned: 375 (million) % 39.15/6.22 % (384595)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=1932991223:i=334:rtra=on_2962 on theBenchmark for (2962ds/334Mi) % 39.15/6.22 % (384597)dis+1010_1_to=lpo:sil=128000:thi=all:fde=unused:si=on:sp=reverse_arity:tha=off:random_seed=4256382961:i=341:gtgl=2:rtra=on:gtg=exists_sym:ev=force:fsd=on:fsdmm=1_2961 on theBenchmark for (2961ds/341Mi) % 39.15/6.22 % (384596)lrs+1010_1_to=kbo:sil=64000:sas=cadical:si=on:sos=on:bce=on:random_seed=1758800573:i=359:rtra=on:gtg=exists_top:ss=axioms_2961 on theBenchmark for (2961ds/359Mi) % 39.15/6.22 % (384598)lrs-2_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_max:tha=off:random_seed=723291036:st=1.5:i=261:sd=1:kws=precedence:rtra=on:ss=axioms_2960 on theBenchmark for (2960ds/261Mi) % 39.15/6.22 % (384599)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=1756383814:s2pl=no:i=235:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2960 on theBenchmark for (2960ds/235Mi) % 39.15/6.22 % (384590)Instruction limit reached! % 39.15/6.22 % (384590)------------------------------ % 39.15/6.22 % (384590)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.15/6.22 % (384590)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.15/6.22 % (384590)CaDiCaL version: 2.1.3 % 39.15/6.22 % (384590)Termination reason: Instruction limit % 39.15/6.22 % (384590)Termination phase: Saturation % 41.42/6.96 % (384590)Time elapsed: 0.545 s % 41.42/6.96 % (384590)Peak memory usage: 93 MB % 41.42/6.96 % (384590)Instructions burned: 514 (million) % 41.42/6.96 % (384597)Instruction limit reached! % 41.42/6.96 % (384597)------------------------------ % 41.42/6.96 % (384597)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 41.42/6.96 % (384597)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.42/6.96 % (384597)CaDiCaL version: 2.1.3 % 41.42/6.96 % (384597)Termination reason: Instruction limit % 41.42/6.96 % (384597)Termination phase: Saturation % 41.42/6.96 % (384597)Time elapsed: 0.212 s % 41.42/6.96 % (384597)Peak memory usage: 120 MB % 41.42/6.96 % (384597)Instructions burned: 342 (million) % 41.42/6.96 % (384600)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=4073568166:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2959 on theBenchmark for (2959ds/273Mi) % 41.42/6.96 % (384598)Instruction limit reached! % 41.42/6.96 % (384598)------------------------------ % 41.42/6.96 % (384598)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 41.42/6.96 % (384598)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.42/6.96 % (384598)CaDiCaL version: 2.1.3 % 41.42/6.96 % (384598)Termination reason: Instruction limit % 41.42/6.96 % (384598)Termination phase: Saturation % 41.42/6.96 % (384598)Time elapsed: 0.255 s % 41.42/6.96 % (384598)Peak memory usage: 118 MB % 41.42/6.96 % (384598)Instructions burned: 261 (million) % 41.42/6.96 % (384595)Instruction limit reached! % 41.42/6.96 % (384595)------------------------------ % 41.42/6.96 % (384595)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 41.42/6.96 % (384595)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.42/6.96 % (384595)CaDiCaL version: 2.1.3 % 41.42/6.96 % (384595)Termination reason: Instruction limit % 41.42/6.96 % (384595)Termination phase: Saturation % 41.42/6.96 % (384595)Time elapsed: 0.421 s % 41.42/6.96 % (384595)Peak memory usage: 135 MB % 41.42/6.96 % (384595)Instructions burned: 334 (million) % 41.42/6.96 % (384596)Instruction limit reached! % 41.42/6.96 % (384596)------------------------------ % 41.42/6.96 % (384596)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 41.42/6.96 % (384596)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.42/6.96 % (384596)CaDiCaL version: 2.1.3 % 41.42/6.96 % (384596)Termination reason: Instruction limit % 41.42/6.96 % (384596)Termination phase: Saturation % 41.42/6.96 % (384596)Time elapsed: 0.372 s % 41.42/6.96 % (384596)Peak memory usage: 92 MB % 41.42/6.96 % (384596)Instructions burned: 359 (million) % 41.42/6.96 % (384599)Instruction limit reached! % 41.42/6.96 % (384599)------------------------------ % 41.42/6.96 % (384599)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 41.42/6.96 % (384599)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.42/6.96 % (384599)CaDiCaL version: 2.1.3 % 41.42/6.96 % (384599)Termination reason: Instruction limit % 41.42/6.96 % (384599)Termination phase: Saturation % 41.42/6.96 % (384599)Time elapsed: 0.279 s % 41.42/6.96 % (384599)Peak memory usage: 117 MB % 41.42/6.96 % (384599)Instructions burned: 235 (million) % 41.42/6.96 % (384611)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=2473637194:i=4428:doe=on:fsr=off:rtra=on_2957 on theBenchmark for (2957ds/4428Mi) % 41.42/6.96 % (384610)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=1474696721:i=146:doe=on:rtra=on_2957 on theBenchmark for (2957ds/146Mi) % 41.42/6.96 % (384600)Instruction limit reached! % 41.42/6.96 % (384600)------------------------------ % 41.42/6.96 % (384600)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 41.42/6.96 % (384600)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.42/6.96 % (384600)CaDiCaL version: 2.1.3 % 41.42/6.96 % (384600)Termination reason: Instruction limit % 41.42/6.96 % (384600)Termination phase: Saturation % 41.42/6.96 % (384600)Time elapsed: 0.341 s % 41.42/6.96 % (384600)Peak memory usage: 92 MB % 41.42/6.96 % (384600)Instructions burned: 273 (million) % 41.42/6.96 % (384613)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=2896221531:avsq=on:i=276:avsqr=1,2:rtra=on_2955 on theBenchmark for (2955ds/276Mi) % 41.42/6.96 % (384614)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=2902797756:i=1052:rtra=on_2955 on theBenchmark for (2955ds/1052Mi) % 48.94/7.78 % (384617)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=1843756038:st=5:i=1054:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2954 on theBenchmark for (2954ds/1054Mi) % 48.94/7.78 % (384610)Instruction limit reached! % 48.94/7.78 % (384610)------------------------------ % 48.94/7.78 % (384610)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.94/7.78 % (384610)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.94/7.78 % (384610)CaDiCaL version: 2.1.3 % 48.94/7.78 % (384610)Termination reason: Instruction limit % 48.94/7.78 % (384610)Termination phase: Saturation % 48.94/7.78 % (384610)Time elapsed: 0.162 s % 48.94/7.78 % (384610)Peak memory usage: 90 MB % 48.94/7.78 % (384610)Instructions burned: 146 (million) % 48.94/7.78 % (384616)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=1484441865:i=655:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2954 on theBenchmark for (2954ds/655Mi) % 48.94/7.78 % (384621)lrs-1002_1_to=kbo:sas=z3:si=on:norm_ineq=on:sos=on:tha=some:random_seed=784312580:i=107:rtra=on_2953 on theBenchmark for (2953ds/107Mi) % 48.94/7.78 % (384625)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=3494966922:s2a=on:i=450:doe=on:nm=32:rtra=on_2952 on theBenchmark for (2952ds/450Mi) % 48.94/7.78 % (384613)Instruction limit reached! % 48.94/7.78 % (384613)------------------------------ % 48.94/7.78 % (384613)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.94/7.78 % (384613)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.94/7.78 % (384613)CaDiCaL version: 2.1.3 % 48.94/7.78 % (384613)Termination reason: Instruction limit % 48.94/7.78 % (384613)Termination phase: Saturation % 48.94/7.78 % (384613)Time elapsed: 0.364 s % 48.94/7.78 % (384613)Peak memory usage: 134 MB % 48.94/7.78 % (384613)Instructions burned: 276 (million) % 48.94/7.78 % (384621)Instruction limit reached! % 48.94/7.78 % (384621)------------------------------ % 48.94/7.78 % (384621)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.94/7.78 % (384621)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.94/7.78 % (384621)CaDiCaL version: 2.1.3 % 48.94/7.78 % (384621)Termination reason: Instruction limit % 48.94/7.78 % (384621)Termination phase: Saturation % 48.94/7.78 % (384621)Time elapsed: 0.133 s % 48.94/7.78 % (384621)Peak memory usage: 117 MB % 48.94/7.78 % (384621)Instructions burned: 107 (million) % 48.94/7.78 % (384632)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 % 48.94/7.78 % (384632)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=1338626647:i=1090:aac=none:nm=0:rtra=on:rawr=on_2949 on theBenchmark for (2949ds/1090Mi) % 48.94/7.78 % (384635)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=1721158062:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2949 on theBenchmark for (2949ds/130Mi) % 48.94/7.78 % (384616)Instruction limit reached! % 48.94/7.78 % (384616)------------------------------ % 48.94/7.78 % (384616)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.94/7.78 % (384616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.94/7.78 % (384616)CaDiCaL version: 2.1.3 % 48.94/7.78 % (384616)Termination reason: Instruction limit % 48.94/7.78 % (384616)Termination phase: Saturation % 48.94/7.78 % (384616)Time elapsed: 0.681 s % 48.94/7.78 % (384616)Peak memory usage: 95 MB % 48.94/7.78 % (384616)Instructions burned: 655 (million) % 48.94/7.78 % (384625)Instruction limit reached! % 48.94/7.78 % (384625)------------------------------ % 48.94/7.78 % (384625)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.94/7.78 % (384625)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.94/7.78 % (384625)CaDiCaL version: 2.1.3 % 48.94/7.78 % (384625)Termination reason: Instruction limit % 48.94/7.78 % (384625)Termination phase: Saturation % 48.94/7.78 % (384625)Time elapsed: 0.479 s % 48.94/7.78 % (384625)Peak memory usage: 136 MB % 48.94/7.78 % (384625)Instructions burned: 450 (million) % 48.94/7.78 % (384635)Instruction limit reached! % 48.94/7.78 % (384635)------------------------------ % 48.94/7.78 % (384635)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.94/7.78 % (384635)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 55.90/8.78 % (384635)CaDiCaL version: 2.1.3 % 55.90/8.78 % (384635)Termination reason: Instruction limit % 55.90/8.78 % (384635)Termination phase: Saturation % 55.90/8.78 % (384635)Time elapsed: 0.169 s % 55.90/8.78 % (384635)Peak memory usage: 117 MB % 55.90/8.78 % (384635)Instructions burned: 130 (million) % 55.90/8.78 % (384617)Instruction limit reached! % 55.90/8.78 % (384617)------------------------------ % 55.90/8.78 % (384617)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 55.90/8.78 % (384617)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 55.90/8.78 % (384617)CaDiCaL version: 2.1.3 % 55.90/8.78 % (384617)Termination reason: Instruction limit % 55.90/8.78 % (384617)Termination phase: Saturation % 55.90/8.78 % (384617)Time elapsed: 0.918 s % 55.90/8.78 % (384617)Peak memory usage: 92 MB % 55.90/8.78 % (384617)Instructions burned: 1054 (million) % 55.90/8.78 % (384643)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=3222613022:i=312:kws=inv_frequency:nm=20:rtra=on_2945 on theBenchmark for (2945ds/312Mi) % 55.90/8.78 % (384614)Instruction limit reached! % 55.90/8.78 % (384614)------------------------------ % 55.90/8.78 % (384614)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 55.90/8.78 % (384614)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 55.90/8.78 % (384614)CaDiCaL version: 2.1.3 % 55.90/8.78 % (384614)Termination reason: Instruction limit % 55.90/8.78 % (384614)Termination phase: Saturation % 55.90/8.78 % (384614)Time elapsed: 1.020 s % 55.90/8.78 % (384614)Peak memory usage: 95 MB % 55.90/8.78 % (384614)Instructions burned: 1052 (million) % 55.90/8.78 % (384644)ott+10_1_to=kbo:sil=64000:si=on:sp=reverse_frequency:sos=on:random_seed=2131337206:i=491:doe=on:rtra=on:gtg=position_2945 on theBenchmark for (2945ds/491Mi) % 55.90/8.78 % (384646)ott+1011_4:1_to=lpo:sil=64000:si=on:spb=intro:random_seed=1683193897:s2a=on:i=835:s2at=2:rtra=on_2944 on theBenchmark for (2944ds/835Mi) % 55.90/8.78 % (384648)ott+1011_2_to=lpo:sil=128000:si=on:sos=on:random_seed=671386036:i=307:bd=preordered:av=off:rtra=on:ev=cautious_2943 on theBenchmark for (2943ds/307Mi) % 55.90/8.78 % (384643)Instruction limit reached! % 55.90/8.78 % (384643)------------------------------ % 55.90/8.78 % (384643)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 55.90/8.78 % (384643)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 55.90/8.78 % (384643)CaDiCaL version: 2.1.3 % 55.90/8.78 % (384643)Termination reason: Instruction limit % 55.90/8.78 % (384643)Termination phase: Saturation % 55.90/8.78 % (384643)Time elapsed: 0.294 s % 55.90/8.78 % (384643)Peak memory usage: 117 MB % 55.90/8.78 % (384643)Instructions burned: 312 (million) % 55.90/8.78 % (384650)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=1233736809:i=776:doe=on:rtra=on_2942 on theBenchmark for (2942ds/776Mi) % 55.90/8.78 % (384654)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=1392528742:s2a=on:i=646:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2940 on theBenchmark for (2940ds/646Mi) % 55.90/8.78 % (384648)Instruction limit reached! % 55.90/8.78 % (384648)------------------------------ % 55.90/8.78 % (384648)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 55.90/8.78 % (384648)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 55.90/8.78 % (384648)CaDiCaL version: 2.1.3 % 55.90/8.78 % (384648)Termination reason: Instruction limit % 55.90/8.78 % (384648)Termination phase: Saturation % 55.90/8.78 % (384648)Time elapsed: 0.348 s % 55.90/8.78 % (384648)Peak memory usage: 94 MB % 55.90/8.78 % (384648)Instructions burned: 307 (million) % 55.90/8.78 % (384632)Instruction limit reached! % 55.90/8.78 % (384632)------------------------------ % 55.90/8.78 % (384632)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 55.90/8.78 % (384632)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 55.90/8.78 % (384632)CaDiCaL version: 2.1.3 % 55.90/8.78 % (384632)Termination reason: Instruction limit % 55.90/8.78 % (384632)Termination phase: Saturation % 55.90/8.78 % (384632)Time elapsed: 1.044 s % 55.90/8.78 % (384632)Peak memory usage: 122 MB % 55.90/8.78 % (384632)Instructions burned: 1090 (million) % 55.90/8.78 % (384644)Instruction limit reached! % 55.90/8.78 % (384644)------------------------------ % 55.90/8.78 % (384644)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 55.90/8.78 % (384644)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 68.07/10.34 % (384644)CaDiCaL version: 2.1.3 % 68.07/10.34 % (384644)Termination reason: Instruction limit % 68.07/10.34 % (384644)Termination phase: Saturation % 68.07/10.34 % (384644)Time elapsed: 0.518 s % 68.07/10.34 % (384644)Peak memory usage: 93 MB % 68.07/10.34 % (384644)Instructions burned: 491 (million) % 68.07/10.34 % (384657)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=400079205:thitd=on:cond=fast:i=784:nm=30:rtra=on:gtg=all:tac=axiom_2937 on theBenchmark for (2937ds/784Mi) % 68.07/10.34 % (384659)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=1223080767:s2pl=no:i=246:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2937 on theBenchmark for (2937ds/246Mi) % 68.07/10.34 % (384658)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=3295465620:thitd=on:s2a=on:i=1131:add=on:canc=force:bd=all:rtra=on:tac=axiom:ev=off_2937 on theBenchmark for (2937ds/1131Mi) % 68.07/10.34 % (384646)Instruction limit reached! % 68.07/10.34 % (384646)------------------------------ % 68.07/10.34 % (384646)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 68.07/10.34 % (384646)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 68.07/10.34 % (384646)CaDiCaL version: 2.1.3 % 68.07/10.34 % (384646)Termination reason: Instruction limit % 68.07/10.34 % (384646)Termination phase: Saturation % 68.07/10.34 % (384646)Time elapsed: 0.904 s % 68.07/10.34 % (384646)Peak memory usage: 96 MB % 68.07/10.34 % (384646)Instructions burned: 836 (million) % 68.07/10.34 % (384659)Instruction limit reached! % 68.07/10.34 % (384659)------------------------------ % 68.07/10.34 % (384659)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 68.07/10.34 % (384659)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 68.07/10.34 % (384659)CaDiCaL version: 2.1.3 % 68.07/10.34 % (384659)Termination reason: Instruction limit % 68.07/10.34 % (384659)Termination phase: Saturation % 68.07/10.34 % (384659)Time elapsed: 0.285 s % 68.07/10.34 % (384659)Peak memory usage: 117 MB % 68.07/10.34 % (384659)Instructions burned: 246 (million) % 68.07/10.34 % (384650)Instruction limit reached! % 68.07/10.34 % (384650)------------------------------ % 68.07/10.34 % (384650)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 68.07/10.34 % (384650)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 68.07/10.34 % (384650)CaDiCaL version: 2.1.3 % 68.07/10.34 % (384650)Termination reason: Instruction limit % 68.07/10.34 % (384650)Termination phase: Saturation % 68.07/10.34 % (384650)Time elapsed: 0.856 s % 68.07/10.34 % (384650)Peak memory usage: 125 MB % 68.07/10.34 % (384650)Instructions burned: 776 (million) % 68.07/10.34 % (384611)Instruction limit reached! % 68.07/10.34 % (384611)------------------------------ % 68.07/10.34 % (384611)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 68.07/10.34 % (384611)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 68.07/10.34 % (384611)CaDiCaL version: 2.1.3 % 68.07/10.34 % (384611)Termination reason: Instruction limit % 68.07/10.34 % (384611)Termination phase: Saturation % 68.07/10.34 % (384611)Time elapsed: 2.353 s % 68.07/10.34 % (384611)Peak memory usage: 110 MB % 68.07/10.34 % (384611)Instructions burned: 4428 (million) % 68.07/10.34 % (384654)Instruction limit reached! % 68.07/10.34 % (384654)------------------------------ % 68.07/10.34 % (384654)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 68.07/10.34 % (384654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 68.07/10.34 % (384654)CaDiCaL version: 2.1.3 % 68.07/10.34 % (384654)Termination reason: Instruction limit % 68.07/10.34 % (384654)Termination phase: Saturation % 68.07/10.34 % (384654)Time elapsed: 0.689 s % 68.07/10.34 % (384654)Peak memory usage: 141 MB % 68.07/10.34 % (384654)Instructions burned: 646 (million) % 68.07/10.34 % (384663)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=3173874424:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2932 on theBenchmark for (2932ds/775Mi) % 68.07/10.34 % (384664)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=3892485733:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2931 on theBenchmark for (2931ds/273Mi) % 68.07/10.34 % (384665)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=475654212:i=102:nm=16:rtra=on_2931 on theBenchmark for (2931ds/102Mi) % 92.20/13.73 % (384666)lrs+10_1_to=lpo:sil=128000:si=on:bsr=unit_only:tha=off:random_seed=630206618:avsq=on:s2a=on:i=1094:s2at=5:avsqr=4463,131072:rtra=on_2931 on theBenchmark for (2931ds/1094Mi) % 92.20/13.73 % (384667)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=952691070:i=6400:doe=on:fsr=off:rtra=on_2930 on theBenchmark for (2930ds/6400Mi) % 92.20/13.73 % (384665)Instruction limit reached! % 92.20/13.73 % (384665)------------------------------ % 92.20/13.73 % (384665)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 92.20/13.73 % (384665)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 92.20/13.73 % (384665)CaDiCaL version: 2.1.3 % 92.20/13.73 % (384665)Termination reason: Instruction limit % 92.20/13.73 % (384665)Termination phase: Saturation % 92.20/13.73 % (384665)Time elapsed: 0.104 s % 92.20/13.73 % (384665)Peak memory usage: 89 MB % 92.20/13.73 % (384665)Instructions burned: 102 (million) % 92.20/13.73 % (384664)Instruction limit reached! % 92.20/13.73 % (384664)------------------------------ % 92.20/13.73 % (384664)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 92.20/13.73 % (384664)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 92.20/13.73 % (384664)CaDiCaL version: 2.1.3 % 92.20/13.73 % (384664)Termination reason: Instruction limit % 92.20/13.73 % (384664)Termination phase: Saturation % 92.20/13.73 % (384664)Time elapsed: 0.174 s % 92.20/13.73 % (384664)Peak memory usage: 92 MB % 92.20/13.73 % (384664)Instructions burned: 273 (million) % 92.20/13.73 % (384674)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=264630401:i=1846:canc=cautious:fsr=off:rtra=on_2927 on theBenchmark for (2927ds/1846Mi) % 92.20/13.73 % (384673)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=574617734:i=868:doe=on:nm=0:rtra=on:gtg=exists_sym_2927 on theBenchmark for (2927ds/868Mi) % 92.20/13.73 % (384657)Instruction limit reached! % 92.20/13.73 % (384657)------------------------------ % 92.20/13.73 % (384657)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 92.20/13.73 % (384657)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 92.20/13.73 % (384657)CaDiCaL version: 2.1.3 % 92.20/13.73 % (384657)Termination reason: Instruction limit % 92.20/13.73 % (384657)Termination phase: Saturation % 92.20/13.73 % (384657)Time elapsed: 0.974 s % 92.20/13.73 % (384657)Peak memory usage: 122 MB % 92.20/13.73 % (384657)Instructions burned: 784 (million) % 92.20/13.73 % (384663)Instruction limit reached! % 92.20/13.73 % (384663)------------------------------ % 92.20/13.73 % (384663)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 92.20/13.73 % (384663)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 92.20/13.73 % (384663)CaDiCaL version: 2.1.3 % 92.20/13.73 % (384663)Termination reason: Instruction limit % 92.20/13.73 % (384663)Termination phase: Saturation % 92.20/13.73 % (384663)Time elapsed: 0.740 s % 92.20/13.73 % (384663)Peak memory usage: 93 MB % 92.20/13.73 % (384663)Instructions burned: 775 (million) % 92.20/13.73 % (384677)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=1388479269:s2a=on:i=36816:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2924 on theBenchmark for (2924ds/36816Mi) % 92.20/13.73 % (384658)Instruction limit reached! % 92.20/13.73 % (384658)------------------------------ % 92.20/13.73 % (384658)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 92.20/13.73 % (384658)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 92.20/13.73 % (384658)CaDiCaL version: 2.1.3 % 92.20/13.73 % (384658)Termination reason: Instruction limit % 92.20/13.73 % (384658)Termination phase: Saturation % 92.20/13.73 % (384658)Time elapsed: 1.256 s % 92.20/13.73 % (384658)Peak memory usage: 127 MB % 92.20/13.73 % (384658)Instructions burned: 1131 (million) % 92.20/13.73 % (384679)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=2256192542:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2922 on theBenchmark for (2922ds/273Mi) % 92.20/13.73 % (384666)Instruction limit reached! % 92.20/13.73 % (384666)------------------------------ % 92.20/13.73 % (384666)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 92.20/13.73 % (384666)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 92.20/13.73 % (384666)CaDiCaL version: 2.1.3 % 104.66/15.59 % (384666)Termination reason: Instruction limit % 104.66/15.59 % (384666)Termination phase: Saturation % 104.66/15.59 % (384666)Time elapsed: 0.956 s % 104.66/15.59 % (384666)Peak memory usage: 96 MB % 104.66/15.59 % (384666)Instructions burned: 1095 (million) % 104.66/15.59 % (384680)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=336537059:i=863:doe=on:nm=0:rtra=on:gtg=exists_sym_2921 on theBenchmark for (2921ds/863Mi) % 104.66/15.59 % (384679)Instruction limit reached! % 104.66/15.59 % (384679)------------------------------ % 104.66/15.59 % (384679)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 104.66/15.59 % (384679)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 104.66/15.59 % (384679)CaDiCaL version: 2.1.3 % 104.66/15.59 % (384679)Termination reason: Instruction limit % 104.66/15.59 % (384679)Termination phase: Saturation % 104.66/15.59 % (384679)Time elapsed: 0.323 s % 104.66/15.59 % (384679)Peak memory usage: 92 MB % 104.66/15.59 % (384679)Instructions burned: 273 (million) % 104.66/15.59 % (384673)Instruction limit reached! % 104.66/15.59 % (384673)------------------------------ % 104.66/15.59 % (384673)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 104.66/15.59 % (384673)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 104.66/15.59 % (384673)CaDiCaL version: 2.1.3 % 104.66/15.59 % (384673)Termination reason: Instruction limit % 104.66/15.59 % (384673)Termination phase: Saturation % 104.66/15.59 % (384673)Time elapsed: 0.885 s % 104.66/15.59 % (384673)Peak memory usage: 120 MB % 104.66/15.59 % (384673)Instructions burned: 868 (million) % 104.66/15.59 % (384684)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=1488260826:i=5811:kws=precedence:nm=0:rtra=on_2918 on theBenchmark for (2918ds/5811Mi) % 104.66/15.59 % (384674)Instruction limit reached! % 104.66/15.59 % (384674)------------------------------ % 104.66/15.59 % (384674)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 104.66/15.59 % (384674)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 104.66/15.59 % (384674)CaDiCaL version: 2.1.3 % 104.66/15.59 % (384674)Termination reason: Instruction limit % 104.66/15.59 % (384674)Termination phase: Saturation % 104.66/15.59 % (384674)Time elapsed: 0.962 s % 104.66/15.59 % (384674)Peak memory usage: 99 MB % 104.66/15.59 % (384674)Instructions burned: 1846 (million) % 104.66/15.59 % (384687)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=1239670558:i=801:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2916 on theBenchmark for (2916ds/801Mi) % 104.66/15.59 % (384686)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=2063147964:i=2216:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2916 on theBenchmark for (2916ds/2216Mi) % 104.66/15.59 % (384689)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=2679315594:st=5:i=1026:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2915 on theBenchmark for (2915ds/1026Mi) % 104.66/15.59 % (384680)Instruction limit reached! % 104.66/15.59 % (384680)------------------------------ % 104.66/15.59 % (384680)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 104.66/15.59 % (384680)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 104.66/15.59 % (384680)CaDiCaL version: 2.1.3 % 104.66/15.59 % (384680)Termination reason: Instruction limit % 104.66/15.59 % (384680)Termination phase: Saturation % 104.66/15.59 % (384680)Time elapsed: 0.921 s % 104.66/15.59 % (384680)Peak memory usage: 120 MB % 104.66/15.59 % (384680)Instructions burned: 863 (million) % 104.66/15.59 % (384693)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=3377693693:i=3509:rtra=on_2909 on theBenchmark for (2909ds/3509Mi) % 104.66/15.59 % (384687)Instruction limit reached! % 104.66/15.59 % (384687)------------------------------ % 104.66/15.59 % (384687)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 104.66/15.59 % (384687)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 104.66/15.59 % (384687)CaDiCaL version: 2.1.3 % 104.66/15.59 % (384687)Termination reason: Instruction limit % 104.66/15.59 % (384687)Termination phase: Saturation % 104.66/15.59 % (384687)Time elapsed: 0.754 s % 104.66/15.59 % (384687)Peak memory usage: 94 MB % 104.66/15.59 % (384687)Instructions burned: 801 (million) % 104.66/15.59 % (384697)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=2416268455:st=2:i=2127:sd=12:ep=R:rtra=on:ss=axioms_2906 on theBenchmark for (2906ds/2127Mi) % 104.66/15.59 % (384689)Instruction limit reached! % 178.78/26.00 % (384689)------------------------------ % 178.78/26.00 % (384689)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 178.78/26.00 % (384689)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 178.78/26.00 % (384689)CaDiCaL version: 2.1.3 % 178.78/26.00 % (384689)Termination reason: Instruction limit % 178.78/26.00 % (384689)Termination phase: Saturation % 178.78/26.00 % (384689)Time elapsed: 0.943 s % 178.78/26.00 % (384689)Peak memory usage: 94 MB % 178.78/26.00 % (384689)Instructions burned: 1026 (million) % 178.78/26.00 % (384686)Instruction limit reached! % 178.78/26.00 % (384686)------------------------------ % 178.78/26.00 % (384686)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 178.78/26.00 % (384686)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 178.78/26.00 % (384686)CaDiCaL version: 2.1.3 % 178.78/26.00 % (384686)Termination reason: Instruction limit % 178.78/26.00 % (384686)Termination phase: Saturation % 178.78/26.00 % (384686)Time elapsed: 1.200 s % 178.78/26.00 % (384686)Peak memory usage: 132 MB % 178.78/26.00 % (384686)Instructions burned: 2216 (million) % 178.78/26.00 % (384699)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=1991853199:i=1959:rtra=on:fsd=on:proc=on_2903 on theBenchmark for (2903ds/1959Mi) % 178.78/26.00 % (384700)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=2843054425:s2a=on:i=3553:nm=0:rtra=on_2901 on theBenchmark for (2901ds/3553Mi) % 178.78/26.00 % (384697)Instruction limit reached! % 178.78/26.00 % (384697)------------------------------ % 178.78/26.00 % (384697)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 178.78/26.00 % (384697)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 178.78/26.00 % (384697)CaDiCaL version: 2.1.3 % 178.78/26.00 % (384697)Termination reason: Instruction limit % 178.78/26.00 % (384697)Termination phase: Saturation % 178.78/26.00 % (384697)Time elapsed: 1.850 s % 178.78/26.00 % (384697)Peak memory usage: 101 MB % 178.78/26.00 % (384697)Instructions burned: 2128 (million) % 178.78/26.00 % (384703)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=2628719404:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2885 on theBenchmark for (2885ds/3201Mi) % 178.78/26.00 % (384699)Instruction limit reached! % 178.78/26.00 % (384699)------------------------------ % 178.78/26.00 % (384699)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 178.78/26.00 % (384699)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 178.78/26.00 % (384699)CaDiCaL version: 2.1.3 % 178.78/26.00 % (384699)Termination reason: Instruction limit % 178.78/26.00 % (384699)Termination phase: Saturation % 178.78/26.00 % (384699)Time elapsed: 1.996 s % 178.78/26.00 % (384699)Peak memory usage: 124 MB % 178.78/26.00 % (384699)Instructions burned: 1959 (million) % 178.78/26.00 % (384705)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=1411890030:thitd=on:cond=on:i=4093:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2881 on theBenchmark for (2881ds/4093Mi) % 178.78/26.00 % (384700)Instruction limit reached! % 178.78/26.00 % (384700)------------------------------ % 178.78/26.00 % (384700)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 178.78/26.00 % (384700)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 178.78/26.00 % (384700)CaDiCaL version: 2.1.3 % 178.78/26.00 % (384700)Termination reason: Instruction limit % 178.78/26.00 % (384700)Termination phase: Saturation % 178.78/26.00 % (384700)Time elapsed: 2.181 s % 178.78/26.00 % (384700)Peak memory usage: 106 MB % 178.78/26.00 % (384700)Instructions burned: 3554 (million) % 178.78/26.00 % (384707)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=4163659771:cond=fast:i=21173:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2877 on theBenchmark for (2877ds/21173Mi) % 178.78/26.00 % (384693)Instruction limit reached! % 178.78/26.00 % (384693)------------------------------ % 178.78/26.00 % (384693)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 178.78/26.00 % (384693)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 178.78/26.00 % (384693)CaDiCaL version: 2.1.3 % 178.78/26.00 % (384693)Termination reason: Instruction limit % 178.78/26.00 % (384693)Termination phase: Saturation % 178.78/26.00 % (384693)Time elapsed: 3.789 s % 178.78/26.00 % (384693)Peak memory usage: 113 MB % 178.78/26.00 % (384693)Instructions burned: 3509 (million) % 210.48/30.42 % (384709)lrs+11_1_to=lpo:thi=all:sas=z3:si=on:fd=off:sac=on:slsq=on:random_seed=1532887755:avsq=on:i=10544:avsqr=17,4:canc=force:rtra=on:gtg=exists_top:er=filter_2869 on theBenchmark for (2869ds/10544Mi) % 210.48/30.42 % (384667)Instruction limit reached! % 210.48/30.42 % (384667)------------------------------ % 210.48/30.42 % (384667)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 210.48/30.42 % (384667)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 210.48/30.42 % (384667)CaDiCaL version: 2.1.3 % 210.48/30.42 % (384667)Termination reason: Instruction limit % 210.48/30.42 % (384667)Termination phase: Saturation % 210.48/30.42 % (384667)Time elapsed: 6.436 s % 210.48/30.42 % (384667)Peak memory usage: 122 MB % 210.48/30.42 % (384667)Instructions burned: 6400 (million) % 210.48/30.42 % (384684)Instruction limit reached! % 210.48/30.42 % (384684)------------------------------ % 210.48/30.42 % (384684)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 210.48/30.42 % (384684)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 210.48/30.42 % (384684)CaDiCaL version: 2.1.3 % 210.48/30.42 % (384684)Termination reason: Instruction limit % 210.48/30.42 % (384684)Termination phase: Saturation % 210.48/30.42 % (384684)Time elapsed: 5.438 s % 210.48/30.42 % (384684)Peak memory usage: 131 MB % 210.48/30.42 % (384684)Instructions burned: 5811 (million) % 210.48/30.42 % (384711)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=1252930569:avsq=on:i=1262:avsqr=1,16:rtra=on:rawr=on_2863 on theBenchmark for (2863ds/1262Mi) % 210.48/30.42 % (384716)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=961900194:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2861 on theBenchmark for (2861ds/775Mi) % 210.48/30.42 % (384703)Instruction limit reached! % 210.48/30.42 % (384703)------------------------------ % 210.48/30.42 % (384703)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 210.48/30.42 % (384703)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 210.48/30.42 % (384703)CaDiCaL version: 2.1.3 % 210.48/30.42 % (384703)Termination reason: Instruction limit % 210.48/30.42 % (384703)Termination phase: Saturation % 210.48/30.42 % (384703)Time elapsed: 2.556 s % 210.48/30.42 % (384703)Peak memory usage: 95 MB % 210.48/30.42 % (384703)Instructions burned: 3202 (million) % 210.48/30.42 % (384705)Instruction limit reached! % 210.48/30.42 % (384705)------------------------------ % 210.48/30.42 % (384705)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 210.48/30.42 % (384705)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 210.48/30.42 % (384705)CaDiCaL version: 2.1.3 % 210.48/30.42 % (384705)Termination reason: Instruction limit % 210.48/30.42 % (384705)Termination phase: Saturation % 210.48/30.42 % (384705)Time elapsed: 2.406 s % 210.48/30.42 % (384705)Peak memory usage: 153 MB % 210.48/30.42 % (384705)Instructions burned: 4094 (million) % 210.48/30.42 % (384719)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=3316137119:i=270:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2856 on theBenchmark for (2856ds/270Mi) % 210.48/30.42 % (384720)ott+10_128_isp=bottom:to=lpo:sil=128000:si=on:urr=on:uwa=alasca_main:sac=on:slsq=on:random_seed=3658269538:i=17165:aac=none:doe=on:rtra=on:gtg=exists_all_2854 on theBenchmark for (2854ds/17165Mi) % 210.48/30.42 % (384719)Instruction limit reached! % 210.48/30.42 % (384719)------------------------------ % 210.48/30.42 % (384719)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 210.48/30.42 % (384719)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 210.48/30.42 % (384719)CaDiCaL version: 2.1.3 % 210.48/30.42 % (384719)Termination reason: Instruction limit % 210.48/30.42 % (384719)Termination phase: Saturation % 210.48/30.42 % (384719)Time elapsed: 0.294 s % 210.48/30.42 % (384719)Peak memory usage: 92 MB % 210.48/30.42 % (384719)Instructions burned: 270 (million) % 210.48/30.42 % (384716)Instruction limit reached! % 210.48/30.42 % (384716)------------------------------ % 210.48/30.42 % (384716)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 210.48/30.42 % (384716)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 210.48/30.42 % (384716)CaDiCaL version: 2.1.3 % 210.48/30.42 % (384716)Termination reason: Instruction limit % 210.48/30.42 % (384716)Termination phase: Saturation % 210.48/30.42 % (384716)Time elapsed: 0.756 s % 210.48/30.42 % (384716)Peak memory usage: 94 MB % 210.48/30.42 % (384716)Instructions burned: 776 (million) % 246.74/35.56 % (384723)lrs+2_10_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_main:tha=some:random_seed=3903646642:s2a=on:i=13094:s2at=-1:rtra=on_2851 on theBenchmark for (2851ds/13094Mi) % 246.74/35.56 % (384711)Instruction limit reached! % 246.74/35.56 % (384711)------------------------------ % 246.74/35.56 % (384711)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 246.74/35.56 % (384711)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 246.74/35.56 % (384711)CaDiCaL version: 2.1.3 % 246.74/35.56 % (384711)Termination reason: Instruction limit % 246.74/35.56 % (384711)Termination phase: Saturation % 246.74/35.56 % (384711)Time elapsed: 1.282 s % 246.74/35.56 % (384711)Peak memory usage: 125 MB % 246.74/35.56 % (384711)Instructions burned: 1262 (million) % 246.74/35.56 % (384724)lrs+10_1_to=lpo:sil=128000:si=on:sp=occurrence:random_seed=797132415:st=2:i=12633:rtra=on:ss=axioms_2850 on theBenchmark for (2850ds/12633Mi) % 246.74/35.56 % (384726)dis+1011_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_frequency:lsd=20:nwc=3:random_seed=4165288009:i=1783:rtra=on:gtg=position_2848 on theBenchmark for (2848ds/1783Mi) % 246.74/35.56 % (384726)Instruction limit reached! % 246.74/35.56 % (384726)------------------------------ % 246.74/35.56 % (384726)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 246.74/35.56 % (384726)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 246.74/35.56 % (384726)CaDiCaL version: 2.1.3 % 246.74/35.56 % (384726)Termination reason: Instruction limit % 246.74/35.56 % (384726)Termination phase: Saturation % 246.74/35.56 % (384726)Time elapsed: 1.896 s % 246.74/35.56 % (384726)Peak memory usage: 125 MB % 246.74/35.56 % (384726)Instructions burned: 1783 (million) % 246.74/35.56 % (384731)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=113892497:i=5451:aac=none:doe=on:nm=0:rtra=on:amm=off:gtg=position_2826 on theBenchmark for (2826ds/5451Mi) % 246.74/35.56 % (384731)Instruction limit reached! % 246.74/35.56 % (384731)------------------------------ % 246.74/35.56 % (384731)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 246.74/35.56 % (384731)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 246.74/35.56 % (384731)CaDiCaL version: 2.1.3 % 246.74/35.56 % (384731)Termination reason: Instruction limit % 246.74/35.56 % (384731)Termination phase: Saturation % 246.74/35.56 % (384731)Time elapsed: 5.118 s % 246.74/35.56 % (384731)Peak memory usage: 133 MB % 246.74/35.56 % (384731)Instructions burned: 5451 (million) % 246.74/35.56 % (384720)Instruction limit reached! % 246.74/35.56 % (384720)------------------------------ % 246.74/35.56 % (384720)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 246.74/35.56 % (384720)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 246.74/35.56 % (384720)CaDiCaL version: 2.1.3 % 246.74/35.56 % (384720)Termination reason: Instruction limit % 246.74/35.56 % (384720)Termination phase: Saturation % 246.74/35.56 % (384720)Time elapsed: 8.156 s % 246.74/35.56 % (384720)Peak memory usage: 171 MB % 246.74/35.56 % (384720)Instructions burned: 17166 (million) % 246.74/35.56 % (384733)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=3677123247:i=4975:doe=on:nm=0:rtra=on:gtg=exists_sym_2772 on theBenchmark for (2772ds/4975Mi) % 246.74/35.56 % (384734)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=1391454230:i=2076:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2771 on theBenchmark for (2771ds/2076Mi) % 246.74/35.57 % (384709)Instruction limit reached! % 246.74/35.57 % (384709)------------------------------ % 246.74/35.57 % (384709)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 246.74/35.57 % (384709)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 246.74/35.57 % (384709)CaDiCaL version: 2.1.3 % 246.74/35.57 % (384709)Termination reason: Instruction limit % 246.74/35.57 % (384709)Termination phase: Saturation % 246.74/35.57 % (384709)Time elapsed: 10.300 s % 246.74/35.57 % (384709)Peak memory usage: 172 MB % 246.74/35.57 % (384709)Instructions burned: 10545 (million) % 246.74/35.57 % (384737)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=3170284926:i=5145:rtra=on_2764 on theBenchmark for (2764ds/5145Mi) % 246.74/35.57 % (384734)Instruction limit reached! % 246.74/35.57 % (384734)------------------------------ % 246.74/35.57 % (384734)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.55/43.10 % (384734)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.55/43.10 % (384734)CaDiCaL version: 2.1.3 % 300.55/43.10 % (384734)Termination reason: Instruction limit % 300.55/43.10 % (384734)Termination phase: Saturation % 300.55/43.10 % (384734)Time elapsed: 2.091 s % 300.55/43.10 % (384734)Peak memory usage: 131 MB % 300.55/43.10 % (384734)Instructions burned: 2078 (million) % 300.55/43.10 % (384733)Instruction limit reached! % 300.55/43.10 % (384733)------------------------------ % 300.55/43.10 % (384733)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.55/43.10 % (384733)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.55/43.10 % (384733)CaDiCaL version: 2.1.3 % 300.55/43.10 % (384733)Termination reason: Instruction limit % 300.55/43.10 % (384733)Termination phase: Saturation % 300.55/43.10 % (384733)Time elapsed: 2.659 s % 300.55/43.10 % (384733)Peak memory usage: 130 MB % 300.55/43.10 % (384733)Instructions burned: 4977 (million) % 300.55/43.10 % (384741)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=179461665:i=3509:rtra=on_2746 on theBenchmark for (2746ds/3509Mi) % 300.55/43.10 % (384744)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=2540809639:st=2:i=13800:sd=12:ep=R:rtra=on:ss=axioms_2744 on theBenchmark for (2744ds/13800Mi) % 300.55/43.10 % (384723)Instruction limit reached! % 300.55/43.10 % (384723)------------------------------ % 300.55/43.10 % (384723)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.55/43.10 % (384723)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.55/43.10 % (384723)CaDiCaL version: 2.1.3 % 300.55/43.10 % (384723)Termination reason: Instruction limit % 300.55/43.10 % (384723)Termination phase: Saturation % 300.55/43.10 % (384723)Time elapsed: 12.357 s % 300.55/43.10 % (384723)Peak memory usage: 156 MB % 300.55/43.10 % (384723)Instructions burned: 13094 (million) % 300.55/43.10 % (384747)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=796382434:i=1412:rtra=on:fsd=on:proc=on_2724 on theBenchmark for (2724ds/1412Mi) % 300.55/43.10 % (384747)Instruction limit reached! % 300.55/43.10 % (384747)------------------------------ % 300.55/43.10 % (384747)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.55/43.10 % (384747)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.55/43.10 % (384747)CaDiCaL version: 2.1.3 % 300.55/43.10 % (384747)Termination reason: Instruction limit % 300.55/43.10 % (384747)Termination phase: Saturation % 300.55/43.10 % (384747)Time elapsed: 0.876 s % 300.55/43.10 % (384747)Peak memory usage: 122 MB % 300.55/43.10 % (384747)Instructions burned: 1413 (million) % 300.55/43.10 % (384749)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 % 300.55/43.10 % (384749)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=2083977621:i=11747:aac=none:nm=0:rtra=on:rawr=on_2713 on theBenchmark for (2713ds/11747Mi) % 300.55/43.10 % (384737)Instruction limit reached! % 300.55/43.10 % (384737)------------------------------ % 300.55/43.10 % (384737)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.55/43.10 % (384737)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.55/43.10 % (384737)CaDiCaL version: 2.1.3 % 300.55/43.10 % (384737)Termination reason: Instruction limit % 300.55/43.10 % (384737)Termination phase: Saturation % 300.55/43.10 % (384737)Time elapsed: 5.164 s % 300.55/43.10 % (384737)Peak memory usage: 111 MB % 300.55/43.10 % (384737)Instructions burned: 5145 (million) % 300.55/43.10 % (384751)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=1196800997:s2a=on:i=3553:nm=0:rtra=on_2709 on theBenchmark for (2709ds/3553Mi) % 300.55/43.10 % (384741)Instruction limit reached! % 300.55/43.10 % (384741)------------------------------ % 300.55/43.10 % (384741)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.55/43.10 % (384741)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.55/43.10 % (384741)CaDiCaL version: 2.1.3 % 300.55/43.10 % (384741)Termination reason: Instruction limit % 300.55/43.10 % (384741)Termination phase: Saturation % 300.55/43.10 % (384741)Time elapsed: 3.840 s % 300.55/43.10 % (384741)Peak memory usage: 113 MB % 300.55/43.10 % (384741)Instructions burned: 3509 (million) % 300.55/43.10 % (384724)Instruction limit reached! % 300.55/43.10 % (384724)------------------------------ % 300.55/43.10 % (384724)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.55/43.10 % (384724)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.55/43.10 % (384724)CaDiCaL version: 2.1.3 % 300.55/43.10 % (384724)Termination reason: Instruction limit % 300.55/43.10 % (384724)Termination phase: Saturation % 300.55/43.10 % (384724)Time elapsed: 14.538 s % 300.55/43.10 % (384724)Peak memory usage: 150 MB % 300.55/43.10 % (384724)Instructions burned: 12633 (million) % 300.55/43.10 % (384753)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=599734168:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2705 on theBenchmark for (2705ds/3201Mi) % 300.55/43.10 % (384757)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=3918133448:thitd=on:cond=on:i=4081:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2702 on theBenchmark for (2702ds/4081Mi) % 300.55/43.10 % (384707)Instruction limit reached! % 300.55/43.10 % (384707)------------------------------ % 300.55/43.10 % (384707)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.55/43.10 % (384707)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.55/43.10 % (384707)CaDiCaL version: 2.1.3 % 300.55/43.10 % (384707)Termination reason: Instruction limit % 300.55/43.10 % (384707)Termination phase: Saturation % 300.55/43.10 % (384707)Time elapsed: 18.324 s % 300.55/43.10 % (384707)Peak memory usage: 178 MB % 300.55/43.10 % (384707)Instructions burned: 21174 (million) % 300.55/43.10 % (384763)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=3233262522:cond=fast:i=20260:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2691 on theBenchmark for (2691ds/20260Mi) % 300.55/43.10 % (384753)Instruction limit reached! % 300.55/43.10 % (384753)------------------------------ % 300.55/43.10 % (384753)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.55/43.10 % (384753)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.55/43.10 % (384753)CaDiCaL version: 2.1.3 % 300.55/43.10 % (384753)Termination reason: Instruction limit % 300.55/43.10 % (384753)Termination phase: Saturation % 300.55/43.10 % (384753)Time elapsed: 2.651 s % 300.55/43.10 % (384753)Peak memory usage: 95 MB % 300.55/43.10 % (384753)Instructions burned: 3202 (million) % 300.55/43.10 % (384781)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=4091575997:s2a=on:i=58627:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2675 on theBenchmark for (2675ds/58627Mi) % 300.55/43.10 % (384751)Instruction limit reached! % 300.55/43.10 % (384751)------------------------------ % 300.55/43.10 % (384751)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.55/43.10 % (384751)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.55/43.10 % (384751)CaDiCaL version: 2.1.3 % 300.55/43.10 % (384751)Termination reason: Instruction limit % 300.55/43.10 % (384751)Termination phase: Saturation % 300.55/43.10 % (384751)Time elapsed: 3.800 s % 300.55/43.10 % (384751)Peak memory usage: 106 MB % 300.55/43.10 % (384751)Instructions burned: 3553 (million) % 300.55/43.10 % (384783)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=1181262133:avsq=on:i=6258:avsqr=1,16:rtra=on:rawr=on_2668 on theBenchmark for (2668ds/6258Mi) % 300.55/43.10 % (384757)Instruction limit reached! % 300.55/43.10 % (384757)------------------------------ % 300.55/43.10 % (384757)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.55/43.10 % (384757)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.55/43.10 % (384757)CaDiCaL version: 2.1.3 % 300.55/43.10 % (384757)Termination reason: Instruction limit % 300.55/43.10 % (384757)Termination phase: Saturation % 300.55/43.10 % (384757)Time elapsed: 4.578 s % 300.55/43.10 % (384757)Peak memory usage: 153 MB % 300.55/43.10 % (384757)Instructions burned: 4081 (million) % 300.55/43.10 % (384749)Instruction limit reached! % 300.55/43.10 % (384749)------------------------------ % 300.55/43.10 % (384749)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.55/43.10 % (384749)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.55/43.10 % (384749)CaDiCaL version: 2.1.3 % 300.55/43.10 % (384749)Termination reason: Instruction limit % 300.55/43.10 % (384749)Termination phase: Saturation % 300.55/43.10 % (384749)Time elapsed: 5.934 s % 300.55/43.10 % (384749)Peak memory usage: 157 MB % 300.55/43.10 % (384749)Instructions burned: 11751 (million) % 300.55/43.10 % (384785)ott+10_128_isp=bottom:to=lpo % 300.55/43.11 Terminated %------------------------------------------------------------------------------