%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SEU264+2 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n001.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:32 PM UTC 2026
% Result : Theorem 70.91s 14.33s
% Output : Proof 70.91s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 34
% Syntax : Number of formulae : 173 ( 79 unt; 0 def)
% Number of atoms : 427 ( 88 equ)
% Maximal formula atoms : 15 ( 2 avg)
% Number of connectives : 500 ( 246 ~; 133 |; 99 &)
% ( 7 <=>; 15 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 14 ( 12 usr; 1 prp; 0-3 aty)
% Number of functors : 29 ( 29 usr; 10 con; 0-4 aty)
% Number of variables : 330 ( 26 sgn 208 !; 20 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f209,lemma,
! [A,B,C,D] :
( relation_of2_as_subset(D,C,A)
=> ( subset(relation_rng(D),B)
=> relation_of2_as_subset(D,C,B) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t14_relset_1) ).
fof(f209_nnf,plain,
! [A,B,C,D] :
( relation_of2_as_subset(D,C,B)
| ~ subset(relation_rng(D),B)
| ~ relation_of2_as_subset(D,C,A) ),
inference(nnf_transformation,[status(thm)],[f209]) ).
fof(f209_sk,plain,
! [D,C,A,B] :
( relation_of2_as_subset(D,C,B)
| ~ subset(relation_rng(D),B)
| ~ relation_of2_as_subset(D,C,A) ),
inference(skolemisation,[status(esa)],[f209_nnf]) ).
cnf(c578,plain,
( relation_of2_as_subset(X3,X2,X1)
| ~ subset(relation_rng(X3),X1)
| ~ relation_of2_as_subset(X3,X2,X0) ),
inference(cnf_transformation,[status(esa)],[f209_sk]) ).
cnf(t155,plain,
ifeq(relation_of2_as_subset(X1,X2,X3),true,ifeq(subset(relation_rng(X1),X4),true,relation_of2_as_subset(X1,X2,X4),true),true) = true,
inference(equality_encoding,[status(esa)],[c578]) ).
cnf(t227,plain,
ifeq(relation_of2_as_subset(X1,X2,X3),true,ifeq(subset(relation_rng(X1),X4),true,relation_of2_as_subset(X1,X2,X4),true),true) = true,
inference(orient,[status(thm)],[t155]) ).
cnf(hi483,axiom,
ifeq(relation_of2_as_subset(X0,X1,X2),true,ifeq(subset(relation_rng(X0),X3),true,relation_of2_as_subset(X0,X1,X3),true),true) = true,
inference(equality_encoding,[status(esa)],[c578]) ).
fof(f213,conjecture,
! [A,B,C,D] :
( relation_of2_as_subset(D,C,A)
=> ( subset(A,B)
=> relation_of2_as_subset(D,C,B) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t16_relset_1) ).
fof(f213_neg,negated_conjecture,
~ ! [A,B,C,D] :
( relation_of2_as_subset(D,C,A)
=> ( subset(A,B)
=> relation_of2_as_subset(D,C,B) ) ),
inference(negated_conjecture,[status(cth)],[f213]) ).
fof(f213_nnf,plain,
? [A,B,C,D] :
( ~ relation_of2_as_subset(D,C,B)
& subset(A,B)
& relation_of2_as_subset(D,C,A) ),
inference(nnf_transformation,[status(thm)],[f213_neg]) ).
fof(f213_sk,plain,
( ~ relation_of2_as_subset(sk111,sk110,sk109)
& subset(sk108,sk109)
& relation_of2_as_subset(sk111,sk110,sk108) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk108,sk109,sk110,sk111])],[f213_nnf]) ).
cnf(c585,plain,
relation_of2_as_subset(sk111,sk110,sk108),
inference(cnf_transformation,[status(esa)],[f213_sk]) ).
cnf(hi490,negated_conjecture,
relation_of2_as_subset(sk111,sk110,sk108) = true,
inference(equality_encoding,[status(esa)],[c585]) ).
fof(f186,axiom,
! [A,B] : subset(A,A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',reflexivity_r1_tarski) ).
fof(f186_nnf,plain,
! [A,B] : subset(A,A),
inference(nnf_transformation,[status(thm)],[f186]) ).
fof(f186_sk,plain,
! [A] : subset(A,A),
inference(skolemisation,[status(esa)],[f186_nnf]) ).
cnf(c543,plain,
subset(X0,X0),
inference(cnf_transformation,[status(esa)],[f186_sk]) ).
cnf(hi448,axiom,
subset(X0,X0) = true,
inference(equality_encoding,[status(esa)],[c543]) ).
cnf(t83,plain,
relation_of2_as_subset(sk111,sk110,relation_rng(sk111)) = true,
inference(hyper_resolution,[status(thm)],[hi483,hi490,hi448]) ).
cnf(t593,plain,
relation_of2_as_subset(sk111,sk110,relation_rng(sk111)) = true,
inference(orient,[status(thm)],[t83]) ).
cnf(t596,plain,
true = ifeq(true,true,ifeq(subset(relation_rng(sk111),X1),true,relation_of2_as_subset(sk111,sk110,X1),true),true),
inference(cp,[status(thm)],[t227,t593]) ).
cnf(t82,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t163,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t82]) ).
cnf(t6246,plain,
true = ifeq(subset(relation_rng(sk111),X1),true,relation_of2_as_subset(sk111,sk110,X1),true),
inference(step,[status(thm)],[t596,t163]) ).
cnf(t5521,plain,
ifeq(subset(relation_rng(sk111),X1),true,relation_of2_as_subset(sk111,sk110,X1),true) = true,
inference(orient,[status(thm)],[t6246]) ).
fof(f224,lemma,
! [A,B,C] :
( ( subset(B,C)
& subset(A,B) )
=> subset(A,C) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t1_xboole_1) ).
fof(f224_nnf,plain,
! [A,B,C] :
( subset(A,C)
| ~ subset(B,C)
| ~ subset(A,B) ),
inference(nnf_transformation,[status(thm)],[f224]) ).
fof(f224_sk,plain,
! [A,B,C] :
( subset(A,C)
| ~ subset(B,C)
| ~ subset(A,B) ),
inference(skolemisation,[status(esa)],[f224_nnf]) ).
cnf(c601,plain,
( subset(X0,X2)
| ~ subset(X1,X2)
| ~ subset(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f224_sk]) ).
cnf(t150,plain,
ifeq(subset(X1,X2),true,ifeq(subset(X2,X3),true,subset(X1,X3),true),true) = true,
inference(equality_encoding,[status(esa)],[c601]) ).
cnf(t198,plain,
ifeq(subset(X1,X2),true,ifeq(subset(X2,X3),true,subset(X1,X3),true),true) = true,
inference(orient,[status(thm)],[t150]) ).
cnf(c586,plain,
subset(sk108,sk109),
inference(cnf_transformation,[status(esa)],[f213_sk]) ).
cnf(t63,plain,
subset(sk108,sk109) = true,
inference(equality_encoding,[status(esa)],[c586]) ).
cnf(t427,plain,
subset(sk108,sk109) = true,
inference(orient,[status(thm)],[t63]) ).
cnf(t437,plain,
true = ifeq(subset(X1,sk108),true,ifeq(true,true,subset(X1,sk109),true),true),
inference(cp,[status(thm)],[t198,t427]) ).
cnf(t5853,plain,
true = ifeq(subset(X1,sk108),true,subset(X1,sk109),true),
inference(step,[status(thm)],[t437,t163]) ).
cnf(t2149,plain,
ifeq(subset(X1,sk108),true,subset(X1,sk109),true) = true,
inference(orient,[status(thm)],[t5853]) ).
fof(f198,lemma,
! [A,B,C] :
( relation_of2_as_subset(C,A,B)
=> ( subset(relation_rng(C),B)
& subset(relation_dom(C),A) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t12_relset_1) ).
fof(f198_nnf,plain,
! [A,B,C] :
( ( subset(relation_rng(C),B)
& subset(relation_dom(C),A) )
| ~ relation_of2_as_subset(C,A,B) ),
inference(nnf_transformation,[status(thm)],[f198]) ).
fof(f198_sk,plain,
! [C,A,B] :
( ( subset(relation_rng(C),B)
& subset(relation_dom(C),A) )
| ~ relation_of2_as_subset(C,A,B) ),
inference(skolemisation,[status(esa)],[f198_nnf]) ).
cnf(c561,plain,
( subset(relation_rng(X2),X1)
| ~ relation_of2_as_subset(X2,X0,X1) ),
inference(cnf_transformation,[status(esa)],[f198_sk]) ).
cnf(t129,plain,
ifeq(relation_of2_as_subset(X1,X2,X3),true,subset(relation_rng(X1),X3),true) = true,
inference(equality_encoding,[status(esa)],[c561]) ).
cnf(t228,plain,
ifeq(relation_of2_as_subset(X1,X2,X3),true,subset(relation_rng(X1),X3),true) = true,
inference(orient,[status(thm)],[t129]) ).
cnf(t67,plain,
relation_of2_as_subset(sk111,sk110,sk108) = true,
inference(equality_encoding,[status(esa)],[c585]) ).
cnf(t604,plain,
relation_of2_as_subset(sk111,sk110,sk108) = true,
inference(orient,[status(thm)],[t67]) ).
cnf(t606,plain,
true = ifeq(true,true,subset(relation_rng(sk111),sk108),true),
inference(cp,[status(thm)],[t228,t604]) ).
cnf(t5679,plain,
true = subset(relation_rng(sk111),sk108),
inference(step,[status(thm)],[t606,t163]) ).
cnf(t843,plain,
subset(relation_rng(sk111),sk108) = true,
inference(orient,[status(thm)],[t5679]) ).
cnf(t2150,plain,
true = ifeq(true,true,subset(relation_rng(sk111),sk109),true),
inference(cp,[status(thm)],[t2149,t843]) ).
cnf(t5854,plain,
true = subset(relation_rng(sk111),sk109),
inference(step,[status(thm)],[t2150,t163]) ).
cnf(t2151,plain,
subset(relation_rng(sk111),sk109) = true,
inference(orient,[status(thm)],[t5854]) ).
cnf(t5522,plain,
true = ifeq(true,true,relation_of2_as_subset(sk111,sk110,sk109),true),
inference(cp,[status(thm)],[t5521,t2151]) ).
cnf(t6247,plain,
true = relation_of2_as_subset(sk111,sk110,sk109),
inference(step,[status(thm)],[t5522,t163]) ).
cnf(c587,plain,
~ relation_of2_as_subset(sk111,sk110,sk109),
inference(cnf_transformation,[status(esa)],[f213_sk]) ).
cnf(t68,plain,
relation_of2_as_subset(sk111,sk110,sk109) = false,
inference(equality_encoding,[status(esa)],[c587]) ).
cnf(t730,plain,
relation_of2_as_subset(sk111,sk110,sk109) = false,
inference(orient,[status(thm)],[t68]) ).
cnf(t6248,plain,
true = false,
inference(step,[status(thm)],[t6247,t730]) ).
cnf(t5524,plain,
false = true,
inference(orient,[status(thm)],[t6248]) ).
fof(f0,axiom,
! [A,B] :
( in(A,B)
=> ~ in(B,A) ),
file('/export/starexec/sandbox/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/sandbox/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(f31,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/sandbox/benchmark/theBenchmark.p',d1_wellord1) ).
fof(f31_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)],[f31]) ).
fof(f31_sk,plain,
! [A,C,B,D] :
( ( ( ( in(ordered_pair(sk25(A,B,C),B),A)
& sk25(A,B,C) != B
& ~ in(sk25(A,B,C),C) )
| ( ( ~ in(ordered_pair(sk25(A,B,C),B),A)
| sk25(A,B,C) = B )
& in(sk25(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,[sk25])],[f31_nnf]) ).
cnf(c131,plain,
( X3 != X1
| ~ in(X3,X2)
| X2 != fiber(X0,X1)
| ~ relation(X0) ),
inference(cnf_transformation,[status(esa)],[f31_sk]) ).
fof(f32,axiom,
! [A] :
( A = empty_set
<=> ! [B] : ~ in(B,A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d1_xboole_0) ).
fof(f32_nnf,plain,
! [A] :
( ( ? [B] : in(B,A)
| A = empty_set )
& ( ! [B] : ~ in(B,A)
| A != empty_set ) ),
inference(nnf_transformation,[status(thm)],[f32]) ).
fof(f32_sk,plain,
! [A,B] :
( ( in(sk26(A),A)
| A = empty_set )
& ( ~ in(B,A)
| A != empty_set ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk26])],[f32_nnf]) ).
cnf(c140,plain,
( ~ in(X1,X0)
| X0 != empty_set ),
inference(cnf_transformation,[status(esa)],[f32_sk]) ).
fof(f53,axiom,
! [A,B,C] :
( C = set_difference(A,B)
<=> ! [D] :
( in(D,C)
<=> ( ~ in(D,B)
& in(D,A) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d4_xboole_0) ).
fof(f53_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)],[f53]) ).
fof(f53_sk,plain,
! [C,A,B,D] :
( ( ( ~ in(sk56(A,B,C),B)
& in(sk56(A,B,C),A)
& ~ in(sk56(A,B,C),C) )
| ( ( in(sk56(A,B,C),B)
| ~ in(sk56(A,B,C),A) )
& in(sk56(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,[sk56])],[f53_nnf]) ).
cnf(c258,plain,
( ~ in(X3,X1)
| ~ in(X3,X2)
| X2 != set_difference(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f53_sk]) ).
fof(f70,axiom,
! [A,B] :
( proper_subset(A,B)
<=> ( A != B
& subset(A,B) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d8_xboole_0) ).
fof(f70_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)],[f70]) ).
fof(f70_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)],[f70_nnf]) ).
cnf(c351,plain,
( X0 != X1
| ~ proper_subset(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f70_sk]) ).
fof(f117,axiom,
! [A] : ~ empty(succ(A)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc1_ordinal1) ).
fof(f117_nnf,plain,
! [A] : ~ empty(succ(A)),
inference(nnf_transformation,[status(thm)],[f117]) ).
fof(f117_sk,plain,
! [A] : ~ empty(succ(A)),
inference(skolemisation,[status(esa)],[f117_nnf]) ).
cnf(c407,plain,
~ empty(succ(X0)),
inference(cnf_transformation,[status(esa)],[f117_sk]) ).
fof(f119,axiom,
! [A] : ~ empty(powerset(A)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc1_subset_1) ).
fof(f119_nnf,plain,
! [A] : ~ empty(powerset(A)),
inference(nnf_transformation,[status(thm)],[f119]) ).
fof(f119_sk,plain,
! [A] : ~ empty(powerset(A)),
inference(skolemisation,[status(esa)],[f119_nnf]) ).
cnf(c409,plain,
~ empty(powerset(X0)),
inference(cnf_transformation,[status(esa)],[f119_sk]) ).
fof(f121,axiom,
! [A,B] : ~ empty(ordered_pair(A,B)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc1_zfmisc_1) ).
fof(f121_nnf,plain,
! [A,B] : ~ empty(ordered_pair(A,B)),
inference(nnf_transformation,[status(thm)],[f121]) ).
fof(f121_sk,plain,
! [A,B] : ~ empty(ordered_pair(A,B)),
inference(skolemisation,[status(esa)],[f121_nnf]) ).
cnf(c411,plain,
~ empty(ordered_pair(X0,X1)),
inference(cnf_transformation,[status(esa)],[f121_sk]) ).
fof(f125,axiom,
! [A] : ~ empty(singleton(A)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc2_subset_1) ).
fof(f125_nnf,plain,
! [A] : ~ empty(singleton(A)),
inference(nnf_transformation,[status(thm)],[f125]) ).
fof(f125_sk,plain,
! [A] : ~ empty(singleton(A)),
inference(skolemisation,[status(esa)],[f125_nnf]) ).
cnf(c423,plain,
~ empty(singleton(X0)),
inference(cnf_transformation,[status(esa)],[f125_sk]) ).
fof(f128,axiom,
! [A] :
( ordinal(A)
=> ( ordinal(succ(A))
& epsilon_connected(succ(A))
& epsilon_transitive(succ(A))
& ~ empty(succ(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc3_ordinal1) ).
fof(f128_nnf,plain,
! [A] :
( ( ordinal(succ(A))
& epsilon_connected(succ(A))
& epsilon_transitive(succ(A))
& ~ empty(succ(A)) )
| ~ ordinal(A) ),
inference(nnf_transformation,[status(thm)],[f128]) ).
fof(f128_sk,plain,
! [A] :
( ( ordinal(succ(A))
& epsilon_connected(succ(A))
& epsilon_transitive(succ(A))
& ~ empty(succ(A)) )
| ~ ordinal(A) ),
inference(skolemisation,[status(esa)],[f128_nnf]) ).
cnf(c427,plain,
( ~ empty(succ(X0))
| ~ ordinal(X0) ),
inference(cnf_transformation,[status(esa)],[f128_sk]) ).
fof(f130,axiom,
! [A,B] : ~ empty(unordered_pair(A,B)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc3_subset_1) ).
fof(f130_nnf,plain,
! [A,B] : ~ empty(unordered_pair(A,B)),
inference(nnf_transformation,[status(thm)],[f130]) ).
fof(f130_sk,plain,
! [A,B] : ~ empty(unordered_pair(A,B)),
inference(skolemisation,[status(esa)],[f130_nnf]) ).
cnf(c432,plain,
~ empty(unordered_pair(X0,X1)),
inference(cnf_transformation,[status(esa)],[f130_sk]) ).
fof(f147,axiom,
! [A,B] : ~ proper_subset(A,A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',irreflexivity_r2_xboole_0) ).
fof(f147_nnf,plain,
! [A,B] : ~ proper_subset(A,A),
inference(nnf_transformation,[status(thm)],[f147]) ).
fof(f147_sk,plain,
! [A] : ~ proper_subset(A,A),
inference(skolemisation,[status(esa)],[f147_nnf]) ).
cnf(c457,plain,
~ proper_subset(X0,X0),
inference(cnf_transformation,[status(esa)],[f147_sk]) ).
fof(f149,lemma,
! [A] : singleton(A) != empty_set,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',l1_zfmisc_1) ).
fof(f149_nnf,plain,
! [A] : singleton(A) != empty_set,
inference(nnf_transformation,[status(thm)],[f149]) ).
fof(f149_sk,plain,
! [A] : singleton(A) != empty_set,
inference(skolemisation,[status(esa)],[f149_nnf]) ).
cnf(c461,plain,
singleton(X0) != empty_set,
inference(cnf_transformation,[status(esa)],[f149_sk]) ).
fof(f151,lemma,
! [A,B] :
~ ( in(A,B)
& disjoint(singleton(A),B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',l25_zfmisc_1) ).
fof(f151_nnf,plain,
! [A,B] :
( ~ in(A,B)
| ~ disjoint(singleton(A),B) ),
inference(nnf_transformation,[status(thm)],[f151]) ).
fof(f151_sk,plain,
! [A,B] :
( ~ in(A,B)
| ~ disjoint(singleton(A),B) ),
inference(skolemisation,[status(esa)],[f151_nnf]) ).
cnf(c463,plain,
( ~ in(X0,X1)
| ~ disjoint(singleton(X0),X1) ),
inference(cnf_transformation,[status(esa)],[f151_sk]) ).
fof(f173,axiom,
? [A] :
( relation(A)
& ~ empty(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc2_relat_1) ).
fof(f173_nnf,plain,
? [A] :
( relation(A)
& ~ empty(A) ),
inference(nnf_transformation,[status(thm)],[f173]) ).
fof(f173_sk,plain,
( relation(sk98)
& ~ empty(sk98) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk98])],[f173_nnf]) ).
cnf(c518,plain,
~ empty(sk98),
inference(cnf_transformation,[status(esa)],[f173_sk]) ).
fof(f175,axiom,
? [A] : ~ empty(A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc2_xboole_0) ).
fof(f175_nnf,plain,
? [A] : ~ empty(A),
inference(nnf_transformation,[status(thm)],[f175]) ).
fof(f175_sk,plain,
~ empty(sk100),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk100])],[f175_nnf]) ).
cnf(c522,plain,
~ empty(sk100),
inference(cnf_transformation,[status(esa)],[f175_sk]) ).
fof(f177,axiom,
? [A] :
( ordinal(A)
& epsilon_connected(A)
& epsilon_transitive(A)
& ~ empty(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc3_ordinal1) ).
fof(f177_nnf,plain,
? [A] :
( ordinal(A)
& epsilon_connected(A)
& epsilon_transitive(A)
& ~ empty(A) ),
inference(nnf_transformation,[status(thm)],[f177]) ).
fof(f177_sk,plain,
( ordinal(sk102)
& epsilon_connected(sk102)
& epsilon_transitive(sk102)
& ~ empty(sk102) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk102])],[f177_nnf]) ).
cnf(c526,plain,
~ empty(sk102),
inference(cnf_transformation,[status(esa)],[f177_sk]) ).
fof(f266,lemma,
! [A,B,C] :
~ ( in(C,A)
& in(B,C)
& in(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t3_ordinal1) ).
fof(f266_nnf,plain,
! [A,B,C] :
( ~ in(C,A)
| ~ in(B,C)
| ~ in(A,B) ),
inference(nnf_transformation,[status(thm)],[f266]) ).
fof(f266_sk,plain,
! [A,B,C] :
( ~ in(C,A)
| ~ in(B,C)
| ~ in(A,B) ),
inference(skolemisation,[status(esa)],[f266_nnf]) ).
cnf(c667,plain,
( ~ in(X2,X0)
| ~ in(X1,X2)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f266_sk]) ).
fof(f268,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/sandbox/benchmark/theBenchmark.p',t3_xboole_0) ).
fof(f268_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)],[f268]) ).
fof(f268_sk,plain,
! [A,B,C] :
( ( ~ disjoint(A,B)
| ~ in(C,B)
| ~ in(C,A) )
& ( ( in(sk116(A,B),B)
& in(sk116(A,B),A) )
| disjoint(A,B) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk116])],[f268_nnf]) ).
cnf(c672,plain,
( ~ disjoint(X0,X1)
| ~ in(X2,X1)
| ~ in(X2,X0) ),
inference(cnf_transformation,[status(esa)],[f268_sk]) ).
fof(f272,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/sandbox/benchmark/theBenchmark.p',t42_ordinal1) ).
fof(f272_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)],[f272]) ).
fof(f272_sk,plain,
! [A,B] :
( ( ( ~ being_limit_ordinal(A)
| A != succ(B)
| ~ ordinal(B) )
& ( ( A = succ(sk118(A))
& ordinal(sk118(A)) )
| being_limit_ordinal(A) ) )
| ~ ordinal(A) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk118])],[f272_nnf]) ).
cnf(c681,plain,
( ~ being_limit_ordinal(X0)
| X0 != succ(X1)
| ~ ordinal(X1)
| ~ ordinal(X0) ),
inference(cnf_transformation,[status(esa)],[f272_sk]) ).
fof(f287,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/sandbox/benchmark/theBenchmark.p',t4_xboole_0) ).
fof(f287_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)],[f287]) ).
fof(f287_sk,plain,
! [A,B,C] :
( ( ~ disjoint(A,B)
| ~ in(C,set_intersection2(A,B)) )
& ( in(sk119(A,B),set_intersection2(A,B))
| disjoint(A,B) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk119])],[f287_nnf]) ).
cnf(c698,plain,
( ~ disjoint(X0,X1)
| ~ in(X2,set_intersection2(X0,X1)) ),
inference(cnf_transformation,[status(esa)],[f287_sk]) ).
fof(f291,lemma,
! [A,B,C] :
( element(C,powerset(A))
=> ~ ( in(B,C)
& in(B,subset_complement(A,C)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t54_subset_1) ).
fof(f291_nnf,plain,
! [A,B,C] :
( ~ in(B,C)
| ~ in(B,subset_complement(A,C))
| ~ element(C,powerset(A)) ),
inference(nnf_transformation,[status(thm)],[f291]) ).
fof(f291_sk,plain,
! [C,A,B] :
( ~ in(B,C)
| ~ in(B,subset_complement(A,C))
| ~ element(C,powerset(A)) ),
inference(skolemisation,[status(esa)],[f291_nnf]) ).
cnf(c719,plain,
( ~ in(X1,X2)
| ~ in(X1,subset_complement(X0,X2))
| ~ element(X2,powerset(X0)) ),
inference(cnf_transformation,[status(esa)],[f291_sk]) ).
fof(f296,axiom,
! [A,B,C] :
~ ( empty(C)
& element(B,powerset(C))
& in(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t5_subset) ).
fof(f296_nnf,plain,
! [A,B,C] :
( ~ empty(C)
| ~ element(B,powerset(C))
| ~ in(A,B) ),
inference(nnf_transformation,[status(thm)],[f296]) ).
fof(f296_sk,plain,
! [A,B,C] :
( ~ empty(C)
| ~ element(B,powerset(C))
| ~ in(A,B) ),
inference(skolemisation,[status(esa)],[f296_nnf]) ).
cnf(c726,plain,
( ~ empty(X2)
| ~ element(X1,powerset(X2))
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f296_sk]) ).
fof(f299,lemma,
! [A,B] :
~ ( proper_subset(B,A)
& subset(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t60_xboole_1) ).
fof(f299_nnf,plain,
! [A,B] :
( ~ proper_subset(B,A)
| ~ subset(A,B) ),
inference(nnf_transformation,[status(thm)],[f299]) ).
fof(f299_sk,plain,
! [A,B] :
( ~ proper_subset(B,A)
| ~ subset(A,B) ),
inference(skolemisation,[status(esa)],[f299_nnf]) ).
cnf(c731,plain,
( ~ proper_subset(X1,X0)
| ~ subset(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f299_sk]) ).
fof(f304,lemma,
! [A,B] :
( set_difference(A,singleton(B)) = A
<=> ~ in(B,A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t65_zfmisc_1) ).
fof(f304_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)],[f304]) ).
fof(f304_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)],[f304_nnf]) ).
cnf(c738,plain,
( ~ in(X1,X0)
| set_difference(X0,singleton(X1)) != X0 ),
inference(cnf_transformation,[status(esa)],[f304_sk]) ).
fof(f313,axiom,
! [A,B] :
~ ( empty(B)
& in(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t7_boole) ).
fof(f313_nnf,plain,
! [A,B] :
( ~ empty(B)
| ~ in(A,B) ),
inference(nnf_transformation,[status(thm)],[f313]) ).
fof(f313_sk,plain,
! [A,B] :
( ~ empty(B)
| ~ in(A,B) ),
inference(skolemisation,[status(esa)],[f313_nnf]) ).
cnf(c754,plain,
( ~ empty(X1)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f313_sk]) ).
fof(f314,axiom,
! [A,B] :
~ ( ! [C] :
~ ( ! [D] :
~ ( in(D,C)
& in(D,B) )
& in(C,B) )
& in(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t7_tarski) ).
fof(f314_nnf,plain,
! [A,B] :
( ? [C] :
( ! [D] :
( ~ in(D,C)
| ~ in(D,B) )
& in(C,B) )
| ~ in(A,B) ),
inference(nnf_transformation,[status(thm)],[f314]) ).
fof(f314_sk,plain,
! [A,B,D] :
( ( ( ~ in(D,sk125(A,B))
| ~ in(D,B) )
& in(sk125(A,B),B) )
| ~ in(A,B) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk125])],[f314_nnf]) ).
cnf(c756,plain,
( ~ in(X3,sk125(X0,X1))
| ~ in(X3,X1)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f314_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c0,c1,c131,c140,c258,c351,c407,c409,c411,c423,c427,c432,c457,c461,c463,c518,c522,c526,c587,c667,c672,c681,c698,c719,c726,c731,c738,c754,c756]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t5524]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU264+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.11/5.37 % Computer : n001.cluster.edu
% 0.11/5.37 % Model : x86_64 x86_64
% 0.11/5.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/5.37 % Memory : 8046.5625MB
% 0.11/5.37 % OS : Linux 6.8.0-71-generic
% 0.11/5.37 % CPULimit : 300
% 0.11/5.37 % WCLimit : 300
% 0.11/5.37 % DateTime : Thu Sep 24 13:33:12 UTC 2026
% 0.11/5.37 % CPUTime :
% 0.11/5.37 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 70.91/14.33 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 70.91/14.33 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------