%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW468-1 : TPTP v9.3.1. Released v5.2.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n026.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:03 PM UTC 2026 % Result : Timeout 300.38s 42.64s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWW468-1 : TPTP v9.3.1. Released v5.2.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.09/0.20 % Computer : n026.cluster.edu % 0.09/0.20 % Model : x86_64 x86_64 % 0.09/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.20 % Memory : 8046.5625MB % 0.09/0.20 % OS : Linux 6.8.0-71-generic % 0.09/0.20 % CPULimit : 300 % 0.09/0.20 % WCLimit : 300 % 0.09/0.20 % DateTime : Mon Sep 28 14:03:12 UTC 2026 % 0.09/0.20 % CPUTime : % 0.09/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.09/0.23 Running first-order model finding % 0.09/0.23 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 % 24.53/3.73 % (3863662)Will run a generic schedule for satisfiability detection. % 24.53/3.73 % (3863667)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1636120568_2999 on theBenchmark for (2999ds/0Mi) % 24.53/3.73 % (3863668)% WARNING: option uhcvi not known. % 24.53/3.73 % TRYING [1] % 24.53/3.73 % TRYING [2] % 24.53/3.73 % TRYING [3] % 24.53/3.73 % (3863668)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=495520244:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 24.53/3.73 % (3863672)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=4062340321:i=131_2999 on theBenchmark for (2999ds/131Mi) % 24.53/3.73 % (3863670)dis+10_1_sil=32000:sp=arity:random_seed=1358954819:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 24.53/3.73 % (3863669)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=684701199:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 24.53/3.73 % (3863671)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=120618507:i=116_2999 on theBenchmark for (2999ds/116Mi) % 24.53/3.73 % (3863673)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=697267840:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 24.53/3.73 % TRYING [4] % 24.53/3.73 % (3863671)Instruction limit reached! % 24.53/3.73 % (3863671)------------------------------ % 24.53/3.73 % (3863671)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 24.53/3.73 % (3863671)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.53/3.73 % (3863671)CaDiCaL version: 2.1.3 % 24.53/3.73 % (3863671)Termination reason: Instruction limit % 24.53/3.73 % (3863671)Termination phase: Saturation % 24.53/3.73 % (3863671)Time elapsed: 0.049 s % 24.53/3.73 % (3863671)Peak memory usage: 12 MB % 24.53/3.73 % (3863671)Instructions burned: 117 (million) % 24.53/3.73 % (3863672)Instruction limit reached! % 24.53/3.73 % (3863672)------------------------------ % 24.53/3.73 % (3863672)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 24.53/3.73 % (3863672)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.53/3.73 % (3863672)CaDiCaL version: 2.1.3 % 24.53/3.73 % (3863672)Termination reason: Instruction limit % 24.53/3.73 % (3863672)Termination phase: Saturation % 24.53/3.73 % (3863672)Time elapsed: 0.060 s % 24.53/3.73 % (3863672)Peak memory usage: 12 MB % 24.53/3.73 % (3863672)Instructions burned: 141 (million) % 24.53/3.73 % (3863670)Instruction limit reached! % 24.53/3.73 % (3863670)------------------------------ % 24.53/3.73 % (3863670)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 24.53/3.73 % (3863670)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.53/3.73 % (3863670)CaDiCaL version: 2.1.3 % 24.53/3.73 % (3863670)Termination reason: Instruction limit % 24.53/3.73 % (3863670)Termination phase: Saturation % 24.53/3.73 % (3863670)Time elapsed: 0.060 s % 24.53/3.73 % (3863670)Peak memory usage: 12 MB % 24.53/3.73 % (3863670)Instructions burned: 103 (million) % 24.53/3.73 % TRYING [5] % 24.53/3.73 % (3863681)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=4056465594:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 24.53/3.73 % TRYING [1] % 24.53/3.73 % TRYING [2] % 24.53/3.73 % TRYING [3] % 24.53/3.73 % (3863683)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=1983692268:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 24.53/3.73 % (3863682)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2414703701:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 24.53/3.73 % (3863673)Instruction limit reached! % 24.53/3.73 % (3863673)------------------------------ % 24.53/3.73 % (3863673)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 24.53/3.73 % (3863673)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.53/3.73 % (3863673)CaDiCaL version: 2.1.3 % 24.53/3.73 % (3863673)Termination reason: Instruction limit % 24.53/3.73 % (3863673)Termination phase: Saturation % 24.53/3.73 % (3863673)Time elapsed: 0.086 s % 24.53/3.73 % (3863673)Peak memory usage: 12 MB % 24.53/3.73 % (3863673)Instructions burned: 161 (million) % 24.53/3.73 % (3863687)ott-21_1_sil=16000:fs=off:random_seed=2041324399:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 24.53/3.73 % TRYING [4] % 24.53/3.73 % (3863682)Instruction limit reached! % 24.53/3.73 % (3863682)------------------------------ % 24.53/3.73 % (3863682)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 45.72/6.72 % (3863682)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.72/6.72 % (3863682)CaDiCaL version: 2.1.3 % 45.72/6.72 % (3863682)Termination reason: Instruction limit % 45.72/6.72 % (3863682)Termination phase: Saturation % 45.72/6.72 % (3863682)Time elapsed: 0.057 s % 45.72/6.72 % (3863682)Peak memory usage: 12 MB % 45.72/6.72 % (3863682)Instructions burned: 131 (million) % 45.72/6.72 % (3863689)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=581532031:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 45.72/6.72 % (3863687)Instruction limit reached! % 45.72/6.72 % (3863687)------------------------------ % 45.72/6.72 % (3863687)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 45.72/6.72 % (3863687)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.72/6.72 % (3863687)CaDiCaL version: 2.1.3 % 45.72/6.72 % (3863687)Termination reason: Instruction limit % 45.72/6.72 % (3863687)Termination phase: Saturation % 45.72/6.72 % (3863687)Time elapsed: 0.073 s % 45.72/6.72 % (3863687)Peak memory usage: 11 MB % 45.72/6.72 % (3863687)Instructions burned: 190 (million) % 45.72/6.72 % (3863691)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2773347250:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi) % 45.72/6.72 % TRYING [1] % 45.72/6.72 % TRYING [2] % 45.72/6.72 % TRYING [3] % 45.72/6.72 % TRYING [4] % 45.72/6.72 % TRYING [6] % 45.72/6.72 % (3863683)Instruction limit reached! % 45.72/6.72 % (3863683)------------------------------ % 45.72/6.72 % (3863683)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 45.72/6.72 % (3863683)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.72/6.72 % (3863683)CaDiCaL version: 2.1.3 % 45.72/6.72 % (3863683)Termination reason: Instruction limit % 45.72/6.72 % (3863683)Termination phase: Saturation % 45.72/6.72 % (3863683)Time elapsed: 0.286 s % 45.72/6.72 % (3863683)Peak memory usage: 16 MB % 45.72/6.72 % (3863683)Instructions burned: 686 (million) % 45.72/6.72 % (3863693)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3006867499:i=1179_2995 on theBenchmark for (2995ds/1179Mi) % 45.72/6.72 % (3863689)Instruction limit reached! % 45.72/6.72 % (3863689)------------------------------ % 45.72/6.72 % (3863689)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 45.72/6.72 % (3863689)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.72/6.72 % (3863689)CaDiCaL version: 2.1.3 % 45.72/6.72 % (3863689)Termination reason: Instruction limit % 45.72/6.72 % (3863689)Termination phase: Saturation % 45.72/6.72 % (3863689)Time elapsed: 0.241 s % 45.72/6.72 % (3863689)Peak memory usage: 13 MB % 45.72/6.72 % (3863689)Instructions burned: 477 (million) % 45.72/6.72 % (3863695)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3594180981:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi) % 45.72/6.72 % (3863681)Instruction limit reached! % 45.72/6.72 % (3863681)------------------------------ % 45.72/6.72 % (3863681)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 45.72/6.72 % (3863681)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.72/6.72 % (3863681)CaDiCaL version: 2.1.3 % 45.72/6.72 % (3863681)Termination reason: Instruction limit % 45.72/6.72 % (3863681)Termination phase: Finite model building SAT solving % 45.72/6.72 % (3863681)Time elapsed: 0.433 s % 45.72/6.72 % (3863681)Peak memory usage: 20 MB % 45.72/6.72 % (3863681)Instructions burned: 714 (million) % 45.72/6.72 % (3863697)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=249057572: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) % 45.72/6.72 % TRYING [14] % 45.72/6.72 % (3863691)Instruction limit reached! % 45.72/6.72 % (3863691)------------------------------ % 45.72/6.72 % (3863691)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 45.72/6.72 % (3863691)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.72/6.72 % (3863691)CaDiCaL version: 2.1.3 % 45.72/6.72 % (3863691)Termination reason: Instruction limit % 45.72/6.72 % (3863691)Termination phase: Finite model building SAT solving % 45.72/6.72 % (3863691)Time elapsed: 0.443 s % 45.72/6.72 % (3863691)Peak memory usage: 15 MB % 45.72/6.72 % (3863691)Instructions burned: 866 (million) % 45.72/6.72 % (3863699)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=305165604:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi) % 45.72/6.72 % (3863695)Instruction limit reached! % 45.72/6.72 % (3863695)------------------------------ % 109.60/15.77 % (3863695)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 109.60/15.77 % (3863695)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 109.60/15.77 % (3863695)CaDiCaL version: 2.1.3 % 109.60/15.77 % (3863695)Termination reason: Instruction limit % 109.60/15.77 % (3863695)Termination phase: Finite model building constraint generation % 109.60/15.77 % (3863695)Time elapsed: 0.366 s % 109.60/15.77 % (3863695)Peak memory usage: 92 MB % 109.60/15.77 % (3863695)Instructions burned: 890 (million) % 109.60/15.77 % (3863701)fmb+10_1_sil=64000:random_seed=1292704446:i=22061:nm=2:gsp=on_2991 on theBenchmark for (2991ds/22061Mi) % 109.60/15.77 % TRYING [1] % 109.60/15.77 % TRYING [2] % 109.60/15.77 % TRYING [3] % 109.60/15.77 % (3863697)Instruction limit reached! % 109.60/15.77 % (3863697)------------------------------ % 109.60/15.77 % (3863697)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 109.60/15.77 % (3863697)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 109.60/15.77 % (3863697)CaDiCaL version: 2.1.3 % 109.60/15.77 % (3863697)Termination reason: Instruction limit % 109.60/15.77 % (3863697)Termination phase: Saturation % 109.60/15.77 % (3863697)Time elapsed: 0.339 s % 109.60/15.77 % (3863697)Peak memory usage: 15 MB % 109.60/15.77 % (3863697)Instructions burned: 692 (million) % 109.60/15.77 % TRYING [4] % 109.60/15.77 % (3863703)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2395250101:i=9515:nm=5_2991 on theBenchmark for (2991ds/9515Mi) % 109.60/15.77 % (3863693)Instruction limit reached! % 109.60/15.77 % (3863693)------------------------------ % 109.60/15.77 % (3863693)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 109.60/15.77 % (3863693)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 109.60/15.77 % (3863693)CaDiCaL version: 2.1.3 % 109.60/15.77 % (3863693)Termination reason: Instruction limit % 109.60/15.77 % (3863693)Termination phase: Saturation % 109.60/15.77 % (3863693)Time elapsed: 0.499 s % 109.60/15.77 % (3863693)Peak memory usage: 22 MB % 109.60/15.77 % (3863693)Instructions burned: 1179 (million) % 109.60/15.77 % TRYING [20] % 109.60/15.77 % (3863705)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3716872230:fmbsr=1.7:i=920_2990 on theBenchmark for (2990ds/920Mi) % 109.60/15.77 % TRYING [8] % 109.60/15.77 % TRYING [5] % 109.60/15.77 % (3863699)Instruction limit reached! % 109.60/15.77 % (3863699)------------------------------ % 109.60/15.77 % (3863699)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 109.60/15.77 % (3863699)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 109.60/15.77 % (3863699)CaDiCaL version: 2.1.3 % 109.60/15.77 % (3863699)Termination reason: Instruction limit % 109.60/15.77 % (3863699)Termination phase: Saturation % 109.60/15.77 % (3863699)Time elapsed: 0.438 s % 109.60/15.77 % (3863699)Peak memory usage: 17 MB % 109.60/15.77 % (3863699)Instructions burned: 879 (million) % 109.60/15.77 % (3863707)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=504173043:i=5131_2988 on theBenchmark for (2988ds/5131Mi) % 109.60/15.77 % (3863705)Instruction limit reached! % 109.60/15.77 % (3863705)------------------------------ % 109.60/15.77 % (3863705)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 109.60/15.77 % (3863705)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 109.60/15.77 % (3863705)CaDiCaL version: 2.1.3 % 109.60/15.77 % (3863705)Termination reason: Instruction limit % 109.60/15.77 % (3863705)Termination phase: Finite model building constraint generation % 109.60/15.77 % (3863705)Time elapsed: 0.351 s % 109.60/15.77 % (3863705)Peak memory usage: 74 MB % 109.60/15.77 % (3863705)Instructions burned: 921 (million) % 109.60/15.77 % (3863709)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=4275118320:i=1472:ins=7:fdi=8:gsp=on_2986 on theBenchmark for (2986ds/1472Mi) % 109.60/15.77 % (3863709)Instruction limit reached! % 109.60/15.77 % (3863709)------------------------------ % 109.60/15.77 % (3863709)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 109.60/15.77 % (3863709)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 109.60/15.77 % (3863709)CaDiCaL version: 2.1.3 % 109.60/15.77 % (3863709)Termination reason: Instruction limit % 109.60/15.77 % (3863709)Termination phase: Saturation % 109.60/15.77 % (3863709)Time elapsed: 0.698 s % 109.60/15.77 % (3863709)Peak memory usage: 24 MB % 109.60/15.77 % (3863709)Instructions burned: 1473 (million) % 109.60/15.77 % (3863711)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1765421332:i=6324_2979 on theBenchmark for (2979ds/6324Mi) % 109.60/15.77 % TRYING [6] % 109.60/15.77 % TRYING [77] % 109.60/15.77 % (3863707)Instruction limit reacheTerminated % 300.38/42.64 % Vampire exiting %------------------------------------------------------------------------------