%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SEU283+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 : n019.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:35 PM UTC 2026
% Result : Theorem 50.72s 7.71s
% Output : Proof 50.72s
% Verified :
% SZS Type : Refutation
% Derivation depth : 48
% Number of leaves : 4
% Syntax : Number of formulae : 147 ( 14 unt; 0 def)
% Number of atoms : 524 ( 248 equ)
% Maximal formula atoms : 15 ( 3 avg)
% Number of connectives : 554 ( 177 ~; 299 |; 61 &)
% ( 5 <=>; 12 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 4 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 2 con; 0-3 aty)
% Number of variables : 189 ( 10 sgn 55 !; 14 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f11,axiom,
! [A] :
( relation(A)
=> ! [B] :
( B = relation_dom(A)
<=> ! [C] :
( in(C,B)
<=> ? [D] : in(ordered_pair(C,D),A) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d4_relat_1) ).
fof(f11_nnf,plain,
! [A] :
( ! [B] :
( ( ? [C] :
( ( ? [D] : in(ordered_pair(C,D),A)
& ~ in(C,B) )
| ( ! [D] : ~ in(ordered_pair(C,D),A)
& in(C,B) ) )
| B = relation_dom(A) )
& ( ! [C] :
( ( ! [D] : ~ in(ordered_pair(C,D),A)
| in(C,B) )
& ( ? [D] : in(ordered_pair(C,D),A)
| ~ in(C,B) ) )
| B != relation_dom(A) ) )
| ~ relation(A) ),
inference(nnf_transformation,[status(thm)],[f11]) ).
fof(f11_sk,plain,
! [A,B,C,D] :
( ( ( ( in(ordered_pair(sk9(A,B),sk10(A,B)),A)
& ~ in(sk9(A,B),B) )
| ( ~ in(ordered_pair(sk9(A,B),D),A)
& in(sk9(A,B),B) )
| B = relation_dom(A) )
& ( ( ( ~ in(ordered_pair(C,D),A)
| in(C,B) )
& ( in(ordered_pair(C,sk8(A,B,C)),A)
| ~ in(C,B) ) )
| B != relation_dom(A) ) )
| ~ relation(A) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk8,sk9,sk10])],[f11_nnf]) ).
cnf(c50,plain,
( in(ordered_pair(sk9(X0,X1),sk10(X0,X1)),X0)
| in(sk9(X0,X1),X1)
| X1 = relation_dom(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(esa)],[f11_sk]) ).
fof(f6,axiom,
! [A] :
( ! [B,C,D] :
( ( D = singleton(B)
& in(B,A)
& C = singleton(B)
& in(B,A) )
=> C = D )
=> ? [B] :
( ! [C,D] :
( in(ordered_pair(C,D),B)
<=> ( D = singleton(C)
& in(C,A)
& in(C,A) ) )
& function(B)
& relation(B) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',s1_funct_1__e16_22__wellord2__1) ).
fof(f6_nnf,plain,
! [A] :
( ? [B] :
( ! [C,D] :
( ( D != singleton(C)
| ~ in(C,A)
| ~ in(C,A)
| in(ordered_pair(C,D),B) )
& ( ( D = singleton(C)
& in(C,A)
& in(C,A) )
| ~ in(ordered_pair(C,D),B) ) )
& function(B)
& relation(B) )
| ? [B,C,D] :
( C != D
& D = singleton(B)
& in(B,A)
& C = singleton(B)
& in(B,A) ) ),
inference(nnf_transformation,[status(thm)],[f6]) ).
fof(f6_sk,plain,
! [A,C,D] :
( ( ( D != singleton(C)
| ~ in(C,A)
| ~ in(C,A)
| in(ordered_pair(C,D),sk7(A)) )
& ( ( D = singleton(C)
& in(C,A)
& in(C,A) )
| ~ in(ordered_pair(C,D),sk7(A)) )
& function(sk7(A))
& relation(sk7(A)) )
| ( sk5(A) != sk6(A)
& sk6(A) = singleton(sk4(A))
& in(sk4(A),A)
& sk5(A) = singleton(sk4(A))
& in(sk4(A),A) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk4,sk5,sk6,sk7])],[f6_nnf]) ).
cnf(c34,plain,
( relation(sk7(X0))
| sk5(X0) != sk6(X0) ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(c28,plain,
( relation(sk7(X0))
| sk6(X0) = singleton(sk4(X0)) ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(c16,plain,
( relation(sk7(X0))
| sk5(X0) = singleton(sk4(X0)) ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(c10,plain,
( relation(sk7(X0))
| in(sk4(X0),X0) ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
fof(f0,conjecture,
! [A] :
( ( ! [B] :
~ ( ! [C] : C != singleton(B)
& in(B,A) )
& ! [B,C,D] :
( ( D = singleton(B)
& C = singleton(B)
& in(B,A) )
=> C = D ) )
=> ? [B] :
( ! [C] :
( in(C,A)
=> apply(B,C) = singleton(C) )
& relation_dom(B) = A
& function(B)
& relation(B) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',s2_funct_1__e16_22__wellord2__1) ).
fof(f0_neg,negated_conjecture,
~ ! [A] :
( ( ! [B] :
~ ( ! [C] : C != singleton(B)
& in(B,A) )
& ! [B,C,D] :
( ( D = singleton(B)
& C = singleton(B)
& in(B,A) )
=> C = D ) )
=> ? [B] :
( ! [C] :
( in(C,A)
=> apply(B,C) = singleton(C) )
& relation_dom(B) = A
& function(B)
& relation(B) ) ),
inference(negated_conjecture,[status(cth)],[f0]) ).
fof(f0_nnf,plain,
? [A] :
( ! [B] :
( ? [C] :
( apply(B,C) != singleton(C)
& in(C,A) )
| relation_dom(B) != A
| ~ function(B)
| ~ relation(B) )
& ! [B] :
( ? [C] : C = singleton(B)
| ~ in(B,A) )
& ! [B,C,D] :
( C = D
| D != singleton(B)
| C != singleton(B)
| ~ in(B,A) ) ),
inference(nnf_transformation,[status(thm)],[f0_neg]) ).
fof(f0_sk,plain,
! [B,C,D] :
( ( ( apply(B,sk2(B)) != singleton(sk2(B))
& in(sk2(B),sk0) )
| relation_dom(B) != sk0
| ~ function(B)
| ~ relation(B) )
& ( sk1(B) = singleton(B)
| ~ in(B,sk0) )
& ( C = D
| D != singleton(B)
| C != singleton(B)
| ~ in(B,sk0) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk0,sk1,sk2])],[f0_nnf]) ).
cnf(c0,plain,
( X2 = X3
| X3 != singleton(X1)
| X2 != singleton(X1)
| ~ in(X1,sk0) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p95,plain,
( X0 = X1
| X1 != singleton(sk4(sk0))
| X0 != singleton(sk4(sk0))
| relation(sk7(sk0)) ),
inference(resolution,[status(thm)],[c10,c0]) ).
cnf(p125,plain,
( sk5(sk0) = X0
| X0 != singleton(sk4(sk0))
| relation(sk7(sk0))
| relation(sk7(sk0)) ),
inference(resolution,[status(thm)],[c16,p95]) ).
cnf(p148,plain,
( sk5(sk0) = X0
| X0 != singleton(sk4(sk0))
| relation(sk7(sk0)) ),
inference(factoring,[status(thm)],[p125]) ).
cnf(p185,plain,
( sk5(sk0) = X0
| X0 != sk6(sk0)
| relation(sk7(sk0))
| relation(sk7(sk0)) ),
inference(superposition,[status(thm)],[c28,p148]) ).
cnf(p203,plain,
( sk5(sk0) = X0
| X0 != sk6(sk0)
| relation(sk7(sk0)) ),
inference(factoring,[status(thm)],[p185]) ).
cnf(p204,plain,
( sk5(sk0) = sk6(sk0)
| relation(sk7(sk0)) ),
inference(equality_resolution,[status(thm)],[p203]) ).
cnf(p218,plain,
( relation(sk7(sk0))
| relation(sk7(sk0)) ),
inference(resolution,[status(thm)],[c34,p204]) ).
cnf(p220,plain,
relation(sk7(sk0)),
inference(factoring,[status(thm)],[p218]) ).
cnf(p349,plain,
( in(ordered_pair(sk9(sk7(sk0),X0),sk10(sk7(sk0),X0)),sk7(sk0))
| in(sk9(sk7(sk0),X0),X0)
| X0 = relation_dom(sk7(sk0)) ),
inference(resolution,[status(thm)],[c50,p220]) ).
cnf(c30,plain,
( in(X2,X0)
| ~ in(ordered_pair(X2,X3),sk7(X0))
| sk6(X0) = singleton(sk4(X0)) ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(p436,plain,
( in(sk9(sk7(sk0),X0),sk0)
| sk6(sk0) = singleton(sk4(sk0))
| in(sk9(sk7(sk0),X0),X0)
| X0 = relation_dom(sk7(sk0)) ),
inference(resolution,[status(thm)],[p349,c30]) ).
cnf(p737,plain,
( sk6(sk0) = singleton(sk4(sk0))
| in(sk9(sk7(sk0),sk0),sk0)
| sk0 = relation_dom(sk7(sk0)) ),
inference(factoring,[status(thm)],[p436]) ).
cnf(c33,plain,
( X3 != singleton(X2)
| ~ in(X2,X0)
| ~ in(X2,X0)
| in(ordered_pair(X2,X3),sk7(X0))
| sk6(X0) = singleton(sk4(X0)) ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(p211,plain,
( X2 != singleton(X1)
| ~ in(X1,X0)
| in(ordered_pair(X1,X2),sk7(X0))
| sk6(X0) = singleton(sk4(X0)) ),
inference(factoring,[status(thm)],[c33]) ).
cnf(p784,plain,
( X0 != singleton(sk9(sk7(sk0),sk0))
| in(ordered_pair(sk9(sk7(sk0),sk0),X0),sk7(sk0))
| sk6(sk0) = singleton(sk4(sk0))
| sk6(sk0) = singleton(sk4(sk0))
| sk0 = relation_dom(sk7(sk0)) ),
inference(resolution,[status(thm)],[p737,p211]) ).
cnf(p5227,plain,
( X0 != singleton(sk9(sk7(sk0),sk0))
| in(ordered_pair(sk9(sk7(sk0),sk0),X0),sk7(sk0))
| sk6(sk0) = singleton(sk4(sk0))
| sk0 = relation_dom(sk7(sk0)) ),
inference(factoring,[status(thm)],[p784]) ).
cnf(p5774,plain,
( in(ordered_pair(sk9(sk7(sk0),sk0),singleton(sk9(sk7(sk0),sk0))),sk7(sk0))
| sk6(sk0) = singleton(sk4(sk0))
| sk0 = relation_dom(sk7(sk0)) ),
inference(equality_resolution,[status(thm)],[p5227]) ).
cnf(c51,plain,
( ~ in(sk9(X0,X1),X1)
| ~ in(ordered_pair(sk9(X0,X1),X3),X0)
| X1 = relation_dom(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(esa)],[f11_sk]) ).
cnf(p360,plain,
( ~ in(sk9(sk7(sk0),X0),X0)
| ~ in(ordered_pair(sk9(sk7(sk0),X0),X1),sk7(sk0))
| X0 = relation_dom(sk7(sk0)) ),
inference(resolution,[status(thm)],[c51,p220]) ).
cnf(p5780,plain,
( ~ in(sk9(sk7(sk0),sk0),sk0)
| sk0 = relation_dom(sk7(sk0))
| sk6(sk0) = singleton(sk4(sk0))
| sk0 = relation_dom(sk7(sk0)) ),
inference(resolution,[status(thm)],[p5774,p360]) ).
cnf(p5802,plain,
( ~ in(sk9(sk7(sk0),sk0),sk0)
| sk6(sk0) = singleton(sk4(sk0))
| sk0 = relation_dom(sk7(sk0)) ),
inference(factoring,[status(thm)],[p5780]) ).
cnf(p5803,plain,
( sk6(sk0) = singleton(sk4(sk0))
| sk0 = relation_dom(sk7(sk0))
| sk6(sk0) = singleton(sk4(sk0))
| sk0 = relation_dom(sk7(sk0)) ),
inference(resolution,[status(thm)],[p5802,p737]) ).
cnf(p5805,plain,
( sk0 = relation_dom(sk7(sk0))
| sk6(sk0) = singleton(sk4(sk0))
| sk0 = relation_dom(sk7(sk0)) ),
inference(factoring,[status(thm)],[p5803]) ).
cnf(p5806,plain,
( sk6(sk0) = singleton(sk4(sk0))
| sk0 = relation_dom(sk7(sk0)) ),
inference(factoring,[status(thm)],[p5805]) ).
cnf(c18,plain,
( in(X2,X0)
| ~ in(ordered_pair(X2,X3),sk7(X0))
| sk5(X0) = singleton(sk4(X0)) ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(p434,plain,
( in(sk9(sk7(sk0),X0),sk0)
| sk5(sk0) = singleton(sk4(sk0))
| in(sk9(sk7(sk0),X0),X0)
| X0 = relation_dom(sk7(sk0)) ),
inference(resolution,[status(thm)],[p349,c18]) ).
cnf(p711,plain,
( sk5(sk0) = singleton(sk4(sk0))
| in(sk9(sk7(sk0),sk0),sk0)
| sk0 = relation_dom(sk7(sk0)) ),
inference(factoring,[status(thm)],[p434]) ).
cnf(c21,plain,
( X3 != singleton(X2)
| ~ in(X2,X0)
| ~ in(X2,X0)
| in(ordered_pair(X2,X3),sk7(X0))
| sk5(X0) = singleton(sk4(X0)) ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(p152,plain,
( X2 != singleton(X1)
| ~ in(X1,X0)
| in(ordered_pair(X1,X2),sk7(X0))
| sk5(X0) = singleton(sk4(X0)) ),
inference(factoring,[status(thm)],[c21]) ).
cnf(p732,plain,
( X0 != singleton(sk9(sk7(sk0),sk0))
| in(ordered_pair(sk9(sk7(sk0),sk0),X0),sk7(sk0))
| sk5(sk0) = singleton(sk4(sk0))
| sk5(sk0) = singleton(sk4(sk0))
| sk0 = relation_dom(sk7(sk0)) ),
inference(resolution,[status(thm)],[p711,p152]) ).
cnf(p4085,plain,
( X0 != singleton(sk9(sk7(sk0),sk0))
| in(ordered_pair(sk9(sk7(sk0),sk0),X0),sk7(sk0))
| sk5(sk0) = singleton(sk4(sk0))
| sk0 = relation_dom(sk7(sk0)) ),
inference(factoring,[status(thm)],[p732]) ).
cnf(p5605,plain,
( in(ordered_pair(sk9(sk7(sk0),sk0),singleton(sk9(sk7(sk0),sk0))),sk7(sk0))
| sk5(sk0) = singleton(sk4(sk0))
| sk0 = relation_dom(sk7(sk0)) ),
inference(equality_resolution,[status(thm)],[p4085]) ).
cnf(p5612,plain,
( ~ in(sk9(sk7(sk0),sk0),sk0)
| sk0 = relation_dom(sk7(sk0))
| sk5(sk0) = singleton(sk4(sk0))
| sk0 = relation_dom(sk7(sk0)) ),
inference(resolution,[status(thm)],[p5605,p360]) ).
cnf(p5633,plain,
( ~ in(sk9(sk7(sk0),sk0),sk0)
| sk5(sk0) = singleton(sk4(sk0))
| sk0 = relation_dom(sk7(sk0)) ),
inference(factoring,[status(thm)],[p5612]) ).
cnf(p5634,plain,
( sk5(sk0) = singleton(sk4(sk0))
| sk0 = relation_dom(sk7(sk0))
| sk5(sk0) = singleton(sk4(sk0))
| sk0 = relation_dom(sk7(sk0)) ),
inference(resolution,[status(thm)],[p5633,p711]) ).
cnf(p5637,plain,
( sk0 = relation_dom(sk7(sk0))
| sk5(sk0) = singleton(sk4(sk0))
| sk0 = relation_dom(sk7(sk0)) ),
inference(factoring,[status(thm)],[p5634]) ).
cnf(p5659,plain,
( sk5(sk0) = singleton(sk4(sk0))
| sk0 = relation_dom(sk7(sk0)) ),
inference(factoring,[status(thm)],[p5637]) ).
cnf(p5822,plain,
( sk5(sk0) = sk6(sk0)
| sk0 = relation_dom(sk7(sk0))
| sk0 = relation_dom(sk7(sk0)) ),
inference(superposition,[status(thm)],[p5806,p5659]) ).
cnf(p5827,plain,
( sk5(sk0) = sk6(sk0)
| sk0 = relation_dom(sk7(sk0)) ),
inference(factoring,[status(thm)],[p5822]) ).
cnf(c36,plain,
( in(X2,X0)
| ~ in(ordered_pair(X2,X3),sk7(X0))
| sk5(X0) != sk6(X0) ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(p5829,plain,
( in(X0,sk0)
| ~ in(ordered_pair(X0,X1),sk7(sk0))
| sk0 = relation_dom(sk7(sk0)) ),
inference(resolution,[status(thm)],[p5827,c36]) ).
cnf(p5835,plain,
( in(sk9(sk7(sk0),X0),X0)
| X0 = relation_dom(sk7(sk0))
| in(sk9(sk7(sk0),X0),sk0)
| sk0 = relation_dom(sk7(sk0)) ),
inference(resolution,[status(thm)],[p5829,p349]) ).
cnf(p6308,plain,
( sk0 = relation_dom(sk7(sk0))
| in(sk9(sk7(sk0),sk0),sk0)
| sk0 = relation_dom(sk7(sk0)) ),
inference(factoring,[status(thm)],[p5835]) ).
cnf(p6329,plain,
( in(sk9(sk7(sk0),sk0),sk0)
| sk0 = relation_dom(sk7(sk0)) ),
inference(factoring,[status(thm)],[p6308]) ).
cnf(c39,plain,
( X3 != singleton(X2)
| ~ in(X2,X0)
| ~ in(X2,X0)
| in(ordered_pair(X2,X3),sk7(X0))
| sk5(X0) != sk6(X0) ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(p239,plain,
( X2 != singleton(X1)
| ~ in(X1,X0)
| in(ordered_pair(X1,X2),sk7(X0))
| sk5(X0) != sk6(X0) ),
inference(factoring,[status(thm)],[c39]) ).
cnf(p824,plain,
( ~ in(X1,X0)
| in(ordered_pair(X1,singleton(X1)),sk7(X0))
| sk5(X0) != sk6(X0) ),
inference(equality_resolution,[status(thm)],[p239]) ).
cnf(p5832,plain,
( ~ in(X0,sk0)
| in(ordered_pair(X0,singleton(X0)),sk7(sk0))
| sk0 = relation_dom(sk7(sk0)) ),
inference(resolution,[status(thm)],[p5827,p824]) ).
cnf(p6335,plain,
( in(ordered_pair(sk9(sk7(sk0),sk0),singleton(sk9(sk7(sk0),sk0))),sk7(sk0))
| sk0 = relation_dom(sk7(sk0))
| sk0 = relation_dom(sk7(sk0)) ),
inference(resolution,[status(thm)],[p6329,p5832]) ).
cnf(p6393,plain,
( in(ordered_pair(sk9(sk7(sk0),sk0),singleton(sk9(sk7(sk0),sk0))),sk7(sk0))
| sk0 = relation_dom(sk7(sk0)) ),
inference(factoring,[status(thm)],[p6335]) ).
cnf(p6396,plain,
( ~ in(sk9(sk7(sk0),sk0),sk0)
| sk0 = relation_dom(sk7(sk0))
| sk0 = relation_dom(sk7(sk0)) ),
inference(resolution,[status(thm)],[p6393,p360]) ).
cnf(p6417,plain,
( ~ in(sk9(sk7(sk0),sk0),sk0)
| sk0 = relation_dom(sk7(sk0)) ),
inference(factoring,[status(thm)],[p6396]) ).
cnf(p6420,plain,
( sk0 = relation_dom(sk7(sk0))
| sk0 = relation_dom(sk7(sk0)) ),
inference(resolution,[status(thm)],[p6417,p6329]) ).
cnf(p6421,plain,
sk0 = relation_dom(sk7(sk0)),
inference(factoring,[status(thm)],[p6420]) ).
fof(f10,axiom,
! [A] :
( ( function(A)
& relation(A) )
=> ! [B,C] :
( ( ~ in(B,relation_dom(A))
=> ( C = apply(A,B)
<=> C = empty_set ) )
& ( in(B,relation_dom(A))
=> ( C = apply(A,B)
<=> in(ordered_pair(B,C),A) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d4_funct_1) ).
fof(f10_nnf,plain,
! [A] :
( ! [B,C] :
( ( ( ( C != empty_set
| C = apply(A,B) )
& ( C = empty_set
| C != apply(A,B) ) )
| in(B,relation_dom(A)) )
& ( ( ( ~ in(ordered_pair(B,C),A)
| C = apply(A,B) )
& ( in(ordered_pair(B,C),A)
| C != apply(A,B) ) )
| ~ in(B,relation_dom(A)) ) )
| ~ function(A)
| ~ relation(A) ),
inference(nnf_transformation,[status(thm)],[f10]) ).
fof(f10_sk,plain,
! [A,B,C] :
( ( ( ( ( C != empty_set
| C = apply(A,B) )
& ( C = empty_set
| C != apply(A,B) ) )
| in(B,relation_dom(A)) )
& ( ( ( ~ in(ordered_pair(B,C),A)
| C = apply(A,B) )
& ( in(ordered_pair(B,C),A)
| C != apply(A,B) ) )
| ~ in(B,relation_dom(A)) ) )
| ~ function(A)
| ~ relation(A) ),
inference(skolemisation,[status(esa)],[f10_nnf]) ).
cnf(c43,plain,
( in(ordered_pair(X1,X2),X0)
| X2 != apply(X0,X1)
| ~ in(X1,relation_dom(X0))
| ~ function(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(esa)],[f10_sk]) ).
cnf(p251,plain,
( in(ordered_pair(X0,X1),sk7(sk0))
| X1 != apply(sk7(sk0),X0)
| ~ in(X0,relation_dom(sk7(sk0)))
| ~ function(sk7(sk0)) ),
inference(resolution,[status(thm)],[c43,p220]) ).
cnf(p253,plain,
( in(ordered_pair(X0,apply(sk7(sk0),X0)),sk7(sk0))
| ~ in(X0,relation_dom(sk7(sk0)))
| ~ function(sk7(sk0)) ),
inference(equality_resolution,[status(thm)],[p251]) ).
cnf(c35,plain,
( function(sk7(X0))
| sk5(X0) != sk6(X0) ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(c29,plain,
( function(sk7(X0))
| sk6(X0) = singleton(sk4(X0)) ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(c17,plain,
( function(sk7(X0))
| sk5(X0) = singleton(sk4(X0)) ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(c11,plain,
( function(sk7(X0))
| in(sk4(X0),X0) ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(p101,plain,
( X0 = X1
| X1 != singleton(sk4(sk0))
| X0 != singleton(sk4(sk0))
| function(sk7(sk0)) ),
inference(resolution,[status(thm)],[c11,c0]) ).
cnf(p137,plain,
( sk5(sk0) = X0
| X0 != singleton(sk4(sk0))
| function(sk7(sk0))
| function(sk7(sk0)) ),
inference(resolution,[status(thm)],[c17,p101]) ).
cnf(p155,plain,
( sk5(sk0) = X0
| X0 != singleton(sk4(sk0))
| function(sk7(sk0)) ),
inference(factoring,[status(thm)],[p137]) ).
cnf(p198,plain,
( sk5(sk0) = X0
| X0 != sk6(sk0)
| function(sk7(sk0))
| function(sk7(sk0)) ),
inference(superposition,[status(thm)],[c29,p155]) ).
cnf(p208,plain,
( sk5(sk0) = X0
| X0 != sk6(sk0)
| function(sk7(sk0)) ),
inference(factoring,[status(thm)],[p198]) ).
cnf(p209,plain,
( sk5(sk0) = sk6(sk0)
| function(sk7(sk0)) ),
inference(equality_resolution,[status(thm)],[p208]) ).
cnf(p224,plain,
( function(sk7(sk0))
| function(sk7(sk0)) ),
inference(resolution,[status(thm)],[c35,p209]) ).
cnf(p225,plain,
function(sk7(sk0)),
inference(factoring,[status(thm)],[p224]) ).
cnf(p255,plain,
( in(ordered_pair(X0,apply(sk7(sk0),X0)),sk7(sk0))
| ~ in(X0,relation_dom(sk7(sk0))) ),
inference(resolution,[status(thm)],[p253,p225]) ).
cnf(p6424,plain,
( in(ordered_pair(X0,apply(sk7(sk0),X0)),sk7(sk0))
| ~ in(X0,sk0) ),
inference(superposition,[status(thm)],[p6421,p255]) ).
cnf(c2,plain,
( in(sk2(X1),sk0)
| relation_dom(X1) != sk0
| ~ function(X1)
| ~ relation(X1) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p221,plain,
( in(sk2(sk7(sk0)),sk0)
| relation_dom(sk7(sk0)) != sk0
| ~ function(sk7(sk0)) ),
inference(resolution,[status(thm)],[p220,c2]) ).
cnf(p226,plain,
( in(sk2(sk7(sk0)),sk0)
| relation_dom(sk7(sk0)) != sk0 ),
inference(resolution,[status(thm)],[p225,p221]) ).
cnf(p6422,plain,
( in(sk2(sk7(sk0)),sk0)
| sk0 != sk0 ),
inference(superposition,[status(thm)],[p6421,p226]) ).
cnf(p6784,plain,
in(sk2(sk7(sk0)),sk0),
inference(equality_resolution,[status(thm)],[p6422]) ).
cnf(p7362,plain,
in(ordered_pair(sk2(sk7(sk0)),apply(sk7(sk0),sk2(sk7(sk0)))),sk7(sk0)),
inference(resolution,[status(thm)],[p6424,p6784]) ).
cnf(c20,plain,
( X3 = singleton(X2)
| ~ in(ordered_pair(X2,X3),sk7(X0))
| sk5(X0) = singleton(sk4(X0)) ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(p7523,plain,
( apply(sk7(sk0),sk2(sk7(sk0))) = singleton(sk2(sk7(sk0)))
| sk5(sk0) = singleton(sk4(sk0)) ),
inference(resolution,[status(thm)],[p7362,c20]) ).
cnf(c3,plain,
( apply(X1,sk2(X1)) != singleton(sk2(X1))
| relation_dom(X1) != sk0
| ~ function(X1)
| ~ relation(X1) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p222,plain,
( apply(sk7(sk0),sk2(sk7(sk0))) != singleton(sk2(sk7(sk0)))
| relation_dom(sk7(sk0)) != sk0
| ~ function(sk7(sk0)) ),
inference(resolution,[status(thm)],[p220,c3]) ).
cnf(p227,plain,
( apply(sk7(sk0),sk2(sk7(sk0))) != singleton(sk2(sk7(sk0)))
| relation_dom(sk7(sk0)) != sk0 ),
inference(resolution,[status(thm)],[p222,p225]) ).
cnf(p6423,plain,
( apply(sk7(sk0),sk2(sk7(sk0))) != singleton(sk2(sk7(sk0)))
| sk0 != sk0 ),
inference(superposition,[status(thm)],[p6421,p227]) ).
cnf(p7611,plain,
apply(sk7(sk0),sk2(sk7(sk0))) != singleton(sk2(sk7(sk0))),
inference(equality_resolution,[status(thm)],[p6423]) ).
cnf(p8202,plain,
sk5(sk0) = singleton(sk4(sk0)),
inference(resolution,[status(thm)],[p7523,p7611]) ).
cnf(c15,plain,
( X3 != singleton(X2)
| ~ in(X2,X0)
| ~ in(X2,X0)
| in(ordered_pair(X2,X3),sk7(X0))
| in(sk4(X0),X0) ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(p114,plain,
( X2 != singleton(X1)
| ~ in(X1,X0)
| in(ordered_pair(X1,X2),sk7(X0))
| in(sk4(X0),X0) ),
inference(factoring,[status(thm)],[c15]) ).
cnf(c12,plain,
( in(X2,X0)
| ~ in(ordered_pair(X2,X3),sk7(X0))
| in(sk4(X0),X0) ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(p432,plain,
( in(sk9(sk7(sk0),X0),sk0)
| in(sk4(sk0),sk0)
| in(sk9(sk7(sk0),X0),X0)
| X0 = relation_dom(sk7(sk0)) ),
inference(resolution,[status(thm)],[p349,c12]) ).
cnf(p497,plain,
( in(sk4(sk0),sk0)
| in(sk9(sk7(sk0),sk0),sk0)
| sk0 = relation_dom(sk7(sk0)) ),
inference(factoring,[status(thm)],[p432]) ).
cnf(p570,plain,
( in(sk4(sk0),sk0)
| sk0 = relation_dom(sk7(sk0))
| X0 != singleton(sk9(sk7(sk0),sk0))
| in(ordered_pair(sk9(sk7(sk0),sk0),X0),sk7(sk0))
| in(sk4(sk0),sk0) ),
inference(resolution,[status(thm)],[p114,p497]) ).
cnf(p2161,plain,
( sk0 = relation_dom(sk7(sk0))
| X0 != singleton(sk9(sk7(sk0),sk0))
| in(ordered_pair(sk9(sk7(sk0),sk0),X0),sk7(sk0))
| in(sk4(sk0),sk0) ),
inference(factoring,[status(thm)],[p570]) ).
cnf(p2171,plain,
( sk0 = relation_dom(sk7(sk0))
| in(ordered_pair(sk9(sk7(sk0),sk0),singleton(sk9(sk7(sk0),sk0))),sk7(sk0))
| in(sk4(sk0),sk0) ),
inference(equality_resolution,[status(thm)],[p2161]) ).
cnf(p2179,plain,
( ~ in(sk9(sk7(sk0),sk0),sk0)
| sk0 = relation_dom(sk7(sk0))
| sk0 = relation_dom(sk7(sk0))
| in(sk4(sk0),sk0) ),
inference(resolution,[status(thm)],[p2171,p360]) ).
cnf(p2214,plain,
( ~ in(sk9(sk7(sk0),sk0),sk0)
| sk0 = relation_dom(sk7(sk0))
| in(sk4(sk0),sk0) ),
inference(factoring,[status(thm)],[p2179]) ).
cnf(p2215,plain,
( in(sk4(sk0),sk0)
| sk0 = relation_dom(sk7(sk0))
| sk0 = relation_dom(sk7(sk0))
| in(sk4(sk0),sk0) ),
inference(resolution,[status(thm)],[p2214,p497]) ).
cnf(p2219,plain,
( in(sk4(sk0),sk0)
| sk0 = relation_dom(sk7(sk0))
| in(sk4(sk0),sk0) ),
inference(factoring,[status(thm)],[p2215]) ).
cnf(p2224,plain,
( sk0 = relation_dom(sk7(sk0))
| in(sk4(sk0),sk0) ),
inference(factoring,[status(thm)],[p2219]) ).
cnf(p2225,plain,
( in(sk2(sk7(sk0)),sk0)
| sk0 != sk0
| in(sk4(sk0),sk0) ),
inference(superposition,[status(thm)],[p2224,p226]) ).
cnf(p2659,plain,
( in(sk2(sk7(sk0)),sk0)
| in(sk4(sk0),sk0) ),
inference(equality_resolution,[status(thm)],[p2225]) ).
cnf(p550,plain,
( ~ in(X1,X0)
| in(ordered_pair(X1,singleton(X1)),sk7(X0))
| in(sk4(X0),X0) ),
inference(equality_resolution,[status(thm)],[p114]) ).
cnf(p2685,plain,
( in(ordered_pair(sk2(sk7(sk0)),singleton(sk2(sk7(sk0)))),sk7(sk0))
| in(sk4(sk0),sk0)
| in(sk4(sk0),sk0) ),
inference(resolution,[status(thm)],[p2659,p550]) ).
cnf(p5162,plain,
( in(ordered_pair(sk2(sk7(sk0)),singleton(sk2(sk7(sk0)))),sk7(sk0))
| in(sk4(sk0),sk0) ),
inference(factoring,[status(thm)],[p2685]) ).
cnf(c48,plain,
( ~ in(ordered_pair(X2,X3),X0)
| in(X2,X1)
| X1 != relation_dom(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(esa)],[f11_sk]) ).
cnf(p323,plain,
( ~ in(ordered_pair(X1,X2),sk7(sk0))
| in(X1,X0)
| X0 != relation_dom(sk7(sk0)) ),
inference(resolution,[status(thm)],[c48,p220]) ).
cnf(p325,plain,
( ~ in(ordered_pair(X0,X1),sk7(sk0))
| in(X0,relation_dom(sk7(sk0))) ),
inference(equality_resolution,[status(thm)],[p323]) ).
cnf(p5164,plain,
( in(sk2(sk7(sk0)),relation_dom(sk7(sk0)))
| in(sk4(sk0),sk0) ),
inference(resolution,[status(thm)],[p5162,p325]) ).
cnf(p5177,plain,
( in(ordered_pair(sk2(sk7(sk0)),apply(sk7(sk0),sk2(sk7(sk0)))),sk7(sk0))
| in(sk4(sk0),sk0) ),
inference(resolution,[status(thm)],[p5164,p255]) ).
cnf(c14,plain,
( X3 = singleton(X2)
| ~ in(ordered_pair(X2,X3),sk7(X0))
| in(sk4(X0),X0) ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(p5217,plain,
( apply(sk7(sk0),sk2(sk7(sk0))) = singleton(sk2(sk7(sk0)))
| in(sk4(sk0),sk0)
| in(sk4(sk0),sk0) ),
inference(resolution,[status(thm)],[p5177,c14]) ).
cnf(p5307,plain,
( apply(sk7(sk0),sk2(sk7(sk0))) = singleton(sk2(sk7(sk0)))
| in(sk4(sk0),sk0) ),
inference(factoring,[status(thm)],[p5217]) ).
cnf(p2226,plain,
( apply(sk7(sk0),sk2(sk7(sk0))) != singleton(sk2(sk7(sk0)))
| sk0 != sk0
| in(sk4(sk0),sk0) ),
inference(superposition,[status(thm)],[p2224,p227]) ).
cnf(p4086,plain,
( apply(sk7(sk0),sk2(sk7(sk0))) != singleton(sk2(sk7(sk0)))
| in(sk4(sk0),sk0) ),
inference(equality_resolution,[status(thm)],[p2226]) ).
cnf(p5309,plain,
( in(sk4(sk0),sk0)
| in(sk4(sk0),sk0) ),
inference(resolution,[status(thm)],[p5307,p4086]) ).
cnf(p5310,plain,
in(sk4(sk0),sk0),
inference(factoring,[status(thm)],[p5309]) ).
cnf(c1,plain,
( sk1(X1) = singleton(X1)
| ~ in(X1,sk0) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p5311,plain,
sk1(sk4(sk0)) = singleton(sk4(sk0)),
inference(resolution,[status(thm)],[p5310,c1]) ).
cnf(p8217,plain,
singleton(sk4(sk0)) = sk5(sk0),
inference(superposition,[status(thm)],[p8202,p5311]) ).
cnf(c32,plain,
( X3 = singleton(X2)
| ~ in(ordered_pair(X2,X3),sk7(X0))
| sk6(X0) = singleton(sk4(X0)) ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(p7524,plain,
( apply(sk7(sk0),sk2(sk7(sk0))) = singleton(sk2(sk7(sk0)))
| sk6(sk0) = singleton(sk4(sk0)) ),
inference(resolution,[status(thm)],[p7362,c32]) ).
cnf(p8793,plain,
( apply(sk7(sk0),sk2(sk7(sk0))) = singleton(sk2(sk7(sk0)))
| sk6(sk0) = sk5(sk0) ),
inference(demodulation,[status(thm)],[p8217,p7524]) ).
cnf(p9004,plain,
sk6(sk0) = sk5(sk0),
inference(resolution,[status(thm)],[p8793,p7611]) ).
cnf(c38,plain,
( X3 = singleton(X2)
| ~ in(ordered_pair(X2,X3),sk7(X0))
| sk5(X0) != sk6(X0) ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(p9005,plain,
( X1 = singleton(X0)
| ~ in(ordered_pair(X0,X1),sk7(sk0))
| sk5(sk0) != sk5(sk0) ),
inference(superposition,[status(thm)],[p9004,c38]) ).
cnf(p9009,plain,
( X1 = singleton(X0)
| ~ in(ordered_pair(X0,X1),sk7(sk0)) ),
inference(equality_resolution,[status(thm)],[p9005]) ).
cnf(p9093,plain,
apply(sk7(sk0),sk2(sk7(sk0))) = singleton(sk2(sk7(sk0))),
inference(resolution,[status(thm)],[p9009,p7362]) ).
cnf(p9104,plain,
singleton(sk2(sk7(sk0))) != singleton(sk2(sk7(sk0))),
inference(demodulation,[status(thm)],[p9093,p7611]) ).
cnf(p9115,plain,
$false,
inference(equality_resolution,[status(thm)],[p9104]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU283+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.12/0.37 % Computer : n019.cluster.edu
% 0.12/0.37 % Model : x86_64 x86_64
% 0.12/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.37 % Memory : 8046.5625MB
% 0.12/0.37 % OS : Linux 6.8.0-71-generic
% 0.12/0.38 % CPULimit : 300
% 0.12/0.38 % WCLimit : 300
% 0.12/0.38 % DateTime : Thu Sep 24 13:32:34 UTC 2026
% 0.12/0.38 % CPUTime :
% 0.12/0.38 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 50.72/7.71 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 50.72/7.71 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------