%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SEU310+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n003.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:41 PM UTC 2026
% Result : Theorem 27.88s 4.46s
% Output : Proof 27.88s
% Verified :
% SZS Type : Refutation
% Derivation depth : 30
% Number of leaves : 2
% Syntax : Number of formulae : 118 ( 10 unt; 0 def)
% Number of atoms : 466 ( 138 equ)
% Maximal formula atoms : 16 ( 3 avg)
% Number of connectives : 569 ( 221 ~; 301 |; 39 &)
% ( 3 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 5 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 2 con; 0-3 aty)
% Number of variables : 159 ( 0 sgn 22 !; 12 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f35,axiom,
! [A,B] :
( ( element(B,powerset(powerset(the_carrier(A))))
& top_str(A)
& topological_space(A) )
=> ( ! [C,D,E] :
( ( in(set_difference(cast_as_carrier_subset(A),E),B)
& C = E
& in(set_difference(cast_as_carrier_subset(A),D),B)
& C = D )
=> D = E )
=> ? [C] :
! [D] :
( in(D,C)
<=> ? [E] :
( in(set_difference(cast_as_carrier_subset(A),D),B)
& E = D
& in(E,powerset(the_carrier(A))) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',s1_tarski__e2_37_1_1__pre_topc__1) ).
fof(f35_nnf,plain,
! [A,B] :
( ? [C] :
! [D] :
( ( ! [E] :
( ~ in(set_difference(cast_as_carrier_subset(A),D),B)
| E != D
| ~ in(E,powerset(the_carrier(A))) )
| in(D,C) )
& ( ? [E] :
( in(set_difference(cast_as_carrier_subset(A),D),B)
& E = D
& in(E,powerset(the_carrier(A))) )
| ~ in(D,C) ) )
| ? [C,D,E] :
( D != E
& in(set_difference(cast_as_carrier_subset(A),E),B)
& C = E
& in(set_difference(cast_as_carrier_subset(A),D),B)
& C = D )
| ~ element(B,powerset(powerset(the_carrier(A))))
| ~ top_str(A)
| ~ topological_space(A) ),
inference(nnf_transformation,[status(thm)],[f35]) ).
fof(f35_sk,plain,
! [A,B,D,E] :
( ( ( ~ in(set_difference(cast_as_carrier_subset(A),D),B)
| E != D
| ~ in(E,powerset(the_carrier(A)))
| in(D,sk10(A,B)) )
& ( ( in(set_difference(cast_as_carrier_subset(A),D),B)
& sk11(A,B,D) = D
& in(sk11(A,B,D),powerset(the_carrier(A))) )
| ~ in(D,sk10(A,B)) ) )
| ( sk8(A,B) != sk9(A,B)
& in(set_difference(cast_as_carrier_subset(A),sk9(A,B)),B)
& sk7(A,B) = sk9(A,B)
& in(set_difference(cast_as_carrier_subset(A),sk8(A,B)),B)
& sk7(A,B) = sk8(A,B) )
| ~ element(B,powerset(powerset(the_carrier(A))))
| ~ top_str(A)
| ~ topological_space(A) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk7,sk8,sk9,sk10,sk11])],[f35_nnf]) ).
cnf(c88,plain,
( ~ in(set_difference(cast_as_carrier_subset(X0),X3),X1)
| X4 != X3
| ~ in(X4,powerset(the_carrier(X0)))
| in(X3,sk10(X0,X1))
| sk7(X0,X1) = sk8(X0,X1)
| ~ element(X1,powerset(powerset(the_carrier(X0))))
| ~ top_str(X0)
| ~ topological_space(X0) ),
inference(cnf_transformation,[status(esa)],[f35_sk]) ).
fof(f0,conjecture,
! [A,B] :
( ( element(B,powerset(powerset(the_carrier(A))))
& top_str(A)
& topological_space(A) )
=> ? [C] :
! [D] :
( in(D,C)
<=> ( in(set_difference(cast_as_carrier_subset(A),D),B)
& in(D,powerset(the_carrier(A))) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',s1_xboole_0__e2_37_1_1__pre_topc__1) ).
fof(f0_neg,negated_conjecture,
~ ! [A,B] :
( ( element(B,powerset(powerset(the_carrier(A))))
& top_str(A)
& topological_space(A) )
=> ? [C] :
! [D] :
( in(D,C)
<=> ( in(set_difference(cast_as_carrier_subset(A),D),B)
& in(D,powerset(the_carrier(A))) ) ) ),
inference(negated_conjecture,[status(cth)],[f0]) ).
fof(f0_nnf,plain,
? [A,B] :
( ! [C] :
? [D] :
( ( in(set_difference(cast_as_carrier_subset(A),D),B)
& in(D,powerset(the_carrier(A)))
& ~ in(D,C) )
| ( ( ~ in(set_difference(cast_as_carrier_subset(A),D),B)
| ~ in(D,powerset(the_carrier(A))) )
& in(D,C) ) )
& element(B,powerset(powerset(the_carrier(A))))
& top_str(A)
& topological_space(A) ),
inference(nnf_transformation,[status(thm)],[f0_neg]) ).
fof(f0_sk,plain,
! [C] :
( ( ( in(set_difference(cast_as_carrier_subset(sk0),sk2(C)),sk1)
& in(sk2(C),powerset(the_carrier(sk0)))
& ~ in(sk2(C),C) )
| ( ( ~ in(set_difference(cast_as_carrier_subset(sk0),sk2(C)),sk1)
| ~ in(sk2(C),powerset(the_carrier(sk0))) )
& in(sk2(C),C) ) )
& element(sk1,powerset(powerset(the_carrier(sk0))))
& top_str(sk0)
& topological_space(sk0) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk0,sk1,sk2])],[f0_nnf]) ).
cnf(c0,plain,
topological_space(sk0),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p311,plain,
( ~ in(set_difference(cast_as_carrier_subset(sk0),X1),X0)
| X2 != X1
| ~ in(X2,powerset(the_carrier(sk0)))
| in(X1,sk10(sk0,X0))
| sk7(sk0,X0) = sk8(sk0,X0)
| ~ element(X0,powerset(powerset(the_carrier(sk0))))
| ~ top_str(sk0) ),
inference(resolution,[status(thm)],[c88,c0]) ).
cnf(p498,plain,
( ~ in(set_difference(cast_as_carrier_subset(sk0),X1),X0)
| ~ in(X1,powerset(the_carrier(sk0)))
| in(X1,sk10(sk0,X0))
| sk7(sk0,X0) = sk8(sk0,X0)
| ~ element(X0,powerset(powerset(the_carrier(sk0))))
| ~ top_str(sk0) ),
inference(equality_resolution,[status(thm)],[p311]) ).
cnf(c1,plain,
top_str(sk0),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p500,plain,
( ~ in(set_difference(cast_as_carrier_subset(sk0),X1),X0)
| ~ in(X1,powerset(the_carrier(sk0)))
| in(X1,sk10(sk0,X0))
| sk7(sk0,X0) = sk8(sk0,X0)
| ~ element(X0,powerset(powerset(the_carrier(sk0)))) ),
inference(resolution,[status(thm)],[p498,c1]) ).
cnf(c2,plain,
element(sk1,powerset(powerset(the_carrier(sk0)))),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p501,plain,
( ~ in(set_difference(cast_as_carrier_subset(sk0),X0),sk1)
| ~ in(X0,powerset(the_carrier(sk0)))
| in(X0,sk10(sk0,sk1))
| sk7(sk0,sk1) = sk8(sk0,sk1) ),
inference(resolution,[status(thm)],[p500,c2]) ).
cnf(c4,plain,
( in(sk2(X2),powerset(the_carrier(sk0)))
| in(sk2(X2),X2) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p504,plain,
( in(sk2(X0),X0)
| ~ in(set_difference(cast_as_carrier_subset(sk0),sk2(X0)),sk1)
| in(sk2(X0),sk10(sk0,sk1))
| sk7(sk0,sk1) = sk8(sk0,sk1) ),
inference(resolution,[status(thm)],[p501,c4]) ).
cnf(c5,plain,
( in(set_difference(cast_as_carrier_subset(sk0),sk2(X2)),sk1)
| in(sk2(X2),X2) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p510,plain,
( in(sk2(X0),X0)
| in(sk2(X0),X0)
| in(sk2(X0),sk10(sk0,sk1))
| sk7(sk0,sk1) = sk8(sk0,sk1) ),
inference(resolution,[status(thm)],[p504,c5]) ).
cnf(p517,plain,
( in(sk2(X0),X0)
| in(sk2(X0),sk10(sk0,sk1))
| sk7(sk0,sk1) = sk8(sk0,sk1) ),
inference(factoring,[status(thm)],[p510]) ).
cnf(p518,plain,
( in(sk2(sk10(sk0,sk1)),sk10(sk0,sk1))
| sk7(sk0,sk1) = sk8(sk0,sk1) ),
inference(factoring,[status(thm)],[p517]) ).
cnf(c86,plain,
( sk11(X0,X1,X3) = X3
| ~ in(X3,sk10(X0,X1))
| sk7(X0,X1) = sk8(X0,X1)
| ~ element(X1,powerset(powerset(the_carrier(X0))))
| ~ top_str(X0)
| ~ topological_space(X0) ),
inference(cnf_transformation,[status(esa)],[f35_sk]) ).
cnf(p295,plain,
( sk11(sk0,X0,X1) = X1
| ~ in(X1,sk10(sk0,X0))
| sk7(sk0,X0) = sk8(sk0,X0)
| ~ element(X0,powerset(powerset(the_carrier(sk0))))
| ~ top_str(sk0) ),
inference(resolution,[status(thm)],[c86,c0]) ).
cnf(p297,plain,
( sk11(sk0,X0,X1) = X1
| ~ in(X1,sk10(sk0,X0))
| sk7(sk0,X0) = sk8(sk0,X0)
| ~ element(X0,powerset(powerset(the_carrier(sk0)))) ),
inference(resolution,[status(thm)],[p295,c1]) ).
cnf(p299,plain,
( sk11(sk0,sk1,X0) = X0
| ~ in(X0,sk10(sk0,sk1))
| sk7(sk0,sk1) = sk8(sk0,sk1) ),
inference(resolution,[status(thm)],[p297,c2]) ).
cnf(p557,plain,
( sk11(sk0,sk1,sk2(sk10(sk0,sk1))) = sk2(sk10(sk0,sk1))
| sk7(sk0,sk1) = sk8(sk0,sk1)
| sk7(sk0,sk1) = sk8(sk0,sk1) ),
inference(resolution,[status(thm)],[p518,p299]) ).
cnf(p578,plain,
( sk11(sk0,sk1,sk2(sk10(sk0,sk1))) = sk2(sk10(sk0,sk1))
| sk7(sk0,sk1) = sk8(sk0,sk1) ),
inference(factoring,[status(thm)],[p557]) ).
cnf(c85,plain,
( in(sk11(X0,X1,X3),powerset(the_carrier(X0)))
| ~ in(X3,sk10(X0,X1))
| sk7(X0,X1) = sk8(X0,X1)
| ~ element(X1,powerset(powerset(the_carrier(X0))))
| ~ top_str(X0)
| ~ topological_space(X0) ),
inference(cnf_transformation,[status(esa)],[f35_sk]) ).
cnf(p287,plain,
( in(sk11(sk0,X0,X1),powerset(the_carrier(sk0)))
| ~ in(X1,sk10(sk0,X0))
| sk7(sk0,X0) = sk8(sk0,X0)
| ~ element(X0,powerset(powerset(the_carrier(sk0))))
| ~ top_str(sk0) ),
inference(resolution,[status(thm)],[c85,c0]) ).
cnf(p288,plain,
( in(sk11(sk0,X0,X1),powerset(the_carrier(sk0)))
| ~ in(X1,sk10(sk0,X0))
| sk7(sk0,X0) = sk8(sk0,X0)
| ~ element(X0,powerset(powerset(the_carrier(sk0)))) ),
inference(resolution,[status(thm)],[p287,c1]) ).
cnf(p289,plain,
( in(sk11(sk0,sk1,X0),powerset(the_carrier(sk0)))
| ~ in(X0,sk10(sk0,sk1))
| sk7(sk0,sk1) = sk8(sk0,sk1) ),
inference(resolution,[status(thm)],[p288,c2]) ).
cnf(p556,plain,
( in(sk11(sk0,sk1,sk2(sk10(sk0,sk1))),powerset(the_carrier(sk0)))
| sk7(sk0,sk1) = sk8(sk0,sk1)
| sk7(sk0,sk1) = sk8(sk0,sk1) ),
inference(resolution,[status(thm)],[p518,p289]) ).
cnf(p565,plain,
( in(sk11(sk0,sk1,sk2(sk10(sk0,sk1))),powerset(the_carrier(sk0)))
| sk7(sk0,sk1) = sk8(sk0,sk1) ),
inference(factoring,[status(thm)],[p556]) ).
cnf(p579,plain,
( in(sk2(sk10(sk0,sk1)),powerset(the_carrier(sk0)))
| sk7(sk0,sk1) = sk8(sk0,sk1)
| sk7(sk0,sk1) = sk8(sk0,sk1) ),
inference(superposition,[status(thm)],[p578,p565]) ).
cnf(p581,plain,
( in(sk2(sk10(sk0,sk1)),powerset(the_carrier(sk0)))
| sk7(sk0,sk1) = sk8(sk0,sk1) ),
inference(factoring,[status(thm)],[p579]) ).
cnf(c6,plain,
( ~ in(sk2(X2),X2)
| ~ in(set_difference(cast_as_carrier_subset(sk0),sk2(X2)),sk1)
| ~ in(sk2(X2),powerset(the_carrier(sk0))) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p582,plain,
( ~ in(sk2(sk10(sk0,sk1)),sk10(sk0,sk1))
| ~ in(set_difference(cast_as_carrier_subset(sk0),sk2(sk10(sk0,sk1))),sk1)
| sk7(sk0,sk1) = sk8(sk0,sk1) ),
inference(resolution,[status(thm)],[p581,c6]) ).
cnf(c87,plain,
( in(set_difference(cast_as_carrier_subset(X0),X3),X1)
| ~ in(X3,sk10(X0,X1))
| sk7(X0,X1) = sk8(X0,X1)
| ~ element(X1,powerset(powerset(the_carrier(X0))))
| ~ top_str(X0)
| ~ topological_space(X0) ),
inference(cnf_transformation,[status(esa)],[f35_sk]) ).
cnf(p298,plain,
( in(set_difference(cast_as_carrier_subset(sk0),X1),X0)
| ~ in(X1,sk10(sk0,X0))
| sk7(sk0,X0) = sk8(sk0,X0)
| ~ element(X0,powerset(powerset(the_carrier(sk0))))
| ~ top_str(sk0) ),
inference(resolution,[status(thm)],[c87,c0]) ).
cnf(p308,plain,
( in(set_difference(cast_as_carrier_subset(sk0),X1),X0)
| ~ in(X1,sk10(sk0,X0))
| sk7(sk0,X0) = sk8(sk0,X0)
| ~ element(X0,powerset(powerset(the_carrier(sk0)))) ),
inference(resolution,[status(thm)],[p298,c1]) ).
cnf(p312,plain,
( in(set_difference(cast_as_carrier_subset(sk0),X0),sk1)
| ~ in(X0,sk10(sk0,sk1))
| sk7(sk0,sk1) = sk8(sk0,sk1) ),
inference(resolution,[status(thm)],[p308,c2]) ).
cnf(p316,plain,
( in(set_difference(cast_as_carrier_subset(sk0),sk2(sk10(sk0,sk1))),sk1)
| in(set_difference(cast_as_carrier_subset(sk0),sk2(sk10(sk0,sk1))),sk1)
| sk7(sk0,sk1) = sk8(sk0,sk1) ),
inference(resolution,[status(thm)],[p312,c5]) ).
cnf(p319,plain,
( in(set_difference(cast_as_carrier_subset(sk0),sk2(sk10(sk0,sk1))),sk1)
| sk7(sk0,sk1) = sk8(sk0,sk1) ),
inference(factoring,[status(thm)],[p316]) ).
cnf(p585,plain,
( sk7(sk0,sk1) = sk8(sk0,sk1)
| ~ in(sk2(sk10(sk0,sk1)),sk10(sk0,sk1))
| sk7(sk0,sk1) = sk8(sk0,sk1) ),
inference(resolution,[status(thm)],[p582,p319]) ).
cnf(p589,plain,
( ~ in(sk2(sk10(sk0,sk1)),sk10(sk0,sk1))
| sk7(sk0,sk1) = sk8(sk0,sk1) ),
inference(factoring,[status(thm)],[p585]) ).
cnf(p590,plain,
( sk7(sk0,sk1) = sk8(sk0,sk1)
| sk7(sk0,sk1) = sk8(sk0,sk1) ),
inference(resolution,[status(thm)],[p589,p518]) ).
cnf(p591,plain,
sk7(sk0,sk1) = sk8(sk0,sk1),
inference(factoring,[status(thm)],[p590]) ).
cnf(c104,plain,
( ~ in(set_difference(cast_as_carrier_subset(X0),X3),X1)
| X4 != X3
| ~ in(X4,powerset(the_carrier(X0)))
| in(X3,sk10(X0,X1))
| sk8(X0,X1) != sk9(X0,X1)
| ~ element(X1,powerset(powerset(the_carrier(X0))))
| ~ top_str(X0)
| ~ topological_space(X0) ),
inference(cnf_transformation,[status(esa)],[f35_sk]) ).
cnf(p428,plain,
( ~ in(set_difference(cast_as_carrier_subset(sk0),X1),X0)
| X2 != X1
| ~ in(X2,powerset(the_carrier(sk0)))
| in(X1,sk10(sk0,X0))
| sk8(sk0,X0) != sk9(sk0,X0)
| ~ element(X0,powerset(powerset(the_carrier(sk0))))
| ~ top_str(sk0) ),
inference(resolution,[status(thm)],[c104,c0]) ).
cnf(p755,plain,
( ~ in(set_difference(cast_as_carrier_subset(sk0),X1),X0)
| ~ in(X1,powerset(the_carrier(sk0)))
| in(X1,sk10(sk0,X0))
| sk8(sk0,X0) != sk9(sk0,X0)
| ~ element(X0,powerset(powerset(the_carrier(sk0))))
| ~ top_str(sk0) ),
inference(equality_resolution,[status(thm)],[p428]) ).
cnf(p757,plain,
( ~ in(set_difference(cast_as_carrier_subset(sk0),X1),X0)
| ~ in(X1,powerset(the_carrier(sk0)))
| in(X1,sk10(sk0,X0))
| sk8(sk0,X0) != sk9(sk0,X0)
| ~ element(X0,powerset(powerset(the_carrier(sk0)))) ),
inference(resolution,[status(thm)],[p755,c1]) ).
cnf(p758,plain,
( ~ in(set_difference(cast_as_carrier_subset(sk0),X0),sk1)
| ~ in(X0,powerset(the_carrier(sk0)))
| in(X0,sk10(sk0,sk1))
| sk8(sk0,sk1) != sk9(sk0,sk1) ),
inference(resolution,[status(thm)],[p757,c2]) ).
cnf(p762,plain,
( ~ in(set_difference(cast_as_carrier_subset(sk0),X0),sk1)
| ~ in(X0,powerset(the_carrier(sk0)))
| in(X0,sk10(sk0,sk1))
| sk7(sk0,sk1) != sk9(sk0,sk1) ),
inference(superposition,[status(thm)],[p591,p758]) ).
cnf(c96,plain,
( ~ in(set_difference(cast_as_carrier_subset(X0),X3),X1)
| X4 != X3
| ~ in(X4,powerset(the_carrier(X0)))
| in(X3,sk10(X0,X1))
| sk7(X0,X1) = sk9(X0,X1)
| ~ element(X1,powerset(powerset(the_carrier(X0))))
| ~ top_str(X0)
| ~ topological_space(X0) ),
inference(cnf_transformation,[status(esa)],[f35_sk]) ).
cnf(p368,plain,
( ~ in(set_difference(cast_as_carrier_subset(sk0),X1),X0)
| X2 != X1
| ~ in(X2,powerset(the_carrier(sk0)))
| in(X1,sk10(sk0,X0))
| sk7(sk0,X0) = sk9(sk0,X0)
| ~ element(X0,powerset(powerset(the_carrier(sk0))))
| ~ top_str(sk0) ),
inference(resolution,[status(thm)],[c96,c0]) ).
cnf(p607,plain,
( ~ in(set_difference(cast_as_carrier_subset(sk0),X1),X0)
| ~ in(X1,powerset(the_carrier(sk0)))
| in(X1,sk10(sk0,X0))
| sk7(sk0,X0) = sk9(sk0,X0)
| ~ element(X0,powerset(powerset(the_carrier(sk0))))
| ~ top_str(sk0) ),
inference(equality_resolution,[status(thm)],[p368]) ).
cnf(p609,plain,
( ~ in(set_difference(cast_as_carrier_subset(sk0),X1),X0)
| ~ in(X1,powerset(the_carrier(sk0)))
| in(X1,sk10(sk0,X0))
| sk7(sk0,X0) = sk9(sk0,X0)
| ~ element(X0,powerset(powerset(the_carrier(sk0)))) ),
inference(resolution,[status(thm)],[p607,c1]) ).
cnf(p610,plain,
( ~ in(set_difference(cast_as_carrier_subset(sk0),X0),sk1)
| ~ in(X0,powerset(the_carrier(sk0)))
| in(X0,sk10(sk0,sk1))
| sk7(sk0,sk1) = sk9(sk0,sk1) ),
inference(resolution,[status(thm)],[p609,c2]) ).
cnf(p616,plain,
( in(sk2(X0),X0)
| ~ in(set_difference(cast_as_carrier_subset(sk0),sk2(X0)),sk1)
| in(sk2(X0),sk10(sk0,sk1))
| sk7(sk0,sk1) = sk9(sk0,sk1) ),
inference(resolution,[status(thm)],[p610,c4]) ).
cnf(p621,plain,
( in(sk2(X0),X0)
| in(sk2(X0),X0)
| in(sk2(X0),sk10(sk0,sk1))
| sk7(sk0,sk1) = sk9(sk0,sk1) ),
inference(resolution,[status(thm)],[p616,c5]) ).
cnf(p626,plain,
( in(sk2(X0),X0)
| in(sk2(X0),sk10(sk0,sk1))
| sk7(sk0,sk1) = sk9(sk0,sk1) ),
inference(factoring,[status(thm)],[p621]) ).
cnf(p627,plain,
( in(sk2(sk10(sk0,sk1)),sk10(sk0,sk1))
| sk7(sk0,sk1) = sk9(sk0,sk1) ),
inference(factoring,[status(thm)],[p626]) ).
cnf(c94,plain,
( sk11(X0,X1,X3) = X3
| ~ in(X3,sk10(X0,X1))
| sk7(X0,X1) = sk9(X0,X1)
| ~ element(X1,powerset(powerset(the_carrier(X0))))
| ~ top_str(X0)
| ~ topological_space(X0) ),
inference(cnf_transformation,[status(esa)],[f35_sk]) ).
cnf(p352,plain,
( sk11(sk0,X0,X1) = X1
| ~ in(X1,sk10(sk0,X0))
| sk7(sk0,X0) = sk9(sk0,X0)
| ~ element(X0,powerset(powerset(the_carrier(sk0))))
| ~ top_str(sk0) ),
inference(resolution,[status(thm)],[c94,c0]) ).
cnf(p353,plain,
( sk11(sk0,X0,X1) = X1
| ~ in(X1,sk10(sk0,X0))
| sk7(sk0,X0) = sk9(sk0,X0)
| ~ element(X0,powerset(powerset(the_carrier(sk0)))) ),
inference(resolution,[status(thm)],[p352,c1]) ).
cnf(p354,plain,
( sk11(sk0,sk1,X0) = X0
| ~ in(X0,sk10(sk0,sk1))
| sk7(sk0,sk1) = sk9(sk0,sk1) ),
inference(resolution,[status(thm)],[p353,c2]) ).
cnf(p668,plain,
( sk11(sk0,sk1,sk2(sk10(sk0,sk1))) = sk2(sk10(sk0,sk1))
| sk7(sk0,sk1) = sk9(sk0,sk1)
| sk7(sk0,sk1) = sk9(sk0,sk1) ),
inference(resolution,[status(thm)],[p627,p354]) ).
cnf(p697,plain,
( sk11(sk0,sk1,sk2(sk10(sk0,sk1))) = sk2(sk10(sk0,sk1))
| sk7(sk0,sk1) = sk9(sk0,sk1) ),
inference(factoring,[status(thm)],[p668]) ).
cnf(c93,plain,
( in(sk11(X0,X1,X3),powerset(the_carrier(X0)))
| ~ in(X3,sk10(X0,X1))
| sk7(X0,X1) = sk9(X0,X1)
| ~ element(X1,powerset(powerset(the_carrier(X0))))
| ~ top_str(X0)
| ~ topological_space(X0) ),
inference(cnf_transformation,[status(esa)],[f35_sk]) ).
cnf(p349,plain,
( in(sk11(sk0,X0,X1),powerset(the_carrier(sk0)))
| ~ in(X1,sk10(sk0,X0))
| sk7(sk0,X0) = sk9(sk0,X0)
| ~ element(X0,powerset(powerset(the_carrier(sk0))))
| ~ top_str(sk0) ),
inference(resolution,[status(thm)],[c93,c0]) ).
cnf(p377,plain,
( in(sk11(sk0,X0,X1),powerset(the_carrier(sk0)))
| ~ in(X1,sk10(sk0,X0))
| sk7(sk0,X0) = sk9(sk0,X0)
| ~ element(X0,powerset(powerset(the_carrier(sk0)))) ),
inference(resolution,[status(thm)],[p349,c1]) ).
cnf(p379,plain,
( in(sk11(sk0,sk1,X0),powerset(the_carrier(sk0)))
| ~ in(X0,sk10(sk0,sk1))
| sk7(sk0,sk1) = sk9(sk0,sk1) ),
inference(resolution,[status(thm)],[p377,c2]) ).
cnf(p669,plain,
( in(sk11(sk0,sk1,sk2(sk10(sk0,sk1))),powerset(the_carrier(sk0)))
| sk7(sk0,sk1) = sk9(sk0,sk1)
| sk7(sk0,sk1) = sk9(sk0,sk1) ),
inference(resolution,[status(thm)],[p627,p379]) ).
cnf(p685,plain,
( in(sk11(sk0,sk1,sk2(sk10(sk0,sk1))),powerset(the_carrier(sk0)))
| sk7(sk0,sk1) = sk9(sk0,sk1) ),
inference(factoring,[status(thm)],[p669]) ).
cnf(p698,plain,
( in(sk2(sk10(sk0,sk1)),powerset(the_carrier(sk0)))
| sk7(sk0,sk1) = sk9(sk0,sk1)
| sk7(sk0,sk1) = sk9(sk0,sk1) ),
inference(superposition,[status(thm)],[p697,p685]) ).
cnf(p700,plain,
( in(sk2(sk10(sk0,sk1)),powerset(the_carrier(sk0)))
| sk7(sk0,sk1) = sk9(sk0,sk1) ),
inference(factoring,[status(thm)],[p698]) ).
cnf(p701,plain,
( ~ in(sk2(sk10(sk0,sk1)),sk10(sk0,sk1))
| ~ in(set_difference(cast_as_carrier_subset(sk0),sk2(sk10(sk0,sk1))),sk1)
| sk7(sk0,sk1) = sk9(sk0,sk1) ),
inference(resolution,[status(thm)],[p700,c6]) ).
cnf(c95,plain,
( in(set_difference(cast_as_carrier_subset(X0),X3),X1)
| ~ in(X3,sk10(X0,X1))
| sk7(X0,X1) = sk9(X0,X1)
| ~ element(X1,powerset(powerset(the_carrier(X0))))
| ~ top_str(X0)
| ~ topological_space(X0) ),
inference(cnf_transformation,[status(esa)],[f35_sk]) ).
cnf(p359,plain,
( in(set_difference(cast_as_carrier_subset(sk0),X1),X0)
| ~ in(X1,sk10(sk0,X0))
| sk7(sk0,X0) = sk9(sk0,X0)
| ~ element(X0,powerset(powerset(the_carrier(sk0))))
| ~ top_str(sk0) ),
inference(resolution,[status(thm)],[c95,c0]) ).
cnf(p362,plain,
( in(set_difference(cast_as_carrier_subset(sk0),X1),X0)
| ~ in(X1,sk10(sk0,X0))
| sk7(sk0,X0) = sk9(sk0,X0)
| ~ element(X0,powerset(powerset(the_carrier(sk0)))) ),
inference(resolution,[status(thm)],[p359,c1]) ).
cnf(p363,plain,
( in(set_difference(cast_as_carrier_subset(sk0),X0),sk1)
| ~ in(X0,sk10(sk0,sk1))
| sk7(sk0,sk1) = sk9(sk0,sk1) ),
inference(resolution,[status(thm)],[p362,c2]) ).
cnf(p370,plain,
( in(set_difference(cast_as_carrier_subset(sk0),sk2(sk10(sk0,sk1))),sk1)
| in(set_difference(cast_as_carrier_subset(sk0),sk2(sk10(sk0,sk1))),sk1)
| sk7(sk0,sk1) = sk9(sk0,sk1) ),
inference(resolution,[status(thm)],[p363,c5]) ).
cnf(p372,plain,
( in(set_difference(cast_as_carrier_subset(sk0),sk2(sk10(sk0,sk1))),sk1)
| sk7(sk0,sk1) = sk9(sk0,sk1) ),
inference(factoring,[status(thm)],[p370]) ).
cnf(p708,plain,
( sk7(sk0,sk1) = sk9(sk0,sk1)
| ~ in(sk2(sk10(sk0,sk1)),sk10(sk0,sk1))
| sk7(sk0,sk1) = sk9(sk0,sk1) ),
inference(resolution,[status(thm)],[p701,p372]) ).
cnf(p710,plain,
( ~ in(sk2(sk10(sk0,sk1)),sk10(sk0,sk1))
| sk7(sk0,sk1) = sk9(sk0,sk1) ),
inference(factoring,[status(thm)],[p708]) ).
cnf(p711,plain,
( sk7(sk0,sk1) = sk9(sk0,sk1)
| sk7(sk0,sk1) = sk9(sk0,sk1) ),
inference(resolution,[status(thm)],[p710,p627]) ).
cnf(p712,plain,
sk7(sk0,sk1) = sk9(sk0,sk1),
inference(factoring,[status(thm)],[p711]) ).
cnf(p764,plain,
( ~ in(set_difference(cast_as_carrier_subset(sk0),X0),sk1)
| ~ in(X0,powerset(the_carrier(sk0)))
| in(X0,sk10(sk0,sk1)) ),
inference(resolution,[status(thm)],[p762,p712]) ).
cnf(c102,plain,
( sk11(X0,X1,X3) = X3
| ~ in(X3,sk10(X0,X1))
| sk8(X0,X1) != sk9(X0,X1)
| ~ element(X1,powerset(powerset(the_carrier(X0))))
| ~ top_str(X0)
| ~ topological_space(X0) ),
inference(cnf_transformation,[status(esa)],[f35_sk]) ).
cnf(p416,plain,
( sk11(sk0,X0,X1) = X1
| ~ in(X1,sk10(sk0,X0))
| sk8(sk0,X0) != sk9(sk0,X0)
| ~ element(X0,powerset(powerset(the_carrier(sk0))))
| ~ top_str(sk0) ),
inference(resolution,[status(thm)],[c102,c0]) ).
cnf(p420,plain,
( sk11(sk0,X0,X1) = X1
| ~ in(X1,sk10(sk0,X0))
| sk8(sk0,X0) != sk9(sk0,X0)
| ~ element(X0,powerset(powerset(the_carrier(sk0)))) ),
inference(resolution,[status(thm)],[p416,c1]) ).
cnf(p421,plain,
( sk11(sk0,sk1,X0) = X0
| ~ in(X0,sk10(sk0,sk1))
| sk8(sk0,sk1) != sk9(sk0,sk1) ),
inference(resolution,[status(thm)],[p420,c2]) ).
cnf(p593,plain,
( sk11(sk0,sk1,X0) = X0
| ~ in(X0,sk10(sk0,sk1))
| sk7(sk0,sk1) != sk9(sk0,sk1) ),
inference(superposition,[status(thm)],[p591,p421]) ).
cnf(p717,plain,
( sk11(sk0,sk1,X0) = X0
| ~ in(X0,sk10(sk0,sk1)) ),
inference(resolution,[status(thm)],[p712,p593]) ).
cnf(p720,plain,
( in(sk2(sk10(sk0,sk1)),powerset(the_carrier(sk0)))
| sk11(sk0,sk1,sk2(sk10(sk0,sk1))) = sk2(sk10(sk0,sk1)) ),
inference(resolution,[status(thm)],[p717,c4]) ).
cnf(c101,plain,
( in(sk11(X0,X1,X3),powerset(the_carrier(X0)))
| ~ in(X3,sk10(X0,X1))
| sk8(X0,X1) != sk9(X0,X1)
| ~ element(X1,powerset(powerset(the_carrier(X0))))
| ~ top_str(X0)
| ~ topological_space(X0) ),
inference(cnf_transformation,[status(esa)],[f35_sk]) ).
cnf(p409,plain,
( in(sk11(sk0,X0,X1),powerset(the_carrier(sk0)))
| ~ in(X1,sk10(sk0,X0))
| sk8(sk0,X0) != sk9(sk0,X0)
| ~ element(X0,powerset(powerset(the_carrier(sk0))))
| ~ top_str(sk0) ),
inference(resolution,[status(thm)],[c101,c0]) ).
cnf(p436,plain,
( in(sk11(sk0,X0,X1),powerset(the_carrier(sk0)))
| ~ in(X1,sk10(sk0,X0))
| sk8(sk0,X0) != sk9(sk0,X0)
| ~ element(X0,powerset(powerset(the_carrier(sk0)))) ),
inference(resolution,[status(thm)],[p409,c1]) ).
cnf(p437,plain,
( in(sk11(sk0,sk1,X0),powerset(the_carrier(sk0)))
| ~ in(X0,sk10(sk0,sk1))
| sk8(sk0,sk1) != sk9(sk0,sk1) ),
inference(resolution,[status(thm)],[p436,c2]) ).
cnf(p595,plain,
( in(sk11(sk0,sk1,X0),powerset(the_carrier(sk0)))
| ~ in(X0,sk10(sk0,sk1))
| sk7(sk0,sk1) != sk9(sk0,sk1) ),
inference(superposition,[status(thm)],[p591,p437]) ).
cnf(p719,plain,
( in(sk11(sk0,sk1,X0),powerset(the_carrier(sk0)))
| ~ in(X0,sk10(sk0,sk1)) ),
inference(resolution,[status(thm)],[p712,p595]) ).
cnf(p724,plain,
( in(sk2(sk10(sk0,sk1)),powerset(the_carrier(sk0)))
| in(sk11(sk0,sk1,sk2(sk10(sk0,sk1))),powerset(the_carrier(sk0))) ),
inference(resolution,[status(thm)],[p719,c4]) ).
cnf(p736,plain,
( in(sk2(sk10(sk0,sk1)),powerset(the_carrier(sk0)))
| in(sk2(sk10(sk0,sk1)),powerset(the_carrier(sk0)))
| in(sk2(sk10(sk0,sk1)),powerset(the_carrier(sk0))) ),
inference(superposition,[status(thm)],[p720,p724]) ).
cnf(p738,plain,
( in(sk2(sk10(sk0,sk1)),powerset(the_carrier(sk0)))
| in(sk2(sk10(sk0,sk1)),powerset(the_carrier(sk0))) ),
inference(factoring,[status(thm)],[p736]) ).
cnf(p739,plain,
in(sk2(sk10(sk0,sk1)),powerset(the_carrier(sk0))),
inference(factoring,[status(thm)],[p738]) ).
cnf(p766,plain,
( ~ in(set_difference(cast_as_carrier_subset(sk0),sk2(sk10(sk0,sk1))),sk1)
| in(sk2(sk10(sk0,sk1)),sk10(sk0,sk1)) ),
inference(resolution,[status(thm)],[p764,p739]) ).
cnf(c103,plain,
( in(set_difference(cast_as_carrier_subset(X0),X3),X1)
| ~ in(X3,sk10(X0,X1))
| sk8(X0,X1) != sk9(X0,X1)
| ~ element(X1,powerset(powerset(the_carrier(X0))))
| ~ top_str(X0)
| ~ topological_space(X0) ),
inference(cnf_transformation,[status(esa)],[f35_sk]) ).
cnf(p419,plain,
( in(set_difference(cast_as_carrier_subset(sk0),X1),X0)
| ~ in(X1,sk10(sk0,X0))
| sk8(sk0,X0) != sk9(sk0,X0)
| ~ element(X0,powerset(powerset(the_carrier(sk0))))
| ~ top_str(sk0) ),
inference(resolution,[status(thm)],[c103,c0]) ).
cnf(p424,plain,
( in(set_difference(cast_as_carrier_subset(sk0),X1),X0)
| ~ in(X1,sk10(sk0,X0))
| sk8(sk0,X0) != sk9(sk0,X0)
| ~ element(X0,powerset(powerset(the_carrier(sk0)))) ),
inference(resolution,[status(thm)],[p419,c1]) ).
cnf(p429,plain,
( in(set_difference(cast_as_carrier_subset(sk0),X0),sk1)
| ~ in(X0,sk10(sk0,sk1))
| sk8(sk0,sk1) != sk9(sk0,sk1) ),
inference(resolution,[status(thm)],[p424,c2]) ).
cnf(p594,plain,
( in(set_difference(cast_as_carrier_subset(sk0),X0),sk1)
| ~ in(X0,sk10(sk0,sk1))
| sk7(sk0,sk1) != sk9(sk0,sk1) ),
inference(superposition,[status(thm)],[p591,p429]) ).
cnf(p718,plain,
( in(set_difference(cast_as_carrier_subset(sk0),X0),sk1)
| ~ in(X0,sk10(sk0,sk1)) ),
inference(resolution,[status(thm)],[p712,p594]) ).
cnf(p723,plain,
( in(set_difference(cast_as_carrier_subset(sk0),sk2(sk10(sk0,sk1))),sk1)
| in(set_difference(cast_as_carrier_subset(sk0),sk2(sk10(sk0,sk1))),sk1) ),
inference(resolution,[status(thm)],[p718,c5]) ).
cnf(p730,plain,
in(set_difference(cast_as_carrier_subset(sk0),sk2(sk10(sk0,sk1))),sk1),
inference(factoring,[status(thm)],[p723]) ).
cnf(p768,plain,
in(sk2(sk10(sk0,sk1)),sk10(sk0,sk1)),
inference(resolution,[status(thm)],[p766,p730]) ).
cnf(p740,plain,
( ~ in(sk2(sk10(sk0,sk1)),sk10(sk0,sk1))
| ~ in(set_difference(cast_as_carrier_subset(sk0),sk2(sk10(sk0,sk1))),sk1) ),
inference(resolution,[status(thm)],[p739,c6]) ).
cnf(p744,plain,
~ in(sk2(sk10(sk0,sk1)),sk10(sk0,sk1)),
inference(resolution,[status(thm)],[p740,p730]) ).
cnf(p772,plain,
$false,
inference(resolution,[status(thm)],[p768,p744]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SEU310+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.06 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.14/0.40 % Computer : n003.cluster.edu
% 0.14/0.40 % Model : x86_64 x86_64
% 0.14/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.40 % Memory : 8046.5625MB
% 0.14/0.40 % OS : Linux 6.8.0-71-generic
% 0.14/0.40 % CPULimit : 300
% 0.14/0.40 % WCLimit : 300
% 0.14/0.40 % DateTime : Thu Sep 24 13:40:05 UTC 2026
% 0.14/0.40 % CPUTime :
% 0.14/0.40 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 27.88/4.46 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 27.88/4.46 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------