%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : NUM628+1 : TPTP v9.3.1. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n011.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 12:25:04 PM UTC 2026 % Result : Timeout 300.49s 42.83s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : NUM628+1 : TPTP v9.3.1. Released v4.0.0. % 0.00/0.07 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.12/0.39 % Computer : n011.cluster.edu % 0.12/0.39 % Model : x86_64 x86_64 % 0.12/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.39 % Memory : 8046.5625MB % 0.12/0.39 % OS : Linux 6.8.0-71-generic % 0.12/0.39 % CPULimit : 300 % 0.12/0.39 % WCLimit : 300 % 0.12/0.39 % DateTime : Sun Sep 27 20:50:31 UTC 2026 % 0.12/0.40 % CPUTime : % 0.12/0.40 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.12/0.42 Running first-order model finding % 0.12/0.42 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 16.79/2.81 % (2745149)Will run a generic schedule for satisfiability detection. % 16.79/2.81 % (2745155)% WARNING: option uhcvi not known. % 16.79/2.81 % (2745155)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2647006933:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 16.79/2.81 % (2745154)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2297258989_2999 on theBenchmark for (2999ds/0Mi) % 16.79/2.81 % (2745156)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2962236202:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 16.79/2.81 % (2745157)dis+10_1_sil=32000:sp=arity:random_seed=2318444762:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 16.79/2.81 % (2745159)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=704093204:i=131_2999 on theBenchmark for (2999ds/131Mi) % 16.79/2.81 % (2745158)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2183660276:i=116_2999 on theBenchmark for (2999ds/116Mi) % 16.79/2.81 % (2745160)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1322249315:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 16.79/2.81 % TRYING [1] % 16.79/2.81 % TRYING [2] % 16.79/2.81 % TRYING [3] % 16.79/2.81 % TRYING [4] % 16.79/2.81 % (2745157)Instruction limit reached! % 16.79/2.81 % (2745157)------------------------------ % 16.79/2.81 % (2745157)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.79/2.81 % (2745157)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.79/2.81 % (2745157)CaDiCaL version: 2.1.3 % 16.79/2.81 % (2745157)Termination reason: Instruction limit % 16.79/2.81 % (2745157)Termination phase: Saturation % 16.79/2.81 % (2745157)Time elapsed: 0.070 s % 16.79/2.81 % (2745157)Peak memory usage: 13 MB % 16.79/2.81 % (2745157)Instructions burned: 108 (million) % 16.79/2.81 % (2745158)Instruction limit reached! % 16.79/2.81 % (2745158)------------------------------ % 16.79/2.81 % (2745158)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.79/2.81 % (2745158)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.79/2.81 % (2745158)CaDiCaL version: 2.1.3 % 16.79/2.81 % (2745158)Termination reason: Instruction limit % 16.79/2.81 % (2745158)Termination phase: Saturation % 16.79/2.81 % (2745158)Time elapsed: 0.075 s % 16.79/2.81 % (2745158)Peak memory usage: 13 MB % 16.79/2.81 % (2745158)Instructions burned: 117 (million) % 16.79/2.81 % (2745159)Instruction limit reached! % 16.79/2.81 % (2745159)------------------------------ % 16.79/2.81 % (2745159)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.79/2.81 % (2745159)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.79/2.81 % (2745159)CaDiCaL version: 2.1.3 % 16.79/2.81 % (2745159)Termination reason: Instruction limit % 16.79/2.81 % (2745159)Termination phase: Saturation % 16.79/2.81 % (2745159)Time elapsed: 0.080 s % 16.79/2.81 % (2745159)Peak memory usage: 13 MB % 16.79/2.81 % (2745159)Instructions burned: 133 (million) % 16.79/2.81 % (2745168)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=4105810587:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi) % 16.79/2.81 % (2745169)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1006350168:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi) % 16.79/2.81 % (2745170)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=2541466946:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 16.79/2.81 % TRYING [1] % 16.79/2.81 % TRYING [2] % 16.79/2.81 % (2745160)Instruction limit reached! % 16.79/2.81 % (2745160)------------------------------ % 16.79/2.81 % (2745160)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.79/2.81 % (2745160)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.79/2.81 % (2745160)CaDiCaL version: 2.1.3 % 16.79/2.81 % (2745160)Termination reason: Instruction limit % 16.79/2.81 % (2745160)Termination phase: Saturation % 16.79/2.81 % (2745160)Time elapsed: 0.112 s % 16.79/2.81 % (2745160)Peak memory usage: 15 MB % 16.79/2.81 % (2745160)Instructions burned: 160 (million) % 16.79/2.81 % TRYING [3] % 16.79/2.81 % TRYING [5] % 16.79/2.81 % (2745174)ott-21_1_sil=16000:fs=off:random_seed=1957008006:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 16.79/2.81 % TRYING [4] % 16.79/2.81 % (2745169)Instruction limit reached! % 16.79/2.81 % (2745169)------------------------------ % 16.79/2.81 % (2745169)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 50.13/7.51 % (2745169)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 50.13/7.51 % (2745169)CaDiCaL version: 2.1.3 % 50.13/7.51 % (2745169)Termination reason: Instruction limit % 50.13/7.51 % (2745169)Termination phase: Saturation % 50.13/7.51 % (2745169)Time elapsed: 0.087 s % 50.13/7.51 % (2745169)Peak memory usage: 14 MB % 50.13/7.51 % (2745169)Instructions burned: 131 (million) % 50.13/7.51 % (2745176)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3821273496:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi) % 50.13/7.51 % TRYING [5] % 50.13/7.51 % (2745174)Instruction limit reached! % 50.13/7.51 % (2745174)------------------------------ % 50.13/7.51 % (2745174)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 50.13/7.51 % (2745174)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 50.13/7.51 % (2745174)CaDiCaL version: 2.1.3 % 50.13/7.51 % (2745174)Termination reason: Instruction limit % 50.13/7.51 % (2745174)Termination phase: Saturation % 50.13/7.51 % (2745174)Time elapsed: 0.104 s % 50.13/7.51 % (2745174)Peak memory usage: 13 MB % 50.13/7.51 % (2745174)Instructions burned: 182 (million) % 50.13/7.51 % (2745178)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2104307193:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi) % 50.13/7.51 % TRYING [1] % 50.13/7.51 % TRYING [2] % 50.13/7.51 % TRYING [6] % 50.13/7.51 % TRYING [3] % 50.13/7.51 % (2745168)Instruction limit reached! % 50.13/7.51 % (2745168)------------------------------ % 50.13/7.51 % (2745168)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 50.13/7.51 % (2745168)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 50.13/7.51 % (2745168)CaDiCaL version: 2.1.3 % 50.13/7.51 % (2745168)Termination reason: Instruction limit % 50.13/7.51 % (2745168)Termination phase: Finite model building constraint generation % 50.13/7.51 % (2745168)Time elapsed: 0.291 s % 50.13/7.51 % (2745168)Peak memory usage: 35 MB % 50.13/7.51 % (2745168)Instructions burned: 715 (million) % 50.13/7.51 % (2745180)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=329879096:i=1179_2995 on theBenchmark for (2995ds/1179Mi) % 50.13/7.51 % TRYING [4] % 50.13/7.51 % (2745170)Instruction limit reached! % 50.13/7.51 % (2745170)------------------------------ % 50.13/7.51 % (2745170)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 50.13/7.51 % (2745170)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 50.13/7.51 % (2745170)CaDiCaL version: 2.1.3 % 50.13/7.51 % (2745170)Termination reason: Instruction limit % 50.13/7.51 % (2745170)Termination phase: Saturation % 50.13/7.51 % (2745170)Time elapsed: 0.407 s % 50.13/7.51 % (2745170)Peak memory usage: 20 MB % 50.13/7.51 % (2745170)Instructions burned: 685 (million) % 50.13/7.51 % (2745182)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2934914145:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi) % 50.13/7.51 % (2745176)Instruction limit reached! % 50.13/7.51 % (2745176)------------------------------ % 50.13/7.51 % (2745176)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 50.13/7.51 % (2745176)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 50.13/7.51 % (2745176)CaDiCaL version: 2.1.3 % 50.13/7.51 % (2745176)Termination reason: Instruction limit % 50.13/7.51 % (2745176)Termination phase: Saturation % 50.13/7.51 % (2745176)Time elapsed: 0.333 s % 50.13/7.51 % (2745176)Peak memory usage: 15 MB % 50.13/7.51 % (2745176)Instructions burned: 477 (million) % 50.13/7.51 % (2745184)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=3125402021:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi) % 50.13/7.51 % (2745178)Instruction limit reached! % 50.13/7.51 % (2745178)------------------------------ % 50.13/7.51 % (2745178)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 50.13/7.51 % (2745178)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 50.13/7.51 % (2745178)CaDiCaL version: 2.1.3 % 50.13/7.51 % (2745178)Termination reason: Instruction limit % 50.13/7.51 % (2745178)Termination phase: Finite model building SAT solving % 50.13/7.51 % (2745178)Time elapsed: 0.359 s % 50.13/7.51 % (2745178)Peak memory usage: 22 MB % 50.13/7.51 % (2745178)Instructions burned: 865 (million) % 50.13/7.51 % (2745186)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=4215810598:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi) % 50.13/7.51 % TRYING [7] % 50.13/7.51 % TRYING [14] % 50.13/7.51 % (2745182)Instruction limit reached! % 102.60/15.00 % (2745182)------------------------------ % 102.60/15.00 % (2745182)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 102.60/15.00 % (2745182)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 102.60/15.00 % (2745182)CaDiCaL version: 2.1.3 % 102.60/15.00 % (2745182)Termination reason: Instruction limit % 102.60/15.00 % (2745182)Termination phase: Finite model building constraint generation % 102.60/15.00 % (2745182)Time elapsed: 0.394 s % 102.60/15.00 % (2745182)Peak memory usage: 94 MB % 102.60/15.00 % (2745182)Instructions burned: 890 (million) % 102.60/15.00 % (2745188)fmb+10_1_sil=64000:random_seed=3390843101:i=22061:nm=2:gsp=on_2990 on theBenchmark for (2990ds/22061Mi) % 102.60/15.00 % TRYING [1] % 102.60/15.00 % TRYING [2] % 102.60/15.00 % TRYING [3] % 102.60/15.00 % (2745184)Instruction limit reached! % 102.60/15.00 % (2745184)------------------------------ % 102.60/15.00 % (2745184)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 102.60/15.00 % (2745184)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 102.60/15.00 % (2745184)CaDiCaL version: 2.1.3 % 102.60/15.00 % (2745184)Termination reason: Instruction limit % 102.60/15.00 % (2745184)Termination phase: Saturation % 102.60/15.00 % (2745184)Time elapsed: 0.444 s % 102.60/15.00 % (2745184)Peak memory usage: 18 MB % 102.60/15.00 % (2745184)Instructions burned: 693 (million) % 102.60/15.00 % (2745190)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1313061631:i=9515:nm=5_2989 on theBenchmark for (2989ds/9515Mi) % 102.60/15.00 % TRYING [20] % 102.60/15.00 % TRYING [4] % 102.60/15.00 % (2745186)Instruction limit reached! % 102.60/15.00 % (2745186)------------------------------ % 102.60/15.00 % (2745186)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 102.60/15.00 % (2745186)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 102.60/15.00 % (2745186)CaDiCaL version: 2.1.3 % 102.60/15.00 % (2745186)Termination reason: Instruction limit % 102.60/15.00 % (2745186)Termination phase: Saturation % 102.60/15.00 % (2745186)Time elapsed: 0.488 s % 102.60/15.00 % (2745186)Peak memory usage: 21 MB % 102.60/15.00 % (2745186)Instructions burned: 879 (million) % 102.60/15.00 % (2745192)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2062685367:fmbsr=1.7:i=920_2988 on theBenchmark for (2988ds/920Mi) % 102.60/15.00 % (2745180)Instruction limit reached! % 102.60/15.00 % (2745180)------------------------------ % 102.60/15.00 % (2745180)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 102.60/15.00 % (2745180)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 102.60/15.00 % (2745180)CaDiCaL version: 2.1.3 % 102.60/15.00 % (2745180)Termination reason: Instruction limit % 102.60/15.00 % (2745180)Termination phase: Saturation % 102.60/15.00 % (2745180)Time elapsed: 0.748 s % 102.60/15.00 % (2745180)Peak memory usage: 25 MB % 102.60/15.00 % (2745180)Instructions burned: 1179 (million) % 102.60/15.00 % TRYING [8] % 102.60/15.00 % (2745194)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3289391262:i=5131_2988 on theBenchmark for (2988ds/5131Mi) % 102.60/15.00 % TRYING [5] % 102.60/15.00 % (2745192)Instruction limit reached! % 102.60/15.00 % (2745192)------------------------------ % 102.60/15.00 % (2745192)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 102.60/15.00 % (2745192)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 102.60/15.00 % (2745192)CaDiCaL version: 2.1.3 % 102.60/15.00 % (2745192)Termination reason: Instruction limit % 102.60/15.00 % (2745192)Termination phase: Finite model building constraint generation % 102.60/15.00 % (2745192)Time elapsed: 0.353 s % 102.60/15.00 % (2745192)Peak memory usage: 79 MB % 102.60/15.00 % (2745192)Instructions burned: 922 (million) % 102.60/15.00 % (2745196)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1626447207:i=1472:ins=7:fdi=8:gsp=on_2984 on theBenchmark for (2984ds/1472Mi) % 102.60/15.00 % TRYING [8] % 102.60/15.00 % TRYING [6] % 102.60/15.00 % (2745196)Instruction limit reached! % 102.60/15.00 % (2745196)------------------------------ % 102.60/15.00 % (2745196)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 102.60/15.00 % (2745196)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 102.60/15.00 % (2745196)CaDiCaL version: 2.1.3 % 102.60/15.00 % (2745196)Termination reason: Instruction limit % 102.60/15.00 % (2745196)Termination phase: Saturation % 102.60/15.00 % (2745196)Time elapsed: 0.789 s % 102.60/15.00 % (2745196)Peak memory usage: 28 MB % 102.60/15.00 % (2745196)Instructions burned: 1474 (million) % 102.60/15.00 % (2745198)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=432748599:i=6324_2976 on theBenchmark for (2976ds/6324Mi) % 284.90/40.65 % TRYING [77] % 284.90/40.65 % TRYING [7] % 284.90/40.65 % TRYING [9] % 284.90/40.65 % (2745194)Instruction limit reached! % 284.90/40.65 % (2745194)------------------------------ % 284.90/40.65 % (2745194)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 284.90/40.65 % (2745194)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.90/40.65 % (2745194)CaDiCaL version: 2.1.3 % 284.90/40.65 % (2745194)Termination reason: Instruction limit % 284.90/40.65 % (2745194)Termination phase: Saturation % 284.90/40.65 % (2745194)Time elapsed: 2.946 s % 284.90/40.65 % (2745194)Peak memory usage: 38 MB % 284.90/40.65 % (2745194)Instructions burned: 5133 (million) % 284.90/40.65 % (2745200)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=758837550:fmbsr=2.30978:i=2174_2958 on theBenchmark for (2958ds/2174Mi) % 284.90/40.65 % (2745190)Instruction limit reached! % 284.90/40.65 % (2745190)------------------------------ % 284.90/40.65 % (2745190)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 284.90/40.65 % (2745190)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.90/40.65 % (2745190)CaDiCaL version: 2.1.3 % 284.90/40.65 % (2745190)Termination reason: Instruction limit % 284.90/40.65 % (2745190)Termination phase: Finite model building constraint generation % 284.90/40.65 % (2745190)Time elapsed: 3.163 s % 284.90/40.65 % (2745190)Peak memory usage: 549 MB % 284.90/40.65 % (2745190)Instructions burned: 9518 (million) % 284.90/40.65 % TRYING [16] % 284.90/40.65 % (2745202)ott-2_1_sil=16000:newcnf=on:random_seed=720156984:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2957 on theBenchmark for (2957ds/869Mi) % 284.90/40.65 % (2745198)Instruction limit reached! % 284.90/40.65 % (2745198)------------------------------ % 284.90/40.65 % (2745198)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 284.90/40.65 % (2745198)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.90/40.65 % (2745198)CaDiCaL version: 2.1.3 % 284.90/40.65 % (2745198)Termination reason: Instruction limit % 284.90/40.65 % (2745198)Termination phase: Finite model building constraint generation % 284.90/40.65 % (2745198)Time elapsed: 2.399 s % 284.90/40.65 % (2745198)Peak memory usage: 523 MB % 284.90/40.65 % (2745198)Instructions burned: 6327 (million) % 284.90/40.65 % (2745202)Instruction limit reached! % 284.90/40.65 % (2745202)------------------------------ % 284.90/40.65 % (2745202)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 284.90/40.65 % (2745202)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.90/40.65 % (2745202)CaDiCaL version: 2.1.3 % 284.90/40.65 % (2745202)Termination reason: Instruction limit % 284.90/40.65 % (2745202)Termination phase: Saturation % 284.90/40.65 % (2745202)Time elapsed: 0.527 s % 284.90/40.65 % (2745202)Peak memory usage: 21 MB % 284.90/40.65 % (2745202)Instructions burned: 870 (million) % 284.90/40.65 % (2745204)ott+10_1_sil=32000:tgt=ground:random_seed=2879475970:i=5114:av=off_2951 on theBenchmark for (2951ds/5114Mi) % 284.90/40.65 % (2745205)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=169796648:i=54282_2951 on theBenchmark for (2951ds/54282Mi) % 284.90/40.65 % TRYING [1] % 284.90/40.65 % TRYING [2] % 284.90/40.65 % TRYING [3] % 284.90/40.65 % TRYING [4] % 284.90/40.65 % (2745200)Instruction limit reached! % 284.90/40.65 % (2745200)------------------------------ % 284.90/40.65 % (2745200)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 284.90/40.65 % (2745200)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.90/40.65 % (2745200)CaDiCaL version: 2.1.3 % 284.90/40.65 % (2745200)Termination reason: Instruction limit % 284.90/40.65 % (2745200)Termination phase: Finite model building constraint generation % 284.90/40.65 % (2745200)Time elapsed: 0.770 s % 284.90/40.65 % (2745200)Peak memory usage: 133 MB % 284.90/40.65 % (2745200)Instructions burned: 2174 (million) % 284.90/40.65 % TRYING [5] % 284.90/40.65 % (2745208)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1825693171:i=3512:aac=none_2950 on theBenchmark for (2950ds/3512Mi) % 284.90/40.65 % TRYING [6] % 284.90/40.65 % TRYING [7] % 284.90/40.65 % TRYING [8] % 284.90/40.65 % TRYING [8] % 284.90/40.65 % (2745208)Instruction limit reached! % 284.90/40.65 % (2745208)------------------------------ % 284.90/40.65 % (2745208)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 284.90/40.65 % (2745208)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.90/40.65 % (2745208)CaDiCaL version: 2.1.3 % 284.90/40.65 % (2745208)Termination reason: Instruction limit % 284.90/40.65 % (2745208)Termination phase: Saturation % 284.90/40.65 % (2745208)Time elapsed: 2.069 s % 284.90/40.65 % (2745208)Peak memory usage: 32 MB % 284.90/40.65 % (2745208)Instructions burned: 3512 (million) % 284.90/40.65 % (2745210)dis+21_1_Terminated % 300.49/42.83 % Vampire exiting %------------------------------------------------------------------------------