%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : TOP040+3 : TPTP v9.3.1. Released v3.4.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/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 02:34:27 PM UTC 2026 % Result : Timeout 300.60s 43.18s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : TOP040+3 : TPTP v9.3.1. Released v3.4.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.07/0.18 % Computer : n001.cluster.edu % 0.07/0.18 % Model : x86_64 x86_64 % 0.07/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.07/0.18 % Memory : 8046.5625MB % 0.07/0.18 % OS : Linux 6.8.0-71-generic % 0.07/0.19 % CPULimit : 300 % 0.07/0.19 % WCLimit : 300 % 0.07/0.19 % DateTime : Mon Sep 28 19:07:35 UTC 2026 % 0.07/0.19 % CPUTime : % 0.07/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.07/0.22 Running first-order model finding % 0.07/0.22 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 % 30.31/5.04 % (632663)Will run a generic schedule for satisfiability detection. % 30.31/5.04 % (632668)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3195834844_2993 on theBenchmark for (2993ds/0Mi) % 30.31/5.04 % (632669)% WARNING: option uhcvi not known. % 30.31/5.04 % (632669)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=935700272:i=135531:add=off:rawr=on_2993 on theBenchmark for (2993ds/135531Mi) % 30.31/5.04 % (632670)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1884048307:i=88024:add=on:rawr=on_2993 on theBenchmark for (2993ds/88024Mi) % 30.31/5.04 % (632671)dis+10_1_sil=32000:sp=arity:random_seed=3609022553:i=103:fgj=on_2993 on theBenchmark for (2993ds/103Mi) % 30.31/5.04 % (632672)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1133757692:i=116_2993 on theBenchmark for (2993ds/116Mi) % 30.31/5.04 % (632673)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1986526458:i=131_2993 on theBenchmark for (2993ds/131Mi) % 30.31/5.04 % (632674)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1291933515:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2993 on theBenchmark for (2993ds/159Mi) % 30.31/5.04 % (632671)Instruction limit reached! % 30.31/5.04 % (632671)------------------------------ % 30.31/5.04 % (632671)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 30.31/5.04 % (632671)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.31/5.04 % (632671)CaDiCaL version: 2.1.3 % 30.31/5.04 % (632671)Termination reason: Instruction limit % 30.31/5.04 % (632671)Termination phase: Preprocessing 1 % 30.31/5.04 % (632671)Time elapsed: 0.071 s % 30.31/5.04 % (632671)Peak memory usage: 35 MB % 30.31/5.04 % (632671)Instructions burned: 104 (million) % 30.31/5.04 % (632682)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1754242651:i=714:nm=2_2992 on theBenchmark for (2992ds/714Mi) % 30.31/5.04 % (632672)Instruction limit reached! % 30.31/5.04 % (632672)------------------------------ % 30.31/5.04 % (632672)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 30.31/5.04 % (632672)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.31/5.04 % (632672)CaDiCaL version: 2.1.3 % 30.31/5.04 % (632672)Termination reason: Instruction limit % 30.31/5.04 % (632672)Termination phase: Preprocessing 2 % 30.31/5.04 % (632672)Time elapsed: 0.100 s % 30.31/5.04 % (632672)Peak memory usage: 37 MB % 30.31/5.04 % (632672)Instructions burned: 117 (million) % 30.31/5.04 % (632673)Instruction limit reached! % 30.31/5.04 % (632673)------------------------------ % 30.31/5.04 % (632673)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 30.31/5.04 % (632673)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.31/5.04 % (632673)CaDiCaL version: 2.1.3 % 30.31/5.04 % (632673)Termination reason: Instruction limit % 30.31/5.04 % (632673)Termination phase: Preprocessing 2 % 30.31/5.04 % (632673)Time elapsed: 0.102 s % 30.31/5.04 % (632673)Peak memory usage: 37 MB % 30.31/5.04 % (632673)Instructions burned: 131 (million) % 30.31/5.04 % (632684)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=631081324:i=131:bd=preordered:fsd=on_2992 on theBenchmark for (2992ds/131Mi) % 30.31/5.04 % (632685)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=1300986301:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2992 on theBenchmark for (2992ds/684Mi) % 30.31/5.04 % (632674)Instruction limit reached! % 30.31/5.04 % (632674)------------------------------ % 30.31/5.04 % (632674)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 30.31/5.04 % (632674)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.31/5.04 % (632674)CaDiCaL version: 2.1.3 % 30.31/5.04 % (632674)Termination reason: Instruction limit % 30.31/5.04 % (632674)Termination phase: Preprocessing 2 % 30.31/5.04 % (632674)Time elapsed: 0.126 s % 30.31/5.04 % (632674)Peak memory usage: 41 MB % 30.31/5.04 % (632674)Instructions burned: 159 (million) % 30.31/5.04 % (632688)ott-21_1_sil=16000:fs=off:random_seed=2741157063:i=180:av=off:fsr=off_2992 on theBenchmark for (2992ds/180Mi) % 30.31/5.04 % (632684)Instruction limit reached! % 30.31/5.04 % (632684)------------------------------ % 30.31/5.04 % (632684)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 30.31/5.04 % (632684)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.31/5.04 % (632684)CaDiCaL version: 2.1.3 % 30.31/5.04 % (632684)Termination reason: Instruction limit % 69.83/10.69 % (632684)Termination phase: Preprocessing 2 % 69.83/10.69 % (632684)Time elapsed: 0.101 s % 69.83/10.69 % (632684)Peak memory usage: 37 MB % 69.83/10.69 % (632684)Instructions burned: 132 (million) % 69.83/10.69 % (632690)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3439263853:i=477:bd=all_2991 on theBenchmark for (2991ds/477Mi) % 69.83/10.69 % (632688)Instruction limit reached! % 69.83/10.69 % (632688)------------------------------ % 69.83/10.69 % (632688)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 69.83/10.69 % (632688)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 69.83/10.69 % (632688)CaDiCaL version: 2.1.3 % 69.83/10.69 % (632688)Termination reason: Instruction limit % 69.83/10.69 % (632688)Termination phase: Preprocessing 2 % 69.83/10.69 % (632688)Time elapsed: 0.146 s % 69.83/10.69 % (632688)Peak memory usage: 45 MB % 69.83/10.69 % (632688)Instructions burned: 181 (million) % 69.83/10.69 % (632692)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2219081056:fmbsr=1.3:i=865:ins=25_2990 on theBenchmark for (2990ds/865Mi) % 69.83/10.69 % (632685)Instruction limit reached! % 69.83/10.69 % (632685)------------------------------ % 69.83/10.69 % (632685)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 69.83/10.69 % (632685)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 69.83/10.69 % (632685)CaDiCaL version: 2.1.3 % 69.83/10.69 % (632685)Termination reason: Instruction limit % 69.83/10.69 % (632685)Termination phase: NewCNF % 69.83/10.69 % (632685)Time elapsed: 0.419 s % 69.83/10.69 % (632685)Peak memory usage: 61 MB % 69.83/10.69 % (632685)Instructions burned: 685 (million) % 69.83/10.69 % (632682)Instruction limit reached! % 69.83/10.69 % (632682)------------------------------ % 69.83/10.69 % (632682)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 69.83/10.69 % (632682)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 69.83/10.69 % (632682)CaDiCaL version: 2.1.3 % 69.83/10.69 % (632682)Termination reason: Instruction limit % 69.83/10.69 % (632682)Termination phase: Preprocessing 3 % 69.83/10.69 % (632682)Time elapsed: 0.463 s % 69.83/10.69 % (632682)Peak memory usage: 69 MB % 69.83/10.69 % (632682)Instructions burned: 714 (million) % 69.83/10.69 % (632690)Instruction limit reached! % 69.83/10.69 % (632690)------------------------------ % 69.83/10.69 % (632690)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 69.83/10.69 % (632690)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 69.83/10.69 % (632690)CaDiCaL version: 2.1.3 % 69.83/10.69 % (632690)Termination reason: Instruction limit % 69.83/10.69 % (632690)Termination phase: Preprocessing 3 % 69.83/10.69 % (632690)Time elapsed: 0.318 s % 69.83/10.69 % (632690)Peak memory usage: 57 MB % 69.83/10.69 % (632690)Instructions burned: 478 (million) % 69.83/10.69 % (632694)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3302355523:i=1179_2988 on theBenchmark for (2988ds/1179Mi) % 69.83/10.69 % (632695)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=4071826568:i=889:ins=1_2987 on theBenchmark for (2987ds/889Mi) % 69.83/10.69 % (632697)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=3925504842:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2987 on theBenchmark for (2987ds/692Mi) % 69.83/10.69 % (632692)Instruction limit reached! % 69.83/10.69 % (632692)------------------------------ % 69.83/10.69 % (632692)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 69.83/10.69 % (632692)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 69.83/10.69 % (632692)CaDiCaL version: 2.1.3 % 69.83/10.69 % (632692)Termination reason: Instruction limit % 69.83/10.69 % (632692)Termination phase: Property scanning % 69.83/10.69 % (632692)Time elapsed: 0.497 s % 69.83/10.69 % (632692)Peak memory usage: 65 MB % 69.83/10.69 % (632692)Instructions burned: 865 (million) % 69.83/10.69 % (632700)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3184111179:i=879:kws=inv_precedence:fsr=off_2985 on theBenchmark for (2985ds/879Mi) % 69.83/10.69 % (632697)Instruction limit reached! % 69.83/10.69 % (632697)------------------------------ % 69.83/10.69 % (632697)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 69.83/10.69 % (632697)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 69.83/10.69 % (632697)CaDiCaL version: 2.1.3 % 69.83/10.69 % (632697)Termination reason: Instruction limit % 69.83/10.69 % (632697)Termination phase: NewCNF % 197.49/28.69 % (632697)Time elapsed: 0.432 s % 197.49/28.69 % (632697)Peak memory usage: 61 MB % 197.49/28.69 % (632697)Instructions burned: 692 (million) % 197.49/28.69 % (632702)fmb+10_1_sil=64000:random_seed=2291941506:i=22061:nm=2:gsp=on_2983 on theBenchmark for (2983ds/22061Mi) % 197.49/28.69 % (632695)Instruction limit reached! % 197.49/28.69 % (632695)------------------------------ % 197.49/28.69 % (632695)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 197.49/28.69 % (632695)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 197.49/28.69 % (632695)CaDiCaL version: 2.1.3 % 197.49/28.69 % (632695)Termination reason: Instruction limit % 197.49/28.69 % (632695)Termination phase: Property scanning % 197.49/28.69 % (632695)Time elapsed: 0.522 s % 197.49/28.69 % (632695)Peak memory usage: 65 MB % 197.49/28.69 % (632695)Instructions burned: 890 (million) % 197.49/28.69 % (632704)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=400824741:i=9515:nm=5_2982 on theBenchmark for (2982ds/9515Mi) % 197.49/28.69 % (632694)Instruction limit reached! % 197.49/28.69 % (632694)------------------------------ % 197.49/28.69 % (632694)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 197.49/28.69 % (632694)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 197.49/28.69 % (632694)CaDiCaL version: 2.1.3 % 197.49/28.69 % (632694)Termination reason: Instruction limit % 197.49/28.69 % (632694)Termination phase: Property scanning % 197.49/28.69 % (632694)Time elapsed: 0.650 s % 197.49/28.69 % (632694)Peak memory usage: 71 MB % 197.49/28.69 % (632694)Instructions burned: 1180 (million) % 197.49/28.69 % (632706)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2449527632:fmbsr=1.7:i=920_2981 on theBenchmark for (2981ds/920Mi) % 197.49/28.69 % (632700)Instruction limit reached! % 197.49/28.69 % (632700)------------------------------ % 197.49/28.69 % (632700)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 197.49/28.69 % (632700)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 197.49/28.69 % (632700)CaDiCaL version: 2.1.3 % 197.49/28.69 % (632700)Termination reason: Instruction limit % 197.49/28.69 % (632700)Termination phase: NewCNF % 197.49/28.69 % (632700)Time elapsed: 0.475 s % 197.49/28.69 % (632700)Peak memory usage: 67 MB % 197.49/28.69 % (632700)Instructions burned: 880 (million) % 197.49/28.69 % (632708)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=4153041499:i=5131_2980 on theBenchmark for (2980ds/5131Mi) % 197.49/28.69 % (632706)Instruction limit reached! % 197.49/28.69 % (632706)------------------------------ % 197.49/28.69 % (632706)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 197.49/28.69 % (632706)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 197.49/28.69 % (632706)CaDiCaL version: 2.1.3 % 197.49/28.69 % (632706)Termination reason: Instruction limit % 197.49/28.69 % (632706)Termination phase: Property scanning % 197.49/28.69 % (632706)Time elapsed: 0.521 s % 197.49/28.69 % (632706)Peak memory usage: 65 MB % 197.49/28.69 % (632706)Instructions burned: 922 (million) % 197.49/28.69 % (632710)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3092424664:i=1472:ins=7:fdi=8:gsp=on_2975 on theBenchmark for (2975ds/1472Mi) % 197.49/28.69 % (632710)Instruction limit reached! % 197.49/28.69 % (632710)------------------------------ % 197.49/28.69 % (632710)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 197.49/28.69 % (632710)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 197.49/28.69 % (632710)CaDiCaL version: 2.1.3 % 197.49/28.69 % (632710)Termination reason: Instruction limit % 197.49/28.69 % (632710)Termination phase: Property scanning % 197.49/28.69 % (632710)Time elapsed: 0.765 s % 197.49/28.69 % (632710)Peak memory usage: 67 MB % 197.49/28.69 % (632710)Instructions burned: 1473 (million) % 197.49/28.69 % (632712)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=926447404:i=6324_2967 on theBenchmark for (2967ds/6324Mi) % 197.49/28.69 % (632708)Instruction limit reached! % 197.49/28.69 % (632708)------------------------------ % 197.49/28.69 % (632708)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 197.49/28.69 % (632708)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 197.49/28.69 % (632708)CaDiCaL version: 2.1.3 % 197.49/28.69 % (632708)Termination reason: Instruction limit % 197.49/28.69 % (632708)Termination phase: Saturation % 197.49/28.69 % (632708)Time elapsed: 2.773 s % 197.49/28.69 % (632708)Peak memory usage: 117 MB % 197.49/28.69 % (632708)Instructions burned: 5131 (million) % 197.49/28.69 % (632714)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:randoTerminated %------------------------------------------------------------------------------