%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : TOP045+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 : n005.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:29 PM UTC 2026 % Result : Timeout 300.36s 43.34s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.04 % Problem : TOP045+3 : TPTP v9.3.1. Released v3.4.0. % 0.00/0.08 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.11/0.21 % Computer : n005.cluster.edu % 0.11/0.21 % Model : x86_64 x86_64 % 0.11/0.21 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.21 % Memory : 8046.5625MB % 0.11/0.21 % OS : Linux 6.8.0-71-generic % 0.11/0.21 % CPULimit : 300 % 0.11/0.21 % WCLimit : 300 % 0.11/0.21 % DateTime : Mon Sep 28 19:05:49 UTC 2026 % 0.11/0.21 % CPUTime : % 0.11/0.21 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.11/0.25 Running first-order model finding % 0.11/0.25 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 % 29.04/5.16 % (1047104)Will run a generic schedule for satisfiability detection. % 29.04/5.16 % (1047262)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1366733904_2990 on theBenchmark for (2990ds/0Mi) % 29.04/5.16 % (1047263)% WARNING: option uhcvi not known. % 29.04/5.16 % (1047263)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1050054426:i=135531:add=off:rawr=on_2990 on theBenchmark for (2990ds/135531Mi) % 29.04/5.16 % (1047264)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3041486086:i=88024:add=on:rawr=on_2990 on theBenchmark for (2990ds/88024Mi) % 29.04/5.16 % (1047265)dis+10_1_sil=32000:sp=arity:random_seed=446950116:i=103:fgj=on_2990 on theBenchmark for (2990ds/103Mi) % 29.04/5.16 % (1047266)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3105282180:i=116_2990 on theBenchmark for (2990ds/116Mi) % 29.04/5.16 % (1047268)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=640510886:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2990 on theBenchmark for (2990ds/159Mi) % 29.04/5.16 % (1047267)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=879593069:i=131_2990 on theBenchmark for (2990ds/131Mi) % 29.04/5.16 % (1047265)Instruction limit reached! % 29.04/5.16 % (1047265)------------------------------ % 29.04/5.16 % (1047265)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 29.04/5.16 % (1047265)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.04/5.16 % (1047265)CaDiCaL version: 2.1.3 % 29.04/5.16 % (1047265)Termination reason: Instruction limit % 29.04/5.16 % (1047265)Termination phase: Preprocessing 1 % 29.04/5.16 % (1047265)Time elapsed: 0.071 s % 29.04/5.16 % (1047265)Peak memory usage: 46 MB % 29.04/5.16 % (1047265)Instructions burned: 103 (million) % 29.04/5.16 % (1047266)Instruction limit reached! % 29.04/5.16 % (1047266)------------------------------ % 29.04/5.16 % (1047266)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 29.04/5.16 % (1047266)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.04/5.16 % (1047266)CaDiCaL version: 2.1.3 % 29.04/5.16 % (1047266)Termination reason: Instruction limit % 29.04/5.16 % (1047266)Termination phase: Preprocessing 1 % 29.04/5.16 % (1047266)Time elapsed: 0.089 s % 29.04/5.16 % (1047266)Peak memory usage: 47 MB % 29.04/5.16 % (1047266)Instructions burned: 116 (million) % 29.04/5.16 % (1047267)Instruction limit reached! % 29.04/5.16 % (1047267)------------------------------ % 29.04/5.16 % (1047267)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 29.04/5.16 % (1047267)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.04/5.16 % (1047267)CaDiCaL version: 2.1.3 % 29.04/5.16 % (1047267)Termination reason: Instruction limit % 29.04/5.16 % (1047267)Termination phase: Preprocessing 1 % 29.04/5.16 % (1047267)Time elapsed: 0.090 s % 29.04/5.16 % (1047267)Peak memory usage: 47 MB % 29.04/5.16 % (1047267)Instructions burned: 132 (million) % 29.04/5.16 % (1047276)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=353495727:i=714:nm=2_2989 on theBenchmark for (2989ds/714Mi) % 29.04/5.16 % (1047268)Instruction limit reached! % 29.04/5.16 % (1047268)------------------------------ % 29.04/5.16 % (1047268)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 29.04/5.16 % (1047268)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.04/5.16 % (1047268)CaDiCaL version: 2.1.3 % 29.04/5.16 % (1047268)Termination reason: Instruction limit % 29.04/5.16 % (1047268)Termination phase: Preprocessing 1 % 29.04/5.16 % (1047268)Time elapsed: 0.108 s % 29.04/5.16 % (1047268)Peak memory usage: 47 MB % 29.04/5.16 % (1047268)Instructions burned: 159 (million) % 29.04/5.16 % (1047277)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1893713538:i=131:bd=preordered:fsd=on_2989 on theBenchmark for (2989ds/131Mi) % 29.04/5.16 % (1047279)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=2299845747:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2989 on theBenchmark for (2989ds/684Mi) % 29.04/5.16 % (1047281)ott-21_1_sil=16000:fs=off:random_seed=448187383:i=180:av=off:fsr=off_2989 on theBenchmark for (2989ds/180Mi) % 29.04/5.16 % (1047277)Instruction limit reached! % 29.04/5.16 % (1047277)------------------------------ % 29.04/5.16 % (1047277)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 29.04/5.16 % (1047277)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.55/9.67 % (1047277)CaDiCaL version: 2.1.3 % 60.55/9.67 % (1047277)Termination reason: Instruction limit % 60.55/9.67 % (1047277)Termination phase: Preprocessing 1 % 60.55/9.67 % (1047277)Time elapsed: 0.089 s % 60.55/9.67 % (1047277)Peak memory usage: 47 MB % 60.55/9.67 % (1047277)Instructions burned: 131 (million) % 60.55/9.67 % (1047284)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1061973963:i=477:bd=all_2988 on theBenchmark for (2988ds/477Mi) % 60.55/9.67 % (1047281)Instruction limit reached! % 60.55/9.67 % (1047281)------------------------------ % 60.55/9.67 % (1047281)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 60.55/9.67 % (1047281)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.55/9.67 % (1047281)CaDiCaL version: 2.1.3 % 60.55/9.67 % (1047281)Termination reason: Instruction limit % 60.55/9.67 % (1047281)Termination phase: Unused predicate definition removal % 60.55/9.67 % (1047281)Time elapsed: 0.127 s % 60.55/9.67 % (1047281)Peak memory usage: 48 MB % 60.55/9.67 % (1047281)Instructions burned: 180 (million) % 60.55/9.67 % (1047286)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2994843049:fmbsr=1.3:i=865:ins=25_2987 on theBenchmark for (2987ds/865Mi) % 60.55/9.67 % (1047284)Instruction limit reached! % 60.55/9.67 % (1047284)------------------------------ % 60.55/9.67 % (1047284)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 60.55/9.67 % (1047284)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.55/9.67 % (1047284)CaDiCaL version: 2.1.3 % 60.55/9.67 % (1047284)Termination reason: Instruction limit % 60.55/9.67 % (1047284)Termination phase: Preprocessing 3 % 60.55/9.67 % (1047284)Time elapsed: 0.338 s % 60.55/9.67 % (1047284)Peak memory usage: 72 MB % 60.55/9.67 % (1047284)Instructions burned: 477 (million) % 60.55/9.67 % (1047276)Instruction limit reached! % 60.55/9.67 % (1047276)------------------------------ % 60.55/9.67 % (1047276)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 60.55/9.67 % (1047276)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.55/9.67 % (1047276)CaDiCaL version: 2.1.3 % 60.55/9.67 % (1047276)Termination reason: Instruction limit % 60.55/9.67 % (1047276)Termination phase: Preprocessing 3 % 60.55/9.67 % (1047276)Time elapsed: 0.492 s % 60.55/9.67 % (1047276)Peak memory usage: 85 MB % 60.55/9.67 % (1047276)Instructions burned: 715 (million) % 60.55/9.67 % (1047279)Instruction limit reached! % 60.55/9.67 % (1047279)------------------------------ % 60.55/9.67 % (1047279)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 60.55/9.67 % (1047279)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.55/9.67 % (1047288)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1558199503:i=1179_2984 on theBenchmark for (2984ds/1179Mi) % 60.55/9.67 % (1047279)CaDiCaL version: 2.1.3 % 60.55/9.67 % (1047279)Termination reason: Instruction limit % 60.55/9.67 % (1047279)Termination phase: NewCNF % 60.55/9.67 % (1047279)Time elapsed: 0.478 s % 60.55/9.67 % (1047279)Peak memory usage: 76 MB % 60.55/9.67 % (1047279)Instructions burned: 685 (million) % 60.55/9.67 % (1047290)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2005571987:i=889:ins=1_2984 on theBenchmark for (2984ds/889Mi) % 60.55/9.67 % (1047291)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=1407892241:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2984 on theBenchmark for (2984ds/692Mi) % 60.55/9.67 % (1047286)Instruction limit reached! % 60.55/9.67 % (1047286)------------------------------ % 60.55/9.67 % (1047286)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 60.55/9.67 % (1047286)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.55/9.67 % (1047286)CaDiCaL version: 2.1.3 % 60.55/9.67 % (1047286)Termination reason: Instruction limit % 60.55/9.67 % (1047286)Termination phase: Preprocessing 3 % 60.55/9.67 % (1047286)Time elapsed: 0.538 s % 60.55/9.67 % (1047286)Peak memory usage: 87 MB % 60.55/9.67 % (1047286)Instructions burned: 866 (million) % 60.55/9.67 % (1047294)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1690317843:i=879:kws=inv_precedence:fsr=off_2982 on theBenchmark for (2982ds/879Mi) % 60.55/9.67 % (1047291)Instruction limit reached! % 60.55/9.67 % (1047291)------------------------------ % 60.55/9.67 % (1047291)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 60.55/9.67 % (1047291)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.77/23.48 % (1047291)CaDiCaL version: 2.1.3 % 158.77/23.48 % (1047291)Termination reason: Instruction limit % 158.77/23.48 % (1047291)Termination phase: NewCNF % 158.77/23.48 % (1047291)Time elapsed: 0.471 s % 158.77/23.48 % (1047291)Peak memory usage: 76 MB % 158.77/23.48 % (1047291)Instructions burned: 694 (million) % 158.77/23.48 % (1047296)fmb+10_1_sil=64000:random_seed=3210914611:i=22061:nm=2:gsp=on_2979 on theBenchmark for (2979ds/22061Mi) % 158.77/23.48 % (1047290)Instruction limit reached! % 158.77/23.48 % (1047290)------------------------------ % 158.77/23.48 % (1047290)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.77/23.48 % (1047290)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.77/23.48 % (1047290)CaDiCaL version: 2.1.3 % 158.77/23.48 % (1047290)Termination reason: Instruction limit % 158.77/23.48 % (1047290)Termination phase: Preprocessing 3 % 158.77/23.48 % (1047290)Time elapsed: 0.583 s % 158.77/23.48 % (1047290)Peak memory usage: 87 MB % 158.77/23.48 % (1047290)Instructions burned: 891 (million) % 158.77/23.48 % (1047298)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=4227135501:i=9515:nm=5_2978 on theBenchmark for (2978ds/9515Mi) % 158.77/23.48 % (1047288)Instruction limit reached! % 158.77/23.48 % (1047288)------------------------------ % 158.77/23.48 % (1047288)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.77/23.48 % (1047288)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.77/23.48 % (1047288)CaDiCaL version: 2.1.3 % 158.77/23.48 % (1047288)Termination reason: Instruction limit % 158.77/23.48 % (1047288)Termination phase: Property scanning % 158.77/23.48 % (1047288)Time elapsed: 0.740 s % 158.77/23.48 % (1047288)Peak memory usage: 96 MB % 158.77/23.48 % (1047288)Instructions burned: 1181 (million) % 158.77/23.48 % (1047300)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1601875650:fmbsr=1.7:i=920_2976 on theBenchmark for (2976ds/920Mi) % 158.77/23.48 % (1047294)Instruction limit reached! % 158.77/23.48 % (1047294)------------------------------ % 158.77/23.48 % (1047294)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.77/23.48 % (1047294)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.77/23.48 % (1047294)CaDiCaL version: 2.1.3 % 158.77/23.48 % (1047294)Termination reason: Instruction limit % 158.77/23.48 % (1047294)Termination phase: NewCNF % 158.77/23.48 % (1047294)Time elapsed: 0.514 s % 158.77/23.48 % (1047294)Peak memory usage: 83 MB % 158.77/23.48 % (1047294)Instructions burned: 881 (million) % 158.77/23.48 % (1047302)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1644167829:i=5131_2976 on theBenchmark for (2976ds/5131Mi) % 158.77/23.48 % (1047300)Instruction limit reached! % 158.77/23.48 % (1047300)------------------------------ % 158.77/23.48 % (1047300)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.77/23.48 % (1047300)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.77/23.48 % (1047300)CaDiCaL version: 2.1.3 % 158.77/23.48 % (1047300)Termination reason: Instruction limit % 158.77/23.48 % (1047300)Termination phase: Preprocessing 3 % 158.77/23.48 % (1047300)Time elapsed: 0.599 s % 158.77/23.48 % (1047300)Peak memory usage: 88 MB % 158.77/23.48 % (1047300)Instructions burned: 921 (million) % 158.77/23.48 % (1047304)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1340356629:i=1472:ins=7:fdi=8:gsp=on_2970 on theBenchmark for (2970ds/1472Mi) % 158.77/23.48 % (1047304)Instruction limit reached! % 158.77/23.48 % (1047304)------------------------------ % 158.77/23.48 % (1047304)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.77/23.48 % (1047304)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.77/23.48 % (1047304)CaDiCaL version: 2.1.3 % 158.77/23.48 % (1047304)Termination reason: Instruction limit % 158.77/23.48 % (1047304)Termination phase: Property scanning % 158.77/23.48 % (1047304)Time elapsed: 0.839 s % 158.77/23.48 % (1047304)Peak memory usage: 96 MB % 158.77/23.48 % (1047304)Instructions burned: 1473 (million) % 158.77/23.48 % (1047306)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=528027234:i=6324_2961 on theBenchmark for (2961ds/6324Mi) % 158.77/23.48 % (1047302)Instruction limit reached! % 158.77/23.48 % (1047302)------------------------------ % 158.77/23.48 % (1047302)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.77/23.48 % (1047302)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.77/23.48 % (1047302)CaDiCaL version: 2.1.3 % 158.77/23.48 % (1047302)Termination reason: Instruction limit % 158.77/23.48 % (1047302)TerminatioTerminated %------------------------------------------------------------------------------