%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWX145_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 : n006.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:45:58 PM UTC 2026 % Result : Timeout 292.26s 42.11s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : SWX145_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.08/0.20 % Computer : n006.cluster.edu % 0.08/0.20 % Model : x86_64 x86_64 % 0.08/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.20 % Memory : 8046.5625MB % 0.08/0.20 % OS : Linux 6.8.0-71-generic % 0.08/0.20 % CPULimit : 300 % 0.08/0.20 % WCLimit : 300 % 0.08/0.20 % DateTime : Mon Sep 28 15:04:14 UTC 2026 % 0.08/0.20 % CPUTime : % 0.08/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.08/0.23 Running first-order theorem proving % 0.08/0.23 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 % 3.55/1.52 % (4035130)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule. % 3.55/1.52 % (4035135)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=1061476378:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2996 on theBenchmark for (2996ds/12Mi) % 3.55/1.52 % (4035135)Instruction limit reached! % 3.55/1.52 % (4035135)------------------------------ % 3.55/1.52 % (4035135)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.55/1.52 % (4035135)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.55/1.52 % (4035135)CaDiCaL version: 2.1.3 % 3.55/1.52 % (4035135)Termination reason: Instruction limit % 3.55/1.52 % (4035135)Termination phase: Property scanning % 3.55/1.52 % (4035135)Time elapsed: 0.003 s % 3.55/1.52 % (4035135)Peak memory usage: 85 MB % 3.55/1.52 % (4035135)Instructions burned: 15 (million) % 3.55/1.52 % (4035137)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=2942184712:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2996 on theBenchmark for (2996ds/201Mi) % 3.55/1.52 % (4035138)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=3297591164:s2a=on:i=7:rtra=on:inst=on_2996 on theBenchmark for (2996ds/7Mi) % 3.55/1.52 % (4035140)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=204647918:i=46:rtra=on_2996 on theBenchmark for (2996ds/46Mi) % 3.55/1.52 % (4035139)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=3379158737:i=4:rtra=on_2996 on theBenchmark for (2996ds/4Mi) % 3.55/1.52 % (4035136)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=686762439:i=307:kws=precedence:nm=0:rtra=on_2996 on theBenchmark for (2996ds/307Mi) % 3.55/1.52 % (4035139)Instruction limit reached! % 3.55/1.52 % (4035139)------------------------------ % 3.55/1.52 % (4035139)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.55/1.52 % (4035139)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.55/1.52 % (4035139)CaDiCaL version: 2.1.3 % 3.55/1.52 % (4035139)Termination reason: Instruction limit % 3.55/1.52 % (4035139)Termination phase: shuffling % 3.55/1.52 % (4035139)Time elapsed: 0.002 s % 3.55/1.52 % (4035139)Peak memory usage: 85 MB % 3.55/1.52 % (4035139)Instructions burned: 4 (million) % 3.55/1.52 % (4035138)Instruction limit reached! % 3.55/1.52 % (4035138)------------------------------ % 3.55/1.52 % (4035138)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.55/1.52 % (4035138)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.55/1.52 % (4035138)CaDiCaL version: 2.1.3 % 3.55/1.52 % (4035138)Termination reason: Instruction limit % 3.55/1.52 % (4035138)Termination phase: shuffling % 3.55/1.52 % (4035138)Time elapsed: 0.004 s % 3.55/1.52 % (4035138)Peak memory usage: 85 MB % 3.55/1.52 % (4035138)Instructions burned: 9 (million) % 3.55/1.52 % (4035141)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=2615284352:i=33:rtra=on_2996 on theBenchmark for (2996ds/33Mi) % 3.55/1.52 % (4035140)Instruction limit reached! % 3.55/1.52 % (4035140)------------------------------ % 3.55/1.52 % (4035140)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.55/1.52 % (4035140)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.55/1.52 % (4035140)CaDiCaL version: 2.1.3 % 3.55/1.52 % (4035140)Termination reason: Instruction limit % 3.55/1.52 % (4035140)Termination phase: Property scanning % 3.55/1.52 % (4035140)Time elapsed: 0.019 s % 3.55/1.52 % (4035140)Peak memory usage: 85 MB % 3.55/1.52 % (4035140)Instructions burned: 46 (million) % 3.55/1.52 % (4035141)Instruction limit reached! % 3.55/1.52 % (4035141)------------------------------ % 3.55/1.52 % (4035141)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.55/1.52 % (4035141)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.55/1.52 % (4035141)CaDiCaL version: 2.1.3 % 3.55/1.52 % (4035141)Termination reason: Instruction limit % 3.55/1.52 % (4035141)Termination phase: Property scanning % 3.55/1.52 % (4035141)Time elapsed: 0.015 s % 3.55/1.52 % (4035141)Peak memory usage: 86 MB % 3.55/1.52 % (4035141)Instructions burned: 36 (million) % 3.55/1.52 % (4035143)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=204539278:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2995 on theBenchmark for (2995ds/14Mi) % 3.55/1.52 % (4035143)Instruction limit reached! % 3.55/1.52 % (4035143)------------------------------ % 4.18/1.67 % (4035143)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.18/1.67 % (4035143)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.18/1.67 % (4035143)CaDiCaL version: 2.1.3 % 4.18/1.67 % (4035143)Termination reason: Instruction limit % 4.18/1.67 % (4035143)Termination phase: shuffling % 4.18/1.67 % (4035143)Time elapsed: 0.004 s % 4.18/1.67 % (4035143)Peak memory usage: 85 MB % 4.18/1.67 % (4035143)Instructions burned: 19 (million) % 4.18/1.67 % (4035137)Instruction limit reached! % 4.18/1.67 % (4035137)------------------------------ % 4.18/1.67 % (4035137)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.18/1.67 % (4035137)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.18/1.67 % (4035137)CaDiCaL version: 2.1.3 % 4.18/1.67 % (4035137)Termination reason: Instruction limit % 4.18/1.67 % (4035137)Termination phase: Property scanning % 4.18/1.67 % (4035137)Time elapsed: 0.074 s % 4.18/1.67 % (4035137)Peak memory usage: 85 MB % 4.18/1.67 % (4035137)Instructions burned: 201 (million) % 4.18/1.67 % (4035149)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=3105591028:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2994 on theBenchmark for (2994ds/29Mi) % 4.18/1.67 % (4035136)Instruction limit reached! % 4.18/1.67 % (4035136)------------------------------ % 4.18/1.67 % (4035136)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.18/1.67 % (4035136)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.18/1.67 % (4035136)CaDiCaL version: 2.1.3 % 4.18/1.67 % (4035136)Termination reason: Instruction limit % 4.18/1.67 % (4035136)Termination phase: Saturation % 4.18/1.67 % (4035136)Time elapsed: 0.138 s % 4.18/1.67 % (4035136)Peak memory usage: 112 MB % 4.18/1.67 % (4035136)Instructions burned: 309 (million) % 4.18/1.67 % (4035150)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=2091768995:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2994 on theBenchmark for (2994ds/16Mi) % 4.18/1.67 % (4035150)Instruction limit reached! % 4.18/1.67 % (4035150)------------------------------ % 4.18/1.67 % (4035150)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.18/1.67 % (4035150)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.18/1.67 % (4035150)CaDiCaL version: 2.1.3 % 4.18/1.67 % (4035150)Termination reason: Instruction limit % 4.18/1.67 % (4035150)Termination phase: shuffling % 4.18/1.67 % (4035150)Time elapsed: 0.007 s % 4.18/1.67 % (4035150)Peak memory usage: 85 MB % 4.18/1.67 % (4035150)Instructions burned: 17 (million) % 4.18/1.67 % (4035149)Instruction limit reached! % 4.18/1.67 % (4035149)------------------------------ % 4.18/1.67 % (4035149)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.18/1.67 % (4035149)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.18/1.67 % (4035149)CaDiCaL version: 2.1.3 % 4.18/1.67 % (4035149)Termination reason: Instruction limit % 4.18/1.67 % (4035149)Termination phase: Property scanning % 4.18/1.67 % (4035149)Time elapsed: 0.013 s % 4.18/1.67 % (4035149)Peak memory usage: 86 MB % 4.18/1.67 % (4035149)Instructions burned: 31 (million) % 4.18/1.67 % (4035152)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=774812670:i=24:canc=force:rtra=on_2994 on theBenchmark for (2994ds/24Mi) % 4.18/1.67 % (4035152)Instruction limit reached! % 4.18/1.67 % (4035152)------------------------------ % 4.18/1.67 % (4035152)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.18/1.67 % (4035152)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.18/1.67 % (4035152)CaDiCaL version: 2.1.3 % 4.18/1.67 % (4035152)Termination reason: Instruction limit % 4.18/1.67 % (4035152)Termination phase: Property scanning % 4.18/1.67 % (4035152)Time elapsed: 0.012 s % 4.18/1.67 % (4035152)Peak memory usage: 86 MB % 4.18/1.67 % (4035152)Instructions burned: 27 (million) % 4.18/1.67 % (4035155)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=934670842:i=85:gtgl=4:rtra=on:gtg=exists_sym_2994 on theBenchmark for (2994ds/85Mi) % 4.18/1.67 % (4035153)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=917085022:i=27:canc=cautious:fsr=off:rtra=on_2994 on theBenchmark for (2994ds/27Mi) % 4.18/1.67 % (4035153)Instruction limit reached! % 4.18/1.67 % (4035153)------------------------------ % 5.30/1.82 % (4035153)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.30/1.82 % (4035153)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.30/1.82 % (4035153)CaDiCaL version: 2.1.3 % 5.30/1.82 % (4035153)Termination reason: Instruction limit % 5.30/1.82 % (4035153)Termination phase: Property scanning % 5.30/1.82 % (4035153)Time elapsed: 0.013 s % 5.30/1.82 % (4035153)Peak memory usage: 86 MB % 5.30/1.82 % (4035153)Instructions burned: 30 (million) % 5.30/1.82 % (4035155)Instruction limit reached! % 5.30/1.82 % (4035155)------------------------------ % 5.30/1.82 % (4035155)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.30/1.82 % (4035155)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.30/1.82 % (4035155)CaDiCaL version: 2.1.3 % 5.30/1.82 % (4035155)Termination reason: Instruction limit % 5.30/1.82 % (4035155)Termination phase: Property scanning % 5.30/1.82 % (4035155)Time elapsed: 0.017 s % 5.30/1.82 % (4035155)Peak memory usage: 85 MB % 5.30/1.82 % (4035155)Instructions burned: 89 (million) % 5.30/1.82 % (4035156)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=3207935365:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2993 on theBenchmark for (2993ds/2Mi) % 5.30/1.82 % (4035156)Instruction limit reached! % 5.30/1.82 % (4035156)------------------------------ % 5.30/1.82 % (4035156)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.30/1.82 % (4035156)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.30/1.82 % (4035156)CaDiCaL version: 2.1.3 % 5.30/1.82 % (4035156)Termination reason: Instruction limit % 5.30/1.82 % (4035156)Termination phase: shuffling % 5.30/1.82 % (4035156)Time elapsed: 0.002 s % 5.30/1.82 % (4035156)Peak memory usage: 85 MB % 5.30/1.82 % (4035156)Instructions burned: 4 (million) % 5.30/1.82 % (4035160)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=3403115105:i=4:ep=RST:ins=2:rtra=on_2993 on theBenchmark for (2993ds/4Mi) % 5.30/1.82 % (4035159)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=1481579079:i=181:rtra=on:ss=axioms:ev=cautious_2993 on theBenchmark for (2993ds/181Mi) % 5.30/1.82 % (4035161)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=2717586387:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2993 on theBenchmark for (2993ds/66Mi) % 5.30/1.82 % (4035160)Instruction limit reached! % 5.30/1.82 % (4035160)------------------------------ % 5.30/1.82 % (4035160)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.30/1.82 % (4035160)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.30/1.82 % (4035160)CaDiCaL version: 2.1.3 % 5.30/1.82 % (4035160)Termination reason: Instruction limit % 5.30/1.82 % (4035160)Termination phase: shuffling % 5.30/1.82 % (4035160)Time elapsed: 0.002 s % 5.30/1.82 % (4035160)Peak memory usage: 85 MB % 5.30/1.82 % (4035160)Instructions burned: 4 (million) % 5.30/1.82 % (4035167)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=1722429427:st=3:i=2:rtra=on:ss=axioms_2992 on theBenchmark for (2992ds/2Mi) % 5.30/1.82 % (4035167)Instruction limit reached! % 5.30/1.82 % (4035167)------------------------------ % 5.30/1.82 % (4035167)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.30/1.82 % (4035167)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.30/1.82 % (4035167)CaDiCaL version: 2.1.3 % 5.30/1.82 % (4035167)Termination reason: Instruction limit % 5.30/1.82 % (4035167)Termination phase: shuffling % 5.30/1.82 % (4035167)Time elapsed: 0.001 s % 5.30/1.82 % (4035167)Peak memory usage: 85 MB % 5.30/1.82 % (4035167)Instructions burned: 4 (million) % 5.30/1.82 % (4035164)lrs+10_1_thi=all:si=on:fd=off:random_seed=1635299660:i=53:rtra=on:gtg=all_2992 on theBenchmark for (2992ds/53Mi) % 5.30/1.82 % (4035161)Instruction limit reached! % 5.30/1.82 % (4035161)------------------------------ % 5.30/1.82 % (4035161)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.30/1.82 % (4035161)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.30/1.82 % (4035161)CaDiCaL version: 2.1.3 % 5.30/1.82 % (4035161)Termination reason: Instruction limit % 5.30/1.82 % (4035161)Termination phase: Property scanning % 5.30/1.82 % (4035161)Time elapsed: 0.027 s % 5.30/1.82 % (4035161)Peak memory usage: 85 MB % 5.30/1.82 % (4035161)Instructions burned: 69 (million) % 5.30/1.82 % (4035164)Instruction limit reached! % 5.30/1.82 % (4035164)------------------------------ % 6.27/1.99 % (4035164)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.27/1.99 % (4035164)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.27/1.99 % (4035164)CaDiCaL version: 2.1.3 % 6.27/1.99 % (4035164)Termination reason: Instruction limit % 6.27/1.99 % (4035164)Termination phase: Property scanning % 6.27/1.99 % (4035164)Time elapsed: 0.020 s % 6.27/1.99 % (4035164)Peak memory usage: 85 MB % 6.27/1.99 % (4035164)Instructions burned: 54 (million) % 6.27/1.99 % (4035166)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=3630323260:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2992 on theBenchmark for (2992ds/8Mi) % 6.27/1.99 % (4035166)Instruction limit reached! % 6.27/1.99 % (4035166)------------------------------ % 6.27/1.99 % (4035166)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.27/1.99 % (4035166)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.27/1.99 % (4035166)CaDiCaL version: 2.1.3 % 6.27/1.99 % (4035166)Termination reason: Instruction limit % 6.27/1.99 % (4035166)Termination phase: Property scanning % 6.27/1.99 % (4035166)Time elapsed: 0.004 s % 6.27/1.99 % (4035166)Peak memory usage: 85 MB % 6.27/1.99 % (4035166)Instructions burned: 9 (million) % 6.27/1.99 % (4035159)Refutation not found, incomplete strategy % 6.27/1.99 % (4035159)------------------------------ % 6.27/1.99 % (4035159)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.27/1.99 % (4035159)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.27/1.99 % (4035159)CaDiCaL version: 2.1.3 % 6.27/1.99 % (4035159)Termination reason: Refutation not found, incomplete strategy % 6.27/1.99 % (4035159)Time elapsed: 0.064 s % 6.27/1.99 % (4035159)Peak memory usage: 88 MB % 6.27/1.99 % (4035159)Instructions burned: 174 (million) % 6.27/1.99 % (4035169)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=978366635:i=2:doe=on:canc=force:asg=cautious:rtra=on_2992 on theBenchmark for (2992ds/2Mi) % 6.27/1.99 % (4035169)Instruction limit reached! % 6.27/1.99 % (4035169)------------------------------ % 6.27/1.99 % (4035169)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.27/1.99 % (4035169)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.27/1.99 % (4035169)CaDiCaL version: 2.1.3 % 6.27/1.99 % (4035169)Termination reason: Instruction limit % 6.27/1.99 % (4035169)Termination phase: shuffling % 6.27/1.99 % (4035169)Time elapsed: 0.002 s % 6.27/1.99 % (4035169)Peak memory usage: 85 MB % 6.27/1.99 % (4035169)Instructions burned: 4 (million) % 6.27/1.99 % (4035175)dis+10_1_si=on:random_seed=941234101:i=10:ep=R:rtra=on_2991 on theBenchmark for (2991ds/10Mi) % 6.27/1.99 % (4035175)Instruction limit reached! % 6.27/1.99 % (4035175)------------------------------ % 6.27/1.99 % (4035175)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.27/1.99 % (4035175)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.27/1.99 % (4035175)CaDiCaL version: 2.1.3 % 6.27/1.99 % (4035175)Termination reason: Instruction limit % 6.27/1.99 % (4035175)Termination phase: shuffling % 6.27/1.99 % (4035175)Time elapsed: 0.003 s % 6.27/1.99 % (4035175)Peak memory usage: 85 MB % 6.27/1.99 % (4035175)Instructions burned: 13 (million) % 6.27/1.99 % (4035174)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=3669128832:i=127:doe=on:rtra=on_2991 on theBenchmark for (2991ds/127Mi) % 6.27/1.99 % (4035177)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=1930531430:i=26:canc=cautious:av=off:rtra=on_2991 on theBenchmark for (2991ds/26Mi) % 6.27/1.99 % (4035178)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=370288132: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) % 6.27/1.99 % (4035177)Instruction limit reached! % 6.27/1.99 % (4035177)------------------------------ % 6.27/1.99 % (4035177)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.27/1.99 % (4035177)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.27/1.99 % (4035177)CaDiCaL version: 2.1.3 % 6.27/1.99 % (4035177)Termination reason: Instruction limit % 6.27/1.99 % (4035177)Termination phase: Property scanning % 6.27/1.99 % (4035177)Time elapsed: 0.012 s % 6.27/1.99 % (4035177)Peak memory usage: 85 MB % 8.05/2.14 % (4035177)Instructions burned: 28 (million) % 8.05/2.14 % (4035178)Instruction limit reached! % 8.05/2.14 % (4035178)------------------------------ % 8.05/2.14 % (4035178)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.05/2.14 % (4035178)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.05/2.14 % (4035178)CaDiCaL version: 2.1.3 % 8.05/2.14 % (4035178)Termination reason: Instruction limit % 8.05/2.14 % (4035178)Termination phase: Property scanning % 8.05/2.14 % (4035178)Time elapsed: 0.015 s % 8.05/2.14 % (4035178)Peak memory usage: 85 MB % 8.05/2.14 % (4035178)Instructions burned: 38 (million) % 8.05/2.14 % (4035180)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=3615954609:i=2:fsr=off:rtra=on:inst=on_2991 on theBenchmark for (2991ds/2Mi) % 8.05/2.14 % (4035174)Instruction limit reached! % 8.05/2.14 % (4035174)------------------------------ % 8.05/2.14 % (4035174)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.05/2.14 % (4035174)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.05/2.14 % (4035174)CaDiCaL version: 2.1.3 % 8.05/2.14 % (4035174)Termination reason: Instruction limit % 8.05/2.14 % (4035174)Termination phase: Property scanning % 8.05/2.14 % (4035174)Time elapsed: 0.049 s % 8.05/2.14 % (4035174)Peak memory usage: 86 MB % 8.05/2.14 % (4035174)Instructions burned: 129 (million) % 8.05/2.14 % (4035180)Instruction limit reached! % 8.05/2.14 % (4035180)------------------------------ % 8.05/2.14 % (4035180)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.05/2.14 % (4035180)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.05/2.14 % (4035180)CaDiCaL version: 2.1.3 % 8.05/2.14 % (4035180)Termination reason: Instruction limit % 8.05/2.14 % (4035180)Termination phase: shuffling % 8.05/2.14 % (4035180)Time elapsed: 0.002 s % 8.05/2.14 % (4035180)Peak memory usage: 85 MB % 8.05/2.14 % (4035180)Instructions burned: 4 (million) % 8.05/2.14 % (4035184)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=3718451280:i=370:ep=RS:fsr=off:rtra=on_2990 on theBenchmark for (2990ds/370Mi) % 8.05/2.14 % (4035182)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=161013653:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2990 on theBenchmark for (2990ds/8Mi) % 8.05/2.14 % (4035182)Instruction limit reached! % 8.05/2.14 % (4035182)------------------------------ % 8.05/2.14 % (4035182)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.05/2.14 % (4035182)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.05/2.14 % (4035182)CaDiCaL version: 2.1.3 % 8.05/2.14 % (4035182)Termination reason: Instruction limit % 8.05/2.14 % (4035182)Termination phase: shuffling % 8.05/2.14 % (4035182)Time elapsed: 0.004 s % 8.05/2.14 % (4035182)Peak memory usage: 85 MB % 8.05/2.14 % (4035182)Instructions burned: 9 (million) % 8.05/2.14 % (4035184)Instruction limit reached! % 8.05/2.14 % (4035184)------------------------------ % 8.05/2.14 % (4035184)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.05/2.14 % (4035184)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.05/2.14 % (4035184)CaDiCaL version: 2.1.3 % 8.05/2.14 % (4035184)Termination reason: Instruction limit % 8.05/2.14 % (4035184)Termination phase: Saturation % 8.05/2.14 % (4035184)Time elapsed: 0.071 s % 8.05/2.14 % (4035184)Peak memory usage: 88 MB % 8.05/2.14 % (4035184)Instructions burned: 372 (million) % 8.05/2.14 % (4035159)------------------------------ % 8.05/2.14 % (4035159)------------------------------ % 8.05/2.14 % (4035189)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=2981436712:i=226:rtra=on:gtg=position:ss=axioms_2989 on theBenchmark for (2989ds/226Mi) % 8.05/2.14 % (4035188)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=1520800617:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2989 on theBenchmark for (2989ds/13Mi) % 8.05/2.14 % (4035188)Instruction limit reached! % 8.05/2.14 % (4035188)------------------------------ % 8.05/2.14 % (4035188)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.05/2.14 % (4035188)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.05/2.14 % (4035188)CaDiCaL version: 2.1.3 % 8.05/2.14 % (4035188)Termination reason: Instruction limit % 8.05/2.14 % (4035188)Termination phase: Property scanning % 8.05/2.14 % (4035188)Time elapsed: 0.006 s % 8.05/2.14 % (4035188)Peak memory usage: 85 MB % 9.26/2.35 % (4035188)Instructions burned: 15 (million) % 9.26/2.35 % (4035192)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=1314193882:i=71:rtra=on:gtg=exists_top_2989 on theBenchmark for (2989ds/71Mi) % 9.26/2.35 % (4035191)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=2051088062:i=10:rtra=on_2989 on theBenchmark for (2989ds/10Mi) % 9.26/2.35 % (4035191)Instruction limit reached! % 9.26/2.35 % (4035191)------------------------------ % 9.26/2.35 % (4035191)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.26/2.35 % (4035191)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.26/2.35 % (4035191)CaDiCaL version: 2.1.3 % 9.26/2.35 % (4035191)Termination reason: Instruction limit % 9.26/2.35 % (4035191)Termination phase: shuffling % 9.26/2.35 % (4035191)Time elapsed: 0.005 s % 9.26/2.35 % (4035191)Peak memory usage: 85 MB % 9.26/2.35 % (4035191)Instructions burned: 12 (million) % 9.26/2.35 % (4035192)Instruction limit reached! % 9.26/2.35 % (4035192)------------------------------ % 9.26/2.35 % (4035192)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.26/2.35 % (4035192)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.26/2.35 % (4035192)CaDiCaL version: 2.1.3 % 9.26/2.35 % (4035192)Termination reason: Instruction limit % 9.26/2.35 % (4035192)Termination phase: Property scanning % 9.26/2.35 % (4035192)Time elapsed: 0.027 s % 9.26/2.35 % (4035192)Peak memory usage: 85 MB % 9.26/2.35 % (4035192)Instructions burned: 72 (million) % 9.26/2.35 % (4035196)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=2176432162:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2988 on theBenchmark for (2988ds/294Mi) % 9.26/2.35 % (4035195)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=3377466576:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2989 on theBenchmark for (2989ds/75Mi) % 9.26/2.35 % (4035189)Instruction limit reached! % 9.26/2.35 % (4035189)------------------------------ % 9.26/2.35 % (4035189)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.26/2.35 % (4035189)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.26/2.35 % (4035189)CaDiCaL version: 2.1.3 % 9.26/2.35 % (4035189)Termination reason: Instruction limit % 9.26/2.35 % (4035189)Termination phase: Property scanning % 9.26/2.35 % (4035189)Time elapsed: 0.084 s % 9.26/2.35 % (4035189)Peak memory usage: 85 MB % 9.26/2.35 % (4035189)Instructions burned: 227 (million) % 9.26/2.35 % (4035195)Instruction limit reached! % 9.26/2.35 % (4035195)------------------------------ % 9.26/2.35 % (4035195)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.26/2.35 % (4035195)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.26/2.35 % (4035195)CaDiCaL version: 2.1.3 % 9.26/2.35 % (4035195)Termination reason: Instruction limit % 9.26/2.35 % (4035195)Termination phase: Property scanning % 9.26/2.35 % (4035195)Time elapsed: 0.029 s % 9.26/2.35 % (4035195)Peak memory usage: 86 MB % 9.26/2.35 % (4035195)Instructions burned: 76 (million) % 9.26/2.35 % (4035196)Instruction limit reached! % 9.26/2.35 % (4035196)------------------------------ % 9.26/2.35 % (4035196)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.26/2.35 % (4035196)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.26/2.35 % (4035196)CaDiCaL version: 2.1.3 % 9.26/2.35 % (4035196)Termination reason: Instruction limit % 9.26/2.35 % (4035196)Termination phase: Property scanning % 9.26/2.35 % (4035196)Time elapsed: 0.058 s % 9.26/2.35 % (4035196)Peak memory usage: 86 MB % 9.26/2.35 % (4035196)Instructions burned: 298 (million) % 9.26/2.35 % (4035197)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=4125357719:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2988 on theBenchmark for (2988ds/130Mi) % 9.26/2.35 % (4035200)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=3415173870:i=131:rtra=on_2988 on theBenchmark for (2988ds/131Mi) % 9.26/2.35 % (4035203)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=1537564323:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2988 on theBenchmark for (2988ds/40Mi) % 9.26/2.35 % (4035197)Instruction limit reached! % 9.26/2.35 % (4035197)------------------------------ % 9.26/2.35 % (4035197)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.20/2.54 % (4035197)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.20/2.54 % (4035197)CaDiCaL version: 2.1.3 % 10.20/2.54 % (4035197)Termination reason: Instruction limit % 10.20/2.54 % (4035197)Termination phase: Property scanning % 10.20/2.54 % (4035197)Time elapsed: 0.050 s % 10.20/2.54 % (4035197)Peak memory usage: 85 MB % 10.20/2.54 % (4035197)Instructions burned: 131 (million) % 10.20/2.54 % (4035203)Instruction limit reached! % 10.20/2.54 % (4035203)------------------------------ % 10.20/2.54 % (4035203)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.20/2.54 % (4035203)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.20/2.54 % (4035203)CaDiCaL version: 2.1.3 % 10.20/2.54 % (4035203)Termination reason: Instruction limit % 10.20/2.54 % (4035203)Termination phase: Property scanning % 10.20/2.54 % (4035203)Time elapsed: 0.016 s % 10.20/2.54 % (4035203)Peak memory usage: 85 MB % 10.20/2.54 % (4035203)Instructions burned: 42 (million) % 10.20/2.54 % (4035204)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=2693291386:i=307:rtra=on:gtg=exists_top_2987 on theBenchmark for (2987ds/307Mi) % 10.20/2.54 % (4035200)Instruction limit reached! % 10.20/2.54 % (4035200)------------------------------ % 10.20/2.54 % (4035200)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.20/2.54 % (4035200)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.20/2.54 % (4035200)CaDiCaL version: 2.1.3 % 10.20/2.54 % (4035200)Termination reason: Instruction limit % 10.20/2.54 % (4035200)Termination phase: Property scanning % 10.20/2.54 % (4035200)Time elapsed: 0.050 s % 10.20/2.54 % (4035200)Peak memory usage: 86 MB % 10.20/2.54 % (4035200)Instructions burned: 133 (million) % 10.20/2.54 % (4035207)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=977099454:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2987 on theBenchmark for (2987ds/598Mi) % 10.20/2.54 % (4035210)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=3370326895:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2987 on theBenchmark for (2987ds/259Mi) % 10.20/2.54 % (4035208)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=786714129:i=131:canc=cautious:fsr=off:rtra=on_2987 on theBenchmark for (2987ds/131Mi) % 10.20/2.54 % (4035210)Instruction limit reached! % 10.20/2.54 % (4035210)------------------------------ % 10.20/2.54 % (4035210)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.20/2.54 % (4035210)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.20/2.54 % (4035210)CaDiCaL version: 2.1.3 % 10.20/2.54 % (4035210)Termination reason: Instruction limit % 10.20/2.54 % (4035210)Termination phase: SInE selection % 10.20/2.54 % (4035210)Time elapsed: 0.051 s % 10.20/2.54 % (4035210)Peak memory usage: 86 MB % 10.20/2.54 % (4035210)Instructions burned: 261 (million) % 10.20/2.54 % (4035208)Instruction limit reached! % 10.20/2.54 % (4035208)------------------------------ % 10.20/2.54 % (4035208)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.20/2.54 % (4035208)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.20/2.54 % (4035208)CaDiCaL version: 2.1.3 % 10.20/2.54 % (4035208)Termination reason: Instruction limit % 10.20/2.54 % (4035208)Termination phase: Property scanning % 10.20/2.54 % (4035208)Time elapsed: 0.050 s % 10.20/2.54 % (4035208)Peak memory usage: 86 MB % 10.20/2.54 % (4035208)Instructions burned: 133 (million) % 10.20/2.54 % (4035213)dis+10_1_si=on:random_seed=2290415082:s2a=on:i=1000:rtra=on:gtg=exists_all_2986 on theBenchmark for (2986ds/1000Mi) % 10.20/2.54 % (4035204)Instruction limit reached! % 10.20/2.54 % (4035204)------------------------------ % 10.20/2.54 % (4035204)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.20/2.54 % (4035204)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.20/2.54 % (4035204)CaDiCaL version: 2.1.3 % 10.20/2.54 % (4035204)Termination reason: Instruction limit % 10.20/2.54 % (4035204)Termination phase: Property scanning % 10.20/2.54 % (4035204)Time elapsed: 0.114 s % 10.20/2.54 % (4035204)Peak memory usage: 86 MB % 10.20/2.54 % (4035204)Instructions burned: 308 (million) % 10.20/2.54 % (4035215)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=3329922251:i=383:fsr=off:rtra=on:ev=force_2986 on theBenchmark for (2986ds/383Mi) % 12.23/2.83 % (4035216)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=2039746488:i=141:doe=on:rtra=on_2986 on theBenchmark for (2986ds/141Mi) % 12.23/2.83 % (4035220)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=1694269870:i=65:nm=16:rtra=on_2985 on theBenchmark for (2985ds/65Mi) % 12.23/2.83 % (4035216)Instruction limit reached! % 12.23/2.83 % (4035216)------------------------------ % 12.23/2.83 % (4035216)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.23/2.83 % (4035216)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.23/2.83 % (4035216)CaDiCaL version: 2.1.3 % 12.23/2.83 % (4035216)Termination reason: Instruction limit % 12.23/2.83 % (4035216)Termination phase: Property scanning % 12.23/2.83 % (4035216)Time elapsed: 0.053 s % 12.23/2.83 % (4035216)Peak memory usage: 86 MB % 12.23/2.83 % (4035216)Instructions burned: 142 (million) % 12.23/2.83 % (4035220)Instruction limit reached! % 12.23/2.83 % (4035220)------------------------------ % 12.23/2.83 % (4035220)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.23/2.83 % (4035220)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.23/2.83 % (4035220)CaDiCaL version: 2.1.3 % 12.23/2.83 % (4035220)Termination reason: Instruction limit % 12.23/2.83 % (4035220)Termination phase: Property scanning % 12.23/2.83 % (4035220)Time elapsed: 0.014 s % 12.23/2.83 % (4035220)Peak memory usage: 86 MB % 12.23/2.83 % (4035220)Instructions burned: 68 (million) % 12.23/2.83 % (4035221)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=3621581513:i=121:nm=16:rtra=on_2985 on theBenchmark for (2985ds/121Mi) % 12.23/2.83 % (4035223)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=4008164640:s2a=on:i=128:s2at=5:ins=3:rtra=on_2985 on theBenchmark for (2985ds/128Mi) % 12.23/2.83 % (4035215)Instruction limit reached! % 12.23/2.83 % (4035215)------------------------------ % 12.23/2.83 % (4035215)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.23/2.83 % (4035215)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.23/2.83 % (4035215)CaDiCaL version: 2.1.3 % 12.23/2.83 % (4035215)Termination reason: Instruction limit % 12.23/2.83 % (4035215)Termination phase: Saturation % 12.23/2.83 % (4035215)Time elapsed: 0.141 s % 12.23/2.83 % (4035215)Peak memory usage: 88 MB % 12.23/2.83 % (4035215)Instructions burned: 384 (million) % 12.23/2.83 % (4035221)Instruction limit reached! % 12.23/2.83 % (4035221)------------------------------ % 12.23/2.83 % (4035221)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.23/2.83 % (4035221)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.23/2.83 % (4035221)CaDiCaL version: 2.1.3 % 12.23/2.83 % (4035221)Termination reason: Instruction limit % 12.23/2.83 % (4035221)Termination phase: Property scanning % 12.23/2.83 % (4035221)Time elapsed: 0.046 s % 12.23/2.83 % (4035221)Peak memory usage: 86 MB % 12.23/2.83 % (4035221)Instructions burned: 123 (million) % 12.23/2.83 % (4035207)Instruction limit reached! % 12.23/2.83 % (4035207)------------------------------ % 12.23/2.83 % (4035207)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.23/2.83 % (4035207)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.23/2.83 % (4035207)CaDiCaL version: 2.1.3 % 12.23/2.83 % (4035207)Termination reason: Instruction limit % 12.23/2.83 % (4035207)Termination phase: Saturation % 12.23/2.83 % (4035207)Time elapsed: 0.274 s % 12.23/2.83 % (4035207)Peak memory usage: 131 MB % 12.23/2.83 % (4035207)Instructions burned: 598 (million) % 12.23/2.83 % (4035228)dis+1010_1_to=kbo:si=on:random_seed=3423363099:i=175:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2984 on theBenchmark for (2984ds/175Mi) % 12.23/2.83 % (4035223)Instruction limit reached! % 12.23/2.83 % (4035223)------------------------------ % 12.23/2.83 % (4035223)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.23/2.83 % (4035223)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.23/2.83 % (4035223)CaDiCaL version: 2.1.3 % 12.23/2.83 % (4035223)Termination reason: Instruction limit % 12.23/2.83 % (4035223)Termination phase: Property scanning % 12.23/2.83 % (4035223)Time elapsed: 0.049 s % 12.23/2.83 % (4035223)Peak memory usage: 86 MB % 12.23/2.83 % (4035223)Instructions burned: 128 (million) % 12.23/2.83 % (4035227)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=3808207068:i=39:ins=3:rtra=on_2984 on theBenchmark for (2984ds/39Mi) % 14.88/3.05 % (4035228)Instruction limit reached! % 14.88/3.05 % (4035228)------------------------------ % 14.88/3.05 % (4035228)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.88/3.05 % (4035228)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.88/3.05 % (4035228)CaDiCaL version: 2.1.3 % 14.88/3.05 % (4035228)Termination reason: Instruction limit % 14.88/3.05 % (4035228)Termination phase: Property scanning % 14.88/3.05 % (4035228)Time elapsed: 0.034 s % 14.88/3.05 % (4035228)Peak memory usage: 85 MB % 14.88/3.05 % (4035228)Instructions burned: 178 (million) % 14.88/3.05 % (4035227)Instruction limit reached! % 14.88/3.05 % (4035227)------------------------------ % 14.88/3.05 % (4035227)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.88/3.05 % (4035227)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.88/3.05 % (4035227)CaDiCaL version: 2.1.3 % 14.88/3.05 % (4035227)Termination reason: Instruction limit % 14.88/3.05 % (4035227)Termination phase: Property scanning % 14.88/3.05 % (4035227)Time elapsed: 0.017 s % 14.88/3.05 % (4035227)Peak memory usage: 86 MB % 14.88/3.05 % (4035227)Instructions burned: 41 (million) % 14.88/3.05 % (4035231)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=3385325016:i=329:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2983 on theBenchmark for (2983ds/329Mi) % 14.88/3.05 % (4035232)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=132550045:s2a=on:i=483:doe=on:nm=32:rtra=on_2983 on theBenchmark for (2983ds/483Mi) % 14.88/3.05 % (4035237)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=2460683785:st=2:i=295:rtra=on:ss=axioms_2983 on theBenchmark for (2983ds/295Mi) % 14.88/3.05 % (4035235)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=2908633500:i=349:rtra=on_2983 on theBenchmark for (2983ds/349Mi) % 14.88/3.05 % (4035234)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=178063954:thitd=on:i=215:nm=0:rtra=on:ev=force_2983 on theBenchmark for (2983ds/215Mi) % 14.88/3.05 % (4035213)Instruction limit reached! % 14.88/3.05 % (4035213)------------------------------ % 14.88/3.05 % (4035213)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.88/3.05 % (4035213)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.88/3.05 % (4035213)CaDiCaL version: 2.1.3 % 14.88/3.05 % (4035213)Termination reason: Instruction limit % 14.88/3.05 % (4035213)Termination phase: Saturation % 14.88/3.05 % (4035213)Time elapsed: 0.375 s % 14.88/3.05 % (4035213)Peak memory usage: 89 MB % 14.88/3.05 % (4035213)Instructions burned: 1000 (million) % 14.88/3.05 % (4035237)Refutation not found, incomplete strategy % 14.88/3.05 % (4035237)------------------------------ % 14.88/3.05 % (4035237)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.88/3.05 % (4035237)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.88/3.05 % (4035237)CaDiCaL version: 2.1.3 % 14.88/3.05 % (4035237)Termination reason: Refutation not found, incomplete strategy % 14.88/3.05 % (4035237)Time elapsed: 0.055 s % 14.88/3.05 % (4035237)Peak memory usage: 88 MB % 14.88/3.05 % (4035237)Instructions burned: 289 (million) % 14.88/3.05 % (4035238)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=867056021:i=328:kws=inv_frequency:nm=20:rtra=on_2982 on theBenchmark for (2982ds/328Mi) % 14.88/3.05 % (4035234)Instruction limit reached! % 14.88/3.05 % (4035234)------------------------------ % 14.88/3.05 % (4035234)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.88/3.05 % (4035234)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.88/3.05 % (4035234)CaDiCaL version: 2.1.3 % 14.88/3.05 % (4035234)Termination reason: Instruction limit % 14.88/3.05 % (4035234)Termination phase: Property scanning % 14.88/3.05 % (4035234)Time elapsed: 0.079 s % 14.88/3.05 % (4035234)Peak memory usage: 86 MB % 14.88/3.05 % (4035234)Instructions burned: 218 (million) % 14.88/3.05 % (4035231)Instruction limit reached! % 14.88/3.05 % (4035231)------------------------------ % 14.88/3.05 % (4035231)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.88/3.05 % (4035231)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.88/3.05 % (4035231)CaDiCaL version: 2.1.3 % 15.46/3.32 % (4035231)Termination reason: Instruction limit % 15.46/3.32 % (4035231)Termination phase: Property scanning % 15.46/3.32 % (4035231)Time elapsed: 0.122 s % 15.46/3.32 % (4035231)Peak memory usage: 86 MB % 15.46/3.32 % (4035231)Instructions burned: 330 (million) % 15.46/3.32 % (4035235)Instruction limit reached! % 15.46/3.32 % (4035235)------------------------------ % 15.46/3.32 % (4035235)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.46/3.32 % (4035235)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.46/3.32 % (4035235)CaDiCaL version: 2.1.3 % 15.46/3.32 % (4035235)Termination reason: Instruction limit % 15.46/3.32 % (4035235)Termination phase: Saturation % 15.46/3.32 % (4035235)Time elapsed: 0.149 s % 15.46/3.32 % (4035235)Peak memory usage: 112 MB % 15.46/3.32 % (4035235)Instructions burned: 349 (million) % 15.46/3.32 % (4035238)Instruction limit reached! % 15.46/3.32 % (4035238)------------------------------ % 15.46/3.32 % (4035238)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.46/3.32 % (4035238)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.46/3.32 % (4035238)CaDiCaL version: 2.1.3 % 15.46/3.32 % (4035238)Termination reason: Instruction limit % 15.46/3.32 % (4035238)Termination phase: Property scanning % 15.46/3.32 % (4035238)Time elapsed: 0.121 s % 15.46/3.32 % (4035238)Peak memory usage: 86 MB % 15.46/3.32 % (4035238)Instructions burned: 328 (million) % 15.46/3.32 % (4035244)dis+1010_1_to=lpo:sil=128000:sas=z3:si=on:nwc=5:random_seed=115283064:i=281:gtgl=2:rtra=on:gtg=all_2981 on theBenchmark for (2981ds/281Mi) % 15.46/3.32 % (4035237)------------------------------ % 15.46/3.32 % (4035237)------------------------------ % 15.46/3.32 % (4035232)Instruction limit reached! % 15.46/3.32 % (4035232)------------------------------ % 15.46/3.32 % (4035232)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.46/3.32 % (4035232)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.46/3.32 % (4035232)CaDiCaL version: 2.1.3 % 15.46/3.32 % (4035232)Termination reason: Instruction limit % 15.46/3.32 % (4035232)Termination phase: Saturation % 15.46/3.32 % (4035232)Time elapsed: 0.227 s % 15.46/3.32 % (4035232)Peak memory usage: 129 MB % 15.46/3.32 % (4035232)Instructions burned: 485 (million) % 15.46/3.32 % (4035246)lrs+1010_1_to=kbo:sil=128000:si=on:sos=on:urr=on:uwa=alasca_main:random_seed=3200069198:i=484:doe=on:nm=0:av=off:rtra=on:ss=axioms_2981 on theBenchmark for (2981ds/484Mi) % 15.46/3.32 % (4035247)lrs+21_1_to=kbo:sil=128000:thi=neg_eq:si=on:random_seed=472625793:i=321:canc=force:rtra=on:tac=axiom:ss=axioms:ev=force_2981 on theBenchmark for (2981ds/321Mi) % 15.46/3.32 % (4035248)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=961772970:i=416:rtra=on:gtg=position:ss=axioms_2980 on theBenchmark for (2980ds/416Mi) % 15.46/3.32 % (4035244)Instruction limit reached! % 15.46/3.32 % (4035244)------------------------------ % 15.46/3.32 % (4035244)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.46/3.32 % (4035244)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.46/3.32 % (4035244)CaDiCaL version: 2.1.3 % 15.46/3.32 % (4035244)Termination reason: Instruction limit % 15.46/3.32 % (4035244)Termination phase: Property scanning % 15.46/3.32 % (4035244)Time elapsed: 0.105 s % 15.46/3.32 % (4035244)Peak memory usage: 86 MB % 15.46/3.32 % (4035244)Instructions burned: 282 (million) % 15.46/3.32 % (4035251)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=2758587401:avsq=on:i=276:avsqr=1,2:rtra=on_2979 on theBenchmark for (2979ds/276Mi) % 15.46/3.32 % (4035250)lrs+1010_1_to=kbo:tgt=ground:fde=unused:sas=z3:si=on:sp=unary_frequency:gve=force:spb=goal:tha=off:random_seed=3846690264:i=471:thf=on:kws=precedence:rtra=on_2980 on theBenchmark for (2980ds/471Mi) % 15.46/3.32 % (4035246)Refutation not found, incomplete strategy % 15.46/3.32 % (4035246)------------------------------ % 15.46/3.32 % (4035246)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.46/3.32 % (4035246)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.46/3.32 % (4035246)CaDiCaL version: 2.1.3 % 15.46/3.32 % (4035246)Termination reason: Refutation not found, incomplete strategy % 15.46/3.32 % (4035246)Time elapsed: 0.102 s % 15.46/3.32 % (4035246)Peak memory usage: 88 MB % 15.46/3.32 % (4035246)Instructions burned: 282 (million) % 15.46/3.32 % (4035251)Instruction limit reached! % 15.46/3.32 % (4035251)------------------------------ % 17.58/3.60 % (4035251)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.58/3.60 % (4035251)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.58/3.60 % (4035251)CaDiCaL version: 2.1.3 % 17.58/3.60 % (4035251)Termination reason: Instruction limit % 17.58/3.60 % (4035251)Termination phase: Property scanning % 17.58/3.60 % (4035251)Time elapsed: 0.053 s % 17.58/3.60 % (4035251)Peak memory usage: 86 MB % 17.58/3.60 % (4035251)Instructions burned: 277 (million) % 17.58/3.60 % (4035253)lrs+1010_2_to=kbo:sil=128000:tgt=ground:fde=unused:sas=z3:si=on:uwa=off:tha=off:nwc=1:random_seed=2472700329:i=375:kws=inv_arity_squared:rtra=on_2979 on theBenchmark for (2979ds/375Mi) % 17.58/3.60 % (4035247)Refutation not found, incomplete strategy % 17.58/3.60 % (4035247)------------------------------ % 17.58/3.60 % (4035247)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.58/3.60 % (4035247)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.58/3.60 % (4035247)CaDiCaL version: 2.1.3 % 17.58/3.60 % (4035247)Termination reason: Refutation not found, incomplete strategy % 17.58/3.60 % (4035247)Time elapsed: 0.129 s % 17.58/3.60 % (4035247)Peak memory usage: 112 MB % 17.58/3.60 % (4035247)Instructions burned: 287 (million) % 17.58/3.60 % (4035248)Refutation not found, incomplete strategy % 17.58/3.60 % (4035248)------------------------------ % 17.58/3.60 % (4035248)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.58/3.60 % (4035248)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.58/3.60 % (4035248)CaDiCaL version: 2.1.3 % 17.58/3.60 % (4035248)Termination reason: Refutation not found, incomplete strategy % 17.58/3.60 % (4035248)Time elapsed: 0.126 s % 17.58/3.60 % (4035248)Peak memory usage: 112 MB % 17.58/3.60 % (4035248)Instructions burned: 286 (million) % 17.58/3.60 % (4035256)lrs+10_1_to=kbo:sil=128000:tgt=full:sas=z3:si=on:uwa=func_ext:slsqc=1:flr=on:slsq=on:random_seed=1427113424:i=387:bd=preordered:rtra=on:ss=axioms:sgt=8_2979 on theBenchmark for (2979ds/387Mi) % 17.58/3.60 % (4035260)lrs+10_1_to=kbo:sil=128000:fde=none:si=on:norm_ineq=on:urr=on:nwc=0.5:random_seed=3919511670:i=513:kws=frequency:bd=all:rtra=on:gtg=exists_all:ss=axioms:sgt=4_2978 on theBenchmark for (2978ds/513Mi) % 17.58/3.60 % (4035250)Instruction limit reached! % 17.58/3.60 % (4035250)------------------------------ % 17.58/3.60 % (4035250)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.58/3.60 % (4035250)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.58/3.60 % (4035250)CaDiCaL version: 2.1.3 % 17.58/3.60 % (4035250)Termination reason: Instruction limit % 17.58/3.60 % (4035250)Termination phase: Saturation % 17.58/3.60 % (4035250)Time elapsed: 0.202 s % 17.58/3.60 % (4035250)Peak memory usage: 114 MB % 17.58/3.60 % (4035250)Instructions burned: 472 (million) % 17.58/3.60 % (4035253)Instruction limit reached! % 17.58/3.60 % (4035253)------------------------------ % 17.58/3.60 % (4035253)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.58/3.60 % (4035253)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.58/3.60 % (4035253)CaDiCaL version: 2.1.3 % 17.58/3.60 % (4035253)Termination reason: Instruction limit % 17.58/3.60 % (4035253)Termination phase: Saturation % 17.58/3.60 % (4035253)Time elapsed: 0.161 s % 17.58/3.60 % (4035253)Peak memory usage: 112 MB % 17.58/3.60 % (4035253)Instructions burned: 377 (million) % 17.58/3.60 % (4035246)------------------------------ % 17.58/3.60 % (4035246)------------------------------ % 17.58/3.60 % (4035256)Refutation not found, incomplete strategy % 17.58/3.60 % (4035256)------------------------------ % 17.58/3.60 % (4035256)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.58/3.60 % (4035256)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.58/3.60 % (4035256)CaDiCaL version: 2.1.3 % 17.58/3.60 % (4035256)Termination reason: Refutation not found, incomplete strategy % 17.58/3.60 % (4035256)Time elapsed: 0.132 s % 17.58/3.60 % (4035256)Peak memory usage: 112 MB % 17.58/3.60 % (4035256)Instructions burned: 302 (million) % 17.58/3.60 % (4035260)Instruction limit reached! % 17.58/3.60 % (4035260)------------------------------ % 17.58/3.60 % (4035260)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.58/3.60 % (4035260)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.58/3.60 % (4035260)CaDiCaL version: 2.1.3 % 17.58/3.60 % (4035260)Termination reason: Instruction limit % 19.75/3.95 % (4035260)Termination phase: Property scanning % 19.75/3.95 % (4035260)Time elapsed: 0.098 s % 19.75/3.95 % (4035260)Peak memory usage: 86 MB % 19.75/3.95 % (4035260)Instructions burned: 514 (million) % 19.75/3.95 % (4035247)------------------------------ % 19.75/3.95 % (4035247)------------------------------ % 19.75/3.95 % (4035248)------------------------------ % 19.75/3.95 % (4035248)------------------------------ % 19.75/3.95 % (4035263)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=2597793090:i=334:rtra=on_2976 on theBenchmark for (2976ds/334Mi) % 19.75/3.95 % (4035264)lrs+1010_1_to=kbo:sil=64000:sas=cadical:si=on:sos=on:bce=on:random_seed=3166263753:i=359:rtra=on:gtg=exists_top:ss=axioms_2976 on theBenchmark for (2976ds/359Mi) % 19.75/3.95 % (4035266)lrs-2_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_max:tha=off:random_seed=2635943345:st=1.5:i=261:sd=1:kws=precedence:rtra=on:ss=axioms_2976 on theBenchmark for (2976ds/261Mi) % 19.75/3.95 % (4035265)dis+1010_1_to=lpo:sil=128000:thi=all:fde=unused:si=on:sp=reverse_arity:tha=off:random_seed=4283628821:i=341:gtgl=2:rtra=on:gtg=exists_sym:ev=force:fsd=on:fsdmm=1_2976 on theBenchmark for (2976ds/341Mi) % 19.75/3.95 % (4035266)Refutation not found, incomplete strategy % 19.75/3.95 % (4035266)------------------------------ % 19.75/3.95 % (4035266)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.75/3.95 % (4035266)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.75/3.95 % (4035266)CaDiCaL version: 2.1.3 % 19.75/3.95 % (4035266)Termination reason: Refutation not found, incomplete strategy % 19.75/3.95 % (4035266)Time elapsed: 0.051 s % 19.75/3.95 % (4035266)Peak memory usage: 112 MB % 19.75/3.95 % (4035266)Instructions burned: 193 (million) % 19.75/3.95 % (4035267)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=143427406:s2pl=no:i=235:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2975 on theBenchmark for (2975ds/235Mi) % 19.75/3.95 % (4035256)------------------------------ % 19.75/3.95 % (4035256)------------------------------ % 19.75/3.95 % (4035264)Instruction limit reached! % 19.75/3.95 % (4035264)------------------------------ % 19.75/3.95 % (4035264)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.75/3.95 % (4035264)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.75/3.95 % (4035264)CaDiCaL version: 2.1.3 % 19.75/3.95 % (4035264)Termination reason: Instruction limit % 19.75/3.95 % (4035264)Termination phase: SInE selection % 19.75/3.95 % (4035264)Time elapsed: 0.134 s % 19.75/3.95 % (4035264)Peak memory usage: 86 MB % 19.75/3.95 % (4035264)Instructions burned: 360 (million) % 19.75/3.95 % (4035268)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=2016448810:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2975 on theBenchmark for (2975ds/273Mi) % 19.75/3.95 % (4035263)Instruction limit reached! % 19.75/3.95 % (4035263)------------------------------ % 19.75/3.95 % (4035263)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.75/3.95 % (4035263)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.75/3.95 % (4035263)CaDiCaL version: 2.1.3 % 19.75/3.95 % (4035263)Termination reason: Instruction limit % 19.75/3.95 % (4035263)Termination phase: Saturation % 19.75/3.95 % (4035263)Time elapsed: 0.168 s % 19.75/3.95 % (4035263)Peak memory usage: 129 MB % 19.75/3.95 % (4035263)Instructions burned: 337 (million) % 19.75/3.95 % (4035265)Instruction limit reached! % 19.75/3.95 % (4035265)------------------------------ % 19.75/3.95 % (4035265)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.75/3.95 % (4035265)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.75/3.95 % (4035265)CaDiCaL version: 2.1.3 % 19.75/3.95 % (4035265)Termination reason: Instruction limit % 19.75/3.95 % (4035265)Termination phase: Property scanning % 19.75/3.95 % (4035265)Time elapsed: 0.127 s % 19.75/3.95 % (4035265)Peak memory usage: 86 MB % 19.75/3.95 % (4035265)Instructions burned: 343 (million) % 19.75/3.95 % (4035267)Instruction limit reached! % 19.75/3.95 % (4035267)------------------------------ % 19.75/3.95 % (4035267)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.75/3.95 % (4035267)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.75/3.95 % (4035267)CaDiCaL version: 2.1.3 % 19.75/3.95 % (4035267)Termination reason: Instruction limit % 19.75/3.95 % (4035267)Termination phase: SInE selection % 23.49/4.32 % (4035267)Time elapsed: 0.086 s % 23.49/4.32 % (4035267)Peak memory usage: 86 MB % 23.49/4.32 % (4035267)Instructions burned: 236 (million) % 23.49/4.32 % (4035266)------------------------------ % 23.49/4.32 % (4035266)------------------------------ % 23.49/4.32 % (4035268)Instruction limit reached! % 23.49/4.32 % (4035268)------------------------------ % 23.49/4.32 % (4035268)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.49/4.32 % (4035268)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.49/4.32 % (4035268)CaDiCaL version: 2.1.3 % 23.49/4.32 % (4035268)Termination reason: Instruction limit % 23.49/4.32 % (4035268)Termination phase: Property scanning % 23.49/4.32 % (4035268)Time elapsed: 0.102 s % 23.49/4.32 % (4035268)Peak memory usage: 86 MB % 23.49/4.32 % (4035268)Instructions burned: 274 (million) % 23.49/4.32 % (4035275)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=681331082:i=146:doe=on:rtra=on_2973 on theBenchmark for (2973ds/146Mi) % 23.49/4.32 % (4035276)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=2891407506:i=4428:doe=on:fsr=off:rtra=on_2973 on theBenchmark for (2973ds/4428Mi) % 23.49/4.32 % (4035278)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=2391593853:i=1052:rtra=on_2973 on theBenchmark for (2973ds/1052Mi) % 23.49/4.32 % (4035279)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=880595021:i=655:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2973 on theBenchmark for (2973ds/655Mi) % 23.49/4.32 % (4035277)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=4034931645:avsq=on:i=276:avsqr=1,2:rtra=on_2973 on theBenchmark for (2973ds/276Mi) % 23.49/4.32 % (4035280)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=3836356899:st=5:i=1054:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2972 on theBenchmark for (2972ds/1054Mi) % 23.49/4.32 % (4035275)Instruction limit reached! % 23.49/4.32 % (4035275)------------------------------ % 23.49/4.32 % (4035275)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.49/4.32 % (4035275)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.49/4.32 % (4035275)CaDiCaL version: 2.1.3 % 23.49/4.32 % (4035275)Termination reason: Instruction limit % 23.49/4.32 % (4035275)Termination phase: Property scanning % 23.49/4.32 % (4035275)Time elapsed: 0.055 s % 23.49/4.32 % (4035275)Peak memory usage: 86 MB % 23.49/4.32 % (4035275)Instructions burned: 147 (million) % 23.49/4.32 % (4035280)Refutation not found, incomplete strategy % 23.49/4.32 % (4035280)------------------------------ % 23.49/4.32 % (4035280)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.49/4.32 % (4035280)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.49/4.32 % (4035280)CaDiCaL version: 2.1.3 % 23.49/4.32 % (4035280)Termination reason: Refutation not found, incomplete strategy % 23.49/4.32 % (4035280)Time elapsed: 0.034 s % 23.49/4.32 % (4035280)Peak memory usage: 88 MB % 23.49/4.32 % (4035280)Instructions burned: 181 (million) % 23.49/4.32 % (4035281)lrs-1002_1_to=kbo:sas=z3:si=on:norm_ineq=on:sos=on:tha=some:random_seed=2546168366:i=107:rtra=on_2972 on theBenchmark for (2972ds/107Mi) % 23.49/4.32 % (4035277)Instruction limit reached! % 23.49/4.32 % (4035277)------------------------------ % 23.49/4.32 % (4035277)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.49/4.32 % (4035277)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.49/4.32 % (4035277)CaDiCaL version: 2.1.3 % 23.49/4.32 % (4035277)Termination reason: Instruction limit % 23.49/4.32 % (4035277)Termination phase: Property scanning % 23.49/4.32 % (4035277)Time elapsed: 0.102 s % 23.49/4.32 % (4035277)Peak memory usage: 86 MB % 23.49/4.32 % (4035277)Instructions burned: 277 (million) % 23.49/4.32 % (4035281)Instruction limit reached! % 23.49/4.32 % (4035281)------------------------------ % 23.49/4.32 % (4035281)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.49/4.32 % (4035281)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.49/4.32 % (4035281)CaDiCaL version: 2.1.3 % 23.49/4.32 % (4035281)Termination reason: Instruction limit % 23.49/4.32 % (4035281)Termination phase: Property scanning % 23.49/4.32 % (4035281)Time elapsed: 0.042 s % 23.49/4.32 % (4035281)Peak memory usage: 86 MB % 23.49/4.32 % (4035281)Instructions burned: 110 (million) % 24.46/4.62 % (4035288)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=4144586272:s2a=on:i=450:doe=on:nm=32:rtra=on_2971 on theBenchmark for (2971ds/450Mi) % 24.46/4.62 % (4035280)------------------------------ % 24.46/4.62 % (4035280)------------------------------ % 24.46/4.62 % (4035279)Instruction limit reached! % 24.46/4.62 % (4035279)------------------------------ % 24.46/4.62 % (4035279)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.46/4.62 % (4035279)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.46/4.62 % (4035279)CaDiCaL version: 2.1.3 % 24.46/4.62 % (4035279)Termination reason: Instruction limit % 24.46/4.62 % (4035279)Termination phase: Saturation % 24.46/4.62 % (4035279)Time elapsed: 0.244 s % 24.46/4.62 % (4035279)Peak memory usage: 89 MB % 24.46/4.62 % (4035279)Instructions burned: 656 (million) % 24.46/4.62 % (4035290)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 % 24.46/4.62 % (4035290)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=2148341762:i=1090:aac=none:nm=0:rtra=on:rawr=on_2970 on theBenchmark for (2970ds/1090Mi) % 24.46/4.62 % (4035291)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=3656441412:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2970 on theBenchmark for (2970ds/130Mi) % 24.46/4.62 % (4035293)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=1807795072:i=312:kws=inv_frequency:nm=20:rtra=on_2970 on theBenchmark for (2970ds/312Mi) % 24.46/4.62 % (4035291)Instruction limit reached! % 24.46/4.62 % (4035291)------------------------------ % 24.46/4.62 % (4035291)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.46/4.62 % (4035291)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.46/4.62 % (4035291)CaDiCaL version: 2.1.3 % 24.46/4.62 % (4035291)Termination reason: Instruction limit % 24.46/4.62 % (4035291)Termination phase: Property scanning % 24.46/4.62 % (4035291)Time elapsed: 0.048 s % 24.46/4.62 % (4035291)Peak memory usage: 85 MB % 24.46/4.62 % (4035291)Instructions burned: 130 (million) % 24.46/4.62 % (4035293)Instruction limit reached! % 24.46/4.62 % (4035293)------------------------------ % 24.46/4.62 % (4035293)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.46/4.62 % (4035293)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.46/4.62 % (4035293)CaDiCaL version: 2.1.3 % 24.46/4.62 % (4035293)Termination reason: Instruction limit % 24.46/4.62 % (4035293)Termination phase: Property scanning % 24.46/4.62 % (4035293)Time elapsed: 0.060 s % 24.46/4.62 % (4035293)Peak memory usage: 86 MB % 24.46/4.62 % (4035293)Instructions burned: 317 (million) % 24.46/4.62 % (4035288)Instruction limit reached! % 24.46/4.62 % (4035288)------------------------------ % 24.46/4.62 % (4035288)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.46/4.62 % (4035288)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.46/4.62 % (4035288)CaDiCaL version: 2.1.3 % 24.46/4.62 % (4035288)Termination reason: Instruction limit % 24.46/4.62 % (4035288)Termination phase: Saturation % 24.46/4.62 % (4035288)Time elapsed: 0.212 s % 24.46/4.62 % (4035288)Peak memory usage: 129 MB % 24.46/4.62 % (4035288)Instructions burned: 452 (million) % 24.46/4.62 % (4035278)Instruction limit reached! % 24.46/4.62 % (4035278)------------------------------ % 24.46/4.62 % (4035278)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.46/4.62 % (4035278)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.46/4.62 % (4035278)CaDiCaL version: 2.1.3 % 24.46/4.62 % (4035278)Termination reason: Instruction limit % 24.46/4.62 % (4035278)Termination phase: Saturation % 24.46/4.62 % (4035278)Time elapsed: 0.396 s % 24.46/4.62 % (4035278)Peak memory usage: 95 MB % 24.46/4.62 % (4035278)Instructions burned: 1052 (million) % 24.46/4.62 % (4035294)ott+10_1_to=kbo:sil=64000:si=on:sp=reverse_frequency:sos=on:random_seed=236280528:i=491:doe=on:rtra=on:gtg=position_2969 on theBenchmark for (2969ds/491Mi) % 24.46/4.62 % (4035299)ott+1011_2_to=lpo:sil=128000:si=on:sos=on:random_seed=974978060:i=307:bd=preordered:av=off:rtra=on:ev=cautious_2968 on theBenchmark for (2968ds/307Mi) % 24.46/4.62 % (4035298)ott+1011_4:1_to=lpo:sil=64000:si=on:spb=intro:random_seed=1847106046:s2a=on:i=835:s2at=2:rtra=on_2968 on theBenchmark for (2968ds/835Mi) % 29.77/5.17 % (4035299)Instruction limit reached! % 29.77/5.17 % (4035299)------------------------------ % 29.77/5.17 % (4035299)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.77/5.17 % (4035299)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.77/5.17 % (4035299)CaDiCaL version: 2.1.3 % 29.77/5.17 % (4035299)Termination reason: Instruction limit % 29.77/5.17 % (4035299)Termination phase: Property scanning % 29.77/5.17 % (4035299)Time elapsed: 0.062 s % 29.77/5.17 % (4035299)Peak memory usage: 86 MB % 29.77/5.17 % (4035299)Instructions burned: 329 (million) % 29.77/5.17 % (4035301)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=1465297911:s2a=on:i=646:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2968 on theBenchmark for (2968ds/646Mi) % 29.77/5.17 % (4035300)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=2677219355:i=776:doe=on:rtra=on_2968 on theBenchmark for (2968ds/776Mi) % 29.77/5.17 % (4035294)Instruction limit reached! % 29.77/5.17 % (4035294)------------------------------ % 29.77/5.17 % (4035294)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.77/5.17 % (4035294)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.77/5.17 % (4035294)CaDiCaL version: 2.1.3 % 29.77/5.17 % (4035294)Termination reason: Instruction limit % 29.77/5.17 % (4035294)Termination phase: Property scanning % 29.77/5.17 % (4035294)Time elapsed: 0.178 s % 29.77/5.17 % (4035294)Peak memory usage: 87 MB % 29.77/5.17 % (4035294)Instructions burned: 492 (million) % 29.77/5.17 % (4035307)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=196284509:thitd=on:cond=fast:i=784:nm=30:rtra=on:gtg=all:tac=axiom_2966 on theBenchmark for (2966ds/784Mi) % 29.77/5.17 % (4035290)Instruction limit reached! % 29.77/5.17 % (4035290)------------------------------ % 29.77/5.17 % (4035290)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.77/5.17 % (4035290)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.77/5.17 % (4035290)CaDiCaL version: 2.1.3 % 29.77/5.17 % (4035290)Termination reason: Instruction limit % 29.77/5.17 % (4035290)Termination phase: Saturation % 29.77/5.17 % (4035290)Time elapsed: 0.438 s % 29.77/5.17 % (4035290)Peak memory usage: 116 MB % 29.77/5.17 % (4035290)Instructions burned: 1090 (million) % 29.77/5.17 % (4035308)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=387721642:thitd=on:s2a=on:i=1131:add=on:canc=force:bd=all:rtra=on:tac=axiom:ev=off_2966 on theBenchmark for (2966ds/1131Mi) % 29.77/5.17 % (4035298)Instruction limit reached! % 29.77/5.17 % (4035298)------------------------------ % 29.77/5.17 % (4035298)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.77/5.17 % (4035298)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.77/5.17 % (4035298)CaDiCaL version: 2.1.3 % 29.77/5.17 % (4035298)Termination reason: Instruction limit % 29.77/5.17 % (4035298)Termination phase: Saturation % 29.77/5.17 % (4035298)Time elapsed: 0.315 s % 29.77/5.17 % (4035298)Peak memory usage: 92 MB % 29.77/5.17 % (4035298)Instructions burned: 835 (million) % 29.77/5.17 % (4035307)Instruction limit reached! % 29.77/5.17 % (4035307)------------------------------ % 29.77/5.17 % (4035307)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.77/5.17 % (4035307)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.77/5.17 % (4035307)CaDiCaL version: 2.1.3 % 29.77/5.17 % (4035307)Termination reason: Instruction limit % 29.77/5.17 % (4035307)Termination phase: Saturation % 29.77/5.17 % (4035307)Time elapsed: 0.163 s % 29.77/5.17 % (4035307)Peak memory usage: 112 MB % 29.77/5.17 % (4035307)Instructions burned: 784 (million) % 29.77/5.17 % (4035301)Instruction limit reached! % 29.77/5.17 % (4035301)------------------------------ % 29.77/5.17 % (4035301)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.77/5.17 % (4035301)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.77/5.17 % (4035301)CaDiCaL version: 2.1.3 % 29.77/5.17 % (4035301)Termination reason: Instruction limit % 29.77/5.17 % (4035301)Termination phase: Saturation % 29.77/5.17 % (4035301)Time elapsed: 0.285 s % 29.77/5.17 % (4035301)Peak memory usage: 130 MB % 29.77/5.17 % (4035301)Instructions burned: 648 (million) % 29.77/5.17 % (4035300)Instruction limit reached! % 29.77/5.17 % (4035300)------------------------------ % 36.14/6.09 % (4035300)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 36.14/6.09 % (4035300)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.14/6.09 % (4035300)CaDiCaL version: 2.1.3 % 36.14/6.09 % (4035300)Termination reason: Instruction limit % 36.14/6.09 % (4035300)Termination phase: Saturation % 36.14/6.09 % (4035300)Time elapsed: 0.317 s % 36.14/6.09 % (4035300)Peak memory usage: 117 MB % 36.14/6.09 % (4035300)Instructions burned: 779 (million) % 36.14/6.09 % (4035310)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=466694173:s2pl=no:i=246:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2964 on theBenchmark for (2964ds/246Mi) % 36.14/6.09 % (4035313)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=969152475:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2963 on theBenchmark for (2963ds/273Mi) % 36.14/6.09 % (4035312)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=2226437137:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2963 on theBenchmark for (2963ds/775Mi) % 36.14/6.09 % (4035310)Instruction limit reached! % 36.14/6.09 % (4035310)------------------------------ % 36.14/6.09 % (4035310)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 36.14/6.09 % (4035310)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.14/6.09 % (4035310)CaDiCaL version: 2.1.3 % 36.14/6.09 % (4035310)Termination reason: Instruction limit % 36.14/6.09 % (4035310)Termination phase: SInE selection % 36.14/6.09 % (4035310)Time elapsed: 0.093 s % 36.14/6.09 % (4035310)Peak memory usage: 86 MB % 36.14/6.09 % (4035310)Instructions burned: 248 (million) % 36.14/6.09 % (4035314)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=169824414:i=102:nm=16:rtra=on_2963 on theBenchmark for (2963ds/102Mi) % 36.14/6.09 % (4035313)Instruction limit reached! % 36.14/6.09 % (4035313)------------------------------ % 36.14/6.09 % (4035313)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 36.14/6.09 % (4035313)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.14/6.09 % (4035313)CaDiCaL version: 2.1.3 % 36.14/6.09 % (4035313)Termination reason: Instruction limit % 36.14/6.09 % (4035313)Termination phase: Property scanning % 36.14/6.09 % (4035313)Time elapsed: 0.054 s % 36.14/6.09 % (4035313)Peak memory usage: 86 MB % 36.14/6.09 % (4035313)Instructions burned: 279 (million) % 36.14/6.09 % (4035314)Instruction limit reached! % 36.14/6.09 % (4035314)------------------------------ % 36.14/6.09 % (4035314)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 36.14/6.09 % (4035314)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.14/6.09 % (4035314)CaDiCaL version: 2.1.3 % 36.14/6.09 % (4035314)Termination reason: Instruction limit % 36.14/6.09 % (4035314)Termination phase: Property scanning % 36.14/6.09 % (4035314)Time elapsed: 0.038 s % 36.14/6.09 % (4035314)Peak memory usage: 86 MB % 36.14/6.09 % (4035314)Instructions burned: 102 (million) % 36.14/6.09 % (4035315)lrs+10_1_to=lpo:sil=128000:si=on:bsr=unit_only:tha=off:random_seed=2694414951:avsq=on:s2a=on:i=1094:s2at=5:avsqr=4463,131072:rtra=on_2963 on theBenchmark for (2963ds/1094Mi) % 36.14/6.09 % (4035312)Refutation not found, incomplete strategy % 36.14/6.09 % (4035312)------------------------------ % 36.14/6.09 % (4035312)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 36.14/6.09 % (4035312)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.14/6.09 % (4035312)CaDiCaL version: 2.1.3 % 36.14/6.09 % (4035312)Termination reason: Refutation not found, incomplete strategy % 36.14/6.09 % (4035312)Time elapsed: 0.112 s % 36.14/6.09 % (4035312)Peak memory usage: 88 MB % 36.14/6.09 % (4035312)Instructions burned: 304 (million) % 36.14/6.09 % (4035321)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=3969608304:i=868:doe=on:nm=0:rtra=on:gtg=exists_sym_2962 on theBenchmark for (2962ds/868Mi) % 36.14/6.09 % (4035319)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=1171064256:i=6400:doe=on:fsr=off:rtra=on_2962 on theBenchmark for (2962ds/6400Mi) % 36.14/6.09 % (4035322)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=3473983443:i=1846:canc=cautious:fsr=off:rtra=on_2961 on theBenchmark for (2961ds/1846Mi) % 43.21/7.05 % (4035308)Instruction limit reached! % 43.21/7.05 % (4035308)------------------------------ % 43.21/7.05 % (4035308)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 43.21/7.05 % (4035308)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.21/7.05 % (4035308)CaDiCaL version: 2.1.3 % 43.21/7.05 % (4035308)Termination reason: Instruction limit % 43.21/7.05 % (4035308)Termination phase: Saturation % 43.21/7.05 % (4035308)Time elapsed: 0.452 s % 43.21/7.05 % (4035308)Peak memory usage: 117 MB % 43.21/7.05 % (4035308)Instructions burned: 1132 (million) % 43.21/7.05 % (4035321)Instruction limit reached! % 43.21/7.05 % (4035321)------------------------------ % 43.21/7.05 % (4035321)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 43.21/7.05 % (4035321)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.21/7.05 % (4035321)CaDiCaL version: 2.1.3 % 43.21/7.05 % (4035321)Termination reason: Instruction limit % 43.21/7.05 % (4035321)Termination phase: Saturation % 43.21/7.05 % (4035321)Time elapsed: 0.181 s % 43.21/7.05 % (4035321)Peak memory usage: 116 MB % 43.21/7.05 % (4035321)Instructions burned: 871 (million) % 43.21/7.05 % (4035312)------------------------------ % 43.21/7.05 % (4035312)------------------------------ % 43.21/7.05 % (4035327)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=1841140113:s2a=on:i=36816:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2960 on theBenchmark for (2960ds/36816Mi) % 43.21/7.05 % (4035328)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=3052503889:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2959 on theBenchmark for (2959ds/273Mi) % 43.21/7.05 % (4035322)Refutation not found, incomplete strategy % 43.21/7.05 % (4035322)------------------------------ % 43.21/7.05 % (4035322)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 43.21/7.05 % (4035322)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.21/7.05 % (4035322)CaDiCaL version: 2.1.3 % 43.21/7.05 % (4035322)Termination reason: Refutation not found, incomplete strategy % 43.21/7.05 % (4035322)Time elapsed: 0.253 s % 43.21/7.05 % (4035322)Peak memory usage: 91 MB % 43.21/7.05 % (4035322)Instructions burned: 676 (million) % 43.21/7.05 % (4035328)Instruction limit reached! % 43.21/7.05 % (4035328)------------------------------ % 43.21/7.05 % (4035328)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 43.21/7.05 % (4035328)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.21/7.05 % (4035328)CaDiCaL version: 2.1.3 % 43.21/7.05 % (4035328)Termination reason: Instruction limit % 43.21/7.05 % (4035328)Termination phase: Property scanning % 43.21/7.05 % (4035328)Time elapsed: 0.052 s % 43.21/7.05 % (4035328)Peak memory usage: 86 MB % 43.21/7.05 % (4035328)Instructions burned: 275 (million) % 43.21/7.05 % (4035315)Instruction limit reached! % 43.21/7.05 % (4035315)------------------------------ % 43.21/7.05 % (4035315)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 43.21/7.05 % (4035315)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.21/7.05 % (4035315)CaDiCaL version: 2.1.3 % 43.21/7.05 % (4035315)Termination reason: Instruction limit % 43.21/7.05 % (4035315)Termination phase: Saturation % 43.21/7.05 % (4035315)Time elapsed: 0.421 s % 43.21/7.05 % (4035315)Peak memory usage: 95 MB % 43.21/7.05 % (4035315)Instructions burned: 1097 (million) % 43.21/7.05 % (4035329)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=1165862541:i=863:doe=on:nm=0:rtra=on:gtg=exists_sym_2958 on theBenchmark for (2958ds/863Mi) % 43.21/7.05 % (4035332)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=1164635635:i=5811:kws=precedence:nm=0:rtra=on_2957 on theBenchmark for (2957ds/5811Mi) % 43.21/7.05 % (4035333)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=1867100456:i=2216:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2957 on theBenchmark for (2957ds/2216Mi) % 43.21/7.05 % (4035322)------------------------------ % 43.21/7.05 % (4035322)------------------------------ % 43.21/7.05 % (4035276)Instruction limit reached! % 43.21/7.05 % (4035276)------------------------------ % 43.21/7.05 % (4035276)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 43.21/7.05 % (4035276)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 46.41/7.69 % (4035276)CaDiCaL version: 2.1.3 % 46.41/7.69 % (4035276)Termination reason: Instruction limit % 46.41/7.69 % (4035276)Termination phase: Saturation % 46.41/7.69 % (4035276)Time elapsed: 1.718 s % 46.41/7.69 % (4035276)Peak memory usage: 92 MB % 46.41/7.69 % (4035276)Instructions burned: 4430 (million) % 46.41/7.69 % (4035329)Instruction limit reached! % 46.41/7.69 % (4035329)------------------------------ % 46.41/7.69 % (4035329)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 46.41/7.69 % (4035329)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 46.41/7.69 % (4035329)CaDiCaL version: 2.1.3 % 46.41/7.69 % (4035329)Termination reason: Instruction limit % 46.41/7.69 % (4035329)Termination phase: Saturation % 46.41/7.69 % (4035329)Time elapsed: 0.327 s % 46.41/7.69 % (4035329)Peak memory usage: 116 MB % 46.41/7.69 % (4035329)Instructions burned: 863 (million) % 46.41/7.69 % (4035337)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=406935318:i=801:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2955 on theBenchmark for (2955ds/801Mi) % 46.41/7.69 % (4035338)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=2521301614:st=5:i=1026:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2954 on theBenchmark for (2954ds/1026Mi) % 46.41/7.69 % (4035338)Refutation not found, incomplete strategy % 46.41/7.69 % (4035338)------------------------------ % 46.41/7.69 % (4035338)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 46.41/7.69 % (4035338)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 46.41/7.69 % (4035338)CaDiCaL version: 2.1.3 % 46.41/7.69 % (4035338)Termination reason: Refutation not found, incomplete strategy % 46.41/7.69 % (4035338)Time elapsed: 0.065 s % 46.41/7.69 % (4035338)Peak memory usage: 88 MB % 46.41/7.69 % (4035338)Instructions burned: 180 (million) % 46.41/7.69 % (4035340)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=373722253:i=3509:rtra=on_2953 on theBenchmark for (2953ds/3509Mi) % 46.41/7.69 % (4035337)Instruction limit reached! % 46.41/7.69 % (4035337)------------------------------ % 46.41/7.69 % (4035337)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 46.41/7.69 % (4035337)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 46.41/7.69 % (4035337)CaDiCaL version: 2.1.3 % 46.41/7.69 % (4035337)Termination reason: Instruction limit % 46.41/7.69 % (4035337)Termination phase: Saturation % 46.41/7.69 % (4035337)Time elapsed: 0.288 s % 46.41/7.69 % (4035337)Peak memory usage: 93 MB % 46.41/7.69 % (4035337)Instructions burned: 801 (million) % 46.41/7.69 % (4035338)------------------------------ % 46.41/7.69 % (4035338)------------------------------ % 46.41/7.69 % (4035343)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=4148587841:st=2:i=2127:sd=12:ep=R:rtra=on:ss=axioms_2950 on theBenchmark for (2950ds/2127Mi) % 46.41/7.69 % (4035344)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=3907617701:i=1959:rtra=on:fsd=on:proc=on_2950 on theBenchmark for (2950ds/1959Mi) % 46.41/7.69 % (4035343)Refutation not found, incomplete strategy % 46.41/7.69 % (4035343)------------------------------ % 46.41/7.69 % (4035343)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 46.41/7.69 % (4035343)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 46.41/7.69 % (4035343)CaDiCaL version: 2.1.3 % 46.41/7.69 % (4035343)Termination reason: Refutation not found, incomplete strategy % 46.41/7.69 % (4035343)Time elapsed: 0.104 s % 46.41/7.69 % (4035343)Peak memory usage: 88 MB % 46.41/7.69 % (4035343)Instructions burned: 289 (million) % 46.41/7.69 % (4035333)Instruction limit reached! % 46.41/7.69 % (4035333)------------------------------ % 46.41/7.69 % (4035333)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 46.41/7.69 % (4035333)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 46.41/7.69 % (4035333)CaDiCaL version: 2.1.3 % 46.41/7.69 % (4035333)Termination reason: Instruction limit % 46.41/7.69 % (4035333)Termination phase: Saturation % 46.41/7.69 % (4035333)Time elapsed: 0.843 s % 46.41/7.69 % (4035333)Peak memory usage: 120 MB % 46.41/7.69 % (4035333)Instructions burned: 2217 (million) % 46.41/7.69 % (4035343)------------------------------ % 46.41/7.69 % (4035343)------------------------------ % 46.41/7.69 % (4035347)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=2224204408:s2a=on:i=3553:nm=0:rtra=on_2947 on theBenchmark for (2947ds/3553Mi) % 64.47/10.13 % (4035332)Instruction limit reached! % 64.47/10.13 % (4035332)------------------------------ % 64.47/10.13 % (4035332)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 64.47/10.13 % (4035332)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 64.47/10.13 % (4035332)CaDiCaL version: 2.1.3 % 64.47/10.13 % (4035332)Termination reason: Instruction limit % 64.47/10.13 % (4035332)Termination phase: Saturation % 64.47/10.13 % (4035332)Time elapsed: 1.163 s % 64.47/10.13 % (4035332)Peak memory usage: 124 MB % 64.47/10.13 % (4035332)Instructions burned: 5812 (million) % 64.47/10.13 % (4035348)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=3391557055:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2946 on theBenchmark for (2946ds/3201Mi) % 64.47/10.13 % (4035350)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=3383744141:thitd=on:cond=on:i=4093:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2944 on theBenchmark for (2944ds/4093Mi) % 64.47/10.13 % (4035344)Instruction limit reached! % 64.47/10.13 % (4035344)------------------------------ % 64.47/10.13 % (4035344)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 64.47/10.13 % (4035344)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 64.47/10.13 % (4035344)CaDiCaL version: 2.1.3 % 64.47/10.13 % (4035344)Termination reason: Instruction limit % 64.47/10.13 % (4035344)Termination phase: Saturation % 64.47/10.13 % (4035344)Time elapsed: 0.766 s % 64.47/10.13 % (4035344)Peak memory usage: 122 MB % 64.47/10.13 % (4035344)Instructions burned: 1959 (million) % 64.47/10.13 % (4035353)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=1089713927:cond=fast:i=21173:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2940 on theBenchmark for (2940ds/21173Mi) % 64.47/10.13 % (4035340)Instruction limit reached! % 64.47/10.13 % (4035340)------------------------------ % 64.47/10.13 % (4035340)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 64.47/10.13 % (4035340)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 64.47/10.13 % (4035340)CaDiCaL version: 2.1.3 % 64.47/10.13 % (4035340)Termination reason: Instruction limit % 64.47/10.13 % (4035340)Termination phase: Saturation % 64.47/10.13 % (4035340)Time elapsed: 1.334 s % 64.47/10.13 % (4035340)Peak memory usage: 92 MB % 64.47/10.13 % (4035340)Instructions burned: 3512 (million) % 64.47/10.13 % (4035353)Refutation not found, incomplete strategy % 64.47/10.13 % (4035353)------------------------------ % 64.47/10.13 % (4035353)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 64.47/10.13 % (4035353)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 64.47/10.13 % (4035353)CaDiCaL version: 2.1.3 % 64.47/10.13 % (4035353)Termination reason: Refutation not found, incomplete strategy % 64.47/10.13 % (4035353)Time elapsed: 0.080 s % 64.47/10.13 % (4035353)Peak memory usage: 113 MB % 64.47/10.13 % (4035353)Instructions burned: 147 (million) % 64.47/10.13 % (4035348)Refutation not found, incomplete strategy % 64.47/10.13 % (4035348)------------------------------ % 64.47/10.13 % (4035348)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 64.47/10.13 % (4035348)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 64.47/10.13 % (4035348)CaDiCaL version: 2.1.3 % 64.47/10.13 % (4035348)Termination reason: Refutation not found, incomplete strategy % 64.47/10.13 % (4035348)Time elapsed: 0.694 s % 64.47/10.13 % (4035348)Peak memory usage: 99 MB % 64.47/10.13 % (4035348)Instructions burned: 1826 (million) % 64.47/10.13 % (4035355)lrs+11_1_to=lpo:thi=all:sas=z3:si=on:fd=off:sac=on:slsq=on:random_seed=694576375:avsq=on:i=10544:avsqr=17,4:canc=force:rtra=on:gtg=exists_top:er=filter_2938 on theBenchmark for (2938ds/10544Mi) % 64.47/10.13 % (4035319)Instruction limit reached! % 64.47/10.13 % (4035319)------------------------------ % 64.47/10.13 % (4035319)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 64.47/10.13 % (4035319)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 64.47/10.13 % (4035319)CaDiCaL version: 2.1.3 % 64.47/10.13 % (4035319)Termination reason: Instruction limit % 64.47/10.13 % (4035319)Termination phase: Saturation % 64.47/10.13 % (4035319)Time elapsed: 2.403 s % 64.47/10.13 % (4035319)Peak memory usage: 92 MB % 64.47/10.13 % (4035319)Instructions burned: 6400 (million) % 64.47/10.13 % (4035353)------------------------------ % 75.31/11.66 % (4035353)------------------------------ % 75.31/11.66 % (4035350)Instruction limit reached! % 75.31/11.66 % (4035350)------------------------------ % 75.31/11.66 % (4035350)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 75.31/11.66 % (4035350)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 75.31/11.66 % (4035350)CaDiCaL version: 2.1.3 % 75.31/11.66 % (4035350)Termination reason: Instruction limit % 75.31/11.66 % (4035350)Termination phase: Saturation % 75.31/11.66 % (4035350)Time elapsed: 0.854 s % 75.31/11.66 % (4035350)Peak memory usage: 134 MB % 75.31/11.66 % (4035350)Instructions burned: 4097 (million) % 75.31/11.66 % (4035357)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=3408282667:avsq=on:i=1262:avsqr=1,16:rtra=on:rawr=on_2936 on theBenchmark for (2936ds/1262Mi) % 75.31/11.66 % (4035348)------------------------------ % 75.31/11.66 % (4035348)------------------------------ % 75.31/11.66 % (4035358)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=1067190484:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2936 on theBenchmark for (2936ds/775Mi) % 75.31/11.66 % (4035360)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=415525953:i=270:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2935 on theBenchmark for (2935ds/270Mi) % 75.31/11.66 % (4035360)Instruction limit reached! % 75.31/11.66 % (4035360)------------------------------ % 75.31/11.66 % (4035360)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 75.31/11.66 % (4035360)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 75.31/11.66 % (4035360)CaDiCaL version: 2.1.3 % 75.31/11.66 % (4035360)Termination reason: Instruction limit % 75.31/11.66 % (4035360)Termination phase: Property scanning % 75.31/11.66 % (4035360)Time elapsed: 0.052 s % 75.31/11.66 % (4035360)Peak memory usage: 86 MB % 75.31/11.66 % (4035360)Instructions burned: 274 (million) % 75.31/11.66 % (4035358)Refutation not found, incomplete strategy % 75.31/11.66 % (4035358)------------------------------ % 75.31/11.66 % (4035358)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 75.31/11.66 % (4035358)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 75.31/11.66 % (4035358)CaDiCaL version: 2.1.3 % 75.31/11.66 % (4035358)Termination reason: Refutation not found, incomplete strategy % 75.31/11.66 % (4035358)Time elapsed: 0.111 s % 75.31/11.66 % (4035358)Peak memory usage: 88 MB % 75.31/11.66 % (4035358)Instructions burned: 304 (million) % 75.31/11.66 % (4035361)ott+10_128_isp=bottom:to=lpo:sil=128000:si=on:urr=on:uwa=alasca_main:sac=on:slsq=on:random_seed=937720996:i=17165:aac=none:doe=on:rtra=on:gtg=exists_all_2934 on theBenchmark for (2934ds/17165Mi) % 75.31/11.66 % (4035347)Instruction limit reached! % 75.31/11.66 % (4035347)------------------------------ % 75.31/11.66 % (4035347)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 75.31/11.66 % (4035347)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 75.31/11.66 % (4035347)CaDiCaL version: 2.1.3 % 75.31/11.66 % (4035347)Termination reason: Instruction limit % 75.31/11.66 % (4035347)Termination phase: Saturation % 75.31/11.66 % (4035347)Time elapsed: 1.346 s % 75.31/11.66 % (4035347)Peak memory usage: 95 MB % 75.31/11.66 % (4035347)Instructions burned: 3556 (million) % 75.31/11.66 % (4035364)lrs+2_10_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_main:tha=some:random_seed=1109271455:s2a=on:i=13094:s2at=-1:rtra=on_2933 on theBenchmark for (2933ds/13094Mi) % 75.31/11.66 % (4035358)------------------------------ % 75.31/11.66 % (4035358)------------------------------ % 75.31/11.66 % (4035367)lrs+10_1_to=lpo:sil=128000:si=on:sp=occurrence:random_seed=2697446725:st=2:i=12633:rtra=on:ss=axioms_2932 on theBenchmark for (2932ds/12633Mi) % 75.31/11.66 % (4035357)Instruction limit reached! % 75.31/11.66 % (4035357)------------------------------ % 75.31/11.66 % (4035357)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 75.31/11.66 % (4035357)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 75.31/11.66 % (4035357)CaDiCaL version: 2.1.3 % 75.31/11.66 % (4035357)Termination reason: Instruction limit % 75.31/11.66 % (4035357)Termination phase: Saturation % 75.31/11.66 % (4035357)Time elapsed: 0.501 s % 75.31/11.66 % (4035357)Peak memory usage: 116 MB % 75.31/11.66 % (4035357)Instructions burned: 1264 (million) % 75.31/11.66 % (4035367)Refutation not found, incomplete strategy % 75.31/11.66 % (4035367)------------------------------ % 75.31/11.66 % (4035367)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 95.26/14.49 % (4035367)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 95.26/14.49 % (4035367)CaDiCaL version: 2.1.3 % 95.26/14.49 % (4035367)Termination reason: Refutation not found, incomplete strategy % 95.26/14.49 % (4035367)Time elapsed: 0.095 s % 95.26/14.49 % (4035367)Peak memory usage: 88 MB % 95.26/14.49 % (4035367)Instructions burned: 257 (million) % 95.26/14.49 % (4035368)dis+1011_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_frequency:lsd=20:nwc=3:random_seed=3153605589:i=1783:rtra=on:gtg=position_2930 on theBenchmark for (2930ds/1783Mi) % 95.26/14.49 % (4035370)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=678803512:i=5451:aac=none:doe=on:nm=0:rtra=on:amm=off:gtg=position_2930 on theBenchmark for (2930ds/5451Mi) % 95.26/14.49 % (4035367)------------------------------ % 95.26/14.49 % (4035367)------------------------------ % 95.26/14.49 % (4035373)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=1095525554:i=4975:doe=on:nm=0:rtra=on:gtg=exists_sym_2927 on theBenchmark for (2927ds/4975Mi) % 95.26/14.49 % (4035368)Instruction limit reached! % 95.26/14.49 % (4035368)------------------------------ % 95.26/14.49 % (4035368)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 95.26/14.49 % (4035368)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 95.26/14.49 % (4035368)CaDiCaL version: 2.1.3 % 95.26/14.49 % (4035368)Termination reason: Instruction limit % 95.26/14.49 % (4035368)Termination phase: Saturation % 95.26/14.49 % (4035368)Time elapsed: 0.674 s % 95.26/14.49 % (4035368)Peak memory usage: 114 MB % 95.26/14.49 % (4035368)Instructions burned: 1783 (million) % 95.26/14.49 % (4035375)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=2908989636:i=2076:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2922 on theBenchmark for (2922ds/2076Mi) % 95.26/14.49 % (4035375)Instruction limit reached! % 95.26/14.49 % (4035375)------------------------------ % 95.26/14.49 % (4035375)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 95.26/14.49 % (4035375)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 95.26/14.49 % (4035375)CaDiCaL version: 2.1.3 % 95.26/14.49 % (4035375)Termination reason: Instruction limit % 95.26/14.49 % (4035375)Termination phase: Saturation % 95.26/14.49 % (4035375)Time elapsed: 0.784 s % 95.26/14.49 % (4035375)Peak memory usage: 116 MB % 95.26/14.49 % (4035375)Instructions burned: 2079 (million) % 95.26/14.49 % (4035377)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=2616785105:i=5145:rtra=on_2912 on theBenchmark for (2912ds/5145Mi) % 95.26/14.49 % (4035370)Instruction limit reached! % 95.26/14.49 % (4035370)------------------------------ % 95.26/14.49 % (4035370)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 95.26/14.49 % (4035370)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 95.26/14.49 % (4035370)CaDiCaL version: 2.1.3 % 95.26/14.49 % (4035370)Termination reason: Instruction limit % 95.26/14.49 % (4035370)Termination phase: Saturation % 95.26/14.49 % (4035370)Time elapsed: 2.090 s % 95.26/14.49 % (4035370)Peak memory usage: 125 MB % 95.26/14.49 % (4035370)Instructions burned: 5453 (million) % 95.26/14.49 % (4035364)Instruction limit reached! % 95.26/14.49 % (4035364)------------------------------ % 95.26/14.49 % (4035364)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 95.26/14.49 % (4035364)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 95.26/14.49 % (4035364)CaDiCaL version: 2.1.3 % 95.26/14.49 % (4035364)Termination reason: Instruction limit % 95.26/14.49 % (4035364)Termination phase: Saturation % 95.26/14.49 % (4035364)Time elapsed: 2.509 s % 95.26/14.49 % (4035364)Peak memory usage: 97 MB % 95.26/14.49 % (4035364)Instructions burned: 13095 (million) % 95.26/14.49 % (4035379)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=2999233522:i=3509:rtra=on_2907 on theBenchmark for (2907ds/3509Mi) % 95.26/14.49 % (4035380)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=2220233090:st=2:i=13800:sd=12:ep=R:rtra=on:ss=axioms_2907 on theBenchmark for (2907ds/13800Mi) % 95.26/14.49 % (4035380)Refutation not found, incomplete strategy % 95.26/14.49 % (4035380)------------------------------ % 95.26/14.49 % (4035380)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 215.04/31.26 % (4035380)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 215.04/31.26 % (4035380)CaDiCaL version: 2.1.3 % 215.04/31.26 % (4035380)Termination reason: Refutation not found, incomplete strategy % 215.04/31.26 % (4035380)Time elapsed: 0.056 s % 215.04/31.26 % (4035380)Peak memory usage: 88 MB % 215.04/31.26 % (4035380)Instructions burned: 289 (million) % 215.04/31.26 % (4035380)------------------------------ % 215.04/31.26 % (4035380)------------------------------ % 215.04/31.26 % (4035447)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=2679717686:i=1412:rtra=on:fsd=on:proc=on_2903 on theBenchmark for (2903ds/1412Mi) % 215.04/31.26 % (4035373)Instruction limit reached! % 215.04/31.26 % (4035373)------------------------------ % 215.04/31.26 % (4035373)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 215.04/31.26 % (4035373)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 215.04/31.26 % (4035373)CaDiCaL version: 2.1.3 % 215.04/31.26 % (4035373)Termination reason: Instruction limit % 215.04/31.26 % (4035373)Termination phase: Saturation % 215.04/31.26 % (4035373)Time elapsed: 2.409 s % 215.04/31.26 % (4035373)Peak memory usage: 166 MB % 215.04/31.26 % (4035373)Instructions burned: 4977 (million) % 215.04/31.26 % (4035501)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 % 215.04/31.26 % (4035501)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=137233233:i=11747:aac=none:nm=0:rtra=on:rawr=on_2901 on theBenchmark for (2901ds/11747Mi) % 215.04/31.26 % (4035447)Instruction limit reached! % 215.04/31.26 % (4035447)------------------------------ % 215.04/31.26 % (4035447)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 215.04/31.26 % (4035447)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 215.04/31.26 % (4035447)CaDiCaL version: 2.1.3 % 215.04/31.26 % (4035447)Termination reason: Instruction limit % 215.04/31.26 % (4035447)Termination phase: Saturation % 215.04/31.26 % (4035447)Time elapsed: 0.295 s % 215.04/31.26 % (4035447)Peak memory usage: 116 MB % 215.04/31.26 % (4035447)Instructions burned: 1415 (million) % 215.04/31.26 % (4035503)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=4137190426:s2a=on:i=3553:nm=0:rtra=on_2899 on theBenchmark for (2899ds/3553Mi) % 215.04/31.26 % (4035379)Instruction limit reached! % 215.04/31.26 % (4035379)------------------------------ % 215.04/31.26 % (4035379)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 215.04/31.26 % (4035379)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 215.04/31.26 % (4035379)CaDiCaL version: 2.1.3 % 215.04/31.26 % (4035379)Termination reason: Instruction limit % 215.04/31.26 % (4035379)Termination phase: Saturation % 215.04/31.26 % (4035379)Time elapsed: 1.326 s % 215.04/31.26 % (4035379)Peak memory usage: 92 MB % 215.04/31.26 % (4035379)Instructions burned: 3509 (million) % 215.04/31.26 % (4035377)Instruction limit reached! % 215.04/31.26 % (4035377)------------------------------ % 215.04/31.26 % (4035377)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 215.04/31.26 % (4035377)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 215.04/31.26 % (4035377)CaDiCaL version: 2.1.3 % 215.04/31.26 % (4035377)Termination reason: Instruction limit % 215.04/31.26 % (4035377)Termination phase: Saturation % 215.04/31.26 % (4035377)Time elapsed: 1.947 s % 215.04/31.26 % (4035377)Peak memory usage: 95 MB % 215.04/31.26 % (4035377)Instructions burned: 5145 (million) % 215.04/31.26 % (4035635)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=2382448733:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2892 on theBenchmark for (2892ds/3201Mi) % 215.04/31.26 % (4035503)Instruction limit reached! % 215.04/31.26 % (4035503)------------------------------ % 215.04/31.26 % (4035503)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 215.04/31.26 % (4035503)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 215.04/31.26 % (4035503)CaDiCaL version: 2.1.3 % 215.04/31.26 % (4035503)Termination reason: Instruction limit % 215.04/31.26 % (4035503)Termination phase: Saturation % 215.04/31.26 % (4035503)Time elapsed: 0.746 s % 215.04/31.26 % (4035503)Peak memory usage: 93 MB % 215.04/31.26 % (4035503)Instructions burned: 3559 (million) % 215.04/31.26 % (4035638)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=879043377:cond=fast:i=20260:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2891 on theBenchmark for (2891ds/20260Mi) % 254.86/36.98 % (4035638)Refutation not found, incomplete strategy % 254.86/36.98 % (4035638)------------------------------ % 254.86/36.98 % (4035638)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 254.86/36.98 % (4035638)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 254.86/36.98 % (4035638)CaDiCaL version: 2.1.3 % 254.86/36.98 % (4035638)Termination reason: Refutation not found, incomplete strategy % 254.86/36.98 % (4035638)Time elapsed: 0.044 s % 254.86/36.98 % (4035638)Peak memory usage: 113 MB % 254.86/36.98 % (4035638)Instructions burned: 147 (million) % 254.86/36.98 % (4035355)Instruction limit reached! % 254.86/36.98 % (4035355)------------------------------ % 254.86/36.98 % (4035355)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 254.86/36.98 % (4035355)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 254.86/36.98 % (4035355)CaDiCaL version: 2.1.3 % 254.86/36.98 % (4035355)Termination reason: Instruction limit % 254.86/36.98 % (4035355)Termination phase: Saturation % 254.86/36.98 % (4035355)Time elapsed: 4.813 s % 254.86/36.98 % (4035355)Peak memory usage: 170 MB % 254.86/36.98 % (4035355)Instructions burned: 10546 (million) % 254.86/36.98 % (4035636)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=2103143281:thitd=on:cond=on:i=4081:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2891 on theBenchmark for (2891ds/4081Mi) % 254.86/36.98 % (4035638)------------------------------ % 254.86/36.98 % (4035638)------------------------------ % 254.86/36.98 % (4035641)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=291501658:s2a=on:i=58627:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2888 on theBenchmark for (2888ds/58627Mi) % 254.86/36.98 % (4035642)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=1171272674:avsq=on:i=6258:avsqr=1,16:rtra=on:rawr=on_2888 on theBenchmark for (2888ds/6258Mi) % 254.86/36.98 % (4035635)Refutation not found, incomplete strategy % 254.86/36.98 % (4035635)------------------------------ % 254.86/36.98 % (4035635)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 254.86/36.98 % (4035635)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 254.86/36.98 % (4035635)CaDiCaL version: 2.1.3 % 254.86/36.98 % (4035635)Termination reason: Refutation not found, incomplete strategy % 254.86/36.98 % (4035635)Time elapsed: 0.940 s % 254.86/36.98 % (4035635)Peak memory usage: 99 MB % 254.86/36.98 % (4035635)Instructions burned: 1889 (million) % 254.86/36.98 % (4035635)------------------------------ % 254.86/36.98 % (4035635)------------------------------ % 254.86/36.98 % (4035694)ott+10_128_isp=bottom:to=lpo:sil=128000:si=on:urr=on:uwa=alasca_main:sac=on:slsq=on:random_seed=2420821232:i=34001:aac=none:doe=on:rtra=on:gtg=exists_all_2877 on theBenchmark for (2877ds/34001Mi) % 254.86/36.98 % (4035642)Instruction limit reached! % 254.86/36.98 % (4035642)------------------------------ % 254.86/36.98 % (4035642)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 254.86/36.98 % (4035642)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 254.86/36.98 % (4035642)CaDiCaL version: 2.1.3 % 254.86/36.98 % (4035642)Termination reason: Instruction limit % 254.86/36.98 % (4035642)Termination phase: Saturation % 254.86/36.98 % (4035642)Time elapsed: 1.831 s % 254.86/36.98 % (4035642)Peak memory usage: 128 MB % 254.86/36.98 % (4035642)Instructions burned: 6259 (million) % 254.86/36.98 % (4035734)lrs+2_10_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_main:tha=some:random_seed=1133786737:s2a=on:i=71622:s2at=-1:rtra=on_2867 on theBenchmark for (2867ds/71622Mi) % 254.86/36.98 % (4035636)Instruction limit reached! % 254.86/36.98 % (4035636)------------------------------ % 254.86/36.98 % (4035636)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 254.86/36.98 % (4035636)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 254.86/36.98 % (4035636)CaDiCaL version: 2.1.3 % 254.86/36.98 % (4035636)Termination reason: Instruction limit % 254.86/36.98 % (4035636)Termination phase: Saturation % 254.86/36.98 % (4035636)Time elapsed: 2.428 s % 254.86/36.98 % (4035636)Peak memory usage: 135 MB % 254.86/36.98 % (4035636)Instructions burned: 4082 (million) % 254.86/36.98 % (4035744)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=191115223:i=24001:kws=precedence:nm=0:rtra=on_2864 on theBenchmark for (2864ds/24001Mi) % 292.26/42.11 % (4035361)Instruction limit reached! % 292.26/42.11 % (4035361)------------------------------ % 292.26/42.11 % (4035361)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 292.26/42.11 % (4035361)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 292.26/42.11 % (4035361)CaDiCaL version: 2.1.3 % 292.26/42.11 % (4035361)Termination reason: Instruction limit % 292.26/42.11 % (4035361)Termination phase: Saturation % 292.26/42.11 % (4035361)Time elapsed: 7.689 s % 292.26/42.11 % (4035361)Peak memory usage: 92 MB % 292.26/42.11 % (4035361)Instructions burned: 17166 (million) % 292.26/42.11 % (4035771)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=3677291018:i=2076:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2856 on theBenchmark for (2856ds/2076Mi) % 292.26/42.11 % (4035771)Instruction limit reached! % 292.26/42.11 % (4035771)------------------------------ % 292.26/42.11 % (4035771)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 292.26/42.11 % (4035771)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 292.26/42.11 % (4035771)CaDiCaL version: 2.1.3 % 292.26/42.11 % (4035771)Termination reason: Instruction limit % 292.26/42.11 % (4035771)Termination phase: Saturation % 292.26/42.11 % (4035771)Time elapsed: 1.490 s % 292.26/42.11 % (4035771)Peak memory usage: 116 MB % 292.26/42.11 % (4035771)Instructions burned: 2077 (million) % 292.26/42.11 % (4035501)Instruction limit reached! % 292.26/42.11 % (4035501)------------------------------ % 292.26/42.11 % (4035501)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 292.26/42.11 % (4035501)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 292.26/42.11 % (4035501)CaDiCaL version: 2.1.3 % 292.26/42.11 % (4035501)Termination reason: Instruction limit % 292.26/42.11 % (4035501)Termination phase: Saturation % 292.26/42.11 % (4035501)Time elapsed: 6.331 s % 292.26/42.11 % (4035501)Peak memory usage: 126 MB % 292.26/42.11 % (4035501)Instructions burned: 11747 (million) % 292.26/42.11 % (4035815)dis+21_20_to=lakbo:si=on:alasca=on:sp=const_max:uwa=alasca_main:sac=on:random_seed=4068892263:s2a=on:i=83971:s2at=4:bd=all:ins=1:rtra=on_2838 on theBenchmark for (2838ds/83971Mi) % 292.26/42.11 % (4035821)lrs+1011_5:1_to=lpo:sil=128000:sas=z3:si=on:norm_ineq=on:tha=some:random_seed=1402457507:i=83944:rtra=on_2836 on theBenchmark for (2836ds/83944Mi) % 292.26/42.11 % (4035327)Instruction limit reached! % 292.26/42.11 % (4035327)------------------------------ % 292.26/42.11 % (4035327)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 292.26/42.11 % (4035327)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 292.26/42.11 % (4035327)CaDiCaL version: 2.1.3 % 292.26/42.11 % (4035327)Termination reason: Instruction limit % 292.26/42.11 % (4035327)Termination phase: Saturation % 292.26/42.11 % (4035327)Time elapsed: 18.959 s % 292.26/42.11 % (4035327)Peak memory usage: 116 MB % 292.26/42.11 % (4035327)Instructions burned: 36817 (million) % 292.26/42.11 % (4035893)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=4066306127:i=9201:rtra=on_2768 on theBenchmark for (2768ds/9201Mi) % 292.26/42.11 % (4035893)Instruction limit reached! % 292.26/42.11 % (4035893)------------------------------ % 292.26/42.11 % (4035893)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 292.26/42.11 % (4035893)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 292.26/42.11 % (4035893)CaDiCaL version: 2.1.3 % 292.26/42.11 % (4035893)Termination reason: Instruction limit % 292.26/42.11 % (4035893)Termination phase: Saturation % 292.26/42.11 % (4035893)Time elapsed: 6.611 s % 292.26/42.11 % (4035893)Peak memory usage: 93 MB % 292.26/42.11 % (4035893)Instructions burned: 9202 (million) % 292.26/42.11 % (4035914)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 % 292.26/42.11 % (4035914)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=1037707168:i=6806:aac=none:nm=0:rtra=on:rawr=on_2699 on theBenchmark for (2699ds/6806Mi) % 292.26/42.11 % (4035744)Instruction limit reached! % 292.26/42.11 % (4035744)------------------------------ % 292.26/42.11 % (4035744)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 292.26/42.11 % (4035744)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 292.26/42.11 % (4035744)CaDiCaL version: 2.1.3 % 300.11/43.18 % (4035744)Termination reason: Instruction limit % 300.11/43.18 % (4035744)Termination phase: Saturation % 300.11/43.18 % (4035744)Time elapsed: 16.772 s % 300.11/43.18 % (4035744)Peak memory usage: 144 MB % 300.11/43.18 % (4035744)Instructions burned: 24001 (million) % 300.11/43.18 % (4035920)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=3815952760:s2a=on:i=3553:nm=0:rtra=on_2693 on theBenchmark for (2693ds/3553Mi) % 300.11/43.18 % (4035920)Instruction limit reached! % 300.11/43.18 % (4035920)------------------------------ % 300.11/43.18 % (4035920)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.11/43.18 % (4035920)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.11/43.18 % (4035920)CaDiCaL version: 2.1.3 % 300.11/43.18 % (4035920)Termination reason: Instruction limit % 300.11/43.18 % (4035920)Termination phase: Saturation % 300.11/43.18 % (4035920)Time elapsed: 2.463 s % 300.11/43.18 % (4035920)Peak memory usage: 97 MB % 300.11/43.18 % (4035920)Instructions burned: 3554 (million) % 300.11/43.18 % (4035932)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=3128559147:thitd=on:cond=on:i=2064:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2666 on theBenchmark for (2666ds/2064Mi) % 300.11/43.18 % (4035914)Instruction limit reached! % 300.11/43.18 % (4035914)------------------------------ % 300.11/43.18 % (4035914)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.11/43.18 % (4035914)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.11/43.18 % (4035914)CaDiCaL version: 2.1.3 % 300.11/43.18 % (4035914)Termination reason: Instruction limit % 300.11/43.18 % (4035914)Termination phase: Saturation % 300.11/43.18 % (4035914)Time elapsed: 4.918 s % 300.11/43.18 % (4035914)Peak memory usage: 125 MB % 300.11/43.18 % (4035914)Instructions burned: 6806 (million) % 300.11/43.18 % (4035932)Instruction limit reached! % 300.11/43.18 % (4035932)------------------------------ % 300.11/43.18 % (4035932)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.11/43.18 % (4035932)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.11/43.18 % (4035932)CaDiCaL version: 2.1.3 % 300.11/43.18 % (4035932)Termination reason: Instruction limit % 300.11/43.18 % (4035932)Termination phase: Saturation % 300.11/43.18 % (4035932)Time elapsed: 1.579 s % 300.11/43.18 % (4035932)Peak memory usage: 137 MB % 300.11/43.18 % (4035932)Instructions burned: 2064 (million) % 300.11/43.18 % (4035941)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=4259560719:avsq=on:i=1244:avsqr=1,16:rtra=on:rawr=on_2647 on theBenchmark for (2647ds/1244Mi) % 300.11/43.18 % (4035940)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=1191817521:cond=fast:i=20260:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2647 on theBenchmark for (2647ds/20260Mi) % 300.11/43.18 % (4035940)Refutation not found, incomplete strategy % 300.11/43.18 % (4035940)------------------------------ % 300.11/43.18 % (4035940)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.11/43.18 % (4035940)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.11/43.18 % (4035940)CaDiCaL version: 2.1.3 % 300.11/43.18 % (4035940)Termination reason: Refutation not found, incomplete strategy % 300.11/43.18 % (4035940)Time elapsed: 0.144 s % 300.11/43.18 % (4035940)Peak memory usage: 113 MB % 300.11/43.18 % (4035940)Instructions burned: 147 (million) % 300.11/43.18 % (4035694)Instruction limit reached! % 300.11/43.18 % (4035694)------------------------------ % 300.11/43.18 % (4035694)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.11/43.18 % (4035694)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.11/43.18 % (4035694)CaDiCaL version: 2.1.3 % 300.11/43.18 % (4035694)Termination reason: Instruction limit % 300.11/43.18 % (4035694)Termination phase: Saturation % 300.11/43.18 % (4035694)Time elapsed: 23.107 s % 300.11/43.18 % (4035694)Peak memory usage: 92 MB % 300.11/43.18 % (4035694)Instructions burned: 34001 (million) % 300.11/43.18 % (4035944)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=434263841:i=58261:doe=on:nm=0:rtra=on:gtg=exists_sym_2643 on theBenchmark for (2643ds/58261Mi) % 300.11/43.18 % (4035940)------------------------------ % 300.11/43.18 % (4035940)------------------------------ % 300.11/43.18 % (4035946)WARNING Broken Constraint: if demodulation_redundancy_check(ordering) % 300.11/43.18 Terminated % 300.11/43.18 % Vampire exiting % 300.11/43.18 Terminated %------------------------------------------------------------------------------