%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW447-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 : n002.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:02 PM UTC 2026 % Result : Timeout 300.40s 42.63s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWW447-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.09/0.19 % Computer : n002.cluster.edu % 0.09/0.19 % Model : x86_64 x86_64 % 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.19 % Memory : 8046.5625MB % 0.09/0.19 % OS : Linux 6.8.0-71-generic % 0.09/0.19 % CPULimit : 300 % 0.09/0.19 % WCLimit : 300 % 0.09/0.19 % DateTime : Mon Sep 28 13:58:52 UTC 2026 % 0.09/0.19 % CPUTime : % 0.09/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.09/0.23 Running first-order model finding % 0.09/0.23 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 % 25.20/3.87 % (361520)Will run a generic schedule for satisfiability detection. % 25.20/3.87 % (361525)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2761912455_2999 on theBenchmark for (2999ds/0Mi) % 25.20/3.87 % TRYING [1] % 25.20/3.87 % TRYING [2] % 25.20/3.87 % (361526)% WARNING: option uhcvi not known. % 25.20/3.87 % TRYING [3] % 25.20/3.87 % (361526)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2178778706:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 25.20/3.87 % (361527)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3171103397:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 25.20/3.87 % (361528)dis+10_1_sil=32000:sp=arity:random_seed=913776772:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 25.20/3.87 % (361530)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2022895964:i=131_2999 on theBenchmark for (2999ds/131Mi) % 25.20/3.87 % (361529)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=636621942:i=116_2999 on theBenchmark for (2999ds/116Mi) % 25.20/3.87 % (361531)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=870087131:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 25.20/3.87 % TRYING [4] % 25.20/3.87 % (361528)Instruction limit reached! % 25.20/3.87 % (361528)------------------------------ % 25.20/3.87 % (361528)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 25.20/3.87 % (361528)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.20/3.87 % (361528)CaDiCaL version: 2.1.3 % 25.20/3.87 % (361528)Termination reason: Instruction limit % 25.20/3.87 % (361528)Termination phase: Saturation % 25.20/3.87 % (361528)Time elapsed: 0.061 s % 25.20/3.87 % (361528)Peak memory usage: 12 MB % 25.20/3.87 % (361528)Instructions burned: 103 (million) % 25.20/3.87 % (361529)Instruction limit reached! % 25.20/3.87 % (361529)------------------------------ % 25.20/3.87 % (361529)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 25.20/3.87 % (361529)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.20/3.87 % (361529)CaDiCaL version: 2.1.3 % 25.20/3.87 % (361529)Termination reason: Instruction limit % 25.20/3.87 % (361529)Termination phase: Saturation % 25.20/3.87 % (361529)Time elapsed: 0.063 s % 25.20/3.87 % (361529)Peak memory usage: 12 MB % 25.20/3.87 % (361529)Instructions burned: 117 (million) % 25.20/3.87 % (361530)Instruction limit reached! % 25.20/3.87 % (361530)------------------------------ % 25.20/3.87 % (361530)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 25.20/3.87 % (361530)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.20/3.87 % (361530)CaDiCaL version: 2.1.3 % 25.20/3.87 % (361530)Termination reason: Instruction limit % 25.20/3.87 % (361530)Termination phase: Saturation % 25.20/3.87 % (361530)Time elapsed: 0.069 s % 25.20/3.87 % (361530)Peak memory usage: 12 MB % 25.20/3.87 % (361530)Instructions burned: 131 (million) % 25.20/3.87 % (361539)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2586585930:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi) % 25.20/3.87 % (361531)Instruction limit reached! % 25.20/3.87 % (361531)------------------------------ % 25.20/3.87 % (361531)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 25.20/3.87 % (361531)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.20/3.87 % (361531)CaDiCaL version: 2.1.3 % 25.20/3.87 % (361531)Termination reason: Instruction limit % 25.20/3.87 % (361531)Termination phase: Saturation % 25.20/3.87 % (361531)Time elapsed: 0.082 s % 25.20/3.87 % (361531)Peak memory usage: 12 MB % 25.20/3.87 % (361531)Instructions burned: 160 (million) % 25.20/3.87 % TRYING [5] % 25.20/3.87 % (361540)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3663408998:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi) % 25.20/3.87 % TRYING [1] % 25.20/3.87 % TRYING [2] % 25.20/3.87 % (361541)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=3295846015:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 25.20/3.87 % TRYING [3] % 25.20/3.87 % (361544)ott-21_1_sil=16000:fs=off:random_seed=3736829797:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 25.20/3.87 % TRYING [4] % 25.20/3.87 % (361540)Instruction limit reached! % 25.20/3.87 % (361540)------------------------------ % 25.20/3.87 % (361540)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 25.20/3.87 % (361540)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.87/7.17 % (361540)CaDiCaL version: 2.1.3 % 48.87/7.17 % (361540)Termination reason: Instruction limit % 48.87/7.17 % (361540)Termination phase: Saturation % 48.87/7.17 % (361540)Time elapsed: 0.073 s % 48.87/7.17 % (361540)Peak memory usage: 12 MB % 48.87/7.17 % (361540)Instructions burned: 131 (million) % 48.87/7.17 % (361544)Instruction limit reached! % 48.87/7.17 % (361544)------------------------------ % 48.87/7.17 % (361544)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 48.87/7.17 % (361544)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.87/7.17 % (361544)CaDiCaL version: 2.1.3 % 48.87/7.17 % (361544)Termination reason: Instruction limit % 48.87/7.17 % (361544)Termination phase: Saturation % 48.87/7.17 % (361544)Time elapsed: 0.072 s % 48.87/7.17 % (361544)Peak memory usage: 11 MB % 48.87/7.17 % (361544)Instructions burned: 183 (million) % 48.87/7.17 % (361547)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1796754054:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi) % 48.87/7.17 % (361548)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=813695159:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi) % 48.87/7.17 % TRYING [1] % 48.87/7.17 % TRYING [2] % 48.87/7.17 % TRYING [3] % 48.87/7.17 % TRYING [4] % 48.87/7.17 % (361541)Instruction limit reached! % 48.87/7.17 % (361541)------------------------------ % 48.87/7.17 % (361541)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 48.87/7.17 % (361541)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.87/7.17 % (361541)CaDiCaL version: 2.1.3 % 48.87/7.17 % (361541)Termination reason: Instruction limit % 48.87/7.17 % (361541)Termination phase: Saturation % 48.87/7.17 % (361541)Time elapsed: 0.314 s % 48.87/7.17 % (361541)Peak memory usage: 15 MB % 48.87/7.17 % (361541)Instructions burned: 684 (million) % 48.87/7.17 % (361547)Instruction limit reached! % 48.87/7.17 % (361547)------------------------------ % 48.87/7.17 % (361547)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 48.87/7.17 % (361547)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.87/7.17 % (361547)CaDiCaL version: 2.1.3 % 48.87/7.17 % (361547)Termination reason: Instruction limit % 48.87/7.17 % (361547)Termination phase: Saturation % 48.87/7.17 % (361547)Time elapsed: 0.240 s % 48.87/7.17 % (361547)Peak memory usage: 13 MB % 48.87/7.17 % (361547)Instructions burned: 478 (million) % 48.87/7.17 % (361551)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1218440717:i=1179_2995 on theBenchmark for (2995ds/1179Mi) % 48.87/7.17 % (361552)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2736931179:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi) % 48.87/7.17 % (361539)Instruction limit reached! % 48.87/7.17 % (361539)------------------------------ % 48.87/7.17 % (361539)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 48.87/7.17 % (361539)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.87/7.17 % (361539)CaDiCaL version: 2.1.3 % 48.87/7.17 % (361539)Termination reason: Instruction limit % 48.87/7.17 % (361539)Termination phase: Finite model building SAT solving % 48.87/7.17 % (361539)Time elapsed: 0.406 s % 48.87/7.17 % (361539)Peak memory usage: 19 MB % 48.87/7.17 % (361539)Instructions burned: 714 (million) % 48.87/7.17 % (361555)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=4202079755: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) % 48.87/7.17 % (361548)Instruction limit reached! % 48.87/7.17 % (361548)------------------------------ % 48.87/7.17 % (361548)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 48.87/7.17 % (361548)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.87/7.17 % (361548)CaDiCaL version: 2.1.3 % 48.87/7.17 % (361548)Termination reason: Instruction limit % 48.87/7.17 % (361548)Termination phase: Finite model building SAT solving % 48.87/7.17 % (361548)Time elapsed: 0.451 s % 48.87/7.17 % (361548)Peak memory usage: 15 MB % 48.87/7.17 % (361548)Instructions burned: 866 (million) % 48.87/7.17 % TRYING [14] % 48.87/7.17 % (361557)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3172991235:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi) % 48.87/7.17 % (361552)Instruction limit reached! % 48.87/7.17 % (361552)------------------------------ % 48.87/7.17 % (361552)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 48.87/7.17 % (361552)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.14/18.69 % (361552)CaDiCaL version: 2.1.3 % 130.14/18.69 % (361552)Termination reason: Instruction limit % 130.14/18.69 % (361552)Termination phase: Finite model building constraint generation % 130.14/18.69 % (361552)Time elapsed: 0.362 s % 130.14/18.69 % (361552)Peak memory usage: 90 MB % 130.14/18.69 % (361552)Instructions burned: 889 (million) % 130.14/18.69 % (361559)fmb+10_1_sil=64000:random_seed=2142076570:i=22061:nm=2:gsp=on_2991 on theBenchmark for (2991ds/22061Mi) % 130.14/18.69 % (361555)Instruction limit reached! % 130.14/18.69 % (361555)------------------------------ % 130.14/18.69 % (361555)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 130.14/18.69 % (361555)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.14/18.69 % (361555)CaDiCaL version: 2.1.3 % 130.14/18.69 % (361555)Termination reason: Instruction limit % 130.14/18.69 % (361555)Termination phase: Saturation % 130.14/18.69 % (361555)Time elapsed: 0.320 s % 130.14/18.69 % (361555)Peak memory usage: 15 MB % 130.14/18.69 % (361555)Instructions burned: 693 (million) % 130.14/18.69 % TRYING [6] % 130.14/18.69 % TRYING [1] % 130.14/18.69 % TRYING [2] % 130.14/18.69 % TRYING [3] % 130.14/18.69 % (361561)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3215137995:i=9515:nm=5_2991 on theBenchmark for (2991ds/9515Mi) % 130.14/18.69 % TRYING [20] % 130.14/18.69 % TRYING [4] % 130.14/18.69 % (361551)Instruction limit reached! % 130.14/18.69 % (361551)------------------------------ % 130.14/18.69 % (361551)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 130.14/18.69 % (361551)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.14/18.69 % (361551)CaDiCaL version: 2.1.3 % 130.14/18.69 % (361551)Termination reason: Instruction limit % 130.14/18.69 % (361551)Termination phase: Saturation % 130.14/18.69 % (361551)Time elapsed: 0.607 s % 130.14/18.69 % (361551)Peak memory usage: 22 MB % 130.14/18.69 % (361551)Instructions burned: 1180 (million) % 130.14/18.69 % (361563)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2155374562:fmbsr=1.7:i=920_2989 on theBenchmark for (2989ds/920Mi) % 130.14/18.69 % TRYING [8] % 130.14/18.69 % (361557)Instruction limit reached! % 130.14/18.69 % (361557)------------------------------ % 130.14/18.69 % (361557)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 130.14/18.69 % (361557)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.14/18.69 % (361557)CaDiCaL version: 2.1.3 % 130.14/18.69 % (361557)Termination reason: Instruction limit % 130.14/18.69 % (361557)Termination phase: Saturation % 130.14/18.69 % (361557)Time elapsed: 0.472 s % 130.14/18.69 % (361557)Peak memory usage: 16 MB % 130.14/18.69 % (361557)Instructions burned: 879 (million) % 130.14/18.69 % (361565)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=4111688051:i=5131_2988 on theBenchmark for (2988ds/5131Mi) % 130.14/18.69 % (361563)Instruction limit reached! % 130.14/18.69 % (361563)------------------------------ % 130.14/18.69 % (361563)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 130.14/18.69 % (361563)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.14/18.69 % (361563)CaDiCaL version: 2.1.3 % 130.14/18.69 % (361563)Termination reason: Instruction limit % 130.14/18.69 % (361563)Termination phase: Finite model building constraint generation % 130.14/18.69 % (361563)Time elapsed: 0.350 s % 130.14/18.69 % (361563)Peak memory usage: 73 MB % 130.14/18.69 % (361563)Instructions burned: 922 (million) % 130.14/18.69 % (361567)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3641407761:i=1472:ins=7:fdi=8:gsp=on_2985 on theBenchmark for (2985ds/1472Mi) % 130.14/18.69 % TRYING [5] % 130.14/18.69 % (361567)Instruction limit reached! % 130.14/18.69 % (361567)------------------------------ % 130.14/18.69 % (361567)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 130.14/18.69 % (361567)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.14/18.69 % (361567)CaDiCaL version: 2.1.3 % 130.14/18.69 % (361567)Termination reason: Instruction limit % 130.14/18.69 % (361567)Termination phase: Saturation % 130.14/18.69 % (361567)Time elapsed: 0.654 s % 130.14/18.69 % (361567)Peak memory usage: 22 MB % 130.14/18.69 % (361567)Instructions burned: 1474 (million) % 130.14/18.69 % (361569)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1216668307:i=6324_2978 on theBenchmark for (2978ds/6324Mi) % 130.14/18.69 % TRYING [77] % 130.14/18.69 % (361565)Instruction limit reached! % 130.14/18.69 % (361565)------------------------------ % 130.14/18.69 % (361565)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 130.14/18.69 % (361565)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42bTerminated % 300.40/42.63 % Vampire exiting %------------------------------------------------------------------------------