%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : SET581+3 : TPTP v9.3.1. Released v2.2.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 : n009.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:57:00 AM UTC 2026
% Result : Theorem 0.13s 0.41s
% Output : Proof 0.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 5
% Syntax : Number of formulae : 45 ( 17 unt; 0 def)
% Number of atoms : 145 ( 22 equ)
% Maximal formula atoms : 10 ( 3 avg)
% Number of connectives : 163 ( 63 ~; 50 |; 44 &)
% ( 4 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 2 ( 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 : 84 ( 1 sgn 61 !; 14 ?)
% Comments :
%------------------------------------------------------------------------------
fof(intersection_defn,axiom,
! [B,C,D] :
( member(D,intersection(B,C))
<=> ( member(D,C)
& member(D,B) ) ),
file('theBenchmark.p',intersection_defn) ).
fof(empty_set_defn,axiom,
! [B] : ~ member(B,empty_set),
file('theBenchmark.p',empty_set_defn) ).
fof(equal_member_defn,axiom,
! [B,C] :
( B = C
<=> ! [D] :
( member(D,B)
<=> member(D,C) ) ),
file('theBenchmark.p',equal_member_defn) ).
fof(not_equal_defn,axiom,
! [B,C] :
( not_equal(B,C)
<=> B != C ),
file('theBenchmark.p',not_equal_defn) ).
fof(prove_th24,conjecture,
! [B,C,D] :
( ( member(B,D)
& member(B,C) )
=> not_equal(intersection(C,D),empty_set) ),
file('theBenchmark.p',prove_th24) ).
fof(f_1_1,plain,
! [B,C,D] :
( ( member(D,intersection(B,C))
| ~ member(D,C)
| ~ member(D,B) )
& ( ( member(D,C)
& member(D,B) )
| ~ member(D,intersection(B,C)) ) ),
inference(fof_nnf,[status(thm)],[intersection_defn]) ).
fof(f_1_2,plain,
! [U_2,U_1,U_0] :
( ( member(U_0,intersection(U_2,U_1))
| ~ member(U_0,U_1)
| ~ member(U_0,U_2) )
& ( ( member(U_0,U_1)
& member(U_0,U_2) )
| ~ member(U_0,intersection(U_2,U_1)) ) ),
inference(variable_rename,[status(thm)],[f_1_1]) ).
fof(f_1_3,plain,
( ! [U_8,U_6,U_4] :
( member(U_4,intersection(U_8,U_6))
| ~ member(U_4,U_6)
| ~ member(U_4,U_8) )
& ! [U_7,U_5,U_3] :
( ( member(U_3,U_5)
& member(U_3,U_7) )
| ~ member(U_3,intersection(U_7,U_5)) ) ),
inference(miniscope,[status(thm)],[f_1_2]) ).
cnf(f_1_6,plain,
( member(U_4,intersection(U_8,U_6))
| ~ member(U_4,U_6)
| ~ member(U_4,U_8) ),
inference(clausify,[status(thm)],[f_1_3]) ).
fof(f_2_1,plain,
! [B] : ~ member(B,empty_set),
inference(fof_nnf,[status(thm)],[empty_set_defn]) ).
fof(f_2_2,plain,
! [U_9] : ~ member(U_9,empty_set),
inference(variable_rename,[status(thm)],[f_2_1]) ).
cnf(f_2_3,plain,
~ member(U_9,empty_set),
inference(clausify,[status(thm)],[f_2_2]) ).
fof(f_3_1,plain,
! [B,C] :
( ( B = C
| ? [D] :
( ( ~ member(D,B)
& member(D,C) )
| ( ~ member(D,C)
& member(D,B) ) ) )
& ( ! [D] :
( ( member(D,B)
| ~ member(D,C) )
& ( member(D,C)
| ~ member(D,B) ) )
| B != C ) ),
inference(fof_nnf,[status(thm)],[equal_member_defn]) ).
fof(f_3_2,plain,
! [U_13,U_12] :
( ( U_13 = U_12
| ? [U_11] :
( ( ~ member(U_11,U_13)
& member(U_11,U_12) )
| ( ~ member(U_11,U_12)
& member(U_11,U_13) ) ) )
& ( ! [U_10] :
( ( member(U_10,U_13)
| ~ member(U_10,U_12) )
& ( member(U_10,U_12)
| ~ member(U_10,U_13) ) )
| U_13 != U_12 ) ),
inference(variable_rename,[status(thm)],[f_3_1]) ).
fof(f_3_3,plain,
( ! [U_21,U_19] :
( U_21 = U_19
| ? [U_17] :
( ~ member(U_17,U_21)
& member(U_17,U_19) )
| ? [U_16] :
( ~ member(U_16,U_19)
& member(U_16,U_21) ) )
& ! [U_20,U_18] :
( ( ! [U_15] :
( member(U_15,U_20)
| ~ member(U_15,U_18) )
& ! [U_14] :
( member(U_14,U_18)
| ~ member(U_14,U_20) ) )
| U_20 != U_18 ) ),
inference(miniscope,[status(thm)],[f_3_2]) ).
fof(f_3_4,plain,
( ! [U_21,U_19] :
( U_21 = U_19
| ? [U_17] :
( ~ member(U_17,U_21)
& member(U_17,U_19) )
| ( ~ member(sK1(U_21,U_19),U_19)
& member(sK1(U_21,U_19),U_21) ) )
& ! [U_20,U_18] :
( ( ! [U_15] :
( member(U_15,U_20)
| ~ member(U_15,U_18) )
& ! [U_14] :
( member(U_14,U_18)
| ~ member(U_14,U_20) ) )
| U_20 != U_18 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(U_16,sK1(U_21,U_19))],[f_3_3]) ).
fof(f_3_5,plain,
( ! [U_21,U_19] :
( U_21 = U_19
| ( ~ member(sK2(U_21,U_19),U_21)
& member(sK2(U_21,U_19),U_19) )
| ( ~ member(sK1(U_21,U_19),U_19)
& member(sK1(U_21,U_19),U_21) ) )
& ! [U_20,U_18] :
( ( ! [U_15] :
( member(U_15,U_20)
| ~ member(U_15,U_18) )
& ! [U_14] :
( member(U_14,U_18)
| ~ member(U_14,U_20) ) )
| U_20 != U_18 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2]),skolemize(U_17,sK2(U_21,U_19))],[f_3_4]) ).
cnf(f_3_6,plain,
( member(U_14,U_18)
| ~ member(U_14,U_20)
| U_20 != U_18 ),
inference(clausify,[status(thm)],[f_3_5]) ).
fof(f_4_1,plain,
! [B,C] :
( ( not_equal(B,C)
| B = C )
& ( B != C
| ~ not_equal(B,C) ) ),
inference(fof_nnf,[status(thm)],[not_equal_defn]) ).
fof(f_4_2,plain,
! [U_23,U_22] :
( ( not_equal(U_23,U_22)
| U_23 = U_22 )
& ( U_23 != U_22
| ~ not_equal(U_23,U_22) ) ),
inference(variable_rename,[status(thm)],[f_4_1]) ).
fof(f_4_3,plain,
( ! [U_27,U_25] :
( not_equal(U_27,U_25)
| U_27 = U_25 )
& ! [U_26,U_24] :
( U_26 != U_24
| ~ not_equal(U_26,U_24) ) ),
inference(miniscope,[status(thm)],[f_4_2]) ).
cnf(f_4_5,plain,
( not_equal(U_27,U_25)
| U_27 = U_25 ),
inference(clausify,[status(thm)],[f_4_3]) ).
fof(f_7_1,negated_conjecture,
~ ! [B,C,D] :
( ( member(B,D)
& member(B,C) )
=> not_equal(intersection(C,D),empty_set) ),
inference(negate,[status(cth)],[prove_th24]) ).
fof(f_7_2,negated_conjecture,
? [B,C,D] :
( ~ not_equal(intersection(C,D),empty_set)
& member(B,D)
& member(B,C) ),
inference(fof_nnf,[status(thm)],[f_7_1]) ).
fof(f_7_3,negated_conjecture,
? [U_37,U_36,U_35] :
( ~ not_equal(intersection(U_36,U_35),empty_set)
& member(U_37,U_35)
& member(U_37,U_36) ),
inference(variable_rename,[status(thm)],[f_7_2]) ).
fof(f_7_4,negated_conjecture,
? [U_36,U_35] :
( ~ not_equal(intersection(U_36,U_35),empty_set)
& member(sK4,U_35)
& member(sK4,U_36) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4]),skolemize(U_37,sK4)],[f_7_3]) ).
fof(f_7_5,negated_conjecture,
? [U_35] :
( ~ not_equal(intersection(sK5,U_35),empty_set)
& member(sK4,U_35)
& member(sK4,sK5) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5]),skolemize(U_36,sK5)],[f_7_4]) ).
fof(f_7_6,negated_conjecture,
( ~ not_equal(intersection(sK5,sK6),empty_set)
& member(sK4,sK6)
& member(sK4,sK5) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6]),skolemize(U_35,sK6)],[f_7_5]) ).
fof(f_7_7,negated_conjecture,
( ~ not_equal(intersection(sK5,sK6),empty_set)
& member(sK4,sK6)
& member(sK4,sK5) ),
inference(definitional_conversion,[status(esa)],[f_7_6]) ).
cnf(f_7_8,negated_conjecture,
member(sK4,sK5),
inference(clausify,[status(thm)],[f_7_7]) ).
cnf(f_7_9,negated_conjecture,
member(sK4,sK6),
inference(clausify,[status(thm)],[f_7_7]) ).
cnf(f_7_10,negated_conjecture,
~ not_equal(intersection(sK5,sK6),empty_set),
inference(clausify,[status(thm)],[f_7_7]) ).
cnf(t1,plain,
~ member(sK4,empty_set),
inference(start,[status(thm),parent(0:0)],[f_2_3]) ).
cnf(t2,plain,
( ~ member(sK4,intersection(sK5,sK6))
| intersection(sK5,sK6) != empty_set
| member(sK4,empty_set) ),
inference(extension,[status(thm),parent(t1:1)],[f_3_6]) ).
cnf(t3,plain,
$false,
inference(connection,[status(thm),parent(t2:1)],[t2:1,t1:1]) ).
cnf(t4,plain,
( not_equal(intersection(sK5,sK6),empty_set)
| intersection(sK5,sK6) = empty_set ),
inference(extension,[status(thm),parent(t2:2)],[f_4_5]) ).
cnf(t5,plain,
$false,
inference(connection,[status(thm),parent(t4:1)],[t4:1,t2:2]) ).
cnf(t6,plain,
~ not_equal(intersection(sK5,sK6),empty_set),
inference(extension,[status(thm),parent(t4:2)],[f_7_10]) ).
cnf(t7,plain,
$false,
inference(connection,[status(thm),parent(t6:1)],[t6:1,t4:2]) ).
cnf(t8,plain,
( ~ member(sK4,sK6)
| ~ member(sK4,sK5)
| member(sK4,intersection(sK5,sK6)) ),
inference(extension,[status(thm),parent(t2:3)],[f_1_6]) ).
cnf(t9,plain,
$false,
inference(connection,[status(thm),parent(t8:1)],[t8:1,t2:3]) ).
cnf(t10,plain,
member(sK4,sK5),
inference(extension,[status(thm),parent(t8:2)],[f_7_8]) ).
cnf(t11,plain,
$false,
inference(connection,[status(thm),parent(t10:1)],[t10:1,t8:2]) ).
cnf(t12,plain,
member(sK4,sK6),
inference(extension,[status(thm),parent(t8:3)],[f_7_9]) ).
cnf(t13,plain,
$false,
inference(connection,[status(thm),parent(t12:1)],[t12:1,t8:3]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SET581+3 : TPTP v9.3.1. Released v2.2.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.10/0.35 % Computer : n009.cluster.edu
% 0.10/0.35 % Model : x86_64 x86_64
% 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35 % Memory : 8046.5625MB
% 0.10/0.35 % OS : Linux 6.8.0-71-generic
% 0.10/0.35 % CPULimit : 300
% 0.10/0.35 % WCLimit : 300
% 0.10/0.35 % DateTime : Sat Sep 19 22:41:11 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.13/0.41 % SZS status Theorem for theBenchmark
% 0.13/0.41 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------