%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWC224-1 : TPTP v9.3.1. Released v2.4.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n001.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:05:10 PM UTC 2026 % Result : Timeout 300.42s 42.64s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWC224-1 : TPTP v9.3.1. Released v2.4.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.09/0.22 % Computer : n001.cluster.edu % 0.09/0.22 % Model : x86_64 x86_64 % 0.09/0.22 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.22 % Memory : 8046.5625MB % 0.09/0.22 % OS : Linux 6.8.0-71-generic % 0.09/0.22 % CPULimit : 300 % 0.09/0.22 % WCLimit : 300 % 0.09/0.22 % DateTime : Mon Sep 28 08:38:47 UTC 2026 % 0.09/0.22 % CPUTime : % 0.09/0.22 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.25/0.28 Running first-order model finding % 0.25/0.28 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 % 44.90/6.70 % (218047)Will run a generic schedule for satisfiability detection. % 44.90/6.70 % (218056)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1743605812:i=116_2999 on theBenchmark for (2999ds/116Mi) % 44.90/6.70 % (218054)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2474601725:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 44.90/6.70 % (218053)% WARNING: option uhcvi not known. % 44.90/6.70 % (218055)dis+10_1_sil=32000:sp=arity:random_seed=472672351:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 44.90/6.70 % (218058)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3274328578:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 44.90/6.70 % (218057)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3083197457:i=131_2999 on theBenchmark for (2999ds/131Mi) % 44.90/6.70 % (218053)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2474528804:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 44.90/6.70 % (218052)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=779816288_2999 on theBenchmark for (2999ds/0Mi) % 44.90/6.70 % TRYING [1] % 44.90/6.70 % TRYING [2] % 44.90/6.70 % TRYING [3] % 44.90/6.70 % (218056)Instruction limit reached! % 44.90/6.70 % (218056)------------------------------ % 44.90/6.70 % (218056)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 44.90/6.70 % (218056)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 44.90/6.70 % (218056)CaDiCaL version: 2.1.3 % 44.90/6.70 % (218056)Termination reason: Instruction limit % 44.90/6.70 % (218056)Termination phase: Saturation % 44.90/6.70 % (218056)Time elapsed: 0.055 s % 44.90/6.70 % (218056)Peak memory usage: 13 MB % 44.90/6.70 % (218056)Instructions burned: 118 (million) % 44.90/6.70 % (218066)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=770776562:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 44.90/6.70 % TRYING [4] % 44.90/6.70 % TRYING [1] % 44.90/6.70 % TRYING [2] % 44.90/6.70 % (218055)Instruction limit reached! % 44.90/6.70 % (218055)------------------------------ % 44.90/6.70 % (218055)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 44.90/6.70 % (218055)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 44.90/6.70 % (218055)CaDiCaL version: 2.1.3 % 44.90/6.70 % (218055)Termination reason: Instruction limit % 44.90/6.70 % (218055)Termination phase: Saturation % 44.90/6.70 % (218055)Time elapsed: 0.096 s % 44.90/6.70 % (218055)Peak memory usage: 13 MB % 44.90/6.70 % (218055)Instructions burned: 103 (million) % 44.90/6.70 % TRYING [3] % 44.90/6.70 % (218057)Instruction limit reached! % 44.90/6.70 % (218057)------------------------------ % 44.90/6.70 % (218057)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 44.90/6.70 % (218057)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 44.90/6.70 % (218057)CaDiCaL version: 2.1.3 % 44.90/6.70 % (218057)Termination reason: Instruction limit % 44.90/6.70 % (218057)Termination phase: Saturation % 44.90/6.70 % (218057)Time elapsed: 0.116 s % 44.90/6.70 % (218057)Peak memory usage: 14 MB % 44.90/6.70 % (218057)Instructions burned: 131 (million) % 44.90/6.70 % (218068)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3147567181:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi) % 44.90/6.70 % TRYING [4] % 44.90/6.70 % (218070)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=1847436741:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 44.90/6.70 % (218058)Instruction limit reached! % 44.90/6.70 % (218058)------------------------------ % 44.90/6.70 % (218058)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 44.90/6.70 % (218058)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 44.90/6.70 % (218058)CaDiCaL version: 2.1.3 % 44.90/6.70 % (218058)Termination reason: Instruction limit % 44.90/6.70 % (218058)Termination phase: Saturation % 44.90/6.70 % (218058)Time elapsed: 0.160 s % 44.90/6.70 % (218058)Peak memory usage: 14 MB % 44.90/6.70 % (218058)Instructions burned: 159 (million) % 44.90/6.70 % (218072)ott-21_1_sil=16000:fs=off:random_seed=3165530408:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 44.90/6.70 % TRYING [5] % 44.90/6.70 % TRYING [5] % 44.90/6.70 % (218068)Instruction limit reached! % 44.90/6.70 % (218068)------------------------------ % 44.90/6.70 % (218068)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 44.90/6.70 % (218068)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 79.65/11.59 % (218068)CaDiCaL version: 2.1.3 % 79.65/11.59 % (218068)Termination reason: Instruction limit % 79.65/11.59 % (218068)Termination phase: Saturation % 79.65/11.59 % (218068)Time elapsed: 0.130 s % 79.65/11.59 % (218068)Peak memory usage: 12 MB % 79.65/11.59 % (218068)Instructions burned: 131 (million) % 79.65/11.59 % (218074)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=93694582:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi) % 79.65/11.59 % (218072)Instruction limit reached! % 79.65/11.59 % (218072)------------------------------ % 79.65/11.59 % (218072)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 79.65/11.59 % (218072)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 79.65/11.59 % (218072)CaDiCaL version: 2.1.3 % 79.65/11.59 % (218072)Termination reason: Instruction limit % 79.65/11.59 % (218072)Termination phase: Saturation % 79.65/11.59 % (218072)Time elapsed: 0.164 s % 79.65/11.59 % (218072)Peak memory usage: 13 MB % 79.65/11.59 % (218072)Instructions burned: 181 (million) % 79.65/11.59 % (218066)Instruction limit reached! % 79.65/11.59 % (218066)------------------------------ % 79.65/11.59 % (218066)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 79.65/11.59 % (218066)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 79.65/11.59 % (218066)CaDiCaL version: 2.1.3 % 79.65/11.59 % (218066)Termination reason: Instruction limit % 79.65/11.59 % (218066)Termination phase: Finite model building SAT solving % 79.65/11.59 % (218066)Time elapsed: 0.299 s % 79.65/11.59 % (218066)Peak memory usage: 37 MB % 79.65/11.59 % (218066)Instructions burned: 714 (million) % 79.65/11.59 % (218076)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2532224127:fmbsr=1.3:i=865:ins=25_2996 on theBenchmark for (2996ds/865Mi) % 79.65/11.59 % TRYING [1] % 79.65/11.59 % TRYING [2] % 79.65/11.59 % (218077)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3799693922:i=1179_2995 on theBenchmark for (2995ds/1179Mi) % 79.65/11.59 % TRYING [3] % 79.65/11.59 % TRYING [4] % 79.65/11.59 % TRYING [6] % 79.65/11.59 % TRYING [5] % 79.65/11.59 % (218074)Instruction limit reached! % 79.65/11.59 % (218074)------------------------------ % 79.65/11.59 % (218074)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 79.65/11.59 % (218074)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 79.65/11.59 % (218074)CaDiCaL version: 2.1.3 % 79.65/11.59 % (218074)Termination reason: Instruction limit % 79.65/11.59 % (218074)Termination phase: Saturation % 79.65/11.59 % (218074)Time elapsed: 0.513 s % 79.65/11.59 % (218074)Peak memory usage: 14 MB % 79.65/11.59 % (218074)Instructions burned: 477 (million) % 79.65/11.59 % (218070)Instruction limit reached! % 79.65/11.59 % (218070)------------------------------ % 79.65/11.59 % (218070)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 79.65/11.59 % (218070)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 79.65/11.59 % (218070)CaDiCaL version: 2.1.3 % 79.65/11.59 % (218070)Termination reason: Instruction limit % 79.65/11.59 % (218070)Termination phase: Saturation % 79.65/11.59 % (218070)Time elapsed: 0.698 s % 79.65/11.59 % (218070)Peak memory usage: 20 MB % 79.65/11.59 % (218070)Instructions burned: 684 (million) % 79.65/11.59 % (218080)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1472846326:i=889:ins=1_2991 on theBenchmark for (2991ds/889Mi) % 79.65/11.59 % (218081)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=1203185422:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2991 on theBenchmark for (2991ds/692Mi) % 79.65/11.59 % (218076)Instruction limit reached! % 79.65/11.59 % (218076)------------------------------ % 79.65/11.59 % (218076)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 79.65/11.59 % (218076)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 79.65/11.59 % (218076)CaDiCaL version: 2.1.3 % 79.65/11.59 % (218076)Termination reason: Instruction limit % 79.65/11.59 % (218076)Termination phase: Finite model building SAT solving % 79.65/11.59 % (218076)Time elapsed: 0.558 s % 79.65/11.59 % (218076)Peak memory usage: 23 MB % 79.65/11.59 % (218076)Instructions burned: 866 (million) % 79.65/11.59 % (218084)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=312726954:i=879:kws=inv_precedence:fsr=off_2990 on theBenchmark for (2990ds/879Mi) % 79.65/11.59 % (218077)Instruction limit reached! % 79.65/11.59 % (218077)------------------------------ % 79.65/11.59 % (218077)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 132.11/19.03 % (218077)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 132.11/19.03 % (218077)CaDiCaL version: 2.1.3 % 132.11/19.03 % (218077)Termination reason: Instruction limit % 132.11/19.03 % (218077)Termination phase: Saturation % 132.11/19.03 % (218077)Time elapsed: 0.614 s % 132.11/19.03 % (218077)Peak memory usage: 28 MB % 132.11/19.03 % (218077)Instructions burned: 1180 (million) % 132.11/19.03 % (218086)fmb+10_1_sil=64000:random_seed=3809109210:i=22061:nm=2:gsp=on_2989 on theBenchmark for (2989ds/22061Mi) % 132.11/19.03 % TRYING [1] % 132.11/19.03 % TRYING [2] % 132.11/19.03 % TRYING [3] % 132.11/19.03 % TRYING [4] % 132.11/19.03 % TRYING [14] % 132.11/19.03 % TRYING [5] % 132.11/19.03 % TRYING [7] % 132.11/19.03 % (218081)Instruction limit reached! % 132.11/19.03 % (218081)------------------------------ % 132.11/19.03 % (218081)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 132.11/19.03 % (218081)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 132.11/19.03 % (218081)CaDiCaL version: 2.1.3 % 132.11/19.03 % (218081)Termination reason: Instruction limit % 132.11/19.03 % (218081)Termination phase: Saturation % 132.11/19.03 % (218081)Time elapsed: 0.651 s % 132.11/19.03 % (218081)Peak memory usage: 18 MB % 132.11/19.03 % (218081)Instructions burned: 692 (million) % 132.11/19.03 % (218080)Instruction limit reached! % 132.11/19.03 % (218080)------------------------------ % 132.11/19.03 % (218080)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 132.11/19.03 % (218080)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 132.11/19.03 % (218080)CaDiCaL version: 2.1.3 % 132.11/19.03 % (218080)Termination reason: Instruction limit % 132.11/19.03 % (218080)Termination phase: Finite model building constraint generation % 132.11/19.03 % (218080)Time elapsed: 0.708 s % 132.11/19.03 % (218080)Peak memory usage: 77 MB % 132.11/19.03 % (218080)Instructions burned: 890 (million) % 132.11/19.03 % (218088)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3793686734:i=9515:nm=5_2984 on theBenchmark for (2984ds/9515Mi) % 132.11/19.03 % TRYING [20] % 132.11/19.03 % (218090)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=808691064:fmbsr=1.7:i=920_2983 on theBenchmark for (2983ds/920Mi) % 132.11/19.03 % TRYING [8] % 132.11/19.03 % TRYING [6] % 132.11/19.03 % (218084)Instruction limit reached! % 132.11/19.03 % (218084)------------------------------ % 132.11/19.03 % (218084)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 132.11/19.03 % (218084)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 132.11/19.03 % (218084)CaDiCaL version: 2.1.3 % 132.11/19.03 % (218084)Termination reason: Instruction limit % 132.11/19.03 % (218084)Termination phase: Saturation % 132.11/19.03 % (218084)Time elapsed: 0.787 s % 132.11/19.03 % (218084)Peak memory usage: 20 MB % 132.11/19.03 % (218084)Instructions burned: 879 (million) % 132.11/19.03 % (218094)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3724619851:i=5131_2981 on theBenchmark for (2981ds/5131Mi) % 132.11/19.03 % (218090)Instruction limit reached! % 132.11/19.03 % (218090)------------------------------ % 132.11/19.03 % (218090)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 132.11/19.03 % (218090)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 132.11/19.03 % (218090)CaDiCaL version: 2.1.3 % 132.11/19.03 % (218090)Termination reason: Instruction limit % 132.11/19.03 % (218090)Termination phase: Finite model building constraint generation % 132.11/19.03 % (218090)Time elapsed: 0.655 s % 132.11/19.03 % (218090)Peak memory usage: 77 MB % 132.11/19.03 % (218090)Instructions burned: 920 (million) % 132.11/19.03 % (218096)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3282996106:i=1472:ins=7:fdi=8:gsp=on_2976 on theBenchmark for (2976ds/1472Mi) % 132.11/19.03 % TRYING [7] % 132.11/19.03 % TRYING [8] % 132.11/19.03 % (218096)Instruction limit reached! % 132.11/19.03 % (218096)------------------------------ % 132.11/19.03 % (218096)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 132.11/19.03 % (218096)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 132.11/19.03 % (218096)CaDiCaL version: 2.1.3 % 132.11/19.03 % (218096)Termination reason: Instruction limit % 132.11/19.03 % (218096)Termination phase: Saturation % 132.11/19.03 % (218096)Time elapsed: 1.187 s % 132.11/19.03 % (218096)Peak memory usage: 15 MB % 132.11/19.03 % (218096)Instructions burned: 1472 (million) % 132.11/19.03 % (218098)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2903305847:i=6324_2964 on theBenchmark for (2964ds/6324Mi) % 132.11/19.03 % TRYING [77] % 132.11/19.03 % TRYING [8] % 132.11/19.03 % (218094)Instruction limit reached! % 132.11/19.03 % (218094)------------------------------ % 132.11/19.03 % (218094)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.42/42.64 % (218094)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.42/42.64 % (218094)CaDiCaL version: 2.1.3 % 300.42/42.64 % (218094)Termination reason: Instruction limit % 300.42/42.64 % (218094)Termination phase: Saturation % 300.42/42.64 % (218094)Time elapsed: 4.550 s % 300.42/42.64 % (218094)Peak memory usage: 56 MB % 300.42/42.64 % (218094)Instructions burned: 5131 (million) % 300.42/42.64 % (218100)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=4211924186:fmbsr=2.30978:i=2174_2935 on theBenchmark for (2935ds/2174Mi) % 300.42/42.64 % TRYING [16] % 300.42/42.64 % TRYING [9] % 300.42/42.64 % (218100)Instruction limit reached! % 300.42/42.64 % (218100)------------------------------ % 300.42/42.64 % (218100)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.42/42.64 % (218100)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.42/42.64 % (218100)CaDiCaL version: 2.1.3 % 300.42/42.64 % (218100)Termination reason: Instruction limit % 300.42/42.64 % (218100)Termination phase: Finite model building constraint generation % 300.42/42.64 % (218100)Time elapsed: 1.434 s % 300.42/42.64 % (218100)Peak memory usage: 129 MB % 300.42/42.64 % (218100)Instructions burned: 2174 (million) % 300.42/42.64 % (218102)ott-2_1_sil=16000:newcnf=on:random_seed=3473134638:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2920 on theBenchmark for (2920ds/869Mi) % 300.42/42.64 % (218088)Instruction limit reached! % 300.42/42.64 % (218088)------------------------------ % 300.42/42.64 % (218088)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.42/42.64 % (218088)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.42/42.64 % (218088)CaDiCaL version: 2.1.3 % 300.42/42.64 % (218088)Termination reason: Instruction limit % 300.42/42.64 % (218088)Termination phase: Finite model building constraint generation % 300.42/42.64 % (218088)Time elapsed: 6.482 s % 300.42/42.64 % (218088)Peak memory usage: 593 MB % 300.42/42.64 % (218088)Instructions burned: 9515 (million) % 300.42/42.64 % (218098)Instruction limit reached! % 300.42/42.64 % (218098)------------------------------ % 300.42/42.64 % (218098)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.42/42.64 % (218098)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.42/42.64 % (218098)CaDiCaL version: 2.1.3 % 300.42/42.64 % (218098)Termination reason: Instruction limit % 300.42/42.64 % (218098)Termination phase: Finite model building constraint generation % 300.42/42.64 % (218098)Time elapsed: 4.579 s % 300.42/42.64 % (218098)Peak memory usage: 524 MB % 300.42/42.64 % (218098)Instructions burned: 6324 (million) % 300.42/42.64 % (218104)ott+10_1_sil=32000:tgt=ground:random_seed=1156291238:i=5114:av=off_2917 on theBenchmark for (2917ds/5114Mi) % 300.42/42.64 % (218106)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2295543613:i=54282_2917 on theBenchmark for (2917ds/54282Mi) % 300.42/42.64 % TRYING [1] % 300.42/42.64 % TRYING [2] % 300.42/42.64 % TRYING [3] % 300.42/42.64 % TRYING [4] % 300.42/42.64 % TRYING [5] % 300.42/42.64 % (218102)Instruction limit reached! % 300.42/42.64 % (218102)------------------------------ % 300.42/42.64 % (218102)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.42/42.64 % (218102)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.42/42.64 % (218102)CaDiCaL version: 2.1.3 % 300.42/42.64 % (218102)Termination reason: Instruction limit % 300.42/42.64 % (218102)Termination phase: Saturation % 300.42/42.64 % (218102)Time elapsed: 0.739 s % 300.42/42.64 % (218102)Peak memory usage: 21 MB % 300.42/42.64 % (218102)Instructions burned: 869 (million) % 300.42/42.64 % (218108)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=258235073:i=3512:aac=none_2913 on theBenchmark for (2913ds/3512Mi) % 300.42/42.64 % TRYING [6] % 300.42/42.64 % TRYING [9] % 300.42/42.64 % (218086)Instruction limit reached! % 300.42/42.64 % (218086)------------------------------ % 300.42/42.64 % (218086)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.42/42.64 % (218086)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.42/42.64 % (218086)CaDiCaL version: 2.1.3 % 300.42/42.64 % (218086)Termination reason: Instruction limit % 300.42/42.64 % (218086)Termination phase: Finite model building constraint generation % 300.42/42.64 % (218086)Time elapsed: 8.379 s % 300.42/42.64 % (218086)Peak memory usage: 172 MB % 300.42/42.64 % (218086)Instructions burned: 22064 (million) % 300.42/42.64 % (218110)dis+21_1_sil=32000:sas=cadical:random_seed=2624679308:i=3773:amm=off_2905 on theBenchmark for (2905ds/3773Mi) % 300.42/42.64 % TRYING [7] % 300.42/42.64 % TRYING [8] % 300.42/42.64 % (218110)Instruction limit reached! % 300.42/42.64 % (218110)------------------------------ % 300.42/42.64 % (218110)Version: Vam % 300.42/42.64 Terminated % 300.42/42.64 % Vampire exiting % 300.42/42.64 Terminated %------------------------------------------------------------------------------