%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : SEU354+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n019.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:59:04 AM UTC 2026
% Result : Theorem 2.80s 3.06s
% Output : Proof 2.80s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 7
% Syntax : Number of formulae : 72 ( 37 unt; 0 def)
% Number of atoms : 147 ( 58 equ)
% Maximal formula atoms : 11 ( 2 avg)
% Number of connectives : 134 ( 59 ~; 50 |; 19 &)
% ( 3 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 6 ( 4 usr; 3 prp; 0-2 aty)
% Number of functors : 4 ( 4 usr; 2 con; 0-1 aty)
% Number of variables : 31 ( 0 sgn 13 !; 5 ?)
% Comments :
%------------------------------------------------------------------------------
fof(d2_tex_2,axiom,
! [A,B] :
( element(B,A)
=> ( proper_element(B,A)
<=> B != union(A) ) ),
file('theBenchmark.p',d2_tex_2) ).
fof(t5_tex_2,conjecture,
! [A,B] :
( element(B,powerset(A))
=> ( proper_element(B,powerset(A))
<=> B != A ) ),
file('theBenchmark.p',t5_tex_2) ).
fof(t99_zfmisc_1,axiom,
! [A] : union(powerset(A)) = A,
file('theBenchmark.p',t99_zfmisc_1) ).
fof(f_17_1,plain,
! [A,B] :
( ( ( proper_element(B,A)
| B = union(A) )
& ( B != union(A)
| ~ proper_element(B,A) ) )
| ~ element(B,A) ),
inference(fof_nnf,[status(thm)],[d2_tex_2]) ).
fof(f_17_2,plain,
! [U_28,U_27] :
( ( ( proper_element(U_27,U_28)
| U_27 = union(U_28) )
& ( U_27 != union(U_28)
| ~ proper_element(U_27,U_28) ) )
| ~ element(U_27,U_28) ),
inference(variable_rename,[status(thm)],[f_17_1]) ).
cnf(f_17_3,plain,
( U_27 != union(U_28)
| ~ proper_element(U_27,U_28)
| ~ element(U_27,U_28) ),
inference(clausify,[status(thm)],[f_17_2]) ).
cnf(f_17_4,plain,
( proper_element(U_27,U_28)
| U_27 = union(U_28)
| ~ element(U_27,U_28) ),
inference(clausify,[status(thm)],[f_17_2]) ).
fof(f_39_1,negated_conjecture,
~ ! [A,B] :
( element(B,powerset(A))
=> ( proper_element(B,powerset(A))
<=> B != A ) ),
inference(negate,[status(cth)],[t5_tex_2]) ).
fof(f_39_2,negated_conjecture,
? [A,B] :
( ( ( ~ proper_element(B,powerset(A))
& B != A )
| ( B = A
& proper_element(B,powerset(A)) ) )
& element(B,powerset(A)) ),
inference(fof_nnf,[status(thm)],[f_39_1]) ).
fof(f_39_3,negated_conjecture,
? [U_64,U_63] :
( ( ( ~ proper_element(U_63,powerset(U_64))
& U_63 != U_64 )
| ( U_63 = U_64
& proper_element(U_63,powerset(U_64)) ) )
& element(U_63,powerset(U_64)) ),
inference(variable_rename,[status(thm)],[f_39_2]) ).
fof(f_39_4,negated_conjecture,
? [U_63] :
( ( ( ~ proper_element(U_63,powerset(sK6))
& U_63 != sK6 )
| ( U_63 = sK6
& proper_element(U_63,powerset(sK6)) ) )
& element(U_63,powerset(sK6)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6]),skolemize(U_64,sK6)],[f_39_3]) ).
fof(f_39_5,negated_conjecture,
( ( ( ~ proper_element(sK7,powerset(sK6))
& sK7 != sK6 )
| ( sK7 = sK6
& proper_element(sK7,powerset(sK6)) ) )
& element(sK7,powerset(sK6)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7]),skolemize(U_63,sK7)],[f_39_4]) ).
fof(f_39_6,negated_conjecture,
( ( ~ proper_element(sK7,powerset(sK6))
| ~ sP1 )
& ( sK7 != sK6
| ~ sP1 )
& ( sK7 = sK6
| ~ sP0 )
& ( proper_element(sK7,powerset(sK6))
| ~ sP0 )
& ( sP1
| sP0 )
& element(sK7,powerset(sK6)) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP0,sP1])],[f_39_5]) ).
cnf(f_39_7,negated_conjecture,
element(sK7,powerset(sK6)),
inference(clausify,[status(thm)],[f_39_6]) ).
cnf(f_39_8,negated_conjecture,
( sP1
| sP0 ),
inference(clausify,[status(thm)],[f_39_6]) ).
cnf(f_39_9,negated_conjecture,
( proper_element(sK7,powerset(sK6))
| ~ sP0 ),
inference(clausify,[status(thm)],[f_39_6]) ).
cnf(f_39_10,negated_conjecture,
( sK7 = sK6
| ~ sP0 ),
inference(clausify,[status(thm)],[f_39_6]) ).
cnf(f_39_11,negated_conjecture,
( sK7 != sK6
| ~ sP1 ),
inference(clausify,[status(thm)],[f_39_6]) ).
cnf(f_39_12,negated_conjecture,
( ~ proper_element(sK7,powerset(sK6))
| ~ sP1 ),
inference(clausify,[status(thm)],[f_39_6]) ).
fof(f_43_1,plain,
! [A] : union(powerset(A)) = A,
inference(fof_nnf,[status(thm)],[t99_zfmisc_1]) ).
fof(f_43_2,plain,
! [U_70] : union(powerset(U_70)) = U_70,
inference(variable_rename,[status(thm)],[f_43_1]) ).
cnf(f_43_3,plain,
union(powerset(U_70)) = U_70,
inference(clausify,[status(thm)],[f_43_2]) ).
cnf(equality_1,axiom,
Eq_x_0 = Eq_x_0,
theory(equality,[reflexivity]) ).
cnf(equality_2,axiom,
( Eq_x_1 = Eq_x_0
| Eq_x_0 != Eq_x_1 ),
theory(equality,[symmetry]) ).
cnf(equality_3,axiom,
( Eq_x_0 = Eq_x_2
| Eq_x_1 != Eq_x_2
| Eq_x_0 != Eq_x_1 ),
theory(equality,[transitivity]) ).
cnf(equality_5,axiom,
( union(Eq_x_0) = union(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(t1,plain,
( ~ proper_element(sK7,powerset(sK6))
| sK7 != union(powerset(sK6))
| ~ element(sK7,powerset(sK6)) ),
inference(start,[status(thm),parent(0:0)],[f_17_3]) ).
cnf(t2,plain,
element(sK7,powerset(sK6)),
inference(extension,[status(thm),parent(t1:1)],[f_39_7]) ).
cnf(t3,plain,
$false,
inference(connection,[status(thm),parent(t2:1)],[t2:1,t1:1]) ).
cnf(l1,lemma,
element(sK7,powerset(sK6)),
inference(lemma,[status(cth),parent(t1:1),below(0:0)],[t1:1]) ).
cnf(t4,plain,
( sK6 != union(powerset(sK6))
| sK7 != sK6
| sK7 = union(powerset(sK6)) ),
inference(extension,[status(thm),parent(t1:2)],[equality_3]) ).
cnf(t5,plain,
$false,
inference(connection,[status(thm),parent(t4:1)],[t4:1,t1:2]) ).
cnf(t6,plain,
( union(powerset(sK6)) != sK6
| sK7 != union(powerset(sK6))
| sK7 = sK6 ),
inference(extension,[status(thm),parent(t4:2)],[equality_3]) ).
cnf(t7,plain,
$false,
inference(connection,[status(thm),parent(t6:1)],[t6:1,t4:2]) ).
cnf(t8,plain,
( proper_element(sK7,powerset(sK6))
| ~ element(sK7,powerset(sK6))
| sK7 = union(powerset(sK6)) ),
inference(extension,[status(thm),parent(t6:2)],[f_17_4]) ).
cnf(t9,plain,
$false,
inference(connection,[status(thm),parent(t8:1)],[t8:1,t6:2]) ).
cnf(t10,plain,
element(sK7,powerset(sK6)),
inference(extension,[status(thm),parent(t8:2)],[f_39_7]) ).
cnf(t11,plain,
$false,
inference(connection,[status(thm),parent(t10:1)],[t10:1,t8:2]) ).
cnf(t12,plain,
( ~ sP1
| ~ proper_element(sK7,powerset(sK6)) ),
inference(extension,[status(thm),parent(t8:3)],[f_39_12]) ).
cnf(t13,plain,
$false,
inference(connection,[status(thm),parent(t12:1)],[t12:1,t8:3]) ).
cnf(t14,plain,
( sP0
| sP1 ),
inference(extension,[status(thm),parent(t12:2)],[f_39_8]) ).
cnf(t15,plain,
$false,
inference(connection,[status(thm),parent(t14:1)],[t14:1,t12:2]) ).
cnf(t16,plain,
( sK7 = sK6
| ~ sP0 ),
inference(extension,[status(thm),parent(t14:2)],[f_39_10]) ).
cnf(t17,plain,
$false,
inference(connection,[status(thm),parent(t16:1)],[t16:1,t14:2]) ).
cnf(t18,plain,
$false,
inference(reduction,[status(thm),parent(t16:2)],[t16:2,t4:2]) ).
cnf(t19,plain,
union(powerset(sK6)) = sK6,
inference(extension,[status(thm),parent(t6:3)],[f_43_3]) ).
cnf(t20,plain,
$false,
inference(connection,[status(thm),parent(t19:1)],[t19:1,t6:3]) ).
cnf(t21,plain,
( union(powerset(sK6)) != union(powerset(sK6))
| sK6 != union(powerset(sK6))
| sK6 = union(powerset(sK6)) ),
inference(extension,[status(thm),parent(t4:3)],[equality_3]) ).
cnf(t22,plain,
$false,
inference(connection,[status(thm),parent(t21:1)],[t21:1,t4:3]) ).
cnf(t23,plain,
( union(powerset(sK6)) != sK6
| sK6 = union(powerset(sK6)) ),
inference(extension,[status(thm),parent(t21:2)],[equality_2]) ).
cnf(t24,plain,
$false,
inference(connection,[status(thm),parent(t23:1)],[t23:1,t21:2]) ).
cnf(t25,plain,
union(powerset(sK6)) = sK6,
inference(extension,[status(thm),parent(t23:2)],[f_43_3]) ).
cnf(t26,plain,
$false,
inference(connection,[status(thm),parent(t25:1)],[t25:1,t23:2]) ).
cnf(t27,plain,
( powerset(sK6) != powerset(sK6)
| union(powerset(sK6)) = union(powerset(sK6)) ),
inference(extension,[status(thm),parent(t21:3)],[equality_5]) ).
cnf(t28,plain,
$false,
inference(connection,[status(thm),parent(t27:1)],[t27:1,t21:3]) ).
cnf(t29,plain,
powerset(sK6) = powerset(sK6),
inference(extension,[status(thm),parent(t27:2)],[equality_1]) ).
cnf(t30,plain,
$false,
inference(connection,[status(thm),parent(t29:1)],[t29:1,t27:2]) ).
cnf(t31,plain,
( sK7 = union(powerset(sK6))
| ~ element(sK7,powerset(sK6))
| proper_element(sK7,powerset(sK6)) ),
inference(extension,[status(thm),parent(t1:3)],[f_17_4]) ).
cnf(t32,plain,
$false,
inference(connection,[status(thm),parent(t31:1)],[t31:1,t1:3]) ).
cnf(t33,plain,
element(sK7,powerset(sK6)),
inference(lemma_extension,[status(thm),parent(t31:2)],[l1:1]) ).
cnf(t34,plain,
$false,
inference(connection,[status(thm),parent(t33:1)],[t33:1,t31:2]) ).
cnf(t35,plain,
( union(powerset(sK6)) != sK6
| sK7 = sK6
| sK7 != union(powerset(sK6)) ),
inference(extension,[status(thm),parent(t31:3)],[equality_3]) ).
cnf(t36,plain,
$false,
inference(connection,[status(thm),parent(t35:1)],[t35:1,t31:3]) ).
cnf(t37,plain,
( ~ sP1
| sK7 != sK6 ),
inference(extension,[status(thm),parent(t35:2)],[f_39_11]) ).
cnf(t38,plain,
$false,
inference(connection,[status(thm),parent(t37:1)],[t37:1,t35:2]) ).
cnf(t39,plain,
( sP0
| sP1 ),
inference(extension,[status(thm),parent(t37:2)],[f_39_8]) ).
cnf(t40,plain,
$false,
inference(connection,[status(thm),parent(t39:1)],[t39:1,t37:2]) ).
cnf(t41,plain,
( proper_element(sK7,powerset(sK6))
| ~ sP0 ),
inference(extension,[status(thm),parent(t39:2)],[f_39_9]) ).
cnf(t42,plain,
$false,
inference(connection,[status(thm),parent(t41:1)],[t41:1,t39:2]) ).
cnf(t43,plain,
$false,
inference(reduction,[status(thm),parent(t41:2)],[t41:2,t1:3]) ).
cnf(t44,plain,
union(powerset(sK6)) = sK6,
inference(extension,[status(thm),parent(t35:3)],[f_43_3]) ).
cnf(t45,plain,
$false,
inference(connection,[status(thm),parent(t44:1)],[t44:1,t35:3]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU354+1 : 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/sandbox2/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n019.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 : Sun Sep 20 00:02:20 UTC 2026
% 0.09/0.36 % CPUTime :
% 2.80/3.06 % SZS status Theorem for theBenchmark
% 2.80/3.06 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------