%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SEU294+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:37 PM UTC 2026
% Result : Theorem 64.75s 8.85s
% Output : Proof 64.75s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 34
% Syntax : Number of formulae : 159 ( 63 unt; 0 def)
% Number of atoms : 421 ( 74 equ)
% Maximal formula atoms : 15 ( 2 avg)
% Number of connectives : 512 ( 250 ~; 129 |; 114 &)
% ( 8 <=>; 11 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 15 ( 13 usr; 1 prp; 0-2 aty)
% Number of functors : 27 ( 27 usr; 10 con; 0-4 aty)
% Number of variables : 275 ( 17 sgn 181 !; 22 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f9,axiom,
! [A] :
( finite(A)
=> ! [B] :
( element(B,powerset(A))
=> finite(B) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cc2_finset_1) ).
fof(f9_nnf,plain,
! [A] :
( ! [B] :
( finite(B)
| ~ element(B,powerset(A)) )
| ~ finite(A) ),
inference(nnf_transformation,[status(thm)],[f9]) ).
fof(f9_sk,plain,
! [A,B] :
( finite(B)
| ~ element(B,powerset(A))
| ~ finite(A) ),
inference(skolemisation,[status(esa)],[f9_nnf]) ).
cnf(c15,plain,
( finite(X1)
| ~ element(X1,powerset(X0))
| ~ finite(X0) ),
inference(cnf_transformation,[status(esa)],[f9_sk]) ).
cnf(t152,plain,
ifeq(finite(X1),true,ifeq(element(X2,powerset(X1)),true,finite(X2),true),true) = true,
inference(equality_encoding,[status(esa)],[c15]) ).
cnf(t268,plain,
ifeq(finite(X1),true,ifeq(element(X2,powerset(X1)),true,finite(X2),true),true) = true,
inference(orient,[status(thm)],[t152]) ).
fof(f322,axiom,
! [A,B] :
( element(A,powerset(B))
<=> subset(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t3_subset) ).
fof(f322_nnf,plain,
! [A,B] :
( ( ~ subset(A,B)
| element(A,powerset(B)) )
& ( subset(A,B)
| ~ element(A,powerset(B)) ) ),
inference(nnf_transformation,[status(thm)],[f322]) ).
fof(f322_sk,plain,
! [A,B] :
( ( ~ subset(A,B)
| element(A,powerset(B)) )
& ( subset(A,B)
| ~ element(A,powerset(B)) ) ),
inference(skolemisation,[status(esa)],[f322_nnf]) ).
cnf(c1461,plain,
( ~ subset(X0,X1)
| element(X0,powerset(X1)) ),
inference(cnf_transformation,[status(esa)],[f322_sk]) ).
cnf(t127,plain,
ifeq(subset(X1,X2),true,element(X1,powerset(X2)),true) = true,
inference(equality_encoding,[status(esa)],[c1461]) ).
cnf(t217,plain,
ifeq(subset(X1,X2),true,element(X1,powerset(X2)),true) = true,
inference(orient,[status(thm)],[t127]) ).
fof(f248,conjecture,
! [A,B] :
( ( finite(B)
& subset(A,B) )
=> finite(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t13_finset_1) ).
fof(f248_neg,negated_conjecture,
~ ! [A,B] :
( ( finite(B)
& subset(A,B) )
=> finite(A) ),
inference(negated_conjecture,[status(cth)],[f248]) ).
fof(f248_nnf,plain,
? [A,B] :
( ~ finite(A)
& finite(B)
& subset(A,B) ),
inference(nnf_transformation,[status(thm)],[f248_neg]) ).
fof(f248_sk,plain,
( ~ finite(sk231)
& finite(sk232)
& subset(sk231,sk232) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk231,sk232])],[f248_nnf]) ).
cnf(c1338,plain,
subset(sk231,sk232),
inference(cnf_transformation,[status(esa)],[f248_sk]) ).
cnf(t87,plain,
subset(sk231,sk232) = true,
inference(equality_encoding,[status(esa)],[c1338]) ).
cnf(t457,plain,
subset(sk231,sk232) = true,
inference(orient,[status(thm)],[t87]) ).
cnf(t462,plain,
true = ifeq(true,true,element(sk231,powerset(sk232)),true),
inference(cp,[status(thm)],[t217,t457]) ).
cnf(t93,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t167,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t93]) ).
cnf(t1377,plain,
true = element(sk231,powerset(sk232)),
inference(step,[status(thm)],[t462,t167]) ).
cnf(t1285,plain,
element(sk231,powerset(sk232)) = true,
inference(orient,[status(thm)],[t1377]) ).
cnf(t1292,plain,
true = ifeq(finite(sk232),true,ifeq(true,true,finite(sk231),true),true),
inference(cp,[status(thm)],[t268,t1285]) ).
cnf(c1339,plain,
finite(sk232),
inference(cnf_transformation,[status(esa)],[f248_sk]) ).
cnf(t18,plain,
finite(sk232) = true,
inference(equality_encoding,[status(esa)],[c1339]) ).
cnf(t949,plain,
finite(sk232) = true,
inference(orient,[status(thm)],[t18]) ).
cnf(t1378,plain,
true = ifeq(true,true,ifeq(true,true,finite(sk231),true),true),
inference(step,[status(thm)],[t1292,t949]) ).
cnf(t1379,plain,
true = ifeq(true,true,finite(sk231),true),
inference(step,[status(thm)],[t1378,t167]) ).
cnf(t1380,plain,
true = finite(sk231),
inference(step,[status(thm)],[t1379,t167]) ).
cnf(c1340,plain,
~ finite(sk231),
inference(cnf_transformation,[status(esa)],[f248_sk]) ).
cnf(t17,plain,
finite(sk231) = false,
inference(equality_encoding,[status(esa)],[c1340]) ).
cnf(t1172,plain,
finite(sk231) = false,
inference(orient,[status(thm)],[t17]) ).
cnf(t1381,plain,
true = false,
inference(step,[status(thm)],[t1380,t1172]) ).
cnf(t1296,plain,
false = true,
inference(orient,[status(thm)],[t1381]) ).
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(f38,axiom,
! [A] :
( relation(A)
=> ! [B,C] :
( C = fiber(A,B)
<=> ! [D] :
( in(D,C)
<=> ( in(ordered_pair(D,B),A)
& D != B ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d1_wellord1) ).
fof(f38_nnf,plain,
! [A] :
( ! [B,C] :
( ( ? [D] :
( ( in(ordered_pair(D,B),A)
& D != B
& ~ in(D,C) )
| ( ( ~ in(ordered_pair(D,B),A)
| D = B )
& in(D,C) ) )
| C = fiber(A,B) )
& ( ! [D] :
( ( ~ in(ordered_pair(D,B),A)
| D = B
| in(D,C) )
& ( ( in(ordered_pair(D,B),A)
& D != B )
| ~ in(D,C) ) )
| C != fiber(A,B) ) )
| ~ relation(A) ),
inference(nnf_transformation,[status(thm)],[f38]) ).
fof(f38_sk,plain,
! [A,C,B,D] :
( ( ( ( in(ordered_pair(sk30(A,B,C),B),A)
& sk30(A,B,C) != B
& ~ in(sk30(A,B,C),C) )
| ( ( ~ in(ordered_pair(sk30(A,B,C),B),A)
| sk30(A,B,C) = B )
& in(sk30(A,B,C),C) )
| C = fiber(A,B) )
& ( ( ( ~ in(ordered_pair(D,B),A)
| D = B
| in(D,C) )
& ( ( in(ordered_pair(D,B),A)
& D != B )
| ~ in(D,C) ) )
| C != fiber(A,B) ) )
| ~ relation(A) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk30])],[f38_nnf]) ).
cnf(c153,plain,
( X3 != X1
| ~ in(X3,X2)
| X2 != fiber(X0,X1)
| ~ relation(X0) ),
inference(cnf_transformation,[status(esa)],[f38_sk]) ).
fof(f40,axiom,
! [A] :
( A = empty_set
<=> ! [B] : ~ in(B,A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d1_xboole_0) ).
fof(f40_nnf,plain,
! [A] :
( ( ? [B] : in(B,A)
| A = empty_set )
& ( ! [B] : ~ in(B,A)
| A != empty_set ) ),
inference(nnf_transformation,[status(thm)],[f40]) ).
fof(f40_sk,plain,
! [A,B] :
( ( in(sk33(A),A)
| A = empty_set )
& ( ~ in(B,A)
| A != empty_set ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk33])],[f40_nnf]) ).
cnf(c171,plain,
( ~ in(X1,X0)
| X0 != empty_set ),
inference(cnf_transformation,[status(esa)],[f40_sk]) ).
fof(f63,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(f63_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)],[f63]) ).
fof(f63_sk,plain,
! [C,A,B,D] :
( ( ( ~ in(sk66(A,B,C),B)
& in(sk66(A,B,C),A)
& ~ in(sk66(A,B,C),C) )
| ( ( in(sk66(A,B,C),B)
| ~ in(sk66(A,B,C),A) )
& in(sk66(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,[sk66])],[f63_nnf]) ).
cnf(c298,plain,
( ~ in(X3,X1)
| ~ in(X3,X2)
| X2 != set_difference(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f63_sk]) ).
fof(f80,axiom,
! [A,B] :
( proper_subset(A,B)
<=> ( A != B
& subset(A,B) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d8_xboole_0) ).
fof(f80_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)],[f80]) ).
fof(f80_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)],[f80_nnf]) ).
cnf(c391,plain,
( X0 != X1
| ~ proper_subset(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f80_sk]) ).
fof(f132,axiom,
! [A] : ~ empty(succ(A)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_ordinal1) ).
fof(f132_nnf,plain,
! [A] : ~ empty(succ(A)),
inference(nnf_transformation,[status(thm)],[f132]) ).
fof(f132_sk,plain,
! [A] : ~ empty(succ(A)),
inference(skolemisation,[status(esa)],[f132_nnf]) ).
cnf(c452,plain,
~ empty(succ(X0)),
inference(cnf_transformation,[status(esa)],[f132_sk]) ).
fof(f134,axiom,
! [A] : ~ empty(powerset(A)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_subset_1) ).
fof(f134_nnf,plain,
! [A] : ~ empty(powerset(A)),
inference(nnf_transformation,[status(thm)],[f134]) ).
fof(f134_sk,plain,
! [A] : ~ empty(powerset(A)),
inference(skolemisation,[status(esa)],[f134_nnf]) ).
cnf(c454,plain,
~ empty(powerset(X0)),
inference(cnf_transformation,[status(esa)],[f134_sk]) ).
fof(f136,axiom,
! [A,B] : ~ empty(ordered_pair(A,B)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_zfmisc_1) ).
fof(f136_nnf,plain,
! [A,B] : ~ empty(ordered_pair(A,B)),
inference(nnf_transformation,[status(thm)],[f136]) ).
fof(f136_sk,plain,
! [A,B] : ~ empty(ordered_pair(A,B)),
inference(skolemisation,[status(esa)],[f136_nnf]) ).
cnf(c456,plain,
~ empty(ordered_pair(X0,X1)),
inference(cnf_transformation,[status(esa)],[f136_sk]) ).
fof(f140,axiom,
! [A] : ~ empty(singleton(A)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc2_subset_1) ).
fof(f140_nnf,plain,
! [A] : ~ empty(singleton(A)),
inference(nnf_transformation,[status(thm)],[f140]) ).
fof(f140_sk,plain,
! [A] : ~ empty(singleton(A)),
inference(skolemisation,[status(esa)],[f140_nnf]) ).
cnf(c468,plain,
~ empty(singleton(X0)),
inference(cnf_transformation,[status(esa)],[f140_sk]) ).
fof(f143,axiom,
! [A] :
( ordinal(A)
=> ( ordinal(succ(A))
& epsilon_connected(succ(A))
& epsilon_transitive(succ(A))
& ~ empty(succ(A)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc3_ordinal1) ).
fof(f143_nnf,plain,
! [A] :
( ( ordinal(succ(A))
& epsilon_connected(succ(A))
& epsilon_transitive(succ(A))
& ~ empty(succ(A)) )
| ~ ordinal(A) ),
inference(nnf_transformation,[status(thm)],[f143]) ).
fof(f143_sk,plain,
! [A] :
( ( ordinal(succ(A))
& epsilon_connected(succ(A))
& epsilon_transitive(succ(A))
& ~ empty(succ(A)) )
| ~ ordinal(A) ),
inference(skolemisation,[status(esa)],[f143_nnf]) ).
cnf(c472,plain,
( ~ empty(succ(X0))
| ~ ordinal(X0) ),
inference(cnf_transformation,[status(esa)],[f143_sk]) ).
fof(f145,axiom,
! [A,B] : ~ empty(unordered_pair(A,B)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc3_subset_1) ).
fof(f145_nnf,plain,
! [A,B] : ~ empty(unordered_pair(A,B)),
inference(nnf_transformation,[status(thm)],[f145]) ).
fof(f145_sk,plain,
! [A,B] : ~ empty(unordered_pair(A,B)),
inference(skolemisation,[status(esa)],[f145_nnf]) ).
cnf(c477,plain,
~ empty(unordered_pair(X0,X1)),
inference(cnf_transformation,[status(esa)],[f145_sk]) ).
fof(f162,axiom,
! [A,B] : ~ proper_subset(A,A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',irreflexivity_r2_xboole_0) ).
fof(f162_nnf,plain,
! [A,B] : ~ proper_subset(A,A),
inference(nnf_transformation,[status(thm)],[f162]) ).
fof(f162_sk,plain,
! [A] : ~ proper_subset(A,A),
inference(skolemisation,[status(esa)],[f162_nnf]) ).
cnf(c502,plain,
~ proper_subset(X0,X0),
inference(cnf_transformation,[status(esa)],[f162_sk]) ).
fof(f164,lemma,
! [A] : singleton(A) != empty_set,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',l1_zfmisc_1) ).
fof(f164_nnf,plain,
! [A] : singleton(A) != empty_set,
inference(nnf_transformation,[status(thm)],[f164]) ).
fof(f164_sk,plain,
! [A] : singleton(A) != empty_set,
inference(skolemisation,[status(esa)],[f164_nnf]) ).
cnf(c506,plain,
singleton(X0) != empty_set,
inference(cnf_transformation,[status(esa)],[f164_sk]) ).
fof(f166,lemma,
! [A,B] :
~ ( in(A,B)
& disjoint(singleton(A),B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',l25_zfmisc_1) ).
fof(f166_nnf,plain,
! [A,B] :
( ~ in(A,B)
| ~ disjoint(singleton(A),B) ),
inference(nnf_transformation,[status(thm)],[f166]) ).
fof(f166_sk,plain,
! [A,B] :
( ~ in(A,B)
| ~ disjoint(singleton(A),B) ),
inference(skolemisation,[status(esa)],[f166_nnf]) ).
cnf(c508,plain,
( ~ in(X0,X1)
| ~ disjoint(singleton(X0),X1) ),
inference(cnf_transformation,[status(esa)],[f166_sk]) ).
fof(f182,axiom,
? [A] :
( natural(A)
& ordinal(A)
& epsilon_connected(A)
& epsilon_transitive(A)
& ~ empty(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rc1_arytm_3) ).
fof(f182_nnf,plain,
? [A] :
( natural(A)
& ordinal(A)
& epsilon_connected(A)
& epsilon_transitive(A)
& ~ empty(A) ),
inference(nnf_transformation,[status(thm)],[f182]) ).
fof(f182_sk,plain,
( natural(sk102)
& ordinal(sk102)
& epsilon_connected(sk102)
& epsilon_transitive(sk102)
& ~ empty(sk102) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk102])],[f182_nnf]) ).
cnf(c545,plain,
~ empty(sk102),
inference(cnf_transformation,[status(esa)],[f182_sk]) ).
fof(f183,axiom,
? [A] :
( finite(A)
& ~ empty(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rc1_finset_1) ).
fof(f183_nnf,plain,
? [A] :
( finite(A)
& ~ empty(A) ),
inference(nnf_transformation,[status(thm)],[f183]) ).
fof(f183_sk,plain,
( finite(sk103)
& ~ empty(sk103) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk103])],[f183_nnf]) ).
cnf(c550,plain,
~ empty(sk103),
inference(cnf_transformation,[status(esa)],[f183_sk]) ).
fof(f195,axiom,
? [A] :
( relation(A)
& ~ empty(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rc2_relat_1) ).
fof(f195_nnf,plain,
? [A] :
( relation(A)
& ~ empty(A) ),
inference(nnf_transformation,[status(thm)],[f195]) ).
fof(f195_sk,plain,
( relation(sk115)
& ~ empty(sk115) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk115])],[f195_nnf]) ).
cnf(c593,plain,
~ empty(sk115),
inference(cnf_transformation,[status(esa)],[f195_sk]) ).
fof(f197,axiom,
? [A] : ~ empty(A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rc2_xboole_0) ).
fof(f197_nnf,plain,
? [A] : ~ empty(A),
inference(nnf_transformation,[status(thm)],[f197]) ).
fof(f197_sk,plain,
~ empty(sk117),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk117])],[f197_nnf]) ).
cnf(c597,plain,
~ empty(sk117),
inference(cnf_transformation,[status(esa)],[f197_sk]) ).
fof(f200,axiom,
? [A] :
( ordinal(A)
& epsilon_connected(A)
& epsilon_transitive(A)
& ~ empty(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rc3_ordinal1) ).
fof(f200_nnf,plain,
? [A] :
( ordinal(A)
& epsilon_connected(A)
& epsilon_transitive(A)
& ~ empty(A) ),
inference(nnf_transformation,[status(thm)],[f200]) ).
fof(f200_sk,plain,
( ordinal(sk120)
& epsilon_connected(sk120)
& epsilon_transitive(sk120)
& ~ empty(sk120) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk120])],[f200_nnf]) ).
cnf(c604,plain,
~ empty(sk120),
inference(cnf_transformation,[status(esa)],[f200_sk]) ).
fof(f321,lemma,
! [A,B,C] :
~ ( in(C,A)
& in(B,C)
& in(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t3_ordinal1) ).
fof(f321_nnf,plain,
! [A,B,C] :
( ~ in(C,A)
| ~ in(B,C)
| ~ in(A,B) ),
inference(nnf_transformation,[status(thm)],[f321]) ).
fof(f321_sk,plain,
! [A,B,C] :
( ~ in(C,A)
| ~ in(B,C)
| ~ in(A,B) ),
inference(skolemisation,[status(esa)],[f321_nnf]) ).
cnf(c1459,plain,
( ~ in(X2,X0)
| ~ in(X1,X2)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f321_sk]) ).
fof(f324,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(f324_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)],[f324]) ).
fof(f324_sk,plain,
! [A,B,C] :
( ( ~ disjoint(A,B)
| ~ in(C,B)
| ~ in(C,A) )
& ( ( in(sk246(A,B),B)
& in(sk246(A,B),A) )
| disjoint(A,B) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk246])],[f324_nnf]) ).
cnf(c1465,plain,
( ~ disjoint(X0,X1)
| ~ in(X2,X1)
| ~ in(X2,X0) ),
inference(cnf_transformation,[status(esa)],[f324_sk]) ).
fof(f328,lemma,
! [A] :
( ordinal(A)
=> ( ~ ( being_limit_ordinal(A)
& ? [B] :
( A = succ(B)
& ordinal(B) ) )
& ~ ( ! [B] :
( ordinal(B)
=> A != succ(B) )
& ~ being_limit_ordinal(A) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t42_ordinal1) ).
fof(f328_nnf,plain,
! [A] :
( ( ( ~ being_limit_ordinal(A)
| ! [B] :
( A != succ(B)
| ~ ordinal(B) ) )
& ( ? [B] :
( A = succ(B)
& ordinal(B) )
| being_limit_ordinal(A) ) )
| ~ ordinal(A) ),
inference(nnf_transformation,[status(thm)],[f328]) ).
fof(f328_sk,plain,
! [A,B] :
( ( ( ~ being_limit_ordinal(A)
| A != succ(B)
| ~ ordinal(B) )
& ( ( A = succ(sk248(A))
& ordinal(sk248(A)) )
| being_limit_ordinal(A) ) )
| ~ ordinal(A) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk248])],[f328_nnf]) ).
cnf(c1474,plain,
( ~ being_limit_ordinal(X0)
| X0 != succ(X1)
| ~ ordinal(X1)
| ~ ordinal(X0) ),
inference(cnf_transformation,[status(esa)],[f328_sk]) ).
fof(f345,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(f345_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)],[f345]) ).
fof(f345_sk,plain,
! [A,B,C] :
( ( ~ disjoint(A,B)
| ~ in(C,set_intersection2(A,B)) )
& ( in(sk249(A,B),set_intersection2(A,B))
| disjoint(A,B) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk249])],[f345_nnf]) ).
cnf(c1495,plain,
( ~ disjoint(X0,X1)
| ~ in(X2,set_intersection2(X0,X1)) ),
inference(cnf_transformation,[status(esa)],[f345_sk]) ).
fof(f349,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(f349_nnf,plain,
! [A,B,C] :
( ~ in(B,C)
| ~ in(B,subset_complement(A,C))
| ~ element(C,powerset(A)) ),
inference(nnf_transformation,[status(thm)],[f349]) ).
fof(f349_sk,plain,
! [C,A,B] :
( ~ in(B,C)
| ~ in(B,subset_complement(A,C))
| ~ element(C,powerset(A)) ),
inference(skolemisation,[status(esa)],[f349_nnf]) ).
cnf(c1516,plain,
( ~ in(X1,X2)
| ~ in(X1,subset_complement(X0,X2))
| ~ element(X2,powerset(X0)) ),
inference(cnf_transformation,[status(esa)],[f349_sk]) ).
fof(f354,axiom,
! [A,B,C] :
~ ( empty(C)
& element(B,powerset(C))
& in(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t5_subset) ).
fof(f354_nnf,plain,
! [A,B,C] :
( ~ empty(C)
| ~ element(B,powerset(C))
| ~ in(A,B) ),
inference(nnf_transformation,[status(thm)],[f354]) ).
fof(f354_sk,plain,
! [A,B,C] :
( ~ empty(C)
| ~ element(B,powerset(C))
| ~ in(A,B) ),
inference(skolemisation,[status(esa)],[f354_nnf]) ).
cnf(c1523,plain,
( ~ empty(X2)
| ~ element(X1,powerset(X2))
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f354_sk]) ).
fof(f358,lemma,
! [A,B] :
~ ( proper_subset(B,A)
& subset(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t60_xboole_1) ).
fof(f358_nnf,plain,
! [A,B] :
( ~ proper_subset(B,A)
| ~ subset(A,B) ),
inference(nnf_transformation,[status(thm)],[f358]) ).
fof(f358_sk,plain,
! [A,B] :
( ~ proper_subset(B,A)
| ~ subset(A,B) ),
inference(skolemisation,[status(esa)],[f358_nnf]) ).
cnf(c1529,plain,
( ~ proper_subset(X1,X0)
| ~ subset(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f358_sk]) ).
fof(f363,lemma,
! [A,B] :
( set_difference(A,singleton(B)) = A
<=> ~ in(B,A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t65_zfmisc_1) ).
fof(f363_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)],[f363]) ).
fof(f363_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)],[f363_nnf]) ).
cnf(c1536,plain,
( ~ in(X1,X0)
| set_difference(X0,singleton(X1)) != X0 ),
inference(cnf_transformation,[status(esa)],[f363_sk]) ).
fof(f374,axiom,
! [A,B] :
~ ( empty(B)
& in(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t7_boole) ).
fof(f374_nnf,plain,
! [A,B] :
( ~ empty(B)
| ~ in(A,B) ),
inference(nnf_transformation,[status(thm)],[f374]) ).
fof(f374_sk,plain,
! [A,B] :
( ~ empty(B)
| ~ in(A,B) ),
inference(skolemisation,[status(esa)],[f374_nnf]) ).
cnf(c1554,plain,
( ~ empty(X1)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f374_sk]) ).
fof(f376,axiom,
! [A,B] :
~ ( ! [C] :
~ ( ! [D] :
~ ( in(D,C)
& in(D,B) )
& in(C,B) )
& in(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t7_tarski) ).
fof(f376_nnf,plain,
! [A,B] :
( ? [C] :
( ! [D] :
( ~ in(D,C)
| ~ in(D,B) )
& in(C,B) )
| ~ in(A,B) ),
inference(nnf_transformation,[status(thm)],[f376]) ).
fof(f376_sk,plain,
! [A,B,D] :
( ( ( ~ in(D,sk255(A,B))
| ~ in(D,B) )
& in(sk255(A,B),B) )
| ~ in(A,B) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk255])],[f376_nnf]) ).
cnf(c1558,plain,
( ~ in(X3,sk255(X0,X1))
| ~ in(X3,X1)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f376_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c0,c1,c153,c171,c298,c391,c452,c454,c456,c468,c472,c477,c502,c506,c508,c545,c550,c593,c597,c604,c1340,c1459,c1465,c1474,c1495,c1516,c1523,c1529,c1536,c1554,c1558]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t1296]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU294+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.10/0.59 % Computer : n014.cluster.edu
% 0.10/0.59 % Model : x86_64 x86_64
% 0.10/0.59 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.59 % Memory : 8046.5625MB
% 0.10/0.59 % OS : Linux 6.8.0-71-generic
% 0.10/0.59 % CPULimit : 300
% 0.10/0.59 % WCLimit : 300
% 0.10/0.59 % DateTime : Thu Sep 24 13:34:19 UTC 2026
% 0.10/0.59 % CPUTime :
% 0.10/0.59 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 64.75/8.85 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 64.75/8.85 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------