%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SEU303+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 : 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:51:39 PM UTC 2026
% Result : Theorem 82.04s 11.61s
% Output : Proof 82.04s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 38
% Syntax : Number of formulae : 190 ( 71 unt; 0 def)
% Number of atoms : 645 ( 129 equ)
% Maximal formula atoms : 49 ( 3 avg)
% Number of connectives : 815 ( 360 ~; 198 |; 210 &)
% ( 7 <=>; 40 =>; 0 <=; 0 <~>)
% Maximal formula depth : 27 ( 4 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 26 ( 24 usr; 1 prp; 0-3 aty)
% Number of functors : 41 ( 41 usr; 15 con; 0-4 aty)
% Number of variables : 344 ( 22 sgn 226 !; 32 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f137,axiom,
! [A,B] :
( ( finite(B)
& function(A)
& relation(A) )
=> finite(relation_image(A,B)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc13_finset_1) ).
fof(f137_nnf,plain,
! [A,B] :
( finite(relation_image(A,B))
| ~ finite(B)
| ~ function(A)
| ~ relation(A) ),
inference(nnf_transformation,[status(thm)],[f137]) ).
fof(f137_sk,plain,
! [A,B] :
( finite(relation_image(A,B))
| ~ finite(B)
| ~ function(A)
| ~ relation(A) ),
inference(skolemisation,[status(esa)],[f137_nnf]) ).
cnf(c469,plain,
( finite(relation_image(X0,X1))
| ~ finite(X1)
| ~ function(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(esa)],[f137_sk]) ).
cnf(t170,plain,
ifeq(relation(X1),true,ifeq(function(X1),true,ifeq(finite(X2),true,finite(relation_image(X1,X2)),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c469]) ).
cnf(t255,plain,
ifeq(relation(X1),true,ifeq(function(X1),true,ifeq(finite(X2),true,finite(relation_image(X1,X2)),true),true),true) = true,
inference(orient,[status(thm)],[t170]) ).
fof(f276,lemma,
! [A] :
( relation(A)
=> relation_image(A,relation_dom(A)) = relation_rng(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t146_relat_1) ).
fof(f276_nnf,plain,
! [A] :
( relation_image(A,relation_dom(A)) = relation_rng(A)
| ~ relation(A) ),
inference(nnf_transformation,[status(thm)],[f276]) ).
fof(f276_sk,plain,
! [A] :
( relation_image(A,relation_dom(A)) = relation_rng(A)
| ~ relation(A) ),
inference(skolemisation,[status(esa)],[f276_nnf]) ).
cnf(c1754,plain,
( relation_image(X0,relation_dom(X0)) = relation_rng(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(esa)],[f276_sk]) ).
cnf(t129,plain,
ifeq(relation(X1),true,relation_image(X1,relation_dom(X1)),relation_rng(X1)) = relation_rng(X1),
inference(equality_encoding,[status(esa)],[c1754]) ).
cnf(t1526,plain,
ifeq(relation(X1),true,relation_image(X1,relation_dom(X1)),relation_rng(X1)) = relation_rng(X1),
inference(orient,[status(thm)],[t129]) ).
fof(f317,conjecture,
! [A] :
( ( function(A)
& relation(A) )
=> ( finite(relation_dom(A))
=> finite(relation_rng(A)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t26_finset_1) ).
fof(f317_neg,negated_conjecture,
~ ! [A] :
( ( function(A)
& relation(A) )
=> ( finite(relation_dom(A))
=> finite(relation_rng(A)) ) ),
inference(negated_conjecture,[status(cth)],[f317]) ).
fof(f317_nnf,plain,
? [A] :
( ~ finite(relation_rng(A))
& finite(relation_dom(A))
& function(A)
& relation(A) ),
inference(nnf_transformation,[status(thm)],[f317_neg]) ).
fof(f317_sk,plain,
( ~ finite(relation_rng(sk291))
& finite(relation_dom(sk291))
& function(sk291)
& relation(sk291) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk291])],[f317_nnf]) ).
cnf(c1812,plain,
relation(sk291),
inference(cnf_transformation,[status(esa)],[f317_sk]) ).
cnf(t10,plain,
relation(sk291) = true,
inference(equality_encoding,[status(esa)],[c1812]) ).
cnf(t815,plain,
relation(sk291) = true,
inference(orient,[status(thm)],[t10]) ).
cnf(t1527,plain,
relation_rng(sk291) = ifeq(true,true,relation_image(sk291,relation_dom(sk291)),relation_rng(sk291)),
inference(cp,[status(thm)],[t1526,t815]) ).
cnf(t57,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t191,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t57]) ).
cnf(t2294,plain,
relation_rng(sk291) = relation_image(sk291,relation_dom(sk291)),
inference(step,[status(thm)],[t1527,t191]) ).
cnf(t2228,plain,
relation_image(sk291,relation_dom(sk291)) = relation_rng(sk291),
inference(orient,[status(thm)],[t2294]) ).
cnf(t2229,plain,
true = ifeq(relation(sk291),true,ifeq(function(sk291),true,ifeq(finite(relation_dom(sk291)),true,finite(relation_rng(sk291)),true),true),true),
inference(cp,[status(thm)],[t255,t2228]) ).
cnf(t2295,plain,
true = ifeq(true,true,ifeq(function(sk291),true,ifeq(finite(relation_dom(sk291)),true,finite(relation_rng(sk291)),true),true),true),
inference(step,[status(thm)],[t2229,t815]) ).
cnf(t2296,plain,
true = ifeq(function(sk291),true,ifeq(finite(relation_dom(sk291)),true,finite(relation_rng(sk291)),true),true),
inference(step,[status(thm)],[t2295,t191]) ).
cnf(c1813,plain,
function(sk291),
inference(cnf_transformation,[status(esa)],[f317_sk]) ).
cnf(t6,plain,
function(sk291) = true,
inference(equality_encoding,[status(esa)],[c1813]) ).
cnf(t1314,plain,
function(sk291) = true,
inference(orient,[status(thm)],[t6]) ).
cnf(t2297,plain,
true = ifeq(true,true,ifeq(finite(relation_dom(sk291)),true,finite(relation_rng(sk291)),true),true),
inference(step,[status(thm)],[t2296,t1314]) ).
cnf(t2298,plain,
true = ifeq(finite(relation_dom(sk291)),true,finite(relation_rng(sk291)),true),
inference(step,[status(thm)],[t2297,t191]) ).
cnf(c1814,plain,
finite(relation_dom(sk291)),
inference(cnf_transformation,[status(esa)],[f317_sk]) ).
cnf(t18,plain,
finite(relation_dom(sk291)) = true,
inference(equality_encoding,[status(esa)],[c1814]) ).
cnf(t1214,plain,
finite(relation_dom(sk291)) = true,
inference(orient,[status(thm)],[t18]) ).
cnf(t2299,plain,
true = ifeq(true,true,finite(relation_rng(sk291)),true),
inference(step,[status(thm)],[t2298,t1214]) ).
cnf(t2300,plain,
true = finite(relation_rng(sk291)),
inference(step,[status(thm)],[t2299,t191]) ).
cnf(c1815,plain,
~ finite(relation_rng(sk291)),
inference(cnf_transformation,[status(esa)],[f317_sk]) ).
cnf(t19,plain,
finite(relation_rng(sk291)) = false,
inference(equality_encoding,[status(esa)],[c1815]) ).
cnf(t2057,plain,
finite(relation_rng(sk291)) = false,
inference(orient,[status(thm)],[t19]) ).
cnf(t2301,plain,
true = false,
inference(step,[status(thm)],[t2300,t2057]) ).
cnf(t2231,plain,
false = true,
inference(orient,[status(thm)],[t2301]) ).
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(f40,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(f40_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)],[f40]) ).
fof(f40_sk,plain,
! [A,C,B,D] :
( ( ( ( in(ordered_pair(sk31(A,B,C),B),A)
& sk31(A,B,C) != B
& ~ in(sk31(A,B,C),C) )
| ( ( ~ in(ordered_pair(sk31(A,B,C),B),A)
| sk31(A,B,C) = B )
& in(sk31(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,[sk31])],[f40_nnf]) ).
cnf(c162,plain,
( X3 != X1
| ~ in(X3,X2)
| X2 != fiber(X0,X1)
| ~ relation(X0) ),
inference(cnf_transformation,[status(esa)],[f40_sk]) ).
fof(f42,axiom,
! [A] :
( A = empty_set
<=> ! [B] : ~ in(B,A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d1_xboole_0) ).
fof(f42_nnf,plain,
! [A] :
( ( ? [B] : in(B,A)
| A = empty_set )
& ( ! [B] : ~ in(B,A)
| A != empty_set ) ),
inference(nnf_transformation,[status(thm)],[f42]) ).
fof(f42_sk,plain,
! [A,B] :
( ( in(sk34(A),A)
| A = empty_set )
& ( ~ in(B,A)
| A != empty_set ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk34])],[f42_nnf]) ).
cnf(c180,plain,
( ~ in(X1,X0)
| X0 != empty_set ),
inference(cnf_transformation,[status(esa)],[f42_sk]) ).
fof(f65,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(f65_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)],[f65]) ).
fof(f65_sk,plain,
! [C,A,B,D] :
( ( ( ~ in(sk67(A,B,C),B)
& in(sk67(A,B,C),A)
& ~ in(sk67(A,B,C),C) )
| ( ( in(sk67(A,B,C),B)
| ~ in(sk67(A,B,C),A) )
& in(sk67(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,[sk67])],[f65_nnf]) ).
cnf(c307,plain,
( ~ in(X3,X1)
| ~ in(X3,X2)
| X2 != set_difference(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f65_sk]) ).
fof(f83,axiom,
! [A,B] :
( proper_subset(A,B)
<=> ( A != B
& subset(A,B) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d8_xboole_0) ).
fof(f83_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)],[f83]) ).
fof(f83_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)],[f83_nnf]) ).
cnf(c408,plain,
( X0 != X1
| ~ proper_subset(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f83_sk]) ).
fof(f139,axiom,
! [A] :
( finite(singleton(A))
& ~ empty(singleton(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_finset_1) ).
fof(f139_nnf,plain,
! [A] :
( finite(singleton(A))
& ~ empty(singleton(A)) ),
inference(nnf_transformation,[status(thm)],[f139]) ).
fof(f139_sk,plain,
! [A] :
( finite(singleton(A))
& ~ empty(singleton(A)) ),
inference(skolemisation,[status(esa)],[f139_nnf]) ).
cnf(c472,plain,
~ empty(singleton(X0)),
inference(cnf_transformation,[status(esa)],[f139_sk]) ).
fof(f141,axiom,
! [A] : ~ empty(succ(A)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_ordinal1) ).
fof(f141_nnf,plain,
! [A] : ~ empty(succ(A)),
inference(nnf_transformation,[status(thm)],[f141]) ).
fof(f141_sk,plain,
! [A] : ~ empty(succ(A)),
inference(skolemisation,[status(esa)],[f141_nnf]) ).
cnf(c476,plain,
~ empty(succ(X0)),
inference(cnf_transformation,[status(esa)],[f141_sk]) ).
fof(f142,axiom,
( ~ empty(omega)
& ordinal(omega)
& epsilon_connected(omega)
& epsilon_transitive(omega) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_ordinal2) ).
fof(f142_nnf,plain,
( ~ empty(omega)
& ordinal(omega)
& epsilon_connected(omega)
& epsilon_transitive(omega) ),
inference(nnf_transformation,[status(thm)],[f142]) ).
fof(f142_sk,plain,
( ~ empty(omega)
& ordinal(omega)
& epsilon_connected(omega)
& epsilon_transitive(omega) ),
inference(skolemisation,[status(esa)],[f142_nnf]) ).
cnf(c480,plain,
~ empty(omega),
inference(cnf_transformation,[status(esa)],[f142_sk]) ).
fof(f144,axiom,
! [A] : ~ empty(powerset(A)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_subset_1) ).
fof(f144_nnf,plain,
! [A] : ~ empty(powerset(A)),
inference(nnf_transformation,[status(thm)],[f144]) ).
fof(f144_sk,plain,
! [A] : ~ empty(powerset(A)),
inference(skolemisation,[status(esa)],[f144_nnf]) ).
cnf(c482,plain,
~ empty(powerset(X0)),
inference(cnf_transformation,[status(esa)],[f144_sk]) ).
fof(f146,axiom,
! [A,B] : ~ empty(ordered_pair(A,B)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_zfmisc_1) ).
fof(f146_nnf,plain,
! [A,B] : ~ empty(ordered_pair(A,B)),
inference(nnf_transformation,[status(thm)],[f146]) ).
fof(f146_sk,plain,
! [A,B] : ~ empty(ordered_pair(A,B)),
inference(skolemisation,[status(esa)],[f146_nnf]) ).
cnf(c484,plain,
~ empty(ordered_pair(X0,X1)),
inference(cnf_transformation,[status(esa)],[f146_sk]) ).
fof(f147,axiom,
! [A] :
( ( natural(A)
& ordinal(A) )
=> ( natural(succ(A))
& ordinal(succ(A))
& epsilon_connected(succ(A))
& epsilon_transitive(succ(A))
& ~ empty(succ(A)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc2_arytm_3) ).
fof(f147_nnf,plain,
! [A] :
( ( natural(succ(A))
& ordinal(succ(A))
& epsilon_connected(succ(A))
& epsilon_transitive(succ(A))
& ~ empty(succ(A)) )
| ~ natural(A)
| ~ ordinal(A) ),
inference(nnf_transformation,[status(thm)],[f147]) ).
fof(f147_sk,plain,
! [A] :
( ( natural(succ(A))
& ordinal(succ(A))
& epsilon_connected(succ(A))
& epsilon_transitive(succ(A))
& ~ empty(succ(A)) )
| ~ natural(A)
| ~ ordinal(A) ),
inference(skolemisation,[status(esa)],[f147_nnf]) ).
cnf(c485,plain,
( ~ empty(succ(X0))
| ~ natural(X0)
| ~ ordinal(X0) ),
inference(cnf_transformation,[status(esa)],[f147_sk]) ).
fof(f151,axiom,
! [A] : ~ empty(singleton(A)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc2_subset_1) ).
fof(f151_nnf,plain,
! [A] : ~ empty(singleton(A)),
inference(nnf_transformation,[status(thm)],[f151]) ).
fof(f151_sk,plain,
! [A] : ~ empty(singleton(A)),
inference(skolemisation,[status(esa)],[f151_nnf]) ).
cnf(c501,plain,
~ empty(singleton(X0)),
inference(cnf_transformation,[status(esa)],[f151_sk]) ).
fof(f154,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(f154_nnf,plain,
! [A] :
( ( ordinal(succ(A))
& epsilon_connected(succ(A))
& epsilon_transitive(succ(A))
& ~ empty(succ(A)) )
| ~ ordinal(A) ),
inference(nnf_transformation,[status(thm)],[f154]) ).
fof(f154_sk,plain,
! [A] :
( ( ordinal(succ(A))
& epsilon_connected(succ(A))
& epsilon_transitive(succ(A))
& ~ empty(succ(A)) )
| ~ ordinal(A) ),
inference(skolemisation,[status(esa)],[f154_nnf]) ).
cnf(c505,plain,
( ~ empty(succ(X0))
| ~ ordinal(X0) ),
inference(cnf_transformation,[status(esa)],[f154_sk]) ).
fof(f156,axiom,
! [A,B] : ~ empty(unordered_pair(A,B)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc3_subset_1) ).
fof(f156_nnf,plain,
! [A,B] : ~ empty(unordered_pair(A,B)),
inference(nnf_transformation,[status(thm)],[f156]) ).
fof(f156_sk,plain,
! [A,B] : ~ empty(unordered_pair(A,B)),
inference(skolemisation,[status(esa)],[f156_nnf]) ).
cnf(c510,plain,
~ empty(unordered_pair(X0,X1)),
inference(cnf_transformation,[status(esa)],[f156_sk]) ).
fof(f174,axiom,
! [A,B] : ~ proper_subset(A,A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',irreflexivity_r2_xboole_0) ).
fof(f174_nnf,plain,
! [A,B] : ~ proper_subset(A,A),
inference(nnf_transformation,[status(thm)],[f174]) ).
fof(f174_sk,plain,
! [A] : ~ proper_subset(A,A),
inference(skolemisation,[status(esa)],[f174_nnf]) ).
cnf(c536,plain,
~ proper_subset(X0,X0),
inference(cnf_transformation,[status(esa)],[f174_sk]) ).
fof(f176,lemma,
! [A] : singleton(A) != empty_set,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',l1_zfmisc_1) ).
fof(f176_nnf,plain,
! [A] : singleton(A) != empty_set,
inference(nnf_transformation,[status(thm)],[f176]) ).
fof(f176_sk,plain,
! [A] : singleton(A) != empty_set,
inference(skolemisation,[status(esa)],[f176_nnf]) ).
cnf(c540,plain,
singleton(X0) != empty_set,
inference(cnf_transformation,[status(esa)],[f176_sk]) ).
fof(f178,lemma,
! [A,B] :
~ ( in(A,B)
& disjoint(singleton(A),B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',l25_zfmisc_1) ).
fof(f178_nnf,plain,
! [A,B] :
( ~ in(A,B)
| ~ disjoint(singleton(A),B) ),
inference(nnf_transformation,[status(thm)],[f178]) ).
fof(f178_sk,plain,
! [A,B] :
( ~ in(A,B)
| ~ disjoint(singleton(A),B) ),
inference(skolemisation,[status(esa)],[f178_nnf]) ).
cnf(c542,plain,
( ~ in(X0,X1)
| ~ disjoint(singleton(X0),X1) ),
inference(cnf_transformation,[status(esa)],[f178_sk]) ).
fof(f194,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(f194_nnf,plain,
? [A] :
( natural(A)
& ordinal(A)
& epsilon_connected(A)
& epsilon_transitive(A)
& ~ empty(A) ),
inference(nnf_transformation,[status(thm)],[f194]) ).
fof(f194_sk,plain,
( natural(sk104)
& ordinal(sk104)
& epsilon_connected(sk104)
& epsilon_transitive(sk104)
& ~ empty(sk104) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk104])],[f194_nnf]) ).
cnf(c579,plain,
~ empty(sk104),
inference(cnf_transformation,[status(esa)],[f194_sk]) ).
fof(f195,axiom,
? [A] :
( finite(A)
& ~ empty(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rc1_finset_1) ).
fof(f195_nnf,plain,
? [A] :
( finite(A)
& ~ empty(A) ),
inference(nnf_transformation,[status(thm)],[f195]) ).
fof(f195_sk,plain,
( finite(sk105)
& ~ empty(sk105) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk105])],[f195_nnf]) ).
cnf(c584,plain,
~ empty(sk105),
inference(cnf_transformation,[status(esa)],[f195_sk]) ).
fof(f208,axiom,
? [A] :
( relation(A)
& ~ empty(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rc2_relat_1) ).
fof(f208_nnf,plain,
? [A] :
( relation(A)
& ~ empty(A) ),
inference(nnf_transformation,[status(thm)],[f208]) ).
fof(f208_sk,plain,
( relation(sk118)
& ~ empty(sk118) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk118])],[f208_nnf]) ).
cnf(c631,plain,
~ empty(sk118),
inference(cnf_transformation,[status(esa)],[f208_sk]) ).
fof(f210,axiom,
? [A] : ~ empty(A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rc2_xboole_0) ).
fof(f210_nnf,plain,
? [A] : ~ empty(A),
inference(nnf_transformation,[status(thm)],[f210]) ).
fof(f210_sk,plain,
~ empty(sk120),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk120])],[f210_nnf]) ).
cnf(c635,plain,
~ empty(sk120),
inference(cnf_transformation,[status(esa)],[f210_sk]) ).
fof(f213,axiom,
? [A] :
( ordinal(A)
& epsilon_connected(A)
& epsilon_transitive(A)
& ~ empty(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rc3_ordinal1) ).
fof(f213_nnf,plain,
? [A] :
( ordinal(A)
& epsilon_connected(A)
& epsilon_transitive(A)
& ~ empty(A) ),
inference(nnf_transformation,[status(thm)],[f213]) ).
fof(f213_sk,plain,
( ordinal(sk123)
& epsilon_connected(sk123)
& epsilon_transitive(sk123)
& ~ empty(sk123) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk123])],[f213_nnf]) ).
cnf(c642,plain,
~ empty(sk123),
inference(cnf_transformation,[status(esa)],[f213_sk]) ).
fof(f230,lemma,
( ( ! [D] :
( ordinal(D)
=> ( ( ! [K] :
( ordinal(K)
=> ( in(K,D)
=> ( in(K,omega)
=> ! [L] :
( element(L,powerset(powerset(K)))
=> ~ ( ! [M] :
~ ( ! [N] :
( ( subset(M,N)
& in(N,L) )
=> N = M )
& in(M,L) )
& L != empty_set ) ) ) ) )
& being_limit_ordinal(D) )
=> ( ( in(D,omega)
=> ! [O] :
( element(O,powerset(powerset(D)))
=> ~ ( ! [P] :
~ ( ! [Q] :
( ( subset(P,Q)
& in(Q,O) )
=> Q = P )
& in(P,O) )
& O != empty_set ) ) )
| D = empty_set ) ) )
& ! [D] :
( ordinal(D)
=> ( ( in(D,omega)
=> ! [E] :
( element(E,powerset(powerset(D)))
=> ~ ( ! [F] :
~ ( ! [G] :
( ( subset(F,G)
& in(G,E) )
=> G = F )
& in(F,E) )
& E != empty_set ) ) )
=> ( in(succ(D),omega)
=> ! [H] :
( element(H,powerset(powerset(succ(D))))
=> ~ ( ! [I] :
~ ( ! [J] :
( ( subset(I,J)
& in(J,H) )
=> J = I )
& in(I,H) )
& H != empty_set ) ) ) ) )
& ( in(empty_set,omega)
=> ! [A] :
( element(A,powerset(powerset(empty_set)))
=> ~ ( ! [B] :
~ ( ! [C] :
( ( subset(B,C)
& in(C,A) )
=> C = B )
& in(B,A) )
& A != empty_set ) ) ) )
=> ! [D] :
( ordinal(D)
=> ( in(D,omega)
=> ! [R] :
( element(R,powerset(powerset(D)))
=> ~ ( ! [S] :
~ ( ! [T] :
( ( subset(S,T)
& in(T,R) )
=> T = S )
& in(S,R) )
& R != empty_set ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',s1_ordinal2__e18_27__finset_1) ).
fof(f230_nnf,plain,
( ! [D] :
( ! [R] :
( ? [S] :
( ! [T] :
( T = S
| ~ subset(S,T)
| ~ in(T,R) )
& in(S,R) )
| R = empty_set
| ~ element(R,powerset(powerset(D))) )
| ~ in(D,omega)
| ~ ordinal(D) )
| ? [D] :
( ? [O] :
( ! [P] :
( ? [Q] :
( Q != P
& subset(P,Q)
& in(Q,O) )
| ~ in(P,O) )
& O != empty_set
& element(O,powerset(powerset(D))) )
& in(D,omega)
& D != empty_set
& ! [K] :
( ! [L] :
( ? [M] :
( ! [N] :
( N = M
| ~ subset(M,N)
| ~ in(N,L) )
& in(M,L) )
| L = empty_set
| ~ element(L,powerset(powerset(K))) )
| ~ in(K,omega)
| ~ in(K,D)
| ~ ordinal(K) )
& being_limit_ordinal(D)
& ordinal(D) )
| ? [D] :
( ? [H] :
( ! [I] :
( ? [J] :
( J != I
& subset(I,J)
& in(J,H) )
| ~ in(I,H) )
& H != empty_set
& element(H,powerset(powerset(succ(D)))) )
& in(succ(D),omega)
& ( ! [E] :
( ? [F] :
( ! [G] :
( G = F
| ~ subset(F,G)
| ~ in(G,E) )
& in(F,E) )
| E = empty_set
| ~ element(E,powerset(powerset(D))) )
| ~ in(D,omega) )
& ordinal(D) )
| ( ? [A] :
( ! [B] :
( ? [C] :
( C != B
& subset(B,C)
& in(C,A) )
| ~ in(B,A) )
& A != empty_set
& element(A,powerset(powerset(empty_set))) )
& in(empty_set,omega) ) ),
inference(nnf_transformation,[status(thm)],[f230]) ).
fof(f230_sk,plain,
! [B,E,G,I,K,L,N,P,D,R,T] :
( ( ( T = sk149(D,R)
| ~ subset(sk149(D,R),T)
| ~ in(T,R) )
& in(sk149(D,R),R) )
| R = empty_set
| ~ element(R,powerset(powerset(D)))
| ~ in(D,omega)
| ~ ordinal(D)
| ( ( ( sk148(P) != P
& subset(P,sk148(P))
& in(sk148(P),sk147) )
| ~ in(P,sk147) )
& sk147 != empty_set
& element(sk147,powerset(powerset(sk145)))
& in(sk145,omega)
& sk145 != empty_set
& ( ( ( N = sk146(K,L)
| ~ subset(sk146(K,L),N)
| ~ in(N,L) )
& in(sk146(K,L),L) )
| L = empty_set
| ~ element(L,powerset(powerset(K)))
| ~ in(K,omega)
| ~ in(K,sk145)
| ~ ordinal(K) )
& being_limit_ordinal(sk145)
& ordinal(sk145) )
| ( ( ( sk144(I) != I
& subset(I,sk144(I))
& in(sk144(I),sk143) )
| ~ in(I,sk143) )
& sk143 != empty_set
& element(sk143,powerset(powerset(succ(sk141))))
& in(succ(sk141),omega)
& ( ( ( G = sk142(E)
| ~ subset(sk142(E),G)
| ~ in(G,E) )
& in(sk142(E),E) )
| E = empty_set
| ~ element(E,powerset(powerset(sk141)))
| ~ in(sk141,omega) )
& ordinal(sk141) )
| ( ( ( sk140(B) != B
& subset(B,sk140(B))
& in(sk140(B),sk139) )
| ~ in(B,sk139) )
& sk139 != empty_set
& element(sk139,powerset(powerset(empty_set)))
& in(empty_set,omega) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk139,sk140,sk141,sk142,sk143,sk144,sk145,sk146,sk147,sk148,sk149])],[f230_nnf]) ).
cnf(c783,plain,
( sk140(X1) != X1
| ~ def1(X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47])],[f230_sk]) ).
cnf(c788,plain,
( sk139 != empty_set
| ~ def3(X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47])],[f230_sk]) ).
cnf(c797,plain,
( ~ subset(sk142(X4),X6)
| ~ in(X6,X4)
| ~ def6(X6,X4) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47])],[f230_sk]) ).
cnf(c819,plain,
( sk144(X8) != X8
| ~ def13(X8) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47])],[f230_sk]) ).
cnf(c824,plain,
( sk143 != empty_set
| ~ def15(X8) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47])],[f230_sk]) ).
cnf(c842,plain,
( ~ subset(sk146(X10,X11),X13)
| ~ in(X13,X11)
| ~ def21(X13,X11,X10) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47])],[f230_sk]) ).
cnf(c873,plain,
( sk148(X15) != X15
| ~ def31(X15) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47])],[f230_sk]) ).
cnf(c878,plain,
( sk147 != empty_set
| ~ def33(X15) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47])],[f230_sk]) ).
cnf(c887,plain,
( sk145 != empty_set
| ~ def36(X15) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47])],[f230_sk]) ).
cnf(c899,plain,
( ~ subset(sk149(X3,X17),X19)
| ~ in(X19,X17)
| ~ def40(X19,X17,X3) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47])],[f230_sk]) ).
fof(f346,lemma,
! [A,B,C] :
~ ( in(C,A)
& in(B,C)
& in(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t3_ordinal1) ).
fof(f346_nnf,plain,
! [A,B,C] :
( ~ in(C,A)
| ~ in(B,C)
| ~ in(A,B) ),
inference(nnf_transformation,[status(thm)],[f346]) ).
fof(f346_sk,plain,
! [A,B,C] :
( ~ in(C,A)
| ~ in(B,C)
| ~ in(A,B) ),
inference(skolemisation,[status(esa)],[f346_nnf]) ).
cnf(c1871,plain,
( ~ in(X2,X0)
| ~ in(X1,X2)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f346_sk]) ).
fof(f349,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(f349_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)],[f349]) ).
fof(f349_sk,plain,
! [A,B,C] :
( ( ~ disjoint(A,B)
| ~ in(C,B)
| ~ in(C,A) )
& ( ( in(sk299(A,B),B)
& in(sk299(A,B),A) )
| disjoint(A,B) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk299])],[f349_nnf]) ).
cnf(c1877,plain,
( ~ disjoint(X0,X1)
| ~ in(X2,X1)
| ~ in(X2,X0) ),
inference(cnf_transformation,[status(esa)],[f349_sk]) ).
fof(f353,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(f353_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)],[f353]) ).
fof(f353_sk,plain,
! [A,B] :
( ( ( ~ being_limit_ordinal(A)
| A != succ(B)
| ~ ordinal(B) )
& ( ( A = succ(sk301(A))
& ordinal(sk301(A)) )
| being_limit_ordinal(A) ) )
| ~ ordinal(A) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk301])],[f353_nnf]) ).
cnf(c1886,plain,
( ~ being_limit_ordinal(X0)
| X0 != succ(X1)
| ~ ordinal(X1)
| ~ ordinal(X0) ),
inference(cnf_transformation,[status(esa)],[f353_sk]) ).
fof(f370,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(f370_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)],[f370]) ).
fof(f370_sk,plain,
! [A,B,C] :
( ( ~ disjoint(A,B)
| ~ in(C,set_intersection2(A,B)) )
& ( in(sk302(A,B),set_intersection2(A,B))
| disjoint(A,B) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk302])],[f370_nnf]) ).
cnf(c1907,plain,
( ~ disjoint(X0,X1)
| ~ in(X2,set_intersection2(X0,X1)) ),
inference(cnf_transformation,[status(esa)],[f370_sk]) ).
fof(f374,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(f374_nnf,plain,
! [A,B,C] :
( ~ in(B,C)
| ~ in(B,subset_complement(A,C))
| ~ element(C,powerset(A)) ),
inference(nnf_transformation,[status(thm)],[f374]) ).
fof(f374_sk,plain,
! [C,A,B] :
( ~ in(B,C)
| ~ in(B,subset_complement(A,C))
| ~ element(C,powerset(A)) ),
inference(skolemisation,[status(esa)],[f374_nnf]) ).
cnf(c1928,plain,
( ~ in(X1,X2)
| ~ in(X1,subset_complement(X0,X2))
| ~ element(X2,powerset(X0)) ),
inference(cnf_transformation,[status(esa)],[f374_sk]) ).
fof(f379,axiom,
! [A,B,C] :
~ ( empty(C)
& element(B,powerset(C))
& in(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t5_subset) ).
fof(f379_nnf,plain,
! [A,B,C] :
( ~ empty(C)
| ~ element(B,powerset(C))
| ~ in(A,B) ),
inference(nnf_transformation,[status(thm)],[f379]) ).
fof(f379_sk,plain,
! [A,B,C] :
( ~ empty(C)
| ~ element(B,powerset(C))
| ~ in(A,B) ),
inference(skolemisation,[status(esa)],[f379_nnf]) ).
cnf(c1935,plain,
( ~ empty(X2)
| ~ element(X1,powerset(X2))
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f379_sk]) ).
fof(f383,lemma,
! [A,B] :
~ ( proper_subset(B,A)
& subset(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t60_xboole_1) ).
fof(f383_nnf,plain,
! [A,B] :
( ~ proper_subset(B,A)
| ~ subset(A,B) ),
inference(nnf_transformation,[status(thm)],[f383]) ).
fof(f383_sk,plain,
! [A,B] :
( ~ proper_subset(B,A)
| ~ subset(A,B) ),
inference(skolemisation,[status(esa)],[f383_nnf]) ).
cnf(c1941,plain,
( ~ proper_subset(X1,X0)
| ~ subset(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f383_sk]) ).
fof(f388,lemma,
! [A,B] :
( set_difference(A,singleton(B)) = A
<=> ~ in(B,A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t65_zfmisc_1) ).
fof(f388_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)],[f388]) ).
fof(f388_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)],[f388_nnf]) ).
cnf(c1948,plain,
( ~ in(X1,X0)
| set_difference(X0,singleton(X1)) != X0 ),
inference(cnf_transformation,[status(esa)],[f388_sk]) ).
fof(f399,axiom,
! [A,B] :
~ ( empty(B)
& in(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t7_boole) ).
fof(f399_nnf,plain,
! [A,B] :
( ~ empty(B)
| ~ in(A,B) ),
inference(nnf_transformation,[status(thm)],[f399]) ).
fof(f399_sk,plain,
! [A,B] :
( ~ empty(B)
| ~ in(A,B) ),
inference(skolemisation,[status(esa)],[f399_nnf]) ).
cnf(c1966,plain,
( ~ empty(X1)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f399_sk]) ).
fof(f401,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(f401_nnf,plain,
! [A,B] :
( ? [C] :
( ! [D] :
( ~ in(D,C)
| ~ in(D,B) )
& in(C,B) )
| ~ in(A,B) ),
inference(nnf_transformation,[status(thm)],[f401]) ).
fof(f401_sk,plain,
! [A,B,D] :
( ( ( ~ in(D,sk308(A,B))
| ~ in(D,B) )
& in(sk308(A,B),B) )
| ~ in(A,B) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk308])],[f401_nnf]) ).
cnf(c1970,plain,
( ~ in(X3,sk308(X0,X1))
| ~ in(X3,X1)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f401_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c0,c1,c162,c180,c307,c408,c472,c476,c480,c482,c484,c485,c501,c505,c510,c536,c540,c542,c579,c584,c631,c635,c642,c783,c788,c797,c819,c824,c842,c873,c878,c887,c899,c1815,c1871,c1877,c1886,c1907,c1928,c1935,c1941,c1948,c1966,c1970]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t2231]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SEU303+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.07 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.20/0.45 % Computer : n007.cluster.edu
% 0.20/0.45 % Model : x86_64 x86_64
% 0.20/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.20/0.45 % Memory : 8046.5625MB
% 0.20/0.45 % OS : Linux 6.8.0-71-generic
% 0.20/0.45 % CPULimit : 300
% 0.20/0.45 % WCLimit : 300
% 0.20/0.45 % DateTime : Thu Sep 24 13:35:23 UTC 2026
% 0.20/0.45 % CPUTime :
% 0.20/0.45 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 82.04/11.61 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 82.04/11.61 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------