%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SEU217+2 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n014.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:51:22 PM UTC 2026
% Result : Theorem 60.28s 8.08s
% Output : Proof 60.28s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 27
% Syntax : Number of formulae : 132 ( 66 unt; 0 def)
% Number of atoms : 292 ( 79 equ)
% Maximal formula atoms : 14 ( 2 avg)
% Number of connectives : 333 ( 173 ~; 89 |; 58 &)
% ( 6 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of predicates : 10 ( 8 usr; 1 prp; 0-2 aty)
% Number of functors : 24 ( 24 usr; 7 con; 0-4 aty)
% Number of variables : 229 ( 22 sgn 141 !; 13 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f164,conjecture,
! [A,B] :
( in(B,A)
=> apply(identity_relation(A),B) = B ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t35_funct_1) ).
fof(f164_neg,negated_conjecture,
~ ! [A,B] :
( in(B,A)
=> apply(identity_relation(A),B) = B ),
inference(negated_conjecture,[status(cth)],[f164]) ).
fof(f164_nnf,plain,
? [A,B] :
( apply(identity_relation(A),B) != B
& in(B,A) ),
inference(nnf_transformation,[status(thm)],[f164_neg]) ).
fof(f164_sk,plain,
( apply(identity_relation(sk66),sk67) != sk67
& in(sk67,sk66) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk66,sk67])],[f164_nnf]) ).
cnf(c376,plain,
apply(identity_relation(sk66),sk67) != sk67,
inference(cnf_transformation,[status(esa)],[f164_sk]) ).
cnf(t121,plain,
eq(apply(identity_relation(sk66),sk67),sk67) = false,
inference(equality_encoding,[status(esa)],[c376]) ).
cnf(t2059,plain,
eq(apply(identity_relation(sk66),sk67),sk67) = false,
inference(orient,[status(thm)],[t121]) ).
fof(f163,lemma,
! [A,B] :
( ( function(B)
& relation(B) )
=> ( B = identity_relation(A)
<=> ( ! [C] :
( in(C,A)
=> apply(B,C) = C )
& relation_dom(B) = A ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t34_funct_1) ).
fof(f163_nnf,plain,
! [A,B] :
( ( ( ? [C] :
( apply(B,C) != C
& in(C,A) )
| relation_dom(B) != A
| B = identity_relation(A) )
& ( ( ! [C] :
( apply(B,C) = C
| ~ in(C,A) )
& relation_dom(B) = A )
| B != identity_relation(A) ) )
| ~ function(B)
| ~ relation(B) ),
inference(nnf_transformation,[status(thm)],[f163]) ).
fof(f163_sk,plain,
! [B,A,C] :
( ( ( ( apply(B,sk65(A,B)) != sk65(A,B)
& in(sk65(A,B),A) )
| relation_dom(B) != A
| B = identity_relation(A) )
& ( ( ( apply(B,C) = C
| ~ in(C,A) )
& relation_dom(B) = A )
| B != identity_relation(A) ) )
| ~ function(B)
| ~ relation(B) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk65])],[f163_nnf]) ).
cnf(c372,plain,
( apply(X1,X2) = X2
| ~ in(X2,X0)
| X1 != identity_relation(X0)
| ~ function(X1)
| ~ relation(X1) ),
inference(cnf_transformation,[status(esa)],[f163_sk]) ).
cnf(t217,plain,
ifeq(relation(X1),true,ifeq(function(X1),true,ifeq(X1,identity_relation(X2),ifeq(in(X3,X2),true,apply(X1,X3),X3),X3),X3),X3) = X3,
inference(equality_encoding,[status(esa)],[c372]) ).
cnf(t242,plain,
ifeq(relation(X1),true,ifeq(function(X1),true,ifeq(X1,identity_relation(X2),ifeq(in(X3,X2),true,apply(X1,X3),X3),X3),X3),X3) = X3,
inference(orient,[status(thm)],[t217]) ).
cnf(t106,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t239,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t106]) ).
cnf(t243,plain,
X1 = ifeq(relation(identity_relation(X2)),true,ifeq(function(identity_relation(X2)),true,ifeq(in(X1,X2),true,apply(identity_relation(X2),X1),X1),X1),X1),
inference(cp,[status(thm)],[t242,t239]) ).
fof(f61,axiom,
! [A] : relation(identity_relation(A)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k6_relat_1) ).
fof(f61_nnf,plain,
! [A] : relation(identity_relation(A)),
inference(nnf_transformation,[status(thm)],[f61]) ).
fof(f61_sk,plain,
! [A] : relation(identity_relation(A)),
inference(skolemisation,[status(esa)],[f61_nnf]) ).
cnf(c224,plain,
relation(identity_relation(X0)),
inference(cnf_transformation,[status(esa)],[f61_sk]) ).
cnf(t51,plain,
relation(identity_relation(X1)) = true,
inference(equality_encoding,[status(esa)],[c224]) ).
cnf(t1186,plain,
relation(identity_relation(X1)) = true,
inference(orient,[status(thm)],[t51]) ).
cnf(t2888,plain,
X1 = ifeq(true,true,ifeq(function(identity_relation(X2)),true,ifeq(in(X1,X2),true,apply(identity_relation(X2),X1),X1),X1),X1),
inference(step,[status(thm)],[t243,t1186]) ).
cnf(t2889,plain,
X1 = ifeq(function(identity_relation(X2)),true,ifeq(in(X1,X2),true,apply(identity_relation(X2),X1),X1),X1),
inference(step,[status(thm)],[t2888,t239]) ).
fof(f77,axiom,
! [A] :
( function(identity_relation(A))
& relation(identity_relation(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc2_funct_1) ).
fof(f77_nnf,plain,
! [A] :
( function(identity_relation(A))
& relation(identity_relation(A)) ),
inference(nnf_transformation,[status(thm)],[f77]) ).
fof(f77_sk,plain,
! [A] :
( function(identity_relation(A))
& relation(identity_relation(A)) ),
inference(skolemisation,[status(esa)],[f77_nnf]) ).
cnf(c245,plain,
function(identity_relation(X0)),
inference(cnf_transformation,[status(esa)],[f77_sk]) ).
cnf(t43,plain,
function(identity_relation(X1)) = true,
inference(equality_encoding,[status(esa)],[c245]) ).
cnf(t1521,plain,
function(identity_relation(X1)) = true,
inference(orient,[status(thm)],[t43]) ).
cnf(t2890,plain,
X1 = ifeq(true,true,ifeq(in(X1,X2),true,apply(identity_relation(X2),X1),X1),X1),
inference(step,[status(thm)],[t2889,t1521]) ).
cnf(t2891,plain,
X1 = ifeq(in(X1,X2),true,apply(identity_relation(X2),X1),X1),
inference(step,[status(thm)],[t2890,t239]) ).
cnf(t2646,plain,
ifeq(in(X1,X2),true,apply(identity_relation(X2),X1),X1) = X1,
inference(orient,[status(thm)],[t2891]) ).
cnf(c375,plain,
in(sk67,sk66),
inference(cnf_transformation,[status(esa)],[f164_sk]) ).
cnf(t46,plain,
in(sk67,sk66) = true,
inference(equality_encoding,[status(esa)],[c375]) ).
cnf(t795,plain,
in(sk67,sk66) = true,
inference(orient,[status(thm)],[t46]) ).
cnf(t2664,plain,
sk67 = ifeq(true,true,apply(identity_relation(sk66),sk67),sk67),
inference(cp,[status(thm)],[t2646,t795]) ).
cnf(t2892,plain,
sk67 = apply(identity_relation(sk66),sk67),
inference(step,[status(thm)],[t2664,t239]) ).
cnf(t2668,plain,
apply(identity_relation(sk66),sk67) = sk67,
inference(orient,[status(thm)],[t2892]) ).
cnf(t2894,plain,
eq(sk67,sk67) = false,
inference(step,[status(thm)],[t2059,t2668]) ).
cnf(t42,plain,
eq(X1,X1) = true,
introduced(definition) ).
cnf(t1668,plain,
eq(X1,X1) = true,
inference(orient,[status(thm)],[t42]) ).
cnf(t2895,plain,
true = false,
inference(step,[status(thm)],[t2894,t1668]) ).
cnf(t2691,plain,
true = false,
inference(rw,[status(thm)],[t2895]) ).
cnf(t2693,plain,
false = true,
inference(orient,[status(thm)],[t2691]) ).
fof(f0,axiom,
! [A,B] :
( in(A,B)
=> ~ in(B,A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',antisymmetry_r2_hidden) ).
fof(f0_nnf,plain,
! [A,B] :
( ~ in(B,A)
| ~ in(A,B) ),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [A,B] :
( ~ in(B,A)
| ~ in(A,B) ),
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
( ~ in(X1,X0)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
fof(f1,axiom,
! [A,B] :
( proper_subset(A,B)
=> ~ proper_subset(B,A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',antisymmetry_r2_xboole_0) ).
fof(f1_nnf,plain,
! [A,B] :
( ~ proper_subset(B,A)
| ~ proper_subset(A,B) ),
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [A,B] :
( ~ proper_subset(B,A)
| ~ proper_subset(A,B) ),
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c1,plain,
( ~ proper_subset(X1,X0)
| ~ proper_subset(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
fof(f16,axiom,
! [A] :
( A = empty_set
<=> ! [B] : ~ in(B,A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d1_xboole_0) ).
fof(f16_nnf,plain,
! [A] :
( ( ? [B] : in(B,A)
| A = empty_set )
& ( ! [B] : ~ in(B,A)
| A != empty_set ) ),
inference(nnf_transformation,[status(thm)],[f16]) ).
fof(f16_sk,plain,
! [A,B] :
( ( in(sk19(A),A)
| A = empty_set )
& ( ~ in(B,A)
| A != empty_set ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk19])],[f16_nnf]) ).
cnf(c75,plain,
( ~ in(X1,X0)
| X0 != empty_set ),
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
fof(f30,axiom,
! [A,B,C] :
( C = set_difference(A,B)
<=> ! [D] :
( in(D,C)
<=> ( ~ in(D,B)
& in(D,A) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d4_xboole_0) ).
fof(f30_nnf,plain,
! [A,B,C] :
( ( ? [D] :
( ( ~ in(D,B)
& in(D,A)
& ~ in(D,C) )
| ( ( in(D,B)
| ~ in(D,A) )
& in(D,C) ) )
| C = set_difference(A,B) )
& ( ! [D] :
( ( in(D,B)
| ~ in(D,A)
| in(D,C) )
& ( ( ~ in(D,B)
& in(D,A) )
| ~ in(D,C) ) )
| C != set_difference(A,B) ) ),
inference(nnf_transformation,[status(thm)],[f30]) ).
fof(f30_sk,plain,
! [C,A,B,D] :
( ( ( ~ in(sk40(A,B,C),B)
& in(sk40(A,B,C),A)
& ~ in(sk40(A,B,C),C) )
| ( ( in(sk40(A,B,C),B)
| ~ in(sk40(A,B,C),A) )
& in(sk40(A,B,C),C) )
| C = set_difference(A,B) )
& ( ( ( in(D,B)
| ~ in(D,A)
| in(D,C) )
& ( ( ~ in(D,B)
& in(D,A) )
| ~ in(D,C) ) )
| C != set_difference(A,B) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk40])],[f30_nnf]) ).
cnf(c159,plain,
( ~ in(X3,X1)
| ~ in(X3,X2)
| X2 != set_difference(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f30_sk]) ).
fof(f39,axiom,
! [A,B] :
( proper_subset(A,B)
<=> ( A != B
& subset(A,B) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d8_xboole_0) ).
fof(f39_nnf,plain,
! [A,B] :
( ( A = B
| ~ subset(A,B)
| proper_subset(A,B) )
& ( ( A != B
& subset(A,B) )
| ~ proper_subset(A,B) ) ),
inference(nnf_transformation,[status(thm)],[f39]) ).
fof(f39_sk,plain,
! [A,B] :
( ( A = B
| ~ subset(A,B)
| proper_subset(A,B) )
& ( ( A != B
& subset(A,B) )
| ~ proper_subset(A,B) ) ),
inference(skolemisation,[status(esa)],[f39_nnf]) ).
cnf(c201,plain,
( X0 != X1
| ~ proper_subset(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f39_sk]) ).
fof(f74,axiom,
! [A] : ~ empty(powerset(A)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_subset_1) ).
fof(f74_nnf,plain,
! [A] : ~ empty(powerset(A)),
inference(nnf_transformation,[status(thm)],[f74]) ).
fof(f74_sk,plain,
! [A] : ~ empty(powerset(A)),
inference(skolemisation,[status(esa)],[f74_nnf]) ).
cnf(c241,plain,
~ empty(powerset(X0)),
inference(cnf_transformation,[status(esa)],[f74_sk]) ).
fof(f76,axiom,
! [A,B] : ~ empty(ordered_pair(A,B)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_zfmisc_1) ).
fof(f76_nnf,plain,
! [A,B] : ~ empty(ordered_pair(A,B)),
inference(nnf_transformation,[status(thm)],[f76]) ).
fof(f76_sk,plain,
! [A,B] : ~ empty(ordered_pair(A,B)),
inference(skolemisation,[status(esa)],[f76_nnf]) ).
cnf(c243,plain,
~ empty(ordered_pair(X0,X1)),
inference(cnf_transformation,[status(esa)],[f76_sk]) ).
fof(f79,axiom,
! [A] : ~ empty(singleton(A)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc2_subset_1) ).
fof(f79_nnf,plain,
! [A] : ~ empty(singleton(A)),
inference(nnf_transformation,[status(thm)],[f79]) ).
fof(f79_sk,plain,
! [A] : ~ empty(singleton(A)),
inference(skolemisation,[status(esa)],[f79_nnf]) ).
cnf(c247,plain,
~ empty(singleton(X0)),
inference(cnf_transformation,[status(esa)],[f79_sk]) ).
fof(f81,axiom,
! [A,B] : ~ empty(unordered_pair(A,B)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc3_subset_1) ).
fof(f81_nnf,plain,
! [A,B] : ~ empty(unordered_pair(A,B)),
inference(nnf_transformation,[status(thm)],[f81]) ).
fof(f81_sk,plain,
! [A,B] : ~ empty(unordered_pair(A,B)),
inference(skolemisation,[status(esa)],[f81_nnf]) ).
cnf(c249,plain,
~ empty(unordered_pair(X0,X1)),
inference(cnf_transformation,[status(esa)],[f81_sk]) ).
fof(f95,axiom,
! [A,B] : ~ proper_subset(A,A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',irreflexivity_r2_xboole_0) ).
fof(f95_nnf,plain,
! [A,B] : ~ proper_subset(A,A),
inference(nnf_transformation,[status(thm)],[f95]) ).
fof(f95_sk,plain,
! [A] : ~ proper_subset(A,A),
inference(skolemisation,[status(esa)],[f95_nnf]) ).
cnf(c267,plain,
~ proper_subset(X0,X0),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
fof(f96,lemma,
! [A] : singleton(A) != empty_set,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',l1_zfmisc_1) ).
fof(f96_nnf,plain,
! [A] : singleton(A) != empty_set,
inference(nnf_transformation,[status(thm)],[f96]) ).
fof(f96_sk,plain,
! [A] : singleton(A) != empty_set,
inference(skolemisation,[status(esa)],[f96_nnf]) ).
cnf(c268,plain,
singleton(X0) != empty_set,
inference(cnf_transformation,[status(esa)],[f96_sk]) ).
fof(f98,lemma,
! [A,B] :
~ ( in(A,B)
& disjoint(singleton(A),B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',l25_zfmisc_1) ).
fof(f98_nnf,plain,
! [A,B] :
( ~ in(A,B)
| ~ disjoint(singleton(A),B) ),
inference(nnf_transformation,[status(thm)],[f98]) ).
fof(f98_sk,plain,
! [A,B] :
( ~ in(A,B)
| ~ disjoint(singleton(A),B) ),
inference(skolemisation,[status(esa)],[f98_nnf]) ).
cnf(c270,plain,
( ~ in(X0,X1)
| ~ disjoint(singleton(X0),X1) ),
inference(cnf_transformation,[status(esa)],[f98_sk]) ).
fof(f112,axiom,
? [A] :
( relation(A)
& ~ empty(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rc2_relat_1) ).
fof(f112_nnf,plain,
? [A] :
( relation(A)
& ~ empty(A) ),
inference(nnf_transformation,[status(thm)],[f112]) ).
fof(f112_sk,plain,
( relation(sk57)
& ~ empty(sk57) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk57])],[f112_nnf]) ).
cnf(c294,plain,
~ empty(sk57),
inference(cnf_transformation,[status(esa)],[f112_sk]) ).
fof(f114,axiom,
? [A] : ~ empty(A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rc2_xboole_0) ).
fof(f114_nnf,plain,
? [A] : ~ empty(A),
inference(nnf_transformation,[status(thm)],[f114]) ).
fof(f114_sk,plain,
~ empty(sk59),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk59])],[f114_nnf]) ).
cnf(c298,plain,
~ empty(sk59),
inference(cnf_transformation,[status(esa)],[f114_sk]) ).
fof(f174,lemma,
! [A,B] :
( ~ ( disjoint(A,B)
& ? [C] :
( in(C,B)
& in(C,A) ) )
& ~ ( ! [C] :
~ ( in(C,B)
& in(C,A) )
& ~ disjoint(A,B) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t3_xboole_0) ).
fof(f174_nnf,plain,
! [A,B] :
( ( ~ disjoint(A,B)
| ! [C] :
( ~ in(C,B)
| ~ in(C,A) ) )
& ( ? [C] :
( in(C,B)
& in(C,A) )
| disjoint(A,B) ) ),
inference(nnf_transformation,[status(thm)],[f174]) ).
fof(f174_sk,plain,
! [A,B,C] :
( ( ~ disjoint(A,B)
| ~ in(C,B)
| ~ in(C,A) )
& ( ( in(sk68(A,B),B)
& in(sk68(A,B),A) )
| disjoint(A,B) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk68])],[f174_nnf]) ).
cnf(c396,plain,
( ~ disjoint(X0,X1)
| ~ in(X2,X1)
| ~ in(X2,X0) ),
inference(cnf_transformation,[status(esa)],[f174_sk]) ).
fof(f190,lemma,
! [A,B] :
( ~ ( disjoint(A,B)
& ? [C] : in(C,set_intersection2(A,B)) )
& ~ ( ! [C] : ~ in(C,set_intersection2(A,B))
& ~ disjoint(A,B) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t4_xboole_0) ).
fof(f190_nnf,plain,
! [A,B] :
( ( ~ disjoint(A,B)
| ! [C] : ~ in(C,set_intersection2(A,B)) )
& ( ? [C] : in(C,set_intersection2(A,B))
| disjoint(A,B) ) ),
inference(nnf_transformation,[status(thm)],[f190]) ).
fof(f190_sk,plain,
! [A,B,C] :
( ( ~ disjoint(A,B)
| ~ in(C,set_intersection2(A,B)) )
& ( in(sk69(A,B),set_intersection2(A,B))
| disjoint(A,B) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk69])],[f190_nnf]) ).
cnf(c414,plain,
( ~ disjoint(X0,X1)
| ~ in(X2,set_intersection2(X0,X1)) ),
inference(cnf_transformation,[status(esa)],[f190_sk]) ).
fof(f192,lemma,
! [A,B,C] :
( element(C,powerset(A))
=> ~ ( in(B,C)
& in(B,subset_complement(A,C)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t54_subset_1) ).
fof(f192_nnf,plain,
! [A,B,C] :
( ~ in(B,C)
| ~ in(B,subset_complement(A,C))
| ~ element(C,powerset(A)) ),
inference(nnf_transformation,[status(thm)],[f192]) ).
fof(f192_sk,plain,
! [C,A,B] :
( ~ in(B,C)
| ~ in(B,subset_complement(A,C))
| ~ element(C,powerset(A)) ),
inference(skolemisation,[status(esa)],[f192_nnf]) ).
cnf(c416,plain,
( ~ in(X1,X2)
| ~ in(X1,subset_complement(X0,X2))
| ~ element(X2,powerset(X0)) ),
inference(cnf_transformation,[status(esa)],[f192_sk]) ).
fof(f194,axiom,
! [A,B,C] :
~ ( empty(C)
& element(B,powerset(C))
& in(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t5_subset) ).
fof(f194_nnf,plain,
! [A,B,C] :
( ~ empty(C)
| ~ element(B,powerset(C))
| ~ in(A,B) ),
inference(nnf_transformation,[status(thm)],[f194]) ).
fof(f194_sk,plain,
! [A,B,C] :
( ~ empty(C)
| ~ element(B,powerset(C))
| ~ in(A,B) ),
inference(skolemisation,[status(esa)],[f194_nnf]) ).
cnf(c418,plain,
( ~ empty(X2)
| ~ element(X1,powerset(X2))
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f194_sk]) ).
fof(f196,lemma,
! [A,B] :
~ ( proper_subset(B,A)
& subset(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t60_xboole_1) ).
fof(f196_nnf,plain,
! [A,B] :
( ~ proper_subset(B,A)
| ~ subset(A,B) ),
inference(nnf_transformation,[status(thm)],[f196]) ).
fof(f196_sk,plain,
! [A,B] :
( ~ proper_subset(B,A)
| ~ subset(A,B) ),
inference(skolemisation,[status(esa)],[f196_nnf]) ).
cnf(c421,plain,
( ~ proper_subset(X1,X0)
| ~ subset(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f196_sk]) ).
fof(f200,lemma,
! [A,B] :
( set_difference(A,singleton(B)) = A
<=> ~ in(B,A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t65_zfmisc_1) ).
fof(f200_nnf,plain,
! [A,B] :
( ( in(B,A)
| set_difference(A,singleton(B)) = A )
& ( ~ in(B,A)
| set_difference(A,singleton(B)) != A ) ),
inference(nnf_transformation,[status(thm)],[f200]) ).
fof(f200_sk,plain,
! [A,B] :
( ( in(B,A)
| set_difference(A,singleton(B)) = A )
& ( ~ in(B,A)
| set_difference(A,singleton(B)) != A ) ),
inference(skolemisation,[status(esa)],[f200_nnf]) ).
cnf(c427,plain,
( ~ in(X1,X0)
| set_difference(X0,singleton(X1)) != X0 ),
inference(cnf_transformation,[status(esa)],[f200_sk]) ).
fof(f206,axiom,
! [A,B] :
~ ( empty(B)
& in(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t7_boole) ).
fof(f206_nnf,plain,
! [A,B] :
( ~ empty(B)
| ~ in(A,B) ),
inference(nnf_transformation,[status(thm)],[f206]) ).
fof(f206_sk,plain,
! [A,B] :
( ~ empty(B)
| ~ in(A,B) ),
inference(skolemisation,[status(esa)],[f206_nnf]) ).
cnf(c437,plain,
( ~ empty(X1)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f206_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c0,c1,c75,c159,c201,c241,c243,c247,c249,c267,c268,c270,c294,c298,c376,c396,c414,c416,c418,c421,c427,c437]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t2693]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU217+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.11/0.35 % Computer : n014.cluster.edu
% 0.11/0.35 % Model : x86_64 x86_64
% 0.11/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.35 % Memory : 8046.5625MB
% 0.11/0.35 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Thu Sep 24 13:13:47 UTC 2026
% 0.11/0.36 % CPUTime :
% 0.11/0.36 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 60.28/8.08 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 60.28/8.08 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------