%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SEU310+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n005.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 : Sun Sep 27 08:45:46 AM UTC 2026
% Result : Theorem 0.96s 0.54s
% Output : CNFRefutation 0.96s
% Verified :
% SZS Type : Refutation
% Derivation depth : 33
% Number of leaves : 2
% Syntax : Number of formulae : 128 ( 12 unt; 0 def)
% Number of atoms : 641 ( 196 equ)
% Maximal formula atoms : 130 ( 5 avg)
% Number of connectives : 849 ( 336 ~; 444 |; 61 &)
% ( 3 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 32 ( 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 : 234 ( 0 sgn 90 !; 12 ?)
% Comments :
%------------------------------------------------------------------------------
fof(s1_tarski__e2_37_1_1__pre_topc__1,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('theBenchmark.p',s1_tarski__e2_37_1_1__pre_topc__1) ).
fof(s1_xboole_0__e2_37_1_1__pre_topc__1,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('theBenchmark.p',s1_xboole_0__e2_37_1_1__pre_topc__1) ).
fof(s1_xboole_0__e2_37_1_1__pre_topc__1_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(assume_negation,[status(cth)],[s1_xboole_0__e2_37_1_1__pre_topc__1]) ).
fof(nnf_36,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(fof_nnf,[status(thm)],[s1_xboole_0__e2_37_1_1__pre_topc__1_neg]) ).
fof(sk_s1_xboole_0__e2_37_1_1__pre_topc__1_neg_sk,plain,
( ! [C] :
( ( ~ in(set_difference(cast_as_carrier_subset(sK0),sK7(C)),sK6)
| ~ in(sK7(C),powerset(the_carrier(sK0)))
| ~ in(sK7(C),C) )
& ( ( in(set_difference(cast_as_carrier_subset(sK0),sK7(C)),sK6)
& in(sK7(C),powerset(the_carrier(sK0))) )
| in(sK7(C),C) ) )
& element(sK6,powerset(powerset(the_carrier(sK0))))
& top_str(sK0)
& topological_space(sK0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK6,sK7]),skolemize(A,sK0),skolemize(B,sK6),skolemize(D,sK7(C))],[nnf_36]) ).
fof(sk_s1_xboole_0__e2_37_1_1__pre_topc__1_neg,plain,
( ! [VAR_0] :
( ~ in(set_difference(cast_as_carrier_subset(sK0),sK7(VAR_0)),sK6)
| ~ in(sK7(VAR_0),powerset(the_carrier(sK0)))
| ~ in(sK7(VAR_0),VAR_0) )
& ! [VAR_0] :
( in(set_difference(cast_as_carrier_subset(sK0),sK7(VAR_0)),sK6)
| in(sK7(VAR_0),VAR_0) )
& ! [VAR_0] :
( in(sK7(VAR_0),powerset(the_carrier(sK0)))
| in(sK7(VAR_0),VAR_0) )
& element(sK6,powerset(powerset(the_carrier(sK0))))
& top_str(sK0)
& topological_space(sK0) ),
inference(cnf_transformation,[status(thm)],[sk_s1_xboole_0__e2_37_1_1__pre_topc__1_neg_sk]) ).
cnf(c_37,negated_conjecture,
topological_space(sK0),
inference(split_conjunct,[status(thm)],[sk_s1_xboole_0__e2_37_1_1__pre_topc__1_neg]) ).
fof(nnf_35,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) )
& ( ? [X3] :
( in(set_difference(cast_as_carrier_subset(A),D),B)
& X3 = D
& in(X3,powerset(the_carrier(A))) )
| ~ in(D,C) ) )
| ? [X0,X1,X2] :
( X2 != X1
& in(set_difference(cast_as_carrier_subset(A),X2),B)
& X2 = X0
& in(set_difference(cast_as_carrier_subset(A),X1),B)
& X0 = X1 )
| ~ element(B,powerset(powerset(the_carrier(A))))
| ~ top_str(A)
| ~ topological_space(A) ),
inference(fof_nnf,[status(thm)],[s1_tarski__e2_37_1_1__pre_topc__1]) ).
fof(sk_s1_tarski__e2_37_1_1__pre_topc__1_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,sK3(A,B)) )
& ( ( in(set_difference(cast_as_carrier_subset(A),D),B)
& sK4(A,B,D) = D
& in(sK4(A,B,D),powerset(the_carrier(A))) )
| ~ in(D,sK3(A,B)) ) )
| ( sK1(A,B) != sK2(A,B)
& in(set_difference(cast_as_carrier_subset(A),sK1(A,B)),B)
& sK1(A,B) = sK5(A,B)
& in(set_difference(cast_as_carrier_subset(A),sK2(A,B)),B)
& sK5(A,B) = sK2(A,B) )
| ~ element(B,powerset(powerset(the_carrier(A))))
| ~ top_str(A)
| ~ topological_space(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5,sK2,sK1,sK3,sK4]),skolemize(X0,sK5(A,B)),skolemize(X1,sK2(A,B)),skolemize(X2,sK1(A,B)),skolemize(C,sK3(A,B)),skolemize(X3,sK4(A,B,D))],[nnf_35]) ).
fof(sk_s1_tarski__e2_37_1_1__pre_topc__1,plain,
( ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ in(set_difference(cast_as_carrier_subset(VAR_0),VAR_2),VAR_1)
| VAR_3 != VAR_2
| ~ in(VAR_3,powerset(the_carrier(VAR_0)))
| in(VAR_2,sK3(VAR_0,VAR_1))
| sK1(VAR_0,VAR_1) != sK2(VAR_0,VAR_1)
| ~ element(VAR_1,powerset(powerset(the_carrier(VAR_0))))
| ~ top_str(VAR_0)
| ~ topological_space(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( in(set_difference(cast_as_carrier_subset(VAR_0),VAR_2),VAR_1)
| ~ in(VAR_2,sK3(VAR_0,VAR_1))
| sK1(VAR_0,VAR_1) != sK2(VAR_0,VAR_1)
| ~ element(VAR_1,powerset(powerset(the_carrier(VAR_0))))
| ~ top_str(VAR_0)
| ~ topological_space(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( sK4(VAR_0,VAR_1,VAR_2) = VAR_2
| ~ in(VAR_2,sK3(VAR_0,VAR_1))
| sK1(VAR_0,VAR_1) != sK2(VAR_0,VAR_1)
| ~ element(VAR_1,powerset(powerset(the_carrier(VAR_0))))
| ~ top_str(VAR_0)
| ~ topological_space(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( in(sK4(VAR_0,VAR_1,VAR_2),powerset(the_carrier(VAR_0)))
| ~ in(VAR_2,sK3(VAR_0,VAR_1))
| sK1(VAR_0,VAR_1) != sK2(VAR_0,VAR_1)
| ~ element(VAR_1,powerset(powerset(the_carrier(VAR_0))))
| ~ top_str(VAR_0)
| ~ topological_space(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ in(set_difference(cast_as_carrier_subset(VAR_0),VAR_2),VAR_1)
| VAR_3 != VAR_2
| ~ in(VAR_3,powerset(the_carrier(VAR_0)))
| in(VAR_2,sK3(VAR_0,VAR_1))
| in(set_difference(cast_as_carrier_subset(VAR_0),sK1(VAR_0,VAR_1)),VAR_1)
| ~ element(VAR_1,powerset(powerset(the_carrier(VAR_0))))
| ~ top_str(VAR_0)
| ~ topological_space(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( in(set_difference(cast_as_carrier_subset(VAR_0),VAR_2),VAR_1)
| ~ in(VAR_2,sK3(VAR_0,VAR_1))
| in(set_difference(cast_as_carrier_subset(VAR_0),sK1(VAR_0,VAR_1)),VAR_1)
| ~ element(VAR_1,powerset(powerset(the_carrier(VAR_0))))
| ~ top_str(VAR_0)
| ~ topological_space(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( sK4(VAR_0,VAR_1,VAR_2) = VAR_2
| ~ in(VAR_2,sK3(VAR_0,VAR_1))
| in(set_difference(cast_as_carrier_subset(VAR_0),sK1(VAR_0,VAR_1)),VAR_1)
| ~ element(VAR_1,powerset(powerset(the_carrier(VAR_0))))
| ~ top_str(VAR_0)
| ~ topological_space(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( in(sK4(VAR_0,VAR_1,VAR_2),powerset(the_carrier(VAR_0)))
| ~ in(VAR_2,sK3(VAR_0,VAR_1))
| in(set_difference(cast_as_carrier_subset(VAR_0),sK1(VAR_0,VAR_1)),VAR_1)
| ~ element(VAR_1,powerset(powerset(the_carrier(VAR_0))))
| ~ top_str(VAR_0)
| ~ topological_space(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ in(set_difference(cast_as_carrier_subset(VAR_0),VAR_2),VAR_1)
| VAR_3 != VAR_2
| ~ in(VAR_3,powerset(the_carrier(VAR_0)))
| in(VAR_2,sK3(VAR_0,VAR_1))
| sK1(VAR_0,VAR_1) = sK5(VAR_0,VAR_1)
| ~ element(VAR_1,powerset(powerset(the_carrier(VAR_0))))
| ~ top_str(VAR_0)
| ~ topological_space(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( in(set_difference(cast_as_carrier_subset(VAR_0),VAR_2),VAR_1)
| ~ in(VAR_2,sK3(VAR_0,VAR_1))
| sK1(VAR_0,VAR_1) = sK5(VAR_0,VAR_1)
| ~ element(VAR_1,powerset(powerset(the_carrier(VAR_0))))
| ~ top_str(VAR_0)
| ~ topological_space(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( sK4(VAR_0,VAR_1,VAR_2) = VAR_2
| ~ in(VAR_2,sK3(VAR_0,VAR_1))
| sK1(VAR_0,VAR_1) = sK5(VAR_0,VAR_1)
| ~ element(VAR_1,powerset(powerset(the_carrier(VAR_0))))
| ~ top_str(VAR_0)
| ~ topological_space(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( in(sK4(VAR_0,VAR_1,VAR_2),powerset(the_carrier(VAR_0)))
| ~ in(VAR_2,sK3(VAR_0,VAR_1))
| sK1(VAR_0,VAR_1) = sK5(VAR_0,VAR_1)
| ~ element(VAR_1,powerset(powerset(the_carrier(VAR_0))))
| ~ top_str(VAR_0)
| ~ topological_space(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ in(set_difference(cast_as_carrier_subset(VAR_0),VAR_2),VAR_1)
| VAR_3 != VAR_2
| ~ in(VAR_3,powerset(the_carrier(VAR_0)))
| in(VAR_2,sK3(VAR_0,VAR_1))
| in(set_difference(cast_as_carrier_subset(VAR_0),sK2(VAR_0,VAR_1)),VAR_1)
| ~ element(VAR_1,powerset(powerset(the_carrier(VAR_0))))
| ~ top_str(VAR_0)
| ~ topological_space(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( in(set_difference(cast_as_carrier_subset(VAR_0),VAR_2),VAR_1)
| ~ in(VAR_2,sK3(VAR_0,VAR_1))
| in(set_difference(cast_as_carrier_subset(VAR_0),sK2(VAR_0,VAR_1)),VAR_1)
| ~ element(VAR_1,powerset(powerset(the_carrier(VAR_0))))
| ~ top_str(VAR_0)
| ~ topological_space(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( sK4(VAR_0,VAR_1,VAR_2) = VAR_2
| ~ in(VAR_2,sK3(VAR_0,VAR_1))
| in(set_difference(cast_as_carrier_subset(VAR_0),sK2(VAR_0,VAR_1)),VAR_1)
| ~ element(VAR_1,powerset(powerset(the_carrier(VAR_0))))
| ~ top_str(VAR_0)
| ~ topological_space(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( in(sK4(VAR_0,VAR_1,VAR_2),powerset(the_carrier(VAR_0)))
| ~ in(VAR_2,sK3(VAR_0,VAR_1))
| in(set_difference(cast_as_carrier_subset(VAR_0),sK2(VAR_0,VAR_1)),VAR_1)
| ~ element(VAR_1,powerset(powerset(the_carrier(VAR_0))))
| ~ top_str(VAR_0)
| ~ topological_space(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ in(set_difference(cast_as_carrier_subset(VAR_0),VAR_2),VAR_1)
| VAR_3 != VAR_2
| ~ in(VAR_3,powerset(the_carrier(VAR_0)))
| in(VAR_2,sK3(VAR_0,VAR_1))
| sK5(VAR_0,VAR_1) = sK2(VAR_0,VAR_1)
| ~ element(VAR_1,powerset(powerset(the_carrier(VAR_0))))
| ~ top_str(VAR_0)
| ~ topological_space(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( in(set_difference(cast_as_carrier_subset(VAR_0),VAR_2),VAR_1)
| ~ in(VAR_2,sK3(VAR_0,VAR_1))
| sK5(VAR_0,VAR_1) = sK2(VAR_0,VAR_1)
| ~ element(VAR_1,powerset(powerset(the_carrier(VAR_0))))
| ~ top_str(VAR_0)
| ~ topological_space(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( sK4(VAR_0,VAR_1,VAR_2) = VAR_2
| ~ in(VAR_2,sK3(VAR_0,VAR_1))
| sK5(VAR_0,VAR_1) = sK2(VAR_0,VAR_1)
| ~ element(VAR_1,powerset(powerset(the_carrier(VAR_0))))
| ~ top_str(VAR_0)
| ~ topological_space(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( in(sK4(VAR_0,VAR_1,VAR_2),powerset(the_carrier(VAR_0)))
| ~ in(VAR_2,sK3(VAR_0,VAR_1))
| sK5(VAR_0,VAR_1) = sK2(VAR_0,VAR_1)
| ~ element(VAR_1,powerset(powerset(the_carrier(VAR_0))))
| ~ top_str(VAR_0)
| ~ topological_space(VAR_0) ) ),
inference(cnf_transformation,[status(thm)],[sk_s1_tarski__e2_37_1_1__pre_topc__1_sk]) ).
cnf(c_38,plain,
( ~ in(set_difference(cast_as_carrier_subset(A),C),B)
| D != C
| ~ in(D,powerset(the_carrier(A)))
| in(C,sK3(A,B))
| sK1(A,B) != sK2(A,B)
| ~ element(B,powerset(powerset(the_carrier(A))))
| ~ top_str(A)
| ~ topological_space(A) ),
inference(split_conjunct,[status(thm)],[sk_s1_tarski__e2_37_1_1__pre_topc__1]) ).
cnf(c_39,plain,
( in(set_difference(cast_as_carrier_subset(A),C),B)
| ~ in(C,sK3(A,B))
| sK1(A,B) != sK2(A,B)
| ~ element(B,powerset(powerset(the_carrier(A))))
| ~ top_str(A)
| ~ topological_space(A) ),
inference(split_conjunct,[status(thm)],[sk_s1_tarski__e2_37_1_1__pre_topc__1]) ).
cnf(c_40,plain,
( sK4(A,B,C) = C
| ~ in(C,sK3(A,B))
| sK1(A,B) != sK2(A,B)
| ~ element(B,powerset(powerset(the_carrier(A))))
| ~ top_str(A)
| ~ topological_space(A) ),
inference(split_conjunct,[status(thm)],[sk_s1_tarski__e2_37_1_1__pre_topc__1]) ).
cnf(c_41,plain,
( in(sK4(A,B,C),powerset(the_carrier(A)))
| ~ in(C,sK3(A,B))
| sK1(A,B) != sK2(A,B)
| ~ element(B,powerset(powerset(the_carrier(A))))
| ~ top_str(A)
| ~ topological_space(A) ),
inference(split_conjunct,[status(thm)],[sk_s1_tarski__e2_37_1_1__pre_topc__1]) ).
cnf(c_46,plain,
( ~ in(set_difference(cast_as_carrier_subset(A),C),B)
| D != C
| ~ in(D,powerset(the_carrier(A)))
| in(C,sK3(A,B))
| sK1(A,B) = sK5(A,B)
| ~ element(B,powerset(powerset(the_carrier(A))))
| ~ top_str(A)
| ~ topological_space(A) ),
inference(split_conjunct,[status(thm)],[sk_s1_tarski__e2_37_1_1__pre_topc__1]) ).
cnf(c_47,plain,
( in(set_difference(cast_as_carrier_subset(A),C),B)
| ~ in(C,sK3(A,B))
| sK1(A,B) = sK5(A,B)
| ~ element(B,powerset(powerset(the_carrier(A))))
| ~ top_str(A)
| ~ topological_space(A) ),
inference(split_conjunct,[status(thm)],[sk_s1_tarski__e2_37_1_1__pre_topc__1]) ).
cnf(c_48,plain,
( sK4(A,B,C) = C
| ~ in(C,sK3(A,B))
| sK1(A,B) = sK5(A,B)
| ~ element(B,powerset(powerset(the_carrier(A))))
| ~ top_str(A)
| ~ topological_space(A) ),
inference(split_conjunct,[status(thm)],[sk_s1_tarski__e2_37_1_1__pre_topc__1]) ).
cnf(c_49,plain,
( in(sK4(A,B,C),powerset(the_carrier(A)))
| ~ in(C,sK3(A,B))
| sK1(A,B) = sK5(A,B)
| ~ element(B,powerset(powerset(the_carrier(A))))
| ~ top_str(A)
| ~ topological_space(A) ),
inference(split_conjunct,[status(thm)],[sk_s1_tarski__e2_37_1_1__pre_topc__1]) ).
cnf(c_54,plain,
( ~ in(set_difference(cast_as_carrier_subset(A),C),B)
| D != C
| ~ in(D,powerset(the_carrier(A)))
| in(C,sK3(A,B))
| sK5(A,B) = sK2(A,B)
| ~ element(B,powerset(powerset(the_carrier(A))))
| ~ top_str(A)
| ~ topological_space(A) ),
inference(split_conjunct,[status(thm)],[sk_s1_tarski__e2_37_1_1__pre_topc__1]) ).
cnf(c_55,plain,
( in(set_difference(cast_as_carrier_subset(A),C),B)
| ~ in(C,sK3(A,B))
| sK5(A,B) = sK2(A,B)
| ~ element(B,powerset(powerset(the_carrier(A))))
| ~ top_str(A)
| ~ topological_space(A) ),
inference(split_conjunct,[status(thm)],[sk_s1_tarski__e2_37_1_1__pre_topc__1]) ).
cnf(c_56,plain,
( sK4(A,B,C) = C
| ~ in(C,sK3(A,B))
| sK5(A,B) = sK2(A,B)
| ~ element(B,powerset(powerset(the_carrier(A))))
| ~ top_str(A)
| ~ topological_space(A) ),
inference(split_conjunct,[status(thm)],[sk_s1_tarski__e2_37_1_1__pre_topc__1]) ).
cnf(c_57,plain,
( in(sK4(A,B,C),powerset(the_carrier(A)))
| ~ in(C,sK3(A,B))
| sK5(A,B) = sK2(A,B)
| ~ element(B,powerset(powerset(the_carrier(A))))
| ~ top_str(A)
| ~ topological_space(A) ),
inference(split_conjunct,[status(thm)],[sk_s1_tarski__e2_37_1_1__pre_topc__1]) ).
cnf(c_115,negated_conjecture,
top_str(sK0),
inference(split_conjunct,[status(thm)],[sk_s1_xboole_0__e2_37_1_1__pre_topc__1_neg]) ).
cnf(c_116,negated_conjecture,
element(sK6,powerset(powerset(the_carrier(sK0)))),
inference(split_conjunct,[status(thm)],[sk_s1_xboole_0__e2_37_1_1__pre_topc__1_neg]) ).
cnf(c_117,negated_conjecture,
( in(sK7(A),powerset(the_carrier(sK0)))
| in(sK7(A),A) ),
inference(split_conjunct,[status(thm)],[sk_s1_xboole_0__e2_37_1_1__pre_topc__1_neg]) ).
cnf(c_118,negated_conjecture,
( in(set_difference(cast_as_carrier_subset(sK0),sK7(A)),sK6)
| in(sK7(A),A) ),
inference(split_conjunct,[status(thm)],[sk_s1_xboole_0__e2_37_1_1__pre_topc__1_neg]) ).
cnf(c_119,negated_conjecture,
( ~ in(set_difference(cast_as_carrier_subset(sK0),sK7(A)),sK6)
| ~ in(sK7(A),powerset(the_carrier(sK0)))
| ~ in(sK7(A),A) ),
inference(split_conjunct,[status(thm)],[sk_s1_xboole_0__e2_37_1_1__pre_topc__1_neg]) ).
cnf(c_120,negated_conjecture,
( ~ in(set_difference(cast_as_carrier_subset(sK0),B),A)
| C != B
| ~ in(C,powerset(the_carrier(sK0)))
| in(B,sK3(sK0,A))
| sK1(sK0,A) != sK2(sK0,A)
| ~ element(A,powerset(powerset(the_carrier(sK0))))
| ~ top_str(sK0) ),
inference(resolve,[status(thm)],[c_37,c_38]) ).
cnf(c_121,negated_conjecture,
( ~ in(set_difference(cast_as_carrier_subset(sK0),B),A)
| C != B
| ~ in(C,powerset(the_carrier(sK0)))
| in(B,sK3(sK0,A))
| sK1(sK0,A) != sK2(sK0,A)
| ~ element(A,powerset(powerset(the_carrier(sK0)))) ),
inference(resolve,[status(thm)],[c_115,c_120]) ).
cnf(c_122,negated_conjecture,
( in(set_difference(cast_as_carrier_subset(sK0),B),A)
| ~ in(B,sK3(sK0,A))
| sK1(sK0,A) != sK2(sK0,A)
| ~ element(A,powerset(powerset(the_carrier(sK0))))
| ~ top_str(sK0) ),
inference(resolve,[status(thm)],[c_37,c_39]) ).
cnf(c_123,negated_conjecture,
( in(set_difference(cast_as_carrier_subset(sK0),B),A)
| ~ in(B,sK3(sK0,A))
| sK1(sK0,A) != sK2(sK0,A)
| ~ element(A,powerset(powerset(the_carrier(sK0)))) ),
inference(resolve,[status(thm)],[c_115,c_122]) ).
cnf(c_124,negated_conjecture,
( sK4(sK0,A,B) = B
| ~ in(B,sK3(sK0,A))
| sK1(sK0,A) != sK2(sK0,A)
| ~ element(A,powerset(powerset(the_carrier(sK0))))
| ~ top_str(sK0) ),
inference(resolve,[status(thm)],[c_37,c_40]) ).
cnf(c_125,negated_conjecture,
( sK4(sK0,A,B) = B
| ~ in(B,sK3(sK0,A))
| sK1(sK0,A) != sK2(sK0,A)
| ~ element(A,powerset(powerset(the_carrier(sK0)))) ),
inference(resolve,[status(thm)],[c_115,c_124]) ).
cnf(c_126,negated_conjecture,
( in(sK4(sK0,A,B),powerset(the_carrier(sK0)))
| ~ in(B,sK3(sK0,A))
| sK1(sK0,A) != sK2(sK0,A)
| ~ element(A,powerset(powerset(the_carrier(sK0))))
| ~ top_str(sK0) ),
inference(resolve,[status(thm)],[c_37,c_41]) ).
cnf(c_127,negated_conjecture,
( in(sK4(sK0,A,B),powerset(the_carrier(sK0)))
| ~ in(B,sK3(sK0,A))
| sK1(sK0,A) != sK2(sK0,A)
| ~ element(A,powerset(powerset(the_carrier(sK0)))) ),
inference(resolve,[status(thm)],[c_115,c_126]) ).
cnf(c_136,negated_conjecture,
( ~ in(set_difference(cast_as_carrier_subset(sK0),B),A)
| C != B
| ~ in(C,powerset(the_carrier(sK0)))
| in(B,sK3(sK0,A))
| sK1(sK0,A) = sK5(sK0,A)
| ~ element(A,powerset(powerset(the_carrier(sK0))))
| ~ top_str(sK0) ),
inference(resolve,[status(thm)],[c_37,c_46]) ).
cnf(c_137,negated_conjecture,
( ~ in(set_difference(cast_as_carrier_subset(sK0),B),A)
| C != B
| ~ in(C,powerset(the_carrier(sK0)))
| in(B,sK3(sK0,A))
| sK1(sK0,A) = sK5(sK0,A)
| ~ element(A,powerset(powerset(the_carrier(sK0)))) ),
inference(resolve,[status(thm)],[c_115,c_136]) ).
cnf(c_138,negated_conjecture,
( in(set_difference(cast_as_carrier_subset(sK0),B),A)
| ~ in(B,sK3(sK0,A))
| sK1(sK0,A) = sK5(sK0,A)
| ~ element(A,powerset(powerset(the_carrier(sK0))))
| ~ top_str(sK0) ),
inference(resolve,[status(thm)],[c_37,c_47]) ).
cnf(c_139,negated_conjecture,
( in(set_difference(cast_as_carrier_subset(sK0),B),A)
| ~ in(B,sK3(sK0,A))
| sK1(sK0,A) = sK5(sK0,A)
| ~ element(A,powerset(powerset(the_carrier(sK0)))) ),
inference(resolve,[status(thm)],[c_115,c_138]) ).
cnf(c_140,negated_conjecture,
( sK4(sK0,A,B) = B
| ~ in(B,sK3(sK0,A))
| sK1(sK0,A) = sK5(sK0,A)
| ~ element(A,powerset(powerset(the_carrier(sK0))))
| ~ top_str(sK0) ),
inference(resolve,[status(thm)],[c_37,c_48]) ).
cnf(c_141,negated_conjecture,
( sK4(sK0,A,B) = B
| ~ in(B,sK3(sK0,A))
| sK1(sK0,A) = sK5(sK0,A)
| ~ element(A,powerset(powerset(the_carrier(sK0)))) ),
inference(resolve,[status(thm)],[c_115,c_140]) ).
cnf(c_142,negated_conjecture,
( in(sK4(sK0,A,B),powerset(the_carrier(sK0)))
| ~ in(B,sK3(sK0,A))
| sK1(sK0,A) = sK5(sK0,A)
| ~ element(A,powerset(powerset(the_carrier(sK0))))
| ~ top_str(sK0) ),
inference(resolve,[status(thm)],[c_37,c_49]) ).
cnf(c_143,negated_conjecture,
( in(sK4(sK0,A,B),powerset(the_carrier(sK0)))
| ~ in(B,sK3(sK0,A))
| sK1(sK0,A) = sK5(sK0,A)
| ~ element(A,powerset(powerset(the_carrier(sK0)))) ),
inference(resolve,[status(thm)],[c_115,c_142]) ).
cnf(c_152,negated_conjecture,
( ~ in(set_difference(cast_as_carrier_subset(sK0),B),A)
| C != B
| ~ in(C,powerset(the_carrier(sK0)))
| in(B,sK3(sK0,A))
| sK5(sK0,A) = sK2(sK0,A)
| ~ element(A,powerset(powerset(the_carrier(sK0))))
| ~ top_str(sK0) ),
inference(resolve,[status(thm)],[c_37,c_54]) ).
cnf(c_1007,negated_conjecture,
( ~ in(set_difference(cast_as_carrier_subset(sK0),B),A)
| C != B
| ~ in(C,powerset(the_carrier(sK0)))
| in(B,sK3(sK0,A))
| sK2(sK0,A) = sK5(sK0,A)
| ~ element(A,powerset(powerset(the_carrier(sK0))))
| ~ top_str(sK0) ),
inference(copy,[status(thm)],[c_152]) ).
cnf(c_153,negated_conjecture,
( ~ in(set_difference(cast_as_carrier_subset(sK0),B),A)
| C != B
| ~ in(C,powerset(the_carrier(sK0)))
| in(B,sK3(sK0,A))
| sK2(sK0,A) = sK5(sK0,A)
| ~ element(A,powerset(powerset(the_carrier(sK0)))) ),
inference(resolve,[status(thm)],[c_115,c_1007]) ).
cnf(c_154,negated_conjecture,
( in(set_difference(cast_as_carrier_subset(sK0),B),A)
| ~ in(B,sK3(sK0,A))
| sK5(sK0,A) = sK2(sK0,A)
| ~ element(A,powerset(powerset(the_carrier(sK0))))
| ~ top_str(sK0) ),
inference(resolve,[status(thm)],[c_37,c_55]) ).
cnf(c_1008,negated_conjecture,
( in(set_difference(cast_as_carrier_subset(sK0),B),A)
| ~ in(B,sK3(sK0,A))
| sK2(sK0,A) = sK5(sK0,A)
| ~ element(A,powerset(powerset(the_carrier(sK0))))
| ~ top_str(sK0) ),
inference(copy,[status(thm)],[c_154]) ).
cnf(c_155,negated_conjecture,
( in(set_difference(cast_as_carrier_subset(sK0),B),A)
| ~ in(B,sK3(sK0,A))
| sK2(sK0,A) = sK5(sK0,A)
| ~ element(A,powerset(powerset(the_carrier(sK0)))) ),
inference(resolve,[status(thm)],[c_115,c_1008]) ).
cnf(c_156,negated_conjecture,
( sK4(sK0,A,B) = B
| ~ in(B,sK3(sK0,A))
| sK5(sK0,A) = sK2(sK0,A)
| ~ element(A,powerset(powerset(the_carrier(sK0))))
| ~ top_str(sK0) ),
inference(resolve,[status(thm)],[c_37,c_56]) ).
cnf(c_1009,negated_conjecture,
( sK4(sK0,A,B) = B
| ~ in(B,sK3(sK0,A))
| sK2(sK0,A) = sK5(sK0,A)
| ~ element(A,powerset(powerset(the_carrier(sK0))))
| ~ top_str(sK0) ),
inference(copy,[status(thm)],[c_156]) ).
cnf(c_157,negated_conjecture,
( sK4(sK0,A,B) = B
| ~ in(B,sK3(sK0,A))
| sK2(sK0,A) = sK5(sK0,A)
| ~ element(A,powerset(powerset(the_carrier(sK0)))) ),
inference(resolve,[status(thm)],[c_115,c_1009]) ).
cnf(c_158,negated_conjecture,
( in(sK4(sK0,A,B),powerset(the_carrier(sK0)))
| ~ in(B,sK3(sK0,A))
| sK5(sK0,A) = sK2(sK0,A)
| ~ element(A,powerset(powerset(the_carrier(sK0))))
| ~ top_str(sK0) ),
inference(resolve,[status(thm)],[c_37,c_57]) ).
cnf(c_1010,negated_conjecture,
( in(sK4(sK0,A,B),powerset(the_carrier(sK0)))
| ~ in(B,sK3(sK0,A))
| sK2(sK0,A) = sK5(sK0,A)
| ~ element(A,powerset(powerset(the_carrier(sK0))))
| ~ top_str(sK0) ),
inference(copy,[status(thm)],[c_158]) ).
cnf(c_159,negated_conjecture,
( in(sK4(sK0,A,B),powerset(the_carrier(sK0)))
| ~ in(B,sK3(sK0,A))
| sK2(sK0,A) = sK5(sK0,A)
| ~ element(A,powerset(powerset(the_carrier(sK0)))) ),
inference(resolve,[status(thm)],[c_115,c_1010]) ).
cnf(c_234,plain,
( ~ in(set_difference(cast_as_carrier_subset(sK0),A),sK6)
| B != A
| ~ in(B,powerset(the_carrier(sK0)))
| in(A,sK3(sK0,sK6))
| sK1(sK0,sK6) != sK2(sK0,sK6) ),
inference(resolve,[status(thm)],[c_121,c_116]) ).
cnf(c_240,plain,
( in(set_difference(cast_as_carrier_subset(sK0),A),sK6)
| ~ in(A,sK3(sK0,sK6))
| sK1(sK0,sK6) != sK2(sK0,sK6) ),
inference(resolve,[status(thm)],[c_123,c_116]) ).
cnf(c_243,plain,
( sK4(sK0,sK6,A) = A
| ~ in(A,sK3(sK0,sK6))
| sK1(sK0,sK6) != sK2(sK0,sK6) ),
inference(resolve,[status(thm)],[c_125,c_116]) ).
cnf(c_246,plain,
( in(sK4(sK0,sK6,A),powerset(the_carrier(sK0)))
| ~ in(A,sK3(sK0,sK6))
| sK1(sK0,sK6) != sK2(sK0,sK6) ),
inference(resolve,[status(thm)],[c_127,c_116]) ).
cnf(c_264,plain,
( ~ in(set_difference(cast_as_carrier_subset(sK0),A),sK6)
| B != A
| ~ in(B,powerset(the_carrier(sK0)))
| in(A,sK3(sK0,sK6))
| sK1(sK0,sK6) = sK5(sK0,sK6) ),
inference(resolve,[status(thm)],[c_137,c_116]) ).
cnf(c_267,plain,
( in(set_difference(cast_as_carrier_subset(sK0),A),sK6)
| ~ in(A,sK3(sK0,sK6))
| sK1(sK0,sK6) = sK5(sK0,sK6) ),
inference(resolve,[status(thm)],[c_139,c_116]) ).
cnf(c_270,plain,
( sK4(sK0,sK6,A) = A
| ~ in(A,sK3(sK0,sK6))
| sK1(sK0,sK6) = sK5(sK0,sK6) ),
inference(resolve,[status(thm)],[c_141,c_116]) ).
cnf(c_273,plain,
( in(sK4(sK0,sK6,A),powerset(the_carrier(sK0)))
| ~ in(A,sK3(sK0,sK6))
| sK1(sK0,sK6) = sK5(sK0,sK6) ),
inference(resolve,[status(thm)],[c_143,c_116]) ).
cnf(c_291,plain,
( ~ in(set_difference(cast_as_carrier_subset(sK0),A),sK6)
| B != A
| ~ in(B,powerset(the_carrier(sK0)))
| in(A,sK3(sK0,sK6))
| sK2(sK0,sK6) = sK5(sK0,sK6) ),
inference(resolve,[status(thm)],[c_153,c_116]) ).
cnf(c_294,plain,
( in(set_difference(cast_as_carrier_subset(sK0),A),sK6)
| ~ in(A,sK3(sK0,sK6))
| sK2(sK0,sK6) = sK5(sK0,sK6) ),
inference(resolve,[status(thm)],[c_155,c_116]) ).
cnf(c_297,plain,
( sK4(sK0,sK6,A) = A
| ~ in(A,sK3(sK0,sK6))
| sK2(sK0,sK6) = sK5(sK0,sK6) ),
inference(resolve,[status(thm)],[c_157,c_116]) ).
cnf(c_300,plain,
( in(sK4(sK0,sK6,A),powerset(the_carrier(sK0)))
| ~ in(A,sK3(sK0,sK6))
| sK2(sK0,sK6) = sK5(sK0,sK6) ),
inference(resolve,[status(thm)],[c_159,c_116]) ).
cnf(c_425,plain,
( in(sK7(B),B)
| ~ in(set_difference(cast_as_carrier_subset(sK0),A),sK6)
| sK7(B) != A
| in(A,sK3(sK0,sK6))
| sK1(sK0,sK6) != sK2(sK0,sK6) ),
inference(resolve,[status(thm)],[c_234,c_117]) ).
cnf(c_435,plain,
( in(sK7(sK3(sK0,sK6)),powerset(the_carrier(sK0)))
| sK4(sK0,sK6,sK7(sK3(sK0,sK6))) = sK7(sK3(sK0,sK6))
| sK1(sK0,sK6) != sK2(sK0,sK6) ),
inference(resolve,[status(thm)],[c_243,c_117]) ).
cnf(c_528,plain,
( in(sK7(B),B)
| ~ in(set_difference(cast_as_carrier_subset(sK0),A),sK6)
| sK7(B) != A
| in(A,sK3(sK0,sK6))
| sK1(sK0,sK6) = sK5(sK0,sK6) ),
inference(resolve,[status(thm)],[c_264,c_117]) ).
cnf(c_604,plain,
( in(sK7(B),B)
| ~ in(set_difference(cast_as_carrier_subset(sK0),A),sK6)
| sK7(B) != A
| in(A,sK3(sK0,sK6))
| sK2(sK0,sK6) = sK5(sK0,sK6) ),
inference(resolve,[status(thm)],[c_291,c_117]) ).
cnf(c_608,plain,
( in(sK7(A),A)
| in(sK7(B),B)
| sK7(B) != sK7(A)
| in(sK7(A),sK3(sK0,sK6))
| sK1(sK0,sK6) != sK2(sK0,sK6) ),
inference(resolve,[status(thm)],[c_425,c_118]) ).
cnf(c_1011,plain,
( in(sK7(sK3(sK0,sK6)),sK3(sK0,sK6))
| sK7(sK3(sK0,sK6)) != sK7(sK3(sK0,sK6))
| in(sK7(sK3(sK0,sK6)),sK3(sK0,sK6))
| sK1(sK0,sK6) != sK2(sK0,sK6) ),
inference(factor,[status(thm)],[c_608]) ).
cnf(c_1012,plain,
( in(sK7(sK3(sK0,sK6)),sK3(sK0,sK6))
| in(sK7(sK3(sK0,sK6)),sK3(sK0,sK6))
| sK1(sK0,sK6) != sK2(sK0,sK6) ),
inference(copy,[status(thm)],[c_1011]) ).
cnf(c_609,plain,
( in(sK7(sK3(sK0,sK6)),sK3(sK0,sK6))
| sK1(sK0,sK6) != sK2(sK0,sK6) ),
inference(copy,[status(thm)],[c_1012]) ).
cnf(c_625,plain,
( in(sK7(A),A)
| in(sK7(B),B)
| sK7(B) != sK7(A)
| in(sK7(A),sK3(sK0,sK6))
| sK1(sK0,sK6) = sK5(sK0,sK6) ),
inference(resolve,[status(thm)],[c_528,c_118]) ).
cnf(c_1013,plain,
( in(sK7(sK3(sK0,sK6)),sK3(sK0,sK6))
| sK7(sK3(sK0,sK6)) != sK7(sK3(sK0,sK6))
| in(sK7(sK3(sK0,sK6)),sK3(sK0,sK6))
| sK1(sK0,sK6) = sK5(sK0,sK6) ),
inference(factor,[status(thm)],[c_625]) ).
cnf(c_1014,plain,
( in(sK7(sK3(sK0,sK6)),sK3(sK0,sK6))
| in(sK7(sK3(sK0,sK6)),sK3(sK0,sK6))
| sK1(sK0,sK6) = sK5(sK0,sK6) ),
inference(copy,[status(thm)],[c_1013]) ).
cnf(c_626,plain,
( in(sK7(sK3(sK0,sK6)),sK3(sK0,sK6))
| sK1(sK0,sK6) = sK5(sK0,sK6) ),
inference(copy,[status(thm)],[c_1014]) ).
cnf(c_1015,plain,
( in(sK4(sK0,sK6,sK7(sK3(sK0,sK6))),powerset(the_carrier(sK0)))
| sK1(sK0,sK6) = sK5(sK0,sK6)
| sK1(sK0,sK6) = sK5(sK0,sK6) ),
inference(resolve,[status(thm)],[c_626,c_273]) ).
cnf(c_666,plain,
( in(sK4(sK0,sK6,sK7(sK3(sK0,sK6))),powerset(the_carrier(sK0)))
| sK1(sK0,sK6) = sK5(sK0,sK6) ),
inference(copy,[status(thm)],[c_1015]) ).
cnf(c_1016,plain,
( sK4(sK0,sK6,sK7(sK3(sK0,sK6))) = sK7(sK3(sK0,sK6))
| sK1(sK0,sK6) = sK5(sK0,sK6)
| sK1(sK0,sK6) = sK5(sK0,sK6) ),
inference(resolve,[status(thm)],[c_626,c_270]) ).
cnf(c_667,plain,
( sK4(sK0,sK6,sK7(sK3(sK0,sK6))) = sK7(sK3(sK0,sK6))
| sK1(sK0,sK6) = sK5(sK0,sK6) ),
inference(copy,[status(thm)],[c_1016]) ).
cnf(c_1017,plain,
( in(set_difference(cast_as_carrier_subset(sK0),sK7(sK3(sK0,sK6))),sK6)
| sK1(sK0,sK6) = sK5(sK0,sK6)
| sK1(sK0,sK6) = sK5(sK0,sK6) ),
inference(resolve,[status(thm)],[c_626,c_267]) ).
cnf(c_668,plain,
( in(set_difference(cast_as_carrier_subset(sK0),sK7(sK3(sK0,sK6))),sK6)
| sK1(sK0,sK6) = sK5(sK0,sK6) ),
inference(copy,[status(thm)],[c_1017]) ).
cnf(c_720,plain,
( ~ in(sK7(sK3(sK0,sK6)),powerset(the_carrier(sK0)))
| ~ in(sK7(sK3(sK0,sK6)),sK3(sK0,sK6))
| sK1(sK0,sK6) = sK5(sK0,sK6) ),
inference(resolve,[status(thm)],[c_668,c_119]) ).
cnf(c_1018,plain,
( in(sK7(sK3(sK0,sK6)),powerset(the_carrier(sK0)))
| sK1(sK0,sK6) = sK5(sK0,sK6)
| sK1(sK0,sK6) = sK5(sK0,sK6) ),
inference(paramod,[status(thm)],[c_667,c_666]) ).
cnf(c_745,plain,
( in(sK7(sK3(sK0,sK6)),powerset(the_carrier(sK0)))
| sK1(sK0,sK6) = sK5(sK0,sK6) ),
inference(copy,[status(thm)],[c_1018]) ).
cnf(c_1019,plain,
( ~ in(sK7(sK3(sK0,sK6)),sK3(sK0,sK6))
| sK1(sK0,sK6) = sK5(sK0,sK6)
| sK1(sK0,sK6) = sK5(sK0,sK6) ),
inference(resolve,[status(thm)],[c_745,c_720]) ).
cnf(c_747,plain,
( ~ in(sK7(sK3(sK0,sK6)),sK3(sK0,sK6))
| sK1(sK0,sK6) = sK5(sK0,sK6) ),
inference(copy,[status(thm)],[c_1019]) ).
cnf(c_1020,plain,
( sK1(sK0,sK6) = sK5(sK0,sK6)
| sK1(sK0,sK6) = sK5(sK0,sK6) ),
inference(resolve,[status(thm)],[c_747,c_626]) ).
cnf(c_767,plain,
sK1(sK0,sK6) = sK5(sK0,sK6),
inference(copy,[status(thm)],[c_1020]) ).
cnf(c_1021,plain,
( in(sK7(sK3(sK0,sK6)),sK3(sK0,sK6))
| sK5(sK0,sK6) != sK2(sK0,sK6) ),
inference(paramod,[status(thm)],[c_767,c_609]) ).
cnf(c_770,plain,
( in(sK7(sK3(sK0,sK6)),sK3(sK0,sK6))
| sK2(sK0,sK6) != sK5(sK0,sK6) ),
inference(copy,[status(thm)],[c_1021]) ).
cnf(c_771,plain,
( in(sK7(A),A)
| in(sK7(B),B)
| sK7(B) != sK7(A)
| in(sK7(A),sK3(sK0,sK6))
| sK2(sK0,sK6) = sK5(sK0,sK6) ),
inference(resolve,[status(thm)],[c_604,c_118]) ).
cnf(c_1022,plain,
( in(sK7(sK3(sK0,sK6)),sK3(sK0,sK6))
| sK7(sK3(sK0,sK6)) != sK7(sK3(sK0,sK6))
| in(sK7(sK3(sK0,sK6)),sK3(sK0,sK6))
| sK2(sK0,sK6) = sK5(sK0,sK6) ),
inference(factor,[status(thm)],[c_771]) ).
cnf(c_1023,plain,
( in(sK7(sK3(sK0,sK6)),sK3(sK0,sK6))
| in(sK7(sK3(sK0,sK6)),sK3(sK0,sK6))
| sK2(sK0,sK6) = sK5(sK0,sK6) ),
inference(copy,[status(thm)],[c_1022]) ).
cnf(c_772,plain,
( in(sK7(sK3(sK0,sK6)),sK3(sK0,sK6))
| sK2(sK0,sK6) = sK5(sK0,sK6) ),
inference(copy,[status(thm)],[c_1023]) ).
cnf(c_1024,plain,
( in(sK4(sK0,sK6,sK7(sK3(sK0,sK6))),powerset(the_carrier(sK0)))
| sK2(sK0,sK6) = sK5(sK0,sK6)
| sK2(sK0,sK6) = sK5(sK0,sK6) ),
inference(resolve,[status(thm)],[c_772,c_300]) ).
cnf(c_808,plain,
( in(sK4(sK0,sK6,sK7(sK3(sK0,sK6))),powerset(the_carrier(sK0)))
| sK2(sK0,sK6) = sK5(sK0,sK6) ),
inference(copy,[status(thm)],[c_1024]) ).
cnf(c_1025,plain,
( sK4(sK0,sK6,sK7(sK3(sK0,sK6))) = sK7(sK3(sK0,sK6))
| sK2(sK0,sK6) = sK5(sK0,sK6)
| sK2(sK0,sK6) = sK5(sK0,sK6) ),
inference(resolve,[status(thm)],[c_772,c_297]) ).
cnf(c_809,plain,
( sK4(sK0,sK6,sK7(sK3(sK0,sK6))) = sK7(sK3(sK0,sK6))
| sK2(sK0,sK6) = sK5(sK0,sK6) ),
inference(copy,[status(thm)],[c_1025]) ).
cnf(c_1026,plain,
( in(set_difference(cast_as_carrier_subset(sK0),sK7(sK3(sK0,sK6))),sK6)
| sK2(sK0,sK6) = sK5(sK0,sK6)
| sK2(sK0,sK6) = sK5(sK0,sK6) ),
inference(resolve,[status(thm)],[c_772,c_294]) ).
cnf(c_810,plain,
( in(set_difference(cast_as_carrier_subset(sK0),sK7(sK3(sK0,sK6))),sK6)
| sK2(sK0,sK6) = sK5(sK0,sK6) ),
inference(copy,[status(thm)],[c_1026]) ).
cnf(c_855,plain,
( ~ in(sK7(sK3(sK0,sK6)),powerset(the_carrier(sK0)))
| ~ in(sK7(sK3(sK0,sK6)),sK3(sK0,sK6))
| sK2(sK0,sK6) = sK5(sK0,sK6) ),
inference(resolve,[status(thm)],[c_810,c_119]) ).
cnf(c_1027,plain,
( in(sK7(sK3(sK0,sK6)),powerset(the_carrier(sK0)))
| sK4(sK0,sK6,sK7(sK3(sK0,sK6))) = sK7(sK3(sK0,sK6))
| sK5(sK0,sK6) != sK2(sK0,sK6) ),
inference(paramod,[status(thm)],[c_767,c_435]) ).
cnf(c_857,plain,
( in(sK7(sK3(sK0,sK6)),powerset(the_carrier(sK0)))
| sK4(sK0,sK6,sK7(sK3(sK0,sK6))) = sK7(sK3(sK0,sK6))
| sK2(sK0,sK6) != sK5(sK0,sK6) ),
inference(copy,[status(thm)],[c_1027]) ).
cnf(c_1028,plain,
( in(sK7(sK3(sK0,sK6)),powerset(the_carrier(sK0)))
| sK2(sK0,sK6) = sK5(sK0,sK6)
| sK2(sK0,sK6) = sK5(sK0,sK6) ),
inference(paramod,[status(thm)],[c_809,c_808]) ).
cnf(c_870,plain,
( in(sK7(sK3(sK0,sK6)),powerset(the_carrier(sK0)))
| sK2(sK0,sK6) = sK5(sK0,sK6) ),
inference(copy,[status(thm)],[c_1028]) ).
cnf(c_1029,plain,
( ~ in(sK7(sK3(sK0,sK6)),sK3(sK0,sK6))
| sK2(sK0,sK6) = sK5(sK0,sK6)
| sK2(sK0,sK6) = sK5(sK0,sK6) ),
inference(resolve,[status(thm)],[c_870,c_855]) ).
cnf(c_872,plain,
( ~ in(sK7(sK3(sK0,sK6)),sK3(sK0,sK6))
| sK2(sK0,sK6) = sK5(sK0,sK6) ),
inference(copy,[status(thm)],[c_1029]) ).
cnf(c_1030,plain,
( sK2(sK0,sK6) = sK5(sK0,sK6)
| sK2(sK0,sK6) = sK5(sK0,sK6) ),
inference(resolve,[status(thm)],[c_872,c_772]) ).
cnf(c_885,plain,
sK2(sK0,sK6) = sK5(sK0,sK6),
inference(copy,[status(thm)],[c_1030]) ).
cnf(c_887,plain,
( in(sK7(sK3(sK0,sK6)),powerset(the_carrier(sK0)))
| sK4(sK0,sK6,sK7(sK3(sK0,sK6))) = sK7(sK3(sK0,sK6)) ),
inference(resolve,[status(thm)],[c_885,c_857]) ).
cnf(c_888,plain,
in(sK7(sK3(sK0,sK6)),sK3(sK0,sK6)),
inference(resolve,[status(thm)],[c_885,c_770]) ).
cnf(c_936,plain,
( in(sK4(sK0,sK6,sK7(sK3(sK0,sK6))),powerset(the_carrier(sK0)))
| sK1(sK0,sK6) != sK2(sK0,sK6) ),
inference(resolve,[status(thm)],[c_888,c_246]) ).
cnf(c_938,plain,
( in(set_difference(cast_as_carrier_subset(sK0),sK7(sK3(sK0,sK6))),sK6)
| sK1(sK0,sK6) != sK2(sK0,sK6) ),
inference(resolve,[status(thm)],[c_888,c_240]) ).
cnf(c_1031,plain,
( in(set_difference(cast_as_carrier_subset(sK0),sK7(sK3(sK0,sK6))),sK6)
| sK5(sK0,sK6) != sK2(sK0,sK6) ),
inference(paramod,[status(thm)],[c_767,c_938]) ).
cnf(c_1032,plain,
( in(set_difference(cast_as_carrier_subset(sK0),sK7(sK3(sK0,sK6))),sK6)
| sK2(sK0,sK6) != sK5(sK0,sK6) ),
inference(copy,[status(thm)],[c_1031]) ).
cnf(c_987,plain,
in(set_difference(cast_as_carrier_subset(sK0),sK7(sK3(sK0,sK6))),sK6),
inference(resolve,[status(thm)],[c_885,c_1032]) ).
cnf(c_1033,negated_conjecture,
( ~ in(sK7(sK3(sK0,sK6)),powerset(the_carrier(sK0)))
| ~ in(sK7(sK3(sK0,sK6)),sK3(sK0,sK6)) ),
inference(resolve,[status(thm)],[c_987,c_119]) ).
cnf(c_988,negated_conjecture,
~ in(sK7(sK3(sK0,sK6)),powerset(the_carrier(sK0))),
inference(resolve,[status(thm)],[c_888,c_1033]) ).
cnf(c_990,plain,
sK4(sK0,sK6,sK7(sK3(sK0,sK6))) = sK7(sK3(sK0,sK6)),
inference(resolve,[status(thm)],[c_988,c_887]) ).
cnf(c_1034,plain,
( in(sK4(sK0,sK6,sK7(sK3(sK0,sK6))),powerset(the_carrier(sK0)))
| sK5(sK0,sK6) != sK2(sK0,sK6) ),
inference(paramod,[status(thm)],[c_767,c_936]) ).
cnf(c_1035,plain,
( in(sK4(sK0,sK6,sK7(sK3(sK0,sK6))),powerset(the_carrier(sK0)))
| sK2(sK0,sK6) != sK5(sK0,sK6) ),
inference(copy,[status(thm)],[c_1034]) ).
cnf(c_991,plain,
in(sK4(sK0,sK6,sK7(sK3(sK0,sK6))),powerset(the_carrier(sK0))),
inference(resolve,[status(thm)],[c_885,c_1035]) ).
cnf(c_1036,plain,
in(sK7(sK3(sK0,sK6)),powerset(the_carrier(sK0))),
inference(paramod,[status(thm)],[c_990,c_991]) ).
cnf(c_1006,plain,
$false,
inference(resolve,[status(thm)],[c_988,c_1036]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU310+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n005.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Sat Sep 26 09:10:02 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.12/0.35 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.12/0.35 % Process 1801048 was started by sandbox on n005,
% 0.12/0.35 % Sat Sep 26 09:10:02 2026
% 0.12/0.35 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.12/0.37
% 0.12/0.37 % From the command line: assign(max_seconds, 300).
% 0.96/0.54
% 0.96/0.54 % SZS status Theorem for theBenchmark
% 0.96/0.54
% 0.96/0.54 % Proof 1 at 0.12 (+ 0.04) seconds.
% 0.96/0.54 % Length of proof is 91.
% 0.96/0.54 % Level of proof is 18.
% 0.96/0.54 % Maximum clause weight is 54.000.
% 0.96/0.54 % Given clauses 442.
% 0.96/0.54
% 0.96/0.54 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------