%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW086_1 : TPTP v9.3.1. Released v5.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n006.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:39:22 PM UTC 2026 % Result : Timeout 290.36s 41.22s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWW086_1 : TPTP v9.3.1. Released v5.0.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.10/0.24 % Computer : n006.cluster.edu % 0.10/0.24 % Model : x86_64 x86_64 % 0.10/0.24 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.24 % Memory : 8046.5625MB % 0.10/0.24 % OS : Linux 6.8.0-71-generic % 0.10/0.24 % CPULimit : 300 % 0.10/0.24 % WCLimit : 300 % 0.10/0.24 % DateTime : Mon Sep 28 13:11:10 UTC 2026 % 0.10/0.25 % CPUTime : % 0.10/0.25 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.24/0.30 Running first-order model finding % 0.24/0.30 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 % 5.99/1.22 % (3956481)Will run a generic schedule for satisfiability detection. % 5.99/1.22 % (3956491)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=417996411:i=131_2999 on theBenchmark for (2999ds/131Mi) % 5.99/1.22 % (3956487)% WARNING: option uhcvi not known. % 5.99/1.22 % (3956486)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1685771454_2999 on theBenchmark for (2999ds/0Mi) % 5.99/1.22 % (3956490)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3622762841:i=116_2999 on theBenchmark for (2999ds/116Mi) % 5.99/1.22 % (3956487)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3068683280:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 5.99/1.22 % (3956492)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2911506796:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 5.99/1.22 % (3956489)dis+10_1_sil=32000:sp=arity:random_seed=4201283237:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 5.99/1.22 % (3956488)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3088738400:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 5.99/1.22 % (3956491)Instruction limit reached! % 5.99/1.22 % (3956491)------------------------------ % 5.99/1.22 % (3956491)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.99/1.22 % (3956491)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.99/1.22 % (3956491)CaDiCaL version: 2.1.3 % 5.99/1.22 % (3956491)Termination reason: Instruction limit % 5.99/1.22 % (3956491)Termination phase: Saturation % 5.99/1.22 % (3956491)Time elapsed: 0.055 s % 5.99/1.22 % (3956491)Peak memory usage: 15 MB % 5.99/1.22 % (3956491)Instructions burned: 133 (million) % 5.99/1.22 % (3956500)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3754724421:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi) % 5.99/1.22 % (3956486)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 5.99/1.22 % (3956486)Terminated due to inappropriate strategy. % 5.99/1.22 % (3956486)------------------------------ % 5.99/1.22 % (3956486)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.99/1.22 % (3956486)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.99/1.22 % (3956486)CaDiCaL version: 2.1.3 % 5.99/1.22 % (3956486)Termination reason: Inappropriate % 5.99/1.22 % (3956486)Time elapsed: 0.082 s % 5.99/1.22 % (3956486)Peak memory usage: 14 MB % 5.99/1.22 % (3956486)Instructions burned: 99 (million) % 5.99/1.22 % (3956486)------------------------------ % 5.99/1.22 % (3956486)------------------------------ % 5.99/1.22 % (3956489)Instruction limit reached! % 5.99/1.22 % (3956489)------------------------------ % 5.99/1.22 % (3956489)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.99/1.22 % (3956489)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.99/1.22 % (3956489)CaDiCaL version: 2.1.3 % 5.99/1.22 % (3956489)Termination reason: Instruction limit % 5.99/1.22 % (3956489)Termination phase: Saturation % 5.99/1.22 % (3956489)Time elapsed: 0.086 s % 5.99/1.22 % (3956489)Peak memory usage: 15 MB % 5.99/1.22 % (3956489)Instructions burned: 104 (million) % 5.99/1.22 % (3956490)Instruction limit reached! % 5.99/1.22 % (3956490)------------------------------ % 5.99/1.22 % (3956490)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.99/1.22 % (3956490)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.99/1.22 % (3956490)CaDiCaL version: 2.1.3 % 5.99/1.22 % (3956490)Termination reason: Instruction limit % 5.99/1.22 % (3956490)Termination phase: Saturation % 5.99/1.22 % (3956490)Time elapsed: 0.100 s % 5.99/1.22 % (3956490)Peak memory usage: 16 MB % 5.99/1.22 % (3956490)Instructions burned: 116 (million) % 5.99/1.22 % (3956502)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2539210980:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi) % 5.99/1.22 % (3956500)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 5.99/1.22 % (3956500)Terminated due to inappropriate strategy. % 5.99/1.22 % (3956500)------------------------------ % 5.99/1.22 % (3956500)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.99/1.22 % (3956500)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.99/1.22 % (3956500)CaDiCaL version: 2.1.3 % 5.99/1.22 % (3956500)Termination reason: Inappropriate % 5.99/1.22 % (3956500)Time elapsed: 0.045 s % 7.65/1.63 % (3956500)Peak memory usage: 14 MB % 7.65/1.63 % (3956500)Instructions burned: 99 (million) % 7.65/1.63 % (3956500)------------------------------ % 7.65/1.63 % (3956500)------------------------------ % 7.65/1.63 % (3956503)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=3915895007:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 7.65/1.63 % (3956492)Instruction limit reached! % 7.65/1.63 % (3956492)------------------------------ % 7.65/1.63 % (3956492)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.65/1.63 % (3956492)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.65/1.63 % (3956492)CaDiCaL version: 2.1.3 % 7.65/1.63 % (3956492)Termination reason: Instruction limit % 7.65/1.63 % (3956492)Termination phase: Saturation % 7.65/1.63 % (3956492)Time elapsed: 0.123 s % 7.65/1.63 % (3956492)Peak memory usage: 16 MB % 7.65/1.63 % (3956492)Instructions burned: 160 (million) % 7.65/1.63 % (3956504)ott-21_1_sil=16000:fs=off:random_seed=1789948248:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 7.65/1.63 % (3956508)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1723639430:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi) % 7.65/1.63 % (3956506)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=355187313:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi) % 7.65/1.63 % (3956508)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 7.65/1.63 % (3956508)Terminated due to inappropriate strategy. % 7.65/1.63 % (3956508)------------------------------ % 7.65/1.63 % (3956508)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.65/1.63 % (3956508)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.65/1.63 % (3956508)CaDiCaL version: 2.1.3 % 7.65/1.63 % (3956508)Termination reason: Inappropriate % 7.65/1.63 % (3956508)Time elapsed: 0.042 s % 7.65/1.63 % (3956508)Peak memory usage: 14 MB % 7.65/1.63 % (3956508)Instructions burned: 98 (million) % 7.65/1.63 % (3956508)------------------------------ % 7.65/1.63 % (3956508)------------------------------ % 7.65/1.63 % (3956502)Instruction limit reached! % 7.65/1.63 % (3956502)------------------------------ % 7.65/1.63 % (3956502)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.65/1.63 % (3956502)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.65/1.63 % (3956502)CaDiCaL version: 2.1.3 % 7.65/1.63 % (3956502)Termination reason: Instruction limit % 7.65/1.63 % (3956502)Termination phase: Saturation % 7.65/1.63 % (3956502)Time elapsed: 0.087 s % 7.65/1.63 % (3956502)Peak memory usage: 15 MB % 7.65/1.63 % (3956502)Instructions burned: 131 (million) % 7.65/1.63 % (3956512)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2803679540:i=1179_2997 on theBenchmark for (2997ds/1179Mi) % 7.65/1.63 % (3956513)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=544353861:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi) % 7.65/1.63 % (3956504)Instruction limit reached! % 7.65/1.63 % (3956504)------------------------------ % 7.65/1.63 % (3956504)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.65/1.63 % (3956504)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.65/1.63 % (3956504)CaDiCaL version: 2.1.3 % 7.65/1.63 % (3956504)Termination reason: Instruction limit % 7.65/1.63 % (3956504)Termination phase: Saturation % 7.65/1.63 % (3956504)Time elapsed: 0.155 s % 7.65/1.63 % (3956504)Peak memory usage: 15 MB % 7.65/1.63 % (3956504)Instructions burned: 181 (million) % 7.65/1.63 % (3956513)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 7.65/1.63 % (3956513)Terminated due to inappropriate strategy. % 7.65/1.63 % (3956513)------------------------------ % 7.65/1.63 % (3956513)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.65/1.63 % (3956513)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.65/1.63 % (3956513)CaDiCaL version: 2.1.3 % 7.65/1.63 % (3956513)Termination reason: Inappropriate % 7.65/1.63 % (3956513)Time elapsed: 0.095 s % 7.65/1.63 % (3956513)Peak memory usage: 16 MB % 7.65/1.63 % (3956513)Instructions burned: 136 (million) % 7.65/1.63 % (3956513)------------------------------ % 7.65/1.63 % (3956513)------------------------------ % 7.65/1.63 % (3956516)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=3109906948: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) % 29.02/4.53 % (3956517)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=30651055:i=879:kws=inv_precedence:fsr=off_2995 on theBenchmark for (2995ds/879Mi) % 29.02/4.53 % (3956506)Instruction limit reached! % 29.02/4.53 % (3956506)------------------------------ % 29.02/4.53 % (3956506)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 29.02/4.53 % (3956506)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.02/4.53 % (3956506)CaDiCaL version: 2.1.3 % 29.02/4.53 % (3956506)Termination reason: Instruction limit % 29.02/4.53 % (3956506)Termination phase: Saturation % 29.02/4.53 % (3956506)Time elapsed: 0.439 s % 29.02/4.53 % (3956506)Peak memory usage: 17 MB % 29.02/4.53 % (3956506)Instructions burned: 477 (million) % 29.02/4.53 % (3956520)fmb+10_1_sil=64000:random_seed=3122315431:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi) % 29.02/4.53 % (3956503)Instruction limit reached! % 29.02/4.53 % (3956503)------------------------------ % 29.02/4.53 % (3956503)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 29.02/4.53 % (3956503)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.02/4.53 % (3956503)CaDiCaL version: 2.1.3 % 29.02/4.53 % (3956503)Termination reason: Instruction limit % 29.02/4.53 % (3956503)Termination phase: Saturation % 29.02/4.53 % (3956503)Time elapsed: 0.593 s % 29.02/4.53 % (3956503)Peak memory usage: 20 MB % 29.02/4.53 % (3956503)Instructions burned: 684 (million) % 29.02/4.53 % (3956520)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 29.02/4.53 % (3956520)Terminated due to inappropriate strategy. % 29.02/4.53 % (3956520)------------------------------ % 29.02/4.53 % (3956520)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 29.02/4.53 % (3956520)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.02/4.53 % (3956520)CaDiCaL version: 2.1.3 % 29.02/4.53 % (3956520)Termination reason: Inappropriate % 29.02/4.53 % (3956520)Time elapsed: 0.092 s % 29.02/4.53 % (3956520)Peak memory usage: 14 MB % 29.02/4.53 % (3956520)Instructions burned: 109 (million) % 29.02/4.53 % (3956520)------------------------------ % 29.02/4.53 % (3956520)------------------------------ % 29.02/4.53 % (3956512)Instruction limit reached! % 29.02/4.53 % (3956512)------------------------------ % 29.02/4.53 % (3956512)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 29.02/4.53 % (3956512)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.02/4.53 % (3956512)CaDiCaL version: 2.1.3 % 29.02/4.53 % (3956512)Termination reason: Instruction limit % 29.02/4.53 % (3956512)Termination phase: Saturation % 29.02/4.53 % (3956512)Time elapsed: 0.518 s % 29.02/4.53 % (3956512)Peak memory usage: 22 MB % 29.02/4.53 % (3956512)Instructions burned: 1185 (million) % 29.02/4.53 % (3956523)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=4002910255:fmbsr=1.7:i=920_2991 on theBenchmark for (2991ds/920Mi) % 29.02/4.53 % (3956524)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=518269943:i=5131_2991 on theBenchmark for (2991ds/5131Mi) % 29.02/4.53 % (3956522)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3726063786:i=9515:nm=5_2991 on theBenchmark for (2991ds/9515Mi) % 29.02/4.53 % (3956523)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 29.02/4.53 % (3956523)Terminated due to inappropriate strategy. % 29.02/4.53 % (3956523)------------------------------ % 29.02/4.53 % (3956523)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 29.02/4.53 % (3956523)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.02/4.53 % (3956523)CaDiCaL version: 2.1.3 % 29.02/4.53 % (3956523)Termination reason: Inappropriate % 29.02/4.53 % (3956523)Time elapsed: 0.070 s % 29.02/4.53 % (3956523)Peak memory usage: 14 MB % 29.02/4.53 % (3956523)Instructions burned: 99 (million) % 29.02/4.53 % (3956523)------------------------------ % 29.02/4.53 % (3956523)------------------------------ % 29.02/4.53 % (3956522)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 29.02/4.53 % (3956522)Terminated due to inappropriate strategy. % 29.02/4.53 % (3956522)------------------------------ % 29.02/4.53 % (3956522)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 29.02/4.53 % (3956522)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.54/6.26 % (3956522)CaDiCaL version: 2.1.3 % 41.54/6.26 % (3956522)Termination reason: Inappropriate % 41.54/6.26 % (3956522)Time elapsed: 0.081 s % 41.54/6.26 % (3956522)Peak memory usage: 14 MB % 41.54/6.26 % (3956522)Instructions burned: 99 (million) % 41.54/6.26 % (3956522)------------------------------ % 41.54/6.26 % (3956522)------------------------------ % 41.54/6.26 % (3956530)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1369770768:i=1472:ins=7:fdi=8:gsp=on_2990 on theBenchmark for (2990ds/1472Mi) % 41.54/6.26 % (3956531)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1933844999:i=6324_2990 on theBenchmark for (2990ds/6324Mi) % 41.54/6.26 % (3956531)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 41.54/6.26 % (3956531)Terminated due to inappropriate strategy. % 41.54/6.26 % (3956531)------------------------------ % 41.54/6.26 % (3956531)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 41.54/6.26 % (3956531)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.54/6.26 % (3956531)CaDiCaL version: 2.1.3 % 41.54/6.26 % (3956531)Termination reason: Inappropriate % 41.54/6.26 % (3956531)Time elapsed: 0.054 s % 41.54/6.26 % (3956531)Peak memory usage: 14 MB % 41.54/6.26 % (3956531)Instructions burned: 99 (million) % 41.54/6.26 % (3956531)------------------------------ % 41.54/6.26 % (3956531)------------------------------ % 41.54/6.26 % (3956536)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2616465874:fmbsr=2.30978:i=2174_2989 on theBenchmark for (2989ds/2174Mi) % 41.54/6.26 % (3956516)Instruction limit reached! % 41.54/6.26 % (3956516)------------------------------ % 41.54/6.26 % (3956516)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 41.54/6.26 % (3956516)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.54/6.26 % (3956516)CaDiCaL version: 2.1.3 % 41.54/6.26 % (3956516)Termination reason: Instruction limit % 41.54/6.26 % (3956516)Termination phase: Saturation % 41.54/6.26 % (3956516)Time elapsed: 0.636 s % 41.54/6.26 % (3956516)Peak memory usage: 22 MB % 41.54/6.26 % (3956516)Instructions burned: 692 (million) % 41.54/6.26 % (3956536)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 41.54/6.26 % (3956536)Terminated due to inappropriate strategy. % 41.54/6.26 % (3956536)------------------------------ % 41.54/6.26 % (3956536)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 41.54/6.26 % (3956536)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.54/6.26 % (3956536)CaDiCaL version: 2.1.3 % 41.54/6.26 % (3956536)Termination reason: Inappropriate % 41.54/6.26 % (3956536)Time elapsed: 0.048 s % 41.54/6.26 % (3956536)Peak memory usage: 14 MB % 41.54/6.26 % (3956536)Instructions burned: 99 (million) % 41.54/6.26 % (3956536)------------------------------ % 41.54/6.26 % (3956536)------------------------------ % 41.54/6.26 % (3956540)ott-2_1_sil=16000:newcnf=on:random_seed=3846623659:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2989 on theBenchmark for (2989ds/869Mi) % 41.54/6.26 % (3956541)ott+10_1_sil=32000:tgt=ground:random_seed=2510354506:i=5114:av=off_2989 on theBenchmark for (2989ds/5114Mi) % 41.54/6.26 % (3956517)Instruction limit reached! % 41.54/6.26 % (3956517)------------------------------ % 41.54/6.26 % (3956517)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 41.54/6.26 % (3956517)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.54/6.26 % (3956517)CaDiCaL version: 2.1.3 % 41.54/6.26 % (3956517)Termination reason: Instruction limit % 41.54/6.26 % (3956517)Termination phase: Saturation % 41.54/6.26 % (3956517)Time elapsed: 0.772 s % 41.54/6.26 % (3956517)Peak memory usage: 23 MB % 41.54/6.26 % (3956517)Instructions burned: 879 (million) % 41.54/6.26 % (3956546)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=520479957:i=54282_2988 on theBenchmark for (2988ds/54282Mi) % 41.54/6.26 % (3956546)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 41.54/6.26 % (3956546)Terminated due to inappropriate strategy. % 41.54/6.26 % (3956546)------------------------------ % 41.54/6.26 % (3956546)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 41.54/6.26 % (3956546)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.54/6.26 % (3956546)CaDiCaL version: 2.1.3 % 41.54/6.26 % (3956546)Termination reason: Inappropriate % 41.54/6.26 % (3956546)Time elapsed: 0.083 s % 41.54/6.26 % (3956546)Peak memory usage: 14 MB % 41.54/6.26 % (3956546)Instructions burned: 99 (million) % 149.70/21.46 % (3956546)------------------------------ % 149.70/21.46 % (3956546)------------------------------ % 149.70/21.46 % (3956550)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1001818250:i=3512:aac=none_2986 on theBenchmark for (2986ds/3512Mi) % 149.70/21.46 % (3956540)Instruction limit reached! % 149.70/21.46 % (3956540)------------------------------ % 149.70/21.46 % (3956540)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 149.70/21.46 % (3956540)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.70/21.46 % (3956540)CaDiCaL version: 2.1.3 % 149.70/21.46 % (3956540)Termination reason: Instruction limit % 149.70/21.46 % (3956540)Termination phase: Saturation % 149.70/21.46 % (3956540)Time elapsed: 0.662 s % 149.70/21.46 % (3956540)Peak memory usage: 21 MB % 149.70/21.46 % (3956540)Instructions burned: 869 (million) % 149.70/21.46 % (3956556)dis+21_1_sil=32000:sas=cadical:random_seed=2570157726:i=3773:amm=off_2982 on theBenchmark for (2982ds/3773Mi) % 149.70/21.46 % (3956530)Instruction limit reached! % 149.70/21.46 % (3956530)------------------------------ % 149.70/21.46 % (3956530)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 149.70/21.46 % (3956530)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.70/21.46 % (3956530)CaDiCaL version: 2.1.3 % 149.70/21.46 % (3956530)Termination reason: Instruction limit % 149.70/21.46 % (3956530)Termination phase: Saturation % 149.70/21.46 % (3956530)Time elapsed: 1.047 s % 149.70/21.46 % (3956530)Peak memory usage: 17 MB % 149.70/21.46 % (3956530)Instructions burned: 1473 (million) % 149.70/21.46 % (3956558)ott+11_1_sil=16000:gs=on:random_seed=2430347904:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2980 on theBenchmark for (2980ds/2251Mi) % 149.70/21.46 % (3956524)Instruction limit reached! % 149.70/21.46 % (3956524)------------------------------ % 149.70/21.46 % (3956524)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 149.70/21.46 % (3956524)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.70/21.46 % (3956524)CaDiCaL version: 2.1.3 % 149.70/21.46 % (3956524)Termination reason: Instruction limit % 149.70/21.46 % (3956524)Termination phase: Saturation % 149.70/21.46 % (3956524)Time elapsed: 2.443 s % 149.70/21.46 % (3956524)Peak memory usage: 44 MB % 149.70/21.46 % (3956524)Instructions burned: 5133 (million) % 149.70/21.46 % (3956560)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=263118306:fmbsr=1.6:i=67534_2967 on theBenchmark for (2967ds/67534Mi) % 149.70/21.46 % (3956560)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 149.70/21.46 % (3956560)Terminated due to inappropriate strategy. % 149.70/21.46 % (3956560)------------------------------ % 149.70/21.46 % (3956560)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 149.70/21.46 % (3956560)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.70/21.46 % (3956560)CaDiCaL version: 2.1.3 % 149.70/21.46 % (3956560)Termination reason: Inappropriate % 149.70/21.46 % (3956560)Time elapsed: 0.071 s % 149.70/21.46 % (3956560)Peak memory usage: 14 MB % 149.70/21.46 % (3956560)Instructions burned: 133 (million) % 149.70/21.46 % (3956560)------------------------------ % 149.70/21.46 % (3956560)------------------------------ % 149.70/21.46 % (3956562)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3108361648:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2966 on theBenchmark for (2966ds/4591Mi) % 149.70/21.46 % (3956558)Instruction limit reached! % 149.70/21.46 % (3956558)------------------------------ % 149.70/21.46 % (3956558)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 149.70/21.46 % (3956558)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.70/21.46 % (3956558)CaDiCaL version: 2.1.3 % 149.70/21.46 % (3956558)Termination reason: Instruction limit % 149.70/21.46 % (3956558)Termination phase: Saturation % 149.70/21.46 % (3956558)Time elapsed: 1.697 s % 149.70/21.46 % (3956558)Peak memory usage: 20 MB % 149.70/21.46 % (3956558)Instructions burned: 2252 (million) % 149.70/21.46 % (3956564)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1640645668:i=29340_2962 on theBenchmark for (2962ds/29340Mi) % 149.70/21.46 % (3956550)Instruction limit reached! % 149.70/21.46 % (3956550)------------------------------ % 149.70/21.46 % (3956550)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 149.70/21.46 % (3956550)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.70/21.46 % (3956550)CaDiCaL version: 2.1.3 % 149.70/21.46 % (3956550)Termination reason: Instruction limit % 197.61/28.14 % (3956550)Termination phase: Saturation % 197.61/28.14 % (3956550)Time elapsed: 2.880 s % 197.61/28.14 % (3956550)Peak memory usage: 28 MB % 197.61/28.14 % (3956550)Instructions burned: 3513 (million) % 197.61/28.14 % (3956568)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2168298014:i=5211_2957 on theBenchmark for (2957ds/5211Mi) % 197.61/28.14 % (3956556)Instruction limit reached! % 197.61/28.14 % (3956556)------------------------------ % 197.61/28.14 % (3956556)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 197.61/28.14 % (3956556)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 197.61/28.14 % (3956556)CaDiCaL version: 2.1.3 % 197.61/28.14 % (3956556)Termination reason: Instruction limit % 197.61/28.14 % (3956556)Termination phase: Saturation % 197.61/28.14 % (3956556)Time elapsed: 2.849 s % 197.61/28.14 % (3956556)Peak memory usage: 26 MB % 197.61/28.14 % (3956556)Instructions burned: 3774 (million) % 197.61/28.14 % (3956570)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=4097386879:i=5497:nm=2_2953 on theBenchmark for (2953ds/5497Mi) % 197.61/28.14 % (3956570)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 197.61/28.14 % (3956570)Terminated due to inappropriate strategy. % 197.61/28.14 % (3956570)------------------------------ % 197.61/28.14 % (3956570)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 197.61/28.14 % (3956570)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 197.61/28.14 % (3956570)CaDiCaL version: 2.1.3 % 197.61/28.14 % (3956570)Termination reason: Inappropriate % 197.61/28.14 % (3956570)Time elapsed: 0.088 s % 197.61/28.14 % (3956570)Peak memory usage: 14 MB % 197.61/28.14 % (3956570)Instructions burned: 99 (million) % 197.61/28.14 % (3956570)------------------------------ % 197.61/28.14 % (3956570)------------------------------ % 197.61/28.14 % (3956572)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=2676350496:fmbsr=2:i=46332_2952 on theBenchmark for (2952ds/46332Mi) % 197.61/28.14 % (3956572)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 197.61/28.14 % (3956572)Terminated due to inappropriate strategy. % 197.61/28.14 % (3956572)------------------------------ % 197.61/28.14 % (3956572)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 197.61/28.14 % (3956572)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 197.61/28.14 % (3956572)CaDiCaL version: 2.1.3 % 197.61/28.14 % (3956572)Termination reason: Inappropriate % 197.61/28.14 % (3956572)Time elapsed: 0.064 s % 197.61/28.14 % (3956572)Peak memory usage: 14 MB % 197.61/28.14 % (3956572)Instructions burned: 138 (million) % 197.61/28.14 % (3956572)------------------------------ % 197.61/28.14 % (3956572)------------------------------ % 197.61/28.14 % (3956574)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=695123345:i=14071_2951 on theBenchmark for (2951ds/14071Mi) % 197.61/28.14 % (3956574)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 197.61/28.14 % (3956574)Terminated due to inappropriate strategy. % 197.61/28.14 % (3956574)------------------------------ % 197.61/28.14 % (3956574)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 197.61/28.14 % (3956574)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 197.61/28.14 % (3956574)CaDiCaL version: 2.1.3 % 197.61/28.14 % (3956574)Termination reason: Inappropriate % 197.61/28.14 % (3956574)Time elapsed: 0.103 s % 197.61/28.14 % (3956574)Peak memory usage: 14 MB % 197.61/28.14 % (3956574)Instructions burned: 138 (million) % 197.61/28.14 % (3956574)------------------------------ % 197.61/28.14 % (3956574)------------------------------ % 197.61/28.14 % (3956576)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3921423789:i=22565:add=on:rawr=on_2950 on theBenchmark for (2950ds/22565Mi) % 197.61/28.14 % (3956541)Instruction limit reached! % 197.61/28.14 % (3956541)------------------------------ % 197.61/28.14 % (3956541)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 197.61/28.14 % (3956541)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 197.61/28.14 % (3956541)CaDiCaL version: 2.1.3 % 197.61/28.14 % (3956541)Termination reason: Instruction limit % 197.61/28.14 % (3956541)Termination phase: Saturation % 197.61/28.14 % (3956541)Time elapsed: 4.810 s % 197.61/28.14 % (3956541)Peak memory usage: 33 MB % 197.61/28.14 % (3956541)Instructions burned: 5114 (million) % 197.61/28.14 % (3956578)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=3841063574:i=8173:av=off_2940 on theBenchmark for (2940ds/8173Mi) % 200.21/28.51 % (3956562)Instruction limit reached! % 200.21/28.51 % (3956562)------------------------------ % 200.21/28.51 % (3956562)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 200.21/28.51 % (3956562)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 200.21/28.51 % (3956562)CaDiCaL version: 2.1.3 % 200.21/28.51 % (3956562)Termination reason: Instruction limit % 200.21/28.51 % (3956562)Termination phase: Saturation % 200.21/28.51 % (3956562)Time elapsed: 3.906 s % 200.21/28.51 % (3956562)Peak memory usage: 43 MB % 200.21/28.51 % (3956562)Instructions burned: 4592 (million) % 200.21/28.51 % (3956580)dis+10_16:1_sil=16000:random_seed=2802992990:i=9155:fsr=off_2926 on theBenchmark for (2926ds/9155Mi) % 200.21/28.51 % (3956568)Instruction limit reached! % 200.21/28.51 % (3956568)------------------------------ % 200.21/28.51 % (3956568)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 200.21/28.51 % (3956568)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 200.21/28.51 % (3956568)CaDiCaL version: 2.1.3 % 200.21/28.51 % (3956568)Termination reason: Instruction limit % 200.21/28.51 % (3956568)Termination phase: Saturation % 200.21/28.51 % (3956568)Time elapsed: 4.737 s % 200.21/28.51 % (3956568)Peak memory usage: 52 MB % 200.21/28.51 % (3956568)Instructions burned: 5211 (million) % 200.21/28.51 % (3956582)ott-3_8_sil=64000:random_seed=1626845872:i=20139:bs=on_2909 on theBenchmark for (2909ds/20139Mi) % 200.21/28.51 % (3956578)Instruction limit reached! % 200.21/28.51 % (3956578)------------------------------ % 200.21/28.51 % (3956578)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 200.21/28.51 % (3956578)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 200.21/28.51 % (3956578)CaDiCaL version: 2.1.3 % 200.21/28.51 % (3956578)Termination reason: Instruction limit % 200.21/28.51 % (3956578)Termination phase: Saturation % 200.21/28.51 % (3956578)Time elapsed: 5.550 s % 200.21/28.51 % (3956578)Peak memory usage: 39 MB % 200.21/28.51 % (3956578)Instructions burned: 8174 (million) % 200.21/28.51 % (3956584)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=3471799524:fmbsr=2:i=32576_2884 on theBenchmark for (2884ds/32576Mi) % 200.21/28.51 % (3956584)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 200.21/28.51 % (3956584)Terminated due to inappropriate strategy. % 200.21/28.51 % (3956584)------------------------------ % 200.21/28.51 % (3956584)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 200.21/28.51 % (3956584)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 200.21/28.51 % (3956584)CaDiCaL version: 2.1.3 % 200.21/28.51 % (3956584)Termination reason: Inappropriate % 200.21/28.51 % (3956584)Time elapsed: 0.065 s % 200.21/28.51 % (3956584)Peak memory usage: 15 MB % 200.21/28.51 % (3956584)Instructions burned: 134 (million) % 200.21/28.51 % (3956584)------------------------------ % 200.21/28.51 % (3956584)------------------------------ % 200.21/28.51 % (3956586)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=548126202:i=11404_2883 on theBenchmark for (2883ds/11404Mi) % 200.21/28.51 % (3956580)Instruction limit reached! % 200.21/28.51 % (3956580)------------------------------ % 200.21/28.51 % (3956580)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 200.21/28.51 % (3956580)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 200.21/28.51 % (3956580)CaDiCaL version: 2.1.3 % 200.21/28.51 % (3956580)Termination reason: Instruction limit % 200.21/28.51 % (3956580)Termination phase: Saturation % 200.21/28.51 % (3956580)Time elapsed: 8.071 s % 200.21/28.51 % (3956580)Peak memory usage: 56 MB % 200.21/28.51 % (3956580)Instructions burned: 9155 (million) % 200.21/28.51 % (3956606)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=2021244620:i=14134_2845 on theBenchmark for (2845ds/14134Mi) % 200.21/28.51 % (3956564)Instruction limit reached! % 200.21/28.51 % (3956564)------------------------------ % 200.21/28.51 % (3956564)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 200.21/28.51 % (3956564)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 200.21/28.51 % (3956564)CaDiCaL version: 2.1.3 % 200.21/28.51 % (3956564)Termination reason: Instruction limit % 200.21/28.51 % (3956564)Termination phase: Saturation % 200.21/28.51 % (3956564)Time elapsed: 12.857 s % 200.21/28.51 % (3956564)Peak memory usage: 43 MB % 200.21/28.51 % (3956564)Instructions burned: 29343 (million) % 200.21/28.51 % (3956612)dis+33_16_sil=32000:sac=on:random_seed=825784358:i=15851:nm=0_2834 on theBenchmark for (2834ds/15851Mi) % 200.21/28.51 % (3956576)Instruction limit reached! % 200.21/28.51 % (3956576)------------------------------ % 200.21/28.51 % (3956576)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 221.44/31.53 % (3956576)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 221.44/31.53 % (3956576)CaDiCaL version: 2.1.3 % 221.44/31.53 % (3956576)Termination reason: Instruction limit % 221.44/31.53 % (3956576)Termination phase: Saturation % 221.44/31.53 % (3956576)Time elapsed: 16.129 s % 221.44/31.53 % (3956576)Peak memory usage: 27 MB % 221.44/31.53 % (3956576)Instructions burned: 22566 (million) % 221.44/31.53 % (3956643)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=1066530893:avsq=on:i=17627:add=on:amm=off_2788 on theBenchmark for (2788ds/17627Mi) % 221.44/31.53 % (3956612)Instruction limit reached! % 221.44/31.53 % (3956612)------------------------------ % 221.44/31.53 % (3956612)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 221.44/31.53 % (3956612)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 221.44/31.53 % (3956612)CaDiCaL version: 2.1.3 % 221.44/31.53 % (3956612)Termination reason: Instruction limit % 221.44/31.53 % (3956612)Termination phase: Saturation % 221.44/31.53 % (3956612)Time elapsed: 6.257 s % 221.44/31.53 % (3956612)Peak memory usage: 35 MB % 221.44/31.53 % (3956612)Instructions burned: 15852 (million) % 221.44/31.53 % (3956645)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=1059457875:s2a=on:i=53295_2771 on theBenchmark for (2771ds/53295Mi) % 221.44/31.53 % (3956586)Instruction limit reached! % 221.44/31.53 % (3956586)------------------------------ % 221.44/31.53 % (3956586)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 221.44/31.53 % (3956586)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 221.44/31.53 % (3956586)CaDiCaL version: 2.1.3 % 221.44/31.53 % (3956586)Termination reason: Instruction limit % 221.44/31.53 % (3956586)Termination phase: Saturation % 221.44/31.53 % (3956586)Time elapsed: 11.488 s % 221.44/31.53 % (3956586)Peak memory usage: 48 MB % 221.44/31.53 % (3956586)Instructions burned: 11404 (million) % 221.44/31.53 % (3956647)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=1691229586:i=26857:ins=20_2768 on theBenchmark for (2768ds/26857Mi) % 221.44/31.53 % (3956647)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 221.44/31.53 % (3956647)Terminated due to inappropriate strategy. % 221.44/31.53 % (3956647)------------------------------ % 221.44/31.53 % (3956647)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 221.44/31.53 % (3956647)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 221.44/31.53 % (3956647)CaDiCaL version: 2.1.3 % 221.44/31.53 % (3956647)Termination reason: Inappropriate % 221.44/31.53 % (3956647)Time elapsed: 0.043 s % 221.44/31.53 % (3956647)Peak memory usage: 14 MB % 221.44/31.53 % (3956647)Instructions burned: 99 (million) % 221.44/31.53 % (3956647)------------------------------ % 221.44/31.53 % (3956647)------------------------------ % 221.44/31.53 % (3956649)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=98407603:i=28120:bs=on:fsr=off_2768 on theBenchmark for (2768ds/28120Mi) % 221.44/31.53 % (3956582)Instruction limit reached! % 221.44/31.53 % (3956582)------------------------------ % 221.44/31.53 % (3956582)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 221.44/31.53 % (3956582)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 221.44/31.53 % (3956582)CaDiCaL version: 2.1.3 % 221.44/31.53 % (3956582)Termination reason: Instruction limit % 221.44/31.53 % (3956582)Termination phase: Saturation % 221.44/31.53 % (3956582)Time elapsed: 18.711 s % 221.44/31.53 % (3956582)Peak memory usage: 60 MB % 221.44/31.53 % (3956582)Instructions burned: 20140 (million) % 221.44/31.53 % (3956745)fmb+10_1_sil=256000:fmbss=7:random_seed=113621410:fmbsr=1.6:i=182295_2722 on theBenchmark for (2722ds/182295Mi) % 221.44/31.53 % (3956745)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 221.44/31.53 % (3956745)Terminated due to inappropriate strategy. % 221.44/31.53 % (3956745)------------------------------ % 221.44/31.53 % (3956745)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 221.44/31.53 % (3956745)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 221.44/31.53 % (3956745)CaDiCaL version: 2.1.3 % 221.44/31.53 % (3956745)Termination reason: Inappropriate % 221.44/31.53 % (3956745)Time elapsed: 0.042 s % 221.44/31.53 % (3956745)Peak memory usage: 14 MB % 221.44/31.53 % (3956745)Instructions burned: 99 (million) % 221.44/31.53 % (3956745)------------------------------ % 221.44/31.53 % (3956745)------------------------------ % 221.44/31.53 % (3956752)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=558000875:i=44625:gsp=on_2721 on theBenchmark for (2721ds/44625Mi) % 227.65/32.47 % (3956752)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 227.65/32.47 % (3956752)Terminated due to inappropriate strategy. % 227.65/32.47 % (3956752)------------------------------ % 227.65/32.47 % (3956752)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 227.65/32.47 % (3956752)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 227.65/32.47 % (3956752)CaDiCaL version: 2.1.3 % 227.65/32.47 % (3956752)Termination reason: Inappropriate % 227.65/32.47 % (3956752)Time elapsed: 0.048 s % 227.65/32.47 % (3956752)Peak memory usage: 15 MB % 227.65/32.47 % (3956752)Instructions burned: 104 (million) % 227.65/32.47 % (3956752)------------------------------ % 227.65/32.47 % (3956752)------------------------------ % 227.65/32.47 % (3956766)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=4278197367:i=160505_2721 on theBenchmark for (2721ds/160505Mi) % 227.65/32.47 % (3956766)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 227.65/32.47 % (3956766)Terminated due to inappropriate strategy. % 227.65/32.47 % (3956766)------------------------------ % 227.65/32.47 % (3956766)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 227.65/32.47 % (3956766)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 227.65/32.47 % (3956766)CaDiCaL version: 2.1.3 % 227.65/32.47 % (3956766)Termination reason: Inappropriate % 227.65/32.47 % (3956766)Time elapsed: 0.042 s % 227.65/32.47 % (3956766)Peak memory usage: 14 MB % 227.65/32.47 % (3956766)Instructions burned: 99 (million) % 227.65/32.47 % (3956766)------------------------------ % 227.65/32.47 % (3956766)------------------------------ % 227.65/32.47 % (3956768)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=3467590569:fmbsr=1.3:i=225729_2720 on theBenchmark for (2720ds/225729Mi) % 227.65/32.47 % (3956768)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 227.65/32.47 % (3956768)Terminated due to inappropriate strategy. % 227.65/32.47 % (3956768)------------------------------ % 227.65/32.47 % (3956768)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 227.65/32.47 % (3956768)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 227.65/32.47 % (3956768)CaDiCaL version: 2.1.3 % 227.65/32.47 % (3956768)Termination reason: Inappropriate % 227.65/32.47 % (3956768)Time elapsed: 0.057 s % 227.65/32.47 % (3956768)Peak memory usage: 14 MB % 227.65/32.47 % (3956768)Instructions burned: 138 (million) % 227.65/32.47 % (3956768)------------------------------ % 227.65/32.47 % (3956768)------------------------------ % 227.65/32.47 % (3956787)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=4241680635:fmbsr=2:i=185024:ins=7_2719 on theBenchmark for (2719ds/185024Mi) % 227.65/32.47 % (3956787)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 227.65/32.47 % (3956787)Terminated due to inappropriate strategy. % 227.65/32.47 % (3956787)------------------------------ % 227.65/32.47 % (3956787)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 227.65/32.47 % (3956787)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 227.65/32.47 % (3956787)CaDiCaL version: 2.1.3 % 227.65/32.47 % (3956787)Termination reason: Inappropriate % 227.65/32.47 % (3956787)Time elapsed: 0.057 s % 227.65/32.47 % (3956787)Peak memory usage: 14 MB % 227.65/32.47 % (3956787)Instructions burned: 138 (million) % 227.65/32.47 % (3956787)------------------------------ % 227.65/32.47 % (3956787)------------------------------ % 227.65/32.47 % (3956819)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=929676911:rtra=on_2718 on theBenchmark for (2718ds/0Mi) % 227.65/32.47 % (3956819)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 227.65/32.47 % (3956819)Terminated due to inappropriate strategy. % 227.65/32.47 % (3956819)------------------------------ % 227.65/32.47 % (3956819)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 227.65/32.47 % (3956819)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 227.65/32.47 % (3956819)CaDiCaL version: 2.1.3 % 227.65/32.47 % (3956819)Termination reason: Inappropriate % 227.65/32.47 % (3956819)Time elapsed: 0.055 s % 227.65/32.47 % (3956819)Peak memory usage: 16 MB % 227.65/32.47 % (3956819)Instructions burned: 116 (million) % 227.65/32.47 % (3956819)------------------------------ % 227.65/32.47 % (3956819)------------------------------ % 227.65/32.47 % (3956821)% WARNING: option uhcvi not known. % 227.65/32.47 % (3956821)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3664718465:i=271062:add=off:rtra=on:rawr=on_2718 on theBenchmark for (2718ds/271062Mi) % 240.67/34.27 % (3956606)Instruction limit reached! % 240.67/34.27 % (3956606)------------------------------ % 240.67/34.27 % (3956606)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 240.67/34.27 % (3956606)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 240.67/34.27 % (3956606)CaDiCaL version: 2.1.3 % 240.67/34.27 % (3956606)Termination reason: Instruction limit % 240.67/34.27 % (3956606)Termination phase: Saturation % 240.67/34.27 % (3956606)Time elapsed: 12.978 s % 240.67/34.27 % (3956606)Peak memory usage: 53 MB % 240.67/34.27 % (3956606)Instructions burned: 14134 (million) % 240.67/34.27 % (3956823)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2844931837:i=176048:add=on:rtra=on:rawr=on_2715 on theBenchmark for (2715ds/176048Mi) % 240.67/34.27 % (3956649)Instruction limit reached! % 240.67/34.27 % (3956649)------------------------------ % 240.67/34.27 % (3956649)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 240.67/34.27 % (3956649)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 240.67/34.27 % (3956649)CaDiCaL version: 2.1.3 % 240.67/34.27 % (3956649)Termination reason: Instruction limit % 240.67/34.27 % (3956649)Termination phase: Saturation % 240.67/34.27 % (3956649)Time elapsed: 7.677 s % 240.67/34.27 % (3956649)Peak memory usage: 26 MB % 240.67/34.27 % (3956649)Instructions burned: 28123 (million) % 240.67/34.27 % (3956825)dis+10_1_sil=32000:si=on:sp=arity:random_seed=488630671:i=206:fgj=on:rtra=on_2691 on theBenchmark for (2691ds/206Mi) % 240.67/34.27 % (3956825)Instruction limit reached! % 240.67/34.27 % (3956825)------------------------------ % 240.67/34.27 % (3956825)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 240.67/34.27 % (3956825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 240.67/34.27 % (3956825)CaDiCaL version: 2.1.3 % 240.67/34.27 % (3956825)Termination reason: Instruction limit % 240.67/34.27 % (3956825)Termination phase: Saturation % 240.67/34.27 % (3956825)Time elapsed: 0.056 s % 240.67/34.27 % (3956825)Peak memory usage: 18 MB % 240.67/34.27 % (3956825)Instructions burned: 207 (million) % 240.67/34.27 % (3956827)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=2920231732:i=232:rtra=on_2690 on theBenchmark for (2690ds/232Mi) % 240.67/34.27 % (3956827)Instruction limit reached! % 240.67/34.27 % (3956827)------------------------------ % 240.67/34.27 % (3956827)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 240.67/34.27 % (3956827)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 240.67/34.27 % (3956827)CaDiCaL version: 2.1.3 % 240.67/34.27 % (3956827)Termination reason: Instruction limit % 240.67/34.27 % (3956827)Termination phase: Saturation % 240.67/34.27 % (3956827)Time elapsed: 0.060 s % 240.67/34.27 % (3956827)Peak memory usage: 18 MB % 240.67/34.27 % (3956827)Instructions burned: 234 (million) % 240.67/34.27 % (3956829)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=1811241737:i=262:rtra=on_2689 on theBenchmark for (2689ds/262Mi) % 240.67/34.27 % (3956829)Instruction limit reached! % 240.67/34.27 % (3956829)------------------------------ % 240.67/34.27 % (3956829)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 240.67/34.27 % (3956829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 240.67/34.27 % (3956829)CaDiCaL version: 2.1.3 % 240.67/34.27 % (3956829)Termination reason: Instruction limit % 240.67/34.27 % (3956829)Termination phase: Saturation % 240.67/34.27 % (3956829)Time elapsed: 0.067 s % 240.67/34.27 % (3956829)Peak memory usage: 18 MB % 240.67/34.27 % (3956829)Instructions burned: 262 (million) % 240.67/34.27 % (3956831)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=1182129100:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2688 on theBenchmark for (2688ds/318Mi) % 240.67/34.27 % (3956831)Instruction limit reached! % 240.67/34.27 % (3956831)------------------------------ % 240.67/34.27 % (3956831)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 240.67/34.27 % (3956831)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 240.67/34.27 % (3956831)CaDiCaL version: 2.1.3 % 240.67/34.27 % (3956831)Termination reason: Instruction limit % 240.67/34.27 % (3956831)Termination phase: Saturation % 240.67/34.27 % (3956831)Time elapsed: 0.082 s % 240.67/34.27 % (3956831)Peak memory usage: 18 MB % 240.67/34.27 % (3956831)Instructions burned: 321 (million) % 240.67/34.27 % (3956833)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=1966696332:i=1428:nm=2:rtra=on_2687 on theBenchmark for (2687ds/1428Mi) % 247.29/35.19 % (3956833)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 247.29/35.19 % (3956833)Terminated due to inappropriate strategy. % 247.29/35.19 % (3956833)------------------------------ % 247.29/35.19 % (3956833)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 247.29/35.19 % (3956833)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 247.29/35.19 % (3956833)CaDiCaL version: 2.1.3 % 247.29/35.19 % (3956833)Termination reason: Inappropriate % 247.29/35.19 % (3956833)Time elapsed: 0.030 s % 247.29/35.19 % (3956833)Peak memory usage: 16 MB % 247.29/35.19 % (3956833)Instructions burned: 115 (million) % 247.29/35.19 % (3956833)------------------------------ % 247.29/35.19 % (3956833)------------------------------ % 247.29/35.19 % (3956835)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=548556218:i=262:bd=preordered:rtra=on:fsd=on_2687 on theBenchmark for (2687ds/262Mi) % 247.29/35.19 % (3956835)Instruction limit reached! % 247.29/35.19 % (3956835)------------------------------ % 247.29/35.19 % (3956835)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 247.29/35.19 % (3956835)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 247.29/35.19 % (3956835)CaDiCaL version: 2.1.3 % 247.29/35.19 % (3956835)Termination reason: Instruction limit % 247.29/35.19 % (3956835)Termination phase: Saturation % 247.29/35.19 % (3956835)Time elapsed: 0.065 s % 247.29/35.19 % (3956835)Peak memory usage: 18 MB % 247.29/35.19 % (3956835)Instructions burned: 267 (million) % 247.29/35.19 % (3956837)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=4187884424:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2686 on theBenchmark for (2686ds/1368Mi) % 247.29/35.19 % (3956837)Instruction limit reached! % 247.29/35.19 % (3956837)------------------------------ % 247.29/35.19 % (3956837)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 247.29/35.19 % (3956837)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 247.29/35.19 % (3956837)CaDiCaL version: 2.1.3 % 247.29/35.19 % (3956837)Termination reason: Instruction limit % 247.29/35.19 % (3956837)Termination phase: Saturation % 247.29/35.19 % (3956837)Time elapsed: 0.372 s % 247.29/35.19 % (3956837)Peak memory usage: 23 MB % 247.29/35.19 % (3956837)Instructions burned: 1369 (million) % 247.29/35.19 % (3956839)ott-21_1_sil=16000:si=on:fs=off:random_seed=2177709264:i=360:av=off:fsr=off:rtra=on_2682 on theBenchmark for (2682ds/360Mi) % 247.29/35.19 % (3956839)Instruction limit reached! % 247.29/35.19 % (3956839)------------------------------ % 247.29/35.19 % (3956839)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 247.29/35.19 % (3956839)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 247.29/35.19 % (3956839)CaDiCaL version: 2.1.3 % 247.29/35.19 % (3956839)Termination reason: Instruction limit % 247.29/35.19 % (3956839)Termination phase: Saturation % 247.29/35.19 % (3956839)Time elapsed: 0.097 s % 247.29/35.19 % (3956839)Peak memory usage: 17 MB % 247.29/35.19 % (3956839)Instructions burned: 364 (million) % 247.29/35.19 % (3956841)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3577703172:i=954:bd=all:rtra=on_2681 on theBenchmark for (2681ds/954Mi) % 247.29/35.19 % (3956841)Instruction limit reached! % 247.29/35.19 % (3956841)------------------------------ % 247.29/35.19 % (3956841)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 247.29/35.19 % (3956841)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 247.29/35.19 % (3956841)CaDiCaL version: 2.1.3 % 247.29/35.19 % (3956841)Termination reason: Instruction limit % 247.29/35.19 % (3956841)Termination phase: Saturation % 247.29/35.19 % (3956841)Time elapsed: 0.288 s % 247.29/35.19 % (3956841)Peak memory usage: 22 MB % 247.29/35.19 % (3956841)Instructions burned: 956 (million) % 247.29/35.19 % (3956843)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=327428412:fmbsr=1.3:i=1730:ins=25:rtra=on_2678 on theBenchmark for (2678ds/1730Mi) % 247.29/35.19 % (3956843)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 247.29/35.19 % (3956843)Terminated due to inappropriate strategy. % 247.29/35.19 % (3956843)------------------------------ % 247.29/35.19 % (3956843)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 247.29/35.19 % (3956843)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 247.29/35.19 % (3956843)CaDiCaL version: 2.1.3 % 247.29/35.19 % (3956843)Termination reason: Inappropriate % 290.36/41.22 % (3956843)Time elapsed: 0.030 s % 290.36/41.22 % (3956843)Peak memory usage: 16 MB % 290.36/41.22 % (3956843)Instructions burned: 114 (million) % 290.36/41.22 % (3956843)------------------------------ % 290.36/41.22 % (3956843)------------------------------ % 290.36/41.22 % (3956845)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=639307005:i=2358:rtra=on_2678 on theBenchmark for (2678ds/2358Mi) % 290.36/41.22 % (3956845)Instruction limit reached! % 290.36/41.22 % (3956845)------------------------------ % 290.36/41.22 % (3956845)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 290.36/41.22 % (3956845)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 290.36/41.22 % (3956845)CaDiCaL version: 2.1.3 % 290.36/41.22 % (3956845)Termination reason: Instruction limit % 290.36/41.22 % (3956845)Termination phase: Saturation % 290.36/41.22 % (3956845)Time elapsed: 0.683 s % 290.36/41.22 % (3956845)Peak memory usage: 26 MB % 290.36/41.22 % (3956845)Instructions burned: 2360 (million) % 290.36/41.22 % (3956847)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=512811701:i=1778:ins=1:rtra=on_2671 on theBenchmark for (2671ds/1778Mi) % 290.36/41.22 % (3956847)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 290.36/41.22 % (3956847)Terminated due to inappropriate strategy. % 290.36/41.22 % (3956847)------------------------------ % 290.36/41.22 % (3956847)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 290.36/41.22 % (3956847)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 290.36/41.22 % (3956847)CaDiCaL version: 2.1.3 % 290.36/41.22 % (3956847)Termination reason: Inappropriate % 290.36/41.22 % (3956847)Time elapsed: 0.041 s % 290.36/41.22 % (3956847)Peak memory usage: 18 MB % 290.36/41.22 % (3956847)Instructions burned: 155 (million) % 290.36/41.22 % (3956847)------------------------------ % 290.36/41.22 % (3956847)------------------------------ % 290.36/41.22 % (3956849)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=936748704:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2670 on theBenchmark for (2670ds/1384Mi) % 290.36/41.22 % (3956849)Instruction limit reached! % 290.36/41.22 % (3956849)------------------------------ % 290.36/41.22 % (3956849)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 290.36/41.22 % (3956849)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 290.36/41.22 % (3956849)CaDiCaL version: 2.1.3 % 290.36/41.22 % (3956849)Termination reason: Instruction limit % 290.36/41.22 % (3956849)Termination phase: Saturation % 290.36/41.22 % (3956849)Time elapsed: 0.431 s % 290.36/41.22 % (3956849)Peak memory usage: 27 MB % 290.36/41.22 % (3956849)Instructions burned: 1386 (million) % 290.36/41.22 % (3956851)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=3510760843:i=1758:kws=inv_precedence:fsr=off:rtra=on_2666 on theBenchmark for (2666ds/1758Mi) % 290.36/41.22 % (3956643)Instruction limit reached! % 290.36/41.22 % (3956643)------------------------------ % 290.36/41.22 % (3956643)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 290.36/41.22 % (3956643)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 290.36/41.22 % (3956643)CaDiCaL version: 2.1.3 % 290.36/41.22 % (3956643)Termination reason: Instruction limit % 290.36/41.22 % (3956643)Termination phase: Saturation % 290.36/41.22 % (3956643)Time elapsed: 12.717 s % 290.36/41.22 % (3956643)Peak memory usage: 120 MB % 290.36/41.22 % (3956643)Instructions burned: 17627 (million) % 290.36/41.22 % (3956851)Instruction limit reached! % 290.36/41.22 % (3956851)------------------------------ % 290.36/41.22 % (3956851)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 290.36/41.22 % (3956851)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 290.36/41.22 % (3956851)CaDiCaL version: 2.1.3 % 290.36/41.22 % (3956851)Termination reason: Instruction limit % 290.36/41.22 % (3956851)Termination phase: Saturation % 290.36/41.22 % (3956851)Time elapsed: 0.543 s % 290.36/41.22 % (3956851)Peak memory usage: 29 MB % 290.36/41.22 % (3956851)Instructions burned: 1758 (million) % 290.36/41.22 % (3956853)fmb+10_1_sil=64000:si=on:random_seed=2368344403:i=44122:nm=2:rtra=on:gsp=on_2660 on theBenchmark for (2660ds/44122Mi) % 290.36/41.22 % (3956854)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=1807079660:i=19030:nm=5:rtra=on_2660 on theBenchmark for (2660ds/19030Mi) % 290.36/41.22 % (3956853)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.02/42.63 % (3956853)Terminated due to inappropriate strategy. % 300.02/42.63 % (3956853)------------------------------ % 300.02/42.63 % (3956853)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.02/42.63 % (3956853)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.02/42.63 % (3956853)CaDiCaL version: 2.1.3 % 300.02/42.63 % (3956853)Termination reason: Inappropriate % 300.02/42.63 % (3956853)Time elapsed: 0.032 s % 300.02/42.63 % (3956853)Peak memory usage: 16 MB % 300.02/42.63 % (3956853)Instructions burned: 125 (million) % 300.02/42.63 % (3956853)------------------------------ % 300.02/42.63 % (3956853)------------------------------ % 300.02/42.63 % (3956857)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=410218120:fmbsr=1.7:i=1840:rtra=on_2660 on theBenchmark for (2660ds/1840Mi) % 300.02/42.63 % (3956854)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.02/42.63 % (3956854)Terminated due to inappropriate strategy. % 300.02/42.63 % (3956854)------------------------------ % 300.02/42.63 % (3956854)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.02/42.63 % (3956854)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.02/42.63 % (3956854)CaDiCaL version: 2.1.3 % 300.02/42.63 % (3956854)Termination reason: Inappropriate % 300.02/42.63 % (3956854)Time elapsed: 0.055 s % 300.02/42.63 % (3956854)Peak memory usage: 16 MB % 300.02/42.63 % (3956854)Instructions burned: 115 (million) % 300.02/42.63 % (3956854)------------------------------ % 300.02/42.63 % (3956854)------------------------------ % 300.02/42.63 % (3956857)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.02/42.63 % (3956857)Terminated due to inappropriate strategy. % 300.02/42.63 % (3956857)------------------------------ % 300.02/42.63 % (3956857)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.02/42.63 % (3956857)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.02/42.63 % (3956857)CaDiCaL version: 2.1.3 % 300.02/42.63 % (3956857)Termination reason: Inappropriate % 300.02/42.63 % (3956857)Time elapsed: 0.030 s % 300.02/42.63 % (3956857)Peak memory usage: 16 MB % 300.02/42.63 % (3956857)Instructions burned: 115 (million) % 300.02/42.63 % (3956857)------------------------------ % 300.02/42.63 % (3956857)------------------------------ % 300.02/42.63 % (3956860)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2263433035:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2659 on theBenchmark for (2659ds/2944Mi) % 300.02/42.63 % (3956859)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=63222261:i=10262:rtra=on_2659 on theBenchmark for (2659ds/10262Mi) % 300.02/42.63 % (3956860)Instruction limit reached! % 300.02/42.63 % (3956860)------------------------------ % 300.02/42.63 % (3956860)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.02/42.63 % (3956860)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.02/42.63 % (3956860)CaDiCaL version: 2.1.3 % 300.02/42.63 % (3956860)Termination reason: Instruction limit % 300.02/42.63 % (3956860)Termination phase: Saturation % 300.02/42.63 % (3956860)Time elapsed: 0.784 s % 300.02/42.63 % (3956860)Peak memory usage: 32 MB % 300.02/42.63 % (3956860)Instructions burned: 2946 (million) % 300.02/42.63 % (3956863)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=1887433064:i=12648:rtra=on_2651 on theBenchmark for (2651ds/12648Mi) % 300.02/42.63 % (3956863)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.02/42.63 % (3956863)Terminated due to inappropriate strategy. % 300.02/42.63 % (3956863)------------------------------ % 300.02/42.63 % (3956863)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.02/42.63 % (3956863)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.02/42.63 % (3956863)CaDiCaL version: 2.1.3 % 300.02/42.63 % (3956863)Termination reason: Inappropriate % 300.02/42.63 % (3956863)Time elapsed: 0.030 s % 300.02/42.63 % (3956863)Peak memory usage: 16 MB % 300.02/42.63 % (3956863)Instructions burned: 115 (million) % 300.02/42.63 % (3956863)------------------------------ % 300.02/42.63 % (3956863)------------------------------ % 300.02/42.63 % (3956865)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=4261083459:fmbsr=2.30978:i=4348:rtra=on_2651 on theBenchmark for (2651ds/4348Mi) % 300.02/42.63 % (3956865)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.02/42.63 % (3956865)Terminated due to inappropriate strategy. % 300.02/42.63 % (3956865)---------- % 300.02/42.63 Terminated % 300.02/42.63 % Vampire exiting %------------------------------------------------------------------------------