%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW472+7 : TPTP v9.3.1. Released v5.3.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:40:08 PM UTC 2026 % Result : Timeout 300.33s 42.64s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWW472+7 : TPTP v9.3.1. Released v5.3.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.10/0.20 % Computer : n001.cluster.edu % 0.10/0.20 % Model : x86_64 x86_64 % 0.10/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.20 % Memory : 8046.5625MB % 0.10/0.20 % OS : Linux 6.8.0-71-generic % 0.10/0.20 % CPULimit : 300 % 0.10/0.20 % WCLimit : 300 % 0.10/0.20 % DateTime : Mon Sep 28 14:11:33 UTC 2026 % 0.10/0.21 % CPUTime : % 0.10/0.21 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.10/0.24 Running first-order model finding % 0.10/0.24 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 % 26.93/4.19 % (364160)Will run a generic schedule for satisfiability detection. % 26.93/4.19 % (364165)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2483847297_2998 on theBenchmark for (2998ds/0Mi) % 26.93/4.19 % (364166)% WARNING: option uhcvi not known. % 26.93/4.19 % (364166)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2521931144:i=135531:add=off:rawr=on_2998 on theBenchmark for (2998ds/135531Mi) % 26.93/4.19 % (364167)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4052694056:i=88024:add=on:rawr=on_2998 on theBenchmark for (2998ds/88024Mi) % 26.93/4.19 % (364168)dis+10_1_sil=32000:sp=arity:random_seed=164407044:i=103:fgj=on_2998 on theBenchmark for (2998ds/103Mi) % 26.93/4.19 % (364169)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1961971056:i=116_2998 on theBenchmark for (2998ds/116Mi) % 26.93/4.19 % (364170)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=97560174:i=131_2998 on theBenchmark for (2998ds/131Mi) % 26.93/4.19 % (364171)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=689501955:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2998 on theBenchmark for (2998ds/159Mi) % 26.93/4.19 % (364168)Instruction limit reached! % 26.93/4.19 % (364168)------------------------------ % 26.93/4.19 % (364168)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 26.93/4.19 % (364168)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.93/4.19 % (364168)CaDiCaL version: 2.1.3 % 26.93/4.19 % (364168)Termination reason: Instruction limit % 26.93/4.19 % (364168)Termination phase: Property scanning % 26.93/4.19 % (364168)Time elapsed: 0.044 s % 26.93/4.19 % (364168)Peak memory usage: 13 MB % 26.93/4.19 % (364168)Instructions burned: 104 (million) % 26.93/4.19 % (364169)Instruction limit reached! % 26.93/4.19 % (364169)------------------------------ % 26.93/4.19 % (364169)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 26.93/4.19 % (364169)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.93/4.19 % (364169)CaDiCaL version: 2.1.3 % 26.93/4.19 % (364169)Termination reason: Instruction limit % 26.93/4.19 % (364169)Termination phase: Equality resolution with deletion % 26.93/4.19 % (364169)Time elapsed: 0.050 s % 26.93/4.19 % (364169)Peak memory usage: 13 MB % 26.93/4.19 % (364169)Instructions burned: 118 (million) % 26.93/4.19 % (364170)Instruction limit reached! % 26.93/4.19 % (364170)------------------------------ % 26.93/4.19 % (364170)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 26.93/4.19 % (364170)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.93/4.19 % (364170)CaDiCaL version: 2.1.3 % 26.93/4.19 % (364170)Termination reason: Instruction limit % 26.93/4.19 % (364170)Termination phase: Property scanning % 26.93/4.19 % (364170)Time elapsed: 0.055 s % 26.93/4.19 % (364170)Peak memory usage: 13 MB % 26.93/4.19 % (364170)Instructions burned: 134 (million) % 26.93/4.19 % (364179)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3366404217:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi) % 26.93/4.19 % (364180)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2481666360:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi) % 26.93/4.19 % (364171)Instruction limit reached! % 26.93/4.19 % (364171)------------------------------ % 26.93/4.19 % (364171)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 26.93/4.19 % (364171)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.93/4.19 % (364171)CaDiCaL version: 2.1.3 % 26.93/4.19 % (364171)Termination reason: Instruction limit % 26.93/4.19 % (364171)Termination phase: Property scanning % 26.93/4.19 % (364171)Time elapsed: 0.070 s % 26.93/4.19 % (364171)Peak memory usage: 13 MB % 26.93/4.19 % (364171)Instructions burned: 161 (million) % 26.93/4.19 % (364181)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=1422735219:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 26.93/4.19 % (364184)ott-21_1_sil=16000:fs=off:random_seed=2897317440:i=180:av=off:fsr=off_2997 on theBenchmark for (2997ds/180Mi) % 26.93/4.19 % (364180)Instruction limit reached! % 26.93/4.19 % (364180)------------------------------ % 26.93/4.19 % (364180)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 26.93/4.19 % (364180)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.93/4.19 % (364180)CaDiCaL version: 2.1.3 % 58.59/8.65 % (364180)Termination reason: Instruction limit % 58.59/8.65 % (364180)Termination phase: Property scanning % 58.59/8.65 % (364180)Time elapsed: 0.055 s % 58.59/8.65 % (364180)Peak memory usage: 13 MB % 58.59/8.65 % (364180)Instructions burned: 132 (million) % 58.59/8.65 % (364187)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3285242357:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi) % 58.59/8.65 % (364184)Instruction limit reached! % 58.59/8.65 % (364184)------------------------------ % 58.59/8.65 % (364184)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 58.59/8.65 % (364184)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 58.59/8.65 % (364184)CaDiCaL version: 2.1.3 % 58.59/8.65 % (364184)Termination reason: Instruction limit % 58.59/8.65 % (364184)Termination phase: Property scanning % 58.59/8.65 % (364184)Time elapsed: 0.072 s % 58.59/8.65 % (364184)Peak memory usage: 13 MB % 58.59/8.65 % (364184)Instructions burned: 183 (million) % 58.59/8.65 % (364189)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3940414294:fmbsr=1.3:i=865:ins=25_2996 on theBenchmark for (2996ds/865Mi) % 58.59/8.65 % (364179)Instruction limit reached! % 58.59/8.65 % (364179)------------------------------ % 58.59/8.65 % (364179)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 58.59/8.65 % (364179)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 58.59/8.65 % (364179)CaDiCaL version: 2.1.3 % 58.59/8.65 % (364179)Termination reason: Instruction limit % 58.59/8.65 % (364179)Termination phase: Finite model building preprocessing % 58.59/8.65 % (364179)Time elapsed: 0.315 s % 58.59/8.65 % (364179)Peak memory usage: 19 MB % 58.59/8.65 % (364179)Instructions burned: 715 (million) % 58.59/8.65 % (364187)Instruction limit reached! % 58.59/8.65 % (364187)------------------------------ % 58.59/8.65 % (364187)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 58.59/8.65 % (364187)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 58.59/8.65 % (364187)CaDiCaL version: 2.1.3 % 58.59/8.65 % (364187)Termination reason: Instruction limit % 58.59/8.65 % (364187)Termination phase: Saturation % 58.59/8.65 % (364187)Time elapsed: 0.241 s % 58.59/8.65 % (364187)Peak memory usage: 16 MB % 58.59/8.65 % (364187)Instructions burned: 478 (million) % 58.59/8.65 % (364191)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2354815028:i=1179_2994 on theBenchmark for (2994ds/1179Mi) % 58.59/8.65 % (364192)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=15524201:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi) % 58.59/8.65 % (364181)Instruction limit reached! % 58.59/8.65 % (364181)------------------------------ % 58.59/8.65 % (364181)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 58.59/8.65 % (364181)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 58.59/8.65 % (364181)CaDiCaL version: 2.1.3 % 58.59/8.65 % (364181)Termination reason: Instruction limit % 58.59/8.65 % (364181)Termination phase: Saturation % 58.59/8.65 % (364181)Time elapsed: 0.349 s % 58.59/8.65 % (364181)Peak memory usage: 18 MB % 58.59/8.65 % (364181)Instructions burned: 686 (million) % 58.59/8.65 % (364195)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=90032872: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) % 58.59/8.65 % (364189)Instruction limit reached! % 58.59/8.65 % (364189)------------------------------ % 58.59/8.65 % (364189)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 58.59/8.65 % (364189)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 58.59/8.65 % (364189)CaDiCaL version: 2.1.3 % 58.59/8.65 % (364189)Termination reason: Instruction limit % 58.59/8.65 % (364189)Termination phase: Finite model building preprocessing % 58.59/8.65 % (364189)Time elapsed: 0.393 s % 58.59/8.65 % (364189)Peak memory usage: 20 MB % 58.59/8.65 % (364189)Instructions burned: 867 (million) % 58.59/8.65 % (364197)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2613208406:i=879:kws=inv_precedence:fsr=off_2992 on theBenchmark for (2992ds/879Mi) % 58.59/8.65 % (364195)Instruction limit reached! % 58.59/8.65 % (364195)------------------------------ % 58.59/8.65 % (364195)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 58.59/8.65 % (364195)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 58.59/8.65 % (364195)CaDiCaL version: 2.1.3 % 58.59/8.65 % (364195)Termination reason: Instruction limit % 136.74/19.63 % (364195)Termination phase: Saturation % 136.74/19.63 % (364195)Time elapsed: 0.350 s % 136.74/19.63 % (364195)Peak memory usage: 19 MB % 136.74/19.63 % (364195)Instructions burned: 692 (million) % 136.74/19.63 % (364192)Instruction limit reached! % 136.74/19.63 % (364192)------------------------------ % 136.74/19.63 % (364192)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 136.74/19.63 % (364192)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.74/19.63 % (364192)CaDiCaL version: 2.1.3 % 136.74/19.63 % (364192)Termination reason: Instruction limit % 136.74/19.63 % (364192)Termination phase: Finite model building preprocessing % 136.74/19.63 % (364192)Time elapsed: 0.404 s % 136.74/19.63 % (364192)Peak memory usage: 20 MB % 136.74/19.63 % (364192)Instructions burned: 891 (million) % 136.74/19.63 % (364199)fmb+10_1_sil=64000:random_seed=263775947:i=22061:nm=2:gsp=on_2990 on theBenchmark for (2990ds/22061Mi) % 136.74/19.63 % (364200)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3831871867:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi) % 136.74/19.63 % (364197)Instruction limit reached! % 136.74/19.63 % (364197)------------------------------ % 136.74/19.63 % (364197)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 136.74/19.63 % (364197)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.74/19.63 % (364197)CaDiCaL version: 2.1.3 % 136.74/19.63 % (364197)Termination reason: Instruction limit % 136.74/19.63 % (364197)Termination phase: Saturation % 136.74/19.63 % (364197)Time elapsed: 0.404 s % 136.74/19.63 % (364197)Peak memory usage: 20 MB % 136.74/19.63 % (364197)Instructions burned: 879 (million) % 136.74/19.63 % (364191)Instruction limit reached! % 136.74/19.63 % (364191)------------------------------ % 136.74/19.63 % (364191)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 136.74/19.63 % (364191)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.74/19.63 % (364191)CaDiCaL version: 2.1.3 % 136.74/19.63 % (364191)Termination reason: Instruction limit % 136.74/19.63 % (364191)Termination phase: Saturation % 136.74/19.63 % (364191)Time elapsed: 0.623 s % 136.74/19.63 % (364191)Peak memory usage: 22 MB % 136.74/19.63 % (364191)Instructions burned: 1180 (million) % 136.74/19.63 % (364203)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1515986927:fmbsr=1.7:i=920_2988 on theBenchmark for (2988ds/920Mi) % 136.74/19.63 % (364205)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=135385804:i=5131_2988 on theBenchmark for (2988ds/5131Mi) % 136.74/19.63 % (364203)Instruction limit reached! % 136.74/19.63 % (364203)------------------------------ % 136.74/19.63 % (364203)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 136.74/19.63 % (364203)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.74/19.63 % (364203)CaDiCaL version: 2.1.3 % 136.74/19.63 % (364203)Termination reason: Instruction limit % 136.74/19.63 % (364203)Termination phase: Finite model building preprocessing % 136.74/19.63 % (364203)Time elapsed: 0.418 s % 136.74/19.63 % (364203)Peak memory usage: 20 MB % 136.74/19.63 % (364203)Instructions burned: 921 (million) % 136.74/19.63 % (364207)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=4091585302:i=1472:ins=7:fdi=8:gsp=on_2984 on theBenchmark for (2984ds/1472Mi) % 136.74/19.63 % (364207)Instruction limit reached! % 136.74/19.63 % (364207)------------------------------ % 136.74/19.63 % (364207)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 136.74/19.63 % (364207)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.74/19.63 % (364207)CaDiCaL version: 2.1.3 % 136.74/19.63 % (364207)Termination reason: Instruction limit % 136.74/19.63 % (364207)Termination phase: Saturation % 136.74/19.63 % (364207)Time elapsed: 0.747 s % 136.74/19.63 % (364207)Peak memory usage: 30 MB % 136.74/19.63 % (364207)Instructions burned: 1473 (million) % 136.74/19.63 % (364209)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1515532380:i=6324_2976 on theBenchmark for (2976ds/6324Mi) % 136.74/19.63 % TRYING [1] % 136.74/19.63 % TRYING [2] % 136.74/19.63 % (364205)Instruction limit reached! % 136.74/19.63 % (364205)------------------------------ % 136.74/19.63 % (364205)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 136.74/19.63 % (364205)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.74/19.63 % (364205)CaDiCaL version: 2.1.3 % 136.74/19.63 % (364205)Termination reason: Instruction limit % 136.74/19.63 % (364205)Termination phase: Saturation % 136.74/19.63 % (364205)Time elapsed: 2.750 s % 136.74/19.63 % (364205)Peak memory usage: 33 MB % 136.74/19.63 % Terminated % 300.33/42.64 % Vampire exiting % 300.33/42.64 Terminated %------------------------------------------------------------------------------