%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWW844_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 : n009.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:37:56 PM UTC 2026 % Result : Timeout 286.53s 41.06s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : SWW844_1 : TPTP v9.3.1. Released v7.0.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.09/0.20 % Computer : n009.cluster.edu % 0.09/0.20 % Model : x86_64 x86_64 % 0.09/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.20 % Memory : 8046.5625MB % 0.09/0.20 % OS : Linux 6.8.0-71-generic % 0.09/0.20 % CPULimit : 300 % 0.09/0.20 % WCLimit : 300 % 0.09/0.20 % DateTime : Mon Sep 28 14:31:45 UTC 2026 % 0.09/0.20 % CPUTime : % 0.09/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.09/0.23 Running first-order theorem proving % 0.09/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.46/1.22 % (3071597)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule. % 3.46/1.22 % (3071608)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=220559463:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi) % 3.46/1.22 % (3071608)Instruction limit reached! % 3.46/1.22 % (3071608)------------------------------ % 3.46/1.22 % (3071608)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.46/1.22 % (3071608)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.46/1.22 % (3071608)CaDiCaL version: 2.1.3 % 3.46/1.22 % (3071608)Termination reason: Instruction limit % 3.46/1.22 % (3071608)Termination phase: Preprocessing 3 % 3.46/1.22 % (3071608)Time elapsed: 0.009 s % 3.46/1.22 % (3071608)Peak memory usage: 87 MB % 3.46/1.22 % (3071608)Instructions burned: 34 (million) % 3.46/1.22 % (3071602)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=3259254045:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi) % 3.46/1.22 % (3071605)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=1595102063:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi) % 3.46/1.22 % (3071604)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=1548220938:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi) % 3.46/1.22 % (3071603)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=3303514750:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi) % 3.46/1.22 % (3071606)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=1537838035:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi) % 3.46/1.22 % (3071607)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=2052252283:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi) % 3.46/1.22 % (3071606)Instruction limit reached! % 3.46/1.22 % (3071606)------------------------------ % 3.46/1.22 % (3071606)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.46/1.22 % (3071606)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.46/1.22 % (3071606)CaDiCaL version: 2.1.3 % 3.46/1.22 % (3071606)Termination reason: Instruction limit % 3.46/1.22 % (3071606)Termination phase: Property scanning % 3.46/1.22 % (3071606)Time elapsed: 0.003 s % 3.46/1.22 % (3071606)Peak memory usage: 85 MB % 3.46/1.22 % (3071606)Instructions burned: 4 (million) % 3.46/1.22 % (3071605)Instruction limit reached! % 3.46/1.22 % (3071605)------------------------------ % 3.46/1.22 % (3071605)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.46/1.22 % (3071605)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.46/1.22 % (3071605)CaDiCaL version: 2.1.3 % 3.46/1.22 % (3071605)Termination reason: Instruction limit % 3.46/1.22 % (3071605)Termination phase: Property scanning % 3.46/1.22 % (3071605)Time elapsed: 0.004 s % 3.46/1.22 % (3071605)Peak memory usage: 85 MB % 3.46/1.22 % (3071605)Instructions burned: 8 (million) % 3.46/1.22 % (3071602)Instruction limit reached! % 3.46/1.22 % (3071602)------------------------------ % 3.46/1.22 % (3071602)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.46/1.22 % (3071602)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.46/1.22 % (3071602)CaDiCaL version: 2.1.3 % 3.46/1.22 % (3071602)Termination reason: Instruction limit % 3.46/1.22 % (3071602)Termination phase: Property scanning % 3.46/1.22 % (3071602)Time elapsed: 0.006 s % 3.46/1.22 % (3071602)Peak memory usage: 85 MB % 3.46/1.22 % (3071602)Instructions burned: 14 (million) % 3.46/1.22 % (3071607)Instruction limit reached! % 3.46/1.22 % (3071607)------------------------------ % 3.46/1.22 % (3071607)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.46/1.22 % (3071607)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.46/1.22 % (3071607)CaDiCaL version: 2.1.3 % 3.46/1.22 % (3071607)Termination reason: Instruction limit % 3.46/1.22 % (3071607)Termination phase: Property scanning % 3.46/1.22 % (3071607)Time elapsed: 0.024 s % 3.46/1.22 % (3071607)Peak memory usage: 88 MB % 3.46/1.22 % (3071607)Instructions burned: 48 (million) % 3.46/1.22 % (3071610)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=719909708:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2998 on theBenchmark for (2998ds/14Mi) % 3.46/1.22 % (3071610)Instruction limit reached! % 3.46/1.22 % (3071610)------------------------------ % 3.92/1.37 % (3071610)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.92/1.37 % (3071610)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.92/1.37 % (3071610)CaDiCaL version: 2.1.3 % 3.92/1.37 % (3071610)Termination reason: Instruction limit % 3.92/1.37 % (3071610)Termination phase: SInE selection % 3.92/1.37 % (3071610)Time elapsed: 0.004 s % 3.92/1.37 % (3071610)Peak memory usage: 86 MB % 3.92/1.37 % (3071610)Instructions burned: 14 (million) % 3.92/1.37 % (3071604)Instruction limit reached! % 3.92/1.37 % (3071604)------------------------------ % 3.92/1.37 % (3071604)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.92/1.37 % (3071604)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.92/1.37 % (3071604)CaDiCaL version: 2.1.3 % 3.92/1.37 % (3071604)Termination reason: Instruction limit % 3.92/1.37 % (3071604)Termination phase: Saturation % 3.92/1.37 % (3071604)Time elapsed: 0.145 s % 3.92/1.37 % (3071604)Peak memory usage: 117 MB % 3.92/1.37 % (3071604)Instructions burned: 202 (million) % 3.92/1.37 % (3071617)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=1955230715:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2997 on theBenchmark for (2997ds/29Mi) % 3.92/1.37 % (3071619)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=3662063320:i=24:canc=force:rtra=on_2997 on theBenchmark for (2997ds/24Mi) % 3.92/1.37 % (3071618)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=3398123600:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2997 on theBenchmark for (2997ds/16Mi) % 3.92/1.37 % (3071618)Instruction limit reached! % 3.92/1.37 % (3071618)------------------------------ % 3.92/1.37 % (3071618)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.92/1.37 % (3071618)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.92/1.37 % (3071618)CaDiCaL version: 2.1.3 % 3.92/1.37 % (3071618)Termination reason: Instruction limit % 3.92/1.37 % (3071618)Termination phase: Preprocessing 3 % 3.92/1.37 % (3071618)Time elapsed: 0.009 s % 3.92/1.37 % (3071618)Peak memory usage: 86 MB % 3.92/1.37 % (3071618)Instructions burned: 17 (million) % 3.92/1.37 % (3071620)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=1660396285:i=27:canc=cautious:fsr=off:rtra=on_2997 on theBenchmark for (2997ds/27Mi) % 3.92/1.37 % (3071619)Instruction limit reached! % 3.92/1.37 % (3071619)------------------------------ % 3.92/1.37 % (3071619)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.92/1.37 % (3071619)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.92/1.37 % (3071619)CaDiCaL version: 2.1.3 % 3.92/1.37 % (3071619)Termination reason: Instruction limit % 3.92/1.37 % (3071619)Termination phase: shuffling % 3.92/1.37 % (3071619)Time elapsed: 0.012 s % 3.92/1.37 % (3071619)Peak memory usage: 86 MB % 3.92/1.37 % (3071619)Instructions burned: 25 (million) % 3.92/1.37 % (3071617)Instruction limit reached! % 3.92/1.37 % (3071617)------------------------------ % 3.92/1.37 % (3071617)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.92/1.37 % (3071617)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.92/1.37 % (3071617)CaDiCaL version: 2.1.3 % 3.92/1.37 % (3071617)Termination reason: Instruction limit % 3.92/1.37 % (3071617)Termination phase: Preprocessing 3 % 3.92/1.37 % (3071617)Time elapsed: 0.016 s % 3.92/1.37 % (3071617)Peak memory usage: 87 MB % 3.92/1.37 % (3071617)Instructions burned: 30 (million) % 3.92/1.37 % (3071620)Instruction limit reached! % 3.92/1.37 % (3071620)------------------------------ % 3.92/1.37 % (3071620)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.92/1.37 % (3071620)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.92/1.37 % (3071620)CaDiCaL version: 2.1.3 % 3.92/1.37 % (3071620)Termination reason: Instruction limit % 3.92/1.37 % (3071620)Termination phase: Preprocessing 3 % 3.92/1.37 % (3071620)Time elapsed: 0.007 s % 3.92/1.37 % (3071620)Peak memory usage: 87 MB % 3.92/1.37 % (3071620)Instructions burned: 28 (million) % 3.92/1.37 % (3071603)Instruction limit reached! % 3.92/1.37 % (3071603)------------------------------ % 3.92/1.37 % (3071603)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.92/1.37 % (3071603)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.57/1.55 % (3071603)CaDiCaL version: 2.1.3 % 5.57/1.55 % (3071603)Termination reason: Instruction limit % 5.57/1.55 % (3071603)Termination phase: Saturation % 5.57/1.55 % (3071603)Time elapsed: 0.187 s % 5.57/1.55 % (3071603)Peak memory usage: 119 MB % 5.57/1.55 % (3071603)Instructions burned: 307 (million) % 5.57/1.55 % (3071622)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=1817114887:i=85:gtgl=4:rtra=on:gtg=exists_sym_2997 on theBenchmark for (2997ds/85Mi) % 5.57/1.55 % (3071631)lrs+10_1_thi=all:si=on:fd=off:random_seed=3868194296:i=53:rtra=on:gtg=all_2996 on theBenchmark for (2996ds/53Mi) % 5.57/1.55 % (3071622)Instruction limit reached! % 5.57/1.55 % (3071622)------------------------------ % 5.57/1.55 % (3071622)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.57/1.55 % (3071622)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.57/1.55 % (3071622)CaDiCaL version: 2.1.3 % 5.57/1.55 % (3071622)Termination reason: Instruction limit % 5.57/1.55 % (3071622)Termination phase: Saturation % 5.57/1.55 % (3071622)Time elapsed: 0.042 s % 5.57/1.55 % (3071622)Peak memory usage: 88 MB % 5.57/1.55 % (3071622)Instructions burned: 86 (million) % 5.57/1.55 % (3071631)Instruction limit reached! % 5.57/1.55 % (3071631)------------------------------ % 5.57/1.55 % (3071631)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.57/1.55 % (3071631)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.57/1.55 % (3071631)CaDiCaL version: 2.1.3 % 5.57/1.55 % (3071631)Termination reason: Instruction limit % 5.57/1.55 % (3071631)Termination phase: Preprocessing 3 % 5.57/1.55 % (3071631)Time elapsed: 0.014 s % 5.57/1.55 % (3071631)Peak memory usage: 87 MB % 5.57/1.55 % (3071631)Instructions burned: 54 (million) % 5.57/1.55 % (3071626)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=2772653575:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2996 on theBenchmark for (2996ds/2Mi) % 5.57/1.55 % (3071626)Instruction limit reached! % 5.57/1.55 % (3071626)------------------------------ % 5.57/1.55 % (3071626)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.57/1.55 % (3071626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.57/1.55 % (3071626)CaDiCaL version: 2.1.3 % 5.57/1.55 % (3071626)Termination reason: Instruction limit % 5.57/1.55 % (3071626)Termination phase: shuffling % 5.57/1.55 % (3071626)Time elapsed: 0.002 s % 5.57/1.55 % (3071626)Peak memory usage: 85 MB % 5.57/1.55 % (3071626)Instructions burned: 2 (million) % 5.57/1.55 % (3071628)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=3300895558:i=181:rtra=on:ss=axioms:ev=cautious_2996 on theBenchmark for (2996ds/181Mi) % 5.57/1.55 % (3071629)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=3035399467:i=4:ep=RST:ins=2:rtra=on_2996 on theBenchmark for (2996ds/4Mi) % 5.57/1.55 % (3071629)Instruction limit reached! % 5.57/1.55 % (3071629)------------------------------ % 5.57/1.55 % (3071629)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.57/1.55 % (3071629)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.57/1.55 % (3071629)CaDiCaL version: 2.1.3 % 5.57/1.55 % (3071629)Termination reason: Instruction limit % 5.57/1.55 % (3071629)Termination phase: Property scanning % 5.57/1.55 % (3071629)Time elapsed: 0.003 s % 5.57/1.55 % (3071629)Peak memory usage: 85 MB % 5.57/1.55 % (3071629)Instructions burned: 4 (million) % 5.57/1.55 % (3071628)Refutation not found, incomplete strategy % 5.57/1.55 % (3071628)------------------------------ % 5.57/1.55 % (3071628)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.57/1.55 % (3071628)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.57/1.55 % (3071628)CaDiCaL version: 2.1.3 % 5.57/1.55 % (3071628)Termination reason: Refutation not found, incomplete strategy % 5.57/1.55 % (3071628)Time elapsed: 0.009 s % 5.57/1.55 % (3071628)Peak memory usage: 88 MB % 5.57/1.55 % (3071628)Instructions burned: 15 (million) % 5.57/1.55 % (3071630)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=741630177:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2996 on theBenchmark for (2996ds/66Mi) % 5.57/1.55 % (3071632)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=3330851816:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2996 on theBenchmark for (2996ds/8Mi) % 6.57/1.75 % (3071632)Instruction limit reached! % 6.57/1.75 % (3071632)------------------------------ % 6.57/1.75 % (3071632)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.57/1.75 % (3071632)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.57/1.75 % (3071632)CaDiCaL version: 2.1.3 % 6.57/1.75 % (3071632)Termination reason: Instruction limit % 6.57/1.75 % (3071632)Termination phase: Property scanning % 6.57/1.75 % (3071632)Time elapsed: 0.005 s % 6.57/1.75 % (3071632)Peak memory usage: 85 MB % 6.57/1.75 % (3071632)Instructions burned: 9 (million) % 6.57/1.75 % (3071630)Instruction limit reached! % 6.57/1.75 % (3071630)------------------------------ % 6.57/1.75 % (3071630)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.57/1.75 % (3071630)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.57/1.75 % (3071630)CaDiCaL version: 2.1.3 % 6.57/1.75 % (3071630)Termination reason: Instruction limit % 6.57/1.75 % (3071630)Termination phase: Saturation % 6.57/1.75 % (3071630)Time elapsed: 0.034 s % 6.57/1.75 % (3071630)Peak memory usage: 88 MB % 6.57/1.75 % (3071630)Instructions burned: 69 (million) % 6.57/1.75 % (3071636)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=3829703446:i=2:doe=on:canc=force:asg=cautious:rtra=on_2995 on theBenchmark for (2995ds/2Mi) % 6.57/1.75 % (3071636)Instruction limit reached! % 6.57/1.75 % (3071636)------------------------------ % 6.57/1.75 % (3071636)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.57/1.75 % (3071636)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.57/1.75 % (3071636)CaDiCaL version: 2.1.3 % 6.57/1.75 % (3071636)Termination reason: Instruction limit % 6.57/1.75 % (3071636)Termination phase: Property scanning % 6.57/1.75 % (3071636)Time elapsed: 0.002 s % 6.57/1.75 % (3071636)Peak memory usage: 86 MB % 6.57/1.75 % (3071636)Instructions burned: 6 (million) % 6.57/1.75 % (3071635)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=3196703994:st=3:i=2:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/2Mi) % 6.57/1.75 % (3071635)Instruction limit reached! % 6.57/1.75 % (3071635)------------------------------ % 6.57/1.75 % (3071635)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.57/1.75 % (3071635)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.57/1.75 % (3071635)CaDiCaL version: 2.1.3 % 6.57/1.75 % (3071635)Termination reason: Instruction limit % 6.57/1.75 % (3071635)Termination phase: shuffling % 6.57/1.75 % (3071635)Time elapsed: 0.002 s % 6.57/1.75 % (3071635)Peak memory usage: 85 MB % 6.57/1.75 % (3071635)Instructions burned: 2 (million) % 6.57/1.75 % (3071640)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=1670920528:i=127:doe=on:rtra=on_2995 on theBenchmark for (2995ds/127Mi) % 6.57/1.75 % (3071641)dis+10_1_si=on:random_seed=1379996189:i=10:ep=R:rtra=on_2994 on theBenchmark for (2994ds/10Mi) % 6.57/1.75 % (3071641)Instruction limit reached! % 6.57/1.75 % (3071641)------------------------------ % 6.57/1.75 % (3071641)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.57/1.75 % (3071641)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.57/1.75 % (3071641)CaDiCaL version: 2.1.3 % 6.57/1.75 % (3071641)Termination reason: Instruction limit % 6.57/1.75 % (3071641)Termination phase: Property scanning % 6.57/1.75 % (3071641)Time elapsed: 0.006 s % 6.57/1.75 % (3071641)Peak memory usage: 86 MB % 6.57/1.75 % (3071641)Instructions burned: 12 (million) % 6.57/1.75 % (3071647)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=1599217327:i=2:fsr=off:rtra=on:inst=on_2994 on theBenchmark for (2994ds/2Mi) % 6.57/1.75 % (3071647)Instruction limit reached! % 6.57/1.75 % (3071647)------------------------------ % 6.57/1.75 % (3071647)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.57/1.75 % (3071647)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.57/1.75 % (3071647)CaDiCaL version: 2.1.3 % 6.57/1.75 % (3071647)Termination reason: Instruction limit % 6.57/1.75 % (3071647)Termination phase: Property scanning % 6.57/1.75 % (3071647)Time elapsed: 0.002 s % 6.57/1.75 % (3071647)Peak memory usage: 86 MB % 6.57/1.75 % (3071647)Instructions burned: 6 (million) % 6.57/1.75 % (3071644)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=582883262:i=26:canc=cautious:av=off:rtra=on_2994 on theBenchmark for (2994ds/26Mi) % 6.57/1.75 % (3071645)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=2364580362: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.93/1.94 % (3071644)Instruction limit reached! % 7.93/1.94 % (3071644)------------------------------ % 7.93/1.94 % (3071644)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.93/1.94 % (3071644)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.93/1.94 % (3071644)CaDiCaL version: 2.1.3 % 7.93/1.94 % (3071644)Termination reason: Instruction limit % 7.93/1.94 % (3071644)Termination phase: Preprocessing 3 % 7.93/1.94 % (3071644)Time elapsed: 0.014 s % 7.93/1.94 % (3071644)Peak memory usage: 87 MB % 7.93/1.94 % (3071644)Instructions burned: 27 (million) % 7.93/1.94 % (3071645)Instruction limit reached! % 7.93/1.94 % (3071645)------------------------------ % 7.93/1.94 % (3071645)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.93/1.94 % (3071645)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.93/1.94 % (3071645)CaDiCaL version: 2.1.3 % 7.93/1.94 % (3071645)Termination reason: Instruction limit % 7.93/1.94 % (3071645)Termination phase: Preprocessing 3 % 7.93/1.94 % (3071645)Time elapsed: 0.019 s % 7.93/1.94 % (3071645)Peak memory usage: 87 MB % 7.93/1.94 % (3071645)Instructions burned: 36 (million) % 7.93/1.94 % (3071640)Instruction limit reached! % 7.93/1.94 % (3071640)------------------------------ % 7.93/1.94 % (3071640)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.93/1.94 % (3071640)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.93/1.94 % (3071640)CaDiCaL version: 2.1.3 % 7.93/1.94 % (3071640)Termination reason: Instruction limit % 7.93/1.94 % (3071640)Termination phase: Saturation % 7.93/1.94 % (3071640)Time elapsed: 0.096 s % 7.93/1.94 % (3071640)Peak memory usage: 118 MB % 7.93/1.94 % (3071640)Instructions burned: 128 (million) % 7.93/1.94 % (3071628)------------------------------ % 7.93/1.94 % (3071628)------------------------------ % 7.93/1.94 % (3071649)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=3595230347:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2993 on theBenchmark for (2993ds/8Mi) % 7.93/1.94 % (3071649)Instruction limit reached! % 7.93/1.94 % (3071649)------------------------------ % 7.93/1.94 % (3071649)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.93/1.94 % (3071649)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.93/1.94 % (3071649)CaDiCaL version: 2.1.3 % 7.93/1.94 % (3071649)Termination reason: Instruction limit % 7.93/1.94 % (3071649)Termination phase: Property scanning % 7.93/1.94 % (3071649)Time elapsed: 0.005 s % 7.93/1.94 % (3071649)Peak memory usage: 86 MB % 7.93/1.94 % (3071649)Instructions burned: 9 (million) % 7.93/1.94 % (3071652)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=407222936:i=370:ep=RS:fsr=off:rtra=on_2993 on theBenchmark for (2993ds/370Mi) % 7.93/1.94 % (3071656)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=1335636033:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2993 on theBenchmark for (2993ds/13Mi) % 7.93/1.94 % (3071656)Instruction limit reached! % 7.93/1.94 % (3071656)------------------------------ % 7.93/1.94 % (3071656)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.93/1.94 % (3071656)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.93/1.94 % (3071656)CaDiCaL version: 2.1.3 % 7.93/1.94 % (3071656)Termination reason: Instruction limit % 7.93/1.94 % (3071656)Termination phase: Property scanning % 7.93/1.94 % (3071656)Time elapsed: 0.004 s % 7.93/1.94 % (3071656)Peak memory usage: 85 MB % 7.93/1.94 % (3071656)Instructions burned: 18 (million) % 7.93/1.94 % (3071657)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=1309398226:i=226:rtra=on:gtg=position:ss=axioms_2992 on theBenchmark for (2992ds/226Mi) % 7.93/1.94 % (3071658)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=2396289425:i=10:rtra=on_2992 on theBenchmark for (2992ds/10Mi) % 7.93/1.94 % (3071658)Instruction limit reached! % 7.93/1.94 % (3071658)------------------------------ % 7.93/1.94 % (3071658)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.93/1.94 % (3071658)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.61/2.23 % (3071658)CaDiCaL version: 2.1.3 % 10.61/2.23 % (3071658)Termination reason: Instruction limit % 10.61/2.23 % (3071658)Termination phase: Preprocessing 1 % 10.61/2.23 % (3071658)Time elapsed: 0.006 s % 10.61/2.23 % (3071658)Peak memory usage: 86 MB % 10.61/2.23 % (3071658)Instructions burned: 12 (million) % 10.61/2.23 % (3071657)Refutation not found, incomplete strategy % 10.61/2.23 % (3071657)------------------------------ % 10.61/2.23 % (3071657)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.61/2.23 % (3071657)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.61/2.23 % (3071657)CaDiCaL version: 2.1.3 % 10.61/2.23 % (3071657)Termination reason: Refutation not found, incomplete strategy % 10.61/2.23 % (3071657)Time elapsed: 0.038 s % 10.61/2.23 % (3071657)Peak memory usage: 112 MB % 10.61/2.23 % (3071657)Instructions burned: 29 (million) % 10.61/2.23 % (3071659)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=3870236003:i=71:rtra=on:gtg=exists_top_2992 on theBenchmark for (2992ds/71Mi) % 10.61/2.23 % (3071661)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=2380725905:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2992 on theBenchmark for (2992ds/75Mi) % 10.61/2.23 % (3071665)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=850113794:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2991 on theBenchmark for (2991ds/130Mi) % 10.61/2.23 % (3071662)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=1941387306:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2992 on theBenchmark for (2992ds/294Mi) % 10.61/2.23 % (3071659)Instruction limit reached! % 10.61/2.23 % (3071659)------------------------------ % 10.61/2.23 % (3071659)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.61/2.23 % (3071659)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.61/2.23 % (3071659)CaDiCaL version: 2.1.3 % 10.61/2.23 % (3071659)Termination reason: Instruction limit % 10.61/2.23 % (3071659)Termination phase: Property scanning % 10.61/2.23 % (3071659)Time elapsed: 0.036 s % 10.61/2.23 % (3071659)Peak memory usage: 88 MB % 10.61/2.23 % (3071659)Instructions burned: 73 (million) % 10.61/2.23 % (3071661)Instruction limit reached! % 10.61/2.23 % (3071661)------------------------------ % 10.61/2.23 % (3071661)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.61/2.23 % (3071661)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.61/2.23 % (3071661)CaDiCaL version: 2.1.3 % 10.61/2.23 % (3071661)Termination reason: Instruction limit % 10.61/2.23 % (3071661)Termination phase: Saturation % 10.61/2.23 % (3071661)Time elapsed: 0.038 s % 10.61/2.23 % (3071661)Peak memory usage: 90 MB % 10.61/2.23 % (3071661)Instructions burned: 76 (million) % 10.61/2.23 % (3071652)Instruction limit reached! % 10.61/2.23 % (3071652)------------------------------ % 10.61/2.23 % (3071652)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.61/2.23 % (3071652)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.61/2.23 % (3071652)CaDiCaL version: 2.1.3 % 10.61/2.23 % (3071652)Termination reason: Instruction limit % 10.61/2.23 % (3071652)Termination phase: Saturation % 10.61/2.23 % (3071652)Time elapsed: 0.162 s % 10.61/2.23 % (3071652)Peak memory usage: 90 MB % 10.61/2.23 % (3071652)Instructions burned: 371 (million) % 10.61/2.23 % (3071665)Instruction limit reached! % 10.61/2.23 % (3071665)------------------------------ % 10.61/2.23 % (3071665)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.61/2.23 % (3071665)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.61/2.23 % (3071665)CaDiCaL version: 2.1.3 % 10.61/2.23 % (3071665)Termination reason: Instruction limit % 10.61/2.23 % (3071665)Termination phase: Saturation % 10.61/2.23 % (3071665)Time elapsed: 0.052 s % 10.61/2.23 % (3071665)Peak memory usage: 118 MB % 10.61/2.23 % (3071665)Instructions burned: 132 (million) % 10.61/2.23 % (3071668)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=1296908130:i=131:rtra=on_2991 on theBenchmark for (2991ds/131Mi) % 10.61/2.23 % (3071673)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=3861091572:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2990 on theBenchmark for (2990ds/40Mi) % 10.61/2.23 % (3071676)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=2758924359:i=131:canc=cautious:fsr=off:rtra=on_2990 on theBenchmark for (2990ds/131Mi) % 11.89/2.50 % (3071674)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=212793820:i=307:rtra=on:gtg=exists_top_2990 on theBenchmark for (2990ds/307Mi) % 11.89/2.50 % (3071673)Instruction limit reached! % 11.89/2.50 % (3071673)------------------------------ % 11.89/2.50 % (3071673)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.89/2.50 % (3071673)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.89/2.50 % (3071673)CaDiCaL version: 2.1.3 % 11.89/2.50 % (3071673)Termination reason: Instruction limit % 11.89/2.50 % (3071673)Termination phase: Preprocessing 1 % 11.89/2.50 % (3071673)Time elapsed: 0.018 s % 11.89/2.50 % (3071673)Peak memory usage: 86 MB % 11.89/2.50 % (3071673)Instructions burned: 41 (million) % 11.89/2.50 % (3071662)Instruction limit reached! % 11.89/2.50 % (3071662)------------------------------ % 11.89/2.50 % (3071662)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.89/2.50 % (3071662)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.89/2.50 % (3071662)CaDiCaL version: 2.1.3 % 11.89/2.50 % (3071662)Termination reason: Instruction limit % 11.89/2.50 % (3071662)Termination phase: Saturation % 11.89/2.50 % (3071662)Time elapsed: 0.172 s % 11.89/2.50 % (3071662)Peak memory usage: 92 MB % 11.89/2.50 % (3071662)Instructions burned: 295 (million) % 11.89/2.50 % (3071675)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=3974840079:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2990 on theBenchmark for (2990ds/598Mi) % 11.89/2.50 % (3071676)Instruction limit reached! % 11.89/2.50 % (3071676)------------------------------ % 11.89/2.50 % (3071676)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.89/2.50 % (3071676)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.89/2.50 % (3071676)CaDiCaL version: 2.1.3 % 11.89/2.50 % (3071676)Termination reason: Instruction limit % 11.89/2.50 % (3071676)Termination phase: Saturation % 11.89/2.50 % (3071676)Time elapsed: 0.053 s % 11.89/2.50 % (3071676)Peak memory usage: 118 MB % 11.89/2.50 % (3071676)Instructions burned: 132 (million) % 11.89/2.50 % (3071657)------------------------------ % 11.89/2.50 % (3071657)------------------------------ % 11.89/2.50 % (3071668)Instruction limit reached! % 11.89/2.50 % (3071668)------------------------------ % 11.89/2.50 % (3071668)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.89/2.50 % (3071668)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.89/2.50 % (3071668)CaDiCaL version: 2.1.3 % 11.89/2.50 % (3071668)Termination reason: Instruction limit % 11.89/2.50 % (3071668)Termination phase: Saturation % 11.89/2.50 % (3071668)Time elapsed: 0.120 s % 11.89/2.50 % (3071668)Peak memory usage: 135 MB % 11.89/2.50 % (3071668)Instructions burned: 131 (million) % 11.89/2.50 % (3071674)Instruction limit reached! % 11.89/2.50 % (3071674)------------------------------ % 11.89/2.50 % (3071674)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.89/2.50 % (3071674)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.89/2.50 % (3071674)CaDiCaL version: 2.1.3 % 11.89/2.50 % (3071674)Termination reason: Instruction limit % 11.89/2.50 % (3071674)Termination phase: Saturation % 11.89/2.50 % (3071674)Time elapsed: 0.141 s % 11.89/2.50 % (3071674)Peak memory usage: 91 MB % 11.89/2.50 % (3071674)Instructions burned: 309 (million) % 11.89/2.50 % (3071681)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=317246707:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2989 on theBenchmark for (2989ds/259Mi) % 11.89/2.50 % (3071682)dis+10_1_si=on:random_seed=1962124059:s2a=on:i=1000:rtra=on:gtg=exists_all_2989 on theBenchmark for (2989ds/1000Mi) % 11.89/2.50 % (3071684)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=1924726352:i=383:fsr=off:rtra=on:ev=force_2988 on theBenchmark for (2988ds/383Mi) % 11.89/2.50 % (3071681)Refutation not found, incomplete strategy % 11.89/2.50 % (3071681)------------------------------ % 11.89/2.50 % (3071681)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.89/2.50 % (3071681)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.89/2.50 % (3071681)CaDiCaL version: 2.1.3 % 11.89/2.50 % (3071681)Termination reason: Refutation not found, incomplete strategy % 11.89/2.50 % (3071681)Time elapsed: 0.039 s % 11.89/2.50 % (3071681)Peak memory usage: 112 MB % 13.28/2.70 % (3071681)Instructions burned: 30 (million) % 13.28/2.70 % (3071685)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=792256579:i=141:doe=on:rtra=on_2988 on theBenchmark for (2988ds/141Mi) % 13.28/2.70 % (3071686)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=1541404285:i=65:nm=16:rtra=on_2988 on theBenchmark for (2988ds/65Mi) % 13.28/2.70 % (3071686)Instruction limit reached! % 13.28/2.70 % (3071686)------------------------------ % 13.28/2.70 % (3071686)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.28/2.70 % (3071686)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.28/2.70 % (3071686)CaDiCaL version: 2.1.3 % 13.28/2.70 % (3071686)Termination reason: Instruction limit % 13.28/2.70 % (3071686)Termination phase: Saturation % 13.28/2.70 % (3071686)Time elapsed: 0.033 s % 13.28/2.70 % (3071686)Peak memory usage: 90 MB % 13.28/2.70 % (3071686)Instructions burned: 65 (million) % 13.28/2.70 % (3071684)Instruction limit reached! % 13.28/2.70 % (3071684)------------------------------ % 13.28/2.70 % (3071684)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.28/2.70 % (3071684)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.28/2.70 % (3071684)CaDiCaL version: 2.1.3 % 13.28/2.70 % (3071684)Termination reason: Instruction limit % 13.28/2.70 % (3071684)Termination phase: Saturation % 13.28/2.70 % (3071684)Time elapsed: 0.113 s % 13.28/2.70 % (3071684)Peak memory usage: 97 MB % 13.28/2.70 % (3071684)Instructions burned: 387 (million) % 13.28/2.70 % (3071685)Instruction limit reached! % 13.28/2.70 % (3071685)------------------------------ % 13.28/2.70 % (3071685)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.28/2.70 % (3071685)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.28/2.70 % (3071685)CaDiCaL version: 2.1.3 % 13.28/2.70 % (3071685)Termination reason: Instruction limit % 13.28/2.70 % (3071685)Termination phase: Saturation % 13.28/2.70 % (3071685)Time elapsed: 0.085 s % 13.28/2.70 % (3071685)Peak memory usage: 91 MB % 13.28/2.70 % (3071685)Instructions burned: 142 (million) % 13.28/2.70 % (3071687)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=3579065294:i=121:nm=16:rtra=on_2987 on theBenchmark for (2987ds/121Mi) % 13.28/2.70 % (3071687)Instruction limit reached! % 13.28/2.70 % (3071687)------------------------------ % 13.28/2.70 % (3071687)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.28/2.70 % (3071687)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.28/2.70 % (3071687)CaDiCaL version: 2.1.3 % 13.28/2.70 % (3071687)Termination reason: Instruction limit % 13.28/2.70 % (3071687)Termination phase: Saturation % 13.28/2.70 % (3071687)Time elapsed: 0.067 s % 13.28/2.70 % (3071687)Peak memory usage: 90 MB % 13.28/2.70 % (3071687)Instructions burned: 122 (million) % 13.28/2.70 % (3071694)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=862900454:i=39:ins=3:rtra=on_2986 on theBenchmark for (2986ds/39Mi) % 13.28/2.70 % (3071694)Instruction limit reached! % 13.28/2.70 % (3071694)------------------------------ % 13.28/2.70 % (3071694)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.28/2.70 % (3071694)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.28/2.70 % (3071694)CaDiCaL version: 2.1.3 % 13.28/2.70 % (3071694)Termination reason: Instruction limit % 13.28/2.70 % (3071694)Termination phase: Property scanning % 13.28/2.70 % (3071694)Time elapsed: 0.012 s % 13.28/2.70 % (3071694)Peak memory usage: 87 MB % 13.28/2.70 % (3071694)Instructions burned: 44 (million) % 13.28/2.70 % (3071693)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=3373723979:s2a=on:i=128:s2at=5:ins=3:rtra=on_2986 on theBenchmark for (2986ds/128Mi) % 13.28/2.70 % (3071681)------------------------------ % 13.28/2.70 % (3071681)------------------------------ % 13.28/2.70 % (3071695)dis+1010_1_to=kbo:si=on:random_seed=463571541:i=175:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2986 on theBenchmark for (2986ds/175Mi) % 13.28/2.70 % (3071675)Instruction limit reached! % 13.28/2.70 % (3071675)------------------------------ % 13.28/2.70 % (3071675)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.28/2.70 % (3071675)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.28/2.70 % (3071675)CaDiCaL version: 2.1.3 % 13.28/2.70 % (3071675)Termination reason: Instruction limit % 17.55/3.16 % (3071675)Termination phase: Saturation % 17.55/3.16 % (3071675)Time elapsed: 0.446 s % 17.55/3.16 % (3071675)Peak memory usage: 143 MB % 17.55/3.16 % (3071675)Instructions burned: 599 (million) % 17.55/3.16 % (3071693)Refutation not found, incomplete strategy % 17.55/3.16 % (3071693)------------------------------ % 17.55/3.16 % (3071693)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.55/3.16 % (3071693)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.55/3.16 % (3071693)CaDiCaL version: 2.1.3 % 17.55/3.16 % (3071693)Termination reason: Refutation not found, incomplete strategy % 17.55/3.16 % (3071693)Time elapsed: 0.089 s % 17.55/3.16 % (3071693)Peak memory usage: 115 MB % 17.55/3.16 % (3071693)Instructions burned: 117 (million) % 17.55/3.16 % (3071699)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=3096733572:s2a=on:i=483:doe=on:nm=32:rtra=on_2985 on theBenchmark for (2985ds/483Mi) % 17.55/3.16 % (3071697)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=1989675849:i=329:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2985 on theBenchmark for (2985ds/329Mi) % 17.55/3.16 % (3071695)Instruction limit reached! % 17.55/3.16 % (3071695)------------------------------ % 17.55/3.16 % (3071695)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.55/3.16 % (3071695)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.55/3.16 % (3071695)CaDiCaL version: 2.1.3 % 17.55/3.16 % (3071695)Termination reason: Instruction limit % 17.55/3.16 % (3071695)Termination phase: Saturation % 17.55/3.16 % (3071695)Time elapsed: 0.111 s % 17.55/3.16 % (3071695)Peak memory usage: 91 MB % 17.55/3.16 % (3071695)Instructions burned: 176 (million) % 17.55/3.16 % (3071701)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=876928304:thitd=on:i=215:nm=0:rtra=on:ev=force_2984 on theBenchmark for (2984ds/215Mi) % 17.55/3.16 % (3071703)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=3957747462:i=349:rtra=on_2984 on theBenchmark for (2984ds/349Mi) % 17.55/3.16 % (3071682)Instruction limit reached! % 17.55/3.16 % (3071682)------------------------------ % 17.55/3.16 % (3071682)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.55/3.16 % (3071682)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.55/3.16 % (3071682)CaDiCaL version: 2.1.3 % 17.55/3.16 % (3071682)Termination reason: Instruction limit % 17.55/3.16 % (3071682)Termination phase: Saturation % 17.55/3.16 % (3071682)Time elapsed: 0.534 s % 17.55/3.16 % (3071682)Peak memory usage: 97 MB % 17.55/3.16 % (3071682)Instructions burned: 1001 (million) % 17.55/3.16 % (3071699)Instruction limit reached! % 17.55/3.16 % (3071699)------------------------------ % 17.55/3.16 % (3071699)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.55/3.16 % (3071699)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.55/3.16 % (3071699)CaDiCaL version: 2.1.3 % 17.55/3.16 % (3071699)Termination reason: Instruction limit % 17.55/3.16 % (3071699)Termination phase: Saturation % 17.55/3.16 % (3071699)Time elapsed: 0.192 s % 17.55/3.16 % (3071699)Peak memory usage: 139 MB % 17.55/3.16 % (3071699)Instructions burned: 485 (million) % 17.55/3.16 % (3071697)Instruction limit reached! % 17.55/3.16 % (3071697)------------------------------ % 17.55/3.16 % (3071697)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.55/3.16 % (3071697)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.55/3.16 % (3071697)CaDiCaL version: 2.1.3 % 17.55/3.16 % (3071697)Termination reason: Instruction limit % 17.55/3.16 % (3071697)Termination phase: Saturation % 17.55/3.16 % (3071697)Time elapsed: 0.222 s % 17.55/3.16 % (3071697)Peak memory usage: 119 MB % 17.55/3.16 % (3071697)Instructions burned: 330 (million) % 17.55/3.16 % (3071706)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=3943905855:st=2:i=295:rtra=on:ss=axioms_2983 on theBenchmark for (2983ds/295Mi) % 17.55/3.16 % (3071693)------------------------------ % 17.55/3.16 % (3071693)------------------------------ % 17.55/3.16 % (3071701)Instruction limit reached! % 17.55/3.16 % (3071701)------------------------------ % 17.55/3.16 % (3071701)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.55/3.16 % (3071701)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.55/3.16 % (3071701)CaDiCaL version: 2.1.3 % 18.30/3.36 % (3071701)Termination reason: Instruction limit % 18.30/3.36 % (3071701)Termination phase: Saturation % 18.30/3.36 % (3071701)Time elapsed: 0.160 s % 18.30/3.36 % (3071701)Peak memory usage: 140 MB % 18.30/3.36 % (3071701)Instructions burned: 217 (million) % 18.30/3.36 % (3071706)Refutation not found, incomplete strategy % 18.30/3.36 % (3071706)------------------------------ % 18.30/3.36 % (3071706)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.30/3.36 % (3071706)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.30/3.36 % (3071706)CaDiCaL version: 2.1.3 % 18.30/3.36 % (3071706)Termination reason: Refutation not found, incomplete strategy % 18.30/3.36 % (3071706)Time elapsed: 0.013 s % 18.30/3.36 % (3071706)Peak memory usage: 88 MB % 18.30/3.36 % (3071706)Instructions burned: 25 (million) % 18.30/3.36 % (3071710)dis+1010_1_to=lpo:sil=128000:sas=z3:si=on:nwc=5:random_seed=841039147:i=281:gtgl=2:rtra=on:gtg=all_2982 on theBenchmark for (2982ds/281Mi) % 18.30/3.36 % (3071709)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=148261689:i=328:kws=inv_frequency:nm=20:rtra=on_2982 on theBenchmark for (2982ds/328Mi) % 18.30/3.36 % (3071703)Instruction limit reached! % 18.30/3.36 % (3071703)------------------------------ % 18.30/3.36 % (3071703)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.30/3.36 % (3071703)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.30/3.36 % (3071703)CaDiCaL version: 2.1.3 % 18.30/3.36 % (3071703)Termination reason: Instruction limit % 18.30/3.36 % (3071703)Termination phase: Saturation % 18.30/3.36 % (3071703)Time elapsed: 0.226 s % 18.30/3.36 % (3071703)Peak memory usage: 121 MB % 18.30/3.36 % (3071703)Instructions burned: 350 (million) % 18.30/3.36 % (3071712)lrs+1010_1_to=kbo:sil=128000:si=on:sos=on:urr=on:uwa=alasca_main:random_seed=622079702:i=484:doe=on:nm=0:av=off:rtra=on:ss=axioms_2981 on theBenchmark for (2981ds/484Mi) % 18.30/3.36 % (3071712)Refutation not found, incomplete strategy % 18.30/3.36 % (3071712)------------------------------ % 18.30/3.36 % (3071712)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.30/3.36 % (3071712)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.30/3.36 % (3071712)CaDiCaL version: 2.1.3 % 18.30/3.36 % (3071712)Termination reason: Refutation not found, incomplete strategy % 18.30/3.36 % (3071712)Time elapsed: 0.013 s % 18.30/3.36 % (3071712)Peak memory usage: 88 MB % 18.30/3.36 % (3071712)Instructions burned: 24 (million) % 18.30/3.36 % (3071713)lrs+21_1_to=kbo:sil=128000:thi=neg_eq:si=on:random_seed=4025507964:i=321:canc=force:rtra=on:tac=axiom:ss=axioms:ev=force_2981 on theBenchmark for (2981ds/321Mi) % 18.30/3.36 % (3071710)Instruction limit reached! % 18.30/3.36 % (3071710)------------------------------ % 18.30/3.36 % (3071710)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.30/3.36 % (3071710)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.30/3.36 % (3071710)CaDiCaL version: 2.1.3 % 18.30/3.36 % (3071710)Termination reason: Instruction limit % 18.30/3.36 % (3071710)Termination phase: Saturation % 18.30/3.36 % (3071710)Time elapsed: 0.092 s % 18.30/3.36 % (3071710)Peak memory usage: 118 MB % 18.30/3.36 % (3071710)Instructions burned: 285 (million) % 18.30/3.36 % (3071714)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=1824314155:i=416:rtra=on:gtg=position:ss=axioms_2981 on theBenchmark for (2981ds/416Mi) % 18.30/3.36 % (3071713)Refutation not found, incomplete strategy % 18.30/3.36 % (3071713)------------------------------ % 18.30/3.36 % (3071713)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.30/3.36 % (3071713)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.30/3.36 % (3071713)CaDiCaL version: 2.1.3 % 18.30/3.36 % (3071713)Termination reason: Refutation not found, incomplete strategy % 18.30/3.36 % (3071713)Time elapsed: 0.038 s % 18.30/3.36 % (3071713)Peak memory usage: 112 MB % 18.30/3.36 % (3071713)Instructions burned: 29 (million) % 18.30/3.36 % (3071714)Refutation not found, incomplete strategy % 18.30/3.36 % (3071714)------------------------------ % 18.30/3.36 % (3071714)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.30/3.36 % (3071714)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.30/3.36 % (3071714)CaDiCaL version: 2.1.3 % 18.30/3.36 % (3071714)Termination reason: Refutation not found, incomplete strategy % 18.30/3.36 % (3071714)Time elapsed: 0.038 s % 19.76/3.74 % (3071714)Peak memory usage: 112 MB % 19.76/3.74 % (3071714)Instructions burned: 28 (million) % 19.76/3.74 % (3071706)------------------------------ % 19.76/3.74 % (3071706)------------------------------ % 19.76/3.74 % (3071718)lrs+1010_1_to=kbo:tgt=ground:fde=unused:sas=z3:si=on:sp=unary_frequency:gve=force:spb=goal:tha=off:random_seed=1895016929:i=471:thf=on:kws=precedence:rtra=on_2980 on theBenchmark for (2980ds/471Mi) % 19.76/3.74 % (3071721)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=3886087258:avsq=on:i=276:avsqr=1,2:rtra=on_2980 on theBenchmark for (2980ds/276Mi) % 19.76/3.74 % (3071709)Instruction limit reached! % 19.76/3.74 % (3071709)------------------------------ % 19.76/3.74 % (3071709)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.76/3.74 % (3071709)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.76/3.74 % (3071709)CaDiCaL version: 2.1.3 % 19.76/3.74 % (3071709)Termination reason: Instruction limit % 19.76/3.74 % (3071709)Termination phase: Saturation % 19.76/3.74 % (3071709)Time elapsed: 0.219 s % 19.76/3.74 % (3071709)Peak memory usage: 121 MB % 19.76/3.74 % (3071709)Instructions burned: 328 (million) % 19.76/3.74 % (3071712)------------------------------ % 19.76/3.74 % (3071712)------------------------------ % 19.76/3.74 % (3071721)Instruction limit reached! % 19.76/3.74 % (3071721)------------------------------ % 19.76/3.74 % (3071721)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.76/3.74 % (3071721)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.76/3.74 % (3071721)CaDiCaL version: 2.1.3 % 19.76/3.74 % (3071721)Termination reason: Instruction limit % 19.76/3.74 % (3071721)Termination phase: Saturation % 19.76/3.74 % (3071721)Time elapsed: 0.123 s % 19.76/3.74 % (3071721)Peak memory usage: 136 MB % 19.76/3.74 % (3071721)Instructions burned: 278 (million) % 19.76/3.74 % (3071722)lrs+1010_2_to=kbo:sil=128000:tgt=ground:fde=unused:sas=z3:si=on:uwa=off:tha=off:nwc=1:random_seed=1530927389:i=375:kws=inv_arity_squared:rtra=on_2979 on theBenchmark for (2979ds/375Mi) % 19.76/3.74 % (3071713)------------------------------ % 19.76/3.74 % (3071713)------------------------------ % 19.76/3.74 % (3071714)------------------------------ % 19.76/3.74 % (3071714)------------------------------ % 19.76/3.74 % (3071725)lrs+10_1_to=kbo:sil=128000:tgt=full:sas=z3:si=on:uwa=func_ext:slsqc=1:flr=on:slsq=on:random_seed=3566041344:i=387:bd=preordered:rtra=on:ss=axioms:sgt=8_2978 on theBenchmark for (2978ds/387Mi) % 19.76/3.74 % (3071725)Refutation not found, incomplete strategy % 19.76/3.74 % (3071725)------------------------------ % 19.76/3.74 % (3071725)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.76/3.74 % (3071725)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.76/3.74 % (3071725)CaDiCaL version: 2.1.3 % 19.76/3.74 % (3071725)Termination reason: Refutation not found, incomplete strategy % 19.76/3.74 % (3071725)Time elapsed: 0.040 s % 19.76/3.74 % (3071725)Peak memory usage: 112 MB % 19.76/3.74 % (3071725)Instructions burned: 31 (million) % 19.76/3.74 % (3071727)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=1131469477:i=334:rtra=on_2977 on theBenchmark for (2977ds/334Mi) % 19.76/3.74 % (3071726)lrs+10_1_to=kbo:sil=128000:fde=none:si=on:norm_ineq=on:urr=on:nwc=0.5:random_seed=2412014785:i=513:kws=frequency:bd=all:rtra=on:gtg=exists_all:ss=axioms:sgt=4_2977 on theBenchmark for (2977ds/513Mi) % 19.76/3.74 % (3071718)Instruction limit reached! % 19.76/3.74 % (3071718)------------------------------ % 19.76/3.74 % (3071718)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.76/3.74 % (3071718)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.76/3.74 % (3071718)CaDiCaL version: 2.1.3 % 19.76/3.74 % (3071718)Termination reason: Instruction limit % 19.76/3.74 % (3071718)Termination phase: Saturation % 19.76/3.74 % (3071718)Time elapsed: 0.296 s % 19.76/3.74 % (3071718)Peak memory usage: 121 MB % 19.76/3.74 % (3071718)Instructions burned: 471 (million) % 19.76/3.74 % (3071729)lrs+1010_1_to=kbo:sil=64000:sas=cadical:si=on:sos=on:bce=on:random_seed=224208082:i=359:rtra=on:gtg=exists_top:ss=axioms_2977 on theBenchmark for (2977ds/359Mi) % 19.76/3.74 % (3071730)dis+1010_1_to=lpo:sil=128000:thi=all:fde=unused:si=on:sp=reverse_arity:tha=off:random_seed=3670568660:i=341:gtgl=2:rtra=on:gtg=exists_sym:ev=force:fsd=on:fsdmm=1_2977 on theBenchmark for (2977ds/341Mi) % 19.76/3.74 % (3071727)Instruction limit reached! % 23.91/4.08 % (3071727)------------------------------ % 23.91/4.08 % (3071727)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.91/4.08 % (3071727)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.91/4.08 % (3071727)CaDiCaL version: 2.1.3 % 23.91/4.08 % (3071727)Termination reason: Instruction limit % 23.91/4.08 % (3071727)Termination phase: Saturation % 23.91/4.08 % (3071727)Time elapsed: 0.138 s % 23.91/4.08 % (3071727)Peak memory usage: 138 MB % 23.91/4.08 % (3071727)Instructions burned: 336 (million) % 23.91/4.08 % (3071722)Instruction limit reached! % 23.91/4.08 % (3071722)------------------------------ % 23.91/4.08 % (3071722)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.91/4.08 % (3071722)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.91/4.08 % (3071722)CaDiCaL version: 2.1.3 % 23.91/4.08 % (3071722)Termination reason: Instruction limit % 23.91/4.08 % (3071722)Termination phase: Saturation % 23.91/4.08 % (3071722)Time elapsed: 0.241 s % 23.91/4.08 % (3071722)Peak memory usage: 120 MB % 23.91/4.08 % (3071722)Instructions burned: 376 (million) % 23.91/4.08 % (3071734)lrs-2_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_max:tha=off:random_seed=3295690280:st=1.5:i=261:sd=1:kws=precedence:rtra=on:ss=axioms_2976 on theBenchmark for (2976ds/261Mi) % 23.91/4.08 % (3071725)------------------------------ % 23.91/4.08 % (3071725)------------------------------ % 23.91/4.08 % (3071734)Refutation not found, incomplete strategy % 23.91/4.08 % (3071734)------------------------------ % 23.91/4.08 % (3071734)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.91/4.08 % (3071734)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.91/4.08 % (3071734)CaDiCaL version: 2.1.3 % 23.91/4.08 % (3071734)Termination reason: Refutation not found, incomplete strategy % 23.91/4.08 % (3071734)Time elapsed: 0.034 s % 23.91/4.08 % (3071734)Peak memory usage: 111 MB % 23.91/4.08 % (3071734)Instructions burned: 21 (million) % 23.91/4.08 % (3071729)Instruction limit reached! % 23.91/4.08 % (3071729)------------------------------ % 23.91/4.08 % (3071729)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.91/4.08 % (3071729)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.91/4.08 % (3071729)CaDiCaL version: 2.1.3 % 23.91/4.08 % (3071729)Termination reason: Instruction limit % 23.91/4.08 % (3071729)Termination phase: Saturation % 23.91/4.08 % (3071729)Time elapsed: 0.194 s % 23.91/4.08 % (3071729)Peak memory usage: 93 MB % 23.91/4.08 % (3071729)Instructions burned: 359 (million) % 23.91/4.08 % (3071737)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=3736539552:s2pl=no:i=235:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2975 on theBenchmark for (2975ds/235Mi) % 23.91/4.08 % (3071737)Refutation not found, incomplete strategy % 23.91/4.08 % (3071737)------------------------------ % 23.91/4.08 % (3071737)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.91/4.08 % (3071737)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.91/4.08 % (3071737)CaDiCaL version: 2.1.3 % 23.91/4.08 % (3071737)Termination reason: Refutation not found, incomplete strategy % 23.91/4.08 % (3071737)Time elapsed: 0.023 s % 23.91/4.08 % (3071737)Peak memory usage: 112 MB % 23.91/4.08 % (3071737)Instructions burned: 31 (million) % 23.91/4.08 % (3071730)Instruction limit reached! % 23.91/4.08 % (3071730)------------------------------ % 23.91/4.08 % (3071730)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.91/4.08 % (3071730)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.91/4.08 % (3071730)CaDiCaL version: 2.1.3 % 23.91/4.08 % (3071730)Termination reason: Instruction limit % 23.91/4.08 % (3071730)Termination phase: Saturation % 23.91/4.08 % (3071730)Time elapsed: 0.220 s % 23.91/4.08 % (3071730)Peak memory usage: 121 MB % 23.91/4.08 % (3071730)Instructions burned: 343 (million) % 23.91/4.08 % (3071738)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=3607995878:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2975 on theBenchmark for (2975ds/273Mi) % 23.91/4.08 % (3071726)Instruction limit reached! % 23.91/4.08 % (3071726)------------------------------ % 23.91/4.08 % (3071726)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.91/4.08 % (3071726)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.59/4.69 % (3071726)CaDiCaL version: 2.1.3 % 26.59/4.69 % (3071726)Termination reason: Instruction limit % 26.59/4.69 % (3071726)Termination phase: Saturation % 26.59/4.69 % (3071726)Time elapsed: 0.313 s % 26.59/4.69 % (3071726)Peak memory usage: 94 MB % 26.59/4.69 % (3071726)Instructions burned: 514 (million) % 26.59/4.69 % (3071740)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=937279072:i=146:doe=on:rtra=on_2974 on theBenchmark for (2974ds/146Mi) % 26.59/4.69 % (3071742)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=4099081473:i=4428:doe=on:fsr=off:rtra=on_2973 on theBenchmark for (2973ds/4428Mi) % 26.59/4.69 % (3071737)------------------------------ % 26.59/4.69 % (3071737)------------------------------ % 26.59/4.69 % (3071744)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=304369712:avsq=on:i=276:avsqr=1,2:rtra=on_2973 on theBenchmark for (2973ds/276Mi) % 26.59/4.69 % (3071740)Instruction limit reached! % 26.59/4.69 % (3071740)------------------------------ % 26.59/4.69 % (3071740)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.59/4.69 % (3071740)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.59/4.69 % (3071740)CaDiCaL version: 2.1.3 % 26.59/4.69 % (3071740)Termination reason: Instruction limit % 26.59/4.69 % (3071740)Termination phase: Saturation % 26.59/4.69 % (3071740)Time elapsed: 0.084 s % 26.59/4.69 % (3071740)Peak memory usage: 91 MB % 26.59/4.69 % (3071740)Instructions burned: 146 (million) % 26.59/4.69 % (3071745)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=1274671990:i=1052:rtra=on_2973 on theBenchmark for (2973ds/1052Mi) % 26.59/4.69 % (3071734)------------------------------ % 26.59/4.69 % (3071734)------------------------------ % 26.59/4.69 % (3071738)Instruction limit reached! % 26.59/4.69 % (3071738)------------------------------ % 26.59/4.69 % (3071738)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.59/4.69 % (3071738)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.59/4.69 % (3071738)CaDiCaL version: 2.1.3 % 26.59/4.69 % (3071738)Termination reason: Instruction limit % 26.59/4.69 % (3071738)Termination phase: Saturation % 26.59/4.70 % (3071738)Time elapsed: 0.179 s % 26.59/4.70 % (3071738)Peak memory usage: 93 MB % 26.59/4.70 % (3071738)Instructions burned: 274 (million) % 26.59/4.70 % (3071748)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=1074666618:i=655:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2972 on theBenchmark for (2972ds/655Mi) % 26.59/4.70 % (3071751)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=1157586307:st=5:i=1054:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2971 on theBenchmark for (2971ds/1054Mi) % 26.59/4.70 % (3071751)Refutation not found, incomplete strategy % 26.59/4.70 % (3071751)------------------------------ % 26.59/4.70 % (3071751)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.59/4.70 % (3071751)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.59/4.70 % (3071751)CaDiCaL version: 2.1.3 % 26.59/4.70 % (3071751)Termination reason: Refutation not found, incomplete strategy % 26.59/4.70 % (3071751)Time elapsed: 0.009 s % 26.59/4.70 % (3071751)Peak memory usage: 88 MB % 26.59/4.70 % (3071751)Instructions burned: 16 (million) % 26.59/4.70 % (3071753)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=3761685594:s2a=on:i=450:doe=on:nm=32:rtra=on_2971 on theBenchmark for (2971ds/450Mi) % 26.59/4.70 % (3071752)lrs-1002_1_to=kbo:sas=z3:si=on:norm_ineq=on:sos=on:tha=some:random_seed=853606091:i=107:rtra=on_2971 on theBenchmark for (2971ds/107Mi) % 26.59/4.70 % (3071744)Instruction limit reached! % 26.59/4.70 % (3071744)------------------------------ % 26.59/4.70 % (3071744)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.59/4.70 % (3071744)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.59/4.70 % (3071744)CaDiCaL version: 2.1.3 % 26.59/4.70 % (3071744)Termination reason: Instruction limit % 26.59/4.70 % (3071744)Termination phase: Saturation % 26.59/4.70 % (3071744)Time elapsed: 0.217 s % 26.59/4.70 % (3071744)Peak memory usage: 136 MB % 26.59/4.70 % (3071744)Instructions burned: 277 (million) % 26.59/4.70 % (3071752)Refutation not found, incomplete strategy % 26.59/4.70 % (3071752)------------------------------ % 26.59/4.70 % (3071752)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 28.21/5.00 % (3071752)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.21/5.00 % (3071752)CaDiCaL version: 2.1.3 % 28.21/5.00 % (3071752)Termination reason: Refutation not found, incomplete strategy % 28.21/5.00 % (3071752)Time elapsed: 0.080 s % 28.21/5.00 % (3071752)Peak memory usage: 115 MB % 28.21/5.00 % (3071752)Instructions burned: 108 (million) % 28.21/5.00 % (3071748)Instruction limit reached! % 28.21/5.00 % (3071748)------------------------------ % 28.21/5.00 % (3071748)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 28.21/5.00 % (3071748)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.21/5.00 % (3071748)CaDiCaL version: 2.1.3 % 28.21/5.00 % (3071748)Termination reason: Instruction limit % 28.21/5.00 % (3071748)Termination phase: Saturation % 28.21/5.00 % (3071748)Time elapsed: 0.188 s % 28.21/5.00 % (3071748)Peak memory usage: 95 MB % 28.21/5.00 % (3071748)Instructions burned: 658 (million) % 28.21/5.00 % (3071758)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.21/5.00 % (3071758)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=796335190:i=1090:aac=none:nm=0:rtra=on:rawr=on_2969 on theBenchmark for (2969ds/1090Mi) % 28.21/5.00 % (3071759)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=3014278669:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2969 on theBenchmark for (2969ds/130Mi) % 28.21/5.00 % (3071751)------------------------------ % 28.21/5.00 % (3071751)------------------------------ % 28.21/5.00 % (3071759)Instruction limit reached! % 28.21/5.00 % (3071759)------------------------------ % 28.21/5.00 % (3071759)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 28.21/5.00 % (3071759)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.21/5.00 % (3071759)CaDiCaL version: 2.1.3 % 28.21/5.00 % (3071759)Termination reason: Instruction limit % 28.21/5.00 % (3071759)Termination phase: Saturation % 28.21/5.00 % (3071759)Time elapsed: 0.051 s % 28.21/5.00 % (3071759)Peak memory usage: 118 MB % 28.21/5.00 % (3071759)Instructions burned: 131 (million) % 28.21/5.00 % (3071752)------------------------------ % 28.21/5.00 % (3071752)------------------------------ % 28.21/5.00 % (3071753)Instruction limit reached! % 28.21/5.00 % (3071753)------------------------------ % 28.21/5.00 % (3071753)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 28.21/5.00 % (3071753)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.21/5.00 % (3071753)CaDiCaL version: 2.1.3 % 28.21/5.00 % (3071753)Termination reason: Instruction limit % 28.21/5.00 % (3071753)Termination phase: Saturation % 28.21/5.00 % (3071753)Time elapsed: 0.330 s % 28.21/5.00 % (3071753)Peak memory usage: 139 MB % 28.21/5.00 % (3071753)Instructions burned: 450 (million) % 28.21/5.00 % (3071762)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=1416681686:i=312:kws=inv_frequency:nm=20:rtra=on_2967 on theBenchmark for (2967ds/312Mi) % 28.21/5.00 % (3071763)ott+10_1_to=kbo:sil=64000:si=on:sp=reverse_frequency:sos=on:random_seed=184114061:i=491:doe=on:rtra=on:gtg=position_2967 on theBenchmark for (2967ds/491Mi) % 28.21/5.00 % (3071745)Instruction limit reached! % 28.21/5.00 % (3071745)------------------------------ % 28.21/5.00 % (3071745)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 28.21/5.00 % (3071745)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.21/5.00 % (3071745)CaDiCaL version: 2.1.3 % 28.21/5.00 % (3071745)Termination reason: Instruction limit % 28.21/5.00 % (3071745)Termination phase: Saturation % 28.21/5.00 % (3071745)Time elapsed: 0.555 s % 28.21/5.00 % (3071745)Peak memory usage: 98 MB % 28.21/5.00 % (3071745)Instructions burned: 1053 (million) % 28.21/5.00 % (3071763)Refutation not found, incomplete strategy % 28.21/5.00 % (3071763)------------------------------ % 28.21/5.00 % (3071763)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 28.21/5.00 % (3071763)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.21/5.00 % (3071763)CaDiCaL version: 2.1.3 % 28.21/5.00 % (3071763)Termination reason: Refutation not found, incomplete strategy % 28.21/5.00 % (3071763)Time elapsed: 0.031 s % 28.21/5.00 % (3071763)Peak memory usage: 91 MB % 28.21/5.00 % (3071763)Instructions burned: 111 (million) % 33.26/5.58 % (3071764)ott+1011_4:1_to=lpo:sil=64000:si=on:spb=intro:random_seed=3714255539:s2a=on:i=835:s2at=2:rtra=on_2966 on theBenchmark for (2966ds/835Mi) % 33.26/5.58 % (3071765)ott+1011_2_to=lpo:sil=128000:si=on:sos=on:random_seed=654208401:i=307:bd=preordered:av=off:rtra=on:ev=cautious_2966 on theBenchmark for (2966ds/307Mi) % 33.26/5.58 % (3071765)Refutation not found, incomplete strategy % 33.26/5.58 % (3071765)------------------------------ % 33.26/5.58 % (3071765)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.26/5.58 % (3071765)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.26/5.58 % (3071765)CaDiCaL version: 2.1.3 % 33.26/5.58 % (3071765)Termination reason: Refutation not found, incomplete strategy % 33.26/5.58 % (3071765)Time elapsed: 0.076 s % 33.26/5.58 % (3071765)Peak memory usage: 91 MB % 33.26/5.58 % (3071765)Instructions burned: 136 (million) % 33.26/5.58 % (3071763)------------------------------ % 33.26/5.58 % (3071763)------------------------------ % 33.26/5.58 % (3071768)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=201993134:i=776:doe=on:rtra=on_2966 on theBenchmark for (2966ds/776Mi) % 33.26/5.58 % (3071762)Instruction limit reached! % 33.26/5.58 % (3071762)------------------------------ % 33.26/5.58 % (3071762)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.26/5.58 % (3071762)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.26/5.58 % (3071762)CaDiCaL version: 2.1.3 % 33.26/5.58 % (3071762)Termination reason: Instruction limit % 33.26/5.58 % (3071762)Termination phase: Saturation % 33.26/5.58 % (3071762)Time elapsed: 0.206 s % 33.26/5.58 % (3071762)Peak memory usage: 120 MB % 33.26/5.58 % (3071762)Instructions burned: 312 (million) % 33.26/5.58 % (3071772)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=1639355500:s2a=on:i=646:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2964 on theBenchmark for (2964ds/646Mi) % 33.26/5.58 % (3071773)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=537258887:thitd=on:cond=fast:i=784:nm=30:rtra=on:gtg=all:tac=axiom_2964 on theBenchmark for (2964ds/784Mi) % 33.26/5.58 % (3071765)------------------------------ % 33.26/5.58 % (3071765)------------------------------ % 33.26/5.58 % (3071758)Instruction limit reached! % 33.26/5.58 % (3071758)------------------------------ % 33.26/5.58 % (3071758)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.26/5.58 % (3071758)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.26/5.58 % (3071758)CaDiCaL version: 2.1.3 % 33.26/5.58 % (3071758)Termination reason: Instruction limit % 33.26/5.58 % (3071758)Termination phase: Saturation % 33.26/5.58 % (3071758)Time elapsed: 0.668 s % 33.26/5.58 % (3071758)Peak memory usage: 128 MB % 33.26/5.58 % (3071758)Instructions burned: 1090 (million) % 33.26/5.58 % (3071764)Instruction limit reached! % 33.26/5.58 % (3071764)------------------------------ % 33.26/5.58 % (3071764)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.26/5.58 % (3071764)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.26/5.58 % (3071764)CaDiCaL version: 2.1.3 % 33.26/5.58 % (3071764)Termination reason: Instruction limit % 33.26/5.58 % (3071764)Termination phase: Saturation % 33.26/5.58 % (3071764)Time elapsed: 0.477 s % 33.26/5.58 % (3071764)Peak memory usage: 97 MB % 33.26/5.58 % (3071764)Instructions burned: 835 (million) % 33.26/5.58 % (3071772)Instruction limit reached! % 33.26/5.58 % (3071772)------------------------------ % 33.26/5.58 % (3071772)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.26/5.58 % (3071772)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.26/5.58 % (3071772)CaDiCaL version: 2.1.3 % 33.26/5.58 % (3071772)Termination reason: Instruction limit % 33.26/5.58 % (3071772)Termination phase: Saturation % 33.26/5.58 % (3071772)Time elapsed: 0.256 s % 33.26/5.58 % (3071772)Peak memory usage: 143 MB % 33.26/5.58 % (3071772)Instructions burned: 649 (million) % 33.26/5.58 % (3071776)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=2840711995:thitd=on:s2a=on:i=1131:add=on:canc=force:bd=all:rtra=on:tac=axiom:ev=off_2962 on theBenchmark for (2962ds/1131Mi) % 33.26/5.58 % (3071777)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=3729037471:s2pl=no:i=246:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2961 on theBenchmark for (2961ds/246Mi) % 42.08/6.71 % (3071768)Instruction limit reached! % 42.08/6.71 % (3071768)------------------------------ % 42.08/6.71 % (3071768)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 42.08/6.71 % (3071768)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.08/6.71 % (3071768)CaDiCaL version: 2.1.3 % 42.08/6.71 % (3071768)Termination reason: Instruction limit % 42.08/6.71 % (3071768)Termination phase: Saturation % 42.08/6.71 % (3071768)Time elapsed: 0.493 s % 42.08/6.71 % (3071768)Peak memory usage: 126 MB % 42.08/6.71 % (3071768)Instructions burned: 777 (million) % 42.08/6.71 % (3071777)Refutation not found, incomplete strategy % 42.08/6.71 % (3071777)------------------------------ % 42.08/6.71 % (3071777)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 42.08/6.71 % (3071777)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.08/6.71 % (3071777)CaDiCaL version: 2.1.3 % 42.08/6.71 % (3071777)Termination reason: Refutation not found, incomplete strategy % 42.08/6.71 % (3071777)Time elapsed: 0.039 s % 42.08/6.71 % (3071777)Peak memory usage: 112 MB % 42.08/6.71 % (3071777)Instructions burned: 30 (million) % 42.08/6.71 % (3071779)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=1362582287:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2960 on theBenchmark for (2960ds/273Mi) % 42.08/6.71 % (3071778)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=3364394259:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2960 on theBenchmark for (2960ds/775Mi) % 42.08/6.71 % (3071778)Refutation not found, incomplete strategy % 42.08/6.71 % (3071778)------------------------------ % 42.08/6.71 % (3071778)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 42.08/6.71 % (3071778)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.08/6.71 % (3071778)CaDiCaL version: 2.1.3 % 42.08/6.71 % (3071778)Termination reason: Refutation not found, incomplete strategy % 42.08/6.71 % (3071778)Time elapsed: 0.014 s % 42.08/6.71 % (3071778)Peak memory usage: 88 MB % 42.08/6.71 % (3071778)Instructions burned: 28 (million) % 42.08/6.71 % (3071779)Instruction limit reached! % 42.08/6.71 % (3071779)------------------------------ % 42.08/6.71 % (3071779)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 42.08/6.71 % (3071779)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.08/6.71 % (3071779)CaDiCaL version: 2.1.3 % 42.08/6.71 % (3071779)Termination reason: Instruction limit % 42.08/6.71 % (3071779)Termination phase: Saturation % 42.08/6.71 % (3071779)Time elapsed: 0.091 s % 42.08/6.71 % (3071779)Peak memory usage: 93 MB % 42.08/6.71 % (3071779)Instructions burned: 273 (million) % 42.08/6.71 % (3071773)Instruction limit reached! % 42.08/6.71 % (3071773)------------------------------ % 42.08/6.71 % (3071773)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 42.08/6.71 % (3071773)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.08/6.71 % (3071773)CaDiCaL version: 2.1.3 % 42.08/6.71 % (3071773)Termination reason: Instruction limit % 42.08/6.71 % (3071773)Termination phase: Saturation % 42.08/6.71 % (3071773)Time elapsed: 0.483 s % 42.08/6.71 % (3071773)Peak memory usage: 124 MB % 42.08/6.71 % (3071773)Instructions burned: 784 (million) % 42.08/6.71 % (3071782)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=771320782:i=102:nm=16:rtra=on_2959 on theBenchmark for (2959ds/102Mi) % 42.08/6.71 % (3071785)lrs+10_1_to=lpo:sil=128000:si=on:bsr=unit_only:tha=off:random_seed=3203632204:avsq=on:s2a=on:i=1094:s2at=5:avsqr=4463,131072:rtra=on_2958 on theBenchmark for (2958ds/1094Mi) % 42.08/6.71 % (3071782)Instruction limit reached! % 42.08/6.71 % (3071782)------------------------------ % 42.08/6.71 % (3071782)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 42.08/6.71 % (3071782)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.08/6.71 % (3071782)CaDiCaL version: 2.1.3 % 42.08/6.71 % (3071782)Termination reason: Instruction limit % 42.08/6.71 % (3071782)Termination phase: Saturation % 42.08/6.71 % (3071782)Time elapsed: 0.054 s % 42.08/6.71 % (3071782)Peak memory usage: 90 MB % 42.08/6.71 % (3071782)Instructions burned: 102 (million) % 42.08/6.71 % (3071777)------------------------------ % 42.08/6.71 % (3071777)------------------------------ % 42.08/6.71 % (3071778)------------------------------ % 42.08/6.71 % (3071778)------------------------------ % 50.14/7.83 % (3071787)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=1324010270:i=6400:doe=on:fsr=off:rtra=on_2957 on theBenchmark for (2957ds/6400Mi) % 50.14/7.83 % (3071789)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=1364981875:i=868:doe=on:nm=0:rtra=on:gtg=exists_sym_2957 on theBenchmark for (2957ds/868Mi) % 50.14/7.83 % (3071790)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=2130127555:i=1846:canc=cautious:fsr=off:rtra=on_2956 on theBenchmark for (2956ds/1846Mi) % 50.14/7.83 % (3071791)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=3534072571:s2a=on:i=36816:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2956 on theBenchmark for (2956ds/36816Mi) % 50.14/7.83 % (3071790)Refutation not found, incomplete strategy % 50.14/7.83 % (3071790)------------------------------ % 50.14/7.83 % (3071790)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 50.14/7.83 % (3071790)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 50.14/7.83 % (3071790)CaDiCaL version: 2.1.3 % 50.14/7.83 % (3071790)Termination reason: Refutation not found, incomplete strategy % 50.14/7.83 % (3071790)Time elapsed: 0.054 s % 50.14/7.83 % (3071790)Peak memory usage: 91 MB % 50.14/7.83 % (3071790)Instructions burned: 104 (million) % 50.14/7.83 % (3071742)Instruction limit reached! % 50.14/7.83 % (3071742)------------------------------ % 50.14/7.83 % (3071742)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 50.14/7.83 % (3071742)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 50.14/7.83 % (3071742)CaDiCaL version: 2.1.3 % 50.14/7.83 % (3071742)Termination reason: Instruction limit % 50.14/7.83 % (3071742)Termination phase: Saturation % 50.14/7.83 % (3071742)Time elapsed: 1.822 s % 50.14/7.83 % (3071742)Peak memory usage: 102 MB % 50.14/7.83 % (3071742)Instructions burned: 4428 (million) % 50.14/7.83 % (3071785)Instruction limit reached! % 50.14/7.83 % (3071785)------------------------------ % 50.14/7.83 % (3071785)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 50.14/7.83 % (3071785)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 50.14/7.83 % (3071785)CaDiCaL version: 2.1.3 % 50.14/7.83 % (3071785)Termination reason: Instruction limit % 50.14/7.83 % (3071785)Termination phase: Saturation % 50.14/7.83 % (3071785)Time elapsed: 0.334 s % 50.14/7.83 % (3071785)Peak memory usage: 97 MB % 50.14/7.83 % (3071785)Instructions burned: 1094 (million) % 50.14/7.83 % (3071776)Instruction limit reached! % 50.14/7.83 % (3071776)------------------------------ % 50.14/7.83 % (3071776)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 50.14/7.83 % (3071776)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 50.14/7.83 % (3071776)CaDiCaL version: 2.1.3 % 50.14/7.83 % (3071776)Termination reason: Instruction limit % 50.14/7.83 % (3071776)Termination phase: Saturation % 50.14/7.83 % (3071776)Time elapsed: 0.726 s % 50.14/7.83 % (3071776)Peak memory usage: 135 MB % 50.14/7.83 % (3071776)Instructions burned: 1132 (million) % 50.14/7.83 % (3071797)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=3048123131:i=863:doe=on:nm=0:rtra=on:gtg=exists_sym_2953 on theBenchmark for (2953ds/863Mi) % 50.14/7.83 % (3071796)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=4139344820:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2954 on theBenchmark for (2954ds/273Mi) % 50.14/7.83 % (3071790)------------------------------ % 50.14/7.83 % (3071790)------------------------------ % 50.14/7.83 % (3071798)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=315173179:i=5811:kws=precedence:nm=0:rtra=on_2953 on theBenchmark for (2953ds/5811Mi) % 50.14/7.83 % (3071796)Instruction limit reached! % 50.14/7.83 % (3071796)------------------------------ % 50.14/7.83 % (3071796)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 50.14/7.83 % (3071796)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 50.14/7.83 % (3071796)CaDiCaL version: 2.1.3 % 50.14/7.83 % (3071796)Termination reason: Instruction limit % 50.14/7.83 % (3071796)Termination phase: Saturation % 50.14/7.83 % (3071796)Time elapsed: 0.174 s % 50.14/7.83 % (3071796)Peak memory usage: 93 MB % 50.14/7.83 % (3071796)Instructions burned: 273 (million) % 57.88/8.94 % (3071801)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=868980269:i=2216:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2952 on theBenchmark for (2952ds/2216Mi) % 57.88/8.94 % (3071789)Instruction limit reached! % 57.88/8.94 % (3071789)------------------------------ % 57.88/8.94 % (3071789)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 57.88/8.94 % (3071789)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 57.88/8.94 % (3071789)CaDiCaL version: 2.1.3 % 57.88/8.94 % (3071789)Termination reason: Instruction limit % 57.88/8.94 % (3071789)Termination phase: Saturation % 57.88/8.94 % (3071789)Time elapsed: 0.497 s % 57.88/8.94 % (3071789)Peak memory usage: 123 MB % 57.88/8.94 % (3071789)Instructions burned: 868 (million) % 57.88/8.94 % (3071797)Instruction limit reached! % 57.88/8.94 % (3071797)------------------------------ % 57.88/8.94 % (3071797)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 57.88/8.94 % (3071797)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 57.88/8.94 % (3071797)CaDiCaL version: 2.1.3 % 57.88/8.94 % (3071797)Termination reason: Instruction limit % 57.88/8.94 % (3071797)Termination phase: Saturation % 57.88/8.94 % (3071797)Time elapsed: 0.269 s % 57.88/8.94 % (3071797)Peak memory usage: 124 MB % 57.88/8.94 % (3071797)Instructions burned: 863 (million) % 57.88/8.94 % (3071803)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=23322979:i=801:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2950 on theBenchmark for (2950ds/801Mi) % 57.88/8.94 % (3071805)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=2457030549:st=5:i=1026:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2950 on theBenchmark for (2950ds/1026Mi) % 57.88/8.94 % (3071805)Refutation not found, incomplete strategy % 57.88/8.94 % (3071805)------------------------------ % 57.88/8.94 % (3071805)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 57.88/8.94 % (3071805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 57.88/8.94 % (3071805)CaDiCaL version: 2.1.3 % 57.88/8.94 % (3071805)Termination reason: Refutation not found, incomplete strategy % 57.88/8.94 % (3071805)Time elapsed: 0.009 s % 57.88/8.94 % (3071805)Peak memory usage: 88 MB % 57.88/8.94 % (3071805)Instructions burned: 16 (million) % 57.88/8.94 % (3071806)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=3252028774:i=3509:rtra=on_2950 on theBenchmark for (2950ds/3509Mi) % 57.88/8.94 % (3071805)------------------------------ % 57.88/8.94 % (3071805)------------------------------ % 57.88/8.94 % (3071810)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=1238383964:st=2:i=2127:sd=12:ep=R:rtra=on:ss=axioms_2946 on theBenchmark for (2946ds/2127Mi) % 57.88/8.94 % (3071810)Refutation not found, incomplete strategy % 57.88/8.94 % (3071810)------------------------------ % 57.88/8.94 % (3071810)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 57.88/8.94 % (3071810)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 57.88/8.94 % (3071810)CaDiCaL version: 2.1.3 % 57.88/8.94 % (3071810)Termination reason: Refutation not found, incomplete strategy % 57.88/8.94 % (3071810)Time elapsed: 0.012 s % 57.88/8.94 % (3071810)Peak memory usage: 88 MB % 57.88/8.94 % (3071810)Instructions burned: 25 (million) % 57.88/8.94 % (3071803)Instruction limit reached! % 57.88/8.94 % (3071803)------------------------------ % 57.88/8.94 % (3071803)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 57.88/8.94 % (3071803)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 57.88/8.94 % (3071803)CaDiCaL version: 2.1.3 % 57.88/8.94 % (3071803)Termination reason: Instruction limit % 57.88/8.94 % (3071803)Termination phase: Saturation % 57.88/8.94 % (3071803)Time elapsed: 0.450 s % 57.88/8.94 % (3071803)Peak memory usage: 98 MB % 57.88/8.94 % (3071803)Instructions burned: 803 (million) % 57.88/8.94 % (3071812)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=1469074010:i=1959:rtra=on:fsd=on:proc=on_2944 on theBenchmark for (2944ds/1959Mi) % 57.88/8.94 % (3071810)------------------------------ % 57.88/8.94 % (3071810)------------------------------ % 57.88/8.94 % (3071814)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=2343505714:s2a=on:i=3553:nm=0:rtra=on_2942 on theBenchmark for (2942ds/3553Mi) % 57.88/8.94 % (3071806)Instruction limit reached! % 57.88/8.94 % (3071806)------------------------------ % 78.61/11.90 % (3071806)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 78.61/11.90 % (3071806)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 78.61/11.90 % (3071806)CaDiCaL version: 2.1.3 % 78.61/11.90 % (3071806)Termination reason: Instruction limit % 78.61/11.90 % (3071806)Termination phase: Saturation % 78.61/11.90 % (3071806)Time elapsed: 0.918 s % 78.61/11.90 % (3071806)Peak memory usage: 109 MB % 78.61/11.90 % (3071806)Instructions burned: 3511 (million) % 78.61/11.90 % (3071816)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=3773812670:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2939 on theBenchmark for (2939ds/3201Mi) % 78.61/11.90 % (3071801)Instruction limit reached! % 78.61/11.90 % (3071801)------------------------------ % 78.61/11.90 % (3071801)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 78.61/11.90 % (3071801)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 78.61/11.90 % (3071801)CaDiCaL version: 2.1.3 % 78.61/11.90 % (3071801)Termination reason: Instruction limit % 78.61/11.90 % (3071801)Termination phase: Saturation % 78.61/11.90 % (3071801)Time elapsed: 1.301 s % 78.61/11.90 % (3071801)Peak memory usage: 137 MB % 78.61/11.90 % (3071801)Instructions burned: 2217 (million) % 78.61/11.90 % (3071818)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=2644655862:thitd=on:cond=on:i=4093:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2937 on theBenchmark for (2937ds/4093Mi) % 78.61/11.90 % (3071812)Instruction limit reached! % 78.61/11.90 % (3071812)------------------------------ % 78.61/11.90 % (3071812)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 78.61/11.90 % (3071812)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 78.61/11.90 % (3071812)CaDiCaL version: 2.1.3 % 78.61/11.90 % (3071812)Termination reason: Instruction limit % 78.61/11.90 % (3071812)Termination phase: Saturation % 78.61/11.90 % (3071812)Time elapsed: 1.228 s % 78.61/11.90 % (3071812)Peak memory usage: 146 MB % 78.61/11.90 % (3071812)Instructions burned: 1960 (million) % 78.61/11.90 % (3071816)Instruction limit reached! % 78.61/11.90 % (3071816)------------------------------ % 78.61/11.90 % (3071816)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 78.61/11.90 % (3071816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 78.61/11.90 % (3071816)CaDiCaL version: 2.1.3 % 78.61/11.90 % (3071816)Termination reason: Instruction limit % 78.61/11.90 % (3071816)Termination phase: Saturation % 78.61/11.90 % (3071816)Time elapsed: 0.765 s % 78.61/11.90 % (3071816)Peak memory usage: 101 MB % 78.61/11.90 % (3071816)Instructions burned: 3201 (million) % 78.61/11.90 % (3071787)Instruction limit reached! % 78.61/11.90 % (3071787)------------------------------ % 78.61/11.90 % (3071787)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 78.61/11.90 % (3071787)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 78.61/11.90 % (3071787)CaDiCaL version: 2.1.3 % 78.61/11.90 % (3071787)Termination reason: Instruction limit % 78.61/11.90 % (3071787)Termination phase: Saturation % 78.61/11.90 % (3071787)Time elapsed: 2.626 s % 78.61/11.90 % (3071787)Peak memory usage: 111 MB % 78.61/11.90 % (3071787)Instructions burned: 6401 (million) % 78.61/11.90 % (3071821)lrs+11_1_to=lpo:thi=all:sas=z3:si=on:fd=off:sac=on:slsq=on:random_seed=149694915:avsq=on:i=10544:avsqr=17,4:canc=force:rtra=on:gtg=exists_top:er=filter_2930 on theBenchmark for (2930ds/10544Mi) % 78.61/11.90 % (3071820)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=163567330:cond=fast:i=21173:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2930 on theBenchmark for (2930ds/21173Mi) % 78.61/11.90 % (3071820)Refutation not found, incomplete strategy % 78.61/11.90 % (3071820)------------------------------ % 78.61/11.90 % (3071820)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 78.61/11.90 % (3071820)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 78.61/11.90 % (3071820)CaDiCaL version: 2.1.3 % 78.61/11.90 % (3071820)Termination reason: Refutation not found, incomplete strategy % 78.61/11.90 % (3071820)Time elapsed: 0.034 s % 78.61/11.90 % (3071820)Peak memory usage: 113 MB % 78.61/11.90 % (3071820)Instructions burned: 19 (million) % 78.61/11.90 % (3071822)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=2249313336:avsq=on:i=1262:avsqr=1,16:rtra=on:rawr=on_2930 on theBenchmark for (2930ds/1262Mi) % 90.26/13.43 % (3071820)------------------------------ % 90.26/13.43 % (3071820)------------------------------ % 90.26/13.43 % (3071826)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=867945405:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2926 on theBenchmark for (2926ds/775Mi) % 90.26/13.43 % (3071826)Refutation not found, incomplete strategy % 90.26/13.43 % (3071826)------------------------------ % 90.26/13.43 % (3071826)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 90.26/13.43 % (3071826)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 90.26/13.43 % (3071826)CaDiCaL version: 2.1.3 % 90.26/13.43 % (3071826)Termination reason: Refutation not found, incomplete strategy % 90.26/13.43 % (3071826)Time elapsed: 0.014 s % 90.26/13.43 % (3071826)Peak memory usage: 88 MB % 90.26/13.43 % (3071826)Instructions burned: 28 (million) % 90.26/13.43 % (3071826)------------------------------ % 90.26/13.43 % (3071826)------------------------------ % 90.26/13.43 % (3071822)Instruction limit reached! % 90.26/13.43 % (3071822)------------------------------ % 90.26/13.43 % (3071822)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 90.26/13.43 % (3071822)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 90.26/13.43 % (3071822)CaDiCaL version: 2.1.3 % 90.26/13.43 % (3071822)Termination reason: Instruction limit % 90.26/13.43 % (3071822)Termination phase: Saturation % 90.26/13.43 % (3071822)Time elapsed: 0.800 s % 90.26/13.43 % (3071822)Peak memory usage: 130 MB % 90.26/13.43 % (3071822)Instructions burned: 1263 (million) % 90.26/13.43 % (3071828)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=914234395:i=270:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2922 on theBenchmark for (2922ds/270Mi) % 90.26/13.43 % (3071798)Instruction limit reached! % 90.26/13.43 % (3071798)------------------------------ % 90.26/13.43 % (3071798)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 90.26/13.43 % (3071798)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 90.26/13.43 % (3071798)CaDiCaL version: 2.1.3 % 90.26/13.43 % (3071798)Termination reason: Instruction limit % 90.26/13.43 % (3071798)Termination phase: Saturation % 90.26/13.43 % (3071798)Time elapsed: 3.184 s % 90.26/13.43 % (3071798)Peak memory usage: 157 MB % 90.26/13.43 % (3071798)Instructions burned: 5811 (million) % 90.26/13.43 % (3071814)Instruction limit reached! % 90.26/13.43 % (3071814)------------------------------ % 90.26/13.43 % (3071814)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 90.26/13.43 % (3071814)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 90.26/13.43 % (3071814)CaDiCaL version: 2.1.3 % 90.26/13.43 % (3071814)Termination reason: Instruction limit % 90.26/13.43 % (3071814)Termination phase: Saturation % 90.26/13.43 % (3071814)Time elapsed: 2.194 s % 90.26/13.43 % (3071814)Peak memory usage: 124 MB % 90.26/13.43 % (3071814)Instructions burned: 3554 (million) % 90.26/13.43 % (3071828)Instruction limit reached! % 90.26/13.43 % (3071828)------------------------------ % 90.26/13.43 % (3071828)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 90.26/13.43 % (3071828)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 90.26/13.43 % (3071828)CaDiCaL version: 2.1.3 % 90.26/13.43 % (3071828)Termination reason: Instruction limit % 90.26/13.43 % (3071828)Termination phase: Saturation % 90.26/13.43 % (3071828)Time elapsed: 0.167 s % 90.26/13.43 % (3071828)Peak memory usage: 93 MB % 90.26/13.43 % (3071828)Instructions burned: 271 (million) % 90.26/13.43 % (3071830)ott+10_128_isp=bottom:to=lpo:sil=128000:si=on:urr=on:uwa=alasca_main:sac=on:slsq=on:random_seed=3350058186:i=17165:aac=none:doe=on:rtra=on:gtg=exists_all_2920 on theBenchmark for (2920ds/17165Mi) % 90.26/13.43 % (3071831)lrs+2_10_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_main:tha=some:random_seed=3163006395:s2a=on:i=13094:s2at=-1:rtra=on_2919 on theBenchmark for (2919ds/13094Mi) % 90.26/13.43 % (3071832)lrs+10_1_to=lpo:sil=128000:si=on:sp=occurrence:random_seed=272150070:st=2:i=12633:rtra=on:ss=axioms_2918 on theBenchmark for (2918ds/12633Mi) % 90.26/13.43 % (3071832)Refutation not found, incomplete strategy % 90.26/13.43 % (3071832)------------------------------ % 90.26/13.43 % (3071832)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 90.26/13.43 % (3071832)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.36/17.21 % (3071832)CaDiCaL version: 2.1.3 % 117.36/17.21 % (3071832)Termination reason: Refutation not found, incomplete strategy % 117.36/17.21 % (3071832)Time elapsed: 0.012 s % 117.36/17.21 % (3071832)Peak memory usage: 88 MB % 117.36/17.21 % (3071832)Instructions burned: 24 (million) % 117.36/17.21 % (3071834)dis+1011_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_frequency:lsd=20:nwc=3:random_seed=1650634658:i=1783:rtra=on:gtg=position_2918 on theBenchmark for (2918ds/1783Mi) % 117.36/17.21 % (3071832)------------------------------ % 117.36/17.21 % (3071832)------------------------------ % 117.36/17.21 % (3071838)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=4077179248:i=5451:aac=none:doe=on:nm=0:rtra=on:amm=off:gtg=position_2914 on theBenchmark for (2914ds/5451Mi) % 117.36/17.21 % (3071818)Instruction limit reached! % 117.36/17.21 % (3071818)------------------------------ % 117.36/17.21 % (3071818)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 117.36/17.21 % (3071818)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.36/17.21 % (3071818)CaDiCaL version: 2.1.3 % 117.36/17.21 % (3071818)Termination reason: Instruction limit % 117.36/17.21 % (3071818)Termination phase: Saturation % 117.36/17.21 % (3071818)Time elapsed: 2.536 s % 117.36/17.21 % (3071818)Peak memory usage: 172 MB % 117.36/17.21 % (3071818)Instructions burned: 4095 (million) % 117.36/17.21 % (3071840)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=3918564302:i=4975:doe=on:nm=0:rtra=on:gtg=exists_sym_2910 on theBenchmark for (2910ds/4975Mi) % 117.36/17.21 % (3071834)Instruction limit reached! % 117.36/17.21 % (3071834)------------------------------ % 117.36/17.21 % (3071834)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 117.36/17.21 % (3071834)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.36/17.21 % (3071834)CaDiCaL version: 2.1.3 % 117.36/17.21 % (3071834)Termination reason: Instruction limit % 117.36/17.21 % (3071834)Termination phase: Saturation % 117.36/17.21 % (3071834)Time elapsed: 1.025 s % 117.36/17.21 % (3071834)Peak memory usage: 129 MB % 117.36/17.21 % (3071834)Instructions burned: 1785 (million) % 117.36/17.21 % (3071842)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=684081921:i=2076:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2906 on theBenchmark for (2906ds/2076Mi) % 117.36/17.21 % (3071821)Instruction limit reached! % 117.36/17.21 % (3071821)------------------------------ % 117.36/17.21 % (3071821)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 117.36/17.21 % (3071821)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.36/17.21 % (3071821)CaDiCaL version: 2.1.3 % 117.36/17.21 % (3071821)Termination reason: Instruction limit % 117.36/17.21 % (3071821)Termination phase: Saturation % 117.36/17.21 % (3071821)Time elapsed: 2.632 s % 117.36/17.21 % (3071821)Peak memory usage: 169 MB % 117.36/17.21 % (3071821)Instructions burned: 10546 (million) % 117.36/17.21 % (3071844)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=3958766261:i=5145:rtra=on_2903 on theBenchmark for (2903ds/5145Mi) % 117.36/17.21 % (3071842)Instruction limit reached! % 117.36/17.21 % (3071842)------------------------------ % 117.36/17.21 % (3071842)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 117.36/17.21 % (3071842)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.36/17.21 % (3071842)CaDiCaL version: 2.1.3 % 117.36/17.21 % (3071842)Termination reason: Instruction limit % 117.36/17.21 % (3071842)Termination phase: Saturation % 117.36/17.21 % (3071842)Time elapsed: 1.205 s % 117.36/17.21 % (3071842)Peak memory usage: 137 MB % 117.36/17.21 % (3071842)Instructions burned: 2076 (million) % 117.36/17.21 % (3071846)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=3188961979:i=3509:rtra=on_2893 on theBenchmark for (2893ds/3509Mi) % 117.36/17.21 % (3071844)Instruction limit reached! % 117.36/17.21 % (3071844)------------------------------ % 117.36/17.21 % (3071844)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 117.36/17.21 % (3071844)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.36/17.21 % (3071844)CaDiCaL version: 2.1.3 % 117.36/17.21 % (3071844)Termination reason: Instruction limit % 117.36/17.21 % (3071844)Termination phase: Saturation % 117.36/17.21 % (3071844)Time elapsed: 1.430 s % 117.36/17.21 % (3071844)Peak memory usage: 125 MB % 117.36/17.21 % (3071844)Instructions burned: 5145 (million) % 187.80/27.18 % (3071848)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=2273222235:st=2:i=13800:sd=12:ep=R:rtra=on:ss=axioms_2887 on theBenchmark for (2887ds/13800Mi) % 187.80/27.18 % (3071848)Refutation not found, incomplete strategy % 187.80/27.18 % (3071848)------------------------------ % 187.80/27.18 % (3071848)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 187.80/27.18 % (3071848)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 187.80/27.18 % (3071848)CaDiCaL version: 2.1.3 % 187.80/27.18 % (3071848)Termination reason: Refutation not found, incomplete strategy % 187.80/27.18 % (3071848)Time elapsed: 0.007 s % 187.80/27.18 % (3071848)Peak memory usage: 88 MB % 187.80/27.18 % (3071848)Instructions burned: 25 (million) % 187.80/27.18 % (3071848)------------------------------ % 187.80/27.18 % (3071848)------------------------------ % 187.80/27.18 % (3071850)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=1687740825:i=1412:rtra=on:fsd=on:proc=on_2885 on theBenchmark for (2885ds/1412Mi) % 187.80/27.18 % (3071838)Instruction limit reached! % 187.80/27.18 % (3071838)------------------------------ % 187.80/27.18 % (3071838)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 187.80/27.18 % (3071838)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 187.80/27.18 % (3071838)CaDiCaL version: 2.1.3 % 187.80/27.18 % (3071838)Termination reason: Instruction limit % 187.80/27.18 % (3071838)Termination phase: Saturation % 187.80/27.18 % (3071838)Time elapsed: 3.080 s % 187.80/27.18 % (3071838)Peak memory usage: 145 MB % 187.80/27.18 % (3071838)Instructions burned: 5452 (million) % 187.80/27.18 % (3071840)Instruction limit reached! % 187.80/27.18 % (3071840)------------------------------ % 187.80/27.18 % (3071840)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 187.80/27.18 % (3071840)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 187.80/27.18 % (3071840)CaDiCaL version: 2.1.3 % 187.80/27.18 % (3071840)Termination reason: Instruction limit % 187.80/27.18 % (3071840)Termination phase: Saturation % 187.80/27.18 % (3071840)Time elapsed: 2.728 s % 187.80/27.18 % (3071840)Peak memory usage: 148 MB % 187.80/27.18 % (3071840)Instructions burned: 4975 (million) % 187.80/27.18 % (3071852)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 % 187.80/27.18 % (3071852)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=3441637682:i=11747:aac=none:nm=0:rtra=on:rawr=on_2882 on theBenchmark for (2882ds/11747Mi) % 187.80/27.18 % (3071853)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=3331208615:s2a=on:i=3553:nm=0:rtra=on_2881 on theBenchmark for (2881ds/3553Mi) % 187.80/27.18 % (3071850)Instruction limit reached! % 187.80/27.18 % (3071850)------------------------------ % 187.80/27.18 % (3071850)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 187.80/27.18 % (3071850)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 187.80/27.18 % (3071850)CaDiCaL version: 2.1.3 % 187.80/27.18 % (3071850)Termination reason: Instruction limit % 187.80/27.18 % (3071850)Termination phase: Saturation % 187.80/27.18 % (3071850)Time elapsed: 0.482 s % 187.80/27.18 % (3071850)Peak memory usage: 139 MB % 187.80/27.18 % (3071850)Instructions burned: 1413 (million) % 187.80/27.18 % (3071856)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=2555797969:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2878 on theBenchmark for (2878ds/3201Mi) % 187.80/27.18 % (3071846)Instruction limit reached! % 187.80/27.18 % (3071846)------------------------------ % 187.80/27.18 % (3071846)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 187.80/27.18 % (3071846)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 187.80/27.18 % (3071846)CaDiCaL version: 2.1.3 % 187.80/27.18 % (3071846)Termination reason: Instruction limit % 187.80/27.18 % (3071846)Termination phase: Saturation % 187.80/27.18 % (3071846)Time elapsed: 1.737 s % 187.80/27.18 % (3071846)Peak memory usage: 109 MB % 187.80/27.18 % (3071846)Instructions burned: 3510 (million) % 187.80/27.18 % (3071858)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=3796717798:thitd=on:cond=on:i=4081:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2874 on theBenchmark for (2874ds/4081Mi) % 217.94/31.41 % (3071856)Instruction limit reached! % 217.94/31.41 % (3071856)------------------------------ % 217.94/31.41 % (3071856)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 217.94/31.41 % (3071856)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 217.94/31.41 % (3071856)CaDiCaL version: 2.1.3 % 217.94/31.41 % (3071856)Termination reason: Instruction limit % 217.94/31.41 % (3071856)Termination phase: Saturation % 217.94/31.41 % (3071856)Time elapsed: 0.760 s % 217.94/31.41 % (3071856)Peak memory usage: 101 MB % 217.94/31.41 % (3071856)Instructions burned: 3202 (million) % 217.94/31.41 % (3071860)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=2157753314:cond=fast:i=20260:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2870 on theBenchmark for (2870ds/20260Mi) % 217.94/31.41 % (3071860)Refutation not found, incomplete strategy % 217.94/31.41 % (3071860)------------------------------ % 217.94/31.41 % (3071860)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 217.94/31.41 % (3071860)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 217.94/31.41 % (3071860)CaDiCaL version: 2.1.3 % 217.94/31.41 % (3071860)Termination reason: Refutation not found, incomplete strategy % 217.94/31.41 % (3071860)Time elapsed: 0.020 s % 217.94/31.41 % (3071860)Peak memory usage: 113 MB % 217.94/31.41 % (3071860)Instructions burned: 19 (million) % 217.94/31.41 % (3071860)------------------------------ % 217.94/31.41 % (3071860)------------------------------ % 217.94/31.41 % (3071863)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=306494059:s2a=on:i=58627:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2867 on theBenchmark for (2867ds/58627Mi) % 217.94/31.41 % (3071831)Instruction limit reached! % 217.94/31.41 % (3071831)------------------------------ % 217.94/31.41 % (3071831)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 217.94/31.41 % (3071831)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 217.94/31.41 % (3071831)CaDiCaL version: 2.1.3 % 217.94/31.41 % (3071831)Termination reason: Instruction limit % 217.94/31.41 % (3071831)Termination phase: Saturation % 217.94/31.41 % (3071831)Time elapsed: 5.313 s % 217.94/31.41 % (3071831)Peak memory usage: 121 MB % 217.94/31.41 % (3071831)Instructions burned: 13096 (million) % 217.94/31.41 % (3071866)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=3302565154:avsq=on:i=6258:avsqr=1,16:rtra=on:rawr=on_2864 on theBenchmark for (2864ds/6258Mi) % 217.94/31.41 % (3071853)Instruction limit reached! % 217.94/31.41 % (3071853)------------------------------ % 217.94/31.41 % (3071853)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 217.94/31.41 % (3071853)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 217.94/31.41 % (3071853)CaDiCaL version: 2.1.3 % 217.94/31.41 % (3071853)Termination reason: Instruction limit % 217.94/31.41 % (3071853)Termination phase: Saturation % 217.94/31.41 % (3071853)Time elapsed: 2.190 s % 217.94/31.41 % (3071853)Peak memory usage: 125 MB % 217.94/31.41 % (3071853)Instructions burned: 3554 (million) % 217.94/31.41 % (3071912)ott+10_128_isp=bottom:to=lpo:sil=128000:si=on:urr=on:uwa=alasca_main:sac=on:slsq=on:random_seed=2015793251:i=34001:aac=none:doe=on:rtra=on:gtg=exists_all_2858 on theBenchmark for (2858ds/34001Mi) % 217.94/31.41 % (3071858)Instruction limit reached! % 217.94/31.41 % (3071858)------------------------------ % 217.94/31.41 % (3071858)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 217.94/31.41 % (3071858)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 217.94/31.41 % (3071858)CaDiCaL version: 2.1.3 % 217.94/31.41 % (3071858)Termination reason: Instruction limit % 217.94/31.41 % (3071858)Termination phase: Saturation % 217.94/31.41 % (3071858)Time elapsed: 2.498 s % 217.94/31.41 % (3071858)Peak memory usage: 174 MB % 217.94/31.41 % (3071858)Instructions burned: 4082 (million) % 217.94/31.41 % (3071915)lrs+2_10_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_main:tha=some:random_seed=3767846857:s2a=on:i=71622:s2at=-1:rtra=on_2847 on theBenchmark for (2847ds/71622Mi) % 217.94/31.41 % (3071830)Instruction limit reached! % 217.94/31.41 % (3071830)------------------------------ % 217.94/31.41 % (3071830)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 217.94/31.41 % (3071830)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 217.94/31.41 % (3071830)CaDiCaL version: 2.1.3 % 217.94/31.41 % (3071830)Termination reason: Instruction limit % 217.94/31.41 % (3071830)Termination phase: Saturation % 248.71/35.76 % (3071830)Time elapsed: 8.407 s % 248.71/35.76 % (3071830)Peak memory usage: 156 MB % 248.71/35.76 % (3071830)Instructions burned: 17166 (million) % 248.71/35.76 % (3071917)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=1470199654:i=24001:kws=precedence:nm=0:rtra=on_2834 on theBenchmark for (2834ds/24001Mi) % 248.71/35.76 % (3071866)Instruction limit reached! % 248.71/35.76 % (3071866)------------------------------ % 248.71/35.76 % (3071866)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 248.71/35.76 % (3071866)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 248.71/35.76 % (3071866)CaDiCaL version: 2.1.3 % 248.71/35.76 % (3071866)Termination reason: Instruction limit % 248.71/35.76 % (3071866)Termination phase: Saturation % 248.71/35.76 % (3071866)Time elapsed: 3.236 s % 248.71/35.76 % (3071866)Peak memory usage: 150 MB % 248.71/35.76 % (3071866)Instructions burned: 6259 (million) % 248.71/35.76 % (3071919)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=3265047760:i=2076:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2830 on theBenchmark for (2830ds/2076Mi) % 248.71/35.77 % (3071919)Instruction limit reached! % 248.71/35.77 % (3071919)------------------------------ % 248.71/35.77 % (3071919)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 248.71/35.77 % (3071919)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 248.71/35.77 % (3071919)CaDiCaL version: 2.1.3 % 248.71/35.77 % (3071919)Termination reason: Instruction limit % 248.71/35.77 % (3071919)Termination phase: Saturation % 248.71/35.77 % (3071919)Time elapsed: 1.223 s % 248.71/35.77 % (3071919)Peak memory usage: 137 MB % 248.71/35.77 % (3071919)Instructions burned: 2077 (million) % 248.71/35.77 % (3071921)dis+21_20_to=lakbo:si=on:alasca=on:sp=const_max:uwa=alasca_main:sac=on:random_seed=1209193008:s2a=on:i=83971:s2at=4:bd=all:ins=1:rtra=on_2816 on theBenchmark for (2816ds/83971Mi) % 248.71/35.77 % (3071852)Instruction limit reached! % 248.71/35.77 % (3071852)------------------------------ % 248.71/35.77 % (3071852)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 248.71/35.77 % (3071852)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 248.71/35.77 % (3071852)CaDiCaL version: 2.1.3 % 248.71/35.77 % (3071852)Termination reason: Instruction limit % 248.71/35.77 % (3071852)Termination phase: Saturation % 248.71/35.77 % (3071852)Time elapsed: 7.093 s % 248.71/35.77 % (3071852)Peak memory usage: 228 MB % 248.71/35.77 % (3071852)Instructions burned: 11748 (million) % 248.71/35.77 % (3071923)lrs+1011_5:1_to=lpo:sil=128000:sas=z3:si=on:norm_ineq=on:tha=some:random_seed=1761852750:i=83944:rtra=on_2809 on theBenchmark for (2809ds/83944Mi) % 248.71/35.77 % (3071791)Instruction limit reached! % 248.71/35.77 % (3071791)------------------------------ % 248.71/35.77 % (3071791)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 248.71/35.77 % (3071791)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 248.71/35.77 % (3071791)CaDiCaL version: 2.1.3 % 248.71/35.77 % (3071791)Termination reason: Instruction limit % 248.71/35.77 % (3071791)Termination phase: Saturation % 248.71/35.77 % (3071791)Time elapsed: 17.947 s % 248.71/35.77 % (3071791)Peak memory usage: 171 MB % 248.71/35.77 % (3071791)Instructions burned: 36817 (million) % 248.71/35.77 % (3071925)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=3790304366:i=9201:rtra=on_2775 on theBenchmark for (2775ds/9201Mi) % 248.71/35.77 % (3071925)Instruction limit reached! % 248.71/35.77 % (3071925)------------------------------ % 248.71/35.77 % (3071925)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 248.71/35.77 % (3071925)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 248.71/35.77 % (3071925)CaDiCaL version: 2.1.3 % 248.71/35.77 % (3071925)Termination reason: Instruction limit % 248.71/35.77 % (3071925)Termination phase: Saturation % 248.71/35.77 % (3071925)Time elapsed: 3.733 s % 248.71/35.77 % (3071925)Peak memory usage: 116 MB % 248.71/35.77 % (3071925)Instructions burned: 9202 (million) % 248.71/35.77 % (3071927)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 % 248.71/35.77 % (3071927)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=680870405:i=6806:aac=none:nm=0:rtra=on:rawr=on_2736 on theBenchmark for (2736ds/6806Mi) % 260.60/37.45 % (3071863)Instruction limit reached! % 260.60/37.45 % (3071863)------------------------------ % 260.60/37.45 % (3071863)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 260.60/37.45 % (3071863)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 260.60/37.45 % (3071863)CaDiCaL version: 2.1.3 % 260.60/37.45 % (3071863)Termination reason: Instruction limit % 260.60/37.45 % (3071863)Termination phase: Saturation % 260.60/37.45 % (3071863)Time elapsed: 15.763 s % 260.60/37.45 % (3071863)Peak memory usage: 224 MB % 260.60/37.45 % (3071863)Instructions burned: 58628 (million) % 260.60/37.45 % (3071931)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=2115669600:s2a=on:i=3553:nm=0:rtra=on_2708 on theBenchmark for (2708ds/3553Mi) % 260.60/37.45 % (3071917)Instruction limit reached! % 260.60/37.45 % (3071917)------------------------------ % 260.60/37.45 % (3071917)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 260.60/37.45 % (3071917)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 260.60/37.45 % (3071917)CaDiCaL version: 2.1.3 % 260.60/37.45 % (3071917)Termination reason: Instruction limit % 260.60/37.45 % (3071917)Termination phase: Saturation % 260.60/37.45 % (3071917)Time elapsed: 12.817 s % 260.60/37.45 % (3071917)Peak memory usage: 271 MB % 260.60/37.45 % (3071917)Instructions burned: 24001 (million) % 260.60/37.45 % (3071912)Instruction limit reached! % 260.60/37.45 % (3071912)------------------------------ % 260.60/37.45 % (3071912)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 260.60/37.45 % (3071912)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 260.60/37.45 % (3071912)CaDiCaL version: 2.1.3 % 260.60/37.45 % (3071912)Termination reason: Instruction limit % 260.60/37.45 % (3071912)Termination phase: Saturation % 260.60/37.45 % (3071912)Time elapsed: 15.306 s % 260.60/37.45 % (3071912)Peak memory usage: 549 MB % 260.60/37.45 % (3071912)Instructions burned: 34003 (million) % 260.60/37.45 % (3071933)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=3265055917:thitd=on:cond=on:i=2064:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2704 on theBenchmark for (2704ds/2064Mi) % 260.60/37.45 % (3071934)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=2674309688:cond=fast:i=20260:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2702 on theBenchmark for (2702ds/20260Mi) % 260.60/37.45 % (3071934)Refutation not found, incomplete strategy % 260.60/37.45 % (3071934)------------------------------ % 260.60/37.45 % (3071934)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 260.60/37.45 % (3071934)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 260.60/37.45 % (3071934)CaDiCaL version: 2.1.3 % 260.60/37.45 % (3071934)Termination reason: Refutation not found, incomplete strategy % 260.60/37.45 % (3071934)Time elapsed: 0.034 s % 260.60/37.45 % (3071934)Peak memory usage: 113 MB % 260.60/37.45 % (3071934)Instructions burned: 19 (million) % 260.60/37.45 % (3071934)------------------------------ % 260.60/37.45 % (3071934)------------------------------ % 260.60/37.45 % (3071937)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=101813981:avsq=on:i=1244:avsqr=1,16:rtra=on:rawr=on_2698 on theBenchmark for (2698ds/1244Mi) % 260.60/37.45 % (3071931)Instruction limit reached! % 260.60/37.45 % (3071931)------------------------------ % 260.60/37.45 % (3071931)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 260.60/37.45 % (3071931)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 260.60/37.45 % (3071931)CaDiCaL version: 2.1.3 % 260.60/37.45 % (3071931)Termination reason: Instruction limit % 260.60/37.45 % (3071931)Termination phase: Saturation % 260.60/37.45 % (3071931)Time elapsed: 1.180 s % 260.60/37.45 % (3071931)Peak memory usage: 124 MB % 260.60/37.45 % (3071931)Instructions burned: 3556 (million) % 260.60/37.45 % (3071939)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=1852797233:i=58261:doe=on:nm=0:rtra=on:gtg=exists_sym_2695 on theBenchmark for (2695ds/58261Mi) % 260.60/37.45 % (3071927)Instruction limit reached! % 260.60/37.45 % (3071927)------------------------------ % 260.60/37.45 % (3071927)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 260.60/37.45 % (3071927)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 260.60/37.45 % (3071927)CaDiCaL version: 2.1.3 % 269.90/38.75 % (3071927)Termination reason: Instruction limit % 269.90/38.75 % (3071927)Termination phase: Saturation % 269.90/38.75 % (3071927)Time elapsed: 4.234 s % 269.90/38.75 % (3071927)Peak memory usage: 192 MB % 269.90/38.75 % (3071927)Instructions burned: 6806 (million) % 269.90/38.75 % (3071941)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 % 269.90/38.75 % (3071941)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=2977555754:i=6806:aac=none:nm=0:rtra=on:rawr=on_2692 on theBenchmark for (2692ds/6806Mi) % 269.90/38.75 % (3071933)Instruction limit reached! % 269.90/38.75 % (3071933)------------------------------ % 269.90/38.75 % (3071933)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 269.90/38.75 % (3071933)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.90/38.75 % (3071933)CaDiCaL version: 2.1.3 % 269.90/38.75 % (3071933)Termination reason: Instruction limit % 269.90/38.75 % (3071933)Termination phase: Saturation % 269.90/38.75 % (3071933)Time elapsed: 1.308 s % 269.90/38.75 % (3071933)Peak memory usage: 154 MB % 269.90/38.75 % (3071933)Instructions burned: 2065 (million) % 269.90/38.75 % (3071937)Instruction limit reached! % 269.90/38.75 % (3071937)------------------------------ % 269.90/38.75 % (3071937)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 269.90/38.75 % (3071937)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.90/38.75 % (3071937)CaDiCaL version: 2.1.3 % 269.90/38.75 % (3071937)Termination reason: Instruction limit % 269.90/38.75 % (3071937)Termination phase: Saturation % 269.90/38.75 % (3071937)Time elapsed: 0.783 s % 269.90/38.75 % (3071937)Peak memory usage: 131 MB % 269.90/38.75 % (3071937)Instructions burned: 1245 (million) % 269.90/38.75 % (3071943)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=2152281085:thitd=on:cond=on:i=4081:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2689 on theBenchmark for (2689ds/4081Mi) % 269.90/38.75 % (3071944)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=3069640791:avsq=on:i=1701:avsqr=1,16:rtra=on:rawr=on_2688 on theBenchmark for (2688ds/1701Mi) % 269.90/38.75 % (3071944)Instruction limit reached! % 269.90/38.75 % (3071944)------------------------------ % 269.90/38.75 % (3071944)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 269.90/38.75 % (3071944)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.90/38.75 % (3071944)CaDiCaL version: 2.1.3 % 269.90/38.75 % (3071944)Termination reason: Instruction limit % 269.90/38.75 % (3071944)Termination phase: Saturation % 269.90/38.75 % (3071944)Time elapsed: 1.050 s % 269.90/38.75 % (3071944)Peak memory usage: 135 MB % 269.90/38.75 % (3071944)Instructions burned: 1701 (million) % 269.90/38.75 % (3071947)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=3847325859:i=57001:doe=on:nm=0:rtra=on:gtg=exists_sym_2676 on theBenchmark for (2676ds/57001Mi) % 269.90/38.75 % (3071943)Instruction limit reached! % 269.90/38.75 % (3071943)------------------------------ % 269.90/38.75 % (3071943)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 269.90/38.75 % (3071943)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.90/38.75 % (3071943)CaDiCaL version: 2.1.3 % 269.90/38.75 % (3071943)Termination reason: Instruction limit % 269.90/38.75 % (3071943)Termination phase: Saturation % 269.90/38.75 % (3071943)Time elapsed: 2.426 s % 269.90/38.75 % (3071943)Peak memory usage: 166 MB % 269.90/38.75 % (3071943)Instructions burned: 4082 (million) % 269.90/38.75 % (3071949)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 % 269.90/38.75 % (3071949)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=2866956313:i=8622:aac=none:nm=0:rtra=on:rawr=on_2663 on theBenchmark for (2663ds/8622Mi) % 269.90/38.75 % (3071941)Instruction limit reached! % 269.90/38.75 % (3071941)------------------------------ % 269.90/38.75 % (3071941)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 269.90/38.75 % (3071941)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 277.75/39.89 % (3071941)CaDiCaL version: 2.1.3 % 277.75/39.89 % (3071941)Termination reason: Instruction limit % 277.75/39.89 % (3071941)Termination phase: Saturation % 277.75/39.89 % (3071941)Time elapsed: 4.181 s % 277.75/39.89 % (3071941)Peak memory usage: 188 MB % 277.75/39.89 % (3071941)Instructions burned: 6807 (million) % 277.75/39.89 % (3071951)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=2709511727:i=24:doe=on:rtra=on:gtg=exists_top:ss=axioms_2648 on theBenchmark for (2648ds/24Mi) % 277.75/39.89 % (3071951)Instruction limit reached! % 277.75/39.89 % (3071951)------------------------------ % 277.75/39.89 % (3071951)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 277.75/39.89 % (3071951)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 277.75/39.89 % (3071951)CaDiCaL version: 2.1.3 % 277.75/39.89 % (3071951)Termination reason: Instruction limit % 277.75/39.89 % (3071951)Termination phase: Property scanning % 277.75/39.89 % (3071951)Time elapsed: 0.011 s % 277.75/39.89 % (3071951)Peak memory usage: 86 MB % 277.75/39.89 % (3071951)Instructions burned: 24 (million) % 277.75/39.89 % (3071953)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=833039989:i=614:kws=precedence:nm=0:rtra=on_2647 on theBenchmark for (2647ds/614Mi) % 277.75/39.89 % (3071953)Instruction limit reached! % 277.75/39.89 % (3071953)------------------------------ % 277.75/39.89 % (3071953)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 277.75/39.89 % (3071953)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 277.75/39.89 % (3071953)CaDiCaL version: 2.1.3 % 277.75/39.89 % (3071953)Termination reason: Instruction limit % 277.75/39.89 % (3071953)Termination phase: Saturation % 277.75/39.89 % (3071953)Time elapsed: 0.347 s % 277.75/39.89 % (3071953)Peak memory usage: 122 MB % 277.75/39.89 % (3071953)Instructions burned: 615 (million) % 277.75/39.89 % (3071955)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=1416316155:i=402:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2642 on theBenchmark for (2642ds/402Mi) % 277.75/39.89 % (3071955)Instruction limit reached! % 277.75/39.89 % (3071955)------------------------------ % 277.75/39.89 % (3071955)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 277.75/39.89 % (3071955)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 277.75/39.89 % (3071955)CaDiCaL version: 2.1.3 % 277.75/39.89 % (3071955)Termination reason: Instruction limit % 277.75/39.89 % (3071955)Termination phase: Saturation % 277.75/39.89 % (3071955)Time elapsed: 0.257 s % 277.75/39.89 % (3071955)Peak memory usage: 120 MB % 277.75/39.89 % (3071955)Instructions burned: 403 (million) % 277.75/39.89 % (3071957)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=2071441206:s2a=on:i=14:rtra=on:inst=on_2637 on theBenchmark for (2637ds/14Mi) % 277.75/39.89 % (3071957)Instruction limit reached! % 277.75/39.89 % (3071957)------------------------------ % 277.75/39.89 % (3071957)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 277.75/39.89 % (3071957)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 277.75/39.89 % (3071957)CaDiCaL version: 2.1.3 % 277.75/39.89 % (3071957)Termination reason: Instruction limit % 277.75/39.89 % (3071957)Termination phase: Property scanning % 277.75/39.89 % (3071957)Time elapsed: 0.008 s % 277.75/39.89 % (3071957)Peak memory usage: 86 MB % 277.75/39.89 % (3071957)Instructions burned: 16 (million) % 277.75/39.89 % (3071959)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=1989697642:i=8:rtra=on_2636 on theBenchmark for (2636ds/8Mi) % 277.75/39.89 % (3071959)Instruction limit reached! % 277.75/39.89 % (3071959)------------------------------ % 277.75/39.89 % (3071959)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 277.75/39.89 % (3071959)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 277.75/39.89 % (3071959)CaDiCaL version: 2.1.3 % 277.75/39.89 % (3071959)Termination reason: Instruction limit % 277.75/39.89 % (3071959)Termination phase: Property scanning % 277.75/39.89 % (3071959)Time elapsed: 0.005 s % 277.75/39.89 % (3071959)Peak memory usage: 86 MB % 277.75/39.89 % (3071959)Instructions burned: 10 (million) % 277.75/39.89 % (3071961)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=1758912275:i=92:rtra=on_2634 on theBenchmark for (2634ds/92Mi) % 277.75/39.89 % (3071961)Instruction limit reached! % 277.75/39.89 % (3071961)------------------------------ % 277.75/39.89 % (3071961)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 277.75/39.89 % (3071961)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 281.81/40.47 % (3071961)CaDiCaL version: 2.1.3 % 281.81/40.47 % (3071961)Termination reason: Instruction limit % 281.81/40.47 % (3071961)Termination phase: Saturation % 281.81/40.47 % (3071961)Time elapsed: 0.069 s % 281.81/40.47 % (3071961)Peak memory usage: 114 MB % 281.81/40.47 % (3071961)Instructions burned: 93 (million) % 281.81/40.47 % (3071963)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=423388433:i=66:rtra=on_2632 on theBenchmark for (2632ds/66Mi) % 281.81/40.47 % (3071963)Instruction limit reached! % 281.81/40.47 % (3071963)------------------------------ % 281.81/40.47 % (3071963)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 281.81/40.47 % (3071963)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 281.81/40.47 % (3071963)CaDiCaL version: 2.1.3 % 281.81/40.47 % (3071963)Termination reason: Instruction limit % 281.81/40.47 % (3071963)Termination phase: Saturation % 281.81/40.47 % (3071963)Time elapsed: 0.031 s % 281.81/40.47 % (3071963)Peak memory usage: 88 MB % 281.81/40.47 % (3071963)Instructions burned: 67 (million) % 281.81/40.47 % (3071965)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=2187318804:st=5:i=28:sd=10:rtra=on:ss=axioms:rawr=on_2630 on theBenchmark for (2630ds/28Mi) % 281.81/40.47 % (3071965)Refutation not found, incomplete strategy % 281.81/40.47 % (3071965)------------------------------ % 281.81/40.47 % (3071965)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 281.81/40.47 % (3071965)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 281.81/40.47 % (3071965)CaDiCaL version: 2.1.3 % 281.81/40.47 % (3071965)Termination reason: Refutation not found, incomplete strategy % 281.81/40.47 % (3071965)Time elapsed: 0.009 s % 281.81/40.47 % (3071965)Peak memory usage: 88 MB % 281.81/40.47 % (3071965)Instructions burned: 16 (million) % 281.81/40.47 % (3071965)------------------------------ % 281.81/40.47 % (3071965)------------------------------ % 281.81/40.47 % (3071967)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=3267647799:i=58:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2626 on theBenchmark for (2626ds/58Mi) % 281.81/40.47 % (3071967)Instruction limit reached! % 281.81/40.47 % (3071967)------------------------------ % 281.81/40.47 % (3071967)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 281.81/40.47 % (3071967)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 281.81/40.47 % (3071967)CaDiCaL version: 2.1.3 % 281.81/40.47 % (3071967)Termination reason: Instruction limit % 281.81/40.47 % (3071967)Termination phase: Property scanning % 281.81/40.47 % (3071967)Time elapsed: 0.027 s % 281.81/40.47 % (3071967)Peak memory usage: 88 MB % 281.81/40.47 % (3071967)Instructions burned: 59 (million) % 281.81/40.47 % (3071969)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=1539106985:cond=on:i=32:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2624 on theBenchmark for (2624ds/32Mi) % 281.81/40.47 % (3071969)Instruction limit reached! % 281.81/40.47 % (3071969)------------------------------ % 281.81/40.47 % (3071969)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 281.81/40.47 % (3071969)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 281.81/40.47 % (3071969)CaDiCaL version: 2.1.3 % 281.81/40.47 % (3071969)Termination reason: Instruction limit % 281.81/40.47 % (3071969)Termination phase: Property scanning % 281.81/40.47 % (3071969)Time elapsed: 0.017 s % 281.81/40.47 % (3071969)Peak memory usage: 87 MB % 281.81/40.47 % (3071969)Instructions burned: 32 (million) % 281.81/40.47 % (3071971)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=4175818578:i=48:canc=force:rtra=on_2622 on theBenchmark for (2622ds/48Mi) % 281.81/40.47 % (3071971)Instruction limit reached! % 281.81/40.47 % (3071971)------------------------------ % 281.81/40.47 % (3071971)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 281.81/40.47 % (3071971)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 281.81/40.47 % (3071971)CaDiCaL version: 2.1.3 % 281.81/40.47 % (3071971)Termination reason: Instruction limit % 281.81/40.47 % (3071971)Termination phase: Property scanning % 281.81/40.47 % (3071971)Time elapsed: 0.024 s % 281.81/40.47 % (3071971)Peak memory usage: 87 MB % 281.81/40.47 % (3071971)Instructions burned: 49 (million) % 281.81/40.47 % (3071973)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=1225825074:i=54:canc=cautious:fsr=off:rtra=on_2620 on theBenchmark for (2620ds/54Mi) % 286.53/41.06 % (3071973)Instruction limit reached! % 286.53/41.06 % (3071973)------------------------------ % 286.53/41.06 % (3071973)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 286.53/41.06 % (3071973)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 286.53/41.06 % (3071973)CaDiCaL version: 2.1.3 % 286.53/41.06 % (3071973)Termination reason: Instruction limit % 286.53/41.06 % (3071973)Termination phase: Property scanning % 286.53/41.06 % (3071973)Time elapsed: 0.027 s % 286.53/41.06 % (3071973)Peak memory usage: 88 MB % 286.53/41.06 % (3071973)Instructions burned: 56 (million) % 286.53/41.06 % (3071975)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=666678414:i=170:gtgl=4:rtra=on:gtg=exists_sym_2618 on theBenchmark for (2618ds/170Mi) % 286.53/41.06 % (3071975)Instruction limit reached! % 286.53/41.06 % (3071975)------------------------------ % 286.53/41.06 % (3071975)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 286.53/41.06 % (3071975)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 286.53/41.06 % (3071975)CaDiCaL version: 2.1.3 % 286.53/41.06 % (3071975)Termination reason: Instruction limit % 286.53/41.06 % (3071975)Termination phase: Saturation % 286.53/41.06 % (3071975)Time elapsed: 0.082 s % 286.53/41.06 % (3071975)Peak memory usage: 90 MB % 286.53/41.06 % (3071975)Instructions burned: 171 (million) % 286.53/41.06 % (3071977)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=1580307564:i=4:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2616 on theBenchmark for (2616ds/4Mi) % 286.53/41.06 % (3071977)Instruction limit reached! % 286.53/41.06 % (3071977)------------------------------ % 286.53/41.06 % (3071977)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 286.53/41.06 % (3071977)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 286.53/41.06 % (3071977)CaDiCaL version: 2.1.3 % 286.53/41.06 % (3071977)Termination reason: Instruction limit % 286.53/41.06 % (3071977)Termination phase: Property scanning % 286.53/41.06 % (3071977)Time elapsed: 0.003 s % 286.53/41.06 % (3071977)Peak memory usage: 86 MB % 286.53/41.06 % (3071977)Instructions burned: 5 (million) % 286.53/41.06 % (3071979)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=1467851228:i=362:rtra=on:ss=axioms:ev=cautious_2614 on theBenchmark for (2614ds/362Mi) % 286.53/41.06 % (3071979)Refutation not found, incomplete strategy % 286.53/41.06 % (3071979)------------------------------ % 286.53/41.06 % (3071979)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 286.53/41.06 % (3071979)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 286.53/41.06 % (3071979)CaDiCaL version: 2.1.3 % 286.53/41.06 % (3071979)Termination reason: Refutation not found, incomplete strategy % 286.53/41.06 % (3071979)Time elapsed: 0.008 s % 286.53/41.06 % (3071979)Peak memory usage: 88 MB % 286.53/41.06 % (3071979)Instructions burned: 15 (million) % 286.53/41.06 % (3071979)------------------------------ % 286.53/41.06 % (3071979)------------------------------ % 286.53/41.06 % (3071981)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=484178590:i=8:ep=RST:ins=2:rtra=on_2610 on theBenchmark for (2610ds/8Mi) % 286.53/41.06 % (3071981)Instruction limit reached! % 286.53/41.06 % (3071981)------------------------------ % 286.53/41.06 % (3071981)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 286.53/41.06 % (3071981)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 286.53/41.06 % (3071981)CaDiCaL version: 2.1.3 % 286.53/41.06 % (3071981)Termination reason: Instruction limit % 286.53/41.06 % (3071981)Termination phase: Property scanning % 286.53/41.06 % (3071981)Time elapsed: 0.005 s % 286.53/41.06 % (3071981)Peak memory usage: 86 MB % 286.53/41.06 % (3071981)Instructions burned: 10 (million) % 286.53/41.06 % (3071949)Instruction limit reached! % 286.53/41.06 % (3071949)------------------------------ % 286.53/41.06 % (3071949)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 286.53/41.06 % (3071949)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 286.53/41.06 % (3071949)CaDiCaL version: 2.1.3 % 286.53/41.06 % (3071949)Termination reason: Instruction limit % 286.53/41.06 % (3071949)Termination phase: Saturation % 286.53/41.06 % (3071949)Time elapsed: 5.334 s % 286.53/41.06 % (3071949)Peak memory usage: 213 MB % 286.53/41.06 % (3071949)Instructions burned: 8623 (million) % 286.53/41.06 % (3071983)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=2326988496:i=132:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2609 on theBenchmark for (2609ds/132Mi) % 293.63/42.06 % (3071984)lrs+10_1_thi=all:si=on:fd=off:random_seed=3686848851:i=106:rtra=on:gtg=all_2608 on theBenchmark for (2608ds/106Mi) % 293.63/42.06 % (3071983)Instruction limit reached! % 293.63/42.06 % (3071983)------------------------------ % 293.63/42.06 % (3071983)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 293.63/42.06 % (3071983)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 293.63/42.06 % (3071983)CaDiCaL version: 2.1.3 % 293.63/42.06 % (3071983)Termination reason: Instruction limit % 293.63/42.06 % (3071983)Termination phase: Saturation % 293.63/42.06 % (3071983)Time elapsed: 0.113 s % 293.63/42.06 % (3071983)Peak memory usage: 137 MB % 293.63/42.06 % (3071983)Instructions burned: 135 (million) % 293.63/42.06 % (3071984)Instruction limit reached! % 293.63/42.06 % (3071984)------------------------------ % 293.63/42.06 % (3071984)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 293.63/42.06 % (3071984)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 293.63/42.06 % (3071984)CaDiCaL version: 2.1.3 % 293.63/42.06 % (3071984)Termination reason: Instruction limit % 293.63/42.06 % (3071984)Termination phase: Saturation % 293.63/42.06 % (3071984)Time elapsed: 0.071 s % 293.63/42.06 % (3071984)Peak memory usage: 115 MB % 293.63/42.06 % (3071984)Instructions burned: 107 (million) % 293.63/42.06 % (3071987)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=1690834988:i=16:ep=RST:nm=16:rtra=on:gtg=exists_top_2606 on theBenchmark for (2606ds/16Mi) % 293.63/42.06 % (3071987)Instruction limit reached! % 293.63/42.06 % (3071987)------------------------------ % 293.63/42.06 % (3071987)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 293.63/42.06 % (3071987)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 293.63/42.06 % (3071987)CaDiCaL version: 2.1.3 % 293.63/42.06 % (3071987)Termination reason: Instruction limit % 293.63/42.06 % (3071987)Termination phase: Property scanning % 293.63/42.06 % (3071987)Time elapsed: 0.008 s % 293.63/42.06 % (3071987)Peak memory usage: 85 MB % 293.63/42.06 % (3071987)Instructions burned: 17 (million) % 293.63/42.06 % (3071988)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=4196488730:st=3:i=4:rtra=on:ss=axioms_2606 on theBenchmark for (2606ds/4Mi) % 293.63/42.06 % (3071988)Instruction limit reached! % 293.63/42.06 % (3071988)------------------------------ % 293.63/42.06 % (3071988)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 293.63/42.06 % (3071988)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 293.63/42.06 % (3071988)CaDiCaL version: 2.1.3 % 293.63/42.06 % (3071988)Termination reason: Instruction limit % 293.63/42.06 % (3071988)Termination phase: Property scanning % 293.63/42.06 % (3071988)Time elapsed: 0.003 s % 293.63/42.06 % (3071988)Peak memory usage: 86 MB % 293.63/42.06 % (3071988)Instructions burned: 5 (million) % 293.63/42.06 % (3071990)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=490067398:i=4:doe=on:canc=force:asg=cautious:rtra=on_2605 on theBenchmark for (2605ds/4Mi) % 293.63/42.06 % (3071990)Instruction limit reached! % 293.63/42.06 % (3071990)------------------------------ % 293.63/42.06 % (3071990)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 293.63/42.06 % (3071990)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 293.63/42.06 % (3071990)CaDiCaL version: 2.1.3 % 293.63/42.06 % (3071990)Termination reason: Instruction limit % 293.63/42.06 % (3071990)Termination phase: Property scanning % 293.63/42.06 % (3071990)Time elapsed: 0.003 s % 293.63/42.06 % (3071990)Peak memory usage: 86 MB % 293.63/42.06 % (3071990)Instructions burned: 4 (million) % 293.63/42.06 % (3071992)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=2090797883:i=254:doe=on:rtra=on_2604 on theBenchmark for (2604ds/254Mi) % 293.63/42.06 % (3071994)dis+10_1_si=on:random_seed=4013868934:i=20:ep=R:rtra=on_2603 on theBenchmark for (2603ds/20Mi) % 293.63/42.06 % (3071994)Instruction limit reached! % 293.63/42.06 % (3071994)------------------------------ % 293.63/42.06 % (3071994)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 293.63/42.06 % (3071994)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 293.63/42.06 % (3071994)CaDiCaL version: 2.1.3 % 293.63/42.06 % (3071994)Termination reason: Instruction limit % 293.63/42.06 % (3071994)Termination phase: Preprocessing 1 % 293.63/42.06 % (3071994)Time elapsed: 0.009 s % 293.63/42.06 % (3071994)Peak memory usage: 86 MB % 293.63/42.06 % (3071994)Instructions burned: 21 (millioTerminated %------------------------------------------------------------------------------