%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWW831_1 : TPTP v9.3.1. Released v7.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % Computer : n004.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:37:54 PM UTC 2026 % Result : Timeout 296.91s 42.93s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWW831_1 : TPTP v9.3.1. Released v7.0.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.09/0.22 % Computer : n004.cluster.edu % 0.09/0.22 % Model : x86_64 x86_64 % 0.09/0.22 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.22 % Memory : 8046.5625MB % 0.09/0.22 % OS : Linux 6.8.0-71-generic % 0.09/0.22 % CPULimit : 300 % 0.09/0.22 % WCLimit : 300 % 0.09/0.22 % DateTime : Mon Sep 28 14:31:07 UTC 2026 % 0.09/0.23 % CPUTime : % 0.09/0.23 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.09/0.28 Running first-order theorem proving % 0.09/0.28 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 5.12/1.82 % (394941)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule. % 5.12/1.82 % (394951)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=3079029056:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi) % 5.12/1.82 % (394950)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=431920087:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi) % 5.12/1.82 % (394950)Instruction limit reached! % 5.12/1.82 % (394950)------------------------------ % 5.12/1.82 % (394950)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.12/1.82 % (394950)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.12/1.82 % (394950)CaDiCaL version: 2.1.3 % 5.12/1.82 % (394950)Termination reason: Instruction limit % 5.12/1.82 % (394950)Termination phase: Property scanning % 5.12/1.82 % (394950)Time elapsed: 0.004 s % 5.12/1.82 % (394950)Peak memory usage: 86 MB % 5.12/1.82 % (394950)Instructions burned: 4 (million) % 5.12/1.82 % (394951)Instruction limit reached! % 5.12/1.82 % (394951)------------------------------ % 5.12/1.82 % (394951)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.12/1.82 % (394951)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.12/1.82 % (394951)CaDiCaL version: 2.1.3 % 5.12/1.82 % (394951)Termination reason: Instruction limit % 5.12/1.82 % (394951)Termination phase: Property scanning % 5.12/1.82 % (394951)Time elapsed: 0.014 s % 5.12/1.82 % (394951)Peak memory usage: 88 MB % 5.12/1.82 % (394951)Instructions burned: 48 (million) % 5.12/1.82 % (394946)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=1607213194:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi) % 5.12/1.82 % (394948)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=1111640391:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi) % 5.12/1.82 % (394947)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=1660311103:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi) % 5.12/1.82 % (394946)Instruction limit reached! % 5.12/1.82 % (394946)------------------------------ % 5.12/1.82 % (394946)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.12/1.82 % (394946)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.12/1.82 % (394946)CaDiCaL version: 2.1.3 % 5.12/1.82 % (394949)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=2262676585:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi) % 5.12/1.82 % (394946)Termination reason: Instruction limit % 5.12/1.82 % (394946)Termination phase: Property scanning % 5.12/1.82 % (394946)Time elapsed: 0.011 s % 5.12/1.82 % (394946)Peak memory usage: 85 MB % 5.12/1.82 % (394946)Instructions burned: 12 (million) % 5.12/1.82 % (394949)Instruction limit reached! % 5.12/1.82 % (394949)------------------------------ % 5.12/1.82 % (394949)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.12/1.82 % (394949)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.12/1.82 % (394949)CaDiCaL version: 2.1.3 % 5.12/1.82 % (394949)Termination reason: Instruction limit % 5.12/1.82 % (394949)Termination phase: Property scanning % 5.12/1.82 % (394949)Time elapsed: 0.008 s % 5.12/1.82 % (394949)Peak memory usage: 86 MB % 5.12/1.82 % (394949)Instructions burned: 9 (million) % 5.12/1.82 % (394952)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=2613755847:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi) % 5.12/1.82 % (394952)Instruction limit reached! % 5.12/1.82 % (394952)------------------------------ % 5.12/1.82 % (394952)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.12/1.82 % (394952)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.12/1.82 % (394952)CaDiCaL version: 2.1.3 % 5.12/1.82 % (394952)Termination reason: Instruction limit % 5.12/1.82 % (394952)Termination phase: Preprocessing 3 % 5.12/1.82 % (394952)Time elapsed: 0.031 s % 5.12/1.82 % (394952)Peak memory usage: 87 MB % 5.12/1.82 % (394952)Instructions burned: 33 (million) % 5.12/1.82 % (394955)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=4156981027:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2997 on theBenchmark for (2997ds/14Mi) % 5.12/1.82 % (394955)Instruction limit reached! % 5.12/1.82 % (394955)------------------------------ % 5.12/1.82 % (394955)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.36/2.09 % (394955)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.36/2.09 % (394955)CaDiCaL version: 2.1.3 % 8.36/2.09 % (394955)Termination reason: Instruction limit % 8.36/2.09 % (394955)Termination phase: Saturation % 8.36/2.09 % (394955)Time elapsed: 0.014 s % 8.36/2.09 % (394955)Peak memory usage: 86 MB % 8.36/2.09 % (394955)Instructions burned: 15 (million) % 8.36/2.09 % (394961)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=3236395307:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2997 on theBenchmark for (2997ds/16Mi) % 8.36/2.09 % (394956)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=373988866:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2997 on theBenchmark for (2997ds/29Mi) % 8.36/2.09 % (394961)Instruction limit reached! % 8.36/2.09 % (394961)------------------------------ % 8.36/2.09 % (394961)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.36/2.09 % (394961)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.36/2.09 % (394961)CaDiCaL version: 2.1.3 % 8.36/2.09 % (394961)Termination reason: Instruction limit % 8.36/2.09 % (394961)Termination phase: Preprocessing 3 % 8.36/2.09 % (394961)Time elapsed: 0.008 s % 8.36/2.09 % (394961)Peak memory usage: 86 MB % 8.36/2.09 % (394961)Instructions burned: 17 (million) % 8.36/2.09 % (394948)Instruction limit reached! % 8.36/2.09 % (394948)------------------------------ % 8.36/2.09 % (394948)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.36/2.09 % (394948)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.36/2.09 % (394948)CaDiCaL version: 2.1.3 % 8.36/2.09 % (394948)Termination reason: Instruction limit % 8.36/2.09 % (394948)Termination phase: Saturation % 8.36/2.09 % (394948)Time elapsed: 0.215 s % 8.36/2.09 % (394948)Peak memory usage: 118 MB % 8.36/2.09 % (394948)Instructions burned: 201 (million) % 8.36/2.09 % (394956)Instruction limit reached! % 8.36/2.09 % (394956)------------------------------ % 8.36/2.09 % (394956)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.36/2.09 % (394956)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.36/2.09 % (394956)CaDiCaL version: 2.1.3 % 8.36/2.09 % (394956)Termination reason: Instruction limit % 8.36/2.09 % (394956)Termination phase: Preprocessing 3 % 8.36/2.09 % (394956)Time elapsed: 0.027 s % 8.36/2.09 % (394956)Peak memory usage: 87 MB % 8.36/2.09 % (394956)Instructions burned: 29 (million) % 8.36/2.09 % (394962)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=2416146855:i=24:canc=force:rtra=on_2996 on theBenchmark for (2996ds/24Mi) % 8.36/2.09 % (394962)Instruction limit reached! % 8.36/2.09 % (394962)------------------------------ % 8.36/2.09 % (394962)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.36/2.09 % (394962)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.36/2.09 % (394962)CaDiCaL version: 2.1.3 % 8.36/2.09 % (394962)Termination reason: Instruction limit % 8.36/2.09 % (394962)Termination phase: Preprocessing 1 % 8.36/2.09 % (394962)Time elapsed: 0.022 s % 8.36/2.09 % (394962)Peak memory usage: 86 MB % 8.36/2.09 % (394962)Instructions burned: 24 (million) % 8.36/2.09 % (394947)Instruction limit reached! % 8.36/2.09 % (394947)------------------------------ % 8.36/2.09 % (394947)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.36/2.09 % (394947)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.36/2.09 % (394947)CaDiCaL version: 2.1.3 % 8.36/2.09 % (394947)Termination reason: Instruction limit % 8.36/2.09 % (394947)Termination phase: Saturation % 8.36/2.09 % (394947)Time elapsed: 0.325 s % 8.36/2.09 % (394947)Peak memory usage: 119 MB % 8.36/2.09 % (394947)Instructions burned: 307 (million) % 8.36/2.09 % (394964)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=2992254417:i=27:canc=cautious:fsr=off:rtra=on_2996 on theBenchmark for (2996ds/27Mi) % 8.36/2.09 % (394964)Instruction limit reached! % 8.36/2.09 % (394964)------------------------------ % 8.36/2.09 % (394964)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.36/2.09 % (394964)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.36/2.09 % (394964)CaDiCaL version: 2.1.3 % 8.36/2.09 % (394964)Termination reason: Instruction limit % 8.76/2.35 % (394964)Termination phase: Preprocessing 3 % 8.76/2.35 % (394964)Time elapsed: 0.026 s % 8.76/2.35 % (394964)Peak memory usage: 87 MB % 8.76/2.35 % (394964)Instructions burned: 28 (million) % 8.76/2.35 % (394966)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=1815156810:i=85:gtgl=4:rtra=on:gtg=exists_sym_2995 on theBenchmark for (2995ds/85Mi) % 8.76/2.35 % (394969)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=1009617184:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2995 on theBenchmark for (2995ds/2Mi) % 8.76/2.35 % (394969)Instruction limit reached! % 8.76/2.35 % (394969)------------------------------ % 8.76/2.35 % (394969)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.76/2.35 % (394969)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.76/2.35 % (394969)CaDiCaL version: 2.1.3 % 8.76/2.35 % (394969)Termination reason: Instruction limit % 8.76/2.35 % (394969)Termination phase: Property scanning % 8.76/2.35 % (394969)Time elapsed: 0.002 s % 8.76/2.35 % (394969)Peak memory usage: 86 MB % 8.76/2.35 % (394969)Instructions burned: 3 (million) % 8.76/2.35 % (394971)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=1463628989:i=4:ep=RST:ins=2:rtra=on_2994 on theBenchmark for (2994ds/4Mi) % 8.76/2.35 % (394971)Instruction limit reached! % 8.76/2.35 % (394971)------------------------------ % 8.76/2.35 % (394971)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.76/2.35 % (394971)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.76/2.35 % (394971)CaDiCaL version: 2.1.3 % 8.76/2.35 % (394971)Termination reason: Instruction limit % 8.76/2.35 % (394971)Termination phase: Property scanning % 8.76/2.35 % (394971)Time elapsed: 0.003 s % 8.76/2.35 % (394971)Peak memory usage: 85 MB % 8.76/2.35 % (394971)Instructions burned: 6 (million) % 8.76/2.35 % (394966)Instruction limit reached! % 8.76/2.35 % (394966)------------------------------ % 8.76/2.35 % (394966)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.76/2.35 % (394966)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.76/2.35 % (394966)CaDiCaL version: 2.1.3 % 8.76/2.35 % (394966)Termination reason: Instruction limit % 8.76/2.35 % (394966)Termination phase: Saturation % 8.76/2.35 % (394966)Time elapsed: 0.075 s % 8.76/2.35 % (394966)Peak memory usage: 88 MB % 8.76/2.35 % (394966)Instructions burned: 86 (million) % 8.76/2.35 % (394970)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=1761363724:i=181:rtra=on:ss=axioms:ev=cautious_2994 on theBenchmark for (2994ds/181Mi) % 8.76/2.35 % (394970)Refutation not found, incomplete strategy % 8.76/2.35 % (394970)------------------------------ % 8.76/2.35 % (394970)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.76/2.35 % (394970)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.76/2.35 % (394970)CaDiCaL version: 2.1.3 % 8.76/2.35 % (394970)Termination reason: Refutation not found, incomplete strategy % 8.76/2.35 % (394970)Time elapsed: 0.015 s % 8.76/2.35 % (394970)Peak memory usage: 88 MB % 8.76/2.35 % (394970)Instructions burned: 15 (million) % 8.76/2.35 % (394973)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=846776560:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2994 on theBenchmark for (2994ds/66Mi) % 8.76/2.35 % (394975)lrs+10_1_thi=all:si=on:fd=off:random_seed=2084003390:i=53:rtra=on:gtg=all_2993 on theBenchmark for (2993ds/53Mi) % 8.76/2.35 % (394981)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=61682603:i=2:doe=on:canc=force:asg=cautious:rtra=on_2993 on theBenchmark for (2993ds/2Mi) % 8.76/2.35 % (394981)Instruction limit reached! % 8.76/2.35 % (394981)------------------------------ % 8.76/2.35 % (394981)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.76/2.35 % (394981)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.76/2.35 % (394981)CaDiCaL version: 2.1.3 % 8.76/2.35 % (394981)Termination reason: Instruction limit % 8.76/2.35 % (394981)Termination phase: Property scanning % 8.76/2.35 % (394981)Time elapsed: 0.002 s % 8.76/2.35 % (394981)Peak memory usage: 86 MB % 8.76/2.35 % (394981)Instructions burned: 3 (million) % 8.76/2.35 % (394976)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=3391046184:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2993 on theBenchmark for (2993ds/8Mi) % 10.32/2.66 % (394979)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=1942808857:st=3:i=2:rtra=on:ss=axioms_2993 on theBenchmark for (2993ds/2Mi) % 10.32/2.66 % (394979)Instruction limit reached! % 10.32/2.66 % (394979)------------------------------ % 10.32/2.66 % (394979)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.32/2.66 % (394979)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.32/2.66 % (394979)CaDiCaL version: 2.1.3 % 10.32/2.66 % (394979)Termination reason: Instruction limit % 10.32/2.66 % (394979)Termination phase: Property scanning % 10.32/2.66 % (394979)Time elapsed: 0.004 s % 10.32/2.66 % (394979)Peak memory usage: 86 MB % 10.32/2.66 % (394979)Instructions burned: 3 (million) % 10.32/2.66 % (394973)Instruction limit reached! % 10.32/2.66 % (394973)------------------------------ % 10.32/2.66 % (394973)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.32/2.66 % (394973)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.32/2.66 % (394973)CaDiCaL version: 2.1.3 % 10.32/2.66 % (394973)Termination reason: Instruction limit % 10.32/2.66 % (394973)Termination phase: Saturation % 10.32/2.66 % (394973)Time elapsed: 0.058 s % 10.32/2.66 % (394973)Peak memory usage: 88 MB % 10.32/2.66 % (394973)Instructions burned: 67 (million) % 10.32/2.66 % (394976)Instruction limit reached! % 10.32/2.66 % (394976)------------------------------ % 10.32/2.66 % (394976)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.32/2.66 % (394976)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.32/2.66 % (394976)CaDiCaL version: 2.1.3 % 10.32/2.66 % (394976)Termination reason: Instruction limit % 10.32/2.66 % (394976)Termination phase: shuffling % 10.32/2.66 % (394976)Time elapsed: 0.008 s % 10.32/2.66 % (394976)Peak memory usage: 85 MB % 10.32/2.66 % (394976)Instructions burned: 9 (million) % 10.32/2.66 % (394975)Instruction limit reached! % 10.32/2.66 % (394975)------------------------------ % 10.32/2.66 % (394975)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.32/2.66 % (394975)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.32/2.66 % (394975)CaDiCaL version: 2.1.3 % 10.32/2.66 % (394975)Termination reason: Instruction limit % 10.32/2.66 % (394975)Termination phase: Preprocessing 3 % 10.32/2.66 % (394975)Time elapsed: 0.047 s % 10.32/2.66 % (394975)Peak memory usage: 87 MB % 10.32/2.66 % (394975)Instructions burned: 54 (million) % 10.32/2.66 % (394982)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=94725025:i=127:doe=on:rtra=on_2992 on theBenchmark for (2992ds/127Mi) % 10.32/2.66 % (394982)Instruction limit reached! % 10.32/2.66 % (394982)------------------------------ % 10.32/2.66 % (394982)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.32/2.66 % (394982)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.32/2.66 % (394982)CaDiCaL version: 2.1.3 % 10.32/2.66 % (394982)Termination reason: Instruction limit % 10.32/2.66 % (394982)Termination phase: Saturation % 10.32/2.66 % (394982)Time elapsed: 0.154 s % 10.32/2.66 % (394982)Peak memory usage: 118 MB % 10.32/2.66 % (394982)Instructions burned: 127 (million) % 10.32/2.66 % (394994)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=4271696877:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2990 on theBenchmark for (2990ds/8Mi) % 10.32/2.66 % (394994)Instruction limit reached! % 10.32/2.66 % (394994)------------------------------ % 10.32/2.66 % (394994)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.32/2.66 % (394994)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.32/2.66 % (394994)CaDiCaL version: 2.1.3 % 10.32/2.66 % (394994)Termination reason: Instruction limit % 10.32/2.66 % (394994)Termination phase: Property scanning % 10.32/2.66 % (394994)Time elapsed: 0.009 s % 10.32/2.66 % (394994)Peak memory usage: 85 MB % 10.32/2.66 % (394994)Instructions burned: 9 (million) % 10.32/2.66 % (394990)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=878749376:i=26:canc=cautious:av=off:rtra=on_2990 on theBenchmark for (2990ds/26Mi) % 10.32/2.66 % (394970)------------------------------ % 10.32/2.66 % (394970)------------------------------ % 10.32/2.66 % (394991)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=4054182775: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_2990 on theBenchmark for (2990ds/35Mi) % 10.32/2.66 % (394989)dis+10_1_si=on:random_seed=1364056987:i=10:ep=R:rtra=on_2990 on theBenchmark for (2990ds/10Mi) % 15.29/3.12 % (394992)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=3058695867:i=2:fsr=off:rtra=on:inst=on_2990 on theBenchmark for (2990ds/2Mi) % 15.29/3.12 % (394992)Instruction limit reached! % 15.29/3.12 % (394992)------------------------------ % 15.29/3.12 % (394992)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.29/3.12 % (394992)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.29/3.12 % (394992)CaDiCaL version: 2.1.3 % 15.29/3.12 % (394992)Termination reason: Instruction limit % 15.29/3.12 % (394992)Termination phase: shuffling % 15.29/3.12 % (394992)Time elapsed: 0.003 s % 15.29/3.12 % (394992)Peak memory usage: 85 MB % 15.29/3.12 % (394992)Instructions burned: 2 (million) % 15.29/3.12 % (394990)Instruction limit reached! % 15.29/3.12 % (394990)------------------------------ % 15.29/3.12 % (394990)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.29/3.12 % (394990)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.29/3.12 % (394990)CaDiCaL version: 2.1.3 % 15.29/3.12 % (394990)Termination reason: Instruction limit % 15.29/3.12 % (394990)Termination phase: Preprocessing 3 % 15.29/3.12 % (394990)Time elapsed: 0.013 s % 15.29/3.12 % (394990)Peak memory usage: 87 MB % 15.29/3.12 % (394990)Instructions burned: 26 (million) % 15.29/3.12 % (394989)Instruction limit reached! % 15.29/3.12 % (394989)------------------------------ % 15.29/3.12 % (394989)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.29/3.12 % (394989)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.29/3.12 % (394989)CaDiCaL version: 2.1.3 % 15.29/3.12 % (394989)Termination reason: Instruction limit % 15.29/3.12 % (394989)Termination phase: Property scanning % 15.29/3.12 % (394989)Time elapsed: 0.011 s % 15.29/3.12 % (394989)Peak memory usage: 86 MB % 15.29/3.12 % (394989)Instructions burned: 12 (million) % 15.29/3.12 % (394991)Instruction limit reached! % 15.29/3.12 % (394991)------------------------------ % 15.29/3.12 % (394991)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.29/3.12 % (394991)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.29/3.12 % (394991)CaDiCaL version: 2.1.3 % 15.29/3.12 % (394991)Termination reason: Instruction limit % 15.29/3.12 % (394991)Termination phase: Preprocessing 3 % 15.29/3.12 % (394991)Time elapsed: 0.032 s % 15.29/3.12 % (394991)Peak memory usage: 87 MB % 15.29/3.12 % (394991)Instructions burned: 35 (million) % 15.29/3.12 % (394995)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=2918487745:i=370:ep=RS:fsr=off:rtra=on_2989 on theBenchmark for (2989ds/370Mi) % 15.29/3.12 % (395005)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=995878928:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2988 on theBenchmark for (2988ds/75Mi) % 15.29/3.12 % (394997)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=1600258937:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2988 on theBenchmark for (2988ds/13Mi) % 15.29/3.12 % (394997)Instruction limit reached! % 15.29/3.12 % (394997)------------------------------ % 15.29/3.12 % (394997)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.29/3.12 % (394997)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.29/3.12 % (394997)CaDiCaL version: 2.1.3 % 15.29/3.12 % (394997)Termination reason: Instruction limit % 15.29/3.12 % (394997)Termination phase: Property scanning % 15.29/3.12 % (394997)Time elapsed: 0.012 s % 15.29/3.12 % (394997)Peak memory usage: 85 MB % 15.29/3.12 % (394997)Instructions burned: 13 (million) % 15.29/3.12 % (395005)Instruction limit reached! % 15.29/3.12 % (395005)------------------------------ % 15.29/3.12 % (395005)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.29/3.12 % (395005)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.29/3.12 % (395005)CaDiCaL version: 2.1.3 % 15.29/3.12 % (395005)Termination reason: Instruction limit % 15.29/3.12 % (395005)Termination phase: Saturation % 15.29/3.12 % (395005)Time elapsed: 0.042 s % 15.29/3.12 % (395005)Peak memory usage: 90 MB % 15.29/3.12 % (395005)Instructions burned: 76 (million) % 15.29/3.12 % (395004)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=1681549509:i=71:rtra=on:gtg=exists_top_2988 on theBenchmark for (2988ds/71Mi) % 15.29/3.12 % (395002)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=737429734:i=226:rtra=on:gtg=position:ss=axioms_2988 on theBenchmark for (2988ds/226Mi) % 16.90/3.47 % (395003)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=2422522243:i=10:rtra=on_2988 on theBenchmark for (2988ds/10Mi) % 16.90/3.47 % (395003)Instruction limit reached! % 16.90/3.47 % (395003)------------------------------ % 16.90/3.47 % (395003)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.90/3.47 % (395003)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.90/3.47 % (395003)CaDiCaL version: 2.1.3 % 16.90/3.47 % (395003)Termination reason: Instruction limit % 16.90/3.47 % (395003)Termination phase: Property scanning % 16.90/3.47 % (395003)Time elapsed: 0.009 s % 16.90/3.47 % (395003)Peak memory usage: 85 MB % 16.90/3.47 % (395003)Instructions burned: 10 (million) % 16.90/3.47 % (395007)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=1393647932:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2987 on theBenchmark for (2987ds/294Mi) % 16.90/3.47 % (395002)Refutation not found, incomplete strategy % 16.90/3.47 % (395002)------------------------------ % 16.90/3.47 % (395002)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.90/3.47 % (395002)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.90/3.47 % (395002)CaDiCaL version: 2.1.3 % 16.90/3.47 % (395002)Termination reason: Refutation not found, incomplete strategy % 16.90/3.47 % (395002)Time elapsed: 0.055 s % 16.90/3.47 % (395002)Peak memory usage: 111 MB % 16.90/3.47 % (395002)Instructions burned: 28 (million) % 16.90/3.47 % (395004)Instruction limit reached! % 16.90/3.47 % (395004)------------------------------ % 16.90/3.47 % (395004)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.90/3.47 % (395004)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.90/3.47 % (395004)CaDiCaL version: 2.1.3 % 16.90/3.47 % (395004)Termination reason: Instruction limit % 16.90/3.47 % (395004)Termination phase: Property scanning % 16.90/3.47 % (395004)Time elapsed: 0.063 s % 16.90/3.47 % (395004)Peak memory usage: 88 MB % 16.90/3.47 % (395004)Instructions burned: 72 (million) % 16.90/3.47 % (395012)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=1878904709:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2986 on theBenchmark for (2986ds/130Mi) % 16.90/3.47 % (395013)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=2377601741:i=131:rtra=on_2986 on theBenchmark for (2986ds/131Mi) % 16.90/3.47 % (394995)Instruction limit reached! % 16.90/3.47 % (394995)------------------------------ % 16.90/3.47 % (394995)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.90/3.47 % (394995)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.90/3.47 % (394995)CaDiCaL version: 2.1.3 % 16.90/3.47 % (394995)Termination reason: Instruction limit % 16.90/3.47 % (394995)Termination phase: Saturation % 16.90/3.47 % (394995)Time elapsed: 0.277 s % 16.90/3.47 % (394995)Peak memory usage: 91 MB % 16.90/3.47 % (394995)Instructions burned: 371 (million) % 16.90/3.47 % (395013)Instruction limit reached! % 16.90/3.47 % (395013)------------------------------ % 16.90/3.47 % (395013)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.90/3.47 % (395013)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.90/3.47 % (395013)CaDiCaL version: 2.1.3 % 16.90/3.47 % (395013)Termination reason: Instruction limit % 16.90/3.47 % (395013)Termination phase: Saturation % 16.90/3.47 % (395013)Time elapsed: 0.103 s % 16.90/3.47 % (395013)Peak memory usage: 135 MB % 16.90/3.47 % (395013)Instructions burned: 132 (million) % 16.90/3.47 % (395017)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=816121075:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2985 on theBenchmark for (2985ds/40Mi) % 16.90/3.47 % (395012)Instruction limit reached! % 16.90/3.47 % (395012)------------------------------ % 16.90/3.47 % (395012)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.90/3.47 % (395012)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.90/3.47 % (395012)CaDiCaL version: 2.1.3 % 16.90/3.47 % (395012)Termination reason: Instruction limit % 16.90/3.47 % (395012)Termination phase: Saturation % 16.90/3.47 % (395012)Time elapsed: 0.160 s % 16.90/3.47 % (395012)Peak memory usage: 118 MB % 16.90/3.47 % (395012)Instructions burned: 130 (million) % 22.38/4.11 % (395017)Instruction limit reached! % 22.38/4.11 % (395017)------------------------------ % 22.38/4.11 % (395017)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 22.38/4.11 % (395017)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.38/4.11 % (395017)CaDiCaL version: 2.1.3 % 22.38/4.11 % (395017)Termination reason: Instruction limit % 22.38/4.11 % (395017)Termination phase: Preprocessing 1 % 22.38/4.11 % (395017)Time elapsed: 0.035 s % 22.38/4.11 % (395017)Peak memory usage: 86 MB % 22.38/4.11 % (395017)Instructions burned: 41 (million) % 22.38/4.11 % (395007)Instruction limit reached! % 22.38/4.11 % (395007)------------------------------ % 22.38/4.11 % (395007)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 22.38/4.11 % (395007)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.38/4.11 % (395007)CaDiCaL version: 2.1.3 % 22.38/4.11 % (395007)Termination reason: Instruction limit % 22.38/4.11 % (395007)Termination phase: Saturation % 22.38/4.11 % (395007)Time elapsed: 0.297 s % 22.38/4.11 % (395007)Peak memory usage: 92 MB % 22.38/4.11 % (395007)Instructions burned: 295 (million) % 22.38/4.11 % (395019)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=14504415:i=307:rtra=on:gtg=exists_top_2985 on theBenchmark for (2985ds/307Mi) % 22.38/4.11 % (395022)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=4139288846:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2983 on theBenchmark for (2983ds/598Mi) % 22.38/4.11 % (395002)------------------------------ % 22.38/4.11 % (395002)------------------------------ % 22.38/4.11 % (395027)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=1968547582:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2982 on theBenchmark for (2982ds/259Mi) % 22.38/4.11 % (395024)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=425219512:i=131:canc=cautious:fsr=off:rtra=on_2982 on theBenchmark for (2982ds/131Mi) % 22.38/4.11 % (395027)Refutation not found, incomplete strategy % 22.38/4.11 % (395027)------------------------------ % 22.38/4.11 % (395027)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 22.38/4.11 % (395027)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.38/4.11 % (395027)CaDiCaL version: 2.1.3 % 22.38/4.11 % (395027)Termination reason: Refutation not found, incomplete strategy % 22.38/4.11 % (395027)Time elapsed: 0.054 s % 22.38/4.11 % (395027)Peak memory usage: 112 MB % 22.38/4.11 % (395027)Instructions burned: 30 (million) % 22.38/4.11 % (395028)dis+10_1_si=on:random_seed=1425717502:s2a=on:i=1000:rtra=on:gtg=exists_all_2982 on theBenchmark for (2982ds/1000Mi) % 22.38/4.11 % (395029)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=921769626:i=383:fsr=off:rtra=on:ev=force_2982 on theBenchmark for (2982ds/383Mi) % 22.38/4.11 % (395019)Instruction limit reached! % 22.38/4.11 % (395019)------------------------------ % 22.38/4.11 % (395019)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 22.38/4.11 % (395019)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.38/4.11 % (395019)CaDiCaL version: 2.1.3 % 22.38/4.11 % (395019)Termination reason: Instruction limit % 22.38/4.11 % (395019)Termination phase: Saturation % 22.38/4.11 % (395019)Time elapsed: 0.279 s % 22.38/4.11 % (395019)Peak memory usage: 92 MB % 22.38/4.11 % (395019)Instructions burned: 307 (million) % 22.38/4.11 % (395024)Instruction limit reached! % 22.38/4.11 % (395024)------------------------------ % 22.38/4.11 % (395024)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 22.38/4.11 % (395024)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.38/4.11 % (395024)CaDiCaL version: 2.1.3 % 22.38/4.11 % (395024)Termination reason: Instruction limit % 22.38/4.11 % (395024)Termination phase: Saturation % 22.38/4.11 % (395024)Time elapsed: 0.140 s % 22.38/4.11 % (395024)Peak memory usage: 118 MB % 22.38/4.11 % (395024)Instructions burned: 131 (million) % 22.38/4.11 % (395032)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=1002851543:i=141:doe=on:rtra=on_2981 on theBenchmark for (2981ds/141Mi) % 22.38/4.11 % (395022)Instruction limit reached! % 22.38/4.11 % (395022)------------------------------ % 22.38/4.11 % (395022)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 22.38/4.11 % (395022)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.81/4.38 % (395022)CaDiCaL version: 2.1.3 % 23.81/4.38 % (395022)Termination reason: Instruction limit % 23.81/4.38 % (395022)Termination phase: Saturation % 23.81/4.38 % (395022)Time elapsed: 0.389 s % 23.81/4.38 % (395022)Peak memory usage: 141 MB % 23.81/4.38 % (395022)Instructions burned: 600 (million) % 23.81/4.38 % (395032)Instruction limit reached! % 23.81/4.38 % (395032)------------------------------ % 23.81/4.38 % (395032)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.81/4.38 % (395032)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.81/4.38 % (395032)CaDiCaL version: 2.1.3 % 23.81/4.38 % (395032)Termination reason: Instruction limit % 23.81/4.38 % (395032)Termination phase: Saturation % 23.81/4.38 % (395032)Time elapsed: 0.137 s % 23.81/4.38 % (395032)Peak memory usage: 91 MB % 23.81/4.38 % (395032)Instructions burned: 142 (million) % 23.81/4.38 % (395027)------------------------------ % 23.81/4.38 % (395027)------------------------------ % 23.81/4.38 % (395037)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=717123032:i=65:nm=16:rtra=on_2979 on theBenchmark for (2979ds/65Mi) % 23.81/4.38 % (395038)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=1290552068:i=121:nm=16:rtra=on_2979 on theBenchmark for (2979ds/121Mi) % 23.81/4.38 % (395037)Instruction limit reached! % 23.81/4.38 % (395037)------------------------------ % 23.81/4.38 % (395037)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.81/4.38 % (395037)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.81/4.38 % (395037)CaDiCaL version: 2.1.3 % 23.81/4.38 % (395037)Termination reason: Instruction limit % 23.81/4.38 % (395037)Termination phase: Saturation % 23.81/4.38 % (395037)Time elapsed: 0.060 s % 23.81/4.38 % (395037)Peak memory usage: 89 MB % 23.81/4.38 % (395037)Instructions burned: 65 (million) % 23.81/4.38 % (395040)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=1769524084:s2a=on:i=128:s2at=5:ins=3:rtra=on_2977 on theBenchmark for (2977ds/128Mi) % 23.81/4.38 % (395029)Instruction limit reached! % 23.81/4.38 % (395029)------------------------------ % 23.81/4.38 % (395029)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.81/4.38 % (395029)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.81/4.38 % (395029)CaDiCaL version: 2.1.3 % 23.81/4.38 % (395029)Termination reason: Instruction limit % 23.81/4.38 % (395029)Termination phase: Saturation % 23.81/4.38 % (395029)Time elapsed: 0.382 s % 23.81/4.38 % (395029)Peak memory usage: 97 MB % 23.81/4.38 % (395029)Instructions burned: 383 (million) % 23.81/4.38 % (395038)Instruction limit reached! % 23.81/4.38 % (395038)------------------------------ % 23.81/4.38 % (395038)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.81/4.38 % (395038)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.81/4.38 % (395038)CaDiCaL version: 2.1.3 % 23.81/4.38 % (395038)Termination reason: Instruction limit % 23.81/4.38 % (395038)Termination phase: Saturation % 23.81/4.38 % (395038)Time elapsed: 0.116 s % 23.81/4.38 % (395038)Peak memory usage: 90 MB % 23.81/4.38 % (395038)Instructions burned: 121 (million) % 23.81/4.38 % (395040)Refutation not found, incomplete strategy % 23.81/4.38 % (395040)------------------------------ % 23.81/4.38 % (395040)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.81/4.38 % (395040)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.81/4.38 % (395040)CaDiCaL version: 2.1.3 % 23.81/4.38 % (395040)Termination reason: Refutation not found, incomplete strategy % 23.81/4.38 % (395040)Time elapsed: 0.078 s % 23.81/4.38 % (395040)Peak memory usage: 115 MB % 23.81/4.38 % (395040)Instructions burned: 117 (million) % 23.81/4.38 % (395041)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=2538269749:i=39:ins=3:rtra=on_2977 on theBenchmark for (2977ds/39Mi) % 23.81/4.38 % (395041)Instruction limit reached! % 23.81/4.38 % (395041)------------------------------ % 23.81/4.38 % (395041)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.81/4.38 % (395041)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.81/4.38 % (395041)CaDiCaL version: 2.1.3 % 23.81/4.38 % (395041)Termination reason: Instruction limit % 23.81/4.38 % (395041)Termination phase: Property scanning % 23.81/4.38 % (395041)Time elapsed: 0.036 s % 23.81/4.38 % (395041)Peak memory usage: 87 MB % 23.81/4.38 % (395041)Instructions burned: 40 (million) % 29.40/5.06 % (395045)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=1096098185:i=329:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2975 on theBenchmark for (2975ds/329Mi) % 29.40/5.06 % (395043)dis+1010_1_to=kbo:si=on:random_seed=3869243658:i=175:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2976 on theBenchmark for (2976ds/175Mi) % 29.40/5.06 % (395047)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=192755561:s2a=on:i=483:doe=on:nm=32:rtra=on_2975 on theBenchmark for (2975ds/483Mi) % 29.40/5.06 % (395040)------------------------------ % 29.40/5.06 % (395040)------------------------------ % 29.40/5.06 % (395048)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=852966038:thitd=on:i=215:nm=0:rtra=on:ev=force_2975 on theBenchmark for (2975ds/215Mi) % 29.40/5.06 % (395043)Instruction limit reached! % 29.40/5.06 % (395043)------------------------------ % 29.40/5.06 % (395043)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.40/5.06 % (395043)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.40/5.06 % (395043)CaDiCaL version: 2.1.3 % 29.40/5.06 % (395043)Termination reason: Instruction limit % 29.40/5.06 % (395043)Termination phase: Saturation % 29.40/5.06 % (395043)Time elapsed: 0.176 s % 29.40/5.06 % (395043)Peak memory usage: 91 MB % 29.40/5.06 % (395043)Instructions burned: 175 (million) % 29.40/5.06 % (395045)Instruction limit reached! % 29.40/5.06 % (395045)------------------------------ % 29.40/5.06 % (395045)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.40/5.06 % (395045)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.40/5.06 % (395045)CaDiCaL version: 2.1.3 % 29.40/5.06 % (395045)Termination reason: Instruction limit % 29.40/5.06 % (395045)Termination phase: Saturation % 29.40/5.06 % (395045)Time elapsed: 0.218 s % 29.40/5.06 % (395045)Peak memory usage: 119 MB % 29.40/5.06 % (395045)Instructions burned: 329 (million) % 29.40/5.06 % (395050)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=3672753069:i=349:rtra=on_2974 on theBenchmark for (2974ds/349Mi) % 29.40/5.06 % (395028)Instruction limit reached! % 29.40/5.06 % (395028)------------------------------ % 29.40/5.06 % (395028)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.40/5.06 % (395028)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.40/5.06 % (395028)CaDiCaL version: 2.1.3 % 29.40/5.06 % (395028)Termination reason: Instruction limit % 29.40/5.06 % (395028)Termination phase: Saturation % 29.40/5.06 % (395028)Time elapsed: 0.876 s % 29.40/5.06 % (395028)Peak memory usage: 95 MB % 29.40/5.06 % (395028)Instructions burned: 1001 (million) % 29.40/5.06 % (395054)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=962898434:st=2:i=295:rtra=on:ss=axioms_2972 on theBenchmark for (2972ds/295Mi) % 29.40/5.06 % (395054)Refutation not found, incomplete strategy % 29.40/5.06 % (395054)------------------------------ % 29.40/5.06 % (395054)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.40/5.06 % (395054)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.40/5.06 % (395054)CaDiCaL version: 2.1.3 % 29.40/5.06 % (395054)Termination reason: Refutation not found, incomplete strategy % 29.40/5.06 % (395054)Time elapsed: 0.012 s % 29.40/5.06 % (395054)Peak memory usage: 88 MB % 29.40/5.06 % (395054)Instructions burned: 25 (million) % 29.40/5.06 % (395056)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=2341469090:i=328:kws=inv_frequency:nm=20:rtra=on_2972 on theBenchmark for (2972ds/328Mi) % 29.40/5.06 % (395048)Instruction limit reached! % 29.40/5.06 % (395048)------------------------------ % 29.40/5.06 % (395048)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.40/5.06 % (395048)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.40/5.06 % (395048)CaDiCaL version: 2.1.3 % 29.40/5.06 % (395048)Termination reason: Instruction limit % 29.40/5.06 % (395048)Termination phase: Saturation % 29.40/5.06 % (395048)Time elapsed: 0.270 s % 29.40/5.06 % (395048)Peak memory usage: 139 MB % 29.40/5.06 % (395048)Instructions burned: 216 (million) % 29.40/5.06 % (395058)dis+1010_1_to=lpo:sil=128000:sas=z3:si=on:nwc=5:random_seed=1037785291:i=281:gtgl=2:rtra=on:gtg=all_2971 on theBenchmark for (2971ds/281Mi) % 29.40/5.06 % (395059)lrs+1010_1_to=kbo:sil=128000:si=on:sos=on:urr=on:uwa=alasca_main:random_seed=2445694105:i=484:doe=on:nm=0:av=off:rtra=on:ss=axioms_2970 on theBenchmark for (2970ds/484Mi) % 31.35/5.42 % (395054)------------------------------ % 31.35/5.42 % (395054)------------------------------ % 31.35/5.42 % (395050)Instruction limit reached! % 31.35/5.42 % (395050)------------------------------ % 31.35/5.42 % (395050)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.35/5.42 % (395050)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.35/5.42 % (395050)CaDiCaL version: 2.1.3 % 31.35/5.42 % (395050)Termination reason: Instruction limit % 31.35/5.42 % (395050)Termination phase: Saturation % 31.35/5.42 % (395050)Time elapsed: 0.378 s % 31.35/5.42 % (395050)Peak memory usage: 120 MB % 31.35/5.42 % (395050)Instructions burned: 349 (million) % 31.35/5.42 % (395059)Refutation not found, incomplete strategy % 31.35/5.42 % (395059)------------------------------ % 31.35/5.42 % (395059)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.35/5.42 % (395059)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.35/5.42 % (395059)CaDiCaL version: 2.1.3 % 31.35/5.42 % (395059)Termination reason: Refutation not found, incomplete strategy % 31.35/5.42 % (395059)Time elapsed: 0.022 s % 31.35/5.42 % (395059)Peak memory usage: 88 MB % 31.35/5.42 % (395059)Instructions burned: 24 (million) % 31.35/5.42 % (395047)Instruction limit reached! % 31.35/5.42 % (395047)------------------------------ % 31.35/5.42 % (395047)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.35/5.42 % (395047)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.35/5.42 % (395047)CaDiCaL version: 2.1.3 % 31.35/5.42 % (395047)Termination reason: Instruction limit % 31.35/5.42 % (395047)Termination phase: Saturation % 31.35/5.42 % (395047)Time elapsed: 0.529 s % 31.35/5.42 % (395047)Peak memory usage: 137 MB % 31.35/5.42 % (395047)Instructions burned: 484 (million) % 31.35/5.42 % (395062)lrs+21_1_to=kbo:sil=128000:thi=neg_eq:si=on:random_seed=4211261022:i=321:canc=force:rtra=on:tac=axiom:ss=axioms:ev=force_2969 on theBenchmark for (2969ds/321Mi) % 31.35/5.42 % (395062)Refutation not found, incomplete strategy % 31.35/5.42 % (395062)------------------------------ % 31.35/5.42 % (395062)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.35/5.42 % (395062)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.35/5.42 % (395062)CaDiCaL version: 2.1.3 % 31.35/5.42 % (395062)Termination reason: Refutation not found, incomplete strategy % 31.35/5.42 % (395062)Time elapsed: 0.059 s % 31.35/5.42 % (395062)Peak memory usage: 112 MB % 31.35/5.42 % (395062)Instructions burned: 29 (million) % 31.35/5.42 % (395056)Instruction limit reached! % 31.35/5.42 % (395056)------------------------------ % 31.35/5.42 % (395056)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.35/5.42 % (395056)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.35/5.42 % (395056)CaDiCaL version: 2.1.3 % 31.35/5.42 % (395056)Termination reason: Instruction limit % 31.35/5.42 % (395056)Termination phase: Saturation % 31.35/5.42 % (395056)Time elapsed: 0.365 s % 31.35/5.42 % (395056)Peak memory usage: 119 MB % 31.35/5.42 % (395056)Instructions burned: 328 (million) % 31.35/5.42 % (395058)Instruction limit reached! % 31.35/5.42 % (395058)------------------------------ % 31.35/5.42 % (395058)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.35/5.42 % (395058)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.35/5.42 % (395058)CaDiCaL version: 2.1.3 % 31.35/5.42 % (395058)Termination reason: Instruction limit % 31.35/5.42 % (395058)Termination phase: Saturation % 31.35/5.42 % (395058)Time elapsed: 0.287 s % 31.35/5.42 % (395058)Peak memory usage: 118 MB % 31.35/5.42 % (395058)Instructions burned: 285 (million) % 31.35/5.42 % (395065)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=1807959192:i=416:rtra=on:gtg=position:ss=axioms_2968 on theBenchmark for (2968ds/416Mi) % 31.35/5.42 % (395065)Refutation not found, incomplete strategy % 31.35/5.42 % (395065)------------------------------ % 31.35/5.42 % (395065)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.35/5.42 % (395065)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.35/5.42 % (395065)CaDiCaL version: 2.1.3 % 31.35/5.42 % (395065)Termination reason: Refutation not found, incomplete strategy % 31.35/5.42 % (395065)Time elapsed: 0.033 s % 31.35/5.42 % (395065)Peak memory usage: 111 MB % 31.35/5.42 % (395065)Instructions burned: 28 (million) % 36.45/6.11 % (395067)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=2434189594:avsq=on:i=276:avsqr=1,2:rtra=on_2967 on theBenchmark for (2967ds/276Mi) % 36.45/6.11 % (395066)lrs+1010_1_to=kbo:tgt=ground:fde=unused:sas=z3:si=on:sp=unary_frequency:gve=force:spb=goal:tha=off:random_seed=1789884399:i=471:thf=on:kws=precedence:rtra=on_2967 on theBenchmark for (2967ds/471Mi) % 36.45/6.11 % (395059)------------------------------ % 36.45/6.11 % (395059)------------------------------ % 36.45/6.11 % (395069)lrs+1010_2_to=kbo:sil=128000:tgt=ground:fde=unused:sas=z3:si=on:uwa=off:tha=off:nwc=1:random_seed=1138903653:i=375:kws=inv_arity_squared:rtra=on_2966 on theBenchmark for (2966ds/375Mi) % 36.45/6.11 % (395065)------------------------------ % 36.45/6.11 % (395065)------------------------------ % 36.45/6.11 % (395070)lrs+10_1_to=kbo:sil=128000:tgt=full:sas=z3:si=on:uwa=func_ext:slsqc=1:flr=on:slsq=on:random_seed=910882961:i=387:bd=preordered:rtra=on:ss=axioms:sgt=8_2965 on theBenchmark for (2965ds/387Mi) % 36.45/6.11 % (395070)Refutation not found, incomplete strategy % 36.45/6.11 % (395070)------------------------------ % 36.45/6.11 % (395070)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 36.45/6.11 % (395070)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.45/6.11 % (395070)CaDiCaL version: 2.1.3 % 36.45/6.11 % (395070)Termination reason: Refutation not found, incomplete strategy % 36.45/6.11 % (395070)Time elapsed: 0.060 s % 36.45/6.11 % (395070)Peak memory usage: 112 MB % 36.45/6.11 % (395070)Instructions burned: 31 (million) % 36.45/6.11 % (395062)------------------------------ % 36.45/6.11 % (395062)------------------------------ % 36.45/6.11 % (395075)lrs+10_1_to=kbo:sil=128000:fde=none:si=on:norm_ineq=on:urr=on:nwc=0.5:random_seed=2614354435:i=513:kws=frequency:bd=all:rtra=on:gtg=exists_all:ss=axioms:sgt=4_2963 on theBenchmark for (2963ds/513Mi) % 36.45/6.11 % (395067)Instruction limit reached! % 36.45/6.11 % (395067)------------------------------ % 36.45/6.11 % (395067)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 36.45/6.11 % (395067)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.45/6.11 % (395067)CaDiCaL version: 2.1.3 % 36.45/6.11 % (395067)Termination reason: Instruction limit % 36.45/6.11 % (395067)Termination phase: Saturation % 36.45/6.11 % (395067)Time elapsed: 0.339 s % 36.45/6.11 % (395067)Peak memory usage: 136 MB % 36.45/6.11 % (395067)Instructions burned: 276 (million) % 36.45/6.11 % (395077)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=130012891:i=334:rtra=on_2963 on theBenchmark for (2963ds/334Mi) % 36.45/6.11 % (395069)Instruction limit reached! % 36.45/6.11 % (395069)------------------------------ % 36.45/6.11 % (395069)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 36.45/6.11 % (395069)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.45/6.11 % (395069)CaDiCaL version: 2.1.3 % 36.45/6.11 % (395069)Termination reason: Instruction limit % 36.45/6.11 % (395069)Termination phase: Saturation % 36.45/6.11 % (395069)Time elapsed: 0.397 s % 36.45/6.11 % (395069)Peak memory usage: 120 MB % 36.45/6.11 % (395069)Instructions burned: 375 (million) % 36.45/6.11 % (395066)Instruction limit reached! % 36.45/6.11 % (395066)------------------------------ % 36.45/6.11 % (395066)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 36.45/6.11 % (395066)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.45/6.11 % (395066)CaDiCaL version: 2.1.3 % 36.45/6.11 % (395066)Termination reason: Instruction limit % 36.45/6.11 % (395066)Termination phase: Saturation % 36.45/6.11 % (395066)Time elapsed: 0.507 s % 36.45/6.11 % (395066)Peak memory usage: 121 MB % 36.45/6.11 % (395066)Instructions burned: 471 (million) % 36.45/6.11 % (395078)lrs+1010_1_to=kbo:sil=64000:sas=cadical:si=on:sos=on:bce=on:random_seed=3398821621:i=359:rtra=on:gtg=exists_top:ss=axioms_2962 on theBenchmark for (2962ds/359Mi) % 36.45/6.11 % (395081)dis+1010_1_to=lpo:sil=128000:thi=all:fde=unused:si=on:sp=reverse_arity:tha=off:random_seed=3702052098:i=341:gtgl=2:rtra=on:gtg=exists_sym:ev=force:fsd=on:fsdmm=1_2961 on theBenchmark for (2961ds/341Mi) % 36.45/6.11 % (395077)Instruction limit reached! % 36.45/6.11 % (395077)------------------------------ % 36.45/6.11 % (395077)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 36.45/6.11 % (395077)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.55/6.80 % (395077)CaDiCaL version: 2.1.3 % 39.55/6.80 % (395077)Termination reason: Instruction limit % 39.55/6.80 % (395077)Termination phase: Saturation % 39.55/6.80 % (395077)Time elapsed: 0.211 s % 39.55/6.80 % (395077)Peak memory usage: 137 MB % 39.55/6.80 % (395077)Instructions burned: 336 (million) % 39.55/6.80 % (395070)------------------------------ % 39.55/6.80 % (395070)------------------------------ % 39.55/6.80 % (395075)Instruction limit reached! % 39.55/6.80 % (395075)------------------------------ % 39.55/6.80 % (395075)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.55/6.80 % (395075)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.55/6.80 % (395075)CaDiCaL version: 2.1.3 % 39.55/6.80 % (395075)Termination reason: Instruction limit % 39.55/6.80 % (395075)Termination phase: Saturation % 39.55/6.80 % (395075)Time elapsed: 0.445 s % 39.55/6.80 % (395075)Peak memory usage: 95 MB % 39.55/6.80 % (395075)Instructions burned: 514 (million) % 39.55/6.80 % (395087)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=3802573325:s2pl=no:i=235:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2959 on theBenchmark for (2959ds/235Mi) % 39.55/6.80 % (395086)lrs-2_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_max:tha=off:random_seed=341467457:st=1.5:i=261:sd=1:kws=precedence:rtra=on:ss=axioms_2959 on theBenchmark for (2959ds/261Mi) % 39.55/6.80 % (395086)Refutation not found, incomplete strategy % 39.55/6.80 % (395086)------------------------------ % 39.55/6.80 % (395086)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.55/6.80 % (395086)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.55/6.80 % (395086)CaDiCaL version: 2.1.3 % 39.55/6.80 % (395086)Termination reason: Refutation not found, incomplete strategy % 39.55/6.80 % (395086)Time elapsed: 0.050 s % 39.55/6.80 % (395086)Peak memory usage: 111 MB % 39.55/6.80 % (395086)Instructions burned: 20 (million) % 39.55/6.80 % (395090)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=964235398:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2958 on theBenchmark for (2958ds/273Mi) % 39.55/6.80 % (395087)Refutation not found, incomplete strategy % 39.55/6.80 % (395087)------------------------------ % 39.55/6.80 % (395087)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.55/6.80 % (395087)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.55/6.80 % (395087)CaDiCaL version: 2.1.3 % 39.55/6.80 % (395087)Termination reason: Refutation not found, incomplete strategy % 39.55/6.80 % (395087)Time elapsed: 0.059 s % 39.55/6.80 % (395087)Peak memory usage: 111 MB % 39.55/6.80 % (395087)Instructions burned: 30 (million) % 39.55/6.80 % (395078)Instruction limit reached! % 39.55/6.80 % (395078)------------------------------ % 39.55/6.80 % (395078)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.55/6.80 % (395078)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.55/6.80 % (395078)CaDiCaL version: 2.1.3 % 39.55/6.80 % (395078)Termination reason: Instruction limit % 39.55/6.80 % (395078)Termination phase: Saturation % 39.55/6.80 % (395078)Time elapsed: 0.326 s % 39.55/6.80 % (395078)Peak memory usage: 92 MB % 39.55/6.80 % (395078)Instructions burned: 359 (million) % 39.55/6.80 % (395091)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=1538401887:i=146:doe=on:rtra=on_2958 on theBenchmark for (2958ds/146Mi) % 39.55/6.80 % (395091)Instruction limit reached! % 39.55/6.80 % (395091)------------------------------ % 39.55/6.80 % (395091)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.55/6.80 % (395091)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.55/6.80 % (395091)CaDiCaL version: 2.1.3 % 39.55/6.80 % (395091)Termination reason: Instruction limit % 39.55/6.80 % (395091)Termination phase: Saturation % 39.55/6.80 % (395091)Time elapsed: 0.076 s % 39.55/6.80 % (395091)Peak memory usage: 91 MB % 39.55/6.80 % (395091)Instructions burned: 147 (million) % 39.55/6.80 % (395092)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=2312188823:i=4428:doe=on:fsr=off:rtra=on_2957 on theBenchmark for (2957ds/4428Mi) % 39.55/6.80 % (395081)Instruction limit reached! % 39.55/6.80 % (395081)------------------------------ % 39.55/6.80 % (395081)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.55/6.80 % (395081)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 46.40/7.61 % (395081)CaDiCaL version: 2.1.3 % 46.40/7.61 % (395081)Termination reason: Instruction limit % 46.40/7.61 % (395081)Termination phase: Saturation % 46.40/7.61 % (395081)Time elapsed: 0.367 s % 46.40/7.61 % (395081)Peak memory usage: 124 MB % 46.40/7.61 % (395081)Instructions burned: 341 (million) % 46.40/7.61 % (395090)Instruction limit reached! % 46.40/7.61 % (395090)------------------------------ % 46.40/7.61 % (395090)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 46.40/7.61 % (395090)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 46.40/7.61 % (395090)CaDiCaL version: 2.1.3 % 46.40/7.61 % (395090)Termination reason: Instruction limit % 46.40/7.61 % (395090)Termination phase: Saturation % 46.40/7.61 % (395090)Time elapsed: 0.290 s % 46.40/7.61 % (395090)Peak memory usage: 93 MB % 46.40/7.61 % (395090)Instructions burned: 274 (million) % 46.40/7.61 % (395097)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=1805699235:avsq=on:i=276:avsqr=1,2:rtra=on_2956 on theBenchmark for (2956ds/276Mi) % 46.40/7.61 % (395098)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=3675704818:i=1052:rtra=on_2955 on theBenchmark for (2955ds/1052Mi) % 46.40/7.61 % (395086)------------------------------ % 46.40/7.61 % (395086)------------------------------ % 46.40/7.61 % (395087)------------------------------ % 46.40/7.61 % (395087)------------------------------ % 46.40/7.61 % (395100)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=1200591150:i=655:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2954 on theBenchmark for (2954ds/655Mi) % 46.40/7.61 % (395102)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=1439634255:st=5:i=1054:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2953 on theBenchmark for (2953ds/1054Mi) % 46.40/7.61 % (395102)Refutation not found, incomplete strategy % 46.40/7.61 % (395102)------------------------------ % 46.40/7.61 % (395102)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 46.40/7.61 % (395102)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 46.40/7.61 % (395102)CaDiCaL version: 2.1.3 % 46.40/7.61 % (395102)Termination reason: Refutation not found, incomplete strategy % 46.40/7.61 % (395102)Time elapsed: 0.015 s % 46.40/7.61 % (395102)Peak memory usage: 88 MB % 46.40/7.61 % (395102)Instructions burned: 16 (million) % 46.40/7.61 % (395097)Instruction limit reached! % 46.40/7.61 % (395097)------------------------------ % 46.40/7.61 % (395097)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 46.40/7.61 % (395097)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 46.40/7.61 % (395097)CaDiCaL version: 2.1.3 % 46.40/7.61 % (395097)Termination reason: Instruction limit % 46.40/7.61 % (395097)Termination phase: Saturation % 46.40/7.61 % (395097)Time elapsed: 0.346 s % 46.40/7.61 % (395097)Peak memory usage: 136 MB % 46.40/7.61 % (395097)Instructions burned: 276 (million) % 46.40/7.61 % (395105)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=1338596744:s2a=on:i=450:doe=on:nm=32:rtra=on_2952 on theBenchmark for (2952ds/450Mi) % 46.40/7.61 % (395104)lrs-1002_1_to=kbo:sas=z3:si=on:norm_ineq=on:sos=on:tha=some:random_seed=409589959:i=107:rtra=on_2952 on theBenchmark for (2952ds/107Mi) % 46.40/7.61 % (395104)Refutation not found, incomplete strategy % 46.40/7.61 % (395104)------------------------------ % 46.40/7.61 % (395104)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 46.40/7.61 % (395104)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 46.40/7.61 % (395104)CaDiCaL version: 2.1.3 % 46.40/7.61 % (395104)Termination reason: Refutation not found, incomplete strategy % 46.40/7.61 % (395104)Time elapsed: 0.134 s % 46.40/7.61 % (395104)Peak memory usage: 115 MB % 46.40/7.61 % (395104)Instructions burned: 108 (million) % 46.40/7.61 % (395098)Instruction limit reached! % 46.40/7.61 % (395098)------------------------------ % 46.40/7.61 % (395098)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 46.40/7.61 % (395098)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 46.40/7.61 % (395098)CaDiCaL version: 2.1.3 % 46.40/7.61 % (395098)Termination reason: Instruction limit % 46.40/7.61 % (395098)Termination phase: Saturation % 46.40/7.61 % (395098)Time elapsed: 0.507 s % 46.40/7.61 % (395098)Peak memory usage: 98 MB % 51.93/8.38 % (395098)Instructions burned: 1052 (million) % 51.93/8.38 % (395102)------------------------------ % 51.93/8.38 % (395102)------------------------------ % 51.93/8.38 % (395108)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 % 51.93/8.38 % (395108)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=458320863:i=1090:aac=none:nm=0:rtra=on:rawr=on_2949 on theBenchmark for (2949ds/1090Mi) % 51.93/8.38 % (395111)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=3590798900:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2948 on theBenchmark for (2948ds/130Mi) % 51.93/8.38 % (395100)Instruction limit reached! % 51.93/8.38 % (395100)------------------------------ % 51.93/8.38 % (395100)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 51.93/8.38 % (395100)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 51.93/8.38 % (395100)CaDiCaL version: 2.1.3 % 51.93/8.38 % (395100)Termination reason: Instruction limit % 51.93/8.38 % (395100)Termination phase: Saturation % 51.93/8.38 % (395100)Time elapsed: 0.629 s % 51.93/8.38 % (395100)Peak memory usage: 98 MB % 51.93/8.38 % (395100)Instructions burned: 655 (million) % 51.93/8.38 % (395105)Instruction limit reached! % 51.93/8.38 % (395105)------------------------------ % 51.93/8.38 % (395105)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 51.93/8.38 % (395105)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 51.93/8.38 % (395105)CaDiCaL version: 2.1.3 % 51.93/8.38 % (395105)Termination reason: Instruction limit % 51.93/8.38 % (395105)Termination phase: Saturation % 51.93/8.38 % (395105)Time elapsed: 0.428 s % 51.93/8.38 % (395105)Peak memory usage: 137 MB % 51.93/8.38 % (395105)Instructions burned: 451 (million) % 51.93/8.38 % (395111)Instruction limit reached! % 51.93/8.38 % (395111)------------------------------ % 51.93/8.38 % (395111)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 51.93/8.38 % (395111)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 51.93/8.38 % (395111)CaDiCaL version: 2.1.3 % 51.93/8.38 % (395111)Termination reason: Instruction limit % 51.93/8.38 % (395111)Termination phase: Saturation % 51.93/8.38 % (395111)Time elapsed: 0.083 s % 51.93/8.38 % (395111)Peak memory usage: 118 MB % 51.93/8.38 % (395111)Instructions burned: 131 (million) % 51.93/8.38 % (395104)------------------------------ % 51.93/8.38 % (395104)------------------------------ % 51.93/8.38 % (395113)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=2123384753:i=312:kws=inv_frequency:nm=20:rtra=on_2947 on theBenchmark for (2947ds/312Mi) % 51.93/8.38 % (395120)ott+10_1_to=kbo:sil=64000:si=on:sp=reverse_frequency:sos=on:random_seed=4022369103:i=491:doe=on:rtra=on:gtg=position_2945 on theBenchmark for (2945ds/491Mi) % 51.93/8.38 % (395128)ott+1011_2_to=lpo:sil=128000:si=on:sos=on:random_seed=2840969533:i=307:bd=preordered:av=off:rtra=on:ev=cautious_2945 on theBenchmark for (2945ds/307Mi) % 51.93/8.38 % (395120)Refutation not found, incomplete strategy % 51.93/8.38 % (395120)------------------------------ % 51.93/8.38 % (395120)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 51.93/8.38 % (395120)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 51.93/8.38 % (395120)CaDiCaL version: 2.1.3 % 51.93/8.38 % (395120)Termination reason: Refutation not found, incomplete strategy % 51.93/8.38 % (395120)Time elapsed: 0.071 s % 51.93/8.38 % (395120)Peak memory usage: 91 MB % 51.93/8.38 % (395120)Instructions burned: 111 (million) % 51.93/8.38 % (395127)ott+1011_4:1_to=lpo:sil=64000:si=on:spb=intro:random_seed=1262600080:s2a=on:i=835:s2at=2:rtra=on_2945 on theBenchmark for (2945ds/835Mi) % 51.93/8.38 % (395128)Refutation not found, incomplete strategy % 51.93/8.38 % (395128)------------------------------ % 51.93/8.38 % (395128)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 51.93/8.38 % (395128)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 51.93/8.38 % (395128)CaDiCaL version: 2.1.3 % 51.93/8.38 % (395128)Termination reason: Refutation not found, incomplete strategy % 51.93/8.38 % (395128)Time elapsed: 0.067 s % 51.93/8.38 % (395128)Peak memory usage: 91 MB % 51.93/8.38 % (395128)Instructions burned: 130 (million) % 51.93/8.38 % (395133)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=3470179314:i=776:doe=on:rtra=on_2944 on theBenchmark for (2944ds/776Mi) % 58.98/9.31 % (395113)Instruction limit reached! % 58.98/9.31 % (395113)------------------------------ % 58.98/9.31 % (395113)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 58.98/9.31 % (395113)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 58.98/9.31 % (395113)CaDiCaL version: 2.1.3 % 58.98/9.31 % (395113)Termination reason: Instruction limit % 58.98/9.31 % (395113)Termination phase: Saturation % 58.98/9.31 % (395113)Time elapsed: 0.346 s % 58.98/9.31 % (395113)Peak memory usage: 119 MB % 58.98/9.31 % (395113)Instructions burned: 313 (million) % 58.98/9.31 % (395128)------------------------------ % 58.98/9.31 % (395128)------------------------------ % 58.98/9.31 % (395120)------------------------------ % 58.98/9.31 % (395120)------------------------------ % 58.98/9.31 % (395139)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=2120005067:thitd=on:cond=fast:i=784:nm=30:rtra=on:gtg=all:tac=axiom_2939 on theBenchmark for (2939ds/784Mi) % 58.98/9.31 % (395138)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=4224356993:s2a=on:i=646:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2940 on theBenchmark for (2940ds/646Mi) % 58.98/9.31 % (395108)Instruction limit reached! % 58.98/9.31 % (395108)------------------------------ % 58.98/9.31 % (395108)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 58.98/9.31 % (395108)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 58.98/9.31 % (395108)CaDiCaL version: 2.1.3 % 58.98/9.31 % (395108)Termination reason: Instruction limit % 58.98/9.31 % (395108)Termination phase: Saturation % 58.98/9.31 % (395108)Time elapsed: 1.059 s % 58.98/9.31 % (395108)Peak memory usage: 127 MB % 58.98/9.31 % (395108)Instructions burned: 1090 (million) % 58.98/9.31 % (395140)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=2473654673:thitd=on:s2a=on:i=1131:add=on:canc=force:bd=all:rtra=on:tac=axiom:ev=off_2938 on theBenchmark for (2938ds/1131Mi) % 58.98/9.31 % (395127)Instruction limit reached! % 58.98/9.31 % (395127)------------------------------ % 58.98/9.31 % (395127)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 58.98/9.31 % (395127)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 58.98/9.31 % (395127)CaDiCaL version: 2.1.3 % 58.98/9.31 % (395127)Termination reason: Instruction limit % 58.98/9.31 % (395127)Termination phase: Saturation % 58.98/9.31 % (395127)Time elapsed: 0.765 s % 58.98/9.31 % (395127)Peak memory usage: 96 MB % 58.98/9.31 % (395127)Instructions burned: 835 (million) % 58.98/9.31 % (395143)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=3420020488:s2pl=no:i=246:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2936 on theBenchmark for (2936ds/246Mi) % 58.98/9.31 % (395139)Instruction limit reached! % 58.98/9.31 % (395139)------------------------------ % 58.98/9.31 % (395139)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 58.98/9.31 % (395139)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 58.98/9.31 % (395139)CaDiCaL version: 2.1.3 % 58.98/9.31 % (395139)Termination reason: Instruction limit % 58.98/9.31 % (395139)Termination phase: Saturation % 58.98/9.31 % (395139)Time elapsed: 0.403 s % 58.98/9.31 % (395139)Peak memory usage: 120 MB % 58.98/9.31 % (395139)Instructions burned: 785 (million) % 58.98/9.31 % (395133)Instruction limit reached! % 58.98/9.31 % (395133)------------------------------ % 58.98/9.31 % (395133)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 58.98/9.31 % (395133)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 58.98/9.31 % (395133)CaDiCaL version: 2.1.3 % 58.98/9.31 % (395133)Termination reason: Instruction limit % 58.98/9.31 % (395133)Termination phase: Saturation % 58.98/9.31 % (395133)Time elapsed: 0.761 s % 58.98/9.31 % (395133)Peak memory usage: 124 MB % 58.98/9.31 % (395133)Instructions burned: 779 (million) % 58.98/9.31 % (395143)Refutation not found, incomplete strategy % 58.98/9.31 % (395143)------------------------------ % 58.98/9.31 % (395143)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 58.98/9.31 % (395143)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 58.98/9.31 % (395143)CaDiCaL version: 2.1.3 % 58.98/9.31 % (395143)Termination reason: Refutation not found, incomplete strategy % 75.25/11.61 % (395143)Time elapsed: 0.060 s % 75.25/11.61 % (395143)Peak memory usage: 112 MB % 75.25/11.61 % (395143)Instructions burned: 30 (million) % 75.25/11.61 % (395145)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=1446960372:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2934 on theBenchmark for (2934ds/775Mi) % 75.25/11.61 % (395145)Refutation not found, incomplete strategy % 75.25/11.61 % (395145)------------------------------ % 75.25/11.61 % (395145)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 75.25/11.61 % (395145)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 75.25/11.61 % (395145)CaDiCaL version: 2.1.3 % 75.25/11.61 % (395145)Termination reason: Refutation not found, incomplete strategy % 75.25/11.61 % (395145)Time elapsed: 0.025 s % 75.25/11.61 % (395145)Peak memory usage: 88 MB % 75.25/11.61 % (395145)Instructions burned: 27 (million) % 75.25/11.61 % (395147)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=939748021:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2933 on theBenchmark for (2933ds/273Mi) % 75.25/11.61 % (395148)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=1940787536:i=102:nm=16:rtra=on_2933 on theBenchmark for (2933ds/102Mi) % 75.25/11.61 % (395138)Instruction limit reached! % 75.25/11.61 % (395138)------------------------------ % 75.25/11.61 % (395138)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 75.25/11.61 % (395138)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 75.25/11.61 % (395138)CaDiCaL version: 2.1.3 % 75.25/11.61 % (395138)Termination reason: Instruction limit % 75.25/11.61 % (395138)Termination phase: Saturation % 75.25/11.61 % (395138)Time elapsed: 0.754 s % 75.25/11.61 % (395138)Peak memory usage: 141 MB % 75.25/11.61 % (395138)Instructions burned: 646 (million) % 75.25/11.61 % (395147)Instruction limit reached! % 75.25/11.61 % (395147)------------------------------ % 75.25/11.61 % (395147)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 75.25/11.61 % (395147)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 75.25/11.61 % (395147)CaDiCaL version: 2.1.3 % 75.25/11.61 % (395147)Termination reason: Instruction limit % 75.25/11.61 % (395147)Termination phase: Saturation % 75.25/11.61 % (395147)Time elapsed: 0.151 s % 75.25/11.61 % (395147)Peak memory usage: 93 MB % 75.25/11.61 % (395147)Instructions burned: 274 (million) % 75.25/11.61 % (395148)Instruction limit reached! % 75.25/11.61 % (395148)------------------------------ % 75.25/11.61 % (395148)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 75.25/11.61 % (395148)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 75.25/11.61 % (395148)CaDiCaL version: 2.1.3 % 75.25/11.61 % (395148)Termination reason: Instruction limit % 75.25/11.61 % (395148)Termination phase: Saturation % 75.25/11.61 % (395148)Time elapsed: 0.095 s % 75.25/11.61 % (395148)Peak memory usage: 90 MB % 75.25/11.61 % (395148)Instructions burned: 103 (million) % 75.25/11.61 % (395143)------------------------------ % 75.25/11.61 % (395143)------------------------------ % 75.25/11.61 % (395145)------------------------------ % 75.25/11.61 % (395145)------------------------------ % 75.25/11.61 % (395152)lrs+10_1_to=lpo:sil=128000:si=on:bsr=unit_only:tha=off:random_seed=529985640:avsq=on:s2a=on:i=1094:s2at=5:avsqr=4463,131072:rtra=on_2930 on theBenchmark for (2930ds/1094Mi) % 75.25/11.61 % (395154)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=1281961249:i=868:doe=on:nm=0:rtra=on:gtg=exists_sym_2929 on theBenchmark for (2929ds/868Mi) % 75.25/11.61 % (395153)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=3239009639:i=6400:doe=on:fsr=off:rtra=on_2929 on theBenchmark for (2929ds/6400Mi) % 75.25/11.61 % (395155)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=3116961788:i=1846:canc=cautious:fsr=off:rtra=on_2929 on theBenchmark for (2929ds/1846Mi) % 75.25/11.61 % (395156)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=1323125676:s2a=on:i=36816:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2928 on theBenchmark for (2928ds/36816Mi) % 75.25/11.61 % (395155)Refutation not found, incomplete strategy % 75.25/11.61 % (395155)------------------------------ % 75.25/11.61 % (395155)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 75.25/11.61 % (395155)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 90.53/13.97 % (395155)CaDiCaL version: 2.1.3 % 90.53/13.97 % (395155)Termination reason: Refutation not found, incomplete strategy % 90.53/13.97 % (395155)Time elapsed: 0.093 s % 90.53/13.97 % (395155)Peak memory usage: 91 MB % 90.53/13.97 % (395155)Instructions burned: 103 (million) % 90.53/13.97 % (395140)Instruction limit reached! % 90.53/13.97 % (395140)------------------------------ % 90.53/13.97 % (395140)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 90.53/13.97 % (395140)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 90.53/13.97 % (395140)CaDiCaL version: 2.1.3 % 90.53/13.97 % (395140)Termination reason: Instruction limit % 90.53/13.97 % (395140)Termination phase: Saturation % 90.53/13.97 % (395140)Time elapsed: 1.205 s % 90.53/13.97 % (395140)Peak memory usage: 133 MB % 90.53/13.97 % (395140)Instructions burned: 1131 (million) % 90.53/13.97 % (395152)Instruction limit reached! % 90.53/13.97 % (395152)------------------------------ % 90.53/13.97 % (395152)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 90.53/13.97 % (395152)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 90.53/13.97 % (395152)CaDiCaL version: 2.1.3 % 90.53/13.97 % (395152)Termination reason: Instruction limit % 90.53/13.97 % (395152)Termination phase: Saturation % 90.53/13.97 % (395152)Time elapsed: 0.519 s % 90.53/13.97 % (395152)Peak memory usage: 97 MB % 90.53/13.97 % (395152)Instructions burned: 1094 (million) % 90.53/13.97 % (395162)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=3939674467:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2923 on theBenchmark for (2923ds/273Mi) % 90.53/13.97 % (395155)------------------------------ % 90.53/13.97 % (395155)------------------------------ % 90.53/13.97 % (395163)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=4315640:i=863:doe=on:nm=0:rtra=on:gtg=exists_sym_2922 on theBenchmark for (2922ds/863Mi) % 90.53/13.97 % (395092)Instruction limit reached! % 90.53/13.97 % (395092)------------------------------ % 90.53/13.97 % (395092)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 90.53/13.97 % (395092)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 90.53/13.97 % (395092)CaDiCaL version: 2.1.3 % 90.53/13.97 % (395092)Termination reason: Instruction limit % 90.53/13.97 % (395092)Termination phase: Saturation % 90.53/13.97 % (395092)Time elapsed: 3.554 s % 90.53/13.97 % (395092)Peak memory usage: 109 MB % 90.53/13.97 % (395092)Instructions burned: 4429 (million) % 90.53/13.97 % (395162)Instruction limit reached! % 90.53/13.97 % (395162)------------------------------ % 90.53/13.97 % (395162)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 90.53/13.97 % (395162)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 90.53/13.97 % (395162)CaDiCaL version: 2.1.3 % 90.53/13.97 % (395162)Termination reason: Instruction limit % 90.53/13.97 % (395162)Termination phase: Saturation % 90.53/13.97 % (395162)Time elapsed: 0.295 s % 90.53/13.97 % (395162)Peak memory usage: 92 MB % 90.53/13.97 % (395162)Instructions burned: 273 (million) % 90.53/13.97 % (395154)Instruction limit reached! % 90.53/13.97 % (395154)------------------------------ % 90.53/13.97 % (395154)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 90.53/13.97 % (395154)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 90.53/13.97 % (395154)CaDiCaL version: 2.1.3 % 90.53/13.97 % (395154)Termination reason: Instruction limit % 90.53/13.97 % (395154)Termination phase: Saturation % 90.53/13.97 % (395154)Time elapsed: 0.841 s % 90.53/13.97 % (395154)Peak memory usage: 122 MB % 90.53/13.97 % (395154)Instructions burned: 868 (million) % 90.53/13.97 % (395165)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=1925981719:i=5811:kws=precedence:nm=0:rtra=on_2921 on theBenchmark for (2921ds/5811Mi) % 90.53/13.97 % (395167)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=3263625354:i=2216:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2919 on theBenchmark for (2919ds/2216Mi) % 90.53/13.97 % (395169)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=49483481:st=5:i=1026:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2918 on theBenchmark for (2918ds/1026Mi) % 90.53/13.97 % (395169)Refutation not found, incomplete strategy % 90.53/13.97 % (395169)------------------------------ % 90.53/13.97 % (395169)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 108.02/16.29 % (395169)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.02/16.29 % (395169)CaDiCaL version: 2.1.3 % 108.02/16.29 % (395169)Termination reason: Refutation not found, incomplete strategy % 108.02/16.29 % (395169)Time elapsed: 0.015 s % 108.02/16.29 % (395169)Peak memory usage: 88 MB % 108.02/16.29 % (395169)Instructions burned: 16 (million) % 108.02/16.29 % (395168)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=1549073165:i=801:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2918 on theBenchmark for (2918ds/801Mi) % 108.02/16.29 % (395163)Instruction limit reached! % 108.02/16.29 % (395163)------------------------------ % 108.02/16.29 % (395163)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 108.02/16.29 % (395163)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.02/16.29 % (395163)CaDiCaL version: 2.1.3 % 108.02/16.29 % (395163)Termination reason: Instruction limit % 108.02/16.29 % (395163)Termination phase: Saturation % 108.02/16.29 % (395163)Time elapsed: 0.444 s % 108.02/16.29 % (395163)Peak memory usage: 122 MB % 108.02/16.29 % (395163)Instructions burned: 864 (million) % 108.02/16.29 % (395174)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=3951211784:i=3509:rtra=on_2915 on theBenchmark for (2915ds/3509Mi) % 108.02/16.29 % (395169)------------------------------ % 108.02/16.29 % (395169)------------------------------ % 108.02/16.29 % (395176)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=568743685:st=2:i=2127:sd=12:ep=R:rtra=on:ss=axioms_2912 on theBenchmark for (2912ds/2127Mi) % 108.02/16.29 % (395176)Refutation not found, incomplete strategy % 108.02/16.29 % (395176)------------------------------ % 108.02/16.29 % (395176)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 108.02/16.29 % (395176)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.02/16.29 % (395176)CaDiCaL version: 2.1.3 % 108.02/16.29 % (395176)Termination reason: Refutation not found, incomplete strategy % 108.02/16.29 % (395176)Time elapsed: 0.023 s % 108.02/16.29 % (395176)Peak memory usage: 88 MB % 108.02/16.29 % (395176)Instructions burned: 25 (million) % 108.02/16.29 % (395168)Instruction limit reached! % 108.02/16.29 % (395168)------------------------------ % 108.02/16.29 % (395168)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 108.02/16.29 % (395168)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.02/16.29 % (395168)CaDiCaL version: 2.1.3 % 108.02/16.29 % (395168)Termination reason: Instruction limit % 108.02/16.29 % (395168)Termination phase: Saturation % 108.02/16.29 % (395168)Time elapsed: 0.771 s % 108.02/16.29 % (395168)Peak memory usage: 99 MB % 108.02/16.29 % (395168)Instructions burned: 802 (million) % 108.02/16.29 % (395178)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=2728592496:i=1959:rtra=on:fsd=on:proc=on_2908 on theBenchmark for (2908ds/1959Mi) % 108.02/16.29 % (395176)------------------------------ % 108.02/16.29 % (395176)------------------------------ % 108.02/16.29 % (395182)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=3604502985:s2a=on:i=3553:nm=0:rtra=on_2905 on theBenchmark for (2905ds/3553Mi) % 108.02/16.29 % (395174)Instruction limit reached! % 108.02/16.29 % (395174)------------------------------ % 108.02/16.29 % (395174)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 108.02/16.29 % (395174)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.02/16.29 % (395174)CaDiCaL version: 2.1.3 % 108.02/16.29 % (395174)Termination reason: Instruction limit % 108.02/16.29 % (395174)Termination phase: Saturation % 108.02/16.29 % (395174)Time elapsed: 1.799 s % 108.02/16.29 % (395174)Peak memory usage: 112 MB % 108.02/16.29 % (395174)Instructions burned: 3509 (million) % 108.02/16.29 % (395167)Instruction limit reached! % 108.02/16.29 % (395167)------------------------------ % 108.02/16.29 % (395167)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 108.02/16.29 % (395167)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.02/16.29 % (395167)CaDiCaL version: 2.1.3 % 108.02/16.29 % (395167)Termination reason: Instruction limit % 108.02/16.29 % (395167)Termination phase: Saturation % 108.02/16.29 % (395167)Time elapsed: 2.177 s % 108.02/16.29 % (395167)Peak memory usage: 135 MB % 108.02/16.29 % (395167)Instructions burned: 2216 (million) % 108.02/16.29 % (395184)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=3958479999:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2895 on theBenchmark for (2895ds/3201Mi) % 140.92/20.83 % (395185)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=1700115508:thitd=on:cond=on:i=4093:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2894 on theBenchmark for (2894ds/4093Mi) % 140.92/20.83 % (395178)Instruction limit reached! % 140.92/20.83 % (395178)------------------------------ % 140.92/20.83 % (395178)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 140.92/20.83 % (395178)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 140.92/20.83 % (395178)CaDiCaL version: 2.1.3 % 140.92/20.83 % (395178)Termination reason: Instruction limit % 140.92/20.83 % (395178)Termination phase: Saturation % 140.92/20.83 % (395178)Time elapsed: 1.938 s % 140.92/20.83 % (395178)Peak memory usage: 141 MB % 140.92/20.83 % (395178)Instructions burned: 1960 (million) % 140.92/20.83 % (395188)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=490551875:cond=fast:i=21173:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2886 on theBenchmark for (2886ds/21173Mi) % 140.92/20.83 % (395188)Refutation not found, incomplete strategy % 140.92/20.83 % (395188)------------------------------ % 140.92/20.83 % (395188)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 140.92/20.83 % (395188)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 140.92/20.83 % (395188)CaDiCaL version: 2.1.3 % 140.92/20.83 % (395188)Termination reason: Refutation not found, incomplete strategy % 140.92/20.83 % (395188)Time elapsed: 0.050 s % 140.92/20.83 % (395188)Peak memory usage: 113 MB % 140.92/20.83 % (395188)Instructions burned: 18 (million) % 140.92/20.83 % (395188)------------------------------ % 140.92/20.83 % (395188)------------------------------ % 140.92/20.83 % (395184)Instruction limit reached! % 140.92/20.83 % (395184)------------------------------ % 140.92/20.83 % (395184)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 140.92/20.83 % (395184)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 140.92/20.83 % (395184)CaDiCaL version: 2.1.3 % 140.92/20.83 % (395184)Termination reason: Instruction limit % 140.92/20.83 % (395184)Termination phase: Saturation % 140.92/20.83 % (395184)Time elapsed: 1.420 s % 140.92/20.83 % (395184)Peak memory usage: 100 MB % 140.92/20.83 % (395184)Instructions burned: 3204 (million) % 140.92/20.83 % (395190)lrs+11_1_to=lpo:thi=all:sas=z3:si=on:fd=off:sac=on:slsq=on:random_seed=2735198346:avsq=on:i=10544:avsqr=17,4:canc=force:rtra=on:gtg=exists_top:er=filter_2879 on theBenchmark for (2879ds/10544Mi) % 140.92/20.83 % (395191)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=2694487767:avsq=on:i=1262:avsqr=1,16:rtra=on:rawr=on_2878 on theBenchmark for (2878ds/1262Mi) % 140.92/20.83 % (395153)Instruction limit reached! % 140.92/20.83 % (395153)------------------------------ % 140.92/20.83 % (395153)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 140.92/20.83 % (395153)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 140.92/20.83 % (395153)CaDiCaL version: 2.1.3 % 140.92/20.83 % (395153)Termination reason: Instruction limit % 140.92/20.83 % (395153)Termination phase: Saturation % 140.92/20.83 % (395153)Time elapsed: 5.100 s % 140.92/20.83 % (395153)Peak memory usage: 119 MB % 140.92/20.83 % (395153)Instructions burned: 6400 (million) % 140.92/20.83 % (395194)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=1810691602:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2876 on theBenchmark for (2876ds/775Mi) % 140.92/20.83 % (395194)Refutation not found, incomplete strategy % 140.92/20.83 % (395194)------------------------------ % 140.92/20.83 % (395194)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 140.92/20.83 % (395194)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 140.92/20.83 % (395194)CaDiCaL version: 2.1.3 % 140.92/20.83 % (395194)Termination reason: Refutation not found, incomplete strategy % 140.92/20.83 % (395194)Time elapsed: 0.025 s % 140.92/20.83 % (395194)Peak memory usage: 88 MB % 140.92/20.83 % (395194)Instructions burned: 27 (million) % 140.92/20.83 % (395191)Instruction limit reached! % 140.92/20.83 % (395191)------------------------------ % 140.92/20.83 % (395191)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 140.92/20.83 % (395191)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 140.92/20.83 % (395191)CaDiCaL version: 2.1.3 % 140.92/20.83 % (395191)Termination reason: Instruction limit % 164.95/24.24 % (395191)Termination phase: Saturation % 164.95/24.24 % (395191)Time elapsed: 0.716 s % 164.95/24.24 % (395191)Peak memory usage: 129 MB % 164.95/24.24 % (395191)Instructions burned: 1263 (million) % 164.95/24.24 % (395194)------------------------------ % 164.95/24.24 % (395194)------------------------------ % 164.95/24.24 % (395196)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=775528122:i=270:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2869 on theBenchmark for (2869ds/270Mi) % 164.95/24.24 % (395182)Instruction limit reached! % 164.95/24.24 % (395182)------------------------------ % 164.95/24.24 % (395182)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 164.95/24.24 % (395182)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.95/24.24 % (395182)CaDiCaL version: 2.1.3 % 164.95/24.24 % (395182)Termination reason: Instruction limit % 164.95/24.24 % (395182)Termination phase: Saturation % 164.95/24.24 % (395182)Time elapsed: 3.540 s % 164.95/24.24 % (395182)Peak memory usage: 118 MB % 164.95/24.24 % (395182)Instructions burned: 3553 (million) % 164.95/24.24 % (395196)Instruction limit reached! % 164.95/24.24 % (395196)------------------------------ % 164.95/24.24 % (395196)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 164.95/24.24 % (395196)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.95/24.24 % (395196)CaDiCaL version: 2.1.3 % 164.95/24.24 % (395196)Termination reason: Instruction limit % 164.95/24.24 % (395196)Termination phase: Saturation % 164.95/24.24 % (395196)Time elapsed: 0.101 s % 164.95/24.24 % (395196)Peak memory usage: 93 MB % 164.95/24.24 % (395196)Instructions burned: 273 (million) % 164.95/24.24 % (395165)Instruction limit reached! % 164.95/24.24 % (395165)------------------------------ % 164.95/24.24 % (395165)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 164.95/24.24 % (395165)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.95/24.24 % (395165)CaDiCaL version: 2.1.3 % 164.95/24.24 % (395165)Termination reason: Instruction limit % 164.95/24.24 % (395165)Termination phase: Saturation % 164.95/24.24 % (395165)Time elapsed: 5.227 s % 164.95/24.24 % (395165)Peak memory usage: 147 MB % 164.95/24.24 % (395165)Instructions burned: 5811 (million) % 164.95/24.24 % (395197)ott+10_128_isp=bottom:to=lpo:sil=128000:si=on:urr=on:uwa=alasca_main:sac=on:slsq=on:random_seed=1934068799:i=17165:aac=none:doe=on:rtra=on:gtg=exists_all_2868 on theBenchmark for (2868ds/17165Mi) % 164.95/24.24 % (395200)lrs+10_1_to=lpo:sil=128000:si=on:sp=occurrence:random_seed=4217468243:st=2:i=12633:rtra=on:ss=axioms_2866 on theBenchmark for (2866ds/12633Mi) % 164.95/24.24 % (395200)Refutation not found, incomplete strategy % 164.95/24.24 % (395200)------------------------------ % 164.95/24.24 % (395200)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 164.95/24.24 % (395200)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.95/24.24 % (395200)CaDiCaL version: 2.1.3 % 164.95/24.24 % (395200)Termination reason: Refutation not found, incomplete strategy % 164.95/24.24 % (395200)Time elapsed: 0.011 s % 164.95/24.24 % (395200)Peak memory usage: 88 MB % 164.95/24.24 % (395200)Instructions burned: 24 (million) % 164.95/24.24 % (395199)lrs+2_10_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_main:tha=some:random_seed=1847236925:s2a=on:i=13094:s2at=-1:rtra=on_2867 on theBenchmark for (2867ds/13094Mi) % 164.95/24.24 % (395202)dis+1011_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_frequency:lsd=20:nwc=3:random_seed=2858710824:i=1783:rtra=on:gtg=position_2866 on theBenchmark for (2866ds/1783Mi) % 164.95/24.24 % (395200)------------------------------ % 164.95/24.24 % (395200)------------------------------ % 164.95/24.24 % (395206)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=1207339420:i=5451:aac=none:doe=on:nm=0:rtra=on:amm=off:gtg=position_2862 on theBenchmark for (2862ds/5451Mi) % 164.95/24.24 % (395185)Instruction limit reached! % 164.95/24.24 % (395185)------------------------------ % 164.95/24.24 % (395185)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 164.95/24.24 % (395185)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.95/24.24 % (395185)CaDiCaL version: 2.1.3 % 164.95/24.24 % (395185)Termination reason: Instruction limit % 164.95/24.24 % (395185)Termination phase: Saturation % 164.95/24.24 % (395185)Time elapsed: 4.309 s % 164.95/24.24 % (395185)Peak memory usage: 153 MB % 164.95/24.24 % (395185)Instructions burned: 4094 (million) % 164.95/24.24 % (395202)Instruction limit reached! % 200.39/29.22 % (395202)------------------------------ % 200.39/29.22 % (395202)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 200.39/29.22 % (395202)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 200.39/29.22 % (395202)CaDiCaL version: 2.1.3 % 200.39/29.22 % (395202)Termination reason: Instruction limit % 200.39/29.22 % (395202)Termination phase: Saturation % 200.39/29.22 % (395202)Time elapsed: 1.693 s % 200.39/29.22 % (395202)Peak memory usage: 128 MB % 200.39/29.22 % (395202)Instructions burned: 1783 (million) % 200.39/29.22 % (395214)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=239259121:i=4975:doe=on:nm=0:rtra=on:gtg=exists_sym_2848 on theBenchmark for (2848ds/4975Mi) % 200.39/29.22 % (395216)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=1543319999:i=2076:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2846 on theBenchmark for (2846ds/2076Mi) % 200.39/29.22 % (395206)Instruction limit reached! % 200.39/29.22 % (395206)------------------------------ % 200.39/29.22 % (395206)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 200.39/29.22 % (395206)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 200.39/29.22 % (395206)CaDiCaL version: 2.1.3 % 200.39/29.22 % (395206)Termination reason: Instruction limit % 200.39/29.22 % (395206)Termination phase: Saturation % 200.39/29.22 % (395206)Time elapsed: 2.868 s % 200.39/29.22 % (395206)Peak memory usage: 144 MB % 200.39/29.22 % (395206)Instructions burned: 5452 (million) % 200.39/29.22 % (395226)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=224506644:i=5145:rtra=on_2831 on theBenchmark for (2831ds/5145Mi) % 200.39/29.22 % (395216)Instruction limit reached! % 200.39/29.22 % (395216)------------------------------ % 200.39/29.22 % (395216)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 200.39/29.22 % (395216)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 200.39/29.22 % (395216)CaDiCaL version: 2.1.3 % 200.39/29.22 % (395216)Termination reason: Instruction limit % 200.39/29.22 % (395216)Termination phase: Saturation % 200.39/29.22 % (395216)Time elapsed: 1.992 s % 200.39/29.22 % (395216)Peak memory usage: 135 MB % 200.39/29.22 % (395216)Instructions burned: 2077 (million) % 200.39/29.22 % (395230)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=2095096194:i=3509:rtra=on_2823 on theBenchmark for (2823ds/3509Mi) % 200.39/29.22 % (395214)Instruction limit reached! % 200.39/29.22 % (395214)------------------------------ % 200.39/29.22 % (395214)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 200.39/29.22 % (395214)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 200.39/29.22 % (395214)CaDiCaL version: 2.1.3 % 200.39/29.22 % (395214)Termination reason: Instruction limit % 200.39/29.22 % (395214)Termination phase: Saturation % 200.39/29.22 % (395214)Time elapsed: 2.989 s % 200.39/29.22 % (395214)Peak memory usage: 139 MB % 200.39/29.22 % (395214)Instructions burned: 4976 (million) % 200.39/29.22 % (395234)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=2434174616:st=2:i=13800:sd=12:ep=R:rtra=on:ss=axioms_2815 on theBenchmark for (2815ds/13800Mi) % 200.39/29.22 % (395234)Refutation not found, incomplete strategy % 200.39/29.22 % (395234)------------------------------ % 200.39/29.22 % (395234)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 200.39/29.22 % (395234)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 200.39/29.22 % (395234)CaDiCaL version: 2.1.3 % 200.39/29.22 % (395234)Termination reason: Refutation not found, incomplete strategy % 200.39/29.22 % (395234)Time elapsed: 0.012 s % 200.39/29.22 % (395234)Peak memory usage: 88 MB % 200.39/29.22 % (395234)Instructions burned: 25 (million) % 200.39/29.22 % (395234)------------------------------ % 200.39/29.22 % (395234)------------------------------ % 200.39/29.22 % (395240)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=1188972270:i=1412:rtra=on:fsd=on:proc=on_2811 on theBenchmark for (2811ds/1412Mi) % 200.39/29.22 % (395240)Instruction limit reached! % 200.39/29.22 % (395240)------------------------------ % 200.39/29.22 % (395240)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 200.39/29.22 % (395240)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 200.39/29.22 % (395240)CaDiCaL version: 2.1.3 % 200.39/29.22 % (395240)Termination reason: Instruction limit % 200.39/29.22 % (395240)Termination phase: Saturation % 296.91/42.93 % (395240)Time elapsed: 0.782 s % 296.91/42.93 % (395240)Peak memory usage: 135 MB % 296.91/42.93 % (395240)Instructions burned: 1412 (million) % 296.91/42.93 % (395242)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 % 296.91/42.93 % (395242)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=1789649088:i=11747:aac=none:nm=0:rtra=on:rawr=on_2800 on theBenchmark for (2800ds/11747Mi) % 296.91/42.93 % (395230)Instruction limit reached! % 296.91/42.93 % (395230)------------------------------ % 296.91/42.93 % (395230)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 296.91/42.93 % (395230)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 296.91/42.93 % (395230)CaDiCaL version: 2.1.3 % 296.91/42.93 % (395230)Termination reason: Instruction limit % 296.91/42.93 % (395230)Termination phase: Saturation % 296.91/42.93 % (395230)Time elapsed: 3.109 s % 296.91/42.93 % (395230)Peak memory usage: 111 MB % 296.91/42.93 % (395230)Instructions burned: 3510 (million) % 296.91/42.93 % (395248)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=2050664836:s2a=on:i=3553:nm=0:rtra=on_2790 on theBenchmark for (2790ds/3553Mi) % 296.91/42.93 % (395226)Instruction limit reached! % 296.91/42.93 % (395226)------------------------------ % 296.91/42.93 % (395226)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 296.91/42.93 % (395226)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 296.91/42.93 % (395226)CaDiCaL version: 2.1.3 % 296.91/42.93 % (395226)Termination reason: Instruction limit % 296.91/42.93 % (395226)Termination phase: Saturation % 296.91/42.93 % (395226)Time elapsed: 4.587 s % 296.91/42.93 % (395226)Peak memory usage: 126 MB % 296.91/42.93 % (395226)Instructions burned: 5145 (million) % 296.91/42.93 % (395190)Instruction limit reached! % 296.91/42.93 % (395190)------------------------------ % 296.91/42.93 % (395190)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 296.91/42.93 % (395190)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 296.91/42.93 % (395190)CaDiCaL version: 2.1.3 % 296.91/42.93 % (395190)Termination reason: Instruction limit % 296.91/42.93 % (395190)Termination phase: Saturation % 296.91/42.93 % (395190)Time elapsed: 9.606 s % 296.91/42.93 % (395190)Peak memory usage: 272 MB % 296.91/42.93 % (395190)Instructions burned: 10545 (million) % 296.91/42.93 % (395250)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=4233609472:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2783 on theBenchmark for (2783ds/3201Mi) % 296.91/42.93 % (395252)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=2416383211:thitd=on:cond=on:i=4081:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2780 on theBenchmark for (2780ds/4081Mi) % 296.91/42.93 % (395199)Instruction limit reached! % 296.91/42.93 % (395199)------------------------------ % 296.91/42.93 % (395199)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 296.91/42.93 % (395199)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 296.91/42.93 % (395199)CaDiCaL version: 2.1.3 % 296.91/42.93 % (395199)Termination reason: Instruction limit % 296.91/42.93 % (395199)Termination phase: Saturation % 296.91/42.93 % (395199)Time elapsed: 9.087 s % 296.91/42.93 % (395199)Peak memory usage: 113 MB % 296.91/42.93 % (395199)Instructions burned: 13094 (million) % 296.91/42.93 % (395256)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=2811498745:cond=fast:i=20260:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2773 on theBenchmark for (2773ds/20260Mi) % 296.91/42.93 % (395256)Refutation not found, incomplete strategy % 296.91/42.93 % (395256)------------------------------ % 296.91/42.93 % (395256)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 296.91/42.93 % (395256)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 296.91/42.93 % (395256)CaDiCaL version: 2.1.3 % 296.91/42.93 % (395256)Termination reason: Refutation not found, incomplete strategy % 296.91/42.93 % (395256)Time elapsed: 0.037 s % 296.91/42.93 % (395256)Peak memory usage: 113 MB % 296.91/42.93 % (395256)Instructions burned: 18 (million) % 296.91/42.93 % (395256)------------------------------ % 296.91/42.93 % (395256)------------------------------ % 300.47/43.33 % (395258)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=3960341911:s2a=on:i=58627:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2766 on theBenchmark for (2766ds/58627Mi) % 300.47/43.33 % (395250)Instruction limit reached! % 300.47/43.33 % (395250)------------------------------ % 300.47/43.33 % (395250)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.47/43.33 % (395250)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.47/43.33 % (395250)CaDiCaL version: 2.1.3 % 300.47/43.33 % (395250)Termination reason: Instruction limit % 300.47/43.33 % (395250)Termination phase: Saturation % 300.47/43.33 % (395250)Time elapsed: 2.616 s % 300.47/43.33 % (395250)Peak memory usage: 100 MB % 300.47/43.33 % (395250)Instructions burned: 3202 (million) % 300.47/43.33 % (395248)Instruction limit reached! % 300.47/43.33 % (395248)------------------------------ % 300.47/43.33 % (395248)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.47/43.33 % (395248)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.47/43.33 % (395248)CaDiCaL version: 2.1.3 % 300.47/43.33 % (395248)Termination reason: Instruction limit % 300.47/43.33 % (395248)Termination phase: Saturation % 300.47/43.33 % (395248)Time elapsed: 3.472 s % 300.47/43.33 % (395248)Peak memory usage: 124 MB % 300.47/43.33 % (395248)Instructions burned: 3553 (million) % 300.47/43.33 % (395268)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=256072509:avsq=on:i=6258:avsqr=1,16:rtra=on:rawr=on_2754 on theBenchmark for (2754ds/6258Mi) % 300.47/43.33 % (395270)ott+10_128_isp=bottom:to=lpo:sil=128000:si=on:urr=on:uwa=alasca_main:sac=on:slsq=on:random_seed=1095390996:i=34001:aac=none:doe=on:rtra=on:gtg=exists_all_2752 on theBenchmark for (2752ds/34001Mi) % 300.47/43.33 % (395242)Instruction limit reached! % 300.47/43.33 % (395242)------------------------------ % 300.47/43.33 % (395242)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.47/43.33 % (395242)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.47/43.33 % (395242)CaDiCaL version: 2.1.3 % 300.47/43.33 % (395242)Termination reason: Instruction limit % 300.47/43.33 % (395242)Termination phase: Saturation % 300.47/43.33 % (395242)Time elapsed: 6.017 s % 300.47/43.33 % (395242)Peak memory usage: 195 MB % 300.47/43.33 % (395242)Instructions burned: 11748 (million) % 300.47/43.33 % (395274)lrs+2_10_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_main:tha=some:random_seed=507205965:s2a=on:i=71622:s2at=-1:rtra=on_2738 on theBenchmark for (2738ds/71622Mi) % 300.47/43.33 % (395252)Instruction limit reached! % 300.47/43.33 % (395252)------------------------------ % 300.47/43.33 % (395252)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.47/43.33 % (395252)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.47/43.33 % (395252)CaDiCaL version: 2.1.3 % 300.47/43.33 % (395252)Termination reason: Instruction limit % 300.47/43.33 % (395252)Termination phase: Saturation % 300.47/43.33 % (395252)Time elapsed: 4.192 s % 300.47/43.33 % (395252)Peak memory usage: 166 MB % 300.47/43.33 % (395252)Instructions burned: 4082 (million) % 300.47/43.33 % (395276)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=779310767:i=24001:kws=precedence:nm=0:rtra=on_2735 on theBenchmark for (2735ds/24001Mi) % 300.47/43.33 % (395197)Instruction limit reached! % 300.47/43.33 % (395197)------------------------------ % 300.47/43.33 % (395197)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.47/43.33 % (395197)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.47/43.33 % (395197)CaDiCaL version: 2.1.3 % 300.47/43.33 % (395197)Termination reason: Instruction limit % 300.47/43.33 % (395197)Termination phase: Saturation % 300.47/43.33 % (395197)Time elapsed: 13.547 s % 300.47/43.33 % (395197)Peak memory usage: 114 MB % 300.47/43.33 % (395197)Instructions burned: 17166 (million) % 300.47/43.33 % (395278)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=2777493094:i=2076:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2730 on theBenchmark for (2730ds/2076Mi) % 300.47/43.33 % (395278)Instruction limit reached! % 300.47/43.33 % (395278)------------------------------ % 300.47/43.33 % (395278)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.47/43.33 % (395278)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.47/43.33 % (395278)CaDiCaL version: 2.1.3 % 300.47/43.33 % (395278)Termination reason: Instruction % 300.47/43.34 Terminated %------------------------------------------------------------------------------