%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW575_2 : TPTP v9.3.1. Released v6.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n003.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:28 PM UTC 2026 % Result : Timeout 297.98s 42.29s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWW575_2 : TPTP v9.3.1. Released v6.1.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.10/0.23 % Computer : n003.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:21:27 UTC 2026 % 0.10/0.24 % CPUTime : % 0.10/0.24 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.24/0.29 Running first-order model finding % 0.24/0.29 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.39/1.06 % (1619311)Will run a generic schedule for satisfiability detection. % 5.39/1.06 % (1619317)% WARNING: option uhcvi not known. % 5.39/1.06 % (1619321)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=707628683:i=131_2999 on theBenchmark for (2999ds/131Mi) % 5.39/1.06 % (1619317)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=244757177:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 5.39/1.06 % (1619316)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3937569757_2999 on theBenchmark for (2999ds/0Mi) % 5.39/1.06 % (1619319)dis+10_1_sil=32000:sp=arity:random_seed=3467713538:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 5.39/1.06 % (1619320)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2542346342:i=116_2999 on theBenchmark for (2999ds/116Mi) % 5.39/1.06 % (1619322)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=4002239471:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 5.39/1.06 % (1619318)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4171317051:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 5.39/1.06 % (1619316)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 5.39/1.06 % (1619316)Terminated due to inappropriate strategy. % 5.39/1.06 % (1619316)------------------------------ % 5.39/1.06 % (1619316)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.39/1.06 % (1619316)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.39/1.06 % (1619316)CaDiCaL version: 2.1.3 % 5.39/1.06 % (1619316)Termination reason: Inappropriate % 5.39/1.06 % (1619316)Time elapsed: 0.015 s % 5.39/1.06 % (1619316)Peak memory usage: 11 MB % 5.39/1.06 % (1619316)Instructions burned: 16 (million) % 5.39/1.06 % (1619316)------------------------------ % 5.39/1.06 % (1619316)------------------------------ % 5.39/1.06 % (1619333)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2925801461:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 5.39/1.06 % (1619321)Instruction limit reached! % 5.39/1.06 % (1619321)------------------------------ % 5.39/1.06 % (1619321)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.39/1.06 % (1619321)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.39/1.06 % (1619321)CaDiCaL version: 2.1.3 % 5.39/1.06 % (1619321)Termination reason: Instruction limit % 5.39/1.06 % (1619321)Termination phase: Saturation % 5.39/1.06 % (1619321)Time elapsed: 0.067 s % 5.39/1.06 % (1619321)Peak memory usage: 13 MB % 5.39/1.06 % (1619321)Instructions burned: 132 (million) % 5.39/1.06 % (1619333)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 5.39/1.06 % (1619333)Terminated due to inappropriate strategy. % 5.39/1.06 % (1619333)------------------------------ % 5.39/1.06 % (1619333)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.39/1.06 % (1619333)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.39/1.06 % (1619333)CaDiCaL version: 2.1.3 % 5.39/1.06 % (1619333)Termination reason: Inappropriate % 5.39/1.06 % (1619333)Time elapsed: 0.012 s % 5.39/1.06 % (1619333)Peak memory usage: 11 MB % 5.39/1.06 % (1619333)Instructions burned: 12 (million) % 5.39/1.06 % (1619333)------------------------------ % 5.39/1.06 % (1619333)------------------------------ % 5.39/1.06 % (1619337)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=561316146:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 5.39/1.06 % (1619340)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=467192086:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 5.39/1.06 % (1619319)Instruction limit reached! % 5.39/1.06 % (1619319)------------------------------ % 5.39/1.06 % (1619319)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.39/1.06 % (1619319)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.39/1.06 % (1619319)CaDiCaL version: 2.1.3 % 5.39/1.06 % (1619319)Termination reason: Instruction limit % 5.39/1.06 % (1619319)Termination phase: Saturation % 5.39/1.06 % (1619319)Time elapsed: 0.105 s % 5.39/1.06 % (1619319)Peak memory usage: 13 MB % 5.39/1.06 % (1619319)Instructions burned: 103 (million) % 5.39/1.06 % (1619320)Instruction limit reached! % 5.39/1.06 % (1619320)------------------------------ % 5.39/1.06 % (1619320)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.20/1.66 % (1619320)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.20/1.66 % (1619320)CaDiCaL version: 2.1.3 % 8.20/1.66 % (1619320)Termination reason: Instruction limit % 8.20/1.66 % (1619320)Termination phase: Saturation % 8.20/1.66 % (1619320)Time elapsed: 0.121 s % 8.20/1.66 % (1619320)Peak memory usage: 13 MB % 8.20/1.66 % (1619320)Instructions burned: 116 (million) % 8.20/1.66 % (1619337)Instruction limit reached! % 8.20/1.66 % (1619337)------------------------------ % 8.20/1.66 % (1619337)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.20/1.66 % (1619337)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.20/1.66 % (1619337)CaDiCaL version: 2.1.3 % 8.20/1.66 % (1619337)Termination reason: Instruction limit % 8.20/1.66 % (1619337)Termination phase: Saturation % 8.20/1.66 % (1619337)Time elapsed: 0.068 s % 8.20/1.66 % (1619337)Peak memory usage: 13 MB % 8.20/1.66 % (1619337)Instructions burned: 131 (million) % 8.20/1.66 % (1619346)ott-21_1_sil=16000:fs=off:random_seed=1992815834:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 8.20/1.66 % (1619350)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1139654862:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 8.20/1.66 % (1619348)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3182312999:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 8.20/1.66 % (1619350)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 8.20/1.66 % (1619350)Terminated due to inappropriate strategy. % 8.20/1.66 % (1619350)------------------------------ % 8.20/1.66 % (1619350)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.20/1.66 % (1619350)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.20/1.66 % (1619350)CaDiCaL version: 2.1.3 % 8.20/1.66 % (1619350)Termination reason: Inappropriate % 8.20/1.66 % (1619350)Time elapsed: 0.003 s % 8.20/1.66 % (1619350)Peak memory usage: 10 MB % 8.20/1.66 % (1619350)Instructions burned: 12 (million) % 8.20/1.66 % (1619350)------------------------------ % 8.20/1.66 % (1619350)------------------------------ % 8.20/1.66 % (1619322)Instruction limit reached! % 8.20/1.66 % (1619322)------------------------------ % 8.20/1.66 % (1619322)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.20/1.66 % (1619322)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.20/1.66 % (1619322)CaDiCaL version: 2.1.3 % 8.20/1.66 % (1619322)Termination reason: Instruction limit % 8.20/1.66 % (1619322)Termination phase: Saturation % 8.20/1.66 % (1619322)Time elapsed: 0.160 s % 8.20/1.66 % (1619322)Peak memory usage: 14 MB % 8.20/1.66 % (1619322)Instructions burned: 159 (million) % 8.20/1.66 % (1619355)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2927600030:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 8.20/1.66 % (1619356)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=328183672:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 8.20/1.66 % (1619356)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 8.20/1.66 % (1619356)Terminated due to inappropriate strategy. % 8.20/1.66 % (1619356)------------------------------ % 8.20/1.66 % (1619356)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.20/1.66 % (1619356)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.20/1.66 % (1619356)CaDiCaL version: 2.1.3 % 8.20/1.66 % (1619356)Termination reason: Inappropriate % 8.20/1.66 % (1619356)Time elapsed: 0.012 s % 8.20/1.66 % (1619356)Peak memory usage: 10 MB % 8.20/1.66 % (1619356)Instructions burned: 12 (million) % 8.20/1.66 % (1619356)------------------------------ % 8.20/1.66 % (1619356)------------------------------ % 8.20/1.66 % (1619360)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=2428206525:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2997 on theBenchmark for (2997ds/692Mi) % 8.20/1.66 % (1619346)Instruction limit reached! % 8.20/1.66 % (1619346)------------------------------ % 8.20/1.66 % (1619346)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.20/1.66 % (1619346)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.20/1.66 % (1619346)CaDiCaL version: 2.1.3 % 8.20/1.66 % (1619346)Termination reason: Instruction limit % 8.20/1.66 % (1619346)Termination phase: Saturation % 32.49/4.96 % (1619346)Time elapsed: 0.169 s % 32.49/4.96 % (1619346)Peak memory usage: 13 MB % 32.49/4.96 % (1619346)Instructions burned: 180 (million) % 32.49/4.96 % (1619362)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=396595108:i=879:kws=inv_precedence:fsr=off_2996 on theBenchmark for (2996ds/879Mi) % 32.49/4.96 % (1619360)Instruction limit reached! % 32.49/4.96 % (1619360)------------------------------ % 32.49/4.96 % (1619360)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 32.49/4.96 % (1619360)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.49/4.96 % (1619360)CaDiCaL version: 2.1.3 % 32.49/4.96 % (1619360)Termination reason: Instruction limit % 32.49/4.96 % (1619360)Termination phase: Saturation % 32.49/4.96 % (1619360)Time elapsed: 0.349 s % 32.49/4.96 % (1619360)Peak memory usage: 21 MB % 32.49/4.96 % (1619360)Instructions burned: 694 (million) % 32.49/4.96 % (1619364)fmb+10_1_sil=64000:random_seed=1072334450:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi) % 32.49/4.96 % (1619364)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 32.49/4.96 % (1619364)Terminated due to inappropriate strategy. % 32.49/4.96 % (1619364)------------------------------ % 32.49/4.96 % (1619364)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 32.49/4.96 % (1619364)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.49/4.96 % (1619364)CaDiCaL version: 2.1.3 % 32.49/4.96 % (1619364)Termination reason: Inappropriate % 32.49/4.96 % (1619364)Time elapsed: 0.010 s % 32.49/4.96 % (1619364)Peak memory usage: 11 MB % 32.49/4.96 % (1619364)Instructions burned: 13 (million) % 32.49/4.96 % (1619364)------------------------------ % 32.49/4.96 % (1619364)------------------------------ % 32.49/4.96 % (1619366)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=428940156:i=9515:nm=5_2993 on theBenchmark for (2993ds/9515Mi) % 32.49/4.96 % (1619366)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 32.49/4.96 % (1619366)Terminated due to inappropriate strategy. % 32.49/4.96 % (1619366)------------------------------ % 32.49/4.96 % (1619366)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 32.49/4.96 % (1619366)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.49/4.96 % (1619366)CaDiCaL version: 2.1.3 % 32.49/4.96 % (1619366)Termination reason: Inappropriate % 32.49/4.96 % (1619366)Time elapsed: 0.008 s % 32.49/4.96 % (1619366)Peak memory usage: 11 MB % 32.49/4.96 % (1619366)Instructions burned: 12 (million) % 32.49/4.96 % (1619366)------------------------------ % 32.49/4.96 % (1619366)------------------------------ % 32.49/4.96 % (1619348)Instruction limit reached! % 32.49/4.96 % (1619348)------------------------------ % 32.49/4.96 % (1619348)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 32.49/4.96 % (1619348)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.49/4.96 % (1619348)CaDiCaL version: 2.1.3 % 32.49/4.96 % (1619348)Termination reason: Instruction limit % 32.49/4.96 % (1619348)Termination phase: Saturation % 32.49/4.96 % (1619348)Time elapsed: 0.502 s % 32.49/4.96 % (1619348)Peak memory usage: 14 MB % 32.49/4.96 % (1619348)Instructions burned: 477 (million) % 32.49/4.96 % (1619368)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1838075029:fmbsr=1.7:i=920_2993 on theBenchmark for (2993ds/920Mi) % 32.49/4.96 % (1619368)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 32.49/4.96 % (1619368)Terminated due to inappropriate strategy. % 32.49/4.96 % (1619368)------------------------------ % 32.49/4.96 % (1619368)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 32.49/4.96 % (1619368)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.49/4.96 % (1619368)CaDiCaL version: 2.1.3 % 32.49/4.96 % (1619368)Termination reason: Inappropriate % 32.49/4.96 % (1619368)Time elapsed: 0.006 s % 32.49/4.96 % (1619368)Peak memory usage: 11 MB % 32.49/4.96 % (1619368)Instructions burned: 12 (million) % 32.49/4.96 % (1619368)------------------------------ % 32.49/4.96 % (1619368)------------------------------ % 32.49/4.96 % (1619369)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1049172270:i=5131_2993 on theBenchmark for (2993ds/5131Mi) % 32.49/4.96 % (1619371)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3756558696:i=1472:ins=7:fdi=8:gsp=on_2992 on theBenchmark for (2992ds/1472Mi) % 32.49/4.96 % (1619340)Instruction limit reached! % 32.49/4.96 % (1619340)------------------------------ % 42.77/6.39 % (1619340)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 42.77/6.39 % (1619340)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.77/6.39 % (1619340)CaDiCaL version: 2.1.3 % 42.77/6.39 % (1619340)Termination reason: Instruction limit % 42.77/6.39 % (1619340)Termination phase: Saturation % 42.77/6.39 % (1619340)Time elapsed: 0.631 s % 42.77/6.39 % (1619340)Peak memory usage: 17 MB % 42.77/6.39 % (1619340)Instructions burned: 684 (million) % 42.77/6.39 % (1619374)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2423556836:i=6324_2992 on theBenchmark for (2992ds/6324Mi) % 42.77/6.39 % (1619374)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 42.77/6.39 % (1619374)Terminated due to inappropriate strategy. % 42.77/6.39 % (1619374)------------------------------ % 42.77/6.39 % (1619374)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 42.77/6.39 % (1619374)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.77/6.39 % (1619374)CaDiCaL version: 2.1.3 % 42.77/6.39 % (1619374)Termination reason: Inappropriate % 42.77/6.39 % (1619374)Time elapsed: 0.010 s % 42.77/6.39 % (1619374)Peak memory usage: 11 MB % 42.77/6.39 % (1619374)Instructions burned: 15 (million) % 42.77/6.39 % (1619374)------------------------------ % 42.77/6.39 % (1619374)------------------------------ % 42.77/6.39 % (1619376)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=100882247:fmbsr=2.30978:i=2174_2992 on theBenchmark for (2992ds/2174Mi) % 42.77/6.39 % (1619376)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 42.77/6.39 % (1619376)Terminated due to inappropriate strategy. % 42.77/6.39 % (1619376)------------------------------ % 42.77/6.39 % (1619376)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 42.77/6.39 % (1619376)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.77/6.39 % (1619376)CaDiCaL version: 2.1.3 % 42.77/6.39 % (1619376)Termination reason: Inappropriate % 42.77/6.39 % (1619376)Time elapsed: 0.008 s % 42.77/6.39 % (1619376)Peak memory usage: 11 MB % 42.77/6.39 % (1619376)Instructions burned: 12 (million) % 42.77/6.39 % (1619376)------------------------------ % 42.77/6.39 % (1619376)------------------------------ % 42.77/6.39 % (1619378)ott-2_1_sil=16000:newcnf=on:random_seed=802658016:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2991 on theBenchmark for (2991ds/869Mi) % 42.77/6.39 % (1619362)Instruction limit reached! % 42.77/6.39 % (1619362)------------------------------ % 42.77/6.39 % (1619362)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 42.77/6.39 % (1619362)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.77/6.39 % (1619362)CaDiCaL version: 2.1.3 % 42.77/6.39 % (1619362)Termination reason: Instruction limit % 42.77/6.39 % (1619362)Termination phase: Saturation % 42.77/6.39 % (1619362)Time elapsed: 0.798 s % 42.77/6.39 % (1619362)Peak memory usage: 19 MB % 42.77/6.39 % (1619362)Instructions burned: 880 (million) % 42.77/6.39 % (1619382)ott+10_1_sil=32000:tgt=ground:random_seed=2889386150:i=5114:av=off_2988 on theBenchmark for (2988ds/5114Mi) % 42.77/6.39 % (1619355)Instruction limit reached! % 42.77/6.39 % (1619355)------------------------------ % 42.77/6.39 % (1619355)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 42.77/6.39 % (1619355)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.77/6.40 % (1619355)CaDiCaL version: 2.1.3 % 42.77/6.40 % (1619355)Termination reason: Instruction limit % 42.77/6.40 % (1619355)Termination phase: Saturation % 42.77/6.40 % (1619355)Time elapsed: 1.112 s % 42.77/6.40 % (1619355)Peak memory usage: 20 MB % 42.77/6.40 % (1619355)Instructions burned: 1180 (million) % 42.77/6.40 % (1619384)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1166539216:i=54282_2986 on theBenchmark for (2986ds/54282Mi) % 42.77/6.40 % (1619384)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 42.77/6.40 % (1619384)Terminated due to inappropriate strategy. % 42.77/6.40 % (1619384)------------------------------ % 42.77/6.40 % (1619384)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 42.77/6.40 % (1619384)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.77/6.40 % (1619384)CaDiCaL version: 2.1.3 % 42.77/6.40 % (1619384)Termination reason: Inappropriate % 42.77/6.40 % (1619384)Time elapsed: 0.011 s % 42.77/6.40 % (1619384)Peak memory usage: 11 MB % 42.77/6.40 % (1619384)Instructions burned: 15 (million) % 169.70/24.16 % (1619384)------------------------------ % 169.70/24.16 % (1619384)------------------------------ % 169.70/24.16 % (1619386)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1440117049:i=3512:aac=none_2986 on theBenchmark for (2986ds/3512Mi) % 169.70/24.16 % (1619378)Instruction limit reached! % 169.70/24.16 % (1619378)------------------------------ % 169.70/24.16 % (1619378)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 169.70/24.16 % (1619378)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.70/24.16 % (1619378)CaDiCaL version: 2.1.3 % 169.70/24.16 % (1619378)Termination reason: Instruction limit % 169.70/24.16 % (1619378)Termination phase: Saturation % 169.70/24.16 % (1619378)Time elapsed: 0.874 s % 169.70/24.16 % (1619378)Peak memory usage: 18 MB % 169.70/24.16 % (1619378)Instructions burned: 869 (million) % 169.70/24.16 % (1619388)dis+21_1_sil=32000:sas=cadical:random_seed=1937851685:i=3773:amm=off_2982 on theBenchmark for (2982ds/3773Mi) % 169.70/24.16 % (1619371)Instruction limit reached! % 169.70/24.16 % (1619371)------------------------------ % 169.70/24.16 % (1619371)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 169.70/24.16 % (1619371)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.70/24.16 % (1619371)CaDiCaL version: 2.1.3 % 169.70/24.16 % (1619371)Termination reason: Instruction limit % 169.70/24.16 % (1619371)Termination phase: Saturation % 169.70/24.16 % (1619371)Time elapsed: 1.338 s % 169.70/24.16 % (1619371)Peak memory usage: 27 MB % 169.70/24.16 % (1619371)Instructions burned: 1473 (million) % 169.70/24.16 % (1619390)ott+11_1_sil=16000:gs=on:random_seed=912524931:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2979 on theBenchmark for (2979ds/2251Mi) % 169.70/24.16 % (1619369)Instruction limit reached! % 169.70/24.16 % (1619369)------------------------------ % 169.70/24.16 % (1619369)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 169.70/24.16 % (1619369)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.70/24.16 % (1619369)CaDiCaL version: 2.1.3 % 169.70/24.16 % (1619369)Termination reason: Instruction limit % 169.70/24.16 % (1619369)Termination phase: Saturation % 169.70/24.16 % (1619369)Time elapsed: 2.570 s % 169.70/24.16 % (1619369)Peak memory usage: 37 MB % 169.70/24.16 % (1619369)Instructions burned: 5133 (million) % 169.70/24.16 % (1619392)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2957505972:fmbsr=1.6:i=67534_2967 on theBenchmark for (2967ds/67534Mi) % 169.70/24.16 % (1619392)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 169.70/24.16 % (1619392)Terminated due to inappropriate strategy. % 169.70/24.16 % (1619392)------------------------------ % 169.70/24.16 % (1619392)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 169.70/24.16 % (1619392)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.70/24.16 % (1619392)CaDiCaL version: 2.1.3 % 169.70/24.16 % (1619392)Termination reason: Inappropriate % 169.70/24.16 % (1619392)Time elapsed: 0.006 s % 169.70/24.16 % (1619392)Peak memory usage: 11 MB % 169.70/24.16 % (1619392)Instructions burned: 12 (million) % 169.70/24.16 % (1619392)------------------------------ % 169.70/24.16 % (1619392)------------------------------ % 169.70/24.16 % (1619394)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=4144236137:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2966 on theBenchmark for (2966ds/4591Mi) % 169.70/24.16 % (1619390)Instruction limit reached! % 169.70/24.16 % (1619390)------------------------------ % 169.70/24.16 % (1619390)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 169.70/24.16 % (1619390)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.70/24.16 % (1619390)CaDiCaL version: 2.1.3 % 169.70/24.16 % (1619390)Termination reason: Instruction limit % 169.70/24.16 % (1619390)Termination phase: Saturation % 169.70/24.16 % (1619390)Time elapsed: 2.133 s % 169.70/24.16 % (1619390)Peak memory usage: 20 MB % 169.70/24.16 % (1619390)Instructions burned: 2252 (million) % 169.70/24.16 % (1619396)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1619398705:i=29340_2957 on theBenchmark for (2957ds/29340Mi) % 169.70/24.16 % (1619386)Instruction limit reached! % 169.70/24.16 % (1619386)------------------------------ % 169.70/24.16 % (1619386)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 169.70/24.16 % (1619386)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.70/24.16 % (1619386)CaDiCaL version: 2.1.3 % 169.70/24.16 % (1619386)Termination reason: Instruction limit % 201.77/28.74 % (1619386)Termination phase: Saturation % 201.77/28.74 % (1619386)Time elapsed: 3.280 s % 201.77/28.74 % (1619386)Peak memory usage: 33 MB % 201.77/28.74 % (1619386)Instructions burned: 3512 (million) % 201.77/28.74 % (1619398)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=351944226:i=5211_2953 on theBenchmark for (2953ds/5211Mi) % 201.77/28.74 % (1619388)Instruction limit reached! % 201.77/28.74 % (1619388)------------------------------ % 201.77/28.74 % (1619388)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 201.77/28.74 % (1619388)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 201.77/28.74 % (1619388)CaDiCaL version: 2.1.3 % 201.77/28.74 % (1619388)Termination reason: Instruction limit % 201.77/28.74 % (1619388)Termination phase: Saturation % 201.77/28.74 % (1619388)Time elapsed: 3.609 s % 201.77/28.74 % (1619388)Peak memory usage: 34 MB % 201.77/28.74 % (1619388)Instructions burned: 3773 (million) % 201.77/28.74 % (1619400)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2925367867:i=5497:nm=2_2946 on theBenchmark for (2946ds/5497Mi) % 201.77/28.74 % (1619400)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 201.77/28.74 % (1619400)Terminated due to inappropriate strategy. % 201.77/28.74 % (1619400)------------------------------ % 201.77/28.74 % (1619400)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 201.77/28.74 % (1619400)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 201.77/28.74 % (1619400)CaDiCaL version: 2.1.3 % 201.77/28.74 % (1619400)Termination reason: Inappropriate % 201.77/28.74 % (1619400)Time elapsed: 0.011 s % 201.77/28.74 % (1619400)Peak memory usage: 11 MB % 201.77/28.74 % (1619400)Instructions burned: 14 (million) % 201.77/28.74 % (1619400)------------------------------ % 201.77/28.74 % (1619400)------------------------------ % 201.77/28.74 % (1619402)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=2772718793:fmbsr=2:i=46332_2945 on theBenchmark for (2945ds/46332Mi) % 201.77/28.74 % (1619402)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 201.77/28.74 % (1619402)Terminated due to inappropriate strategy. % 201.77/28.74 % (1619402)------------------------------ % 201.77/28.74 % (1619402)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 201.77/28.74 % (1619402)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 201.77/28.74 % (1619402)CaDiCaL version: 2.1.3 % 201.77/28.74 % (1619402)Termination reason: Inappropriate % 201.77/28.74 % (1619402)Time elapsed: 0.007 s % 201.77/28.74 % (1619402)Peak memory usage: 11 MB % 201.77/28.74 % (1619402)Instructions burned: 12 (million) % 201.77/28.74 % (1619402)------------------------------ % 201.77/28.74 % (1619402)------------------------------ % 201.77/28.74 % (1619404)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=2233033174:i=14071_2945 on theBenchmark for (2945ds/14071Mi) % 201.77/28.74 % (1619404)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 201.77/28.74 % (1619404)Terminated due to inappropriate strategy. % 201.77/28.74 % (1619404)------------------------------ % 201.77/28.74 % (1619404)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 201.77/28.74 % (1619404)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 201.77/28.74 % (1619404)CaDiCaL version: 2.1.3 % 201.77/28.74 % (1619404)Termination reason: Inappropriate % 201.77/28.74 % (1619404)Time elapsed: 0.007 s % 201.77/28.74 % (1619404)Peak memory usage: 11 MB % 201.77/28.74 % (1619404)Instructions burned: 12 (million) % 201.77/28.74 % (1619404)------------------------------ % 201.77/28.74 % (1619404)------------------------------ % 201.77/28.74 % (1619406)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1276480400:i=22565:add=on:rawr=on_2945 on theBenchmark for (2945ds/22565Mi) % 201.77/28.74 % (1619394)Instruction limit reached! % 201.77/28.74 % (1619394)------------------------------ % 201.77/28.74 % (1619394)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 201.77/28.74 % (1619394)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 201.77/28.74 % (1619394)CaDiCaL version: 2.1.3 % 201.77/28.74 % (1619394)Termination reason: Instruction limit % 201.77/28.74 % (1619394)Termination phase: Saturation % 201.77/28.74 % (1619394)Time elapsed: 2.228 s % 201.77/28.74 % (1619394)Peak memory usage: 46 MB % 201.77/28.74 % (1619394)Instructions burned: 4591 (million) % 201.77/28.74 % (1619408)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=2856537087:i=8173:av=off_2944 on theBenchmark for (2944ds/8173Mi) % 201.77/28.74 % (1619382)Instruction limit reached! % 202.28/28.88 % (1619382)------------------------------ % 202.28/28.88 % (1619382)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 202.28/28.88 % (1619382)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.28/28.88 % (1619382)CaDiCaL version: 2.1.3 % 202.28/28.88 % (1619382)Termination reason: Instruction limit % 202.28/28.88 % (1619382)Termination phase: Saturation % 202.28/28.88 % (1619382)Time elapsed: 4.879 s % 202.28/28.88 % (1619382)Peak memory usage: 44 MB % 202.28/28.88 % (1619382)Instructions burned: 5114 (million) % 202.28/28.88 % (1619410)dis+10_16:1_sil=16000:random_seed=2743866136:i=9155:fsr=off_2938 on theBenchmark for (2938ds/9155Mi) % 202.28/28.88 % (1619398)Instruction limit reached! % 202.28/28.88 % (1619398)------------------------------ % 202.28/28.88 % (1619398)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 202.28/28.88 % (1619398)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.28/28.88 % (1619398)CaDiCaL version: 2.1.3 % 202.28/28.88 % (1619398)Termination reason: Instruction limit % 202.28/28.88 % (1619398)Termination phase: Saturation % 202.28/28.88 % (1619398)Time elapsed: 4.412 s % 202.28/28.88 % (1619398)Peak memory usage: 37 MB % 202.28/28.88 % (1619398)Instructions burned: 5211 (million) % 202.28/28.88 % (1619416)ott-3_8_sil=64000:random_seed=218554864:i=20139:bs=on_2908 on theBenchmark for (2908ds/20139Mi) % 202.28/28.88 % (1619408)Instruction limit reached! % 202.28/28.88 % (1619408)------------------------------ % 202.28/28.88 % (1619408)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 202.28/28.88 % (1619408)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.28/28.88 % (1619408)CaDiCaL version: 2.1.3 % 202.28/28.88 % (1619408)Termination reason: Instruction limit % 202.28/28.88 % (1619408)Termination phase: Saturation % 202.28/28.88 % (1619408)Time elapsed: 4.507 s % 202.28/28.88 % (1619408)Peak memory usage: 95 MB % 202.28/28.88 % (1619408)Instructions burned: 8176 (million) % 202.28/28.88 % (1619426)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=3221410154:fmbsr=2:i=32576_2898 on theBenchmark for (2898ds/32576Mi) % 202.28/28.88 % (1619426)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 202.28/28.88 % (1619426)Terminated due to inappropriate strategy. % 202.28/28.88 % (1619426)------------------------------ % 202.28/28.88 % (1619426)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 202.28/28.88 % (1619426)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.28/28.88 % (1619426)CaDiCaL version: 2.1.3 % 202.28/28.88 % (1619426)Termination reason: Inappropriate % 202.28/28.88 % (1619426)Time elapsed: 0.014 s % 202.28/28.88 % (1619426)Peak memory usage: 11 MB % 202.28/28.88 % (1619426)Instructions burned: 16 (million) % 202.28/28.88 % (1619426)------------------------------ % 202.28/28.88 % (1619426)------------------------------ % 202.28/28.88 % (1619429)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=3919856685:i=11404_2898 on theBenchmark for (2898ds/11404Mi) % 202.28/28.88 % (1619410)Instruction limit reached! % 202.28/28.88 % (1619410)------------------------------ % 202.28/28.88 % (1619410)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 202.28/28.88 % (1619410)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.28/28.88 % (1619410)CaDiCaL version: 2.1.3 % 202.28/28.88 % (1619410)Termination reason: Instruction limit % 202.28/28.88 % (1619410)Termination phase: Saturation % 202.28/28.88 % (1619410)Time elapsed: 8.261 s % 202.28/28.88 % (1619410)Peak memory usage: 56 MB % 202.28/28.88 % (1619410)Instructions burned: 9156 (million) % 202.28/28.88 % (1619440)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=389243375:i=14134_2855 on theBenchmark for (2855ds/14134Mi) % 202.28/28.88 % (1619429)Instruction limit reached! % 202.28/28.88 % (1619429)------------------------------ % 202.28/28.88 % (1619429)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 202.28/28.88 % (1619429)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.28/28.88 % (1619429)CaDiCaL version: 2.1.3 % 202.28/28.88 % (1619429)Termination reason: Instruction limit % 202.28/28.88 % (1619429)Termination phase: Saturation % 202.28/28.88 % (1619429)Time elapsed: 6.327 s % 202.28/28.88 % (1619429)Peak memory usage: 81 MB % 202.28/28.88 % (1619429)Instructions burned: 11405 (million) % 202.28/28.88 % (1619448)dis+33_16_sil=32000:sac=on:random_seed=2925120129:i=15851:nm=0_2834 on theBenchmark for (2834ds/15851Mi) % 202.28/28.88 % (1619448)Instruction limit reached! % 202.28/28.88 % (1619448)------------------------------ % 202.28/28.88 % (1619448)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 216.35/30.70 % (1619448)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 216.35/30.70 % (1619448)CaDiCaL version: 2.1.3 % 216.35/30.70 % (1619448)Termination reason: Instruction limit % 216.35/30.70 % (1619448)Termination phase: Saturation % 216.35/30.70 % (1619448)Time elapsed: 7.313 s % 216.35/30.70 % (1619448)Peak memory usage: 84 MB % 216.35/30.70 % (1619448)Instructions burned: 15854 (million) % 216.35/30.70 % (1619469)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=4122550972:avsq=on:i=17627:add=on:amm=off_2761 on theBenchmark for (2761ds/17627Mi) % 216.35/30.70 % (1619440)Instruction limit reached! % 216.35/30.70 % (1619440)------------------------------ % 216.35/30.70 % (1619440)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 216.35/30.70 % (1619440)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 216.35/30.70 % (1619440)CaDiCaL version: 2.1.3 % 216.35/30.70 % (1619440)Termination reason: Instruction limit % 216.35/30.70 % (1619440)Termination phase: Saturation % 216.35/30.70 % (1619440)Time elapsed: 13.589 s % 216.35/30.70 % (1619440)Peak memory usage: 87 MB % 216.35/30.70 % (1619440)Instructions burned: 14135 (million) % 216.35/30.70 % (1619582)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=3833838707:s2a=on:i=53295_2719 on theBenchmark for (2719ds/53295Mi) % 216.35/30.70 % (1619396)Instruction limit reached! % 216.35/30.70 % (1619396)------------------------------ % 216.35/30.70 % (1619396)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 216.35/30.70 % (1619396)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 216.35/30.70 % (1619396)CaDiCaL version: 2.1.3 % 216.35/30.70 % (1619396)Termination reason: Instruction limit % 216.35/30.70 % (1619396)Termination phase: Saturation % 216.35/30.70 % (1619396)Time elapsed: 24.067 s % 216.35/30.70 % (1619396)Peak memory usage: 143 MB % 216.35/30.70 % (1619396)Instructions burned: 29340 (million) % 216.35/30.70 % (1619416)Instruction limit reached! % 216.35/30.70 % (1619416)------------------------------ % 216.35/30.70 % (1619416)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 216.35/30.70 % (1619416)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 216.35/30.70 % (1619416)CaDiCaL version: 2.1.3 % 216.35/30.70 % (1619416)Termination reason: Instruction limit % 216.35/30.70 % (1619416)Termination phase: Saturation % 216.35/30.70 % (1619416)Time elapsed: 19.209 s % 216.35/30.70 % (1619416)Peak memory usage: 91 MB % 216.35/30.70 % (1619416)Instructions burned: 20140 (million) % 216.35/30.70 % (1619631)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=2241998507:i=26857:ins=20_2716 on theBenchmark for (2716ds/26857Mi) % 216.35/30.70 % (1619632)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=423472066:i=28120:bs=on:fsr=off_2716 on theBenchmark for (2716ds/28120Mi) % 216.35/30.70 % (1619631)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 216.35/30.70 % (1619631)Terminated due to inappropriate strategy. % 216.35/30.70 % (1619631)------------------------------ % 216.35/30.70 % (1619631)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 216.35/30.70 % (1619631)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 216.35/30.70 % (1619631)CaDiCaL version: 2.1.3 % 216.35/30.70 % (1619631)Termination reason: Inappropriate % 216.35/30.70 % (1619631)Time elapsed: 0.006 s % 216.35/30.70 % (1619631)Peak memory usage: 11 MB % 216.35/30.70 % (1619631)Instructions burned: 12 (million) % 216.35/30.70 % (1619631)------------------------------ % 216.35/30.70 % (1619631)------------------------------ % 216.35/30.70 % (1619635)fmb+10_1_sil=256000:fmbss=7:random_seed=1596094517:fmbsr=1.6:i=182295_2716 on theBenchmark for (2716ds/182295Mi) % 216.35/30.70 % (1619635)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 216.35/30.70 % (1619635)Terminated due to inappropriate strategy. % 216.35/30.70 % (1619635)------------------------------ % 216.35/30.70 % (1619635)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 216.35/30.70 % (1619635)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 216.35/30.70 % (1619635)CaDiCaL version: 2.1.3 % 216.35/30.70 % (1619635)Termination reason: Inappropriate % 216.35/30.70 % (1619635)Time elapsed: 0.006 s % 216.35/30.70 % (1619635)Peak memory usage: 11 MB % 216.35/30.70 % (1619635)Instructions burned: 12 (million) % 216.35/30.70 % (1619635)------------------------------ % 216.35/30.70 % (1619635)------------------------------ % 216.35/30.70 % (1619637)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=2380512350:i=44625:gsp=on_2715 on theBenchmark for (2715ds/44625Mi) % 222.48/31.65 % (1619637)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 222.48/31.65 % (1619637)Terminated due to inappropriate strategy. % 222.48/31.65 % (1619637)------------------------------ % 222.48/31.65 % (1619637)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 222.48/31.65 % (1619637)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 222.48/31.65 % (1619637)CaDiCaL version: 2.1.3 % 222.48/31.65 % (1619637)Termination reason: Inappropriate % 222.48/31.65 % (1619637)Time elapsed: 0.007 s % 222.48/31.65 % (1619637)Peak memory usage: 11 MB % 222.48/31.65 % (1619637)Instructions burned: 13 (million) % 222.48/31.65 % (1619637)------------------------------ % 222.48/31.65 % (1619637)------------------------------ % 222.48/31.65 % (1619639)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=3841990617:i=160505_2715 on theBenchmark for (2715ds/160505Mi) % 222.48/31.65 % (1619639)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 222.48/31.65 % (1619639)Terminated due to inappropriate strategy. % 222.48/31.65 % (1619639)------------------------------ % 222.48/31.65 % (1619639)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 222.48/31.65 % (1619639)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 222.48/31.65 % (1619639)CaDiCaL version: 2.1.3 % 222.48/31.65 % (1619639)Termination reason: Inappropriate % 222.48/31.65 % (1619639)Time elapsed: 0.006 s % 222.48/31.65 % (1619639)Peak memory usage: 11 MB % 222.48/31.65 % (1619639)Instructions burned: 12 (million) % 222.48/31.65 % (1619639)------------------------------ % 222.48/31.65 % (1619639)------------------------------ % 222.48/31.65 % (1619641)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=3869782771:fmbsr=1.3:i=225729_2715 on theBenchmark for (2715ds/225729Mi) % 222.48/31.65 % (1619641)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 222.48/31.65 % (1619641)Terminated due to inappropriate strategy. % 222.48/31.65 % (1619641)------------------------------ % 222.48/31.65 % (1619641)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 222.48/31.65 % (1619641)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 222.48/31.65 % (1619641)CaDiCaL version: 2.1.3 % 222.48/31.65 % (1619641)Termination reason: Inappropriate % 222.48/31.65 % (1619641)Time elapsed: 0.006 s % 222.48/31.65 % (1619641)Peak memory usage: 11 MB % 222.48/31.65 % (1619641)Instructions burned: 12 (million) % 222.48/31.65 % (1619641)------------------------------ % 222.48/31.65 % (1619641)------------------------------ % 222.48/31.65 % (1619643)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=1611018958:fmbsr=2:i=185024:ins=7_2714 on theBenchmark for (2714ds/185024Mi) % 222.48/31.65 % (1619643)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 222.48/31.65 % (1619643)Terminated due to inappropriate strategy. % 222.48/31.65 % (1619643)------------------------------ % 222.48/31.65 % (1619643)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 222.48/31.65 % (1619643)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 222.48/31.65 % (1619643)CaDiCaL version: 2.1.3 % 222.48/31.65 % (1619643)Termination reason: Inappropriate % 222.48/31.65 % (1619643)Time elapsed: 0.006 s % 222.48/31.65 % (1619643)Peak memory usage: 11 MB % 222.48/31.65 % (1619643)Instructions burned: 12 (million) % 222.48/31.65 % (1619643)------------------------------ % 222.48/31.65 % (1619643)------------------------------ % 222.48/31.65 % (1619645)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=137798953:rtra=on_2714 on theBenchmark for (2714ds/0Mi) % 222.48/31.65 % (1619645)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 222.48/31.65 % (1619645)Terminated due to inappropriate strategy. % 222.48/31.65 % (1619645)------------------------------ % 222.48/31.65 % (1619645)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 222.48/31.65 % (1619645)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 222.48/31.65 % (1619645)CaDiCaL version: 2.1.3 % 222.48/31.65 % (1619645)Termination reason: Inappropriate % 222.48/31.65 % (1619645)Time elapsed: 0.009 s % 222.48/31.65 % (1619645)Peak memory usage: 11 MB % 222.48/31.65 % (1619645)Instructions burned: 17 (million) % 222.48/31.65 % (1619645)------------------------------ % 222.48/31.65 % (1619645)------------------------------ % 222.48/31.65 % (1619647)% WARNING: option uhcvi not known. % 222.48/31.65 % (1619647)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1770595042:i=271062:add=off:rtra=on:rawr=on_2714 on theBenchmark for (2714ds/271062Mi) % 235.73/33.58 % (1619406)Instruction limit reached! % 235.73/33.58 % (1619406)------------------------------ % 235.73/33.58 % (1619406)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 235.73/33.58 % (1619406)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.73/33.58 % (1619406)CaDiCaL version: 2.1.3 % 235.73/33.58 % (1619406)Termination reason: Instruction limit % 235.73/33.58 % (1619406)Termination phase: Saturation % 235.73/33.58 % (1619406)Time elapsed: 23.424 s % 235.73/33.58 % (1619406)Peak memory usage: 94 MB % 235.73/33.58 % (1619406)Instructions burned: 22565 (million) % 235.73/33.58 % (1619649)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2959394434:i=176048:add=on:rtra=on:rawr=on_2710 on theBenchmark for (2710ds/176048Mi) % 235.73/33.58 % (1619469)Instruction limit reached! % 235.73/33.58 % (1619469)------------------------------ % 235.73/33.58 % (1619469)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 235.73/33.58 % (1619469)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.73/33.58 % (1619469)CaDiCaL version: 2.1.3 % 235.73/33.58 % (1619469)Termination reason: Instruction limit % 235.73/33.58 % (1619469)Termination phase: Saturation % 235.73/33.58 % (1619469)Time elapsed: 6.112 s % 235.73/33.58 % (1619469)Peak memory usage: 62 MB % 235.73/33.58 % (1619469)Instructions burned: 17633 (million) % 235.73/33.58 % (1619651)dis+10_1_sil=32000:si=on:sp=arity:random_seed=1405679643:i=206:fgj=on:rtra=on_2699 on theBenchmark for (2699ds/206Mi) % 235.73/33.58 % (1619651)Instruction limit reached! % 235.73/33.58 % (1619651)------------------------------ % 235.73/33.58 % (1619651)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 235.73/33.58 % (1619651)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.73/33.58 % (1619651)CaDiCaL version: 2.1.3 % 235.73/33.58 % (1619651)Termination reason: Instruction limit % 235.73/33.58 % (1619651)Termination phase: Saturation % 235.73/33.58 % (1619651)Time elapsed: 0.069 s % 235.73/33.58 % (1619651)Peak memory usage: 14 MB % 235.73/33.58 % (1619651)Instructions burned: 207 (million) % 235.73/33.58 % (1619653)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=2669384412:i=232:rtra=on_2699 on theBenchmark for (2699ds/232Mi) % 235.73/33.58 % (1619653)Instruction limit reached! % 235.73/33.58 % (1619653)------------------------------ % 235.73/33.58 % (1619653)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 235.73/33.58 % (1619653)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.73/33.58 % (1619653)CaDiCaL version: 2.1.3 % 235.73/33.58 % (1619653)Termination reason: Instruction limit % 235.73/33.58 % (1619653)Termination phase: Saturation % 235.73/33.58 % (1619653)Time elapsed: 0.079 s % 235.73/33.58 % (1619653)Peak memory usage: 14 MB % 235.73/33.58 % (1619653)Instructions burned: 235 (million) % 235.73/33.58 % (1619655)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=1109678483:i=262:rtra=on_2698 on theBenchmark for (2698ds/262Mi) % 235.73/33.58 % (1619655)Instruction limit reached! % 235.73/33.58 % (1619655)------------------------------ % 235.73/33.58 % (1619655)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 235.73/33.58 % (1619655)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.73/33.58 % (1619655)CaDiCaL version: 2.1.3 % 235.73/33.58 % (1619655)Termination reason: Instruction limit % 235.73/33.58 % (1619655)Termination phase: Saturation % 235.73/33.58 % (1619655)Time elapsed: 0.087 s % 235.73/33.58 % (1619655)Peak memory usage: 14 MB % 235.73/33.58 % (1619655)Instructions burned: 263 (million) % 235.73/33.58 % (1619657)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=3143507776:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2697 on theBenchmark for (2697ds/318Mi) % 235.73/33.58 % (1619657)Instruction limit reached! % 235.73/33.58 % (1619657)------------------------------ % 235.73/33.58 % (1619657)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 235.73/33.58 % (1619657)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.73/33.58 % (1619657)CaDiCaL version: 2.1.3 % 235.73/33.58 % (1619657)Termination reason: Instruction limit % 235.73/33.58 % (1619657)Termination phase: Saturation % 235.73/33.58 % (1619657)Time elapsed: 0.102 s % 235.73/33.58 % (1619657)Peak memory usage: 17 MB % 235.73/33.58 % (1619657)Instructions burned: 318 (million) % 235.73/33.58 % (1619659)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=4142830105:i=1428:nm=2:rtra=on_2696 on theBenchmark for (2696ds/1428Mi) % 260.37/37.03 % (1619659)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 260.37/37.03 % (1619659)Terminated due to inappropriate strategy. % 260.37/37.03 % (1619659)------------------------------ % 260.37/37.03 % (1619659)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 260.37/37.03 % (1619659)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 260.37/37.03 % (1619659)CaDiCaL version: 2.1.3 % 260.37/37.03 % (1619659)Termination reason: Inappropriate % 260.37/37.03 % (1619659)Time elapsed: 0.004 s % 260.37/37.03 % (1619659)Peak memory usage: 11 MB % 260.37/37.03 % (1619659)Instructions burned: 13 (million) % 260.37/37.03 % (1619659)------------------------------ % 260.37/37.03 % (1619659)------------------------------ % 260.37/37.03 % (1619661)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=4136419555:i=262:bd=preordered:rtra=on:fsd=on_2695 on theBenchmark for (2695ds/262Mi) % 260.37/37.03 % (1619661)Instruction limit reached! % 260.37/37.03 % (1619661)------------------------------ % 260.37/37.03 % (1619661)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 260.37/37.03 % (1619661)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 260.37/37.03 % (1619661)CaDiCaL version: 2.1.3 % 260.37/37.03 % (1619661)Termination reason: Instruction limit % 260.37/37.03 % (1619661)Termination phase: Saturation % 260.37/37.03 % (1619661)Time elapsed: 0.091 s % 260.37/37.03 % (1619661)Peak memory usage: 13 MB % 260.37/37.03 % (1619661)Instructions burned: 263 (million) % 260.37/37.03 % (1619663)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=153355193:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2694 on theBenchmark for (2694ds/1368Mi) % 260.37/37.03 % (1619663)Instruction limit reached! % 260.37/37.03 % (1619663)------------------------------ % 260.37/37.03 % (1619663)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 260.37/37.03 % (1619663)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 260.37/37.03 % (1619663)CaDiCaL version: 2.1.3 % 260.37/37.03 % (1619663)Termination reason: Instruction limit % 260.37/37.03 % (1619663)Termination phase: Saturation % 260.37/37.03 % (1619663)Time elapsed: 0.391 s % 260.37/37.03 % (1619663)Peak memory usage: 21 MB % 260.37/37.03 % (1619663)Instructions burned: 1371 (million) % 260.37/37.03 % (1619665)ott-21_1_sil=16000:si=on:fs=off:random_seed=4186596265:i=360:av=off:fsr=off:rtra=on_2690 on theBenchmark for (2690ds/360Mi) % 260.37/37.03 % (1619665)Instruction limit reached! % 260.37/37.03 % (1619665)------------------------------ % 260.37/37.03 % (1619665)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 260.37/37.03 % (1619665)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 260.37/37.03 % (1619665)CaDiCaL version: 2.1.3 % 260.37/37.03 % (1619665)Termination reason: Instruction limit % 260.37/37.03 % (1619665)Termination phase: Saturation % 260.37/37.03 % (1619665)Time elapsed: 0.101 s % 260.37/37.03 % (1619665)Peak memory usage: 14 MB % 260.37/37.03 % (1619665)Instructions burned: 363 (million) % 260.37/37.03 % (1619667)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2249313155:i=954:bd=all:rtra=on_2689 on theBenchmark for (2689ds/954Mi) % 260.37/37.03 % (1619667)Instruction limit reached! % 260.37/37.03 % (1619667)------------------------------ % 260.37/37.03 % (1619667)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 260.37/37.03 % (1619667)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 260.37/37.03 % (1619667)CaDiCaL version: 2.1.3 % 260.37/37.03 % (1619667)Termination reason: Instruction limit % 260.37/37.03 % (1619667)Termination phase: Saturation % 260.37/37.03 % (1619667)Time elapsed: 0.297 s % 260.37/37.03 % (1619667)Peak memory usage: 17 MB % 260.37/37.03 % (1619667)Instructions burned: 954 (million) % 260.37/37.03 % (1619669)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=3711047306:fmbsr=1.3:i=1730:ins=25:rtra=on_2686 on theBenchmark for (2686ds/1730Mi) % 260.37/37.03 % (1619669)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 260.37/37.03 % (1619669)Terminated due to inappropriate strategy. % 260.37/37.03 % (1619669)------------------------------ % 260.37/37.03 % (1619669)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 260.37/37.03 % (1619669)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 260.37/37.03 % (1619669)CaDiCaL version: 2.1.3 % 260.37/37.03 % (1619669)Termination reason: Inappropriate % 297.98/42.29 % (1619669)Time elapsed: 0.004 s % 297.98/42.29 % (1619669)Peak memory usage: 11 MB % 297.98/42.29 % (1619669)Instructions burned: 14 (million) % 297.98/42.29 % (1619669)------------------------------ % 297.98/42.29 % (1619669)------------------------------ % 297.98/42.29 % (1619671)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=902271296:i=2358:rtra=on_2686 on theBenchmark for (2686ds/2358Mi) % 297.98/42.29 % (1619671)Instruction limit reached! % 297.98/42.29 % (1619671)------------------------------ % 297.98/42.29 % (1619671)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 297.98/42.29 % (1619671)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 297.98/42.29 % (1619671)CaDiCaL version: 2.1.3 % 297.98/42.29 % (1619671)Termination reason: Instruction limit % 297.98/42.29 % (1619671)Termination phase: Saturation % 297.98/42.29 % (1619671)Time elapsed: 0.811 s % 297.98/42.29 % (1619671)Peak memory usage: 26 MB % 297.98/42.29 % (1619671)Instructions burned: 2358 (million) % 297.98/42.29 % (1619673)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=371981177:i=1778:ins=1:rtra=on_2678 on theBenchmark for (2678ds/1778Mi) % 297.98/42.29 % (1619673)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 297.98/42.29 % (1619673)Terminated due to inappropriate strategy. % 297.98/42.29 % (1619673)------------------------------ % 297.98/42.29 % (1619673)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 297.98/42.29 % (1619673)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 297.98/42.29 % (1619673)CaDiCaL version: 2.1.3 % 297.98/42.29 % (1619673)Termination reason: Inappropriate % 297.98/42.29 % (1619673)Time elapsed: 0.004 s % 297.98/42.29 % (1619673)Peak memory usage: 11 MB % 297.98/42.29 % (1619673)Instructions burned: 13 (million) % 297.98/42.29 % (1619673)------------------------------ % 297.98/42.29 % (1619673)------------------------------ % 297.98/42.29 % (1619675)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=526749873:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2678 on theBenchmark for (2678ds/1384Mi) % 297.98/42.29 % (1619675)Instruction limit reached! % 297.98/42.29 % (1619675)------------------------------ % 297.98/42.29 % (1619675)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 297.98/42.29 % (1619675)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 297.98/42.29 % (1619675)CaDiCaL version: 2.1.3 % 297.98/42.29 % (1619675)Termination reason: Instruction limit % 297.98/42.29 % (1619675)Termination phase: Saturation % 297.98/42.29 % (1619675)Time elapsed: 0.494 s % 297.98/42.29 % (1619675)Peak memory usage: 30 MB % 297.98/42.29 % (1619675)Instructions burned: 1387 (million) % 297.98/42.29 % (1619677)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=2675379376:i=1758:kws=inv_precedence:fsr=off:rtra=on_2672 on theBenchmark for (2672ds/1758Mi) % 297.98/42.29 % (1619677)Instruction limit reached! % 297.98/42.29 % (1619677)------------------------------ % 297.98/42.29 % (1619677)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 297.98/42.29 % (1619677)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 297.98/42.29 % (1619677)CaDiCaL version: 2.1.3 % 297.98/42.29 % (1619677)Termination reason: Instruction limit % 297.98/42.29 % (1619677)Termination phase: Saturation % 297.98/42.29 % (1619677)Time elapsed: 0.541 s % 297.98/42.29 % (1619677)Peak memory usage: 25 MB % 297.98/42.29 % (1619677)Instructions burned: 1759 (million) % 297.98/42.29 % (1619679)fmb+10_1_sil=64000:si=on:random_seed=2457006848:i=44122:nm=2:rtra=on:gsp=on_2667 on theBenchmark for (2667ds/44122Mi) % 297.98/42.29 % (1619679)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 297.98/42.29 % (1619679)Terminated due to inappropriate strategy. % 297.98/42.29 % (1619679)------------------------------ % 297.98/42.29 % (1619679)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 297.98/42.29 % (1619679)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 297.98/42.29 % (1619679)CaDiCaL version: 2.1.3 % 297.98/42.29 % (1619679)Termination reason: Inappropriate % 297.98/42.29 % (1619679)Time elapsed: 0.004 s % 297.98/42.29 % (1619679)Peak memory usage: 11 MB % 297.98/42.29 % (1619679)Instructions burned: 15 (million) % 297.98/42.29 % (1619679)------------------------------ % 297.98/42.29 % (1619679)------------------------------ % 297.98/42.29 % (1619681)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=1848018052:i=19030:nm=5:rtra=on_2667 on theBenchmark for (2667ds/19030Mi) % 300.50/42.63 % (1619681)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.50/42.63 % (1619681)Terminated due to inappropriate strategy. % 300.50/42.63 % (1619681)------------------------------ % 300.50/42.63 % (1619681)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.50/42.63 % (1619681)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.50/42.63 % (1619681)CaDiCaL version: 2.1.3 % 300.50/42.63 % (1619681)Termination reason: Inappropriate % 300.50/42.63 % (1619681)Time elapsed: 0.004 s % 300.50/42.63 % (1619681)Peak memory usage: 11 MB % 300.50/42.63 % (1619681)Instructions burned: 13 (million) % 300.50/42.63 % (1619681)------------------------------ % 300.50/42.63 % (1619681)------------------------------ % 300.50/42.63 % (1619683)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=1774397217:fmbsr=1.7:i=1840:rtra=on_2667 on theBenchmark for (2667ds/1840Mi) % 300.50/42.63 % (1619683)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.50/42.63 % (1619683)Terminated due to inappropriate strategy. % 300.50/42.63 % (1619683)------------------------------ % 300.50/42.63 % (1619683)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.50/42.63 % (1619683)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.50/42.63 % (1619683)CaDiCaL version: 2.1.3 % 300.50/42.63 % (1619683)Termination reason: Inappropriate % 300.50/42.63 % (1619683)Time elapsed: 0.004 s % 300.50/42.63 % (1619683)Peak memory usage: 11 MB % 300.50/42.63 % (1619683)Instructions burned: 13 (million) % 300.50/42.63 % (1619683)------------------------------ % 300.50/42.63 % (1619683)------------------------------ % 300.50/42.63 % (1619685)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=2485722547:i=10262:rtra=on_2666 on theBenchmark for (2666ds/10262Mi) % 300.50/42.63 % (1619685)Instruction limit reached! % 300.50/42.63 % (1619685)------------------------------ % 300.50/42.63 % (1619685)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.50/42.63 % (1619685)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.50/42.63 % (1619685)CaDiCaL version: 2.1.3 % 300.50/42.63 % (1619685)Termination reason: Instruction limit % 300.50/42.63 % (1619685)Termination phase: Saturation % 300.50/42.63 % (1619685)Time elapsed: 3.268 s % 300.50/42.63 % (1619685)Peak memory usage: 56 MB % 300.50/42.63 % (1619685)Instructions burned: 10264 (million) % 300.50/42.63 % (1619687)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=4090803366:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2634 on theBenchmark for (2634ds/2944Mi) % 300.50/42.63 % (1619632)Instruction limit reached! % 300.50/42.63 % (1619632)------------------------------ % 300.50/42.63 % (1619632)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.50/42.63 % (1619632)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.50/42.63 % (1619632)CaDiCaL version: 2.1.3 % 300.50/42.63 % (1619632)Termination reason: Instruction limit % 300.50/42.63 % (1619632)Termination phase: Saturation % 300.50/42.63 % (1619632)Time elapsed: 8.284 s % 300.50/42.63 % (1619632)Peak memory usage: 19 MB % 300.50/42.63 % (1619632)Instructions burned: 28123 (million) % 300.50/42.63 % (1619689)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=3954061282:i=12648:rtra=on_2633 on theBenchmark for (2633ds/12648Mi) % 300.50/42.63 % (1619689)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.50/42.63 % (1619689)Terminated due to inappropriate strategy. % 300.50/42.63 % (1619689)------------------------------ % 300.50/42.63 % (1619689)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.50/42.63 % (1619689)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.50/42.63 % (1619689)CaDiCaL version: 2.1.3 % 300.50/42.63 % (1619689)Termination reason: Inappropriate % 300.50/42.63 % (1619689)Time elapsed: 0.009 s % 300.50/42.63 % (1619689)Peak memory usage: 11 MB % 300.50/42.63 % (1619689)Instructions burned: 17 (million) % 300.50/42.63 % (1619689)------------------------------ % 300.50/42.63 % (1619689)------------------------------ % 300.50/42.63 % (1619691)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=2120624323:fmbsr=2.30978:i=4348:rtra=on_2632 on theBenchmark for (2632ds/4348Mi) % 300.50/42.63 % (1619691)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.50/42.63 % (1619691)Terminated due to inappropriate strategy. % 300.50/42.63 % (1619691)---------------------- % 300.50/42.63 Terminated % 300.50/42.63 % Vampire exiting %------------------------------------------------------------------------------