%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWX110_1 : TPTP v9.3.1. Released v9.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n002.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:46:30 PM UTC 2026 % Result : Timeout 300.45s 42.54s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWX110_1 : TPTP v9.3.1. Released v9.1.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.07/0.17 % Computer : n002.cluster.edu % 0.07/0.17 % Model : x86_64 x86_64 % 0.07/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.07/0.17 % Memory : 8046.5625MB % 0.07/0.17 % OS : Linux 6.8.0-71-generic % 0.07/0.17 % CPULimit : 300 % 0.07/0.17 % WCLimit : 300 % 0.07/0.17 % DateTime : Mon Sep 28 15:04:22 UTC 2026 % 0.07/0.17 % CPUTime : % 0.07/0.17 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.07/0.20 Running first-order model finding % 0.07/0.20 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 3.79/0.81 % (422310)Will run a generic schedule for satisfiability detection. % 3.79/0.81 % (422315)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2835156068_2999 on theBenchmark for (2999ds/0Mi) % 3.79/0.81 % (422315)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.79/0.81 % (422315)Terminated due to inappropriate strategy. % 3.79/0.81 % (422315)------------------------------ % 3.79/0.81 % (422315)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.79/0.81 % (422315)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.79/0.81 % (422315)CaDiCaL version: 2.1.3 % 3.79/0.81 % (422315)Termination reason: Inappropriate % 3.79/0.81 % (422315)Time elapsed: 0.002 s % 3.79/0.81 % (422315)Peak memory usage: 11 MB % 3.79/0.81 % (422315)Instructions burned: 5 (million) % 3.79/0.81 % (422315)------------------------------ % 3.79/0.81 % (422315)------------------------------ % 3.79/0.81 % (422316)% WARNING: option uhcvi not known. % 3.79/0.81 % (422317)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1670816040:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 3.79/0.81 % (422316)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2799799037:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 3.79/0.81 % (422318)dis+10_1_sil=32000:sp=arity:random_seed=2378770829:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 3.79/0.81 % (422319)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3684693305:i=116_2999 on theBenchmark for (2999ds/116Mi) % 3.79/0.81 % (422321)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1684679598:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 3.79/0.81 % (422320)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3906262418:i=131_2999 on theBenchmark for (2999ds/131Mi) % 3.79/0.81 % (422323)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2233146909:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 3.79/0.81 % (422323)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.79/0.81 % (422323)Terminated due to inappropriate strategy. % 3.79/0.81 % (422323)------------------------------ % 3.79/0.81 % (422323)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.79/0.81 % (422323)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.79/0.81 % (422323)CaDiCaL version: 2.1.3 % 3.79/0.81 % (422323)Termination reason: Inappropriate % 3.79/0.81 % (422323)Time elapsed: 0.001 s % 3.79/0.81 % (422323)Peak memory usage: 11 MB % 3.79/0.81 % (422323)Instructions burned: 5 (million) % 3.79/0.81 % (422323)------------------------------ % 3.79/0.81 % (422323)------------------------------ % 3.79/0.81 % (422331)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2954357577:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 3.79/0.81 % (422331)Instruction limit reached! % 3.79/0.81 % (422331)------------------------------ % 3.79/0.81 % (422331)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.79/0.81 % (422331)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.79/0.81 % (422331)CaDiCaL version: 2.1.3 % 3.79/0.81 % (422331)Termination reason: Instruction limit % 3.79/0.81 % (422331)Termination phase: Saturation % 3.79/0.81 % (422331)Time elapsed: 0.047 s % 3.79/0.81 % (422331)Peak memory usage: 13 MB % 3.79/0.81 % (422331)Instructions burned: 132 (million) % 3.79/0.81 % (422318)Instruction limit reached! % 3.79/0.81 % (422318)------------------------------ % 3.79/0.81 % (422318)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.79/0.81 % (422318)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.79/0.81 % (422318)CaDiCaL version: 2.1.3 % 3.79/0.81 % (422318)Termination reason: Instruction limit % 3.79/0.81 % (422318)Termination phase: Saturation % 3.79/0.81 % (422318)Time elapsed: 0.067 s % 3.79/0.81 % (422318)Peak memory usage: 13 MB % 3.79/0.81 % (422318)Instructions burned: 104 (million) % 3.79/0.81 % (422319)Instruction limit reached! % 3.79/0.81 % (422319)------------------------------ % 3.79/0.81 % (422319)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.79/0.81 % (422319)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.79/0.81 % (422319)CaDiCaL version: 2.1.3 % 3.79/0.81 % (422319)Termination reason: Instruction limit % 3.79/0.81 % (422319)Termination phase: Saturation % 7.47/1.36 % (422319)Time elapsed: 0.069 s % 7.47/1.36 % (422319)Peak memory usage: 13 MB % 7.47/1.36 % (422319)Instructions burned: 117 (million) % 7.47/1.36 % (422333)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=1961447598:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 7.47/1.36 % (422320)Instruction limit reached! % 7.47/1.36 % (422320)------------------------------ % 7.47/1.36 % (422320)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.47/1.36 % (422320)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.47/1.36 % (422320)CaDiCaL version: 2.1.3 % 7.47/1.36 % (422320)Termination reason: Instruction limit % 7.47/1.36 % (422320)Termination phase: Saturation % 7.47/1.36 % (422320)Time elapsed: 0.080 s % 7.47/1.36 % (422320)Peak memory usage: 13 MB % 7.47/1.36 % (422320)Instructions burned: 131 (million) % 7.47/1.36 % (422334)ott-21_1_sil=16000:fs=off:random_seed=32169272:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 7.47/1.36 % (422335)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=105409208:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 7.47/1.36 % (422337)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2848219107:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 7.47/1.36 % (422337)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 7.47/1.36 % (422337)Terminated due to inappropriate strategy. % 7.47/1.36 % (422337)------------------------------ % 7.47/1.36 % (422337)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.47/1.36 % (422337)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.47/1.36 % (422337)CaDiCaL version: 2.1.3 % 7.47/1.36 % (422337)Termination reason: Inappropriate % 7.47/1.36 % (422337)Time elapsed: 0.002 s % 7.47/1.36 % (422337)Peak memory usage: 10 MB % 7.47/1.36 % (422337)Instructions burned: 3 (million) % 7.47/1.36 % (422337)------------------------------ % 7.47/1.36 % (422337)------------------------------ % 7.47/1.36 % (422321)Instruction limit reached! % 7.47/1.36 % (422321)------------------------------ % 7.47/1.36 % (422321)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.47/1.36 % (422321)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.47/1.36 % (422321)CaDiCaL version: 2.1.3 % 7.47/1.36 % (422321)Termination reason: Instruction limit % 7.47/1.36 % (422321)Termination phase: Saturation % 7.47/1.36 % (422321)Time elapsed: 0.111 s % 7.47/1.36 % (422321)Peak memory usage: 14 MB % 7.47/1.36 % (422321)Instructions burned: 160 (million) % 7.47/1.36 % (422341)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=899877836:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 7.47/1.36 % (422342)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1896945285:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 7.47/1.36 % (422342)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 7.47/1.36 % (422342)Terminated due to inappropriate strategy. % 7.47/1.36 % (422342)------------------------------ % 7.47/1.36 % (422342)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.47/1.36 % (422342)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.47/1.36 % (422342)CaDiCaL version: 2.1.3 % 7.47/1.37 % (422342)Termination reason: Inappropriate % 7.47/1.37 % (422342)Time elapsed: 0.002 s % 7.47/1.37 % (422342)Peak memory usage: 10 MB % 7.47/1.37 % (422342)Instructions burned: 4 (million) % 7.47/1.37 % (422342)------------------------------ % 7.47/1.37 % (422342)------------------------------ % 7.47/1.37 % (422345)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=1202395369:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2998 on theBenchmark for (2998ds/692Mi) % 7.47/1.37 % (422334)Instruction limit reached! % 7.47/1.37 % (422334)------------------------------ % 7.47/1.37 % (422334)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.47/1.37 % (422334)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.47/1.37 % (422334)CaDiCaL version: 2.1.3 % 7.47/1.37 % (422334)Termination reason: Instruction limit % 7.47/1.37 % (422334)Termination phase: Saturation % 7.47/1.37 % (422334)Time elapsed: 0.085 s % 7.47/1.37 % (422334)Peak memory usage: 12 MB % 7.47/1.37 % (422334)Instructions burned: 182 (million) % 20.96/3.29 % (422347)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1534982179:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 20.96/3.29 % (422333)Instruction limit reached! % 20.96/3.29 % (422333)------------------------------ % 20.96/3.29 % (422333)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.96/3.29 % (422333)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.96/3.29 % (422333)CaDiCaL version: 2.1.3 % 20.96/3.29 % (422333)Termination reason: Instruction limit % 20.96/3.29 % (422333)Termination phase: Saturation % 20.96/3.29 % (422333)Time elapsed: 0.199 s % 20.96/3.29 % (422333)Peak memory usage: 15 MB % 20.96/3.29 % (422333)Instructions burned: 688 (million) % 20.96/3.29 % (422349)fmb+10_1_sil=64000:random_seed=2341786836:i=22061:nm=2:gsp=on_2996 on theBenchmark for (2996ds/22061Mi) % 20.96/3.29 % (422349)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 20.96/3.29 % (422349)Terminated due to inappropriate strategy. % 20.96/3.29 % (422349)------------------------------ % 20.96/3.29 % (422349)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.96/3.29 % (422349)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.96/3.29 % (422349)CaDiCaL version: 2.1.3 % 20.96/3.29 % (422349)Termination reason: Inappropriate % 20.96/3.29 % (422349)Time elapsed: 0.001 s % 20.96/3.29 % (422349)Peak memory usage: 10 MB % 20.96/3.29 % (422349)Instructions burned: 5 (million) % 20.96/3.29 % (422349)------------------------------ % 20.96/3.29 % (422349)------------------------------ % 20.96/3.29 % (422351)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3669298939:i=9515:nm=5_2996 on theBenchmark for (2996ds/9515Mi) % 20.96/3.29 % (422351)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 20.96/3.29 % (422351)Terminated due to inappropriate strategy. % 20.96/3.29 % (422351)------------------------------ % 20.96/3.29 % (422351)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.96/3.29 % (422351)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.96/3.29 % (422351)CaDiCaL version: 2.1.3 % 20.96/3.29 % (422351)Termination reason: Inappropriate % 20.96/3.29 % (422351)Time elapsed: 0.001 s % 20.96/3.29 % (422351)Peak memory usage: 10 MB % 20.96/3.29 % (422351)Instructions burned: 4 (million) % 20.96/3.29 % (422351)------------------------------ % 20.96/3.29 % (422351)------------------------------ % 20.96/3.29 % (422353)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1894119662:fmbsr=1.7:i=920_2996 on theBenchmark for (2996ds/920Mi) % 20.96/3.29 % (422353)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 20.96/3.29 % (422353)Terminated due to inappropriate strategy. % 20.96/3.29 % (422353)------------------------------ % 20.96/3.29 % (422353)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.96/3.29 % (422353)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.96/3.29 % (422353)CaDiCaL version: 2.1.3 % 20.96/3.29 % (422353)Termination reason: Inappropriate % 20.96/3.29 % (422353)Time elapsed: 0.001 s % 20.96/3.29 % (422353)Peak memory usage: 10 MB % 20.96/3.29 % (422353)Instructions burned: 4 (million) % 20.96/3.29 % (422353)------------------------------ % 20.96/3.29 % (422353)------------------------------ % 20.96/3.29 % (422355)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1464107489:i=5131_2996 on theBenchmark for (2996ds/5131Mi) % 20.96/3.29 % (422335)Instruction limit reached! % 20.96/3.29 % (422335)------------------------------ % 20.96/3.29 % (422335)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.96/3.29 % (422335)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.96/3.29 % (422335)CaDiCaL version: 2.1.3 % 20.96/3.29 % (422335)Termination reason: Instruction limit % 20.96/3.29 % (422335)Termination phase: Saturation % 20.96/3.29 % (422335)Time elapsed: 0.329 s % 20.96/3.29 % (422335)Peak memory usage: 14 MB % 20.96/3.29 % (422335)Instructions burned: 478 (million) % 20.96/3.29 % (422357)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1572013177:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi) % 20.96/3.29 % (422345)Instruction limit reached! % 20.96/3.29 % (422345)------------------------------ % 20.96/3.29 % (422345)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.96/3.29 % (422345)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.11/3.48 % (422345)CaDiCaL version: 2.1.3 % 22.11/3.48 % (422345)Termination reason: Instruction limit % 22.11/3.48 % (422345)Termination phase: Saturation % 22.11/3.48 % (422345)Time elapsed: 0.404 s % 22.11/3.48 % (422345)Peak memory usage: 17 MB % 22.11/3.48 % (422345)Instructions burned: 692 (million) % 22.11/3.48 % (422359)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3535232370:i=6324_2994 on theBenchmark for (2994ds/6324Mi) % 22.11/3.48 % (422359)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 22.11/3.48 % (422359)Terminated due to inappropriate strategy. % 22.11/3.48 % (422359)------------------------------ % 22.11/3.48 % (422359)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.11/3.48 % (422359)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.11/3.48 % (422359)CaDiCaL version: 2.1.3 % 22.11/3.48 % (422359)Termination reason: Inappropriate % 22.11/3.48 % (422359)Time elapsed: 0.003 s % 22.11/3.48 % (422359)Peak memory usage: 11 MB % 22.11/3.48 % (422359)Instructions burned: 5 (million) % 22.11/3.48 % (422359)------------------------------ % 22.11/3.48 % (422359)------------------------------ % 22.11/3.48 % (422361)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=263356987:fmbsr=2.30978:i=2174_2993 on theBenchmark for (2993ds/2174Mi) % 22.11/3.48 % (422361)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 22.11/3.48 % (422361)Terminated due to inappropriate strategy. % 22.11/3.48 % (422361)------------------------------ % 22.11/3.48 % (422361)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.11/3.48 % (422361)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.11/3.48 % (422361)CaDiCaL version: 2.1.3 % 22.11/3.48 % (422361)Termination reason: Inappropriate % 22.11/3.48 % (422361)Time elapsed: 0.003 s % 22.11/3.48 % (422361)Peak memory usage: 10 MB % 22.11/3.48 % (422361)Instructions burned: 4 (million) % 22.11/3.48 % (422361)------------------------------ % 22.11/3.48 % (422361)------------------------------ % 22.11/3.48 % (422363)ott-2_1_sil=16000:newcnf=on:random_seed=1638482705:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2993 on theBenchmark for (2993ds/869Mi) % 22.11/3.48 % (422347)Instruction limit reached! % 22.11/3.48 % (422347)------------------------------ % 22.11/3.48 % (422347)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.11/3.48 % (422347)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.11/3.48 % (422347)CaDiCaL version: 2.1.3 % 22.11/3.48 % (422347)Termination reason: Instruction limit % 22.11/3.48 % (422347)Termination phase: Saturation % 22.11/3.48 % (422347)Time elapsed: 0.505 s % 22.11/3.48 % (422347)Peak memory usage: 19 MB % 22.11/3.48 % (422347)Instructions burned: 879 (million) % 22.11/3.48 % (422365)ott+10_1_sil=32000:tgt=ground:random_seed=4078471331:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi) % 22.11/3.48 % (422341)Instruction limit reached! % 22.11/3.48 % (422341)------------------------------ % 22.11/3.48 % (422341)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.11/3.48 % (422341)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.11/3.48 % (422341)CaDiCaL version: 2.1.3 % 22.11/3.48 % (422341)Termination reason: Instruction limit % 22.11/3.48 % (422341)Termination phase: Saturation % 22.11/3.48 % (422341)Time elapsed: 0.710 s % 22.11/3.48 % (422341)Peak memory usage: 22 MB % 22.11/3.48 % (422341)Instructions burned: 1179 (million) % 22.11/3.48 % (422367)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1642258500:i=54282_2991 on theBenchmark for (2991ds/54282Mi) % 22.11/3.48 % (422367)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 22.11/3.48 % (422367)Terminated due to inappropriate strategy. % 22.11/3.48 % (422367)------------------------------ % 22.11/3.48 % (422367)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.11/3.48 % (422367)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.11/3.48 % (422367)CaDiCaL version: 2.1.3 % 22.11/3.48 % (422367)Termination reason: Inappropriate % 22.11/3.48 % (422367)Time elapsed: 0.003 s % 22.11/3.48 % (422367)Peak memory usage: 11 MB % 22.11/3.48 % (422367)Instructions burned: 5 (million) % 22.11/3.48 % (422367)------------------------------ % 22.11/3.48 % (422367)------------------------------ % 22.11/3.48 % (422369)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3948711679:i=3512:aac=none_2991 on theBenchmark for (2991ds/3512Mi) % 22.11/3.48 % (422363)Instruction limit reached! % 92.12/13.26 % (422363)------------------------------ % 92.12/13.26 % (422363)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 92.12/13.26 % (422363)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 92.12/13.26 % (422363)CaDiCaL version: 2.1.3 % 92.12/13.26 % (422363)Termination reason: Instruction limit % 92.12/13.26 % (422363)Termination phase: Saturation % 92.12/13.26 % (422363)Time elapsed: 0.490 s % 92.12/13.26 % (422363)Peak memory usage: 19 MB % 92.12/13.26 % (422363)Instructions burned: 869 (million) % 92.12/13.26 % (422371)dis+21_1_sil=32000:sas=cadical:random_seed=3447035257:i=3773:amm=off_2988 on theBenchmark for (2988ds/3773Mi) % 92.12/13.26 % (422357)Instruction limit reached! % 92.12/13.26 % (422357)------------------------------ % 92.12/13.26 % (422357)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 92.12/13.26 % (422357)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 92.12/13.26 % (422357)CaDiCaL version: 2.1.3 % 92.12/13.26 % (422357)Termination reason: Instruction limit % 92.12/13.26 % (422357)Termination phase: Saturation % 92.12/13.26 % (422357)Time elapsed: 0.700 s % 92.12/13.26 % (422357)Peak memory usage: 25 MB % 92.12/13.26 % (422357)Instructions burned: 1474 (million) % 92.12/13.26 % (422373)ott+11_1_sil=16000:gs=on:random_seed=1052058939:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2988 on theBenchmark for (2988ds/2251Mi) % 92.12/13.26 % (422355)Instruction limit reached! % 92.12/13.26 % (422355)------------------------------ % 92.12/13.26 % (422355)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 92.12/13.26 % (422355)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 92.12/13.26 % (422355)CaDiCaL version: 2.1.3 % 92.12/13.26 % (422355)Termination reason: Instruction limit % 92.12/13.26 % (422355)Termination phase: Saturation % 92.12/13.26 % (422355)Time elapsed: 1.490 s % 92.12/13.26 % (422355)Peak memory usage: 42 MB % 92.12/13.26 % (422355)Instructions burned: 5132 (million) % 92.12/13.26 % (422375)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1162649924:fmbsr=1.6:i=67534_2981 on theBenchmark for (2981ds/67534Mi) % 92.12/13.26 % (422375)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 92.12/13.26 % (422375)Terminated due to inappropriate strategy. % 92.12/13.26 % (422375)------------------------------ % 92.12/13.26 % (422375)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 92.12/13.26 % (422375)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 92.12/13.26 % (422375)CaDiCaL version: 2.1.3 % 92.12/13.26 % (422375)Termination reason: Inappropriate % 92.12/13.26 % (422375)Time elapsed: 0.001 s % 92.12/13.26 % (422375)Peak memory usage: 10 MB % 92.12/13.26 % (422375)Instructions burned: 4 (million) % 92.12/13.26 % (422375)------------------------------ % 92.12/13.26 % (422375)------------------------------ % 92.12/13.26 % (422377)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2837553314:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2981 on theBenchmark for (2981ds/4591Mi) % 92.12/13.26 % (422373)Instruction limit reached! % 92.12/13.26 % (422373)------------------------------ % 92.12/13.26 % (422373)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 92.12/13.26 % (422373)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 92.12/13.26 % (422373)CaDiCaL version: 2.1.3 % 92.12/13.26 % (422373)Termination reason: Instruction limit % 92.12/13.26 % (422373)Termination phase: Saturation % 92.12/13.26 % (422373)Time elapsed: 1.271 s % 92.12/13.26 % (422373)Peak memory usage: 25 MB % 92.12/13.26 % (422373)Instructions burned: 2252 (million) % 92.12/13.26 % (422379)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=926148906:i=29340_2975 on theBenchmark for (2975ds/29340Mi) % 92.12/13.26 % (422369)Instruction limit reached! % 92.12/13.26 % (422369)------------------------------ % 92.12/13.26 % (422369)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 92.12/13.26 % (422369)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 92.12/13.26 % (422369)CaDiCaL version: 2.1.3 % 92.12/13.26 % (422369)Termination reason: Instruction limit % 92.12/13.26 % (422369)Termination phase: Saturation % 92.12/13.26 % (422369)Time elapsed: 1.868 s % 92.12/13.26 % (422369)Peak memory usage: 32 MB % 92.12/13.26 % (422369)Instructions burned: 3512 (million) % 92.12/13.26 % (422381)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3638320087:i=5211_2972 on theBenchmark for (2972ds/5211Mi) % 92.12/13.26 % (422377)Instruction limit reached! % 132.59/19.01 % (422377)------------------------------ % 132.59/19.01 % (422377)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 132.59/19.01 % (422377)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 132.59/19.01 % (422377)CaDiCaL version: 2.1.3 % 132.59/19.01 % (422377)Termination reason: Instruction limit % 132.59/19.01 % (422377)Termination phase: Saturation % 132.59/19.01 % (422377)Time elapsed: 1.201 s % 132.59/19.01 % (422377)Peak memory usage: 56 MB % 132.59/19.01 % (422377)Instructions burned: 4592 (million) % 132.59/19.01 % (422383)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1672014950:i=5497:nm=2_2969 on theBenchmark for (2969ds/5497Mi) % 132.59/19.01 % (422383)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 132.59/19.01 % (422383)Terminated due to inappropriate strategy. % 132.59/19.01 % (422383)------------------------------ % 132.59/19.01 % (422383)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 132.59/19.01 % (422383)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 132.59/19.01 % (422383)CaDiCaL version: 2.1.3 % 132.59/19.01 % (422383)Termination reason: Inappropriate % 132.59/19.01 % (422383)Time elapsed: 0.002 s % 132.59/19.01 % (422383)Peak memory usage: 11 MB % 132.59/19.01 % (422383)Instructions burned: 5 (million) % 132.59/19.01 % (422383)------------------------------ % 132.59/19.01 % (422383)------------------------------ % 132.59/19.01 % (422385)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=326270260:fmbsr=2:i=46332_2969 on theBenchmark for (2969ds/46332Mi) % 132.59/19.01 % (422385)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 132.59/19.01 % (422385)Terminated due to inappropriate strategy. % 132.59/19.01 % (422385)------------------------------ % 132.59/19.01 % (422385)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 132.59/19.01 % (422385)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 132.59/19.01 % (422385)CaDiCaL version: 2.1.3 % 132.59/19.01 % (422385)Termination reason: Inappropriate % 132.59/19.01 % (422385)Time elapsed: 0.001 s % 132.59/19.01 % (422385)Peak memory usage: 10 MB % 132.59/19.01 % (422385)Instructions burned: 4 (million) % 132.59/19.01 % (422385)------------------------------ % 132.59/19.01 % (422385)------------------------------ % 132.59/19.01 % (422387)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=881849815:i=14071_2968 on theBenchmark for (2968ds/14071Mi) % 132.59/19.01 % (422387)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 132.59/19.01 % (422387)Terminated due to inappropriate strategy. % 132.59/19.01 % (422387)------------------------------ % 132.59/19.01 % (422387)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 132.59/19.01 % (422387)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 132.59/19.01 % (422387)CaDiCaL version: 2.1.3 % 132.59/19.01 % (422387)Termination reason: Inappropriate % 132.59/19.01 % (422387)Time elapsed: 0.001 s % 132.59/19.01 % (422387)Peak memory usage: 10 MB % 132.59/19.01 % (422387)Instructions burned: 4 (million) % 132.59/19.01 % (422387)------------------------------ % 132.59/19.01 % (422387)------------------------------ % 132.59/19.01 % (422389)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2373637803:i=22565:add=on:rawr=on_2968 on theBenchmark for (2968ds/22565Mi) % 132.59/19.01 % (422371)Instruction limit reached! % 132.59/19.01 % (422371)------------------------------ % 132.59/19.01 % (422371)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 132.59/19.01 % (422371)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 132.59/19.01 % (422371)CaDiCaL version: 2.1.3 % 132.59/19.01 % (422371)Termination reason: Instruction limit % 132.59/19.01 % (422371)Termination phase: Saturation % 132.59/19.01 % (422371)Time elapsed: 2.055 s % 132.59/19.01 % (422371)Peak memory usage: 35 MB % 132.59/19.01 % (422371)Instructions burned: 3774 (million) % 132.59/19.01 % (422391)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=409227092:i=8173:av=off_2967 on theBenchmark for (2967ds/8173Mi) % 132.59/19.01 % (422365)Instruction limit reached! % 132.59/19.01 % (422365)------------------------------ % 132.59/19.01 % (422365)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 132.59/19.01 % (422365)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 132.59/19.01 % (422365)CaDiCaL version: 2.1.3 % 132.59/19.01 % (422365)Termination reason: Instruction limit % 132.59/19.01 % (422365)Termination phase: Saturation % 132.59/19.01 % (422365)Time elapsed: 2.513 s % 150.44/21.46 % (422365)Peak memory usage: 33 MB % 150.44/21.46 % (422365)Instructions burned: 5114 (million) % 150.44/21.46 % (422393)dis+10_16:1_sil=16000:random_seed=1740171489:i=9155:fsr=off_2967 on theBenchmark for (2967ds/9155Mi) % 150.44/21.46 % (422381)Instruction limit reached! % 150.44/21.46 % (422381)------------------------------ % 150.44/21.46 % (422381)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 150.44/21.46 % (422381)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 150.44/21.46 % (422381)CaDiCaL version: 2.1.3 % 150.44/21.46 % (422381)Termination reason: Instruction limit % 150.44/21.46 % (422381)Termination phase: Saturation % 150.44/21.46 % (422381)Time elapsed: 2.809 s % 150.44/21.46 % (422381)Peak memory usage: 58 MB % 150.44/21.46 % (422381)Instructions burned: 5212 (million) % 150.44/21.46 % (422395)ott-3_8_sil=64000:random_seed=1686249556:i=20139:bs=on_2943 on theBenchmark for (2943ds/20139Mi) % 150.44/21.46 % (422393)Instruction limit reached! % 150.44/21.46 % (422393)------------------------------ % 150.44/21.46 % (422393)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 150.44/21.46 % (422393)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 150.44/21.46 % (422393)CaDiCaL version: 2.1.3 % 150.44/21.46 % (422393)Termination reason: Instruction limit % 150.44/21.46 % (422393)Termination phase: Saturation % 150.44/21.46 % (422393)Time elapsed: 4.706 s % 150.44/21.46 % (422393)Peak memory usage: 53 MB % 150.44/21.46 % (422393)Instructions burned: 9156 (million) % 150.44/21.46 % (422397)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=1690378542:fmbsr=2:i=32576_2919 on theBenchmark for (2919ds/32576Mi) % 150.44/21.46 % (422397)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 150.44/21.46 % (422397)Terminated due to inappropriate strategy. % 150.44/21.46 % (422397)------------------------------ % 150.44/21.46 % (422397)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 150.44/21.46 % (422397)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 150.44/21.46 % (422397)CaDiCaL version: 2.1.3 % 150.44/21.46 % (422397)Termination reason: Inappropriate % 150.44/21.46 % (422397)Time elapsed: 0.003 s % 150.44/21.46 % (422397)Peak memory usage: 11 MB % 150.44/21.46 % (422397)Instructions burned: 5 (million) % 150.44/21.46 % (422397)------------------------------ % 150.44/21.46 % (422397)------------------------------ % 150.44/21.46 % (422399)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=932636003:i=11404_2919 on theBenchmark for (2919ds/11404Mi) % 150.44/21.46 % (422391)Instruction limit reached! % 150.44/21.46 % (422391)------------------------------ % 150.44/21.46 % (422391)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 150.44/21.46 % (422391)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 150.44/21.46 % (422391)CaDiCaL version: 2.1.3 % 150.44/21.46 % (422391)Termination reason: Instruction limit % 150.44/21.46 % (422391)Termination phase: Saturation % 150.44/21.46 % (422391)Time elapsed: 4.930 s % 150.44/21.46 % (422391)Peak memory usage: 52 MB % 150.44/21.46 % (422391)Instructions burned: 8173 (million) % 150.44/21.46 % (422401)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=235680651:i=14134_2918 on theBenchmark for (2918ds/14134Mi) % 150.44/21.46 % (422389)Instruction limit reached! % 150.44/21.46 % (422389)------------------------------ % 150.44/21.46 % (422389)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 150.44/21.46 % (422389)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 150.44/21.46 % (422389)CaDiCaL version: 2.1.3 % 150.44/21.46 % (422389)Termination reason: Instruction limit % 150.44/21.46 % (422389)Termination phase: Saturation % 150.44/21.46 % (422389)Time elapsed: 5.188 s % 150.44/21.46 % (422389)Peak memory usage: 67 MB % 150.44/21.46 % (422389)Instructions burned: 22569 (million) % 150.44/21.46 % (422403)dis+33_16_sil=32000:sac=on:random_seed=3660185819:i=15851:nm=0_2916 on theBenchmark for (2916ds/15851Mi) % 150.44/21.46 % (422403)Instruction limit reached! % 150.44/21.46 % (422403)------------------------------ % 150.44/21.46 % (422403)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 150.44/21.46 % (422403)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 150.44/21.46 % (422403)CaDiCaL version: 2.1.3 % 150.44/21.46 % (422403)Termination reason: Instruction limit % 150.44/21.46 % (422403)Termination phase: Saturation % 150.44/21.46 % (422403)Time elapsed: 4.679 s % 150.44/21.46 % (422403)Peak memory usage: 141 MB % 150.44/21.46 % (422403)Instructions burned: 15854 (million) % 150.44/21.46 % (422405)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=783922706:avsq=on:i=17627:add=on:amm=off_2869 on theBenchmark for (2869ds/17627Mi) % 161.14/22.91 % (422399)Instruction limit reached! % 161.14/22.91 % (422399)------------------------------ % 161.14/22.91 % (422399)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 161.14/22.91 % (422399)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 161.14/22.91 % (422399)CaDiCaL version: 2.1.3 % 161.14/22.91 % (422399)Termination reason: Instruction limit % 161.14/22.91 % (422399)Termination phase: Saturation % 161.14/22.91 % (422399)Time elapsed: 7.565 s % 161.14/22.91 % (422399)Peak memory usage: 64 MB % 161.14/22.91 % (422399)Instructions burned: 11404 (million) % 161.14/22.91 % (422703)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=3631794297:s2a=on:i=53295_2843 on theBenchmark for (2843ds/53295Mi) % 161.14/22.91 % (422379)Instruction limit reached! % 161.14/22.91 % (422379)------------------------------ % 161.14/22.91 % (422379)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 161.14/22.91 % (422379)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 161.14/22.91 % (422379)CaDiCaL version: 2.1.3 % 161.14/22.91 % (422379)Termination reason: Instruction limit % 161.14/22.91 % (422379)Termination phase: Saturation % 161.14/22.91 % (422379)Time elapsed: 15.944 s % 161.14/22.91 % (422379)Peak memory usage: 282 MB % 161.14/22.91 % (422379)Instructions burned: 29341 (million) % 161.14/22.91 % (422721)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=1889900235:i=26857:ins=20_2814 on theBenchmark for (2814ds/26857Mi) % 161.14/22.91 % (422721)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 161.14/22.91 % (422721)Terminated due to inappropriate strategy. % 161.14/22.91 % (422721)------------------------------ % 161.14/22.91 % (422721)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 161.14/22.91 % (422721)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 161.14/22.91 % (422721)CaDiCaL version: 2.1.3 % 161.14/22.91 % (422721)Termination reason: Inappropriate % 161.14/22.91 % (422721)Time elapsed: 0.005 s % 161.14/22.91 % (422721)Peak memory usage: 10 MB % 161.14/22.91 % (422721)Instructions burned: 4 (million) % 161.14/22.91 % (422721)------------------------------ % 161.14/22.91 % (422721)------------------------------ % 161.14/22.91 % (422723)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=2398025971:i=28120:bs=on:fsr=off_2814 on theBenchmark for (2814ds/28120Mi) % 161.14/22.91 % (422401)Instruction limit reached! % 161.14/22.91 % (422401)------------------------------ % 161.14/22.91 % (422401)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 161.14/22.91 % (422401)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 161.14/22.91 % (422401)CaDiCaL version: 2.1.3 % 161.14/22.91 % (422401)Termination reason: Instruction limit % 161.14/22.91 % (422401)Termination phase: Saturation % 161.14/22.91 % (422401)Time elapsed: 10.499 s % 161.14/22.91 % (422401)Peak memory usage: 72 MB % 161.14/22.91 % (422401)Instructions burned: 14134 (million) % 161.14/22.91 % (422725)fmb+10_1_sil=256000:fmbss=7:random_seed=1241230731:fmbsr=1.6:i=182295_2812 on theBenchmark for (2812ds/182295Mi) % 161.14/22.91 % (422725)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 161.14/22.91 % (422725)Terminated due to inappropriate strategy. % 161.14/22.91 % (422725)------------------------------ % 161.14/22.91 % (422725)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 161.14/22.91 % (422725)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 161.14/22.91 % (422725)CaDiCaL version: 2.1.3 % 161.14/22.91 % (422725)Termination reason: Inappropriate % 161.14/22.91 % (422725)Time elapsed: 0.004 s % 161.14/22.91 % (422725)Peak memory usage: 11 MB % 161.14/22.91 % (422725)Instructions burned: 4 (million) % 161.14/22.91 % (422725)------------------------------ % 161.14/22.91 % (422725)------------------------------ % 161.14/22.91 % (422727)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=2790013432:i=44625:gsp=on_2812 on theBenchmark for (2812ds/44625Mi) % 161.14/22.91 % (422727)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 161.14/22.91 % (422727)Terminated due to inappropriate strategy. % 161.14/22.91 % (422727)------------------------------ % 161.14/22.91 % (422727)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 161.14/22.91 % (422727)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 161.14/22.91 % (422727)CaDiCaL version: 2.1.3 % 161.14/22.91 % (422727)Termination reason: Inappropriate % 196.63/28.00 % (422727)Time elapsed: 0.008 s % 196.63/28.00 % (422727)Peak memory usage: 11 MB % 196.63/28.00 % (422727)Instructions burned: 8 (million) % 196.63/28.00 % (422727)------------------------------ % 196.63/28.00 % (422727)------------------------------ % 196.63/28.00 % (422729)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=2703987691:i=160505_2812 on theBenchmark for (2812ds/160505Mi) % 196.63/28.00 % (422729)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 196.63/28.00 % (422729)Terminated due to inappropriate strategy. % 196.63/28.00 % (422729)------------------------------ % 196.63/28.00 % (422729)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 196.63/28.00 % (422729)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 196.63/28.00 % (422729)CaDiCaL version: 2.1.3 % 196.63/28.00 % (422729)Termination reason: Inappropriate % 196.63/28.00 % (422729)Time elapsed: 0.005 s % 196.63/28.00 % (422729)Peak memory usage: 10 MB % 196.63/28.00 % (422729)Instructions burned: 4 (million) % 196.63/28.00 % (422729)------------------------------ % 196.63/28.00 % (422729)------------------------------ % 196.63/28.00 % (422731)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=572194354:fmbsr=1.3:i=225729_2811 on theBenchmark for (2811ds/225729Mi) % 196.63/28.00 % (422731)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 196.63/28.00 % (422731)Terminated due to inappropriate strategy. % 196.63/28.00 % (422731)------------------------------ % 196.63/28.00 % (422731)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 196.63/28.00 % (422731)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 196.63/28.00 % (422731)CaDiCaL version: 2.1.3 % 196.63/28.00 % (422731)Termination reason: Inappropriate % 196.63/28.00 % (422731)Time elapsed: 0.004 s % 196.63/28.00 % (422731)Peak memory usage: 11 MB % 196.63/28.00 % (422731)Instructions burned: 4 (million) % 196.63/28.00 % (422731)------------------------------ % 196.63/28.00 % (422731)------------------------------ % 196.63/28.00 % (422733)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=2301093232:fmbsr=2:i=185024:ins=7_2811 on theBenchmark for (2811ds/185024Mi) % 196.63/28.00 % (422733)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 196.63/28.00 % (422733)Terminated due to inappropriate strategy. % 196.63/28.00 % (422733)------------------------------ % 196.63/28.00 % (422733)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 196.63/28.00 % (422733)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 196.63/28.00 % (422733)CaDiCaL version: 2.1.3 % 196.63/28.00 % (422733)Termination reason: Inappropriate % 196.63/28.00 % (422733)Time elapsed: 0.005 s % 196.63/28.00 % (422733)Peak memory usage: 10 MB % 196.63/28.00 % (422733)Instructions burned: 4 (million) % 196.63/28.00 % (422733)------------------------------ % 196.63/28.00 % (422733)------------------------------ % 196.63/28.00 % (422735)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=438818910:rtra=on_2810 on theBenchmark for (2810ds/0Mi) % 196.63/28.00 % (422735)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 196.63/28.00 % (422735)Terminated due to inappropriate strategy. % 196.63/28.00 % (422735)------------------------------ % 196.63/28.00 % (422735)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 196.63/28.00 % (422735)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 196.63/28.00 % (422735)CaDiCaL version: 2.1.3 % 196.63/28.00 % (422735)Termination reason: Inappropriate % 196.63/28.00 % (422735)Time elapsed: 0.007 s % 196.63/28.00 % (422735)Peak memory usage: 11 MB % 196.63/28.00 % (422735)Instructions burned: 6 (million) % 196.63/28.00 % (422735)------------------------------ % 196.63/28.00 % (422735)------------------------------ % 196.63/28.00 % (422737)% WARNING: option uhcvi not known. % 196.63/28.00 % (422737)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=870487529:i=271062:add=off:rtra=on:rawr=on_2810 on theBenchmark for (2810ds/271062Mi) % 196.63/28.00 % (422405)Instruction limit reached! % 196.63/28.00 % (422405)------------------------------ % 196.63/28.00 % (422405)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 196.63/28.00 % (422405)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 196.63/28.00 % (422405)CaDiCaL version: 2.1.3 % 196.63/28.00 % (422405)Termination reason: Instruction limit % 196.63/28.00 % (422405)Termination phase: Saturation % 196.63/28.00 % (422405)Time elapsed: 8.163 s % 196.63/28.00 % (422405)Peak memory usage: 82 MB % 196.63/28.00 % (422405)Instructions burned: 17629 (million) % 196.63/28.00 % (422757)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3343867591:i=176048:add=on:rtra=on:rawr=on_2787 on theBenchmark for (2787ds/176048Mi) % 218.92/31.08 % (422395)Instruction limit reached! % 218.92/31.08 % (422395)------------------------------ % 218.92/31.08 % (422395)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 218.92/31.08 % (422395)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 218.92/31.08 % (422395)CaDiCaL version: 2.1.3 % 218.92/31.08 % (422395)Termination reason: Instruction limit % 218.92/31.08 % (422395)Termination phase: Saturation % 218.92/31.08 % (422395)Time elapsed: 15.958 s % 218.92/31.08 % (422395)Peak memory usage: 86 MB % 218.92/31.08 % (422395)Instructions burned: 20140 (million) % 218.92/31.08 % (422759)dis+10_1_sil=32000:si=on:sp=arity:random_seed=2616495649:i=206:fgj=on:rtra=on_2783 on theBenchmark for (2783ds/206Mi) % 218.92/31.08 % (422759)Instruction limit reached! % 218.92/31.08 % (422759)------------------------------ % 218.92/31.08 % (422759)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 218.92/31.08 % (422759)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 218.92/31.08 % (422759)CaDiCaL version: 2.1.3 % 218.92/31.08 % (422759)Termination reason: Instruction limit % 218.92/31.08 % (422759)Termination phase: Saturation % 218.92/31.08 % (422759)Time elapsed: 0.188 s % 218.92/31.08 % (422759)Peak memory usage: 14 MB % 218.92/31.08 % (422759)Instructions burned: 207 (million) % 218.92/31.08 % (422761)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=3217957808:i=232:rtra=on_2781 on theBenchmark for (2781ds/232Mi) % 218.92/31.08 % (422761)Instruction limit reached! % 218.92/31.08 % (422761)------------------------------ % 218.92/31.08 % (422761)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 218.92/31.08 % (422761)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 218.92/31.08 % (422761)CaDiCaL version: 2.1.3 % 218.92/31.08 % (422761)Termination reason: Instruction limit % 218.92/31.08 % (422761)Termination phase: Saturation % 218.92/31.08 % (422761)Time elapsed: 0.229 s % 218.92/31.08 % (422761)Peak memory usage: 14 MB % 218.92/31.08 % (422761)Instructions burned: 232 (million) % 218.92/31.08 % (422763)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=2918408796:i=262:rtra=on_2779 on theBenchmark for (2779ds/262Mi) % 218.92/31.08 % (422763)Instruction limit reached! % 218.92/31.08 % (422763)------------------------------ % 218.92/31.08 % (422763)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 218.92/31.08 % (422763)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 218.92/31.08 % (422763)CaDiCaL version: 2.1.3 % 218.92/31.08 % (422763)Termination reason: Instruction limit % 218.92/31.08 % (422763)Termination phase: Saturation % 218.92/31.08 % (422763)Time elapsed: 0.192 s % 218.92/31.08 % (422763)Peak memory usage: 14 MB % 218.92/31.08 % (422763)Instructions burned: 262 (million) % 218.92/31.08 % (422765)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=2626360932:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2776 on theBenchmark for (2776ds/318Mi) % 218.92/31.08 % (422765)Instruction limit reached! % 218.92/31.08 % (422765)------------------------------ % 218.92/31.08 % (422765)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 218.92/31.08 % (422765)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 218.92/31.08 % (422765)CaDiCaL version: 2.1.3 % 218.92/31.08 % (422765)Termination reason: Instruction limit % 218.92/31.08 % (422765)Termination phase: Saturation % 218.92/31.08 % (422765)Time elapsed: 0.316 s % 218.92/31.08 % (422765)Peak memory usage: 15 MB % 218.92/31.08 % (422765)Instructions burned: 318 (million) % 218.92/31.08 % (422767)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=2953219877:i=1428:nm=2:rtra=on_2773 on theBenchmark for (2773ds/1428Mi) % 218.92/31.08 % (422767)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 218.92/31.08 % (422767)Terminated due to inappropriate strategy. % 218.92/31.08 % (422767)------------------------------ % 218.92/31.08 % (422767)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 218.92/31.08 % (422767)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 218.92/31.08 % (422767)CaDiCaL version: 2.1.3 % 218.92/31.08 % (422767)Termination reason: Inappropriate % 218.92/31.08 % (422767)Time elapsed: 0.004 s % 218.92/31.08 % (422767)Peak memory usage: 11 MB % 218.92/31.08 % (422767)Instructions burned: 5 (million) % 218.92/31.08 % (422767)------------------------------ % 218.92/31.08 % (422767)------------------------------ % 300.45/42.54 % (422769)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=1670639224:i=262:bd=preordered:rtra=on:fsd=on_2772 on theBenchmark for (2772ds/262Mi) % 300.45/42.54 % (422769)Instruction limit reached! % 300.45/42.54 % (422769)------------------------------ % 300.45/42.54 % (422769)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.45/42.54 % (422769)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.45/42.54 % (422769)CaDiCaL version: 2.1.3 % 300.45/42.54 % (422769)Termination reason: Instruction limit % 300.45/42.54 % (422769)Termination phase: Saturation % 300.45/42.54 % (422769)Time elapsed: 0.285 s % 300.45/42.54 % (422769)Peak memory usage: 14 MB % 300.45/42.54 % (422769)Instructions burned: 262 (million) % 300.45/42.54 % (422771)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=1042087744:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2769 on theBenchmark for (2769ds/1368Mi) % 300.45/42.54 % (422771)Instruction limit reached! % 300.45/42.54 % (422771)------------------------------ % 300.45/42.54 % (422771)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.45/42.54 % (422771)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.45/42.54 % (422771)CaDiCaL version: 2.1.3 % 300.45/42.54 % (422771)Termination reason: Instruction limit % 300.45/42.54 % (422771)Termination phase: Saturation % 300.45/42.54 % (422771)Time elapsed: 1.283 s % 300.45/42.54 % (422771)Peak memory usage: 19 MB % 300.45/42.54 % (422771)Instructions burned: 1368 (million) % 300.45/42.54 % (422775)ott-21_1_sil=16000:si=on:fs=off:random_seed=2500216492:i=360:av=off:fsr=off:rtra=on_2756 on theBenchmark for (2756ds/360Mi) % 300.45/42.54 % (422775)Instruction limit reached! % 300.45/42.54 % (422775)------------------------------ % 300.45/42.54 % (422775)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.45/42.54 % (422775)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.45/42.54 % (422775)CaDiCaL version: 2.1.3 % 300.45/42.54 % (422775)Termination reason: Instruction limit % 300.45/42.54 % (422775)Termination phase: Saturation % 300.45/42.54 % (422775)Time elapsed: 0.290 s % 300.45/42.54 % (422775)Peak memory usage: 13 MB % 300.45/42.54 % (422775)Instructions burned: 360 (million) % 300.45/42.54 % (422777)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=964153511:i=954:bd=all:rtra=on_2753 on theBenchmark for (2753ds/954Mi) % 300.45/42.54 % (422777)Instruction limit reached! % 300.45/42.54 % (422777)------------------------------ % 300.45/42.54 % (422777)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.45/42.54 % (422777)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.45/42.54 % (422777)CaDiCaL version: 2.1.3 % 300.45/42.54 % (422777)Termination reason: Instruction limit % 300.45/42.54 % (422777)Termination phase: Saturation % 300.45/42.54 % (422777)Time elapsed: 0.998 s % 300.45/42.54 % (422777)Peak memory usage: 16 MB % 300.45/42.54 % (422777)Instructions burned: 954 (million) % 300.45/42.54 % (422781)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=466693632:fmbsr=1.3:i=1730:ins=25:rtra=on_2743 on theBenchmark for (2743ds/1730Mi) % 300.45/42.54 % (422781)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.45/42.54 % (422781)Terminated due to inappropriate strategy. % 300.45/42.54 % (422781)------------------------------ % 300.45/42.54 % (422781)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.45/42.54 % (422781)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.45/42.54 % (422781)CaDiCaL version: 2.1.3 % 300.45/42.54 % (422781)Termination reason: Inappropriate % 300.45/42.54 % (422781)Time elapsed: 0.004 s % 300.45/42.54 % (422781)Peak memory usage: 11 MB % 300.45/42.54 % (422781)Instructions burned: 4 (million) % 300.45/42.54 % (422781)------------------------------ % 300.45/42.54 % (422781)------------------------------ % 300.45/42.54 % (422783)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=4145185380:i=2358:rtra=on_2742 on theBenchmark for (2742ds/2358Mi) % 300.45/42.54 % (422783)Instruction limit reached! % 300.45/42.54 % (422783)------------------------------ % 300.45/42.54 % (422783)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.45/42.54 % (422783)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.45/42.54 % (422783)CaDiCaL version: 2.1.3 % 300.45/42.54 % (422783)Termination reason: Instruction limit % 300.45/42.54 % (422783)Termination p % 300.45/42.54 Terminated % 300.45/42.54 % Vampire exiting % 300.45/42.54 Terminated %------------------------------------------------------------------------------