%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWW656_2 : TPTP v9.3.1. Released v6.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % Computer : n019.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:31:04 PM UTC 2026 % Result : Timeout 300.18s 42.74s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : SWW656_2 : TPTP v9.3.1. Released v6.1.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.09/0.16 % Computer : n019.cluster.edu % 0.09/0.16 % Model : x86_64 x86_64 % 0.09/0.16 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.16 % Memory : 8046.5625MB % 0.09/0.16 % OS : Linux 6.8.0-71-generic % 0.09/0.17 % CPULimit : 300 % 0.09/0.17 % WCLimit : 300 % 0.09/0.17 % DateTime : Mon Sep 28 14:24:03 UTC 2026 % 0.09/0.17 % CPUTime : % 0.09/0.17 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.09/0.20 Running first-order theorem proving % 0.09/0.20 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 2.62/0.99 % (4032643)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule. % 2.62/0.99 % (4032747)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=509247519:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi) % 2.62/0.99 % (4032747)Instruction limit reached! % 2.62/0.99 % (4032747)------------------------------ % 2.62/0.99 % (4032747)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 2.62/0.99 % (4032747)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.62/0.99 % (4032747)CaDiCaL version: 2.1.3 % 2.62/0.99 % (4032747)Termination reason: Instruction limit % 2.62/0.99 % (4032747)Termination phase: Saturation % 2.62/0.99 % (4032747)Time elapsed: 0.026 s % 2.62/0.99 % (4032747)Peak memory usage: 116 MB % 2.62/0.99 % (4032747)Instructions burned: 34 (million) % 2.62/0.99 % (4032744)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=4228410794:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi) % 2.62/0.99 % (4032738)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=1965579480:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi) % 2.62/0.99 % (4032742)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=1077485703:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi) % 2.62/0.99 % (4032745)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=3478287185:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi) % 2.62/0.99 % (4032739)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=1963800132:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi) % 2.62/0.99 % (4032741)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=1803209128:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi) % 2.62/0.99 % (4032744)Instruction limit reached! % 2.62/0.99 % (4032744)------------------------------ % 2.62/0.99 % (4032744)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 2.62/0.99 % (4032744)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.62/0.99 % (4032744)CaDiCaL version: 2.1.3 % 2.62/0.99 % (4032744)Termination reason: Instruction limit % 2.62/0.99 % (4032744)Termination phase: Preprocessing 3 % 2.62/0.99 % (4032744)Time elapsed: 0.003 s % 2.62/0.99 % (4032744)Peak memory usage: 86 MB % 2.62/0.99 % (4032744)Instructions burned: 4 (million) % 2.62/0.99 % (4032742)Instruction limit reached! % 2.62/0.99 % (4032742)------------------------------ % 2.62/0.99 % (4032742)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 2.62/0.99 % (4032742)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.62/0.99 % (4032742)CaDiCaL version: 2.1.3 % 2.62/0.99 % (4032742)Termination reason: Instruction limit % 2.62/0.99 % (4032742)Termination phase: Property scanning % 2.62/0.99 % (4032742)Time elapsed: 0.005 s % 2.62/0.99 % (4032742)Peak memory usage: 86 MB % 2.62/0.99 % (4032742)Instructions burned: 9 (million) % 2.62/0.99 % (4032738)Instruction limit reached! % 2.62/0.99 % (4032738)------------------------------ % 2.62/0.99 % (4032738)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 2.62/0.99 % (4032738)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.62/0.99 % (4032738)CaDiCaL version: 2.1.3 % 2.62/0.99 % (4032738)Termination reason: Instruction limit % 2.62/0.99 % (4032738)Termination phase: Saturation % 2.62/0.99 % (4032738)Time elapsed: 0.028 s % 2.62/0.99 % (4032738)Peak memory usage: 112 MB % 2.62/0.99 % (4032738)Instructions burned: 12 (million) % 2.62/0.99 % (4032745)Instruction limit reached! % 2.62/0.99 % (4032745)------------------------------ % 2.62/0.99 % (4032745)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 2.62/0.99 % (4032745)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.62/0.99 % (4032745)CaDiCaL version: 2.1.3 % 2.62/0.99 % (4032745)Termination reason: Instruction limit % 2.62/0.99 % (4032745)Termination phase: Saturation % 2.62/0.99 % (4032745)Time elapsed: 0.055 s % 2.62/0.99 % (4032745)Peak memory usage: 116 MB % 2.62/0.99 % (4032745)Instructions burned: 47 (million) % 2.62/0.99 % (4032777)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=3249535785:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2998 on theBenchmark for (2998ds/14Mi) % 2.62/0.99 % (4032777)Instruction limit reached! % 2.62/0.99 % (4032777)------------------------------ % 4.68/1.15 % (4032777)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.68/1.15 % (4032777)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.68/1.15 % (4032777)CaDiCaL version: 2.1.3 % 4.68/1.15 % (4032777)Termination reason: Instruction limit % 4.68/1.15 % (4032777)Termination phase: Saturation % 4.68/1.15 % (4032777)Time elapsed: 0.005 s % 4.68/1.15 % (4032777)Peak memory usage: 88 MB % 4.68/1.15 % (4032777)Instructions burned: 14 (million) % 4.68/1.15 % (4032778)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=1238725629:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2998 on theBenchmark for (2998ds/29Mi) % 4.68/1.15 % (4032779)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=3588910595:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/16Mi) % 4.68/1.15 % (4032779)Instruction limit reached! % 4.68/1.15 % (4032779)------------------------------ % 4.68/1.15 % (4032779)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.68/1.15 % (4032779)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.68/1.15 % (4032779)CaDiCaL version: 2.1.3 % 4.68/1.15 % (4032779)Termination reason: Instruction limit % 4.68/1.15 % (4032779)Termination phase: Saturation % 4.68/1.15 % (4032779)Time elapsed: 0.010 s % 4.68/1.15 % (4032779)Peak memory usage: 88 MB % 4.68/1.15 % (4032779)Instructions burned: 16 (million) % 4.68/1.15 % (4032741)Instruction limit reached! % 4.68/1.15 % (4032741)------------------------------ % 4.68/1.15 % (4032741)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.68/1.15 % (4032741)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.68/1.15 % (4032741)CaDiCaL version: 2.1.3 % 4.68/1.15 % (4032741)Termination reason: Instruction limit % 4.68/1.15 % (4032741)Termination phase: Saturation % 4.68/1.15 % (4032741)Time elapsed: 0.170 s % 4.68/1.15 % (4032741)Peak memory usage: 119 MB % 4.68/1.15 % (4032741)Instructions burned: 202 (million) % 4.68/1.15 % (4032778)Instruction limit reached! % 4.68/1.15 % (4032778)------------------------------ % 4.68/1.15 % (4032778)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.68/1.15 % (4032778)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.68/1.15 % (4032778)CaDiCaL version: 2.1.3 % 4.68/1.15 % (4032778)Termination reason: Instruction limit % 4.68/1.15 % (4032778)Termination phase: Saturation % 4.68/1.15 % (4032778)Time elapsed: 0.023 s % 4.68/1.15 % (4032778)Peak memory usage: 88 MB % 4.68/1.15 % (4032778)Instructions burned: 30 (million) % 4.68/1.15 % (4032780)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=4276232171:i=24:canc=force:rtra=on_2998 on theBenchmark for (2998ds/24Mi) % 4.68/1.15 % (4032780)Instruction limit reached! % 4.68/1.15 % (4032780)------------------------------ % 4.68/1.15 % (4032780)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.68/1.15 % (4032780)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.68/1.15 % (4032780)CaDiCaL version: 2.1.3 % 4.68/1.15 % (4032780)Termination reason: Instruction limit % 4.68/1.15 % (4032780)Termination phase: Saturation % 4.68/1.15 % (4032780)Time elapsed: 0.017 s % 4.68/1.15 % (4032780)Peak memory usage: 89 MB % 4.68/1.15 % (4032780)Instructions burned: 25 (million) % 4.68/1.15 % (4032781)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=837369742:i=27:canc=cautious:fsr=off:rtra=on_2997 on theBenchmark for (2997ds/27Mi) % 4.68/1.15 % (4032739)Instruction limit reached! % 4.68/1.15 % (4032739)------------------------------ % 4.68/1.15 % (4032739)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.68/1.15 % (4032739)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.68/1.15 % (4032739)CaDiCaL version: 2.1.3 % 4.68/1.15 % (4032739)Termination reason: Instruction limit % 4.68/1.15 % (4032739)Termination phase: Saturation % 4.68/1.15 % (4032739)Time elapsed: 0.207 s % 4.68/1.15 % (4032739)Peak memory usage: 117 MB % 4.68/1.15 % (4032739)Instructions burned: 308 (million) % 4.68/1.15 % (4032781)Refutation not found, incomplete strategy % 4.68/1.15 % (4032781)------------------------------ % 4.68/1.15 % (4032781)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.68/1.15 % (4032781)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.35/1.36 % (4032781)CaDiCaL version: 2.1.3 % 5.35/1.36 % (4032781)Termination reason: Refutation not found, incomplete strategy % 5.35/1.36 % (4032781)Time elapsed: 0.013 s % 5.35/1.36 % (4032781)Peak memory usage: 89 MB % 5.35/1.36 % (4032781)Instructions burned: 19 (million) % 5.35/1.36 % (4032783)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=1918825975:i=85:gtgl=4:rtra=on:gtg=exists_sym_2997 on theBenchmark for (2997ds/85Mi) % 5.35/1.36 % (4032783)Instruction limit reached! % 5.35/1.36 % (4032783)------------------------------ % 5.35/1.36 % (4032783)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.35/1.36 % (4032783)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.35/1.36 % (4032783)CaDiCaL version: 2.1.3 % 5.35/1.36 % (4032783)Termination reason: Instruction limit % 5.35/1.36 % (4032783)Termination phase: Saturation % 5.35/1.36 % (4032783)Time elapsed: 0.025 s % 5.35/1.36 % (4032783)Peak memory usage: 89 MB % 5.35/1.36 % (4032783)Instructions burned: 89 (million) % 5.35/1.36 % (4032788)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=3511604720:i=181:rtra=on:ss=axioms:ev=cautious_2996 on theBenchmark for (2996ds/181Mi) % 5.35/1.36 % (4032786)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=2622450090:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2996 on theBenchmark for (2996ds/2Mi) % 5.35/1.36 % (4032789)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=334185955:i=4:ep=RST:ins=2:rtra=on_2996 on theBenchmark for (2996ds/4Mi) % 5.35/1.36 % (4032786)Instruction limit reached! % 5.35/1.36 % (4032786)------------------------------ % 5.35/1.36 % (4032786)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.35/1.36 % (4032786)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.35/1.36 % (4032786)CaDiCaL version: 2.1.3 % 5.35/1.36 % (4032786)Termination reason: Instruction limit % 5.35/1.36 % (4032786)Termination phase: Preprocessing 1 % 5.35/1.36 % (4032786)Time elapsed: 0.002 s % 5.35/1.36 % (4032786)Peak memory usage: 85 MB % 5.35/1.36 % (4032786)Instructions burned: 3 (million) % 5.35/1.36 % (4032789)Instruction limit reached! % 5.35/1.36 % (4032789)------------------------------ % 5.35/1.36 % (4032789)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.35/1.36 % (4032789)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.35/1.36 % (4032789)CaDiCaL version: 2.1.3 % 5.35/1.36 % (4032789)Termination reason: Instruction limit % 5.35/1.36 % (4032789)Termination phase: Preprocessing 3 % 5.35/1.36 % (4032789)Time elapsed: 0.003 s % 5.35/1.36 % (4032789)Peak memory usage: 86 MB % 5.35/1.36 % (4032789)Instructions burned: 4 (million) % 5.35/1.36 % (4032790)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=3522104394:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2996 on theBenchmark for (2996ds/66Mi) % 5.35/1.36 % (4032792)lrs+10_1_thi=all:si=on:fd=off:random_seed=1634975036:i=53:rtra=on:gtg=all_2996 on theBenchmark for (2996ds/53Mi) % 5.35/1.36 % (4032794)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=2527150980:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2995 on theBenchmark for (2995ds/8Mi) % 5.35/1.36 % (4032794)Instruction limit reached! % 5.35/1.36 % (4032794)------------------------------ % 5.35/1.36 % (4032794)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.35/1.36 % (4032794)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.35/1.36 % (4032794)CaDiCaL version: 2.1.3 % 5.35/1.36 % (4032794)Termination reason: Instruction limit % 5.35/1.36 % (4032794)Termination phase: Function definition elimination % 5.35/1.36 % (4032794)Time elapsed: 0.003 s % 5.35/1.36 % (4032794)Peak memory usage: 86 MB % 5.35/1.36 % (4032794)Instructions burned: 10 (million) % 5.35/1.36 % (4032792)Instruction limit reached! % 5.35/1.36 % (4032792)------------------------------ % 5.35/1.36 % (4032792)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.35/1.36 % (4032792)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.35/1.36 % (4032792)CaDiCaL version: 2.1.3 % 5.35/1.36 % (4032792)Termination reason: Instruction limit % 5.35/1.36 % (4032792)Termination phase: Saturation % 5.35/1.36 % (4032792)Time elapsed: 0.061 s % 5.35/1.36 % (4032792)Peak memory usage: 118 MB % 5.35/1.36 % (4032792)Instructions burned: 53 (million) % 7.18/1.59 % (4032788)Instruction limit reached! % 7.18/1.59 % (4032788)------------------------------ % 7.18/1.59 % (4032788)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.18/1.59 % (4032788)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.18/1.59 % (4032788)CaDiCaL version: 2.1.3 % 7.18/1.59 % (4032788)Termination reason: Instruction limit % 7.18/1.59 % (4032788)Termination phase: Saturation % 7.18/1.59 % (4032788)Time elapsed: 0.110 s % 7.18/1.59 % (4032788)Peak memory usage: 90 MB % 7.18/1.59 % (4032788)Instructions burned: 183 (million) % 7.18/1.59 % (4032790)Instruction limit reached! % 7.18/1.59 % (4032790)------------------------------ % 7.18/1.59 % (4032790)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.18/1.59 % (4032790)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.18/1.59 % (4032790)CaDiCaL version: 2.1.3 % 7.18/1.59 % (4032790)Termination reason: Instruction limit % 7.18/1.59 % (4032790)Termination phase: Saturation % 7.18/1.59 % (4032790)Time elapsed: 0.091 s % 7.18/1.59 % (4032790)Peak memory usage: 134 MB % 7.18/1.59 % (4032790)Instructions burned: 66 (million) % 7.18/1.59 % (4032781)------------------------------ % 7.18/1.59 % (4032781)------------------------------ % 7.18/1.59 % (4032799)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=477870713:i=2:doe=on:canc=force:asg=cautious:rtra=on_2995 on theBenchmark for (2995ds/2Mi) % 7.18/1.59 % (4032798)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=2329697079:st=3:i=2:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/2Mi) % 7.18/1.59 % (4032798)Instruction limit reached! % 7.18/1.59 % (4032798)------------------------------ % 7.18/1.59 % (4032798)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.18/1.59 % (4032798)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.18/1.59 % (4032798)CaDiCaL version: 2.1.3 % 7.18/1.59 % (4032798)Termination reason: Instruction limit % 7.18/1.59 % (4032798)Termination phase: Preprocessing 1 % 7.18/1.59 % (4032798)Time elapsed: 0.002 s % 7.18/1.59 % (4032798)Peak memory usage: 85 MB % 7.18/1.59 % (4032798)Instructions burned: 2 (million) % 7.18/1.59 % (4032799)Instruction limit reached! % 7.18/1.59 % (4032799)------------------------------ % 7.18/1.59 % (4032799)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.18/1.59 % (4032799)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.18/1.59 % (4032799)CaDiCaL version: 2.1.3 % 7.18/1.59 % (4032799)Termination reason: Instruction limit % 7.18/1.59 % (4032799)Termination phase: shuffling % 7.18/1.59 % (4032799)Time elapsed: 0.002 s % 7.18/1.59 % (4032799)Peak memory usage: 85 MB % 7.18/1.59 % (4032799)Instructions burned: 3 (million) % 7.18/1.59 % (4032803)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=1241702608:i=127:doe=on:rtra=on_2994 on theBenchmark for (2994ds/127Mi) % 7.18/1.59 % (4032804)dis+10_1_si=on:random_seed=592290470:i=10:ep=R:rtra=on_2994 on theBenchmark for (2994ds/10Mi) % 7.18/1.59 % (4032805)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=4269368936:i=26:canc=cautious:av=off:rtra=on_2994 on theBenchmark for (2994ds/26Mi) % 7.18/1.59 % (4032804)Instruction limit reached! % 7.18/1.59 % (4032804)------------------------------ % 7.18/1.59 % (4032804)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.18/1.59 % (4032804)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.18/1.59 % (4032804)CaDiCaL version: 2.1.3 % 7.18/1.59 % (4032804)Termination reason: Instruction limit % 7.18/1.59 % (4032804)Termination phase: Property scanning % 7.18/1.59 % (4032804)Time elapsed: 0.006 s % 7.18/1.59 % (4032804)Peak memory usage: 87 MB % 7.18/1.59 % (4032804)Instructions burned: 11 (million) % 7.18/1.59 % (4032805)Refutation not found, incomplete strategy % 7.18/1.59 % (4032805)------------------------------ % 7.18/1.59 % (4032805)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.18/1.59 % (4032803)Instruction limit reached! % 7.18/1.59 % (4032803)------------------------------ % 7.18/1.59 % (4032803)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.18/1.59 % (4032803)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.18/1.59 % (4032805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.18/1.59 % (4032803)CaDiCaL version: 2.1.3 % 7.18/1.59 % (4032805)CaDiCaL version: 2.1.3 % 7.18/1.59 % (4032803)Termination reason: Instruction limit % 8.85/1.81 % (4032803)Termination phase: Saturation % 8.85/1.81 % (4032805)Termination reason: Refutation not found, incomplete strategy % 8.85/1.81 % (4032805)Time elapsed: 0.011 s % 8.85/1.81 % (4032803)Time elapsed: 0.064 s % 8.85/1.81 % (4032805)Peak memory usage: 89 MB % 8.85/1.81 % (4032803)Peak memory usage: 117 MB % 8.85/1.81 % (4032805)Instructions burned: 16 (million) % 8.85/1.81 % (4032803)Instructions burned: 127 (million) % 8.85/1.81 % (4032806)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=1392792153:avsq=on:i=35:doe=on:thsqd=64:nm=64:fsr=off:thsqc=32:rtra=on:tac=light:ss=included:thsq=on:ev=off:sgt=32_2993 on theBenchmark for (2993ds/35Mi) % 8.85/1.81 % (4032807)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=428834888:i=2:fsr=off:rtra=on:inst=on_2993 on theBenchmark for (2993ds/2Mi) % 8.85/1.81 % (4032807)Instruction limit reached! % 8.85/1.81 % (4032807)------------------------------ % 8.85/1.81 % (4032807)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.85/1.81 % (4032807)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.85/1.81 % (4032807)CaDiCaL version: 2.1.3 % 8.85/1.81 % (4032807)Termination reason: Instruction limit % 8.85/1.81 % (4032807)Termination phase: Preprocessing 1 % 8.85/1.81 % (4032807)Time elapsed: 0.002 s % 8.85/1.81 % (4032807)Peak memory usage: 85 MB % 8.85/1.81 % (4032807)Instructions burned: 3 (million) % 8.85/1.81 % (4032806)Instruction limit reached! % 8.85/1.81 % (4032806)------------------------------ % 8.85/1.81 % (4032806)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.85/1.81 % (4032806)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.85/1.81 % (4032806)CaDiCaL version: 2.1.3 % 8.85/1.81 % (4032806)Termination reason: Instruction limit % 8.85/1.81 % (4032806)Termination phase: Saturation % 8.85/1.81 % (4032806)Time elapsed: 0.028 s % 8.85/1.81 % (4032806)Peak memory usage: 89 MB % 8.85/1.81 % (4032806)Instructions burned: 37 (million) % 8.85/1.81 % (4032810)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=965947774:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2993 on theBenchmark for (2993ds/8Mi) % 8.85/1.81 % (4032811)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=3018719869:i=370:ep=RS:fsr=off:rtra=on_2993 on theBenchmark for (2993ds/370Mi) % 8.85/1.81 % (4032810)Instruction limit reached! % 8.85/1.81 % (4032810)------------------------------ % 8.85/1.81 % (4032810)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.85/1.81 % (4032810)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.85/1.81 % (4032810)CaDiCaL version: 2.1.3 % 8.85/1.81 % (4032810)Termination reason: Instruction limit % 8.85/1.81 % (4032810)Termination phase: Function definition elimination % 8.85/1.81 % (4032810)Time elapsed: 0.005 s % 8.85/1.81 % (4032810)Peak memory usage: 86 MB % 8.85/1.81 % (4032810)Instructions burned: 8 (million) % 8.85/1.81 % (4032815)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=560122252:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2992 on theBenchmark for (2992ds/13Mi) % 8.85/1.81 % (4032816)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=2715218739:i=226:rtra=on:gtg=position:ss=axioms_2992 on theBenchmark for (2992ds/226Mi) % 8.85/1.81 % (4032815)Instruction limit reached! % 8.85/1.81 % (4032815)------------------------------ % 8.85/1.81 % (4032815)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.85/1.81 % (4032815)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.85/1.81 % (4032815)CaDiCaL version: 2.1.3 % 8.85/1.81 % (4032815)Termination reason: Instruction limit % 8.85/1.81 % (4032815)Termination phase: Saturation % 8.85/1.81 % (4032815)Time elapsed: 0.012 s % 8.85/1.81 % (4032815)Peak memory usage: 92 MB % 8.85/1.81 % (4032815)Instructions burned: 13 (million) % 8.85/1.81 % (4032820)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=3872330912:i=71:rtra=on:gtg=exists_top_2992 on theBenchmark for (2992ds/71Mi) % 8.85/1.81 % (4032819)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=113633117:i=10:rtra=on_2992 on theBenchmark for (2992ds/10Mi) % 8.85/1.81 % (4032819)Instruction limit reached! % 8.85/1.81 % (4032819)------------------------------ % 8.85/1.81 % (4032819)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.48/2.11 % (4032819)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.48/2.11 % (4032819)CaDiCaL version: 2.1.3 % 11.48/2.11 % (4032819)Termination reason: Instruction limit % 11.48/2.11 % (4032819)Termination phase: Saturation % 11.48/2.11 % (4032819)Time elapsed: 0.006 s % 11.48/2.11 % (4032819)Peak memory usage: 88 MB % 11.48/2.11 % (4032819)Instructions burned: 10 (million) % 11.48/2.11 % (4032823)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=1315640726:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2991 on theBenchmark for (2991ds/75Mi) % 11.48/2.11 % (4032820)Instruction limit reached! % 11.48/2.11 % (4032820)------------------------------ % 11.48/2.11 % (4032820)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.48/2.11 % (4032820)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.48/2.11 % (4032820)CaDiCaL version: 2.1.3 % 11.48/2.11 % (4032820)Termination reason: Instruction limit % 11.48/2.11 % (4032820)Termination phase: Saturation % 11.48/2.11 % (4032820)Time elapsed: 0.054 s % 11.48/2.11 % (4032820)Peak memory usage: 133 MB % 11.48/2.11 % (4032820)Instructions burned: 72 (million) % 11.48/2.11 % (4032805)------------------------------ % 11.48/2.11 % (4032805)------------------------------ % 11.48/2.11 % (4032823)Instruction limit reached! % 11.48/2.11 % (4032823)------------------------------ % 11.48/2.11 % (4032823)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.48/2.11 % (4032823)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.48/2.11 % (4032823)CaDiCaL version: 2.1.3 % 11.48/2.11 % (4032823)Termination reason: Instruction limit % 11.48/2.11 % (4032823)Termination phase: Saturation % 11.48/2.11 % (4032823)Time elapsed: 0.053 s % 11.48/2.11 % (4032823)Peak memory usage: 90 MB % 11.48/2.11 % (4032823)Instructions burned: 76 (million) % 11.48/2.11 % (4032811)Instruction limit reached! % 11.48/2.11 % (4032811)------------------------------ % 11.48/2.11 % (4032811)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.48/2.11 % (4032811)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.48/2.11 % (4032811)CaDiCaL version: 2.1.3 % 11.48/2.11 % (4032811)Termination reason: Instruction limit % 11.48/2.11 % (4032811)Termination phase: Saturation % 11.48/2.11 % (4032811)Time elapsed: 0.213 s % 11.48/2.11 % (4032811)Peak memory usage: 91 MB % 11.48/2.11 % (4032811)Instructions burned: 371 (million) % 11.48/2.11 % (4032826)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=461615498:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2990 on theBenchmark for (2990ds/294Mi) % 11.48/2.11 % (4032816)Instruction limit reached! % 11.48/2.11 % (4032816)------------------------------ % 11.48/2.11 % (4032816)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.48/2.11 % (4032816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.48/2.11 % (4032816)CaDiCaL version: 2.1.3 % 11.48/2.11 % (4032816)Termination reason: Instruction limit % 11.48/2.11 % (4032816)Termination phase: Saturation % 11.48/2.11 % (4032816)Time elapsed: 0.174 s % 11.48/2.11 % (4032816)Peak memory usage: 118 MB % 11.48/2.11 % (4032816)Instructions burned: 227 (million) % 11.48/2.11 % (4032831)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=240136600:i=131:rtra=on_2990 on theBenchmark for (2990ds/131Mi) % 11.48/2.11 % (4032829)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=962636562:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2990 on theBenchmark for (2990ds/130Mi) % 11.48/2.11 % (4032832)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=630988248:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2990 on theBenchmark for (2990ds/40Mi) % 11.48/2.11 % (4032831)Instruction limit reached! % 11.48/2.11 % (4032831)------------------------------ % 11.48/2.11 % (4032831)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.48/2.11 % (4032831)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.48/2.11 % (4032831)CaDiCaL version: 2.1.3 % 11.48/2.11 % (4032831)Termination reason: Instruction limit % 11.48/2.11 % (4032831)Termination phase: Saturation % 11.48/2.11 % (4032831)Time elapsed: 0.079 s % 11.48/2.11 % (4032831)Peak memory usage: 134 MB % 11.48/2.11 % (4032831)Instructions burned: 133 (million) % 11.48/2.11 % (4032834)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=547653715:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2989 on theBenchmark for (2989ds/598Mi) % 12.82/2.40 % (4032833)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=620891379:i=307:rtra=on:gtg=exists_top_2989 on theBenchmark for (2989ds/307Mi) % 12.82/2.40 % (4032832)Instruction limit reached! % 12.82/2.40 % (4032832)------------------------------ % 12.82/2.40 % (4032832)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.82/2.40 % (4032832)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.82/2.40 % (4032832)CaDiCaL version: 2.1.3 % 12.82/2.40 % (4032832)Termination reason: Instruction limit % 12.82/2.40 % (4032832)Termination phase: Saturation % 12.82/2.40 % (4032832)Time elapsed: 0.066 s % 12.82/2.40 % (4032832)Peak memory usage: 133 MB % 12.82/2.40 % (4032832)Instructions burned: 41 (million) % 12.82/2.40 % (4032829)Instruction limit reached! % 12.82/2.40 % (4032829)------------------------------ % 12.82/2.40 % (4032829)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.82/2.40 % (4032829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.82/2.40 % (4032829)CaDiCaL version: 2.1.3 % 12.82/2.40 % (4032829)Termination reason: Instruction limit % 12.82/2.40 % (4032829)Termination phase: Saturation % 12.82/2.40 % (4032829)Time elapsed: 0.114 s % 12.82/2.40 % (4032829)Peak memory usage: 117 MB % 12.82/2.40 % (4032829)Instructions burned: 131 (million) % 12.82/2.40 % (4032837)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=1790747769:i=131:canc=cautious:fsr=off:rtra=on_2989 on theBenchmark for (2989ds/131Mi) % 12.82/2.40 % (4032826)Instruction limit reached! % 12.82/2.40 % (4032826)------------------------------ % 12.82/2.40 % (4032826)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.82/2.40 % (4032826)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.82/2.40 % (4032826)CaDiCaL version: 2.1.3 % 12.82/2.40 % (4032826)Termination reason: Instruction limit % 12.82/2.40 % (4032826)Termination phase: Saturation % 12.82/2.40 % (4032826)Time elapsed: 0.201 s % 12.82/2.40 % (4032826)Peak memory usage: 91 MB % 12.82/2.40 % (4032826)Instructions burned: 294 (million) % 12.82/2.40 % (4032840)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=3342354990:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2988 on theBenchmark for (2988ds/259Mi) % 12.82/2.40 % (4032837)Instruction limit reached! % 12.82/2.40 % (4032837)------------------------------ % 12.82/2.40 % (4032837)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.82/2.40 % (4032837)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.82/2.40 % (4032837)CaDiCaL version: 2.1.3 % 12.82/2.40 % (4032837)Termination reason: Instruction limit % 12.82/2.40 % (4032837)Termination phase: Saturation % 12.82/2.40 % (4032837)Time elapsed: 0.115 s % 12.82/2.40 % (4032837)Peak memory usage: 118 MB % 12.82/2.40 % (4032837)Instructions burned: 131 (million) % 12.82/2.40 % (4032843)dis+10_1_si=on:random_seed=3636202304:s2a=on:i=1000:rtra=on:gtg=exists_all_2987 on theBenchmark for (2987ds/1000Mi) % 12.82/2.40 % (4032833)Instruction limit reached! % 12.82/2.40 % (4032833)------------------------------ % 12.82/2.40 % (4032833)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.82/2.40 % (4032833)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.82/2.40 % (4032833)CaDiCaL version: 2.1.3 % 12.82/2.40 % (4032833)Termination reason: Instruction limit % 12.82/2.40 % (4032833)Termination phase: Saturation % 12.82/2.40 % (4032833)Time elapsed: 0.195 s % 12.82/2.40 % (4032833)Peak memory usage: 92 MB % 12.82/2.40 % (4032833)Instructions burned: 308 (million) % 12.82/2.40 % (4032844)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=3194142137:i=383:fsr=off:rtra=on:ev=force_2987 on theBenchmark for (2987ds/383Mi) % 12.82/2.40 % (4032840)Instruction limit reached! % 12.82/2.40 % (4032840)------------------------------ % 12.82/2.40 % (4032840)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.82/2.40 % (4032840)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.82/2.40 % (4032840)CaDiCaL version: 2.1.3 % 12.82/2.40 % (4032840)Termination reason: Instruction limit % 12.82/2.40 % (4032840)Termination phase: Saturation % 12.82/2.40 % (4032840)Time elapsed: 0.105 s % 12.82/2.40 % (4032840)Peak memory usage: 117 MB % 12.82/2.40 % (4032840)Instructions burned: 260 (million) % 15.07/2.70 % (4032846)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=2968591659:i=141:doe=on:rtra=on_2987 on theBenchmark for (2987ds/141Mi) % 15.07/2.70 % (4032849)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=328256194:i=65:nm=16:rtra=on_2986 on theBenchmark for (2986ds/65Mi) % 15.07/2.70 % (4032850)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=551822472:i=121:nm=16:rtra=on_2986 on theBenchmark for (2986ds/121Mi) % 15.07/2.70 % (4032852)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=529805508:s2a=on:i=128:s2at=5:ins=3:rtra=on_2985 on theBenchmark for (2985ds/128Mi) % 15.07/2.70 % (4032846)Instruction limit reached! % 15.07/2.70 % (4032846)------------------------------ % 15.07/2.70 % (4032846)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.07/2.70 % (4032846)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.07/2.70 % (4032846)CaDiCaL version: 2.1.3 % 15.07/2.70 % (4032846)Termination reason: Instruction limit % 15.07/2.70 % (4032846)Termination phase: Saturation % 15.07/2.70 % (4032846)Time elapsed: 0.098 s % 15.07/2.70 % (4032846)Peak memory usage: 90 MB % 15.07/2.70 % (4032846)Instructions burned: 141 (million) % 15.07/2.70 % (4032849)Refutation not found, incomplete strategy % 15.07/2.70 % (4032849)------------------------------ % 15.07/2.70 % (4032849)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.07/2.70 % (4032849)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.07/2.70 % (4032849)CaDiCaL version: 2.1.3 % 15.07/2.70 % (4032849)Termination reason: Refutation not found, incomplete strategy % 15.07/2.70 % (4032849)Time elapsed: 0.044 s % 15.07/2.70 % (4032849)Peak memory usage: 116 MB % 15.07/2.70 % (4032849)Instructions burned: 30 (million) % 15.07/2.70 % (4032852)Instruction limit reached! % 15.07/2.70 % (4032852)------------------------------ % 15.07/2.70 % (4032852)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.07/2.70 % (4032852)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.07/2.70 % (4032852)CaDiCaL version: 2.1.3 % 15.07/2.70 % (4032852)Termination reason: Instruction limit % 15.07/2.70 % (4032852)Termination phase: Saturation % 15.07/2.70 % (4032852)Time elapsed: 0.060 s % 15.07/2.70 % (4032852)Peak memory usage: 117 MB % 15.07/2.70 % (4032852)Instructions burned: 130 (million) % 15.07/2.70 % (4032844)Instruction limit reached! % 15.07/2.70 % (4032844)------------------------------ % 15.07/2.70 % (4032844)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.07/2.70 % (4032844)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.07/2.70 % (4032844)CaDiCaL version: 2.1.3 % 15.07/2.70 % (4032844)Termination reason: Instruction limit % 15.07/2.70 % (4032844)Termination phase: Saturation % 15.07/2.70 % (4032844)Time elapsed: 0.208 s % 15.07/2.70 % (4032844)Peak memory usage: 92 MB % 15.07/2.70 % (4032844)Instructions burned: 390 (million) % 15.07/2.70 % (4032850)Instruction limit reached! % 15.07/2.70 % (4032850)------------------------------ % 15.07/2.70 % (4032850)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.07/2.70 % (4032850)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.07/2.70 % (4032850)CaDiCaL version: 2.1.3 % 15.07/2.70 % (4032850)Termination reason: Instruction limit % 15.07/2.70 % (4032850)Termination phase: Saturation % 15.07/2.70 % (4032850)Time elapsed: 0.079 s % 15.07/2.70 % (4032850)Peak memory usage: 90 MB % 15.07/2.70 % (4032850)Instructions burned: 121 (million) % 15.07/2.70 % (4032834)Instruction limit reached! % 15.07/2.70 % (4032834)------------------------------ % 15.07/2.70 % (4032834)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.07/2.70 % (4032834)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.07/2.70 % (4032834)CaDiCaL version: 2.1.3 % 15.07/2.70 % (4032834)Termination reason: Instruction limit % 15.07/2.70 % (4032834)Termination phase: Saturation % 15.07/2.70 % (4032834)Time elapsed: 0.421 s % 15.07/2.70 % (4032834)Peak memory usage: 138 MB % 15.07/2.70 % (4032834)Instructions burned: 598 (million) % 15.07/2.70 % (4032857)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=361748428:i=39:ins=3:rtra=on_2984 on theBenchmark for (2984ds/39Mi) % 15.07/2.70 % (4032858)dis+1010_1_to=kbo:si=on:random_seed=2918544584:i=175:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2984 on theBenchmark for (2984ds/175Mi) % 16.20/3.01 % (4032857)Instruction limit reached! % 16.20/3.01 % (4032857)------------------------------ % 16.20/3.01 % (4032857)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.20/3.01 % (4032857)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.20/3.01 % (4032857)CaDiCaL version: 2.1.3 % 16.20/3.01 % (4032857)Termination reason: Instruction limit % 16.20/3.01 % (4032857)Termination phase: Saturation % 16.20/3.01 % (4032857)Time elapsed: 0.048 s % 16.20/3.01 % (4032857)Peak memory usage: 116 MB % 16.20/3.01 % (4032857)Instructions burned: 39 (million) % 16.20/3.01 % (4032860)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=1579960315:s2a=on:i=483:doe=on:nm=32:rtra=on_2984 on theBenchmark for (2984ds/483Mi) % 16.20/3.01 % (4032859)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=493690365:i=329:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2984 on theBenchmark for (2984ds/329Mi) % 16.20/3.01 % (4032861)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=2780058237:thitd=on:i=215:nm=0:rtra=on:ev=force_2983 on theBenchmark for (2983ds/215Mi) % 16.20/3.01 % (4032858)Instruction limit reached! % 16.20/3.01 % (4032858)------------------------------ % 16.20/3.01 % (4032858)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.20/3.01 % (4032858)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.20/3.01 % (4032858)CaDiCaL version: 2.1.3 % 16.20/3.01 % (4032858)Termination reason: Instruction limit % 16.20/3.01 % (4032858)Termination phase: Saturation % 16.20/3.01 % (4032858)Time elapsed: 0.067 s % 16.20/3.01 % (4032858)Peak memory usage: 91 MB % 16.20/3.01 % (4032858)Instructions burned: 175 (million) % 16.20/3.01 % (4032849)------------------------------ % 16.20/3.01 % (4032849)------------------------------ % 16.20/3.01 % (4032864)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=531025847:i=349:rtra=on_2982 on theBenchmark for (2982ds/349Mi) % 16.20/3.01 % (4032868)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=1933715357:st=2:i=295:rtra=on:ss=axioms_2982 on theBenchmark for (2982ds/295Mi) % 16.20/3.01 % (4032843)Instruction limit reached! % 16.20/3.01 % (4032843)------------------------------ % 16.20/3.01 % (4032843)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.20/3.01 % (4032843)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.20/3.01 % (4032843)CaDiCaL version: 2.1.3 % 16.20/3.01 % (4032843)Termination reason: Instruction limit % 16.20/3.01 % (4032843)Termination phase: Saturation % 16.20/3.01 % (4032843)Time elapsed: 0.561 s % 16.20/3.01 % (4032843)Peak memory usage: 93 MB % 16.20/3.01 % (4032843)Instructions burned: 1000 (million) % 16.20/3.01 % (4032861)Instruction limit reached! % 16.20/3.01 % (4032861)------------------------------ % 16.20/3.01 % (4032861)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.20/3.01 % (4032861)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.20/3.01 % (4032861)CaDiCaL version: 2.1.3 % 16.20/3.01 % (4032861)Termination reason: Instruction limit % 16.20/3.01 % (4032861)Termination phase: Saturation % 16.20/3.01 % (4032861)Time elapsed: 0.163 s % 16.20/3.01 % (4032861)Peak memory usage: 135 MB % 16.20/3.01 % (4032861)Instructions burned: 217 (million) % 16.20/3.01 % (4032869)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=3943033385:i=328:kws=inv_frequency:nm=20:rtra=on_2982 on theBenchmark for (2982ds/328Mi) % 16.20/3.01 % (4032868)Instruction limit reached! % 16.20/3.01 % (4032868)------------------------------ % 16.20/3.01 % (4032868)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.20/3.01 % (4032868)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.20/3.01 % (4032868)CaDiCaL version: 2.1.3 % 16.20/3.01 % (4032868)Termination reason: Instruction limit % 16.20/3.01 % (4032868)Termination phase: Saturation % 16.20/3.01 % (4032868)Time elapsed: 0.088 s % 16.20/3.01 % (4032868)Peak memory usage: 91 MB % 16.20/3.01 % (4032868)Instructions burned: 297 (million) % 16.20/3.01 % (4032859)Instruction limit reached! % 16.20/3.01 % (4032859)------------------------------ % 16.20/3.01 % (4032859)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.20/3.01 % (4032859)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.73/3.29 % (4032859)CaDiCaL version: 2.1.3 % 19.73/3.29 % (4032859)Termination reason: Instruction limit % 19.73/3.29 % (4032859)Termination phase: Saturation % 19.73/3.29 % (4032859)Time elapsed: 0.249 s % 19.73/3.29 % (4032859)Peak memory usage: 120 MB % 19.73/3.29 % (4032859)Instructions burned: 330 (million) % 19.73/3.29 % (4032872)dis+1010_1_to=lpo:sil=128000:sas=z3:si=on:nwc=5:random_seed=2830699713:i=281:gtgl=2:rtra=on:gtg=all_2980 on theBenchmark for (2980ds/281Mi) % 19.73/3.29 % (4032874)lrs+1010_1_to=kbo:sil=128000:si=on:sos=on:urr=on:uwa=alasca_main:random_seed=1793062158:i=484:doe=on:nm=0:av=off:rtra=on:ss=axioms_2980 on theBenchmark for (2980ds/484Mi) % 19.73/3.29 % (4032875)lrs+21_1_to=kbo:sil=128000:thi=neg_eq:si=on:random_seed=89670552:i=321:canc=force:rtra=on:tac=axiom:ss=axioms:ev=force_2980 on theBenchmark for (2980ds/321Mi) % 19.73/3.29 % (4032860)Instruction limit reached! % 19.73/3.29 % (4032860)------------------------------ % 19.73/3.29 % (4032860)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.73/3.29 % (4032860)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.73/3.29 % (4032860)CaDiCaL version: 2.1.3 % 19.73/3.29 % (4032860)Termination reason: Instruction limit % 19.73/3.29 % (4032860)Termination phase: Saturation % 19.73/3.29 % (4032860)Time elapsed: 0.343 s % 19.73/3.29 % (4032860)Peak memory usage: 135 MB % 19.73/3.29 % (4032860)Instructions burned: 483 (million) % 19.73/3.29 % (4032864)Instruction limit reached! % 19.73/3.29 % (4032864)------------------------------ % 19.73/3.29 % (4032864)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.73/3.29 % (4032864)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.73/3.29 % (4032864)CaDiCaL version: 2.1.3 % 19.73/3.29 % (4032864)Termination reason: Instruction limit % 19.73/3.29 % (4032864)Termination phase: Saturation % 19.73/3.29 % (4032864)Time elapsed: 0.227 s % 19.73/3.29 % (4032864)Peak memory usage: 118 MB % 19.73/3.29 % (4032864)Instructions burned: 350 (million) % 19.73/3.29 % (4032876)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=3032915435:i=416:rtra=on:gtg=position:ss=axioms_2980 on theBenchmark for (2980ds/416Mi) % 19.73/3.29 % (4032869)Instruction limit reached! % 19.73/3.29 % (4032869)------------------------------ % 19.73/3.29 % (4032869)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.73/3.29 % (4032869)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.73/3.29 % (4032869)CaDiCaL version: 2.1.3 % 19.73/3.29 % (4032869)Termination reason: Instruction limit % 19.73/3.29 % (4032869)Termination phase: Saturation % 19.73/3.29 % (4032869)Time elapsed: 0.222 s % 19.73/3.29 % (4032869)Peak memory usage: 117 MB % 19.73/3.29 % (4032869)Instructions burned: 328 (million) % 19.73/3.29 % (4032875)Instruction limit reached! % 19.73/3.29 % (4032875)------------------------------ % 19.73/3.29 % (4032875)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.73/3.29 % (4032875)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.73/3.29 % (4032875)CaDiCaL version: 2.1.3 % 19.73/3.29 % (4032875)Termination reason: Instruction limit % 19.73/3.29 % (4032875)Termination phase: Saturation % 19.73/3.29 % (4032875)Time elapsed: 0.092 s % 19.73/3.29 % (4032875)Peak memory usage: 115 MB % 19.73/3.29 % (4032875)Instructions burned: 321 (million) % 19.73/3.29 % (4032881)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=1726653486:avsq=on:i=276:avsqr=1,2:rtra=on_2978 on theBenchmark for (2978ds/276Mi) % 19.73/3.30 % (4032880)lrs+1010_1_to=kbo:tgt=ground:fde=unused:sas=z3:si=on:sp=unary_frequency:gve=force:spb=goal:tha=off:random_seed=2507510604:i=471:thf=on:kws=precedence:rtra=on_2979 on theBenchmark for (2979ds/471Mi) % 19.73/3.30 % (4032872)Instruction limit reached! % 19.73/3.30 % (4032872)------------------------------ % 19.73/3.30 % (4032872)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.73/3.30 % (4032872)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.73/3.30 % (4032872)CaDiCaL version: 2.1.3 % 19.73/3.30 % (4032872)Termination reason: Instruction limit % 19.73/3.30 % (4032872)Termination phase: Saturation % 19.73/3.30 % (4032872)Time elapsed: 0.200 s % 19.73/3.30 % (4032872)Peak memory usage: 117 MB % 19.73/3.30 % (4032872)Instructions burned: 281 (million) % 19.73/3.30 % (4032884)lrs+10_1_to=kbo:sil=128000:tgt=full:sas=z3:si=on:uwa=func_ext:slsqc=1:flr=on:slsq=on:random_seed=1452678059:i=387:bd=preordered:rtra=on:ss=axioms:sgt=8_2978 on theBenchmark for (2978ds/387Mi) % 21.08/3.81 % (4032883)lrs+1010_2_to=kbo:sil=128000:tgt=ground:fde=unused:sas=z3:si=on:uwa=off:tha=off:nwc=1:random_seed=3693695211:i=375:kws=inv_arity_squared:rtra=on_2978 on theBenchmark for (2978ds/375Mi) % 21.08/3.81 % (4032874)Instruction limit reached! % 21.08/3.81 % (4032874)------------------------------ % 21.08/3.81 % (4032874)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.08/3.81 % (4032874)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.08/3.81 % (4032874)CaDiCaL version: 2.1.3 % 21.08/3.81 % (4032874)Termination reason: Instruction limit % 21.08/3.81 % (4032874)Termination phase: Saturation % 21.08/3.81 % (4032874)Time elapsed: 0.272 s % 21.08/3.81 % (4032874)Peak memory usage: 90 MB % 21.08/3.81 % (4032874)Instructions burned: 484 (million) % 21.08/3.81 % (4032876)Instruction limit reached! % 21.08/3.81 % (4032876)------------------------------ % 21.08/3.81 % (4032876)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.08/3.81 % (4032876)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.08/3.81 % (4032876)CaDiCaL version: 2.1.3 % 21.08/3.81 % (4032876)Termination reason: Instruction limit % 21.08/3.81 % (4032876)Termination phase: Saturation % 21.08/3.81 % (4032876)Time elapsed: 0.284 s % 21.08/3.81 % (4032876)Peak memory usage: 119 MB % 21.08/3.81 % (4032876)Instructions burned: 416 (million) % 21.08/3.81 % (4032884)Instruction limit reached! % 21.08/3.81 % (4032884)------------------------------ % 21.08/3.81 % (4032884)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.08/3.81 % (4032884)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.08/3.81 % (4032884)CaDiCaL version: 2.1.3 % 21.08/3.81 % (4032884)Termination reason: Instruction limit % 21.08/3.81 % (4032884)Termination phase: Saturation % 21.08/3.81 % (4032884)Time elapsed: 0.152 s % 21.08/3.81 % (4032884)Peak memory usage: 119 MB % 21.08/3.81 % (4032884)Instructions burned: 389 (million) % 21.08/3.81 % (4032887)lrs+10_1_to=kbo:sil=128000:fde=none:si=on:norm_ineq=on:urr=on:nwc=0.5:random_seed=3286005195:i=513:kws=frequency:bd=all:rtra=on:gtg=exists_all:ss=axioms:sgt=4_2977 on theBenchmark for (2977ds/513Mi) % 21.08/3.81 % (4032881)Instruction limit reached! % 21.08/3.81 % (4032881)------------------------------ % 21.08/3.81 % (4032881)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.08/3.81 % (4032881)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.08/3.81 % (4032881)CaDiCaL version: 2.1.3 % 21.08/3.81 % (4032881)Termination reason: Instruction limit % 21.08/3.81 % (4032881)Termination phase: Saturation % 21.08/3.81 % (4032881)Time elapsed: 0.250 s % 21.08/3.81 % (4032881)Peak memory usage: 134 MB % 21.08/3.81 % (4032881)Instructions burned: 276 (million) % 21.08/3.81 % (4032890)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=3904446754:i=334:rtra=on_2976 on theBenchmark for (2976ds/334Mi) % 21.08/3.81 % (4032880)Instruction limit reached! % 21.08/3.81 % (4032880)------------------------------ % 21.08/3.81 % (4032880)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.08/3.81 % (4032880)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.08/3.81 % (4032880)CaDiCaL version: 2.1.3 % 21.08/3.81 % (4032880)Termination reason: Instruction limit % 21.08/3.81 % (4032880)Termination phase: Saturation % 21.08/3.81 % (4032880)Time elapsed: 0.293 s % 21.08/3.81 % (4032880)Peak memory usage: 118 MB % 21.08/3.81 % (4032880)Instructions burned: 472 (million) % 21.08/3.81 % (4032883)Instruction limit reached! % 21.08/3.81 % (4032883)------------------------------ % 21.08/3.81 % (4032883)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.08/3.81 % (4032883)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.08/3.81 % (4032883)CaDiCaL version: 2.1.3 % 21.08/3.81 % (4032883)Termination reason: Instruction limit % 21.08/3.81 % (4032883)Termination phase: Saturation % 21.08/3.81 % (4032883)Time elapsed: 0.243 s % 21.08/3.81 % (4032883)Peak memory usage: 118 MB % 21.08/3.81 % (4032883)Instructions burned: 376 (million) % 21.08/3.81 % (4032893)dis+1010_1_to=lpo:sil=128000:thi=all:fde=unused:si=on:sp=reverse_arity:tha=off:random_seed=3717853343:i=341:gtgl=2:rtra=on:gtg=exists_sym:ev=force:fsd=on:fsdmm=1_2975 on theBenchmark for (2975ds/341Mi) % 21.08/3.81 % (4032891)lrs+1010_1_to=kbo:sil=64000:sas=cadical:si=on:sos=on:bce=on:random_seed=1965132792:i=359:rtra=on:gtg=exists_top:ss=axioms_2975 on theBenchmark for (2975ds/359Mi) % 26.24/4.19 % (4032894)lrs-2_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_max:tha=off:random_seed=141819749:st=1.5:i=261:sd=1:kws=precedence:rtra=on:ss=axioms_2974 on theBenchmark for (2974ds/261Mi) % 26.24/4.19 % (4032896)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=3693125302:s2pl=no:i=235:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2974 on theBenchmark for (2974ds/235Mi) % 26.24/4.19 % (4032894)Refutation not found, incomplete strategy % 26.24/4.19 % (4032894)------------------------------ % 26.24/4.19 % (4032894)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.24/4.19 % (4032894)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.24/4.19 % (4032894)CaDiCaL version: 2.1.3 % 26.24/4.19 % (4032894)Termination reason: Refutation not found, incomplete strategy % 26.24/4.19 % (4032894)Time elapsed: 0.031 s % 26.24/4.19 % (4032894)Peak memory usage: 115 MB % 26.24/4.19 % (4032894)Instructions burned: 10 (million) % 26.24/4.19 % (4032893)Instruction limit reached! % 26.24/4.19 % (4032893)------------------------------ % 26.24/4.19 % (4032893)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.24/4.19 % (4032893)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.24/4.19 % (4032893)CaDiCaL version: 2.1.3 % 26.24/4.19 % (4032893)Termination reason: Instruction limit % 26.24/4.19 % (4032893)Termination phase: Saturation % 26.24/4.19 % (4032893)Time elapsed: 0.131 s % 26.24/4.19 % (4032893)Peak memory usage: 120 MB % 26.24/4.19 % (4032893)Instructions burned: 343 (million) % 26.24/4.19 % (4032897)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=2497527858:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2974 on theBenchmark for (2974ds/273Mi) % 26.24/4.19 % (4032887)Instruction limit reached! % 26.24/4.19 % (4032887)------------------------------ % 26.24/4.19 % (4032887)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.24/4.19 % (4032887)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.24/4.19 % (4032887)CaDiCaL version: 2.1.3 % 26.24/4.19 % (4032887)Termination reason: Instruction limit % 26.24/4.19 % (4032887)Termination phase: Saturation % 26.24/4.19 % (4032887)Time elapsed: 0.313 s % 26.24/4.19 % (4032887)Peak memory usage: 93 MB % 26.24/4.19 % (4032887)Instructions burned: 515 (million) % 26.24/4.19 % (4032890)Instruction limit reached! % 26.24/4.19 % (4032890)------------------------------ % 26.24/4.19 % (4032890)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.24/4.19 % (4032890)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.24/4.19 % (4032890)CaDiCaL version: 2.1.3 % 26.24/4.19 % (4032890)Termination reason: Instruction limit % 26.24/4.19 % (4032890)Termination phase: Saturation % 26.24/4.19 % (4032890)Time elapsed: 0.287 s % 26.24/4.19 % (4032890)Peak memory usage: 137 MB % 26.24/4.19 % (4032890)Instructions burned: 334 (million) % 26.24/4.19 % (4032891)Instruction limit reached! % 26.24/4.19 % (4032891)------------------------------ % 26.24/4.19 % (4032891)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.24/4.19 % (4032891)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.24/4.19 % (4032891)CaDiCaL version: 2.1.3 % 26.24/4.19 % (4032891)Termination reason: Instruction limit % 26.24/4.19 % (4032891)Termination phase: Saturation % 26.24/4.19 % (4032891)Time elapsed: 0.224 s % 26.24/4.19 % (4032891)Peak memory usage: 91 MB % 26.24/4.19 % (4032891)Instructions burned: 359 (million) % 26.24/4.19 % (4032903)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=1845876036:i=146:doe=on:rtra=on_2972 on theBenchmark for (2972ds/146Mi) % 26.24/4.19 % (4032896)Instruction limit reached! % 26.24/4.19 % (4032896)------------------------------ % 26.24/4.19 % (4032896)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.24/4.19 % (4032896)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.24/4.19 % (4032896)CaDiCaL version: 2.1.3 % 26.24/4.19 % (4032896)Termination reason: Instruction limit % 26.24/4.19 % (4032896)Termination phase: Saturation % 26.24/4.19 % (4032896)Time elapsed: 0.176 s % 26.24/4.19 % (4032896)Peak memory usage: 117 MB % 26.24/4.19 % (4032896)Instructions burned: 235 (million) % 26.24/4.19 % (4032903)Instruction limit reached! % 26.24/4.19 % (4032903)------------------------------ % 26.24/4.19 % (4032903)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 28.38/4.74 % (4032903)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.38/4.74 % (4032903)CaDiCaL version: 2.1.3 % 28.38/4.74 % (4032903)Termination reason: Instruction limit % 28.38/4.74 % (4032903)Termination phase: Saturation % 28.38/4.74 % (4032903)Time elapsed: 0.054 s % 28.38/4.74 % (4032903)Peak memory usage: 91 MB % 28.38/4.74 % (4032903)Instructions burned: 147 (million) % 28.38/4.74 % (4032897)Instruction limit reached! % 28.38/4.74 % (4032897)------------------------------ % 28.38/4.74 % (4032897)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 28.38/4.74 % (4032897)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.38/4.74 % (4032897)CaDiCaL version: 2.1.3 % 28.38/4.74 % (4032897)Termination reason: Instruction limit % 28.38/4.74 % (4032897)Termination phase: Saturation % 28.38/4.74 % (4032897)Time elapsed: 0.191 s % 28.38/4.74 % (4032897)Peak memory usage: 92 MB % 28.38/4.74 % (4032897)Instructions burned: 275 (million) % 28.38/4.74 % (4032904)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=2832559223:i=4428:doe=on:fsr=off:rtra=on_2972 on theBenchmark for (2972ds/4428Mi) % 28.38/4.74 % (4032894)------------------------------ % 28.38/4.74 % (4032894)------------------------------ % 28.38/4.74 % (4032906)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=1798439309:i=1052:rtra=on_2971 on theBenchmark for (2971ds/1052Mi) % 28.38/4.74 % (4032905)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=4154215993:avsq=on:i=276:avsqr=1,2:rtra=on_2971 on theBenchmark for (2971ds/276Mi) % 28.38/4.74 % (4032910)lrs-1002_1_to=kbo:sas=z3:si=on:norm_ineq=on:sos=on:tha=some:random_seed=410728809:i=107:rtra=on_2970 on theBenchmark for (2970ds/107Mi) % 28.38/4.74 % (4032908)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=2931680207:i=655:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2971 on theBenchmark for (2971ds/655Mi) % 28.38/4.74 % (4032910)Refutation not found, incomplete strategy % 28.38/4.74 % (4032910)------------------------------ % 28.38/4.74 % (4032910)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 28.38/4.74 % (4032910)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.38/4.74 % (4032910)CaDiCaL version: 2.1.3 % 28.38/4.74 % (4032910)Termination reason: Refutation not found, incomplete strategy % 28.38/4.74 % (4032910)Time elapsed: 0.024 s % 28.38/4.74 % (4032910)Peak memory usage: 116 MB % 28.38/4.74 % (4032910)Instructions burned: 27 (million) % 28.38/4.74 % (4032909)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=2165021003:st=5:i=1054:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2971 on theBenchmark for (2971ds/1054Mi) % 28.38/4.74 % (4032912)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=3129999525:s2a=on:i=450:doe=on:nm=32:rtra=on_2970 on theBenchmark for (2970ds/450Mi) % 28.38/4.74 % (4032910)------------------------------ % 28.38/4.74 % (4032910)------------------------------ % 28.38/4.74 % (4032905)Instruction limit reached! % 28.38/4.74 % (4032905)------------------------------ % 28.38/4.74 % (4032905)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 28.38/4.74 % (4032905)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.38/4.74 % (4032905)CaDiCaL version: 2.1.3 % 28.38/4.74 % (4032905)Termination reason: Instruction limit % 28.38/4.74 % (4032905)Termination phase: Saturation % 28.38/4.74 % (4032905)Time elapsed: 0.248 s % 28.38/4.74 % (4032905)Peak memory usage: 134 MB % 28.38/4.74 % (4032905)Instructions burned: 277 (million) % 28.38/4.74 % (4032919)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 % 28.38/4.74 % (4032919)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=3914611360:i=1090:aac=none:nm=0:rtra=on:rawr=on_2968 on theBenchmark for (2968ds/1090Mi) % 28.38/4.74 % (4032920)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=1318412025:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2967 on theBenchmark for (2967ds/130Mi) % 28.38/4.74 % (4032912)Instruction limit reached! % 28.38/4.74 % (4032912)------------------------------ % 32.70/5.09 % (4032912)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.70/5.09 % (4032912)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.70/5.09 % (4032912)CaDiCaL version: 2.1.3 % 32.70/5.09 % (4032912)Termination reason: Instruction limit % 32.70/5.09 % (4032912)Termination phase: Saturation % 32.70/5.09 % (4032912)Time elapsed: 0.273 s % 32.70/5.09 % (4032912)Peak memory usage: 134 MB % 32.70/5.09 % (4032912)Instructions burned: 452 (million) % 32.70/5.09 % (4032908)Instruction limit reached! % 32.70/5.09 % (4032908)------------------------------ % 32.70/5.09 % (4032908)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.70/5.09 % (4032908)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.70/5.09 % (4032908)CaDiCaL version: 2.1.3 % 32.70/5.09 % (4032908)Termination reason: Instruction limit % 32.70/5.09 % (4032908)Termination phase: Saturation % 32.70/5.09 % (4032908)Time elapsed: 0.437 s % 32.70/5.09 % (4032908)Peak memory usage: 93 MB % 32.70/5.09 % (4032908)Instructions burned: 656 (million) % 32.70/5.09 % (4032920)Instruction limit reached! % 32.70/5.09 % (4032920)------------------------------ % 32.70/5.09 % (4032920)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.70/5.09 % (4032920)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.70/5.09 % (4032920)CaDiCaL version: 2.1.3 % 32.70/5.09 % (4032920)Termination reason: Instruction limit % 32.70/5.09 % (4032920)Termination phase: Saturation % 32.70/5.09 % (4032920)Time elapsed: 0.109 s % 32.70/5.09 % (4032920)Peak memory usage: 117 MB % 32.70/5.09 % (4032920)Instructions burned: 131 (million) % 32.70/5.09 % (4032923)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=3508211086:i=312:kws=inv_frequency:nm=20:rtra=on_2965 on theBenchmark for (2965ds/312Mi) % 32.70/5.09 % (4032924)ott+10_1_to=kbo:sil=64000:si=on:sp=reverse_frequency:sos=on:random_seed=3222950190:i=491:doe=on:rtra=on:gtg=position_2965 on theBenchmark for (2965ds/491Mi) % 32.70/5.09 % (4032906)Instruction limit reached! % 32.70/5.09 % (4032906)------------------------------ % 32.70/5.09 % (4032906)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.70/5.09 % (4032906)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.70/5.09 % (4032906)CaDiCaL version: 2.1.3 % 32.70/5.09 % (4032906)Termination reason: Instruction limit % 32.70/5.09 % (4032906)Termination phase: Saturation % 32.70/5.09 % (4032906)Time elapsed: 0.677 s % 32.70/5.09 % (4032906)Peak memory usage: 93 MB % 32.70/5.09 % (4032906)Instructions burned: 1052 (million) % 32.70/5.09 % (4032919)Instruction limit reached! % 32.70/5.09 % (4032919)------------------------------ % 32.70/5.09 % (4032919)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.70/5.09 % (4032919)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.70/5.09 % (4032919)CaDiCaL version: 2.1.3 % 32.70/5.09 % (4032919)Termination reason: Instruction limit % 32.70/5.09 % (4032919)Termination phase: Saturation % 32.70/5.09 % (4032919)Time elapsed: 0.354 s % 32.70/5.09 % (4032919)Peak memory usage: 123 MB % 32.70/5.09 % (4032919)Instructions burned: 1092 (million) % 32.70/5.09 % (4032925)ott+1011_4:1_to=lpo:sil=64000:si=on:spb=intro:random_seed=3347423369:s2a=on:i=835:s2at=2:rtra=on_2965 on theBenchmark for (2965ds/835Mi) % 32.70/5.09 % (4032909)Instruction limit reached! % 32.70/5.09 % (4032909)------------------------------ % 32.70/5.09 % (4032909)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.70/5.09 % (4032909)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.70/5.09 % (4032909)CaDiCaL version: 2.1.3 % 32.70/5.09 % (4032909)Termination reason: Instruction limit % 32.70/5.09 % (4032909)Termination phase: Saturation % 32.70/5.09 % (4032909)Time elapsed: 0.680 s % 32.70/5.09 % (4032909)Peak memory usage: 96 MB % 32.70/5.09 % (4032909)Instructions burned: 1054 (million) % 32.70/5.09 % (4032930)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=2716610995:i=776:doe=on:rtra=on_2963 on theBenchmark for (2963ds/776Mi) % 32.70/5.09 % (4032923)Instruction limit reached! % 32.70/5.09 % (4032923)------------------------------ % 32.70/5.09 % (4032923)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.70/5.09 % (4032923)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.70/5.09 % (4032923)CaDiCaL version: 2.1.3 % 32.70/5.09 % (4032923)Termination reason: Instruction limit % 32.70/5.09 % (4032923)Termination phase: Saturation % 39.83/6.07 % (4032923)Time elapsed: 0.210 s % 39.83/6.07 % (4032923)Peak memory usage: 117 MB % 39.83/6.07 % (4032923)Instructions burned: 312 (million) % 39.83/6.07 % (4032928)ott+1011_2_to=lpo:sil=128000:si=on:sos=on:random_seed=554735506:i=307:bd=preordered:av=off:rtra=on:ev=cautious_2963 on theBenchmark for (2963ds/307Mi) % 39.83/6.07 % (4032931)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=3991073629:s2a=on:i=646:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2962 on theBenchmark for (2962ds/646Mi) % 39.83/6.07 % (4032933)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=631160992:thitd=on:cond=fast:i=784:nm=30:rtra=on:gtg=all:tac=axiom_2962 on theBenchmark for (2962ds/784Mi) % 39.83/6.07 % (4032924)Instruction limit reached! % 39.83/6.07 % (4032924)------------------------------ % 39.83/6.07 % (4032924)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.83/6.07 % (4032924)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.83/6.07 % (4032924)CaDiCaL version: 2.1.3 % 39.83/6.07 % (4032924)Termination reason: Instruction limit % 39.83/6.07 % (4032924)Termination phase: Saturation % 39.83/6.07 % (4032924)Time elapsed: 0.324 s % 39.83/6.07 % (4032924)Peak memory usage: 93 MB % 39.83/6.07 % (4032924)Instructions burned: 492 (million) % 39.83/6.07 % (4032928)Instruction limit reached! % 39.83/6.07 % (4032928)------------------------------ % 39.83/6.07 % (4032928)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.83/6.07 % (4032928)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.83/6.07 % (4032928)CaDiCaL version: 2.1.3 % 39.83/6.07 % (4032928)Termination reason: Instruction limit % 39.83/6.07 % (4032928)Termination phase: Saturation % 39.83/6.07 % (4032928)Time elapsed: 0.206 s % 39.83/6.07 % (4032928)Peak memory usage: 92 MB % 39.83/6.07 % (4032928)Instructions burned: 308 (million) % 39.83/6.07 % (4032930)Instruction limit reached! % 39.83/6.07 % (4032930)------------------------------ % 39.83/6.07 % (4032930)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.83/6.07 % (4032930)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.83/6.07 % (4032930)CaDiCaL version: 2.1.3 % 39.83/6.07 % (4032930)Termination reason: Instruction limit % 39.83/6.07 % (4032930)Termination phase: Saturation % 39.83/6.07 % (4032930)Time elapsed: 0.276 s % 39.83/6.07 % (4032930)Peak memory usage: 123 MB % 39.83/6.07 % (4032930)Instructions burned: 778 (million) % 39.83/6.07 % (4032937)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=740704230:thitd=on:s2a=on:i=1131:add=on:canc=force:bd=all:rtra=on:tac=axiom:ev=off_2960 on theBenchmark for (2960ds/1131Mi) % 39.83/6.07 % (4032925)Instruction limit reached! % 39.83/6.07 % (4032925)------------------------------ % 39.83/6.07 % (4032925)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.83/6.07 % (4032925)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.83/6.07 % (4032925)CaDiCaL version: 2.1.3 % 39.83/6.07 % (4032925)Termination reason: Instruction limit % 39.83/6.07 % (4032925)Termination phase: Saturation % 39.83/6.07 % (4032925)Time elapsed: 0.486 s % 39.83/6.07 % (4032925)Peak memory usage: 94 MB % 39.83/6.07 % (4032925)Instructions burned: 835 (million) % 39.83/6.07 % (4032939)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=589039254:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2959 on theBenchmark for (2959ds/775Mi) % 39.83/6.07 % (4032938)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=3181918026:s2pl=no:i=246:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2959 on theBenchmark for (2959ds/246Mi) % 39.83/6.07 % (4032943)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=4287745640:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2958 on theBenchmark for (2958ds/273Mi) % 39.83/6.07 % (4032931)Instruction limit reached! % 39.83/6.07 % (4032931)------------------------------ % 39.83/6.07 % (4032931)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.83/6.07 % (4032931)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.83/6.07 % (4032931)CaDiCaL version: 2.1.3 % 39.83/6.07 % (4032931)Termination reason: Instruction limit % 39.83/6.07 % (4032931)Termination phase: Saturation % 50.45/7.64 % (4032931)Time elapsed: 0.440 s % 50.45/7.64 % (4032931)Peak memory usage: 139 MB % 50.45/7.64 % (4032931)Instructions burned: 648 (million) % 50.45/7.64 % (4032938)Instruction limit reached! % 50.45/7.64 % (4032938)------------------------------ % 50.45/7.64 % (4032938)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 50.45/7.64 % (4032938)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 50.45/7.64 % (4032938)CaDiCaL version: 2.1.3 % 50.45/7.64 % (4032938)Termination reason: Instruction limit % 50.45/7.64 % (4032938)Termination phase: Saturation % 50.45/7.64 % (4032938)Time elapsed: 0.179 s % 50.45/7.64 % (4032938)Peak memory usage: 117 MB % 50.45/7.64 % (4032938)Instructions burned: 247 (million) % 50.45/7.64 % (4032939)Instruction limit reached! % 50.45/7.64 % (4032939)------------------------------ % 50.45/7.64 % (4032939)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 50.45/7.64 % (4032939)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 50.45/7.64 % (4032939)CaDiCaL version: 2.1.3 % 50.45/7.64 % (4032939)Termination reason: Instruction limit % 50.45/7.64 % (4032939)Termination phase: Saturation % 50.45/7.64 % (4032939)Time elapsed: 0.244 s % 50.45/7.64 % (4032939)Peak memory usage: 93 MB % 50.45/7.64 % (4032939)Instructions burned: 777 (million) % 50.45/7.64 % (4032933)Instruction limit reached! % 50.45/7.64 % (4032933)------------------------------ % 50.45/7.64 % (4032933)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 50.45/7.64 % (4032933)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 50.45/7.64 % (4032933)CaDiCaL version: 2.1.3 % 50.45/7.64 % (4032933)Termination reason: Instruction limit % 50.45/7.64 % (4032933)Termination phase: Saturation % 50.45/7.64 % (4032933)Time elapsed: 0.543 s % 50.45/7.64 % (4032933)Peak memory usage: 122 MB % 50.45/7.64 % (4032933)Instructions burned: 785 (million) % 50.45/7.64 % (4032947)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=2140173913:i=102:nm=16:rtra=on_2956 on theBenchmark for (2956ds/102Mi) % 50.45/7.64 % (4032948)lrs+10_1_to=lpo:sil=128000:si=on:bsr=unit_only:tha=off:random_seed=2039015143:avsq=on:s2a=on:i=1094:s2at=5:avsqr=4463,131072:rtra=on_2956 on theBenchmark for (2956ds/1094Mi) % 50.45/7.64 % (4032943)Instruction limit reached! % 50.45/7.64 % (4032943)------------------------------ % 50.45/7.64 % (4032943)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 50.45/7.64 % (4032943)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 50.45/7.64 % (4032943)CaDiCaL version: 2.1.3 % 50.45/7.64 % (4032943)Termination reason: Instruction limit % 50.45/7.64 % (4032943)Termination phase: Saturation % 50.45/7.64 % (4032943)Time elapsed: 0.193 s % 50.45/7.64 % (4032943)Peak memory usage: 92 MB % 50.45/7.64 % (4032943)Instructions burned: 273 (million) % 50.45/7.64 % (4032949)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=1035141405:i=6400:doe=on:fsr=off:rtra=on_2955 on theBenchmark for (2955ds/6400Mi) % 50.45/7.64 % (4032947)Instruction limit reached! % 50.45/7.64 % (4032947)------------------------------ % 50.45/7.64 % (4032947)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 50.45/7.64 % (4032947)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 50.45/7.64 % (4032947)CaDiCaL version: 2.1.3 % 50.45/7.64 % (4032947)Termination reason: Instruction limit % 50.45/7.64 % (4032947)Termination phase: Saturation % 50.45/7.64 % (4032947)Time elapsed: 0.068 s % 50.45/7.64 % (4032947)Peak memory usage: 89 MB % 50.45/7.64 % (4032947)Instructions burned: 102 (million) % 50.45/7.64 % (4032952)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=855252971:i=868:doe=on:nm=0:rtra=on:gtg=exists_sym_2955 on theBenchmark for (2955ds/868Mi) % 50.45/7.64 % (4032953)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=432727423:i=1846:canc=cautious:fsr=off:rtra=on_2954 on theBenchmark for (2954ds/1846Mi) % 50.45/7.64 % (4032953)Refutation not found, incomplete strategy % 50.45/7.64 % (4032953)------------------------------ % 50.45/7.64 % (4032953)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 50.45/7.64 % (4032953)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 50.45/7.64 % (4032953)CaDiCaL version: 2.1.3 % 50.45/7.64 % (4032953)Termination reason: Refutation not found, incomplete strategy % 62.28/9.26 % (4032953)Time elapsed: 0.013 s % 62.28/9.26 % (4032953)Peak memory usage: 90 MB % 62.28/9.26 % (4032953)Instructions burned: 19 (million) % 62.28/9.26 % (4032955)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=2727081564:s2a=on:i=36816:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2954 on theBenchmark for (2954ds/36816Mi) % 62.28/9.26 % (4032937)Instruction limit reached! % 62.28/9.26 % (4032937)------------------------------ % 62.28/9.26 % (4032937)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 62.28/9.26 % (4032937)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 62.28/9.26 % (4032937)CaDiCaL version: 2.1.3 % 62.28/9.26 % (4032937)Termination reason: Instruction limit % 62.28/9.26 % (4032937)Termination phase: Saturation % 62.28/9.26 % (4032937)Time elapsed: 0.714 s % 62.28/9.26 % (4032937)Peak memory usage: 123 MB % 62.28/9.26 % (4032937)Instructions burned: 1131 (million) % 62.28/9.26 % (4032953)------------------------------ % 62.28/9.26 % (4032953)------------------------------ % 62.28/9.26 % (4032959)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=3327735513:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2951 on theBenchmark for (2951ds/273Mi) % 62.28/9.26 % (4032960)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=945685721:i=863:doe=on:nm=0:rtra=on:gtg=exists_sym_2950 on theBenchmark for (2950ds/863Mi) % 62.28/9.26 % (4032959)Instruction limit reached! % 62.28/9.26 % (4032959)------------------------------ % 62.28/9.26 % (4032959)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 62.28/9.26 % (4032959)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 62.28/9.26 % (4032959)CaDiCaL version: 2.1.3 % 62.28/9.26 % (4032959)Termination reason: Instruction limit % 62.28/9.26 % (4032959)Termination phase: Saturation % 62.28/9.26 % (4032959)Time elapsed: 0.192 s % 62.28/9.26 % (4032959)Peak memory usage: 92 MB % 62.28/9.26 % (4032959)Instructions burned: 273 (million) % 62.28/9.26 % (4032948)Instruction limit reached! % 62.28/9.26 % (4032948)------------------------------ % 62.28/9.26 % (4032948)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 62.28/9.26 % (4032948)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 62.28/9.26 % (4032948)CaDiCaL version: 2.1.3 % 62.28/9.26 % (4032948)Termination reason: Instruction limit % 62.28/9.26 % (4032948)Termination phase: Saturation % 62.28/9.26 % (4032948)Time elapsed: 0.690 s % 62.28/9.26 % (4032948)Peak memory usage: 97 MB % 62.28/9.26 % (4032948)Instructions burned: 1095 (million) % 62.28/9.26 % (4032952)Instruction limit reached! % 62.28/9.26 % (4032952)------------------------------ % 62.28/9.26 % (4032952)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 62.28/9.26 % (4032952)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 62.28/9.26 % (4032952)CaDiCaL version: 2.1.3 % 62.28/9.26 % (4032952)Termination reason: Instruction limit % 62.28/9.26 % (4032952)Termination phase: Saturation % 62.28/9.26 % (4032952)Time elapsed: 0.589 s % 62.28/9.26 % (4032952)Peak memory usage: 122 MB % 62.28/9.26 % (4032952)Instructions burned: 869 (million) % 62.28/9.26 % (4032963)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=4225499540:i=5811:kws=precedence:nm=0:rtra=on_2948 on theBenchmark for (2948ds/5811Mi) % 62.28/9.26 % (4032964)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=4069481314:i=2216:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2948 on theBenchmark for (2948ds/2216Mi) % 62.28/9.26 % (4032965)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=191148888:i=801:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2947 on theBenchmark for (2947ds/801Mi) % 62.28/9.26 % (4032904)Instruction limit reached! % 62.28/9.26 % (4032904)------------------------------ % 62.28/9.26 % (4032904)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 62.28/9.26 % (4032904)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 62.28/9.26 % (4032904)CaDiCaL version: 2.1.3 % 62.28/9.26 % (4032904)Termination reason: Instruction limit % 62.28/9.26 % (4032904)Termination phase: Saturation % 62.28/9.26 % (4032904)Time elapsed: 2.679 s % 62.28/9.26 % (4032904)Peak memory usage: 121 MB % 62.28/9.26 % (4032904)Instructions burned: 4429 (million) % 62.28/9.26 % (4032960)Instruction limit reached! % 62.28/9.26 % (4032960)------------------------------ % 93.52/13.69 % (4032960)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 93.52/13.69 % (4032960)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 93.52/13.69 % (4032960)CaDiCaL version: 2.1.3 % 93.52/13.69 % (4032960)Termination reason: Instruction limit % 93.52/13.69 % (4032960)Termination phase: Saturation % 93.52/13.69 % (4032960)Time elapsed: 0.583 s % 93.52/13.69 % (4032960)Peak memory usage: 121 MB % 93.52/13.69 % (4032960)Instructions burned: 865 (million) % 93.52/13.69 % (4032969)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=1220536778:st=5:i=1026:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2943 on theBenchmark for (2943ds/1026Mi) % 93.52/13.69 % (4032970)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=3239895722:i=3509:rtra=on_2943 on theBenchmark for (2943ds/3509Mi) % 93.52/13.69 % (4032965)Instruction limit reached! % 93.52/13.69 % (4032965)------------------------------ % 93.52/13.69 % (4032965)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 93.52/13.69 % (4032965)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 93.52/13.69 % (4032965)CaDiCaL version: 2.1.3 % 93.52/13.69 % (4032965)Termination reason: Instruction limit % 93.52/13.69 % (4032965)Termination phase: Saturation % 93.52/13.69 % (4032965)Time elapsed: 0.510 s % 93.52/13.69 % (4032965)Peak memory usage: 95 MB % 93.52/13.69 % (4032965)Instructions burned: 802 (million) % 93.52/13.69 % (4032973)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=4161650156:st=2:i=2127:sd=12:ep=R:rtra=on:ss=axioms_2940 on theBenchmark for (2940ds/2127Mi) % 93.52/13.69 % (4032969)Instruction limit reached! % 93.52/13.69 % (4032969)------------------------------ % 93.52/13.69 % (4032969)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 93.52/13.69 % (4032969)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 93.52/13.69 % (4032969)CaDiCaL version: 2.1.3 % 93.52/13.69 % (4032969)Termination reason: Instruction limit % 93.52/13.69 % (4032969)Termination phase: Saturation % 93.52/13.69 % (4032969)Time elapsed: 0.649 s % 93.52/13.69 % (4032969)Peak memory usage: 96 MB % 93.52/13.69 % (4032969)Instructions burned: 1027 (million) % 93.52/13.69 % (4032949)Instruction limit reached! % 93.52/13.69 % (4032949)------------------------------ % 93.52/13.69 % (4032949)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 93.52/13.69 % (4032949)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 93.52/13.69 % (4032949)CaDiCaL version: 2.1.3 % 93.52/13.69 % (4032949)Termination reason: Instruction limit % 93.52/13.69 % (4032949)Termination phase: Saturation % 93.52/13.69 % (4032949)Time elapsed: 2.019 s % 93.52/13.69 % (4032949)Peak memory usage: 131 MB % 93.52/13.69 % (4032949)Instructions burned: 6400 (million) % 93.52/13.69 % (4032975)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=2104687934:i=1959:rtra=on:fsd=on:proc=on_2935 on theBenchmark for (2935ds/1959Mi) % 93.52/13.69 % (4032976)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=479642520:s2a=on:i=3553:nm=0:rtra=on_2934 on theBenchmark for (2934ds/3553Mi) % 93.52/13.69 % (4032964)Instruction limit reached! % 93.52/13.69 % (4032964)------------------------------ % 93.52/13.69 % (4032964)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 93.52/13.69 % (4032964)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 93.52/13.69 % (4032964)CaDiCaL version: 2.1.3 % 93.52/13.69 % (4032964)Termination reason: Instruction limit % 93.52/13.69 % (4032964)Termination phase: Saturation % 93.52/13.69 % (4032964)Time elapsed: 1.361 s % 93.52/13.69 % (4032964)Peak memory usage: 132 MB % 93.52/13.69 % (4032964)Instructions burned: 2216 (million) % 93.52/13.69 % (4032979)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=1829456673:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2933 on theBenchmark for (2933ds/3201Mi) % 93.52/13.69 % (4032973)Instruction limit reached! % 93.52/13.69 % (4032973)------------------------------ % 93.52/13.69 % (4032973)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 93.52/13.69 % (4032973)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 93.52/13.69 % (4032973)CaDiCaL version: 2.1.3 % 93.52/13.69 % (4032973)Termination reason: Instruction limit % 93.52/13.69 % (4032973)Termination phase: Saturation % 93.52/13.69 % (4032973)Time elapsed: 1.149 s % 93.52/13.69 % (4032973)Peak memory usage: 99 MB % 93.52/13.69 % (4032973)Instructions burned: 2129 (million) % 112.52/16.39 % (4032981)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=970472454:thitd=on:cond=on:i=4093:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2927 on theBenchmark for (2927ds/4093Mi) % 112.52/16.39 % (4032976)Instruction limit reached! % 112.52/16.39 % (4032976)------------------------------ % 112.52/16.39 % (4032976)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 112.52/16.39 % (4032976)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.52/16.39 % (4032976)CaDiCaL version: 2.1.3 % 112.52/16.39 % (4032976)Termination reason: Instruction limit % 112.52/16.39 % (4032976)Termination phase: Saturation % 112.52/16.39 % (4032976)Time elapsed: 1.094 s % 112.52/16.39 % (4032976)Peak memory usage: 98 MB % 112.52/16.39 % (4032976)Instructions burned: 3554 (million) % 112.52/16.39 % (4032975)Instruction limit reached! % 112.52/16.39 % (4032975)------------------------------ % 112.52/16.39 % (4032975)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 112.52/16.39 % (4032975)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.52/16.39 % (4032975)CaDiCaL version: 2.1.3 % 112.52/16.39 % (4032975)Termination reason: Instruction limit % 112.52/16.39 % (4032975)Termination phase: Saturation % 112.52/16.39 % (4032975)Time elapsed: 1.234 s % 112.52/16.39 % (4032975)Peak memory usage: 125 MB % 112.52/16.39 % (4032975)Instructions burned: 1961 (million) % 112.52/16.39 % (4032983)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=3762459773:cond=fast:i=21173:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2922 on theBenchmark for (2922ds/21173Mi) % 112.52/16.39 % (4032984)lrs+11_1_to=lpo:thi=all:sas=z3:si=on:fd=off:sac=on:slsq=on:random_seed=920170756:avsq=on:i=10544:avsqr=17,4:canc=force:rtra=on:gtg=exists_top:er=filter_2921 on theBenchmark for (2921ds/10544Mi) % 112.52/16.39 % (4032970)Instruction limit reached! % 112.52/16.39 % (4032970)------------------------------ % 112.52/16.39 % (4032970)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 112.52/16.39 % (4032970)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.52/16.39 % (4032970)CaDiCaL version: 2.1.3 % 112.52/16.39 % (4032970)Termination reason: Instruction limit % 112.52/16.39 % (4032970)Termination phase: Saturation % 112.52/16.39 % (4032970)Time elapsed: 2.303 s % 112.52/16.39 % (4032970)Peak memory usage: 110 MB % 112.52/16.39 % (4032970)Instructions burned: 3510 (million) % 112.52/16.39 % (4032979)Instruction limit reached! % 112.52/16.39 % (4032979)------------------------------ % 112.52/16.39 % (4032979)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 112.52/16.39 % (4032979)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.52/16.39 % (4032979)CaDiCaL version: 2.1.3 % 112.52/16.39 % (4032979)Termination reason: Instruction limit % 112.52/16.39 % (4032979)Termination phase: Saturation % 112.52/16.39 % (4032979)Time elapsed: 1.407 s % 112.52/16.39 % (4032979)Peak memory usage: 96 MB % 112.52/16.39 % (4032979)Instructions burned: 3201 (million) % 112.52/16.39 % (4032987)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=714088213:avsq=on:i=1262:avsqr=1,16:rtra=on:rawr=on_2918 on theBenchmark for (2918ds/1262Mi) % 112.52/16.39 % (4032988)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=3996148260:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2917 on theBenchmark for (2917ds/775Mi) % 112.52/16.39 % (4032963)Instruction limit reached! % 112.52/16.39 % (4032963)------------------------------ % 112.52/16.39 % (4032963)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 112.52/16.39 % (4032963)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.52/16.39 % (4032963)CaDiCaL version: 2.1.3 % 112.52/16.39 % (4032963)Termination reason: Instruction limit % 112.52/16.39 % (4032963)Termination phase: Saturation % 112.52/16.39 % (4032963)Time elapsed: 3.179 s % 112.52/16.39 % (4032963)Peak memory usage: 130 MB % 112.52/16.39 % (4032963)Instructions burned: 5812 (million) % 112.52/16.39 % (4032991)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=2801830929:i=270:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2915 on theBenchmark for (2915ds/270Mi) % 112.52/16.39 % (4032991)Instruction limit reached! % 112.52/16.39 % (4032991)------------------------------ % 112.52/16.39 % (4032991)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 127.13/18.45 % (4032991)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 127.13/18.45 % (4032991)CaDiCaL version: 2.1.3 % 127.13/18.45 % (4032991)Termination reason: Instruction limit % 127.13/18.45 % (4032991)Termination phase: Saturation % 127.13/18.45 % (4032991)Time elapsed: 0.189 s % 127.13/18.45 % (4032991)Peak memory usage: 92 MB % 127.13/18.45 % (4032991)Instructions burned: 271 (million) % 127.13/18.45 % (4032988)Instruction limit reached! % 127.13/18.45 % (4032988)------------------------------ % 127.13/18.45 % (4032988)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 127.13/18.45 % (4032988)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 127.13/18.45 % (4032988)CaDiCaL version: 2.1.3 % 127.13/18.45 % (4032988)Termination reason: Instruction limit % 127.13/18.45 % (4032988)Termination phase: Saturation % 127.13/18.45 % (4032988)Time elapsed: 0.459 s % 127.13/18.45 % (4032988)Peak memory usage: 93 MB % 127.13/18.45 % (4032988)Instructions burned: 775 (million) % 127.13/18.45 % (4032987)Instruction limit reached! % 127.13/18.45 % (4032987)------------------------------ % 127.13/18.45 % (4032987)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 127.13/18.45 % (4032987)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 127.13/18.45 % (4032987)CaDiCaL version: 2.1.3 % 127.13/18.45 % (4032987)Termination reason: Instruction limit % 127.13/18.45 % (4032987)Termination phase: Saturation % 127.13/18.45 % (4032987)Time elapsed: 0.683 s % 127.13/18.45 % (4032987)Peak memory usage: 120 MB % 127.13/18.45 % (4032987)Instructions burned: 1263 (million) % 127.13/18.45 % (4032993)ott+10_128_isp=bottom:to=lpo:sil=128000:si=on:urr=on:uwa=alasca_main:sac=on:slsq=on:random_seed=209326149:i=17165:aac=none:doe=on:rtra=on:gtg=exists_all_2911 on theBenchmark for (2911ds/17165Mi) % 127.13/18.45 % (4032994)lrs+2_10_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_main:tha=some:random_seed=1352070947:s2a=on:i=13094:s2at=-1:rtra=on_2911 on theBenchmark for (2911ds/13094Mi) % 127.13/18.45 % (4032995)lrs+10_1_to=lpo:sil=128000:si=on:sp=occurrence:random_seed=4006753200:st=2:i=12633:rtra=on:ss=axioms_2910 on theBenchmark for (2910ds/12633Mi) % 127.13/18.45 % (4032981)Instruction limit reached! % 127.13/18.45 % (4032981)------------------------------ % 127.13/18.45 % (4032981)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 127.13/18.45 % (4032981)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 127.13/18.45 % (4032981)CaDiCaL version: 2.1.3 % 127.13/18.45 % (4032981)Termination reason: Instruction limit % 127.13/18.45 % (4032981)Termination phase: Saturation % 127.13/18.45 % (4032981)Time elapsed: 2.455 s % 127.13/18.45 % (4032981)Peak memory usage: 151 MB % 127.13/18.45 % (4032981)Instructions burned: 4095 (million) % 127.13/18.45 % (4032999)dis+1011_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_frequency:lsd=20:nwc=3:random_seed=1347862149:i=1783:rtra=on:gtg=position_2901 on theBenchmark for (2901ds/1783Mi) % 127.13/18.45 % (4032999)Instruction limit reached! % 127.13/18.45 % (4032999)------------------------------ % 127.13/18.45 % (4032999)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 127.13/18.45 % (4032999)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 127.13/18.45 % (4032999)CaDiCaL version: 2.1.3 % 127.13/18.45 % (4032999)Termination reason: Instruction limit % 127.13/18.45 % (4032999)Termination phase: Saturation % 127.13/18.45 % (4032999)Time elapsed: 1.076 s % 127.13/18.45 % (4032999)Peak memory usage: 123 MB % 127.13/18.45 % (4032999)Instructions burned: 1783 (million) % 127.13/18.45 % (4033001)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=3669308850:i=5451:aac=none:doe=on:nm=0:rtra=on:amm=off:gtg=position_2888 on theBenchmark for (2888ds/5451Mi) % 127.13/18.45 % (4032983)Instruction limit reached! % 127.13/18.45 % (4032983)------------------------------ % 127.13/18.45 % (4032983)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 127.13/18.45 % (4032983)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 127.13/18.45 % (4032983)CaDiCaL version: 2.1.3 % 127.13/18.45 % (4032983)Termination reason: Instruction limit % 127.13/18.45 % (4032983)Termination phase: Saturation % 127.13/18.45 % (4032983)Time elapsed: 5.257 s % 127.13/18.45 % (4032983)Peak memory usage: 139 MB % 127.13/18.45 % (4032983)Instructions burned: 21175 (million) % 127.13/18.45 % (4033003)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=2219396257:i=4975:doe=on:nm=0:rtra=on:gtg=exists_sym_2868 on theBenchmark for (2868ds/4975Mi) % 173.03/24.83 % (4032984)Instruction limit reached! % 173.03/24.83 % (4032984)------------------------------ % 173.03/24.83 % (4032984)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 173.03/24.83 % (4032984)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 173.03/24.83 % (4032984)CaDiCaL version: 2.1.3 % 173.03/24.83 % (4032984)Termination reason: Instruction limit % 173.03/24.83 % (4032984)Termination phase: Saturation % 173.03/24.83 % (4032984)Time elapsed: 6.538 s % 173.03/24.83 % (4032984)Peak memory usage: 237 MB % 173.03/24.83 % (4032984)Instructions burned: 10545 (million) % 173.03/24.83 % (4033001)Instruction limit reached! % 173.03/24.83 % (4033001)------------------------------ % 173.03/24.83 % (4033001)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 173.03/24.83 % (4033001)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 173.03/24.83 % (4033001)CaDiCaL version: 2.1.3 % 173.03/24.83 % (4033001)Termination reason: Instruction limit % 173.03/24.83 % (4033001)Termination phase: Saturation % 173.03/24.83 % (4033001)Time elapsed: 3.255 s % 173.03/24.83 % (4033001)Peak memory usage: 147 MB % 173.03/24.83 % (4033001)Instructions burned: 5460 (million) % 173.03/24.83 % (4033213)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=2130444575:i=5145:rtra=on_2854 on theBenchmark for (2854ds/5145Mi) % 173.03/24.83 % (4033212)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=2084901901:i=2076:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2854 on theBenchmark for (2854ds/2076Mi) % 173.03/24.83 % (4033003)Instruction limit reached! % 173.03/24.83 % (4033003)------------------------------ % 173.03/24.83 % (4033003)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 173.03/24.83 % (4033003)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 173.03/24.83 % (4033003)CaDiCaL version: 2.1.3 % 173.03/24.83 % (4033003)Termination reason: Instruction limit % 173.03/24.83 % (4033003)Termination phase: Saturation % 173.03/24.83 % (4033003)Time elapsed: 1.628 s % 173.03/24.83 % (4033003)Peak memory usage: 137 MB % 173.03/24.83 % (4033003)Instructions burned: 4976 (million) % 173.03/24.83 % (4033351)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=2310595098:i=3509:rtra=on_2850 on theBenchmark for (2850ds/3509Mi) % 173.03/24.83 % (4032995)Instruction limit reached! % 173.03/24.83 % (4032995)------------------------------ % 173.03/24.83 % (4032995)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 173.03/24.83 % (4032995)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 173.03/24.83 % (4032995)CaDiCaL version: 2.1.3 % 173.03/24.83 % (4032995)Termination reason: Instruction limit % 173.03/24.83 % (4032995)Termination phase: Saturation % 173.03/24.83 % (4032995)Time elapsed: 6.270 s % 173.03/24.83 % (4032995)Peak memory usage: 150 MB % 173.03/24.83 % (4032995)Instructions burned: 12633 (million) % 173.03/24.83 % (4033370)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=3650652825:st=2:i=13800:sd=12:ep=R:rtra=on:ss=axioms_2845 on theBenchmark for (2845ds/13800Mi) % 173.03/24.83 % (4032994)Instruction limit reached! % 173.03/24.83 % (4032994)------------------------------ % 173.03/24.83 % (4032994)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 173.03/24.83 % (4032994)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 173.03/24.83 % (4032994)CaDiCaL version: 2.1.3 % 173.03/24.83 % (4032994)Termination reason: Instruction limit % 173.03/24.83 % (4032994)Termination phase: Saturation % 173.03/24.83 % (4032994)Time elapsed: 6.621 s % 173.03/24.83 % (4032994)Peak memory usage: 96 MB % 173.03/24.83 % (4032994)Instructions burned: 13095 (million) % 173.03/24.83 % (4033372)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=3600050661:i=1412:rtra=on:fsd=on:proc=on_2843 on theBenchmark for (2843ds/1412Mi) % 173.03/24.83 % (4033212)Instruction limit reached! % 173.03/24.83 % (4033212)------------------------------ % 173.03/24.83 % (4033212)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 173.03/24.83 % (4033212)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 173.03/24.83 % (4033212)CaDiCaL version: 2.1.3 % 173.03/24.83 % (4033212)Termination reason: Instruction limit % 173.03/24.83 % (4033212)Termination phase: Saturation % 173.03/24.83 % (4033212)Time elapsed: 1.285 s % 173.03/24.83 % (4033212)Peak memory usage: 129 MB % 173.03/24.83 % (4033212)Instructions burned: 2076 (million) % 236.98/33.89 % (4033374)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 % 236.98/33.89 % (4033374)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=4240354833:i=11747:aac=none:nm=0:rtra=on:rawr=on_2840 on theBenchmark for (2840ds/11747Mi) % 236.98/33.89 % (4033351)Instruction limit reached! % 236.98/33.89 % (4033351)------------------------------ % 236.98/33.89 % (4033351)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 236.98/33.89 % (4033351)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 236.98/33.89 % (4033351)CaDiCaL version: 2.1.3 % 236.98/33.89 % (4033351)Termination reason: Instruction limit % 236.98/33.89 % (4033351)Termination phase: Saturation % 236.98/33.89 % (4033351)Time elapsed: 1.223 s % 236.98/33.89 % (4033351)Peak memory usage: 111 MB % 236.98/33.89 % (4033351)Instructions burned: 3509 (million) % 236.98/33.89 % (4033376)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=679448080:s2a=on:i=3553:nm=0:rtra=on_2837 on theBenchmark for (2837ds/3553Mi) % 236.98/33.89 % (4033372)Instruction limit reached! % 236.98/33.89 % (4033372)------------------------------ % 236.98/33.89 % (4033372)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 236.98/33.89 % (4033372)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 236.98/33.89 % (4033372)CaDiCaL version: 2.1.3 % 236.98/33.89 % (4033372)Termination reason: Instruction limit % 236.98/33.89 % (4033372)Termination phase: Saturation % 236.98/33.89 % (4033372)Time elapsed: 0.963 s % 236.98/33.89 % (4033372)Peak memory usage: 125 MB % 236.98/33.89 % (4033372)Instructions burned: 1413 (million) % 236.98/33.89 % (4033378)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=573125808:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2831 on theBenchmark for (2831ds/3201Mi) % 236.98/33.89 % (4033376)Instruction limit reached! % 236.98/33.89 % (4033376)------------------------------ % 236.98/33.89 % (4033376)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 236.98/33.89 % (4033376)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 236.98/33.89 % (4033376)CaDiCaL version: 2.1.3 % 236.98/33.89 % (4033376)Termination reason: Instruction limit % 236.98/33.89 % (4033376)Termination phase: Saturation % 236.98/33.89 % (4033376)Time elapsed: 1.103 s % 236.98/33.89 % (4033376)Peak memory usage: 98 MB % 236.98/33.89 % (4033376)Instructions burned: 3553 (million) % 236.98/33.89 % (4032993)Instruction limit reached! % 236.98/33.89 % (4032993)------------------------------ % 236.98/33.89 % (4032993)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 236.98/33.89 % (4032993)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 236.98/33.89 % (4032993)CaDiCaL version: 2.1.3 % 236.98/33.89 % (4032993)Termination reason: Instruction limit % 236.98/33.89 % (4032993)Termination phase: Saturation % 236.98/33.89 % (4032993)Time elapsed: 8.595 s % 236.98/33.89 % (4032993)Peak memory usage: 211 MB % 236.98/33.89 % (4032993)Instructions burned: 17166 (million) % 236.98/33.89 % (4033380)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=3278776684:thitd=on:cond=on:i=4081:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2825 on theBenchmark for (2825ds/4081Mi) % 236.98/33.89 % (4033381)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=2674565500:cond=fast:i=20260:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2823 on theBenchmark for (2823ds/20260Mi) % 236.98/33.89 % (4033213)Instruction limit reached! % 236.98/33.89 % (4033213)------------------------------ % 236.98/33.89 % (4033213)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 236.98/33.89 % (4033213)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 236.98/33.89 % (4033213)CaDiCaL version: 2.1.3 % 236.98/33.89 % (4033213)Termination reason: Instruction limit % 236.98/33.89 % (4033213)Termination phase: Saturation % 236.98/33.89 % (4033213)Time elapsed: 3.181 s % 236.98/33.89 % (4033213)Peak memory usage: 107 MB % 236.98/33.89 % (4033213)Instructions burned: 5147 (million) % 236.98/33.89 % (4033384)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=788841105:s2a=on:i=58627:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2821 on theBenchmark for (2Terminated %------------------------------------------------------------------------------