%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : SEU236+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 : n010.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:17 PM UTC 2026
% Result : Theorem 99.86s 25.78s
% Output : CNFRefutation 99.86s
% Verified :
% SZS Type : Refutation
% Derivation depth : 54
% Number of leaves : 13
% Syntax : Number of formulae : 144 ( 22 unt; 0 def)
% Number of atoms : 500 ( 148 equ)
% Maximal formula atoms : 14 ( 3 avg)
% Number of connectives : 542 ( 186 ~; 284 |; 51 &)
% ( 9 <=>; 11 =>; 0 <=; 1 <~>)
% Maximal formula depth : 11 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 9 ( 7 usr; 1 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 2 con; 0-3 aty)
% Number of variables : 165 ( 0 sgn 154 !; 11 ?; 35 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] :
( in(X0,X1)
=> ~ in(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',antisymmetry_r2_hidden) ).
fof(f10,axiom,
! [X0,X1] : set_union2(X0,X1) = set_union2(X1,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',commutativity_k2_xboole_0) ).
fof(f12,axiom,
! [X0,X1] :
( ( ordinal(X1)
& ordinal(X0) )
=> ( ordinal_subset(X1,X0)
| ordinal_subset(X0,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',connectedness_r1_ordinal1) ).
fof(f22,axiom,
! [X0] : succ(X0) = set_union2(X0,singleton(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d1_ordinal1) ).
fof(f25,axiom,
! [X0,X1] :
( X1 = singleton(X0)
<=> ! [X2] :
( in(X2,X1)
<=> X2 = X0 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d1_tarski) ).
fof(f32,axiom,
! [X0,X1,X2] :
( X2 = set_union2(X0,X1)
<=> ! [X3] :
( in(X3,X2)
<=> ( in(X3,X1)
| in(X3,X0) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d2_xboole_0) ).
fof(f105,axiom,
! [X0] :
( ordinal(X0)
=> ( ordinal(succ(X0))
& epsilon_connected(succ(X0))
& epsilon_transitive(succ(X0))
& ~ empty(succ(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc3_ordinal1) ).
fof(f153,axiom,
! [X0,X1] :
( ( ordinal(X1)
& ordinal(X0) )
=> ( ordinal_subset(X0,X1)
<=> subset(X0,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_r1_ordinal1) ).
fof(f158,axiom,
! [X0] : in(X0,succ(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t10_ordinal1) ).
fof(f167,axiom,
! [X0,X1] :
( subset(X0,X1)
=> set_union2(X0,X1) = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t12_xboole_1) ).
fof(f195,axiom,
! [X0] :
( ordinal(X0)
=> ! [X1] :
( ordinal(X1)
=> ~ ( ~ in(X1,X0)
& X0 != X1
& ~ in(X0,X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t24_ordinal1) ).
fof(f206,conjecture,
! [X0] :
( ordinal(X0)
=> ! [X1] :
( ordinal(X1)
=> ( in(X0,X1)
<=> ordinal_subset(succ(X0),X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t33_ordinal1) ).
fof(f207,negated_conjecture,
~ ! [X0] :
( ordinal(X0)
=> ! [X1] :
( ordinal(X1)
=> ( in(X0,X1)
<=> ordinal_subset(succ(X0),X1) ) ) ),
inference(negated_conjecture,[status(cth)],[f206]) ).
fof(f254,axiom,
! [X0] : unordered_pair(X0,X0) = singleton(X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t69_enumset1) ).
fof(f289,plain,
! [X0,X1] :
( ~ in(X0,X1)
| ~ in(X1,X0) ),
inference(ennf_transformation,[],[f1]) ).
fof(f299,plain,
! [X0,X1] :
( ~ ordinal(X1)
| ~ ordinal(X0)
| ordinal_subset(X1,X0)
| ordinal_subset(X0,X1) ),
inference(ennf_transformation,[],[f12]) ).
fof(f300,plain,
! [X0,X1] :
( ~ ordinal(X1)
| ~ ordinal(X0)
| ordinal_subset(X1,X0)
| ordinal_subset(X0,X1) ),
inference(flattening,[],[f299]) ).
fof(f363,plain,
! [X0] :
( ~ ordinal(X0)
| ( ordinal(succ(X0))
& epsilon_connected(succ(X0))
& epsilon_transitive(succ(X0))
& ~ empty(succ(X0)) ) ),
inference(ennf_transformation,[],[f105]) ).
fof(f397,plain,
! [X0,X1] :
( ~ ordinal(X1)
| ~ ordinal(X0)
| ( ordinal_subset(X0,X1)
<=> subset(X0,X1) ) ),
inference(ennf_transformation,[],[f153]) ).
fof(f398,plain,
! [X0,X1] :
( ~ ordinal(X1)
| ~ ordinal(X0)
| ( ordinal_subset(X0,X1)
<=> subset(X0,X1) ) ),
inference(flattening,[],[f397]) ).
fof(f411,plain,
! [X0,X1] :
( ~ subset(X0,X1)
| set_union2(X0,X1) = X1 ),
inference(ennf_transformation,[],[f167]) ).
fof(f450,plain,
! [X0] :
( ~ ordinal(X0)
| ! [X1] :
( ~ ordinal(X1)
| in(X1,X0)
| X0 = X1
| in(X0,X1) ) ),
inference(ennf_transformation,[],[f195]) ).
fof(f451,plain,
! [X0] :
( ~ ordinal(X0)
| ! [X1] :
( ~ ordinal(X1)
| in(X1,X0)
| X0 = X1
| in(X0,X1) ) ),
inference(flattening,[],[f450]) ).
fof(f464,plain,
? [X0] :
( ordinal(X0)
& ? [X1] :
( ordinal(X1)
& ( in(X0,X1)
<~> ordinal_subset(succ(X0),X1) ) ) ),
inference(ennf_transformation,[],[f207]) ).
fof(f578,plain,
! [X0,X1] :
( ( singleton(X0) != X1
| ! [X2] :
( ( ~ in(X2,X1)
| X2 = X0 )
& ( X0 != X2
| in(X2,X1) ) ) )
& ( ? [X2] :
( ( in(X2,X1)
| X2 = X0 )
& ( ~ in(X2,X1)
| X0 != X2 ) )
| X1 = singleton(X0) ) ),
inference(nnf_transformation,[],[f25]) ).
fof(f579,plain,
! [X0,X1] :
( ( singleton(X0) != X1
| ! [X3] :
( ( ~ in(X3,X1)
| X0 = X3 )
& ( X0 != X3
| in(X3,X1) ) ) )
& ( ? [X2] :
( ( in(X2,X1)
| X2 = X0 )
& ( ~ in(X2,X1)
| X0 != X2 ) )
| X1 = singleton(X0) ) ),
inference(rectify,[],[f578]) ).
fof(f580,plain,
! [X0,X1] :
( ( singleton(X0) != X1
| ! [X3] :
( ( ~ in(X3,X1)
| X0 = X3 )
& ( X0 != X3
| in(X3,X1) ) ) )
& ( ( ( in(sK24(X0,X1),X1)
| sK24(X0,X1) = X0 )
& ( ~ in(sK24(X0,X1),X1)
| sK24(X0,X1) != X0 ) )
| X1 = singleton(X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK24]),skolemize(X2,sK24(X0,X1))],[f579]) ).
fof(f598,plain,
! [X0,X1,X2] :
( ( set_union2(X0,X1) != X2
| ! [X3] :
( ( ~ in(X3,X2)
| in(X3,X1)
| in(X3,X0) )
& ( ( ~ in(X3,X1)
& ~ in(X3,X0) )
| in(X3,X2) ) ) )
& ( ? [X3] :
( ( in(X3,X2)
| in(X3,X1)
| in(X3,X0) )
& ( ~ in(X3,X2)
| ( ~ in(X3,X1)
& ~ in(X3,X0) ) ) )
| X2 = set_union2(X0,X1) ) ),
inference(nnf_transformation,[],[f32]) ).
fof(f599,plain,
! [X0,X1,X2] :
( ( set_union2(X0,X1) != X2
| ! [X3] :
( ( ~ in(X3,X2)
| in(X3,X1)
| in(X3,X0) )
& ( ( ~ in(X3,X1)
& ~ in(X3,X0) )
| in(X3,X2) ) ) )
& ( ? [X3] :
( ( in(X3,X2)
| in(X3,X1)
| in(X3,X0) )
& ( ~ in(X3,X2)
| ( ~ in(X3,X1)
& ~ in(X3,X0) ) ) )
| X2 = set_union2(X0,X1) ) ),
inference(flattening,[],[f598]) ).
fof(f600,plain,
! [X0,X1,X2] :
( ( set_union2(X0,X1) != X2
| ! [X4] :
( ( ~ in(X4,X2)
| in(X4,X1)
| in(X4,X0) )
& ( ( ~ in(X4,X1)
& ~ in(X4,X0) )
| in(X4,X2) ) ) )
& ( ? [X3] :
( ( in(X3,X2)
| in(X3,X1)
| in(X3,X0) )
& ( ~ in(X3,X2)
| ( ~ in(X3,X1)
& ~ in(X3,X0) ) ) )
| X2 = set_union2(X0,X1) ) ),
inference(rectify,[],[f599]) ).
fof(f601,plain,
! [X0,X1,X2] :
( ( set_union2(X0,X1) != X2
| ! [X4] :
( ( ~ in(X4,X2)
| in(X4,X1)
| in(X4,X0) )
& ( ( ~ in(X4,X1)
& ~ in(X4,X0) )
| in(X4,X2) ) ) )
& ( ( ( in(sK31(X0,X1,X2),X2)
| in(sK31(X0,X1,X2),X1)
| in(sK31(X0,X1,X2),X0) )
& ( ~ in(sK31(X0,X1,X2),X2)
| ( ~ in(sK31(X0,X1,X2),X1)
& ~ in(sK31(X0,X1,X2),X0) ) ) )
| X2 = set_union2(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK31]),skolemize(X3,sK31(X0,X1,X2))],[f600]) ).
fof(f675,plain,
! [X0,X1] :
( ~ ordinal(X1)
| ~ ordinal(X0)
| ( ( ~ ordinal_subset(X0,X1)
| subset(X0,X1) )
& ( ~ subset(X0,X1)
| ordinal_subset(X0,X1) ) ) ),
inference(nnf_transformation,[],[f398]) ).
fof(f693,plain,
? [X0] :
( ordinal(X0)
& ? [X1] :
( ordinal(X1)
& ( in(X0,X1)
| ordinal_subset(succ(X0),X1) )
& ( ~ in(X0,X1)
| ~ ordinal_subset(succ(X0),X1) ) ) ),
inference(nnf_transformation,[],[f464]) ).
fof(f694,plain,
? [X0] :
( ordinal(X0)
& ? [X1] :
( ordinal(X1)
& ( in(X0,X1)
| ordinal_subset(succ(X0),X1) )
& ( ~ in(X0,X1)
| ~ ordinal_subset(succ(X0),X1) ) ) ),
inference(flattening,[],[f693]) ).
fof(f695,plain,
( ordinal(sK87)
& ordinal(sK88)
& ( in(sK87,sK88)
| ordinal_subset(succ(sK87),sK88) )
& ( ~ in(sK87,sK88)
| ~ ordinal_subset(succ(sK87),sK88) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK87,sK88]),skolemize(X0,sK87),skolemize(X1,sK88)],[f694]) ).
fof(f733,plain,
! [X0,X1] :
( ~ in(X0,X1)
| ~ in(X1,X0) ),
inference(cnf_transformation,[],[f289]) ).
fof(f747,plain,
! [X0,X1] : set_union2(X0,X1) = set_union2(X1,X0),
inference(cnf_transformation,[],[f10]) ).
fof(f749,plain,
! [X0,X1] :
( ~ ordinal(X1)
| ~ ordinal(X0)
| ordinal_subset(X1,X0)
| ordinal_subset(X0,X1) ),
inference(cnf_transformation,[],[f300]) ).
fof(f805,plain,
! [X0] : succ(X0) = set_union2(X0,singleton(X0)),
inference(cnf_transformation,[],[f22]) ).
fof(f817,plain,
! [X3,X0,X1] :
( singleton(X0) != X1
| ~ in(X3,X1)
| X0 = X3 ),
inference(cnf_transformation,[],[f580]) ).
fof(f844,plain,
! [X2,X0,X1,X4] :
( set_union2(X0,X1) != X2
| ~ in(X4,X2)
| in(X4,X1)
| in(X4,X0) ),
inference(cnf_transformation,[],[f601]) ).
fof(f845,plain,
! [X2,X0,X1,X4] :
( set_union2(X0,X1) != X2
| ~ in(X4,X1)
| in(X4,X2) ),
inference(cnf_transformation,[],[f601]) ).
fof(f846,plain,
! [X2,X0,X1,X4] :
( set_union2(X0,X1) != X2
| ~ in(X4,X0)
| in(X4,X2) ),
inference(cnf_transformation,[],[f601]) ).
fof(f982,plain,
! [X0] :
( ~ ordinal(X0)
| ordinal(succ(X0)) ),
inference(cnf_transformation,[],[f363]) ).
fof(f1070,plain,
! [X0,X1] :
( ~ ordinal(X1)
| ~ ordinal(X0)
| ~ ordinal_subset(X0,X1)
| subset(X0,X1) ),
inference(cnf_transformation,[],[f675]) ).
fof(f1078,plain,
! [X0] : in(X0,succ(X0)),
inference(cnf_transformation,[],[f158]) ).
fof(f1090,plain,
! [X0,X1] :
( ~ subset(X0,X1)
| set_union2(X0,X1) = X1 ),
inference(cnf_transformation,[],[f411]) ).
fof(f1129,plain,
! [X0,X1] :
( ~ ordinal(X0)
| ~ ordinal(X1)
| in(X1,X0)
| X0 = X1
| in(X0,X1) ),
inference(cnf_transformation,[],[f451]) ).
fof(f1146,plain,
ordinal(sK87),
inference(cnf_transformation,[],[f695]) ).
fof(f1147,plain,
ordinal(sK88),
inference(cnf_transformation,[],[f695]) ).
fof(f1148,plain,
( in(sK87,sK88)
| ordinal_subset(succ(sK87),sK88) ),
inference(cnf_transformation,[],[f695]) ).
fof(f1149,plain,
( ~ in(sK87,sK88)
| ~ ordinal_subset(succ(sK87),sK88) ),
inference(cnf_transformation,[],[f695]) ).
fof(f1232,plain,
! [X0] : singleton(X0) = unordered_pair(X0,X0),
inference(cnf_transformation,[],[f254]) ).
fof(f1269,plain,
! [X0] : succ(X0) = set_union2(X0,unordered_pair(X0,X0)),
inference(definition_unfolding,[],[f805,f1232]) ).
fof(f1302,plain,
! [X3,X0,X1] :
( unordered_pair(X0,X0) != X1
| ~ in(X3,X1)
| X0 = X3 ),
inference(definition_unfolding,[],[f817,f1232]) ).
fof(f1349,plain,
! [X0] :
( ~ ordinal(X0)
| ordinal(set_union2(X0,unordered_pair(X0,X0))) ),
inference(definition_unfolding,[],[f982,f1269]) ).
fof(f1367,plain,
! [X0] : in(X0,set_union2(X0,unordered_pair(X0,X0))),
inference(definition_unfolding,[],[f1078,f1269]) ).
fof(f1384,plain,
( ~ in(sK87,sK88)
| ~ ordinal_subset(set_union2(sK87,unordered_pair(sK87,sK87)),sK88) ),
inference(definition_unfolding,[],[f1149,f1269]) ).
fof(f1385,plain,
( in(sK87,sK88)
| ordinal_subset(set_union2(sK87,unordered_pair(sK87,sK87)),sK88) ),
inference(definition_unfolding,[],[f1148,f1269]) ).
fof(f1454,plain,
! [X3,X0] :
( ~ in(X3,unordered_pair(X0,X0))
| X0 = X3 ),
inference(equality_resolution,[],[f1302]) ).
fof(f1465,plain,
! [X0,X1,X4] :
( ~ in(X4,X0)
| in(X4,set_union2(X0,X1)) ),
inference(equality_resolution,[],[f846]) ).
fof(f1466,plain,
! [X0,X1,X4] :
( ~ in(X4,X1)
| in(X4,set_union2(X0,X1)) ),
inference(equality_resolution,[],[f845]) ).
fof(f1467,plain,
! [X0,X1,X4] :
( ~ in(X4,set_union2(X0,X1))
| in(X4,X1)
| in(X4,X0) ),
inference(equality_resolution,[],[f844]) ).
tcf(c_49,plain,
! [X0: $i,X1: $i] :
( ~ in(X1,X0)
| ~ in(X0,X1) ),
inference(cnf_transformation,[],[f733]) ).
tcf(c_61,plain,
! [X0: $i,X1: $i] : set_union2(X0,X1) = set_union2(X1,X0),
inference(cnf_transformation,[],[f747]) ).
tcf(c_63,plain,
! [X0: $i,X1: $i] :
( ordinal_subset(X1,X0)
| ordinal_subset(X0,X1)
| ~ ordinal(X1)
| ~ ordinal(X0) ),
inference(cnf_transformation,[],[f749]) ).
tcf(c_133,plain,
! [X0: $i,X1: $i] :
( ( X0 = X1 )
| ~ in(X0,unordered_pair(X1,X1)) ),
inference(cnf_transformation,[],[f1454]) ).
tcf(c_160,plain,
! [X0: $i,X1: $i,X2: $i] :
( in(X0,set_union2(X1,X2))
| ~ in(X0,X1) ),
inference(cnf_transformation,[],[f1465]) ).
tcf(c_161,plain,
! [X0: $i,X1: $i,X2: $i] :
( in(X0,set_union2(X2,X1))
| ~ in(X0,X1) ),
inference(cnf_transformation,[],[f1466]) ).
tcf(c_162,plain,
! [X0: $i,X1: $i,X2: $i] :
( in(X0,X2)
| in(X0,X1)
| ~ in(X0,set_union2(X1,X2)) ),
inference(cnf_transformation,[],[f1467]) ).
tcf(c_297,plain,
! [X0: $i] :
( ordinal(set_union2(X0,unordered_pair(X0,X0)))
| ~ ordinal(X0) ),
inference(cnf_transformation,[],[f1349]) ).
tcf(c_383,plain,
! [X0: $i,X1: $i] :
( subset(X0,X1)
| ~ ordinal(X1)
| ~ ordinal(X0)
| ~ ordinal_subset(X0,X1) ),
inference(cnf_transformation,[],[f1070]) ).
tcf(c_390,plain,
! [X0: $i] : in(X0,set_union2(X0,unordered_pair(X0,X0))),
inference(cnf_transformation,[],[f1367]) ).
tcf(c_402,plain,
! [X0: $i,X1: $i] :
( ( set_union2(X0,X1) = X1 )
| ~ subset(X0,X1) ),
inference(cnf_transformation,[],[f1090]) ).
tcf(c_441,plain,
! [X0: $i,X1: $i] :
( in(X1,X0)
| in(X0,X1)
| ( X0 = X1 )
| ~ ordinal(X1)
| ~ ordinal(X0) ),
inference(cnf_transformation,[],[f1129]) ).
tcf(c_458,negated_conjecture,
( ~ in(sK87,sK88)
| ~ ordinal_subset(set_union2(sK87,unordered_pair(sK87,sK87)),sK88) ),
inference(cnf_transformation,[],[f1384]) ).
tcf(c_459,negated_conjecture,
( in(sK87,sK88)
| ordinal_subset(set_union2(sK87,unordered_pair(sK87,sK87)),sK88) ),
inference(cnf_transformation,[],[f1385]) ).
tcf(c_460,negated_conjecture,
ordinal(sK88),
inference(cnf_transformation,[],[f1147]) ).
tcf(c_461,negated_conjecture,
ordinal(sK87),
inference(cnf_transformation,[],[f1146]) ).
tcf(c_1152,plain,
( ordinal_subset(sK88,set_union2(sK87,unordered_pair(sK87,sK87)))
| ~ ordinal(sK88)
| ~ in(sK87,sK88)
| ~ ordinal(set_union2(sK87,unordered_pair(sK87,sK87))) ),
inference(superposition,[status(thm)],[c_63,c_458]) ).
tcf(c_1158,plain,
( ordinal_subset(sK88,set_union2(sK87,unordered_pair(sK87,sK87)))
| ~ ordinal(set_union2(sK87,unordered_pair(sK87,sK87)))
| ~ in(sK87,sK88) ),
inference(global_subsumption_just,[status(thm)],[c_1152,c_460,c_1152]) ).
tcf(c_1159,plain,
( ordinal_subset(sK88,set_union2(sK87,unordered_pair(sK87,sK87)))
| ~ in(sK87,sK88)
| ~ ordinal(set_union2(sK87,unordered_pair(sK87,sK87))) ),
inference(renaming,[status(thm)],[c_1158]) ).
tcf(c_1470,plain,
( in(sK87,sK88)
| subset(set_union2(sK87,unordered_pair(sK87,sK87)),sK88)
| ~ ordinal(sK88)
| ~ ordinal(set_union2(sK87,unordered_pair(sK87,sK87))) ),
inference(superposition,[status(thm)],[c_459,c_383]) ).
tcf(c_1471,plain,
( subset(sK88,set_union2(sK87,unordered_pair(sK87,sK87)))
| ~ ordinal(sK88)
| ~ in(sK87,sK88)
| ~ ordinal(set_union2(sK87,unordered_pair(sK87,sK87))) ),
inference(superposition,[status(thm)],[c_1159,c_383]) ).
tcf(c_1476,plain,
( in(sK87,sK88)
| subset(set_union2(sK87,unordered_pair(sK87,sK87)),sK88)
| ~ ordinal(set_union2(sK87,unordered_pair(sK87,sK87))) ),
inference(global_subsumption_just,[status(thm)],[c_1470,c_460,c_1470]) ).
tcf(c_1481,plain,
( subset(sK88,set_union2(sK87,unordered_pair(sK87,sK87)))
| ~ ordinal(set_union2(sK87,unordered_pair(sK87,sK87)))
| ~ in(sK87,sK88) ),
inference(global_subsumption_just,[status(thm)],[c_1471,c_460,c_1471]) ).
tcf(c_1482,plain,
( subset(sK88,set_union2(sK87,unordered_pair(sK87,sK87)))
| ~ in(sK87,sK88)
| ~ ordinal(set_union2(sK87,unordered_pair(sK87,sK87))) ),
inference(renaming,[status(thm)],[c_1481]) ).
tcf(c_1685,plain,
( in(sK87,sK88)
| ( set_union2(set_union2(sK87,unordered_pair(sK87,sK87)),sK88) = sK88 )
| ~ ordinal(set_union2(sK87,unordered_pair(sK87,sK87))) ),
inference(superposition,[status(thm)],[c_1476,c_402]) ).
tcf(c_1686,plain,
( ( set_union2(sK88,set_union2(sK87,unordered_pair(sK87,sK87))) = set_union2(sK87,unordered_pair(sK87,sK87)) )
| ~ in(sK87,sK88)
| ~ ordinal(set_union2(sK87,unordered_pair(sK87,sK87))) ),
inference(superposition,[status(thm)],[c_1482,c_402]) ).
tcf(c_1690,plain,
( in(sK87,sK88)
| ( set_union2(sK88,set_union2(sK87,unordered_pair(sK87,sK87))) = sK88 )
| ~ ordinal(set_union2(sK87,unordered_pair(sK87,sK87))) ),
inference(demodulation,[status(thm)],[c_1685,c_61]) ).
tcf(c_1764,plain,
( ( set_union2(sK88,set_union2(sK87,unordered_pair(sK87,sK87))) = set_union2(sK87,unordered_pair(sK87,sK87)) )
| ~ ordinal(sK87)
| ~ in(sK87,sK88) ),
inference(superposition,[status(thm)],[c_297,c_1686]) ).
tcf(c_1765,plain,
( ( set_union2(sK88,set_union2(sK87,unordered_pair(sK87,sK87))) = set_union2(sK87,unordered_pair(sK87,sK87)) )
| ~ in(sK87,sK88) ),
inference(global_subsumption_just,[status(thm)],[c_1764,c_461,c_1764]) ).
tcf(c_1795,plain,
( in(sK87,sK88)
| ( set_union2(sK88,set_union2(sK87,unordered_pair(sK87,sK87))) = sK88 )
| ~ ordinal(sK87) ),
inference(superposition,[status(thm)],[c_297,c_1690]) ).
tcf(c_1796,plain,
( in(sK87,sK88)
| ( set_union2(sK88,set_union2(sK87,unordered_pair(sK87,sK87))) = sK88 ) ),
inference(global_subsumption_just,[status(thm)],[c_1795,c_461,c_1795]) ).
tcf(c_1818,plain,
( ( set_union2(sK88,set_union2(sK87,unordered_pair(sK87,sK87))) = sK88 )
| ~ in(sK88,sK87) ),
inference(superposition,[status(thm)],[c_1796,c_49]) ).
tcf(c_1819,plain,
( ( set_union2(sK88,set_union2(sK87,unordered_pair(sK87,sK87))) = sK88 )
| ( set_union2(sK88,set_union2(sK87,unordered_pair(sK87,sK87))) = set_union2(sK87,unordered_pair(sK87,sK87)) ) ),
inference(superposition,[status(thm)],[c_1796,c_1765]) ).
tcf(c_1942,plain,
! [X0: $i] :
( in(X0,set_union2(sK87,unordered_pair(sK87,sK87)))
| ( set_union2(sK88,set_union2(sK87,unordered_pair(sK87,sK87))) = sK88 )
| ~ in(X0,sK88) ),
inference(superposition,[status(thm)],[c_1819,c_160]) ).
tcf(c_2019,plain,
! [X0: $i] :
( ( set_union2(sK88,set_union2(sK87,unordered_pair(sK87,sK87))) = sK88 )
| ~ in(X0,sK88)
| ~ in(set_union2(sK87,unordered_pair(sK87,sK87)),X0) ),
inference(superposition,[status(thm)],[c_1942,c_49]) ).
tcf(c_2020,plain,
! [X0: $i] :
( in(X0,sK87)
| in(X0,unordered_pair(sK87,sK87))
| ( set_union2(sK88,set_union2(sK87,unordered_pair(sK87,sK87))) = sK88 )
| ~ in(X0,sK88) ),
inference(superposition,[status(thm)],[c_1942,c_162]) ).
tcf(c_2083,plain,
( ( set_union2(sK88,set_union2(sK87,unordered_pair(sK87,sK87))) = sK88 )
| ~ in(set_union2(sK87,unordered_pair(sK87,sK87)),sK88) ),
inference(superposition,[status(thm)],[c_1942,c_2019]) ).
tcf(c_2292,plain,
! [X0: $i] :
( in(X0,sK87)
| ( X0 = sK87 )
| ( set_union2(sK88,set_union2(sK87,unordered_pair(sK87,sK87))) = sK88 )
| ~ in(X0,sK88) ),
inference(superposition,[status(thm)],[c_2020,c_133]) ).
tcf(c_6224,plain,
! [X0: $i] :
( in(sK88,X0)
| in(X0,sK87)
| ( X0 = sK88 )
| ( X0 = sK87 )
| ( set_union2(sK88,set_union2(sK87,unordered_pair(sK87,sK87))) = sK88 )
| ~ ordinal(sK88)
| ~ ordinal(X0) ),
inference(superposition,[status(thm)],[c_441,c_2292]) ).
tcf(c_6236,plain,
( in(sK88,set_union2(sK87,unordered_pair(sK87,sK87)))
| ( set_union2(sK87,unordered_pair(sK87,sK87)) = sK88 )
| ( set_union2(sK88,set_union2(sK87,unordered_pair(sK87,sK87))) = sK88 )
| ~ ordinal(sK88)
| ~ ordinal(set_union2(sK87,unordered_pair(sK87,sK87))) ),
inference(superposition,[status(thm)],[c_441,c_2083]) ).
tcf(c_6306,plain,
! [X0: $i] :
( in(sK88,X0)
| in(X0,sK87)
| ( X0 = sK88 )
| ( X0 = sK87 )
| ( set_union2(sK88,set_union2(sK87,unordered_pair(sK87,sK87))) = sK88 )
| ~ ordinal(X0) ),
inference(global_subsumption_just,[status(thm)],[c_6224,c_460,c_6224]) ).
tcf(c_6326,plain,
( in(sK88,set_union2(sK87,unordered_pair(sK87,sK87)))
| ( set_union2(sK87,unordered_pair(sK87,sK87)) = sK88 )
| ( set_union2(sK88,set_union2(sK87,unordered_pair(sK87,sK87))) = sK88 )
| ~ ordinal(set_union2(sK87,unordered_pair(sK87,sK87))) ),
inference(global_subsumption_just,[status(thm)],[c_6236,c_460,c_6236]) ).
tcf(c_10666,plain,
( in(sK88,sK87)
| in(sK88,unordered_pair(sK87,sK87))
| ( set_union2(sK87,unordered_pair(sK87,sK87)) = sK88 )
| ( set_union2(sK88,set_union2(sK87,unordered_pair(sK87,sK87))) = sK88 )
| ~ ordinal(set_union2(sK87,unordered_pair(sK87,sK87))) ),
inference(superposition,[status(thm)],[c_6326,c_162]) ).
tcf(c_10669,plain,
( ~ ordinal(set_union2(sK87,unordered_pair(sK87,sK87)))
| ( set_union2(sK88,set_union2(sK87,unordered_pair(sK87,sK87))) = sK88 )
| ( set_union2(sK87,unordered_pair(sK87,sK87)) = sK88 )
| in(sK88,unordered_pair(sK87,sK87)) ),
inference(global_subsumption_just,[status(thm)],[c_10666,c_1818,c_10666]) ).
tcf(c_10670,plain,
( in(sK88,unordered_pair(sK87,sK87))
| ( set_union2(sK87,unordered_pair(sK87,sK87)) = sK88 )
| ( set_union2(sK88,set_union2(sK87,unordered_pair(sK87,sK87))) = sK88 )
| ~ ordinal(set_union2(sK87,unordered_pair(sK87,sK87))) ),
inference(renaming,[status(thm)],[c_10669]) ).
tcf(c_10959,plain,
( in(sK88,unordered_pair(sK87,sK87))
| ( set_union2(sK87,unordered_pair(sK87,sK87)) = sK88 )
| ( set_union2(sK88,set_union2(sK87,unordered_pair(sK87,sK87))) = sK88 )
| ~ ordinal(sK87) ),
inference(superposition,[status(thm)],[c_297,c_10670]) ).
tcf(c_10960,plain,
( in(sK88,unordered_pair(sK87,sK87))
| ( set_union2(sK87,unordered_pair(sK87,sK87)) = sK88 )
| ( set_union2(sK88,set_union2(sK87,unordered_pair(sK87,sK87))) = sK88 ) ),
inference(global_subsumption_just,[status(thm)],[c_10959,c_461,c_10959]) ).
tcf(c_11509,plain,
( ( sK87 = sK88 )
| ( set_union2(sK87,unordered_pair(sK87,sK87)) = sK88 )
| ( set_union2(sK88,set_union2(sK87,unordered_pair(sK87,sK87))) = sK88 ) ),
inference(superposition,[status(thm)],[c_10960,c_133]) ).
tcf(c_14564,plain,
! [X0: $i,X1: $i] :
( in(sK88,X1)
| in(sK88,X0)
| in(set_union2(X0,X1),sK87)
| ( set_union2(X0,X1) = sK88 )
| ( set_union2(X0,X1) = sK87 )
| ( set_union2(sK88,set_union2(sK87,unordered_pair(sK87,sK87))) = sK88 )
| ~ ordinal(set_union2(X0,X1)) ),
inference(superposition,[status(thm)],[c_6306,c_162]) ).
tcf(c_24358,plain,
( in(sK88,sK88)
| in(sK88,set_union2(sK87,unordered_pair(sK87,sK87)))
| in(set_union2(sK87,unordered_pair(sK87,sK87)),sK87)
| ( set_union2(sK88,set_union2(sK87,unordered_pair(sK87,sK87))) = sK88 )
| ( set_union2(sK88,set_union2(sK87,unordered_pair(sK87,sK87))) = sK87 )
| ~ ordinal(set_union2(sK88,set_union2(sK87,unordered_pair(sK87,sK87)))) ),
inference(superposition,[status(thm)],[c_1819,c_14564]) ).
tcf(c_24407,plain,
( in(sK88,set_union2(sK87,unordered_pair(sK87,sK87)))
| in(set_union2(sK87,unordered_pair(sK87,sK87)),sK87)
| ( set_union2(sK88,set_union2(sK87,unordered_pair(sK87,sK87))) = sK88 )
| ( set_union2(sK88,set_union2(sK87,unordered_pair(sK87,sK87))) = sK87 )
| ~ ordinal(set_union2(sK88,set_union2(sK87,unordered_pair(sK87,sK87)))) ),
inference(forward_subsumption_resolution,[status(thm)],[c_24358,c_1942]) ).
tcf(c_24899,plain,
( in(sK88,set_union2(sK87,unordered_pair(sK87,sK87)))
| in(set_union2(sK87,unordered_pair(sK87,sK87)),sK87)
| ( set_union2(sK88,set_union2(sK87,unordered_pair(sK87,sK87))) = sK88 )
| ( set_union2(sK88,set_union2(sK87,unordered_pair(sK87,sK87))) = sK87 )
| ~ ordinal(set_union2(sK87,unordered_pair(sK87,sK87))) ),
inference(superposition,[status(thm)],[c_1819,c_24407]) ).
tcf(c_24998,plain,
( in(sK88,set_union2(sK87,unordered_pair(sK87,sK87)))
| ( set_union2(sK88,set_union2(sK87,unordered_pair(sK87,sK87))) = sK88 )
| ( set_union2(sK88,set_union2(sK87,unordered_pair(sK87,sK87))) = sK87 )
| ~ in(sK87,sK88)
| ~ ordinal(set_union2(sK87,unordered_pair(sK87,sK87))) ),
inference(superposition,[status(thm)],[c_24899,c_2019]) ).
tcf(c_25000,plain,
( in(sK88,set_union2(sK87,unordered_pair(sK87,sK87)))
| ( set_union2(sK88,set_union2(sK87,unordered_pair(sK87,sK87))) = sK88 )
| ( set_union2(sK88,set_union2(sK87,unordered_pair(sK87,sK87))) = sK87 )
| ~ ordinal(set_union2(sK87,unordered_pair(sK87,sK87))) ),
inference(global_subsumption_just,[status(thm)],[c_24998,c_1796,c_24998]) ).
tcf(c_25080,plain,
( in(sK88,sK87)
| in(sK88,unordered_pair(sK87,sK87))
| ( set_union2(sK88,set_union2(sK87,unordered_pair(sK87,sK87))) = sK88 )
| ( set_union2(sK88,set_union2(sK87,unordered_pair(sK87,sK87))) = sK87 )
| ~ ordinal(set_union2(sK87,unordered_pair(sK87,sK87))) ),
inference(superposition,[status(thm)],[c_25000,c_162]) ).
tcf(c_25083,plain,
( ~ ordinal(set_union2(sK87,unordered_pair(sK87,sK87)))
| ( set_union2(sK88,set_union2(sK87,unordered_pair(sK87,sK87))) = sK87 )
| ( set_union2(sK88,set_union2(sK87,unordered_pair(sK87,sK87))) = sK88 )
| in(sK88,unordered_pair(sK87,sK87)) ),
inference(global_subsumption_just,[status(thm)],[c_25080,c_1818,c_25080]) ).
tcf(c_25084,plain,
( in(sK88,unordered_pair(sK87,sK87))
| ( set_union2(sK88,set_union2(sK87,unordered_pair(sK87,sK87))) = sK88 )
| ( set_union2(sK88,set_union2(sK87,unordered_pair(sK87,sK87))) = sK87 )
| ~ ordinal(set_union2(sK87,unordered_pair(sK87,sK87))) ),
inference(renaming,[status(thm)],[c_25083]) ).
tcf(c_25291,plain,
( in(sK88,unordered_pair(sK87,sK87))
| ( set_union2(sK88,set_union2(sK87,unordered_pair(sK87,sK87))) = sK88 )
| ( set_union2(sK88,set_union2(sK87,unordered_pair(sK87,sK87))) = sK87 )
| ~ ordinal(sK87) ),
inference(superposition,[status(thm)],[c_297,c_25084]) ).
tcf(c_25292,plain,
( in(sK88,unordered_pair(sK87,sK87))
| ( set_union2(sK88,set_union2(sK87,unordered_pair(sK87,sK87))) = sK88 )
| ( set_union2(sK88,set_union2(sK87,unordered_pair(sK87,sK87))) = sK87 ) ),
inference(global_subsumption_just,[status(thm)],[c_25291,c_461,c_25291]) ).
tcf(c_25452,plain,
( ( sK87 = sK88 )
| ( set_union2(sK88,set_union2(sK87,unordered_pair(sK87,sK87))) = sK88 )
| ( set_union2(sK88,set_union2(sK87,unordered_pair(sK87,sK87))) = sK87 ) ),
inference(superposition,[status(thm)],[c_25292,c_133]) ).
tcf(c_25542,plain,
( ( sK87 = sK88 )
| ( set_union2(sK87,unordered_pair(sK87,sK87)) = sK87 )
| ( set_union2(sK88,set_union2(sK87,unordered_pair(sK87,sK87))) = sK88 ) ),
inference(superposition,[status(thm)],[c_25452,c_1819]) ).
tcf(c_26565,plain,
! [X0: $i] :
( in(X0,sK88)
| ( sK87 = sK88 )
| ( set_union2(sK87,unordered_pair(sK87,sK87)) = sK87 )
| ~ in(X0,set_union2(sK87,unordered_pair(sK87,sK87))) ),
inference(superposition,[status(thm)],[c_25542,c_161]) ).
tcf(c_30312,plain,
( in(sK87,sK88)
| ( sK87 = sK88 )
| ( set_union2(sK87,unordered_pair(sK87,sK87)) = sK87 ) ),
inference(superposition,[status(thm)],[c_390,c_26565]) ).
tcf(c_30496,plain,
( ( sK87 = sK88 )
| ( set_union2(sK87,unordered_pair(sK87,sK87)) = sK87 )
| ( set_union2(sK88,set_union2(sK87,unordered_pair(sK87,sK87))) = set_union2(sK87,unordered_pair(sK87,sK87)) ) ),
inference(superposition,[status(thm)],[c_30312,c_1765]) ).
tcf(c_30595,plain,
( ( sK87 = sK88 )
| ( set_union2(sK87,unordered_pair(sK87,sK87)) = sK88 )
| ( set_union2(sK87,unordered_pair(sK87,sK87)) = sK87 ) ),
inference(superposition,[status(thm)],[c_30496,c_11509]) ).
tcf(c_31074,plain,
( in(sK87,sK87)
| ( sK87 = sK88 )
| ( set_union2(sK87,unordered_pair(sK87,sK87)) = sK88 ) ),
inference(superposition,[status(thm)],[c_30595,c_390]) ).
tcf(c_33066,plain,
( ( sK87 = sK88 )
| ( set_union2(sK87,unordered_pair(sK87,sK87)) = sK88 )
| ~ in(sK87,sK87) ),
inference(superposition,[status(thm)],[c_31074,c_49]) ).
tcf(c_33067,plain,
( ( sK87 = sK88 )
| ( set_union2(sK87,unordered_pair(sK87,sK87)) = sK88 ) ),
inference(global_subsumption_just,[status(thm)],[c_33066,c_31074,c_33066]) ).
tcf(c_35568,plain,
( in(sK87,sK88)
| ( sK87 = sK88 ) ),
inference(superposition,[status(thm)],[c_33067,c_390]) ).
tcf(c_35649,plain,
( ( sK87 = sK88 )
| ~ ordinal_subset(sK88,sK88)
| ~ in(sK87,sK88) ),
inference(superposition,[status(thm)],[c_33067,c_458]) ).
tcf(c_35660,plain,
( ( sK87 = sK88 )
| ~ ordinal_subset(sK88,sK88) ),
inference(global_subsumption_just,[status(thm)],[c_35649,c_35568,c_35649]) ).
tcf(c_36784,plain,
( ordinal_subset(sK88,sK88)
| ( sK87 = sK88 )
| ~ ordinal(sK88) ),
inference(superposition,[status(thm)],[c_63,c_35660]) ).
tcf(c_36786,plain,
sK87 = sK88,
inference(global_subsumption_just,[status(thm)],[c_36784,c_460,c_35660,c_36784]) ).
tcf(c_37379,plain,
( ( set_union2(sK88,set_union2(sK87,unordered_pair(sK87,sK87))) = sK88 )
| ~ in(sK88,sK88) ),
inference(superposition,[status(thm)],[c_36786,c_1818]) ).
tcf(c_37380,plain,
( in(sK88,sK88)
| ( set_union2(sK88,set_union2(sK87,unordered_pair(sK87,sK87))) = sK88 ) ),
inference(superposition,[status(thm)],[c_36786,c_1796]) ).
tcf(c_37405,plain,
set_union2(sK88,set_union2(sK87,unordered_pair(sK87,sK87))) = sK88,
inference(global_subsumption_just,[status(thm)],[c_37379,c_37380,c_37379]) ).
tcf(c_37407,plain,
set_union2(sK88,set_union2(sK88,unordered_pair(sK88,sK88))) = sK88,
inference(light_normalisation,[status(thm)],[c_37405,c_36786]) ).
tcf(c_38117,plain,
! [X0: $i] :
( in(X0,sK88)
| ~ in(X0,set_union2(sK88,unordered_pair(sK88,sK88))) ),
inference(superposition,[status(thm)],[c_37407,c_161]) ).
tcf(c_38850,plain,
in(sK88,sK88),
inference(superposition,[status(thm)],[c_390,c_38117]) ).
tcf(c_38966,plain,
~ in(sK88,sK88),
inference(superposition,[status(thm)],[c_38850,c_49]) ).
tcf(c_38970,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_38966,c_38850]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU236+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.38 % Computer : n010.cluster.edu
% 0.10/0.38 % Model : x86_64 x86_64
% 0.10/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.38 % Memory : 8046.5625MB
% 0.10/0.38 % OS : Linux 6.8.0-71-generic
% 0.10/0.38 % CPULimit : 300
% 0.10/0.38 % WCLimit : 300
% 0.10/0.38 % DateTime : Thu Sep 24 13:21:02 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.10/0.45 Running first-order theorem proving
% 0.10/0.45 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.46
% 0.10/0.46 % ======== iProver multi-core TPTP/SMT =========
% 0.10/0.46
% 0.10/0.47 % Detected problem language: tptp
% 0.20/0.48 % Proving...
% 99.86/25.78 % SZS status Started for theBenchmark.p
% 99.86/25.78 % SZS status Theorem for theBenchmark.p
% 99.86/25.78
% 99.86/25.78 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 99.86/25.78
% 99.86/25.78 % ------ iProver source info
% 99.86/25.78
% 99.86/25.78 % git: date: 2026-07-19 20:42:38 +0200
% 99.86/25.78 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 99.86/25.78 % git: non_committed_changes: false
% 99.86/25.78
% 99.86/25.78 % ------ Parsing...
% 99.86/25.78 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 99.86/25.78
% 99.86/25.78 % ------ Preprocessing... sf_s rm: 6 0s sf_e sf_s rm: 2 0s sf_e %
% 99.86/25.78
% 99.86/25.78 % ------ Preprocessing...%
% 99.86/25.78
% 99.86/25.78 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 99.86/25.78 % ------ Proving...
% 99.86/25.78 % ------ Problem Properties
% 99.86/25.78
% 99.86/25.78 %
% 99.86/25.78 % clauses 474
% 99.86/25.78 % conjectures 4
% 99.86/25.78 % EPR 81
% 99.86/25.78 % Horn 381
% 99.86/25.78 % unary 89
% 99.86/25.78 % binary 133
% 99.86/25.78 % lits 1343
% 99.86/25.78 % lits eq 239
% 99.86/25.78 % fd_pure 0
% 99.86/25.78 % fd_pseudo 0
% 99.86/25.78 % fd_cond 17
% 99.86/25.78 % fd_pseudo_cond 92
% 99.86/25.78 % AC symbols 0
% 99.86/25.78
% 99.86/25.78 % ------ Input Options Time Limit: Unbounded
% 99.86/25.78
% 99.86/25.78
% 99.86/25.78 % ------
% 99.86/25.78 % Current options:
% 99.86/25.78 % ------
% 99.86/25.78
% 99.86/25.78
% 99.86/25.78 %
% 99.86/25.78
% 99.86/25.78 % ------ Proving...
% 99.86/25.78 %
% 99.86/25.78
% 99.86/25.78 % SZS status Theorem for theBenchmark.p
% 99.86/25.78
% 99.86/25.78 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 99.86/25.79
% 99.86/25.79
%------------------------------------------------------------------------------