%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : SEU311+2 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 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:56:36 PM UTC 2026
% Result : Theorem 154.16s 24.47s
% Output : CNFRefutation 154.16s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 11
% Syntax : Number of formulae : 129 ( 14 unt; 0 def)
% Number of atoms : 456 ( 20 equ)
% Maximal formula atoms : 10 ( 3 avg)
% Number of connectives : 552 ( 225 ~; 237 |; 61 &)
% ( 14 <=>; 13 =>; 0 <=; 2 <~>)
% Maximal formula depth : 10 ( 5 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 10 ( 8 usr; 1 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 2 con; 0-2 aty)
% Number of variables : 225 ( 0 sgn 202 !; 23 ?; 87 :)
% Comments :
%------------------------------------------------------------------------------
fof(f65,axiom,
! [X0,X1] :
( X1 = powerset(X0)
<=> ! [X2] :
( in(X2,X1)
<=> subset(X2,X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d1_zfmisc_1) ).
fof(f70,axiom,
! [X0,X1] :
( ( empty(X0)
=> ( element(X1,X0)
<=> empty(X1) ) )
& ( ~ empty(X0)
=> ( element(X1,X0)
<=> in(X1,X0) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d2_subset_1) ).
fof(f77,axiom,
! [X0] :
( one_sorted_str(X0)
=> cast_as_carrier_subset(X0) = the_carrier(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d3_pre_topc) ).
fof(f79,axiom,
! [X0,X1] :
( subset(X0,X1)
<=> ! [X2] :
( in(X2,X0)
=> in(X2,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d3_tarski) ).
fof(f160,axiom,
! [X0] :
( top_str(X0)
=> one_sorted_str(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_l1_pre_topc) ).
fof(f192,axiom,
! [X0] : ~ empty(powerset(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_subset_1) ).
fof(f320,axiom,
! [X0,X1] :
( ( element(X1,powerset(powerset(the_carrier(X0))))
& top_str(X0)
& topological_space(X0) )
=> ? [X2] :
! [X3] :
( in(X3,X2)
<=> ( in(set_difference(cast_as_carrier_subset(X0),X3),X1)
& in(X3,powerset(the_carrier(X0))) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',s1_xboole_0__e2_37_1_1__pre_topc__1) ).
fof(f330,conjecture,
! [X0,X1] :
( ( element(X1,powerset(powerset(the_carrier(X0))))
& top_str(X0)
& topological_space(X0) )
=> ? [X2] :
( ! [X3] :
( element(X3,powerset(the_carrier(X0)))
=> ( in(X3,X2)
<=> in(set_difference(cast_as_carrier_subset(X0),X3),X1) ) )
& element(X2,powerset(powerset(the_carrier(X0)))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',s3_subset_1__e2_37_1_1__pre_topc) ).
fof(f331,negated_conjecture,
~ ! [X0,X1] :
( ( element(X1,powerset(powerset(the_carrier(X0))))
& top_str(X0)
& topological_space(X0) )
=> ? [X2] :
( ! [X3] :
( element(X3,powerset(the_carrier(X0)))
=> ( in(X3,X2)
<=> in(set_difference(cast_as_carrier_subset(X0),X3),X1) ) )
& element(X2,powerset(powerset(the_carrier(X0)))) ) ),
inference(negated_conjecture,[status(cth)],[f330]) ).
fof(f376,axiom,
! [X0,X1] :
( in(X0,X1)
=> element(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t1_subset) ).
fof(f392,axiom,
! [X0,X1] :
( ordinal(X1)
=> ( in(X0,X1)
=> ordinal(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t23_ordinal1) ).
fof(f431,axiom,
! [X0,X1] :
( element(X0,powerset(X1))
<=> subset(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t3_subset) ).
fof(f577,plain,
! [X0,X1] :
( ~ element(X1,powerset(powerset(the_carrier(X0))))
| ~ top_str(X0)
| ~ topological_space(X0)
| ? [X2] :
! [X3] :
( in(X3,X2)
<=> ( in(set_difference(cast_as_carrier_subset(X0),X3),X1)
& in(X3,powerset(the_carrier(X0))) ) ) ),
inference(ennf_transformation,[],[f320]) ).
fof(f578,plain,
! [X0,X1] :
( ~ element(X1,powerset(powerset(the_carrier(X0))))
| ~ top_str(X0)
| ~ topological_space(X0)
| ? [X2] :
! [X3] :
( in(X3,X2)
<=> ( in(set_difference(cast_as_carrier_subset(X0),X3),X1)
& in(X3,powerset(the_carrier(X0))) ) ) ),
inference(flattening,[],[f577]) ).
fof(f593,plain,
? [X0,X1] :
( element(X1,powerset(powerset(the_carrier(X0))))
& top_str(X0)
& topological_space(X0)
& ! [X2] :
( ? [X3] :
( element(X3,powerset(the_carrier(X0)))
& ( in(X3,X2)
<~> in(set_difference(cast_as_carrier_subset(X0),X3),X1) ) )
| ~ element(X2,powerset(powerset(the_carrier(X0)))) ) ),
inference(ennf_transformation,[],[f331]) ).
fof(f594,plain,
? [X0,X1] :
( element(X1,powerset(powerset(the_carrier(X0))))
& top_str(X0)
& topological_space(X0)
& ! [X2] :
( ? [X3] :
( element(X3,powerset(the_carrier(X0)))
& ( in(X3,X2)
<~> in(set_difference(cast_as_carrier_subset(X0),X3),X1) ) )
| ~ element(X2,powerset(powerset(the_carrier(X0)))) ) ),
inference(flattening,[],[f593]) ).
fof(f668,plain,
! [X0,X1] :
( ~ ordinal(X1)
| ~ in(X0,X1)
| ordinal(X0) ),
inference(ennf_transformation,[],[f392]) ).
fof(f669,plain,
! [X0,X1] :
( ~ ordinal(X1)
| ~ in(X0,X1)
| ordinal(X0) ),
inference(flattening,[],[f668]) ).
fof(f819,plain,
! [X0,X1] :
( subset(X0,X1)
<=> ! [X2] :
( ~ in(X2,X0)
| in(X2,X1) ) ),
inference(ennf_transformation,[],[f79]) ).
fof(f831,plain,
! [X0,X1] :
( ~ in(X0,X1)
| element(X0,X1) ),
inference(ennf_transformation,[],[f376]) ).
fof(f832,plain,
! [X0,X1] :
( ( ~ empty(X0)
| ( element(X1,X0)
<=> empty(X1) ) )
& ( empty(X0)
| ( element(X1,X0)
<=> in(X1,X0) ) ) ),
inference(ennf_transformation,[],[f70]) ).
fof(f874,plain,
! [X0] :
( ~ one_sorted_str(X0)
| cast_as_carrier_subset(X0) = the_carrier(X0) ),
inference(ennf_transformation,[],[f77]) ).
fof(f877,plain,
! [X0] :
( ~ top_str(X0)
| one_sorted_str(X0) ),
inference(ennf_transformation,[],[f160]) ).
fof(f1150,plain,
! [X0,X1] :
( ~ element(X1,powerset(powerset(the_carrier(X0))))
| ~ top_str(X0)
| ~ topological_space(X0)
| ? [X2] :
! [X3] :
( ( ~ in(X3,X2)
| ( in(set_difference(cast_as_carrier_subset(X0),X3),X1)
& in(X3,powerset(the_carrier(X0))) ) )
& ( ~ in(set_difference(cast_as_carrier_subset(X0),X3),X1)
| ~ in(X3,powerset(the_carrier(X0)))
| in(X3,X2) ) ) ),
inference(nnf_transformation,[],[f578]) ).
fof(f1151,plain,
! [X0,X1] :
( ~ element(X1,powerset(powerset(the_carrier(X0))))
| ~ top_str(X0)
| ~ topological_space(X0)
| ? [X2] :
! [X3] :
( ( ~ in(X3,X2)
| ( in(set_difference(cast_as_carrier_subset(X0),X3),X1)
& in(X3,powerset(the_carrier(X0))) ) )
& ( ~ in(set_difference(cast_as_carrier_subset(X0),X3),X1)
| ~ in(X3,powerset(the_carrier(X0)))
| in(X3,X2) ) ) ),
inference(flattening,[],[f1150]) ).
fof(f1152,plain,
! [X0,X1] :
( ~ element(X1,powerset(powerset(the_carrier(X0))))
| ~ top_str(X0)
| ~ topological_space(X0)
| ! [X3] :
( ( ~ in(X3,sK86(X0,X1))
| ( in(set_difference(cast_as_carrier_subset(X0),X3),X1)
& in(X3,powerset(the_carrier(X0))) ) )
& ( ~ in(set_difference(cast_as_carrier_subset(X0),X3),X1)
| ~ in(X3,powerset(the_carrier(X0)))
| in(X3,sK86(X0,X1)) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK86]),skolemize(X2,sK86(X0,X1))],[f1151]) ).
fof(f1190,plain,
? [X0,X1] :
( element(X1,powerset(powerset(the_carrier(X0))))
& top_str(X0)
& topological_space(X0)
& ! [X2] :
( ? [X3] :
( element(X3,powerset(the_carrier(X0)))
& ( in(X3,X2)
| in(set_difference(cast_as_carrier_subset(X0),X3),X1) )
& ( ~ in(X3,X2)
| ~ in(set_difference(cast_as_carrier_subset(X0),X3),X1) ) )
| ~ element(X2,powerset(powerset(the_carrier(X0)))) ) ),
inference(nnf_transformation,[],[f594]) ).
fof(f1191,plain,
? [X0,X1] :
( element(X1,powerset(powerset(the_carrier(X0))))
& top_str(X0)
& topological_space(X0)
& ! [X2] :
( ? [X3] :
( element(X3,powerset(the_carrier(X0)))
& ( in(X3,X2)
| in(set_difference(cast_as_carrier_subset(X0),X3),X1) )
& ( ~ in(X3,X2)
| ~ in(set_difference(cast_as_carrier_subset(X0),X3),X1) ) )
| ~ element(X2,powerset(powerset(the_carrier(X0)))) ) ),
inference(flattening,[],[f1190]) ).
fof(f1192,plain,
( element(sK117,powerset(powerset(the_carrier(sK116))))
& top_str(sK116)
& topological_space(sK116)
& ! [X2] :
( ( element(sK118(X2),powerset(the_carrier(sK116)))
& ( in(sK118(X2),X2)
| in(set_difference(cast_as_carrier_subset(sK116),sK118(X2)),sK117) )
& ( ~ in(sK118(X2),X2)
| ~ in(set_difference(cast_as_carrier_subset(sK116),sK118(X2)),sK117) ) )
| ~ element(X2,powerset(powerset(the_carrier(sK116)))) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK116,sK117,sK118]),skolemize(X0,sK116),skolemize(X1,sK117),skolemize(X3,sK118(X2))],[f1191]) ).
fof(f1322,plain,
! [X0,X1] :
( ( ~ element(X0,powerset(X1))
| subset(X0,X1) )
& ( ~ subset(X0,X1)
| element(X0,powerset(X1)) ) ),
inference(nnf_transformation,[],[f431]) ).
fof(f1323,plain,
! [X0,X1] :
( ( ~ subset(X0,X1)
| ! [X2] :
( ~ in(X2,X0)
| in(X2,X1) ) )
& ( ? [X2] :
( in(X2,X0)
& ~ in(X2,X1) )
| subset(X0,X1) ) ),
inference(nnf_transformation,[],[f819]) ).
fof(f1324,plain,
! [X0,X1] :
( ( ~ subset(X0,X1)
| ! [X3] :
( ~ in(X3,X0)
| in(X3,X1) ) )
& ( ? [X2] :
( in(X2,X0)
& ~ in(X2,X1) )
| subset(X0,X1) ) ),
inference(rectify,[],[f1323]) ).
fof(f1325,plain,
! [X0,X1] :
( ( ~ subset(X0,X1)
| ! [X3] :
( ~ in(X3,X0)
| in(X3,X1) ) )
& ( ( in(sK190(X0,X1),X0)
& ~ in(sK190(X0,X1),X1) )
| subset(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK190]),skolemize(X2,sK190(X0,X1))],[f1324]) ).
fof(f1326,plain,
! [X0,X1] :
( ( powerset(X0) != X1
| ! [X2] :
( ( ~ in(X2,X1)
| subset(X2,X0) )
& ( ~ subset(X2,X0)
| in(X2,X1) ) ) )
& ( ? [X2] :
( ( in(X2,X1)
| subset(X2,X0) )
& ( ~ in(X2,X1)
| ~ subset(X2,X0) ) )
| X1 = powerset(X0) ) ),
inference(nnf_transformation,[],[f65]) ).
fof(f1327,plain,
! [X0,X1] :
( ( powerset(X0) != X1
| ! [X3] :
( ( ~ in(X3,X1)
| subset(X3,X0) )
& ( ~ subset(X3,X0)
| in(X3,X1) ) ) )
& ( ? [X2] :
( ( in(X2,X1)
| subset(X2,X0) )
& ( ~ in(X2,X1)
| ~ subset(X2,X0) ) )
| X1 = powerset(X0) ) ),
inference(rectify,[],[f1326]) ).
fof(f1328,plain,
! [X0,X1] :
( ( powerset(X0) != X1
| ! [X3] :
( ( ~ in(X3,X1)
| subset(X3,X0) )
& ( ~ subset(X3,X0)
| in(X3,X1) ) ) )
& ( ( ( in(sK191(X0,X1),X1)
| subset(sK191(X0,X1),X0) )
& ( ~ in(sK191(X0,X1),X1)
| ~ subset(sK191(X0,X1),X0) ) )
| X1 = powerset(X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK191]),skolemize(X2,sK191(X0,X1))],[f1327]) ).
fof(f1341,plain,
! [X0,X1] :
( ( ~ empty(X0)
| ( ( ~ element(X1,X0)
| empty(X1) )
& ( ~ empty(X1)
| element(X1,X0) ) ) )
& ( empty(X0)
| ( ( ~ element(X1,X0)
| in(X1,X0) )
& ( ~ in(X1,X0)
| element(X1,X0) ) ) ) ),
inference(nnf_transformation,[],[f832]) ).
fof(f1690,plain,
! [X3,X0,X1] :
( ~ element(X1,powerset(powerset(the_carrier(X0))))
| ~ top_str(X0)
| ~ topological_space(X0)
| ~ in(X3,sK86(X0,X1))
| in(set_difference(cast_as_carrier_subset(X0),X3),X1) ),
inference(cnf_transformation,[],[f1152]) ).
fof(f1691,plain,
! [X3,X0,X1] :
( ~ element(X1,powerset(powerset(the_carrier(X0))))
| ~ top_str(X0)
| ~ topological_space(X0)
| ~ in(X3,sK86(X0,X1))
| in(X3,powerset(the_carrier(X0))) ),
inference(cnf_transformation,[],[f1152]) ).
fof(f1692,plain,
! [X3,X0,X1] :
( ~ element(X1,powerset(powerset(the_carrier(X0))))
| ~ top_str(X0)
| ~ topological_space(X0)
| ~ in(set_difference(cast_as_carrier_subset(X0),X3),X1)
| ~ in(X3,powerset(the_carrier(X0)))
| in(X3,sK86(X0,X1)) ),
inference(cnf_transformation,[],[f1152]) ).
fof(f1757,plain,
element(sK117,powerset(powerset(the_carrier(sK116)))),
inference(cnf_transformation,[],[f1192]) ).
fof(f1758,plain,
top_str(sK116),
inference(cnf_transformation,[],[f1192]) ).
fof(f1759,plain,
topological_space(sK116),
inference(cnf_transformation,[],[f1192]) ).
fof(f1760,plain,
! [X2] :
( element(sK118(X2),powerset(the_carrier(sK116)))
| ~ element(X2,powerset(powerset(the_carrier(sK116)))) ),
inference(cnf_transformation,[],[f1192]) ).
fof(f1761,plain,
! [X2] :
( in(sK118(X2),X2)
| in(set_difference(cast_as_carrier_subset(sK116),sK118(X2)),sK117)
| ~ element(X2,powerset(powerset(the_carrier(sK116)))) ),
inference(cnf_transformation,[],[f1192]) ).
fof(f1762,plain,
! [X2] :
( ~ in(sK118(X2),X2)
| ~ in(set_difference(cast_as_carrier_subset(sK116),sK118(X2)),sK117)
| ~ element(X2,powerset(powerset(the_carrier(sK116)))) ),
inference(cnf_transformation,[],[f1192]) ).
fof(f1843,plain,
! [X0,X1] :
( ~ ordinal(X1)
| ~ in(X0,X1)
| ordinal(X0) ),
inference(cnf_transformation,[],[f669]) ).
fof(f2138,plain,
! [X0,X1] :
( ~ element(X0,powerset(X1))
| subset(X0,X1) ),
inference(cnf_transformation,[],[f1322]) ).
fof(f2139,plain,
! [X0,X1] :
( ~ subset(X0,X1)
| element(X0,powerset(X1)) ),
inference(cnf_transformation,[],[f1322]) ).
fof(f2142,plain,
! [X0,X1] :
( in(sK190(X0,X1),X0)
| subset(X0,X1) ),
inference(cnf_transformation,[],[f1325]) ).
fof(f2143,plain,
! [X0,X1] :
( ~ in(sK190(X0,X1),X1)
| subset(X0,X1) ),
inference(cnf_transformation,[],[f1325]) ).
fof(f2145,plain,
! [X3,X0,X1] :
( powerset(X0) != X1
| ~ subset(X3,X0)
| in(X3,X1) ),
inference(cnf_transformation,[],[f1328]) ).
fof(f2177,plain,
! [X0] : ~ empty(powerset(X0)),
inference(cnf_transformation,[],[f192]) ).
fof(f2179,plain,
! [X0,X1] :
( ~ in(X0,X1)
| element(X0,X1) ),
inference(cnf_transformation,[],[f831]) ).
fof(f2183,plain,
! [X0,X1] :
( empty(X0)
| ~ element(X1,X0)
| in(X1,X0) ),
inference(cnf_transformation,[],[f1341]) ).
fof(f2378,plain,
! [X0] :
( ~ one_sorted_str(X0)
| the_carrier(X0) = cast_as_carrier_subset(X0) ),
inference(cnf_transformation,[],[f874]) ).
fof(f2388,plain,
! [X0] :
( ~ top_str(X0)
| one_sorted_str(X0) ),
inference(cnf_transformation,[],[f877]) ).
fof(f3170,plain,
! [X3,X0] :
( ~ subset(X3,X0)
| in(X3,powerset(X0)) ),
inference(equality_resolution,[],[f2145]) ).
tcf(c_187,plain,
! [X0: $i,X1: $i,X2: $i] :
( in(X1,sK86(X0,X2))
| ~ top_str(X0)
| ~ topological_space(X0)
| ~ in(X1,powerset(the_carrier(X0)))
| ~ element(X2,powerset(powerset(the_carrier(X0))))
| ~ in(set_difference(cast_as_carrier_subset(X0),X1),X2) ),
inference(cnf_transformation,[],[f1692]) ).
tcf(c_188,plain,
! [X0: $i,X1: $i,X2: $i] :
( in(X2,powerset(the_carrier(X1)))
| ~ top_str(X1)
| ~ topological_space(X1)
| ~ in(X2,sK86(X1,X0))
| ~ element(X0,powerset(powerset(the_carrier(X1)))) ),
inference(cnf_transformation,[],[f1691]) ).
tcf(c_189,plain,
! [X0: $i,X1: $i,X2: $i] :
( in(set_difference(cast_as_carrier_subset(X1),X2),X0)
| ~ top_str(X1)
| ~ topological_space(X1)
| ~ in(X2,sK86(X1,X0))
| ~ element(X0,powerset(powerset(the_carrier(X1)))) ),
inference(cnf_transformation,[],[f1690]) ).
tcf(c_254,negated_conjecture,
! [X0: $i] :
( ~ in(sK118(X0),X0)
| ~ element(X0,powerset(powerset(the_carrier(sK116))))
| ~ in(set_difference(cast_as_carrier_subset(sK116),sK118(X0)),sK117) ),
inference(cnf_transformation,[],[f1762]) ).
tcf(c_255,negated_conjecture,
! [X0: $i] :
( in(sK118(X0),X0)
| in(set_difference(cast_as_carrier_subset(sK116),sK118(X0)),sK117)
| ~ element(X0,powerset(powerset(the_carrier(sK116)))) ),
inference(cnf_transformation,[],[f1761]) ).
tcf(c_256,negated_conjecture,
! [X0: $i] :
( element(sK118(X0),powerset(the_carrier(sK116)))
| ~ element(X0,powerset(powerset(the_carrier(sK116)))) ),
inference(cnf_transformation,[],[f1760]) ).
tcf(c_257,negated_conjecture,
topological_space(sK116),
inference(cnf_transformation,[],[f1759]) ).
tcf(c_258,negated_conjecture,
top_str(sK116),
inference(cnf_transformation,[],[f1758]) ).
tcf(c_259,negated_conjecture,
element(sK117,powerset(powerset(the_carrier(sK116)))),
inference(cnf_transformation,[],[f1757]) ).
tcf(c_340,plain,
! [X0: $i,X1: $i] :
( ordinal(X0)
| ~ ordinal(X1)
| ~ in(X0,X1) ),
inference(cnf_transformation,[],[f1843]) ).
tcf(c_630,plain,
! [X0: $i,X1: $i] :
( element(X0,powerset(X1))
| ~ subset(X0,X1) ),
inference(cnf_transformation,[],[f2139]) ).
tcf(c_631,plain,
! [X0: $i,X1: $i] :
( subset(X0,X1)
| ~ element(X0,powerset(X1)) ),
inference(cnf_transformation,[],[f2138]) ).
tcf(c_633,plain,
! [X0: $i,X1: $i] :
( subset(X0,X1)
| ~ in(sK190(X0,X1),X1) ),
inference(cnf_transformation,[],[f2143]) ).
tcf(c_634,plain,
! [X0: $i,X1: $i] :
( subset(X0,X1)
| in(sK190(X0,X1),X0) ),
inference(cnf_transformation,[],[f2142]) ).
tcf(c_638,plain,
! [X0: $i,X1: $i] :
( in(X0,powerset(X1))
| ~ subset(X0,X1) ),
inference(cnf_transformation,[],[f3170]) ).
tcf(c_669,plain,
! [X0: $i] : ~ empty(powerset(X0)),
inference(cnf_transformation,[],[f2177]) ).
tcf(c_671,plain,
! [X0: $i,X1: $i] :
( element(X0,X1)
| ~ in(X0,X1) ),
inference(cnf_transformation,[],[f2179]) ).
tcf(c_674,plain,
! [X0: $i,X1: $i] :
( empty(X1)
| in(X0,X1)
| ~ element(X0,X1) ),
inference(cnf_transformation,[],[f2183]) ).
tcf(c_870,plain,
! [X0: $i] :
( ( the_carrier(X0) = cast_as_carrier_subset(X0) )
| ~ one_sorted_str(X0) ),
inference(cnf_transformation,[],[f2378]) ).
tcf(c_880,plain,
! [X0: $i] :
( one_sorted_str(X0)
| ~ top_str(X0) ),
inference(cnf_transformation,[],[f2388]) ).
tcf(c_2502,plain,
! [X0: $i] :
( one_sorted_str(X0)
| ~ top_str(X0) ),
inference(prop_impl_just,[status(thm)],[c_880]) ).
tcf(c_2560,plain,
! [X0: $i] :
( ( the_carrier(X0) = cast_as_carrier_subset(X0) )
| ~ one_sorted_str(X0) ),
inference(prop_impl_just,[status(thm)],[c_870]) ).
tcf(c_20161,plain,
! [X0: $i,X1: $i,X2: $i] :
( in(X1,sK86(X0,X2))
| ~ top_str(X0)
| ~ in(X1,powerset(the_carrier(X0)))
| ~ element(X2,powerset(powerset(the_carrier(X0))))
| ~ in(set_difference(cast_as_carrier_subset(X0),X1),X2)
| ( X0 != sK116 ) ),
inference(resolution_lifted,[status(thm)],[c_187,c_257]) ).
tcf(c_20162,plain,
! [X0: $i,X1: $i] :
( in(X0,sK86(sK116,X1))
| ~ top_str(sK116)
| ~ in(X0,powerset(the_carrier(sK116)))
| ~ element(X1,powerset(powerset(the_carrier(sK116))))
| ~ in(set_difference(cast_as_carrier_subset(sK116),X0),X1) ),
inference(unflattening,[status(thm)],[c_20161]) ).
tcf(c_20164,plain,
! [X0: $i,X1: $i] :
( in(X0,sK86(sK116,X1))
| ~ in(set_difference(cast_as_carrier_subset(sK116),X0),X1)
| ~ element(X1,powerset(powerset(the_carrier(sK116))))
| ~ in(X0,powerset(the_carrier(sK116))) ),
inference(global_subsumption_just,[status(thm)],[c_20162,c_258,c_20162]) ).
tcf(c_20165,plain,
! [X0: $i,X1: $i] :
( in(X0,sK86(sK116,X1))
| ~ in(X0,powerset(the_carrier(sK116)))
| ~ element(X1,powerset(powerset(the_carrier(sK116))))
| ~ in(set_difference(cast_as_carrier_subset(sK116),X0),X1) ),
inference(renaming,[status(thm)],[c_20164]) ).
tcf(c_20233,plain,
! [X0: $i,X1: $i,X2: $i] :
( in(set_difference(cast_as_carrier_subset(X0),X2),X1)
| ~ top_str(X0)
| ~ in(X2,sK86(X0,X1))
| ~ element(X1,powerset(powerset(the_carrier(X0))))
| ( X0 != sK116 ) ),
inference(resolution_lifted,[status(thm)],[c_189,c_257]) ).
tcf(c_20234,plain,
! [X0: $i,X1: $i] :
( in(set_difference(cast_as_carrier_subset(sK116),X1),X0)
| ~ top_str(sK116)
| ~ in(X1,sK86(sK116,X0))
| ~ element(X0,powerset(powerset(the_carrier(sK116)))) ),
inference(unflattening,[status(thm)],[c_20233]) ).
tcf(c_20236,plain,
! [X0: $i,X1: $i] :
( in(set_difference(cast_as_carrier_subset(sK116),X1),X0)
| ~ element(X0,powerset(powerset(the_carrier(sK116))))
| ~ in(X1,sK86(sK116,X0)) ),
inference(global_subsumption_just,[status(thm)],[c_20234,c_258,c_20234]) ).
tcf(c_20237,plain,
! [X0: $i,X1: $i] :
( in(set_difference(cast_as_carrier_subset(sK116),X1),X0)
| ~ in(X1,sK86(sK116,X0))
| ~ element(X0,powerset(powerset(the_carrier(sK116)))) ),
inference(renaming,[status(thm)],[c_20236]) ).
tcf(c_20248,plain,
! [X0: $i,X1: $i,X2: $i] :
( in(X2,powerset(the_carrier(X0)))
| ~ top_str(X0)
| ~ in(X2,sK86(X0,X1))
| ~ element(X1,powerset(powerset(the_carrier(X0))))
| ( X0 != sK116 ) ),
inference(resolution_lifted,[status(thm)],[c_188,c_257]) ).
tcf(c_20249,plain,
! [X0: $i,X1: $i] :
( in(X1,powerset(the_carrier(sK116)))
| ~ top_str(sK116)
| ~ in(X1,sK86(sK116,X0))
| ~ element(X0,powerset(powerset(the_carrier(sK116)))) ),
inference(unflattening,[status(thm)],[c_20248]) ).
tcf(c_20251,plain,
! [X0: $i,X1: $i] :
( in(X1,powerset(the_carrier(sK116)))
| ~ element(X0,powerset(powerset(the_carrier(sK116))))
| ~ in(X1,sK86(sK116,X0)) ),
inference(global_subsumption_just,[status(thm)],[c_20249,c_258,c_20249]) ).
tcf(c_20252,plain,
! [X0: $i,X1: $i] :
( in(X1,powerset(the_carrier(sK116)))
| ~ in(X1,sK86(sK116,X0))
| ~ element(X0,powerset(powerset(the_carrier(sK116)))) ),
inference(renaming,[status(thm)],[c_20251]) ).
tcf(c_20290,plain,
! [X0: $i] :
( one_sorted_str(X0)
| ( X0 != sK116 ) ),
inference(resolution_lifted,[status(thm)],[c_2502,c_258]) ).
tcf(c_20291,plain,
one_sorted_str(sK116),
inference(unflattening,[status(thm)],[c_20290]) ).
tcf(c_21071,plain,
! [X0: $i] :
( ( the_carrier(X0) = cast_as_carrier_subset(X0) )
| ( X0 != sK116 ) ),
inference(resolution_lifted,[status(thm)],[c_2560,c_20291]) ).
tcf(c_21072,plain,
the_carrier(sK116) = cast_as_carrier_subset(sK116),
inference(unflattening,[status(thm)],[c_21071]) ).
tcf(c_53236,plain,
! [X0: $i] :
( in(sK118(X0),X0)
| in(set_difference(the_carrier(sK116),sK118(X0)),sK117)
| ~ element(X0,powerset(powerset(the_carrier(sK116)))) ),
inference(light_normalisation,[status(thm)],[c_255,c_21072]) ).
tcf(c_53286,plain,
! [X0: $i,X1: $i] :
( in(set_difference(the_carrier(sK116),X1),X0)
| ~ in(X1,sK86(sK116,X0))
| ~ element(X0,powerset(powerset(the_carrier(sK116)))) ),
inference(light_normalisation,[status(thm)],[c_20237,c_21072]) ).
tcf(c_53622,plain,
! [X0: $i] :
( ~ in(sK118(X0),X0)
| ~ element(X0,powerset(powerset(the_carrier(sK116))))
| ~ in(set_difference(the_carrier(sK116),sK118(X0)),sK117) ),
inference(light_normalisation,[status(thm)],[c_254,c_21072]) ).
tcf(c_54477,plain,
! [X0: $i,X1: $i] :
( in(X0,sK86(sK116,X1))
| ~ in(X0,powerset(the_carrier(sK116)))
| ~ element(X1,powerset(powerset(the_carrier(sK116))))
| ~ in(set_difference(the_carrier(sK116),X0),X1) ),
inference(light_normalisation,[status(thm)],[c_20165,c_21072]) ).
tcf(c_134188,plain,
! [X0: $i] :
( in(X0,powerset(the_carrier(sK116)))
| ~ in(X0,sK86(sK116,sK117)) ),
inference(superposition,[status(thm)],[c_259,c_20252]) ).
tcf(c_134304,plain,
! [X0: $i] :
( in(X0,sK86(sK116,sK117))
| ~ in(X0,powerset(the_carrier(sK116)))
| ~ in(set_difference(the_carrier(sK116),X0),sK117) ),
inference(superposition,[status(thm)],[c_259,c_54477]) ).
tcf(c_134315,plain,
! [X0: $i] :
( in(sK118(X0),X0)
| in(sK118(X0),sK86(sK116,sK117))
| ~ element(X0,powerset(powerset(the_carrier(sK116))))
| ~ in(sK118(X0),powerset(the_carrier(sK116))) ),
inference(superposition,[status(thm)],[c_53236,c_134304]) ).
tcf(c_142284,plain,
! [X0: $i] :
( in(set_difference(the_carrier(sK116),X0),sK117)
| ~ in(X0,sK86(sK116,sK117))
| ~ element(sK117,powerset(powerset(the_carrier(sK116)))) ),
inference(instantiation,[status(thm)],[c_53286]) ).
tcf(c_143438,plain,
! [X0: $i] :
( element(X0,powerset(powerset(the_carrier(sK116))))
| ~ subset(X0,powerset(the_carrier(sK116))) ),
inference(instantiation,[status(thm)],[c_630]) ).
tcf(c_144708,plain,
! [X0: $i] :
( in(sK118(X0),X0)
| in(sK118(X0),sK86(sK116,sK117))
| ~ subset(X0,powerset(the_carrier(sK116)))
| ~ in(sK118(X0),powerset(the_carrier(sK116))) ),
inference(superposition,[status(thm)],[c_630,c_134315]) ).
tcf(c_144715,plain,
! [X0: $i] :
( element(sK118(X0),powerset(the_carrier(sK116)))
| ~ subset(X0,powerset(the_carrier(sK116))) ),
inference(superposition,[status(thm)],[c_630,c_256]) ).
tcf(c_145071,plain,
! [X0: $i] :
( subset(sK86(sK116,sK117),X0)
| in(sK190(sK86(sK116,sK117),X0),powerset(the_carrier(sK116))) ),
inference(superposition,[status(thm)],[c_634,c_134188]) ).
tcf(c_151983,plain,
subset(sK86(sK116,sK117),powerset(the_carrier(sK116))),
inference(superposition,[status(thm)],[c_145071,c_633]) ).
tcf(c_152454,plain,
! [X0: $i] :
( empty(powerset(the_carrier(sK116)))
| in(sK118(X0),powerset(the_carrier(sK116)))
| ~ subset(X0,powerset(the_carrier(sK116))) ),
inference(superposition,[status(thm)],[c_144715,c_674]) ).
tcf(c_152528,plain,
! [X0: $i] :
( in(sK118(X0),powerset(the_carrier(sK116)))
| ~ subset(X0,powerset(the_carrier(sK116))) ),
inference(forward_subsumption_resolution,[status(thm)],[c_152454,c_669]) ).
tcf(c_155173,plain,
! [X0: $i] :
( subset(X0,powerset(the_carrier(sK116)))
| ~ element(X0,powerset(powerset(the_carrier(sK116)))) ),
inference(instantiation,[status(thm)],[c_631]) ).
tcf(c_155187,plain,
! [X0: $i] :
( in(X0,powerset(powerset(the_carrier(sK116))))
| ~ subset(X0,powerset(the_carrier(sK116))) ),
inference(instantiation,[status(thm)],[c_638]) ).
tcf(c_159349,plain,
! [X0: $i] :
( in(set_difference(the_carrier(sK116),X0),sK117)
| ~ in(X0,sK86(sK116,sK117)) ),
inference(superposition,[status(thm)],[c_259,c_53286]) ).
tcf(c_183325,plain,
( ~ element(sK86(sK116,sK117),powerset(powerset(the_carrier(sK116))))
| ~ in(sK118(sK86(sK116,sK117)),sK86(sK116,sK117))
| ~ in(set_difference(the_carrier(sK116),sK118(sK86(sK116,sK117))),sK117) ),
inference(instantiation,[status(thm)],[c_53622]) ).
tcf(c_183327,plain,
! [X0: $i] :
( in(set_difference(the_carrier(sK116),sK118(X0)),sK117)
| ~ element(sK117,powerset(powerset(the_carrier(sK116))))
| ~ in(sK118(X0),sK86(sK116,sK117)) ),
inference(instantiation,[status(thm)],[c_142284]) ).
tcf(c_216809,plain,
( element(sK86(sK116,sK117),powerset(powerset(the_carrier(sK116))))
| ~ subset(sK86(sK116,sK117),powerset(the_carrier(sK116))) ),
inference(instantiation,[status(thm)],[c_143438]) ).
tcf(c_217449,plain,
( in(sK86(sK116,sK117),powerset(powerset(the_carrier(sK116))))
| ~ subset(sK86(sK116,sK117),powerset(the_carrier(sK116))) ),
inference(instantiation,[status(thm)],[c_155187]) ).
tcf(c_231077,plain,
! [X0: $i] :
( ordinal(set_difference(the_carrier(sK116),X0))
| ~ ordinal(sK117)
| ~ in(X0,sK86(sK116,sK117)) ),
inference(superposition,[status(thm)],[c_159349,c_340]) ).
tcf(c_238462,plain,
( ordinal(set_difference(the_carrier(sK116),sK118(sK86(sK116,sK117))))
| in(set_difference(the_carrier(sK116),sK118(sK86(sK116,sK117))),sK117)
| ~ ordinal(sK117)
| ~ element(sK86(sK116,sK117),powerset(powerset(the_carrier(sK116)))) ),
inference(superposition,[status(thm)],[c_53236,c_231077]) ).
tcf(c_248261,plain,
( in(set_difference(the_carrier(sK116),sK118(sK86(sK116,sK117))),sK117)
| ~ element(sK117,powerset(powerset(the_carrier(sK116))))
| ~ in(sK118(sK86(sK116,sK117)),sK86(sK116,sK117)) ),
inference(instantiation,[status(thm)],[c_183327]) ).
tcf(c_248262,plain,
( in(sK118(sK86(sK116,sK117)),sK86(sK116,sK117))
| in(set_difference(the_carrier(sK116),sK118(sK86(sK116,sK117))),sK117)
| ~ element(sK86(sK116,sK117),powerset(powerset(the_carrier(sK116)))) ),
inference(instantiation,[status(thm)],[c_53236]) ).
tcf(c_266199,plain,
in(set_difference(the_carrier(sK116),sK118(sK86(sK116,sK117))),sK117),
inference(global_subsumption_just,[status(thm)],[c_238462,c_259,c_151983,c_216809,c_248262,c_248261]) ).
tcf(c_338253,plain,
! [X0: $i] :
( in(X0,sK86(sK116,sK117))
| ~ in(X0,powerset(the_carrier(sK116)))
| ~ in(set_difference(the_carrier(sK116),X0),sK117) ),
inference(resolution,[status(thm)],[c_54477,c_259]) ).
tcf(c_338260,plain,
! [X0: $i] :
( in(sK118(X0),X0)
| in(sK118(X0),sK86(sK116,sK117))
| ~ element(X0,powerset(powerset(the_carrier(sK116))))
| ~ in(sK118(X0),powerset(the_carrier(sK116))) ),
inference(resolution,[status(thm)],[c_338253,c_53236]) ).
tcf(c_338272,plain,
! [X0: $i] :
( in(sK118(X0),X0)
| in(sK118(X0),sK86(sK116,sK117))
| ~ element(X0,powerset(powerset(the_carrier(sK116)))) ),
inference(global_subsumption_just,[status(thm)],[c_338260,c_144708,c_152528,c_155173]) ).
tcf(c_345839,plain,
! [X0: $i] :
( in(sK118(X0),X0)
| in(sK118(X0),sK86(sK116,sK117))
| ~ in(X0,powerset(powerset(the_carrier(sK116)))) ),
inference(resolution,[status(thm)],[c_671,c_338272]) ).
tcf(c_346507,plain,
( in(sK118(sK86(sK116,sK117)),sK86(sK116,sK117))
| ~ in(sK86(sK116,sK117),powerset(powerset(the_carrier(sK116)))) ),
inference(factoring,[status(thm)],[c_345839]) ).
tcf(c_346508,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_346507,c_266199,c_217449,c_216809,c_183325,c_151983]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU311+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.10/0.36 % Computer : n020.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Thu Sep 24 13:39:48 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.36 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.10/0.40 Running first-order theorem proving
% 0.10/0.40 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.41
% 0.10/0.41 % ======== iProver multi-core TPTP/SMT =========
% 0.10/0.41
% 0.10/0.41 % Detected problem language: tptp
% 0.10/0.43 % Proving...
% 154.16/24.47 % SZS status Started for theBenchmark.p
% 154.16/24.47 % SZS status Theorem for theBenchmark.p
% 154.16/24.47
% 154.16/24.47 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 154.16/24.47
% 154.16/24.47 % ------ iProver source info
% 154.16/24.47
% 154.16/24.47 % git: date: 2026-07-19 20:42:38 +0200
% 154.16/24.47 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 154.16/24.47 % git: non_committed_changes: false
% 154.16/24.47
% 154.16/24.47 % ------ Parsing...
% 154.16/24.47 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 154.16/24.47
% 154.16/24.47 % ------ Preprocessing... sup_sim: 96 sf_s rm: 44 0s sf_e pe_s pe:1:0s pe:2:0s pe:4:0s pe:8:0s pe:16:0s pe_e sup_sim: 30 sf_s rm: 19 0s sf_e pe_s pe_e sup_sim: 0 sf_s rm: 19 0s sf_e pe_s pe_e %
% 154.16/24.47
% 154.16/24.47 % ------ Preprocessing... gs_s sp: 15 0s gs_e snvd_s sp: 0 0s snvd_e %
% 154.16/24.47
% 154.16/24.47 % ------ Preprocessing... sf_s rm: 3 0s sf_e sf_s rm: 0 0s sf_e
% 154.16/24.47 % ------ Proving...
% 154.16/24.47 % ------ Problem Properties
% 154.16/24.47
% 154.16/24.47 %
% 154.16/24.47 % clauses 1076
% 154.16/24.47 % conjectures 2
% 154.16/24.47 % EPR 162
% 154.16/24.47 % Horn 806
% 154.16/24.47 % unary 130
% 154.16/24.47 % binary 344
% 154.16/24.47 % lits 3209
% 154.16/24.47 % lits eq 481
% 154.16/24.47 % fd_pure 0
% 154.16/24.47 % fd_pseudo 0
% 154.16/24.47 % fd_cond 41
% 154.16/24.47 % fd_pseudo_cond 108
% 154.16/24.47 % AC symbols 0
% 154.16/24.47
% 154.16/24.47 % ------ Schedule dynamic 5 is on
% 154.16/24.47
% 154.16/24.47 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 154.16/24.47
% 154.16/24.47
% 154.16/24.47 % ------
% 154.16/24.47 % Current options:
% 154.16/24.47 % ------
% 154.16/24.47
% 154.16/24.47
% 154.16/24.47 %
% 154.16/24.47
% 154.16/24.47 % ------ Proving...
% 154.16/24.47 % Proof_search_loop: time out after: 4973 full_loop iterations
% 154.16/24.47
% 154.16/24.47 % ------ Input Options"1. --res_lit_sel adaptive --res_lit_sel_side num_symb" Time Limit: 15.
% 154.16/24.47
% 154.16/24.47
% 154.16/24.47 % ------
% 154.16/24.47 % Current options:
% 154.16/24.47 % ------
% 154.16/24.47
% 154.16/24.47
% 154.16/24.47 %
% 154.16/24.47
% 154.16/24.47 % ------ Proving...
% 154.16/24.47 %
% 154.16/24.47
% 154.16/24.47 % SZS status Theorem for theBenchmark.p
% 154.16/24.47
% 154.16/24.47 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 154.16/24.47
% 154.16/24.47
%------------------------------------------------------------------------------