%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW830_1 : TPTP v9.3.1. Released v7.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n001.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:45:02 PM UTC 2026 % Result : Timeout 300.09s 42.53s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWW830_1 : TPTP v9.3.1. Released v7.0.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.08/0.17 % Computer : n001.cluster.edu % 0.08/0.17 % Model : x86_64 x86_64 % 0.08/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.17 % Memory : 8046.5625MB % 0.08/0.17 % OS : Linux 6.8.0-71-generic % 0.08/0.17 % CPULimit : 300 % 0.08/0.17 % WCLimit : 300 % 0.08/0.17 % DateTime : Mon Sep 28 14:36:49 UTC 2026 % 0.08/0.17 % CPUTime : % 0.08/0.17 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.08/0.21 Running first-order model finding % 0.08/0.21 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 % 2.93/0.69 % (393365)Will run a generic schedule for satisfiability detection. % 2.93/0.69 % (393375)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3721221207:i=131_2999 on theBenchmark for (2999ds/131Mi) % 2.93/0.69 % (393371)% WARNING: option uhcvi not known. % 2.93/0.69 % (393370)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2513311249_2999 on theBenchmark for (2999ds/0Mi) % 2.93/0.69 % (393371)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1804269389:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 2.93/0.69 % (393372)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1271077515:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 2.93/0.69 % (393373)dis+10_1_sil=32000:sp=arity:random_seed=523371149:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 2.93/0.69 % (393374)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2976591486:i=116_2999 on theBenchmark for (2999ds/116Mi) % 2.93/0.69 % (393376)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2683032967:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 2.93/0.69 % (393370)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 2.93/0.69 % (393370)Terminated due to inappropriate strategy. % 2.93/0.69 % (393370)------------------------------ % 2.93/0.69 % (393370)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.93/0.69 % (393370)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.93/0.69 % (393370)CaDiCaL version: 2.1.3 % 2.93/0.69 % (393370)Termination reason: Inappropriate % 2.93/0.69 % (393370)Time elapsed: 0.027 s % 2.93/0.69 % (393370)Peak memory usage: 12 MB % 2.93/0.69 % (393370)Instructions burned: 61 (million) % 2.93/0.69 % (393370)------------------------------ % 2.93/0.69 % (393370)------------------------------ % 2.93/0.69 % (393375)Instruction limit reached! % 2.93/0.69 % (393375)------------------------------ % 2.93/0.69 % (393375)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.93/0.69 % (393375)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.93/0.69 % (393375)CaDiCaL version: 2.1.3 % 2.93/0.69 % (393375)Termination reason: Instruction limit % 2.93/0.69 % (393375)Termination phase: Saturation % 2.93/0.69 % (393375)Time elapsed: 0.039 s % 2.93/0.69 % (393375)Peak memory usage: 14 MB % 2.93/0.69 % (393375)Instructions burned: 134 (million) % 2.93/0.69 % (393390)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2261050282:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 2.93/0.69 % (393388)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2577162288:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 2.93/0.69 % (393373)Instruction limit reached! % 2.93/0.69 % (393373)------------------------------ % 2.93/0.69 % (393373)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.93/0.69 % (393373)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.93/0.69 % (393373)CaDiCaL version: 2.1.3 % 2.93/0.69 % (393373)Termination reason: Instruction limit % 2.93/0.69 % (393373)Termination phase: Saturation % 2.93/0.69 % (393373)Time elapsed: 0.054 s % 2.93/0.69 % (393373)Peak memory usage: 13 MB % 2.93/0.69 % (393373)Instructions burned: 105 (million) % 2.93/0.69 % (393374)Instruction limit reached! % 2.93/0.69 % (393374)------------------------------ % 2.93/0.69 % (393374)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.93/0.69 % (393374)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.93/0.69 % (393374)CaDiCaL version: 2.1.3 % 2.93/0.69 % (393374)Termination reason: Instruction limit % 2.93/0.69 % (393374)Termination phase: Saturation % 2.93/0.69 % (393374)Time elapsed: 0.061 s % 2.93/0.69 % (393374)Peak memory usage: 13 MB % 2.93/0.69 % (393374)Instructions burned: 116 (million) % 2.93/0.69 % (393395)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=1910542398:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 2.93/0.69 % (393388)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 2.93/0.69 % (393388)Terminated due to inappropriate strategy. % 2.93/0.69 % (393388)------------------------------ % 2.93/0.69 % (393388)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.93/0.69 % (393388)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.80/1.27 % (393388)CaDiCaL version: 2.1.3 % 6.80/1.27 % (393388)Termination reason: Inappropriate % 6.80/1.27 % (393388)Time elapsed: 0.027 s % 6.80/1.27 % (393388)Peak memory usage: 11 MB % 6.80/1.27 % (393388)Instructions burned: 61 (million) % 6.80/1.27 % (393388)------------------------------ % 6.80/1.27 % (393388)------------------------------ % 6.80/1.27 % (393397)ott-21_1_sil=16000:fs=off:random_seed=3182797738:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 6.80/1.27 % (393390)Instruction limit reached! % 6.80/1.27 % (393390)------------------------------ % 6.80/1.27 % (393390)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.80/1.27 % (393390)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.80/1.27 % (393390)CaDiCaL version: 2.1.3 % 6.80/1.27 % (393390)Termination reason: Instruction limit % 6.80/1.27 % (393390)Termination phase: Saturation % 6.80/1.27 % (393390)Time elapsed: 0.040 s % 6.80/1.27 % (393390)Peak memory usage: 14 MB % 6.80/1.27 % (393390)Instructions burned: 139 (million) % 6.80/1.27 % (393376)Instruction limit reached! % 6.80/1.27 % (393376)------------------------------ % 6.80/1.27 % (393376)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.80/1.27 % (393376)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.80/1.27 % (393376)CaDiCaL version: 2.1.3 % 6.80/1.27 % (393376)Termination reason: Instruction limit % 6.80/1.27 % (393376)Termination phase: Saturation % 6.80/1.27 % (393376)Time elapsed: 0.087 s % 6.80/1.27 % (393376)Peak memory usage: 14 MB % 6.80/1.27 % (393376)Instructions burned: 159 (million) % 6.80/1.27 % (393411)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3789576112:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 6.80/1.27 % (393407)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=374839394:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 6.80/1.27 % (393411)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 6.80/1.27 % (393411)Terminated due to inappropriate strategy. % 6.80/1.27 % (393411)------------------------------ % 6.80/1.27 % (393411)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.80/1.27 % (393411)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.80/1.27 % (393411)CaDiCaL version: 2.1.3 % 6.80/1.27 % (393411)Termination reason: Inappropriate % 6.80/1.27 % (393411)Time elapsed: 0.014 s % 6.80/1.27 % (393411)Peak memory usage: 11 MB % 6.80/1.27 % (393411)Instructions burned: 60 (million) % 6.80/1.27 % (393411)------------------------------ % 6.80/1.27 % (393411)------------------------------ % 6.80/1.27 % (393417)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3505869065:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 6.80/1.27 % (393432)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=31781729:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 6.80/1.27 % (393432)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 6.80/1.27 % (393432)Terminated due to inappropriate strategy. % 6.80/1.27 % (393432)------------------------------ % 6.80/1.27 % (393432)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.80/1.27 % (393432)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.80/1.27 % (393432)CaDiCaL version: 2.1.3 % 6.80/1.27 % (393432)Termination reason: Inappropriate % 6.80/1.27 % (393432)Time elapsed: 0.014 s % 6.80/1.27 % (393432)Peak memory usage: 11 MB % 6.80/1.27 % (393432)Instructions burned: 61 (million) % 6.80/1.27 % (393432)------------------------------ % 6.80/1.27 % (393432)------------------------------ % 6.80/1.27 % (393443)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=33514657: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) % 6.80/1.27 % (393397)Instruction limit reached! % 6.80/1.27 % (393397)------------------------------ % 6.80/1.27 % (393397)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.80/1.27 % (393397)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.80/1.27 % (393397)CaDiCaL version: 2.1.3 % 6.80/1.27 % (393397)Termination reason: Instruction limit % 6.80/1.27 % (393397)Termination phase: Saturation % 6.80/1.27 % (393397)Time elapsed: 0.084 s % 6.80/1.27 % (393397)Peak memory usage: 14 MB % 6.80/1.27 % (393397)Instructions burned: 182 (million) % 21.13/3.29 % (393449)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1573115951:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 21.13/3.29 % (393443)Instruction limit reached! % 21.13/3.29 % (393443)------------------------------ % 21.13/3.29 % (393443)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.13/3.29 % (393443)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.13/3.29 % (393443)CaDiCaL version: 2.1.3 % 21.13/3.29 % (393443)Termination reason: Instruction limit % 21.13/3.29 % (393443)Termination phase: Saturation % 21.13/3.29 % (393443)Time elapsed: 0.221 s % 21.13/3.29 % (393443)Peak memory usage: 20 MB % 21.13/3.29 % (393443)Instructions burned: 695 (million) % 21.13/3.29 % (393451)fmb+10_1_sil=64000:random_seed=2558582089:i=22061:nm=2:gsp=on_2995 on theBenchmark for (2995ds/22061Mi) % 21.13/3.29 % (393407)Instruction limit reached! % 21.13/3.29 % (393407)------------------------------ % 21.13/3.29 % (393407)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.13/3.29 % (393407)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.13/3.29 % (393407)CaDiCaL version: 2.1.3 % 21.13/3.29 % (393407)Termination reason: Instruction limit % 21.13/3.29 % (393407)Termination phase: Saturation % 21.13/3.29 % (393407)Time elapsed: 0.290 s % 21.13/3.29 % (393407)Peak memory usage: 16 MB % 21.13/3.29 % (393407)Instructions burned: 477 (million) % 21.13/3.29 % (393451)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 21.13/3.29 % (393451)Terminated due to inappropriate strategy. % 21.13/3.29 % (393451)------------------------------ % 21.13/3.29 % (393451)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.13/3.29 % (393451)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.13/3.29 % (393451)CaDiCaL version: 2.1.3 % 21.13/3.29 % (393451)Termination reason: Inappropriate % 21.13/3.29 % (393451)Time elapsed: 0.015 s % 21.13/3.29 % (393451)Peak memory usage: 11 MB % 21.13/3.29 % (393451)Instructions burned: 61 (million) % 21.13/3.29 % (393451)------------------------------ % 21.13/3.29 % (393451)------------------------------ % 21.13/3.29 % (393454)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=4242122306:fmbsr=1.7:i=920_2995 on theBenchmark for (2995ds/920Mi) % 21.13/3.29 % (393453)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2199622923:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi) % 21.13/3.29 % (393454)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 21.13/3.29 % (393454)Terminated due to inappropriate strategy. % 21.13/3.29 % (393454)------------------------------ % 21.13/3.29 % (393454)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.13/3.29 % (393454)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.13/3.29 % (393454)CaDiCaL version: 2.1.3 % 21.13/3.29 % (393454)Termination reason: Inappropriate % 21.13/3.29 % (393454)Time elapsed: 0.014 s % 21.13/3.29 % (393454)Peak memory usage: 11 MB % 21.13/3.29 % (393454)Instructions burned: 61 (million) % 21.13/3.29 % (393454)------------------------------ % 21.13/3.29 % (393454)------------------------------ % 21.13/3.29 % (393395)Instruction limit reached! % 21.13/3.29 % (393395)------------------------------ % 21.13/3.29 % (393395)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.13/3.29 % (393395)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.13/3.29 % (393395)CaDiCaL version: 2.1.3 % 21.13/3.29 % (393395)Termination reason: Instruction limit % 21.13/3.29 % (393395)Termination phase: Saturation % 21.13/3.29 % (393395)Time elapsed: 0.355 s % 21.13/3.29 % (393395)Peak memory usage: 17 MB % 21.13/3.29 % (393395)Instructions burned: 685 (million) % 21.13/3.29 % (393457)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=111412883:i=5131_2995 on theBenchmark for (2995ds/5131Mi) % 21.13/3.29 % (393453)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 21.13/3.29 % (393453)Terminated due to inappropriate strategy. % 21.13/3.29 % (393453)------------------------------ % 21.13/3.29 % (393453)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.13/3.29 % (393453)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.13/3.29 % (393453)CaDiCaL version: 2.1.3 % 21.13/3.29 % (393453)Termination reason: Inappropriate % 21.13/3.29 % (393453)Time elapsed: 0.027 s % 21.13/3.29 % (393453)Peak memory usage: 11 MB % 21.13/3.29 % (393453)Instructions burned: 61 (million) % 24.90/3.84 % (393453)------------------------------ % 24.90/3.84 % (393453)------------------------------ % 24.90/3.84 % (393459)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3259339291:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi) % 24.90/3.84 % (393460)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=4251043585:i=6324_2995 on theBenchmark for (2995ds/6324Mi) % 24.90/3.84 % (393460)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 24.90/3.84 % (393460)Terminated due to inappropriate strategy. % 24.90/3.84 % (393460)------------------------------ % 24.90/3.84 % (393460)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 24.90/3.84 % (393460)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.90/3.84 % (393460)CaDiCaL version: 2.1.3 % 24.90/3.84 % (393460)Termination reason: Inappropriate % 24.90/3.84 % (393460)Time elapsed: 0.027 s % 24.90/3.84 % (393460)Peak memory usage: 12 MB % 24.90/3.84 % (393460)Instructions burned: 61 (million) % 24.90/3.84 % (393460)------------------------------ % 24.90/3.84 % (393460)------------------------------ % 24.90/3.84 % (393463)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2653353392:fmbsr=2.30978:i=2174_2994 on theBenchmark for (2994ds/2174Mi) % 24.90/3.84 % (393463)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 24.90/3.84 % (393463)Terminated due to inappropriate strategy. % 24.90/3.84 % (393463)------------------------------ % 24.90/3.84 % (393463)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 24.90/3.84 % (393463)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.90/3.84 % (393463)CaDiCaL version: 2.1.3 % 24.90/3.84 % (393463)Termination reason: Inappropriate % 24.90/3.84 % (393463)Time elapsed: 0.027 s % 24.90/3.84 % (393463)Peak memory usage: 11 MB % 24.90/3.84 % (393463)Instructions burned: 61 (million) % 24.90/3.84 % (393463)------------------------------ % 24.90/3.84 % (393463)------------------------------ % 24.90/3.84 % (393465)ott-2_1_sil=16000:newcnf=on:random_seed=1227154333:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2994 on theBenchmark for (2994ds/869Mi) % 24.90/3.84 % (393449)Instruction limit reached! % 24.90/3.84 % (393449)------------------------------ % 24.90/3.84 % (393449)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 24.90/3.84 % (393449)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.90/3.84 % (393449)CaDiCaL version: 2.1.3 % 24.90/3.84 % (393449)Termination reason: Instruction limit % 24.90/3.84 % (393449)Termination phase: Saturation % 24.90/3.84 % (393449)Time elapsed: 0.492 s % 24.90/3.84 % (393449)Peak memory usage: 19 MB % 24.90/3.84 % (393449)Instructions burned: 880 (million) % 24.90/3.84 % (393467)ott+10_1_sil=32000:tgt=ground:random_seed=807118366:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi) % 24.90/3.84 % (393417)Instruction limit reached! % 24.90/3.84 % (393417)------------------------------ % 24.90/3.84 % (393417)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 24.90/3.84 % (393417)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.90/3.84 % (393417)CaDiCaL version: 2.1.3 % 24.90/3.84 % (393417)Termination reason: Instruction limit % 24.90/3.84 % (393417)Termination phase: Saturation % 24.90/3.84 % (393417)Time elapsed: 0.648 s % 24.90/3.84 % (393417)Peak memory usage: 23 MB % 24.90/3.84 % (393417)Instructions burned: 1180 (million) % 24.90/3.84 % (393469)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2589212586:i=54282_2991 on theBenchmark for (2991ds/54282Mi) % 24.90/3.84 % (393469)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 24.90/3.84 % (393469)Terminated due to inappropriate strategy. % 24.90/3.84 % (393469)------------------------------ % 24.90/3.84 % (393469)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 24.90/3.84 % (393469)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.90/3.84 % (393469)CaDiCaL version: 2.1.3 % 24.90/3.84 % (393469)Termination reason: Inappropriate % 24.90/3.84 % (393469)Time elapsed: 0.028 s % 24.90/3.84 % (393469)Peak memory usage: 12 MB % 24.90/3.84 % (393469)Instructions burned: 61 (million) % 24.90/3.84 % (393469)------------------------------ % 24.90/3.84 % (393469)------------------------------ % 24.90/3.84 % (393471)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1112529716:i=3512:aac=none_2991 on theBenchmark for (2991ds/3512Mi) % 24.90/3.84 % (393465)Instruction limit reached! % 89.97/13.02 % (393465)------------------------------ % 89.97/13.02 % (393465)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 89.97/13.02 % (393465)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 89.97/13.02 % (393465)CaDiCaL version: 2.1.3 % 89.97/13.02 % (393465)Termination reason: Instruction limit % 89.97/13.02 % (393465)Termination phase: Saturation % 89.97/13.02 % (393465)Time elapsed: 0.465 s % 89.97/13.02 % (393465)Peak memory usage: 19 MB % 89.97/13.02 % (393465)Instructions burned: 871 (million) % 89.97/13.02 % (393473)dis+21_1_sil=32000:sas=cadical:random_seed=401306629:i=3773:amm=off_2989 on theBenchmark for (2989ds/3773Mi) % 89.97/13.02 % (393459)Instruction limit reached! % 89.97/13.02 % (393459)------------------------------ % 89.97/13.02 % (393459)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 89.97/13.02 % (393459)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 89.97/13.02 % (393459)CaDiCaL version: 2.1.3 % 89.97/13.02 % (393459)Termination reason: Instruction limit % 89.97/13.02 % (393459)Termination phase: Saturation % 89.97/13.02 % (393459)Time elapsed: 0.723 s % 89.97/13.02 % (393459)Peak memory usage: 29 MB % 89.97/13.02 % (393459)Instructions burned: 1473 (million) % 89.97/13.02 % (393475)ott+11_1_sil=16000:gs=on:random_seed=1900754668:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2987 on theBenchmark for (2987ds/2251Mi) % 89.97/13.02 % (393457)Instruction limit reached! % 89.97/13.02 % (393457)------------------------------ % 89.97/13.02 % (393457)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 89.97/13.02 % (393457)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 89.97/13.02 % (393457)CaDiCaL version: 2.1.3 % 89.97/13.02 % (393457)Termination reason: Instruction limit % 89.97/13.02 % (393457)Termination phase: Saturation % 89.97/13.02 % (393457)Time elapsed: 1.457 s % 89.97/13.02 % (393457)Peak memory usage: 48 MB % 89.97/13.02 % (393457)Instructions burned: 5133 (million) % 89.97/13.02 % (393477)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1632790207:fmbsr=1.6:i=67534_2980 on theBenchmark for (2980ds/67534Mi) % 89.97/13.02 % (393477)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 89.97/13.02 % (393477)Terminated due to inappropriate strategy. % 89.97/13.02 % (393477)------------------------------ % 89.97/13.02 % (393477)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 89.97/13.02 % (393477)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 89.97/13.02 % (393477)CaDiCaL version: 2.1.3 % 89.97/13.02 % (393477)Termination reason: Inappropriate % 89.97/13.02 % (393477)Time elapsed: 0.015 s % 89.97/13.02 % (393477)Peak memory usage: 11 MB % 89.97/13.02 % (393477)Instructions burned: 61 (million) % 89.97/13.02 % (393477)------------------------------ % 89.97/13.02 % (393477)------------------------------ % 89.97/13.02 % (393479)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2953764361:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2980 on theBenchmark for (2980ds/4591Mi) % 89.97/13.02 % (393475)Instruction limit reached! % 89.97/13.02 % (393475)------------------------------ % 89.97/13.02 % (393475)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 89.97/13.02 % (393475)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 89.97/13.02 % (393475)CaDiCaL version: 2.1.3 % 89.97/13.02 % (393475)Termination reason: Instruction limit % 89.97/13.02 % (393475)Termination phase: Saturation % 89.97/13.02 % (393475)Time elapsed: 1.263 s % 89.97/13.02 % (393475)Peak memory usage: 42 MB % 89.97/13.02 % (393475)Instructions burned: 2251 (million) % 89.97/13.02 % (393481)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3860257455:i=29340_2974 on theBenchmark for (2974ds/29340Mi) % 89.97/13.02 % (393471)Instruction limit reached! % 89.97/13.02 % (393471)------------------------------ % 89.97/13.02 % (393471)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 89.97/13.02 % (393471)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 89.97/13.02 % (393471)CaDiCaL version: 2.1.3 % 89.97/13.02 % (393471)Termination reason: Instruction limit % 89.97/13.02 % (393471)Termination phase: Saturation % 89.97/13.02 % (393471)Time elapsed: 1.857 s % 89.97/13.02 % (393471)Peak memory usage: 34 MB % 89.97/13.02 % (393471)Instructions burned: 3514 (million) % 89.97/13.02 % (393483)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2322836441:i=5211_2972 on theBenchmark for (2972ds/5211Mi) % 89.97/13.02 % (393473)Instruction limit reached! % 110.52/15.85 % (393473)------------------------------ % 110.52/15.85 % (393473)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 110.52/15.85 % (393473)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 110.52/15.85 % (393473)CaDiCaL version: 2.1.3 % 110.52/15.85 % (393473)Termination reason: Instruction limit % 110.52/15.85 % (393473)Termination phase: Saturation % 110.52/15.85 % (393473)Time elapsed: 1.997 s % 110.52/15.85 % (393473)Peak memory usage: 36 MB % 110.52/15.85 % (393473)Instructions burned: 3774 (million) % 110.52/15.85 % (393485)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=696729347:i=5497:nm=2_2969 on theBenchmark for (2969ds/5497Mi) % 110.52/15.85 % (393485)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 110.52/15.85 % (393485)Terminated due to inappropriate strategy. % 110.52/15.85 % (393485)------------------------------ % 110.52/15.85 % (393485)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 110.52/15.85 % (393485)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 110.52/15.85 % (393485)CaDiCaL version: 2.1.3 % 110.52/15.85 % (393485)Termination reason: Inappropriate % 110.52/15.85 % (393485)Time elapsed: 0.027 s % 110.52/15.85 % (393485)Peak memory usage: 12 MB % 110.52/15.85 % (393485)Instructions burned: 61 (million) % 110.52/15.85 % (393485)------------------------------ % 110.52/15.85 % (393485)------------------------------ % 110.52/15.85 % (393487)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=325009423:fmbsr=2:i=46332_2968 on theBenchmark for (2968ds/46332Mi) % 110.52/15.85 % (393487)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 110.52/15.85 % (393487)Terminated due to inappropriate strategy. % 110.52/15.85 % (393487)------------------------------ % 110.52/15.85 % (393487)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 110.52/15.85 % (393487)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 110.52/15.85 % (393487)CaDiCaL version: 2.1.3 % 110.52/15.85 % (393487)Termination reason: Inappropriate % 110.52/15.85 % (393487)Time elapsed: 0.027 s % 110.52/15.85 % (393487)Peak memory usage: 11 MB % 110.52/15.85 % (393487)Instructions burned: 61 (million) % 110.52/15.85 % (393487)------------------------------ % 110.52/15.85 % (393487)------------------------------ % 110.52/15.85 % (393489)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=399833628:i=14071_2968 on theBenchmark for (2968ds/14071Mi) % 110.52/15.85 % (393489)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 110.52/15.85 % (393489)Terminated due to inappropriate strategy. % 110.52/15.85 % (393489)------------------------------ % 110.52/15.85 % (393489)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 110.52/15.85 % (393489)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 110.52/15.85 % (393489)CaDiCaL version: 2.1.3 % 110.52/15.85 % (393489)Termination reason: Inappropriate % 110.52/15.85 % (393489)Time elapsed: 0.027 s % 110.52/15.85 % (393489)Peak memory usage: 11 MB % 110.52/15.85 % (393489)Instructions burned: 61 (million) % 110.52/15.85 % (393489)------------------------------ % 110.52/15.85 % (393489)------------------------------ % 110.52/15.85 % (393491)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2263898594:i=22565:add=on:rawr=on_2967 on theBenchmark for (2967ds/22565Mi) % 110.52/15.85 % (393479)Instruction limit reached! % 110.52/15.85 % (393479)------------------------------ % 110.52/15.85 % (393479)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 110.52/15.85 % (393479)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 110.52/15.85 % (393479)CaDiCaL version: 2.1.3 % 110.52/15.85 % (393479)Termination reason: Instruction limit % 110.52/15.85 % (393479)Termination phase: Saturation % 110.52/15.85 % (393479)Time elapsed: 1.471 s % 110.52/15.85 % (393479)Peak memory usage: 49 MB % 110.52/15.85 % (393479)Instructions burned: 4594 (million) % 110.52/15.85 % (393493)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=1486734874:i=8173:av=off_2965 on theBenchmark for (2965ds/8173Mi) % 110.52/15.85 % (393467)Instruction limit reached! % 110.52/15.85 % (393467)------------------------------ % 110.52/15.85 % (393467)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 110.52/15.85 % (393467)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 110.52/15.85 % (393467)CaDiCaL version: 2.1.3 % 110.52/15.85 % (393467)Termination reason: Instruction limit % 110.52/15.85 % (393467)Termination phase: Saturation % 115.09/16.54 % (393467)Time elapsed: 2.881 s % 115.09/16.54 % (393467)Peak memory usage: 48 MB % 115.09/16.54 % (393467)Instructions burned: 5114 (million) % 115.09/16.54 % (393495)dis+10_16:1_sil=16000:random_seed=2611571127:i=9155:fsr=off_2963 on theBenchmark for (2963ds/9155Mi) % 115.09/16.54 % (393483)Instruction limit reached! % 115.09/16.54 % (393483)------------------------------ % 115.09/16.54 % (393483)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 115.09/16.54 % (393483)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 115.09/16.54 % (393483)CaDiCaL version: 2.1.3 % 115.09/16.54 % (393483)Termination reason: Instruction limit % 115.09/16.54 % (393483)Termination phase: Saturation % 115.09/16.54 % (393483)Time elapsed: 2.815 s % 115.09/16.54 % (393483)Peak memory usage: 47 MB % 115.09/16.54 % (393483)Instructions burned: 5213 (million) % 115.09/16.54 % (393497)ott-3_8_sil=64000:random_seed=2026059046:i=20139:bs=on_2944 on theBenchmark for (2944ds/20139Mi) % 115.09/16.54 % (393493)Instruction limit reached! % 115.09/16.54 % (393493)------------------------------ % 115.09/16.54 % (393493)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 115.09/16.54 % (393493)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 115.09/16.54 % (393493)CaDiCaL version: 2.1.3 % 115.09/16.54 % (393493)Termination reason: Instruction limit % 115.09/16.54 % (393493)Termination phase: Saturation % 115.09/16.54 % (393493)Time elapsed: 2.569 s % 115.09/16.54 % (393493)Peak memory usage: 76 MB % 115.09/16.54 % (393493)Instructions burned: 8173 (million) % 115.09/16.54 % (393499)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=646869213:fmbsr=2:i=32576_2939 on theBenchmark for (2939ds/32576Mi) % 115.09/16.54 % (393499)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 115.09/16.54 % (393499)Terminated due to inappropriate strategy. % 115.09/16.54 % (393499)------------------------------ % 115.09/16.54 % (393499)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 115.09/16.54 % (393499)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 115.09/16.54 % (393499)CaDiCaL version: 2.1.3 % 115.09/16.54 % (393499)Termination reason: Inappropriate % 115.09/16.54 % (393499)Time elapsed: 0.015 s % 115.09/16.54 % (393499)Peak memory usage: 12 MB % 115.09/16.54 % (393499)Instructions burned: 61 (million) % 115.09/16.54 % (393499)------------------------------ % 115.09/16.54 % (393499)------------------------------ % 115.09/16.54 % (393501)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=1497700327:i=11404_2939 on theBenchmark for (2939ds/11404Mi) % 115.09/16.54 % (393495)Instruction limit reached! % 115.09/16.54 % (393495)------------------------------ % 115.09/16.54 % (393495)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 115.09/16.54 % (393495)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 115.09/16.54 % (393495)CaDiCaL version: 2.1.3 % 115.09/16.54 % (393495)Termination reason: Instruction limit % 115.09/16.54 % (393495)Termination phase: Saturation % 115.09/16.54 % (393495)Time elapsed: 4.680 s % 115.09/16.54 % (393495)Peak memory usage: 57 MB % 115.09/16.54 % (393495)Instructions burned: 9156 (million) % 115.09/16.54 % (393503)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=2171786739:i=14134_2916 on theBenchmark for (2916ds/14134Mi) % 115.09/16.54 % (393501)Instruction limit reached! % 115.09/16.54 % (393501)------------------------------ % 115.09/16.54 % (393501)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 115.09/16.54 % (393501)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 115.09/16.54 % (393501)CaDiCaL version: 2.1.3 % 115.09/16.54 % (393501)Termination reason: Instruction limit % 115.09/16.54 % (393501)Termination phase: Saturation % 115.09/16.54 % (393501)Time elapsed: 3.548 s % 115.09/16.54 % (393501)Peak memory usage: 81 MB % 115.09/16.54 % (393501)Instructions burned: 11406 (million) % 115.09/16.54 % (393505)dis+33_16_sil=32000:sac=on:random_seed=2702511102:i=15851:nm=0_2903 on theBenchmark for (2903ds/15851Mi) % 115.09/16.54 % (393491)Instruction limit reached! % 115.09/16.54 % (393491)------------------------------ % 115.09/16.54 % (393491)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 115.09/16.54 % (393491)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 115.09/16.54 % (393491)CaDiCaL version: 2.1.3 % 115.09/16.54 % (393491)Termination reason: Instruction limit % 115.09/16.54 % (393491)Termination phase: Saturation % 115.09/16.54 % (393491)Time elapsed: 9.533 s % 115.09/16.54 % (393491)Peak memory usage: 85 MB % 115.09/16.54 % (393491)Instructions burned: 22565 (million) % 115.09/16.54 % (393507)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=259870568:avsq=on:i=17627:add=on:amm=off_2872 on theBenchmark for (2872ds/17627Mi) % 157.40/22.43 % (393505)Instruction limit reached! % 157.40/22.43 % (393505)------------------------------ % 157.40/22.43 % (393505)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 157.40/22.43 % (393505)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.40/22.43 % (393505)CaDiCaL version: 2.1.3 % 157.40/22.43 % (393505)Termination reason: Instruction limit % 157.40/22.43 % (393505)Termination phase: Saturation % 157.40/22.43 % (393505)Time elapsed: 3.559 s % 157.40/22.43 % (393505)Peak memory usage: 18 MB % 157.40/22.43 % (393505)Instructions burned: 15855 (million) % 157.40/22.43 % (393557)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=1181265929:s2a=on:i=53295_2868 on theBenchmark for (2868ds/53295Mi) % 157.40/22.43 % (393497)Instruction limit reached! % 157.40/22.43 % (393497)------------------------------ % 157.40/22.43 % (393497)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 157.40/22.43 % (393497)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.40/22.43 % (393497)CaDiCaL version: 2.1.3 % 157.40/22.43 % (393497)Termination reason: Instruction limit % 157.40/22.43 % (393497)Termination phase: Saturation % 157.40/22.43 % (393497)Time elapsed: 8.570 s % 157.40/22.43 % (393497)Peak memory usage: 59 MB % 157.40/22.43 % (393497)Instructions burned: 20139 (million) % 157.40/22.43 % (393748)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=4171900806:i=26857:ins=20_2858 on theBenchmark for (2858ds/26857Mi) % 157.40/22.43 % (393748)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 157.40/22.43 % (393748)Terminated due to inappropriate strategy. % 157.40/22.43 % (393748)------------------------------ % 157.40/22.43 % (393748)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 157.40/22.43 % (393748)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.40/22.43 % (393748)CaDiCaL version: 2.1.3 % 157.40/22.43 % (393748)Termination reason: Inappropriate % 157.40/22.43 % (393748)Time elapsed: 0.039 s % 157.40/22.43 % (393748)Peak memory usage: 11 MB % 157.40/22.43 % (393748)Instructions burned: 61 (million) % 157.40/22.43 % (393748)------------------------------ % 157.40/22.43 % (393748)------------------------------ % 157.40/22.43 % (393767)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=3908135934:i=28120:bs=on:fsr=off_2857 on theBenchmark for (2857ds/28120Mi) % 157.40/22.43 % (393481)Instruction limit reached! % 157.40/22.43 % (393481)------------------------------ % 157.40/22.43 % (393481)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 157.40/22.43 % (393481)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.40/22.43 % (393481)CaDiCaL version: 2.1.3 % 157.40/22.43 % (393481)Termination reason: Instruction limit % 157.40/22.43 % (393481)Termination phase: Saturation % 157.40/22.43 % (393481)Time elapsed: 13.012 s % 157.40/22.43 % (393481)Peak memory usage: 50 MB % 157.40/22.43 % (393481)Instructions burned: 29340 (million) % 157.40/22.43 % (393928)fmb+10_1_sil=256000:fmbss=7:random_seed=662956112:fmbsr=1.6:i=182295_2844 on theBenchmark for (2844ds/182295Mi) % 157.40/22.43 % (393928)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 157.40/22.43 % (393928)Terminated due to inappropriate strategy. % 157.40/22.43 % (393928)------------------------------ % 157.40/22.43 % (393928)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 157.40/22.43 % (393928)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.40/22.43 % (393928)CaDiCaL version: 2.1.3 % 157.40/22.43 % (393928)Termination reason: Inappropriate % 157.40/22.43 % (393928)Time elapsed: 0.027 s % 157.40/22.43 % (393928)Peak memory usage: 11 MB % 157.40/22.43 % (393928)Instructions burned: 61 (million) % 157.40/22.43 % (393928)------------------------------ % 157.40/22.43 % (393928)------------------------------ % 157.40/22.43 % (393930)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=3280231535:i=44625:gsp=on_2844 on theBenchmark for (2844ds/44625Mi) % 157.40/22.43 % (393930)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 157.40/22.43 % (393930)Terminated due to inappropriate strategy. % 157.40/22.43 % (393930)------------------------------ % 157.40/22.43 % (393930)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 157.40/22.43 % (393930)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.40/22.43 % (393930)CaDiCaL version: 2.1.3 % 157.40/22.43 % (393930)Termination reason: Inappropriate % 180.08/25.68 % (393930)Time elapsed: 0.028 s % 180.08/25.68 % (393930)Peak memory usage: 12 MB % 180.08/25.68 % (393930)Instructions burned: 61 (million) % 180.08/25.68 % (393930)------------------------------ % 180.08/25.68 % (393930)------------------------------ % 180.08/25.68 % (393932)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=3768394181:i=160505_2843 on theBenchmark for (2843ds/160505Mi) % 180.08/25.68 % (393932)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 180.08/25.68 % (393932)Terminated due to inappropriate strategy. % 180.08/25.68 % (393932)------------------------------ % 180.08/25.68 % (393932)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 180.08/25.68 % (393932)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.08/25.68 % (393932)CaDiCaL version: 2.1.3 % 180.08/25.68 % (393932)Termination reason: Inappropriate % 180.08/25.68 % (393932)Time elapsed: 0.027 s % 180.08/25.68 % (393932)Peak memory usage: 11 MB % 180.08/25.68 % (393932)Instructions burned: 61 (million) % 180.08/25.68 % (393932)------------------------------ % 180.08/25.68 % (393932)------------------------------ % 180.08/25.68 % (393934)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=1971210002:fmbsr=1.3:i=225729_2843 on theBenchmark for (2843ds/225729Mi) % 180.08/25.68 % (393934)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 180.08/25.68 % (393934)Terminated due to inappropriate strategy. % 180.08/25.68 % (393934)------------------------------ % 180.08/25.68 % (393934)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 180.08/25.68 % (393934)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.08/25.68 % (393934)CaDiCaL version: 2.1.3 % 180.08/25.68 % (393934)Termination reason: Inappropriate % 180.08/25.68 % (393934)Time elapsed: 0.027 s % 180.08/25.68 % (393934)Peak memory usage: 11 MB % 180.08/25.68 % (393934)Instructions burned: 61 (million) % 180.08/25.68 % (393934)------------------------------ % 180.08/25.68 % (393934)------------------------------ % 180.08/25.68 % (393936)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=2036952736:fmbsr=2:i=185024:ins=7_2842 on theBenchmark for (2842ds/185024Mi) % 180.08/25.68 % (393936)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 180.08/25.68 % (393936)Terminated due to inappropriate strategy. % 180.08/25.68 % (393936)------------------------------ % 180.08/25.68 % (393936)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 180.08/25.68 % (393936)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.08/25.68 % (393936)CaDiCaL version: 2.1.3 % 180.08/25.68 % (393936)Termination reason: Inappropriate % 180.08/25.68 % (393936)Time elapsed: 0.027 s % 180.08/25.68 % (393936)Peak memory usage: 11 MB % 180.08/25.68 % (393936)Instructions burned: 61 (million) % 180.08/25.68 % (393936)------------------------------ % 180.08/25.68 % (393936)------------------------------ % 180.08/25.68 % (393938)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=3980346151:rtra=on_2842 on theBenchmark for (2842ds/0Mi) % 180.08/25.68 % (393938)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 180.08/25.68 % (393938)Terminated due to inappropriate strategy. % 180.08/25.68 % (393938)------------------------------ % 180.08/25.68 % (393938)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 180.08/25.68 % (393938)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.08/25.68 % (393938)CaDiCaL version: 2.1.3 % 180.08/25.68 % (393938)Termination reason: Inappropriate % 180.08/25.68 % (393938)Time elapsed: 0.032 s % 180.08/25.68 % (393938)Peak memory usage: 13 MB % 180.08/25.68 % (393938)Instructions burned: 65 (million) % 180.08/25.68 % (393938)------------------------------ % 180.08/25.68 % (393938)------------------------------ % 180.08/25.68 % (393940)% WARNING: option uhcvi not known. % 180.08/25.68 % (393940)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=4032813257:i=271062:add=off:rtra=on:rawr=on_2841 on theBenchmark for (2841ds/271062Mi) % 180.08/25.68 % (393503)Instruction limit reached! % 180.08/25.68 % (393503)------------------------------ % 180.08/25.68 % (393503)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 180.08/25.68 % (393503)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.08/25.68 % (393503)CaDiCaL version: 2.1.3 % 180.08/25.68 % (393503)Termination reason: Instruction limit % 180.08/25.68 % (393503)Termination phase: Saturation % 180.08/25.68 % (393503)Time elapsed: 7.971 s % 180.08/25.68 % (393503)Peak memory usage: 88 MB % 180.08/25.68 % (393503)Instructions burned: 14134 (million) % 193.60/27.52 % (393942)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3877672829:i=176048:add=on:rtra=on:rawr=on_2836 on theBenchmark for (2836ds/176048Mi) % 193.60/27.52 % (393507)Instruction limit reached! % 193.60/27.52 % (393507)------------------------------ % 193.60/27.52 % (393507)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 193.60/27.52 % (393507)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 193.60/27.52 % (393507)CaDiCaL version: 2.1.3 % 193.60/27.52 % (393507)Termination reason: Instruction limit % 193.60/27.52 % (393507)Termination phase: Saturation % 193.60/27.52 % (393507)Time elapsed: 8.643 s % 193.60/27.52 % (393507)Peak memory usage: 197 MB % 193.60/27.52 % (393507)Instructions burned: 17629 (million) % 193.60/27.52 % (393944)dis+10_1_sil=32000:si=on:sp=arity:random_seed=2753252248:i=206:fgj=on:rtra=on_2785 on theBenchmark for (2785ds/206Mi) % 193.60/27.52 % (393944)Instruction limit reached! % 193.60/27.52 % (393944)------------------------------ % 193.60/27.52 % (393944)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 193.60/27.52 % (393944)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 193.60/27.52 % (393944)CaDiCaL version: 2.1.3 % 193.60/27.52 % (393944)Termination reason: Instruction limit % 193.60/27.52 % (393944)Termination phase: Saturation % 193.60/27.52 % (393944)Time elapsed: 0.119 s % 193.60/27.52 % (393944)Peak memory usage: 15 MB % 193.60/27.52 % (393944)Instructions burned: 207 (million) % 193.60/27.52 % (393946)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=1556395195:i=232:rtra=on_2783 on theBenchmark for (2783ds/232Mi) % 193.60/27.52 % (393946)Instruction limit reached! % 193.60/27.52 % (393946)------------------------------ % 193.60/27.52 % (393946)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 193.60/27.52 % (393946)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 193.60/27.52 % (393946)CaDiCaL version: 2.1.3 % 193.60/27.52 % (393946)Termination reason: Instruction limit % 193.60/27.52 % (393946)Termination phase: Saturation % 193.60/27.52 % (393946)Time elapsed: 0.139 s % 193.60/27.52 % (393946)Peak memory usage: 15 MB % 193.60/27.52 % (393946)Instructions burned: 232 (million) % 193.60/27.52 % (393948)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=4012553138:i=262:rtra=on_2782 on theBenchmark for (2782ds/262Mi) % 193.60/27.52 % (393948)Instruction limit reached! % 193.60/27.52 % (393948)------------------------------ % 193.60/27.52 % (393948)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 193.60/27.52 % (393948)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 193.60/27.52 % (393948)CaDiCaL version: 2.1.3 % 193.60/27.52 % (393948)Termination reason: Instruction limit % 193.60/27.52 % (393948)Termination phase: Saturation % 193.60/27.52 % (393948)Time elapsed: 0.157 s % 193.60/27.52 % (393948)Peak memory usage: 16 MB % 193.60/27.52 % (393948)Instructions burned: 263 (million) % 193.60/27.52 % (393950)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=3734500554:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2780 on theBenchmark for (2780ds/318Mi) % 193.60/27.52 % (393950)Instruction limit reached! % 193.60/27.52 % (393950)------------------------------ % 193.60/27.52 % (393950)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 193.60/27.52 % (393950)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 193.60/27.52 % (393950)CaDiCaL version: 2.1.3 % 193.60/27.52 % (393950)Termination reason: Instruction limit % 193.60/27.52 % (393950)Termination phase: Saturation % 193.60/27.52 % (393950)Time elapsed: 0.192 s % 193.60/27.52 % (393950)Peak memory usage: 15 MB % 193.60/27.52 % (393950)Instructions burned: 319 (million) % 193.60/27.52 % (393952)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=1895730858:i=1428:nm=2:rtra=on_2778 on theBenchmark for (2778ds/1428Mi) % 193.60/27.52 % (393952)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 193.60/27.52 % (393952)Terminated due to inappropriate strategy. % 193.60/27.52 % (393952)------------------------------ % 193.60/27.52 % (393952)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 193.60/27.52 % (393952)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 193.60/27.52 % (393952)CaDiCaL version: 2.1.3 % 193.60/27.52 % (393952)Termination reason: Inappropriate % 193.60/27.52 % (393952)Time elapsed: 0.032 s % 193.60/27.52 % (393952)Peak memory usage: 12 MB % 193.60/27.52 % (393952)Instructions burned: 65 (million) % 193.60/27.52 % (393952)------------------------------ % 207.71/29.52 % (393952)------------------------------ % 207.71/29.52 % (393954)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=3391910213:i=262:bd=preordered:rtra=on:fsd=on_2777 on theBenchmark for (2777ds/262Mi) % 207.71/29.52 % (393954)Instruction limit reached! % 207.71/29.52 % (393954)------------------------------ % 207.71/29.52 % (393954)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 207.71/29.52 % (393954)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 207.71/29.52 % (393954)CaDiCaL version: 2.1.3 % 207.71/29.52 % (393954)Termination reason: Instruction limit % 207.71/29.52 % (393954)Termination phase: Saturation % 207.71/29.52 % (393954)Time elapsed: 0.169 s % 207.71/29.52 % (393954)Peak memory usage: 16 MB % 207.71/29.52 % (393954)Instructions burned: 262 (million) % 207.71/29.52 % (393956)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=2136185492:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2775 on theBenchmark for (2775ds/1368Mi) % 207.71/29.52 % (393956)Instruction limit reached! % 207.71/29.52 % (393956)------------------------------ % 207.71/29.52 % (393956)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 207.71/29.52 % (393956)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 207.71/29.52 % (393956)CaDiCaL version: 2.1.3 % 207.71/29.52 % (393956)Termination reason: Instruction limit % 207.71/29.52 % (393956)Termination phase: Saturation % 207.71/29.52 % (393956)Time elapsed: 0.790 s % 207.71/29.52 % (393956)Peak memory usage: 21 MB % 207.71/29.52 % (393956)Instructions burned: 1369 (million) % 207.71/29.52 % (393958)ott-21_1_sil=16000:si=on:fs=off:random_seed=429206625:i=360:av=off:fsr=off:rtra=on_2767 on theBenchmark for (2767ds/360Mi) % 207.71/29.52 % (393958)Instruction limit reached! % 207.71/29.52 % (393958)------------------------------ % 207.71/29.52 % (393958)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 207.71/29.52 % (393958)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 207.71/29.52 % (393958)CaDiCaL version: 2.1.3 % 207.71/29.52 % (393958)Termination reason: Instruction limit % 207.71/29.52 % (393958)Termination phase: Saturation % 207.71/29.52 % (393958)Time elapsed: 0.175 s % 207.71/29.52 % (393958)Peak memory usage: 15 MB % 207.71/29.52 % (393958)Instructions burned: 361 (million) % 207.71/29.52 % (393960)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1370906046:i=954:bd=all:rtra=on_2765 on theBenchmark for (2765ds/954Mi) % 207.71/29.52 % (393960)Instruction limit reached! % 207.71/29.52 % (393960)------------------------------ % 207.71/29.52 % (393960)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 207.71/29.52 % (393960)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 207.71/29.52 % (393960)CaDiCaL version: 2.1.3 % 207.71/29.52 % (393960)Termination reason: Instruction limit % 207.71/29.52 % (393960)Termination phase: Saturation % 207.71/29.52 % (393960)Time elapsed: 0.581 s % 207.71/29.52 % (393960)Peak memory usage: 19 MB % 207.71/29.52 % (393960)Instructions burned: 954 (million) % 207.71/29.52 % (393962)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=2488210272:fmbsr=1.3:i=1730:ins=25:rtra=on_2759 on theBenchmark for (2759ds/1730Mi) % 207.71/29.52 % (393962)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 207.71/29.52 % (393962)Terminated due to inappropriate strategy. % 207.71/29.52 % (393962)------------------------------ % 207.71/29.52 % (393962)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 207.71/29.52 % (393962)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 207.71/29.52 % (393962)CaDiCaL version: 2.1.3 % 207.71/29.52 % (393962)Termination reason: Inappropriate % 207.71/29.52 % (393962)Time elapsed: 0.032 s % 207.71/29.52 % (393962)Peak memory usage: 12 MB % 207.71/29.52 % (393962)Instructions burned: 65 (million) % 207.71/29.52 % (393962)------------------------------ % 207.71/29.52 % (393962)------------------------------ % 207.71/29.52 % (393964)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=1167174399:i=2358:rtra=on_2759 on theBenchmark for (2759ds/2358Mi) % 207.71/29.52 % (393964)Instruction limit reached! % 207.71/29.52 % (393964)------------------------------ % 207.71/29.52 % (393964)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 207.71/29.52 % (393964)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 207.71/29.52 % (393964)CaDiCaL version: 2.1.3 % 207.71/29.52 % (393964)Termination reason: Instruction limit % 207.71/29.52 % (393964)Termination phase: Saturation % 241.82/34.30 % (393964)Time elapsed: 1.368 s % 241.82/34.30 % (393964)Peak memory usage: 33 MB % 241.82/34.30 % (393964)Instructions burned: 2358 (million) % 241.82/34.30 % (393966)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=4178992831:i=1778:ins=1:rtra=on_2745 on theBenchmark for (2745ds/1778Mi) % 241.82/34.30 % (393966)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 241.82/34.30 % (393966)Terminated due to inappropriate strategy. % 241.82/34.30 % (393966)------------------------------ % 241.82/34.30 % (393966)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 241.82/34.30 % (393966)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 241.82/34.30 % (393966)CaDiCaL version: 2.1.3 % 241.82/34.30 % (393966)Termination reason: Inappropriate % 241.82/34.30 % (393966)Time elapsed: 0.032 s % 241.82/34.30 % (393966)Peak memory usage: 12 MB % 241.82/34.30 % (393966)Instructions burned: 65 (million) % 241.82/34.30 % (393966)------------------------------ % 241.82/34.30 % (393966)------------------------------ % 241.82/34.30 % (393968)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=3110666628:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2744 on theBenchmark for (2744ds/1384Mi) % 241.82/34.30 % (393968)Instruction limit reached! % 241.82/34.30 % (393968)------------------------------ % 241.82/34.30 % (393968)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 241.82/34.30 % (393968)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 241.82/34.30 % (393968)CaDiCaL version: 2.1.3 % 241.82/34.30 % (393968)Termination reason: Instruction limit % 241.82/34.30 % (393968)Termination phase: Saturation % 241.82/34.30 % (393968)Time elapsed: 0.820 s % 241.82/34.30 % (393968)Peak memory usage: 24 MB % 241.82/34.30 % (393968)Instructions burned: 1386 (million) % 241.82/34.30 % (393970)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=1806855102:i=1758:kws=inv_precedence:fsr=off:rtra=on_2736 on theBenchmark for (2736ds/1758Mi) % 241.82/34.30 % (393557)Instruction limit reached! % 241.82/34.30 % (393557)------------------------------ % 241.82/34.30 % (393557)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 241.82/34.30 % (393557)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 241.82/34.30 % (393557)CaDiCaL version: 2.1.3 % 241.82/34.30 % (393557)Termination reason: Instruction limit % 241.82/34.30 % (393557)Termination phase: Saturation % 241.82/34.30 % (393557)Time elapsed: 13.981 s % 241.82/34.30 % (393557)Peak memory usage: 647 MB % 241.82/34.30 % (393557)Instructions burned: 53297 (million) % 241.82/34.30 % (393972)fmb+10_1_sil=64000:si=on:random_seed=1538763307:i=44122:nm=2:rtra=on:gsp=on_2727 on theBenchmark for (2727ds/44122Mi) % 241.82/34.30 % (393972)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 241.82/34.30 % (393972)Terminated due to inappropriate strategy. % 241.82/34.30 % (393972)------------------------------ % 241.82/34.30 % (393972)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 241.82/34.30 % (393972)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 241.82/34.30 % (393972)CaDiCaL version: 2.1.3 % 241.82/34.30 % (393972)Termination reason: Inappropriate % 241.82/34.30 % (393972)Time elapsed: 0.017 s % 241.82/34.30 % (393972)Peak memory usage: 12 MB % 241.82/34.30 % (393972)Instructions burned: 66 (million) % 241.82/34.30 % (393972)------------------------------ % 241.82/34.30 % (393972)------------------------------ % 241.82/34.30 % (393974)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=2051396158:i=19030:nm=5:rtra=on_2727 on theBenchmark for (2727ds/19030Mi) % 241.82/34.30 % (393974)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 241.82/34.30 % (393974)Terminated due to inappropriate strategy. % 241.82/34.30 % (393974)------------------------------ % 241.82/34.30 % (393974)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 241.82/34.30 % (393974)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 241.82/34.30 % (393974)CaDiCaL version: 2.1.3 % 241.82/34.30 % (393974)Termination reason: Inappropriate % 241.82/34.30 % (393974)Time elapsed: 0.017 s % 241.82/34.30 % (393974)Peak memory usage: 12 MB % 241.82/34.30 % (393974)Instructions burned: 66 (million) % 241.82/34.30 % (393974)------------------------------ % 241.82/34.30 % (393974)------------------------------ % 241.82/34.30 % (393976)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=3886507457:fmbsr=1.7:i=1840:rtra=on_2727 on theBenchmark for (2727ds/1840Mi) % 272.41/38.65 % (393976)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 272.41/38.65 % (393976)Terminated due to inappropriate strategy. % 272.41/38.65 % (393976)------------------------------ % 272.41/38.65 % (393976)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 272.41/38.65 % (393976)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 272.41/38.65 % (393976)CaDiCaL version: 2.1.3 % 272.41/38.65 % (393976)Termination reason: Inappropriate % 272.41/38.65 % (393976)Time elapsed: 0.017 s % 272.41/38.65 % (393976)Peak memory usage: 12 MB % 272.41/38.65 % (393976)Instructions burned: 65 (million) % 272.41/38.65 % (393976)------------------------------ % 272.41/38.65 % (393976)------------------------------ % 272.41/38.65 % (393978)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=1972948521:i=10262:rtra=on_2726 on theBenchmark for (2726ds/10262Mi) % 272.41/38.65 % (393970)Instruction limit reached! % 272.41/38.65 % (393970)------------------------------ % 272.41/38.65 % (393970)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 272.41/38.65 % (393970)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 272.41/38.65 % (393970)CaDiCaL version: 2.1.3 % 272.41/38.65 % (393970)Termination reason: Instruction limit % 272.41/38.65 % (393970)Termination phase: Saturation % 272.41/38.65 % (393970)Time elapsed: 0.988 s % 272.41/38.65 % (393970)Peak memory usage: 25 MB % 272.41/38.65 % (393970)Instructions burned: 1760 (million) % 272.41/38.65 % (393980)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2244339956:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2726 on theBenchmark for (2726ds/2944Mi) % 272.41/38.65 % (393980)Instruction limit reached! % 272.41/38.65 % (393980)------------------------------ % 272.41/38.65 % (393980)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 272.41/38.65 % (393980)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 272.41/38.65 % (393980)CaDiCaL version: 2.1.3 % 272.41/38.65 % (393980)Termination reason: Instruction limit % 272.41/38.65 % (393980)Termination phase: Saturation % 272.41/38.65 % (393980)Time elapsed: 1.675 s % 272.41/38.65 % (393980)Peak memory usage: 41 MB % 272.41/38.65 % (393980)Instructions burned: 2944 (million) % 272.41/38.65 % (394270)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=1237760432:i=12648:rtra=on_2709 on theBenchmark for (2709ds/12648Mi) % 272.41/38.65 % (394270)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 272.41/38.65 % (394270)Terminated due to inappropriate strategy. % 272.41/38.65 % (394270)------------------------------ % 272.41/38.65 % (394270)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 272.41/38.65 % (394270)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 272.41/38.65 % (394270)CaDiCaL version: 2.1.3 % 272.41/38.65 % (394270)Termination reason: Inappropriate % 272.41/38.65 % (394270)Time elapsed: 0.032 s % 272.41/38.65 % (394270)Peak memory usage: 12 MB % 272.41/38.65 % (394270)Instructions burned: 66 (million) % 272.41/38.65 % (394270)------------------------------ % 272.41/38.65 % (394270)------------------------------ % 272.41/38.65 % (394288)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=1395503226:fmbsr=2.30978:i=4348:rtra=on_2708 on theBenchmark for (2708ds/4348Mi) % 272.41/38.65 % (394288)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 272.41/38.65 % (394288)Terminated due to inappropriate strategy. % 272.41/38.65 % (394288)------------------------------ % 272.41/38.65 % (394288)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 272.41/38.65 % (394288)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 272.41/38.65 % (394288)CaDiCaL version: 2.1.3 % 272.41/38.65 % (394288)Termination reason: Inappropriate % 272.41/38.65 % (394288)Time elapsed: 0.032 s % 272.41/38.65 % (394288)Peak memory usage: 12 MB % 272.41/38.65 % (394288)Instructions burned: 65 (million) % 272.41/38.65 % (394288)------------------------------ % 272.41/38.65 % (394288)------------------------------ % 272.41/38.65 % (394320)ott-2_1_sil=16000:si=on:newcnf=on:random_seed=3221842947:avsq=on:i=1738:avsqr=1,16:kws=inv_arity_squared:rtra=on_2708 on theBenchmark for (2708ds/1738Mi) % 272.41/38.65 % (393767)Instruction limit reached! % 272.41/38.65 % (393767)------------------------------ % 272.41/38.65 % (393767)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 272.41/38.65 % (393767)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.09/42.53 % (393767)CaDiCaL version: 2.1.3 % 300.09/42.53 % (393767)Termination reason: Instruction limit % 300.09/42.53 % (393767)Termination phase: Saturation % 300.09/42.53 % (393767)Time elapsed: 15.039 s % 300.09/42.53 % (393767)Peak memory usage: 93 MB % 300.09/42.53 % (393767)Instructions burned: 28121 (million) % 300.09/42.53 % (394331)ott+10_1_sil=32000:tgt=ground:si=on:random_seed=1846245120:i=10228:av=off:rtra=on_2706 on theBenchmark for (2706ds/10228Mi) % 300.09/42.53 % (394320)Instruction limit reached! % 300.09/42.53 % (394320)------------------------------ % 300.09/42.53 % (394320)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.09/42.53 % (394320)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.09/42.53 % (394320)CaDiCaL version: 2.1.3 % 300.09/42.53 % (394320)Termination reason: Instruction limit % 300.09/42.53 % (394320)Termination phase: Saturation % 300.09/42.53 % (394320)Time elapsed: 0.954 s % 300.09/42.53 % (394320)Peak memory usage: 27 MB % 300.09/42.53 % (394320)Instructions burned: 1739 (million) % 300.09/42.53 % (394333)fmb+10_1_sil=64000:sas=cadical:si=on:bce=on:rp=on:random_seed=1951523065:i=108564:rtra=on_2698 on theBenchmark for (2698ds/108564Mi) % 300.09/42.53 % (394333)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.09/42.53 % (394333)Terminated due to inappropriate strategy. % 300.09/42.53 % (394333)------------------------------ % 300.09/42.53 % (394333)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.09/42.53 % (394333)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.09/42.53 % (394333)CaDiCaL version: 2.1.3 % 300.09/42.53 % (394333)Termination reason: Inappropriate % 300.09/42.53 % (394333)Time elapsed: 0.032 s % 300.09/42.53 % (394333)Peak memory usage: 12 MB % 300.09/42.53 % (394333)Instructions burned: 66 (million) % 300.09/42.53 % (394333)------------------------------ % 300.09/42.53 % (394333)------------------------------ % 300.09/42.53 % (394335)dis-11_1_sil=16000:si=on:sp=reverse_frequency:alpa=true:random_seed=612430737:i=7024:aac=none:rtra=on_2697 on theBenchmark for (2697ds/7024Mi) % 300.09/42.53 % (393978)Instruction limit reached! % 300.09/42.53 % (393978)------------------------------ % 300.09/42.53 % (393978)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.09/42.53 % (393978)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.09/42.53 % (393978)CaDiCaL version: 2.1.3 % 300.09/42.53 % (393978)Termination reason: Instruction limit % 300.09/42.53 % (393978)Termination phase: Saturation % 300.09/42.53 % (393978)Time elapsed: 3.116 s % 300.09/42.53 % (393978)Peak memory usage: 72 MB % 300.09/42.53 % (393978)Instructions burned: 10264 (million) % 300.09/42.53 % (394337)dis+21_1_sil=32000:sas=cadical:si=on:random_seed=280718962:i=7546:rtra=on:amm=off_2695 on theBenchmark for (2695ds/7546Mi) % 300.09/42.53 % (394337)Instruction limit reached! % 300.09/42.53 % (394337)------------------------------ % 300.09/42.53 % (394337)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.09/42.53 % (394337)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.09/42.53 % (394337)CaDiCaL version: 2.1.3 % 300.09/42.53 % (394337)Termination reason: Instruction limit % 300.09/42.53 % (394337)Termination phase: Saturation % 300.09/42.53 % (394337)Time elapsed: 2.233 s % 300.09/42.53 % (394337)Peak memory usage: 57 MB % 300.09/42.53 % (394337)Instructions burned: 7546 (million) % 300.09/42.53 % (394339)ott+11_1_sil=16000:si=on:gs=on:random_seed=3311967665:s2a=on:i=4502:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:rtra=on:fsd=on_2672 on theBenchmark for (2672ds/4502Mi) % 300.09/42.53 % (394335)Instruction limit reached! % 300.09/42.53 % (394335)------------------------------ % 300.09/42.53 % (394335)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.09/42.53 % (394335)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.09/42.53 % (394335)CaDiCaL version: 2.1.3 % 300.09/42.53 % (394335)Termination reason: Instruction limit % 300.09/42.53 % (394335)Termination phase: Saturation % 300.09/42.53 % (394335)Time elapsed: 3.802 s % 300.09/42.53 % (394335)Peak memory usage: 52 MB % 300.09/42.53 % (394335)Instructions burned: 7024 (million) % 300.09/42.53 % (394341)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:si=on:fmbss=7:random_seed=4039900694:fmbsr=1.6:i=135068:rtra=on_2659 on theBenchmark for (2659ds/135068Mi) % 300.09/42.53 % (394341)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.09/42.53 % (394341)Terminated due to inappropriate strategy. % 300.09/42.53 % (394341)------------------------------ % 300.09/42.53 % (39434 % 300.09/42.54 Terminated % 300.09/42.54 % Vampire exiting %------------------------------------------------------------------------------