%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW602_2 : TPTP v9.3.1. Released v6.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n010.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:40:30 PM UTC 2026 % Result : Timeout 300.06s 42.54s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWW602_2 : TPTP v9.3.1. Released v6.1.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.09/0.18 % Computer : n010.cluster.edu % 0.09/0.18 % Model : x86_64 x86_64 % 0.09/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.18 % Memory : 8046.5625MB % 0.09/0.18 % OS : Linux 6.8.0-71-generic % 0.09/0.18 % CPULimit : 300 % 0.09/0.18 % WCLimit : 300 % 0.09/0.18 % DateTime : Mon Sep 28 14:21:32 UTC 2026 % 0.09/0.18 % CPUTime : % 0.09/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.09/0.22 Running first-order model finding % 0.09/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 % 2.92/0.67 % (1952396)Will run a generic schedule for satisfiability detection. % 2.92/0.67 % (1952405)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1770307159:i=116_2999 on theBenchmark for (2999ds/116Mi) % 2.92/0.67 % (1952402)% WARNING: option uhcvi not known. % 2.92/0.67 % (1952401)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2364514585_2999 on theBenchmark for (2999ds/0Mi) % 2.92/0.67 % (1952406)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=107844356:i=131_2999 on theBenchmark for (2999ds/131Mi) % 2.92/0.67 % (1952403)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2327506559:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 2.92/0.67 % (1952404)dis+10_1_sil=32000:sp=arity:random_seed=465921400:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 2.92/0.67 % (1952402)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=421043225:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 2.92/0.67 % (1952407)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2559030443:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 2.92/0.67 % (1952401)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 2.92/0.67 % (1952401)Terminated due to inappropriate strategy. % 2.92/0.67 % (1952401)------------------------------ % 2.92/0.67 % (1952401)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.92/0.67 % (1952401)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.92/0.67 % (1952401)CaDiCaL version: 2.1.3 % 2.92/0.67 % (1952401)Termination reason: Inappropriate % 2.92/0.67 % (1952401)Time elapsed: 0.005 s % 2.92/0.67 % (1952401)Peak memory usage: 11 MB % 2.92/0.67 % (1952401)Instructions burned: 8 (million) % 2.92/0.67 % (1952401)------------------------------ % 2.92/0.67 % (1952401)------------------------------ % 2.92/0.67 % (1952415)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2928331152:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 2.92/0.67 % (1952405)Instruction limit reached! % 2.92/0.67 % (1952405)------------------------------ % 2.92/0.67 % (1952405)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.92/0.67 % (1952405)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.92/0.67 % (1952405)CaDiCaL version: 2.1.3 % 2.92/0.67 % (1952405)Termination reason: Instruction limit % 2.92/0.67 % (1952405)Termination phase: Saturation % 2.92/0.67 % (1952405)Time elapsed: 0.037 s % 2.92/0.67 % (1952405)Peak memory usage: 13 MB % 2.92/0.67 % (1952405)Instructions burned: 116 (million) % 2.92/0.67 % (1952415)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 2.92/0.67 % (1952415)Terminated due to inappropriate strategy. % 2.92/0.67 % (1952415)------------------------------ % 2.92/0.67 % (1952415)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.92/0.67 % (1952415)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.92/0.67 % (1952415)CaDiCaL version: 2.1.3 % 2.92/0.67 % (1952415)Termination reason: Inappropriate % 2.92/0.67 % (1952415)Time elapsed: 0.004 s % 2.92/0.67 % (1952415)Peak memory usage: 11 MB % 2.92/0.67 % (1952415)Instructions burned: 8 (million) % 2.92/0.67 % (1952415)------------------------------ % 2.92/0.67 % (1952415)------------------------------ % 2.92/0.67 % (1952417)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1605683912:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 2.92/0.67 % (1952418)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=3358273604:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 2.92/0.67 % (1952404)Instruction limit reached! % 2.92/0.67 % (1952404)------------------------------ % 2.92/0.67 % (1952404)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.92/0.67 % (1952404)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.92/0.67 % (1952404)CaDiCaL version: 2.1.3 % 2.92/0.67 % (1952404)Termination reason: Instruction limit % 2.92/0.67 % (1952404)Termination phase: Saturation % 2.92/0.67 % (1952404)Time elapsed: 0.065 s % 2.92/0.67 % (1952404)Peak memory usage: 13 MB % 2.92/0.67 % (1952404)Instructions burned: 103 (million) % 2.92/0.67 % (1952406)Instruction limit reached! % 2.92/0.67 % (1952406)------------------------------ % 2.92/0.67 % (1952406)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.43/1.13 % (1952406)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.43/1.13 % (1952406)CaDiCaL version: 2.1.3 % 6.43/1.13 % (1952406)Termination reason: Instruction limit % 6.43/1.13 % (1952406)Termination phase: Saturation % 6.43/1.13 % (1952406)Time elapsed: 0.080 s % 6.43/1.13 % (1952406)Peak memory usage: 13 MB % 6.43/1.13 % (1952406)Instructions burned: 131 (million) % 6.43/1.13 % (1952421)ott-21_1_sil=16000:fs=off:random_seed=938241953:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi) % 6.43/1.13 % (1952417)Instruction limit reached! % 6.43/1.13 % (1952417)------------------------------ % 6.43/1.13 % (1952417)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.43/1.13 % (1952417)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.43/1.13 % (1952417)CaDiCaL version: 2.1.3 % 6.43/1.13 % (1952417)Termination reason: Instruction limit % 6.43/1.13 % (1952417)Termination phase: Saturation % 6.43/1.13 % (1952417)Time elapsed: 0.047 s % 6.43/1.13 % (1952417)Peak memory usage: 13 MB % 6.43/1.13 % (1952417)Instructions burned: 133 (million) % 6.43/1.13 % (1952407)Instruction limit reached! % 6.43/1.13 % (1952407)------------------------------ % 6.43/1.13 % (1952407)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.43/1.13 % (1952407)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.43/1.13 % (1952407)CaDiCaL version: 2.1.3 % 6.43/1.13 % (1952407)Termination reason: Instruction limit % 6.43/1.13 % (1952407)Termination phase: Saturation % 6.43/1.13 % (1952407)Time elapsed: 0.096 s % 6.43/1.13 % (1952407)Peak memory usage: 13 MB % 6.43/1.13 % (1952407)Instructions burned: 159 (million) % 6.43/1.13 % (1952424)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3778420337:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 6.43/1.13 % (1952422)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2010712141:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 6.43/1.13 % (1952424)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 6.43/1.13 % (1952424)Terminated due to inappropriate strategy. % 6.43/1.13 % (1952424)------------------------------ % 6.43/1.13 % (1952424)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.43/1.13 % (1952424)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.43/1.13 % (1952424)CaDiCaL version: 2.1.3 % 6.43/1.13 % (1952424)Termination reason: Inappropriate % 6.43/1.13 % (1952424)Time elapsed: 0.002 s % 6.43/1.13 % (1952424)Peak memory usage: 11 MB % 6.43/1.13 % (1952424)Instructions burned: 7 (million) % 6.43/1.13 % (1952424)------------------------------ % 6.43/1.13 % (1952424)------------------------------ % 6.43/1.13 % (1952428)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=4032371065:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 6.43/1.13 % (1952428)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 6.43/1.13 % (1952428)Terminated due to inappropriate strategy. % 6.43/1.13 % (1952428)------------------------------ % 6.43/1.13 % (1952428)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.43/1.13 % (1952428)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.43/1.13 % (1952428)CaDiCaL version: 2.1.3 % 6.43/1.13 % (1952428)Termination reason: Inappropriate % 6.43/1.13 % (1952428)Time elapsed: 0.002 s % 6.43/1.13 % (1952428)Peak memory usage: 11 MB % 6.43/1.13 % (1952428)Instructions burned: 7 (million) % 6.43/1.13 % (1952428)------------------------------ % 6.43/1.13 % (1952428)------------------------------ % 6.43/1.13 % (1952425)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3708749993:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 6.43/1.13 % (1952430)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=868182777: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) % 6.43/1.13 % (1952421)Instruction limit reached! % 6.43/1.13 % (1952421)------------------------------ % 6.43/1.13 % (1952421)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.43/1.13 % (1952421)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.43/1.13 % (1952421)CaDiCaL version: 2.1.3 % 6.43/1.13 % (1952421)Termination reason: Instruction limit % 6.43/1.13 % (1952421)Termination phase: Saturation % 20.65/3.17 % (1952421)Time elapsed: 0.099 s % 20.65/3.17 % (1952421)Peak memory usage: 13 MB % 20.65/3.17 % (1952421)Instructions burned: 181 (million) % 20.65/3.17 % (1952433)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2959469845:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 20.65/3.17 % (1952430)Instruction limit reached! % 20.65/3.17 % (1952430)------------------------------ % 20.65/3.17 % (1952430)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.65/3.17 % (1952430)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.65/3.17 % (1952430)CaDiCaL version: 2.1.3 % 20.65/3.17 % (1952430)Termination reason: Instruction limit % 20.65/3.17 % (1952430)Termination phase: Saturation % 20.65/3.17 % (1952430)Time elapsed: 0.230 s % 20.65/3.17 % (1952430)Peak memory usage: 18 MB % 20.65/3.17 % (1952430)Instructions burned: 692 (million) % 20.65/3.17 % (1952435)fmb+10_1_sil=64000:random_seed=3652472390:i=22061:nm=2:gsp=on_2996 on theBenchmark for (2996ds/22061Mi) % 20.65/3.17 % (1952435)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 20.65/3.17 % (1952435)Terminated due to inappropriate strategy. % 20.65/3.17 % (1952435)------------------------------ % 20.65/3.17 % (1952435)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.65/3.17 % (1952435)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.65/3.17 % (1952435)CaDiCaL version: 2.1.3 % 20.65/3.17 % (1952435)Termination reason: Inappropriate % 20.65/3.17 % (1952435)Time elapsed: 0.002 s % 20.65/3.17 % (1952435)Peak memory usage: 11 MB % 20.65/3.17 % (1952435)Instructions burned: 8 (million) % 20.65/3.17 % (1952435)------------------------------ % 20.65/3.17 % (1952435)------------------------------ % 20.65/3.17 % (1952437)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2050839373:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi) % 20.65/3.17 % (1952437)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 20.65/3.17 % (1952437)Terminated due to inappropriate strategy. % 20.65/3.17 % (1952437)------------------------------ % 20.65/3.17 % (1952437)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.65/3.17 % (1952437)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.65/3.17 % (1952437)CaDiCaL version: 2.1.3 % 20.65/3.17 % (1952437)Termination reason: Inappropriate % 20.65/3.17 % (1952437)Time elapsed: 0.002 s % 20.65/3.17 % (1952437)Peak memory usage: 11 MB % 20.65/3.17 % (1952437)Instructions burned: 7 (million) % 20.65/3.17 % (1952437)------------------------------ % 20.65/3.17 % (1952437)------------------------------ % 20.65/3.17 % (1952439)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3611784433:fmbsr=1.7:i=920_2995 on theBenchmark for (2995ds/920Mi) % 20.65/3.17 % (1952439)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 20.65/3.17 % (1952439)Terminated due to inappropriate strategy. % 20.65/3.17 % (1952439)------------------------------ % 20.65/3.17 % (1952439)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.65/3.17 % (1952439)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.65/3.17 % (1952439)CaDiCaL version: 2.1.3 % 20.65/3.17 % (1952439)Termination reason: Inappropriate % 20.65/3.17 % (1952439)Time elapsed: 0.002 s % 20.65/3.17 % (1952439)Peak memory usage: 11 MB % 20.65/3.17 % (1952439)Instructions burned: 7 (million) % 20.65/3.17 % (1952439)------------------------------ % 20.65/3.17 % (1952439)------------------------------ % 20.65/3.17 % (1952418)Instruction limit reached! % 20.65/3.17 % (1952418)------------------------------ % 20.65/3.17 % (1952418)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.65/3.17 % (1952418)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.65/3.17 % (1952418)CaDiCaL version: 2.1.3 % 20.65/3.17 % (1952418)Termination reason: Instruction limit % 20.65/3.17 % (1952418)Termination phase: Saturation % 20.65/3.17 % (1952418)Time elapsed: 0.353 s % 20.65/3.17 % (1952418)Peak memory usage: 16 MB % 20.65/3.17 % (1952418)Instructions burned: 685 (million) % 20.65/3.17 % (1952441)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=462904365:i=5131_2995 on theBenchmark for (2995ds/5131Mi) % 20.65/3.17 % (1952422)Instruction limit reached! % 20.65/3.17 % (1952422)------------------------------ % 20.65/3.17 % (1952422)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.65/3.17 % (1952422)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.21/4.28 % (1952422)CaDiCaL version: 2.1.3 % 28.21/4.28 % (1952422)Termination reason: Instruction limit % 28.21/4.28 % (1952422)Termination phase: Saturation % 28.21/4.28 % (1952422)Time elapsed: 0.311 s % 28.21/4.28 % (1952422)Peak memory usage: 14 MB % 28.21/4.28 % (1952422)Instructions burned: 478 (million) % 28.21/4.28 % (1952442)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2231016692:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi) % 28.21/4.28 % (1952444)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3686690042:i=6324_2995 on theBenchmark for (2995ds/6324Mi) % 28.21/4.28 % (1952444)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 28.21/4.28 % (1952444)Terminated due to inappropriate strategy. % 28.21/4.28 % (1952444)------------------------------ % 28.21/4.28 % (1952444)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.21/4.28 % (1952444)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.21/4.28 % (1952444)CaDiCaL version: 2.1.3 % 28.21/4.28 % (1952444)Termination reason: Inappropriate % 28.21/4.28 % (1952444)Time elapsed: 0.005 s % 28.21/4.28 % (1952444)Peak memory usage: 11 MB % 28.21/4.28 % (1952444)Instructions burned: 8 (million) % 28.21/4.28 % (1952444)------------------------------ % 28.21/4.28 % (1952444)------------------------------ % 28.21/4.28 % (1952447)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1863346709:fmbsr=2.30978:i=2174_2995 on theBenchmark for (2995ds/2174Mi) % 28.21/4.28 % (1952447)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 28.21/4.28 % (1952447)Terminated due to inappropriate strategy. % 28.21/4.28 % (1952447)------------------------------ % 28.21/4.28 % (1952447)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.21/4.28 % (1952447)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.21/4.28 % (1952447)CaDiCaL version: 2.1.3 % 28.21/4.28 % (1952447)Termination reason: Inappropriate % 28.21/4.28 % (1952447)Time elapsed: 0.004 s % 28.21/4.28 % (1952447)Peak memory usage: 11 MB % 28.21/4.28 % (1952447)Instructions burned: 7 (million) % 28.21/4.28 % (1952447)------------------------------ % 28.21/4.28 % (1952447)------------------------------ % 28.21/4.28 % (1952449)ott-2_1_sil=16000:newcnf=on:random_seed=2811658227:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2995 on theBenchmark for (2995ds/869Mi) % 28.21/4.28 % (1952433)Instruction limit reached! % 28.21/4.28 % (1952433)------------------------------ % 28.21/4.28 % (1952433)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.21/4.28 % (1952433)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.21/4.28 % (1952433)CaDiCaL version: 2.1.3 % 28.21/4.28 % (1952433)Termination reason: Instruction limit % 28.21/4.28 % (1952433)Termination phase: Saturation % 28.21/4.28 % (1952433)Time elapsed: 0.511 s % 28.21/4.28 % (1952433)Peak memory usage: 19 MB % 28.21/4.28 % (1952433)Instructions burned: 879 (million) % 28.21/4.28 % (1952451)ott+10_1_sil=32000:tgt=ground:random_seed=573951666:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi) % 28.21/4.28 % (1952425)Instruction limit reached! % 28.21/4.28 % (1952425)------------------------------ % 28.21/4.28 % (1952425)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.21/4.28 % (1952425)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.21/4.28 % (1952425)CaDiCaL version: 2.1.3 % 28.21/4.28 % (1952425)Termination reason: Instruction limit % 28.21/4.28 % (1952425)Termination phase: Saturation % 28.21/4.28 % (1952425)Time elapsed: 0.732 s % 28.21/4.28 % (1952425)Peak memory usage: 23 MB % 28.21/4.28 % (1952425)Instructions burned: 1179 (million) % 28.21/4.28 % (1952453)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3707438233:i=54282_2991 on theBenchmark for (2991ds/54282Mi) % 28.21/4.28 % (1952453)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 28.21/4.28 % (1952453)Terminated due to inappropriate strategy. % 28.21/4.28 % (1952453)------------------------------ % 28.21/4.28 % (1952453)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.21/4.28 % (1952453)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.21/4.28 % (1952453)CaDiCaL version: 2.1.3 % 28.21/4.28 % (1952453)Termination reason: Inappropriate % 28.21/4.28 % (1952453)Time elapsed: 0.005 s % 28.21/4.28 % (1952453)Peak memory usage: 11 MB % 28.21/4.28 % (1952453)Instructions burned: 8 (million) % 99.89/14.34 % (1952453)------------------------------ % 99.89/14.34 % (1952453)------------------------------ % 99.89/14.34 % (1952455)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=650157813:i=3512:aac=none_2990 on theBenchmark for (2990ds/3512Mi) % 99.89/14.34 % (1952449)Instruction limit reached! % 99.89/14.34 % (1952449)------------------------------ % 99.89/14.34 % (1952449)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 99.89/14.34 % (1952449)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.89/14.34 % (1952449)CaDiCaL version: 2.1.3 % 99.89/14.34 % (1952449)Termination reason: Instruction limit % 99.89/14.34 % (1952449)Termination phase: Saturation % 99.89/14.34 % (1952449)Time elapsed: 0.522 s % 99.89/14.34 % (1952449)Peak memory usage: 16 MB % 99.89/14.34 % (1952449)Instructions burned: 870 (million) % 99.89/14.34 % (1952457)dis+21_1_sil=32000:sas=cadical:random_seed=4227053345:i=3773:amm=off_2989 on theBenchmark for (2989ds/3773Mi) % 99.89/14.34 % (1952442)Instruction limit reached! % 99.89/14.34 % (1952442)------------------------------ % 99.89/14.34 % (1952442)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 99.89/14.34 % (1952442)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.89/14.34 % (1952442)CaDiCaL version: 2.1.3 % 99.89/14.34 % (1952442)Termination reason: Instruction limit % 99.89/14.34 % (1952442)Termination phase: Saturation % 99.89/14.34 % (1952442)Time elapsed: 0.755 s % 99.89/14.34 % (1952442)Peak memory usage: 24 MB % 99.89/14.34 % (1952442)Instructions burned: 1473 (million) % 99.89/14.34 % (1952459)ott+11_1_sil=16000:gs=on:random_seed=1561753457:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2987 on theBenchmark for (2987ds/2251Mi) % 99.89/14.34 % (1952441)Instruction limit reached! % 99.89/14.34 % (1952441)------------------------------ % 99.89/14.34 % (1952441)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 99.89/14.34 % (1952441)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.89/14.34 % (1952441)CaDiCaL version: 2.1.3 % 99.89/14.34 % (1952441)Termination reason: Instruction limit % 99.89/14.34 % (1952441)Termination phase: Saturation % 99.89/14.34 % (1952441)Time elapsed: 1.545 s % 99.89/14.34 % (1952441)Peak memory usage: 51 MB % 99.89/14.34 % (1952441)Instructions burned: 5134 (million) % 99.89/14.34 % (1952461)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2621764679:fmbsr=1.6:i=67534_2980 on theBenchmark for (2980ds/67534Mi) % 99.89/14.34 % (1952461)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 99.89/14.34 % (1952461)Terminated due to inappropriate strategy. % 99.89/14.34 % (1952461)------------------------------ % 99.89/14.34 % (1952461)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 99.89/14.34 % (1952461)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.89/14.34 % (1952461)CaDiCaL version: 2.1.3 % 99.89/14.34 % (1952461)Termination reason: Inappropriate % 99.89/14.34 % (1952461)Time elapsed: 0.002 s % 99.89/14.34 % (1952461)Peak memory usage: 11 MB % 99.89/14.34 % (1952461)Instructions burned: 8 (million) % 99.89/14.34 % (1952461)------------------------------ % 99.89/14.34 % (1952461)------------------------------ % 99.89/14.34 % (1952463)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1594169258:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2979 on theBenchmark for (2979ds/4591Mi) % 99.89/14.34 % (1952459)Instruction limit reached! % 99.89/14.34 % (1952459)------------------------------ % 99.89/14.34 % (1952459)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 99.89/14.34 % (1952459)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.89/14.34 % (1952459)CaDiCaL version: 2.1.3 % 99.89/14.34 % (1952459)Termination reason: Instruction limit % 99.89/14.34 % (1952459)Termination phase: Saturation % 99.89/14.34 % (1952459)Time elapsed: 1.464 s % 99.89/14.34 % (1952459)Peak memory usage: 30 MB % 99.89/14.34 % (1952459)Instructions burned: 2252 (million) % 99.89/14.34 % (1952465)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1287021451:i=29340_2973 on theBenchmark for (2973ds/29340Mi) % 99.89/14.34 % (1952455)Instruction limit reached! % 99.89/14.34 % (1952455)------------------------------ % 99.89/14.34 % (1952455)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 99.89/14.34 % (1952455)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.89/14.34 % (1952455)CaDiCaL version: 2.1.3 % 99.89/14.34 % (1952455)Termination reason: Instruction limit % 129.72/18.51 % (1952455)Termination phase: Saturation % 129.72/18.51 % (1952455)Time elapsed: 2.018 s % 129.72/18.51 % (1952455)Peak memory usage: 51 MB % 129.72/18.51 % (1952455)Instructions burned: 3513 (million) % 129.72/18.51 % (1952467)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3512095543:i=5211_2970 on theBenchmark for (2970ds/5211Mi) % 129.72/18.51 % (1952457)Instruction limit reached! % 129.72/18.51 % (1952457)------------------------------ % 129.72/18.51 % (1952457)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 129.72/18.51 % (1952457)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 129.72/18.51 % (1952457)CaDiCaL version: 2.1.3 % 129.72/18.51 % (1952457)Termination reason: Instruction limit % 129.72/18.51 % (1952457)Termination phase: Saturation % 129.72/18.51 % (1952457)Time elapsed: 2.172 s % 129.72/18.51 % (1952457)Peak memory usage: 33 MB % 129.72/18.51 % (1952457)Instructions burned: 3773 (million) % 129.72/18.51 % (1952469)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3681356362:i=5497:nm=2_2967 on theBenchmark for (2967ds/5497Mi) % 129.72/18.51 % (1952469)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 129.72/18.51 % (1952469)Terminated due to inappropriate strategy. % 129.72/18.51 % (1952469)------------------------------ % 129.72/18.51 % (1952469)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 129.72/18.51 % (1952469)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 129.72/18.51 % (1952469)CaDiCaL version: 2.1.3 % 129.72/18.51 % (1952469)Termination reason: Inappropriate % 129.72/18.51 % (1952469)Time elapsed: 0.005 s % 129.72/18.51 % (1952469)Peak memory usage: 11 MB % 129.72/18.51 % (1952469)Instructions burned: 8 (million) % 129.72/18.51 % (1952469)------------------------------ % 129.72/18.51 % (1952469)------------------------------ % 129.72/18.51 % (1952471)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=2952618360:fmbsr=2:i=46332_2967 on theBenchmark for (2967ds/46332Mi) % 129.72/18.51 % (1952471)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 129.72/18.51 % (1952471)Terminated due to inappropriate strategy. % 129.72/18.51 % (1952471)------------------------------ % 129.72/18.51 % (1952471)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 129.72/18.51 % (1952471)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 129.72/18.51 % (1952471)CaDiCaL version: 2.1.3 % 129.72/18.51 % (1952471)Termination reason: Inappropriate % 129.72/18.51 % (1952471)Time elapsed: 0.005 s % 129.72/18.51 % (1952471)Peak memory usage: 11 MB % 129.72/18.51 % (1952471)Instructions burned: 8 (million) % 129.72/18.51 % (1952471)------------------------------ % 129.72/18.51 % (1952471)------------------------------ % 129.72/18.51 % (1952473)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=2718598747:i=14071_2967 on theBenchmark for (2967ds/14071Mi) % 129.72/18.51 % (1952473)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 129.72/18.51 % (1952473)Terminated due to inappropriate strategy. % 129.72/18.51 % (1952473)------------------------------ % 129.72/18.51 % (1952473)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 129.72/18.51 % (1952473)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 129.72/18.51 % (1952473)CaDiCaL version: 2.1.3 % 129.72/18.51 % (1952473)Termination reason: Inappropriate % 129.72/18.51 % (1952473)Time elapsed: 0.005 s % 129.72/18.51 % (1952473)Peak memory usage: 11 MB % 129.72/18.51 % (1952473)Instructions burned: 8 (million) % 129.72/18.51 % (1952473)------------------------------ % 129.72/18.51 % (1952473)------------------------------ % 129.72/18.51 % (1952475)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=139841959:i=22565:add=on:rawr=on_2966 on theBenchmark for (2966ds/22565Mi) % 129.72/18.51 % (1952463)Instruction limit reached! % 129.72/18.51 % (1952463)------------------------------ % 129.72/18.51 % (1952463)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 129.72/18.51 % (1952463)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 129.72/18.51 % (1952463)CaDiCaL version: 2.1.3 % 129.72/18.51 % (1952463)Termination reason: Instruction limit % 129.72/18.51 % (1952463)Termination phase: Saturation % 129.72/18.51 % (1952463)Time elapsed: 1.386 s % 129.72/18.51 % (1952463)Peak memory usage: 64 MB % 129.72/18.51 % (1952463)Instructions burned: 4592 (million) % 129.72/18.51 % (1952477)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=1885382957:i=8173:av=off_2965 on theBenchmark for (2965ds/8173Mi) % 129.72/18.51 % (1952451)Instruction limit reached! % 130.44/18.64 % (1952451)------------------------------ % 130.44/18.64 % (1952451)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 130.44/18.64 % (1952451)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.44/18.64 % (1952451)CaDiCaL version: 2.1.3 % 130.44/18.64 % (1952451)Termination reason: Instruction limit % 130.44/18.64 % (1952451)Termination phase: Saturation % 130.44/18.64 % (1952451)Time elapsed: 3.288 s % 130.44/18.64 % (1952451)Peak memory usage: 44 MB % 130.44/18.64 % (1952451)Instructions burned: 5114 (million) % 130.44/18.64 % (1952479)dis+10_16:1_sil=16000:random_seed=1407657276:i=9155:fsr=off_2959 on theBenchmark for (2959ds/9155Mi) % 130.44/18.64 % (1952467)Instruction limit reached! % 130.44/18.64 % (1952467)------------------------------ % 130.44/18.64 % (1952467)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 130.44/18.64 % (1952467)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.44/18.64 % (1952467)CaDiCaL version: 2.1.3 % 130.44/18.64 % (1952467)Termination reason: Instruction limit % 130.44/18.64 % (1952467)Termination phase: Saturation % 130.44/18.64 % (1952467)Time elapsed: 2.708 s % 130.44/18.64 % (1952467)Peak memory usage: 47 MB % 130.44/18.64 % (1952467)Instructions burned: 5214 (million) % 130.44/18.64 % (1952481)ott-3_8_sil=64000:random_seed=2535534290:i=20139:bs=on_2943 on theBenchmark for (2943ds/20139Mi) % 130.44/18.64 % (1952477)Instruction limit reached! % 130.44/18.64 % (1952477)------------------------------ % 130.44/18.64 % (1952477)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 130.44/18.64 % (1952477)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.44/18.64 % (1952477)CaDiCaL version: 2.1.3 % 130.44/18.64 % (1952477)Termination reason: Instruction limit % 130.44/18.64 % (1952477)Termination phase: Saturation % 130.44/18.64 % (1952477)Time elapsed: 2.899 s % 130.44/18.64 % (1952477)Peak memory usage: 72 MB % 130.44/18.64 % (1952477)Instructions burned: 8174 (million) % 130.44/18.64 % (1952483)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=2311918339:fmbsr=2:i=32576_2936 on theBenchmark for (2936ds/32576Mi) % 130.44/18.64 % (1952483)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 130.44/18.64 % (1952483)Terminated due to inappropriate strategy. % 130.44/18.64 % (1952483)------------------------------ % 130.44/18.64 % (1952483)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 130.44/18.64 % (1952483)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.44/18.64 % (1952483)CaDiCaL version: 2.1.3 % 130.44/18.64 % (1952483)Termination reason: Inappropriate % 130.44/18.64 % (1952483)Time elapsed: 0.003 s % 130.44/18.64 % (1952483)Peak memory usage: 11 MB % 130.44/18.64 % (1952483)Instructions burned: 9 (million) % 130.44/18.64 % (1952483)------------------------------ % 130.44/18.64 % (1952483)------------------------------ % 130.44/18.64 % (1952485)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=2819329219:i=11404_2936 on theBenchmark for (2936ds/11404Mi) % 130.44/18.64 % (1952479)Instruction limit reached! % 130.44/18.64 % (1952479)------------------------------ % 130.44/18.64 % (1952479)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 130.44/18.64 % (1952479)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.44/18.64 % (1952479)CaDiCaL version: 2.1.3 % 130.44/18.64 % (1952479)Termination reason: Instruction limit % 130.44/18.64 % (1952479)Termination phase: Saturation % 130.44/18.64 % (1952479)Time elapsed: 4.803 s % 130.44/18.64 % (1952479)Peak memory usage: 55 MB % 130.44/18.64 % (1952479)Instructions burned: 9155 (million) % 130.44/18.64 % (1952487)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=1787419837:i=14134_2911 on theBenchmark for (2911ds/14134Mi) % 130.44/18.64 % (1952485)Instruction limit reached! % 130.44/18.64 % (1952485)------------------------------ % 130.44/18.64 % (1952485)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 130.44/18.64 % (1952485)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.44/18.64 % (1952485)CaDiCaL version: 2.1.3 % 130.44/18.64 % (1952485)Termination reason: Instruction limit % 130.44/18.64 % (1952485)Termination phase: Saturation % 130.44/18.64 % (1952485)Time elapsed: 4.012 s % 130.44/18.64 % (1952485)Peak memory usage: 73 MB % 130.44/18.64 % (1952485)Instructions burned: 11405 (million) % 130.44/18.64 % (1952490)dis+33_16_sil=32000:sac=on:random_seed=3624592059:i=15851:nm=0_2896 on theBenchmark for (2896ds/15851Mi) % 130.44/18.64 % (1952490)Instruction limit reached! % 130.44/18.64 % (1952490)------------------------------ % 130.44/18.64 % (1952490)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 137.42/19.64 % (1952490)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 137.42/19.64 % (1952490)CaDiCaL version: 2.1.3 % 137.42/19.64 % (1952490)Termination reason: Instruction limit % 137.42/19.64 % (1952490)Termination phase: Saturation % 137.42/19.64 % (1952490)Time elapsed: 3.741 s % 137.42/19.64 % (1952490)Peak memory usage: 147 MB % 137.42/19.64 % (1952490)Instructions burned: 15852 (million) % 137.42/19.64 % (1952518)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=2642519087:avsq=on:i=17627:add=on:amm=off_2858 on theBenchmark for (2858ds/17627Mi) % 137.42/19.64 % (1952475)Instruction limit reached! % 137.42/19.64 % (1952475)------------------------------ % 137.42/19.64 % (1952475)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 137.42/19.64 % (1952475)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 137.42/19.64 % (1952475)CaDiCaL version: 2.1.3 % 137.42/19.64 % (1952475)Termination reason: Instruction limit % 137.42/19.64 % (1952475)Termination phase: Saturation % 137.42/19.64 % (1952475)Time elapsed: 12.102 s % 137.42/19.64 % (1952475)Peak memory usage: 98 MB % 137.42/19.64 % (1952475)Instructions burned: 22565 (million) % 137.42/19.64 % (1952540)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=448970746:s2a=on:i=53295_2845 on theBenchmark for (2845ds/53295Mi) % 137.42/19.64 % (1952465)Instruction limit reached! % 137.42/19.64 % (1952465)------------------------------ % 137.42/19.64 % (1952465)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 137.42/19.64 % (1952465)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 137.42/19.64 % (1952465)CaDiCaL version: 2.1.3 % 137.42/19.64 % (1952465)Termination reason: Instruction limit % 137.42/19.64 % (1952465)Termination phase: Saturation % 137.42/19.64 % (1952465)Time elapsed: 14.973 s % 137.42/19.64 % (1952465)Peak memory usage: 273 MB % 137.42/19.64 % (1952465)Instructions burned: 29342 (million) % 137.42/19.64 % (1952542)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=1583431465:i=26857:ins=20_2822 on theBenchmark for (2822ds/26857Mi) % 137.42/19.64 % (1952542)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 137.42/19.64 % (1952542)Terminated due to inappropriate strategy. % 137.42/19.64 % (1952542)------------------------------ % 137.42/19.64 % (1952542)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 137.42/19.64 % (1952542)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 137.42/19.64 % (1952542)CaDiCaL version: 2.1.3 % 137.42/19.64 % (1952542)Termination reason: Inappropriate % 137.42/19.64 % (1952542)Time elapsed: 0.004 s % 137.42/19.64 % (1952542)Peak memory usage: 11 MB % 137.42/19.64 % (1952542)Instructions burned: 7 (million) % 137.42/19.64 % (1952542)------------------------------ % 137.42/19.64 % (1952542)------------------------------ % 137.42/19.64 % (1952544)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=3906402596:i=28120:bs=on:fsr=off_2822 on theBenchmark for (2822ds/28120Mi) % 137.42/19.64 % (1952487)Instruction limit reached! % 137.42/19.64 % (1952487)------------------------------ % 137.42/19.64 % (1952487)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 137.42/19.64 % (1952487)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 137.42/19.64 % (1952487)CaDiCaL version: 2.1.3 % 137.42/19.64 % (1952487)Termination reason: Instruction limit % 137.42/19.64 % (1952487)Termination phase: Saturation % 137.42/19.64 % (1952487)Time elapsed: 9.318 s % 137.42/19.64 % (1952487)Peak memory usage: 80 MB % 137.42/19.64 % (1952487)Instructions burned: 14134 (million) % 137.42/19.64 % (1952546)fmb+10_1_sil=256000:fmbss=7:random_seed=1597880668:fmbsr=1.6:i=182295_2817 on theBenchmark for (2817ds/182295Mi) % 137.42/19.64 % (1952546)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 137.42/19.64 % (1952546)Terminated due to inappropriate strategy. % 137.42/19.64 % (1952546)------------------------------ % 137.42/19.64 % (1952546)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 137.42/19.64 % (1952546)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 137.42/19.64 % (1952546)CaDiCaL version: 2.1.3 % 137.42/19.64 % (1952546)Termination reason: Inappropriate % 137.42/19.64 % (1952546)Time elapsed: 0.004 s % 137.42/19.64 % (1952546)Peak memory usage: 11 MB % 137.42/19.64 % (1952546)Instructions burned: 7 (million) % 137.42/19.64 % (1952546)------------------------------ % 137.42/19.64 % (1952546)------------------------------ % 137.42/19.64 % (1952548)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=3691041169:i=44625:gsp=on_2817 on theBenchmark for (2817ds/44625Mi) % 144.32/20.62 % (1952548)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 144.32/20.62 % (1952548)Terminated due to inappropriate strategy. % 144.32/20.62 % (1952548)------------------------------ % 144.32/20.62 % (1952548)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 144.32/20.62 % (1952548)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 144.32/20.62 % (1952548)CaDiCaL version: 2.1.3 % 144.32/20.62 % (1952548)Termination reason: Inappropriate % 144.32/20.62 % (1952548)Time elapsed: 0.004 s % 144.32/20.62 % (1952548)Peak memory usage: 11 MB % 144.32/20.62 % (1952548)Instructions burned: 8 (million) % 144.32/20.62 % (1952548)------------------------------ % 144.32/20.62 % (1952548)------------------------------ % 144.32/20.62 % (1952550)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=4101851330:i=160505_2817 on theBenchmark for (2817ds/160505Mi) % 144.32/20.62 % (1952550)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 144.32/20.62 % (1952550)Terminated due to inappropriate strategy. % 144.32/20.62 % (1952550)------------------------------ % 144.32/20.62 % (1952550)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 144.32/20.62 % (1952550)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 144.32/20.62 % (1952550)CaDiCaL version: 2.1.3 % 144.32/20.62 % (1952550)Termination reason: Inappropriate % 144.32/20.62 % (1952550)Time elapsed: 0.004 s % 144.32/20.62 % (1952550)Peak memory usage: 11 MB % 144.32/20.62 % (1952550)Instructions burned: 7 (million) % 144.32/20.62 % (1952550)------------------------------ % 144.32/20.62 % (1952550)------------------------------ % 144.32/20.62 % (1952552)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=3420350037:fmbsr=1.3:i=225729_2816 on theBenchmark for (2816ds/225729Mi) % 144.32/20.62 % (1952552)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 144.32/20.62 % (1952552)Terminated due to inappropriate strategy. % 144.32/20.62 % (1952552)------------------------------ % 144.32/20.62 % (1952552)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 144.32/20.62 % (1952552)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 144.32/20.62 % (1952552)CaDiCaL version: 2.1.3 % 144.32/20.62 % (1952552)Termination reason: Inappropriate % 144.32/20.62 % (1952552)Time elapsed: 0.005 s % 144.32/20.62 % (1952552)Peak memory usage: 11 MB % 144.32/20.62 % (1952552)Instructions burned: 8 (million) % 144.32/20.62 % (1952552)------------------------------ % 144.32/20.62 % (1952552)------------------------------ % 144.32/20.62 % (1952554)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=530483630:fmbsr=2:i=185024:ins=7_2816 on theBenchmark for (2816ds/185024Mi) % 144.32/20.62 % (1952554)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 144.32/20.62 % (1952554)Terminated due to inappropriate strategy. % 144.32/20.62 % (1952554)------------------------------ % 144.32/20.62 % (1952554)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 144.32/20.62 % (1952554)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 144.32/20.62 % (1952554)CaDiCaL version: 2.1.3 % 144.32/20.62 % (1952554)Termination reason: Inappropriate % 144.32/20.62 % (1952554)Time elapsed: 0.005 s % 144.32/20.62 % (1952554)Peak memory usage: 11 MB % 144.32/20.62 % (1952554)Instructions burned: 8 (million) % 144.32/20.62 % (1952554)------------------------------ % 144.32/20.62 % (1952554)------------------------------ % 144.32/20.62 % (1952556)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=396233392:rtra=on_2816 on theBenchmark for (2816ds/0Mi) % 144.32/20.62 % (1952556)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 144.32/20.62 % (1952556)Terminated due to inappropriate strategy. % 144.32/20.62 % (1952556)------------------------------ % 144.32/20.62 % (1952556)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 144.32/20.62 % (1952556)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 144.32/20.62 % (1952556)CaDiCaL version: 2.1.3 % 144.32/20.62 % (1952556)Termination reason: Inappropriate % 144.32/20.62 % (1952556)Time elapsed: 0.005 s % 144.32/20.62 % (1952556)Peak memory usage: 11 MB % 144.32/20.62 % (1952556)Instructions burned: 9 (million) % 144.32/20.62 % (1952556)------------------------------ % 144.32/20.62 % (1952556)------------------------------ % 144.32/20.62 % (1952558)% WARNING: option uhcvi not known. % 144.32/20.62 % (1952558)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2236595879:i=271062:add=off:rtra=on:rawr=on_2816 on theBenchmark for (2816ds/271062Mi) % 158.13/22.52 % (1952481)Instruction limit reached! % 158.13/22.52 % (1952481)------------------------------ % 158.13/22.52 % (1952481)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.13/22.52 % (1952481)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.13/22.52 % (1952481)CaDiCaL version: 2.1.3 % 158.13/22.52 % (1952481)Termination reason: Instruction limit % 158.13/22.52 % (1952481)Termination phase: Saturation % 158.13/22.52 % (1952481)Time elapsed: 12.815 s % 158.13/22.52 % (1952481)Peak memory usage: 114 MB % 158.13/22.52 % (1952481)Instructions burned: 20140 (million) % 158.13/22.52 % (1952560)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1203125811:i=176048:add=on:rtra=on:rawr=on_2814 on theBenchmark for (2814ds/176048Mi) % 158.13/22.52 % (1952518)Instruction limit reached! % 158.13/22.52 % (1952518)------------------------------ % 158.13/22.52 % (1952518)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.13/22.52 % (1952518)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.13/22.52 % (1952518)CaDiCaL version: 2.1.3 % 158.13/22.52 % (1952518)Termination reason: Instruction limit % 158.13/22.52 % (1952518)Termination phase: Saturation % 158.13/22.52 % (1952518)Time elapsed: 4.851 s % 158.13/22.52 % (1952518)Peak memory usage: 85 MB % 158.13/22.52 % (1952518)Instructions burned: 17628 (million) % 158.13/22.52 % (1952562)dis+10_1_sil=32000:si=on:sp=arity:random_seed=4055952990:i=206:fgj=on:rtra=on_2810 on theBenchmark for (2810ds/206Mi) % 158.13/22.52 % (1952562)Instruction limit reached! % 158.13/22.52 % (1952562)------------------------------ % 158.13/22.52 % (1952562)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.13/22.52 % (1952562)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.13/22.52 % (1952562)CaDiCaL version: 2.1.3 % 158.13/22.52 % (1952562)Termination reason: Instruction limit % 158.13/22.52 % (1952562)Termination phase: Saturation % 158.13/22.52 % (1952562)Time elapsed: 0.072 s % 158.13/22.52 % (1952562)Peak memory usage: 14 MB % 158.13/22.52 % (1952562)Instructions burned: 207 (million) % 158.13/22.52 % (1952564)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=188177701:i=232:rtra=on_2809 on theBenchmark for (2809ds/232Mi) % 158.13/22.52 % (1952564)Instruction limit reached! % 158.13/22.52 % (1952564)------------------------------ % 158.13/22.52 % (1952564)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.13/22.52 % (1952564)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.13/22.52 % (1952564)CaDiCaL version: 2.1.3 % 158.13/22.52 % (1952564)Termination reason: Instruction limit % 158.13/22.52 % (1952564)Termination phase: Saturation % 158.13/22.52 % (1952564)Time elapsed: 0.072 s % 158.13/22.52 % (1952564)Peak memory usage: 14 MB % 158.13/22.52 % (1952564)Instructions burned: 232 (million) % 158.13/22.52 % (1952566)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=3133251192:i=262:rtra=on_2808 on theBenchmark for (2808ds/262Mi) % 158.13/22.52 % (1952566)Instruction limit reached! % 158.13/22.52 % (1952566)------------------------------ % 158.13/22.52 % (1952566)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.13/22.52 % (1952566)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.13/22.52 % (1952566)CaDiCaL version: 2.1.3 % 158.13/22.52 % (1952566)Termination reason: Instruction limit % 158.13/22.52 % (1952566)Termination phase: Saturation % 158.13/22.52 % (1952566)Time elapsed: 0.089 s % 158.13/22.52 % (1952566)Peak memory usage: 15 MB % 158.13/22.52 % (1952566)Instructions burned: 264 (million) % 158.13/22.52 % (1952568)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=1271380622:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2807 on theBenchmark for (2807ds/318Mi) % 158.13/22.52 % (1952568)Instruction limit reached! % 158.13/22.52 % (1952568)------------------------------ % 158.13/22.52 % (1952568)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.13/22.52 % (1952568)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.13/22.52 % (1952568)CaDiCaL version: 2.1.3 % 158.13/22.52 % (1952568)Termination reason: Instruction limit % 158.13/22.52 % (1952568)Termination phase: Saturation % 158.13/22.52 % (1952568)Time elapsed: 0.116 s % 158.13/22.52 % (1952568)Peak memory usage: 15 MB % 158.13/22.52 % (1952568)Instructions burned: 321 (million) % 158.13/22.52 % (1952570)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=3249154543:i=1428:nm=2:rtra=on_2806 on theBenchmark for (2806ds/1428Mi) % 187.21/26.66 % (1952570)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 187.21/26.66 % (1952570)Terminated due to inappropriate strategy. % 187.21/26.66 % (1952570)------------------------------ % 187.21/26.66 % (1952570)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 187.21/26.66 % (1952570)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 187.21/26.66 % (1952570)CaDiCaL version: 2.1.3 % 187.21/26.66 % (1952570)Termination reason: Inappropriate % 187.21/26.66 % (1952570)Time elapsed: 0.002 s % 187.21/26.66 % (1952570)Peak memory usage: 11 MB % 187.21/26.66 % (1952570)Instructions burned: 8 (million) % 187.21/26.66 % (1952570)------------------------------ % 187.21/26.66 % (1952570)------------------------------ % 187.21/26.66 % (1952572)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=1748718472:i=262:bd=preordered:rtra=on:fsd=on_2805 on theBenchmark for (2805ds/262Mi) % 187.21/26.66 % (1952572)Instruction limit reached! % 187.21/26.66 % (1952572)------------------------------ % 187.21/26.66 % (1952572)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 187.21/26.66 % (1952572)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 187.21/26.66 % (1952572)CaDiCaL version: 2.1.3 % 187.21/26.66 % (1952572)Termination reason: Instruction limit % 187.21/26.66 % (1952572)Termination phase: Saturation % 187.21/26.66 % (1952572)Time elapsed: 0.119 s % 187.21/26.66 % (1952572)Peak memory usage: 14 MB % 187.21/26.66 % (1952572)Instructions burned: 263 (million) % 187.21/26.66 % (1952574)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=2928729256:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2804 on theBenchmark for (2804ds/1368Mi) % 187.21/26.66 % (1952574)Instruction limit reached! % 187.21/26.66 % (1952574)------------------------------ % 187.21/26.66 % (1952574)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 187.21/26.66 % (1952574)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 187.21/26.66 % (1952574)CaDiCaL version: 2.1.3 % 187.21/26.66 % (1952574)Termination reason: Instruction limit % 187.21/26.66 % (1952574)Termination phase: Saturation % 187.21/26.66 % (1952574)Time elapsed: 0.379 s % 187.21/26.66 % (1952574)Peak memory usage: 19 MB % 187.21/26.66 % (1952574)Instructions burned: 1370 (million) % 187.21/26.66 % (1952576)ott-21_1_sil=16000:si=on:fs=off:random_seed=1565337291:i=360:av=off:fsr=off:rtra=on_2800 on theBenchmark for (2800ds/360Mi) % 187.21/26.66 % (1952576)Instruction limit reached! % 187.21/26.66 % (1952576)------------------------------ % 187.21/26.66 % (1952576)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 187.21/26.66 % (1952576)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 187.21/26.66 % (1952576)CaDiCaL version: 2.1.3 % 187.21/26.66 % (1952576)Termination reason: Instruction limit % 187.21/26.66 % (1952576)Termination phase: Saturation % 187.21/26.66 % (1952576)Time elapsed: 0.095 s % 187.21/26.66 % (1952576)Peak memory usage: 14 MB % 187.21/26.66 % (1952576)Instructions burned: 362 (million) % 187.21/26.66 % (1952578)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=590190520:i=954:bd=all:rtra=on_2799 on theBenchmark for (2799ds/954Mi) % 187.21/26.66 % (1952578)Instruction limit reached! % 187.21/26.66 % (1952578)------------------------------ % 187.21/26.66 % (1952578)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 187.21/26.66 % (1952578)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 187.21/26.66 % (1952578)CaDiCaL version: 2.1.3 % 187.21/26.66 % (1952578)Termination reason: Instruction limit % 187.21/26.66 % (1952578)Termination phase: Saturation % 187.21/26.66 % (1952578)Time elapsed: 0.313 s % 187.21/26.66 % (1952578)Peak memory usage: 16 MB % 187.21/26.66 % (1952578)Instructions burned: 955 (million) % 187.21/26.66 % (1952580)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=1576289556:fmbsr=1.3:i=1730:ins=25:rtra=on_2796 on theBenchmark for (2796ds/1730Mi) % 187.21/26.66 % (1952580)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 187.21/26.66 % (1952580)Terminated due to inappropriate strategy. % 187.21/26.66 % (1952580)------------------------------ % 187.21/26.66 % (1952580)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 187.21/26.66 % (1952580)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 187.21/26.66 % (1952580)CaDiCaL version: 2.1.3 % 187.21/26.66 % (1952580)Termination reason: Inappropriate % 187.21/26.66 % (1952580)Time elapsed: 0.002 s % 236.89/33.65 % (1952580)Peak memory usage: 10 MB % 236.89/33.65 % (1952580)Instructions burned: 8 (million) % 236.89/33.65 % (1952580)------------------------------ % 236.89/33.65 % (1952580)------------------------------ % 236.89/33.65 % (1952582)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=427723938:i=2358:rtra=on_2796 on theBenchmark for (2796ds/2358Mi) % 236.89/33.65 % (1952582)Instruction limit reached! % 236.89/33.65 % (1952582)------------------------------ % 236.89/33.65 % (1952582)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 236.89/33.65 % (1952582)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 236.89/33.65 % (1952582)CaDiCaL version: 2.1.3 % 236.89/33.65 % (1952582)Termination reason: Instruction limit % 236.89/33.65 % (1952582)Termination phase: Saturation % 236.89/33.65 % (1952582)Time elapsed: 0.813 s % 236.89/33.65 % (1952582)Peak memory usage: 31 MB % 236.89/33.65 % (1952582)Instructions burned: 2359 (million) % 236.89/33.65 % (1952584)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=944076644:i=1778:ins=1:rtra=on_2787 on theBenchmark for (2787ds/1778Mi) % 236.89/33.65 % (1952584)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 236.89/33.65 % (1952584)Terminated due to inappropriate strategy. % 236.89/33.65 % (1952584)------------------------------ % 236.89/33.65 % (1952584)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 236.89/33.65 % (1952584)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 236.89/33.65 % (1952584)CaDiCaL version: 2.1.3 % 236.89/33.65 % (1952584)Termination reason: Inappropriate % 236.89/33.65 % (1952584)Time elapsed: 0.002 s % 236.89/33.65 % (1952584)Peak memory usage: 10 MB % 236.89/33.65 % (1952584)Instructions burned: 8 (million) % 236.89/33.65 % (1952584)------------------------------ % 236.89/33.65 % (1952584)------------------------------ % 236.89/33.65 % (1952586)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=1940844923:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2787 on theBenchmark for (2787ds/1384Mi) % 236.89/33.65 % (1952586)Instruction limit reached! % 236.89/33.65 % (1952586)------------------------------ % 236.89/33.65 % (1952586)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 236.89/33.65 % (1952586)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 236.89/33.65 % (1952586)CaDiCaL version: 2.1.3 % 236.89/33.65 % (1952586)Termination reason: Instruction limit % 236.89/33.65 % (1952586)Termination phase: Saturation % 236.89/33.65 % (1952586)Time elapsed: 0.451 s % 236.89/33.65 % (1952586)Peak memory usage: 23 MB % 236.89/33.65 % (1952586)Instructions burned: 1386 (million) % 236.89/33.65 % (1952588)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=2978779621:i=1758:kws=inv_precedence:fsr=off:rtra=on_2782 on theBenchmark for (2782ds/1758Mi) % 236.89/33.65 % (1952588)Instruction limit reached! % 236.89/33.65 % (1952588)------------------------------ % 236.89/33.65 % (1952588)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 236.89/33.65 % (1952588)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 236.89/33.65 % (1952588)CaDiCaL version: 2.1.3 % 236.89/33.65 % (1952588)Termination reason: Instruction limit % 236.89/33.65 % (1952588)Termination phase: Saturation % 236.89/33.65 % (1952588)Time elapsed: 0.543 s % 236.89/33.65 % (1952588)Peak memory usage: 25 MB % 236.89/33.65 % (1952588)Instructions burned: 1760 (million) % 236.89/33.65 % (1952590)fmb+10_1_sil=64000:si=on:random_seed=3038240187:i=44122:nm=2:rtra=on:gsp=on_2777 on theBenchmark for (2777ds/44122Mi) % 236.89/33.65 % (1952590)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 236.89/33.65 % (1952590)Terminated due to inappropriate strategy. % 236.89/33.65 % (1952590)------------------------------ % 236.89/33.65 % (1952590)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 236.89/33.65 % (1952590)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 236.89/33.65 % (1952590)CaDiCaL version: 2.1.3 % 236.89/33.65 % (1952590)Termination reason: Inappropriate % 236.89/33.65 % (1952590)Time elapsed: 0.003 s % 236.89/33.65 % (1952590)Peak memory usage: 11 MB % 236.89/33.65 % (1952590)Instructions burned: 9 (million) % 236.89/33.65 % (1952590)------------------------------ % 236.89/33.65 % (1952590)------------------------------ % 236.89/33.65 % (1952592)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=3902658870:i=19030:nm=5:rtra=on_2777 on theBenchmark for (2777ds/19030Mi) % 261.98/40.78 % (1952592)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 261.98/40.78 % (1952592)Terminated due to inappropriate strategy. % 261.98/40.78 % (1952592)------------------------------ % 261.98/40.78 % (1952592)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 261.98/40.78 % (1952592)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 261.98/40.78 % (1952592)CaDiCaL version: 2.1.3 % 261.98/40.78 % (1952592)Termination reason: Inappropriate % 261.98/40.78 % (1952592)Time elapsed: 0.005 s % 261.98/40.78 % (1952592)Peak memory usage: 11 MB % 261.98/40.78 % (1952592)Instructions burned: 8 (million) % 261.98/40.78 % (1952592)------------------------------ % 261.98/40.78 % (1952592)------------------------------ % 261.98/40.78 % (1952594)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=3027431644:fmbsr=1.7:i=1840:rtra=on_2776 on theBenchmark for (2776ds/1840Mi) % 261.98/40.78 % (1952594)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 261.98/40.78 % (1952594)Terminated due to inappropriate strategy. % 261.98/40.78 % (1952594)------------------------------ % 261.98/40.78 % (1952594)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 261.98/40.78 % (1952594)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 261.98/40.78 % (1952594)CaDiCaL version: 2.1.3 % 261.98/40.78 % (1952594)Termination reason: Inappropriate % 261.98/40.78 % (1952594)Time elapsed: 0.005 s % 261.98/40.78 % (1952594)Peak memory usage: 11 MB % 261.98/40.78 % (1952594)Instructions burned: 8 (million) % 261.98/40.78 % (1952594)------------------------------ % 261.98/40.78 % (1952594)------------------------------ % 261.98/40.78 % (1952596)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=1540974346:i=10262:rtra=on_2776 on theBenchmark for (2776ds/10262Mi) % 261.98/40.78 % (1952596)Instruction limit reached! % 261.98/40.78 % (1952596)------------------------------ % 261.98/40.78 % (1952596)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 261.98/40.78 % (1952596)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 261.98/40.78 % (1952596)CaDiCaL version: 2.1.3 % 261.98/40.78 % (1952596)Termination reason: Instruction limit % 261.98/40.78 % (1952596)Termination phase: Saturation % 261.98/40.78 % (1952596)Time elapsed: 3.256 s % 261.98/40.78 % (1952596)Peak memory usage: 98 MB % 261.98/40.78 % (1952596)Instructions burned: 10264 (million) % 261.98/40.78 % (1952598)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2754786389:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2743 on theBenchmark for (2743ds/2944Mi) % 261.98/40.78 % (1952598)Instruction limit reached! % 261.98/40.78 % (1952598)------------------------------ % 261.98/40.78 % (1952598)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 261.98/40.78 % (1952598)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 261.98/40.78 % (1952598)CaDiCaL version: 2.1.3 % 261.98/40.78 % (1952598)Termination reason: Instruction limit % 261.98/40.78 % (1952598)Termination phase: Saturation % 261.98/40.78 % (1952598)Time elapsed: 0.775 s % 261.98/40.78 % (1952598)Peak memory usage: 26 MB % 261.98/40.78 % (1952598)Instructions burned: 2945 (million) % 261.98/40.78 % (1952600)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=1723339915:i=12648:rtra=on_2735 on theBenchmark for (2735ds/12648Mi) % 261.98/40.78 % (1952600)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 261.98/40.78 % (1952600)Terminated due to inappropriate strategy. % 261.98/40.78 % (1952600)------------------------------ % 261.98/40.78 % (1952600)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 261.98/40.78 % (1952600)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 261.98/40.78 % (1952600)CaDiCaL version: 2.1.3 % 261.98/40.78 % (1952600)Termination reason: Inappropriate % 261.98/40.78 % (1952600)Time elapsed: 0.003 s % 261.98/40.78 % (1952600)Peak memory usage: 11 MB % 261.98/40.78 % (1952600)Instructions burned: 9 (million) % 261.98/40.78 % (1952600)------------------------------ % 261.98/40.78 % (1952600)------------------------------ % 261.98/40.78 % (1952602)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=1896157811:fmbsr=2.30978:i=4348:rtra=on_2735 on theBenchmark for (2735ds/4348Mi) % 261.98/40.78 % (1952602)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 261.98/40.78 % (1952602)Terminated due to inappropriate strategy. % 261.98/40.78 % (1952602)------------------------------ % 261.98/40.78 % (1952602)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.06/42.54 % (1952602)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.06/42.54 % (1952602)CaDiCaL version: 2.1.3 % 300.06/42.54 % (1952602)Termination reason: Inappropriate % 300.06/42.54 % (1952602)Time elapsed: 0.002 s % 300.06/42.54 % (1952602)Peak memory usage: 11 MB % 300.06/42.54 % (1952602)Instructions burned: 8 (million) % 300.06/42.54 % (1952602)------------------------------ % 300.06/42.54 % (1952602)------------------------------ % 300.06/42.54 % (1952604)ott-2_1_sil=16000:si=on:newcnf=on:random_seed=235364414:avsq=on:i=1738:avsqr=1,16:kws=inv_arity_squared:rtra=on_2735 on theBenchmark for (2735ds/1738Mi) % 300.06/42.54 % (1952604)Instruction limit reached! % 300.06/42.54 % (1952604)------------------------------ % 300.06/42.54 % (1952604)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.06/42.54 % (1952604)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.06/42.54 % (1952604)CaDiCaL version: 2.1.3 % 300.06/42.54 % (1952604)Termination reason: Instruction limit % 300.06/42.54 % (1952604)Termination phase: Saturation % 300.06/42.54 % (1952604)Time elapsed: 0.592 s % 300.06/42.54 % (1952604)Peak memory usage: 19 MB % 300.06/42.54 % (1952604)Instructions burned: 1740 (million) % 300.06/42.54 % (1952606)ott+10_1_sil=32000:tgt=ground:si=on:random_seed=3093833151:i=10228:av=off:rtra=on_2729 on theBenchmark for (2729ds/10228Mi) % 300.06/42.54 % (1952606)Instruction limit reached! % 300.06/42.54 % (1952606)------------------------------ % 300.06/42.54 % (1952606)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.06/42.54 % (1952606)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.06/42.54 % (1952606)CaDiCaL version: 2.1.3 % 300.06/42.54 % (1952606)Termination reason: Instruction limit % 300.06/42.54 % (1952606)Termination phase: Saturation % 300.06/42.54 % (1952606)Time elapsed: 4.007 s % 300.06/42.54 % (1952606)Peak memory usage: 70 MB % 300.06/42.54 % (1952606)Instructions burned: 10230 (million) % 300.06/42.54 % (1952610)fmb+10_1_sil=64000:sas=cadical:si=on:bce=on:rp=on:random_seed=1129871362:i=108564:rtra=on_2689 on theBenchmark for (2689ds/108564Mi) % 300.06/42.54 % (1952610)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.06/42.54 % (1952610)Terminated due to inappropriate strategy. % 300.06/42.54 % (1952610)------------------------------ % 300.06/42.54 % (1952610)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.06/42.54 % (1952610)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.06/42.54 % (1952610)CaDiCaL version: 2.1.3 % 300.06/42.54 % (1952610)Termination reason: Inappropriate % 300.06/42.54 % (1952610)Time elapsed: 0.003 s % 300.06/42.54 % (1952610)Peak memory usage: 11 MB % 300.06/42.54 % (1952610)Instructions burned: 9 (million) % 300.06/42.54 % (1952610)------------------------------ % 300.06/42.54 % (1952610)------------------------------ % 300.06/42.54 % (1952612)dis-11_1_sil=16000:si=on:sp=reverse_frequency:alpa=true:random_seed=2839251274:i=7024:aac=none:rtra=on_2689 on theBenchmark for (2689ds/7024Mi) % 300.06/42.54 % (1952544)Instruction limit reached! % 300.06/42.54 % (1952544)------------------------------ % 300.06/42.54 % (1952544)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.06/42.54 % (1952544)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.06/42.54 % (1952544)CaDiCaL version: 2.1.3 % 300.06/42.54 % (1952544)Termination reason: Instruction limit % 300.06/42.54 % (1952544)Termination phase: Saturation % 300.06/42.54 % (1952544)Time elapsed: 13.848 s % 300.06/42.54 % (1952544)Peak memory usage: 37 MB % 300.06/42.54 % (1952544)Instructions burned: 28120 (million) % 300.06/42.54 % (1952614)dis+21_1_sil=32000:sas=cadical:si=on:random_seed=3949981122:i=7546:rtra=on:amm=off_2683 on theBenchmark for (2683ds/7546Mi) % 300.06/42.54 % (1952612)Instruction limit reached! % 300.06/42.54 % (1952612)------------------------------ % 300.06/42.54 % (1952612)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.06/42.54 % (1952612)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.06/42.54 % (1952612)CaDiCaL version: 2.1.3 % 300.06/42.54 % (1952612)Termination reason: Instruction limit % 300.06/42.54 % (1952612)Termination phase: Saturation % 300.06/42.54 % (1952612)Time elapsed: 2.315 s % 300.06/42.54 % (1952612)Peak memory usage: 75 MB % 300.06/42.54 % (1952612)Instructions burned: 7026 (million) % 300.06/42.54 % (1952616)ott+11_1_sil=16000:si=on:gs=on:random_seed=1622216398:s2a=on:i=4502:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:rtra=on:fsd=on_2665 on theBenchmark f % 300.06/42.54 Terminated % 300.06/42.54 % Vampire exiting % 300.06/42.54 Terminated %------------------------------------------------------------------------------