%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SET679+3 : TPTP v9.3.1. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n026.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 : Sun Sep 27 08:36:48 AM UTC 2026
% Result : Theorem 0.14s 0.42s
% Output : CNFRefutation 0.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 7
% Syntax : Number of formulae : 39 ( 11 unt; 0 def)
% Number of atoms : 125 ( 14 equ)
% Maximal formula atoms : 10 ( 3 avg)
% Number of connectives : 150 ( 64 ~; 55 |; 13 &)
% ( 5 <=>; 13 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-2 aty)
% Number of functors : 6 ( 6 usr; 3 con; 0-2 aty)
% Number of variables : 60 ( 3 sgn 22 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(p2,axiom,
! [B] :
( ilf_type(B,set_type)
=> ~ member(B,empty_set) ),
file('theBenchmark.p',p2) ).
fof(p4,axiom,
! [B] :
( ilf_type(B,set_type)
=> ! [C] :
( ilf_type(C,set_type)
=> ! [D] :
( ilf_type(D,set_type)
=> ( member(ordered_pair(C,D),identity_relation_of(B))
<=> ( C = D
& member(C,B) ) ) ) ) ),
file('theBenchmark.p',p4) ).
fof(p6,axiom,
! [B] :
( ilf_type(B,set_type)
=> ! [C] :
( ilf_type(C,set_type)
=> ( B = C
<=> ! [D] :
( ilf_type(D,set_type)
=> ( member(D,B)
<=> member(D,C) ) ) ) ) ),
file('theBenchmark.p',p6) ).
fof(p7,axiom,
! [B] :
( ilf_type(B,set_type)
=> ! [C] :
( ilf_type(C,set_type)
=> ( not_equal(B,C)
<=> B != C ) ) ),
file('theBenchmark.p',p7) ).
fof(p8,axiom,
! [B] :
( ilf_type(B,set_type)
=> ( empty(B)
<=> ! [C] :
( ilf_type(C,set_type)
=> ~ member(C,B) ) ) ),
file('theBenchmark.p',p8) ).
fof(p22,axiom,
! [B] : ilf_type(B,set_type),
file('theBenchmark.p',p22) ).
fof(prove_relset_1_46,conjecture,
! [B] :
( ( ilf_type(B,set_type)
& ~ empty(B) )
=> not_equal(identity_relation_of(B),empty_set) ),
file('theBenchmark.p',prove_relset_1_46) ).
fof(prove_relset_1_46_neg,negated_conjecture,
~ ! [B] :
( ( ilf_type(B,set_type)
& ~ empty(B) )
=> not_equal(identity_relation_of(B),empty_set) ),
inference(assume_negation,[status(cth)],[prove_relset_1_46]) ).
cnf(c_71,plain,
( ~ member(A,empty_set)
| ~ ilf_type(A,set_type) ),
inference(clausify,[status(thm)],[p2]) ).
cnf(c_75,plain,
( C != B
| ~ member(B,A)
| member(ordered_pair(B,C),identity_relation_of(A))
| ~ ilf_type(C,set_type)
| ~ ilf_type(B,set_type)
| ~ ilf_type(A,set_type) ),
inference(clausify,[status(thm)],[p4]) ).
cnf(c_78,plain,
( ~ member(C,B)
| member(C,A)
| ~ ilf_type(C,set_type)
| B != A
| ~ ilf_type(B,set_type)
| ~ ilf_type(A,set_type) ),
inference(clausify,[status(thm)],[p6]) ).
cnf(c_83,plain,
( B = A
| not_equal(A,B)
| ~ ilf_type(B,set_type)
| ~ ilf_type(A,set_type) ),
inference(clausify,[status(thm)],[p7]) ).
fof(nnf_7,plain,
! [B] :
( ( ( ? [C] :
( member(C,B)
& ilf_type(C,set_type) )
| empty(B) )
& ( ! [X0] :
( ~ member(X0,B)
| ~ ilf_type(X0,set_type) )
| ~ empty(B) ) )
| ~ ilf_type(B,set_type) ),
inference(fof_nnf,[status(thm)],[p8]) ).
fof(sk_p8_sk,plain,
! [B] :
( ( ( ( member(sK0(B),B)
& ilf_type(sK0(B),set_type) )
| empty(B) )
& ( ! [X0] :
( ~ member(X0,B)
| ~ ilf_type(X0,set_type) )
| ~ empty(B) ) )
| ~ ilf_type(B,set_type) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(C,sK0(B))],[nnf_7]) ).
fof(sk_p8,plain,
( ! [VAR_0] :
( member(sK0(VAR_0),VAR_0)
| empty(VAR_0)
| ~ ilf_type(VAR_0,set_type) )
& ! [VAR_0] :
( ilf_type(sK0(VAR_0),set_type)
| empty(VAR_0)
| ~ ilf_type(VAR_0,set_type) )
& ! [VAR_0,VAR_1] :
( ~ member(VAR_1,VAR_0)
| ~ ilf_type(VAR_1,set_type)
| ~ empty(VAR_0)
| ~ ilf_type(VAR_0,set_type) ) ),
inference(cnf_transformation,[status(thm)],[sk_p8_sk]) ).
cnf(c_86,plain,
( member(sK0(A),A)
| empty(A)
| ~ ilf_type(A,set_type) ),
inference(split_conjunct,[status(thm)],[sk_p8]) ).
cnf(c_102,plain,
ilf_type(A,set_type),
inference(clausify,[status(thm)],[p22]) ).
fof(nnf_22,plain,
? [B] :
( ~ not_equal(identity_relation_of(B),empty_set)
& ilf_type(B,set_type)
& ~ empty(B) ),
inference(fof_nnf,[status(thm)],[prove_relset_1_46_neg]) ).
fof(sk_prove_relset_1_46_neg,plain,
( ~ not_equal(identity_relation_of(sK1),empty_set)
& ilf_type(sK1,set_type)
& ~ empty(sK1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(B,sK1)],[nnf_22]) ).
cnf(c_103,negated_conjecture,
~ empty(sK1),
inference(split_conjunct,[status(thm)],[sk_prove_relset_1_46_neg]) ).
cnf(c_104,negated_conjecture,
~ not_equal(identity_relation_of(sK1),empty_set),
inference(split_conjunct,[status(thm)],[sk_prove_relset_1_46_neg]) ).
cnf(c_324,plain,
( B != B
| ~ member(B,A)
| member(ordered_pair(B,B),identity_relation_of(A))
| ~ ilf_type(B,set_type)
| ~ ilf_type(A,set_type) ),
inference(factor,[status(thm)],[c_75]) ).
cnf(c_325,plain,
( ~ member(B,A)
| member(ordered_pair(B,B),identity_relation_of(A))
| ~ ilf_type(B,set_type)
| ~ ilf_type(A,set_type) ),
inference(copy,[status(thm)],[c_324]) ).
cnf(c_326,plain,
( ~ member(A,B)
| member(ordered_pair(A,A),identity_relation_of(B))
| ~ ilf_type(A,set_type) ),
inference(resolve,[status(thm)],[c_102,c_325]) ).
cnf(c_134,plain,
( ~ member(A,B)
| member(ordered_pair(A,A),identity_relation_of(B)) ),
inference(resolve,[status(thm)],[c_102,c_326]) ).
cnf(c_160,plain,
( member(sK0(A),A)
| empty(A) ),
inference(resolve,[status(thm)],[c_102,c_86]) ).
cnf(c_327,plain,
( A = B
| not_equal(B,A)
| ~ ilf_type(A,set_type) ),
inference(resolve,[status(thm)],[c_102,c_83]) ).
cnf(c_162,plain,
( B = A
| not_equal(A,B) ),
inference(resolve,[status(thm)],[c_102,c_327]) ).
cnf(c_328,plain,
( ~ member(C,A)
| member(C,B)
| ~ ilf_type(C,set_type)
| A != B
| ~ ilf_type(A,set_type) ),
inference(resolve,[status(thm)],[c_102,c_78]) ).
cnf(c_329,plain,
( ~ member(C,A)
| member(C,B)
| ~ ilf_type(C,set_type)
| A != B ),
inference(resolve,[status(thm)],[c_102,c_328]) ).
cnf(c_166,plain,
( ~ member(C,A)
| member(C,B)
| A != B ),
inference(resolve,[status(thm)],[c_102,c_329]) ).
cnf(c_172,plain,
~ member(A,empty_set),
inference(resolve,[status(thm)],[c_102,c_71]) ).
cnf(c_199,plain,
member(sK0(sK1),sK1),
inference(resolve,[status(thm)],[c_160,c_103]) ).
cnf(c_330,negated_conjecture,
empty_set = identity_relation_of(sK1),
inference(resolve,[status(thm)],[c_162,c_104]) ).
cnf(c_205,negated_conjecture,
identity_relation_of(sK1) = empty_set,
inference(copy,[status(thm)],[c_330]) ).
cnf(c_319,plain,
member(ordered_pair(sK0(sK1),sK0(sK1)),identity_relation_of(sK1)),
inference(resolve,[status(thm)],[c_199,c_134]) ).
cnf(c_331,plain,
( ~ member(A,identity_relation_of(sK1))
| member(A,empty_set) ),
inference(resolve,[status(thm)],[c_166,c_205]) ).
cnf(c_322,plain,
~ member(A,identity_relation_of(sK1)),
inference(resolve,[status(thm)],[c_331,c_172]) ).
cnf(c_323,plain,
$false,
inference(resolve,[status(thm)],[c_322,c_319]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SET679+3 : TPTP v9.3.1. Released v2.2.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.36 % Computer : n026.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Sat Sep 26 08:07:56 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.08/0.36 % Process 501268 was started by sandbox2 on n026,
% 0.08/0.36 % Sat Sep 26 08:07:56 2026
% 0.08/0.36 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.08/0.37
% 0.08/0.37 % From the command line: assign(max_seconds, 300).
% 0.14/0.42
% 0.14/0.42 % SZS status Theorem for theBenchmark
% 0.14/0.42
% 0.14/0.42 % Proof 1 at 0.02 (+ 0.02) seconds.
% 0.14/0.42 % Length of proof is 25.
% 0.14/0.42 % Level of proof is 5.
% 0.14/0.42 % Maximum clause weight is 31.000.
% 0.14/0.42 % Given clauses 50.
% 0.14/0.42
% 0.14/0.42 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------