%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWX027+1 : TPTP v9.3.1. Released v9.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n020.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:46:22 PM UTC 2026 % Result : Timeout 291.38s 41.39s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : SWX027+1 : TPTP v9.3.1. Released v9.1.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.10/0.17 % Computer : n020.cluster.edu % 0.10/0.17 % Model : x86_64 x86_64 % 0.10/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.17 % Memory : 8046.5625MB % 0.10/0.17 % OS : Linux 6.8.0-71-generic % 0.10/0.17 % CPULimit : 300 % 0.10/0.17 % WCLimit : 300 % 0.10/0.17 % DateTime : Mon Sep 28 14:52:50 UTC 2026 % 0.10/0.17 % CPUTime : % 0.10/0.17 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.10/0.20 Running first-order model finding % 0.10/0.20 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 % 14.83/2.32 % (219738)Will run a generic schedule for satisfiability detection. % 14.83/2.32 % (219749)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2382728431:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 14.83/2.32 % (219744)% WARNING: option uhcvi not known. % 14.83/2.32 % (219743)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=4081564667_2999 on theBenchmark for (2999ds/0Mi) % 14.83/2.32 % (219745)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=488554961:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 14.83/2.32 % (219746)dis+10_1_sil=32000:sp=arity:random_seed=1528594738:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 14.83/2.32 % (219747)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3200927362:i=116_2999 on theBenchmark for (2999ds/116Mi) % 14.83/2.32 % (219748)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=806668568:i=131_2999 on theBenchmark for (2999ds/131Mi) % 14.83/2.32 % (219744)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=449135784:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 14.83/2.32 % TRYING [1] % 14.83/2.32 % TRYING [2] % 14.83/2.32 % TRYING [3] % 14.83/2.32 % (219749)Instruction limit reached! % 14.83/2.32 % (219749)------------------------------ % 14.83/2.32 % (219749)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 14.83/2.32 % (219749)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.83/2.32 % (219749)CaDiCaL version: 2.1.3 % 14.83/2.32 % (219749)Termination reason: Instruction limit % 14.83/2.32 % (219749)Termination phase: Saturation % 14.83/2.32 % (219749)Time elapsed: 0.057 s % 14.83/2.32 % (219749)Peak memory usage: 15 MB % 14.83/2.32 % (219749)Instructions burned: 160 (million) % 14.83/2.32 % (219757)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2824792587:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 14.83/2.32 % (219746)Instruction limit reached! % 14.83/2.32 % (219746)------------------------------ % 14.83/2.32 % (219746)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 14.83/2.32 % (219746)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.83/2.32 % (219746)CaDiCaL version: 2.1.3 % 14.83/2.32 % (219746)Termination reason: Instruction limit % 14.83/2.32 % (219746)Termination phase: Saturation % 14.83/2.32 % (219746)Time elapsed: 0.070 s % 14.83/2.32 % (219746)Peak memory usage: 13 MB % 14.83/2.32 % (219746)Instructions burned: 104 (million) % 14.83/2.32 % TRYING [1] % 14.83/2.32 % TRYING [2] % 14.83/2.32 % (219748)Instruction limit reached! % 14.83/2.32 % (219748)------------------------------ % 14.83/2.32 % (219748)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 14.83/2.32 % (219748)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.83/2.32 % (219748)CaDiCaL version: 2.1.3 % 14.83/2.32 % (219748)Termination reason: Instruction limit % 14.83/2.32 % (219748)Termination phase: Saturation % 14.83/2.32 % (219748)Time elapsed: 0.075 s % 14.83/2.32 % (219748)Peak memory usage: 14 MB % 14.83/2.32 % (219748)Instructions burned: 132 (million) % 14.83/2.32 % (219747)Instruction limit reached! % 14.83/2.32 % (219747)------------------------------ % 14.83/2.32 % (219747)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 14.83/2.32 % (219747)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.83/2.32 % (219747)CaDiCaL version: 2.1.3 % 14.83/2.32 % (219747)Termination reason: Instruction limit % 14.83/2.32 % (219747)Termination phase: Saturation % 14.83/2.32 % (219747)Time elapsed: 0.075 s % 14.83/2.32 % (219747)Peak memory usage: 14 MB % 14.83/2.32 % (219747)Instructions burned: 117 (million) % 14.83/2.32 % TRYING [3] % 14.83/2.32 % TRYING [4] % 14.83/2.32 % (219759)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1266037915:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi) % 14.83/2.32 % (219761)ott-21_1_sil=16000:fs=off:random_seed=3792161794:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 14.83/2.32 % (219760)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=2991264261:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 14.83/2.32 % TRYING [4] % 14.83/2.32 % (219759)Instruction limit reached! % 14.83/2.32 % (219759)------------------------------ % 14.83/2.32 % (219759)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 14.83/2.32 % (219759)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.66/6.71 % (219759)CaDiCaL version: 2.1.3 % 45.66/6.71 % (219759)Termination reason: Instruction limit % 45.66/6.71 % (219759)Termination phase: Saturation % 45.66/6.71 % (219759)Time elapsed: 0.080 s % 45.66/6.71 % (219759)Peak memory usage: 13 MB % 45.66/6.71 % (219759)Instructions burned: 131 (million) % 45.66/6.71 % (219761)Instruction limit reached! % 45.66/6.71 % (219761)------------------------------ % 45.66/6.71 % (219761)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 45.66/6.71 % (219761)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.66/6.71 % (219761)CaDiCaL version: 2.1.3 % 45.66/6.71 % (219761)Termination reason: Instruction limit % 45.66/6.71 % (219761)Termination phase: Saturation % 45.66/6.71 % (219761)Time elapsed: 0.087 s % 45.66/6.71 % (219761)Peak memory usage: 13 MB % 45.66/6.71 % (219761)Instructions burned: 180 (million) % 45.66/6.71 % (219765)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1098634784:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi) % 45.66/6.71 % (219766)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=477596058:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi) % 45.66/6.71 % TRYING [5] % 45.66/6.71 % (219757)Instruction limit reached! % 45.66/6.71 % (219757)------------------------------ % 45.66/6.71 % (219757)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 45.66/6.71 % (219757)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.66/6.71 % (219757)CaDiCaL version: 2.1.3 % 45.66/6.71 % (219757)Termination reason: Instruction limit % 45.66/6.71 % (219757)Termination phase: Finite model building constraint generation % 45.66/6.71 % (219757)Time elapsed: 0.151 s % 45.66/6.71 % (219757)Peak memory usage: 39 MB % 45.66/6.71 % (219757)Instructions burned: 720 (million) % 45.66/6.71 % TRYING [1] % 45.66/6.71 % TRYING [2] % 45.66/6.71 % (219769)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1561716448:i=1179_2997 on theBenchmark for (2997ds/1179Mi) % 45.66/6.71 % TRYING [3] % 45.66/6.71 % TRYING [5] % 45.66/6.71 % TRYING [4] % 45.66/6.71 % (219760)Instruction limit reached! % 45.66/6.71 % (219760)------------------------------ % 45.66/6.71 % (219760)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 45.66/6.71 % (219760)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.66/6.71 % (219760)CaDiCaL version: 2.1.3 % 45.66/6.71 % (219760)Termination reason: Instruction limit % 45.66/6.71 % (219760)Termination phase: Saturation % 45.66/6.71 % (219760)Time elapsed: 0.419 s % 45.66/6.71 % (219760)Peak memory usage: 20 MB % 45.66/6.71 % (219760)Instructions burned: 685 (million) % 45.66/6.71 % (219765)Instruction limit reached! % 45.66/6.71 % (219765)------------------------------ % 45.66/6.71 % (219765)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 45.66/6.71 % (219765)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.66/6.71 % (219765)CaDiCaL version: 2.1.3 % 45.66/6.71 % (219765)Termination reason: Instruction limit % 45.66/6.71 % (219765)Termination phase: Saturation % 45.66/6.71 % (219765)Time elapsed: 0.333 s % 45.66/6.71 % (219765)Peak memory usage: 15 MB % 45.66/6.71 % (219765)Instructions burned: 478 (million) % 45.66/6.71 % (219771)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=4093151392:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi) % 45.66/6.71 % (219772)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=880478260: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) % 45.66/6.71 % (219766)Instruction limit reached! % 45.66/6.71 % (219766)------------------------------ % 45.66/6.71 % (219766)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 45.66/6.71 % (219766)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.66/6.71 % (219766)CaDiCaL version: 2.1.3 % 45.66/6.71 % (219766)Termination reason: Instruction limit % 45.66/6.71 % (219766)Termination phase: Finite model building SAT solving % 45.66/6.71 % (219766)Time elapsed: 0.344 s % 45.66/6.71 % (219766)Peak memory usage: 31 MB % 45.66/6.71 % (219766)Instructions burned: 866 (million) % 45.66/6.71 % (219775)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2486782052:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi) % 45.66/6.71 % (219769)Instruction limit reached! % 45.66/6.71 % (219769)------------------------------ % 45.66/6.71 % (219769)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 45.66/6.71 % (219769)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 77.92/11.21 % (219769)CaDiCaL version: 2.1.3 % 77.92/11.21 % (219769)Termination reason: Instruction limit % 77.92/11.21 % (219769)Termination phase: Saturation % 77.92/11.21 % (219769)Time elapsed: 0.393 s % 77.92/11.21 % (219769)Peak memory usage: 27 MB % 77.92/11.21 % (219769)Instructions burned: 1181 (million) % 77.92/11.21 % (219777)fmb+10_1_sil=64000:random_seed=4097812419:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi) % 77.92/11.21 % TRYING [1] % 77.92/11.21 % TRYING [2] % 77.92/11.21 % TRYING [3] % 77.92/11.21 % TRYING [6] % 77.92/11.21 % TRYING [4] % 77.92/11.21 % (219772)Instruction limit reached! % 77.92/11.21 % (219772)------------------------------ % 77.92/11.21 % (219772)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 77.92/11.21 % (219772)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 77.92/11.21 % (219772)CaDiCaL version: 2.1.3 % 77.92/11.21 % (219772)Termination reason: Instruction limit % 77.92/11.21 % (219772)Termination phase: Saturation % 77.92/11.21 % (219772)Time elapsed: 0.402 s % 77.92/11.21 % (219772)Peak memory usage: 19 MB % 77.92/11.21 % (219772)Instructions burned: 693 (million) % 77.92/11.21 % (219771)Instruction limit reached! % 77.92/11.21 % (219771)------------------------------ % 77.92/11.21 % (219771)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 77.92/11.21 % (219771)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 77.92/11.21 % (219771)CaDiCaL version: 2.1.3 % 77.92/11.21 % (219771)Termination reason: Instruction limit % 77.92/11.21 % (219771)Termination phase: Finite model building constraint generation % 77.92/11.21 % (219771)Time elapsed: 0.411 s % 77.92/11.21 % (219771)Peak memory usage: 105 MB % 77.92/11.21 % (219771)Instructions burned: 890 (million) % 77.92/11.21 % (219779)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=82669807:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi) % 77.92/11.21 % (219780)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3427744573:fmbsr=1.7:i=920_2990 on theBenchmark for (2990ds/920Mi) % 77.92/11.21 % TRYING [5] % 77.92/11.21 % TRYING [20] % 77.92/11.21 % TRYING [8] % 77.92/11.21 % (219775)Instruction limit reached! % 77.92/11.21 % (219775)------------------------------ % 77.92/11.21 % (219775)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 77.92/11.21 % (219775)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 77.92/11.21 % (219775)CaDiCaL version: 2.1.3 % 77.92/11.21 % (219775)Termination reason: Instruction limit % 77.92/11.21 % (219775)Termination phase: Saturation % 77.92/11.21 % (219775)Time elapsed: 0.463 s % 77.92/11.21 % (219775)Peak memory usage: 20 MB % 77.92/11.21 % (219775)Instructions burned: 879 (million) % 77.92/11.21 % (219783)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=4122049569:i=5131_2989 on theBenchmark for (2989ds/5131Mi) % 77.92/11.21 % (219780)Instruction limit reached! % 77.92/11.21 % (219780)------------------------------ % 77.92/11.21 % (219780)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 77.92/11.21 % (219780)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 77.92/11.21 % (219780)CaDiCaL version: 2.1.3 % 77.92/11.21 % (219780)Termination reason: Instruction limit % 77.92/11.21 % (219780)Termination phase: Finite model building constraint generation % 77.92/11.21 % (219780)Time elapsed: 0.318 s % 77.92/11.21 % (219780)Peak memory usage: 66 MB % 77.92/11.21 % (219780)Instructions burned: 921 (million) % 77.92/11.21 % (219785)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=514807865:i=1472:ins=7:fdi=8:gsp=on_2986 on theBenchmark for (2986ds/1472Mi) % 77.92/11.21 % TRYING [6] % 77.92/11.21 % TRYING [7] % 77.92/11.21 % (219785)Instruction limit reached! % 77.92/11.21 % (219785)------------------------------ % 77.92/11.21 % (219785)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 77.92/11.21 % (219785)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 77.92/11.21 % (219785)CaDiCaL version: 2.1.3 % 77.92/11.21 % (219785)Termination reason: Instruction limit % 77.92/11.21 % (219785)Termination phase: Saturation % 77.92/11.21 % (219785)Time elapsed: 0.703 s % 77.92/11.21 % (219785)Peak memory usage: 25 MB % 77.92/11.21 % (219785)Instructions burned: 1473 (million) % 77.92/11.21 % (219787)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1483562458:i=6324_2979 on theBenchmark for (2979ds/6324Mi) % 77.92/11.21 % (219787)Cannot represent all propositional literals internally % 77.92/11.21 % (219787)Refutation not found, incomplete strategy % 77.92/11.21 % (219787)------------------------------ % 77.92/11.21 % (219787)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 199.18/28.37 % (219787)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 199.18/28.37 % (219787)CaDiCaL version: 2.1.3 % 199.18/28.37 % (219787)Termination reason: Refutation not found, incomplete strategy % 199.18/28.37 % (219787)Time elapsed: 0.023 s % 199.18/28.37 % (219787)Peak memory usage: 11 MB % 199.18/28.37 % (219787)Instructions burned: 43 (million) % 199.18/28.37 % (219787)------------------------------ % 199.18/28.37 % (219787)------------------------------ % 199.18/28.37 % (219789)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1488324373:fmbsr=2.30978:i=2174_2978 on theBenchmark for (2978ds/2174Mi) % 199.18/28.37 % TRYING [16] % 199.18/28.37 % (219789)Instruction limit reached! % 199.18/28.37 % (219789)------------------------------ % 199.18/28.37 % (219789)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 199.18/28.37 % (219789)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 199.18/28.37 % (219789)CaDiCaL version: 2.1.3 % 199.18/28.37 % (219789)Termination reason: Instruction limit % 199.18/28.37 % (219789)Termination phase: Finite model building constraint generation % 199.18/28.38 % (219789)Time elapsed: 0.764 s % 199.18/28.38 % (219789)Peak memory usage: 130 MB % 199.18/28.38 % (219789)Instructions burned: 2177 (million) % 199.18/28.38 % (219791)ott-2_1_sil=16000:newcnf=on:random_seed=3319636282:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2970 on theBenchmark for (2970ds/869Mi) % 199.18/28.38 % (219791)Instruction limit reached! % 199.18/28.38 % (219791)------------------------------ % 199.18/28.38 % (219791)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 199.18/28.38 % (219791)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 199.18/28.38 % (219791)CaDiCaL version: 2.1.3 % 199.18/28.38 % (219791)Termination reason: Instruction limit % 199.18/28.38 % (219791)Termination phase: Saturation % 199.18/28.38 % (219791)Time elapsed: 0.479 s % 199.18/28.38 % (219791)Peak memory usage: 22 MB % 199.18/28.38 % (219791)Instructions burned: 871 (million) % 199.18/28.38 % (219793)ott+10_1_sil=32000:tgt=ground:random_seed=1356066697:i=5114:av=off_2965 on theBenchmark for (2965ds/5114Mi) % 199.18/28.38 % TRYING [7] % 199.18/28.38 % (219783)Instruction limit reached! % 199.18/28.38 % (219783)------------------------------ % 199.18/28.38 % (219783)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 199.18/28.38 % (219783)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 199.18/28.38 % (219783)CaDiCaL version: 2.1.3 % 199.18/28.38 % (219783)Termination reason: Instruction limit % 199.18/28.38 % (219783)Termination phase: Saturation % 199.18/28.38 % (219783)Time elapsed: 2.858 s % 199.18/28.38 % (219783)Peak memory usage: 40 MB % 199.18/28.38 % (219783)Instructions burned: 5132 (million) % 199.18/28.38 % (219795)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3868841633:i=54282_2960 on theBenchmark for (2960ds/54282Mi) % 199.18/28.38 % TRYING [1] % 199.18/28.38 % TRYING [2] % 199.18/28.38 % TRYING [3] % 199.18/28.38 % TRYING [4] % 199.18/28.38 % TRYING [8] % 199.18/28.38 % TRYING [5] % 199.18/28.38 % (219779)Instruction limit reached! % 199.18/28.38 % (219779)------------------------------ % 199.18/28.38 % (219779)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 199.18/28.38 % (219779)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 199.18/28.38 % (219779)CaDiCaL version: 2.1.3 % 199.18/28.38 % (219779)Termination reason: Instruction limit % 199.18/28.38 % (219779)Termination phase: Finite model building constraint generation % 199.18/28.38 % (219779)Time elapsed: 3.420 s % 199.18/28.38 % (219779)Peak memory usage: 586 MB % 199.18/28.38 % (219779)Instructions burned: 9518 (million) % 199.18/28.38 % (219797)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3973543190:i=3512:aac=none_2955 on theBenchmark for (2955ds/3512Mi) % 199.18/28.38 % TRYING [6] % 199.18/28.38 % TRYING [7] % 199.18/28.38 % (219777)Instruction limit reached! % 199.18/28.38 % (219777)------------------------------ % 199.18/28.38 % (219777)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 199.18/28.38 % (219777)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 199.18/28.38 % (219777)CaDiCaL version: 2.1.3 % 199.18/28.38 % (219777)Termination reason: Instruction limit % 199.18/28.38 % (219777)Termination phase: Finite model building SAT solving % 199.18/28.38 % (219777)Time elapsed: 5.442 s % 199.18/28.38 % (219777)Peak memory usage: 285 MB % 199.18/28.38 % (219777)Instructions burned: 22062 (million) % 199.18/28.38 % (219799)dis+21_1_sil=32000:sas=cadical:random_seed=95320463:i=3773:amm=off_2938 on theBenchmark for (2938ds/3773Mi) % 199.18/28.38 % (219793)Instruction limit reached! % 199.18/28.38 % (219793)------------------------------ % 199.18/28.38 % (219793)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 291.38/41.39 % (219793)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 291.38/41.39 % (219793)CaDiCaL version: 2.1.3 % 291.38/41.39 % (219793)Termination reason: Instruction limit % 291.38/41.39 % (219793)Termination phase: Saturation % 291.38/41.39 % (219793)Time elapsed: 3.073 s % 291.38/41.39 % (219793)Peak memory usage: 54 MB % 291.38/41.39 % (219793)Instructions burned: 5115 (million) % 291.38/41.39 % (219801)ott+11_1_sil=16000:gs=on:random_seed=4091239535:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2934 on theBenchmark for (2934ds/2251Mi) % 291.38/41.39 % (219797)Instruction limit reached! % 291.38/41.39 % (219797)------------------------------ % 291.38/41.39 % (219797)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 291.38/41.39 % (219797)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 291.38/41.39 % (219797)CaDiCaL version: 2.1.3 % 291.38/41.39 % (219797)Termination reason: Instruction limit % 291.38/41.39 % (219797)Termination phase: Saturation % 291.38/41.39 % (219797)Time elapsed: 2.031 s % 291.38/41.39 % (219797)Peak memory usage: 33 MB % 291.38/41.39 % (219797)Instructions burned: 3513 (million) % 291.38/41.39 % (219803)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2335414526:fmbsr=1.6:i=67534_2934 on theBenchmark for (2934ds/67534Mi) % 291.38/41.39 % TRYING [7] % 291.38/41.39 % (219799)Instruction limit reached! % 291.38/41.39 % (219799)------------------------------ % 291.38/41.39 % (219799)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 291.38/41.39 % (219799)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 291.38/41.39 % (219799)CaDiCaL version: 2.1.3 % 291.38/41.39 % (219799)Termination reason: Instruction limit % 291.38/41.39 % (219799)Termination phase: Saturation % 291.38/41.39 % (219799)Time elapsed: 1.173 s % 291.38/41.39 % (219799)Peak memory usage: 40 MB % 291.38/41.39 % (219799)Instructions burned: 3775 (million) % 291.38/41.39 % (219805)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=680057874:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2926 on theBenchmark for (2926ds/4591Mi) % 291.38/41.39 % (219801)Instruction limit reached! % 291.38/41.39 % (219801)------------------------------ % 291.38/41.39 % (219801)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 291.38/41.39 % (219801)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 291.38/41.39 % (219801)CaDiCaL version: 2.1.3 % 291.38/41.39 % (219801)Termination reason: Instruction limit % 291.38/41.39 % (219801)Termination phase: Saturation % 291.38/41.39 % (219801)Time elapsed: 1.081 s % 291.38/41.39 % (219801)Peak memory usage: 21 MB % 291.38/41.39 % (219801)Instructions burned: 2253 (million) % 291.38/41.39 % (219807)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=513252841:i=29340_2923 on theBenchmark for (2923ds/29340Mi) % 291.38/41.39 % TRYING [8] % 291.38/41.39 % (219805)Instruction limit reached! % 291.38/41.39 % (219805)------------------------------ % 291.38/41.39 % (219805)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 291.38/41.39 % (219805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 291.38/41.39 % (219805)CaDiCaL version: 2.1.3 % 291.38/41.39 % (219805)Termination reason: Instruction limit % 291.38/41.39 % (219805)Termination phase: Saturation % 291.38/41.39 % (219805)Time elapsed: 1.243 s % 291.38/41.39 % (219805)Peak memory usage: 57 MB % 291.38/41.39 % (219805)Instructions burned: 4594 (million) % 291.38/41.39 % (219809)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2984879545:i=5211_2914 on theBenchmark for (2914ds/5211Mi) % 291.38/41.39 % TRYING [9] % 291.38/41.39 % (219809)Instruction limit reached! % 291.38/41.39 % (219809)------------------------------ % 291.38/41.39 % (219809)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 291.38/41.39 % (219809)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 291.38/41.39 % (219809)CaDiCaL version: 2.1.3 % 291.38/41.39 % (219809)Termination reason: Instruction limit % 291.38/41.39 % (219809)Termination phase: Saturation % 291.38/41.39 % (219809)Time elapsed: 1.363 s % 291.38/41.39 % (219809)Peak memory usage: 44 MB % 291.38/41.39 % (219809)Instructions burned: 5214 (million) % 291.38/41.39 % (219811)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=266574136:i=5497:nm=2_2900 on theBenchmark for (2900ds/5497Mi) % 291.38/41.39 % TRYING [17] % 291.38/41.39 % (219811)Instruction limit reached! % 291.38/41.39 % (219811)------------------------------ % 291.38/41.39 % (219811)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54Terminated % 300.55/42.63 % Vampire exiting % 300.55/42.63 Terminated %------------------------------------------------------------------------------