%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWC461_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:02 PM UTC 2026 % Result : Timeout 300.11s 42.53s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWC461_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.08/0.18 % Computer : n014.cluster.edu % 0.08/0.18 % Model : x86_64 x86_64 % 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.18 % Memory : 8046.5625MB % 0.08/0.18 % OS : Linux 6.8.0-71-generic % 0.08/0.18 % CPULimit : 300 % 0.08/0.18 % WCLimit : 300 % 0.08/0.18 % DateTime : Mon Sep 28 09:39:08 UTC 2026 % 0.08/0.18 % CPUTime : % 0.08/0.18 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 % 3.32/0.70 % (1663487)Will run a generic schedule for satisfiability detection. % 3.32/0.70 % (1663492)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=466977637_2999 on theBenchmark for (2999ds/0Mi) % 3.32/0.70 % (1663492)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.32/0.70 % (1663492)Terminated due to inappropriate strategy. % 3.32/0.70 % (1663492)------------------------------ % 3.32/0.70 % (1663492)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.32/0.70 % (1663492)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.32/0.70 % (1663492)CaDiCaL version: 2.1.3 % 3.32/0.70 % (1663492)Termination reason: Inappropriate % 3.32/0.70 % (1663492)Time elapsed: 0.001 s % 3.32/0.70 % (1663492)Peak memory usage: 10 MB % 3.32/0.70 % (1663492)Instructions burned: 2 (million) % 3.32/0.70 % (1663492)------------------------------ % 3.32/0.70 % (1663492)------------------------------ % 3.32/0.70 % (1663493)% WARNING: option uhcvi not known. % 3.32/0.70 % (1663495)dis+10_1_sil=32000:sp=arity:random_seed=3385002983:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 3.32/0.70 % (1663497)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=315236293:i=131_2999 on theBenchmark for (2999ds/131Mi) % 3.32/0.70 % (1663494)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2308526149:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 3.32/0.70 % (1663493)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3963619860:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 3.32/0.70 % (1663496)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=4008426527:i=116_2999 on theBenchmark for (2999ds/116Mi) % 3.32/0.70 % (1663498)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3291829854:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 3.32/0.70 % (1663500)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2140515973:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 3.32/0.70 % (1663500)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.32/0.70 % (1663500)Terminated due to inappropriate strategy. % 3.32/0.70 % (1663500)------------------------------ % 3.32/0.70 % (1663500)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.32/0.70 % (1663500)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.32/0.70 % (1663500)CaDiCaL version: 2.1.3 % 3.32/0.70 % (1663500)Termination reason: Inappropriate % 3.32/0.70 % (1663500)Time elapsed: 0.0000 s % 3.32/0.70 % (1663500)Peak memory usage: 11 MB % 3.32/0.70 % (1663500)Instructions burned: 2 (million) % 3.32/0.70 % (1663500)------------------------------ % 3.32/0.70 % (1663500)------------------------------ % 3.32/0.70 % (1663508)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=41410762:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 3.32/0.70 % (1663495)Instruction limit reached! % 3.32/0.70 % (1663495)------------------------------ % 3.32/0.70 % (1663495)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.32/0.70 % (1663495)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.32/0.70 % (1663495)CaDiCaL version: 2.1.3 % 3.32/0.70 % (1663495)Termination reason: Instruction limit % 3.32/0.70 % (1663495)Termination phase: Saturation % 3.32/0.70 % (1663495)Time elapsed: 0.063 s % 3.32/0.70 % (1663495)Peak memory usage: 13 MB % 3.32/0.70 % (1663495)Instructions burned: 104 (million) % 3.32/0.70 % (1663496)Instruction limit reached! % 3.32/0.70 % (1663496)------------------------------ % 3.32/0.70 % (1663496)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.32/0.70 % (1663496)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.32/0.70 % (1663496)CaDiCaL version: 2.1.3 % 3.32/0.70 % (1663496)Termination reason: Instruction limit % 3.32/0.70 % (1663496)Termination phase: Saturation % 3.32/0.70 % (1663496)Time elapsed: 0.070 s % 3.32/0.70 % (1663496)Peak memory usage: 12 MB % 3.32/0.70 % (1663496)Instructions burned: 117 (million) % 3.32/0.70 % (1663497)Instruction limit reached! % 3.32/0.70 % (1663497)------------------------------ % 3.32/0.70 % (1663497)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.32/0.70 % (1663497)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.32/0.70 % (1663497)CaDiCaL version: 2.1.3 % 3.32/0.70 % (1663497)Termination reason: Instruction limit % 5.79/1.04 % (1663497)Termination phase: Saturation % 5.79/1.04 % (1663497)Time elapsed: 0.077 s % 5.79/1.04 % (1663497)Peak memory usage: 13 MB % 5.79/1.04 % (1663497)Instructions burned: 132 (million) % 5.79/1.04 % (1663510)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=3248834239:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 5.79/1.04 % (1663511)ott-21_1_sil=16000:fs=off:random_seed=3585759770:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi) % 5.79/1.04 % (1663512)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3091787169:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 5.79/1.04 % (1663498)Instruction limit reached! % 5.79/1.04 % (1663498)------------------------------ % 5.79/1.04 % (1663498)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.79/1.04 % (1663498)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.79/1.04 % (1663498)CaDiCaL version: 2.1.3 % 5.79/1.04 % (1663498)Termination reason: Instruction limit % 5.79/1.04 % (1663498)Termination phase: Saturation % 5.79/1.04 % (1663498)Time elapsed: 0.102 s % 5.79/1.04 % (1663498)Peak memory usage: 13 MB % 5.79/1.04 % (1663498)Instructions burned: 159 (million) % 5.79/1.04 % (1663508)Instruction limit reached! % 5.79/1.04 % (1663508)------------------------------ % 5.79/1.04 % (1663508)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.79/1.04 % (1663508)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.79/1.04 % (1663508)CaDiCaL version: 2.1.3 % 5.79/1.04 % (1663508)Termination reason: Instruction limit % 5.79/1.04 % (1663508)Termination phase: Saturation % 5.79/1.04 % (1663508)Time elapsed: 0.077 s % 5.79/1.04 % (1663508)Peak memory usage: 12 MB % 5.79/1.04 % (1663508)Instructions burned: 132 (million) % 5.79/1.04 % (1663516)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1358879511:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 5.79/1.04 % (1663516)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 5.79/1.04 % (1663516)Terminated due to inappropriate strategy. % 5.79/1.04 % (1663516)------------------------------ % 5.79/1.04 % (1663516)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.79/1.04 % (1663516)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.79/1.04 % (1663516)CaDiCaL version: 2.1.3 % 5.79/1.04 % (1663516)Termination reason: Inappropriate % 5.79/1.04 % (1663516)Time elapsed: 0.0000 s % 5.79/1.04 % (1663516)Peak memory usage: 10 MB % 5.79/1.04 % (1663516)Instructions burned: 2 (million) % 5.79/1.04 % (1663516)------------------------------ % 5.79/1.04 % (1663516)------------------------------ % 5.79/1.04 % (1663519)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3658656080:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 5.79/1.04 % (1663517)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2125900444:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 5.79/1.04 % (1663519)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 5.79/1.04 % (1663519)Terminated due to inappropriate strategy. % 5.79/1.04 % (1663519)------------------------------ % 5.79/1.04 % (1663519)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.79/1.04 % (1663519)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.79/1.04 % (1663519)CaDiCaL version: 2.1.3 % 5.79/1.04 % (1663519)Termination reason: Inappropriate % 5.79/1.04 % (1663519)Time elapsed: 0.0000 s % 5.79/1.04 % (1663519)Peak memory usage: 11 MB % 5.79/1.04 % (1663519)Instructions burned: 2 (million) % 5.79/1.04 % (1663519)------------------------------ % 5.79/1.04 % (1663519)------------------------------ % 5.79/1.04 % (1663522)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=4282165809: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) % 5.79/1.04 % (1663511)Instruction limit reached! % 5.79/1.04 % (1663511)------------------------------ % 5.79/1.04 % (1663511)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.79/1.04 % (1663511)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.79/1.04 % (1663511)CaDiCaL version: 2.1.3 % 5.79/1.04 % (1663511)Termination reason: Instruction limit % 5.79/1.04 % (1663511)Termination phase: Saturation % 18.14/2.93 % (1663511)Time elapsed: 0.083 s % 18.14/2.93 % (1663511)Peak memory usage: 12 MB % 18.14/2.93 % (1663511)Instructions burned: 180 (million) % 18.14/2.93 % (1663524)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2613709360:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 18.14/2.93 % (1663522)Instruction limit reached! % 18.14/2.93 % (1663522)------------------------------ % 18.14/2.93 % (1663522)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.14/2.93 % (1663522)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.14/2.93 % (1663522)CaDiCaL version: 2.1.3 % 18.14/2.93 % (1663522)Termination reason: Instruction limit % 18.14/2.93 % (1663522)Termination phase: Saturation % 18.14/2.93 % (1663522)Time elapsed: 0.221 s % 18.14/2.93 % (1663522)Peak memory usage: 18 MB % 18.14/2.93 % (1663522)Instructions burned: 694 (million) % 18.14/2.93 % (1663526)fmb+10_1_sil=64000:random_seed=2638147844:i=22061:nm=2:gsp=on_2996 on theBenchmark for (2996ds/22061Mi) % 18.14/2.93 % (1663526)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 18.14/2.93 % (1663526)Terminated due to inappropriate strategy. % 18.14/2.93 % (1663526)------------------------------ % 18.14/2.93 % (1663526)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.14/2.93 % (1663526)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.14/2.93 % (1663526)CaDiCaL version: 2.1.3 % 18.14/2.93 % (1663526)Termination reason: Inappropriate % 18.14/2.93 % (1663526)Time elapsed: 0.0000 s % 18.14/2.93 % (1663526)Peak memory usage: 10 MB % 18.14/2.93 % (1663526)Instructions burned: 2 (million) % 18.14/2.93 % (1663526)------------------------------ % 18.14/2.93 % (1663526)------------------------------ % 18.14/2.93 % (1663512)Instruction limit reached! % 18.14/2.93 % (1663512)------------------------------ % 18.14/2.93 % (1663512)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.14/2.93 % (1663512)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.14/2.93 % (1663512)CaDiCaL version: 2.1.3 % 18.14/2.93 % (1663512)Termination reason: Instruction limit % 18.14/2.93 % (1663512)Termination phase: Saturation % 18.14/2.93 % (1663512)Time elapsed: 0.286 s % 18.14/2.93 % (1663512)Peak memory usage: 13 MB % 18.14/2.93 % (1663512)Instructions burned: 477 (million) % 18.14/2.93 % (1663528)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=872587846:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi) % 18.14/2.93 % (1663528)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 18.14/2.93 % (1663528)Terminated due to inappropriate strategy. % 18.14/2.93 % (1663528)------------------------------ % 18.14/2.93 % (1663528)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.14/2.93 % (1663528)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.14/2.93 % (1663528)CaDiCaL version: 2.1.3 % 18.14/2.93 % (1663528)Termination reason: Inappropriate % 18.14/2.93 % (1663528)Time elapsed: 0.0000 s % 18.14/2.93 % (1663528)Peak memory usage: 10 MB % 18.14/2.93 % (1663528)Instructions burned: 2 (million) % 18.14/2.93 % (1663528)------------------------------ % 18.14/2.93 % (1663528)------------------------------ % 18.14/2.93 % (1663529)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=464564316:fmbsr=1.7:i=920_2995 on theBenchmark for (2995ds/920Mi) % 18.14/2.93 % (1663531)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3326709542:i=5131_2995 on theBenchmark for (2995ds/5131Mi) % 18.14/2.93 % (1663529)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 18.14/2.93 % (1663529)Terminated due to inappropriate strategy. % 18.14/2.93 % (1663529)------------------------------ % 18.14/2.93 % (1663529)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.14/2.93 % (1663529)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.14/2.93 % (1663529)CaDiCaL version: 2.1.3 % 18.14/2.93 % (1663529)Termination reason: Inappropriate % 18.14/2.93 % (1663529)Time elapsed: 0.001 s % 18.14/2.93 % (1663529)Peak memory usage: 10 MB % 18.14/2.93 % (1663529)Instructions burned: 2 (million) % 18.14/2.93 % (1663529)------------------------------ % 18.14/2.93 % (1663529)------------------------------ % 18.14/2.93 % (1663534)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3944221626:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi) % 18.14/2.93 % (1663510)Instruction limit reached! % 18.14/2.93 % (1663510)------------------------------ % 27.10/4.10 % (1663510)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.10/4.10 % (1663510)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.10/4.10 % (1663510)CaDiCaL version: 2.1.3 % 27.10/4.10 % (1663510)Termination reason: Instruction limit % 27.10/4.10 % (1663510)Termination phase: Saturation % 27.10/4.10 % (1663510)Time elapsed: 0.375 s % 27.10/4.10 % (1663510)Peak memory usage: 17 MB % 27.10/4.10 % (1663510)Instructions burned: 685 (million) % 27.10/4.10 % (1663536)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2646482450:i=6324_2995 on theBenchmark for (2995ds/6324Mi) % 27.10/4.10 % (1663536)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 27.10/4.10 % (1663536)Terminated due to inappropriate strategy. % 27.10/4.10 % (1663536)------------------------------ % 27.10/4.10 % (1663536)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.10/4.10 % (1663536)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.10/4.10 % (1663536)CaDiCaL version: 2.1.3 % 27.10/4.10 % (1663536)Termination reason: Inappropriate % 27.10/4.10 % (1663536)Time elapsed: 0.001 s % 27.10/4.10 % (1663536)Peak memory usage: 10 MB % 27.10/4.10 % (1663536)Instructions burned: 2 (million) % 27.10/4.10 % (1663536)------------------------------ % 27.10/4.10 % (1663536)------------------------------ % 27.10/4.10 % (1663538)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2729063594:fmbsr=2.30978:i=2174_2994 on theBenchmark for (2994ds/2174Mi) % 27.10/4.10 % (1663538)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 27.10/4.10 % (1663538)Terminated due to inappropriate strategy. % 27.10/4.10 % (1663538)------------------------------ % 27.10/4.10 % (1663538)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.10/4.10 % (1663538)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.10/4.10 % (1663538)CaDiCaL version: 2.1.3 % 27.10/4.10 % (1663538)Termination reason: Inappropriate % 27.10/4.10 % (1663538)Time elapsed: 0.001 s % 27.10/4.10 % (1663538)Peak memory usage: 11 MB % 27.10/4.10 % (1663538)Instructions burned: 2 (million) % 27.10/4.10 % (1663538)------------------------------ % 27.10/4.10 % (1663538)------------------------------ % 27.10/4.10 % (1663540)ott-2_1_sil=16000:newcnf=on:random_seed=3544035288:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2994 on theBenchmark for (2994ds/869Mi) % 27.10/4.10 % (1663524)Instruction limit reached! % 27.10/4.10 % (1663524)------------------------------ % 27.10/4.10 % (1663524)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.10/4.10 % (1663524)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.10/4.10 % (1663524)CaDiCaL version: 2.1.3 % 27.10/4.10 % (1663524)Termination reason: Instruction limit % 27.10/4.10 % (1663524)Termination phase: Saturation % 27.10/4.10 % (1663524)Time elapsed: 0.497 s % 27.10/4.10 % (1663524)Peak memory usage: 19 MB % 27.10/4.10 % (1663524)Instructions burned: 879 (million) % 27.10/4.10 % (1663542)ott+10_1_sil=32000:tgt=ground:random_seed=2479974263:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi) % 27.10/4.10 % (1663517)Instruction limit reached! % 27.10/4.10 % (1663517)------------------------------ % 27.10/4.10 % (1663517)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.10/4.10 % (1663517)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.10/4.10 % (1663517)CaDiCaL version: 2.1.3 % 27.10/4.10 % (1663517)Termination reason: Instruction limit % 27.10/4.10 % (1663517)Termination phase: Saturation % 27.10/4.10 % (1663517)Time elapsed: 0.646 s % 27.10/4.10 % (1663517)Peak memory usage: 19 MB % 27.10/4.10 % (1663517)Instructions burned: 1179 (million) % 27.10/4.10 % (1663544)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2802593452:i=54282_2991 on theBenchmark for (2991ds/54282Mi) % 27.10/4.10 % (1663544)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 27.10/4.10 % (1663544)Terminated due to inappropriate strategy. % 27.10/4.10 % (1663544)------------------------------ % 27.10/4.10 % (1663544)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.10/4.10 % (1663544)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.10/4.10 % (1663544)CaDiCaL version: 2.1.3 % 27.10/4.10 % (1663544)Termination reason: Inappropriate % 27.10/4.10 % (1663544)Time elapsed: 0.002 s % 27.10/4.10 % (1663544)Peak memory usage: 10 MB % 27.10/4.10 % (1663544)Instructions burned: 2 (million) % 82.92/12.01 % (1663544)------------------------------ % 82.92/12.01 % (1663544)------------------------------ % 82.92/12.01 % (1663546)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3440221957:i=3512:aac=none_2991 on theBenchmark for (2991ds/3512Mi) % 82.92/12.01 % (1663540)Instruction limit reached! % 82.92/12.01 % (1663540)------------------------------ % 82.92/12.01 % (1663540)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 82.92/12.01 % (1663540)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 82.92/12.01 % (1663540)CaDiCaL version: 2.1.3 % 82.92/12.01 % (1663540)Termination reason: Instruction limit % 82.92/12.01 % (1663540)Termination phase: Saturation % 82.92/12.01 % (1663540)Time elapsed: 0.479 s % 82.92/12.01 % (1663540)Peak memory usage: 15 MB % 82.92/12.01 % (1663540)Instructions burned: 869 (million) % 82.92/12.01 % (1663548)dis+21_1_sil=32000:sas=cadical:random_seed=1893526622:i=3773:amm=off_2989 on theBenchmark for (2989ds/3773Mi) % 82.92/12.01 % (1663534)Instruction limit reached! % 82.92/12.01 % (1663534)------------------------------ % 82.92/12.01 % (1663534)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 82.92/12.01 % (1663534)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 82.92/12.01 % (1663534)CaDiCaL version: 2.1.3 % 82.92/12.01 % (1663534)Termination reason: Instruction limit % 82.92/12.01 % (1663534)Termination phase: Saturation % 82.92/12.01 % (1663534)Time elapsed: 0.830 s % 82.92/12.01 % (1663534)Peak memory usage: 24 MB % 82.92/12.01 % (1663534)Instructions burned: 1472 (million) % 82.92/12.01 % (1663550)ott+11_1_sil=16000:gs=on:random_seed=226988923:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2987 on theBenchmark for (2987ds/2251Mi) % 82.92/12.01 % (1663531)Instruction limit reached! % 82.92/12.01 % (1663531)------------------------------ % 82.92/12.01 % (1663531)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 82.92/12.01 % (1663531)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 82.92/12.01 % (1663531)CaDiCaL version: 2.1.3 % 82.92/12.01 % (1663531)Termination reason: Instruction limit % 82.92/12.01 % (1663531)Termination phase: Saturation % 82.92/12.01 % (1663531)Time elapsed: 1.469 s % 82.92/12.01 % (1663531)Peak memory usage: 40 MB % 82.92/12.01 % (1663531)Instructions burned: 5133 (million) % 82.92/12.01 % (1663552)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2404881559:fmbsr=1.6:i=67534_2980 on theBenchmark for (2980ds/67534Mi) % 82.92/12.01 % (1663552)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 82.92/12.01 % (1663552)Terminated due to inappropriate strategy. % 82.92/12.01 % (1663552)------------------------------ % 82.92/12.01 % (1663552)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 82.92/12.01 % (1663552)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 82.92/12.01 % (1663552)CaDiCaL version: 2.1.3 % 82.92/12.01 % (1663552)Termination reason: Inappropriate % 82.92/12.01 % (1663552)Time elapsed: 0.0000 s % 82.92/12.01 % (1663552)Peak memory usage: 10 MB % 82.92/12.01 % (1663552)Instructions burned: 2 (million) % 82.92/12.01 % (1663552)------------------------------ % 82.92/12.01 % (1663552)------------------------------ % 82.92/12.01 % (1663554)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1510503845:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2980 on theBenchmark for (2980ds/4591Mi) % 82.92/12.01 % (1663550)Instruction limit reached! % 82.92/12.01 % (1663550)------------------------------ % 82.92/12.01 % (1663550)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 82.92/12.01 % (1663550)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 82.92/12.01 % (1663550)CaDiCaL version: 2.1.3 % 82.92/12.01 % (1663550)Termination reason: Instruction limit % 82.92/12.01 % (1663550)Termination phase: Saturation % 82.92/12.01 % (1663550)Time elapsed: 1.229 s % 82.92/12.01 % (1663550)Peak memory usage: 23 MB % 82.92/12.01 % (1663550)Instructions burned: 2251 (million) % 82.92/12.01 % (1663556)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2585283213:i=29340_2974 on theBenchmark for (2974ds/29340Mi) % 82.92/12.01 % (1663546)Instruction limit reached! % 82.92/12.01 % (1663546)------------------------------ % 82.92/12.01 % (1663546)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 82.92/12.01 % (1663546)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 82.92/12.01 % (1663546)CaDiCaL version: 2.1.3 % 82.92/12.01 % (1663546)Termination reason: Instruction limit % 115.15/16.51 % (1663546)Termination phase: Saturation % 115.15/16.51 % (1663546)Time elapsed: 1.864 s % 115.15/16.51 % (1663546)Peak memory usage: 31 MB % 115.15/16.51 % (1663546)Instructions burned: 3514 (million) % 115.15/16.51 % (1663558)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2712562168:i=5211_2972 on theBenchmark for (2972ds/5211Mi) % 115.15/16.51 % (1663548)Instruction limit reached! % 115.15/16.51 % (1663548)------------------------------ % 115.15/16.51 % (1663548)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 115.15/16.51 % (1663548)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 115.15/16.51 % (1663548)CaDiCaL version: 2.1.3 % 115.15/16.51 % (1663548)Termination reason: Instruction limit % 115.15/16.51 % (1663548)Termination phase: Saturation % 115.15/16.51 % (1663548)Time elapsed: 2.057 s % 115.15/16.51 % (1663548)Peak memory usage: 31 MB % 115.15/16.51 % (1663548)Instructions burned: 3773 (million) % 115.15/16.51 % (1663560)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1703573941:i=5497:nm=2_2968 on theBenchmark for (2968ds/5497Mi) % 115.15/16.51 % (1663554)Instruction limit reached! % 115.15/16.51 % (1663554)------------------------------ % 115.15/16.51 % (1663554)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 115.15/16.51 % (1663554)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 115.15/16.51 % (1663554)CaDiCaL version: 2.1.3 % 115.15/16.51 % (1663554)Termination reason: Instruction limit % 115.15/16.51 % (1663554)Termination phase: Saturation % 115.15/16.51 % (1663554)Time elapsed: 1.201 s % 115.15/16.51 % (1663554)Peak memory usage: 43 MB % 115.15/16.51 % (1663554)Instructions burned: 4594 (million) % 115.15/16.51 % (1663560)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 115.15/16.51 % (1663560)Terminated due to inappropriate strategy. % 115.15/16.51 % (1663560)------------------------------ % 115.15/16.51 % (1663560)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 115.15/16.51 % (1663560)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 115.15/16.51 % (1663560)CaDiCaL version: 2.1.3 % 115.15/16.51 % (1663560)Termination reason: Inappropriate % 115.15/16.51 % (1663560)Time elapsed: 0.001 s % 115.15/16.51 % (1663560)Peak memory usage: 10 MB % 115.15/16.51 % (1663560)Instructions burned: 2 (million) % 115.15/16.51 % (1663560)------------------------------ % 115.15/16.51 % (1663560)------------------------------ % 115.15/16.51 % (1663563)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=531208582:i=14071_2968 on theBenchmark for (2968ds/14071Mi) % 115.15/16.51 % (1663563)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 115.15/16.51 % (1663563)Terminated due to inappropriate strategy. % 115.15/16.51 % (1663563)------------------------------ % 115.15/16.51 % (1663563)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 115.15/16.51 % (1663563)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 115.15/16.51 % (1663563)CaDiCaL version: 2.1.3 % 115.15/16.51 % (1663563)Termination reason: Inappropriate % 115.15/16.51 % (1663563)Time elapsed: 0.0000 s % 115.15/16.51 % (1663563)Peak memory usage: 10 MB % 115.15/16.51 % (1663563)Instructions burned: 2 (million) % 115.15/16.51 % (1663563)------------------------------ % 115.15/16.51 % (1663563)------------------------------ % 115.15/16.51 % (1663562)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3874080124:fmbsr=2:i=46332_2968 on theBenchmark for (2968ds/46332Mi) % 115.15/16.52 % (1663562)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 115.15/16.52 % (1663562)Terminated due to inappropriate strategy. % 115.15/16.52 % (1663562)------------------------------ % 115.15/16.52 % (1663562)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 115.15/16.52 % (1663562)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 115.15/16.52 % (1663562)CaDiCaL version: 2.1.3 % 115.15/16.52 % (1663562)Termination reason: Inappropriate % 115.15/16.52 % (1663562)Time elapsed: 0.001 s % 115.15/16.52 % (1663562)Peak memory usage: 10 MB % 115.15/16.52 % (1663562)Instructions burned: 2 (million) % 115.15/16.52 % (1663562)------------------------------ % 115.15/16.52 % (1663562)------------------------------ % 115.15/16.52 % (1663565)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2250425985:i=22565:add=on:rawr=on_2968 on theBenchmark for (2968ds/22565Mi) % 115.15/16.52 % (1663567)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=2163694960:i=8173:av=off_2968 on theBenchmark for (2968ds/8173Mi) % 115.15/16.52 % (1663542)Instruction limit reached! % 115.75/16.62 % (1663542)------------------------------ % 115.75/16.62 % (1663542)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 115.75/16.62 % (1663542)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 115.75/16.62 % (1663542)CaDiCaL version: 2.1.3 % 115.75/16.62 % (1663542)Termination reason: Instruction limit % 115.75/16.62 % (1663542)Termination phase: Saturation % 115.75/16.62 % (1663542)Time elapsed: 3.141 s % 115.75/16.62 % (1663542)Peak memory usage: 36 MB % 115.75/16.62 % (1663542)Instructions burned: 5115 (million) % 115.75/16.62 % (1663571)dis+10_16:1_sil=16000:random_seed=549015847:i=9155:fsr=off_2961 on theBenchmark for (2961ds/9155Mi) % 115.75/16.62 % (1663558)Instruction limit reached! % 115.75/16.62 % (1663558)------------------------------ % 115.75/16.62 % (1663558)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 115.75/16.62 % (1663558)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 115.75/16.62 % (1663558)CaDiCaL version: 2.1.3 % 115.75/16.62 % (1663558)Termination reason: Instruction limit % 115.75/16.62 % (1663558)Termination phase: Saturation % 115.75/16.62 % (1663558)Time elapsed: 2.714 s % 115.75/16.62 % (1663558)Peak memory usage: 49 MB % 115.75/16.62 % (1663558)Instructions burned: 5213 (million) % 115.75/16.62 % (1663573)ott-3_8_sil=64000:random_seed=1592661325:i=20139:bs=on_2945 on theBenchmark for (2945ds/20139Mi) % 115.75/16.62 % (1663565)Instruction limit reached! % 115.75/16.62 % (1663565)------------------------------ % 115.75/16.62 % (1663565)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 115.75/16.62 % (1663565)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 115.75/16.62 % (1663565)CaDiCaL version: 2.1.3 % 115.75/16.62 % (1663565)Termination reason: Instruction limit % 115.75/16.62 % (1663565)Termination phase: Saturation % 115.75/16.62 % (1663565)Time elapsed: 4.811 s % 115.75/16.62 % (1663565)Peak memory usage: 59 MB % 115.75/16.62 % (1663565)Instructions burned: 22566 (million) % 115.75/16.62 % (1663918)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=1400416810:fmbsr=2:i=32576_2920 on theBenchmark for (2920ds/32576Mi) % 115.75/16.62 % (1663918)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 115.75/16.62 % (1663918)Terminated due to inappropriate strategy. % 115.75/16.62 % (1663918)------------------------------ % 115.75/16.62 % (1663918)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 115.75/16.62 % (1663918)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 115.75/16.62 % (1663918)CaDiCaL version: 2.1.3 % 115.75/16.62 % (1663918)Termination reason: Inappropriate % 115.75/16.62 % (1663918)Time elapsed: 0.001 s % 115.75/16.62 % (1663918)Peak memory usage: 10 MB % 115.75/16.62 % (1663918)Instructions burned: 2 (million) % 115.75/16.62 % (1663918)------------------------------ % 115.75/16.62 % (1663918)------------------------------ % 115.75/16.62 % (1663920)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=764793785:i=11404_2920 on theBenchmark for (2920ds/11404Mi) % 115.75/16.62 % (1663567)Instruction limit reached! % 115.75/16.62 % (1663567)------------------------------ % 115.75/16.62 % (1663567)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 115.75/16.62 % (1663567)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 115.75/16.62 % (1663567)CaDiCaL version: 2.1.3 % 115.75/16.62 % (1663567)Termination reason: Instruction limit % 115.75/16.62 % (1663567)Termination phase: Saturation % 115.75/16.62 % (1663567)Time elapsed: 5.045 s % 115.75/16.62 % (1663567)Peak memory usage: 56 MB % 115.75/16.62 % (1663567)Instructions burned: 8174 (million) % 115.75/16.62 % (1663922)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=783833563:i=14134_2917 on theBenchmark for (2917ds/14134Mi) % 115.75/16.62 % (1663571)Instruction limit reached! % 115.75/16.62 % (1663571)------------------------------ % 115.75/16.62 % (1663571)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 115.75/16.62 % (1663571)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 115.75/16.62 % (1663571)CaDiCaL version: 2.1.3 % 115.75/16.62 % (1663571)Termination reason: Instruction limit % 115.75/16.62 % (1663571)Termination phase: Saturation % 115.75/16.62 % (1663571)Time elapsed: 4.632 s % 115.75/16.62 % (1663571)Peak memory usage: 52 MB % 115.75/16.62 % (1663571)Instructions burned: 9157 (million) % 115.75/16.62 % (1663924)dis+33_16_sil=32000:sac=on:random_seed=1624805248:i=15851:nm=0_2914 on theBenchmark for (2914ds/15851Mi) % 115.75/16.62 % (1663920)Instruction limit reached! % 115.75/16.62 % (1663920)------------------------------ % 115.75/16.62 % (1663920)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 124.57/17.83 % (1663920)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.57/17.83 % (1663920)CaDiCaL version: 2.1.3 % 124.57/17.83 % (1663920)Termination reason: Instruction limit % 124.57/17.83 % (1663920)Termination phase: Saturation % 124.57/17.83 % (1663920)Time elapsed: 3.805 s % 124.57/17.83 % (1663920)Peak memory usage: 61 MB % 124.57/17.83 % (1663920)Instructions burned: 11406 (million) % 124.57/17.83 % (1663926)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=543034389:avsq=on:i=17627:add=on:amm=off_2881 on theBenchmark for (2881ds/17627Mi) % 124.57/17.83 % (1663556)Instruction limit reached! % 124.57/17.83 % (1663556)------------------------------ % 124.57/17.83 % (1663556)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 124.57/17.83 % (1663556)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.57/17.83 % (1663556)CaDiCaL version: 2.1.3 % 124.57/17.83 % (1663556)Termination reason: Instruction limit % 124.57/17.83 % (1663556)Termination phase: Saturation % 124.57/17.83 % (1663556)Time elapsed: 12.545 s % 124.57/17.83 % (1663556)Peak memory usage: 124 MB % 124.57/17.83 % (1663556)Instructions burned: 29342 (million) % 124.57/17.83 % (1663928)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=2395536429:s2a=on:i=53295_2848 on theBenchmark for (2848ds/53295Mi) % 124.57/17.83 % (1663924)Instruction limit reached! % 124.57/17.83 % (1663924)------------------------------ % 124.57/17.83 % (1663924)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 124.57/17.83 % (1663924)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.57/17.83 % (1663924)CaDiCaL version: 2.1.3 % 124.57/17.83 % (1663924)Termination reason: Instruction limit % 124.57/17.83 % (1663924)Termination phase: Saturation % 124.57/17.83 % (1663924)Time elapsed: 7.256 s % 124.57/17.83 % (1663924)Peak memory usage: 138 MB % 124.57/17.83 % (1663924)Instructions burned: 15851 (million) % 124.57/17.83 % (1663930)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=1496530490:i=26857:ins=20_2841 on theBenchmark for (2841ds/26857Mi) % 124.57/17.83 % (1663930)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 124.57/17.83 % (1663930)Terminated due to inappropriate strategy. % 124.57/17.83 % (1663930)------------------------------ % 124.57/17.83 % (1663930)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 124.57/17.83 % (1663930)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.57/17.83 % (1663930)CaDiCaL version: 2.1.3 % 124.57/17.83 % (1663930)Termination reason: Inappropriate % 124.57/17.83 % (1663930)Time elapsed: 0.001 s % 124.57/17.83 % (1663930)Peak memory usage: 10 MB % 124.57/17.83 % (1663930)Instructions burned: 2 (million) % 124.57/17.83 % (1663930)------------------------------ % 124.57/17.83 % (1663930)------------------------------ % 124.57/17.83 % (1663932)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=3751098773:i=28120:bs=on:fsr=off_2841 on theBenchmark for (2841ds/28120Mi) % 124.57/17.83 % (1663573)Instruction limit reached! % 124.57/17.83 % (1663573)------------------------------ % 124.57/17.83 % (1663573)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 124.57/17.83 % (1663573)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.57/17.83 % (1663573)CaDiCaL version: 2.1.3 % 124.57/17.83 % (1663573)Termination reason: Instruction limit % 124.57/17.83 % (1663573)Termination phase: Saturation % 124.57/17.83 % (1663573)Time elapsed: 10.777 s % 124.57/17.83 % (1663573)Peak memory usage: 72 MB % 124.57/17.83 % (1663573)Instructions burned: 20141 (million) % 124.57/17.83 % (1663934)fmb+10_1_sil=256000:fmbss=7:random_seed=2642162350:fmbsr=1.6:i=182295_2837 on theBenchmark for (2837ds/182295Mi) % 124.57/17.83 % (1663934)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 124.57/17.83 % (1663934)Terminated due to inappropriate strategy. % 124.57/17.83 % (1663934)------------------------------ % 124.57/17.83 % (1663934)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 124.57/17.83 % (1663934)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.57/17.83 % (1663934)CaDiCaL version: 2.1.3 % 124.57/17.83 % (1663934)Termination reason: Inappropriate % 124.57/17.83 % (1663934)Time elapsed: 0.001 s % 124.57/17.83 % (1663934)Peak memory usage: 10 MB % 124.57/17.83 % (1663934)Instructions burned: 2 (million) % 124.57/17.83 % (1663934)------------------------------ % 124.57/17.83 % (1663934)------------------------------ % 124.57/17.83 % (1663936)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=1916113617:i=44625:gsp=on_2837 on theBenchmark for (2837ds/44625Mi) % 137.57/19.66 % (1663936)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 137.57/19.66 % (1663936)Terminated due to inappropriate strategy. % 137.57/19.66 % (1663936)------------------------------ % 137.57/19.66 % (1663936)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 137.57/19.66 % (1663936)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 137.57/19.66 % (1663936)CaDiCaL version: 2.1.3 % 137.57/19.66 % (1663936)Termination reason: Inappropriate % 137.57/19.66 % (1663936)Time elapsed: 0.001 s % 137.57/19.66 % (1663936)Peak memory usage: 11 MB % 137.57/19.66 % (1663936)Instructions burned: 2 (million) % 137.57/19.66 % (1663936)------------------------------ % 137.57/19.66 % (1663936)------------------------------ % 137.57/19.66 % (1663938)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=2378585843:i=160505_2836 on theBenchmark for (2836ds/160505Mi) % 137.57/19.66 % (1663938)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 137.57/19.66 % (1663938)Terminated due to inappropriate strategy. % 137.57/19.66 % (1663938)------------------------------ % 137.57/19.66 % (1663938)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 137.57/19.66 % (1663938)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 137.57/19.66 % (1663938)CaDiCaL version: 2.1.3 % 137.57/19.66 % (1663938)Termination reason: Inappropriate % 137.57/19.66 % (1663938)Time elapsed: 0.001 s % 137.57/19.66 % (1663938)Peak memory usage: 10 MB % 137.57/19.66 % (1663938)Instructions burned: 2 (million) % 137.57/19.66 % (1663938)------------------------------ % 137.57/19.66 % (1663938)------------------------------ % 137.57/19.66 % (1663940)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=1603794094:fmbsr=1.3:i=225729_2836 on theBenchmark for (2836ds/225729Mi) % 137.57/19.66 % (1663940)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 137.57/19.66 % (1663940)Terminated due to inappropriate strategy. % 137.57/19.66 % (1663940)------------------------------ % 137.57/19.66 % (1663940)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 137.57/19.66 % (1663940)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 137.57/19.66 % (1663940)CaDiCaL version: 2.1.3 % 137.57/19.66 % (1663940)Termination reason: Inappropriate % 137.57/19.66 % (1663940)Time elapsed: 0.001 s % 137.57/19.66 % (1663940)Peak memory usage: 11 MB % 137.57/19.66 % (1663940)Instructions burned: 2 (million) % 137.57/19.66 % (1663940)------------------------------ % 137.57/19.66 % (1663940)------------------------------ % 137.57/19.66 % (1663942)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=1269869861:fmbsr=2:i=185024:ins=7_2836 on theBenchmark for (2836ds/185024Mi) % 137.57/19.66 % (1663942)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 137.57/19.66 % (1663942)Terminated due to inappropriate strategy. % 137.57/19.66 % (1663942)------------------------------ % 137.57/19.66 % (1663942)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 137.57/19.66 % (1663942)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 137.57/19.66 % (1663942)CaDiCaL version: 2.1.3 % 137.57/19.66 % (1663942)Termination reason: Inappropriate % 137.57/19.66 % (1663942)Time elapsed: 0.001 s % 137.57/19.66 % (1663942)Peak memory usage: 11 MB % 137.57/19.66 % (1663942)Instructions burned: 2 (million) % 137.57/19.66 % (1663942)------------------------------ % 137.57/19.66 % (1663942)------------------------------ % 137.57/19.66 % (1663944)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=3578210457:rtra=on_2836 on theBenchmark for (2836ds/0Mi) % 137.57/19.66 % (1663944)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 137.57/19.66 % (1663944)Terminated due to inappropriate strategy. % 137.57/19.66 % (1663944)------------------------------ % 137.57/19.66 % (1663944)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 137.57/19.66 % (1663944)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 137.57/19.66 % (1663944)CaDiCaL version: 2.1.3 % 137.57/19.66 % (1663944)Termination reason: Inappropriate % 137.57/19.66 % (1663944)Time elapsed: 0.001 s % 137.57/19.66 % (1663944)Peak memory usage: 10 MB % 137.57/19.66 % (1663944)Instructions burned: 2 (million) % 137.57/19.66 % (1663944)------------------------------ % 137.57/19.66 % (1663944)------------------------------ % 137.57/19.66 % (1663946)% WARNING: option uhcvi not known. % 137.57/19.66 % (1663946)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1836093565:i=271062:add=off:rtra=on:rawr=on_2836 on theBenchmark for (2836ds/271062Mi) % 158.86/22.69 % (1663926)Instruction limit reached! % 158.86/22.69 % (1663926)------------------------------ % 158.86/22.69 % (1663926)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.86/22.69 % (1663926)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.86/22.69 % (1663926)CaDiCaL version: 2.1.3 % 158.86/22.69 % (1663926)Termination reason: Instruction limit % 158.86/22.69 % (1663926)Termination phase: Saturation % 158.86/22.69 % (1663926)Time elapsed: 4.890 s % 158.86/22.69 % (1663926)Peak memory usage: 131 MB % 158.86/22.69 % (1663926)Instructions burned: 17627 (million) % 158.86/22.69 % (1663948)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3084638377:i=176048:add=on:rtra=on:rawr=on_2832 on theBenchmark for (2832ds/176048Mi) % 158.86/22.69 % (1663922)Instruction limit reached! % 158.86/22.69 % (1663922)------------------------------ % 158.86/22.69 % (1663922)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.86/22.69 % (1663922)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.86/22.69 % (1663922)CaDiCaL version: 2.1.3 % 158.86/22.69 % (1663922)Termination reason: Instruction limit % 158.86/22.69 % (1663922)Termination phase: Saturation % 158.86/22.69 % (1663922)Time elapsed: 8.633 s % 158.86/22.69 % (1663922)Peak memory usage: 78 MB % 158.86/22.69 % (1663922)Instructions burned: 14135 (million) % 158.86/22.69 % (1663950)dis+10_1_sil=32000:si=on:sp=arity:random_seed=557447923:i=206:fgj=on:rtra=on_2831 on theBenchmark for (2831ds/206Mi) % 158.86/22.69 % (1663950)Instruction limit reached! % 158.86/22.69 % (1663950)------------------------------ % 158.86/22.69 % (1663950)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.86/22.69 % (1663950)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.86/22.69 % (1663950)CaDiCaL version: 2.1.3 % 158.86/22.69 % (1663950)Termination reason: Instruction limit % 158.86/22.69 % (1663950)Termination phase: Saturation % 158.86/22.69 % (1663950)Time elapsed: 0.121 s % 158.86/22.69 % (1663950)Peak memory usage: 13 MB % 158.86/22.69 % (1663950)Instructions burned: 206 (million) % 158.86/22.69 % (1663952)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=2657075563:i=232:rtra=on_2829 on theBenchmark for (2829ds/232Mi) % 158.86/22.69 % (1663952)Instruction limit reached! % 158.86/22.69 % (1663952)------------------------------ % 158.86/22.69 % (1663952)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.86/22.69 % (1663952)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.86/22.69 % (1663952)CaDiCaL version: 2.1.3 % 158.86/22.69 % (1663952)Termination reason: Instruction limit % 158.86/22.69 % (1663952)Termination phase: Saturation % 158.86/22.69 % (1663952)Time elapsed: 0.145 s % 158.86/22.69 % (1663952)Peak memory usage: 13 MB % 158.86/22.69 % (1663952)Instructions burned: 233 (million) % 158.86/22.69 % (1663954)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=2460000767:i=262:rtra=on_2828 on theBenchmark for (2828ds/262Mi) % 158.86/22.69 % (1663954)Instruction limit reached! % 158.86/22.69 % (1663954)------------------------------ % 158.86/22.69 % (1663954)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.86/22.69 % (1663954)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.86/22.69 % (1663954)CaDiCaL version: 2.1.3 % 158.86/22.69 % (1663954)Termination reason: Instruction limit % 158.86/22.69 % (1663954)Termination phase: Saturation % 158.86/22.69 % (1663954)Time elapsed: 0.149 s % 158.86/22.69 % (1663954)Peak memory usage: 14 MB % 158.86/22.69 % (1663954)Instructions burned: 263 (million) % 158.86/22.69 % (1663956)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=63068556:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2826 on theBenchmark for (2826ds/318Mi) % 158.86/22.69 % (1663956)Instruction limit reached! % 158.86/22.69 % (1663956)------------------------------ % 158.86/22.69 % (1663956)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.86/22.69 % (1663956)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.86/22.69 % (1663956)CaDiCaL version: 2.1.3 % 158.86/22.69 % (1663956)Termination reason: Instruction limit % 158.86/22.69 % (1663956)Termination phase: Saturation % 158.86/22.69 % (1663956)Time elapsed: 0.215 s % 158.86/22.69 % (1663956)Peak memory usage: 15 MB % 158.86/22.69 % (1663956)Instructions burned: 319 (million) % 158.86/22.69 % (1663958)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=2435189729:i=1428:nm=2:rtra=on_2824 on theBenchmark for (2824ds/1428Mi) % 202.81/28.83 % (1663958)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 202.81/28.83 % (1663958)Terminated due to inappropriate strategy. % 202.81/28.83 % (1663958)------------------------------ % 202.81/28.83 % (1663958)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 202.81/28.83 % (1663958)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.81/28.83 % (1663958)CaDiCaL version: 2.1.3 % 202.81/28.83 % (1663958)Termination reason: Inappropriate % 202.81/28.83 % (1663958)Time elapsed: 0.001 s % 202.81/28.83 % (1663958)Peak memory usage: 10 MB % 202.81/28.83 % (1663958)Instructions burned: 2 (million) % 202.81/28.83 % (1663958)------------------------------ % 202.81/28.83 % (1663958)------------------------------ % 202.81/28.83 % (1663960)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=3980325746:i=262:bd=preordered:rtra=on:fsd=on_2823 on theBenchmark for (2823ds/262Mi) % 202.81/28.83 % (1663960)Instruction limit reached! % 202.81/28.83 % (1663960)------------------------------ % 202.81/28.83 % (1663960)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 202.81/28.83 % (1663960)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.81/28.83 % (1663960)CaDiCaL version: 2.1.3 % 202.81/28.83 % (1663960)Termination reason: Instruction limit % 202.81/28.83 % (1663960)Termination phase: Saturation % 202.81/28.83 % (1663960)Time elapsed: 0.153 s % 202.81/28.83 % (1663960)Peak memory usage: 13 MB % 202.81/28.83 % (1663960)Instructions burned: 262 (million) % 202.81/28.83 % (1663962)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=2429166560:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2822 on theBenchmark for (2822ds/1368Mi) % 202.81/28.83 % (1663962)Instruction limit reached! % 202.81/28.83 % (1663962)------------------------------ % 202.81/28.83 % (1663962)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 202.81/28.83 % (1663962)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.81/28.83 % (1663962)CaDiCaL version: 2.1.3 % 202.81/28.83 % (1663962)Termination reason: Instruction limit % 202.81/28.83 % (1663962)Termination phase: Saturation % 202.81/28.83 % (1663962)Time elapsed: 0.777 s % 202.81/28.83 % (1663962)Peak memory usage: 23 MB % 202.81/28.83 % (1663962)Instructions burned: 1372 (million) % 202.81/28.83 % (1663964)ott-21_1_sil=16000:si=on:fs=off:random_seed=1158388690:i=360:av=off:fsr=off:rtra=on_2814 on theBenchmark for (2814ds/360Mi) % 202.81/28.83 % (1663964)Instruction limit reached! % 202.81/28.83 % (1663964)------------------------------ % 202.81/28.83 % (1663964)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 202.81/28.83 % (1663964)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.81/28.83 % (1663964)CaDiCaL version: 2.1.3 % 202.81/28.83 % (1663964)Termination reason: Instruction limit % 202.81/28.83 % (1663964)Termination phase: Saturation % 202.81/28.83 % (1663964)Time elapsed: 0.158 s % 202.81/28.83 % (1663964)Peak memory usage: 13 MB % 202.81/28.83 % (1663964)Instructions burned: 362 (million) % 202.81/28.83 % (1663966)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3784982607:i=954:bd=all:rtra=on_2812 on theBenchmark for (2812ds/954Mi) % 202.81/28.83 % (1663966)Instruction limit reached! % 202.81/28.83 % (1663966)------------------------------ % 202.81/28.83 % (1663966)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 202.81/28.83 % (1663966)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.81/28.83 % (1663966)CaDiCaL version: 2.1.3 % 202.81/28.83 % (1663966)Termination reason: Instruction limit % 202.81/28.83 % (1663966)Termination phase: Saturation % 202.81/28.83 % (1663966)Time elapsed: 0.635 s % 202.81/28.83 % (1663966)Peak memory usage: 17 MB % 202.81/28.83 % (1663966)Instructions burned: 955 (million) % 202.81/28.83 % (1663968)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=2238878039:fmbsr=1.3:i=1730:ins=25:rtra=on_2805 on theBenchmark for (2805ds/1730Mi) % 202.81/28.83 % (1663968)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 202.81/28.83 % (1663968)Terminated due to inappropriate strategy. % 202.81/28.83 % (1663968)------------------------------ % 202.81/28.83 % (1663968)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 202.81/28.83 % (1663968)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.81/28.83 % (1663968)CaDiCaL version: 2.1.3 % 202.81/28.83 % (1663968)Termination reason: Inappropriate % 262.53/37.27 % (1663968)Time elapsed: 0.001 s % 262.53/37.27 % (1663968)Peak memory usage: 10 MB % 262.53/37.27 % (1663968)Instructions burned: 2 (million) % 262.53/37.27 % (1663968)------------------------------ % 262.53/37.27 % (1663968)------------------------------ % 262.53/37.27 % (1663970)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=1968682249:i=2358:rtra=on_2805 on theBenchmark for (2805ds/2358Mi) % 262.53/37.27 % (1663970)Instruction limit reached! % 262.53/37.27 % (1663970)------------------------------ % 262.53/37.27 % (1663970)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 262.53/37.27 % (1663970)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 262.53/37.27 % (1663970)CaDiCaL version: 2.1.3 % 262.53/37.27 % (1663970)Termination reason: Instruction limit % 262.53/37.27 % (1663970)Termination phase: Saturation % 262.53/37.27 % (1663970)Time elapsed: 1.187 s % 262.53/37.27 % (1663970)Peak memory usage: 23 MB % 262.53/37.27 % (1663970)Instructions burned: 2360 (million) % 262.53/37.27 % (1663972)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=3225855267:i=1778:ins=1:rtra=on_2793 on theBenchmark for (2793ds/1778Mi) % 262.53/37.27 % (1663972)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 262.53/37.27 % (1663972)Terminated due to inappropriate strategy. % 262.53/37.27 % (1663972)------------------------------ % 262.53/37.27 % (1663972)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 262.53/37.27 % (1663972)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 262.53/37.27 % (1663972)CaDiCaL version: 2.1.3 % 262.53/37.27 % (1663972)Termination reason: Inappropriate % 262.53/37.27 % (1663972)Time elapsed: 0.001 s % 262.53/37.27 % (1663972)Peak memory usage: 10 MB % 262.53/37.27 % (1663972)Instructions burned: 2 (million) % 262.53/37.27 % (1663972)------------------------------ % 262.53/37.27 % (1663972)------------------------------ % 262.53/37.27 % (1663974)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=305414867:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2793 on theBenchmark for (2793ds/1384Mi) % 262.53/37.27 % (1663974)Instruction limit reached! % 262.53/37.27 % (1663974)------------------------------ % 262.53/37.27 % (1663974)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 262.53/37.27 % (1663974)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 262.53/37.27 % (1663974)CaDiCaL version: 2.1.3 % 262.53/37.27 % (1663974)Termination reason: Instruction limit % 262.53/37.27 % (1663974)Termination phase: Saturation % 262.53/37.27 % (1663974)Time elapsed: 0.716 s % 262.53/37.27 % (1663974)Peak memory usage: 18 MB % 262.53/37.27 % (1663974)Instructions burned: 1385 (million) % 262.53/37.27 % (1664054)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=3237513860:i=1758:kws=inv_precedence:fsr=off:rtra=on_2785 on theBenchmark for (2785ds/1758Mi) % 262.53/37.27 % (1664054)Instruction limit reached! % 262.53/37.27 % (1664054)------------------------------ % 262.53/37.27 % (1664054)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 262.53/37.27 % (1664054)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 262.53/37.27 % (1664054)CaDiCaL version: 2.1.3 % 262.53/37.27 % (1664054)Termination reason: Instruction limit % 262.53/37.27 % (1664054)Termination phase: Saturation % 262.53/37.27 % (1664054)Time elapsed: 1.004 s % 262.53/37.27 % (1664054)Peak memory usage: 25 MB % 262.53/37.27 % (1664054)Instructions burned: 1759 (million) % 262.53/37.27 % (1664317)fmb+10_1_sil=64000:si=on:random_seed=1653815628:i=44122:nm=2:rtra=on:gsp=on_2775 on theBenchmark for (2775ds/44122Mi) % 262.53/37.27 % (1664317)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 262.53/37.27 % (1664317)Terminated due to inappropriate strategy. % 262.53/37.27 % (1664317)------------------------------ % 262.53/37.27 % (1664317)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 262.53/37.27 % (1664317)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 262.53/37.27 % (1664317)CaDiCaL version: 2.1.3 % 262.53/37.27 % (1664317)Termination reason: Inappropriate % 262.53/37.27 % (1664317)Time elapsed: 0.001 s % 262.53/37.27 % (1664317)Peak memory usage: 10 MB % 262.53/37.27 % (1664317)Instructions burned: 2 (million) % 262.53/37.27 % (1664317)------------------------------ % 262.53/37.27 % (1664317)------------------------------ % 262.53/37.27 % (1664323)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=4046532389:i=19030:nm=5:rtra=on_2775 on theBenchmark for (2775ds/19030Mi) % 280.75/39.92 % (1664323)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 280.75/39.92 % (1664323)Terminated due to inappropriate strategy. % 280.75/39.92 % (1664323)------------------------------ % 280.75/39.92 % (1664323)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 280.75/39.92 % (1664323)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 280.75/39.92 % (1664323)CaDiCaL version: 2.1.3 % 280.75/39.92 % (1664323)Termination reason: Inappropriate % 280.75/39.92 % (1664323)Time elapsed: 0.001 s % 280.75/39.92 % (1664323)Peak memory usage: 10 MB % 280.75/39.92 % (1664323)Instructions burned: 2 (million) % 280.75/39.92 % (1664323)------------------------------ % 280.75/39.92 % (1664323)------------------------------ % 280.75/39.92 % (1664325)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=3573593634:fmbsr=1.7:i=1840:rtra=on_2775 on theBenchmark for (2775ds/1840Mi) % 280.75/39.92 % (1664325)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 280.75/39.92 % (1664325)Terminated due to inappropriate strategy. % 280.75/39.92 % (1664325)------------------------------ % 280.75/39.92 % (1664325)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 280.75/39.92 % (1664325)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 280.75/39.92 % (1664325)CaDiCaL version: 2.1.3 % 280.75/39.92 % (1664325)Termination reason: Inappropriate % 280.75/39.92 % (1664325)Time elapsed: 0.001 s % 280.75/39.92 % (1664325)Peak memory usage: 10 MB % 280.75/39.92 % (1664325)Instructions burned: 2 (million) % 280.75/39.92 % (1664325)------------------------------ % 280.75/39.92 % (1664325)------------------------------ % 280.75/39.92 % (1664327)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=2995976243:i=10262:rtra=on_2774 on theBenchmark for (2774ds/10262Mi) % 280.75/39.92 % (1663932)Instruction limit reached! % 280.75/39.92 % (1663932)------------------------------ % 280.75/39.92 % (1663932)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 280.75/39.92 % (1663932)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 280.75/39.92 % (1663932)CaDiCaL version: 2.1.3 % 280.75/39.92 % (1663932)Termination reason: Instruction limit % 280.75/39.92 % (1663932)Termination phase: Saturation % 280.75/39.92 % (1663932)Time elapsed: 12.613 s % 280.75/39.92 % (1663932)Peak memory usage: 32 MB % 280.75/39.92 % (1663932)Instructions burned: 28122 (million) % 280.75/39.92 % (1664330)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2047896284:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2715 on theBenchmark for (2715ds/2944Mi) % 280.75/39.92 % (1664327)Instruction limit reached! % 280.75/39.92 % (1664327)------------------------------ % 280.75/39.92 % (1664327)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 280.75/39.92 % (1664327)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 280.75/39.92 % (1664327)CaDiCaL version: 2.1.3 % 280.75/39.92 % (1664327)Termination reason: Instruction limit % 280.75/39.92 % (1664327)Termination phase: Saturation % 280.75/39.92 % (1664327)Time elapsed: 6.041 s % 280.75/39.92 % (1664327)Peak memory usage: 68 MB % 280.75/39.92 % (1664327)Instructions burned: 10262 (million) % 280.75/39.92 % (1664332)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=2587750426:i=12648:rtra=on_2714 on theBenchmark for (2714ds/12648Mi) % 280.75/39.92 % (1664332)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 280.75/39.92 % (1664332)Terminated due to inappropriate strategy. % 280.75/39.92 % (1664332)------------------------------ % 280.75/39.92 % (1664332)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 280.75/39.92 % (1664332)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 280.75/39.92 % (1664332)CaDiCaL version: 2.1.3 % 280.75/39.92 % (1664332)Termination reason: Inappropriate % 280.75/39.92 % (1664332)Time elapsed: 0.001 s % 280.75/39.92 % (1664332)Peak memory usage: 10 MB % 280.75/39.92 % (1664332)Instructions burned: 2 (million) % 280.75/39.92 % (1664332)------------------------------ % 280.75/39.92 % (1664332)------------------------------ % 280.75/39.92 % (1664334)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=1203045779:fmbsr=2.30978:i=4348:rtra=on_2714 on theBenchmark for (2714ds/4348Mi) % 280.75/39.92 % (1664334)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 280.75/39.92 % (1664334)Terminated due to inappropriate strategy. % 280.75/39.92 % (1664334)------------------------------ % 280.75/39.92 % (1664334)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.11/42.53 % (1664334)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.11/42.53 % (1664334)CaDiCaL version: 2.1.3 % 300.11/42.53 % (1664334)Termination reason: Inappropriate % 300.11/42.53 % (1664334)Time elapsed: 0.001 s % 300.11/42.53 % (1664334)Peak memory usage: 10 MB % 300.11/42.53 % (1664334)Instructions burned: 2 (million) % 300.11/42.53 % (1664334)------------------------------ % 300.11/42.53 % (1664334)------------------------------ % 300.11/42.53 % (1664336)ott-2_1_sil=16000:si=on:newcnf=on:random_seed=2406980148:avsq=on:i=1738:avsqr=1,16:kws=inv_arity_squared:rtra=on_2713 on theBenchmark for (2713ds/1738Mi) % 300.11/42.53 % (1664336)Instruction limit reached! % 300.11/42.53 % (1664336)------------------------------ % 300.11/42.53 % (1664336)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.11/42.53 % (1664336)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.11/42.53 % (1664336)CaDiCaL version: 2.1.3 % 300.11/42.53 % (1664336)Termination reason: Instruction limit % 300.11/42.53 % (1664336)Termination phase: Saturation % 300.11/42.53 % (1664336)Time elapsed: 1.101 s % 300.11/42.53 % (1664336)Peak memory usage: 18 MB % 300.11/42.53 % (1664336)Instructions burned: 1739 (million) % 300.11/42.53 % (1664338)ott+10_1_sil=32000:tgt=ground:si=on:random_seed=2742864094:i=10228:av=off:rtra=on_2702 on theBenchmark for (2702ds/10228Mi) % 300.11/42.53 % (1664330)Instruction limit reached! % 300.11/42.53 % (1664330)------------------------------ % 300.11/42.53 % (1664330)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.11/42.53 % (1664330)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.11/42.53 % (1664330)CaDiCaL version: 2.1.3 % 300.11/42.53 % (1664330)Termination reason: Instruction limit % 300.11/42.53 % (1664330)Termination phase: Saturation % 300.11/42.53 % (1664330)Time elapsed: 1.834 s % 300.11/42.53 % (1664330)Peak memory usage: 32 MB % 300.11/42.53 % (1664330)Instructions burned: 2945 (million) % 300.11/42.53 % (1664340)fmb+10_1_sil=64000:sas=cadical:si=on:bce=on:rp=on:random_seed=661751733:i=108564:rtra=on_2696 on theBenchmark for (2696ds/108564Mi) % 300.11/42.53 % (1664340)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.11/42.53 % (1664340)Terminated due to inappropriate strategy. % 300.11/42.53 % (1664340)------------------------------ % 300.11/42.53 % (1664340)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.11/42.53 % (1664340)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.11/42.53 % (1664340)CaDiCaL version: 2.1.3 % 300.11/42.53 % (1664340)Termination reason: Inappropriate % 300.11/42.53 % (1664340)Time elapsed: 0.001 s % 300.11/42.53 % (1664340)Peak memory usage: 10 MB % 300.11/42.53 % (1664340)Instructions burned: 2 (million) % 300.11/42.53 % (1664340)------------------------------ % 300.11/42.53 % (1664340)------------------------------ % 300.11/42.53 % (1664342)dis-11_1_sil=16000:si=on:sp=reverse_frequency:alpa=true:random_seed=3512686880:i=7024:aac=none:rtra=on_2696 on theBenchmark for (2696ds/7024Mi) % 300.11/42.53 % (1664342)Instruction limit reached! % 300.11/42.53 % (1664342)------------------------------ % 300.11/42.53 % (1664342)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.11/42.53 % (1664342)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.11/42.53 % (1664342)CaDiCaL version: 2.1.3 % 300.11/42.53 % (1664342)Termination reason: Instruction limit % 300.11/42.53 % (1664342)Termination phase: Saturation % 300.11/42.53 % (1664342)Time elapsed: 4.075 s % 300.11/42.53 % (1664342)Peak memory usage: 48 MB % 300.11/42.53 % (1664342)Instructions burned: 7025 (million) % 300.11/42.53 % (1664344)dis+21_1_sil=32000:sas=cadical:si=on:random_seed=520000893:i=7546:rtra=on:amm=off_2655 on theBenchmark for (2655ds/7546Mi) % 300.11/42.53 % (1664338)Instruction limit reached! % 300.11/42.53 % (1664338)------------------------------ % 300.11/42.53 % (1664338)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.11/42.53 % (1664338)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.11/42.53 % (1664338)CaDiCaL version: 2.1.3 % 300.11/42.53 % (1664338)Termination reason: Instruction limit % 300.11/42.53 % (1664338)Termination phase: Saturation % 300.11/42.53 % (1664338)Time elapsed: 7.270 s % 300.11/42.53 % (1664338)Peak memory usage: 56 MB % 300.11/42.53 % (1664338)Instructions burned: 10228 (million) % 300.11/42.53 % (1664689)ott+11_1_sil=16000:si=on:gs=on:random_seed=3455047373:s2a=on:i=4502:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:rtra=on:fsd=on_2629 on theBenchm % 300.11/42.54 Terminated % 300.11/42.54 % Vampire exiting %------------------------------------------------------------------------------