%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWC474_1 : TPTP v9.3.1. Released v9.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 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:06:03 PM UTC 2026 % Result : Timeout 289.86s 41.12s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWC474_1 : TPTP v9.3.1. Released v9.0.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.10/0.23 % Computer : n017.cluster.edu % 0.10/0.23 % Model : x86_64 x86_64 % 0.10/0.23 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.23 % Memory : 8046.5625MB % 0.10/0.23 % OS : Linux 6.8.0-71-generic % 0.10/0.23 % CPULimit : 300 % 0.10/0.23 % WCLimit : 300 % 0.10/0.23 % DateTime : Mon Sep 28 09:35:20 UTC 2026 % 0.10/0.23 % CPUTime : % 0.10/0.23 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.26/0.28 Running first-order model finding % 0.26/0.28 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 5.43/1.05 % (3431903)Will run a generic schedule for satisfiability detection. % 5.43/1.05 % (3431911)dis+10_1_sil=32000:sp=arity:random_seed=3118250618:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 5.43/1.05 % (3431912)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2121213004:i=116_2999 on theBenchmark for (2999ds/116Mi) % 5.43/1.05 % (3431909)% WARNING: option uhcvi not known. % 5.43/1.05 % (3431908)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=4089236901_2999 on theBenchmark for (2999ds/0Mi) % 5.43/1.05 % (3431913)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2671603855:i=131_2999 on theBenchmark for (2999ds/131Mi) % 5.43/1.05 % (3431910)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1222955829:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 5.43/1.05 % (3431909)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3777858758:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 5.43/1.05 % (3431914)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2069566121:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 5.43/1.05 % (3431908)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 5.43/1.05 % (3431908)Terminated due to inappropriate strategy. % 5.43/1.05 % (3431908)------------------------------ % 5.43/1.05 % (3431908)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.43/1.05 % (3431908)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.43/1.05 % (3431908)CaDiCaL version: 2.1.3 % 5.43/1.05 % (3431908)Termination reason: Inappropriate % 5.43/1.05 % (3431908)Time elapsed: 0.002 s % 5.43/1.05 % (3431908)Peak memory usage: 10 MB % 5.43/1.05 % (3431908)Instructions burned: 1 (million) % 5.43/1.05 % (3431908)------------------------------ % 5.43/1.05 % (3431908)------------------------------ % 5.43/1.05 % (3431922)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2780531945:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 5.43/1.05 % (3431922)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 5.43/1.05 % (3431922)Terminated due to inappropriate strategy. % 5.43/1.05 % (3431922)------------------------------ % 5.43/1.05 % (3431922)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.43/1.05 % (3431922)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.43/1.05 % (3431922)CaDiCaL version: 2.1.3 % 5.43/1.05 % (3431922)Termination reason: Inappropriate % 5.43/1.05 % (3431922)Time elapsed: 0.002 s % 5.43/1.05 % (3431922)Peak memory usage: 10 MB % 5.43/1.05 % (3431922)Instructions burned: 1 (million) % 5.43/1.05 % (3431922)------------------------------ % 5.43/1.05 % (3431922)------------------------------ % 5.43/1.05 % (3431911)Instruction limit reached! % 5.43/1.05 % (3431911)------------------------------ % 5.43/1.05 % (3431911)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.43/1.05 % (3431911)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.43/1.05 % (3431911)CaDiCaL version: 2.1.3 % 5.43/1.05 % (3431911)Termination reason: Instruction limit % 5.43/1.05 % (3431911)Termination phase: Saturation % 5.43/1.05 % (3431911)Time elapsed: 0.055 s % 5.43/1.05 % (3431911)Peak memory usage: 12 MB % 5.43/1.05 % (3431911)Instructions burned: 104 (million) % 5.43/1.05 % (3431924)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2408668883:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 5.43/1.05 % (3431925)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=3019796868:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 5.43/1.05 % (3431912)Instruction limit reached! % 5.43/1.05 % (3431912)------------------------------ % 5.43/1.05 % (3431912)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.43/1.05 % (3431912)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.43/1.05 % (3431912)CaDiCaL version: 2.1.3 % 5.43/1.05 % (3431912)Termination reason: Instruction limit % 5.43/1.05 % (3431912)Termination phase: Saturation % 5.43/1.05 % (3431912)Time elapsed: 0.113 s % 5.43/1.05 % (3431912)Peak memory usage: 12 MB % 5.43/1.05 % (3431912)Instructions burned: 116 (million) % 5.43/1.05 % (3431913)Instruction limit reached! % 5.43/1.05 % (3431913)------------------------------ % 5.43/1.05 % (3431913)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.66/1.61 % (3431913)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.66/1.61 % (3431913)CaDiCaL version: 2.1.3 % 7.66/1.61 % (3431913)Termination reason: Instruction limit % 7.66/1.61 % (3431913)Termination phase: Saturation % 7.66/1.61 % (3431913)Time elapsed: 0.132 s % 7.66/1.61 % (3431913)Peak memory usage: 13 MB % 7.66/1.61 % (3431913)Instructions burned: 131 (million) % 7.66/1.61 % (3431928)ott-21_1_sil=16000:fs=off:random_seed=3633989275:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 7.66/1.61 % (3431924)Instruction limit reached! % 7.66/1.61 % (3431924)------------------------------ % 7.66/1.61 % (3431924)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.66/1.61 % (3431924)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.66/1.61 % (3431924)CaDiCaL version: 2.1.3 % 7.66/1.61 % (3431924)Termination reason: Instruction limit % 7.66/1.61 % (3431924)Termination phase: Saturation % 7.66/1.61 % (3431924)Time elapsed: 0.075 s % 7.66/1.61 % (3431924)Peak memory usage: 12 MB % 7.66/1.61 % (3431924)Instructions burned: 133 (million) % 7.66/1.61 % (3431931)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2360202885:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 7.66/1.61 % (3431931)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 7.66/1.61 % (3431931)Terminated due to inappropriate strategy. % 7.66/1.61 % (3431931)------------------------------ % 7.66/1.61 % (3431931)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.66/1.61 % (3431931)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.66/1.61 % (3431931)CaDiCaL version: 2.1.3 % 7.66/1.61 % (3431931)Termination reason: Inappropriate % 7.66/1.61 % (3431931)Time elapsed: 0.001 s % 7.66/1.61 % (3431931)Peak memory usage: 10 MB % 7.66/1.61 % (3431931)Instructions burned: 1 (million) % 7.66/1.61 % (3431931)------------------------------ % 7.66/1.61 % (3431931)------------------------------ % 7.66/1.61 % (3431929)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3633450099:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 7.66/1.61 % (3431933)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=857685444:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 7.66/1.61 % (3431914)Instruction limit reached! % 7.66/1.61 % (3431914)------------------------------ % 7.66/1.61 % (3431914)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.66/1.61 % (3431914)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.66/1.61 % (3431914)CaDiCaL version: 2.1.3 % 7.66/1.61 % (3431914)Termination reason: Instruction limit % 7.66/1.61 % (3431914)Termination phase: Saturation % 7.66/1.61 % (3431914)Time elapsed: 0.178 s % 7.66/1.61 % (3431914)Peak memory usage: 13 MB % 7.66/1.61 % (3431914)Instructions burned: 159 (million) % 7.66/1.61 % (3431936)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1776926506:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi) % 7.66/1.61 % (3431936)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 7.66/1.61 % (3431936)Terminated due to inappropriate strategy. % 7.66/1.61 % (3431936)------------------------------ % 7.66/1.61 % (3431936)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.66/1.61 % (3431936)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.66/1.61 % (3431936)CaDiCaL version: 2.1.3 % 7.66/1.61 % (3431936)Termination reason: Inappropriate % 7.66/1.61 % (3431936)Time elapsed: 0.001 s % 7.66/1.61 % (3431936)Peak memory usage: 11 MB % 7.66/1.61 % (3431936)Instructions burned: 1 (million) % 7.66/1.61 % (3431936)------------------------------ % 7.66/1.61 % (3431936)------------------------------ % 7.66/1.61 % (3431938)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=3205649260:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2997 on theBenchmark for (2997ds/692Mi) % 7.66/1.61 % (3431928)Instruction limit reached! % 7.66/1.61 % (3431928)------------------------------ % 7.66/1.61 % (3431928)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.66/1.61 % (3431928)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.66/1.61 % (3431928)CaDiCaL version: 2.1.3 % 7.66/1.61 % (3431928)Termination reason: Instruction limit % 7.66/1.61 % (3431928)Termination phase: Saturation % 32.15/4.89 % (3431928)Time elapsed: 0.150 s % 32.15/4.89 % (3431928)Peak memory usage: 12 MB % 32.15/4.89 % (3431928)Instructions burned: 180 (million) % 32.15/4.89 % (3431940)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=558415440:i=879:kws=inv_precedence:fsr=off_2996 on theBenchmark for (2996ds/879Mi) % 32.15/4.89 % (3431938)Instruction limit reached! % 32.15/4.89 % (3431938)------------------------------ % 32.15/4.89 % (3431938)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 32.15/4.89 % (3431938)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.15/4.89 % (3431938)CaDiCaL version: 2.1.3 % 32.15/4.89 % (3431938)Termination reason: Instruction limit % 32.15/4.89 % (3431938)Termination phase: Saturation % 32.15/4.89 % (3431938)Time elapsed: 0.383 s % 32.15/4.89 % (3431938)Peak memory usage: 17 MB % 32.15/4.89 % (3431938)Instructions burned: 692 (million) % 32.15/4.89 % (3431942)fmb+10_1_sil=64000:random_seed=1951218998:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi) % 32.15/4.89 % (3431942)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 32.15/4.89 % (3431942)Terminated due to inappropriate strategy. % 32.15/4.89 % (3431942)------------------------------ % 32.15/4.89 % (3431942)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 32.15/4.89 % (3431942)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.15/4.89 % (3431942)CaDiCaL version: 2.1.3 % 32.15/4.89 % (3431942)Termination reason: Inappropriate % 32.15/4.89 % (3431942)Time elapsed: 0.001 s % 32.15/4.89 % (3431942)Peak memory usage: 11 MB % 32.15/4.89 % (3431942)Instructions burned: 1 (million) % 32.15/4.89 % (3431942)------------------------------ % 32.15/4.89 % (3431942)------------------------------ % 32.15/4.89 % (3431944)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1061087951:i=9515:nm=5_2993 on theBenchmark for (2993ds/9515Mi) % 32.15/4.89 % (3431944)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 32.15/4.89 % (3431944)Terminated due to inappropriate strategy. % 32.15/4.89 % (3431944)------------------------------ % 32.15/4.89 % (3431944)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 32.15/4.89 % (3431944)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.15/4.89 % (3431944)CaDiCaL version: 2.1.3 % 32.15/4.89 % (3431944)Termination reason: Inappropriate % 32.15/4.89 % (3431944)Time elapsed: 0.001 s % 32.15/4.89 % (3431944)Peak memory usage: 10 MB % 32.15/4.89 % (3431944)Instructions burned: 1 (million) % 32.15/4.89 % (3431944)------------------------------ % 32.15/4.89 % (3431944)------------------------------ % 32.15/4.89 % (3431946)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=576834764:fmbsr=1.7:i=920_2993 on theBenchmark for (2993ds/920Mi) % 32.15/4.89 % (3431946)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 32.15/4.89 % (3431946)Terminated due to inappropriate strategy. % 32.15/4.89 % (3431946)------------------------------ % 32.15/4.89 % (3431946)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 32.15/4.89 % (3431946)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.15/4.89 % (3431946)CaDiCaL version: 2.1.3 % 32.15/4.89 % (3431946)Termination reason: Inappropriate % 32.15/4.89 % (3431946)Time elapsed: 0.001 s % 32.15/4.89 % (3431946)Peak memory usage: 10 MB % 32.15/4.89 % (3431946)Instructions burned: 1 (million) % 32.15/4.89 % (3431946)------------------------------ % 32.15/4.89 % (3431946)------------------------------ % 32.15/4.89 % (3431929)Instruction limit reached! % 32.15/4.89 % (3431929)------------------------------ % 32.15/4.89 % (3431929)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 32.15/4.89 % (3431929)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.15/4.89 % (3431929)CaDiCaL version: 2.1.3 % 32.15/4.89 % (3431929)Termination reason: Instruction limit % 32.15/4.89 % (3431929)Termination phase: Saturation % 32.15/4.89 % (3431929)Time elapsed: 0.517 s % 32.15/4.89 % (3431929)Peak memory usage: 14 MB % 32.15/4.89 % (3431929)Instructions burned: 477 (million) % 32.15/4.89 % (3431948)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3964270014:i=5131_2992 on theBenchmark for (2992ds/5131Mi) % 32.15/4.89 % (3431949)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2269753598:i=1472:ins=7:fdi=8:gsp=on_2992 on theBenchmark for (2992ds/1472Mi) % 32.15/4.89 % (3431925)Instruction limit reached! % 32.15/4.89 % (3431925)------------------------------ % 42.86/6.40 % (3431925)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 42.86/6.40 % (3431925)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.86/6.40 % (3431925)CaDiCaL version: 2.1.3 % 42.86/6.40 % (3431925)Termination reason: Instruction limit % 42.86/6.40 % (3431925)Termination phase: Saturation % 42.86/6.40 % (3431925)Time elapsed: 0.650 s % 42.86/6.40 % (3431925)Peak memory usage: 17 MB % 42.86/6.40 % (3431925)Instructions burned: 685 (million) % 42.86/6.40 % (3431952)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3135118139:i=6324_2992 on theBenchmark for (2992ds/6324Mi) % 42.86/6.40 % (3431952)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 42.86/6.40 % (3431952)Terminated due to inappropriate strategy. % 42.86/6.40 % (3431952)------------------------------ % 42.86/6.40 % (3431952)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 42.86/6.40 % (3431952)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.86/6.40 % (3431952)CaDiCaL version: 2.1.3 % 42.86/6.40 % (3431952)Termination reason: Inappropriate % 42.86/6.40 % (3431952)Time elapsed: 0.001 s % 42.86/6.40 % (3431952)Peak memory usage: 10 MB % 42.86/6.40 % (3431952)Instructions burned: 1 (million) % 42.86/6.40 % (3431952)------------------------------ % 42.86/6.40 % (3431952)------------------------------ % 42.86/6.40 % (3431954)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=4016393581:fmbsr=2.30978:i=2174_2992 on theBenchmark for (2992ds/2174Mi) % 42.86/6.40 % (3431954)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 42.86/6.40 % (3431954)Terminated due to inappropriate strategy. % 42.86/6.40 % (3431954)------------------------------ % 42.86/6.40 % (3431954)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 42.86/6.40 % (3431954)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.86/6.40 % (3431954)CaDiCaL version: 2.1.3 % 42.86/6.40 % (3431954)Termination reason: Inappropriate % 42.86/6.40 % (3431954)Time elapsed: 0.001 s % 42.86/6.40 % (3431954)Peak memory usage: 11 MB % 42.86/6.40 % (3431954)Instructions burned: 1 (million) % 42.86/6.40 % (3431954)------------------------------ % 42.86/6.40 % (3431954)------------------------------ % 42.86/6.40 % (3431956)ott-2_1_sil=16000:newcnf=on:random_seed=2064836735:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2991 on theBenchmark for (2991ds/869Mi) % 42.86/6.40 % (3431940)Instruction limit reached! % 42.86/6.40 % (3431940)------------------------------ % 42.86/6.40 % (3431940)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 42.86/6.40 % (3431940)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.86/6.40 % (3431940)CaDiCaL version: 2.1.3 % 42.86/6.40 % (3431940)Termination reason: Instruction limit % 42.86/6.40 % (3431940)Termination phase: Saturation % 42.86/6.40 % (3431940)Time elapsed: 0.844 s % 42.86/6.40 % (3431940)Peak memory usage: 18 MB % 42.86/6.40 % (3431940)Instructions burned: 880 (million) % 42.86/6.40 % (3431958)ott+10_1_sil=32000:tgt=ground:random_seed=2561434784:i=5114:av=off_2988 on theBenchmark for (2988ds/5114Mi) % 42.86/6.40 % (3431933)Instruction limit reached! % 42.86/6.40 % (3431933)------------------------------ % 42.86/6.40 % (3431933)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 42.86/6.40 % (3431933)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.86/6.40 % (3431933)CaDiCaL version: 2.1.3 % 42.86/6.40 % (3431933)Termination reason: Instruction limit % 42.86/6.40 % (3431933)Termination phase: Saturation % 42.86/6.40 % (3431933)Time elapsed: 1.077 s % 42.86/6.40 % (3431933)Peak memory usage: 17 MB % 42.86/6.40 % (3431933)Instructions burned: 1179 (million) % 42.86/6.40 % (3431961)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1371109076:i=54282_2987 on theBenchmark for (2987ds/54282Mi) % 42.86/6.40 % (3431961)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 42.86/6.40 % (3431961)Terminated due to inappropriate strategy. % 42.86/6.40 % (3431961)------------------------------ % 42.86/6.40 % (3431961)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 42.86/6.40 % (3431961)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.86/6.40 % (3431961)CaDiCaL version: 2.1.3 % 42.86/6.40 % (3431961)Termination reason: Inappropriate % 42.86/6.40 % (3431961)Time elapsed: 0.002 s % 42.86/6.40 % (3431961)Peak memory usage: 10 MB % 42.86/6.40 % (3431961)Instructions burned: 1 (million) % 104.84/15.05 % (3431961)------------------------------ % 104.84/15.05 % (3431961)------------------------------ % 104.84/15.05 % (3431963)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1311858416:i=3512:aac=none_2986 on theBenchmark for (2986ds/3512Mi) % 104.84/15.05 % (3431956)Instruction limit reached! % 104.84/15.05 % (3431956)------------------------------ % 104.84/15.05 % (3431956)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 104.84/15.05 % (3431956)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 104.84/15.05 % (3431956)CaDiCaL version: 2.1.3 % 104.84/15.05 % (3431956)Termination reason: Instruction limit % 104.84/15.05 % (3431956)Termination phase: Saturation % 104.84/15.05 % (3431956)Time elapsed: 0.806 s % 104.84/15.05 % (3431956)Peak memory usage: 17 MB % 104.84/15.05 % (3431956)Instructions burned: 870 (million) % 104.84/15.05 % (3431966)dis+21_1_sil=32000:sas=cadical:random_seed=338452897:i=3773:amm=off_2983 on theBenchmark for (2983ds/3773Mi) % 104.84/15.05 % (3431949)Instruction limit reached! % 104.84/15.05 % (3431949)------------------------------ % 104.84/15.05 % (3431949)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 104.84/15.05 % (3431949)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 104.84/15.05 % (3431949)CaDiCaL version: 2.1.3 % 104.84/15.05 % (3431949)Termination reason: Instruction limit % 104.84/15.05 % (3431949)Termination phase: Saturation % 104.84/15.05 % (3431949)Time elapsed: 1.532 s % 104.84/15.05 % (3431949)Peak memory usage: 25 MB % 104.84/15.05 % (3431949)Instructions burned: 1472 (million) % 104.84/15.05 % (3431972)ott+11_1_sil=16000:gs=on:random_seed=4169583553:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2977 on theBenchmark for (2977ds/2251Mi) % 104.84/15.05 % (3431948)Instruction limit reached! % 104.84/15.05 % (3431948)------------------------------ % 104.84/15.05 % (3431948)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 104.84/15.05 % (3431948)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 104.84/15.05 % (3431948)CaDiCaL version: 2.1.3 % 104.84/15.05 % (3431948)Termination reason: Instruction limit % 104.84/15.05 % (3431948)Termination phase: Saturation % 104.84/15.05 % (3431948)Time elapsed: 2.439 s % 104.84/15.05 % (3431948)Peak memory usage: 42 MB % 104.84/15.05 % (3431948)Instructions burned: 5131 (million) % 104.84/15.05 % (3431976)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1272146796:fmbsr=1.6:i=67534_2968 on theBenchmark for (2968ds/67534Mi) % 104.84/15.05 % (3431976)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 104.84/15.05 % (3431976)Terminated due to inappropriate strategy. % 104.84/15.05 % (3431976)------------------------------ % 104.84/15.05 % (3431976)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 104.84/15.05 % (3431976)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 104.84/15.05 % (3431976)CaDiCaL version: 2.1.3 % 104.84/15.05 % (3431976)Termination reason: Inappropriate % 104.84/15.05 % (3431976)Time elapsed: 0.001 s % 104.84/15.05 % (3431976)Peak memory usage: 11 MB % 104.84/15.05 % (3431976)Instructions burned: 1 (million) % 104.84/15.05 % (3431976)------------------------------ % 104.84/15.05 % (3431976)------------------------------ % 104.84/15.05 % (3431978)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3135866703:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2968 on theBenchmark for (2968ds/4591Mi) % 104.84/15.05 % (3431972)Instruction limit reached! % 104.84/15.05 % (3431972)------------------------------ % 104.84/15.05 % (3431972)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 104.84/15.05 % (3431972)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 104.84/15.05 % (3431972)CaDiCaL version: 2.1.3 % 104.84/15.05 % (3431972)Termination reason: Instruction limit % 104.84/15.05 % (3431972)Termination phase: Saturation % 104.84/15.05 % (3431972)Time elapsed: 2.119 s % 104.84/15.05 % (3431972)Peak memory usage: 23 MB % 104.84/15.05 % (3431972)Instructions burned: 2251 (million) % 104.84/15.05 % (3431980)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1509525071:i=29340_2955 on theBenchmark for (2955ds/29340Mi) % 104.84/15.05 % (3431963)Instruction limit reached! % 104.84/15.05 % (3431963)------------------------------ % 104.84/15.05 % (3431963)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 104.84/15.05 % (3431963)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 104.84/15.05 % (3431963)CaDiCaL version: 2.1.3 % 104.84/15.05 % (3431963)Termination reason: Instruction limit % 157.99/22.53 % (3431963)Termination phase: Saturation % 157.99/22.53 % (3431963)Time elapsed: 3.257 s % 157.99/22.53 % (3431963)Peak memory usage: 31 MB % 157.99/22.53 % (3431963)Instructions burned: 3513 (million) % 157.99/22.53 % (3431982)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=161064771:i=5211_2953 on theBenchmark for (2953ds/5211Mi) % 157.99/22.53 % (3431966)Instruction limit reached! % 157.99/22.53 % (3431966)------------------------------ % 157.99/22.53 % (3431966)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 157.99/22.53 % (3431966)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.99/22.53 % (3431966)CaDiCaL version: 2.1.3 % 157.99/22.53 % (3431966)Termination reason: Instruction limit % 157.99/22.53 % (3431966)Termination phase: Saturation % 157.99/22.53 % (3431966)Time elapsed: 3.476 s % 157.99/22.53 % (3431966)Peak memory usage: 31 MB % 157.99/22.53 % (3431966)Instructions burned: 3773 (million) % 157.99/22.53 % (3431984)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=507180727:i=5497:nm=2_2948 on theBenchmark for (2948ds/5497Mi) % 157.99/22.53 % (3431984)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 157.99/22.53 % (3431984)Terminated due to inappropriate strategy. % 157.99/22.53 % (3431984)------------------------------ % 157.99/22.53 % (3431984)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 157.99/22.53 % (3431984)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.99/22.53 % (3431984)CaDiCaL version: 2.1.3 % 157.99/22.53 % (3431984)Termination reason: Inappropriate % 157.99/22.53 % (3431984)Time elapsed: 0.001 s % 157.99/22.53 % (3431984)Peak memory usage: 11 MB % 157.99/22.53 % (3431984)Instructions burned: 1 (million) % 157.99/22.53 % (3431984)------------------------------ % 157.99/22.53 % (3431984)------------------------------ % 157.99/22.53 % (3431986)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1101952475:fmbsr=2:i=46332_2948 on theBenchmark for (2948ds/46332Mi) % 157.99/22.53 % (3431986)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 157.99/22.53 % (3431986)Terminated due to inappropriate strategy. % 157.99/22.53 % (3431986)------------------------------ % 157.99/22.53 % (3431986)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 157.99/22.53 % (3431986)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.99/22.53 % (3431986)CaDiCaL version: 2.1.3 % 157.99/22.53 % (3431986)Termination reason: Inappropriate % 157.99/22.53 % (3431986)Time elapsed: 0.002 s % 157.99/22.53 % (3431986)Peak memory usage: 10 MB % 157.99/22.53 % (3431986)Instructions burned: 1 (million) % 157.99/22.53 % (3431986)------------------------------ % 157.99/22.53 % (3431986)------------------------------ % 157.99/22.53 % (3431988)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=4137396037:i=14071_2947 on theBenchmark for (2947ds/14071Mi) % 157.99/22.53 % (3431988)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 157.99/22.53 % (3431988)Terminated due to inappropriate strategy. % 157.99/22.53 % (3431988)------------------------------ % 157.99/22.53 % (3431988)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 157.99/22.53 % (3431988)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.99/22.53 % (3431988)CaDiCaL version: 2.1.3 % 157.99/22.53 % (3431988)Termination reason: Inappropriate % 157.99/22.53 % (3431988)Time elapsed: 0.002 s % 157.99/22.53 % (3431988)Peak memory usage: 10 MB % 157.99/22.53 % (3431988)Instructions burned: 1 (million) % 157.99/22.53 % (3431988)------------------------------ % 157.99/22.53 % (3431988)------------------------------ % 157.99/22.53 % (3431990)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1031427787:i=22565:add=on:rawr=on_2947 on theBenchmark for (2947ds/22565Mi) % 157.99/22.53 % (3431978)Instruction limit reached! % 157.99/22.53 % (3431978)------------------------------ % 157.99/22.53 % (3431978)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 157.99/22.53 % (3431978)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.99/22.53 % (3431978)CaDiCaL version: 2.1.3 % 157.99/22.53 % (3431978)Termination reason: Instruction limit % 157.99/22.53 % (3431978)Termination phase: Saturation % 157.99/22.53 % (3431978)Time elapsed: 2.166 s % 157.99/22.53 % (3431978)Peak memory usage: 43 MB % 157.99/22.53 % (3431978)Instructions burned: 4593 (million) % 157.99/22.53 % (3431994)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=2209107:i=8173:av=off_2946 on theBenchmark for (2946ds/8173Mi) % 157.99/22.53 % (3431958)Instruction limit reached! % 158.69/22.68 % (3431958)------------------------------ % 158.69/22.68 % (3431958)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.69/22.68 % (3431958)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.69/22.68 % (3431958)CaDiCaL version: 2.1.3 % 158.69/22.68 % (3431958)Termination reason: Instruction limit % 158.69/22.68 % (3431958)Termination phase: Saturation % 158.69/22.68 % (3431958)Time elapsed: 4.896 s % 158.69/22.68 % (3431958)Peak memory usage: 40 MB % 158.69/22.68 % (3431958)Instructions burned: 5116 (million) % 158.69/22.68 % (3432102)dis+10_16:1_sil=16000:random_seed=2270065498:i=9155:fsr=off_2938 on theBenchmark for (2938ds/9155Mi) % 158.69/22.68 % (3431982)Instruction limit reached! % 158.69/22.68 % (3431982)------------------------------ % 158.69/22.68 % (3431982)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.69/22.68 % (3431982)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.69/22.68 % (3431982)CaDiCaL version: 2.1.3 % 158.69/22.68 % (3431982)Termination reason: Instruction limit % 158.69/22.68 % (3431982)Termination phase: Saturation % 158.69/22.68 % (3431982)Time elapsed: 3.119 s % 158.69/22.68 % (3431982)Peak memory usage: 49 MB % 158.69/22.68 % (3431982)Instructions burned: 5211 (million) % 158.69/22.68 % (3432151)ott-3_8_sil=64000:random_seed=2516887020:i=20139:bs=on_2922 on theBenchmark for (2922ds/20139Mi) % 158.69/22.68 % (3431994)Instruction limit reached! % 158.69/22.68 % (3431994)------------------------------ % 158.69/22.68 % (3431994)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.69/22.68 % (3431994)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.69/22.68 % (3431994)CaDiCaL version: 2.1.3 % 158.69/22.68 % (3431994)Termination reason: Instruction limit % 158.69/22.68 % (3431994)Termination phase: Saturation % 158.69/22.68 % (3431994)Time elapsed: 2.756 s % 158.69/22.68 % (3431994)Peak memory usage: 53 MB % 158.69/22.68 % (3431994)Instructions burned: 8174 (million) % 158.69/22.68 % (3432153)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=2563988259:fmbsr=2:i=32576_2918 on theBenchmark for (2918ds/32576Mi) % 158.69/22.68 % (3432153)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 158.69/22.68 % (3432153)Terminated due to inappropriate strategy. % 158.69/22.68 % (3432153)------------------------------ % 158.69/22.68 % (3432153)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.69/22.68 % (3432153)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.69/22.68 % (3432153)CaDiCaL version: 2.1.3 % 158.69/22.68 % (3432153)Termination reason: Inappropriate % 158.69/22.68 % (3432153)Time elapsed: 0.0000 s % 158.69/22.68 % (3432153)Peak memory usage: 10 MB % 158.69/22.68 % (3432153)Instructions burned: 1 (million) % 158.69/22.68 % (3432153)------------------------------ % 158.69/22.68 % (3432153)------------------------------ % 158.69/22.68 % (3432155)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=2930212328:i=11404_2918 on theBenchmark for (2918ds/11404Mi) % 158.69/22.68 % (3432102)Instruction limit reached! % 158.69/22.68 % (3432102)------------------------------ % 158.69/22.68 % (3432102)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.69/22.68 % (3432102)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.69/22.68 % (3432102)CaDiCaL version: 2.1.3 % 158.69/22.68 % (3432102)Termination reason: Instruction limit % 158.69/22.68 % (3432102)Termination phase: Saturation % 158.69/22.68 % (3432102)Time elapsed: 4.658 s % 158.69/22.68 % (3432102)Peak memory usage: 52 MB % 158.69/22.68 % (3432102)Instructions burned: 9157 (million) % 158.69/22.68 % (3432157)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=3592616728:i=14134_2892 on theBenchmark for (2892ds/14134Mi) % 158.69/22.68 % (3432155)Instruction limit reached! % 158.69/22.68 % (3432155)------------------------------ % 158.69/22.68 % (3432155)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.69/22.68 % (3432155)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.69/22.68 % (3432155)CaDiCaL version: 2.1.3 % 158.69/22.68 % (3432155)Termination reason: Instruction limit % 158.69/22.68 % (3432155)Termination phase: Saturation % 158.69/22.68 % (3432155)Time elapsed: 3.840 s % 158.69/22.68 % (3432155)Peak memory usage: 61 MB % 158.69/22.68 % (3432155)Instructions burned: 11405 (million) % 158.69/22.68 % (3432159)dis+33_16_sil=32000:sac=on:random_seed=3729575990:i=15851:nm=0_2879 on theBenchmark for (2879ds/15851Mi) % 158.69/22.68 % (3431990)Instruction limit reached! % 158.69/22.68 % (3431990)------------------------------ % 158.69/22.68 % (3431990)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 229.50/32.65 % (3431990)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 229.50/32.65 % (3431990)CaDiCaL version: 2.1.3 % 229.50/32.65 % (3431990)Termination reason: Instruction limit % 229.50/32.65 % (3431990)Termination phase: Saturation % 229.50/32.65 % (3431990)Time elapsed: 9.450 s % 229.50/32.65 % (3431990)Peak memory usage: 72 MB % 229.50/32.65 % (3431990)Instructions burned: 22566 (million) % 229.50/32.65 % (3432302)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=1683408834:avsq=on:i=17627:add=on:amm=off_2852 on theBenchmark for (2852ds/17627Mi) % 229.50/32.65 % (3432159)Instruction limit reached! % 229.50/32.65 % (3432159)------------------------------ % 229.50/32.65 % (3432159)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 229.50/32.65 % (3432159)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 229.50/32.65 % (3432159)CaDiCaL version: 2.1.3 % 229.50/32.65 % (3432159)Termination reason: Instruction limit % 229.50/32.65 % (3432159)Termination phase: Saturation % 229.50/32.65 % (3432159)Time elapsed: 4.862 s % 229.50/32.65 % (3432159)Peak memory usage: 173 MB % 229.50/32.65 % (3432159)Instructions burned: 15853 (million) % 229.50/32.65 % (3432481)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=3414797377:s2a=on:i=53295_2830 on theBenchmark for (2830ds/53295Mi) % 229.50/32.65 % (3431980)Instruction limit reached! % 229.50/32.65 % (3431980)------------------------------ % 229.50/32.65 % (3431980)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 229.50/32.65 % (3431980)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 229.50/32.65 % (3431980)CaDiCaL version: 2.1.3 % 229.50/32.65 % (3431980)Termination reason: Instruction limit % 229.50/32.65 % (3431980)Termination phase: Saturation % 229.50/32.65 % (3431980)Time elapsed: 13.549 s % 229.50/32.65 % (3431980)Peak memory usage: 116 MB % 229.50/32.65 % (3431980)Instructions burned: 29341 (million) % 229.50/32.65 % (3432487)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=1707487890:i=26857:ins=20_2819 on theBenchmark for (2819ds/26857Mi) % 229.50/32.65 % (3432487)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 229.50/32.65 % (3432487)Terminated due to inappropriate strategy. % 229.50/32.65 % (3432487)------------------------------ % 229.50/32.65 % (3432487)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 229.50/32.65 % (3432487)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 229.50/32.65 % (3432487)CaDiCaL version: 2.1.3 % 229.50/32.65 % (3432487)Termination reason: Inappropriate % 229.50/32.65 % (3432487)Time elapsed: 0.001 s % 229.50/32.65 % (3432487)Peak memory usage: 11 MB % 229.50/32.65 % (3432487)Instructions burned: 1 (million) % 229.50/32.65 % (3432487)------------------------------ % 229.50/32.65 % (3432487)------------------------------ % 229.50/32.65 % (3432489)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=3674795138:i=28120:bs=on:fsr=off_2819 on theBenchmark for (2819ds/28120Mi) % 229.50/32.65 % (3432157)Instruction limit reached! % 229.50/32.65 % (3432157)------------------------------ % 229.50/32.65 % (3432157)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 229.50/32.65 % (3432157)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 229.50/32.65 % (3432157)CaDiCaL version: 2.1.3 % 229.50/32.65 % (3432157)Termination reason: Instruction limit % 229.50/32.65 % (3432157)Termination phase: Saturation % 229.50/32.65 % (3432157)Time elapsed: 11.353 s % 229.50/32.65 % (3432157)Peak memory usage: 72 MB % 229.50/32.65 % (3432157)Instructions burned: 14134 (million) % 229.50/32.65 % (3432509)fmb+10_1_sil=256000:fmbss=7:random_seed=1829439786:fmbsr=1.6:i=182295_2778 on theBenchmark for (2778ds/182295Mi) % 229.50/32.65 % (3432509)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 229.50/32.65 % (3432509)Terminated due to inappropriate strategy. % 229.50/32.65 % (3432509)------------------------------ % 229.50/32.65 % (3432509)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 229.50/32.65 % (3432509)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 229.50/32.65 % (3432509)CaDiCaL version: 2.1.3 % 229.50/32.65 % (3432509)Termination reason: Inappropriate % 229.50/32.65 % (3432509)Time elapsed: 0.001 s % 229.50/32.65 % (3432509)Peak memory usage: 11 MB % 229.50/32.65 % (3432509)Instructions burned: 1 (million) % 229.50/32.65 % (3432509)------------------------------ % 229.50/32.65 % (3432509)------------------------------ % 229.50/32.65 % (3432511)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=1204524329:i=44625:gsp=on_2777 on theBenchmark for (2777ds/44625Mi) % 250.46/35.57 % (3432511)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 250.46/35.57 % (3432511)Terminated due to inappropriate strategy. % 250.46/35.57 % (3432511)------------------------------ % 250.46/35.57 % (3432511)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 250.46/35.57 % (3432511)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 250.46/35.57 % (3432511)CaDiCaL version: 2.1.3 % 250.46/35.57 % (3432511)Termination reason: Inappropriate % 250.46/35.57 % (3432511)Time elapsed: 0.002 s % 250.46/35.57 % (3432511)Peak memory usage: 11 MB % 250.46/35.57 % (3432511)Instructions burned: 1 (million) % 250.46/35.57 % (3432511)------------------------------ % 250.46/35.57 % (3432511)------------------------------ % 250.46/35.57 % (3432513)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=1279305589:i=160505_2777 on theBenchmark for (2777ds/160505Mi) % 250.46/35.57 % (3432513)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 250.46/35.57 % (3432513)Terminated due to inappropriate strategy. % 250.46/35.57 % (3432513)------------------------------ % 250.46/35.57 % (3432513)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 250.46/35.57 % (3432513)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 250.46/35.57 % (3432513)CaDiCaL version: 2.1.3 % 250.46/35.57 % (3432513)Termination reason: Inappropriate % 250.46/35.57 % (3432513)Time elapsed: 0.001 s % 250.46/35.57 % (3432513)Peak memory usage: 11 MB % 250.46/35.57 % (3432513)Instructions burned: 1 (million) % 250.46/35.57 % (3432513)------------------------------ % 250.46/35.57 % (3432513)------------------------------ % 250.46/35.57 % (3432515)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=1609428221:fmbsr=1.3:i=225729_2777 on theBenchmark for (2777ds/225729Mi) % 250.46/35.57 % (3432515)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 250.46/35.57 % (3432515)Terminated due to inappropriate strategy. % 250.46/35.57 % (3432515)------------------------------ % 250.46/35.57 % (3432515)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 250.46/35.57 % (3432515)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 250.46/35.57 % (3432515)CaDiCaL version: 2.1.3 % 250.46/35.57 % (3432515)Termination reason: Inappropriate % 250.46/35.57 % (3432515)Time elapsed: 0.001 s % 250.46/35.57 % (3432515)Peak memory usage: 11 MB % 250.46/35.57 % (3432515)Instructions burned: 1 (million) % 250.46/35.57 % (3432515)------------------------------ % 250.46/35.57 % (3432515)------------------------------ % 250.46/35.57 % (3432517)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=324127826:fmbsr=2:i=185024:ins=7_2777 on theBenchmark for (2777ds/185024Mi) % 250.46/35.57 % (3432517)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 250.46/35.57 % (3432517)Terminated due to inappropriate strategy. % 250.46/35.57 % (3432517)------------------------------ % 250.46/35.57 % (3432517)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 250.46/35.57 % (3432517)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 250.46/35.57 % (3432517)CaDiCaL version: 2.1.3 % 250.46/35.57 % (3432517)Termination reason: Inappropriate % 250.46/35.57 % (3432517)Time elapsed: 0.002 s % 250.46/35.57 % (3432517)Peak memory usage: 10 MB % 250.46/35.57 % (3432517)Instructions burned: 1 (million) % 250.46/35.57 % (3432517)------------------------------ % 250.46/35.57 % (3432517)------------------------------ % 250.46/35.57 % (3432519)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=3759365332:rtra=on_2776 on theBenchmark for (2776ds/0Mi) % 250.46/35.57 % (3432519)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 250.46/35.57 % (3432519)Terminated due to inappropriate strategy. % 250.46/35.57 % (3432519)------------------------------ % 250.46/35.57 % (3432519)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 250.46/35.57 % (3432519)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 250.46/35.57 % (3432519)CaDiCaL version: 2.1.3 % 250.46/35.57 % (3432519)Termination reason: Inappropriate % 250.46/35.57 % (3432519)Time elapsed: 0.002 s % 250.46/35.57 % (3432519)Peak memory usage: 10 MB % 250.46/35.57 % (3432519)Instructions burned: 1 (million) % 250.46/35.57 % (3432519)------------------------------ % 250.46/35.57 % (3432519)------------------------------ % 250.46/35.57 % (3432521)% WARNING: option uhcvi not known. % 250.46/35.57 % (3432521)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3234390580:i=271062:add=off:rtra=on:rawr=on_2776 on theBenchmark for (2776ds/271062Mi) % 278.86/39.54 % (3432151)Instruction limit reached! % 278.86/39.54 % (3432151)------------------------------ % 278.86/39.54 % (3432151)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 278.86/39.54 % (3432151)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 278.86/39.54 % (3432151)CaDiCaL version: 2.1.3 % 278.86/39.54 % (3432151)Termination reason: Instruction limit % 278.86/39.54 % (3432151)Termination phase: Saturation % 278.86/39.54 % (3432151)Time elapsed: 15.114 s % 278.86/39.54 % (3432151)Peak memory usage: 67 MB % 278.86/39.54 % (3432151)Instructions burned: 20139 (million) % 278.86/39.54 % (3432523)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2478158474:i=176048:add=on:rtra=on:rawr=on_2770 on theBenchmark for (2770ds/176048Mi) % 278.86/39.54 % (3432302)Instruction limit reached! % 278.86/39.54 % (3432302)------------------------------ % 278.86/39.54 % (3432302)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 278.86/39.54 % (3432302)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 278.86/39.54 % (3432302)CaDiCaL version: 2.1.3 % 278.86/39.54 % (3432302)Termination reason: Instruction limit % 278.86/39.54 % (3432302)Termination phase: Saturation % 278.86/39.54 % (3432302)Time elapsed: 16.363 s % 278.86/39.54 % (3432302)Peak memory usage: 151 MB % 278.86/39.54 % (3432302)Instructions burned: 17628 (million) % 278.86/39.54 % (3432533)dis+10_1_sil=32000:si=on:sp=arity:random_seed=633212571:i=206:fgj=on:rtra=on_2688 on theBenchmark for (2688ds/206Mi) % 278.86/39.54 % (3432533)Instruction limit reached! % 278.86/39.54 % (3432533)------------------------------ % 278.86/39.54 % (3432533)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 278.86/39.54 % (3432533)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 278.86/39.54 % (3432533)CaDiCaL version: 2.1.3 % 278.86/39.54 % (3432533)Termination reason: Instruction limit % 278.86/39.54 % (3432533)Termination phase: Saturation % 278.86/39.54 % (3432533)Time elapsed: 0.197 s % 278.86/39.54 % (3432533)Peak memory usage: 13 MB % 278.86/39.54 % (3432533)Instructions burned: 206 (million) % 278.86/39.54 % (3432535)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=4156207214:i=232:rtra=on_2685 on theBenchmark for (2685ds/232Mi) % 278.86/39.54 % (3432535)Instruction limit reached! % 278.86/39.54 % (3432535)------------------------------ % 278.86/39.54 % (3432535)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 278.86/39.54 % (3432535)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 278.86/39.54 % (3432535)CaDiCaL version: 2.1.3 % 278.86/39.54 % (3432535)Termination reason: Instruction limit % 278.86/39.54 % (3432535)Termination phase: Saturation % 278.86/39.54 % (3432535)Time elapsed: 0.228 s % 278.86/39.54 % (3432535)Peak memory usage: 13 MB % 278.86/39.54 % (3432535)Instructions burned: 233 (million) % 278.86/39.54 % (3432537)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=2729775673:i=262:rtra=on_2683 on theBenchmark for (2683ds/262Mi) % 278.86/39.54 % (3432537)Instruction limit reached! % 278.86/39.54 % (3432537)------------------------------ % 278.86/39.54 % (3432537)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 278.86/39.54 % (3432537)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 278.86/39.54 % (3432537)CaDiCaL version: 2.1.3 % 278.86/39.54 % (3432537)Termination reason: Instruction limit % 278.86/39.54 % (3432537)Termination phase: Saturation % 278.86/39.54 % (3432537)Time elapsed: 0.230 s % 278.86/39.54 % (3432537)Peak memory usage: 13 MB % 278.86/39.54 % (3432537)Instructions burned: 263 (million) % 278.86/39.54 % (3432539)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=1147806178:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2680 on theBenchmark for (2680ds/318Mi) % 278.86/39.54 % (3432539)Instruction limit reached! % 278.86/39.54 % (3432539)------------------------------ % 278.86/39.54 % (3432539)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 278.86/39.54 % (3432539)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 278.86/39.54 % (3432539)CaDiCaL version: 2.1.3 % 278.86/39.54 % (3432539)Termination reason: Instruction limit % 278.86/39.54 % (3432539)Termination phase: Saturation % 278.86/39.54 % (3432539)Time elapsed: 0.337 s % 278.86/39.54 % (3432539)Peak memory usage: 15 MB % 278.86/39.54 % (3432539)Instructions burned: 318 (million) % 278.86/39.54 % (3432543)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=3604997103:i=1428:nm=2:rtra=on_2676 on theBenchmark for (2676ds/1428Mi) % 289.86/41.12 % (3432543)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 289.86/41.12 % (3432543)Terminated due to inappropriate strategy. % 289.86/41.12 % (3432543)------------------------------ % 289.86/41.12 % (3432543)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 289.86/41.12 % (3432543)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.86/41.12 % (3432543)CaDiCaL version: 2.1.3 % 289.86/41.12 % (3432543)Termination reason: Inappropriate % 289.86/41.12 % (3432543)Time elapsed: 0.002 s % 289.86/41.12 % (3432543)Peak memory usage: 10 MB % 289.86/41.12 % (3432543)Instructions burned: 1 (million) % 289.86/41.12 % (3432543)------------------------------ % 289.86/41.12 % (3432543)------------------------------ % 289.86/41.12 % (3432545)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=738896417:i=262:bd=preordered:rtra=on:fsd=on_2676 on theBenchmark for (2676ds/262Mi) % 289.86/41.12 % (3432545)Instruction limit reached! % 289.86/41.12 % (3432545)------------------------------ % 289.86/41.12 % (3432545)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 289.86/41.12 % (3432545)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.86/41.12 % (3432545)CaDiCaL version: 2.1.3 % 289.86/41.12 % (3432545)Termination reason: Instruction limit % 289.86/41.12 % (3432545)Termination phase: Saturation % 289.86/41.12 % (3432545)Time elapsed: 0.237 s % 289.86/41.12 % (3432545)Peak memory usage: 14 MB % 289.86/41.12 % (3432545)Instructions burned: 262 (million) % 289.86/41.12 % (3432547)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:si=on:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=2211506236:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2673 on theBenchmark for (2673ds/1368Mi) % 289.86/41.12 % (3432547)Instruction limit reached! % 289.86/41.12 % (3432547)------------------------------ % 289.86/41.12 % (3432547)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 289.86/41.12 % (3432547)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.86/41.12 % (3432547)CaDiCaL version: 2.1.3 % 289.86/41.12 % (3432547)Termination reason: Instruction limit % 289.86/41.12 % (3432547)Termination phase: Saturation % 289.86/41.12 % (3432547)Time elapsed: 1.279 s % 289.86/41.12 % (3432547)Peak memory usage: 21 MB % 289.86/41.12 % (3432547)Instructions burned: 1368 (million) % 289.86/41.12 % (3432549)ott-21_1_sil=16000:si=on:fs=off:random_seed=2080601162:i=360:av=off:fsr=off:rtra=on_2660 on theBenchmark for (2660ds/360Mi) % 289.86/41.12 % (3432549)Instruction limit reached! % 289.86/41.12 % (3432549)------------------------------ % 289.86/41.12 % (3432549)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 289.86/41.12 % (3432549)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.86/41.12 % (3432549)CaDiCaL version: 2.1.3 % 289.86/41.12 % (3432549)Termination reason: Instruction limit % 289.86/41.12 % (3432549)Termination phase: Saturation % 289.86/41.12 % (3432549)Time elapsed: 0.282 s % 289.86/41.12 % (3432549)Peak memory usage: 13 MB % 289.86/41.12 % (3432549)Instructions burned: 360 (million) % 289.86/41.12 % (3432551)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1584477774:i=954:bd=all:rtra=on_2657 on theBenchmark for (2657ds/954Mi) % 289.86/41.12 % (3432551)Instruction limit reached! % 289.86/41.12 % (3432551)------------------------------ % 289.86/41.12 % (3432551)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 289.86/41.12 % (3432551)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.86/41.12 % (3432551)CaDiCaL version: 2.1.3 % 289.86/41.12 % (3432551)Termination reason: Instruction limit % 289.86/41.12 % (3432551)Termination phase: Saturation % 289.86/41.12 % (3432551)Time elapsed: 0.992 s % 289.86/41.12 % (3432551)Peak memory usage: 16 MB % 289.86/41.12 % (3432551)Instructions burned: 954 (million) % 289.86/41.12 % (3432553)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=4030720956:fmbsr=1.3:i=1730:ins=25:rtra=on_2647 on theBenchmark for (2647ds/1730Mi) % 289.86/41.12 % (3432553)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 289.86/41.12 % (3432553)Terminated due to inappropriate strategy. % 289.86/41.12 % (3432553)------------------------------ % 289.86/41.12 % (3432553)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 289.86/41.12 % (3432553)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.86/41.12 % (3432553)CaDiCaL version: 2.1.3 % 289.86/41.12 % (3432553)Termination reason: InappropriateTerminated % 300.24/42.54 % Vampire exiting % 300.24/42.55 Terminated %------------------------------------------------------------------------------