%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : NUM879_1 : TPTP v9.3.1. Released v5.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % Computer : n001.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 12:17:21 PM UTC 2026 % Result : Timeout 293.05s 42.16s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : NUM879_1 : TPTP v9.3.1. Released v5.0.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.13/0.39 % Computer : n001.cluster.edu % 0.13/0.39 % Model : x86_64 x86_64 % 0.13/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.39 % Memory : 8046.5625MB % 0.13/0.39 % OS : Linux 6.8.0-71-generic % 0.13/0.39 % CPULimit : 300 % 0.13/0.39 % WCLimit : 300 % 0.13/0.39 % DateTime : Sun Sep 27 21:43:02 UTC 2026 % 0.13/0.39 % CPUTime : % 0.13/0.39 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.13/0.43 Running first-order theorem proving % 0.13/0.43 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 3.87/1.48 % (3978983)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule. % 3.87/1.48 % (3979078)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=573132434:i=46:rtra=on_3000 on theBenchmark for (3000ds/46Mi) % 3.87/1.48 % (3979078)Refutation not found, incomplete strategy % 3.87/1.48 % (3979078)------------------------------ % 3.87/1.48 % (3979078)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.87/1.48 % (3979078)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.87/1.48 % (3979078)CaDiCaL version: 2.1.3 % 3.87/1.48 % (3979078)Termination reason: Refutation not found, incomplete strategy % 3.87/1.48 % (3979078)Time elapsed: 0.018 s % 3.87/1.48 % (3979078)Peak memory usage: 116 MB % 3.87/1.48 % (3979078)Instructions burned: 6 (million) % 3.87/1.48 % (3979074)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=3495914241:i=307:kws=precedence:nm=0:rtra=on_3000 on theBenchmark for (3000ds/307Mi) % 3.87/1.48 % (3979077)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=3654281820:i=4:rtra=on_3000 on theBenchmark for (3000ds/4Mi) % 3.87/1.48 % (3979076)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=3543544778:s2a=on:i=7:rtra=on:inst=on_3000 on theBenchmark for (3000ds/7Mi) % 3.87/1.48 % (3979077)Instruction limit reached! % 3.87/1.48 % (3979077)------------------------------ % 3.87/1.48 % (3979077)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.87/1.48 % (3979077)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.87/1.48 % (3979077)CaDiCaL version: 2.1.3 % 3.87/1.48 % (3979077)Termination reason: Instruction limit % 3.87/1.48 % (3979077)Termination phase: Saturation % 3.87/1.48 % (3979077)Time elapsed: 0.004 s % 3.87/1.48 % (3979077)Peak memory usage: 89 MB % 3.87/1.48 % (3979077)Instructions burned: 5 (million) % 3.87/1.48 % (3979073)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=1699961527:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_3000 on theBenchmark for (3000ds/12Mi) % 3.87/1.48 % (3979075)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=2365553415:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_3000 on theBenchmark for (3000ds/201Mi) % 3.87/1.48 % (3979076)Instruction limit reached! % 3.87/1.48 % (3979076)------------------------------ % 3.87/1.48 % (3979076)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.87/1.48 % (3979076)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.87/1.48 % (3979076)CaDiCaL version: 2.1.3 % 3.87/1.48 % (3979076)Termination reason: Instruction limit % 3.87/1.48 % (3979076)Termination phase: Saturation % 3.87/1.48 % (3979076)Time elapsed: 0.008 s % 3.87/1.48 % (3979076)Peak memory usage: 88 MB % 3.87/1.48 % (3979076)Instructions burned: 12 (million) % 3.87/1.48 % (3979079)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=3739007357:i=33:rtra=on_3000 on theBenchmark for (3000ds/33Mi) % 3.87/1.48 % (3979074)Refutation not found, incomplete strategy % 3.87/1.48 % (3979074)------------------------------ % 3.87/1.48 % (3979074)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.87/1.48 % (3979074)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.87/1.48 % (3979074)CaDiCaL version: 2.1.3 % 3.87/1.48 % (3979074)Termination reason: Refutation not found, incomplete strategy % 3.87/1.48 % (3979074)Time elapsed: 0.029 s % 3.87/1.48 % (3979074)Peak memory usage: 116 MB % 3.87/1.48 % (3979074)Instructions burned: 6 (million) % 3.87/1.48 % (3979073)Refutation not found, incomplete strategy % 3.87/1.48 % (3979073)------------------------------ % 3.87/1.48 % (3979073)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.87/1.48 % (3979073)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.87/1.48 % (3979073)CaDiCaL version: 2.1.3 % 3.87/1.48 % (3979073)Termination reason: Refutation not found, incomplete strategy % 3.87/1.48 % (3979073)Time elapsed: 0.029 s % 3.87/1.48 % (3979073)Peak memory usage: 116 MB % 3.87/1.48 % (3979073)Instructions burned: 7 (million) % 3.87/1.48 % (3979079)Instruction limit reached! % 3.87/1.48 % (3979079)------------------------------ % 3.87/1.48 % (3979079)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.87/1.48 % (3979079)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.68/1.64 % (3979079)CaDiCaL version: 2.1.3 % 4.68/1.64 % (3979079)Termination reason: Instruction limit % 4.68/1.64 % (3979079)Termination phase: Saturation % 4.68/1.64 % (3979079)Time elapsed: 0.048 s % 4.68/1.64 % (3979079)Peak memory usage: 117 MB % 4.68/1.64 % (3979079)Instructions burned: 34 (million) % 4.68/1.64 % (3979086)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=3357703013:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2998 on theBenchmark for (2998ds/14Mi) % 4.68/1.64 % (3979087)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=155302279:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2998 on theBenchmark for (2998ds/29Mi) % 4.68/1.64 % (3979078)------------------------------ % 4.68/1.64 % (3979078)------------------------------ % 4.68/1.64 % (3979086)Refutation not found, incomplete strategy % 4.68/1.64 % (3979086)------------------------------ % 4.68/1.64 % (3979086)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.68/1.64 % (3979086)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.68/1.64 % (3979086)CaDiCaL version: 2.1.3 % 4.68/1.64 % (3979086)Termination reason: Refutation not found, incomplete strategy % 4.68/1.64 % (3979086)Time elapsed: 0.001 s % 4.68/1.64 % (3979086)Peak memory usage: 88 MB % 4.68/1.64 % (3979075)Instruction limit reached! % 4.68/1.64 % (3979075)------------------------------ % 4.68/1.64 % (3979075)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.68/1.64 % (3979075)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.68/1.64 % (3979075)CaDiCaL version: 2.1.3 % 4.68/1.64 % (3979075)Termination reason: Instruction limit % 4.68/1.64 % (3979075)Termination phase: Saturation % 4.68/1.64 % (3979075)Time elapsed: 0.134 s % 4.68/1.64 % (3979075)Peak memory usage: 113 MB % 4.68/1.64 % (3979075)Instructions burned: 201 (million) % 4.68/1.64 % (3979087)Instruction limit reached! % 4.68/1.64 % (3979087)------------------------------ % 4.68/1.64 % (3979087)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.68/1.64 % (3979087)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.68/1.64 % (3979087)CaDiCaL version: 2.1.3 % 4.68/1.64 % (3979087)Termination reason: Instruction limit % 4.68/1.65 % (3979087)Termination phase: Saturation % 4.68/1.65 % (3979087)Time elapsed: 0.015 s % 4.68/1.65 % (3979087)Peak memory usage: 88 MB % 4.68/1.65 % (3979087)Instructions burned: 30 (million) % 4.68/1.65 % (3979089)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=1939442082:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2997 on theBenchmark for (2997ds/16Mi) % 4.68/1.65 % (3979089)Instruction limit reached! % 4.68/1.65 % (3979089)------------------------------ % 4.68/1.65 % (3979089)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.68/1.65 % (3979089)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.68/1.65 % (3979089)CaDiCaL version: 2.1.3 % 4.68/1.65 % (3979089)Termination reason: Instruction limit % 4.68/1.65 % (3979089)Termination phase: Saturation % 4.68/1.65 % (3979089)Time elapsed: 0.010 s % 4.68/1.65 % (3979089)Peak memory usage: 90 MB % 4.68/1.65 % (3979089)Instructions burned: 17 (million) % 4.68/1.65 % (3979093)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=3122455167:i=27:canc=cautious:fsr=off:rtra=on_2997 on theBenchmark for (2997ds/27Mi) % 4.68/1.65 % (3979093)Refutation not found, incomplete strategy % 4.68/1.65 % (3979093)------------------------------ % 4.68/1.65 % (3979093)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.68/1.65 % (3979093)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.68/1.65 % (3979093)CaDiCaL version: 2.1.3 % 4.68/1.65 % (3979093)Termination reason: Refutation not found, incomplete strategy % 4.68/1.65 % (3979093)Time elapsed: 0.001 s % 4.68/1.65 % (3979093)Peak memory usage: 89 MB % 4.68/1.65 % (3979074)------------------------------ % 4.68/1.65 % (3979074)------------------------------ % 4.68/1.65 % (3979092)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=1113101229:i=24:canc=force:rtra=on_2997 on theBenchmark for (2997ds/24Mi) % 4.68/1.65 % (3979073)------------------------------ % 4.68/1.65 % (3979073)------------------------------ % 4.68/1.65 % (3979094)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=4208090331:i=85:gtgl=4:rtra=on:gtg=exists_sym_2997 on theBenchmark for (2997ds/85Mi) % 6.31/1.83 % (3979092)Instruction limit reached! % 6.31/1.83 % (3979092)------------------------------ % 6.31/1.83 % (3979092)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.31/1.83 % (3979092)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.31/1.83 % (3979092)CaDiCaL version: 2.1.3 % 6.31/1.83 % (3979092)Termination reason: Instruction limit % 6.31/1.83 % (3979092)Termination phase: Saturation % 6.31/1.83 % (3979092)Time elapsed: 0.016 s % 6.31/1.83 % (3979092)Peak memory usage: 89 MB % 6.31/1.83 % (3979092)Instructions burned: 25 (million) % 6.31/1.83 % (3979094)Instruction limit reached! % 6.31/1.83 % (3979094)------------------------------ % 6.31/1.83 % (3979094)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.31/1.83 % (3979094)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.31/1.83 % (3979094)CaDiCaL version: 2.1.3 % 6.31/1.83 % (3979094)Termination reason: Instruction limit % 6.31/1.83 % (3979094)Termination phase: Saturation % 6.31/1.83 % (3979094)Time elapsed: 0.057 s % 6.31/1.83 % (3979094)Peak memory usage: 89 MB % 6.31/1.83 % (3979094)Instructions burned: 86 (million) % 6.31/1.83 % (3979097)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=3037817148:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2996 on theBenchmark for (2996ds/2Mi) % 6.31/1.83 % (3979097)Instruction limit reached! % 6.31/1.83 % (3979097)------------------------------ % 6.31/1.83 % (3979097)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.31/1.83 % (3979097)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.31/1.83 % (3979097)CaDiCaL version: 2.1.3 % 6.31/1.83 % (3979097)Termination reason: Instruction limit % 6.31/1.83 % (3979097)Termination phase: Saturation % 6.31/1.83 % (3979097)Time elapsed: 0.003 s % 6.31/1.83 % (3979097)Peak memory usage: 89 MB % 6.31/1.83 % (3979097)Instructions burned: 3 (million) % 6.31/1.83 % (3979086)------------------------------ % 6.31/1.83 % (3979086)------------------------------ % 6.31/1.83 % (3979093)------------------------------ % 6.31/1.83 % (3979093)------------------------------ % 6.31/1.83 % (3979099)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=1373721239:i=181:rtra=on:ss=axioms:ev=cautious_2995 on theBenchmark for (2995ds/181Mi) % 6.31/1.83 % (3979099)Refutation not found, incomplete strategy % 6.31/1.83 % (3979099)------------------------------ % 6.31/1.83 % (3979099)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.31/1.83 % (3979099)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.31/1.83 % (3979099)CaDiCaL version: 2.1.3 % 6.31/1.83 % (3979099)Termination reason: Refutation not found, incomplete strategy % 6.31/1.83 % (3979099)Time elapsed: 0.001 s % 6.31/1.83 % (3979099)Peak memory usage: 89 MB % 6.31/1.83 % (3979101)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=1404200252:i=4:ep=RST:ins=2:rtra=on_2995 on theBenchmark for (2995ds/4Mi) % 6.31/1.83 % (3979102)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=2527179395:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2995 on theBenchmark for (2995ds/66Mi) % 6.31/1.83 % (3979101)Refutation not found, incomplete strategy % 6.31/1.83 % (3979101)------------------------------ % 6.31/1.83 % (3979101)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.31/1.83 % (3979101)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.31/1.83 % (3979101)CaDiCaL version: 2.1.3 % 6.31/1.83 % (3979101)Termination reason: Refutation not found, incomplete strategy % 6.31/1.83 % (3979101)Time elapsed: 0.001 s % 6.31/1.83 % (3979101)Peak memory usage: 89 MB % 6.31/1.83 % (3979101)Instructions burned: 1 (million) % 6.31/1.83 % (3979107)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=1884696017:i=2:doe=on:canc=force:asg=cautious:rtra=on_2994 on theBenchmark for (2994ds/2Mi) % 6.31/1.83 % (3979103)lrs+10_1_thi=all:si=on:fd=off:random_seed=2763884802:i=53:rtra=on:gtg=all_2995 on theBenchmark for (2995ds/53Mi) % 6.31/1.83 % (3979107)Instruction limit reached! % 6.31/1.83 % (3979107)------------------------------ % 6.31/1.83 % (3979107)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.31/1.83 % (3979107)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.31/1.83 % (3979107)CaDiCaL version: 2.1.3 % 6.31/1.83 % (3979107)Termination reason: Instruction limit % 8.69/2.05 % (3979107)Termination phase: Saturation % 8.69/2.05 % (3979107)Time elapsed: 0.002 s % 8.69/2.05 % (3979107)Peak memory usage: 89 MB % 8.69/2.05 % (3979107)Instructions burned: 4 (million) % 8.69/2.05 % (3979105)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=2674615812:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2995 on theBenchmark for (2995ds/8Mi) % 8.69/2.05 % (3979105)Instruction limit reached! % 8.69/2.05 % (3979105)------------------------------ % 8.69/2.05 % (3979105)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.69/2.05 % (3979105)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.69/2.05 % (3979105)CaDiCaL version: 2.1.3 % 8.69/2.05 % (3979105)Termination reason: Instruction limit % 8.69/2.05 % (3979105)Termination phase: Saturation % 8.69/2.05 % (3979105)Time elapsed: 0.006 s % 8.69/2.05 % (3979105)Peak memory usage: 88 MB % 8.69/2.05 % (3979105)Instructions burned: 8 (million) % 8.69/2.05 % (3979102)Instruction limit reached! % 8.69/2.05 % (3979102)------------------------------ % 8.69/2.05 % (3979102)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.69/2.05 % (3979102)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.69/2.05 % (3979102)CaDiCaL version: 2.1.3 % 8.69/2.05 % (3979102)Termination reason: Instruction limit % 8.69/2.05 % (3979102)Termination phase: Saturation % 8.69/2.05 % (3979102)Time elapsed: 0.089 s % 8.69/2.05 % (3979102)Peak memory usage: 134 MB % 8.69/2.05 % (3979102)Instructions burned: 67 (million) % 8.69/2.05 % (3979106)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=3965619810:st=3:i=2:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/2Mi) % 8.69/2.05 % (3979106)Instruction limit reached! % 8.69/2.05 % (3979106)------------------------------ % 8.69/2.05 % (3979106)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.69/2.05 % (3979106)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.69/2.05 % (3979106)CaDiCaL version: 2.1.3 % 8.69/2.05 % (3979106)Termination reason: Instruction limit % 8.69/2.05 % (3979106)Termination phase: Saturation % 8.69/2.05 % (3979106)Time elapsed: 0.003 s % 8.69/2.05 % (3979106)Peak memory usage: 90 MB % 8.69/2.05 % (3979106)Instructions burned: 3 (million) % 8.69/2.05 % (3979103)Instruction limit reached! % 8.69/2.05 % (3979103)------------------------------ % 8.69/2.05 % (3979103)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.69/2.05 % (3979103)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.69/2.05 % (3979103)CaDiCaL version: 2.1.3 % 8.69/2.05 % (3979103)Termination reason: Instruction limit % 8.69/2.05 % (3979103)Termination phase: Saturation % 8.69/2.05 % (3979103)Time elapsed: 0.059 s % 8.69/2.05 % (3979103)Peak memory usage: 112 MB % 8.69/2.05 % (3979103)Instructions burned: 54 (million) % 8.69/2.05 % (3979113)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=602077195:i=127:doe=on:rtra=on_2993 on theBenchmark for (2993ds/127Mi) % 8.69/2.05 % (3979113)Refutation not found, incomplete strategy % 8.69/2.05 % (3979113)------------------------------ % 8.69/2.05 % (3979113)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.69/2.05 % (3979113)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.69/2.06 % (3979113)CaDiCaL version: 2.1.3 % 8.69/2.06 % (3979113)Termination reason: Refutation not found, incomplete strategy % 8.69/2.06 % (3979113)Time elapsed: 0.018 s % 8.69/2.06 % (3979113)Peak memory usage: 116 MB % 8.69/2.06 % (3979113)Instructions burned: 8 (million) % 8.69/2.06 % (3979115)dis+10_1_si=on:random_seed=3132869717:i=10:ep=R:rtra=on_2993 on theBenchmark for (2993ds/10Mi) % 8.69/2.06 % (3979115)Instruction limit reached! % 8.69/2.06 % (3979115)------------------------------ % 8.69/2.06 % (3979115)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.69/2.06 % (3979115)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.69/2.06 % (3979115)CaDiCaL version: 2.1.3 % 8.69/2.06 % (3979115)Termination reason: Instruction limit % 8.69/2.06 % (3979115)Termination phase: Saturation % 8.69/2.06 % (3979115)Time elapsed: 0.008 s % 8.69/2.06 % (3979115)Peak memory usage: 88 MB % 8.69/2.06 % (3979115)Instructions burned: 11 (million) % 8.69/2.06 % (3979117)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=1177885875:i=26:canc=cautious:av=off:rtra=on_2993 on theBenchmark for (2993ds/26Mi) % 8.69/2.06 % (3979118)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=2460123894: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_2993 on theBenchmark for (2993ds/35Mi) % 9.40/2.25 % (3979099)------------------------------ % 9.40/2.25 % (3979099)------------------------------ % 9.40/2.25 % (3979117)Refutation not found, incomplete strategy % 9.40/2.25 % (3979117)------------------------------ % 9.40/2.25 % (3979117)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.40/2.25 % (3979117)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.40/2.25 % (3979117)CaDiCaL version: 2.1.3 % 9.40/2.25 % (3979117)Termination reason: Refutation not found, incomplete strategy % 9.40/2.25 % (3979117)Time elapsed: 0.002 s % 9.40/2.25 % (3979117)Peak memory usage: 89 MB % 9.40/2.25 % (3979117)Instructions burned: 1 (million) % 9.40/2.25 % (3979118)Instruction limit reached! % 9.40/2.25 % (3979118)------------------------------ % 9.40/2.25 % (3979118)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.40/2.25 % (3979118)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.40/2.25 % (3979118)CaDiCaL version: 2.1.3 % 9.40/2.25 % (3979118)Termination reason: Instruction limit % 9.40/2.25 % (3979118)Termination phase: Saturation % 9.40/2.25 % (3979118)Time elapsed: 0.029 s % 9.40/2.25 % (3979118)Peak memory usage: 89 MB % 9.40/2.25 % (3979118)Instructions burned: 36 (million) % 9.40/2.25 % (3979101)------------------------------ % 9.40/2.25 % (3979101)------------------------------ % 9.40/2.25 % (3979119)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=1936044727:i=2:fsr=off:rtra=on:inst=on_2993 on theBenchmark for (2993ds/2Mi) % 9.40/2.25 % (3979119)Instruction limit reached! % 9.40/2.25 % (3979119)------------------------------ % 9.40/2.25 % (3979119)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.40/2.25 % (3979119)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.40/2.25 % (3979119)CaDiCaL version: 2.1.3 % 9.40/2.25 % (3979119)Termination reason: Instruction limit % 9.40/2.25 % (3979119)Termination phase: Saturation % 9.40/2.25 % (3979119)Time elapsed: 0.003 s % 9.40/2.25 % (3979119)Peak memory usage: 89 MB % 9.40/2.25 % (3979119)Instructions burned: 3 (million) % 9.40/2.25 % (3979113)------------------------------ % 9.40/2.25 % (3979113)------------------------------ % 9.40/2.25 % (3979124)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=1616917947:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2992 on theBenchmark for (2992ds/8Mi) % 9.40/2.25 % (3979124)Instruction limit reached! % 9.40/2.25 % (3979124)------------------------------ % 9.40/2.25 % (3979124)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.40/2.25 % (3979124)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.40/2.25 % (3979124)CaDiCaL version: 2.1.3 % 9.40/2.25 % (3979124)Termination reason: Instruction limit % 9.40/2.25 % (3979124)Termination phase: Saturation % 9.40/2.25 % (3979124)Time elapsed: 0.006 s % 9.40/2.25 % (3979124)Peak memory usage: 88 MB % 9.40/2.25 % (3979124)Instructions burned: 8 (million) % 9.40/2.25 % (3979125)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=2979311171:i=370:ep=RS:fsr=off:rtra=on_2992 on theBenchmark for (2992ds/370Mi) % 9.40/2.25 % (3979126)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=2135848018:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2991 on theBenchmark for (2991ds/13Mi) % 9.40/2.25 % (3979129)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=2524747818:i=10:rtra=on_2991 on theBenchmark for (2991ds/10Mi) % 9.40/2.25 % (3979129)Refutation not found, incomplete strategy % 9.40/2.25 % (3979129)------------------------------ % 9.40/2.25 % (3979129)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.40/2.25 % (3979129)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.40/2.25 % (3979129)CaDiCaL version: 2.1.3 % 9.40/2.25 % (3979129)Termination reason: Refutation not found, incomplete strategy % 9.40/2.25 % (3979129)Time elapsed: 0.001 s % 9.40/2.25 % (3979129)Peak memory usage: 88 MB % 9.40/2.25 % (3979128)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=1970798922:i=226:rtra=on:gtg=position:ss=axioms_2991 on theBenchmark for (2991ds/226Mi) % 9.40/2.25 % (3979126)Instruction limit reached! % 11.77/2.61 % (3979126)------------------------------ % 11.77/2.61 % (3979126)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.77/2.61 % (3979126)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.77/2.61 % (3979126)CaDiCaL version: 2.1.3 % 11.77/2.61 % (3979126)Termination reason: Instruction limit % 11.77/2.61 % (3979126)Termination phase: Saturation % 11.77/2.61 % (3979126)Time elapsed: 0.029 s % 11.77/2.61 % (3979126)Peak memory usage: 112 MB % 11.77/2.61 % (3979126)Instructions burned: 15 (million) % 11.77/2.61 % (3979130)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=960594151:i=71:rtra=on:gtg=exists_top_2991 on theBenchmark for (2991ds/71Mi) % 11.77/2.61 % (3979128)Refutation not found, incomplete strategy % 11.77/2.61 % (3979128)------------------------------ % 11.77/2.61 % (3979128)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.77/2.61 % (3979128)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.77/2.61 % (3979128)CaDiCaL version: 2.1.3 % 11.77/2.61 % (3979128)Termination reason: Refutation not found, incomplete strategy % 11.77/2.61 % (3979128)Time elapsed: 0.029 s % 11.77/2.61 % (3979128)Peak memory usage: 116 MB % 11.77/2.61 % (3979128)Instructions burned: 6 (million) % 11.77/2.61 % (3979130)Refutation not found, incomplete strategy % 11.77/2.61 % (3979130)------------------------------ % 11.77/2.61 % (3979130)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.77/2.61 % (3979130)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.77/2.61 % (3979130)CaDiCaL version: 2.1.3 % 11.77/2.61 % (3979130)Termination reason: Refutation not found, incomplete strategy % 11.77/2.61 % (3979130)Time elapsed: 0.033 s % 11.77/2.61 % (3979130)Peak memory usage: 133 MB % 11.77/2.61 % (3979130)Instructions burned: 11 (million) % 11.77/2.61 % (3979117)------------------------------ % 11.77/2.61 % (3979117)------------------------------ % 11.77/2.61 % (3979133)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=4119514820:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2990 on theBenchmark for (2990ds/75Mi) % 11.77/2.61 % (3979133)Instruction limit reached! % 11.77/2.61 % (3979133)------------------------------ % 11.77/2.61 % (3979133)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.77/2.61 % (3979133)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.77/2.61 % (3979133)CaDiCaL version: 2.1.3 % 11.77/2.61 % (3979133)Termination reason: Instruction limit % 11.77/2.61 % (3979133)Termination phase: Saturation % 11.77/2.61 % (3979133)Time elapsed: 0.032 s % 11.77/2.61 % (3979133)Peak memory usage: 89 MB % 11.77/2.61 % (3979133)Instructions burned: 77 (million) % 11.77/2.61 % (3979137)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=4171779501:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2990 on theBenchmark for (2990ds/294Mi) % 11.77/2.61 % (3979125)Instruction limit reached! % 11.77/2.61 % (3979125)------------------------------ % 11.77/2.61 % (3979125)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.77/2.61 % (3979125)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.77/2.61 % (3979125)CaDiCaL version: 2.1.3 % 11.77/2.61 % (3979125)Termination reason: Instruction limit % 11.77/2.61 % (3979125)Termination phase: Saturation % 11.77/2.61 % (3979125)Time elapsed: 0.185 s % 11.77/2.61 % (3979125)Peak memory usage: 91 MB % 11.77/2.61 % (3979125)Instructions burned: 371 (million) % 11.77/2.61 % (3979130)------------------------------ % 11.77/2.61 % (3979130)------------------------------ % 11.77/2.61 % (3979139)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=2675406753:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2989 on theBenchmark for (2989ds/130Mi) % 11.77/2.61 % (3979129)------------------------------ % 11.77/2.61 % (3979129)------------------------------ % 11.77/2.61 % (3979139)Refutation not found, incomplete strategy % 11.77/2.61 % (3979139)------------------------------ % 11.77/2.61 % (3979139)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.77/2.61 % (3979139)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.77/2.61 % (3979139)CaDiCaL version: 2.1.3 % 11.77/2.61 % (3979139)Termination reason: Refutation not found, incomplete strategy % 11.77/2.61 % (3979139)Time elapsed: 0.029 s % 11.77/2.61 % (3979139)Peak memory usage: 116 MB % 12.63/2.85 % (3979139)Instructions burned: 6 (million) % 12.63/2.85 % (3979141)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=2652147308:i=131:rtra=on_2989 on theBenchmark for (2989ds/131Mi) % 12.63/2.85 % (3979143)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=3801640330:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2988 on theBenchmark for (2988ds/40Mi) % 12.63/2.85 % (3979128)------------------------------ % 12.63/2.85 % (3979128)------------------------------ % 12.63/2.85 % (3979137)Instruction limit reached! % 12.63/2.85 % (3979137)------------------------------ % 12.63/2.85 % (3979137)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.63/2.85 % (3979137)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.63/2.85 % (3979137)CaDiCaL version: 2.1.3 % 12.63/2.85 % (3979137)Termination reason: Instruction limit % 12.63/2.85 % (3979137)Termination phase: Saturation % 12.63/2.85 % (3979137)Time elapsed: 0.131 s % 12.63/2.85 % (3979137)Peak memory usage: 88 MB % 12.63/2.85 % (3979137)Instructions burned: 295 (million) % 12.63/2.85 % (3979145)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=1367569505:i=307:rtra=on:gtg=exists_top_2988 on theBenchmark for (2988ds/307Mi) % 12.63/2.85 % (3979145)Refutation not found, incomplete strategy % 12.63/2.85 % (3979145)------------------------------ % 12.63/2.85 % (3979145)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.63/2.85 % (3979145)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.63/2.85 % (3979145)CaDiCaL version: 2.1.3 % 12.63/2.85 % (3979145)Termination reason: Refutation not found, incomplete strategy % 12.63/2.85 % (3979145)Time elapsed: 0.001 s % 12.63/2.85 % (3979145)Peak memory usage: 89 MB % 12.63/2.85 % (3979145)Instructions burned: 1 (million) % 12.63/2.85 % (3979141)Refutation not found, incomplete strategy % 12.63/2.85 % (3979141)------------------------------ % 12.63/2.85 % (3979141)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.63/2.85 % (3979141)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.63/2.85 % (3979141)CaDiCaL version: 2.1.3 % 12.63/2.85 % (3979141)Termination reason: Refutation not found, incomplete strategy % 12.63/2.85 % (3979141)Time elapsed: 0.054 s % 12.63/2.85 % (3979141)Peak memory usage: 133 MB % 12.63/2.85 % (3979141)Instructions burned: 11 (million) % 12.63/2.85 % (3979143)Instruction limit reached! % 12.63/2.85 % (3979143)------------------------------ % 12.63/2.85 % (3979143)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.63/2.85 % (3979143)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.63/2.85 % (3979143)CaDiCaL version: 2.1.3 % 12.63/2.85 % (3979143)Termination reason: Instruction limit % 12.63/2.85 % (3979143)Termination phase: Saturation % 12.63/2.85 % (3979143)Time elapsed: 0.068 s % 12.63/2.85 % (3979143)Peak memory usage: 134 MB % 12.63/2.85 % (3979143)Instructions burned: 40 (million) % 12.63/2.85 % (3979146)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=1974344501:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2988 on theBenchmark for (2988ds/598Mi) % 12.63/2.85 % (3979149)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=1205262070:i=131:canc=cautious:fsr=off:rtra=on_2987 on theBenchmark for (2987ds/131Mi) % 12.63/2.85 % (3979150)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=2443236938:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2987 on theBenchmark for (2987ds/259Mi) % 12.63/2.85 % (3979146)Refutation not found, incomplete strategy % 12.63/2.85 % (3979146)------------------------------ % 12.63/2.85 % (3979146)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.63/2.85 % (3979146)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.63/2.85 % (3979146)CaDiCaL version: 2.1.3 % 12.63/2.85 % (3979146)Termination reason: Refutation not found, incomplete strategy % 12.63/2.85 % (3979146)Time elapsed: 0.054 s % 12.63/2.85 % (3979146)Peak memory usage: 133 MB % 12.63/2.85 % (3979146)Instructions burned: 11 (million) % 12.63/2.85 % (3979150)Refutation not found, incomplete strategy % 12.63/2.85 % (3979150)------------------------------ % 12.63/2.85 % (3979150)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.63/2.85 % (3979150)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.23/3.16 % (3979150)CaDiCaL version: 2.1.3 % 16.23/3.16 % (3979150)Termination reason: Refutation not found, incomplete strategy % 16.23/3.16 % (3979150)Time elapsed: 0.029 s % 16.23/3.16 % (3979150)Peak memory usage: 116 MB % 16.23/3.16 % (3979150)Instructions burned: 6 (million) % 16.23/3.16 % (3979145)------------------------------ % 16.23/3.16 % (3979145)------------------------------ % 16.23/3.16 % (3979152)dis+10_1_si=on:random_seed=1088024455:s2a=on:i=1000:rtra=on:gtg=exists_all_2986 on theBenchmark for (2986ds/1000Mi) % 16.23/3.16 % (3979139)------------------------------ % 16.23/3.16 % (3979139)------------------------------ % 16.23/3.16 % (3979149)Instruction limit reached! % 16.23/3.16 % (3979149)------------------------------ % 16.23/3.16 % (3979149)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.23/3.16 % (3979149)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.23/3.16 % (3979149)CaDiCaL version: 2.1.3 % 16.23/3.16 % (3979149)Termination reason: Instruction limit % 16.23/3.16 % (3979149)Termination phase: Saturation % 16.23/3.16 % (3979149)Time elapsed: 0.106 s % 16.23/3.16 % (3979149)Peak memory usage: 118 MB % 16.23/3.16 % (3979149)Instructions burned: 131 (million) % 16.23/3.16 % (3979156)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=3355878561:i=383:fsr=off:rtra=on:ev=force_2985 on theBenchmark for (2985ds/383Mi) % 16.23/3.16 % (3979156)Refutation not found, incomplete strategy % 16.23/3.16 % (3979156)------------------------------ % 16.23/3.16 % (3979156)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.23/3.16 % (3979156)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.23/3.16 % (3979156)CaDiCaL version: 2.1.3 % 16.23/3.16 % (3979156)Termination reason: Refutation not found, incomplete strategy % 16.23/3.16 % (3979156)Time elapsed: 0.001 s % 16.23/3.16 % (3979156)Peak memory usage: 89 MB % 16.23/3.16 % (3979141)------------------------------ % 16.23/3.16 % (3979141)------------------------------ % 16.23/3.16 % (3979158)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=1318824247:i=141:doe=on:rtra=on_2985 on theBenchmark for (2985ds/141Mi) % 16.23/3.16 % (3979159)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=1789495906:i=65:nm=16:rtra=on_2985 on theBenchmark for (2985ds/65Mi) % 16.23/3.16 % (3979146)------------------------------ % 16.23/3.16 % (3979146)------------------------------ % 16.23/3.16 % (3979150)------------------------------ % 16.23/3.16 % (3979150)------------------------------ % 16.23/3.16 % (3979159)Refutation not found, incomplete strategy % 16.23/3.16 % (3979159)------------------------------ % 16.23/3.16 % (3979159)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.23/3.16 % (3979159)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.23/3.16 % (3979159)CaDiCaL version: 2.1.3 % 16.23/3.16 % (3979159)Termination reason: Refutation not found, incomplete strategy % 16.23/3.16 % (3979159)Time elapsed: 0.029 s % 16.23/3.16 % (3979159)Peak memory usage: 116 MB % 16.23/3.16 % (3979159)Instructions burned: 6 (million) % 16.23/3.16 % (3979158)Instruction limit reached! % 16.23/3.16 % (3979158)------------------------------ % 16.23/3.16 % (3979158)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.23/3.16 % (3979158)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.23/3.16 % (3979158)CaDiCaL version: 2.1.3 % 16.23/3.16 % (3979158)Termination reason: Instruction limit % 16.23/3.16 % (3979158)Termination phase: Saturation % 16.23/3.16 % (3979158)Time elapsed: 0.091 s % 16.23/3.16 % (3979158)Peak memory usage: 90 MB % 16.23/3.16 % (3979158)Instructions burned: 142 (million) % 16.23/3.16 % (3979156)------------------------------ % 16.23/3.16 % (3979156)------------------------------ % 16.23/3.16 % (3979161)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=2569970120:i=121:nm=16:rtra=on_2984 on theBenchmark for (2984ds/121Mi) % 16.23/3.16 % (3979161)Instruction limit reached! % 16.23/3.16 % (3979161)------------------------------ % 16.23/3.16 % (3979161)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.23/3.16 % (3979161)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.23/3.16 % (3979161)CaDiCaL version: 2.1.3 % 16.23/3.16 % (3979161)Termination reason: Instruction limit % 16.23/3.16 % (3979161)Termination phase: Saturation % 16.23/3.16 % (3979161)Time elapsed: 0.053 s % 16.23/3.16 % (3979161)Peak memory usage: 88 MB % 16.23/3.16 % (3979161)Instructions burned: 122 (million) % 16.23/3.16 % (3979164)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=3773632658:s2a=on:i=128:s2at=5:ins=3:rtra=on_2983 on theBenchmark for (2983ds/128Mi) % 16.79/3.35 % (3979165)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=2085588551:i=39:ins=3:rtra=on_2983 on theBenchmark for (2983ds/39Mi) % 16.79/3.35 % (3979166)dis+1010_1_to=kbo:si=on:random_seed=3974210897:i=175:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2983 on theBenchmark for (2983ds/175Mi) % 16.79/3.35 % (3979165)Refutation not found, incomplete strategy % 16.79/3.35 % (3979165)------------------------------ % 16.79/3.35 % (3979165)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.79/3.35 % (3979165)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.79/3.35 % (3979165)CaDiCaL version: 2.1.3 % 16.79/3.35 % (3979165)Termination reason: Refutation not found, incomplete strategy % 16.79/3.35 % (3979165)Time elapsed: 0.028 s % 16.79/3.35 % (3979165)Peak memory usage: 115 MB % 16.79/3.35 % (3979165)Instructions burned: 6 (million) % 16.79/3.35 % (3979168)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=3180103445:i=329:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2983 on theBenchmark for (2983ds/329Mi) % 16.79/3.35 % (3979164)Instruction limit reached! % 16.79/3.35 % (3979164)------------------------------ % 16.79/3.35 % (3979164)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.79/3.35 % (3979164)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.79/3.35 % (3979164)CaDiCaL version: 2.1.3 % 16.79/3.35 % (3979164)Termination reason: Instruction limit % 16.79/3.35 % (3979164)Termination phase: Saturation % 16.79/3.35 % (3979164)Time elapsed: 0.092 s % 16.79/3.35 % (3979164)Peak memory usage: 119 MB % 16.79/3.35 % (3979164)Instructions burned: 130 (million) % 16.79/3.35 % (3979169)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=1548827431:s2a=on:i=483:doe=on:nm=32:rtra=on_2982 on theBenchmark for (2982ds/483Mi) % 16.79/3.35 % (3979159)------------------------------ % 16.79/3.35 % (3979159)------------------------------ % 16.79/3.35 % (3979166)Instruction limit reached! % 16.79/3.35 % (3979166)------------------------------ % 16.79/3.35 % (3979166)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.79/3.35 % (3979166)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.79/3.35 % (3979166)CaDiCaL version: 2.1.3 % 16.79/3.35 % (3979166)Termination reason: Instruction limit % 16.79/3.35 % (3979166)Termination phase: Saturation % 16.79/3.35 % (3979166)Time elapsed: 0.095 s % 16.79/3.35 % (3979166)Peak memory usage: 90 MB % 16.79/3.35 % (3979166)Instructions burned: 176 (million) % 16.79/3.35 % (3979169)Refutation not found, incomplete strategy % 16.79/3.35 % (3979169)------------------------------ % 16.79/3.35 % (3979169)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.79/3.35 % (3979169)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.79/3.35 % (3979169)CaDiCaL version: 2.1.3 % 16.79/3.35 % (3979169)Termination reason: Refutation not found, incomplete strategy % 16.79/3.35 % (3979169)Time elapsed: 0.053 s % 16.79/3.35 % (3979169)Peak memory usage: 133 MB % 16.79/3.35 % (3979169)Instructions burned: 11 (million) % 16.79/3.35 % (3979152)Instruction limit reached! % 16.79/3.35 % (3979152)------------------------------ % 16.79/3.35 % (3979152)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.79/3.35 % (3979152)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.79/3.35 % (3979152)CaDiCaL version: 2.1.3 % 16.79/3.35 % (3979152)Termination reason: Instruction limit % 16.79/3.35 % (3979152)Termination phase: Saturation % 16.79/3.35 % (3979152)Time elapsed: 0.505 s % 16.79/3.35 % (3979152)Peak memory usage: 93 MB % 16.79/3.35 % (3979152)Instructions burned: 1000 (million) % 16.79/3.35 % (3979174)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=1977643085:thitd=on:i=215:nm=0:rtra=on:ev=force_2981 on theBenchmark for (2981ds/215Mi) % 16.79/3.35 % (3979174)Refutation not found, incomplete strategy % 16.79/3.35 % (3979174)------------------------------ % 16.79/3.35 % (3979174)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.79/3.35 % (3979174)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.79/3.35 % (3979174)CaDiCaL version: 2.1.3 % 18.28/3.64 % (3979174)Termination reason: Refutation not found, incomplete strategy % 18.28/3.64 % (3979174)Time elapsed: 0.037 s % 18.28/3.64 % (3979174)Peak memory usage: 134 MB % 18.28/3.64 % (3979174)Instructions burned: 19 (million) % 18.28/3.64 % (3979168)Instruction limit reached! % 18.28/3.64 % (3979168)------------------------------ % 18.28/3.64 % (3979168)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.28/3.64 % (3979168)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.28/3.64 % (3979168)CaDiCaL version: 2.1.3 % 18.28/3.64 % (3979168)Termination reason: Instruction limit % 18.28/3.64 % (3979168)Termination phase: Saturation % 18.28/3.64 % (3979168)Time elapsed: 0.201 s % 18.28/3.64 % (3979168)Peak memory usage: 114 MB % 18.28/3.64 % (3979168)Instructions burned: 330 (million) % 18.28/3.64 % (3979176)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=1431651814:i=349:rtra=on_2981 on theBenchmark for (2981ds/349Mi) % 18.28/3.64 % (3979177)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=2174135404:st=2:i=295:rtra=on:ss=axioms_2981 on theBenchmark for (2981ds/295Mi) % 18.28/3.64 % (3979176)Refutation not found, incomplete strategy % 18.28/3.64 % (3979176)------------------------------ % 18.28/3.64 % (3979176)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.28/3.64 % (3979176)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.28/3.64 % (3979176)CaDiCaL version: 2.1.3 % 18.28/3.64 % (3979176)Termination reason: Refutation not found, incomplete strategy % 18.28/3.64 % (3979176)Time elapsed: 0.029 s % 18.28/3.64 % (3979176)Peak memory usage: 116 MB % 18.28/3.64 % (3979176)Instructions burned: 6 (million) % 18.28/3.64 % (3979165)------------------------------ % 18.28/3.64 % (3979165)------------------------------ % 18.28/3.64 % (3979178)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=504688597:i=328:kws=inv_frequency:nm=20:rtra=on_2980 on theBenchmark for (2980ds/328Mi) % 18.28/3.64 % (3979181)dis+1010_1_to=lpo:sil=128000:sas=z3:si=on:nwc=5:random_seed=3153281777:i=281:gtgl=2:rtra=on:gtg=all_2979 on theBenchmark for (2979ds/281Mi) % 18.28/3.64 % (3979174)------------------------------ % 18.28/3.64 % (3979174)------------------------------ % 18.28/3.64 % (3979169)------------------------------ % 18.28/3.64 % (3979169)------------------------------ % 18.28/3.64 % (3979183)lrs+1010_1_to=kbo:sil=128000:si=on:sos=on:urr=on:uwa=alasca_main:random_seed=1025873154:i=484:doe=on:nm=0:av=off:rtra=on:ss=axioms_2979 on theBenchmark for (2979ds/484Mi) % 18.28/3.64 % (3979177)Instruction limit reached! % 18.28/3.64 % (3979177)------------------------------ % 18.28/3.64 % (3979177)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.28/3.64 % (3979177)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.28/3.64 % (3979177)CaDiCaL version: 2.1.3 % 18.28/3.64 % (3979177)Termination reason: Instruction limit % 18.28/3.64 % (3979177)Termination phase: Saturation % 18.28/3.64 % (3979177)Time elapsed: 0.165 s % 18.28/3.64 % (3979177)Peak memory usage: 90 MB % 18.28/3.64 % (3979177)Instructions burned: 296 (million) % 18.28/3.64 % (3979183)Refutation not found, incomplete strategy % 18.28/3.64 % (3979183)------------------------------ % 18.28/3.64 % (3979183)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.28/3.64 % (3979183)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.28/3.64 % (3979183)CaDiCaL version: 2.1.3 % 18.28/3.64 % (3979183)Termination reason: Refutation not found, incomplete strategy % 18.28/3.64 % (3979183)Time elapsed: 0.001 s % 18.28/3.64 % (3979183)Peak memory usage: 89 MB % 18.28/3.64 % (3979186)lrs+21_1_to=kbo:sil=128000:thi=neg_eq:si=on:random_seed=3899563195:i=321:canc=force:rtra=on:tac=axiom:ss=axioms:ev=force_2978 on theBenchmark for (2978ds/321Mi) % 18.28/3.64 % (3979176)------------------------------ % 18.28/3.64 % (3979176)------------------------------ % 18.28/3.64 % (3979187)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=78549735:i=416:rtra=on:gtg=position:ss=axioms_2978 on theBenchmark for (2978ds/416Mi) % 18.28/3.64 % (3979178)Instruction limit reached! % 18.28/3.64 % (3979178)------------------------------ % 18.28/3.64 % (3979178)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.28/3.64 % (3979178)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.28/3.64 % (3979178)CaDiCaL version: 2.1.3 % 18.28/3.64 % (3979178)Termination reason: Instruction limit % 20.93/4.00 % (3979178)Termination phase: Saturation % 20.93/4.00 % (3979178)Time elapsed: 0.233 s % 20.93/4.00 % (3979178)Peak memory usage: 119 MB % 20.93/4.00 % (3979178)Instructions burned: 328 (million) % 20.93/4.00 % (3979187)Refutation not found, incomplete strategy % 20.93/4.00 % (3979187)------------------------------ % 20.93/4.00 % (3979187)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.93/4.00 % (3979187)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.93/4.00 % (3979187)CaDiCaL version: 2.1.3 % 20.93/4.00 % (3979187)Termination reason: Refutation not found, incomplete strategy % 20.93/4.00 % (3979187)Time elapsed: 0.028 s % 20.93/4.00 % (3979187)Peak memory usage: 116 MB % 20.93/4.00 % (3979187)Instructions burned: 6 (million) % 20.93/4.00 % (3979189)lrs+1010_1_to=kbo:tgt=ground:fde=unused:sas=z3:si=on:sp=unary_frequency:gve=force:spb=goal:tha=off:random_seed=2401502578:i=471:thf=on:kws=precedence:rtra=on_2977 on theBenchmark for (2977ds/471Mi) % 20.93/4.00 % (3979181)Instruction limit reached! % 20.93/4.00 % (3979181)------------------------------ % 20.93/4.00 % (3979181)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.93/4.00 % (3979181)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.93/4.00 % (3979181)CaDiCaL version: 2.1.3 % 20.93/4.00 % (3979181)Termination reason: Instruction limit % 20.93/4.00 % (3979181)Termination phase: Saturation % 20.93/4.00 % (3979181)Time elapsed: 0.195 s % 20.93/4.00 % (3979181)Peak memory usage: 118 MB % 20.93/4.00 % (3979181)Instructions burned: 281 (million) % 20.93/4.00 % (3979186)Instruction limit reached! % 20.93/4.00 % (3979186)------------------------------ % 20.93/4.00 % (3979186)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.93/4.00 % (3979186)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.93/4.00 % (3979186)CaDiCaL version: 2.1.3 % 20.93/4.00 % (3979186)Termination reason: Instruction limit % 20.93/4.00 % (3979186)Termination phase: Saturation % 20.93/4.00 % (3979186)Time elapsed: 0.110 s % 20.93/4.00 % (3979186)Peak memory usage: 115 MB % 20.93/4.00 % (3979186)Instructions burned: 322 (million) % 20.93/4.00 % (3979189)Refutation not found, incomplete strategy % 20.93/4.00 % (3979189)------------------------------ % 20.93/4.00 % (3979189)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.93/4.00 % (3979189)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.93/4.00 % (3979189)CaDiCaL version: 2.1.3 % 20.93/4.00 % (3979189)Termination reason: Refutation not found, incomplete strategy % 20.93/4.00 % (3979189)Time elapsed: 0.029 s % 20.93/4.00 % (3979189)Peak memory usage: 116 MB % 20.93/4.00 % (3979189)Instructions burned: 6 (million) % 20.93/4.00 % (3979191)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=3610450339:avsq=on:i=276:avsqr=1,2:rtra=on_2977 on theBenchmark for (2977ds/276Mi) % 20.93/4.00 % (3979193)lrs+1010_2_to=kbo:sil=128000:tgt=ground:fde=unused:sas=z3:si=on:uwa=off:tha=off:nwc=1:random_seed=4009053760:i=375:kws=inv_arity_squared:rtra=on_2976 on theBenchmark for (2976ds/375Mi) % 20.93/4.00 % (3979196)lrs+10_1_to=kbo:sil=128000:fde=none:si=on:norm_ineq=on:urr=on:nwc=0.5:random_seed=2883506862:i=513:kws=frequency:bd=all:rtra=on:gtg=exists_all:ss=axioms:sgt=4_2976 on theBenchmark for (2976ds/513Mi) % 20.93/4.00 % (3979183)------------------------------ % 20.93/4.00 % (3979183)------------------------------ % 20.93/4.00 % (3979193)Refutation not found, incomplete strategy % 20.93/4.00 % (3979193)------------------------------ % 20.93/4.00 % (3979193)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.93/4.00 % (3979193)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.93/4.00 % (3979193)CaDiCaL version: 2.1.3 % 20.93/4.00 % (3979193)Termination reason: Refutation not found, incomplete strategy % 20.93/4.00 % (3979193)Time elapsed: 0.029 s % 20.93/4.00 % (3979193)Peak memory usage: 116 MB % 20.93/4.00 % (3979193)Instructions burned: 6 (million) % 20.93/4.00 % (3979195)lrs+10_1_to=kbo:sil=128000:tgt=full:sas=z3:si=on:uwa=func_ext:slsqc=1:flr=on:slsq=on:random_seed=538419370:i=387:bd=preordered:rtra=on:ss=axioms:sgt=8_2976 on theBenchmark for (2976ds/387Mi) % 20.93/4.00 % (3979191)Refutation not found, incomplete strategy % 20.93/4.00 % (3979191)------------------------------ % 20.93/4.00 % (3979191)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.93/4.00 % (3979191)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.06/4.34 % (3979191)CaDiCaL version: 2.1.3 % 24.06/4.34 % (3979191)Termination reason: Refutation not found, incomplete strategy % 24.06/4.34 % (3979191)Time elapsed: 0.054 s % 24.06/4.34 % (3979191)Peak memory usage: 133 MB % 24.06/4.34 % (3979191)Instructions burned: 11 (million) % 24.06/4.34 % (3979187)------------------------------ % 24.06/4.34 % (3979187)------------------------------ % 24.06/4.34 % (3979196)Instruction limit reached! % 24.06/4.34 % (3979196)------------------------------ % 24.06/4.34 % (3979196)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.06/4.34 % (3979196)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.06/4.34 % (3979196)CaDiCaL version: 2.1.3 % 24.06/4.34 % (3979196)Termination reason: Instruction limit % 24.06/4.34 % (3979196)Termination phase: Saturation % 24.06/4.34 % (3979196)Time elapsed: 0.139 s % 24.06/4.34 % (3979196)Peak memory usage: 90 MB % 24.06/4.34 % (3979196)Instructions burned: 517 (million) % 24.06/4.34 % (3979200)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=3234121888:i=334:rtra=on_2975 on theBenchmark for (2975ds/334Mi) % 24.06/4.34 % (3979189)------------------------------ % 24.06/4.34 % (3979189)------------------------------ % 24.06/4.34 % (3979200)Refutation not found, incomplete strategy % 24.06/4.34 % (3979200)------------------------------ % 24.06/4.34 % (3979200)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.06/4.34 % (3979200)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.06/4.34 % (3979200)CaDiCaL version: 2.1.3 % 24.06/4.34 % (3979200)Termination reason: Refutation not found, incomplete strategy % 24.06/4.34 % (3979200)Time elapsed: 0.053 s % 24.06/4.34 % (3979200)Peak memory usage: 133 MB % 24.06/4.34 % (3979200)Instructions burned: 11 (million) % 24.06/4.34 % (3979204)dis+1010_1_to=lpo:sil=128000:thi=all:fde=unused:si=on:sp=reverse_arity:tha=off:random_seed=1990195541:i=341:gtgl=2:rtra=on:gtg=exists_sym:ev=force:fsd=on:fsdmm=1_2974 on theBenchmark for (2974ds/341Mi) % 24.06/4.34 % (3979204)Refutation not found, incomplete strategy % 24.06/4.34 % (3979204)------------------------------ % 24.06/4.34 % (3979204)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.06/4.34 % (3979204)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.06/4.34 % (3979204)CaDiCaL version: 2.1.3 % 24.06/4.34 % (3979204)Termination reason: Refutation not found, incomplete strategy % 24.06/4.34 % (3979204)Time elapsed: 0.016 s % 24.06/4.34 % (3979204)Peak memory usage: 113 MB % 24.06/4.34 % (3979204)Instructions burned: 5 (million) % 24.06/4.34 % (3979193)------------------------------ % 24.06/4.34 % (3979193)------------------------------ % 24.06/4.34 % (3979202)lrs+1010_1_to=kbo:sil=64000:sas=cadical:si=on:sos=on:bce=on:random_seed=1985541930:i=359:rtra=on:gtg=exists_top:ss=axioms_2974 on theBenchmark for (2974ds/359Mi) % 24.06/4.34 % (3979202)Refutation not found, incomplete strategy % 24.06/4.34 % (3979202)------------------------------ % 24.06/4.34 % (3979202)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.06/4.34 % (3979202)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.06/4.34 % (3979202)CaDiCaL version: 2.1.3 % 24.06/4.34 % (3979202)Termination reason: Refutation not found, incomplete strategy % 24.06/4.34 % (3979202)Time elapsed: 0.001 s % 24.06/4.34 % (3979202)Peak memory usage: 89 MB % 24.06/4.34 % (3979191)------------------------------ % 24.06/4.34 % (3979191)------------------------------ % 24.06/4.34 % (3979205)lrs-2_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_max:tha=off:random_seed=92699740:st=1.5:i=261:sd=1:kws=precedence:rtra=on:ss=axioms_2973 on theBenchmark for (2973ds/261Mi) % 24.06/4.34 % (3979205)Refutation not found, incomplete strategy % 24.06/4.34 % (3979205)------------------------------ % 24.06/4.34 % (3979205)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.06/4.34 % (3979205)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.06/4.34 % (3979205)CaDiCaL version: 2.1.3 % 24.06/4.34 % (3979205)Termination reason: Refutation not found, incomplete strategy % 24.06/4.34 % (3979205)Time elapsed: 0.029 s % 24.06/4.34 % (3979205)Peak memory usage: 116 MB % 24.06/4.34 % (3979205)Instructions burned: 6 (million) % 24.06/4.34 % (3979195)Instruction limit reached! % 24.06/4.34 % (3979195)------------------------------ % 24.06/4.34 % (3979195)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.38/4.69 % (3979195)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.38/4.69 % (3979195)CaDiCaL version: 2.1.3 % 25.38/4.69 % (3979195)Termination reason: Instruction limit % 25.38/4.69 % (3979195)Termination phase: Saturation % 25.38/4.69 % (3979195)Time elapsed: 0.303 s % 25.38/4.69 % (3979195)Peak memory usage: 121 MB % 25.38/4.69 % (3979195)Instructions burned: 388 (million) % 25.38/4.69 % (3979204)------------------------------ % 25.38/4.69 % (3979204)------------------------------ % 25.38/4.69 % (3979207)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=3985516463:s2pl=no:i=235:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2972 on theBenchmark for (2972ds/235Mi) % 25.38/4.69 % (3979210)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=1752486114:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2972 on theBenchmark for (2972ds/273Mi) % 25.38/4.69 % (3979207)Refutation not found, incomplete strategy % 25.38/4.69 % (3979207)------------------------------ % 25.38/4.69 % (3979207)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.38/4.69 % (3979207)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.38/4.69 % (3979207)CaDiCaL version: 2.1.3 % 25.38/4.69 % (3979207)Termination reason: Refutation not found, incomplete strategy % 25.38/4.69 % (3979207)Time elapsed: 0.029 s % 25.38/4.69 % (3979207)Peak memory usage: 116 MB % 25.38/4.69 % (3979207)Instructions burned: 6 (million) % 25.38/4.69 % (3979200)------------------------------ % 25.38/4.69 % (3979200)------------------------------ % 25.38/4.69 % (3979211)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=2291464250:i=146:doe=on:rtra=on_2972 on theBenchmark for (2972ds/146Mi) % 25.38/4.69 % (3979213)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=2548759151:i=4428:doe=on:fsr=off:rtra=on_2971 on theBenchmark for (2971ds/4428Mi) % 25.38/4.69 % (3979202)------------------------------ % 25.38/4.69 % (3979202)------------------------------ % 25.38/4.69 % (3979205)------------------------------ % 25.38/4.69 % (3979205)------------------------------ % 25.38/4.69 % (3979211)Instruction limit reached! % 25.38/4.69 % (3979211)------------------------------ % 25.38/4.69 % (3979211)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.38/4.69 % (3979211)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.38/4.69 % (3979211)CaDiCaL version: 2.1.3 % 25.38/4.69 % (3979211)Termination reason: Instruction limit % 25.38/4.69 % (3979211)Termination phase: Saturation % 25.38/4.69 % (3979211)Time elapsed: 0.093 s % 25.38/4.69 % (3979211)Peak memory usage: 90 MB % 25.38/4.69 % (3979211)Instructions burned: 146 (million) % 25.38/4.69 % (3979215)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=2022926013:avsq=on:i=276:avsqr=1,2:rtra=on_2971 on theBenchmark for (2971ds/276Mi) % 25.38/4.69 % (3979210)Instruction limit reached! % 25.38/4.69 % (3979210)------------------------------ % 25.38/4.69 % (3979210)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.38/4.69 % (3979210)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.38/4.69 % (3979210)CaDiCaL version: 2.1.3 % 25.38/4.69 % (3979210)Termination reason: Instruction limit % 25.38/4.69 % (3979210)Termination phase: Saturation % 25.38/4.69 % (3979210)Time elapsed: 0.166 s % 25.38/4.69 % (3979210)Peak memory usage: 92 MB % 25.38/4.69 % (3979210)Instructions burned: 274 (million) % 25.38/4.69 % (3979218)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=1747986301:i=1052:rtra=on_2970 on theBenchmark for (2970ds/1052Mi) % 25.38/4.69 % (3979207)------------------------------ % 25.38/4.69 % (3979207)------------------------------ % 25.38/4.69 % (3979220)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=3059060378:st=5:i=1054:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2969 on theBenchmark for (2969ds/1054Mi) % 25.38/4.69 % (3979219)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=2021188959:i=655:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2969 on theBenchmark for (2969ds/655Mi) % 25.38/4.69 % (3979220)Refutation not found, incomplete strategy % 25.38/4.69 % (3979220)------------------------------ % 25.38/4.69 % (3979220)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.90/5.09 % (3979219)Refutation not found, incomplete strategy % 29.90/5.09 % (3979219)------------------------------ % 29.90/5.09 % (3979219)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.90/5.09 % (3979220)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.90/5.09 % (3979219)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.90/5.09 % (3979220)CaDiCaL version: 2.1.3 % 29.90/5.09 % (3979220)Termination reason: Refutation not found, incomplete strategy % 29.90/5.09 % (3979220)Time elapsed: 0.001 s % 29.90/5.09 % (3979219)CaDiCaL version: 2.1.3 % 29.90/5.09 % (3979220)Peak memory usage: 89 MB % 29.90/5.09 % (3979219)Termination reason: Refutation not found, incomplete strategy % 29.90/5.09 % (3979219)Time elapsed: 0.001 s % 29.90/5.09 % (3979219)Peak memory usage: 89 MB % 29.90/5.09 % (3979222)lrs-1002_1_to=kbo:sas=z3:si=on:norm_ineq=on:sos=on:tha=some:random_seed=3619002892:i=107:rtra=on_2969 on theBenchmark for (2969ds/107Mi) % 29.90/5.09 % (3979215)Instruction limit reached! % 29.90/5.09 % (3979215)------------------------------ % 29.90/5.09 % (3979215)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.90/5.09 % (3979215)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.90/5.09 % (3979215)CaDiCaL version: 2.1.3 % 29.90/5.09 % (3979215)Termination reason: Instruction limit % 29.90/5.09 % (3979215)Termination phase: Saturation % 29.90/5.09 % (3979215)Time elapsed: 0.158 s % 29.90/5.09 % (3979215)Peak memory usage: 133 MB % 29.90/5.09 % (3979215)Instructions burned: 279 (million) % 29.90/5.09 % (3979222)Refutation not found, incomplete strategy % 29.90/5.09 % (3979222)------------------------------ % 29.90/5.09 % (3979222)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.90/5.09 % (3979222)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.90/5.09 % (3979222)CaDiCaL version: 2.1.3 % 29.90/5.09 % (3979222)Termination reason: Refutation not found, incomplete strategy % 29.90/5.09 % (3979222)Time elapsed: 0.029 s % 29.90/5.09 % (3979222)Peak memory usage: 116 MB % 29.90/5.09 % (3979222)Instructions burned: 6 (million) % 29.90/5.09 % (3979224)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=1889143694:s2a=on:i=450:doe=on:nm=32:rtra=on_2968 on theBenchmark for (2968ds/450Mi) % 29.90/5.09 % (3979224)Refutation not found, incomplete strategy % 29.90/5.09 % (3979224)------------------------------ % 29.90/5.09 % (3979224)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.90/5.09 % (3979224)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.90/5.09 % (3979224)CaDiCaL version: 2.1.3 % 29.90/5.09 % (3979224)Termination reason: Refutation not found, incomplete strategy % 29.90/5.09 % (3979224)Time elapsed: 0.052 s % 29.90/5.09 % (3979224)Peak memory usage: 133 MB % 29.90/5.09 % (3979224)Instructions burned: 11 (million) % 29.90/5.09 % (3979228)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 % 29.90/5.09 % (3979228)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=2441344109:i=1090:aac=none:nm=0:rtra=on:rawr=on_2968 on theBenchmark for (2968ds/1090Mi) % 29.90/5.09 % (3979228)Refutation not found, incomplete strategy % 29.90/5.09 % (3979228)------------------------------ % 29.90/5.09 % (3979228)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.90/5.09 % (3979228)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.90/5.09 % (3979228)CaDiCaL version: 2.1.3 % 29.90/5.09 % (3979228)Termination reason: Refutation not found, incomplete strategy % 29.90/5.09 % (3979228)Time elapsed: 0.028 s % 29.90/5.09 % (3979228)Peak memory usage: 116 MB % 29.90/5.09 % (3979228)Instructions burned: 6 (million) % 29.90/5.09 % (3979220)------------------------------ % 29.90/5.09 % (3979220)------------------------------ % 29.90/5.09 % (3979219)------------------------------ % 29.90/5.09 % (3979219)------------------------------ % 29.90/5.09 % (3979222)------------------------------ % 29.90/5.09 % (3979222)------------------------------ % 29.90/5.09 % (3979218)Instruction limit reached! % 29.90/5.09 % (3979218)------------------------------ % 29.90/5.09 % (3979218)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.90/5.09 % (3979218)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.20/5.32 % (3979218)CaDiCaL version: 2.1.3 % 31.20/5.32 % (3979218)Termination reason: Instruction limit % 31.20/5.32 % (3979218)Termination phase: Saturation % 31.20/5.32 % (3979218)Time elapsed: 0.377 s % 31.20/5.32 % (3979218)Peak memory usage: 88 MB % 31.20/5.32 % (3979218)Instructions burned: 1055 (million) % 31.20/5.32 % (3979231)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=2494194620:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2966 on theBenchmark for (2966ds/130Mi) % 31.20/5.32 % (3979232)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=1517732917:i=312:kws=inv_frequency:nm=20:rtra=on_2966 on theBenchmark for (2966ds/312Mi) % 31.20/5.32 % (3979224)------------------------------ % 31.20/5.32 % (3979224)------------------------------ % 31.20/5.32 % (3979231)Refutation not found, incomplete strategy % 31.20/5.32 % (3979231)------------------------------ % 31.20/5.32 % (3979231)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.20/5.32 % (3979231)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.20/5.32 % (3979231)CaDiCaL version: 2.1.3 % 31.20/5.32 % (3979231)Termination reason: Refutation not found, incomplete strategy % 31.20/5.32 % (3979231)Time elapsed: 0.028 s % 31.20/5.32 % (3979231)Peak memory usage: 116 MB % 31.20/5.32 % (3979231)Instructions burned: 6 (million) % 31.20/5.32 % (3979233)ott+10_1_to=kbo:sil=64000:si=on:sp=reverse_frequency:sos=on:random_seed=3834553852:i=491:doe=on:rtra=on:gtg=position_2965 on theBenchmark for (2965ds/491Mi) % 31.20/5.32 % (3979233)Refutation not found, incomplete strategy % 31.20/5.32 % (3979233)------------------------------ % 31.20/5.32 % (3979233)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.20/5.32 % (3979233)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.20/5.32 % (3979233)CaDiCaL version: 2.1.3 % 31.20/5.32 % (3979233)Termination reason: Refutation not found, incomplete strategy % 31.20/5.32 % (3979233)Time elapsed: 0.002 s % 31.20/5.32 % (3979233)Peak memory usage: 89 MB % 31.20/5.32 % (3979233)Instructions burned: 1 (million) % 31.20/5.32 % (3979228)------------------------------ % 31.20/5.32 % (3979228)------------------------------ % 31.20/5.32 % (3979234)ott+1011_4:1_to=lpo:sil=64000:si=on:spb=intro:random_seed=849975439:s2a=on:i=835:s2at=2:rtra=on_2965 on theBenchmark for (2965ds/835Mi) % 31.20/5.32 % (3979237)ott+1011_2_to=lpo:sil=128000:si=on:sos=on:random_seed=1091045661:i=307:bd=preordered:av=off:rtra=on:ev=cautious_2964 on theBenchmark for (2964ds/307Mi) % 31.20/5.32 % (3979237)Refutation not found, incomplete strategy % 31.20/5.32 % (3979237)------------------------------ % 31.20/5.32 % (3979237)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.20/5.32 % (3979237)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.20/5.32 % (3979237)CaDiCaL version: 2.1.3 % 31.20/5.32 % (3979237)Termination reason: Refutation not found, incomplete strategy % 31.20/5.32 % (3979237)Time elapsed: 0.002 s % 31.20/5.32 % (3979237)Peak memory usage: 89 MB % 31.20/5.32 % (3979237)Instructions burned: 1 (million) % 31.20/5.32 % (3979232)Instruction limit reached! % 31.20/5.32 % (3979232)------------------------------ % 31.20/5.32 % (3979232)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.20/5.32 % (3979232)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.20/5.32 % (3979232)CaDiCaL version: 2.1.3 % 31.20/5.32 % (3979232)Termination reason: Instruction limit % 31.20/5.32 % (3979232)Termination phase: Saturation % 31.20/5.32 % (3979232)Time elapsed: 0.223 s % 31.20/5.32 % (3979232)Peak memory usage: 119 MB % 31.20/5.32 % (3979232)Instructions burned: 312 (million) % 31.20/5.32 % (3979240)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=1776504422:i=776:doe=on:rtra=on_2963 on theBenchmark for (2963ds/776Mi) % 31.20/5.32 % (3979231)------------------------------ % 31.20/5.32 % (3979231)------------------------------ % 31.20/5.32 % (3979240)Refutation not found, incomplete strategy % 31.20/5.32 % (3979240)------------------------------ % 31.20/5.32 % (3979240)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.20/5.32 % (3979240)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.20/5.32 % (3979240)CaDiCaL version: 2.1.3 % 31.20/5.32 % (3979240)Termination reason: Refutation not found, incomplete strategy % 31.20/5.32 % (3979240)Time elapsed: 0.030 s % 31.20/5.32 % (3979240)Peak memory usage: 116 MB % 31.20/5.32 % (3979240)Instructions burned: 8 (million) % 31.20/5.32 % (3979233)------------------------------ % 32.47/5.68 % (3979233)------------------------------ % 32.47/5.68 % (3979213)Instruction limit reached! % 32.47/5.68 % (3979213)------------------------------ % 32.47/5.68 % (3979213)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.47/5.68 % (3979213)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.47/5.68 % (3979213)CaDiCaL version: 2.1.3 % 32.47/5.68 % (3979213)Termination reason: Instruction limit % 32.47/5.68 % (3979213)Termination phase: Saturation % 32.47/5.68 % (3979213)Time elapsed: 0.939 s % 32.47/5.68 % (3979213)Peak memory usage: 102 MB % 32.47/5.68 % (3979213)Instructions burned: 4433 (million) % 32.47/5.68 % (3979242)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=3949614650:s2a=on:i=646:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2962 on theBenchmark for (2962ds/646Mi) % 32.47/5.68 % (3979237)------------------------------ % 32.47/5.68 % (3979237)------------------------------ % 32.47/5.68 % (3979244)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=3828365490:thitd=on:cond=fast:i=784:nm=30:rtra=on:gtg=all:tac=axiom_2962 on theBenchmark for (2962ds/784Mi) % 32.47/5.68 % (3979242)Refutation not found, incomplete strategy % 32.47/5.68 % (3979242)------------------------------ % 32.47/5.68 % (3979242)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.47/5.68 % (3979242)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.47/5.68 % (3979242)CaDiCaL version: 2.1.3 % 32.47/5.68 % (3979242)Termination reason: Refutation not found, incomplete strategy % 32.47/5.68 % (3979242)Time elapsed: 0.054 s % 32.47/5.68 % (3979242)Peak memory usage: 133 MB % 32.47/5.68 % (3979242)Instructions burned: 11 (million) % 32.47/5.68 % (3979246)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=121050511:s2pl=no:i=246:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2961 on theBenchmark for (2961ds/246Mi) % 32.47/5.68 % (3979246)Refutation not found, incomplete strategy % 32.47/5.68 % (3979246)------------------------------ % 32.47/5.68 % (3979246)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.47/5.68 % (3979246)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.47/5.68 % (3979246)CaDiCaL version: 2.1.3 % 32.47/5.68 % (3979246)Termination reason: Refutation not found, incomplete strategy % 32.47/5.68 % (3979246)Time elapsed: 0.017 s % 32.47/5.68 % (3979246)Peak memory usage: 116 MB % 32.47/5.68 % (3979246)Instructions burned: 6 (million) % 32.47/5.68 % (3979245)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=3168773533:thitd=on:s2a=on:i=1131:add=on:canc=force:bd=all:rtra=on:tac=axiom:ev=off_2961 on theBenchmark for (2961ds/1131Mi) % 32.47/5.68 % (3979240)------------------------------ % 32.47/5.68 % (3979240)------------------------------ % 32.47/5.68 % (3979249)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=2181634528:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2960 on theBenchmark for (2960ds/775Mi) % 32.47/5.68 % (3979234)Instruction limit reached! % 32.47/5.68 % (3979234)------------------------------ % 32.47/5.68 % (3979234)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.47/5.68 % (3979234)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.47/5.68 % (3979234)CaDiCaL version: 2.1.3 % 32.47/5.68 % (3979234)Termination reason: Instruction limit % 32.47/5.68 % (3979234)Termination phase: Saturation % 32.47/5.68 % (3979234)Time elapsed: 0.453 s % 32.47/5.68 % (3979234)Peak memory usage: 93 MB % 32.47/5.68 % (3979234)Instructions burned: 836 (million) % 32.47/5.68 % (3979246)------------------------------ % 32.47/5.68 % (3979246)------------------------------ % 32.47/5.68 % (3979253)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=661922598:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2959 on theBenchmark for (2959ds/273Mi) % 32.47/5.68 % (3979242)------------------------------ % 32.47/5.68 % (3979242)------------------------------ % 32.47/5.68 % (3979255)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=1969019226:i=102:nm=16:rtra=on_2959 on theBenchmark for (2959ds/102Mi) % 32.47/5.68 % (3979256)lrs+10_1_to=lpo:sil=128000:si=on:bsr=unit_only:tha=off:random_seed=1195359464:avsq=on:s2a=on:i=1094:s2at=5:avsqr=4463,131072:rtra=on_2958 on theBenchmark for (2958ds/1094Mi) % 39.29/6.44 % (3979256)Refutation not found, incomplete strategy % 39.29/6.44 % (3979256)------------------------------ % 39.29/6.44 % (3979256)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.29/6.44 % (3979256)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.29/6.44 % (3979256)CaDiCaL version: 2.1.3 % 39.29/6.44 % (3979256)Termination reason: Refutation not found, incomplete strategy % 39.29/6.44 % (3979256)Time elapsed: 0.0000 s % 39.29/6.44 % (3979256)Peak memory usage: 88 MB % 39.29/6.44 % (3979255)Instruction limit reached! % 39.29/6.44 % (3979255)------------------------------ % 39.29/6.44 % (3979255)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.29/6.44 % (3979255)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.29/6.44 % (3979255)CaDiCaL version: 2.1.3 % 39.29/6.44 % (3979255)Termination reason: Instruction limit % 39.29/6.44 % (3979255)Termination phase: Saturation % 39.29/6.44 % (3979255)Time elapsed: 0.044 s % 39.29/6.44 % (3979255)Peak memory usage: 88 MB % 39.29/6.44 % (3979255)Instructions burned: 103 (million) % 39.29/6.44 % (3979244)Instruction limit reached! % 39.29/6.44 % (3979244)------------------------------ % 39.29/6.44 % (3979244)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.29/6.44 % (3979244)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.29/6.44 % (3979244)CaDiCaL version: 2.1.3 % 39.29/6.44 % (3979244)Termination reason: Instruction limit % 39.29/6.44 % (3979244)Termination phase: Saturation % 39.29/6.44 % (3979244)Time elapsed: 0.388 s % 39.29/6.44 % (3979244)Peak memory usage: 117 MB % 39.29/6.44 % (3979244)Instructions burned: 785 (million) % 39.29/6.44 % (3979258)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=539848508:i=6400:doe=on:fsr=off:rtra=on_2958 on theBenchmark for (2958ds/6400Mi) % 39.29/6.44 % (3979253)Instruction limit reached! % 39.29/6.44 % (3979253)------------------------------ % 39.29/6.44 % (3979253)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.29/6.44 % (3979253)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.29/6.44 % (3979253)CaDiCaL version: 2.1.3 % 39.29/6.44 % (3979253)Termination reason: Instruction limit % 39.29/6.44 % (3979253)Termination phase: Saturation % 39.29/6.44 % (3979253)Time elapsed: 0.167 s % 39.29/6.44 % (3979253)Peak memory usage: 92 MB % 39.29/6.44 % (3979253)Instructions burned: 275 (million) % 39.29/6.44 % (3979261)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=1029505004:i=868:doe=on:nm=0:rtra=on:gtg=exists_sym_2957 on theBenchmark for (2957ds/868Mi) % 39.29/6.44 % (3979256)------------------------------ % 39.29/6.44 % (3979256)------------------------------ % 39.29/6.44 % (3979261)Refutation not found, incomplete strategy % 39.29/6.44 % (3979261)------------------------------ % 39.29/6.44 % (3979261)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.29/6.44 % (3979261)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.29/6.44 % (3979261)CaDiCaL version: 2.1.3 % 39.29/6.44 % (3979261)Termination reason: Refutation not found, incomplete strategy % 39.29/6.44 % (3979261)Time elapsed: 0.029 s % 39.29/6.44 % (3979261)Peak memory usage: 116 MB % 39.29/6.44 % (3979261)Instructions burned: 6 (million) % 39.29/6.44 % (3979262)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=1827903855:i=1846:canc=cautious:fsr=off:rtra=on_2956 on theBenchmark for (2956ds/1846Mi) % 39.29/6.44 % (3979262)Refutation not found, incomplete strategy % 39.29/6.44 % (3979262)------------------------------ % 39.29/6.44 % (3979262)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.29/6.44 % (3979262)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.29/6.44 % (3979262)CaDiCaL version: 2.1.3 % 39.29/6.44 % (3979262)Termination reason: Refutation not found, incomplete strategy % 39.29/6.44 % (3979262)Time elapsed: 0.001 s % 39.29/6.44 % (3979262)Peak memory usage: 89 MB % 39.29/6.44 % (3979249)Instruction limit reached! % 39.29/6.44 % (3979249)------------------------------ % 39.29/6.44 % (3979249)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.29/6.44 % (3979249)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.29/6.44 % (3979249)CaDiCaL version: 2.1.3 % 49.62/7.92 % (3979249)Termination reason: Instruction limit % 49.62/7.92 % (3979249)Termination phase: Saturation % 49.62/7.92 % (3979249)Time elapsed: 0.397 s % 49.62/7.92 % (3979249)Peak memory usage: 91 MB % 49.62/7.92 % (3979249)Instructions burned: 775 (million) % 49.62/7.92 % (3979266)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=3369018512:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2956 on theBenchmark for (2956ds/273Mi) % 49.62/7.92 % (3979264)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=2606126471:s2a=on:i=36816:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2956 on theBenchmark for (2956ds/36816Mi) % 49.62/7.92 % (3979264)Refutation not found, incomplete strategy % 49.62/7.92 % (3979264)------------------------------ % 49.62/7.92 % (3979264)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 49.62/7.92 % (3979264)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 49.62/7.92 % (3979264)CaDiCaL version: 2.1.3 % 49.62/7.92 % (3979264)Termination reason: Refutation not found, incomplete strategy % 49.62/7.93 % (3979264)Time elapsed: 0.001 s % 49.62/7.93 % (3979264)Peak memory usage: 88 MB % 49.62/7.93 % (3979266)Instruction limit reached! % 49.62/7.93 % (3979266)------------------------------ % 49.62/7.93 % (3979266)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 49.62/7.93 % (3979266)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 49.62/7.93 % (3979266)CaDiCaL version: 2.1.3 % 49.62/7.93 % (3979266)Termination reason: Instruction limit % 49.62/7.93 % (3979266)Termination phase: Saturation % 49.62/7.93 % (3979266)Time elapsed: 0.088 s % 49.62/7.93 % (3979266)Peak memory usage: 92 MB % 49.62/7.93 % (3979266)Instructions burned: 273 (million) % 49.62/7.93 % (3979268)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=2185681950:i=863:doe=on:nm=0:rtra=on:gtg=exists_sym_2955 on theBenchmark for (2955ds/863Mi) % 49.62/7.93 % (3979268)Refutation not found, incomplete strategy % 49.62/7.93 % (3979268)------------------------------ % 49.62/7.93 % (3979268)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 49.62/7.93 % (3979268)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 49.62/7.93 % (3979268)CaDiCaL version: 2.1.3 % 49.62/7.93 % (3979268)Termination reason: Refutation not found, incomplete strategy % 49.62/7.93 % (3979268)Time elapsed: 0.029 s % 49.62/7.93 % (3979268)Peak memory usage: 116 MB % 49.62/7.93 % (3979268)Instructions burned: 6 (million) % 49.62/7.93 % (3979261)------------------------------ % 49.62/7.93 % (3979261)------------------------------ % 49.62/7.93 % (3979271)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=1774457343:i=5811:kws=precedence:nm=0:rtra=on_2954 on theBenchmark for (2954ds/5811Mi) % 49.62/7.93 % (3979271)Refutation not found, incomplete strategy % 49.62/7.93 % (3979271)------------------------------ % 49.62/7.93 % (3979271)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 49.62/7.93 % (3979271)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 49.62/7.93 % (3979271)CaDiCaL version: 2.1.3 % 49.62/7.93 % (3979271)Termination reason: Refutation not found, incomplete strategy % 49.62/7.93 % (3979271)Time elapsed: 0.017 s % 49.62/7.93 % (3979271)Peak memory usage: 116 MB % 49.62/7.93 % (3979271)Instructions burned: 6 (million) % 49.62/7.93 % (3979245)Instruction limit reached! % 49.62/7.93 % (3979245)------------------------------ % 49.62/7.93 % (3979245)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 49.62/7.93 % (3979245)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 49.62/7.93 % (3979245)CaDiCaL version: 2.1.3 % 49.62/7.93 % (3979245)Termination reason: Instruction limit % 49.62/7.93 % (3979245)Termination phase: Saturation % 49.62/7.93 % (3979245)Time elapsed: 0.701 s % 49.62/7.93 % (3979245)Peak memory usage: 120 MB % 49.62/7.93 % (3979245)Instructions burned: 1132 (million) % 49.62/7.93 % (3979262)------------------------------ % 49.62/7.93 % (3979262)------------------------------ % 49.62/7.93 % (3979264)------------------------------ % 49.62/7.93 % (3979264)------------------------------ % 49.62/7.93 % (3979274)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=518475607:i=2216:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2953 on theBenchmark for (2953ds/2216Mi) % 49.62/7.93 % (3979275)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=155764340:i=801:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2953 on theBenchmark for (2953ds/801Mi) % 70.86/10.89 % (3979275)Refutation not found, incomplete strategy % 70.86/10.89 % (3979275)------------------------------ % 70.86/10.89 % (3979275)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 70.86/10.89 % (3979275)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 70.86/10.89 % (3979275)CaDiCaL version: 2.1.3 % 70.86/10.89 % (3979275)Termination reason: Refutation not found, incomplete strategy % 70.86/10.89 % (3979275)Time elapsed: 0.001 s % 70.86/10.89 % (3979275)Peak memory usage: 89 MB % 70.86/10.89 % (3979271)------------------------------ % 70.86/10.89 % (3979271)------------------------------ % 70.86/10.89 % (3979276)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=1628680554:st=5:i=1026:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2953 on theBenchmark for (2953ds/1026Mi) % 70.86/10.89 % (3979276)Refutation not found, incomplete strategy % 70.86/10.89 % (3979276)------------------------------ % 70.86/10.89 % (3979276)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 70.86/10.89 % (3979276)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 70.86/10.89 % (3979276)CaDiCaL version: 2.1.3 % 70.86/10.89 % (3979276)Termination reason: Refutation not found, incomplete strategy % 70.86/10.89 % (3979276)Time elapsed: 0.001 s % 70.86/10.89 % (3979276)Peak memory usage: 89 MB % 70.86/10.89 % (3979268)------------------------------ % 70.86/10.89 % (3979268)------------------------------ % 70.86/10.89 % (3979277)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=604730948:i=3509:rtra=on_2952 on theBenchmark for (2952ds/3509Mi) % 70.86/10.89 % (3979281)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=136315730:st=2:i=2127:sd=12:ep=R:rtra=on:ss=axioms_2951 on theBenchmark for (2951ds/2127Mi) % 70.86/10.89 % (3979282)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=3159598191:i=1959:rtra=on:fsd=on:proc=on_2951 on theBenchmark for (2951ds/1959Mi) % 70.86/10.89 % (3979282)Refutation not found, incomplete strategy % 70.86/10.89 % (3979282)------------------------------ % 70.86/10.89 % (3979282)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 70.86/10.89 % (3979282)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 70.86/10.89 % (3979282)CaDiCaL version: 2.1.3 % 70.86/10.89 % (3979282)Termination reason: Refutation not found, incomplete strategy % 70.86/10.89 % (3979282)Time elapsed: 0.028 s % 70.86/10.89 % (3979282)Peak memory usage: 116 MB % 70.86/10.89 % (3979282)Instructions burned: 6 (million) % 70.86/10.89 % (3979275)------------------------------ % 70.86/10.89 % (3979275)------------------------------ % 70.86/10.89 % (3979276)------------------------------ % 70.86/10.89 % (3979276)------------------------------ % 70.86/10.89 % (3979286)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=2097633166:s2a=on:i=3553:nm=0:rtra=on_2949 on theBenchmark for (2949ds/3553Mi) % 70.86/10.89 % (3979287)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=2881282450:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2949 on theBenchmark for (2949ds/3201Mi) % 70.86/10.89 % (3979282)------------------------------ % 70.86/10.89 % (3979282)------------------------------ % 70.86/10.89 % (3979290)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=2084606657:thitd=on:cond=on:i=4093:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2947 on theBenchmark for (2947ds/4093Mi) % 70.86/10.89 % (3979281)Instruction limit reached! % 70.86/10.89 % (3979281)------------------------------ % 70.86/10.89 % (3979281)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 70.86/10.89 % (3979281)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 70.86/10.89 % (3979281)CaDiCaL version: 2.1.3 % 70.86/10.89 % (3979281)Termination reason: Instruction limit % 70.86/10.89 % (3979281)Termination phase: Saturation % 70.86/10.89 % (3979281)Time elapsed: 0.549 s % 70.86/10.89 % (3979281)Peak memory usage: 101 MB % 70.86/10.89 % (3979281)Instructions burned: 2127 (million) % 70.86/10.89 % (3979292)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=3359682697:cond=fast:i=21173:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2945 on theBenchmark for (2945ds/21173Mi) % 82.43/12.57 % (3979274)Instruction limit reached! % 82.43/12.57 % (3979274)------------------------------ % 82.43/12.57 % (3979274)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 82.43/12.57 % (3979274)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 82.43/12.57 % (3979274)CaDiCaL version: 2.1.3 % 82.43/12.57 % (3979274)Termination reason: Instruction limit % 82.43/12.57 % (3979274)Termination phase: Saturation % 82.43/12.57 % (3979274)Time elapsed: 1.141 s % 82.43/12.57 % (3979274)Peak memory usage: 131 MB % 82.43/12.57 % (3979274)Instructions burned: 2217 (million) % 82.43/12.57 % (3979294)lrs+11_1_to=lpo:thi=all:sas=z3:si=on:fd=off:sac=on:slsq=on:random_seed=3117597945:avsq=on:i=10544:avsqr=17,4:canc=force:rtra=on:gtg=exists_top:er=filter_2940 on theBenchmark for (2940ds/10544Mi) % 82.43/12.57 % (3979277)Instruction limit reached! % 82.43/12.57 % (3979277)------------------------------ % 82.43/12.57 % (3979277)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 82.43/12.57 % (3979277)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 82.43/12.57 % (3979277)CaDiCaL version: 2.1.3 % 82.43/12.57 % (3979277)Termination reason: Instruction limit % 82.43/12.57 % (3979277)Termination phase: Saturation % 82.43/12.57 % (3979277)Time elapsed: 1.575 s % 82.43/12.57 % (3979277)Peak memory usage: 102 MB % 82.43/12.57 % (3979277)Instructions burned: 3509 (million) % 82.43/12.57 % (3979296)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=1443120845:avsq=on:i=1262:avsqr=1,16:rtra=on:rawr=on_2935 on theBenchmark for (2935ds/1262Mi) % 82.43/12.57 % (3979296)Refutation not found, incomplete strategy % 82.43/12.57 % (3979296)------------------------------ % 82.43/12.57 % (3979296)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 82.43/12.57 % (3979296)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 82.43/12.57 % (3979296)CaDiCaL version: 2.1.3 % 82.43/12.57 % (3979296)Termination reason: Refutation not found, incomplete strategy % 82.43/12.57 % (3979296)Time elapsed: 0.028 s % 82.43/12.57 % (3979296)Peak memory usage: 116 MB % 82.43/12.57 % (3979296)Instructions burned: 6 (million) % 82.43/12.57 % (3979287)Instruction limit reached! % 82.43/12.57 % (3979287)------------------------------ % 82.43/12.57 % (3979287)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 82.43/12.57 % (3979287)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 82.43/12.57 % (3979287)CaDiCaL version: 2.1.3 % 82.43/12.57 % (3979287)Termination reason: Instruction limit % 82.43/12.57 % (3979287)Termination phase: Saturation % 82.43/12.57 % (3979287)Time elapsed: 1.452 s % 82.43/12.57 % (3979287)Peak memory usage: 97 MB % 82.43/12.57 % (3979287)Instructions burned: 3203 (million) % 82.43/12.57 % (3979298)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=3971562181:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2933 on theBenchmark for (2933ds/775Mi) % 82.43/12.57 % (3979296)------------------------------ % 82.43/12.57 % (3979296)------------------------------ % 82.43/12.57 % (3979258)Instruction limit reached! % 82.43/12.57 % (3979258)------------------------------ % 82.43/12.57 % (3979258)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 82.43/12.57 % (3979258)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 82.43/12.57 % (3979258)CaDiCaL version: 2.1.3 % 82.43/12.57 % (3979258)Termination reason: Instruction limit % 82.43/12.57 % (3979258)Termination phase: Saturation % 82.43/12.57 % (3979258)Time elapsed: 2.603 s % 82.43/12.57 % (3979258)Peak memory usage: 112 MB % 82.43/12.57 % (3979258)Instructions burned: 6402 (million) % 82.43/12.57 % (3979300)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=701926181:i=270:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2931 on theBenchmark for (2931ds/270Mi) % 82.43/12.57 % (3979286)Instruction limit reached! % 82.43/12.57 % (3979286)------------------------------ % 82.43/12.57 % (3979286)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 82.43/12.57 % (3979286)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 82.43/12.57 % (3979286)CaDiCaL version: 2.1.3 % 82.43/12.57 % (3979286)Termination reason: Instruction limit % 82.43/12.57 % (3979286)Termination phase: Saturation % 82.43/12.57 % (3979286)Time elapsed: 1.807 s % 82.43/12.57 % (3979286)Peak memory usage: 100 MB % 82.43/12.57 % (3979286)Instructions burned: 3553 (million) % 82.43/12.57 % (3979301)ott+10_128_isp=bottom:to=lpo:sil=128000:si=on:urr=on:uwa=alasca_main:sac=on:slsq=on:random_seed=3301299827:i=17165:aac=none:doe=on:rtra=on:gtg=exists_all_2930 on theBenchmark for (2930ds/17165Mi) % 91.20/13.81 % (3979303)lrs+2_10_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_main:tha=some:random_seed=3713518062:s2a=on:i=13094:s2at=-1:rtra=on_2929 on theBenchmark for (2929ds/13094Mi) % 91.20/13.81 % (3979300)Instruction limit reached! % 91.20/13.81 % (3979300)------------------------------ % 91.20/13.81 % (3979300)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 91.20/13.81 % (3979300)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.20/13.81 % (3979300)CaDiCaL version: 2.1.3 % 91.20/13.81 % (3979300)Termination reason: Instruction limit % 91.20/13.81 % (3979300)Termination phase: Saturation % 91.20/13.81 % (3979300)Time elapsed: 0.166 s % 91.20/13.81 % (3979300)Peak memory usage: 92 MB % 91.20/13.81 % (3979300)Instructions burned: 272 (million) % 91.20/13.81 % (3979298)Instruction limit reached! % 91.20/13.81 % (3979298)------------------------------ % 91.20/13.81 % (3979298)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 91.20/13.81 % (3979298)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.20/13.81 % (3979298)CaDiCaL version: 2.1.3 % 91.20/13.81 % (3979298)Termination reason: Instruction limit % 91.20/13.81 % (3979298)Termination phase: Saturation % 91.20/13.81 % (3979298)Time elapsed: 0.390 s % 91.20/13.81 % (3979298)Peak memory usage: 91 MB % 91.20/13.81 % (3979298)Instructions burned: 776 (million) % 91.20/13.81 % (3979306)lrs+10_1_to=lpo:sil=128000:si=on:sp=occurrence:random_seed=3046476027:st=2:i=12633:rtra=on:ss=axioms_2928 on theBenchmark for (2928ds/12633Mi) % 91.20/13.81 % (3979307)dis+1011_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_frequency:lsd=20:nwc=3:random_seed=1474668860:i=1783:rtra=on:gtg=position_2927 on theBenchmark for (2927ds/1783Mi) % 91.20/13.81 % (3979290)Instruction limit reached! % 91.20/13.81 % (3979290)------------------------------ % 91.20/13.81 % (3979290)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 91.20/13.81 % (3979290)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.20/13.81 % (3979290)CaDiCaL version: 2.1.3 % 91.20/13.81 % (3979290)Termination reason: Instruction limit % 91.20/13.81 % (3979290)Termination phase: Saturation % 91.20/13.81 % (3979290)Time elapsed: 2.582 s % 91.20/13.81 % (3979290)Peak memory usage: 162 MB % 91.20/13.81 % (3979290)Instructions burned: 4094 (million) % 91.20/13.81 % (3979310)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=645418330:i=5451:aac=none:doe=on:nm=0:rtra=on:amm=off:gtg=position_2920 on theBenchmark for (2920ds/5451Mi) % 91.20/13.81 % (3979307)Instruction limit reached! % 91.20/13.81 % (3979307)------------------------------ % 91.20/13.81 % (3979307)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 91.20/13.81 % (3979307)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.20/13.81 % (3979307)CaDiCaL version: 2.1.3 % 91.20/13.81 % (3979307)Termination reason: Instruction limit % 91.20/13.81 % (3979307)Termination phase: Saturation % 91.20/13.81 % (3979307)Time elapsed: 1.070 s % 91.20/13.81 % (3979307)Peak memory usage: 130 MB % 91.20/13.81 % (3979307)Instructions burned: 1783 (million) % 91.20/13.81 % (3979312)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=897318867:i=4975:doe=on:nm=0:rtra=on:gtg=exists_sym_2915 on theBenchmark for (2915ds/4975Mi) % 91.20/13.81 % (3979312)Refutation not found, incomplete strategy % 91.20/13.81 % (3979312)------------------------------ % 91.20/13.81 % (3979312)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 91.20/13.81 % (3979312)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.20/13.81 % (3979312)CaDiCaL version: 2.1.3 % 91.20/13.81 % (3979312)Termination reason: Refutation not found, incomplete strategy % 91.20/13.81 % (3979312)Time elapsed: 0.028 s % 91.20/13.81 % (3979312)Peak memory usage: 116 MB % 91.20/13.81 % (3979312)Instructions burned: 6 (million) % 91.20/13.81 % (3979312)------------------------------ % 91.20/13.81 % (3979312)------------------------------ % 91.20/13.81 % (3979314)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=4204716481:i=2076:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2912 on theBenchmark for (2912ds/2076Mi) % 91.20/13.81 % (3979314)Instruction limit reached! % 91.20/13.81 % (3979314)------------------------------ % 112.04/16.67 % (3979314)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 112.04/16.67 % (3979314)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.04/16.67 % (3979314)CaDiCaL version: 2.1.3 % 112.04/16.67 % (3979314)Termination reason: Instruction limit % 112.04/16.67 % (3979314)Termination phase: Saturation % 112.04/16.67 % (3979314)Time elapsed: 1.111 s % 112.04/16.67 % (3979314)Peak memory usage: 125 MB % 112.04/16.67 % (3979314)Instructions burned: 2078 (million) % 112.04/16.67 % (3979316)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=684170282:i=5145:rtra=on_2899 on theBenchmark for (2899ds/5145Mi) % 112.04/16.67 % (3979292)Instruction limit reached! % 112.04/16.67 % (3979292)------------------------------ % 112.04/16.67 % (3979292)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 112.04/16.67 % (3979292)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.04/16.67 % (3979292)CaDiCaL version: 2.1.3 % 112.04/16.67 % (3979292)Termination reason: Instruction limit % 112.04/16.67 % (3979292)Termination phase: Saturation % 112.04/16.67 % (3979292)Time elapsed: 4.892 s % 112.04/16.67 % (3979292)Peak memory usage: 146 MB % 112.04/16.67 % (3979292)Instructions burned: 21177 (million) % 112.04/16.67 % (3979318)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=3821179148:i=3509:rtra=on_2895 on theBenchmark for (2895ds/3509Mi) % 112.04/16.67 % (3979310)Instruction limit reached! % 112.04/16.67 % (3979310)------------------------------ % 112.04/16.67 % (3979310)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 112.04/16.67 % (3979310)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.04/16.67 % (3979310)CaDiCaL version: 2.1.3 % 112.04/16.67 % (3979310)Termination reason: Instruction limit % 112.04/16.67 % (3979310)Termination phase: Saturation % 112.04/16.67 % (3979310)Time elapsed: 3.070 s % 112.04/16.67 % (3979310)Peak memory usage: 147 MB % 112.04/16.67 % (3979310)Instructions burned: 5451 (million) % 112.04/16.67 % (3979320)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=1409487097:st=2:i=13800:sd=12:ep=R:rtra=on:ss=axioms_2888 on theBenchmark for (2888ds/13800Mi) % 112.04/16.67 % (3979318)Instruction limit reached! % 112.04/16.67 % (3979318)------------------------------ % 112.04/16.67 % (3979318)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 112.04/16.67 % (3979318)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.04/16.67 % (3979318)CaDiCaL version: 2.1.3 % 112.04/16.67 % (3979318)Termination reason: Instruction limit % 112.04/16.67 % (3979318)Termination phase: Saturation % 112.04/16.67 % (3979318)Time elapsed: 0.781 s % 112.04/16.67 % (3979318)Peak memory usage: 106 MB % 112.04/16.67 % (3979318)Instructions burned: 3510 (million) % 112.04/16.67 % (3979322)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=2352930167:i=1412:rtra=on:fsd=on:proc=on_2886 on theBenchmark for (2886ds/1412Mi) % 112.04/16.67 % (3979322)Refutation not found, incomplete strategy % 112.04/16.67 % (3979322)------------------------------ % 112.04/16.67 % (3979322)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 112.04/16.67 % (3979322)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.04/16.67 % (3979322)CaDiCaL version: 2.1.3 % 112.04/16.67 % (3979322)Termination reason: Refutation not found, incomplete strategy % 112.04/16.67 % (3979322)Time elapsed: 0.017 s % 112.04/16.67 % (3979322)Peak memory usage: 116 MB % 112.04/16.67 % (3979322)Instructions burned: 6 (million) % 112.04/16.67 % (3979322)------------------------------ % 112.04/16.67 % (3979322)------------------------------ % 112.04/16.67 % (3979324)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 % 112.04/16.67 % (3979324)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=2336207691:i=11747:aac=none:nm=0:rtra=on:rawr=on_2883 on theBenchmark for (2883ds/11747Mi) % 112.04/16.67 % (3979324)Refutation not found, incomplete strategy % 112.04/16.67 % (3979324)------------------------------ % 112.04/16.67 % (3979324)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 112.04/16.67 % (3979324)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.04/16.67 % (3979324)CaDiCaL version: 2.1.3 % 112.04/16.67 % (3979324)Termination reason: Refutation not found, incomplete strategy % 173.54/25.32 % (3979324)Time elapsed: 0.017 s % 173.54/25.32 % (3979324)Peak memory usage: 116 MB % 173.54/25.32 % (3979324)Instructions burned: 6 (million) % 173.54/25.32 % (3979324)------------------------------ % 173.54/25.32 % (3979324)------------------------------ % 173.54/25.32 % (3979326)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=504546270:s2a=on:i=3553:nm=0:rtra=on_2881 on theBenchmark for (2881ds/3553Mi) % 173.54/25.32 % (3979303)Instruction limit reached! % 173.54/25.32 % (3979303)------------------------------ % 173.54/25.32 % (3979303)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 173.54/25.32 % (3979303)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 173.54/25.32 % (3979303)CaDiCaL version: 2.1.3 % 173.54/25.32 % (3979303)Termination reason: Instruction limit % 173.54/25.32 % (3979303)Termination phase: Saturation % 173.54/25.32 % (3979303)Time elapsed: 4.827 s % 173.54/25.32 % (3979303)Peak memory usage: 91 MB % 173.54/25.32 % (3979303)Instructions burned: 13095 (million) % 173.54/25.32 % (3979316)Instruction limit reached! % 173.54/25.32 % (3979316)------------------------------ % 173.54/25.32 % (3979316)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 173.54/25.32 % (3979316)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 173.54/25.32 % (3979316)CaDiCaL version: 2.1.3 % 173.54/25.32 % (3979316)Termination reason: Instruction limit % 173.54/25.32 % (3979316)Termination phase: Saturation % 173.54/25.32 % (3979316)Time elapsed: 1.827 s % 173.54/25.32 % (3979316)Peak memory usage: 89 MB % 173.54/25.32 % (3979316)Instructions burned: 5146 (million) % 173.54/25.32 % (3979328)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=3770799482:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2880 on theBenchmark for (2880ds/3201Mi) % 173.54/25.32 % (3979329)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=1553591736:thitd=on:cond=on:i=4081:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2880 on theBenchmark for (2880ds/4081Mi) % 173.54/25.32 % (3979306)Instruction limit reached! % 173.54/25.32 % (3979306)------------------------------ % 173.54/25.32 % (3979306)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 173.54/25.32 % (3979306)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 173.54/25.32 % (3979306)CaDiCaL version: 2.1.3 % 173.54/25.32 % (3979306)Termination reason: Instruction limit % 173.54/25.32 % (3979306)Termination phase: Saturation % 173.54/25.32 % (3979306)Time elapsed: 5.047 s % 173.54/25.32 % (3979306)Peak memory usage: 144 MB % 173.54/25.32 % (3979306)Instructions burned: 12634 (million) % 173.54/25.32 % (3979332)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=1043220319:cond=fast:i=20260:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2876 on theBenchmark for (2876ds/20260Mi) % 173.54/25.32 % (3979294)Instruction limit reached! % 173.54/25.32 % (3979294)------------------------------ % 173.54/25.32 % (3979294)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 173.54/25.32 % (3979294)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 173.54/25.32 % (3979294)CaDiCaL version: 2.1.3 % 173.54/25.32 % (3979294)Termination reason: Instruction limit % 173.54/25.32 % (3979294)Termination phase: Saturation % 173.54/25.32 % (3979294)Time elapsed: 6.519 s % 173.54/25.32 % (3979294)Peak memory usage: 210 MB % 173.54/25.32 % (3979294)Instructions burned: 10545 (million) % 173.54/25.32 % (3979335)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=627358679:s2a=on:i=58627:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2874 on theBenchmark for (2874ds/58627Mi) % 173.54/25.32 % (3979335)Refutation not found, incomplete strategy % 173.54/25.32 % (3979335)------------------------------ % 173.54/25.32 % (3979335)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 173.54/25.32 % (3979335)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 173.54/25.32 % (3979335)CaDiCaL version: 2.1.3 % 173.54/25.32 % (3979335)Termination reason: Refutation not found, incomplete strategy % 173.54/25.32 % (3979335)Time elapsed: 0.001 s % 173.54/25.32 % (3979335)Peak memory usage: 88 MB % 173.54/25.32 % (3979326)Instruction limit reached! % 173.54/25.32 % (3979326)------------------------------ % 173.54/25.32 % (3979326)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 173.54/25.32 % (3979326)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 195.84/28.45 % (3979326)CaDiCaL version: 2.1.3 % 195.84/28.45 % (3979326)Termination reason: Instruction limit % 195.84/28.45 % (3979326)Termination phase: Saturation % 195.84/28.45 % (3979326)Time elapsed: 1.0000 s % 195.84/28.45 % (3979326)Peak memory usage: 100 MB % 195.84/28.45 % (3979326)Instructions burned: 3556 (million) % 195.84/28.45 % (3979335)------------------------------ % 195.84/28.45 % (3979335)------------------------------ % 195.84/28.45 % (3979420)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=3821987154:avsq=on:i=6258:avsqr=1,16:rtra=on:rawr=on_2870 on theBenchmark for (2870ds/6258Mi) % 195.84/28.45 % (3979420)Refutation not found, incomplete strategy % 195.84/28.45 % (3979420)------------------------------ % 195.84/28.45 % (3979420)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 195.84/28.45 % (3979420)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 195.84/28.45 % (3979420)CaDiCaL version: 2.1.3 % 195.84/28.45 % (3979420)Termination reason: Refutation not found, incomplete strategy % 195.84/28.45 % (3979420)Time elapsed: 0.017 s % 195.84/28.45 % (3979420)Peak memory usage: 116 MB % 195.84/28.45 % (3979420)Instructions burned: 6 (million) % 195.84/28.45 % (3979425)ott+10_128_isp=bottom:to=lpo:sil=128000:si=on:urr=on:uwa=alasca_main:sac=on:slsq=on:random_seed=1995355657:i=34001:aac=none:doe=on:rtra=on:gtg=exists_all_2870 on theBenchmark for (2870ds/34001Mi) % 195.84/28.45 % (3979420)------------------------------ % 195.84/28.45 % (3979420)------------------------------ % 195.84/28.45 % (3979472)lrs+2_10_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_main:tha=some:random_seed=3602005489:s2a=on:i=71622:s2at=-1:rtra=on_2868 on theBenchmark for (2868ds/71622Mi) % 195.84/28.45 % (3979328)Instruction limit reached! % 195.84/28.45 % (3979328)------------------------------ % 195.84/28.45 % (3979328)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 195.84/28.45 % (3979328)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 195.84/28.45 % (3979328)CaDiCaL version: 2.1.3 % 195.84/28.45 % (3979328)Termination reason: Instruction limit % 195.84/28.45 % (3979328)Termination phase: Saturation % 195.84/28.45 % (3979328)Time elapsed: 1.479 s % 195.84/28.45 % (3979328)Peak memory usage: 95 MB % 195.84/28.45 % (3979328)Instructions burned: 3203 (million) % 195.84/28.45 % (3979527)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=1751483112:i=24001:kws=precedence:nm=0:rtra=on_2864 on theBenchmark for (2864ds/24001Mi) % 195.84/28.45 % (3979527)Refutation not found, incomplete strategy % 195.84/28.45 % (3979527)------------------------------ % 195.84/28.45 % (3979527)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 195.84/28.45 % (3979527)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 195.84/28.45 % (3979527)CaDiCaL version: 2.1.3 % 195.84/28.45 % (3979527)Termination reason: Refutation not found, incomplete strategy % 195.84/28.45 % (3979527)Time elapsed: 0.027 s % 195.84/28.45 % (3979527)Peak memory usage: 116 MB % 195.84/28.45 % (3979527)Instructions burned: 6 (million) % 195.84/28.45 % (3979527)------------------------------ % 195.84/28.45 % (3979527)------------------------------ % 195.84/28.45 % (3979571)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=336801915:i=2076:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2860 on theBenchmark for (2860ds/2076Mi) % 195.84/28.45 % (3979329)Instruction limit reached! % 195.84/28.45 % (3979329)------------------------------ % 195.84/28.45 % (3979329)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 195.84/28.45 % (3979329)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 195.84/28.45 % (3979329)CaDiCaL version: 2.1.3 % 195.84/28.45 % (3979329)Termination reason: Instruction limit % 195.84/28.45 % (3979329)Termination phase: Saturation % 195.84/28.45 % (3979329)Time elapsed: 2.146 s % 195.84/28.45 % (3979329)Peak memory usage: 148 MB % 195.84/28.45 % (3979329)Instructions burned: 4083 (million) % 195.84/28.45 % (3979587)dis+21_20_to=lakbo:si=on:alasca=on:sp=const_max:uwa=alasca_main:sac=on:random_seed=2608111399:s2a=on:i=83971:s2at=4:bd=all:ins=1:rtra=on_2857 on theBenchmark for (2857ds/83971Mi) % 195.84/28.45 % (3979571)Instruction limit reached! % 195.84/28.45 % (3979571)------------------------------ % 195.84/28.45 % (3979571)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 195.84/28.45 % (3979571)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 195.84/28.45 % (3979571)CaDiCaL version: 2.1.3 % 216.48/31.34 % (3979571)Termination reason: Instruction limit % 216.48/31.34 % (3979571)Termination phase: Saturation % 216.48/31.34 % (3979571)Time elapsed: 1.701 s % 216.48/31.34 % (3979571)Peak memory usage: 126 MB % 216.48/31.34 % (3979571)Instructions burned: 2076 (million) % 216.48/31.34 % (3979650)lrs+1011_5:1_to=lpo:sil=128000:sas=z3:si=on:norm_ineq=on:tha=some:random_seed=2740427283:i=83944:rtra=on_2841 on theBenchmark for (2841ds/83944Mi) % 216.48/31.34 % (3979301)Instruction limit reached! % 216.48/31.34 % (3979301)------------------------------ % 216.48/31.34 % (3979301)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 216.48/31.34 % (3979301)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 216.48/31.34 % (3979301)CaDiCaL version: 2.1.3 % 216.48/31.34 % (3979301)Termination reason: Instruction limit % 216.48/31.34 % (3979301)Termination phase: Saturation % 216.48/31.34 % (3979301)Time elapsed: 9.759 s % 216.48/31.34 % (3979301)Peak memory usage: 212 MB % 216.48/31.34 % (3979301)Instructions burned: 17166 (million) % 216.48/31.34 % (3979656)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=705732717:i=9201:rtra=on_2831 on theBenchmark for (2831ds/9201Mi) % 216.48/31.34 % (3979320)Instruction limit reached! % 216.48/31.34 % (3979320)------------------------------ % 216.48/31.34 % (3979320)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 216.48/31.34 % (3979320)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 216.48/31.34 % (3979320)CaDiCaL version: 2.1.3 % 216.48/31.34 % (3979320)Termination reason: Instruction limit % 216.48/31.34 % (3979320)Termination phase: Saturation % 216.48/31.34 % (3979320)Time elapsed: 8.813 s % 216.48/31.34 % (3979320)Peak memory usage: 138 MB % 216.48/31.34 % (3979320)Instructions burned: 13800 (million) % 216.48/31.34 % (3979676)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 % 216.48/31.34 % (3979676)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=1588964040:i=6806:aac=none:nm=0:rtra=on:rawr=on_2798 on theBenchmark for (2798ds/6806Mi) % 216.48/31.34 % (3979676)Refutation not found, incomplete strategy % 216.48/31.34 % (3979676)------------------------------ % 216.48/31.34 % (3979676)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 216.48/31.34 % (3979676)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 216.48/31.34 % (3979676)CaDiCaL version: 2.1.3 % 216.48/31.34 % (3979676)Termination reason: Refutation not found, incomplete strategy % 216.48/31.34 % (3979676)Time elapsed: 0.041 s % 216.48/31.34 % (3979676)Peak memory usage: 116 MB % 216.48/31.34 % (3979676)Instructions burned: 6 (million) % 216.48/31.34 % (3979676)------------------------------ % 216.48/31.34 % (3979676)------------------------------ % 216.48/31.34 % (3979680)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=13311791:s2a=on:i=3553:nm=0:rtra=on_2791 on theBenchmark for (2791ds/3553Mi) % 216.48/31.34 % (3979656)Instruction limit reached! % 216.48/31.34 % (3979656)------------------------------ % 216.48/31.34 % (3979656)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 216.48/31.34 % (3979656)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 216.48/31.34 % (3979656)CaDiCaL version: 2.1.3 % 216.48/31.34 % (3979656)Termination reason: Instruction limit % 216.48/31.34 % (3979656)Termination phase: Saturation % 216.48/31.34 % (3979656)Time elapsed: 7.076 s % 216.48/31.34 % (3979656)Peak memory usage: 129 MB % 216.48/31.34 % (3979656)Instructions burned: 9201 (million) % 216.48/31.34 % (3979680)Instruction limit reached! % 216.48/31.34 % (3979680)------------------------------ % 216.48/31.34 % (3979680)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 216.48/31.34 % (3979680)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 216.48/31.34 % (3979680)CaDiCaL version: 2.1.3 % 216.48/31.34 % (3979680)Termination reason: Instruction limit % 216.48/31.34 % (3979680)Termination phase: Saturation % 216.48/31.34 % (3979680)Time elapsed: 3.201 s % 216.48/31.34 % (3979680)Peak memory usage: 100 MB % 216.48/31.34 % (3979680)Instructions burned: 3553 (million) % 216.48/31.34 % (3979684)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=565695620:thitd=on:cond=on:i=2064:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2758 on theBenchmark for (2758ds/2064Mi) % 216.48/31.34 % (3979685)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=931047133:cond=fast:i=20260:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2757 on theBenchmark for (2757ds/20260Mi) % 230.11/33.24 % (3979332)Instruction limit reached! % 230.11/33.24 % (3979332)------------------------------ % 230.11/33.24 % (3979332)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 230.11/33.24 % (3979332)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 230.11/33.24 % (3979332)CaDiCaL version: 2.1.3 % 230.11/33.24 % (3979332)Termination reason: Instruction limit % 230.11/33.24 % (3979332)Termination phase: Saturation % 230.11/33.24 % (3979332)Time elapsed: 13.829 s % 230.11/33.24 % (3979332)Peak memory usage: 132 MB % 230.11/33.24 % (3979332)Instructions burned: 20260 (million) % 230.11/33.24 % (3979688)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=3837658210:avsq=on:i=1244:avsqr=1,16:rtra=on:rawr=on_2736 on theBenchmark for (2736ds/1244Mi) % 230.11/33.24 % (3979688)Refutation not found, incomplete strategy % 230.11/33.24 % (3979688)------------------------------ % 230.11/33.24 % (3979688)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 230.11/33.24 % (3979688)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 230.11/33.24 % (3979688)CaDiCaL version: 2.1.3 % 230.11/33.24 % (3979688)Termination reason: Refutation not found, incomplete strategy % 230.11/33.24 % (3979688)Time elapsed: 0.041 s % 230.11/33.24 % (3979688)Peak memory usage: 116 MB % 230.11/33.24 % (3979688)Instructions burned: 6 (million) % 230.11/33.24 % (3979684)Instruction limit reached! % 230.11/33.24 % (3979684)------------------------------ % 230.11/33.24 % (3979684)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 230.11/33.24 % (3979684)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 230.11/33.24 % (3979684)CaDiCaL version: 2.1.3 % 230.11/33.24 % (3979684)Termination reason: Instruction limit % 230.11/33.24 % (3979684)Termination phase: Saturation % 230.11/33.24 % (3979684)Time elapsed: 2.264 s % 230.11/33.24 % (3979684)Peak memory usage: 154 MB % 230.11/33.24 % (3979684)Instructions burned: 2064 (million) % 230.11/33.24 % (3979690)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=2565962612:i=58261:doe=on:nm=0:rtra=on:gtg=exists_sym_2733 on theBenchmark for (2733ds/58261Mi) % 230.11/33.24 % (3979690)Refutation not found, incomplete strategy % 230.11/33.24 % (3979690)------------------------------ % 230.11/33.24 % (3979690)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 230.11/33.24 % (3979690)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 230.11/33.24 % (3979690)CaDiCaL version: 2.1.3 % 230.11/33.24 % (3979690)Termination reason: Refutation not found, incomplete strategy % 230.11/33.24 % (3979690)Time elapsed: 0.040 s % 230.11/33.24 % (3979690)Peak memory usage: 116 MB % 230.11/33.24 % (3979690)Instructions burned: 6 (million) % 230.11/33.24 % (3979688)------------------------------ % 230.11/33.24 % (3979688)------------------------------ % 230.11/33.24 % (3979692)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 % 230.11/33.24 % (3979692)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=318883926:i=6806:aac=none:nm=0:rtra=on:rawr=on_2730 on theBenchmark for (2730ds/6806Mi) % 230.11/33.24 % (3979692)Refutation not found, incomplete strategy % 230.11/33.24 % (3979692)------------------------------ % 230.11/33.24 % (3979692)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 230.11/33.24 % (3979692)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 230.11/33.24 % (3979692)CaDiCaL version: 2.1.3 % 230.11/33.24 % (3979692)Termination reason: Refutation not found, incomplete strategy % 230.11/33.24 % (3979692)Time elapsed: 0.042 s % 230.11/33.24 % (3979692)Peak memory usage: 116 MB % 230.11/33.24 % (3979692)Instructions burned: 6 (million) % 230.11/33.24 % (3979690)------------------------------ % 230.11/33.24 % (3979690)------------------------------ % 230.11/33.24 % (3979694)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=1042949621:thitd=on:cond=on:i=4081:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2726 on theBenchmark for (2726ds/4081Mi) % 230.11/33.24 % (3979692)------------------------------ % 238.22/34.44 % (3979692)------------------------------ % 238.22/34.44 % (3979696)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=1093837573:avsq=on:i=1701:avsqr=1,16:rtra=on:rawr=on_2723 on theBenchmark for (2723ds/1701Mi) % 238.22/34.44 % (3979696)Refutation not found, incomplete strategy % 238.22/34.44 % (3979696)------------------------------ % 238.22/34.44 % (3979696)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 238.22/34.44 % (3979696)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.22/34.44 % (3979696)CaDiCaL version: 2.1.3 % 238.22/34.44 % (3979696)Termination reason: Refutation not found, incomplete strategy % 238.22/34.44 % (3979696)Time elapsed: 0.041 s % 238.22/34.44 % (3979696)Peak memory usage: 116 MB % 238.22/34.44 % (3979696)Instructions burned: 6 (million) % 238.22/34.44 % (3979696)------------------------------ % 238.22/34.44 % (3979696)------------------------------ % 238.22/34.44 % (3979704)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=1526362808:i=57001:doe=on:nm=0:rtra=on:gtg=exists_sym_2717 on theBenchmark for (2717ds/57001Mi) % 238.22/34.44 % (3979704)Refutation not found, incomplete strategy % 238.22/34.44 % (3979704)------------------------------ % 238.22/34.44 % (3979704)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 238.22/34.44 % (3979704)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.22/34.44 % (3979704)CaDiCaL version: 2.1.3 % 238.22/34.44 % (3979704)Termination reason: Refutation not found, incomplete strategy % 238.22/34.44 % (3979704)Time elapsed: 0.041 s % 238.22/34.44 % (3979704)Peak memory usage: 116 MB % 238.22/34.44 % (3979704)Instructions burned: 6 (million) % 238.22/34.44 % (3979704)------------------------------ % 238.22/34.44 % (3979704)------------------------------ % 238.22/34.44 % (3979708)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 % 238.22/34.44 % (3979708)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=1558581965:i=8622:aac=none:nm=0:rtra=on:rawr=on_2710 on theBenchmark for (2710ds/8622Mi) % 238.22/34.44 % (3979708)Refutation not found, incomplete strategy % 238.22/34.44 % (3979708)------------------------------ % 238.22/34.44 % (3979708)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 238.22/34.44 % (3979708)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.22/34.44 % (3979708)CaDiCaL version: 2.1.3 % 238.22/34.44 % (3979708)Termination reason: Refutation not found, incomplete strategy % 238.22/34.44 % (3979708)Time elapsed: 0.041 s % 238.22/34.44 % (3979708)Peak memory usage: 116 MB % 238.22/34.44 % (3979708)Instructions burned: 6 (million) % 238.22/34.44 % (3979708)------------------------------ % 238.22/34.44 % (3979708)------------------------------ % 238.22/34.44 % (3979710)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=3521514641:i=24:doe=on:rtra=on:gtg=exists_top:ss=axioms_2704 on theBenchmark for (2704ds/24Mi) % 238.22/34.44 % (3979710)Refutation not found, incomplete strategy % 238.22/34.44 % (3979710)------------------------------ % 238.22/34.44 % (3979710)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 238.22/34.44 % (3979710)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.22/34.44 % (3979710)CaDiCaL version: 2.1.3 % 238.22/34.44 % (3979710)Termination reason: Refutation not found, incomplete strategy % 238.22/34.44 % (3979710)Time elapsed: 0.041 s % 238.22/34.44 % (3979710)Peak memory usage: 116 MB % 238.22/34.44 % (3979710)Instructions burned: 7 (million) % 238.22/34.44 % (3979710)------------------------------ % 238.22/34.44 % (3979710)------------------------------ % 238.22/34.44 % (3979712)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=334576767:i=614:kws=precedence:nm=0:rtra=on_2697 on theBenchmark for (2697ds/614Mi) % 238.22/34.44 % (3979712)Refutation not found, incomplete strategy % 238.22/34.44 % (3979712)------------------------------ % 238.22/34.44 % (3979712)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 238.22/34.44 % (3979712)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.22/34.44 % (3979712)CaDiCaL version: 2.1.3 % 238.22/34.44 % (3979712)Termination reason: Refutation not found, incomplete strategy % 238.22/34.44 % (3979712)Time elapsed: 0.041 s % 247.52/35.73 % (3979712)Peak memory usage: 116 MB % 247.52/35.73 % (3979712)Instructions burned: 6 (million) % 247.52/35.73 % (3979712)------------------------------ % 247.52/35.73 % (3979712)------------------------------ % 247.52/35.73 % (3979714)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=1486595020:i=402:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2691 on theBenchmark for (2691ds/402Mi) % 247.52/35.73 % (3979714)Instruction limit reached! % 247.52/35.73 % (3979714)------------------------------ % 247.52/35.73 % (3979714)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 247.52/35.73 % (3979714)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 247.52/35.73 % (3979714)CaDiCaL version: 2.1.3 % 247.52/35.73 % (3979714)Termination reason: Instruction limit % 247.52/35.73 % (3979714)Termination phase: Saturation % 247.52/35.73 % (3979714)Time elapsed: 0.402 s % 247.52/35.73 % (3979714)Peak memory usage: 114 MB % 247.52/35.73 % (3979714)Instructions burned: 403 (million) % 247.52/35.73 % (3979694)Instruction limit reached! % 247.52/35.73 % (3979694)------------------------------ % 247.52/35.73 % (3979694)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 247.52/35.73 % (3979694)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 247.52/35.73 % (3979694)CaDiCaL version: 2.1.3 % 247.52/35.73 % (3979694)Termination reason: Instruction limit % 247.52/35.73 % (3979694)Termination phase: Saturation % 247.52/35.73 % (3979694)Time elapsed: 4.158 s % 247.52/35.73 % (3979694)Peak memory usage: 160 MB % 247.52/35.73 % (3979694)Instructions burned: 4081 (million) % 247.52/35.73 % (3979716)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=268134896:s2a=on:i=14:rtra=on:inst=on_2684 on theBenchmark for (2684ds/14Mi) % 247.52/35.73 % (3979716)Instruction limit reached! % 247.52/35.73 % (3979716)------------------------------ % 247.52/35.73 % (3979716)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 247.52/35.73 % (3979716)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 247.52/35.73 % (3979716)CaDiCaL version: 2.1.3 % 247.52/35.73 % (3979716)Termination reason: Instruction limit % 247.52/35.73 % (3979716)Termination phase: Saturation % 247.52/35.73 % (3979716)Time elapsed: 0.016 s % 247.52/35.73 % (3979716)Peak memory usage: 88 MB % 247.52/35.74 % (3979716)Instructions burned: 14 (million) % 247.52/35.74 % (3979717)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=151989016:i=8:rtra=on_2682 on theBenchmark for (2682ds/8Mi) % 247.52/35.74 % (3979719)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=1345840721:i=92:rtra=on_2682 on theBenchmark for (2682ds/92Mi) % 247.52/35.74 % (3979717)Instruction limit reached! % 247.52/35.74 % (3979717)------------------------------ % 247.52/35.74 % (3979717)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 247.52/35.74 % (3979717)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 247.52/35.74 % (3979717)CaDiCaL version: 2.1.3 % 247.52/35.74 % (3979717)Termination reason: Instruction limit % 247.52/35.74 % (3979717)Termination phase: Saturation % 247.52/35.74 % (3979717)Time elapsed: 0.009 s % 247.52/35.74 % (3979717)Peak memory usage: 89 MB % 247.52/35.74 % (3979717)Instructions burned: 8 (million) % 247.52/35.74 % (3979719)Refutation not found, incomplete strategy % 247.52/35.74 % (3979719)------------------------------ % 247.52/35.74 % (3979719)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 247.52/35.74 % (3979719)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 247.52/35.74 % (3979719)CaDiCaL version: 2.1.3 % 247.52/35.74 % (3979719)Termination reason: Refutation not found, incomplete strategy % 247.52/35.74 % (3979719)Time elapsed: 0.040 s % 247.52/35.74 % (3979719)Peak memory usage: 116 MB % 247.52/35.74 % (3979719)Instructions burned: 6 (million) % 247.52/35.74 % (3979722)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=3885108488:i=66:rtra=on_2680 on theBenchmark for (2680ds/66Mi) % 247.52/35.74 % (3979722)Instruction limit reached! % 247.52/35.74 % (3979722)------------------------------ % 247.52/35.74 % (3979722)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 247.52/35.74 % (3979722)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 247.52/35.74 % (3979722)CaDiCaL version: 2.1.3 % 247.52/35.74 % (3979722)Termination reason: Instruction limit % 247.52/35.74 % (3979722)Termination phase: Saturation % 247.52/35.74 % (3979722)Time elapsed: 0.103 s % 247.52/35.74 % (3979722)Peak memory usage: 117 MB % 247.52/35.74 % (3979722)Instructions burned: 67 (million) % 247.52/35.74 % (3979719)------------------------------ % 247.52/35.74 % (3979719)------------------------------ % 255.79/36.93 % (3979724)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=844531982:st=5:i=28:sd=10:rtra=on:ss=axioms:rawr=on_2677 on theBenchmark for (2677ds/28Mi) % 255.79/36.93 % (3979724)Refutation not found, incomplete strategy % 255.79/36.93 % (3979724)------------------------------ % 255.79/36.93 % (3979724)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 255.79/36.93 % (3979724)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 255.79/36.93 % (3979724)CaDiCaL version: 2.1.3 % 255.79/36.93 % (3979724)Termination reason: Refutation not found, incomplete strategy % 255.79/36.93 % (3979724)Time elapsed: 0.002 s % 255.79/36.93 % (3979724)Peak memory usage: 88 MB % 255.79/36.93 % (3979725)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=2296121288:i=58:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2676 on theBenchmark for (2676ds/58Mi) % 255.79/36.93 % (3979725)Instruction limit reached! % 255.79/36.93 % (3979725)------------------------------ % 255.79/36.93 % (3979725)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 255.79/36.93 % (3979725)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 255.79/36.93 % (3979725)CaDiCaL version: 2.1.3 % 255.79/36.93 % (3979725)Termination reason: Instruction limit % 255.79/36.93 % (3979725)Termination phase: Saturation % 255.79/36.93 % (3979725)Time elapsed: 0.032 s % 255.79/36.93 % (3979725)Peak memory usage: 88 MB % 255.79/36.93 % (3979725)Instructions burned: 60 (million) % 255.79/36.93 % (3979724)------------------------------ % 255.79/36.93 % (3979724)------------------------------ % 255.79/36.93 % (3979728)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=2185990367:cond=on:i=32:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2673 on theBenchmark for (2673ds/32Mi) % 255.79/36.93 % (3979728)Instruction limit reached! % 255.79/36.93 % (3979728)------------------------------ % 255.79/36.93 % (3979728)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 255.79/36.93 % (3979728)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 255.79/36.93 % (3979728)CaDiCaL version: 2.1.3 % 255.79/36.93 % (3979728)Termination reason: Instruction limit % 255.79/36.93 % (3979728)Termination phase: Saturation % 255.79/36.93 % (3979728)Time elapsed: 0.030 s % 255.79/36.93 % (3979728)Peak memory usage: 90 MB % 255.79/36.93 % (3979728)Instructions burned: 32 (million) % 255.79/36.93 % (3979730)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=2454070078:i=48:canc=force:rtra=on_2670 on theBenchmark for (2670ds/48Mi) % 255.79/36.93 % (3979731)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=758402086:i=54:canc=cautious:fsr=off:rtra=on_2670 on theBenchmark for (2670ds/54Mi) % 255.79/36.93 % (3979731)Refutation not found, incomplete strategy % 255.79/36.93 % (3979731)------------------------------ % 255.79/36.93 % (3979731)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 255.79/36.93 % (3979731)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 255.79/36.93 % (3979731)CaDiCaL version: 2.1.3 % 255.79/36.93 % (3979731)Termination reason: Refutation not found, incomplete strategy % 255.79/36.93 % (3979731)Time elapsed: 0.002 s % 255.79/36.93 % (3979731)Peak memory usage: 89 MB % 255.79/36.93 % (3979730)Instruction limit reached! % 255.79/36.93 % (3979730)------------------------------ % 255.79/36.93 % (3979730)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 255.79/36.93 % (3979730)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 255.79/36.93 % (3979730)CaDiCaL version: 2.1.3 % 255.79/36.93 % (3979730)Termination reason: Instruction limit % 255.79/36.93 % (3979730)Termination phase: Saturation % 255.79/36.93 % (3979730)Time elapsed: 0.046 s % 255.79/36.93 % (3979730)Peak memory usage: 89 MB % 255.79/36.93 % (3979730)Instructions burned: 49 (million) % 255.79/36.93 % (3979734)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=2198179683:i=170:gtgl=4:rtra=on:gtg=exists_sym_2668 on theBenchmark for (2668ds/170Mi) % 255.79/36.93 % (3979731)------------------------------ % 255.79/36.93 % (3979731)------------------------------ % 255.79/36.93 % (3979734)Instruction limit reached! % 255.79/36.93 % (3979734)------------------------------ % 255.79/36.93 % (3979734)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 255.79/36.93 % (3979734)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 258.13/37.35 % (3979734)CaDiCaL version: 2.1.3 % 258.13/37.35 % (3979734)Termination reason: Instruction limit % 258.13/37.35 % (3979734)Termination phase: Saturation % 258.13/37.35 % (3979734)Time elapsed: 0.172 s % 258.13/37.35 % (3979734)Peak memory usage: 89 MB % 258.13/37.35 % (3979734)Instructions burned: 170 (million) % 258.13/37.35 % (3979736)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=143315048:i=4:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2664 on theBenchmark for (2664ds/4Mi) % 258.13/37.35 % (3979736)Instruction limit reached! % 258.13/37.35 % (3979736)------------------------------ % 258.13/37.35 % (3979736)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 258.13/37.35 % (3979736)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 258.13/37.35 % (3979736)CaDiCaL version: 2.1.3 % 258.13/37.35 % (3979736)Termination reason: Instruction limit % 258.13/37.35 % (3979736)Termination phase: Saturation % 258.13/37.35 % (3979736)Time elapsed: 0.006 s % 258.13/37.35 % (3979736)Peak memory usage: 89 MB % 258.13/37.35 % (3979736)Instructions burned: 4 (million) % 258.13/37.35 % (3979737)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=618185965:i=362:rtra=on:ss=axioms:ev=cautious_2664 on theBenchmark for (2664ds/362Mi) % 258.13/37.35 % (3979737)Refutation not found, incomplete strategy % 258.13/37.35 % (3979737)------------------------------ % 258.13/37.35 % (3979737)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 258.13/37.35 % (3979737)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 258.13/37.35 % (3979737)CaDiCaL version: 2.1.3 % 258.13/37.35 % (3979737)Termination reason: Refutation not found, incomplete strategy % 258.13/37.35 % (3979737)Time elapsed: 0.002 s % 258.13/37.35 % (3979737)Peak memory usage: 89 MB % 258.13/37.35 % (3979741)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=372734227:i=8:ep=RST:ins=2:rtra=on_2662 on theBenchmark for (2662ds/8Mi) % 258.13/37.35 % (3979741)Refutation not found, incomplete strategy % 258.13/37.35 % (3979741)------------------------------ % 258.13/37.35 % (3979741)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 258.13/37.35 % (3979741)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 258.13/37.35 % (3979741)CaDiCaL version: 2.1.3 % 258.13/37.35 % (3979741)Termination reason: Refutation not found, incomplete strategy % 258.13/37.35 % (3979741)Time elapsed: 0.002 s % 258.13/37.35 % (3979741)Peak memory usage: 89 MB % 258.13/37.35 % (3979741)Instructions burned: 1 (million) % 258.13/37.35 % (3979737)------------------------------ % 258.13/37.35 % (3979737)------------------------------ % 258.13/37.35 % (3979741)------------------------------ % 258.13/37.35 % (3979741)------------------------------ % 258.13/37.35 % (3979744)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=1655692778:i=132:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2658 on theBenchmark for (2658ds/132Mi) % 258.13/37.35 % (3979744)Instruction limit reached! % 258.13/37.35 % (3979744)------------------------------ % 258.13/37.35 % (3979744)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 258.13/37.35 % (3979744)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 258.13/37.35 % (3979744)CaDiCaL version: 2.1.3 % 258.13/37.35 % (3979744)Termination reason: Instruction limit % 258.13/37.35 % (3979744)Termination phase: Saturation % 258.13/37.35 % (3979744)Time elapsed: 0.201 s % 258.13/37.35 % (3979744)Peak memory usage: 136 MB % 258.13/37.35 % (3979744)Instructions burned: 133 (million) % 258.13/37.35 % (3979745)lrs+10_1_thi=all:si=on:fd=off:random_seed=2079502997:i=106:rtra=on:gtg=all_2656 on theBenchmark for (2656ds/106Mi) % 258.13/37.35 % (3979745)Instruction limit reached! % 258.13/37.35 % (3979745)------------------------------ % 258.13/37.35 % (3979745)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 258.13/37.35 % (3979745)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 258.13/37.35 % (3979745)CaDiCaL version: 2.1.3 % 258.13/37.35 % (3979745)Termination reason: Instruction limit % 258.13/37.35 % (3979745)Termination phase: Saturation % 258.13/37.35 % (3979745)Time elapsed: 0.144 s % 258.13/37.35 % (3979745)Peak memory usage: 113 MB % 258.13/37.35 % (3979745)Instructions burned: 106 (million) % 258.13/37.35 % (3979747)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=356457531:i=16:ep=RST:nm=16:rtra=on:gtg=exists_top_2653 on theBenchmark for (2653ds/16Mi) % 258.13/37.35 % (3979747)Instruction limit reached! % 258.13/37.35 % (3979747)------------------------------ % 265.18/38.28 % (3979747)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 265.18/38.28 % (3979747)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 265.18/38.28 % (3979747)CaDiCaL version: 2.1.3 % 265.18/38.28 % (3979747)Termination reason: Instruction limit % 265.18/38.28 % (3979747)Termination phase: Saturation % 265.18/38.28 % (3979747)Time elapsed: 0.018 s % 265.18/38.28 % (3979747)Peak memory usage: 88 MB % 265.18/38.28 % (3979747)Instructions burned: 16 (million) % 265.18/38.28 % (3979749)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=2381826184:st=3:i=4:rtra=on:ss=axioms_2652 on theBenchmark for (2652ds/4Mi) % 265.18/38.28 % (3979749)Instruction limit reached! % 265.18/38.28 % (3979749)------------------------------ % 265.18/38.28 % (3979749)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 265.18/38.28 % (3979749)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 265.18/38.28 % (3979749)CaDiCaL version: 2.1.3 % 265.18/38.28 % (3979749)Termination reason: Instruction limit % 265.18/38.28 % (3979749)Termination phase: Saturation % 265.18/38.28 % (3979749)Time elapsed: 0.006 s % 265.18/38.28 % (3979749)Peak memory usage: 90 MB % 265.18/38.28 % (3979749)Instructions burned: 4 (million) % 265.18/38.28 % (3979751)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=3687972646:i=4:doe=on:canc=force:asg=cautious:rtra=on_2651 on theBenchmark for (2651ds/4Mi) % 265.18/38.28 % (3979751)Instruction limit reached! % 265.18/38.28 % (3979751)------------------------------ % 265.18/38.28 % (3979751)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 265.18/38.28 % (3979751)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 265.18/38.28 % (3979751)CaDiCaL version: 2.1.3 % 265.18/38.28 % (3979751)Termination reason: Instruction limit % 265.18/38.28 % (3979751)Termination phase: Saturation % 265.18/38.28 % (3979751)Time elapsed: 0.006 s % 265.18/38.28 % (3979751)Peak memory usage: 89 MB % 265.18/38.28 % (3979751)Instructions burned: 4 (million) % 265.18/38.28 % (3979753)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=3411942113:i=254:doe=on:rtra=on_2649 on theBenchmark for (2649ds/254Mi) % 265.18/38.28 % (3979755)dis+10_1_si=on:random_seed=2065675195:i=20:ep=R:rtra=on_2648 on theBenchmark for (2648ds/20Mi) % 265.18/38.28 % (3979753)Refutation not found, incomplete strategy % 265.18/38.28 % (3979753)------------------------------ % 265.18/38.28 % (3979753)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 265.18/38.28 % (3979753)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 265.18/38.28 % (3979753)CaDiCaL version: 2.1.3 % 265.18/38.28 % (3979753)Termination reason: Refutation not found, incomplete strategy % 265.18/38.28 % (3979753)Time elapsed: 0.043 s % 265.18/38.28 % (3979753)Peak memory usage: 116 MB % 265.18/38.28 % (3979755)Instruction limit reached! % 265.18/38.28 % (3979755)------------------------------ % 265.18/38.28 % (3979755)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 265.18/38.28 % (3979753)Instructions burned: 8 (million) % 265.18/38.28 % (3979755)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 265.18/38.28 % (3979755)CaDiCaL version: 2.1.3 % 265.18/38.28 % (3979755)Termination reason: Instruction limit % 265.18/38.28 % (3979755)Termination phase: Saturation % 265.18/38.28 % (3979755)Time elapsed: 0.020 s % 265.18/38.28 % (3979755)Peak memory usage: 88 MB % 265.18/38.29 % (3979755)Instructions burned: 20 (million) % 265.18/38.29 % (3979758)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=1198148928:i=52:canc=cautious:av=off:rtra=on_2645 on theBenchmark for (2645ds/52Mi) % 265.18/38.29 % (3979758)Refutation not found, incomplete strategy % 265.18/38.29 % (3979758)------------------------------ % 265.18/38.29 % (3979758)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 265.18/38.29 % (3979758)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 265.18/38.29 % (3979758)CaDiCaL version: 2.1.3 % 265.18/38.29 % (3979758)Termination reason: Refutation not found, incomplete strategy % 265.18/38.29 % (3979758)Time elapsed: 0.002 s % 265.18/38.29 % (3979758)Peak memory usage: 89 MB % 265.18/38.29 % (3979758)Instructions burned: 1 (million) % 265.18/38.29 % (3979753)------------------------------ % 265.18/38.29 % (3979753)------------------------------ % 265.18/38.29 % (3979758)------------------------------ % 265.18/38.29 % (3979758)------------------------------ % 265.18/38.29 % (3979760)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=1431533942:avsq=on:i=70:doe=on:thsqd=64:nm=64:fsr=off:thsqc=32:rtra=on:tac=light:ss=included:thsq=on:ev=off:sgt=32_2641 on theBenchmark for (2641ds/70Mi) % 271.86/39.19 % (3979472)Instruction limit reached! % 271.86/39.19 % (3979472)------------------------------ % 271.86/39.19 % (3979472)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 271.86/39.19 % (3979472)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 271.86/39.19 % (3979472)CaDiCaL version: 2.1.3 % 271.86/39.19 % (3979472)Termination reason: Instruction limit % 271.86/39.19 % (3979472)Termination phase: Saturation % 271.86/39.19 % (3979472)Time elapsed: 22.754 s % 271.86/39.19 % (3979472)Peak memory usage: 95 MB % 271.86/39.19 % (3979472)Instructions burned: 71623 (million) % 271.86/39.19 % (3979760)Instruction limit reached! % 271.86/39.19 % (3979760)------------------------------ % 271.86/39.19 % (3979760)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 271.86/39.19 % (3979760)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 271.86/39.19 % (3979760)CaDiCaL version: 2.1.3 % 271.86/39.19 % (3979760)Termination reason: Instruction limit % 271.86/39.19 % (3979760)Termination phase: Saturation % 271.86/39.19 % (3979760)Time elapsed: 0.083 s % 271.86/39.19 % (3979760)Peak memory usage: 90 MB % 271.86/39.19 % (3979760)Instructions burned: 70 (million) % 271.86/39.19 % (3979761)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=184796462:i=4:fsr=off:rtra=on:inst=on_2639 on theBenchmark for (2639ds/4Mi) % 271.86/39.19 % (3979761)Instruction limit reached! % 271.86/39.19 % (3979761)------------------------------ % 271.86/39.19 % (3979761)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 271.86/39.19 % (3979761)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 271.86/39.19 % (3979761)CaDiCaL version: 2.1.3 % 271.86/39.19 % (3979761)Termination reason: Instruction limit % 271.86/39.19 % (3979761)Termination phase: Saturation % 271.86/39.19 % (3979761)Time elapsed: 0.006 s % 271.86/39.19 % (3979761)Peak memory usage: 89 MB % 271.86/39.19 % (3979761)Instructions burned: 5 (million) % 271.86/39.19 % (3979763)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=1233106938:s2a=on:i=16:kws=inv_precedence:doe=on:rtra=on_2639 on theBenchmark for (2639ds/16Mi) % 271.86/39.19 % (3979763)Instruction limit reached! % 271.86/39.19 % (3979763)------------------------------ % 271.86/39.19 % (3979763)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 271.86/39.19 % (3979763)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 271.86/39.19 % (3979763)CaDiCaL version: 2.1.3 % 271.86/39.19 % (3979763)Termination reason: Instruction limit % 271.86/39.19 % (3979763)Termination phase: Saturation % 271.86/39.19 % (3979763)Time elapsed: 0.010 s % 271.86/39.19 % (3979763)Peak memory usage: 88 MB % 271.86/39.19 % (3979763)Instructions burned: 16 (million) % 271.86/39.19 % (3979764)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=2150545443:i=740:ep=RS:fsr=off:rtra=on_2638 on theBenchmark for (2638ds/740Mi) % 271.86/39.19 % (3979768)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=3976668096:i=452:rtra=on:gtg=position:ss=axioms_2637 on theBenchmark for (2637ds/452Mi) % 271.86/39.19 % (3979768)Refutation not found, incomplete strategy % 271.86/39.19 % (3979768)------------------------------ % 271.86/39.19 % (3979768)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 271.86/39.19 % (3979768)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 271.86/39.19 % (3979768)CaDiCaL version: 2.1.3 % 271.86/39.19 % (3979768)Termination reason: Refutation not found, incomplete strategy % 271.86/39.19 % (3979768)Time elapsed: 0.023 s % 271.86/39.19 % (3979768)Peak memory usage: 116 MB % 271.86/39.19 % (3979768)Instructions burned: 6 (million) % 271.86/39.19 % (3979767)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=3837984797:i=26:av=off:rtra=on:gtg=exists_sym:ev=force_2637 on theBenchmark for (2637ds/26Mi) % 271.86/39.19 % (3979767)Instruction limit reached! % 271.86/39.19 % (3979767)------------------------------ % 271.86/39.19 % (3979767)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 271.86/39.19 % (3979767)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 271.86/39.19 % (3979767)CaDiCaL version: 2.1.3 % 271.86/39.19 % (3979767)Termination reason: Instruction limit % 271.86/39.19 % (3979767)Termination phase: Saturation % 271.86/39.19 % (3979767)Time elapsed: 0.049 s % 271.86/39.19 % (3979767)Peak memory usage: 112 MB % 271.86/39.19 % (3979767)Instructions burned: 27 (million) % 280.95/40.51 % (3979768)------------------------------ % 280.95/40.51 % (3979768)------------------------------ % 280.95/40.51 % (3979772)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=2030279267:i=20:rtra=on_2635 on theBenchmark for (2635ds/20Mi) % 280.95/40.51 % (3979772)Refutation not found, incomplete strategy % 280.95/40.51 % (3979772)------------------------------ % 280.95/40.51 % (3979772)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 280.95/40.51 % (3979772)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 280.95/40.51 % (3979772)CaDiCaL version: 2.1.3 % 280.95/40.51 % (3979772)Termination reason: Refutation not found, incomplete strategy % 280.95/40.51 % (3979772)Time elapsed: 0.001 s % 280.95/40.51 % (3979772)Peak memory usage: 88 MB % 280.95/40.51 % (3979773)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=3084290562:i=142:rtra=on:gtg=exists_top_2633 on theBenchmark for (2633ds/142Mi) % 280.95/40.51 % (3979773)Refutation not found, incomplete strategy % 280.95/40.51 % (3979773)------------------------------ % 280.95/40.51 % (3979773)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 280.95/40.51 % (3979773)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 280.95/40.51 % (3979773)CaDiCaL version: 2.1.3 % 280.95/40.51 % (3979773)Termination reason: Refutation not found, incomplete strategy % 280.95/40.51 % (3979773)Time elapsed: 0.043 s % 280.95/40.51 % (3979773)Peak memory usage: 133 MB % 280.95/40.51 % (3979773)Instructions burned: 11 (million) % 280.95/40.51 % (3979764)Instruction limit reached! % 280.95/40.51 % (3979764)------------------------------ % 280.95/40.51 % (3979764)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 280.95/40.51 % (3979764)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 280.95/40.51 % (3979764)CaDiCaL version: 2.1.3 % 280.95/40.51 % (3979764)Termination reason: Instruction limit % 280.95/40.51 % (3979764)Termination phase: Saturation % 280.95/40.51 % (3979764)Time elapsed: 0.658 s % 280.95/40.51 % (3979764)Peak memory usage: 95 MB % 280.95/40.51 % (3979764)Instructions burned: 741 (million) % 280.95/40.51 % (3979773)------------------------------ % 280.95/40.51 % (3979773)------------------------------ % 280.95/40.51 % (3979772)------------------------------ % 280.95/40.51 % (3979772)------------------------------ % 280.95/40.51 % (3979777)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=326748774:i=588:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2629 on theBenchmark for (2629ds/588Mi) % 280.95/40.51 % (3979776)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=3808027208:i=150:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2629 on theBenchmark for (2629ds/150Mi) % 280.95/40.51 % (3979778)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=72253374:i=260:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2628 on theBenchmark for (2628ds/260Mi) % 280.95/40.51 % (3979776)Instruction limit reached! % 280.95/40.51 % (3979776)------------------------------ % 280.95/40.51 % (3979776)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 280.95/40.51 % (3979776)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 280.95/40.51 % (3979776)CaDiCaL version: 2.1.3 % 280.95/40.51 % (3979776)Termination reason: Instruction limit % 280.95/40.51 % (3979776)Termination phase: Saturation % 280.95/40.51 % (3979776)Time elapsed: 0.101 s % 280.95/40.51 % (3979776)Peak memory usage: 89 MB % 280.95/40.51 % (3979776)Instructions burned: 151 (million) % 280.95/40.51 % (3979778)Refutation not found, incomplete strategy % 280.95/40.51 % (3979778)------------------------------ % 280.95/40.51 % (3979778)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 280.95/40.51 % (3979778)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 280.95/40.51 % (3979778)CaDiCaL version: 2.1.3 % 280.95/40.51 % (3979778)Termination reason: Refutation not found, incomplete strategy % 280.95/40.51 % (3979778)Time elapsed: 0.039 s % 280.95/40.51 % (3979778)Peak memory usage: 116 MB % 280.95/40.51 % (3979778)Instructions burned: 6 (million) % 280.95/40.51 % (3979777)Instruction limit reached! % 280.95/40.51 % (3979777)------------------------------ % 280.95/40.51 % (3979777)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 280.95/40.51 % (3979777)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 280.95/40.51 % (3979777)CaDiCaL version: 2.1.3 % 285.37/41.08 % (3979777)Termination reason: Instruction limit % 285.37/41.08 % (3979777)Termination phase: Saturation % 285.37/41.08 % (3979777)Time elapsed: 0.196 s % 285.37/41.08 % (3979777)Peak memory usage: 88 MB % 285.37/41.08 % (3979777)Instructions burned: 588 (million) % 285.37/41.08 % (3979782)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=3230419058:i=262:rtra=on_2626 on theBenchmark for (2626ds/262Mi) % 285.37/41.08 % (3979783)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=1050636339:i=80:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2625 on theBenchmark for (2625ds/80Mi) % 285.37/41.08 % (3979782)Refutation not found, incomplete strategy % 285.37/41.08 % (3979782)------------------------------ % 285.37/41.08 % (3979782)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 285.37/41.08 % (3979782)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 285.37/41.08 % (3979782)CaDiCaL version: 2.1.3 % 285.37/41.08 % (3979782)Termination reason: Refutation not found, incomplete strategy % 285.37/41.08 % (3979782)Time elapsed: 0.076 s % 285.37/41.08 % (3979782)Peak memory usage: 133 MB % 285.37/41.09 % (3979782)Instructions burned: 11 (million) % 285.37/41.09 % (3979783)Instruction limit reached! % 285.37/41.09 % (3979783)------------------------------ % 285.37/41.09 % (3979783)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 285.37/41.09 % (3979783)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 285.37/41.09 % (3979783)CaDiCaL version: 2.1.3 % 285.37/41.09 % (3979783)Termination reason: Instruction limit % 285.37/41.09 % (3979783)Termination phase: Saturation % 285.37/41.09 % (3979783)Time elapsed: 0.079 s % 285.37/41.09 % (3979783)Peak memory usage: 134 MB % 285.37/41.09 % (3979783)Instructions burned: 82 (million) % 285.37/41.09 % (3979778)------------------------------ % 285.37/41.09 % (3979778)------------------------------ % 285.37/41.09 % (3979786)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=3223550198:i=614:rtra=on:gtg=exists_top_2623 on theBenchmark for (2623ds/614Mi) % 285.37/41.09 % (3979786)Refutation not found, incomplete strategy % 285.37/41.09 % (3979786)------------------------------ % 285.37/41.09 % (3979786)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 285.37/41.09 % (3979786)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 285.37/41.09 % (3979786)CaDiCaL version: 2.1.3 % 285.37/41.09 % (3979786)Termination reason: Refutation not found, incomplete strategy % 285.37/41.09 % (3979786)Time elapsed: 0.001 s % 285.37/41.09 % (3979786)Peak memory usage: 89 MB % 285.37/41.09 % (3979786)Instructions burned: 1 (million) % 285.37/41.09 % (3979787)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=1867595840:s2a=on:i=1196:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2622 on theBenchmark for (2622ds/1196Mi) % 285.37/41.09 % (3979787)Refutation not found, incomplete strategy % 285.37/41.09 % (3979787)------------------------------ % 285.37/41.09 % (3979787)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 285.37/41.09 % (3979787)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 285.37/41.09 % (3979787)CaDiCaL version: 2.1.3 % 285.37/41.09 % (3979787)Termination reason: Refutation not found, incomplete strategy % 285.37/41.09 % (3979787)Time elapsed: 0.073 s % 285.37/41.09 % (3979787)Peak memory usage: 133 MB % 285.37/41.09 % (3979787)Instructions burned: 11 (million) % 285.37/41.09 % (3979782)------------------------------ % 285.37/41.09 % (3979782)------------------------------ % 285.37/41.09 % (3979786)------------------------------ % 285.37/41.09 % (3979786)------------------------------ % 285.37/41.09 % (3979790)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=2306221378:i=262:canc=cautious:fsr=off:rtra=on_2619 on theBenchmark for (2619ds/262Mi) % 285.37/41.09 % (3979791)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=1904968450:s2pl=no:i=518:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2619 on theBenchmark for (2619ds/518Mi) % 285.37/41.09 % (3979791)Refutation not found, incomplete strategy % 285.37/41.09 % (3979791)------------------------------ % 285.37/41.09 % (3979791)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 285.37/41.09 % (3979791)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 285.37/41.09 % (3979791)CaDiCaL version: 2.1.3 % 285.37/41.09 % (3979791)Termination reason: Refutation not found, incomplete strategy % 285.37/41.09 % (3979791)Time elapsed: 0.041 s % 285.37/41.09 % (3979791)Peak memory usage: 116 MB % 293.05/42.16 % (3979791)Instructions burned: 6 (million) % 293.05/42.16 % (3979790)Instruction limit reached! % 293.05/42.16 % (3979790)------------------------------ % 293.05/42.16 % (3979790)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 293.05/42.16 % (3979790)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 293.05/42.16 % (3979790)CaDiCaL version: 2.1.3 % 293.05/42.16 % (3979790)Termination reason: Instruction limit % 293.05/42.16 % (3979790)Termination phase: Saturation % 293.05/42.16 % (3979790)Time elapsed: 0.144 s % 293.05/42.16 % (3979790)Peak memory usage: 118 MB % 293.05/42.16 % (3979790)Instructions burned: 263 (million) % 293.05/42.16 % (3979787)------------------------------ % 293.05/42.16 % (3979787)------------------------------ % 293.05/42.16 % (3979794)dis+10_1_si=on:random_seed=2902502156:s2a=on:i=2000:rtra=on:gtg=exists_all_2616 on theBenchmark for (2616ds/2000Mi) % 293.05/42.16 % (3979795)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=2581071888:i=766:fsr=off:rtra=on:ev=force_2615 on theBenchmark for (2615ds/766Mi) % 293.05/42.16 % (3979795)Refutation not found, incomplete strategy % 293.05/42.16 % (3979795)------------------------------ % 293.05/42.16 % (3979795)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 293.05/42.16 % (3979795)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 293.05/42.16 % (3979795)CaDiCaL version: 2.1.3 % 293.05/42.16 % (3979795)Termination reason: Refutation not found, incomplete strategy % 293.05/42.16 % (3979795)Time elapsed: 0.002 s % 293.05/42.16 % (3979795)Peak memory usage: 89 MB % 293.05/42.16 % (3979791)------------------------------ % 293.05/42.16 % (3979791)------------------------------ % 293.05/42.16 % (3979798)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=2211034479:i=282:doe=on:rtra=on_2612 on theBenchmark for (2612ds/282Mi) % 293.05/42.16 % (3979795)------------------------------ % 293.05/42.16 % (3979795)------------------------------ % 293.05/42.16 % (3979798)Instruction limit reached! % 293.05/42.16 % (3979798)------------------------------ % 293.05/42.16 % (3979798)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 293.05/42.16 % (3979798)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 293.05/42.16 % (3979798)CaDiCaL version: 2.1.3 % 293.05/42.16 % (3979798)Termination reason: Instruction limit % 293.05/42.16 % (3979798)Termination phase: Saturation % 293.05/42.16 % (3979798)Time elapsed: 0.290 s % 293.05/42.16 % (3979798)Peak memory usage: 91 MB % 293.05/42.16 % (3979798)Instructions burned: 282 (million) % 293.05/42.16 % (3979800)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=1488474218:i=130:nm=16:rtra=on_2609 on theBenchmark for (2609ds/130Mi) % 293.05/42.16 % (3979800)Refutation not found, incomplete strategy % 293.05/42.16 % (3979800)------------------------------ % 293.05/42.16 % (3979800)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 293.05/42.16 % (3979800)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 293.05/42.16 % (3979800)CaDiCaL version: 2.1.3 % 293.05/42.16 % (3979800)Termination reason: Refutation not found, incomplete strategy % 293.05/42.16 % (3979800)Time elapsed: 0.039 s % 293.05/42.16 % (3979800)Peak memory usage: 116 MB % 293.05/42.16 % (3979800)Instructions burned: 6 (million) % 293.05/42.16 % (3979794)Instruction limit reached! % 293.05/42.16 % (3979794)------------------------------ % 293.05/42.16 % (3979794)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 293.05/42.16 % (3979794)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 293.05/42.16 % (3979794)CaDiCaL version: 2.1.3 % 293.05/42.16 % (3979794)Termination reason: Instruction limit % 293.05/42.16 % (3979794)Termination phase: Saturation % 293.05/42.16 % (3979794)Time elapsed: 0.890 s % 293.05/42.16 % (3979794)Peak memory usage: 98 MB % 293.05/42.16 % (3979794)Instructions burned: 2000 (million) % 293.05/42.16 % (3979801)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=4244671120:i=242:nm=16:rtra=on_2607 on theBenchmark for (2607ds/242Mi) % 293.05/42.16 % (3979803)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=770651625:s2a=on:i=256:s2at=5:ins=3:rtra=on_2605 on theBenchmark for (2605ds/256Mi) % 293.05/42.16 % (3979801)Instruction limit reached! % 293.05/42.16 % (3979801)------------------------------ % 293.05/42.16 % (3979801)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 293.05/42.16 % (3979801)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 297.27/42.94 % (3979801)CaDiCaL version: 2.1.3 % 297.27/42.94 % (3979801)Termination reason: Instruction limit % 297.27/42.94 % (3979801)Termination phase: Saturation % 297.27/42.94 % (3979801)Time elapsed: 0.165 s % 297.27/42.94 % (3979801)Peak memory usage: 88 MB % 297.27/42.94 % (3979801)Instructions burned: 243 (million) % 297.27/42.94 % (3979800)------------------------------ % 297.27/42.94 % (3979800)------------------------------ % 297.27/42.94 % (3979803)Instruction limit reached! % 297.27/42.94 % (3979803)------------------------------ % 297.27/42.94 % (3979803)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 297.27/42.94 % (3979803)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 297.27/42.94 % (3979803)CaDiCaL version: 2.1.3 % 297.27/42.94 % (3979803)Termination reason: Instruction limit % 297.27/42.94 % (3979803)Termination phase: Saturation % 297.27/42.94 % (3979803)Time elapsed: 0.145 s % 297.27/42.94 % (3979803)Peak memory usage: 120 MB % 297.27/42.94 % (3979803)Instructions burned: 256 (million) % 297.27/42.94 % (3979808)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=1860419525:i=658:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2602 on theBenchmark for (2602ds/658Mi) % 297.27/42.94 % (3979806)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=4282239580:i=78:ins=3:rtra=on_2603 on theBenchmark for (2603ds/78Mi) % 297.27/42.94 % (3979807)dis+1010_1_to=kbo:si=on:random_seed=1048461532:i=350:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2603 on theBenchmark for (2603ds/350Mi) % 297.27/42.94 % (3979806)Refutation not found, incomplete strategy % 297.27/42.94 % (3979806)------------------------------ % 297.27/42.94 % (3979806)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 297.27/42.94 % (3979806)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 297.27/42.94 % (3979806)CaDiCaL version: 2.1.3 % 297.27/42.94 % (3979806)Termination reason: Refutation not found, incomplete strategy % 297.27/42.94 % (3979806)Time elapsed: 0.040 s % 297.27/42.94 % (3979806)Peak memory usage: 115 MB % 297.27/42.94 % (3979806)Instructions burned: 6 (million) % 297.27/42.94 % (3979685)Instruction limit reached! % 297.27/42.94 % (3979685)------------------------------ % 297.27/42.94 % (3979685)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 297.27/42.94 % (3979685)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 297.27/42.94 % (3979685)CaDiCaL version: 2.1.3 % 297.27/42.94 % (3979685)Termination reason: Instruction limit % 297.27/42.94 % (3979685)Termination phase: Saturation % 297.27/42.94 % (3979685)Time elapsed: 15.457 s % 297.27/42.94 % (3979685)Peak memory usage: 131 MB % 297.27/42.94 % (3979685)Instructions burned: 20261 (million) % 297.27/42.94 % (3979812)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=2290843903:s2a=on:i=966:doe=on:nm=32:rtra=on_2600 on theBenchmark for (2600ds/966Mi) % 297.27/42.94 % (3979808)Instruction limit reached! % 297.27/42.94 % (3979808)------------------------------ % 297.27/42.94 % (3979808)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 297.27/42.94 % (3979808)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 297.27/42.94 % (3979808)CaDiCaL version: 2.1.3 % 297.27/42.94 % (3979808)Termination reason: Instruction limit % 297.27/42.94 % (3979808)Termination phase: Saturation % 297.27/42.94 % (3979808)Time elapsed: 0.314 s % 297.27/42.94 % (3979808)Peak memory usage: 114 MB % 297.27/42.94 % (3979808)Instructions burned: 660 (million) % 297.27/42.94 % (3979807)Instruction limit reached! % 297.27/42.94 % (3979807)------------------------------ % 297.27/42.94 % (3979807)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 297.27/42.94 % (3979807)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 297.27/42.94 % (3979807)CaDiCaL version: 2.1.3 % 297.27/42.94 % (3979807)Termination reason: Instruction limit % 297.27/42.94 % (3979807)Termination phase: Saturation % 297.27/42.94 % (3979807)Time elapsed: 0.309 s % 297.27/42.94 % (3979807)Peak memory usage: 91 MB % 297.27/42.94 % (3979807)Instructions burned: 351 (million) % 297.27/42.94 % (3979812)Refutation not found, incomplete strategy % 297.27/42.94 % (3979812)------------------------------ % 297.27/42.94 % (3979812)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 297.27/42.94 % (3979812)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 297.27/42.94 % (3979812)CaDiCaL version: 2.1.3 % 297.27/42.94 % (3979812)Termination reason: Refutation not found, incomplete Terminated %------------------------------------------------------------------------------