%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SEU248+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 : n004.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:29 PM UTC 2026
% Result : Theorem 61.11s 13.49s
% Output : Proof 61.11s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 32
% Syntax : Number of formulae : 157 ( 67 unt; 0 def)
% Number of atoms : 372 ( 65 equ)
% Maximal formula atoms : 14 ( 2 avg)
% Number of connectives : 440 ( 225 ~; 114 |; 83 &)
% ( 5 <=>; 13 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of predicates : 13 ( 11 usr; 1 prp; 0-2 aty)
% Number of functors : 26 ( 26 usr; 8 con; 0-4 aty)
% Number of variables : 279 ( 35 sgn 175 !; 17 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f145,conjecture,
! [A,B] :
( relation(B)
=> subset(relation_dom(relation_rng_restriction(A,B)),relation_dom(B)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',l29_wellord1) ).
fof(f145_neg,negated_conjecture,
~ ! [A,B] :
( relation(B)
=> subset(relation_dom(relation_rng_restriction(A,B)),relation_dom(B)) ),
inference(negated_conjecture,[status(cth)],[f145]) ).
fof(f145_nnf,plain,
? [A,B] :
( ~ subset(relation_dom(relation_rng_restriction(A,B)),relation_dom(B))
& relation(B) ),
inference(nnf_transformation,[status(thm)],[f145_neg]) ).
fof(f145_sk,plain,
( ~ subset(relation_dom(relation_rng_restriction(sk78,sk79)),relation_dom(sk79))
& relation(sk79) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk78,sk79])],[f145_nnf]) ).
cnf(c435,plain,
~ subset(relation_dom(relation_rng_restriction(sk78,sk79)),relation_dom(sk79)),
inference(cnf_transformation,[status(esa)],[f145_sk]) ).
cnf(t58,plain,
subset(relation_dom(relation_rng_restriction(sk78,sk79)),relation_dom(sk79)) = false,
inference(equality_encoding,[status(esa)],[c435]) ).
cnf(t495,plain,
subset(relation_dom(relation_rng_restriction(sk78,sk79)),relation_dom(sk79)) = false,
inference(orient,[status(thm)],[t58]) ).
fof(f221,lemma,
! [A] :
( relation(A)
=> ! [B] :
( relation(B)
=> ( subset(A,B)
=> ( subset(relation_rng(A),relation_rng(B))
& subset(relation_dom(A),relation_dom(B)) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t25_relat_1) ).
fof(f221_nnf,plain,
! [A] :
( ! [B] :
( ( subset(relation_rng(A),relation_rng(B))
& subset(relation_dom(A),relation_dom(B)) )
| ~ subset(A,B)
| ~ relation(B) )
| ~ relation(A) ),
inference(nnf_transformation,[status(thm)],[f221]) ).
fof(f221_sk,plain,
! [A,B] :
( ( subset(relation_rng(A),relation_rng(B))
& subset(relation_dom(A),relation_dom(B)) )
| ~ subset(A,B)
| ~ relation(B)
| ~ relation(A) ),
inference(skolemisation,[status(esa)],[f221_nnf]) ).
cnf(c574,plain,
( subset(relation_dom(X0),relation_dom(X1))
| ~ subset(X0,X1)
| ~ relation(X1)
| ~ relation(X0) ),
inference(cnf_transformation,[status(esa)],[f221_sk]) ).
cnf(t92,plain,
ifeq(relation(X1),true,ifeq(relation(X2),true,ifeq(subset(X1,X2),true,subset(relation_dom(X1),relation_dom(X2)),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c574]) ).
cnf(t146,plain,
ifeq(relation(X1),true,ifeq(relation(X2),true,ifeq(subset(X1,X2),true,subset(relation_dom(X1),relation_dom(X2)),true),true),true) = true,
inference(orient,[status(thm)],[t92]) ).
fof(f184,lemma,
! [A,B] :
( relation(B)
=> subset(relation_rng_restriction(A,B),B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t117_relat_1) ).
fof(f184_nnf,plain,
! [A,B] :
( subset(relation_rng_restriction(A,B),B)
| ~ relation(B) ),
inference(nnf_transformation,[status(thm)],[f184]) ).
fof(f184_sk,plain,
! [B,A] :
( subset(relation_rng_restriction(A,B),B)
| ~ relation(B) ),
inference(skolemisation,[status(esa)],[f184_nnf]) ).
cnf(c522,plain,
( subset(relation_rng_restriction(X0,X1),X1)
| ~ relation(X1) ),
inference(cnf_transformation,[status(esa)],[f184_sk]) ).
cnf(t64,plain,
ifeq(relation(X1),true,subset(relation_rng_restriction(X2,X1),X1),true) = true,
inference(equality_encoding,[status(esa)],[c522]) ).
cnf(t154,plain,
ifeq(relation(X1),true,subset(relation_rng_restriction(X2,X1),X1),true) = true,
inference(orient,[status(thm)],[t64]) ).
cnf(c434,plain,
relation(sk79),
inference(cnf_transformation,[status(esa)],[f145_sk]) ).
cnf(t0,plain,
relation(sk79) = true,
inference(equality_encoding,[status(esa)],[c434]) ).
cnf(t299,plain,
relation(sk79) = true,
inference(orient,[status(thm)],[t0]) ).
cnf(t301,plain,
true = ifeq(true,true,subset(relation_rng_restriction(X1,sk79),sk79),true),
inference(cp,[status(thm)],[t154,t299]) ).
cnf(t40,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t103,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t40]) ).
cnf(t1073,plain,
true = subset(relation_rng_restriction(X1,sk79),sk79),
inference(step,[status(thm)],[t301,t103]) ).
cnf(t804,plain,
subset(relation_rng_restriction(X1,sk79),sk79) = true,
inference(orient,[status(thm)],[t1073]) ).
cnf(t813,plain,
true = ifeq(relation(relation_rng_restriction(X1,sk79)),true,ifeq(relation(sk79),true,ifeq(true,true,subset(relation_dom(relation_rng_restriction(X1,sk79)),relation_dom(sk79)),true),true),true),
inference(cp,[status(thm)],[t146,t804]) ).
fof(f100,axiom,
! [A,B] :
( relation(B)
=> relation(relation_rng_restriction(A,B)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k8_relat_1) ).
fof(f100_nnf,plain,
! [A,B] :
( relation(relation_rng_restriction(A,B))
| ~ relation(B) ),
inference(nnf_transformation,[status(thm)],[f100]) ).
fof(f100_sk,plain,
! [B,A] :
( relation(relation_rng_restriction(A,B))
| ~ relation(B) ),
inference(skolemisation,[status(esa)],[f100_nnf]) ).
cnf(c361,plain,
( relation(relation_rng_restriction(X0,X1))
| ~ relation(X1) ),
inference(cnf_transformation,[status(esa)],[f100_sk]) ).
cnf(t62,plain,
ifeq(relation(X1),true,relation(relation_rng_restriction(X2,X1)),true) = true,
inference(equality_encoding,[status(esa)],[c361]) ).
cnf(t150,plain,
ifeq(relation(X1),true,relation(relation_rng_restriction(X2,X1)),true) = true,
inference(orient,[status(thm)],[t62]) ).
cnf(t302,plain,
true = ifeq(true,true,relation(relation_rng_restriction(X1,sk79)),true),
inference(cp,[status(thm)],[t150,t299]) ).
cnf(t1070,plain,
true = relation(relation_rng_restriction(X1,sk79)),
inference(step,[status(thm)],[t302,t103]) ).
cnf(t721,plain,
relation(relation_rng_restriction(X1,sk79)) = true,
inference(orient,[status(thm)],[t1070]) ).
cnf(t1105,plain,
true = ifeq(true,true,ifeq(relation(sk79),true,ifeq(true,true,subset(relation_dom(relation_rng_restriction(X1,sk79)),relation_dom(sk79)),true),true),true),
inference(step,[status(thm)],[t813,t721]) ).
cnf(t1106,plain,
true = ifeq(relation(sk79),true,ifeq(true,true,subset(relation_dom(relation_rng_restriction(X1,sk79)),relation_dom(sk79)),true),true),
inference(step,[status(thm)],[t1105,t103]) ).
cnf(t1107,plain,
true = ifeq(true,true,ifeq(true,true,subset(relation_dom(relation_rng_restriction(X1,sk79)),relation_dom(sk79)),true),true),
inference(step,[status(thm)],[t1106,t299]) ).
cnf(t1108,plain,
true = ifeq(true,true,subset(relation_dom(relation_rng_restriction(X1,sk79)),relation_dom(sk79)),true),
inference(step,[status(thm)],[t1107,t103]) ).
cnf(t1109,plain,
true = subset(relation_dom(relation_rng_restriction(X1,sk79)),relation_dom(sk79)),
inference(step,[status(thm)],[t1108,t103]) ).
cnf(t962,plain,
subset(relation_dom(relation_rng_restriction(X1,sk79)),relation_dom(sk79)) = true,
inference(orient,[status(thm)],[t1109]) ).
cnf(t1110,plain,
true = false,
inference(step,[status(thm)],[t495,t962]) ).
cnf(t972,plain,
true = false,
inference(rw,[status(thm)],[t1110]) ).
cnf(t973,plain,
false = true,
inference(orient,[status(thm)],[t972]) ).
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(f29,axiom,
! [A] :
( A = empty_set
<=> ! [B] : ~ in(B,A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d1_xboole_0) ).
fof(f29_nnf,plain,
! [A] :
( ( ? [B] : in(B,A)
| A = empty_set )
& ( ! [B] : ~ in(B,A)
| A != empty_set ) ),
inference(nnf_transformation,[status(thm)],[f29]) ).
fof(f29_sk,plain,
! [A,B] :
( ( in(sk25(A),A)
| A = empty_set )
& ( ~ in(B,A)
| A != empty_set ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk25])],[f29_nnf]) ).
cnf(c128,plain,
( ~ in(X1,X0)
| X0 != empty_set ),
inference(cnf_transformation,[status(esa)],[f29_sk]) ).
fof(f50,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(f50_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)],[f50]) ).
fof(f50_sk,plain,
! [C,A,B,D] :
( ( ( ~ in(sk55(A,B,C),B)
& in(sk55(A,B,C),A)
& ~ in(sk55(A,B,C),C) )
| ( ( in(sk55(A,B,C),B)
| ~ in(sk55(A,B,C),A) )
& in(sk55(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,[sk55])],[f50_nnf]) ).
cnf(c246,plain,
( ~ in(X3,X1)
| ~ in(X3,X2)
| X2 != set_difference(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f50_sk]) ).
fof(f66,axiom,
! [A,B] :
( proper_subset(A,B)
<=> ( A != B
& subset(A,B) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d8_xboole_0) ).
fof(f66_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)],[f66]) ).
fof(f66_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)],[f66_nnf]) ).
cnf(c324,plain,
( X0 != X1
| ~ proper_subset(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f66_sk]) ).
fof(f109,axiom,
! [A] : ~ empty(succ(A)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_ordinal1) ).
fof(f109_nnf,plain,
! [A] : ~ empty(succ(A)),
inference(nnf_transformation,[status(thm)],[f109]) ).
fof(f109_sk,plain,
! [A] : ~ empty(succ(A)),
inference(skolemisation,[status(esa)],[f109_nnf]) ).
cnf(c376,plain,
~ empty(succ(X0)),
inference(cnf_transformation,[status(esa)],[f109_sk]) ).
fof(f111,axiom,
! [A] : ~ empty(powerset(A)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_subset_1) ).
fof(f111_nnf,plain,
! [A] : ~ empty(powerset(A)),
inference(nnf_transformation,[status(thm)],[f111]) ).
fof(f111_sk,plain,
! [A] : ~ empty(powerset(A)),
inference(skolemisation,[status(esa)],[f111_nnf]) ).
cnf(c378,plain,
~ empty(powerset(X0)),
inference(cnf_transformation,[status(esa)],[f111_sk]) ).
fof(f113,axiom,
! [A,B] : ~ empty(ordered_pair(A,B)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_zfmisc_1) ).
fof(f113_nnf,plain,
! [A,B] : ~ empty(ordered_pair(A,B)),
inference(nnf_transformation,[status(thm)],[f113]) ).
fof(f113_sk,plain,
! [A,B] : ~ empty(ordered_pair(A,B)),
inference(skolemisation,[status(esa)],[f113_nnf]) ).
cnf(c380,plain,
~ empty(ordered_pair(X0,X1)),
inference(cnf_transformation,[status(esa)],[f113_sk]) ).
fof(f117,axiom,
! [A] : ~ empty(singleton(A)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc2_subset_1) ).
fof(f117_nnf,plain,
! [A] : ~ empty(singleton(A)),
inference(nnf_transformation,[status(thm)],[f117]) ).
fof(f117_sk,plain,
! [A] : ~ empty(singleton(A)),
inference(skolemisation,[status(esa)],[f117_nnf]) ).
cnf(c392,plain,
~ empty(singleton(X0)),
inference(cnf_transformation,[status(esa)],[f117_sk]) ).
fof(f120,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(f120_nnf,plain,
! [A] :
( ( ordinal(succ(A))
& epsilon_connected(succ(A))
& epsilon_transitive(succ(A))
& ~ empty(succ(A)) )
| ~ ordinal(A) ),
inference(nnf_transformation,[status(thm)],[f120]) ).
fof(f120_sk,plain,
! [A] :
( ( ordinal(succ(A))
& epsilon_connected(succ(A))
& epsilon_transitive(succ(A))
& ~ empty(succ(A)) )
| ~ ordinal(A) ),
inference(skolemisation,[status(esa)],[f120_nnf]) ).
cnf(c396,plain,
( ~ empty(succ(X0))
| ~ ordinal(X0) ),
inference(cnf_transformation,[status(esa)],[f120_sk]) ).
fof(f122,axiom,
! [A,B] : ~ empty(unordered_pair(A,B)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc3_subset_1) ).
fof(f122_nnf,plain,
! [A,B] : ~ empty(unordered_pair(A,B)),
inference(nnf_transformation,[status(thm)],[f122]) ).
fof(f122_sk,plain,
! [A,B] : ~ empty(unordered_pair(A,B)),
inference(skolemisation,[status(esa)],[f122_nnf]) ).
cnf(c401,plain,
~ empty(unordered_pair(X0,X1)),
inference(cnf_transformation,[status(esa)],[f122_sk]) ).
fof(f139,axiom,
! [A,B] : ~ proper_subset(A,A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',irreflexivity_r2_xboole_0) ).
fof(f139_nnf,plain,
! [A,B] : ~ proper_subset(A,A),
inference(nnf_transformation,[status(thm)],[f139]) ).
fof(f139_sk,plain,
! [A] : ~ proper_subset(A,A),
inference(skolemisation,[status(esa)],[f139_nnf]) ).
cnf(c426,plain,
~ proper_subset(X0,X0),
inference(cnf_transformation,[status(esa)],[f139_sk]) ).
fof(f141,lemma,
! [A] : singleton(A) != empty_set,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',l1_zfmisc_1) ).
fof(f141_nnf,plain,
! [A] : singleton(A) != empty_set,
inference(nnf_transformation,[status(thm)],[f141]) ).
fof(f141_sk,plain,
! [A] : singleton(A) != empty_set,
inference(skolemisation,[status(esa)],[f141_nnf]) ).
cnf(c430,plain,
singleton(X0) != empty_set,
inference(cnf_transformation,[status(esa)],[f141_sk]) ).
fof(f143,lemma,
! [A,B] :
~ ( in(A,B)
& disjoint(singleton(A),B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',l25_zfmisc_1) ).
fof(f143_nnf,plain,
! [A,B] :
( ~ in(A,B)
| ~ disjoint(singleton(A),B) ),
inference(nnf_transformation,[status(thm)],[f143]) ).
fof(f143_sk,plain,
! [A,B] :
( ~ in(A,B)
| ~ disjoint(singleton(A),B) ),
inference(skolemisation,[status(esa)],[f143_nnf]) ).
cnf(c432,plain,
( ~ in(X0,X1)
| ~ disjoint(singleton(X0),X1) ),
inference(cnf_transformation,[status(esa)],[f143_sk]) ).
fof(f165,axiom,
? [A] :
( relation(A)
& ~ empty(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rc2_relat_1) ).
fof(f165_nnf,plain,
? [A] :
( relation(A)
& ~ empty(A) ),
inference(nnf_transformation,[status(thm)],[f165]) ).
fof(f165_sk,plain,
( relation(sk95)
& ~ empty(sk95) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk95])],[f165_nnf]) ).
cnf(c488,plain,
~ empty(sk95),
inference(cnf_transformation,[status(esa)],[f165_sk]) ).
fof(f167,axiom,
? [A] : ~ empty(A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rc2_xboole_0) ).
fof(f167_nnf,plain,
? [A] : ~ empty(A),
inference(nnf_transformation,[status(thm)],[f167]) ).
fof(f167_sk,plain,
~ empty(sk97),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk97])],[f167_nnf]) ).
cnf(c492,plain,
~ empty(sk97),
inference(cnf_transformation,[status(esa)],[f167_sk]) ).
fof(f169,axiom,
? [A] :
( ordinal(A)
& epsilon_connected(A)
& epsilon_transitive(A)
& ~ empty(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rc3_ordinal1) ).
fof(f169_nnf,plain,
? [A] :
( ordinal(A)
& epsilon_connected(A)
& epsilon_transitive(A)
& ~ empty(A) ),
inference(nnf_transformation,[status(thm)],[f169]) ).
fof(f169_sk,plain,
( ordinal(sk99)
& epsilon_connected(sk99)
& epsilon_transitive(sk99)
& ~ empty(sk99) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk99])],[f169_nnf]) ).
cnf(c496,plain,
~ empty(sk99),
inference(cnf_transformation,[status(esa)],[f169_sk]) ).
fof(f244,lemma,
! [A,B,C] :
~ ( in(C,A)
& in(B,C)
& in(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t3_ordinal1) ).
fof(f244_nnf,plain,
! [A,B,C] :
( ~ in(C,A)
| ~ in(B,C)
| ~ in(A,B) ),
inference(nnf_transformation,[status(thm)],[f244]) ).
fof(f244_sk,plain,
! [A,B,C] :
( ~ in(C,A)
| ~ in(B,C)
| ~ in(A,B) ),
inference(skolemisation,[status(esa)],[f244_nnf]) ).
cnf(c617,plain,
( ~ in(X2,X0)
| ~ in(X1,X2)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f244_sk]) ).
fof(f246,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(f246_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)],[f246]) ).
fof(f246_sk,plain,
! [A,B,C] :
( ( ~ disjoint(A,B)
| ~ in(C,B)
| ~ in(C,A) )
& ( ( in(sk109(A,B),B)
& in(sk109(A,B),A) )
| disjoint(A,B) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk109])],[f246_nnf]) ).
cnf(c622,plain,
( ~ disjoint(X0,X1)
| ~ in(X2,X1)
| ~ in(X2,X0) ),
inference(cnf_transformation,[status(esa)],[f246_sk]) ).
fof(f250,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(f250_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)],[f250]) ).
fof(f250_sk,plain,
! [A,B] :
( ( ( ~ being_limit_ordinal(A)
| A != succ(B)
| ~ ordinal(B) )
& ( ( A = succ(sk111(A))
& ordinal(sk111(A)) )
| being_limit_ordinal(A) ) )
| ~ ordinal(A) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk111])],[f250_nnf]) ).
cnf(c631,plain,
( ~ being_limit_ordinal(X0)
| X0 != succ(X1)
| ~ ordinal(X1)
| ~ ordinal(X0) ),
inference(cnf_transformation,[status(esa)],[f250_sk]) ).
fof(f264,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(f264_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)],[f264]) ).
fof(f264_sk,plain,
! [A,B,C] :
( ( ~ disjoint(A,B)
| ~ in(C,set_intersection2(A,B)) )
& ( in(sk112(A,B),set_intersection2(A,B))
| disjoint(A,B) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk112])],[f264_nnf]) ).
cnf(c647,plain,
( ~ disjoint(X0,X1)
| ~ in(X2,set_intersection2(X0,X1)) ),
inference(cnf_transformation,[status(esa)],[f264_sk]) ).
fof(f267,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(f267_nnf,plain,
! [A,B,C] :
( ~ in(B,C)
| ~ in(B,subset_complement(A,C))
| ~ element(C,powerset(A)) ),
inference(nnf_transformation,[status(thm)],[f267]) ).
fof(f267_sk,plain,
! [C,A,B] :
( ~ in(B,C)
| ~ in(B,subset_complement(A,C))
| ~ element(C,powerset(A)) ),
inference(skolemisation,[status(esa)],[f267_nnf]) ).
cnf(c663,plain,
( ~ in(X1,X2)
| ~ in(X1,subset_complement(X0,X2))
| ~ element(X2,powerset(X0)) ),
inference(cnf_transformation,[status(esa)],[f267_sk]) ).
fof(f271,axiom,
! [A,B,C] :
~ ( empty(C)
& element(B,powerset(C))
& in(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t5_subset) ).
fof(f271_nnf,plain,
! [A,B,C] :
( ~ empty(C)
| ~ element(B,powerset(C))
| ~ in(A,B) ),
inference(nnf_transformation,[status(thm)],[f271]) ).
fof(f271_sk,plain,
! [A,B,C] :
( ~ empty(C)
| ~ element(B,powerset(C))
| ~ in(A,B) ),
inference(skolemisation,[status(esa)],[f271_nnf]) ).
cnf(c669,plain,
( ~ empty(X2)
| ~ element(X1,powerset(X2))
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f271_sk]) ).
fof(f274,lemma,
! [A,B] :
~ ( proper_subset(B,A)
& subset(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t60_xboole_1) ).
fof(f274_nnf,plain,
! [A,B] :
( ~ proper_subset(B,A)
| ~ subset(A,B) ),
inference(nnf_transformation,[status(thm)],[f274]) ).
fof(f274_sk,plain,
! [A,B] :
( ~ proper_subset(B,A)
| ~ subset(A,B) ),
inference(skolemisation,[status(esa)],[f274_nnf]) ).
cnf(c674,plain,
( ~ proper_subset(X1,X0)
| ~ subset(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f274_sk]) ).
fof(f279,lemma,
! [A,B] :
( set_difference(A,singleton(B)) = A
<=> ~ in(B,A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t65_zfmisc_1) ).
fof(f279_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)],[f279]) ).
fof(f279_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)],[f279_nnf]) ).
cnf(c681,plain,
( ~ in(X1,X0)
| set_difference(X0,singleton(X1)) != X0 ),
inference(cnf_transformation,[status(esa)],[f279_sk]) ).
fof(f288,axiom,
! [A,B] :
~ ( empty(B)
& in(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t7_boole) ).
fof(f288_nnf,plain,
! [A,B] :
( ~ empty(B)
| ~ in(A,B) ),
inference(nnf_transformation,[status(thm)],[f288]) ).
fof(f288_sk,plain,
! [A,B] :
( ~ empty(B)
| ~ in(A,B) ),
inference(skolemisation,[status(esa)],[f288_nnf]) ).
cnf(c697,plain,
( ~ empty(X1)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f288_sk]) ).
fof(f289,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(f289_nnf,plain,
! [A,B] :
( ? [C] :
( ! [D] :
( ~ in(D,C)
| ~ in(D,B) )
& in(C,B) )
| ~ in(A,B) ),
inference(nnf_transformation,[status(thm)],[f289]) ).
fof(f289_sk,plain,
! [A,B,D] :
( ( ( ~ in(D,sk118(A,B))
| ~ in(D,B) )
& in(sk118(A,B),B) )
| ~ in(A,B) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk118])],[f289_nnf]) ).
cnf(c699,plain,
( ~ in(X3,sk118(X0,X1))
| ~ in(X3,X1)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f289_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c0,c1,c128,c246,c324,c376,c378,c380,c392,c396,c401,c426,c430,c432,c435,c488,c492,c496,c617,c622,c631,c647,c663,c669,c674,c681,c697,c699]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t973]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU248+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/5.36 % Computer : n004.cluster.edu
% 0.10/5.36 % Model : x86_64 x86_64
% 0.10/5.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/5.36 % Memory : 8046.5625MB
% 0.10/5.36 % OS : Linux 6.8.0-71-generic
% 0.10/5.36 % CPULimit : 300
% 0.10/5.36 % WCLimit : 300
% 0.10/5.36 % DateTime : Thu Sep 24 13:24:13 UTC 2026
% 0.10/5.36 % CPUTime :
% 0.10/5.36 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 61.11/13.49 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 61.11/13.49 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------