%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWC453_1 : TPTP v9.3.1. Released v9.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n006.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:06:01 PM UTC 2026 % Result : Timeout 300.64s 42.54s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWC453_1 : TPTP v9.3.1. Released v9.0.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.08/0.21 % Computer : n006.cluster.edu % 0.08/0.21 % Model : x86_64 x86_64 % 0.08/0.21 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.21 % Memory : 8046.5625MB % 0.08/0.21 % OS : Linux 6.8.0-71-generic % 0.08/0.21 % CPULimit : 300 % 0.08/0.21 % WCLimit : 300 % 0.08/0.21 % DateTime : Mon Sep 28 09:38:19 UTC 2026 % 0.08/0.21 % CPUTime : % 0.08/0.21 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.08/0.24 Running first-order model finding % 0.08/0.24 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 % 4.06/0.90 % (3843753)Will run a generic schedule for satisfiability detection. % 4.06/0.90 % (3843762)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1243547135:i=116_2999 on theBenchmark for (2999ds/116Mi) % 4.06/0.90 % (3843759)% WARNING: option uhcvi not known. % 4.06/0.90 % (3843761)dis+10_1_sil=32000:sp=arity:random_seed=220419694:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 4.06/0.90 % (3843760)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3725594403:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 4.06/0.90 % (3843758)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=143806276_2999 on theBenchmark for (2999ds/0Mi) % 4.06/0.90 % (3843759)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3452644648:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 4.06/0.90 % (3843764)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1740651872:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 4.06/0.90 % (3843763)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=862548020:i=131_2999 on theBenchmark for (2999ds/131Mi) % 4.06/0.90 % (3843758)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 4.06/0.90 % (3843758)Terminated due to inappropriate strategy. % 4.06/0.90 % (3843758)------------------------------ % 4.06/0.90 % (3843758)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.06/0.90 % (3843758)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.06/0.90 % (3843758)CaDiCaL version: 2.1.3 % 4.06/0.90 % (3843758)Termination reason: Inappropriate % 4.06/0.90 % (3843758)Time elapsed: 0.001 s % 4.06/0.90 % (3843758)Peak memory usage: 10 MB % 4.06/0.90 % (3843758)Instructions burned: 1 (million) % 4.06/0.90 % (3843758)------------------------------ % 4.06/0.90 % (3843758)------------------------------ % 4.06/0.90 % (3843772)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3987263334:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 4.06/0.90 % (3843772)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 4.06/0.90 % (3843772)Terminated due to inappropriate strategy. % 4.06/0.90 % (3843772)------------------------------ % 4.06/0.90 % (3843772)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.06/0.90 % (3843772)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.06/0.90 % (3843772)CaDiCaL version: 2.1.3 % 4.06/0.90 % (3843772)Termination reason: Inappropriate % 4.06/0.90 % (3843772)Time elapsed: 0.001 s % 4.06/0.90 % (3843772)Peak memory usage: 11 MB % 4.06/0.90 % (3843772)Instructions burned: 1 (million) % 4.06/0.90 % (3843772)------------------------------ % 4.06/0.90 % (3843772)------------------------------ % 4.06/0.90 % (3843762)Instruction limit reached! % 4.06/0.90 % (3843762)------------------------------ % 4.06/0.90 % (3843762)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.06/0.90 % (3843762)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.06/0.90 % (3843762)CaDiCaL version: 2.1.3 % 4.06/0.90 % (3843762)Termination reason: Instruction limit % 4.06/0.90 % (3843762)Termination phase: Saturation % 4.06/0.90 % (3843762)Time elapsed: 0.041 s % 4.06/0.90 % (3843762)Peak memory usage: 12 MB % 4.06/0.90 % (3843762)Instructions burned: 118 (million) % 4.06/0.90 % (3843779)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2824146457:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 4.06/0.90 % (3843782)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=242037762:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 4.06/0.90 % (3843761)Instruction limit reached! % 4.06/0.90 % (3843761)------------------------------ % 4.06/0.90 % (3843761)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.06/0.90 % (3843761)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.06/0.90 % (3843761)CaDiCaL version: 2.1.3 % 4.06/0.90 % (3843761)Termination reason: Instruction limit % 4.06/0.90 % (3843761)Termination phase: Saturation % 4.06/0.90 % (3843761)Time elapsed: 0.065 s % 4.06/0.90 % (3843761)Peak memory usage: 12 MB % 4.06/0.90 % (3843761)Instructions burned: 104 (million) % 4.06/0.90 % (3843763)Instruction limit reached! % 4.06/0.90 % (3843763)------------------------------ % 4.06/0.90 % (3843763)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.42/1.33 % (3843763)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.42/1.33 % (3843763)CaDiCaL version: 2.1.3 % 7.42/1.33 % (3843763)Termination reason: Instruction limit % 7.42/1.33 % (3843763)Termination phase: Saturation % 7.42/1.33 % (3843763)Time elapsed: 0.081 s % 7.42/1.33 % (3843763)Peak memory usage: 13 MB % 7.42/1.33 % (3843763)Instructions burned: 131 (million) % 7.42/1.33 % (3843787)ott-21_1_sil=16000:fs=off:random_seed=523491916:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi) % 7.42/1.33 % (3843789)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=4207454645:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 7.42/1.33 % (3843764)Instruction limit reached! % 7.42/1.33 % (3843764)------------------------------ % 7.42/1.33 % (3843764)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.42/1.33 % (3843764)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.42/1.33 % (3843764)CaDiCaL version: 2.1.3 % 7.42/1.33 % (3843764)Termination reason: Instruction limit % 7.42/1.33 % (3843764)Termination phase: Saturation % 7.42/1.33 % (3843764)Time elapsed: 0.111 s % 7.42/1.33 % (3843764)Peak memory usage: 13 MB % 7.42/1.33 % (3843764)Instructions burned: 160 (million) % 7.42/1.33 % (3843797)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=848654516:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 7.42/1.33 % (3843797)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 7.42/1.33 % (3843797)Terminated due to inappropriate strategy. % 7.42/1.33 % (3843797)------------------------------ % 7.42/1.33 % (3843797)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.42/1.33 % (3843797)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.42/1.33 % (3843797)CaDiCaL version: 2.1.3 % 7.42/1.33 % (3843797)Termination reason: Inappropriate % 7.42/1.33 % (3843797)Time elapsed: 0.001 s % 7.42/1.33 % (3843797)Peak memory usage: 10 MB % 7.42/1.33 % (3843797)Instructions burned: 1 (million) % 7.42/1.33 % (3843797)------------------------------ % 7.42/1.33 % (3843797)------------------------------ % 7.42/1.33 % (3843779)Instruction limit reached! % 7.42/1.33 % (3843779)------------------------------ % 7.42/1.33 % (3843779)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.42/1.33 % (3843779)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.42/1.33 % (3843779)CaDiCaL version: 2.1.3 % 7.42/1.33 % (3843779)Termination reason: Instruction limit % 7.42/1.33 % (3843779)Termination phase: Saturation % 7.42/1.33 % (3843779)Time elapsed: 0.090 s % 7.42/1.33 % (3843779)Peak memory usage: 12 MB % 7.42/1.33 % (3843779)Instructions burned: 132 (million) % 7.42/1.33 % (3843805)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2918299203:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 7.42/1.33 % (3843806)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3295013708:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 7.42/1.33 % (3843806)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 7.42/1.33 % (3843806)Terminated due to inappropriate strategy. % 7.42/1.33 % (3843806)------------------------------ % 7.42/1.33 % (3843806)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.42/1.33 % (3843806)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.42/1.33 % (3843806)CaDiCaL version: 2.1.3 % 7.42/1.33 % (3843806)Termination reason: Inappropriate % 7.42/1.33 % (3843806)Time elapsed: 0.001 s % 7.42/1.33 % (3843806)Peak memory usage: 10 MB % 7.42/1.33 % (3843806)Instructions burned: 1 (million) % 7.42/1.33 % (3843806)------------------------------ % 7.42/1.33 % (3843806)------------------------------ % 7.42/1.33 % (3843787)Instruction limit reached! % 7.42/1.33 % (3843787)------------------------------ % 7.42/1.33 % (3843787)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.42/1.33 % (3843787)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.42/1.33 % (3843787)CaDiCaL version: 2.1.3 % 7.42/1.33 % (3843787)Termination reason: Instruction limit % 7.42/1.33 % (3843787)Termination phase: Saturation % 7.42/1.33 % (3843787)Time elapsed: 0.079 s % 7.42/1.33 % (3843787)Peak memory usage: 12 MB % 7.42/1.33 % (3843787)Instructions burned: 181 (million) % 7.42/1.33 % (3843813)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=3753365792: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) % 28.80/4.31 % (3843817)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3243686136:i=879:kws=inv_precedence:fsr=off_2998 on theBenchmark for (2998ds/879Mi) % 28.80/4.31 % (3843782)Instruction limit reached! % 28.80/4.31 % (3843782)------------------------------ % 28.80/4.31 % (3843782)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.80/4.31 % (3843782)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.80/4.31 % (3843782)CaDiCaL version: 2.1.3 % 28.80/4.31 % (3843782)Termination reason: Instruction limit % 28.80/4.31 % (3843782)Termination phase: Saturation % 28.80/4.31 % (3843782)Time elapsed: 0.185 s % 28.80/4.31 % (3843782)Peak memory usage: 17 MB % 28.80/4.31 % (3843782)Instructions burned: 684 (million) % 28.80/4.31 % (3843832)fmb+10_1_sil=64000:random_seed=1404672574:i=22061:nm=2:gsp=on_2997 on theBenchmark for (2997ds/22061Mi) % 28.80/4.31 % (3843832)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 28.80/4.31 % (3843832)Terminated due to inappropriate strategy. % 28.80/4.31 % (3843832)------------------------------ % 28.80/4.31 % (3843832)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.80/4.31 % (3843832)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.80/4.31 % (3843832)CaDiCaL version: 2.1.3 % 28.80/4.31 % (3843832)Termination reason: Inappropriate % 28.80/4.31 % (3843832)Time elapsed: 0.0000 s % 28.80/4.31 % (3843832)Peak memory usage: 10 MB % 28.80/4.31 % (3843832)Instructions burned: 1 (million) % 28.80/4.31 % (3843832)------------------------------ % 28.80/4.31 % (3843832)------------------------------ % 28.80/4.31 % (3843836)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3395985927:i=9515:nm=5_2997 on theBenchmark for (2997ds/9515Mi) % 28.80/4.31 % (3843836)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 28.80/4.31 % (3843836)Terminated due to inappropriate strategy. % 28.80/4.31 % (3843836)------------------------------ % 28.80/4.31 % (3843836)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.80/4.31 % (3843836)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.80/4.31 % (3843836)CaDiCaL version: 2.1.3 % 28.80/4.31 % (3843836)Termination reason: Inappropriate % 28.80/4.31 % (3843836)Time elapsed: 0.0000 s % 28.80/4.31 % (3843836)Peak memory usage: 10 MB % 28.80/4.31 % (3843836)Instructions burned: 1 (million) % 28.80/4.31 % (3843836)------------------------------ % 28.80/4.31 % (3843836)------------------------------ % 28.80/4.31 % (3843840)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1994868069:fmbsr=1.7:i=920_2997 on theBenchmark for (2997ds/920Mi) % 28.80/4.31 % (3843840)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 28.80/4.31 % (3843840)Terminated due to inappropriate strategy. % 28.80/4.31 % (3843840)------------------------------ % 28.80/4.31 % (3843840)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.80/4.31 % (3843840)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.80/4.31 % (3843840)CaDiCaL version: 2.1.3 % 28.80/4.31 % (3843840)Termination reason: Inappropriate % 28.80/4.31 % (3843840)Time elapsed: 0.0000 s % 28.80/4.31 % (3843840)Peak memory usage: 11 MB % 28.80/4.31 % (3843840)Instructions burned: 1 (million) % 28.80/4.31 % (3843840)------------------------------ % 28.80/4.31 % (3843840)------------------------------ % 28.80/4.31 % (3843844)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3962493192:i=5131_2997 on theBenchmark for (2997ds/5131Mi) % 28.80/4.31 % (3843789)Instruction limit reached! % 28.80/4.31 % (3843789)------------------------------ % 28.80/4.31 % (3843789)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.80/4.31 % (3843789)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.80/4.31 % (3843789)CaDiCaL version: 2.1.3 % 28.80/4.31 % (3843789)Termination reason: Instruction limit % 28.80/4.31 % (3843789)Termination phase: Saturation % 28.80/4.31 % (3843789)Time elapsed: 0.288 s % 28.80/4.31 % (3843789)Peak memory usage: 14 MB % 28.80/4.31 % (3843789)Instructions burned: 477 (million) % 28.80/4.31 % (3843880)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3549286119:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi) % 28.80/4.31 % (3843813)Instruction limit reached! % 28.80/4.31 % (3843813)------------------------------ % 38.71/5.78 % (3843813)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 38.71/5.78 % (3843813)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.71/5.78 % (3843813)CaDiCaL version: 2.1.3 % 38.71/5.78 % (3843813)Termination reason: Instruction limit % 38.71/5.78 % (3843813)Termination phase: Saturation % 38.71/5.78 % (3843813)Time elapsed: 0.437 s % 38.71/5.78 % (3843813)Peak memory usage: 19 MB % 38.71/5.78 % (3843813)Instructions burned: 693 (million) % 38.71/5.78 % (3843923)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=447085165:i=6324_2993 on theBenchmark for (2993ds/6324Mi) % 38.71/5.78 % (3843923)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 38.71/5.78 % (3843923)Terminated due to inappropriate strategy. % 38.71/5.78 % (3843923)------------------------------ % 38.71/5.78 % (3843923)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 38.71/5.78 % (3843923)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.71/5.78 % (3843923)CaDiCaL version: 2.1.3 % 38.71/5.78 % (3843923)Termination reason: Inappropriate % 38.71/5.78 % (3843923)Time elapsed: 0.001 s % 38.71/5.78 % (3843923)Peak memory usage: 10 MB % 38.71/5.78 % (3843923)Instructions burned: 1 (million) % 38.71/5.78 % (3843923)------------------------------ % 38.71/5.78 % (3843923)------------------------------ % 38.71/5.78 % (3843928)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2517336498:fmbsr=2.30978:i=2174_2993 on theBenchmark for (2993ds/2174Mi) % 38.71/5.78 % (3843928)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 38.71/5.78 % (3843928)Terminated due to inappropriate strategy. % 38.71/5.78 % (3843928)------------------------------ % 38.71/5.78 % (3843928)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 38.71/5.78 % (3843928)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.71/5.78 % (3843928)CaDiCaL version: 2.1.3 % 38.71/5.78 % (3843928)Termination reason: Inappropriate % 38.71/5.78 % (3843928)Time elapsed: 0.001 s % 38.71/5.78 % (3843928)Peak memory usage: 10 MB % 38.71/5.78 % (3843928)Instructions burned: 1 (million) % 38.71/5.78 % (3843928)------------------------------ % 38.71/5.78 % (3843928)------------------------------ % 38.71/5.78 % (3843936)ott-2_1_sil=16000:newcnf=on:random_seed=4250670371:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2993 on theBenchmark for (2993ds/869Mi) % 38.71/5.78 % (3843817)Instruction limit reached! % 38.71/5.78 % (3843817)------------------------------ % 38.71/5.78 % (3843817)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 38.71/5.78 % (3843817)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.71/5.78 % (3843817)CaDiCaL version: 2.1.3 % 38.71/5.78 % (3843817)Termination reason: Instruction limit % 38.71/5.78 % (3843817)Termination phase: Saturation % 38.71/5.78 % (3843817)Time elapsed: 0.499 s % 38.71/5.78 % (3843817)Peak memory usage: 19 MB % 38.71/5.78 % (3843817)Instructions burned: 880 (million) % 38.71/5.78 % (3843938)ott+10_1_sil=32000:tgt=ground:random_seed=3773725778:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi) % 38.71/5.78 % (3843805)Instruction limit reached! % 38.71/5.78 % (3843805)------------------------------ % 38.71/5.78 % (3843805)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 38.71/5.78 % (3843805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.71/5.78 % (3843805)CaDiCaL version: 2.1.3 % 38.71/5.78 % (3843805)Termination reason: Instruction limit % 38.71/5.78 % (3843805)Termination phase: Saturation % 38.71/5.78 % (3843805)Time elapsed: 0.867 s % 38.71/5.78 % (3843805)Peak memory usage: 18 MB % 38.71/5.78 % (3843805)Instructions burned: 1179 (million) % 38.71/5.78 % (3843940)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=645865187:i=54282_2989 on theBenchmark for (2989ds/54282Mi) % 38.71/5.78 % (3843940)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 38.71/5.78 % (3843940)Terminated due to inappropriate strategy. % 38.71/5.78 % (3843940)------------------------------ % 38.71/5.78 % (3843940)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 38.71/5.78 % (3843940)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.71/5.78 % (3843940)CaDiCaL version: 2.1.3 % 38.71/5.78 % (3843940)Termination reason: Inappropriate % 38.71/5.78 % (3843940)Time elapsed: 0.001 s % 38.71/5.78 % (3843940)Peak memory usage: 11 MB % 38.71/5.78 % (3843940)Instructions burned: 1 (million) % 146.93/20.96 % (3843940)------------------------------ % 146.93/20.96 % (3843940)------------------------------ % 146.93/20.96 % (3843942)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1738353916:i=3512:aac=none_2989 on theBenchmark for (2989ds/3512Mi) % 146.93/20.96 % (3843936)Instruction limit reached! % 146.93/20.96 % (3843936)------------------------------ % 146.93/20.96 % (3843936)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 146.93/20.96 % (3843936)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 146.93/20.96 % (3843936)CaDiCaL version: 2.1.3 % 146.93/20.96 % (3843936)Termination reason: Instruction limit % 146.93/20.96 % (3843936)Termination phase: Saturation % 146.93/20.96 % (3843936)Time elapsed: 0.541 s % 146.93/20.96 % (3843936)Peak memory usage: 15 MB % 146.93/20.96 % (3843936)Instructions burned: 870 (million) % 146.93/20.96 % (3843944)dis+21_1_sil=32000:sas=cadical:random_seed=834178158:i=3773:amm=off_2987 on theBenchmark for (2987ds/3773Mi) % 146.93/20.96 % (3843880)Instruction limit reached! % 146.93/20.96 % (3843880)------------------------------ % 146.93/20.96 % (3843880)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 146.93/20.96 % (3843880)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 146.93/20.96 % (3843880)CaDiCaL version: 2.1.3 % 146.93/20.96 % (3843880)Termination reason: Instruction limit % 146.93/20.96 % (3843880)Termination phase: Saturation % 146.93/20.96 % (3843880)Time elapsed: 0.857 s % 146.93/20.96 % (3843880)Peak memory usage: 29 MB % 146.93/20.96 % (3843880)Instructions burned: 1473 (million) % 146.93/20.96 % (3843949)ott+11_1_sil=16000:gs=on:random_seed=3367371252:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2986 on theBenchmark for (2986ds/2251Mi) % 146.93/20.96 % (3843844)Instruction limit reached! % 146.93/20.96 % (3843844)------------------------------ % 146.93/20.96 % (3843844)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 146.93/20.96 % (3843844)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 146.93/20.96 % (3843844)CaDiCaL version: 2.1.3 % 146.93/20.96 % (3843844)Termination reason: Instruction limit % 146.93/20.96 % (3843844)Termination phase: Saturation % 146.93/20.96 % (3843844)Time elapsed: 1.713 s % 146.93/20.96 % (3843844)Peak memory usage: 42 MB % 146.93/20.96 % (3843844)Instructions burned: 5134 (million) % 146.93/20.96 % (3843992)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=882617998:fmbsr=1.6:i=67534_2979 on theBenchmark for (2979ds/67534Mi) % 146.93/20.96 % (3843992)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 146.93/20.96 % (3843992)Terminated due to inappropriate strategy. % 146.93/20.96 % (3843992)------------------------------ % 146.93/20.96 % (3843992)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 146.93/20.96 % (3843992)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 146.93/20.96 % (3843992)CaDiCaL version: 2.1.3 % 146.93/20.96 % (3843992)Termination reason: Inappropriate % 146.93/20.96 % (3843992)Time elapsed: 0.0000 s % 146.93/20.96 % (3843992)Peak memory usage: 10 MB % 146.93/20.96 % (3843992)Instructions burned: 1 (million) % 146.93/20.96 % (3843992)------------------------------ % 146.93/20.96 % (3843992)------------------------------ % 146.93/20.96 % (3843994)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=728474162:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2979 on theBenchmark for (2979ds/4591Mi) % 146.93/20.96 % (3843949)Instruction limit reached! % 146.93/20.96 % (3843949)------------------------------ % 146.93/20.96 % (3843949)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 146.93/20.96 % (3843949)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 146.93/20.96 % (3843949)CaDiCaL version: 2.1.3 % 146.93/20.96 % (3843949)Termination reason: Instruction limit % 146.93/20.96 % (3843949)Termination phase: Saturation % 146.93/20.96 % (3843949)Time elapsed: 1.930 s % 146.93/20.96 % (3843949)Peak memory usage: 24 MB % 146.93/20.96 % (3843949)Instructions burned: 2251 (million) % 146.93/20.96 % (3844045)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=303289415:i=29340_2967 on theBenchmark for (2967ds/29340Mi) % 146.93/20.96 % (3843942)Instruction limit reached! % 146.93/20.96 % (3843942)------------------------------ % 146.93/20.96 % (3843942)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 146.93/20.96 % (3843942)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 146.93/20.96 % (3843942)CaDiCaL version: 2.1.3 % 146.93/20.96 % (3843942)Termination reason: Instruction limit % 162.87/26.48 % (3843942)Termination phase: Saturation % 162.87/26.48 % (3843942)Time elapsed: 2.962 s % 162.87/26.48 % (3843942)Peak memory usage: 35 MB % 162.87/26.48 % (3843942)Instructions burned: 3513 (million) % 162.87/26.48 % (3844068)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=523088755:i=5211_2959 on theBenchmark for (2959ds/5211Mi) % 162.87/26.48 % (3843994)Instruction limit reached! % 162.87/26.48 % (3843994)------------------------------ % 162.87/26.48 % (3843994)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 162.87/26.48 % (3843994)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 162.87/26.48 % (3843994)CaDiCaL version: 2.1.3 % 162.87/26.48 % (3843994)Termination reason: Instruction limit % 162.87/26.48 % (3843994)Termination phase: Saturation % 162.87/26.48 % (3843994)Time elapsed: 2.119 s % 162.87/26.48 % (3843994)Peak memory usage: 49 MB % 162.87/26.48 % (3843994)Instructions burned: 4593 (million) % 162.87/26.48 % (3844073)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=546213032:i=5497:nm=2_2958 on theBenchmark for (2958ds/5497Mi) % 162.87/26.48 % (3844073)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 162.87/26.48 % (3844073)Terminated due to inappropriate strategy. % 162.87/26.48 % (3844073)------------------------------ % 162.87/26.48 % (3844073)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 162.87/26.48 % (3844073)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 162.87/26.48 % (3844073)CaDiCaL version: 2.1.3 % 162.87/26.48 % (3844073)Termination reason: Inappropriate % 162.87/26.48 % (3844073)Time elapsed: 0.001 s % 162.87/26.48 % (3844073)Peak memory usage: 10 MB % 162.87/26.48 % (3844073)Instructions burned: 1 (million) % 162.87/26.48 % (3844073)------------------------------ % 162.87/26.48 % (3844073)------------------------------ % 162.87/26.48 % (3844077)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=838050029:fmbsr=2:i=46332_2957 on theBenchmark for (2957ds/46332Mi) % 162.87/26.48 % (3844077)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 162.87/26.48 % (3844077)Terminated due to inappropriate strategy. % 162.87/26.48 % (3844077)------------------------------ % 162.87/26.48 % (3844077)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 162.87/26.48 % (3844077)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 162.87/26.48 % (3844077)CaDiCaL version: 2.1.3 % 162.87/26.48 % (3844077)Termination reason: Inappropriate % 162.87/26.48 % (3844077)Time elapsed: 0.002 s % 162.87/26.48 % (3844077)Peak memory usage: 10 MB % 162.87/26.48 % (3844077)Instructions burned: 1 (million) % 162.87/26.48 % (3844077)------------------------------ % 162.87/26.48 % (3844077)------------------------------ % 162.87/26.48 % (3844082)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=4005027590:i=14071_2957 on theBenchmark for (2957ds/14071Mi) % 162.87/26.48 % (3844082)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 162.87/26.48 % (3844082)Terminated due to inappropriate strategy. % 162.87/26.48 % (3844082)------------------------------ % 162.87/26.48 % (3844082)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 162.87/26.48 % (3844082)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 162.87/26.48 % (3844082)CaDiCaL version: 2.1.3 % 162.87/26.48 % (3844082)Termination reason: Inappropriate % 162.87/26.48 % (3844082)Time elapsed: 0.001 s % 162.87/26.48 % (3844082)Peak memory usage: 11 MB % 162.87/26.48 % (3844082)Instructions burned: 1 (million) % 162.87/26.48 % (3844082)------------------------------ % 162.87/26.48 % (3844082)------------------------------ % 162.87/26.48 % (3844084)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3240399620:i=22565:add=on:rawr=on_2956 on theBenchmark for (2956ds/22565Mi) % 162.87/26.48 % (3843944)Instruction limit reached! % 162.87/26.48 % (3843944)------------------------------ % 162.87/26.48 % (3843944)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 162.87/26.48 % (3843944)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 162.87/26.48 % (3843944)CaDiCaL version: 2.1.3 % 162.87/26.48 % (3843944)Termination reason: Instruction limit % 162.87/26.48 % (3843944)Termination phase: Saturation % 162.87/26.48 % (3843944)Time elapsed: 3.305 s % 162.87/26.48 % (3843944)Peak memory usage: 31 MB % 162.87/26.48 % (3843944)Instructions burned: 3773 (million) % 162.87/26.48 % (3844093)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=2841808112:i=8173:av=off_2954 on theBenchmark for (2954ds/8173Mi) % 162.87/26.48 % (3843938)Instruction limit reached! % 187.49/26.65 % (3843938)------------------------------ % 187.49/26.65 % (3843938)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 187.49/26.65 % (3843938)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 187.49/26.65 % (3843938)CaDiCaL version: 2.1.3 % 187.49/26.65 % (3843938)Termination reason: Instruction limit % 187.49/26.65 % (3843938)Termination phase: Saturation % 187.49/26.65 % (3843938)Time elapsed: 4.787 s % 187.49/26.65 % (3843938)Peak memory usage: 41 MB % 187.49/26.65 % (3843938)Instructions burned: 5115 (million) % 187.49/26.65 % (3844122)dis+10_16:1_sil=16000:random_seed=3891081005:i=9155:fsr=off_2944 on theBenchmark for (2944ds/9155Mi) % 187.49/26.65 % (3844068)Instruction limit reached! % 187.49/26.65 % (3844068)------------------------------ % 187.49/26.65 % (3844068)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 187.49/26.65 % (3844068)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 187.49/26.65 % (3844068)CaDiCaL version: 2.1.3 % 187.49/26.65 % (3844068)Termination reason: Instruction limit % 187.49/26.65 % (3844068)Termination phase: Saturation % 187.49/26.65 % (3844068)Time elapsed: 2.402 s % 187.49/26.65 % (3844068)Peak memory usage: 50 MB % 187.49/26.65 % (3844068)Instructions burned: 5212 (million) % 187.49/26.65 % (3844141)ott-3_8_sil=64000:random_seed=312465909:i=20139:bs=on_2935 on theBenchmark for (2935ds/20139Mi) % 187.49/26.65 % (3844093)Instruction limit reached! % 187.49/26.65 % (3844093)------------------------------ % 187.49/26.65 % (3844093)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 187.49/26.65 % (3844093)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 187.49/26.65 % (3844093)CaDiCaL version: 2.1.3 % 187.49/26.65 % (3844093)Termination reason: Instruction limit % 187.49/26.65 % (3844093)Termination phase: Saturation % 187.49/26.65 % (3844093)Time elapsed: 8.082 s % 187.49/26.65 % (3844093)Peak memory usage: 51 MB % 187.49/26.65 % (3844093)Instructions burned: 8173 (million) % 187.49/26.65 % (3844198)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=2909374987:fmbsr=2:i=32576_2873 on theBenchmark for (2873ds/32576Mi) % 187.49/26.65 % (3844198)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 187.49/26.65 % (3844198)Terminated due to inappropriate strategy. % 187.49/26.65 % (3844198)------------------------------ % 187.49/26.65 % (3844198)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 187.49/26.65 % (3844198)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 187.49/26.65 % (3844198)CaDiCaL version: 2.1.3 % 187.49/26.65 % (3844198)Termination reason: Inappropriate % 187.49/26.65 % (3844198)Time elapsed: 0.001 s % 187.49/26.65 % (3844198)Peak memory usage: 11 MB % 187.49/26.65 % (3844198)Instructions burned: 1 (million) % 187.49/26.65 % (3844198)------------------------------ % 187.49/26.65 % (3844198)------------------------------ % 187.49/26.65 % (3844201)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=1672596214:i=11404_2872 on theBenchmark for (2872ds/11404Mi) % 187.49/26.65 % (3844122)Instruction limit reached! % 187.49/26.65 % (3844122)------------------------------ % 187.49/26.65 % (3844122)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 187.49/26.65 % (3844122)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 187.49/26.65 % (3844122)CaDiCaL version: 2.1.3 % 187.49/26.65 % (3844122)Termination reason: Instruction limit % 187.49/26.65 % (3844122)Termination phase: Saturation % 187.49/26.65 % (3844122)Time elapsed: 8.193 s % 187.49/26.65 % (3844122)Peak memory usage: 52 MB % 187.49/26.65 % (3844122)Instructions burned: 9155 (million) % 187.49/26.65 % (3844211)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=2462150878:i=14134_2862 on theBenchmark for (2862ds/14134Mi) % 187.49/26.65 % (3844141)Instruction limit reached! % 187.49/26.65 % (3844141)------------------------------ % 187.49/26.65 % (3844141)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 187.49/26.65 % (3844141)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 187.49/26.65 % (3844141)CaDiCaL version: 2.1.3 % 187.49/26.65 % (3844141)Termination reason: Instruction limit % 187.49/26.65 % (3844141)Termination phase: Saturation % 187.49/26.65 % (3844141)Time elapsed: 10.243 s % 187.49/26.65 % (3844141)Peak memory usage: 57 MB % 187.49/26.65 % (3844141)Instructions burned: 20141 (million) % 187.49/26.65 % (3844217)dis+33_16_sil=32000:sac=on:random_seed=623596735:i=15851:nm=0_2832 on theBenchmark for (2832ds/15851Mi) % 187.49/26.65 % (3844084)Instruction limit reached! % 187.49/26.65 % (3844084)------------------------------ % 187.49/26.65 % (3844084)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 261.78/37.11 % (3844084)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 261.78/37.11 % (3844084)CaDiCaL version: 2.1.3 % 261.78/37.11 % (3844084)Termination reason: Instruction limit % 261.78/37.11 % (3844084)Termination phase: Saturation % 261.78/37.11 % (3844084)Time elapsed: 16.343 s % 261.78/37.11 % (3844084)Peak memory usage: 75 MB % 261.78/37.11 % (3844084)Instructions burned: 22565 (million) % 261.78/37.11 % (3844228)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=807470290:avsq=on:i=17627:add=on:amm=off_2792 on theBenchmark for (2792ds/17627Mi) % 261.78/37.11 % (3844217)Instruction limit reached! % 261.78/37.11 % (3844217)------------------------------ % 261.78/37.11 % (3844217)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 261.78/37.11 % (3844217)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 261.78/37.11 % (3844217)CaDiCaL version: 2.1.3 % 261.78/37.11 % (3844217)Termination reason: Instruction limit % 261.78/37.11 % (3844217)Termination phase: Saturation % 261.78/37.11 % (3844217)Time elapsed: 6.863 s % 261.78/37.11 % (3844217)Peak memory usage: 205 MB % 261.78/37.11 % (3844217)Instructions burned: 15851 (million) % 261.78/37.11 % (3844235)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=2077170049:s2a=on:i=53295_2763 on theBenchmark for (2763ds/53295Mi) % 261.78/37.11 % (3844201)Instruction limit reached! % 261.78/37.11 % (3844201)------------------------------ % 261.78/37.11 % (3844201)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 261.78/37.11 % (3844201)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 261.78/37.11 % (3844201)CaDiCaL version: 2.1.3 % 261.78/37.11 % (3844201)Termination reason: Instruction limit % 261.78/37.11 % (3844201)Termination phase: Saturation % 261.78/37.11 % (3844201)Time elapsed: 11.521 s % 261.78/37.11 % (3844201)Peak memory usage: 71 MB % 261.78/37.11 % (3844201)Instructions burned: 11404 (million) % 261.78/37.11 % (3844239)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=3032032523:i=26857:ins=20_2757 on theBenchmark for (2757ds/26857Mi) % 261.78/37.11 % (3844239)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 261.78/37.11 % (3844239)Terminated due to inappropriate strategy. % 261.78/37.11 % (3844239)------------------------------ % 261.78/37.11 % (3844239)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 261.78/37.11 % (3844239)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 261.78/37.11 % (3844239)CaDiCaL version: 2.1.3 % 261.78/37.11 % (3844239)Termination reason: Inappropriate % 261.78/37.11 % (3844239)Time elapsed: 0.001 s % 261.78/37.11 % (3844239)Peak memory usage: 10 MB % 261.78/37.11 % (3844239)Instructions burned: 1 (million) % 261.78/37.11 % (3844239)------------------------------ % 261.78/37.11 % (3844239)------------------------------ % 261.78/37.11 % (3844241)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=305541015:i=28120:bs=on:fsr=off_2756 on theBenchmark for (2756ds/28120Mi) % 261.78/37.11 % (3844045)Instruction limit reached! % 261.78/37.11 % (3844045)------------------------------ % 261.78/37.11 % (3844045)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 261.78/37.11 % (3844045)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 261.78/37.11 % (3844045)CaDiCaL version: 2.1.3 % 261.78/37.11 % (3844045)Termination reason: Instruction limit % 261.78/37.11 % (3844045)Termination phase: Saturation % 261.78/37.11 % (3844045)Time elapsed: 22.804 s % 261.78/37.11 % (3844045)Peak memory usage: 168 MB % 261.78/37.11 % (3844045)Instructions burned: 29340 (million) % 261.78/37.11 % (3844248)fmb+10_1_sil=256000:fmbss=7:random_seed=418707107:fmbsr=1.6:i=182295_2738 on theBenchmark for (2738ds/182295Mi) % 261.78/37.11 % (3844248)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 261.78/37.11 % (3844248)Terminated due to inappropriate strategy. % 261.78/37.11 % (3844248)------------------------------ % 261.78/37.11 % (3844248)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 261.78/37.11 % (3844248)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 261.78/37.11 % (3844248)CaDiCaL version: 2.1.3 % 261.78/37.11 % (3844248)Termination reason: Inappropriate % 261.78/37.11 % (3844248)Time elapsed: 0.001 s % 261.78/37.11 % (3844248)Peak memory usage: 10 MB % 261.78/37.11 % (3844248)Instructions burned: 1 (million) % 261.78/37.11 % (3844248)------------------------------ % 261.78/37.11 % (3844248)------------------------------ % 261.78/37.11 % (3844250)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=3057269122:i=44625:gsp=on_2738 on theBenchmark for (2738ds/44625Mi) % 283.13/40.04 % (3844250)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 283.13/40.04 % (3844250)Terminated due to inappropriate strategy. % 283.13/40.04 % (3844250)------------------------------ % 283.13/40.04 % (3844250)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 283.13/40.04 % (3844250)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 283.13/40.04 % (3844250)CaDiCaL version: 2.1.3 % 283.13/40.04 % (3844250)Termination reason: Inappropriate % 283.13/40.04 % (3844250)Time elapsed: 0.001 s % 283.13/40.04 % (3844250)Peak memory usage: 10 MB % 283.13/40.04 % (3844250)Instructions burned: 1 (million) % 283.13/40.04 % (3844250)------------------------------ % 283.13/40.04 % (3844250)------------------------------ % 283.13/40.04 % (3844252)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=793669193:i=160505_2737 on theBenchmark for (2737ds/160505Mi) % 283.13/40.04 % (3844252)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 283.13/40.04 % (3844252)Terminated due to inappropriate strategy. % 283.13/40.04 % (3844252)------------------------------ % 283.13/40.04 % (3844252)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 283.13/40.04 % (3844252)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 283.13/40.04 % (3844252)CaDiCaL version: 2.1.3 % 283.13/40.04 % (3844252)Termination reason: Inappropriate % 283.13/40.04 % (3844252)Time elapsed: 0.002 s % 283.13/40.04 % (3844252)Peak memory usage: 10 MB % 283.13/40.04 % (3844252)Instructions burned: 1 (million) % 283.13/40.04 % (3844252)------------------------------ % 283.13/40.04 % (3844252)------------------------------ % 283.13/40.04 % (3844254)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=3022953387:fmbsr=1.3:i=225729_2737 on theBenchmark for (2737ds/225729Mi) % 283.13/40.04 % (3844254)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 283.13/40.04 % (3844254)Terminated due to inappropriate strategy. % 283.13/40.04 % (3844254)------------------------------ % 283.13/40.04 % (3844254)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 283.13/40.04 % (3844254)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 283.13/40.04 % (3844254)CaDiCaL version: 2.1.3 % 283.13/40.04 % (3844254)Termination reason: Inappropriate % 283.13/40.04 % (3844254)Time elapsed: 0.001 s % 283.13/40.04 % (3844254)Peak memory usage: 11 MB % 283.13/40.04 % (3844254)Instructions burned: 1 (million) % 283.13/40.04 % (3844254)------------------------------ % 283.13/40.04 % (3844254)------------------------------ % 283.13/40.04 % (3844256)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=985794345:fmbsr=2:i=185024:ins=7_2737 on theBenchmark for (2737ds/185024Mi) % 283.13/40.04 % (3844256)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 283.13/40.04 % (3844256)Terminated due to inappropriate strategy. % 283.13/40.04 % (3844256)------------------------------ % 283.13/40.04 % (3844256)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 283.13/40.04 % (3844256)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 283.13/40.04 % (3844256)CaDiCaL version: 2.1.3 % 283.13/40.04 % (3844256)Termination reason: Inappropriate % 283.13/40.04 % (3844256)Time elapsed: 0.001 s % 283.13/40.04 % (3844256)Peak memory usage: 11 MB % 283.13/40.04 % (3844256)Instructions burned: 1 (million) % 283.13/40.04 % (3844256)------------------------------ % 283.13/40.04 % (3844256)------------------------------ % 283.13/40.04 % (3844259)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=54505755:rtra=on_2736 on theBenchmark for (2736ds/0Mi) % 283.13/40.04 % (3844259)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 283.13/40.04 % (3844259)Terminated due to inappropriate strategy. % 283.13/40.04 % (3844259)------------------------------ % 283.13/40.04 % (3844259)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 283.13/40.04 % (3844259)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 283.13/40.04 % (3844259)CaDiCaL version: 2.1.3 % 283.13/40.04 % (3844259)Termination reason: Inappropriate % 283.13/40.04 % (3844259)Time elapsed: 0.001 s % 283.13/40.04 % (3844259)Peak memory usage: 10 MB % 283.13/40.04 % (3844259)Instructions burned: 1 (million) % 283.13/40.04 % (3844259)------------------------------ % 283.13/40.04 % (3844259)------------------------------ % 283.13/40.04 % (3844261)% WARNING: option uhcvi not known. % 283.13/40.04 % (3844261)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2514406112:i=271062:addTerminated % 300.64/42.54 % Vampire exiting % 300.64/42.54 Terminated %------------------------------------------------------------------------------