%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWX136_1 : TPTP v9.3.1. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % Computer : n010.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:45:57 PM UTC 2026 % Result : Timeout 289.45s 41.55s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWX136_1 : TPTP v9.3.1. Released v9.3.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.11/0.23 % Computer : n010.cluster.edu % 0.11/0.23 % Model : x86_64 x86_64 % 0.11/0.23 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.23 % Memory : 8046.5625MB % 0.11/0.23 % OS : Linux 6.8.0-71-generic % 0.11/0.23 % CPULimit : 300 % 0.11/0.23 % WCLimit : 300 % 0.11/0.23 % DateTime : Mon Sep 28 15:03:32 UTC 2026 % 0.11/0.23 % CPUTime : % 0.11/0.24 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.25/0.29 Running first-order theorem proving % 0.25/0.29 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 4.56/1.43 % (1989645)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule. % 4.56/1.43 % (1989650)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=52011106:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi) % 4.56/1.43 % (1989650)Instruction limit reached! % 4.56/1.43 % (1989650)------------------------------ % 4.56/1.43 % (1989650)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.56/1.43 % (1989650)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.56/1.43 % (1989650)CaDiCaL version: 2.1.3 % 4.56/1.43 % (1989650)Termination reason: Instruction limit % 4.56/1.43 % (1989650)Termination phase: Property scanning % 4.56/1.43 % (1989650)Time elapsed: 0.003 s % 4.56/1.43 % (1989650)Peak memory usage: 85 MB % 4.56/1.43 % (1989650)Instructions burned: 14 (million) % 4.56/1.43 % (1989656)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=936580359:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi) % 4.56/1.43 % (1989653)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=3246128779:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi) % 4.56/1.43 % (1989654)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=2317246047:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi) % 4.56/1.43 % (1989655)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=1755586643:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi) % 4.56/1.43 % (1989651)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=2976550336:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi) % 4.56/1.43 % (1989652)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=3064201374:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi) % 4.56/1.43 % (1989654)Instruction limit reached! % 4.56/1.43 % (1989654)------------------------------ % 4.56/1.43 % (1989654)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.56/1.43 % (1989654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.56/1.43 % (1989654)CaDiCaL version: 2.1.3 % 4.56/1.43 % (1989654)Termination reason: Instruction limit % 4.56/1.43 % (1989654)Termination phase: shuffling % 4.56/1.43 % (1989654)Time elapsed: 0.003 s % 4.56/1.43 % (1989654)Peak memory usage: 85 MB % 4.56/1.43 % (1989654)Instructions burned: 4 (million) % 4.56/1.43 % (1989653)Instruction limit reached! % 4.56/1.43 % (1989653)------------------------------ % 4.56/1.43 % (1989653)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.56/1.43 % (1989653)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.56/1.43 % (1989653)CaDiCaL version: 2.1.3 % 4.56/1.43 % (1989653)Termination reason: Instruction limit % 4.56/1.43 % (1989653)Termination phase: Property scanning % 4.56/1.43 % (1989653)Time elapsed: 0.005 s % 4.56/1.43 % (1989653)Peak memory usage: 85 MB % 4.56/1.43 % (1989653)Instructions burned: 7 (million) % 4.56/1.43 % (1989656)Instruction limit reached! % 4.56/1.43 % (1989656)------------------------------ % 4.56/1.43 % (1989656)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.56/1.43 % (1989656)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.56/1.43 % (1989656)CaDiCaL version: 2.1.3 % 4.56/1.43 % (1989656)Termination reason: Instruction limit % 4.56/1.43 % (1989656)Termination phase: Property scanning % 4.56/1.43 % (1989656)Time elapsed: 0.016 s % 4.56/1.43 % (1989656)Peak memory usage: 85 MB % 4.56/1.43 % (1989656)Instructions burned: 33 (million) % 4.56/1.43 % (1989655)Instruction limit reached! % 4.56/1.43 % (1989655)------------------------------ % 4.56/1.43 % (1989655)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.56/1.43 % (1989655)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.56/1.43 % (1989655)CaDiCaL version: 2.1.3 % 4.56/1.43 % (1989655)Termination reason: Instruction limit % 4.56/1.43 % (1989655)Termination phase: Property scanning % 4.56/1.43 % (1989655)Time elapsed: 0.035 s % 4.56/1.43 % (1989655)Peak memory usage: 86 MB % 4.56/1.43 % (1989655)Instructions burned: 47 (million) % 4.56/1.43 % (1989658)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=963106261:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2998 on theBenchmark for (2998ds/14Mi) % 4.56/1.43 % (1989658)Instruction limit reached! % 4.56/1.43 % (1989658)------------------------------ % 6.19/1.67 % (1989658)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.19/1.67 % (1989658)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.19/1.67 % (1989658)CaDiCaL version: 2.1.3 % 6.19/1.67 % (1989658)Termination reason: Instruction limit % 6.19/1.67 % (1989658)Termination phase: Property scanning % 6.19/1.67 % (1989658)Time elapsed: 0.006 s % 6.19/1.67 % (1989658)Peak memory usage: 85 MB % 6.19/1.67 % (1989658)Instructions burned: 16 (million) % 6.19/1.67 % (1989652)Instruction limit reached! % 6.19/1.67 % (1989652)------------------------------ % 6.19/1.67 % (1989652)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.19/1.67 % (1989652)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.19/1.67 % (1989652)CaDiCaL version: 2.1.3 % 6.19/1.67 % (1989652)Termination reason: Instruction limit % 6.19/1.67 % (1989652)Termination phase: Saturation % 6.19/1.67 % (1989652)Time elapsed: 0.181 s % 6.19/1.67 % (1989652)Peak memory usage: 112 MB % 6.19/1.67 % (1989652)Instructions burned: 201 (million) % 6.19/1.67 % (1989665)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=461750544:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2997 on theBenchmark for (2997ds/29Mi) % 6.19/1.67 % (1989665)Instruction limit reached! % 6.19/1.67 % (1989665)------------------------------ % 6.19/1.67 % (1989665)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.19/1.67 % (1989665)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.19/1.67 % (1989665)CaDiCaL version: 2.1.3 % 6.19/1.67 % (1989665)Termination reason: Instruction limit % 6.19/1.67 % (1989665)Termination phase: Property scanning % 6.19/1.67 % (1989665)Time elapsed: 0.012 s % 6.19/1.67 % (1989665)Peak memory usage: 85 MB % 6.19/1.67 % (1989665)Instructions burned: 31 (million) % 6.19/1.67 % (1989667)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=3830455360:i=24:canc=force:rtra=on_2996 on theBenchmark for (2996ds/24Mi) % 6.19/1.67 % (1989666)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=3665123804:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2997 on theBenchmark for (2997ds/16Mi) % 6.19/1.67 % (1989666)Instruction limit reached! % 6.19/1.67 % (1989666)------------------------------ % 6.19/1.67 % (1989666)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.19/1.67 % (1989666)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.19/1.67 % (1989666)CaDiCaL version: 2.1.3 % 6.19/1.67 % (1989666)Termination reason: Instruction limit % 6.19/1.67 % (1989666)Termination phase: Property scanning % 6.19/1.67 % (1989666)Time elapsed: 0.013 s % 6.19/1.67 % (1989666)Peak memory usage: 85 MB % 6.19/1.67 % (1989666)Instructions burned: 16 (million) % 6.19/1.67 % (1989651)Instruction limit reached! % 6.19/1.67 % (1989651)------------------------------ % 6.19/1.67 % (1989651)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.19/1.67 % (1989651)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.19/1.67 % (1989651)CaDiCaL version: 2.1.3 % 6.19/1.67 % (1989651)Termination reason: Instruction limit % 6.19/1.67 % (1989651)Termination phase: Saturation % 6.19/1.67 % (1989651)Time elapsed: 0.259 s % 6.19/1.67 % (1989651)Peak memory usage: 112 MB % 6.19/1.67 % (1989651)Instructions burned: 307 (million) % 6.19/1.67 % (1989667)Instruction limit reached! % 6.19/1.67 % (1989667)------------------------------ % 6.19/1.67 % (1989667)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.19/1.67 % (1989667)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.19/1.67 % (1989667)CaDiCaL version: 2.1.3 % 6.19/1.67 % (1989667)Termination reason: Instruction limit % 6.19/1.67 % (1989667)Termination phase: Property scanning % 6.19/1.67 % (1989667)Time elapsed: 0.018 s % 6.19/1.67 % (1989667)Peak memory usage: 85 MB % 6.19/1.67 % (1989667)Instructions burned: 24 (million) % 6.19/1.67 % (1989669)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=3841415939:i=27:canc=cautious:fsr=off:rtra=on_2996 on theBenchmark for (2996ds/27Mi) % 6.19/1.67 % (1989670)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=3043684599:i=85:gtgl=4:rtra=on:gtg=exists_sym_2996 on theBenchmark for (2996ds/85Mi) % 6.19/1.67 % (1989669)Instruction limit reached! % 6.19/1.67 % (1989669)------------------------------ % 7.71/1.85 % (1989669)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.71/1.85 % (1989669)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.71/1.85 % (1989669)CaDiCaL version: 2.1.3 % 7.71/1.85 % (1989669)Termination reason: Instruction limit % 7.71/1.85 % (1989669)Termination phase: Property scanning % 7.71/1.85 % (1989669)Time elapsed: 0.021 s % 7.71/1.85 % (1989669)Peak memory usage: 85 MB % 7.71/1.85 % (1989669)Instructions burned: 28 (million) % 7.71/1.85 % (1989670)Instruction limit reached! % 7.71/1.85 % (1989670)------------------------------ % 7.71/1.85 % (1989670)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.71/1.85 % (1989670)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.71/1.85 % (1989670)CaDiCaL version: 2.1.3 % 7.71/1.85 % (1989670)Termination reason: Instruction limit % 7.71/1.85 % (1989670)Termination phase: Property scanning % 7.71/1.85 % (1989670)Time elapsed: 0.064 s % 7.71/1.85 % (1989670)Peak memory usage: 85 MB % 7.71/1.85 % (1989670)Instructions burned: 85 (million) % 7.71/1.85 % (1989673)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=4198373994:i=181:rtra=on:ss=axioms:ev=cautious_2994 on theBenchmark for (2994ds/181Mi) % 7.71/1.85 % (1989671)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=2558359666:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2995 on theBenchmark for (2995ds/2Mi) % 7.71/1.85 % (1989671)Instruction limit reached! % 7.71/1.85 % (1989671)------------------------------ % 7.71/1.85 % (1989671)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.71/1.85 % (1989671)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.71/1.85 % (1989671)CaDiCaL version: 2.1.3 % 7.71/1.85 % (1989671)Termination reason: Instruction limit % 7.71/1.85 % (1989671)Termination phase: shuffling % 7.71/1.85 % (1989671)Time elapsed: 0.003 s % 7.71/1.85 % (1989671)Peak memory usage: 85 MB % 7.71/1.85 % (1989671)Instructions burned: 3 (million) % 7.71/1.85 % (1989673)Refutation not found, incomplete strategy % 7.71/1.85 % (1989673)------------------------------ % 7.71/1.85 % (1989673)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.71/1.85 % (1989673)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.71/1.85 % (1989673)CaDiCaL version: 2.1.3 % 7.71/1.85 % (1989673)Termination reason: Refutation not found, incomplete strategy % 7.71/1.85 % (1989673)Time elapsed: 0.016 s % 7.71/1.85 % (1989673)Peak memory usage: 87 MB % 7.71/1.85 % (1989673)Instructions burned: 40 (million) % 7.71/1.85 % (1989677)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=1220135859:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2994 on theBenchmark for (2994ds/66Mi) % 7.71/1.85 % (1989676)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=1459320898:i=4:ep=RST:ins=2:rtra=on_2994 on theBenchmark for (2994ds/4Mi) % 7.71/1.85 % (1989678)lrs+10_1_thi=all:si=on:fd=off:random_seed=1160772642:i=53:rtra=on:gtg=all_2994 on theBenchmark for (2994ds/53Mi) % 7.71/1.85 % (1989676)Instruction limit reached! % 7.71/1.85 % (1989676)------------------------------ % 7.71/1.85 % (1989676)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.71/1.85 % (1989676)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.71/1.85 % (1989676)CaDiCaL version: 2.1.3 % 7.71/1.85 % (1989676)Termination reason: Instruction limit % 7.71/1.85 % (1989676)Termination phase: shuffling % 7.71/1.85 % (1989676)Time elapsed: 0.003 s % 7.71/1.85 % (1989676)Peak memory usage: 84 MB % 7.71/1.85 % (1989676)Instructions burned: 4 (million) % 7.71/1.85 % (1989681)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=4234330009:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2993 on theBenchmark for (2993ds/8Mi) % 7.71/1.85 % (1989682)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=2962672067:st=3:i=2:rtra=on:ss=axioms_2993 on theBenchmark for (2993ds/2Mi) % 7.71/1.85 % (1989678)Instruction limit reached! % 7.71/1.85 % (1989678)------------------------------ % 7.71/1.85 % (1989678)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.71/1.85 % (1989678)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.71/1.85 % (1989678)CaDiCaL version: 2.1.3 % 7.71/1.85 % (1989678)Termination reason: Instruction limit % 10.54/2.23 % (1989678)Termination phase: Property scanning % 10.54/2.23 % (1989678)Time elapsed: 0.041 s % 10.54/2.23 % (1989678)Peak memory usage: 84 MB % 10.54/2.23 % (1989678)Instructions burned: 53 (million) % 10.54/2.23 % (1989682)Instruction limit reached! % 10.54/2.23 % (1989682)------------------------------ % 10.54/2.23 % (1989682)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.54/2.23 % (1989682)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.54/2.23 % (1989682)CaDiCaL version: 2.1.3 % 10.54/2.23 % (1989682)Termination reason: Instruction limit % 10.54/2.23 % (1989682)Termination phase: shuffling % 10.54/2.23 % (1989682)Time elapsed: 0.002 s % 10.54/2.23 % (1989682)Peak memory usage: 85 MB % 10.54/2.23 % (1989682)Instructions burned: 3 (million) % 10.54/2.23 % (1989681)Instruction limit reached! % 10.54/2.23 % (1989681)------------------------------ % 10.54/2.23 % (1989681)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.54/2.23 % (1989681)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.54/2.23 % (1989681)CaDiCaL version: 2.1.3 % 10.54/2.23 % (1989681)Termination reason: Instruction limit % 10.54/2.23 % (1989681)Termination phase: Property scanning % 10.54/2.23 % (1989681)Time elapsed: 0.008 s % 10.54/2.23 % (1989681)Peak memory usage: 85 MB % 10.54/2.23 % (1989681)Instructions burned: 9 (million) % 10.54/2.23 % (1989677)Instruction limit reached! % 10.54/2.23 % (1989677)------------------------------ % 10.54/2.23 % (1989677)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.54/2.23 % (1989677)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.54/2.23 % (1989677)CaDiCaL version: 2.1.3 % 10.54/2.23 % (1989677)Termination reason: Instruction limit % 10.54/2.23 % (1989677)Termination phase: Property scanning % 10.54/2.23 % (1989677)Time elapsed: 0.052 s % 10.54/2.23 % (1989677)Peak memory usage: 85 MB % 10.54/2.23 % (1989677)Instructions burned: 67 (million) % 10.54/2.23 % (1989673)------------------------------ % 10.54/2.23 % (1989673)------------------------------ % 10.54/2.23 % (1989685)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=1895008310:i=2:doe=on:canc=force:asg=cautious:rtra=on_2993 on theBenchmark for (2993ds/2Mi) % 10.54/2.23 % (1989685)Instruction limit reached! % 10.54/2.23 % (1989685)------------------------------ % 10.54/2.23 % (1989685)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.54/2.23 % (1989685)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.54/2.23 % (1989685)CaDiCaL version: 2.1.3 % 10.54/2.23 % (1989685)Termination reason: Instruction limit % 10.54/2.23 % (1989685)Termination phase: shuffling % 10.54/2.23 % (1989685)Time elapsed: 0.002 s % 10.54/2.23 % (1989685)Peak memory usage: 85 MB % 10.54/2.23 % (1989685)Instructions burned: 2 (million) % 10.54/2.23 % (1989695)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=3388098725:i=2:fsr=off:rtra=on:inst=on_2991 on theBenchmark for (2991ds/2Mi) % 10.54/2.23 % (1989695)Instruction limit reached! % 10.54/2.23 % (1989695)------------------------------ % 10.54/2.23 % (1989695)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.54/2.23 % (1989695)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.54/2.23 % (1989695)CaDiCaL version: 2.1.3 % 10.54/2.23 % (1989695)Termination reason: Instruction limit % 10.54/2.23 % (1989695)Termination phase: shuffling % 10.54/2.23 % (1989695)Time elapsed: 0.001 s % 10.54/2.23 % (1989695)Peak memory usage: 84 MB % 10.54/2.23 % (1989695)Instructions burned: 2 (million) % 10.54/2.23 % (1989689)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=1582091222:i=127:doe=on:rtra=on_2992 on theBenchmark for (2992ds/127Mi) % 10.54/2.23 % (1989693)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=2067653721:i=26:canc=cautious:av=off:rtra=on_2991 on theBenchmark for (2991ds/26Mi) % 10.54/2.23 % (1989694)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=3733659387:avsq=on:i=35:doe=on:thsqd=64:nm=64:fsr=off:thsqc=32:rtra=on:tac=light:ss=included:thsq=on:ev=off:sgt=32_2991 on theBenchmark for (2991ds/35Mi) % 10.54/2.23 % (1989692)dis+10_1_si=on:random_seed=2139485881:i=10:ep=R:rtra=on_2991 on theBenchmark for (2991ds/10Mi) % 10.54/2.23 % (1989692)Instruction limit reached! % 10.54/2.23 % (1989692)------------------------------ % 10.54/2.23 % (1989692)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.54/2.23 % (1989692)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.89/2.56 % (1989692)CaDiCaL version: 2.1.3 % 11.89/2.56 % (1989692)Termination reason: Instruction limit % 11.89/2.56 % (1989692)Termination phase: Property scanning % 11.89/2.56 % (1989692)Time elapsed: 0.008 s % 11.89/2.56 % (1989692)Peak memory usage: 85 MB % 11.89/2.56 % (1989692)Instructions burned: 10 (million) % 11.89/2.56 % (1989693)Instruction limit reached! % 11.89/2.56 % (1989693)------------------------------ % 11.89/2.56 % (1989693)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.89/2.56 % (1989693)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.89/2.56 % (1989693)CaDiCaL version: 2.1.3 % 11.89/2.56 % (1989693)Termination reason: Instruction limit % 11.89/2.56 % (1989693)Termination phase: Property scanning % 11.89/2.56 % (1989693)Time elapsed: 0.020 s % 11.89/2.56 % (1989693)Peak memory usage: 85 MB % 11.89/2.56 % (1989693)Instructions burned: 26 (million) % 11.89/2.56 % (1989694)Instruction limit reached! % 11.89/2.56 % (1989694)------------------------------ % 11.89/2.56 % (1989694)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.89/2.56 % (1989694)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.89/2.56 % (1989694)CaDiCaL version: 2.1.3 % 11.89/2.56 % (1989694)Termination reason: Instruction limit % 11.89/2.56 % (1989694)Termination phase: Property scanning % 11.89/2.56 % (1989694)Time elapsed: 0.027 s % 11.89/2.56 % (1989694)Peak memory usage: 85 MB % 11.89/2.56 % (1989694)Instructions burned: 35 (million) % 11.89/2.56 % (1989698)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=491144173:i=370:ep=RS:fsr=off:rtra=on_2990 on theBenchmark for (2990ds/370Mi) % 11.89/2.56 % (1989689)Instruction limit reached! % 11.89/2.56 % (1989689)------------------------------ % 11.89/2.56 % (1989689)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.89/2.56 % (1989689)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.89/2.56 % (1989689)CaDiCaL version: 2.1.3 % 11.89/2.56 % (1989689)Termination reason: Instruction limit % 11.89/2.56 % (1989689)Termination phase: Saturation % 11.89/2.56 % (1989689)Time elapsed: 0.126 s % 11.89/2.56 % (1989689)Peak memory usage: 112 MB % 11.89/2.56 % (1989689)Instructions burned: 128 (million) % 11.89/2.56 % (1989696)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=2067337388:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2990 on theBenchmark for (2990ds/8Mi) % 11.89/2.56 % (1989696)Instruction limit reached! % 11.89/2.56 % (1989696)------------------------------ % 11.89/2.56 % (1989696)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.89/2.56 % (1989696)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.89/2.56 % (1989696)CaDiCaL version: 2.1.3 % 11.89/2.56 % (1989696)Termination reason: Instruction limit % 11.89/2.56 % (1989696)Termination phase: Property scanning % 11.89/2.56 % (1989696)Time elapsed: 0.007 s % 11.89/2.56 % (1989696)Peak memory usage: 85 MB % 11.89/2.56 % (1989696)Instructions burned: 8 (million) % 11.89/2.56 % (1989698)Refutation not found, incomplete strategy % 11.89/2.56 % (1989698)------------------------------ % 11.89/2.56 % (1989698)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.89/2.56 % (1989698)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.89/2.56 % (1989698)CaDiCaL version: 2.1.3 % 11.89/2.56 % (1989698)Termination reason: Refutation not found, incomplete strategy % 11.89/2.56 % (1989698)Time elapsed: 0.092 s % 11.89/2.56 % (1989698)Peak memory usage: 88 MB % 11.89/2.56 % (1989698)Instructions burned: 161 (million) % 11.89/2.56 % (1989701)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=1021264098:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2989 on theBenchmark for (2989ds/13Mi) % 11.89/2.56 % (1989705)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=506518470:i=226:rtra=on:gtg=position:ss=axioms_2989 on theBenchmark for (2989ds/226Mi) % 11.89/2.56 % (1989701)Instruction limit reached! % 11.89/2.56 % (1989701)------------------------------ % 11.89/2.56 % (1989701)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.89/2.56 % (1989701)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.89/2.56 % (1989701)CaDiCaL version: 2.1.3 % 11.89/2.56 % (1989701)Termination reason: Instruction limit % 11.89/2.56 % (1989701)Termination phase: Property scanning % 11.89/2.56 % (1989701)Time elapsed: 0.011 s % 14.21/3.01 % (1989701)Peak memory usage: 85 MB % 14.21/3.01 % (1989701)Instructions burned: 13 (million) % 14.21/3.01 % (1989705)Refutation not found, incomplete strategy % 14.21/3.01 % (1989705)------------------------------ % 14.21/3.01 % (1989705)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.21/3.01 % (1989705)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.21/3.01 % (1989705)CaDiCaL version: 2.1.3 % 14.21/3.01 % (1989705)Termination reason: Refutation not found, incomplete strategy % 14.21/3.01 % (1989705)Time elapsed: 0.048 s % 14.21/3.01 % (1989705)Peak memory usage: 111 MB % 14.21/3.01 % (1989705)Instructions burned: 72 (million) % 14.21/3.01 % (1989709)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=283807765:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2988 on theBenchmark for (2988ds/75Mi) % 14.21/3.01 % (1989706)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=371288715:i=10:rtra=on_2989 on theBenchmark for (2989ds/10Mi) % 14.21/3.01 % (1989707)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=1338665454:i=71:rtra=on:gtg=exists_top_2989 on theBenchmark for (2989ds/71Mi) % 14.21/3.01 % (1989706)Instruction limit reached! % 14.21/3.01 % (1989706)------------------------------ % 14.21/3.01 % (1989706)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.21/3.01 % (1989706)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.21/3.01 % (1989706)CaDiCaL version: 2.1.3 % 14.21/3.01 % (1989706)Termination reason: Instruction limit % 14.21/3.01 % (1989706)Termination phase: Property scanning % 14.21/3.01 % (1989706)Time elapsed: 0.009 s % 14.21/3.01 % (1989706)Peak memory usage: 85 MB % 14.21/3.01 % (1989706)Instructions burned: 11 (million) % 14.21/3.01 % (1989709)Instruction limit reached! % 14.21/3.01 % (1989709)------------------------------ % 14.21/3.01 % (1989709)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.21/3.01 % (1989709)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.21/3.01 % (1989709)CaDiCaL version: 2.1.3 % 14.21/3.01 % (1989709)Termination reason: Instruction limit % 14.21/3.01 % (1989709)Termination phase: Property scanning % 14.21/3.01 % (1989709)Time elapsed: 0.050 s % 14.21/3.01 % (1989709)Peak memory usage: 86 MB % 14.21/3.01 % (1989709)Instructions burned: 75 (million) % 14.21/3.01 % (1989707)Instruction limit reached! % 14.21/3.01 % (1989707)------------------------------ % 14.21/3.01 % (1989707)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.21/3.01 % (1989707)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.21/3.01 % (1989707)CaDiCaL version: 2.1.3 % 14.21/3.01 % (1989707)Termination reason: Instruction limit % 14.21/3.01 % (1989707)Termination phase: Property scanning % 14.21/3.01 % (1989707)Time elapsed: 0.055 s % 14.21/3.01 % (1989707)Peak memory usage: 85 MB % 14.21/3.01 % (1989707)Instructions burned: 72 (million) % 14.21/3.01 % (1989711)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=3989563173:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2988 on theBenchmark for (2988ds/294Mi) % 14.21/3.01 % (1989714)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=2821717322:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2987 on theBenchmark for (2987ds/130Mi) % 14.21/3.01 % (1989705)------------------------------ % 14.21/3.01 % (1989705)------------------------------ % 14.21/3.01 % (1989718)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=3820478857:i=131:rtra=on_2986 on theBenchmark for (2986ds/131Mi) % 14.21/3.01 % (1989698)------------------------------ % 14.21/3.01 % (1989698)------------------------------ % 14.21/3.01 % (1989719)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=1155484768:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2986 on theBenchmark for (2986ds/40Mi) % 14.21/3.01 % (1989714)Instruction limit reached! % 14.21/3.01 % (1989714)------------------------------ % 14.21/3.01 % (1989714)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.21/3.01 % (1989714)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.21/3.01 % (1989714)CaDiCaL version: 2.1.3 % 14.21/3.01 % (1989714)Termination reason: Instruction limit % 14.21/3.01 % (1989714)Termination phase: Twee Goal Transformation % 14.21/3.01 % (1989714)Time elapsed: 0.102 s % 14.21/3.01 % (1989714)Peak memory usage: 87 MB % 18.12/3.36 % (1989714)Instructions burned: 131 (million) % 18.12/3.36 % (1989719)Instruction limit reached! % 18.12/3.36 % (1989719)------------------------------ % 18.12/3.36 % (1989719)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.12/3.36 % (1989719)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.12/3.36 % (1989719)CaDiCaL version: 2.1.3 % 18.12/3.36 % (1989719)Termination reason: Instruction limit % 18.12/3.36 % (1989719)Termination phase: Property scanning % 18.12/3.36 % (1989719)Time elapsed: 0.031 s % 18.12/3.36 % (1989719)Peak memory usage: 85 MB % 18.12/3.36 % (1989719)Instructions burned: 41 (million) % 18.12/3.36 % (1989720)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=2957056229:i=307:rtra=on:gtg=exists_top_2986 on theBenchmark for (2986ds/307Mi) % 18.12/3.36 % (1989711)Instruction limit reached! % 18.12/3.36 % (1989711)------------------------------ % 18.12/3.36 % (1989711)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.12/3.36 % (1989711)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.12/3.36 % (1989711)CaDiCaL version: 2.1.3 % 18.12/3.36 % (1989711)Termination reason: Instruction limit % 18.12/3.36 % (1989711)Termination phase: Saturation % 18.12/3.36 % (1989711)Time elapsed: 0.221 s % 18.12/3.36 % (1989711)Peak memory usage: 91 MB % 18.12/3.36 % (1989711)Instructions burned: 295 (million) % 18.12/3.36 % (1989723)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=1571117414:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2984 on theBenchmark for (2984ds/598Mi) % 18.12/3.36 % (1989718)Instruction limit reached! % 18.12/3.36 % (1989718)------------------------------ % 18.12/3.36 % (1989718)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.12/3.36 % (1989718)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.12/3.36 % (1989718)CaDiCaL version: 2.1.3 % 18.12/3.36 % (1989718)Termination reason: Instruction limit % 18.12/3.36 % (1989718)Termination phase: Saturation % 18.12/3.36 % (1989718)Time elapsed: 0.153 s % 18.12/3.36 % (1989718)Peak memory usage: 128 MB % 18.12/3.36 % (1989718)Instructions burned: 131 (million) % 18.12/3.36 % (1989720)Refutation not found, incomplete strategy % 18.12/3.36 % (1989720)------------------------------ % 18.12/3.36 % (1989720)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.12/3.36 % (1989720)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.12/3.36 % (1989720)CaDiCaL version: 2.1.3 % 18.12/3.36 % (1989720)Termination reason: Refutation not found, incomplete strategy % 18.12/3.36 % (1989720)Time elapsed: 0.171 s % 18.12/3.36 % (1989720)Peak memory usage: 89 MB % 18.12/3.36 % (1989720)Instructions burned: 226 (million) % 18.12/3.36 % (1989726)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=1798921412:i=131:canc=cautious:fsr=off:rtra=on_2983 on theBenchmark for (2983ds/131Mi) % 18.12/3.36 % (1989727)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=3712150750:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2983 on theBenchmark for (2983ds/259Mi) % 18.12/3.36 % (1989729)dis+10_1_si=on:random_seed=2414689927:s2a=on:i=1000:rtra=on:gtg=exists_all_2983 on theBenchmark for (2983ds/1000Mi) % 18.12/3.36 % (1989730)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=4187924906:i=383:fsr=off:rtra=on:ev=force_2983 on theBenchmark for (2983ds/383Mi) % 18.12/3.36 % (1989727)Refutation not found, incomplete strategy % 18.12/3.36 % (1989727)------------------------------ % 18.12/3.36 % (1989727)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.12/3.36 % (1989727)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.12/3.36 % (1989727)CaDiCaL version: 2.1.3 % 18.12/3.36 % (1989727)Termination reason: Refutation not found, incomplete strategy % 18.12/3.36 % (1989727)Time elapsed: 0.091 s % 18.12/3.36 % (1989727)Peak memory usage: 111 MB % 18.12/3.36 % (1989727)Instructions burned: 76 (million) % 18.12/3.36 % (1989726)Instruction limit reached! % 18.12/3.36 % (1989726)------------------------------ % 18.12/3.36 % (1989726)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.12/3.36 % (1989726)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.12/3.36 % (1989726)CaDiCaL version: 2.1.3 % 18.12/3.36 % (1989726)Termination reason: Instruction limit % 19.98/3.75 % (1989726)Termination phase: Saturation % 19.98/3.75 % (1989726)Time elapsed: 0.128 s % 19.98/3.75 % (1989726)Peak memory usage: 111 MB % 19.98/3.75 % (1989726)Instructions burned: 132 (million) % 19.98/3.75 % (1989732)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=302937653:i=141:doe=on:rtra=on_2982 on theBenchmark for (2982ds/141Mi) % 19.98/3.75 % (1989723)Instruction limit reached! % 19.98/3.75 % (1989723)------------------------------ % 19.98/3.75 % (1989723)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.98/3.75 % (1989723)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.98/3.75 % (1989723)CaDiCaL version: 2.1.3 % 19.98/3.75 % (1989723)Termination reason: Instruction limit % 19.98/3.75 % (1989723)Termination phase: Saturation % 19.98/3.75 % (1989723)Time elapsed: 0.281 s % 19.98/3.75 % (1989723)Peak memory usage: 135 MB % 19.98/3.75 % (1989723)Instructions burned: 598 (million) % 19.98/3.75 % (1989732)Instruction limit reached! % 19.98/3.75 % (1989732)------------------------------ % 19.98/3.75 % (1989732)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.98/3.75 % (1989732)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.98/3.75 % (1989732)CaDiCaL version: 2.1.3 % 19.98/3.75 % (1989732)Termination reason: Instruction limit % 19.98/3.75 % (1989732)Termination phase: Saturation % 19.98/3.75 % (1989732)Time elapsed: 0.106 s % 19.98/3.75 % (1989732)Peak memory usage: 87 MB % 19.98/3.75 % (1989732)Instructions burned: 141 (million) % 19.98/3.75 % (1989737)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=2835290408:i=65:nm=16:rtra=on_2980 on theBenchmark for (2980ds/65Mi) % 19.98/3.75 % (1989737)Instruction limit reached! % 19.98/3.75 % (1989737)------------------------------ % 19.98/3.75 % (1989737)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.98/3.75 % (1989737)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.98/3.75 % (1989737)CaDiCaL version: 2.1.3 % 19.98/3.75 % (1989737)Termination reason: Instruction limit % 19.98/3.75 % (1989737)Termination phase: Saturation % 19.98/3.75 % (1989737)Time elapsed: 0.026 s % 19.98/3.75 % (1989737)Peak memory usage: 88 MB % 19.98/3.75 % (1989737)Instructions burned: 66 (million) % 19.98/3.75 % (1989720)------------------------------ % 19.98/3.75 % (1989720)------------------------------ % 19.98/3.75 % (1989730)Instruction limit reached! % 19.98/3.75 % (1989730)------------------------------ % 19.98/3.75 % (1989730)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.98/3.75 % (1989730)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.98/3.75 % (1989730)CaDiCaL version: 2.1.3 % 19.98/3.75 % (1989730)Termination reason: Instruction limit % 19.98/3.75 % (1989730)Termination phase: Saturation % 19.98/3.75 % (1989730)Time elapsed: 0.289 s % 19.98/3.75 % (1989730)Peak memory usage: 90 MB % 19.98/3.75 % (1989730)Instructions burned: 386 (million) % 19.98/3.75 % (1989739)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=161620958:i=121:nm=16:rtra=on_2979 on theBenchmark for (2979ds/121Mi) % 19.98/3.75 % (1989740)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=308469494:s2a=on:i=128:s2at=5:ins=3:rtra=on_2978 on theBenchmark for (2978ds/128Mi) % 19.98/3.75 % (1989739)Instruction limit reached! % 19.98/3.75 % (1989739)------------------------------ % 19.98/3.75 % (1989739)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.98/3.75 % (1989739)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.98/3.75 % (1989739)CaDiCaL version: 2.1.3 % 19.98/3.75 % (1989739)Termination reason: Instruction limit % 19.98/3.75 % (1989739)Termination phase: Saturation % 19.98/3.75 % (1989739)Time elapsed: 0.092 s % 19.98/3.75 % (1989739)Peak memory usage: 88 MB % 19.98/3.75 % (1989739)Instructions burned: 122 (million) % 19.98/3.75 % (1989727)------------------------------ % 19.98/3.75 % (1989727)------------------------------ % 19.98/3.75 % (1989742)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=810698278:i=39:ins=3:rtra=on_2978 on theBenchmark for (2978ds/39Mi) % 19.98/3.75 % (1989740)Instruction limit reached! % 19.98/3.75 % (1989740)------------------------------ % 19.98/3.75 % (1989740)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.98/3.75 % (1989740)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.98/3.75 % (1989740)CaDiCaL version: 2.1.3 % 25.07/4.23 % (1989740)Termination reason: Instruction limit % 25.07/4.23 % (1989740)Termination phase: Saturation % 25.07/4.23 % (1989740)Time elapsed: 0.098 s % 25.07/4.23 % (1989740)Peak memory usage: 88 MB % 25.07/4.23 % (1989740)Instructions burned: 129 (million) % 25.07/4.23 % (1989744)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=492978066:i=329:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2977 on theBenchmark for (2977ds/329Mi) % 25.07/4.23 % (1989742)Instruction limit reached! % 25.07/4.23 % (1989742)------------------------------ % 25.07/4.23 % (1989742)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.07/4.23 % (1989742)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.07/4.23 % (1989742)CaDiCaL version: 2.1.3 % 25.07/4.23 % (1989742)Termination reason: Instruction limit % 25.07/4.23 % (1989742)Termination phase: Property scanning % 25.07/4.23 % (1989742)Time elapsed: 0.032 s % 25.07/4.23 % (1989742)Peak memory usage: 85 MB % 25.07/4.23 % (1989742)Instructions burned: 40 (million) % 25.07/4.23 % (1989743)dis+1010_1_to=kbo:si=on:random_seed=2924243042:i=175:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2977 on theBenchmark for (2977ds/175Mi) % 25.07/4.23 % (1989729)Instruction limit reached! % 25.07/4.23 % (1989729)------------------------------ % 25.07/4.23 % (1989729)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.07/4.23 % (1989729)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.07/4.23 % (1989729)CaDiCaL version: 2.1.3 % 25.07/4.23 % (1989729)Termination reason: Instruction limit % 25.07/4.23 % (1989729)Termination phase: Saturation % 25.07/4.23 % (1989729)Time elapsed: 0.680 s % 25.07/4.23 % (1989729)Peak memory usage: 90 MB % 25.07/4.23 % (1989729)Instructions burned: 1000 (million) % 25.07/4.23 % (1989744)Instruction limit reached! % 25.07/4.23 % (1989744)------------------------------ % 25.07/4.23 % (1989744)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.07/4.23 % (1989744)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.07/4.23 % (1989744)CaDiCaL version: 2.1.3 % 25.07/4.23 % (1989744)Termination reason: Instruction limit % 25.07/4.23 % (1989744)Termination phase: Saturation % 25.07/4.23 % (1989744)Time elapsed: 0.151 s % 25.07/4.23 % (1989744)Peak memory usage: 117 MB % 25.07/4.23 % (1989744)Instructions burned: 331 (million) % 25.07/4.23 % (1989747)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=1136585425:s2a=on:i=483:doe=on:nm=32:rtra=on_2976 on theBenchmark for (2976ds/483Mi) % 25.07/4.23 % (1989748)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=2301985465:thitd=on:i=215:nm=0:rtra=on:ev=force_2976 on theBenchmark for (2976ds/215Mi) % 25.07/4.23 % (1989743)Instruction limit reached! % 25.07/4.23 % (1989743)------------------------------ % 25.07/4.23 % (1989743)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.07/4.23 % (1989743)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.07/4.23 % (1989743)CaDiCaL version: 2.1.3 % 25.07/4.23 % (1989743)Termination reason: Instruction limit % 25.07/4.23 % (1989743)Termination phase: Property scanning % 25.07/4.23 % (1989743)Time elapsed: 0.134 s % 25.07/4.23 % (1989743)Peak memory usage: 86 MB % 25.07/4.23 % (1989743)Instructions burned: 176 (million) % 25.07/4.23 % (1989752)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=3803505152:st=2:i=295:rtra=on:ss=axioms_2975 on theBenchmark for (2975ds/295Mi) % 25.07/4.23 % (1989751)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=1011456464:i=349:rtra=on_2975 on theBenchmark for (2975ds/349Mi) % 25.07/4.23 % (1989752)Refutation not found, incomplete strategy % 25.07/4.23 % (1989752)------------------------------ % 25.07/4.23 % (1989752)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.07/4.23 % (1989752)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.07/4.23 % (1989752)CaDiCaL version: 2.1.3 % 25.07/4.23 % (1989752)Termination reason: Refutation not found, incomplete strategy % 25.07/4.23 % (1989752)Time elapsed: 0.053 s % 25.07/4.23 % (1989752)Peak memory usage: 88 MB % 25.07/4.23 % (1989752)Instructions burned: 70 (million) % 25.07/4.23 % (1989754)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=2228280685:i=328:kws=inv_frequency:nm=20:rtra=on_2974 on theBenchmark for (2974ds/328Mi) % 25.99/4.64 % (1989756)dis+1010_1_to=lpo:sil=128000:sas=z3:si=on:nwc=5:random_seed=1577435558:i=281:gtgl=2:rtra=on:gtg=all_2974 on theBenchmark for (2974ds/281Mi) % 25.99/4.64 % (1989748)Instruction limit reached! % 25.99/4.64 % (1989748)------------------------------ % 25.99/4.64 % (1989748)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.99/4.64 % (1989748)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.99/4.64 % (1989748)CaDiCaL version: 2.1.3 % 25.99/4.64 % (1989748)Termination reason: Instruction limit % 25.99/4.64 % (1989748)Termination phase: Saturation % 25.99/4.64 % (1989748)Time elapsed: 0.221 s % 25.99/4.64 % (1989748)Peak memory usage: 129 MB % 25.99/4.64 % (1989748)Instructions burned: 215 (million) % 25.99/4.64 % (1989758)lrs+1010_1_to=kbo:sil=128000:si=on:sos=on:urr=on:uwa=alasca_main:random_seed=3079056674:i=484:doe=on:nm=0:av=off:rtra=on:ss=axioms_2973 on theBenchmark for (2973ds/484Mi) % 25.99/4.64 % (1989756)Instruction limit reached! % 25.99/4.64 % (1989756)------------------------------ % 25.99/4.64 % (1989756)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.99/4.64 % (1989756)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.99/4.64 % (1989756)CaDiCaL version: 2.1.3 % 25.99/4.64 % (1989756)Termination reason: Instruction limit % 25.99/4.64 % (1989756)Termination phase: Saturation % 25.99/4.64 % (1989756)Time elapsed: 0.129 s % 25.99/4.64 % (1989756)Peak memory usage: 112 MB % 25.99/4.64 % (1989756)Instructions burned: 283 (million) % 25.99/4.64 % (1989758)Refutation not found, incomplete strategy % 25.99/4.64 % (1989758)------------------------------ % 25.99/4.64 % (1989758)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.99/4.64 % (1989758)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.99/4.64 % (1989758)CaDiCaL version: 2.1.3 % 25.99/4.64 % (1989758)Termination reason: Refutation not found, incomplete strategy % 25.99/4.64 % (1989758)Time elapsed: 0.052 s % 25.99/4.64 % (1989758)Peak memory usage: 88 MB % 25.99/4.64 % (1989758)Instructions burned: 68 (million) % 25.99/4.64 % (1989751)Instruction limit reached! % 25.99/4.64 % (1989751)------------------------------ % 25.99/4.64 % (1989751)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.99/4.64 % (1989751)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.99/4.64 % (1989751)CaDiCaL version: 2.1.3 % 25.99/4.64 % (1989751)Termination reason: Instruction limit % 25.99/4.64 % (1989751)Termination phase: Saturation % 25.99/4.64 % (1989751)Time elapsed: 0.291 s % 25.99/4.64 % (1989751)Peak memory usage: 113 MB % 25.99/4.64 % (1989751)Instructions burned: 350 (million) % 25.99/4.64 % (1989747)Instruction limit reached! % 25.99/4.64 % (1989747)------------------------------ % 25.99/4.64 % (1989747)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.99/4.64 % (1989747)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.99/4.64 % (1989747)CaDiCaL version: 2.1.3 % 25.99/4.64 % (1989747)Termination reason: Instruction limit % 25.99/4.64 % (1989747)Termination phase: Saturation % 25.99/4.64 % (1989747)Time elapsed: 0.424 s % 25.99/4.64 % (1989747)Peak memory usage: 133 MB % 25.99/4.64 % (1989747)Instructions burned: 483 (million) % 25.99/4.64 % (1989754)Instruction limit reached! % 25.99/4.64 % (1989754)------------------------------ % 25.99/4.64 % (1989754)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.99/4.64 % (1989754)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.99/4.64 % (1989754)CaDiCaL version: 2.1.3 % 25.99/4.64 % (1989754)Termination reason: Instruction limit % 25.99/4.64 % (1989754)Termination phase: Saturation % 25.99/4.64 % (1989754)Time elapsed: 0.276 s % 25.99/4.64 % (1989754)Peak memory usage: 112 MB % 25.99/4.64 % (1989754)Instructions burned: 329 (million) % 25.99/4.64 % (1989752)------------------------------ % 25.99/4.64 % (1989752)------------------------------ % 25.99/4.64 % (1989763)lrs+21_1_to=kbo:sil=128000:thi=neg_eq:si=on:random_seed=2869343360:i=321:canc=force:rtra=on:tac=axiom:ss=axioms:ev=force_2971 on theBenchmark for (2971ds/321Mi) % 25.99/4.64 % (1989765)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=3530400136:i=416:rtra=on:gtg=position:ss=axioms_2970 on theBenchmark for (2970ds/416Mi) % 25.99/4.64 % (1989766)lrs+1010_1_to=kbo:tgt=ground:fde=unused:sas=z3:si=on:sp=unary_frequency:gve=force:spb=goal:tha=off:random_seed=997987266:i=471:thf=on:kws=precedence:rtra=on_2970 on theBenchmark for (2970ds/471Mi) % 25.99/4.64 % (1989765)Refutation not found, incomplete strategy % 32.28/5.23 % (1989765)------------------------------ % 32.28/5.23 % (1989765)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.28/5.23 % (1989765)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.28/5.23 % (1989765)CaDiCaL version: 2.1.3 % 32.28/5.23 % (1989765)Termination reason: Refutation not found, incomplete strategy % 32.28/5.23 % (1989765)Time elapsed: 0.047 s % 32.28/5.23 % (1989765)Peak memory usage: 111 MB % 32.28/5.23 % (1989765)Instructions burned: 73 (million) % 32.28/5.23 % (1989763)Refutation not found, incomplete strategy % 32.28/5.23 % (1989763)------------------------------ % 32.28/5.23 % (1989763)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.28/5.23 % (1989763)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.28/5.23 % (1989763)CaDiCaL version: 2.1.3 % 32.28/5.23 % (1989763)Termination reason: Refutation not found, incomplete strategy % 32.28/5.23 % (1989763)Time elapsed: 0.088 s % 32.28/5.23 % (1989763)Peak memory usage: 112 MB % 32.28/5.23 % (1989763)Instructions burned: 73 (million) % 32.28/5.23 % (1989767)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=1816314484:avsq=on:i=276:avsqr=1,2:rtra=on_2969 on theBenchmark for (2969ds/276Mi) % 32.28/5.23 % (1989768)lrs+1010_2_to=kbo:sil=128000:tgt=ground:fde=unused:sas=z3:si=on:uwa=off:tha=off:nwc=1:random_seed=374077592:i=375:kws=inv_arity_squared:rtra=on_2969 on theBenchmark for (2969ds/375Mi) % 32.28/5.23 % (1989758)------------------------------ % 32.28/5.23 % (1989758)------------------------------ % 32.28/5.23 % (1989771)lrs+10_1_to=kbo:sil=128000:tgt=full:sas=z3:si=on:uwa=func_ext:slsqc=1:flr=on:slsq=on:random_seed=531110529:i=387:bd=preordered:rtra=on:ss=axioms:sgt=8_2969 on theBenchmark for (2969ds/387Mi) % 32.28/5.23 % (1989765)------------------------------ % 32.28/5.23 % (1989765)------------------------------ % 32.28/5.23 % (1989766)Instruction limit reached! % 32.28/5.23 % (1989766)------------------------------ % 32.28/5.23 % (1989766)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.28/5.23 % (1989766)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.28/5.23 % (1989766)CaDiCaL version: 2.1.3 % 32.28/5.23 % (1989766)Termination reason: Instruction limit % 32.28/5.23 % (1989766)Termination phase: Saturation % 32.28/5.23 % (1989766)Time elapsed: 0.286 s % 32.28/5.23 % (1989766)Peak memory usage: 112 MB % 32.28/5.23 % (1989766)Instructions burned: 472 (million) % 32.28/5.23 % (1989771)Refutation not found, incomplete strategy % 32.28/5.23 % (1989771)------------------------------ % 32.28/5.23 % (1989771)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.28/5.23 % (1989771)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.28/5.23 % (1989771)CaDiCaL version: 2.1.3 % 32.28/5.23 % (1989771)Termination reason: Refutation not found, incomplete strategy % 32.28/5.23 % (1989771)Time elapsed: 0.090 s % 32.28/5.23 % (1989771)Peak memory usage: 111 MB % 32.28/5.23 % (1989771)Instructions burned: 77 (million) % 32.28/5.23 % (1989767)Instruction limit reached! % 32.28/5.23 % (1989767)------------------------------ % 32.28/5.23 % (1989767)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.28/5.23 % (1989767)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.28/5.23 % (1989767)CaDiCaL version: 2.1.3 % 32.28/5.23 % (1989767)Termination reason: Instruction limit % 32.28/5.23 % (1989767)Termination phase: Saturation % 32.28/5.23 % (1989767)Time elapsed: 0.261 s % 32.28/5.23 % (1989767)Peak memory usage: 130 MB % 32.28/5.23 % (1989767)Instructions burned: 276 (million) % 32.28/5.23 % (1989763)------------------------------ % 32.28/5.23 % (1989763)------------------------------ % 32.28/5.23 % (1989775)lrs+10_1_to=kbo:sil=128000:fde=none:si=on:norm_ineq=on:urr=on:nwc=0.5:random_seed=3474839650:i=513:kws=frequency:bd=all:rtra=on:gtg=exists_all:ss=axioms:sgt=4_2966 on theBenchmark for (2966ds/513Mi) % 32.28/5.23 % (1989777)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=531967593:i=334:rtra=on_2966 on theBenchmark for (2966ds/334Mi) % 32.28/5.23 % (1989768)Instruction limit reached! % 32.28/5.23 % (1989768)------------------------------ % 32.28/5.23 % (1989768)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.28/5.23 % (1989768)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.47/5.78 % (1989768)CaDiCaL version: 2.1.3 % 34.47/5.78 % (1989768)Termination reason: Instruction limit % 34.47/5.78 % (1989768)Termination phase: Saturation % 34.47/5.78 % (1989768)Time elapsed: 0.309 s % 34.47/5.78 % (1989768)Peak memory usage: 113 MB % 34.47/5.78 % (1989768)Instructions burned: 375 (million) % 34.47/5.78 % (1989778)lrs+1010_1_to=kbo:sil=64000:sas=cadical:si=on:sos=on:bce=on:random_seed=757836990:i=359:rtra=on:gtg=exists_top:ss=axioms_2965 on theBenchmark for (2965ds/359Mi) % 34.47/5.78 % (1989778)Refutation not found, incomplete strategy % 34.47/5.78 % (1989778)------------------------------ % 34.47/5.78 % (1989778)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.47/5.78 % (1989778)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.47/5.78 % (1989778)CaDiCaL version: 2.1.3 % 34.47/5.78 % (1989778)Termination reason: Refutation not found, incomplete strategy % 34.47/5.78 % (1989778)Time elapsed: 0.073 s % 34.47/5.78 % (1989778)Peak memory usage: 88 MB % 34.47/5.78 % (1989778)Instructions burned: 97 (million) % 34.47/5.78 % (1989777)Instruction limit reached! % 34.47/5.78 % (1989777)------------------------------ % 34.47/5.78 % (1989777)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.47/5.78 % (1989777)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.47/5.78 % (1989777)CaDiCaL version: 2.1.3 % 34.47/5.78 % (1989777)Termination reason: Instruction limit % 34.47/5.78 % (1989777)Termination phase: Saturation % 34.47/5.78 % (1989777)Time elapsed: 0.164 s % 34.47/5.78 % (1989777)Peak memory usage: 130 MB % 34.47/5.78 % (1989777)Instructions burned: 334 (million) % 34.47/5.78 % (1989779)dis+1010_1_to=lpo:sil=128000:thi=all:fde=unused:si=on:sp=reverse_arity:tha=off:random_seed=2859808247:i=341:gtgl=2:rtra=on:gtg=exists_sym:ev=force:fsd=on:fsdmm=1_2964 on theBenchmark for (2964ds/341Mi) % 34.47/5.78 % (1989781)lrs-2_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_max:tha=off:random_seed=947580720:st=1.5:i=261:sd=1:kws=precedence:rtra=on:ss=axioms_2964 on theBenchmark for (2964ds/261Mi) % 34.47/5.78 % (1989771)------------------------------ % 34.47/5.78 % (1989771)------------------------------ % 34.47/5.78 % (1989783)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=3893970169:s2pl=no:i=235:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2963 on theBenchmark for (2963ds/235Mi) % 34.47/5.78 % (1989781)Refutation not found, incomplete strategy % 34.47/5.78 % (1989781)------------------------------ % 34.47/5.78 % (1989781)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.47/5.78 % (1989781)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.47/5.78 % (1989781)CaDiCaL version: 2.1.3 % 34.47/5.78 % (1989781)Termination reason: Refutation not found, incomplete strategy % 34.47/5.78 % (1989781)Time elapsed: 0.069 s % 34.47/5.78 % (1989781)Peak memory usage: 111 MB % 34.47/5.78 % (1989781)Instructions burned: 48 (million) % 34.47/5.78 % (1989783)Refutation not found, incomplete strategy % 34.47/5.78 % (1989783)------------------------------ % 34.47/5.78 % (1989783)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.47/5.78 % (1989783)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.47/5.78 % (1989783)CaDiCaL version: 2.1.3 % 34.47/5.78 % (1989783)Termination reason: Refutation not found, incomplete strategy % 34.47/5.78 % (1989783)Time elapsed: 0.091 s % 34.47/5.78 % (1989783)Peak memory usage: 111 MB % 34.47/5.78 % (1989783)Instructions burned: 76 (million) % 34.47/5.78 % (1989775)Instruction limit reached! % 34.47/5.78 % (1989775)------------------------------ % 34.47/5.78 % (1989775)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.47/5.78 % (1989775)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.47/5.78 % (1989775)CaDiCaL version: 2.1.3 % 34.47/5.78 % (1989775)Termination reason: Instruction limit % 34.47/5.78 % (1989775)Termination phase: Saturation % 34.47/5.78 % (1989775)Time elapsed: 0.376 s % 34.47/5.78 % (1989775)Peak memory usage: 90 MB % 34.47/5.78 % (1989775)Instructions burned: 513 (million) % 34.47/5.78 % (1989787)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=55138696:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2962 on theBenchmark for (2962ds/273Mi) % 34.47/5.78 % (1989779)Instruction limit reached! % 34.47/5.78 % (1989779)------------------------------ % 34.47/5.78 % (1989779)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 40.56/6.55 % (1989779)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.56/6.55 % (1989779)CaDiCaL version: 2.1.3 % 40.56/6.55 % (1989779)Termination reason: Instruction limit % 40.56/6.55 % (1989779)Termination phase: Saturation % 40.56/6.55 % (1989779)Time elapsed: 0.242 s % 40.56/6.55 % (1989779)Peak memory usage: 117 MB % 40.56/6.55 % (1989779)Instructions burned: 342 (million) % 40.56/6.55 % (1989787)Instruction limit reached! % 40.56/6.55 % (1989787)------------------------------ % 40.56/6.55 % (1989787)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 40.56/6.55 % (1989787)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.56/6.55 % (1989787)CaDiCaL version: 2.1.3 % 40.56/6.55 % (1989787)Termination reason: Instruction limit % 40.56/6.55 % (1989787)Termination phase: Saturation % 40.56/6.55 % (1989787)Time elapsed: 0.110 s % 40.56/6.55 % (1989787)Peak memory usage: 91 MB % 40.56/6.55 % (1989787)Instructions burned: 274 (million) % 40.56/6.55 % (1989790)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=1440569368:i=146:doe=on:rtra=on_2961 on theBenchmark for (2961ds/146Mi) % 40.56/6.55 % (1989778)------------------------------ % 40.56/6.55 % (1989778)------------------------------ % 40.56/6.55 % (1989792)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=1976431475:i=4428:doe=on:fsr=off:rtra=on_2960 on theBenchmark for (2960ds/4428Mi) % 40.56/6.55 % (1989790)Instruction limit reached! % 40.56/6.55 % (1989790)------------------------------ % 40.56/6.55 % (1989790)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 40.56/6.55 % (1989790)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.56/6.55 % (1989790)CaDiCaL version: 2.1.3 % 40.56/6.55 % (1989790)Termination reason: Instruction limit % 40.56/6.55 % (1989790)Termination phase: Saturation % 40.56/6.55 % (1989790)Time elapsed: 0.111 s % 40.56/6.55 % (1989790)Peak memory usage: 88 MB % 40.56/6.55 % (1989790)Instructions burned: 146 (million) % 40.56/6.55 % (1989796)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=3647614340:i=1052:rtra=on_2959 on theBenchmark for (2959ds/1052Mi) % 40.56/6.55 % (1989795)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=2067348746:avsq=on:i=276:avsqr=1,2:rtra=on_2959 on theBenchmark for (2959ds/276Mi) % 40.56/6.55 % (1989781)------------------------------ % 40.56/6.55 % (1989781)------------------------------ % 40.56/6.55 % (1989783)------------------------------ % 40.56/6.55 % (1989783)------------------------------ % 40.56/6.55 % (1989798)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=4196250765:i=655:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2958 on theBenchmark for (2958ds/655Mi) % 40.56/6.55 % (1989800)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=1773773556:st=5:i=1054:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2957 on theBenchmark for (2957ds/1054Mi) % 40.56/6.55 % (1989800)Refutation not found, incomplete strategy % 40.56/6.55 % (1989800)------------------------------ % 40.56/6.55 % (1989800)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 40.56/6.55 % (1989800)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.56/6.55 % (1989800)CaDiCaL version: 2.1.3 % 40.56/6.55 % (1989800)Termination reason: Refutation not found, incomplete strategy % 40.56/6.55 % (1989800)Time elapsed: 0.031 s % 40.56/6.55 % (1989800)Peak memory usage: 87 MB % 40.56/6.55 % (1989800)Instructions burned: 42 (million) % 40.56/6.55 % (1989795)Instruction limit reached! % 40.56/6.55 % (1989795)------------------------------ % 40.56/6.55 % (1989795)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 40.56/6.55 % (1989795)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.56/6.55 % (1989795)CaDiCaL version: 2.1.3 % 40.56/6.55 % (1989795)Termination reason: Instruction limit % 40.56/6.55 % (1989795)Termination phase: Saturation % 40.56/6.55 % (1989795)Time elapsed: 0.261 s % 40.56/6.55 % (1989795)Peak memory usage: 129 MB % 40.56/6.55 % (1989795)Instructions burned: 277 (million) % 40.56/6.55 % (1989803)lrs-1002_1_to=kbo:sas=z3:si=on:norm_ineq=on:sos=on:tha=some:random_seed=3352094355:i=107:rtra=on_2956 on theBenchmark for (2956ds/107Mi) % 40.56/6.55 % (1989804)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=3584689006:s2a=on:i=450:doe=on:nm=32:rtra=on_2956 on theBenchmark for (2956ds/450Mi) % 42.12/7.04 % (1989803)Instruction limit reached! % 42.12/7.04 % (1989803)------------------------------ % 42.12/7.04 % (1989803)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 42.12/7.04 % (1989803)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.12/7.04 % (1989803)CaDiCaL version: 2.1.3 % 42.12/7.04 % (1989803)Termination reason: Instruction limit % 42.12/7.04 % (1989803)Termination phase: Saturation % 42.12/7.04 % (1989803)Time elapsed: 0.098 s % 42.12/7.04 % (1989803)Peak memory usage: 88 MB % 42.12/7.04 % (1989803)Instructions burned: 109 (million) % 42.12/7.04 % (1989796)Instruction limit reached! % 42.12/7.04 % (1989796)------------------------------ % 42.12/7.04 % (1989796)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 42.12/7.04 % (1989796)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.12/7.04 % (1989796)CaDiCaL version: 2.1.3 % 42.12/7.04 % (1989796)Termination reason: Instruction limit % 42.12/7.04 % (1989796)Termination phase: Saturation % 42.12/7.04 % (1989796)Time elapsed: 0.391 s % 42.12/7.04 % (1989796)Peak memory usage: 91 MB % 42.12/7.04 % (1989796)Instructions burned: 1053 (million) % 42.12/7.04 % (1989798)Refutation not found, incomplete strategy % 42.12/7.04 % (1989798)------------------------------ % 42.12/7.04 % (1989798)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 42.12/7.04 % (1989798)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.12/7.04 % (1989798)CaDiCaL version: 2.1.3 % 42.12/7.04 % (1989798)Termination reason: Refutation not found, incomplete strategy % 42.12/7.04 % (1989798)Time elapsed: 0.447 s % 42.12/7.04 % (1989798)Peak memory usage: 95 MB % 42.12/7.04 % (1989798)Instructions burned: 497 (million) % 42.12/7.04 % (1989811)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=3413657782:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2953 on theBenchmark for (2953ds/130Mi) % 42.12/7.04 % (1989808)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 % 42.12/7.04 % (1989808)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=564071963:i=1090:aac=none:nm=0:rtra=on:rawr=on_2954 on theBenchmark for (2954ds/1090Mi) % 42.12/7.04 % (1989800)------------------------------ % 42.12/7.04 % (1989800)------------------------------ % 42.12/7.04 % (1989811)Instruction limit reached! % 42.12/7.04 % (1989811)------------------------------ % 42.12/7.04 % (1989811)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 42.12/7.04 % (1989811)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.12/7.04 % (1989811)CaDiCaL version: 2.1.3 % 42.12/7.04 % (1989811)Termination reason: Instruction limit % 42.12/7.04 % (1989811)Termination phase: Twee Goal Transformation % 42.12/7.04 % (1989811)Time elapsed: 0.060 s % 42.12/7.04 % (1989811)Peak memory usage: 87 MB % 42.12/7.04 % (1989811)Instructions burned: 130 (million) % 42.12/7.04 % (1989812)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=3367127459:i=312:kws=inv_frequency:nm=20:rtra=on_2953 on theBenchmark for (2953ds/312Mi) % 42.12/7.04 % (1989804)Instruction limit reached! % 42.12/7.04 % (1989804)------------------------------ % 42.12/7.04 % (1989804)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 42.12/7.04 % (1989804)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.12/7.04 % (1989804)CaDiCaL version: 2.1.3 % 42.12/7.04 % (1989804)Termination reason: Instruction limit % 42.12/7.04 % (1989804)Termination phase: Saturation % 42.12/7.04 % (1989804)Time elapsed: 0.390 s % 42.12/7.04 % (1989804)Peak memory usage: 130 MB % 42.12/7.04 % (1989804)Instructions burned: 450 (million) % 42.12/7.04 % (1989816)ott+10_1_to=kbo:sil=64000:si=on:sp=reverse_frequency:sos=on:random_seed=1303329650:i=491:doe=on:rtra=on:gtg=position_2951 on theBenchmark for (2951ds/491Mi) % 42.12/7.04 % (1989817)ott+1011_4:1_to=lpo:sil=64000:si=on:spb=intro:random_seed=3293239973:s2a=on:i=835:s2at=2:rtra=on_2950 on theBenchmark for (2950ds/835Mi) % 42.12/7.04 % (1989816)Refutation not found, incomplete strategy % 42.12/7.04 % (1989816)------------------------------ % 42.12/7.04 % (1989816)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 42.12/7.04 % (1989816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.44/7.83 % (1989816)CaDiCaL version: 2.1.3 % 48.44/7.83 % (1989816)Termination reason: Refutation not found, incomplete strategy % 48.44/7.83 % (1989816)Time elapsed: 0.099 s % 48.44/7.83 % (1989816)Peak memory usage: 90 MB % 48.44/7.83 % (1989816)Instructions burned: 254 (million) % 48.44/7.83 % (1989798)------------------------------ % 48.44/7.83 % (1989798)------------------------------ % 48.44/7.83 % (1989812)Instruction limit reached! % 48.44/7.83 % (1989812)------------------------------ % 48.44/7.83 % (1989812)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.44/7.83 % (1989812)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.44/7.83 % (1989812)CaDiCaL version: 2.1.3 % 48.44/7.83 % (1989812)Termination reason: Instruction limit % 48.44/7.83 % (1989812)Termination phase: Saturation % 48.44/7.83 % (1989812)Time elapsed: 0.264 s % 48.44/7.83 % (1989812)Peak memory usage: 112 MB % 48.44/7.83 % (1989812)Instructions burned: 312 (million) % 48.44/7.83 % (1989819)ott+1011_2_to=lpo:sil=128000:si=on:sos=on:random_seed=2266006329:i=307:bd=preordered:av=off:rtra=on:ev=cautious_2949 on theBenchmark for (2949ds/307Mi) % 48.44/7.83 % (1989816)------------------------------ % 48.44/7.83 % (1989816)------------------------------ % 48.44/7.83 % (1989819)Refutation not found, incomplete strategy % 48.44/7.83 % (1989819)------------------------------ % 48.44/7.83 % (1989819)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.44/7.83 % (1989819)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.44/7.83 % (1989819)CaDiCaL version: 2.1.3 % 48.44/7.83 % (1989819)Termination reason: Refutation not found, incomplete strategy % 48.44/7.83 % (1989819)Time elapsed: 0.148 s % 48.44/7.83 % (1989819)Peak memory usage: 90 MB % 48.44/7.83 % (1989819)Instructions burned: 195 (million) % 48.44/7.83 % (1989822)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=2631034109:i=776:doe=on:rtra=on_2947 on theBenchmark for (2947ds/776Mi) % 48.44/7.83 % (1989823)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=1828799023:s2a=on:i=646:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2947 on theBenchmark for (2947ds/646Mi) % 48.44/7.83 % (1989825)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=3478153451:thitd=on:cond=fast:i=784:nm=30:rtra=on:gtg=all:tac=axiom_2945 on theBenchmark for (2945ds/784Mi) % 48.44/7.83 % (1989808)Instruction limit reached! % 48.44/7.83 % (1989808)------------------------------ % 48.44/7.83 % (1989808)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.44/7.83 % (1989808)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.44/7.83 % (1989808)CaDiCaL version: 2.1.3 % 48.44/7.83 % (1989808)Termination reason: Instruction limit % 48.44/7.83 % (1989808)Termination phase: Saturation % 48.44/7.83 % (1989808)Time elapsed: 0.822 s % 48.44/7.83 % (1989808)Peak memory usage: 118 MB % 48.44/7.83 % (1989808)Instructions burned: 1091 (million) % 48.44/7.83 % (1989817)Instruction limit reached! % 48.44/7.83 % (1989817)------------------------------ % 48.44/7.83 % (1989817)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.44/7.83 % (1989817)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.44/7.83 % (1989817)CaDiCaL version: 2.1.3 % 48.44/7.83 % (1989817)Termination reason: Instruction limit % 48.44/7.83 % (1989817)Termination phase: Saturation % 48.44/7.83 % (1989817)Time elapsed: 0.593 s % 48.44/7.83 % (1989817)Peak memory usage: 89 MB % 48.44/7.83 % (1989817)Instructions burned: 835 (million) % 48.44/7.83 % (1989819)------------------------------ % 48.44/7.83 % (1989819)------------------------------ % 48.44/7.83 % (1989830)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=3300133977:s2pl=no:i=246:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2942 on theBenchmark for (2942ds/246Mi) % 48.44/7.83 % (1989829)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=1575866580:thitd=on:s2a=on:i=1131:add=on:canc=force:bd=all:rtra=on:tac=axiom:ev=off_2943 on theBenchmark for (2943ds/1131Mi) % 48.44/7.83 % (1989825)Instruction limit reached! % 48.44/7.83 % (1989825)------------------------------ % 48.44/7.83 % (1989825)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.44/7.83 % (1989825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.42/9.28 % (1989825)CaDiCaL version: 2.1.3 % 60.42/9.28 % (1989825)Termination reason: Instruction limit % 60.42/9.28 % (1989825)Termination phase: Saturation % 60.42/9.28 % (1989825)Time elapsed: 0.311 s % 60.42/9.28 % (1989825)Peak memory usage: 113 MB % 60.42/9.28 % (1989825)Instructions burned: 787 (million) % 60.42/9.28 % (1989831)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=1270991085:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2941 on theBenchmark for (2941ds/775Mi) % 60.42/9.28 % (1989831)Refutation not found, incomplete strategy % 60.42/9.28 % (1989831)------------------------------ % 60.42/9.28 % (1989831)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 60.42/9.28 % (1989831)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.42/9.28 % (1989831)CaDiCaL version: 2.1.3 % 60.42/9.28 % (1989831)Termination reason: Refutation not found, incomplete strategy % 60.42/9.28 % (1989831)Time elapsed: 0.034 s % 60.42/9.28 % (1989831)Peak memory usage: 88 MB % 60.42/9.28 % (1989831)Instructions burned: 74 (million) % 60.42/9.28 % (1989830)Refutation not found, incomplete strategy % 60.42/9.28 % (1989830)------------------------------ % 60.42/9.28 % (1989830)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 60.42/9.28 % (1989830)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.42/9.28 % (1989830)CaDiCaL version: 2.1.3 % 60.42/9.28 % (1989830)Termination reason: Refutation not found, incomplete strategy % 60.42/9.28 % (1989830)Time elapsed: 0.089 s % 60.42/9.28 % (1989830)Peak memory usage: 111 MB % 60.42/9.28 % (1989830)Instructions burned: 76 (million) % 60.42/9.28 % (1989822)Instruction limit reached! % 60.42/9.28 % (1989822)------------------------------ % 60.42/9.28 % (1989822)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 60.42/9.28 % (1989822)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.42/9.28 % (1989822)CaDiCaL version: 2.1.3 % 60.42/9.28 % (1989822)Termination reason: Instruction limit % 60.42/9.28 % (1989822)Termination phase: Saturation % 60.42/9.28 % (1989822)Time elapsed: 0.573 s % 60.42/9.28 % (1989822)Peak memory usage: 114 MB % 60.42/9.28 % (1989822)Instructions burned: 777 (million) % 60.42/9.28 % (1989823)Instruction limit reached! % 60.42/9.28 % (1989823)------------------------------ % 60.42/9.28 % (1989823)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 60.42/9.28 % (1989823)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.42/9.28 % (1989823)CaDiCaL version: 2.1.3 % 60.42/9.28 % (1989823)Termination reason: Instruction limit % 60.42/9.28 % (1989823)Termination phase: Saturation % 60.42/9.28 % (1989823)Time elapsed: 0.565 s % 60.42/9.28 % (1989823)Peak memory usage: 136 MB % 60.42/9.28 % (1989823)Instructions burned: 646 (million) % 60.42/9.28 % (1989834)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=4131367719:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2940 on theBenchmark for (2940ds/273Mi) % 60.42/9.28 % (1989836)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=19347941:i=102:nm=16:rtra=on_2939 on theBenchmark for (2939ds/102Mi) % 60.42/9.28 % (1989836)Instruction limit reached! % 60.42/9.28 % (1989836)------------------------------ % 60.42/9.28 % (1989836)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 60.42/9.28 % (1989836)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.42/9.28 % (1989836)CaDiCaL version: 2.1.3 % 60.42/9.28 % (1989836)Termination reason: Instruction limit % 60.42/9.28 % (1989836)Termination phase: Saturation % 60.42/9.28 % (1989836)Time elapsed: 0.041 s % 60.42/9.28 % (1989836)Peak memory usage: 88 MB % 60.42/9.28 % (1989836)Instructions burned: 103 (million) % 60.42/9.28 % (1989831)------------------------------ % 60.42/9.28 % (1989831)------------------------------ % 60.42/9.28 % (1989837)lrs+10_1_to=lpo:sil=128000:si=on:bsr=unit_only:tha=off:random_seed=2719677192:avsq=on:s2a=on:i=1094:s2at=5:avsqr=4463,131072:rtra=on_2939 on theBenchmark for (2939ds/1094Mi) % 60.42/9.28 % (1989830)------------------------------ % 60.42/9.28 % (1989830)------------------------------ % 60.42/9.28 % (1989834)Instruction limit reached! % 60.42/9.28 % (1989834)------------------------------ % 60.42/9.28 % (1989834)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 60.42/9.28 % (1989834)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.42/9.28 % (1989834)CaDiCaL version: 2.1.3 % 75.25/11.39 % (1989834)Termination reason: Instruction limit % 75.25/11.39 % (1989834)Termination phase: Saturation % 75.25/11.39 % (1989834)Time elapsed: 0.207 s % 75.25/11.39 % (1989834)Peak memory usage: 91 MB % 75.25/11.39 % (1989834)Instructions burned: 274 (million) % 75.25/11.39 % (1989840)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=1388381023:i=6400:doe=on:fsr=off:rtra=on_2937 on theBenchmark for (2937ds/6400Mi) % 75.25/11.39 % (1989841)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=3865775945:i=868:doe=on:nm=0:rtra=on:gtg=exists_sym_2936 on theBenchmark for (2936ds/868Mi) % 75.25/11.39 % (1989843)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=1972716644:i=1846:canc=cautious:fsr=off:rtra=on_2935 on theBenchmark for (2935ds/1846Mi) % 75.25/11.39 % (1989844)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=1056745215:s2a=on:i=36816:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2935 on theBenchmark for (2935ds/36816Mi) % 75.25/11.39 % (1989829)Instruction limit reached! % 75.25/11.39 % (1989829)------------------------------ % 75.25/11.39 % (1989829)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 75.25/11.39 % (1989829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 75.25/11.39 % (1989829)CaDiCaL version: 2.1.3 % 75.25/11.39 % (1989829)Termination reason: Instruction limit % 75.25/11.39 % (1989829)Termination phase: Saturation % 75.25/11.39 % (1989829)Time elapsed: 0.881 s % 75.25/11.39 % (1989829)Peak memory usage: 114 MB % 75.25/11.39 % (1989829)Instructions burned: 1131 (million) % 75.25/11.39 % (1989843)Refutation not found, incomplete strategy % 75.25/11.39 % (1989843)------------------------------ % 75.25/11.39 % (1989843)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 75.25/11.39 % (1989843)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 75.25/11.39 % (1989843)CaDiCaL version: 2.1.3 % 75.25/11.39 % (1989843)Termination reason: Refutation not found, incomplete strategy % 75.25/11.39 % (1989843)Time elapsed: 0.129 s % 75.25/11.39 % (1989843)Peak memory usage: 89 MB % 75.25/11.39 % (1989843)Instructions burned: 170 (million) % 75.25/11.39 % (1989841)Instruction limit reached! % 75.25/11.39 % (1989841)------------------------------ % 75.25/11.39 % (1989841)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 75.25/11.39 % (1989841)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 75.25/11.39 % (1989841)CaDiCaL version: 2.1.3 % 75.25/11.39 % (1989841)Termination reason: Instruction limit % 75.25/11.39 % (1989841)Termination phase: Saturation % 75.25/11.39 % (1989841)Time elapsed: 0.408 s % 75.25/11.39 % (1989841)Peak memory usage: 129 MB % 75.25/11.39 % (1989841)Instructions burned: 869 (million) % 75.25/11.39 % (1989849)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=3102469488:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2931 on theBenchmark for (2931ds/273Mi) % 75.25/11.39 % (1989837)Instruction limit reached! % 75.25/11.39 % (1989837)------------------------------ % 75.25/11.39 % (1989837)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 75.25/11.39 % (1989837)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 75.25/11.39 % (1989837)CaDiCaL version: 2.1.3 % 75.25/11.39 % (1989837)Termination reason: Instruction limit % 75.25/11.39 % (1989837)Termination phase: Saturation % 75.25/11.39 % (1989837)Time elapsed: 0.756 s % 75.25/11.39 % (1989837)Peak memory usage: 92 MB % 75.25/11.39 % (1989837)Instructions burned: 1095 (million) % 75.25/11.39 % (1989850)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=4097739993:i=863:doe=on:nm=0:rtra=on:gtg=exists_sym_2930 on theBenchmark for (2930ds/863Mi) % 75.25/11.39 % (1989843)------------------------------ % 75.25/11.39 % (1989843)------------------------------ % 75.25/11.39 % (1989849)Instruction limit reached! % 75.25/11.39 % (1989849)------------------------------ % 75.25/11.39 % (1989849)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 75.25/11.39 % (1989849)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 75.25/11.39 % (1989849)CaDiCaL version: 2.1.3 % 75.25/11.39 % (1989849)Termination reason: Instruction limit % 75.25/11.39 % (1989849)Termination phase: Saturation % 75.25/11.39 % (1989849)Time elapsed: 0.208 s % 75.25/11.39 % (1989849)Peak memory usage: 91 MB % 75.25/11.39 % (1989849)Instructions burned: 274 (million) % 81.12/12.18 % (1989792)Instruction limit reached! % 81.12/12.18 % (1989792)------------------------------ % 81.12/12.18 % (1989792)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 81.12/12.18 % (1989792)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 81.12/12.18 % (1989792)CaDiCaL version: 2.1.3 % 81.12/12.18 % (1989792)Termination reason: Instruction limit % 81.12/12.18 % (1989792)Termination phase: Saturation % 81.12/12.18 % (1989792)Time elapsed: 3.073 s % 81.12/12.18 % (1989792)Peak memory usage: 90 MB % 81.12/12.18 % (1989792)Instructions burned: 4429 (million) % 81.12/12.18 % (1989852)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=1790769359:i=5811:kws=precedence:nm=0:rtra=on_2928 on theBenchmark for (2928ds/5811Mi) % 81.12/12.18 % (1989854)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=1253053874:i=2216:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2927 on theBenchmark for (2927ds/2216Mi) % 81.12/12.18 % (1989855)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=1631230274:i=801:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2927 on theBenchmark for (2927ds/801Mi) % 81.12/12.18 % (1989856)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=1903145912:st=5:i=1026:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2926 on theBenchmark for (2926ds/1026Mi) % 81.12/12.18 % (1989850)Instruction limit reached! % 81.12/12.18 % (1989850)------------------------------ % 81.12/12.18 % (1989850)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 81.12/12.18 % (1989850)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 81.12/12.18 % (1989850)CaDiCaL version: 2.1.3 % 81.12/12.18 % (1989850)Termination reason: Instruction limit % 81.12/12.18 % (1989850)Termination phase: Saturation % 81.12/12.18 % (1989850)Time elapsed: 0.408 s % 81.12/12.18 % (1989850)Peak memory usage: 128 MB % 81.12/12.18 % (1989850)Instructions burned: 865 (million) % 81.12/12.18 % (1989856)Refutation not found, incomplete strategy % 81.12/12.18 % (1989856)------------------------------ % 81.12/12.18 % (1989856)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 81.12/12.18 % (1989856)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 81.12/12.18 % (1989856)CaDiCaL version: 2.1.3 % 81.12/12.18 % (1989856)Termination reason: Refutation not found, incomplete strategy % 81.12/12.18 % (1989856)Time elapsed: 0.031 s % 81.12/12.18 % (1989856)Peak memory usage: 87 MB % 81.12/12.18 % (1989856)Instructions burned: 42 (million) % 81.12/12.18 % (1989861)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=2096363754:i=3509:rtra=on_2924 on theBenchmark for (2924ds/3509Mi) % 81.12/12.18 % (1989855)Refutation not found, incomplete strategy % 81.12/12.18 % (1989855)------------------------------ % 81.12/12.18 % (1989855)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 81.12/12.18 % (1989855)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 81.12/12.18 % (1989855)CaDiCaL version: 2.1.3 % 81.12/12.18 % (1989855)Termination reason: Refutation not found, incomplete strategy % 81.12/12.18 % (1989855)Time elapsed: 0.462 s % 81.12/12.18 % (1989855)Peak memory usage: 95 MB % 81.12/12.18 % (1989855)Instructions burned: 497 (million) % 81.12/12.18 % (1989856)------------------------------ % 81.12/12.18 % (1989856)------------------------------ % 81.12/12.18 % (1989863)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=2681931380:st=2:i=2127:sd=12:ep=R:rtra=on:ss=axioms_2920 on theBenchmark for (2920ds/2127Mi) % 81.12/12.18 % (1989863)Refutation not found, incomplete strategy % 81.12/12.18 % (1989863)------------------------------ % 81.12/12.18 % (1989863)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 81.12/12.18 % (1989863)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 81.12/12.18 % (1989863)CaDiCaL version: 2.1.3 % 81.12/12.18 % (1989863)Termination reason: Refutation not found, incomplete strategy % 81.12/12.18 % (1989863)Time elapsed: 0.053 s % 81.12/12.18 % (1989863)Peak memory usage: 88 MB % 81.12/12.18 % (1989863)Instructions burned: 70 (million) % 81.12/12.18 % (1989855)------------------------------ % 81.12/12.18 % (1989855)------------------------------ % 81.12/12.18 % (1989865)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=450859841:i=1959:rtra=on:fsd=on:proc=on_2916 on theBenchmark for (2916ds/1959Mi) % 114.37/16.97 % (1989863)------------------------------ % 114.37/16.97 % (1989863)------------------------------ % 114.37/16.97 % (1989867)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=1547131725:s2a=on:i=3553:nm=0:rtra=on_2913 on theBenchmark for (2913ds/3553Mi) % 114.37/16.97 % (1989854)Instruction limit reached! % 114.37/16.97 % (1989854)------------------------------ % 114.37/16.97 % (1989854)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 114.37/16.97 % (1989854)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.37/16.97 % (1989854)CaDiCaL version: 2.1.3 % 114.37/16.97 % (1989854)Termination reason: Instruction limit % 114.37/16.97 % (1989854)Termination phase: Saturation % 114.37/16.97 % (1989854)Time elapsed: 1.606 s % 114.37/16.97 % (1989854)Peak memory usage: 120 MB % 114.37/16.97 % (1989854)Instructions burned: 2217 (million) % 114.37/16.97 % (1989861)Instruction limit reached! % 114.37/16.97 % (1989861)------------------------------ % 114.37/16.97 % (1989861)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 114.37/16.97 % (1989861)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.37/16.97 % (1989861)CaDiCaL version: 2.1.3 % 114.37/16.97 % (1989861)Termination reason: Instruction limit % 114.37/16.97 % (1989861)Termination phase: Saturation % 114.37/16.97 % (1989861)Time elapsed: 1.281 s % 114.37/16.97 % (1989861)Peak memory usage: 90 MB % 114.37/16.97 % (1989861)Instructions burned: 3511 (million) % 114.37/16.97 % (1989870)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=1916249873:thitd=on:cond=on:i=4093:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2909 on theBenchmark for (2909ds/4093Mi) % 114.37/16.97 % (1989869)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=745286119:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2909 on theBenchmark for (2909ds/3201Mi) % 114.37/16.97 % (1989869)Refutation not found, incomplete strategy % 114.37/16.97 % (1989869)------------------------------ % 114.37/16.97 % (1989869)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 114.37/16.97 % (1989869)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.37/16.97 % (1989869)CaDiCaL version: 2.1.3 % 114.37/16.97 % (1989869)Termination reason: Refutation not found, incomplete strategy % 114.37/16.97 % (1989869)Time elapsed: 0.495 s % 114.37/16.97 % (1989869)Peak memory usage: 93 MB % 114.37/16.97 % (1989869)Instructions burned: 668 (million) % 114.37/16.97 % (1989865)Instruction limit reached! % 114.37/16.97 % (1989865)------------------------------ % 114.37/16.97 % (1989865)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 114.37/16.97 % (1989865)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.37/16.97 % (1989865)CaDiCaL version: 2.1.3 % 114.37/16.97 % (1989865)Termination reason: Instruction limit % 114.37/16.97 % (1989865)Termination phase: Saturation % 114.37/16.97 % (1989865)Time elapsed: 1.456 s % 114.37/16.97 % (1989865)Peak memory usage: 119 MB % 114.37/16.97 % (1989865)Instructions burned: 1959 (million) % 114.37/16.97 % (1989869)------------------------------ % 114.37/16.97 % (1989869)------------------------------ % 114.37/16.97 % (1989875)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=250178165:cond=fast:i=21173:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2898 on theBenchmark for (2898ds/21173Mi) % 114.37/16.97 % (1989875)Refutation not found, incomplete strategy % 114.37/16.97 % (1989875)------------------------------ % 114.37/16.97 % (1989875)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 114.37/16.97 % (1989875)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.37/16.97 % (1989875)CaDiCaL version: 2.1.3 % 114.37/16.97 % (1989875)Termination reason: Refutation not found, incomplete strategy % 114.37/16.97 % (1989875)Time elapsed: 0.064 s % 114.37/16.97 % (1989875)Peak memory usage: 112 MB % 114.37/16.97 % (1989875)Instructions burned: 41 (million) % 114.37/16.97 % (1989877)lrs+11_1_to=lpo:thi=all:sas=z3:si=on:fd=off:sac=on:slsq=on:random_seed=2521287040:avsq=on:i=10544:avsqr=17,4:canc=force:rtra=on:gtg=exists_top:er=filter_2897 on theBenchmark for (2897ds/10544Mi) % 114.37/16.97 % (1989870)Instruction limit reached! % 114.37/16.97 % (1989870)------------------------------ % 114.37/16.97 % (1989870)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 114.37/16.97 % (1989870)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.29/19.30 % (1989870)CaDiCaL version: 2.1.3 % 131.29/19.30 % (1989870)Termination reason: Instruction limit % 131.29/19.30 % (1989870)Termination phase: Saturation % 131.29/19.30 % (1989870)Time elapsed: 1.526 s % 131.29/19.30 % (1989870)Peak memory usage: 132 MB % 131.29/19.30 % (1989870)Instructions burned: 4095 (million) % 131.29/19.30 % (1989875)------------------------------ % 131.29/19.30 % (1989875)------------------------------ % 131.29/19.30 % (1989881)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=839815338:avsq=on:i=1262:avsqr=1,16:rtra=on:rawr=on_2892 on theBenchmark for (2892ds/1262Mi) % 131.29/19.30 % (1989840)Instruction limit reached! % 131.29/19.30 % (1989840)------------------------------ % 131.29/19.30 % (1989840)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 131.29/19.30 % (1989840)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.29/19.30 % (1989840)CaDiCaL version: 2.1.3 % 131.29/19.30 % (1989840)Termination reason: Instruction limit % 131.29/19.30 % (1989840)Termination phase: Saturation % 131.29/19.30 % (1989840)Time elapsed: 4.461 s % 131.29/19.30 % (1989840)Peak memory usage: 90 MB % 131.29/19.30 % (1989840)Instructions burned: 6401 (million) % 131.29/19.30 % (1989882)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=3445552018:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2891 on theBenchmark for (2891ds/775Mi) % 131.29/19.30 % (1989882)Refutation not found, incomplete strategy % 131.29/19.30 % (1989882)------------------------------ % 131.29/19.30 % (1989882)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 131.29/19.30 % (1989882)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.29/19.30 % (1989882)CaDiCaL version: 2.1.3 % 131.29/19.30 % (1989882)Termination reason: Refutation not found, incomplete strategy % 131.29/19.30 % (1989882)Time elapsed: 0.056 s % 131.29/19.30 % (1989882)Peak memory usage: 88 MB % 131.29/19.30 % (1989882)Instructions burned: 74 (million) % 131.29/19.30 % (1989867)Instruction limit reached! % 131.29/19.30 % (1989867)------------------------------ % 131.29/19.30 % (1989867)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 131.29/19.30 % (1989867)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.29/19.30 % (1989867)CaDiCaL version: 2.1.3 % 131.29/19.30 % (1989867)Termination reason: Instruction limit % 131.29/19.30 % (1989867)Termination phase: Saturation % 131.29/19.30 % (1989867)Time elapsed: 2.314 s % 131.29/19.30 % (1989867)Peak memory usage: 91 MB % 131.29/19.30 % (1989867)Instructions burned: 3553 (million) % 131.29/19.30 % (1989884)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=3488148367:i=270:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2890 on theBenchmark for (2890ds/270Mi) % 131.29/19.30 % (1989884)Instruction limit reached! % 131.29/19.30 % (1989884)------------------------------ % 131.29/19.30 % (1989884)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 131.29/19.30 % (1989884)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.29/19.30 % (1989884)CaDiCaL version: 2.1.3 % 131.29/19.30 % (1989884)Termination reason: Instruction limit % 131.29/19.30 % (1989884)Termination phase: Saturation % 131.29/19.30 % (1989884)Time elapsed: 0.203 s % 131.29/19.30 % (1989884)Peak memory usage: 91 MB % 131.29/19.30 % (1989884)Instructions burned: 270 (million) % 131.29/19.30 % (1989881)Instruction limit reached! % 131.29/19.30 % (1989881)------------------------------ % 131.29/19.30 % (1989881)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 131.29/19.30 % (1989881)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.29/19.30 % (1989881)CaDiCaL version: 2.1.3 % 131.29/19.30 % (1989881)Termination reason: Instruction limit % 131.29/19.30 % (1989881)Termination phase: Saturation % 131.29/19.30 % (1989881)Time elapsed: 0.496 s % 131.29/19.30 % (1989881)Peak memory usage: 119 MB % 131.29/19.30 % (1989881)Instructions burned: 1263 (million) % 131.29/19.30 % (1989886)ott+10_128_isp=bottom:to=lpo:sil=128000:si=on:urr=on:uwa=alasca_main:sac=on:slsq=on:random_seed=2245292541:i=17165:aac=none:doe=on:rtra=on:gtg=exists_all_2887 on theBenchmark for (2887ds/17165Mi) % 131.29/19.30 % (1989882)------------------------------ % 131.29/19.30 % (1989882)------------------------------ % 131.29/19.30 % (1989852)Instruction limit reached! % 131.29/19.30 % (1989852)------------------------------ % 131.29/19.30 % (1989852)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 131.29/19.30 % (1989852)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 154.58/22.50 % (1989852)CaDiCaL version: 2.1.3 % 154.58/22.50 % (1989852)Termination reason: Instruction limit % 154.58/22.50 % (1989852)Termination phase: Saturation % 154.58/22.50 % (1989852)Time elapsed: 4.204 s % 154.58/22.50 % (1989852)Peak memory usage: 119 MB % 154.58/22.50 % (1989852)Instructions burned: 5811 (million) % 154.58/22.50 % (1989888)lrs+2_10_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_main:tha=some:random_seed=445879177:s2a=on:i=13094:s2at=-1:rtra=on_2885 on theBenchmark for (2885ds/13094Mi) % 154.58/22.50 % (1989889)lrs+10_1_to=lpo:sil=128000:si=on:sp=occurrence:random_seed=4043439371:st=2:i=12633:rtra=on:ss=axioms_2885 on theBenchmark for (2885ds/12633Mi) % 154.58/22.50 % (1989889)Refutation not found, incomplete strategy % 154.58/22.50 % (1989889)------------------------------ % 154.58/22.50 % (1989889)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 154.58/22.50 % (1989889)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 154.58/22.50 % (1989889)CaDiCaL version: 2.1.3 % 154.58/22.50 % (1989889)Termination reason: Refutation not found, incomplete strategy % 154.58/22.50 % (1989889)Time elapsed: 0.051 s % 154.58/22.50 % (1989889)Peak memory usage: 87 MB % 154.58/22.50 % (1989889)Instructions burned: 65 (million) % 154.58/22.50 % (1989891)dis+1011_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_frequency:lsd=20:nwc=3:random_seed=3642202070:i=1783:rtra=on:gtg=position_2884 on theBenchmark for (2884ds/1783Mi) % 154.58/22.50 % (1989892)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=4219421538:i=5451:aac=none:doe=on:nm=0:rtra=on:amm=off:gtg=position_2884 on theBenchmark for (2884ds/5451Mi) % 154.58/22.50 % (1989889)------------------------------ % 154.58/22.50 % (1989889)------------------------------ % 154.58/22.50 % (1989899)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=3824764197:i=4975:doe=on:nm=0:rtra=on:gtg=exists_sym_2878 on theBenchmark for (2878ds/4975Mi) % 154.58/22.50 % (1989891)Instruction limit reached! % 154.58/22.50 % (1989891)------------------------------ % 154.58/22.50 % (1989891)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 154.58/22.50 % (1989891)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 154.58/22.50 % (1989891)CaDiCaL version: 2.1.3 % 154.58/22.50 % (1989891)Termination reason: Instruction limit % 154.58/22.50 % (1989891)Termination phase: Saturation % 154.58/22.50 % (1989891)Time elapsed: 1.316 s % 154.58/22.50 % (1989891)Peak memory usage: 120 MB % 154.58/22.50 % (1989891)Instructions burned: 1783 (million) % 154.58/22.50 % (1989905)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=3687955435:i=2076:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2869 on theBenchmark for (2869ds/2076Mi) % 154.58/22.50 % (1989905)Instruction limit reached! % 154.58/22.50 % (1989905)------------------------------ % 154.58/22.50 % (1989905)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 154.58/22.50 % (1989905)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 154.58/22.50 % (1989905)CaDiCaL version: 2.1.3 % 154.58/22.50 % (1989905)Termination reason: Instruction limit % 154.58/22.50 % (1989905)Termination phase: Saturation % 154.58/22.50 % (1989905)Time elapsed: 1.526 s % 154.58/22.50 % (1989905)Peak memory usage: 119 MB % 154.58/22.50 % (1989905)Instructions burned: 2077 (million) % 154.58/22.50 % (1989911)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=1628613719:i=5145:rtra=on_2851 on theBenchmark for (2851ds/5145Mi) % 154.58/22.50 % (1989892)Instruction limit reached! % 154.58/22.50 % (1989892)------------------------------ % 154.58/22.50 % (1989892)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 154.58/22.50 % (1989892)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 154.58/22.50 % (1989892)CaDiCaL version: 2.1.3 % 154.58/22.50 % (1989892)Termination reason: Instruction limit % 154.58/22.50 % (1989892)Termination phase: Saturation % 154.58/22.50 % (1989892)Time elapsed: 3.842 s % 154.58/22.50 % (1989892)Peak memory usage: 120 MB % 154.58/22.50 % (1989892)Instructions burned: 5452 (million) % 154.58/22.50 % (1989914)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=1994748759:i=3509:rtra=on_2843 on theBenchmark for (2843ds/3509Mi) % 154.58/22.50 % (1989899)Instruction limit reached! % 154.58/22.50 % (1989899)------------------------------ % 154.58/22.50 % (1989899)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 211.99/30.68 % (1989899)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 211.99/30.68 % (1989899)CaDiCaL version: 2.1.3 % 211.99/30.68 % (1989899)Termination reason: Instruction limit % 211.99/30.68 % (1989899)Termination phase: Saturation % 211.99/30.68 % (1989899)Time elapsed: 4.067 s % 211.99/30.68 % (1989899)Peak memory usage: 131 MB % 211.99/30.68 % (1989899)Instructions burned: 4975 (million) % 211.99/30.68 % (1989888)Instruction limit reached! % 211.99/30.68 % (1989888)------------------------------ % 211.99/30.68 % (1989888)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 211.99/30.68 % (1989888)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 211.99/30.68 % (1989888)CaDiCaL version: 2.1.3 % 211.99/30.68 % (1989888)Termination reason: Instruction limit % 211.99/30.68 % (1989888)Termination phase: Saturation % 211.99/30.68 % (1989888)Time elapsed: 4.828 s % 211.99/30.68 % (1989888)Peak memory usage: 107 MB % 211.99/30.68 % (1989888)Instructions burned: 13097 (million) % 211.99/30.68 % (1989917)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=642632885:st=2:i=13800:sd=12:ep=R:rtra=on:ss=axioms_2836 on theBenchmark for (2836ds/13800Mi) % 211.99/30.68 % (1989918)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=536596706:i=1412:rtra=on:fsd=on:proc=on_2835 on theBenchmark for (2835ds/1412Mi) % 211.99/30.68 % (1989917)Refutation not found, incomplete strategy % 211.99/30.68 % (1989917)------------------------------ % 211.99/30.68 % (1989917)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 211.99/30.68 % (1989917)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 211.99/30.68 % (1989917)CaDiCaL version: 2.1.3 % 211.99/30.68 % (1989917)Termination reason: Refutation not found, incomplete strategy % 211.99/30.68 % (1989917)Time elapsed: 0.053 s % 211.99/30.68 % (1989917)Peak memory usage: 88 MB % 211.99/30.68 % (1989917)Instructions burned: 70 (million) % 211.99/30.68 % (1989917)------------------------------ % 211.99/30.68 % (1989917)------------------------------ % 211.99/30.68 % (1989923)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 % 211.99/30.68 % (1989923)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=2171338661:i=11747:aac=none:nm=0:rtra=on:rawr=on_2829 on theBenchmark for (2829ds/11747Mi) % 211.99/30.68 % (1989918)Instruction limit reached! % 211.99/30.68 % (1989918)------------------------------ % 211.99/30.68 % (1989918)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 211.99/30.68 % (1989918)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 211.99/30.68 % (1989918)CaDiCaL version: 2.1.3 % 211.99/30.68 % (1989918)Termination reason: Instruction limit % 211.99/30.68 % (1989918)Termination phase: Saturation % 211.99/30.68 % (1989918)Time elapsed: 0.688 s % 211.99/30.68 % (1989918)Peak memory usage: 119 MB % 211.99/30.68 % (1989918)Instructions burned: 1412 (million) % 211.99/30.68 % (1989926)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=598523066:s2a=on:i=3553:nm=0:rtra=on_2826 on theBenchmark for (2826ds/3553Mi) % 211.99/30.68 % (1989914)Instruction limit reached! % 211.99/30.68 % (1989914)------------------------------ % 211.99/30.68 % (1989914)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 211.99/30.68 % (1989914)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 211.99/30.68 % (1989914)CaDiCaL version: 2.1.3 % 211.99/30.68 % (1989914)Termination reason: Instruction limit % 211.99/30.68 % (1989914)Termination phase: Saturation % 211.99/30.68 % (1989914)Time elapsed: 2.420 s % 211.99/30.68 % (1989914)Peak memory usage: 89 MB % 211.99/30.68 % (1989914)Instructions burned: 3509 (million) % 211.99/30.68 % (1989929)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=2409114361:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2816 on theBenchmark for (2816ds/3201Mi) % 211.99/30.68 % (1989911)Instruction limit reached! % 211.99/30.68 % (1989911)------------------------------ % 211.99/30.68 % (1989911)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 211.99/30.68 % (1989911)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 211.99/30.68 % (1989911)CaDiCaL version: 2.1.3 % 211.99/30.68 % (1989911)Termination reason: Instruction limit % 211.99/30.68 % (1989911)Termination phase: Saturation % 211.99/30.68 % (1989911)Time elapsed: 3.572 s % 235.19/33.90 % (1989911)Peak memory usage: 95 MB % 235.19/33.90 % (1989911)Instructions burned: 5145 (million) % 235.19/33.90 % (1989932)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=1333761353:thitd=on:cond=on:i=4081:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2812 on theBenchmark for (2812ds/4081Mi) % 235.19/33.90 % (1989877)Instruction limit reached! % 235.19/33.90 % (1989877)------------------------------ % 235.19/33.90 % (1989877)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 235.19/33.90 % (1989877)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.19/33.90 % (1989877)CaDiCaL version: 2.1.3 % 235.19/33.90 % (1989877)Termination reason: Instruction limit % 235.19/33.90 % (1989877)Termination phase: Saturation % 235.19/33.90 % (1989877)Time elapsed: 8.509 s % 235.19/33.90 % (1989877)Peak memory usage: 164 MB % 235.19/33.90 % (1989877)Instructions burned: 10545 (million) % 235.19/33.90 % (1989929)Refutation not found, incomplete strategy % 235.19/33.90 % (1989929)------------------------------ % 235.19/33.90 % (1989929)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 235.19/33.90 % (1989929)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.19/33.90 % (1989929)CaDiCaL version: 2.1.3 % 235.19/33.90 % (1989929)Termination reason: Refutation not found, incomplete strategy % 235.19/33.90 % (1989929)Time elapsed: 0.422 s % 235.19/33.90 % (1989929)Peak memory usage: 93 MB % 235.19/33.90 % (1989929)Instructions burned: 666 (million) % 235.19/33.90 % (1989935)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=278032537:cond=fast:i=20260:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2810 on theBenchmark for (2810ds/20260Mi) % 235.19/33.90 % (1989935)Refutation not found, incomplete strategy % 235.19/33.90 % (1989935)------------------------------ % 235.19/33.90 % (1989935)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 235.19/33.90 % (1989935)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.19/33.90 % (1989935)CaDiCaL version: 2.1.3 % 235.19/33.90 % (1989935)Termination reason: Refutation not found, incomplete strategy % 235.19/33.91 % (1989935)Time elapsed: 0.065 s % 235.19/33.91 % (1989935)Peak memory usage: 112 MB % 235.19/33.91 % (1989935)Instructions burned: 41 (million) % 235.19/33.91 % (1989929)------------------------------ % 235.19/33.91 % (1989929)------------------------------ % 235.19/33.91 % (1989938)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=716124542:s2a=on:i=58627:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2806 on theBenchmark for (2806ds/58627Mi) % 235.19/33.91 % (1989935)------------------------------ % 235.19/33.91 % (1989935)------------------------------ % 235.19/33.91 % (1989941)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=3840764741:avsq=on:i=6258:avsqr=1,16:rtra=on:rawr=on_2802 on theBenchmark for (2802ds/6258Mi) % 235.19/33.91 % (1989926)Instruction limit reached! % 235.19/33.91 % (1989926)------------------------------ % 235.19/33.91 % (1989926)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 235.19/33.91 % (1989926)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.19/33.91 % (1989926)CaDiCaL version: 2.1.3 % 235.19/33.91 % (1989926)Termination reason: Instruction limit % 235.19/33.91 % (1989926)Termination phase: Saturation % 235.19/33.91 % (1989926)Time elapsed: 2.448 s % 235.19/33.91 % (1989926)Peak memory usage: 91 MB % 235.19/33.91 % (1989926)Instructions burned: 3553 (million) % 235.19/33.91 % (1989944)ott+10_128_isp=bottom:to=lpo:sil=128000:si=on:urr=on:uwa=alasca_main:sac=on:slsq=on:random_seed=2775382353:i=34001:aac=none:doe=on:rtra=on:gtg=exists_all_2799 on theBenchmark for (2799ds/34001Mi) % 235.19/33.91 % (1989932)Instruction limit reached! % 235.19/33.91 % (1989932)------------------------------ % 235.19/33.91 % (1989932)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 235.19/33.91 % (1989932)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.19/33.91 % (1989932)CaDiCaL version: 2.1.3 % 235.19/33.91 % (1989932)Termination reason: Instruction limit % 235.19/33.91 % (1989932)Termination phase: Saturation % 235.19/33.91 % (1989932)Time elapsed: 2.861 s % 235.19/33.91 % (1989932)Peak memory usage: 136 MB % 235.19/33.91 % (1989932)Instructions burned: 4082 (million) % 235.19/33.91 % (1989923)Instruction limit reached! % 235.19/33.91 % (1989923)------------------------------ % 235.19/33.91 % (1989923)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 257.86/37.08 % (1989923)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 257.86/37.08 % (1989923)CaDiCaL version: 2.1.3 % 257.86/37.08 % (1989923)Termination reason: Instruction limit % 257.86/37.08 % (1989923)Termination phase: Saturation % 257.86/37.08 % (1989923)Time elapsed: 4.605 s % 257.86/37.08 % (1989923)Peak memory usage: 124 MB % 257.86/37.08 % (1989923)Instructions burned: 11750 (million) % 257.86/37.08 % (1989956)lrs+2_10_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_main:tha=some:random_seed=4163638052:s2a=on:i=71622:s2at=-1:rtra=on_2782 on theBenchmark for (2782ds/71622Mi) % 257.86/37.08 % (1989957)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=2753292460:i=24001:kws=precedence:nm=0:rtra=on_2780 on theBenchmark for (2780ds/24001Mi) % 257.86/37.08 % (1989886)Instruction limit reached! % 257.86/37.08 % (1989886)------------------------------ % 257.86/37.08 % (1989886)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 257.86/37.08 % (1989886)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 257.86/37.08 % (1989886)CaDiCaL version: 2.1.3 % 257.86/37.08 % (1989886)Termination reason: Instruction limit % 257.86/37.08 % (1989886)Termination phase: Saturation % 257.86/37.08 % (1989886)Time elapsed: 11.761 s % 257.86/37.08 % (1989886)Peak memory usage: 90 MB % 257.86/37.08 % (1989886)Instructions burned: 17165 (million) % 257.86/37.08 % (1989966)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=3537091539:i=2076:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2767 on theBenchmark for (2767ds/2076Mi) % 257.86/37.08 % (1989941)Instruction limit reached! % 257.86/37.08 % (1989941)------------------------------ % 257.86/37.08 % (1989941)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 257.86/37.08 % (1989941)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 257.86/37.08 % (1989941)CaDiCaL version: 2.1.3 % 257.86/37.08 % (1989941)Termination reason: Instruction limit % 257.86/37.08 % (1989941)Termination phase: Saturation % 257.86/37.08 % (1989941)Time elapsed: 3.856 s % 257.86/37.08 % (1989941)Peak memory usage: 120 MB % 257.86/37.08 % (1989941)Instructions burned: 6258 (million) % 257.86/37.08 % (1989971)dis+21_20_to=lakbo:si=on:alasca=on:sp=const_max:uwa=alasca_main:sac=on:random_seed=1679575263:s2a=on:i=83971:s2at=4:bd=all:ins=1:rtra=on_2762 on theBenchmark for (2762ds/83971Mi) % 257.86/37.08 % (1989966)Instruction limit reached! % 257.86/37.08 % (1989966)------------------------------ % 257.86/37.08 % (1989966)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 257.86/37.08 % (1989966)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 257.86/37.08 % (1989966)CaDiCaL version: 2.1.3 % 257.86/37.08 % (1989966)Termination reason: Instruction limit % 257.86/37.08 % (1989966)Termination phase: Saturation % 257.86/37.08 % (1989966)Time elapsed: 1.394 s % 257.86/37.08 % (1989966)Peak memory usage: 119 MB % 257.86/37.08 % (1989966)Instructions burned: 2076 (million) % 257.86/37.08 % (1989982)lrs+1011_5:1_to=lpo:sil=128000:sas=z3:si=on:norm_ineq=on:tha=some:random_seed=2108709657:i=83944:rtra=on_2750 on theBenchmark for (2750ds/83944Mi) % 257.86/37.08 % (1989957)Instruction limit reached! % 257.86/37.08 % (1989957)------------------------------ % 257.86/37.08 % (1989957)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 257.86/37.08 % (1989957)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 257.86/37.08 % (1989957)CaDiCaL version: 2.1.3 % 257.86/37.08 % (1989957)Termination reason: Instruction limit % 257.86/37.08 % (1989957)Termination phase: Saturation % 257.86/37.08 % (1989957)Time elapsed: 7.647 s % 257.86/37.08 % (1989957)Peak memory usage: 128 MB % 257.86/37.08 % (1989957)Instructions burned: 24001 (million) % 257.86/37.08 % (1990052)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=3938409966:i=9201:rtra=on_2702 on theBenchmark for (2702ds/9201Mi) % 257.86/37.08 % (1989844)Instruction limit reached! % 257.86/37.08 % (1989844)------------------------------ % 257.86/37.08 % (1989844)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 257.86/37.08 % (1989844)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 257.86/37.08 % (1989844)CaDiCaL version: 2.1.3 % 257.86/37.08 % (1989844)Termination reason: Instruction limit % 257.86/37.08 % (1989844)Termination phase: Saturation % 257.86/37.08 % (1989844)Time elapsed: 23.381 s % 257.86/37.08 % (1989844)Peak memory usage: 104 MB % 257.86/37.08 % (1989844)Instructions burned: 36818 (million) % 289.45/41.55 % (1990054)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 % 289.45/41.55 % (1990054)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=2624639278:i=6806:aac=none:nm=0:rtra=on:rawr=on_2699 on theBenchmark for (2699ds/6806Mi) % 289.45/41.55 % (1990052)Instruction limit reached! % 289.45/41.55 % (1990052)------------------------------ % 289.45/41.55 % (1990052)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 289.45/41.55 % (1990052)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.45/41.55 % (1990052)CaDiCaL version: 2.1.3 % 289.45/41.55 % (1990052)Termination reason: Instruction limit % 289.45/41.55 % (1990052)Termination phase: Saturation % 289.45/41.55 % (1990052)Time elapsed: 1.771 s % 289.45/41.55 % (1990052)Peak memory usage: 90 MB % 289.45/41.55 % (1990052)Instructions burned: 9205 (million) % 289.45/41.55 % (1990056)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=1903268695:s2a=on:i=3553:nm=0:rtra=on_2683 on theBenchmark for (2683ds/3553Mi) % 289.45/41.55 % (1990056)Instruction limit reached! % 289.45/41.55 % (1990056)------------------------------ % 289.45/41.55 % (1990056)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 289.45/41.55 % (1990056)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.45/41.55 % (1990056)CaDiCaL version: 2.1.3 % 289.45/41.55 % (1990056)Termination reason: Instruction limit % 289.45/41.55 % (1990056)Termination phase: Saturation % 289.45/41.55 % (1990056)Time elapsed: 0.688 s % 289.45/41.55 % (1990056)Peak memory usage: 92 MB % 289.45/41.55 % (1990056)Instructions burned: 3560 (million) % 289.45/41.55 % (1990058)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=2916500549:thitd=on:cond=on:i=2064:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2675 on theBenchmark for (2675ds/2064Mi) % 289.45/41.55 % (1990054)Instruction limit reached! % 289.45/41.55 % (1990054)------------------------------ % 289.45/41.55 % (1990054)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 289.45/41.55 % (1990054)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.45/41.55 % (1990054)CaDiCaL version: 2.1.3 % 289.45/41.55 % (1990054)Termination reason: Instruction limit % 289.45/41.55 % (1990054)Termination phase: Saturation % 289.45/41.55 % (1990054)Time elapsed: 2.459 s % 289.45/41.55 % (1990054)Peak memory usage: 119 MB % 289.45/41.55 % (1990054)Instructions burned: 6809 (million) % 289.45/41.55 % (1990060)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=860525277:cond=fast:i=20260:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2672 on theBenchmark for (2672ds/20260Mi) % 289.45/41.55 % (1990060)Refutation not found, incomplete strategy % 289.45/41.55 % (1990060)------------------------------ % 289.45/41.55 % (1990060)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 289.45/41.55 % (1990060)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.45/41.55 % (1990060)CaDiCaL version: 2.1.3 % 289.45/41.55 % (1990060)Termination reason: Refutation not found, incomplete strategy % 289.45/41.55 % (1990060)Time elapsed: 0.039 s % 289.45/41.55 % (1990060)Peak memory usage: 112 MB % 289.45/41.55 % (1990060)Instructions burned: 41 (million) % 289.45/41.55 % (1990058)Instruction limit reached! % 289.45/41.55 % (1990058)------------------------------ % 289.45/41.55 % (1990058)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 289.45/41.55 % (1990058)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.45/41.55 % (1990058)CaDiCaL version: 2.1.3 % 289.45/41.55 % (1990058)Termination reason: Instruction limit % 289.45/41.55 % (1990058)Termination phase: Saturation % 289.45/41.55 % (1990058)Time elapsed: 0.422 s % 289.45/41.55 % (1990058)Peak memory usage: 131 MB % 289.45/41.55 % (1990058)Instructions burned: 2065 (million) % 289.45/41.55 % (1990060)------------------------------ % 289.45/41.55 % (1990060)------------------------------ % 289.45/41.55 % (1990062)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=2059644756:avsq=on:i=1244:avsqr=1,16:rtra=on:rawr=on_2669 on theBenchmark for (2669ds/1244Mi) % 289.45/41.55 % (1990064)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=872623393:i=58261:doe=on:nm=0:rtra=on:gtg=exists_sym_2668 on theBenchmark for (2668ds/58261Mi) % 297.21/42.63 % (1990062)Instruction limit reached! % 297.21/42.63 % (1990062)------------------------------ % 297.21/42.63 % (1990062)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 297.21/42.63 % (1990062)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 297.21/42.63 % (1990062)CaDiCaL version: 2.1.3 % 297.21/42.63 % (1990062)Termination reason: Instruction limit % 297.21/42.63 % (1990062)Termination phase: Saturation % 297.21/42.63 % (1990062)Time elapsed: 0.259 s % 297.21/42.63 % (1990062)Peak memory usage: 119 MB % 297.21/42.63 % (1990062)Instructions burned: 1253 (million) % 297.21/42.63 % (1990066)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 % 297.21/42.63 % (1990066)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=380410080:i=6806:aac=none:nm=0:rtra=on:rawr=on_2665 on theBenchmark for (2665ds/6806Mi) % 297.21/42.63 % (1990066)Instruction limit reached! % 297.21/42.63 % (1990066)------------------------------ % 297.21/42.63 % (1990066)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 297.21/42.63 % (1990066)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 297.21/42.63 % (1990066)CaDiCaL version: 2.1.3 % 297.21/42.63 % (1990066)Termination reason: Instruction limit % 297.21/42.63 % (1990066)Termination phase: Saturation % 297.21/42.63 % (1990066)Time elapsed: 1.309 s % 297.21/42.63 % (1990066)Peak memory usage: 119 MB % 297.21/42.63 % (1990066)Instructions burned: 6812 (million) % 297.21/42.63 % (1990068)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=4062507411:thitd=on:cond=on:i=4081:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2651 on theBenchmark for (2651ds/4081Mi) % 297.21/42.63 % (1990068)Instruction limit reached! % 297.21/42.63 % (1990068)------------------------------ % 297.21/42.63 % (1990068)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 297.21/42.63 % (1990068)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 297.21/42.63 % (1990068)CaDiCaL version: 2.1.3 % 297.21/42.63 % (1990068)Termination reason: Instruction limit % 297.21/42.63 % (1990068)Termination phase: Saturation % 297.21/42.63 % (1990068)Time elapsed: 0.813 s % 297.21/42.63 % (1990068)Peak memory usage: 132 MB % 297.21/42.63 % (1990068)Instructions burned: 4086 (million) % 297.21/42.63 % (1990070)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=296644078:avsq=on:i=1701:avsqr=1,16:rtra=on:rawr=on_2642 on theBenchmark for (2642ds/1701Mi) % 297.21/42.63 % (1990070)Instruction limit reached! % 297.21/42.63 % (1990070)------------------------------ % 297.21/42.63 % (1990070)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 297.21/42.63 % (1990070)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 297.21/42.63 % (1990070)CaDiCaL version: 2.1.3 % 297.21/42.63 % (1990070)Termination reason: Instruction limit % 297.21/42.63 % (1990070)Termination phase: Saturation % 297.21/42.63 % (1990070)Time elapsed: 0.343 s % 297.21/42.63 % (1990070)Peak memory usage: 119 MB % 297.21/42.63 % (1990070)Instructions burned: 1706 (million) % 297.21/42.63 % (1989944)Instruction limit reached! % 297.21/42.63 % (1989944)------------------------------ % 297.21/42.63 % (1989944)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 297.21/42.63 % (1989944)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 297.21/42.63 % (1989944)CaDiCaL version: 2.1.3 % 297.21/42.63 % (1989944)Termination reason: Instruction limit % 297.21/42.63 % (1989944)Termination phase: Saturation % 297.21/42.63 % (1989944)Time elapsed: 15.956 s % 297.21/42.63 % (1989944)Peak memory usage: 91 MB % 297.21/42.63 % (1989944)Instructions burned: 34004 (million) % 297.21/42.63 % (1990072)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=1713501498:i=57001:doe=on:nm=0:rtra=on:gtg=exists_sym_2637 on theBenchmark for (2637ds/57001Mi) % 297.21/42.63 % (1990073)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 % 297.21/42.63 % (1990073)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=49456084:i=8622:aac=none:nm=0:rtra=on:rawr=on_2636 on theBenchmark for (2636ds/8622Mi) % 300.44/43.07 % (1990073)Instruction limit reached! % 300.44/43.07 % (1990073)------------------------------ % 300.44/43.07 % (1990073)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.44/43.07 % (1990073)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.44/43.07 % (1990073)CaDiCaL version: 2.1.3 % 300.44/43.07 % (1990073)Termination reason: Instruction limit % 300.44/43.07 % (1990073)Termination phase: Saturation % 300.44/43.07 % (1990073)Time elapsed: 3.137 s % 300.44/43.07 % (1990073)Peak memory usage: 123 MB % 300.44/43.07 % (1990073)Instructions burned: 8623 (million) % 300.44/43.07 % (1990076)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=4115626753:i=24:doe=on:rtra=on:gtg=exists_top:ss=axioms_2603 on theBenchmark for (2603ds/24Mi) % 300.44/43.07 % (1990076)Instruction limit reached! % 300.44/43.07 % (1990076)------------------------------ % 300.44/43.07 % (1990076)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.44/43.07 % (1990076)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.44/43.07 % (1990076)CaDiCaL version: 2.1.3 % 300.44/43.07 % (1990076)Termination reason: Instruction limit % 300.44/43.07 % (1990076)Termination phase: Property scanning % 300.44/43.07 % (1990076)Time elapsed: 0.009 s % 300.44/43.07 % (1990076)Peak memory usage: 85 MB % 300.44/43.07 % (1990076)Instructions burned: 24 (million) % 300.44/43.07 % (1990078)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=961307958:i=614:kws=precedence:nm=0:rtra=on_2601 on theBenchmark for (2601ds/614Mi) % 300.44/43.07 % (1990078)Instruction limit reached! % 300.44/43.07 % (1990078)------------------------------ % 300.44/43.07 % (1990078)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.44/43.07 % (1990078)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.44/43.07 % (1990078)CaDiCaL version: 2.1.3 % 300.44/43.07 % (1990078)Termination reason: Instruction limit % 300.44/43.07 % (1990078)Termination phase: Saturation % 300.44/43.07 % (1990078)Time elapsed: 0.251 s % 300.44/43.07 % (1990078)Peak memory usage: 118 MB % 300.44/43.07 % (1990078)Instructions burned: 615 (million) % 300.44/43.07 % (1990080)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=1708835357:i=402:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2597 on theBenchmark for (2597ds/402Mi) % 300.44/43.07 % (1990080)Instruction limit reached! % 300.44/43.07 % (1990080)------------------------------ % 300.44/43.07 % (1990080)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.44/43.07 % (1990080)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.44/43.07 % (1990080)CaDiCaL version: 2.1.3 % 300.44/43.07 % (1990080)Termination reason: Instruction limit % 300.44/43.07 % (1990080)Termination phase: Saturation % 300.44/43.07 % (1990080)Time elapsed: 0.177 s % 300.44/43.07 % (1990080)Peak memory usage: 117 MB % 300.44/43.07 % (1990080)Instructions burned: 404 (million) % 300.44/43.07 % (1990082)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=3351901043:s2a=on:i=14:rtra=on:inst=on_2594 on theBenchmark for (2594ds/14Mi) % 300.44/43.07 % (1990082)Instruction limit reached! % 300.44/43.07 % (1990082)------------------------------ % 300.44/43.07 % (1990082)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.44/43.07 % (1990082)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.44/43.07 % (1990082)CaDiCaL version: 2.1.3 % 300.44/43.07 % (1990082)Termination reason: Instruction limit % 300.44/43.07 % (1990082)Termination phase: Property scanning % 300.44/43.07 % (1990082)Time elapsed: 0.006 s % 300.44/43.07 % (1990082)Peak memory usage: 85 MB % 300.44/43.07 % (1990082)Instructions burned: 16 (million) % 300.44/43.07 % (1990084)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=2262017500:i=8:rtra=on_2592 on theBenchmark for (2592ds/8Mi) % 300.44/43.07 % (1990084)Instruction limit reached! % 300.44/43.07 % (1990084)------------------------------ % 300.44/43.07 % (1990084)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.44/43.07 % (1990084)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.44/43.07 % (1990084)CaDiCaL version: 2.1.3 % 300.44/43.07 % (1990084)Termination reason: Instruction limit % 300.44/43.07 % (1990084)Termination phase: Property scanning % 300.44/43.07 % (1990084)Time elapsed: 0.004 s % 300.44/43.07 % (1990084)Peak memory usage: 85 MB % 300.44/43.07 % (1990084)Instructions burned: 10 (million) % 300.44/43.07 % (1990086)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=3270343228:i=92:rtra=on_2590 on theBenchmark for (2590ds/92Mi) % 300.44/43.07 % (1990086)Instruction limit reached! % 300.44/43.07 % (1990086)------------------------------ % 300.44/43.07 % (1990086)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.44/43.07 % (1990086)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.44/43.07 % (1990086)CaDiCaL version: 2.1.3 % 300.44/43.07 % (1990086)Termination reason: Instruction limit % 300.44/43.07 % (1990086)Termination phase: Saturation % 300.44/43.07 % (1990086)Time elapsed: 0.056 s % 300.44/43.07 % (1990086)Peak memory usage: 111 MB % 300.44/43.07 % (1990086)Instructions burned: 94 (million) % 300.44/43.07 % (1990088)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=2206782407:i=66:rtra=on_2588 on theBenchmark for (2588ds/66Mi) % 300.44/43.07 % (1990088)Instruction limit reached! % 300.44/43.07 % (1990088)------------------------------ % 300.44/43.07 % (1990088)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.44/43.07 % (1990088)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.44/43.07 % (1990088)CaDiCaL version: 2.1.3 % 300.44/43.07 % (1990088)Termination reason: Instruction limit % 300.44/43.07 % (1990088)Termination phase: Property scanning % 300.44/43.07 % (1990088)Time elapsed: 0.025 s % 300.44/43.07 % (1990088)Peak memory usage: 86 MB % 300.44/43.07 % (1990088)Instructions burned: 68 (million) % 300.44/43.07 % (1990090)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=3912268276:st=5:i=28:sd=10:rtra=on:ss=axioms:rawr=on_2586 on theBenchmark for (2586ds/28Mi) % 300.44/43.07 % (1990090)Instruction limit reached! % 300.44/43.07 % (1990090)------------------------------ % 300.44/43.07 % (1990090)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.44/43.07 % (1990090)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.44/43.07 % (1990090)CaDiCaL version: 2.1.3 % 300.44/43.07 % (1990090)Termination reason: Instruction limit % 300.44/43.07 % (1990090)Termination phase: Property scanning % 300.44/43.07 % (1990090)Time elapsed: 0.011 s % 300.44/43.07 % (1990090)Peak memory usage: 85 MB % 300.44/43.07 % (1990090)Instructions burned: 29 (million) % 300.44/43.07 % (1990092)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=242978616:i=58:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2584 on theBenchmark for (2584ds/58Mi) % 300.44/43.07 % (1990092)Instruction limit reached! % 300.44/43.07 % (1990092)------------------------------ % 300.44/43.07 % (1990092)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.44/43.07 % (1990092)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.44/43.07 % (1990092)CaDiCaL version: 2.1.3 % 300.44/43.07 % (1990092)Termination reason: Instruction limit % 300.44/43.07 % (1990092)Termination phase: Unused predicate definition removal % 300.44/43.07 % (1990092)Time elapsed: 0.022 s % 300.44/43.07 % (1990092)Peak memory usage: 86 MB % 300.44/43.07 % (1990092)Instructions burned: 59 (million) % 300.44/43.07 % (1990094)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=1633239091:cond=on:i=32:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2583 on theBenchmark for (2583ds/32Mi) % 300.44/43.07 % (1990094)Instruction limit reached! % 300.44/43.07 % (1990094)------------------------------ % 300.44/43.07 % (1990094)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.44/43.07 % (1990094)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.44/43.07 % (1990094)CaDiCaL version: 2.1.3 % 300.44/43.07 % (1990094)Termination reason: Instruction limit % 300.44/43.07 % (1990094)Termination phase: Property scanning % 300.44/43.07 % (1990094)Time elapsed: 0.013 s % 300.44/43.07 % (1990094)Peak memory usage: 86 MB % 300.44/43.07 % (1990094)Instructions burned: 34 (million) % 300.44/43.07 % (1990096)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=1402863258:i=48:canc=force:rtra=on_2581 on theBenchmark for (2581ds/48Mi) % 300.44/43.07 % (1990096)Instruction limit reached! % 300.44/43.07 % (1990096)------------------------------ % 300.44/43.07 % (1990096)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.44/43.07 % (1990096)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.44/43.07 % (1990096)CaDiCaL version: 2.1.3 % 300.44/43.07 % (1990096)Terminati % 300.44/43.07 Terminated %------------------------------------------------------------------------------