%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWW835_1 : TPTP v9.3.1. Released v7.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % Computer : n017.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:37:55 PM UTC 2026 % Result : Timeout 300.02s 42.84s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : SWW835_1 : TPTP v9.3.1. Released v7.0.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.08/0.19 % Computer : n017.cluster.edu % 0.08/0.19 % Model : x86_64 x86_64 % 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.19 % Memory : 8046.5625MB % 0.08/0.19 % OS : Linux 6.8.0-71-generic % 0.08/0.19 % CPULimit : 300 % 0.08/0.19 % WCLimit : 300 % 0.08/0.20 % DateTime : Mon Sep 28 14:26:36 UTC 2026 % 0.08/0.20 % CPUTime : % 0.08/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.08/0.23 Running first-order theorem proving % 0.08/0.23 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 4.18/1.36 % (3600154)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule. % 4.18/1.36 % (3600244)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=1926653243:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi) % 4.18/1.36 % (3600244)Refutation not found, incomplete strategy % 4.18/1.36 % (3600244)------------------------------ % 4.18/1.36 % (3600244)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.18/1.36 % (3600244)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.18/1.36 % (3600244)CaDiCaL version: 2.1.3 % 4.18/1.36 % (3600244)Termination reason: Refutation not found, incomplete strategy % 4.18/1.36 % (3600244)Time elapsed: 0.018 s % 4.18/1.36 % (3600244)Peak memory usage: 111 MB % 4.18/1.36 % (3600244)Instructions burned: 7 (million) % 4.18/1.36 % (3600250)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=324646884:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi) % 4.18/1.36 % (3600247)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=3208289611:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi) % 4.18/1.36 % (3600246)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=2320927457:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi) % 4.18/1.36 % (3600249)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=1023237176:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi) % 4.18/1.36 % (3600245)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=3169641190:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi) % 4.18/1.36 % (3600248)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=2209797007:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi) % 4.18/1.36 % (3600248)Instruction limit reached! % 4.18/1.36 % (3600248)------------------------------ % 4.18/1.36 % (3600248)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.18/1.36 % (3600248)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.18/1.36 % (3600248)CaDiCaL version: 2.1.3 % 4.18/1.36 % (3600248)Termination reason: Instruction limit % 4.18/1.36 % (3600248)Termination phase: Saturation % 4.18/1.36 % (3600248)Time elapsed: 0.003 s % 4.18/1.36 % (3600248)Peak memory usage: 88 MB % 4.18/1.36 % (3600248)Instructions burned: 4 (million) % 4.18/1.36 % (3600247)Instruction limit reached! % 4.18/1.36 % (3600247)------------------------------ % 4.18/1.36 % (3600247)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.18/1.36 % (3600247)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.18/1.36 % (3600247)CaDiCaL version: 2.1.3 % 4.18/1.36 % (3600247)Termination reason: Instruction limit % 4.18/1.36 % (3600247)Termination phase: Saturation % 4.18/1.36 % (3600247)Time elapsed: 0.005 s % 4.18/1.36 % (3600247)Peak memory usage: 88 MB % 4.18/1.36 % (3600247)Instructions burned: 8 (million) % 4.18/1.36 % (3600250)Instruction limit reached! % 4.18/1.36 % (3600250)------------------------------ % 4.18/1.36 % (3600250)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.18/1.36 % (3600250)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.18/1.36 % (3600250)CaDiCaL version: 2.1.3 % 4.18/1.36 % (3600250)Termination reason: Instruction limit % 4.18/1.36 % (3600250)Termination phase: Saturation % 4.18/1.36 % (3600250)Time elapsed: 0.047 s % 4.18/1.36 % (3600250)Peak memory usage: 116 MB % 4.18/1.36 % (3600250)Instructions burned: 33 (million) % 4.18/1.36 % (3600249)Instruction limit reached! % 4.18/1.36 % (3600249)------------------------------ % 4.18/1.36 % (3600249)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.18/1.36 % (3600249)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.18/1.36 % (3600249)CaDiCaL version: 2.1.3 % 4.18/1.36 % (3600249)Termination reason: Instruction limit % 4.18/1.36 % (3600249)Termination phase: Saturation % 4.18/1.36 % (3600249)Time elapsed: 0.057 s % 4.18/1.36 % (3600249)Peak memory usage: 117 MB % 4.18/1.36 % (3600249)Instructions burned: 49 (million) % 4.18/1.36 % (3600244)------------------------------ % 4.18/1.36 % (3600244)------------------------------ % 4.18/1.36 % (3600258)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=745644416:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2998 on theBenchmark for (2998ds/14Mi) % 4.18/1.36 % (3600259)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=3841569590:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2998 on theBenchmark for (2998ds/29Mi) % 4.56/1.50 % (3600258)Refutation not found, incomplete strategy % 4.56/1.50 % (3600258)------------------------------ % 4.56/1.50 % (3600258)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.56/1.50 % (3600258)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.56/1.50 % (3600258)CaDiCaL version: 2.1.3 % 4.56/1.50 % (3600258)Termination reason: Refutation not found, incomplete strategy % 4.56/1.50 % (3600258)Time elapsed: 0.001 s % 4.56/1.50 % (3600258)Peak memory usage: 88 MB % 4.56/1.50 % (3600258)Instructions burned: 1 (million) % 4.56/1.50 % (3600246)Instruction limit reached! % 4.56/1.50 % (3600246)------------------------------ % 4.56/1.50 % (3600246)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.56/1.50 % (3600246)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.56/1.50 % (3600246)CaDiCaL version: 2.1.3 % 4.56/1.50 % (3600246)Termination reason: Instruction limit % 4.56/1.50 % (3600246)Termination phase: Saturation % 4.56/1.50 % (3600246)Time elapsed: 0.171 s % 4.56/1.50 % (3600246)Peak memory usage: 118 MB % 4.56/1.50 % (3600246)Instructions burned: 202 (million) % 4.56/1.50 % (3600259)Instruction limit reached! % 4.56/1.50 % (3600259)------------------------------ % 4.56/1.50 % (3600259)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.56/1.50 % (3600259)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.56/1.50 % (3600259)CaDiCaL version: 2.1.3 % 4.56/1.50 % (3600259)Termination reason: Instruction limit % 4.56/1.50 % (3600259)Termination phase: Saturation % 4.56/1.50 % (3600259)Time elapsed: 0.021 s % 4.56/1.50 % (3600259)Peak memory usage: 88 MB % 4.56/1.50 % (3600259)Instructions burned: 30 (million) % 4.56/1.50 % (3600260)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=542123860:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2997 on theBenchmark for (2997ds/16Mi) % 4.56/1.50 % (3600245)Instruction limit reached! % 4.56/1.50 % (3600245)------------------------------ % 4.56/1.50 % (3600245)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.56/1.50 % (3600245)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.56/1.50 % (3600245)CaDiCaL version: 2.1.3 % 4.56/1.50 % (3600245)Termination reason: Instruction limit % 4.56/1.50 % (3600245)Termination phase: Saturation % 4.56/1.50 % (3600245)Time elapsed: 0.215 s % 4.56/1.50 % (3600245)Peak memory usage: 118 MB % 4.56/1.50 % (3600245)Instructions burned: 307 (million) % 4.56/1.50 % (3600261)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=3352699785:i=24:canc=force:rtra=on_2997 on theBenchmark for (2997ds/24Mi) % 4.56/1.50 % (3600260)Instruction limit reached! % 4.56/1.50 % (3600260)------------------------------ % 4.56/1.50 % (3600260)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.56/1.50 % (3600260)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.56/1.50 % (3600260)CaDiCaL version: 2.1.3 % 4.56/1.50 % (3600260)Termination reason: Instruction limit % 4.56/1.50 % (3600260)Termination phase: Saturation % 4.56/1.50 % (3600260)Time elapsed: 0.010 s % 4.56/1.50 % (3600260)Peak memory usage: 89 MB % 4.56/1.50 % (3600260)Instructions burned: 17 (million) % 4.56/1.50 % (3600261)Instruction limit reached! % 4.56/1.50 % (3600261)------------------------------ % 4.56/1.50 % (3600261)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.56/1.50 % (3600261)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.56/1.50 % (3600261)CaDiCaL version: 2.1.3 % 4.56/1.50 % (3600261)Termination reason: Instruction limit % 4.56/1.50 % (3600261)Termination phase: Saturation % 4.56/1.50 % (3600261)Time elapsed: 0.018 s % 4.56/1.50 % (3600261)Peak memory usage: 89 MB % 4.56/1.50 % (3600261)Instructions burned: 24 (million) % 4.56/1.50 % (3600262)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=3138862273:i=27:canc=cautious:fsr=off:rtra=on_2996 on theBenchmark for (2996ds/27Mi) % 4.56/1.50 % (3600262)Refutation not found, incomplete strategy % 4.56/1.50 % (3600262)------------------------------ % 4.56/1.50 % (3600262)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.17/1.77 % (3600262)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.17/1.77 % (3600262)CaDiCaL version: 2.1.3 % 7.17/1.77 % (3600262)Termination reason: Refutation not found, incomplete strategy % 7.17/1.77 % (3600262)Time elapsed: 0.003 s % 7.17/1.77 % (3600262)Peak memory usage: 89 MB % 7.17/1.77 % (3600262)Instructions burned: 6 (million) % 7.17/1.77 % (3600265)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=3759436576:i=85:gtgl=4:rtra=on:gtg=exists_sym_2996 on theBenchmark for (2996ds/85Mi) % 7.17/1.77 % (3600266)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=2737864306:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2996 on theBenchmark for (2996ds/2Mi) % 7.17/1.77 % (3600266)Instruction limit reached! % 7.17/1.77 % (3600266)------------------------------ % 7.17/1.77 % (3600266)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.17/1.77 % (3600266)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.17/1.77 % (3600266)CaDiCaL version: 2.1.3 % 7.17/1.77 % (3600266)Termination reason: Instruction limit % 7.17/1.77 % (3600266)Termination phase: Property scanning % 7.17/1.77 % (3600266)Time elapsed: 0.002 s % 7.17/1.77 % (3600266)Peak memory usage: 86 MB % 7.17/1.77 % (3600266)Instructions burned: 3 (million) % 7.17/1.77 % (3600269)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=1446756418:i=181:rtra=on:ss=axioms:ev=cautious_2996 on theBenchmark for (2996ds/181Mi) % 7.17/1.77 % (3600270)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=852540934:i=4:ep=RST:ins=2:rtra=on_2996 on theBenchmark for (2996ds/4Mi) % 7.17/1.77 % (3600269)Refutation not found, incomplete strategy % 7.17/1.77 % (3600269)------------------------------ % 7.17/1.77 % (3600269)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.17/1.77 % (3600269)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.17/1.77 % (3600269)CaDiCaL version: 2.1.3 % 7.17/1.77 % (3600269)Termination reason: Refutation not found, incomplete strategy % 7.17/1.77 % (3600269)Time elapsed: 0.001 s % 7.17/1.77 % (3600269)Peak memory usage: 87 MB % 7.17/1.77 % (3600269)Instructions burned: 1 (million) % 7.17/1.77 % (3600270)Instruction limit reached! % 7.17/1.77 % (3600270)------------------------------ % 7.17/1.77 % (3600270)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.17/1.77 % (3600270)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.17/1.77 % (3600270)CaDiCaL version: 2.1.3 % 7.17/1.77 % (3600270)Termination reason: Instruction limit % 7.17/1.77 % (3600270)Termination phase: Saturation % 7.17/1.77 % (3600270)Time elapsed: 0.003 s % 7.17/1.77 % (3600270)Peak memory usage: 86 MB % 7.17/1.77 % (3600270)Instructions burned: 5 (million) % 7.17/1.77 % (3600265)Instruction limit reached! % 7.17/1.77 % (3600265)------------------------------ % 7.17/1.77 % (3600265)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.17/1.77 % (3600265)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.17/1.77 % (3600265)CaDiCaL version: 2.1.3 % 7.17/1.77 % (3600265)Termination reason: Instruction limit % 7.17/1.77 % (3600265)Termination phase: Saturation % 7.17/1.77 % (3600265)Time elapsed: 0.050 s % 7.17/1.77 % (3600265)Peak memory usage: 89 MB % 7.17/1.77 % (3600265)Instructions burned: 86 (million) % 7.17/1.77 % (3600271)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=1603354030:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2995 on theBenchmark for (2995ds/66Mi) % 7.17/1.77 % (3600258)------------------------------ % 7.17/1.77 % (3600258)------------------------------ % 7.17/1.77 % (3600262)------------------------------ % 7.17/1.77 % (3600262)------------------------------ % 7.17/1.77 % (3600271)Instruction limit reached! % 7.17/1.77 % (3600271)------------------------------ % 7.17/1.77 % (3600271)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.17/1.77 % (3600271)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.17/1.77 % (3600271)CaDiCaL version: 2.1.3 % 7.17/1.77 % (3600271)Termination reason: Instruction limit % 7.17/1.77 % (3600271)Termination phase: Saturation % 7.17/1.77 % (3600271)Time elapsed: 0.094 s % 7.17/1.77 % (3600271)Peak memory usage: 135 MB % 7.17/1.77 % (3600271)Instructions burned: 66 (million) % 7.17/1.77 % (3600275)lrs+10_1_thi=all:si=on:fd=off:random_seed=2031816071:i=53:rtra=on:gtg=all_2994 on theBenchmark for (2994ds/53Mi) % 7.17/1.77 % (3600281)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=1885932528:i=2:doe=on:canc=force:asg=cautious:rtra=on_2994 on theBenchmark for (2994ds/2Mi) % 8.23/1.93 % (3600281)Instruction limit reached! % 8.23/1.93 % (3600281)------------------------------ % 8.23/1.93 % (3600281)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.23/1.93 % (3600281)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.23/1.93 % (3600281)CaDiCaL version: 2.1.3 % 8.23/1.93 % (3600281)Termination reason: Instruction limit % 8.23/1.93 % (3600281)Termination phase: Property scanning % 8.23/1.93 % (3600281)Time elapsed: 0.001 s % 8.23/1.93 % (3600281)Peak memory usage: 86 MB % 8.23/1.93 % (3600281)Instructions burned: 2 (million) % 8.23/1.93 % (3600279)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=3426282522:st=3:i=2:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/2Mi) % 8.23/1.93 % (3600278)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=2134949690:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2994 on theBenchmark for (2994ds/8Mi) % 8.23/1.93 % (3600279)Refutation not found, incomplete strategy % 8.23/1.93 % (3600279)------------------------------ % 8.23/1.93 % (3600279)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.23/1.93 % (3600279)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.23/1.93 % (3600279)CaDiCaL version: 2.1.3 % 8.23/1.93 % (3600279)Termination reason: Refutation not found, incomplete strategy % 8.23/1.93 % (3600279)Time elapsed: 0.001 s % 8.23/1.93 % (3600279)Peak memory usage: 88 MB % 8.23/1.93 % (3600279)Instructions burned: 1 (million) % 8.23/1.93 % (3600278)Refutation not found, incomplete strategy % 8.23/1.93 % (3600278)------------------------------ % 8.23/1.93 % (3600278)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.23/1.93 % (3600278)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.23/1.93 % (3600278)CaDiCaL version: 2.1.3 % 8.23/1.93 % (3600278)Termination reason: Refutation not found, incomplete strategy % 8.23/1.93 % (3600278)Time elapsed: 0.005 s % 8.23/1.93 % (3600278)Peak memory usage: 89 MB % 8.23/1.93 % (3600278)Instructions burned: 7 (million) % 8.23/1.93 % (3600282)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=1391849679:i=127:doe=on:rtra=on_2994 on theBenchmark for (2994ds/127Mi) % 8.23/1.93 % (3600275)Instruction limit reached! % 8.23/1.93 % (3600275)------------------------------ % 8.23/1.93 % (3600275)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.23/1.93 % (3600275)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.23/1.93 % (3600275)CaDiCaL version: 2.1.3 % 8.23/1.93 % (3600275)Termination reason: Instruction limit % 8.23/1.93 % (3600275)Termination phase: Saturation % 8.23/1.93 % (3600275)Time elapsed: 0.063 s % 8.23/1.93 % (3600275)Peak memory usage: 116 MB % 8.23/1.93 % (3600275)Instructions burned: 53 (million) % 8.23/1.93 % (3600269)------------------------------ % 8.23/1.93 % (3600269)------------------------------ % 8.23/1.93 % (3600288)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=1834281577:i=26:canc=cautious:av=off:rtra=on_2993 on theBenchmark for (2993ds/26Mi) % 8.23/1.93 % (3600284)dis+10_1_si=on:random_seed=2754748082:i=10:ep=R:rtra=on_2993 on theBenchmark for (2993ds/10Mi) % 8.23/1.93 % (3600288)Refutation not found, incomplete strategy % 8.23/1.93 % (3600288)------------------------------ % 8.23/1.93 % (3600288)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.23/1.93 % (3600288)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.23/1.93 % (3600288)CaDiCaL version: 2.1.3 % 8.23/1.93 % (3600288)Termination reason: Refutation not found, incomplete strategy % 8.23/1.93 % (3600288)Time elapsed: 0.003 s % 8.23/1.93 % (3600288)Peak memory usage: 88 MB % 8.23/1.93 % (3600288)Instructions burned: 7 (million) % 8.23/1.93 % (3600284)Instruction limit reached! % 8.23/1.93 % (3600284)------------------------------ % 8.23/1.93 % (3600284)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.23/1.93 % (3600284)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.23/1.93 % (3600284)CaDiCaL version: 2.1.3 % 8.23/1.93 % (3600284)Termination reason: Instruction limit % 8.23/1.93 % (3600284)Termination phase: Saturation % 8.23/1.93 % (3600284)Time elapsed: 0.007 s % 8.23/1.93 % (3600284)Peak memory usage: 88 MB % 10.41/2.19 % (3600284)Instructions burned: 11 (million) % 10.41/2.19 % (3600282)Instruction limit reached! % 10.41/2.19 % (3600282)------------------------------ % 10.41/2.19 % (3600282)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.41/2.19 % (3600282)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.41/2.19 % (3600282)CaDiCaL version: 2.1.3 % 10.41/2.19 % (3600282)Termination reason: Instruction limit % 10.41/2.19 % (3600282)Termination phase: Saturation % 10.41/2.19 % (3600282)Time elapsed: 0.116 s % 10.41/2.19 % (3600282)Peak memory usage: 118 MB % 10.41/2.19 % (3600282)Instructions burned: 127 (million) % 10.41/2.19 % (3600290)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=295446959: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_2992 on theBenchmark for (2992ds/35Mi) % 10.41/2.19 % (3600290)Instruction limit reached! % 10.41/2.19 % (3600290)------------------------------ % 10.41/2.19 % (3600290)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.41/2.19 % (3600290)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.41/2.19 % (3600290)CaDiCaL version: 2.1.3 % 10.41/2.19 % (3600290)Termination reason: Instruction limit % 10.41/2.19 % (3600290)Termination phase: Saturation % 10.41/2.19 % (3600290)Time elapsed: 0.029 s % 10.41/2.19 % (3600290)Peak memory usage: 89 MB % 10.41/2.19 % (3600290)Instructions burned: 36 (million) % 10.41/2.19 % (3600279)------------------------------ % 10.41/2.19 % (3600279)------------------------------ % 10.41/2.19 % (3600278)------------------------------ % 10.41/2.19 % (3600278)------------------------------ % 10.41/2.19 % (3600292)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=1794022682:i=2:fsr=off:rtra=on:inst=on_2991 on theBenchmark for (2991ds/2Mi) % 10.41/2.19 % (3600292)Instruction limit reached! % 10.41/2.19 % (3600292)------------------------------ % 10.41/2.19 % (3600292)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.41/2.19 % (3600292)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.41/2.19 % (3600292)CaDiCaL version: 2.1.3 % 10.41/2.19 % (3600292)Termination reason: Instruction limit % 10.41/2.19 % (3600292)Termination phase: Property scanning % 10.41/2.19 % (3600292)Time elapsed: 0.002 s % 10.41/2.19 % (3600292)Peak memory usage: 86 MB % 10.41/2.19 % (3600292)Instructions burned: 3 (million) % 10.41/2.19 % (3600288)------------------------------ % 10.41/2.19 % (3600288)------------------------------ % 10.41/2.19 % (3600294)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=2528865831:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2991 on theBenchmark for (2991ds/8Mi) % 10.41/2.19 % (3600294)Instruction limit reached! % 10.41/2.19 % (3600294)------------------------------ % 10.41/2.19 % (3600294)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.41/2.19 % (3600294)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.41/2.19 % (3600294)CaDiCaL version: 2.1.3 % 10.41/2.19 % (3600294)Termination reason: Instruction limit % 10.41/2.19 % (3600294)Termination phase: Saturation % 10.41/2.19 % (3600294)Time elapsed: 0.006 s % 10.41/2.19 % (3600294)Peak memory usage: 88 MB % 10.41/2.19 % (3600294)Instructions burned: 8 (million) % 10.41/2.19 % (3600295)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=297560451:i=370:ep=RS:fsr=off:rtra=on_2991 on theBenchmark for (2991ds/370Mi) % 10.41/2.19 % (3600297)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=457633105:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2990 on theBenchmark for (2990ds/13Mi) % 10.41/2.19 % (3600303)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=443723815:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2990 on theBenchmark for (2990ds/75Mi) % 10.41/2.19 % (3600300)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=2961639896:i=10:rtra=on_2990 on theBenchmark for (2990ds/10Mi) % 10.41/2.19 % (3600301)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=2532052004:i=71:rtra=on:gtg=exists_top_2990 on theBenchmark for (2990ds/71Mi) % 10.41/2.19 % (3600298)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=3856105373:i=226:rtra=on:gtg=position:ss=axioms_2990 on theBenchmark for (2990ds/226Mi) % 10.41/2.19 % (3600300)Instruction limit reached! % 12.00/2.51 % (3600300)------------------------------ % 12.00/2.51 % (3600300)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.00/2.51 % (3600300)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.00/2.51 % (3600300)CaDiCaL version: 2.1.3 % 12.00/2.51 % (3600300)Termination reason: Instruction limit % 12.00/2.51 % (3600300)Termination phase: Saturation % 12.00/2.51 % (3600300)Time elapsed: 0.007 s % 12.00/2.51 % (3600300)Peak memory usage: 88 MB % 12.00/2.51 % (3600300)Instructions burned: 11 (million) % 12.00/2.51 % (3600297)Instruction limit reached! % 12.00/2.51 % (3600297)------------------------------ % 12.00/2.51 % (3600297)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.00/2.51 % (3600297)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.00/2.51 % (3600297)CaDiCaL version: 2.1.3 % 12.00/2.51 % (3600297)Termination reason: Instruction limit % 12.00/2.51 % (3600297)Termination phase: Saturation % 12.00/2.51 % (3600297)Time elapsed: 0.029 s % 12.00/2.51 % (3600297)Peak memory usage: 112 MB % 12.00/2.51 % (3600297)Instructions burned: 13 (million) % 12.00/2.51 % (3600303)Instruction limit reached! % 12.00/2.51 % (3600303)------------------------------ % 12.00/2.51 % (3600303)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.00/2.51 % (3600303)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.00/2.51 % (3600303)CaDiCaL version: 2.1.3 % 12.00/2.51 % (3600303)Termination reason: Instruction limit % 12.00/2.51 % (3600303)Termination phase: Saturation % 12.00/2.51 % (3600303)Time elapsed: 0.029 s % 12.00/2.51 % (3600303)Peak memory usage: 90 MB % 12.00/2.51 % (3600303)Instructions burned: 76 (million) % 12.00/2.51 % (3600298)Refutation not found, incomplete strategy % 12.00/2.51 % (3600298)------------------------------ % 12.00/2.51 % (3600298)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.00/2.51 % (3600298)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.00/2.51 % (3600298)CaDiCaL version: 2.1.3 % 12.00/2.51 % (3600298)Termination reason: Refutation not found, incomplete strategy % 12.00/2.51 % (3600298)Time elapsed: 0.027 s % 12.00/2.51 % (3600298)Peak memory usage: 111 MB % 12.00/2.51 % (3600298)Instructions burned: 6 (million) % 12.00/2.51 % (3600304)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=2355748331:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2990 on theBenchmark for (2990ds/294Mi) % 12.00/2.51 % (3600301)Instruction limit reached! % 12.00/2.51 % (3600301)------------------------------ % 12.00/2.51 % (3600301)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.00/2.51 % (3600301)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.00/2.51 % (3600301)CaDiCaL version: 2.1.3 % 12.00/2.51 % (3600301)Termination reason: Instruction limit % 12.00/2.51 % (3600301)Termination phase: Saturation % 12.00/2.51 % (3600301)Time elapsed: 0.093 s % 12.00/2.51 % (3600301)Peak memory usage: 134 MB % 12.00/2.51 % (3600301)Instructions burned: 72 (million) % 12.00/2.51 % (3600295)Instruction limit reached! % 12.00/2.51 % (3600295)------------------------------ % 12.00/2.51 % (3600295)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.00/2.51 % (3600295)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.00/2.51 % (3600295)CaDiCaL version: 2.1.3 % 12.00/2.51 % (3600295)Termination reason: Instruction limit % 12.00/2.51 % (3600295)Termination phase: Saturation % 12.00/2.51 % (3600295)Time elapsed: 0.189 s % 12.00/2.51 % (3600295)Peak memory usage: 92 MB % 12.00/2.51 % (3600295)Instructions burned: 371 (million) % 12.00/2.51 % (3600313)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=2073893617:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2988 on theBenchmark for (2988ds/40Mi) % 12.00/2.51 % (3600311)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=3343112877:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2989 on theBenchmark for (2989ds/130Mi) % 12.00/2.51 % (3600313)Instruction limit reached! % 12.00/2.51 % (3600313)------------------------------ % 12.00/2.51 % (3600313)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.00/2.51 % (3600313)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.00/2.51 % (3600313)CaDiCaL version: 2.1.3 % 12.00/2.51 % (3600313)Termination reason: Instruction limit % 12.00/2.51 % (3600313)Termination phase: Saturation % 12.00/2.51 % (3600313)Time elapsed: 0.041 s % 14.12/2.85 % (3600313)Peak memory usage: 134 MB % 14.12/2.85 % (3600313)Instructions burned: 41 (million) % 14.12/2.85 % (3600312)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=1712263764:i=131:rtra=on_2988 on theBenchmark for (2988ds/131Mi) % 14.12/2.85 % (3600304)Instruction limit reached! % 14.12/2.85 % (3600304)------------------------------ % 14.12/2.85 % (3600304)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.12/2.85 % (3600304)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.12/2.85 % (3600304)CaDiCaL version: 2.1.3 % 14.12/2.85 % (3600304)Termination reason: Instruction limit % 14.12/2.85 % (3600304)Termination phase: Saturation % 14.12/2.85 % (3600304)Time elapsed: 0.188 s % 14.12/2.85 % (3600304)Peak memory usage: 91 MB % 14.12/2.85 % (3600304)Instructions burned: 294 (million) % 14.12/2.85 % (3600315)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=223430113:i=307:rtra=on:gtg=exists_top_2988 on theBenchmark for (2988ds/307Mi) % 14.12/2.85 % (3600315)Refutation not found, incomplete strategy % 14.12/2.85 % (3600315)------------------------------ % 14.12/2.85 % (3600315)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.12/2.85 % (3600315)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.12/2.85 % (3600315)CaDiCaL version: 2.1.3 % 14.12/2.85 % (3600315)Termination reason: Refutation not found, incomplete strategy % 14.12/2.85 % (3600315)Time elapsed: 0.005 s % 14.12/2.85 % (3600315)Peak memory usage: 89 MB % 14.12/2.85 % (3600315)Instructions burned: 7 (million) % 14.12/2.85 % (3600316)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=2935902428:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2987 on theBenchmark for (2987ds/598Mi) % 14.12/2.85 % (3600298)------------------------------ % 14.12/2.85 % (3600298)------------------------------ % 14.12/2.85 % (3600311)Instruction limit reached! % 14.12/2.85 % (3600311)------------------------------ % 14.12/2.85 % (3600311)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.12/2.85 % (3600311)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.12/2.85 % (3600311)CaDiCaL version: 2.1.3 % 14.12/2.85 % (3600311)Termination reason: Instruction limit % 14.12/2.85 % (3600311)Termination phase: Saturation % 14.12/2.85 % (3600311)Time elapsed: 0.110 s % 14.12/2.85 % (3600311)Peak memory usage: 118 MB % 14.12/2.85 % (3600311)Instructions burned: 131 (million) % 14.12/2.85 % (3600320)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=2792802554:i=131:canc=cautious:fsr=off:rtra=on_2987 on theBenchmark for (2987ds/131Mi) % 14.12/2.85 % (3600312)Instruction limit reached! % 14.12/2.85 % (3600312)------------------------------ % 14.12/2.85 % (3600312)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.12/2.85 % (3600312)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.12/2.85 % (3600312)CaDiCaL version: 2.1.3 % 14.12/2.85 % (3600312)Termination reason: Instruction limit % 14.12/2.85 % (3600312)Termination phase: Saturation % 14.12/2.85 % (3600312)Time elapsed: 0.129 s % 14.12/2.85 % (3600312)Peak memory usage: 134 MB % 14.12/2.85 % (3600312)Instructions burned: 131 (million) % 14.12/2.85 % (3600320)Instruction limit reached! % 14.12/2.85 % (3600320)------------------------------ % 14.12/2.85 % (3600320)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.12/2.85 % (3600320)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.12/2.85 % (3600320)CaDiCaL version: 2.1.3 % 14.12/2.85 % (3600320)Termination reason: Instruction limit % 14.12/2.85 % (3600320)Termination phase: Saturation % 14.12/2.85 % (3600320)Time elapsed: 0.055 s % 14.12/2.85 % (3600320)Peak memory usage: 117 MB % 14.12/2.85 % (3600320)Instructions burned: 133 (million) % 14.12/2.85 % (3600322)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=2331488381:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2986 on theBenchmark for (2986ds/259Mi) % 14.12/2.85 % (3600324)dis+10_1_si=on:random_seed=440305202:s2a=on:i=1000:rtra=on:gtg=exists_all_2986 on theBenchmark for (2986ds/1000Mi) % 14.12/2.85 % (3600325)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=3223974130:i=383:fsr=off:rtra=on:ev=force_2986 on theBenchmark for (2986ds/383Mi) % 14.12/2.85 % (3600322)Refutation not found, incomplete strategy % 14.12/2.85 % (3600322)------------------------------ % 16.56/3.09 % (3600322)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.56/3.09 % (3600322)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.56/3.09 % (3600322)CaDiCaL version: 2.1.3 % 16.56/3.09 % (3600322)Termination reason: Refutation not found, incomplete strategy % 16.56/3.09 % (3600322)Time elapsed: 0.027 s % 16.56/3.09 % (3600322)Peak memory usage: 111 MB % 16.56/3.09 % (3600322)Instructions burned: 6 (million) % 16.56/3.09 % (3600327)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=677494871:i=141:doe=on:rtra=on_2985 on theBenchmark for (2985ds/141Mi) % 16.56/3.09 % (3600315)------------------------------ % 16.56/3.09 % (3600315)------------------------------ % 16.56/3.09 % (3600328)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=2830728078:i=65:nm=16:rtra=on_2985 on theBenchmark for (2985ds/65Mi) % 16.56/3.09 % (3600328)Refutation not found, incomplete strategy % 16.56/3.09 % (3600328)------------------------------ % 16.56/3.09 % (3600328)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.56/3.09 % (3600328)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.56/3.09 % (3600328)CaDiCaL version: 2.1.3 % 16.56/3.09 % (3600328)Termination reason: Refutation not found, incomplete strategy % 16.56/3.09 % (3600328)Time elapsed: 0.030 s % 16.56/3.09 % (3600328)Peak memory usage: 112 MB % 16.56/3.09 % (3600328)Instructions burned: 10 (million) % 16.56/3.09 % (3600327)Instruction limit reached! % 16.56/3.09 % (3600327)------------------------------ % 16.56/3.09 % (3600327)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.56/3.09 % (3600327)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.56/3.09 % (3600327)CaDiCaL version: 2.1.3 % 16.56/3.09 % (3600327)Termination reason: Instruction limit % 16.56/3.09 % (3600327)Termination phase: Saturation % 16.56/3.09 % (3600327)Time elapsed: 0.094 s % 16.56/3.09 % (3600327)Peak memory usage: 90 MB % 16.56/3.09 % (3600327)Instructions burned: 142 (million) % 16.56/3.09 % (3600325)Instruction limit reached! % 16.56/3.09 % (3600325)------------------------------ % 16.56/3.09 % (3600325)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.56/3.09 % (3600325)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.56/3.09 % (3600325)CaDiCaL version: 2.1.3 % 16.56/3.09 % (3600325)Termination reason: Instruction limit % 16.56/3.09 % (3600325)Termination phase: Saturation % 16.56/3.09 % (3600325)Time elapsed: 0.212 s % 16.56/3.09 % (3600325)Peak memory usage: 95 MB % 16.56/3.09 % (3600325)Instructions burned: 385 (million) % 16.56/3.09 % (3600333)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=933333434:i=121:nm=16:rtra=on_2984 on theBenchmark for (2984ds/121Mi) % 16.56/3.09 % (3600322)------------------------------ % 16.56/3.09 % (3600322)------------------------------ % 16.56/3.09 % (3600316)Instruction limit reached! % 16.56/3.09 % (3600316)------------------------------ % 16.56/3.09 % (3600316)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.56/3.09 % (3600316)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.56/3.09 % (3600316)CaDiCaL version: 2.1.3 % 16.56/3.09 % (3600316)Termination reason: Instruction limit % 16.56/3.09 % (3600316)Termination phase: Saturation % 16.56/3.09 % (3600316)Time elapsed: 0.455 s % 16.56/3.09 % (3600316)Peak memory usage: 139 MB % 16.56/3.09 % (3600316)Instructions burned: 598 (million) % 16.56/3.09 % (3600335)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=775326355:s2a=on:i=128:s2at=5:ins=3:rtra=on_2983 on theBenchmark for (2983ds/128Mi) % 16.56/3.09 % (3600333)Instruction limit reached! % 16.56/3.09 % (3600333)------------------------------ % 16.56/3.09 % (3600333)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.56/3.09 % (3600333)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.56/3.09 % (3600333)CaDiCaL version: 2.1.3 % 16.56/3.09 % (3600333)Termination reason: Instruction limit % 16.56/3.09 % (3600333)Termination phase: Saturation % 16.56/3.09 % (3600333)Time elapsed: 0.073 s % 16.56/3.09 % (3600333)Peak memory usage: 89 MB % 16.56/3.09 % (3600333)Instructions burned: 122 (million) % 16.56/3.09 % (3600324)Instruction limit reached! % 16.56/3.09 % (3600324)------------------------------ % 16.56/3.09 % (3600324)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.56/3.09 % (3600324)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.48/3.41 % (3600324)CaDiCaL version: 2.1.3 % 18.48/3.41 % (3600324)Termination reason: Instruction limit % 18.48/3.41 % (3600324)Termination phase: Saturation % 18.48/3.41 % (3600324)Time elapsed: 0.327 s % 18.48/3.41 % (3600324)Peak memory usage: 95 MB % 18.48/3.41 % (3600324)Instructions burned: 1003 (million) % 18.48/3.41 % (3600335)Refutation not found, incomplete strategy % 18.48/3.41 % (3600335)------------------------------ % 18.48/3.41 % (3600335)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.48/3.41 % (3600335)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.48/3.41 % (3600335)CaDiCaL version: 2.1.3 % 18.48/3.41 % (3600335)Termination reason: Refutation not found, incomplete strategy % 18.48/3.41 % (3600335)Time elapsed: 0.032 s % 18.48/3.41 % (3600335)Peak memory usage: 113 MB % 18.48/3.41 % (3600335)Instructions burned: 12 (million) % 18.48/3.41 % (3600336)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=2077339995:i=39:ins=3:rtra=on_2982 on theBenchmark for (2982ds/39Mi) % 18.48/3.41 % (3600328)------------------------------ % 18.48/3.41 % (3600328)------------------------------ % 18.48/3.41 % (3600336)Refutation not found, incomplete strategy % 18.48/3.41 % (3600336)------------------------------ % 18.48/3.41 % (3600336)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.48/3.41 % (3600336)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.48/3.41 % (3600336)CaDiCaL version: 2.1.3 % 18.48/3.41 % (3600336)Termination reason: Refutation not found, incomplete strategy % 18.48/3.41 % (3600336)Time elapsed: 0.031 s % 18.48/3.41 % (3600336)Peak memory usage: 112 MB % 18.48/3.41 % (3600336)Instructions burned: 11 (million) % 18.48/3.41 % (3600338)dis+1010_1_to=kbo:si=on:random_seed=967285009:i=175:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2982 on theBenchmark for (2982ds/175Mi) % 18.48/3.41 % (3600342)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=1931452496:thitd=on:i=215:nm=0:rtra=on:ev=force_2981 on theBenchmark for (2981ds/215Mi) % 18.48/3.41 % (3600340)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=2670736944:i=329:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2981 on theBenchmark for (2981ds/329Mi) % 18.48/3.41 % (3600341)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=3308793997:s2a=on:i=483:doe=on:nm=32:rtra=on_2981 on theBenchmark for (2981ds/483Mi) % 18.48/3.41 % (3600338)Instruction limit reached! % 18.48/3.41 % (3600338)------------------------------ % 18.48/3.41 % (3600338)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.48/3.41 % (3600338)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.48/3.41 % (3600338)CaDiCaL version: 2.1.3 % 18.48/3.41 % (3600338)Termination reason: Instruction limit % 18.48/3.41 % (3600338)Termination phase: Saturation % 18.48/3.41 % (3600338)Time elapsed: 0.121 s % 18.48/3.41 % (3600338)Peak memory usage: 91 MB % 18.48/3.41 % (3600338)Instructions burned: 176 (million) % 18.48/3.41 % (3600342)Instruction limit reached! % 18.48/3.41 % (3600342)------------------------------ % 18.48/3.41 % (3600342)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.48/3.41 % (3600342)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.48/3.41 % (3600342)CaDiCaL version: 2.1.3 % 18.48/3.41 % (3600342)Termination reason: Instruction limit % 18.48/3.41 % (3600342)Termination phase: Saturation % 18.48/3.41 % (3600342)Time elapsed: 0.098 s % 18.48/3.41 % (3600342)Peak memory usage: 136 MB % 18.48/3.41 % (3600342)Instructions burned: 218 (million) % 18.48/3.41 % (3600344)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=1091799126:i=349:rtra=on_2981 on theBenchmark for (2981ds/349Mi) % 18.48/3.41 % (3600335)------------------------------ % 18.48/3.41 % (3600335)------------------------------ % 18.48/3.41 % (3600336)------------------------------ % 18.48/3.41 % (3600336)------------------------------ % 18.48/3.41 % (3600351)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=9739037:i=328:kws=inv_frequency:nm=20:rtra=on_2979 on theBenchmark for (2979ds/328Mi) % 18.48/3.41 % (3600349)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=261391399:st=2:i=295:rtra=on:ss=axioms_2979 on theBenchmark for (2979ds/295Mi) % 18.48/3.41 % (3600349)Refutation not found, incomplete strategy % 20.07/3.72 % (3600349)------------------------------ % 20.07/3.72 % (3600349)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.07/3.72 % (3600349)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.07/3.72 % (3600349)CaDiCaL version: 2.1.3 % 20.07/3.72 % (3600349)Termination reason: Refutation not found, incomplete strategy % 20.07/3.72 % (3600349)Time elapsed: 0.002 s % 20.07/3.72 % (3600349)Peak memory usage: 88 MB % 20.07/3.72 % (3600349)Instructions burned: 2 (million) % 20.07/3.72 % (3600340)Instruction limit reached! % 20.07/3.72 % (3600340)------------------------------ % 20.07/3.72 % (3600340)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.07/3.72 % (3600340)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.07/3.72 % (3600340)CaDiCaL version: 2.1.3 % 20.07/3.72 % (3600340)Termination reason: Instruction limit % 20.07/3.72 % (3600340)Termination phase: Saturation % 20.07/3.72 % (3600340)Time elapsed: 0.247 s % 20.07/3.72 % (3600340)Peak memory usage: 119 MB % 20.07/3.72 % (3600340)Instructions burned: 331 (million) % 20.07/3.72 % (3600352)dis+1010_1_to=lpo:sil=128000:sas=z3:si=on:nwc=5:random_seed=3671229342:i=281:gtgl=2:rtra=on:gtg=all_2978 on theBenchmark for (2978ds/281Mi) % 20.07/3.72 % (3600344)Instruction limit reached! % 20.07/3.72 % (3600344)------------------------------ % 20.07/3.72 % (3600344)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.07/3.72 % (3600344)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.07/3.72 % (3600344)CaDiCaL version: 2.1.3 % 20.07/3.72 % (3600344)Termination reason: Instruction limit % 20.07/3.72 % (3600344)Termination phase: Saturation % 20.07/3.72 % (3600344)Time elapsed: 0.233 s % 20.07/3.72 % (3600344)Peak memory usage: 120 MB % 20.07/3.72 % (3600344)Instructions burned: 350 (million) % 20.07/3.72 % (3600351)Instruction limit reached! % 20.07/3.72 % (3600351)------------------------------ % 20.07/3.72 % (3600351)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.07/3.72 % (3600351)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.07/3.72 % (3600351)CaDiCaL version: 2.1.3 % 20.07/3.72 % (3600351)Termination reason: Instruction limit % 20.07/3.72 % (3600351)Termination phase: Saturation % 20.07/3.72 % (3600351)Time elapsed: 0.127 s % 20.07/3.72 % (3600351)Peak memory usage: 119 MB % 20.07/3.72 % (3600351)Instructions burned: 328 (million) % 20.07/3.72 % (3600353)lrs+1010_1_to=kbo:sil=128000:si=on:sos=on:urr=on:uwa=alasca_main:random_seed=1822663542:i=484:doe=on:nm=0:av=off:rtra=on:ss=axioms_2978 on theBenchmark for (2978ds/484Mi) % 20.07/3.72 % (3600353)Refutation not found, incomplete strategy % 20.07/3.72 % (3600353)------------------------------ % 20.07/3.72 % (3600353)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.07/3.72 % (3600353)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.07/3.72 % (3600353)CaDiCaL version: 2.1.3 % 20.07/3.72 % (3600353)Termination reason: Refutation not found, incomplete strategy % 20.07/3.72 % (3600353)Time elapsed: 0.002 s % 20.07/3.72 % (3600353)Peak memory usage: 87 MB % 20.07/3.72 % (3600353)Instructions burned: 2 (million) % 20.07/3.72 % (3600341)Instruction limit reached! % 20.07/3.72 % (3600341)------------------------------ % 20.07/3.72 % (3600341)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.07/3.72 % (3600341)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.07/3.72 % (3600341)CaDiCaL version: 2.1.3 % 20.07/3.72 % (3600341)Termination reason: Instruction limit % 20.07/3.72 % (3600341)Termination phase: Saturation % 20.07/3.72 % (3600341)Time elapsed: 0.357 s % 20.07/3.72 % (3600341)Peak memory usage: 137 MB % 20.07/3.72 % (3600341)Instructions burned: 483 (million) % 20.07/3.72 % (3600356)lrs+21_1_to=kbo:sil=128000:thi=neg_eq:si=on:random_seed=1128366875:i=321:canc=force:rtra=on:tac=axiom:ss=axioms:ev=force_2977 on theBenchmark for (2977ds/321Mi) % 20.07/3.72 % (3600359)lrs+1010_1_to=kbo:tgt=ground:fde=unused:sas=z3:si=on:sp=unary_frequency:gve=force:spb=goal:tha=off:random_seed=2262638679:i=471:thf=on:kws=precedence:rtra=on_2976 on theBenchmark for (2976ds/471Mi) % 20.07/3.72 % (3600356)Refutation not found, incomplete strategy % 20.07/3.72 % (3600356)------------------------------ % 20.07/3.72 % (3600356)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.07/3.72 % (3600356)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.07/3.72 % (3600356)CaDiCaL version: 2.1.3 % 22.26/4.00 % (3600356)Termination reason: Refutation not found, incomplete strategy % 22.26/4.00 % (3600356)Time elapsed: 0.027 s % 22.26/4.00 % (3600356)Peak memory usage: 112 MB % 22.26/4.00 % (3600356)Instructions burned: 6 (million) % 22.26/4.00 % (3600349)------------------------------ % 22.26/4.00 % (3600349)------------------------------ % 22.26/4.00 % (3600358)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=1205075362:i=416:rtra=on:gtg=position:ss=axioms_2977 on theBenchmark for (2977ds/416Mi) % 22.26/4.00 % (3600352)Instruction limit reached! % 22.26/4.00 % (3600352)------------------------------ % 22.26/4.00 % (3600352)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 22.26/4.00 % (3600352)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.26/4.00 % (3600352)CaDiCaL version: 2.1.3 % 22.26/4.00 % (3600352)Termination reason: Instruction limit % 22.26/4.00 % (3600352)Termination phase: Saturation % 22.26/4.00 % (3600352)Time elapsed: 0.212 s % 22.26/4.00 % (3600352)Peak memory usage: 118 MB % 22.26/4.00 % (3600352)Instructions burned: 281 (million) % 22.26/4.00 % (3600358)Refutation not found, incomplete strategy % 22.26/4.00 % (3600358)------------------------------ % 22.26/4.00 % (3600358)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 22.26/4.00 % (3600358)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.26/4.00 % (3600358)CaDiCaL version: 2.1.3 % 22.26/4.00 % (3600358)Termination reason: Refutation not found, incomplete strategy % 22.26/4.00 % (3600358)Time elapsed: 0.027 s % 22.26/4.00 % (3600358)Peak memory usage: 111 MB % 22.26/4.00 % (3600358)Instructions burned: 6 (million) % 22.26/4.00 % (3600361)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=2319902180:avsq=on:i=276:avsqr=1,2:rtra=on_2976 on theBenchmark for (2976ds/276Mi) % 22.26/4.00 % (3600353)------------------------------ % 22.26/4.00 % (3600353)------------------------------ % 22.26/4.00 % (3600359)Instruction limit reached! % 22.26/4.00 % (3600359)------------------------------ % 22.26/4.00 % (3600359)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 22.26/4.00 % (3600359)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.26/4.00 % (3600359)CaDiCaL version: 2.1.3 % 22.26/4.00 % (3600359)Termination reason: Instruction limit % 22.26/4.00 % (3600359)Termination phase: Saturation % 22.26/4.00 % (3600359)Time elapsed: 0.167 s % 22.26/4.00 % (3600359)Peak memory usage: 121 MB % 22.26/4.00 % (3600359)Instructions burned: 474 (million) % 22.26/4.00 % (3600364)lrs+1010_2_to=kbo:sil=128000:tgt=ground:fde=unused:sas=z3:si=on:uwa=off:tha=off:nwc=1:random_seed=3249355293:i=375:kws=inv_arity_squared:rtra=on_2975 on theBenchmark for (2975ds/375Mi) % 22.26/4.00 % (3600366)lrs+10_1_to=kbo:sil=128000:tgt=full:sas=z3:si=on:uwa=func_ext:slsqc=1:flr=on:slsq=on:random_seed=1370633180:i=387:bd=preordered:rtra=on:ss=axioms:sgt=8_2975 on theBenchmark for (2975ds/387Mi) % 22.26/4.00 % (3600356)------------------------------ % 22.26/4.00 % (3600356)------------------------------ % 22.26/4.00 % (3600366)Refutation not found, incomplete strategy % 22.26/4.00 % (3600366)------------------------------ % 22.26/4.00 % (3600366)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 22.26/4.00 % (3600366)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.26/4.00 % (3600366)CaDiCaL version: 2.1.3 % 22.26/4.00 % (3600366)Termination reason: Refutation not found, incomplete strategy % 22.26/4.00 % (3600366)Time elapsed: 0.028 s % 22.26/4.00 % (3600366)Peak memory usage: 111 MB % 22.26/4.00 % (3600366)Instructions burned: 7 (million) % 22.26/4.00 % (3600369)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=3694260014:i=334:rtra=on_2974 on theBenchmark for (2974ds/334Mi) % 22.26/4.00 % (3600368)lrs+10_1_to=kbo:sil=128000:fde=none:si=on:norm_ineq=on:urr=on:nwc=0.5:random_seed=3999237710:i=513:kws=frequency:bd=all:rtra=on:gtg=exists_all:ss=axioms:sgt=4_2974 on theBenchmark for (2974ds/513Mi) % 22.26/4.00 % (3600358)------------------------------ % 22.26/4.00 % (3600358)------------------------------ % 22.26/4.00 % (3600361)Instruction limit reached! % 22.26/4.00 % (3600361)------------------------------ % 22.26/4.00 % (3600361)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 22.26/4.00 % (3600361)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.26/4.00 % (3600361)CaDiCaL version: 2.1.3 % 26.41/4.46 % (3600361)Termination reason: Instruction limit % 26.41/4.46 % (3600361)Termination phase: Saturation % 26.41/4.46 % (3600361)Time elapsed: 0.228 s % 26.41/4.46 % (3600361)Peak memory usage: 136 MB % 26.41/4.46 % (3600361)Instructions burned: 277 (million) % 26.41/4.46 % (3600372)lrs+1010_1_to=kbo:sil=64000:sas=cadical:si=on:sos=on:bce=on:random_seed=3921963243:i=359:rtra=on:gtg=exists_top:ss=axioms_2973 on theBenchmark for (2973ds/359Mi) % 26.41/4.46 % (3600372)Refutation not found, incomplete strategy % 26.41/4.46 % (3600372)------------------------------ % 26.41/4.46 % (3600372)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.41/4.46 % (3600372)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.41/4.46 % (3600372)CaDiCaL version: 2.1.3 % 26.41/4.46 % (3600372)Termination reason: Refutation not found, incomplete strategy % 26.41/4.46 % (3600372)Time elapsed: 0.002 s % 26.41/4.46 % (3600372)Peak memory usage: 88 MB % 26.41/4.46 % (3600372)Instructions burned: 2 (million) % 26.41/4.46 % (3600364)Instruction limit reached! % 26.41/4.46 % (3600364)------------------------------ % 26.41/4.46 % (3600364)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.41/4.46 % (3600364)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.41/4.46 % (3600364)CaDiCaL version: 2.1.3 % 26.41/4.46 % (3600364)Termination reason: Instruction limit % 26.41/4.46 % (3600364)Termination phase: Saturation % 26.41/4.46 % (3600364)Time elapsed: 0.255 s % 26.41/4.46 % (3600364)Peak memory usage: 119 MB % 26.41/4.46 % (3600364)Instructions burned: 375 (million) % 26.41/4.46 % (3600369)Instruction limit reached! % 26.41/4.46 % (3600369)------------------------------ % 26.41/4.46 % (3600369)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.41/4.46 % (3600369)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.41/4.46 % (3600369)CaDiCaL version: 2.1.3 % 26.41/4.46 % (3600369)Termination reason: Instruction limit % 26.41/4.46 % (3600369)Termination phase: Saturation % 26.41/4.46 % (3600369)Time elapsed: 0.139 s % 26.41/4.46 % (3600369)Peak memory usage: 136 MB % 26.41/4.46 % (3600369)Instructions burned: 335 (million) % 26.41/4.46 % (3600375)dis+1010_1_to=lpo:sil=128000:thi=all:fde=unused:si=on:sp=reverse_arity:tha=off:random_seed=3304839186:i=341:gtgl=2:rtra=on:gtg=exists_sym:ev=force:fsd=on:fsdmm=1_2972 on theBenchmark for (2972ds/341Mi) % 26.41/4.46 % (3600376)lrs-2_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_max:tha=off:random_seed=2831886547:st=1.5:i=261:sd=1:kws=precedence:rtra=on:ss=axioms_2972 on theBenchmark for (2972ds/261Mi) % 26.41/4.46 % (3600366)------------------------------ % 26.41/4.46 % (3600366)------------------------------ % 26.41/4.46 % (3600376)Refutation not found, incomplete strategy % 26.41/4.46 % (3600376)------------------------------ % 26.41/4.46 % (3600376)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.41/4.46 % (3600376)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.41/4.46 % (3600376)CaDiCaL version: 2.1.3 % 26.41/4.46 % (3600376)Termination reason: Refutation not found, incomplete strategy % 26.41/4.46 % (3600376)Time elapsed: 0.027 s % 26.41/4.46 % (3600376)Peak memory usage: 111 MB % 26.41/4.46 % (3600376)Instructions burned: 5 (million) % 26.41/4.46 % (3600379)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=1374925715:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2971 on theBenchmark for (2971ds/273Mi) % 26.41/4.46 % (3600378)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=954462912:s2pl=no:i=235:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2971 on theBenchmark for (2971ds/235Mi) % 26.41/4.46 % (3600368)Instruction limit reached! % 26.41/4.46 % (3600368)------------------------------ % 26.41/4.46 % (3600368)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.41/4.46 % (3600368)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.41/4.46 % (3600368)CaDiCaL version: 2.1.3 % 26.41/4.46 % (3600368)Termination reason: Instruction limit % 26.41/4.46 % (3600368)Termination phase: Saturation % 26.41/4.46 % (3600368)Time elapsed: 0.315 s % 26.41/4.46 % (3600368)Peak memory usage: 92 MB % 26.41/4.46 % (3600368)Instructions burned: 513 (million) % 26.41/4.46 % (3600378)Refutation not found, incomplete strategy % 26.41/4.46 % (3600378)------------------------------ % 26.41/4.46 % (3600378)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 28.48/4.87 % (3600378)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.48/4.87 % (3600378)CaDiCaL version: 2.1.3 % 28.48/4.87 % (3600378)Termination reason: Refutation not found, incomplete strategy % 28.48/4.87 % (3600378)Time elapsed: 0.027 s % 28.48/4.87 % (3600378)Peak memory usage: 111 MB % 28.48/4.87 % (3600378)Instructions burned: 6 (million) % 28.48/4.87 % (3600379)Instruction limit reached! % 28.48/4.87 % (3600379)------------------------------ % 28.48/4.87 % (3600379)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 28.48/4.87 % (3600379)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.48/4.87 % (3600379)CaDiCaL version: 2.1.3 % 28.48/4.87 % (3600379)Termination reason: Instruction limit % 28.48/4.87 % (3600379)Termination phase: Saturation % 28.48/4.87 % (3600379)Time elapsed: 0.094 s % 28.48/4.87 % (3600379)Peak memory usage: 91 MB % 28.48/4.87 % (3600379)Instructions burned: 273 (million) % 28.48/4.87 % (3600372)------------------------------ % 28.48/4.87 % (3600372)------------------------------ % 28.48/4.87 % (3600382)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=3883504633:i=146:doe=on:rtra=on_2970 on theBenchmark for (2970ds/146Mi) % 28.48/4.87 % (3600375)Instruction limit reached! % 28.48/4.87 % (3600375)------------------------------ % 28.48/4.87 % (3600375)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 28.48/4.87 % (3600375)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.48/4.87 % (3600375)CaDiCaL version: 2.1.3 % 28.48/4.87 % (3600375)Termination reason: Instruction limit % 28.48/4.87 % (3600375)Termination phase: Saturation % 28.48/4.87 % (3600375)Time elapsed: 0.224 s % 28.48/4.87 % (3600375)Peak memory usage: 120 MB % 28.48/4.87 % (3600375)Instructions burned: 342 (million) % 28.48/4.87 % (3600376)------------------------------ % 28.48/4.87 % (3600376)------------------------------ % 28.48/4.87 % (3600385)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=2135289314:i=4428:doe=on:fsr=off:rtra=on_2969 on theBenchmark for (2969ds/4428Mi) % 28.48/4.87 % (3600386)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=758242586:avsq=on:i=276:avsqr=1,2:rtra=on_2969 on theBenchmark for (2969ds/276Mi) % 28.48/4.87 % (3600382)Instruction limit reached! % 28.48/4.87 % (3600382)------------------------------ % 28.48/4.87 % (3600382)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 28.48/4.87 % (3600382)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.48/4.87 % (3600382)CaDiCaL version: 2.1.3 % 28.48/4.87 % (3600382)Termination reason: Instruction limit % 28.48/4.87 % (3600382)Termination phase: Saturation % 28.48/4.87 % (3600382)Time elapsed: 0.099 s % 28.48/4.87 % (3600382)Peak memory usage: 90 MB % 28.48/4.87 % (3600382)Instructions burned: 146 (million) % 28.48/4.87 % (3600387)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=48234468:i=1052:rtra=on_2969 on theBenchmark for (2969ds/1052Mi) % 28.48/4.87 % (3600389)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=3962157064:i=655:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2968 on theBenchmark for (2968ds/655Mi) % 28.48/4.87 % (3600378)------------------------------ % 28.48/4.87 % (3600378)------------------------------ % 28.48/4.87 % (3600386)Instruction limit reached! % 28.48/4.87 % (3600386)------------------------------ % 28.48/4.87 % (3600386)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 28.48/4.87 % (3600386)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.48/4.87 % (3600386)CaDiCaL version: 2.1.3 % 28.48/4.87 % (3600386)Termination reason: Instruction limit % 28.48/4.87 % (3600386)Termination phase: Saturation % 28.48/4.87 % (3600386)Time elapsed: 0.124 s % 28.48/4.87 % (3600386)Peak memory usage: 136 MB % 28.48/4.87 % (3600386)Instructions burned: 277 (million) % 28.48/4.87 % (3600391)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=2332008785:st=5:i=1054:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2968 on theBenchmark for (2968ds/1054Mi) % 28.48/4.87 % (3600391)Refutation not found, incomplete strategy % 28.48/4.87 % (3600391)------------------------------ % 28.48/4.87 % (3600391)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 28.48/4.87 % (3600391)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.48/4.87 % (3600391)CaDiCaL version: 2.1.3 % 32.64/5.37 % (3600391)Termination reason: Refutation not found, incomplete strategy % 32.64/5.37 % (3600391)Time elapsed: 0.001 s % 32.64/5.37 % (3600391)Peak memory usage: 87 MB % 32.64/5.37 % (3600391)Instructions burned: 1 (million) % 32.64/5.37 % (3600393)lrs-1002_1_to=kbo:sas=z3:si=on:norm_ineq=on:sos=on:tha=some:random_seed=3650343280:i=107:rtra=on_2968 on theBenchmark for (2968ds/107Mi) % 32.64/5.37 % (3600393)Refutation not found, incomplete strategy % 32.64/5.37 % (3600393)------------------------------ % 32.64/5.37 % (3600393)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.64/5.37 % (3600393)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.64/5.37 % (3600393)CaDiCaL version: 2.1.3 % 32.64/5.37 % (3600393)Termination reason: Refutation not found, incomplete strategy % 32.64/5.37 % (3600393)Time elapsed: 0.032 s % 32.64/5.37 % (3600393)Peak memory usage: 112 MB % 32.64/5.37 % (3600393)Instructions burned: 11 (million) % 32.64/5.37 % (3600397)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 % 32.64/5.37 % (3600397)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=1030840847:i=1090:aac=none:nm=0:rtra=on:rawr=on_2966 on theBenchmark for (2966ds/1090Mi) % 32.64/5.37 % (3600396)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=263500765:s2a=on:i=450:doe=on:nm=32:rtra=on_2966 on theBenchmark for (2966ds/450Mi) % 32.64/5.37 % (3600391)------------------------------ % 32.64/5.37 % (3600391)------------------------------ % 32.64/5.37 % (3600389)Instruction limit reached! % 32.64/5.37 % (3600389)------------------------------ % 32.64/5.37 % (3600389)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.64/5.37 % (3600389)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.64/5.37 % (3600389)CaDiCaL version: 2.1.3 % 32.64/5.37 % (3600389)Termination reason: Instruction limit % 32.64/5.37 % (3600389)Termination phase: Saturation % 32.64/5.37 % (3600389)Time elapsed: 0.328 s % 32.64/5.37 % (3600389)Peak memory usage: 94 MB % 32.64/5.37 % (3600389)Instructions burned: 657 (million) % 32.64/5.37 % (3600393)------------------------------ % 32.64/5.37 % (3600393)------------------------------ % 32.64/5.37 % (3600402)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=3939173667:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2964 on theBenchmark for (2964ds/130Mi) % 32.64/5.37 % (3600403)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=475975666:i=312:kws=inv_frequency:nm=20:rtra=on_2963 on theBenchmark for (2963ds/312Mi) % 32.64/5.37 % (3600404)ott+10_1_to=kbo:sil=64000:si=on:sp=reverse_frequency:sos=on:random_seed=2082073829:i=491:doe=on:rtra=on:gtg=position_2963 on theBenchmark for (2963ds/491Mi) % 32.64/5.37 % (3600396)Instruction limit reached! % 32.64/5.37 % (3600396)------------------------------ % 32.64/5.37 % (3600396)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.64/5.37 % (3600396)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.64/5.37 % (3600396)CaDiCaL version: 2.1.3 % 32.64/5.37 % (3600396)Termination reason: Instruction limit % 32.64/5.37 % (3600396)Termination phase: Saturation % 32.64/5.37 % (3600396)Time elapsed: 0.332 s % 32.64/5.37 % (3600396)Peak memory usage: 136 MB % 32.64/5.37 % (3600396)Instructions burned: 450 (million) % 32.64/5.37 % (3600404)Refutation not found, incomplete strategy % 32.64/5.37 % (3600404)------------------------------ % 32.64/5.37 % (3600404)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.64/5.37 % (3600404)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.64/5.37 % (3600404)CaDiCaL version: 2.1.3 % 32.64/5.37 % (3600404)Termination reason: Refutation not found, incomplete strategy % 32.64/5.37 % (3600404)Time elapsed: 0.005 s % 32.64/5.37 % (3600404)Peak memory usage: 89 MB % 32.64/5.37 % (3600404)Instructions burned: 7 (million) % 32.64/5.37 % (3600397)Instruction limit reached! % 32.64/5.37 % (3600397)------------------------------ % 32.64/5.37 % (3600397)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.64/5.37 % (3600397)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.64/5.37 % (3600397)CaDiCaL version: 2.1.3 % 32.64/5.37 % (3600397)Termination reason: Instruction limit % 34.33/5.89 % (3600397)Termination phase: Saturation % 34.33/5.89 % (3600397)Time elapsed: 0.350 s % 34.33/5.89 % (3600397)Peak memory usage: 124 MB % 34.33/5.89 % (3600397)Instructions burned: 1090 (million) % 34.33/5.89 % (3600402)Instruction limit reached! % 34.33/5.89 % (3600402)------------------------------ % 34.33/5.89 % (3600402)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.33/5.89 % (3600402)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.33/5.89 % (3600402)CaDiCaL version: 2.1.3 % 34.33/5.89 % (3600402)Termination reason: Instruction limit % 34.33/5.89 % (3600402)Termination phase: Saturation % 34.33/5.89 % (3600402)Time elapsed: 0.106 s % 34.33/5.89 % (3600402)Peak memory usage: 118 MB % 34.33/5.89 % (3600402)Instructions burned: 131 (million) % 34.33/5.89 % (3600387)Instruction limit reached! % 34.33/5.89 % (3600387)------------------------------ % 34.33/5.89 % (3600387)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.33/5.89 % (3600387)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.33/5.89 % (3600387)CaDiCaL version: 2.1.3 % 34.33/5.89 % (3600387)Termination reason: Instruction limit % 34.33/5.89 % (3600387)Termination phase: Saturation % 34.33/5.89 % (3600387)Time elapsed: 0.620 s % 34.33/5.89 % (3600387)Peak memory usage: 94 MB % 34.33/5.89 % (3600387)Instructions burned: 1052 (million) % 34.33/5.89 % (3600409)ott+1011_2_to=lpo:sil=128000:si=on:sos=on:random_seed=1781334239:i=307:bd=preordered:av=off:rtra=on:ev=cautious_2962 on theBenchmark for (2962ds/307Mi) % 34.33/5.89 % (3600408)ott+1011_4:1_to=lpo:sil=64000:si=on:spb=intro:random_seed=2737810419:s2a=on:i=835:s2at=2:rtra=on_2962 on theBenchmark for (2962ds/835Mi) % 34.33/5.89 % (3600409)Refutation not found, incomplete strategy % 34.33/5.89 % (3600409)------------------------------ % 34.33/5.89 % (3600409)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.33/5.89 % (3600409)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.33/5.89 % (3600409)CaDiCaL version: 2.1.3 % 34.33/5.89 % (3600409)Termination reason: Refutation not found, incomplete strategy % 34.33/5.89 % (3600409)Time elapsed: 0.003 s % 34.33/5.89 % (3600409)Peak memory usage: 88 MB % 34.33/5.89 % (3600409)Instructions burned: 8 (million) % 34.33/5.89 % (3600403)Instruction limit reached! % 34.33/5.89 % (3600403)------------------------------ % 34.33/5.89 % (3600403)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.33/5.89 % (3600403)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.33/5.89 % (3600403)CaDiCaL version: 2.1.3 % 34.33/5.89 % (3600403)Termination reason: Instruction limit % 34.33/5.89 % (3600403)Termination phase: Saturation % 34.33/5.89 % (3600403)Time elapsed: 0.228 s % 34.33/5.89 % (3600403)Peak memory usage: 119 MB % 34.33/5.89 % (3600403)Instructions burned: 312 (million) % 34.33/5.89 % (3600410)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=164168529:i=776:doe=on:rtra=on_2961 on theBenchmark for (2961ds/776Mi) % 34.33/5.89 % (3600404)------------------------------ % 34.33/5.89 % (3600404)------------------------------ % 34.33/5.89 % (3600411)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=1048018810:s2a=on:i=646:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2961 on theBenchmark for (2961ds/646Mi) % 34.33/5.89 % (3600409)------------------------------ % 34.33/5.89 % (3600409)------------------------------ % 34.33/5.89 % (3600415)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=118511412:thitd=on:cond=fast:i=784:nm=30:rtra=on:gtg=all:tac=axiom_2959 on theBenchmark for (2959ds/784Mi) % 34.33/5.89 % (3600418)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=1131255253:s2pl=no:i=246:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2959 on theBenchmark for (2959ds/246Mi) % 34.33/5.89 % (3600416)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=104924795:thitd=on:s2a=on:i=1131:add=on:canc=force:bd=all:rtra=on:tac=axiom:ev=off_2959 on theBenchmark for (2959ds/1131Mi) % 34.33/5.89 % (3600418)Refutation not found, incomplete strategy % 34.33/5.89 % (3600418)------------------------------ % 34.33/5.89 % (3600418)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.33/5.89 % (3600418)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.33/5.89 % (3600418)CaDiCaL version: 2.1.3 % 41.31/6.59 % (3600418)Termination reason: Refutation not found, incomplete strategy % 41.31/6.59 % (3600418)Time elapsed: 0.016 s % 41.31/6.59 % (3600418)Peak memory usage: 111 MB % 41.31/6.59 % (3600418)Instructions burned: 6 (million) % 41.31/6.59 % (3600418)------------------------------ % 41.31/6.59 % (3600418)------------------------------ % 41.31/6.59 % (3600408)Instruction limit reached! % 41.31/6.59 % (3600408)------------------------------ % 41.31/6.59 % (3600408)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 41.31/6.59 % (3600408)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.31/6.59 % (3600408)CaDiCaL version: 2.1.3 % 41.31/6.59 % (3600408)Termination reason: Instruction limit % 41.31/6.59 % (3600408)Termination phase: Saturation % 41.31/6.59 % (3600408)Time elapsed: 0.480 s % 41.31/6.59 % (3600408)Peak memory usage: 94 MB % 41.31/6.59 % (3600408)Instructions burned: 835 (million) % 41.31/6.59 % (3600410)Instruction limit reached! % 41.31/6.59 % (3600410)------------------------------ % 41.31/6.59 % (3600410)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 41.31/6.59 % (3600410)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.31/6.59 % (3600410)CaDiCaL version: 2.1.3 % 41.31/6.59 % (3600410)Termination reason: Instruction limit % 41.31/6.59 % (3600410)Termination phase: Saturation % 41.31/6.59 % (3600410)Time elapsed: 0.445 s % 41.31/6.59 % (3600410)Peak memory usage: 121 MB % 41.31/6.59 % (3600410)Instructions burned: 778 (million) % 41.31/6.59 % (3600422)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=1199146454:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2956 on theBenchmark for (2956ds/775Mi) % 41.31/6.59 % (3600422)Refutation not found, incomplete strategy % 41.31/6.59 % (3600422)------------------------------ % 41.31/6.59 % (3600422)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 41.31/6.59 % (3600422)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.31/6.59 % (3600422)CaDiCaL version: 2.1.3 % 41.31/6.59 % (3600422)Termination reason: Refutation not found, incomplete strategy % 41.31/6.59 % (3600422)Time elapsed: 0.001 s % 41.31/6.59 % (3600422)Peak memory usage: 88 MB % 41.31/6.59 % (3600422)Instructions burned: 2 (million) % 41.31/6.59 % (3600411)Instruction limit reached! % 41.31/6.59 % (3600411)------------------------------ % 41.31/6.59 % (3600411)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 41.31/6.59 % (3600411)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.31/6.59 % (3600411)CaDiCaL version: 2.1.3 % 41.31/6.59 % (3600411)Termination reason: Instruction limit % 41.31/6.59 % (3600411)Termination phase: Saturation % 41.31/6.59 % (3600411)Time elapsed: 0.474 s % 41.31/6.59 % (3600411)Peak memory usage: 139 MB % 41.31/6.59 % (3600411)Instructions burned: 648 (million) % 41.31/6.59 % (3600423)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=1717589319:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2956 on theBenchmark for (2956ds/273Mi) % 41.31/6.59 % (3600422)------------------------------ % 41.31/6.59 % (3600422)------------------------------ % 41.31/6.59 % (3600425)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=1346393073:i=102:nm=16:rtra=on_2955 on theBenchmark for (2955ds/102Mi) % 41.31/6.59 % (3600426)lrs+10_1_to=lpo:sil=128000:si=on:bsr=unit_only:tha=off:random_seed=3848995513:avsq=on:s2a=on:i=1094:s2at=5:avsqr=4463,131072:rtra=on_2954 on theBenchmark for (2954ds/1094Mi) % 41.31/6.59 % (3600425)Instruction limit reached! % 41.31/6.59 % (3600425)------------------------------ % 41.31/6.59 % (3600425)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 41.31/6.59 % (3600425)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.31/6.59 % (3600425)CaDiCaL version: 2.1.3 % 41.31/6.59 % (3600425)Termination reason: Instruction limit % 41.31/6.59 % (3600425)Termination phase: Saturation % 41.31/6.59 % (3600425)Time elapsed: 0.062 s % 41.31/6.59 % (3600425)Peak memory usage: 89 MB % 41.31/6.59 % (3600425)Instructions burned: 102 (million) % 41.31/6.59 % (3600415)Instruction limit reached! % 41.31/6.59 % (3600415)------------------------------ % 41.31/6.59 % (3600415)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 41.31/6.59 % (3600415)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.31/6.59 % (3600415)CaDiCaL version: 2.1.3 % 41.31/6.59 % (3600415)Termination reason: Instruction limit % 53.25/8.17 % (3600415)Termination phase: Saturation % 53.25/8.17 % (3600415)Time elapsed: 0.540 s % 53.25/8.17 % (3600415)Peak memory usage: 122 MB % 53.25/8.17 % (3600415)Instructions burned: 785 (million) % 53.25/8.17 % (3600428)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=707217536:i=6400:doe=on:fsr=off:rtra=on_2953 on theBenchmark for (2953ds/6400Mi) % 53.25/8.17 % (3600423)Instruction limit reached! % 53.25/8.17 % (3600423)------------------------------ % 53.25/8.17 % (3600423)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 53.25/8.17 % (3600423)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.25/8.17 % (3600423)CaDiCaL version: 2.1.3 % 53.25/8.17 % (3600423)Termination reason: Instruction limit % 53.25/8.17 % (3600423)Termination phase: Saturation % 53.25/8.17 % (3600423)Time elapsed: 0.185 s % 53.25/8.17 % (3600423)Peak memory usage: 92 MB % 53.25/8.17 % (3600423)Instructions burned: 274 (million) % 53.25/8.17 % (3600431)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=1826904426:i=868:doe=on:nm=0:rtra=on:gtg=exists_sym_2953 on theBenchmark for (2953ds/868Mi) % 53.25/8.17 % (3600432)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=1457826671:i=1846:canc=cautious:fsr=off:rtra=on_2952 on theBenchmark for (2952ds/1846Mi) % 53.25/8.17 % (3600432)Refutation not found, incomplete strategy % 53.25/8.17 % (3600432)------------------------------ % 53.25/8.17 % (3600432)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 53.25/8.17 % (3600432)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.25/8.17 % (3600432)CaDiCaL version: 2.1.3 % 53.25/8.17 % (3600432)Termination reason: Refutation not found, incomplete strategy % 53.25/8.17 % (3600432)Time elapsed: 0.004 s % 53.25/8.17 % (3600432)Peak memory usage: 89 MB % 53.25/8.17 % (3600432)Instructions burned: 6 (million) % 53.25/8.17 % (3600416)Instruction limit reached! % 53.25/8.17 % (3600416)------------------------------ % 53.25/8.17 % (3600416)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 53.25/8.17 % (3600416)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.25/8.17 % (3600416)CaDiCaL version: 2.1.3 % 53.25/8.17 % (3600416)Termination reason: Instruction limit % 53.25/8.17 % (3600416)Termination phase: Saturation % 53.25/8.17 % (3600416)Time elapsed: 0.705 s % 53.25/8.17 % (3600416)Peak memory usage: 126 MB % 53.25/8.17 % (3600416)Instructions burned: 1132 (million) % 53.25/8.17 % (3600385)Instruction limit reached! % 53.25/8.17 % (3600385)------------------------------ % 53.25/8.17 % (3600385)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 53.25/8.17 % (3600385)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.25/8.17 % (3600385)CaDiCaL version: 2.1.3 % 53.25/8.17 % (3600385)Termination reason: Instruction limit % 53.25/8.17 % (3600385)Termination phase: Saturation % 53.25/8.17 % (3600385)Time elapsed: 1.723 s % 53.25/8.17 % (3600385)Peak memory usage: 101 MB % 53.25/8.17 % (3600385)Instructions burned: 4428 (million) % 53.25/8.17 % (3600434)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=3494976305:s2a=on:i=36816:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2952 on theBenchmark for (2952ds/36816Mi) % 53.25/8.17 % (3600437)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=4053128179:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2951 on theBenchmark for (2951ds/273Mi) % 53.25/8.17 % (3600439)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=3732794250:i=863:doe=on:nm=0:rtra=on:gtg=exists_sym_2950 on theBenchmark for (2950ds/863Mi) % 53.25/8.17 % (3600432)------------------------------ % 53.25/8.17 % (3600432)------------------------------ % 53.25/8.17 % (3600426)Instruction limit reached! % 53.25/8.17 % (3600426)------------------------------ % 53.25/8.17 % (3600426)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 53.25/8.17 % (3600426)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.25/8.17 % (3600426)CaDiCaL version: 2.1.3 % 53.25/8.17 % (3600426)Termination reason: Instruction limit % 53.25/8.17 % (3600426)Termination phase: Saturation % 53.25/8.17 % (3600426)Time elapsed: 0.482 s % 53.25/8.17 % (3600426)Peak memory usage: 91 MB % 53.25/8.17 % (3600426)Instructions burned: 1096 (million) % 53.25/8.17 % (3600437)Instruction limit reached! % 56.54/8.79 % (3600437)------------------------------ % 56.54/8.79 % (3600437)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 56.54/8.79 % (3600437)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.54/8.79 % (3600437)CaDiCaL version: 2.1.3 % 56.54/8.79 % (3600437)Termination reason: Instruction limit % 56.54/8.79 % (3600437)Termination phase: Saturation % 56.54/8.79 % (3600437)Time elapsed: 0.171 s % 56.54/8.79 % (3600437)Peak memory usage: 91 MB % 56.54/8.79 % (3600437)Instructions burned: 273 (million) % 56.54/8.79 % (3600442)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=4148483462:i=5811:kws=precedence:nm=0:rtra=on_2948 on theBenchmark for (2948ds/5811Mi) % 56.54/8.79 % (3600443)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=1257659950:i=2216:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2948 on theBenchmark for (2948ds/2216Mi) % 56.54/8.79 % (3600431)Instruction limit reached! % 56.54/8.79 % (3600431)------------------------------ % 56.54/8.79 % (3600431)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 56.54/8.79 % (3600431)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.54/8.79 % (3600431)CaDiCaL version: 2.1.3 % 56.54/8.79 % (3600431)Termination reason: Instruction limit % 56.54/8.79 % (3600431)Termination phase: Saturation % 56.54/8.79 % (3600431)Time elapsed: 0.521 s % 56.54/8.79 % (3600431)Peak memory usage: 122 MB % 56.54/8.79 % (3600431)Instructions burned: 868 (million) % 56.54/8.79 % (3600444)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=3198169296:i=801:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2947 on theBenchmark for (2947ds/801Mi) % 56.54/8.79 % (3600447)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=3566272107:st=5:i=1026:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2946 on theBenchmark for (2946ds/1026Mi) % 56.54/8.79 % (3600447)Refutation not found, incomplete strategy % 56.54/8.79 % (3600447)------------------------------ % 56.54/8.79 % (3600447)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 56.54/8.79 % (3600447)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.54/8.79 % (3600447)CaDiCaL version: 2.1.3 % 56.54/8.79 % (3600447)Termination reason: Refutation not found, incomplete strategy % 56.54/8.79 % (3600447)Time elapsed: 0.001 s % 56.54/8.79 % (3600447)Peak memory usage: 87 MB % 56.54/8.79 % (3600447)Instructions burned: 1 (million) % 56.54/8.79 % (3600439)Instruction limit reached! % 56.54/8.79 % (3600439)------------------------------ % 56.54/8.79 % (3600439)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 56.54/8.79 % (3600439)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.54/8.79 % (3600439)CaDiCaL version: 2.1.3 % 56.54/8.79 % (3600439)Termination reason: Instruction limit % 56.54/8.79 % (3600439)Termination phase: Saturation % 56.54/8.79 % (3600439)Time elapsed: 0.523 s % 56.54/8.79 % (3600439)Peak memory usage: 121 MB % 56.54/8.79 % (3600439)Instructions burned: 864 (million) % 56.54/8.79 % (3600450)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=933817200:i=3509:rtra=on_2943 on theBenchmark for (2943ds/3509Mi) % 56.54/8.79 % (3600447)------------------------------ % 56.54/8.79 % (3600447)------------------------------ % 56.54/8.79 % (3600444)Instruction limit reached! % 56.54/8.79 % (3600444)------------------------------ % 56.54/8.79 % (3600444)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 56.54/8.79 % (3600444)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.54/8.79 % (3600444)CaDiCaL version: 2.1.3 % 56.54/8.79 % (3600444)Termination reason: Instruction limit % 56.54/8.79 % (3600444)Termination phase: Saturation % 56.54/8.79 % (3600444)Time elapsed: 0.380 s % 56.54/8.79 % (3600444)Peak memory usage: 94 MB % 56.54/8.79 % (3600444)Instructions burned: 801 (million) % 56.54/8.79 % (3600452)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=2458317156:st=2:i=2127:sd=12:ep=R:rtra=on:ss=axioms_2942 on theBenchmark for (2942ds/2127Mi) % 56.54/8.79 % (3600453)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=2879272493:i=1959:rtra=on:fsd=on:proc=on_2942 on theBenchmark for (2942ds/1959Mi) % 56.54/8.79 % (3600452)Refutation not found, incomplete strategy % 56.54/8.79 % (3600452)------------------------------ % 56.54/8.79 % (3600452)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 74.83/11.22 % (3600452)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.83/11.22 % (3600452)CaDiCaL version: 2.1.3 % 74.83/11.22 % (3600452)Termination reason: Refutation not found, incomplete strategy % 74.83/11.22 % (3600452)Time elapsed: 0.002 s % 74.83/11.22 % (3600452)Peak memory usage: 88 MB % 74.83/11.22 % (3600452)Instructions burned: 2 (million) % 74.83/11.22 % (3600428)Instruction limit reached! % 74.83/11.22 % (3600428)------------------------------ % 74.83/11.22 % (3600428)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 74.83/11.22 % (3600428)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.83/11.22 % (3600428)CaDiCaL version: 2.1.3 % 74.83/11.22 % (3600428)Termination reason: Instruction limit % 74.83/11.22 % (3600428)Termination phase: Saturation % 74.83/11.22 % (3600428)Time elapsed: 1.353 s % 74.83/11.22 % (3600428)Peak memory usage: 105 MB % 74.83/11.22 % (3600428)Instructions burned: 6403 (million) % 74.83/11.22 % (3600452)------------------------------ % 74.83/11.22 % (3600452)------------------------------ % 74.83/11.22 % (3600456)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=3932510324:s2a=on:i=3553:nm=0:rtra=on_2939 on theBenchmark for (2939ds/3553Mi) % 74.83/11.23 % (3600457)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=1297405482:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2938 on theBenchmark for (2938ds/3201Mi) % 74.83/11.23 % (3600443)Instruction limit reached! % 74.83/11.23 % (3600443)------------------------------ % 74.83/11.23 % (3600443)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 74.83/11.23 % (3600443)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.83/11.23 % (3600443)CaDiCaL version: 2.1.3 % 74.83/11.23 % (3600443)Termination reason: Instruction limit % 74.83/11.23 % (3600443)Termination phase: Saturation % 74.83/11.23 % (3600443)Time elapsed: 1.278 s % 74.83/11.23 % (3600443)Peak memory usage: 130 MB % 74.83/11.23 % (3600443)Instructions burned: 2218 (million) % 74.83/11.23 % (3600460)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=1833859923:thitd=on:cond=on:i=4093:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2933 on theBenchmark for (2933ds/4093Mi) % 74.83/11.23 % (3600453)Instruction limit reached! % 74.83/11.23 % (3600453)------------------------------ % 74.83/11.23 % (3600453)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 74.83/11.23 % (3600453)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.83/11.23 % (3600453)CaDiCaL version: 2.1.3 % 74.83/11.23 % (3600453)Termination reason: Instruction limit % 74.83/11.23 % (3600453)Termination phase: Saturation % 74.83/11.23 % (3600453)Time elapsed: 1.108 s % 74.83/11.23 % (3600453)Peak memory usage: 135 MB % 74.83/11.23 % (3600453)Instructions burned: 1961 (million) % 74.83/11.23 % (3600462)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=1341353767:cond=fast:i=21173:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2929 on theBenchmark for (2929ds/21173Mi) % 74.83/11.23 % (3600462)Refutation not found, incomplete strategy % 74.83/11.23 % (3600462)------------------------------ % 74.83/11.23 % (3600462)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 74.83/11.23 % (3600462)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.83/11.23 % (3600462)CaDiCaL version: 2.1.3 % 74.83/11.23 % (3600462)Termination reason: Refutation not found, incomplete strategy % 74.83/11.23 % (3600462)Time elapsed: 0.026 s % 74.83/11.23 % (3600462)Peak memory usage: 112 MB % 74.83/11.23 % (3600462)Instructions burned: 6 (million) % 74.83/11.23 % (3600462)------------------------------ % 74.83/11.23 % (3600462)------------------------------ % 74.83/11.23 % (3600456)Instruction limit reached! % 74.83/11.23 % (3600456)------------------------------ % 74.83/11.23 % (3600456)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 74.83/11.23 % (3600456)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.83/11.23 % (3600456)CaDiCaL version: 2.1.3 % 74.83/11.23 % (3600456)Termination reason: Instruction limit % 74.83/11.23 % (3600456)Termination phase: Saturation % 74.83/11.23 % (3600456)Time elapsed: 1.268 s % 74.83/11.23 % (3600456)Peak memory usage: 111 MB % 74.83/11.23 % (3600456)Instructions burned: 3555 (million) % 74.83/11.23 % (3600450)Instruction limit reached! % 74.83/11.23 % (3600450)------------------------------ % 93.69/13.98 % (3600450)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 93.69/13.98 % (3600450)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 93.69/13.98 % (3600450)CaDiCaL version: 2.1.3 % 93.69/13.98 % (3600450)Termination reason: Instruction limit % 93.69/13.98 % (3600450)Termination phase: Saturation % 93.69/13.98 % (3600450)Time elapsed: 1.741 s % 93.69/13.98 % (3600450)Peak memory usage: 105 MB % 93.69/13.98 % (3600450)Instructions burned: 3513 (million) % 93.69/13.98 % (3600465)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=3897239109:avsq=on:i=1262:avsqr=1,16:rtra=on:rawr=on_2925 on theBenchmark for (2925ds/1262Mi) % 93.69/13.98 % (3600464)lrs+11_1_to=lpo:thi=all:sas=z3:si=on:fd=off:sac=on:slsq=on:random_seed=3365902978:avsq=on:i=10544:avsqr=17,4:canc=force:rtra=on:gtg=exists_top:er=filter_2925 on theBenchmark for (2925ds/10544Mi) % 93.69/13.98 % (3600457)Instruction limit reached! % 93.69/13.98 % (3600457)------------------------------ % 93.69/13.98 % (3600457)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 93.69/13.98 % (3600457)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 93.69/13.98 % (3600457)CaDiCaL version: 2.1.3 % 93.69/13.98 % (3600457)Termination reason: Instruction limit % 93.69/13.98 % (3600457)Termination phase: Saturation % 93.69/13.98 % (3600457)Time elapsed: 1.311 s % 93.69/13.98 % (3600457)Peak memory usage: 92 MB % 93.69/13.98 % (3600457)Instructions burned: 3203 (million) % 93.69/13.98 % (3600466)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=1310463240:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2924 on theBenchmark for (2924ds/775Mi) % 93.69/13.98 % (3600466)Refutation not found, incomplete strategy % 93.69/13.98 % (3600466)------------------------------ % 93.69/13.98 % (3600466)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 93.69/13.98 % (3600466)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 93.69/13.98 % (3600466)CaDiCaL version: 2.1.3 % 93.69/13.98 % (3600466)Termination reason: Refutation not found, incomplete strategy % 93.69/13.98 % (3600466)Time elapsed: 0.002 s % 93.69/13.98 % (3600466)Peak memory usage: 88 MB % 93.69/13.98 % (3600466)Instructions burned: 2 (million) % 93.69/13.98 % (3600469)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=1183271191:i=270:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2923 on theBenchmark for (2923ds/270Mi) % 93.69/13.98 % (3600466)------------------------------ % 93.69/13.98 % (3600466)------------------------------ % 93.69/13.98 % (3600469)Instruction limit reached! % 93.69/13.98 % (3600469)------------------------------ % 93.69/13.98 % (3600469)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 93.69/13.98 % (3600469)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 93.69/13.98 % (3600469)CaDiCaL version: 2.1.3 % 93.69/13.98 % (3600469)Termination reason: Instruction limit % 93.69/13.98 % (3600469)Termination phase: Saturation % 93.69/13.98 % (3600469)Time elapsed: 0.173 s % 93.69/13.98 % (3600469)Peak memory usage: 91 MB % 93.69/13.98 % (3600469)Instructions burned: 271 (million) % 93.69/13.98 % (3600465)Instruction limit reached! % 93.69/13.98 % (3600465)------------------------------ % 93.69/13.98 % (3600465)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 93.69/13.98 % (3600465)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 93.69/13.98 % (3600465)CaDiCaL version: 2.1.3 % 93.69/13.98 % (3600465)Termination reason: Instruction limit % 93.69/13.98 % (3600465)Termination phase: Saturation % 93.69/13.98 % (3600465)Time elapsed: 0.413 s % 93.69/13.98 % (3600465)Peak memory usage: 128 MB % 93.69/13.98 % (3600465)Instructions burned: 1263 (million) % 93.69/13.98 % (3600472)ott+10_128_isp=bottom:to=lpo:sil=128000:si=on:urr=on:uwa=alasca_main:sac=on:slsq=on:random_seed=2482781453:i=17165:aac=none:doe=on:rtra=on:gtg=exists_all_2920 on theBenchmark for (2920ds/17165Mi) % 93.69/13.98 % (3600474)lrs+10_1_to=lpo:sil=128000:si=on:sp=occurrence:random_seed=1120006220:st=2:i=12633:rtra=on:ss=axioms_2919 on theBenchmark for (2919ds/12633Mi) % 93.69/13.98 % (3600474)Refutation not found, incomplete strategy % 93.69/13.98 % (3600474)------------------------------ % 93.69/13.98 % (3600474)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 93.69/13.98 % (3600474)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 93.69/13.98 % (3600474)CaDiCaL version: 2.1.3 % 113.07/16.67 % (3600474)Termination reason: Refutation not found, incomplete strategy % 113.07/16.67 % (3600474)Time elapsed: 0.001 s % 113.07/16.67 % (3600474)Peak memory usage: 88 MB % 113.07/16.67 % (3600474)Instructions burned: 2 (million) % 113.07/16.67 % (3600473)lrs+2_10_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_main:tha=some:random_seed=97357052:s2a=on:i=13094:s2at=-1:rtra=on_2920 on theBenchmark for (2920ds/13094Mi) % 113.07/16.67 % (3600474)------------------------------ % 113.07/16.67 % (3600474)------------------------------ % 113.07/16.67 % (3600478)dis+1011_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_frequency:lsd=20:nwc=3:random_seed=3207233615:i=1783:rtra=on:gtg=position_2917 on theBenchmark for (2917ds/1783Mi) % 113.07/16.67 % (3600442)Instruction limit reached! % 113.07/16.67 % (3600442)------------------------------ % 113.07/16.67 % (3600442)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 113.07/16.67 % (3600442)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.07/16.67 % (3600442)CaDiCaL version: 2.1.3 % 113.07/16.67 % (3600442)Termination reason: Instruction limit % 113.07/16.67 % (3600442)Termination phase: Saturation % 113.07/16.67 % (3600442)Time elapsed: 3.187 s % 113.07/16.67 % (3600442)Peak memory usage: 136 MB % 113.07/16.67 % (3600442)Instructions burned: 5815 (million) % 113.07/16.67 % (3600480)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=3075589308:i=5451:aac=none:doe=on:nm=0:rtra=on:amm=off:gtg=position_2915 on theBenchmark for (2915ds/5451Mi) % 113.07/16.67 % (3600478)Instruction limit reached! % 113.07/16.67 % (3600478)------------------------------ % 113.07/16.67 % (3600478)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 113.07/16.67 % (3600478)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.07/16.67 % (3600478)CaDiCaL version: 2.1.3 % 113.07/16.67 % (3600478)Termination reason: Instruction limit % 113.07/16.67 % (3600478)Termination phase: Saturation % 113.07/16.67 % (3600478)Time elapsed: 0.584 s % 113.07/16.67 % (3600478)Peak memory usage: 124 MB % 113.07/16.67 % (3600478)Instructions burned: 1787 (million) % 113.07/16.67 % (3600460)Instruction limit reached! % 113.07/16.67 % (3600460)------------------------------ % 113.07/16.67 % (3600460)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 113.07/16.67 % (3600460)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.07/16.67 % (3600460)CaDiCaL version: 2.1.3 % 113.07/16.67 % (3600460)Termination reason: Instruction limit % 113.07/16.67 % (3600460)Termination phase: Saturation % 113.07/16.67 % (3600460)Time elapsed: 2.295 s % 113.07/16.67 % (3600460)Peak memory usage: 152 MB % 113.07/16.67 % (3600460)Instructions burned: 4093 (million) % 113.07/16.67 % (3600482)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=4045118627:i=4975:doe=on:nm=0:rtra=on:gtg=exists_sym_2910 on theBenchmark for (2910ds/4975Mi) % 113.07/16.67 % (3600483)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=301918774:i=2076:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2909 on theBenchmark for (2909ds/2076Mi) % 113.07/16.67 % (3600483)Instruction limit reached! % 113.07/16.67 % (3600483)------------------------------ % 113.07/16.67 % (3600483)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 113.07/16.67 % (3600483)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.07/16.67 % (3600483)CaDiCaL version: 2.1.3 % 113.07/16.67 % (3600483)Termination reason: Instruction limit % 113.07/16.67 % (3600483)Termination phase: Saturation % 113.07/16.67 % (3600483)Time elapsed: 1.097 s % 113.07/16.67 % (3600483)Peak memory usage: 129 MB % 113.07/16.67 % (3600483)Instructions burned: 2077 (million) % 113.07/16.67 % (3600486)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=1757991771:i=5145:rtra=on_2896 on theBenchmark for (2896ds/5145Mi) % 113.07/16.67 % (3600482)Instruction limit reached! % 113.07/16.67 % (3600482)------------------------------ % 113.07/16.67 % (3600482)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 113.07/16.67 % (3600482)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.07/16.67 % (3600482)CaDiCaL version: 2.1.3 % 113.07/16.67 % (3600482)Termination reason: Instruction limit % 113.07/16.67 % (3600482)Termination phase: Saturation % 113.07/16.67 % (3600482)Time elapsed: 1.452 s % 113.07/16.67 % (3600482)Peak memory usage: 140 MB % 113.07/16.67 % (3600482)Instructions burned: 4977 (million) % 270.07/38.64 % (3600488)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=4024728336:i=3509:rtra=on_2894 on theBenchmark for (2894ds/3509Mi) % 270.07/38.64 % (3600488)Instruction limit reached! % 270.07/38.64 % (3600488)------------------------------ % 270.07/38.64 % (3600488)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 270.07/38.64 % (3600488)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 270.07/38.64 % (3600488)CaDiCaL version: 2.1.3 % 270.07/38.64 % (3600488)Termination reason: Instruction limit % 270.07/38.64 % (3600488)Termination phase: Saturation % 270.07/38.64 % (3600488)Time elapsed: 0.910 s % 270.07/38.64 % (3600488)Peak memory usage: 105 MB % 270.07/38.64 % (3600488)Instructions burned: 3514 (million) % 270.07/38.64 % (3600490)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=3906782159:st=2:i=13800:sd=12:ep=R:rtra=on:ss=axioms_2883 on theBenchmark for (2883ds/13800Mi) % 270.07/38.64 % (3600490)Refutation not found, incomplete strategy % 270.07/38.64 % (3600490)------------------------------ % 270.07/38.64 % (3600490)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 270.07/38.64 % (3600490)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 270.07/38.64 % (3600490)CaDiCaL version: 2.1.3 % 270.07/38.64 % (3600490)Termination reason: Refutation not found, incomplete strategy % 270.07/38.64 % (3600490)Time elapsed: 0.001 s % 270.07/38.64 % (3600490)Peak memory usage: 88 MB % 270.07/38.64 % (3600490)Instructions burned: 2 (million) % 270.07/38.64 % (3600480)Instruction limit reached! % 270.07/38.64 % (3600480)------------------------------ % 270.07/38.64 % (3600480)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 270.07/38.64 % (3600480)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 270.07/38.64 % (3600480)CaDiCaL version: 2.1.3 % 270.07/38.64 % (3600480)Termination reason: Instruction limit % 270.07/38.64 % (3600480)Termination phase: Saturation % 270.07/38.64 % (3600480)Time elapsed: 3.225 s % 270.07/38.64 % (3600480)Peak memory usage: 147 MB % 270.07/38.64 % (3600480)Instructions burned: 5451 (million) % 270.07/38.64 % (3600490)------------------------------ % 270.07/38.64 % (3600490)------------------------------ % 270.07/38.64 % (3600493)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 % 270.07/38.64 % (3600493)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=299180520:i=11747:aac=none:nm=0:rtra=on:rawr=on_2881 on theBenchmark for (2881ds/11747Mi) % 270.07/38.64 % (3600492)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=4066533438:i=1412:rtra=on:fsd=on:proc=on_2881 on theBenchmark for (2881ds/1412Mi) % 270.07/38.64 % (3600492)Instruction limit reached! % 270.07/38.64 % (3600492)------------------------------ % 270.07/38.64 % (3600492)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 270.07/38.64 % (3600492)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 270.07/38.64 % (3600492)CaDiCaL version: 2.1.3 % 270.07/38.64 % (3600492)Termination reason: Instruction limit % 270.07/38.64 % (3600492)Termination phase: Saturation % 270.07/38.64 % (3600492)Time elapsed: 0.824 s % 270.07/38.64 % (3600492)Peak memory usage: 130 MB % 270.07/38.64 % (3600492)Instructions burned: 1413 (million) % 270.07/38.65 % (3600496)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=4213386080:s2a=on:i=3553:nm=0:rtra=on_2871 on theBenchmark for (2871ds/3553Mi) % 270.07/38.65 % (3600473)Instruction limit reached! % 270.07/38.65 % (3600473)------------------------------ % 270.07/38.65 % (3600473)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 270.07/38.65 % (3600473)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 270.07/38.65 % (3600473)CaDiCaL version: 2.1.3 % 270.07/38.65 % (3600473)Termination reason: Instruction limit % 270.07/38.65 % (3600473)Termination phase: Saturation % 270.07/38.65 % (3600473)Time elapsed: 5.005 s % 270.07/38.65 % (3600473)Peak memory usage: 112 MB % 270.07/38.65 % (3600473)Instructions burned: 13097 (million) % 270.07/38.65 % (3600498)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=4052253665:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2868 on theBenchmark for (2868ds/3201Mi) % 270.07/38.65 % (3600486)Instruction limit reached! % 270.07/38.65 % (3600486)------------------------------ % 270.07/38.65 % (3600486)Version: VampTerminated %------------------------------------------------------------------------------