%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : TOP011-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n017.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:33:50 PM UTC 2026
% Result : Satisfiable 19.22s 3.73s
% Output : Saturation 20.85s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u120,negated_conjecture,
element_of_set(cu,top_of_basis(f)) ).
cnf(u129,negated_conjecture,
( ~ equal_sets(cu,union_of_members(X0))
| ~ subset_collections(X0,f) ) ).
cnf(u133,axiom,
( element_of_collection(empty_set,X1)
| ~ topological_space(X0,X1) ) ).
cnf(u137,axiom,
( ~ topological_space(X0,X1)
| element_of_collection(X0,X1) ) ).
cnf(u141,axiom,
( ~ hausdorff(X0,X1)
| topological_space(X0,X1) ) ).
cnf(u145,axiom,
( ~ connected_space(X0,X1)
| topological_space(X0,X1) ) ).
cnf(u149,axiom,
( ~ compact_space(X0,X1)
| topological_space(X0,X1) ) ).
cnf(u153,axiom,
( equal_sets(union_of_members(X1),X0)
| ~ topological_space(X0,X1) ) ).
cnf(u157,axiom,
( ~ open(X0,X1,X2)
| topological_space(X1,X2) ) ).
cnf(u161,axiom,
( element_of_collection(X0,X2)
| ~ open(X0,X1,X2) ) ).
cnf(u165,axiom,
( ~ closed(X0,X1,X2)
| topological_space(X1,X2) ) ).
cnf(u169,axiom,
( ~ finer(X0,X1,X2)
| topological_space(X2,X0) ) ).
cnf(u173,axiom,
( ~ finer(X0,X1,X2)
| topological_space(X2,X1) ) ).
cnf(u177,axiom,
( subset_collections(X1,X0)
| ~ finer(X0,X1,X2) ) ).
cnf(u181,axiom,
( equal_sets(union_of_members(X1),X0)
| ~ basis(X0,X1) ) ).
cnf(u185,axiom,
( ~ connected_set(X0,X1,X2)
| topological_space(X1,X2) ) ).
cnf(u189,axiom,
( subset_sets(X0,X1)
| ~ connected_set(X0,X1,X2) ) ).
cnf(u193,axiom,
( ~ open_covering(X0,X1,X2)
| topological_space(X1,X2) ) ).
cnf(u197,axiom,
( subset_collections(X0,X2)
| ~ open_covering(X0,X1,X2) ) ).
cnf(u201,axiom,
( ~ compact_set(X0,X1,X2)
| topological_space(X1,X2) ) ).
cnf(u205,axiom,
( subset_sets(X0,X1)
| ~ compact_set(X0,X1,X2) ) ).
cnf(u209,axiom,
( ~ neighborhood(X0,X1,X2,X3)
| topological_space(X2,X3) ) ).
cnf(u213,axiom,
( element_of_set(X1,X0)
| ~ neighborhood(X0,X1,X2,X3) ) ).
cnf(u217,axiom,
( ~ limit_point(X0,X1,X2,X3)
| topological_space(X2,X3) ) ).
cnf(u221,axiom,
( subset_sets(X1,X2)
| ~ limit_point(X0,X1,X2,X3) ) ).
cnf(u225,axiom,
( ~ separation(X0,X1,X2,X3)
| topological_space(X2,X3) ) ).
cnf(u229,axiom,
( ~ separation(X0,X1,X2,X3)
| ~ equal_sets(X0,empty_set) ) ).
cnf(u233,axiom,
( ~ separation(X0,X1,X2,X3)
| ~ equal_sets(X1,empty_set) ) ).
cnf(u237,axiom,
( element_of_collection(X0,X3)
| ~ separation(X0,X1,X2,X3) ) ).
cnf(u241,axiom,
( element_of_collection(X1,X3)
| ~ separation(X0,X1,X2,X3) ) ).
cnf(u245,axiom,
( disjoint_s(X0,X1)
| ~ separation(X0,X1,X2,X3) ) ).
cnf(u249,axiom,
( ~ separation(X2,X3,X0,X1)
| ~ connected_space(X0,X1) ) ).
cnf(u253,axiom,
( equal_sets(union_of_members(X0),X1)
| ~ open_covering(X0,X1,X2) ) ).
cnf(u257,axiom,
( element_of_set(X0,f1(X1,X0))
| ~ element_of_set(X0,union_of_members(X1)) ) ).
cnf(u261,axiom,
( element_of_collection(f1(X1,X0),X1)
| ~ element_of_set(X0,union_of_members(X1)) ) ).
cnf(u265,axiom,
( element_of_collection(f2(X1,X0),X1)
| element_of_set(X0,intersection_of_members(X1)) ) ).
cnf(u269,axiom,
( element_of_set(X0,intersection_of_members(X1))
| ~ element_of_set(X0,f2(X1,X0)) ) ).
cnf(u273,axiom,
( element_of_collection(X0,top_of_basis(X1))
| element_of_set(f11(X1,X0),X0) ) ).
cnf(u277,axiom,
( topological_space(X1,X2)
| ~ element_of_collection(X0,subspace_topology(X1,X2,X3)) ) ).
cnf(u281,axiom,
( subset_sets(X3,X1)
| ~ element_of_collection(X0,subspace_topology(X1,X2,X3)) ) ).
cnf(u285,axiom,
( ~ element_of_set(X0,interior(X1,X2,X3))
| topological_space(X2,X3) ) ).
cnf(u289,axiom,
( subset_sets(X1,X2)
| ~ element_of_set(X0,interior(X1,X2,X3)) ) ).
cnf(u293,axiom,
( ~ element_of_set(X0,closure(X1,X2,X3))
| topological_space(X2,X3) ) ).
cnf(u297,axiom,
( subset_sets(X1,X2)
| ~ element_of_set(X0,closure(X1,X2,X3)) ) ).
cnf(u301,axiom,
( ~ neighborhood(X0,X1,X2,X3)
| open(X0,X2,X3) ) ).
cnf(u305,axiom,
( ~ element_of_set(X0,boundary(X1,X2,X3))
| topological_space(X2,X3) ) ).
cnf(u313,axiom,
( element_of_collection(X1,X2)
| ~ element_of_collection(X0,subspace_topology(X1,X2,X3)) ) ).
cnf(u317,axiom,
( element_of_set(X0,union_of_members(X1))
| ~ element_of_set(X0,X2)
| ~ element_of_collection(X2,X1) ) ).
cnf(u321,axiom,
( element_of_set(X0,X2)
| ~ element_of_collection(X2,X1)
| ~ element_of_set(X0,intersection_of_members(X1)) ) ).
cnf(u325,axiom,
( element_of_collection(union_of_members(X2),X1)
| ~ subset_collections(X2,X1)
| ~ topological_space(X0,X1) ) ).
cnf(u329,axiom,
( open(X0,X1,X2)
| ~ topological_space(X1,X2)
| ~ element_of_collection(X0,X2) ) ).
cnf(u333,axiom,
( open(relative_complement_sets(X0,X1),X1,X2)
| ~ closed(X0,X1,X2) ) ).
cnf(u337,axiom,
( equal_sets(union_of_sets(X0,X1),X2)
| ~ separation(X0,X1,X2,X3) ) ).
cnf(u341,axiom,
( connected_space(X0,subspace_topology(X1,X2,X0))
| ~ connected_set(X0,X1,X2) ) ).
cnf(u345,axiom,
( compact_space(X0,subspace_topology(X1,X2,X0))
| ~ compact_set(X0,X1,X2) ) ).
cnf(u356,axiom,
( topological_space(X0,subspace_topology(X1,X2,X0))
| ~ connected_set(X0,X1,X2) ) ).
cnf(u360,axiom,
( topological_space(X0,subspace_topology(X1,X2,X0))
| ~ compact_set(X0,X1,X2) ) ).
cnf(u366,axiom,
( element_of_collection(X0,subspace_topology(X1,X2,X0))
| ~ connected_set(X0,X1,X2) ) ).
cnf(u370,axiom,
( element_of_collection(X0,subspace_topology(X1,X2,X0))
| ~ compact_set(X0,X1,X2) ) ).
cnf(u374,axiom,
( hausdorff(X0,X1)
| ~ topological_space(X0,X1)
| element_of_set(f19(X0,X1),X0) ) ).
cnf(u378,axiom,
( hausdorff(X0,X1)
| ~ topological_space(X0,X1)
| element_of_set(f20(X0,X1),X0) ) ).
cnf(u384,axiom,
( ~ neighborhood(interior(X2,X0,X1),X3,X4,X5)
| topological_space(X0,X1) ) ).
cnf(u388,axiom,
( ~ neighborhood(closure(X2,X0,X1),X3,X4,X5)
| topological_space(X0,X1) ) ).
cnf(u392,axiom,
( ~ neighborhood(boundary(X2,X0,X1),X3,X4,X5)
| topological_space(X0,X1) ) ).
cnf(u396,axiom,
( basis(X0,X1)
| ~ equal_sets(union_of_members(X1),X0)
| element_of_set(f7(X0,X1),X0) ) ).
cnf(u400,axiom,
( element_of_collection(f8(X0,X1),X1)
| ~ equal_sets(union_of_members(X1),X0)
| basis(X0,X1) ) ).
cnf(u404,axiom,
( element_of_collection(f9(X0,X1),X1)
| ~ equal_sets(union_of_members(X1),X0)
| basis(X0,X1) ) ).
cnf(u408,axiom,
( element_of_set(X0,closure(X1,X2,X3))
| ~ element_of_set(X0,boundary(X1,X2,X3)) ) ).
cnf(u412,axiom,
( finite(f23(X0,X1,X2))
| ~ open_covering(X2,X0,X1)
| ~ compact_space(X0,X1) ) ).
cnf(u416,axiom,
( compact_space(X0,X1)
| ~ topological_space(X0,X1)
| open_covering(f24(X0,X1),X0,X1) ) ).
cnf(u422,axiom,
( closed(X0,X1,X2)
| ~ topological_space(X1,X2)
| ~ open(relative_complement_sets(X0,X1),X1,X2) ) ).
cnf(u426,axiom,
( finer(X0,X1,X2)
| ~ topological_space(X2,X0)
| ~ topological_space(X2,X1)
| ~ subset_collections(X1,X0) ) ).
cnf(u430,axiom,
( element_of_set(X2,f10(X1,X0,X2))
| ~ element_of_set(X2,X0)
| ~ element_of_collection(X0,top_of_basis(X1)) ) ).
cnf(u434,axiom,
( element_of_collection(f10(X1,X0,X2),X1)
| ~ element_of_set(X2,X0)
| ~ element_of_collection(X0,top_of_basis(X1)) ) ).
cnf(u438,axiom,
( subset_sets(f10(X1,X0,X2),X0)
| ~ element_of_set(X2,X0)
| ~ element_of_collection(X0,top_of_basis(X1)) ) ).
cnf(u442,axiom,
( element_of_collection(f12(X1,X2,X3,X0),X2)
| ~ element_of_collection(X0,subspace_topology(X1,X2,X3)) ) ).
cnf(u446,axiom,
( element_of_set(X0,f13(X1,X2,X3,X0))
| ~ element_of_set(X0,interior(X1,X2,X3)) ) ).
cnf(u450,axiom,
( subset_sets(f13(X1,X2,X3,X0),X1)
| ~ element_of_set(X0,interior(X1,X2,X3)) ) ).
cnf(u454,axiom,
( ~ eq_p(f19(X0,X1),f20(X0,X1))
| ~ topological_space(X0,X1)
| hausdorff(X0,X1) ) ).
cnf(u458,axiom,
( subset_collections(f23(X0,X1,X2),X2)
| ~ open_covering(X2,X0,X1)
| ~ compact_space(X0,X1) ) ).
cnf(u465,axiom,
( topological_space(X1,X2)
| ~ element_of_set(X4,intersection_of_members(X3))
| ~ element_of_collection(interior(X0,X1,X2),X3) ) ).
cnf(u469,axiom,
( topological_space(X1,X2)
| ~ element_of_set(X4,intersection_of_members(X3))
| ~ element_of_collection(closure(X0,X1,X2),X3) ) ).
cnf(u473,axiom,
( topological_space(X1,X2)
| ~ element_of_set(X4,intersection_of_members(X3))
| ~ element_of_collection(boundary(X0,X1,X2),X3) ) ).
cnf(u479,axiom,
( element_of_collection(intersection_of_sets(X2,X3),X1)
| ~ element_of_collection(X2,X1)
| ~ element_of_collection(X3,X1)
| ~ topological_space(X0,X1) ) ).
cnf(u484,axiom,
( element_of_collection(X3,X4)
| ~ element_of_collection(interior(X2,X3,X4),X1)
| ~ element_of_set(X0,intersection_of_members(X1)) ) ).
cnf(u488,axiom,
( element_of_collection(X3,X4)
| ~ element_of_collection(closure(X2,X3,X4),X1)
| ~ element_of_set(X0,intersection_of_members(X1)) ) ).
cnf(u492,axiom,
( element_of_collection(X3,X4)
| ~ element_of_collection(boundary(X2,X3,X4),X1)
| ~ element_of_set(X0,intersection_of_members(X1)) ) ).
cnf(u496,axiom,
( open(f13(X1,X2,X3,X0),X2,X3)
| ~ element_of_set(X0,interior(X1,X2,X3)) ) ).
cnf(u500,axiom,
( element_of_set(X0,closure(relative_complement_sets(X1,X2),X2,X3))
| ~ element_of_set(X0,boundary(X1,X2,X3)) ) ).
cnf(u504,axiom,
( open_covering(X0,X1,X2)
| ~ topological_space(X1,X2)
| ~ subset_collections(X0,X2)
| ~ equal_sets(union_of_members(X0),X1) ) ).
cnf(u508,axiom,
( open_covering(f23(X0,X1,X2),X0,X1)
| ~ open_covering(X2,X0,X1)
| ~ compact_space(X0,X1) ) ).
cnf(u516,axiom,
( element_of_collection(X0,top_of_basis(X1))
| ~ element_of_set(f11(X1,X0),X2)
| ~ element_of_collection(X2,X1)
| ~ subset_sets(X2,X0) ) ).
cnf(u520,axiom,
( equal_sets(X0,intersection_of_sets(X3,f12(X1,X2,X3,X0)))
| ~ element_of_collection(X0,subspace_topology(X1,X2,X3)) ) ).
cnf(u524,axiom,
( neighborhood(X0,X1,X2,X3)
| ~ topological_space(X2,X3)
| ~ open(X0,X2,X3)
| ~ element_of_set(X1,X0) ) ).
cnf(u528,axiom,
( connected_space(X0,X1)
| ~ topological_space(X0,X1)
| separation(f21(X0,X1),f22(X0,X1),X0,X1) ) ).
cnf(u538,axiom,
( element_of_set(X0,X4)
| ~ subset_sets(X1,X4)
| ~ closed(X4,X2,X3)
| ~ element_of_set(X0,closure(X1,X2,X3)) ) ).
cnf(u542,axiom,
( connected_set(X0,X1,X2)
| ~ topological_space(X1,X2)
| ~ subset_sets(X0,X1)
| ~ connected_space(X0,subspace_topology(X1,X2,X0)) ) ).
cnf(u546,axiom,
( compact_set(X0,X1,X2)
| ~ topological_space(X1,X2)
| ~ subset_sets(X0,X1)
| ~ compact_space(X0,subspace_topology(X1,X2,X0)) ) ).
cnf(u555,axiom,
( compact_space(X0,X1)
| ~ topological_space(X0,X1)
| ~ finite(X2)
| ~ subset_collections(X2,f24(X0,X1))
| ~ open_covering(X2,X0,X1) ) ).
cnf(u560,axiom,
( element_of_set(f7(X0,X1),intersection_of_sets(f8(X0,X1),f9(X0,X1)))
| ~ equal_sets(union_of_members(X1),X0)
| basis(X0,X1) ) ).
cnf(u564,axiom,
( ~ eq_p(f15(X0,X1,X2,X3,X4),X0)
| ~ neighborhood(X4,X0,X2,X3)
| ~ limit_point(X0,X1,X2,X3) ) ).
cnf(u568,axiom,
( subset_sets(X1,f14(X1,X2,X3,X0))
| ~ topological_space(X2,X3)
| ~ subset_sets(X1,X2)
| element_of_set(X0,closure(X1,X2,X3)) ) ).
cnf(u572,axiom,
( element_of_set(X0,closure(X1,X2,X3))
| ~ topological_space(X2,X3)
| ~ subset_sets(X1,X2)
| ~ element_of_set(X0,f14(X1,X2,X3,X0)) ) ).
cnf(u577,axiom,
( element_of_collection(X0,subspace_topology(X1,X2,X3))
| ~ topological_space(X1,X2)
| ~ subset_sets(X3,X1)
| ~ element_of_collection(X4,X2)
| ~ equal_sets(X0,intersection_of_sets(X3,X4)) ) ).
cnf(u581,axiom,
( element_of_set(X0,closure(X1,X2,X3))
| ~ topological_space(X2,X3)
| ~ subset_sets(X1,X2)
| closed(f14(X1,X2,X3,X0),X2,X3) ) ).
cnf(u585,axiom,
( element_of_set(f15(X0,X1,X2,X3,X4),intersection_of_sets(X4,X1))
| ~ neighborhood(X4,X0,X2,X3)
| ~ limit_point(X0,X1,X2,X3) ) ).
cnf(u589,axiom,
( limit_point(X0,X1,X2,X3)
| ~ topological_space(X2,X3)
| ~ subset_sets(X1,X2)
| neighborhood(f16(X0,X1,X2,X3),X0,X2,X3) ) ).
cnf(u595,axiom,
( eq_p(X2,X3)
| ~ element_of_set(X2,X0)
| ~ element_of_set(X3,X0)
| ~ hausdorff(X0,X1)
| neighborhood(f17(X0,X1,X2,X3),X2,X0,X1) ) ).
cnf(u599,axiom,
( eq_p(X2,X3)
| ~ element_of_set(X2,X0)
| ~ element_of_set(X3,X0)
| ~ hausdorff(X0,X1)
| neighborhood(f18(X0,X1,X2,X3),X3,X0,X1) ) ).
cnf(u607,axiom,
( element_of_set(X0,interior(X1,X2,X3))
| ~ topological_space(X2,X3)
| ~ subset_sets(X1,X2)
| ~ element_of_set(X0,X4)
| ~ subset_sets(X4,X1)
| ~ open(X4,X2,X3) ) ).
cnf(u612,axiom,
( topological_space(X2,X3)
| ~ closed(interior(X1,X2,X3),X4,X5)
| ~ element_of_set(X6,closure(X0,X4,X5))
| ~ subset_sets(X0,interior(X1,X2,X3)) ) ).
cnf(u616,axiom,
( topological_space(X2,X3)
| ~ closed(closure(X1,X2,X3),X4,X5)
| ~ element_of_set(X6,closure(X0,X4,X5))
| ~ subset_sets(X0,closure(X1,X2,X3)) ) ).
cnf(u620,axiom,
( topological_space(X2,X3)
| ~ closed(boundary(X1,X2,X3),X4,X5)
| ~ element_of_set(X6,closure(X0,X4,X5))
| ~ subset_sets(X0,boundary(X1,X2,X3)) ) ).
cnf(u627,axiom,
( element_of_collection(X1,X2)
| ~ element_of_set(X5,closure(X6,X3,X4))
| ~ subset_sets(X6,interior(X0,X1,X2))
| ~ closed(interior(X0,X1,X2),X3,X4) ) ).
cnf(u631,axiom,
( element_of_collection(X1,X2)
| ~ element_of_set(X5,closure(X6,X3,X4))
| ~ subset_sets(X6,closure(X0,X1,X2))
| ~ closed(closure(X0,X1,X2),X3,X4) ) ).
cnf(u635,axiom,
( element_of_collection(X1,X2)
| ~ element_of_set(X5,closure(X6,X3,X4))
| ~ subset_sets(X6,boundary(X0,X1,X2))
| ~ closed(boundary(X0,X1,X2),X3,X4) ) ).
cnf(u639,axiom,
( subset_collections(f5(X0,X1),X1)
| ~ equal_sets(union_of_members(X1),X0)
| ~ element_of_collection(empty_set,X1)
| ~ element_of_collection(X0,X1)
| element_of_collection(f3(X0,X1),X1)
| topological_space(X0,X1) ) ).
cnf(u643,axiom,
( subset_collections(f5(X0,X1),X1)
| ~ equal_sets(union_of_members(X1),X0)
| ~ element_of_collection(empty_set,X1)
| ~ element_of_collection(X0,X1)
| element_of_collection(f4(X0,X1),X1)
| topological_space(X0,X1) ) ).
cnf(u647,axiom,
( limit_point(X0,X1,X2,X3)
| ~ topological_space(X2,X3)
| ~ subset_sets(X1,X2)
| ~ element_of_set(X4,intersection_of_sets(f16(X0,X1,X2,X3),X1))
| eq_p(X4,X0) ) ).
cnf(u651,axiom,
( element_of_set(X0,boundary(X1,X2,X3))
| ~ topological_space(X2,X3)
| ~ element_of_set(X0,closure(X1,X2,X3))
| ~ element_of_set(X0,closure(relative_complement_sets(X1,X2),X2,X3)) ) ).
cnf(u655,axiom,
( disjoint_s(f17(X0,X1,X2,X3),f18(X0,X1,X2,X3))
| ~ element_of_set(X2,X0)
| ~ element_of_set(X3,X0)
| eq_p(X2,X3)
| ~ hausdorff(X0,X1) ) ).
cnf(u659,axiom,
( hausdorff(X0,X1)
| ~ topological_space(X0,X1)
| ~ neighborhood(X2,f19(X0,X1),X0,X1)
| ~ neighborhood(X3,f20(X0,X1),X0,X1)
| ~ disjoint_s(X2,X3) ) ).
cnf(u666,axiom,
( element_of_collection(f3(X0,X1),X1)
| ~ equal_sets(union_of_members(X1),X0)
| ~ element_of_collection(empty_set,X1)
| ~ element_of_collection(X0,X1)
| topological_space(X0,X1)
| ~ element_of_collection(union_of_members(f5(X0,X1)),X1) ) ).
cnf(u670,axiom,
( element_of_collection(f4(X0,X1),X1)
| ~ equal_sets(union_of_members(X1),X0)
| ~ element_of_collection(empty_set,X1)
| ~ element_of_collection(X0,X1)
| topological_space(X0,X1)
| ~ element_of_collection(union_of_members(f5(X0,X1)),X1) ) ).
cnf(u674,axiom,
( basis(X0,X1)
| ~ equal_sets(union_of_members(X1),X0)
| ~ element_of_set(f7(X0,X1),X2)
| ~ element_of_collection(X2,X1)
| ~ subset_sets(X2,intersection_of_sets(f8(X0,X1),f9(X0,X1))) ) ).
cnf(u678,axiom,
( element_of_set(X2,f6(X0,X1,X2,X3,X4))
| ~ element_of_set(X2,X0)
| ~ element_of_collection(X3,X1)
| ~ element_of_collection(X4,X1)
| ~ element_of_set(X2,intersection_of_sets(X3,X4))
| ~ basis(X0,X1) ) ).
cnf(u682,axiom,
( element_of_collection(f6(X0,X1,X2,X3,X4),X1)
| ~ element_of_set(X2,X0)
| ~ element_of_collection(X3,X1)
| ~ element_of_collection(X4,X1)
| ~ element_of_set(X2,intersection_of_sets(X3,X4))
| ~ basis(X0,X1) ) ).
cnf(u686,axiom,
( subset_collections(f5(X0,X1),X1)
| ~ equal_sets(union_of_members(X1),X0)
| ~ element_of_collection(empty_set,X1)
| ~ element_of_collection(X0,X1)
| ~ element_of_collection(intersection_of_sets(f3(X0,X1),f4(X0,X1)),X1)
| topological_space(X0,X1) ) ).
cnf(u690,axiom,
( subset_sets(f6(X0,X1,X2,X3,X4),intersection_of_sets(X3,X4))
| ~ element_of_set(X2,X0)
| ~ element_of_collection(X3,X1)
| ~ element_of_collection(X4,X1)
| ~ element_of_set(X2,intersection_of_sets(X3,X4))
| ~ basis(X0,X1) ) ).
cnf(u694,axiom,
( topological_space(X0,X1)
| ~ equal_sets(union_of_members(X1),X0)
| ~ element_of_collection(empty_set,X1)
| ~ element_of_collection(X0,X1)
| ~ element_of_collection(intersection_of_sets(f3(X0,X1),f4(X0,X1)),X1)
| ~ element_of_collection(union_of_members(f5(X0,X1)),X1) ) ).
cnf(u698,axiom,
( equal_sets(X1,empty_set)
| ~ topological_space(X2,X3)
| equal_sets(X0,empty_set)
| separation(X0,X1,X2,X3)
| ~ element_of_collection(X0,X3)
| ~ element_of_collection(X1,X3)
| ~ equal_sets(union_of_sets(X0,X1),X2)
| ~ disjoint_s(X0,X1) ) ).
cnf(u703,axiom,
( hausdorff(X0,X1)
| ~ element_of_set(f20(X0,X1),X2)
| ~ hausdorff(X2,X3)
| neighborhood(f17(X2,X3,f19(X0,X1),f20(X0,X1)),f19(X0,X1),X2,X3)
| ~ topological_space(X0,X1)
| ~ element_of_set(f19(X0,X1),X2) ) ).
cnf(u707,axiom,
( hausdorff(X0,X1)
| ~ element_of_set(f20(X0,X1),X2)
| ~ hausdorff(X2,X3)
| neighborhood(f18(X2,X3,f19(X0,X1),f20(X0,X1)),f20(X0,X1),X2,X3)
| ~ topological_space(X0,X1)
| ~ element_of_set(f19(X0,X1),X2) ) ).
cnf(u713,axiom,
( neighborhood(f18(X5,X6,f15(X0,X1,X2,X3,X4),X0),X0,X5,X6)
| ~ element_of_set(X0,X5)
| ~ hausdorff(X5,X6)
| ~ element_of_set(f15(X0,X1,X2,X3,X4),X5)
| ~ neighborhood(X4,X0,X2,X3)
| ~ limit_point(X0,X1,X2,X3) ) ).
cnf(u719,axiom,
( open(f18(X1,X2,f15(X0,X3,X4,X5,X6),X0),X1,X2)
| ~ hausdorff(X1,X2)
| ~ element_of_set(f15(X0,X3,X4,X5,X6),X1)
| ~ neighborhood(X6,X0,X4,X5)
| ~ limit_point(X0,X3,X4,X5)
| ~ element_of_set(X0,X1) ) ).
cnf(u724,axiom,
( neighborhood(f17(X5,X6,f15(X0,X1,X2,X3,X4),X0),f15(X0,X1,X2,X3,X4),X5,X6)
| ~ element_of_set(X0,X5)
| ~ hausdorff(X5,X6)
| ~ element_of_set(f15(X0,X1,X2,X3,X4),X5)
| ~ neighborhood(X4,X0,X2,X3)
| ~ limit_point(X0,X1,X2,X3) ) ).
cnf(u730,axiom,
( open(f17(X1,X2,f15(X0,X3,X4,X5,X6),X0),X1,X2)
| ~ hausdorff(X1,X2)
| ~ element_of_set(f15(X0,X3,X4,X5,X6),X1)
| ~ neighborhood(X6,X0,X4,X5)
| ~ limit_point(X0,X3,X4,X5)
| ~ element_of_set(X0,X1) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : TOP011-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.23 % Computer : n017.cluster.edu
% 0.11/0.23 % Model : x86_64 x86_64
% 0.11/0.23 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.23 % Memory : 8046.5625MB
% 0.11/0.23 % OS : Linux 6.8.0-71-generic
% 0.11/0.23 % CPULimit : 300
% 0.11/0.23 % WCLimit : 300
% 0.11/0.23 % DateTime : Mon Sep 28 18:44:21 UTC 2026
% 0.11/0.24 % CPUTime :
% 0.11/0.24 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.24/0.29 Running first-order theorem proving
% 0.24/0.29 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 13.23/3.04 % (3874457)Input is clausal, will run a generic CNF schedule.
% 13.23/3.04 % (3874467)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=4102215984:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 13.23/3.04 % (3874466)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=3101174713:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 13.23/3.04 % (3874466)Refutation not found, incomplete strategy
% 13.23/3.04 % (3874466)------------------------------
% 13.23/3.04 % (3874466)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.23/3.04 % (3874466)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.23/3.04 % (3874466)CaDiCaL version: 2.1.3
% 13.23/3.04 % (3874466)Termination reason: Refutation not found, incomplete strategy
% 13.23/3.04 % (3874466)Time elapsed: 0.002 s
% 13.23/3.04 % (3874466)Peak memory usage: 88 MB
% 13.23/3.04 % (3874466)Instructions burned: 1 (million)
% 13.23/3.04 % (3874463)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=2444316481:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 13.23/3.04 % (3874462)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=4037688493:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 13.23/3.04 % (3874467)Instruction limit reached!
% 13.23/3.04 % (3874467)------------------------------
% 13.23/3.04 % (3874467)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.23/3.04 % (3874467)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.23/3.04 % (3874467)CaDiCaL version: 2.1.3
% 13.23/3.04 % (3874467)Termination reason: Instruction limit
% 13.23/3.04 % (3874467)Termination phase: Saturation
% 13.23/3.04 % (3874467)Time elapsed: 0.096 s
% 13.23/3.04 % (3874467)Peak memory usage: 89 MB
% 13.23/3.04 % (3874467)Instructions burned: 181 (million)
% 13.23/3.04 % (3874465)lrs+10_1_sil=8000:sp=occurrence:random_seed=2303890207:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 13.23/3.04 % (3874468)dis-21_1_sil=8000:lcm=predicate:random_seed=1627109821:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 13.23/3.04 % (3874464)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=2373427796:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 13.23/3.04 % (3874465)Instruction limit reached!
% 13.23/3.04 % (3874465)------------------------------
% 13.23/3.04 % (3874465)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.23/3.04 % (3874465)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.23/3.04 % (3874465)CaDiCaL version: 2.1.3
% 13.23/3.04 % (3874465)Termination reason: Instruction limit
% 13.23/3.04 % (3874465)Termination phase: Saturation
% 13.23/3.04 % (3874465)Time elapsed: 0.093 s
% 13.23/3.04 % (3874465)Peak memory usage: 89 MB
% 13.23/3.04 % (3874465)Instructions burned: 107 (million)
% 13.23/3.04 % (3874468)Instruction limit reached!
% 13.23/3.04 % (3874468)------------------------------
% 13.23/3.04 % (3874468)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.23/3.04 % (3874468)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.23/3.04 % (3874468)CaDiCaL version: 2.1.3
% 13.23/3.04 % (3874468)Termination reason: Instruction limit
% 13.23/3.04 % (3874468)Termination phase: Saturation
% 13.23/3.04 % (3874468)Time elapsed: 0.110 s
% 13.23/3.04 % (3874468)Peak memory usage: 88 MB
% 13.23/3.04 % (3874468)Instructions burned: 118 (million)
% 13.23/3.04 % (3874466)------------------------------
% 13.23/3.04 % (3874466)------------------------------
% 13.23/3.04 % (3874473)dis+1010_3_sil=8000:plsq=on:drc=off:fde=none:plsqc=1:bsd=on:plsqr=7,2:sos=on:spb=goal_then_units:random_seed=574631148:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 13.23/3.04 % (3874473)Refutation not found, incomplete strategy
% 13.23/3.04 % (3874473)------------------------------
% 13.23/3.04 % (3874473)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.23/3.04 % (3874473)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.23/3.04 % (3874473)CaDiCaL version: 2.1.3
% 13.23/3.04 % (3874473)Termination reason: Refutation not found, incomplete strategy
% 13.23/3.04 % (3874473)Time elapsed: 0.003 s
% 13.23/3.04 % (3874473)Peak memory usage: 88 MB
% 19.22/3.73 % (3874473)Instructions burned: 1 (million)
% 19.22/3.73 % (3874478)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=813471239:st=4:i=219:sd=3:ss=axioms_2996 on theBenchmark for (2996ds/219Mi)
% 19.22/3.73 % (3874478)Refutation not found, incomplete strategy
% 19.22/3.73 % (3874478)------------------------------
% 19.22/3.73 % (3874478)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.22/3.73 % (3874478)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.22/3.73 % (3874478)CaDiCaL version: 2.1.3
% 19.22/3.73 % (3874478)Termination reason: Refutation not found, incomplete strategy
% 19.22/3.73 % (3874478)Time elapsed: 0.002 s
% 19.22/3.73 % (3874478)Peak memory usage: 88 MB
% 19.22/3.73 % (3874478)Instructions burned: 3 (million)
% 19.22/3.73 % (3874477)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=1474082681:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2996 on theBenchmark for (2996ds/189Mi)
% 19.22/3.73 % (3874477)Refutation not found, incomplete strategy
% 19.22/3.73 % (3874477)------------------------------
% 19.22/3.73 % (3874477)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.22/3.73 % (3874477)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.22/3.73 % (3874477)CaDiCaL version: 2.1.3
% 19.22/3.73 % (3874477)Termination reason: Refutation not found, incomplete strategy
% 19.22/3.73 % (3874477)Time elapsed: 0.009 s
% 19.22/3.73 % (3874477)Peak memory usage: 88 MB
% 19.22/3.73 % (3874477)Instructions burned: 8 (million)
% 19.22/3.73 % (3874479)lrs+10_64_to=lpo:sil=8000:random_seed=961060887:i=126:bd=preordered_2995 on theBenchmark for (2995ds/126Mi)
% 19.22/3.73 % (3874479)Instruction limit reached!
% 19.22/3.73 % (3874479)------------------------------
% 19.22/3.73 % (3874479)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.22/3.73 % (3874479)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.22/3.73 % (3874479)CaDiCaL version: 2.1.3
% 19.22/3.73 % (3874479)Termination reason: Instruction limit
% 19.22/3.73 % (3874479)Termination phase: Saturation
% 19.22/3.73 % (3874479)Time elapsed: 0.106 s
% 19.22/3.73 % (3874479)Peak memory usage: 88 MB
% 19.22/3.73 % (3874479)Instructions burned: 127 (million)
% 19.22/3.73 % (3874478)------------------------------
% 19.22/3.73 % (3874478)------------------------------
% 19.22/3.73 % (3874473)------------------------------
% 19.22/3.73 % (3874473)------------------------------
% 19.22/3.73 % (3874477)------------------------------
% 19.22/3.73 % (3874477)------------------------------
% 19.22/3.73 % (3874485)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=2945210557:i=157:gtg=all_2991 on theBenchmark for (2991ds/157Mi)
% 19.22/3.73 % (3874484)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=3845817421:avsq=on:i=194:fgj=on:bd=preordered_2991 on theBenchmark for (2991ds/194Mi)
% 19.22/3.73 % (3874485)Instruction limit reached!
% 19.22/3.73 % (3874485)------------------------------
% 19.22/3.73 % (3874485)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.22/3.73 % (3874485)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.22/3.73 % (3874485)CaDiCaL version: 2.1.3
% 19.22/3.73 % (3874485)Termination reason: Instruction limit
% 19.22/3.73 % (3874485)Termination phase: Saturation
% 19.22/3.73 % (3874485)Time elapsed: 0.090 s
% 19.22/3.73 % (3874485)Peak memory usage: 90 MB
% 19.22/3.73 % (3874485)Instructions burned: 157 (million)
% 19.22/3.73 % (3874463)Refutation not found, incomplete strategy
% 19.22/3.73 % (3874463)------------------------------
% 19.22/3.73 % (3874463)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.22/3.73 % (3874463)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.22/3.73 % (3874463)CaDiCaL version: 2.1.3
% 19.22/3.73 % (3874463)Termination reason: Refutation not found, incomplete strategy
% 19.22/3.73 % (3874463)Time elapsed: 0.914 s
% 19.22/3.73 % (3874463)Peak memory usage: 128 MB
% 19.22/3.73 % (3874463)Instructions burned: 898 (million)
% 19.22/3.73 % (3874486)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=1187578363:i=3394:sd=4:ss=included:sgt=64_2990 on theBenchmark for (2990ds/3394Mi)
% 19.22/3.73 % (3874484)Instruction limit reached!
% 19.22/3.73 % (3874484)------------------------------
% 19.22/3.73 % (3874484)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.22/3.73 % (3874484)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.22/3.73 % (3874484)CaDiCaL version: 2.1.3
% 19.22/3.73 % (3874484)Termination reason: Instruction limit
% 19.22/3.73 % (3874484)Termination phase: Saturation
% 19.22/3.73 % (3874484)Time elapsed: 0.188 s
% 19.22/3.73 % (3874484)Peak memory usage: 90 MB
% 19.22/3.73 % (3874484)Instructions burned: 195 (million)
% 19.22/3.73 % (3874487)lrs+1011_5_to=lpo:sil=8000:tgt=full:plsq=on:prc=on:drc=off:plsqr=31,4:sp=occurrence:urr=on:nwc=0.8:s2agt=16:br=off:random_seed=3109170259:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2989 on theBenchmark for (2989ds/106Mi)
% 19.22/3.73 % (3874487)Refutation not found, incomplete strategy
% 19.22/3.73 % (3874487)------------------------------
% 19.22/3.73 % (3874487)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.22/3.73 % (3874487)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.22/3.73 % (3874487)CaDiCaL version: 2.1.3
% 19.22/3.73 % (3874487)Termination reason: Refutation not found, incomplete strategy
% 19.22/3.73 % (3874487)Time elapsed: 0.009 s
% 19.22/3.73 % (3874487)Peak memory usage: 88 MB
% 19.22/3.73 % (3874487)Instructions burned: 8 (million)
% 19.22/3.73 % (3874490)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=516636280:i=107_2988 on theBenchmark for (2988ds/107Mi)
% 19.22/3.73 % (3874490)Instruction limit reached!
% 19.22/3.73 % (3874490)------------------------------
% 19.22/3.73 % (3874490)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.22/3.73 % (3874490)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.22/3.73 % (3874490)CaDiCaL version: 2.1.3
% 19.22/3.73 % (3874490)Termination reason: Instruction limit
% 19.22/3.73 % (3874490)Termination phase: Saturation
% 19.22/3.73 % (3874490)Time elapsed: 0.046 s
% 19.22/3.73 % (3874490)Peak memory usage: 88 MB
% 19.22/3.73 % (3874490)Instructions burned: 110 (million)
% 19.22/3.73 % (3874492)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=2790173552:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2987 on theBenchmark for (2987ds/242Mi)
% 19.22/3.73 % (3874463)------------------------------
% 19.22/3.73 % (3874463)------------------------------
% 19.22/3.73 % (3874495)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=3351004638:cond=fast:i=5208:av=off_2985 on theBenchmark for (2985ds/5208Mi)
% 19.22/3.73 % (3874487)------------------------------
% 19.22/3.73 % (3874487)------------------------------
% 19.22/3.73 % (3874492)Instruction limit reached!
% 19.22/3.73 % (3874492)------------------------------
% 19.22/3.73 % (3874492)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.22/3.73 % (3874492)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.22/3.73 % (3874492)CaDiCaL version: 2.1.3
% 19.22/3.73 % (3874492)Termination reason: Instruction limit
% 19.22/3.73 % (3874492)Termination phase: Saturation
% 19.22/3.73 % (3874492)Time elapsed: 0.185 s
% 19.22/3.73 % (3874492)Peak memory usage: 89 MB
% 19.22/3.73 % (3874492)Instructions burned: 242 (million)
% 19.22/3.73 % (3874497)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=3064746081:i=134:sd=2:doe=on:ss=axioms:sgt=14_2984 on theBenchmark for (2984ds/134Mi)
% 19.22/3.73 % (3874497)Refutation not found, incomplete strategy
% 19.22/3.73 % (3874497)------------------------------
% 19.22/3.73 % (3874497)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.22/3.73 % (3874497)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.22/3.73 % (3874497)CaDiCaL version: 2.1.3
% 19.22/3.73 % (3874497)Termination reason: Refutation not found, incomplete strategy
% 19.22/3.73 % (3874497)Time elapsed: 0.010 s
% 19.22/3.73 % (3874497)Peak memory usage: 88 MB
% 19.22/3.73 % (3874497)Instructions burned: 9 (million)
% 19.22/3.73 % (3874499)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=3653274026:i=499:bd=all_2983 on theBenchmark for (2983ds/499Mi)
% 19.22/3.73 % (3874500)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=3708563686:i=191:fgj=on:bd=all_2982 on theBenchmark for (2982ds/191Mi)
% 19.22/3.73 % (3874500)Instruction limit reached!
% 19.22/3.73 % (3874500)------------------------------
% 19.22/3.73 % (3874500)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.22/3.73 % (3874500)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.22/3.73 % (3874500)CaDiCaL version: 2.1.3
% 19.22/3.73 % (3874500)Termination reason: Instruction limit
% 19.22/3.73 % (3874500)Termination phase: Saturation
% 19.22/3.73 % (3874500)Time elapsed: 0.161 s
% 19.22/3.73 % (3874500)Peak memory usage: 89 MB
% 19.22/3.73 % (3874500)Instructions burned: 191 (million)
% 19.22/3.73 % (3874497)------------------------------
% 19.22/3.73 % (3874497)------------------------------
% 19.22/3.73 % (3874499)Instruction limit reached!
% 19.22/3.73 % (3874499)------------------------------
% 19.22/3.73 % (3874499)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.22/3.73 % (3874499)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.22/3.73 % (3874499)CaDiCaL version: 2.1.3
% 19.22/3.73 % (3874499)Termination reason: Instruction limit
% 19.22/3.73 % (3874499)Termination phase: Saturation
% 19.22/3.73 % (3874499)Time elapsed: 0.453 s
% 19.22/3.73 % (3874499)Peak memory usage: 93 MB
% 19.22/3.73 % (3874499)Instructions burned: 500 (million)
% 19.22/3.73 % (3874505)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=1966831891:cond=on:i=156:bs=on:gtg=exists_all:er=known_2977 on theBenchmark for (2977ds/156Mi)
% 19.22/3.73 % (3874504)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=1600450230:i=264:kws=precedence:fsr=off_2978 on theBenchmark for (2978ds/264Mi)
% 19.22/3.73 % (3874504)First to succeed.
% 19.22/3.73 % (3874504)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3874457"
% 19.22/3.73 % (3874505)Instruction limit reached!
% 19.22/3.73 % (3874505)------------------------------
% 19.22/3.73 % (3874505)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.22/3.73 % (3874505)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.22/3.73 % (3874505)CaDiCaL version: 2.1.3
% 19.22/3.73 % (3874505)Termination reason: Instruction limit
% 19.22/3.73 % (3874505)Termination phase: Saturation
% 19.22/3.73 % (3874505)Time elapsed: 0.164 s
% 19.22/3.73 % (3874505)Peak memory usage: 89 MB
% 19.22/3.73 % (3874505)Instructions burned: 156 (million)
% 19.22/3.73 % (3874508)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=reverse_frequency:spb=units:lcm=predicate:urr=on:s2agt=8:updr=off:random_seed=2275908328:i=3256:kws=precedence:bd=preordered:av=off_2975 on theBenchmark for (2975ds/3256Mi)
% 19.22/3.73 % (3874509)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=239603396:i=537:av=off:ss=included_2974 on theBenchmark for (2974ds/537Mi)
% 19.22/3.73 % (3874509)Refutation not found, incomplete strategy
% 19.22/3.73 % (3874509)------------------------------
% 19.22/3.73 % (3874509)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.22/3.73 % (3874509)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.22/3.73 % (3874509)CaDiCaL version: 2.1.3
% 19.22/3.73 % (3874509)Termination reason: Refutation not found, incomplete strategy
% 19.22/3.73 % (3874509)Time elapsed: 0.002 s
% 19.22/3.73 % (3874509)Peak memory usage: 87 MB
% 19.22/3.73 % SZS status Satisfiable for theBenchmark
% 19.22/3.73 % SZS output start Saturation.
% See solution above
% 20.85/3.97 % SZS output start Definitions and Model Updates.
% 20.85/3.97 % SZS output end Definitions and Model Updates.
% 20.85/3.97 % (3874504)------------------------------
% 20.85/3.97 % (3874504)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.85/3.97 % (3874504)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.85/3.97 % (3874504)CaDiCaL version: 2.1.3
% 20.85/3.97 % (3874504)Termination reason: Satisfiable
% 20.85/3.97 % (3874504)Time elapsed: 0.020 s
% 20.85/3.97 % (3874504)Peak memory usage: 88 MB
% 20.85/3.97 % (3874504)Instructions burned: 17 (million)
% 20.85/3.97 % (3874504)------------------------------
% 20.85/3.97 % (3874504)------------------------------
% 20.85/3.97 % (3874457)Success in time 2.846 s
% 20.85/3.97 % Vampire exiting
%------------------------------------------------------------------------------