%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SEU171+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 : n007.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:18 AM UTC 2026
% Result : Theorem 33.41s 4.70s
% Output : CNFRefutation 0.12s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 35
% Syntax : Number of formulae : 160 ( 79 unt; 0 def)
% Number of atoms : 287 ( 85 equ)
% Maximal formula atoms : 7 ( 1 avg)
% Number of connectives : 219 ( 92 ~; 72 |; 21 &)
% ( 12 <=>; 22 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 7 ( 5 usr; 1 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 5 con; 0-2 aty)
% Number of variables : 244 ( 29 sgn 85 !; 7 ?)
% 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(d1_xboole_0,axiom,
! [A] :
( A = empty_set
<=> ! [B] : ~ in(B,A) ),
file('theBenchmark.p',d1_xboole_0) ).
fof(d1_zfmisc_1,axiom,
! [A,B] :
( B = powerset(A)
<=> ! [C] :
( in(C,B)
<=> subset(C,A) ) ),
file('theBenchmark.p',d1_zfmisc_1) ).
fof(d2_subset_1,axiom,
! [A,B] :
( ( empty(A)
=> ( element(B,A)
<=> empty(B) ) )
& ( ~ empty(A)
=> ( element(B,A)
<=> in(B,A) ) ) ),
file('theBenchmark.p',d2_subset_1) ).
fof(d3_tarski,axiom,
! [A,B] :
( subset(A,B)
<=> ! [C] :
( in(C,A)
=> in(C,B) ) ),
file('theBenchmark.p',d3_tarski) ).
fof(d5_subset_1,axiom,
! [A,B] :
( element(B,powerset(A))
=> subset_complement(A,B) = set_difference(A,B) ),
file('theBenchmark.p',d5_subset_1) ).
fof(fc1_subset_1,axiom,
! [A] : ~ empty(powerset(A)),
file('theBenchmark.p',fc1_subset_1) ).
fof(idempotence_k2_xboole_0,axiom,
! [A,B] : set_union2(A,A) = A,
file('theBenchmark.p',idempotence_k2_xboole_0) ).
fof(l28_zfmisc_1,axiom,
! [A,B] :
( ~ in(A,B)
=> disjoint(singleton(A),B) ),
file('theBenchmark.p',l28_zfmisc_1) ).
fof(rc1_xboole_0,axiom,
? [A] : empty(A),
file('theBenchmark.p',rc1_xboole_0) ).
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(t12_xboole_1,axiom,
! [A,B] :
( subset(A,B)
=> set_union2(A,B) = B ),
file('theBenchmark.p',t12_xboole_1) ).
fof(t28_xboole_1,axiom,
! [A,B] :
( subset(A,B)
=> set_intersection2(A,B) = A ),
file('theBenchmark.p',t28_xboole_1) ).
fof(t37_xboole_1,axiom,
! [A,B] :
( set_difference(A,B) = empty_set
<=> subset(A,B) ),
file('theBenchmark.p',t37_xboole_1) ).
fof(t37_zfmisc_1,axiom,
! [A,B] :
( subset(singleton(A),B)
<=> in(A,B) ),
file('theBenchmark.p',t37_zfmisc_1) ).
fof(t38_zfmisc_1,axiom,
! [A,B,C] :
( subset(unordered_pair(A,B),C)
<=> ( in(B,C)
& in(A,C) ) ),
file('theBenchmark.p',t38_zfmisc_1) ).
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_xboole_1,axiom,
! [A] :
( subset(A,empty_set)
=> A = empty_set ),
file('theBenchmark.p',t3_xboole_1) ).
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(t43_subset_1,axiom,
! [A,B] :
( element(B,powerset(A))
=> ! [C] :
( element(C,powerset(A))
=> ( disjoint(B,C)
<=> subset(B,subset_complement(A,C)) ) ) ),
file('theBenchmark.p',t43_subset_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(t4_boole,axiom,
! [A] : set_difference(empty_set,A) = empty_set,
file('theBenchmark.p',t4_boole) ).
fof(t4_xboole_0,axiom,
! [A,B] :
( ~ ( disjoint(A,B)
& ? [C] : in(C,set_intersection2(A,B)) )
& ~ ( ! [C] : ~ in(C,set_intersection2(A,B))
& ~ disjoint(A,B) ) ),
file('theBenchmark.p',t4_xboole_0) ).
fof(t63_xboole_1,axiom,
! [A,B,C] :
( ( disjoint(B,C)
& subset(A,B) )
=> disjoint(A,C) ),
file('theBenchmark.p',t63_xboole_1) ).
fof(t65_zfmisc_1,axiom,
! [A,B] :
( set_difference(A,singleton(B)) = A
<=> ~ in(B,A) ),
file('theBenchmark.p',t65_zfmisc_1) ).
fof(t69_enumset1,axiom,
! [A] : unordered_pair(A,A) = singleton(A),
file('theBenchmark.p',t69_enumset1) ).
fof(t6_boole,axiom,
! [A] :
( empty(A)
=> A = empty_set ),
file('theBenchmark.p',t6_boole) ).
fof(t7_boole,axiom,
! [A,B] :
~ ( empty(B)
& in(A,B) ),
file('theBenchmark.p',t7_boole) ).
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(t92_zfmisc_1,axiom,
! [A,B] :
( in(A,B)
=> subset(A,union(B)) ),
file('theBenchmark.p',t92_zfmisc_1) ).
fof(t99_zfmisc_1,axiom,
! [A] : union(powerset(A)) = A,
file('theBenchmark.p',t99_zfmisc_1) ).
fof(t50_subset_1,conjecture,
! [A] :
( A != empty_set
=> ! [B] :
( element(B,powerset(A))
=> ! [C] :
( element(C,A)
=> ( ~ in(C,B)
=> in(C,subset_complement(A,B)) ) ) ) ),
file('theBenchmark.p',t50_subset_1) ).
fof(t50_subset_1_neg,negated_conjecture,
~ ! [A] :
( A != empty_set
=> ! [B] :
( element(B,powerset(A))
=> ! [C] :
( element(C,A)
=> ( ~ in(C,B)
=> in(C,subset_complement(A,B)) ) ) ) ),
inference(assume_negation,[status(cth)],[t50_subset_1]) ).
fof(nnf_109,plain,
? [A] :
( ? [B] :
( ? [C] :
( ~ in(C,subset_complement(A,B))
& ~ in(C,B)
& element(C,A) )
& element(B,powerset(A)) )
& empty_set != A ),
inference(fof_nnf,[status(thm)],[t50_subset_1_neg]) ).
fof(sk_t50_subset_1_neg,plain,
( ~ in(sK0,subset_complement(sK1,sK2))
& ~ in(sK0,sK2)
& element(sK0,sK1)
& element(sK2,powerset(sK1))
& empty_set != sK1 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1,sK2,sK0]),skolemize(A,sK1),skolemize(B,sK2),skolemize(C,sK0)],[nnf_109]) ).
cnf(c_110,negated_conjecture,
~ in(sK0,subset_complement(sK1,sK2)),
inference(split_conjunct,[status(thm)],[sk_t50_subset_1_neg]) ).
cnf(c_111,negated_conjecture,
~ in(sK0,sK2),
inference(split_conjunct,[status(thm)],[sk_t50_subset_1_neg]) ).
cnf(c_112,negated_conjecture,
element(sK0,sK1),
inference(split_conjunct,[status(thm)],[sk_t50_subset_1_neg]) ).
cnf(c_113,negated_conjecture,
element(sK2,powerset(sK1)),
inference(split_conjunct,[status(thm)],[sk_t50_subset_1_neg]) ).
cnf(c_114,negated_conjecture,
empty_set != sK1,
inference(split_conjunct,[status(thm)],[sk_t50_subset_1_neg]) ).
cnf(c_120,plain,
union(powerset(A)) = A,
inference(clausify,[status(thm)],[t99_zfmisc_1]) ).
cnf(c_121,plain,
( subset(A,union(B))
| ~ in(A,B) ),
inference(clausify,[status(thm)],[t92_zfmisc_1]) ).
cnf(c_125,plain,
( set_difference(A,B) != A
| disjoint(A,B) ),
inference(clausify,[status(thm)],[t83_xboole_1]) ).
cnf(c_126,plain,
( set_difference(A,B) = A
| ~ disjoint(A,B) ),
inference(clausify,[status(thm)],[t83_xboole_1]) ).
cnf(c_127,plain,
subset(A,set_union2(A,B)),
inference(clausify,[status(thm)],[t7_xboole_1]) ).
cnf(c_128,plain,
( ~ empty(B)
| ~ in(A,B) ),
inference(clausify,[status(thm)],[t7_boole]) ).
cnf(c_130,plain,
( empty_set = A
| ~ empty(A) ),
inference(clausify,[status(thm)],[t6_boole]) ).
cnf(c_131,plain,
singleton(A) = unordered_pair(A,A),
inference(clausify,[status(thm)],[t69_enumset1]) ).
cnf(c_132,plain,
( in(B,A)
| set_difference(A,singleton(B)) = A ),
inference(clausify,[status(thm)],[t65_zfmisc_1]) ).
cnf(c_133,plain,
( in(B,A)
| set_difference(A,unordered_pair(B,B)) = A ),
inference(paramod,[status(thm)],[c_131,c_132]) ).
cnf(c_136,plain,
( disjoint(A,C)
| ~ disjoint(B,C)
| ~ subset(A,B) ),
inference(clausify,[status(thm)],[t63_xboole_1]) ).
cnf(c_138,plain,
( ~ disjoint(B,C)
| ~ in(A,set_intersection2(B,C)) ),
inference(clausify,[status(thm)],[t4_xboole_0]) ).
cnf(c_140,plain,
set_difference(empty_set,A) = empty_set,
inference(clausify,[status(thm)],[t4_boole]) ).
cnf(c_141,plain,
set_difference(A,set_difference(A,B)) = set_intersection2(A,B),
inference(clausify,[status(thm)],[t48_xboole_1]) ).
cnf(c_142,plain,
set_intersection2(A,B) = set_difference(A,set_difference(A,B)),
inference(copy,[status(thm)],[c_141]) ).
cnf(c_147,plain,
( subset(A,subset_complement(B,C))
| ~ disjoint(A,C)
| ~ element(C,powerset(B))
| ~ element(A,powerset(B)) ),
inference(clausify,[status(thm)],[t43_subset_1]) ).
cnf(c_148,plain,
set_difference(set_union2(A,B),B) = set_difference(A,B),
inference(clausify,[status(thm)],[t40_xboole_1]) ).
cnf(c_149,plain,
( empty_set = A
| ~ subset(A,empty_set) ),
inference(clausify,[status(thm)],[t3_xboole_1]) ).
cnf(c_160,plain,
set_union2(A,set_difference(B,A)) = set_union2(A,B),
inference(clausify,[status(thm)],[t39_xboole_1]) ).
cnf(c_163,plain,
( in(A,C)
| ~ subset(unordered_pair(A,B),C) ),
inference(clausify,[status(thm)],[t38_zfmisc_1]) ).
cnf(c_164,plain,
( ~ in(A,B)
| subset(singleton(A),B) ),
inference(clausify,[status(thm)],[t37_zfmisc_1]) ).
cnf(c_165,plain,
( ~ in(A,B)
| subset(unordered_pair(A,A),B) ),
inference(paramod,[status(thm)],[c_131,c_164]) ).
cnf(c_167,plain,
( ~ subset(A,B)
| set_difference(A,B) = empty_set ),
inference(clausify,[status(thm)],[t37_xboole_1]) ).
cnf(c_178,plain,
( set_intersection2(A,B) = A
| ~ subset(A,B) ),
inference(clausify,[status(thm)],[t28_xboole_1]) ).
cnf(c_179,plain,
( set_difference(A,set_difference(A,B)) = A
| ~ subset(A,B) ),
inference(paramod,[status(thm)],[c_142,c_178]) ).
cnf(c_192,plain,
( set_union2(A,B) = B
| ~ subset(A,B) ),
inference(clausify,[status(thm)],[t12_xboole_1]) ).
cnf(c_200,plain,
( disjoint(B,A)
| ~ disjoint(A,B) ),
inference(clausify,[status(thm)],[symmetry_r1_xboole_0]) ).
cnf(c_201,plain,
subset(A,A),
inference(clausify,[status(thm)],[reflexivity_r1_tarski]) ).
fof(nnf_55,plain,
? [A] : empty(A),
inference(fof_nnf,[status(thm)],[rc1_xboole_0]) ).
fof(sk_rc1_xboole_0,plain,
empty(sK3),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3]),skolemize(A,sK3)],[nnf_55]) ).
cnf(c_205,plain,
empty(sK3),
inference(split_conjunct,[status(thm)],[sk_rc1_xboole_0]) ).
cnf(c_216,plain,
( disjoint(singleton(A),B)
| in(A,B) ),
inference(clausify,[status(thm)],[l28_zfmisc_1]) ).
cnf(c_217,plain,
( disjoint(unordered_pair(A,A),B)
| in(A,B) ),
inference(paramod,[status(thm)],[c_131,c_216]) ).
cnf(c_226,plain,
set_union2(A,A) = A,
inference(clausify,[status(thm)],[idempotence_k2_xboole_0]) ).
cnf(c_231,plain,
~ empty(powerset(A)),
inference(clausify,[status(thm)],[fc1_subset_1]) ).
cnf(c_243,plain,
( subset_complement(B,A) = set_difference(B,A)
| ~ element(A,powerset(B)) ),
inference(clausify,[status(thm)],[d5_subset_1]) ).
fof(nnf_14,plain,
! [A,B] :
( ( ? [C] :
( ~ in(C,B)
& in(C,A) )
| subset(A,B) )
& ( ! [X0] :
( in(X0,B)
| ~ in(X0,A) )
| ~ subset(A,B) ) ),
inference(fof_nnf,[status(thm)],[d3_tarski]) ).
fof(sk_d3_tarski_sk,plain,
! [A,B] :
( ( ( ~ in(sK4(A,B),B)
& in(sK4(A,B),A) )
| subset(A,B) )
& ( ! [X0] :
( in(X0,B)
| ~ in(X0,A) )
| ~ subset(A,B) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4]),skolemize(C,sK4(A,B))],[nnf_14]) ).
fof(sk_d3_tarski,plain,
( ! [VAR_0,VAR_1] :
( ~ in(sK4(VAR_0,VAR_1),VAR_1)
| subset(VAR_0,VAR_1) )
& ! [VAR_0,VAR_1] :
( in(sK4(VAR_0,VAR_1),VAR_0)
| subset(VAR_0,VAR_1) )
& ! [VAR_0,VAR_1,VAR_2] :
( in(VAR_2,VAR_1)
| ~ in(VAR_2,VAR_0)
| ~ subset(VAR_0,VAR_1) ) ),
inference(cnf_transformation,[status(thm)],[sk_d3_tarski_sk]) ).
cnf(c_268,plain,
( in(sK4(A,B),A)
| subset(A,B) ),
inference(split_conjunct,[status(thm)],[sk_d3_tarski]) ).
cnf(c_296,plain,
( ~ in(B,A)
| element(B,A)
| empty(A) ),
inference(clausify,[status(thm)],[d2_subset_1]) ).
cnf(c_297,plain,
( in(B,A)
| ~ element(B,A)
| empty(A) ),
inference(clausify,[status(thm)],[d2_subset_1]) ).
cnf(c_300,plain,
( ~ subset(C,A)
| in(C,B)
| powerset(A) != B ),
inference(clausify,[status(thm)],[d1_zfmisc_1]) ).
cnf(c_303,plain,
( ~ in(B,A)
| empty_set != A ),
inference(clausify,[status(thm)],[d1_xboole_0]) ).
cnf(c_314,plain,
set_intersection2(A,B) = set_intersection2(B,A),
inference(clausify,[status(thm)],[commutativity_k3_xboole_0]) ).
cnf(c_19567,plain,
set_difference(A,set_difference(A,B)) = set_intersection2(B,A),
inference(paramod,[status(thm)],[c_142,c_314]) ).
cnf(c_315,plain,
set_difference(A,set_difference(A,B)) = set_difference(B,set_difference(B,A)),
inference(paramod,[status(thm)],[c_142,c_19567]) ).
cnf(c_316,plain,
set_union2(A,B) = set_union2(B,A),
inference(clausify,[status(thm)],[commutativity_k2_xboole_0]) ).
cnf(c_324,plain,
( ~ disjoint(B,C)
| ~ in(A,set_difference(B,set_difference(B,C))) ),
inference(paramod,[status(thm)],[c_142,c_138]) ).
cnf(c_381,plain,
set_difference(sK2,unordered_pair(sK0,sK0)) = sK2,
inference(resolve,[status(thm)],[c_133,c_111]) ).
cnf(c_387,plain,
disjoint(empty_set,A),
inference(resolve,[status(thm)],[c_140,c_125]) ).
cnf(c_393,plain,
( subset(A,subset_complement(sK1,sK2))
| ~ disjoint(A,sK2)
| ~ element(A,powerset(sK1)) ),
inference(resolve,[status(thm)],[c_147,c_113]) ).
cnf(c_19568,plain,
set_difference(set_union2(set_union2(A,B),B),B) = set_difference(A,B),
inference(paramod,[status(thm)],[c_148,c_148]) ).
cnf(c_396,plain,
set_difference(set_union2(A,set_union2(B,A)),A) = set_difference(B,A),
inference(paramod,[status(thm)],[c_316,c_19568]) ).
cnf(c_412,plain,
set_difference(set_union2(A,B),set_difference(B,A)) = set_difference(A,set_difference(B,A)),
inference(paramod,[status(thm)],[c_160,c_148]) ).
cnf(c_19569,plain,
set_union2(A,set_difference(B,A)) = set_union2(A,set_union2(B,A)),
inference(paramod,[status(thm)],[c_148,c_160]) ).
cnf(c_19570,plain,
set_union2(A,B) = set_union2(A,set_union2(B,A)),
inference(paramod,[status(thm)],[c_160,c_19569]) ).
cnf(c_413,plain,
set_union2(A,set_union2(B,A)) = set_union2(A,B),
inference(copy,[status(thm)],[c_19570]) ).
cnf(c_414,plain,
set_difference(set_union2(A,B),A) = set_difference(B,A),
inference(paramod,[status(thm)],[c_413,c_396]) ).
cnf(c_522,plain,
in(A,unordered_pair(A,B)),
inference(resolve,[status(thm)],[c_201,c_163]) ).
cnf(c_530,plain,
empty_set = sK3,
inference(resolve,[status(thm)],[c_205,c_130]) ).
cnf(c_555,plain,
disjoint(sK3,A),
inference(paramod,[status(thm)],[c_530,c_387]) ).
cnf(c_556,plain,
( ~ in(B,A)
| sK3 != A ),
inference(paramod,[status(thm)],[c_530,c_303]) ).
cnf(c_566,plain,
( ~ subset(A,B)
| set_difference(A,B) = sK3 ),
inference(paramod,[status(thm)],[c_530,c_167]) ).
cnf(c_19571,plain,
( empty_set = A
| ~ subset(A,sK3) ),
inference(paramod,[status(thm)],[c_530,c_149]) ).
cnf(c_570,plain,
( sK3 = A
| ~ subset(A,sK3) ),
inference(paramod,[status(thm)],[c_530,c_19571]) ).
cnf(c_19572,negated_conjecture,
sK3 != sK1,
inference(paramod,[status(thm)],[c_530,c_114]) ).
cnf(c_572,negated_conjecture,
sK1 != sK3,
inference(copy,[status(thm)],[c_19572]) ).
cnf(c_593,plain,
( set_difference(unordered_pair(A,A),B) = unordered_pair(A,A)
| in(A,B) ),
inference(resolve,[status(thm)],[c_217,c_126]) ).
cnf(c_617,plain,
subset_complement(sK1,sK2) = set_difference(sK1,sK2),
inference(resolve,[status(thm)],[c_243,c_113]) ).
cnf(c_624,plain,
( subset(A,set_difference(sK1,sK2))
| ~ disjoint(A,sK2)
| ~ element(A,powerset(sK1)) ),
inference(paramod,[status(thm)],[c_617,c_393]) ).
cnf(c_627,negated_conjecture,
~ in(sK0,set_difference(sK1,sK2)),
inference(paramod,[status(thm)],[c_617,c_110]) ).
cnf(c_19573,negated_conjecture,
( in(sK2,powerset(sK1))
| empty(powerset(sK1)) ),
inference(resolve,[status(thm)],[c_297,c_113]) ).
cnf(c_2055,negated_conjecture,
in(sK2,powerset(sK1)),
inference(resolve,[status(thm)],[c_231,c_19573]) ).
cnf(c_2056,plain,
( in(sK0,sK1)
| empty(sK1) ),
inference(resolve,[status(thm)],[c_297,c_112]) ).
cnf(c_19574,plain,
A = set_union2(A,A),
inference(copy,[status(thm)],[c_226]) ).
cnf(c_19575,plain,
( ~ subset(A,B)
| in(A,set_union2(powerset(B),powerset(B))) ),
inference(resolve,[status(thm)],[c_300,c_19574]) ).
cnf(c_2085,plain,
( ~ subset(A,B)
| in(A,powerset(B)) ),
inference(paramod,[status(thm)],[c_226,c_19575]) ).
cnf(c_2179,plain,
set_difference(set_union2(A,B),set_difference(A,B)) = set_difference(B,set_difference(B,set_union2(A,B))),
inference(paramod,[status(thm)],[c_148,c_315]) ).
cnf(c_2194,plain,
subset(A,set_union2(B,A)),
inference(paramod,[status(thm)],[c_316,c_127]) ).
cnf(c_2990,plain,
( disjoint(A,B)
| ~ subset(A,sK3) ),
inference(resolve,[status(thm)],[c_555,c_136]) ).
cnf(c_3075,plain,
( subset(unordered_pair(sK0,sK0),sK1)
| empty(sK1) ),
inference(resolve,[status(thm)],[c_2056,c_165]) ).
cnf(c_3127,plain,
( in(sK4(A,sK3),A)
| sK3 = A ),
inference(resolve,[status(thm)],[c_570,c_268]) ).
cnf(c_3173,plain,
( in(sK4(A,sK3),A)
| disjoint(A,B) ),
inference(resolve,[status(thm)],[c_2990,c_268]) ).
cnf(c_3263,plain,
disjoint(sK2,unordered_pair(sK0,sK0)),
inference(resolve,[status(thm)],[c_381,c_125]) ).
cnf(c_19576,plain,
subset(sK2,union(powerset(sK1))),
inference(resolve,[status(thm)],[c_2055,c_121]) ).
cnf(c_3332,plain,
subset(sK2,sK1),
inference(paramod,[status(thm)],[c_120,c_19576]) ).
cnf(c_19577,plain,
set_union2(sK2,sK1) = sK1,
inference(resolve,[status(thm)],[c_3332,c_192]) ).
cnf(c_3345,plain,
set_union2(sK1,sK2) = sK1,
inference(paramod,[status(thm)],[c_316,c_19577]) ).
cnf(c_19578,plain,
sK3 != unordered_pair(A,B),
inference(resolve,[status(thm)],[c_522,c_556]) ).
cnf(c_3996,plain,
unordered_pair(A,B) != sK3,
inference(copy,[status(thm)],[c_19578]) ).
cnf(c_4248,plain,
set_difference(A,set_difference(A,set_union2(B,A))) = A,
inference(resolve,[status(thm)],[c_2194,c_179]) ).
cnf(c_4256,plain,
set_difference(set_union2(A,B),set_difference(A,B)) = B,
inference(paramod,[status(thm)],[c_4248,c_2179]) ).
cnf(c_4468,plain,
disjoint(unordered_pair(sK0,sK0),sK2),
inference(resolve,[status(thm)],[c_3263,c_200]) ).
cnf(c_19579,plain,
set_difference(set_union2(A,B),set_difference(A,B)) = set_difference(B,set_difference(A,B)),
inference(paramod,[status(thm)],[c_316,c_412]) ).
cnf(c_19580,plain,
B = set_difference(B,set_difference(A,B)),
inference(paramod,[status(thm)],[c_4256,c_19579]) ).
cnf(c_4596,plain,
set_difference(A,set_difference(B,A)) = A,
inference(copy,[status(thm)],[c_19580]) ).
cnf(c_4606,plain,
set_difference(set_union2(A,B),set_difference(B,A)) = A,
inference(paramod,[status(thm)],[c_4596,c_412]) ).
cnf(c_19581,plain,
( ~ disjoint(set_union2(B,C),B)
| ~ in(A,set_difference(set_union2(B,C),set_difference(C,B))) ),
inference(paramod,[status(thm)],[c_414,c_324]) ).
cnf(c_4743,plain,
( ~ disjoint(set_union2(B,C),B)
| ~ in(A,B) ),
inference(paramod,[status(thm)],[c_4606,c_19581]) ).
cnf(c_9022,plain,
( in(unordered_pair(sK0,sK0),powerset(sK1))
| empty(sK1) ),
inference(resolve,[status(thm)],[c_3075,c_2085]) ).
cnf(c_11809,plain,
set_difference(unordered_pair(sK0,sK0),set_difference(sK1,sK2)) = unordered_pair(sK0,sK0),
inference(resolve,[status(thm)],[c_593,c_627]) ).
cnf(c_12522,plain,
( subset(unordered_pair(sK0,sK0),set_difference(sK1,sK2))
| ~ element(unordered_pair(sK0,sK0),powerset(sK1)) ),
inference(resolve,[status(thm)],[c_624,c_4468]) ).
cnf(c_13834,plain,
( disjoint(B,A)
| in(sK4(A,sK3),A) ),
inference(resolve,[status(thm)],[c_3173,c_200]) ).
cnf(c_14003,plain,
( sK3 = A
| ~ disjoint(set_union2(A,B),A) ),
inference(resolve,[status(thm)],[c_4743,c_3127]) ).
cnf(c_19582,plain,
( element(unordered_pair(sK0,sK0),powerset(sK1))
| empty(powerset(sK1))
| empty(sK1) ),
inference(resolve,[status(thm)],[c_9022,c_296]) ).
cnf(c_16221,plain,
( element(unordered_pair(sK0,sK0),powerset(sK1))
| empty(sK1) ),
inference(resolve,[status(thm)],[c_231,c_19582]) ).
cnf(c_19583,plain,
( sK3 = sK1
| ~ disjoint(sK1,sK1) ),
inference(paramod,[status(thm)],[c_3345,c_14003]) ).
cnf(c_19584,plain,
( sK1 = sK3
| ~ disjoint(sK1,sK1) ),
inference(copy,[status(thm)],[c_19583]) ).
cnf(c_17517,negated_conjecture,
~ disjoint(sK1,sK1),
inference(resolve,[status(thm)],[c_572,c_19584]) ).
cnf(c_17566,plain,
in(sK4(sK1,sK3),sK1),
inference(resolve,[status(thm)],[c_17517,c_13834]) ).
cnf(c_17627,plain,
~ empty(sK1),
inference(resolve,[status(thm)],[c_17566,c_128]) ).
cnf(c_17718,plain,
element(unordered_pair(sK0,sK0),powerset(sK1)),
inference(resolve,[status(thm)],[c_17627,c_16221]) ).
cnf(c_18271,plain,
subset(unordered_pair(sK0,sK0),set_difference(sK1,sK2)),
inference(resolve,[status(thm)],[c_17718,c_12522]) ).
cnf(c_19585,plain,
set_difference(unordered_pair(sK0,sK0),set_difference(sK1,sK2)) = sK3,
inference(resolve,[status(thm)],[c_18271,c_566]) ).
cnf(c_19586,plain,
unordered_pair(sK0,sK0) = sK3,
inference(paramod,[status(thm)],[c_11809,c_19585]) ).
cnf(c_19566,plain,
$false,
inference(resolve,[status(thm)],[c_3996,c_19586]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU171+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.36 % Computer : n007.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sat Sep 26 08:42:25 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/0.36 % Process 3326839 was started by sandbox2 on n007,
% 0.09/0.36 % Sat Sep 26 08:42:25 2026
% 0.09/0.36 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.09/0.39
% 0.09/0.39 % From the command line: assign(max_seconds, 300).
% 33.41/4.70
% 33.41/4.70 % given #500 (T,wt=15): 7142 element(powerset(c4),f20(c3)). [resolve(6926,a,296,c),unit_del(a,500)].
% 33.41/4.70
% 33.41/4.70 % given #1000 (F,wt=18): 4047 -in(A,B) | -disjoint(unordered_pair(A,C),B). [resolve(522,a,150,a)].
% 33.41/4.70
% 33.41/4.70 % given #1500 (T,wt=18): 12564 -in(f17(c4),set_difference(A,c3)) | empty(c4). [resolve(696,b,5349,b)].
% 33.41/4.70
% 33.41/4.70 % SZS status Theorem for theBenchmark
% 33.41/4.70
% 33.41/4.70 % Proof 1 at 3.33 (+ 0.92) seconds.
% 33.41/4.70 % Length of proof is 132.
% 33.41/4.70 % Level of proof is 15.
% 33.41/4.70 % Maximum clause weight is 45.000.
% 33.41/4.70 % Given clauses 1839.
% 33.41/4.70
% 33.41/4.70 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------