%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : TOP028+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 : n018.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:24 PM UTC 2026 % Result : Timeout 300.61s 43.34s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : TOP028+3 : TPTP v9.3.1. Released v3.4.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.10/0.23 % Computer : n018.cluster.edu % 0.10/0.23 % Model : x86_64 x86_64 % 0.10/0.23 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.23 % Memory : 8046.5625MB % 0.10/0.23 % OS : Linux 6.8.0-71-generic % 0.10/0.23 % CPULimit : 300 % 0.10/0.23 % WCLimit : 300 % 0.10/0.23 % DateTime : Mon Sep 28 18:56:12 UTC 2026 % 0.10/0.23 % CPUTime : % 0.10/0.23 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.24/0.28 Running first-order model finding % 0.24/0.28 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 % 51.12/8.17 % (3665894)Will run a generic schedule for satisfiability detection. % 51.12/8.17 % (3665902)% WARNING: option uhcvi not known. % 51.12/8.17 % (3665902)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3931912870:i=135531:add=off:rawr=on_2992 on theBenchmark for (2992ds/135531Mi) % 51.12/8.17 % (3665904)dis+10_1_sil=32000:sp=arity:random_seed=2322176503:i=103:fgj=on_2992 on theBenchmark for (2992ds/103Mi) % 51.12/8.17 % (3665901)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3416620714_2992 on theBenchmark for (2992ds/0Mi) % 51.12/8.17 % (3665903)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1731646201:i=88024:add=on:rawr=on_2992 on theBenchmark for (2992ds/88024Mi) % 51.12/8.17 % (3665905)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2158155790:i=116_2992 on theBenchmark for (2992ds/116Mi) % 51.12/8.17 % (3665906)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2501560968:i=131_2992 on theBenchmark for (2992ds/131Mi) % 51.12/8.17 % (3665907)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3467669849:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2992 on theBenchmark for (2992ds/159Mi) % 51.12/8.17 % (3665904)Instruction limit reached! % 51.12/8.17 % (3665904)------------------------------ % 51.12/8.17 % (3665904)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 51.12/8.17 % (3665904)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 51.12/8.17 % (3665904)CaDiCaL version: 2.1.3 % 51.12/8.17 % (3665904)Termination reason: Instruction limit % 51.12/8.17 % (3665904)Termination phase: Preprocessing 1 % 51.12/8.17 % (3665904)Time elapsed: 0.098 s % 51.12/8.17 % (3665904)Peak memory usage: 35 MB % 51.12/8.17 % (3665904)Instructions burned: 104 (million) % 51.12/8.17 % (3665915)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3866118250:i=714:nm=2_2990 on theBenchmark for (2990ds/714Mi) % 51.12/8.17 % (3665905)Instruction limit reached! % 51.12/8.17 % (3665905)------------------------------ % 51.12/8.17 % (3665905)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 51.12/8.17 % (3665905)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 51.12/8.17 % (3665905)CaDiCaL version: 2.1.3 % 51.12/8.17 % (3665905)Termination reason: Instruction limit % 51.12/8.17 % (3665905)Termination phase: Preprocessing 2 % 51.12/8.17 % (3665905)Time elapsed: 0.147 s % 51.12/8.17 % (3665905)Peak memory usage: 37 MB % 51.12/8.17 % (3665905)Instructions burned: 117 (million) % 51.12/8.17 % (3665906)Instruction limit reached! % 51.12/8.17 % (3665906)------------------------------ % 51.12/8.17 % (3665906)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 51.12/8.17 % (3665906)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 51.12/8.17 % (3665906)CaDiCaL version: 2.1.3 % 51.12/8.17 % (3665906)Termination reason: Instruction limit % 51.12/8.17 % (3665906)Termination phase: Preprocessing 2 % 51.12/8.17 % (3665906)Time elapsed: 0.155 s % 51.12/8.17 % (3665906)Peak memory usage: 37 MB % 51.12/8.17 % (3665906)Instructions burned: 131 (million) % 51.12/8.17 % (3665918)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=565538012:i=131:bd=preordered:fsd=on_2990 on theBenchmark for (2990ds/131Mi) % 51.12/8.17 % (3665907)Instruction limit reached! % 51.12/8.17 % (3665907)------------------------------ % 51.12/8.17 % (3665907)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 51.12/8.17 % (3665907)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 51.12/8.17 % (3665907)CaDiCaL version: 2.1.3 % 51.12/8.17 % (3665907)Termination reason: Instruction limit % 51.12/8.17 % (3665907)Termination phase: Preprocessing 2 % 51.12/8.17 % (3665907)Time elapsed: 0.191 s % 51.12/8.17 % (3665907)Peak memory usage: 41 MB % 51.12/8.17 % (3665907)Instructions burned: 159 (million) % 51.12/8.17 % (3665919)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=1104957705:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2990 on theBenchmark for (2990ds/684Mi) % 51.12/8.17 % (3665923)ott-21_1_sil=16000:fs=off:random_seed=477959727:i=180:av=off:fsr=off_2989 on theBenchmark for (2989ds/180Mi) % 51.12/8.17 % (3665918)Instruction limit reached! % 51.12/8.17 % (3665918)------------------------------ % 51.12/8.17 % (3665918)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 51.12/8.17 % (3665918)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 106.28/15.90 % (3665918)CaDiCaL version: 2.1.3 % 106.28/15.90 % (3665918)Termination reason: Instruction limit % 106.28/15.90 % (3665918)Termination phase: Preprocessing 2 % 106.28/15.90 % (3665918)Time elapsed: 0.151 s % 106.28/15.90 % (3665918)Peak memory usage: 37 MB % 106.28/15.90 % (3665918)Instructions burned: 131 (million) % 106.28/15.90 % (3665925)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=211314575:i=477:bd=all_2988 on theBenchmark for (2988ds/477Mi) % 106.28/15.90 % (3665923)Instruction limit reached! % 106.28/15.90 % (3665923)------------------------------ % 106.28/15.90 % (3665923)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 106.28/15.90 % (3665923)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 106.28/15.90 % (3665923)CaDiCaL version: 2.1.3 % 106.28/15.90 % (3665923)Termination reason: Instruction limit % 106.28/15.90 % (3665923)Termination phase: Preprocessing 2 % 106.28/15.90 % (3665923)Time elapsed: 0.222 s % 106.28/15.90 % (3665923)Peak memory usage: 45 MB % 106.28/15.90 % (3665923)Instructions burned: 180 (million) % 106.28/15.90 % (3665927)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=4126947330:fmbsr=1.3:i=865:ins=25_2987 on theBenchmark for (2987ds/865Mi) % 106.28/15.90 % (3665925)Instruction limit reached! % 106.28/15.90 % (3665925)------------------------------ % 106.28/15.90 % (3665925)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 106.28/15.90 % (3665925)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 106.28/15.90 % (3665925)CaDiCaL version: 2.1.3 % 106.28/15.90 % (3665925)Termination reason: Instruction limit % 106.28/15.90 % (3665925)Termination phase: Preprocessing 3 % 106.28/15.90 % (3665925)Time elapsed: 0.488 s % 106.28/15.90 % (3665925)Peak memory usage: 57 MB % 106.28/15.90 % (3665925)Instructions burned: 477 (million) % 106.28/15.90 % (3665919)Instruction limit reached! % 106.28/15.90 % (3665919)------------------------------ % 106.28/15.90 % (3665919)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 106.28/15.90 % (3665919)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 106.28/15.90 % (3665919)CaDiCaL version: 2.1.3 % 106.28/15.90 % (3665919)Termination reason: Instruction limit % 106.28/15.90 % (3665919)Termination phase: NewCNF % 106.28/15.90 % (3665919)Time elapsed: 0.665 s % 106.28/15.90 % (3665919)Peak memory usage: 61 MB % 106.28/15.90 % (3665919)Instructions burned: 685 (million) % 106.28/15.90 % (3665915)Instruction limit reached! % 106.28/15.90 % (3665915)------------------------------ % 106.28/15.90 % (3665915)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 106.28/15.90 % (3665915)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 106.28/15.90 % (3665915)CaDiCaL version: 2.1.3 % 106.28/15.90 % (3665915)Termination reason: Instruction limit % 106.28/15.90 % (3665915)Termination phase: Preprocessing 3 % 106.28/15.90 % (3665915)Time elapsed: 0.742 s % 106.28/15.90 % (3665915)Peak memory usage: 70 MB % 106.28/15.90 % (3665915)Instructions burned: 714 (million) % 106.28/15.90 % (3665931)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=447237944:i=1179_2983 on theBenchmark for (2983ds/1179Mi) % 106.28/15.90 % (3665932)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1687826573:i=889:ins=1_2983 on theBenchmark for (2983ds/889Mi) % 106.28/15.90 % (3665933)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=2937031748:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2982 on theBenchmark for (2982ds/692Mi) % 106.28/15.90 % (3665927)Instruction limit reached! % 106.28/15.90 % (3665927)------------------------------ % 106.28/15.90 % (3665927)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 106.28/15.90 % (3665927)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 106.28/15.90 % (3665927)CaDiCaL version: 2.1.3 % 106.28/15.90 % (3665927)Termination reason: Instruction limit % 106.28/15.90 % (3665927)Termination phase: Property scanning % 106.28/15.90 % (3665927)Time elapsed: 0.859 s % 106.28/15.90 % (3665927)Peak memory usage: 65 MB % 106.28/15.90 % (3665927)Instructions burned: 866 (million) % 106.28/15.90 % (3665937)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3637424207:i=879:kws=inv_precedence:fsr=off_2978 on theBenchmark for (2978ds/879Mi) % 106.28/15.90 % (3665933)Instruction limit reached! % 106.28/15.90 % (3665933)------------------------------ % 106.28/15.90 % (3665933)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 106.28/15.90 % (3665933)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.19/25.92 % (3665933)CaDiCaL version: 2.1.3 % 177.19/25.92 % (3665933)Termination reason: Instruction limit % 177.19/25.92 % (3665933)Termination phase: NewCNF % 177.19/25.92 % (3665933)Time elapsed: 0.680 s % 177.19/25.92 % (3665933)Peak memory usage: 61 MB % 177.19/25.92 % (3665933)Instructions burned: 693 (million) % 177.19/25.92 % (3665939)fmb+10_1_sil=64000:random_seed=812215881:i=22061:nm=2:gsp=on_2975 on theBenchmark for (2975ds/22061Mi) % 177.19/25.92 % (3665932)Instruction limit reached! % 177.19/25.92 % (3665932)------------------------------ % 177.19/25.92 % (3665932)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 177.19/25.92 % (3665932)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.19/25.92 % (3665932)CaDiCaL version: 2.1.3 % 177.19/25.92 % (3665932)Termination reason: Instruction limit % 177.19/25.92 % (3665932)Termination phase: Property scanning % 177.19/25.92 % (3665932)Time elapsed: 0.872 s % 177.19/25.92 % (3665932)Peak memory usage: 65 MB % 177.19/25.92 % (3665932)Instructions burned: 889 (million) % 177.19/25.92 % (3665941)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1891382713:i=9515:nm=5_2973 on theBenchmark for (2973ds/9515Mi) % 177.19/25.92 % (3665931)Instruction limit reached! % 177.19/25.92 % (3665931)------------------------------ % 177.19/25.92 % (3665931)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 177.19/25.92 % (3665931)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.19/25.92 % (3665931)CaDiCaL version: 2.1.3 % 177.19/25.92 % (3665931)Termination reason: Instruction limit % 177.19/25.92 % (3665931)Termination phase: Property scanning % 177.19/25.92 % (3665931)Time elapsed: 1.139 s % 177.19/25.92 % (3665931)Peak memory usage: 71 MB % 177.19/25.92 % (3665931)Instructions burned: 1180 (million) % 177.19/25.92 % (3665943)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=260762015:fmbsr=1.7:i=920_2971 on theBenchmark for (2971ds/920Mi) % 177.19/25.92 % (3665937)Instruction limit reached! % 177.19/25.92 % (3665937)------------------------------ % 177.19/25.92 % (3665937)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 177.19/25.92 % (3665937)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.19/25.92 % (3665937)CaDiCaL version: 2.1.3 % 177.19/25.92 % (3665937)Termination reason: Instruction limit % 177.19/25.92 % (3665937)Termination phase: NewCNF % 177.19/25.92 % (3665937)Time elapsed: 0.771 s % 177.19/25.92 % (3665937)Peak memory usage: 67 MB % 177.19/25.92 % (3665937)Instructions burned: 879 (million) % 177.19/25.92 % (3665945)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=867486191:i=5131_2969 on theBenchmark for (2969ds/5131Mi) % 177.19/25.92 % (3665943)Instruction limit reached! % 177.19/25.92 % (3665943)------------------------------ % 177.19/25.92 % (3665943)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 177.19/25.92 % (3665943)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.19/25.92 % (3665943)CaDiCaL version: 2.1.3 % 177.19/25.92 % (3665943)Termination reason: Instruction limit % 177.19/25.92 % (3665943)Termination phase: Property scanning % 177.19/25.92 % (3665943)Time elapsed: 0.904 s % 177.19/25.92 % (3665943)Peak memory usage: 65 MB % 177.19/25.92 % (3665943)Instructions burned: 920 (million) % 177.19/25.92 % (3665951)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=723087501:i=1472:ins=7:fdi=8:gsp=on_2961 on theBenchmark for (2961ds/1472Mi) % 177.19/25.92 % (3665951)Instruction limit reached! % 177.19/25.92 % (3665951)------------------------------ % 177.19/25.92 % (3665951)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 177.19/25.92 % (3665951)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.19/25.92 % (3665951)CaDiCaL version: 2.1.3 % 177.19/25.92 % (3665951)Termination reason: Instruction limit % 177.19/25.92 % (3665951)Termination phase: Property scanning % 177.19/25.92 % (3665951)Time elapsed: 1.330 s % 177.19/25.92 % (3665951)Peak memory usage: 67 MB % 177.19/25.92 % (3665951)Instructions burned: 1472 (million) % 177.19/25.92 % (3665957)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=289546699:i=6324_2948 on theBenchmark for (2948ds/6324Mi) % 177.19/25.92 % (3665945)Instruction limit reached! % 177.19/25.92 % (3665945)------------------------------ % 177.19/25.92 % (3665945)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 177.19/25.92 % (3665945)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.19/25.92 % (3665945)CaDiCaL version: 2.1.3 % 177.19/25.92 % (3665945)Termination reason: Instruction limit % 177.19/25.92 % (3665945)Termination phase: SaturatiTerminated %------------------------------------------------------------------------------