%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SET901+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:15 PM UTC 2026
% Result : Theorem 4.33s 1.21s
% Output : Proof 4.33s
% Verified :
% SZS Type : Refutation
% Derivation depth : 24
% Number of leaves : 2
% Syntax : Number of formulae : 41 ( 4 unt; 0 def)
% Number of atoms : 164 ( 133 equ)
% Maximal formula atoms : 10 ( 4 avg)
% Number of connectives : 178 ( 55 ~; 93 |; 27 &)
% ( 3 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 5 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 6 ( 6 usr; 4 con; 0-2 aty)
% Number of variables : 37 ( 8 sgn 15 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f6,axiom,
! [A,B,C] :
( subset(A,unordered_pair(B,C))
<=> ~ ( A != unordered_pair(B,C)
& A != singleton(C)
& A != singleton(B)
& A != empty_set ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',l46_zfmisc_1) ).
fof(f6_nnf,plain,
! [A,B,C] :
( ( ( A != unordered_pair(B,C)
& A != singleton(C)
& A != singleton(B)
& A != empty_set )
| subset(A,unordered_pair(B,C)) )
& ( A = unordered_pair(B,C)
| A = singleton(C)
| A = singleton(B)
| A = empty_set
| ~ subset(A,unordered_pair(B,C)) ) ),
inference(nnf_transformation,[status(thm)],[f6]) ).
fof(f6_sk,plain,
! [A,B,C] :
( ( ( A != unordered_pair(B,C)
& A != singleton(C)
& A != singleton(B)
& A != empty_set )
| subset(A,unordered_pair(B,C)) )
& ( A = unordered_pair(B,C)
| A = singleton(C)
| A = singleton(B)
| A = empty_set
| ~ subset(A,unordered_pair(B,C)) ) ),
inference(skolemisation,[status(esa)],[f6_nnf]) ).
cnf(c15,plain,
( X0 = unordered_pair(X1,X2)
| X0 = singleton(X2)
| X0 = singleton(X1)
| X0 = empty_set
| ~ subset(X0,unordered_pair(X1,X2)) ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
fof(f5,conjecture,
! [A,B,C] :
( subset(A,unordered_pair(B,C))
<=> ~ ( A != unordered_pair(B,C)
& A != singleton(C)
& A != singleton(B)
& A != empty_set ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t42_zfmisc_1) ).
fof(f5_neg,negated_conjecture,
~ ! [A,B,C] :
( subset(A,unordered_pair(B,C))
<=> ~ ( A != unordered_pair(B,C)
& A != singleton(C)
& A != singleton(B)
& A != empty_set ) ),
inference(negated_conjecture,[status(cth)],[f5]) ).
fof(f5_nnf,plain,
? [A,B,C] :
( ( ( A = unordered_pair(B,C)
| A = singleton(C)
| A = singleton(B)
| A = empty_set )
& ~ subset(A,unordered_pair(B,C)) )
| ( A != unordered_pair(B,C)
& A != singleton(C)
& A != singleton(B)
& A != empty_set
& subset(A,unordered_pair(B,C)) ) ),
inference(nnf_transformation,[status(thm)],[f5_neg]) ).
fof(f5_sk,plain,
( ( ( sk2 = unordered_pair(sk3,sk4)
| sk2 = singleton(sk4)
| sk2 = singleton(sk3)
| sk2 = empty_set )
& ~ subset(sk2,unordered_pair(sk3,sk4)) )
| ( sk2 != unordered_pair(sk3,sk4)
& sk2 != singleton(sk4)
& sk2 != singleton(sk3)
& sk2 != empty_set
& subset(sk2,unordered_pair(sk3,sk4)) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk2,sk3,sk4])],[f5_nnf]) ).
cnf(c6,plain,
( sk2 = unordered_pair(sk3,sk4)
| sk2 = singleton(sk4)
| sk2 = singleton(sk3)
| sk2 = empty_set
| subset(sk2,unordered_pair(sk3,sk4)) ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p108,plain,
( sk2 = unordered_pair(sk3,sk4)
| sk2 = singleton(sk4)
| sk2 = singleton(sk3)
| sk2 = empty_set
| sk2 = unordered_pair(sk3,sk4)
| sk2 = singleton(sk4)
| sk2 = singleton(sk3)
| sk2 = empty_set ),
inference(resolution,[status(thm)],[c15,c6]) ).
cnf(p410,plain,
( sk2 = singleton(sk4)
| sk2 = singleton(sk3)
| sk2 = empty_set
| sk2 = unordered_pair(sk3,sk4)
| sk2 = singleton(sk4)
| sk2 = singleton(sk3)
| sk2 = empty_set ),
inference(factoring,[status(thm)],[p108]) ).
cnf(p475,plain,
( sk2 = singleton(sk4)
| sk2 = empty_set
| sk2 = unordered_pair(sk3,sk4)
| sk2 = singleton(sk4)
| sk2 = singleton(sk3)
| sk2 = empty_set ),
inference(factoring,[status(thm)],[p410]) ).
cnf(p483,plain,
( sk2 = empty_set
| sk2 = unordered_pair(sk3,sk4)
| sk2 = singleton(sk4)
| sk2 = singleton(sk3)
| sk2 = empty_set ),
inference(factoring,[status(thm)],[p475]) ).
cnf(p484,plain,
( sk2 = unordered_pair(sk3,sk4)
| sk2 = singleton(sk4)
| sk2 = singleton(sk3)
| sk2 = empty_set ),
inference(factoring,[status(thm)],[p483]) ).
cnf(c19,plain,
( X0 != unordered_pair(X1,X2)
| subset(X0,unordered_pair(X1,X2)) ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(p501,plain,
( subset(sk2,unordered_pair(sk3,sk4))
| sk2 = singleton(sk4)
| sk2 = singleton(sk3)
| sk2 = empty_set ),
inference(resolution,[status(thm)],[p484,c19]) ).
cnf(c13,plain,
( ~ subset(sk2,unordered_pair(sk3,sk4))
| sk2 != unordered_pair(sk3,sk4) ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p499,plain,
( ~ subset(sk2,unordered_pair(sk3,sk4))
| sk2 = singleton(sk4)
| sk2 = singleton(sk3)
| sk2 = empty_set ),
inference(resolution,[status(thm)],[p484,c13]) ).
cnf(p657,plain,
( sk2 = singleton(sk4)
| sk2 = singleton(sk3)
| sk2 = empty_set
| sk2 = singleton(sk4)
| sk2 = singleton(sk3)
| sk2 = empty_set ),
inference(resolution,[status(thm)],[p501,p499]) ).
cnf(p1281,plain,
( sk2 = singleton(sk4)
| sk2 = empty_set
| sk2 = singleton(sk4)
| sk2 = singleton(sk3)
| sk2 = empty_set ),
inference(factoring,[status(thm)],[p657]) ).
cnf(p1284,plain,
( sk2 = empty_set
| sk2 = singleton(sk4)
| sk2 = singleton(sk3)
| sk2 = empty_set ),
inference(factoring,[status(thm)],[p1281]) ).
cnf(p1285,plain,
( sk2 = singleton(sk4)
| sk2 = singleton(sk3)
| sk2 = empty_set ),
inference(factoring,[status(thm)],[p1284]) ).
cnf(c18,plain,
( X0 != singleton(X2)
| subset(X0,unordered_pair(X1,X2)) ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(p1295,plain,
( subset(sk2,unordered_pair(X0,sk4))
| sk2 = singleton(sk3)
| sk2 = empty_set ),
inference(resolution,[status(thm)],[p1285,c18]) ).
cnf(c11,plain,
( ~ subset(sk2,unordered_pair(sk3,sk4))
| sk2 != singleton(sk4) ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p1292,plain,
( ~ subset(sk2,unordered_pair(sk3,sk4))
| sk2 = singleton(sk3)
| sk2 = empty_set ),
inference(resolution,[status(thm)],[p1285,c11]) ).
cnf(p1394,plain,
( sk2 = singleton(sk3)
| sk2 = empty_set
| sk2 = singleton(sk3)
| sk2 = empty_set ),
inference(resolution,[status(thm)],[p1295,p1292]) ).
cnf(p1407,plain,
( sk2 = empty_set
| sk2 = singleton(sk3)
| sk2 = empty_set ),
inference(factoring,[status(thm)],[p1394]) ).
cnf(p1408,plain,
( sk2 = singleton(sk3)
| sk2 = empty_set ),
inference(factoring,[status(thm)],[p1407]) ).
cnf(c17,plain,
( X0 != singleton(X1)
| subset(X0,unordered_pair(X1,X2)) ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(p1412,plain,
( subset(sk2,unordered_pair(sk3,X0))
| sk2 = empty_set ),
inference(resolution,[status(thm)],[p1408,c17]) ).
cnf(c9,plain,
( ~ subset(sk2,unordered_pair(sk3,sk4))
| sk2 != singleton(sk3) ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p1411,plain,
( ~ subset(sk2,unordered_pair(sk3,sk4))
| sk2 = empty_set ),
inference(resolution,[status(thm)],[p1408,c9]) ).
cnf(p1477,plain,
( sk2 = empty_set
| sk2 = empty_set ),
inference(resolution,[status(thm)],[p1412,p1411]) ).
cnf(p1478,plain,
sk2 = empty_set,
inference(factoring,[status(thm)],[p1477]) ).
cnf(c7,plain,
( ~ subset(sk2,unordered_pair(sk3,sk4))
| sk2 != empty_set ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p1479,plain,
( ~ subset(empty_set,unordered_pair(sk3,sk4))
| empty_set != empty_set ),
inference(demodulation,[status(thm)],[p1478,c7]) ).
cnf(p1517,plain,
~ subset(empty_set,unordered_pair(sk3,sk4)),
inference(equality_resolution,[status(thm)],[p1479]) ).
cnf(c16,plain,
( X0 != empty_set
| subset(X0,unordered_pair(X1,X2)) ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(p115,plain,
subset(empty_set,unordered_pair(X0,X1)),
inference(equality_resolution,[status(thm)],[c16]) ).
cnf(p1520,plain,
$false,
inference(resolution,[status(thm)],[p1517,p115]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SET901+1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.10/0.36 % Computer : n014.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Thu Sep 24 12:21:03 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 4.33/1.21 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 4.33/1.21 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------