%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : TOP044+4 : TPTP v9.3.1. Released v3.4.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n017.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 02:34:29 PM UTC 2026 % Result : Timeout 300.15s 43.84s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : TOP044+4 : TPTP v9.3.1. Released v3.4.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.11/0.19 % Computer : n017.cluster.edu % 0.11/0.19 % Model : x86_64 x86_64 % 0.11/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.19 % Memory : 8046.5625MB % 0.11/0.19 % OS : Linux 6.8.0-71-generic % 0.11/0.19 % CPULimit : 300 % 0.11/0.19 % WCLimit : 300 % 0.11/0.19 % DateTime : Mon Sep 28 19:00:04 UTC 2026 % 0.11/0.20 % CPUTime : % 0.11/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.11/0.22 Running first-order model finding % 0.11/0.22 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 % 31.26/5.94 % (3897235)Will run a generic schedule for satisfiability detection. % 31.26/5.94 % (3897241)% WARNING: option uhcvi not known. % 31.26/5.94 % (3897246)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3396188035:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2985 on theBenchmark for (2985ds/159Mi) % 31.26/5.94 % (3897240)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1018497348_2985 on theBenchmark for (2985ds/0Mi) % 31.26/5.94 % (3897241)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3977059052:i=135531:add=off:rawr=on_2985 on theBenchmark for (2985ds/135531Mi) % 31.26/5.94 % (3897242)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3315279449:i=88024:add=on:rawr=on_2985 on theBenchmark for (2985ds/88024Mi) % 31.26/5.94 % (3897243)dis+10_1_sil=32000:sp=arity:random_seed=4260621889:i=103:fgj=on_2985 on theBenchmark for (2985ds/103Mi) % 31.26/5.94 % (3897244)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=972575112:i=116_2985 on theBenchmark for (2985ds/116Mi) % 31.26/5.94 % (3897245)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=24291543:i=131_2985 on theBenchmark for (2985ds/131Mi) % 31.26/5.94 % (3897246)Instruction limit reached! % 31.26/5.94 % (3897246)------------------------------ % 31.26/5.94 % (3897246)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 31.26/5.94 % (3897246)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.26/5.94 % (3897246)CaDiCaL version: 2.1.3 % 31.26/5.94 % (3897246)Termination reason: Instruction limit % 31.26/5.94 % (3897246)Termination phase: Preprocessing 1 % 31.26/5.94 % (3897246)Time elapsed: 0.067 s % 31.26/5.94 % (3897246)Peak memory usage: 129 MB % 31.26/5.94 % (3897246)Instructions burned: 160 (million) % 31.26/5.94 % (3897243)Instruction limit reached! % 31.26/5.94 % (3897243)------------------------------ % 31.26/5.94 % (3897243)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 31.26/5.94 % (3897243)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.26/5.94 % (3897243)CaDiCaL version: 2.1.3 % 31.26/5.94 % (3897243)Termination reason: Instruction limit % 31.26/5.94 % (3897243)Termination phase: Preprocessing 1 % 31.26/5.94 % (3897243)Time elapsed: 0.074 s % 31.26/5.94 % (3897243)Peak memory usage: 129 MB % 31.26/5.94 % (3897243)Instructions burned: 103 (million) % 31.26/5.94 % (3897254)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3108456916:i=714:nm=2_2984 on theBenchmark for (2984ds/714Mi) % 31.26/5.94 % (3897244)Instruction limit reached! % 31.26/5.94 % (3897244)------------------------------ % 31.26/5.94 % (3897244)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 31.26/5.94 % (3897244)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.26/5.94 % (3897244)CaDiCaL version: 2.1.3 % 31.26/5.94 % (3897244)Termination reason: Instruction limit % 31.26/5.94 % (3897244)Termination phase: Preprocessing 1 % 31.26/5.94 % (3897244)Time elapsed: 0.090 s % 31.26/5.94 % (3897244)Peak memory usage: 129 MB % 31.26/5.94 % (3897244)Instructions burned: 116 (million) % 31.26/5.94 % (3897245)Instruction limit reached! % 31.26/5.94 % (3897245)------------------------------ % 31.26/5.94 % (3897245)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 31.26/5.94 % (3897245)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.26/5.94 % (3897245)CaDiCaL version: 2.1.3 % 31.26/5.94 % (3897245)Termination reason: Instruction limit % 31.26/5.94 % (3897245)Termination phase: Preprocessing 1 % 31.26/5.94 % (3897245)Time elapsed: 0.093 s % 31.26/5.94 % (3897245)Peak memory usage: 129 MB % 31.26/5.94 % (3897245)Instructions burned: 131 (million) % 31.26/5.94 % (3897256)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=758668250:i=131:bd=preordered:fsd=on_2984 on theBenchmark for (2984ds/131Mi) % 31.26/5.94 % (3897257)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=1628825531:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2983 on theBenchmark for (2983ds/684Mi) % 31.26/5.94 % (3897259)ott-21_1_sil=16000:fs=off:random_seed=1864060177:i=180:av=off:fsr=off_2983 on theBenchmark for (2983ds/180Mi) % 31.26/5.94 % (3897256)Instruction limit reached! % 31.26/5.94 % (3897256)------------------------------ % 31.26/5.94 % (3897256)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 31.26/5.94 % (3897256)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 64.61/10.65 % (3897256)CaDiCaL version: 2.1.3 % 64.61/10.65 % (3897256)Termination reason: Instruction limit % 64.61/10.65 % (3897256)Termination phase: Preprocessing 1 % 64.61/10.65 % (3897256)Time elapsed: 0.097 s % 64.61/10.65 % (3897256)Peak memory usage: 129 MB % 64.61/10.65 % (3897256)Instructions burned: 131 (million) % 64.61/10.65 % (3897262)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1613170870:i=477:bd=all_2982 on theBenchmark for (2982ds/477Mi) % 64.61/10.65 % (3897259)Instruction limit reached! % 64.61/10.65 % (3897259)------------------------------ % 64.61/10.65 % (3897259)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 64.61/10.65 % (3897259)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 64.61/10.65 % (3897259)CaDiCaL version: 2.1.3 % 64.61/10.65 % (3897259)Termination reason: Instruction limit % 64.61/10.65 % (3897259)Termination phase: Preprocessing 1 % 64.61/10.65 % (3897259)Time elapsed: 0.130 s % 64.61/10.65 % (3897259)Peak memory usage: 129 MB % 64.61/10.65 % (3897259)Instructions burned: 181 (million) % 64.61/10.65 % (3897264)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2825972250:fmbsr=1.3:i=865:ins=25_2982 on theBenchmark for (2982ds/865Mi) % 64.61/10.65 % (3897254)Instruction limit reached! % 64.61/10.65 % (3897254)------------------------------ % 64.61/10.65 % (3897254)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 64.61/10.65 % (3897254)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 64.61/10.65 % (3897254)CaDiCaL version: 2.1.3 % 64.61/10.65 % (3897254)Termination reason: Instruction limit % 64.61/10.65 % (3897254)Termination phase: Preprocessing 2 % 64.61/10.65 % (3897254)Time elapsed: 0.331 s % 64.61/10.65 % (3897254)Peak memory usage: 140 MB % 64.61/10.65 % (3897254)Instructions burned: 715 (million) % 64.61/10.65 % (3897266)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=4280013499:i=1179_2980 on theBenchmark for (2980ds/1179Mi) % 64.61/10.65 % (3897262)Instruction limit reached! % 64.61/10.65 % (3897262)------------------------------ % 64.61/10.65 % (3897262)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 64.61/10.65 % (3897262)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 64.61/10.65 % (3897262)CaDiCaL version: 2.1.3 % 64.61/10.65 % (3897262)Termination reason: Instruction limit % 64.61/10.65 % (3897262)Termination phase: Preprocessing 1 % 64.61/10.65 % (3897262)Time elapsed: 0.331 s % 64.61/10.65 % (3897262)Peak memory usage: 130 MB % 64.61/10.65 % (3897262)Instructions burned: 477 (million) % 64.61/10.65 % (3897268)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3684362738:i=889:ins=1_2979 on theBenchmark for (2979ds/889Mi) % 64.61/10.65 % (3897257)Instruction limit reached! % 64.61/10.65 % (3897257)------------------------------ % 64.61/10.65 % (3897257)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 64.61/10.65 % (3897257)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 64.61/10.65 % (3897257)CaDiCaL version: 2.1.3 % 64.61/10.65 % (3897257)Termination reason: Instruction limit % 64.61/10.65 % (3897257)Termination phase: Preprocessing 1 % 64.61/10.65 % (3897257)Time elapsed: 0.486 s % 64.61/10.65 % (3897257)Peak memory usage: 130 MB % 64.61/10.65 % (3897257)Instructions burned: 685 (million) % 64.61/10.65 % (3897270)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=2725985855:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2978 on theBenchmark for (2978ds/692Mi) % 64.61/10.65 % (3897264)Instruction limit reached! % 64.61/10.65 % (3897264)------------------------------ % 64.61/10.65 % (3897264)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 64.61/10.65 % (3897264)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 64.61/10.65 % (3897264)CaDiCaL version: 2.1.3 % 64.61/10.65 % (3897264)Termination reason: Instruction limit % 64.61/10.65 % (3897264)Termination phase: Preprocessing 2 % 64.61/10.65 % (3897264)Time elapsed: 0.646 s % 64.61/10.65 % (3897264)Peak memory usage: 188 MB % 64.61/10.65 % (3897264)Instructions burned: 865 (million) % 64.61/10.65 % (3897272)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=4248049200:i=879:kws=inv_precedence:fsr=off_2975 on theBenchmark for (2975ds/879Mi) % 64.61/10.65 % (3897266)Instruction limit reached! % 64.61/10.65 % (3897266)------------------------------ % 64.61/10.65 % (3897266)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 64.61/10.65 % (3897266)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 125.61/19.22 % (3897266)CaDiCaL version: 2.1.3 % 125.61/19.22 % (3897266)Termination reason: Instruction limit % 125.61/19.22 % (3897266)Termination phase: Naming % 125.61/19.22 % (3897266)Time elapsed: 0.577 s % 125.61/19.22 % (3897266)Peak memory usage: 202 MB % 125.61/19.22 % (3897266)Instructions burned: 1180 (million) % 125.61/19.22 % (3897274)fmb+10_1_sil=64000:random_seed=1229764831:i=22061:nm=2:gsp=on_2974 on theBenchmark for (2974ds/22061Mi) % 125.61/19.22 % (3897270)Instruction limit reached! % 125.61/19.22 % (3897270)------------------------------ % 125.61/19.22 % (3897270)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 125.61/19.22 % (3897270)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 125.61/19.22 % (3897270)CaDiCaL version: 2.1.3 % 125.61/19.22 % (3897270)Termination reason: Instruction limit % 125.61/19.22 % (3897270)Termination phase: Preprocessing 1 % 125.61/19.22 % (3897270)Time elapsed: 0.514 s % 125.61/19.22 % (3897270)Peak memory usage: 130 MB % 125.61/19.22 % (3897270)Instructions burned: 693 (million) % 125.61/19.22 % (3897276)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2618040667:i=9515:nm=5_2973 on theBenchmark for (2973ds/9515Mi) % 125.61/19.22 % (3897268)Instruction limit reached! % 125.61/19.22 % (3897268)------------------------------ % 125.61/19.22 % (3897268)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 125.61/19.22 % (3897268)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 125.61/19.22 % (3897268)CaDiCaL version: 2.1.3 % 125.61/19.22 % (3897268)Termination reason: Instruction limit % 125.61/19.22 % (3897268)Termination phase: Preprocessing 2 % 125.61/19.22 % (3897268)Time elapsed: 0.731 s % 125.61/19.22 % (3897268)Peak memory usage: 175 MB % 125.61/19.22 % (3897268)Instructions burned: 889 (million) % 125.61/19.22 % (3897278)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3132795878:fmbsr=1.7:i=920_2971 on theBenchmark for (2971ds/920Mi) % 125.61/19.22 % (3897272)Instruction limit reached! % 125.61/19.22 % (3897272)------------------------------ % 125.61/19.22 % (3897272)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 125.61/19.22 % (3897272)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 125.61/19.22 % (3897272)CaDiCaL version: 2.1.3 % 125.61/19.22 % (3897272)Termination reason: Instruction limit % 125.61/19.22 % (3897272)Termination phase: Preprocessing 2 % 125.61/19.22 % (3897272)Time elapsed: 0.751 s % 125.61/19.22 % (3897272)Peak memory usage: 191 MB % 125.61/19.22 % (3897272)Instructions burned: 879 (million) % 125.61/19.22 % (3897281)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2489219145:i=5131_2967 on theBenchmark for (2967ds/5131Mi) % 125.61/19.22 % (3897278)Instruction limit reached! % 125.61/19.22 % (3897278)------------------------------ % 125.61/19.22 % (3897278)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 125.61/19.22 % (3897278)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 125.61/19.22 % (3897278)CaDiCaL version: 2.1.3 % 125.61/19.22 % (3897278)Termination reason: Instruction limit % 125.61/19.22 % (3897278)Termination phase: Preprocessing 2 % 125.61/19.22 % (3897278)Time elapsed: 0.740 s % 125.61/19.22 % (3897278)Peak memory usage: 181 MB % 125.61/19.22 % (3897278)Instructions burned: 920 (million) % 125.61/19.22 % (3897283)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2438777474:i=1472:ins=7:fdi=8:gsp=on_2963 on theBenchmark for (2963ds/1472Mi) % 125.61/19.22 % (3897283)Instruction limit reached! % 125.61/19.22 % (3897283)------------------------------ % 125.61/19.22 % (3897283)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 125.61/19.22 % (3897283)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 125.61/19.22 % (3897283)CaDiCaL version: 2.1.3 % 125.61/19.22 % (3897283)Termination reason: Instruction limit % 125.61/19.22 % (3897283)Termination phase: Preprocessing 3 % 125.61/19.22 % (3897283)Time elapsed: 1.051 s % 125.61/19.22 % (3897283)Peak memory usage: 208 MB % 125.61/19.22 % (3897283)Instructions burned: 1474 (million) % 125.61/19.22 % (3897285)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2577156642:i=6324_2952 on theBenchmark for (2952ds/6324Mi) % 125.61/19.22 % (3897281)Instruction limit reached! % 125.61/19.22 % (3897281)------------------------------ % 125.61/19.22 % (3897281)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 125.61/19.22 % (3897281)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 125.61/19.22 % (3897281)CaDiCaL version: 2.1.3 % 125.61/19.22 % (3897281)Termination reason: Instruction limit % 125.61/19.22 % (3897281)Termination phase: NewCNF % 215.00/31.86 % (3897281)Time elapsed: 2.435 s % 215.00/31.86 % (3897281)Peak memory usage: 262 MB % 215.00/31.86 % (3897281)Instructions burned: 5134 (million) % 215.00/31.86 % (3897287)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1168461021:fmbsr=2.30978:i=2174_2942 on theBenchmark for (2942ds/2174Mi) % 215.00/31.86 % (3897287)Instruction limit reached! % 215.00/31.86 % (3897287)------------------------------ % 215.00/31.86 % (3897287)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 215.00/31.86 % (3897287)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 215.00/31.86 % (3897287)CaDiCaL version: 2.1.3 % 215.00/31.86 % (3897287)Termination reason: Instruction limit % 215.00/31.86 % (3897287)Termination phase: Preprocessing 3 % 215.00/31.86 % (3897287)Time elapsed: 1.428 s % 215.00/31.86 % (3897287)Peak memory usage: 232 MB % 215.00/31.86 % (3897287)Instructions burned: 2174 (million) % 215.00/31.86 % (3897289)ott-2_1_sil=16000:newcnf=on:random_seed=1155230396:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2927 on theBenchmark for (2927ds/869Mi) % 215.00/31.86 % (3897276)Instruction limit reached! % 215.00/31.86 % (3897276)------------------------------ % 215.00/31.86 % (3897276)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 215.00/31.86 % (3897276)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 215.00/31.86 % (3897276)CaDiCaL version: 2.1.3 % 215.00/31.86 % (3897276)Termination reason: Instruction limit % 215.00/31.86 % (3897276)Termination phase: Property scanning % 215.00/31.86 % (3897276)Time elapsed: 4.755 s % 215.00/31.86 % (3897276)Peak memory usage: 321 MB % 215.00/31.86 % (3897276)Instructions burned: 9518 (million) % 215.00/31.86 % (3897291)ott+10_1_sil=32000:tgt=ground:random_seed=255151654:i=5114:av=off_2925 on theBenchmark for (2925ds/5114Mi) % 215.00/31.86 % (3897274)Instruction limit reached! % 215.00/31.86 % (3897274)------------------------------ % 215.00/31.86 % (3897274)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 215.00/31.86 % (3897274)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 215.00/31.86 % (3897274)CaDiCaL version: 2.1.3 % 215.00/31.86 % (3897274)Termination reason: Instruction limit % 215.00/31.86 % (3897274)Termination phase: Finite model building preprocessing % 215.00/31.86 % (3897274)Time elapsed: 5.057 s % 215.00/31.86 % (3897274)Peak memory usage: 392 MB % 215.00/31.86 % (3897274)Instructions burned: 22069 (million) % 215.00/31.86 % (3897293)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=970916849:i=54282_2923 on theBenchmark for (2923ds/54282Mi) % 215.00/31.86 % (3897289)Instruction limit reached! % 215.00/31.86 % (3897289)------------------------------ % 215.00/31.86 % (3897289)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 215.00/31.86 % (3897289)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 215.00/31.86 % (3897289)CaDiCaL version: 2.1.3 % 215.00/31.86 % (3897289)Termination reason: Instruction limit % 215.00/31.86 % (3897289)Termination phase: Preprocessing 2 % 215.00/31.86 % (3897289)Time elapsed: 0.747 s % 215.00/31.86 % (3897289)Peak memory usage: 189 MB % 215.00/31.86 % (3897289)Instructions burned: 869 (million) % 215.00/31.86 % (3897295)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3793368150:i=3512:aac=none_2919 on theBenchmark for (2919ds/3512Mi) % 215.00/31.86 % (3897285)Instruction limit reached! % 215.00/31.86 % (3897285)------------------------------ % 215.00/31.86 % (3897285)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 215.00/31.86 % (3897285)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 215.00/31.86 % (3897285)CaDiCaL version: 2.1.3 % 215.00/31.86 % (3897285)Termination reason: Instruction limit % 215.00/31.86 % (3897285)Termination phase: Function definition elimination % 215.00/31.86 % (3897285)Time elapsed: 3.540 s % 215.00/31.86 % (3897285)Peak memory usage: 295 MB % 215.00/31.86 % (3897285)Instructions burned: 6326 (million) % 215.00/31.86 % (3897297)dis+21_1_sil=32000:sas=cadical:random_seed=2043123317:i=3773:amm=off_2916 on theBenchmark for (2916ds/3773Mi) % 215.00/31.86 % (3897295)Instruction limit reached! % 215.00/31.86 % (3897295)------------------------------ % 215.00/31.86 % (3897295)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 215.00/31.86 % (3897295)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 215.00/31.86 % (3897295)CaDiCaL version: 2.1.3 % 215.00/31.86 % (3897295)Termination reason: Instruction limit % 215.00/31.86 % (3897295)Termination phase: Property scanning % 215.00/31.86 % (3897295)Time elapsed: 2.390 s % 215.00/31.86 % (3897295)Peak memory usage: 291 MB % 215.00/31.86 %Terminated %------------------------------------------------------------------------------