%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : TOP048+3 : TPTP v9.3.1. Released v3.4.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n013.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:30 PM UTC 2026 % Result : Timeout 300.32s 43.25s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : TOP048+3 : TPTP v9.3.1. Released v3.4.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.08/0.17 % Computer : n013.cluster.edu % 0.08/0.17 % Model : x86_64 x86_64 % 0.08/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.17 % Memory : 8046.5625MB % 0.08/0.17 % OS : Linux 6.8.0-71-generic % 0.08/0.17 % CPULimit : 300 % 0.08/0.17 % WCLimit : 300 % 0.08/0.17 % DateTime : Mon Sep 28 19:06:38 UTC 2026 % 0.08/0.17 % CPUTime : % 0.08/0.17 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.08/0.20 Running first-order model finding % 0.08/0.20 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.06/6.29 % (1462542)Will run a generic schedule for satisfiability detection. % 37.06/6.29 % (1462551)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=502886448:i=116_2990 on theBenchmark for (2990ds/116Mi) % 37.06/6.29 % (1462548)% WARNING: option uhcvi not known. % 37.06/6.29 % (1462547)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2923880677_2990 on theBenchmark for (2990ds/0Mi) % 37.06/6.29 % (1462548)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=432766550:i=135531:add=off:rawr=on_2990 on theBenchmark for (2990ds/135531Mi) % 37.06/6.29 % (1462549)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3379166868:i=88024:add=on:rawr=on_2990 on theBenchmark for (2990ds/88024Mi) % 37.06/6.29 % (1462550)dis+10_1_sil=32000:sp=arity:random_seed=123327573:i=103:fgj=on_2990 on theBenchmark for (2990ds/103Mi) % 37.06/6.29 % (1462552)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2673289934:i=131_2990 on theBenchmark for (2990ds/131Mi) % 37.06/6.29 % (1462553)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=847848151:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2990 on theBenchmark for (2990ds/159Mi) % 37.06/6.29 % (1462551)Instruction limit reached! % 37.06/6.29 % (1462551)------------------------------ % 37.06/6.29 % (1462551)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 37.06/6.29 % (1462551)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.06/6.29 % (1462551)CaDiCaL version: 2.1.3 % 37.06/6.29 % (1462551)Termination reason: Instruction limit % 37.06/6.29 % (1462551)Termination phase: Preprocessing 1 % 37.06/6.29 % (1462551)Time elapsed: 0.051 s % 37.06/6.29 % (1462551)Peak memory usage: 47 MB % 37.06/6.29 % (1462551)Instructions burned: 119 (million) % 37.06/6.29 % (1462561)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=4052610684:i=714:nm=2_2990 on theBenchmark for (2990ds/714Mi) % 37.06/6.29 % (1462550)Instruction limit reached! % 37.06/6.29 % (1462550)------------------------------ % 37.06/6.29 % (1462550)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 37.06/6.29 % (1462550)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.06/6.29 % (1462550)CaDiCaL version: 2.1.3 % 37.06/6.29 % (1462550)Termination reason: Instruction limit % 37.06/6.29 % (1462550)Termination phase: Preprocessing 1 % 37.06/6.29 % (1462550)Time elapsed: 0.068 s % 37.06/6.29 % (1462550)Peak memory usage: 46 MB % 37.06/6.29 % (1462550)Instructions burned: 103 (million) % 37.06/6.29 % (1462552)Instruction limit reached! % 37.06/6.29 % (1462552)------------------------------ % 37.06/6.29 % (1462552)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 37.06/6.29 % (1462552)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.06/6.29 % (1462552)CaDiCaL version: 2.1.3 % 37.06/6.29 % (1462552)Termination reason: Instruction limit % 37.06/6.29 % (1462552)Termination phase: Preprocessing 1 % 37.06/6.29 % (1462552)Time elapsed: 0.088 s % 37.06/6.29 % (1462552)Peak memory usage: 47 MB % 37.06/6.29 % (1462552)Instructions burned: 132 (million) % 37.06/6.29 % (1462563)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3858452848:i=131:bd=preordered:fsd=on_2989 on theBenchmark for (2989ds/131Mi) % 37.06/6.29 % (1462553)Instruction limit reached! % 37.06/6.29 % (1462553)------------------------------ % 37.06/6.29 % (1462553)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 37.06/6.29 % (1462553)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.06/6.29 % (1462553)CaDiCaL version: 2.1.3 % 37.06/6.29 % (1462553)Termination reason: Instruction limit % 37.06/6.29 % (1462553)Termination phase: Preprocessing 1 % 37.06/6.29 % (1462553)Time elapsed: 0.105 s % 37.06/6.29 % (1462553)Peak memory usage: 47 MB % 37.06/6.29 % (1462553)Instructions burned: 160 (million) % 37.06/6.29 % (1462565)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=2336795086:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2989 on theBenchmark for (2989ds/684Mi) % 37.06/6.29 % (1462566)ott-21_1_sil=16000:fs=off:random_seed=2075595440:i=180:av=off:fsr=off_2989 on theBenchmark for (2989ds/180Mi) % 37.06/6.29 % (1462563)Instruction limit reached! % 37.06/6.29 % (1462563)------------------------------ % 37.06/6.29 % (1462563)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 37.06/6.29 % (1462563)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 89.70/13.63 % (1462563)CaDiCaL version: 2.1.3 % 89.70/13.63 % (1462563)Termination reason: Instruction limit % 89.70/13.63 % (1462563)Termination phase: Preprocessing 1 % 89.70/13.63 % (1462563)Time elapsed: 0.090 s % 89.70/13.63 % (1462563)Peak memory usage: 47 MB % 89.70/13.63 % (1462563)Instructions burned: 132 (million) % 89.70/13.63 % (1462569)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1600123416:i=477:bd=all_2988 on theBenchmark for (2988ds/477Mi) % 89.70/13.63 % (1462566)Instruction limit reached! % 89.70/13.63 % (1462566)------------------------------ % 89.70/13.63 % (1462566)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 89.70/13.63 % (1462566)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 89.70/13.63 % (1462566)CaDiCaL version: 2.1.3 % 89.70/13.63 % (1462566)Termination reason: Instruction limit % 89.70/13.63 % (1462566)Termination phase: Unused predicate definition removal % 89.70/13.63 % (1462566)Time elapsed: 0.128 s % 89.70/13.63 % (1462566)Peak memory usage: 48 MB % 89.70/13.63 % (1462566)Instructions burned: 180 (million) % 89.70/13.63 % (1462571)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1139775353:fmbsr=1.3:i=865:ins=25_2987 on theBenchmark for (2987ds/865Mi) % 89.70/13.63 % (1462561)Instruction limit reached! % 89.70/13.63 % (1462561)------------------------------ % 89.70/13.63 % (1462561)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 89.70/13.63 % (1462561)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 89.70/13.63 % (1462561)CaDiCaL version: 2.1.3 % 89.70/13.63 % (1462561)Termination reason: Instruction limit % 89.70/13.63 % (1462561)Termination phase: Preprocessing 3 % 89.70/13.63 % (1462561)Time elapsed: 0.278 s % 89.70/13.63 % (1462561)Peak memory usage: 85 MB % 89.70/13.63 % (1462561)Instructions burned: 717 (million) % 89.70/13.63 % (1462573)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=4208593987:i=1179_2987 on theBenchmark for (2987ds/1179Mi) % 89.70/13.63 % (1462569)Instruction limit reached! % 89.70/13.63 % (1462569)------------------------------ % 89.70/13.63 % (1462569)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 89.70/13.63 % (1462569)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 89.70/13.63 % (1462569)CaDiCaL version: 2.1.3 % 89.70/13.63 % (1462569)Termination reason: Instruction limit % 89.70/13.63 % (1462569)Termination phase: Preprocessing 3 % 89.70/13.63 % (1462569)Time elapsed: 0.333 s % 89.70/13.63 % (1462569)Peak memory usage: 72 MB % 89.70/13.63 % (1462569)Instructions burned: 477 (million) % 89.70/13.63 % (1462575)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1042547022:i=889:ins=1_2985 on theBenchmark for (2985ds/889Mi) % 89.70/13.63 % (1462565)Instruction limit reached! % 89.70/13.63 % (1462565)------------------------------ % 89.70/13.63 % (1462565)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 89.70/13.63 % (1462565)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 89.70/13.63 % (1462565)CaDiCaL version: 2.1.3 % 89.70/13.63 % (1462565)Termination reason: Instruction limit % 89.70/13.63 % (1462565)Termination phase: NewCNF % 89.70/13.63 % (1462565)Time elapsed: 0.475 s % 89.70/13.63 % (1462565)Peak memory usage: 76 MB % 89.70/13.63 % (1462565)Instructions burned: 686 (million) % 89.70/13.63 % (1462577)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=1232589521: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) % 89.70/13.63 % (1462573)Instruction limit reached! % 89.70/13.63 % (1462573)------------------------------ % 89.70/13.63 % (1462573)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 89.70/13.63 % (1462573)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 89.70/13.63 % (1462573)CaDiCaL version: 2.1.3 % 89.70/13.63 % (1462573)Termination reason: Instruction limit % 89.70/13.63 % (1462573)Termination phase: Property scanning % 89.70/13.63 % (1462573)Time elapsed: 0.419 s % 89.70/13.63 % (1462573)Peak memory usage: 96 MB % 89.70/13.63 % (1462573)Instructions burned: 1182 (million) % 89.70/13.63 % (1462579)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=128775476:i=879:kws=inv_precedence:fsr=off_2982 on theBenchmark for (2982ds/879Mi) % 89.70/13.63 % (1462571)Instruction limit reached! % 89.70/13.63 % (1462571)------------------------------ % 89.70/13.63 % (1462571)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 89.70/13.63 % (1462571)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 222.07/32.23 % (1462571)CaDiCaL version: 2.1.3 % 222.07/32.23 % (1462571)Termination reason: Instruction limit % 222.07/32.23 % (1462571)Termination phase: Preprocessing 3 % 222.07/32.23 % (1462571)Time elapsed: 0.769 s % 222.07/32.23 % (1462571)Peak memory usage: 87 MB % 222.07/32.23 % (1462571)Instructions burned: 865 (million) % 222.07/32.23 % (1462581)fmb+10_1_sil=64000:random_seed=1822163506:i=22061:nm=2:gsp=on_2979 on theBenchmark for (2979ds/22061Mi) % 222.07/32.23 % (1462579)Instruction limit reached! % 222.07/32.23 % (1462579)------------------------------ % 222.07/32.23 % (1462579)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 222.07/32.23 % (1462579)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 222.07/32.23 % (1462579)CaDiCaL version: 2.1.3 % 222.07/32.23 % (1462579)Termination reason: Instruction limit % 222.07/32.23 % (1462579)Termination phase: NewCNF % 222.07/32.23 % (1462579)Time elapsed: 0.296 s % 222.07/32.23 % (1462579)Peak memory usage: 83 MB % 222.07/32.23 % (1462579)Instructions burned: 880 (million) % 222.07/32.23 % (1462577)Instruction limit reached! % 222.07/32.23 % (1462577)------------------------------ % 222.07/32.23 % (1462577)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 222.07/32.23 % (1462577)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 222.07/32.23 % (1462577)CaDiCaL version: 2.1.3 % 222.07/32.23 % (1462577)Termination reason: Instruction limit % 222.07/32.23 % (1462577)Termination phase: NewCNF % 222.07/32.23 % (1462577)Time elapsed: 0.486 s % 222.07/32.23 % (1462577)Peak memory usage: 76 MB % 222.07/32.23 % (1462577)Instructions burned: 693 (million) % 222.07/32.23 % (1462583)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1160668206:i=9515:nm=5_2979 on theBenchmark for (2979ds/9515Mi) % 222.07/32.23 % (1462585)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1921656468:fmbsr=1.7:i=920_2979 on theBenchmark for (2979ds/920Mi) % 222.07/32.23 % (1462575)Instruction limit reached! % 222.07/32.23 % (1462575)------------------------------ % 222.07/32.23 % (1462575)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 222.07/32.23 % (1462575)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 222.07/32.23 % (1462575)CaDiCaL version: 2.1.3 % 222.07/32.23 % (1462575)Termination reason: Instruction limit % 222.07/32.23 % (1462575)Termination phase: Preprocessing 3 % 222.07/32.23 % (1462575)Time elapsed: 0.578 s % 222.07/32.23 % (1462575)Peak memory usage: 87 MB % 222.07/32.23 % (1462575)Instructions burned: 890 (million) % 222.07/32.23 % (1462587)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2105138054:i=5131_2979 on theBenchmark for (2979ds/5131Mi) % 222.07/32.23 % (1462585)Instruction limit reached! % 222.07/32.23 % (1462585)------------------------------ % 222.07/32.23 % (1462585)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 222.07/32.23 % (1462585)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 222.07/32.23 % (1462585)CaDiCaL version: 2.1.3 % 222.07/32.23 % (1462585)Termination reason: Instruction limit % 222.07/32.23 % (1462585)Termination phase: Preprocessing 3 % 222.07/32.23 % (1462585)Time elapsed: 0.579 s % 222.07/32.23 % (1462585)Peak memory usage: 88 MB % 222.07/32.23 % (1462585)Instructions burned: 920 (million) % 222.07/32.23 % (1462589)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=4188889031:i=1472:ins=7:fdi=8:gsp=on_2973 on theBenchmark for (2973ds/1472Mi) % 222.07/32.23 % (1462589)Instruction limit reached! % 222.07/32.23 % (1462589)------------------------------ % 222.07/32.23 % (1462589)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 222.07/32.23 % (1462589)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 222.07/32.23 % (1462589)CaDiCaL version: 2.1.3 % 222.07/32.23 % (1462589)Termination reason: Instruction limit % 222.07/32.23 % (1462589)Termination phase: Property scanning % 222.07/32.23 % (1462589)Time elapsed: 1.414 s % 222.07/32.23 % (1462589)Peak memory usage: 96 MB % 222.07/32.23 % (1462589)Instructions burned: 1472 (million) % 222.07/32.23 % (1462623)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=965035300:i=6324_2958 on theBenchmark for (2958ds/6324Mi) % 222.07/32.23 % (1462583)Instruction limit reached! % 222.07/32.23 % (1462583)------------------------------ % 222.07/32.23 % (1462583)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 222.07/32.23 % (1462583)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 222.07/32.23 % (1462583)CaDiCaL version: 2.1.3 % 222.07/32.23 % (1462583)Termination reason: Instruction limit % 222.07/32.23 % (1462583)TerminatioTerminated %------------------------------------------------------------------------------