%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SEU216+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n004.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:22 PM UTC 2026
% Result : Theorem 14.15s 2.28s
% Output : Proof 14.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 33
% Number of leaves : 5
% Syntax : Number of formulae : 78 ( 10 unt; 0 def)
% Number of atoms : 291 ( 147 equ)
% Maximal formula atoms : 15 ( 3 avg)
% Number of connectives : 330 ( 117 ~; 151 |; 46 &)
% ( 7 <=>; 9 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 4 con; 0-2 aty)
% Number of variables : 92 ( 3 sgn 41 !; 5 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f41,axiom,
! [A,B,C] :
( ( function(C)
& relation(C) )
=> ( in(ordered_pair(A,B),C)
<=> ( B = apply(C,A)
& in(A,relation_dom(C)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t8_funct_1) ).
fof(f41_nnf,plain,
! [A,B,C] :
( ( ( B != apply(C,A)
| ~ in(A,relation_dom(C))
| in(ordered_pair(A,B),C) )
& ( ( B = apply(C,A)
& in(A,relation_dom(C)) )
| ~ in(ordered_pair(A,B),C) ) )
| ~ function(C)
| ~ relation(C) ),
inference(nnf_transformation,[status(thm)],[f41]) ).
fof(f41_sk,plain,
! [C,A,B] :
( ( ( B != apply(C,A)
| ~ in(A,relation_dom(C))
| in(ordered_pair(A,B),C) )
& ( ( B = apply(C,A)
& in(A,relation_dom(C)) )
| ~ in(ordered_pair(A,B),C) ) )
| ~ function(C)
| ~ relation(C) ),
inference(skolemisation,[status(esa)],[f41_nnf]) ).
cnf(c74,plain,
( X1 = apply(X2,X0)
| ~ in(ordered_pair(X0,X1),X2)
| ~ function(X2)
| ~ relation(X2) ),
inference(cnf_transformation,[status(esa)],[f41_sk]) ).
fof(f36,conjecture,
! [A,B] :
( ( function(B)
& relation(B) )
=> ( B = identity_relation(A)
<=> ( ! [C] :
( in(C,A)
=> apply(B,C) = C )
& relation_dom(B) = A ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t34_funct_1) ).
fof(f36_neg,negated_conjecture,
~ ! [A,B] :
( ( function(B)
& relation(B) )
=> ( B = identity_relation(A)
<=> ( ! [C] :
( in(C,A)
=> apply(B,C) = C )
& relation_dom(B) = A ) ) ),
inference(negated_conjecture,[status(cth)],[f36]) ).
fof(f36_nnf,plain,
? [A,B] :
( ( ( ! [C] :
( apply(B,C) = C
| ~ in(C,A) )
& relation_dom(B) = A
& B != identity_relation(A) )
| ( ( ? [C] :
( apply(B,C) != C
& in(C,A) )
| relation_dom(B) != A )
& B = identity_relation(A) ) )
& function(B)
& relation(B) ),
inference(nnf_transformation,[status(thm)],[f36_neg]) ).
fof(f36_sk,plain,
! [C] :
( ( ( ( apply(sk10,C) = C
| ~ in(C,sk9) )
& relation_dom(sk10) = sk9
& sk10 != identity_relation(sk9) )
| ( ( ( apply(sk10,sk11) != sk11
& in(sk11,sk9) )
| relation_dom(sk10) != sk9 )
& sk10 = identity_relation(sk9) ) )
& function(sk10)
& relation(sk10) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk9,sk10,sk11])],[f36_nnf]) ).
cnf(c57,plain,
relation(sk10),
inference(cnf_transformation,[status(esa)],[f36_sk]) ).
cnf(p397,plain,
( X1 = apply(sk10,X0)
| ~ in(ordered_pair(X0,X1),sk10)
| ~ function(sk10) ),
inference(resolution,[status(thm)],[c74,c57]) ).
cnf(c58,plain,
function(sk10),
inference(cnf_transformation,[status(esa)],[f36_sk]) ).
cnf(p440,plain,
( X1 = apply(sk10,X0)
| ~ in(ordered_pair(X0,X1),sk10) ),
inference(resolution,[status(thm)],[p397,c58]) ).
fof(f4,axiom,
! [A,B] :
( relation(B)
=> ( B = identity_relation(A)
<=> ! [C,D] :
( in(ordered_pair(C,D),B)
<=> ( C = D
& in(C,A) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d10_relat_1) ).
fof(f4_nnf,plain,
! [A,B] :
( ( ( ? [C,D] :
( ( C = D
& in(C,A)
& ~ in(ordered_pair(C,D),B) )
| ( ( C != D
| ~ in(C,A) )
& in(ordered_pair(C,D),B) ) )
| B = identity_relation(A) )
& ( ! [C,D] :
( ( C != D
| ~ in(C,A)
| in(ordered_pair(C,D),B) )
& ( ( C = D
& in(C,A) )
| ~ in(ordered_pair(C,D),B) ) )
| B != identity_relation(A) ) )
| ~ relation(B) ),
inference(nnf_transformation,[status(thm)],[f4]) ).
fof(f4_sk,plain,
! [B,A,C,D] :
( ( ( ( sk0(A,B) = sk1(A,B)
& in(sk0(A,B),A)
& ~ in(ordered_pair(sk0(A,B),sk1(A,B)),B) )
| ( ( sk0(A,B) != sk1(A,B)
| ~ in(sk0(A,B),A) )
& in(ordered_pair(sk0(A,B),sk1(A,B)),B) )
| B = identity_relation(A) )
& ( ( ( C != D
| ~ in(C,A)
| in(ordered_pair(C,D),B) )
& ( ( C = D
& in(C,A) )
| ~ in(ordered_pair(C,D),B) ) )
| B != identity_relation(A) ) )
| ~ relation(B) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk0,sk1])],[f4_nnf]) ).
cnf(c9,plain,
( sk0(X0,X1) = sk1(X0,X1)
| in(ordered_pair(sk0(X0,X1),sk1(X0,X1)),X1)
| X1 = identity_relation(X0)
| ~ relation(X1) ),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(p114,plain,
( sk0(X0,sk10) = sk1(X0,sk10)
| in(ordered_pair(sk0(X0,sk10),sk1(X0,sk10)),sk10)
| sk10 = identity_relation(X0) ),
inference(resolution,[status(thm)],[c9,c57]) ).
cnf(p442,plain,
( sk0(X0,sk10) = sk1(X0,sk10)
| sk10 = identity_relation(X0)
| sk1(X0,sk10) = apply(sk10,sk0(X0,sk10)) ),
inference(resolution,[status(thm)],[p440,p114]) ).
cnf(c60,plain,
( relation_dom(sk10) = sk9
| sk10 = identity_relation(sk9) ),
inference(cnf_transformation,[status(esa)],[f36_sk]) ).
cnf(c73,plain,
( in(X0,relation_dom(X2))
| ~ in(ordered_pair(X0,X1),X2)
| ~ function(X2)
| ~ relation(X2) ),
inference(cnf_transformation,[status(esa)],[f41_sk]) ).
cnf(p364,plain,
( in(X0,relation_dom(sk10))
| ~ in(ordered_pair(X0,X1),sk10)
| ~ function(sk10) ),
inference(resolution,[status(thm)],[c73,c57]) ).
cnf(p371,plain,
( in(X0,relation_dom(sk10))
| ~ in(ordered_pair(X0,X1),sk10) ),
inference(resolution,[status(thm)],[p364,c58]) ).
cnf(c8,plain,
( in(sk0(X0,X1),X0)
| in(ordered_pair(sk0(X0,X1),sk1(X0,X1)),X1)
| X1 = identity_relation(X0)
| ~ relation(X1) ),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(p104,plain,
( in(sk0(X0,sk10),X0)
| in(ordered_pair(sk0(X0,sk10),sk1(X0,sk10)),sk10)
| sk10 = identity_relation(X0) ),
inference(resolution,[status(thm)],[c8,c57]) ).
cnf(p372,plain,
( in(sk0(X0,sk10),X0)
| sk10 = identity_relation(X0)
| in(sk0(X0,sk10),relation_dom(sk10)) ),
inference(resolution,[status(thm)],[p371,p104]) ).
cnf(p378,plain,
( in(sk0(X0,sk10),X0)
| sk10 = identity_relation(X0)
| in(sk0(X0,sk10),sk9)
| sk10 = identity_relation(sk9) ),
inference(superposition,[status(thm)],[c60,p372]) ).
cnf(p551,plain,
( sk10 = identity_relation(sk9)
| in(sk0(sk9,sk10),sk9)
| sk10 = identity_relation(sk9) ),
inference(factoring,[status(thm)],[p378]) ).
cnf(p559,plain,
( in(sk0(sk9,sk10),sk9)
| sk10 = identity_relation(sk9) ),
inference(factoring,[status(thm)],[p551]) ).
cnf(c61,plain,
( apply(sk10,X2) = X2
| ~ in(X2,sk9)
| sk10 = identity_relation(sk9) ),
inference(cnf_transformation,[status(esa)],[f36_sk]) ).
cnf(p561,plain,
( apply(sk10,sk0(sk9,sk10)) = sk0(sk9,sk10)
| sk10 = identity_relation(sk9)
| sk10 = identity_relation(sk9) ),
inference(resolution,[status(thm)],[p559,c61]) ).
cnf(p570,plain,
( apply(sk10,sk0(sk9,sk10)) = sk0(sk9,sk10)
| sk10 = identity_relation(sk9) ),
inference(factoring,[status(thm)],[p561]) ).
fof(f5,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/sandbox/benchmark/theBenchmark.p',d4_funct_1) ).
fof(f5_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)],[f5]) ).
fof(f5_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)],[f5_nnf]) ).
cnf(c13,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)],[f5_sk]) ).
cnf(p137,plain,
( in(ordered_pair(X0,X1),sk10)
| X1 != apply(sk10,X0)
| ~ in(X0,relation_dom(sk10))
| ~ function(sk10) ),
inference(resolution,[status(thm)],[c13,c57]) ).
cnf(p145,plain,
( in(ordered_pair(X0,apply(sk10,X0)),sk10)
| ~ in(X0,relation_dom(sk10))
| ~ function(sk10) ),
inference(equality_resolution,[status(thm)],[p137]) ).
cnf(p147,plain,
( in(ordered_pair(X0,apply(sk10,X0)),sk10)
| ~ in(X0,relation_dom(sk10)) ),
inference(resolution,[status(thm)],[p145,c58]) ).
cnf(p148,plain,
( in(ordered_pair(X0,apply(sk10,X0)),sk10)
| ~ in(X0,sk9)
| sk10 = identity_relation(sk9) ),
inference(superposition,[status(thm)],[c60,p147]) ).
cnf(p563,plain,
( in(ordered_pair(sk0(sk9,sk10),apply(sk10,sk0(sk9,sk10))),sk10)
| sk10 = identity_relation(sk9)
| sk10 = identity_relation(sk9) ),
inference(resolution,[status(thm)],[p559,p148]) ).
cnf(p620,plain,
( in(ordered_pair(sk0(sk9,sk10),apply(sk10,sk0(sk9,sk10))),sk10)
| sk10 = identity_relation(sk9) ),
inference(factoring,[status(thm)],[p563]) ).
cnf(p627,plain,
( in(ordered_pair(sk0(sk9,sk10),sk0(sk9,sk10)),sk10)
| sk10 = identity_relation(sk9)
| sk10 = identity_relation(sk9) ),
inference(superposition,[status(thm)],[p570,p620]) ).
cnf(p634,plain,
( in(ordered_pair(sk0(sk9,sk10),sk0(sk9,sk10)),sk10)
| sk10 = identity_relation(sk9) ),
inference(factoring,[status(thm)],[p627]) ).
cnf(p637,plain,
( sk0(sk9,sk10) = apply(sk10,sk0(sk9,sk10))
| sk10 = identity_relation(sk9) ),
inference(resolution,[status(thm)],[p634,p440]) ).
cnf(p645,plain,
( sk0(sk9,sk10) = sk1(sk9,sk10)
| sk10 = identity_relation(sk9)
| sk0(sk9,sk10) = sk1(sk9,sk10)
| sk10 = identity_relation(sk9) ),
inference(superposition,[status(thm)],[p442,p637]) ).
cnf(p978,plain,
( sk10 = identity_relation(sk9)
| sk0(sk9,sk10) = sk1(sk9,sk10)
| sk10 = identity_relation(sk9) ),
inference(factoring,[status(thm)],[p645]) ).
cnf(p979,plain,
( sk0(sk9,sk10) = sk1(sk9,sk10)
| sk10 = identity_relation(sk9) ),
inference(factoring,[status(thm)],[p978]) ).
cnf(c10,plain,
( ~ in(ordered_pair(sk0(X0,X1),sk1(X0,X1)),X1)
| sk0(X0,X1) != sk1(X0,X1)
| ~ in(sk0(X0,X1),X0)
| X1 = identity_relation(X0)
| ~ relation(X1) ),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(p123,plain,
( ~ in(ordered_pair(sk0(X0,sk10),sk1(X0,sk10)),sk10)
| sk0(X0,sk10) != sk1(X0,sk10)
| ~ in(sk0(X0,sk10),X0)
| sk10 = identity_relation(X0) ),
inference(resolution,[status(thm)],[c10,c57]) ).
cnf(p562,plain,
( ~ in(ordered_pair(sk0(sk9,sk10),sk1(sk9,sk10)),sk10)
| sk0(sk9,sk10) != sk1(sk9,sk10)
| sk10 = identity_relation(sk9)
| sk10 = identity_relation(sk9) ),
inference(resolution,[status(thm)],[p559,p123]) ).
cnf(p1011,plain,
( ~ in(ordered_pair(sk0(sk9,sk10),sk1(sk9,sk10)),sk10)
| sk0(sk9,sk10) != sk1(sk9,sk10)
| sk10 = identity_relation(sk9) ),
inference(factoring,[status(thm)],[p562]) ).
cnf(p1012,plain,
( sk10 = identity_relation(sk9)
| ~ in(ordered_pair(sk0(sk9,sk10),sk1(sk9,sk10)),sk10)
| sk10 = identity_relation(sk9) ),
inference(resolution,[status(thm)],[p1011,p979]) ).
cnf(p1013,plain,
( ~ in(ordered_pair(sk0(sk9,sk10),sk1(sk9,sk10)),sk10)
| sk10 = identity_relation(sk9) ),
inference(factoring,[status(thm)],[p1012]) ).
cnf(p1014,plain,
( ~ in(ordered_pair(sk0(sk9,sk10),sk0(sk9,sk10)),sk10)
| sk10 = identity_relation(sk9)
| sk10 = identity_relation(sk9) ),
inference(superposition,[status(thm)],[p979,p1013]) ).
cnf(p1015,plain,
( ~ in(ordered_pair(sk0(sk9,sk10),sk0(sk9,sk10)),sk10)
| sk10 = identity_relation(sk9) ),
inference(factoring,[status(thm)],[p1014]) ).
cnf(p1016,plain,
( sk10 = identity_relation(sk9)
| sk10 = identity_relation(sk9) ),
inference(resolution,[status(thm)],[p1015,p634]) ).
cnf(p1017,plain,
sk10 = identity_relation(sk9),
inference(factoring,[status(thm)],[p1016]) ).
fof(f38,axiom,
! [A] :
( relation_rng(identity_relation(A)) = A
& relation_dom(identity_relation(A)) = A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t71_relat_1) ).
fof(f38_nnf,plain,
! [A] :
( relation_rng(identity_relation(A)) = A
& relation_dom(identity_relation(A)) = A ),
inference(nnf_transformation,[status(thm)],[f38]) ).
fof(f38_sk,plain,
! [A] :
( relation_rng(identity_relation(A)) = A
& relation_dom(identity_relation(A)) = A ),
inference(skolemisation,[status(esa)],[f38_nnf]) ).
cnf(c69,plain,
relation_dom(identity_relation(X0)) = X0,
inference(cnf_transformation,[status(esa)],[f38_sk]) ).
cnf(p1020,plain,
relation_dom(sk10) = sk9,
inference(superposition,[status(thm)],[p1017,c69]) ).
cnf(c62,plain,
( sk10 != identity_relation(sk9)
| in(sk11,sk9)
| relation_dom(sk10) != sk9 ),
inference(cnf_transformation,[status(esa)],[f36_sk]) ).
cnf(p1021,plain,
( sk10 != identity_relation(sk9)
| in(sk11,sk9)
| sk9 != sk9 ),
inference(demodulation,[status(thm)],[p1020,c62]) ).
cnf(p1104,plain,
( sk10 != identity_relation(sk9)
| in(sk11,sk9) ),
inference(equality_resolution,[status(thm)],[p1021]) ).
cnf(p1105,plain,
in(sk11,sk9),
inference(resolution,[status(thm)],[p1104,p1017]) ).
cnf(c6,plain,
( X2 != X3
| ~ in(X2,X0)
| in(ordered_pair(X2,X3),X1)
| X1 != identity_relation(X0)
| ~ relation(X1) ),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(p89,plain,
( X1 != X2
| ~ in(X1,X0)
| in(ordered_pair(X1,X2),sk10)
| sk10 != identity_relation(X0) ),
inference(resolution,[status(thm)],[c6,c57]) ).
cnf(p262,plain,
( ~ in(X1,X0)
| in(ordered_pair(X1,X1),sk10)
| sk10 != identity_relation(X0) ),
inference(equality_resolution,[status(thm)],[p89]) ).
cnf(p1062,plain,
( ~ in(X0,sk9)
| in(ordered_pair(X0,X0),sk10) ),
inference(resolution,[status(thm)],[p1017,p262]) ).
cnf(p1109,plain,
in(ordered_pair(sk11,sk11),sk10),
inference(resolution,[status(thm)],[p1105,p1062]) ).
cnf(p1114,plain,
sk11 = apply(sk10,sk11),
inference(resolution,[status(thm)],[p1109,p440]) ).
cnf(c65,plain,
( sk10 != identity_relation(sk9)
| apply(sk10,sk11) != sk11
| relation_dom(sk10) != sk9 ),
inference(cnf_transformation,[status(esa)],[f36_sk]) ).
cnf(p1023,plain,
( sk10 != identity_relation(sk9)
| apply(sk10,sk11) != sk11
| sk9 != sk9 ),
inference(demodulation,[status(thm)],[p1020,c65]) ).
cnf(p1123,plain,
( sk10 != identity_relation(sk9)
| apply(sk10,sk11) != sk11 ),
inference(equality_resolution,[status(thm)],[p1023]) ).
cnf(p1124,plain,
( sk10 != identity_relation(sk9)
| sk11 != sk11 ),
inference(superposition,[status(thm)],[p1114,p1123]) ).
cnf(p1125,plain,
sk10 != identity_relation(sk9),
inference(equality_resolution,[status(thm)],[p1124]) ).
cnf(p1126,plain,
$false,
inference(resolution,[status(thm)],[p1125,p1017]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU216+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.08/0.35 % Computer : n004.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Thu Sep 24 13:13:20 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.36 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 14.15/2.28 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 14.15/2.28 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------