%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : NUM927_2 : TPTP v9.3.1. Released v6.4.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n012.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 12:26:14 PM UTC 2026 % Result : Timeout 300.11s 42.93s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.01 % Problem : NUM927_2 : TPTP v9.3.1. Released v6.4.0. % 0.00/0.03 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.04/0.31 % Computer : n012.cluster.edu % 0.04/0.31 % Model : x86_64 x86_64 % 0.04/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.04/0.31 % Memory : 8046.5625MB % 0.04/0.31 % OS : Linux 6.8.0-71-generic % 0.04/0.31 % CPULimit : 300 % 0.04/0.31 % WCLimit : 300 % 0.04/0.31 % DateTime : Sun Sep 27 21:44:34 UTC 2026 % 0.04/0.31 % CPUTime : % 0.04/0.31 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.08/0.33 Running first-order model finding % 0.08/0.33 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 % 2.32/0.70 % (2777529)Will run a generic schedule for satisfiability detection. % 2.32/0.70 % (2777535)% WARNING: option uhcvi not known. % 2.32/0.70 % (2777536)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3235500504:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 2.32/0.70 % (2777534)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3363760818_2999 on theBenchmark for (2999ds/0Mi) % 2.32/0.70 % (2777537)dis+10_1_sil=32000:sp=arity:random_seed=2701007047:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 2.32/0.70 % (2777535)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1912475828:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 2.32/0.70 % (2777538)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=612293934:i=116_2999 on theBenchmark for (2999ds/116Mi) % 2.32/0.70 % (2777539)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=261798889:i=131_2999 on theBenchmark for (2999ds/131Mi) % 2.32/0.70 % (2777540)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=20880327:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 2.32/0.70 % (2777534)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 2.32/0.70 % (2777534)Terminated due to inappropriate strategy. % 2.32/0.70 % (2777534)------------------------------ % 2.32/0.70 % (2777534)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.32/0.70 % (2777534)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.32/0.70 % (2777534)CaDiCaL version: 2.1.3 % 2.32/0.70 % (2777534)Termination reason: Inappropriate % 2.32/0.70 % (2777534)Time elapsed: 0.0000 s % 2.32/0.70 % (2777534)Peak memory usage: 10 MB % 2.32/0.70 % (2777534)------------------------------ % 2.32/0.70 % (2777534)------------------------------ % 2.32/0.70 % (2777548)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2301992659:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 2.32/0.70 % (2777548)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 2.32/0.70 % (2777548)Terminated due to inappropriate strategy. % 2.32/0.70 % (2777548)------------------------------ % 2.32/0.70 % (2777548)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.32/0.70 % (2777548)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.32/0.70 % (2777548)CaDiCaL version: 2.1.3 % 2.32/0.70 % (2777548)Termination reason: Inappropriate % 2.32/0.70 % (2777548)Time elapsed: 0.0000 s % 2.32/0.70 % (2777548)Peak memory usage: 10 MB % 2.32/0.70 % (2777548)------------------------------ % 2.32/0.70 % (2777548)------------------------------ % 2.32/0.70 % (2777550)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=492450019:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 2.32/0.70 % (2777537)Instruction limit reached! % 2.32/0.70 % (2777537)------------------------------ % 2.32/0.70 % (2777537)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.32/0.70 % (2777537)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.32/0.70 % (2777537)CaDiCaL version: 2.1.3 % 2.32/0.70 % (2777537)Termination reason: Instruction limit % 2.32/0.70 % (2777537)Termination phase: Saturation % 2.32/0.70 % (2777537)Time elapsed: 0.035 s % 2.32/0.70 % (2777537)Peak memory usage: 12 MB % 2.32/0.70 % (2777537)Instructions burned: 103 (million) % 2.32/0.70 % (2777538)Instruction limit reached! % 2.32/0.70 % (2777538)------------------------------ % 2.32/0.70 % (2777538)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.32/0.70 % (2777538)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.32/0.70 % (2777538)CaDiCaL version: 2.1.3 % 2.32/0.70 % (2777538)Termination reason: Instruction limit % 2.32/0.70 % (2777538)Termination phase: Saturation % 2.32/0.70 % (2777538)Time elapsed: 0.039 s % 2.32/0.70 % (2777538)Peak memory usage: 12 MB % 2.32/0.70 % (2777538)Instructions burned: 118 (million) % 2.32/0.70 % (2777539)Instruction limit reached! % 2.32/0.70 % (2777539)------------------------------ % 2.32/0.70 % (2777539)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.32/0.70 % (2777539)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.32/0.70 % (2777539)CaDiCaL version: 2.1.3 % 2.32/0.70 % (2777539)Termination reason: Instruction limit % 2.32/0.70 % (2777539)Termination phase: Saturation % 2.32/0.70 % (2777539)Time elapsed: 0.046 s % 2.93/1.01 % (2777539)Peak memory usage: 13 MB % 2.93/1.01 % (2777539)Instructions burned: 134 (million) % 2.93/1.01 % (2777552)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=1941750816:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 2.93/1.01 % (2777553)ott-21_1_sil=16000:fs=off:random_seed=4021678246:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi) % 2.93/1.01 % (2777554)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1752731132:i=477:bd=all_2999 on theBenchmark for (2999ds/477Mi) % 2.93/1.01 % (2777540)Instruction limit reached! % 2.93/1.01 % (2777540)------------------------------ % 2.93/1.01 % (2777540)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.93/1.01 % (2777540)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.93/1.01 % (2777540)CaDiCaL version: 2.1.3 % 2.93/1.01 % (2777540)Termination reason: Instruction limit % 2.93/1.01 % (2777540)Termination phase: Saturation % 2.93/1.01 % (2777540)Time elapsed: 0.062 s % 2.93/1.01 % (2777540)Peak memory usage: 13 MB % 2.93/1.01 % (2777540)Instructions burned: 165 (million) % 2.93/1.01 % (2777550)Instruction limit reached! % 2.93/1.01 % (2777550)------------------------------ % 2.93/1.01 % (2777550)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.93/1.01 % (2777550)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.93/1.01 % (2777550)CaDiCaL version: 2.1.3 % 2.93/1.01 % (2777550)Termination reason: Instruction limit % 2.93/1.01 % (2777550)Termination phase: Saturation % 2.93/1.01 % (2777550)Time elapsed: 0.049 s % 2.93/1.01 % (2777550)Peak memory usage: 12 MB % 2.93/1.01 % (2777550)Instructions burned: 133 (million) % 2.93/1.01 % (2777558)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3214665171:fmbsr=1.3:i=865:ins=25_2999 on theBenchmark for (2999ds/865Mi) % 2.93/1.01 % (2777558)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 2.93/1.01 % (2777558)Terminated due to inappropriate strategy. % 2.93/1.01 % (2777558)------------------------------ % 2.93/1.01 % (2777558)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.93/1.01 % (2777558)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.93/1.01 % (2777558)CaDiCaL version: 2.1.3 % 2.93/1.01 % (2777558)Termination reason: Inappropriate % 2.93/1.01 % (2777558)Time elapsed: 0.0000 s % 2.93/1.01 % (2777558)Peak memory usage: 10 MB % 2.93/1.01 % (2777558)------------------------------ % 2.93/1.01 % (2777558)------------------------------ % 2.93/1.01 % (2777559)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=732905180:i=1179_2999 on theBenchmark for (2999ds/1179Mi) % 2.93/1.01 % (2777561)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=584709952:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 2.93/1.01 % (2777561)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 2.93/1.01 % (2777561)Terminated due to inappropriate strategy. % 2.93/1.01 % (2777561)------------------------------ % 2.93/1.01 % (2777561)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.93/1.01 % (2777561)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.93/1.01 % (2777561)CaDiCaL version: 2.1.3 % 2.93/1.01 % (2777561)Termination reason: Inappropriate % 2.93/1.01 % (2777561)Time elapsed: 0.0000 s % 2.93/1.01 % (2777561)Peak memory usage: 10 MB % 2.93/1.01 % (2777561)------------------------------ % 2.93/1.01 % (2777561)------------------------------ % 2.93/1.01 % (2777553)Instruction limit reached! % 2.93/1.01 % (2777553)------------------------------ % 2.93/1.01 % (2777553)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.93/1.01 % (2777553)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.93/1.01 % (2777553)CaDiCaL version: 2.1.3 % 2.93/1.01 % (2777553)Termination reason: Instruction limit % 2.93/1.01 % (2777553)Termination phase: Saturation % 2.93/1.01 % (2777553)Time elapsed: 0.043 s % 2.93/1.01 % (2777553)Peak memory usage: 12 MB % 2.93/1.01 % (2777553)Instructions burned: 181 (million) % 2.93/1.01 % (2777564)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=3476301196: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) % 2.93/1.01 % (2777565)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=544060980:i=879:kws=inv_precedence:fsr=off_2998 on theBenchmark for (2998ds/879Mi) % 11.38/2.12 % (2777554)Instruction limit reached! % 11.38/2.12 % (2777554)------------------------------ % 11.38/2.12 % (2777554)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 11.38/2.12 % (2777554)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.38/2.12 % (2777554)CaDiCaL version: 2.1.3 % 11.38/2.12 % (2777554)Termination reason: Instruction limit % 11.38/2.12 % (2777554)Termination phase: Saturation % 11.38/2.12 % (2777554)Time elapsed: 0.160 s % 11.38/2.12 % (2777554)Peak memory usage: 15 MB % 11.38/2.12 % (2777554)Instructions burned: 477 (million) % 11.38/2.12 % (2777568)fmb+10_1_sil=64000:random_seed=252046821:i=22061:nm=2:gsp=on_2997 on theBenchmark for (2997ds/22061Mi) % 11.38/2.12 % (2777568)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 11.38/2.12 % (2777568)Terminated due to inappropriate strategy. % 11.38/2.12 % (2777568)------------------------------ % 11.38/2.12 % (2777568)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 11.38/2.12 % (2777568)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.38/2.12 % (2777568)CaDiCaL version: 2.1.3 % 11.38/2.12 % (2777568)Termination reason: Inappropriate % 11.38/2.12 % (2777568)Time elapsed: 0.0000 s % 11.38/2.12 % (2777568)Peak memory usage: 10 MB % 11.38/2.12 % (2777568)Instructions burned: 1 (million) % 11.38/2.12 % (2777568)------------------------------ % 11.38/2.12 % (2777568)------------------------------ % 11.38/2.12 % (2777552)Instruction limit reached! % 11.38/2.12 % (2777552)------------------------------ % 11.38/2.12 % (2777552)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 11.38/2.12 % (2777552)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.38/2.12 % (2777552)CaDiCaL version: 2.1.3 % 11.38/2.12 % (2777552)Termination reason: Instruction limit % 11.38/2.12 % (2777552)Termination phase: Saturation % 11.38/2.12 % (2777552)Time elapsed: 0.190 s % 11.38/2.12 % (2777552)Peak memory usage: 16 MB % 11.38/2.12 % (2777552)Instructions burned: 686 (million) % 11.38/2.12 % (2777570)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1043738458:i=9515:nm=5_2997 on theBenchmark for (2997ds/9515Mi) % 11.38/2.12 % (2777570)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 11.38/2.12 % (2777570)Terminated due to inappropriate strategy. % 11.38/2.12 % (2777570)------------------------------ % 11.38/2.12 % (2777570)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 11.38/2.12 % (2777570)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.38/2.12 % (2777570)CaDiCaL version: 2.1.3 % 11.38/2.12 % (2777570)Termination reason: Inappropriate % 11.38/2.12 % (2777570)Time elapsed: 0.0000 s % 11.38/2.12 % (2777570)Peak memory usage: 10 MB % 11.38/2.12 % (2777570)------------------------------ % 11.38/2.12 % (2777570)------------------------------ % 11.38/2.12 % (2777571)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2390965975:fmbsr=1.7:i=920_2997 on theBenchmark for (2997ds/920Mi) % 11.38/2.12 % (2777571)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 11.38/2.12 % (2777571)Terminated due to inappropriate strategy. % 11.38/2.12 % (2777571)------------------------------ % 11.38/2.12 % (2777571)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 11.38/2.12 % (2777571)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.38/2.12 % (2777571)CaDiCaL version: 2.1.3 % 11.38/2.12 % (2777571)Termination reason: Inappropriate % 11.38/2.12 % (2777571)Time elapsed: 0.0000 s % 11.38/2.12 % (2777571)Peak memory usage: 10 MB % 11.38/2.12 % (2777571)------------------------------ % 11.38/2.12 % (2777571)------------------------------ % 11.38/2.12 % (2777573)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2594464005:i=5131_2997 on theBenchmark for (2997ds/5131Mi) % 11.38/2.12 % (2777575)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1970305760:i=1472:ins=7:fdi=8:gsp=on_2997 on theBenchmark for (2997ds/1472Mi) % 11.38/2.12 % (2777564)Instruction limit reached! % 11.38/2.12 % (2777564)------------------------------ % 11.38/2.12 % (2777564)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 11.38/2.12 % (2777564)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.38/2.12 % (2777564)CaDiCaL version: 2.1.3 % 16.02/2.97 % (2777564)Termination reason: Instruction limit % 16.02/2.97 % (2777564)Termination phase: Saturation % 16.02/2.97 % (2777564)Time elapsed: 0.245 s % 16.02/2.97 % (2777564)Peak memory usage: 17 MB % 16.02/2.97 % (2777564)Instructions burned: 694 (million) % 16.02/2.97 % (2777578)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=979706693:i=6324_2996 on theBenchmark for (2996ds/6324Mi) % 16.02/2.97 % (2777578)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 16.02/2.97 % (2777578)Terminated due to inappropriate strategy. % 16.02/2.97 % (2777578)------------------------------ % 16.02/2.97 % (2777578)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.02/2.97 % (2777578)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.02/2.97 % (2777578)CaDiCaL version: 2.1.3 % 16.02/2.97 % (2777578)Termination reason: Inappropriate % 16.02/2.97 % (2777578)Time elapsed: 0.0000 s % 16.02/2.97 % (2777578)Peak memory usage: 10 MB % 16.02/2.97 % (2777578)------------------------------ % 16.02/2.97 % (2777578)------------------------------ % 16.02/2.97 % (2777580)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3104817830:fmbsr=2.30978:i=2174_2996 on theBenchmark for (2996ds/2174Mi) % 16.02/2.97 % (2777580)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 16.02/2.97 % (2777580)Terminated due to inappropriate strategy. % 16.02/2.97 % (2777580)------------------------------ % 16.02/2.97 % (2777580)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.02/2.97 % (2777580)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.02/2.97 % (2777580)CaDiCaL version: 2.1.3 % 16.02/2.97 % (2777580)Termination reason: Inappropriate % 16.02/2.97 % (2777580)Time elapsed: 0.0000 s % 16.02/2.97 % (2777580)Peak memory usage: 10 MB % 16.02/2.97 % (2777580)------------------------------ % 16.02/2.97 % (2777580)------------------------------ % 16.02/2.97 % (2777565)Instruction limit reached! % 16.02/2.97 % (2777565)------------------------------ % 16.02/2.97 % (2777565)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.02/2.97 % (2777565)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.02/2.97 % (2777565)CaDiCaL version: 2.1.3 % 16.02/2.97 % (2777565)Termination reason: Instruction limit % 16.02/2.97 % (2777565)Termination phase: Saturation % 16.02/2.97 % (2777565)Time elapsed: 0.272 s % 16.02/2.97 % (2777565)Peak memory usage: 18 MB % 16.02/2.97 % (2777565)Instructions burned: 882 (million) % 16.02/2.97 % (2777582)ott-2_1_sil=16000:newcnf=on:random_seed=4160680980:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2996 on theBenchmark for (2996ds/869Mi) % 16.02/2.97 % (2777583)ott+10_1_sil=32000:tgt=ground:random_seed=3744519866:i=5114:av=off_2995 on theBenchmark for (2995ds/5114Mi) % 16.02/2.97 % (2777559)Instruction limit reached! % 16.02/2.97 % (2777559)------------------------------ % 16.02/2.97 % (2777559)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.02/2.97 % (2777559)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.02/2.97 % (2777559)CaDiCaL version: 2.1.3 % 16.02/2.97 % (2777559)Termination reason: Instruction limit % 16.02/2.97 % (2777559)Termination phase: Saturation % 16.02/2.97 % (2777559)Time elapsed: 0.361 s % 16.02/2.97 % (2777559)Peak memory usage: 17 MB % 16.02/2.97 % (2777559)Instructions burned: 1179 (million) % 16.02/2.97 % (2777586)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2123338001:i=54282_2995 on theBenchmark for (2995ds/54282Mi) % 16.02/2.97 % (2777586)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 16.02/2.97 % (2777586)Terminated due to inappropriate strategy. % 16.02/2.97 % (2777586)------------------------------ % 16.02/2.97 % (2777586)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.02/2.97 % (2777586)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.02/2.97 % (2777586)CaDiCaL version: 2.1.3 % 16.02/2.97 % (2777586)Termination reason: Inappropriate % 16.02/2.97 % (2777586)Time elapsed: 0.0000 s % 16.02/2.97 % (2777586)Peak memory usage: 10 MB % 16.02/2.97 % (2777586)------------------------------ % 16.02/2.97 % (2777586)------------------------------ % 16.02/2.97 % (2777588)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1053511331:i=3512:aac=none_2995 on theBenchmark for (2995ds/3512Mi) % 16.02/2.97 % (2777582)Instruction limit reached! % 16.02/2.97 % (2777582)------------------------------ % 16.02/2.97 % (2777582)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 61.88/9.15 % (2777582)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.88/9.15 % (2777582)CaDiCaL version: 2.1.3 % 61.88/9.15 % (2777582)Termination reason: Instruction limit % 61.88/9.15 % (2777582)Termination phase: Saturation % 61.88/9.15 % (2777582)Time elapsed: 0.274 s % 61.88/9.15 % (2777582)Peak memory usage: 15 MB % 61.88/9.15 % (2777582)Instructions burned: 870 (million) % 61.88/9.15 % (2777590)dis+21_1_sil=32000:sas=cadical:random_seed=716747742:i=3773:amm=off_2993 on theBenchmark for (2993ds/3773Mi) % 61.88/9.15 % (2777575)Instruction limit reached! % 61.88/9.15 % (2777575)------------------------------ % 61.88/9.15 % (2777575)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 61.88/9.15 % (2777575)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.88/9.15 % (2777575)CaDiCaL version: 2.1.3 % 61.88/9.15 % (2777575)Termination reason: Instruction limit % 61.88/9.15 % (2777575)Termination phase: Saturation % 61.88/9.15 % (2777575)Time elapsed: 0.460 s % 61.88/9.15 % (2777575)Peak memory usage: 25 MB % 61.88/9.15 % (2777575)Instructions burned: 1473 (million) % 61.88/9.15 % (2777592)ott+11_1_sil=16000:gs=on:random_seed=3741412958:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2992 on theBenchmark for (2992ds/2251Mi) % 61.88/9.15 % (2777592)Instruction limit reached! % 61.88/9.15 % (2777592)------------------------------ % 61.88/9.15 % (2777592)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 61.88/9.15 % (2777592)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.88/9.15 % (2777592)CaDiCaL version: 2.1.3 % 61.88/9.15 % (2777592)Termination reason: Instruction limit % 61.88/9.15 % (2777592)Termination phase: Saturation % 61.88/9.15 % (2777592)Time elapsed: 0.653 s % 61.88/9.15 % (2777592)Peak memory usage: 24 MB % 61.88/9.15 % (2777592)Instructions burned: 2254 (million) % 61.88/9.15 % (2777594)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=211581153:fmbsr=1.6:i=67534_2985 on theBenchmark for (2985ds/67534Mi) % 61.88/9.15 % (2777594)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 61.88/9.15 % (2777594)Terminated due to inappropriate strategy. % 61.88/9.15 % (2777594)------------------------------ % 61.88/9.15 % (2777594)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 61.88/9.15 % (2777594)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.88/9.15 % (2777594)CaDiCaL version: 2.1.3 % 61.88/9.15 % (2777594)Termination reason: Inappropriate % 61.88/9.15 % (2777594)Time elapsed: 0.0000 s % 61.88/9.15 % (2777594)Peak memory usage: 10 MB % 61.88/9.15 % (2777594)------------------------------ % 61.88/9.15 % (2777594)------------------------------ % 61.88/9.15 % (2777596)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=4043845926:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2985 on theBenchmark for (2985ds/4591Mi) % 61.88/9.15 % (2777588)Instruction limit reached! % 61.88/9.15 % (2777588)------------------------------ % 61.88/9.15 % (2777588)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 61.88/9.15 % (2777588)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.88/9.15 % (2777588)CaDiCaL version: 2.1.3 % 61.88/9.15 % (2777588)Termination reason: Instruction limit % 61.88/9.15 % (2777588)Termination phase: Saturation % 61.88/9.15 % (2777588)Time elapsed: 0.985 s % 61.88/9.15 % (2777588)Peak memory usage: 34 MB % 61.88/9.15 % (2777588)Instructions burned: 3512 (million) % 61.88/9.15 % (2777598)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=4103062734:i=29340_2985 on theBenchmark for (2985ds/29340Mi) % 61.88/9.15 % (2777573)Instruction limit reached! % 61.88/9.15 % (2777573)------------------------------ % 61.88/9.15 % (2777573)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 61.88/9.15 % (2777573)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.88/9.15 % (2777573)CaDiCaL version: 2.1.3 % 61.88/9.15 % (2777573)Termination reason: Instruction limit % 61.88/9.15 % (2777573)Termination phase: Saturation % 61.88/9.15 % (2777573)Time elapsed: 1.473 s % 61.88/9.15 % (2777573)Peak memory usage: 41 MB % 61.88/9.15 % (2777573)Instructions burned: 5134 (million) % 61.88/9.15 % (2777600)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=1338092931:i=5211_2982 on theBenchmark for (2982ds/5211Mi) % 61.88/9.15 % (2777590)Instruction limit reached! % 61.88/9.15 % (2777590)------------------------------ % 61.88/9.15 % (2777590)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 70.07/10.35 % (2777590)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 70.07/10.35 % (2777590)CaDiCaL version: 2.1.3 % 70.07/10.35 % (2777590)Termination reason: Instruction limit % 70.07/10.35 % (2777590)Termination phase: Saturation % 70.07/10.35 % (2777590)Time elapsed: 1.094 s % 70.07/10.35 % (2777590)Peak memory usage: 32 MB % 70.07/10.35 % (2777590)Instructions burned: 3776 (million) % 70.07/10.35 % (2777602)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2955781059:i=5497:nm=2_2982 on theBenchmark for (2982ds/5497Mi) % 70.07/10.35 % (2777602)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 70.07/10.35 % (2777602)Terminated due to inappropriate strategy. % 70.07/10.35 % (2777602)------------------------------ % 70.07/10.35 % (2777602)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 70.07/10.35 % (2777602)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 70.07/10.35 % (2777602)CaDiCaL version: 2.1.3 % 70.07/10.35 % (2777602)Termination reason: Inappropriate % 70.07/10.35 % (2777602)Time elapsed: 0.0000 s % 70.07/10.35 % (2777602)Peak memory usage: 10 MB % 70.07/10.35 % (2777602)------------------------------ % 70.07/10.35 % (2777602)------------------------------ % 70.07/10.35 % (2777604)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=989381782:fmbsr=2:i=46332_2982 on theBenchmark for (2982ds/46332Mi) % 70.07/10.35 % (2777604)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 70.07/10.35 % (2777604)Terminated due to inappropriate strategy. % 70.07/10.35 % (2777604)------------------------------ % 70.07/10.35 % (2777604)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 70.07/10.35 % (2777604)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 70.07/10.35 % (2777604)CaDiCaL version: 2.1.3 % 70.07/10.35 % (2777604)Termination reason: Inappropriate % 70.07/10.35 % (2777604)Time elapsed: 0.0000 s % 70.07/10.35 % (2777604)Peak memory usage: 10 MB % 70.07/10.35 % (2777604)------------------------------ % 70.07/10.35 % (2777604)------------------------------ % 70.07/10.35 % (2777606)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=2173188101:i=14071_2981 on theBenchmark for (2981ds/14071Mi) % 70.07/10.35 % (2777606)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 70.07/10.35 % (2777606)Terminated due to inappropriate strategy. % 70.07/10.35 % (2777606)------------------------------ % 70.07/10.35 % (2777606)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 70.07/10.35 % (2777606)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 70.07/10.35 % (2777606)CaDiCaL version: 2.1.3 % 70.07/10.35 % (2777606)Termination reason: Inappropriate % 70.07/10.35 % (2777606)Time elapsed: 0.0000 s % 70.07/10.35 % (2777606)Peak memory usage: 10 MB % 70.07/10.35 % (2777606)------------------------------ % 70.07/10.35 % (2777606)------------------------------ % 70.07/10.35 % (2777608)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3384858723:i=22565:add=on:rawr=on_2981 on theBenchmark for (2981ds/22565Mi) % 70.07/10.35 % (2777583)Instruction limit reached! % 70.07/10.35 % (2777583)------------------------------ % 70.07/10.35 % (2777583)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 70.07/10.35 % (2777583)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 70.07/10.35 % (2777583)CaDiCaL version: 2.1.3 % 70.07/10.35 % (2777583)Termination reason: Instruction limit % 70.07/10.35 % (2777583)Termination phase: Saturation % 70.07/10.35 % (2777583)Time elapsed: 1.698 s % 70.07/10.35 % (2777583)Peak memory usage: 33 MB % 70.07/10.35 % (2777583)Instructions burned: 5115 (million) % 70.07/10.35 % (2777610)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=540835978:i=8173:av=off_2978 on theBenchmark for (2978ds/8173Mi) % 70.07/10.35 % (2777596)Instruction limit reached! % 70.07/10.35 % (2777596)------------------------------ % 70.07/10.35 % (2777596)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 70.07/10.35 % (2777596)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 70.07/10.35 % (2777596)CaDiCaL version: 2.1.3 % 70.07/10.35 % (2777596)Termination reason: Instruction limit % 70.07/10.35 % (2777596)Termination phase: Saturation % 70.07/10.35 % (2777596)Time elapsed: 1.190 s % 70.07/10.35 % (2777596)Peak memory usage: 55 MB % 70.07/10.35 % (2777596)Instructions burned: 4595 (million) % 70.07/10.35 % (2777612)dis+10_16:1_sil=16000:random_seed=2493148862:i=9155:fsr=off_2973 on theBenchmark for (2973ds/9155Mi) % 94.90/13.88 % (2777600)Instruction limit reached! % 94.90/13.88 % (2777600)------------------------------ % 94.90/13.88 % (2777600)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 94.90/13.88 % (2777600)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 94.90/13.88 % (2777600)CaDiCaL version: 2.1.3 % 94.90/13.88 % (2777600)Termination reason: Instruction limit % 94.90/13.88 % (2777600)Termination phase: Saturation % 94.90/13.88 % (2777600)Time elapsed: 1.517 s % 94.90/13.88 % (2777600)Peak memory usage: 55 MB % 94.90/13.88 % (2777600)Instructions burned: 5215 (million) % 94.90/13.88 % (2777614)ott-3_8_sil=64000:random_seed=175156424:i=20139:bs=on_2967 on theBenchmark for (2967ds/20139Mi) % 94.90/13.88 % (2777610)Instruction limit reached! % 94.90/13.88 % (2777610)------------------------------ % 94.90/13.88 % (2777610)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 94.90/13.88 % (2777610)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 94.90/13.88 % (2777610)CaDiCaL version: 2.1.3 % 94.90/13.88 % (2777610)Termination reason: Instruction limit % 94.90/13.88 % (2777610)Termination phase: Saturation % 94.90/13.88 % (2777610)Time elapsed: 2.774 s % 94.90/13.88 % (2777610)Peak memory usage: 56 MB % 94.90/13.88 % (2777610)Instructions burned: 8173 (million) % 94.90/13.88 % (2777616)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=3568528641:fmbsr=2:i=32576_2950 on theBenchmark for (2950ds/32576Mi) % 94.90/13.88 % (2777616)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 94.90/13.88 % (2777616)Terminated due to inappropriate strategy. % 94.90/13.88 % (2777616)------------------------------ % 94.90/13.88 % (2777616)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 94.90/13.88 % (2777616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 94.90/13.88 % (2777616)CaDiCaL version: 2.1.3 % 94.90/13.88 % (2777616)Termination reason: Inappropriate % 94.90/13.88 % (2777616)Time elapsed: 0.0000 s % 94.90/13.88 % (2777616)Peak memory usage: 10 MB % 94.90/13.88 % (2777616)------------------------------ % 94.90/13.88 % (2777616)------------------------------ % 94.90/13.88 % (2777618)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=3676126748:i=11404_2950 on theBenchmark for (2950ds/11404Mi) % 94.90/13.88 % (2777612)Instruction limit reached! % 94.90/13.88 % (2777612)------------------------------ % 94.90/13.88 % (2777612)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 94.90/13.88 % (2777612)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 94.90/13.88 % (2777612)CaDiCaL version: 2.1.3 % 94.90/13.88 % (2777612)Termination reason: Instruction limit % 94.90/13.88 % (2777612)Termination phase: Saturation % 94.90/13.88 % (2777612)Time elapsed: 2.481 s % 94.90/13.88 % (2777612)Peak memory usage: 51 MB % 94.90/13.88 % (2777612)Instructions burned: 9156 (million) % 94.90/13.88 % (2777620)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=436622915:i=14134_2948 on theBenchmark for (2948ds/14134Mi) % 94.90/13.88 % (2777608)Instruction limit reached! % 94.90/13.88 % (2777608)------------------------------ % 94.90/13.88 % (2777608)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 94.90/13.88 % (2777608)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 94.90/13.88 % (2777608)CaDiCaL version: 2.1.3 % 94.90/13.88 % (2777608)Termination reason: Instruction limit % 94.90/13.88 % (2777608)Termination phase: Saturation % 94.90/13.88 % (2777608)Time elapsed: 5.100 s % 94.90/13.88 % (2777608)Peak memory usage: 81 MB % 94.90/13.88 % (2777608)Instructions burned: 22569 (million) % 94.90/13.88 % (2777622)dis+33_16_sil=32000:sac=on:random_seed=4243171279:i=15851:nm=0_2930 on theBenchmark for (2930ds/15851Mi) % 94.90/13.88 % (2777598)Instruction limit reached! % 94.90/13.88 % (2777598)------------------------------ % 94.90/13.88 % (2777598)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 94.90/13.88 % (2777598)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 94.90/13.88 % (2777598)CaDiCaL version: 2.1.3 % 94.90/13.88 % (2777598)Termination reason: Instruction limit % 94.90/13.88 % (2777598)Termination phase: Saturation % 94.90/13.88 % (2777598)Time elapsed: 7.034 s % 94.90/13.88 % (2777598)Peak memory usage: 151 MB % 94.90/13.88 % (2777598)Instructions burned: 29342 (million) % 94.90/13.88 % (2777624)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=813398683:avsq=on:i=17627:add=on:amm=off_2914 on theBenchmark for (2914ds/17627Mi) % 94.90/13.88 % (2777618)Instruction limit reached! % 94.90/13.88 % (2777618)------------------------------ % 98.32/14.33 % (2777618)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 98.32/14.33 % (2777618)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 98.32/14.33 % (2777618)CaDiCaL version: 2.1.3 % 98.32/14.33 % (2777618)Termination reason: Instruction limit % 98.32/14.33 % (2777618)Termination phase: Saturation % 98.32/14.33 % (2777618)Time elapsed: 3.894 s % 98.32/14.33 % (2777618)Peak memory usage: 61 MB % 98.32/14.33 % (2777618)Instructions burned: 11406 (million) % 98.32/14.33 % (2777626)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=1779444206:s2a=on:i=53295_2911 on theBenchmark for (2911ds/53295Mi) % 98.32/14.33 % (2777614)Instruction limit reached! % 98.32/14.33 % (2777614)------------------------------ % 98.32/14.33 % (2777614)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 98.32/14.33 % (2777614)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 98.32/14.33 % (2777614)CaDiCaL version: 2.1.3 % 98.32/14.33 % (2777614)Termination reason: Instruction limit % 98.32/14.33 % (2777614)Termination phase: Saturation % 98.32/14.33 % (2777614)Time elapsed: 6.496 s % 98.32/14.33 % (2777614)Peak memory usage: 69 MB % 98.32/14.33 % (2777614)Instructions burned: 20140 (million) % 98.32/14.33 % (2777628)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=3697491853:i=26857:ins=20_2902 on theBenchmark for (2902ds/26857Mi) % 98.32/14.33 % (2777628)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 98.32/14.33 % (2777628)Terminated due to inappropriate strategy. % 98.32/14.33 % (2777628)------------------------------ % 98.32/14.33 % (2777628)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 98.32/14.33 % (2777628)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 98.32/14.33 % (2777628)CaDiCaL version: 2.1.3 % 98.32/14.33 % (2777628)Termination reason: Inappropriate % 98.32/14.33 % (2777628)Time elapsed: 0.0000 s % 98.32/14.33 % (2777628)Peak memory usage: 10 MB % 98.32/14.33 % (2777628)------------------------------ % 98.32/14.33 % (2777628)------------------------------ % 98.32/14.33 % (2777630)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=511207191:i=28120:bs=on:fsr=off_2901 on theBenchmark for (2901ds/28120Mi) % 98.32/14.33 % (2777620)Instruction limit reached! % 98.32/14.33 % (2777620)------------------------------ % 98.32/14.33 % (2777620)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 98.32/14.33 % (2777620)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 98.32/14.33 % (2777620)CaDiCaL version: 2.1.3 % 98.32/14.33 % (2777620)Termination reason: Instruction limit % 98.32/14.33 % (2777620)Termination phase: Saturation % 98.32/14.33 % (2777620)Time elapsed: 4.847 s % 98.32/14.33 % (2777620)Peak memory usage: 69 MB % 98.32/14.33 % (2777620)Instructions burned: 14135 (million) % 98.32/14.33 % (2777632)fmb+10_1_sil=256000:fmbss=7:random_seed=2104710179:fmbsr=1.6:i=182295_2900 on theBenchmark for (2900ds/182295Mi) % 98.32/14.33 % (2777632)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 98.32/14.33 % (2777632)Terminated due to inappropriate strategy. % 98.32/14.33 % (2777632)------------------------------ % 98.32/14.33 % (2777632)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 98.32/14.33 % (2777632)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 98.32/14.33 % (2777632)CaDiCaL version: 2.1.3 % 98.32/14.33 % (2777632)Termination reason: Inappropriate % 98.32/14.33 % (2777632)Time elapsed: 0.0000 s % 98.32/14.33 % (2777632)Peak memory usage: 10 MB % 98.32/14.33 % (2777632)------------------------------ % 98.32/14.33 % (2777632)------------------------------ % 98.32/14.33 % (2777634)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=288864746:i=44625:gsp=on_2899 on theBenchmark for (2899ds/44625Mi) % 98.32/14.33 % (2777634)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 98.32/14.33 % (2777634)Terminated due to inappropriate strategy. % 98.32/14.33 % (2777634)------------------------------ % 98.32/14.33 % (2777634)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 98.32/14.33 % (2777634)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 98.32/14.33 % (2777634)CaDiCaL version: 2.1.3 % 98.32/14.33 % (2777634)Termination reason: Inappropriate % 98.32/14.33 % (2777634)Time elapsed: 0.0000 s % 98.32/14.33 % (2777634)Peak memory usage: 10 MB % 98.32/14.33 % (2777634)Instructions burned: 1 (million) % 98.32/14.33 % (2777634)------------------------------ % 98.32/14.33 % (2777634)------------------------------ % 109.17/15.94 % (2777636)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=3792963286:i=160505_2899 on theBenchmark for (2899ds/160505Mi) % 109.17/15.94 % (2777636)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 109.17/15.94 % (2777636)Terminated due to inappropriate strategy. % 109.17/15.94 % (2777636)------------------------------ % 109.17/15.94 % (2777636)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 109.17/15.94 % (2777636)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 109.17/15.94 % (2777636)CaDiCaL version: 2.1.3 % 109.17/15.94 % (2777636)Termination reason: Inappropriate % 109.17/15.94 % (2777636)Time elapsed: 0.0000 s % 109.17/15.94 % (2777636)Peak memory usage: 10 MB % 109.17/15.94 % (2777636)------------------------------ % 109.17/15.94 % (2777636)------------------------------ % 109.17/15.94 % (2777638)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=2859707640:fmbsr=1.3:i=225729_2899 on theBenchmark for (2899ds/225729Mi) % 109.17/15.94 % (2777638)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 109.17/15.94 % (2777638)Terminated due to inappropriate strategy. % 109.17/15.94 % (2777638)------------------------------ % 109.17/15.94 % (2777638)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 109.17/15.94 % (2777638)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 109.17/15.94 % (2777638)CaDiCaL version: 2.1.3 % 109.17/15.94 % (2777638)Termination reason: Inappropriate % 109.17/15.94 % (2777638)Time elapsed: 0.0000 s % 109.17/15.94 % (2777638)Peak memory usage: 10 MB % 109.17/15.94 % (2777638)------------------------------ % 109.17/15.94 % (2777638)------------------------------ % 109.17/15.94 % (2777640)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=3197511207:fmbsr=2:i=185024:ins=7_2899 on theBenchmark for (2899ds/185024Mi) % 109.17/15.94 % (2777640)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 109.17/15.94 % (2777640)Terminated due to inappropriate strategy. % 109.17/15.94 % (2777640)------------------------------ % 109.17/15.94 % (2777640)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 109.17/15.94 % (2777640)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 109.17/15.94 % (2777640)CaDiCaL version: 2.1.3 % 109.17/15.94 % (2777640)Termination reason: Inappropriate % 109.17/15.94 % (2777640)Time elapsed: 0.0000 s % 109.17/15.94 % (2777640)Peak memory usage: 10 MB % 109.17/15.94 % (2777640)------------------------------ % 109.17/15.94 % (2777640)------------------------------ % 109.17/15.94 % (2777642)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=1308519537:rtra=on_2899 on theBenchmark for (2899ds/0Mi) % 109.17/15.94 % (2777642)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 109.17/15.94 % (2777642)Terminated due to inappropriate strategy. % 109.17/15.94 % (2777642)------------------------------ % 109.17/15.94 % (2777642)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 109.17/15.94 % (2777642)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 109.17/15.94 % (2777642)CaDiCaL version: 2.1.3 % 109.17/15.94 % (2777642)Termination reason: Inappropriate % 109.17/15.94 % (2777642)Time elapsed: 0.0000 s % 109.17/15.94 % (2777642)Peak memory usage: 10 MB % 109.17/15.94 % (2777642)Instructions burned: 1 (million) % 109.17/15.94 % (2777642)------------------------------ % 109.17/15.94 % (2777642)------------------------------ % 109.17/15.94 % (2777644)% WARNING: option uhcvi not known. % 109.17/15.94 % (2777644)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3425862234:i=271062:add=off:rtra=on:rawr=on_2899 on theBenchmark for (2899ds/271062Mi) % 109.17/15.94 % (2777622)Instruction limit reached! % 109.17/15.94 % (2777622)------------------------------ % 109.17/15.94 % (2777622)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 109.17/15.94 % (2777622)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 109.17/15.94 % (2777622)CaDiCaL version: 2.1.3 % 109.17/15.94 % (2777622)Termination reason: Instruction limit % 109.17/15.94 % (2777622)Termination phase: Saturation % 109.17/15.94 % (2777622)Time elapsed: 3.753 s % 109.17/15.94 % (2777622)Peak memory usage: 102 MB % 109.17/15.94 % (2777622)Instructions burned: 15854 (million) % 109.17/15.94 % (2777646)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1998050914:i=176048:add=on:rtra=on:rawr=on_2892 on theBenchmark for (2892ds/176048Mi) % 109.17/15.94 % (2777624)Instruction limit reached! % 113.04/16.44 % (2777624)------------------------------ % 113.04/16.44 % (2777624)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 113.04/16.44 % (2777624)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.04/16.44 % (2777624)CaDiCaL version: 2.1.3 % 113.04/16.44 % (2777624)Termination reason: Instruction limit % 113.04/16.44 % (2777624)Termination phase: Saturation % 113.04/16.44 % (2777624)Time elapsed: 4.995 s % 113.04/16.44 % (2777624)Peak memory usage: 65 MB % 113.04/16.44 % (2777624)Instructions burned: 17628 (million) % 113.04/16.44 % (2777648)dis+10_1_sil=32000:si=on:sp=arity:random_seed=348684383:i=206:fgj=on:rtra=on_2864 on theBenchmark for (2864ds/206Mi) % 113.04/16.44 % (2777648)Instruction limit reached! % 113.04/16.44 % (2777648)------------------------------ % 113.04/16.44 % (2777648)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 113.04/16.44 % (2777648)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.04/16.44 % (2777648)CaDiCaL version: 2.1.3 % 113.04/16.44 % (2777648)Termination reason: Instruction limit % 113.04/16.44 % (2777648)Termination phase: Saturation % 113.04/16.44 % (2777648)Time elapsed: 0.070 s % 113.04/16.44 % (2777648)Peak memory usage: 13 MB % 113.04/16.44 % (2777648)Instructions burned: 209 (million) % 113.04/16.44 % (2777651)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=2083268406:i=232:rtra=on_2863 on theBenchmark for (2863ds/232Mi) % 113.04/16.44 % (2777651)Instruction limit reached! % 113.04/16.44 % (2777651)------------------------------ % 113.04/16.44 % (2777651)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 113.04/16.44 % (2777651)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.04/16.44 % (2777651)CaDiCaL version: 2.1.3 % 113.04/16.44 % (2777651)Termination reason: Instruction limit % 113.04/16.44 % (2777651)Termination phase: Saturation % 113.04/16.44 % (2777651)Time elapsed: 0.078 s % 113.04/16.44 % (2777651)Peak memory usage: 13 MB % 113.04/16.44 % (2777651)Instructions burned: 234 (million) % 113.04/16.44 % (2777678)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=506389067:i=262:rtra=on_2862 on theBenchmark for (2862ds/262Mi) % 113.04/16.44 % (2777678)Instruction limit reached! % 113.04/16.44 % (2777678)------------------------------ % 113.04/16.44 % (2777678)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 113.04/16.44 % (2777678)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.04/16.44 % (2777678)CaDiCaL version: 2.1.3 % 113.04/16.44 % (2777678)Termination reason: Instruction limit % 113.04/16.44 % (2777678)Termination phase: Saturation % 113.04/16.44 % (2777678)Time elapsed: 0.092 s % 113.04/16.44 % (2777678)Peak memory usage: 14 MB % 113.04/16.44 % (2777678)Instructions burned: 262 (million) % 113.04/16.44 % (2777711)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=1498082805:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2861 on theBenchmark for (2861ds/318Mi) % 113.04/16.44 % (2777711)Instruction limit reached! % 113.04/16.44 % (2777711)------------------------------ % 113.04/16.44 % (2777711)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 113.04/16.44 % (2777711)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.04/16.44 % (2777711)CaDiCaL version: 2.1.3 % 113.04/16.44 % (2777711)Termination reason: Instruction limit % 113.04/16.44 % (2777711)Termination phase: Saturation % 113.04/16.44 % (2777711)Time elapsed: 0.120 s % 113.04/16.44 % (2777711)Peak memory usage: 15 MB % 113.04/16.44 % (2777711)Instructions burned: 320 (million) % 113.04/16.44 % (2777772)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=674033718:i=1428:nm=2:rtra=on_2860 on theBenchmark for (2860ds/1428Mi) % 113.04/16.44 % (2777772)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 113.04/16.44 % (2777772)Terminated due to inappropriate strategy. % 113.04/16.44 % (2777772)------------------------------ % 113.04/16.44 % (2777772)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 113.04/16.44 % (2777772)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.04/16.44 % (2777772)CaDiCaL version: 2.1.3 % 113.04/16.44 % (2777772)Termination reason: Inappropriate % 113.04/16.44 % (2777772)Time elapsed: 0.0000 s % 113.04/16.44 % (2777772)Peak memory usage: 10 MB % 113.04/16.44 % (2777772)Instructions burned: 1 (million) % 113.04/16.44 % (2777772)------------------------------ % 113.04/16.44 % (2777772)------------------------------ % 113.04/16.44 % (2777774)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=1408537062:i=262:bd=preordered:rtra=on:fsd=on_2860 on theBenchmark for (2860ds/262Mi) % 127.38/18.45 % (2777774)Instruction limit reached! % 127.38/18.45 % (2777774)------------------------------ % 127.38/18.45 % (2777774)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 127.38/18.45 % (2777774)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 127.38/18.45 % (2777774)CaDiCaL version: 2.1.3 % 127.38/18.45 % (2777774)Termination reason: Instruction limit % 127.38/18.45 % (2777774)Termination phase: Saturation % 127.38/18.45 % (2777774)Time elapsed: 0.096 s % 127.38/18.45 % (2777774)Peak memory usage: 14 MB % 127.38/18.45 % (2777774)Instructions burned: 262 (million) % 127.38/18.45 % (2777776)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=2554479949:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2859 on theBenchmark for (2859ds/1368Mi) % 127.38/18.45 % (2777776)Instruction limit reached! % 127.38/18.45 % (2777776)------------------------------ % 127.38/18.45 % (2777776)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 127.38/18.45 % (2777776)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 127.38/18.45 % (2777776)CaDiCaL version: 2.1.3 % 127.38/18.45 % (2777776)Termination reason: Instruction limit % 127.38/18.45 % (2777776)Termination phase: Saturation % 127.38/18.45 % (2777776)Time elapsed: 0.410 s % 127.38/18.45 % (2777776)Peak memory usage: 19 MB % 127.38/18.45 % (2777776)Instructions burned: 1368 (million) % 127.38/18.45 % (2777844)ott-21_1_sil=16000:si=on:fs=off:random_seed=854838706:i=360:av=off:fsr=off:rtra=on_2854 on theBenchmark for (2854ds/360Mi) % 127.38/18.45 % (2777844)Instruction limit reached! % 127.38/18.45 % (2777844)------------------------------ % 127.38/18.45 % (2777844)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 127.38/18.45 % (2777844)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 127.38/18.45 % (2777844)CaDiCaL version: 2.1.3 % 127.38/18.45 % (2777844)Termination reason: Instruction limit % 127.38/18.45 % (2777844)Termination phase: Saturation % 127.38/18.45 % (2777844)Time elapsed: 0.088 s % 127.38/18.45 % (2777844)Peak memory usage: 13 MB % 127.38/18.45 % (2777844)Instructions burned: 360 (million) % 127.38/18.45 % (2777875)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3385829487:i=954:bd=all:rtra=on_2853 on theBenchmark for (2853ds/954Mi) % 127.38/18.45 % (2777875)Instruction limit reached! % 127.38/18.45 % (2777875)------------------------------ % 127.38/18.45 % (2777875)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 127.38/18.45 % (2777875)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 127.38/18.45 % (2777875)CaDiCaL version: 2.1.3 % 127.38/18.45 % (2777875)Termination reason: Instruction limit % 127.38/18.45 % (2777875)Termination phase: Saturation % 127.38/18.45 % (2777875)Time elapsed: 0.355 s % 127.38/18.45 % (2777875)Peak memory usage: 17 MB % 127.38/18.45 % (2777875)Instructions burned: 954 (million) % 127.38/18.45 % (2777919)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=1501368014:fmbsr=1.3:i=1730:ins=25:rtra=on_2850 on theBenchmark for (2850ds/1730Mi) % 127.38/18.45 % (2777919)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 127.38/18.45 % (2777919)Terminated due to inappropriate strategy. % 127.38/18.45 % (2777919)------------------------------ % 127.38/18.45 % (2777919)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 127.38/18.45 % (2777919)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 127.38/18.45 % (2777919)CaDiCaL version: 2.1.3 % 127.38/18.45 % (2777919)Termination reason: Inappropriate % 127.38/18.45 % (2777919)Time elapsed: 0.001 s % 127.38/18.45 % (2777919)Peak memory usage: 10 MB % 127.38/18.45 % (2777919)------------------------------ % 127.38/18.45 % (2777919)------------------------------ % 127.38/18.45 % (2777925)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=1046859271:i=2358:rtra=on_2849 on theBenchmark for (2849ds/2358Mi) % 127.38/18.45 % (2777925)Instruction limit reached! % 127.38/18.45 % (2777925)------------------------------ % 127.38/18.45 % (2777925)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 127.38/18.45 % (2777925)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 127.38/18.45 % (2777925)CaDiCaL version: 2.1.3 % 127.38/18.45 % (2777925)Termination reason: Instruction limit % 127.38/18.45 % (2777925)Termination phase: Saturation % 127.38/18.45 % (2777925)Time elapsed: 0.563 s % 127.38/18.45 % (2777925)Peak memory usage: 24 MB % 127.38/18.45 % (2777925)Instructions burned: 2363 (million) % 155.83/22.50 % (2778082)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=2491378836:i=1778:ins=1:rtra=on_2843 on theBenchmark for (2843ds/1778Mi) % 155.83/22.50 % (2778082)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 155.83/22.50 % (2778082)Terminated due to inappropriate strategy. % 155.83/22.50 % (2778082)------------------------------ % 155.83/22.50 % (2778082)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 155.83/22.50 % (2778082)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.83/22.50 % (2778082)CaDiCaL version: 2.1.3 % 155.83/22.50 % (2778082)Termination reason: Inappropriate % 155.83/22.50 % (2778082)Time elapsed: 0.0000 s % 155.83/22.50 % (2778082)Peak memory usage: 10 MB % 155.83/22.50 % (2778082)Instructions burned: 1 (million) % 155.83/22.50 % (2778082)------------------------------ % 155.83/22.50 % (2778082)------------------------------ % 155.83/22.50 % (2778084)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=1127976017:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2843 on theBenchmark for (2843ds/1384Mi) % 155.83/22.50 % (2777630)Instruction limit reached! % 155.83/22.50 % (2777630)------------------------------ % 155.83/22.50 % (2777630)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 155.83/22.50 % (2777630)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.83/22.50 % (2777630)CaDiCaL version: 2.1.3 % 155.83/22.50 % (2777630)Termination reason: Instruction limit % 155.83/22.50 % (2777630)Termination phase: Saturation % 155.83/22.50 % (2777630)Time elapsed: 6.027 s % 155.83/22.50 % (2777630)Peak memory usage: 22 MB % 155.83/22.50 % (2777630)Instructions burned: 28121 (million) % 155.83/22.50 % (2778086)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=2747426574:i=1758:kws=inv_precedence:fsr=off:rtra=on_2841 on theBenchmark for (2841ds/1758Mi) % 155.83/22.50 % (2778084)Instruction limit reached! % 155.83/22.50 % (2778084)------------------------------ % 155.83/22.50 % (2778084)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 155.83/22.50 % (2778084)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.83/22.50 % (2778084)CaDiCaL version: 2.1.3 % 155.83/22.50 % (2778084)Termination reason: Instruction limit % 155.83/22.50 % (2778084)Termination phase: Saturation % 155.83/22.50 % (2778084)Time elapsed: 0.436 s % 155.83/22.50 % (2778084)Peak memory usage: 19 MB % 155.83/22.50 % (2778084)Instructions burned: 1384 (million) % 155.83/22.50 % (2778088)fmb+10_1_sil=64000:si=on:random_seed=2601148817:i=44122:nm=2:rtra=on:gsp=on_2839 on theBenchmark for (2839ds/44122Mi) % 155.83/22.50 % (2778088)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 155.83/22.50 % (2778088)Terminated due to inappropriate strategy. % 155.83/22.50 % (2778088)------------------------------ % 155.83/22.50 % (2778088)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 155.83/22.50 % (2778088)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.83/22.50 % (2778088)CaDiCaL version: 2.1.3 % 155.83/22.50 % (2778088)Termination reason: Inappropriate % 155.83/22.50 % (2778088)Time elapsed: 0.0000 s % 155.83/22.50 % (2778088)Peak memory usage: 10 MB % 155.83/22.50 % (2778088)Instructions burned: 1 (million) % 155.83/22.50 % (2778088)------------------------------ % 155.83/22.50 % (2778088)------------------------------ % 155.83/22.50 % (2778090)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=623300535:i=19030:nm=5:rtra=on_2839 on theBenchmark for (2839ds/19030Mi) % 155.83/22.50 % (2778090)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 155.83/22.50 % (2778090)Terminated due to inappropriate strategy. % 155.83/22.50 % (2778090)------------------------------ % 155.83/22.50 % (2778090)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 155.83/22.50 % (2778090)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.83/22.50 % (2778090)CaDiCaL version: 2.1.3 % 155.83/22.50 % (2778090)Termination reason: Inappropriate % 155.83/22.50 % (2778090)Time elapsed: 0.0000 s % 155.83/22.50 % (2778090)Peak memory usage: 10 MB % 155.83/22.50 % (2778090)Instructions burned: 1 (million) % 155.83/22.50 % (2778090)------------------------------ % 155.83/22.50 % (2778090)------------------------------ % 155.83/22.50 % (2778092)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=1307323555:fmbsr=1.7:i=1840:rtra=on_2839 on theBenchmark for (2839ds/1840Mi) % 155.83/22.50 % (2778092)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 168.98/24.37 % (2778092)Terminated due to inappropriate strategy. % 168.98/24.37 % (2778092)------------------------------ % 168.98/24.37 % (2778092)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 168.98/24.37 % (2778092)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 168.98/24.37 % (2778092)CaDiCaL version: 2.1.3 % 168.98/24.37 % (2778092)Termination reason: Inappropriate % 168.98/24.37 % (2778092)Time elapsed: 0.0000 s % 168.98/24.37 % (2778092)Peak memory usage: 10 MB % 168.98/24.37 % (2778092)Instructions burned: 1 (million) % 168.98/24.37 % (2778092)------------------------------ % 168.98/24.37 % (2778092)------------------------------ % 168.98/24.37 % (2778094)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=3324656548:i=10262:rtra=on_2838 on theBenchmark for (2838ds/10262Mi) % 168.98/24.37 % (2778086)Instruction limit reached! % 168.98/24.37 % (2778086)------------------------------ % 168.98/24.37 % (2778086)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 168.98/24.37 % (2778086)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 168.98/24.37 % (2778086)CaDiCaL version: 2.1.3 % 168.98/24.37 % (2778086)Termination reason: Instruction limit % 168.98/24.37 % (2778086)Termination phase: Saturation % 168.98/24.37 % (2778086)Time elapsed: 0.546 s % 168.98/24.37 % (2778086)Peak memory usage: 24 MB % 168.98/24.37 % (2778086)Instructions burned: 1759 (million) % 168.98/24.37 % (2778096)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=238414093:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2835 on theBenchmark for (2835ds/2944Mi) % 168.98/24.37 % (2778096)Instruction limit reached! % 168.98/24.37 % (2778096)------------------------------ % 168.98/24.37 % (2778096)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 168.98/24.37 % (2778096)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 168.98/24.37 % (2778096)CaDiCaL version: 2.1.3 % 168.98/24.37 % (2778096)Termination reason: Instruction limit % 168.98/24.37 % (2778096)Termination phase: Saturation % 168.98/24.37 % (2778096)Time elapsed: 1.034 s % 168.98/24.37 % (2778096)Peak memory usage: 30 MB % 168.98/24.37 % (2778096)Instructions burned: 2944 (million) % 168.98/24.37 % (2778098)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=171052921:i=12648:rtra=on_2825 on theBenchmark for (2825ds/12648Mi) % 168.98/24.37 % (2778098)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 168.98/24.37 % (2778098)Terminated due to inappropriate strategy. % 168.98/24.37 % (2778098)------------------------------ % 168.98/24.37 % (2778098)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 168.98/24.37 % (2778098)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 168.98/24.37 % (2778098)CaDiCaL version: 2.1.3 % 168.98/24.37 % (2778098)Termination reason: Inappropriate % 168.98/24.37 % (2778098)Time elapsed: 0.0000 s % 168.98/24.37 % (2778098)Peak memory usage: 10 MB % 168.98/24.37 % (2778098)Instructions burned: 1 (million) % 168.98/24.37 % (2778098)------------------------------ % 168.98/24.37 % (2778098)------------------------------ % 168.98/24.37 % (2778100)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=3877091889:fmbsr=2.30978:i=4348:rtra=on_2825 on theBenchmark for (2825ds/4348Mi) % 168.98/24.37 % (2778100)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 168.98/24.37 % (2778100)Terminated due to inappropriate strategy. % 168.98/24.37 % (2778100)------------------------------ % 168.98/24.37 % (2778100)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 168.98/24.37 % (2778100)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 168.98/24.37 % (2778100)CaDiCaL version: 2.1.3 % 168.98/24.37 % (2778100)Termination reason: Inappropriate % 168.98/24.37 % (2778100)Time elapsed: 0.0000 s % 168.98/24.37 % (2778100)Peak memory usage: 10 MB % 168.98/24.37 % (2778100)Instructions burned: 1 (million) % 168.98/24.37 % (2778100)------------------------------ % 168.98/24.37 % (2778100)------------------------------ % 168.98/24.37 % (2778102)ott-2_1_sil=16000:si=on:newcnf=on:random_seed=3211430815:avsq=on:i=1738:avsqr=1,16:kws=inv_arity_squared:rtra=on_2825 on theBenchmark for (2825ds/1738Mi) % 168.98/24.37 % (2778102)Instruction limit reached! % 168.98/24.37 % (2778102)------------------------------ % 168.98/24.37 % (2778102)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 168.98/24.37 % (2778102)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 225.43/32.33 % (2778102)CaDiCaL version: 2.1.3 % 225.43/32.33 % (2778102)Termination reason: Instruction limit % 225.43/32.33 % (2778102)Termination phase: Saturation % 225.43/32.33 % (2778102)Time elapsed: 0.609 s % 225.43/32.33 % (2778102)Peak memory usage: 17 MB % 225.43/32.33 % (2778102)Instructions burned: 1740 (million) % 225.43/32.33 % (2778104)ott+10_1_sil=32000:tgt=ground:si=on:random_seed=3588451135:i=10228:av=off:rtra=on_2818 on theBenchmark for (2818ds/10228Mi) % 225.43/32.33 % (2778094)Instruction limit reached! % 225.43/32.33 % (2778094)------------------------------ % 225.43/32.33 % (2778094)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 225.43/32.33 % (2778094)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 225.43/32.33 % (2778094)CaDiCaL version: 2.1.3 % 225.43/32.33 % (2778094)Termination reason: Instruction limit % 225.43/32.33 % (2778094)Termination phase: Saturation % 225.43/32.33 % (2778094)Time elapsed: 3.293 s % 225.43/32.33 % (2778094)Peak memory usage: 69 MB % 225.43/32.33 % (2778094)Instructions burned: 10263 (million) % 225.43/32.33 % (2778106)fmb+10_1_sil=64000:sas=cadical:si=on:bce=on:rp=on:random_seed=1119136196:i=108564:rtra=on_2805 on theBenchmark for (2805ds/108564Mi) % 225.43/32.33 % (2778106)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 225.43/32.33 % (2778106)Terminated due to inappropriate strategy. % 225.43/32.33 % (2778106)------------------------------ % 225.43/32.33 % (2778106)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 225.43/32.33 % (2778106)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 225.43/32.33 % (2778106)CaDiCaL version: 2.1.3 % 225.43/32.33 % (2778106)Termination reason: Inappropriate % 225.43/32.33 % (2778106)Time elapsed: 0.0000 s % 225.43/32.33 % (2778106)Peak memory usage: 10 MB % 225.43/32.33 % (2778106)Instructions burned: 1 (million) % 225.43/32.33 % (2778106)------------------------------ % 225.43/32.33 % (2778106)------------------------------ % 225.43/32.33 % (2778108)dis-11_1_sil=16000:si=on:sp=reverse_frequency:alpa=true:random_seed=1765230521:i=7024:aac=none:rtra=on_2805 on theBenchmark for (2805ds/7024Mi) % 225.43/32.33 % (2777536)Instruction limit reached! % 225.43/32.33 % (2777536)------------------------------ % 225.43/32.33 % (2777536)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 225.43/32.33 % (2777536)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 225.43/32.33 % (2777536)CaDiCaL version: 2.1.3 % 225.43/32.33 % (2777536)Termination reason: Instruction limit % 225.43/32.33 % (2777536)Termination phase: Saturation % 225.43/32.33 % (2777536)Time elapsed: 21.466 s % 225.43/32.33 % (2777536)Peak memory usage: 1092 MB % 225.43/32.33 % (2777536)Instructions burned: 88028 (million) % 225.43/32.33 % (2778110)dis+21_1_sil=32000:sas=cadical:si=on:random_seed=3740080379:i=7546:rtra=on:amm=off_2784 on theBenchmark for (2784ds/7546Mi) % 225.43/32.33 % (2778108)Instruction limit reached! % 225.43/32.33 % (2778108)------------------------------ % 225.43/32.33 % (2778108)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 225.43/32.33 % (2778108)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 225.43/32.33 % (2778108)CaDiCaL version: 2.1.3 % 225.43/32.33 % (2778108)Termination reason: Instruction limit % 225.43/32.33 % (2778108)Termination phase: Saturation % 225.43/32.33 % (2778108)Time elapsed: 2.219 s % 225.43/32.33 % (2778108)Peak memory usage: 56 MB % 225.43/32.33 % (2778108)Instructions burned: 7025 (million) % 225.43/32.33 % (2778112)ott+11_1_sil=16000:si=on:gs=on:random_seed=3223694015:s2a=on:i=4502:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:rtra=on:fsd=on_2783 on theBenchmark for (2783ds/4502Mi) % 225.43/32.33 % (2778104)Instruction limit reached! % 225.43/32.33 % (2778104)------------------------------ % 225.43/32.33 % (2778104)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 225.43/32.33 % (2778104)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 225.43/32.33 % (2778104)CaDiCaL version: 2.1.3 % 225.43/32.33 % (2778104)Termination reason: Instruction limit % 225.43/32.33 % (2778104)Termination phase: Saturation % 225.43/32.33 % (2778104)Time elapsed: 4.023 s % 225.43/32.33 % (2778104)Peak memory usage: 53 MB % 225.43/32.33 % (2778104)Instructions burned: 10230 (million) % 225.43/32.33 % (2778114)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:si=on:fmbss=7:random_seed=3249453209:fmbsr=1.6:i=135068:rtra=on_2778 on theBenchmark for (2778ds/135068Mi) % 225.43/32.33 % (2778114)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 225.43/32.33 % (2778114)Terminated due to inappropriate strategy. % 225.43/32.33 % (2778114)------------------------------ % 300.11/42.93 % (2778114)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.11/42.93 % (2778114)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.11/42.93 % (2778114)CaDiCaL version: 2.1.3 % 300.11/42.93 % (2778114)Termination reason: Inappropriate % 300.11/42.93 % (2778114)Time elapsed: 0.0000 s % 300.11/42.93 % (2778114)Peak memory usage: 10 MB % 300.11/42.93 % (2778114)Instructions burned: 1 (million) % 300.11/42.93 % (2778114)------------------------------ % 300.11/42.93 % (2778114)------------------------------ % 300.11/42.93 % (2778116)ott-22_32_sil=16000:tgt=full:si=on:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=419767951:avsq=on:i=9182:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:rtra=on:fdi=4_2778 on theBenchmark for (2778ds/9182Mi) % 300.11/42.93 % (2777626)Instruction limit reached! % 300.11/42.93 % (2777626)------------------------------ % 300.11/42.93 % (2777626)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.11/42.93 % (2777626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.11/42.93 % (2777626)CaDiCaL version: 2.1.3 % 300.11/42.93 % (2777626)Termination reason: Instruction limit % 300.11/42.93 % (2777626)Termination phase: Saturation % 300.11/42.93 % (2777626)Time elapsed: 13.935 s % 300.11/42.93 % (2777626)Peak memory usage: 227 MB % 300.11/42.93 % (2777626)Instructions burned: 53295 (million) % 300.11/42.93 % (2778118)dis+10_64_to=lpo:sil=32000:si=on:spb=intro:urr=on:sac=on:random_seed=3375952331:i=58680:rtra=on_2772 on theBenchmark for (2772ds/58680Mi) % 300.11/42.93 % (2778112)Instruction limit reached! % 300.11/42.93 % (2778112)------------------------------ % 300.11/42.93 % (2778112)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.11/42.93 % (2778112)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.11/42.93 % (2778112)CaDiCaL version: 2.1.3 % 300.11/42.93 % (2778112)Termination reason: Instruction limit % 300.11/42.93 % (2778112)Termination phase: Saturation % 300.11/42.93 % (2778112)Time elapsed: 1.526 s % 300.11/42.93 % (2778112)Peak memory usage: 34 MB % 300.11/42.93 % (2778112)Instructions burned: 4505 (million) % 300.11/42.93 % (2778120)dis-10_1_sil=64000:sas=cadical:si=on:cn=on:random_seed=2636575063:i=10422:rtra=on_2767 on theBenchmark for (2767ds/10422Mi) % 300.11/42.93 % (2778110)Instruction limit reached! % 300.11/42.93 % (2778110)------------------------------ % 300.11/42.93 % (2778110)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.11/42.93 % (2778110)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.11/42.93 % (2778110)CaDiCaL version: 2.1.3 % 300.11/42.93 % (2778110)Termination reason: Instruction limit % 300.11/42.93 % (2778110)Termination phase: Saturation % 300.11/42.93 % (2778110)Time elapsed: 2.416 s % 300.11/42.93 % (2778110)Peak memory usage: 51 MB % 300.11/42.93 % (2778110)Instructions burned: 7547 (million) % 300.11/42.93 % (2778122)fmb+10_1_sil=32000:sas=cadical:si=on:bce=on:fmbss=17:random_seed=1300121361:i=10994:nm=2:rtra=on_2759 on theBenchmark for (2759ds/10994Mi) % 300.11/42.93 % (2778122)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.11/42.93 % (2778122)Terminated due to inappropriate strategy. % 300.11/42.93 % (2778122)------------------------------ % 300.11/42.93 % (2778122)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.11/42.93 % (2778122)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.11/42.93 % (2778122)CaDiCaL version: 2.1.3 % 300.11/42.93 % (2778122)Termination reason: Inappropriate % 300.11/42.93 % (2778122)Time elapsed: 0.0000 s % 300.11/42.93 % (2778122)Peak memory usage: 10 MB % 300.11/42.93 % (2778122)Instructions burned: 1 (million) % 300.11/42.93 % (2778122)------------------------------ % 300.11/42.93 % (2778122)------------------------------ % 300.11/42.93 % (2778124)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:si=on:fmbss=15:random_seed=3027020518:fmbsr=2:i=92664:rtra=on_2759 on theBenchmark for (2759ds/92664Mi) % 300.11/42.93 % (2778124)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.11/42.93 % (2778124)Terminated due to inappropriate strategy. % 300.11/42.93 % (2778124)------------------------------ % 300.11/42.93 % (2778124)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.11/42.93 % (2778124)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.11/42.93 % (2778124)CaDiCaL version: 2.1.3 % 300.11/42.93 % (2778124)Termination reason: Inappropriate % 300.11/42.93 % (2778124)Time elapsed: 0.0000 s % 300.11/42.93 % (277812 % 300.11/42.93 Terminated % 300.11/42.93 % Vampire exiting %------------------------------------------------------------------------------