%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SET959+1 : TPTP v9.3.1. Bugfixed v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n002.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:22 PM UTC 2026
% Result : Theorem 6.13s 1.28s
% Output : Proof 6.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 2
% Syntax : Number of formulae : 34 ( 3 unt; 0 def)
% Number of atoms : 117 ( 50 equ)
% Maximal formula atoms : 9 ( 3 avg)
% Number of connectives : 117 ( 34 ~; 57 |; 20 &)
% ( 3 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 2 con; 0-2 aty)
% Number of variables : 57 ( 0 sgn 33 !; 7 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f7,axiom,
! [A,B] :
( ! [C] :
( in(C,A)
<=> in(C,B) )
=> A = B ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t2_tarski) ).
fof(f7_nnf,plain,
! [A,B] :
( A = B
| ? [C] :
( ( in(C,B)
& ~ in(C,A) )
| ( ~ in(C,B)
& in(C,A) ) ) ),
inference(nnf_transformation,[status(thm)],[f7]) ).
fof(f7_sk,plain,
! [A,B] :
( A = B
| ( in(sk8(A,B),B)
& ~ in(sk8(A,B),A) )
| ( ~ in(sk8(A,B),B)
& in(sk8(A,B),A) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk8])],[f7_nnf]) ).
cnf(c12,plain,
( X0 = X1
| in(sk8(X0,X1),X1)
| in(sk8(X0,X1),X0) ),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
fof(f6,conjecture,
! [A,B] :
( ( ! [C,D] :
( in(ordered_pair(C,D),A)
<=> in(ordered_pair(C,D),B) )
& ! [C] :
~ ( ! [D,E] : C != ordered_pair(D,E)
& in(C,B) )
& ! [C] :
~ ( ! [D,E] : C != ordered_pair(D,E)
& in(C,A) ) )
=> A = B ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t112_zfmisc_1) ).
fof(f6_neg,negated_conjecture,
~ ! [A,B] :
( ( ! [C,D] :
( in(ordered_pair(C,D),A)
<=> in(ordered_pair(C,D),B) )
& ! [C] :
~ ( ! [D,E] : C != ordered_pair(D,E)
& in(C,B) )
& ! [C] :
~ ( ! [D,E] : C != ordered_pair(D,E)
& in(C,A) ) )
=> A = B ),
inference(negated_conjecture,[status(cth)],[f6]) ).
fof(f6_nnf,plain,
? [A,B] :
( A != B
& ! [C,D] :
( ( ~ in(ordered_pair(C,D),B)
| in(ordered_pair(C,D),A) )
& ( in(ordered_pair(C,D),B)
| ~ in(ordered_pair(C,D),A) ) )
& ! [C] :
( ? [D,E] : C = ordered_pair(D,E)
| ~ in(C,B) )
& ! [C] :
( ? [D,E] : C = ordered_pair(D,E)
| ~ in(C,A) ) ),
inference(nnf_transformation,[status(thm)],[f6_neg]) ).
fof(f6_sk,plain,
! [C,D] :
( sk2 != sk3
& ( ~ in(ordered_pair(C,D),sk3)
| in(ordered_pair(C,D),sk2) )
& ( in(ordered_pair(C,D),sk3)
| ~ in(ordered_pair(C,D),sk2) )
& ( C = ordered_pair(sk6(C),sk7(C))
| ~ in(C,sk3) )
& ( C = ordered_pair(sk4(C),sk5(C))
| ~ in(C,sk2) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk2,sk3,sk4,sk5,sk6,sk7])],[f6_nnf]) ).
cnf(c6,plain,
( X2 = ordered_pair(sk4(X2),sk5(X2))
| ~ in(X2,sk2) ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(p39,plain,
( sk8(sk2,X0) = ordered_pair(sk4(sk8(sk2,X0)),sk5(sk8(sk2,X0)))
| sk2 = X0
| in(sk8(sk2,X0),X0) ),
inference(resolution,[status(thm)],[c12,c6]) ).
cnf(c8,plain,
( in(ordered_pair(X2,X3),sk3)
| ~ in(ordered_pair(X2,X3),sk2) ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(p45,plain,
( in(ordered_pair(sk4(sk8(sk2,X0)),sk5(sk8(sk2,X0))),sk3)
| ~ in(sk8(sk2,X0),sk2)
| sk2 = X0
| in(sk8(sk2,X0),X0) ),
inference(superposition,[status(thm)],[p39,c8]) ).
cnf(p81,plain,
( sk2 = X0
| in(sk8(sk2,X0),X0)
| in(ordered_pair(sk4(sk8(sk2,X0)),sk5(sk8(sk2,X0))),sk3)
| sk2 = X0
| in(sk8(sk2,X0),X0) ),
inference(resolution,[status(thm)],[p45,c12]) ).
cnf(p238,plain,
( sk2 = X0
| in(ordered_pair(sk4(sk8(sk2,X0)),sk5(sk8(sk2,X0))),sk3)
| sk2 = X0
| in(sk8(sk2,X0),X0) ),
inference(factoring,[status(thm)],[p81]) ).
cnf(p240,plain,
( in(ordered_pair(sk4(sk8(sk2,X0)),sk5(sk8(sk2,X0))),sk3)
| sk2 = X0
| in(sk8(sk2,X0),X0) ),
inference(factoring,[status(thm)],[p238]) ).
cnf(p244,plain,
( in(sk8(sk2,X0),sk3)
| sk2 = X0
| in(sk8(sk2,X0),X0)
| sk2 = X0
| in(sk8(sk2,X0),X0) ),
inference(superposition,[status(thm)],[p39,p240]) ).
cnf(p279,plain,
( in(sk8(sk2,X0),sk3)
| sk2 = X0
| sk2 = X0
| in(sk8(sk2,X0),X0) ),
inference(factoring,[status(thm)],[p244]) ).
cnf(p281,plain,
( sk2 = sk3
| sk2 = sk3
| in(sk8(sk2,sk3),sk3) ),
inference(factoring,[status(thm)],[p279]) ).
cnf(p283,plain,
( sk2 = sk3
| in(sk8(sk2,sk3),sk3) ),
inference(factoring,[status(thm)],[p281]) ).
cnf(c7,plain,
( X2 = ordered_pair(sk6(X2),sk7(X2))
| ~ in(X2,sk3) ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(p284,plain,
( sk8(sk2,sk3) = ordered_pair(sk6(sk8(sk2,sk3)),sk7(sk8(sk2,sk3)))
| sk2 = sk3 ),
inference(resolution,[status(thm)],[p283,c7]) ).
cnf(c9,plain,
( ~ in(ordered_pair(X2,X3),sk3)
| in(ordered_pair(X2,X3),sk2) ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(p332,plain,
( ~ in(sk8(sk2,sk3),sk3)
| in(ordered_pair(sk6(sk8(sk2,sk3)),sk7(sk8(sk2,sk3))),sk2)
| sk2 = sk3 ),
inference(superposition,[status(thm)],[p284,c9]) ).
cnf(p391,plain,
( sk2 = sk3
| in(ordered_pair(sk6(sk8(sk2,sk3)),sk7(sk8(sk2,sk3))),sk2)
| sk2 = sk3 ),
inference(resolution,[status(thm)],[p332,p283]) ).
cnf(p392,plain,
( in(ordered_pair(sk6(sk8(sk2,sk3)),sk7(sk8(sk2,sk3))),sk2)
| sk2 = sk3 ),
inference(factoring,[status(thm)],[p391]) ).
cnf(p397,plain,
( in(sk8(sk2,sk3),sk2)
| sk2 = sk3
| sk2 = sk3 ),
inference(superposition,[status(thm)],[p284,p392]) ).
cnf(p398,plain,
( in(sk8(sk2,sk3),sk2)
| sk2 = sk3 ),
inference(factoring,[status(thm)],[p397]) ).
cnf(c13,plain,
( X0 = X1
| ~ in(sk8(X0,X1),X0)
| ~ in(sk8(X0,X1),X1) ),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(p286,plain,
( sk2 = sk3
| ~ in(sk8(sk2,sk3),sk2)
| sk2 = sk3 ),
inference(resolution,[status(thm)],[p283,c13]) ).
cnf(p305,plain,
( ~ in(sk8(sk2,sk3),sk2)
| sk2 = sk3 ),
inference(factoring,[status(thm)],[p286]) ).
cnf(p423,plain,
( sk2 = sk3
| sk2 = sk3 ),
inference(resolution,[status(thm)],[p398,p305]) ).
cnf(p424,plain,
sk2 = sk3,
inference(factoring,[status(thm)],[p423]) ).
cnf(c10,plain,
sk2 != sk3,
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(p425,plain,
$false,
inference(resolution,[status(thm)],[p424,c10]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SET959+1 : TPTP v9.3.1. Bugfixed v4.0.0.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.08/0.35 % Computer : n002.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Thu Sep 24 12:29:33 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.35 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 6.13/1.28 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 6.13/1.28 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------