%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SEU216+3 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n017.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 17.51s 3.22s
% Output : Proof 17.51s
% Verified :
% SZS Type : Refutation
% Derivation depth : 38
% Number of leaves : 7
% Syntax : Number of formulae : 116 ( 19 unt; 0 def)
% Number of atoms : 381 ( 195 equ)
% Maximal formula atoms : 15 ( 3 avg)
% Number of connectives : 404 ( 139 ~; 200 |; 49 &)
% ( 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 : 126 ( 7 sgn 47 !; 5 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f32,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/sandbox2/benchmark/theBenchmark.p',t34_funct_1) ).
fof(f32_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)],[f32]) ).
fof(f32_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)],[f32_neg]) ).
fof(f32_sk,plain,
! [C] :
( ( ( ( apply(sk12,C) = C
| ~ in(C,sk11) )
& relation_dom(sk12) = sk11
& sk12 != identity_relation(sk11) )
| ( ( ( apply(sk12,sk13) != sk13
& in(sk13,sk11) )
| relation_dom(sk12) != sk11 )
& sk12 = identity_relation(sk11) ) )
& function(sk12)
& relation(sk12) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk11,sk12,sk13])],[f32_nnf]) ).
cnf(c58,plain,
( relation_dom(sk12) = sk11
| sk12 = identity_relation(sk11) ),
inference(cnf_transformation,[status(esa)],[f32_sk]) ).
fof(f40,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/sandbox2/benchmark/theBenchmark.p',t8_funct_1) ).
fof(f40_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)],[f40]) ).
fof(f40_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)],[f40_nnf]) ).
cnf(c75,plain,
( in(X0,relation_dom(X2))
| ~ in(ordered_pair(X0,X1),X2)
| ~ function(X2)
| ~ relation(X2) ),
inference(cnf_transformation,[status(esa)],[f40_sk]) ).
cnf(c55,plain,
relation(sk12),
inference(cnf_transformation,[status(esa)],[f32_sk]) ).
cnf(p603,plain,
( in(X0,relation_dom(sk12))
| ~ in(ordered_pair(X0,X1),sk12)
| ~ function(sk12) ),
inference(resolution,[status(thm)],[c75,c55]) ).
cnf(c56,plain,
function(sk12),
inference(cnf_transformation,[status(esa)],[f32_sk]) ).
cnf(p610,plain,
( in(X0,relation_dom(sk12))
| ~ in(ordered_pair(X0,X1),sk12) ),
inference(resolution,[status(thm)],[p603,c56]) ).
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/sandbox2/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(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(p115,plain,
( in(sk0(X0,sk12),X0)
| in(ordered_pair(sk0(X0,sk12),sk1(X0,sk12)),sk12)
| sk12 = identity_relation(X0) ),
inference(resolution,[status(thm)],[c8,c55]) ).
cnf(p611,plain,
( in(sk0(X0,sk12),X0)
| sk12 = identity_relation(X0)
| in(sk0(X0,sk12),relation_dom(sk12)) ),
inference(resolution,[status(thm)],[p610,p115]) ).
cnf(p614,plain,
( in(sk0(X0,sk12),X0)
| sk12 = identity_relation(X0)
| in(sk0(X0,sk12),sk11)
| sk12 = identity_relation(sk11) ),
inference(superposition,[status(thm)],[c58,p611]) ).
cnf(p965,plain,
( sk12 = identity_relation(sk11)
| in(sk0(sk11,sk12),sk11)
| sk12 = identity_relation(sk11) ),
inference(factoring,[status(thm)],[p614]) ).
cnf(p975,plain,
( in(sk0(sk11,sk12),sk11)
| sk12 = identity_relation(sk11) ),
inference(factoring,[status(thm)],[p965]) ).
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(p135,plain,
( ~ in(ordered_pair(sk0(X0,sk12),sk1(X0,sk12)),sk12)
| sk0(X0,sk12) != sk1(X0,sk12)
| ~ in(sk0(X0,sk12),X0)
| sk12 = identity_relation(X0) ),
inference(resolution,[status(thm)],[c10,c55]) ).
cnf(p978,plain,
( ~ in(ordered_pair(sk0(sk11,sk12),sk1(sk11,sk12)),sk12)
| sk0(sk11,sk12) != sk1(sk11,sk12)
| sk12 = identity_relation(sk11)
| sk12 = identity_relation(sk11) ),
inference(resolution,[status(thm)],[p975,p135]) ).
cnf(p2666,plain,
( ~ in(ordered_pair(sk0(sk11,sk12),sk1(sk11,sk12)),sk12)
| sk0(sk11,sk12) != sk1(sk11,sk12)
| sk12 = identity_relation(sk11) ),
inference(factoring,[status(thm)],[p978]) ).
cnf(c76,plain,
( X1 = apply(X2,X0)
| ~ in(ordered_pair(X0,X1),X2)
| ~ function(X2)
| ~ relation(X2) ),
inference(cnf_transformation,[status(esa)],[f40_sk]) ).
cnf(p643,plain,
( X1 = apply(sk12,X0)
| ~ in(ordered_pair(X0,X1),sk12)
| ~ function(sk12) ),
inference(resolution,[status(thm)],[c76,c55]) ).
cnf(p706,plain,
( X1 = apply(sk12,X0)
| ~ in(ordered_pair(X0,X1),sk12) ),
inference(resolution,[status(thm)],[p643,c56]) ).
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(p124,plain,
( sk0(X0,sk12) = sk1(X0,sk12)
| in(ordered_pair(sk0(X0,sk12),sk1(X0,sk12)),sk12)
| sk12 = identity_relation(X0) ),
inference(resolution,[status(thm)],[c9,c55]) ).
cnf(p708,plain,
( sk0(X0,sk12) = sk1(X0,sk12)
| sk12 = identity_relation(X0)
| sk1(X0,sk12) = apply(sk12,sk0(X0,sk12)) ),
inference(resolution,[status(thm)],[p706,p124]) ).
cnf(c59,plain,
( apply(sk12,X2) = X2
| ~ in(X2,sk11)
| sk12 = identity_relation(sk11) ),
inference(cnf_transformation,[status(esa)],[f32_sk]) ).
cnf(p981,plain,
( apply(sk12,sk0(sk11,sk12)) = sk0(sk11,sk12)
| sk12 = identity_relation(sk11)
| sk12 = identity_relation(sk11) ),
inference(resolution,[status(thm)],[p975,c59]) ).
cnf(p988,plain,
( apply(sk12,sk0(sk11,sk12)) = sk0(sk11,sk12)
| sk12 = identity_relation(sk11) ),
inference(factoring,[status(thm)],[p981]) ).
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/sandbox2/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(p154,plain,
( in(ordered_pair(X0,X1),sk12)
| X1 != apply(sk12,X0)
| ~ in(X0,relation_dom(sk12))
| ~ function(sk12) ),
inference(resolution,[status(thm)],[c13,c55]) ).
cnf(p162,plain,
( in(ordered_pair(X0,apply(sk12,X0)),sk12)
| ~ in(X0,relation_dom(sk12))
| ~ function(sk12) ),
inference(equality_resolution,[status(thm)],[p154]) ).
cnf(p164,plain,
( in(ordered_pair(X0,apply(sk12,X0)),sk12)
| ~ in(X0,relation_dom(sk12)) ),
inference(resolution,[status(thm)],[p162,c56]) ).
cnf(p165,plain,
( in(ordered_pair(X0,apply(sk12,X0)),sk12)
| ~ in(X0,sk11)
| sk12 = identity_relation(sk11) ),
inference(superposition,[status(thm)],[c58,p164]) ).
cnf(p979,plain,
( in(ordered_pair(sk0(sk11,sk12),apply(sk12,sk0(sk11,sk12))),sk12)
| sk12 = identity_relation(sk11)
| sk12 = identity_relation(sk11) ),
inference(resolution,[status(thm)],[p975,p165]) ).
cnf(p1058,plain,
( in(ordered_pair(sk0(sk11,sk12),apply(sk12,sk0(sk11,sk12))),sk12)
| sk12 = identity_relation(sk11) ),
inference(factoring,[status(thm)],[p979]) ).
cnf(p1067,plain,
( in(ordered_pair(sk0(sk11,sk12),sk0(sk11,sk12)),sk12)
| sk12 = identity_relation(sk11)
| sk12 = identity_relation(sk11) ),
inference(superposition,[status(thm)],[p988,p1058]) ).
cnf(p1083,plain,
( in(ordered_pair(sk0(sk11,sk12),sk0(sk11,sk12)),sk12)
| sk12 = identity_relation(sk11) ),
inference(factoring,[status(thm)],[p1067]) ).
cnf(p1087,plain,
( sk0(sk11,sk12) = apply(sk12,sk0(sk11,sk12))
| sk12 = identity_relation(sk11) ),
inference(resolution,[status(thm)],[p1083,p706]) ).
cnf(p1108,plain,
( sk0(sk11,sk12) = sk1(sk11,sk12)
| sk12 = identity_relation(sk11)
| sk0(sk11,sk12) = sk1(sk11,sk12)
| sk12 = identity_relation(sk11) ),
inference(superposition,[status(thm)],[p708,p1087]) ).
cnf(p1566,plain,
( sk12 = identity_relation(sk11)
| sk0(sk11,sk12) = sk1(sk11,sk12)
| sk12 = identity_relation(sk11) ),
inference(factoring,[status(thm)],[p1108]) ).
cnf(p1567,plain,
( sk0(sk11,sk12) = sk1(sk11,sk12)
| sk12 = identity_relation(sk11) ),
inference(factoring,[status(thm)],[p1566]) ).
cnf(p2667,plain,
( sk12 = identity_relation(sk11)
| ~ in(ordered_pair(sk0(sk11,sk12),sk1(sk11,sk12)),sk12)
| sk12 = identity_relation(sk11) ),
inference(resolution,[status(thm)],[p2666,p1567]) ).
cnf(p2668,plain,
( ~ in(ordered_pair(sk0(sk11,sk12),sk1(sk11,sk12)),sk12)
| sk12 = identity_relation(sk11) ),
inference(factoring,[status(thm)],[p2667]) ).
cnf(p613,plain,
( sk12 = identity_relation(relation_dom(sk12))
| in(sk0(relation_dom(sk12),sk12),relation_dom(sk12)) ),
inference(factoring,[status(thm)],[p611]) ).
cnf(p632,plain,
( sk12 = identity_relation(relation_dom(sk12))
| in(sk0(relation_dom(sk12),sk12),sk11)
| sk12 = identity_relation(sk11) ),
inference(superposition,[status(thm)],[c58,p613]) ).
cnf(p760,plain,
( identity_relation(sk11) != identity_relation(relation_dom(sk12))
| in(sk0(relation_dom(sk12),sk12),sk11)
| sk12 = identity_relation(sk11) ),
inference(equality_factoring,[status(thm)],[p632]) ).
cnf(p1892,plain,
( identity_relation(sk11) != identity_relation(sk11)
| in(sk0(relation_dom(sk12),sk12),sk11)
| sk12 = identity_relation(sk11)
| sk12 = identity_relation(sk11) ),
inference(superposition,[status(thm)],[c58,p760]) ).
cnf(p1893,plain,
( identity_relation(sk11) != identity_relation(sk11)
| in(sk0(relation_dom(sk12),sk12),sk11)
| sk12 = identity_relation(sk11) ),
inference(factoring,[status(thm)],[p1892]) ).
cnf(p1894,plain,
( in(sk0(relation_dom(sk12),sk12),sk11)
| sk12 = identity_relation(sk11) ),
inference(equality_resolution,[status(thm)],[p1893]) ).
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(p98,plain,
( X1 != X2
| ~ in(X1,X0)
| in(ordered_pair(X1,X2),identity_relation(X0))
| ~ relation(identity_relation(X0)) ),
inference(equality_resolution,[status(thm)],[c6]) ).
fof(f7,axiom,
! [A] : relation(identity_relation(A)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k6_relat_1) ).
fof(f7_nnf,plain,
! [A] : relation(identity_relation(A)),
inference(nnf_transformation,[status(thm)],[f7]) ).
fof(f7_sk,plain,
! [A] : relation(identity_relation(A)),
inference(skolemisation,[status(esa)],[f7_nnf]) ).
cnf(c18,plain,
relation(identity_relation(X0)),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(p735,plain,
( X0 != X1
| ~ in(X0,X2)
| in(ordered_pair(X0,X1),identity_relation(X2)) ),
inference(resolution,[status(thm)],[p98,c18]) ).
cnf(p1901,plain,
( sk0(relation_dom(sk12),sk12) != X0
| in(ordered_pair(sk0(relation_dom(sk12),sk12),X0),identity_relation(sk11))
| sk12 = identity_relation(sk11) ),
inference(resolution,[status(thm)],[p1894,p735]) ).
cnf(p1984,plain,
( sk0(sk11,sk12) != X0
| in(ordered_pair(sk0(relation_dom(sk12),sk12),X0),identity_relation(sk11))
| sk12 = identity_relation(sk11)
| sk12 = identity_relation(sk11) ),
inference(superposition,[status(thm)],[c58,p1901]) ).
cnf(p2209,plain,
( sk0(sk11,sk12) != X0
| in(ordered_pair(sk0(relation_dom(sk12),sk12),X0),identity_relation(sk11))
| sk12 = identity_relation(sk11) ),
inference(factoring,[status(thm)],[p1984]) ).
cnf(p2210,plain,
( sk12 = identity_relation(sk11)
| in(ordered_pair(sk0(relation_dom(sk12),sk12),sk1(sk11,sk12)),identity_relation(sk11))
| sk12 = identity_relation(sk11) ),
inference(resolution,[status(thm)],[p2209,p1567]) ).
cnf(p2211,plain,
( in(ordered_pair(sk0(relation_dom(sk12),sk12),sk1(sk11,sk12)),identity_relation(sk11))
| sk12 = identity_relation(sk11) ),
inference(factoring,[status(thm)],[p2210]) ).
cnf(c5,plain,
( X2 = X3
| ~ in(ordered_pair(X2,X3),X1)
| X1 != identity_relation(X0)
| ~ relation(X1) ),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(p90,plain,
( X1 = X2
| ~ in(ordered_pair(X1,X2),identity_relation(X0))
| ~ relation(identity_relation(X0)) ),
inference(equality_resolution,[status(thm)],[c5]) ).
cnf(p709,plain,
( X0 = X1
| ~ in(ordered_pair(X0,X1),identity_relation(X2)) ),
inference(resolution,[status(thm)],[p90,c18]) ).
cnf(p2215,plain,
( sk0(relation_dom(sk12),sk12) = sk1(sk11,sk12)
| sk12 = identity_relation(sk11) ),
inference(resolution,[status(thm)],[p2211,p709]) ).
cnf(p1898,plain,
( apply(sk12,sk0(relation_dom(sk12),sk12)) = sk0(relation_dom(sk12),sk12)
| sk12 = identity_relation(sk11)
| sk12 = identity_relation(sk11) ),
inference(resolution,[status(thm)],[p1894,c59]) ).
cnf(p1902,plain,
( apply(sk12,sk0(relation_dom(sk12),sk12)) = sk0(relation_dom(sk12),sk12)
| sk12 = identity_relation(sk11) ),
inference(factoring,[status(thm)],[p1898]) ).
cnf(p1903,plain,
( apply(sk12,sk0(sk11,sk12)) = sk0(relation_dom(sk12),sk12)
| sk12 = identity_relation(sk11)
| sk12 = identity_relation(sk11) ),
inference(superposition,[status(thm)],[c58,p1902]) ).
cnf(p1933,plain,
( apply(sk12,sk0(sk11,sk12)) = sk0(relation_dom(sk12),sk12)
| sk12 = identity_relation(sk11) ),
inference(factoring,[status(thm)],[p1903]) ).
cnf(p1936,plain,
( in(ordered_pair(sk0(sk11,sk12),sk0(relation_dom(sk12),sk12)),sk12)
| sk12 = identity_relation(sk11)
| sk12 = identity_relation(sk11) ),
inference(superposition,[status(thm)],[p1933,p1058]) ).
cnf(p1976,plain,
( in(ordered_pair(sk0(sk11,sk12),sk0(relation_dom(sk12),sk12)),sk12)
| sk12 = identity_relation(sk11) ),
inference(factoring,[status(thm)],[p1936]) ).
cnf(p2249,plain,
( in(ordered_pair(sk0(sk11,sk12),sk1(sk11,sk12)),sk12)
| sk12 = identity_relation(sk11)
| sk12 = identity_relation(sk11) ),
inference(superposition,[status(thm)],[p2215,p1976]) ).
cnf(p2360,plain,
( in(ordered_pair(sk0(sk11,sk12),sk1(sk11,sk12)),sk12)
| sk12 = identity_relation(sk11) ),
inference(factoring,[status(thm)],[p2249]) ).
cnf(p2670,plain,
( sk12 = identity_relation(sk11)
| sk12 = identity_relation(sk11) ),
inference(resolution,[status(thm)],[p2668,p2360]) ).
cnf(p2671,plain,
sk12 = identity_relation(sk11),
inference(factoring,[status(thm)],[p2670]) ).
fof(f37,axiom,
! [A] :
( relation_rng(identity_relation(A)) = A
& relation_dom(identity_relation(A)) = A ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t71_relat_1) ).
fof(f37_nnf,plain,
! [A] :
( relation_rng(identity_relation(A)) = A
& relation_dom(identity_relation(A)) = A ),
inference(nnf_transformation,[status(thm)],[f37]) ).
fof(f37_sk,plain,
! [A] :
( relation_rng(identity_relation(A)) = A
& relation_dom(identity_relation(A)) = A ),
inference(skolemisation,[status(esa)],[f37_nnf]) ).
cnf(c71,plain,
relation_dom(identity_relation(X0)) = X0,
inference(cnf_transformation,[status(esa)],[f37_sk]) ).
cnf(p2677,plain,
relation_dom(sk12) = sk11,
inference(superposition,[status(thm)],[p2671,c71]) ).
cnf(c60,plain,
( sk12 != identity_relation(sk11)
| in(sk13,sk11)
| relation_dom(sk12) != sk11 ),
inference(cnf_transformation,[status(esa)],[f32_sk]) ).
cnf(p2678,plain,
( sk12 != identity_relation(sk11)
| in(sk13,sk11)
| sk11 != sk11 ),
inference(demodulation,[status(thm)],[p2677,c60]) ).
cnf(p2943,plain,
( sk12 != identity_relation(sk11)
| in(sk13,sk11) ),
inference(equality_resolution,[status(thm)],[p2678]) ).
cnf(p2944,plain,
in(sk13,sk11),
inference(resolution,[status(thm)],[p2943,p2671]) ).
cnf(p101,plain,
( X1 != X2
| ~ in(X1,X0)
| in(ordered_pair(X1,X2),sk12)
| sk12 != identity_relation(X0) ),
inference(resolution,[status(thm)],[c6,c55]) ).
cnf(p107,plain,
( ~ in(X1,X0)
| in(ordered_pair(X1,X1),sk12)
| sk12 != identity_relation(X0) ),
inference(equality_resolution,[status(thm)],[p101]) ).
cnf(p2675,plain,
( ~ in(X0,sk11)
| in(ordered_pair(X0,X0),sk12) ),
inference(resolution,[status(thm)],[p2671,p107]) ).
cnf(p2953,plain,
in(ordered_pair(sk13,sk13),sk12),
inference(resolution,[status(thm)],[p2944,p2675]) ).
cnf(p2961,plain,
sk13 = apply(sk12,sk13),
inference(resolution,[status(thm)],[p2953,p706]) ).
cnf(p160,plain,
( in(ordered_pair(X1,X2),identity_relation(X0))
| X2 != apply(identity_relation(X0),X1)
| ~ in(X1,X0)
| ~ function(identity_relation(X0)) ),
inference(resolution,[status(thm)],[c13,c18]) ).
fof(f13,axiom,
! [A] :
( function(identity_relation(A))
& relation(identity_relation(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc2_funct_1) ).
fof(f13_nnf,plain,
! [A] :
( function(identity_relation(A))
& relation(identity_relation(A)) ),
inference(nnf_transformation,[status(thm)],[f13]) ).
fof(f13_sk,plain,
! [A] :
( function(identity_relation(A))
& relation(identity_relation(A)) ),
inference(skolemisation,[status(esa)],[f13_nnf]) ).
cnf(c27,plain,
function(identity_relation(X0)),
inference(cnf_transformation,[status(esa)],[f13_sk]) ).
cnf(p952,plain,
( in(ordered_pair(X0,X2),identity_relation(X1))
| X2 != apply(identity_relation(X1),X0)
| ~ in(X0,X1) ),
inference(resolution,[status(thm)],[p160,c27]) ).
cnf(p2952,plain,
( in(ordered_pair(sk13,X0),identity_relation(sk11))
| X0 != apply(identity_relation(sk11),sk13) ),
inference(resolution,[status(thm)],[p2944,p952]) ).
cnf(p3107,plain,
in(ordered_pair(sk13,apply(identity_relation(sk11),sk13)),identity_relation(sk11)),
inference(equality_resolution,[status(thm)],[p2952]) ).
cnf(p3115,plain,
in(ordered_pair(sk13,apply(identity_relation(sk11),sk13)),sk12),
inference(superposition,[status(thm)],[p2671,p3107]) ).
cnf(p3120,plain,
apply(identity_relation(sk11),sk13) = apply(sk12,sk13),
inference(resolution,[status(thm)],[p3115,p706]) ).
cnf(p3121,plain,
apply(sk12,sk13) = sk13,
inference(superposition,[status(thm)],[p2961,p3120]) ).
cnf(c63,plain,
( sk12 != identity_relation(sk11)
| apply(sk12,sk13) != sk13
| relation_dom(sk12) != sk11 ),
inference(cnf_transformation,[status(esa)],[f32_sk]) ).
cnf(p2680,plain,
( sk12 != identity_relation(sk11)
| apply(sk12,sk13) != sk13
| sk11 != sk11 ),
inference(demodulation,[status(thm)],[p2677,c63]) ).
cnf(p3122,plain,
( sk12 != identity_relation(sk11)
| sk13 != sk13
| sk11 != sk11 ),
inference(demodulation,[status(thm)],[p3121,p2680]) ).
cnf(p3125,plain,
( sk12 != identity_relation(sk11)
| sk13 != sk13 ),
inference(equality_resolution,[status(thm)],[p3122]) ).
cnf(p3127,plain,
sk12 != identity_relation(sk11),
inference(equality_resolution,[status(thm)],[p3125]) ).
cnf(p3128,plain,
$false,
inference(resolution,[status(thm)],[p3127,p2671]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU216+3 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.09/0.37 % Computer : n017.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Thu Sep 24 13:09:00 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 17.51/3.22 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 17.51/3.22 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------