%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW648_2 : TPTP v9.3.1. Released v6.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/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:40:35 PM UTC 2026 % Result : Timeout 300.49s 42.53s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWW648_2 : TPTP v9.3.1. Released v6.1.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/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 14:23:15 UTC 2026 % 0.08/0.18 % CPUTime : % 0.08/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.08/0.21 Running first-order model finding % 0.08/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.65/0.90 % (1807764)Will run a generic schedule for satisfiability detection. % 3.65/0.90 % (1807769)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1574093301_2999 on theBenchmark for (2999ds/0Mi) % 3.65/0.90 % (1807769)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.65/0.90 % (1807769)Terminated due to inappropriate strategy. % 3.65/0.90 % (1807769)------------------------------ % 3.65/0.90 % (1807769)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.65/0.90 % (1807769)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.65/0.90 % (1807769)CaDiCaL version: 2.1.3 % 3.65/0.90 % (1807769)Termination reason: Inappropriate % 3.65/0.90 % (1807769)Time elapsed: 0.001 s % 3.65/0.90 % (1807769)Peak memory usage: 10 MB % 3.65/0.90 % (1807769)Instructions burned: 4 (million) % 3.65/0.90 % (1807769)------------------------------ % 3.65/0.90 % (1807769)------------------------------ % 3.65/0.90 % (1807770)% WARNING: option uhcvi not known. % 3.65/0.90 % (1807770)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3655145659:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 3.65/0.90 % (1807773)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=4104704170:i=116_2999 on theBenchmark for (2999ds/116Mi) % 3.65/0.90 % (1807771)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=265773378:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 3.65/0.90 % (1807772)dis+10_1_sil=32000:sp=arity:random_seed=413740293:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 3.65/0.90 % (1807777)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1838049966:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 3.65/0.90 % (1807777)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.65/0.90 % (1807777)Terminated due to inappropriate strategy. % 3.65/0.90 % (1807777)------------------------------ % 3.65/0.90 % (1807777)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.65/0.90 % (1807777)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.65/0.90 % (1807777)CaDiCaL version: 2.1.3 % 3.65/0.90 % (1807777)Termination reason: Inappropriate % 3.65/0.90 % (1807777)Time elapsed: 0.001 s % 3.65/0.90 % (1807777)Peak memory usage: 10 MB % 3.65/0.90 % (1807777)Instructions burned: 4 (million) % 3.65/0.90 % (1807777)------------------------------ % 3.65/0.90 % (1807777)------------------------------ % 3.65/0.90 % (1807775)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=379867475:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 3.65/0.90 % (1807774)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=438319120:i=131_2999 on theBenchmark for (2999ds/131Mi) % 3.65/0.90 % (1807784)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=428179938:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 3.65/0.90 % (1807772)Instruction limit reached! % 3.65/0.90 % (1807772)------------------------------ % 3.65/0.90 % (1807772)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.65/0.90 % (1807772)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.65/0.90 % (1807772)CaDiCaL version: 2.1.3 % 3.65/0.90 % (1807772)Termination reason: Instruction limit % 3.65/0.90 % (1807772)Termination phase: Saturation % 3.65/0.90 % (1807772)Time elapsed: 0.070 s % 3.65/0.90 % (1807772)Peak memory usage: 13 MB % 3.65/0.90 % (1807772)Instructions burned: 104 (million) % 3.65/0.90 % (1807784)Instruction limit reached! % 3.65/0.90 % (1807784)------------------------------ % 3.65/0.90 % (1807784)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.65/0.90 % (1807784)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.65/0.90 % (1807784)CaDiCaL version: 2.1.3 % 3.65/0.90 % (1807784)Termination reason: Instruction limit % 3.65/0.90 % (1807784)Termination phase: Saturation % 3.65/0.90 % (1807784)Time elapsed: 0.051 s % 3.65/0.90 % (1807784)Peak memory usage: 14 MB % 3.65/0.90 % (1807784)Instructions burned: 132 (million) % 3.65/0.90 % (1807773)Instruction limit reached! % 3.65/0.90 % (1807773)------------------------------ % 3.65/0.90 % (1807773)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.65/0.90 % (1807773)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.65/0.90 % (1807773)CaDiCaL version: 2.1.3 % 3.65/0.90 % (1807773)Termination reason: Instruction limit % 7.28/1.38 % (1807773)Termination phase: Saturation % 7.28/1.38 % (1807773)Time elapsed: 0.080 s % 7.28/1.38 % (1807773)Peak memory usage: 13 MB % 7.28/1.38 % (1807773)Instructions burned: 116 (million) % 7.28/1.38 % (1807787)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=2644320219:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 7.28/1.38 % (1807788)ott-21_1_sil=16000:fs=off:random_seed=2560209217:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 7.28/1.38 % (1807789)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3397607301:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 7.28/1.38 % (1807775)Instruction limit reached! % 7.28/1.38 % (1807775)------------------------------ % 7.28/1.38 % (1807775)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.28/1.38 % (1807775)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.28/1.38 % (1807775)CaDiCaL version: 2.1.3 % 7.28/1.38 % (1807775)Termination reason: Instruction limit % 7.28/1.38 % (1807775)Termination phase: Saturation % 7.28/1.38 % (1807775)Time elapsed: 0.110 s % 7.28/1.38 % (1807775)Peak memory usage: 12 MB % 7.28/1.38 % (1807775)Instructions burned: 159 (million) % 7.28/1.38 % (1807774)Instruction limit reached! % 7.28/1.38 % (1807774)------------------------------ % 7.28/1.38 % (1807774)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.28/1.38 % (1807774)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.28/1.38 % (1807774)CaDiCaL version: 2.1.3 % 7.28/1.38 % (1807774)Termination reason: Instruction limit % 7.28/1.38 % (1807774)Termination phase: Saturation % 7.28/1.38 % (1807774)Time elapsed: 0.121 s % 7.28/1.38 % (1807774)Peak memory usage: 13 MB % 7.28/1.38 % (1807774)Instructions burned: 132 (million) % 7.28/1.38 % (1807793)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=788941135:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 7.28/1.38 % (1807793)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 7.28/1.38 % (1807793)Terminated due to inappropriate strategy. % 7.28/1.38 % (1807793)------------------------------ % 7.28/1.38 % (1807793)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.28/1.38 % (1807793)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.28/1.38 % (1807793)CaDiCaL version: 2.1.3 % 7.28/1.38 % (1807793)Termination reason: Inappropriate % 7.28/1.38 % (1807793)Time elapsed: 0.002 s % 7.28/1.38 % (1807793)Peak memory usage: 10 MB % 7.28/1.38 % (1807793)Instructions burned: 3 (million) % 7.28/1.38 % (1807793)------------------------------ % 7.28/1.38 % (1807793)------------------------------ % 7.28/1.38 % (1807794)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=4209033361:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 7.28/1.38 % (1807796)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2748692361:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 7.28/1.38 % (1807796)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 7.28/1.38 % (1807796)Terminated due to inappropriate strategy. % 7.28/1.38 % (1807796)------------------------------ % 7.28/1.38 % (1807796)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.28/1.38 % (1807796)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.28/1.38 % (1807796)CaDiCaL version: 2.1.3 % 7.28/1.38 % (1807796)Termination reason: Inappropriate % 7.28/1.38 % (1807796)Time elapsed: 0.002 s % 7.28/1.38 % (1807796)Peak memory usage: 10 MB % 7.28/1.38 % (1807796)Instructions burned: 4 (million) % 7.28/1.38 % (1807796)------------------------------ % 7.28/1.38 % (1807796)------------------------------ % 7.28/1.38 % (1807802)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=1773382211: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) % 7.28/1.38 % (1807788)Instruction limit reached! % 7.28/1.38 % (1807788)------------------------------ % 7.28/1.38 % (1807788)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.28/1.38 % (1807788)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.28/1.38 % (1807788)CaDiCaL version: 2.1.3 % 7.28/1.38 % (1807788)Termination reason: Instruction limit % 7.28/1.38 % (1807788)Termination phase: Saturation % 31.73/4.82 % (1807788)Time elapsed: 0.095 s % 31.73/4.82 % (1807788)Peak memory usage: 13 MB % 31.73/4.82 % (1807788)Instructions burned: 181 (million) % 31.73/4.82 % (1807810)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=4225524422:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 31.73/4.82 % (1807787)Instruction limit reached! % 31.73/4.82 % (1807787)------------------------------ % 31.73/4.82 % (1807787)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 31.73/4.82 % (1807787)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.73/4.82 % (1807787)CaDiCaL version: 2.1.3 % 31.73/4.82 % (1807787)Termination reason: Instruction limit % 31.73/4.82 % (1807787)Termination phase: Saturation % 31.73/4.82 % (1807787)Time elapsed: 0.223 s % 31.73/4.82 % (1807787)Peak memory usage: 17 MB % 31.73/4.82 % (1807787)Instructions burned: 688 (million) % 31.73/4.82 % (1807856)fmb+10_1_sil=64000:random_seed=2583802986:i=22061:nm=2:gsp=on_2996 on theBenchmark for (2996ds/22061Mi) % 31.73/4.82 % (1807856)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 31.73/4.82 % (1807856)Terminated due to inappropriate strategy. % 31.73/4.82 % (1807856)------------------------------ % 31.73/4.82 % (1807856)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 31.73/4.82 % (1807856)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.73/4.82 % (1807856)CaDiCaL version: 2.1.3 % 31.73/4.82 % (1807856)Termination reason: Inappropriate % 31.73/4.82 % (1807856)Time elapsed: 0.001 s % 31.73/4.82 % (1807856)Peak memory usage: 10 MB % 31.73/4.82 % (1807856)Instructions burned: 4 (million) % 31.73/4.82 % (1807856)------------------------------ % 31.73/4.82 % (1807856)------------------------------ % 31.73/4.82 % (1807865)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2183990051:i=9515:nm=5_2996 on theBenchmark for (2996ds/9515Mi) % 31.73/4.82 % (1807865)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 31.73/4.82 % (1807865)Terminated due to inappropriate strategy. % 31.73/4.82 % (1807865)------------------------------ % 31.73/4.82 % (1807865)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 31.73/4.82 % (1807865)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.73/4.82 % (1807865)CaDiCaL version: 2.1.3 % 31.73/4.82 % (1807865)Termination reason: Inappropriate % 31.73/4.82 % (1807865)Time elapsed: 0.001 s % 31.73/4.82 % (1807865)Peak memory usage: 10 MB % 31.73/4.82 % (1807865)Instructions burned: 4 (million) % 31.73/4.82 % (1807865)------------------------------ % 31.73/4.82 % (1807865)------------------------------ % 31.73/4.82 % (1807871)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3895926786:fmbsr=1.7:i=920_2996 on theBenchmark for (2996ds/920Mi) % 31.73/4.82 % (1807871)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 31.73/4.82 % (1807871)Terminated due to inappropriate strategy. % 31.73/4.82 % (1807871)------------------------------ % 31.73/4.82 % (1807871)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 31.73/4.82 % (1807871)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.73/4.82 % (1807871)CaDiCaL version: 2.1.3 % 31.73/4.82 % (1807871)Termination reason: Inappropriate % 31.73/4.82 % (1807871)Time elapsed: 0.002 s % 31.73/4.82 % (1807871)Peak memory usage: 10 MB % 31.73/4.82 % (1807871)Instructions burned: 4 (million) % 31.73/4.82 % (1807871)------------------------------ % 31.73/4.82 % (1807871)------------------------------ % 31.73/4.82 % (1807875)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3873650596:i=5131_2996 on theBenchmark for (2996ds/5131Mi) % 31.73/4.82 % (1807789)Instruction limit reached! % 31.73/4.82 % (1807789)------------------------------ % 31.73/4.82 % (1807789)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 31.73/4.82 % (1807789)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.73/4.82 % (1807789)CaDiCaL version: 2.1.3 % 31.73/4.82 % (1807789)Termination reason: Instruction limit % 31.73/4.82 % (1807789)Termination phase: Saturation % 31.73/4.82 % (1807789)Time elapsed: 0.311 s % 31.73/4.82 % (1807789)Peak memory usage: 13 MB % 31.73/4.82 % (1807789)Instructions burned: 478 (million) % 31.73/4.82 % (1807896)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2678767403:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi) % 31.73/4.82 % (1807802)Instruction limit reached! % 31.73/4.82 % (1807802)------------------------------ % 44.41/6.50 % (1807802)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 44.41/6.50 % (1807802)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 44.41/6.50 % (1807802)CaDiCaL version: 2.1.3 % 44.41/6.50 % (1807802)Termination reason: Instruction limit % 44.41/6.50 % (1807802)Termination phase: Saturation % 44.41/6.50 % (1807802)Time elapsed: 0.448 s % 44.41/6.50 % (1807802)Peak memory usage: 18 MB % 44.41/6.50 % (1807802)Instructions burned: 693 (million) % 44.41/6.50 % (1807952)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1456295124:i=6324_2993 on theBenchmark for (2993ds/6324Mi) % 44.41/6.50 % (1807952)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 44.41/6.50 % (1807952)Terminated due to inappropriate strategy. % 44.41/6.50 % (1807952)------------------------------ % 44.41/6.50 % (1807952)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 44.41/6.50 % (1807952)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 44.41/6.50 % (1807952)CaDiCaL version: 2.1.3 % 44.41/6.50 % (1807952)Termination reason: Inappropriate % 44.41/6.50 % (1807952)Time elapsed: 0.005 s % 44.41/6.50 % (1807952)Peak memory usage: 10 MB % 44.41/6.50 % (1807952)Instructions burned: 4 (million) % 44.41/6.50 % (1807952)------------------------------ % 44.41/6.50 % (1807952)------------------------------ % 44.41/6.50 % (1807962)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2517872953:fmbsr=2.30978:i=2174_2992 on theBenchmark for (2992ds/2174Mi) % 44.41/6.50 % (1807962)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 44.41/6.50 % (1807962)Terminated due to inappropriate strategy. % 44.41/6.50 % (1807962)------------------------------ % 44.41/6.50 % (1807962)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 44.41/6.50 % (1807962)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 44.41/6.50 % (1807962)CaDiCaL version: 2.1.3 % 44.41/6.50 % (1807962)Termination reason: Inappropriate % 44.41/6.50 % (1807962)Time elapsed: 0.005 s % 44.41/6.50 % (1807962)Peak memory usage: 10 MB % 44.41/6.50 % (1807962)Instructions burned: 4 (million) % 44.41/6.50 % (1807962)------------------------------ % 44.41/6.50 % (1807962)------------------------------ % 44.41/6.50 % (1807965)ott-2_1_sil=16000:newcnf=on:random_seed=2130738583:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2992 on theBenchmark for (2992ds/869Mi) % 44.41/6.50 % (1807810)Instruction limit reached! % 44.41/6.50 % (1807810)------------------------------ % 44.41/6.50 % (1807810)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 44.41/6.50 % (1807810)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 44.41/6.50 % (1807810)CaDiCaL version: 2.1.3 % 44.41/6.50 % (1807810)Termination reason: Instruction limit % 44.41/6.50 % (1807810)Termination phase: Saturation % 44.41/6.50 % (1807810)Time elapsed: 0.597 s % 44.41/6.50 % (1807810)Peak memory usage: 20 MB % 44.41/6.50 % (1807810)Instructions burned: 880 (million) % 44.41/6.50 % (1807972)ott+10_1_sil=32000:tgt=ground:random_seed=429358232:i=5114:av=off_2991 on theBenchmark for (2991ds/5114Mi) % 44.41/6.50 % (1807794)Instruction limit reached! % 44.41/6.50 % (1807794)------------------------------ % 44.41/6.50 % (1807794)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 44.41/6.50 % (1807794)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 44.41/6.50 % (1807794)CaDiCaL version: 2.1.3 % 44.41/6.50 % (1807794)Termination reason: Instruction limit % 44.41/6.50 % (1807794)Termination phase: Saturation % 44.41/6.50 % (1807794)Time elapsed: 0.930 s % 44.41/6.50 % (1807794)Peak memory usage: 21 MB % 44.41/6.50 % (1807794)Instructions burned: 1179 (million) % 44.41/6.50 % (1807985)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1612145221:i=54282_2988 on theBenchmark for (2988ds/54282Mi) % 44.41/6.50 % (1807985)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 44.41/6.50 % (1807985)Terminated due to inappropriate strategy. % 44.41/6.50 % (1807985)------------------------------ % 44.41/6.50 % (1807985)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 44.41/6.50 % (1807985)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 44.41/6.50 % (1807985)CaDiCaL version: 2.1.3 % 44.41/6.50 % (1807985)Termination reason: Inappropriate % 44.41/6.50 % (1807985)Time elapsed: 0.004 s % 44.41/6.50 % (1807985)Peak memory usage: 11 MB % 44.41/6.50 % (1807985)Instructions burned: 4 (million) % 183.56/26.04 % (1807985)------------------------------ % 183.56/26.04 % (1807985)------------------------------ % 183.56/26.04 % (1807987)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=4025221571:i=3512:aac=none_2988 on theBenchmark for (2988ds/3512Mi) % 183.56/26.04 % (1807965)Instruction limit reached! % 183.56/26.04 % (1807965)------------------------------ % 183.56/26.04 % (1807965)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 183.56/26.04 % (1807965)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 183.56/26.04 % (1807965)CaDiCaL version: 2.1.3 % 183.56/26.04 % (1807965)Termination reason: Instruction limit % 183.56/26.04 % (1807965)Termination phase: Saturation % 183.56/26.04 % (1807965)Time elapsed: 0.828 s % 183.56/26.04 % (1807965)Peak memory usage: 15 MB % 183.56/26.04 % (1807965)Instructions burned: 869 (million) % 183.56/26.04 % (1807999)dis+21_1_sil=32000:sas=cadical:random_seed=726701053:i=3773:amm=off_2983 on theBenchmark for (2983ds/3773Mi) % 183.56/26.04 % (1807896)Instruction limit reached! % 183.56/26.04 % (1807896)------------------------------ % 183.56/26.04 % (1807896)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 183.56/26.04 % (1807896)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 183.56/26.04 % (1807896)CaDiCaL version: 2.1.3 % 183.56/26.04 % (1807896)Termination reason: Instruction limit % 183.56/26.04 % (1807896)Termination phase: Saturation % 183.56/26.04 % (1807896)Time elapsed: 1.226 s % 183.56/26.04 % (1807896)Peak memory usage: 26 MB % 183.56/26.04 % (1807896)Instructions burned: 1472 (million) % 183.56/26.04 % (1808004)ott+11_1_sil=16000:gs=on:random_seed=2287851164:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2982 on theBenchmark for (2982ds/2251Mi) % 183.56/26.04 % (1807875)Instruction limit reached! % 183.56/26.04 % (1807875)------------------------------ % 183.56/26.04 % (1807875)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 183.56/26.04 % (1807875)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 183.56/26.04 % (1807875)CaDiCaL version: 2.1.3 % 183.56/26.04 % (1807875)Termination reason: Instruction limit % 183.56/26.04 % (1807875)Termination phase: Saturation % 183.56/26.04 % (1807875)Time elapsed: 2.398 s % 183.56/26.04 % (1807875)Peak memory usage: 44 MB % 183.56/26.04 % (1807875)Instructions burned: 5133 (million) % 183.56/26.04 % (1808017)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2194098627:fmbsr=1.6:i=67534_2971 on theBenchmark for (2971ds/67534Mi) % 183.56/26.04 % (1808017)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 183.56/26.04 % (1808017)Terminated due to inappropriate strategy. % 183.56/26.04 % (1808017)------------------------------ % 183.56/26.04 % (1808017)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 183.56/26.04 % (1808017)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 183.56/26.04 % (1808017)CaDiCaL version: 2.1.3 % 183.56/26.04 % (1808017)Termination reason: Inappropriate % 183.56/26.04 % (1808017)Time elapsed: 0.004 s % 183.56/26.04 % (1808017)Peak memory usage: 10 MB % 183.56/26.04 % (1808017)Instructions burned: 4 (million) % 183.56/26.04 % (1808017)------------------------------ % 183.56/26.04 % (1808017)------------------------------ % 183.56/26.04 % (1808019)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2295054822:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2971 on theBenchmark for (2971ds/4591Mi) % 183.56/26.04 % (1808004)Instruction limit reached! % 183.56/26.04 % (1808004)------------------------------ % 183.56/26.04 % (1808004)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 183.56/26.04 % (1808004)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 183.56/26.04 % (1808004)CaDiCaL version: 2.1.3 % 183.56/26.04 % (1808004)Termination reason: Instruction limit % 183.56/26.04 % (1808004)Termination phase: Saturation % 183.56/26.04 % (1808004)Time elapsed: 2.194 s % 183.56/26.04 % (1808004)Peak memory usage: 25 MB % 183.56/26.04 % (1808004)Instructions burned: 2253 (million) % 183.56/26.04 % (1808023)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1212864312:i=29340_2960 on theBenchmark for (2960ds/29340Mi) % 183.56/26.04 % (1807987)Instruction limit reached! % 183.56/26.04 % (1807987)------------------------------ % 183.56/26.04 % (1807987)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 183.56/26.04 % (1807987)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 183.56/26.04 % (1807987)CaDiCaL version: 2.1.3 % 183.56/26.04 % (1807987)Termination reason: Instruction limit % 213.17/30.24 % (1807987)Termination phase: Saturation % 213.17/30.24 % (1807987)Time elapsed: 3.409 s % 213.17/30.24 % (1807987)Peak memory usage: 32 MB % 213.17/30.24 % (1807987)Instructions burned: 3512 (million) % 213.17/30.24 % (1808025)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3067232111:i=5211_2953 on theBenchmark for (2953ds/5211Mi) % 213.17/30.24 % (1808019)Instruction limit reached! % 213.17/30.24 % (1808019)------------------------------ % 213.17/30.24 % (1808019)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 213.17/30.24 % (1808019)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.17/30.24 % (1808019)CaDiCaL version: 2.1.3 % 213.17/30.24 % (1808019)Termination reason: Instruction limit % 213.17/30.24 % (1808019)Termination phase: Saturation % 213.17/30.24 % (1808019)Time elapsed: 2.288 s % 213.17/30.24 % (1808019)Peak memory usage: 71 MB % 213.17/30.24 % (1808019)Instructions burned: 4593 (million) % 213.17/30.24 % (1808030)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3749154403:i=5497:nm=2_2948 on theBenchmark for (2948ds/5497Mi) % 213.17/30.24 % (1808030)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 213.17/30.24 % (1808030)Terminated due to inappropriate strategy. % 213.17/30.24 % (1808030)------------------------------ % 213.17/30.24 % (1808030)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 213.17/30.24 % (1808030)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.17/30.24 % (1808030)CaDiCaL version: 2.1.3 % 213.17/30.24 % (1808030)Termination reason: Inappropriate % 213.17/30.24 % (1808030)Time elapsed: 0.005 s % 213.17/30.24 % (1808030)Peak memory usage: 11 MB % 213.17/30.24 % (1808030)Instructions burned: 5 (million) % 213.17/30.24 % (1808030)------------------------------ % 213.17/30.24 % (1808030)------------------------------ % 213.17/30.24 % (1808033)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=4179450956:fmbsr=2:i=46332_2947 on theBenchmark for (2947ds/46332Mi) % 213.17/30.24 % (1808033)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 213.17/30.24 % (1808033)Terminated due to inappropriate strategy. % 213.17/30.24 % (1808033)------------------------------ % 213.17/30.24 % (1808033)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 213.17/30.24 % (1808033)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.17/30.24 % (1808033)CaDiCaL version: 2.1.3 % 213.17/30.24 % (1808033)Termination reason: Inappropriate % 213.17/30.24 % (1808033)Time elapsed: 0.004 s % 213.17/30.24 % (1808033)Peak memory usage: 11 MB % 213.17/30.24 % (1808033)Instructions burned: 4 (million) % 213.17/30.24 % (1808033)------------------------------ % 213.17/30.24 % (1808033)------------------------------ % 213.17/30.24 % (1808035)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=4141040711:i=14071_2947 on theBenchmark for (2947ds/14071Mi) % 213.17/30.24 % (1808035)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 213.17/30.24 % (1808035)Terminated due to inappropriate strategy. % 213.17/30.24 % (1808035)------------------------------ % 213.17/30.24 % (1808035)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 213.17/30.24 % (1808035)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.17/30.24 % (1808035)CaDiCaL version: 2.1.3 % 213.17/30.24 % (1808035)Termination reason: Inappropriate % 213.17/30.24 % (1808035)Time elapsed: 0.004 s % 213.17/30.24 % (1808035)Peak memory usage: 11 MB % 213.17/30.24 % (1808035)Instructions burned: 4 (million) % 213.17/30.24 % (1808035)------------------------------ % 213.17/30.24 % (1808035)------------------------------ % 213.17/30.24 % (1808037)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1003182659:i=22565:add=on:rawr=on_2947 on theBenchmark for (2947ds/22565Mi) % 213.17/30.24 % (1807999)Instruction limit reached! % 213.17/30.24 % (1807999)------------------------------ % 213.17/30.24 % (1807999)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 213.17/30.24 % (1807999)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.17/30.24 % (1807999)CaDiCaL version: 2.1.3 % 213.17/30.24 % (1807999)Termination reason: Instruction limit % 213.17/30.24 % (1807999)Termination phase: Saturation % 213.17/30.24 % (1807999)Time elapsed: 3.670 s % 213.17/30.24 % (1807999)Peak memory usage: 39 MB % 213.17/30.24 % (1807999)Instructions burned: 3773 (million) % 213.17/30.24 % (1808039)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=3847200181:i=8173:av=off_2946 on theBenchmark for (2946ds/8173Mi) % 213.17/30.24 % (1807972)Instruction limit reached! % 214.59/30.42 % (1807972)------------------------------ % 214.59/30.42 % (1807972)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 214.59/30.42 % (1807972)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 214.59/30.42 % (1807972)CaDiCaL version: 2.1.3 % 214.59/30.42 % (1807972)Termination reason: Instruction limit % 214.59/30.42 % (1807972)Termination phase: Saturation % 214.59/30.42 % (1807972)Time elapsed: 5.397 s % 214.59/30.42 % (1807972)Peak memory usage: 42 MB % 214.59/30.42 % (1807972)Instructions burned: 5114 (million) % 214.59/30.42 % (1808045)dis+10_16:1_sil=16000:random_seed=3459372932:i=9155:fsr=off_2937 on theBenchmark for (2937ds/9155Mi) % 214.59/30.42 % (1808025)Instruction limit reached! % 214.59/30.42 % (1808025)------------------------------ % 214.59/30.42 % (1808025)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 214.59/30.42 % (1808025)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 214.59/30.42 % (1808025)CaDiCaL version: 2.1.3 % 214.59/30.42 % (1808025)Termination reason: Instruction limit % 214.59/30.42 % (1808025)Termination phase: Saturation % 214.59/30.42 % (1808025)Time elapsed: 4.461 s % 214.59/30.42 % (1808025)Peak memory usage: 42 MB % 214.59/30.42 % (1808025)Instructions burned: 5212 (million) % 214.59/30.42 % (1808057)ott-3_8_sil=64000:random_seed=3571406929:i=20139:bs=on_2909 on theBenchmark for (2909ds/20139Mi) % 214.59/30.42 % (1808039)Instruction limit reached! % 214.59/30.42 % (1808039)------------------------------ % 214.59/30.42 % (1808039)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 214.59/30.42 % (1808039)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 214.59/30.42 % (1808039)CaDiCaL version: 2.1.3 % 214.59/30.42 % (1808039)Termination reason: Instruction limit % 214.59/30.42 % (1808039)Termination phase: Saturation % 214.59/30.42 % (1808039)Time elapsed: 8.539 s % 214.59/30.42 % (1808039)Peak memory usage: 61 MB % 214.59/30.42 % (1808039)Instructions burned: 8173 (million) % 214.59/30.42 % (1808063)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=1787977543:fmbsr=2:i=32576_2860 on theBenchmark for (2860ds/32576Mi) % 214.59/30.42 % (1808063)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 214.59/30.42 % (1808063)Terminated due to inappropriate strategy. % 214.59/30.42 % (1808063)------------------------------ % 214.59/30.42 % (1808063)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 214.59/30.42 % (1808063)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 214.59/30.42 % (1808063)CaDiCaL version: 2.1.3 % 214.59/30.42 % (1808063)Termination reason: Inappropriate % 214.59/30.42 % (1808063)Time elapsed: 0.006 s % 214.59/30.42 % (1808063)Peak memory usage: 10 MB % 214.59/30.42 % (1808063)Instructions burned: 5 (million) % 214.59/30.42 % (1808063)------------------------------ % 214.59/30.42 % (1808063)------------------------------ % 214.59/30.42 % (1808065)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=3632794024:i=11404_2860 on theBenchmark for (2860ds/11404Mi) % 214.59/30.42 % (1808045)Instruction limit reached! % 214.59/30.42 % (1808045)------------------------------ % 214.59/30.42 % (1808045)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 214.59/30.42 % (1808045)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 214.59/30.42 % (1808045)CaDiCaL version: 2.1.3 % 214.59/30.42 % (1808045)Termination reason: Instruction limit % 214.59/30.42 % (1808045)Termination phase: Saturation % 214.59/30.42 % (1808045)Time elapsed: 8.379 s % 214.59/30.42 % (1808045)Peak memory usage: 53 MB % 214.59/30.42 % (1808045)Instructions burned: 9155 (million) % 214.59/30.42 % (1808067)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=988484576:i=14134_2852 on theBenchmark for (2852ds/14134Mi) % 214.59/30.42 % (1808037)Instruction limit reached! % 214.59/30.42 % (1808037)------------------------------ % 214.59/30.42 % (1808037)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 214.59/30.42 % (1808037)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 214.59/30.42 % (1808037)CaDiCaL version: 2.1.3 % 214.59/30.42 % (1808037)Termination reason: Instruction limit % 214.59/30.42 % (1808037)Termination phase: Saturation % 214.59/30.42 % (1808037)Time elapsed: 16.483 s % 214.59/30.42 % (1808037)Peak memory usage: 63 MB % 214.59/30.42 % (1808037)Instructions burned: 22569 (million) % 214.59/30.42 % (1808075)dis+33_16_sil=32000:sac=on:random_seed=1312657858:i=15851:nm=0_2782 on theBenchmark for (2782ds/15851Mi) % 214.59/30.42 % (1808065)Instruction limit reached! % 214.59/30.42 % (1808065)------------------------------ % 214.59/30.42 % (1808065)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 285.10/40.33 % (1808065)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 285.10/40.33 % (1808065)CaDiCaL version: 2.1.3 % 285.10/40.33 % (1808065)Termination reason: Instruction limit % 285.10/40.33 % (1808065)Termination phase: Saturation % 285.10/40.33 % (1808065)Time elapsed: 11.855 s % 285.10/40.33 % (1808065)Peak memory usage: 71 MB % 285.10/40.33 % (1808065)Instructions burned: 11404 (million) % 285.10/40.33 % (1808079)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=4072684512:avsq=on:i=17627:add=on:amm=off_2741 on theBenchmark for (2741ds/17627Mi) % 285.10/40.33 % (1808023)Instruction limit reached! % 285.10/40.33 % (1808023)------------------------------ % 285.10/40.33 % (1808023)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 285.10/40.33 % (1808023)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 285.10/40.33 % (1808023)CaDiCaL version: 2.1.3 % 285.10/40.33 % (1808023)Termination reason: Instruction limit % 285.10/40.33 % (1808023)Termination phase: Saturation % 285.10/40.33 % (1808023)Time elapsed: 23.972 s % 285.10/40.33 % (1808023)Peak memory usage: 167 MB % 285.10/40.33 % (1808023)Instructions burned: 29340 (million) % 285.10/40.33 % (1808083)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=2572334912:s2a=on:i=53295_2720 on theBenchmark for (2720ds/53295Mi) % 285.10/40.33 % (1808057)Instruction limit reached! % 285.10/40.33 % (1808057)------------------------------ % 285.10/40.33 % (1808057)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 285.10/40.33 % (1808057)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 285.10/40.33 % (1808057)CaDiCaL version: 2.1.3 % 285.10/40.33 % (1808057)Termination reason: Instruction limit % 285.10/40.33 % (1808057)Termination phase: Saturation % 285.10/40.33 % (1808057)Time elapsed: 20.581 s % 285.10/40.33 % (1808057)Peak memory usage: 82 MB % 285.10/40.33 % (1808057)Instructions burned: 20140 (million) % 285.10/40.33 % (1808087)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=1918400337:i=26857:ins=20_2702 on theBenchmark for (2702ds/26857Mi) % 285.10/40.33 % (1808087)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 285.10/40.33 % (1808087)Terminated due to inappropriate strategy. % 285.10/40.33 % (1808087)------------------------------ % 285.10/40.33 % (1808087)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 285.10/40.33 % (1808087)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 285.10/40.33 % (1808087)CaDiCaL version: 2.1.3 % 285.10/40.33 % (1808087)Termination reason: Inappropriate % 285.10/40.33 % (1808087)Time elapsed: 0.003 s % 285.10/40.33 % (1808087)Peak memory usage: 10 MB % 285.10/40.33 % (1808087)Instructions burned: 4 (million) % 285.10/40.33 % (1808087)------------------------------ % 285.10/40.33 % (1808087)------------------------------ % 285.10/40.33 % (1808089)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=507464246:i=28120:bs=on:fsr=off_2702 on theBenchmark for (2702ds/28120Mi) % 285.10/40.33 % (1808067)Instruction limit reached! % 285.10/40.33 % (1808067)------------------------------ % 285.10/40.33 % (1808067)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 285.10/40.33 % (1808067)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 285.10/40.33 % (1808067)CaDiCaL version: 2.1.3 % 285.10/40.33 % (1808067)Termination reason: Instruction limit % 285.10/40.33 % (1808067)Termination phase: Saturation % 285.10/40.33 % (1808067)Time elapsed: 15.172 s % 285.10/40.33 % (1808067)Peak memory usage: 80 MB % 285.10/40.33 % (1808067)Instructions burned: 14134 (million) % 285.10/40.33 % (1808091)fmb+10_1_sil=256000:fmbss=7:random_seed=738940359:fmbsr=1.6:i=182295_2700 on theBenchmark for (2700ds/182295Mi) % 285.10/40.33 % (1808091)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 285.10/40.33 % (1808091)Terminated due to inappropriate strategy. % 285.10/40.33 % (1808091)------------------------------ % 285.10/40.33 % (1808091)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 285.10/40.33 % (1808091)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 285.10/40.33 % (1808091)CaDiCaL version: 2.1.3 % 285.10/40.33 % (1808091)Termination reason: Inappropriate % 285.10/40.33 % (1808091)Time elapsed: 0.005 s % 285.10/40.33 % (1808091)Peak memory usage: 10 MB % 285.10/40.33 % (1808091)Instructions burned: 4 (million) % 285.10/40.33 % (1808091)------------------------------ % 285.10/40.33 % (1808091)------------------------------ % 285.10/40.33 % (1808093)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seedTerminated % 300.49/42.53 % Vampire exiting % 300.49/42.54 Terminated %------------------------------------------------------------------------------