%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : SEU169+2 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n003.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 : Thu Sep 24 08:58:20 AM UTC 2026
% Result : Theorem 97.67s 98.01s
% Output : Proof 97.67s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 6
% Syntax : Number of formulae : 48 ( 23 unt; 0 def)
% Number of atoms : 200 ( 26 equ)
% Maximal formula atoms : 14 ( 4 avg)
% Number of connectives : 240 ( 88 ~; 79 |; 63 &)
% ( 4 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 3 con; 0-3 aty)
% Number of variables : 113 ( 1 sgn 77 !; 26 ?)
% Comments :
%------------------------------------------------------------------------------
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(d4_tarski,axiom,
! [A,B] :
( B = union(A)
<=> ! [C] :
( in(C,B)
<=> ? [D] :
( in(D,A)
& in(C,D) ) ) ),
file('theBenchmark.p',d4_tarski) ).
fof(fc1_subset_1,axiom,
! [A] : ~ empty(powerset(A)),
file('theBenchmark.p',fc1_subset_1) ).
fof(l3_subset_1,conjecture,
! [A,B] :
( element(B,powerset(A))
=> ! [C] :
( in(C,B)
=> in(C,A) ) ),
file('theBenchmark.p',l3_subset_1) ).
fof(t99_zfmisc_1,lemma,
! [A] : union(powerset(A)) = A,
file('theBenchmark.p',t99_zfmisc_1) ).
fof(f_10_1,plain,
! [A,B] :
( ( ( ( element(B,A)
| ~ empty(B) )
& ( empty(B)
| ~ element(B,A) ) )
| ~ empty(A) )
& ( ( ( element(B,A)
| ~ in(B,A) )
& ( in(B,A)
| ~ element(B,A) ) )
| empty(A) ) ),
inference(fof_nnf,[status(thm)],[d2_subset_1]) ).
fof(f_10_2,plain,
! [U_46,U_45] :
( ( ( ( element(U_45,U_46)
| ~ empty(U_45) )
& ( empty(U_45)
| ~ element(U_45,U_46) ) )
| ~ empty(U_46) )
& ( ( ( element(U_45,U_46)
| ~ in(U_45,U_46) )
& ( in(U_45,U_46)
| ~ element(U_45,U_46) ) )
| empty(U_46) ) ),
inference(variable_rename,[status(thm)],[f_10_1]) ).
fof(f_10_3,plain,
( ! [U_54] :
( ( ! [U_52] :
( element(U_52,U_54)
| ~ empty(U_52) )
& ! [U_51] :
( empty(U_51)
| ~ element(U_51,U_54) ) )
| ~ empty(U_54) )
& ! [U_53] :
( ( ! [U_50] :
( element(U_50,U_53)
| ~ in(U_50,U_53) )
& ! [U_49] :
( in(U_49,U_53)
| ~ element(U_49,U_53) ) )
| empty(U_53) ) ),
inference(miniscope,[status(thm)],[f_10_2]) ).
cnf(f_10_4,plain,
( in(U_49,U_53)
| ~ element(U_49,U_53)
| empty(U_53) ),
inference(clausify,[status(thm)],[f_10_3]) ).
fof(f_16_1,plain,
! [A,B] :
( ( B = union(A)
| ? [C] :
( ( ~ in(C,B)
& ? [D] :
( in(D,A)
& in(C,D) ) )
| ( ! [D] :
( ~ in(D,A)
| ~ in(C,D) )
& in(C,B) ) ) )
& ( ! [C] :
( ( in(C,B)
| ! [D] :
( ~ in(D,A)
| ~ in(C,D) ) )
& ( ? [D] :
( in(D,A)
& in(C,D) )
| ~ in(C,B) ) )
| B != union(A) ) ),
inference(fof_nnf,[status(thm)],[d4_tarski]) ).
fof(f_16_2,plain,
! [U_138,U_137] :
( ( U_137 = union(U_138)
| ? [U_136] :
( ( ~ in(U_136,U_137)
& ? [U_135] :
( in(U_135,U_138)
& in(U_136,U_135) ) )
| ( ! [U_134] :
( ~ in(U_134,U_138)
| ~ in(U_136,U_134) )
& in(U_136,U_137) ) ) )
& ( ! [U_133] :
( ( in(U_133,U_137)
| ! [U_132] :
( ~ in(U_132,U_138)
| ~ in(U_133,U_132) ) )
& ( ? [U_131] :
( in(U_131,U_138)
& in(U_133,U_131) )
| ~ in(U_133,U_137) ) )
| U_137 != union(U_138) ) ),
inference(variable_rename,[status(thm)],[f_16_1]) ).
fof(f_16_3,plain,
( ! [U_146,U_144] :
( U_144 = union(U_146)
| ? [U_142] :
( ~ in(U_142,U_144)
& ? [U_135] :
( in(U_135,U_146)
& in(U_142,U_135) ) )
| ? [U_141] :
( ! [U_134] :
( ~ in(U_134,U_146)
| ~ in(U_141,U_134) )
& in(U_141,U_144) ) )
& ! [U_145,U_143] :
( ( ! [U_140] :
( in(U_140,U_143)
| ! [U_132] :
( ~ in(U_132,U_145)
| ~ in(U_140,U_132) ) )
& ! [U_139] :
( ? [U_131] :
( in(U_131,U_145)
& in(U_139,U_131) )
| ~ in(U_139,U_143) ) )
| U_143 != union(U_145) ) ),
inference(miniscope,[status(thm)],[f_16_2]) ).
fof(f_16_4,plain,
( ! [U_146,U_144] :
( U_144 = union(U_146)
| ? [U_142] :
( ~ in(U_142,U_144)
& ? [U_135] :
( in(U_135,U_146)
& in(U_142,U_135) ) )
| ? [U_141] :
( ! [U_134] :
( ~ in(U_134,U_146)
| ~ in(U_141,U_134) )
& in(U_141,U_144) ) )
& ! [U_145,U_143] :
( ( ! [U_140] :
( in(U_140,U_143)
| ! [U_132] :
( ~ in(U_132,U_145)
| ~ in(U_140,U_132) ) )
& ! [U_139] :
( ( in(sK19(U_145,U_143,U_139),U_145)
& in(U_139,sK19(U_145,U_143,U_139)) )
| ~ in(U_139,U_143) ) )
| U_143 != union(U_145) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK19]),skolemize(U_131,sK19(U_145,U_143,U_139))],[f_16_3]) ).
fof(f_16_5,plain,
( ! [U_146,U_144] :
( U_144 = union(U_146)
| ? [U_142] :
( ~ in(U_142,U_144)
& ? [U_135] :
( in(U_135,U_146)
& in(U_142,U_135) ) )
| ( ! [U_134] :
( ~ in(U_134,U_146)
| ~ in(sK20(U_146,U_144),U_134) )
& in(sK20(U_146,U_144),U_144) ) )
& ! [U_145,U_143] :
( ( ! [U_140] :
( in(U_140,U_143)
| ! [U_132] :
( ~ in(U_132,U_145)
| ~ in(U_140,U_132) ) )
& ! [U_139] :
( ( in(sK19(U_145,U_143,U_139),U_145)
& in(U_139,sK19(U_145,U_143,U_139)) )
| ~ in(U_139,U_143) ) )
| U_143 != union(U_145) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK20]),skolemize(U_141,sK20(U_146,U_144))],[f_16_4]) ).
fof(f_16_6,plain,
( ! [U_146,U_144] :
( U_144 = union(U_146)
| ( ~ in(sK21(U_146,U_144),U_144)
& ? [U_135] :
( in(U_135,U_146)
& in(sK21(U_146,U_144),U_135) ) )
| ( ! [U_134] :
( ~ in(U_134,U_146)
| ~ in(sK20(U_146,U_144),U_134) )
& in(sK20(U_146,U_144),U_144) ) )
& ! [U_145,U_143] :
( ( ! [U_140] :
( in(U_140,U_143)
| ! [U_132] :
( ~ in(U_132,U_145)
| ~ in(U_140,U_132) ) )
& ! [U_139] :
( ( in(sK19(U_145,U_143,U_139),U_145)
& in(U_139,sK19(U_145,U_143,U_139)) )
| ~ in(U_139,U_143) ) )
| U_143 != union(U_145) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK21]),skolemize(U_142,sK21(U_146,U_144))],[f_16_5]) ).
fof(f_16_7,plain,
( ! [U_146,U_144] :
( U_144 = union(U_146)
| ( ~ in(sK21(U_146,U_144),U_144)
& in(sK22(U_146,U_144),U_146)
& in(sK21(U_146,U_144),sK22(U_146,U_144)) )
| ( ! [U_134] :
( ~ in(U_134,U_146)
| ~ in(sK20(U_146,U_144),U_134) )
& in(sK20(U_146,U_144),U_144) ) )
& ! [U_145,U_143] :
( ( ! [U_140] :
( in(U_140,U_143)
| ! [U_132] :
( ~ in(U_132,U_145)
| ~ in(U_140,U_132) ) )
& ! [U_139] :
( ( in(sK19(U_145,U_143,U_139),U_145)
& in(U_139,sK19(U_145,U_143,U_139)) )
| ~ in(U_139,U_143) ) )
| U_143 != union(U_145) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK22]),skolemize(U_135,sK22(U_146,U_144))],[f_16_6]) ).
cnf(f_16_10,plain,
( in(U_140,U_143)
| ~ in(U_132,U_145)
| ~ in(U_140,U_132)
| U_143 != union(U_145) ),
inference(clausify,[status(thm)],[f_16_7]) ).
fof(f_33_1,plain,
! [A] : ~ empty(powerset(A)),
inference(fof_nnf,[status(thm)],[fc1_subset_1]) ).
fof(f_33_2,plain,
! [U_178] : ~ empty(powerset(U_178)),
inference(variable_rename,[status(thm)],[f_33_1]) ).
cnf(f_33_3,plain,
~ empty(powerset(U_178)),
inference(clausify,[status(thm)],[f_33_2]) ).
fof(f_47_1,negated_conjecture,
~ ! [A,B] :
( element(B,powerset(A))
=> ! [C] :
( in(C,B)
=> in(C,A) ) ),
inference(negate,[status(cth)],[l3_subset_1]) ).
fof(f_47_2,negated_conjecture,
? [A,B] :
( ? [C] :
( ~ in(C,A)
& in(C,B) )
& element(B,powerset(A)) ),
inference(fof_nnf,[status(thm)],[f_47_1]) ).
fof(f_47_3,negated_conjecture,
? [U_212,U_211] :
( ? [U_210] :
( ~ in(U_210,U_212)
& in(U_210,U_211) )
& element(U_211,powerset(U_212)) ),
inference(variable_rename,[status(thm)],[f_47_2]) ).
fof(f_47_4,negated_conjecture,
? [U_211] :
( ? [U_210] :
( ~ in(U_210,sK26)
& in(U_210,U_211) )
& element(U_211,powerset(sK26)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK26]),skolemize(U_212,sK26)],[f_47_3]) ).
fof(f_47_5,negated_conjecture,
( ? [U_210] :
( ~ in(U_210,sK26)
& in(U_210,sK27) )
& element(sK27,powerset(sK26)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK27]),skolemize(U_211,sK27)],[f_47_4]) ).
fof(f_47_6,negated_conjecture,
( ~ in(sK28,sK26)
& in(sK28,sK27)
& element(sK27,powerset(sK26)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK28]),skolemize(U_210,sK28)],[f_47_5]) ).
cnf(f_47_7,negated_conjecture,
element(sK27,powerset(sK26)),
inference(clausify,[status(thm)],[f_47_6]) ).
cnf(f_47_8,negated_conjecture,
in(sK28,sK27),
inference(clausify,[status(thm)],[f_47_6]) ).
cnf(f_47_9,negated_conjecture,
~ in(sK28,sK26),
inference(clausify,[status(thm)],[f_47_6]) ).
fof(f_103_1,plain,
! [A] : union(powerset(A)) = A,
inference(fof_nnf,[status(thm)],[t99_zfmisc_1]) ).
fof(f_103_2,plain,
! [U_398] : union(powerset(U_398)) = U_398,
inference(variable_rename,[status(thm)],[f_103_1]) ).
cnf(f_103_3,plain,
union(powerset(U_398)) = U_398,
inference(clausify,[status(thm)],[f_103_2]) ).
cnf(equality_2,axiom,
( Eq_x_1 = Eq_x_0
| Eq_x_0 != Eq_x_1 ),
theory(equality,[symmetry]) ).
cnf(t1,plain,
~ in(sK28,sK26),
inference(start,[status(thm),parent(0:0)],[f_47_9]) ).
cnf(t2,plain,
( ~ in(sK28,sK27)
| ~ in(sK27,powerset(sK26))
| sK26 != union(powerset(sK26))
| in(sK28,sK26) ),
inference(extension,[status(thm),parent(t1:1)],[f_16_10]) ).
cnf(t3,plain,
$false,
inference(connection,[status(thm),parent(t2:1)],[t2:1,t1:1]) ).
cnf(t4,plain,
( union(powerset(sK26)) != sK26
| sK26 = union(powerset(sK26)) ),
inference(extension,[status(thm),parent(t2:2)],[equality_2]) ).
cnf(t5,plain,
$false,
inference(connection,[status(thm),parent(t4:1)],[t4:1,t2:2]) ).
cnf(t6,plain,
union(powerset(sK26)) = sK26,
inference(extension,[status(thm),parent(t4:2)],[f_103_3]) ).
cnf(t7,plain,
$false,
inference(connection,[status(thm),parent(t6:1)],[t6:1,t4:2]) ).
cnf(t8,plain,
( ~ element(sK27,powerset(sK26))
| empty(powerset(sK26))
| in(sK27,powerset(sK26)) ),
inference(extension,[status(thm),parent(t2:3)],[f_10_4]) ).
cnf(t9,plain,
$false,
inference(connection,[status(thm),parent(t8:1)],[t8:1,t2:3]) ).
cnf(t10,plain,
~ empty(powerset(sK26)),
inference(extension,[status(thm),parent(t8:2)],[f_33_3]) ).
cnf(t11,plain,
$false,
inference(connection,[status(thm),parent(t10:1)],[t10:1,t8:2]) ).
cnf(t12,plain,
element(sK27,powerset(sK26)),
inference(extension,[status(thm),parent(t8:3)],[f_47_7]) ).
cnf(t13,plain,
$false,
inference(connection,[status(thm),parent(t12:1)],[t12:1,t8:3]) ).
cnf(t14,plain,
in(sK28,sK27),
inference(extension,[status(thm),parent(t2:4)],[f_47_8]) ).
cnf(t15,plain,
$false,
inference(connection,[status(thm),parent(t14:1)],[t14:1,t2:4]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU169+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.03 This is a FOF_THM_RFO_SEQ problem
% 0.00/0.04 % Command : /export/starexec/sandbox/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n003.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Sat Sep 19 23:26:43 UTC 2026
% 0.08/0.35 % CPUTime :
% 97.67/98.01 % SZS status Theorem for theBenchmark
% 97.67/98.01 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------