%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW645_2 : TPTP v9.3.1. Released v6.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n009.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:35 PM UTC 2026 % Result : Timeout 300.16s 42.64s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWW645_2 : TPTP v9.3.1. Released v6.1.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.10/0.23 % Computer : n009.cluster.edu % 0.10/0.23 % Model : x86_64 x86_64 % 0.10/0.23 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.23 % Memory : 8046.5625MB % 0.10/0.23 % OS : Linux 6.8.0-71-generic % 0.10/0.23 % CPULimit : 300 % 0.10/0.23 % WCLimit : 300 % 0.10/0.23 % DateTime : Mon Sep 28 14:23:30 UTC 2026 % 0.10/0.23 % CPUTime : % 0.10/0.23 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.26/0.29 Running first-order model finding % 0.26/0.29 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 5.19/1.12 % (3061358)Will run a generic schedule for satisfiability detection. % 5.19/1.12 % (3061366)dis+10_1_sil=32000:sp=arity:random_seed=1877486142:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 5.19/1.12 % (3061364)% WARNING: option uhcvi not known. % 5.19/1.12 % (3061363)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3925494082_2999 on theBenchmark for (2999ds/0Mi) % 5.19/1.12 % (3061364)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1998486340:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 5.19/1.12 % (3061365)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3210006687:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 5.19/1.12 % (3061368)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2207332833:i=131_2999 on theBenchmark for (2999ds/131Mi) % 5.19/1.12 % (3061367)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1228353307:i=116_2999 on theBenchmark for (2999ds/116Mi) % 5.19/1.12 % (3061369)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2779538051:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 5.19/1.12 % (3061366)Instruction limit reached! % 5.19/1.12 % (3061366)------------------------------ % 5.19/1.12 % (3061366)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.19/1.12 % (3061366)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.19/1.12 % (3061366)CaDiCaL version: 2.1.3 % 5.19/1.12 % (3061366)Termination reason: Instruction limit % 5.19/1.12 % (3061366)Termination phase: Saturation % 5.19/1.12 % (3061366)Time elapsed: 0.047 s % 5.19/1.12 % (3061366)Peak memory usage: 13 MB % 5.19/1.12 % (3061366)Instructions burned: 104 (million) % 5.19/1.12 % (3061377)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1373587236:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi) % 5.19/1.12 % (3061363)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 5.19/1.12 % (3061363)Terminated due to inappropriate strategy. % 5.19/1.12 % (3061363)------------------------------ % 5.19/1.12 % (3061363)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.19/1.12 % (3061363)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.19/1.12 % (3061363)CaDiCaL version: 2.1.3 % 5.19/1.12 % (3061363)Termination reason: Inappropriate % 5.19/1.12 % (3061363)Time elapsed: 0.076 s % 5.19/1.12 % (3061363)Peak memory usage: 12 MB % 5.19/1.12 % (3061363)Instructions burned: 91 (million) % 5.19/1.12 % (3061363)------------------------------ % 5.19/1.12 % (3061363)------------------------------ % 5.19/1.12 % (3061367)Instruction limit reached! % 5.19/1.12 % (3061367)------------------------------ % 5.19/1.12 % (3061367)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.19/1.12 % (3061367)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.19/1.12 % (3061367)CaDiCaL version: 2.1.3 % 5.19/1.12 % (3061367)Termination reason: Instruction limit % 5.19/1.12 % (3061367)Termination phase: NewCNF % 5.19/1.12 % (3061367)Time elapsed: 0.083 s % 5.19/1.12 % (3061367)Peak memory usage: 12 MB % 5.19/1.12 % (3061367)Instructions burned: 117 (million) % 5.19/1.12 % (3061377)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 5.19/1.12 % (3061377)Terminated due to inappropriate strategy. % 5.19/1.12 % (3061377)------------------------------ % 5.19/1.12 % (3061377)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.19/1.12 % (3061377)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.19/1.12 % (3061377)CaDiCaL version: 2.1.3 % 5.19/1.12 % (3061377)Termination reason: Inappropriate % 5.19/1.12 % (3061377)Time elapsed: 0.035 s % 5.19/1.12 % (3061377)Peak memory usage: 13 MB % 5.19/1.12 % (3061377)Instructions burned: 70 (million) % 5.19/1.12 % (3061377)------------------------------ % 5.19/1.12 % (3061377)------------------------------ % 5.19/1.12 % (3061380)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=1137840870:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 5.19/1.12 % (3061379)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1538478295:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi) % 5.19/1.12 % (3061368)Instruction limit reached! % 5.19/1.12 % (3061368)------------------------------ % 5.19/1.12 % (3061368)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.39/1.70 % (3061368)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.39/1.70 % (3061368)CaDiCaL version: 2.1.3 % 7.39/1.70 % (3061368)Termination reason: Instruction limit % 7.39/1.70 % (3061368)Termination phase: Saturation % 7.39/1.70 % (3061368)Time elapsed: 0.113 s % 7.39/1.70 % (3061368)Peak memory usage: 14 MB % 7.39/1.70 % (3061368)Instructions burned: 132 (million) % 7.39/1.70 % (3061381)ott-21_1_sil=16000:fs=off:random_seed=1060302811:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 7.39/1.70 % (3061384)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3247098300:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 7.39/1.70 % (3061369)Instruction limit reached! % 7.39/1.70 % (3061369)------------------------------ % 7.39/1.70 % (3061369)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.39/1.70 % (3061369)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.39/1.70 % (3061369)CaDiCaL version: 2.1.3 % 7.39/1.70 % (3061369)Termination reason: Instruction limit % 7.39/1.70 % (3061369)Termination phase: Saturation % 7.39/1.70 % (3061369)Time elapsed: 0.149 s % 7.39/1.70 % (3061369)Peak memory usage: 14 MB % 7.39/1.70 % (3061369)Instructions burned: 159 (million) % 7.39/1.70 % (3061387)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=298081481:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi) % 7.39/1.70 % (3061379)Instruction limit reached! % 7.39/1.70 % (3061379)------------------------------ % 7.39/1.70 % (3061379)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.39/1.70 % (3061379)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.39/1.70 % (3061379)CaDiCaL version: 2.1.3 % 7.39/1.70 % (3061379)Termination reason: Instruction limit % 7.39/1.70 % (3061379)Termination phase: Saturation % 7.39/1.70 % (3061379)Time elapsed: 0.110 s % 7.39/1.70 % (3061379)Peak memory usage: 14 MB % 7.39/1.70 % (3061379)Instructions burned: 131 (million) % 7.39/1.70 % (3061381)Instruction limit reached! % 7.39/1.70 % (3061381)------------------------------ % 7.39/1.70 % (3061381)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.39/1.70 % (3061381)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.39/1.70 % (3061381)CaDiCaL version: 2.1.3 % 7.39/1.70 % (3061381)Termination reason: Instruction limit % 7.39/1.70 % (3061381)Termination phase: Saturation % 7.39/1.70 % (3061381)Time elapsed: 0.140 s % 7.39/1.70 % (3061381)Peak memory usage: 13 MB % 7.39/1.70 % (3061381)Instructions burned: 181 (million) % 7.39/1.70 % (3061389)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1014248104:i=1179_2996 on theBenchmark for (2996ds/1179Mi) % 7.39/1.70 % (3061387)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 7.39/1.70 % (3061387)Terminated due to inappropriate strategy. % 7.39/1.70 % (3061387)------------------------------ % 7.39/1.70 % (3061387)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.39/1.70 % (3061387)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.39/1.70 % (3061387)CaDiCaL version: 2.1.3 % 7.39/1.70 % (3061387)Termination reason: Inappropriate % 7.39/1.70 % (3061387)Time elapsed: 0.070 s % 7.39/1.70 % (3061387)Peak memory usage: 12 MB % 7.39/1.70 % (3061387)Instructions burned: 78 (million) % 7.39/1.70 % (3061387)------------------------------ % 7.39/1.70 % (3061387)------------------------------ % 7.39/1.70 % (3061390)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3141623228:i=889:ins=1_2996 on theBenchmark for (2996ds/889Mi) % 7.39/1.70 % (3061392)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=1733131073:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2996 on theBenchmark for (2996ds/692Mi) % 7.39/1.70 % (3061390)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 7.39/1.70 % (3061390)Terminated due to inappropriate strategy. % 7.39/1.70 % (3061390)------------------------------ % 7.39/1.70 % (3061390)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.39/1.70 % (3061390)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.39/1.70 % (3061390)CaDiCaL version: 2.1.3 % 7.39/1.70 % (3061390)Termination reason: Inappropriate % 7.39/1.70 % (3061390)Time elapsed: 0.040 s % 7.39/1.70 % (3061390)Peak memory usage: 12 MB % 31.30/4.84 % (3061390)Instructions burned: 77 (million) % 31.30/4.84 % (3061390)------------------------------ % 31.30/4.84 % (3061390)------------------------------ % 31.30/4.84 % (3061395)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2657206792:i=879:kws=inv_precedence:fsr=off_2995 on theBenchmark for (2995ds/879Mi) % 31.30/4.84 % (3061380)Instruction limit reached! % 31.30/4.84 % (3061380)------------------------------ % 31.30/4.84 % (3061380)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 31.30/4.84 % (3061380)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.30/4.84 % (3061380)CaDiCaL version: 2.1.3 % 31.30/4.84 % (3061380)Termination reason: Instruction limit % 31.30/4.84 % (3061380)Termination phase: Saturation % 31.30/4.84 % (3061380)Time elapsed: 0.293 s % 31.30/4.84 % (3061380)Peak memory usage: 17 MB % 31.30/4.84 % (3061380)Instructions burned: 684 (million) % 31.30/4.84 % (3061397)fmb+10_1_sil=64000:random_seed=3024787159:i=22061:nm=2:gsp=on_2995 on theBenchmark for (2995ds/22061Mi) % 31.30/4.84 % (3061397)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 31.30/4.84 % (3061397)Terminated due to inappropriate strategy. % 31.30/4.84 % (3061397)------------------------------ % 31.30/4.84 % (3061397)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 31.30/4.84 % (3061397)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.30/4.84 % (3061397)CaDiCaL version: 2.1.3 % 31.30/4.84 % (3061397)Termination reason: Inappropriate % 31.30/4.84 % (3061397)Time elapsed: 0.077 s % 31.30/4.84 % (3061397)Peak memory usage: 12 MB % 31.30/4.84 % (3061397)Instructions burned: 75 (million) % 31.30/4.84 % (3061397)------------------------------ % 31.30/4.84 % (3061397)------------------------------ % 31.30/4.84 % (3061399)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1775894473:i=9515:nm=5_2993 on theBenchmark for (2993ds/9515Mi) % 31.30/4.84 % (3061399)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 31.30/4.84 % (3061399)Terminated due to inappropriate strategy. % 31.30/4.84 % (3061399)------------------------------ % 31.30/4.84 % (3061399)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 31.30/4.84 % (3061399)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.30/4.84 % (3061399)CaDiCaL version: 2.1.3 % 31.30/4.84 % (3061399)Termination reason: Inappropriate % 31.30/4.84 % (3061399)Time elapsed: 0.037 s % 31.30/4.84 % (3061399)Peak memory usage: 12 MB % 31.30/4.84 % (3061399)Instructions burned: 75 (million) % 31.30/4.84 % (3061399)------------------------------ % 31.30/4.84 % (3061399)------------------------------ % 31.30/4.84 % (3061401)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3655316725:fmbsr=1.7:i=920_2993 on theBenchmark for (2993ds/920Mi) % 31.30/4.84 % (3061384)Instruction limit reached! % 31.30/4.84 % (3061384)------------------------------ % 31.30/4.84 % (3061384)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 31.30/4.84 % (3061384)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.30/4.84 % (3061384)CaDiCaL version: 2.1.3 % 31.30/4.84 % (3061384)Termination reason: Instruction limit % 31.30/4.84 % (3061384)Termination phase: Saturation % 31.30/4.84 % (3061384)Time elapsed: 0.485 s % 31.30/4.84 % (3061384)Peak memory usage: 15 MB % 31.30/4.84 % (3061384)Instructions burned: 477 (million) % 31.30/4.84 % (3061401)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 31.30/4.84 % (3061401)Terminated due to inappropriate strategy. % 31.30/4.84 % (3061401)------------------------------ % 31.30/4.84 % (3061401)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 31.30/4.84 % (3061401)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.30/4.84 % (3061401)CaDiCaL version: 2.1.3 % 31.30/4.84 % (3061401)Termination reason: Inappropriate % 31.30/4.84 % (3061401)Time elapsed: 0.070 s % 31.30/4.84 % (3061401)Peak memory usage: 12 MB % 31.30/4.84 % (3061401)Instructions burned: 77 (million) % 31.30/4.84 % (3061401)------------------------------ % 31.30/4.84 % (3061401)------------------------------ % 31.30/4.84 % (3061403)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2823481761:i=5131_2992 on theBenchmark for (2992ds/5131Mi) % 31.30/4.84 % (3061405)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2921241287:i=1472:ins=7:fdi=8:gsp=on_2992 on theBenchmark for (2992ds/1472Mi) % 31.30/4.84 % (3061395)Instruction limit reached! % 31.30/4.84 % (3061395)------------------------------ % 41.71/6.26 % (3061395)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 41.71/6.26 % (3061395)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.71/6.26 % (3061395)CaDiCaL version: 2.1.3 % 41.71/6.26 % (3061395)Termination reason: Instruction limit % 41.71/6.26 % (3061395)Termination phase: Saturation % 41.71/6.26 % (3061395)Time elapsed: 0.389 s % 41.71/6.26 % (3061395)Peak memory usage: 17 MB % 41.71/6.26 % (3061395)Instructions burned: 881 (million) % 41.71/6.26 % (3061407)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=826362081:i=6324_2991 on theBenchmark for (2991ds/6324Mi) % 41.71/6.26 % (3061407)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 41.71/6.26 % (3061407)Terminated due to inappropriate strategy. % 41.71/6.26 % (3061407)------------------------------ % 41.71/6.26 % (3061407)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 41.71/6.26 % (3061407)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.71/6.26 % (3061407)CaDiCaL version: 2.1.3 % 41.71/6.26 % (3061407)Termination reason: Inappropriate % 41.71/6.26 % (3061407)Time elapsed: 0.086 s % 41.71/6.26 % (3061407)Peak memory usage: 12 MB % 41.71/6.26 % (3061407)Instructions burned: 90 (million) % 41.71/6.26 % (3061407)------------------------------ % 41.71/6.26 % (3061407)------------------------------ % 41.71/6.26 % (3061409)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2591785950:fmbsr=2.30978:i=2174_2990 on theBenchmark for (2990ds/2174Mi) % 41.71/6.26 % (3061392)Instruction limit reached! % 41.71/6.26 % (3061392)------------------------------ % 41.71/6.26 % (3061392)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 41.71/6.26 % (3061392)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.71/6.26 % (3061392)CaDiCaL version: 2.1.3 % 41.71/6.26 % (3061392)Termination reason: Instruction limit % 41.71/6.26 % (3061392)Termination phase: Saturation % 41.71/6.26 % (3061392)Time elapsed: 0.585 s % 41.71/6.26 % (3061392)Peak memory usage: 17 MB % 41.71/6.26 % (3061392)Instructions burned: 692 (million) % 41.71/6.26 % (3061411)ott-2_1_sil=16000:newcnf=on:random_seed=572670626:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2990 on theBenchmark for (2990ds/869Mi) % 41.71/6.26 % (3061409)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 41.71/6.26 % (3061409)Terminated due to inappropriate strategy. % 41.71/6.26 % (3061409)------------------------------ % 41.71/6.26 % (3061409)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 41.71/6.26 % (3061409)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.71/6.26 % (3061409)CaDiCaL version: 2.1.3 % 41.71/6.26 % (3061409)Termination reason: Inappropriate % 41.71/6.26 % (3061409)Time elapsed: 0.069 s % 41.71/6.26 % (3061409)Peak memory usage: 11 MB % 41.71/6.26 % (3061409)Instructions burned: 77 (million) % 41.71/6.26 % (3061409)------------------------------ % 41.71/6.26 % (3061409)------------------------------ % 41.71/6.26 % (3061413)ott+10_1_sil=32000:tgt=ground:random_seed=2461002433:i=5114:av=off_2989 on theBenchmark for (2989ds/5114Mi) % 41.71/6.26 % (3061389)Instruction limit reached! % 41.71/6.26 % (3061389)------------------------------ % 41.71/6.26 % (3061389)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 41.71/6.26 % (3061389)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.71/6.26 % (3061389)CaDiCaL version: 2.1.3 % 41.71/6.26 % (3061389)Termination reason: Instruction limit % 41.71/6.26 % (3061389)Termination phase: Saturation % 41.71/6.26 % (3061389)Time elapsed: 0.985 s % 41.71/6.26 % (3061389)Peak memory usage: 20 MB % 41.71/6.26 % (3061389)Instructions burned: 1180 (million) % 41.71/6.26 % (3061415)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3964740376:i=54282_2986 on theBenchmark for (2986ds/54282Mi) % 41.71/6.26 % (3061415)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 41.71/6.26 % (3061415)Terminated due to inappropriate strategy. % 41.71/6.26 % (3061415)------------------------------ % 41.71/6.26 % (3061415)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 41.71/6.26 % (3061415)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.71/6.26 % (3061415)CaDiCaL version: 2.1.3 % 41.71/6.26 % (3061415)Termination reason: Inappropriate % 41.71/6.26 % (3061415)Time elapsed: 0.046 s % 41.71/6.26 % (3061415)Peak memory usage: 12 MB % 41.71/6.26 % (3061415)Instructions burned: 91 (million) % 134.08/19.30 % (3061415)------------------------------ % 134.08/19.30 % (3061415)------------------------------ % 134.08/19.30 % (3061417)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3716841116:i=3512:aac=none_2985 on theBenchmark for (2985ds/3512Mi) % 134.08/19.30 % (3061405)Instruction limit reached! % 134.08/19.30 % (3061405)------------------------------ % 134.08/19.30 % (3061405)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 134.08/19.30 % (3061405)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 134.08/19.30 % (3061405)CaDiCaL version: 2.1.3 % 134.08/19.30 % (3061405)Termination reason: Instruction limit % 134.08/19.30 % (3061405)Termination phase: Saturation % 134.08/19.30 % (3061405)Time elapsed: 0.711 s % 134.08/19.30 % (3061405)Peak memory usage: 27 MB % 134.08/19.30 % (3061405)Instructions burned: 1474 (million) % 134.08/19.30 % (3061419)dis+21_1_sil=32000:sas=cadical:random_seed=859728810:i=3773:amm=off_2984 on theBenchmark for (2984ds/3773Mi) % 134.08/19.30 % (3061411)Instruction limit reached! % 134.08/19.30 % (3061411)------------------------------ % 134.08/19.30 % (3061411)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 134.08/19.30 % (3061411)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 134.08/19.30 % (3061411)CaDiCaL version: 2.1.3 % 134.08/19.30 % (3061411)Termination reason: Instruction limit % 134.08/19.30 % (3061411)Termination phase: Saturation % 134.08/19.30 % (3061411)Time elapsed: 0.766 s % 134.08/19.30 % (3061411)Peak memory usage: 18 MB % 134.08/19.30 % (3061411)Instructions burned: 870 (million) % 134.08/19.30 % (3061421)ott+11_1_sil=16000:gs=on:random_seed=385070405:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2982 on theBenchmark for (2982ds/2251Mi) % 134.08/19.30 % (3061419)Instruction limit reached! % 134.08/19.30 % (3061419)------------------------------ % 134.08/19.30 % (3061419)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 134.08/19.30 % (3061419)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 134.08/19.30 % (3061419)CaDiCaL version: 2.1.3 % 134.08/19.30 % (3061419)Termination reason: Instruction limit % 134.08/19.30 % (3061419)Termination phase: Saturation % 134.08/19.30 % (3061419)Time elapsed: 1.854 s % 134.08/19.30 % (3061419)Peak memory usage: 31 MB % 134.08/19.30 % (3061419)Instructions burned: 3774 (million) % 134.08/19.30 % (3061423)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=461784979:fmbsr=1.6:i=67534_2966 on theBenchmark for (2966ds/67534Mi) % 134.08/19.30 % (3061423)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 134.08/19.30 % (3061423)Terminated due to inappropriate strategy. % 134.08/19.30 % (3061423)------------------------------ % 134.08/19.30 % (3061423)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 134.08/19.30 % (3061423)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 134.08/19.30 % (3061423)CaDiCaL version: 2.1.3 % 134.08/19.30 % (3061423)Termination reason: Inappropriate % 134.08/19.30 % (3061423)Time elapsed: 0.042 s % 134.08/19.30 % (3061423)Peak memory usage: 12 MB % 134.08/19.30 % (3061423)Instructions burned: 78 (million) % 134.08/19.30 % (3061423)------------------------------ % 134.08/19.30 % (3061423)------------------------------ % 134.08/19.30 % (3061425)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3613163569:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2965 on theBenchmark for (2965ds/4591Mi) % 134.08/19.30 % (3061421)Instruction limit reached! % 134.08/19.30 % (3061421)------------------------------ % 134.08/19.30 % (3061421)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 134.08/19.30 % (3061421)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 134.08/19.30 % (3061421)CaDiCaL version: 2.1.3 % 134.08/19.30 % (3061421)Termination reason: Instruction limit % 134.08/19.30 % (3061421)Termination phase: Saturation % 134.08/19.30 % (3061421)Time elapsed: 2.229 s % 134.08/19.30 % (3061421)Peak memory usage: 25 MB % 134.08/19.30 % (3061421)Instructions burned: 2252 (million) % 134.08/19.30 % (3061427)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3818020987:i=29340_2959 on theBenchmark for (2959ds/29340Mi) % 134.08/19.30 % (3061417)Instruction limit reached! % 134.08/19.30 % (3061417)------------------------------ % 134.08/19.30 % (3061417)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 134.08/19.30 % (3061417)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 134.08/19.30 % (3061417)CaDiCaL version: 2.1.3 % 134.08/19.30 % (3061417)Termination reason: Instruction limit % 154.17/22.05 % (3061417)Termination phase: Saturation % 154.17/22.05 % (3061417)Time elapsed: 3.117 s % 154.17/22.05 % (3061417)Peak memory usage: 31 MB % 154.17/22.05 % (3061417)Instructions burned: 3513 (million) % 154.17/22.05 % (3061429)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=1948856993:i=5211_2954 on theBenchmark for (2954ds/5211Mi) % 154.17/22.05 % (3061413)Instruction limit reached! % 154.17/22.05 % (3061413)------------------------------ % 154.17/22.05 % (3061413)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 154.17/22.05 % (3061413)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 154.17/22.05 % (3061413)CaDiCaL version: 2.1.3 % 154.17/22.05 % (3061413)Termination reason: Instruction limit % 154.17/22.05 % (3061413)Termination phase: Saturation % 154.17/22.05 % (3061413)Time elapsed: 3.954 s % 154.17/22.05 % (3061413)Peak memory usage: 22 MB % 154.17/22.05 % (3061413)Instructions burned: 5114 (million) % 154.17/22.05 % (3061431)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=707446000:i=5497:nm=2_2949 on theBenchmark for (2949ds/5497Mi) % 154.17/22.05 % (3061431)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 154.17/22.05 % (3061431)Terminated due to inappropriate strategy. % 154.17/22.05 % (3061431)------------------------------ % 154.17/22.05 % (3061431)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 154.17/22.05 % (3061431)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 154.17/22.05 % (3061431)CaDiCaL version: 2.1.3 % 154.17/22.05 % (3061431)Termination reason: Inappropriate % 154.17/22.05 % (3061431)Time elapsed: 0.070 s % 154.17/22.05 % (3061431)Peak memory usage: 13 MB % 154.17/22.05 % (3061431)Instructions burned: 83 (million) % 154.17/22.05 % (3061431)------------------------------ % 154.17/22.05 % (3061431)------------------------------ % 154.17/22.05 % (3061433)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1633873607:fmbsr=2:i=46332_2948 on theBenchmark for (2948ds/46332Mi) % 154.17/22.05 % (3061433)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 154.17/22.05 % (3061433)Terminated due to inappropriate strategy. % 154.17/22.05 % (3061433)------------------------------ % 154.17/22.05 % (3061433)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 154.17/22.05 % (3061433)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 154.17/22.05 % (3061433)CaDiCaL version: 2.1.3 % 154.17/22.05 % (3061433)Termination reason: Inappropriate % 154.17/22.05 % (3061433)Time elapsed: 0.044 s % 154.17/22.05 % (3061433)Peak memory usage: 12 MB % 154.17/22.05 % (3061433)Instructions burned: 78 (million) % 154.17/22.05 % (3061433)------------------------------ % 154.17/22.05 % (3061433)------------------------------ % 154.17/22.05 % (3061435)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=818952619:i=14071_2947 on theBenchmark for (2947ds/14071Mi) % 154.17/22.05 % (3061435)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 154.17/22.05 % (3061435)Terminated due to inappropriate strategy. % 154.17/22.05 % (3061435)------------------------------ % 154.17/22.05 % (3061435)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 154.17/22.05 % (3061435)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 154.17/22.05 % (3061435)CaDiCaL version: 2.1.3 % 154.17/22.05 % (3061435)Termination reason: Inappropriate % 154.17/22.05 % (3061435)Time elapsed: 0.041 s % 154.17/22.05 % (3061435)Peak memory usage: 12 MB % 154.17/22.05 % (3061435)Instructions burned: 78 (million) % 154.17/22.05 % (3061435)------------------------------ % 154.17/22.05 % (3061435)------------------------------ % 154.17/22.05 % (3061403)Instruction limit reached! % 154.17/22.05 % (3061403)------------------------------ % 154.17/22.05 % (3061403)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 154.17/22.05 % (3061403)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 154.17/22.05 % (3061403)CaDiCaL version: 2.1.3 % 154.17/22.05 % (3061403)Termination reason: Instruction limit % 154.17/22.05 % (3061403)Termination phase: Saturation % 154.17/22.05 % (3061403)Time elapsed: 4.524 s % 154.17/22.05 % (3061403)Peak memory usage: 45 MB % 154.17/22.05 % (3061403)Instructions burned: 5132 (million) % 154.17/22.05 % (3061437)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=269858391:i=22565:add=on:rawr=on_2947 on theBenchmark for (2947ds/22565Mi) % 154.17/22.05 % (3061438)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=755952874:i=8173:av=off_2946 on theBenchmark for (2946ds/8173Mi) % 154.17/22.05 % (3061425)Instruction limit reached! % 156.73/22.49 % (3061425)------------------------------ % 156.73/22.49 % (3061425)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 156.73/22.49 % (3061425)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 156.73/22.49 % (3061425)CaDiCaL version: 2.1.3 % 156.73/22.49 % (3061425)Termination reason: Instruction limit % 156.73/22.49 % (3061425)Termination phase: Saturation % 156.73/22.49 % (3061425)Time elapsed: 2.480 s % 156.73/22.49 % (3061425)Peak memory usage: 46 MB % 156.73/22.49 % (3061425)Instructions burned: 4591 (million) % 156.73/22.49 % (3061441)dis+10_16:1_sil=16000:random_seed=704161560:i=9155:fsr=off_2940 on theBenchmark for (2940ds/9155Mi) % 156.73/22.49 % (3061429)Instruction limit reached! % 156.73/22.49 % (3061429)------------------------------ % 156.73/22.49 % (3061429)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 156.73/22.49 % (3061429)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 156.73/22.49 % (3061429)CaDiCaL version: 2.1.3 % 156.73/22.49 % (3061429)Termination reason: Instruction limit % 156.73/22.49 % (3061429)Termination phase: Saturation % 156.73/22.49 % (3061429)Time elapsed: 4.548 s % 156.73/22.49 % (3061429)Peak memory usage: 52 MB % 156.73/22.49 % (3061429)Instructions burned: 5212 (million) % 156.73/22.49 % (3061445)ott-3_8_sil=64000:random_seed=1580120614:i=20139:bs=on_2908 on theBenchmark for (2908ds/20139Mi) % 156.73/22.49 % (3061441)Instruction limit reached! % 156.73/22.49 % (3061441)------------------------------ % 156.73/22.49 % (3061441)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 156.73/22.49 % (3061441)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 156.73/22.49 % (3061441)CaDiCaL version: 2.1.3 % 156.73/22.49 % (3061441)Termination reason: Instruction limit % 156.73/22.49 % (3061441)Termination phase: Saturation % 156.73/22.49 % (3061441)Time elapsed: 4.303 s % 156.73/22.49 % (3061441)Peak memory usage: 53 MB % 156.73/22.49 % (3061441)Instructions burned: 9156 (million) % 156.73/22.49 % (3061453)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=3654469907:fmbsr=2:i=32576_2897 on theBenchmark for (2897ds/32576Mi) % 156.73/22.49 % (3061453)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 156.73/22.49 % (3061453)Terminated due to inappropriate strategy. % 156.73/22.49 % (3061453)------------------------------ % 156.73/22.49 % (3061453)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 156.73/22.49 % (3061453)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 156.73/22.49 % (3061453)CaDiCaL version: 2.1.3 % 156.73/22.49 % (3061453)Termination reason: Inappropriate % 156.73/22.49 % (3061453)Time elapsed: 0.041 s % 156.73/22.49 % (3061453)Peak memory usage: 13 MB % 156.73/22.49 % (3061453)Instructions burned: 91 (million) % 156.73/22.49 % (3061453)------------------------------ % 156.73/22.49 % (3061453)------------------------------ % 156.73/22.49 % (3061455)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=1969347724:i=11404_2896 on theBenchmark for (2896ds/11404Mi) % 156.73/22.49 % (3061438)Instruction limit reached! % 156.73/22.49 % (3061438)------------------------------ % 156.73/22.49 % (3061438)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 156.73/22.49 % (3061438)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 156.73/22.49 % (3061438)CaDiCaL version: 2.1.3 % 156.73/22.49 % (3061438)Termination reason: Instruction limit % 156.73/22.49 % (3061438)Termination phase: Saturation % 156.73/22.49 % (3061438)Time elapsed: 7.721 s % 156.73/22.49 % (3061438)Peak memory usage: 60 MB % 156.73/22.49 % (3061438)Instructions burned: 8173 (million) % 156.73/22.49 % (3061464)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=3205835747:i=14134_2869 on theBenchmark for (2869ds/14134Mi) % 156.73/22.49 % (3061455)Instruction limit reached! % 156.73/22.49 % (3061455)------------------------------ % 156.73/22.49 % (3061455)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 156.73/22.49 % (3061455)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 156.73/22.49 % (3061455)CaDiCaL version: 2.1.3 % 156.73/22.49 % (3061455)Termination reason: Instruction limit % 156.73/22.49 % (3061455)Termination phase: Saturation % 156.73/22.49 % (3061455)Time elapsed: 8.074 s % 156.73/22.49 % (3061455)Peak memory usage: 65 MB % 156.73/22.49 % (3061455)Instructions burned: 11405 (million) % 156.73/22.49 % (3061619)dis+33_16_sil=32000:sac=on:random_seed=3057728359:i=15851:nm=0_2815 on theBenchmark for (2815ds/15851Mi) % 156.73/22.49 % (3061437)Instruction limit reached! % 156.73/22.49 % (3061437)------------------------------ % 156.73/22.49 % (3061437)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 201.37/28.79 % (3061437)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 201.37/28.79 % (3061437)CaDiCaL version: 2.1.3 % 201.37/28.79 % (3061437)Termination reason: Instruction limit % 201.37/28.79 % (3061437)Termination phase: Saturation % 201.37/28.79 % (3061437)Time elapsed: 13.681 s % 201.37/28.79 % (3061437)Peak memory usage: 289 MB % 201.37/28.79 % (3061437)Instructions burned: 22566 (million) % 201.37/28.79 % (3061622)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=4137095325:avsq=on:i=17627:add=on:amm=off_2809 on theBenchmark for (2809ds/17627Mi) % 201.37/28.79 % (3061445)Instruction limit reached! % 201.37/28.79 % (3061445)------------------------------ % 201.37/28.79 % (3061445)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 201.37/28.79 % (3061445)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 201.37/28.79 % (3061445)CaDiCaL version: 2.1.3 % 201.37/28.79 % (3061445)Termination reason: Instruction limit % 201.37/28.79 % (3061445)Termination phase: Saturation % 201.37/28.79 % (3061445)Time elapsed: 10.923 s % 201.37/28.79 % (3061445)Peak memory usage: 62 MB % 201.37/28.79 % (3061445)Instructions burned: 20139 (million) % 201.37/28.79 % (3061624)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=1019925918:s2a=on:i=53295_2799 on theBenchmark for (2799ds/53295Mi) % 201.37/28.79 % (3061427)Instruction limit reached! % 201.37/28.79 % (3061427)------------------------------ % 201.37/28.79 % (3061427)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 201.37/28.79 % (3061427)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 201.37/28.79 % (3061427)CaDiCaL version: 2.1.3 % 201.37/28.79 % (3061427)Termination reason: Instruction limit % 201.37/28.79 % (3061427)Termination phase: Saturation % 201.37/28.79 % (3061427)Time elapsed: 17.087 s % 201.37/28.79 % (3061427)Peak memory usage: 50 MB % 201.37/28.79 % (3061427)Instructions burned: 29341 (million) % 201.37/28.79 % (3061626)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=1478848020:i=26857:ins=20_2788 on theBenchmark for (2788ds/26857Mi) % 201.37/28.79 % (3061626)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 201.37/28.79 % (3061626)Terminated due to inappropriate strategy. % 201.37/28.79 % (3061626)------------------------------ % 201.37/28.79 % (3061626)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 201.37/28.79 % (3061626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 201.37/28.79 % (3061626)CaDiCaL version: 2.1.3 % 201.37/28.79 % (3061626)Termination reason: Inappropriate % 201.37/28.79 % (3061626)Time elapsed: 0.034 s % 201.37/28.79 % (3061626)Peak memory usage: 12 MB % 201.37/28.79 % (3061626)Instructions burned: 77 (million) % 201.37/28.79 % (3061626)------------------------------ % 201.37/28.79 % (3061626)------------------------------ % 201.37/28.79 % (3061628)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=3687625525:i=28120:bs=on:fsr=off_2787 on theBenchmark for (2787ds/28120Mi) % 201.37/28.79 % (3061464)Instruction limit reached! % 201.37/28.79 % (3061464)------------------------------ % 201.37/28.79 % (3061464)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 201.37/28.79 % (3061464)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 201.37/28.79 % (3061464)CaDiCaL version: 2.1.3 % 201.37/28.79 % (3061464)Termination reason: Instruction limit % 201.37/28.79 % (3061464)Termination phase: Saturation % 201.37/28.79 % (3061464)Time elapsed: 8.580 s % 201.37/28.79 % (3061464)Peak memory usage: 72 MB % 201.37/28.79 % (3061464)Instructions burned: 14135 (million) % 201.37/28.79 % (3061630)fmb+10_1_sil=256000:fmbss=7:random_seed=2040276271:fmbsr=1.6:i=182295_2783 on theBenchmark for (2783ds/182295Mi) % 201.37/28.79 % (3061630)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 201.37/28.79 % (3061630)Terminated due to inappropriate strategy. % 201.37/28.79 % (3061630)------------------------------ % 201.37/28.79 % (3061630)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 201.37/28.79 % (3061630)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 201.37/28.79 % (3061630)CaDiCaL version: 2.1.3 % 201.37/28.79 % (3061630)Termination reason: Inappropriate % 201.37/28.79 % (3061630)Time elapsed: 0.034 s % 201.37/28.79 % (3061630)Peak memory usage: 12 MB % 201.37/28.79 % (3061630)Instructions burned: 77 (million) % 201.37/28.79 % (3061630)------------------------------ % 201.37/28.79 % (3061630)------------------------------ % 201.37/28.79 % (3061632)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=2149086042:i=44625:gsp=on_2782 on theBenchmark for (2782ds/44625Mi) % 214.98/30.64 % (3061632)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 214.98/30.64 % (3061632)Terminated due to inappropriate strategy. % 214.98/30.64 % (3061632)------------------------------ % 214.98/30.64 % (3061632)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 214.98/30.64 % (3061632)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 214.98/30.64 % (3061632)CaDiCaL version: 2.1.3 % 214.98/30.64 % (3061632)Termination reason: Inappropriate % 214.98/30.64 % (3061632)Time elapsed: 0.186 s % 214.98/30.64 % (3061632)Peak memory usage: 14 MB % 214.98/30.64 % (3061632)Instructions burned: 465 (million) % 214.98/30.64 % (3061632)------------------------------ % 214.98/30.64 % (3061632)------------------------------ % 214.98/30.64 % (3061634)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=945586934:i=160505_2780 on theBenchmark for (2780ds/160505Mi) % 214.98/30.64 % (3061634)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 214.98/30.64 % (3061634)Terminated due to inappropriate strategy. % 214.98/30.64 % (3061634)------------------------------ % 214.98/30.64 % (3061634)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 214.98/30.64 % (3061634)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 214.98/30.64 % (3061634)CaDiCaL version: 2.1.3 % 214.98/30.64 % (3061634)Termination reason: Inappropriate % 214.98/30.64 % (3061634)Time elapsed: 0.034 s % 214.98/30.64 % (3061634)Peak memory usage: 12 MB % 214.98/30.64 % (3061634)Instructions burned: 77 (million) % 214.98/30.64 % (3061634)------------------------------ % 214.98/30.64 % (3061634)------------------------------ % 214.98/30.64 % (3061636)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=3522603510:fmbsr=1.3:i=225729_2780 on theBenchmark for (2780ds/225729Mi) % 214.98/30.64 % (3061636)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 214.98/30.64 % (3061636)Terminated due to inappropriate strategy. % 214.98/30.64 % (3061636)------------------------------ % 214.98/30.64 % (3061636)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 214.98/30.64 % (3061636)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 214.98/30.64 % (3061636)CaDiCaL version: 2.1.3 % 214.98/30.64 % (3061636)Termination reason: Inappropriate % 214.98/30.64 % (3061636)Time elapsed: 0.034 s % 214.98/30.64 % (3061636)Peak memory usage: 12 MB % 214.98/30.64 % (3061636)Instructions burned: 78 (million) % 214.98/30.64 % (3061636)------------------------------ % 214.98/30.64 % (3061636)------------------------------ % 214.98/30.64 % (3061638)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=3565351061:fmbsr=2:i=185024:ins=7_2779 on theBenchmark for (2779ds/185024Mi) % 214.98/30.64 % (3061638)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 214.98/30.64 % (3061638)Terminated due to inappropriate strategy. % 214.98/30.64 % (3061638)------------------------------ % 214.98/30.64 % (3061638)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 214.98/30.64 % (3061638)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 214.98/30.64 % (3061638)CaDiCaL version: 2.1.3 % 214.98/30.64 % (3061638)Termination reason: Inappropriate % 214.98/30.64 % (3061638)Time elapsed: 0.034 s % 214.98/30.64 % (3061638)Peak memory usage: 12 MB % 214.98/30.64 % (3061638)Instructions burned: 78 (million) % 214.98/30.64 % (3061638)------------------------------ % 214.98/30.64 % (3061638)------------------------------ % 214.98/30.64 % (3061640)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=1225589147:rtra=on_2778 on theBenchmark for (2778ds/0Mi) % 214.98/30.64 % (3061640)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 214.98/30.64 % (3061640)Terminated due to inappropriate strategy. % 214.98/30.64 % (3061640)------------------------------ % 214.98/30.64 % (3061640)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 214.98/30.64 % (3061640)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 214.98/30.64 % (3061640)CaDiCaL version: 2.1.3 % 214.98/30.64 % (3061640)Termination reason: Inappropriate % 214.98/30.64 % (3061640)Time elapsed: 0.043 s % 214.98/30.64 % (3061640)Peak memory usage: 12 MB % 214.98/30.64 % (3061640)Instructions burned: 93 (million) % 214.98/30.64 % (3061640)------------------------------ % 214.98/30.64 % (3061640)------------------------------ % 214.98/30.64 % (3061642)% WARNING: option uhcvi not known. % 214.98/30.64 % (3061642)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1075241872:i=271062:add=off:rtra=on:rawr=on_2778 on theBenchmark for (2778ds/271062Mi) % 237.71/33.87 % (3061619)Instruction limit reached! % 237.71/33.87 % (3061619)------------------------------ % 237.71/33.87 % (3061619)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 237.71/33.87 % (3061619)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 237.71/33.87 % (3061619)CaDiCaL version: 2.1.3 % 237.71/33.87 % (3061619)Termination reason: Instruction limit % 237.71/33.87 % (3061619)Termination phase: Saturation % 237.71/33.87 % (3061619)Time elapsed: 6.897 s % 237.71/33.87 % (3061619)Peak memory usage: 25 MB % 237.71/33.87 % (3061619)Instructions burned: 15853 (million) % 237.71/33.87 % (3061644)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2872085209:i=176048:add=on:rtra=on:rawr=on_2746 on theBenchmark for (2746ds/176048Mi) % 237.71/33.87 % (3061622)Instruction limit reached! % 237.71/33.87 % (3061622)------------------------------ % 237.71/33.87 % (3061622)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 237.71/33.87 % (3061622)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 237.71/33.87 % (3061622)CaDiCaL version: 2.1.3 % 237.71/33.87 % (3061622)Termination reason: Instruction limit % 237.71/33.87 % (3061622)Termination phase: Saturation % 237.71/33.87 % (3061622)Time elapsed: 8.727 s % 237.71/33.87 % (3061622)Peak memory usage: 193 MB % 237.71/33.87 % (3061622)Instructions burned: 17627 (million) % 237.71/33.87 % (3061646)dis+10_1_sil=32000:si=on:sp=arity:random_seed=1039700333:i=206:fgj=on:rtra=on_2721 on theBenchmark for (2721ds/206Mi) % 237.71/33.87 % (3061646)Instruction limit reached! % 237.71/33.87 % (3061646)------------------------------ % 237.71/33.87 % (3061646)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 237.71/33.87 % (3061646)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 237.71/33.87 % (3061646)CaDiCaL version: 2.1.3 % 237.71/33.87 % (3061646)Termination reason: Instruction limit % 237.71/33.87 % (3061646)Termination phase: Saturation % 237.71/33.87 % (3061646)Time elapsed: 0.117 s % 237.71/33.87 % (3061646)Peak memory usage: 14 MB % 237.71/33.87 % (3061646)Instructions burned: 207 (million) % 237.71/33.87 % (3061648)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=3611141055:i=232:rtra=on_2720 on theBenchmark for (2720ds/232Mi) % 237.71/33.87 % (3061648)Instruction limit reached! % 237.71/33.87 % (3061648)------------------------------ % 237.71/33.87 % (3061648)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 237.71/33.87 % (3061648)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 237.71/33.87 % (3061648)CaDiCaL version: 2.1.3 % 237.71/33.87 % (3061648)Termination reason: Instruction limit % 237.71/33.87 % (3061648)Termination phase: Property scanning % 237.71/33.87 % (3061648)Time elapsed: 0.109 s % 237.71/33.87 % (3061648)Peak memory usage: 14 MB % 237.71/33.87 % (3061648)Instructions burned: 233 (million) % 237.71/33.87 % (3061650)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=2040705319:i=262:rtra=on_2719 on theBenchmark for (2719ds/262Mi) % 237.71/33.87 % (3061650)Instruction limit reached! % 237.71/33.87 % (3061650)------------------------------ % 237.71/33.87 % (3061650)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 237.71/33.87 % (3061650)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 237.71/33.87 % (3061650)CaDiCaL version: 2.1.3 % 237.71/33.87 % (3061650)Termination reason: Instruction limit % 237.71/33.87 % (3061650)Termination phase: Saturation % 237.71/33.87 % (3061650)Time elapsed: 0.153 s % 237.71/33.87 % (3061650)Peak memory usage: 15 MB % 237.71/33.87 % (3061650)Instructions burned: 263 (million) % 237.71/33.87 % (3061652)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=3813177583:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2717 on theBenchmark for (2717ds/318Mi) % 237.71/33.87 % (3061652)Instruction limit reached! % 237.71/33.87 % (3061652)------------------------------ % 237.71/33.87 % (3061652)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 237.71/33.87 % (3061652)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 237.71/33.87 % (3061652)CaDiCaL version: 2.1.3 % 237.71/33.87 % (3061652)Termination reason: Instruction limit % 237.71/33.87 % (3061652)Termination phase: Saturation % 237.71/33.87 % (3061652)Time elapsed: 0.189 s % 237.71/33.87 % (3061652)Peak memory usage: 15 MB % 237.71/33.87 % (3061652)Instructions burned: 319 (million) % 237.71/33.87 % (3061654)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=2360476677:i=1428:nm=2:rtra=on_2715 on theBenchmark for (2715ds/1428Mi) % 273.13/38.86 % (3061654)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 273.13/38.86 % (3061654)Terminated due to inappropriate strategy. % 273.13/38.86 % (3061654)------------------------------ % 273.13/38.86 % (3061654)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 273.13/38.86 % (3061654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 273.13/38.86 % (3061654)CaDiCaL version: 2.1.3 % 273.13/38.86 % (3061654)Termination reason: Inappropriate % 273.13/38.86 % (3061654)Time elapsed: 0.034 s % 273.13/38.86 % (3061654)Peak memory usage: 12 MB % 273.13/38.86 % (3061654)Instructions burned: 72 (million) % 273.13/38.86 % (3061654)------------------------------ % 273.13/38.86 % (3061654)------------------------------ % 273.13/38.86 % (3061656)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=2018067904:i=262:bd=preordered:rtra=on:fsd=on_2714 on theBenchmark for (2714ds/262Mi) % 273.13/38.86 % (3061656)Instruction limit reached! % 273.13/38.86 % (3061656)------------------------------ % 273.13/38.86 % (3061656)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 273.13/38.86 % (3061656)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 273.13/38.86 % (3061656)CaDiCaL version: 2.1.3 % 273.13/38.86 % (3061656)Termination reason: Instruction limit % 273.13/38.86 % (3061656)Termination phase: Saturation % 273.13/38.86 % (3061656)Time elapsed: 0.152 s % 273.13/38.86 % (3061656)Peak memory usage: 15 MB % 273.13/38.86 % (3061656)Instructions burned: 263 (million) % 273.13/38.86 % (3061658)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=76056447:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2713 on theBenchmark for (2713ds/1368Mi) % 273.13/38.86 % (3061658)Instruction limit reached! % 273.13/38.86 % (3061658)------------------------------ % 273.13/38.86 % (3061658)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 273.13/38.86 % (3061658)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 273.13/38.86 % (3061658)CaDiCaL version: 2.1.3 % 273.13/38.86 % (3061658)Termination reason: Instruction limit % 273.13/38.86 % (3061658)Termination phase: Saturation % 273.13/38.86 % (3061658)Time elapsed: 0.712 s % 273.13/38.86 % (3061658)Peak memory usage: 20 MB % 273.13/38.86 % (3061658)Instructions burned: 1369 (million) % 273.13/38.86 % (3061867)ott-21_1_sil=16000:si=on:fs=off:random_seed=1640852326:i=360:av=off:fsr=off:rtra=on_2705 on theBenchmark for (2705ds/360Mi) % 273.13/38.86 % (3061867)Instruction limit reached! % 273.13/38.86 % (3061867)------------------------------ % 273.13/38.86 % (3061867)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 273.13/38.86 % (3061867)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 273.13/38.86 % (3061867)CaDiCaL version: 2.1.3 % 273.13/38.86 % (3061867)Termination reason: Instruction limit % 273.13/38.86 % (3061867)Termination phase: Saturation % 273.13/38.86 % (3061867)Time elapsed: 0.180 s % 273.13/38.86 % (3061867)Peak memory usage: 14 MB % 273.13/38.86 % (3061867)Instructions burned: 361 (million) % 273.13/38.86 % (3061936)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=707427194:i=954:bd=all:rtra=on_2703 on theBenchmark for (2703ds/954Mi) % 273.13/38.86 % (3061936)Instruction limit reached! % 273.13/38.86 % (3061936)------------------------------ % 273.13/38.86 % (3061936)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 273.13/38.86 % (3061936)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 273.13/38.86 % (3061936)CaDiCaL version: 2.1.3 % 273.13/38.86 % (3061936)Termination reason: Instruction limit % 273.13/38.86 % (3061936)Termination phase: Saturation % 273.13/38.86 % (3061936)Time elapsed: 0.627 s % 273.13/38.86 % (3061936)Peak memory usage: 19 MB % 273.13/38.86 % (3061936)Instructions burned: 954 (million) % 273.13/38.86 % (3062023)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=1864716299:fmbsr=1.3:i=1730:ins=25:rtra=on_2697 on theBenchmark for (2697ds/1730Mi) % 273.13/38.86 % (3062023)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 273.13/38.86 % (3062023)Terminated due to inappropriate strategy. % 273.13/38.86 % (3062023)------------------------------ % 273.13/38.86 % (3062023)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 273.13/38.86 % (3062023)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 273.13/38.86 % (3062023)CaDiCaL version: 2.1.3 % 273.13/38.86 % (3062023)Termination reason: Inappropriate % 300.16/42.64 % (3062023)Time elapsed: 0.037 s % 300.16/42.64 % (3062023)Peak memory usage: 12 MB % 300.16/42.64 % (3062023)Instructions burned: 80 (million) % 300.16/42.64 % (3062023)------------------------------ % 300.16/42.64 % (3062023)------------------------------ % 300.16/42.64 % (3062025)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=3507650415:i=2358:rtra=on_2696 on theBenchmark for (2696ds/2358Mi) % 300.16/42.64 % (3062025)Instruction limit reached! % 300.16/42.64 % (3062025)------------------------------ % 300.16/42.64 % (3062025)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.16/42.64 % (3062025)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.16/42.64 % (3062025)CaDiCaL version: 2.1.3 % 300.16/42.64 % (3062025)Termination reason: Instruction limit % 300.16/42.64 % (3062025)Termination phase: Saturation % 300.16/42.64 % (3062025)Time elapsed: 1.394 s % 300.16/42.64 % (3062025)Peak memory usage: 33 MB % 300.16/42.64 % (3062025)Instructions burned: 2359 (million) % 300.16/42.64 % (3062027)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=2432349251:i=1778:ins=1:rtra=on_2682 on theBenchmark for (2682ds/1778Mi) % 300.16/42.64 % (3062027)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.16/42.64 % (3062027)Terminated due to inappropriate strategy. % 300.16/42.64 % (3062027)------------------------------ % 300.16/42.64 % (3062027)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.16/42.64 % (3062027)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.16/42.64 % (3062027)CaDiCaL version: 2.1.3 % 300.16/42.64 % (3062027)Termination reason: Inappropriate % 300.16/42.64 % (3062027)Time elapsed: 0.036 s % 300.16/42.64 % (3062027)Peak memory usage: 12 MB % 300.16/42.64 % (3062027)Instructions burned: 80 (million) % 300.16/42.64 % (3062027)------------------------------ % 300.16/42.64 % (3062027)------------------------------ % 300.16/42.64 % (3062029)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=1126236347:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2681 on theBenchmark for (2681ds/1384Mi) % 300.16/42.64 % (3062029)Instruction limit reached! % 300.16/42.64 % (3062029)------------------------------ % 300.16/42.64 % (3062029)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.16/42.64 % (3062029)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.16/42.64 % (3062029)CaDiCaL version: 2.1.3 % 300.16/42.64 % (3062029)Termination reason: Instruction limit % 300.16/42.64 % (3062029)Termination phase: Saturation % 300.16/42.64 % (3062029)Time elapsed: 0.790 s % 300.16/42.64 % (3062029)Peak memory usage: 23 MB % 300.16/42.64 % (3062029)Instructions burned: 1385 (million) % 300.16/42.64 % (3062031)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=1283072464:i=1758:kws=inv_precedence:fsr=off:rtra=on_2673 on theBenchmark for (2673ds/1758Mi) % 300.16/42.64 % (3062031)Instruction limit reached! % 300.16/42.64 % (3062031)------------------------------ % 300.16/42.64 % (3062031)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.16/42.64 % (3062031)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.16/42.64 % (3062031)CaDiCaL version: 2.1.3 % 300.16/42.64 % (3062031)Termination reason: Instruction limit % 300.16/42.64 % (3062031)Termination phase: Saturation % 300.16/42.64 % (3062031)Time elapsed: 0.838 s % 300.16/42.64 % (3062031)Peak memory usage: 23 MB % 300.16/42.64 % (3062031)Instructions burned: 1758 (million) % 300.16/42.64 % (3062033)fmb+10_1_sil=64000:si=on:random_seed=2216945211:i=44122:nm=2:rtra=on:gsp=on_2665 on theBenchmark for (2665ds/44122Mi) % 300.16/42.64 % (3062033)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.16/42.64 % (3062033)Terminated due to inappropriate strategy. % 300.16/42.64 % (3062033)------------------------------ % 300.16/42.64 % (3062033)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.16/42.64 % (3062033)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.16/42.64 % (3062033)CaDiCaL version: 2.1.3 % 300.16/42.64 % (3062033)Termination reason: Inappropriate % 300.16/42.64 % (3062033)Time elapsed: 0.036 s % 300.16/42.64 % (3062033)Peak memory usage: 12 MB % 300.16/42.64 % (3062033)Instructions burned: 77 (million) % 300.16/42.64 % (3062033)------------------------------ % 300.16/42.64 % (3062033)------------------------------ % 300.16/42.64 % (3062035)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=3273765627:i=19030:nm=5:rtra=on_2664 on theBenchmark for (2664ds/19030Mi) % 300.16/42.64 % (3062035)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.16/42.64 % (3062035)Terminated due to inappropriate strategy. % 300.16/42.64 % (3062035)------------------------------ % 300.16/42.64 % (3062035)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.16/42.64 % (3062035)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.16/42.64 % (3062035)CaDiCaL version: 2.1.3 % 300.16/42.64 % (3062035)Termination reason: Inappropriate % 300.16/42.64 % (3062035)Time elapsed: 0.036 s % 300.16/42.64 % (3062035)Peak memory usage: 12 MB % 300.16/42.64 % (3062035)Instructions burned: 78 (million) % 300.16/42.64 % (3062035)------------------------------ % 300.16/42.64 % (3062035)------------------------------ % 300.16/42.64 % (3062037)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=3082492919:fmbsr=1.7:i=1840:rtra=on_2663 on theBenchmark for (2663ds/1840Mi) % 300.16/42.64 % (3062037)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.16/42.64 % (3062037)Terminated due to inappropriate strategy. % 300.16/42.64 % (3062037)------------------------------ % 300.16/42.64 % (3062037)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.16/42.64 % (3062037)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.16/42.64 % (3062037)CaDiCaL version: 2.1.3 % 300.16/42.64 % (3062037)Termination reason: Inappropriate % 300.16/42.64 % (3062037)Time elapsed: 0.036 s % 300.16/42.64 % (3062037)Peak memory usage: 12 MB % 300.16/42.64 % (3062037)Instructions burned: 80 (million) % 300.16/42.64 % (3062037)------------------------------ % 300.16/42.64 % (3062037)------------------------------ % 300.16/42.64 % (3062039)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=1674675056:i=10262:rtra=on_2663 on theBenchmark for (2663ds/10262Mi) % 300.16/42.64 % (3061628)Instruction limit reached! % 300.16/42.64 % (3061628)------------------------------ % 300.16/42.64 % (3061628)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.16/42.64 % (3061628)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.16/42.64 % (3061628)CaDiCaL version: 2.1.3 % 300.16/42.64 % (3061628)Termination reason: Instruction limit % 300.16/42.64 % (3061628)Termination phase: Saturation % 300.16/42.64 % (3061628)Time elapsed: 15.696 s % 300.16/42.64 % (3061628)Peak memory usage: 51 MB % 300.16/42.64 % (3061628)Instructions burned: 28121 (million) % 300.16/42.64 % (3062041)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2722984551:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2630 on theBenchmark for (2630ds/2944Mi) % 300.16/42.64 % (3062041)Instruction limit reached! % 300.16/42.64 % (3062041)------------------------------ % 300.16/42.64 % (3062041)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.16/42.64 % (3062041)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.16/42.64 % (3062041)CaDiCaL version: 2.1.3 % 300.16/42.64 % (3062041)Termination reason: Instruction limit % 300.16/42.64 % (3062041)Termination phase: Saturation % 300.16/42.64 % (3062041)Time elapsed: 1.485 s % 300.16/42.64 % (3062041)Peak memory usage: 33 MB % 300.16/42.64 % (3062041)Instructions burned: 2945 (million) % 300.16/42.64 % (3062043)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=3903232453:i=12648:rtra=on_2615 on theBenchmark for (2615ds/12648Mi) % 300.16/42.64 % (3062043)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.16/42.64 % (3062043)Terminated due to inappropriate strategy. % 300.16/42.64 % (3062043)------------------------------ % 300.16/42.64 % (3062043)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.16/42.64 % (3062043)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.16/42.64 % (3062043)CaDiCaL version: 2.1.3 % 300.16/42.64 % (3062043)Termination reason: Inappropriate % 300.16/42.64 % (3062043)Time elapsed: 0.043 s % 300.16/42.64 % (3062043)Peak memory usage: 12 MB % 300.16/42.64 % (3062043)Instructions burned: 92 (million) % 300.16/42.64 % (3062043)------------------------------ % 300.16/42.64 % (3062043)------------------------------ % 300.16/42.64 % (3062045)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=2532208444:fmbsr=2.30978:i=4348:rtra=on_2614 on theBenchmark for (2614ds/4348Mi) % 300.16/42.64 % (3062045)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.16/42.64 % (3062045)Terminated due to inappropriate strategy. % 300.16/42.64 % (3062045)-------------- % 300.16/42.64 Terminated % 300.16/42.64 % Vampire exiting % 300.16/42.64 Terminated %------------------------------------------------------------------------------