%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWW828_1 : TPTP v9.3.1. Released v7.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % Computer : n002.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:37:54 PM UTC 2026 % Result : Timeout 300.55s 42.94s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWW828_1 : TPTP v9.3.1. Released v7.0.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.09/0.19 % Computer : n002.cluster.edu % 0.09/0.19 % Model : x86_64 x86_64 % 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.19 % Memory : 8046.5625MB % 0.09/0.19 % OS : Linux 6.8.0-71-generic % 0.09/0.19 % CPULimit : 300 % 0.09/0.19 % WCLimit : 300 % 0.09/0.19 % DateTime : Mon Sep 28 14:33:37 UTC 2026 % 0.09/0.20 % CPUTime : % 0.09/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.09/0.23 Running first-order theorem proving % 0.09/0.23 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 3.37/1.24 % (393960)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule. % 3.37/1.24 % (393969)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=2110754591:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi) % 3.37/1.24 % (393969)Instruction limit reached! % 3.37/1.24 % (393969)------------------------------ % 3.37/1.24 % (393969)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.37/1.24 % (393969)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.37/1.24 % (393969)CaDiCaL version: 2.1.3 % 3.37/1.24 % (393969)Termination reason: Instruction limit % 3.37/1.24 % (393969)Termination phase: Property scanning % 3.37/1.24 % (393969)Time elapsed: 0.002 s % 3.37/1.24 % (393969)Peak memory usage: 85 MB % 3.37/1.24 % (393969)Instructions burned: 5 (million) % 3.37/1.24 % (393966)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=522357464:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi) % 3.37/1.24 % (393967)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=654036935:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi) % 3.37/1.24 % (393968)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=2606549582:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi) % 3.37/1.24 % (393965)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=694254721:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi) % 3.37/1.24 % (393968)Instruction limit reached! % 3.37/1.24 % (393968)------------------------------ % 3.37/1.24 % (393968)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.37/1.24 % (393968)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.37/1.24 % (393968)CaDiCaL version: 2.1.3 % 3.37/1.24 % (393968)Termination reason: Instruction limit % 3.37/1.24 % (393968)Termination phase: Property scanning % 3.37/1.24 % (393968)Time elapsed: 0.005 s % 3.37/1.24 % (393968)Peak memory usage: 85 MB % 3.37/1.24 % (393968)Instructions burned: 9 (million) % 3.37/1.24 % (393965)Instruction limit reached! % 3.37/1.24 % (393965)------------------------------ % 3.37/1.24 % (393965)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.37/1.24 % (393965)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.37/1.24 % (393965)CaDiCaL version: 2.1.3 % 3.37/1.24 % (393965)Termination reason: Instruction limit % 3.37/1.24 % (393965)Termination phase: Property scanning % 3.37/1.24 % (393965)Time elapsed: 0.006 s % 3.37/1.24 % (393965)Peak memory usage: 85 MB % 3.37/1.24 % (393965)Instructions burned: 13 (million) % 3.37/1.24 % (393970)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=2891924679:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi) % 3.37/1.24 % (393971)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=3033889441:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi) % 3.37/1.24 % (393971)Instruction limit reached! % 3.37/1.24 % (393971)------------------------------ % 3.37/1.24 % (393971)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.37/1.24 % (393971)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.37/1.24 % (393971)CaDiCaL version: 2.1.3 % 3.37/1.24 % (393971)Termination reason: Instruction limit % 3.37/1.24 % (393971)Termination phase: Preprocessing 3 % 3.37/1.24 % (393971)Time elapsed: 0.017 s % 3.37/1.24 % (393971)Peak memory usage: 87 MB % 3.37/1.24 % (393971)Instructions burned: 34 (million) % 3.37/1.24 % (393970)Instruction limit reached! % 3.37/1.24 % (393970)------------------------------ % 3.37/1.24 % (393970)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.37/1.24 % (393970)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.37/1.24 % (393970)CaDiCaL version: 2.1.3 % 3.37/1.24 % (393970)Termination reason: Instruction limit % 3.37/1.24 % (393970)Termination phase: Property scanning % 3.37/1.24 % (393970)Time elapsed: 0.026 s % 3.37/1.24 % (393970)Peak memory usage: 87 MB % 3.37/1.24 % (393970)Instructions burned: 48 (million) % 3.37/1.24 % (393973)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=2520542464:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2998 on theBenchmark for (2998ds/14Mi) % 3.37/1.24 % (393973)Instruction limit reached! % 3.37/1.24 % (393973)------------------------------ % 3.37/1.24 % (393973)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.42/1.40 % (393973)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.42/1.40 % (393973)CaDiCaL version: 2.1.3 % 4.42/1.40 % (393973)Termination reason: Instruction limit % 4.42/1.40 % (393973)Termination phase: SInE selection % 4.42/1.40 % (393973)Time elapsed: 0.004 s % 4.42/1.40 % (393973)Peak memory usage: 86 MB % 4.42/1.40 % (393973)Instructions burned: 15 (million) % 4.42/1.40 % (393967)Instruction limit reached! % 4.42/1.40 % (393967)------------------------------ % 4.42/1.40 % (393967)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.42/1.40 % (393967)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.42/1.40 % (393967)CaDiCaL version: 2.1.3 % 4.42/1.40 % (393967)Termination reason: Instruction limit % 4.42/1.40 % (393967)Termination phase: Saturation % 4.42/1.40 % (393967)Time elapsed: 0.132 s % 4.42/1.40 % (393967)Peak memory usage: 118 MB % 4.42/1.40 % (393967)Instructions burned: 202 (million) % 4.42/1.40 % (393981)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=3539502724:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2997 on theBenchmark for (2997ds/16Mi) % 4.42/1.40 % (393980)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=3182262984:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2997 on theBenchmark for (2997ds/29Mi) % 4.42/1.40 % (393981)Instruction limit reached! % 4.42/1.40 % (393981)------------------------------ % 4.42/1.40 % (393981)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.42/1.40 % (393981)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.42/1.40 % (393981)CaDiCaL version: 2.1.3 % 4.42/1.40 % (393981)Termination reason: Instruction limit % 4.42/1.40 % (393981)Termination phase: Preprocessing 1 % 4.42/1.40 % (393981)Time elapsed: 0.009 s % 4.42/1.40 % (393981)Peak memory usage: 86 MB % 4.42/1.40 % (393981)Instructions burned: 17 (million) % 4.42/1.40 % (393980)Instruction limit reached! % 4.42/1.40 % (393980)------------------------------ % 4.42/1.40 % (393980)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.42/1.40 % (393980)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.42/1.40 % (393980)CaDiCaL version: 2.1.3 % 4.42/1.40 % (393980)Termination reason: Instruction limit % 4.42/1.40 % (393980)Termination phase: Preprocessing 2 % 4.42/1.40 % (393980)Time elapsed: 0.015 s % 4.42/1.40 % (393980)Peak memory usage: 86 MB % 4.42/1.40 % (393980)Instructions burned: 29 (million) % 4.42/1.40 % (393982)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=3984552073:i=24:canc=force:rtra=on_2997 on theBenchmark for (2997ds/24Mi) % 4.42/1.40 % (393985)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=3605729057:i=85:gtgl=4:rtra=on:gtg=exists_sym_2997 on theBenchmark for (2997ds/85Mi) % 4.42/1.40 % (393982)Instruction limit reached! % 4.42/1.40 % (393982)------------------------------ % 4.42/1.40 % (393982)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.42/1.40 % (393982)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.42/1.40 % (393982)CaDiCaL version: 2.1.3 % 4.42/1.40 % (393982)Termination reason: Instruction limit % 4.42/1.40 % (393982)Termination phase: Preprocessing 1 % 4.42/1.40 % (393982)Time elapsed: 0.012 s % 4.42/1.40 % (393982)Peak memory usage: 86 MB % 4.42/1.40 % (393982)Instructions burned: 25 (million) % 4.42/1.40 % (393983)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=1735951361:i=27:canc=cautious:fsr=off:rtra=on_2997 on theBenchmark for (2997ds/27Mi) % 4.42/1.40 % (393985)Instruction limit reached! % 4.42/1.40 % (393985)------------------------------ % 4.42/1.40 % (393985)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.42/1.40 % (393985)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.42/1.40 % (393985)CaDiCaL version: 2.1.3 % 4.42/1.40 % (393985)Termination reason: Instruction limit % 4.42/1.40 % (393985)Termination phase: Function definition elimination % 4.42/1.40 % (393985)Time elapsed: 0.022 s % 4.42/1.40 % (393985)Peak memory usage: 88 MB % 4.42/1.40 % (393985)Instructions burned: 86 (million) % 4.42/1.40 % (393983)Instruction limit reached! % 4.42/1.40 % (393983)------------------------------ % 4.42/1.40 % (393983)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.49/1.54 % (393983)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.49/1.54 % (393983)CaDiCaL version: 2.1.3 % 5.49/1.54 % (393983)Termination reason: Instruction limit % 5.49/1.54 % (393983)Termination phase: Preprocessing 1 % 5.49/1.54 % (393983)Time elapsed: 0.014 s % 5.49/1.54 % (393983)Peak memory usage: 86 MB % 5.49/1.54 % (393983)Instructions burned: 28 (million) % 5.49/1.54 % (393966)Instruction limit reached! % 5.49/1.54 % (393966)------------------------------ % 5.49/1.54 % (393966)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.49/1.54 % (393966)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.49/1.54 % (393966)CaDiCaL version: 2.1.3 % 5.49/1.54 % (393966)Termination reason: Instruction limit % 5.49/1.54 % (393966)Termination phase: Saturation % 5.49/1.54 % (393966)Time elapsed: 0.205 s % 5.49/1.54 % (393966)Peak memory usage: 119 MB % 5.49/1.54 % (393966)Instructions burned: 307 (million) % 5.49/1.54 % (393986)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=366907717:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2996 on theBenchmark for (2996ds/2Mi) % 5.49/1.54 % (393986)Instruction limit reached! % 5.49/1.54 % (393986)------------------------------ % 5.49/1.54 % (393986)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.49/1.54 % (393986)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.49/1.54 % (393986)CaDiCaL version: 2.1.3 % 5.49/1.54 % (393986)Termination reason: Instruction limit % 5.49/1.54 % (393986)Termination phase: shuffling % 5.49/1.54 % (393986)Time elapsed: 0.002 s % 5.49/1.54 % (393986)Peak memory usage: 85 MB % 5.49/1.54 % (393986)Instructions burned: 2 (million) % 5.49/1.54 % (393989)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=1344800635:i=181:rtra=on:ss=axioms:ev=cautious_2996 on theBenchmark for (2996ds/181Mi) % 5.49/1.54 % (393990)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=177173004:i=4:ep=RST:ins=2:rtra=on_2996 on theBenchmark for (2996ds/4Mi) % 5.49/1.54 % (393995)lrs+10_1_thi=all:si=on:fd=off:random_seed=502012048:i=53:rtra=on:gtg=all_2995 on theBenchmark for (2995ds/53Mi) % 5.49/1.54 % (393990)Instruction limit reached! % 5.49/1.54 % (393990)------------------------------ % 5.49/1.54 % (393990)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.49/1.54 % (393990)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.49/1.54 % (393990)CaDiCaL version: 2.1.3 % 5.49/1.54 % (393990)Termination reason: Instruction limit % 5.49/1.54 % (393990)Termination phase: Property scanning % 5.49/1.54 % (393990)Time elapsed: 0.003 s % 5.49/1.54 % (393990)Peak memory usage: 85 MB % 5.49/1.54 % (393990)Instructions burned: 4 (million) % 5.49/1.54 % (393989)Refutation not found, incomplete strategy % 5.49/1.54 % (393989)------------------------------ % 5.49/1.54 % (393989)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.49/1.54 % (393989)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.49/1.54 % (393989)CaDiCaL version: 2.1.3 % 5.49/1.54 % (393989)Termination reason: Refutation not found, incomplete strategy % 5.49/1.54 % (393989)Time elapsed: 0.010 s % 5.49/1.54 % (393989)Peak memory usage: 88 MB % 5.49/1.54 % (393989)Instructions burned: 17 (million) % 5.49/1.54 % (393995)Instruction limit reached! % 5.49/1.54 % (393995)------------------------------ % 5.49/1.54 % (393995)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.49/1.54 % (393995)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.49/1.54 % (393995)CaDiCaL version: 2.1.3 % 5.49/1.54 % (393995)Termination reason: Instruction limit % 5.49/1.54 % (393995)Termination phase: Preprocessing 3 % 5.49/1.54 % (393995)Time elapsed: 0.014 s % 5.49/1.54 % (393995)Peak memory usage: 87 MB % 5.49/1.54 % (393995)Instructions burned: 56 (million) % 5.49/1.54 % (393994)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=2545302282:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2996 on theBenchmark for (2996ds/66Mi) % 5.49/1.54 % (393996)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=3638034014:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2995 on theBenchmark for (2995ds/8Mi) % 5.49/1.54 % (393994)Instruction limit reached! % 5.49/1.54 % (393994)------------------------------ % 5.49/1.54 % (393994)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.60/1.77 % (393994)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.60/1.77 % (393994)CaDiCaL version: 2.1.3 % 6.60/1.77 % (393994)Termination reason: Instruction limit % 6.60/1.77 % (393994)Termination phase: Function definition elimination % 6.60/1.77 % (393994)Time elapsed: 0.036 s % 6.60/1.77 % (393994)Peak memory usage: 88 MB % 6.60/1.77 % (393994)Instructions burned: 67 (million) % 6.60/1.77 % (393996)Instruction limit reached! % 6.60/1.77 % (393996)------------------------------ % 6.60/1.77 % (393996)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.60/1.77 % (393996)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.60/1.77 % (393996)CaDiCaL version: 2.1.3 % 6.60/1.77 % (393996)Termination reason: Instruction limit % 6.60/1.77 % (393996)Termination phase: Property scanning % 6.60/1.77 % (393996)Time elapsed: 0.004 s % 6.60/1.77 % (393996)Peak memory usage: 85 MB % 6.60/1.77 % (393996)Instructions burned: 8 (million) % 6.60/1.77 % (393997)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=3352490223:st=3:i=2:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/2Mi) % 6.60/1.77 % (393997)Instruction limit reached! % 6.60/1.77 % (393997)------------------------------ % 6.60/1.77 % (393997)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.60/1.77 % (393997)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.60/1.77 % (393997)CaDiCaL version: 2.1.3 % 6.60/1.77 % (393997)Termination reason: Instruction limit % 6.60/1.77 % (393997)Termination phase: shuffling % 6.60/1.77 % (393997)Time elapsed: 0.002 s % 6.60/1.77 % (393997)Peak memory usage: 85 MB % 6.60/1.77 % (393997)Instructions burned: 2 (million) % 6.60/1.77 % (394004)dis+10_1_si=on:random_seed=1212385165:i=10:ep=R:rtra=on_2994 on theBenchmark for (2994ds/10Mi) % 6.60/1.77 % (394004)Instruction limit reached! % 6.60/1.77 % (394004)------------------------------ % 6.60/1.77 % (394004)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.60/1.77 % (394004)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.60/1.77 % (394004)CaDiCaL version: 2.1.3 % 6.60/1.77 % (394004)Termination reason: Instruction limit % 6.60/1.77 % (394004)Termination phase: Property scanning % 6.60/1.77 % (394004)Time elapsed: 0.003 s % 6.60/1.77 % (394004)Peak memory usage: 85 MB % 6.60/1.77 % (394004)Instructions burned: 10 (million) % 6.60/1.77 % (394000)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=4070304624:i=2:doe=on:canc=force:asg=cautious:rtra=on_2995 on theBenchmark for (2995ds/2Mi) % 6.60/1.77 % (394000)Instruction limit reached! % 6.60/1.77 % (394000)------------------------------ % 6.60/1.77 % (394000)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.60/1.77 % (394000)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.60/1.77 % (394000)CaDiCaL version: 2.1.3 % 6.60/1.77 % (394000)Termination reason: Instruction limit % 6.60/1.77 % (394000)Termination phase: shuffling % 6.60/1.77 % (394000)Time elapsed: 0.002 s % 6.60/1.77 % (394000)Peak memory usage: 85 MB % 6.60/1.77 % (394000)Instructions burned: 2 (million) % 6.60/1.77 % (394003)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=1175150476:i=127:doe=on:rtra=on_2994 on theBenchmark for (2994ds/127Mi) % 6.60/1.77 % (394008)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=1014092215: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_2994 on theBenchmark for (2994ds/35Mi) % 6.60/1.77 % (394007)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=506668227:i=26:canc=cautious:av=off:rtra=on_2994 on theBenchmark for (2994ds/26Mi) % 6.60/1.77 % (394007)Instruction limit reached! % 6.60/1.77 % (394007)------------------------------ % 6.60/1.77 % (394007)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.60/1.77 % (394007)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.60/1.77 % (394007)CaDiCaL version: 2.1.3 % 6.60/1.77 % (394007)Termination reason: Instruction limit % 6.60/1.77 % (394007)Termination phase: Preprocessing 1 % 6.60/1.77 % (394007)Time elapsed: 0.013 s % 6.60/1.77 % (394007)Peak memory usage: 86 MB % 6.60/1.77 % (394007)Instructions burned: 26 (million) % 6.60/1.77 % (394010)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=2594333710:i=2:fsr=off:rtra=on:inst=on_2994 on theBenchmark for (2994ds/2Mi) % 9.79/2.06 % (394008)Instruction limit reached! % 9.79/2.06 % (394008)------------------------------ % 9.79/2.06 % (394008)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.79/2.06 % (394008)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.79/2.06 % (394008)CaDiCaL version: 2.1.3 % 9.79/2.06 % (394008)Termination reason: Instruction limit % 9.79/2.06 % (394008)Termination phase: Preprocessing 3 % 9.79/2.06 % (394008)Time elapsed: 0.020 s % 9.79/2.06 % (394008)Peak memory usage: 87 MB % 9.79/2.06 % (394008)Instructions burned: 38 (million) % 9.79/2.06 % (394010)Instruction limit reached! % 9.79/2.06 % (394010)------------------------------ % 9.79/2.06 % (394010)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.79/2.06 % (394010)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.79/2.06 % (394010)CaDiCaL version: 2.1.3 % 9.79/2.06 % (394010)Termination reason: Instruction limit % 9.79/2.06 % (394010)Termination phase: Property scanning % 9.79/2.06 % (394010)Time elapsed: 0.003 s % 9.79/2.06 % (394010)Peak memory usage: 85 MB % 9.79/2.06 % (394010)Instructions burned: 3 (million) % 9.79/2.06 % (394003)Instruction limit reached! % 9.79/2.06 % (394003)------------------------------ % 9.79/2.06 % (394003)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.79/2.06 % (394003)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.79/2.06 % (394003)CaDiCaL version: 2.1.3 % 9.79/2.06 % (394003)Termination reason: Instruction limit % 9.79/2.06 % (394003)Termination phase: Saturation % 9.79/2.06 % (394003)Time elapsed: 0.092 s % 9.79/2.06 % (394003)Peak memory usage: 115 MB % 9.79/2.06 % (394003)Instructions burned: 127 (million) % 9.79/2.06 % (394012)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=4148273362:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2993 on theBenchmark for (2993ds/8Mi) % 9.79/2.06 % (394012)Instruction limit reached! % 9.79/2.06 % (394012)------------------------------ % 9.79/2.06 % (394012)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.79/2.06 % (394012)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.79/2.06 % (394012)CaDiCaL version: 2.1.3 % 9.79/2.06 % (394012)Termination reason: Instruction limit % 9.79/2.06 % (394012)Termination phase: Property scanning % 9.79/2.06 % (394012)Time elapsed: 0.003 s % 9.79/2.06 % (394012)Peak memory usage: 85 MB % 9.79/2.06 % (394012)Instructions burned: 10 (million) % 9.79/2.06 % (393989)------------------------------ % 9.79/2.06 % (393989)------------------------------ % 9.79/2.06 % (394014)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=820228863:i=370:ep=RS:fsr=off:rtra=on_2993 on theBenchmark for (2993ds/370Mi) % 9.79/2.06 % (394018)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=847636811:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2992 on theBenchmark for (2992ds/13Mi) % 9.79/2.06 % (394021)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=543668879:i=10:rtra=on_2992 on theBenchmark for (2992ds/10Mi) % 9.79/2.06 % (394018)Instruction limit reached! % 9.79/2.06 % (394018)------------------------------ % 9.79/2.06 % (394018)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.79/2.06 % (394018)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.79/2.06 % (394020)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=15603778:i=226:rtra=on:gtg=position:ss=axioms_2992 on theBenchmark for (2992ds/226Mi) % 9.79/2.06 % (394018)CaDiCaL version: 2.1.3 % 9.79/2.06 % (394018)Termination reason: Instruction limit % 9.79/2.06 % (394018)Termination phase: Property scanning % 9.79/2.06 % (394018)Time elapsed: 0.006 s % 9.79/2.06 % (394018)Peak memory usage: 85 MB % 9.79/2.06 % (394018)Instructions burned: 14 (million) % 9.79/2.06 % (394021)Instruction limit reached! % 9.79/2.06 % (394021)------------------------------ % 9.79/2.06 % (394021)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.79/2.06 % (394021)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.79/2.06 % (394021)CaDiCaL version: 2.1.3 % 9.79/2.06 % (394021)Termination reason: Instruction limit % 9.79/2.06 % (394021)Termination phase: Property scanning % 9.79/2.06 % (394021)Time elapsed: 0.007 s % 9.79/2.06 % (394021)Peak memory usage: 85 MB % 9.79/2.06 % (394021)Instructions burned: 13 (million) % 9.79/2.06 % (394024)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=3940517860:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2992 on theBenchmark for (2992ds/75Mi) % 10.69/2.26 % (394024)Instruction limit reached! % 10.69/2.26 % (394024)------------------------------ % 10.69/2.26 % (394024)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.69/2.26 % (394024)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.69/2.26 % (394024)CaDiCaL version: 2.1.3 % 10.69/2.26 % (394024)Termination reason: Instruction limit % 10.69/2.26 % (394024)Termination phase: Property scanning % 10.69/2.26 % (394024)Time elapsed: 0.020 s % 10.69/2.26 % (394024)Peak memory usage: 88 MB % 10.69/2.26 % (394024)Instructions burned: 76 (million) % 10.69/2.26 % (394020)Refutation not found, incomplete strategy % 10.69/2.26 % (394020)------------------------------ % 10.69/2.26 % (394020)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.69/2.26 % (394020)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.69/2.26 % (394020)CaDiCaL version: 2.1.3 % 10.69/2.26 % (394020)Termination reason: Refutation not found, incomplete strategy % 10.69/2.26 % (394020)Time elapsed: 0.040 s % 10.69/2.26 % (394020)Peak memory usage: 111 MB % 10.69/2.26 % (394020)Instructions burned: 32 (million) % 10.69/2.26 % (394023)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=2264858335:i=71:rtra=on:gtg=exists_top_2992 on theBenchmark for (2992ds/71Mi) % 10.69/2.26 % (394025)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=2889282488:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2992 on theBenchmark for (2992ds/294Mi) % 10.69/2.26 % (394023)Instruction limit reached! % 10.69/2.26 % (394023)------------------------------ % 10.69/2.26 % (394023)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.69/2.26 % (394023)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.69/2.26 % (394023)CaDiCaL version: 2.1.3 % 10.69/2.26 % (394023)Termination reason: Instruction limit % 10.69/2.26 % (394023)Termination phase: Function definition elimination % 10.69/2.26 % (394023)Time elapsed: 0.037 s % 10.69/2.26 % (394023)Peak memory usage: 88 MB % 10.69/2.26 % (394023)Instructions burned: 72 (million) % 10.69/2.26 % (394033)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=2026960288:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2991 on theBenchmark for (2991ds/40Mi) % 10.69/2.26 % (394032)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=3027698286:i=131:rtra=on_2991 on theBenchmark for (2991ds/131Mi) % 10.69/2.26 % (394031)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=1955797291:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2991 on theBenchmark for (2991ds/130Mi) % 10.69/2.26 % (394014)Instruction limit reached! % 10.69/2.26 % (394014)------------------------------ % 10.69/2.26 % (394014)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.69/2.26 % (394014)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.69/2.26 % (394014)CaDiCaL version: 2.1.3 % 10.69/2.26 % (394014)Termination reason: Instruction limit % 10.69/2.26 % (394014)Termination phase: Saturation % 10.69/2.26 % (394014)Time elapsed: 0.205 s % 10.69/2.26 % (394014)Peak memory usage: 93 MB % 10.69/2.26 % (394014)Instructions burned: 372 (million) % 10.69/2.26 % (394033)Instruction limit reached! % 10.69/2.26 % (394033)------------------------------ % 10.69/2.26 % (394033)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.69/2.26 % (394033)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.69/2.26 % (394033)CaDiCaL version: 2.1.3 % 10.69/2.26 % (394033)Termination reason: Instruction limit % 10.69/2.26 % (394033)Termination phase: Property scanning % 10.69/2.26 % (394033)Time elapsed: 0.009 s % 10.69/2.26 % (394033)Peak memory usage: 86 MB % 10.69/2.26 % (394033)Instructions burned: 41 (million) % 10.69/2.26 % (394031)Instruction limit reached! % 10.69/2.26 % (394031)------------------------------ % 10.69/2.26 % (394031)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.69/2.26 % (394031)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.69/2.26 % (394031)CaDiCaL version: 2.1.3 % 10.69/2.26 % (394031)Termination reason: Instruction limit % 10.69/2.26 % (394031)Termination phase: Saturation % 10.69/2.26 % (394031)Time elapsed: 0.089 s % 12.19/2.61 % (394031)Peak memory usage: 115 MB % 12.19/2.61 % (394031)Instructions burned: 130 (million) % 12.19/2.61 % (394025)Instruction limit reached! % 12.19/2.61 % (394025)------------------------------ % 12.19/2.61 % (394025)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.19/2.61 % (394025)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.19/2.61 % (394025)CaDiCaL version: 2.1.3 % 12.19/2.61 % (394025)Termination reason: Instruction limit % 12.19/2.61 % (394025)Termination phase: Saturation % 12.19/2.61 % (394025)Time elapsed: 0.179 s % 12.19/2.61 % (394025)Peak memory usage: 93 MB % 12.19/2.61 % (394025)Instructions burned: 294 (million) % 12.19/2.61 % (394036)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=1687570243:i=307:rtra=on:gtg=exists_top_2990 on theBenchmark for (2990ds/307Mi) % 12.19/2.61 % (394032)Instruction limit reached! % 12.19/2.61 % (394032)------------------------------ % 12.19/2.61 % (394032)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.19/2.61 % (394032)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.19/2.61 % (394032)CaDiCaL version: 2.1.3 % 12.19/2.61 % (394032)Termination reason: Instruction limit % 12.19/2.61 % (394032)Termination phase: Saturation % 12.19/2.61 % (394032)Time elapsed: 0.116 s % 12.19/2.61 % (394032)Peak memory usage: 135 MB % 12.19/2.61 % (394032)Instructions burned: 131 (million) % 12.19/2.61 % (394040)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=1362550463:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2989 on theBenchmark for (2989ds/598Mi) % 12.19/2.61 % (394020)------------------------------ % 12.19/2.61 % (394020)------------------------------ % 12.19/2.61 % (394041)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=978085977:i=131:canc=cautious:fsr=off:rtra=on_2989 on theBenchmark for (2989ds/131Mi) % 12.19/2.61 % (394042)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=3341561028:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2988 on theBenchmark for (2988ds/259Mi) % 12.19/2.61 % (394043)dis+10_1_si=on:random_seed=1079589659:s2a=on:i=1000:rtra=on:gtg=exists_all_2988 on theBenchmark for (2988ds/1000Mi) % 12.19/2.61 % (394036)Instruction limit reached! % 12.19/2.61 % (394036)------------------------------ % 12.19/2.61 % (394036)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.19/2.61 % (394036)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.19/2.61 % (394036)CaDiCaL version: 2.1.3 % 12.19/2.61 % (394036)Termination reason: Instruction limit % 12.19/2.61 % (394036)Termination phase: Saturation % 12.19/2.61 % (394036)Time elapsed: 0.152 s % 12.19/2.61 % (394036)Peak memory usage: 92 MB % 12.19/2.61 % (394036)Instructions burned: 307 (million) % 12.19/2.61 % (394041)Instruction limit reached! % 12.19/2.61 % (394041)------------------------------ % 12.19/2.61 % (394041)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.19/2.61 % (394041)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.19/2.61 % (394041)CaDiCaL version: 2.1.3 % 12.19/2.61 % (394041)Termination reason: Instruction limit % 12.19/2.61 % (394041)Termination phase: Saturation % 12.19/2.61 % (394041)Time elapsed: 0.093 s % 12.19/2.61 % (394041)Peak memory usage: 118 MB % 12.19/2.61 % (394041)Instructions burned: 132 (million) % 12.19/2.61 % (394046)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=26077119:i=383:fsr=off:rtra=on:ev=force_2988 on theBenchmark for (2988ds/383Mi) % 12.19/2.61 % (394042)Refutation not found, incomplete strategy % 12.19/2.61 % (394042)------------------------------ % 12.19/2.61 % (394042)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.19/2.61 % (394042)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.19/2.61 % (394042)CaDiCaL version: 2.1.3 % 12.19/2.61 % (394042)Termination reason: Refutation not found, incomplete strategy % 12.19/2.61 % (394042)Time elapsed: 0.041 s % 12.19/2.61 % (394042)Peak memory usage: 111 MB % 12.19/2.61 % (394042)Instructions burned: 34 (million) % 12.19/2.61 % (394047)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=1332261065:i=141:doe=on:rtra=on_2988 on theBenchmark for (2988ds/141Mi) % 12.19/2.61 % (394040)Instruction limit reached! % 12.19/2.61 % (394040)------------------------------ % 12.19/2.61 % (394040)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.14/2.80 % (394040)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.14/2.80 % (394040)CaDiCaL version: 2.1.3 % 14.14/2.80 % (394040)Termination reason: Instruction limit % 14.14/2.80 % (394040)Termination phase: Saturation % 14.14/2.80 % (394040)Time elapsed: 0.246 s % 14.14/2.80 % (394040)Peak memory usage: 140 MB % 14.14/2.80 % (394040)Instructions burned: 602 (million) % 14.14/2.80 % (394047)Instruction limit reached! % 14.14/2.80 % (394047)------------------------------ % 14.14/2.80 % (394047)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.14/2.80 % (394047)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.14/2.80 % (394047)CaDiCaL version: 2.1.3 % 14.14/2.80 % (394047)Termination reason: Instruction limit % 14.14/2.80 % (394047)Termination phase: Saturation % 14.14/2.80 % (394047)Time elapsed: 0.078 s % 14.14/2.80 % (394047)Peak memory usage: 91 MB % 14.14/2.80 % (394047)Instructions burned: 141 (million) % 14.14/2.80 % (394051)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=3243888093:i=65:nm=16:rtra=on_2987 on theBenchmark for (2987ds/65Mi) % 14.14/2.80 % (394053)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=3829776531:i=121:nm=16:rtra=on_2987 on theBenchmark for (2987ds/121Mi) % 14.14/2.80 % (394051)Instruction limit reached! % 14.14/2.80 % (394051)------------------------------ % 14.14/2.80 % (394051)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.14/2.80 % (394051)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.14/2.80 % (394051)CaDiCaL version: 2.1.3 % 14.14/2.80 % (394051)Termination reason: Instruction limit % 14.14/2.80 % (394051)Termination phase: Property scanning % 14.14/2.80 % (394051)Time elapsed: 0.034 s % 14.14/2.80 % (394051)Peak memory usage: 88 MB % 14.14/2.80 % (394051)Instructions burned: 67 (million) % 14.14/2.80 % (394053)Instruction limit reached! % 14.14/2.80 % (394053)------------------------------ % 14.14/2.80 % (394053)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.14/2.80 % (394053)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.14/2.80 % (394053)CaDiCaL version: 2.1.3 % 14.14/2.80 % (394053)Termination reason: Instruction limit % 14.14/2.80 % (394053)Termination phase: Saturation % 14.14/2.80 % (394053)Time elapsed: 0.062 s % 14.14/2.80 % (394053)Peak memory usage: 90 MB % 14.14/2.80 % (394053)Instructions burned: 121 (million) % 14.14/2.80 % (394055)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=868285661:s2a=on:i=128:s2at=5:ins=3:rtra=on_2986 on theBenchmark for (2986ds/128Mi) % 14.14/2.80 % (394046)Instruction limit reached! % 14.14/2.80 % (394046)------------------------------ % 14.14/2.80 % (394046)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.14/2.80 % (394046)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.14/2.80 % (394046)CaDiCaL version: 2.1.3 % 14.14/2.80 % (394046)Termination reason: Instruction limit % 14.14/2.80 % (394046)Termination phase: Saturation % 14.14/2.80 % (394046)Time elapsed: 0.226 s % 14.14/2.80 % (394046)Peak memory usage: 97 MB % 14.14/2.80 % (394046)Instructions burned: 384 (million) % 14.14/2.80 % (394042)------------------------------ % 14.14/2.80 % (394042)------------------------------ % 14.14/2.80 % (394055)Instruction limit reached! % 14.14/2.80 % (394055)------------------------------ % 14.14/2.80 % (394055)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.14/2.80 % (394055)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.14/2.80 % (394055)CaDiCaL version: 2.1.3 % 14.14/2.80 % (394055)Termination reason: Instruction limit % 14.14/2.80 % (394055)Termination phase: Saturation % 14.14/2.80 % (394055)Time elapsed: 0.038 s % 14.14/2.80 % (394055)Peak memory usage: 91 MB % 14.14/2.80 % (394055)Instructions burned: 129 (million) % 14.14/2.80 % (394057)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=1319048476:i=39:ins=3:rtra=on_2985 on theBenchmark for (2985ds/39Mi) % 14.14/2.80 % (394057)Instruction limit reached! % 14.14/2.80 % (394057)------------------------------ % 14.14/2.80 % (394057)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.14/2.80 % (394057)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.14/2.80 % (394057)CaDiCaL version: 2.1.3 % 14.14/2.80 % (394057)Termination reason: Instruction limit % 14.14/2.80 % (394057)Termination phase: Preprocessing 3 % 14.14/2.80 % (394057)Time elapsed: 0.023 s % 17.44/3.19 % (394057)Peak memory usage: 87 MB % 17.44/3.19 % (394057)Instructions burned: 41 (million) % 17.44/3.19 % (394059)dis+1010_1_to=kbo:si=on:random_seed=1122641360:i=175:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2985 on theBenchmark for (2985ds/175Mi) % 17.44/3.19 % (394061)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=338034117:i=329:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2985 on theBenchmark for (2985ds/329Mi) % 17.44/3.19 % (394063)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=3853264348:thitd=on:i=215:nm=0:rtra=on:ev=force_2984 on theBenchmark for (2984ds/215Mi) % 17.44/3.19 % (394062)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=3766757449:s2a=on:i=483:doe=on:nm=32:rtra=on_2984 on theBenchmark for (2984ds/483Mi) % 17.44/3.19 % (394064)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=2343398942:i=349:rtra=on_2984 on theBenchmark for (2984ds/349Mi) % 17.44/3.19 % (394059)Instruction limit reached! % 17.44/3.19 % (394059)------------------------------ % 17.44/3.19 % (394059)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.44/3.19 % (394059)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.44/3.19 % (394059)CaDiCaL version: 2.1.3 % 17.44/3.19 % (394059)Termination reason: Instruction limit % 17.44/3.19 % (394059)Termination phase: Saturation % 17.44/3.19 % (394059)Time elapsed: 0.110 s % 17.44/3.19 % (394059)Peak memory usage: 91 MB % 17.44/3.19 % (394059)Instructions burned: 176 (million) % 17.44/3.19 % (394063)Instruction limit reached! % 17.44/3.19 % (394063)------------------------------ % 17.44/3.19 % (394063)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.44/3.19 % (394063)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.44/3.19 % (394063)CaDiCaL version: 2.1.3 % 17.44/3.19 % (394063)Termination reason: Instruction limit % 17.44/3.19 % (394063)Termination phase: Saturation % 17.44/3.19 % (394063)Time elapsed: 0.089 s % 17.44/3.19 % (394063)Peak memory usage: 138 MB % 17.44/3.19 % (394063)Instructions burned: 217 (million) % 17.44/3.19 % (394067)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=2652007450:st=2:i=295:rtra=on:ss=axioms_2984 on theBenchmark for (2984ds/295Mi) % 17.44/3.19 % (394067)Refutation not found, incomplete strategy % 17.44/3.19 % (394067)------------------------------ % 17.44/3.19 % (394067)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.44/3.19 % (394067)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.44/3.19 % (394067)CaDiCaL version: 2.1.3 % 17.44/3.19 % (394067)Termination reason: Refutation not found, incomplete strategy % 17.44/3.19 % (394067)Time elapsed: 0.015 s % 17.44/3.19 % (394067)Peak memory usage: 88 MB % 17.44/3.19 % (394067)Instructions burned: 29 (million) % 17.44/3.19 % (394043)Instruction limit reached! % 17.44/3.19 % (394043)------------------------------ % 17.44/3.19 % (394043)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.44/3.19 % (394043)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.44/3.19 % (394043)CaDiCaL version: 2.1.3 % 17.44/3.19 % (394043)Termination reason: Instruction limit % 17.44/3.19 % (394043)Termination phase: Saturation % 17.44/3.19 % (394043)Time elapsed: 0.556 s % 17.44/3.19 % (394043)Peak memory usage: 95 MB % 17.44/3.19 % (394043)Instructions burned: 1000 (million) % 17.44/3.19 % (394061)Instruction limit reached! % 17.44/3.19 % (394061)------------------------------ % 17.44/3.19 % (394061)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.44/3.19 % (394061)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.44/3.19 % (394061)CaDiCaL version: 2.1.3 % 17.44/3.19 % (394061)Termination reason: Instruction limit % 17.44/3.19 % (394061)Termination phase: Saturation % 17.44/3.19 % (394061)Time elapsed: 0.203 s % 17.44/3.19 % (394061)Peak memory usage: 119 MB % 17.44/3.19 % (394061)Instructions burned: 330 (million) % 17.44/3.19 % (394072)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=201706501:i=328:kws=inv_frequency:nm=20:rtra=on_2982 on theBenchmark for (2982ds/328Mi) % 17.44/3.19 % (394073)dis+1010_1_to=lpo:sil=128000:sas=z3:si=on:nwc=5:random_seed=742732008:i=281:gtgl=2:rtra=on:gtg=all_2982 on theBenchmark for (2982ds/281Mi) % 17.44/3.19 % (394064)Instruction limit reached! % 18.10/3.41 % (394064)------------------------------ % 18.10/3.41 % (394064)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.10/3.41 % (394064)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.10/3.41 % (394064)CaDiCaL version: 2.1.3 % 18.10/3.41 % (394064)Termination reason: Instruction limit % 18.10/3.41 % (394064)Termination phase: Saturation % 18.10/3.41 % (394064)Time elapsed: 0.236 s % 18.10/3.41 % (394064)Peak memory usage: 120 MB % 18.10/3.41 % (394064)Instructions burned: 349 (million) % 18.10/3.41 % (394073)Instruction limit reached! % 18.10/3.41 % (394073)------------------------------ % 18.10/3.41 % (394073)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.10/3.41 % (394073)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.10/3.41 % (394073)CaDiCaL version: 2.1.3 % 18.10/3.41 % (394073)Termination reason: Instruction limit % 18.10/3.41 % (394073)Termination phase: Saturation % 18.10/3.41 % (394073)Time elapsed: 0.098 s % 18.10/3.41 % (394073)Peak memory usage: 119 MB % 18.10/3.41 % (394073)Instructions burned: 282 (million) % 18.10/3.41 % (394075)lrs+1010_1_to=kbo:sil=128000:si=on:sos=on:urr=on:uwa=alasca_main:random_seed=386820826:i=484:doe=on:nm=0:av=off:rtra=on:ss=axioms_2981 on theBenchmark for (2981ds/484Mi) % 18.10/3.41 % (394075)Refutation not found, incomplete strategy % 18.10/3.41 % (394075)------------------------------ % 18.10/3.41 % (394075)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.10/3.41 % (394075)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.10/3.41 % (394075)CaDiCaL version: 2.1.3 % 18.10/3.41 % (394075)Termination reason: Refutation not found, incomplete strategy % 18.10/3.41 % (394075)Time elapsed: 0.015 s % 18.10/3.41 % (394075)Peak memory usage: 88 MB % 18.10/3.41 % (394075)Instructions burned: 28 (million) % 18.10/3.41 % (394062)Instruction limit reached! % 18.10/3.41 % (394062)------------------------------ % 18.10/3.41 % (394062)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.10/3.41 % (394062)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.10/3.41 % (394062)CaDiCaL version: 2.1.3 % 18.10/3.41 % (394062)Termination reason: Instruction limit % 18.10/3.41 % (394062)Termination phase: Saturation % 18.10/3.41 % (394062)Time elapsed: 0.349 s % 18.10/3.41 % (394062)Peak memory usage: 137 MB % 18.10/3.41 % (394062)Instructions burned: 484 (million) % 18.10/3.41 % (394077)lrs+21_1_to=kbo:sil=128000:thi=neg_eq:si=on:random_seed=3534615268:i=321:canc=force:rtra=on:tac=axiom:ss=axioms:ev=force_2981 on theBenchmark for (2981ds/321Mi) % 18.10/3.41 % (394067)------------------------------ % 18.10/3.41 % (394067)------------------------------ % 18.10/3.41 % (394077)Refutation not found, incomplete strategy % 18.10/3.41 % (394077)------------------------------ % 18.10/3.41 % (394077)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.10/3.41 % (394077)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.10/3.41 % (394077)CaDiCaL version: 2.1.3 % 18.10/3.41 % (394077)Termination reason: Refutation not found, incomplete strategy % 18.10/3.41 % (394077)Time elapsed: 0.040 s % 18.10/3.41 % (394077)Peak memory usage: 112 MB % 18.10/3.41 % (394077)Instructions burned: 32 (million) % 18.10/3.41 % (394072)Instruction limit reached! % 18.10/3.41 % (394072)------------------------------ % 18.10/3.41 % (394072)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.10/3.41 % (394072)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.10/3.41 % (394072)CaDiCaL version: 2.1.3 % 18.10/3.41 % (394072)Termination reason: Instruction limit % 18.10/3.41 % (394072)Termination phase: Saturation % 18.10/3.41 % (394072)Time elapsed: 0.221 s % 18.10/3.41 % (394072)Peak memory usage: 119 MB % 18.10/3.41 % (394072)Instructions burned: 328 (million) % 18.10/3.41 % (394080)lrs+1010_1_to=kbo:tgt=ground:fde=unused:sas=z3:si=on:sp=unary_frequency:gve=force:spb=goal:tha=off:random_seed=1119752395:i=471:thf=on:kws=precedence:rtra=on_2980 on theBenchmark for (2980ds/471Mi) % 18.10/3.41 % (394079)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=3721099335:i=416:rtra=on:gtg=position:ss=axioms_2980 on theBenchmark for (2980ds/416Mi) % 18.10/3.41 % (394079)Refutation not found, incomplete strategy % 18.10/3.41 % (394079)------------------------------ % 18.10/3.41 % (394079)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.10/3.41 % (394079)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.45/3.83 % (394079)CaDiCaL version: 2.1.3 % 20.45/3.83 % (394079)Termination reason: Refutation not found, incomplete strategy % 20.45/3.83 % (394079)Time elapsed: 0.039 s % 20.45/3.83 % (394079)Peak memory usage: 111 MB % 20.45/3.83 % (394079)Instructions burned: 32 (million) % 20.45/3.83 % (394084)lrs+1010_2_to=kbo:sil=128000:tgt=ground:fde=unused:sas=z3:si=on:uwa=off:tha=off:nwc=1:random_seed=2720945382:i=375:kws=inv_arity_squared:rtra=on_2979 on theBenchmark for (2979ds/375Mi) % 20.45/3.83 % (394083)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=603077454:avsq=on:i=276:avsqr=1,2:rtra=on_2979 on theBenchmark for (2979ds/276Mi) % 20.45/3.83 % (394075)------------------------------ % 20.45/3.83 % (394075)------------------------------ % 20.45/3.83 % (394087)lrs+10_1_to=kbo:sil=128000:tgt=full:sas=z3:si=on:uwa=func_ext:slsqc=1:flr=on:slsq=on:random_seed=2091525797:i=387:bd=preordered:rtra=on:ss=axioms:sgt=8_2979 on theBenchmark for (2979ds/387Mi) % 20.45/3.83 % (394080)Instruction limit reached! % 20.45/3.83 % (394080)------------------------------ % 20.45/3.83 % (394080)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.45/3.84 % (394080)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.45/3.84 % (394080)CaDiCaL version: 2.1.3 % 20.45/3.84 % (394080)Termination reason: Instruction limit % 20.45/3.84 % (394080)Termination phase: Saturation % 20.45/3.84 % (394080)Time elapsed: 0.170 s % 20.45/3.84 % (394080)Peak memory usage: 122 MB % 20.45/3.84 % (394080)Instructions burned: 472 (million) % 20.45/3.84 % (394087)Refutation not found, incomplete strategy % 20.45/3.84 % (394087)------------------------------ % 20.45/3.84 % (394087)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.45/3.84 % (394087)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.45/3.84 % (394087)CaDiCaL version: 2.1.3 % 20.45/3.84 % (394087)Termination reason: Refutation not found, incomplete strategy % 20.45/3.84 % (394087)Time elapsed: 0.042 s % 20.45/3.84 % (394087)Peak memory usage: 112 MB % 20.45/3.84 % (394087)Instructions burned: 35 (million) % 20.45/3.84 % (394077)------------------------------ % 20.45/3.84 % (394077)------------------------------ % 20.45/3.84 % (394079)------------------------------ % 20.45/3.84 % (394079)------------------------------ % 20.45/3.84 % (394092)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=1606725542:i=334:rtra=on_2977 on theBenchmark for (2977ds/334Mi) % 20.45/3.84 % (394083)Instruction limit reached! % 20.45/3.84 % (394083)------------------------------ % 20.45/3.84 % (394083)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.45/3.84 % (394083)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.45/3.84 % (394083)CaDiCaL version: 2.1.3 % 20.45/3.84 % (394083)Termination reason: Instruction limit % 20.45/3.84 % (394083)Termination phase: Saturation % 20.45/3.84 % (394083)Time elapsed: 0.207 s % 20.45/3.84 % (394083)Peak memory usage: 136 MB % 20.45/3.84 % (394083)Instructions burned: 276 (million) % 20.45/3.84 % (394084)Instruction limit reached! % 20.45/3.84 % (394084)------------------------------ % 20.45/3.84 % (394084)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.45/3.84 % (394084)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.45/3.84 % (394084)CaDiCaL version: 2.1.3 % 20.45/3.84 % (394084)Termination reason: Instruction limit % 20.45/3.84 % (394084)Termination phase: Saturation % 20.45/3.84 % (394084)Time elapsed: 0.238 s % 20.45/3.84 % (394084)Peak memory usage: 120 MB % 20.45/3.84 % (394084)Instructions burned: 376 (million) % 20.45/3.84 % (394091)lrs+10_1_to=kbo:sil=128000:fde=none:si=on:norm_ineq=on:urr=on:nwc=0.5:random_seed=81591952:i=513:kws=frequency:bd=all:rtra=on:gtg=exists_all:ss=axioms:sgt=4_2977 on theBenchmark for (2977ds/513Mi) % 20.45/3.84 % (394093)lrs+1010_1_to=kbo:sil=64000:sas=cadical:si=on:sos=on:bce=on:random_seed=940959425:i=359:rtra=on:gtg=exists_top:ss=axioms_2977 on theBenchmark for (2977ds/359Mi) % 20.45/3.84 % (394095)dis+1010_1_to=lpo:sil=128000:thi=all:fde=unused:si=on:sp=reverse_arity:tha=off:random_seed=781620307:i=341:gtgl=2:rtra=on:gtg=exists_sym:ev=force:fsd=on:fsdmm=1_2976 on theBenchmark for (2976ds/341Mi) % 20.45/3.84 % (394092)Instruction limit reached! % 20.45/3.84 % (394092)------------------------------ % 20.45/3.84 % (394092)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.45/3.84 % (394092)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.45/4.18 % (394092)CaDiCaL version: 2.1.3 % 24.45/4.18 % (394092)Termination reason: Instruction limit % 24.45/4.18 % (394092)Termination phase: Saturation % 24.45/4.18 % (394092)Time elapsed: 0.146 s % 24.45/4.18 % (394092)Peak memory usage: 136 MB % 24.45/4.18 % (394092)Instructions burned: 335 (million) % 24.45/4.18 % (394087)------------------------------ % 24.45/4.18 % (394087)------------------------------ % 24.45/4.18 % (394096)lrs-2_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_max:tha=off:random_seed=2137092710:st=1.5:i=261:sd=1:kws=precedence:rtra=on:ss=axioms_2976 on theBenchmark for (2976ds/261Mi) % 24.45/4.18 % (394098)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=2971424691:s2pl=no:i=235:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2975 on theBenchmark for (2975ds/235Mi) % 24.45/4.18 % (394096)Refutation not found, incomplete strategy % 24.45/4.18 % (394096)------------------------------ % 24.45/4.18 % (394096)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.45/4.18 % (394096)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.45/4.18 % (394096)CaDiCaL version: 2.1.3 % 24.45/4.18 % (394096)Termination reason: Refutation not found, incomplete strategy % 24.45/4.18 % (394096)Time elapsed: 0.036 s % 24.45/4.18 % (394096)Peak memory usage: 111 MB % 24.45/4.18 % (394096)Instructions burned: 23 (million) % 24.45/4.18 % (394098)Refutation not found, incomplete strategy % 24.45/4.18 % (394098)------------------------------ % 24.45/4.18 % (394098)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.45/4.18 % (394098)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.45/4.18 % (394098)CaDiCaL version: 2.1.3 % 24.45/4.18 % (394098)Termination reason: Refutation not found, incomplete strategy % 24.45/4.18 % (394098)Time elapsed: 0.041 s % 24.45/4.18 % (394098)Peak memory usage: 112 MB % 24.45/4.18 % (394098)Instructions burned: 34 (million) % 24.45/4.18 % (394101)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=3137440728:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2974 on theBenchmark for (2974ds/273Mi) % 24.45/4.18 % (394093)Instruction limit reached! % 24.45/4.18 % (394093)------------------------------ % 24.45/4.18 % (394093)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.45/4.18 % (394093)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.45/4.18 % (394093)CaDiCaL version: 2.1.3 % 24.45/4.18 % (394093)Termination reason: Instruction limit % 24.45/4.18 % (394093)Termination phase: Saturation % 24.45/4.18 % (394093)Time elapsed: 0.199 s % 24.45/4.18 % (394093)Peak memory usage: 93 MB % 24.45/4.18 % (394093)Instructions burned: 360 (million) % 24.45/4.18 % (394102)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=1588306314:i=146:doe=on:rtra=on_2974 on theBenchmark for (2974ds/146Mi) % 24.45/4.18 % (394091)Instruction limit reached! % 24.45/4.18 % (394091)------------------------------ % 24.45/4.18 % (394091)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.45/4.18 % (394091)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.45/4.18 % (394091)CaDiCaL version: 2.1.3 % 24.45/4.18 % (394091)Termination reason: Instruction limit % 24.45/4.18 % (394091)Termination phase: Saturation % 24.45/4.18 % (394091)Time elapsed: 0.316 s % 24.45/4.18 % (394091)Peak memory usage: 94 MB % 24.45/4.18 % (394091)Instructions burned: 514 (million) % 24.45/4.18 % (394101)Instruction limit reached! % 24.45/4.18 % (394101)------------------------------ % 24.45/4.18 % (394101)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.45/4.18 % (394101)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.45/4.18 % (394101)CaDiCaL version: 2.1.3 % 24.45/4.18 % (394101)Termination reason: Instruction limit % 24.45/4.18 % (394101)Termination phase: Saturation % 24.45/4.18 % (394101)Time elapsed: 0.092 s % 24.45/4.18 % (394101)Peak memory usage: 93 MB % 24.45/4.18 % (394101)Instructions burned: 275 (million) % 24.45/4.18 % (394095)Instruction limit reached! % 24.45/4.18 % (394095)------------------------------ % 24.45/4.18 % (394095)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.45/4.18 % (394095)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.45/4.18 % (394095)CaDiCaL version: 2.1.3 % 24.45/4.18 % (394095)Termination reason: Instruction limit % 24.45/4.18 % (394095)Termination phase: Saturation % 26.91/4.69 % (394095)Time elapsed: 0.223 s % 26.91/4.69 % (394095)Peak memory usage: 124 MB % 26.91/4.69 % (394095)Instructions burned: 342 (million) % 26.91/4.69 % (394102)Instruction limit reached! % 26.91/4.69 % (394102)------------------------------ % 26.91/4.69 % (394102)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.91/4.69 % (394102)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.91/4.69 % (394102)CaDiCaL version: 2.1.3 % 26.91/4.69 % (394102)Termination reason: Instruction limit % 26.91/4.69 % (394102)Termination phase: Saturation % 26.91/4.69 % (394102)Time elapsed: 0.081 s % 26.91/4.69 % (394102)Peak memory usage: 91 MB % 26.91/4.69 % (394102)Instructions burned: 146 (million) % 26.91/4.69 % (394106)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=1365579911:i=4428:doe=on:fsr=off:rtra=on_2973 on theBenchmark for (2973ds/4428Mi) % 26.91/4.69 % (394096)------------------------------ % 26.91/4.69 % (394096)------------------------------ % 26.91/4.69 % (394109)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=1202937985:i=1052:rtra=on_2972 on theBenchmark for (2972ds/1052Mi) % 26.91/4.69 % (394098)------------------------------ % 26.91/4.69 % (394098)------------------------------ % 26.91/4.69 % (394110)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=3541314912:i=655:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2972 on theBenchmark for (2972ds/655Mi) % 26.91/4.69 % (394108)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=2846583563:avsq=on:i=276:avsqr=1,2:rtra=on_2972 on theBenchmark for (2972ds/276Mi) % 26.91/4.69 % (394111)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=1596827195:st=5:i=1054:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2972 on theBenchmark for (2972ds/1054Mi) % 26.91/4.69 % (394111)Refutation not found, incomplete strategy % 26.91/4.69 % (394111)------------------------------ % 26.91/4.69 % (394111)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.91/4.69 % (394111)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.91/4.69 % (394111)CaDiCaL version: 2.1.3 % 26.91/4.69 % (394111)Termination reason: Refutation not found, incomplete strategy % 26.91/4.69 % (394111)Time elapsed: 0.011 s % 26.91/4.69 % (394111)Peak memory usage: 88 MB % 26.91/4.69 % (394111)Instructions burned: 18 (million) % 26.91/4.69 % (394113)lrs-1002_1_to=kbo:sas=z3:si=on:norm_ineq=on:sos=on:tha=some:random_seed=880826192:i=107:rtra=on_2971 on theBenchmark for (2971ds/107Mi) % 26.91/4.69 % (394115)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=389733827:s2a=on:i=450:doe=on:nm=32:rtra=on_2971 on theBenchmark for (2971ds/450Mi) % 26.91/4.69 % (394113)Instruction limit reached! % 26.91/4.69 % (394113)------------------------------ % 26.91/4.69 % (394113)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.91/4.69 % (394113)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.91/4.69 % (394113)CaDiCaL version: 2.1.3 % 26.91/4.69 % (394113)Termination reason: Instruction limit % 26.91/4.69 % (394113)Termination phase: Saturation % 26.91/4.69 % (394113)Time elapsed: 0.055 s % 26.91/4.69 % (394113)Peak memory usage: 90 MB % 26.91/4.69 % (394113)Instructions burned: 108 (million) % 26.91/4.69 % (394108)Instruction limit reached! % 26.91/4.69 % (394108)------------------------------ % 26.91/4.69 % (394108)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.91/4.69 % (394108)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.91/4.69 % (394108)CaDiCaL version: 2.1.3 % 26.91/4.69 % (394108)Termination reason: Instruction limit % 26.91/4.69 % (394108)Termination phase: Saturation % 26.91/4.69 % (394108)Time elapsed: 0.209 s % 26.91/4.69 % (394108)Peak memory usage: 136 MB % 26.91/4.69 % (394108)Instructions burned: 277 (million) % 26.91/4.69 % (394109)Instruction limit reached! % 26.91/4.69 % (394109)------------------------------ % 26.91/4.69 % (394109)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.91/4.69 % (394109)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.91/4.69 % (394109)CaDiCaL version: 2.1.3 % 26.91/4.69 % (394109)Termination reason: Instruction limit % 26.91/4.69 % (394109)Termination phase: Saturation % 26.91/4.69 % (394109)Time elapsed: 0.314 s % 26.91/4.69 % (394109)Peak memory usage: 98 MB % 26.91/4.69 % (394109)Instructions burned: 1056 (million) % 30.99/5.08 % (394111)------------------------------ % 30.99/5.08 % (394111)------------------------------ % 30.99/5.08 % (394121)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 % 30.99/5.08 % (394121)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=1146791107:i=1090:aac=none:nm=0:rtra=on:rawr=on_2969 on theBenchmark for (2969ds/1090Mi) % 30.99/5.08 % (394110)Instruction limit reached! % 30.99/5.08 % (394110)------------------------------ % 30.99/5.08 % (394110)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 30.99/5.08 % (394110)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.99/5.08 % (394110)CaDiCaL version: 2.1.3 % 30.99/5.08 % (394110)Termination reason: Instruction limit % 30.99/5.08 % (394110)Termination phase: Saturation % 30.99/5.08 % (394110)Time elapsed: 0.313 s % 30.99/5.08 % (394110)Peak memory usage: 93 MB % 30.99/5.08 % (394110)Instructions burned: 655 (million) % 30.99/5.08 % (394122)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=1405640174:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2968 on theBenchmark for (2968ds/130Mi) % 30.99/5.08 % (394123)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=916112036:i=312:kws=inv_frequency:nm=20:rtra=on_2968 on theBenchmark for (2968ds/312Mi) % 30.99/5.08 % (394124)ott+10_1_to=kbo:sil=64000:si=on:sp=reverse_frequency:sos=on:random_seed=3709050114:i=491:doe=on:rtra=on:gtg=position_2968 on theBenchmark for (2968ds/491Mi) % 30.99/5.08 % (394115)Instruction limit reached! % 30.99/5.08 % (394115)------------------------------ % 30.99/5.08 % (394115)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 30.99/5.08 % (394115)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.99/5.08 % (394115)CaDiCaL version: 2.1.3 % 30.99/5.08 % (394115)Termination reason: Instruction limit % 30.99/5.08 % (394115)Termination phase: Saturation % 30.99/5.08 % (394115)Time elapsed: 0.325 s % 30.99/5.08 % (394115)Peak memory usage: 137 MB % 30.99/5.08 % (394115)Instructions burned: 451 (million) % 30.99/5.08 % (394122)Instruction limit reached! % 30.99/5.08 % (394122)------------------------------ % 30.99/5.08 % (394122)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 30.99/5.08 % (394122)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.99/5.08 % (394122)CaDiCaL version: 2.1.3 % 30.99/5.08 % (394122)Termination reason: Instruction limit % 30.99/5.08 % (394122)Termination phase: Saturation % 30.99/5.08 % (394122)Time elapsed: 0.087 s % 30.99/5.08 % (394122)Peak memory usage: 114 MB % 30.99/5.08 % (394122)Instructions burned: 130 (million) % 30.99/5.08 % (394126)ott+1011_4:1_to=lpo:sil=64000:si=on:spb=intro:random_seed=3727911376:s2a=on:i=835:s2at=2:rtra=on_2967 on theBenchmark for (2967ds/835Mi) % 30.99/5.08 % (394123)Instruction limit reached! % 30.99/5.08 % (394123)------------------------------ % 30.99/5.08 % (394123)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 30.99/5.08 % (394123)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.99/5.08 % (394123)CaDiCaL version: 2.1.3 % 30.99/5.08 % (394123)Termination reason: Instruction limit % 30.99/5.08 % (394123)Termination phase: Saturation % 30.99/5.08 % (394123)Time elapsed: 0.113 s % 30.99/5.08 % (394123)Peak memory usage: 119 MB % 30.99/5.08 % (394123)Instructions burned: 313 (million) % 30.99/5.08 % (394124)Refutation not found, incomplete strategy % 30.99/5.08 % (394124)------------------------------ % 30.99/5.08 % (394124)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 30.99/5.08 % (394124)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.99/5.08 % (394124)CaDiCaL version: 2.1.3 % 30.99/5.08 % (394124)Termination reason: Refutation not found, incomplete strategy % 30.99/5.08 % (394124)Time elapsed: 0.072 s % 30.99/5.08 % (394124)Peak memory usage: 91 MB % 30.99/5.08 % (394124)Instructions burned: 136 (million) % 30.99/5.08 % (394130)ott+1011_2_to=lpo:sil=128000:si=on:sos=on:random_seed=1901468170:i=307:bd=preordered:av=off:rtra=on:ev=cautious_2966 on theBenchmark for (2966ds/307Mi) % 30.99/5.08 % (394132)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=3729099473:i=776:doe=on:rtra=on_2966 on theBenchmark for (2966ds/776Mi) % 35.60/5.88 % (394133)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=471119246:s2a=on:i=646:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2966 on theBenchmark for (2966ds/646Mi) % 35.60/5.88 % (394130)Refutation not found, incomplete strategy % 35.60/5.88 % (394130)------------------------------ % 35.60/5.88 % (394130)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 35.60/5.88 % (394130)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.60/5.88 % (394130)CaDiCaL version: 2.1.3 % 35.60/5.88 % (394130)Termination reason: Refutation not found, incomplete strategy % 35.60/5.88 % (394130)Time elapsed: 0.099 s % 35.60/5.88 % (394130)Peak memory usage: 92 MB % 35.60/5.88 % (394130)Instructions burned: 173 (million) % 35.60/5.88 % (394124)------------------------------ % 35.60/5.88 % (394124)------------------------------ % 35.60/5.88 % (394133)Instruction limit reached! % 35.60/5.88 % (394133)------------------------------ % 35.60/5.88 % (394133)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 35.60/5.88 % (394133)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.60/5.88 % (394133)CaDiCaL version: 2.1.3 % 35.60/5.88 % (394133)Termination reason: Instruction limit % 35.60/5.88 % (394133)Termination phase: Saturation % 35.60/5.88 % (394133)Time elapsed: 0.256 s % 35.60/5.88 % (394133)Peak memory usage: 141 MB % 35.60/5.88 % (394133)Instructions burned: 647 (million) % 35.60/5.88 % (394137)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=1830440276:thitd=on:cond=fast:i=784:nm=30:rtra=on:gtg=all:tac=axiom_2963 on theBenchmark for (2963ds/784Mi) % 35.60/5.88 % (394130)------------------------------ % 35.60/5.88 % (394130)------------------------------ % 35.60/5.88 % (394126)Instruction limit reached! % 35.60/5.88 % (394126)------------------------------ % 35.60/5.88 % (394126)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 35.60/5.88 % (394126)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.60/5.88 % (394126)CaDiCaL version: 2.1.3 % 35.60/5.88 % (394126)Termination reason: Instruction limit % 35.60/5.88 % (394126)Termination phase: Saturation % 35.60/5.88 % (394126)Time elapsed: 0.487 s % 35.60/5.88 % (394126)Peak memory usage: 97 MB % 35.60/5.88 % (394126)Instructions burned: 835 (million) % 35.60/5.88 % (394121)Instruction limit reached! % 35.60/5.88 % (394121)------------------------------ % 35.60/5.88 % (394121)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 35.60/5.88 % (394121)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.60/5.88 % (394121)CaDiCaL version: 2.1.3 % 35.60/5.88 % (394121)Termination reason: Instruction limit % 35.60/5.88 % (394121)Termination phase: Saturation % 35.60/5.88 % (394121)Time elapsed: 0.709 s % 35.60/5.88 % (394121)Peak memory usage: 128 MB % 35.60/5.88 % (394121)Instructions burned: 1091 (million) % 35.60/5.88 % (394138)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=3030238654:thitd=on:s2a=on:i=1131:add=on:canc=force:bd=all:rtra=on:tac=axiom:ev=off_2962 on theBenchmark for (2962ds/1131Mi) % 35.60/5.88 % (394140)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=1170273117:s2pl=no:i=246:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2961 on theBenchmark for (2961ds/246Mi) % 35.60/5.88 % (394132)Instruction limit reached! % 35.60/5.88 % (394132)------------------------------ % 35.60/5.88 % (394132)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 35.60/5.88 % (394132)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.60/5.88 % (394132)CaDiCaL version: 2.1.3 % 35.60/5.88 % (394132)Termination reason: Instruction limit % 35.60/5.88 % (394132)Termination phase: Saturation % 35.60/5.88 % (394132)Time elapsed: 0.486 s % 35.60/5.88 % (394132)Peak memory usage: 123 MB % 35.60/5.88 % (394132)Instructions burned: 776 (million) % 35.60/5.88 % (394141)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=135671638:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2961 on theBenchmark for (2961ds/775Mi) % 35.60/5.88 % (394141)Refutation not found, incomplete strategy % 35.60/5.88 % (394141)------------------------------ % 35.60/5.88 % (394141)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 35.60/5.88 % (394141)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 46.23/7.28 % (394141)CaDiCaL version: 2.1.3 % 46.23/7.28 % (394141)Termination reason: Refutation not found, incomplete strategy % 46.23/7.28 % (394141)Time elapsed: 0.017 s % 46.23/7.28 % (394141)Peak memory usage: 88 MB % 46.23/7.28 % (394141)Instructions burned: 32 (million) % 46.23/7.28 % (394140)Refutation not found, incomplete strategy % 46.23/7.28 % (394140)------------------------------ % 46.23/7.28 % (394140)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 46.23/7.28 % (394140)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 46.23/7.28 % (394140)CaDiCaL version: 2.1.3 % 46.23/7.28 % (394140)Termination reason: Refutation not found, incomplete strategy % 46.23/7.28 % (394140)Time elapsed: 0.041 s % 46.23/7.28 % (394140)Peak memory usage: 112 MB % 46.23/7.28 % (394140)Instructions burned: 34 (million) % 46.23/7.28 % (394143)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=3970739264:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2960 on theBenchmark for (2960ds/273Mi) % 46.23/7.28 % (394146)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=1263010178:i=102:nm=16:rtra=on_2960 on theBenchmark for (2960ds/102Mi) % 46.23/7.28 % (394146)Instruction limit reached! % 46.23/7.28 % (394146)------------------------------ % 46.23/7.28 % (394146)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 46.23/7.28 % (394146)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 46.23/7.28 % (394146)CaDiCaL version: 2.1.3 % 46.23/7.28 % (394146)Termination reason: Instruction limit % 46.23/7.28 % (394146)Termination phase: Saturation % 46.23/7.28 % (394146)Time elapsed: 0.049 s % 46.23/7.28 % (394146)Peak memory usage: 90 MB % 46.23/7.28 % (394146)Instructions burned: 102 (million) % 46.23/7.28 % (394143)Instruction limit reached! % 46.23/7.28 % (394143)------------------------------ % 46.23/7.28 % (394143)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 46.23/7.28 % (394143)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 46.23/7.28 % (394143)CaDiCaL version: 2.1.3 % 46.23/7.28 % (394143)Termination reason: Instruction limit % 46.23/7.28 % (394143)Termination phase: Saturation % 46.23/7.28 % (394143)Time elapsed: 0.167 s % 46.23/7.28 % (394143)Peak memory usage: 93 MB % 46.23/7.28 % (394143)Instructions burned: 274 (million) % 46.23/7.28 % (394137)Instruction limit reached! % 46.23/7.28 % (394137)------------------------------ % 46.23/7.28 % (394137)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 46.23/7.28 % (394137)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 46.23/7.28 % (394137)CaDiCaL version: 2.1.3 % 46.23/7.28 % (394137)Termination reason: Instruction limit % 46.23/7.28 % (394137)Termination phase: Saturation % 46.23/7.28 % (394137)Time elapsed: 0.430 s % 46.23/7.28 % (394137)Peak memory usage: 122 MB % 46.23/7.28 % (394137)Instructions burned: 785 (million) % 46.23/7.28 % (394140)------------------------------ % 46.23/7.28 % (394140)------------------------------ % 46.23/7.28 % (394141)------------------------------ % 46.23/7.28 % (394141)------------------------------ % 46.23/7.28 % (394138)Instruction limit reached! % 46.23/7.28 % (394138)------------------------------ % 46.23/7.28 % (394138)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 46.23/7.28 % (394138)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 46.23/7.28 % (394138)CaDiCaL version: 2.1.3 % 46.23/7.28 % (394138)Termination reason: Instruction limit % 46.23/7.28 % (394138)Termination phase: Saturation % 46.23/7.28 % (394138)Time elapsed: 0.397 s % 46.23/7.28 % (394138)Peak memory usage: 133 MB % 46.23/7.28 % (394138)Instructions burned: 1133 (million) % 46.23/7.28 % (394149)lrs+10_1_to=lpo:sil=128000:si=on:bsr=unit_only:tha=off:random_seed=4247659951:avsq=on:s2a=on:i=1094:s2at=5:avsqr=4463,131072:rtra=on_2957 on theBenchmark for (2957ds/1094Mi) % 46.23/7.28 % (394151)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=1482687967:i=868:doe=on:nm=0:rtra=on:gtg=exists_sym_2957 on theBenchmark for (2957ds/868Mi) % 46.23/7.28 % (394150)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=3063278365:i=6400:doe=on:fsr=off:rtra=on_2957 on theBenchmark for (2957ds/6400Mi) % 46.23/7.28 % (394152)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=595332541:i=1846:canc=cautious:fsr=off:rtra=on_2957 on theBenchmark for (2957ds/1846Mi) % 57.53/8.87 % (394153)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=2832111920:s2a=on:i=36816:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2957 on theBenchmark for (2957ds/36816Mi) % 57.53/8.87 % (394154)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=1326100533:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2956 on theBenchmark for (2956ds/273Mi) % 57.53/8.87 % (394152)Refutation not found, incomplete strategy % 57.53/8.87 % (394152)------------------------------ % 57.53/8.87 % (394152)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 57.53/8.87 % (394152)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 57.53/8.87 % (394152)CaDiCaL version: 2.1.3 % 57.53/8.87 % (394152)Termination reason: Refutation not found, incomplete strategy % 57.53/8.87 % (394152)Time elapsed: 0.069 s % 57.53/8.87 % (394152)Peak memory usage: 91 MB % 57.53/8.87 % (394152)Instructions burned: 130 (million) % 57.53/8.87 % (394154)Instruction limit reached! % 57.53/8.87 % (394154)------------------------------ % 57.53/8.87 % (394154)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 57.53/8.87 % (394154)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 57.53/8.87 % (394154)CaDiCaL version: 2.1.3 % 57.53/8.87 % (394154)Termination reason: Instruction limit % 57.53/8.87 % (394154)Termination phase: Saturation % 57.53/8.87 % (394154)Time elapsed: 0.089 s % 57.53/8.87 % (394154)Peak memory usage: 93 MB % 57.53/8.87 % (394154)Instructions burned: 274 (million) % 57.53/8.87 % (394161)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=1735002072:i=863:doe=on:nm=0:rtra=on:gtg=exists_sym_2954 on theBenchmark for (2954ds/863Mi) % 57.53/8.87 % (394152)------------------------------ % 57.53/8.87 % (394152)------------------------------ % 57.53/8.87 % (394163)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=2729412553:i=5811:kws=precedence:nm=0:rtra=on_2952 on theBenchmark for (2952ds/5811Mi) % 57.53/8.87 % (394151)Instruction limit reached! % 57.53/8.87 % (394151)------------------------------ % 57.53/8.87 % (394151)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 57.53/8.87 % (394151)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 57.53/8.87 % (394151)CaDiCaL version: 2.1.3 % 57.53/8.87 % (394151)Termination reason: Instruction limit % 57.53/8.87 % (394151)Termination phase: Saturation % 57.53/8.87 % (394151)Time elapsed: 0.505 s % 57.53/8.87 % (394151)Peak memory usage: 122 MB % 57.53/8.87 % (394151)Instructions burned: 870 (million) % 57.53/8.87 % (394161)Instruction limit reached! % 57.53/8.87 % (394161)------------------------------ % 57.53/8.87 % (394161)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 57.53/8.87 % (394161)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 57.53/8.87 % (394161)CaDiCaL version: 2.1.3 % 57.53/8.87 % (394161)Termination reason: Instruction limit % 57.53/8.87 % (394161)Termination phase: Saturation % 57.53/8.87 % (394161)Time elapsed: 0.268 s % 57.53/8.87 % (394161)Peak memory usage: 123 MB % 57.53/8.87 % (394161)Instructions burned: 865 (million) % 57.53/8.87 % (394149)Instruction limit reached! % 57.53/8.87 % (394149)------------------------------ % 57.53/8.87 % (394149)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 57.53/8.87 % (394149)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 57.53/8.87 % (394149)CaDiCaL version: 2.1.3 % 57.53/8.87 % (394149)Termination reason: Instruction limit % 57.53/8.87 % (394149)Termination phase: Saturation % 57.53/8.87 % (394149)Time elapsed: 0.657 s % 57.53/8.87 % (394149)Peak memory usage: 97 MB % 57.53/8.87 % (394149)Instructions burned: 1096 (million) % 57.53/8.87 % (394166)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=3335461070:i=801:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2950 on theBenchmark for (2950ds/801Mi) % 57.53/8.87 % (394165)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=4213312712:i=2216:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2951 on theBenchmark for (2951ds/2216Mi) % 57.53/8.87 % (394167)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=1710898018:st=5:i=1026:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2949 on theBenchmark for (2949ds/1026Mi) % 57.53/8.87 % (394167)Refutation not found, incomplete strategy % 61.95/9.69 % (394167)------------------------------ % 61.95/9.69 % (394167)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 61.95/9.69 % (394167)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.95/9.69 % (394167)CaDiCaL version: 2.1.3 % 61.95/9.69 % (394167)Termination reason: Refutation not found, incomplete strategy % 61.95/9.69 % (394167)Time elapsed: 0.010 s % 61.95/9.69 % (394167)Peak memory usage: 88 MB % 61.95/9.69 % (394167)Instructions burned: 18 (million) % 61.95/9.69 % (394166)Instruction limit reached! % 61.95/9.69 % (394166)------------------------------ % 61.95/9.69 % (394166)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 61.95/9.69 % (394166)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.95/9.69 % (394166)CaDiCaL version: 2.1.3 % 61.95/9.69 % (394166)Termination reason: Instruction limit % 61.95/9.69 % (394166)Termination phase: Saturation % 61.95/9.69 % (394166)Time elapsed: 0.195 s % 61.95/9.69 % (394166)Peak memory usage: 93 MB % 61.95/9.69 % (394166)Instructions burned: 806 (million) % 61.95/9.69 % (394106)Instruction limit reached! % 61.95/9.69 % (394106)------------------------------ % 61.95/9.69 % (394106)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 61.95/9.69 % (394106)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.95/9.69 % (394106)CaDiCaL version: 2.1.3 % 61.95/9.69 % (394106)Termination reason: Instruction limit % 61.95/9.69 % (394106)Termination phase: Saturation % 61.95/9.69 % (394106)Time elapsed: 2.524 s % 61.95/9.69 % (394106)Peak memory usage: 115 MB % 61.95/9.69 % (394106)Instructions burned: 4429 (million) % 61.95/9.69 % (394171)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=3092028616:i=3509:rtra=on_2947 on theBenchmark for (2947ds/3509Mi) % 61.95/9.69 % (394167)------------------------------ % 61.95/9.69 % (394167)------------------------------ % 61.95/9.69 % (394172)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=3884933823:st=2:i=2127:sd=12:ep=R:rtra=on:ss=axioms_2946 on theBenchmark for (2946ds/2127Mi) % 61.95/9.69 % (394172)Refutation not found, incomplete strategy % 61.95/9.69 % (394172)------------------------------ % 61.95/9.69 % (394172)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 61.95/9.69 % (394172)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.95/9.69 % (394172)CaDiCaL version: 2.1.3 % 61.95/9.69 % (394172)Termination reason: Refutation not found, incomplete strategy % 61.95/9.69 % (394172)Time elapsed: 0.015 s % 61.95/9.69 % (394172)Peak memory usage: 88 MB % 61.95/9.69 % (394172)Instructions burned: 29 (million) % 61.95/9.69 % (394174)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=828011341:i=1959:rtra=on:fsd=on:proc=on_2945 on theBenchmark for (2945ds/1959Mi) % 61.95/9.69 % (394172)------------------------------ % 61.95/9.69 % (394172)------------------------------ % 61.95/9.69 % (394177)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=960052676:s2a=on:i=3553:nm=0:rtra=on_2942 on theBenchmark for (2942ds/3553Mi) % 61.95/9.69 % (394165)Instruction limit reached! % 61.95/9.69 % (394165)------------------------------ % 61.95/9.69 % (394165)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 61.95/9.69 % (394165)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.95/9.69 % (394165)CaDiCaL version: 2.1.3 % 61.95/9.69 % (394165)Termination reason: Instruction limit % 61.95/9.69 % (394165)Termination phase: Saturation % 61.95/9.69 % (394165)Time elapsed: 1.298 s % 61.95/9.69 % (394165)Peak memory usage: 135 MB % 61.95/9.69 % (394165)Instructions burned: 2217 (million) % 61.95/9.69 % (394171)Instruction limit reached! % 61.95/9.69 % (394171)------------------------------ % 61.95/9.69 % (394171)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 61.95/9.69 % (394171)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.95/9.69 % (394171)CaDiCaL version: 2.1.3 % 61.95/9.69 % (394171)Termination reason: Instruction limit % 61.95/9.69 % (394171)Termination phase: Saturation % 61.95/9.69 % (394171)Time elapsed: 1.104 s % 61.95/9.69 % (394171)Peak memory usage: 118 MB % 61.95/9.69 % (394171)Instructions burned: 3510 (million) % 61.95/9.69 % (394179)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=535944937:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2936 on theBenchmark for (2936ds/3201Mi) % 61.95/9.69 % (394180)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=2456993869:thitd=on:cond=on:i=4093:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2935 on theBenchmark for (2935ds/4093Mi) % 85.69/12.82 % (394174)Instruction limit reached! % 85.69/12.82 % (394174)------------------------------ % 85.69/12.82 % (394174)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 85.69/12.82 % (394174)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 85.69/12.82 % (394174)CaDiCaL version: 2.1.3 % 85.69/12.82 % (394174)Termination reason: Instruction limit % 85.69/12.82 % (394174)Termination phase: Saturation % 85.69/12.82 % (394174)Time elapsed: 1.228 s % 85.69/12.82 % (394174)Peak memory usage: 138 MB % 85.69/12.82 % (394174)Instructions burned: 1960 (million) % 85.69/12.82 % (394183)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=3005532923:cond=fast:i=21173:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2931 on theBenchmark for (2931ds/21173Mi) % 85.69/12.82 % (394183)Refutation not found, incomplete strategy % 85.69/12.82 % (394183)------------------------------ % 85.69/12.82 % (394183)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 85.69/12.82 % (394183)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 85.69/12.82 % (394183)CaDiCaL version: 2.1.3 % 85.69/12.82 % (394183)Termination reason: Refutation not found, incomplete strategy % 85.69/12.82 % (394183)Time elapsed: 0.035 s % 85.69/12.82 % (394183)Peak memory usage: 113 MB % 85.69/12.82 % (394183)Instructions burned: 21 (million) % 85.69/12.82 % (394183)------------------------------ % 85.69/12.82 % (394183)------------------------------ % 85.69/12.82 % (394185)lrs+11_1_to=lpo:thi=all:sas=z3:si=on:fd=off:sac=on:slsq=on:random_seed=3300931121:avsq=on:i=10544:avsqr=17,4:canc=force:rtra=on:gtg=exists_top:er=filter_2927 on theBenchmark for (2927ds/10544Mi) % 85.69/12.82 % (394180)Instruction limit reached! % 85.69/12.82 % (394180)------------------------------ % 85.69/12.82 % (394180)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 85.69/12.82 % (394180)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 85.69/12.82 % (394180)CaDiCaL version: 2.1.3 % 85.69/12.82 % (394180)Termination reason: Instruction limit % 85.69/12.82 % (394180)Termination phase: Saturation % 85.69/12.82 % (394180)Time elapsed: 1.333 s % 85.69/12.82 % (394180)Peak memory usage: 166 MB % 85.69/12.82 % (394180)Instructions burned: 4093 (million) % 85.69/12.82 % (394150)Instruction limit reached! % 85.69/12.82 % (394150)------------------------------ % 85.69/12.82 % (394150)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 85.69/12.82 % (394150)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 85.69/12.82 % (394150)CaDiCaL version: 2.1.3 % 85.69/12.82 % (394150)Termination reason: Instruction limit % 85.69/12.82 % (394150)Termination phase: Saturation % 85.69/12.82 % (394150)Time elapsed: 3.627 s % 85.69/12.82 % (394150)Peak memory usage: 127 MB % 85.69/12.82 % (394150)Instructions burned: 6400 (million) % 85.69/12.82 % (394187)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=3813866224:avsq=on:i=1262:avsqr=1,16:rtra=on:rawr=on_2920 on theBenchmark for (2920ds/1262Mi) % 85.69/12.82 % (394177)Instruction limit reached! % 85.69/12.82 % (394177)------------------------------ % 85.69/12.82 % (394177)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 85.69/12.82 % (394177)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 85.69/12.82 % (394177)CaDiCaL version: 2.1.3 % 85.69/12.82 % (394177)Termination reason: Instruction limit % 85.69/12.82 % (394177)Termination phase: Saturation % 85.69/12.82 % (394177)Time elapsed: 2.177 s % 85.69/12.82 % (394177)Peak memory usage: 117 MB % 85.69/12.82 % (394177)Instructions burned: 3553 (million) % 85.69/12.82 % (394163)Instruction limit reached! % 85.69/12.82 % (394163)------------------------------ % 85.69/12.82 % (394163)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 85.69/12.82 % (394163)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 85.69/12.82 % (394163)CaDiCaL version: 2.1.3 % 85.69/12.82 % (394163)Termination reason: Instruction limit % 85.69/12.82 % (394163)Termination phase: Saturation % 85.69/12.82 % (394163)Time elapsed: 3.260 s % 85.69/12.82 % (394163)Peak memory usage: 139 MB % 85.69/12.82 % (394163)Instructions burned: 5811 (million) % 85.69/12.82 % (394188)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=159417353:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2919 on theBenchmark for (2919ds/775Mi) % 100.45/14.96 % (394188)Refutation not found, incomplete strategy % 100.45/14.96 % (394188)------------------------------ % 100.45/14.96 % (394188)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 100.45/14.96 % (394188)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 100.45/14.96 % (394188)CaDiCaL version: 2.1.3 % 100.45/14.96 % (394188)Termination reason: Refutation not found, incomplete strategy % 100.45/14.96 % (394188)Time elapsed: 0.017 s % 100.45/14.96 % (394188)Peak memory usage: 88 MB % 100.45/14.96 % (394188)Instructions burned: 32 (million) % 100.45/14.96 % (394190)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=1329945223:i=270:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2918 on theBenchmark for (2918ds/270Mi) % 100.45/14.96 % (394191)ott+10_128_isp=bottom:to=lpo:sil=128000:si=on:urr=on:uwa=alasca_main:sac=on:slsq=on:random_seed=1072076674:i=17165:aac=none:doe=on:rtra=on:gtg=exists_all_2918 on theBenchmark for (2918ds/17165Mi) % 100.45/14.96 % (394179)Instruction limit reached! % 100.45/14.96 % (394179)------------------------------ % 100.45/14.96 % (394179)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 100.45/14.96 % (394179)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 100.45/14.96 % (394179)CaDiCaL version: 2.1.3 % 100.45/14.96 % (394179)Termination reason: Instruction limit % 100.45/14.96 % (394179)Termination phase: Saturation % 100.45/14.96 % (394179)Time elapsed: 1.837 s % 100.45/14.96 % (394179)Peak memory usage: 105 MB % 100.45/14.96 % (394179)Instructions burned: 3202 (million) % 100.45/14.96 % (394190)Instruction limit reached! % 100.45/14.96 % (394190)------------------------------ % 100.45/14.96 % (394190)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 100.45/14.96 % (394190)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 100.45/14.96 % (394190)CaDiCaL version: 2.1.3 % 100.45/14.96 % (394190)Termination reason: Instruction limit % 100.45/14.96 % (394190)Termination phase: Saturation % 100.45/14.96 % (394190)Time elapsed: 0.166 s % 100.45/14.96 % (394190)Peak memory usage: 93 MB % 100.45/14.96 % (394190)Instructions burned: 271 (million) % 100.45/14.97 % (394188)------------------------------ % 100.45/14.97 % (394188)------------------------------ % 100.45/14.97 % (394187)Instruction limit reached! % 100.45/14.97 % (394187)------------------------------ % 100.45/14.97 % (394187)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 100.45/14.97 % (394187)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 100.45/14.97 % (394187)CaDiCaL version: 2.1.3 % 100.45/14.97 % (394187)Termination reason: Instruction limit % 100.45/14.97 % (394187)Termination phase: Saturation % 100.45/14.97 % (394187)Time elapsed: 0.420 s % 100.45/14.97 % (394187)Peak memory usage: 128 MB % 100.45/14.97 % (394187)Instructions burned: 1262 (million) % 100.45/14.97 % (394195)lrs+2_10_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_main:tha=some:random_seed=3005239651:s2a=on:i=13094:s2at=-1:rtra=on_2916 on theBenchmark for (2916ds/13094Mi) % 100.45/14.97 % (394196)lrs+10_1_to=lpo:sil=128000:si=on:sp=occurrence:random_seed=1793964662:st=2:i=12633:rtra=on:ss=axioms_2915 on theBenchmark for (2915ds/12633Mi) % 100.45/14.97 % (394196)Refutation not found, incomplete strategy % 100.45/14.97 % (394196)------------------------------ % 100.45/14.97 % (394196)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 100.45/14.97 % (394196)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 100.45/14.97 % (394196)CaDiCaL version: 2.1.3 % 100.45/14.97 % (394196)Termination reason: Refutation not found, incomplete strategy % 100.45/14.97 % (394196)Time elapsed: 0.015 s % 100.45/14.97 % (394196)Peak memory usage: 88 MB % 100.45/14.97 % (394196)Instructions burned: 28 (million) % 100.45/14.97 % (394197)dis+1011_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_frequency:lsd=20:nwc=3:random_seed=3971998210:i=1783:rtra=on:gtg=position_2915 on theBenchmark for (2915ds/1783Mi) % 100.45/14.97 % (394198)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=3166480234:i=5451:aac=none:doe=on:nm=0:rtra=on:amm=off:gtg=position_2914 on theBenchmark for (2914ds/5451Mi) % 100.45/14.97 % (394196)------------------------------ % 100.45/14.97 % (394196)------------------------------ % 100.45/14.97 % (394203)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=226164866:i=4975:doe=on:nm=0:rtra=on:gtg=exists_sym_2911 on theBenchmark for (2911ds/4975Mi) % 159.75/23.16 % (394197)Instruction limit reached! % 159.75/23.16 % (394197)------------------------------ % 159.75/23.16 % (394197)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 159.75/23.16 % (394197)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 159.75/23.16 % (394197)CaDiCaL version: 2.1.3 % 159.75/23.16 % (394197)Termination reason: Instruction limit % 159.75/23.16 % (394197)Termination phase: Saturation % 159.75/23.16 % (394197)Time elapsed: 1.043 s % 159.75/23.16 % (394197)Peak memory usage: 129 MB % 159.75/23.16 % (394197)Instructions burned: 1783 (million) % 159.75/23.16 % (394205)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=1719349203:i=2076:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2903 on theBenchmark for (2903ds/2076Mi) % 159.75/23.16 % (394198)Instruction limit reached! % 159.75/23.16 % (394198)------------------------------ % 159.75/23.16 % (394198)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 159.75/23.16 % (394198)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 159.75/23.16 % (394198)CaDiCaL version: 2.1.3 % 159.75/23.16 % (394198)Termination reason: Instruction limit % 159.75/23.16 % (394198)Termination phase: Saturation % 159.75/23.16 % (394198)Time elapsed: 1.734 s % 159.75/23.16 % (394198)Peak memory usage: 144 MB % 159.75/23.16 % (394198)Instructions burned: 5452 (million) % 159.75/23.16 % (394207)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=4271903475:i=5145:rtra=on_2896 on theBenchmark for (2896ds/5145Mi) % 159.75/23.16 % (394205)Instruction limit reached! % 159.75/23.16 % (394205)------------------------------ % 159.75/23.16 % (394205)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 159.75/23.16 % (394205)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 159.75/23.16 % (394205)CaDiCaL version: 2.1.3 % 159.75/23.16 % (394205)Termination reason: Instruction limit % 159.75/23.16 % (394205)Termination phase: Saturation % 159.75/23.16 % (394205)Time elapsed: 1.214 s % 159.75/23.16 % (394205)Peak memory usage: 133 MB % 159.75/23.16 % (394205)Instructions burned: 2077 (million) % 159.75/23.16 % (394209)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=4251342360:i=3509:rtra=on_2889 on theBenchmark for (2889ds/3509Mi) % 159.75/23.16 % (394203)Instruction limit reached! % 159.75/23.16 % (394203)------------------------------ % 159.75/23.16 % (394203)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 159.75/23.16 % (394203)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 159.75/23.16 % (394203)CaDiCaL version: 2.1.3 % 159.75/23.16 % (394203)Termination reason: Instruction limit % 159.75/23.16 % (394203)Termination phase: Saturation % 159.75/23.16 % (394203)Time elapsed: 2.710 s % 159.75/23.16 % (394203)Peak memory usage: 145 MB % 159.75/23.16 % (394203)Instructions burned: 4976 (million) % 159.75/23.16 % (394211)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=907841136:st=2:i=13800:sd=12:ep=R:rtra=on:ss=axioms_2882 on theBenchmark for (2882ds/13800Mi) % 159.75/23.16 % (394211)Refutation not found, incomplete strategy % 159.75/23.16 % (394211)------------------------------ % 159.75/23.16 % (394211)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 159.75/23.16 % (394211)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 159.75/23.16 % (394211)CaDiCaL version: 2.1.3 % 159.75/23.16 % (394211)Termination reason: Refutation not found, incomplete strategy % 159.75/23.16 % (394211)Time elapsed: 0.014 s % 159.75/23.16 % (394211)Peak memory usage: 88 MB % 159.75/23.16 % (394211)Instructions burned: 29 (million) % 159.75/23.16 % (394207)Instruction limit reached! % 159.75/23.16 % (394207)------------------------------ % 159.75/23.16 % (394207)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 159.75/23.16 % (394207)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 159.75/23.16 % (394207)CaDiCaL version: 2.1.3 % 159.75/23.16 % (394207)Termination reason: Instruction limit % 159.75/23.16 % (394207)Termination phase: Saturation % 159.75/23.16 % (394207)Time elapsed: 1.505 s % 159.75/23.16 % (394207)Peak memory usage: 125 MB % 159.75/23.16 % (394207)Instructions burned: 5149 (million) % 159.75/23.16 % (394213)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=4226382836:i=1412:rtra=on:fsd=on:proc=on_2879 on theBenchmark for (2879ds/1412Mi) % 159.75/23.16 % (394211)------------------------------ % 300.55/42.94 % (394211)------------------------------ % 300.55/42.94 % (394215)WARNING Broken Constraint: if demodulation_redundancy_check(ordering) has been set then forward_demodulation(off) is not equal to off or backward_demodulation(off) is not equal to off or partial_redundancy_check(off) is not equal to off % 300.55/42.94 % (394215)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=3992834640:i=11747:aac=none:nm=0:rtra=on:rawr=on_2878 on theBenchmark for (2878ds/11747Mi) % 300.55/42.94 % (394213)Instruction limit reached! % 300.55/42.94 % (394213)------------------------------ % 300.55/42.94 % (394213)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.55/42.94 % (394213)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.55/42.94 % (394213)CaDiCaL version: 2.1.3 % 300.55/42.94 % (394213)Termination reason: Instruction limit % 300.55/42.94 % (394213)Termination phase: Saturation % 300.55/42.94 % (394213)Time elapsed: 0.488 s % 300.55/42.94 % (394213)Peak memory usage: 133 MB % 300.55/42.94 % (394213)Instructions burned: 1413 (million) % 300.55/42.94 % (394217)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=2359051018:s2a=on:i=3553:nm=0:rtra=on_2873 on theBenchmark for (2873ds/3553Mi) % 300.55/42.94 % (394209)Instruction limit reached! % 300.55/42.94 % (394209)------------------------------ % 300.55/42.94 % (394209)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.55/42.94 % (394209)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.55/42.94 % (394209)CaDiCaL version: 2.1.3 % 300.55/42.94 % (394209)Termination reason: Instruction limit % 300.55/42.94 % (394209)Termination phase: Saturation % 300.55/42.94 % (394209)Time elapsed: 2.042 s % 300.55/42.94 % (394209)Peak memory usage: 117 MB % 300.55/42.94 % (394209)Instructions burned: 3509 (million) % 300.55/42.94 % (394221)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=3330923632:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2867 on theBenchmark for (2867ds/3201Mi) % 300.55/42.94 % (394185)Instruction limit reached! % 300.55/42.94 % (394185)------------------------------ % 300.55/42.94 % (394185)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.55/42.94 % (394185)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.55/42.94 % (394185)CaDiCaL version: 2.1.3 % 300.55/42.94 % (394185)Termination reason: Instruction limit % 300.55/42.94 % (394185)Termination phase: Saturation % 300.55/42.94 % (394185)Time elapsed: 6.109 s % 300.55/42.94 % (394185)Peak memory usage: 243 MB % 300.55/42.94 % (394185)Instructions burned: 10546 (million) % 300.55/42.94 % (394308)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=3931143635:thitd=on:cond=on:i=4081:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2864 on theBenchmark for (2864ds/4081Mi) % 300.55/42.94 % (394217)Instruction limit reached! % 300.55/42.94 % (394217)------------------------------ % 300.55/42.94 % (394217)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.55/42.94 % (394217)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.55/42.94 % (394217)CaDiCaL version: 2.1.3 % 300.55/42.94 % (394217)Termination reason: Instruction limit % 300.55/42.94 % (394217)Termination phase: Saturation % 300.55/42.94 % (394217)Time elapsed: 1.160 s % 300.55/42.94 % (394217)Peak memory usage: 118 MB % 300.55/42.94 % (394217)Instructions burned: 3555 (million) % 300.55/42.94 % (394355)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=288276054:cond=fast:i=20260:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2860 on theBenchmark for (2860ds/20260Mi) % 300.55/42.94 % (394355)Refutation not found, incomplete strategy % 300.55/42.94 % (394355)------------------------------ % 300.55/42.94 % (394355)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.55/42.94 % (394355)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.55/42.94 % (394355)CaDiCaL version: 2.1.3 % 300.55/42.94 % (394355)Termination reason: Refutation not found, incomplete strategy % 300.55/42.94 % (394355)Time elapsed: 0.020 s % 300.55/42.94 % (394355)Peak memory usage: 113 MB % 300.55/42.94 % (394355)Instructions burned: 21 (million) % 300.55/42.94 % (394355)------------------------------ % 300.55/42.94 % (394355)------------------------------ % 300.55/42.94 % (394195)Instruction limit reached! % 300.55/42.94 % (394195)------------------------------ % 300.55/42.94 % (394195)Ve % 300.55/42.94 Terminated %------------------------------------------------------------------------------