%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWX117_1 : TPTP v9.3.1. Released v9.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n009.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:46:31 PM UTC 2026 % Result : Timeout 300.37s 42.64s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWX117_1 : TPTP v9.3.1. Released v9.1.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.09/0.26 % Computer : n009.cluster.edu % 0.09/0.26 % Model : x86_64 x86_64 % 0.09/0.26 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.26 % Memory : 8046.5625MB % 0.09/0.26 % OS : Linux 6.8.0-71-generic % 0.09/0.26 % CPULimit : 300 % 0.09/0.26 % WCLimit : 300 % 0.09/0.26 % DateTime : Mon Sep 28 15:02:15 UTC 2026 % 0.09/0.26 % CPUTime : % 0.09/0.26 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.26/0.31 Running first-order model finding % 0.26/0.31 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 6.86/1.37 % (3127544)Will run a generic schedule for satisfiability detection. % 6.86/1.37 % (3127550)% WARNING: option uhcvi not known. % 6.86/1.37 % (3127550)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=449781434:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 6.86/1.37 % (3127552)dis+10_1_sil=32000:sp=arity:random_seed=2429245991:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 6.86/1.37 % (3127554)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=908782446:i=131_2999 on theBenchmark for (2999ds/131Mi) % 6.86/1.37 % (3127553)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=883793805:i=116_2999 on theBenchmark for (2999ds/116Mi) % 6.86/1.37 % (3127549)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1776370869_2999 on theBenchmark for (2999ds/0Mi) % 6.86/1.37 % (3127551)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=980469336:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 6.86/1.37 % (3127555)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=26176889:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 6.86/1.37 % (3127549)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 6.86/1.37 % (3127549)Terminated due to inappropriate strategy. % 6.86/1.37 % (3127549)------------------------------ % 6.86/1.37 % (3127549)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.86/1.37 % (3127549)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.86/1.37 % (3127549)CaDiCaL version: 2.1.3 % 6.86/1.37 % (3127549)Termination reason: Inappropriate % 6.86/1.37 % (3127549)Time elapsed: 0.006 s % 6.86/1.37 % (3127549)Peak memory usage: 11 MB % 6.86/1.37 % (3127549)Instructions burned: 6 (million) % 6.86/1.37 % (3127549)------------------------------ % 6.86/1.37 % (3127549)------------------------------ % 6.86/1.37 % (3127563)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1825936104:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 6.86/1.37 % (3127563)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 6.86/1.37 % (3127563)Terminated due to inappropriate strategy. % 6.86/1.37 % (3127563)------------------------------ % 6.86/1.37 % (3127563)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.86/1.37 % (3127563)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.86/1.37 % (3127563)CaDiCaL version: 2.1.3 % 6.86/1.37 % (3127563)Termination reason: Inappropriate % 6.86/1.37 % (3127563)Time elapsed: 0.005 s % 6.86/1.37 % (3127563)Peak memory usage: 10 MB % 6.86/1.37 % (3127563)Instructions burned: 4 (million) % 6.86/1.37 % (3127563)------------------------------ % 6.86/1.37 % (3127563)------------------------------ % 6.86/1.37 % (3127565)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1458594288:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 6.86/1.37 % (3127552)Instruction limit reached! % 6.86/1.37 % (3127552)------------------------------ % 6.86/1.37 % (3127552)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.86/1.37 % (3127552)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.86/1.37 % (3127552)CaDiCaL version: 2.1.3 % 6.86/1.37 % (3127552)Termination reason: Instruction limit % 6.86/1.37 % (3127552)Termination phase: Saturation % 6.86/1.37 % (3127552)Time elapsed: 0.112 s % 6.86/1.37 % (3127552)Peak memory usage: 13 MB % 6.86/1.37 % (3127552)Instructions burned: 103 (million) % 6.86/1.37 % (3127553)Instruction limit reached! % 6.86/1.37 % (3127553)------------------------------ % 6.86/1.37 % (3127553)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.86/1.37 % (3127553)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.86/1.37 % (3127553)CaDiCaL version: 2.1.3 % 6.86/1.37 % (3127553)Termination reason: Instruction limit % 6.86/1.37 % (3127553)Termination phase: Saturation % 6.86/1.37 % (3127553)Time elapsed: 0.112 s % 6.86/1.37 % (3127553)Peak memory usage: 13 MB % 6.86/1.37 % (3127553)Instructions burned: 116 (million) % 6.86/1.37 % (3127554)Instruction limit reached! % 6.86/1.37 % (3127554)------------------------------ % 6.86/1.37 % (3127554)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.86/1.37 % (3127554)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.86/1.37 % (3127554)CaDiCaL version: 2.1.3 % 6.86/1.37 % (3127554)Termination reason: Instruction limit % 8.69/1.82 % (3127554)Termination phase: Saturation % 8.69/1.82 % (3127554)Time elapsed: 0.121 s % 8.69/1.82 % (3127554)Peak memory usage: 13 MB % 8.69/1.82 % (3127554)Instructions burned: 131 (million) % 8.69/1.82 % (3127567)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=1206430866:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 8.69/1.82 % (3127568)ott-21_1_sil=16000:fs=off:random_seed=1673870559:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 8.69/1.82 % (3127569)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=716550463:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 8.69/1.82 % (3127555)Instruction limit reached! % 8.69/1.82 % (3127555)------------------------------ % 8.69/1.82 % (3127555)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.69/1.82 % (3127555)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.69/1.82 % (3127555)CaDiCaL version: 2.1.3 % 8.69/1.82 % (3127555)Termination reason: Instruction limit % 8.69/1.82 % (3127555)Termination phase: Saturation % 8.69/1.82 % (3127555)Time elapsed: 0.179 s % 8.69/1.82 % (3127555)Peak memory usage: 14 MB % 8.69/1.82 % (3127555)Instructions burned: 159 (million) % 8.69/1.82 % (3127573)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1427186275:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi) % 8.69/1.82 % (3127573)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 8.69/1.82 % (3127573)Terminated due to inappropriate strategy. % 8.69/1.82 % (3127573)------------------------------ % 8.69/1.82 % (3127573)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.69/1.82 % (3127573)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.69/1.82 % (3127573)CaDiCaL version: 2.1.3 % 8.69/1.82 % (3127573)Termination reason: Inappropriate % 8.69/1.82 % (3127573)Time elapsed: 0.004 s % 8.69/1.82 % (3127573)Peak memory usage: 10 MB % 8.69/1.82 % (3127573)Instructions burned: 3 (million) % 8.69/1.82 % (3127573)------------------------------ % 8.69/1.82 % (3127573)------------------------------ % 8.69/1.82 % (3127565)Instruction limit reached! % 8.69/1.82 % (3127565)------------------------------ % 8.69/1.82 % (3127565)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.69/1.82 % (3127565)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.69/1.82 % (3127565)CaDiCaL version: 2.1.3 % 8.69/1.82 % (3127565)Termination reason: Instruction limit % 8.69/1.82 % (3127565)Termination phase: Saturation % 8.69/1.82 % (3127565)Time elapsed: 0.139 s % 8.69/1.82 % (3127565)Peak memory usage: 13 MB % 8.69/1.82 % (3127565)Instructions burned: 132 (million) % 8.69/1.82 % (3127575)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1026640555:i=1179_2997 on theBenchmark for (2997ds/1179Mi) % 8.69/1.82 % (3127576)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=269179477:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi) % 8.69/1.82 % (3127576)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 8.69/1.82 % (3127576)Terminated due to inappropriate strategy. % 8.69/1.82 % (3127576)------------------------------ % 8.69/1.82 % (3127576)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.69/1.82 % (3127576)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.69/1.82 % (3127576)CaDiCaL version: 2.1.3 % 8.69/1.82 % (3127576)Termination reason: Inappropriate % 8.69/1.82 % (3127576)Time elapsed: 0.005 s % 8.69/1.82 % (3127576)Peak memory usage: 11 MB % 8.69/1.82 % (3127576)Instructions burned: 4 (million) % 8.69/1.82 % (3127576)------------------------------ % 8.69/1.82 % (3127576)------------------------------ % 8.69/1.82 % (3127568)Instruction limit reached! % 8.69/1.82 % (3127568)------------------------------ % 8.69/1.82 % (3127568)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.69/1.82 % (3127568)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.69/1.82 % (3127568)CaDiCaL version: 2.1.3 % 8.69/1.82 % (3127568)Termination reason: Instruction limit % 8.69/1.82 % (3127568)Termination phase: Saturation % 8.69/1.82 % (3127568)Time elapsed: 0.148 s % 8.69/1.82 % (3127568)Peak memory usage: 12 MB % 8.69/1.82 % (3127568)Instructions burned: 181 (million) % 8.69/1.82 % (3127579)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=1942807892:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2996 on theBenchmark for (2996ds/692Mi) % 37.23/5.67 % (3127580)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3011471818:i=879:kws=inv_precedence:fsr=off_2996 on theBenchmark for (2996ds/879Mi) % 37.23/5.67 % (3127569)Instruction limit reached! % 37.23/5.67 % (3127569)------------------------------ % 37.23/5.67 % (3127569)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 37.23/5.67 % (3127569)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.23/5.67 % (3127569)CaDiCaL version: 2.1.3 % 37.23/5.67 % (3127569)Termination reason: Instruction limit % 37.23/5.67 % (3127569)Termination phase: Saturation % 37.23/5.67 % (3127569)Time elapsed: 0.529 s % 37.23/5.67 % (3127569)Peak memory usage: 14 MB % 37.23/5.67 % (3127569)Instructions burned: 477 (million) % 37.23/5.67 % (3127583)fmb+10_1_sil=64000:random_seed=1891264618:i=22061:nm=2:gsp=on_2992 on theBenchmark for (2992ds/22061Mi) % 37.23/5.67 % (3127583)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 37.23/5.67 % (3127583)Terminated due to inappropriate strategy. % 37.23/5.67 % (3127583)------------------------------ % 37.23/5.67 % (3127583)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 37.23/5.67 % (3127583)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.23/5.67 % (3127583)CaDiCaL version: 2.1.3 % 37.23/5.67 % (3127583)Termination reason: Inappropriate % 37.23/5.67 % (3127583)Time elapsed: 0.004 s % 37.23/5.67 % (3127583)Peak memory usage: 11 MB % 37.23/5.67 % (3127583)Instructions burned: 5 (million) % 37.23/5.67 % (3127583)------------------------------ % 37.23/5.67 % (3127583)------------------------------ % 37.23/5.67 % (3127585)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1607140621:i=9515:nm=5_2992 on theBenchmark for (2992ds/9515Mi) % 37.23/5.67 % (3127585)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 37.23/5.67 % (3127585)Terminated due to inappropriate strategy. % 37.23/5.67 % (3127585)------------------------------ % 37.23/5.67 % (3127585)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 37.23/5.67 % (3127585)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.23/5.67 % (3127585)CaDiCaL version: 2.1.3 % 37.23/5.67 % (3127585)Termination reason: Inappropriate % 37.23/5.67 % (3127585)Time elapsed: 0.004 s % 37.23/5.67 % (3127585)Peak memory usage: 11 MB % 37.23/5.67 % (3127585)Instructions burned: 4 (million) % 37.23/5.67 % (3127585)------------------------------ % 37.23/5.67 % (3127585)------------------------------ % 37.23/5.67 % (3127587)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1486343917:fmbsr=1.7:i=920_2992 on theBenchmark for (2992ds/920Mi) % 37.23/5.67 % (3127587)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 37.23/5.67 % (3127587)Terminated due to inappropriate strategy. % 37.23/5.67 % (3127587)------------------------------ % 37.23/5.67 % (3127587)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 37.23/5.67 % (3127587)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.23/5.67 % (3127587)CaDiCaL version: 2.1.3 % 37.23/5.67 % (3127587)Termination reason: Inappropriate % 37.23/5.67 % (3127587)Time elapsed: 0.003 s % 37.23/5.67 % (3127587)Peak memory usage: 11 MB % 37.23/5.67 % (3127587)Instructions burned: 4 (million) % 37.23/5.67 % (3127587)------------------------------ % 37.23/5.67 % (3127587)------------------------------ % 37.23/5.67 % (3127589)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=890332603:i=5131_2991 on theBenchmark for (2991ds/5131Mi) % 37.23/5.67 % (3127567)Instruction limit reached! % 37.23/5.67 % (3127567)------------------------------ % 37.23/5.67 % (3127567)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 37.23/5.67 % (3127567)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.23/5.67 % (3127567)CaDiCaL version: 2.1.3 % 37.23/5.67 % (3127567)Termination reason: Instruction limit % 37.23/5.67 % (3127567)Termination phase: Saturation % 37.23/5.67 % (3127567)Time elapsed: 0.686 s % 37.23/5.67 % (3127567)Peak memory usage: 26 MB % 37.23/5.67 % (3127567)Instructions burned: 684 (million) % 37.23/5.67 % (3127591)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=203415411:i=1472:ins=7:fdi=8:gsp=on_2991 on theBenchmark for (2991ds/1472Mi) % 37.23/5.67 % (3127579)Instruction limit reached! % 37.23/5.67 % (3127579)------------------------------ % 58.23/8.52 % (3127579)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 58.23/8.52 % (3127579)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 58.23/8.52 % (3127579)CaDiCaL version: 2.1.3 % 58.23/8.52 % (3127579)Termination reason: Instruction limit % 58.23/8.52 % (3127579)Termination phase: Saturation % 58.23/8.52 % (3127579)Time elapsed: 0.711 s % 58.23/8.52 % (3127579)Peak memory usage: 18 MB % 58.23/8.52 % (3127579)Instructions burned: 692 (million) % 58.23/8.52 % (3127597)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3772731681:i=6324_2989 on theBenchmark for (2989ds/6324Mi) % 58.23/8.52 % (3127597)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 58.23/8.52 % (3127597)Terminated due to inappropriate strategy. % 58.23/8.52 % (3127597)------------------------------ % 58.23/8.52 % (3127597)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 58.23/8.52 % (3127597)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 58.23/8.52 % (3127597)CaDiCaL version: 2.1.3 % 58.23/8.52 % (3127597)Termination reason: Inappropriate % 58.23/8.52 % (3127597)Time elapsed: 0.006 s % 58.23/8.52 % (3127597)Peak memory usage: 11 MB % 58.23/8.52 % (3127597)Instructions burned: 6 (million) % 58.23/8.52 % (3127597)------------------------------ % 58.23/8.52 % (3127597)------------------------------ % 58.23/8.52 % (3127599)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3118530539:fmbsr=2.30978:i=2174_2989 on theBenchmark for (2989ds/2174Mi) % 58.23/8.52 % (3127599)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 58.23/8.52 % (3127599)Terminated due to inappropriate strategy. % 58.23/8.52 % (3127599)------------------------------ % 58.23/8.52 % (3127599)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 58.23/8.52 % (3127599)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 58.23/8.52 % (3127599)CaDiCaL version: 2.1.3 % 58.23/8.52 % (3127599)Termination reason: Inappropriate % 58.23/8.52 % (3127599)Time elapsed: 0.004 s % 58.23/8.52 % (3127599)Peak memory usage: 11 MB % 58.23/8.52 % (3127599)Instructions burned: 4 (million) % 58.23/8.52 % (3127599)------------------------------ % 58.23/8.52 % (3127599)------------------------------ % 58.23/8.52 % (3127601)ott-2_1_sil=16000:newcnf=on:random_seed=4267129006:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2988 on theBenchmark for (2988ds/869Mi) % 58.23/8.52 % (3127580)Instruction limit reached! % 58.23/8.52 % (3127580)------------------------------ % 58.23/8.52 % (3127580)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 58.23/8.52 % (3127580)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 58.23/8.52 % (3127580)CaDiCaL version: 2.1.3 % 58.23/8.52 % (3127580)Termination reason: Instruction limit % 58.23/8.52 % (3127580)Termination phase: Saturation % 58.23/8.52 % (3127580)Time elapsed: 0.805 s % 58.23/8.52 % (3127580)Peak memory usage: 19 MB % 58.23/8.52 % (3127580)Instructions burned: 879 (million) % 58.23/8.52 % (3127603)ott+10_1_sil=32000:tgt=ground:random_seed=2089283163:i=5114:av=off_2988 on theBenchmark for (2988ds/5114Mi) % 58.23/8.52 % (3127575)Instruction limit reached! % 58.23/8.52 % (3127575)------------------------------ % 58.23/8.52 % (3127575)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 58.23/8.52 % (3127575)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 58.23/8.52 % (3127575)CaDiCaL version: 2.1.3 % 58.23/8.52 % (3127575)Termination reason: Instruction limit % 58.23/8.52 % (3127575)Termination phase: Saturation % 58.23/8.52 % (3127575)Time elapsed: 1.168 s % 58.23/8.52 % (3127575)Peak memory usage: 20 MB % 58.23/8.52 % (3127575)Instructions burned: 1179 (million) % 58.23/8.52 % (3127605)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1186278412:i=54282_2985 on theBenchmark for (2985ds/54282Mi) % 58.23/8.52 % (3127605)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 58.23/8.52 % (3127605)Terminated due to inappropriate strategy. % 58.23/8.52 % (3127605)------------------------------ % 58.23/8.52 % (3127605)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 58.23/8.52 % (3127605)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 58.23/8.52 % (3127605)CaDiCaL version: 2.1.3 % 58.23/8.52 % (3127605)Termination reason: Inappropriate % 58.23/8.52 % (3127605)Time elapsed: 0.006 s % 58.23/8.52 % (3127605)Peak memory usage: 11 MB % 58.23/8.52 % (3127605)Instructions burned: 6 (million) % 146.35/20.96 % (3127605)------------------------------ % 146.35/20.96 % (3127605)------------------------------ % 146.35/20.96 % (3127608)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3793337016:i=3512:aac=none_2985 on theBenchmark for (2985ds/3512Mi) % 146.35/20.96 % (3127601)Instruction limit reached! % 146.35/20.96 % (3127601)------------------------------ % 146.35/20.96 % (3127601)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 146.35/20.96 % (3127601)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 146.35/20.96 % (3127601)CaDiCaL version: 2.1.3 % 146.35/20.96 % (3127601)Termination reason: Instruction limit % 146.35/20.96 % (3127601)Termination phase: Saturation % 146.35/20.96 % (3127601)Time elapsed: 0.811 s % 146.35/20.96 % (3127601)Peak memory usage: 18 MB % 146.35/20.96 % (3127601)Instructions burned: 870 (million) % 146.35/20.96 % (3127611)dis+21_1_sil=32000:sas=cadical:random_seed=1040641986:i=3773:amm=off_2980 on theBenchmark for (2980ds/3773Mi) % 146.35/20.96 % (3127591)Instruction limit reached! % 146.35/20.96 % (3127591)------------------------------ % 146.35/20.96 % (3127591)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 146.35/20.96 % (3127591)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 146.35/20.96 % (3127591)CaDiCaL version: 2.1.3 % 146.35/20.96 % (3127591)Termination reason: Instruction limit % 146.35/20.96 % (3127591)Termination phase: Saturation % 146.35/20.96 % (3127591)Time elapsed: 1.457 s % 146.35/20.96 % (3127591)Peak memory usage: 28 MB % 146.35/20.96 % (3127591)Instructions burned: 1472 (million) % 146.35/20.96 % (3127613)ott+11_1_sil=16000:gs=on:random_seed=3679587939:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2976 on theBenchmark for (2976ds/2251Mi) % 146.35/20.96 % (3127613)Instruction limit reached! % 146.35/20.96 % (3127613)------------------------------ % 146.35/20.96 % (3127613)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 146.35/20.96 % (3127613)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 146.35/20.96 % (3127613)CaDiCaL version: 2.1.3 % 146.35/20.96 % (3127613)Termination reason: Instruction limit % 146.35/20.96 % (3127613)Termination phase: Saturation % 146.35/20.96 % (3127613)Time elapsed: 2.166 s % 146.35/20.96 % (3127613)Peak memory usage: 25 MB % 146.35/20.96 % (3127613)Instructions burned: 2251 (million) % 146.35/20.96 % (3127615)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3127777070:fmbsr=1.6:i=67534_2954 on theBenchmark for (2954ds/67534Mi) % 146.35/20.96 % (3127615)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 146.35/20.96 % (3127615)Terminated due to inappropriate strategy. % 146.35/20.96 % (3127615)------------------------------ % 146.35/20.96 % (3127615)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 146.35/20.96 % (3127615)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 146.35/20.96 % (3127615)CaDiCaL version: 2.1.3 % 146.35/20.96 % (3127615)Termination reason: Inappropriate % 146.35/20.96 % (3127615)Time elapsed: 0.005 s % 146.35/20.96 % (3127615)Peak memory usage: 10 MB % 146.35/20.96 % (3127615)Instructions burned: 4 (million) % 146.35/20.96 % (3127615)------------------------------ % 146.35/20.96 % (3127615)------------------------------ % 146.35/20.96 % (3127617)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1365680086:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2954 on theBenchmark for (2954ds/4591Mi) % 146.35/20.96 % (3127608)Instruction limit reached! % 146.35/20.96 % (3127608)------------------------------ % 146.35/20.96 % (3127608)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 146.35/20.96 % (3127608)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 146.35/20.96 % (3127608)CaDiCaL version: 2.1.3 % 146.35/20.96 % (3127608)Termination reason: Instruction limit % 146.35/20.96 % (3127608)Termination phase: Saturation % 146.35/20.96 % (3127608)Time elapsed: 3.344 s % 146.35/20.96 % (3127608)Peak memory usage: 32 MB % 146.35/20.96 % (3127608)Instructions burned: 3513 (million) % 146.35/20.96 % (3127621)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1953855745:i=29340_2951 on theBenchmark for (2951ds/29340Mi) % 146.35/20.96 % (3127589)Instruction limit reached! % 146.35/20.96 % (3127589)------------------------------ % 146.35/20.96 % (3127589)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 146.35/20.96 % (3127589)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 146.35/20.96 % (3127589)CaDiCaL version: 2.1.3 % 146.35/20.96 % (3127589)Termination reason: Instruction limit % 170.49/24.35 % (3127589)Termination phase: Saturation % 170.49/24.35 % (3127589)Time elapsed: 4.511 s % 170.49/24.35 % (3127589)Peak memory usage: 34 MB % 170.49/24.35 % (3127589)Instructions burned: 5133 (million) % 170.49/24.35 % (3127623)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=1043693766:i=5211_2946 on theBenchmark for (2946ds/5211Mi) % 170.49/24.35 % (3127611)Instruction limit reached! % 170.49/24.35 % (3127611)------------------------------ % 170.49/24.35 % (3127611)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 170.49/24.35 % (3127611)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 170.49/24.35 % (3127611)CaDiCaL version: 2.1.3 % 170.49/24.35 % (3127611)Termination reason: Instruction limit % 170.49/24.35 % (3127611)Termination phase: Saturation % 170.49/24.35 % (3127611)Time elapsed: 3.565 s % 170.49/24.35 % (3127611)Peak memory usage: 35 MB % 170.49/24.35 % (3127611)Instructions burned: 3773 (million) % 170.49/24.35 % (3127625)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=997939129:i=5497:nm=2_2944 on theBenchmark for (2944ds/5497Mi) % 170.49/24.35 % (3127625)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 170.49/24.35 % (3127625)Terminated due to inappropriate strategy. % 170.49/24.35 % (3127625)------------------------------ % 170.49/24.35 % (3127625)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 170.49/24.35 % (3127625)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 170.49/24.35 % (3127625)CaDiCaL version: 2.1.3 % 170.49/24.35 % (3127625)Termination reason: Inappropriate % 170.49/24.35 % (3127625)Time elapsed: 0.006 s % 170.49/24.35 % (3127625)Peak memory usage: 11 MB % 170.49/24.35 % (3127625)Instructions burned: 6 (million) % 170.49/24.35 % (3127625)------------------------------ % 170.49/24.35 % (3127625)------------------------------ % 170.49/24.35 % (3127627)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=2781272490:fmbsr=2:i=46332_2943 on theBenchmark for (2943ds/46332Mi) % 170.49/24.35 % (3127627)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 170.49/24.35 % (3127627)Terminated due to inappropriate strategy. % 170.49/24.35 % (3127627)------------------------------ % 170.49/24.35 % (3127627)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 170.49/24.35 % (3127627)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 170.49/24.35 % (3127627)CaDiCaL version: 2.1.3 % 170.49/24.35 % (3127627)Termination reason: Inappropriate % 170.49/24.35 % (3127627)Time elapsed: 0.005 s % 170.49/24.35 % (3127627)Peak memory usage: 11 MB % 170.49/24.35 % (3127627)Instructions burned: 4 (million) % 170.49/24.35 % (3127627)------------------------------ % 170.49/24.35 % (3127627)------------------------------ % 170.49/24.35 % (3127629)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=606599796:i=14071_2943 on theBenchmark for (2943ds/14071Mi) % 170.49/24.35 % (3127629)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 170.49/24.35 % (3127629)Terminated due to inappropriate strategy. % 170.49/24.35 % (3127629)------------------------------ % 170.49/24.35 % (3127629)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 170.49/24.35 % (3127629)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 170.49/24.35 % (3127629)CaDiCaL version: 2.1.3 % 170.49/24.35 % (3127629)Termination reason: Inappropriate % 170.49/24.35 % (3127629)Time elapsed: 0.004 s % 170.49/24.35 % (3127629)Peak memory usage: 11 MB % 170.49/24.35 % (3127629)Instructions burned: 4 (million) % 170.49/24.35 % (3127629)------------------------------ % 170.49/24.35 % (3127629)------------------------------ % 170.49/24.35 % (3127631)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2251452349:i=22565:add=on:rawr=on_2943 on theBenchmark for (2943ds/22565Mi) % 170.49/24.35 % (3127603)Instruction limit reached! % 170.49/24.35 % (3127603)------------------------------ % 170.49/24.35 % (3127603)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 170.49/24.35 % (3127603)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 170.49/24.35 % (3127603)CaDiCaL version: 2.1.3 % 170.49/24.35 % (3127603)Termination reason: Instruction limit % 170.49/24.35 % (3127603)Termination phase: Saturation % 170.49/24.35 % (3127603)Time elapsed: 4.598 s % 170.49/24.35 % (3127603)Peak memory usage: 31 MB % 170.49/24.35 % (3127603)Instructions burned: 5114 (million) % 170.49/24.35 % (3127633)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=3578672224:i=8173:av=off_2942 on theBenchmark for (2942ds/8173Mi) % 170.49/24.35 % (3127617)Instruction limit reached! % 171.22/24.48 % (3127617)------------------------------ % 171.22/24.48 % (3127617)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 171.22/24.48 % (3127617)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 171.22/24.48 % (3127617)CaDiCaL version: 2.1.3 % 171.22/24.48 % (3127617)Termination reason: Instruction limit % 171.22/24.48 % (3127617)Termination phase: Saturation % 171.22/24.48 % (3127617)Time elapsed: 3.592 s % 171.22/24.48 % (3127617)Peak memory usage: 35 MB % 171.22/24.48 % (3127617)Instructions burned: 4593 (million) % 171.22/24.48 % (3127639)dis+10_16:1_sil=16000:random_seed=3903779430:i=9155:fsr=off_2917 on theBenchmark for (2917ds/9155Mi) % 171.22/24.48 % (3127623)Instruction limit reached! % 171.22/24.48 % (3127623)------------------------------ % 171.22/24.48 % (3127623)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 171.22/24.48 % (3127623)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 171.22/24.48 % (3127623)CaDiCaL version: 2.1.3 % 171.22/24.48 % (3127623)Termination reason: Instruction limit % 171.22/24.48 % (3127623)Termination phase: Saturation % 171.22/24.48 % (3127623)Time elapsed: 4.282 s % 171.22/24.48 % (3127623)Peak memory usage: 30 MB % 171.22/24.48 % (3127623)Instructions burned: 5212 (million) % 171.22/24.48 % (3127643)ott-3_8_sil=64000:random_seed=3226765358:i=20139:bs=on_2903 on theBenchmark for (2903ds/20139Mi) % 171.22/24.48 % (3127633)Instruction limit reached! % 171.22/24.48 % (3127633)------------------------------ % 171.22/24.48 % (3127633)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 171.22/24.48 % (3127633)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 171.22/24.48 % (3127633)CaDiCaL version: 2.1.3 % 171.22/24.48 % (3127633)Termination reason: Instruction limit % 171.22/24.48 % (3127633)Termination phase: Saturation % 171.22/24.48 % (3127633)Time elapsed: 7.456 s % 171.22/24.48 % (3127633)Peak memory usage: 53 MB % 171.22/24.48 % (3127633)Instructions burned: 8173 (million) % 171.22/24.48 % (3127789)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=1394645595:fmbsr=2:i=32576_2867 on theBenchmark for (2867ds/32576Mi) % 171.22/24.48 % (3127789)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 171.22/24.48 % (3127789)Terminated due to inappropriate strategy. % 171.22/24.48 % (3127789)------------------------------ % 171.22/24.48 % (3127789)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 171.22/24.48 % (3127789)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 171.22/24.48 % (3127789)CaDiCaL version: 2.1.3 % 171.22/24.48 % (3127789)Termination reason: Inappropriate % 171.22/24.48 % (3127789)Time elapsed: 0.004 s % 171.22/24.48 % (3127789)Peak memory usage: 11 MB % 171.22/24.48 % (3127789)Instructions burned: 6 (million) % 171.22/24.48 % (3127789)------------------------------ % 171.22/24.48 % (3127789)------------------------------ % 171.22/24.48 % (3127799)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=3699450933:i=11404_2866 on theBenchmark for (2866ds/11404Mi) % 171.22/24.48 % (3127639)Instruction limit reached! % 171.22/24.48 % (3127639)------------------------------ % 171.22/24.48 % (3127639)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 171.22/24.48 % (3127639)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 171.22/24.48 % (3127639)CaDiCaL version: 2.1.3 % 171.22/24.48 % (3127639)Termination reason: Instruction limit % 171.22/24.48 % (3127639)Termination phase: Saturation % 171.22/24.48 % (3127639)Time elapsed: 6.523 s % 171.22/24.48 % (3127639)Peak memory usage: 53 MB % 171.22/24.48 % (3127639)Instructions burned: 9155 (million) % 171.22/24.48 % (3127805)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=408349486:i=14134_2852 on theBenchmark for (2852ds/14134Mi) % 171.22/24.48 % (3127631)Instruction limit reached! % 171.22/24.48 % (3127631)------------------------------ % 171.22/24.48 % (3127631)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 171.22/24.48 % (3127631)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 171.22/24.48 % (3127631)CaDiCaL version: 2.1.3 % 171.22/24.48 % (3127631)Termination reason: Instruction limit % 171.22/24.48 % (3127631)Termination phase: Saturation % 171.22/24.48 % (3127631)Time elapsed: 12.503 s % 171.22/24.48 % (3127631)Peak memory usage: 74 MB % 171.22/24.48 % (3127631)Instructions burned: 22565 (million) % 171.22/24.48 % (3127807)dis+33_16_sil=32000:sac=on:random_seed=1154506168:i=15851:nm=0_2817 on theBenchmark for (2817ds/15851Mi) % 171.22/24.48 % (3127799)Instruction limit reached! % 171.22/24.48 % (3127799)------------------------------ % 171.22/24.48 % (3127799)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 235.09/33.41 % (3127799)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.09/33.41 % (3127799)CaDiCaL version: 2.1.3 % 235.09/33.41 % (3127799)Termination reason: Instruction limit % 235.09/33.41 % (3127799)Termination phase: Saturation % 235.09/33.41 % (3127799)Time elapsed: 7.311 s % 235.09/33.41 % (3127799)Peak memory usage: 63 MB % 235.09/33.41 % (3127799)Instructions burned: 11405 (million) % 235.09/33.41 % (3127809)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=2898505774:avsq=on:i=17627:add=on:amm=off_2793 on theBenchmark for (2793ds/17627Mi) % 235.09/33.41 % (3127621)Instruction limit reached! % 235.09/33.41 % (3127621)------------------------------ % 235.09/33.41 % (3127621)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 235.09/33.41 % (3127621)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.09/33.41 % (3127621)CaDiCaL version: 2.1.3 % 235.09/33.41 % (3127621)Termination reason: Instruction limit % 235.09/33.41 % (3127621)Termination phase: Saturation % 235.09/33.41 % (3127621)Time elapsed: 18.397 s % 235.09/33.41 % (3127621)Peak memory usage: 77 MB % 235.09/33.41 % (3127621)Instructions burned: 29341 (million) % 235.09/33.41 % (3127811)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=3873944412:s2a=on:i=53295_2766 on theBenchmark for (2766ds/53295Mi) % 235.09/33.41 % (3127643)Instruction limit reached! % 235.09/33.41 % (3127643)------------------------------ % 235.09/33.41 % (3127643)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 235.09/33.41 % (3127643)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.09/33.41 % (3127643)CaDiCaL version: 2.1.3 % 235.09/33.41 % (3127643)Termination reason: Instruction limit % 235.09/33.41 % (3127643)Termination phase: Saturation % 235.09/33.41 % (3127643)Time elapsed: 13.792 s % 235.09/33.41 % (3127643)Peak memory usage: 84 MB % 235.09/33.41 % (3127643)Instructions burned: 20140 (million) % 235.09/33.41 % (3127813)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=3253442008:i=26857:ins=20_2764 on theBenchmark for (2764ds/26857Mi) % 235.09/33.41 % (3127813)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 235.09/33.41 % (3127813)Terminated due to inappropriate strategy. % 235.09/33.41 % (3127813)------------------------------ % 235.09/33.41 % (3127813)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 235.09/33.41 % (3127813)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.09/33.41 % (3127813)CaDiCaL version: 2.1.3 % 235.09/33.41 % (3127813)Termination reason: Inappropriate % 235.09/33.41 % (3127813)Time elapsed: 0.003 s % 235.09/33.41 % (3127813)Peak memory usage: 10 MB % 235.09/33.41 % (3127813)Instructions burned: 4 (million) % 235.09/33.41 % (3127813)------------------------------ % 235.09/33.41 % (3127813)------------------------------ % 235.09/33.41 % (3127815)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=2042652207:i=28120:bs=on:fsr=off_2764 on theBenchmark for (2764ds/28120Mi) % 235.09/33.41 % (3127805)Instruction limit reached! % 235.09/33.41 % (3127805)------------------------------ % 235.09/33.41 % (3127805)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 235.09/33.41 % (3127805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.09/33.41 % (3127805)CaDiCaL version: 2.1.3 % 235.09/33.41 % (3127805)Termination reason: Instruction limit % 235.09/33.41 % (3127805)Termination phase: Saturation % 235.09/33.41 % (3127805)Time elapsed: 9.191 s % 235.09/33.41 % (3127805)Peak memory usage: 72 MB % 235.09/33.41 % (3127805)Instructions burned: 14135 (million) % 235.09/33.41 % (3127817)fmb+10_1_sil=256000:fmbss=7:random_seed=758037009:fmbsr=1.6:i=182295_2760 on theBenchmark for (2760ds/182295Mi) % 235.09/33.41 % (3127817)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 235.09/33.41 % (3127817)Terminated due to inappropriate strategy. % 235.09/33.41 % (3127817)------------------------------ % 235.09/33.41 % (3127817)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 235.09/33.41 % (3127817)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.09/33.41 % (3127817)CaDiCaL version: 2.1.3 % 235.09/33.41 % (3127817)Termination reason: Inappropriate % 235.09/33.41 % (3127817)Time elapsed: 0.003 s % 235.09/33.41 % (3127817)Peak memory usage: 10 MB % 235.09/33.41 % (3127817)Instructions burned: 4 (million) % 235.09/33.41 % (3127817)------------------------------ % 235.09/33.41 % (3127817)------------------------------ % 235.09/33.41 % (3127819)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=485026847:i=44625:gsp=on_2759 on theBenchmark for (2759ds/44625Mi) % 248.56/35.39 % (3127819)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 248.56/35.39 % (3127819)Terminated due to inappropriate strategy. % 248.56/35.39 % (3127819)------------------------------ % 248.56/35.39 % (3127819)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 248.56/35.39 % (3127819)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 248.56/35.39 % (3127819)CaDiCaL version: 2.1.3 % 248.56/35.39 % (3127819)Termination reason: Inappropriate % 248.56/35.39 % (3127819)Time elapsed: 0.003 s % 248.56/35.39 % (3127819)Peak memory usage: 11 MB % 248.56/35.39 % (3127819)Instructions burned: 5 (million) % 248.56/35.39 % (3127819)------------------------------ % 248.56/35.39 % (3127819)------------------------------ % 248.56/35.39 % (3127821)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=4244979530:i=160505_2759 on theBenchmark for (2759ds/160505Mi) % 248.56/35.39 % (3127821)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 248.56/35.39 % (3127821)Terminated due to inappropriate strategy. % 248.56/35.39 % (3127821)------------------------------ % 248.56/35.39 % (3127821)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 248.56/35.39 % (3127821)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 248.56/35.39 % (3127821)CaDiCaL version: 2.1.3 % 248.56/35.39 % (3127821)Termination reason: Inappropriate % 248.56/35.39 % (3127821)Time elapsed: 0.003 s % 248.56/35.39 % (3127821)Peak memory usage: 10 MB % 248.56/35.39 % (3127821)Instructions burned: 4 (million) % 248.56/35.39 % (3127821)------------------------------ % 248.56/35.39 % (3127821)------------------------------ % 248.56/35.39 % (3127823)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=3368695727:fmbsr=1.3:i=225729_2759 on theBenchmark for (2759ds/225729Mi) % 248.56/35.39 % (3127823)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 248.56/35.39 % (3127823)Terminated due to inappropriate strategy. % 248.56/35.39 % (3127823)------------------------------ % 248.56/35.39 % (3127823)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 248.56/35.39 % (3127823)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 248.56/35.39 % (3127823)CaDiCaL version: 2.1.3 % 248.56/35.39 % (3127823)Termination reason: Inappropriate % 248.56/35.39 % (3127823)Time elapsed: 0.003 s % 248.56/35.39 % (3127823)Peak memory usage: 11 MB % 248.56/35.39 % (3127823)Instructions burned: 4 (million) % 248.56/35.39 % (3127823)------------------------------ % 248.56/35.39 % (3127823)------------------------------ % 248.56/35.39 % (3127825)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=609311863:fmbsr=2:i=185024:ins=7_2759 on theBenchmark for (2759ds/185024Mi) % 248.56/35.39 % (3127825)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 248.56/35.39 % (3127825)Terminated due to inappropriate strategy. % 248.56/35.39 % (3127825)------------------------------ % 248.56/35.39 % (3127825)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 248.56/35.39 % (3127825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 248.56/35.39 % (3127825)CaDiCaL version: 2.1.3 % 248.56/35.39 % (3127825)Termination reason: Inappropriate % 248.56/35.39 % (3127825)Time elapsed: 0.003 s % 248.56/35.39 % (3127825)Peak memory usage: 11 MB % 248.56/35.39 % (3127825)Instructions burned: 4 (million) % 248.56/35.39 % (3127825)------------------------------ % 248.56/35.39 % (3127825)------------------------------ % 248.56/35.39 % (3127827)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=2507812223:rtra=on_2758 on theBenchmark for (2758ds/0Mi) % 248.56/35.39 % (3127827)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 248.56/35.39 % (3127827)Terminated due to inappropriate strategy. % 248.56/35.39 % (3127827)------------------------------ % 248.56/35.39 % (3127827)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 248.56/35.39 % (3127827)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 248.56/35.39 % (3127827)CaDiCaL version: 2.1.3 % 248.56/35.39 % (3127827)Termination reason: Inappropriate % 248.56/35.39 % (3127827)Time elapsed: 0.004 s % 248.56/35.39 % (3127827)Peak memory usage: 11 MB % 248.56/35.39 % (3127827)Instructions burned: 6 (million) % 248.56/35.39 % (3127827)------------------------------ % 248.56/35.39 % (3127827)------------------------------ % 248.56/35.39 % (3127829)% WARNING: option uhcvi not known. % 248.56/35.39 % (3127829)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3019815613:i=271062:add=off:rtra=on:rawr=on_2758 on theBenchmark for (2758ds/271062Mi) % 264.16/37.55 % (3127807)Instruction limit reached! % 264.16/37.55 % (3127807)------------------------------ % 264.16/37.55 % (3127807)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 264.16/37.55 % (3127807)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 264.16/37.55 % (3127807)CaDiCaL version: 2.1.3 % 264.16/37.55 % (3127807)Termination reason: Instruction limit % 264.16/37.55 % (3127807)Termination phase: Saturation % 264.16/37.55 % (3127807)Time elapsed: 8.586 s % 264.16/37.55 % (3127807)Peak memory usage: 120 MB % 264.16/37.55 % (3127807)Instructions burned: 15852 (million) % 264.16/37.55 % (3127831)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1286707123:i=176048:add=on:rtra=on:rawr=on_2731 on theBenchmark for (2731ds/176048Mi) % 264.16/37.55 % (3127809)Instruction limit reached! % 264.16/37.55 % (3127809)------------------------------ % 264.16/37.55 % (3127809)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 264.16/37.55 % (3127809)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 264.16/37.55 % (3127809)CaDiCaL version: 2.1.3 % 264.16/37.55 % (3127809)Termination reason: Instruction limit % 264.16/37.55 % (3127809)Termination phase: Saturation % 264.16/37.55 % (3127809)Time elapsed: 11.648 s % 264.16/37.55 % (3127809)Peak memory usage: 90 MB % 264.16/37.55 % (3127809)Instructions burned: 17627 (million) % 264.16/37.55 % (3128176)dis+10_1_sil=32000:si=on:sp=arity:random_seed=679700729:i=206:fgj=on:rtra=on_2676 on theBenchmark for (2676ds/206Mi) % 264.16/37.55 % (3128176)Instruction limit reached! % 264.16/37.55 % (3128176)------------------------------ % 264.16/37.55 % (3128176)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 264.16/37.55 % (3128176)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 264.16/37.55 % (3128176)CaDiCaL version: 2.1.3 % 264.16/37.55 % (3128176)Termination reason: Instruction limit % 264.16/37.55 % (3128176)Termination phase: Saturation % 264.16/37.55 % (3128176)Time elapsed: 0.133 s % 264.16/37.55 % (3128176)Peak memory usage: 14 MB % 264.16/37.55 % (3128176)Instructions burned: 206 (million) % 264.16/37.55 % (3128181)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=2528722936:i=232:rtra=on_2675 on theBenchmark for (2675ds/232Mi) % 264.16/37.55 % (3128181)Instruction limit reached! % 264.16/37.55 % (3128181)------------------------------ % 264.16/37.55 % (3128181)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 264.16/37.55 % (3128181)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 264.16/37.55 % (3128181)CaDiCaL version: 2.1.3 % 264.16/37.55 % (3128181)Termination reason: Instruction limit % 264.16/37.55 % (3128181)Termination phase: Saturation % 264.16/37.55 % (3128181)Time elapsed: 0.147 s % 264.16/37.55 % (3128181)Peak memory usage: 14 MB % 264.16/37.55 % (3128181)Instructions burned: 232 (million) % 264.16/37.55 % (3128183)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=2106752422:i=262:rtra=on_2673 on theBenchmark for (2673ds/262Mi) % 264.16/37.55 % (3128183)Instruction limit reached! % 264.16/37.55 % (3128183)------------------------------ % 264.16/37.55 % (3128183)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 264.16/37.55 % (3128183)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 264.16/37.55 % (3128183)CaDiCaL version: 2.1.3 % 264.16/37.55 % (3128183)Termination reason: Instruction limit % 264.16/37.55 % (3128183)Termination phase: Saturation % 264.16/37.55 % (3128183)Time elapsed: 0.154 s % 264.16/37.55 % (3128183)Peak memory usage: 14 MB % 264.16/37.55 % (3128183)Instructions burned: 264 (million) % 264.16/37.55 % (3128185)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=4210301100:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2671 on theBenchmark for (2671ds/318Mi) % 264.16/37.55 % (3128185)Instruction limit reached! % 264.16/37.55 % (3128185)------------------------------ % 264.16/37.55 % (3128185)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 264.16/37.55 % (3128185)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 264.16/37.55 % (3128185)CaDiCaL version: 2.1.3 % 264.16/37.55 % (3128185)Termination reason: Instruction limit % 264.16/37.55 % (3128185)Termination phase: Saturation % 264.16/37.55 % (3128185)Time elapsed: 0.227 s % 264.16/37.55 % (3128185)Peak memory usage: 16 MB % 264.16/37.55 % (3128185)Instructions burned: 319 (million) % 264.16/37.55 % (3128187)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=2973050272:i=1428:nm=2:rtra=on_2669 on theBenchmark for (2669ds/1428Mi) % 279.07/39.70 % (3128187)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 279.07/39.70 % (3128187)Terminated due to inappropriate strategy. % 279.07/39.70 % (3128187)------------------------------ % 279.07/39.70 % (3128187)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 279.07/39.70 % (3128187)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.07/39.70 % (3128187)CaDiCaL version: 2.1.3 % 279.07/39.70 % (3128187)Termination reason: Inappropriate % 279.07/39.70 % (3128187)Time elapsed: 0.003 s % 279.07/39.70 % (3128187)Peak memory usage: 10 MB % 279.07/39.70 % (3128187)Instructions burned: 5 (million) % 279.07/39.70 % (3128187)------------------------------ % 279.07/39.70 % (3128187)------------------------------ % 279.07/39.70 % (3128189)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=1479610059:i=262:bd=preordered:rtra=on:fsd=on_2669 on theBenchmark for (2669ds/262Mi) % 279.07/39.70 % (3128189)Instruction limit reached! % 279.07/39.70 % (3128189)------------------------------ % 279.07/39.70 % (3128189)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 279.07/39.70 % (3128189)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.07/39.70 % (3128189)CaDiCaL version: 2.1.3 % 279.07/39.70 % (3128189)Termination reason: Instruction limit % 279.07/39.70 % (3128189)Termination phase: Saturation % 279.07/39.70 % (3128189)Time elapsed: 0.152 s % 279.07/39.70 % (3128189)Peak memory usage: 13 MB % 279.07/39.70 % (3128189)Instructions burned: 264 (million) % 279.07/39.70 % (3128191)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=3448141458:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2667 on theBenchmark for (2667ds/1368Mi) % 279.07/39.70 % (3128191)Instruction limit reached! % 279.07/39.70 % (3128191)------------------------------ % 279.07/39.70 % (3128191)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 279.07/39.70 % (3128191)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.07/39.70 % (3128191)CaDiCaL version: 2.1.3 % 279.07/39.70 % (3128191)Termination reason: Instruction limit % 279.07/39.70 % (3128191)Termination phase: Saturation % 279.07/39.70 % (3128191)Time elapsed: 0.877 s % 279.07/39.70 % (3128191)Peak memory usage: 25 MB % 279.07/39.70 % (3128191)Instructions burned: 1368 (million) % 279.07/39.70 % (3128193)ott-21_1_sil=16000:si=on:fs=off:random_seed=3797645918:i=360:av=off:fsr=off:rtra=on_2658 on theBenchmark for (2658ds/360Mi) % 279.07/39.70 % (3128193)Instruction limit reached! % 279.07/39.70 % (3128193)------------------------------ % 279.07/39.70 % (3128193)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 279.07/39.70 % (3128193)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.07/39.70 % (3128193)CaDiCaL version: 2.1.3 % 279.07/39.70 % (3128193)Termination reason: Instruction limit % 279.07/39.70 % (3128193)Termination phase: Saturation % 279.07/39.70 % (3128193)Time elapsed: 0.165 s % 279.07/39.70 % (3128193)Peak memory usage: 13 MB % 279.07/39.70 % (3128193)Instructions burned: 362 (million) % 279.07/39.70 % (3128195)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3638173744:i=954:bd=all:rtra=on_2656 on theBenchmark for (2656ds/954Mi) % 279.07/39.70 % (3128195)Instruction limit reached! % 279.07/39.70 % (3128195)------------------------------ % 279.07/39.70 % (3128195)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 279.07/39.70 % (3128195)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.07/39.70 % (3128195)CaDiCaL version: 2.1.3 % 279.07/39.70 % (3128195)Termination reason: Instruction limit % 279.07/39.70 % (3128195)Termination phase: Saturation % 279.07/39.70 % (3128195)Time elapsed: 0.667 s % 279.07/39.70 % (3128195)Peak memory usage: 17 MB % 279.07/39.70 % (3128195)Instructions burned: 954 (million) % 279.07/39.70 % (3128197)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=619070735:fmbsr=1.3:i=1730:ins=25:rtra=on_2649 on theBenchmark for (2649ds/1730Mi) % 279.07/39.70 % (3128197)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 279.07/39.70 % (3128197)Terminated due to inappropriate strategy. % 279.07/39.70 % (3128197)------------------------------ % 279.07/39.70 % (3128197)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 279.07/39.70 % (3128197)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.07/39.70 % (3128197)CaDiCaL version: 2.1.3 % 279.07/39.70 % (3128197)Termination reason: Inappropriate % 279.07/39.70 % (3128197)Time elapsed: 0.002 s % 300.37/42.64 % (3128197)Peak memory usage: 10 MB % 300.37/42.64 % (3128197)Instructions burned: 3 (million) % 300.37/42.64 % (3128197)------------------------------ % 300.37/42.64 % (3128197)------------------------------ % 300.37/42.64 % (3128199)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=189677626:i=2358:rtra=on_2649 on theBenchmark for (2649ds/2358Mi) % 300.37/42.64 % (3127815)Instruction limit reached! % 300.37/42.64 % (3127815)------------------------------ % 300.37/42.64 % (3127815)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.37/42.64 % (3127815)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.37/42.64 % (3127815)CaDiCaL version: 2.1.3 % 300.37/42.64 % (3127815)Termination reason: Instruction limit % 300.37/42.64 % (3127815)Termination phase: Saturation % 300.37/42.64 % (3127815)Time elapsed: 12.806 s % 300.37/42.64 % (3127815)Peak memory usage: 59 MB % 300.37/42.64 % (3127815)Instructions burned: 28122 (million) % 300.37/42.64 % (3128201)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=1835484440:i=1778:ins=1:rtra=on_2636 on theBenchmark for (2636ds/1778Mi) % 300.37/42.64 % (3128201)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.37/42.64 % (3128201)Terminated due to inappropriate strategy. % 300.37/42.64 % (3128201)------------------------------ % 300.37/42.64 % (3128201)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.37/42.64 % (3128201)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.37/42.64 % (3128201)CaDiCaL version: 2.1.3 % 300.37/42.64 % (3128201)Termination reason: Inappropriate % 300.37/42.64 % (3128201)Time elapsed: 0.003 s % 300.37/42.64 % (3128201)Peak memory usage: 10 MB % 300.37/42.64 % (3128201)Instructions burned: 4 (million) % 300.37/42.64 % (3128201)------------------------------ % 300.37/42.64 % (3128201)------------------------------ % 300.37/42.64 % (3128203)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:si=on:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=2761066676:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2635 on theBenchmark for (2635ds/1384Mi) % 300.37/42.64 % (3128199)Instruction limit reached! % 300.37/42.64 % (3128199)------------------------------ % 300.37/42.64 % (3128199)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.37/42.64 % (3128199)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.37/42.64 % (3128199)CaDiCaL version: 2.1.3 % 300.37/42.64 % (3128199)Termination reason: Instruction limit % 300.37/42.64 % (3128199)Termination phase: Saturation % 300.37/42.64 % (3128199)Time elapsed: 1.405 s % 300.37/42.64 % (3128199)Peak memory usage: 25 MB % 300.37/42.64 % (3128199)Instructions burned: 2360 (million) % 300.37/42.64 % (3128205)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=2484838151:i=1758:kws=inv_precedence:fsr=off:rtra=on_2635 on theBenchmark for (2635ds/1758Mi) % 300.37/42.64 % (3128203)Instruction limit reached! % 300.37/42.64 % (3128203)------------------------------ % 300.37/42.64 % (3128203)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.37/42.64 % (3128203)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.37/42.64 % (3128203)CaDiCaL version: 2.1.3 % 300.37/42.64 % (3128203)Termination reason: Instruction limit % 300.37/42.64 % (3128203)Termination phase: Saturation % 300.37/42.64 % (3128203)Time elapsed: 0.761 s % 300.37/42.64 % (3128203)Peak memory usage: 19 MB % 300.37/42.64 % (3128203)Instructions burned: 1386 (million) % 300.37/42.64 % (3128207)fmb+10_1_sil=64000:si=on:random_seed=2295045511:i=44122:nm=2:rtra=on:gsp=on_2628 on theBenchmark for (2628ds/44122Mi) % 300.37/42.64 % (3128207)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.37/42.64 % (3128207)Terminated due to inappropriate strategy. % 300.37/42.64 % (3128207)------------------------------ % 300.37/42.64 % (3128207)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.37/42.64 % (3128207)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.37/42.64 % (3128207)CaDiCaL version: 2.1.3 % 300.37/42.64 % (3128207)Termination reason: Inappropriate % 300.37/42.64 % (3128207)Time elapsed: 0.003 s % 300.37/42.64 % (3128207)Peak memory usage: 10 MB % 300.37/42.64 % (3128207)Instructions burned: 5 (million) % 300.37/42.64 % (3128207)------------------------------ % 300.37/42.64 % (3128207)------------------------------ % 300.37/42.64 % (3128209)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=2848947473:i=19030:nm=5:rtra=on_2627 on theBenchmark fo % 300.37/42.64 Terminated % 300.37/42.64 % Vampire exiting %------------------------------------------------------------------------------