%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SET995+1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/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:44:26 PM UTC 2026
% Result : Theorem 54.14s 7.40s
% Output : Proof 54.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 51
% Number of leaves : 15
% Syntax : Number of formulae : 155 ( 123 unt; 0 def)
% Number of atoms : 297 ( 167 equ)
% Maximal formula atoms : 16 ( 1 avg)
% Number of connectives : 246 ( 104 ~; 71 |; 55 &)
% ( 4 <=>; 12 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 2 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of predicates : 7 ( 5 usr; 1 prp; 0-2 aty)
% Number of functors : 20 ( 20 usr; 7 con; 0-4 aty)
% Number of variables : 165 ( 6 sgn 61 !; 13 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f24,conjecture,
! [A,B] :
( ( function(B)
& relation(B) )
=> ! [C] :
( ( function(C)
& relation(C) )
=> ( ( relation_rng(C) = singleton(A)
& relation_rng(B) = singleton(A)
& relation_dom(B) = relation_dom(C) )
=> B = C ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t17_funct_1) ).
fof(f24_neg,negated_conjecture,
~ ! [A,B] :
( ( function(B)
& relation(B) )
=> ! [C] :
( ( function(C)
& relation(C) )
=> ( ( relation_rng(C) = singleton(A)
& relation_rng(B) = singleton(A)
& relation_dom(B) = relation_dom(C) )
=> B = C ) ) ),
inference(negated_conjecture,[status(cth)],[f24]) ).
fof(f24_nnf,plain,
? [A,B] :
( ? [C] :
( B != C
& relation_rng(C) = singleton(A)
& relation_rng(B) = singleton(A)
& relation_dom(B) = relation_dom(C)
& function(C)
& relation(C) )
& function(B)
& relation(B) ),
inference(nnf_transformation,[status(thm)],[f24_neg]) ).
fof(f24_sk,plain,
( sk14 != sk15
& relation_rng(sk15) = singleton(sk13)
& relation_rng(sk14) = singleton(sk13)
& relation_dom(sk14) = relation_dom(sk15)
& function(sk15)
& relation(sk15)
& function(sk14)
& relation(sk14) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk13,sk14,sk15])],[f24_nnf]) ).
cnf(c55,plain,
sk14 != sk15,
inference(cnf_transformation,[status(esa)],[f24_sk]) ).
cnf(t57,plain,
eq(sk14,sk15) = false,
inference(equality_encoding,[status(esa)],[c55]) ).
cnf(t1595,plain,
eq(sk14,sk15) = false,
inference(orient,[status(thm)],[t57]) ).
fof(f33,axiom,
! [A] :
( ( function(A)
& relation(A) )
=> ! [B] :
( ( function(B)
& relation(B) )
=> ( ( ! [C] :
( in(C,relation_dom(A))
=> apply(A,C) = apply(B,C) )
& relation_dom(A) = relation_dom(B) )
=> A = B ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t9_funct_1) ).
fof(f33_nnf,plain,
! [A] :
( ! [B] :
( A = B
| ? [C] :
( apply(A,C) != apply(B,C)
& in(C,relation_dom(A)) )
| relation_dom(A) != relation_dom(B)
| ~ function(B)
| ~ relation(B) )
| ~ function(A)
| ~ relation(A) ),
inference(nnf_transformation,[status(thm)],[f33]) ).
fof(f33_sk,plain,
! [A,B] :
( A = B
| ( apply(A,sk16(A,B)) != apply(B,sk16(A,B))
& in(sk16(A,B),relation_dom(A)) )
| relation_dom(A) != relation_dom(B)
| ~ function(B)
| ~ relation(B)
| ~ function(A)
| ~ relation(A) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk16])],[f33_nnf]) ).
cnf(c66,plain,
( X0 = X1
| apply(X0,sk16(X0,X1)) != apply(X1,sk16(X0,X1))
| relation_dom(X0) != relation_dom(X1)
| ~ function(X1)
| ~ relation(X1)
| ~ function(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(esa)],[f33_sk]) ).
cnf(t253,plain,
ifeq(relation(X1),true,ifeq(function(X1),true,ifeq(relation(X2),true,ifeq(function(X2),true,ifeq(relation_dom(X1),relation_dom(X2),ifeq(apply(X1,sk16(X1,X2)),apply(X2,sk16(X1,X2)),X1,X2),X2),X2),X2),X2),X2) = X2,
inference(equality_encoding,[status(esa)],[c66]) ).
cnf(t264,plain,
ifeq(relation(X1),true,ifeq(function(X1),true,ifeq(relation(X2),true,ifeq(function(X2),true,ifeq(relation_dom(X1),relation_dom(X2),ifeq(apply(X1,sk16(X1,X2)),apply(X2,sk16(X1,X2)),X1,X2),X2),X2),X2),X2),X2) = X2,
inference(orient,[status(thm)],[t253]) ).
fof(f3,axiom,
! [A,B] :
( B = singleton(A)
<=> ! [C] :
( in(C,B)
<=> C = A ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d1_tarski) ).
fof(f3_nnf,plain,
! [A,B] :
( ( ? [C] :
( ( C = A
& ~ in(C,B) )
| ( C != A
& in(C,B) ) )
| B = singleton(A) )
& ( ! [C] :
( ( C != A
| in(C,B) )
& ( C = A
| ~ in(C,B) ) )
| B != singleton(A) ) ),
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
! [B,A,C] :
( ( ( sk0(A,B) = A
& ~ in(sk0(A,B),B) )
| ( sk0(A,B) != A
& in(sk0(A,B),B) )
| B = singleton(A) )
& ( ( ( C != A
| in(C,B) )
& ( C = A
| ~ in(C,B) ) )
| B != singleton(A) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk0])],[f3_nnf]) ).
cnf(c3,plain,
( X2 = X0
| ~ in(X2,X1)
| X1 != singleton(X0) ),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(t221,plain,
ifeq(X1,singleton(X2),ifeq(in(X3,X1),true,X3,X2),X2) = X2,
inference(equality_encoding,[status(esa)],[c3]) ).
cnf(t259,plain,
ifeq(X1,singleton(X2),ifeq(in(X3,X1),true,X3,X2),X2) = X2,
inference(orient,[status(thm)],[t221]) ).
cnf(t167,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t258,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t167]) ).
cnf(t260,plain,
X1 = ifeq(in(X2,singleton(X1)),true,X2,X1),
inference(cp,[status(thm)],[t259,t258]) ).
cnf(t1735,plain,
ifeq(in(X1,singleton(X2)),true,X1,X2) = X2,
inference(orient,[status(thm)],[t260]) ).
fof(f4,axiom,
! [A] :
( ( function(A)
& relation(A) )
=> ! [B] :
( B = relation_rng(A)
<=> ! [C] :
( in(C,B)
<=> ? [D] :
( C = apply(A,D)
& in(D,relation_dom(A)) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d5_funct_1) ).
fof(f4_nnf,plain,
! [A] :
( ! [B] :
( ( ? [C] :
( ( ? [D] :
( C = apply(A,D)
& in(D,relation_dom(A)) )
& ~ in(C,B) )
| ( ! [D] :
( C != apply(A,D)
| ~ in(D,relation_dom(A)) )
& in(C,B) ) )
| B = relation_rng(A) )
& ( ! [C] :
( ( ! [D] :
( C != apply(A,D)
| ~ in(D,relation_dom(A)) )
| in(C,B) )
& ( ? [D] :
( C = apply(A,D)
& in(D,relation_dom(A)) )
| ~ in(C,B) ) )
| B != relation_rng(A) ) )
| ~ function(A)
| ~ relation(A) ),
inference(nnf_transformation,[status(thm)],[f4]) ).
fof(f4_sk,plain,
! [A,B,C,D] :
( ( ( ( sk2(A,B) = apply(A,sk3(A,B))
& in(sk3(A,B),relation_dom(A))
& ~ in(sk2(A,B),B) )
| ( ( sk2(A,B) != apply(A,D)
| ~ in(D,relation_dom(A)) )
& in(sk2(A,B),B) )
| B = relation_rng(A) )
& ( ( ( C != apply(A,D)
| ~ in(D,relation_dom(A))
| in(C,B) )
& ( ( C = apply(A,sk1(A,B,C))
& in(sk1(A,B,C),relation_dom(A)) )
| ~ in(C,B) ) )
| B != relation_rng(A) ) )
| ~ function(A)
| ~ relation(A) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk1,sk2,sk3])],[f4_nnf]) ).
cnf(c11,plain,
( X2 != apply(X0,X3)
| ~ in(X3,relation_dom(X0))
| in(X2,X1)
| X1 != relation_rng(X0)
| ~ function(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(t247,plain,
ifeq(relation(X1),true,ifeq(function(X1),true,ifeq(X2,relation_rng(X1),ifeq(in(X3,relation_dom(X1)),true,ifeq(X4,apply(X1,X3),in(X4,X2),true),true),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c11]) ).
cnf(t324,plain,
ifeq(relation(X1),true,ifeq(function(X1),true,ifeq(X2,relation_rng(X1),ifeq(in(X3,relation_dom(X1)),true,ifeq(X4,apply(X1,X3),in(X4,X2),true),true),true),true),true) = true,
inference(orient,[status(thm)],[t247]) ).
cnf(t325,plain,
true = ifeq(relation(X1),true,ifeq(function(X1),true,ifeq(in(X2,relation_dom(X1)),true,ifeq(X3,apply(X1,X2),in(X3,relation_rng(X1)),true),true),true),true),
inference(cp,[status(thm)],[t324,t258]) ).
cnf(t2234,plain,
ifeq(relation(X1),true,ifeq(function(X1),true,ifeq(in(X2,relation_dom(X1)),true,ifeq(X3,apply(X1,X2),in(X3,relation_rng(X1)),true),true),true),true) = true,
inference(orient,[status(thm)],[t325]) ).
cnf(c48,plain,
relation(sk14),
inference(cnf_transformation,[status(esa)],[f24_sk]) ).
cnf(t21,plain,
relation(sk14) = true,
inference(equality_encoding,[status(esa)],[c48]) ).
cnf(t1010,plain,
relation(sk14) = true,
inference(orient,[status(thm)],[t21]) ).
cnf(t2239,plain,
true = ifeq(true,true,ifeq(function(sk14),true,ifeq(in(X1,relation_dom(sk14)),true,ifeq(X2,apply(sk14,X1),in(X2,relation_rng(sk14)),true),true),true),true),
inference(cp,[status(thm)],[t2234,t1010]) ).
cnf(t3620,plain,
true = ifeq(function(sk14),true,ifeq(in(X1,relation_dom(sk14)),true,ifeq(X2,apply(sk14,X1),in(X2,relation_rng(sk14)),true),true),true),
inference(step,[status(thm)],[t2239,t258]) ).
cnf(c49,plain,
function(sk14),
inference(cnf_transformation,[status(esa)],[f24_sk]) ).
cnf(t11,plain,
function(sk14) = true,
inference(equality_encoding,[status(esa)],[c49]) ).
cnf(t1234,plain,
function(sk14) = true,
inference(orient,[status(thm)],[t11]) ).
cnf(t3621,plain,
true = ifeq(true,true,ifeq(in(X1,relation_dom(sk14)),true,ifeq(X2,apply(sk14,X1),in(X2,relation_rng(sk14)),true),true),true),
inference(step,[status(thm)],[t3620,t1234]) ).
cnf(t3622,plain,
true = ifeq(in(X1,relation_dom(sk14)),true,ifeq(X2,apply(sk14,X1),in(X2,relation_rng(sk14)),true),true),
inference(step,[status(thm)],[t3621,t258]) ).
cnf(c52,plain,
relation_dom(sk14) = relation_dom(sk15),
inference(cnf_transformation,[status(esa)],[f24_sk]) ).
cnf(t87,plain,
relation_dom(sk15) = relation_dom(sk14),
inference(equality_encoding,[status(esa)],[c52]) ).
cnf(t1488,plain,
relation_dom(sk14) = relation_dom(sk15),
inference(orient,[status(thm)],[t87]) ).
cnf(t3623,plain,
true = ifeq(in(X1,relation_dom(sk15)),true,ifeq(X2,apply(sk14,X1),in(X2,relation_rng(sk14)),true),true),
inference(step,[status(thm)],[t3622,t1488]) ).
cnf(c53,plain,
relation_rng(sk14) = singleton(sk13),
inference(cnf_transformation,[status(esa)],[f24_sk]) ).
cnf(t114,plain,
singleton(sk13) = relation_rng(sk14),
inference(equality_encoding,[status(esa)],[c53]) ).
cnf(t1454,plain,
relation_rng(sk14) = singleton(sk13),
inference(orient,[status(thm)],[t114]) ).
cnf(t3624,plain,
true = ifeq(in(X1,relation_dom(sk15)),true,ifeq(X2,apply(sk14,X1),in(X2,singleton(sk13)),true),true),
inference(step,[status(thm)],[t3623,t1454]) ).
cnf(t2985,plain,
ifeq(in(X1,relation_dom(sk15)),true,ifeq(X2,apply(sk14,X1),in(X2,singleton(sk13)),true),true) = true,
inference(orient,[status(thm)],[t3624]) ).
cnf(t208,plain,
ifeq(eq(X1,X2),true,X1,X2) = X2,
introduced(definition) ).
cnf(t263,plain,
ifeq(eq(X1,X2),true,X1,X2) = X2,
inference(orient,[status(thm)],[t208]) ).
cnf(c65,plain,
( X0 = X1
| in(sk16(X0,X1),relation_dom(X0))
| relation_dom(X0) != relation_dom(X1)
| ~ function(X1)
| ~ relation(X1)
| ~ function(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(esa)],[f33_sk]) ).
cnf(t251,plain,
ifeq(relation(X1),true,ifeq(function(X1),true,ifeq(relation(X2),true,ifeq(function(X2),true,ifeq(relation_dom(X1),relation_dom(X2),or(eq(in(sk16(X1,X2),relation_dom(X1)),true),eq(X1,X2)),true),true),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c65]) ).
cnf(t329,plain,
ifeq(relation(X1),true,ifeq(function(X1),true,ifeq(relation(X2),true,ifeq(function(X2),true,ifeq(relation_dom(X1),relation_dom(X2),or(eq(in(sk16(X1,X2),relation_dom(X1)),true),eq(X1,X2)),true),true),true),true),true) = true,
inference(orient,[status(thm)],[t251]) ).
cnf(t1597,plain,
true = ifeq(relation(sk14),true,ifeq(function(sk14),true,ifeq(relation(sk15),true,ifeq(function(sk15),true,ifeq(relation_dom(sk14),relation_dom(sk15),or(eq(in(sk16(sk14,sk15),relation_dom(sk14)),true),false),true),true),true),true),true),
inference(cp,[status(thm)],[t329,t1595]) ).
cnf(t3383,plain,
true = ifeq(true,true,ifeq(function(sk14),true,ifeq(relation(sk15),true,ifeq(function(sk15),true,ifeq(relation_dom(sk14),relation_dom(sk15),or(eq(in(sk16(sk14,sk15),relation_dom(sk14)),true),false),true),true),true),true),true),
inference(step,[status(thm)],[t1597,t1010]) ).
cnf(t3384,plain,
true = ifeq(function(sk14),true,ifeq(relation(sk15),true,ifeq(function(sk15),true,ifeq(relation_dom(sk14),relation_dom(sk15),or(eq(in(sk16(sk14,sk15),relation_dom(sk14)),true),false),true),true),true),true),
inference(step,[status(thm)],[t3383,t258]) ).
cnf(t3385,plain,
true = ifeq(true,true,ifeq(relation(sk15),true,ifeq(function(sk15),true,ifeq(relation_dom(sk14),relation_dom(sk15),or(eq(in(sk16(sk14,sk15),relation_dom(sk14)),true),false),true),true),true),true),
inference(step,[status(thm)],[t3384,t1234]) ).
cnf(t3386,plain,
true = ifeq(relation(sk15),true,ifeq(function(sk15),true,ifeq(relation_dom(sk14),relation_dom(sk15),or(eq(in(sk16(sk14,sk15),relation_dom(sk14)),true),false),true),true),true),
inference(step,[status(thm)],[t3385,t258]) ).
cnf(c50,plain,
relation(sk15),
inference(cnf_transformation,[status(esa)],[f24_sk]) ).
cnf(t22,plain,
relation(sk15) = true,
inference(equality_encoding,[status(esa)],[c50]) ).
cnf(t1024,plain,
relation(sk15) = true,
inference(orient,[status(thm)],[t22]) ).
cnf(t3387,plain,
true = ifeq(true,true,ifeq(function(sk15),true,ifeq(relation_dom(sk14),relation_dom(sk15),or(eq(in(sk16(sk14,sk15),relation_dom(sk14)),true),false),true),true),true),
inference(step,[status(thm)],[t3386,t1024]) ).
cnf(t3388,plain,
true = ifeq(function(sk15),true,ifeq(relation_dom(sk14),relation_dom(sk15),or(eq(in(sk16(sk14,sk15),relation_dom(sk14)),true),false),true),true),
inference(step,[status(thm)],[t3387,t258]) ).
cnf(c51,plain,
function(sk15),
inference(cnf_transformation,[status(esa)],[f24_sk]) ).
cnf(t12,plain,
function(sk15) = true,
inference(equality_encoding,[status(esa)],[c51]) ).
cnf(t1246,plain,
function(sk15) = true,
inference(orient,[status(thm)],[t12]) ).
cnf(t3389,plain,
true = ifeq(true,true,ifeq(relation_dom(sk14),relation_dom(sk15),or(eq(in(sk16(sk14,sk15),relation_dom(sk14)),true),false),true),true),
inference(step,[status(thm)],[t3388,t1246]) ).
cnf(t3390,plain,
true = ifeq(relation_dom(sk14),relation_dom(sk15),or(eq(in(sk16(sk14,sk15),relation_dom(sk14)),true),false),true),
inference(step,[status(thm)],[t3389,t258]) ).
cnf(t3391,plain,
true = ifeq(relation_dom(sk15),relation_dom(sk15),or(eq(in(sk16(sk14,sk15),relation_dom(sk14)),true),false),true),
inference(step,[status(thm)],[t3390,t1488]) ).
cnf(t3392,plain,
true = or(eq(in(sk16(sk14,sk15),relation_dom(sk14)),true),false),
inference(step,[status(thm)],[t3391,t258]) ).
cnf(t64,plain,
or(X1,false) = X1,
introduced(definition) ).
cnf(t256,plain,
or(X1,false) = X1,
inference(orient,[status(thm)],[t64]) ).
cnf(t3393,plain,
true = eq(in(sk16(sk14,sk15),relation_dom(sk14)),true),
inference(step,[status(thm)],[t3392,t256]) ).
cnf(t3394,plain,
true = eq(in(sk16(sk14,sk15),relation_dom(sk15)),true),
inference(step,[status(thm)],[t3393,t1488]) ).
cnf(t1850,plain,
eq(in(sk16(sk14,sk15),relation_dom(sk15)),true) = true,
inference(orient,[status(thm)],[t3394]) ).
cnf(t1851,plain,
true = ifeq(true,true,in(sk16(sk14,sk15),relation_dom(sk15)),true),
inference(cp,[status(thm)],[t263,t1850]) ).
cnf(t3395,plain,
true = in(sk16(sk14,sk15),relation_dom(sk15)),
inference(step,[status(thm)],[t1851,t258]) ).
cnf(t1854,plain,
in(sk16(sk14,sk15),relation_dom(sk15)) = true,
inference(orient,[status(thm)],[t3395]) ).
cnf(t2988,plain,
true = ifeq(true,true,ifeq(X1,apply(sk14,sk16(sk14,sk15)),in(X1,singleton(sk13)),true),true),
inference(cp,[status(thm)],[t2985,t1854]) ).
cnf(t3625,plain,
true = ifeq(X1,apply(sk14,sk16(sk14,sk15)),in(X1,singleton(sk13)),true),
inference(step,[status(thm)],[t2988,t258]) ).
cnf(t2993,plain,
ifeq(X1,apply(sk14,sk16(sk14,sk15)),in(X1,singleton(sk13)),true) = true,
inference(orient,[status(thm)],[t3625]) ).
cnf(t2994,plain,
true = in(apply(sk14,sk16(sk14,sk15)),singleton(sk13)),
inference(cp,[status(thm)],[t2993,t258]) ).
cnf(t2998,plain,
in(apply(sk14,sk16(sk14,sk15)),singleton(sk13)) = true,
inference(orient,[status(thm)],[t2994]) ).
cnf(t3003,plain,
sk13 = ifeq(true,true,apply(sk14,sk16(sk14,sk15)),sk13),
inference(cp,[status(thm)],[t1735,t2998]) ).
cnf(t3626,plain,
sk13 = apply(sk14,sk16(sk14,sk15)),
inference(step,[status(thm)],[t3003,t258]) ).
cnf(t3021,plain,
apply(sk14,sk16(sk14,sk15)) = sk13,
inference(orient,[status(thm)],[t3626]) ).
cnf(t3024,plain,
sk15 = ifeq(relation(sk14),true,ifeq(function(sk14),true,ifeq(relation(sk15),true,ifeq(function(sk15),true,ifeq(relation_dom(sk14),relation_dom(sk15),ifeq(sk13,apply(sk15,sk16(sk14,sk15)),sk14,sk15),sk15),sk15),sk15),sk15),sk15),
inference(cp,[status(thm)],[t264,t3021]) ).
cnf(t3629,plain,
sk15 = ifeq(true,true,ifeq(function(sk14),true,ifeq(relation(sk15),true,ifeq(function(sk15),true,ifeq(relation_dom(sk14),relation_dom(sk15),ifeq(sk13,apply(sk15,sk16(sk14,sk15)),sk14,sk15),sk15),sk15),sk15),sk15),sk15),
inference(step,[status(thm)],[t3024,t1010]) ).
cnf(t3630,plain,
sk15 = ifeq(function(sk14),true,ifeq(relation(sk15),true,ifeq(function(sk15),true,ifeq(relation_dom(sk14),relation_dom(sk15),ifeq(sk13,apply(sk15,sk16(sk14,sk15)),sk14,sk15),sk15),sk15),sk15),sk15),
inference(step,[status(thm)],[t3629,t258]) ).
cnf(t3631,plain,
sk15 = ifeq(true,true,ifeq(relation(sk15),true,ifeq(function(sk15),true,ifeq(relation_dom(sk14),relation_dom(sk15),ifeq(sk13,apply(sk15,sk16(sk14,sk15)),sk14,sk15),sk15),sk15),sk15),sk15),
inference(step,[status(thm)],[t3630,t1234]) ).
cnf(t3632,plain,
sk15 = ifeq(relation(sk15),true,ifeq(function(sk15),true,ifeq(relation_dom(sk14),relation_dom(sk15),ifeq(sk13,apply(sk15,sk16(sk14,sk15)),sk14,sk15),sk15),sk15),sk15),
inference(step,[status(thm)],[t3631,t258]) ).
cnf(t3633,plain,
sk15 = ifeq(true,true,ifeq(function(sk15),true,ifeq(relation_dom(sk14),relation_dom(sk15),ifeq(sk13,apply(sk15,sk16(sk14,sk15)),sk14,sk15),sk15),sk15),sk15),
inference(step,[status(thm)],[t3632,t1024]) ).
cnf(t3634,plain,
sk15 = ifeq(function(sk15),true,ifeq(relation_dom(sk14),relation_dom(sk15),ifeq(sk13,apply(sk15,sk16(sk14,sk15)),sk14,sk15),sk15),sk15),
inference(step,[status(thm)],[t3633,t258]) ).
cnf(t3635,plain,
sk15 = ifeq(true,true,ifeq(relation_dom(sk14),relation_dom(sk15),ifeq(sk13,apply(sk15,sk16(sk14,sk15)),sk14,sk15),sk15),sk15),
inference(step,[status(thm)],[t3634,t1246]) ).
cnf(t3636,plain,
sk15 = ifeq(relation_dom(sk14),relation_dom(sk15),ifeq(sk13,apply(sk15,sk16(sk14,sk15)),sk14,sk15),sk15),
inference(step,[status(thm)],[t3635,t258]) ).
cnf(t3637,plain,
sk15 = ifeq(relation_dom(sk15),relation_dom(sk15),ifeq(sk13,apply(sk15,sk16(sk14,sk15)),sk14,sk15),sk15),
inference(step,[status(thm)],[t3636,t1488]) ).
cnf(t3638,plain,
sk15 = ifeq(sk13,apply(sk15,sk16(sk14,sk15)),sk14,sk15),
inference(step,[status(thm)],[t3637,t258]) ).
cnf(t2245,plain,
true = ifeq(relation(sk15),true,ifeq(function(sk15),true,ifeq(true,true,ifeq(X1,apply(sk15,sk16(sk14,sk15)),in(X1,relation_rng(sk15)),true),true),true),true),
inference(cp,[status(thm)],[t2234,t1854]) ).
cnf(t3452,plain,
true = ifeq(true,true,ifeq(function(sk15),true,ifeq(true,true,ifeq(X1,apply(sk15,sk16(sk14,sk15)),in(X1,relation_rng(sk15)),true),true),true),true),
inference(step,[status(thm)],[t2245,t1024]) ).
cnf(t3453,plain,
true = ifeq(function(sk15),true,ifeq(true,true,ifeq(X1,apply(sk15,sk16(sk14,sk15)),in(X1,relation_rng(sk15)),true),true),true),
inference(step,[status(thm)],[t3452,t258]) ).
cnf(t3454,plain,
true = ifeq(true,true,ifeq(true,true,ifeq(X1,apply(sk15,sk16(sk14,sk15)),in(X1,relation_rng(sk15)),true),true),true),
inference(step,[status(thm)],[t3453,t1246]) ).
cnf(t3455,plain,
true = ifeq(true,true,ifeq(X1,apply(sk15,sk16(sk14,sk15)),in(X1,relation_rng(sk15)),true),true),
inference(step,[status(thm)],[t3454,t258]) ).
cnf(t3456,plain,
true = ifeq(X1,apply(sk15,sk16(sk14,sk15)),in(X1,relation_rng(sk15)),true),
inference(step,[status(thm)],[t3455,t258]) ).
cnf(c54,plain,
relation_rng(sk15) = singleton(sk13),
inference(cnf_transformation,[status(esa)],[f24_sk]) ).
cnf(t115,plain,
singleton(sk13) = relation_rng(sk15),
inference(equality_encoding,[status(esa)],[c54]) ).
cnf(t1471,plain,
relation_rng(sk15) = singleton(sk13),
inference(orient,[status(thm)],[t115]) ).
cnf(t3457,plain,
true = ifeq(X1,apply(sk15,sk16(sk14,sk15)),in(X1,singleton(sk13)),true),
inference(step,[status(thm)],[t3456,t1471]) ).
cnf(t2255,plain,
ifeq(X1,apply(sk15,sk16(sk14,sk15)),in(X1,singleton(sk13)),true) = true,
inference(orient,[status(thm)],[t3457]) ).
cnf(t2256,plain,
true = in(apply(sk15,sk16(sk14,sk15)),singleton(sk13)),
inference(cp,[status(thm)],[t2255,t258]) ).
cnf(t2260,plain,
in(apply(sk15,sk16(sk14,sk15)),singleton(sk13)) = true,
inference(orient,[status(thm)],[t2256]) ).
cnf(t2265,plain,
sk13 = ifeq(true,true,apply(sk15,sk16(sk14,sk15)),sk13),
inference(cp,[status(thm)],[t1735,t2260]) ).
cnf(t3458,plain,
sk13 = apply(sk15,sk16(sk14,sk15)),
inference(step,[status(thm)],[t2265,t258]) ).
cnf(t2277,plain,
apply(sk15,sk16(sk14,sk15)) = sk13,
inference(orient,[status(thm)],[t3458]) ).
cnf(t3639,plain,
sk15 = ifeq(sk13,sk13,sk14,sk15),
inference(step,[status(thm)],[t3638,t2277]) ).
cnf(t3640,plain,
sk15 = sk14,
inference(step,[status(thm)],[t3639,t258]) ).
cnf(t3028,plain,
sk14 = sk15,
inference(orient,[status(thm)],[t3640]) ).
cnf(t3642,plain,
eq(sk15,sk15) = false,
inference(step,[status(thm)],[t1595,t3028]) ).
cnf(t56,plain,
eq(X1,X1) = true,
introduced(definition) ).
cnf(t810,plain,
eq(X1,X1) = true,
inference(orient,[status(thm)],[t56]) ).
cnf(t3643,plain,
true = false,
inference(step,[status(thm)],[t3642,t810]) ).
cnf(t3030,plain,
true = false,
inference(rw,[status(thm)],[t3643]) ).
cnf(t3057,plain,
false = true,
inference(orient,[status(thm)],[t3030]) ).
fof(f0,axiom,
! [A,B] :
( in(A,B)
=> ~ in(B,A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',antisymmetry_r2_hidden) ).
fof(f0_nnf,plain,
! [A,B] :
( ~ in(B,A)
| ~ in(A,B) ),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [A,B] :
( ~ in(B,A)
| ~ in(A,B) ),
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
( ~ in(X1,X0)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
fof(f7,axiom,
! [A] : ~ empty(powerset(A)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc1_subset_1) ).
fof(f7_nnf,plain,
! [A] : ~ empty(powerset(A)),
inference(nnf_transformation,[status(thm)],[f7]) ).
fof(f7_sk,plain,
! [A] : ~ empty(powerset(A)),
inference(skolemisation,[status(esa)],[f7_nnf]) ).
cnf(c22,plain,
~ empty(powerset(X0)),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
fof(f9,axiom,
! [A] : ~ empty(singleton(A)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc2_subset_1) ).
fof(f9_nnf,plain,
! [A] : ~ empty(singleton(A)),
inference(nnf_transformation,[status(thm)],[f9]) ).
fof(f9_sk,plain,
! [A] : ~ empty(singleton(A)),
inference(skolemisation,[status(esa)],[f9_nnf]) ).
cnf(c24,plain,
~ empty(singleton(X0)),
inference(cnf_transformation,[status(esa)],[f9_sk]) ).
fof(f19,axiom,
? [A] :
( relation(A)
& ~ empty(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc2_relat_1) ).
fof(f19_nnf,plain,
? [A] :
( relation(A)
& ~ empty(A) ),
inference(nnf_transformation,[status(thm)],[f19]) ).
fof(f19_sk,plain,
( relation(sk9)
& ~ empty(sk9) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk9])],[f19_nnf]) ).
cnf(c40,plain,
~ empty(sk9),
inference(cnf_transformation,[status(esa)],[f19_sk]) ).
fof(f21,axiom,
? [A] : ~ empty(A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc2_xboole_0) ).
fof(f21_nnf,plain,
? [A] : ~ empty(A),
inference(nnf_transformation,[status(thm)],[f21]) ).
fof(f21_sk,plain,
~ empty(sk11),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk11])],[f21_nnf]) ).
cnf(c44,plain,
~ empty(sk11),
inference(cnf_transformation,[status(esa)],[f21_sk]) ).
fof(f29,axiom,
! [A,B,C] :
~ ( empty(C)
& element(B,powerset(C))
& in(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t5_subset) ).
fof(f29_nnf,plain,
! [A,B,C] :
( ~ empty(C)
| ~ element(B,powerset(C))
| ~ in(A,B) ),
inference(nnf_transformation,[status(thm)],[f29]) ).
fof(f29_sk,plain,
! [A,B,C] :
( ~ empty(C)
| ~ element(B,powerset(C))
| ~ in(A,B) ),
inference(skolemisation,[status(esa)],[f29_nnf]) ).
cnf(c61,plain,
( ~ empty(X2)
| ~ element(X1,powerset(X2))
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f29_sk]) ).
fof(f31,axiom,
! [A,B] :
~ ( empty(B)
& in(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t7_boole) ).
fof(f31_nnf,plain,
! [A,B] :
( ~ empty(B)
| ~ in(A,B) ),
inference(nnf_transformation,[status(thm)],[f31]) ).
fof(f31_sk,plain,
! [A,B] :
( ~ empty(B)
| ~ in(A,B) ),
inference(skolemisation,[status(esa)],[f31_nnf]) ).
cnf(c63,plain,
( ~ empty(X1)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f31_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c0,c22,c24,c40,c44,c55,c61,c63]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t3057]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SET995+1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.07/0.36 % Computer : n014.cluster.edu
% 0.07/0.36 % Model : x86_64 x86_64
% 0.07/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.36 % Memory : 8046.5625MB
% 0.07/0.36 % OS : Linux 6.8.0-71-generic
% 0.07/0.36 % CPULimit : 300
% 0.07/0.36 % WCLimit : 300
% 0.07/0.36 % DateTime : Thu Sep 24 12:32:19 UTC 2026
% 0.12/0.36 % CPUTime :
% 0.12/0.36 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 54.14/7.40 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 54.14/7.40 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------