%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SEU323-10 : TPTP v9.3.1. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n020.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 : Fri Sep 25 02:51:43 PM UTC 2026
% Result : Unsatisfiable 16.34s 2.52s
% Output : CNFRefutation 16.34s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 13
% Syntax : Number of clauses : 63 ( 63 unt; 0 nHn; 49 RR)
% Number of literals : 63 ( 62 equ; 4 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 10 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 17 ( 17 usr; 5 con; 0-4 aty)
% Number of variables : 32 ( 4 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t24,axiom,
sFlat0 = interior(sK2_t51_tops_1_A,sK1_t51_tops_1_B),
introduced(definition) ).
cnf(t102,plain,
interior(sK2_t51_tops_1_A,sK1_t51_tops_1_B) = sFlat0,
inference(orient,[status(thm)],[t24]) ).
cnf(t25,axiom,
sFlat1 = open_subset(interior(sK2_t51_tops_1_A,sK1_t51_tops_1_B),sK2_t51_tops_1_A),
introduced(definition) ).
cnf(t683,plain,
sFlat1 = open_subset(sFlat0,sK2_t51_tops_1_A),
inference(step,[status(thm)],[t25,t102]) ).
cnf(t106,plain,
open_subset(sFlat0,sK2_t51_tops_1_A) = sFlat1,
inference(orient,[status(thm)],[t683]) ).
cnf(t22,axiom,
ifeq(element(X1,powerset(the_carrier(X2))),true,ifeq(closed_subset(X1,X2),true,ifeq(topological_space(X2),true,ifeq(top_str(X2),true,open_subset(subset_complement(the_carrier(X2),X1),X2),true),true),true),true) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t34,plain,
ifeq(element(X1,powerset(the_carrier(X2))),true,ifeq(closed_subset(X1,X2),true,ifeq(topological_space(X2),true,ifeq(top_str(X2),true,open_subset(subset_complement(the_carrier(X2),X1),X2),true),true),true),true) = true,
inference(orient,[status(thm)],[t22]) ).
cnf(t19,axiom,
ifeq(element(X1,powerset(the_carrier(X2))),true,ifeq(top_str(X2),true,element(topstr_closure(X2,X1),powerset(the_carrier(X2))),true),true) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t32,plain,
ifeq(element(X1,powerset(the_carrier(X2))),true,ifeq(top_str(X2),true,element(topstr_closure(X2,X1),powerset(the_carrier(X2))),true),true) = true,
inference(orient,[status(thm)],[t19]) ).
cnf(t13,axiom,
ifeq(element(X1,powerset(X2)),true,element(subset_complement(X2,X1),powerset(X2)),true) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t29,plain,
ifeq(element(X1,powerset(X2)),true,element(subset_complement(X2,X1),powerset(X2)),true) = true,
inference(orient,[status(thm)],[t13]) ).
cnf(t6,axiom,
element(sK1_t51_tops_1_B,powerset(the_carrier(sK2_t51_tops_1_A))) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t42,plain,
element(sK1_t51_tops_1_B,powerset(the_carrier(sK2_t51_tops_1_A))) = true,
inference(orient,[status(thm)],[t6]) ).
cnf(t46,plain,
true = ifeq(true,true,element(subset_complement(the_carrier(sK2_t51_tops_1_A),sK1_t51_tops_1_B),powerset(the_carrier(sK2_t51_tops_1_A))),true),
inference(cp,[status(thm)],[t29,t42]) ).
cnf(t7,axiom,
ifeq(X1,X1,X2,X3) = X2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t26,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t7]) ).
cnf(t735,plain,
true = element(subset_complement(the_carrier(sK2_t51_tops_1_A),sK1_t51_tops_1_B),powerset(the_carrier(sK2_t51_tops_1_A))),
inference(step,[status(thm)],[t46,t26]) ).
cnf(t219,plain,
element(subset_complement(the_carrier(sK2_t51_tops_1_A),sK1_t51_tops_1_B),powerset(the_carrier(sK2_t51_tops_1_A))) = true,
inference(orient,[status(thm)],[t735]) ).
cnf(t224,plain,
true = ifeq(true,true,ifeq(top_str(sK2_t51_tops_1_A),true,element(topstr_closure(sK2_t51_tops_1_A,subset_complement(the_carrier(sK2_t51_tops_1_A),sK1_t51_tops_1_B)),powerset(the_carrier(sK2_t51_tops_1_A))),true),true),
inference(cp,[status(thm)],[t32,t219]) ).
cnf(t934,plain,
true = ifeq(top_str(sK2_t51_tops_1_A),true,element(topstr_closure(sK2_t51_tops_1_A,subset_complement(the_carrier(sK2_t51_tops_1_A),sK1_t51_tops_1_B)),powerset(the_carrier(sK2_t51_tops_1_A))),true),
inference(step,[status(thm)],[t224,t26]) ).
cnf(t1,axiom,
top_str(sK2_t51_tops_1_A) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t62,plain,
top_str(sK2_t51_tops_1_A) = true,
inference(orient,[status(thm)],[t1]) ).
cnf(t935,plain,
true = ifeq(true,true,element(topstr_closure(sK2_t51_tops_1_A,subset_complement(the_carrier(sK2_t51_tops_1_A),sK1_t51_tops_1_B)),powerset(the_carrier(sK2_t51_tops_1_A))),true),
inference(step,[status(thm)],[t934,t62]) ).
cnf(t936,plain,
true = element(topstr_closure(sK2_t51_tops_1_A,subset_complement(the_carrier(sK2_t51_tops_1_A),sK1_t51_tops_1_B)),powerset(the_carrier(sK2_t51_tops_1_A))),
inference(step,[status(thm)],[t935,t26]) ).
cnf(t489,plain,
element(topstr_closure(sK2_t51_tops_1_A,subset_complement(the_carrier(sK2_t51_tops_1_A),sK1_t51_tops_1_B)),powerset(the_carrier(sK2_t51_tops_1_A))) = true,
inference(orient,[status(thm)],[t936]) ).
cnf(t497,plain,
true = ifeq(true,true,ifeq(closed_subset(topstr_closure(sK2_t51_tops_1_A,subset_complement(the_carrier(sK2_t51_tops_1_A),sK1_t51_tops_1_B)),sK2_t51_tops_1_A),true,ifeq(topological_space(sK2_t51_tops_1_A),true,ifeq(top_str(sK2_t51_tops_1_A),true,open_subset(subset_complement(the_carrier(sK2_t51_tops_1_A),topstr_closure(sK2_t51_tops_1_A,subset_complement(the_carrier(sK2_t51_tops_1_A),sK1_t51_tops_1_B))),sK2_t51_tops_1_A),true),true),true),true),
inference(cp,[status(thm)],[t34,t489]) ).
cnf(t937,plain,
true = ifeq(closed_subset(topstr_closure(sK2_t51_tops_1_A,subset_complement(the_carrier(sK2_t51_tops_1_A),sK1_t51_tops_1_B)),sK2_t51_tops_1_A),true,ifeq(topological_space(sK2_t51_tops_1_A),true,ifeq(top_str(sK2_t51_tops_1_A),true,open_subset(subset_complement(the_carrier(sK2_t51_tops_1_A),topstr_closure(sK2_t51_tops_1_A,subset_complement(the_carrier(sK2_t51_tops_1_A),sK1_t51_tops_1_B))),sK2_t51_tops_1_A),true),true),true),
inference(step,[status(thm)],[t497,t26]) ).
cnf(t20,axiom,
ifeq(element(X1,powerset(the_carrier(X2))),true,ifeq(topological_space(X2),true,ifeq(top_str(X2),true,closed_subset(topstr_closure(X2,X1),X2),true),true),true) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t33,plain,
ifeq(element(X1,powerset(the_carrier(X2))),true,ifeq(topological_space(X2),true,ifeq(top_str(X2),true,closed_subset(topstr_closure(X2,X1),X2),true),true),true) = true,
inference(orient,[status(thm)],[t20]) ).
cnf(t223,plain,
true = ifeq(true,true,ifeq(topological_space(sK2_t51_tops_1_A),true,ifeq(top_str(sK2_t51_tops_1_A),true,closed_subset(topstr_closure(sK2_t51_tops_1_A,subset_complement(the_carrier(sK2_t51_tops_1_A),sK1_t51_tops_1_B)),sK2_t51_tops_1_A),true),true),true),
inference(cp,[status(thm)],[t33,t219]) ).
cnf(t790,plain,
true = ifeq(topological_space(sK2_t51_tops_1_A),true,ifeq(top_str(sK2_t51_tops_1_A),true,closed_subset(topstr_closure(sK2_t51_tops_1_A,subset_complement(the_carrier(sK2_t51_tops_1_A),sK1_t51_tops_1_B)),sK2_t51_tops_1_A),true),true),
inference(step,[status(thm)],[t223,t26]) ).
cnf(t3,axiom,
topological_space(sK2_t51_tops_1_A) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t84,plain,
topological_space(sK2_t51_tops_1_A) = true,
inference(orient,[status(thm)],[t3]) ).
cnf(t791,plain,
true = ifeq(true,true,ifeq(top_str(sK2_t51_tops_1_A),true,closed_subset(topstr_closure(sK2_t51_tops_1_A,subset_complement(the_carrier(sK2_t51_tops_1_A),sK1_t51_tops_1_B)),sK2_t51_tops_1_A),true),true),
inference(step,[status(thm)],[t790,t84]) ).
cnf(t792,plain,
true = ifeq(top_str(sK2_t51_tops_1_A),true,closed_subset(topstr_closure(sK2_t51_tops_1_A,subset_complement(the_carrier(sK2_t51_tops_1_A),sK1_t51_tops_1_B)),sK2_t51_tops_1_A),true),
inference(step,[status(thm)],[t791,t26]) ).
cnf(t793,plain,
true = ifeq(true,true,closed_subset(topstr_closure(sK2_t51_tops_1_A,subset_complement(the_carrier(sK2_t51_tops_1_A),sK1_t51_tops_1_B)),sK2_t51_tops_1_A),true),
inference(step,[status(thm)],[t792,t62]) ).
cnf(t794,plain,
true = closed_subset(topstr_closure(sK2_t51_tops_1_A,subset_complement(the_carrier(sK2_t51_tops_1_A),sK1_t51_tops_1_B)),sK2_t51_tops_1_A),
inference(step,[status(thm)],[t793,t26]) ).
cnf(t314,plain,
closed_subset(topstr_closure(sK2_t51_tops_1_A,subset_complement(the_carrier(sK2_t51_tops_1_A),sK1_t51_tops_1_B)),sK2_t51_tops_1_A) = true,
inference(orient,[status(thm)],[t794]) ).
cnf(t938,plain,
true = ifeq(true,true,ifeq(topological_space(sK2_t51_tops_1_A),true,ifeq(top_str(sK2_t51_tops_1_A),true,open_subset(subset_complement(the_carrier(sK2_t51_tops_1_A),topstr_closure(sK2_t51_tops_1_A,subset_complement(the_carrier(sK2_t51_tops_1_A),sK1_t51_tops_1_B))),sK2_t51_tops_1_A),true),true),true),
inference(step,[status(thm)],[t937,t314]) ).
cnf(t939,plain,
true = ifeq(topological_space(sK2_t51_tops_1_A),true,ifeq(top_str(sK2_t51_tops_1_A),true,open_subset(subset_complement(the_carrier(sK2_t51_tops_1_A),topstr_closure(sK2_t51_tops_1_A,subset_complement(the_carrier(sK2_t51_tops_1_A),sK1_t51_tops_1_B))),sK2_t51_tops_1_A),true),true),
inference(step,[status(thm)],[t938,t26]) ).
cnf(t940,plain,
true = ifeq(true,true,ifeq(top_str(sK2_t51_tops_1_A),true,open_subset(subset_complement(the_carrier(sK2_t51_tops_1_A),topstr_closure(sK2_t51_tops_1_A,subset_complement(the_carrier(sK2_t51_tops_1_A),sK1_t51_tops_1_B))),sK2_t51_tops_1_A),true),true),
inference(step,[status(thm)],[t939,t84]) ).
cnf(t941,plain,
true = ifeq(top_str(sK2_t51_tops_1_A),true,open_subset(subset_complement(the_carrier(sK2_t51_tops_1_A),topstr_closure(sK2_t51_tops_1_A,subset_complement(the_carrier(sK2_t51_tops_1_A),sK1_t51_tops_1_B))),sK2_t51_tops_1_A),true),
inference(step,[status(thm)],[t940,t26]) ).
cnf(t942,plain,
true = ifeq(true,true,open_subset(subset_complement(the_carrier(sK2_t51_tops_1_A),topstr_closure(sK2_t51_tops_1_A,subset_complement(the_carrier(sK2_t51_tops_1_A),sK1_t51_tops_1_B))),sK2_t51_tops_1_A),true),
inference(step,[status(thm)],[t941,t62]) ).
cnf(t943,plain,
true = open_subset(subset_complement(the_carrier(sK2_t51_tops_1_A),topstr_closure(sK2_t51_tops_1_A,subset_complement(the_carrier(sK2_t51_tops_1_A),sK1_t51_tops_1_B))),sK2_t51_tops_1_A),
inference(step,[status(thm)],[t942,t26]) ).
cnf(t21,axiom,
ifeq2(element(X1,powerset(the_carrier(X2))),true,ifeq2(top_str(X2),true,subset_complement(the_carrier(X2),topstr_closure(X2,subset_complement(the_carrier(X2),X1))),interior(X2,X1)),interior(X2,X1)) = interior(X2,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t97,plain,
ifeq2(element(X1,powerset(the_carrier(X2))),true,ifeq2(top_str(X2),true,subset_complement(the_carrier(X2),topstr_closure(X2,subset_complement(the_carrier(X2),X1))),interior(X2,X1)),interior(X2,X1)) = interior(X2,X1),
inference(orient,[status(thm)],[t21]) ).
cnf(t104,plain,
interior(sK2_t51_tops_1_A,sK1_t51_tops_1_B) = ifeq2(element(sK1_t51_tops_1_B,powerset(the_carrier(sK2_t51_tops_1_A))),true,ifeq2(top_str(sK2_t51_tops_1_A),true,subset_complement(the_carrier(sK2_t51_tops_1_A),topstr_closure(sK2_t51_tops_1_A,subset_complement(the_carrier(sK2_t51_tops_1_A),sK1_t51_tops_1_B))),sFlat0),interior(sK2_t51_tops_1_A,sK1_t51_tops_1_B)),
inference(cp,[status(thm)],[t97,t102]) ).
cnf(t832,plain,
sFlat0 = ifeq2(element(sK1_t51_tops_1_B,powerset(the_carrier(sK2_t51_tops_1_A))),true,ifeq2(top_str(sK2_t51_tops_1_A),true,subset_complement(the_carrier(sK2_t51_tops_1_A),topstr_closure(sK2_t51_tops_1_A,subset_complement(the_carrier(sK2_t51_tops_1_A),sK1_t51_tops_1_B))),sFlat0),interior(sK2_t51_tops_1_A,sK1_t51_tops_1_B)),
inference(step,[status(thm)],[t104,t102]) ).
cnf(t833,plain,
sFlat0 = ifeq2(true,true,ifeq2(top_str(sK2_t51_tops_1_A),true,subset_complement(the_carrier(sK2_t51_tops_1_A),topstr_closure(sK2_t51_tops_1_A,subset_complement(the_carrier(sK2_t51_tops_1_A),sK1_t51_tops_1_B))),sFlat0),interior(sK2_t51_tops_1_A,sK1_t51_tops_1_B)),
inference(step,[status(thm)],[t832,t42]) ).
cnf(t8,axiom,
ifeq2(X1,X1,X2,X3) = X2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t27,plain,
ifeq2(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t8]) ).
cnf(t834,plain,
sFlat0 = ifeq2(top_str(sK2_t51_tops_1_A),true,subset_complement(the_carrier(sK2_t51_tops_1_A),topstr_closure(sK2_t51_tops_1_A,subset_complement(the_carrier(sK2_t51_tops_1_A),sK1_t51_tops_1_B))),sFlat0),
inference(step,[status(thm)],[t833,t27]) ).
cnf(t835,plain,
sFlat0 = ifeq2(true,true,subset_complement(the_carrier(sK2_t51_tops_1_A),topstr_closure(sK2_t51_tops_1_A,subset_complement(the_carrier(sK2_t51_tops_1_A),sK1_t51_tops_1_B))),sFlat0),
inference(step,[status(thm)],[t834,t62]) ).
cnf(t836,plain,
sFlat0 = subset_complement(the_carrier(sK2_t51_tops_1_A),topstr_closure(sK2_t51_tops_1_A,subset_complement(the_carrier(sK2_t51_tops_1_A),sK1_t51_tops_1_B))),
inference(step,[status(thm)],[t835,t27]) ).
cnf(t344,plain,
subset_complement(the_carrier(sK2_t51_tops_1_A),topstr_closure(sK2_t51_tops_1_A,subset_complement(the_carrier(sK2_t51_tops_1_A),sK1_t51_tops_1_B))) = sFlat0,
inference(orient,[status(thm)],[t836]) ).
cnf(t944,plain,
true = open_subset(sFlat0,sK2_t51_tops_1_A),
inference(step,[status(thm)],[t943,t344]) ).
cnf(t945,plain,
true = sFlat1,
inference(step,[status(thm)],[t944,t106]) ).
cnf(t499,plain,
true = sFlat1,
inference(orient,[status(thm)],[t945]) ).
cnf(goal_0,negated_conjecture,
open_subset(interior(sK2_t51_tops_1_A,sK1_t51_tops_1_B),sK2_t51_tops_1_A) != true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
open_subset(sFlat0,sK2_t51_tops_1_A) != true,
inference(rw,[status(thm)],[goal_0,t102]) ).
cnf(g0_1,plain,
sFlat1 != true,
inference(rw,[status(thm)],[g0_0,t106]) ).
cnf(g0_2,plain,
sFlat1 != sFlat1,
inference(rw,[status(thm)],[g0_1,t499]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_2]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU323-10 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.11/0.36 % Computer : n020.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Thu Sep 24 13:42:49 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 16.34/2.52 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 16.34/2.52 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------