%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW457-1 : TPTP v9.3.1. Released v5.2.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n015.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:40:03 PM UTC 2026 % Result : Timeout 300.24s 42.64s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWW457-1 : TPTP v9.3.1. Released v5.2.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.11/0.25 % Computer : n015.cluster.edu % 0.11/0.25 % Model : x86_64 x86_64 % 0.11/0.25 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.25 % Memory : 8046.5625MB % 0.11/0.25 % OS : Linux 6.8.0-71-generic % 0.11/0.25 % CPULimit : 300 % 0.11/0.25 % WCLimit : 300 % 0.11/0.25 % DateTime : Mon Sep 28 14:02:32 UTC 2026 % 0.11/0.25 % CPUTime : % 0.11/0.25 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.24/0.31 Running first-order model finding % 0.24/0.31 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 % 39.82/5.98 % (2640105)Will run a generic schedule for satisfiability detection. % 39.82/5.98 % (2640116)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2977379427:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 39.82/5.98 % (2640111)% WARNING: option uhcvi not known. % 39.82/5.98 % (2640113)dis+10_1_sil=32000:sp=arity:random_seed=3066448727:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 39.82/5.98 % (2640114)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=943670121:i=116_2999 on theBenchmark for (2999ds/116Mi) % 39.82/5.98 % (2640111)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1381549655:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 39.82/5.98 % (2640115)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1547817515:i=131_2999 on theBenchmark for (2999ds/131Mi) % 39.82/5.98 % (2640110)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3598158775_2999 on theBenchmark for (2999ds/0Mi) % 39.82/5.98 % (2640112)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1378298183:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 39.82/5.98 % TRYING [1] % 39.82/5.98 % TRYING [2] % 39.82/5.98 % TRYING [3] % 39.82/5.98 % TRYING [4] % 39.82/5.98 % (2640116)Instruction limit reached! % 39.82/5.98 % (2640116)------------------------------ % 39.82/5.98 % (2640116)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.82/5.98 % (2640116)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.82/5.98 % (2640116)CaDiCaL version: 2.1.3 % 39.82/5.98 % (2640116)Termination reason: Instruction limit % 39.82/5.98 % (2640116)Termination phase: Saturation % 39.82/5.98 % (2640116)Time elapsed: 0.075 s % 39.82/5.98 % (2640116)Peak memory usage: 13 MB % 39.82/5.98 % (2640116)Instructions burned: 160 (million) % 39.82/5.98 % (2640124)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=4046325653:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 39.82/5.98 % TRYING [1] % 39.82/5.98 % TRYING [2] % 39.82/5.98 % TRYING [3] % 39.82/5.98 % (2640114)Instruction limit reached! % 39.82/5.98 % (2640114)------------------------------ % 39.82/5.98 % (2640114)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.82/5.98 % (2640114)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.82/5.98 % (2640114)CaDiCaL version: 2.1.3 % 39.82/5.98 % (2640114)Termination reason: Instruction limit % 39.82/5.98 % (2640114)Termination phase: Saturation % 39.82/5.98 % (2640114)Time elapsed: 0.096 s % 39.82/5.98 % (2640114)Peak memory usage: 12 MB % 39.82/5.98 % (2640114)Instructions burned: 118 (million) % 39.82/5.98 % (2640113)Instruction limit reached! % 39.82/5.98 % (2640113)------------------------------ % 39.82/5.98 % (2640113)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.82/5.98 % (2640113)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.82/5.98 % (2640113)CaDiCaL version: 2.1.3 % 39.82/5.98 % (2640113)Termination reason: Instruction limit % 39.82/5.98 % (2640113)Termination phase: Saturation % 39.82/5.98 % (2640113)Time elapsed: 0.098 s % 39.82/5.98 % (2640113)Peak memory usage: 12 MB % 39.82/5.98 % (2640113)Instructions burned: 103 (million) % 39.82/5.98 % (2640115)Instruction limit reached! % 39.82/5.98 % (2640115)------------------------------ % 39.82/5.98 % (2640115)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.82/5.98 % (2640115)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.82/5.98 % (2640115)CaDiCaL version: 2.1.3 % 39.82/5.98 % (2640115)Termination reason: Instruction limit % 39.82/5.98 % (2640115)Termination phase: Saturation % 39.82/5.98 % (2640115)Time elapsed: 0.099 s % 39.82/5.98 % (2640115)Peak memory usage: 12 MB % 39.82/5.98 % (2640115)Instructions burned: 131 (million) % 39.82/5.98 % (2640126)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2382148907:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi) % 39.82/5.98 % (2640127)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=1260145477:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 39.82/5.98 % (2640128)ott-21_1_sil=16000:fs=off:random_seed=869372796:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 39.82/5.98 % TRYING [4] % 39.82/5.98 % (2640126)Instruction limit reached! % 39.82/5.98 % (2640126)------------------------------ % 39.82/5.98 % (2640126)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.82/5.98 % (2640126)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 81.54/11.89 % (2640126)CaDiCaL version: 2.1.3 % 81.54/11.89 % (2640126)Termination reason: Instruction limit % 81.54/11.89 % (2640126)Termination phase: Saturation % 81.54/11.89 % (2640126)Time elapsed: 0.117 s % 81.54/11.89 % (2640126)Peak memory usage: 13 MB % 81.54/11.89 % (2640126)Instructions burned: 131 (million) % 81.54/11.89 % (2640132)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3722128256:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi) % 81.54/11.89 % (2640128)Instruction limit reached! % 81.54/11.89 % (2640128)------------------------------ % 81.54/11.89 % (2640128)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 81.54/11.89 % (2640128)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 81.54/11.89 % (2640128)CaDiCaL version: 2.1.3 % 81.54/11.89 % (2640128)Termination reason: Instruction limit % 81.54/11.89 % (2640128)Termination phase: Saturation % 81.54/11.89 % (2640128)Time elapsed: 0.141 s % 81.54/11.89 % (2640128)Peak memory usage: 11 MB % 81.54/11.89 % (2640128)Instructions burned: 181 (million) % 81.54/11.89 % (2640134)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1686817007:fmbsr=1.3:i=865:ins=25_2996 on theBenchmark for (2996ds/865Mi) % 81.54/11.89 % TRYING [1] % 81.54/11.89 % TRYING [2] % 81.54/11.89 % TRYING [3] % 81.54/11.89 % (2640124)Instruction limit reached! % 81.54/11.89 % (2640124)------------------------------ % 81.54/11.89 % (2640124)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 81.54/11.89 % (2640124)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 81.54/11.89 % (2640124)CaDiCaL version: 2.1.3 % 81.54/11.89 % (2640124)Termination reason: Instruction limit % 81.54/11.89 % (2640124)Termination phase: Finite model building SAT solving % 81.54/11.89 % (2640124)Time elapsed: 0.337 s % 81.54/11.89 % (2640124)Peak memory usage: 19 MB % 81.54/11.89 % (2640124)Instructions burned: 715 (million) % 81.54/11.89 % TRYING [4] % 81.54/11.89 % (2640136)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3629007235:i=1179_2995 on theBenchmark for (2995ds/1179Mi) % 81.54/11.89 % TRYING [5] % 81.54/11.89 % (2640132)Instruction limit reached! % 81.54/11.89 % (2640132)------------------------------ % 81.54/11.89 % (2640132)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 81.54/11.89 % (2640132)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 81.54/11.89 % (2640132)CaDiCaL version: 2.1.3 % 81.54/11.89 % (2640132)Termination reason: Instruction limit % 81.54/11.89 % (2640132)Termination phase: Saturation % 81.54/11.89 % (2640132)Time elapsed: 0.369 s % 81.54/11.89 % (2640132)Peak memory usage: 13 MB % 81.54/11.89 % (2640132)Instructions burned: 477 (million) % 81.54/11.89 % (2640127)Instruction limit reached! % 81.54/11.89 % (2640127)------------------------------ % 81.54/11.89 % (2640127)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 81.54/11.89 % (2640127)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 81.54/11.89 % (2640127)CaDiCaL version: 2.1.3 % 81.54/11.89 % (2640127)Termination reason: Instruction limit % 81.54/11.89 % (2640127)Termination phase: Saturation % 81.54/11.89 % (2640127)Time elapsed: 0.523 s % 81.54/11.89 % (2640127)Peak memory usage: 15 MB % 81.54/11.89 % (2640127)Instructions burned: 685 (million) % 81.54/11.89 % (2640138)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2252196625:i=889:ins=1_2993 on theBenchmark for (2993ds/889Mi) % 81.54/11.89 % (2640139)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=950919023:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2993 on theBenchmark for (2993ds/692Mi) % 81.54/11.89 % TRYING [5] % 81.54/11.89 % (2640136)Instruction limit reached! % 81.54/11.89 % (2640136)------------------------------ % 81.54/11.89 % (2640136)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 81.54/11.89 % (2640136)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 81.54/11.89 % (2640136)CaDiCaL version: 2.1.3 % 81.54/11.89 % (2640136)Termination reason: Instruction limit % 81.54/11.89 % (2640136)Termination phase: Saturation % 81.54/11.89 % (2640136)Time elapsed: 0.518 s % 81.54/11.89 % (2640136)Peak memory usage: 21 MB % 81.54/11.89 % (2640136)Instructions burned: 1180 (million) % 81.54/11.89 % (2640134)Instruction limit reached! % 81.54/11.89 % (2640134)------------------------------ % 81.54/11.89 % (2640134)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 81.54/11.89 % (2640134)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 162.54/23.28 % (2640134)CaDiCaL version: 2.1.3 % 162.54/23.28 % (2640134)Termination reason: Instruction limit % 162.54/23.28 % (2640134)Termination phase: Finite model building SAT solving % 162.54/23.28 % (2640134)Time elapsed: 0.681 s % 162.54/23.28 % (2640134)Peak memory usage: 21 MB % 162.54/23.28 % (2640134)Instructions burned: 865 (million) % 162.54/23.28 % (2640142)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=604377314:i=879:kws=inv_precedence:fsr=off_2989 on theBenchmark for (2989ds/879Mi) % 162.54/23.28 % (2640143)fmb+10_1_sil=64000:random_seed=3700477849:i=22061:nm=2:gsp=on_2989 on theBenchmark for (2989ds/22061Mi) % 162.54/23.28 % TRYING [1] % 162.54/23.28 % TRYING [2] % 162.54/23.28 % TRYING [3] % 162.54/23.28 % TRYING [14] % 162.54/23.28 % TRYING [4] % 162.54/23.28 % (2640139)Instruction limit reached! % 162.54/23.28 % (2640139)------------------------------ % 162.54/23.28 % (2640139)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 162.54/23.28 % (2640139)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 162.54/23.28 % (2640139)CaDiCaL version: 2.1.3 % 162.54/23.28 % (2640139)Termination reason: Instruction limit % 162.54/23.28 % (2640139)Termination phase: Saturation % 162.54/23.28 % (2640139)Time elapsed: 0.557 s % 162.54/23.28 % (2640139)Peak memory usage: 14 MB % 162.54/23.28 % (2640139)Instructions burned: 693 (million) % 162.54/23.28 % (2640146)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1025528082:i=9515:nm=5_2987 on theBenchmark for (2987ds/9515Mi) % 162.54/23.28 % TRYING [20] % 162.54/23.28 % (2640138)Instruction limit reached! % 162.54/23.28 % (2640138)------------------------------ % 162.54/23.28 % (2640138)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 162.54/23.28 % (2640138)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 162.54/23.28 % (2640138)CaDiCaL version: 2.1.3 % 162.54/23.28 % (2640138)Termination reason: Instruction limit % 162.54/23.28 % (2640138)Termination phase: Finite model building constraint generation % 162.54/23.28 % (2640138)Time elapsed: 0.702 s % 162.54/23.28 % (2640138)Peak memory usage: 91 MB % 162.54/23.28 % (2640138)Instructions burned: 890 (million) % 162.54/23.28 % (2640148)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2836193832:fmbsr=1.7:i=920_2985 on theBenchmark for (2985ds/920Mi) % 162.54/23.28 % TRYING [8] % 162.54/23.28 % TRYING [5] % 162.54/23.28 % (2640142)Instruction limit reached! % 162.54/23.28 % (2640142)------------------------------ % 162.54/23.28 % (2640142)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 162.54/23.28 % (2640142)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 162.54/23.28 % (2640142)CaDiCaL version: 2.1.3 % 162.54/23.28 % (2640142)Termination reason: Instruction limit % 162.54/23.28 % (2640142)Termination phase: Saturation % 162.54/23.28 % (2640142)Time elapsed: 0.497 s % 162.54/23.28 % (2640142)Peak memory usage: 17 MB % 162.54/23.28 % (2640142)Instructions burned: 881 (million) % 162.54/23.28 % (2640150)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=738322424:i=5131_2984 on theBenchmark for (2984ds/5131Mi) % 162.54/23.28 % (2640148)Instruction limit reached! % 162.54/23.28 % (2640148)------------------------------ % 162.54/23.28 % (2640148)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 162.54/23.28 % (2640148)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 162.54/23.28 % (2640148)CaDiCaL version: 2.1.3 % 162.54/23.28 % (2640148)Termination reason: Instruction limit % 162.54/23.28 % (2640148)Termination phase: Finite model building constraint generation % 162.54/23.28 % (2640148)Time elapsed: 0.401 s % 162.54/23.28 % (2640148)Peak memory usage: 73 MB % 162.54/23.28 % (2640148)Instructions burned: 920 (million) % 162.54/23.28 % (2640152)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=456655576:i=1472:ins=7:fdi=8:gsp=on_2981 on theBenchmark for (2981ds/1472Mi) % 162.54/23.28 % (2640152)Instruction limit reached! % 162.54/23.28 % (2640152)------------------------------ % 162.54/23.28 % (2640152)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 162.54/23.28 % (2640152)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 162.54/23.28 % (2640152)CaDiCaL version: 2.1.3 % 162.54/23.28 % (2640152)Termination reason: Instruction limit % 162.54/23.28 % (2640152)Termination phase: Saturation % 162.54/23.28 % (2640152)Time elapsed: 1.230 s % 162.54/23.28 % (2640152)Peak memory usage: 26 MB % 162.54/23.28 % (2640152)Instructions burned: 1472 (million) % 162.54/23.28 % (2640156)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=676919058:i=6324_2968 on theBenchmark for (2968ds/6324Mi) % 162.54/23.28 % TRYING [77] % 162.54/23.28 % TRYING [6] % 162.54/23.28 % TRYING [6] % 162.54/23.28 % (2640150)InstructioTerminated % 300.24/42.64 % Vampire exiting %------------------------------------------------------------------------------