%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SEU154+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 : n010.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:13 AM UTC 2026
% Result : Theorem 25.64s 8.95s
% Output : CNFRefutation 25.64s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 15
% Syntax : Number of formulae : 55 ( 36 unt; 0 def)
% Number of atoms : 79 ( 29 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 42 ( 18 ~; 14 |; 3 &)
% ( 2 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 2 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 3 con; 0-2 aty)
% Number of variables : 99 ( 8 sgn 32 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(commutativity_k2_xboole_0,axiom,
! [A,B] : set_union2(A,B) = set_union2(B,A),
file('theBenchmark.p',commutativity_k2_xboole_0) ).
fof(commutativity_k3_xboole_0,axiom,
! [A,B] : set_intersection2(A,B) = set_intersection2(B,A),
file('theBenchmark.p',commutativity_k3_xboole_0) ).
fof(l32_xboole_1,axiom,
! [A,B] :
( set_difference(A,B) = empty_set
<=> subset(A,B) ),
file('theBenchmark.p',l32_xboole_1) ).
fof(l3_zfmisc_1,axiom,
! [A,B,C] :
( subset(A,B)
=> ( subset(A,set_difference(B,singleton(C)))
| in(C,A) ) ),
file('theBenchmark.p',l3_zfmisc_1) ).
fof(reflexivity_r1_tarski,axiom,
! [A,B] : subset(A,A),
file('theBenchmark.p',reflexivity_r1_tarski) ).
fof(symmetry_r1_xboole_0,axiom,
! [A,B] :
( disjoint(A,B)
=> disjoint(B,A) ),
file('theBenchmark.p',symmetry_r1_xboole_0) ).
fof(t39_xboole_1,axiom,
! [A,B] : set_union2(A,set_difference(B,A)) = set_union2(A,B),
file('theBenchmark.p',t39_xboole_1) ).
fof(t3_boole,axiom,
! [A] : set_difference(A,empty_set) = A,
file('theBenchmark.p',t3_boole) ).
fof(t40_xboole_1,axiom,
! [A,B] : set_difference(set_union2(A,B),B) = set_difference(A,B),
file('theBenchmark.p',t40_xboole_1) ).
fof(t48_xboole_1,axiom,
! [A,B] : set_difference(A,set_difference(A,B)) = set_intersection2(A,B),
file('theBenchmark.p',t48_xboole_1) ).
fof(t63_xboole_1,axiom,
! [A,B,C] :
( ( disjoint(B,C)
& subset(A,B) )
=> disjoint(A,C) ),
file('theBenchmark.p',t63_xboole_1) ).
fof(t69_enumset1,axiom,
! [A] : unordered_pair(A,A) = singleton(A),
file('theBenchmark.p',t69_enumset1) ).
fof(t7_xboole_1,axiom,
! [A,B] : subset(A,set_union2(A,B)),
file('theBenchmark.p',t7_xboole_1) ).
fof(t83_xboole_1,axiom,
! [A,B] :
( disjoint(A,B)
<=> set_difference(A,B) = A ),
file('theBenchmark.p',t83_xboole_1) ).
fof(l28_zfmisc_1,conjecture,
! [A,B] :
( ~ in(A,B)
=> disjoint(singleton(A),B) ),
file('theBenchmark.p',l28_zfmisc_1) ).
fof(l28_zfmisc_1_neg,negated_conjecture,
~ ! [A,B] :
( ~ in(A,B)
=> disjoint(singleton(A),B) ),
inference(assume_negation,[status(cth)],[l28_zfmisc_1]) ).
cnf(c_79,plain,
set_union2(A,B) = set_union2(B,A),
inference(clausify,[status(thm)],[commutativity_k2_xboole_0]) ).
cnf(c_80,plain,
set_intersection2(A,B) = set_intersection2(B,A),
inference(clausify,[status(thm)],[commutativity_k3_xboole_0]) ).
cnf(c_138,plain,
( ~ subset(A,B)
| set_difference(A,B) = empty_set ),
inference(clausify,[status(thm)],[l32_xboole_1]) ).
cnf(c_139,plain,
( subset(A,set_difference(B,singleton(C)))
| in(C,A)
| ~ subset(A,B) ),
inference(clausify,[status(thm)],[l3_zfmisc_1]) ).
cnf(c_144,plain,
subset(A,A),
inference(clausify,[status(thm)],[reflexivity_r1_tarski]) ).
cnf(c_145,plain,
( disjoint(B,A)
| ~ disjoint(A,B) ),
inference(clausify,[status(thm)],[symmetry_r1_xboole_0]) ).
cnf(c_161,plain,
set_union2(A,set_difference(B,A)) = set_union2(A,B),
inference(clausify,[status(thm)],[t39_xboole_1]) ).
cnf(c_162,plain,
set_difference(A,empty_set) = A,
inference(clausify,[status(thm)],[t3_boole]) ).
cnf(c_167,plain,
set_difference(set_union2(A,B),B) = set_difference(A,B),
inference(clausify,[status(thm)],[t40_xboole_1]) ).
cnf(c_169,plain,
set_difference(A,set_difference(A,B)) = set_intersection2(A,B),
inference(clausify,[status(thm)],[t48_xboole_1]) ).
cnf(c_170,plain,
set_intersection2(A,B) = set_difference(A,set_difference(A,B)),
inference(copy,[status(thm)],[c_169]) ).
cnf(c_177,plain,
( disjoint(A,C)
| ~ disjoint(B,C)
| ~ subset(A,B) ),
inference(clausify,[status(thm)],[t63_xboole_1]) ).
cnf(c_178,plain,
singleton(A) = unordered_pair(A,A),
inference(clausify,[status(thm)],[t69_enumset1]) ).
cnf(c_183,plain,
subset(A,set_union2(A,B)),
inference(clausify,[status(thm)],[t7_xboole_1]) ).
cnf(c_185,plain,
( set_difference(A,B) != A
| disjoint(A,B) ),
inference(clausify,[status(thm)],[t83_xboole_1]) ).
fof(nnf_75,plain,
? [A,B] :
( ~ disjoint(singleton(A),B)
& ~ in(A,B) ),
inference(fof_nnf,[status(thm)],[l28_zfmisc_1_neg]) ).
fof(sk_l28_zfmisc_1_neg,plain,
( ~ disjoint(singleton(sK0),sK1)
& ~ in(sK0,sK1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1]),skolemize(A,sK0),skolemize(B,sK1)],[nnf_75]) ).
cnf(c_192,negated_conjecture,
~ in(sK0,sK1),
inference(split_conjunct,[status(thm)],[sk_l28_zfmisc_1_neg]) ).
cnf(c_193,negated_conjecture,
~ disjoint(singleton(sK0),sK1),
inference(split_conjunct,[status(thm)],[sk_l28_zfmisc_1_neg]) ).
cnf(c_194,negated_conjecture,
~ disjoint(unordered_pair(sK0,sK0),sK1),
inference(paramod,[status(thm)],[c_178,c_193]) ).
cnf(c_11117,plain,
set_difference(A,set_difference(A,B)) = set_intersection2(B,A),
inference(paramod,[status(thm)],[c_170,c_80]) ).
cnf(c_230,plain,
set_difference(A,set_difference(A,B)) = set_difference(B,set_difference(B,A)),
inference(paramod,[status(thm)],[c_170,c_11117]) ).
cnf(c_234,plain,
( subset(A,set_difference(B,unordered_pair(C,C)))
| in(C,A)
| ~ subset(A,B) ),
inference(paramod,[status(thm)],[c_178,c_139]) ).
cnf(c_616,plain,
set_difference(set_union2(A,B),A) = set_difference(B,A),
inference(paramod,[status(thm)],[c_79,c_167]) ).
cnf(c_620,plain,
set_difference(set_union2(A,B),set_difference(B,A)) = set_difference(A,set_difference(B,A)),
inference(paramod,[status(thm)],[c_161,c_167]) ).
cnf(c_648,plain,
set_difference(A,set_union2(A,B)) = empty_set,
inference(resolve,[status(thm)],[c_183,c_138]) ).
cnf(c_1111,plain,
( subset(B,set_difference(B,unordered_pair(A,A)))
| in(A,B) ),
inference(resolve,[status(thm)],[c_234,c_144]) ).
cnf(c_11118,plain,
set_difference(A,empty_set) = set_difference(set_union2(A,B),set_difference(set_union2(A,B),A)),
inference(paramod,[status(thm)],[c_648,c_230]) ).
cnf(c_11119,plain,
A = set_difference(set_union2(A,B),set_difference(set_union2(A,B),A)),
inference(paramod,[status(thm)],[c_162,c_11118]) ).
cnf(c_11120,plain,
A = set_difference(set_union2(A,B),set_difference(B,A)),
inference(paramod,[status(thm)],[c_616,c_11119]) ).
cnf(c_11121,plain,
A = set_difference(A,set_difference(B,A)),
inference(paramod,[status(thm)],[c_620,c_11120]) ).
cnf(c_1438,plain,
set_difference(A,set_difference(B,A)) = A,
inference(copy,[status(thm)],[c_11121]) ).
cnf(c_1642,plain,
disjoint(A,set_difference(B,A)),
inference(resolve,[status(thm)],[c_1438,c_185]) ).
cnf(c_1649,plain,
disjoint(set_difference(A,B),B),
inference(resolve,[status(thm)],[c_1642,c_145]) ).
cnf(c_1651,plain,
( disjoint(A,C)
| ~ subset(A,set_difference(B,C)) ),
inference(resolve,[status(thm)],[c_1649,c_177]) ).
cnf(c_11080,plain,
( disjoint(B,unordered_pair(A,A))
| in(A,B) ),
inference(resolve,[status(thm)],[c_1111,c_1651]) ).
cnf(c_11114,plain,
( disjoint(unordered_pair(A,A),B)
| in(A,B) ),
inference(resolve,[status(thm)],[c_11080,c_145]) ).
cnf(c_11122,negated_conjecture,
in(sK0,sK1),
inference(resolve,[status(thm)],[c_11114,c_194]) ).
cnf(c_11116,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_192,c_11122]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU154+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/5.57 % Computer : n010.cluster.edu
% 0.09/5.57 % Model : x86_64 x86_64
% 0.09/5.57 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.57 % Memory : 8046.5625MB
% 0.09/5.57 % OS : Linux 6.8.0-71-generic
% 0.09/5.57 % CPULimit : 300
% 0.09/5.57 % WCLimit : 300
% 0.09/5.57 % DateTime : Sat Sep 26 08:41:52 UTC 2026
% 0.09/5.57 % CPUTime :
% 0.09/5.57 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/5.57 % Process 2934330 was started by sandbox2 on n010,
% 0.09/5.57 % Sat Sep 26 08:41:52 2026
% 0.09/5.57 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.09/5.59
% 0.09/5.59 % From the command line: assign(max_seconds, 300).
% 25.64/8.95
% 25.64/8.95 % given #500 (T,wt=6): 3901 in(A,powerset(set_union2(A,B))). [para(161(a,1),3812(a,2,1)),rewrite([1438(2)])].
% 25.64/8.95
% 25.64/8.95 % given #1000 (F,wt=10): 6416 -in(set_union2(powerset(A),B),set_difference(f2(powerset(A)),C)). [para(1753(a,1),4183(a,1,1,1))].
% 25.64/8.95
% 25.64/8.95 % SZS status Theorem for theBenchmark
% 25.64/8.95
% 25.64/8.95 % Proof 1 at 2.38 (+ 0.82) seconds.
% 25.64/8.95 % Length of proof is 46.
% 25.64/8.95 % Level of proof is 10.
% 25.64/8.95 % Maximum clause weight is 13.000.
% 25.64/8.95 % Given clauses 1328.
% 25.64/8.95
% 25.64/8.95 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------