%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWW744_1 : TPTP v9.3.1. Released v7.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % Computer : n026.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:31:11 PM UTC 2026 % Result : Timeout 300.04s 42.94s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWW744_1 : TPTP v9.3.1. Released v7.0.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.08/0.19 % Computer : n026.cluster.edu % 0.08/0.19 % Model : x86_64 x86_64 % 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.19 % Memory : 8046.5625MB % 0.08/0.19 % OS : Linux 6.8.0-71-generic % 0.08/0.19 % CPULimit : 300 % 0.08/0.19 % WCLimit : 300 % 0.08/0.19 % DateTime : Mon Sep 28 14:31:27 UTC 2026 % 0.08/0.20 % CPUTime : % 0.08/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.08/0.23 Running first-order theorem proving % 0.08/0.23 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 3.71/1.21 % (3888609)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule. % 3.71/1.21 % (3888619)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=390930581:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi) % 3.71/1.21 % (3888619)Instruction limit reached! % 3.71/1.21 % (3888619)------------------------------ % 3.71/1.21 % (3888619)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.71/1.21 % (3888619)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.71/1.21 % (3888619)CaDiCaL version: 2.1.3 % 3.71/1.21 % (3888619)Termination reason: Instruction limit % 3.71/1.21 % (3888619)Termination phase: Property scanning % 3.71/1.21 % (3888619)Time elapsed: 0.012 s % 3.71/1.21 % (3888619)Peak memory usage: 88 MB % 3.71/1.21 % (3888619)Instructions burned: 46 (million) % 3.71/1.21 % (3888614)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=4128121838:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi) % 3.71/1.21 % (3888615)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=760775896:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi) % 3.71/1.21 % (3888616)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=841558061:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi) % 3.71/1.21 % (3888617)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=2940349583:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi) % 3.71/1.21 % (3888618)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=2818486468:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi) % 3.71/1.21 % (3888618)Instruction limit reached! % 3.71/1.21 % (3888618)------------------------------ % 3.71/1.21 % (3888618)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.71/1.21 % (3888618)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.71/1.21 % (3888618)CaDiCaL version: 2.1.3 % 3.71/1.21 % (3888618)Termination reason: Instruction limit % 3.71/1.21 % (3888618)Termination phase: Property scanning % 3.71/1.21 % (3888618)Time elapsed: 0.002 s % 3.71/1.21 % (3888618)Peak memory usage: 85 MB % 3.71/1.21 % (3888618)Instructions burned: 4 (million) % 3.71/1.21 % (3888617)Instruction limit reached! % 3.71/1.21 % (3888617)------------------------------ % 3.71/1.21 % (3888617)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.71/1.21 % (3888617)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.71/1.21 % (3888617)CaDiCaL version: 2.1.3 % 3.71/1.21 % (3888617)Termination reason: Instruction limit % 3.71/1.21 % (3888617)Termination phase: Property scanning % 3.71/1.21 % (3888617)Time elapsed: 0.003 s % 3.71/1.21 % (3888617)Peak memory usage: 85 MB % 3.71/1.21 % (3888617)Instructions burned: 8 (million) % 3.71/1.21 % (3888614)Instruction limit reached! % 3.71/1.21 % (3888614)------------------------------ % 3.71/1.21 % (3888614)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.71/1.21 % (3888614)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.71/1.21 % (3888614)CaDiCaL version: 2.1.3 % 3.71/1.21 % (3888614)Termination reason: Instruction limit % 3.71/1.21 % (3888614)Termination phase: Property scanning % 3.71/1.21 % (3888614)Time elapsed: 0.005 s % 3.71/1.21 % (3888614)Peak memory usage: 85 MB % 3.71/1.21 % (3888614)Instructions burned: 12 (million) % 3.71/1.21 % (3888620)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=2430204554:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi) % 3.71/1.21 % (3888620)Instruction limit reached! % 3.71/1.21 % (3888620)------------------------------ % 3.71/1.21 % (3888620)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.71/1.21 % (3888620)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.71/1.21 % (3888620)CaDiCaL version: 2.1.3 % 3.71/1.21 % (3888620)Termination reason: Instruction limit % 3.71/1.21 % (3888620)Termination phase: Property scanning % 3.71/1.21 % (3888620)Time elapsed: 0.017 s % 3.71/1.21 % (3888620)Peak memory usage: 88 MB % 3.71/1.21 % (3888620)Instructions burned: 35 (million) % 3.71/1.21 % (3888622)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=806251586:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2998 on theBenchmark for (2998ds/14Mi) % 3.71/1.21 % (3888622)Refutation not found, incomplete strategy % 4.36/1.38 % (3888622)------------------------------ % 4.36/1.38 % (3888622)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.36/1.38 % (3888622)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.36/1.38 % (3888622)CaDiCaL version: 2.1.3 % 4.36/1.38 % (3888622)Termination reason: Refutation not found, incomplete strategy % 4.36/1.38 % (3888622)Time elapsed: 0.003 s % 4.36/1.38 % (3888622)Peak memory usage: 88 MB % 4.36/1.38 % (3888622)Instructions burned: 11 (million) % 4.36/1.38 % (3888629)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=4143336100:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2998 on theBenchmark for (2998ds/29Mi) % 4.36/1.38 % (3888630)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=3488218003:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/16Mi) % 4.36/1.38 % (3888630)Instruction limit reached! % 4.36/1.38 % (3888630)------------------------------ % 4.36/1.38 % (3888630)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.36/1.38 % (3888630)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.36/1.38 % (3888630)CaDiCaL version: 2.1.3 % 4.36/1.38 % (3888630)Termination reason: Instruction limit % 4.36/1.38 % (3888630)Termination phase: Naming % 4.36/1.38 % (3888630)Time elapsed: 0.008 s % 4.36/1.38 % (3888630)Peak memory usage: 86 MB % 4.36/1.38 % (3888630)Instructions burned: 17 (million) % 4.36/1.38 % (3888631)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=1868675191:i=24:canc=force:rtra=on_2998 on theBenchmark for (2998ds/24Mi) % 4.36/1.38 % (3888616)Instruction limit reached! % 4.36/1.38 % (3888616)------------------------------ % 4.36/1.38 % (3888616)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.36/1.38 % (3888616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.36/1.38 % (3888616)CaDiCaL version: 2.1.3 % 4.36/1.38 % (3888616)Termination reason: Instruction limit % 4.36/1.38 % (3888616)Termination phase: Saturation % 4.36/1.38 % (3888616)Time elapsed: 0.144 s % 4.36/1.38 % (3888616)Peak memory usage: 120 MB % 4.36/1.38 % (3888616)Instructions burned: 201 (million) % 4.36/1.38 % (3888629)Instruction limit reached! % 4.36/1.38 % (3888629)------------------------------ % 4.36/1.38 % (3888629)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.36/1.38 % (3888629)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.36/1.38 % (3888629)CaDiCaL version: 2.1.3 % 4.36/1.38 % (3888629)Termination reason: Instruction limit % 4.36/1.38 % (3888629)Termination phase: Clausification % 4.36/1.38 % (3888629)Time elapsed: 0.017 s % 4.36/1.38 % (3888629)Peak memory usage: 91 MB % 4.36/1.38 % (3888629)Instructions burned: 29 (million) % 4.36/1.38 % (3888631)Instruction limit reached! % 4.36/1.38 % (3888631)------------------------------ % 4.36/1.38 % (3888631)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.36/1.38 % (3888631)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.36/1.38 % (3888631)CaDiCaL version: 2.1.3 % 4.36/1.38 % (3888631)Termination reason: Instruction limit % 4.36/1.38 % (3888631)Termination phase: Naming % 4.36/1.38 % (3888631)Time elapsed: 0.012 s % 4.36/1.38 % (3888631)Peak memory usage: 87 MB % 4.36/1.38 % (3888631)Instructions burned: 25 (million) % 4.36/1.38 % (3888632)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=153724033:i=27:canc=cautious:fsr=off:rtra=on_2998 on theBenchmark for (2998ds/27Mi) % 4.36/1.38 % (3888632)Instruction limit reached! % 4.36/1.38 % (3888632)------------------------------ % 4.36/1.38 % (3888632)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.36/1.38 % (3888632)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.36/1.38 % (3888632)CaDiCaL version: 2.1.3 % 4.36/1.38 % (3888632)Termination reason: Instruction limit % 4.36/1.38 % (3888632)Termination phase: Preprocessing 3 % 4.36/1.38 % (3888632)Time elapsed: 0.013 s % 4.36/1.38 % (3888632)Peak memory usage: 87 MB % 4.36/1.38 % (3888632)Instructions burned: 28 (million) % 4.36/1.38 % (3888622)------------------------------ % 4.36/1.38 % (3888622)------------------------------ % 4.36/1.38 % (3888639)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=2892992974:i=181:rtra=on:ss=axioms:ev=cautious_2996 on theBenchmark for (2996ds/181Mi) % 5.44/1.50 % (3888638)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=473828687:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2996 on theBenchmark for (2996ds/2Mi) % 5.44/1.50 % (3888637)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=1957890223:i=85:gtgl=4:rtra=on:gtg=exists_sym_2997 on theBenchmark for (2997ds/85Mi) % 5.44/1.50 % (3888638)Instruction limit reached! % 5.44/1.50 % (3888638)------------------------------ % 5.44/1.50 % (3888638)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.44/1.50 % (3888638)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.44/1.50 % (3888638)CaDiCaL version: 2.1.3 % 5.44/1.50 % (3888638)Termination reason: Instruction limit % 5.44/1.50 % (3888638)Termination phase: Property scanning % 5.44/1.50 % (3888638)Time elapsed: 0.002 s % 5.44/1.50 % (3888638)Peak memory usage: 85 MB % 5.44/1.50 % (3888638)Instructions burned: 4 (million) % 5.44/1.50 % (3888639)Refutation not found, incomplete strategy % 5.44/1.50 % (3888639)------------------------------ % 5.44/1.50 % (3888639)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.44/1.50 % (3888639)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.44/1.50 % (3888639)CaDiCaL version: 2.1.3 % 5.44/1.50 % (3888639)Termination reason: Refutation not found, incomplete strategy % 5.44/1.50 % (3888639)Time elapsed: 0.005 s % 5.44/1.50 % (3888639)Peak memory usage: 88 MB % 5.44/1.50 % (3888639)Instructions burned: 10 (million) % 5.44/1.50 % (3888641)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=3699249799:i=4:ep=RST:ins=2:rtra=on_2996 on theBenchmark for (2996ds/4Mi) % 5.44/1.50 % (3888641)Instruction limit reached! % 5.44/1.50 % (3888641)------------------------------ % 5.44/1.50 % (3888641)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.44/1.50 % (3888641)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.44/1.50 % (3888641)CaDiCaL version: 2.1.3 % 5.44/1.50 % (3888641)Termination reason: Instruction limit % 5.44/1.50 % (3888641)Termination phase: Property scanning % 5.44/1.50 % (3888641)Time elapsed: 0.003 s % 5.44/1.50 % (3888641)Peak memory usage: 85 MB % 5.44/1.50 % (3888641)Instructions burned: 6 (million) % 5.44/1.50 % (3888642)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=3520670583:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2996 on theBenchmark for (2996ds/66Mi) % 5.44/1.50 % (3888615)Instruction limit reached! % 5.44/1.50 % (3888615)------------------------------ % 5.44/1.50 % (3888615)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.44/1.50 % (3888615)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.44/1.50 % (3888615)CaDiCaL version: 2.1.3 % 5.44/1.50 % (3888615)Termination reason: Instruction limit % 5.44/1.50 % (3888615)Termination phase: Clausification % 5.44/1.50 % (3888615)Time elapsed: 0.305 s % 5.44/1.50 % (3888615)Peak memory usage: 245 MB % 5.44/1.50 % (3888615)Instructions burned: 307 (million) % 5.44/1.50 % (3888637)Instruction limit reached! % 5.44/1.50 % (3888637)------------------------------ % 5.44/1.50 % (3888637)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.44/1.50 % (3888637)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.44/1.50 % (3888637)CaDiCaL version: 2.1.3 % 5.44/1.50 % (3888637)Termination reason: Instruction limit % 5.44/1.50 % (3888637)Termination phase: Saturation % 5.44/1.50 % (3888637)Time elapsed: 0.039 s % 5.44/1.50 % (3888637)Peak memory usage: 90 MB % 5.44/1.50 % (3888637)Instructions burned: 85 (million) % 5.44/1.50 % (3888643)lrs+10_1_thi=all:si=on:fd=off:random_seed=95069705:i=53:rtra=on:gtg=all_2996 on theBenchmark for (2996ds/53Mi) % 5.44/1.50 % (3888642)Instruction limit reached! % 5.44/1.50 % (3888642)------------------------------ % 5.44/1.50 % (3888642)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.44/1.50 % (3888642)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.44/1.50 % (3888642)CaDiCaL version: 2.1.3 % 5.44/1.50 % (3888642)Termination reason: Instruction limit % 5.44/1.50 % (3888642)Termination phase: Saturation % 5.44/1.50 % (3888642)Time elapsed: 0.051 s % 5.44/1.50 % (3888642)Peak memory usage: 113 MB % 5.44/1.50 % (3888642)Instructions burned: 67 (million) % 5.44/1.50 % (3888643)Instruction limit reached! % 5.44/1.50 % (3888643)------------------------------ % 5.44/1.50 % (3888643)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.15/1.68 % (3888643)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.15/1.68 % (3888643)CaDiCaL version: 2.1.3 % 6.15/1.68 % (3888643)Termination reason: Instruction limit % 6.15/1.68 % (3888643)Termination phase: Property scanning % 6.15/1.68 % (3888643)Time elapsed: 0.018 s % 6.15/1.68 % (3888643)Peak memory usage: 88 MB % 6.15/1.68 % (3888643)Instructions burned: 55 (million) % 6.15/1.68 % (3888647)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=840944967:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2995 on theBenchmark for (2995ds/8Mi) % 6.15/1.68 % (3888647)Instruction limit reached! % 6.15/1.68 % (3888647)------------------------------ % 6.15/1.68 % (3888647)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.15/1.68 % (3888647)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.15/1.68 % (3888647)CaDiCaL version: 2.1.3 % 6.15/1.68 % (3888647)Termination reason: Instruction limit % 6.15/1.68 % (3888647)Termination phase: Property scanning % 6.15/1.68 % (3888647)Time elapsed: 0.004 s % 6.15/1.68 % (3888647)Peak memory usage: 86 MB % 6.15/1.68 % (3888647)Instructions burned: 9 (million) % 6.15/1.68 % (3888650)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=662761908:st=3:i=2:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/2Mi) % 6.15/1.68 % (3888650)Instruction limit reached! % 6.15/1.68 % (3888650)------------------------------ % 6.15/1.68 % (3888650)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.15/1.68 % (3888650)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.15/1.68 % (3888650)CaDiCaL version: 2.1.3 % 6.15/1.68 % (3888650)Termination reason: Instruction limit % 6.15/1.68 % (3888650)Termination phase: Property scanning % 6.15/1.68 % (3888650)Time elapsed: 0.002 s % 6.15/1.68 % (3888650)Peak memory usage: 85 MB % 6.15/1.68 % (3888650)Instructions burned: 3 (million) % 6.15/1.68 % (3888651)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=2583780360:i=2:doe=on:canc=force:asg=cautious:rtra=on_2995 on theBenchmark for (2995ds/2Mi) % 6.15/1.68 % (3888651)Instruction limit reached! % 6.15/1.68 % (3888651)------------------------------ % 6.15/1.68 % (3888651)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.15/1.68 % (3888651)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.15/1.68 % (3888651)CaDiCaL version: 2.1.3 % 6.15/1.68 % (3888651)Termination reason: Instruction limit % 6.15/1.68 % (3888651)Termination phase: Property scanning % 6.15/1.68 % (3888651)Time elapsed: 0.002 s % 6.15/1.68 % (3888651)Peak memory usage: 85 MB % 6.15/1.68 % (3888651)Instructions burned: 3 (million) % 6.15/1.68 % (3888655)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=2636595946:i=26:canc=cautious:av=off:rtra=on_2994 on theBenchmark for (2994ds/26Mi) % 6.15/1.68 % (3888655)Instruction limit reached! % 6.15/1.68 % (3888655)------------------------------ % 6.15/1.68 % (3888655)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.15/1.68 % (3888655)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.15/1.68 % (3888655)CaDiCaL version: 2.1.3 % 6.15/1.68 % (3888655)Termination reason: Instruction limit % 6.15/1.68 % (3888655)Termination phase: Preprocessing 3 % 6.15/1.68 % (3888655)Time elapsed: 0.007 s % 6.15/1.68 % (3888655)Peak memory usage: 87 MB % 6.15/1.68 % (3888655)Instructions burned: 28 (million) % 6.15/1.68 % (3888652)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=3141125490:i=127:doe=on:rtra=on_2995 on theBenchmark for (2995ds/127Mi) % 6.15/1.68 % (3888654)dis+10_1_si=on:random_seed=743190946:i=10:ep=R:rtra=on_2994 on theBenchmark for (2994ds/10Mi) % 6.15/1.68 % (3888654)Instruction limit reached! % 6.15/1.68 % (3888654)------------------------------ % 6.15/1.68 % (3888654)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.15/1.68 % (3888654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.15/1.68 % (3888654)CaDiCaL version: 2.1.3 % 6.15/1.68 % (3888654)Termination reason: Instruction limit % 6.15/1.68 % (3888654)Termination phase: Property scanning % 6.15/1.68 % (3888654)Time elapsed: 0.005 s % 6.15/1.68 % (3888654)Peak memory usage: 86 MB % 6.15/1.68 % (3888654)Instructions burned: 12 (million) % 6.15/1.68 % (3888639)------------------------------ % 6.15/1.68 % (3888639)------------------------------ % 6.15/1.68 % (3888657)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=1990226083: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) % 7.72/1.90 % (3888664)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=2829112472:i=370:ep=RS:fsr=off:rtra=on_2993 on theBenchmark for (2993ds/370Mi) % 7.72/1.90 % (3888659)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=540892276:i=2:fsr=off:rtra=on:inst=on_2994 on theBenchmark for (2994ds/2Mi) % 7.72/1.90 % (3888659)Instruction limit reached! % 7.72/1.90 % (3888659)------------------------------ % 7.72/1.90 % (3888659)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.72/1.90 % (3888659)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.72/1.90 % (3888659)CaDiCaL version: 2.1.3 % 7.72/1.90 % (3888659)Termination reason: Instruction limit % 7.72/1.90 % (3888659)Termination phase: shuffling % 7.72/1.90 % (3888659)Time elapsed: 0.001 s % 7.72/1.90 % (3888659)Peak memory usage: 85 MB % 7.72/1.90 % (3888659)Instructions burned: 2 (million) % 7.72/1.90 % (3888657)Instruction limit reached! % 7.72/1.90 % (3888657)------------------------------ % 7.72/1.90 % (3888657)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.72/1.90 % (3888657)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.72/1.90 % (3888657)CaDiCaL version: 2.1.3 % 7.72/1.90 % (3888657)Termination reason: Instruction limit % 7.72/1.90 % (3888657)Termination phase: Property scanning % 7.72/1.90 % (3888657)Time elapsed: 0.018 s % 7.72/1.90 % (3888657)Peak memory usage: 88 MB % 7.72/1.90 % (3888657)Instructions burned: 35 (million) % 7.72/1.90 % (3888652)Instruction limit reached! % 7.72/1.90 % (3888652)------------------------------ % 7.72/1.90 % (3888652)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.72/1.90 % (3888652)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.72/1.90 % (3888652)CaDiCaL version: 2.1.3 % 7.72/1.90 % (3888652)Termination reason: Instruction limit % 7.72/1.90 % (3888652)Termination phase: Saturation % 7.72/1.90 % (3888652)Time elapsed: 0.098 s % 7.72/1.90 % (3888652)Peak memory usage: 117 MB % 7.72/1.90 % (3888652)Instructions burned: 127 (million) % 7.72/1.90 % (3888662)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=398444995:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2993 on theBenchmark for (2993ds/8Mi) % 7.72/1.90 % (3888662)Instruction limit reached! % 7.72/1.90 % (3888662)------------------------------ % 7.72/1.90 % (3888662)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.72/1.90 % (3888662)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.72/1.90 % (3888662)CaDiCaL version: 2.1.3 % 7.72/1.90 % (3888662)Termination reason: Instruction limit % 7.72/1.90 % (3888662)Termination phase: Property scanning % 7.72/1.90 % (3888662)Time elapsed: 0.004 s % 7.72/1.90 % (3888662)Peak memory usage: 86 MB % 7.72/1.90 % (3888662)Instructions burned: 9 (million) % 7.72/1.90 % (3888666)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=2849888196:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2993 on theBenchmark for (2993ds/13Mi) % 7.72/1.90 % (3888666)Instruction limit reached! % 7.72/1.90 % (3888666)------------------------------ % 7.72/1.90 % (3888666)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.72/1.90 % (3888666)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.72/1.90 % (3888666)CaDiCaL version: 2.1.3 % 7.72/1.90 % (3888666)Termination reason: Instruction limit % 7.72/1.90 % (3888666)Termination phase: Property scanning % 7.72/1.90 % (3888666)Time elapsed: 0.006 s % 7.72/1.90 % (3888666)Peak memory usage: 86 MB % 7.72/1.90 % (3888666)Instructions burned: 15 (million) % 7.72/1.90 % (3888667)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=1025930971:i=226:rtra=on:gtg=position:ss=axioms_2993 on theBenchmark for (2993ds/226Mi) % 7.72/1.90 % (3888664)Instruction limit reached! % 7.72/1.90 % (3888664)------------------------------ % 7.72/1.90 % (3888664)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.72/1.90 % (3888664)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.72/1.90 % (3888664)CaDiCaL version: 2.1.3 % 7.72/1.90 % (3888664)Termination reason: Instruction limit % 10.29/2.18 % (3888664)Termination phase: Saturation % 10.29/2.18 % (3888664)Time elapsed: 0.116 s % 10.29/2.18 % (3888664)Peak memory usage: 96 MB % 10.29/2.18 % (3888664)Instructions burned: 371 (million) % 10.29/2.18 % (3888672)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=508991505:i=71:rtra=on:gtg=exists_top_2992 on theBenchmark for (2992ds/71Mi) % 10.29/2.18 % (3888671)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=3866131842:i=10:rtra=on_2992 on theBenchmark for (2992ds/10Mi) % 10.29/2.18 % (3888667)Refutation not found, incomplete strategy % 10.29/2.18 % (3888667)------------------------------ % 10.29/2.18 % (3888667)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.29/2.18 % (3888667)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.29/2.18 % (3888667)CaDiCaL version: 2.1.3 % 10.29/2.18 % (3888667)Termination reason: Refutation not found, incomplete strategy % 10.29/2.18 % (3888667)Time elapsed: 0.033 s % 10.29/2.18 % (3888667)Peak memory usage: 112 MB % 10.29/2.18 % (3888667)Instructions burned: 21 (million) % 10.29/2.18 % (3888671)Instruction limit reached! % 10.29/2.18 % (3888671)------------------------------ % 10.29/2.18 % (3888671)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.29/2.18 % (3888671)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.29/2.18 % (3888671)CaDiCaL version: 2.1.3 % 10.29/2.18 % (3888671)Termination reason: Instruction limit % 10.29/2.18 % (3888671)Termination phase: Unused predicate definition removal % 10.29/2.18 % (3888671)Time elapsed: 0.005 s % 10.29/2.18 % (3888671)Peak memory usage: 86 MB % 10.29/2.18 % (3888671)Instructions burned: 11 (million) % 10.29/2.18 % (3888673)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=3476936022:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2992 on theBenchmark for (2992ds/75Mi) % 10.29/2.18 % (3888675)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=3510435266:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2992 on theBenchmark for (2992ds/294Mi) % 10.29/2.18 % (3888673)Instruction limit reached! % 10.29/2.18 % (3888673)------------------------------ % 10.29/2.18 % (3888673)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.29/2.18 % (3888673)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.29/2.18 % (3888673)CaDiCaL version: 2.1.3 % 10.29/2.18 % (3888673)Termination reason: Instruction limit % 10.29/2.18 % (3888673)Termination phase: Saturation % 10.29/2.18 % (3888673)Time elapsed: 0.035 s % 10.29/2.18 % (3888673)Peak memory usage: 90 MB % 10.29/2.18 % (3888673)Instructions burned: 75 (million) % 10.29/2.18 % (3888677)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=387154543:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2992 on theBenchmark for (2992ds/130Mi) % 10.29/2.18 % (3888672)Instruction limit reached! % 10.29/2.18 % (3888672)------------------------------ % 10.29/2.18 % (3888672)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.29/2.18 % (3888672)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.29/2.18 % (3888672)CaDiCaL version: 2.1.3 % 10.29/2.18 % (3888672)Termination reason: Instruction limit % 10.29/2.18 % (3888672)Termination phase: Saturation % 10.29/2.18 % (3888672)Time elapsed: 0.062 s % 10.29/2.18 % (3888672)Peak memory usage: 121 MB % 10.29/2.18 % (3888672)Instructions burned: 71 (million) % 10.29/2.18 % (3888679)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=3522402889:i=131:rtra=on_2991 on theBenchmark for (2991ds/131Mi) % 10.29/2.18 % (3888679)Instruction limit reached! % 10.29/2.18 % (3888679)------------------------------ % 10.29/2.18 % (3888679)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.29/2.18 % (3888679)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.29/2.18 % (3888679)CaDiCaL version: 2.1.3 % 10.29/2.18 % (3888679)Termination reason: Instruction limit % 10.29/2.18 % (3888679)Termination phase: Saturation % 10.29/2.18 % (3888679)Time elapsed: 0.068 s % 10.29/2.18 % (3888679)Peak memory usage: 133 MB % 10.29/2.18 % (3888679)Instructions burned: 133 (million) % 10.29/2.18 % (3888683)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=2257021480:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2991 on theBenchmark for (2991ds/40Mi) % 10.29/2.18 % (3888683)Instruction limit reached! % 10.92/2.47 % (3888683)------------------------------ % 10.92/2.47 % (3888683)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.92/2.47 % (3888683)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.92/2.47 % (3888683)CaDiCaL version: 2.1.3 % 10.92/2.47 % (3888683)Termination reason: Instruction limit % 10.92/2.47 % (3888683)Termination phase: Preprocessing 3 % 10.92/2.47 % (3888683)Time elapsed: 0.018 s % 10.92/2.47 % (3888683)Peak memory usage: 87 MB % 10.92/2.47 % (3888683)Instructions burned: 41 (million) % 10.92/2.47 % (3888677)Instruction limit reached! % 10.92/2.47 % (3888677)------------------------------ % 10.92/2.47 % (3888677)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.92/2.47 % (3888677)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.92/2.47 % (3888677)CaDiCaL version: 2.1.3 % 10.92/2.47 % (3888677)Termination reason: Instruction limit % 10.92/2.47 % (3888677)Termination phase: Clausification % 10.92/2.47 % (3888677)Time elapsed: 0.118 s % 10.92/2.47 % (3888677)Peak memory usage: 143 MB % 10.92/2.47 % (3888677)Instructions burned: 131 (million) % 10.92/2.47 % (3888688)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=2016903726:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2990 on theBenchmark for (2990ds/598Mi) % 10.92/2.47 % (3888686)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=2421479357:i=307:rtra=on:gtg=exists_top_2991 on theBenchmark for (2991ds/307Mi) % 10.92/2.47 % (3888690)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=2967766531:i=131:canc=cautious:fsr=off:rtra=on_2990 on theBenchmark for (2990ds/131Mi) % 10.92/2.47 % (3888686)Refutation not found, incomplete strategy % 10.92/2.47 % (3888686)------------------------------ % 10.92/2.47 % (3888686)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.92/2.47 % (3888686)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.92/2.47 % (3888686)CaDiCaL version: 2.1.3 % 10.92/2.47 % (3888686)Termination reason: Refutation not found, incomplete strategy % 10.92/2.47 % (3888686)Time elapsed: 0.056 s % 10.92/2.47 % (3888686)Peak memory usage: 92 MB % 10.92/2.47 % (3888686)Instructions burned: 107 (million) % 10.92/2.47 % (3888667)------------------------------ % 10.92/2.47 % (3888667)------------------------------ % 10.92/2.47 % (3888690)Instruction limit reached! % 10.92/2.47 % (3888690)------------------------------ % 10.92/2.47 % (3888690)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.92/2.47 % (3888690)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.92/2.47 % (3888690)CaDiCaL version: 2.1.3 % 10.92/2.47 % (3888690)Termination reason: Instruction limit % 10.92/2.47 % (3888690)Termination phase: Saturation % 10.92/2.47 % (3888690)Time elapsed: 0.052 s % 10.92/2.47 % (3888690)Peak memory usage: 117 MB % 10.92/2.47 % (3888690)Instructions burned: 134 (million) % 10.92/2.47 % (3888691)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=2986044716:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2989 on theBenchmark for (2989ds/259Mi) % 10.92/2.47 % (3888675)Instruction limit reached! % 10.92/2.47 % (3888675)------------------------------ % 10.92/2.47 % (3888675)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.92/2.47 % (3888675)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.92/2.47 % (3888675)CaDiCaL version: 2.1.3 % 10.92/2.47 % (3888675)Termination reason: Instruction limit % 10.92/2.47 % (3888675)Termination phase: Clausification % 10.92/2.47 % (3888675)Time elapsed: 0.273 s % 10.92/2.47 % (3888675)Peak memory usage: 225 MB % 10.92/2.47 % (3888675)Instructions burned: 295 (million) % 10.92/2.47 % (3888692)dis+10_1_si=on:random_seed=3526662840:s2a=on:i=1000:rtra=on:gtg=exists_all_2989 on theBenchmark for (2989ds/1000Mi) % 10.92/2.47 % (3888691)Refutation not found, incomplete strategy % 10.92/2.47 % (3888691)------------------------------ % 10.92/2.47 % (3888691)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.92/2.47 % (3888691)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.92/2.47 % (3888691)CaDiCaL version: 2.1.3 % 10.92/2.47 % (3888691)Termination reason: Refutation not found, incomplete strategy % 10.92/2.47 % (3888691)Time elapsed: 0.034 s % 10.92/2.47 % (3888691)Peak memory usage: 112 MB % 10.92/2.47 % (3888691)Instructions burned: 22 (million) % 10.92/2.47 % (3888697)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=702733745:i=141:doe=on:rtra=on_2988 on theBenchmark for (2988ds/141Mi) % 13.15/2.68 % (3888696)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=1768156483:i=383:fsr=off:rtra=on:ev=force_2988 on theBenchmark for (2988ds/383Mi) % 13.15/2.68 % (3888697)Instruction limit reached! % 13.15/2.68 % (3888697)------------------------------ % 13.15/2.68 % (3888697)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.15/2.68 % (3888697)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.15/2.68 % (3888697)CaDiCaL version: 2.1.3 % 13.15/2.68 % (3888697)Termination reason: Instruction limit % 13.15/2.68 % (3888697)Termination phase: Saturation % 13.15/2.68 % (3888697)Time elapsed: 0.041 s % 13.15/2.68 % (3888697)Peak memory usage: 93 MB % 13.15/2.68 % (3888697)Instructions burned: 142 (million) % 13.15/2.68 % (3888700)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=1912859131:i=65:nm=16:rtra=on_2988 on theBenchmark for (2988ds/65Mi) % 13.15/2.68 % (3888686)------------------------------ % 13.15/2.68 % (3888686)------------------------------ % 13.15/2.68 % (3888700)Instruction limit reached! % 13.15/2.68 % (3888700)------------------------------ % 13.15/2.68 % (3888700)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.15/2.68 % (3888700)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.15/2.68 % (3888700)CaDiCaL version: 2.1.3 % 13.15/2.68 % (3888700)Termination reason: Instruction limit % 13.15/2.68 % (3888700)Termination phase: Saturation % 13.15/2.68 % (3888700)Time elapsed: 0.029 s % 13.15/2.68 % (3888700)Peak memory usage: 89 MB % 13.15/2.68 % (3888700)Instructions burned: 67 (million) % 13.15/2.68 % (3888703)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=4048209598:i=121:nm=16:rtra=on_2987 on theBenchmark for (2987ds/121Mi) % 13.15/2.68 % (3888703)Instruction limit reached! % 13.15/2.68 % (3888703)------------------------------ % 13.15/2.68 % (3888703)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.15/2.68 % (3888703)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.15/2.68 % (3888703)CaDiCaL version: 2.1.3 % 13.15/2.68 % (3888703)Termination reason: Instruction limit % 13.15/2.68 % (3888703)Termination phase: Saturation % 13.15/2.68 % (3888703)Time elapsed: 0.033 s % 13.15/2.68 % (3888703)Peak memory usage: 91 MB % 13.15/2.68 % (3888703)Instructions burned: 123 (million) % 13.15/2.68 % (3888688)Instruction limit reached! % 13.15/2.68 % (3888688)------------------------------ % 13.15/2.68 % (3888688)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.15/2.68 % (3888688)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.15/2.68 % (3888688)CaDiCaL version: 2.1.3 % 13.15/2.68 % (3888688)Termination reason: Instruction limit % 13.15/2.68 % (3888688)Termination phase: Saturation % 13.15/2.68 % (3888688)Time elapsed: 0.369 s % 13.15/2.68 % (3888688)Peak memory usage: 141 MB % 13.15/2.68 % (3888688)Instructions burned: 599 (million) % 13.15/2.68 % (3888691)------------------------------ % 13.15/2.68 % (3888691)------------------------------ % 13.15/2.68 % (3888696)Instruction limit reached! % 13.15/2.68 % (3888696)------------------------------ % 13.15/2.68 % (3888696)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.15/2.68 % (3888696)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.15/2.68 % (3888696)CaDiCaL version: 2.1.3 % 13.15/2.68 % (3888696)Termination reason: Instruction limit % 13.15/2.68 % (3888696)Termination phase: Saturation % 13.15/2.68 % (3888696)Time elapsed: 0.211 s % 13.15/2.68 % (3888696)Peak memory usage: 96 MB % 13.15/2.68 % (3888696)Instructions burned: 383 (million) % 13.15/2.68 % (3888705)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=4037870524:s2a=on:i=128:s2at=5:ins=3:rtra=on_2986 on theBenchmark for (2986ds/128Mi) % 13.15/2.68 % (3888708)dis+1010_1_to=kbo:si=on:random_seed=1038421160:i=175:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2986 on theBenchmark for (2986ds/175Mi) % 13.15/2.68 % (3888706)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=1488886790:i=39:ins=3:rtra=on_2986 on theBenchmark for (2986ds/39Mi) % 13.15/2.68 % (3888706)Instruction limit reached! % 13.15/2.68 % (3888706)------------------------------ % 13.15/2.68 % (3888706)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.20/3.01 % (3888706)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.20/3.01 % (3888706)CaDiCaL version: 2.1.3 % 15.20/3.01 % (3888706)Termination reason: Instruction limit % 15.20/3.01 % (3888706)Termination phase: Property scanning % 15.20/3.01 % (3888706)Time elapsed: 0.019 s % 15.20/3.01 % (3888706)Peak memory usage: 88 MB % 15.20/3.01 % (3888706)Instructions burned: 41 (million) % 15.20/3.01 % (3888705)Refutation not found, incomplete strategy % 15.20/3.01 % (3888705)------------------------------ % 15.20/3.01 % (3888705)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.20/3.01 % (3888705)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.20/3.01 % (3888705)CaDiCaL version: 2.1.3 % 15.20/3.01 % (3888705)Termination reason: Refutation not found, incomplete strategy % 15.20/3.01 % (3888705)Time elapsed: 0.082 s % 15.20/3.01 % (3888705)Peak memory usage: 116 MB % 15.20/3.01 % (3888705)Instructions burned: 112 (million) % 15.20/3.01 % (3888709)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=843274515:i=329:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2985 on theBenchmark for (2985ds/329Mi) % 15.20/3.01 % (3888708)Instruction limit reached! % 15.20/3.01 % (3888708)------------------------------ % 15.20/3.01 % (3888708)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.20/3.01 % (3888708)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.20/3.01 % (3888708)CaDiCaL version: 2.1.3 % 15.20/3.01 % (3888708)Termination reason: Instruction limit % 15.20/3.01 % (3888708)Termination phase: Clausification % 15.20/3.01 % (3888708)Time elapsed: 0.092 s % 15.20/3.01 % (3888708)Peak memory usage: 163 MB % 15.20/3.01 % (3888708)Instructions burned: 176 (million) % 15.20/3.01 % (3888710)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=3388927221:s2a=on:i=483:doe=on:nm=32:rtra=on_2985 on theBenchmark for (2985ds/483Mi) % 15.20/3.01 % (3888711)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=1672554492:thitd=on:i=215:nm=0:rtra=on:ev=force_2985 on theBenchmark for (2985ds/215Mi) % 15.20/3.01 % (3888715)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=1514876002:i=349:rtra=on_2984 on theBenchmark for (2984ds/349Mi) % 15.20/3.01 % (3888719)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=116142731:st=2:i=295:rtra=on:ss=axioms_2984 on theBenchmark for (2984ds/295Mi) % 15.20/3.01 % (3888719)Refutation not found, incomplete strategy % 15.20/3.01 % (3888719)------------------------------ % 15.20/3.01 % (3888719)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.20/3.01 % (3888719)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.20/3.01 % (3888719)CaDiCaL version: 2.1.3 % 15.20/3.01 % (3888719)Termination reason: Refutation not found, incomplete strategy % 15.20/3.01 % (3888719)Time elapsed: 0.004 s % 15.20/3.01 % (3888719)Peak memory usage: 88 MB % 15.20/3.01 % (3888719)Instructions burned: 17 (million) % 15.20/3.01 % (3888692)Instruction limit reached! % 15.20/3.01 % (3888692)------------------------------ % 15.20/3.01 % (3888692)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.20/3.01 % (3888692)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.20/3.01 % (3888692)CaDiCaL version: 2.1.3 % 15.20/3.01 % (3888692)Termination reason: Instruction limit % 15.20/3.01 % (3888692)Termination phase: Saturation % 15.20/3.01 % (3888692)Time elapsed: 0.555 s % 15.20/3.01 % (3888692)Peak memory usage: 98 MB % 15.20/3.01 % (3888692)Instructions burned: 1000 (million) % 15.20/3.01 % (3888711)Instruction limit reached! % 15.20/3.01 % (3888711)------------------------------ % 15.20/3.01 % (3888711)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.20/3.01 % (3888711)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.20/3.01 % (3888711)CaDiCaL version: 2.1.3 % 15.20/3.01 % (3888711)Termination reason: Instruction limit % 15.20/3.01 % (3888711)Termination phase: Clausification % 15.20/3.01 % (3888711)Time elapsed: 0.195 s % 15.20/3.01 % (3888711)Peak memory usage: 185 MB % 15.20/3.01 % (3888711)Instructions burned: 215 (million) % 15.20/3.01 % (3888705)------------------------------ % 15.20/3.01 % (3888705)------------------------------ % 15.20/3.01 % (3888709)Instruction limit reached! % 15.20/3.01 % (3888709)------------------------------ % 15.20/3.01 % (3888709)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.80/3.23 % (3888709)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.80/3.23 % (3888709)CaDiCaL version: 2.1.3 % 17.80/3.23 % (3888709)Termination reason: Instruction limit % 17.80/3.23 % (3888709)Termination phase: Saturation % 17.80/3.23 % (3888709)Time elapsed: 0.237 s % 17.80/3.23 % (3888709)Peak memory usage: 122 MB % 17.80/3.23 % (3888709)Instructions burned: 330 (million) % 17.80/3.23 % (3888719)------------------------------ % 17.80/3.23 % (3888719)------------------------------ % 17.80/3.23 % (3888722)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=3025953354:i=328:kws=inv_frequency:nm=20:rtra=on_2982 on theBenchmark for (2982ds/328Mi) % 17.80/3.23 % (3888710)Instruction limit reached! % 17.80/3.23 % (3888710)------------------------------ % 17.80/3.23 % (3888710)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.80/3.23 % (3888710)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.80/3.23 % (3888710)CaDiCaL version: 2.1.3 % 17.80/3.23 % (3888710)Termination reason: Instruction limit % 17.80/3.23 % (3888710)Termination phase: Saturation % 17.80/3.23 % (3888710)Time elapsed: 0.291 s % 17.80/3.23 % (3888710)Peak memory usage: 140 MB % 17.80/3.23 % (3888710)Instructions burned: 483 (million) % 17.80/3.23 % (3888715)Instruction limit reached! % 17.80/3.23 % (3888715)------------------------------ % 17.80/3.23 % (3888715)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.80/3.23 % (3888715)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.80/3.23 % (3888715)CaDiCaL version: 2.1.3 % 17.80/3.23 % (3888715)Termination reason: Instruction limit % 17.80/3.23 % (3888715)Termination phase: Saturation % 17.80/3.23 % (3888715)Time elapsed: 0.215 s % 17.80/3.23 % (3888715)Peak memory usage: 123 MB % 17.80/3.23 % (3888715)Instructions burned: 350 (million) % 17.80/3.23 % (3888723)dis+1010_1_to=lpo:sil=128000:sas=z3:si=on:nwc=5:random_seed=4131324510:i=281:gtgl=2:rtra=on:gtg=all_2982 on theBenchmark for (2982ds/281Mi) % 17.80/3.23 % (3888726)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=3685184658:i=416:rtra=on:gtg=position:ss=axioms_2981 on theBenchmark for (2981ds/416Mi) % 17.80/3.23 % (3888726)Refutation not found, incomplete strategy % 17.80/3.23 % (3888726)------------------------------ % 17.80/3.23 % (3888726)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.80/3.23 % (3888726)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.80/3.23 % (3888726)CaDiCaL version: 2.1.3 % 17.80/3.23 % (3888726)Termination reason: Refutation not found, incomplete strategy % 17.80/3.23 % (3888726)Time elapsed: 0.020 s % 17.80/3.23 % (3888726)Peak memory usage: 112 MB % 17.80/3.23 % (3888726)Instructions burned: 21 (million) % 17.80/3.23 % (3888724)lrs+1010_1_to=kbo:sil=128000:si=on:sos=on:urr=on:uwa=alasca_main:random_seed=611464329:i=484:doe=on:nm=0:av=off:rtra=on:ss=axioms_2982 on theBenchmark for (2982ds/484Mi) % 17.80/3.23 % (3888725)lrs+21_1_to=kbo:sil=128000:thi=neg_eq:si=on:random_seed=3747802690:i=321:canc=force:rtra=on:tac=axiom:ss=axioms:ev=force_2982 on theBenchmark for (2982ds/321Mi) % 17.80/3.23 % (3888724)Refutation not found, incomplete strategy % 17.80/3.23 % (3888724)------------------------------ % 17.80/3.23 % (3888724)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.80/3.23 % (3888724)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.80/3.23 % (3888724)CaDiCaL version: 2.1.3 % 17.80/3.23 % (3888724)Termination reason: Refutation not found, incomplete strategy % 17.80/3.23 % (3888724)Time elapsed: 0.007 s % 17.80/3.23 % (3888724)Peak memory usage: 88 MB % 17.80/3.23 % (3888724)Instructions burned: 16 (million) % 17.80/3.23 % (3888725)Refutation not found, incomplete strategy % 17.80/3.23 % (3888725)------------------------------ % 17.80/3.23 % (3888725)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.80/3.23 % (3888725)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.80/3.23 % (3888725)CaDiCaL version: 2.1.3 % 17.80/3.23 % (3888725)Termination reason: Refutation not found, incomplete strategy % 17.80/3.23 % (3888725)Time elapsed: 0.033 s % 17.80/3.23 % (3888725)Peak memory usage: 112 MB % 17.80/3.23 % (3888725)Instructions burned: 21 (million) % 17.80/3.23 % (3888728)lrs+1010_1_to=kbo:tgt=ground:fde=unused:sas=z3:si=on:sp=unary_frequency:gve=force:spb=goal:tha=off:random_seed=12352661:i=471:thf=on:kws=precedence:rtra=on_2981 on theBenchmark for (2981ds/471Mi) % 18.99/3.54 % (3888729)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=2378654874:avsq=on:i=276:avsqr=1,2:rtra=on_2981 on theBenchmark for (2981ds/276Mi) % 18.99/3.54 % (3888722)Instruction limit reached! % 18.99/3.54 % (3888722)------------------------------ % 18.99/3.54 % (3888722)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.99/3.54 % (3888722)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.99/3.54 % (3888722)CaDiCaL version: 2.1.3 % 18.99/3.54 % (3888722)Termination reason: Instruction limit % 18.99/3.54 % (3888722)Termination phase: Saturation % 18.99/3.54 % (3888722)Time elapsed: 0.197 s % 18.99/3.54 % (3888722)Peak memory usage: 123 MB % 18.99/3.54 % (3888722)Instructions burned: 330 (million) % 18.99/3.54 % (3888723)Instruction limit reached! % 18.99/3.54 % (3888723)------------------------------ % 18.99/3.54 % (3888723)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.99/3.54 % (3888723)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.99/3.54 % (3888723)CaDiCaL version: 2.1.3 % 18.99/3.54 % (3888723)Termination reason: Instruction limit % 18.99/3.54 % (3888723)Termination phase: Saturation % 18.99/3.54 % (3888723)Time elapsed: 0.170 s % 18.99/3.54 % (3888723)Peak memory usage: 122 MB % 18.99/3.54 % (3888723)Instructions burned: 282 (million) % 18.99/3.54 % (3888726)------------------------------ % 18.99/3.54 % (3888726)------------------------------ % 18.99/3.54 % (3888738)lrs+10_1_to=kbo:sil=128000:fde=none:si=on:norm_ineq=on:urr=on:nwc=0.5:random_seed=3835593675:i=513:kws=frequency:bd=all:rtra=on:gtg=exists_all:ss=axioms:sgt=4_2979 on theBenchmark for (2979ds/513Mi) % 18.99/3.54 % (3888736)lrs+1010_2_to=kbo:sil=128000:tgt=ground:fde=unused:sas=z3:si=on:uwa=off:tha=off:nwc=1:random_seed=4235009983:i=375:kws=inv_arity_squared:rtra=on_2979 on theBenchmark for (2979ds/375Mi) % 18.99/3.54 % (3888724)------------------------------ % 18.99/3.54 % (3888724)------------------------------ % 18.99/3.54 % (3888729)Instruction limit reached! % 18.99/3.54 % (3888729)------------------------------ % 18.99/3.54 % (3888729)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.99/3.54 % (3888729)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.99/3.54 % (3888729)CaDiCaL version: 2.1.3 % 18.99/3.54 % (3888729)Termination reason: Instruction limit % 18.99/3.54 % (3888729)Termination phase: Saturation % 18.99/3.54 % (3888729)Time elapsed: 0.190 s % 18.99/3.54 % (3888729)Peak memory usage: 135 MB % 18.99/3.54 % (3888729)Instructions burned: 277 (million) % 18.99/3.54 % (3888725)------------------------------ % 18.99/3.54 % (3888725)------------------------------ % 18.99/3.54 % (3888737)lrs+10_1_to=kbo:sil=128000:tgt=full:sas=z3:si=on:uwa=func_ext:slsqc=1:flr=on:slsq=on:random_seed=1395335131:i=387:bd=preordered:rtra=on:ss=axioms:sgt=8_2979 on theBenchmark for (2979ds/387Mi) % 18.99/3.54 % (3888737)Refutation not found, incomplete strategy % 18.99/3.54 % (3888737)------------------------------ % 18.99/3.54 % (3888737)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.99/3.54 % (3888737)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.99/3.54 % (3888737)CaDiCaL version: 2.1.3 % 18.99/3.54 % (3888737)Termination reason: Refutation not found, incomplete strategy % 18.99/3.54 % (3888737)Time elapsed: 0.034 s % 18.99/3.54 % (3888737)Peak memory usage: 112 MB % 18.99/3.54 % (3888737)Instructions burned: 23 (million) % 18.99/3.54 % (3888728)Instruction limit reached! % 18.99/3.54 % (3888728)------------------------------ % 18.99/3.54 % (3888728)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.99/3.54 % (3888728)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.99/3.54 % (3888728)CaDiCaL version: 2.1.3 % 18.99/3.54 % (3888728)Termination reason: Instruction limit % 18.99/3.54 % (3888728)Termination phase: Saturation % 18.99/3.54 % (3888728)Time elapsed: 0.276 s % 18.99/3.54 % (3888728)Peak memory usage: 123 MB % 18.99/3.54 % (3888728)Instructions burned: 471 (million) % 18.99/3.54 % (3888741)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=3481507324:i=334:rtra=on_2978 on theBenchmark for (2978ds/334Mi) % 18.99/3.54 % (3888742)lrs+1010_1_to=kbo:sil=64000:sas=cadical:si=on:sos=on:bce=on:random_seed=1152557739:i=359:rtra=on:gtg=exists_top:ss=axioms_2978 on theBenchmark for (2978ds/359Mi) % 18.99/3.54 % (3888742)Refutation not found, incomplete strategy % 21.02/3.95 % (3888742)------------------------------ % 21.02/3.95 % (3888742)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.02/3.95 % (3888742)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.02/3.95 % (3888742)CaDiCaL version: 2.1.3 % 21.02/3.95 % (3888742)Termination reason: Refutation not found, incomplete strategy % 21.02/3.95 % (3888742)Time elapsed: 0.010 s % 21.02/3.95 % (3888742)Peak memory usage: 89 MB % 21.02/3.95 % (3888742)Instructions burned: 22 (million) % 21.02/3.95 % (3888738)Instruction limit reached! % 21.02/3.95 % (3888738)------------------------------ % 21.02/3.95 % (3888738)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.02/3.95 % (3888738)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.02/3.95 % (3888738)CaDiCaL version: 2.1.3 % 21.02/3.95 % (3888738)Termination reason: Instruction limit % 21.02/3.95 % (3888738)Termination phase: Saturation % 21.02/3.95 % (3888738)Time elapsed: 0.168 s % 21.02/3.95 % (3888738)Peak memory usage: 97 MB % 21.02/3.95 % (3888738)Instructions burned: 514 (million) % 21.02/3.95 % (3888744)dis+1010_1_to=lpo:sil=128000:thi=all:fde=unused:si=on:sp=reverse_arity:tha=off:random_seed=3720897396:i=341:gtgl=2:rtra=on:gtg=exists_sym:ev=force:fsd=on:fsdmm=1_2977 on theBenchmark for (2977ds/341Mi) % 21.02/3.96 % (3888736)Instruction limit reached! % 21.02/3.96 % (3888736)------------------------------ % 21.02/3.96 % (3888736)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.02/3.96 % (3888736)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.02/3.96 % (3888736)CaDiCaL version: 2.1.3 % 21.02/3.96 % (3888736)Termination reason: Instruction limit % 21.02/3.96 % (3888736)Termination phase: Saturation % 21.02/3.96 % (3888736)Time elapsed: 0.227 s % 21.02/3.96 % (3888736)Peak memory usage: 123 MB % 21.02/3.96 % (3888736)Instructions burned: 376 (million) % 21.02/3.96 % (3888745)lrs-2_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_max:tha=off:random_seed=1651597971:st=1.5:i=261:sd=1:kws=precedence:rtra=on:ss=axioms_2977 on theBenchmark for (2977ds/261Mi) % 21.02/3.96 % (3888749)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=3106107873:s2pl=no:i=235:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2976 on theBenchmark for (2976ds/235Mi) % 21.02/3.96 % (3888749)Refutation not found, incomplete strategy % 21.02/3.96 % (3888749)------------------------------ % 21.02/3.96 % (3888749)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.02/3.96 % (3888749)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.02/3.96 % (3888749)CaDiCaL version: 2.1.3 % 21.02/3.96 % (3888749)Termination reason: Refutation not found, incomplete strategy % 21.02/3.96 % (3888749)Time elapsed: 0.020 s % 21.02/3.96 % (3888749)Peak memory usage: 112 MB % 21.02/3.96 % (3888749)Instructions burned: 22 (million) % 21.02/3.96 % (3888745)Refutation not found, incomplete strategy % 21.02/3.96 % (3888745)------------------------------ % 21.02/3.96 % (3888745)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.02/3.96 % (3888745)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.02/3.96 % (3888745)CaDiCaL version: 2.1.3 % 21.02/3.96 % (3888745)Termination reason: Refutation not found, incomplete strategy % 21.02/3.96 % (3888745)Time elapsed: 0.031 s % 21.02/3.96 % (3888745)Peak memory usage: 111 MB % 21.02/3.96 % (3888745)Instructions burned: 16 (million) % 21.02/3.96 % (3888737)------------------------------ % 21.02/3.96 % (3888737)------------------------------ % 21.02/3.96 % (3888741)Instruction limit reached! % 21.02/3.96 % (3888741)------------------------------ % 21.02/3.96 % (3888741)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.02/3.96 % (3888741)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.02/3.96 % (3888741)CaDiCaL version: 2.1.3 % 21.02/3.96 % (3888741)Termination reason: Instruction limit % 21.02/3.96 % (3888741)Termination phase: Saturation % 21.02/3.96 % (3888741)Time elapsed: 0.227 s % 21.02/3.96 % (3888741)Peak memory usage: 139 MB % 21.02/3.96 % (3888741)Instructions burned: 335 (million) % 21.02/3.96 % (3888750)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=3850383151:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2976 on theBenchmark for (2976ds/273Mi) % 21.02/3.96 % (3888744)Instruction limit reached! % 21.02/3.96 % (3888744)------------------------------ % 25.81/4.47 % (3888744)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.81/4.47 % (3888744)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.81/4.47 % (3888744)CaDiCaL version: 2.1.3 % 25.81/4.47 % (3888744)Termination reason: Instruction limit % 25.81/4.47 % (3888744)Termination phase: Saturation % 25.81/4.47 % (3888744)Time elapsed: 0.214 s % 25.81/4.47 % (3888744)Peak memory usage: 119 MB % 25.81/4.47 % (3888744)Instructions burned: 342 (million) % 25.81/4.47 % (3888742)------------------------------ % 25.81/4.47 % (3888742)------------------------------ % 25.81/4.47 % (3888749)------------------------------ % 25.81/4.47 % (3888749)------------------------------ % 25.81/4.47 % (3888753)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=2371495275:i=146:doe=on:rtra=on_2975 on theBenchmark for (2975ds/146Mi) % 25.81/4.47 % (3888755)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=2201285133:i=4428:doe=on:fsr=off:rtra=on_2974 on theBenchmark for (2974ds/4428Mi) % 25.81/4.47 % (3888756)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=3582898182:avsq=on:i=276:avsqr=1,2:rtra=on_2974 on theBenchmark for (2974ds/276Mi) % 25.81/4.47 % (3888758)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=1136854659:i=655:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2974 on theBenchmark for (2974ds/655Mi) % 25.81/4.47 % (3888745)------------------------------ % 25.81/4.47 % (3888745)------------------------------ % 25.81/4.47 % (3888753)Instruction limit reached! % 25.81/4.47 % (3888753)------------------------------ % 25.81/4.47 % (3888753)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.81/4.47 % (3888753)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.81/4.47 % (3888753)CaDiCaL version: 2.1.3 % 25.81/4.47 % (3888753)Termination reason: Instruction limit % 25.81/4.47 % (3888753)Termination phase: Saturation % 25.81/4.47 % (3888753)Time elapsed: 0.081 s % 25.81/4.47 % (3888753)Peak memory usage: 93 MB % 25.81/4.47 % (3888753)Instructions burned: 147 (million) % 25.81/4.47 % (3888750)Instruction limit reached! % 25.81/4.47 % (3888750)------------------------------ % 25.81/4.47 % (3888750)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.81/4.47 % (3888750)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.81/4.47 % (3888750)CaDiCaL version: 2.1.3 % 25.81/4.47 % (3888750)Termination reason: Instruction limit % 25.81/4.47 % (3888750)Termination phase: Saturation % 25.81/4.47 % (3888750)Time elapsed: 0.164 s % 25.81/4.47 % (3888750)Peak memory usage: 95 MB % 25.81/4.47 % (3888750)Instructions burned: 273 (million) % 25.81/4.47 % (3888757)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=1574179600:i=1052:rtra=on_2974 on theBenchmark for (2974ds/1052Mi) % 25.81/4.47 % (3888765)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=270133669:s2a=on:i=450:doe=on:nm=32:rtra=on_2972 on theBenchmark for (2972ds/450Mi) % 25.81/4.47 % (3888764)lrs-1002_1_to=kbo:sas=z3:si=on:norm_ineq=on:sos=on:tha=some:random_seed=1649581215:i=107:rtra=on_2972 on theBenchmark for (2972ds/107Mi) % 25.81/4.47 % (3888763)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=3226884687:st=5:i=1054:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2972 on theBenchmark for (2972ds/1054Mi) % 25.81/4.47 % (3888763)Refutation not found, incomplete strategy % 25.81/4.47 % (3888763)------------------------------ % 25.81/4.47 % (3888763)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.81/4.47 % (3888763)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.81/4.47 % (3888763)CaDiCaL version: 2.1.3 % 25.81/4.47 % (3888763)Termination reason: Refutation not found, incomplete strategy % 25.81/4.47 % (3888763)Time elapsed: 0.005 s % 25.81/4.47 % (3888763)Peak memory usage: 88 MB % 25.81/4.47 % (3888763)Instructions burned: 11 (million) % 25.81/4.47 % (3888756)Instruction limit reached! % 25.81/4.47 % (3888756)------------------------------ % 25.81/4.47 % (3888756)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.81/4.47 % (3888756)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.81/4.47 % (3888756)CaDiCaL version: 2.1.3 % 25.81/4.47 % (3888756)Termination reason: Instruction limit % 25.81/4.47 % (3888756)Termination phase: Saturation % 28.67/4.84 % (3888756)Time elapsed: 0.184 s % 28.67/4.84 % (3888756)Peak memory usage: 137 MB % 28.67/4.84 % (3888756)Instructions burned: 277 (million) % 28.67/4.84 % (3888758)Instruction limit reached! % 28.67/4.84 % (3888758)------------------------------ % 28.67/4.84 % (3888758)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 28.67/4.84 % (3888758)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.67/4.84 % (3888758)CaDiCaL version: 2.1.3 % 28.67/4.84 % (3888758)Termination reason: Instruction limit % 28.67/4.84 % (3888758)Termination phase: Saturation % 28.67/4.84 % (3888758)Time elapsed: 0.203 s % 28.67/4.84 % (3888758)Peak memory usage: 96 MB % 28.67/4.84 % (3888758)Instructions burned: 656 (million) % 28.67/4.84 % (3888764)Refutation not found, incomplete strategy % 28.67/4.84 % (3888764)------------------------------ % 28.67/4.84 % (3888764)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 28.67/4.84 % (3888764)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.67/4.84 % (3888764)CaDiCaL version: 2.1.3 % 28.67/4.84 % (3888764)Termination reason: Refutation not found, incomplete strategy % 28.67/4.84 % (3888764)Time elapsed: 0.073 s % 28.67/4.84 % (3888764)Peak memory usage: 115 MB % 28.67/4.84 % (3888764)Instructions burned: 101 (million) % 28.67/4.84 % (3888771)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=499687257:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2971 on theBenchmark for (2971ds/130Mi) % 28.67/4.84 % (3888770)WARNING Broken Constraint: if demodulation_redundancy_check(ordering) has been set then forward_demodulation(off) is not equal to off or backward_demodulation(off) is not equal to off or partial_redundancy_check(off) is not equal to off % 28.67/4.84 % (3888770)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=1424554583:i=1090:aac=none:nm=0:rtra=on:rawr=on_2971 on theBenchmark for (2971ds/1090Mi) % 28.67/4.84 % (3888771)Instruction limit reached! % 28.67/4.84 % (3888771)------------------------------ % 28.67/4.84 % (3888771)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 28.67/4.84 % (3888771)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.67/4.84 % (3888771)CaDiCaL version: 2.1.3 % 28.67/4.84 % (3888771)Termination reason: Instruction limit % 28.67/4.84 % (3888771)Termination phase: Clausification % 28.67/4.84 % (3888771)Time elapsed: 0.070 s % 28.67/4.84 % (3888771)Peak memory usage: 147 MB % 28.67/4.84 % (3888771)Instructions burned: 131 (million) % 28.67/4.84 % (3888763)------------------------------ % 28.67/4.84 % (3888763)------------------------------ % 28.67/4.84 % (3888765)Instruction limit reached! % 28.67/4.84 % (3888765)------------------------------ % 28.67/4.84 % (3888765)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 28.67/4.84 % (3888765)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.67/4.84 % (3888765)CaDiCaL version: 2.1.3 % 28.67/4.84 % (3888765)Termination reason: Instruction limit % 28.67/4.84 % (3888765)Termination phase: Saturation % 28.67/4.84 % (3888765)Time elapsed: 0.269 s % 28.67/4.84 % (3888765)Peak memory usage: 138 MB % 28.67/4.84 % (3888765)Instructions burned: 451 (million) % 28.67/4.84 % (3888774)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=2228830215:i=312:kws=inv_frequency:nm=20:rtra=on_2969 on theBenchmark for (2969ds/312Mi) % 28.67/4.84 % (3888764)------------------------------ % 28.67/4.84 % (3888764)------------------------------ % 28.67/4.84 % (3888775)ott+10_1_to=kbo:sil=64000:si=on:sp=reverse_frequency:sos=on:random_seed=3994816431:i=491:doe=on:rtra=on:gtg=position_2969 on theBenchmark for (2969ds/491Mi) % 28.67/4.84 % (3888774)Instruction limit reached! % 28.67/4.84 % (3888774)------------------------------ % 28.67/4.84 % (3888774)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 28.67/4.84 % (3888774)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.67/4.84 % (3888774)CaDiCaL version: 2.1.3 % 28.67/4.84 % (3888774)Termination reason: Instruction limit % 28.67/4.84 % (3888774)Termination phase: Saturation % 28.67/4.84 % (3888774)Time elapsed: 0.105 s % 28.67/4.84 % (3888774)Peak memory usage: 122 MB % 28.67/4.84 % (3888774)Instructions burned: 318 (million) % 28.67/4.84 % (3888776)ott+1011_4:1_to=lpo:sil=64000:si=on:spb=intro:random_seed=1529682024:s2a=on:i=835:s2at=2:rtra=on_2968 on theBenchmark for (2968ds/835Mi) % 28.67/4.84 % (3888775)Refutation not found, incomplete strategy % 28.67/4.84 % (3888775)------------------------------ % 34.10/5.60 % (3888775)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.10/5.60 % (3888775)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.10/5.60 % (3888775)CaDiCaL version: 2.1.3 % 34.10/5.60 % (3888775)Termination reason: Refutation not found, incomplete strategy % 34.10/5.60 % (3888775)Time elapsed: 0.048 s % 34.10/5.60 % (3888775)Peak memory usage: 91 MB % 34.10/5.60 % (3888775)Instructions burned: 98 (million) % 34.10/5.60 % (3888778)ott+1011_2_to=lpo:sil=128000:si=on:sos=on:random_seed=2253532286:i=307:bd=preordered:av=off:rtra=on:ev=cautious_2968 on theBenchmark for (2968ds/307Mi) % 34.10/5.60 % (3888757)Instruction limit reached! % 34.10/5.60 % (3888757)------------------------------ % 34.10/5.60 % (3888757)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.10/5.60 % (3888757)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.10/5.60 % (3888757)CaDiCaL version: 2.1.3 % 34.10/5.60 % (3888757)Termination reason: Instruction limit % 34.10/5.60 % (3888757)Termination phase: Saturation % 34.10/5.60 % (3888757)Time elapsed: 0.612 s % 34.10/5.60 % (3888757)Peak memory usage: 97 MB % 34.10/5.60 % (3888757)Instructions burned: 1054 (million) % 34.10/5.60 % (3888781)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=1856645814:i=776:doe=on:rtra=on_2967 on theBenchmark for (2967ds/776Mi) % 34.10/5.60 % (3888778)Refutation not found, incomplete strategy % 34.10/5.60 % (3888778)------------------------------ % 34.10/5.60 % (3888778)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.10/5.60 % (3888778)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.10/5.60 % (3888778)CaDiCaL version: 2.1.3 % 34.10/5.60 % (3888778)Termination reason: Refutation not found, incomplete strategy % 34.10/5.60 % (3888778)Time elapsed: 0.064 s % 34.10/5.60 % (3888778)Peak memory usage: 92 MB % 34.10/5.60 % (3888778)Instructions burned: 122 (million) % 34.10/5.60 % (3888783)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=873487911:s2a=on:i=646:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2966 on theBenchmark for (2966ds/646Mi) % 34.10/5.60 % (3888775)------------------------------ % 34.10/5.60 % (3888775)------------------------------ % 34.10/5.60 % (3888781)Instruction limit reached! % 34.10/5.60 % (3888781)------------------------------ % 34.10/5.60 % (3888781)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.10/5.60 % (3888781)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.10/5.60 % (3888781)CaDiCaL version: 2.1.3 % 34.10/5.60 % (3888781)Termination reason: Instruction limit % 34.10/5.60 % (3888781)Termination phase: Saturation % 34.10/5.60 % (3888781)Time elapsed: 0.228 s % 34.10/5.60 % (3888781)Peak memory usage: 123 MB % 34.10/5.60 % (3888781)Instructions burned: 778 (million) % 34.10/5.60 % (3888778)------------------------------ % 34.10/5.60 % (3888778)------------------------------ % 34.10/5.60 % (3888786)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=3916187319:thitd=on:cond=fast:i=784:nm=30:rtra=on:gtg=all:tac=axiom_2964 on theBenchmark for (2964ds/784Mi) % 34.10/5.60 % (3888787)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=782893323:thitd=on:s2a=on:i=1131:add=on:canc=force:bd=all:rtra=on:tac=axiom:ev=off_2964 on theBenchmark for (2964ds/1131Mi) % 34.10/5.60 % (3888776)Instruction limit reached! % 34.10/5.60 % (3888776)------------------------------ % 34.10/5.60 % (3888776)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.10/5.60 % (3888776)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.10/5.60 % (3888776)CaDiCaL version: 2.1.3 % 34.10/5.60 % (3888776)Termination reason: Instruction limit % 34.10/5.60 % (3888776)Termination phase: Saturation % 34.10/5.60 % (3888776)Time elapsed: 0.486 s % 34.10/5.60 % (3888776)Peak memory usage: 98 MB % 34.10/5.60 % (3888776)Instructions burned: 837 (million) % 34.10/5.60 % (3888788)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=721753246:s2pl=no:i=246:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2963 on theBenchmark for (2963ds/246Mi) % 34.10/5.60 % (3888788)Refutation not found, incomplete strategy % 34.10/5.60 % (3888788)------------------------------ % 34.10/5.60 % (3888788)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.75/6.37 % (3888788)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.75/6.37 % (3888788)CaDiCaL version: 2.1.3 % 39.75/6.37 % (3888788)Termination reason: Refutation not found, incomplete strategy % 39.75/6.37 % (3888788)Time elapsed: 0.034 s % 39.75/6.37 % (3888788)Peak memory usage: 112 MB % 39.75/6.37 % (3888788)Instructions burned: 23 (million) % 39.75/6.37 % (3888783)Instruction limit reached! % 39.75/6.37 % (3888783)------------------------------ % 39.75/6.37 % (3888783)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.75/6.37 % (3888783)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.75/6.37 % (3888783)CaDiCaL version: 2.1.3 % 39.75/6.37 % (3888783)Termination reason: Instruction limit % 39.75/6.37 % (3888783)Termination phase: Saturation % 39.75/6.37 % (3888783)Time elapsed: 0.390 s % 39.75/6.37 % (3888783)Peak memory usage: 140 MB % 39.75/6.37 % (3888783)Instructions burned: 647 (million) % 39.75/6.37 % (3888793)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=247691735:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2962 on theBenchmark for (2962ds/775Mi) % 39.75/6.37 % (3888793)Refutation not found, incomplete strategy % 39.75/6.37 % (3888793)------------------------------ % 39.75/6.37 % (3888793)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.75/6.37 % (3888793)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.75/6.37 % (3888793)CaDiCaL version: 2.1.3 % 39.75/6.37 % (3888793)Termination reason: Refutation not found, incomplete strategy % 39.75/6.37 % (3888793)Time elapsed: 0.009 s % 39.75/6.37 % (3888793)Peak memory usage: 88 MB % 39.75/6.37 % (3888793)Instructions burned: 19 (million) % 39.75/6.37 % (3888795)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=521665028:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2961 on theBenchmark for (2961ds/273Mi) % 39.75/6.37 % (3888788)------------------------------ % 39.75/6.37 % (3888788)------------------------------ % 39.75/6.37 % (3888787)Instruction limit reached! % 39.75/6.37 % (3888787)------------------------------ % 39.75/6.37 % (3888787)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.75/6.37 % (3888787)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.75/6.37 % (3888787)CaDiCaL version: 2.1.3 % 39.75/6.37 % (3888787)Termination reason: Instruction limit % 39.75/6.37 % (3888787)Termination phase: Saturation % 39.75/6.37 % (3888787)Time elapsed: 0.366 s % 39.75/6.37 % (3888787)Peak memory usage: 122 MB % 39.75/6.37 % (3888787)Instructions burned: 1132 (million) % 39.75/6.37 % (3888786)Instruction limit reached! % 39.75/6.37 % (3888786)------------------------------ % 39.75/6.37 % (3888786)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.75/6.37 % (3888786)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.75/6.37 % (3888786)CaDiCaL version: 2.1.3 % 39.75/6.37 % (3888786)Termination reason: Instruction limit % 39.75/6.37 % (3888786)Termination phase: Saturation % 39.75/6.37 % (3888786)Time elapsed: 0.442 s % 39.75/6.37 % (3888786)Peak memory usage: 121 MB % 39.75/6.37 % (3888786)Instructions burned: 784 (million) % 39.75/6.37 % (3888798)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=3072931664:i=102:nm=16:rtra=on_2959 on theBenchmark for (2959ds/102Mi) % 39.75/6.37 % (3888793)------------------------------ % 39.75/6.37 % (3888793)------------------------------ % 39.75/6.37 % (3888798)Instruction limit reached! % 39.75/6.37 % (3888798)------------------------------ % 39.75/6.37 % (3888798)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.75/6.37 % (3888798)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.75/6.37 % (3888798)CaDiCaL version: 2.1.3 % 39.75/6.37 % (3888798)Termination reason: Instruction limit % 39.75/6.37 % (3888798)Termination phase: Saturation % 39.75/6.37 % (3888798)Time elapsed: 0.026 s % 39.75/6.37 % (3888798)Peak memory usage: 90 MB % 39.75/6.37 % (3888798)Instructions burned: 102 (million) % 39.75/6.37 % (3888770)Instruction limit reached! % 39.75/6.37 % (3888770)------------------------------ % 39.75/6.37 % (3888770)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.75/6.37 % (3888770)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.75/6.37 % (3888770)CaDiCaL version: 2.1.3 % 39.75/6.37 % (3888770)Termination reason: Instruction limit % 39.75/6.37 % (3888770)Termination phase: Clausification % 39.75/6.37 % (3888770)Time elapsed: 1.171 s % 53.97/8.31 % (3888770)Peak memory usage: 740 MB % 53.97/8.31 % (3888770)Instructions burned: 1090 (million) % 53.97/8.31 % (3888799)lrs+10_1_to=lpo:sil=128000:si=on:bsr=unit_only:tha=off:random_seed=651816237:avsq=on:s2a=on:i=1094:s2at=5:avsqr=4463,131072:rtra=on_2959 on theBenchmark for (2959ds/1094Mi) % 53.97/8.31 % (3888795)Instruction limit reached! % 53.97/8.31 % (3888795)------------------------------ % 53.97/8.31 % (3888795)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 53.97/8.31 % (3888795)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.97/8.31 % (3888795)CaDiCaL version: 2.1.3 % 53.97/8.31 % (3888795)Termination reason: Instruction limit % 53.97/8.31 % (3888795)Termination phase: Saturation % 53.97/8.31 % (3888795)Time elapsed: 0.163 s % 53.97/8.31 % (3888795)Peak memory usage: 95 MB % 53.97/8.31 % (3888795)Instructions burned: 273 (million) % 53.97/8.31 % (3888800)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=2801194650:i=6400:doe=on:fsr=off:rtra=on_2959 on theBenchmark for (2959ds/6400Mi) % 53.97/8.31 % (3888803)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=595178140:i=1846:canc=cautious:fsr=off:rtra=on_2958 on theBenchmark for (2958ds/1846Mi) % 53.97/8.31 % (3888803)Refutation not found, incomplete strategy % 53.97/8.31 % (3888803)------------------------------ % 53.97/8.31 % (3888803)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 53.97/8.31 % (3888803)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.97/8.31 % (3888803)CaDiCaL version: 2.1.3 % 53.97/8.31 % (3888803)Termination reason: Refutation not found, incomplete strategy % 53.97/8.31 % (3888803)Time elapsed: 0.026 s % 53.97/8.31 % (3888803)Peak memory usage: 91 MB % 53.97/8.31 % (3888803)Instructions burned: 96 (million) % 53.97/8.31 % (3888802)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=2193610745:i=868:doe=on:nm=0:rtra=on:gtg=exists_sym_2958 on theBenchmark for (2958ds/868Mi) % 53.97/8.31 % (3888805)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=3815512513:s2a=on:i=36816:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2958 on theBenchmark for (2958ds/36816Mi) % 53.97/8.31 % (3888808)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=386297195:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2957 on theBenchmark for (2957ds/273Mi) % 53.97/8.31 % (3888803)------------------------------ % 53.97/8.31 % (3888803)------------------------------ % 53.97/8.31 % (3888812)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=1437727688:i=863:doe=on:nm=0:rtra=on:gtg=exists_sym_2955 on theBenchmark for (2955ds/863Mi) % 53.97/8.31 % (3888808)Instruction limit reached! % 53.97/8.31 % (3888808)------------------------------ % 53.97/8.31 % (3888808)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 53.97/8.31 % (3888808)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.97/8.31 % (3888808)CaDiCaL version: 2.1.3 % 53.97/8.31 % (3888808)Termination reason: Instruction limit % 53.97/8.31 % (3888808)Termination phase: Saturation % 53.97/8.31 % (3888808)Time elapsed: 0.160 s % 53.97/8.31 % (3888808)Peak memory usage: 95 MB % 53.97/8.31 % (3888808)Instructions burned: 273 (million) % 53.97/8.31 % (3888814)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=679119914:i=5811:kws=precedence:nm=0:rtra=on_2954 on theBenchmark for (2954ds/5811Mi) % 53.97/8.31 % (3888799)Instruction limit reached! % 53.97/8.31 % (3888799)------------------------------ % 53.97/8.31 % (3888799)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 53.97/8.31 % (3888799)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.97/8.31 % (3888799)CaDiCaL version: 2.1.3 % 53.97/8.31 % (3888799)Termination reason: Instruction limit % 53.97/8.31 % (3888799)Termination phase: Saturation % 53.97/8.31 % (3888799)Time elapsed: 0.608 s % 53.97/8.31 % (3888799)Peak memory usage: 102 MB % 53.97/8.31 % (3888799)Instructions burned: 1095 (million) % 53.97/8.31 % (3888816)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=3333351349:i=2216:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2952 on theBenchmark for (2952ds/2216Mi) % 56.58/8.86 % (3888812)Instruction limit reached! % 56.58/8.86 % (3888812)------------------------------ % 56.58/8.86 % (3888812)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 56.58/8.86 % (3888812)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.58/8.86 % (3888812)CaDiCaL version: 2.1.3 % 56.58/8.86 % (3888812)Termination reason: Instruction limit % 56.58/8.86 % (3888812)Termination phase: Clausification % 56.58/8.86 % (3888812)Time elapsed: 0.509 s % 56.58/8.86 % (3888812)Peak memory usage: 556 MB % 56.58/8.86 % (3888812)Instructions burned: 864 (million) % 56.58/8.86 % (3888802)Instruction limit reached! % 56.58/8.86 % (3888802)------------------------------ % 56.58/8.86 % (3888802)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 56.58/8.86 % (3888802)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.58/8.86 % (3888802)CaDiCaL version: 2.1.3 % 56.58/8.86 % (3888802)Termination reason: Instruction limit % 56.58/8.86 % (3888802)Termination phase: Clausification % 56.58/8.86 % (3888802)Time elapsed: 0.827 s % 56.58/8.86 % (3888802)Peak memory usage: 510 MB % 56.58/8.86 % (3888802)Instructions burned: 868 (million) % 56.58/8.86 % (3888818)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=1415263328:i=801:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2949 on theBenchmark for (2949ds/801Mi) % 56.58/8.86 % (3888755)Instruction limit reached! % 56.58/8.86 % (3888755)------------------------------ % 56.58/8.86 % (3888755)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 56.58/8.86 % (3888755)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.58/8.86 % (3888755)CaDiCaL version: 2.1.3 % 56.58/8.86 % (3888755)Termination reason: Instruction limit % 56.58/8.86 % (3888755)Termination phase: Saturation % 56.58/8.86 % (3888755)Time elapsed: 2.475 s % 56.58/8.86 % (3888755)Peak memory usage: 117 MB % 56.58/8.86 % (3888755)Instructions burned: 4430 (million) % 56.58/8.86 % (3888820)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=1981600850:st=5:i=1026:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2948 on theBenchmark for (2948ds/1026Mi) % 56.58/8.86 % (3888820)Refutation not found, incomplete strategy % 56.58/8.86 % (3888820)------------------------------ % 56.58/8.86 % (3888820)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 56.58/8.86 % (3888820)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.58/8.86 % (3888820)CaDiCaL version: 2.1.3 % 56.58/8.86 % (3888820)Termination reason: Refutation not found, incomplete strategy % 56.58/8.86 % (3888820)Time elapsed: 0.006 s % 56.58/8.86 % (3888820)Peak memory usage: 88 MB % 56.58/8.86 % (3888820)Instructions burned: 11 (million) % 56.58/8.86 % (3888821)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=4204088798:i=3509:rtra=on_2948 on theBenchmark for (2948ds/3509Mi) % 56.58/8.86 % (3888818)Instruction limit reached! % 56.58/8.86 % (3888818)------------------------------ % 56.58/8.86 % (3888818)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 56.58/8.86 % (3888818)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.58/8.86 % (3888818)CaDiCaL version: 2.1.3 % 56.58/8.86 % (3888818)Termination reason: Instruction limit % 56.58/8.86 % (3888818)Termination phase: Saturation % 56.58/8.86 % (3888818)Time elapsed: 0.246 s % 56.58/8.86 % (3888818)Peak memory usage: 97 MB % 56.58/8.86 % (3888818)Instructions burned: 802 (million) % 56.58/8.86 % (3888824)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=1453144160:st=2:i=2127:sd=12:ep=R:rtra=on:ss=axioms_2946 on theBenchmark for (2946ds/2127Mi) % 56.58/8.86 % (3888824)Refutation not found, incomplete strategy % 56.58/8.86 % (3888824)------------------------------ % 56.58/8.86 % (3888824)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 56.58/8.86 % (3888824)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.58/8.86 % (3888824)CaDiCaL version: 2.1.3 % 56.58/8.86 % (3888824)Termination reason: Refutation not found, incomplete strategy % 56.58/8.86 % (3888824)Time elapsed: 0.004 s % 56.58/8.86 % (3888824)Peak memory usage: 88 MB % 56.58/8.86 % (3888824)Instructions burned: 17 (million) % 56.58/8.86 % (3888820)------------------------------ % 56.58/8.86 % (3888820)------------------------------ % 56.58/8.86 % (3888826)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=3857096454:i=1959:rtra=on:fsd=on:proc=on_2944 on theBenchmark for (2944ds/1959Mi) % 56.58/8.86 % (3888824)------------------------------ % 68.20/11.17 % (3888824)------------------------------ % 68.20/11.17 % (3888828)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=2015443068:s2a=on:i=3553:nm=0:rtra=on_2943 on theBenchmark for (2943ds/3553Mi) % 68.20/11.17 % (3888816)Instruction limit reached! % 68.20/11.17 % (3888816)------------------------------ % 68.20/11.17 % (3888816)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 68.20/11.17 % (3888816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 68.20/11.17 % (3888816)CaDiCaL version: 2.1.3 % 68.20/11.17 % (3888816)Termination reason: Instruction limit % 68.20/11.17 % (3888816)Termination phase: Saturation % 68.20/11.17 % (3888816)Time elapsed: 1.101 s % 68.20/11.17 % (3888816)Peak memory usage: 125 MB % 68.20/11.17 % (3888816)Instructions burned: 2217 (million) % 68.20/11.17 % (3888830)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=4052708358:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2939 on theBenchmark for (2939ds/3201Mi) % 68.20/11.17 % (3888826)Instruction limit reached! % 68.20/11.17 % (3888826)------------------------------ % 68.20/11.17 % (3888826)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 68.20/11.17 % (3888826)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 68.20/11.17 % (3888826)CaDiCaL version: 2.1.3 % 68.20/11.17 % (3888826)Termination reason: Instruction limit % 68.20/11.17 % (3888826)Termination phase: Saturation % 68.20/11.17 % (3888826)Time elapsed: 0.979 s % 68.20/11.17 % (3888826)Peak memory usage: 127 MB % 68.20/11.17 % (3888826)Instructions burned: 1959 (million) % 68.20/11.17 % (3888832)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=3779642943:thitd=on:cond=on:i=4093:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2933 on theBenchmark for (2933ds/4093Mi) % 68.20/11.17 % (3888828)Instruction limit reached! % 68.20/11.17 % (3888828)------------------------------ % 68.20/11.17 % (3888828)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 68.20/11.17 % (3888828)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 68.20/11.17 % (3888828)CaDiCaL version: 2.1.3 % 68.20/11.17 % (3888828)Termination reason: Instruction limit % 68.20/11.17 % (3888828)Termination phase: NewCNF % 68.20/11.17 % (3888828)Time elapsed: 1.118 s % 68.20/11.17 % (3888828)Peak memory usage: 518 MB % 68.20/11.17 % (3888828)Instructions burned: 3556 (million) % 68.20/11.17 % (3888834)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=2773708728:cond=fast:i=21173:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2930 on theBenchmark for (2930ds/21173Mi) % 68.20/11.17 % (3888834)Refutation not found, incomplete strategy % 68.20/11.17 % (3888834)------------------------------ % 68.20/11.17 % (3888834)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 68.20/11.17 % (3888834)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 68.20/11.17 % (3888834)CaDiCaL version: 2.1.3 % 68.20/11.17 % (3888834)Termination reason: Refutation not found, incomplete strategy % 68.20/11.17 % (3888834)Time elapsed: 0.018 s % 68.20/11.17 % (3888834)Peak memory usage: 113 MB % 68.20/11.17 % (3888834)Instructions burned: 14 (million) % 68.20/11.17 % (3888834)------------------------------ % 68.20/11.17 % (3888834)------------------------------ % 68.20/11.17 % (3888805)Refutation not found, incomplete strategy % 68.20/11.17 % (3888805)------------------------------ % 68.20/11.17 % (3888805)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 68.20/11.17 % (3888805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 68.20/11.17 % (3888805)CaDiCaL version: 2.1.3 % 68.20/11.17 % (3888805)Termination reason: Refutation not found, incomplete strategy % 68.20/11.17 % (3888805)Time elapsed: 2.946 s % 68.20/11.17 % (3888805)Peak memory usage: 125 MB % 68.20/11.17 % (3888805)Instructions burned: 7108 (million) % 68.20/11.17 % (3888836)lrs+11_1_to=lpo:thi=all:sas=z3:si=on:fd=off:sac=on:slsq=on:random_seed=4190075775:avsq=on:i=10544:avsqr=17,4:canc=force:rtra=on:gtg=exists_top:er=filter_2927 on theBenchmark for (2927ds/10544Mi) % 68.20/11.17 % (3888805)------------------------------ % 68.20/11.17 % (3888805)------------------------------ % 68.20/11.17 % (3888838)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=1105177385:avsq=on:i=1262:avsqr=1,16:rtra=on:rawr=on_2924 on theBenchmark for (2924ds/1262Mi) % 97.36/14.45 % (3888830)Instruction limit reached! % 97.36/14.45 % (3888830)------------------------------ % 97.36/14.45 % (3888830)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 97.36/14.45 % (3888830)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 97.36/14.45 % (3888830)CaDiCaL version: 2.1.3 % 97.36/14.45 % (3888830)Termination reason: Instruction limit % 97.36/14.45 % (3888830)Termination phase: Saturation % 97.36/14.45 % (3888830)Time elapsed: 1.493 s % 97.36/14.45 % (3888830)Peak memory usage: 98 MB % 97.36/14.45 % (3888830)Instructions burned: 3202 (million) % 97.36/14.45 % (3888821)Instruction limit reached! % 97.36/14.45 % (3888821)------------------------------ % 97.36/14.45 % (3888821)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 97.36/14.45 % (3888821)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 97.36/14.45 % (3888821)CaDiCaL version: 2.1.3 % 97.36/14.45 % (3888821)Termination reason: Instruction limit % 97.36/14.45 % (3888821)Termination phase: Saturation % 97.36/14.45 % (3888821)Time elapsed: 2.399 s % 97.36/14.45 % (3888821)Peak memory usage: 108 MB % 97.36/14.45 % (3888821)Instructions burned: 3510 (million) % 97.36/14.45 % (3888840)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=4239866311:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2923 on theBenchmark for (2923ds/775Mi) % 97.36/14.45 % (3888840)Refutation not found, incomplete strategy % 97.36/14.45 % (3888840)------------------------------ % 97.36/14.45 % (3888840)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 97.36/14.45 % (3888840)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 97.36/14.45 % (3888840)CaDiCaL version: 2.1.3 % 97.36/14.45 % (3888840)Termination reason: Refutation not found, incomplete strategy % 97.36/14.45 % (3888840)Time elapsed: 0.009 s % 97.36/14.45 % (3888840)Peak memory usage: 88 MB % 97.36/14.45 % (3888840)Instructions burned: 19 (million) % 97.36/14.45 % (3888800)Instruction limit reached! % 97.36/14.45 % (3888800)------------------------------ % 97.36/14.45 % (3888800)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 97.36/14.45 % (3888800)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 97.36/14.45 % (3888800)CaDiCaL version: 2.1.3 % 97.36/14.45 % (3888800)Termination reason: Instruction limit % 97.36/14.45 % (3888800)Termination phase: Saturation % 97.36/14.45 % (3888800)Time elapsed: 3.612 s % 97.36/14.45 % (3888800)Peak memory usage: 125 MB % 97.36/14.45 % (3888800)Instructions burned: 6400 (million) % 97.36/14.45 % (3888841)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=4109049536:i=270:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2922 on theBenchmark for (2922ds/270Mi) % 97.36/14.45 % (3888843)ott+10_128_isp=bottom:to=lpo:sil=128000:si=on:urr=on:uwa=alasca_main:sac=on:slsq=on:random_seed=316997360:i=17165:aac=none:doe=on:rtra=on:gtg=exists_all_2921 on theBenchmark for (2921ds/17165Mi) % 97.36/14.45 % (3888841)Instruction limit reached! % 97.36/14.45 % (3888841)------------------------------ % 97.36/14.45 % (3888841)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 97.36/14.45 % (3888841)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 97.36/14.45 % (3888841)CaDiCaL version: 2.1.3 % 97.36/14.45 % (3888841)Termination reason: Instruction limit % 97.36/14.45 % (3888841)Termination phase: Saturation % 97.36/14.45 % (3888841)Time elapsed: 0.155 s % 97.36/14.45 % (3888841)Peak memory usage: 95 MB % 97.36/14.45 % (3888841)Instructions burned: 271 (million) % 97.36/14.45 % (3888840)------------------------------ % 97.36/14.45 % (3888840)------------------------------ % 97.36/14.45 % (3888846)lrs+2_10_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_main:tha=some:random_seed=58031014:s2a=on:i=13094:s2at=-1:rtra=on_2919 on theBenchmark for (2919ds/13094Mi) % 97.36/14.45 % (3888847)lrs+10_1_to=lpo:sil=128000:si=on:sp=occurrence:random_seed=3719522331:st=2:i=12633:rtra=on:ss=axioms_2919 on theBenchmark for (2919ds/12633Mi) % 97.36/14.45 % (3888847)Refutation not found, incomplete strategy % 97.36/14.45 % (3888847)------------------------------ % 97.36/14.45 % (3888847)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 97.36/14.45 % (3888847)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 97.36/14.45 % (3888847)CaDiCaL version: 2.1.3 % 97.36/14.45 % (3888847)Termination reason: Refutation not found, incomplete strategy % 97.36/14.45 % (3888847)Time elapsed: 0.007 s % 98.86/15.67 % (3888847)Peak memory usage: 88 MB % 98.86/15.67 % (3888847)Instructions burned: 16 (million) % 98.86/15.67 % (3888838)Instruction limit reached! % 98.86/15.67 % (3888838)------------------------------ % 98.86/15.67 % (3888838)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 98.86/15.67 % (3888838)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 98.86/15.67 % (3888838)CaDiCaL version: 2.1.3 % 98.86/15.67 % (3888838)Termination reason: Instruction limit % 98.86/15.67 % (3888838)Termination phase: Saturation % 98.86/15.67 % (3888838)Time elapsed: 0.660 s % 98.86/15.67 % (3888838)Peak memory usage: 124 MB % 98.86/15.67 % (3888838)Instructions burned: 1264 (million) % 98.86/15.67 % (3888847)------------------------------ % 98.86/15.67 % (3888847)------------------------------ % 98.86/15.67 % (3888850)dis+1011_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_frequency:lsd=20:nwc=3:random_seed=3977325250:i=1783:rtra=on:gtg=position_2917 on theBenchmark for (2917ds/1783Mi) % 98.86/15.67 % (3888851)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=299543928:i=5451:aac=none:doe=on:nm=0:rtra=on:amm=off:gtg=position_2915 on theBenchmark for (2915ds/5451Mi) % 98.86/15.67 % (3888832)Instruction limit reached! % 98.86/15.67 % (3888832)------------------------------ % 98.86/15.67 % (3888832)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 98.86/15.67 % (3888832)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 98.86/15.67 % (3888832)CaDiCaL version: 2.1.3 % 98.86/15.67 % (3888832)Termination reason: Instruction limit % 98.86/15.67 % (3888832)Termination phase: Saturation % 98.86/15.67 % (3888832)Time elapsed: 2.018 s % 98.86/15.67 % (3888832)Peak memory usage: 144 MB % 98.86/15.67 % (3888832)Instructions burned: 4096 (million) % 98.86/15.67 % (3888854)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=743041921:i=4975:doe=on:nm=0:rtra=on:gtg=exists_sym_2911 on theBenchmark for (2911ds/4975Mi) % 98.86/15.67 % (3888850)Instruction limit reached! % 98.86/15.67 % (3888850)------------------------------ % 98.86/15.67 % (3888850)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 98.86/15.67 % (3888850)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 98.86/15.67 % (3888850)CaDiCaL version: 2.1.3 % 98.86/15.67 % (3888850)Termination reason: Instruction limit % 98.86/15.67 % (3888850)Termination phase: Saturation % 98.86/15.67 % (3888850)Time elapsed: 0.880 s % 98.86/15.67 % (3888850)Peak memory usage: 125 MB % 98.86/15.67 % (3888850)Instructions burned: 1788 (million) % 98.86/15.67 % (3888856)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=2310126210:i=2076:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2906 on theBenchmark for (2906ds/2076Mi) % 98.86/15.67 % (3888836)Instruction limit reached! % 98.86/15.67 % (3888836)------------------------------ % 98.86/15.67 % (3888836)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 98.86/15.67 % (3888836)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 98.86/15.67 % (3888836)CaDiCaL version: 2.1.3 % 98.86/15.67 % (3888836)Termination reason: Instruction limit % 98.86/15.67 % (3888836)Termination phase: Saturation % 98.86/15.67 % (3888836)Time elapsed: 2.790 s % 98.86/15.67 % (3888836)Peak memory usage: 150 MB % 98.86/15.67 % (3888836)Instructions burned: 10545 (million) % 98.86/15.67 % (3888858)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=3668780549:i=5145:rtra=on_2898 on theBenchmark for (2898ds/5145Mi) % 98.86/15.67 % (3888814)Instruction limit reached! % 98.86/15.67 % (3888814)------------------------------ % 98.86/15.67 % (3888814)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 98.86/15.67 % (3888814)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 98.86/15.67 % (3888814)CaDiCaL version: 2.1.3 % 98.86/15.67 % (3888814)Termination reason: Instruction limit % 98.86/15.67 % (3888814)Termination phase: Clausification % 98.86/15.67 % (3888814)Time elapsed: 5.625 s % 98.86/15.67 % (3888814)Peak memory usage: 3026 MB % 98.86/15.67 % (3888814)Instructions burned: 5811 (million) % 98.86/15.67 % (3888856)Instruction limit reached! % 98.86/15.67 % (3888856)------------------------------ % 98.86/15.67 % (3888856)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 98.86/15.67 % (3888856)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 163.39/23.77 % (3888856)CaDiCaL version: 2.1.3 % 163.39/23.77 % (3888856)Termination reason: Instruction limit % 163.39/23.77 % (3888856)Termination phase: Saturation % 163.39/23.77 % (3888856)Time elapsed: 1.027 s % 163.39/23.77 % (3888856)Peak memory usage: 126 MB % 163.39/23.77 % (3888856)Instructions burned: 2077 (million) % 163.39/23.77 % (3888860)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=3812307987:i=3509:rtra=on_2895 on theBenchmark for (2895ds/3509Mi) % 163.39/23.77 % (3888862)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=3688491122:st=2:i=13800:sd=12:ep=R:rtra=on:ss=axioms_2893 on theBenchmark for (2893ds/13800Mi) % 163.39/23.77 % (3888862)Refutation not found, incomplete strategy % 163.39/23.77 % (3888862)------------------------------ % 163.39/23.77 % (3888862)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 163.39/23.77 % (3888862)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 163.39/23.77 % (3888862)CaDiCaL version: 2.1.3 % 163.39/23.77 % (3888862)Termination reason: Refutation not found, incomplete strategy % 163.39/23.77 % (3888862)Time elapsed: 0.008 s % 163.39/23.77 % (3888862)Peak memory usage: 88 MB % 163.39/23.77 % (3888862)Instructions burned: 17 (million) % 163.39/23.77 % (3888862)------------------------------ % 163.39/23.77 % (3888862)------------------------------ % 163.39/23.77 % (3888864)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=1677264751:i=1412:rtra=on:fsd=on:proc=on_2889 on theBenchmark for (2889ds/1412Mi) % 163.39/23.77 % (3888858)Instruction limit reached! % 163.39/23.77 % (3888858)------------------------------ % 163.39/23.77 % (3888858)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 163.39/23.77 % (3888858)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 163.39/23.77 % (3888858)CaDiCaL version: 2.1.3 % 163.39/23.77 % (3888858)Termination reason: Instruction limit % 163.39/23.77 % (3888858)Termination phase: Saturation % 163.39/23.77 % (3888858)Time elapsed: 1.541 s % 163.39/23.77 % (3888858)Peak memory usage: 106 MB % 163.39/23.77 % (3888858)Instructions burned: 5145 (million) % 163.39/23.77 % (3888866)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 % 163.39/23.77 % (3888866)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=2129170184:i=11747:aac=none:nm=0:rtra=on:rawr=on_2881 on theBenchmark for (2881ds/11747Mi) % 163.39/23.77 % (3888864)Instruction limit reached! % 163.39/23.77 % (3888864)------------------------------ % 163.39/23.77 % (3888864)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 163.39/23.77 % (3888864)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 163.39/23.77 % (3888864)CaDiCaL version: 2.1.3 % 163.39/23.77 % (3888864)Termination reason: Instruction limit % 163.39/23.77 % (3888864)Termination phase: Saturation % 163.39/23.77 % (3888864)Time elapsed: 0.732 s % 163.39/23.77 % (3888864)Peak memory usage: 127 MB % 163.39/23.77 % (3888864)Instructions burned: 1412 (million) % 163.39/23.77 % (3888868)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=1068445097:s2a=on:i=3553:nm=0:rtra=on_2880 on theBenchmark for (2880ds/3553Mi) % 163.39/23.77 % (3888860)Instruction limit reached! % 163.39/23.77 % (3888860)------------------------------ % 163.39/23.77 % (3888860)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 163.39/23.77 % (3888860)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 163.39/23.77 % (3888860)CaDiCaL version: 2.1.3 % 163.39/23.77 % (3888860)Termination reason: Instruction limit % 163.39/23.77 % (3888860)Termination phase: Saturation % 163.39/23.77 % (3888860)Time elapsed: 1.768 s % 163.39/23.77 % (3888860)Peak memory usage: 141 MB % 163.39/23.77 % (3888860)Instructions burned: 3510 (million) % 163.39/23.77 % (3888870)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=100675554:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2875 on theBenchmark for (2875ds/3201Mi) % 163.39/23.77 % (3888854)Instruction limit reached! % 163.39/23.77 % (3888854)------------------------------ % 163.39/23.77 % (3888854)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 163.39/23.77 % (3888854)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 163.39/23.77 % (3888854)CaDiCaL version: 2.1.3 % 163.39/23.77 % (3888854)Termination reason: Instruction limit % 163.39/23.77 % (3888854)Termination phase: Clausification % 218.42/31.55 % (3888854)Time elapsed: 4.819 s % 218.42/31.55 % (3888854)Peak memory usage: 2592 MB % 218.42/31.55 % (3888854)Instructions burned: 4975 (million) % 218.42/31.55 % (3888870)Instruction limit reached! % 218.42/31.55 % (3888870)------------------------------ % 218.42/31.55 % (3888870)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 218.42/31.55 % (3888870)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 218.42/31.55 % (3888870)CaDiCaL version: 2.1.3 % 218.42/31.55 % (3888870)Termination reason: Instruction limit % 218.42/31.55 % (3888870)Termination phase: Saturation % 218.42/31.55 % (3888870)Time elapsed: 1.494 s % 218.42/31.55 % (3888870)Peak memory usage: 98 MB % 218.42/31.55 % (3888870)Instructions burned: 3202 (million) % 218.42/31.55 % (3889068)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=678236462:thitd=on:cond=on:i=4081:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2859 on theBenchmark for (2859ds/4081Mi) % 218.42/31.55 % (3888868)Instruction limit reached! % 218.42/31.55 % (3888868)------------------------------ % 218.42/31.55 % (3888868)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 218.42/31.55 % (3888868)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 218.42/31.55 % (3888868)CaDiCaL version: 2.1.3 % 218.42/31.55 % (3888868)Termination reason: Instruction limit % 218.42/31.55 % (3888868)Termination phase: NewCNF % 218.42/31.55 % (3888868)Time elapsed: 2.177 s % 218.42/31.55 % (3888868)Peak memory usage: 425 MB % 218.42/31.55 % (3888868)Instructions burned: 3554 (million) % 218.42/31.55 % (3889086)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=988401877:cond=fast:i=20260:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2858 on theBenchmark for (2858ds/20260Mi) % 218.42/31.55 % (3889086)Refutation not found, incomplete strategy % 218.42/31.55 % (3889086)------------------------------ % 218.42/31.55 % (3889086)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 218.42/31.55 % (3889086)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 218.42/31.55 % (3889086)CaDiCaL version: 2.1.3 % 218.42/31.55 % (3889086)Termination reason: Refutation not found, incomplete strategy % 218.42/31.55 % (3889086)Time elapsed: 0.030 s % 218.42/31.55 % (3889086)Peak memory usage: 113 MB % 218.42/31.55 % (3889086)Instructions burned: 14 (million) % 218.42/31.55 % (3889122)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=3492124067:s2a=on:i=58627:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2857 on theBenchmark for (2857ds/58627Mi) % 218.42/31.55 % (3889086)------------------------------ % 218.42/31.55 % (3889086)------------------------------ % 218.42/31.55 % (3888851)Instruction limit reached! % 218.42/31.55 % (3888851)------------------------------ % 218.42/31.55 % (3888851)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 218.42/31.55 % (3888851)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 218.42/31.55 % (3888851)CaDiCaL version: 2.1.3 % 218.42/31.55 % (3888851)Termination reason: Instruction limit % 218.42/31.55 % (3888851)Termination phase: Clausification % 218.42/31.55 % (3888851)Time elapsed: 5.947 s % 218.42/31.55 % (3888851)Peak memory usage: 3368 MB % 218.42/31.55 % (3888851)Instructions burned: 5451 (million) % 218.42/31.55 % (3889124)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=2843586516:avsq=on:i=6258:avsqr=1,16:rtra=on:rawr=on_2855 on theBenchmark for (2855ds/6258Mi) % 218.42/31.55 % (3888846)Instruction limit reached! % 218.42/31.55 % (3888846)------------------------------ % 218.42/31.55 % (3888846)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 218.42/31.55 % (3888846)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 218.42/31.55 % (3888846)CaDiCaL version: 2.1.3 % 218.42/31.55 % (3888846)Termination reason: Instruction limit % 218.42/31.55 % (3888846)Termination phase: Saturation % 218.42/31.55 % (3888846)Time elapsed: 6.825 s % 218.42/31.55 % (3888846)Peak memory usage: 113 MB % 218.42/31.55 % (3888846)Instructions burned: 13094 (million) % 218.42/31.55 % (3888843)Instruction limit reached! % 218.42/31.55 % (3888843)------------------------------ % 218.42/31.55 % (3888843)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 218.42/31.55 % (3888843)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 218.42/31.55 % (3888843)CaDiCaL version: 2.1.3 % 218.42/31.55 % (3888843)Termination reason: Instruction limit % 218.42/31.55 % (3888843)Termination phase: Saturation % 251.84/36.17 % (3888843)Time elapsed: 7.019 s % 251.84/36.17 % (3888843)Peak memory usage: 141 MB % 251.84/36.17 % (3888843)Instructions burned: 17167 (million) % 251.84/36.17 % (3889135)lrs+2_10_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_main:tha=some:random_seed=3015331403:s2a=on:i=71622:s2at=-1:rtra=on_2850 on theBenchmark for (2850ds/71622Mi) % 251.84/36.17 % (3889134)ott+10_128_isp=bottom:to=lpo:sil=128000:si=on:urr=on:uwa=alasca_main:sac=on:slsq=on:random_seed=923910731:i=34001:aac=none:doe=on:rtra=on:gtg=exists_all_2850 on theBenchmark for (2850ds/34001Mi) % 251.84/36.17 % (3889138)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=3690188312:i=24001:kws=precedence:nm=0:rtra=on_2849 on theBenchmark for (2849ds/24001Mi) % 251.84/36.17 % (3889124)Instruction limit reached! % 251.84/36.17 % (3889124)------------------------------ % 251.84/36.17 % (3889124)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 251.84/36.17 % (3889124)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 251.84/36.17 % (3889124)CaDiCaL version: 2.1.3 % 251.84/36.18 % (3889124)Termination reason: Instruction limit % 251.84/36.18 % (3889124)Termination phase: Saturation % 251.84/36.18 % (3889124)Time elapsed: 2.454 s % 251.84/36.18 % (3889124)Peak memory usage: 128 MB % 251.84/36.18 % (3889124)Instructions burned: 6261 (million) % 251.84/36.18 % (3889068)Instruction limit reached! % 251.84/36.18 % (3889068)------------------------------ % 251.84/36.18 % (3889068)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 251.84/36.18 % (3889068)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 251.84/36.18 % (3889068)CaDiCaL version: 2.1.3 % 251.84/36.18 % (3889068)Termination reason: Instruction limit % 251.84/36.18 % (3889068)Termination phase: Saturation % 251.84/36.18 % (3889068)Time elapsed: 2.922 s % 251.84/36.18 % (3889068)Peak memory usage: 145 MB % 251.84/36.18 % (3889068)Instructions burned: 4081 (million) % 251.84/36.18 % (3889230)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=3623916123:i=2076:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2829 on theBenchmark for (2829ds/2076Mi) % 251.84/36.18 % (3889235)dis+21_20_to=lakbo:si=on:alasca=on:sp=const_max:uwa=alasca_main:sac=on:random_seed=4134480938:s2a=on:i=83971:s2at=4:bd=all:ins=1:rtra=on_2828 on theBenchmark for (2828ds/83971Mi) % 251.84/36.18 % (3889230)Instruction limit reached! % 251.84/36.18 % (3889230)------------------------------ % 251.84/36.18 % (3889230)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 251.84/36.18 % (3889230)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 251.84/36.18 % (3889230)CaDiCaL version: 2.1.3 % 251.84/36.18 % (3889230)Termination reason: Instruction limit % 251.84/36.18 % (3889230)Termination phase: Saturation % 251.84/36.18 % (3889230)Time elapsed: 1.020 s % 251.84/36.18 % (3889230)Peak memory usage: 125 MB % 251.84/36.18 % (3889230)Instructions burned: 2080 (million) % 251.84/36.18 % (3889265)lrs+1011_5:1_to=lpo:sil=128000:sas=z3:si=on:norm_ineq=on:tha=some:random_seed=3030642765:i=83944:rtra=on_2817 on theBenchmark for (2817ds/83944Mi) % 251.84/36.18 % (3889235)Refutation not found, incomplete strategy % 251.84/36.18 % (3889235)------------------------------ % 251.84/36.18 % (3889235)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 251.84/36.18 % (3889235)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 251.84/36.18 % (3889235)CaDiCaL version: 2.1.3 % 251.84/36.18 % (3889235)Termination reason: Refutation not found, incomplete strategy % 251.84/36.18 % (3889235)Time elapsed: 3.163 s % 251.84/36.18 % (3889235)Peak memory usage: 99 MB % 251.84/36.18 % (3889235)Instructions burned: 3357 (million) % 251.84/36.18 % (3889235)------------------------------ % 251.84/36.18 % (3889235)------------------------------ % 251.84/36.18 % (3889320)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=1808857018:i=9201:rtra=on_2790 on theBenchmark for (2790ds/9201Mi) % 251.84/36.18 % (3889265)Refutation not found, incomplete strategy % 251.84/36.18 % (3889265)------------------------------ % 251.84/36.18 % (3889265)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 251.84/36.18 % (3889265)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 251.84/36.18 % (3889265)CaDiCaL version: 2.1.3 % 251.84/36.18 % (3889265)Termination reason: Refutation not found, incomplete strategy % 251.84/36.18 % (3889265)Time elapsed: 4.692 s % 251.84/36.18 % (3889265)Peak memory usage: 137 MB % 251.84/36.18 % (3889265)InstructionTerminated %------------------------------------------------------------------------------