%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW476+6 : 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 : n008.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:14 PM UTC 2026 % Result : Timeout 300.43s 43.18s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.04 % Problem : SWW476+6 : TPTP v9.3.1. Released v5.3.0. % 0.00/0.08 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.13/0.24 % Computer : n008.cluster.edu % 0.13/0.24 % Model : x86_64 x86_64 % 0.13/0.24 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.24 % Memory : 8046.5625MB % 0.13/0.24 % OS : Linux 6.8.0-71-generic % 0.13/0.24 % CPULimit : 300 % 0.13/0.24 % WCLimit : 300 % 0.13/0.24 % DateTime : Mon Sep 28 14:12:24 UTC 2026 % 0.13/0.25 % CPUTime : % 0.13/0.25 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.26/0.30 Running first-order model finding % 0.26/0.30 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 % 37.68/6.16 % (2269915)Will run a generic schedule for satisfiability detection. % 37.68/6.16 % (2269925)dis+10_1_sil=32000:sp=arity:random_seed=3036160938:i=103:fgj=on_2993 on theBenchmark for (2993ds/103Mi) % 37.68/6.16 % (2269922)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1303153394_2993 on theBenchmark for (2993ds/0Mi) % 37.68/6.16 % (2269923)% WARNING: option uhcvi not known. % 37.68/6.16 % (2269924)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1473179504:i=88024:add=on:rawr=on_2993 on theBenchmark for (2993ds/88024Mi) % 37.68/6.16 % (2269927)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3900821120:i=131_2993 on theBenchmark for (2993ds/131Mi) % 37.68/6.16 % (2269928)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3167806593:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2993 on theBenchmark for (2993ds/159Mi) % 37.68/6.16 % (2269926)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2920527059:i=116_2993 on theBenchmark for (2993ds/116Mi) % 37.68/6.16 % (2269923)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3888217496:i=135531:add=off:rawr=on_2993 on theBenchmark for (2993ds/135531Mi) % 37.68/6.16 % (2269925)Instruction limit reached! % 37.68/6.16 % (2269925)------------------------------ % 37.68/6.16 % (2269925)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 37.68/6.16 % (2269925)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.68/6.16 % (2269925)CaDiCaL version: 2.1.3 % 37.68/6.16 % (2269925)Termination reason: Instruction limit % 37.68/6.16 % (2269925)Termination phase: Property scanning % 37.68/6.16 % (2269925)Time elapsed: 0.044 s % 37.68/6.16 % (2269925)Peak memory usage: 11 MB % 37.68/6.16 % (2269925)Instructions burned: 104 (million) % 37.68/6.16 % (2269936)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2679253108:i=714:nm=2_2993 on theBenchmark for (2993ds/714Mi) % 37.68/6.16 % (2269926)Instruction limit reached! % 37.68/6.16 % (2269926)------------------------------ % 37.68/6.16 % (2269926)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 37.68/6.16 % (2269926)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.68/6.16 % (2269926)CaDiCaL version: 2.1.3 % 37.68/6.16 % (2269926)Termination reason: Instruction limit % 37.68/6.16 % (2269926)Termination phase: Property scanning % 37.68/6.16 % (2269926)Time elapsed: 0.089 s % 37.68/6.16 % (2269926)Peak memory usage: 11 MB % 37.68/6.16 % (2269926)Instructions burned: 116 (million) % 37.68/6.16 % (2269927)Instruction limit reached! % 37.68/6.16 % (2269927)------------------------------ % 37.68/6.16 % (2269927)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 37.68/6.16 % (2269927)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.68/6.16 % (2269927)CaDiCaL version: 2.1.3 % 37.68/6.16 % (2269927)Termination reason: Instruction limit % 37.68/6.16 % (2269927)Termination phase: Property scanning % 37.68/6.16 % (2269927)Time elapsed: 0.102 s % 37.68/6.16 % (2269927)Peak memory usage: 11 MB % 37.68/6.16 % (2269927)Instructions burned: 132 (million) % 37.68/6.16 % (2269928)Instruction limit reached! % 37.68/6.16 % (2269928)------------------------------ % 37.68/6.16 % (2269928)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 37.68/6.16 % (2269928)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.68/6.16 % (2269928)CaDiCaL version: 2.1.3 % 37.68/6.16 % (2269928)Termination reason: Instruction limit % 37.68/6.16 % (2269928)Termination phase: Property scanning % 37.68/6.16 % (2269928)Time elapsed: 0.123 s % 37.68/6.16 % (2269928)Peak memory usage: 11 MB % 37.68/6.16 % (2269928)Instructions burned: 159 (million) % 37.68/6.16 % (2269938)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2762926610:i=131:bd=preordered:fsd=on_2992 on theBenchmark for (2992ds/131Mi) % 37.68/6.16 % (2269939)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=1809827167:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2992 on theBenchmark for (2992ds/684Mi) % 37.68/6.16 % (2269941)ott-21_1_sil=16000:fs=off:random_seed=3950790389:i=180:av=off:fsr=off_2992 on theBenchmark for (2992ds/180Mi) % 37.68/6.16 % (2269938)Instruction limit reached! % 37.68/6.16 % (2269938)------------------------------ % 37.68/6.16 % (2269938)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 37.68/6.16 % (2269938)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 69.78/10.74 % (2269938)CaDiCaL version: 2.1.3 % 69.78/10.74 % (2269938)Termination reason: Instruction limit % 69.78/10.74 % (2269938)Termination phase: Property scanning % 69.78/10.74 % (2269938)Time elapsed: 0.144 s % 69.78/10.74 % (2269938)Peak memory usage: 12 MB % 69.78/10.74 % (2269938)Instructions burned: 132 (million) % 69.78/10.74 % (2269941)Instruction limit reached! % 69.78/10.74 % (2269941)------------------------------ % 69.78/10.74 % (2269941)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 69.78/10.74 % (2269941)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 69.78/10.74 % (2269941)CaDiCaL version: 2.1.3 % 69.78/10.74 % (2269941)Termination reason: Instruction limit % 69.78/10.74 % (2269941)Termination phase: Property scanning % 69.78/10.74 % (2269941)Time elapsed: 0.139 s % 69.78/10.74 % (2269941)Peak memory usage: 11 MB % 69.78/10.74 % (2269941)Instructions burned: 180 (million) % 69.78/10.74 % (2269944)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1051615742:i=477:bd=all_2990 on theBenchmark for (2990ds/477Mi) % 69.78/10.74 % (2269936)Instruction limit reached! % 69.78/10.74 % (2269936)------------------------------ % 69.78/10.74 % (2269936)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 69.78/10.74 % (2269936)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 69.78/10.74 % (2269936)CaDiCaL version: 2.1.3 % 69.78/10.74 % (2269936)Termination reason: Instruction limit % 69.78/10.74 % (2269936)Termination phase: Finite model building preprocessing % 69.78/10.74 % (2269936)Time elapsed: 0.277 s % 69.78/10.74 % (2269936)Peak memory usage: 12 MB % 69.78/10.74 % (2269936)Instructions burned: 715 (million) % 69.78/10.74 % (2269945)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1611333138:fmbsr=1.3:i=865:ins=25_2990 on theBenchmark for (2990ds/865Mi) % 69.78/10.74 % (2269947)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2906669850:i=1179_2990 on theBenchmark for (2990ds/1179Mi) % 69.78/10.74 % (2269939)Instruction limit reached! % 69.78/10.74 % (2269939)------------------------------ % 69.78/10.74 % (2269939)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 69.78/10.74 % (2269939)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 69.78/10.74 % (2269939)CaDiCaL version: 2.1.3 % 69.78/10.74 % (2269939)Termination reason: Instruction limit % 69.78/10.74 % (2269939)Termination phase: Property scanning % 69.78/10.74 % (2269939)Time elapsed: 0.359 s % 69.78/10.74 % (2269939)Peak memory usage: 12 MB % 69.78/10.74 % (2269939)Instructions burned: 685 (million) % 69.78/10.74 % (2269950)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=169243462:i=889:ins=1_2988 on theBenchmark for (2988ds/889Mi) % 69.78/10.74 % (2269944)Instruction limit reached! % 69.78/10.74 % (2269944)------------------------------ % 69.78/10.74 % (2269944)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 69.78/10.74 % (2269944)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 69.78/10.74 % (2269944)CaDiCaL version: 2.1.3 % 69.78/10.74 % (2269944)Termination reason: Instruction limit % 69.78/10.74 % (2269944)Termination phase: Property scanning % 69.78/10.74 % (2269944)Time elapsed: 0.363 s % 69.78/10.74 % (2269944)Peak memory usage: 12 MB % 69.78/10.74 % (2269944)Instructions burned: 477 (million) % 69.78/10.74 % (2269952)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=3026026018:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2986 on theBenchmark for (2986ds/692Mi) % 69.78/10.74 % (2269950)Instruction limit reached! % 69.78/10.74 % (2269950)------------------------------ % 69.78/10.74 % (2269950)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 69.78/10.74 % (2269950)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 69.78/10.74 % (2269950)CaDiCaL version: 2.1.3 % 69.78/10.74 % (2269950)Termination reason: Instruction limit % 69.78/10.74 % (2269950)Termination phase: Finite model building preprocessing % 69.78/10.74 % (2269950)Time elapsed: 0.348 s % 69.78/10.74 % (2269950)Peak memory usage: 16 MB % 69.78/10.74 % (2269950)Instructions burned: 891 (million) % 69.78/10.74 % (2269954)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1063282651:i=879:kws=inv_precedence:fsr=off_2984 on theBenchmark for (2984ds/879Mi) % 69.78/10.74 % (2269945)Instruction limit reached! % 69.78/10.74 % (2269945)------------------------------ % 69.78/10.74 % (2269945)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 69.78/10.74 % (2269945)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 160.88/23.53 % (2269945)CaDiCaL version: 2.1.3 % 160.88/23.53 % (2269945)Termination reason: Instruction limit % 160.88/23.53 % (2269945)Termination phase: Finite model building preprocessing % 160.88/23.53 % (2269945)Time elapsed: 0.633 s % 160.88/23.53 % (2269945)Peak memory usage: 16 MB % 160.88/23.53 % (2269945)Instructions burned: 866 (million) % 160.88/23.53 % (2269956)fmb+10_1_sil=64000:random_seed=1706200272:i=22061:nm=2:gsp=on_2983 on theBenchmark for (2983ds/22061Mi) % 160.88/23.53 % (2269952)Instruction limit reached! % 160.88/23.53 % (2269952)------------------------------ % 160.88/23.53 % (2269952)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 160.88/23.53 % (2269952)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 160.88/23.53 % (2269952)CaDiCaL version: 2.1.3 % 160.88/23.53 % (2269952)Termination reason: Instruction limit % 160.88/23.53 % (2269952)Termination phase: Property scanning % 160.88/23.53 % (2269952)Time elapsed: 0.493 s % 160.88/23.53 % (2269952)Peak memory usage: 12 MB % 160.88/23.53 % (2269952)Instructions burned: 692 (million) % 160.88/23.53 % (2269958)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=384280628:i=9515:nm=5_2981 on theBenchmark for (2981ds/9515Mi) % 160.88/23.53 % (2269954)Instruction limit reached! % 160.88/23.53 % (2269954)------------------------------ % 160.88/23.53 % (2269954)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 160.88/23.53 % (2269954)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 160.88/23.53 % (2269954)CaDiCaL version: 2.1.3 % 160.88/23.53 % (2269954)Termination reason: Instruction limit % 160.88/23.53 % (2269954)Termination phase: Saturation % 160.88/23.53 % (2269954)Time elapsed: 0.359 s % 160.88/23.53 % (2269954)Peak memory usage: 13 MB % 160.88/23.53 % (2269954)Instructions burned: 881 (million) % 160.88/23.53 % (2269960)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3347827201:fmbsr=1.7:i=920_2980 on theBenchmark for (2980ds/920Mi) % 160.88/23.53 % (2269947)Instruction limit reached! % 160.88/23.53 % (2269947)------------------------------ % 160.88/23.53 % (2269947)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 160.88/23.53 % (2269947)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 160.88/23.53 % (2269947)CaDiCaL version: 2.1.3 % 160.88/23.53 % (2269947)Termination reason: Instruction limit % 160.88/23.53 % (2269947)Termination phase: Saturation % 160.88/23.53 % (2269947)Time elapsed: 0.940 s % 160.88/23.53 % (2269947)Peak memory usage: 19 MB % 160.88/23.53 % (2269947)Instructions burned: 1179 (million) % 160.88/23.53 % (2269962)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3009844684:i=5131_2980 on theBenchmark for (2980ds/5131Mi) % 160.88/23.53 % (2269960)Instruction limit reached! % 160.88/23.53 % (2269960)------------------------------ % 160.88/23.53 % (2269960)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 160.88/23.53 % (2269960)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 160.88/23.53 % (2269960)CaDiCaL version: 2.1.3 % 160.88/23.53 % (2269960)Termination reason: Instruction limit % 160.88/23.53 % (2269960)Termination phase: Finite model building preprocessing % 160.88/23.53 % (2269960)Time elapsed: 0.375 s % 160.88/23.53 % (2269960)Peak memory usage: 16 MB % 160.88/23.53 % (2269960)Instructions burned: 923 (million) % 160.88/23.53 % (2269964)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1333299824:i=1472:ins=7:fdi=8:gsp=on_2976 on theBenchmark for (2976ds/1472Mi) % 160.88/23.53 % (2269964)Instruction limit reached! % 160.88/23.53 % (2269964)------------------------------ % 160.88/23.53 % (2269964)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 160.88/23.53 % (2269964)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 160.88/23.53 % (2269964)CaDiCaL version: 2.1.3 % 160.88/23.53 % (2269964)Termination reason: Instruction limit % 160.88/23.53 % (2269964)Termination phase: Saturation % 160.88/23.53 % (2269964)Time elapsed: 0.593 s % 160.88/23.53 % (2269964)Peak memory usage: 18 MB % 160.88/23.53 % (2269964)Instructions burned: 1473 (million) % 160.88/23.53 % (2269966)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=140508430:i=6324_2970 on theBenchmark for (2970ds/6324Mi) % 160.88/23.53 % (2269966)Instruction limit reached! % 160.88/23.53 % (2269966)------------------------------ % 160.88/23.53 % (2269966)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 160.88/23.53 % (2269966)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 160.88/23.53 % (2269966)CaDiTerminated % 300.43/43.18 Terminated %------------------------------------------------------------------------------