%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SEU430+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n016.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:52:04 PM UTC 2026
% Result : Theorem 7.71s 1.45s
% Output : Proof 7.71s
% Verified :
% SZS Type : Refutation
% Derivation depth : 35
% Number of leaves : 4
% Syntax : Number of formulae : 69 ( 9 unt; 0 def)
% Number of atoms : 200 ( 98 equ)
% Maximal formula atoms : 14 ( 2 avg)
% Number of connectives : 197 ( 66 ~; 98 |; 23 &)
% ( 5 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 4 con; 0-3 aty)
% Number of variables : 80 ( 5 sgn 32 !; 8 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f4,axiom,
! [A,B] :
( B = k3_tarski(A)
<=> ! [C] :
( r2_hidden(C,B)
<=> ? [D] :
( r2_hidden(D,A)
& r2_hidden(C,D) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d4_tarski) ).
fof(f4_nnf,plain,
! [A,B] :
( ( ? [C] :
( ( ? [D] :
( r2_hidden(D,A)
& r2_hidden(C,D) )
& ~ r2_hidden(C,B) )
| ( ! [D] :
( ~ r2_hidden(D,A)
| ~ r2_hidden(C,D) )
& r2_hidden(C,B) ) )
| B = k3_tarski(A) )
& ( ! [C] :
( ( ! [D] :
( ~ r2_hidden(D,A)
| ~ r2_hidden(C,D) )
| r2_hidden(C,B) )
& ( ? [D] :
( r2_hidden(D,A)
& r2_hidden(C,D) )
| ~ r2_hidden(C,B) ) )
| B != k3_tarski(A) ) ),
inference(nnf_transformation,[status(thm)],[f4]) ).
fof(f4_sk,plain,
! [B,A,C,D] :
( ( ( r2_hidden(sk6(A,B),A)
& r2_hidden(sk5(A,B),sk6(A,B))
& ~ r2_hidden(sk5(A,B),B) )
| ( ( ~ r2_hidden(D,A)
| ~ r2_hidden(sk5(A,B),D) )
& r2_hidden(sk5(A,B),B) )
| B = k3_tarski(A) )
& ( ( ( ~ r2_hidden(D,A)
| ~ r2_hidden(C,D)
| r2_hidden(C,B) )
& ( ( r2_hidden(sk4(A,B,C),A)
& r2_hidden(C,sk4(A,B,C)) )
| ~ r2_hidden(C,B) ) )
| B != k3_tarski(A) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk4,sk5,sk6])],[f4_nnf]) ).
cnf(c12,plain,
( r2_hidden(sk4(X0,X1,X2),X0)
| ~ r2_hidden(X2,X1)
| X1 != k3_tarski(X0) ),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(p67,plain,
( r2_hidden(sk4(X1,k3_tarski(X1),X0),X1)
| ~ r2_hidden(X0,k3_tarski(X1)) ),
inference(equality_resolution,[status(thm)],[c12]) ).
fof(f3,axiom,
! [A] :
( A = k1_xboole_0
<=> ! [B] : ~ r2_hidden(B,A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d1_xboole_0) ).
fof(f3_nnf,plain,
! [A] :
( ( ? [B] : r2_hidden(B,A)
| A = k1_xboole_0 )
& ( ! [B] : ~ r2_hidden(B,A)
| A != k1_xboole_0 ) ),
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
! [A,B] :
( ( r2_hidden(sk3(A),A)
| A = k1_xboole_0 )
& ( ~ r2_hidden(B,A)
| A != k1_xboole_0 ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk3])],[f3_nnf]) ).
cnf(c10,plain,
( r2_hidden(sk3(X0),X0)
| X0 = k1_xboole_0 ),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p284,plain,
( k3_tarski(X0) = k1_xboole_0
| r2_hidden(sk4(X0,k3_tarski(X0),sk3(k3_tarski(X0))),X0) ),
inference(resolution,[status(thm)],[p67,c10]) ).
fof(f19,axiom,
! [A,B] :
( m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(A)))
=> k5_setfam_1(A,B) = k3_tarski(B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k5_setfam_1) ).
fof(f19_nnf,plain,
! [A,B] :
( k5_setfam_1(A,B) = k3_tarski(B)
| ~ m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(A))) ),
inference(nnf_transformation,[status(thm)],[f19]) ).
fof(f19_sk,plain,
! [B,A] :
( k5_setfam_1(A,B) = k3_tarski(B)
| ~ m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(A))) ),
inference(skolemisation,[status(esa)],[f19_nnf]) ).
cnf(c42,plain,
( k5_setfam_1(X0,X1) = k3_tarski(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(k1_zfmisc_1(X0))) ),
inference(cnf_transformation,[status(esa)],[f19_sk]) ).
fof(f0,conjecture,
! [A,B] :
( m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(A)))
=> ( k5_setfam_1(A,B) = k1_xboole_0
<=> ! [C] :
( r2_hidden(C,B)
=> C = k1_xboole_0 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t30_relset_2) ).
fof(f0_neg,negated_conjecture,
~ ! [A,B] :
( m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(A)))
=> ( k5_setfam_1(A,B) = k1_xboole_0
<=> ! [C] :
( r2_hidden(C,B)
=> C = k1_xboole_0 ) ) ),
inference(negated_conjecture,[status(cth)],[f0]) ).
fof(f0_nnf,plain,
? [A,B] :
( ( ( ! [C] :
( C = k1_xboole_0
| ~ r2_hidden(C,B) )
& k5_setfam_1(A,B) != k1_xboole_0 )
| ( ? [C] :
( C != k1_xboole_0
& r2_hidden(C,B) )
& k5_setfam_1(A,B) = k1_xboole_0 ) )
& m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(A))) ),
inference(nnf_transformation,[status(thm)],[f0_neg]) ).
fof(f0_sk,plain,
! [C] :
( ( ( ( C = k1_xboole_0
| ~ r2_hidden(C,sk1) )
& k5_setfam_1(sk0,sk1) != k1_xboole_0 )
| ( sk2 != k1_xboole_0
& r2_hidden(sk2,sk1)
& k5_setfam_1(sk0,sk1) = k1_xboole_0 ) )
& m1_subset_1(sk1,k1_zfmisc_1(k1_zfmisc_1(sk0))) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk0,sk1,sk2])],[f0_nnf]) ).
cnf(c0,plain,
m1_subset_1(sk1,k1_zfmisc_1(k1_zfmisc_1(sk0))),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p166,plain,
k5_setfam_1(sk0,sk1) = k3_tarski(sk1),
inference(resolution,[status(thm)],[c42,c0]) ).
cnf(c2,plain,
( X2 = k1_xboole_0
| ~ r2_hidden(X2,sk1)
| k5_setfam_1(sk0,sk1) = k1_xboole_0 ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p167,plain,
( X0 = k1_xboole_0
| ~ r2_hidden(X0,sk1)
| k3_tarski(sk1) = k1_xboole_0 ),
inference(demodulation,[status(thm)],[p166,c2]) ).
cnf(c16,plain,
( r2_hidden(sk6(X0,X1),X0)
| r2_hidden(sk5(X0,X1),X1)
| X1 = k3_tarski(X0) ),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(c4,plain,
( X2 = k1_xboole_0
| ~ r2_hidden(X2,sk1)
| r2_hidden(sk2,sk1) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p77,plain,
( sk6(sk1,X0) = k1_xboole_0
| r2_hidden(sk2,sk1)
| r2_hidden(sk5(sk1,X0),X0)
| X0 = k3_tarski(sk1) ),
inference(resolution,[status(thm)],[c16,c4]) ).
cnf(c9,plain,
( ~ r2_hidden(X1,X0)
| X0 != k1_xboole_0 ),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p55,plain,
~ r2_hidden(X0,k1_xboole_0),
inference(equality_resolution,[status(thm)],[c9]) ).
cnf(p100,plain,
( sk6(sk1,k1_xboole_0) = k1_xboole_0
| r2_hidden(sk2,sk1)
| k1_xboole_0 = k3_tarski(sk1) ),
inference(resolution,[status(thm)],[p77,p55]) ).
cnf(p103,plain,
( ~ r2_hidden(X0,sk6(sk1,k1_xboole_0))
| r2_hidden(sk2,sk1)
| k1_xboole_0 = k3_tarski(sk1) ),
inference(resolution,[status(thm)],[p100,c9]) ).
cnf(c15,plain,
( r2_hidden(sk5(X0,X1),sk6(X0,X1))
| r2_hidden(sk5(X0,X1),X1)
| X1 = k3_tarski(X0) ),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(p106,plain,
( r2_hidden(sk5(sk1,k1_xboole_0),k1_xboole_0)
| k1_xboole_0 = k3_tarski(sk1)
| r2_hidden(sk2,sk1)
| k1_xboole_0 = k3_tarski(sk1) ),
inference(resolution,[status(thm)],[p103,c15]) ).
cnf(p111,plain,
( r2_hidden(sk5(sk1,k1_xboole_0),k1_xboole_0)
| r2_hidden(sk2,sk1)
| k1_xboole_0 = k3_tarski(sk1) ),
inference(factoring,[status(thm)],[p106]) ).
cnf(p113,plain,
( r2_hidden(sk2,sk1)
| k1_xboole_0 = k3_tarski(sk1) ),
inference(resolution,[status(thm)],[p111,p55]) ).
cnf(p190,plain,
( k3_tarski(sk1) = k1_xboole_0
| r2_hidden(sk2,sk1) ),
inference(superposition,[status(thm)],[p113,p166]) ).
cnf(c3,plain,
( k5_setfam_1(sk0,sk1) != k1_xboole_0
| r2_hidden(sk2,sk1) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p168,plain,
( k3_tarski(sk1) != k1_xboole_0
| r2_hidden(sk2,sk1) ),
inference(demodulation,[status(thm)],[p166,c3]) ).
cnf(p203,plain,
( r2_hidden(sk2,sk1)
| r2_hidden(sk2,sk1) ),
inference(resolution,[status(thm)],[p190,p168]) ).
cnf(p204,plain,
r2_hidden(sk2,sk1),
inference(factoring,[status(thm)],[p203]) ).
cnf(p220,plain,
( sk2 = k1_xboole_0
| k3_tarski(sk1) = k1_xboole_0 ),
inference(resolution,[status(thm)],[p167,p204]) ).
cnf(p221,plain,
( ~ r2_hidden(X0,k3_tarski(sk1))
| sk2 = k1_xboole_0 ),
inference(resolution,[status(thm)],[p220,c9]) ).
cnf(p223,plain,
( r2_hidden(sk6(X0,k3_tarski(sk1)),X0)
| k3_tarski(sk1) = k3_tarski(X0)
| sk2 = k1_xboole_0 ),
inference(resolution,[status(thm)],[p221,c16]) ).
cnf(p257,plain,
( sk2 = k1_xboole_0
| k3_tarski(sk1) = k3_tarski(k3_tarski(sk1))
| sk2 = k1_xboole_0 ),
inference(resolution,[status(thm)],[p223,p221]) ).
cnf(p288,plain,
( k3_tarski(sk1) = k3_tarski(k3_tarski(sk1))
| sk2 = k1_xboole_0 ),
inference(factoring,[status(thm)],[p257]) ).
cnf(p291,plain,
( k1_xboole_0 = k3_tarski(k3_tarski(sk1))
| sk2 = k1_xboole_0
| sk2 = k1_xboole_0 ),
inference(superposition,[status(thm)],[p220,p288]) ).
cnf(p293,plain,
( k1_xboole_0 = k3_tarski(k3_tarski(sk1))
| sk2 = k1_xboole_0 ),
inference(factoring,[status(thm)],[p291]) ).
cnf(p295,plain,
( k1_xboole_0 = k3_tarski(sk1)
| sk2 = k1_xboole_0
| sk2 = k1_xboole_0 ),
inference(superposition,[status(thm)],[p288,p293]) ).
cnf(p315,plain,
( k1_xboole_0 = k3_tarski(sk1)
| sk2 = k1_xboole_0 ),
inference(factoring,[status(thm)],[p295]) ).
cnf(c13,plain,
( ~ r2_hidden(X3,X0)
| ~ r2_hidden(X2,X3)
| r2_hidden(X2,X1)
| X1 != k3_tarski(X0) ),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(p316,plain,
( ~ r2_hidden(X1,sk1)
| ~ r2_hidden(X0,X1)
| r2_hidden(X0,k1_xboole_0)
| sk2 = k1_xboole_0 ),
inference(resolution,[status(thm)],[p315,c13]) ).
cnf(p371,plain,
( X0 = k1_xboole_0
| ~ r2_hidden(X0,sk1)
| r2_hidden(sk3(X0),k1_xboole_0)
| sk2 = k1_xboole_0 ),
inference(resolution,[status(thm)],[p316,c10]) ).
cnf(p566,plain,
( ~ r2_hidden(sk2,sk1)
| r2_hidden(sk3(sk2),k1_xboole_0)
| sk2 = k1_xboole_0 ),
inference(factoring,[status(thm)],[p371]) ).
cnf(p575,plain,
( r2_hidden(sk3(sk2),k1_xboole_0)
| sk2 = k1_xboole_0 ),
inference(resolution,[status(thm)],[p566,p204]) ).
cnf(p577,plain,
sk2 = k1_xboole_0,
inference(resolution,[status(thm)],[p575,p55]) ).
cnf(c6,plain,
( X2 = k1_xboole_0
| ~ r2_hidden(X2,sk1)
| sk2 != k1_xboole_0 ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p578,plain,
( X0 = k1_xboole_0
| ~ r2_hidden(X0,sk1)
| k1_xboole_0 != k1_xboole_0 ),
inference(demodulation,[status(thm)],[p577,c6]) ).
cnf(p608,plain,
( X0 = k1_xboole_0
| ~ r2_hidden(X0,sk1) ),
inference(equality_resolution,[status(thm)],[p578]) ).
cnf(p1001,plain,
( sk4(sk1,k3_tarski(sk1),sk3(k3_tarski(sk1))) = k1_xboole_0
| k3_tarski(sk1) = k1_xboole_0 ),
inference(resolution,[status(thm)],[p284,p608]) ).
cnf(p2076,plain,
( ~ r2_hidden(X0,sk4(sk1,k3_tarski(sk1),sk3(k3_tarski(sk1))))
| k3_tarski(sk1) = k1_xboole_0 ),
inference(resolution,[status(thm)],[p1001,c9]) ).
cnf(c11,plain,
( r2_hidden(X2,sk4(X0,X1,X2))
| ~ r2_hidden(X2,X1)
| X1 != k3_tarski(X0) ),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(p62,plain,
( r2_hidden(X0,sk4(X1,k3_tarski(X1),X0))
| ~ r2_hidden(X0,k3_tarski(X1)) ),
inference(equality_resolution,[status(thm)],[c11]) ).
cnf(p275,plain,
( k3_tarski(X0) = k1_xboole_0
| r2_hidden(sk3(k3_tarski(X0)),sk4(X0,k3_tarski(X0),sk3(k3_tarski(X0)))) ),
inference(resolution,[status(thm)],[p62,c10]) ).
cnf(p2362,plain,
( k3_tarski(sk1) = k1_xboole_0
| k3_tarski(sk1) = k1_xboole_0 ),
inference(resolution,[status(thm)],[p2076,p275]) ).
cnf(p2369,plain,
k3_tarski(sk1) = k1_xboole_0,
inference(factoring,[status(thm)],[p2362]) ).
cnf(c5,plain,
( k5_setfam_1(sk0,sk1) != k1_xboole_0
| sk2 != k1_xboole_0 ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p169,plain,
( k3_tarski(sk1) != k1_xboole_0
| sk2 != k1_xboole_0 ),
inference(demodulation,[status(thm)],[p166,c5]) ).
cnf(p579,plain,
( k3_tarski(sk1) != k1_xboole_0
| k1_xboole_0 != k1_xboole_0 ),
inference(demodulation,[status(thm)],[p577,p169]) ).
cnf(p601,plain,
k3_tarski(sk1) != k1_xboole_0,
inference(equality_resolution,[status(thm)],[p579]) ).
cnf(p2372,plain,
k1_xboole_0 != k1_xboole_0,
inference(demodulation,[status(thm)],[p2369,p601]) ).
cnf(p2392,plain,
$false,
inference(equality_resolution,[status(thm)],[p2372]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU430+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.10/0.37 % Computer : n016.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Thu Sep 24 14:16:42 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 7.71/1.45 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 7.71/1.45 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------