%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWX114_1 : TPTP v9.3.1. Released v9.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n007.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:30 PM UTC 2026 % Result : Timeout 300.34s 42.54s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWX114_1 : TPTP v9.3.1. Released v9.1.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.08/0.18 % Computer : n007.cluster.edu % 0.08/0.18 % Model : x86_64 x86_64 % 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.18 % Memory : 8046.5625MB % 0.08/0.18 % OS : Linux 6.8.0-71-generic % 0.08/0.18 % CPULimit : 300 % 0.08/0.18 % WCLimit : 300 % 0.08/0.19 % DateTime : Mon Sep 28 14:59:55 UTC 2026 % 0.08/0.19 % CPUTime : % 0.08/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.08/0.22 Running first-order model finding % 0.08/0.22 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 % 2.78/0.69 % (2477254)Will run a generic schedule for satisfiability detection. % 2.78/0.69 % (2477282)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1597366639:i=116_2999 on theBenchmark for (2999ds/116Mi) % 2.78/0.69 % (2477279)% WARNING: option uhcvi not known. % 2.78/0.69 % (2477279)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=595263559:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 2.78/0.69 % (2477278)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1432671593_2999 on theBenchmark for (2999ds/0Mi) % 2.78/0.69 % (2477280)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=211412655:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 2.78/0.69 % (2477281)dis+10_1_sil=32000:sp=arity:random_seed=1507767774:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 2.78/0.69 % (2477283)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=459036508:i=131_2999 on theBenchmark for (2999ds/131Mi) % 2.78/0.69 % (2477285)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2429162768:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 2.78/0.70 % (2477278)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 2.78/0.70 % (2477278)Terminated due to inappropriate strategy. % 2.78/0.70 % (2477278)------------------------------ % 2.78/0.70 % (2477278)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.78/0.70 % (2477278)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.78/0.70 % (2477278)CaDiCaL version: 2.1.3 % 2.78/0.70 % (2477278)Termination reason: Inappropriate % 2.78/0.70 % (2477278)Time elapsed: 0.006 s % 2.78/0.70 % (2477278)Peak memory usage: 10 MB % 2.78/0.70 % (2477278)Instructions burned: 12 (million) % 2.78/0.70 % (2477278)------------------------------ % 2.78/0.70 % (2477278)------------------------------ % 2.78/0.70 % (2477282)Instruction limit reached! % 2.78/0.70 % (2477282)------------------------------ % 2.78/0.70 % (2477282)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.78/0.70 % (2477282)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.78/0.70 % (2477282)CaDiCaL version: 2.1.3 % 2.78/0.70 % (2477282)Termination reason: Instruction limit % 2.78/0.70 % (2477282)Termination phase: Saturation % 2.78/0.70 % (2477282)Time elapsed: 0.032 s % 2.78/0.70 % (2477282)Peak memory usage: 13 MB % 2.78/0.70 % (2477282)Instructions burned: 118 (million) % 2.78/0.70 % (2477300)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1843974366:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 2.78/0.70 % (2477300)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 2.78/0.70 % (2477300)Terminated due to inappropriate strategy. % 2.78/0.70 % (2477300)------------------------------ % 2.78/0.70 % (2477300)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.78/0.70 % (2477300)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.78/0.70 % (2477300)CaDiCaL version: 2.1.3 % 2.78/0.70 % (2477300)Termination reason: Inappropriate % 2.78/0.70 % (2477300)Time elapsed: 0.004 s % 2.78/0.70 % (2477300)Peak memory usage: 10 MB % 2.78/0.70 % (2477300)Instructions burned: 7 (million) % 2.78/0.70 % (2477300)------------------------------ % 2.78/0.70 % (2477300)------------------------------ % 2.78/0.70 % (2477307)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=864046022:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 2.78/0.70 % (2477312)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=3660996300:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 2.78/0.70 % (2477281)Instruction limit reached! % 2.78/0.70 % (2477281)------------------------------ % 2.78/0.70 % (2477281)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.78/0.70 % (2477281)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.78/0.70 % (2477281)CaDiCaL version: 2.1.3 % 2.78/0.70 % (2477281)Termination reason: Instruction limit % 2.78/0.70 % (2477281)Termination phase: Saturation % 2.78/0.70 % (2477281)Time elapsed: 0.054 s % 2.78/0.70 % (2477281)Peak memory usage: 13 MB % 2.78/0.70 % (2477281)Instructions burned: 103 (million) % 2.78/0.70 % (2477283)Instruction limit reached! % 2.78/0.70 % (2477283)------------------------------ % 2.78/0.70 % (2477283)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.04/0.94 % (2477283)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.04/0.94 % (2477283)CaDiCaL version: 2.1.3 % 4.04/0.94 % (2477283)Termination reason: Instruction limit % 4.04/0.94 % (2477283)Termination phase: Saturation % 4.04/0.94 % (2477283)Time elapsed: 0.069 s % 4.04/0.94 % (2477283)Peak memory usage: 13 MB % 4.04/0.94 % (2477283)Instructions burned: 131 (million) % 4.04/0.94 % (2477307)Instruction limit reached! % 4.04/0.94 % (2477307)------------------------------ % 4.04/0.94 % (2477307)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.04/0.94 % (2477307)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.04/0.94 % (2477307)CaDiCaL version: 2.1.3 % 4.04/0.94 % (2477307)Termination reason: Instruction limit % 4.04/0.94 % (2477307)Termination phase: Saturation % 4.04/0.94 % (2477307)Time elapsed: 0.039 s % 4.04/0.94 % (2477307)Peak memory usage: 13 MB % 4.04/0.94 % (2477307)Instructions burned: 131 (million) % 4.04/0.94 % (2477324)ott-21_1_sil=16000:fs=off:random_seed=1792219432:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi) % 4.04/0.94 % (2477330)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=820891518:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 4.04/0.94 % (2477330)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 4.04/0.94 % (2477330)Terminated due to inappropriate strategy. % 4.04/0.94 % (2477330)------------------------------ % 4.04/0.94 % (2477330)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.04/0.94 % (2477330)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.04/0.94 % (2477330)CaDiCaL version: 2.1.3 % 4.04/0.94 % (2477330)Termination reason: Inappropriate % 4.04/0.94 % (2477330)Time elapsed: 0.001 s % 4.04/0.94 % (2477330)Peak memory usage: 10 MB % 4.04/0.94 % (2477330)Instructions burned: 5 (million) % 4.04/0.94 % (2477330)------------------------------ % 4.04/0.94 % (2477330)------------------------------ % 4.04/0.94 % (2477328)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1011780440:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 4.04/0.94 % (2477285)Instruction limit reached! % 4.04/0.94 % (2477285)------------------------------ % 4.04/0.94 % (2477285)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.04/0.94 % (2477285)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.04/0.94 % (2477285)CaDiCaL version: 2.1.3 % 4.04/0.94 % (2477285)Termination reason: Instruction limit % 4.04/0.94 % (2477285)Termination phase: Saturation % 4.04/0.94 % (2477285)Time elapsed: 0.092 s % 4.04/0.94 % (2477285)Peak memory usage: 14 MB % 4.04/0.94 % (2477285)Instructions burned: 160 (million) % 4.04/0.94 % (2477336)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1915333711:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 4.04/0.94 % (2477342)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3345402162:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 4.04/0.94 % (2477342)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 4.04/0.94 % (2477342)Terminated due to inappropriate strategy. % 4.04/0.94 % (2477342)------------------------------ % 4.04/0.94 % (2477342)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.04/0.94 % (2477342)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.04/0.94 % (2477342)CaDiCaL version: 2.1.3 % 4.04/0.94 % (2477342)Termination reason: Inappropriate % 4.04/0.94 % (2477342)Time elapsed: 0.004 s % 4.04/0.94 % (2477342)Peak memory usage: 10 MB % 4.04/0.94 % (2477342)Instructions burned: 6 (million) % 4.04/0.94 % (2477342)------------------------------ % 4.04/0.94 % (2477342)------------------------------ % 4.04/0.94 % (2477353)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=372240535:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2998 on theBenchmark for (2998ds/692Mi) % 4.04/0.94 % (2477324)Instruction limit reached! % 4.04/0.94 % (2477324)------------------------------ % 4.04/0.94 % (2477324)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.04/0.94 % (2477324)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.04/0.94 % (2477324)CaDiCaL version: 2.1.3 % 4.04/0.94 % (2477324)Termination reason: Instruction limit % 4.04/0.94 % (2477324)Termination phase: Saturation % 16.87/2.75 % (2477324)Time elapsed: 0.086 s % 16.87/2.75 % (2477324)Peak memory usage: 13 MB % 16.87/2.75 % (2477324)Instructions burned: 181 (million) % 16.87/2.75 % (2477376)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=4197100253:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 16.87/2.75 % (2477336)Instruction limit reached! % 16.87/2.75 % (2477336)------------------------------ % 16.87/2.75 % (2477336)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.87/2.75 % (2477336)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.87/2.75 % (2477336)CaDiCaL version: 2.1.3 % 16.87/2.75 % (2477336)Termination reason: Instruction limit % 16.87/2.75 % (2477336)Termination phase: Saturation % 16.87/2.75 % (2477336)Time elapsed: 0.219 s % 16.87/2.75 % (2477336)Peak memory usage: 14 MB % 16.87/2.75 % (2477336)Instructions burned: 1183 (million) % 16.87/2.75 % (2477399)fmb+10_1_sil=64000:random_seed=783458412:i=22061:nm=2:gsp=on_2996 on theBenchmark for (2996ds/22061Mi) % 16.87/2.75 % (2477399)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 16.87/2.75 % (2477399)Terminated due to inappropriate strategy. % 16.87/2.75 % (2477399)------------------------------ % 16.87/2.75 % (2477399)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.87/2.75 % (2477399)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.87/2.75 % (2477399)CaDiCaL version: 2.1.3 % 16.87/2.75 % (2477399)Termination reason: Inappropriate % 16.87/2.75 % (2477399)Time elapsed: 0.002 s % 16.87/2.75 % (2477399)Peak memory usage: 10 MB % 16.87/2.75 % (2477399)Instructions burned: 9 (million) % 16.87/2.75 % (2477399)------------------------------ % 16.87/2.75 % (2477399)------------------------------ % 16.87/2.75 % (2477401)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2214508376:i=9515:nm=5_2996 on theBenchmark for (2996ds/9515Mi) % 16.87/2.75 % (2477401)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 16.87/2.75 % (2477401)Terminated due to inappropriate strategy. % 16.87/2.75 % (2477401)------------------------------ % 16.87/2.75 % (2477401)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.87/2.75 % (2477401)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.87/2.75 % (2477401)CaDiCaL version: 2.1.3 % 16.87/2.75 % (2477401)Termination reason: Inappropriate % 16.87/2.75 % (2477401)Time elapsed: 0.002 s % 16.87/2.75 % (2477401)Peak memory usage: 10 MB % 16.87/2.75 % (2477401)Instructions burned: 7 (million) % 16.87/2.75 % (2477401)------------------------------ % 16.87/2.75 % (2477401)------------------------------ % 16.87/2.75 % (2477403)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2664018936:fmbsr=1.7:i=920_2996 on theBenchmark for (2996ds/920Mi) % 16.87/2.75 % (2477403)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 16.87/2.75 % (2477403)Terminated due to inappropriate strategy. % 16.87/2.75 % (2477403)------------------------------ % 16.87/2.75 % (2477403)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.87/2.75 % (2477403)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.87/2.75 % (2477403)CaDiCaL version: 2.1.3 % 16.87/2.75 % (2477403)Termination reason: Inappropriate % 16.87/2.75 % (2477403)Time elapsed: 0.002 s % 16.87/2.75 % (2477403)Peak memory usage: 10 MB % 16.87/2.75 % (2477403)Instructions burned: 7 (million) % 16.87/2.75 % (2477403)------------------------------ % 16.87/2.75 % (2477403)------------------------------ % 16.87/2.75 % (2477405)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3048717483:i=5131_2995 on theBenchmark for (2995ds/5131Mi) % 16.87/2.75 % (2477328)Instruction limit reached! % 16.87/2.75 % (2477328)------------------------------ % 16.87/2.75 % (2477328)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.87/2.75 % (2477328)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.87/2.75 % (2477328)CaDiCaL version: 2.1.3 % 16.87/2.75 % (2477328)Termination reason: Instruction limit % 16.87/2.75 % (2477328)Termination phase: Saturation % 16.87/2.75 % (2477328)Time elapsed: 0.315 s % 16.87/2.75 % (2477328)Peak memory usage: 15 MB % 16.87/2.75 % (2477328)Instructions burned: 477 (million) % 16.87/2.75 % (2477312)Instruction limit reached! % 16.87/2.75 % (2477312)------------------------------ % 16.87/2.75 % (2477312)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.87/2.75 % (2477312)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.80/3.03 % (2477312)CaDiCaL version: 2.1.3 % 17.80/3.03 % (2477312)Termination reason: Instruction limit % 17.80/3.03 % (2477312)Termination phase: Saturation % 17.80/3.03 % (2477312)Time elapsed: 0.372 s % 17.80/3.03 % (2477312)Peak memory usage: 18 MB % 17.80/3.03 % (2477312)Instructions burned: 685 (million) % 17.80/3.03 % (2477407)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=922119546:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi) % 17.80/3.03 % (2477409)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=244936124:i=6324_2995 on theBenchmark for (2995ds/6324Mi) % 17.80/3.03 % (2477409)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 17.80/3.03 % (2477409)Terminated due to inappropriate strategy. % 17.80/3.03 % (2477409)------------------------------ % 17.80/3.03 % (2477409)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.80/3.03 % (2477409)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.80/3.03 % (2477409)CaDiCaL version: 2.1.3 % 17.80/3.03 % (2477409)Termination reason: Inappropriate % 17.80/3.03 % (2477409)Time elapsed: 0.006 s % 17.80/3.03 % (2477409)Peak memory usage: 11 MB % 17.80/3.03 % (2477409)Instructions burned: 12 (million) % 17.80/3.03 % (2477409)------------------------------ % 17.80/3.03 % (2477409)------------------------------ % 17.80/3.03 % (2477411)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3328895944:fmbsr=2.30978:i=2174_2995 on theBenchmark for (2995ds/2174Mi) % 17.80/3.03 % (2477411)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 17.80/3.03 % (2477411)Terminated due to inappropriate strategy. % 17.80/3.03 % (2477411)------------------------------ % 17.80/3.03 % (2477411)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.80/3.03 % (2477411)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.80/3.03 % (2477411)CaDiCaL version: 2.1.3 % 17.80/3.03 % (2477411)Termination reason: Inappropriate % 17.80/3.03 % (2477411)Time elapsed: 0.004 s % 17.80/3.03 % (2477411)Peak memory usage: 10 MB % 17.80/3.03 % (2477411)Instructions burned: 7 (million) % 17.80/3.03 % (2477411)------------------------------ % 17.80/3.03 % (2477411)------------------------------ % 17.80/3.03 % (2477413)ott-2_1_sil=16000:newcnf=on:random_seed=800607250:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2994 on theBenchmark for (2994ds/869Mi) % 17.80/3.03 % (2477353)Instruction limit reached! % 17.80/3.03 % (2477353)------------------------------ % 17.80/3.03 % (2477353)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.80/3.03 % (2477353)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.80/3.03 % (2477353)CaDiCaL version: 2.1.3 % 17.80/3.03 % (2477353)Termination reason: Instruction limit % 17.80/3.03 % (2477353)Termination phase: Saturation % 17.80/3.03 % (2477353)Time elapsed: 0.447 s % 17.80/3.03 % (2477353)Peak memory usage: 19 MB % 17.80/3.03 % (2477353)Instructions burned: 692 (million) % 17.80/3.03 % (2477415)ott+10_1_sil=32000:tgt=ground:random_seed=1438115635:i=5114:av=off_2993 on theBenchmark for (2993ds/5114Mi) % 17.80/3.03 % (2477376)Instruction limit reached! % 17.80/3.03 % (2477376)------------------------------ % 17.80/3.03 % (2477376)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.80/3.03 % (2477376)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.80/3.03 % (2477376)CaDiCaL version: 2.1.3 % 17.80/3.03 % (2477376)Termination reason: Instruction limit % 17.80/3.03 % (2477376)Termination phase: Saturation % 17.80/3.03 % (2477376)Time elapsed: 0.463 s % 17.80/3.03 % (2477376)Peak memory usage: 19 MB % 17.80/3.03 % (2477376)Instructions burned: 881 (million) % 17.80/3.03 % (2477417)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1264368031:i=54282_2993 on theBenchmark for (2993ds/54282Mi) % 17.80/3.03 % (2477417)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 17.80/3.03 % (2477417)Terminated due to inappropriate strategy. % 17.80/3.03 % (2477417)------------------------------ % 17.80/3.03 % (2477417)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.80/3.03 % (2477417)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.80/3.03 % (2477417)CaDiCaL version: 2.1.3 % 17.80/3.03 % (2477417)Termination reason: Inappropriate % 17.80/3.03 % (2477417)Time elapsed: 0.006 s % 17.80/3.03 % (2477417)Peak memory usage: 11 MB % 17.80/3.03 % (2477417)Instructions burned: 12 (million) % 60.57/8.85 % (2477417)------------------------------ % 60.57/8.85 % (2477417)------------------------------ % 60.57/8.85 % (2477419)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2157791035:i=3512:aac=none_2992 on theBenchmark for (2992ds/3512Mi) % 60.57/8.85 % (2477413)Instruction limit reached! % 60.57/8.85 % (2477413)------------------------------ % 60.57/8.85 % (2477413)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 60.57/8.85 % (2477413)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.57/8.85 % (2477413)CaDiCaL version: 2.1.3 % 60.57/8.85 % (2477413)Termination reason: Instruction limit % 60.57/8.85 % (2477413)Termination phase: Saturation % 60.57/8.85 % (2477413)Time elapsed: 0.496 s % 60.57/8.85 % (2477413)Peak memory usage: 20 MB % 60.57/8.85 % (2477413)Instructions burned: 869 (million) % 60.57/8.85 % (2477421)dis+21_1_sil=32000:sas=cadical:random_seed=1307818464:i=3773:amm=off_2989 on theBenchmark for (2989ds/3773Mi) % 60.57/8.85 % (2477407)Instruction limit reached! % 60.57/8.85 % (2477407)------------------------------ % 60.57/8.85 % (2477407)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 60.57/8.85 % (2477407)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.57/8.85 % (2477407)CaDiCaL version: 2.1.3 % 60.57/8.85 % (2477407)Termination reason: Instruction limit % 60.57/8.85 % (2477407)Termination phase: Saturation % 60.57/8.85 % (2477407)Time elapsed: 0.864 s % 60.57/8.85 % (2477407)Peak memory usage: 30 MB % 60.57/8.85 % (2477407)Instructions burned: 1473 (million) % 60.57/8.85 % (2477423)ott+11_1_sil=16000:gs=on:random_seed=2293581574:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2986 on theBenchmark for (2986ds/2251Mi) % 60.57/8.85 % (2477405)Instruction limit reached! % 60.57/8.85 % (2477405)------------------------------ % 60.57/8.85 % (2477405)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 60.57/8.85 % (2477405)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.57/8.85 % (2477405)CaDiCaL version: 2.1.3 % 60.57/8.85 % (2477405)Termination reason: Instruction limit % 60.57/8.85 % (2477405)Termination phase: Saturation % 60.57/8.85 % (2477405)Time elapsed: 1.447 s % 60.57/8.85 % (2477405)Peak memory usage: 40 MB % 60.57/8.85 % (2477405)Instructions burned: 5136 (million) % 60.57/8.85 % (2477425)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2699895990:fmbsr=1.6:i=67534_2981 on theBenchmark for (2981ds/67534Mi) % 60.57/8.85 % (2477425)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 60.57/8.85 % (2477425)Terminated due to inappropriate strategy. % 60.57/8.85 % (2477425)------------------------------ % 60.57/8.85 % (2477425)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 60.57/8.85 % (2477425)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.57/8.85 % (2477425)CaDiCaL version: 2.1.3 % 60.57/8.85 % (2477425)Termination reason: Inappropriate % 60.57/8.85 % (2477425)Time elapsed: 0.004 s % 60.57/8.85 % (2477425)Peak memory usage: 10 MB % 60.57/8.85 % (2477425)Instructions burned: 7 (million) % 60.57/8.85 % (2477425)------------------------------ % 60.57/8.85 % (2477425)------------------------------ % 60.57/8.85 % (2477427)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2492694382:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2981 on theBenchmark for (2981ds/4591Mi) % 60.57/8.85 % (2477419)Instruction limit reached! % 60.57/8.85 % (2477419)------------------------------ % 60.57/8.85 % (2477419)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 60.57/8.85 % (2477419)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.57/8.85 % (2477419)CaDiCaL version: 2.1.3 % 60.57/8.85 % (2477419)Termination reason: Instruction limit % 60.57/8.85 % (2477419)Termination phase: Saturation % 60.57/8.85 % (2477419)Time elapsed: 1.757 s % 60.57/8.85 % (2477419)Peak memory usage: 38 MB % 60.57/8.85 % (2477419)Instructions burned: 3513 (million) % 60.57/8.85 % (2477430)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2261339587:i=29340_2975 on theBenchmark for (2975ds/29340Mi) % 60.57/8.85 % (2477423)Instruction limit reached! % 60.57/8.85 % (2477423)------------------------------ % 60.57/8.85 % (2477423)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 60.57/8.85 % (2477423)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.57/8.85 % (2477423)CaDiCaL version: 2.1.3 % 60.57/8.85 % (2477423)Termination reason: Instruction limit % 106.92/15.39 % (2477423)Termination phase: Saturation % 106.92/15.39 % (2477423)Time elapsed: 1.169 s % 106.92/15.39 % (2477423)Peak memory usage: 28 MB % 106.92/15.39 % (2477423)Instructions burned: 2252 (million) % 106.92/15.39 % (2477432)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3913744397:i=5211_2974 on theBenchmark for (2974ds/5211Mi) % 106.92/15.39 % (2477421)Instruction limit reached! % 106.92/15.39 % (2477421)------------------------------ % 106.92/15.39 % (2477421)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 106.92/15.39 % (2477421)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 106.92/15.39 % (2477421)CaDiCaL version: 2.1.3 % 106.92/15.39 % (2477421)Termination reason: Instruction limit % 106.92/15.39 % (2477421)Termination phase: Saturation % 106.92/15.39 % (2477421)Time elapsed: 1.577 s % 106.92/15.39 % (2477421)Peak memory usage: 18 MB % 106.92/15.39 % (2477421)Instructions burned: 3775 (million) % 106.92/15.39 % (2477434)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3110632309:i=5497:nm=2_2973 on theBenchmark for (2973ds/5497Mi) % 106.92/15.39 % (2477434)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 106.92/15.39 % (2477434)Terminated due to inappropriate strategy. % 106.92/15.39 % (2477434)------------------------------ % 106.92/15.39 % (2477434)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 106.92/15.39 % (2477434)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 106.92/15.39 % (2477434)CaDiCaL version: 2.1.3 % 106.92/15.39 % (2477434)Termination reason: Inappropriate % 106.92/15.39 % (2477434)Time elapsed: 0.006 s % 106.92/15.39 % (2477434)Peak memory usage: 11 MB % 106.92/15.39 % (2477434)Instructions burned: 12 (million) % 106.92/15.39 % (2477434)------------------------------ % 106.92/15.39 % (2477434)------------------------------ % 106.92/15.39 % (2477436)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=263895948:fmbsr=2:i=46332_2973 on theBenchmark for (2973ds/46332Mi) % 106.92/15.39 % (2477415)Instruction limit reached! % 106.92/15.39 % (2477415)------------------------------ % 106.92/15.39 % (2477415)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 106.92/15.39 % (2477415)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 106.92/15.39 % (2477415)CaDiCaL version: 2.1.3 % 106.92/15.39 % (2477415)Termination reason: Instruction limit % 106.92/15.39 % (2477415)Termination phase: Saturation % 106.92/15.39 % (2477415)Time elapsed: 2.035 s % 106.92/15.39 % (2477415)Peak memory usage: 26 MB % 106.92/15.39 % (2477415)Instructions burned: 5116 (million) % 106.92/15.39 % (2477436)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 106.92/15.39 % (2477436)Terminated due to inappropriate strategy. % 106.92/15.39 % (2477436)------------------------------ % 106.92/15.39 % (2477436)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 106.92/15.39 % (2477436)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 106.92/15.39 % (2477436)CaDiCaL version: 2.1.3 % 106.92/15.39 % (2477436)Termination reason: Inappropriate % 106.92/15.39 % (2477436)Time elapsed: 0.004 s % 106.92/15.39 % (2477436)Peak memory usage: 11 MB % 106.92/15.39 % (2477436)Instructions burned: 7 (million) % 106.92/15.39 % (2477436)------------------------------ % 106.92/15.39 % (2477436)------------------------------ % 106.92/15.39 % (2477438)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=232632045:i=14071_2973 on theBenchmark for (2973ds/14071Mi) % 106.92/15.39 % (2477439)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1499699798:i=22565:add=on:rawr=on_2973 on theBenchmark for (2973ds/22565Mi) % 106.92/15.39 % (2477438)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 106.92/15.39 % (2477438)Terminated due to inappropriate strategy. % 106.92/15.39 % (2477438)------------------------------ % 106.92/15.39 % (2477438)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 106.92/15.39 % (2477438)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 106.92/15.39 % (2477438)CaDiCaL version: 2.1.3 % 106.92/15.39 % (2477438)Termination reason: Inappropriate % 106.92/15.39 % (2477438)Time elapsed: 0.004 s % 106.92/15.39 % (2477438)Peak memory usage: 11 MB % 106.92/15.39 % (2477438)Instructions burned: 7 (million) % 106.92/15.39 % (2477438)------------------------------ % 106.92/15.39 % (2477438)------------------------------ % 106.92/15.39 % (2477442)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=2810854329:i=8173:av=off_2972 on theBenchmark for (2972ds/8173Mi) % 106.92/15.39 % (2477427)Instruction limit reached! % 108.33/15.54 % (2477427)------------------------------ % 108.33/15.54 % (2477427)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 108.33/15.54 % (2477427)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.33/15.54 % (2477427)CaDiCaL version: 2.1.3 % 108.33/15.54 % (2477427)Termination reason: Instruction limit % 108.33/15.54 % (2477427)Termination phase: Saturation % 108.33/15.54 % (2477427)Time elapsed: 0.896 s % 108.33/15.54 % (2477427)Peak memory usage: 32 MB % 108.33/15.54 % (2477427)Instructions burned: 4596 (million) % 108.33/15.54 % (2477444)dis+10_16:1_sil=16000:random_seed=1942182:i=9155:fsr=off_2971 on theBenchmark for (2971ds/9155Mi) % 108.33/15.54 % (2477444)Instruction limit reached! % 108.33/15.54 % (2477444)------------------------------ % 108.33/15.54 % (2477444)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 108.33/15.54 % (2477444)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.33/15.54 % (2477444)CaDiCaL version: 2.1.3 % 108.33/15.54 % (2477444)Termination reason: Instruction limit % 108.33/15.54 % (2477444)Termination phase: Saturation % 108.33/15.54 % (2477444)Time elapsed: 1.605 s % 108.33/15.54 % (2477444)Peak memory usage: 19 MB % 108.33/15.54 % (2477444)Instructions burned: 9158 (million) % 108.33/15.54 % (2477447)ott-3_8_sil=64000:random_seed=1508684644:i=20139:bs=on_2955 on theBenchmark for (2955ds/20139Mi) % 108.33/15.54 % (2477432)Instruction limit reached! % 108.33/15.54 % (2477432)------------------------------ % 108.33/15.54 % (2477432)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 108.33/15.54 % (2477432)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.33/15.54 % (2477432)CaDiCaL version: 2.1.3 % 108.33/15.54 % (2477432)Termination reason: Instruction limit % 108.33/15.54 % (2477432)Termination phase: Saturation % 108.33/15.54 % (2477432)Time elapsed: 2.331 s % 108.33/15.54 % (2477432)Peak memory usage: 33 MB % 108.33/15.54 % (2477432)Instructions burned: 5213 (million) % 108.33/15.54 % (2477449)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=4182734617:fmbsr=2:i=32576_2951 on theBenchmark for (2951ds/32576Mi) % 108.33/15.54 % (2477449)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 108.33/15.54 % (2477449)Terminated due to inappropriate strategy. % 108.33/15.54 % (2477449)------------------------------ % 108.33/15.54 % (2477449)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 108.33/15.54 % (2477449)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.33/15.54 % (2477449)CaDiCaL version: 2.1.3 % 108.33/15.54 % (2477449)Termination reason: Inappropriate % 108.33/15.54 % (2477449)Time elapsed: 0.006 s % 108.33/15.54 % (2477449)Peak memory usage: 11 MB % 108.33/15.54 % (2477449)Instructions burned: 12 (million) % 108.33/15.54 % (2477449)------------------------------ % 108.33/15.54 % (2477449)------------------------------ % 108.33/15.54 % (2477451)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=1238653774:i=11404_2950 on theBenchmark for (2950ds/11404Mi) % 108.33/15.54 % (2477442)Instruction limit reached! % 108.33/15.54 % (2477442)------------------------------ % 108.33/15.54 % (2477442)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 108.33/15.54 % (2477442)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.33/15.54 % (2477442)CaDiCaL version: 2.1.3 % 108.33/15.54 % (2477442)Termination reason: Instruction limit % 108.33/15.54 % (2477442)Termination phase: Saturation % 108.33/15.55 % (2477442)Time elapsed: 3.654 s % 108.33/15.55 % (2477442)Peak memory usage: 29 MB % 108.33/15.55 % (2477442)Instructions burned: 8173 (million) % 108.33/15.55 % (2477453)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=144583028:i=14134_2936 on theBenchmark for (2936ds/14134Mi) % 108.33/15.55 % (2477447)Instruction limit reached! % 108.33/15.55 % (2477447)------------------------------ % 108.33/15.55 % (2477447)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 108.33/15.55 % (2477447)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.33/15.55 % (2477447)CaDiCaL version: 2.1.3 % 108.33/15.55 % (2477447)Termination reason: Instruction limit % 108.33/15.55 % (2477447)Termination phase: Saturation % 108.33/15.55 % (2477447)Time elapsed: 3.931 s % 108.33/15.55 % (2477447)Peak memory usage: 26 MB % 108.33/15.55 % (2477447)Instructions burned: 20145 (million) % 108.33/15.55 % (2477455)dis+33_16_sil=32000:sac=on:random_seed=1219808306:i=15851:nm=0_2916 on theBenchmark for (2916ds/15851Mi) % 108.33/15.55 % (2477451)Instruction limit reached! % 108.33/15.55 % (2477451)------------------------------ % 108.33/15.55 % (2477451)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 171.61/24.41 % (2477451)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 171.61/24.41 % (2477451)CaDiCaL version: 2.1.3 % 171.61/24.41 % (2477451)Termination reason: Instruction limit % 171.61/24.41 % (2477451)Termination phase: Saturation % 171.61/24.41 % (2477451)Time elapsed: 3.700 s % 171.61/24.41 % (2477451)Peak memory usage: 19 MB % 171.61/24.41 % (2477451)Instructions burned: 11407 (million) % 171.61/24.41 % (2477457)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=1492213510:avsq=on:i=17627:add=on:amm=off_2913 on theBenchmark for (2913ds/17627Mi) % 171.61/24.41 % (2477455)Instruction limit reached! % 171.61/24.41 % (2477455)------------------------------ % 171.61/24.41 % (2477455)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 171.61/24.41 % (2477455)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 171.61/24.41 % (2477455)CaDiCaL version: 2.1.3 % 171.61/24.41 % (2477455)Termination reason: Instruction limit % 171.61/24.41 % (2477455)Termination phase: Saturation % 171.61/24.41 % (2477455)Time elapsed: 3.402 s % 171.61/24.41 % (2477455)Peak memory usage: 56 MB % 171.61/24.41 % (2477455)Instructions burned: 15851 (million) % 171.61/24.41 % (2477459)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=3996469959:s2a=on:i=53295_2882 on theBenchmark for (2882ds/53295Mi) % 171.61/24.41 % (2477439)Instruction limit reached! % 171.61/24.41 % (2477439)------------------------------ % 171.61/24.41 % (2477439)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 171.61/24.41 % (2477439)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 171.61/24.41 % (2477439)CaDiCaL version: 2.1.3 % 171.61/24.41 % (2477439)Termination reason: Instruction limit % 171.61/24.41 % (2477439)Termination phase: Saturation % 171.61/24.41 % (2477439)Time elapsed: 9.546 s % 171.61/24.41 % (2477439)Peak memory usage: 79 MB % 171.61/24.41 % (2477439)Instructions burned: 22566 (million) % 171.61/24.41 % (2477461)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=957742577:i=26857:ins=20_2877 on theBenchmark for (2877ds/26857Mi) % 171.61/24.41 % (2477461)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 171.61/24.41 % (2477461)Terminated due to inappropriate strategy. % 171.61/24.41 % (2477461)------------------------------ % 171.61/24.41 % (2477461)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 171.61/24.41 % (2477461)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 171.61/24.41 % (2477461)CaDiCaL version: 2.1.3 % 171.61/24.41 % (2477461)Termination reason: Inappropriate % 171.61/24.41 % (2477461)Time elapsed: 0.004 s % 171.61/24.41 % (2477461)Peak memory usage: 10 MB % 171.61/24.41 % (2477461)Instructions burned: 7 (million) % 171.61/24.41 % (2477461)------------------------------ % 171.61/24.41 % (2477461)------------------------------ % 171.61/24.41 % (2477463)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=2324935987:i=28120:bs=on:fsr=off_2877 on theBenchmark for (2877ds/28120Mi) % 171.61/24.41 % (2477453)Instruction limit reached! % 171.61/24.41 % (2477453)------------------------------ % 171.61/24.41 % (2477453)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 171.61/24.41 % (2477453)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 171.61/24.41 % (2477453)CaDiCaL version: 2.1.3 % 171.61/24.41 % (2477453)Termination reason: Instruction limit % 171.61/24.41 % (2477453)Termination phase: Saturation % 171.61/24.41 % (2477453)Time elapsed: 8.698 s % 171.61/24.41 % (2477453)Peak memory usage: 71 MB % 171.61/24.41 % (2477453)Instructions burned: 14134 (million) % 171.61/24.41 % (2477733)fmb+10_1_sil=256000:fmbss=7:random_seed=2489145867:fmbsr=1.6:i=182295_2848 on theBenchmark for (2848ds/182295Mi) % 171.61/24.41 % (2477733)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 171.61/24.41 % (2477733)Terminated due to inappropriate strategy. % 171.61/24.41 % (2477733)------------------------------ % 171.61/24.41 % (2477733)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 171.61/24.41 % (2477733)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 171.61/24.41 % (2477733)CaDiCaL version: 2.1.3 % 171.61/24.41 % (2477733)Termination reason: Inappropriate % 171.61/24.41 % (2477733)Time elapsed: 0.004 s % 171.61/24.41 % (2477733)Peak memory usage: 10 MB % 171.61/24.41 % (2477733)Instructions burned: 7 (million) % 171.61/24.41 % (2477733)------------------------------ % 171.61/24.41 % (2477733)------------------------------ % 171.61/24.41 % (2477735)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=2724433758:i=44625:gsp=on_2848 on theBenchmark for (2848ds/44625Mi) % 193.66/27.51 % (2477735)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 193.66/27.51 % (2477735)Terminated due to inappropriate strategy. % 193.66/27.51 % (2477735)------------------------------ % 193.66/27.51 % (2477735)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 193.66/27.51 % (2477735)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 193.66/27.51 % (2477735)CaDiCaL version: 2.1.3 % 193.66/27.51 % (2477735)Termination reason: Inappropriate % 193.66/27.51 % (2477735)Time elapsed: 0.005 s % 193.66/27.51 % (2477735)Peak memory usage: 11 MB % 193.66/27.51 % (2477735)Instructions burned: 9 (million) % 193.66/27.51 % (2477735)------------------------------ % 193.66/27.51 % (2477735)------------------------------ % 193.66/27.51 % (2477737)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=2160968099:i=160505_2848 on theBenchmark for (2848ds/160505Mi) % 193.66/27.51 % (2477737)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 193.66/27.51 % (2477737)Terminated due to inappropriate strategy. % 193.66/27.51 % (2477737)------------------------------ % 193.66/27.51 % (2477737)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 193.66/27.51 % (2477737)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 193.66/27.51 % (2477737)CaDiCaL version: 2.1.3 % 193.66/27.51 % (2477737)Termination reason: Inappropriate % 193.66/27.51 % (2477737)Time elapsed: 0.004 s % 193.66/27.51 % (2477737)Peak memory usage: 11 MB % 193.66/27.51 % (2477737)Instructions burned: 7 (million) % 193.66/27.51 % (2477737)------------------------------ % 193.66/27.51 % (2477737)------------------------------ % 193.66/27.51 % (2477739)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=2174208162:fmbsr=1.3:i=225729_2847 on theBenchmark for (2847ds/225729Mi) % 193.66/27.51 % (2477739)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 193.66/27.51 % (2477739)Terminated due to inappropriate strategy. % 193.66/27.51 % (2477739)------------------------------ % 193.66/27.51 % (2477739)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 193.66/27.51 % (2477739)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 193.66/27.51 % (2477739)CaDiCaL version: 2.1.3 % 193.66/27.51 % (2477739)Termination reason: Inappropriate % 193.66/27.51 % (2477739)Time elapsed: 0.004 s % 193.66/27.51 % (2477739)Peak memory usage: 11 MB % 193.66/27.51 % (2477739)Instructions burned: 7 (million) % 193.66/27.51 % (2477739)------------------------------ % 193.66/27.51 % (2477739)------------------------------ % 193.66/27.51 % (2477741)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=1701829028:fmbsr=2:i=185024:ins=7_2847 on theBenchmark for (2847ds/185024Mi) % 193.66/27.51 % (2477741)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 193.66/27.51 % (2477741)Terminated due to inappropriate strategy. % 193.66/27.51 % (2477741)------------------------------ % 193.66/27.51 % (2477741)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 193.66/27.51 % (2477741)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 193.66/27.51 % (2477741)CaDiCaL version: 2.1.3 % 193.66/27.51 % (2477741)Termination reason: Inappropriate % 193.66/27.51 % (2477741)Time elapsed: 0.004 s % 193.66/27.51 % (2477741)Peak memory usage: 11 MB % 193.66/27.51 % (2477741)Instructions burned: 7 (million) % 193.66/27.51 % (2477741)------------------------------ % 193.66/27.51 % (2477741)------------------------------ % 193.66/27.51 % (2477743)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=327025713:rtra=on_2847 on theBenchmark for (2847ds/0Mi) % 193.66/27.51 % (2477743)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 193.66/27.51 % (2477743)Terminated due to inappropriate strategy. % 193.66/27.51 % (2477743)------------------------------ % 193.66/27.51 % (2477743)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 193.66/27.51 % (2477743)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 193.66/27.51 % (2477743)CaDiCaL version: 2.1.3 % 193.66/27.51 % (2477743)Termination reason: Inappropriate % 193.66/27.51 % (2477743)Time elapsed: 0.006 s % 193.66/27.51 % (2477743)Peak memory usage: 11 MB % 193.66/27.51 % (2477743)Instructions burned: 11 (million) % 193.66/27.51 % (2477743)------------------------------ % 193.66/27.51 % (2477743)------------------------------ % 193.66/27.51 % (2477745)% WARNING: option uhcvi not known. % 193.66/27.51 % (2477745)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3672946166:i=271062:add=off:rtra=on:rawr=on_2847 on theBenchmark for (2847ds/271062Mi) % 207.02/29.44 % (2477430)Instruction limit reached! % 207.02/29.44 % (2477430)------------------------------ % 207.02/29.44 % (2477430)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 207.02/29.44 % (2477430)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 207.02/29.44 % (2477430)CaDiCaL version: 2.1.3 % 207.02/29.44 % (2477430)Termination reason: Instruction limit % 207.02/29.44 % (2477430)Termination phase: Saturation % 207.02/29.44 % (2477430)Time elapsed: 13.682 s % 207.02/29.44 % (2477430)Peak memory usage: 112 MB % 207.02/29.44 % (2477430)Instructions burned: 29342 (million) % 207.02/29.44 % (2477771)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2612669451:i=176048:add=on:rtra=on:rawr=on_2837 on theBenchmark for (2837ds/176048Mi) % 207.02/29.44 % (2477457)Instruction limit reached! % 207.02/29.44 % (2477457)------------------------------ % 207.02/29.44 % (2477457)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 207.02/29.44 % (2477457)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 207.02/29.44 % (2477457)CaDiCaL version: 2.1.3 % 207.02/29.44 % (2477457)Termination reason: Instruction limit % 207.02/29.44 % (2477457)Termination phase: Saturation % 207.02/29.44 % (2477457)Time elapsed: 14.432 s % 207.02/29.44 % (2477457)Peak memory usage: 97 MB % 207.02/29.44 % (2477457)Instructions burned: 17627 (million) % 207.02/29.44 % (2477938)dis+10_1_sil=32000:si=on:sp=arity:random_seed=3394487821:i=206:fgj=on:rtra=on_2768 on theBenchmark for (2768ds/206Mi) % 207.02/29.44 % (2477938)Instruction limit reached! % 207.02/29.44 % (2477938)------------------------------ % 207.02/29.44 % (2477938)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 207.02/29.44 % (2477938)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 207.02/29.44 % (2477938)CaDiCaL version: 2.1.3 % 207.02/29.44 % (2477938)Termination reason: Instruction limit % 207.02/29.44 % (2477938)Termination phase: Saturation % 207.02/29.44 % (2477938)Time elapsed: 0.179 s % 207.02/29.44 % (2477938)Peak memory usage: 13 MB % 207.02/29.44 % (2477938)Instructions burned: 206 (million) % 207.02/29.44 % (2477945)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=3194166246:i=232:rtra=on_2766 on theBenchmark for (2766ds/232Mi) % 207.02/29.44 % (2477945)Instruction limit reached! % 207.02/29.44 % (2477945)------------------------------ % 207.02/29.44 % (2477945)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 207.02/29.44 % (2477945)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 207.02/29.44 % (2477945)CaDiCaL version: 2.1.3 % 207.02/29.44 % (2477945)Termination reason: Instruction limit % 207.02/29.44 % (2477945)Termination phase: Saturation % 207.02/29.44 % (2477945)Time elapsed: 0.192 s % 207.02/29.44 % (2477945)Peak memory usage: 13 MB % 207.02/29.44 % (2477945)Instructions burned: 232 (million) % 207.02/29.44 % (2477950)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=3649392584:i=262:rtra=on_2764 on theBenchmark for (2764ds/262Mi) % 207.02/29.44 % (2477950)Instruction limit reached! % 207.02/29.44 % (2477950)------------------------------ % 207.02/29.44 % (2477950)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 207.02/29.44 % (2477950)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 207.02/29.44 % (2477950)CaDiCaL version: 2.1.3 % 207.02/29.44 % (2477950)Termination reason: Instruction limit % 207.02/29.44 % (2477950)Termination phase: Saturation % 207.02/29.44 % (2477950)Time elapsed: 0.199 s % 207.02/29.44 % (2477950)Peak memory usage: 14 MB % 207.02/29.44 % (2477950)Instructions burned: 262 (million) % 207.02/29.44 % (2477952)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=2314859391:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2761 on theBenchmark for (2761ds/318Mi) % 207.02/29.44 % (2477952)Instruction limit reached! % 207.02/29.44 % (2477952)------------------------------ % 207.02/29.44 % (2477952)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 207.02/29.44 % (2477952)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 207.02/29.44 % (2477952)CaDiCaL version: 2.1.3 % 207.02/29.44 % (2477952)Termination reason: Instruction limit % 207.02/29.44 % (2477952)Termination phase: Saturation % 207.02/29.44 % (2477952)Time elapsed: 0.311 s % 207.02/29.44 % (2477952)Peak memory usage: 16 MB % 207.02/29.44 % (2477952)Instructions burned: 319 (million) % 207.02/29.44 % (2477955)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=2437236934:i=1428:nm=2:rtra=on_2758 on theBenchmark for (2758ds/1428Mi) % 241.28/34.21 % (2477955)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 241.28/34.21 % (2477955)Terminated due to inappropriate strategy. % 241.28/34.21 % (2477955)------------------------------ % 241.28/34.21 % (2477955)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 241.28/34.21 % (2477955)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 241.28/34.21 % (2477955)CaDiCaL version: 2.1.3 % 241.28/34.21 % (2477955)Termination reason: Inappropriate % 241.28/34.21 % (2477955)Time elapsed: 0.007 s % 241.28/34.21 % (2477955)Peak memory usage: 10 MB % 241.28/34.21 % (2477955)Instructions burned: 8 (million) % 241.28/34.21 % (2477955)------------------------------ % 241.28/34.21 % (2477955)------------------------------ % 241.28/34.21 % (2477959)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=4032923480:i=262:bd=preordered:rtra=on:fsd=on_2758 on theBenchmark for (2758ds/262Mi) % 241.28/34.21 % (2477959)Instruction limit reached! % 241.28/34.21 % (2477959)------------------------------ % 241.28/34.21 % (2477959)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 241.28/34.21 % (2477959)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 241.28/34.21 % (2477959)CaDiCaL version: 2.1.3 % 241.28/34.21 % (2477959)Termination reason: Instruction limit % 241.28/34.21 % (2477959)Termination phase: Saturation % 241.28/34.21 % (2477959)Time elapsed: 0.262 s % 241.28/34.21 % (2477959)Peak memory usage: 14 MB % 241.28/34.21 % (2477959)Instructions burned: 262 (million) % 241.28/34.21 % (2477963)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=1736279982:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2754 on theBenchmark for (2754ds/1368Mi) % 241.28/34.21 % (2477963)Instruction limit reached! % 241.28/34.21 % (2477963)------------------------------ % 241.28/34.21 % (2477963)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 241.28/34.21 % (2477963)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 241.28/34.21 % (2477963)CaDiCaL version: 2.1.3 % 241.28/34.21 % (2477963)Termination reason: Instruction limit % 241.28/34.21 % (2477963)Termination phase: Saturation % 241.28/34.21 % (2477963)Time elapsed: 1.303 s % 241.28/34.21 % (2477963)Peak memory usage: 19 MB % 241.28/34.21 % (2477963)Instructions burned: 1368 (million) % 241.28/34.21 % (2477972)ott-21_1_sil=16000:si=on:fs=off:random_seed=2229075510:i=360:av=off:fsr=off:rtra=on_2741 on theBenchmark for (2741ds/360Mi) % 241.28/34.21 % (2477972)Instruction limit reached! % 241.28/34.21 % (2477972)------------------------------ % 241.28/34.21 % (2477972)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 241.28/34.21 % (2477972)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 241.28/34.21 % (2477972)CaDiCaL version: 2.1.3 % 241.28/34.21 % (2477972)Termination reason: Instruction limit % 241.28/34.21 % (2477972)Termination phase: Saturation % 241.28/34.21 % (2477972)Time elapsed: 0.272 s % 241.28/34.21 % (2477972)Peak memory usage: 13 MB % 241.28/34.21 % (2477972)Instructions burned: 361 (million) % 241.28/34.21 % (2477975)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=252353955:i=954:bd=all:rtra=on_2738 on theBenchmark for (2738ds/954Mi) % 241.28/34.21 % (2477975)Instruction limit reached! % 241.28/34.21 % (2477975)------------------------------ % 241.28/34.21 % (2477975)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 241.28/34.22 % (2477975)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 241.28/34.22 % (2477975)CaDiCaL version: 2.1.3 % 241.28/34.22 % (2477975)Termination reason: Instruction limit % 241.28/34.22 % (2477975)Termination phase: Saturation % 241.28/34.22 % (2477975)Time elapsed: 1.064 s % 241.28/34.22 % (2477975)Peak memory usage: 17 MB % 241.28/34.22 % (2477975)Instructions burned: 955 (million) % 241.28/34.22 % (2477984)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=3589037616:fmbsr=1.3:i=1730:ins=25:rtra=on_2727 on theBenchmark for (2727ds/1730Mi) % 241.28/34.22 % (2477984)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 241.28/34.22 % (2477984)Terminated due to inappropriate strategy. % 241.28/34.22 % (2477984)------------------------------ % 241.28/34.22 % (2477984)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 241.28/34.22 % (2477984)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 241.28/34.22 % (2477984)CaDiCaL version: 2.1.3 % 241.28/34.22 % (2477984)Termination reason: Inappropriate % 241.28/34.22 % (2477984)Time elapsed: 0.008 s % 268.61/38.07 % (2477984)Peak memory usage: 10 MB % 268.61/38.07 % (2477984)Instructions burned: 5 (million) % 268.61/38.07 % (2477984)------------------------------ % 268.61/38.07 % (2477984)------------------------------ % 268.61/38.07 % (2477986)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=2448156236:i=2358:rtra=on_2727 on theBenchmark for (2727ds/2358Mi) % 268.61/38.07 % (2477463)Instruction limit reached! % 268.61/38.07 % (2477463)------------------------------ % 268.61/38.07 % (2477463)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 268.61/38.07 % (2477463)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 268.61/38.07 % (2477463)CaDiCaL version: 2.1.3 % 268.61/38.07 % (2477463)Termination reason: Instruction limit % 268.61/38.07 % (2477463)Termination phase: Saturation % 268.61/38.07 % (2477463)Time elapsed: 15.375 s % 268.61/38.07 % (2477463)Peak memory usage: 27 MB % 268.61/38.07 % (2477463)Instructions burned: 28121 (million) % 268.61/38.07 % (2477988)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=4258884463:i=1778:ins=1:rtra=on_2723 on theBenchmark for (2723ds/1778Mi) % 268.61/38.07 % (2477988)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 268.61/38.07 % (2477988)Terminated due to inappropriate strategy. % 268.61/38.07 % (2477988)------------------------------ % 268.61/38.07 % (2477988)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 268.61/38.07 % (2477988)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 268.61/38.07 % (2477988)CaDiCaL version: 2.1.3 % 268.61/38.07 % (2477988)Termination reason: Inappropriate % 268.61/38.07 % (2477988)Time elapsed: 0.005 s % 268.61/38.07 % (2477988)Peak memory usage: 10 MB % 268.61/38.07 % (2477988)Instructions burned: 7 (million) % 268.61/38.07 % (2477988)------------------------------ % 268.61/38.07 % (2477988)------------------------------ % 268.61/38.07 % (2477990)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=141811478:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2722 on theBenchmark for (2722ds/1384Mi) % 268.61/38.07 % (2477986)Instruction limit reached! % 268.61/38.07 % (2477986)------------------------------ % 268.61/38.07 % (2477986)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 268.61/38.07 % (2477986)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 268.61/38.07 % (2477986)CaDiCaL version: 2.1.3 % 268.61/38.07 % (2477986)Termination reason: Instruction limit % 268.61/38.07 % (2477986)Termination phase: Saturation % 268.61/38.07 % (2477986)Time elapsed: 1.761 s % 268.61/38.07 % (2477986)Peak memory usage: 19 MB % 268.61/38.07 % (2477986)Instructions burned: 2359 (million) % 268.61/38.07 % (2478000)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=1688370668:i=1758:kws=inv_precedence:fsr=off:rtra=on_2709 on theBenchmark for (2709ds/1758Mi) % 268.61/38.07 % (2477990)Instruction limit reached! % 268.61/38.07 % (2477990)------------------------------ % 268.61/38.07 % (2477990)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 268.61/38.07 % (2477990)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 268.61/38.07 % (2477990)CaDiCaL version: 2.1.3 % 268.61/38.07 % (2477990)Termination reason: Instruction limit % 268.61/38.07 % (2477990)Termination phase: Saturation % 268.61/38.07 % (2477990)Time elapsed: 1.370 s % 268.61/38.07 % (2477990)Peak memory usage: 24 MB % 268.61/38.07 % (2477990)Instructions burned: 1384 (million) % 268.61/38.07 % (2478002)fmb+10_1_sil=64000:si=on:random_seed=936021396:i=44122:nm=2:rtra=on:gsp=on_2708 on theBenchmark for (2708ds/44122Mi) % 268.61/38.07 % (2478002)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 268.61/38.07 % (2478002)Terminated due to inappropriate strategy. % 268.61/38.07 % (2478002)------------------------------ % 268.61/38.07 % (2478002)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 268.61/38.07 % (2478002)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 268.61/38.07 % (2478002)CaDiCaL version: 2.1.3 % 268.61/38.07 % (2478002)Termination reason: Inappropriate % 268.61/38.07 % (2478002)Time elapsed: 0.010 s % 268.61/38.07 % (2478002)Peak memory usage: 10 MB % 268.61/38.07 % (2478002)Instructions burned: 10 (million) % 268.61/38.07 % (2478002)------------------------------ % 268.61/38.07 % (2478002)------------------------------ % 268.61/38.07 % (2478004)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=483093866:i=19030:nm=5:rtra=on_2708 on theBenchmark Terminated % 300.34/42.54 % Vampire exiting %------------------------------------------------------------------------------