%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : SEU298+1 : 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 : n012.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:31 PM UTC 2026
% Result : Theorem 7.89s 1.66s
% Output : CNFRefutation 7.89s
% Verified :
% SZS Type : Refutation
% Derivation depth : 69
% Number of leaves : 4
% Syntax : Number of formulae : 202 ( 14 unt; 1 def)
% Number of atoms : 821 ( 278 equ)
% Maximal formula atoms : 14 ( 4 avg)
% Number of connectives : 949 ( 330 ~; 492 |; 109 &)
% ( 7 <=>; 9 =>; 0 <=; 2 <~>)
% Maximal formula depth : 14 ( 5 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-2 aty)
% Number of functors : 16 ( 16 usr; 2 con; 0-3 aty)
% Number of variables : 239 ( 0 sgn 165 !; 74 ?; 64 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
! [X0,X1] :
( ( element(X1,powerset(powerset(succ(X0))))
& ordinal(X0) )
=> ? [X2] :
! [X3] :
( in(X3,X2)
<=> ( ? [X4] :
( X3 = set_difference(X4,singleton(X0))
& in(X4,X1) )
& in(X3,powerset(X0)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',s1_xboole_0__e4_27_3_1__finset_1) ).
fof(f2,negated_conjecture,
~ ! [X0,X1] :
( ( element(X1,powerset(powerset(succ(X0))))
& ordinal(X0) )
=> ? [X2] :
! [X3] :
( in(X3,X2)
<=> ( ? [X4] :
( X3 = set_difference(X4,singleton(X0))
& in(X4,X1) )
& in(X3,powerset(X0)) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f30,axiom,
! [X0,X1] :
( in(X0,X1)
=> ~ in(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',antisymmetry_r2_hidden) ).
fof(f43,axiom,
! [X0,X1] :
( ( element(X1,powerset(powerset(succ(X0))))
& ordinal(X0) )
=> ( ! [X2,X3,X4] :
( ( ? [X6] :
( X4 = set_difference(X6,singleton(X0))
& in(X6,X1) )
& X2 = X4
& ? [X5] :
( X3 = set_difference(X5,singleton(X0))
& in(X5,X1) )
& X2 = X3 )
=> X3 = X4 )
=> ? [X2] :
! [X3] :
( in(X3,X2)
<=> ? [X4] :
( ? [X7] :
( X3 = set_difference(X7,singleton(X0))
& in(X7,X1) )
& X4 = X3
& in(X4,powerset(X0)) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',s1_tarski__e4_27_3_1__finset_1__1) ).
fof(f44,plain,
! [X0,X1] :
( ( element(X1,powerset(powerset(succ(X0))))
& ordinal(X0) )
=> ( ! [X2,X3,X4] :
( ( ? [X6] :
( X4 = set_difference(X6,singleton(X0))
& in(X6,X1) )
& X2 = X4
& ? [X5] :
( X3 = set_difference(X5,singleton(X0))
& in(X5,X1) )
& X2 = X3 )
=> X3 = X4 )
=> ? [X7] :
! [X8] :
( in(X8,X7)
<=> ? [X9] :
( ? [X10] :
( set_difference(X10,singleton(X0)) = X8
& in(X10,X1) )
& X8 = X9
& in(X9,powerset(X0)) ) ) ) ),
inference(rectify,[],[f43]) ).
fof(f49,plain,
? [X0,X1] :
( element(X1,powerset(powerset(succ(X0))))
& ordinal(X0)
& ! [X2] :
? [X3] :
( in(X3,X2)
<~> ( ? [X4] :
( X3 = set_difference(X4,singleton(X0))
& in(X4,X1) )
& in(X3,powerset(X0)) ) ) ),
inference(ennf_transformation,[],[f2]) ).
fof(f50,plain,
? [X0,X1] :
( element(X1,powerset(powerset(succ(X0))))
& ordinal(X0)
& ! [X2] :
? [X3] :
( in(X3,X2)
<~> ( ? [X4] :
( X3 = set_difference(X4,singleton(X0))
& in(X4,X1) )
& in(X3,powerset(X0)) ) ) ),
inference(flattening,[],[f49]) ).
fof(f51,plain,
! [X0,X1] :
( ~ element(X1,powerset(powerset(succ(X0))))
| ~ ordinal(X0)
| ? [X2,X3,X4] :
( ? [X6] :
( X4 = set_difference(X6,singleton(X0))
& in(X6,X1) )
& X2 = X4
& ? [X5] :
( X3 = set_difference(X5,singleton(X0))
& in(X5,X1) )
& X2 = X3
& X3 != X4 )
| ? [X7] :
! [X8] :
( in(X8,X7)
<=> ? [X9] :
( ? [X10] :
( set_difference(X10,singleton(X0)) = X8
& in(X10,X1) )
& X8 = X9
& in(X9,powerset(X0)) ) ) ),
inference(ennf_transformation,[],[f44]) ).
fof(f52,plain,
! [X0,X1] :
( ~ element(X1,powerset(powerset(succ(X0))))
| ~ ordinal(X0)
| ? [X2,X3,X4] :
( ? [X6] :
( X4 = set_difference(X6,singleton(X0))
& in(X6,X1) )
& X2 = X4
& ? [X5] :
( X3 = set_difference(X5,singleton(X0))
& in(X5,X1) )
& X2 = X3
& X3 != X4 )
| ? [X7] :
! [X8] :
( in(X8,X7)
<=> ? [X9] :
( ? [X10] :
( set_difference(X10,singleton(X0)) = X8
& in(X10,X1) )
& X8 = X9
& in(X9,powerset(X0)) ) ) ),
inference(flattening,[],[f51]) ).
fof(f64,plain,
! [X0,X1] :
( ~ in(X0,X1)
| ~ in(X1,X0) ),
inference(ennf_transformation,[],[f30]) ).
fof(f77,plain,
? [X0,X1] :
( element(X1,powerset(powerset(succ(X0))))
& ordinal(X0)
& ! [X2] :
? [X3] :
( ( in(X3,X2)
| ( ? [X4] :
( X3 = set_difference(X4,singleton(X0))
& in(X4,X1) )
& in(X3,powerset(X0)) ) )
& ( ~ in(X3,X2)
| ! [X4] :
( set_difference(X4,singleton(X0)) != X3
| ~ in(X4,X1) )
| ~ in(X3,powerset(X0)) ) ) ),
inference(nnf_transformation,[],[f50]) ).
fof(f78,plain,
? [X0,X1] :
( element(X1,powerset(powerset(succ(X0))))
& ordinal(X0)
& ! [X2] :
? [X3] :
( ( in(X3,X2)
| ( ? [X4] :
( X3 = set_difference(X4,singleton(X0))
& in(X4,X1) )
& in(X3,powerset(X0)) ) )
& ( ~ in(X3,X2)
| ! [X4] :
( set_difference(X4,singleton(X0)) != X3
| ~ in(X4,X1) )
| ~ in(X3,powerset(X0)) ) ) ),
inference(flattening,[],[f77]) ).
fof(f79,plain,
? [X0,X1] :
( element(X1,powerset(powerset(succ(X0))))
& ordinal(X0)
& ! [X2] :
? [X3] :
( ( in(X3,X2)
| ( ? [X5] :
( set_difference(X5,singleton(X0)) = X3
& in(X5,X1) )
& in(X3,powerset(X0)) ) )
& ( ~ in(X3,X2)
| ! [X4] :
( set_difference(X4,singleton(X0)) != X3
| ~ in(X4,X1) )
| ~ in(X3,powerset(X0)) ) ) ),
inference(rectify,[],[f78]) ).
fof(f80,plain,
( element(sK2,powerset(powerset(succ(sK1))))
& ordinal(sK1)
& ! [X2] :
( ( in(sK3(X2),X2)
| ( sK3(X2) = set_difference(sK4(X2),singleton(sK1))
& in(sK4(X2),sK2)
& in(sK3(X2),powerset(sK1)) ) )
& ( ~ in(sK3(X2),X2)
| ! [X4] :
( sK3(X2) != set_difference(X4,singleton(sK1))
| ~ in(X4,sK2) )
| ~ in(sK3(X2),powerset(sK1)) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1,sK2,sK3,sK4]),skolemize(X0,sK1),skolemize(X1,sK2),skolemize(X3,sK3(X2)),skolemize(X5,sK4(X2))],[f79]) ).
fof(f84,plain,
! [X0,X1] :
( ~ element(X1,powerset(powerset(succ(X0))))
| ~ ordinal(X0)
| sP0(X1,X0)
| ? [X7] :
! [X8] :
( ( ~ in(X8,X7)
| ? [X9] :
( ? [X10] :
( set_difference(X10,singleton(X0)) = X8
& in(X10,X1) )
& X8 = X9
& in(X9,powerset(X0)) ) )
& ( ! [X9] :
( ! [X10] :
( set_difference(X10,singleton(X0)) != X8
| ~ in(X10,X1) )
| X8 != X9
| ~ in(X9,powerset(X0)) )
| in(X8,X7) ) ) ),
inference(nnf_transformation,[],[f76]) ).
fof(f85,plain,
! [X0,X1] :
( ~ element(X1,powerset(powerset(succ(X0))))
| ~ ordinal(X0)
| sP0(X1,X0)
| ? [X2] :
! [X3] :
( ( ~ in(X3,X2)
| ? [X6] :
( ? [X7] :
( set_difference(X7,singleton(X0)) = X3
& in(X7,X1) )
& X3 = X6
& in(X6,powerset(X0)) ) )
& ( ! [X4] :
( ! [X5] :
( set_difference(X5,singleton(X0)) != X3
| ~ in(X5,X1) )
| X3 != X4
| ~ in(X4,powerset(X0)) )
| in(X3,X2) ) ) ),
inference(rectify,[],[f84]) ).
fof(f86,plain,
! [X0,X1] :
( ~ element(X1,powerset(powerset(succ(X0))))
| ~ ordinal(X0)
| sP0(X1,X0)
| ! [X3] :
( ( ~ in(X3,sK10(X0,X1))
| ( set_difference(sK12(X0,X1,X3),singleton(X0)) = X3
& in(sK12(X0,X1,X3),X1)
& sK11(X0,X1,X3) = X3
& in(sK11(X0,X1,X3),powerset(X0)) ) )
& ( ! [X4] :
( ! [X5] :
( set_difference(X5,singleton(X0)) != X3
| ~ in(X5,X1) )
| X3 != X4
| ~ in(X4,powerset(X0)) )
| in(X3,sK10(X0,X1)) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10,sK11,sK12]),skolemize(X2,sK10(X0,X1)),skolemize(X6,sK11(X0,X1,X3)),skolemize(X7,sK12(X0,X1,X3))],[f85]) ).
fof(f103,plain,
element(sK2,powerset(powerset(succ(sK1)))),
inference(cnf_transformation,[],[f80]) ).
fof(f104,plain,
ordinal(sK1),
inference(cnf_transformation,[],[f80]) ).
fof(f105,plain,
! [X2] :
( in(sK3(X2),X2)
| sK3(X2) = set_difference(sK4(X2),singleton(sK1)) ),
inference(cnf_transformation,[],[f80]) ).
fof(f106,plain,
! [X2] :
( in(sK3(X2),X2)
| in(sK4(X2),sK2) ),
inference(cnf_transformation,[],[f80]) ).
fof(f107,plain,
! [X2] :
( in(sK3(X2),X2)
| in(sK3(X2),powerset(sK1)) ),
inference(cnf_transformation,[],[f80]) ).
fof(f108,plain,
! [X2,X4] :
( ~ in(sK3(X2),X2)
| sK3(X2) != set_difference(X4,singleton(sK1))
| ~ in(X4,sK2)
| ~ in(sK3(X2),powerset(sK1)) ),
inference(cnf_transformation,[],[f80]) ).
fof(f116,plain,
! [X3,X0,X1] :
( ~ element(X1,powerset(powerset(succ(X0))))
| ~ ordinal(X0)
| sP0(X1,X0)
| ~ in(X3,sK10(X0,X1))
| set_difference(sK12(X0,X1,X3),singleton(X0)) = X3 ),
inference(cnf_transformation,[],[f86]) ).
fof(f117,plain,
! [X3,X0,X1] :
( ~ element(X1,powerset(powerset(succ(X0))))
| ~ ordinal(X0)
| sP0(X1,X0)
| ~ in(X3,sK10(X0,X1))
| in(sK12(X0,X1,X3),X1) ),
inference(cnf_transformation,[],[f86]) ).
fof(f118,plain,
! [X3,X0,X1] :
( ~ element(X1,powerset(powerset(succ(X0))))
| ~ ordinal(X0)
| sP0(X1,X0)
| ~ in(X3,sK10(X0,X1))
| sK11(X0,X1,X3) = X3 ),
inference(cnf_transformation,[],[f86]) ).
fof(f119,plain,
! [X3,X0,X1] :
( ~ element(X1,powerset(powerset(succ(X0))))
| ~ ordinal(X0)
| sP0(X1,X0)
| ~ in(X3,sK10(X0,X1))
| in(sK11(X0,X1,X3),powerset(X0)) ),
inference(cnf_transformation,[],[f86]) ).
fof(f120,plain,
! [X3,X0,X1,X4,X5] :
( ~ element(X1,powerset(powerset(succ(X0))))
| ~ ordinal(X0)
| sP0(X1,X0)
| set_difference(X5,singleton(X0)) != X3
| ~ in(X5,X1)
| X3 != X4
| ~ in(X4,powerset(X0))
| in(X3,sK10(X0,X1)) ),
inference(cnf_transformation,[],[f86]) ).
fof(f159,plain,
! [X0,X1] :
( ~ in(X0,X1)
| ~ in(X1,X0) ),
inference(cnf_transformation,[],[f64]) ).
fof(f206,plain,
! [X0,X1,X4,X5] :
( ~ element(X1,powerset(powerset(succ(X0))))
| ~ ordinal(X0)
| sP0(X1,X0)
| set_difference(X5,singleton(X0)) != X4
| ~ in(X5,X1)
| ~ in(X4,powerset(X0))
| in(X4,sK10(X0,X1)) ),
inference(equality_resolution,[],[f120]) ).
fof(f207,plain,
! [X0,X1,X5] :
( ~ element(X1,powerset(powerset(succ(X0))))
| ~ ordinal(X0)
| sP0(X1,X0)
| ~ in(X5,X1)
| ~ in(set_difference(X5,singleton(X0)),powerset(X0))
| in(set_difference(X5,singleton(X0)),sK10(X0,X1)) ),
inference(equality_resolution,[],[f206]) ).
tcf(c_49,negated_conjecture,
! [X0: $i,X1: $i] :
( ~ in(X0,sK2)
| ~ in(sK3(X1),X1)
| ~ in(sK3(X1),powerset(sK1))
| ( set_difference(X0,singleton(sK1)) != sK3(X1) ) ),
inference(cnf_transformation,[],[f108]) ).
tcf(c_50,negated_conjecture,
! [X0: $i] :
( in(sK3(X0),X0)
| in(sK3(X0),powerset(sK1)) ),
inference(cnf_transformation,[],[f107]) ).
tcf(c_51,negated_conjecture,
! [X0: $i] :
( in(sK4(X0),sK2)
| in(sK3(X0),X0) ),
inference(cnf_transformation,[],[f106]) ).
tcf(c_52,negated_conjecture,
! [X0: $i] :
( in(sK3(X0),X0)
| ( set_difference(sK4(X0),singleton(sK1)) = sK3(X0) ) ),
inference(cnf_transformation,[],[f105]) ).
tcf(c_53,negated_conjecture,
ordinal(sK1),
inference(cnf_transformation,[],[f104]) ).
tcf(c_54,negated_conjecture,
element(sK2,powerset(powerset(succ(sK1)))),
inference(cnf_transformation,[],[f103]) ).
tcf(c_62,plain,
! [X0: $i,X1: $i,X2: $i] :
( sP0(X2,X1)
| in(set_difference(X0,singleton(X1)),sK10(X1,X2))
| ~ ordinal(X1)
| ~ in(X0,X2)
| ~ element(X2,powerset(powerset(succ(X1))))
| ~ in(set_difference(X0,singleton(X1)),powerset(X1)) ),
inference(cnf_transformation,[],[f207]) ).
tcf(c_63,plain,
! [X0: $i,X1: $i,X2: $i] :
( sP0(X0,X1)
| in(sK11(X1,X0,X2),powerset(X1))
| ~ ordinal(X1)
| ~ in(X2,sK10(X1,X0))
| ~ element(X0,powerset(powerset(succ(X1)))) ),
inference(cnf_transformation,[],[f119]) ).
tcf(c_64,plain,
! [X0: $i,X1: $i,X2: $i] :
( sP0(X0,X1)
| ( sK11(X1,X0,X2) = X2 )
| ~ ordinal(X1)
| ~ in(X2,sK10(X1,X0))
| ~ element(X0,powerset(powerset(succ(X1)))) ),
inference(cnf_transformation,[],[f118]) ).
tcf(c_65,plain,
! [X0: $i,X1: $i,X2: $i] :
( sP0(X0,X1)
| in(sK12(X1,X0,X2),X0)
| ~ ordinal(X1)
| ~ in(X2,sK10(X1,X0))
| ~ element(X0,powerset(powerset(succ(X1)))) ),
inference(cnf_transformation,[],[f117]) ).
tcf(c_66,plain,
! [X0: $i,X1: $i,X2: $i] :
( sP0(X0,X1)
| ( set_difference(sK12(X1,X0,X2),singleton(X1)) = X2 )
| ~ ordinal(X1)
| ~ in(X2,sK10(X1,X0))
| ~ element(X0,powerset(powerset(succ(X1)))) ),
inference(cnf_transformation,[],[f116]) ).
tcf(c_105,plain,
! [X0: $i,X1: $i] :
( ~ in(X1,X0)
| ~ in(X0,X1) ),
inference(cnf_transformation,[],[f159]) ).
tcf(c_4756,plain,
! [X0: $i] :
( sP0(sK2,sK1)
| in(sK12(sK1,sK2,X0),sK2)
| ~ ordinal(sK1)
| ~ in(X0,sK10(sK1,sK2)) ),
inference(superposition,[status(thm)],[c_54,c_65]) ).
tcf(c_4761,plain,
! [X0: $i] :
( sP0(sK2,sK1)
| in(sK12(sK1,sK2,X0),sK2)
| ~ in(X0,sK10(sK1,sK2)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_4756,c_53]) ).
tcf(c_4834,plain,
! [X0: $i] :
( sP0(sK2,sK1)
| ( sK11(sK1,sK2,X0) = X0 )
| ~ ordinal(sK1)
| ~ in(X0,sK10(sK1,sK2)) ),
inference(superposition,[status(thm)],[c_54,c_64]) ).
tcf(c_4839,plain,
! [X0: $i] :
( sP0(sK2,sK1)
| ( sK11(sK1,sK2,X0) = X0 )
| ~ in(X0,sK10(sK1,sK2)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_4834,c_53]) ).
tcf(c_4876,plain,
! [X0: $i] :
( sP0(sK2,sK1)
| ( set_difference(sK12(sK1,sK2,X0),singleton(sK1)) = X0 )
| ~ ordinal(sK1)
| ~ in(X0,sK10(sK1,sK2)) ),
inference(superposition,[status(thm)],[c_54,c_66]) ).
tcf(c_4881,plain,
! [X0: $i] :
( sP0(sK2,sK1)
| ( set_difference(sK12(sK1,sK2,X0),singleton(sK1)) = X0 )
| ~ in(X0,sK10(sK1,sK2)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_4876,c_53]) ).
tcf(c_4925,plain,
( sP0(sK2,sK1)
| ( sK11(sK1,sK2,sK3(sK10(sK1,sK2))) = sK3(sK10(sK1,sK2)) )
| ( set_difference(sK4(sK10(sK1,sK2)),singleton(sK1)) = sK3(sK10(sK1,sK2)) ) ),
inference(superposition,[status(thm)],[c_52,c_4839]) ).
tcf(c_4926,plain,
( sP0(sK2,sK1)
| in(sK3(sK10(sK1,sK2)),powerset(sK1))
| ( sK11(sK1,sK2,sK3(sK10(sK1,sK2))) = sK3(sK10(sK1,sK2)) ) ),
inference(superposition,[status(thm)],[c_50,c_4839]) ).
tcf(c_4927,plain,
( sP0(sK2,sK1)
| in(sK4(sK10(sK1,sK2)),sK2)
| ( sK11(sK1,sK2,sK3(sK10(sK1,sK2))) = sK3(sK10(sK1,sK2)) ) ),
inference(superposition,[status(thm)],[c_51,c_4839]) ).
tcf(c_4966,plain,
( sP0(sK2,sK1)
| ( set_difference(sK4(sK10(sK1,sK2)),singleton(sK1)) = sK3(sK10(sK1,sK2)) )
| ( set_difference(sK12(sK1,sK2,sK3(sK10(sK1,sK2))),singleton(sK1)) = sK3(sK10(sK1,sK2)) ) ),
inference(superposition,[status(thm)],[c_52,c_4881]) ).
tcf(c_4968,plain,
( sP0(sK2,sK1)
| in(sK4(sK10(sK1,sK2)),sK2)
| ( set_difference(sK12(sK1,sK2,sK3(sK10(sK1,sK2))),singleton(sK1)) = sK3(sK10(sK1,sK2)) ) ),
inference(superposition,[status(thm)],[c_51,c_4881]) ).
tcf(c_7223,plain,
! [X0: $i] :
( sP0(sK2,sK1)
| in(sK12(sK1,sK2,X0),sK2)
| ~ ordinal(sK1)
| ~ in(X0,sK10(sK1,sK2)) ),
inference(superposition,[status(thm)],[c_54,c_65]) ).
tcf(c_7228,plain,
! [X0: $i] :
( sP0(sK2,sK1)
| in(sK12(sK1,sK2,X0),sK2)
| ~ in(X0,sK10(sK1,sK2)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_7223,c_53]) ).
tcf(c_7366,plain,
( in(sK3(sK10(sK1,sK2)),sK10(sK1,sK2))
| ( set_difference(sK4(sK10(sK1,sK2)),singleton(sK1)) = sK3(sK10(sK1,sK2)) ) ),
inference(instantiation,[status(thm)],[c_52]) ).
tcf(c_7367,plain,
( in(sK4(sK10(sK1,sK2)),sK2)
| in(sK3(sK10(sK1,sK2)),sK10(sK1,sK2)) ),
inference(instantiation,[status(thm)],[c_51]) ).
tcf(c_7368,plain,
( in(sK3(sK10(sK1,sK2)),powerset(sK1))
| in(sK3(sK10(sK1,sK2)),sK10(sK1,sK2)) ),
inference(instantiation,[status(thm)],[c_50]) ).
tcf(c_8151,plain,
! [X0: $i] :
( sP0(sK2,sK1)
| ( sK11(sK1,sK2,X0) = X0 )
| ~ ordinal(sK1)
| ~ in(X0,sK10(sK1,sK2)) ),
inference(superposition,[status(thm)],[c_54,c_64]) ).
tcf(c_8156,plain,
! [X0: $i] :
( sP0(sK2,sK1)
| ( sK11(sK1,sK2,X0) = X0 )
| ~ in(X0,sK10(sK1,sK2)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_8151,c_53]) ).
tcf(c_8352,plain,
! [X0: $i] :
( sP0(sK2,sK1)
| ( set_difference(sK12(sK1,sK2,X0),singleton(sK1)) = X0 )
| ~ ordinal(sK1)
| ~ in(X0,sK10(sK1,sK2)) ),
inference(superposition,[status(thm)],[c_54,c_66]) ).
tcf(c_8357,plain,
! [X0: $i] :
( sP0(sK2,sK1)
| ( set_difference(sK12(sK1,sK2,X0),singleton(sK1)) = X0 )
| ~ in(X0,sK10(sK1,sK2)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_8352,c_53]) ).
tcf(c_8607,plain,
( sP0(sK2,sK1)
| ( sK11(sK1,sK2,sK3(sK10(sK1,sK2))) = sK3(sK10(sK1,sK2)) )
| ( set_difference(sK4(sK10(sK1,sK2)),singleton(sK1)) = sK3(sK10(sK1,sK2)) ) ),
inference(superposition,[status(thm)],[c_52,c_8156]) ).
tcf(c_8608,plain,
( sP0(sK2,sK1)
| in(sK3(sK10(sK1,sK2)),powerset(sK1))
| ( sK11(sK1,sK2,sK3(sK10(sK1,sK2))) = sK3(sK10(sK1,sK2)) ) ),
inference(superposition,[status(thm)],[c_50,c_8156]) ).
tcf(c_8612,plain,
! [X0: $i] :
( sP0(sK2,sK1)
| ( sK11(sK1,sK2,set_difference(X0,singleton(sK1))) = set_difference(X0,singleton(sK1)) )
| ~ ordinal(sK1)
| ~ in(X0,sK2)
| ~ element(sK2,powerset(powerset(succ(sK1))))
| ~ in(set_difference(X0,singleton(sK1)),powerset(sK1)) ),
inference(superposition,[status(thm)],[c_62,c_8156]) ).
tcf(c_8628,plain,
! [X0: $i] :
( sP0(sK2,sK1)
| ( sK11(sK1,sK2,set_difference(X0,singleton(sK1))) = set_difference(X0,singleton(sK1)) )
| ~ in(X0,sK2)
| ~ in(set_difference(X0,singleton(sK1)),powerset(sK1)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_8612,c_53,c_54]) ).
tcf(c_9594,plain,
( sP0(sK2,sK1)
| ( set_difference(sK4(sK10(sK1,sK2)),singleton(sK1)) = sK3(sK10(sK1,sK2)) )
| ( set_difference(sK12(sK1,sK2,sK3(sK10(sK1,sK2))),singleton(sK1)) = sK3(sK10(sK1,sK2)) ) ),
inference(superposition,[status(thm)],[c_52,c_8357]) ).
fof(f75,definition,
! [X1,X0] :
( ~ sP0(X1,X0)
| ? [X2,X3,X4] :
( ? [X6] :
( X4 = set_difference(X6,singleton(X0))
& in(X6,X1) )
& X2 = X4
& ? [X5] :
( X3 = set_difference(X5,singleton(X0))
& in(X5,X1) )
& X2 = X3
& X3 != X4 ) ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f76,plain,
! [X0,X1] :
( ~ element(X1,powerset(powerset(succ(X0))))
| ~ ordinal(X0)
| sP0(X1,X0)
| ? [X7] :
! [X8] :
( in(X8,X7)
<=> ? [X9] :
( ? [X10] :
( set_difference(X10,singleton(X0)) = X8
& in(X10,X1) )
& X8 = X9
& in(X9,powerset(X0)) ) ) ),
inference(definition_folding,[],[f52,f75]) ).
fof(f81,plain,
! [X1,X0] :
( ~ sP0(X1,X0)
| ? [X2,X3,X4] :
( ? [X6] :
( X4 = set_difference(X6,singleton(X0))
& in(X6,X1) )
& X2 = X4
& ? [X5] :
( X3 = set_difference(X5,singleton(X0))
& in(X5,X1) )
& X2 = X3
& X3 != X4 ) ),
inference(nnf_transformation,[],[f75]) ).
fof(f82,plain,
! [X0,X1] :
( ~ sP0(X0,X1)
| ? [X2,X3,X4] :
( ? [X6] :
( set_difference(X6,singleton(X1)) = X4
& in(X6,X0) )
& X2 = X4
& ? [X5] :
( set_difference(X5,singleton(X1)) = X3
& in(X5,X0) )
& X2 = X3
& X3 != X4 ) ),
inference(rectify,[],[f81]) ).
fof(f83,plain,
! [X0,X1] :
( ~ sP0(X0,X1)
| ( sK7(X0,X1) = set_difference(sK9(X0,X1),singleton(X1))
& in(sK9(X0,X1),X0)
& sK5(X0,X1) = sK7(X0,X1)
& sK6(X0,X1) = set_difference(sK8(X0,X1),singleton(X1))
& in(sK8(X0,X1),X0)
& sK5(X0,X1) = sK6(X0,X1)
& sK6(X0,X1) != sK7(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5,sK6,sK7,sK8,sK9]),skolemize(X2,sK5(X0,X1)),skolemize(X3,sK6(X0,X1)),skolemize(X4,sK7(X0,X1)),skolemize(X5,sK8(X0,X1)),skolemize(X6,sK9(X0,X1))],[f82]) ).
fof(f111,plain,
! [X0,X1] :
( ~ sP0(X0,X1)
| sK5(X0,X1) = sK7(X0,X1) ),
inference(cnf_transformation,[],[f83]) ).
fof(f114,plain,
! [X0,X1] :
( ~ sP0(X0,X1)
| sK5(X0,X1) = sK6(X0,X1) ),
inference(cnf_transformation,[],[f83]) ).
fof(f115,plain,
! [X0,X1] :
( ~ sP0(X0,X1)
| sK6(X0,X1) != sK7(X0,X1) ),
inference(cnf_transformation,[],[f83]) ).
tcf(c_55,plain,
! [X0: $i,X1: $i] :
( ~ sP0(X0,X1)
| ( sK6(X0,X1) != sK7(X0,X1) ) ),
inference(cnf_transformation,[],[f115]) ).
tcf(c_56,plain,
! [X0: $i,X1: $i] :
( ( sK6(X0,X1) = sK5(X0,X1) )
| ~ sP0(X0,X1) ),
inference(cnf_transformation,[],[f114]) ).
tcf(c_59,plain,
! [X0: $i,X1: $i] :
( ( sK7(X0,X1) = sK5(X0,X1) )
| ~ sP0(X0,X1) ),
inference(cnf_transformation,[],[f111]) ).
tcf(c_5051,plain,
( ( sK7(sK2,sK1) = sK5(sK2,sK1) )
| ( sK11(sK1,sK2,sK3(sK10(sK1,sK2))) = sK3(sK10(sK1,sK2)) )
| ( set_difference(sK4(sK10(sK1,sK2)),singleton(sK1)) = sK3(sK10(sK1,sK2)) ) ),
inference(superposition,[status(thm)],[c_4925,c_59]) ).
tcf(c_5052,plain,
( ( sK6(sK2,sK1) = sK5(sK2,sK1) )
| ( sK11(sK1,sK2,sK3(sK10(sK1,sK2))) = sK3(sK10(sK1,sK2)) )
| ( set_difference(sK4(sK10(sK1,sK2)),singleton(sK1)) = sK3(sK10(sK1,sK2)) ) ),
inference(superposition,[status(thm)],[c_4925,c_56]) ).
tcf(c_5086,plain,
( ( sK7(sK2,sK1) = sK5(sK2,sK1) )
| ( set_difference(sK4(sK10(sK1,sK2)),singleton(sK1)) = sK3(sK10(sK1,sK2)) )
| ( set_difference(sK12(sK1,sK2,sK3(sK10(sK1,sK2))),singleton(sK1)) = sK3(sK10(sK1,sK2)) ) ),
inference(superposition,[status(thm)],[c_4966,c_59]) ).
tcf(c_5087,plain,
( ( sK6(sK2,sK1) = sK5(sK2,sK1) )
| ( set_difference(sK4(sK10(sK1,sK2)),singleton(sK1)) = sK3(sK10(sK1,sK2)) )
| ( set_difference(sK12(sK1,sK2,sK3(sK10(sK1,sK2))),singleton(sK1)) = sK3(sK10(sK1,sK2)) ) ),
inference(superposition,[status(thm)],[c_4966,c_56]) ).
tcf(c_5219,plain,
( sP0(sK2,sK1)
| in(sK3(sK10(sK1,sK2)),powerset(sK1))
| ( sK7(sK2,sK1) = sK5(sK2,sK1) )
| ( set_difference(sK4(sK10(sK1,sK2)),singleton(sK1)) = sK3(sK10(sK1,sK2)) )
| ~ ordinal(sK1)
| ~ element(sK2,powerset(powerset(succ(sK1))))
| ~ in(sK3(sK10(sK1,sK2)),sK10(sK1,sK2)) ),
inference(superposition,[status(thm)],[c_5051,c_63]) ).
tcf(c_5221,plain,
( sP0(sK2,sK1)
| in(sK3(sK10(sK1,sK2)),powerset(sK1))
| ( sK7(sK2,sK1) = sK5(sK2,sK1) )
| ( set_difference(sK4(sK10(sK1,sK2)),singleton(sK1)) = sK3(sK10(sK1,sK2)) )
| ~ in(sK3(sK10(sK1,sK2)),sK10(sK1,sK2)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_5219,c_53,c_54]) ).
tcf(c_5276,plain,
( sP0(sK2,sK1)
| in(sK3(sK10(sK1,sK2)),powerset(sK1))
| ( sK6(sK2,sK1) = sK5(sK2,sK1) )
| ( set_difference(sK4(sK10(sK1,sK2)),singleton(sK1)) = sK3(sK10(sK1,sK2)) )
| ~ ordinal(sK1)
| ~ element(sK2,powerset(powerset(succ(sK1))))
| ~ in(sK3(sK10(sK1,sK2)),sK10(sK1,sK2)) ),
inference(superposition,[status(thm)],[c_5052,c_63]) ).
tcf(c_5278,plain,
( sP0(sK2,sK1)
| in(sK3(sK10(sK1,sK2)),powerset(sK1))
| ( sK6(sK2,sK1) = sK5(sK2,sK1) )
| ( set_difference(sK4(sK10(sK1,sK2)),singleton(sK1)) = sK3(sK10(sK1,sK2)) )
| ~ in(sK3(sK10(sK1,sK2)),sK10(sK1,sK2)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_5276,c_53,c_54]) ).
tcf(c_5619,plain,
( ( sK7(sK2,sK1) = sK5(sK2,sK1) )
| ~ sP0(sK2,sK1) ),
inference(instantiation,[status(thm)],[c_59]) ).
tcf(c_5620,plain,
( ( sK6(sK2,sK1) = sK5(sK2,sK1) )
| ~ sP0(sK2,sK1) ),
inference(instantiation,[status(thm)],[c_56]) ).
tcf(c_5621,plain,
( ~ sP0(sK2,sK1)
| ( sK6(sK2,sK1) != sK7(sK2,sK1) ) ),
inference(instantiation,[status(thm)],[c_55]) ).
tcf(c_5624,plain,
( ~ in(sK3(sK10(sK1,sK2)),sK10(sK1,sK2))
| ( set_difference(sK4(sK10(sK1,sK2)),singleton(sK1)) = sK3(sK10(sK1,sK2)) )
| ( sK6(sK2,sK1) = sK5(sK2,sK1) )
| in(sK3(sK10(sK1,sK2)),powerset(sK1)) ),
inference(global_subsumption_just,[status(thm)],[c_5278,c_5278,c_5620]) ).
tcf(c_5625,plain,
( in(sK3(sK10(sK1,sK2)),powerset(sK1))
| ( sK6(sK2,sK1) = sK5(sK2,sK1) )
| ( set_difference(sK4(sK10(sK1,sK2)),singleton(sK1)) = sK3(sK10(sK1,sK2)) )
| ~ in(sK3(sK10(sK1,sK2)),sK10(sK1,sK2)) ),
inference(renaming,[status(thm)],[c_5624]) ).
tcf(c_6272,plain,
! [X0: $i] :
( ( sK7(sK2,sK1) = sK5(sK2,sK1) )
| ( set_difference(sK4(sK10(sK1,sK2)),singleton(sK1)) = sK3(sK10(sK1,sK2)) )
| ~ in(sK3(X0),X0)
| ~ in(sK3(X0),powerset(sK1))
| ~ in(sK12(sK1,sK2,sK3(sK10(sK1,sK2))),sK2)
| ( sK3(sK10(sK1,sK2)) != sK3(X0) ) ),
inference(superposition,[status(thm)],[c_5086,c_49]) ).
tcf(c_6357,plain,
! [X0: $i] :
( ( sK6(sK2,sK1) = sK5(sK2,sK1) )
| ( set_difference(sK4(sK10(sK1,sK2)),singleton(sK1)) = sK3(sK10(sK1,sK2)) )
| ~ in(sK3(X0),X0)
| ~ in(sK3(X0),powerset(sK1))
| ~ in(sK12(sK1,sK2,sK3(sK10(sK1,sK2))),sK2)
| ( sK3(sK10(sK1,sK2)) != sK3(X0) ) ),
inference(superposition,[status(thm)],[c_5087,c_49]) ).
tcf(c_6858,plain,
( ( sK7(sK2,sK1) = sK5(sK2,sK1) )
| ( set_difference(sK4(sK10(sK1,sK2)),singleton(sK1)) = sK3(sK10(sK1,sK2)) )
| ~ in(sK3(sK10(sK1,sK2)),powerset(sK1))
| ~ in(sK3(sK10(sK1,sK2)),sK10(sK1,sK2))
| ~ in(sK12(sK1,sK2,sK3(sK10(sK1,sK2))),sK2) ),
inference(equality_resolution,[status(thm)],[c_6272]) ).
tcf(c_6876,plain,
( ( sK6(sK2,sK1) = sK5(sK2,sK1) )
| ( set_difference(sK4(sK10(sK1,sK2)),singleton(sK1)) = sK3(sK10(sK1,sK2)) )
| ~ in(sK3(sK10(sK1,sK2)),powerset(sK1))
| ~ in(sK3(sK10(sK1,sK2)),sK10(sK1,sK2))
| ~ in(sK12(sK1,sK2,sK3(sK10(sK1,sK2))),sK2) ),
inference(equality_resolution,[status(thm)],[c_6357]) ).
tcf(c_7581,plain,
( ( sK7(sK2,sK1) = sK5(sK2,sK1) )
| ( set_difference(sK4(sK10(sK1,sK2)),singleton(sK1)) = sK3(sK10(sK1,sK2)) )
| ~ in(sK12(sK1,sK2,sK3(sK10(sK1,sK2))),sK2) ),
inference(global_subsumption_just,[status(thm)],[c_6858,c_5221,c_5619,c_6858,c_7366]) ).
tcf(c_7589,plain,
( sP0(sK2,sK1)
| ( sK7(sK2,sK1) = sK5(sK2,sK1) )
| ( set_difference(sK4(sK10(sK1,sK2)),singleton(sK1)) = sK3(sK10(sK1,sK2)) )
| ~ in(sK3(sK10(sK1,sK2)),sK10(sK1,sK2)) ),
inference(superposition,[status(thm)],[c_4761,c_7581]) ).
tcf(c_7741,plain,
( ( set_difference(sK4(sK10(sK1,sK2)),singleton(sK1)) = sK3(sK10(sK1,sK2)) )
| ( sK7(sK2,sK1) = sK5(sK2,sK1) ) ),
inference(global_subsumption_just,[status(thm)],[c_7589,c_5619,c_7366,c_7589]) ).
tcf(c_7742,plain,
( ( sK7(sK2,sK1) = sK5(sK2,sK1) )
| ( set_difference(sK4(sK10(sK1,sK2)),singleton(sK1)) = sK3(sK10(sK1,sK2)) ) ),
inference(renaming,[status(thm)],[c_7741]) ).
tcf(c_7749,plain,
! [X0: $i] :
( ( sK7(sK2,sK1) = sK5(sK2,sK1) )
| ~ in(sK3(X0),X0)
| ~ in(sK3(X0),powerset(sK1))
| ~ in(sK4(sK10(sK1,sK2)),sK2)
| ( sK3(sK10(sK1,sK2)) != sK3(X0) ) ),
inference(superposition,[status(thm)],[c_7742,c_49]) ).
tcf(c_7754,plain,
! [X0: $i] :
( sP0(X0,sK1)
| in(sK3(sK10(sK1,sK2)),sK10(sK1,X0))
| ( sK7(sK2,sK1) = sK5(sK2,sK1) )
| ~ ordinal(sK1)
| ~ element(X0,powerset(powerset(succ(sK1))))
| ~ in(sK4(sK10(sK1,sK2)),X0)
| ~ in(set_difference(sK4(sK10(sK1,sK2)),singleton(sK1)),powerset(sK1)) ),
inference(superposition,[status(thm)],[c_7742,c_62]) ).
tcf(c_7768,plain,
! [X0: $i] :
( sP0(X0,sK1)
| in(sK3(sK10(sK1,sK2)),sK10(sK1,X0))
| ( sK7(sK2,sK1) = sK5(sK2,sK1) )
| ~ element(X0,powerset(powerset(succ(sK1))))
| ~ in(sK4(sK10(sK1,sK2)),X0)
| ~ in(set_difference(sK4(sK10(sK1,sK2)),singleton(sK1)),powerset(sK1)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_7754,c_53]) ).
tcf(c_7863,plain,
( ( sK7(sK2,sK1) = sK5(sK2,sK1) )
| ~ in(sK4(sK10(sK1,sK2)),sK2)
| ~ in(sK3(sK10(sK1,sK2)),powerset(sK1))
| ~ in(sK3(sK10(sK1,sK2)),sK10(sK1,sK2)) ),
inference(equality_resolution,[status(thm)],[c_7749]) ).
tcf(c_7899,plain,
! [X0: $i] :
( sP0(X0,sK1)
| in(sK3(sK10(sK1,sK2)),sK10(sK1,X0))
| ( sK7(sK2,sK1) = sK5(sK2,sK1) )
| ~ element(X0,powerset(powerset(succ(sK1))))
| ~ in(sK4(sK10(sK1,sK2)),X0)
| ~ in(sK3(sK10(sK1,sK2)),powerset(sK1)) ),
inference(superposition,[status(thm)],[c_7742,c_7768]) ).
tcf(c_7989,plain,
( ( sK6(sK2,sK1) = sK5(sK2,sK1) )
| ( set_difference(sK4(sK10(sK1,sK2)),singleton(sK1)) = sK3(sK10(sK1,sK2)) )
| ~ in(sK12(sK1,sK2,sK3(sK10(sK1,sK2))),sK2) ),
inference(global_subsumption_just,[status(thm)],[c_6876,c_5625,c_6876,c_7366]) ).
tcf(c_7997,plain,
( sP0(sK2,sK1)
| ( sK6(sK2,sK1) = sK5(sK2,sK1) )
| ( set_difference(sK4(sK10(sK1,sK2)),singleton(sK1)) = sK3(sK10(sK1,sK2)) )
| ~ in(sK3(sK10(sK1,sK2)),sK10(sK1,sK2)) ),
inference(superposition,[status(thm)],[c_4761,c_7989]) ).
tcf(c_8034,plain,
( ( set_difference(sK4(sK10(sK1,sK2)),singleton(sK1)) = sK3(sK10(sK1,sK2)) )
| ( sK6(sK2,sK1) = sK5(sK2,sK1) ) ),
inference(global_subsumption_just,[status(thm)],[c_7997,c_5620,c_7366,c_7997]) ).
tcf(c_8035,plain,
( ( sK6(sK2,sK1) = sK5(sK2,sK1) )
| ( set_difference(sK4(sK10(sK1,sK2)),singleton(sK1)) = sK3(sK10(sK1,sK2)) ) ),
inference(renaming,[status(thm)],[c_8034]) ).
tcf(c_8042,plain,
! [X0: $i] :
( ( sK6(sK2,sK1) = sK5(sK2,sK1) )
| ~ in(sK3(X0),X0)
| ~ in(sK3(X0),powerset(sK1))
| ~ in(sK4(sK10(sK1,sK2)),sK2)
| ( sK3(sK10(sK1,sK2)) != sK3(X0) ) ),
inference(superposition,[status(thm)],[c_8035,c_49]) ).
tcf(c_8047,plain,
! [X0: $i] :
( sP0(X0,sK1)
| in(sK3(sK10(sK1,sK2)),sK10(sK1,X0))
| ( sK6(sK2,sK1) = sK5(sK2,sK1) )
| ~ ordinal(sK1)
| ~ element(X0,powerset(powerset(succ(sK1))))
| ~ in(sK4(sK10(sK1,sK2)),X0)
| ~ in(set_difference(sK4(sK10(sK1,sK2)),singleton(sK1)),powerset(sK1)) ),
inference(superposition,[status(thm)],[c_8035,c_62]) ).
tcf(c_8063,plain,
! [X0: $i] :
( sP0(X0,sK1)
| in(sK3(sK10(sK1,sK2)),sK10(sK1,X0))
| ( sK6(sK2,sK1) = sK5(sK2,sK1) )
| ~ element(X0,powerset(powerset(succ(sK1))))
| ~ in(sK4(sK10(sK1,sK2)),X0)
| ~ in(set_difference(sK4(sK10(sK1,sK2)),singleton(sK1)),powerset(sK1)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_8047,c_53]) ).
tcf(c_8188,plain,
( ( sK6(sK2,sK1) = sK5(sK2,sK1) )
| ~ in(sK4(sK10(sK1,sK2)),sK2)
| ~ in(sK3(sK10(sK1,sK2)),powerset(sK1))
| ~ in(sK3(sK10(sK1,sK2)),sK10(sK1,sK2)) ),
inference(equality_resolution,[status(thm)],[c_8042]) ).
tcf(c_8217,plain,
( sP0(sK2,sK1)
| ( sK7(sK2,sK1) = sK5(sK2,sK1) )
| ( set_difference(sK12(sK1,sK2,sK3(sK10(sK1,sK2))),singleton(sK1)) = sK3(sK10(sK1,sK2)) )
| ~ element(sK2,powerset(powerset(succ(sK1))))
| ~ in(sK4(sK10(sK1,sK2)),sK2)
| ~ in(sK3(sK10(sK1,sK2)),powerset(sK1)) ),
inference(superposition,[status(thm)],[c_7899,c_4881]) ).
tcf(c_8218,plain,
( sP0(sK2,sK1)
| ( sK7(sK2,sK1) = sK5(sK2,sK1) )
| ( sK11(sK1,sK2,sK3(sK10(sK1,sK2))) = sK3(sK10(sK1,sK2)) )
| ~ element(sK2,powerset(powerset(succ(sK1))))
| ~ in(sK4(sK10(sK1,sK2)),sK2)
| ~ in(sK3(sK10(sK1,sK2)),powerset(sK1)) ),
inference(superposition,[status(thm)],[c_7899,c_4839]) ).
tcf(c_8228,plain,
( sP0(sK2,sK1)
| ( sK7(sK2,sK1) = sK5(sK2,sK1) )
| ~ element(sK2,powerset(powerset(succ(sK1))))
| ~ in(sK4(sK10(sK1,sK2)),sK2)
| ~ in(sK3(sK10(sK1,sK2)),powerset(sK1)) ),
inference(superposition,[status(thm)],[c_7899,c_7863]) ).
tcf(c_8230,plain,
( sP0(sK2,sK1)
| ( sK7(sK2,sK1) = sK5(sK2,sK1) )
| ~ in(sK4(sK10(sK1,sK2)),sK2)
| ~ in(sK3(sK10(sK1,sK2)),powerset(sK1)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_8228,c_54]) ).
tcf(c_8247,plain,
( sP0(sK2,sK1)
| ( sK7(sK2,sK1) = sK5(sK2,sK1) )
| ( sK11(sK1,sK2,sK3(sK10(sK1,sK2))) = sK3(sK10(sK1,sK2)) )
| ~ in(sK4(sK10(sK1,sK2)),sK2)
| ~ in(sK3(sK10(sK1,sK2)),powerset(sK1)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_8218,c_54]) ).
tcf(c_8253,plain,
( sP0(sK2,sK1)
| ( sK7(sK2,sK1) = sK5(sK2,sK1) )
| ( set_difference(sK12(sK1,sK2,sK3(sK10(sK1,sK2))),singleton(sK1)) = sK3(sK10(sK1,sK2)) )
| ~ in(sK4(sK10(sK1,sK2)),sK2)
| ~ in(sK3(sK10(sK1,sK2)),powerset(sK1)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_8217,c_54]) ).
tcf(c_8389,plain,
( ~ in(sK3(sK10(sK1,sK2)),powerset(sK1))
| ~ in(sK4(sK10(sK1,sK2)),sK2)
| ( sK7(sK2,sK1) = sK5(sK2,sK1) ) ),
inference(global_subsumption_just,[status(thm)],[c_8230,c_5619,c_8230]) ).
tcf(c_8390,plain,
( ( sK7(sK2,sK1) = sK5(sK2,sK1) )
| ~ in(sK4(sK10(sK1,sK2)),sK2)
| ~ in(sK3(sK10(sK1,sK2)),powerset(sK1)) ),
inference(renaming,[status(thm)],[c_8389]) ).
tcf(c_8397,plain,
( in(sK3(sK10(sK1,sK2)),sK10(sK1,sK2))
| ( sK7(sK2,sK1) = sK5(sK2,sK1) )
| ~ in(sK4(sK10(sK1,sK2)),sK2) ),
inference(superposition,[status(thm)],[c_50,c_8390]) ).
tcf(c_8416,plain,
( in(sK3(sK10(sK1,sK2)),sK10(sK1,sK2))
| ( sK7(sK2,sK1) = sK5(sK2,sK1) ) ),
inference(global_subsumption_just,[status(thm)],[c_8397,c_7367,c_8397]) ).
tcf(c_8423,plain,
( sP0(sK2,sK1)
| ( sK7(sK2,sK1) = sK5(sK2,sK1) )
| ( set_difference(sK12(sK1,sK2,sK3(sK10(sK1,sK2))),singleton(sK1)) = sK3(sK10(sK1,sK2)) ) ),
inference(superposition,[status(thm)],[c_8416,c_4881]) ).
tcf(c_8424,plain,
( sP0(sK2,sK1)
| ( sK7(sK2,sK1) = sK5(sK2,sK1) )
| ( sK11(sK1,sK2,sK3(sK10(sK1,sK2))) = sK3(sK10(sK1,sK2)) ) ),
inference(superposition,[status(thm)],[c_8416,c_4839]) ).
tcf(c_8449,plain,
( ( sK11(sK1,sK2,sK3(sK10(sK1,sK2))) = sK3(sK10(sK1,sK2)) )
| ( sK7(sK2,sK1) = sK5(sK2,sK1) ) ),
inference(global_subsumption_just,[status(thm)],[c_8247,c_5619,c_8424]) ).
tcf(c_8450,plain,
( ( sK7(sK2,sK1) = sK5(sK2,sK1) )
| ( sK11(sK1,sK2,sK3(sK10(sK1,sK2))) = sK3(sK10(sK1,sK2)) ) ),
inference(renaming,[status(thm)],[c_8449]) ).
tcf(c_8455,plain,
( sP0(sK2,sK1)
| in(sK3(sK10(sK1,sK2)),powerset(sK1))
| ( sK7(sK2,sK1) = sK5(sK2,sK1) )
| ~ ordinal(sK1)
| ~ element(sK2,powerset(powerset(succ(sK1))))
| ~ in(sK3(sK10(sK1,sK2)),sK10(sK1,sK2)) ),
inference(superposition,[status(thm)],[c_8450,c_63]) ).
tcf(c_8457,plain,
( sP0(sK2,sK1)
| in(sK3(sK10(sK1,sK2)),powerset(sK1))
| ( sK7(sK2,sK1) = sK5(sK2,sK1) )
| ~ in(sK3(sK10(sK1,sK2)),sK10(sK1,sK2)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_8455,c_53,c_54]) ).
tcf(c_8473,plain,
( ( sK7(sK2,sK1) = sK5(sK2,sK1) )
| in(sK3(sK10(sK1,sK2)),powerset(sK1)) ),
inference(global_subsumption_just,[status(thm)],[c_8457,c_5619,c_7368,c_8457]) ).
tcf(c_8474,plain,
( in(sK3(sK10(sK1,sK2)),powerset(sK1))
| ( sK7(sK2,sK1) = sK5(sK2,sK1) ) ),
inference(renaming,[status(thm)],[c_8473]) ).
tcf(c_8480,plain,
! [X0: $i] :
( sP0(X0,sK1)
| in(sK3(sK10(sK1,sK2)),sK10(sK1,X0))
| ( sK7(sK2,sK1) = sK5(sK2,sK1) )
| ~ element(X0,powerset(powerset(succ(sK1))))
| ~ in(sK4(sK10(sK1,sK2)),X0) ),
inference(backward_subsumption_resolution,[status(thm)],[c_7899,c_8474]) ).
tcf(c_8514,plain,
( ( set_difference(sK12(sK1,sK2,sK3(sK10(sK1,sK2))),singleton(sK1)) = sK3(sK10(sK1,sK2)) )
| ( sK7(sK2,sK1) = sK5(sK2,sK1) ) ),
inference(global_subsumption_just,[status(thm)],[c_8253,c_5619,c_8423]) ).
tcf(c_8515,plain,
( ( sK7(sK2,sK1) = sK5(sK2,sK1) )
| ( set_difference(sK12(sK1,sK2,sK3(sK10(sK1,sK2))),singleton(sK1)) = sK3(sK10(sK1,sK2)) ) ),
inference(renaming,[status(thm)],[c_8514]) ).
tcf(c_8522,plain,
! [X0: $i] :
( ( sK7(sK2,sK1) = sK5(sK2,sK1) )
| ~ in(sK3(X0),X0)
| ~ in(sK3(X0),powerset(sK1))
| ~ in(sK12(sK1,sK2,sK3(sK10(sK1,sK2))),sK2)
| ( sK3(sK10(sK1,sK2)) != sK3(X0) ) ),
inference(superposition,[status(thm)],[c_8515,c_49]) ).
tcf(c_8670,plain,
( ( sK7(sK2,sK1) = sK5(sK2,sK1) )
| ~ in(sK3(sK10(sK1,sK2)),powerset(sK1))
| ~ in(sK3(sK10(sK1,sK2)),sK10(sK1,sK2))
| ~ in(sK12(sK1,sK2,sK3(sK10(sK1,sK2))),sK2) ),
inference(equality_resolution,[status(thm)],[c_8522]) ).
tcf(c_8878,plain,
! [X0: $i] :
( sP0(X0,sK1)
| ( sK7(sK2,sK1) = sK5(sK2,sK1) )
| ~ element(X0,powerset(powerset(succ(sK1))))
| ~ in(sK4(sK10(sK1,sK2)),X0)
| ~ in(sK10(sK1,X0),sK3(sK10(sK1,sK2))) ),
inference(superposition,[status(thm)],[c_8480,c_105]) ).
tcf(c_9010,plain,
( ( sK7(sK2,sK1) = sK5(sK2,sK1) )
| ~ in(sK12(sK1,sK2,sK3(sK10(sK1,sK2))),sK2) ),
inference(global_subsumption_just,[status(thm)],[c_8670,c_5619,c_7367,c_8397,c_8457,c_8670]) ).
tcf(c_9016,plain,
( sP0(sK2,sK1)
| ( sK7(sK2,sK1) = sK5(sK2,sK1) )
| ~ in(sK3(sK10(sK1,sK2)),sK10(sK1,sK2)) ),
inference(superposition,[status(thm)],[c_4761,c_9010]) ).
tcf(c_9020,plain,
sK7(sK2,sK1) = sK5(sK2,sK1),
inference(global_subsumption_just,[status(thm)],[c_8878,c_5619,c_8416,c_9016]) ).
tcf(c_9040,plain,
! [X0: $i] :
( sP0(X0,sK1)
| in(sK3(sK10(sK1,sK2)),sK10(sK1,X0))
| ( sK6(sK2,sK1) = sK7(sK2,sK1) )
| ~ element(X0,powerset(powerset(succ(sK1))))
| ~ in(sK4(sK10(sK1,sK2)),X0)
| ~ in(set_difference(sK4(sK10(sK1,sK2)),singleton(sK1)),powerset(sK1)) ),
inference(demodulation,[status(thm)],[c_8063,c_9020]) ).
tcf(c_9045,plain,
( ( sK6(sK2,sK1) = sK7(sK2,sK1) )
| ~ in(sK4(sK10(sK1,sK2)),sK2)
| ~ in(sK3(sK10(sK1,sK2)),powerset(sK1))
| ~ in(sK3(sK10(sK1,sK2)),sK10(sK1,sK2)) ),
inference(demodulation,[status(thm)],[c_8188,c_9020]) ).
tcf(c_9047,plain,
( ( sK6(sK2,sK1) = sK7(sK2,sK1) )
| ( set_difference(sK4(sK10(sK1,sK2)),singleton(sK1)) = sK3(sK10(sK1,sK2)) ) ),
inference(demodulation,[status(thm)],[c_8035,c_9020]) ).
tcf(c_9154,plain,
! [X0: $i] :
( sP0(X0,sK1)
| in(sK3(sK10(sK1,sK2)),sK10(sK1,X0))
| ( sK6(sK2,sK1) = sK7(sK2,sK1) )
| ~ element(X0,powerset(powerset(succ(sK1))))
| ~ in(sK4(sK10(sK1,sK2)),X0)
| ~ in(sK3(sK10(sK1,sK2)),powerset(sK1)) ),
inference(superposition,[status(thm)],[c_9047,c_9040]) ).
tcf(c_9486,plain,
( sP0(sK2,sK1)
| ( sK6(sK2,sK1) = sK7(sK2,sK1) )
| ~ element(sK2,powerset(powerset(succ(sK1))))
| ~ in(sK4(sK10(sK1,sK2)),sK2)
| ~ in(sK3(sK10(sK1,sK2)),powerset(sK1)) ),
inference(superposition,[status(thm)],[c_9154,c_9045]) ).
tcf(c_9488,plain,
( sP0(sK2,sK1)
| ( sK6(sK2,sK1) = sK7(sK2,sK1) )
| ~ in(sK4(sK10(sK1,sK2)),sK2)
| ~ in(sK3(sK10(sK1,sK2)),powerset(sK1)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_9486,c_54]) ).
tcf(c_9640,plain,
( sP0(sK2,sK1)
| in(sK3(sK10(sK1,sK2)),sK10(sK1,sK2))
| ( sK6(sK2,sK1) = sK7(sK2,sK1) )
| ~ in(sK4(sK10(sK1,sK2)),sK2) ),
inference(superposition,[status(thm)],[c_50,c_9488]) ).
tcf(c_9655,plain,
( sP0(sK2,sK1)
| in(sK3(sK10(sK1,sK2)),sK10(sK1,sK2))
| ( sK6(sK2,sK1) = sK7(sK2,sK1) ) ),
inference(global_subsumption_just,[status(thm)],[c_9640,c_7368,c_7367,c_9488]) ).
tcf(c_9664,plain,
( sP0(sK2,sK1)
| ( sK6(sK2,sK1) = sK7(sK2,sK1) )
| ( set_difference(sK12(sK1,sK2,sK3(sK10(sK1,sK2))),singleton(sK1)) = sK3(sK10(sK1,sK2)) ) ),
inference(superposition,[status(thm)],[c_9655,c_4881]) ).
tcf(c_9665,plain,
( sP0(sK2,sK1)
| ( sK6(sK2,sK1) = sK7(sK2,sK1) )
| ( sK11(sK1,sK2,sK3(sK10(sK1,sK2))) = sK3(sK10(sK1,sK2)) ) ),
inference(superposition,[status(thm)],[c_9655,c_4839]) ).
tcf(c_9856,plain,
( ( sK6(sK2,sK1) = sK5(sK2,sK1) )
| ( sK6(sK2,sK1) = sK7(sK2,sK1) )
| ( sK11(sK1,sK2,sK3(sK10(sK1,sK2))) = sK3(sK10(sK1,sK2)) ) ),
inference(superposition,[status(thm)],[c_9665,c_56]) ).
tcf(c_9857,plain,
( ( sK6(sK2,sK1) = sK7(sK2,sK1) )
| ( sK11(sK1,sK2,sK3(sK10(sK1,sK2))) = sK3(sK10(sK1,sK2)) ) ),
inference(light_normalisation,[status(thm)],[c_9856,c_9020]) ).
tcf(c_9864,plain,
( sP0(sK2,sK1)
| in(sK3(sK10(sK1,sK2)),powerset(sK1))
| ( sK6(sK2,sK1) = sK7(sK2,sK1) )
| ~ ordinal(sK1)
| ~ element(sK2,powerset(powerset(succ(sK1))))
| ~ in(sK3(sK10(sK1,sK2)),sK10(sK1,sK2)) ),
inference(superposition,[status(thm)],[c_9857,c_63]) ).
tcf(c_9866,plain,
( sP0(sK2,sK1)
| in(sK3(sK10(sK1,sK2)),powerset(sK1))
| ( sK6(sK2,sK1) = sK7(sK2,sK1) )
| ~ in(sK3(sK10(sK1,sK2)),sK10(sK1,sK2)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_9864,c_53,c_54]) ).
tcf(c_9889,plain,
( ( sK6(sK2,sK1) = sK5(sK2,sK1) )
| ( sK6(sK2,sK1) = sK7(sK2,sK1) )
| ( set_difference(sK12(sK1,sK2,sK3(sK10(sK1,sK2))),singleton(sK1)) = sK3(sK10(sK1,sK2)) ) ),
inference(superposition,[status(thm)],[c_9664,c_56]) ).
tcf(c_9890,plain,
( ( sK6(sK2,sK1) = sK7(sK2,sK1) )
| ( set_difference(sK12(sK1,sK2,sK3(sK10(sK1,sK2))),singleton(sK1)) = sK3(sK10(sK1,sK2)) ) ),
inference(light_normalisation,[status(thm)],[c_9889,c_9020]) ).
tcf(c_9899,plain,
! [X0: $i] :
( ( sK6(sK2,sK1) = sK7(sK2,sK1) )
| ~ in(sK3(X0),X0)
| ~ in(sK3(X0),powerset(sK1))
| ~ in(sK12(sK1,sK2,sK3(sK10(sK1,sK2))),sK2)
| ( sK3(sK10(sK1,sK2)) != sK3(X0) ) ),
inference(superposition,[status(thm)],[c_9890,c_49]) ).
tcf(c_9965,plain,
( ( sK11(sK1,sK2,sK3(sK10(sK1,sK2))) = sK3(sK10(sK1,sK2)) )
| in(sK3(sK10(sK1,sK2)),powerset(sK1)) ),
inference(global_subsumption_just,[status(thm)],[c_8608,c_4926,c_5621,c_9857]) ).
tcf(c_9966,plain,
( in(sK3(sK10(sK1,sK2)),powerset(sK1))
| ( sK11(sK1,sK2,sK3(sK10(sK1,sK2))) = sK3(sK10(sK1,sK2)) ) ),
inference(renaming,[status(thm)],[c_9965]) ).
tcf(c_9998,plain,
( sP0(sK2,sK1)
| in(sK3(sK10(sK1,sK2)),powerset(sK1))
| ( sK6(sK2,sK1) = sK7(sK2,sK1) ) ),
inference(global_subsumption_just,[status(thm)],[c_9866,c_7368,c_9866]) ).
tcf(c_10026,plain,
( ( sK6(sK2,sK1) = sK7(sK2,sK1) )
| ~ in(sK3(sK10(sK1,sK2)),powerset(sK1))
| ~ in(sK3(sK10(sK1,sK2)),sK10(sK1,sK2))
| ~ in(sK12(sK1,sK2,sK3(sK10(sK1,sK2))),sK2) ),
inference(equality_resolution,[status(thm)],[c_9899]) ).
tcf(c_10088,plain,
( ( set_difference(sK4(sK10(sK1,sK2)),singleton(sK1)) = sK3(sK10(sK1,sK2)) )
| ( sK11(sK1,sK2,sK3(sK10(sK1,sK2))) = sK3(sK10(sK1,sK2)) ) ),
inference(global_subsumption_just,[status(thm)],[c_8607,c_4925,c_5621,c_9857]) ).
tcf(c_10089,plain,
( ( sK11(sK1,sK2,sK3(sK10(sK1,sK2))) = sK3(sK10(sK1,sK2)) )
| ( set_difference(sK4(sK10(sK1,sK2)),singleton(sK1)) = sK3(sK10(sK1,sK2)) ) ),
inference(renaming,[status(thm)],[c_10088]) ).
tcf(c_10094,plain,
( sP0(sK2,sK1)
| in(sK3(sK10(sK1,sK2)),powerset(sK1))
| ( set_difference(sK4(sK10(sK1,sK2)),singleton(sK1)) = sK3(sK10(sK1,sK2)) )
| ~ ordinal(sK1)
| ~ element(sK2,powerset(powerset(succ(sK1))))
| ~ in(sK3(sK10(sK1,sK2)),sK10(sK1,sK2)) ),
inference(superposition,[status(thm)],[c_10089,c_63]) ).
tcf(c_10095,plain,
( sP0(sK2,sK1)
| in(sK3(sK10(sK1,sK2)),powerset(sK1))
| ( set_difference(sK4(sK10(sK1,sK2)),singleton(sK1)) = sK3(sK10(sK1,sK2)) )
| ~ in(sK3(sK10(sK1,sK2)),sK10(sK1,sK2)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_10094,c_53,c_54]) ).
tcf(c_10190,plain,
( ( set_difference(sK12(sK1,sK2,sK3(sK10(sK1,sK2))),singleton(sK1)) = sK3(sK10(sK1,sK2)) )
| ( set_difference(sK4(sK10(sK1,sK2)),singleton(sK1)) = sK3(sK10(sK1,sK2)) ) ),
inference(global_subsumption_just,[status(thm)],[c_9594,c_4966,c_5621,c_9047]) ).
tcf(c_10191,plain,
( ( set_difference(sK4(sK10(sK1,sK2)),singleton(sK1)) = sK3(sK10(sK1,sK2)) )
| ( set_difference(sK12(sK1,sK2,sK3(sK10(sK1,sK2))),singleton(sK1)) = sK3(sK10(sK1,sK2)) ) ),
inference(renaming,[status(thm)],[c_10190]) ).
tcf(c_10198,plain,
! [X0: $i] :
( ( set_difference(sK4(sK10(sK1,sK2)),singleton(sK1)) = sK3(sK10(sK1,sK2)) )
| ~ in(sK3(X0),X0)
| ~ in(sK3(X0),powerset(sK1))
| ~ in(sK12(sK1,sK2,sK3(sK10(sK1,sK2))),sK2)
| ( sK3(sK10(sK1,sK2)) != sK3(X0) ) ),
inference(superposition,[status(thm)],[c_10191,c_49]) ).
tcf(c_10362,plain,
( ( set_difference(sK4(sK10(sK1,sK2)),singleton(sK1)) = sK3(sK10(sK1,sK2)) )
| in(sK3(sK10(sK1,sK2)),powerset(sK1)) ),
inference(global_subsumption_just,[status(thm)],[c_10095,c_5621,c_7368,c_9047,c_10095]) ).
tcf(c_10363,plain,
( in(sK3(sK10(sK1,sK2)),powerset(sK1))
| ( set_difference(sK4(sK10(sK1,sK2)),singleton(sK1)) = sK3(sK10(sK1,sK2)) ) ),
inference(renaming,[status(thm)],[c_10362]) ).
tcf(c_10392,plain,
( sP0(sK2,sK1)
| ( sK6(sK2,sK1) = sK7(sK2,sK1) )
| ~ in(sK3(sK10(sK1,sK2)),powerset(sK1))
| ~ in(sK3(sK10(sK1,sK2)),sK10(sK1,sK2)) ),
inference(superposition,[status(thm)],[c_4761,c_10026]) ).
tcf(c_10754,plain,
( ( set_difference(sK4(sK10(sK1,sK2)),singleton(sK1)) = sK3(sK10(sK1,sK2)) )
| ~ in(sK3(sK10(sK1,sK2)),powerset(sK1))
| ~ in(sK3(sK10(sK1,sK2)),sK10(sK1,sK2))
| ~ in(sK12(sK1,sK2,sK3(sK10(sK1,sK2))),sK2) ),
inference(equality_resolution,[status(thm)],[c_10198]) ).
tcf(c_10805,plain,
( ( set_difference(sK4(sK10(sK1,sK2)),singleton(sK1)) = sK3(sK10(sK1,sK2)) )
| ~ in(sK12(sK1,sK2,sK3(sK10(sK1,sK2))),sK2) ),
inference(global_subsumption_just,[status(thm)],[c_10754,c_7366,c_10363,c_10754]) ).
tcf(c_10811,plain,
( sP0(sK2,sK1)
| ( set_difference(sK4(sK10(sK1,sK2)),singleton(sK1)) = sK3(sK10(sK1,sK2)) )
| ~ in(sK3(sK10(sK1,sK2)),sK10(sK1,sK2)) ),
inference(superposition,[status(thm)],[c_7228,c_10805]) ).
tcf(c_10835,plain,
set_difference(sK4(sK10(sK1,sK2)),singleton(sK1)) = sK3(sK10(sK1,sK2)),
inference(global_subsumption_just,[status(thm)],[c_10811,c_5621,c_7366,c_9047,c_10811]) ).
tcf(c_10842,plain,
( sP0(sK2,sK1)
| ( sK11(sK1,sK2,set_difference(sK4(sK10(sK1,sK2)),singleton(sK1))) = set_difference(sK4(sK10(sK1,sK2)),singleton(sK1)) )
| ~ in(sK4(sK10(sK1,sK2)),sK2)
| ~ in(sK3(sK10(sK1,sK2)),powerset(sK1)) ),
inference(superposition,[status(thm)],[c_10835,c_8628]) ).
tcf(c_10843,plain,
! [X0: $i] :
( ~ in(sK3(X0),X0)
| ~ in(sK3(X0),powerset(sK1))
| ~ in(sK4(sK10(sK1,sK2)),sK2)
| ( sK3(sK10(sK1,sK2)) != sK3(X0) ) ),
inference(superposition,[status(thm)],[c_10835,c_49]) ).
tcf(c_10844,plain,
! [X0: $i] :
( sP0(X0,sK1)
| in(sK3(sK10(sK1,sK2)),sK10(sK1,X0))
| ~ ordinal(sK1)
| ~ element(X0,powerset(powerset(succ(sK1))))
| ~ in(sK4(sK10(sK1,sK2)),X0)
| ~ in(set_difference(sK4(sK10(sK1,sK2)),singleton(sK1)),powerset(sK1)) ),
inference(superposition,[status(thm)],[c_10835,c_62]) ).
tcf(c_10849,plain,
( sP0(sK2,sK1)
| ( sK11(sK1,sK2,sK3(sK10(sK1,sK2))) = sK3(sK10(sK1,sK2)) )
| ~ in(sK4(sK10(sK1,sK2)),sK2)
| ~ in(sK3(sK10(sK1,sK2)),powerset(sK1)) ),
inference(light_normalisation,[status(thm)],[c_10842,c_10835]) ).
tcf(c_10854,plain,
! [X0: $i] :
( sP0(X0,sK1)
| in(sK3(sK10(sK1,sK2)),sK10(sK1,X0))
| ~ ordinal(sK1)
| ~ element(X0,powerset(powerset(succ(sK1))))
| ~ in(sK4(sK10(sK1,sK2)),X0)
| ~ in(sK3(sK10(sK1,sK2)),powerset(sK1)) ),
inference(light_normalisation,[status(thm)],[c_10844,c_10835]) ).
tcf(c_10855,plain,
! [X0: $i] :
( sP0(X0,sK1)
| in(sK3(sK10(sK1,sK2)),sK10(sK1,X0))
| ~ element(X0,powerset(powerset(succ(sK1))))
| ~ in(sK4(sK10(sK1,sK2)),X0)
| ~ in(sK3(sK10(sK1,sK2)),powerset(sK1)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_10854,c_53]) ).
tcf(c_10896,plain,
( ~ in(sK4(sK10(sK1,sK2)),sK2)
| ~ in(sK3(sK10(sK1,sK2)),powerset(sK1))
| ~ in(sK3(sK10(sK1,sK2)),sK10(sK1,sK2)) ),
inference(equality_resolution,[status(thm)],[c_10843]) ).
tcf(c_10930,plain,
( sP0(sK2,sK1)
| ~ element(sK2,powerset(powerset(succ(sK1))))
| ~ in(sK4(sK10(sK1,sK2)),sK2)
| ~ in(sK3(sK10(sK1,sK2)),powerset(sK1)) ),
inference(superposition,[status(thm)],[c_10855,c_10896]) ).
tcf(c_10931,plain,
( sP0(sK2,sK1)
| ~ in(sK4(sK10(sK1,sK2)),sK2)
| ~ in(sK3(sK10(sK1,sK2)),powerset(sK1)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_10930,c_54]) ).
tcf(c_10935,plain,
( sP0(sK2,sK1)
| ( sK6(sK2,sK1) = sK7(sK2,sK1) ) ),
inference(global_subsumption_just,[status(thm)],[c_10392,c_9655,c_9998,c_10392]) ).
tcf(c_10944,plain,
( ( sK6(sK2,sK1) = sK5(sK2,sK1) )
| ( sK6(sK2,sK1) = sK7(sK2,sK1) ) ),
inference(superposition,[status(thm)],[c_10935,c_56]) ).
tcf(c_10945,plain,
sK6(sK2,sK1) = sK7(sK2,sK1),
inference(light_normalisation,[status(thm)],[c_10944,c_9020]) ).
tcf(c_11019,plain,
~ sP0(sK2,sK1),
inference(superposition,[status(thm)],[c_10945,c_55]) ).
tcf(c_11027,plain,
( in(sK4(sK10(sK1,sK2)),sK2)
| ( set_difference(sK12(sK1,sK2,sK3(sK10(sK1,sK2))),singleton(sK1)) = sK3(sK10(sK1,sK2)) ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_4968,c_11019]) ).
tcf(c_11033,plain,
( in(sK4(sK10(sK1,sK2)),sK2)
| ( sK11(sK1,sK2,sK3(sK10(sK1,sK2))) = sK3(sK10(sK1,sK2)) ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_4927,c_11019]) ).
tcf(c_11039,plain,
! [X0: $i] :
( in(sK12(sK1,sK2,X0),sK2)
| ~ in(X0,sK10(sK1,sK2)) ),
inference(backward_subsumption_resolution,[status(thm)],[c_4761,c_11019]) ).
tcf(c_11187,plain,
sK11(sK1,sK2,sK3(sK10(sK1,sK2))) = sK3(sK10(sK1,sK2)),
inference(global_subsumption_just,[status(thm)],[c_11033,c_4927,c_5621,c_9966,c_10849,c_10945]) ).
tcf(c_11189,plain,
( sP0(sK2,sK1)
| in(sK3(sK10(sK1,sK2)),powerset(sK1))
| ~ ordinal(sK1)
| ~ element(sK2,powerset(powerset(succ(sK1))))
| ~ in(sK3(sK10(sK1,sK2)),sK10(sK1,sK2)) ),
inference(superposition,[status(thm)],[c_11187,c_63]) ).
tcf(c_11191,plain,
( in(sK3(sK10(sK1,sK2)),powerset(sK1))
| ~ in(sK3(sK10(sK1,sK2)),sK10(sK1,sK2)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_11189,c_11019,c_53,c_54]) ).
tcf(c_11197,plain,
in(sK3(sK10(sK1,sK2)),powerset(sK1)),
inference(global_subsumption_just,[status(thm)],[c_11191,c_7368,c_11191]) ).
tcf(c_11309,plain,
set_difference(sK12(sK1,sK2,sK3(sK10(sK1,sK2))),singleton(sK1)) = sK3(sK10(sK1,sK2)),
inference(global_subsumption_just,[status(thm)],[c_11027,c_4968,c_5621,c_10931,c_10945,c_11197]) ).
tcf(c_11311,plain,
! [X0: $i] :
( ~ in(sK3(X0),X0)
| ~ in(sK3(X0),powerset(sK1))
| ~ in(sK12(sK1,sK2,sK3(sK10(sK1,sK2))),sK2)
| ( sK3(sK10(sK1,sK2)) != sK3(X0) ) ),
inference(superposition,[status(thm)],[c_11309,c_49]) ).
tcf(c_11414,plain,
( ~ in(sK3(sK10(sK1,sK2)),powerset(sK1))
| ~ in(sK3(sK10(sK1,sK2)),sK10(sK1,sK2))
| ~ in(sK12(sK1,sK2,sK3(sK10(sK1,sK2))),sK2) ),
inference(equality_resolution,[status(thm)],[c_11311]) ).
tcf(c_11415,plain,
( ~ in(sK3(sK10(sK1,sK2)),sK10(sK1,sK2))
| ~ in(sK12(sK1,sK2,sK3(sK10(sK1,sK2))),sK2) ),
inference(forward_subsumption_resolution,[status(thm)],[c_11414,c_11197]) ).
tcf(c_11483,plain,
~ in(sK12(sK1,sK2,sK3(sK10(sK1,sK2))),sK2),
inference(global_subsumption_just,[status(thm)],[c_11415,c_5621,c_7367,c_10931,c_10945,c_11197,c_11415]) ).
tcf(c_11485,plain,
~ in(sK3(sK10(sK1,sK2)),sK10(sK1,sK2)),
inference(superposition,[status(thm)],[c_11039,c_11483]) ).
tcf(c_11486,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_11485,c_11197,c_10945,c_10931,c_7367,c_5621]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : SEU298+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.02 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.04/0.31 % Computer : n012.cluster.edu
% 0.04/0.31 % Model : x86_64 x86_64
% 0.04/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.04/0.31 % Memory : 8046.5625MB
% 0.04/0.31 % OS : Linux 6.8.0-71-generic
% 0.04/0.31 % CPULimit : 300
% 0.04/0.31 % WCLimit : 300
% 0.04/0.31 % DateTime : Thu Sep 24 13:36:06 UTC 2026
% 0.04/0.31 % CPUTime :
% 0.04/0.31 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.04/0.35 Running first-order theorem proving
% 0.04/0.35 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.04/0.36
% 0.04/0.36 % ======== iProver multi-core TPTP/SMT =========
% 0.04/0.36
% 0.10/0.36 % Detected problem language: tptp
% 0.10/0.37 % Proving...
% 7.89/1.66 % SZS status Started for theBenchmark.p
% 7.89/1.66 % SZS status Theorem for theBenchmark.p
% 7.89/1.66
% 7.89/1.66 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 7.89/1.66
% 7.89/1.66 % ------ iProver source info
% 7.89/1.66
% 7.89/1.66 % git: date: 2026-07-19 20:42:38 +0200
% 7.89/1.66 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 7.89/1.66 % git: non_committed_changes: false
% 7.89/1.66
% 7.89/1.66 % ------ Parsing...
% 7.89/1.66 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 7.89/1.66
% 7.89/1.66 % ------ Preprocessing... sup_sim: 0 sf_s rm: 31 0s sf_e pe_s pe:1:0s pe:2:0s pe_e sup_sim: 0 sf_s rm: 7 0s sf_e pe_s pe_e %
% 7.89/1.66
% 7.89/1.66 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 7.89/1.66
% 7.89/1.66 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 7.89/1.66 % ------ Proving...
% 7.89/1.66 % ------ Problem Properties
% 7.89/1.66
% 7.89/1.66 %
% 7.89/1.66 % clauses 47
% 7.89/1.66 % conjectures 6
% 7.89/1.66 % EPR 17
% 7.89/1.66 % Horn 37
% 7.89/1.66 % unary 23
% 7.89/1.66 % binary 17
% 7.89/1.66 % lits 90
% 7.89/1.66 % lits eq 9
% 7.89/1.66 % fd_pure 0
% 7.89/1.66 % fd_pseudo 0
% 7.89/1.66 % fd_cond 0
% 7.89/1.66 % fd_pseudo_cond 0
% 7.89/1.66 % AC symbols 0
% 7.89/1.66
% 7.89/1.66 % ------ Schedule dynamic 5 is on
% 7.89/1.66
% 7.89/1.66 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 7.89/1.66
% 7.89/1.66
% 7.89/1.66 % ------
% 7.89/1.66 % Current options:
% 7.89/1.66 % ------
% 7.89/1.66
% 7.89/1.66
% 7.89/1.66 %
% 7.89/1.66
% 7.89/1.66 % ------ Proving...
% 7.89/1.66 %
% 7.89/1.66
% 7.89/1.66 % SZS status Theorem for theBenchmark.p
% 7.89/1.66
% 7.89/1.66 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 7.89/1.66
% 7.89/1.66
%------------------------------------------------------------------------------