%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SEU263+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 : n005.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 126.35s 16.78s
% Output : Proof 126.35s
% Verified :
% SZS Type : Refutation
% Derivation depth : 41
% Number of leaves : 47
% Syntax : Number of formulae : 316 ( 179 unt; 0 def)
% Number of atoms : 646 ( 196 equ)
% Maximal formula atoms : 15 ( 2 avg)
% Number of connectives : 610 ( 280 ~; 165 |; 137 &)
% ( 10 <=>; 18 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 3 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 17 ( 15 usr; 1 prp; 0-3 aty)
% Number of functors : 34 ( 34 usr; 13 con; 0-4 aty)
% Number of variables : 533 ( 50 sgn 269 !; 26 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f183,axiom,
! [A,B,C] :
( relation_of2_as_subset(C,A,B)
<=> relation_of2(C,A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_m2_relset_1) ).
fof(f183_nnf,plain,
! [A,B,C] :
( ( ~ relation_of2(C,A,B)
| relation_of2_as_subset(C,A,B) )
& ( relation_of2(C,A,B)
| ~ relation_of2_as_subset(C,A,B) ) ),
inference(nnf_transformation,[status(thm)],[f183]) ).
fof(f183_sk,plain,
! [C,A,B] :
( ( ~ relation_of2(C,A,B)
| relation_of2_as_subset(C,A,B) )
& ( relation_of2(C,A,B)
| ~ relation_of2_as_subset(C,A,B) ) ),
inference(skolemisation,[status(esa)],[f183_nnf]) ).
cnf(c539,plain,
( ~ relation_of2(X2,X0,X1)
| relation_of2_as_subset(X2,X0,X1) ),
inference(cnf_transformation,[status(esa)],[f183_sk]) ).
cnf(t182,plain,
ifeq(relation_of2(X1,X2,X3),true,relation_of2_as_subset(X1,X2,X3),true) = true,
inference(equality_encoding,[status(esa)],[c539]) ).
cnf(t440,plain,
ifeq(relation_of2(X1,X2,X3),true,relation_of2_as_subset(X1,X2,X3),true) = true,
inference(orient,[status(thm)],[t182]) ).
fof(f28,axiom,
! [A,B,C] :
( relation_of2(C,A,B)
<=> subset(C,cartesian_product2(A,B)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d1_relset_1) ).
fof(f28_nnf,plain,
! [A,B,C] :
( ( ~ subset(C,cartesian_product2(A,B))
| relation_of2(C,A,B) )
& ( subset(C,cartesian_product2(A,B))
| ~ relation_of2(C,A,B) ) ),
inference(nnf_transformation,[status(thm)],[f28]) ).
fof(f28_sk,plain,
! [C,A,B] :
( ( ~ subset(C,cartesian_product2(A,B))
| relation_of2(C,A,B) )
& ( subset(C,cartesian_product2(A,B))
| ~ relation_of2(C,A,B) ) ),
inference(skolemisation,[status(esa)],[f28_nnf]) ).
cnf(c113,plain,
( ~ subset(X2,cartesian_product2(X0,X1))
| relation_of2(X2,X0,X1) ),
inference(cnf_transformation,[status(esa)],[f28_sk]) ).
cnf(t198,plain,
ifeq(subset(X1,cartesian_product2(X2,X3)),true,relation_of2(X1,X2,X3),true) = true,
inference(equality_encoding,[status(esa)],[c113]) ).
cnf(t362,plain,
ifeq(subset(X1,cartesian_product2(X2,X3)),true,relation_of2(X1,X2,X3),true) = true,
inference(orient,[status(thm)],[t198]) ).
fof(f156,lemma,
! [A,B] :
( set_difference(A,B) = empty_set
<=> subset(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',l32_xboole_1) ).
fof(f156_nnf,plain,
! [A,B] :
( ( ~ subset(A,B)
| set_difference(A,B) = empty_set )
& ( subset(A,B)
| set_difference(A,B) != empty_set ) ),
inference(nnf_transformation,[status(thm)],[f156]) ).
fof(f156_sk,plain,
! [A,B] :
( ( ~ subset(A,B)
| set_difference(A,B) = empty_set )
& ( subset(A,B)
| set_difference(A,B) != empty_set ) ),
inference(skolemisation,[status(esa)],[f156_nnf]) ).
cnf(c472,plain,
( subset(X0,X1)
| set_difference(X0,X1) != empty_set ),
inference(cnf_transformation,[status(esa)],[f156_sk]) ).
cnf(t162,plain,
ifeq(set_difference(X1,X2),empty_set,subset(X1,X2),true) = true,
inference(equality_encoding,[status(esa)],[c472]) ).
cnf(t431,plain,
ifeq(set_difference(X1,X2),empty_set,subset(X1,X2),true) = true,
inference(orient,[status(thm)],[t162]) ).
fof(f318,axiom,
! [A,B] :
~ ( empty(B)
& A != B
& empty(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t8_boole) ).
fof(f318_nnf,plain,
! [A,B] :
( ~ empty(B)
| A = B
| ~ empty(A) ),
inference(nnf_transformation,[status(thm)],[f318]) ).
fof(f318_sk,plain,
! [A,B] :
( ~ empty(B)
| A = B
| ~ empty(A) ),
inference(skolemisation,[status(esa)],[f318_nnf]) ).
cnf(c763,plain,
( ~ empty(X1)
| X0 = X1
| ~ empty(X0) ),
inference(cnf_transformation,[status(esa)],[f318_sk]) ).
cnf(hi649,axiom,
ifeq(empty(X0),true,ifeq(empty(X1),true,X0,X1),X1) = X1,
inference(equality_encoding,[status(esa)],[c763]) ).
fof(f134,axiom,
( relation(empty_set)
& empty(empty_set) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc4_relat_1) ).
fof(f134_nnf,plain,
( relation(empty_set)
& empty(empty_set) ),
inference(nnf_transformation,[status(thm)],[f134]) ).
fof(f134_sk,plain,
( relation(empty_set)
& empty(empty_set) ),
inference(skolemisation,[status(esa)],[f134_nnf]) ).
cnf(c439,plain,
empty(empty_set),
inference(cnf_transformation,[status(esa)],[f134_sk]) ).
cnf(hi350,axiom,
empty(empty_set) = true,
inference(equality_encoding,[status(esa)],[c439]) ).
fof(f170,axiom,
? [A] : empty(A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc1_xboole_0) ).
fof(f170_nnf,plain,
? [A] : empty(A),
inference(nnf_transformation,[status(thm)],[f170]) ).
fof(f170_sk,plain,
empty(sk95),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk95])],[f170_nnf]) ).
cnf(c507,plain,
empty(sk95),
inference(cnf_transformation,[status(esa)],[f170_sk]) ).
cnf(hi415,axiom,
empty(sk95) = true,
inference(equality_encoding,[status(esa)],[c507]) ).
cnf(t1,plain,
sk95 = empty_set,
inference(hyper_resolution,[status(thm)],[hi649,hi350,hi415]) ).
cnf(t1365,plain,
empty_set = sk95,
inference(orient,[status(thm)],[t1]) ).
cnf(t40237,plain,
ifeq(set_difference(X1,X2),sk95,subset(X1,X2),true) = true,
inference(step,[status(thm)],[t431,t1365]) ).
cnf(t1380,plain,
ifeq(set_difference(X1,X2),sk95,subset(X1,X2),true) = true,
inference(rw,[status(thm)],[t40237]) ).
fof(f171,axiom,
? [A] :
( function(A)
& empty(A)
& relation(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc2_funct_1) ).
fof(f171_nnf,plain,
? [A] :
( function(A)
& empty(A)
& relation(A) ),
inference(nnf_transformation,[status(thm)],[f171]) ).
fof(f171_sk,plain,
( function(sk96)
& empty(sk96)
& relation(sk96) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk96])],[f171_nnf]) ).
cnf(c509,plain,
empty(sk96),
inference(cnf_transformation,[status(esa)],[f171_sk]) ).
cnf(hi417,axiom,
empty(sk96) = true,
inference(equality_encoding,[status(esa)],[c509]) ).
cnf(t3,plain,
sk96 = empty_set,
inference(hyper_resolution,[status(thm)],[hi649,hi350,hi417]) ).
cnf(t40264,plain,
sk96 = sk95,
inference(step,[status(thm)],[t3,t1365]) ).
cnf(t1391,plain,
sk95 = sk96,
inference(orient,[status(thm)],[t40264]) ).
fof(f172,axiom,
? [A] :
( ordinal(A)
& epsilon_connected(A)
& epsilon_transitive(A)
& empty(A)
& one_to_one(A)
& function(A)
& relation(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc2_ordinal1) ).
fof(f172_nnf,plain,
? [A] :
( ordinal(A)
& epsilon_connected(A)
& epsilon_transitive(A)
& empty(A)
& one_to_one(A)
& function(A)
& relation(A) ),
inference(nnf_transformation,[status(thm)],[f172]) ).
fof(f172_sk,plain,
( ordinal(sk97)
& epsilon_connected(sk97)
& epsilon_transitive(sk97)
& empty(sk97)
& one_to_one(sk97)
& function(sk97)
& relation(sk97) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk97])],[f172_nnf]) ).
cnf(c514,plain,
empty(sk97),
inference(cnf_transformation,[status(esa)],[f172_sk]) ).
cnf(hi422,axiom,
empty(sk97) = true,
inference(equality_encoding,[status(esa)],[c514]) ).
cnf(t6,plain,
sk97 = empty_set,
inference(hyper_resolution,[status(thm)],[hi649,hi350,hi422]) ).
cnf(t40269,plain,
empty_set = sk96,
inference(step,[status(thm)],[t1365,t1391]) ).
cnf(t1396,plain,
empty_set = sk96,
inference(orient,[status(thm)],[t40269]) ).
cnf(t40281,plain,
sk97 = sk96,
inference(step,[status(thm)],[t6,t1396]) ).
cnf(t1425,plain,
sk96 = sk97,
inference(orient,[status(thm)],[t40281]) ).
cnf(t40290,plain,
sk95 = sk97,
inference(step,[status(thm)],[t1391,t1425]) ).
cnf(t1434,plain,
sk95 = sk97,
inference(orient,[status(thm)],[t40290]) ).
cnf(t40856,plain,
ifeq(set_difference(X1,X2),sk97,subset(X1,X2),true) = true,
inference(step,[status(thm)],[t1380,t1434]) ).
cnf(t13571,plain,
ifeq(set_difference(X1,X2),sk97,subset(X1,X2),true) = true,
inference(orient,[status(thm)],[t40856]) ).
cnf(c473,plain,
( ~ subset(X0,X1)
| set_difference(X0,X1) = empty_set ),
inference(cnf_transformation,[status(esa)],[f156_sk]) ).
cnf(t164,plain,
ifeq(subset(X1,X2),true,set_difference(X1,X2),empty_set) = empty_set,
inference(equality_encoding,[status(esa)],[c473]) ).
cnf(t1268,plain,
ifeq(subset(X1,X2),true,set_difference(X1,X2),empty_set) = empty_set,
inference(orient,[status(thm)],[t164]) ).
cnf(t40234,plain,
ifeq(subset(X1,X2),true,set_difference(X1,X2),sk95) = empty_set,
inference(step,[status(thm)],[t1268,t1365]) ).
cnf(t40235,plain,
ifeq(subset(X1,X2),true,set_difference(X1,X2),sk95) = sk95,
inference(step,[status(thm)],[t40234,t1365]) ).
cnf(t1378,plain,
ifeq(subset(X1,X2),true,set_difference(X1,X2),sk95) = sk95,
inference(rw,[status(thm)],[t40235]) ).
cnf(t40848,plain,
ifeq(subset(X1,X2),true,set_difference(X1,X2),sk97) = sk95,
inference(step,[status(thm)],[t1378,t1434]) ).
cnf(t40849,plain,
ifeq(subset(X1,X2),true,set_difference(X1,X2),sk97) = sk97,
inference(step,[status(thm)],[t40848,t1434]) ).
cnf(t13472,plain,
ifeq(subset(X1,X2),true,set_difference(X1,X2),sk97) = sk97,
inference(orient,[status(thm)],[t40849]) ).
fof(f223,lemma,
! [A,B,C] :
( ( subset(B,C)
& subset(A,B) )
=> subset(A,C) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t1_xboole_1) ).
fof(f223_nnf,plain,
! [A,B,C] :
( subset(A,C)
| ~ subset(B,C)
| ~ subset(A,B) ),
inference(nnf_transformation,[status(thm)],[f223]) ).
fof(f223_sk,plain,
! [A,B,C] :
( subset(A,C)
| ~ subset(B,C)
| ~ subset(A,B) ),
inference(skolemisation,[status(esa)],[f223_nnf]) ).
cnf(c600,plain,
( subset(X0,X2)
| ~ subset(X1,X2)
| ~ subset(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f223_sk]) ).
cnf(t225,plain,
ifeq(subset(X1,X2),true,ifeq(subset(X2,X3),true,subset(X1,X3),true),true) = true,
inference(equality_encoding,[status(esa)],[c600]) ).
cnf(t348,plain,
ifeq(subset(X1,X2),true,ifeq(subset(X2,X3),true,subset(X1,X3),true),true) = true,
inference(orient,[status(thm)],[t225]) ).
fof(f314,lemma,
! [A,B] : subset(A,set_union2(A,B)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t7_xboole_1) ).
fof(f314_nnf,plain,
! [A,B] : subset(A,set_union2(A,B)),
inference(nnf_transformation,[status(thm)],[f314]) ).
fof(f314_sk,plain,
! [A,B] : subset(A,set_union2(A,B)),
inference(skolemisation,[status(esa)],[f314_nnf]) ).
cnf(c756,plain,
subset(X0,set_union2(X0,X1)),
inference(cnf_transformation,[status(esa)],[f314_sk]) ).
cnf(t125,plain,
subset(X1,set_union2(X1,X2)) = true,
inference(equality_encoding,[status(esa)],[c756]) ).
cnf(t469,plain,
subset(X1,set_union2(X1,X2)) = true,
inference(orient,[status(thm)],[t125]) ).
cnf(t483,plain,
true = ifeq(true,true,ifeq(subset(set_union2(X1,X2),X3),true,subset(X1,X3),true),true),
inference(cp,[status(thm)],[t348,t469]) ).
cnf(t120,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t249,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t120]) ).
cnf(t41017,plain,
true = ifeq(subset(set_union2(X1,X2),X3),true,subset(X1,X3),true),
inference(step,[status(thm)],[t483,t249]) ).
cnf(t19162,plain,
ifeq(subset(set_union2(X1,X2),X3),true,subset(X1,X3),true) = true,
inference(orient,[status(thm)],[t41017]) ).
fof(f10,axiom,
! [A,B] : set_union2(A,B) = set_union2(B,A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',commutativity_k2_xboole_0) ).
fof(f10_nnf,plain,
! [A,B] : set_union2(A,B) = set_union2(B,A),
inference(nnf_transformation,[status(thm)],[f10]) ).
fof(f10_sk,plain,
! [A,B] : set_union2(A,B) = set_union2(B,A),
inference(skolemisation,[status(esa)],[f10_nnf]) ).
cnf(c15,plain,
set_union2(X0,X1) = set_union2(X1,X0),
inference(cnf_transformation,[status(esa)],[f10_sk]) ).
cnf(t123,plain,
set_union2(X1,X2) = set_union2(X2,X1),
inference(equality_encoding,[status(esa)],[c15]) ).
cnf(t1555,plain,
set_union2(X1,X2) = set_union2(X2,X1),
inference(orient,[status(thm)],[t123]) ).
cnf(t1558,plain,
true = subset(X1,set_union2(X2,X1)),
inference(cp,[status(thm)],[t469,t1555]) ).
cnf(t1996,plain,
subset(X1,set_union2(X2,X1)) = true,
inference(orient,[status(thm)],[t1558]) ).
cnf(t19164,plain,
true = ifeq(true,true,subset(X1,set_union2(X2,set_union2(X1,X3))),true),
inference(cp,[status(thm)],[t19162,t1996]) ).
cnf(t41019,plain,
true = subset(X1,set_union2(X2,set_union2(X1,X3))),
inference(step,[status(thm)],[t19164,t249]) ).
cnf(t19232,plain,
subset(X1,set_union2(X2,set_union2(X1,X3))) = true,
inference(orient,[status(thm)],[t41019]) ).
cnf(t19250,plain,
sk97 = ifeq(true,true,set_difference(X1,set_union2(X2,set_union2(X1,X3))),sk97),
inference(cp,[status(thm)],[t13472,t19232]) ).
cnf(t41021,plain,
sk97 = set_difference(X1,set_union2(X2,set_union2(X1,X3))),
inference(step,[status(thm)],[t19250,t249]) ).
cnf(t19532,plain,
set_difference(X1,set_union2(X2,set_union2(X1,X3))) = sk97,
inference(orient,[status(thm)],[t41021]) ).
fof(f199,lemma,
! [A,B] :
( subset(A,B)
=> set_union2(A,B) = B ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t12_xboole_1) ).
fof(f199_nnf,plain,
! [A,B] :
( set_union2(A,B) = B
| ~ subset(A,B) ),
inference(nnf_transformation,[status(thm)],[f199]) ).
fof(f199_sk,plain,
! [A,B] :
( set_union2(A,B) = B
| ~ subset(A,B) ),
inference(skolemisation,[status(esa)],[f199_nnf]) ).
cnf(c562,plain,
( set_union2(X0,X1) = X1
| ~ subset(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f199_sk]) ).
cnf(t166,plain,
ifeq(subset(X1,X2),true,set_union2(X1,X2),X2) = X2,
inference(equality_encoding,[status(esa)],[c562]) ).
cnf(t254,plain,
ifeq(subset(X1,X2),true,set_union2(X1,X2),X2) = X2,
inference(orient,[status(thm)],[t166]) ).
fof(f229,lemma,
! [A] :
( relation(A)
=> subset(A,cartesian_product2(relation_dom(A),relation_rng(A))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t21_relat_1) ).
fof(f229_nnf,plain,
! [A] :
( subset(A,cartesian_product2(relation_dom(A),relation_rng(A)))
| ~ relation(A) ),
inference(nnf_transformation,[status(thm)],[f229]) ).
fof(f229_sk,plain,
! [A] :
( subset(A,cartesian_product2(relation_dom(A),relation_rng(A)))
| ~ relation(A) ),
inference(skolemisation,[status(esa)],[f229_nnf]) ).
cnf(c610,plain,
( subset(X0,cartesian_product2(relation_dom(X0),relation_rng(X0)))
| ~ relation(X0) ),
inference(cnf_transformation,[status(esa)],[f229_sk]) ).
cnf(t196,plain,
ifeq(relation(X1),true,subset(X1,cartesian_product2(relation_dom(X1),relation_rng(X1))),true) = true,
inference(equality_encoding,[status(esa)],[c610]) ).
cnf(t430,plain,
ifeq(relation(X1),true,subset(X1,cartesian_product2(relation_dom(X1),relation_rng(X1))),true) = true,
inference(orient,[status(thm)],[t196]) ).
fof(f5,axiom,
! [A,B,C] :
( element(C,powerset(cartesian_product2(A,B)))
=> relation(C) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc1_relset_1) ).
fof(f5_nnf,plain,
! [A,B,C] :
( relation(C)
| ~ element(C,powerset(cartesian_product2(A,B))) ),
inference(nnf_transformation,[status(thm)],[f5]) ).
fof(f5_sk,plain,
! [C,A,B] :
( relation(C)
| ~ element(C,powerset(cartesian_product2(A,B))) ),
inference(skolemisation,[status(esa)],[f5_nnf]) ).
cnf(c6,plain,
( relation(X2)
| ~ element(X2,powerset(cartesian_product2(X0,X1))) ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(t178,plain,
ifeq(element(X1,powerset(cartesian_product2(X2,X3))),true,relation(X1),true) = true,
inference(equality_encoding,[status(esa)],[c6]) ).
cnf(t438,plain,
ifeq(element(X1,powerset(cartesian_product2(X2,X3))),true,relation(X1),true) = true,
inference(orient,[status(thm)],[t178]) ).
fof(f108,axiom,
! [A,B,C] :
( relation_of2_as_subset(C,A,B)
=> element(C,powerset(cartesian_product2(A,B))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_m2_relset_1) ).
fof(f108_nnf,plain,
! [A,B,C] :
( element(C,powerset(cartesian_product2(A,B)))
| ~ relation_of2_as_subset(C,A,B) ),
inference(nnf_transformation,[status(thm)],[f108]) ).
fof(f108_sk,plain,
! [C,A,B] :
( element(C,powerset(cartesian_product2(A,B)))
| ~ relation_of2_as_subset(C,A,B) ),
inference(skolemisation,[status(esa)],[f108_nnf]) ).
cnf(c392,plain,
( element(X2,powerset(cartesian_product2(X0,X1)))
| ~ relation_of2_as_subset(X2,X0,X1) ),
inference(cnf_transformation,[status(esa)],[f108_sk]) ).
cnf(t210,plain,
ifeq(relation_of2_as_subset(X1,X2,X3),true,element(X1,powerset(cartesian_product2(X2,X3))),true) = true,
inference(equality_encoding,[status(esa)],[c392]) ).
cnf(t444,plain,
ifeq(relation_of2_as_subset(X1,X2,X3),true,element(X1,powerset(cartesian_product2(X2,X3))),true) = true,
inference(orient,[status(thm)],[t210]) ).
fof(f209,conjecture,
! [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_neg,negated_conjecture,
~ ! [A,B,C,D] :
( relation_of2_as_subset(D,C,A)
=> ( subset(relation_rng(D),B)
=> relation_of2_as_subset(D,C,B) ) ),
inference(negated_conjecture,[status(cth)],[f209]) ).
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_neg]) ).
fof(f209_sk,plain,
( ~ relation_of2_as_subset(sk110,sk109,sk108)
& subset(relation_rng(sk110),sk108)
& relation_of2_as_subset(sk110,sk109,sk107) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk107,sk108,sk109,sk110])],[f209_nnf]) ).
cnf(c578,plain,
relation_of2_as_subset(sk110,sk109,sk107),
inference(cnf_transformation,[status(esa)],[f209_sk]) ).
cnf(t108,plain,
relation_of2_as_subset(sk110,sk109,sk107) = true,
inference(equality_encoding,[status(esa)],[c578]) ).
cnf(t1239,plain,
relation_of2_as_subset(sk110,sk109,sk107) = true,
inference(orient,[status(thm)],[t108]) ).
cnf(t1242,plain,
true = ifeq(true,true,element(sk110,powerset(cartesian_product2(sk109,sk107))),true),
inference(cp,[status(thm)],[t444,t1239]) ).
cnf(t40384,plain,
true = element(sk110,powerset(cartesian_product2(sk109,sk107))),
inference(step,[status(thm)],[t1242,t249]) ).
cnf(t2463,plain,
element(sk110,powerset(cartesian_product2(sk109,sk107))) = true,
inference(orient,[status(thm)],[t40384]) ).
cnf(t2470,plain,
true = ifeq(true,true,relation(sk110),true),
inference(cp,[status(thm)],[t438,t2463]) ).
cnf(t40385,plain,
true = relation(sk110),
inference(step,[status(thm)],[t2470,t249]) ).
cnf(t2474,plain,
relation(sk110) = true,
inference(orient,[status(thm)],[t40385]) ).
cnf(t2477,plain,
true = ifeq(true,true,subset(sk110,cartesian_product2(relation_dom(sk110),relation_rng(sk110))),true),
inference(cp,[status(thm)],[t430,t2474]) ).
cnf(t40462,plain,
true = subset(sk110,cartesian_product2(relation_dom(sk110),relation_rng(sk110))),
inference(step,[status(thm)],[t2477,t249]) ).
cnf(t3459,plain,
subset(sk110,cartesian_product2(relation_dom(sk110),relation_rng(sk110))) = true,
inference(orient,[status(thm)],[t40462]) ).
cnf(t3460,plain,
cartesian_product2(relation_dom(sk110),relation_rng(sk110)) = ifeq(true,true,set_union2(sk110,cartesian_product2(relation_dom(sk110),relation_rng(sk110))),cartesian_product2(relation_dom(sk110),relation_rng(sk110))),
inference(cp,[status(thm)],[t254,t3459]) ).
cnf(t40697,plain,
cartesian_product2(relation_dom(sk110),relation_rng(sk110)) = set_union2(sk110,cartesian_product2(relation_dom(sk110),relation_rng(sk110))),
inference(step,[status(thm)],[t3460,t249]) ).
cnf(t9041,plain,
set_union2(sk110,cartesian_product2(relation_dom(sk110),relation_rng(sk110))) = cartesian_product2(relation_dom(sk110),relation_rng(sk110)),
inference(orient,[status(thm)],[t40697]) ).
cnf(t19246,plain,
true = subset(sk110,set_union2(X1,cartesian_product2(relation_dom(sk110),relation_rng(sk110)))),
inference(cp,[status(thm)],[t19232,t9041]) ).
cnf(t38680,plain,
subset(sk110,set_union2(X1,cartesian_product2(relation_dom(sk110),relation_rng(sk110)))) = true,
inference(orient,[status(thm)],[t19246]) ).
fof(f195,lemma,
! [A,B,C] :
( subset(A,B)
=> ( subset(cartesian_product2(C,A),cartesian_product2(C,B))
& subset(cartesian_product2(A,C),cartesian_product2(B,C)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t118_zfmisc_1) ).
fof(f195_nnf,plain,
! [A,B,C] :
( ( subset(cartesian_product2(C,A),cartesian_product2(C,B))
& subset(cartesian_product2(A,C),cartesian_product2(B,C)) )
| ~ subset(A,B) ),
inference(nnf_transformation,[status(thm)],[f195]) ).
fof(f195_sk,plain,
! [A,B,C] :
( ( subset(cartesian_product2(C,A),cartesian_product2(C,B))
& subset(cartesian_product2(A,C),cartesian_product2(B,C)) )
| ~ subset(A,B) ),
inference(skolemisation,[status(esa)],[f195_nnf]) ).
cnf(c556,plain,
( subset(cartesian_product2(X0,X2),cartesian_product2(X1,X2))
| ~ subset(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f195_sk]) ).
cnf(t212,plain,
ifeq(subset(X1,X2),true,subset(cartesian_product2(X1,X3),cartesian_product2(X2,X3)),true) = true,
inference(equality_encoding,[status(esa)],[c556]) ).
cnf(t358,plain,
ifeq(subset(X1,X2),true,subset(cartesian_product2(X1,X3),cartesian_product2(X2,X3)),true) = true,
inference(orient,[status(thm)],[t212]) ).
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(c560,plain,
( subset(relation_dom(X2),X0)
| ~ relation_of2_as_subset(X2,X0,X1) ),
inference(cnf_transformation,[status(esa)],[f198_sk]) ).
cnf(t184,plain,
ifeq(relation_of2_as_subset(X1,X2,X3),true,subset(relation_dom(X1),X2),true) = true,
inference(equality_encoding,[status(esa)],[c560]) ).
cnf(t443,plain,
ifeq(relation_of2_as_subset(X1,X2,X3),true,subset(relation_dom(X1),X2),true) = true,
inference(orient,[status(thm)],[t184]) ).
cnf(t1240,plain,
true = ifeq(true,true,subset(relation_dom(sk110),sk109),true),
inference(cp,[status(thm)],[t443,t1239]) ).
cnf(t40333,plain,
true = subset(relation_dom(sk110),sk109),
inference(step,[status(thm)],[t1240,t249]) ).
cnf(t1730,plain,
subset(relation_dom(sk110),sk109) = true,
inference(orient,[status(thm)],[t40333]) ).
cnf(t1737,plain,
true = ifeq(true,true,subset(cartesian_product2(relation_dom(sk110),X1),cartesian_product2(sk109,X1)),true),
inference(cp,[status(thm)],[t358,t1730]) ).
cnf(t40514,plain,
true = subset(cartesian_product2(relation_dom(sk110),X1),cartesian_product2(sk109,X1)),
inference(step,[status(thm)],[t1737,t249]) ).
cnf(t4464,plain,
subset(cartesian_product2(relation_dom(sk110),X1),cartesian_product2(sk109,X1)) = true,
inference(orient,[status(thm)],[t40514]) ).
cnf(t4465,plain,
cartesian_product2(sk109,X1) = ifeq(true,true,set_union2(cartesian_product2(relation_dom(sk110),X1),cartesian_product2(sk109,X1)),cartesian_product2(sk109,X1)),
inference(cp,[status(thm)],[t254,t4464]) ).
cnf(t40714,plain,
cartesian_product2(sk109,X1) = set_union2(cartesian_product2(relation_dom(sk110),X1),cartesian_product2(sk109,X1)),
inference(step,[status(thm)],[t4465,t249]) ).
cnf(t40715,plain,
cartesian_product2(sk109,X1) = set_union2(cartesian_product2(sk109,X1),cartesian_product2(relation_dom(sk110),X1)),
inference(step,[status(thm)],[t40714,t1555]) ).
cnf(t9475,plain,
set_union2(cartesian_product2(sk109,X1),cartesian_product2(relation_dom(sk110),X1)) = cartesian_product2(sk109,X1),
inference(orient,[status(thm)],[t40715]) ).
cnf(t38682,plain,
true = subset(sk110,cartesian_product2(sk109,relation_rng(sk110))),
inference(cp,[status(thm)],[t38680,t9475]) ).
cnf(t38744,plain,
subset(sk110,cartesian_product2(sk109,relation_rng(sk110))) = true,
inference(orient,[status(thm)],[t38682]) ).
cnf(t38745,plain,
cartesian_product2(sk109,relation_rng(sk110)) = ifeq(true,true,set_union2(sk110,cartesian_product2(sk109,relation_rng(sk110))),cartesian_product2(sk109,relation_rng(sk110))),
inference(cp,[status(thm)],[t254,t38744]) ).
cnf(t41370,plain,
cartesian_product2(sk109,relation_rng(sk110)) = set_union2(sk110,cartesian_product2(sk109,relation_rng(sk110))),
inference(step,[status(thm)],[t38745,t249]) ).
cnf(t39073,plain,
set_union2(sk110,cartesian_product2(sk109,relation_rng(sk110))) = cartesian_product2(sk109,relation_rng(sk110)),
inference(orient,[status(thm)],[t41370]) ).
cnf(t39110,plain,
sk97 = set_difference(sk110,set_union2(X1,cartesian_product2(sk109,relation_rng(sk110)))),
inference(cp,[status(thm)],[t19532,t39073]) ).
cnf(t40113,plain,
set_difference(sk110,set_union2(X1,cartesian_product2(sk109,relation_rng(sk110)))) = sk97,
inference(orient,[status(thm)],[t39110]) ).
cnf(c557,plain,
( subset(cartesian_product2(X2,X0),cartesian_product2(X2,X1))
| ~ subset(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f195_sk]) ).
cnf(t213,plain,
ifeq(subset(X1,X2),true,subset(cartesian_product2(X3,X1),cartesian_product2(X3,X2)),true) = true,
inference(equality_encoding,[status(esa)],[c557]) ).
cnf(t356,plain,
ifeq(subset(X1,X2),true,subset(cartesian_product2(X3,X1),cartesian_product2(X3,X2)),true) = true,
inference(orient,[status(thm)],[t213]) ).
cnf(c579,plain,
subset(relation_rng(sk110),sk108),
inference(cnf_transformation,[status(esa)],[f209_sk]) ).
cnf(t119,plain,
subset(relation_rng(sk110),sk108) = true,
inference(equality_encoding,[status(esa)],[c579]) ).
cnf(t657,plain,
subset(relation_rng(sk110),sk108) = true,
inference(orient,[status(thm)],[t119]) ).
cnf(t666,plain,
true = ifeq(true,true,subset(cartesian_product2(X1,relation_rng(sk110)),cartesian_product2(X1,sk108)),true),
inference(cp,[status(thm)],[t356,t657]) ).
cnf(t40496,plain,
true = subset(cartesian_product2(X1,relation_rng(sk110)),cartesian_product2(X1,sk108)),
inference(step,[status(thm)],[t666,t249]) ).
cnf(t4289,plain,
subset(cartesian_product2(X1,relation_rng(sk110)),cartesian_product2(X1,sk108)) = true,
inference(orient,[status(thm)],[t40496]) ).
cnf(t4290,plain,
cartesian_product2(X1,sk108) = ifeq(true,true,set_union2(cartesian_product2(X1,relation_rng(sk110)),cartesian_product2(X1,sk108)),cartesian_product2(X1,sk108)),
inference(cp,[status(thm)],[t254,t4289]) ).
cnf(t40708,plain,
cartesian_product2(X1,sk108) = set_union2(cartesian_product2(X1,relation_rng(sk110)),cartesian_product2(X1,sk108)),
inference(step,[status(thm)],[t4290,t249]) ).
cnf(t40709,plain,
cartesian_product2(X1,sk108) = set_union2(cartesian_product2(X1,sk108),cartesian_product2(X1,relation_rng(sk110))),
inference(step,[status(thm)],[t40708,t1555]) ).
cnf(t9309,plain,
set_union2(cartesian_product2(X1,sk108),cartesian_product2(X1,relation_rng(sk110))) = cartesian_product2(X1,sk108),
inference(orient,[status(thm)],[t40709]) ).
cnf(t40114,plain,
sk97 = set_difference(sk110,cartesian_product2(sk109,sk108)),
inference(cp,[status(thm)],[t40113,t9309]) ).
cnf(t40132,plain,
set_difference(sk110,cartesian_product2(sk109,sk108)) = sk97,
inference(orient,[status(thm)],[t40114]) ).
cnf(t40133,plain,
true = ifeq(sk97,sk97,subset(sk110,cartesian_product2(sk109,sk108)),true),
inference(cp,[status(thm)],[t13571,t40132]) ).
cnf(t41440,plain,
true = subset(sk110,cartesian_product2(sk109,sk108)),
inference(step,[status(thm)],[t40133,t249]) ).
cnf(t40149,plain,
subset(sk110,cartesian_product2(sk109,sk108)) = true,
inference(orient,[status(thm)],[t41440]) ).
cnf(t40156,plain,
true = ifeq(true,true,relation_of2(sk110,sk109,sk108),true),
inference(cp,[status(thm)],[t362,t40149]) ).
cnf(t41441,plain,
true = relation_of2(sk110,sk109,sk108),
inference(step,[status(thm)],[t40156,t249]) ).
cnf(t40176,plain,
relation_of2(sk110,sk109,sk108) = true,
inference(orient,[status(thm)],[t41441]) ).
cnf(t40177,plain,
true = ifeq(true,true,relation_of2_as_subset(sk110,sk109,sk108),true),
inference(cp,[status(thm)],[t440,t40176]) ).
cnf(t41444,plain,
true = relation_of2_as_subset(sk110,sk109,sk108),
inference(step,[status(thm)],[t40177,t249]) ).
cnf(c580,plain,
~ relation_of2_as_subset(sk110,sk109,sk108),
inference(cnf_transformation,[status(esa)],[f209_sk]) ).
cnf(t109,plain,
relation_of2_as_subset(sk110,sk109,sk108) = false,
inference(equality_encoding,[status(esa)],[c580]) ).
cnf(t1594,plain,
relation_of2_as_subset(sk110,sk109,sk108) = false,
inference(orient,[status(thm)],[t109]) ).
cnf(t41445,plain,
true = false,
inference(step,[status(thm)],[t41444,t1594]) ).
cnf(t40179,plain,
false = true,
inference(orient,[status(thm)],[t41445]) ).
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(f265,lemma,
! [A,B,C] :
~ ( in(C,A)
& in(B,C)
& in(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t3_ordinal1) ).
fof(f265_nnf,plain,
! [A,B,C] :
( ~ in(C,A)
| ~ in(B,C)
| ~ in(A,B) ),
inference(nnf_transformation,[status(thm)],[f265]) ).
fof(f265_sk,plain,
! [A,B,C] :
( ~ in(C,A)
| ~ in(B,C)
| ~ in(A,B) ),
inference(skolemisation,[status(esa)],[f265_nnf]) ).
cnf(c666,plain,
( ~ in(X2,X0)
| ~ in(X1,X2)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f265_sk]) ).
fof(f267,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(f267_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)],[f267]) ).
fof(f267_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])],[f267_nnf]) ).
cnf(c671,plain,
( ~ disjoint(X0,X1)
| ~ in(X2,X1)
| ~ in(X2,X0) ),
inference(cnf_transformation,[status(esa)],[f267_sk]) ).
fof(f271,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(f271_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)],[f271]) ).
fof(f271_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])],[f271_nnf]) ).
cnf(c680,plain,
( ~ being_limit_ordinal(X0)
| X0 != succ(X1)
| ~ ordinal(X1)
| ~ ordinal(X0) ),
inference(cnf_transformation,[status(esa)],[f271_sk]) ).
fof(f286,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(f286_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)],[f286]) ).
fof(f286_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])],[f286_nnf]) ).
cnf(c697,plain,
( ~ disjoint(X0,X1)
| ~ in(X2,set_intersection2(X0,X1)) ),
inference(cnf_transformation,[status(esa)],[f286_sk]) ).
fof(f290,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(f290_nnf,plain,
! [A,B,C] :
( ~ in(B,C)
| ~ in(B,subset_complement(A,C))
| ~ element(C,powerset(A)) ),
inference(nnf_transformation,[status(thm)],[f290]) ).
fof(f290_sk,plain,
! [C,A,B] :
( ~ in(B,C)
| ~ in(B,subset_complement(A,C))
| ~ element(C,powerset(A)) ),
inference(skolemisation,[status(esa)],[f290_nnf]) ).
cnf(c718,plain,
( ~ in(X1,X2)
| ~ in(X1,subset_complement(X0,X2))
| ~ element(X2,powerset(X0)) ),
inference(cnf_transformation,[status(esa)],[f290_sk]) ).
fof(f295,axiom,
! [A,B,C] :
~ ( empty(C)
& element(B,powerset(C))
& in(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t5_subset) ).
fof(f295_nnf,plain,
! [A,B,C] :
( ~ empty(C)
| ~ element(B,powerset(C))
| ~ in(A,B) ),
inference(nnf_transformation,[status(thm)],[f295]) ).
fof(f295_sk,plain,
! [A,B,C] :
( ~ empty(C)
| ~ element(B,powerset(C))
| ~ in(A,B) ),
inference(skolemisation,[status(esa)],[f295_nnf]) ).
cnf(c725,plain,
( ~ empty(X2)
| ~ element(X1,powerset(X2))
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f295_sk]) ).
fof(f298,lemma,
! [A,B] :
~ ( proper_subset(B,A)
& subset(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t60_xboole_1) ).
fof(f298_nnf,plain,
! [A,B] :
( ~ proper_subset(B,A)
| ~ subset(A,B) ),
inference(nnf_transformation,[status(thm)],[f298]) ).
fof(f298_sk,plain,
! [A,B] :
( ~ proper_subset(B,A)
| ~ subset(A,B) ),
inference(skolemisation,[status(esa)],[f298_nnf]) ).
cnf(c730,plain,
( ~ proper_subset(X1,X0)
| ~ subset(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f298_sk]) ).
fof(f303,lemma,
! [A,B] :
( set_difference(A,singleton(B)) = A
<=> ~ in(B,A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t65_zfmisc_1) ).
fof(f303_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)],[f303]) ).
fof(f303_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)],[f303_nnf]) ).
cnf(c737,plain,
( ~ in(X1,X0)
| set_difference(X0,singleton(X1)) != X0 ),
inference(cnf_transformation,[status(esa)],[f303_sk]) ).
fof(f312,axiom,
! [A,B] :
~ ( empty(B)
& in(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t7_boole) ).
fof(f312_nnf,plain,
! [A,B] :
( ~ empty(B)
| ~ in(A,B) ),
inference(nnf_transformation,[status(thm)],[f312]) ).
fof(f312_sk,plain,
! [A,B] :
( ~ empty(B)
| ~ in(A,B) ),
inference(skolemisation,[status(esa)],[f312_nnf]) ).
cnf(c753,plain,
( ~ empty(X1)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f312_sk]) ).
fof(f313,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(f313_nnf,plain,
! [A,B] :
( ? [C] :
( ! [D] :
( ~ in(D,C)
| ~ in(D,B) )
& in(C,B) )
| ~ in(A,B) ),
inference(nnf_transformation,[status(thm)],[f313]) ).
fof(f313_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])],[f313_nnf]) ).
cnf(c755,plain,
( ~ in(X3,sk125(X0,X1))
| ~ in(X3,X1)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f313_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,c580,c666,c671,c680,c697,c718,c725,c730,c737,c753,c755]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t40179]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU263+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.09/0.36 % Computer : n005.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Thu Sep 24 13:27:02 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 126.35/16.78 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 126.35/16.78 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------