%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWC445_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 : n026.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.27s 42.54s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : SWC445_1 : TPTP v9.3.1. Released v9.0.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.07/0.19 % Computer : n026.cluster.edu % 0.07/0.19 % Model : x86_64 x86_64 % 0.07/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.07/0.19 % Memory : 8046.5625MB % 0.07/0.19 % OS : Linux 6.8.0-71-generic % 0.07/0.19 % CPULimit : 300 % 0.07/0.19 % WCLimit : 300 % 0.07/0.19 % DateTime : Mon Sep 28 09:40:56 UTC 2026 % 0.07/0.19 % CPUTime : % 0.07/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.07/0.22 Running first-order model finding % 0.07/0.22 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 % 3.88/0.85 % (3725483)Will run a generic schedule for satisfiability detection. % 3.88/0.85 % (3725489)% WARNING: option uhcvi not known. % 3.88/0.85 % (3725489)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=707758136:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 3.88/0.85 % (3725488)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1693720480_2999 on theBenchmark for (2999ds/0Mi) % 3.88/0.85 % (3725490)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=658178852:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 3.88/0.85 % (3725493)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3936229747:i=131_2999 on theBenchmark for (2999ds/131Mi) % 3.88/0.85 % (3725491)dis+10_1_sil=32000:sp=arity:random_seed=515607465:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 3.88/0.85 % (3725492)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2551515762:i=116_2999 on theBenchmark for (2999ds/116Mi) % 3.88/0.85 % (3725494)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1306654872:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 3.88/0.85 % (3725488)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.88/0.85 % (3725488)Terminated due to inappropriate strategy. % 3.88/0.85 % (3725488)------------------------------ % 3.88/0.85 % (3725488)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.88/0.85 % (3725488)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.88/0.85 % (3725488)CaDiCaL version: 2.1.3 % 3.88/0.85 % (3725488)Termination reason: Inappropriate % 3.88/0.85 % (3725488)Time elapsed: 0.001 s % 3.88/0.85 % (3725488)Peak memory usage: 10 MB % 3.88/0.85 % (3725488)Instructions burned: 1 (million) % 3.88/0.85 % (3725488)------------------------------ % 3.88/0.85 % (3725488)------------------------------ % 3.88/0.85 % (3725502)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2239921743:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 3.88/0.85 % (3725502)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.88/0.85 % (3725502)Terminated due to inappropriate strategy. % 3.88/0.85 % (3725502)------------------------------ % 3.88/0.85 % (3725502)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.88/0.85 % (3725502)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.88/0.85 % (3725502)CaDiCaL version: 2.1.3 % 3.88/0.85 % (3725502)Termination reason: Inappropriate % 3.88/0.85 % (3725502)Time elapsed: 0.001 s % 3.88/0.85 % (3725502)Peak memory usage: 10 MB % 3.88/0.85 % (3725502)Instructions burned: 1 (million) % 3.88/0.85 % (3725502)------------------------------ % 3.88/0.85 % (3725502)------------------------------ % 3.88/0.85 % (3725504)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3076673912:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 3.88/0.85 % (3725491)Instruction limit reached! % 3.88/0.85 % (3725491)------------------------------ % 3.88/0.85 % (3725491)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.88/0.85 % (3725491)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.88/0.85 % (3725491)CaDiCaL version: 2.1.3 % 3.88/0.85 % (3725491)Termination reason: Instruction limit % 3.88/0.85 % (3725491)Termination phase: Saturation % 3.88/0.85 % (3725491)Time elapsed: 0.064 s % 3.88/0.85 % (3725491)Peak memory usage: 12 MB % 3.88/0.85 % (3725491)Instructions burned: 105 (million) % 3.88/0.85 % (3725492)Instruction limit reached! % 3.88/0.85 % (3725492)------------------------------ % 3.88/0.85 % (3725492)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.88/0.85 % (3725492)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.88/0.85 % (3725492)CaDiCaL version: 2.1.3 % 3.88/0.85 % (3725492)Termination reason: Instruction limit % 3.88/0.85 % (3725492)Termination phase: Saturation % 3.88/0.85 % (3725492)Time elapsed: 0.071 s % 3.88/0.85 % (3725492)Peak memory usage: 12 MB % 3.88/0.85 % (3725492)Instructions burned: 116 (million) % 3.88/0.85 % (3725493)Instruction limit reached! % 3.88/0.85 % (3725493)------------------------------ % 3.88/0.85 % (3725493)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.88/0.85 % (3725493)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.88/0.85 % (3725493)CaDiCaL version: 2.1.3 % 3.88/0.85 % (3725493)Termination reason: Instruction limit % 5.68/1.10 % (3725493)Termination phase: Saturation % 5.68/1.10 % (3725493)Time elapsed: 0.080 s % 5.68/1.10 % (3725493)Peak memory usage: 13 MB % 5.68/1.10 % (3725493)Instructions burned: 131 (million) % 5.68/1.10 % (3725506)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=1640829381:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 5.68/1.10 % (3725507)ott-21_1_sil=16000:fs=off:random_seed=70472685:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 5.68/1.10 % (3725508)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3980924867:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 5.68/1.10 % (3725494)Instruction limit reached! % 5.68/1.10 % (3725494)------------------------------ % 5.68/1.10 % (3725494)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.68/1.10 % (3725494)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.68/1.10 % (3725494)CaDiCaL version: 2.1.3 % 5.68/1.10 % (3725494)Termination reason: Instruction limit % 5.68/1.10 % (3725494)Termination phase: Saturation % 5.68/1.10 % (3725494)Time elapsed: 0.107 s % 5.68/1.10 % (3725494)Peak memory usage: 13 MB % 5.68/1.10 % (3725494)Instructions burned: 159 (million) % 5.68/1.10 % (3725504)Instruction limit reached! % 5.68/1.10 % (3725504)------------------------------ % 5.68/1.10 % (3725504)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.68/1.10 % (3725504)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.68/1.10 % (3725504)CaDiCaL version: 2.1.3 % 5.68/1.10 % (3725504)Termination reason: Instruction limit % 5.68/1.10 % (3725504)Termination phase: Saturation % 5.68/1.10 % (3725504)Time elapsed: 0.082 s % 5.68/1.10 % (3725504)Peak memory usage: 12 MB % 5.68/1.10 % (3725504)Instructions burned: 131 (million) % 5.68/1.10 % (3725512)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2850303058:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 5.68/1.10 % (3725512)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 5.68/1.10 % (3725512)Terminated due to inappropriate strategy. % 5.68/1.10 % (3725512)------------------------------ % 5.68/1.10 % (3725512)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.68/1.10 % (3725512)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.68/1.10 % (3725512)CaDiCaL version: 2.1.3 % 5.68/1.10 % (3725512)Termination reason: Inappropriate % 5.68/1.10 % (3725512)Time elapsed: 0.001 s % 5.68/1.10 % (3725512)Peak memory usage: 10 MB % 5.68/1.10 % (3725512)Instructions burned: 1 (million) % 5.68/1.10 % (3725512)------------------------------ % 5.68/1.10 % (3725512)------------------------------ % 5.68/1.10 % (3725513)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2570083966:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 5.68/1.10 % (3725515)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2271873425:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 5.68/1.10 % (3725515)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 5.68/1.10 % (3725515)Terminated due to inappropriate strategy. % 5.68/1.10 % (3725515)------------------------------ % 5.68/1.10 % (3725515)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.68/1.10 % (3725515)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.68/1.10 % (3725515)CaDiCaL version: 2.1.3 % 5.68/1.10 % (3725515)Termination reason: Inappropriate % 5.68/1.10 % (3725515)Time elapsed: 0.001 s % 5.68/1.10 % (3725515)Peak memory usage: 10 MB % 5.68/1.10 % (3725515)Instructions burned: 1 (million) % 5.68/1.10 % (3725515)------------------------------ % 5.68/1.10 % (3725515)------------------------------ % 5.68/1.10 % (3725518)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=2837029807: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) % 5.68/1.10 % (3725507)Instruction limit reached! % 5.68/1.10 % (3725507)------------------------------ % 5.68/1.10 % (3725507)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.68/1.10 % (3725507)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.68/1.10 % (3725507)CaDiCaL version: 2.1.3 % 5.68/1.10 % (3725507)Termination reason: Instruction limit % 5.68/1.10 % (3725507)Termination phase: Saturation % 22.47/3.45 % (3725507)Time elapsed: 0.083 s % 22.47/3.45 % (3725507)Peak memory usage: 12 MB % 22.47/3.45 % (3725507)Instructions burned: 182 (million) % 22.47/3.45 % (3725520)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3276649085:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 22.47/3.45 % (3725508)Instruction limit reached! % 22.47/3.45 % (3725508)------------------------------ % 22.47/3.45 % (3725508)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.47/3.45 % (3725508)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.47/3.45 % (3725508)CaDiCaL version: 2.1.3 % 22.47/3.45 % (3725508)Termination reason: Instruction limit % 22.47/3.45 % (3725508)Termination phase: Saturation % 22.47/3.45 % (3725508)Time elapsed: 0.299 s % 22.47/3.45 % (3725508)Peak memory usage: 14 MB % 22.47/3.45 % (3725508)Instructions burned: 478 (million) % 22.47/3.45 % (3725522)fmb+10_1_sil=64000:random_seed=2110671565:i=22061:nm=2:gsp=on_2995 on theBenchmark for (2995ds/22061Mi) % 22.47/3.45 % (3725522)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 22.47/3.45 % (3725522)Terminated due to inappropriate strategy. % 22.47/3.45 % (3725522)------------------------------ % 22.47/3.45 % (3725522)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.47/3.45 % (3725522)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.47/3.45 % (3725522)CaDiCaL version: 2.1.3 % 22.47/3.45 % (3725522)Termination reason: Inappropriate % 22.47/3.45 % (3725522)Time elapsed: 0.001 s % 22.47/3.45 % (3725522)Peak memory usage: 10 MB % 22.47/3.45 % (3725522)Instructions burned: 1 (million) % 22.47/3.45 % (3725522)------------------------------ % 22.47/3.45 % (3725522)------------------------------ % 22.47/3.45 % (3725524)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=236540939:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi) % 22.47/3.45 % (3725524)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 22.47/3.45 % (3725524)Terminated due to inappropriate strategy. % 22.47/3.45 % (3725524)------------------------------ % 22.47/3.45 % (3725524)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.47/3.45 % (3725524)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.47/3.45 % (3725524)CaDiCaL version: 2.1.3 % 22.47/3.45 % (3725524)Termination reason: Inappropriate % 22.47/3.45 % (3725524)Time elapsed: 0.001 s % 22.47/3.45 % (3725524)Peak memory usage: 10 MB % 22.47/3.45 % (3725524)Instructions burned: 1 (million) % 22.47/3.45 % (3725524)------------------------------ % 22.47/3.45 % (3725524)------------------------------ % 22.47/3.45 % (3725506)Instruction limit reached! % 22.47/3.45 % (3725506)------------------------------ % 22.47/3.45 % (3725506)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.47/3.45 % (3725506)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.47/3.45 % (3725506)CaDiCaL version: 2.1.3 % 22.47/3.45 % (3725506)Termination reason: Instruction limit % 22.47/3.45 % (3725506)Termination phase: Saturation % 22.47/3.45 % (3725506)Time elapsed: 0.359 s % 22.47/3.45 % (3725506)Peak memory usage: 17 MB % 22.47/3.45 % (3725506)Instructions burned: 684 (million) % 22.47/3.45 % (3725526)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2202779687:fmbsr=1.7:i=920_2995 on theBenchmark for (2995ds/920Mi) % 22.47/3.45 % (3725526)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 22.47/3.45 % (3725526)Terminated due to inappropriate strategy. % 22.47/3.45 % (3725526)------------------------------ % 22.47/3.45 % (3725526)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.47/3.45 % (3725526)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.47/3.45 % (3725526)CaDiCaL version: 2.1.3 % 22.47/3.45 % (3725526)Termination reason: Inappropriate % 22.47/3.45 % (3725526)Time elapsed: 0.001 s % 22.47/3.45 % (3725526)Peak memory usage: 10 MB % 22.47/3.45 % (3725526)Instructions burned: 1 (million) % 22.47/3.45 % (3725526)------------------------------ % 22.47/3.45 % (3725526)------------------------------ % 22.47/3.45 % (3725527)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=4213782640:i=5131_2995 on theBenchmark for (2995ds/5131Mi) % 22.47/3.45 % (3725529)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1290316886:i=1472:ins=7:fdi=8:gsp=on_2994 on theBenchmark for (2994ds/1472Mi) % 22.47/3.45 % (3725518)Instruction limit reached! % 22.47/3.45 % (3725518)------------------------------ % 35.96/5.36 % (3725518)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 35.96/5.36 % (3725518)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.96/5.36 % (3725518)CaDiCaL version: 2.1.3 % 35.96/5.36 % (3725518)Termination reason: Instruction limit % 35.96/5.36 % (3725518)Termination phase: Saturation % 35.96/5.36 % (3725518)Time elapsed: 0.415 s % 35.96/5.36 % (3725518)Peak memory usage: 18 MB % 35.96/5.36 % (3725518)Instructions burned: 693 (million) % 35.96/5.36 % (3725532)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1049627853:i=6324_2993 on theBenchmark for (2993ds/6324Mi) % 35.96/5.36 % (3725532)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 35.96/5.36 % (3725532)Terminated due to inappropriate strategy. % 35.96/5.36 % (3725532)------------------------------ % 35.96/5.36 % (3725532)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 35.96/5.36 % (3725532)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.96/5.36 % (3725532)CaDiCaL version: 2.1.3 % 35.96/5.36 % (3725532)Termination reason: Inappropriate % 35.96/5.36 % (3725532)Time elapsed: 0.001 s % 35.96/5.36 % (3725532)Peak memory usage: 10 MB % 35.96/5.36 % (3725532)Instructions burned: 1 (million) % 35.96/5.36 % (3725532)------------------------------ % 35.96/5.36 % (3725532)------------------------------ % 35.96/5.36 % (3725534)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2949012838:fmbsr=2.30978:i=2174_2993 on theBenchmark for (2993ds/2174Mi) % 35.96/5.36 % (3725534)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 35.96/5.36 % (3725534)Terminated due to inappropriate strategy. % 35.96/5.36 % (3725534)------------------------------ % 35.96/5.36 % (3725534)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 35.96/5.36 % (3725534)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.96/5.36 % (3725534)CaDiCaL version: 2.1.3 % 35.96/5.36 % (3725534)Termination reason: Inappropriate % 35.96/5.36 % (3725534)Time elapsed: 0.001 s % 35.96/5.36 % (3725534)Peak memory usage: 10 MB % 35.96/5.36 % (3725534)Instructions burned: 1 (million) % 35.96/5.36 % (3725534)------------------------------ % 35.96/5.36 % (3725534)------------------------------ % 35.96/5.36 % (3725536)ott-2_1_sil=16000:newcnf=on:random_seed=1871906149:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2993 on theBenchmark for (2993ds/869Mi) % 35.96/5.36 % (3725520)Instruction limit reached! % 35.96/5.36 % (3725520)------------------------------ % 35.96/5.36 % (3725520)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 35.96/5.36 % (3725520)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.96/5.36 % (3725520)CaDiCaL version: 2.1.3 % 35.96/5.36 % (3725520)Termination reason: Instruction limit % 35.96/5.36 % (3725520)Termination phase: Saturation % 35.96/5.36 % (3725520)Time elapsed: 0.493 s % 35.96/5.36 % (3725520)Peak memory usage: 19 MB % 35.96/5.36 % (3725520)Instructions burned: 880 (million) % 35.96/5.36 % (3725538)ott+10_1_sil=32000:tgt=ground:random_seed=1840200387:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi) % 35.96/5.36 % (3725513)Instruction limit reached! % 35.96/5.36 % (3725513)------------------------------ % 35.96/5.36 % (3725513)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 35.96/5.36 % (3725513)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.96/5.36 % (3725513)CaDiCaL version: 2.1.3 % 35.96/5.36 % (3725513)Termination reason: Instruction limit % 35.96/5.36 % (3725513)Termination phase: Saturation % 35.96/5.36 % (3725513)Time elapsed: 0.667 s % 35.96/5.36 % (3725513)Peak memory usage: 18 MB % 35.96/5.36 % (3725513)Instructions burned: 1181 (million) % 35.96/5.36 % (3725540)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1271046238:i=54282_2991 on theBenchmark for (2991ds/54282Mi) % 35.96/5.36 % (3725540)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 35.96/5.36 % (3725540)Terminated due to inappropriate strategy. % 35.96/5.36 % (3725540)------------------------------ % 35.96/5.36 % (3725540)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 35.96/5.36 % (3725540)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.96/5.36 % (3725540)CaDiCaL version: 2.1.3 % 35.96/5.36 % (3725540)Termination reason: Inappropriate % 35.96/5.36 % (3725540)Time elapsed: 0.001 s % 35.96/5.36 % (3725540)Peak memory usage: 10 MB % 35.96/5.36 % (3725540)Instructions burned: 1 (million) % 104.10/14.99 % (3725540)------------------------------ % 104.10/14.99 % (3725540)------------------------------ % 104.10/14.99 % (3725542)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1381897453:i=3512:aac=none_2991 on theBenchmark for (2991ds/3512Mi) % 104.10/14.99 % (3725536)Instruction limit reached! % 104.10/14.99 % (3725536)------------------------------ % 104.10/14.99 % (3725536)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 104.10/14.99 % (3725536)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 104.10/14.99 % (3725536)CaDiCaL version: 2.1.3 % 104.10/14.99 % (3725536)Termination reason: Instruction limit % 104.10/14.99 % (3725536)Termination phase: Saturation % 104.10/14.99 % (3725536)Time elapsed: 0.442 s % 104.10/14.99 % (3725536)Peak memory usage: 17 MB % 104.10/14.99 % (3725536)Instructions burned: 870 (million) % 104.10/14.99 % (3725544)dis+21_1_sil=32000:sas=cadical:random_seed=4120612805:i=3773:amm=off_2988 on theBenchmark for (2988ds/3773Mi) % 104.10/14.99 % (3725529)Instruction limit reached! % 104.10/14.99 % (3725529)------------------------------ % 104.10/14.99 % (3725529)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 104.10/14.99 % (3725529)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 104.10/14.99 % (3725529)CaDiCaL version: 2.1.3 % 104.10/14.99 % (3725529)Termination reason: Instruction limit % 104.10/14.99 % (3725529)Termination phase: Saturation % 104.10/14.99 % (3725529)Time elapsed: 0.880 s % 104.10/14.99 % (3725529)Peak memory usage: 27 MB % 104.10/14.99 % (3725529)Instructions burned: 1472 (million) % 104.10/14.99 % (3725546)ott+11_1_sil=16000:gs=on:random_seed=3224329235:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2985 on theBenchmark for (2985ds/2251Mi) % 104.10/14.99 % (3725546)Instruction limit reached! % 104.10/14.99 % (3725546)------------------------------ % 104.10/14.99 % (3725546)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 104.10/14.99 % (3725546)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 104.10/14.99 % (3725546)CaDiCaL version: 2.1.3 % 104.10/14.99 % (3725546)Termination reason: Instruction limit % 104.10/14.99 % (3725546)Termination phase: Saturation % 104.10/14.99 % (3725546)Time elapsed: 1.218 s % 104.10/14.99 % (3725546)Peak memory usage: 23 MB % 104.10/14.99 % (3725546)Instructions burned: 2251 (million) % 104.10/14.99 % (3725548)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3071412704:fmbsr=1.6:i=67534_2973 on theBenchmark for (2973ds/67534Mi) % 104.10/14.99 % (3725548)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 104.10/14.99 % (3725548)Terminated due to inappropriate strategy. % 104.10/14.99 % (3725548)------------------------------ % 104.10/14.99 % (3725548)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 104.10/14.99 % (3725548)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 104.10/14.99 % (3725548)CaDiCaL version: 2.1.3 % 104.10/14.99 % (3725548)Termination reason: Inappropriate % 104.10/14.99 % (3725548)Time elapsed: 0.001 s % 104.10/14.99 % (3725548)Peak memory usage: 10 MB % 104.10/14.99 % (3725548)Instructions burned: 1 (million) % 104.10/14.99 % (3725548)------------------------------ % 104.10/14.99 % (3725548)------------------------------ % 104.10/14.99 % (3725550)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3553139047:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2973 on theBenchmark for (2973ds/4591Mi) % 104.10/14.99 % (3725542)Instruction limit reached! % 104.10/14.99 % (3725542)------------------------------ % 104.10/14.99 % (3725542)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 104.10/14.99 % (3725542)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 104.10/14.99 % (3725542)CaDiCaL version: 2.1.3 % 104.10/14.99 % (3725542)Termination reason: Instruction limit % 104.10/14.99 % (3725542)Termination phase: Saturation % 104.10/14.99 % (3725542)Time elapsed: 1.871 s % 104.10/14.99 % (3725542)Peak memory usage: 36 MB % 104.10/14.99 % (3725542)Instructions burned: 3513 (million) % 104.10/14.99 % (3725552)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1714739026:i=29340_2972 on theBenchmark for (2972ds/29340Mi) % 104.10/14.99 % (3725544)Instruction limit reached! % 104.10/14.99 % (3725544)------------------------------ % 104.10/14.99 % (3725544)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 104.10/14.99 % (3725544)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 104.10/14.99 % (3725544)CaDiCaL version: 2.1.3 % 104.10/14.99 % (3725544)Termination reason: Instruction limit % 134.15/19.15 % (3725544)Termination phase: Saturation % 134.15/19.15 % (3725544)Time elapsed: 2.075 s % 134.15/19.15 % (3725544)Peak memory usage: 33 MB % 134.15/19.15 % (3725544)Instructions burned: 3776 (million) % 134.15/19.15 % (3725554)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=4099112590:i=5211_2967 on theBenchmark for (2967ds/5211Mi) % 134.15/19.15 % (3725527)Instruction limit reached! % 134.15/19.15 % (3725527)------------------------------ % 134.15/19.15 % (3725527)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 134.15/19.15 % (3725527)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 134.15/19.15 % (3725527)CaDiCaL version: 2.1.3 % 134.15/19.15 % (3725527)Termination reason: Instruction limit % 134.15/19.15 % (3725527)Termination phase: Saturation % 134.15/19.15 % (3725527)Time elapsed: 2.791 s % 134.15/19.15 % (3725527)Peak memory usage: 42 MB % 134.15/19.15 % (3725527)Instructions burned: 5132 (million) % 134.15/19.15 % (3725556)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=325407426:i=5497:nm=2_2967 on theBenchmark for (2967ds/5497Mi) % 134.15/19.15 % (3725556)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 134.15/19.15 % (3725556)Terminated due to inappropriate strategy. % 134.15/19.15 % (3725556)------------------------------ % 134.15/19.15 % (3725556)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 134.15/19.15 % (3725556)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 134.15/19.15 % (3725556)CaDiCaL version: 2.1.3 % 134.15/19.15 % (3725556)Termination reason: Inappropriate % 134.15/19.15 % (3725556)Time elapsed: 0.001 s % 134.15/19.15 % (3725556)Peak memory usage: 10 MB % 134.15/19.15 % (3725556)Instructions burned: 1 (million) % 134.15/19.15 % (3725556)------------------------------ % 134.15/19.15 % (3725556)------------------------------ % 134.15/19.15 % (3725558)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1908987353:fmbsr=2:i=46332_2966 on theBenchmark for (2966ds/46332Mi) % 134.15/19.15 % (3725558)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 134.15/19.15 % (3725558)Terminated due to inappropriate strategy. % 134.15/19.15 % (3725558)------------------------------ % 134.15/19.15 % (3725558)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 134.15/19.15 % (3725558)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 134.15/19.15 % (3725558)CaDiCaL version: 2.1.3 % 134.15/19.15 % (3725558)Termination reason: Inappropriate % 134.15/19.15 % (3725558)Time elapsed: 0.001 s % 134.15/19.15 % (3725558)Peak memory usage: 10 MB % 134.15/19.15 % (3725558)Instructions burned: 1 (million) % 134.15/19.15 % (3725558)------------------------------ % 134.15/19.15 % (3725558)------------------------------ % 134.15/19.15 % (3725560)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=103481047:i=14071_2966 on theBenchmark for (2966ds/14071Mi) % 134.15/19.15 % (3725560)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 134.15/19.15 % (3725560)Terminated due to inappropriate strategy. % 134.15/19.15 % (3725560)------------------------------ % 134.15/19.15 % (3725560)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 134.15/19.15 % (3725560)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 134.15/19.15 % (3725560)CaDiCaL version: 2.1.3 % 134.15/19.15 % (3725560)Termination reason: Inappropriate % 134.15/19.15 % (3725560)Time elapsed: 0.001 s % 134.15/19.15 % (3725560)Peak memory usage: 10 MB % 134.15/19.15 % (3725560)Instructions burned: 1 (million) % 134.15/19.15 % (3725560)------------------------------ % 134.15/19.15 % (3725560)------------------------------ % 134.15/19.15 % (3725562)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3327882260:i=22565:add=on:rawr=on_2966 on theBenchmark for (2966ds/22565Mi) % 134.15/19.15 % (3725538)Instruction limit reached! % 134.15/19.15 % (3725538)------------------------------ % 134.15/19.15 % (3725538)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 134.15/19.15 % (3725538)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 134.15/19.15 % (3725538)CaDiCaL version: 2.1.3 % 134.15/19.15 % (3725538)Termination reason: Instruction limit % 134.15/19.15 % (3725538)Termination phase: Saturation % 134.15/19.15 % (3725538)Time elapsed: 3.220 s % 134.15/19.15 % (3725538)Peak memory usage: 34 MB % 134.15/19.15 % (3725538)Instructions burned: 5116 (million) % 134.15/19.15 % (3725564)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=1548952173:i=8173:av=off_2960 on theBenchmark for (2960ds/8173Mi) % 134.15/19.15 % (3725550)Instruction limit reached! % 134.64/19.26 % (3725550)------------------------------ % 134.64/19.26 % (3725550)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 134.64/19.26 % (3725550)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 134.64/19.26 % (3725550)CaDiCaL version: 2.1.3 % 134.64/19.26 % (3725550)Termination reason: Instruction limit % 134.64/19.26 % (3725550)Termination phase: Saturation % 134.64/19.26 % (3725550)Time elapsed: 2.449 s % 134.64/19.26 % (3725550)Peak memory usage: 44 MB % 134.64/19.26 % (3725550)Instructions burned: 4593 (million) % 134.64/19.26 % (3725566)dis+10_16:1_sil=16000:random_seed=2317254879:i=9155:fsr=off_2948 on theBenchmark for (2948ds/9155Mi) % 134.64/19.26 % (3725554)Instruction limit reached! % 134.64/19.26 % (3725554)------------------------------ % 134.64/19.26 % (3725554)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 134.64/19.26 % (3725554)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 134.64/19.26 % (3725554)CaDiCaL version: 2.1.3 % 134.64/19.26 % (3725554)Termination reason: Instruction limit % 134.64/19.26 % (3725554)Termination phase: Saturation % 134.64/19.26 % (3725554)Time elapsed: 2.791 s % 134.64/19.26 % (3725554)Peak memory usage: 51 MB % 134.64/19.26 % (3725554)Instructions burned: 5211 (million) % 134.64/19.26 % (3725568)ott-3_8_sil=64000:random_seed=3216185422:i=20139:bs=on_2939 on theBenchmark for (2939ds/20139Mi) % 134.64/19.26 % (3725564)Instruction limit reached! % 134.64/19.26 % (3725564)------------------------------ % 134.64/19.26 % (3725564)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 134.64/19.26 % (3725564)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 134.64/19.26 % (3725564)CaDiCaL version: 2.1.3 % 134.64/19.26 % (3725564)Termination reason: Instruction limit % 134.64/19.26 % (3725564)Termination phase: Saturation % 134.64/19.26 % (3725564)Time elapsed: 5.123 s % 134.64/19.26 % (3725564)Peak memory usage: 60 MB % 134.64/19.26 % (3725564)Instructions burned: 8175 (million) % 134.64/19.26 % (3725722)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=701573983:fmbsr=2:i=32576_2908 on theBenchmark for (2908ds/32576Mi) % 134.64/19.26 % (3725722)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 134.64/19.26 % (3725722)Terminated due to inappropriate strategy. % 134.64/19.26 % (3725722)------------------------------ % 134.64/19.26 % (3725722)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 134.64/19.26 % (3725722)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 134.64/19.26 % (3725722)CaDiCaL version: 2.1.3 % 134.64/19.26 % (3725722)Termination reason: Inappropriate % 134.64/19.26 % (3725722)Time elapsed: 0.001 s % 134.64/19.26 % (3725722)Peak memory usage: 10 MB % 134.64/19.26 % (3725722)Instructions burned: 1 (million) % 134.64/19.26 % (3725722)------------------------------ % 134.64/19.26 % (3725722)------------------------------ % 134.64/19.26 % (3725724)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=4102271267:i=11404_2908 on theBenchmark for (2908ds/11404Mi) % 134.64/19.26 % (3725566)Instruction limit reached! % 134.64/19.26 % (3725566)------------------------------ % 134.64/19.26 % (3725566)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 134.64/19.26 % (3725566)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 134.64/19.26 % (3725566)CaDiCaL version: 2.1.3 % 134.64/19.26 % (3725566)Termination reason: Instruction limit % 134.64/19.26 % (3725566)Termination phase: Saturation % 134.64/19.26 % (3725566)Time elapsed: 4.686 s % 134.64/19.26 % (3725566)Peak memory usage: 53 MB % 134.64/19.26 % (3725566)Instructions burned: 9156 (million) % 134.64/19.26 % (3725726)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=2079889650:i=14134_2901 on theBenchmark for (2901ds/14134Mi) % 134.64/19.26 % (3725562)Instruction limit reached! % 134.64/19.26 % (3725562)------------------------------ % 134.64/19.26 % (3725562)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 134.64/19.26 % (3725562)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 134.64/19.26 % (3725562)CaDiCaL version: 2.1.3 % 134.64/19.26 % (3725562)Termination reason: Instruction limit % 134.64/19.26 % (3725562)Termination phase: Saturation % 134.64/19.26 % (3725562)Time elapsed: 9.441 s % 134.64/19.26 % (3725562)Peak memory usage: 52 MB % 134.64/19.26 % (3725562)Instructions burned: 22565 (million) % 134.64/19.26 % (3725728)dis+33_16_sil=32000:sac=on:random_seed=1154948947:i=15851:nm=0_2871 on theBenchmark for (2871ds/15851Mi) % 134.64/19.26 % (3725552)Instruction limit reached! % 134.64/19.26 % (3725552)------------------------------ % 134.64/19.26 % (3725552)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 176.08/25.11 % (3725552)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.08/25.11 % (3725552)CaDiCaL version: 2.1.3 % 176.08/25.11 % (3725552)Termination reason: Instruction limit % 176.08/25.11 % (3725552)Termination phase: Saturation % 176.08/25.11 % (3725552)Time elapsed: 11.974 s % 176.08/25.11 % (3725552)Peak memory usage: 118 MB % 176.08/25.11 % (3725552)Instructions burned: 29341 (million) % 176.08/25.11 % (3725776)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=2016757586:avsq=on:i=17627:add=on:amm=off_2852 on theBenchmark for (2852ds/17627Mi) % 176.08/25.11 % (3725724)Instruction limit reached! % 176.08/25.11 % (3725724)------------------------------ % 176.08/25.11 % (3725724)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 176.08/25.11 % (3725724)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.08/25.11 % (3725724)CaDiCaL version: 2.1.3 % 176.08/25.11 % (3725724)Termination reason: Instruction limit % 176.08/25.11 % (3725724)Termination phase: Saturation % 176.08/25.11 % (3725724)Time elapsed: 6.990 s % 176.08/25.11 % (3725724)Peak memory usage: 62 MB % 176.08/25.11 % (3725724)Instructions burned: 11405 (million) % 176.08/25.11 % (3725778)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=1727021452:s2a=on:i=53295_2838 on theBenchmark for (2838ds/53295Mi) % 176.08/25.11 % (3725726)Instruction limit reached! % 176.08/25.11 % (3725726)------------------------------ % 176.08/25.11 % (3725726)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 176.08/25.11 % (3725726)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.08/25.11 % (3725726)CaDiCaL version: 2.1.3 % 176.08/25.11 % (3725726)Termination reason: Instruction limit % 176.08/25.11 % (3725726)Termination phase: Saturation % 176.08/25.11 % (3725726)Time elapsed: 8.617 s % 176.08/25.11 % (3725726)Peak memory usage: 77 MB % 176.08/25.11 % (3725726)Instructions burned: 14135 (million) % 176.08/25.11 % (3725780)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=4252777281:i=26857:ins=20_2815 on theBenchmark for (2815ds/26857Mi) % 176.08/25.11 % (3725780)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 176.08/25.11 % (3725780)Terminated due to inappropriate strategy. % 176.08/25.11 % (3725780)------------------------------ % 176.08/25.11 % (3725780)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 176.08/25.11 % (3725780)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.08/25.11 % (3725780)CaDiCaL version: 2.1.3 % 176.08/25.11 % (3725780)Termination reason: Inappropriate % 176.08/25.11 % (3725780)Time elapsed: 0.001 s % 176.08/25.11 % (3725780)Peak memory usage: 10 MB % 176.08/25.11 % (3725780)Instructions burned: 1 (million) % 176.08/25.11 % (3725780)------------------------------ % 176.08/25.11 % (3725780)------------------------------ % 176.08/25.11 % (3725782)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=2225429549:i=28120:bs=on:fsr=off_2814 on theBenchmark for (2814ds/28120Mi) % 176.08/25.11 % (3725568)Instruction limit reached! % 176.08/25.11 % (3725568)------------------------------ % 176.08/25.11 % (3725568)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 176.08/25.11 % (3725568)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.08/25.11 % (3725568)CaDiCaL version: 2.1.3 % 176.08/25.11 % (3725568)Termination reason: Instruction limit % 176.08/25.11 % (3725568)Termination phase: Saturation % 176.08/25.11 % (3725568)Time elapsed: 12.812 s % 176.08/25.11 % (3725568)Peak memory usage: 70 MB % 176.08/25.11 % (3725568)Instructions burned: 20141 (million) % 176.08/25.11 % (3725784)fmb+10_1_sil=256000:fmbss=7:random_seed=1294921948:fmbsr=1.6:i=182295_2811 on theBenchmark for (2811ds/182295Mi) % 176.08/25.11 % (3725784)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 176.08/25.11 % (3725784)Terminated due to inappropriate strategy. % 176.08/25.11 % (3725784)------------------------------ % 176.08/25.11 % (3725784)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 176.08/25.11 % (3725784)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.08/25.11 % (3725784)CaDiCaL version: 2.1.3 % 176.08/25.11 % (3725784)Termination reason: Inappropriate % 176.08/25.11 % (3725784)Time elapsed: 0.001 s % 176.08/25.11 % (3725784)Peak memory usage: 10 MB % 176.08/25.11 % (3725784)Instructions burned: 1 (million) % 176.08/25.11 % (3725784)------------------------------ % 176.08/25.11 % (3725784)------------------------------ % 176.08/25.11 % (3725786)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=680604004:i=44625:gsp=on_2810 on theBenchmark for (2810ds/44625Mi) % 197.42/28.06 % (3725786)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 197.42/28.06 % (3725786)Terminated due to inappropriate strategy. % 197.42/28.06 % (3725786)------------------------------ % 197.42/28.06 % (3725786)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 197.42/28.06 % (3725786)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 197.42/28.06 % (3725786)CaDiCaL version: 2.1.3 % 197.42/28.06 % (3725786)Termination reason: Inappropriate % 197.42/28.06 % (3725786)Time elapsed: 0.001 s % 197.42/28.06 % (3725786)Peak memory usage: 11 MB % 197.42/28.06 % (3725786)Instructions burned: 1 (million) % 197.42/28.06 % (3725786)------------------------------ % 197.42/28.06 % (3725786)------------------------------ % 197.42/28.06 % (3725788)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=3787410005:i=160505_2810 on theBenchmark for (2810ds/160505Mi) % 197.42/28.06 % (3725788)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 197.42/28.06 % (3725788)Terminated due to inappropriate strategy. % 197.42/28.06 % (3725788)------------------------------ % 197.42/28.06 % (3725788)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 197.42/28.06 % (3725788)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 197.42/28.06 % (3725788)CaDiCaL version: 2.1.3 % 197.42/28.06 % (3725788)Termination reason: Inappropriate % 197.42/28.06 % (3725788)Time elapsed: 0.001 s % 197.42/28.06 % (3725788)Peak memory usage: 10 MB % 197.42/28.06 % (3725788)Instructions burned: 1 (million) % 197.42/28.06 % (3725788)------------------------------ % 197.42/28.06 % (3725788)------------------------------ % 197.42/28.06 % (3725790)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=3122270440:fmbsr=1.3:i=225729_2810 on theBenchmark for (2810ds/225729Mi) % 197.42/28.06 % (3725790)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 197.42/28.06 % (3725790)Terminated due to inappropriate strategy. % 197.42/28.06 % (3725790)------------------------------ % 197.42/28.06 % (3725790)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 197.42/28.06 % (3725790)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 197.42/28.06 % (3725790)CaDiCaL version: 2.1.3 % 197.42/28.06 % (3725790)Termination reason: Inappropriate % 197.42/28.06 % (3725790)Time elapsed: 0.001 s % 197.42/28.06 % (3725790)Peak memory usage: 10 MB % 197.42/28.06 % (3725790)Instructions burned: 1 (million) % 197.42/28.06 % (3725790)------------------------------ % 197.42/28.06 % (3725790)------------------------------ % 197.42/28.06 % (3725792)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=2155088380:fmbsr=2:i=185024:ins=7_2810 on theBenchmark for (2810ds/185024Mi) % 197.42/28.06 % (3725792)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 197.42/28.06 % (3725792)Terminated due to inappropriate strategy. % 197.42/28.06 % (3725792)------------------------------ % 197.42/28.06 % (3725792)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 197.42/28.06 % (3725792)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 197.42/28.06 % (3725792)CaDiCaL version: 2.1.3 % 197.42/28.06 % (3725792)Termination reason: Inappropriate % 197.42/28.06 % (3725792)Time elapsed: 0.001 s % 197.42/28.06 % (3725792)Peak memory usage: 11 MB % 197.42/28.06 % (3725792)Instructions burned: 1 (million) % 197.42/28.06 % (3725792)------------------------------ % 197.42/28.06 % (3725792)------------------------------ % 197.42/28.06 % (3725794)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=498497034:rtra=on_2810 on theBenchmark for (2810ds/0Mi) % 197.42/28.06 % (3725794)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 197.42/28.06 % (3725794)Terminated due to inappropriate strategy. % 197.42/28.06 % (3725794)------------------------------ % 197.42/28.06 % (3725794)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 197.42/28.06 % (3725794)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 197.42/28.06 % (3725794)CaDiCaL version: 2.1.3 % 197.42/28.06 % (3725794)Termination reason: Inappropriate % 197.42/28.06 % (3725794)Time elapsed: 0.001 s % 197.42/28.06 % (3725794)Peak memory usage: 10 MB % 197.42/28.06 % (3725794)Instructions burned: 1 (million) % 197.42/28.06 % (3725794)------------------------------ % 197.42/28.06 % (3725794)------------------------------ % 197.42/28.06 % (3725796)% WARNING: option uhcvi not known. % 197.42/28.06 % (3725796)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=809321591:i=271062:add=off:rtra=on:rawr=on_2809 on theBenchmark for (2809ds/271062Mi) % 233.08/33.34 % (3725728)Instruction limit reached! % 233.08/33.34 % (3725728)------------------------------ % 233.08/33.34 % (3725728)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 233.08/33.34 % (3725728)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 233.08/33.34 % (3725728)CaDiCaL version: 2.1.3 % 233.08/33.34 % (3725728)Termination reason: Instruction limit % 233.08/33.34 % (3725728)Termination phase: Saturation % 233.08/33.34 % (3725728)Time elapsed: 7.796 s % 233.08/33.34 % (3725728)Peak memory usage: 124 MB % 233.08/33.34 % (3725728)Instructions burned: 15851 (million) % 233.08/33.34 % (3725798)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=692851241:i=176048:add=on:rtra=on:rawr=on_2793 on theBenchmark for (2793ds/176048Mi) % 233.08/33.34 % (3725776)Instruction limit reached! % 233.08/33.34 % (3725776)------------------------------ % 233.08/33.34 % (3725776)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 233.08/33.34 % (3725776)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 233.08/33.34 % (3725776)CaDiCaL version: 2.1.3 % 233.08/33.34 % (3725776)Termination reason: Instruction limit % 233.08/33.34 % (3725776)Termination phase: Saturation % 233.08/33.34 % (3725776)Time elapsed: 9.141 s % 233.08/33.34 % (3725776)Peak memory usage: 108 MB % 233.08/33.34 % (3725776)Instructions burned: 17628 (million) % 233.08/33.34 % (3725997)dis+10_1_sil=32000:si=on:sp=arity:random_seed=3494320313:i=206:fgj=on:rtra=on_2760 on theBenchmark for (2760ds/206Mi) % 233.08/33.34 % (3725997)Instruction limit reached! % 233.08/33.34 % (3725997)------------------------------ % 233.08/33.34 % (3725997)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 233.08/33.34 % (3725997)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 233.08/33.34 % (3725997)CaDiCaL version: 2.1.3 % 233.08/33.34 % (3725997)Termination reason: Instruction limit % 233.08/33.34 % (3725997)Termination phase: Saturation % 233.08/33.34 % (3725997)Time elapsed: 0.158 s % 233.08/33.34 % (3725997)Peak memory usage: 13 MB % 233.08/33.34 % (3725997)Instructions burned: 208 (million) % 233.08/33.34 % (3726003)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=2363701383:i=232:rtra=on_2758 on theBenchmark for (2758ds/232Mi) % 233.08/33.34 % (3726003)Instruction limit reached! % 233.08/33.34 % (3726003)------------------------------ % 233.08/33.34 % (3726003)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 233.08/33.34 % (3726003)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 233.08/33.34 % (3726003)CaDiCaL version: 2.1.3 % 233.08/33.34 % (3726003)Termination reason: Instruction limit % 233.08/33.34 % (3726003)Termination phase: Saturation % 233.08/33.34 % (3726003)Time elapsed: 0.144 s % 233.08/33.34 % (3726003)Peak memory usage: 13 MB % 233.08/33.34 % (3726003)Instructions burned: 232 (million) % 233.08/33.34 % (3726005)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=3899243113:i=262:rtra=on_2757 on theBenchmark for (2757ds/262Mi) % 233.08/33.34 % (3726005)Instruction limit reached! % 233.08/33.34 % (3726005)------------------------------ % 233.08/33.34 % (3726005)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 233.08/33.34 % (3726005)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 233.08/33.34 % (3726005)CaDiCaL version: 2.1.3 % 233.08/33.34 % (3726005)Termination reason: Instruction limit % 233.08/33.34 % (3726005)Termination phase: Saturation % 233.08/33.34 % (3726005)Time elapsed: 0.164 s % 233.08/33.34 % (3726005)Peak memory usage: 14 MB % 233.08/33.34 % (3726005)Instructions burned: 262 (million) % 233.08/33.34 % (3726015)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=3176132950:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2755 on theBenchmark for (2755ds/318Mi) % 233.08/33.34 % (3726015)Instruction limit reached! % 233.08/33.34 % (3726015)------------------------------ % 233.08/33.34 % (3726015)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 233.08/33.34 % (3726015)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 233.08/33.34 % (3726015)CaDiCaL version: 2.1.3 % 233.08/33.34 % (3726015)Termination reason: Instruction limit % 233.08/33.34 % (3726015)Termination phase: Saturation % 233.08/33.34 % (3726015)Time elapsed: 0.324 s % 233.08/33.34 % (3726015)Peak memory usage: 15 MB % 233.08/33.34 % (3726015)Instructions burned: 318 (million) % 233.08/33.34 % (3726030)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=619937672:i=1428:nm=2:rtra=on_2751 on theBenchmark for (2751ds/1428Mi) % 275.65/39.07 % (3726030)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 275.65/39.07 % (3726030)Terminated due to inappropriate strategy. % 275.65/39.07 % (3726030)------------------------------ % 275.65/39.07 % (3726030)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 275.65/39.07 % (3726030)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 275.65/39.07 % (3726030)CaDiCaL version: 2.1.3 % 275.65/39.07 % (3726030)Termination reason: Inappropriate % 275.65/39.07 % (3726030)Time elapsed: 0.002 s % 275.65/39.07 % (3726030)Peak memory usage: 10 MB % 275.65/39.07 % (3726030)Instructions burned: 1 (million) % 275.65/39.07 % (3726030)------------------------------ % 275.65/39.07 % (3726030)------------------------------ % 275.65/39.07 % (3726035)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=475422689:i=262:bd=preordered:rtra=on:fsd=on_2751 on theBenchmark for (2751ds/262Mi) % 275.65/39.07 % (3726035)Instruction limit reached! % 275.65/39.07 % (3726035)------------------------------ % 275.65/39.07 % (3726035)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 275.65/39.07 % (3726035)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 275.65/39.07 % (3726035)CaDiCaL version: 2.1.3 % 275.65/39.07 % (3726035)Termination reason: Instruction limit % 275.65/39.07 % (3726035)Termination phase: Saturation % 275.65/39.07 % (3726035)Time elapsed: 0.251 s % 275.65/39.07 % (3726035)Peak memory usage: 14 MB % 275.65/39.07 % (3726035)Instructions burned: 262 (million) % 275.65/39.07 % (3726055)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=3921477193:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2748 on theBenchmark for (2748ds/1368Mi) % 275.65/39.07 % (3726055)Instruction limit reached! % 275.65/39.07 % (3726055)------------------------------ % 275.65/39.07 % (3726055)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 275.65/39.07 % (3726055)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 275.65/39.07 % (3726055)CaDiCaL version: 2.1.3 % 275.65/39.07 % (3726055)Termination reason: Instruction limit % 275.65/39.07 % (3726055)Termination phase: Saturation % 275.65/39.07 % (3726055)Time elapsed: 1.256 s % 275.65/39.07 % (3726055)Peak memory usage: 22 MB % 275.65/39.07 % (3726055)Instructions burned: 1369 (million) % 275.65/39.07 % (3726109)ott-21_1_sil=16000:si=on:fs=off:random_seed=1709620382:i=360:av=off:fsr=off:rtra=on_2735 on theBenchmark for (2735ds/360Mi) % 275.65/39.07 % (3726109)Instruction limit reached! % 275.65/39.07 % (3726109)------------------------------ % 275.65/39.07 % (3726109)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 275.65/39.07 % (3726109)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 275.65/39.07 % (3726109)CaDiCaL version: 2.1.3 % 275.65/39.07 % (3726109)Termination reason: Instruction limit % 275.65/39.07 % (3726109)Termination phase: Saturation % 275.65/39.07 % (3726109)Time elapsed: 0.306 s % 275.65/39.07 % (3726109)Peak memory usage: 13 MB % 275.65/39.07 % (3726109)Instructions burned: 360 (million) % 275.65/39.07 % (3726122)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1199407787:i=954:bd=all:rtra=on_2731 on theBenchmark for (2731ds/954Mi) % 275.65/39.07 % (3726122)Instruction limit reached! % 275.65/39.07 % (3726122)------------------------------ % 275.65/39.07 % (3726122)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 275.65/39.07 % (3726122)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 275.65/39.07 % (3726122)CaDiCaL version: 2.1.3 % 275.65/39.07 % (3726122)Termination reason: Instruction limit % 275.65/39.07 % (3726122)Termination phase: Saturation % 275.65/39.07 % (3726122)Time elapsed: 0.918 s % 275.65/39.07 % (3726122)Peak memory usage: 16 MB % 275.65/39.07 % (3726122)Instructions burned: 954 (million) % 275.65/39.07 % (3726148)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=2523471582:fmbsr=1.3:i=1730:ins=25:rtra=on_2722 on theBenchmark for (2722ds/1730Mi) % 275.65/39.07 % (3726148)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 275.65/39.07 % (3726148)Terminated due to inappropriate strategy. % 275.65/39.07 % (3726148)------------------------------ % 275.65/39.07 % (3726148)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 275.65/39.07 % (3726148)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 275.65/39.07 % (3726148)CaDiCaL version: 2.1.3 % 275.65/39.07 % (3726148)Termination reason: Inappropriate % 275.65/39.07 % (37Terminated % 300.27/42.54 % Vampire exiting %------------------------------------------------------------------------------