%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWC438_1 : TPTP v9.3.1. Released v9.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n014.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:06:00 PM UTC 2026 % Result : Timeout 285.97s 40.52s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWC438_1 : TPTP v9.3.1. Released v9.0.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.10/0.20 % Computer : n014.cluster.edu % 0.10/0.20 % Model : x86_64 x86_64 % 0.10/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.20 % Memory : 8046.5625MB % 0.10/0.20 % OS : Linux 6.8.0-71-generic % 0.10/0.20 % CPULimit : 300 % 0.10/0.20 % WCLimit : 300 % 0.10/0.20 % DateTime : Mon Sep 28 09:37:31 UTC 2026 % 0.10/0.20 % CPUTime : % 0.10/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.10/0.23 Running first-order model finding % 0.10/0.23 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.56/0.85 % (1662346)Will run a generic schedule for satisfiability detection. % 3.56/0.85 % (1662356)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=4158713117:i=131_2999 on theBenchmark for (2999ds/131Mi) % 3.56/0.85 % (1662352)% WARNING: option uhcvi not known. % 3.56/0.85 % (1662351)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3553513899_2999 on theBenchmark for (2999ds/0Mi) % 3.56/0.85 % (1662352)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=596976076:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 3.56/0.85 % (1662353)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2693858907:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 3.56/0.85 % (1662354)dis+10_1_sil=32000:sp=arity:random_seed=3279492292:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 3.56/0.85 % (1662355)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2548049894:i=116_2999 on theBenchmark for (2999ds/116Mi) % 3.56/0.85 % (1662351)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.56/0.85 % (1662351)Terminated due to inappropriate strategy. % 3.56/0.85 % (1662351)------------------------------ % 3.56/0.85 % (1662351)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.56/0.85 % (1662351)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.56/0.85 % (1662351)CaDiCaL version: 2.1.3 % 3.56/0.85 % (1662351)Termination reason: Inappropriate % 3.56/0.85 % (1662351)Time elapsed: 0.001 s % 3.56/0.85 % (1662351)Peak memory usage: 10 MB % 3.56/0.85 % (1662351)Instructions burned: 1 (million) % 3.56/0.85 % (1662357)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2740917345:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 3.56/0.85 % (1662351)------------------------------ % 3.56/0.85 % (1662351)------------------------------ % 3.56/0.85 % (1662365)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=741595886:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 3.56/0.85 % (1662365)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.56/0.85 % (1662365)Terminated due to inappropriate strategy. % 3.56/0.85 % (1662365)------------------------------ % 3.56/0.85 % (1662365)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.56/0.85 % (1662365)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.56/0.85 % (1662365)CaDiCaL version: 2.1.3 % 3.56/0.85 % (1662365)Termination reason: Inappropriate % 3.56/0.85 % (1662365)Time elapsed: 0.001 s % 3.56/0.85 % (1662365)Peak memory usage: 10 MB % 3.56/0.85 % (1662365)Instructions burned: 1 (million) % 3.56/0.85 % (1662365)------------------------------ % 3.56/0.85 % (1662365)------------------------------ % 3.56/0.85 % (1662356)Instruction limit reached! % 3.56/0.85 % (1662356)------------------------------ % 3.56/0.85 % (1662356)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.56/0.85 % (1662356)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.56/0.85 % (1662356)CaDiCaL version: 2.1.3 % 3.56/0.85 % (1662356)Termination reason: Instruction limit % 3.56/0.85 % (1662356)Termination phase: Saturation % 3.56/0.85 % (1662356)Time elapsed: 0.044 s % 3.56/0.85 % (1662356)Peak memory usage: 13 MB % 3.56/0.85 % (1662356)Instructions burned: 134 (million) % 3.56/0.85 % (1662367)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3244311089:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 3.56/0.85 % (1662368)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=1496428247:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 3.56/0.85 % (1662354)Instruction limit reached! % 3.56/0.85 % (1662354)------------------------------ % 3.56/0.85 % (1662354)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.56/0.85 % (1662354)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.56/0.85 % (1662354)CaDiCaL version: 2.1.3 % 3.56/0.85 % (1662354)Termination reason: Instruction limit % 3.56/0.85 % (1662354)Termination phase: Saturation % 3.56/0.85 % (1662354)Time elapsed: 0.063 s % 3.56/0.85 % (1662354)Peak memory usage: 12 MB % 3.56/0.85 % (1662354)Instructions burned: 104 (million) % 3.56/0.85 % (1662355)Instruction limit reached! % 3.56/0.85 % (1662355)------------------------------ % 3.56/0.85 % (1662355)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.31/1.16 % (1662355)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.31/1.16 % (1662355)CaDiCaL version: 2.1.3 % 6.31/1.16 % (1662355)Termination reason: Instruction limit % 6.31/1.16 % (1662355)Termination phase: Saturation % 6.31/1.16 % (1662355)Time elapsed: 0.071 s % 6.31/1.16 % (1662355)Peak memory usage: 12 MB % 6.31/1.16 % (1662355)Instructions burned: 116 (million) % 6.31/1.16 % (1662371)ott-21_1_sil=16000:fs=off:random_seed=2291407532:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi) % 6.31/1.16 % (1662372)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1356757132:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 6.31/1.16 % (1662357)Instruction limit reached! % 6.31/1.16 % (1662357)------------------------------ % 6.31/1.16 % (1662357)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.31/1.16 % (1662357)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.31/1.16 % (1662357)CaDiCaL version: 2.1.3 % 6.31/1.16 % (1662357)Termination reason: Instruction limit % 6.31/1.16 % (1662357)Termination phase: Saturation % 6.31/1.16 % (1662357)Time elapsed: 0.101 s % 6.31/1.16 % (1662357)Peak memory usage: 13 MB % 6.31/1.16 % (1662357)Instructions burned: 159 (million) % 6.31/1.16 % (1662375)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=120510493:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 6.31/1.16 % (1662375)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 6.31/1.16 % (1662375)Terminated due to inappropriate strategy. % 6.31/1.16 % (1662375)------------------------------ % 6.31/1.16 % (1662375)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.31/1.16 % (1662375)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.31/1.16 % (1662375)CaDiCaL version: 2.1.3 % 6.31/1.16 % (1662375)Termination reason: Inappropriate % 6.31/1.16 % (1662375)Time elapsed: 0.001 s % 6.31/1.16 % (1662375)Peak memory usage: 10 MB % 6.31/1.16 % (1662375)Instructions burned: 1 (million) % 6.31/1.16 % (1662375)------------------------------ % 6.31/1.16 % (1662375)------------------------------ % 6.31/1.16 % (1662367)Instruction limit reached! % 6.31/1.16 % (1662367)------------------------------ % 6.31/1.16 % (1662367)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.31/1.16 % (1662367)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.31/1.16 % (1662367)CaDiCaL version: 2.1.3 % 6.31/1.16 % (1662367)Termination reason: Instruction limit % 6.31/1.16 % (1662367)Termination phase: Saturation % 6.31/1.16 % (1662367)Time elapsed: 0.087 s % 6.31/1.16 % (1662367)Peak memory usage: 13 MB % 6.31/1.16 % (1662367)Instructions burned: 132 (million) % 6.31/1.16 % (1662377)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=473734594:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 6.31/1.16 % (1662378)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=6569587:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 6.31/1.16 % (1662378)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 6.31/1.16 % (1662378)Terminated due to inappropriate strategy. % 6.31/1.16 % (1662378)------------------------------ % 6.31/1.16 % (1662378)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.31/1.16 % (1662378)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.31/1.16 % (1662378)CaDiCaL version: 2.1.3 % 6.31/1.16 % (1662378)Termination reason: Inappropriate % 6.31/1.16 % (1662378)Time elapsed: 0.001 s % 6.31/1.16 % (1662378)Peak memory usage: 10 MB % 6.31/1.16 % (1662378)Instructions burned: 1 (million) % 6.31/1.16 % (1662378)------------------------------ % 6.31/1.16 % (1662378)------------------------------ % 6.31/1.16 % (1662371)Instruction limit reached! % 6.31/1.16 % (1662371)------------------------------ % 6.31/1.16 % (1662371)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.31/1.16 % (1662371)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.31/1.16 % (1662371)CaDiCaL version: 2.1.3 % 6.31/1.16 % (1662371)Termination reason: Instruction limit % 6.31/1.16 % (1662371)Termination phase: Saturation % 6.31/1.16 % (1662371)Time elapsed: 0.079 s % 6.31/1.16 % (1662371)Peak memory usage: 12 MB % 6.31/1.16 % (1662371)Instructions burned: 180 (million) % 6.31/1.16 % (1662381)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=1319322699: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) % 17.96/3.03 % (1662382)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3086528076:i=879:kws=inv_precedence:fsr=off_2998 on theBenchmark for (2998ds/879Mi) % 17.96/3.03 % (1662368)Instruction limit reached! % 17.96/3.03 % (1662368)------------------------------ % 17.96/3.03 % (1662368)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.96/3.03 % (1662368)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.96/3.03 % (1662368)CaDiCaL version: 2.1.3 % 17.96/3.03 % (1662368)Termination reason: Instruction limit % 17.96/3.03 % (1662368)Termination phase: Saturation % 17.96/3.03 % (1662368)Time elapsed: 0.190 s % 17.96/3.03 % (1662368)Peak memory usage: 17 MB % 17.96/3.03 % (1662368)Instructions burned: 685 (million) % 17.96/3.03 % (1662385)fmb+10_1_sil=64000:random_seed=837820171:i=22061:nm=2:gsp=on_2997 on theBenchmark for (2997ds/22061Mi) % 17.96/3.03 % (1662385)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 17.96/3.03 % (1662385)Terminated due to inappropriate strategy. % 17.96/3.03 % (1662385)------------------------------ % 17.96/3.03 % (1662385)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.96/3.03 % (1662385)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.96/3.03 % (1662385)CaDiCaL version: 2.1.3 % 17.96/3.03 % (1662385)Termination reason: Inappropriate % 17.96/3.03 % (1662385)Time elapsed: 0.0000 s % 17.96/3.03 % (1662385)Peak memory usage: 11 MB % 17.96/3.03 % (1662385)Instructions burned: 1 (million) % 17.96/3.03 % (1662385)------------------------------ % 17.96/3.03 % (1662385)------------------------------ % 17.96/3.03 % (1662387)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3343566409:i=9515:nm=5_2997 on theBenchmark for (2997ds/9515Mi) % 17.96/3.03 % (1662387)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 17.96/3.03 % (1662387)Terminated due to inappropriate strategy. % 17.96/3.03 % (1662387)------------------------------ % 17.96/3.03 % (1662387)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.96/3.03 % (1662387)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.96/3.03 % (1662387)CaDiCaL version: 2.1.3 % 17.96/3.03 % (1662387)Termination reason: Inappropriate % 17.96/3.03 % (1662387)Time elapsed: 0.0000 s % 17.96/3.03 % (1662387)Peak memory usage: 10 MB % 17.96/3.03 % (1662387)Instructions burned: 1 (million) % 17.96/3.03 % (1662387)------------------------------ % 17.96/3.03 % (1662387)------------------------------ % 17.96/3.03 % (1662389)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3412767018:fmbsr=1.7:i=920_2997 on theBenchmark for (2997ds/920Mi) % 17.96/3.03 % (1662389)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 17.96/3.03 % (1662389)Terminated due to inappropriate strategy. % 17.96/3.03 % (1662389)------------------------------ % 17.96/3.03 % (1662389)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.96/3.03 % (1662389)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.96/3.03 % (1662389)CaDiCaL version: 2.1.3 % 17.96/3.03 % (1662389)Termination reason: Inappropriate % 17.96/3.03 % (1662389)Time elapsed: 0.0000 s % 17.96/3.03 % (1662389)Peak memory usage: 11 MB % 17.96/3.03 % (1662389)Instructions burned: 1 (million) % 17.96/3.03 % (1662389)------------------------------ % 17.96/3.03 % (1662389)------------------------------ % 17.96/3.03 % (1662391)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3510874514:i=5131_2996 on theBenchmark for (2996ds/5131Mi) % 17.96/3.03 % (1662372)Instruction limit reached! % 17.96/3.03 % (1662372)------------------------------ % 17.96/3.03 % (1662372)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.96/3.03 % (1662372)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.96/3.03 % (1662372)CaDiCaL version: 2.1.3 % 17.96/3.03 % (1662372)Termination reason: Instruction limit % 17.96/3.03 % (1662372)Termination phase: Saturation % 17.96/3.03 % (1662372)Time elapsed: 0.292 s % 17.96/3.03 % (1662372)Peak memory usage: 14 MB % 17.96/3.03 % (1662372)Instructions burned: 477 (million) % 17.96/3.03 % (1662393)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=22960710:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi) % 17.96/3.03 % (1662381)Instruction limit reached! % 17.96/3.03 % (1662381)------------------------------ % 28.06/4.28 % (1662381)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.06/4.28 % (1662381)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.06/4.28 % (1662381)CaDiCaL version: 2.1.3 % 28.06/4.28 % (1662381)Termination reason: Instruction limit % 28.06/4.28 % (1662381)Termination phase: Saturation % 28.06/4.28 % (1662381)Time elapsed: 0.406 s % 28.06/4.28 % (1662381)Peak memory usage: 20 MB % 28.06/4.28 % (1662381)Instructions burned: 693 (million) % 28.06/4.28 % (1662395)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3868188084:i=6324_2993 on theBenchmark for (2993ds/6324Mi) % 28.06/4.28 % (1662395)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 28.06/4.28 % (1662395)Terminated due to inappropriate strategy. % 28.06/4.28 % (1662395)------------------------------ % 28.06/4.28 % (1662395)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.06/4.28 % (1662395)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.06/4.28 % (1662395)CaDiCaL version: 2.1.3 % 28.06/4.28 % (1662395)Termination reason: Inappropriate % 28.06/4.28 % (1662395)Time elapsed: 0.001 s % 28.06/4.28 % (1662395)Peak memory usage: 10 MB % 28.06/4.28 % (1662395)Instructions burned: 1 (million) % 28.06/4.28 % (1662395)------------------------------ % 28.06/4.28 % (1662395)------------------------------ % 28.06/4.28 % (1662397)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3535410486:fmbsr=2.30978:i=2174_2993 on theBenchmark for (2993ds/2174Mi) % 28.06/4.28 % (1662397)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 28.06/4.28 % (1662397)Terminated due to inappropriate strategy. % 28.06/4.28 % (1662397)------------------------------ % 28.06/4.28 % (1662397)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.06/4.28 % (1662397)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.06/4.28 % (1662397)CaDiCaL version: 2.1.3 % 28.06/4.28 % (1662397)Termination reason: Inappropriate % 28.06/4.28 % (1662397)Time elapsed: 0.001 s % 28.06/4.28 % (1662397)Peak memory usage: 10 MB % 28.06/4.28 % (1662397)Instructions burned: 1 (million) % 28.06/4.28 % (1662397)------------------------------ % 28.06/4.28 % (1662397)------------------------------ % 28.06/4.28 % (1662399)ott-2_1_sil=16000:newcnf=on:random_seed=1665344371:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2993 on theBenchmark for (2993ds/869Mi) % 28.06/4.28 % (1662382)Instruction limit reached! % 28.06/4.28 % (1662382)------------------------------ % 28.06/4.28 % (1662382)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.06/4.28 % (1662382)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.06/4.28 % (1662382)CaDiCaL version: 2.1.3 % 28.06/4.28 % (1662382)Termination reason: Instruction limit % 28.06/4.28 % (1662382)Termination phase: Saturation % 28.06/4.28 % (1662382)Time elapsed: 0.497 s % 28.06/4.28 % (1662382)Peak memory usage: 18 MB % 28.06/4.28 % (1662382)Instructions burned: 881 (million) % 28.06/4.28 % (1662401)ott+10_1_sil=32000:tgt=ground:random_seed=2911880646:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi) % 28.06/4.28 % (1662377)Instruction limit reached! % 28.06/4.28 % (1662377)------------------------------ % 28.06/4.28 % (1662377)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.06/4.28 % (1662377)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.06/4.28 % (1662377)CaDiCaL version: 2.1.3 % 28.06/4.28 % (1662377)Termination reason: Instruction limit % 28.06/4.28 % (1662377)Termination phase: Saturation % 28.06/4.28 % (1662377)Time elapsed: 0.724 s % 28.06/4.28 % (1662377)Peak memory usage: 18 MB % 28.06/4.28 % (1662377)Instructions burned: 1179 (million) % 28.06/4.28 % (1662403)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3778520299:i=54282_2990 on theBenchmark for (2990ds/54282Mi) % 28.06/4.28 % (1662403)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 28.06/4.28 % (1662403)Terminated due to inappropriate strategy. % 28.06/4.28 % (1662403)------------------------------ % 28.06/4.28 % (1662403)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.06/4.28 % (1662403)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.06/4.28 % (1662403)CaDiCaL version: 2.1.3 % 28.06/4.28 % (1662403)Termination reason: Inappropriate % 28.06/4.28 % (1662403)Time elapsed: 0.001 s % 28.06/4.28 % (1662403)Peak memory usage: 10 MB % 28.06/4.28 % (1662403)Instructions burned: 1 (million) % 85.59/12.36 % (1662403)------------------------------ % 85.59/12.36 % (1662403)------------------------------ % 85.59/12.36 % (1662405)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=4045739781:i=3512:aac=none_2990 on theBenchmark for (2990ds/3512Mi) % 85.59/12.36 % (1662399)Instruction limit reached! % 85.59/12.36 % (1662399)------------------------------ % 85.59/12.36 % (1662399)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 85.59/12.36 % (1662399)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 85.59/12.36 % (1662399)CaDiCaL version: 2.1.3 % 85.59/12.36 % (1662399)Termination reason: Instruction limit % 85.59/12.36 % (1662399)Termination phase: Saturation % 85.59/12.36 % (1662399)Time elapsed: 0.530 s % 85.59/12.36 % (1662399)Peak memory usage: 14 MB % 85.59/12.36 % (1662399)Instructions burned: 870 (million) % 85.59/12.36 % (1662407)dis+21_1_sil=32000:sas=cadical:random_seed=2478567569:i=3773:amm=off_2987 on theBenchmark for (2987ds/3773Mi) % 85.59/12.36 % (1662393)Instruction limit reached! % 85.59/12.36 % (1662393)------------------------------ % 85.59/12.36 % (1662393)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 85.59/12.36 % (1662393)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 85.59/12.36 % (1662393)CaDiCaL version: 2.1.3 % 85.59/12.36 % (1662393)Termination reason: Instruction limit % 85.59/12.36 % (1662393)Termination phase: Saturation % 85.59/12.36 % (1662393)Time elapsed: 0.877 s % 85.59/12.36 % (1662393)Peak memory usage: 26 MB % 85.59/12.36 % (1662393)Instructions burned: 1473 (million) % 85.59/12.36 % (1662409)ott+11_1_sil=16000:gs=on:random_seed=1921731793:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2986 on theBenchmark for (2986ds/2251Mi) % 85.59/12.36 % (1662391)Instruction limit reached! % 85.59/12.36 % (1662391)------------------------------ % 85.59/12.36 % (1662391)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 85.59/12.36 % (1662391)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 85.59/12.36 % (1662391)CaDiCaL version: 2.1.3 % 85.59/12.36 % (1662391)Termination reason: Instruction limit % 85.59/12.36 % (1662391)Termination phase: Saturation % 85.59/12.36 % (1662391)Time elapsed: 1.480 s % 85.59/12.36 % (1662391)Peak memory usage: 42 MB % 85.59/12.36 % (1662391)Instructions burned: 5133 (million) % 85.59/12.36 % (1662411)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1936840021:fmbsr=1.6:i=67534_2982 on theBenchmark for (2982ds/67534Mi) % 85.59/12.36 % (1662411)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 85.59/12.36 % (1662411)Terminated due to inappropriate strategy. % 85.59/12.36 % (1662411)------------------------------ % 85.59/12.36 % (1662411)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 85.59/12.36 % (1662411)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 85.59/12.36 % (1662411)CaDiCaL version: 2.1.3 % 85.59/12.36 % (1662411)Termination reason: Inappropriate % 85.59/12.36 % (1662411)Time elapsed: 0.0000 s % 85.59/12.36 % (1662411)Peak memory usage: 10 MB % 85.59/12.36 % (1662411)Instructions burned: 1 (million) % 85.59/12.36 % (1662411)------------------------------ % 85.59/12.36 % (1662411)------------------------------ % 85.59/12.36 % (1662413)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2142759723:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2981 on theBenchmark for (2981ds/4591Mi) % 85.59/12.36 % (1662409)Instruction limit reached! % 85.59/12.36 % (1662409)------------------------------ % 85.59/12.36 % (1662409)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 85.59/12.36 % (1662409)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 85.59/12.36 % (1662409)CaDiCaL version: 2.1.3 % 85.59/12.36 % (1662409)Termination reason: Instruction limit % 85.59/12.36 % (1662409)Termination phase: Saturation % 85.59/12.36 % (1662409)Time elapsed: 1.254 s % 85.59/12.36 % (1662409)Peak memory usage: 23 MB % 85.59/12.36 % (1662409)Instructions burned: 2252 (million) % 85.59/12.36 % (1662415)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2229321014:i=29340_2974 on theBenchmark for (2974ds/29340Mi) % 85.59/12.36 % (1662405)Instruction limit reached! % 85.59/12.36 % (1662405)------------------------------ % 85.59/12.36 % (1662405)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 85.59/12.36 % (1662405)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 85.59/12.36 % (1662405)CaDiCaL version: 2.1.3 % 85.59/12.36 % (1662405)Termination reason: Instruction limit % 131.68/18.87 % (1662405)Termination phase: Saturation % 131.68/18.87 % (1662405)Time elapsed: 1.851 s % 131.68/18.87 % (1662405)Peak memory usage: 35 MB % 131.68/18.87 % (1662405)Instructions burned: 3513 (million) % 131.68/18.87 % (1662417)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=1958676459:i=5211_2972 on theBenchmark for (2972ds/5211Mi) % 131.68/18.87 % (1662413)Instruction limit reached! % 131.68/18.87 % (1662413)------------------------------ % 131.68/18.87 % (1662413)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 131.68/18.87 % (1662413)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.68/18.87 % (1662413)CaDiCaL version: 2.1.3 % 131.68/18.87 % (1662413)Termination reason: Instruction limit % 131.68/18.87 % (1662413)Termination phase: Saturation % 131.68/18.87 % (1662413)Time elapsed: 1.323 s % 131.68/18.87 % (1662413)Peak memory usage: 45 MB % 131.68/18.87 % (1662413)Instructions burned: 4594 (million) % 131.68/18.87 % (1662419)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=990192478:i=5497:nm=2_2968 on theBenchmark for (2968ds/5497Mi) % 131.68/18.87 % (1662419)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 131.68/18.87 % (1662419)Terminated due to inappropriate strategy. % 131.68/18.87 % (1662419)------------------------------ % 131.68/18.87 % (1662419)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 131.68/18.87 % (1662419)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.68/18.87 % (1662419)CaDiCaL version: 2.1.3 % 131.68/18.87 % (1662419)Termination reason: Inappropriate % 131.68/18.87 % (1662419)Time elapsed: 0.0000 s % 131.68/18.87 % (1662419)Peak memory usage: 10 MB % 131.68/18.87 % (1662419)Instructions burned: 1 (million) % 131.68/18.87 % (1662419)------------------------------ % 131.68/18.87 % (1662419)------------------------------ % 131.68/18.87 % (1662421)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1679937849:fmbsr=2:i=46332_2968 on theBenchmark for (2968ds/46332Mi) % 131.68/18.87 % (1662421)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 131.68/18.87 % (1662421)Terminated due to inappropriate strategy. % 131.68/18.87 % (1662421)------------------------------ % 131.68/18.87 % (1662421)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 131.68/18.87 % (1662421)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.68/18.87 % (1662421)CaDiCaL version: 2.1.3 % 131.68/18.87 % (1662421)Termination reason: Inappropriate % 131.68/18.87 % (1662421)Time elapsed: 0.0000 s % 131.68/18.87 % (1662421)Peak memory usage: 10 MB % 131.68/18.87 % (1662421)Instructions burned: 1 (million) % 131.68/18.87 % (1662421)------------------------------ % 131.68/18.87 % (1662421)------------------------------ % 131.68/18.87 % (1662423)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=257940927:i=14071_2968 on theBenchmark for (2968ds/14071Mi) % 131.68/18.87 % (1662423)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 131.68/18.87 % (1662423)Terminated due to inappropriate strategy. % 131.68/18.87 % (1662423)------------------------------ % 131.68/18.87 % (1662423)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 131.68/18.87 % (1662423)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.68/18.87 % (1662423)CaDiCaL version: 2.1.3 % 131.68/18.87 % (1662423)Termination reason: Inappropriate % 131.68/18.87 % (1662423)Time elapsed: 0.0000 s % 131.68/18.87 % (1662423)Peak memory usage: 10 MB % 131.68/18.87 % (1662423)Instructions burned: 1 (million) % 131.68/18.87 % (1662423)------------------------------ % 131.68/18.87 % (1662423)------------------------------ % 131.68/18.87 % (1662425)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1917466539:i=22565:add=on:rawr=on_2968 on theBenchmark for (2968ds/22565Mi) % 131.68/18.87 % (1662407)Instruction limit reached! % 131.68/18.87 % (1662407)------------------------------ % 131.68/18.87 % (1662407)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 131.68/18.87 % (1662407)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.68/18.87 % (1662407)CaDiCaL version: 2.1.3 % 131.68/18.87 % (1662407)Termination reason: Instruction limit % 131.68/18.87 % (1662407)Termination phase: Saturation % 131.68/18.87 % (1662407)Time elapsed: 2.024 s % 131.68/18.87 % (1662407)Peak memory usage: 31 MB % 131.68/18.87 % (1662407)Instructions burned: 3773 (million) % 131.68/18.87 % (1662427)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=3322533571:i=8173:av=off_2967 on theBenchmark for (2967ds/8173Mi) % 131.68/18.87 % (1662401)Instruction limit reached! % 132.28/18.97 % (1662401)------------------------------ % 132.28/18.97 % (1662401)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 132.28/18.97 % (1662401)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 132.28/18.97 % (1662401)CaDiCaL version: 2.1.3 % 132.28/18.97 % (1662401)Termination reason: Instruction limit % 132.28/18.97 % (1662401)Termination phase: Saturation % 132.28/18.97 % (1662401)Time elapsed: 3.307 s % 132.28/18.97 % (1662401)Peak memory usage: 40 MB % 132.28/18.97 % (1662401)Instructions burned: 5116 (million) % 132.28/18.97 % (1662429)dis+10_16:1_sil=16000:random_seed=737509548:i=9155:fsr=off_2959 on theBenchmark for (2959ds/9155Mi) % 132.28/18.97 % (1662417)Instruction limit reached! % 132.28/18.97 % (1662417)------------------------------ % 132.28/18.97 % (1662417)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 132.28/18.97 % (1662417)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 132.28/18.97 % (1662417)CaDiCaL version: 2.1.3 % 132.28/18.97 % (1662417)Termination reason: Instruction limit % 132.28/18.97 % (1662417)Termination phase: Saturation % 132.28/18.97 % (1662417)Time elapsed: 2.772 s % 132.28/18.97 % (1662417)Peak memory usage: 51 MB % 132.28/18.97 % (1662417)Instructions burned: 5212 (million) % 132.28/18.97 % (1662431)ott-3_8_sil=64000:random_seed=2998414415:i=20139:bs=on_2944 on theBenchmark for (2944ds/20139Mi) % 132.28/18.97 % (1662425)Instruction limit reached! % 132.28/18.97 % (1662425)------------------------------ % 132.28/18.97 % (1662425)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 132.28/18.97 % (1662425)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 132.28/18.97 % (1662425)CaDiCaL version: 2.1.3 % 132.28/18.97 % (1662425)Termination reason: Instruction limit % 132.28/18.97 % (1662425)Termination phase: Saturation % 132.28/18.97 % (1662425)Time elapsed: 5.061 s % 132.28/18.97 % (1662425)Peak memory usage: 78 MB % 132.28/18.97 % (1662425)Instructions burned: 22568 (million) % 132.28/18.97 % (1662433)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=903530026:fmbsr=2:i=32576_2917 on theBenchmark for (2917ds/32576Mi) % 132.28/18.97 % (1662433)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 132.28/18.97 % (1662433)Terminated due to inappropriate strategy. % 132.28/18.97 % (1662433)------------------------------ % 132.28/18.97 % (1662433)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 132.28/18.97 % (1662433)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 132.28/18.97 % (1662433)CaDiCaL version: 2.1.3 % 132.28/18.97 % (1662433)Termination reason: Inappropriate % 132.28/18.97 % (1662433)Time elapsed: 0.001 s % 132.28/18.97 % (1662433)Peak memory usage: 10 MB % 132.28/18.97 % (1662433)Instructions burned: 1 (million) % 132.28/18.97 % (1662433)------------------------------ % 132.28/18.97 % (1662433)------------------------------ % 132.28/18.97 % (1662435)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=1848688246:i=11404_2917 on theBenchmark for (2917ds/11404Mi) % 132.28/18.97 % (1662427)Instruction limit reached! % 132.28/18.97 % (1662427)------------------------------ % 132.28/18.97 % (1662427)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 132.28/18.97 % (1662427)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 132.28/18.97 % (1662427)CaDiCaL version: 2.1.3 % 132.28/18.97 % (1662427)Termination reason: Instruction limit % 132.28/18.97 % (1662427)Termination phase: Saturation % 132.28/18.97 % (1662427)Time elapsed: 5.109 s % 132.28/18.97 % (1662427)Peak memory usage: 54 MB % 132.28/18.97 % (1662427)Instructions burned: 8173 (million) % 132.28/18.97 % (1662437)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=3486218844:i=14134_2916 on theBenchmark for (2916ds/14134Mi) % 132.28/18.97 % (1662429)Instruction limit reached! % 132.28/18.97 % (1662429)------------------------------ % 132.28/18.97 % (1662429)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 132.28/18.97 % (1662429)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 132.28/18.97 % (1662429)CaDiCaL version: 2.1.3 % 132.28/18.97 % (1662429)Termination reason: Instruction limit % 132.28/18.97 % (1662429)Termination phase: Saturation % 132.28/18.97 % (1662429)Time elapsed: 4.608 s % 132.28/18.97 % (1662429)Peak memory usage: 52 MB % 132.28/18.97 % (1662429)Instructions burned: 9156 (million) % 132.28/18.97 % (1662439)dis+33_16_sil=32000:sac=on:random_seed=4103389495:i=15851:nm=0_2913 on theBenchmark for (2913ds/15851Mi) % 132.28/18.97 % (1662435)Instruction limit reached! % 132.28/18.97 % (1662435)------------------------------ % 132.28/18.97 % (1662435)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 148.77/21.30 % (1662435)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.77/21.30 % (1662435)CaDiCaL version: 2.1.3 % 148.77/21.30 % (1662435)Termination reason: Instruction limit % 148.77/21.30 % (1662435)Termination phase: Saturation % 148.77/21.30 % (1662435)Time elapsed: 3.821 s % 148.77/21.30 % (1662435)Peak memory usage: 62 MB % 148.77/21.30 % (1662435)Instructions burned: 11405 (million) % 148.77/21.30 % (1662441)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=652712657:avsq=on:i=17627:add=on:amm=off_2878 on theBenchmark for (2878ds/17627Mi) % 148.77/21.30 % (1662439)Instruction limit reached! % 148.77/21.30 % (1662439)------------------------------ % 148.77/21.30 % (1662439)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 148.77/21.30 % (1662439)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.77/21.30 % (1662439)CaDiCaL version: 2.1.3 % 148.77/21.30 % (1662439)Termination reason: Instruction limit % 148.77/21.30 % (1662439)Termination phase: Saturation % 148.77/21.30 % (1662439)Time elapsed: 7.920 s % 148.77/21.30 % (1662439)Peak memory usage: 201 MB % 148.77/21.30 % (1662439)Instructions burned: 15851 (million) % 148.77/21.30 % (1662747)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=3651719125:s2a=on:i=53295_2833 on theBenchmark for (2833ds/53295Mi) % 148.77/21.30 % (1662415)Instruction limit reached! % 148.77/21.30 % (1662415)------------------------------ % 148.77/21.30 % (1662415)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 148.77/21.30 % (1662415)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.77/21.30 % (1662415)CaDiCaL version: 2.1.3 % 148.77/21.30 % (1662415)Termination reason: Instruction limit % 148.77/21.30 % (1662415)Termination phase: Saturation % 148.77/21.30 % (1662415)Time elapsed: 15.756 s % 148.77/21.30 % (1662415)Peak memory usage: 124 MB % 148.77/21.30 % (1662415)Instructions burned: 29341 (million) % 148.77/21.30 % (1662755)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=2774458711:i=26857:ins=20_2816 on theBenchmark for (2816ds/26857Mi) % 148.77/21.30 % (1662755)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 148.77/21.30 % (1662755)Terminated due to inappropriate strategy. % 148.77/21.30 % (1662755)------------------------------ % 148.77/21.30 % (1662755)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 148.77/21.30 % (1662755)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.77/21.30 % (1662755)CaDiCaL version: 2.1.3 % 148.77/21.30 % (1662755)Termination reason: Inappropriate % 148.77/21.30 % (1662755)Time elapsed: 0.001 s % 148.77/21.30 % (1662755)Peak memory usage: 10 MB % 148.77/21.30 % (1662755)Instructions burned: 1 (million) % 148.77/21.30 % (1662755)------------------------------ % 148.77/21.30 % (1662755)------------------------------ % 148.77/21.30 % (1662757)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=2998003135:i=28120:bs=on:fsr=off_2815 on theBenchmark for (2815ds/28120Mi) % 148.77/21.30 % (1662441)Instruction limit reached! % 148.77/21.30 % (1662441)------------------------------ % 148.77/21.30 % (1662441)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 148.77/21.30 % (1662441)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.77/21.30 % (1662441)CaDiCaL version: 2.1.3 % 148.77/21.30 % (1662441)Termination reason: Instruction limit % 148.77/21.30 % (1662441)Termination phase: Saturation % 148.77/21.30 % (1662441)Time elapsed: 6.441 s % 148.77/21.30 % (1662441)Peak memory usage: 79 MB % 148.77/21.30 % (1662441)Instructions burned: 17627 (million) % 148.77/21.30 % (1662759)fmb+10_1_sil=256000:fmbss=7:random_seed=1667634114:fmbsr=1.6:i=182295_2814 on theBenchmark for (2814ds/182295Mi) % 148.77/21.30 % (1662759)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 148.77/21.30 % (1662759)Terminated due to inappropriate strategy. % 148.77/21.30 % (1662759)------------------------------ % 148.77/21.30 % (1662759)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 148.77/21.30 % (1662759)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.77/21.30 % (1662759)CaDiCaL version: 2.1.3 % 148.77/21.30 % (1662759)Termination reason: Inappropriate % 148.77/21.30 % (1662759)Time elapsed: 0.001 s % 148.77/21.30 % (1662759)Peak memory usage: 10 MB % 148.77/21.30 % (1662759)Instructions burned: 1 (million) % 148.77/21.30 % (1662759)------------------------------ % 148.77/21.30 % (1662759)------------------------------ % 148.77/21.30 % (1662761)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=2142472259:i=44625:gsp=on_2813 on theBenchmark for (2813ds/44625Mi) % 170.07/24.23 % (1662761)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 170.07/24.23 % (1662761)Terminated due to inappropriate strategy. % 170.07/24.23 % (1662761)------------------------------ % 170.07/24.23 % (1662761)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 170.07/24.23 % (1662761)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 170.07/24.23 % (1662761)CaDiCaL version: 2.1.3 % 170.07/24.23 % (1662761)Termination reason: Inappropriate % 170.07/24.23 % (1662761)Time elapsed: 0.002 s % 170.07/24.23 % (1662761)Peak memory usage: 11 MB % 170.07/24.23 % (1662761)Instructions burned: 1 (million) % 170.07/24.23 % (1662761)------------------------------ % 170.07/24.23 % (1662761)------------------------------ % 170.07/24.23 % (1662763)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=2635101031:i=160505_2813 on theBenchmark for (2813ds/160505Mi) % 170.07/24.23 % (1662763)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 170.07/24.23 % (1662763)Terminated due to inappropriate strategy. % 170.07/24.23 % (1662763)------------------------------ % 170.07/24.23 % (1662763)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 170.07/24.23 % (1662763)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 170.07/24.23 % (1662763)CaDiCaL version: 2.1.3 % 170.07/24.23 % (1662763)Termination reason: Inappropriate % 170.07/24.23 % (1662763)Time elapsed: 0.001 s % 170.07/24.23 % (1662763)Peak memory usage: 11 MB % 170.07/24.23 % (1662763)Instructions burned: 1 (million) % 170.07/24.23 % (1662763)------------------------------ % 170.07/24.23 % (1662763)------------------------------ % 170.07/24.23 % (1662765)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=3885489450:fmbsr=1.3:i=225729_2813 on theBenchmark for (2813ds/225729Mi) % 170.07/24.23 % (1662765)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 170.07/24.23 % (1662765)Terminated due to inappropriate strategy. % 170.07/24.23 % (1662765)------------------------------ % 170.07/24.23 % (1662765)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 170.07/24.23 % (1662765)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 170.07/24.23 % (1662765)CaDiCaL version: 2.1.3 % 170.07/24.23 % (1662765)Termination reason: Inappropriate % 170.07/24.23 % (1662765)Time elapsed: 0.001 s % 170.07/24.23 % (1662765)Peak memory usage: 10 MB % 170.07/24.23 % (1662765)Instructions burned: 1 (million) % 170.07/24.23 % (1662765)------------------------------ % 170.07/24.23 % (1662765)------------------------------ % 170.07/24.23 % (1662437)Instruction limit reached! % 170.07/24.23 % (1662437)------------------------------ % 170.07/24.23 % (1662437)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 170.07/24.23 % (1662437)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 170.07/24.23 % (1662437)CaDiCaL version: 2.1.3 % 170.07/24.23 % (1662437)Termination reason: Instruction limit % 170.07/24.23 % (1662437)Termination phase: Saturation % 170.07/24.23 % (1662437)Time elapsed: 10.284 s % 170.07/24.23 % (1662437)Peak memory usage: 77 MB % 170.07/24.23 % (1662437)Instructions burned: 14134 (million) % 170.07/24.23 % (1662767)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=305828720:fmbsr=2:i=185024:ins=7_2813 on theBenchmark for (2813ds/185024Mi) % 170.07/24.23 % (1662767)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 170.07/24.23 % (1662767)Terminated due to inappropriate strategy. % 170.07/24.23 % (1662767)------------------------------ % 170.07/24.23 % (1662767)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 170.07/24.23 % (1662767)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 170.07/24.23 % (1662767)CaDiCaL version: 2.1.3 % 170.07/24.23 % (1662767)Termination reason: Inappropriate % 170.07/24.23 % (1662767)Time elapsed: 0.001 s % 170.07/24.23 % (1662767)Peak memory usage: 11 MB % 170.07/24.23 % (1662767)Instructions burned: 1 (million) % 170.07/24.23 % (1662767)------------------------------ % 170.07/24.23 % (1662767)------------------------------ % 170.07/24.23 % (1662770)% WARNING: option uhcvi not known. % 170.07/24.23 % (1662770)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=4122219645:i=271062:add=off:rtra=on:rawr=on_2812 on theBenchmark for (2812ds/271062Mi) % 170.07/24.23 % (1662769)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=2719544433:rtra=on_2812 on theBenchmark for (2812ds/0Mi) % 170.07/24.23 % (1662769)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 206.24/29.33 % (1662769)Terminated due to inappropriate strategy. % 206.24/29.33 % (1662769)------------------------------ % 206.24/29.33 % (1662769)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 206.24/29.33 % (1662769)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.24/29.33 % (1662769)CaDiCaL version: 2.1.3 % 206.24/29.33 % (1662769)Termination reason: Inappropriate % 206.24/29.33 % (1662769)Time elapsed: 0.001 s % 206.24/29.33 % (1662769)Peak memory usage: 11 MB % 206.24/29.33 % (1662769)Instructions burned: 1 (million) % 206.24/29.33 % (1662769)------------------------------ % 206.24/29.33 % (1662769)------------------------------ % 206.24/29.33 % (1662773)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3700574766:i=176048:add=on:rtra=on:rawr=on_2812 on theBenchmark for (2812ds/176048Mi) % 206.24/29.33 % (1662431)Instruction limit reached! % 206.24/29.33 % (1662431)------------------------------ % 206.24/29.33 % (1662431)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 206.24/29.33 % (1662431)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.24/29.33 % (1662431)CaDiCaL version: 2.1.3 % 206.24/29.33 % (1662431)Termination reason: Instruction limit % 206.24/29.33 % (1662431)Termination phase: Saturation % 206.24/29.33 % (1662431)Time elapsed: 14.202 s % 206.24/29.33 % (1662431)Peak memory usage: 75 MB % 206.24/29.33 % (1662431)Instructions burned: 20139 (million) % 206.24/29.33 % (1662779)dis+10_1_sil=32000:si=on:sp=arity:random_seed=416496363:i=206:fgj=on:rtra=on_2801 on theBenchmark for (2801ds/206Mi) % 206.24/29.33 % (1662779)Instruction limit reached! % 206.24/29.33 % (1662779)------------------------------ % 206.24/29.33 % (1662779)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 206.24/29.33 % (1662779)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.24/29.33 % (1662779)CaDiCaL version: 2.1.3 % 206.24/29.33 % (1662779)Termination reason: Instruction limit % 206.24/29.33 % (1662779)Termination phase: Saturation % 206.24/29.33 % (1662779)Time elapsed: 0.209 s % 206.24/29.33 % (1662779)Peak memory usage: 13 MB % 206.24/29.33 % (1662779)Instructions burned: 207 (million) % 206.24/29.33 % (1662789)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=18036004:i=232:rtra=on_2799 on theBenchmark for (2799ds/232Mi) % 206.24/29.33 % (1662789)Instruction limit reached! % 206.24/29.33 % (1662789)------------------------------ % 206.24/29.33 % (1662789)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 206.24/29.33 % (1662789)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.24/29.33 % (1662789)CaDiCaL version: 2.1.3 % 206.24/29.33 % (1662789)Termination reason: Instruction limit % 206.24/29.33 % (1662789)Termination phase: Saturation % 206.24/29.33 % (1662789)Time elapsed: 0.271 s % 206.24/29.33 % (1662789)Peak memory usage: 13 MB % 206.24/29.33 % (1662789)Instructions burned: 232 (million) % 206.24/29.33 % (1662793)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=4273803832:i=262:rtra=on_2796 on theBenchmark for (2796ds/262Mi) % 206.24/29.33 % (1662793)Instruction limit reached! % 206.24/29.33 % (1662793)------------------------------ % 206.24/29.33 % (1662793)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 206.24/29.33 % (1662793)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.24/29.33 % (1662793)CaDiCaL version: 2.1.3 % 206.24/29.33 % (1662793)Termination reason: Instruction limit % 206.24/29.33 % (1662793)Termination phase: Saturation % 206.24/29.33 % (1662793)Time elapsed: 0.230 s % 206.24/29.33 % (1662793)Peak memory usage: 13 MB % 206.24/29.33 % (1662793)Instructions burned: 262 (million) % 206.24/29.33 % (1662795)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=1467440836:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2793 on theBenchmark for (2793ds/318Mi) % 206.24/29.33 % (1662795)Instruction limit reached! % 206.24/29.33 % (1662795)------------------------------ % 206.24/29.33 % (1662795)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 206.24/29.33 % (1662795)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.24/29.33 % (1662795)CaDiCaL version: 2.1.3 % 206.24/29.33 % (1662795)Termination reason: Instruction limit % 206.24/29.33 % (1662795)Termination phase: Saturation % 206.24/29.33 % (1662795)Time elapsed: 0.358 s % 206.24/29.33 % (1662795)Peak memory usage: 15 MB % 206.24/29.33 % (1662795)Instructions burned: 318 (million) % 206.24/29.33 % (1662799)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=409605651:i=1428:nm=2:rtra=on_2789 on theBenchmark for (2789ds/1428Mi) % 285.97/40.52 % (1662799)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 285.97/40.52 % (1662799)Terminated due to inappropriate strategy. % 285.97/40.52 % (1662799)------------------------------ % 285.97/40.52 % (1662799)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 285.97/40.52 % (1662799)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 285.97/40.52 % (1662799)CaDiCaL version: 2.1.3 % 285.97/40.52 % (1662799)Termination reason: Inappropriate % 285.97/40.52 % (1662799)Time elapsed: 0.002 s % 285.97/40.52 % (1662799)Peak memory usage: 10 MB % 285.97/40.52 % (1662799)Instructions burned: 1 (million) % 285.97/40.52 % (1662799)------------------------------ % 285.97/40.52 % (1662799)------------------------------ % 285.97/40.52 % (1662801)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=1652288142:i=262:bd=preordered:rtra=on:fsd=on_2789 on theBenchmark for (2789ds/262Mi) % 285.97/40.52 % (1662801)Instruction limit reached! % 285.97/40.52 % (1662801)------------------------------ % 285.97/40.52 % (1662801)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 285.97/40.52 % (1662801)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 285.97/40.52 % (1662801)CaDiCaL version: 2.1.3 % 285.97/40.52 % (1662801)Termination reason: Instruction limit % 285.97/40.52 % (1662801)Termination phase: Saturation % 285.97/40.52 % (1662801)Time elapsed: 0.276 s % 285.97/40.52 % (1662801)Peak memory usage: 14 MB % 285.97/40.52 % (1662801)Instructions burned: 262 (million) % 285.97/40.52 % (1662803)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=708425811:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2786 on theBenchmark for (2786ds/1368Mi) % 285.97/40.52 % (1662803)Instruction limit reached! % 285.97/40.52 % (1662803)------------------------------ % 285.97/40.52 % (1662803)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 285.97/40.52 % (1662803)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 285.97/40.52 % (1662803)CaDiCaL version: 2.1.3 % 285.97/40.52 % (1662803)Termination reason: Instruction limit % 285.97/40.52 % (1662803)Termination phase: Saturation % 285.97/40.52 % (1662803)Time elapsed: 1.309 s % 285.97/40.52 % (1662803)Peak memory usage: 23 MB % 285.97/40.52 % (1662803)Instructions burned: 1368 (million) % 285.97/40.52 % (1662805)ott-21_1_sil=16000:si=on:fs=off:random_seed=3366643615:i=360:av=off:fsr=off:rtra=on_2772 on theBenchmark for (2772ds/360Mi) % 285.97/40.52 % (1662805)Instruction limit reached! % 285.97/40.52 % (1662805)------------------------------ % 285.97/40.52 % (1662805)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 285.97/40.52 % (1662805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 285.97/40.52 % (1662805)CaDiCaL version: 2.1.3 % 285.97/40.52 % (1662805)Termination reason: Instruction limit % 285.97/40.52 % (1662805)Termination phase: Saturation % 285.97/40.52 % (1662805)Time elapsed: 0.291 s % 285.97/40.52 % (1662805)Peak memory usage: 13 MB % 285.97/40.52 % (1662805)Instructions burned: 360 (million) % 285.97/40.52 % (1662807)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=4046809835:i=954:bd=all:rtra=on_2769 on theBenchmark for (2769ds/954Mi) % 285.97/40.52 % (1662807)Instruction limit reached! % 285.97/40.52 % (1662807)------------------------------ % 285.97/40.52 % (1662807)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 285.97/40.52 % (1662807)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 285.97/40.52 % (1662807)CaDiCaL version: 2.1.3 % 285.97/40.52 % (1662807)Termination reason: Instruction limit % 285.97/40.52 % (1662807)Termination phase: Saturation % 285.97/40.52 % (1662807)Time elapsed: 0.925 s % 285.97/40.52 % (1662807)Peak memory usage: 16 MB % 285.97/40.52 % (1662807)Instructions burned: 954 (million) % 285.97/40.52 % (1662811)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=956253058:fmbsr=1.3:i=1730:ins=25:rtra=on_2760 on theBenchmark for (2760ds/1730Mi) % 285.97/40.52 % (1662811)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 285.97/40.52 % (1662811)Terminated due to inappropriate strategy. % 285.97/40.52 % (1662811)------------------------------ % 285.97/40.52 % (1662811)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 285.97/40.52 % (1662811)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 285.97/40.52 % (1662811)CaDiCaL version: 2.1.3 % 285.97/40.52 % (1662811)Termination reason: Inappropriate % 285.97/40.52 % (1662811)Time elapsed: 0.001 s % 300.48/42.63 % (1662811)Peak memory usage: 10 MB % 300.48/42.63 % (1662811)Instructions burned: 1 (million) % 300.48/42.63 % (1662811)------------------------------ % 300.48/42.63 % (1662811)------------------------------ % 300.48/42.63 % (1662813)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=104221229:i=2358:rtra=on_2760 on theBenchmark for (2760ds/2358Mi) % 300.48/42.63 % (1662813)Instruction limit reached! % 300.48/42.63 % (1662813)------------------------------ % 300.48/42.63 % (1662813)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.48/42.63 % (1662813)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.48/42.63 % (1662813)CaDiCaL version: 2.1.3 % 300.48/42.63 % (1662813)Termination reason: Instruction limit % 300.48/42.63 % (1662813)Termination phase: Saturation % 300.48/42.63 % (1662813)Time elapsed: 1.862 s % 300.48/42.63 % (1662813)Peak memory usage: 17 MB % 300.48/42.63 % (1662813)Instructions burned: 2358 (million) % 300.48/42.63 % (1662815)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=2576472315:i=1778:ins=1:rtra=on_2741 on theBenchmark for (2741ds/1778Mi) % 300.48/42.63 % (1662815)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.48/42.63 % (1662815)Terminated due to inappropriate strategy. % 300.48/42.63 % (1662815)------------------------------ % 300.48/42.63 % (1662815)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.48/42.63 % (1662815)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.48/42.63 % (1662815)CaDiCaL version: 2.1.3 % 300.48/42.63 % (1662815)Termination reason: Inappropriate % 300.48/42.63 % (1662815)Time elapsed: 0.001 s % 300.48/42.63 % (1662815)Peak memory usage: 10 MB % 300.48/42.63 % (1662815)Instructions burned: 1 (million) % 300.48/42.63 % (1662815)------------------------------ % 300.48/42.63 % (1662815)------------------------------ % 300.48/42.63 % (1662817)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=2737939028:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2740 on theBenchmark for (2740ds/1384Mi) % 300.48/42.63 % (1662817)Instruction limit reached! % 300.48/42.63 % (1662817)------------------------------ % 300.48/42.63 % (1662817)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.48/42.63 % (1662817)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.48/42.63 % (1662817)CaDiCaL version: 2.1.3 % 300.48/42.63 % (1662817)Termination reason: Instruction limit % 300.48/42.63 % (1662817)Termination phase: Saturation % 300.48/42.63 % (1662817)Time elapsed: 1.444 s % 300.48/42.63 % (1662817)Peak memory usage: 29 MB % 300.48/42.63 % (1662817)Instructions burned: 1385 (million) % 300.48/42.63 % (1662819)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=3846837029:i=1758:kws=inv_precedence:fsr=off:rtra=on_2726 on theBenchmark for (2726ds/1758Mi) % 300.48/42.63 % (1662819)Instruction limit reached! % 300.48/42.63 % (1662819)------------------------------ % 300.48/42.63 % (1662819)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.48/42.63 % (1662819)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.48/42.63 % (1662819)CaDiCaL version: 2.1.3 % 300.48/42.63 % (1662819)Termination reason: Instruction limit % 300.48/42.63 % (1662819)Termination phase: Saturation % 300.48/42.63 % (1662819)Time elapsed: 1.597 s % 300.48/42.63 % (1662819)Peak memory usage: 26 MB % 300.48/42.63 % (1662819)Instructions burned: 1758 (million) % 300.48/42.63 % (1662827)fmb+10_1_sil=64000:si=on:random_seed=1915152926:i=44122:nm=2:rtra=on:gsp=on_2709 on theBenchmark for (2709ds/44122Mi) % 300.48/42.63 % (1662827)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.48/42.63 % (1662827)Terminated due to inappropriate strategy. % 300.48/42.63 % (1662827)------------------------------ % 300.48/42.63 % (1662827)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.48/42.63 % (1662827)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.48/42.63 % (1662827)CaDiCaL version: 2.1.3 % 300.48/42.63 % (1662827)Termination reason: Inappropriate % 300.48/42.63 % (1662827)Time elapsed: 0.002 s % 300.48/42.63 % (1662827)Peak memory usage: 10 MB % 300.48/42.63 % (1662827)Instructions burned: 1 (million) % 300.48/42.63 % (1662827)------------------------------ % 300.48/42.63 % (1662827)------------------------------ % 300.48/42.63 % (1662829)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=4248826297:i=19030:nm=5:rtra=on_2709 on theBenchmark for (2709ds/19030Mi) % 300.48/42.63 % (1662829)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.48/42.63 % (1662829)Terminated due to inappropriate strategy. % 300.48/42.63 % (1662829)------------------------------ % 300.48/42.63 % (1662829)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.48/42.63 % (1662829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.48/42.63 % (1662829)CaDiCaL version: 2.1.3 % 300.48/42.63 % (1662829)Termination reason: Inappropriate % 300.48/42.63 % (1662829)Time elapsed: 0.001 s % 300.48/42.63 % (1662829)Peak memory usage: 10 MB % 300.48/42.63 % (1662829)Instructions burned: 1 (million) % 300.48/42.63 % (1662829)------------------------------ % 300.48/42.63 % (1662829)------------------------------ % 300.48/42.63 % (1662831)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=4133461902:fmbsr=1.7:i=1840:rtra=on_2709 on theBenchmark for (2709ds/1840Mi) % 300.48/42.63 % (1662831)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.48/42.63 % (1662831)Terminated due to inappropriate strategy. % 300.48/42.63 % (1662831)------------------------------ % 300.48/42.63 % (1662831)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.48/42.63 % (1662831)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.48/42.63 % (1662831)CaDiCaL version: 2.1.3 % 300.48/42.63 % (1662831)Termination reason: Inappropriate % 300.48/42.63 % (1662831)Time elapsed: 0.001 s % 300.48/42.63 % (1662831)Peak memory usage: 10 MB % 300.48/42.63 % (1662831)Instructions burned: 1 (million) % 300.48/42.63 % (1662831)------------------------------ % 300.48/42.63 % (1662831)------------------------------ % 300.48/42.63 % (1662833)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=2901987225:i=10262:rtra=on_2708 on theBenchmark for (2708ds/10262Mi) % 300.48/42.63 % (1662833)Instruction limit reached! % 300.48/42.63 % (1662833)------------------------------ % 300.48/42.63 % (1662833)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.48/42.63 % (1662833)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.48/42.63 % (1662833)CaDiCaL version: 2.1.3 % 300.48/42.63 % (1662833)Termination reason: Instruction limit % 300.48/42.63 % (1662833)Termination phase: Saturation % 300.48/42.63 % (1662833)Time elapsed: 10.032 s % 300.48/42.63 % (1662833)Peak memory usage: 68 MB % 300.48/42.63 % (1662833)Instructions burned: 10263 (million) % 300.48/42.63 % (1662838)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1622466878:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2608 on theBenchmark for (2608ds/2944Mi) % 300.48/42.63 % (1662757)Instruction limit reached! % 300.48/42.63 % (1662757)------------------------------ % 300.48/42.63 % (1662757)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.48/42.63 % (1662757)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.48/42.63 % (1662757)CaDiCaL version: 2.1.3 % 300.48/42.63 % (1662757)Termination reason: Instruction limit % 300.48/42.63 % (1662757)Termination phase: Saturation % 300.48/42.63 % (1662757)Time elapsed: 21.727 s % 300.48/42.63 % (1662757)Peak memory usage: 27 MB % 300.48/42.63 % (1662757)Instructions burned: 28120 (million) % 300.48/42.63 % (1662842)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=3181703377:i=12648:rtra=on_2597 on theBenchmark for (2597ds/12648Mi) % 300.48/42.63 % (1662842)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.48/42.63 % (1662842)Terminated due to inappropriate strategy. % 300.48/42.63 % (1662842)------------------------------ % 300.48/42.63 % (1662842)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.48/42.63 % (1662842)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.48/42.63 % (1662842)CaDiCaL version: 2.1.3 % 300.48/42.63 % (1662842)Termination reason: Inappropriate % 300.48/42.63 % (1662842)Time elapsed: 0.002 s % 300.48/42.63 % (1662842)Peak memory usage: 10 MB % 300.48/42.63 % (1662842)Instructions burned: 1 (million) % 300.48/42.63 % (1662842)------------------------------ % 300.48/42.63 % (1662842)------------------------------ % 300.48/42.63 % (1662844)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=4083993777:fmbsr=2.30978:i=4348:rtra=on_2597 on theBenchmark for (2597ds/4348Mi) % 300.48/42.63 % (1662844)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.48/42.63 % (1662844)Terminated due to inappropriate strategy. % 300.48/42.63 % (1662844)------------------------------ % 300.48/42.63 % (1662844)Vers % 300.48/42.63 Terminated % 300.48/42.63 % Vampire exiting % 300.48/42.63 Terminated %------------------------------------------------------------------------------