%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : NUM703+4 : TPTP v9.3.1. Released v7.3.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n006.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 12:25:26 PM UTC 2026 % Result : Timeout 301.06s 42.94s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.04 % Problem : NUM703+4 : TPTP v9.3.1. Released v7.3.0. % 0.00/0.08 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.15/0.43 % Computer : n006.cluster.edu % 0.15/0.43 % Model : x86_64 x86_64 % 0.15/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.43 % Memory : 8046.5625MB % 0.15/0.43 % OS : Linux 6.8.0-71-generic % 0.15/0.43 % CPULimit : 300 % 0.15/0.43 % WCLimit : 300 % 0.15/0.43 % DateTime : Sun Sep 27 21:08:55 UTC 2026 % 0.15/0.43 % CPUTime : % 0.15/0.43 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.21/0.47 Running first-order model finding % 0.21/0.48 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.75/4.94 % (3315539)Will run a generic schedule for satisfiability detection. % 30.75/4.94 % (3315544)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=69463558_2999 on theBenchmark for (2999ds/0Mi) % 30.75/4.94 % (3315548)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=303834951:i=116_2999 on theBenchmark for (2999ds/116Mi) % 30.75/4.94 % (3315545)% WARNING: option uhcvi not known. % 30.75/4.94 % (3315547)dis+10_1_sil=32000:sp=arity:random_seed=2963313720:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 30.75/4.94 % (3315546)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3854931116:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 30.75/4.94 % (3315545)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3327715607:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 30.75/4.94 % (3315549)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2048453685:i=131_2999 on theBenchmark for (2999ds/131Mi) % 30.75/4.94 % (3315550)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1029002397:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 30.75/4.94 % (3315548)Instruction limit reached! % 30.75/4.94 % (3315548)------------------------------ % 30.75/4.94 % (3315548)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 30.75/4.94 % (3315548)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.75/4.94 % (3315548)CaDiCaL version: 2.1.3 % 30.75/4.94 % (3315548)Termination reason: Instruction limit % 30.75/4.94 % (3315548)Termination phase: Saturation % 30.75/4.94 % (3315548)Time elapsed: 0.104 s % 30.75/4.94 % (3315548)Peak memory usage: 13 MB % 30.75/4.94 % (3315548)Instructions burned: 118 (million) % 30.75/4.94 % (3315547)Instruction limit reached! % 30.75/4.94 % (3315547)------------------------------ % 30.75/4.94 % (3315547)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 30.75/4.94 % (3315547)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.75/4.94 % (3315547)CaDiCaL version: 2.1.3 % 30.75/4.94 % (3315547)Termination reason: Instruction limit % 30.75/4.94 % (3315547)Termination phase: Saturation % 30.75/4.94 % (3315547)Time elapsed: 0.094 s % 30.75/4.94 % (3315547)Peak memory usage: 13 MB % 30.75/4.94 % (3315547)Instructions burned: 104 (million) % 30.75/4.94 % (3315558)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1512129014:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi) % 30.75/4.94 % (3315549)Instruction limit reached! % 30.75/4.94 % (3315549)------------------------------ % 30.75/4.94 % (3315549)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 30.75/4.94 % (3315549)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.75/4.94 % (3315549)CaDiCaL version: 2.1.3 % 30.75/4.94 % (3315549)Termination reason: Instruction limit % 30.75/4.94 % (3315549)Termination phase: Saturation % 30.75/4.94 % (3315549)Time elapsed: 0.119 s % 30.75/4.94 % (3315549)Peak memory usage: 14 MB % 30.75/4.94 % (3315549)Instructions burned: 131 (million) % 30.75/4.94 % (3315559)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3199681652:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi) % 30.75/4.94 % (3315561)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=2045265396:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 30.75/4.94 % (3315550)Instruction limit reached! % 30.75/4.94 % (3315550)------------------------------ % 30.75/4.94 % (3315550)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 30.75/4.94 % (3315550)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.75/4.94 % (3315550)CaDiCaL version: 2.1.3 % 30.75/4.94 % (3315550)Termination reason: Instruction limit % 30.75/4.94 % (3315550)Termination phase: Saturation % 30.75/4.94 % (3315550)Time elapsed: 0.161 s % 30.75/4.94 % (3315550)Peak memory usage: 15 MB % 30.75/4.94 % (3315550)Instructions burned: 159 (million) % 30.75/4.94 % (3315564)ott-21_1_sil=16000:fs=off:random_seed=81862235:i=180:av=off:fsr=off_2997 on theBenchmark for (2997ds/180Mi) % 30.75/4.94 % (3315559)Instruction limit reached! % 30.75/4.94 % (3315559)------------------------------ % 30.75/4.94 % (3315559)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 30.75/4.94 % (3315559)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.75/4.94 % (3315559)CaDiCaL version: 2.1.3 % 86.12/12.77 % (3315559)Termination reason: Instruction limit % 86.12/12.77 % (3315559)Termination phase: Saturation % 86.12/12.77 % (3315559)Time elapsed: 0.114 s % 86.12/12.77 % (3315559)Peak memory usage: 14 MB % 86.12/12.77 % (3315559)Instructions burned: 131 (million) % 86.12/12.77 % (3315566)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=4290645915:i=477:bd=all_2996 on theBenchmark for (2996ds/477Mi) % 86.12/12.77 % TRYING [1] % 86.12/12.77 % TRYING [2] % 86.12/12.77 % (3315564)Instruction limit reached! % 86.12/12.77 % (3315564)------------------------------ % 86.12/12.77 % (3315564)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 86.12/12.77 % (3315564)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 86.12/12.77 % (3315564)CaDiCaL version: 2.1.3 % 86.12/12.77 % (3315564)Termination reason: Instruction limit % 86.12/12.77 % (3315564)Termination phase: Saturation % 86.12/12.77 % (3315564)Time elapsed: 0.125 s % 86.12/12.77 % (3315564)Peak memory usage: 13 MB % 86.12/12.77 % (3315564)Instructions burned: 181 (million) % 86.12/12.77 % (3315568)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=753064177:fmbsr=1.3:i=865:ins=25_2996 on theBenchmark for (2996ds/865Mi) % 86.12/12.77 % TRYING [3] % 86.12/12.77 % TRYING [1] % 86.12/12.77 % TRYING [2] % 86.12/12.77 % (3315558)Instruction limit reached! % 86.12/12.77 % (3315558)------------------------------ % 86.12/12.77 % (3315558)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 86.12/12.77 % (3315558)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 86.12/12.77 % (3315558)CaDiCaL version: 2.1.3 % 86.12/12.77 % (3315558)Termination reason: Instruction limit % 86.12/12.77 % (3315558)Termination phase: Finite model building constraint generation % 86.12/12.77 % (3315558)Time elapsed: 0.593 s % 86.12/12.77 % (3315558)Peak memory usage: 27 MB % 86.12/12.77 % (3315558)Instructions burned: 714 (million) % 86.12/12.77 % (3315566)Instruction limit reached! % 86.12/12.77 % (3315566)------------------------------ % 86.12/12.77 % (3315566)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 86.12/12.77 % (3315566)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 86.12/12.77 % (3315566)CaDiCaL version: 2.1.3 % 86.12/12.77 % (3315566)Termination reason: Instruction limit % 86.12/12.77 % (3315566)Termination phase: Saturation % 86.12/12.77 % (3315566)Time elapsed: 0.451 s % 86.12/12.77 % (3315566)Peak memory usage: 16 MB % 86.12/12.77 % (3315566)Instructions burned: 477 (million) % 86.12/12.77 % (3315561)Instruction limit reached! % 86.12/12.77 % (3315561)------------------------------ % 86.12/12.77 % (3315561)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 86.12/12.77 % (3315561)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 86.12/12.77 % (3315561)CaDiCaL version: 2.1.3 % 86.12/12.77 % (3315561)Termination reason: Instruction limit % 86.12/12.77 % (3315561)Termination phase: Saturation % 86.12/12.77 % (3315561)Time elapsed: 0.586 s % 86.12/12.77 % (3315561)Peak memory usage: 17 MB % 86.12/12.77 % (3315561)Instructions burned: 684 (million) % 86.12/12.77 % (3315570)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1018807452:i=1179_2992 on theBenchmark for (2992ds/1179Mi) % 86.12/12.77 % (3315571)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=278423458:i=889:ins=1_2992 on theBenchmark for (2992ds/889Mi) % 86.12/12.77 % (3315572)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=1111724557:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2992 on theBenchmark for (2992ds/692Mi) % 86.12/12.77 % TRYING [1] % 86.12/12.77 % TRYING [4] % 86.12/12.77 % TRYING [2] % 86.12/12.77 % (3315568)Instruction limit reached! % 86.12/12.77 % (3315568)------------------------------ % 86.12/12.77 % (3315568)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 86.12/12.77 % (3315568)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 86.12/12.77 % (3315568)CaDiCaL version: 2.1.3 % 86.12/12.77 % (3315568)Termination reason: Instruction limit % 86.12/12.77 % (3315568)Termination phase: Finite model building constraint generation % 86.12/12.77 % (3315568)Time elapsed: 0.740 s % 86.12/12.77 % (3315568)Peak memory usage: 34 MB % 86.12/12.77 % (3315568)Instructions burned: 865 (million) % 86.12/12.77 % (3315576)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=360932554:i=879:kws=inv_precedence:fsr=off_2988 on theBenchmark for (2988ds/879Mi) % 86.12/12.77 % (3315572)Instruction limit reached! % 86.12/12.77 % (3315572)------------------------------ % 86.12/12.77 % (3315572)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 169.84/24.44 % (3315572)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.84/24.44 % (3315572)CaDiCaL version: 2.1.3 % 169.84/24.44 % (3315572)Termination reason: Instruction limit % 169.84/24.44 % (3315572)Termination phase: Saturation % 169.84/24.44 % (3315572)Time elapsed: 0.681 s % 169.84/24.44 % (3315572)Peak memory usage: 18 MB % 169.84/24.44 % (3315572)Instructions burned: 692 (million) % 169.84/24.44 % (3315579)fmb+10_1_sil=64000:random_seed=3322424770:i=22061:nm=2:gsp=on_2984 on theBenchmark for (2984ds/22061Mi) % 169.84/24.44 % (3315571)Instruction limit reached! % 169.84/24.44 % (3315571)------------------------------ % 169.84/24.44 % (3315571)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 169.84/24.44 % (3315571)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.84/24.44 % (3315571)CaDiCaL version: 2.1.3 % 169.84/24.44 % (3315571)Termination reason: Instruction limit % 169.84/24.44 % (3315571)Termination phase: Finite model building constraint generation % 169.84/24.44 % (3315571)Time elapsed: 0.802 s % 169.84/24.44 % (3315571)Peak memory usage: 55 MB % 169.84/24.44 % (3315571)Instructions burned: 890 (million) % 169.84/24.44 % (3315581)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3072354957:i=9515:nm=5_2983 on theBenchmark for (2983ds/9515Mi) % 169.84/24.44 % (3315576)Instruction limit reached! % 169.84/24.44 % (3315576)------------------------------ % 169.84/24.44 % (3315576)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 169.84/24.44 % (3315576)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.84/24.44 % (3315576)CaDiCaL version: 2.1.3 % 169.84/24.44 % (3315576)Termination reason: Instruction limit % 169.84/24.44 % (3315576)Termination phase: Saturation % 169.84/24.44 % (3315576)Time elapsed: 0.658 s % 169.84/24.44 % (3315576)Peak memory usage: 19 MB % 169.84/24.44 % (3315576)Instructions burned: 880 (million) % 169.84/24.44 % (3315583)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3642194273:fmbsr=1.7:i=920_2981 on theBenchmark for (2981ds/920Mi) % 169.84/24.44 % (3315570)Instruction limit reached! % 169.84/24.44 % (3315570)------------------------------ % 169.84/24.44 % (3315570)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 169.84/24.44 % (3315570)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.84/24.44 % (3315570)CaDiCaL version: 2.1.3 % 169.84/24.44 % (3315570)Termination reason: Instruction limit % 169.84/24.44 % (3315570)Termination phase: Saturation % 169.84/24.44 % (3315570)Time elapsed: 1.147 s % 169.84/24.44 % (3315570)Peak memory usage: 24 MB % 169.84/24.44 % (3315570)Instructions burned: 1179 (million) % 169.84/24.44 % (3315585)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2099006127:i=5131_2980 on theBenchmark for (2980ds/5131Mi) % 169.84/24.44 % TRYING [1] % 169.84/24.44 % TRYING [20] % 169.84/24.44 % TRYING [2] % 169.84/24.44 % TRYING [8] % 169.84/24.44 % (3315583)Instruction limit reached! % 169.84/24.44 % (3315583)------------------------------ % 169.84/24.44 % (3315583)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 169.84/24.44 % (3315583)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.84/24.44 % (3315583)CaDiCaL version: 2.1.3 % 169.84/24.44 % (3315583)Termination reason: Instruction limit % 169.84/24.44 % (3315583)Termination phase: Finite model building constraint generation % 169.84/24.44 % (3315583)Time elapsed: 0.724 s % 169.84/24.44 % (3315583)Peak memory usage: 44 MB % 169.84/24.44 % (3315583)Instructions burned: 920 (million) % 169.84/24.44 % (3315587)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1266169150:i=1472:ins=7:fdi=8:gsp=on_2974 on theBenchmark for (2974ds/1472Mi) % 169.84/24.44 % TRYING [5] % 169.84/24.44 % TRYING [3] % 169.84/24.44 % (3315587)Instruction limit reached! % 169.84/24.44 % (3315587)------------------------------ % 169.84/24.44 % (3315587)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 169.84/24.44 % (3315587)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.84/24.44 % (3315587)CaDiCaL version: 2.1.3 % 169.84/24.44 % (3315587)Termination reason: Instruction limit % 169.84/24.44 % (3315587)Termination phase: Saturation % 169.84/24.44 % (3315587)Time elapsed: 1.302 s % 169.84/24.44 % (3315587)Peak memory usage: 27 MB % 169.84/24.44 % (3315587)Instructions burned: 1472 (million) % 169.84/24.44 % (3315589)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1265389306:i=6324_2960 on theBenchmark for (2960ds/6324Mi) % 169.84/24.44 % (3315589)Cannot represent all propositional literals internally % 169.84/24.44 % (3315589)Refutation not found, incomplete strategy % 169.84/24.44 % (3315589)-----------------Terminated % 301.06/42.94 % Vampire exiting % 301.06/42.94 Terminated %------------------------------------------------------------------------------