%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SEU146+2 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n010.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:05 PM UTC 2026
% Result : Theorem 45.55s 6.29s
% Output : Proof 45.55s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 8
% Syntax : Number of formulae : 59 ( 12 unt; 0 def)
% Number of atoms : 177 ( 80 equ)
% Maximal formula atoms : 10 ( 3 avg)
% Number of connectives : 177 ( 59 ~; 82 |; 27 &)
% ( 8 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 3 con; 0-2 aty)
% Number of variables : 74 ( 3 sgn 48 !; 5 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f10,axiom,
! [A,B] :
( subset(A,B)
<=> ! [C] :
( in(C,A)
=> in(C,B) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d3_tarski) ).
fof(f10_nnf,plain,
! [A,B] :
( ( ? [C] :
( ~ in(C,B)
& in(C,A) )
| subset(A,B) )
& ( ! [C] :
( in(C,B)
| ~ in(C,A) )
| ~ subset(A,B) ) ),
inference(nnf_transformation,[status(thm)],[f10]) ).
fof(f10_sk,plain,
! [A,B,C] :
( ( ( ~ in(sk4(A,B),B)
& in(sk4(A,B),A) )
| subset(A,B) )
& ( in(C,B)
| ~ in(C,A)
| ~ subset(A,B) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk4])],[f10_nnf]) ).
cnf(c34,plain,
( in(X2,X1)
| ~ in(X2,X0)
| ~ subset(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f10_sk]) ).
fof(f31,conjecture,
! [A,B] :
( subset(A,singleton(B))
<=> ( A = singleton(B)
| A = empty_set ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',l4_zfmisc_1) ).
fof(f31_neg,negated_conjecture,
~ ! [A,B] :
( subset(A,singleton(B))
<=> ( A = singleton(B)
| A = empty_set ) ),
inference(negated_conjecture,[status(cth)],[f31]) ).
fof(f31_nnf,plain,
? [A,B] :
( ( ( A = singleton(B)
| A = empty_set )
& ~ subset(A,singleton(B)) )
| ( A != singleton(B)
& A != empty_set
& subset(A,singleton(B)) ) ),
inference(nnf_transformation,[status(thm)],[f31_neg]) ).
fof(f31_sk,plain,
( ( ( sk7 = singleton(sk8)
| sk7 = empty_set )
& ~ subset(sk7,singleton(sk8)) )
| ( sk7 != singleton(sk8)
& sk7 != empty_set
& subset(sk7,singleton(sk8)) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk7,sk8])],[f31_nnf]) ).
cnf(c79,plain,
( sk7 = singleton(sk8)
| sk7 = empty_set
| subset(sk7,singleton(sk8)) ),
inference(cnf_transformation,[status(esa)],[f31_sk]) ).
cnf(p366,plain,
( sk7 = singleton(sk8)
| sk7 = empty_set
| in(X0,singleton(sk8))
| ~ in(X0,sk7) ),
inference(resolution,[status(thm)],[c34,c79]) ).
fof(f7,axiom,
! [A] :
( A = empty_set
<=> ! [B] : ~ in(B,A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d1_xboole_0) ).
fof(f7_nnf,plain,
! [A] :
( ( ? [B] : in(B,A)
| A = empty_set )
& ( ! [B] : ~ in(B,A)
| A != empty_set ) ),
inference(nnf_transformation,[status(thm)],[f7]) ).
fof(f7_sk,plain,
! [A,B] :
( ( in(sk1(A),A)
| A = empty_set )
& ( ~ in(B,A)
| A != empty_set ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk1])],[f7_nnf]) ).
cnf(c15,plain,
( in(sk1(X0),X0)
| X0 = empty_set ),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(p377,plain,
( sk7 = empty_set
| sk7 = singleton(sk8)
| sk7 = empty_set
| in(sk1(sk7),singleton(sk8)) ),
inference(resolution,[status(thm)],[p366,c15]) ).
cnf(p398,plain,
( sk7 = singleton(sk8)
| sk7 = empty_set
| in(sk1(sk7),singleton(sk8)) ),
inference(factoring,[status(thm)],[p377]) ).
fof(f6,axiom,
! [A,B] :
( B = singleton(A)
<=> ! [C] :
( in(C,B)
<=> C = A ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d1_tarski) ).
fof(f6_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)],[f6]) ).
fof(f6_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])],[f6_nnf]) ).
cnf(c8,plain,
( X2 = X0
| ~ in(X2,X1)
| X1 != singleton(X0) ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(p147,plain,
( X0 = X1
| ~ in(X0,singleton(X1)) ),
inference(equality_resolution,[status(thm)],[c8]) ).
cnf(p402,plain,
( sk1(sk7) = sk8
| sk7 = singleton(sk8)
| sk7 = empty_set ),
inference(resolution,[status(thm)],[p398,p147]) ).
cnf(p409,plain,
( in(sk8,sk7)
| sk7 = empty_set
| sk7 = singleton(sk8)
| sk7 = empty_set ),
inference(superposition,[status(thm)],[p402,c15]) ).
cnf(p576,plain,
( in(sk8,sk7)
| sk7 = singleton(sk8)
| sk7 = empty_set ),
inference(factoring,[status(thm)],[p409]) ).
fof(f28,lemma,
! [A,B] :
( subset(singleton(A),B)
<=> in(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',l2_zfmisc_1) ).
fof(f28_nnf,plain,
! [A,B] :
( ( ~ in(A,B)
| subset(singleton(A),B) )
& ( in(A,B)
| ~ subset(singleton(A),B) ) ),
inference(nnf_transformation,[status(thm)],[f28]) ).
fof(f28_sk,plain,
! [A,B] :
( ( ~ in(A,B)
| subset(singleton(A),B) )
& ( in(A,B)
| ~ subset(singleton(A),B) ) ),
inference(skolemisation,[status(esa)],[f28_nnf]) ).
cnf(c73,plain,
( in(X0,X1)
| ~ subset(singleton(X0),X1) ),
inference(cnf_transformation,[status(esa)],[f28_sk]) ).
fof(f34,axiom,
! [A,B] : subset(A,A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',reflexivity_r1_tarski) ).
fof(f34_nnf,plain,
! [A,B] : subset(A,A),
inference(nnf_transformation,[status(thm)],[f34]) ).
fof(f34_sk,plain,
! [A] : subset(A,A),
inference(skolemisation,[status(esa)],[f34_nnf]) ).
cnf(c86,plain,
subset(X0,X0),
inference(cnf_transformation,[status(esa)],[f34_sk]) ).
cnf(p178,plain,
in(X0,singleton(X0)),
inference(resolution,[status(thm)],[c73,c86]) ).
cnf(p589,plain,
( in(sk8,sk7)
| in(sk8,sk7)
| sk7 = empty_set ),
inference(superposition,[status(thm)],[p576,p178]) ).
cnf(p620,plain,
( in(sk8,sk7)
| sk7 = empty_set ),
inference(factoring,[status(thm)],[p589]) ).
cnf(c74,plain,
( ~ in(X0,X1)
| subset(singleton(X0),X1) ),
inference(cnf_transformation,[status(esa)],[f28_sk]) ).
cnf(p653,plain,
( subset(singleton(sk8),sk7)
| sk7 = empty_set ),
inference(resolution,[status(thm)],[p620,c74]) ).
fof(f5,axiom,
! [A,B] :
( A = B
<=> ( subset(B,A)
& subset(A,B) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d10_xboole_0) ).
fof(f5_nnf,plain,
! [A,B] :
( ( ~ subset(B,A)
| ~ subset(A,B)
| A = B )
& ( ( subset(B,A)
& subset(A,B) )
| A != B ) ),
inference(nnf_transformation,[status(thm)],[f5]) ).
fof(f5_sk,plain,
! [A,B] :
( ( ~ subset(B,A)
| ~ subset(A,B)
| A = B )
& ( ( subset(B,A)
& subset(A,B) )
| A != B ) ),
inference(skolemisation,[status(esa)],[f5_nnf]) ).
cnf(c7,plain,
( ~ subset(X1,X0)
| ~ subset(X0,X1)
| X0 = X1 ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p139,plain,
( sk7 = singleton(sk8)
| sk7 = empty_set
| ~ subset(singleton(sk8),sk7)
| sk7 = singleton(sk8) ),
inference(resolution,[status(thm)],[c7,c79]) ).
cnf(p145,plain,
( sk7 = empty_set
| ~ subset(singleton(sk8),sk7)
| sk7 = singleton(sk8) ),
inference(factoring,[status(thm)],[p139]) ).
cnf(p655,plain,
( sk7 = empty_set
| sk7 = singleton(sk8)
| sk7 = empty_set ),
inference(resolution,[status(thm)],[p653,p145]) ).
cnf(p686,plain,
( sk7 = singleton(sk8)
| sk7 = empty_set ),
inference(factoring,[status(thm)],[p655]) ).
cnf(c5,plain,
( subset(X0,X1)
| X0 != X1 ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p690,plain,
( subset(sk7,singleton(sk8))
| sk7 = empty_set ),
inference(resolution,[status(thm)],[p686,c5]) ).
cnf(c82,plain,
( ~ subset(sk7,singleton(sk8))
| sk7 != singleton(sk8) ),
inference(cnf_transformation,[status(esa)],[f31_sk]) ).
cnf(p689,plain,
( ~ subset(sk7,singleton(sk8))
| sk7 = empty_set ),
inference(resolution,[status(thm)],[p686,c82]) ).
cnf(p716,plain,
( sk7 = empty_set
| sk7 = empty_set ),
inference(resolution,[status(thm)],[p690,p689]) ).
cnf(p717,plain,
sk7 = empty_set,
inference(factoring,[status(thm)],[p716]) ).
cnf(c80,plain,
( ~ subset(sk7,singleton(sk8))
| sk7 != empty_set ),
inference(cnf_transformation,[status(esa)],[f31_sk]) ).
cnf(p718,plain,
( ~ subset(empty_set,singleton(sk8))
| empty_set != empty_set ),
inference(demodulation,[status(thm)],[p717,c80]) ).
cnf(p726,plain,
~ subset(empty_set,singleton(sk8)),
inference(equality_resolution,[status(thm)],[p718]) ).
fof(f45,lemma,
! [A] : subset(empty_set,A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t2_xboole_1) ).
fof(f45_nnf,plain,
! [A] : subset(empty_set,A),
inference(nnf_transformation,[status(thm)],[f45]) ).
fof(f45_sk,plain,
! [A] : subset(empty_set,A),
inference(skolemisation,[status(esa)],[f45_nnf]) ).
cnf(c100,plain,
subset(empty_set,X0),
inference(cnf_transformation,[status(esa)],[f45_sk]) ).
cnf(p727,plain,
$false,
inference(resolution,[status(thm)],[p726,c100]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU146+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.10/0.37 % Computer : n010.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 12:57:00 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 45.55/6.29 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 45.55/6.29 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------