%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SEU298+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n014.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 02:51:38 PM UTC 2026
% Result : Theorem 29.92s 9.81s
% Output : Proof 29.92s
% Verified :
% SZS Type : Refutation
% Derivation depth : 42
% Number of leaves : 2
% Syntax : Number of formulae : 187 ( 11 unt; 0 def)
% Number of atoms : 707 ( 280 equ)
% Maximal formula atoms : 19 ( 3 avg)
% Number of connectives : 796 ( 276 ~; 465 |; 47 &)
% ( 3 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 4 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 16 ( 16 usr; 2 con; 0-3 aty)
% Number of variables : 223 ( 0 sgn 26 !; 21 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f41,axiom,
! [A,B] :
( ( element(B,powerset(powerset(succ(A))))
& ordinal(A) )
=> ( ! [C,D,E] :
( ( ? [G] :
( E = set_difference(G,singleton(A))
& in(G,B) )
& C = E
& ? [F] :
( D = set_difference(F,singleton(A))
& in(F,B) )
& C = D )
=> D = E )
=> ? [C] :
! [D] :
( in(D,C)
<=> ? [E] :
( ? [H] :
( D = set_difference(H,singleton(A))
& in(H,B) )
& E = D
& in(E,powerset(A)) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',s1_tarski__e4_27_3_1__finset_1__1) ).
fof(f41_nnf,plain,
! [A,B] :
( ? [C] :
! [D] :
( ( ! [E] :
( ! [H] :
( D != set_difference(H,singleton(A))
| ~ in(H,B) )
| E != D
| ~ in(E,powerset(A)) )
| in(D,C) )
& ( ? [E] :
( ? [H] :
( D = set_difference(H,singleton(A))
& in(H,B) )
& E = D
& in(E,powerset(A)) )
| ~ in(D,C) ) )
| ? [C,D,E] :
( D != E
& ? [G] :
( E = set_difference(G,singleton(A))
& in(G,B) )
& C = E
& ? [F] :
( D = set_difference(F,singleton(A))
& in(F,B) )
& C = D )
| ~ element(B,powerset(powerset(succ(A))))
| ~ ordinal(A) ),
inference(nnf_transformation,[status(thm)],[f41]) ).
fof(f41_sk,plain,
! [A,B,D,E,H] :
( ( ( D != set_difference(H,singleton(A))
| ~ in(H,B)
| E != D
| ~ in(E,powerset(A))
| in(D,sk25(A,B)) )
& ( ( D = set_difference(sk27(A,B,D),singleton(A))
& in(sk27(A,B,D),B)
& sk26(A,B,D) = D
& in(sk26(A,B,D),powerset(A)) )
| ~ in(D,sk25(A,B)) ) )
| ( sk21(A,B) != sk22(A,B)
& sk22(A,B) = set_difference(sk24(A,B),singleton(A))
& in(sk24(A,B),B)
& sk20(A,B) = sk22(A,B)
& sk21(A,B) = set_difference(sk23(A,B),singleton(A))
& in(sk23(A,B),B)
& sk20(A,B) = sk21(A,B) )
| ~ element(B,powerset(powerset(succ(A))))
| ~ ordinal(A) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk20,sk21,sk22,sk23,sk24,sk25,sk26,sk27])],[f41_nnf]) ).
cnf(c123,plain,
( X3 != set_difference(X7,singleton(X0))
| ~ in(X7,X1)
| X4 != X3
| ~ in(X4,powerset(X0))
| in(X3,sk25(X0,X1))
| sk20(X0,X1) = sk22(X0,X1)
| ~ element(X1,powerset(powerset(succ(X0))))
| ~ ordinal(X0) ),
inference(cnf_transformation,[status(esa)],[f41_sk]) ).
fof(f0,conjecture,
! [A,B] :
( ( element(B,powerset(powerset(succ(A))))
& ordinal(A) )
=> ? [C] :
! [D] :
( in(D,C)
<=> ( ? [E] :
( D = set_difference(E,singleton(A))
& in(E,B) )
& in(D,powerset(A)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',s1_xboole_0__e4_27_3_1__finset_1) ).
fof(f0_neg,negated_conjecture,
~ ! [A,B] :
( ( element(B,powerset(powerset(succ(A))))
& ordinal(A) )
=> ? [C] :
! [D] :
( in(D,C)
<=> ( ? [E] :
( D = set_difference(E,singleton(A))
& in(E,B) )
& in(D,powerset(A)) ) ) ),
inference(negated_conjecture,[status(cth)],[f0]) ).
fof(f0_nnf,plain,
? [A,B] :
( ! [C] :
? [D] :
( ( ? [E] :
( D = set_difference(E,singleton(A))
& in(E,B) )
& in(D,powerset(A))
& ~ in(D,C) )
| ( ( ! [E] :
( D != set_difference(E,singleton(A))
| ~ in(E,B) )
| ~ in(D,powerset(A)) )
& in(D,C) ) )
& element(B,powerset(powerset(succ(A))))
& ordinal(A) ),
inference(nnf_transformation,[status(thm)],[f0_neg]) ).
fof(f0_sk,plain,
! [C,E] :
( ( ( sk2(C) = set_difference(sk3(C),singleton(sk0))
& in(sk3(C),sk1)
& in(sk2(C),powerset(sk0))
& ~ in(sk2(C),C) )
| ( ( sk2(C) != set_difference(E,singleton(sk0))
| ~ in(E,sk1)
| ~ in(sk2(C),powerset(sk0)) )
& in(sk2(C),C) ) )
& element(sk1,powerset(powerset(succ(sk0))))
& ordinal(sk0) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk0,sk1,sk2,sk3])],[f0_nnf]) ).
cnf(c0,plain,
ordinal(sk0),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p995,plain,
( X1 != set_difference(X3,singleton(sk0))
| ~ in(X3,X0)
| X2 != X1
| ~ in(X2,powerset(sk0))
| in(X1,sk25(sk0,X0))
| sk20(sk0,X0) = sk22(sk0,X0)
| ~ element(X0,powerset(powerset(succ(sk0)))) ),
inference(resolution,[status(thm)],[c123,c0]) ).
cnf(c1,plain,
element(sk1,powerset(powerset(succ(sk0)))),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p7204,plain,
( X0 != set_difference(X2,singleton(sk0))
| ~ in(X2,sk1)
| X1 != X0
| ~ in(X1,powerset(sk0))
| in(X0,sk25(sk0,sk1))
| sk20(sk0,sk1) = sk22(sk0,sk1) ),
inference(resolution,[status(thm)],[p995,c1]) ).
cnf(p7214,plain,
( X0 != set_difference(X1,singleton(sk0))
| ~ in(X1,sk1)
| ~ in(X0,powerset(sk0))
| in(X0,sk25(sk0,sk1))
| sk20(sk0,sk1) = sk22(sk0,sk1) ),
inference(equality_resolution,[status(thm)],[p7204]) ).
cnf(c3,plain,
( in(sk2(X2),powerset(sk0))
| in(sk2(X2),X2) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p7236,plain,
( in(sk2(X0),X0)
| sk2(X0) != set_difference(X1,singleton(sk0))
| ~ in(X1,sk1)
| in(sk2(X0),sk25(sk0,sk1))
| sk20(sk0,sk1) = sk22(sk0,sk1) ),
inference(resolution,[status(thm)],[p7214,c3]) ).
cnf(p7265,plain,
( sk2(sk25(sk0,sk1)) != set_difference(X0,singleton(sk0))
| ~ in(X0,sk1)
| in(sk2(sk25(sk0,sk1)),sk25(sk0,sk1))
| sk20(sk0,sk1) = sk22(sk0,sk1) ),
inference(factoring,[status(thm)],[p7236]) ).
cnf(c4,plain,
( in(sk3(X2),sk1)
| in(sk2(X2),X2) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p7279,plain,
( in(sk2(X0),X0)
| sk2(sk25(sk0,sk1)) != set_difference(sk3(X0),singleton(sk0))
| in(sk2(sk25(sk0,sk1)),sk25(sk0,sk1))
| sk20(sk0,sk1) = sk22(sk0,sk1) ),
inference(resolution,[status(thm)],[p7265,c4]) ).
cnf(p7302,plain,
( sk2(sk25(sk0,sk1)) != set_difference(sk3(sk25(sk0,sk1)),singleton(sk0))
| in(sk2(sk25(sk0,sk1)),sk25(sk0,sk1))
| sk20(sk0,sk1) = sk22(sk0,sk1) ),
inference(factoring,[status(thm)],[p7279]) ).
cnf(c5,plain,
( sk2(X2) = set_difference(sk3(X2),singleton(sk0))
| in(sk2(X2),X2) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p7305,plain,
( in(sk2(sk25(sk0,sk1)),sk25(sk0,sk1))
| in(sk2(sk25(sk0,sk1)),sk25(sk0,sk1))
| sk20(sk0,sk1) = sk22(sk0,sk1) ),
inference(resolution,[status(thm)],[p7302,c5]) ).
cnf(p7306,plain,
( in(sk2(sk25(sk0,sk1)),sk25(sk0,sk1))
| sk20(sk0,sk1) = sk22(sk0,sk1) ),
inference(factoring,[status(thm)],[p7305]) ).
cnf(c121,plain,
( in(sk27(X0,X1,X3),X1)
| ~ in(X3,sk25(X0,X1))
| sk20(X0,X1) = sk22(X0,X1)
| ~ element(X1,powerset(powerset(succ(X0))))
| ~ ordinal(X0) ),
inference(cnf_transformation,[status(esa)],[f41_sk]) ).
cnf(p912,plain,
( in(sk27(sk0,X0,X1),X0)
| ~ in(X1,sk25(sk0,X0))
| sk20(sk0,X0) = sk22(sk0,X0)
| ~ element(X0,powerset(powerset(succ(sk0)))) ),
inference(resolution,[status(thm)],[c121,c0]) ).
cnf(p1964,plain,
( in(sk27(sk0,sk1,X0),sk1)
| ~ in(X0,sk25(sk0,sk1))
| sk20(sk0,sk1) = sk22(sk0,sk1) ),
inference(resolution,[status(thm)],[p912,c1]) ).
cnf(p7309,plain,
( in(sk27(sk0,sk1,sk2(sk25(sk0,sk1))),sk1)
| sk20(sk0,sk1) = sk22(sk0,sk1)
| sk20(sk0,sk1) = sk22(sk0,sk1) ),
inference(resolution,[status(thm)],[p7306,p1964]) ).
cnf(p7324,plain,
( in(sk27(sk0,sk1,sk2(sk25(sk0,sk1))),sk1)
| sk20(sk0,sk1) = sk22(sk0,sk1) ),
inference(factoring,[status(thm)],[p7309]) ).
cnf(c120,plain,
( sk26(X0,X1,X3) = X3
| ~ in(X3,sk25(X0,X1))
| sk20(X0,X1) = sk22(X0,X1)
| ~ element(X1,powerset(powerset(succ(X0))))
| ~ ordinal(X0) ),
inference(cnf_transformation,[status(esa)],[f41_sk]) ).
cnf(p862,plain,
( sk26(sk0,X0,X1) = X1
| ~ in(X1,sk25(sk0,X0))
| sk20(sk0,X0) = sk22(sk0,X0)
| ~ element(X0,powerset(powerset(succ(sk0)))) ),
inference(resolution,[status(thm)],[c120,c0]) ).
cnf(p1949,plain,
( sk26(sk0,sk1,X0) = X0
| ~ in(X0,sk25(sk0,sk1))
| sk20(sk0,sk1) = sk22(sk0,sk1) ),
inference(resolution,[status(thm)],[p862,c1]) ).
cnf(p1955,plain,
( in(sk2(sk25(sk0,sk1)),powerset(sk0))
| sk26(sk0,sk1,sk2(sk25(sk0,sk1))) = sk2(sk25(sk0,sk1))
| sk20(sk0,sk1) = sk22(sk0,sk1) ),
inference(resolution,[status(thm)],[p1949,c3]) ).
cnf(c119,plain,
( in(sk26(X0,X1,X3),powerset(X0))
| ~ in(X3,sk25(X0,X1))
| sk20(X0,X1) = sk22(X0,X1)
| ~ element(X1,powerset(powerset(succ(X0))))
| ~ ordinal(X0) ),
inference(cnf_transformation,[status(esa)],[f41_sk]) ).
cnf(p839,plain,
( in(sk26(sk0,X0,X1),powerset(sk0))
| ~ in(X1,sk25(sk0,X0))
| sk20(sk0,X0) = sk22(sk0,X0)
| ~ element(X0,powerset(powerset(succ(sk0)))) ),
inference(resolution,[status(thm)],[c119,c0]) ).
cnf(p2110,plain,
( in(sk26(sk0,sk1,X0),powerset(sk0))
| ~ in(X0,sk25(sk0,sk1))
| sk20(sk0,sk1) = sk22(sk0,sk1) ),
inference(resolution,[status(thm)],[p839,c1]) ).
cnf(p2116,plain,
( in(sk2(sk25(sk0,sk1)),powerset(sk0))
| in(sk26(sk0,sk1,sk2(sk25(sk0,sk1))),powerset(sk0))
| sk20(sk0,sk1) = sk22(sk0,sk1) ),
inference(resolution,[status(thm)],[p2110,c3]) ).
cnf(p2145,plain,
( in(sk2(sk25(sk0,sk1)),powerset(sk0))
| in(sk2(sk25(sk0,sk1)),powerset(sk0))
| sk20(sk0,sk1) = sk22(sk0,sk1)
| in(sk2(sk25(sk0,sk1)),powerset(sk0))
| sk20(sk0,sk1) = sk22(sk0,sk1) ),
inference(superposition,[status(thm)],[p1955,p2116]) ).
cnf(p6865,plain,
( in(sk2(sk25(sk0,sk1)),powerset(sk0))
| in(sk2(sk25(sk0,sk1)),powerset(sk0))
| in(sk2(sk25(sk0,sk1)),powerset(sk0))
| sk20(sk0,sk1) = sk22(sk0,sk1) ),
inference(factoring,[status(thm)],[p2145]) ).
cnf(p6867,plain,
( in(sk2(sk25(sk0,sk1)),powerset(sk0))
| in(sk2(sk25(sk0,sk1)),powerset(sk0))
| sk20(sk0,sk1) = sk22(sk0,sk1) ),
inference(factoring,[status(thm)],[p6865]) ).
cnf(p6872,plain,
( in(sk2(sk25(sk0,sk1)),powerset(sk0))
| sk20(sk0,sk1) = sk22(sk0,sk1) ),
inference(factoring,[status(thm)],[p6867]) ).
cnf(c6,plain,
( ~ in(sk2(X2),X2)
| sk2(X2) != set_difference(X4,singleton(sk0))
| ~ in(X4,sk1)
| ~ in(sk2(X2),powerset(sk0)) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p6873,plain,
( ~ in(sk2(sk25(sk0,sk1)),sk25(sk0,sk1))
| sk2(sk25(sk0,sk1)) != set_difference(X0,singleton(sk0))
| ~ in(X0,sk1)
| sk20(sk0,sk1) = sk22(sk0,sk1) ),
inference(resolution,[status(thm)],[p6872,c6]) ).
cnf(p7328,plain,
( ~ in(sk2(sk25(sk0,sk1)),sk25(sk0,sk1))
| sk2(sk25(sk0,sk1)) != set_difference(sk27(sk0,sk1,sk2(sk25(sk0,sk1))),singleton(sk0))
| sk20(sk0,sk1) = sk22(sk0,sk1)
| sk20(sk0,sk1) = sk22(sk0,sk1) ),
inference(resolution,[status(thm)],[p7324,p6873]) ).
cnf(p12001,plain,
( ~ in(sk2(sk25(sk0,sk1)),sk25(sk0,sk1))
| sk2(sk25(sk0,sk1)) != set_difference(sk27(sk0,sk1,sk2(sk25(sk0,sk1))),singleton(sk0))
| sk20(sk0,sk1) = sk22(sk0,sk1) ),
inference(factoring,[status(thm)],[p7328]) ).
cnf(c122,plain,
( X3 = set_difference(sk27(X0,X1,X3),singleton(X0))
| ~ in(X3,sk25(X0,X1))
| sk20(X0,X1) = sk22(X0,X1)
| ~ element(X1,powerset(powerset(succ(X0))))
| ~ ordinal(X0) ),
inference(cnf_transformation,[status(esa)],[f41_sk]) ).
cnf(p966,plain,
( X1 = set_difference(sk27(sk0,X0,X1),singleton(sk0))
| ~ in(X1,sk25(sk0,X0))
| sk20(sk0,X0) = sk22(sk0,X0)
| ~ element(X0,powerset(powerset(succ(sk0)))) ),
inference(resolution,[status(thm)],[c122,c0]) ).
cnf(p2302,plain,
( X0 = set_difference(sk27(sk0,sk1,X0),singleton(sk0))
| ~ in(X0,sk25(sk0,sk1))
| sk20(sk0,sk1) = sk22(sk0,sk1) ),
inference(resolution,[status(thm)],[p966,c1]) ).
cnf(p7313,plain,
( sk2(sk25(sk0,sk1)) = set_difference(sk27(sk0,sk1,sk2(sk25(sk0,sk1))),singleton(sk0))
| sk20(sk0,sk1) = sk22(sk0,sk1)
| sk20(sk0,sk1) = sk22(sk0,sk1) ),
inference(resolution,[status(thm)],[p7306,p2302]) ).
cnf(p7349,plain,
( sk2(sk25(sk0,sk1)) = set_difference(sk27(sk0,sk1,sk2(sk25(sk0,sk1))),singleton(sk0))
| sk20(sk0,sk1) = sk22(sk0,sk1) ),
inference(factoring,[status(thm)],[p7313]) ).
cnf(p12006,plain,
( sk20(sk0,sk1) = sk22(sk0,sk1)
| ~ in(sk2(sk25(sk0,sk1)),sk25(sk0,sk1))
| sk20(sk0,sk1) = sk22(sk0,sk1) ),
inference(resolution,[status(thm)],[p12001,p7349]) ).
cnf(p12009,plain,
( ~ in(sk2(sk25(sk0,sk1)),sk25(sk0,sk1))
| sk20(sk0,sk1) = sk22(sk0,sk1) ),
inference(factoring,[status(thm)],[p12006]) ).
cnf(c108,plain,
( X3 != set_difference(X7,singleton(X0))
| ~ in(X7,X1)
| X4 != X3
| ~ in(X4,powerset(X0))
| in(X3,sk25(X0,X1))
| sk20(X0,X1) = sk21(X0,X1)
| ~ element(X1,powerset(powerset(succ(X0))))
| ~ ordinal(X0) ),
inference(cnf_transformation,[status(esa)],[f41_sk]) ).
cnf(p478,plain,
( X1 != set_difference(X3,singleton(sk0))
| ~ in(X3,X0)
| X2 != X1
| ~ in(X2,powerset(sk0))
| in(X1,sk25(sk0,X0))
| sk20(sk0,X0) = sk21(sk0,X0)
| ~ element(X0,powerset(powerset(succ(sk0)))) ),
inference(resolution,[status(thm)],[c108,c0]) ).
cnf(p5606,plain,
( X0 != set_difference(X2,singleton(sk0))
| ~ in(X2,sk1)
| X1 != X0
| ~ in(X1,powerset(sk0))
| in(X0,sk25(sk0,sk1))
| sk20(sk0,sk1) = sk21(sk0,sk1) ),
inference(resolution,[status(thm)],[p478,c1]) ).
cnf(p5629,plain,
( X0 != set_difference(X1,singleton(sk0))
| ~ in(X1,sk1)
| ~ in(X0,powerset(sk0))
| in(X0,sk25(sk0,sk1))
| sk20(sk0,sk1) = sk21(sk0,sk1) ),
inference(equality_resolution,[status(thm)],[p5606]) ).
cnf(p5645,plain,
( in(sk2(X0),X0)
| sk2(X0) != set_difference(X1,singleton(sk0))
| ~ in(X1,sk1)
| in(sk2(X0),sk25(sk0,sk1))
| sk20(sk0,sk1) = sk21(sk0,sk1) ),
inference(resolution,[status(thm)],[p5629,c3]) ).
cnf(p5663,plain,
( sk2(sk25(sk0,sk1)) != set_difference(X0,singleton(sk0))
| ~ in(X0,sk1)
| in(sk2(sk25(sk0,sk1)),sk25(sk0,sk1))
| sk20(sk0,sk1) = sk21(sk0,sk1) ),
inference(factoring,[status(thm)],[p5645]) ).
cnf(p5680,plain,
( in(sk2(X0),X0)
| sk2(sk25(sk0,sk1)) != set_difference(sk3(X0),singleton(sk0))
| in(sk2(sk25(sk0,sk1)),sk25(sk0,sk1))
| sk20(sk0,sk1) = sk21(sk0,sk1) ),
inference(resolution,[status(thm)],[p5663,c4]) ).
cnf(p5695,plain,
( sk2(sk25(sk0,sk1)) != set_difference(sk3(sk25(sk0,sk1)),singleton(sk0))
| in(sk2(sk25(sk0,sk1)),sk25(sk0,sk1))
| sk20(sk0,sk1) = sk21(sk0,sk1) ),
inference(factoring,[status(thm)],[p5680]) ).
cnf(p5698,plain,
( in(sk2(sk25(sk0,sk1)),sk25(sk0,sk1))
| in(sk2(sk25(sk0,sk1)),sk25(sk0,sk1))
| sk20(sk0,sk1) = sk21(sk0,sk1) ),
inference(resolution,[status(thm)],[p5695,c5]) ).
cnf(p5703,plain,
( in(sk2(sk25(sk0,sk1)),sk25(sk0,sk1))
| sk20(sk0,sk1) = sk21(sk0,sk1) ),
inference(factoring,[status(thm)],[p5698]) ).
cnf(c105,plain,
( sk26(X0,X1,X3) = X3
| ~ in(X3,sk25(X0,X1))
| sk20(X0,X1) = sk21(X0,X1)
| ~ element(X1,powerset(powerset(succ(X0))))
| ~ ordinal(X0) ),
inference(cnf_transformation,[status(esa)],[f41_sk]) ).
cnf(p402,plain,
( sk26(sk0,X0,X1) = X1
| ~ in(X1,sk25(sk0,X0))
| sk20(sk0,X0) = sk21(sk0,X0)
| ~ element(X0,powerset(powerset(succ(sk0)))) ),
inference(resolution,[status(thm)],[c105,c0]) ).
cnf(p1915,plain,
( sk26(sk0,sk1,X0) = X0
| ~ in(X0,sk25(sk0,sk1))
| sk20(sk0,sk1) = sk21(sk0,sk1) ),
inference(resolution,[status(thm)],[p402,c1]) ).
cnf(p5705,plain,
( sk26(sk0,sk1,sk2(sk25(sk0,sk1))) = sk2(sk25(sk0,sk1))
| sk20(sk0,sk1) = sk21(sk0,sk1)
| sk20(sk0,sk1) = sk21(sk0,sk1) ),
inference(resolution,[status(thm)],[p5703,p1915]) ).
cnf(p5756,plain,
( sk26(sk0,sk1,sk2(sk25(sk0,sk1))) = sk2(sk25(sk0,sk1))
| sk20(sk0,sk1) = sk21(sk0,sk1) ),
inference(factoring,[status(thm)],[p5705]) ).
cnf(c104,plain,
( in(sk26(X0,X1,X3),powerset(X0))
| ~ in(X3,sk25(X0,X1))
| sk20(X0,X1) = sk21(X0,X1)
| ~ element(X1,powerset(powerset(succ(X0))))
| ~ ordinal(X0) ),
inference(cnf_transformation,[status(esa)],[f41_sk]) ).
cnf(p378,plain,
( in(sk26(sk0,X0,X1),powerset(sk0))
| ~ in(X1,sk25(sk0,X0))
| sk20(sk0,X0) = sk21(sk0,X0)
| ~ element(X0,powerset(powerset(succ(sk0)))) ),
inference(resolution,[status(thm)],[c104,c0]) ).
cnf(p2072,plain,
( in(sk26(sk0,sk1,X0),powerset(sk0))
| ~ in(X0,sk25(sk0,sk1))
| sk20(sk0,sk1) = sk21(sk0,sk1) ),
inference(resolution,[status(thm)],[p378,c1]) ).
cnf(p5709,plain,
( in(sk26(sk0,sk1,sk2(sk25(sk0,sk1))),powerset(sk0))
| sk20(sk0,sk1) = sk21(sk0,sk1)
| sk20(sk0,sk1) = sk21(sk0,sk1) ),
inference(resolution,[status(thm)],[p5703,p2072]) ).
cnf(p5739,plain,
( in(sk26(sk0,sk1,sk2(sk25(sk0,sk1))),powerset(sk0))
| sk20(sk0,sk1) = sk21(sk0,sk1) ),
inference(factoring,[status(thm)],[p5709]) ).
cnf(p5757,plain,
( in(sk2(sk25(sk0,sk1)),powerset(sk0))
| sk20(sk0,sk1) = sk21(sk0,sk1)
| sk20(sk0,sk1) = sk21(sk0,sk1) ),
inference(superposition,[status(thm)],[p5756,p5739]) ).
cnf(p5763,plain,
( in(sk2(sk25(sk0,sk1)),powerset(sk0))
| sk20(sk0,sk1) = sk21(sk0,sk1) ),
inference(factoring,[status(thm)],[p5757]) ).
cnf(p5764,plain,
( ~ in(sk2(sk25(sk0,sk1)),sk25(sk0,sk1))
| sk2(sk25(sk0,sk1)) != set_difference(X0,singleton(sk0))
| ~ in(X0,sk1)
| sk20(sk0,sk1) = sk21(sk0,sk1) ),
inference(resolution,[status(thm)],[p5763,c6]) ).
cnf(c106,plain,
( in(sk27(X0,X1,X3),X1)
| ~ in(X3,sk25(X0,X1))
| sk20(X0,X1) = sk21(X0,X1)
| ~ element(X1,powerset(powerset(succ(X0))))
| ~ ordinal(X0) ),
inference(cnf_transformation,[status(esa)],[f41_sk]) ).
cnf(p428,plain,
( in(sk27(sk0,X0,X1),X0)
| ~ in(X1,sk25(sk0,X0))
| sk20(sk0,X0) = sk21(sk0,X0)
| ~ element(X0,powerset(powerset(succ(sk0)))) ),
inference(resolution,[status(thm)],[c106,c0]) ).
cnf(p1930,plain,
( in(sk27(sk0,sk1,X0),sk1)
| ~ in(X0,sk25(sk0,sk1))
| sk20(sk0,sk1) = sk21(sk0,sk1) ),
inference(resolution,[status(thm)],[p428,c1]) ).
cnf(p5706,plain,
( in(sk27(sk0,sk1,sk2(sk25(sk0,sk1))),sk1)
| sk20(sk0,sk1) = sk21(sk0,sk1)
| sk20(sk0,sk1) = sk21(sk0,sk1) ),
inference(resolution,[status(thm)],[p5703,p1930]) ).
cnf(p5721,plain,
( in(sk27(sk0,sk1,sk2(sk25(sk0,sk1))),sk1)
| sk20(sk0,sk1) = sk21(sk0,sk1) ),
inference(factoring,[status(thm)],[p5706]) ).
cnf(p5774,plain,
( sk20(sk0,sk1) = sk21(sk0,sk1)
| ~ in(sk2(sk25(sk0,sk1)),sk25(sk0,sk1))
| sk2(sk25(sk0,sk1)) != set_difference(sk27(sk0,sk1,sk2(sk25(sk0,sk1))),singleton(sk0))
| sk20(sk0,sk1) = sk21(sk0,sk1) ),
inference(resolution,[status(thm)],[p5764,p5721]) ).
cnf(p9848,plain,
( ~ in(sk2(sk25(sk0,sk1)),sk25(sk0,sk1))
| sk2(sk25(sk0,sk1)) != set_difference(sk27(sk0,sk1,sk2(sk25(sk0,sk1))),singleton(sk0))
| sk20(sk0,sk1) = sk21(sk0,sk1) ),
inference(factoring,[status(thm)],[p5774]) ).
cnf(c107,plain,
( X3 = set_difference(sk27(X0,X1,X3),singleton(X0))
| ~ in(X3,sk25(X0,X1))
| sk20(X0,X1) = sk21(X0,X1)
| ~ element(X1,powerset(powerset(succ(X0))))
| ~ ordinal(X0) ),
inference(cnf_transformation,[status(esa)],[f41_sk]) ).
cnf(p458,plain,
( X1 = set_difference(sk27(sk0,X0,X1),singleton(sk0))
| ~ in(X1,sk25(sk0,X0))
| sk20(sk0,X0) = sk21(sk0,X0)
| ~ element(X0,powerset(powerset(succ(sk0)))) ),
inference(resolution,[status(thm)],[c107,c0]) ).
cnf(p2276,plain,
( X0 = set_difference(sk27(sk0,sk1,X0),singleton(sk0))
| ~ in(X0,sk25(sk0,sk1))
| sk20(sk0,sk1) = sk21(sk0,sk1) ),
inference(resolution,[status(thm)],[p458,c1]) ).
cnf(p5711,plain,
( sk2(sk25(sk0,sk1)) = set_difference(sk27(sk0,sk1,sk2(sk25(sk0,sk1))),singleton(sk0))
| sk20(sk0,sk1) = sk21(sk0,sk1)
| sk20(sk0,sk1) = sk21(sk0,sk1) ),
inference(resolution,[status(thm)],[p5703,p2276]) ).
cnf(p5779,plain,
( sk2(sk25(sk0,sk1)) = set_difference(sk27(sk0,sk1,sk2(sk25(sk0,sk1))),singleton(sk0))
| sk20(sk0,sk1) = sk21(sk0,sk1) ),
inference(factoring,[status(thm)],[p5711]) ).
cnf(p9853,plain,
( sk20(sk0,sk1) = sk21(sk0,sk1)
| ~ in(sk2(sk25(sk0,sk1)),sk25(sk0,sk1))
| sk20(sk0,sk1) = sk21(sk0,sk1) ),
inference(resolution,[status(thm)],[p9848,p5779]) ).
cnf(p9855,plain,
( ~ in(sk2(sk25(sk0,sk1)),sk25(sk0,sk1))
| sk20(sk0,sk1) = sk21(sk0,sk1) ),
inference(factoring,[status(thm)],[p9853]) ).
cnf(p9856,plain,
( sk20(sk0,sk1) = sk21(sk0,sk1)
| sk20(sk0,sk1) = sk21(sk0,sk1) ),
inference(resolution,[status(thm)],[p9855,p5703]) ).
cnf(p9858,plain,
sk20(sk0,sk1) = sk21(sk0,sk1),
inference(factoring,[status(thm)],[p9856]) ).
cnf(c138,plain,
( X3 != set_difference(X7,singleton(X0))
| ~ in(X7,X1)
| X4 != X3
| ~ in(X4,powerset(X0))
| in(X3,sk25(X0,X1))
| sk21(X0,X1) != sk22(X0,X1)
| ~ element(X1,powerset(powerset(succ(X0))))
| ~ ordinal(X0) ),
inference(cnf_transformation,[status(esa)],[f41_sk]) ).
cnf(p1729,plain,
( X1 != set_difference(X3,singleton(sk0))
| ~ in(X3,X0)
| X2 != X1
| ~ in(X2,powerset(sk0))
| in(X1,sk25(sk0,X0))
| sk21(sk0,X0) != sk22(sk0,X0)
| ~ element(X0,powerset(powerset(succ(sk0)))) ),
inference(resolution,[status(thm)],[c138,c0]) ).
cnf(p9391,plain,
( X0 != set_difference(X2,singleton(sk0))
| ~ in(X2,sk1)
| X1 != X0
| ~ in(X1,powerset(sk0))
| in(X0,sk25(sk0,sk1))
| sk21(sk0,sk1) != sk22(sk0,sk1) ),
inference(resolution,[status(thm)],[p1729,c1]) ).
cnf(p9398,plain,
( X0 != set_difference(X1,singleton(sk0))
| ~ in(X1,sk1)
| ~ in(X0,powerset(sk0))
| in(X0,sk25(sk0,sk1))
| sk21(sk0,sk1) != sk22(sk0,sk1) ),
inference(equality_resolution,[status(thm)],[p9391]) ).
cnf(p9872,plain,
( X0 != set_difference(X1,singleton(sk0))
| ~ in(X1,sk1)
| ~ in(X0,powerset(sk0))
| in(X0,sk25(sk0,sk1))
| sk20(sk0,sk1) != sk22(sk0,sk1) ),
inference(superposition,[status(thm)],[p9858,p9398]) ).
cnf(p7235,plain,
( ~ in(X0,sk1)
| ~ in(set_difference(X0,singleton(sk0)),powerset(sk0))
| in(set_difference(X0,singleton(sk0)),sk25(sk0,sk1))
| sk20(sk0,sk1) = sk22(sk0,sk1) ),
inference(equality_resolution,[status(thm)],[p7214]) ).
cnf(p7252,plain,
( ~ in(sk3(X0),sk1)
| ~ in(sk2(X0),powerset(sk0))
| in(set_difference(sk3(X0),singleton(sk0)),sk25(sk0,sk1))
| sk20(sk0,sk1) = sk22(sk0,sk1)
| in(sk2(X0),X0) ),
inference(superposition,[status(thm)],[c5,p7235]) ).
cnf(p7364,plain,
( in(sk2(X0),X0)
| ~ in(sk3(X0),sk1)
| in(set_difference(sk3(X0),singleton(sk0)),sk25(sk0,sk1))
| sk20(sk0,sk1) = sk22(sk0,sk1)
| in(sk2(X0),X0) ),
inference(resolution,[status(thm)],[p7252,c3]) ).
cnf(p7365,plain,
( ~ in(sk3(X0),sk1)
| in(set_difference(sk3(X0),singleton(sk0)),sk25(sk0,sk1))
| sk20(sk0,sk1) = sk22(sk0,sk1)
| in(sk2(X0),X0) ),
inference(factoring,[status(thm)],[p7364]) ).
cnf(p7370,plain,
( in(sk2(X0),X0)
| in(set_difference(sk3(X0),singleton(sk0)),sk25(sk0,sk1))
| sk20(sk0,sk1) = sk22(sk0,sk1)
| in(sk2(X0),X0) ),
inference(resolution,[status(thm)],[p7365,c4]) ).
cnf(p7371,plain,
( in(set_difference(sk3(X0),singleton(sk0)),sk25(sk0,sk1))
| sk20(sk0,sk1) = sk22(sk0,sk1)
| in(sk2(X0),X0) ),
inference(factoring,[status(thm)],[p7370]) ).
cnf(p7372,plain,
( in(sk2(X0),sk25(sk0,sk1))
| sk20(sk0,sk1) = sk22(sk0,sk1)
| in(sk2(X0),X0)
| in(sk2(X0),X0) ),
inference(superposition,[status(thm)],[c5,p7371]) ).
cnf(p7481,plain,
( in(sk2(X0),sk25(sk0,sk1))
| sk20(sk0,sk1) = sk22(sk0,sk1)
| in(sk2(X0),X0) ),
inference(factoring,[status(thm)],[p7372]) ).
cnf(p9890,plain,
( in(sk2(X2),sk25(sk0,sk1))
| in(sk2(X2),X2)
| X0 != set_difference(X1,singleton(sk0))
| ~ in(X1,sk1)
| ~ in(X0,powerset(sk0))
| in(X0,sk25(sk0,sk1)) ),
inference(resolution,[status(thm)],[p9872,p7481]) ).
cnf(p9902,plain,
( in(sk2(X0),X0)
| sk2(X0) != set_difference(X1,singleton(sk0))
| ~ in(X1,sk1)
| ~ in(sk2(X0),powerset(sk0))
| in(sk2(X0),sk25(sk0,sk1)) ),
inference(factoring,[status(thm)],[p9890]) ).
cnf(p9921,plain,
( in(sk2(X0),X0)
| in(sk2(X0),X0)
| sk2(X0) != set_difference(X1,singleton(sk0))
| ~ in(X1,sk1)
| in(sk2(X0),sk25(sk0,sk1)) ),
inference(resolution,[status(thm)],[p9902,c3]) ).
cnf(p9923,plain,
( in(sk2(X0),X0)
| sk2(X0) != set_difference(X1,singleton(sk0))
| ~ in(X1,sk1)
| in(sk2(X0),sk25(sk0,sk1)) ),
inference(factoring,[status(thm)],[p9921]) ).
cnf(p9928,plain,
( sk2(sk25(sk0,sk1)) != set_difference(X0,singleton(sk0))
| ~ in(X0,sk1)
| in(sk2(sk25(sk0,sk1)),sk25(sk0,sk1)) ),
inference(factoring,[status(thm)],[p9923]) ).
cnf(p1954,plain,
( in(sk3(sk25(sk0,sk1)),sk1)
| sk26(sk0,sk1,sk2(sk25(sk0,sk1))) = sk2(sk25(sk0,sk1))
| sk20(sk0,sk1) = sk22(sk0,sk1) ),
inference(resolution,[status(thm)],[p1949,c4]) ).
cnf(p2115,plain,
( in(sk3(sk25(sk0,sk1)),sk1)
| in(sk26(sk0,sk1,sk2(sk25(sk0,sk1))),powerset(sk0))
| sk20(sk0,sk1) = sk22(sk0,sk1) ),
inference(resolution,[status(thm)],[p2110,c4]) ).
cnf(p2118,plain,
( in(sk3(sk25(sk0,sk1)),sk1)
| in(sk2(sk25(sk0,sk1)),powerset(sk0))
| sk20(sk0,sk1) = sk22(sk0,sk1)
| in(sk3(sk25(sk0,sk1)),sk1)
| sk20(sk0,sk1) = sk22(sk0,sk1) ),
inference(superposition,[status(thm)],[p1954,p2115]) ).
cnf(p3405,plain,
( in(sk3(sk25(sk0,sk1)),sk1)
| in(sk2(sk25(sk0,sk1)),powerset(sk0))
| in(sk3(sk25(sk0,sk1)),sk1)
| sk20(sk0,sk1) = sk22(sk0,sk1) ),
inference(factoring,[status(thm)],[p2118]) ).
cnf(p3407,plain,
( in(sk2(sk25(sk0,sk1)),powerset(sk0))
| in(sk3(sk25(sk0,sk1)),sk1)
| sk20(sk0,sk1) = sk22(sk0,sk1) ),
inference(factoring,[status(thm)],[p3405]) ).
cnf(c8,plain,
( in(sk3(X2),sk1)
| sk2(X2) != set_difference(X4,singleton(sk0))
| ~ in(X4,sk1)
| ~ in(sk2(X2),powerset(sk0)) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p3454,plain,
( in(sk3(sk25(sk0,sk1)),sk1)
| sk2(sk25(sk0,sk1)) != set_difference(X0,singleton(sk0))
| ~ in(X0,sk1)
| in(sk3(sk25(sk0,sk1)),sk1)
| sk20(sk0,sk1) = sk22(sk0,sk1) ),
inference(resolution,[status(thm)],[p3407,c8]) ).
cnf(p3457,plain,
( sk2(sk25(sk0,sk1)) != set_difference(X0,singleton(sk0))
| ~ in(X0,sk1)
| in(sk3(sk25(sk0,sk1)),sk1)
| sk20(sk0,sk1) = sk22(sk0,sk1) ),
inference(factoring,[status(thm)],[p3454]) ).
cnf(p7327,plain,
( sk2(sk25(sk0,sk1)) != set_difference(sk27(sk0,sk1,sk2(sk25(sk0,sk1))),singleton(sk0))
| in(sk3(sk25(sk0,sk1)),sk1)
| sk20(sk0,sk1) = sk22(sk0,sk1)
| sk20(sk0,sk1) = sk22(sk0,sk1) ),
inference(resolution,[status(thm)],[p7324,p3457]) ).
cnf(p9019,plain,
( sk2(sk25(sk0,sk1)) != set_difference(sk27(sk0,sk1,sk2(sk25(sk0,sk1))),singleton(sk0))
| in(sk3(sk25(sk0,sk1)),sk1)
| sk20(sk0,sk1) = sk22(sk0,sk1) ),
inference(factoring,[status(thm)],[p7327]) ).
cnf(p9022,plain,
( sk20(sk0,sk1) = sk22(sk0,sk1)
| in(sk3(sk25(sk0,sk1)),sk1)
| sk20(sk0,sk1) = sk22(sk0,sk1) ),
inference(resolution,[status(thm)],[p9019,p7349]) ).
cnf(p9023,plain,
( in(sk3(sk25(sk0,sk1)),sk1)
| sk20(sk0,sk1) = sk22(sk0,sk1) ),
inference(factoring,[status(thm)],[p9022]) ).
cnf(p1920,plain,
( in(sk3(sk25(sk0,sk1)),sk1)
| sk26(sk0,sk1,sk2(sk25(sk0,sk1))) = sk2(sk25(sk0,sk1))
| sk20(sk0,sk1) = sk21(sk0,sk1) ),
inference(resolution,[status(thm)],[p1915,c4]) ).
cnf(p2077,plain,
( in(sk3(sk25(sk0,sk1)),sk1)
| in(sk26(sk0,sk1,sk2(sk25(sk0,sk1))),powerset(sk0))
| sk20(sk0,sk1) = sk21(sk0,sk1) ),
inference(resolution,[status(thm)],[p2072,c4]) ).
cnf(p2080,plain,
( in(sk3(sk25(sk0,sk1)),sk1)
| in(sk2(sk25(sk0,sk1)),powerset(sk0))
| sk20(sk0,sk1) = sk21(sk0,sk1)
| in(sk3(sk25(sk0,sk1)),sk1)
| sk20(sk0,sk1) = sk21(sk0,sk1) ),
inference(superposition,[status(thm)],[p1920,p2077]) ).
cnf(p3255,plain,
( in(sk3(sk25(sk0,sk1)),sk1)
| in(sk2(sk25(sk0,sk1)),powerset(sk0))
| in(sk3(sk25(sk0,sk1)),sk1)
| sk20(sk0,sk1) = sk21(sk0,sk1) ),
inference(factoring,[status(thm)],[p2080]) ).
cnf(p3302,plain,
( in(sk2(sk25(sk0,sk1)),powerset(sk0))
| in(sk3(sk25(sk0,sk1)),sk1)
| sk20(sk0,sk1) = sk21(sk0,sk1) ),
inference(factoring,[status(thm)],[p3255]) ).
cnf(p3304,plain,
( in(sk3(sk25(sk0,sk1)),sk1)
| sk2(sk25(sk0,sk1)) != set_difference(X0,singleton(sk0))
| ~ in(X0,sk1)
| in(sk3(sk25(sk0,sk1)),sk1)
| sk20(sk0,sk1) = sk21(sk0,sk1) ),
inference(resolution,[status(thm)],[p3302,c8]) ).
cnf(p3307,plain,
( sk2(sk25(sk0,sk1)) != set_difference(X0,singleton(sk0))
| ~ in(X0,sk1)
| in(sk3(sk25(sk0,sk1)),sk1)
| sk20(sk0,sk1) = sk21(sk0,sk1) ),
inference(factoring,[status(thm)],[p3304]) ).
cnf(p5728,plain,
( sk2(sk25(sk0,sk1)) != set_difference(sk27(sk0,sk1,sk2(sk25(sk0,sk1))),singleton(sk0))
| in(sk3(sk25(sk0,sk1)),sk1)
| sk20(sk0,sk1) = sk21(sk0,sk1)
| sk20(sk0,sk1) = sk21(sk0,sk1) ),
inference(resolution,[status(thm)],[p5721,p3307]) ).
cnf(p6785,plain,
( sk2(sk25(sk0,sk1)) != set_difference(sk27(sk0,sk1,sk2(sk25(sk0,sk1))),singleton(sk0))
| in(sk3(sk25(sk0,sk1)),sk1)
| sk20(sk0,sk1) = sk21(sk0,sk1) ),
inference(factoring,[status(thm)],[p5728]) ).
cnf(p6789,plain,
( sk20(sk0,sk1) = sk21(sk0,sk1)
| in(sk3(sk25(sk0,sk1)),sk1)
| sk20(sk0,sk1) = sk21(sk0,sk1) ),
inference(resolution,[status(thm)],[p6785,p5779]) ).
cnf(p6790,plain,
( in(sk3(sk25(sk0,sk1)),sk1)
| sk20(sk0,sk1) = sk21(sk0,sk1) ),
inference(factoring,[status(thm)],[p6789]) ).
cnf(c137,plain,
( X3 = set_difference(sk27(X0,X1,X3),singleton(X0))
| ~ in(X3,sk25(X0,X1))
| sk21(X0,X1) != sk22(X0,X1)
| ~ element(X1,powerset(powerset(succ(X0))))
| ~ ordinal(X0) ),
inference(cnf_transformation,[status(esa)],[f41_sk]) ).
cnf(p1692,plain,
( X1 = set_difference(sk27(sk0,X0,X1),singleton(sk0))
| ~ in(X1,sk25(sk0,X0))
| sk21(sk0,X0) != sk22(sk0,X0)
| ~ element(X0,powerset(powerset(succ(sk0)))) ),
inference(resolution,[status(thm)],[c137,c0]) ).
cnf(p2333,plain,
( X0 = set_difference(sk27(sk0,sk1,X0),singleton(sk0))
| ~ in(X0,sk25(sk0,sk1))
| sk21(sk0,sk1) != sk22(sk0,sk1) ),
inference(resolution,[status(thm)],[p1692,c1]) ).
cnf(p6796,plain,
( X0 = set_difference(sk27(sk0,sk1,X0),singleton(sk0))
| ~ in(X0,sk25(sk0,sk1))
| sk20(sk0,sk1) != sk22(sk0,sk1)
| in(sk3(sk25(sk0,sk1)),sk1) ),
inference(superposition,[status(thm)],[p6790,p2333]) ).
cnf(p9035,plain,
( X0 = set_difference(sk27(sk0,sk1,X0),singleton(sk0))
| ~ in(X0,sk25(sk0,sk1))
| in(sk3(sk25(sk0,sk1)),sk1)
| in(sk3(sk25(sk0,sk1)),sk1) ),
inference(resolution,[status(thm)],[p9023,p6796]) ).
cnf(p9125,plain,
( X0 = set_difference(sk27(sk0,sk1,X0),singleton(sk0))
| ~ in(X0,sk25(sk0,sk1))
| in(sk3(sk25(sk0,sk1)),sk1) ),
inference(factoring,[status(thm)],[p9035]) ).
cnf(p9130,plain,
( in(sk3(sk25(sk0,sk1)),sk1)
| sk2(sk25(sk0,sk1)) = set_difference(sk27(sk0,sk1,sk2(sk25(sk0,sk1))),singleton(sk0))
| in(sk3(sk25(sk0,sk1)),sk1) ),
inference(resolution,[status(thm)],[p9125,c4]) ).
cnf(p9198,plain,
( sk2(sk25(sk0,sk1)) = set_difference(sk27(sk0,sk1,sk2(sk25(sk0,sk1))),singleton(sk0))
| in(sk3(sk25(sk0,sk1)),sk1) ),
inference(factoring,[status(thm)],[p9130]) ).
cnf(c135,plain,
( sk26(X0,X1,X3) = X3
| ~ in(X3,sk25(X0,X1))
| sk21(X0,X1) != sk22(X0,X1)
| ~ element(X1,powerset(powerset(succ(X0))))
| ~ ordinal(X0) ),
inference(cnf_transformation,[status(esa)],[f41_sk]) ).
cnf(p1610,plain,
( sk26(sk0,X0,X1) = X1
| ~ in(X1,sk25(sk0,X0))
| sk21(sk0,X0) != sk22(sk0,X0)
| ~ element(X0,powerset(powerset(succ(sk0)))) ),
inference(resolution,[status(thm)],[c135,c0]) ).
cnf(p1991,plain,
( sk26(sk0,sk1,X0) = X0
| ~ in(X0,sk25(sk0,sk1))
| sk21(sk0,sk1) != sk22(sk0,sk1) ),
inference(resolution,[status(thm)],[p1610,c1]) ).
cnf(p6791,plain,
( sk26(sk0,sk1,X0) = X0
| ~ in(X0,sk25(sk0,sk1))
| sk20(sk0,sk1) != sk22(sk0,sk1)
| in(sk3(sk25(sk0,sk1)),sk1) ),
inference(superposition,[status(thm)],[p6790,p1991]) ).
cnf(p9032,plain,
( sk26(sk0,sk1,X0) = X0
| ~ in(X0,sk25(sk0,sk1))
| in(sk3(sk25(sk0,sk1)),sk1)
| in(sk3(sk25(sk0,sk1)),sk1) ),
inference(resolution,[status(thm)],[p9023,p6791]) ).
cnf(p9040,plain,
( sk26(sk0,sk1,X0) = X0
| ~ in(X0,sk25(sk0,sk1))
| in(sk3(sk25(sk0,sk1)),sk1) ),
inference(factoring,[status(thm)],[p9032]) ).
cnf(p9041,plain,
( in(sk3(sk25(sk0,sk1)),sk1)
| sk26(sk0,sk1,sk2(sk25(sk0,sk1))) = sk2(sk25(sk0,sk1))
| in(sk3(sk25(sk0,sk1)),sk1) ),
inference(resolution,[status(thm)],[p9040,c4]) ).
cnf(p9067,plain,
( sk26(sk0,sk1,sk2(sk25(sk0,sk1))) = sk2(sk25(sk0,sk1))
| in(sk3(sk25(sk0,sk1)),sk1) ),
inference(factoring,[status(thm)],[p9041]) ).
cnf(c134,plain,
( in(sk26(X0,X1,X3),powerset(X0))
| ~ in(X3,sk25(X0,X1))
| sk21(X0,X1) != sk22(X0,X1)
| ~ element(X1,powerset(powerset(succ(X0))))
| ~ ordinal(X0) ),
inference(cnf_transformation,[status(esa)],[f41_sk]) ).
cnf(p1572,plain,
( in(sk26(sk0,X0,X1),powerset(sk0))
| ~ in(X1,sk25(sk0,X0))
| sk21(sk0,X0) != sk22(sk0,X0)
| ~ element(X0,powerset(powerset(succ(sk0)))) ),
inference(resolution,[status(thm)],[c134,c0]) ).
cnf(p2136,plain,
( in(sk26(sk0,sk1,X0),powerset(sk0))
| ~ in(X0,sk25(sk0,sk1))
| sk21(sk0,sk1) != sk22(sk0,sk1) ),
inference(resolution,[status(thm)],[p1572,c1]) ).
cnf(p6793,plain,
( in(sk26(sk0,sk1,X0),powerset(sk0))
| ~ in(X0,sk25(sk0,sk1))
| sk20(sk0,sk1) != sk22(sk0,sk1)
| in(sk3(sk25(sk0,sk1)),sk1) ),
inference(superposition,[status(thm)],[p6790,p2136]) ).
cnf(p9034,plain,
( in(sk26(sk0,sk1,X0),powerset(sk0))
| ~ in(X0,sk25(sk0,sk1))
| in(sk3(sk25(sk0,sk1)),sk1)
| in(sk3(sk25(sk0,sk1)),sk1) ),
inference(resolution,[status(thm)],[p9023,p6793]) ).
cnf(p9080,plain,
( in(sk26(sk0,sk1,X0),powerset(sk0))
| ~ in(X0,sk25(sk0,sk1))
| in(sk3(sk25(sk0,sk1)),sk1) ),
inference(factoring,[status(thm)],[p9034]) ).
cnf(p9081,plain,
( in(sk3(sk25(sk0,sk1)),sk1)
| in(sk26(sk0,sk1,sk2(sk25(sk0,sk1))),powerset(sk0))
| in(sk3(sk25(sk0,sk1)),sk1) ),
inference(resolution,[status(thm)],[p9080,c4]) ).
cnf(p9087,plain,
( in(sk26(sk0,sk1,sk2(sk25(sk0,sk1))),powerset(sk0))
| in(sk3(sk25(sk0,sk1)),sk1) ),
inference(factoring,[status(thm)],[p9081]) ).
cnf(p9093,plain,
( in(sk2(sk25(sk0,sk1)),powerset(sk0))
| in(sk3(sk25(sk0,sk1)),sk1)
| in(sk3(sk25(sk0,sk1)),sk1) ),
inference(superposition,[status(thm)],[p9067,p9087]) ).
cnf(p9095,plain,
( in(sk2(sk25(sk0,sk1)),powerset(sk0))
| in(sk3(sk25(sk0,sk1)),sk1) ),
inference(factoring,[status(thm)],[p9093]) ).
cnf(p9101,plain,
( in(sk3(sk25(sk0,sk1)),sk1)
| sk2(sk25(sk0,sk1)) != set_difference(X0,singleton(sk0))
| ~ in(X0,sk1)
| in(sk3(sk25(sk0,sk1)),sk1) ),
inference(resolution,[status(thm)],[p9095,c8]) ).
cnf(p9108,plain,
( sk2(sk25(sk0,sk1)) != set_difference(X0,singleton(sk0))
| ~ in(X0,sk1)
| in(sk3(sk25(sk0,sk1)),sk1) ),
inference(factoring,[status(thm)],[p9101]) ).
cnf(c136,plain,
( in(sk27(X0,X1,X3),X1)
| ~ in(X3,sk25(X0,X1))
| sk21(X0,X1) != sk22(X0,X1)
| ~ element(X1,powerset(powerset(succ(X0))))
| ~ ordinal(X0) ),
inference(cnf_transformation,[status(esa)],[f41_sk]) ).
cnf(p1654,plain,
( in(sk27(sk0,X0,X1),X0)
| ~ in(X1,sk25(sk0,X0))
| sk21(sk0,X0) != sk22(sk0,X0)
| ~ element(X0,powerset(powerset(succ(sk0)))) ),
inference(resolution,[status(thm)],[c136,c0]) ).
cnf(p1997,plain,
( in(sk27(sk0,sk1,X0),sk1)
| ~ in(X0,sk25(sk0,sk1))
| sk21(sk0,sk1) != sk22(sk0,sk1) ),
inference(resolution,[status(thm)],[p1654,c1]) ).
cnf(p6792,plain,
( in(sk27(sk0,sk1,X0),sk1)
| ~ in(X0,sk25(sk0,sk1))
| sk20(sk0,sk1) != sk22(sk0,sk1)
| in(sk3(sk25(sk0,sk1)),sk1) ),
inference(superposition,[status(thm)],[p6790,p1997]) ).
cnf(p9033,plain,
( in(sk27(sk0,sk1,X0),sk1)
| ~ in(X0,sk25(sk0,sk1))
| in(sk3(sk25(sk0,sk1)),sk1)
| in(sk3(sk25(sk0,sk1)),sk1) ),
inference(resolution,[status(thm)],[p9023,p6792]) ).
cnf(p9047,plain,
( in(sk27(sk0,sk1,X0),sk1)
| ~ in(X0,sk25(sk0,sk1))
| in(sk3(sk25(sk0,sk1)),sk1) ),
inference(factoring,[status(thm)],[p9033]) ).
cnf(p9048,plain,
( in(sk3(sk25(sk0,sk1)),sk1)
| in(sk27(sk0,sk1,sk2(sk25(sk0,sk1))),sk1)
| in(sk3(sk25(sk0,sk1)),sk1) ),
inference(resolution,[status(thm)],[p9047,c4]) ).
cnf(p9056,plain,
( in(sk27(sk0,sk1,sk2(sk25(sk0,sk1))),sk1)
| in(sk3(sk25(sk0,sk1)),sk1) ),
inference(factoring,[status(thm)],[p9048]) ).
cnf(p9114,plain,
( in(sk3(sk25(sk0,sk1)),sk1)
| sk2(sk25(sk0,sk1)) != set_difference(sk27(sk0,sk1,sk2(sk25(sk0,sk1))),singleton(sk0))
| in(sk3(sk25(sk0,sk1)),sk1) ),
inference(resolution,[status(thm)],[p9108,p9056]) ).
cnf(p9131,plain,
( sk2(sk25(sk0,sk1)) != set_difference(sk27(sk0,sk1,sk2(sk25(sk0,sk1))),singleton(sk0))
| in(sk3(sk25(sk0,sk1)),sk1) ),
inference(factoring,[status(thm)],[p9114]) ).
cnf(p9204,plain,
( in(sk3(sk25(sk0,sk1)),sk1)
| in(sk3(sk25(sk0,sk1)),sk1) ),
inference(resolution,[status(thm)],[p9198,p9131]) ).
cnf(p9205,plain,
in(sk3(sk25(sk0,sk1)),sk1),
inference(factoring,[status(thm)],[p9204]) ).
cnf(p9945,plain,
( sk2(sk25(sk0,sk1)) != set_difference(sk3(sk25(sk0,sk1)),singleton(sk0))
| in(sk2(sk25(sk0,sk1)),sk25(sk0,sk1)) ),
inference(resolution,[status(thm)],[p9928,p9205]) ).
cnf(p9946,plain,
( in(sk2(sk25(sk0,sk1)),sk25(sk0,sk1))
| in(sk2(sk25(sk0,sk1)),sk25(sk0,sk1)) ),
inference(resolution,[status(thm)],[p9945,c5]) ).
cnf(p9947,plain,
in(sk2(sk25(sk0,sk1)),sk25(sk0,sk1)),
inference(factoring,[status(thm)],[p9946]) ).
cnf(p12014,plain,
sk20(sk0,sk1) = sk22(sk0,sk1),
inference(resolution,[status(thm)],[p12009,p9947]) ).
cnf(p9865,plain,
( in(sk26(sk0,sk1,X0),powerset(sk0))
| ~ in(X0,sk25(sk0,sk1))
| sk20(sk0,sk1) != sk22(sk0,sk1) ),
inference(superposition,[status(thm)],[p9858,p2136]) ).
cnf(p12028,plain,
( in(sk26(sk0,sk1,X0),powerset(sk0))
| ~ in(X0,sk25(sk0,sk1)) ),
inference(resolution,[status(thm)],[p12014,p9865]) ).
cnf(p12179,plain,
in(sk2(sk25(sk0,sk1)),powerset(sk0)),
inference(resolution,[status(thm)],[p12028,p9947]) ).
cnf(p12181,plain,
( ~ in(sk2(sk25(sk0,sk1)),sk25(sk0,sk1))
| sk2(sk25(sk0,sk1)) != set_difference(X0,singleton(sk0))
| ~ in(X0,sk1) ),
inference(resolution,[status(thm)],[p12179,c6]) ).
cnf(p9864,plain,
( in(sk27(sk0,sk1,X0),sk1)
| ~ in(X0,sk25(sk0,sk1))
| sk20(sk0,sk1) != sk22(sk0,sk1) ),
inference(superposition,[status(thm)],[p9858,p1997]) ).
cnf(p12027,plain,
( in(sk27(sk0,sk1,X0),sk1)
| ~ in(X0,sk25(sk0,sk1)) ),
inference(resolution,[status(thm)],[p12014,p9864]) ).
cnf(p12056,plain,
in(sk27(sk0,sk1,sk2(sk25(sk0,sk1))),sk1),
inference(resolution,[status(thm)],[p12027,p9947]) ).
cnf(p12351,plain,
( ~ in(sk2(sk25(sk0,sk1)),sk25(sk0,sk1))
| sk2(sk25(sk0,sk1)) != set_difference(sk27(sk0,sk1,sk2(sk25(sk0,sk1))),singleton(sk0)) ),
inference(resolution,[status(thm)],[p12181,p12056]) ).
cnf(p9867,plain,
( X0 = set_difference(sk27(sk0,sk1,X0),singleton(sk0))
| ~ in(X0,sk25(sk0,sk1))
| sk20(sk0,sk1) != sk22(sk0,sk1) ),
inference(superposition,[status(thm)],[p9858,p2333]) ).
cnf(p12029,plain,
( X0 = set_difference(sk27(sk0,sk1,X0),singleton(sk0))
| ~ in(X0,sk25(sk0,sk1)) ),
inference(resolution,[status(thm)],[p12014,p9867]) ).
cnf(p12305,plain,
sk2(sk25(sk0,sk1)) = set_difference(sk27(sk0,sk1,sk2(sk25(sk0,sk1))),singleton(sk0)),
inference(resolution,[status(thm)],[p12029,p9947]) ).
cnf(p12382,plain,
~ in(sk2(sk25(sk0,sk1)),sk25(sk0,sk1)),
inference(resolution,[status(thm)],[p12351,p12305]) ).
cnf(p12383,plain,
$false,
inference(resolution,[status(thm)],[p12382,p9947]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU298+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.10/5.38 % Computer : n014.cluster.edu
% 0.10/5.38 % Model : x86_64 x86_64
% 0.10/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/5.38 % Memory : 8046.5625MB
% 0.10/5.38 % OS : Linux 6.8.0-71-generic
% 0.10/5.38 % CPULimit : 300
% 0.10/5.38 % WCLimit : 300
% 0.10/5.38 % DateTime : Thu Sep 24 13:36:09 UTC 2026
% 0.10/5.38 % CPUTime :
% 0.10/5.38 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 29.92/9.81 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 29.92/9.81 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------