%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SET679+3 : TPTP v9.3.1. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 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 : Fri Sep 25 02:43:47 PM UTC 2026
% Result : Theorem 7.91s 1.62s
% Output : Proof 7.91s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 12
% Syntax : Number of formulae : 90 ( 64 unt; 0 def)
% Number of atoms : 164 ( 64 equ)
% Maximal formula atoms : 7 ( 1 avg)
% Number of connectives : 139 ( 65 ~; 44 |; 17 &)
% ( 3 <=>; 10 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 2 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 5 con; 0-4 aty)
% Number of variables : 95 ( 15 sgn 29 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f0,axiom,
! [B] :
( ilf_type(B,set_type)
=> ! [C] :
( ilf_type(C,set_type)
=> ( member(C,B)
<=> member(ordered_pair(C,C),identity_relation_of(B)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p1) ).
fof(f0_nnf,plain,
! [B] :
( ! [C] :
( ( ( ~ member(ordered_pair(C,C),identity_relation_of(B))
| member(C,B) )
& ( member(ordered_pair(C,C),identity_relation_of(B))
| ~ member(C,B) ) )
| ~ ilf_type(C,set_type) )
| ~ ilf_type(B,set_type) ),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [B,C] :
( ( ( ~ member(ordered_pair(C,C),identity_relation_of(B))
| member(C,B) )
& ( member(ordered_pair(C,C),identity_relation_of(B))
| ~ member(C,B) ) )
| ~ ilf_type(C,set_type)
| ~ ilf_type(B,set_type) ),
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
( member(ordered_pair(X1,X1),identity_relation_of(X0))
| ~ member(X1,X0)
| ~ ilf_type(X1,set_type)
| ~ ilf_type(X0,set_type) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(t67,plain,
ifeq(ilf_type(X1,set_type),true,ifeq(ilf_type(X2,set_type),true,ifeq(member(X2,X1),true,member(ordered_pair(X2,X2),identity_relation_of(X1)),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c0]) ).
cnf(t102,plain,
ifeq(ilf_type(X1,set_type),true,ifeq(ilf_type(X2,set_type),true,ifeq(member(X2,X1),true,member(ordered_pair(X2,X2),identity_relation_of(X1)),true),true),true) = true,
inference(orient,[status(thm)],[t67]) ).
fof(f22,axiom,
! [B] : ilf_type(B,set_type),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p22) ).
fof(f22_nnf,plain,
! [B] : ilf_type(B,set_type),
inference(nnf_transformation,[status(thm)],[f22]) ).
fof(f22_sk,plain,
! [B] : ilf_type(B,set_type),
inference(skolemisation,[status(esa)],[f22_nnf]) ).
cnf(c47,plain,
ilf_type(X0,set_type),
inference(cnf_transformation,[status(esa)],[f22_sk]) ).
cnf(t7,plain,
ilf_type(X1,set_type) = true,
inference(equality_encoding,[status(esa)],[c47]) ).
cnf(t139,plain,
ilf_type(X1,set_type) = true,
inference(orient,[status(thm)],[t7]) ).
cnf(t412,plain,
ifeq(true,true,ifeq(ilf_type(X2,set_type),true,ifeq(member(X2,X1),true,member(ordered_pair(X2,X2),identity_relation_of(X1)),true),true),true) = true,
inference(step,[status(thm)],[t102,t139]) ).
cnf(t19,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t84,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t19]) ).
cnf(t413,plain,
ifeq(ilf_type(X2,set_type),true,ifeq(member(X2,X1),true,member(ordered_pair(X2,X2),identity_relation_of(X1)),true),true) = true,
inference(step,[status(thm)],[t412,t84]) ).
cnf(t414,plain,
ifeq(true,true,ifeq(member(X2,X1),true,member(ordered_pair(X2,X2),identity_relation_of(X1)),true),true) = true,
inference(step,[status(thm)],[t413,t139]) ).
cnf(t415,plain,
ifeq(member(X2,X1),true,member(ordered_pair(X2,X2),identity_relation_of(X1)),true) = true,
inference(step,[status(thm)],[t414,t84]) ).
cnf(t161,plain,
ifeq(member(X2,X1),true,member(ordered_pair(X2,X2),identity_relation_of(X1)),true) = true,
inference(rw,[status(thm)],[t415]) ).
cnf(t320,plain,
ifeq(member(X1,X2),true,member(ordered_pair(X1,X1),identity_relation_of(X2)),true) = true,
inference(orient,[status(thm)],[t161]) ).
fof(f8,axiom,
! [B] :
( ilf_type(B,set_type)
=> ( empty(B)
<=> ! [C] :
( ilf_type(C,set_type)
=> ~ member(C,B) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p8) ).
fof(f8_nnf,plain,
! [B] :
( ( ( ? [C] :
( member(C,B)
& ilf_type(C,set_type) )
| empty(B) )
& ( ! [C] :
( ~ member(C,B)
| ~ ilf_type(C,set_type) )
| ~ empty(B) ) )
| ~ ilf_type(B,set_type) ),
inference(nnf_transformation,[status(thm)],[f8]) ).
fof(f8_sk,plain,
! [B,C] :
( ( ( ( member(sk1(B),B)
& ilf_type(sk1(B),set_type) )
| empty(B) )
& ( ~ member(C,B)
| ~ ilf_type(C,set_type)
| ~ empty(B) ) )
| ~ ilf_type(B,set_type) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk1])],[f8_nnf]) ).
cnf(c20,plain,
( member(sk1(X0),X0)
| empty(X0)
| ~ ilf_type(X0,set_type) ),
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
cnf(hi15,axiom,
ifeq(ilf_type(X0,set_type),true,or(empty(X0),member(sk1(X0),X0)),true) = true,
inference(equality_encoding,[status(esa)],[c20]) ).
cnf(hi40,axiom,
ilf_type(X0,set_type) = true,
inference(equality_encoding,[status(esa)],[c47]) ).
cnf(t28,plain,
or(empty(X1),member(sk1(X1),X1)) = true,
inference(hyper_resolution,[status(thm)],[hi15,hi40]) ).
cnf(t187,plain,
or(empty(X1),member(sk1(X1),X1)) = true,
inference(orient,[status(thm)],[t28]) ).
fof(f23,conjecture,
! [B] :
( ( ilf_type(B,set_type)
& ~ empty(B) )
=> not_equal(identity_relation_of(B),empty_set) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_relset_1_46) ).
fof(f23_neg,negated_conjecture,
~ ! [B] :
( ( ilf_type(B,set_type)
& ~ empty(B) )
=> not_equal(identity_relation_of(B),empty_set) ),
inference(negated_conjecture,[status(cth)],[f23]) ).
fof(f23_nnf,plain,
? [B] :
( ~ not_equal(identity_relation_of(B),empty_set)
& ilf_type(B,set_type)
& ~ empty(B) ),
inference(nnf_transformation,[status(thm)],[f23_neg]) ).
fof(f23_sk,plain,
( ~ not_equal(identity_relation_of(sk9),empty_set)
& ilf_type(sk9,set_type)
& ~ empty(sk9) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk9])],[f23_nnf]) ).
cnf(c48,plain,
~ empty(sk9),
inference(cnf_transformation,[status(esa)],[f23_sk]) ).
cnf(t1,plain,
empty(sk9) = false,
inference(equality_encoding,[status(esa)],[c48]) ).
cnf(t211,plain,
empty(sk9) = false,
inference(orient,[status(thm)],[t1]) ).
cnf(t212,plain,
true = or(false,member(sk1(sk9),sk9)),
inference(cp,[status(thm)],[t187,t211]) ).
cnf(t13,plain,
or(false,X1) = X1,
introduced(definition) ).
cnf(t89,plain,
or(false,X1) = X1,
inference(orient,[status(thm)],[t13]) ).
cnf(t514,plain,
true = member(sk1(sk9),sk9),
inference(step,[status(thm)],[t212,t89]) ).
cnf(t224,plain,
member(sk1(sk9),sk9) = true,
inference(orient,[status(thm)],[t514]) ).
cnf(t323,plain,
true = ifeq(true,true,member(ordered_pair(sk1(sk9),sk1(sk9)),identity_relation_of(sk9)),true),
inference(cp,[status(thm)],[t320,t224]) ).
cnf(t532,plain,
true = member(ordered_pair(sk1(sk9),sk1(sk9)),identity_relation_of(sk9)),
inference(step,[status(thm)],[t323,t84]) ).
cnf(t26,plain,
ifeq(eq(X1,X2),true,X1,X2) = X2,
introduced(definition) ).
cnf(t87,plain,
ifeq(eq(X1,X2),true,X1,X2) = X2,
inference(orient,[status(thm)],[t26]) ).
fof(f7,axiom,
! [B] :
( ilf_type(B,set_type)
=> ! [C] :
( ilf_type(C,set_type)
=> ( not_equal(B,C)
<=> B != C ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p7) ).
fof(f7_nnf,plain,
! [B] :
( ! [C] :
( ( ( B = C
| not_equal(B,C) )
& ( B != C
| ~ not_equal(B,C) ) )
| ~ ilf_type(C,set_type) )
| ~ ilf_type(B,set_type) ),
inference(nnf_transformation,[status(thm)],[f7]) ).
fof(f7_sk,plain,
! [B,C] :
( ( ( B = C
| not_equal(B,C) )
& ( B != C
| ~ not_equal(B,C) ) )
| ~ ilf_type(C,set_type)
| ~ ilf_type(B,set_type) ),
inference(skolemisation,[status(esa)],[f7_nnf]) ).
cnf(c17,plain,
( X0 = X1
| not_equal(X0,X1)
| ~ ilf_type(X1,set_type)
| ~ ilf_type(X0,set_type) ),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(hi13,axiom,
ifeq(ilf_type(X0,set_type),true,ifeq(ilf_type(X1,set_type),true,or(not_equal(X0,X1),eq(X0,X1)),true),true) = true,
inference(equality_encoding,[status(esa)],[c17]) ).
cnf(t29,plain,
or(not_equal(X1,X2),eq(X1,X2)) = true,
inference(hyper_resolution,[status(thm)],[hi13,hi40,hi40]) ).
cnf(t195,plain,
or(not_equal(X1,X2),eq(X1,X2)) = true,
inference(orient,[status(thm)],[t29]) ).
cnf(c50,plain,
~ not_equal(identity_relation_of(sk9),empty_set),
inference(cnf_transformation,[status(esa)],[f23_sk]) ).
cnf(t18,plain,
not_equal(identity_relation_of(sk9),empty_set) = false,
inference(equality_encoding,[status(esa)],[c50]) ).
cnf(t221,plain,
not_equal(identity_relation_of(sk9),empty_set) = false,
inference(orient,[status(thm)],[t18]) ).
cnf(t222,plain,
true = or(false,eq(identity_relation_of(sk9),empty_set)),
inference(cp,[status(thm)],[t195,t221]) ).
cnf(t519,plain,
true = eq(identity_relation_of(sk9),empty_set),
inference(step,[status(thm)],[t222,t89]) ).
cnf(t239,plain,
eq(identity_relation_of(sk9),empty_set) = true,
inference(orient,[status(thm)],[t519]) ).
cnf(t240,plain,
empty_set = ifeq(true,true,identity_relation_of(sk9),empty_set),
inference(cp,[status(thm)],[t87,t239]) ).
cnf(t520,plain,
empty_set = identity_relation_of(sk9),
inference(step,[status(thm)],[t240,t84]) ).
cnf(t241,plain,
identity_relation_of(sk9) = empty_set,
inference(orient,[status(thm)],[t520]) ).
cnf(t533,plain,
true = member(ordered_pair(sk1(sk9),sk1(sk9)),empty_set),
inference(step,[status(thm)],[t532,t241]) ).
cnf(t23,plain,
ifeq(not(X1),true,X1,false) = false,
introduced(definition) ).
cnf(t210,plain,
ifeq(not(X1),true,X1,false) = false,
inference(orient,[status(thm)],[t23]) ).
fof(f1,axiom,
! [B] :
( ilf_type(B,set_type)
=> ~ member(B,empty_set) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p2) ).
fof(f1_nnf,plain,
! [B] :
( ~ member(B,empty_set)
| ~ ilf_type(B,set_type) ),
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [B] :
( ~ member(B,empty_set)
| ~ ilf_type(B,set_type) ),
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c2,plain,
( ~ member(X0,empty_set)
| ~ ilf_type(X0,set_type) ),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(t37,plain,
or(not(ilf_type(X1,set_type)),not(member(X1,empty_set))) = true,
inference(equality_encoding,[status(esa)],[c2]) ).
cnf(t494,plain,
or(not(true),not(member(X1,empty_set))) = true,
inference(step,[status(thm)],[t37,t139]) ).
cnf(t192,plain,
or(not(true),not(member(X1,empty_set))) = true,
inference(orient,[status(thm)],[t494]) ).
cnf(t3,plain,
not(true) = false,
introduced(definition) ).
cnf(t215,plain,
not(true) = false,
inference(orient,[status(thm)],[t3]) ).
cnf(t501,plain,
or(false,not(member(X1,empty_set))) = true,
inference(step,[status(thm)],[t192,t215]) ).
cnf(t502,plain,
not(member(X1,empty_set)) = true,
inference(step,[status(thm)],[t501,t89]) ).
cnf(t217,plain,
not(member(X1,empty_set)) = true,
inference(rw,[status(thm)],[t502]) ).
cnf(t226,plain,
not(member(X1,empty_set)) = true,
inference(orient,[status(thm)],[t217]) ).
cnf(t227,plain,
false = ifeq(true,true,member(X1,empty_set),false),
inference(cp,[status(thm)],[t210,t226]) ).
cnf(t515,plain,
false = member(X1,empty_set),
inference(step,[status(thm)],[t227,t84]) ).
cnf(t228,plain,
member(X1,empty_set) = false,
inference(orient,[status(thm)],[t515]) ).
cnf(t534,plain,
true = false,
inference(step,[status(thm)],[t533,t228]) ).
cnf(t326,plain,
false = true,
inference(orient,[status(thm)],[t534]) ).
cnf(c16,plain,
( X0 != X1
| ~ not_equal(X0,X1)
| ~ ilf_type(X1,set_type)
| ~ ilf_type(X0,set_type) ),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(c18,plain,
( ~ member(X1,X0)
| ~ ilf_type(X1,set_type)
| ~ empty(X0)
| ~ ilf_type(X0,set_type) ),
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
fof(f19,axiom,
! [B] :
( ilf_type(B,set_type)
=> ( ilf_type(power_set(B),set_type)
& ~ empty(power_set(B)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p19) ).
fof(f19_nnf,plain,
! [B] :
( ( ilf_type(power_set(B),set_type)
& ~ empty(power_set(B)) )
| ~ ilf_type(B,set_type) ),
inference(nnf_transformation,[status(thm)],[f19]) ).
fof(f19_sk,plain,
! [B] :
( ( ilf_type(power_set(B),set_type)
& ~ empty(power_set(B)) )
| ~ ilf_type(B,set_type) ),
inference(skolemisation,[status(esa)],[f19_nnf]) ).
cnf(c42,plain,
( ~ empty(power_set(X0))
| ~ ilf_type(X0,set_type) ),
inference(cnf_transformation,[status(esa)],[f19_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c2,c16,c18,c42,c48,c50]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t326]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SET679+3 : TPTP v9.3.1. Released v2.2.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.08/0.35 % Computer : n007.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 : Thu Sep 24 11:36:52 UTC 2026
% 0.12/0.36 % CPUTime :
% 0.12/0.36 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 7.91/1.62 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 7.91/1.62 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------