%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SET624+3 : TPTP v9.3.1. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n015.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 : Fri Sep 25 02:43:38 PM UTC 2026
% Result : Theorem 39.30s 5.48s
% Output : Proof 39.30s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 14
% Syntax : Number of formulae : 86 ( 1 unt; 10 def)
% Number of atoms : 227 ( 0 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 249 ( 108 ~; 111 |; 15 &)
% ( 14 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 13 ( 12 usr; 11 prp; 0-2 aty)
% Number of functors : 5 ( 5 usr; 3 con; 0-2 aty)
% Number of variables : 59 ( 6 sgn 29 !; 5 ?)
% Comments :
%------------------------------------------------------------------------------
fof(sdef4,definition,
( spl4
<=> ~ intersect(sk2,sk3) ),
introduced(definition,[new_symbols(naming,[spl4])],[avatar_definition]) ).
cnf(p21,plain,
( ~ spl4
| ~ intersect(sk2,sk3) ),
inference(avatar_component_clause,[status(thm)],[sdef4]) ).
fof(sdef2,definition,
( spl2
<=> intersect(sk2,sk3) ),
introduced(definition,[new_symbols(naming,[spl2])],[avatar_definition]) ).
cnf(p18,plain,
( ~ spl2
| intersect(sk2,sk3) ),
inference(avatar_component_clause,[status(thm)],[sdef2]) ).
cnf(p26,plain,
( ~ spl4
| ~ spl2
| $false ),
inference(resolution,[status(thm)],[p21,p18]) ).
cnf(sct0,plain,
( ~ spl4
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p26]) ).
fof(sdef5,definition,
( spl5
<=> ~ intersect(sk2,sk4) ),
introduced(definition,[new_symbols(naming,[spl5])],[avatar_definition]) ).
cnf(p24,plain,
( ~ spl5
| ~ intersect(sk2,sk4) ),
inference(avatar_component_clause,[status(thm)],[sdef5]) ).
fof(sdef3,definition,
( spl3
<=> intersect(sk2,sk4) ),
introduced(definition,[new_symbols(naming,[spl3])],[avatar_definition]) ).
cnf(p19,plain,
( ~ spl3
| intersect(sk2,sk4) ),
inference(avatar_component_clause,[status(thm)],[sdef3]) ).
cnf(p27,plain,
( ~ spl5
| ~ spl3
| $false ),
inference(resolution,[status(thm)],[p24,p19]) ).
cnf(sct1,plain,
( ~ spl5
| ~ spl3 ),
inference(avatar_contradiction_clause,[status(thm)],[p27]) ).
fof(sdef1,definition,
( spl1
<=> ~ intersect(sk2,union(sk3,sk4)) ),
introduced(definition,[new_symbols(naming,[spl1])],[avatar_definition]) ).
cnf(p16,plain,
( ~ spl1
| ~ intersect(sk2,union(sk3,sk4)) ),
inference(avatar_component_clause,[status(thm)],[sdef1]) ).
fof(sdef0,definition,
( spl0
<=> intersect(sk2,union(sk3,sk4)) ),
introduced(definition,[new_symbols(naming,[spl0])],[avatar_definition]) ).
cnf(p15,plain,
( ~ spl0
| intersect(sk2,union(sk3,sk4)) ),
inference(avatar_component_clause,[status(thm)],[sdef0]) ).
cnf(p29,plain,
( ~ spl1
| ~ spl0
| $false ),
inference(resolution,[status(thm)],[p16,p15]) ).
cnf(sct2,plain,
( ~ spl1
| ~ spl0 ),
inference(avatar_contradiction_clause,[status(thm)],[p29]) ).
fof(f1,axiom,
! [B,C] :
( intersect(B,C)
<=> ? [D] :
( member(D,C)
& member(D,B) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',intersect_defn) ).
fof(f1_nnf,plain,
! [B,C] :
( ( ! [D] :
( ~ member(D,C)
| ~ member(D,B) )
| intersect(B,C) )
& ( ? [D] :
( member(D,C)
& member(D,B) )
| ~ intersect(B,C) ) ),
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [B,C,D] :
( ( ~ member(D,C)
| ~ member(D,B)
| intersect(B,C) )
& ( ( member(sk0(B,C),C)
& member(sk0(B,C),B) )
| ~ intersect(B,C) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk0])],[f1_nnf]) ).
cnf(c5,plain,
( ~ member(X2,X1)
| ~ member(X2,X0)
| intersect(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(c3,plain,
( member(sk0(X0,X1),X0)
| ~ intersect(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(p31,plain,
( ~ spl0
| member(sk0(sk2,union(sk3,sk4)),sk2) ),
inference(resolution,[status(thm)],[c3,p15]) ).
cnf(p47,plain,
( ~ spl0
| ~ member(sk0(sk2,union(sk3,sk4)),X0)
| intersect(sk2,X0) ),
inference(resolution,[status(thm)],[c5,p31]) ).
fof(sdef8,definition,
( spl8
<=> member(sk0(sk2,union(sk3,sk4)),sk3) ),
introduced(definition,[new_symbols(naming,[spl8])],[avatar_definition]) ).
cnf(p55,plain,
( ~ spl8
| member(sk0(sk2,union(sk3,sk4)),sk3) ),
inference(avatar_component_clause,[status(thm)],[sdef8]) ).
cnf(p118,plain,
( ~ spl8
| ~ spl0
| intersect(sk2,sk3) ),
inference(resolution,[status(thm)],[p47,p55]) ).
cnf(p127,plain,
( ~ spl8
| ~ spl4
| ~ spl0
| $false ),
inference(resolution,[status(thm)],[p118,p21]) ).
cnf(sct3,plain,
( ~ spl8
| ~ spl4
| ~ spl0 ),
inference(avatar_contradiction_clause,[status(thm)],[p127]) ).
fof(sdef9,definition,
( spl9
<=> member(sk0(sk2,union(sk3,sk4)),sk4) ),
introduced(definition,[new_symbols(naming,[spl9])],[avatar_definition]) ).
cnf(p56,plain,
( ~ spl9
| member(sk0(sk2,union(sk3,sk4)),sk4) ),
inference(avatar_component_clause,[status(thm)],[sdef9]) ).
cnf(p119,plain,
( ~ spl9
| ~ spl0
| intersect(sk2,sk4) ),
inference(resolution,[status(thm)],[p47,p56]) ).
cnf(p128,plain,
( ~ spl9
| ~ spl5
| ~ spl0
| $false ),
inference(resolution,[status(thm)],[p119,p24]) ).
cnf(sct4,plain,
( ~ spl9
| ~ spl5
| ~ spl0 ),
inference(avatar_contradiction_clause,[status(thm)],[p128]) ).
cnf(p130,plain,
( ~ spl2
| member(sk0(sk2,sk3),sk2) ),
inference(resolution,[status(thm)],[p18,c3]) ).
cnf(p136,plain,
( ~ spl2
| ~ member(sk0(sk2,sk3),X0)
| intersect(sk2,X0) ),
inference(resolution,[status(thm)],[p130,c5]) ).
cnf(c4,plain,
( member(sk0(X0,X1),X1)
| ~ intersect(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(p131,plain,
( ~ spl2
| member(sk0(sk2,sk3),sk3) ),
inference(resolution,[status(thm)],[p18,c4]) ).
fof(f0,axiom,
! [B,C,D] :
( member(D,union(B,C))
<=> ( member(D,C)
| member(D,B) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',union_defn) ).
fof(f0_nnf,plain,
! [B,C,D] :
( ( ( ~ member(D,C)
& ~ member(D,B) )
| member(D,union(B,C)) )
& ( member(D,C)
| member(D,B)
| ~ member(D,union(B,C)) ) ),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [D,B,C] :
( ( ( ~ member(D,C)
& ~ member(D,B) )
| member(D,union(B,C)) )
& ( member(D,C)
| member(D,B)
| ~ member(D,union(B,C)) ) ),
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c1,plain,
( ~ member(X2,X0)
| member(X2,union(X0,X1)) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p137,plain,
( ~ spl2
| member(sk0(sk2,sk3),union(sk3,X0)) ),
inference(resolution,[status(thm)],[p131,c1]) ).
cnf(p898,plain,
( ~ spl2
| intersect(sk2,union(sk3,X0)) ),
inference(resolution,[status(thm)],[p136,p137]) ).
cnf(p906,plain,
( ~ spl2
| ~ spl1
| $false ),
inference(resolution,[status(thm)],[p898,p16]) ).
cnf(sct5,plain,
( ~ spl2
| ~ spl1 ),
inference(avatar_contradiction_clause,[status(thm)],[p906]) ).
cnf(p908,plain,
( ~ spl3
| member(sk0(sk2,sk4),sk2) ),
inference(resolution,[status(thm)],[p19,c3]) ).
cnf(p927,plain,
( ~ spl3
| ~ member(sk0(sk2,sk4),X0)
| intersect(sk2,X0) ),
inference(resolution,[status(thm)],[p908,c5]) ).
cnf(p909,plain,
( ~ spl3
| member(sk0(sk2,sk4),sk4) ),
inference(resolution,[status(thm)],[p19,c4]) ).
cnf(c2,plain,
( ~ member(X2,X1)
| member(X2,union(X0,X1)) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p943,plain,
( ~ spl3
| member(sk0(sk2,sk4),union(X0,sk4)) ),
inference(resolution,[status(thm)],[p909,c2]) ).
cnf(p2380,plain,
( ~ spl3
| intersect(sk2,union(X0,sk4)) ),
inference(resolution,[status(thm)],[p927,p943]) ).
cnf(p2397,plain,
( ~ spl3
| ~ spl1
| $false ),
inference(resolution,[status(thm)],[p2380,p16]) ).
cnf(sct6,plain,
( ~ spl3
| ~ spl1 ),
inference(avatar_contradiction_clause,[status(thm)],[p2397]) ).
fof(f5,conjecture,
! [B,C,D] :
( intersect(B,union(C,D))
<=> ( intersect(B,D)
| intersect(B,C) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_intersect_with_union) ).
fof(f5_neg,negated_conjecture,
~ ! [B,C,D] :
( intersect(B,union(C,D))
<=> ( intersect(B,D)
| intersect(B,C) ) ),
inference(negated_conjecture,[status(cth)],[f5]) ).
fof(f5_nnf,plain,
? [B,C,D] :
( ( ( intersect(B,D)
| intersect(B,C) )
& ~ intersect(B,union(C,D)) )
| ( ~ intersect(B,D)
& ~ intersect(B,C)
& intersect(B,union(C,D)) ) ),
inference(nnf_transformation,[status(thm)],[f5_neg]) ).
fof(f5_sk,plain,
( ( ( intersect(sk2,sk4)
| intersect(sk2,sk3) )
& ~ intersect(sk2,union(sk3,sk4)) )
| ( ~ intersect(sk2,sk4)
& ~ intersect(sk2,sk3)
& intersect(sk2,union(sk3,sk4)) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk2,sk3,sk4])],[f5_nnf]) ).
cnf(c14,plain,
( ~ intersect(sk2,union(sk3,sk4))
| intersect(sk2,union(sk3,sk4)) ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(ssp0,plain,
( spl1
| spl0 ),
inference(avatar_split_clause,[status(thm)],[c14,sdef0,sdef1]) ).
cnf(c15,plain,
( intersect(sk2,sk4)
| intersect(sk2,sk3)
| intersect(sk2,union(sk3,sk4)) ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(ssp1,plain,
( spl3
| spl2
| spl0 ),
inference(avatar_split_clause,[status(thm)],[c15,sdef0,sdef2,sdef3]) ).
cnf(c16,plain,
( ~ intersect(sk2,union(sk3,sk4))
| ~ intersect(sk2,sk3) ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(ssp2,plain,
( spl4
| spl1 ),
inference(avatar_split_clause,[status(thm)],[c16,sdef1,sdef4]) ).
cnf(c17,plain,
( intersect(sk2,sk4)
| intersect(sk2,sk3)
| ~ intersect(sk2,sk3) ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(ssp3,plain,
( spl4
| spl3
| spl2 ),
inference(avatar_split_clause,[status(thm)],[c17,sdef2,sdef3,sdef4]) ).
cnf(c18,plain,
( ~ intersect(sk2,union(sk3,sk4))
| ~ intersect(sk2,sk4) ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(ssp4,plain,
( spl5
| spl1 ),
inference(avatar_split_clause,[status(thm)],[c18,sdef1,sdef5]) ).
cnf(c19,plain,
( intersect(sk2,sk4)
| intersect(sk2,sk3)
| ~ intersect(sk2,sk4) ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(ssp5,plain,
( spl5
| spl3
| spl2 ),
inference(avatar_split_clause,[status(thm)],[c19,sdef2,sdef3,sdef5]) ).
fof(f3,axiom,
! [B,C] :
( intersect(B,C)
=> intersect(C,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',symmetry_of_intersect) ).
fof(f3_nnf,plain,
! [B,C] :
( intersect(C,B)
| ~ intersect(B,C) ),
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
! [B,C] :
( intersect(C,B)
| ~ intersect(B,C) ),
inference(skolemisation,[status(esa)],[f3_nnf]) ).
cnf(c7,plain,
( intersect(X1,X0)
| ~ intersect(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p30,plain,
( ~ spl0
| intersect(union(sk3,sk4),sk2) ),
inference(resolution,[status(thm)],[c7,p15]) ).
cnf(p32,plain,
( ~ spl0
| member(sk0(union(sk3,sk4),sk2),union(sk3,sk4)) ),
inference(resolution,[status(thm)],[c3,p30]) ).
cnf(c0,plain,
( member(X2,X1)
| member(X2,X0)
| ~ member(X2,union(X0,X1)) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p39,plain,
( ~ spl0
| member(sk0(union(sk3,sk4),sk2),sk4)
| member(sk0(union(sk3,sk4),sk2),sk3) ),
inference(resolution,[status(thm)],[p32,c0]) ).
fof(sdef6,definition,
( spl6
<=> member(sk0(union(sk3,sk4),sk2),sk3) ),
introduced(definition,[new_symbols(naming,[spl6])],[avatar_definition]) ).
fof(sdef7,definition,
( spl7
<=> member(sk0(union(sk3,sk4),sk2),sk4) ),
introduced(definition,[new_symbols(naming,[spl7])],[avatar_definition]) ).
cnf(ssp6,plain,
( spl7
| spl6
| ~ spl0 ),
inference(avatar_split_clause,[status(thm)],[p39,sdef6,sdef7]) ).
cnf(p33,plain,
( ~ spl0
| member(sk0(sk2,union(sk3,sk4)),union(sk3,sk4)) ),
inference(resolution,[status(thm)],[c4,p15]) ).
cnf(p54,plain,
( ~ spl0
| member(sk0(sk2,union(sk3,sk4)),sk4)
| member(sk0(sk2,union(sk3,sk4)),sk3) ),
inference(resolution,[status(thm)],[p33,c0]) ).
cnf(ssp7,plain,
( spl9
| spl8
| ~ spl0 ),
inference(avatar_split_clause,[status(thm)],[p54,sdef8,sdef9]) ).
cnf(sat_ref,plain,
$false,
inference(avatar_sat_refutation,[status(thm)],[ssp0,ssp1,ssp2,ssp3,ssp4,ssp5,ssp6,ssp7,sct0,sct1,sct2,sct3,sct4,sct5,sct6]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SET624+3 : TPTP v9.3.1. Released v2.2.0.
% 0.00/0.06 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.16/0.42 % Computer : n015.cluster.edu
% 0.16/0.42 % Model : x86_64 x86_64
% 0.16/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.42 % Memory : 8046.5625MB
% 0.16/0.42 % OS : Linux 6.8.0-71-generic
% 0.16/0.42 % CPULimit : 300
% 0.16/0.42 % WCLimit : 300
% 0.16/0.42 % DateTime : Thu Sep 24 11:32:56 UTC 2026
% 0.16/0.42 % CPUTime :
% 0.16/0.42 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 39.30/5.48 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 39.30/5.48 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------