%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SET988+1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n001.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:25 PM UTC 2026
% Result : Theorem 3.61s 0.95s
% Output : Proof 3.61s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 3
% Syntax : Number of formulae : 29 ( 4 unt; 0 def)
% Number of atoms : 101 ( 27 equ)
% Maximal formula atoms : 8 ( 3 avg)
% Number of connectives : 113 ( 41 ~; 41 |; 24 &)
% ( 2 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 1 con; 0-2 aty)
% Number of variables : 67 ( 2 sgn 45 !; 9 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f30,conjecture,
! [A] :
( ( ! [B,C,D] :
( ( in(ordered_pair(B,D),A)
& in(ordered_pair(B,C),A) )
=> C = D )
& ! [B] :
~ ( ! [C,D] : ordered_pair(C,D) != B
& in(B,A) ) )
=> ( function(A)
& relation(A) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t2_funct_1) ).
fof(f30_neg,negated_conjecture,
~ ! [A] :
( ( ! [B,C,D] :
( ( in(ordered_pair(B,D),A)
& in(ordered_pair(B,C),A) )
=> C = D )
& ! [B] :
~ ( ! [C,D] : ordered_pair(C,D) != B
& in(B,A) ) )
=> ( function(A)
& relation(A) ) ),
inference(negated_conjecture,[status(cth)],[f30]) ).
fof(f30_nnf,plain,
? [A] :
( ( ~ function(A)
| ~ relation(A) )
& ! [B,C,D] :
( C = D
| ~ in(ordered_pair(B,D),A)
| ~ in(ordered_pair(B,C),A) )
& ! [B] :
( ? [C,D] : ordered_pair(C,D) = B
| ~ in(B,A) ) ),
inference(nnf_transformation,[status(thm)],[f30_neg]) ).
fof(f30_sk,plain,
! [B,C,D] :
( ( ~ function(sk9)
| ~ relation(sk9) )
& ( C = D
| ~ in(ordered_pair(B,D),sk9)
| ~ in(ordered_pair(B,C),sk9) )
& ( ordered_pair(sk10(B),sk11(B)) = B
| ~ in(B,sk9) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk9,sk10,sk11])],[f30_nnf]) ).
cnf(c41,plain,
( X2 = X3
| ~ in(ordered_pair(X1,X3),sk9)
| ~ in(ordered_pair(X1,X2),sk9) ),
inference(cnf_transformation,[status(esa)],[f30_sk]) ).
fof(f31,axiom,
! [A] :
( function(A)
<=> ! [B,C,D] :
( ( in(ordered_pair(B,D),A)
& in(ordered_pair(B,C),A) )
=> C = D ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d1_funct_1) ).
fof(f31_nnf,plain,
! [A] :
( ( ? [B,C,D] :
( C != D
& in(ordered_pair(B,D),A)
& in(ordered_pair(B,C),A) )
| function(A) )
& ( ! [B,C,D] :
( C = D
| ~ in(ordered_pair(B,D),A)
| ~ in(ordered_pair(B,C),A) )
| ~ function(A) ) ),
inference(nnf_transformation,[status(thm)],[f31]) ).
fof(f31_sk,plain,
! [A,B,C,D] :
( ( ( sk13(A) != sk14(A)
& in(ordered_pair(sk12(A),sk14(A)),A)
& in(ordered_pair(sk12(A),sk13(A)),A) )
| function(A) )
& ( C = D
| ~ in(ordered_pair(B,D),A)
| ~ in(ordered_pair(B,C),A)
| ~ function(A) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk12,sk13,sk14])],[f31_nnf]) ).
cnf(c44,plain,
( in(ordered_pair(sk12(X0),sk13(X0)),X0)
| function(X0) ),
inference(cnf_transformation,[status(esa)],[f31_sk]) ).
cnf(p101,plain,
( function(sk9)
| sk13(sk9) = X0
| ~ in(ordered_pair(sk12(sk9),X0),sk9) ),
inference(resolution,[status(thm)],[c41,c44]) ).
cnf(c45,plain,
( in(ordered_pair(sk12(X0),sk14(X0)),X0)
| function(X0) ),
inference(cnf_transformation,[status(esa)],[f31_sk]) ).
cnf(p270,plain,
( function(sk9)
| function(sk9)
| sk13(sk9) = sk14(sk9) ),
inference(resolution,[status(thm)],[p101,c45]) ).
cnf(p272,plain,
( function(sk9)
| sk13(sk9) = sk14(sk9) ),
inference(factoring,[status(thm)],[p270]) ).
cnf(c46,plain,
( sk13(X0) != sk14(X0)
| function(X0) ),
inference(cnf_transformation,[status(esa)],[f31_sk]) ).
cnf(p273,plain,
( function(sk9)
| function(sk9) ),
inference(resolution,[status(thm)],[p272,c46]) ).
cnf(p274,plain,
function(sk9),
inference(factoring,[status(thm)],[p273]) ).
cnf(c40,plain,
( ordered_pair(sk10(X1),sk11(X1)) = X1
| ~ in(X1,sk9) ),
inference(cnf_transformation,[status(esa)],[f30_sk]) ).
fof(f32,axiom,
! [A] :
( relation(A)
<=> ! [B] :
~ ( ! [C,D] : B != ordered_pair(C,D)
& in(B,A) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d1_relat_1) ).
fof(f32_nnf,plain,
! [A] :
( ( ? [B] :
( ! [C,D] : B != ordered_pair(C,D)
& in(B,A) )
| relation(A) )
& ( ! [B] :
( ? [C,D] : B = ordered_pair(C,D)
| ~ in(B,A) )
| ~ relation(A) ) ),
inference(nnf_transformation,[status(thm)],[f32]) ).
fof(f32_sk,plain,
! [A,B,C,D] :
( ( ( sk17(A) != ordered_pair(C,D)
& in(sk17(A),A) )
| relation(A) )
& ( B = ordered_pair(sk15(A,B),sk16(A,B))
| ~ in(B,A)
| ~ relation(A) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk15,sk16,sk17])],[f32_nnf]) ).
cnf(c48,plain,
( in(sk17(X0),X0)
| relation(X0) ),
inference(cnf_transformation,[status(esa)],[f32_sk]) ).
cnf(p87,plain,
( relation(sk9)
| ordered_pair(sk10(sk17(sk9)),sk11(sk17(sk9))) = sk17(sk9) ),
inference(resolution,[status(thm)],[c40,c48]) ).
cnf(c49,plain,
( sk17(X0) != ordered_pair(X2,X3)
| relation(X0) ),
inference(cnf_transformation,[status(esa)],[f32_sk]) ).
cnf(p209,plain,
( sk17(X0) != sk17(sk9)
| relation(X0)
| relation(sk9) ),
inference(superposition,[status(thm)],[p87,c49]) ).
cnf(p212,plain,
( relation(sk9)
| relation(sk9) ),
inference(equality_resolution,[status(thm)],[p209]) ).
cnf(p214,plain,
relation(sk9),
inference(factoring,[status(thm)],[p212]) ).
cnf(c42,plain,
( ~ function(sk9)
| ~ relation(sk9) ),
inference(cnf_transformation,[status(esa)],[f30_sk]) ).
cnf(p215,plain,
~ function(sk9),
inference(resolution,[status(thm)],[p214,c42]) ).
cnf(p278,plain,
$false,
inference(resolution,[status(thm)],[p274,p215]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SET988+1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.10/0.37 % Computer : n001.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:37:09 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 3.61/0.95 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 3.61/0.95 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------