%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SEU149+2 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n013.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:45:11 AM UTC 2026
% Result : Theorem 0.14s 0.84s
% Output : CNFRefutation 0.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 24
% Number of leaves : 8
% Syntax : Number of formulae : 57 ( 23 unt; 0 def)
% Number of atoms : 111 ( 84 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 79 ( 25 ~; 42 |; 5 &)
% ( 4 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 4 con; 0-2 aty)
% Number of variables : 73 ( 5 sgn 27 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(commutativity_k2_tarski,axiom,
! [A,B] : unordered_pair(A,B) = unordered_pair(B,A),
file('theBenchmark.p',commutativity_k2_tarski) ).
fof(d1_xboole_0,axiom,
! [A] :
( A = empty_set
<=> ! [B] : ~ in(B,A) ),
file('theBenchmark.p',d1_xboole_0) ).
fof(d2_tarski,axiom,
! [A,B,C] :
( C = unordered_pair(A,B)
<=> ! [D] :
( in(D,C)
<=> ( D = B
| D = A ) ) ),
file('theBenchmark.p',d2_tarski) ).
fof(l1_zfmisc_1,axiom,
! [A] : singleton(A) != empty_set,
file('theBenchmark.p',l1_zfmisc_1) ).
fof(l2_zfmisc_1,axiom,
! [A,B] :
( subset(singleton(A),B)
<=> in(A,B) ),
file('theBenchmark.p',l2_zfmisc_1) ).
fof(t69_enumset1,axiom,
! [A] : unordered_pair(A,A) = singleton(A),
file('theBenchmark.p',t69_enumset1) ).
fof(t6_zfmisc_1,axiom,
! [A,B] :
( subset(singleton(A),singleton(B))
=> A = B ),
file('theBenchmark.p',t6_zfmisc_1) ).
fof(t8_zfmisc_1,conjecture,
! [A,B,C] :
( singleton(A) = unordered_pair(B,C)
=> A = B ),
file('theBenchmark.p',t8_zfmisc_1) ).
fof(t8_zfmisc_1_neg,negated_conjecture,
~ ! [A,B,C] :
( singleton(A) = unordered_pair(B,C)
=> A = B ),
inference(assume_negation,[status(cth)],[t8_zfmisc_1]) ).
cnf(c_73,plain,
unordered_pair(A,B) = unordered_pair(B,A),
inference(clausify,[status(thm)],[commutativity_k2_tarski]) ).
fof(nnf_8,plain,
! [A] :
( ( ? [B] : in(B,A)
| empty_set = A )
& ( ! [X0] : ~ in(X0,A)
| empty_set != A ) ),
inference(fof_nnf,[status(thm)],[d1_xboole_0]) ).
fof(sk_d1_xboole_0_sk,plain,
! [A] :
( ( in(sK0(A),A)
| empty_set = A )
& ( ! [X0] : ~ in(X0,A)
| empty_set != A ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(B,sK0(A))],[nnf_8]) ).
fof(sk_d1_xboole_0,plain,
( ! [VAR_0] :
( in(sK0(VAR_0),VAR_0)
| empty_set = VAR_0 )
& ! [VAR_0,VAR_1] :
( ~ in(VAR_1,VAR_0)
| empty_set != VAR_0 ) ),
inference(cnf_transformation,[status(thm)],[sk_d1_xboole_0_sk]) ).
cnf(c_84,plain,
( in(sK0(A),A)
| empty_set = A ),
inference(split_conjunct,[status(thm)],[sk_d1_xboole_0]) ).
cnf(c_89,plain,
( D = B
| D = A
| ~ in(D,C)
| unordered_pair(A,B) != C ),
inference(clausify,[status(thm)],[d2_tarski]) ).
cnf(c_90,plain,
( D != A
| in(D,C)
| unordered_pair(A,B) != C ),
inference(clausify,[status(thm)],[d2_tarski]) ).
cnf(c_127,plain,
singleton(A) != empty_set,
inference(clausify,[status(thm)],[l1_zfmisc_1]) ).
cnf(c_129,plain,
( ~ in(A,B)
| subset(singleton(A),B) ),
inference(clausify,[status(thm)],[l2_zfmisc_1]) ).
cnf(c_170,plain,
singleton(A) = unordered_pair(A,A),
inference(clausify,[status(thm)],[t69_enumset1]) ).
cnf(c_172,plain,
( B = A
| ~ subset(singleton(A),singleton(B)) ),
inference(clausify,[status(thm)],[t6_zfmisc_1]) ).
cnf(c_1653,plain,
( B = A
| ~ subset(unordered_pair(A,A),singleton(B)) ),
inference(paramod,[status(thm)],[c_170,c_172]) ).
cnf(c_173,plain,
( B = A
| ~ subset(unordered_pair(A,A),unordered_pair(B,B)) ),
inference(paramod,[status(thm)],[c_170,c_1653]) ).
fof(nnf_70,plain,
? [A,B,C] :
( B != A
& singleton(A) = unordered_pair(B,C) ),
inference(fof_nnf,[status(thm)],[t8_zfmisc_1_neg]) ).
fof(sk_t8_zfmisc_1_neg,plain,
( sK2 != sK1
& singleton(sK1) = unordered_pair(sK2,sK3) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1,sK2,sK3]),skolemize(A,sK1),skolemize(B,sK2),skolemize(C,sK3)],[nnf_70]) ).
cnf(c_180,negated_conjecture,
singleton(sK1) = unordered_pair(sK2,sK3),
inference(split_conjunct,[status(thm)],[sk_t8_zfmisc_1_neg]) ).
cnf(c_1654,negated_conjecture,
unordered_pair(sK1,sK1) = unordered_pair(sK2,sK3),
inference(paramod,[status(thm)],[c_170,c_180]) ).
cnf(c_181,negated_conjecture,
unordered_pair(sK2,sK3) = unordered_pair(sK1,sK1),
inference(copy,[status(thm)],[c_1654]) ).
cnf(c_182,negated_conjecture,
sK2 != sK1,
inference(split_conjunct,[status(thm)],[sk_t8_zfmisc_1_neg]) ).
cnf(c_222,plain,
( ~ in(A,B)
| subset(unordered_pair(A,A),B) ),
inference(paramod,[status(thm)],[c_170,c_129]) ).
cnf(c_224,plain,
unordered_pair(A,A) != empty_set,
inference(paramod,[status(thm)],[c_170,c_127]) ).
cnf(c_233,plain,
( empty_set = C
| sK0(C) = B
| sK0(C) = A
| unordered_pair(A,B) != C ),
inference(resolve,[status(thm)],[c_89,c_84]) ).
cnf(c_235,plain,
( A != C
| in(A,unordered_pair(B,C)) ),
inference(resolve,[status(thm)],[c_90,c_73]) ).
cnf(c_1655,negated_conjecture,
( empty_set = unordered_pair(sK1,sK1)
| sK0(unordered_pair(sK1,sK1)) = sK3
| sK0(unordered_pair(sK1,sK1)) = sK2 ),
inference(resolve,[status(thm)],[c_233,c_181]) ).
cnf(c_1656,negated_conjecture,
( unordered_pair(sK1,sK1) = empty_set
| sK0(unordered_pair(sK1,sK1)) = sK3
| sK0(unordered_pair(sK1,sK1)) = sK2 ),
inference(copy,[status(thm)],[c_1655]) ).
cnf(c_1380,negated_conjecture,
( sK0(unordered_pair(sK1,sK1)) = sK3
| sK0(unordered_pair(sK1,sK1)) = sK2 ),
inference(resolve,[status(thm)],[c_224,c_1656]) ).
cnf(c_1657,plain,
unordered_pair(A,A) = singleton(A),
inference(copy,[status(thm)],[c_170]) ).
cnf(c_1658,plain,
( empty_set = singleton(A)
| sK0(singleton(A)) = A
| sK0(singleton(A)) = A ),
inference(resolve,[status(thm)],[c_233,c_1657]) ).
cnf(c_1659,plain,
( empty_set = singleton(A)
| sK0(singleton(A)) = A
| sK0(unordered_pair(A,A)) = A ),
inference(paramod,[status(thm)],[c_170,c_1658]) ).
cnf(c_1660,plain,
( empty_set = singleton(A)
| sK0(unordered_pair(A,A)) = A
| sK0(unordered_pair(A,A)) = A ),
inference(paramod,[status(thm)],[c_170,c_1659]) ).
cnf(c_1661,plain,
( empty_set = unordered_pair(A,A)
| sK0(unordered_pair(A,A)) = A
| sK0(unordered_pair(A,A)) = A ),
inference(paramod,[status(thm)],[c_170,c_1660]) ).
cnf(c_1662,plain,
( unordered_pair(A,A) = empty_set
| sK0(unordered_pair(A,A)) = A
| sK0(unordered_pair(A,A)) = A ),
inference(copy,[status(thm)],[c_1661]) ).
cnf(c_1663,plain,
( unordered_pair(A,A) = empty_set
| sK0(unordered_pair(A,A)) = A ),
inference(copy,[status(thm)],[c_1662]) ).
cnf(c_1383,plain,
sK0(unordered_pair(A,A)) = A,
inference(resolve,[status(thm)],[c_224,c_1663]) ).
cnf(c_1664,negated_conjecture,
( sK0(unordered_pair(sK1,sK1)) = sK3
| sK1 = sK2 ),
inference(paramod,[status(thm)],[c_1383,c_1380]) ).
cnf(c_1665,negated_conjecture,
( sK1 = sK3
| sK1 = sK2 ),
inference(paramod,[status(thm)],[c_1383,c_1664]) ).
cnf(c_1666,negated_conjecture,
( sK1 = sK3
| sK2 = sK1 ),
inference(copy,[status(thm)],[c_1665]) ).
cnf(c_1667,negated_conjecture,
( sK3 = sK1
| sK2 = sK1 ),
inference(copy,[status(thm)],[c_1666]) ).
cnf(c_1385,negated_conjecture,
sK3 = sK1,
inference(resolve,[status(thm)],[c_182,c_1667]) ).
cnf(c_1668,negated_conjecture,
unordered_pair(sK2,sK1) = unordered_pair(sK1,sK1),
inference(paramod,[status(thm)],[c_1385,c_181]) ).
cnf(c_1388,negated_conjecture,
unordered_pair(sK1,sK2) = unordered_pair(sK1,sK1),
inference(paramod,[status(thm)],[c_73,c_1668]) ).
cnf(c_1669,plain,
in(sK0(unordered_pair(A,A)),unordered_pair(B,A)),
inference(resolve,[status(thm)],[c_235,c_1383]) ).
cnf(c_1492,plain,
in(A,unordered_pair(B,A)),
inference(paramod,[status(thm)],[c_1383,c_1669]) ).
cnf(c_1587,plain,
in(sK2,unordered_pair(sK1,sK1)),
inference(paramod,[status(thm)],[c_1388,c_1492]) ).
cnf(c_1592,plain,
subset(unordered_pair(sK2,sK2),unordered_pair(sK1,sK1)),
inference(resolve,[status(thm)],[c_1587,c_222]) ).
cnf(c_1670,plain,
sK1 = sK2,
inference(resolve,[status(thm)],[c_1592,c_173]) ).
cnf(c_1671,plain,
sK2 = sK1,
inference(copy,[status(thm)],[c_1670]) ).
cnf(c_1652,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_182,c_1671]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU149+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.57 % Computer : n013.cluster.edu
% 0.09/0.57 % Model : x86_64 x86_64
% 0.09/0.57 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.57 % Memory : 8046.5625MB
% 0.09/0.57 % OS : Linux 6.8.0-71-generic
% 0.09/0.57 % CPULimit : 300
% 0.09/0.57 % WCLimit : 300
% 0.09/0.57 % DateTime : Sat Sep 26 08:40:22 UTC 2026
% 0.09/0.57 % CPUTime :
% 0.09/0.57 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/0.57 % Process 2354893 was started by sandbox2 on n013,
% 0.09/0.57 % Sat Sep 26 08:40:22 2026
% 0.09/0.57 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.09/0.59
% 0.09/0.59 % From the command line: assign(max_seconds, 300).
% 0.14/0.84
% 0.14/0.84 % SZS status Theorem for theBenchmark
% 0.14/0.84
% 0.14/0.84 % Proof 1 at 0.18 (+ 0.06) seconds.
% 0.14/0.84 % Length of proof is 32.
% 0.14/0.84 % Level of proof is 8.
% 0.14/0.84 % Maximum clause weight is 16.000.
% 0.14/0.84 % Given clauses 217.
% 0.14/0.84
% 0.14/0.84 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------