%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW044_1 : TPTP v9.3.1. Released v5.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n015.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:38:40 PM UTC 2026 % Result : Timeout 300.53s 42.63s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWW044_1 : TPTP v9.3.1. Released v5.0.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.10/0.18 % Computer : n015.cluster.edu % 0.10/0.18 % Model : x86_64 x86_64 % 0.10/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.18 % Memory : 8046.5625MB % 0.10/0.18 % OS : Linux 6.8.0-71-generic % 0.10/0.18 % CPULimit : 300 % 0.10/0.18 % WCLimit : 300 % 0.10/0.18 % DateTime : Mon Sep 28 13:13:32 UTC 2026 % 0.10/0.18 % CPUTime : % 0.10/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.10/0.21 Running first-order model finding % 0.10/0.21 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 3.87/0.85 % (2616846)Will run a generic schedule for satisfiability detection. % 3.87/0.85 % (2616853)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3743644201:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 3.87/0.85 % (2616852)% WARNING: option uhcvi not known. % 3.87/0.85 % (2616851)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2054077636_2999 on theBenchmark for (2999ds/0Mi) % 3.87/0.85 % (2616852)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=76231964:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 3.87/0.85 % (2616854)dis+10_1_sil=32000:sp=arity:random_seed=3377440762:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 3.87/0.85 % (2616855)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3897100164:i=116_2999 on theBenchmark for (2999ds/116Mi) % 3.87/0.85 % (2616856)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2402043167:i=131_2999 on theBenchmark for (2999ds/131Mi) % 3.87/0.85 % (2616857)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3786697955:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 3.87/0.85 % (2616851)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.87/0.85 % (2616851)Terminated due to inappropriate strategy. % 3.87/0.85 % (2616851)------------------------------ % 3.87/0.85 % (2616851)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.87/0.85 % (2616851)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.87/0.85 % (2616851)CaDiCaL version: 2.1.3 % 3.87/0.85 % (2616851)Termination reason: Inappropriate % 3.87/0.85 % (2616851)Time elapsed: 0.036 s % 3.87/0.85 % (2616851)Peak memory usage: 13 MB % 3.87/0.85 % (2616851)Instructions burned: 83 (million) % 3.87/0.85 % (2616851)------------------------------ % 3.87/0.85 % (2616851)------------------------------ % 3.87/0.85 % (2616854)Instruction limit reached! % 3.87/0.85 % (2616854)------------------------------ % 3.87/0.85 % (2616854)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.87/0.85 % (2616854)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.87/0.85 % (2616854)CaDiCaL version: 2.1.3 % 3.87/0.85 % (2616854)Termination reason: Instruction limit % 3.87/0.85 % (2616854)Termination phase: Saturation % 3.87/0.85 % (2616854)Time elapsed: 0.046 s % 3.87/0.85 % (2616854)Peak memory usage: 14 MB % 3.87/0.85 % (2616854)Instructions burned: 104 (million) % 3.87/0.85 % (2616855)Instruction limit reached! % 3.87/0.85 % (2616855)------------------------------ % 3.87/0.85 % (2616855)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.87/0.85 % (2616856)Instruction limit reached! % 3.87/0.85 % (2616856)------------------------------ % 3.87/0.85 % (2616856)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.87/0.85 % (2616855)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.87/0.85 % (2616855)CaDiCaL version: 2.1.3 % 3.87/0.85 % (2616856)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.87/0.85 % (2616855)Termination reason: Instruction limit % 3.87/0.85 % (2616855)Termination phase: Saturation % 3.87/0.85 % (2616855)Time elapsed: 0.054 s % 3.87/0.85 % (2616855)Peak memory usage: 15 MB % 3.87/0.85 % (2616856)CaDiCaL version: 2.1.3 % 3.87/0.85 % (2616855)Instructions burned: 120 (million) % 3.87/0.85 % (2616856)Termination reason: Instruction limit % 3.87/0.85 % (2616856)Termination phase: Saturation % 3.87/0.85 % (2616856)Time elapsed: 0.054 s % 3.87/0.85 % (2616856)Peak memory usage: 14 MB % 3.87/0.85 % (2616856)Instructions burned: 133 (million) % 3.87/0.85 % (2616865)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1103686688:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 3.87/0.85 % (2616866)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1040570386:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi) % 3.87/0.85 % (2616857)Instruction limit reached! % 3.87/0.85 % (2616857)------------------------------ % 3.87/0.85 % (2616857)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.87/0.85 % (2616857)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.87/0.85 % (2616857)CaDiCaL version: 2.1.3 % 3.87/0.85 % (2616857)Termination reason: Instruction limit % 3.87/0.85 % (2616857)Termination phase: Saturation % 3.87/0.85 % (2616857)Time elapsed: 0.065 s % 3.87/0.85 % (2616857)Peak memory usage: 15 MB % 3.87/0.85 % (2616857)Instructions burned: 161 (million) % 5.60/1.07 % (2616867)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=2764795413:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 5.60/1.07 % (2616868)ott-21_1_sil=16000:fs=off:random_seed=806622313:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 5.60/1.07 % (2616871)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2623810201:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 5.60/1.07 % (2616865)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 5.60/1.07 % (2616865)Terminated due to inappropriate strategy. % 5.60/1.07 % (2616865)------------------------------ % 5.60/1.07 % (2616865)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.60/1.07 % (2616865)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.60/1.07 % (2616865)CaDiCaL version: 2.1.3 % 5.60/1.07 % (2616865)Termination reason: Inappropriate % 5.60/1.07 % (2616865)Time elapsed: 0.036 s % 5.60/1.07 % (2616865)Peak memory usage: 13 MB % 5.60/1.07 % (2616865)Instructions burned: 83 (million) % 5.60/1.07 % (2616865)------------------------------ % 5.60/1.07 % (2616865)------------------------------ % 5.60/1.07 % (2616875)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1629911768:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 5.60/1.07 % (2616866)Instruction limit reached! % 5.60/1.07 % (2616866)------------------------------ % 5.60/1.07 % (2616866)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.60/1.07 % (2616866)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.60/1.07 % (2616866)CaDiCaL version: 2.1.3 % 5.60/1.07 % (2616866)Termination reason: Instruction limit % 5.60/1.07 % (2616866)Termination phase: Saturation % 5.60/1.07 % (2616866)Time elapsed: 0.056 s % 5.60/1.07 % (2616866)Peak memory usage: 15 MB % 5.60/1.07 % (2616866)Instructions burned: 133 (million) % 5.60/1.07 % (2616877)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=4130596460:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 5.60/1.07 % (2616875)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 5.60/1.07 % (2616875)Terminated due to inappropriate strategy. % 5.60/1.07 % (2616875)------------------------------ % 5.60/1.07 % (2616875)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.60/1.07 % (2616875)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.60/1.07 % (2616875)CaDiCaL version: 2.1.3 % 5.60/1.07 % (2616875)Termination reason: Inappropriate % 5.60/1.07 % (2616875)Time elapsed: 0.035 s % 5.60/1.07 % (2616875)Peak memory usage: 14 MB % 5.60/1.07 % (2616875)Instructions burned: 82 (million) % 5.60/1.07 % (2616875)------------------------------ % 5.60/1.07 % (2616875)------------------------------ % 5.60/1.07 % (2616868)Instruction limit reached! % 5.60/1.07 % (2616868)------------------------------ % 5.60/1.07 % (2616868)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.60/1.07 % (2616868)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.60/1.07 % (2616868)CaDiCaL version: 2.1.3 % 5.60/1.07 % (2616868)Termination reason: Instruction limit % 5.60/1.07 % (2616868)Termination phase: Saturation % 5.60/1.07 % (2616868)Time elapsed: 0.083 s % 5.60/1.07 % (2616868)Peak memory usage: 15 MB % 5.60/1.07 % (2616868)Instructions burned: 181 (million) % 5.60/1.07 % (2616879)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1736199623:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi) % 5.60/1.07 % (2616880)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=2669213691:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2997 on theBenchmark for (2997ds/692Mi) % 5.60/1.07 % (2616879)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 5.60/1.07 % (2616879)Terminated due to inappropriate strategy. % 5.60/1.07 % (2616879)------------------------------ % 5.60/1.07 % (2616879)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.60/1.07 % (2616879)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.60/1.07 % (2616879)CaDiCaL version: 2.1.3 % 5.60/1.07 % (2616879)Termination reason: Inappropriate % 5.60/1.07 % (2616879)Time elapsed: 0.050 s % 5.60/1.07 % (2616879)Peak memory usage: 15 MB % 18.31/2.95 % (2616879)Instructions burned: 114 (million) % 18.31/2.95 % (2616879)------------------------------ % 18.31/2.95 % (2616879)------------------------------ % 18.31/2.95 % (2616883)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2294160152:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 18.31/2.95 % (2616871)Instruction limit reached! % 18.31/2.95 % (2616871)------------------------------ % 18.31/2.95 % (2616871)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.31/2.95 % (2616871)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.31/2.95 % (2616871)CaDiCaL version: 2.1.3 % 18.31/2.95 % (2616871)Termination reason: Instruction limit % 18.31/2.95 % (2616871)Termination phase: Saturation % 18.31/2.95 % (2616871)Time elapsed: 0.265 s % 18.31/2.95 % (2616871)Peak memory usage: 17 MB % 18.31/2.95 % (2616871)Instructions burned: 478 (million) % 18.31/2.95 % (2616885)fmb+10_1_sil=64000:random_seed=1163471458:i=22061:nm=2:gsp=on_2995 on theBenchmark for (2995ds/22061Mi) % 18.31/2.95 % (2616867)Instruction limit reached! % 18.31/2.95 % (2616867)------------------------------ % 18.31/2.95 % (2616867)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.31/2.95 % (2616867)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.31/2.95 % (2616867)CaDiCaL version: 2.1.3 % 18.31/2.95 % (2616867)Termination reason: Instruction limit % 18.31/2.95 % (2616867)Termination phase: Saturation % 18.31/2.95 % (2616867)Time elapsed: 0.323 s % 18.31/2.95 % (2616867)Peak memory usage: 19 MB % 18.31/2.95 % (2616867)Instructions burned: 685 (million) % 18.31/2.95 % (2616885)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 18.31/2.95 % (2616885)Terminated due to inappropriate strategy. % 18.31/2.95 % (2616885)------------------------------ % 18.31/2.95 % (2616885)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.31/2.95 % (2616885)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.31/2.95 % (2616885)CaDiCaL version: 2.1.3 % 18.31/2.95 % (2616885)Termination reason: Inappropriate % 18.31/2.95 % (2616885)Time elapsed: 0.040 s % 18.31/2.95 % (2616885)Peak memory usage: 13 MB % 18.31/2.95 % (2616885)Instructions burned: 91 (million) % 18.31/2.95 % (2616885)------------------------------ % 18.31/2.95 % (2616885)------------------------------ % 18.31/2.95 % (2616887)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=506088135:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi) % 18.31/2.95 % (2616888)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=222997783:fmbsr=1.7:i=920_2995 on theBenchmark for (2995ds/920Mi) % 18.31/2.95 % (2616887)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 18.31/2.95 % (2616887)Terminated due to inappropriate strategy. % 18.31/2.95 % (2616887)------------------------------ % 18.31/2.95 % (2616887)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.31/2.95 % (2616887)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.31/2.95 % (2616887)CaDiCaL version: 2.1.3 % 18.31/2.95 % (2616887)Termination reason: Inappropriate % 18.31/2.95 % (2616887)Time elapsed: 0.036 s % 18.31/2.95 % (2616887)Peak memory usage: 13 MB % 18.31/2.95 % (2616887)Instructions burned: 83 (million) % 18.31/2.95 % (2616887)------------------------------ % 18.31/2.95 % (2616887)------------------------------ % 18.31/2.95 % (2616888)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 18.31/2.95 % (2616888)Terminated due to inappropriate strategy. % 18.31/2.95 % (2616888)------------------------------ % 18.31/2.95 % (2616888)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.31/2.95 % (2616888)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.31/2.95 % (2616888)CaDiCaL version: 2.1.3 % 18.31/2.95 % (2616888)Termination reason: Inappropriate % 18.31/2.95 % (2616888)Time elapsed: 0.036 s % 18.31/2.95 % (2616888)Peak memory usage: 13 MB % 18.31/2.95 % (2616888)Instructions burned: 83 (million) % 18.31/2.95 % (2616888)------------------------------ % 18.31/2.95 % (2616888)------------------------------ % 18.31/2.95 % (2616891)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3390352462:i=5131_2994 on theBenchmark for (2994ds/5131Mi) % 18.31/2.95 % (2616892)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=161505149:i=1472:ins=7:fdi=8:gsp=on_2994 on theBenchmark for (2994ds/1472Mi) % 18.31/2.95 % (2616880)Instruction limit reached! % 18.31/2.95 % (2616880)------------------------------ % 25.68/4.02 % (2616880)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 25.68/4.02 % (2616880)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.68/4.02 % (2616880)CaDiCaL version: 2.1.3 % 25.68/4.02 % (2616880)Termination reason: Instruction limit % 25.68/4.02 % (2616880)Termination phase: Saturation % 25.68/4.02 % (2616880)Time elapsed: 0.399 s % 25.68/4.02 % (2616880)Peak memory usage: 22 MB % 25.68/4.02 % (2616880)Instructions burned: 692 (million) % 25.68/4.02 % (2616895)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1215134581:i=6324_2993 on theBenchmark for (2993ds/6324Mi) % 25.68/4.02 % (2616895)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 25.68/4.02 % (2616895)Terminated due to inappropriate strategy. % 25.68/4.02 % (2616895)------------------------------ % 25.68/4.02 % (2616895)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 25.68/4.02 % (2616895)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.68/4.02 % (2616895)CaDiCaL version: 2.1.3 % 25.68/4.02 % (2616895)Termination reason: Inappropriate % 25.68/4.02 % (2616895)Time elapsed: 0.035 s % 25.68/4.02 % (2616895)Peak memory usage: 13 MB % 25.68/4.02 % (2616895)Instructions burned: 83 (million) % 25.68/4.02 % (2616895)------------------------------ % 25.68/4.02 % (2616895)------------------------------ % 25.68/4.02 % (2616897)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=780627555:fmbsr=2.30978:i=2174_2993 on theBenchmark for (2993ds/2174Mi) % 25.68/4.02 % (2616897)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 25.68/4.02 % (2616897)Terminated due to inappropriate strategy. % 25.68/4.02 % (2616897)------------------------------ % 25.68/4.02 % (2616897)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 25.68/4.02 % (2616897)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.68/4.02 % (2616897)CaDiCaL version: 2.1.3 % 25.68/4.02 % (2616897)Termination reason: Inappropriate % 25.68/4.02 % (2616897)Time elapsed: 0.035 s % 25.68/4.02 % (2616897)Peak memory usage: 13 MB % 25.68/4.02 % (2616897)Instructions burned: 83 (million) % 25.68/4.02 % (2616897)------------------------------ % 25.68/4.02 % (2616897)------------------------------ % 25.68/4.02 % (2616899)ott-2_1_sil=16000:newcnf=on:random_seed=2222027656:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2992 on theBenchmark for (2992ds/869Mi) % 25.68/4.02 % (2616877)Instruction limit reached! % 25.68/4.02 % (2616877)------------------------------ % 25.68/4.02 % (2616877)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 25.68/4.02 % (2616877)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.68/4.02 % (2616877)CaDiCaL version: 2.1.3 % 25.68/4.02 % (2616877)Termination reason: Instruction limit % 25.68/4.02 % (2616877)Termination phase: Saturation % 25.68/4.02 % (2616877)Time elapsed: 0.568 s % 25.68/4.02 % (2616877)Peak memory usage: 19 MB % 25.68/4.02 % (2616877)Instructions burned: 1179 (million) % 25.68/4.02 % (2616901)ott+10_1_sil=32000:tgt=ground:random_seed=3079406969:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi) % 25.68/4.02 % (2616883)Instruction limit reached! % 25.68/4.02 % (2616883)------------------------------ % 25.68/4.02 % (2616883)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 25.68/4.02 % (2616883)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.68/4.02 % (2616883)CaDiCaL version: 2.1.3 % 25.68/4.02 % (2616883)Termination reason: Instruction limit % 25.68/4.02 % (2616883)Termination phase: Saturation % 25.68/4.02 % (2616883)Time elapsed: 0.489 s % 25.68/4.02 % (2616883)Peak memory usage: 21 MB % 25.68/4.02 % (2616883)Instructions burned: 879 (million) % 25.68/4.02 % (2616903)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=484569555:i=54282_2992 on theBenchmark for (2992ds/54282Mi) % 25.68/4.02 % (2616903)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 25.68/4.02 % (2616903)Terminated due to inappropriate strategy. % 25.68/4.02 % (2616903)------------------------------ % 25.68/4.02 % (2616903)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 25.68/4.02 % (2616903)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.68/4.02 % (2616903)CaDiCaL version: 2.1.3 % 25.68/4.02 % (2616903)Termination reason: Inappropriate % 25.68/4.02 % (2616903)Time elapsed: 0.036 s % 25.68/4.02 % (2616903)Peak memory usage: 13 MB % 25.68/4.02 % (2616903)Instructions burned: 83 (million) % 110.46/15.86 % (2616903)------------------------------ % 110.46/15.86 % (2616903)------------------------------ % 110.46/15.86 % (2616905)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1448957478:i=3512:aac=none_2991 on theBenchmark for (2991ds/3512Mi) % 110.46/15.86 % (2616892)Instruction limit reached! % 110.46/15.86 % (2616892)------------------------------ % 110.46/15.86 % (2616892)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 110.46/15.86 % (2616892)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 110.46/15.86 % (2616892)CaDiCaL version: 2.1.3 % 110.46/15.86 % (2616892)Termination reason: Instruction limit % 110.46/15.86 % (2616892)Termination phase: Saturation % 110.46/15.86 % (2616892)Time elapsed: 0.519 s % 110.46/15.86 % (2616892)Peak memory usage: 17 MB % 110.46/15.86 % (2616892)Instructions burned: 1473 (million) % 110.46/15.86 % (2616907)dis+21_1_sil=32000:sas=cadical:random_seed=1089627188:i=3773:amm=off_2989 on theBenchmark for (2989ds/3773Mi) % 110.46/15.86 % (2616899)Instruction limit reached! % 110.46/15.86 % (2616899)------------------------------ % 110.46/15.86 % (2616899)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 110.46/15.86 % (2616899)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 110.46/15.86 % (2616899)CaDiCaL version: 2.1.3 % 110.46/15.86 % (2616899)Termination reason: Instruction limit % 110.46/15.86 % (2616899)Termination phase: Saturation % 110.46/15.86 % (2616899)Time elapsed: 0.471 s % 110.46/15.86 % (2616899)Peak memory usage: 20 MB % 110.46/15.86 % (2616899)Instructions burned: 869 (million) % 110.46/15.86 % (2616909)ott+11_1_sil=16000:gs=on:random_seed=1610151861:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2987 on theBenchmark for (2987ds/2251Mi) % 110.46/15.86 % (2616909)Instruction limit reached! % 110.46/15.86 % (2616909)------------------------------ % 110.46/15.86 % (2616909)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 110.46/15.86 % (2616909)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 110.46/15.86 % (2616909)CaDiCaL version: 2.1.3 % 110.46/15.86 % (2616909)Termination reason: Instruction limit % 110.46/15.86 % (2616909)Termination phase: Saturation % 110.46/15.86 % (2616909)Time elapsed: 0.844 s % 110.46/15.86 % (2616909)Peak memory usage: 19 MB % 110.46/15.86 % (2616909)Instructions burned: 2251 (million) % 110.46/15.86 % (2616911)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3735087620:fmbsr=1.6:i=67534_2978 on theBenchmark for (2978ds/67534Mi) % 110.46/15.86 % (2616911)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 110.46/15.86 % (2616911)Terminated due to inappropriate strategy. % 110.46/15.86 % (2616911)------------------------------ % 110.46/15.86 % (2616911)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 110.46/15.86 % (2616911)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 110.46/15.86 % (2616911)CaDiCaL version: 2.1.3 % 110.46/15.86 % (2616911)Termination reason: Inappropriate % 110.46/15.86 % (2616911)Time elapsed: 0.046 s % 110.46/15.86 % (2616911)Peak memory usage: 14 MB % 110.46/15.86 % (2616911)Instructions burned: 112 (million) % 110.46/15.86 % (2616911)------------------------------ % 110.46/15.86 % (2616911)------------------------------ % 110.46/15.86 % (2616913)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3828212413:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2978 on theBenchmark for (2978ds/4591Mi) % 110.46/15.86 % (2616905)Instruction limit reached! % 110.46/15.86 % (2616905)------------------------------ % 110.46/15.86 % (2616905)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 110.46/15.86 % (2616905)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 110.46/15.86 % (2616905)CaDiCaL version: 2.1.3 % 110.46/15.86 % (2616905)Termination reason: Instruction limit % 110.46/15.86 % (2616905)Termination phase: Saturation % 110.46/15.86 % (2616905)Time elapsed: 1.747 s % 110.46/15.86 % (2616905)Peak memory usage: 30 MB % 110.46/15.86 % (2616905)Instructions burned: 3514 (million) % 110.46/15.86 % (2616915)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3254987598:i=29340_2973 on theBenchmark for (2973ds/29340Mi) % 110.46/15.86 % (2616907)Instruction limit reached! % 110.46/15.86 % (2616907)------------------------------ % 110.46/15.86 % (2616907)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 110.46/15.86 % (2616907)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 110.46/15.86 % (2616907)CaDiCaL version: 2.1.3 % 110.46/15.86 % (2616907)Termination reason: Instruction limit % 129.60/18.55 % (2616907)Termination phase: Saturation % 129.60/18.55 % (2616907)Time elapsed: 1.643 s % 129.60/18.55 % (2616907)Peak memory usage: 23 MB % 129.60/18.55 % (2616907)Instructions burned: 3773 (million) % 129.60/18.55 % (2616917)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=715578004:i=5211_2972 on theBenchmark for (2972ds/5211Mi) % 129.60/18.55 % (2616891)Instruction limit reached! % 129.60/18.55 % (2616891)------------------------------ % 129.60/18.55 % (2616891)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 129.60/18.55 % (2616891)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 129.60/18.55 % (2616891)CaDiCaL version: 2.1.3 % 129.60/18.55 % (2616891)Termination reason: Instruction limit % 129.60/18.55 % (2616891)Termination phase: Saturation % 129.60/18.55 % (2616891)Time elapsed: 2.682 s % 129.60/18.55 % (2616891)Peak memory usage: 43 MB % 129.60/18.55 % (2616891)Instructions burned: 5131 (million) % 129.60/18.55 % (2616919)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3178544303:i=5497:nm=2_2967 on theBenchmark for (2967ds/5497Mi) % 129.60/18.55 % (2616919)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 129.60/18.55 % (2616919)Terminated due to inappropriate strategy. % 129.60/18.55 % (2616919)------------------------------ % 129.60/18.55 % (2616919)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 129.60/18.55 % (2616919)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 129.60/18.55 % (2616919)CaDiCaL version: 2.1.3 % 129.60/18.55 % (2616919)Termination reason: Inappropriate % 129.60/18.55 % (2616919)Time elapsed: 0.036 s % 129.60/18.55 % (2616919)Peak memory usage: 14 MB % 129.60/18.55 % (2616919)Instructions burned: 83 (million) % 129.60/18.55 % (2616919)------------------------------ % 129.60/18.55 % (2616919)------------------------------ % 129.60/18.55 % (2616921)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=497834748:fmbsr=2:i=46332_2967 on theBenchmark for (2967ds/46332Mi) % 129.60/18.55 % (2616921)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 129.60/18.55 % (2616921)Terminated due to inappropriate strategy. % 129.60/18.55 % (2616921)------------------------------ % 129.60/18.55 % (2616921)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 129.60/18.55 % (2616921)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 129.60/18.55 % (2616921)CaDiCaL version: 2.1.3 % 129.60/18.55 % (2616921)Termination reason: Inappropriate % 129.60/18.55 % (2616921)Time elapsed: 0.048 s % 129.60/18.55 % (2616921)Peak memory usage: 14 MB % 129.60/18.55 % (2616921)Instructions burned: 115 (million) % 129.60/18.55 % (2616921)------------------------------ % 129.60/18.55 % (2616921)------------------------------ % 129.60/18.55 % (2616923)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=3608488255:i=14071_2966 on theBenchmark for (2966ds/14071Mi) % 129.60/18.55 % (2616923)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 129.60/18.55 % (2616923)Terminated due to inappropriate strategy. % 129.60/18.55 % (2616923)------------------------------ % 129.60/18.55 % (2616923)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 129.60/18.55 % (2616923)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 129.60/18.55 % (2616923)CaDiCaL version: 2.1.3 % 129.60/18.55 % (2616923)Termination reason: Inappropriate % 129.60/18.55 % (2616923)Time elapsed: 0.048 s % 129.60/18.55 % (2616923)Peak memory usage: 14 MB % 129.60/18.55 % (2616923)Instructions burned: 115 (million) % 129.60/18.55 % (2616923)------------------------------ % 129.60/18.55 % (2616923)------------------------------ % 129.60/18.55 % (2616925)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2100773168:i=22565:add=on:rawr=on_2965 on theBenchmark for (2965ds/22565Mi) % 129.60/18.55 % (2616901)Instruction limit reached! % 129.60/18.55 % (2616901)------------------------------ % 129.60/18.55 % (2616901)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 129.60/18.55 % (2616901)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 129.60/18.55 % (2616901)CaDiCaL version: 2.1.3 % 129.60/18.55 % (2616901)Termination reason: Instruction limit % 129.60/18.55 % (2616901)Termination phase: Saturation % 129.60/18.55 % (2616901)Time elapsed: 2.993 s % 129.60/18.55 % (2616901)Peak memory usage: 32 MB % 129.60/18.55 % (2616901)Instructions burned: 5118 (million) % 129.60/18.55 % (2616927)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=2307389758:i=8173:av=off_2962 on theBenchmark for (2962ds/8173Mi) % 131.75/18.85 % (2616913)Instruction limit reached! % 131.75/18.85 % (2616913)------------------------------ % 131.75/18.85 % (2616913)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 131.75/18.85 % (2616913)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.75/18.85 % (2616913)CaDiCaL version: 2.1.3 % 131.75/18.85 % (2616913)Termination reason: Instruction limit % 131.75/18.85 % (2616913)Termination phase: Saturation % 131.75/18.85 % (2616913)Time elapsed: 2.328 s % 131.75/18.85 % (2616913)Peak memory usage: 47 MB % 131.75/18.85 % (2616913)Instructions burned: 4592 (million) % 131.75/18.85 % (2616929)dis+10_16:1_sil=16000:random_seed=1369740089:i=9155:fsr=off_2954 on theBenchmark for (2954ds/9155Mi) % 131.75/18.85 % (2616917)Instruction limit reached! % 131.75/18.85 % (2616917)------------------------------ % 131.75/18.85 % (2616917)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 131.75/18.85 % (2616917)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.75/18.85 % (2616917)CaDiCaL version: 2.1.3 % 131.75/18.85 % (2616917)Termination reason: Instruction limit % 131.75/18.85 % (2616917)Termination phase: Saturation % 131.75/18.85 % (2616917)Time elapsed: 2.752 s % 131.75/18.85 % (2616917)Peak memory usage: 47 MB % 131.75/18.85 % (2616917)Instructions burned: 5211 (million) % 131.75/18.85 % (2616931)ott-3_8_sil=64000:random_seed=2650872503:i=20139:bs=on_2944 on theBenchmark for (2944ds/20139Mi) % 131.75/18.85 % (2616927)Instruction limit reached! % 131.75/18.85 % (2616927)------------------------------ % 131.75/18.85 % (2616927)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 131.75/18.85 % (2616927)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.75/18.85 % (2616927)CaDiCaL version: 2.1.3 % 131.75/18.85 % (2616927)Termination reason: Instruction limit % 131.75/18.85 % (2616927)Termination phase: Saturation % 131.75/18.85 % (2616927)Time elapsed: 3.505 s % 131.75/18.85 % (2616927)Peak memory usage: 37 MB % 131.75/18.85 % (2616927)Instructions burned: 8173 (million) % 131.75/18.85 % (2616933)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=1588163649:fmbsr=2:i=32576_2926 on theBenchmark for (2926ds/32576Mi) % 131.75/18.85 % (2616933)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 131.75/18.85 % (2616933)Terminated due to inappropriate strategy. % 131.75/18.85 % (2616933)------------------------------ % 131.75/18.85 % (2616933)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 131.75/18.85 % (2616933)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.75/18.85 % (2616933)CaDiCaL version: 2.1.3 % 131.75/18.85 % (2616933)Termination reason: Inappropriate % 131.75/18.85 % (2616933)Time elapsed: 0.046 s % 131.75/18.85 % (2616933)Peak memory usage: 14 MB % 131.75/18.85 % (2616933)Instructions burned: 112 (million) % 131.75/18.85 % (2616933)------------------------------ % 131.75/18.85 % (2616933)------------------------------ % 131.75/18.85 % (2616935)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=3977591998:i=11404_2926 on theBenchmark for (2926ds/11404Mi) % 131.75/18.85 % (2616929)Instruction limit reached! % 131.75/18.85 % (2616929)------------------------------ % 131.75/18.85 % (2616929)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 131.75/18.85 % (2616929)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.75/18.85 % (2616929)CaDiCaL version: 2.1.3 % 131.75/18.85 % (2616929)Termination reason: Instruction limit % 131.75/18.85 % (2616929)Termination phase: Saturation % 131.75/18.85 % (2616929)Time elapsed: 4.710 s % 131.75/18.85 % (2616929)Peak memory usage: 54 MB % 131.75/18.85 % (2616929)Instructions burned: 9157 (million) % 131.75/18.85 % (2616937)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=4130408242:i=14134_2907 on theBenchmark for (2907ds/14134Mi) % 131.75/18.85 % (2616935)Instruction limit reached! % 131.75/18.85 % (2616935)------------------------------ % 131.75/18.85 % (2616935)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 131.75/18.85 % (2616935)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.75/18.85 % (2616935)CaDiCaL version: 2.1.3 % 131.75/18.85 % (2616935)Termination reason: Instruction limit % 131.75/18.85 % (2616935)Termination phase: Saturation % 131.75/18.85 % (2616935)Time elapsed: 7.345 s % 131.75/18.85 % (2616935)Peak memory usage: 47 MB % 131.75/18.85 % (2616935)Instructions burned: 11404 (million) % 131.75/18.85 % (2616939)dis+33_16_sil=32000:sac=on:random_seed=2800106282:i=15851:nm=0_2852 on theBenchmark for (2852ds/15851Mi) % 131.75/18.85 % (2616931)Instruction limit reached! % 131.75/18.85 % (2616931)------------------------------ % 131.75/18.85 % (2616931)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 159.29/22.74 % (2616931)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 159.29/22.74 % (2616931)CaDiCaL version: 2.1.3 % 159.29/22.74 % (2616931)Termination reason: Instruction limit % 159.29/22.74 % (2616931)Termination phase: Saturation % 159.29/22.74 % (2616931)Time elapsed: 10.108 s % 159.29/22.74 % (2616931)Peak memory usage: 51 MB % 159.29/22.74 % (2616931)Instructions burned: 20139 (million) % 159.29/22.74 % (2616941)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=3344431356:avsq=on:i=17627:add=on:amm=off_2843 on theBenchmark for (2843ds/17627Mi) % 159.29/22.74 % (2616915)Instruction limit reached! % 159.29/22.74 % (2616915)------------------------------ % 159.29/22.74 % (2616915)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 159.29/22.74 % (2616915)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 159.29/22.74 % (2616915)CaDiCaL version: 2.1.3 % 159.29/22.74 % (2616915)Termination reason: Instruction limit % 159.29/22.74 % (2616915)Termination phase: Saturation % 159.29/22.74 % (2616915)Time elapsed: 13.771 s % 159.29/22.74 % (2616915)Peak memory usage: 41 MB % 159.29/22.74 % (2616915)Instructions burned: 29341 (million) % 159.29/22.74 % (2616943)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=3757611974:s2a=on:i=53295_2835 on theBenchmark for (2835ds/53295Mi) % 159.29/22.74 % (2616925)Instruction limit reached! % 159.29/22.74 % (2616925)------------------------------ % 159.29/22.74 % (2616925)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 159.29/22.74 % (2616925)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 159.29/22.74 % (2616925)CaDiCaL version: 2.1.3 % 159.29/22.74 % (2616925)Termination reason: Instruction limit % 159.29/22.74 % (2616925)Termination phase: Saturation % 159.29/22.74 % (2616925)Time elapsed: 13.680 s % 159.29/22.74 % (2616925)Peak memory usage: 302 MB % 159.29/22.74 % (2616925)Instructions burned: 22567 (million) % 159.29/22.74 % (2616945)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=2737137860:i=26857:ins=20_2828 on theBenchmark for (2828ds/26857Mi) % 159.29/22.74 % (2616945)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 159.29/22.74 % (2616945)Terminated due to inappropriate strategy. % 159.29/22.74 % (2616945)------------------------------ % 159.29/22.74 % (2616945)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 159.29/22.74 % (2616945)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 159.29/22.74 % (2616945)CaDiCaL version: 2.1.3 % 159.29/22.74 % (2616945)Termination reason: Inappropriate % 159.29/22.74 % (2616945)Time elapsed: 0.036 s % 159.29/22.74 % (2616945)Peak memory usage: 13 MB % 159.29/22.74 % (2616945)Instructions burned: 83 (million) % 159.29/22.74 % (2616945)------------------------------ % 159.29/22.74 % (2616945)------------------------------ % 159.29/22.74 % (2616947)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=4281034274:i=28120:bs=on:fsr=off_2827 on theBenchmark for (2827ds/28120Mi) % 159.29/22.74 % (2616937)Instruction limit reached! % 159.29/22.74 % (2616937)------------------------------ % 159.29/22.74 % (2616937)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 159.29/22.74 % (2616937)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 159.29/22.74 % (2616937)CaDiCaL version: 2.1.3 % 159.29/22.74 % (2616937)Termination reason: Instruction limit % 159.29/22.74 % (2616937)Termination phase: Saturation % 159.29/22.74 % (2616937)Time elapsed: 8.967 s % 159.29/22.74 % (2616937)Peak memory usage: 53 MB % 159.29/22.74 % (2616937)Instructions burned: 14135 (million) % 159.29/22.74 % (2616949)fmb+10_1_sil=256000:fmbss=7:random_seed=4275887883:fmbsr=1.6:i=182295_2817 on theBenchmark for (2817ds/182295Mi) % 159.29/22.74 % (2616949)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 159.29/22.74 % (2616949)Terminated due to inappropriate strategy. % 159.29/22.74 % (2616949)------------------------------ % 159.29/22.74 % (2616949)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 159.29/22.74 % (2616949)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 159.29/22.74 % (2616949)CaDiCaL version: 2.1.3 % 159.29/22.74 % (2616949)Termination reason: Inappropriate % 159.29/22.74 % (2616949)Time elapsed: 0.036 s % 159.29/22.74 % (2616949)Peak memory usage: 13 MB % 159.29/22.74 % (2616949)Instructions burned: 83 (million) % 159.29/22.74 % (2616949)------------------------------ % 159.29/22.74 % (2616949)------------------------------ % 159.29/22.74 % (2616951)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=986425693:i=44625:gsp=on_2816 on theBenchmark for (2816ds/44625Mi) % 172.22/24.53 % (2616951)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 172.22/24.53 % (2616951)Terminated due to inappropriate strategy. % 172.22/24.53 % (2616951)------------------------------ % 172.22/24.53 % (2616951)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 172.22/24.53 % (2616951)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 172.22/24.53 % (2616951)CaDiCaL version: 2.1.3 % 172.22/24.53 % (2616951)Termination reason: Inappropriate % 172.22/24.53 % (2616951)Time elapsed: 0.040 s % 172.22/24.53 % (2616951)Peak memory usage: 14 MB % 172.22/24.53 % (2616951)Instructions burned: 87 (million) % 172.22/24.53 % (2616951)------------------------------ % 172.22/24.53 % (2616951)------------------------------ % 172.22/24.53 % (2616953)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=2498661579:i=160505_2816 on theBenchmark for (2816ds/160505Mi) % 172.22/24.53 % (2616953)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 172.22/24.53 % (2616953)Terminated due to inappropriate strategy. % 172.22/24.53 % (2616953)------------------------------ % 172.22/24.53 % (2616953)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 172.22/24.53 % (2616953)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 172.22/24.53 % (2616953)CaDiCaL version: 2.1.3 % 172.22/24.53 % (2616953)Termination reason: Inappropriate % 172.22/24.53 % (2616953)Time elapsed: 0.036 s % 172.22/24.53 % (2616953)Peak memory usage: 13 MB % 172.22/24.53 % (2616953)Instructions burned: 83 (million) % 172.22/24.53 % (2616953)------------------------------ % 172.22/24.53 % (2616953)------------------------------ % 172.22/24.53 % (2616955)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=1322278721:fmbsr=1.3:i=225729_2815 on theBenchmark for (2815ds/225729Mi) % 172.22/24.53 % (2616955)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 172.22/24.53 % (2616955)Terminated due to inappropriate strategy. % 172.22/24.53 % (2616955)------------------------------ % 172.22/24.53 % (2616955)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 172.22/24.53 % (2616955)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 172.22/24.53 % (2616955)CaDiCaL version: 2.1.3 % 172.22/24.53 % (2616955)Termination reason: Inappropriate % 172.22/24.53 % (2616955)Time elapsed: 0.048 s % 172.22/24.53 % (2616955)Peak memory usage: 14 MB % 172.22/24.53 % (2616955)Instructions burned: 115 (million) % 172.22/24.53 % (2616955)------------------------------ % 172.22/24.53 % (2616955)------------------------------ % 172.22/24.53 % (2616957)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=3853277561:fmbsr=2:i=185024:ins=7_2815 on theBenchmark for (2815ds/185024Mi) % 172.22/24.53 % (2616957)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 172.22/24.53 % (2616957)Terminated due to inappropriate strategy. % 172.22/24.53 % (2616957)------------------------------ % 172.22/24.53 % (2616957)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 172.22/24.53 % (2616957)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 172.22/24.53 % (2616957)CaDiCaL version: 2.1.3 % 172.22/24.53 % (2616957)Termination reason: Inappropriate % 172.22/24.53 % (2616957)Time elapsed: 0.048 s % 172.22/24.53 % (2616957)Peak memory usage: 14 MB % 172.22/24.53 % (2616957)Instructions burned: 116 (million) % 172.22/24.53 % (2616957)------------------------------ % 172.22/24.53 % (2616957)------------------------------ % 172.22/24.53 % (2616853)Instruction limit reached! % 172.22/24.53 % (2616853)------------------------------ % 172.22/24.53 % (2616853)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 172.22/24.53 % (2616853)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 172.22/24.53 % (2616853)CaDiCaL version: 2.1.3 % 172.22/24.53 % (2616853)Termination reason: Instruction limit % 172.22/24.53 % (2616853)Termination phase: Saturation % 172.22/24.53 % (2616853)Time elapsed: 18.533 s % 172.22/24.53 % (2616853)Peak memory usage: 377 MB % 172.22/24.53 % (2616853)Instructions burned: 88027 (million) % 172.22/24.53 % (2616959)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=1475008913:rtra=on_2814 on theBenchmark for (2814ds/0Mi) % 172.22/24.53 % (2616961)% WARNING: option uhcvi not known. % 172.22/24.53 % (2616961)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1775381285:i=271062:add=off:rtra=on:rawr=on_2813 on theBenchmark for (2813ds/271062Mi) % 172.22/24.53 % (2616959)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 188.11/26.86 % (2616959)Terminated due to inappropriate strategy. % 188.11/26.86 % (2616959)------------------------------ % 188.11/26.86 % (2616959)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 188.11/26.86 % (2616959)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.11/26.86 % (2616959)CaDiCaL version: 2.1.3 % 188.11/26.86 % (2616959)Termination reason: Inappropriate % 188.11/26.86 % (2616959)Time elapsed: 0.046 s % 188.11/26.86 % (2616959)Peak memory usage: 15 MB % 188.11/26.86 % (2616959)Instructions burned: 97 (million) % 188.11/26.86 % (2616959)------------------------------ % 188.11/26.86 % (2616959)------------------------------ % 188.11/26.86 % (2616963)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3039134687:i=176048:add=on:rtra=on:rawr=on_2813 on theBenchmark for (2813ds/176048Mi) % 188.11/26.86 % (2616939)Instruction limit reached! % 188.11/26.86 % (2616939)------------------------------ % 188.11/26.86 % (2616939)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 188.11/26.86 % (2616939)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.11/26.86 % (2616939)CaDiCaL version: 2.1.3 % 188.11/26.86 % (2616939)Termination reason: Instruction limit % 188.11/26.86 % (2616939)Termination phase: Saturation % 188.11/26.86 % (2616939)Time elapsed: 7.155 s % 188.11/26.86 % (2616939)Peak memory usage: 34 MB % 188.11/26.86 % (2616939)Instructions burned: 15851 (million) % 188.11/26.86 % (2616966)dis+10_1_sil=32000:si=on:sp=arity:random_seed=2381719913:i=206:fgj=on:rtra=on_2780 on theBenchmark for (2780ds/206Mi) % 188.11/26.86 % (2616966)Instruction limit reached! % 188.11/26.86 % (2616966)------------------------------ % 188.11/26.86 % (2616966)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 188.11/26.86 % (2616966)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.11/26.86 % (2616966)CaDiCaL version: 2.1.3 % 188.11/26.86 % (2616966)Termination reason: Instruction limit % 188.11/26.86 % (2616966)Termination phase: Saturation % 188.11/26.86 % (2616966)Time elapsed: 0.104 s % 188.11/26.86 % (2616966)Peak memory usage: 17 MB % 188.11/26.86 % (2616966)Instructions burned: 207 (million) % 188.11/26.86 % (2616968)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=2175204637:i=232:rtra=on_2779 on theBenchmark for (2779ds/232Mi) % 188.11/26.86 % (2616968)Instruction limit reached! % 188.11/26.86 % (2616968)------------------------------ % 188.11/26.86 % (2616968)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 188.11/26.86 % (2616968)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.11/26.86 % (2616968)CaDiCaL version: 2.1.3 % 188.11/26.86 % (2616968)Termination reason: Instruction limit % 188.11/26.86 % (2616968)Termination phase: Saturation % 188.11/26.86 % (2616968)Time elapsed: 0.106 s % 188.11/26.86 % (2616968)Peak memory usage: 16 MB % 188.11/26.86 % (2616968)Instructions burned: 233 (million) % 188.11/26.86 % (2616970)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=3859462181:i=262:rtra=on_2778 on theBenchmark for (2778ds/262Mi) % 188.11/26.86 % (2616970)Instruction limit reached! % 188.11/26.86 % (2616970)------------------------------ % 188.11/26.86 % (2616970)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 188.11/26.86 % (2616970)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.11/26.86 % (2616970)CaDiCaL version: 2.1.3 % 188.11/26.86 % (2616970)Termination reason: Instruction limit % 188.11/26.86 % (2616970)Termination phase: Saturation % 188.11/26.86 % (2616970)Time elapsed: 0.119 s % 188.11/26.86 % (2616970)Peak memory usage: 17 MB % 188.11/26.86 % (2616970)Instructions burned: 262 (million) % 188.11/26.86 % (2616972)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=2490763358:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2776 on theBenchmark for (2776ds/318Mi) % 188.11/26.86 % (2616972)Instruction limit reached! % 188.11/26.86 % (2616972)------------------------------ % 188.11/26.86 % (2616972)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 188.11/26.86 % (2616972)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.11/26.86 % (2616972)CaDiCaL version: 2.1.3 % 188.11/26.86 % (2616972)Termination reason: Instruction limit % 188.11/26.86 % (2616972)Termination phase: Saturation % 188.11/26.86 % (2616972)Time elapsed: 0.156 s % 188.11/26.86 % (2616972)Peak memory usage: 18 MB % 188.11/26.86 % (2616972)Instructions burned: 318 (million) % 188.11/26.86 % (2616974)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=2326279778:i=1428:nm=2:rtra=on_2775 on theBenchmark for (2775ds/1428Mi) % 202.00/28.71 % (2616974)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 202.00/28.71 % (2616974)Terminated due to inappropriate strategy. % 202.00/28.71 % (2616974)------------------------------ % 202.00/28.71 % (2616974)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 202.00/28.71 % (2616974)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.00/28.71 % (2616974)CaDiCaL version: 2.1.3 % 202.00/28.71 % (2616974)Termination reason: Inappropriate % 202.00/28.71 % (2616974)Time elapsed: 0.046 s % 202.00/28.71 % (2616974)Peak memory usage: 15 MB % 202.00/28.71 % (2616974)Instructions burned: 97 (million) % 202.00/28.71 % (2616974)------------------------------ % 202.00/28.71 % (2616974)------------------------------ % 202.00/28.71 % (2616976)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=474955917:i=262:bd=preordered:rtra=on:fsd=on_2774 on theBenchmark for (2774ds/262Mi) % 202.00/28.71 % (2616976)Instruction limit reached! % 202.00/28.71 % (2616976)------------------------------ % 202.00/28.71 % (2616976)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 202.00/28.71 % (2616976)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.00/28.71 % (2616976)CaDiCaL version: 2.1.3 % 202.00/28.71 % (2616976)Termination reason: Instruction limit % 202.00/28.71 % (2616976)Termination phase: Saturation % 202.00/28.71 % (2616976)Time elapsed: 0.119 s % 202.00/28.71 % (2616976)Peak memory usage: 17 MB % 202.00/28.71 % (2616976)Instructions burned: 263 (million) % 202.00/28.71 % (2616978)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=334396435:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2772 on theBenchmark for (2772ds/1368Mi) % 202.00/28.71 % (2616978)Instruction limit reached! % 202.00/28.71 % (2616978)------------------------------ % 202.00/28.71 % (2616978)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 202.00/28.71 % (2616978)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.00/28.71 % (2616978)CaDiCaL version: 2.1.3 % 202.00/28.71 % (2616978)Termination reason: Instruction limit % 202.00/28.71 % (2616978)Termination phase: Saturation % 202.00/28.71 % (2616978)Time elapsed: 0.717 s % 202.00/28.71 % (2616978)Peak memory usage: 24 MB % 202.00/28.71 % (2616978)Instructions burned: 1369 (million) % 202.00/28.71 % (2616980)ott-21_1_sil=16000:si=on:fs=off:random_seed=2784883319:i=360:av=off:fsr=off:rtra=on_2765 on theBenchmark for (2765ds/360Mi) % 202.00/28.71 % (2616980)Instruction limit reached! % 202.00/28.71 % (2616980)------------------------------ % 202.00/28.71 % (2616980)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 202.00/28.71 % (2616980)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.00/28.71 % (2616980)CaDiCaL version: 2.1.3 % 202.00/28.71 % (2616980)Termination reason: Instruction limit % 202.00/28.71 % (2616980)Termination phase: Saturation % 202.00/28.71 % (2616980)Time elapsed: 0.178 s % 202.00/28.71 % (2616980)Peak memory usage: 17 MB % 202.00/28.71 % (2616980)Instructions burned: 361 (million) % 202.00/28.71 % (2616982)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3292001453:i=954:bd=all:rtra=on_2763 on theBenchmark for (2763ds/954Mi) % 202.00/28.71 % (2616982)Instruction limit reached! % 202.00/28.71 % (2616982)------------------------------ % 202.00/28.71 % (2616982)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 202.00/28.71 % (2616982)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.00/28.71 % (2616982)CaDiCaL version: 2.1.3 % 202.00/28.71 % (2616982)Termination reason: Instruction limit % 202.00/28.71 % (2616982)Termination phase: Saturation % 202.00/28.71 % (2616982)Time elapsed: 0.586 s % 202.00/28.71 % (2616982)Peak memory usage: 20 MB % 202.00/28.71 % (2616982)Instructions burned: 955 (million) % 202.00/28.71 % (2616984)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=3034367434:fmbsr=1.3:i=1730:ins=25:rtra=on_2757 on theBenchmark for (2757ds/1730Mi) % 202.00/28.71 % (2616984)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 202.00/28.71 % (2616984)Terminated due to inappropriate strategy. % 202.00/28.71 % (2616984)------------------------------ % 202.00/28.71 % (2616984)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 202.00/28.71 % (2616984)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.00/28.71 % (2616984)CaDiCaL version: 2.1.3 % 202.00/28.71 % (2616984)Termination reason: Inappropriate % 238.96/33.94 % (2616984)Time elapsed: 0.045 s % 238.96/33.94 % (2616984)Peak memory usage: 15 MB % 238.96/33.94 % (2616984)Instructions burned: 96 (million) % 238.96/33.94 % (2616984)------------------------------ % 238.96/33.94 % (2616984)------------------------------ % 238.96/33.94 % (2616986)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=1581840314:i=2358:rtra=on_2756 on theBenchmark for (2756ds/2358Mi) % 238.96/33.94 % (2616986)Instruction limit reached! % 238.96/33.94 % (2616986)------------------------------ % 238.96/33.94 % (2616986)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 238.96/33.94 % (2616986)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.96/33.94 % (2616986)CaDiCaL version: 2.1.3 % 238.96/33.94 % (2616986)Termination reason: Instruction limit % 238.96/33.94 % (2616986)Termination phase: Saturation % 238.96/33.94 % (2616986)Time elapsed: 1.346 s % 238.96/33.94 % (2616986)Peak memory usage: 25 MB % 238.96/33.94 % (2616986)Instructions burned: 2358 (million) % 238.96/33.94 % (2616988)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=478068680:i=1778:ins=1:rtra=on_2743 on theBenchmark for (2743ds/1778Mi) % 238.96/33.94 % (2616988)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 238.96/33.94 % (2616988)Terminated due to inappropriate strategy. % 238.96/33.94 % (2616988)------------------------------ % 238.96/33.94 % (2616988)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 238.96/33.94 % (2616988)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.96/33.94 % (2616988)CaDiCaL version: 2.1.3 % 238.96/33.94 % (2616988)Termination reason: Inappropriate % 238.96/33.94 % (2616988)Time elapsed: 0.062 s % 238.96/33.94 % (2616988)Peak memory usage: 16 MB % 238.96/33.94 % (2616988)Instructions burned: 129 (million) % 238.96/33.94 % (2616988)------------------------------ % 238.96/33.94 % (2616988)------------------------------ % 238.96/33.94 % (2616990)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=2947480739:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2742 on theBenchmark for (2742ds/1384Mi) % 238.96/33.94 % (2616941)Instruction limit reached! % 238.96/33.94 % (2616941)------------------------------ % 238.96/33.94 % (2616941)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 238.96/33.94 % (2616941)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.96/33.94 % (2616941)CaDiCaL version: 2.1.3 % 238.96/33.94 % (2616941)Termination reason: Instruction limit % 238.96/33.94 % (2616941)Termination phase: Saturation % 238.96/33.94 % (2616941)Time elapsed: 10.466 s % 238.96/33.94 % (2616941)Peak memory usage: 113 MB % 238.96/33.94 % (2616941)Instructions burned: 17628 (million) % 238.96/33.94 % (2616992)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=2037481115:i=1758:kws=inv_precedence:fsr=off:rtra=on_2738 on theBenchmark for (2738ds/1758Mi) % 238.96/33.94 % (2616990)Instruction limit reached! % 238.96/33.94 % (2616990)------------------------------ % 238.96/33.94 % (2616990)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 238.96/33.94 % (2616990)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.96/33.94 % (2616990)CaDiCaL version: 2.1.3 % 238.96/33.94 % (2616990)Termination reason: Instruction limit % 238.96/33.94 % (2616990)Termination phase: Saturation % 238.96/33.94 % (2616990)Time elapsed: 0.759 s % 238.96/33.94 % (2616990)Peak memory usage: 24 MB % 238.96/33.94 % (2616990)Instructions burned: 1384 (million) % 238.96/33.94 % (2616994)fmb+10_1_sil=64000:si=on:random_seed=4235987546:i=44122:nm=2:rtra=on:gsp=on_2734 on theBenchmark for (2734ds/44122Mi) % 238.96/33.94 % (2616994)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 238.96/33.94 % (2616994)Terminated due to inappropriate strategy. % 238.96/33.94 % (2616994)------------------------------ % 238.96/33.94 % (2616994)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 238.96/33.94 % (2616994)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.96/33.94 % (2616994)CaDiCaL version: 2.1.3 % 238.96/33.94 % (2616994)Termination reason: Inappropriate % 238.96/33.94 % (2616994)Time elapsed: 0.050 s % 238.96/33.94 % (2616994)Peak memory usage: 15 MB % 238.96/33.94 % (2616994)Instructions burned: 105 (million) % 238.96/33.94 % (2616994)------------------------------ % 238.96/33.94 % (2616994)------------------------------ % 238.96/33.94 % (2616996)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=927219135:i=19030:nm=5:rtra=on_2733 on theBenchmark for (2733ds/19030Mi) % 277.31/39.33 % (2616996)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 277.31/39.33 % (2616996)Terminated due to inappropriate strategy. % 277.31/39.33 % (2616996)------------------------------ % 277.31/39.33 % (2616996)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 277.31/39.33 % (2616996)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 277.31/39.33 % (2616996)CaDiCaL version: 2.1.3 % 277.31/39.33 % (2616996)Termination reason: Inappropriate % 277.31/39.33 % (2616996)Time elapsed: 0.046 s % 277.31/39.33 % (2616996)Peak memory usage: 15 MB % 277.31/39.33 % (2616996)Instructions burned: 97 (million) % 277.31/39.33 % (2616996)------------------------------ % 277.31/39.33 % (2616996)------------------------------ % 277.31/39.33 % (2616998)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=1975566408:fmbsr=1.7:i=1840:rtra=on_2733 on theBenchmark for (2733ds/1840Mi) % 277.31/39.33 % (2616998)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 277.31/39.33 % (2616998)Terminated due to inappropriate strategy. % 277.31/39.33 % (2616998)------------------------------ % 277.31/39.33 % (2616998)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 277.31/39.33 % (2616998)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 277.31/39.33 % (2616998)CaDiCaL version: 2.1.3 % 277.31/39.33 % (2616998)Termination reason: Inappropriate % 277.31/39.33 % (2616998)Time elapsed: 0.046 s % 277.31/39.33 % (2616998)Peak memory usage: 15 MB % 277.31/39.33 % (2616998)Instructions burned: 97 (million) % 277.31/39.33 % (2616998)------------------------------ % 277.31/39.33 % (2616998)------------------------------ % 277.31/39.33 % (2617000)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=1868477330:i=10262:rtra=on_2732 on theBenchmark for (2732ds/10262Mi) % 277.31/39.33 % (2616992)Instruction limit reached! % 277.31/39.33 % (2616992)------------------------------ % 277.31/39.33 % (2616992)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 277.31/39.33 % (2616992)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 277.31/39.33 % (2616992)CaDiCaL version: 2.1.3 % 277.31/39.33 % (2616992)Termination reason: Instruction limit % 277.31/39.33 % (2616992)Termination phase: Saturation % 277.31/39.33 % (2616992)Time elapsed: 1.006 s % 277.31/39.33 % (2616992)Peak memory usage: 29 MB % 277.31/39.33 % (2616992)Instructions burned: 1759 (million) % 277.31/39.33 % (2617002)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1728124885:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2728 on theBenchmark for (2728ds/2944Mi) % 277.31/39.33 % (2616947)Instruction limit reached! % 277.31/39.33 % (2616947)------------------------------ % 277.31/39.33 % (2616947)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 277.31/39.33 % (2616947)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 277.31/39.33 % (2616947)CaDiCaL version: 2.1.3 % 277.31/39.33 % (2616947)Termination reason: Instruction limit % 277.31/39.33 % (2616947)Termination phase: Saturation % 277.31/39.33 % (2616947)Time elapsed: 11.114 s % 277.31/39.33 % (2616947)Peak memory usage: 26 MB % 277.31/39.33 % (2616947)Instructions burned: 28120 (million) % 277.31/39.33 % (2617004)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=3688311234:i=12648:rtra=on_2716 on theBenchmark for (2716ds/12648Mi) % 277.31/39.33 % (2617004)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 277.31/39.33 % (2617004)Terminated due to inappropriate strategy. % 277.31/39.33 % (2617004)------------------------------ % 277.31/39.33 % (2617004)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 277.31/39.33 % (2617004)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 277.31/39.33 % (2617004)CaDiCaL version: 2.1.3 % 277.31/39.33 % (2617004)Termination reason: Inappropriate % 277.31/39.33 % (2617004)Time elapsed: 0.046 s % 277.31/39.33 % (2617004)Peak memory usage: 15 MB % 277.31/39.33 % (2617004)Instructions burned: 97 (million) % 277.31/39.33 % (2617004)------------------------------ % 277.31/39.33 % (2617004)------------------------------ % 277.31/39.33 % (2617006)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=2573250941:fmbsr=2.30978:i=4348:rtra=on_2715 on theBenchmark for (2715ds/4348Mi) % 277.31/39.33 % (2617006)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 277.31/39.33 % (2617006)Terminated due to inappropriate strategy. % 277.31/39.33 % (2617006)-----Terminated % 300.53/42.63 % Vampire exiting % 300.53/42.63 Terminated %------------------------------------------------------------------------------