%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SEU098+1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n007.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 02:19:13 PM UTC 2026
% Result : Theorem 0.14s 0.41s
% Output : CNFRefutation 0.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 132
% Syntax : Number of formulae : 589 ( 129 unt; 95 def)
% Number of atoms : 1207 ( 44 equ)
% Maximal formula atoms : 10 ( 2 avg)
% Number of connectives : 956 ( 338 ~; 370 |; 129 &)
% ( 98 <=>; 20 =>; 0 <=; 1 <~>)
% Maximal formula depth : 12 ( 3 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of predicates : 116 ( 114 usr; 96 prp; 0-3 aty)
% Number of functors : 26 ( 26 usr; 17 con; 0-4 aty)
% Number of variables : 147 ( 130 !; 17 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
! [A] :
( empty(A)
=> finite(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [A] :
( empty(A)
=> function(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [A] :
( empty(A)
=> relation(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f13,axiom,
! [A] :
( element(A,positive_rationals)
=> ( ordinal(A)
=> ( natural(A)
& ordinal(A)
& epsilon_connected(A)
& epsilon_transitive(A) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f15,axiom,
! [A,B] :
( function(first_projection(A,B))
& relation(first_projection(A,B)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f16,axiom,
! [A,B] :
( relation_of2_as_subset(first_projection_as_func_of(A,B),cartesian_product2(A,B),A)
& quasi_total(first_projection_as_func_of(A,B),cartesian_product2(A,B),A)
& function(first_projection_as_func_of(A,B)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f21,axiom,
( relation_empty_yielding(empty_set)
& relation(empty_set)
& empty(empty_set) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f26,axiom,
( ordinal(empty_set)
& epsilon_connected(empty_set)
& epsilon_transitive(empty_set)
& empty(empty_set)
& one_to_one(empty_set)
& function(empty_set)
& relation_empty_yielding(empty_set)
& relation(empty_set) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f30,axiom,
! [A] :
( ( relation(A)
& ~ empty(A) )
=> ~ empty(relation_dom(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f33,axiom,
! [A] :
( empty(A)
=> ( relation(relation_dom(A))
& empty(relation_dom(A)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f35,axiom,
! [A] :
( empty(A)
=> ( relation(relation_rng(A))
& empty(relation_rng(A)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f37,axiom,
? [A] :
( finite(A)
& ~ empty(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f38,axiom,
? [A] :
( function_yielding(A)
& function(A)
& relation(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f39,axiom,
? [A] :
( function(A)
& relation(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f42,axiom,
? [A] :
( relation(A)
& empty(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f44,axiom,
? [A] : empty(A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f45,axiom,
? [A] :
( ordinal(A)
& epsilon_connected(A)
& epsilon_transitive(A)
& ~ empty(A)
& element(A,positive_rationals) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f46,axiom,
! [A] :
? [B] :
( finite(B)
& natural(B)
& ordinal(B)
& epsilon_connected(B)
& epsilon_transitive(B)
& one_to_one(B)
& function(B)
& relation(B)
& empty(B)
& element(B,powerset(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f47,axiom,
? [A] :
( function(A)
& empty(A)
& relation(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f48,axiom,
? [A] :
( ordinal(A)
& epsilon_connected(A)
& epsilon_transitive(A)
& empty(A)
& one_to_one(A)
& function(A)
& relation(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f49,axiom,
? [A] :
( ordinal_yielding(A)
& transfinite_sequence(A)
& function(A)
& relation(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f53,axiom,
? [A] :
( natural(A)
& ordinal(A)
& epsilon_connected(A)
& epsilon_transitive(A)
& empty(A)
& element(A,positive_rationals) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f55,axiom,
? [A] :
( one_to_one(A)
& function(A)
& relation(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f59,axiom,
? [A] :
( function(A)
& relation_empty_yielding(A)
& relation(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f60,axiom,
? [A] :
( transfinite_sequence(A)
& function(A)
& relation(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f61,axiom,
? [A] :
( function(A)
& relation_non_empty(A)
& relation(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f62,axiom,
! [A,B,C,D] :
( ( relation_of2(C,A,B)
& quasi_total(C,A,B)
& function(C) )
=> function_image(A,B,C,D) = relation_image(C,D) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f63,axiom,
! [A,B] : first_projection_as_func_of(A,B) = first_projection(A,B),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f64,axiom,
! [A,B,C] :
( relation_of2_as_subset(C,A,B)
<=> relation_of2(C,A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f66,axiom,
! [A] :
( ( function(A)
& relation(A) )
=> function_image(cartesian_product2(relation_dom(A),relation_rng(A)),relation_dom(A),first_projection_as_func_of(relation_dom(A),relation_rng(A)),A) = relation_dom(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f67,axiom,
! [A,B] :
( ( finite(B)
& subset(A,B) )
=> finite(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f68,axiom,
! [A,B] :
( ( function(B)
& relation(B) )
=> ( finite(A)
=> finite(relation_image(B,A)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f69,axiom,
! [A,B] :
( ( finite(B)
& finite(A) )
=> finite(cartesian_product2(A,B)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f71,axiom,
! [A] :
( relation(A)
=> subset(A,cartesian_product2(relation_dom(A),relation_rng(A))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f72,axiom,
! [A] :
( ( function(A)
& relation(A) )
=> ( finite(relation_dom(A))
=> finite(relation_rng(A)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f73,conjecture,
! [A] :
( ( function(A)
& relation(A) )
=> ( finite(relation_dom(A))
<=> finite(A) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f74,negated_conjecture,
~ ! [A] :
( ( function(A)
& relation(A) )
=> ( finite(relation_dom(A))
<=> finite(A) ) ),
inference(negated_conjecture,[status(cth)],[f73]) ).
fof(f79,axiom,
! [A] :
( empty(A)
=> A = empty_set ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f88,plain,
! [A] :
( finite(A)
| ~ empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f3]) ).
fof(f89,plain,
! [X0] :
( finite(X0)
| ~ empty(X0) ),
inference(cnf_transformation,[status(thm)],[f88]) ).
fof(f90,plain,
! [A] :
( function(A)
| ~ empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f4]) ).
fof(f91,plain,
! [X0] :
( function(X0)
| ~ empty(X0) ),
inference(cnf_transformation,[status(thm)],[f90]) ).
fof(f95,plain,
! [A] :
( relation(A)
| ~ empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f6]) ).
fof(f96,plain,
! [X0] :
( relation(X0)
| ~ empty(X0) ),
inference(cnf_transformation,[status(thm)],[f95]) ).
fof(f117,plain,
! [A] :
( ( natural(A)
& ordinal(A)
& epsilon_connected(A)
& epsilon_transitive(A) )
| ~ ordinal(A)
| ~ element(A,positive_rationals) ),
inference(pre_NNF_transformation,[status(thm)],[f13]) ).
fof(f121,plain,
! [X0] :
( natural(X0)
| ~ ordinal(X0)
| ~ element(X0,positive_rationals) ),
inference(cnf_transformation,[status(thm)],[f117]) ).
fof(f125,plain,
( ! [A,B] : function(first_projection(A,B))
& ! [A,B] : relation(first_projection(A,B)) ),
inference(miniscoping,[status(thm)],[f15]) ).
fof(f126,plain,
! [X0,X1] : relation(first_projection(X0,X1)),
inference(cnf_transformation,[status(thm)],[f125]) ).
fof(f128,plain,
( ! [A,B] : relation_of2_as_subset(first_projection_as_func_of(A,B),cartesian_product2(A,B),A)
& ! [A,B] : quasi_total(first_projection_as_func_of(A,B),cartesian_product2(A,B),A)
& ! [A,B] : function(first_projection_as_func_of(A,B)) ),
inference(miniscoping,[status(thm)],[f16]) ).
fof(f129,plain,
! [X0,X1] : function(first_projection_as_func_of(X0,X1)),
inference(cnf_transformation,[status(thm)],[f128]) ).
fof(f130,plain,
! [X0,X1] : quasi_total(first_projection_as_func_of(X0,X1),cartesian_product2(X0,X1),X0),
inference(cnf_transformation,[status(thm)],[f128]) ).
fof(f131,plain,
! [X0,X1] : relation_of2_as_subset(first_projection_as_func_of(X0,X1),cartesian_product2(X0,X1),X0),
inference(cnf_transformation,[status(thm)],[f128]) ).
fof(f140,plain,
empty(empty_set),
inference(cnf_transformation,[status(thm)],[f21]) ).
fof(f156,plain,
ordinal(empty_set),
inference(cnf_transformation,[status(thm)],[f26]) ).
fof(f165,plain,
! [A] :
( ~ empty(relation_dom(A))
| ~ relation(A)
| empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f30]) ).
fof(f166,plain,
! [X0] :
( ~ empty(relation_dom(X0))
| ~ relation(X0)
| empty(X0) ),
inference(cnf_transformation,[status(thm)],[f165]) ).
fof(f171,plain,
! [A] :
( ( relation(relation_dom(A))
& empty(relation_dom(A)) )
| ~ empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f33]) ).
fof(f172,plain,
! [X0] :
( empty(relation_dom(X0))
| ~ empty(X0) ),
inference(cnf_transformation,[status(thm)],[f171]) ).
fof(f173,plain,
! [X0] :
( relation(relation_dom(X0))
| ~ empty(X0) ),
inference(cnf_transformation,[status(thm)],[f171]) ).
fof(f175,plain,
! [A] :
( ( relation(relation_rng(A))
& empty(relation_rng(A)) )
| ~ empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f35]) ).
fof(f176,plain,
! [X0] :
( empty(relation_rng(X0))
| ~ empty(X0) ),
inference(cnf_transformation,[status(thm)],[f175]) ).
fof(f184,plain,
( finite(sK4_skl)
& ~ empty(sK4_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl]),skolemize(A,sK4_skl)],[f37]) ).
fof(f186,plain,
finite(sK4_skl),
inference(cnf_transformation,[status(thm)],[f184]) ).
fof(f187,plain,
( function_yielding(sK5_skl)
& function(sK5_skl)
& relation(sK5_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5_skl]),skolemize(A,sK5_skl)],[f38]) ).
fof(f188,plain,
relation(sK5_skl),
inference(cnf_transformation,[status(thm)],[f187]) ).
fof(f189,plain,
function(sK5_skl),
inference(cnf_transformation,[status(thm)],[f187]) ).
fof(f191,plain,
( function(sK6_skl)
& relation(sK6_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6_skl]),skolemize(A,sK6_skl)],[f39]) ).
fof(f192,plain,
relation(sK6_skl),
inference(cnf_transformation,[status(thm)],[f191]) ).
fof(f193,plain,
function(sK6_skl),
inference(cnf_transformation,[status(thm)],[f191]) ).
fof(f203,plain,
( relation(sK9_skl)
& empty(sK9_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl]),skolemize(A,sK9_skl)],[f42]) ).
fof(f204,plain,
empty(sK9_skl),
inference(cnf_transformation,[status(thm)],[f203]) ).
fof(f210,plain,
empty(sK11_skl),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11_skl]),skolemize(A,sK11_skl)],[f44]) ).
fof(f211,plain,
empty(sK11_skl),
inference(cnf_transformation,[status(thm)],[f210]) ).
fof(f212,plain,
( ordinal(sK12_skl)
& epsilon_connected(sK12_skl)
& epsilon_transitive(sK12_skl)
& ~ empty(sK12_skl)
& element(sK12_skl,positive_rationals) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12_skl]),skolemize(A,sK12_skl)],[f45]) ).
fof(f213,plain,
element(sK12_skl,positive_rationals),
inference(cnf_transformation,[status(thm)],[f212]) ).
fof(f217,plain,
ordinal(sK12_skl),
inference(cnf_transformation,[status(thm)],[f212]) ).
fof(f218,plain,
! [A] :
( finite(sK13_skl(A))
& natural(sK13_skl(A))
& ordinal(sK13_skl(A))
& epsilon_connected(sK13_skl(A))
& epsilon_transitive(sK13_skl(A))
& one_to_one(sK13_skl(A))
& function(sK13_skl(A))
& relation(sK13_skl(A))
& empty(sK13_skl(A))
& element(sK13_skl(A),powerset(A)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13_skl]),skolemize(B,sK13_skl(A))],[f46]) ).
fof(f220,plain,
! [X0] : empty(sK13_skl(X0)),
inference(cnf_transformation,[status(thm)],[f218]) ).
fof(f229,plain,
( function(sK14_skl)
& empty(sK14_skl)
& relation(sK14_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK14_skl]),skolemize(A,sK14_skl)],[f47]) ).
fof(f231,plain,
empty(sK14_skl),
inference(cnf_transformation,[status(thm)],[f229]) ).
fof(f233,plain,
( ordinal(sK15_skl)
& epsilon_connected(sK15_skl)
& epsilon_transitive(sK15_skl)
& empty(sK15_skl)
& one_to_one(sK15_skl)
& function(sK15_skl)
& relation(sK15_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK15_skl]),skolemize(A,sK15_skl)],[f48]) ).
fof(f237,plain,
empty(sK15_skl),
inference(cnf_transformation,[status(thm)],[f233]) ).
fof(f241,plain,
( ordinal_yielding(sK16_skl)
& transfinite_sequence(sK16_skl)
& function(sK16_skl)
& relation(sK16_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK16_skl]),skolemize(A,sK16_skl)],[f49]) ).
fof(f242,plain,
relation(sK16_skl),
inference(cnf_transformation,[status(thm)],[f241]) ).
fof(f243,plain,
function(sK16_skl),
inference(cnf_transformation,[status(thm)],[f241]) ).
fof(f254,plain,
( natural(sK20_skl)
& ordinal(sK20_skl)
& epsilon_connected(sK20_skl)
& epsilon_transitive(sK20_skl)
& empty(sK20_skl)
& element(sK20_skl,positive_rationals) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK20_skl]),skolemize(A,sK20_skl)],[f53]) ).
fof(f255,plain,
element(sK20_skl,positive_rationals),
inference(cnf_transformation,[status(thm)],[f254]) ).
fof(f256,plain,
empty(sK20_skl),
inference(cnf_transformation,[status(thm)],[f254]) ).
fof(f259,plain,
ordinal(sK20_skl),
inference(cnf_transformation,[status(thm)],[f254]) ).
fof(f266,plain,
( one_to_one(sK22_skl)
& function(sK22_skl)
& relation(sK22_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK22_skl]),skolemize(A,sK22_skl)],[f55]) ).
fof(f267,plain,
relation(sK22_skl),
inference(cnf_transformation,[status(thm)],[f266]) ).
fof(f268,plain,
function(sK22_skl),
inference(cnf_transformation,[status(thm)],[f266]) ).
fof(f283,plain,
( function(sK26_skl)
& relation_empty_yielding(sK26_skl)
& relation(sK26_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK26_skl]),skolemize(A,sK26_skl)],[f59]) ).
fof(f284,plain,
relation(sK26_skl),
inference(cnf_transformation,[status(thm)],[f283]) ).
fof(f286,plain,
function(sK26_skl),
inference(cnf_transformation,[status(thm)],[f283]) ).
fof(f287,plain,
( transfinite_sequence(sK27_skl)
& function(sK27_skl)
& relation(sK27_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK27_skl]),skolemize(A,sK27_skl)],[f60]) ).
fof(f288,plain,
relation(sK27_skl),
inference(cnf_transformation,[status(thm)],[f287]) ).
fof(f289,plain,
function(sK27_skl),
inference(cnf_transformation,[status(thm)],[f287]) ).
fof(f291,plain,
( function(sK28_skl)
& relation_non_empty(sK28_skl)
& relation(sK28_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK28_skl]),skolemize(A,sK28_skl)],[f61]) ).
fof(f292,plain,
relation(sK28_skl),
inference(cnf_transformation,[status(thm)],[f291]) ).
fof(f294,plain,
function(sK28_skl),
inference(cnf_transformation,[status(thm)],[f291]) ).
fof(f295,plain,
! [A,B,C,D] :
( function_image(A,B,C,D) = relation_image(C,D)
| ~ relation_of2(C,A,B)
| ~ quasi_total(C,A,B)
| ~ function(C) ),
inference(pre_NNF_transformation,[status(thm)],[f62]) ).
fof(f296,plain,
! [A,B,C] :
( ! [D] : function_image(A,B,C,D) = relation_image(C,D)
| ~ relation_of2(C,A,B)
| ~ quasi_total(C,A,B)
| ~ function(C) ),
inference(miniscoping,[status(thm)],[f295]) ).
fof(f297,plain,
! [X0,X1,X2,X3] :
( function_image(X1,X2,X0,X3) = relation_image(X0,X3)
| ~ relation_of2(X0,X1,X2)
| ~ quasi_total(X0,X1,X2)
| ~ function(X0) ),
inference(cnf_transformation,[status(thm)],[f296]) ).
fof(f298,plain,
! [X0,X1] : first_projection_as_func_of(X0,X1) = first_projection(X0,X1),
inference(cnf_transformation,[status(thm)],[f63]) ).
fof(f299,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)],[f64]) ).
fof(f300,plain,
( ! [A,B,C] :
( ~ relation_of2(C,A,B)
| relation_of2_as_subset(C,A,B) )
& ! [A,B,C] :
( relation_of2(C,A,B)
| ~ relation_of2_as_subset(C,A,B) ) ),
inference(miniscoping,[status(thm)],[f299]) ).
fof(f301,plain,
! [X0,X1,X2] :
( relation_of2(X0,X1,X2)
| ~ relation_of2_as_subset(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f300]) ).
fof(f305,plain,
! [A] :
( function_image(cartesian_product2(relation_dom(A),relation_rng(A)),relation_dom(A),first_projection_as_func_of(relation_dom(A),relation_rng(A)),A) = relation_dom(A)
| ~ function(A)
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f66]) ).
fof(f306,plain,
! [X0] :
( function_image(cartesian_product2(relation_dom(X0),relation_rng(X0)),relation_dom(X0),first_projection_as_func_of(relation_dom(X0),relation_rng(X0)),X0) = relation_dom(X0)
| ~ function(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f305]) ).
fof(f307,plain,
! [A,B] :
( finite(A)
| ~ finite(B)
| ~ subset(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f67]) ).
fof(f308,plain,
! [A] :
( finite(A)
| ! [B] :
( ~ finite(B)
| ~ subset(A,B) ) ),
inference(miniscoping,[status(thm)],[f307]) ).
fof(f309,plain,
! [X0,X1] :
( finite(X0)
| ~ finite(X1)
| ~ subset(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f308]) ).
fof(f310,plain,
! [A,B] :
( finite(relation_image(B,A))
| ~ finite(A)
| ~ function(B)
| ~ relation(B) ),
inference(pre_NNF_transformation,[status(thm)],[f68]) ).
fof(f311,plain,
! [B] :
( ! [A] :
( finite(relation_image(B,A))
| ~ finite(A) )
| ~ function(B)
| ~ relation(B) ),
inference(miniscoping,[status(thm)],[f310]) ).
fof(f312,plain,
! [X0,X1] :
( finite(relation_image(X0,X1))
| ~ finite(X1)
| ~ function(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f311]) ).
fof(f313,plain,
! [A,B] :
( finite(cartesian_product2(A,B))
| ~ finite(B)
| ~ finite(A) ),
inference(pre_NNF_transformation,[status(thm)],[f69]) ).
fof(f314,plain,
! [X0,X1] :
( finite(cartesian_product2(X0,X1))
| ~ finite(X1)
| ~ finite(X0) ),
inference(cnf_transformation,[status(thm)],[f313]) ).
fof(f317,plain,
! [A] :
( subset(A,cartesian_product2(relation_dom(A),relation_rng(A)))
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f71]) ).
fof(f318,plain,
! [X0] :
( subset(X0,cartesian_product2(relation_dom(X0),relation_rng(X0)))
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f317]) ).
fof(f319,plain,
! [A] :
( finite(relation_rng(A))
| ~ finite(relation_dom(A))
| ~ function(A)
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f72]) ).
fof(f320,plain,
! [X0] :
( finite(relation_rng(X0))
| ~ finite(relation_dom(X0))
| ~ function(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f319]) ).
fof(f321,plain,
? [A] :
( ( finite(relation_dom(A))
<~> finite(A) )
& function(A)
& relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f74]) ).
fof(f322,plain,
? [A] :
( ( ~ finite(A)
| ~ finite(relation_dom(A)) )
& ( finite(A)
| finite(relation_dom(A)) )
& function(A)
& relation(A) ),
inference(NNF_transformation,[status(thm)],[f321]) ).
fof(f323,plain,
( ( ~ finite(sK29_skl)
| ~ finite(relation_dom(sK29_skl)) )
& ( finite(sK29_skl)
| finite(relation_dom(sK29_skl)) )
& function(sK29_skl)
& relation(sK29_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK29_skl]),skolemize(A,sK29_skl)],[f322]) ).
fof(f324,plain,
relation(sK29_skl),
inference(cnf_transformation,[status(thm)],[f323]) ).
fof(f325,plain,
function(sK29_skl),
inference(cnf_transformation,[status(thm)],[f323]) ).
fof(f326,plain,
( finite(sK29_skl)
| finite(relation_dom(sK29_skl)) ),
inference(cnf_transformation,[status(thm)],[f323]) ).
fof(f327,plain,
( ~ finite(sK29_skl)
| ~ finite(relation_dom(sK29_skl)) ),
inference(cnf_transformation,[status(thm)],[f323]) ).
fof(f340,plain,
! [A] :
( A = empty_set
| ~ empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f79]) ).
fof(f341,plain,
! [X0] :
( X0 = empty_set
| ~ empty(X0) ),
inference(cnf_transformation,[status(thm)],[f340]) ).
fof(f348,definition,
( sQ0_spl
<=> finite(relation_dom(sK29_skl)) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f351,definition,
( sQ1_spl
<=> finite(sK29_skl) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f353,plain,
( sQ1_spl
| ~ finite(sK29_skl) ),
inference(component_clause,[status(thm)],[f351]) ).
fof(f354,plain,
( sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f326,f348,f351]) ).
fof(f355,plain,
( ~ sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f327,f348,f351]) ).
fof(f356,plain,
empty(relation_dom(empty_set)),
inference(resolution,[status(thm)],[f140,f172]) ).
fof(f357,plain,
relation(empty_set),
inference(resolution,[status(thm)],[f140,f96]) ).
fof(f358,plain,
function(empty_set),
inference(resolution,[status(thm)],[f140,f91]) ).
fof(f359,plain,
finite(empty_set),
inference(resolution,[status(thm)],[f140,f89]) ).
fof(f361,plain,
empty(relation_dom(relation_dom(empty_set))),
inference(resolution,[status(thm)],[f356,f172]) ).
fof(f365,definition,
( sQ2_spl
<=> empty(empty_set) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f367,plain,
( sQ2_spl
| ~ empty(empty_set) ),
inference(component_clause,[status(thm)],[f365]) ).
fof(f368,definition,
( sQ3_spl
<=> relation(empty_set) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f372,plain,
( ~ relation(relation_dom(empty_set))
| empty(relation_dom(empty_set)) ),
inference(resolution,[status(thm)],[f361,f166]) ).
fof(f373,plain,
empty(relation_dom(relation_dom(relation_dom(empty_set)))),
inference(resolution,[status(thm)],[f361,f172]) ).
fof(f377,definition,
( sQ4_spl
<=> empty(relation_dom(empty_set)) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f380,definition,
( sQ5_spl
<=> relation(relation_dom(empty_set)) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f382,plain,
( sQ5_spl
| ~ relation(relation_dom(empty_set)) ),
inference(component_clause,[status(thm)],[f380]) ).
fof(f383,plain,
( ~ sQ5_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f372,f377,f380]) ).
fof(f384,plain,
( ~ relation(relation_dom(relation_dom(empty_set)))
| empty(relation_dom(relation_dom(empty_set))) ),
inference(resolution,[status(thm)],[f373,f166]) ).
fof(f385,plain,
empty(relation_dom(relation_dom(relation_dom(relation_dom(empty_set))))),
inference(resolution,[status(thm)],[f373,f172]) ).
fof(f389,definition,
( sQ6_spl
<=> empty(relation_dom(relation_dom(empty_set))) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f392,definition,
( sQ7_spl
<=> relation(relation_dom(relation_dom(empty_set))) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f394,plain,
( sQ7_spl
| ~ relation(relation_dom(relation_dom(empty_set))) ),
inference(component_clause,[status(thm)],[f392]) ).
fof(f395,plain,
( ~ sQ7_spl
| sQ6_spl ),
inference(split_clause,[status(thm)],[f384,f389,f392]) ).
fof(f396,plain,
( ~ relation(relation_dom(relation_dom(relation_dom(empty_set))))
| empty(relation_dom(relation_dom(relation_dom(empty_set)))) ),
inference(resolution,[status(thm)],[f385,f166]) ).
fof(f397,plain,
empty(relation_dom(relation_dom(relation_dom(relation_dom(relation_dom(empty_set)))))),
inference(resolution,[status(thm)],[f385,f172]) ).
fof(f401,definition,
( sQ8_spl
<=> empty(relation_dom(relation_dom(relation_dom(empty_set)))) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f404,definition,
( sQ9_spl
<=> relation(relation_dom(relation_dom(relation_dom(empty_set)))) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f406,plain,
( sQ9_spl
| ~ relation(relation_dom(relation_dom(relation_dom(empty_set)))) ),
inference(component_clause,[status(thm)],[f404]) ).
fof(f407,plain,
( ~ sQ9_spl
| sQ8_spl ),
inference(split_clause,[status(thm)],[f396,f401,f404]) ).
fof(f408,plain,
( ~ relation(relation_dom(relation_dom(relation_dom(relation_dom(empty_set)))))
| empty(relation_dom(relation_dom(relation_dom(relation_dom(empty_set))))) ),
inference(resolution,[status(thm)],[f397,f166]) ).
fof(f409,plain,
empty(relation_dom(relation_dom(relation_dom(relation_dom(relation_dom(relation_dom(empty_set))))))),
inference(resolution,[status(thm)],[f397,f172]) ).
fof(f413,definition,
( sQ10_spl
<=> empty(relation_dom(relation_dom(relation_dom(relation_dom(empty_set))))) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f416,definition,
( sQ11_spl
<=> relation(relation_dom(relation_dom(relation_dom(relation_dom(empty_set))))) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f418,plain,
( sQ11_spl
| ~ relation(relation_dom(relation_dom(relation_dom(relation_dom(empty_set))))) ),
inference(component_clause,[status(thm)],[f416]) ).
fof(f419,plain,
( ~ sQ11_spl
| sQ10_spl ),
inference(split_clause,[status(thm)],[f408,f413,f416]) ).
fof(f420,plain,
( ~ relation(relation_dom(relation_dom(relation_dom(relation_dom(relation_dom(empty_set))))))
| empty(relation_dom(relation_dom(relation_dom(relation_dom(relation_dom(empty_set)))))) ),
inference(resolution,[status(thm)],[f409,f166]) ).
fof(f421,plain,
empty(relation_dom(relation_dom(relation_dom(relation_dom(relation_dom(relation_dom(relation_dom(empty_set)))))))),
inference(resolution,[status(thm)],[f409,f172]) ).
fof(f425,definition,
( sQ12_spl
<=> empty(relation_dom(relation_dom(relation_dom(relation_dom(relation_dom(empty_set)))))) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f428,definition,
( sQ13_spl
<=> relation(relation_dom(relation_dom(relation_dom(relation_dom(relation_dom(empty_set)))))) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f430,plain,
( sQ13_spl
| ~ relation(relation_dom(relation_dom(relation_dom(relation_dom(relation_dom(empty_set)))))) ),
inference(component_clause,[status(thm)],[f428]) ).
fof(f431,plain,
( ~ sQ13_spl
| sQ12_spl ),
inference(split_clause,[status(thm)],[f420,f425,f428]) ).
fof(f432,plain,
( ~ relation(relation_dom(relation_dom(relation_dom(relation_dom(relation_dom(relation_dom(empty_set)))))))
| empty(relation_dom(relation_dom(relation_dom(relation_dom(relation_dom(relation_dom(empty_set))))))) ),
inference(resolution,[status(thm)],[f421,f166]) ).
fof(f433,plain,
empty(relation_dom(relation_dom(relation_dom(relation_dom(relation_dom(relation_dom(relation_dom(relation_dom(empty_set))))))))),
inference(resolution,[status(thm)],[f421,f172]) ).
fof(f437,definition,
( sQ14_spl
<=> empty(relation_dom(relation_dom(relation_dom(relation_dom(relation_dom(relation_dom(empty_set))))))) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f440,definition,
( sQ15_spl
<=> relation(relation_dom(relation_dom(relation_dom(relation_dom(relation_dom(relation_dom(empty_set))))))) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f442,plain,
( sQ15_spl
| ~ relation(relation_dom(relation_dom(relation_dom(relation_dom(relation_dom(relation_dom(empty_set))))))) ),
inference(component_clause,[status(thm)],[f440]) ).
fof(f443,plain,
( ~ sQ15_spl
| sQ14_spl ),
inference(split_clause,[status(thm)],[f432,f437,f440]) ).
fof(f444,plain,
( ~ relation(relation_dom(relation_dom(relation_dom(relation_dom(relation_dom(relation_dom(relation_dom(empty_set))))))))
| empty(relation_dom(relation_dom(relation_dom(relation_dom(relation_dom(relation_dom(relation_dom(empty_set)))))))) ),
inference(resolution,[status(thm)],[f433,f166]) ).
fof(f449,definition,
( sQ16_spl
<=> empty(relation_dom(relation_dom(relation_dom(relation_dom(relation_dom(relation_dom(relation_dom(empty_set)))))))) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f452,definition,
( sQ17_spl
<=> relation(relation_dom(relation_dom(relation_dom(relation_dom(relation_dom(relation_dom(relation_dom(empty_set)))))))) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f454,plain,
( sQ17_spl
| ~ relation(relation_dom(relation_dom(relation_dom(relation_dom(relation_dom(relation_dom(relation_dom(empty_set)))))))) ),
inference(component_clause,[status(thm)],[f452]) ).
fof(f455,plain,
( ~ sQ17_spl
| sQ16_spl ),
inference(split_clause,[status(thm)],[f444,f449,f452]) ).
fof(f456,plain,
empty(relation_dom(sK9_skl)),
inference(resolution,[status(thm)],[f204,f172]) ).
fof(f460,plain,
empty(relation_dom(sK11_skl)),
inference(resolution,[status(thm)],[f211,f172]) ).
fof(f464,plain,
( ~ relation(sK9_skl)
| empty(sK9_skl) ),
inference(resolution,[status(thm)],[f456,f166]) ).
fof(f465,plain,
empty(relation_dom(relation_dom(sK9_skl))),
inference(resolution,[status(thm)],[f456,f172]) ).
fof(f469,definition,
( sQ18_spl
<=> empty(sK9_skl) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f472,definition,
( sQ19_spl
<=> relation(sK9_skl) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f474,plain,
( sQ19_spl
| ~ relation(sK9_skl) ),
inference(component_clause,[status(thm)],[f472]) ).
fof(f475,plain,
( ~ sQ19_spl
| sQ18_spl ),
inference(split_clause,[status(thm)],[f464,f469,f472]) ).
fof(f476,plain,
( ~ relation(sK11_skl)
| empty(sK11_skl) ),
inference(resolution,[status(thm)],[f460,f166]) ).
fof(f477,plain,
empty(relation_dom(relation_dom(sK11_skl))),
inference(resolution,[status(thm)],[f460,f172]) ).
fof(f481,definition,
( sQ20_spl
<=> empty(sK11_skl) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f484,definition,
( sQ21_spl
<=> relation(sK11_skl) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f486,plain,
( sQ21_spl
| ~ relation(sK11_skl) ),
inference(component_clause,[status(thm)],[f484]) ).
fof(f487,plain,
( ~ sQ21_spl
| sQ20_spl ),
inference(split_clause,[status(thm)],[f476,f481,f484]) ).
fof(f488,plain,
( ~ relation(relation_dom(sK9_skl))
| empty(relation_dom(sK9_skl)) ),
inference(resolution,[status(thm)],[f465,f166]) ).
fof(f489,plain,
empty(relation_dom(relation_dom(relation_dom(sK9_skl)))),
inference(resolution,[status(thm)],[f465,f172]) ).
fof(f493,definition,
( sQ22_spl
<=> empty(relation_dom(sK9_skl)) ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f496,definition,
( sQ23_spl
<=> relation(relation_dom(sK9_skl)) ),
introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition]) ).
fof(f498,plain,
( sQ23_spl
| ~ relation(relation_dom(sK9_skl)) ),
inference(component_clause,[status(thm)],[f496]) ).
fof(f499,plain,
( ~ sQ23_spl
| sQ22_spl ),
inference(split_clause,[status(thm)],[f488,f493,f496]) ).
fof(f500,plain,
( ~ relation(relation_dom(sK11_skl))
| empty(relation_dom(sK11_skl)) ),
inference(resolution,[status(thm)],[f477,f166]) ).
fof(f501,plain,
empty(relation_dom(relation_dom(relation_dom(sK11_skl)))),
inference(resolution,[status(thm)],[f477,f172]) ).
fof(f505,definition,
( sQ24_spl
<=> empty(relation_dom(sK11_skl)) ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f508,definition,
( sQ25_spl
<=> relation(relation_dom(sK11_skl)) ),
introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition]) ).
fof(f510,plain,
( sQ25_spl
| ~ relation(relation_dom(sK11_skl)) ),
inference(component_clause,[status(thm)],[f508]) ).
fof(f511,plain,
( ~ sQ25_spl
| sQ24_spl ),
inference(split_clause,[status(thm)],[f500,f505,f508]) ).
fof(f512,plain,
empty(relation_dom(sK14_skl)),
inference(resolution,[status(thm)],[f231,f172]) ).
fof(f516,plain,
empty(relation_dom(sK15_skl)),
inference(resolution,[status(thm)],[f237,f172]) ).
fof(f521,plain,
( ~ relation(sK14_skl)
| empty(sK14_skl) ),
inference(resolution,[status(thm)],[f512,f166]) ).
fof(f522,plain,
empty(relation_dom(relation_dom(sK14_skl))),
inference(resolution,[status(thm)],[f512,f172]) ).
fof(f526,definition,
( sQ26_spl
<=> empty(sK14_skl) ),
introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition]) ).
fof(f529,definition,
( sQ27_spl
<=> relation(sK14_skl) ),
introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition]) ).
fof(f531,plain,
( sQ27_spl
| ~ relation(sK14_skl) ),
inference(component_clause,[status(thm)],[f529]) ).
fof(f532,plain,
( ~ sQ27_spl
| sQ26_spl ),
inference(split_clause,[status(thm)],[f521,f526,f529]) ).
fof(f533,plain,
( ~ relation(sK15_skl)
| empty(sK15_skl) ),
inference(resolution,[status(thm)],[f516,f166]) ).
fof(f534,plain,
empty(relation_dom(relation_dom(sK15_skl))),
inference(resolution,[status(thm)],[f516,f172]) ).
fof(f538,definition,
( sQ28_spl
<=> empty(sK15_skl) ),
introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition]) ).
fof(f541,definition,
( sQ29_spl
<=> relation(sK15_skl) ),
introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition]) ).
fof(f543,plain,
( sQ29_spl
| ~ relation(sK15_skl) ),
inference(component_clause,[status(thm)],[f541]) ).
fof(f544,plain,
( ~ sQ29_spl
| sQ28_spl ),
inference(split_clause,[status(thm)],[f533,f538,f541]) ).
fof(f545,plain,
( ~ relation(relation_dom(sK14_skl))
| empty(relation_dom(sK14_skl)) ),
inference(resolution,[status(thm)],[f522,f166]) ).
fof(f546,plain,
empty(relation_dom(relation_dom(relation_dom(sK14_skl)))),
inference(resolution,[status(thm)],[f522,f172]) ).
fof(f550,definition,
( sQ30_spl
<=> empty(relation_dom(sK14_skl)) ),
introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition]) ).
fof(f553,definition,
( sQ31_spl
<=> relation(relation_dom(sK14_skl)) ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f555,plain,
( sQ31_spl
| ~ relation(relation_dom(sK14_skl)) ),
inference(component_clause,[status(thm)],[f553]) ).
fof(f556,plain,
( ~ sQ31_spl
| sQ30_spl ),
inference(split_clause,[status(thm)],[f545,f550,f553]) ).
fof(f557,plain,
( ~ relation(relation_dom(sK15_skl))
| empty(relation_dom(sK15_skl)) ),
inference(resolution,[status(thm)],[f534,f166]) ).
fof(f558,plain,
empty(relation_dom(relation_dom(relation_dom(sK15_skl)))),
inference(resolution,[status(thm)],[f534,f172]) ).
fof(f562,definition,
( sQ32_spl
<=> empty(relation_dom(sK15_skl)) ),
introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition]) ).
fof(f565,definition,
( sQ33_spl
<=> relation(relation_dom(sK15_skl)) ),
introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition]) ).
fof(f567,plain,
( sQ33_spl
| ~ relation(relation_dom(sK15_skl)) ),
inference(component_clause,[status(thm)],[f565]) ).
fof(f568,plain,
( ~ sQ33_spl
| sQ32_spl ),
inference(split_clause,[status(thm)],[f557,f562,f565]) ).
fof(f569,plain,
empty(relation_dom(sK20_skl)),
inference(resolution,[status(thm)],[f256,f172]) ).
fof(f573,plain,
( ~ relation(sK20_skl)
| empty(sK20_skl) ),
inference(resolution,[status(thm)],[f569,f166]) ).
fof(f574,plain,
empty(relation_dom(relation_dom(sK20_skl))),
inference(resolution,[status(thm)],[f569,f172]) ).
fof(f578,definition,
( sQ34_spl
<=> empty(sK20_skl) ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f581,definition,
( sQ35_spl
<=> relation(sK20_skl) ),
introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition]) ).
fof(f583,plain,
( sQ35_spl
| ~ relation(sK20_skl) ),
inference(component_clause,[status(thm)],[f581]) ).
fof(f584,plain,
( ~ sQ35_spl
| sQ34_spl ),
inference(split_clause,[status(thm)],[f573,f578,f581]) ).
fof(f585,plain,
( ~ relation(relation_dom(sK20_skl))
| empty(relation_dom(sK20_skl)) ),
inference(resolution,[status(thm)],[f574,f166]) ).
fof(f586,plain,
empty(relation_dom(relation_dom(relation_dom(sK20_skl)))),
inference(resolution,[status(thm)],[f574,f172]) ).
fof(f590,definition,
( sQ36_spl
<=> empty(relation_dom(sK20_skl)) ),
introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition]) ).
fof(f593,definition,
( sQ37_spl
<=> relation(relation_dom(sK20_skl)) ),
introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition]) ).
fof(f595,plain,
( sQ37_spl
| ~ relation(relation_dom(sK20_skl)) ),
inference(component_clause,[status(thm)],[f593]) ).
fof(f596,plain,
( ~ sQ37_spl
| sQ36_spl ),
inference(split_clause,[status(thm)],[f585,f590,f593]) ).
fof(f597,plain,
( ~ relation(relation_dom(relation_dom(sK9_skl)))
| empty(relation_dom(relation_dom(sK9_skl))) ),
inference(resolution,[status(thm)],[f489,f166]) ).
fof(f598,plain,
empty(relation_dom(relation_dom(relation_dom(relation_dom(sK9_skl))))),
inference(resolution,[status(thm)],[f489,f172]) ).
fof(f602,definition,
( sQ38_spl
<=> empty(relation_dom(relation_dom(sK9_skl))) ),
introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition]) ).
fof(f605,definition,
( sQ39_spl
<=> relation(relation_dom(relation_dom(sK9_skl))) ),
introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition]) ).
fof(f607,plain,
( sQ39_spl
| ~ relation(relation_dom(relation_dom(sK9_skl))) ),
inference(component_clause,[status(thm)],[f605]) ).
fof(f608,plain,
( ~ sQ39_spl
| sQ38_spl ),
inference(split_clause,[status(thm)],[f597,f602,f605]) ).
fof(f609,plain,
( ~ relation(relation_dom(relation_dom(sK11_skl)))
| empty(relation_dom(relation_dom(sK11_skl))) ),
inference(resolution,[status(thm)],[f501,f166]) ).
fof(f610,plain,
empty(relation_dom(relation_dom(relation_dom(relation_dom(sK11_skl))))),
inference(resolution,[status(thm)],[f501,f172]) ).
fof(f614,definition,
( sQ40_spl
<=> empty(relation_dom(relation_dom(sK11_skl))) ),
introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition]) ).
fof(f617,definition,
( sQ41_spl
<=> relation(relation_dom(relation_dom(sK11_skl))) ),
introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition]) ).
fof(f619,plain,
( sQ41_spl
| ~ relation(relation_dom(relation_dom(sK11_skl))) ),
inference(component_clause,[status(thm)],[f617]) ).
fof(f620,plain,
( ~ sQ41_spl
| sQ40_spl ),
inference(split_clause,[status(thm)],[f609,f614,f617]) ).
fof(f622,plain,
( ~ relation(relation_dom(relation_dom(sK14_skl)))
| empty(relation_dom(relation_dom(sK14_skl))) ),
inference(resolution,[status(thm)],[f546,f166]) ).
fof(f623,plain,
empty(relation_dom(relation_dom(relation_dom(relation_dom(sK14_skl))))),
inference(resolution,[status(thm)],[f546,f172]) ).
fof(f627,definition,
( sQ42_spl
<=> empty(relation_dom(relation_dom(sK14_skl))) ),
introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition]) ).
fof(f630,definition,
( sQ43_spl
<=> relation(relation_dom(relation_dom(sK14_skl))) ),
introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition]) ).
fof(f632,plain,
( sQ43_spl
| ~ relation(relation_dom(relation_dom(sK14_skl))) ),
inference(component_clause,[status(thm)],[f630]) ).
fof(f633,plain,
( ~ sQ43_spl
| sQ42_spl ),
inference(split_clause,[status(thm)],[f622,f627,f630]) ).
fof(f634,plain,
( ~ relation(relation_dom(relation_dom(sK15_skl)))
| empty(relation_dom(relation_dom(sK15_skl))) ),
inference(resolution,[status(thm)],[f558,f166]) ).
fof(f639,definition,
( sQ44_spl
<=> empty(relation_dom(relation_dom(sK15_skl))) ),
introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition]) ).
fof(f642,definition,
( sQ45_spl
<=> relation(relation_dom(relation_dom(sK15_skl))) ),
introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition]) ).
fof(f644,plain,
( sQ45_spl
| ~ relation(relation_dom(relation_dom(sK15_skl))) ),
inference(component_clause,[status(thm)],[f642]) ).
fof(f645,plain,
( ~ sQ45_spl
| sQ44_spl ),
inference(split_clause,[status(thm)],[f634,f639,f642]) ).
fof(f646,plain,
( ~ relation(relation_dom(relation_dom(sK20_skl)))
| empty(relation_dom(relation_dom(sK20_skl))) ),
inference(resolution,[status(thm)],[f586,f166]) ).
fof(f651,definition,
( sQ46_spl
<=> empty(relation_dom(relation_dom(sK20_skl))) ),
introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition]) ).
fof(f654,definition,
( sQ47_spl
<=> relation(relation_dom(relation_dom(sK20_skl))) ),
introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition]) ).
fof(f656,plain,
( sQ47_spl
| ~ relation(relation_dom(relation_dom(sK20_skl))) ),
inference(component_clause,[status(thm)],[f654]) ).
fof(f657,plain,
( ~ sQ47_spl
| sQ46_spl ),
inference(split_clause,[status(thm)],[f646,f651,f654]) ).
fof(f658,plain,
( ~ relation(relation_dom(relation_dom(relation_dom(sK9_skl))))
| empty(relation_dom(relation_dom(relation_dom(sK9_skl)))) ),
inference(resolution,[status(thm)],[f598,f166]) ).
fof(f663,definition,
( sQ48_spl
<=> empty(relation_dom(relation_dom(relation_dom(sK9_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition]) ).
fof(f666,definition,
( sQ49_spl
<=> relation(relation_dom(relation_dom(relation_dom(sK9_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition]) ).
fof(f668,plain,
( sQ49_spl
| ~ relation(relation_dom(relation_dom(relation_dom(sK9_skl)))) ),
inference(component_clause,[status(thm)],[f666]) ).
fof(f669,plain,
( ~ sQ49_spl
| sQ48_spl ),
inference(split_clause,[status(thm)],[f658,f663,f666]) ).
fof(f670,plain,
! [X0] : empty(relation_dom(sK13_skl(X0))),
inference(resolution,[status(thm)],[f220,f172]) ).
fof(f689,plain,
( ~ relation(relation_dom(relation_dom(relation_dom(sK11_skl))))
| empty(relation_dom(relation_dom(relation_dom(sK11_skl)))) ),
inference(resolution,[status(thm)],[f610,f166]) ).
fof(f694,definition,
( sQ50_spl
<=> empty(relation_dom(relation_dom(relation_dom(sK11_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition]) ).
fof(f697,definition,
( sQ51_spl
<=> relation(relation_dom(relation_dom(relation_dom(sK11_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition]) ).
fof(f699,plain,
( sQ51_spl
| ~ relation(relation_dom(relation_dom(relation_dom(sK11_skl)))) ),
inference(component_clause,[status(thm)],[f697]) ).
fof(f700,plain,
( ~ sQ51_spl
| sQ50_spl ),
inference(split_clause,[status(thm)],[f689,f694,f697]) ).
fof(f722,plain,
( ~ relation(relation_dom(relation_dom(relation_dom(sK14_skl))))
| empty(relation_dom(relation_dom(relation_dom(sK14_skl)))) ),
inference(resolution,[status(thm)],[f623,f166]) ).
fof(f727,definition,
( sQ52_spl
<=> empty(relation_dom(relation_dom(relation_dom(sK14_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition]) ).
fof(f730,definition,
( sQ53_spl
<=> relation(relation_dom(relation_dom(relation_dom(sK14_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition]) ).
fof(f732,plain,
( sQ53_spl
| ~ relation(relation_dom(relation_dom(relation_dom(sK14_skl)))) ),
inference(component_clause,[status(thm)],[f730]) ).
fof(f733,plain,
( ~ sQ53_spl
| sQ52_spl ),
inference(split_clause,[status(thm)],[f722,f727,f730]) ).
fof(f743,plain,
( natural(sK12_skl)
| ~ ordinal(sK12_skl) ),
inference(resolution,[status(thm)],[f213,f121]) ).
fof(f744,definition,
( sQ56_spl
<=> ordinal(sK12_skl) ),
introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition]) ).
fof(f746,plain,
( sQ56_spl
| ~ ordinal(sK12_skl) ),
inference(component_clause,[status(thm)],[f744]) ).
fof(f747,definition,
( sQ57_spl
<=> natural(sK12_skl) ),
introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition]) ).
fof(f750,plain,
( sQ57_spl
| ~ sQ56_spl ),
inference(split_clause,[status(thm)],[f743,f744,f747]) ).
fof(f751,plain,
( sQ56_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f746,f217]) ).
fof(f752,plain,
sQ56_spl,
inference(contradiction_clause,[status(thm)],[f751]) ).
fof(f753,plain,
( natural(sK20_skl)
| ~ ordinal(sK20_skl) ),
inference(resolution,[status(thm)],[f255,f121]) ).
fof(f754,definition,
( sQ58_spl
<=> ordinal(sK20_skl) ),
introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition]) ).
fof(f756,plain,
( sQ58_spl
| ~ ordinal(sK20_skl) ),
inference(component_clause,[status(thm)],[f754]) ).
fof(f757,definition,
( sQ59_spl
<=> natural(sK20_skl) ),
introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition]) ).
fof(f760,plain,
( sQ59_spl
| ~ sQ58_spl ),
inference(split_clause,[status(thm)],[f753,f754,f757]) ).
fof(f761,plain,
( sQ58_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f756,f259]) ).
fof(f762,plain,
sQ58_spl,
inference(contradiction_clause,[status(thm)],[f761]) ).
fof(f764,plain,
! [X0] : sK13_skl(X0) = empty_set,
inference(resolution,[status(thm)],[f341,f220]) ).
fof(f765,plain,
sK20_skl = empty_set,
inference(resolution,[status(thm)],[f341,f256]) ).
fof(f766,plain,
sK15_skl = empty_set,
inference(resolution,[status(thm)],[f341,f237]) ).
fof(f767,plain,
sK14_skl = empty_set,
inference(resolution,[status(thm)],[f341,f231]) ).
fof(f768,plain,
sK11_skl = empty_set,
inference(resolution,[status(thm)],[f341,f211]) ).
fof(f769,plain,
sK9_skl = empty_set,
inference(resolution,[status(thm)],[f341,f204]) ).
fof(f771,plain,
! [X0] : relation_dom(sK13_skl(X0)) = empty_set,
inference(resolution,[status(thm)],[f341,f670]) ).
fof(f772,plain,
relation_dom(sK20_skl) = empty_set,
inference(resolution,[status(thm)],[f341,f569]) ).
fof(f803,plain,
element(empty_set,positive_rationals),
inference(backward_demodulation,[status(thm)],[f765,f255]) ).
fof(f932,plain,
relation_dom(empty_set) = empty_set,
inference(forward_demodulation,[status(thm)],[f765,f772]) ).
fof(f934,plain,
( relation(empty_set)
| ~ empty(empty_set) ),
inference(paramodulation,[status(thm)],[f932,f173]) ).
fof(f1027,plain,
( sQ3_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f934,f365,f368]) ).
fof(f1028,plain,
( sQ2_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f367,f140]) ).
fof(f1029,plain,
sQ2_spl,
inference(contradiction_clause,[status(thm)],[f1028]) ).
fof(f1044,plain,
! [X0] :
( ~ empty(empty_set)
| ~ relation(sK13_skl(X0))
| empty(sK13_skl(X0)) ),
inference(paramodulation,[status(thm)],[f771,f166]) ).
fof(f1052,definition,
! [X0] :
( sQ60_spl
<=> ( ~ relation(sK13_skl(X0))
| empty(sK13_skl(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition]) ).
fof(f1055,plain,
( ~ sQ2_spl
| sQ60_spl ),
inference(split_clause,[status(thm)],[f1044,f1052,f365]) ).
fof(f1056,definition,
! [X0] :
( sQ61_spl
<=> ~ empty(sK13_skl(X0)) ),
introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition]) ).
fof(f1057,plain,
! [X0] :
( ~ sQ61_spl
| ~ empty(sK13_skl(X0)) ),
inference(component_clause,[status(thm)],[f1056]) ).
fof(f1093,plain,
( natural(empty_set)
| ~ ordinal(empty_set) ),
inference(resolution,[status(thm)],[f803,f121]) ).
fof(f1094,definition,
( sQ64_spl
<=> ordinal(empty_set) ),
introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition]) ).
fof(f1096,plain,
( sQ64_spl
| ~ ordinal(empty_set) ),
inference(component_clause,[status(thm)],[f1094]) ).
fof(f1097,definition,
( sQ65_spl
<=> natural(empty_set) ),
introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition]) ).
fof(f1100,plain,
( sQ65_spl
| ~ sQ64_spl ),
inference(split_clause,[status(thm)],[f1093,f1094,f1097]) ).
fof(f1101,plain,
( sQ64_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1096,f156]) ).
fof(f1102,plain,
sQ64_spl,
inference(contradiction_clause,[status(thm)],[f1101]) ).
fof(f1110,plain,
empty(relation_rng(empty_set)),
inference(resolution,[status(thm)],[f176,f140]) ).
fof(f1112,plain,
relation_rng(empty_set) = empty_set,
inference(resolution,[status(thm)],[f1110,f341]) ).
fof(f1168,definition,
! [X0] :
( sQ66_spl
<=> ~ finite(X0) ),
introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition]) ).
fof(f1169,plain,
! [X0] :
( ~ sQ66_spl
| ~ finite(X0) ),
inference(component_clause,[status(thm)],[f1168]) ).
fof(f1171,definition,
( sQ67_spl
<=> finite(empty_set) ),
introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition]) ).
fof(f1176,plain,
( ~ sQ66_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f186,f1169]) ).
fof(f1179,plain,
~ sQ66_spl,
inference(contradiction_clause,[status(thm)],[f1176]) ).
fof(f1183,definition,
( sQ68_spl
<=> function(empty_set) ),
introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition]) ).
fof(f1185,plain,
( sQ68_spl
| ~ function(empty_set) ),
inference(component_clause,[status(thm)],[f1183]) ).
fof(f1193,plain,
( sQ68_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1185,f358]) ).
fof(f1194,plain,
sQ68_spl,
inference(contradiction_clause,[status(thm)],[f1193]) ).
fof(f1254,plain,
! [X0,X1] : relation(first_projection_as_func_of(X0,X1)),
inference(backward_demodulation,[status(thm)],[f298,f126]) ).
fof(f1258,plain,
! [X0] :
( sQ1_spl
| ~ finite(X0)
| ~ subset(sK29_skl,X0) ),
inference(resolution,[status(thm)],[f309,f353]) ).
fof(f1436,plain,
( function_image(cartesian_product2(relation_dom(sK28_skl),relation_rng(sK28_skl)),relation_dom(sK28_skl),first_projection_as_func_of(relation_dom(sK28_skl),relation_rng(sK28_skl)),sK28_skl) = relation_dom(sK28_skl)
| ~ relation(sK28_skl) ),
inference(resolution,[status(thm)],[f306,f294]) ).
fof(f1437,plain,
( function_image(cartesian_product2(relation_dom(sK27_skl),relation_rng(sK27_skl)),relation_dom(sK27_skl),first_projection_as_func_of(relation_dom(sK27_skl),relation_rng(sK27_skl)),sK27_skl) = relation_dom(sK27_skl)
| ~ relation(sK27_skl) ),
inference(resolution,[status(thm)],[f306,f289]) ).
fof(f1438,plain,
( function_image(cartesian_product2(relation_dom(sK26_skl),relation_rng(sK26_skl)),relation_dom(sK26_skl),first_projection_as_func_of(relation_dom(sK26_skl),relation_rng(sK26_skl)),sK26_skl) = relation_dom(sK26_skl)
| ~ relation(sK26_skl) ),
inference(resolution,[status(thm)],[f306,f286]) ).
fof(f1439,plain,
( function_image(cartesian_product2(relation_dom(sK22_skl),relation_rng(sK22_skl)),relation_dom(sK22_skl),first_projection_as_func_of(relation_dom(sK22_skl),relation_rng(sK22_skl)),sK22_skl) = relation_dom(sK22_skl)
| ~ relation(sK22_skl) ),
inference(resolution,[status(thm)],[f306,f268]) ).
fof(f1440,plain,
( function_image(cartesian_product2(relation_dom(sK16_skl),relation_rng(sK16_skl)),relation_dom(sK16_skl),first_projection_as_func_of(relation_dom(sK16_skl),relation_rng(sK16_skl)),sK16_skl) = relation_dom(sK16_skl)
| ~ relation(sK16_skl) ),
inference(resolution,[status(thm)],[f306,f243]) ).
fof(f1441,plain,
( function_image(cartesian_product2(relation_dom(sK6_skl),relation_rng(sK6_skl)),relation_dom(sK6_skl),first_projection_as_func_of(relation_dom(sK6_skl),relation_rng(sK6_skl)),sK6_skl) = relation_dom(sK6_skl)
| ~ relation(sK6_skl) ),
inference(resolution,[status(thm)],[f306,f193]) ).
fof(f1442,plain,
( function_image(cartesian_product2(relation_dom(sK5_skl),relation_rng(sK5_skl)),relation_dom(sK5_skl),first_projection_as_func_of(relation_dom(sK5_skl),relation_rng(sK5_skl)),sK5_skl) = relation_dom(sK5_skl)
| ~ relation(sK5_skl) ),
inference(resolution,[status(thm)],[f306,f189]) ).
fof(f1443,plain,
( function_image(cartesian_product2(relation_dom(empty_set),relation_rng(empty_set)),relation_dom(empty_set),first_projection_as_func_of(relation_dom(empty_set),relation_rng(empty_set)),empty_set) = relation_dom(empty_set)
| ~ relation(empty_set) ),
inference(resolution,[status(thm)],[f306,f358]) ).
fof(f1444,plain,
( function_image(cartesian_product2(relation_dom(sK29_skl),relation_rng(sK29_skl)),relation_dom(sK29_skl),first_projection_as_func_of(relation_dom(sK29_skl),relation_rng(sK29_skl)),sK29_skl) = relation_dom(sK29_skl)
| ~ relation(sK29_skl) ),
inference(resolution,[status(thm)],[f306,f325]) ).
fof(f1446,definition,
( sQ76_spl
<=> relation(sK28_skl) ),
introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition]) ).
fof(f1448,plain,
( sQ76_spl
| ~ relation(sK28_skl) ),
inference(component_clause,[status(thm)],[f1446]) ).
fof(f1449,definition,
( sQ77_spl
<=> function_image(cartesian_product2(relation_dom(sK28_skl),relation_rng(sK28_skl)),relation_dom(sK28_skl),first_projection_as_func_of(relation_dom(sK28_skl),relation_rng(sK28_skl)),sK28_skl) = relation_dom(sK28_skl) ),
introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition]) ).
fof(f1452,plain,
( sQ77_spl
| ~ sQ76_spl ),
inference(split_clause,[status(thm)],[f1436,f1446,f1449]) ).
fof(f1453,definition,
( sQ78_spl
<=> relation(sK27_skl) ),
introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition]) ).
fof(f1455,plain,
( sQ78_spl
| ~ relation(sK27_skl) ),
inference(component_clause,[status(thm)],[f1453]) ).
fof(f1456,definition,
( sQ79_spl
<=> function_image(cartesian_product2(relation_dom(sK27_skl),relation_rng(sK27_skl)),relation_dom(sK27_skl),first_projection_as_func_of(relation_dom(sK27_skl),relation_rng(sK27_skl)),sK27_skl) = relation_dom(sK27_skl) ),
introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition]) ).
fof(f1459,plain,
( sQ79_spl
| ~ sQ78_spl ),
inference(split_clause,[status(thm)],[f1437,f1453,f1456]) ).
fof(f1460,definition,
( sQ80_spl
<=> relation(sK26_skl) ),
introduced(definition,[new_symbols(definition,[sQ80_spl])],[split_symbol_definition]) ).
fof(f1462,plain,
( sQ80_spl
| ~ relation(sK26_skl) ),
inference(component_clause,[status(thm)],[f1460]) ).
fof(f1463,definition,
( sQ81_spl
<=> function_image(cartesian_product2(relation_dom(sK26_skl),relation_rng(sK26_skl)),relation_dom(sK26_skl),first_projection_as_func_of(relation_dom(sK26_skl),relation_rng(sK26_skl)),sK26_skl) = relation_dom(sK26_skl) ),
introduced(definition,[new_symbols(definition,[sQ81_spl])],[split_symbol_definition]) ).
fof(f1466,plain,
( sQ81_spl
| ~ sQ80_spl ),
inference(split_clause,[status(thm)],[f1438,f1460,f1463]) ).
fof(f1467,definition,
( sQ82_spl
<=> relation(sK22_skl) ),
introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition]) ).
fof(f1469,plain,
( sQ82_spl
| ~ relation(sK22_skl) ),
inference(component_clause,[status(thm)],[f1467]) ).
fof(f1470,definition,
( sQ83_spl
<=> function_image(cartesian_product2(relation_dom(sK22_skl),relation_rng(sK22_skl)),relation_dom(sK22_skl),first_projection_as_func_of(relation_dom(sK22_skl),relation_rng(sK22_skl)),sK22_skl) = relation_dom(sK22_skl) ),
introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition]) ).
fof(f1473,plain,
( sQ83_spl
| ~ sQ82_spl ),
inference(split_clause,[status(thm)],[f1439,f1467,f1470]) ).
fof(f1474,definition,
( sQ84_spl
<=> relation(sK16_skl) ),
introduced(definition,[new_symbols(definition,[sQ84_spl])],[split_symbol_definition]) ).
fof(f1476,plain,
( sQ84_spl
| ~ relation(sK16_skl) ),
inference(component_clause,[status(thm)],[f1474]) ).
fof(f1477,definition,
( sQ85_spl
<=> function_image(cartesian_product2(relation_dom(sK16_skl),relation_rng(sK16_skl)),relation_dom(sK16_skl),first_projection_as_func_of(relation_dom(sK16_skl),relation_rng(sK16_skl)),sK16_skl) = relation_dom(sK16_skl) ),
introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition]) ).
fof(f1480,plain,
( sQ85_spl
| ~ sQ84_spl ),
inference(split_clause,[status(thm)],[f1440,f1474,f1477]) ).
fof(f1481,definition,
( sQ86_spl
<=> relation(sK6_skl) ),
introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition]) ).
fof(f1483,plain,
( sQ86_spl
| ~ relation(sK6_skl) ),
inference(component_clause,[status(thm)],[f1481]) ).
fof(f1484,definition,
( sQ87_spl
<=> function_image(cartesian_product2(relation_dom(sK6_skl),relation_rng(sK6_skl)),relation_dom(sK6_skl),first_projection_as_func_of(relation_dom(sK6_skl),relation_rng(sK6_skl)),sK6_skl) = relation_dom(sK6_skl) ),
introduced(definition,[new_symbols(definition,[sQ87_spl])],[split_symbol_definition]) ).
fof(f1487,plain,
( sQ87_spl
| ~ sQ86_spl ),
inference(split_clause,[status(thm)],[f1441,f1481,f1484]) ).
fof(f1488,definition,
( sQ88_spl
<=> relation(sK5_skl) ),
introduced(definition,[new_symbols(definition,[sQ88_spl])],[split_symbol_definition]) ).
fof(f1490,plain,
( sQ88_spl
| ~ relation(sK5_skl) ),
inference(component_clause,[status(thm)],[f1488]) ).
fof(f1491,definition,
( sQ89_spl
<=> function_image(cartesian_product2(relation_dom(sK5_skl),relation_rng(sK5_skl)),relation_dom(sK5_skl),first_projection_as_func_of(relation_dom(sK5_skl),relation_rng(sK5_skl)),sK5_skl) = relation_dom(sK5_skl) ),
introduced(definition,[new_symbols(definition,[sQ89_spl])],[split_symbol_definition]) ).
fof(f1494,plain,
( sQ89_spl
| ~ sQ88_spl ),
inference(split_clause,[status(thm)],[f1442,f1488,f1491]) ).
fof(f1495,definition,
( sQ90_spl
<=> function_image(cartesian_product2(relation_dom(empty_set),relation_rng(empty_set)),relation_dom(empty_set),first_projection_as_func_of(relation_dom(empty_set),relation_rng(empty_set)),empty_set) = relation_dom(empty_set) ),
introduced(definition,[new_symbols(definition,[sQ90_spl])],[split_symbol_definition]) ).
fof(f1498,plain,
( sQ90_spl
| ~ sQ3_spl ),
inference(split_clause,[status(thm)],[f1443,f368,f1495]) ).
fof(f1499,definition,
( sQ91_spl
<=> relation(sK29_skl) ),
introduced(definition,[new_symbols(definition,[sQ91_spl])],[split_symbol_definition]) ).
fof(f1501,plain,
( sQ91_spl
| ~ relation(sK29_skl) ),
inference(component_clause,[status(thm)],[f1499]) ).
fof(f1502,definition,
( sQ92_spl
<=> function_image(cartesian_product2(relation_dom(sK29_skl),relation_rng(sK29_skl)),relation_dom(sK29_skl),first_projection_as_func_of(relation_dom(sK29_skl),relation_rng(sK29_skl)),sK29_skl) = relation_dom(sK29_skl) ),
introduced(definition,[new_symbols(definition,[sQ92_spl])],[split_symbol_definition]) ).
fof(f1503,plain,
( ~ sQ92_spl
| function_image(cartesian_product2(relation_dom(sK29_skl),relation_rng(sK29_skl)),relation_dom(sK29_skl),first_projection_as_func_of(relation_dom(sK29_skl),relation_rng(sK29_skl)),sK29_skl) = relation_dom(sK29_skl) ),
inference(component_clause,[status(thm)],[f1502]) ).
fof(f1505,plain,
( sQ92_spl
| ~ sQ91_spl ),
inference(split_clause,[status(thm)],[f1444,f1499,f1502]) ).
fof(f1512,plain,
( sQ91_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1501,f324]) ).
fof(f1513,plain,
sQ91_spl,
inference(contradiction_clause,[status(thm)],[f1512]) ).
fof(f1514,plain,
( sQ88_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1490,f188]) ).
fof(f1515,plain,
sQ88_spl,
inference(contradiction_clause,[status(thm)],[f1514]) ).
fof(f1516,plain,
( sQ86_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1483,f192]) ).
fof(f1517,plain,
sQ86_spl,
inference(contradiction_clause,[status(thm)],[f1516]) ).
fof(f1518,plain,
( sQ84_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1476,f242]) ).
fof(f1519,plain,
sQ84_spl,
inference(contradiction_clause,[status(thm)],[f1518]) ).
fof(f1520,plain,
( sQ82_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1469,f267]) ).
fof(f1521,plain,
sQ82_spl,
inference(contradiction_clause,[status(thm)],[f1520]) ).
fof(f1522,plain,
( sQ80_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1462,f284]) ).
fof(f1523,plain,
sQ80_spl,
inference(contradiction_clause,[status(thm)],[f1522]) ).
fof(f1524,plain,
( sQ78_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1455,f288]) ).
fof(f1525,plain,
sQ78_spl,
inference(contradiction_clause,[status(thm)],[f1524]) ).
fof(f1526,plain,
( sQ76_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1448,f292]) ).
fof(f1527,plain,
sQ76_spl,
inference(contradiction_clause,[status(thm)],[f1526]) ).
fof(f1528,plain,
( ~ sQ92_spl
| relation_dom(sK29_skl) = relation_image(first_projection_as_func_of(relation_dom(sK29_skl),relation_rng(sK29_skl)),sK29_skl)
| ~ relation_of2(first_projection_as_func_of(relation_dom(sK29_skl),relation_rng(sK29_skl)),cartesian_product2(relation_dom(sK29_skl),relation_rng(sK29_skl)),relation_dom(sK29_skl))
| ~ quasi_total(first_projection_as_func_of(relation_dom(sK29_skl),relation_rng(sK29_skl)),cartesian_product2(relation_dom(sK29_skl),relation_rng(sK29_skl)),relation_dom(sK29_skl))
| ~ function(first_projection_as_func_of(relation_dom(sK29_skl),relation_rng(sK29_skl))) ),
inference(paramodulation,[status(thm)],[f1503,f297]) ).
fof(f1529,definition,
( sQ93_spl
<=> function(first_projection_as_func_of(relation_dom(sK29_skl),relation_rng(sK29_skl))) ),
introduced(definition,[new_symbols(definition,[sQ93_spl])],[split_symbol_definition]) ).
fof(f1531,plain,
( sQ93_spl
| ~ function(first_projection_as_func_of(relation_dom(sK29_skl),relation_rng(sK29_skl))) ),
inference(component_clause,[status(thm)],[f1529]) ).
fof(f1532,definition,
( sQ94_spl
<=> quasi_total(first_projection_as_func_of(relation_dom(sK29_skl),relation_rng(sK29_skl)),cartesian_product2(relation_dom(sK29_skl),relation_rng(sK29_skl)),relation_dom(sK29_skl)) ),
introduced(definition,[new_symbols(definition,[sQ94_spl])],[split_symbol_definition]) ).
fof(f1534,plain,
( sQ94_spl
| ~ quasi_total(first_projection_as_func_of(relation_dom(sK29_skl),relation_rng(sK29_skl)),cartesian_product2(relation_dom(sK29_skl),relation_rng(sK29_skl)),relation_dom(sK29_skl)) ),
inference(component_clause,[status(thm)],[f1532]) ).
fof(f1535,definition,
( sQ95_spl
<=> relation_of2(first_projection_as_func_of(relation_dom(sK29_skl),relation_rng(sK29_skl)),cartesian_product2(relation_dom(sK29_skl),relation_rng(sK29_skl)),relation_dom(sK29_skl)) ),
introduced(definition,[new_symbols(definition,[sQ95_spl])],[split_symbol_definition]) ).
fof(f1537,plain,
( sQ95_spl
| ~ relation_of2(first_projection_as_func_of(relation_dom(sK29_skl),relation_rng(sK29_skl)),cartesian_product2(relation_dom(sK29_skl),relation_rng(sK29_skl)),relation_dom(sK29_skl)) ),
inference(component_clause,[status(thm)],[f1535]) ).
fof(f1538,definition,
( sQ96_spl
<=> relation_dom(sK29_skl) = relation_image(first_projection_as_func_of(relation_dom(sK29_skl),relation_rng(sK29_skl)),sK29_skl) ),
introduced(definition,[new_symbols(definition,[sQ96_spl])],[split_symbol_definition]) ).
fof(f1539,plain,
( ~ sQ96_spl
| relation_dom(sK29_skl) = relation_image(first_projection_as_func_of(relation_dom(sK29_skl),relation_rng(sK29_skl)),sK29_skl) ),
inference(component_clause,[status(thm)],[f1538]) ).
fof(f1541,plain,
( ~ sQ92_spl
| sQ96_spl
| ~ sQ95_spl
| ~ sQ94_spl
| ~ sQ93_spl ),
inference(split_clause,[status(thm)],[f1528,f1529,f1532,f1535,f1538,f1502]) ).
fof(f1542,plain,
( sQ94_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1534,f130]) ).
fof(f1543,plain,
sQ94_spl,
inference(contradiction_clause,[status(thm)],[f1542]) ).
fof(f1544,plain,
( sQ93_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1531,f129]) ).
fof(f1545,plain,
sQ93_spl,
inference(contradiction_clause,[status(thm)],[f1544]) ).
fof(f1571,plain,
( ~ sQ61_spl
| ~ empty(empty_set) ),
inference(forward_demodulation,[status(thm)],[f764,f1057]) ).
fof(f1572,plain,
( ~ sQ61_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1571,f140]) ).
fof(f1573,plain,
~ sQ61_spl,
inference(contradiction_clause,[status(thm)],[f1572]) ).
fof(f1574,plain,
( sQ53_spl
| ~ relation(relation_dom(relation_dom(relation_dom(empty_set)))) ),
inference(forward_demodulation,[status(thm)],[f767,f732]) ).
fof(f1575,plain,
( sQ53_spl
| ~ relation(relation_dom(relation_dom(empty_set))) ),
inference(forward_demodulation,[status(thm)],[f932,f1574]) ).
fof(f1576,plain,
( sQ53_spl
| ~ relation(relation_dom(empty_set)) ),
inference(forward_demodulation,[status(thm)],[f932,f1575]) ).
fof(f1577,plain,
( sQ53_spl
| ~ relation(empty_set) ),
inference(forward_demodulation,[status(thm)],[f932,f1576]) ).
fof(f1578,plain,
( sQ53_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1577,f357]) ).
fof(f1579,plain,
sQ53_spl,
inference(contradiction_clause,[status(thm)],[f1578]) ).
fof(f1580,plain,
( sQ51_spl
| ~ relation(relation_dom(relation_dom(relation_dom(empty_set)))) ),
inference(forward_demodulation,[status(thm)],[f768,f699]) ).
fof(f1581,plain,
( sQ51_spl
| ~ relation(relation_dom(relation_dom(empty_set))) ),
inference(forward_demodulation,[status(thm)],[f932,f1580]) ).
fof(f1582,plain,
( sQ51_spl
| ~ relation(relation_dom(empty_set)) ),
inference(forward_demodulation,[status(thm)],[f932,f1581]) ).
fof(f1583,plain,
( sQ51_spl
| ~ relation(empty_set) ),
inference(forward_demodulation,[status(thm)],[f932,f1582]) ).
fof(f1584,plain,
( sQ51_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1583,f357]) ).
fof(f1585,plain,
sQ51_spl,
inference(contradiction_clause,[status(thm)],[f1584]) ).
fof(f1586,plain,
( sQ49_spl
| ~ relation(relation_dom(relation_dom(relation_dom(empty_set)))) ),
inference(forward_demodulation,[status(thm)],[f769,f668]) ).
fof(f1587,plain,
( sQ49_spl
| ~ relation(relation_dom(relation_dom(empty_set))) ),
inference(forward_demodulation,[status(thm)],[f932,f1586]) ).
fof(f1588,plain,
( sQ49_spl
| ~ relation(relation_dom(empty_set)) ),
inference(forward_demodulation,[status(thm)],[f932,f1587]) ).
fof(f1589,plain,
( sQ49_spl
| ~ relation(empty_set) ),
inference(forward_demodulation,[status(thm)],[f932,f1588]) ).
fof(f1590,plain,
( sQ49_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1589,f357]) ).
fof(f1591,plain,
sQ49_spl,
inference(contradiction_clause,[status(thm)],[f1590]) ).
fof(f1592,plain,
( sQ47_spl
| ~ relation(relation_dom(relation_dom(empty_set))) ),
inference(forward_demodulation,[status(thm)],[f765,f656]) ).
fof(f1593,plain,
( sQ47_spl
| ~ relation(relation_dom(empty_set)) ),
inference(forward_demodulation,[status(thm)],[f932,f1592]) ).
fof(f1594,plain,
( sQ47_spl
| ~ relation(empty_set) ),
inference(forward_demodulation,[status(thm)],[f932,f1593]) ).
fof(f1595,plain,
( sQ47_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1594,f357]) ).
fof(f1596,plain,
sQ47_spl,
inference(contradiction_clause,[status(thm)],[f1595]) ).
fof(f1597,plain,
( sQ45_spl
| ~ relation(relation_dom(relation_dom(empty_set))) ),
inference(forward_demodulation,[status(thm)],[f766,f644]) ).
fof(f1598,plain,
( sQ45_spl
| ~ relation(relation_dom(empty_set)) ),
inference(forward_demodulation,[status(thm)],[f932,f1597]) ).
fof(f1599,plain,
( sQ45_spl
| ~ relation(empty_set) ),
inference(forward_demodulation,[status(thm)],[f932,f1598]) ).
fof(f1600,plain,
( sQ45_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1599,f357]) ).
fof(f1601,plain,
sQ45_spl,
inference(contradiction_clause,[status(thm)],[f1600]) ).
fof(f1602,plain,
( sQ43_spl
| ~ relation(relation_dom(relation_dom(empty_set))) ),
inference(forward_demodulation,[status(thm)],[f767,f632]) ).
fof(f1603,plain,
( sQ43_spl
| ~ relation(relation_dom(empty_set)) ),
inference(forward_demodulation,[status(thm)],[f932,f1602]) ).
fof(f1604,plain,
( sQ43_spl
| ~ relation(empty_set) ),
inference(forward_demodulation,[status(thm)],[f932,f1603]) ).
fof(f1605,plain,
( sQ43_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1604,f357]) ).
fof(f1606,plain,
sQ43_spl,
inference(contradiction_clause,[status(thm)],[f1605]) ).
fof(f1607,plain,
( sQ41_spl
| ~ relation(relation_dom(relation_dom(empty_set))) ),
inference(forward_demodulation,[status(thm)],[f768,f619]) ).
fof(f1608,plain,
( sQ41_spl
| ~ relation(relation_dom(empty_set)) ),
inference(forward_demodulation,[status(thm)],[f932,f1607]) ).
fof(f1609,plain,
( sQ41_spl
| ~ relation(empty_set) ),
inference(forward_demodulation,[status(thm)],[f932,f1608]) ).
fof(f1610,plain,
( sQ41_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1609,f357]) ).
fof(f1611,plain,
sQ41_spl,
inference(contradiction_clause,[status(thm)],[f1610]) ).
fof(f1612,plain,
( sQ39_spl
| ~ relation(relation_dom(relation_dom(empty_set))) ),
inference(forward_demodulation,[status(thm)],[f769,f607]) ).
fof(f1613,plain,
( sQ39_spl
| ~ relation(relation_dom(empty_set)) ),
inference(forward_demodulation,[status(thm)],[f932,f1612]) ).
fof(f1614,plain,
( sQ39_spl
| ~ relation(empty_set) ),
inference(forward_demodulation,[status(thm)],[f932,f1613]) ).
fof(f1615,plain,
( sQ39_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1614,f357]) ).
fof(f1616,plain,
sQ39_spl,
inference(contradiction_clause,[status(thm)],[f1615]) ).
fof(f1617,plain,
( sQ37_spl
| ~ relation(relation_dom(empty_set)) ),
inference(forward_demodulation,[status(thm)],[f765,f595]) ).
fof(f1618,plain,
( sQ37_spl
| ~ relation(empty_set) ),
inference(forward_demodulation,[status(thm)],[f932,f1617]) ).
fof(f1619,plain,
( sQ37_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1618,f357]) ).
fof(f1620,plain,
sQ37_spl,
inference(contradiction_clause,[status(thm)],[f1619]) ).
fof(f1621,plain,
( sQ35_spl
| ~ relation(empty_set) ),
inference(forward_demodulation,[status(thm)],[f765,f583]) ).
fof(f1622,plain,
( sQ35_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1621,f357]) ).
fof(f1623,plain,
sQ35_spl,
inference(contradiction_clause,[status(thm)],[f1622]) ).
fof(f1624,plain,
( sQ33_spl
| ~ relation(relation_dom(empty_set)) ),
inference(forward_demodulation,[status(thm)],[f766,f567]) ).
fof(f1625,plain,
( sQ33_spl
| ~ relation(empty_set) ),
inference(forward_demodulation,[status(thm)],[f932,f1624]) ).
fof(f1626,plain,
( sQ33_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1625,f357]) ).
fof(f1627,plain,
sQ33_spl,
inference(contradiction_clause,[status(thm)],[f1626]) ).
fof(f1628,plain,
( sQ31_spl
| ~ relation(relation_dom(empty_set)) ),
inference(forward_demodulation,[status(thm)],[f767,f555]) ).
fof(f1629,plain,
( sQ31_spl
| ~ relation(empty_set) ),
inference(forward_demodulation,[status(thm)],[f932,f1628]) ).
fof(f1630,plain,
( sQ31_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1629,f357]) ).
fof(f1631,plain,
sQ31_spl,
inference(contradiction_clause,[status(thm)],[f1630]) ).
fof(f1632,plain,
( sQ29_spl
| ~ relation(empty_set) ),
inference(forward_demodulation,[status(thm)],[f766,f543]) ).
fof(f1633,plain,
( sQ29_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1632,f357]) ).
fof(f1634,plain,
sQ29_spl,
inference(contradiction_clause,[status(thm)],[f1633]) ).
fof(f1635,plain,
( sQ27_spl
| ~ relation(empty_set) ),
inference(forward_demodulation,[status(thm)],[f767,f531]) ).
fof(f1636,plain,
( sQ27_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1635,f357]) ).
fof(f1637,plain,
sQ27_spl,
inference(contradiction_clause,[status(thm)],[f1636]) ).
fof(f1638,plain,
( sQ25_spl
| ~ relation(relation_dom(empty_set)) ),
inference(forward_demodulation,[status(thm)],[f768,f510]) ).
fof(f1639,plain,
( sQ25_spl
| ~ relation(empty_set) ),
inference(forward_demodulation,[status(thm)],[f932,f1638]) ).
fof(f1640,plain,
( sQ25_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1639,f357]) ).
fof(f1641,plain,
sQ25_spl,
inference(contradiction_clause,[status(thm)],[f1640]) ).
fof(f1642,plain,
( sQ23_spl
| ~ relation(relation_dom(empty_set)) ),
inference(forward_demodulation,[status(thm)],[f769,f498]) ).
fof(f1643,plain,
( sQ23_spl
| ~ relation(empty_set) ),
inference(forward_demodulation,[status(thm)],[f932,f1642]) ).
fof(f1644,plain,
( sQ23_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1643,f357]) ).
fof(f1645,plain,
sQ23_spl,
inference(contradiction_clause,[status(thm)],[f1644]) ).
fof(f1646,plain,
( sQ21_spl
| ~ relation(empty_set) ),
inference(forward_demodulation,[status(thm)],[f768,f486]) ).
fof(f1647,plain,
( sQ21_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1646,f357]) ).
fof(f1648,plain,
sQ21_spl,
inference(contradiction_clause,[status(thm)],[f1647]) ).
fof(f1649,plain,
( sQ19_spl
| ~ relation(empty_set) ),
inference(forward_demodulation,[status(thm)],[f769,f474]) ).
fof(f1650,plain,
( sQ19_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1649,f357]) ).
fof(f1651,plain,
sQ19_spl,
inference(contradiction_clause,[status(thm)],[f1650]) ).
fof(f1652,plain,
( sQ17_spl
| ~ relation(relation_dom(relation_dom(relation_dom(relation_dom(relation_dom(relation_dom(empty_set))))))) ),
inference(forward_demodulation,[status(thm)],[f932,f454]) ).
fof(f1653,plain,
( sQ17_spl
| ~ relation(relation_dom(relation_dom(relation_dom(relation_dom(relation_dom(empty_set)))))) ),
inference(forward_demodulation,[status(thm)],[f932,f1652]) ).
fof(f1654,plain,
( sQ17_spl
| ~ relation(relation_dom(relation_dom(relation_dom(relation_dom(empty_set))))) ),
inference(forward_demodulation,[status(thm)],[f932,f1653]) ).
fof(f1655,plain,
( sQ17_spl
| ~ relation(relation_dom(relation_dom(relation_dom(empty_set)))) ),
inference(forward_demodulation,[status(thm)],[f932,f1654]) ).
fof(f1656,plain,
( sQ17_spl
| ~ relation(relation_dom(relation_dom(empty_set))) ),
inference(forward_demodulation,[status(thm)],[f932,f1655]) ).
fof(f1657,plain,
( sQ17_spl
| ~ relation(relation_dom(empty_set)) ),
inference(forward_demodulation,[status(thm)],[f932,f1656]) ).
fof(f1658,plain,
( sQ17_spl
| ~ relation(empty_set) ),
inference(forward_demodulation,[status(thm)],[f932,f1657]) ).
fof(f1659,plain,
( sQ17_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1658,f357]) ).
fof(f1660,plain,
sQ17_spl,
inference(contradiction_clause,[status(thm)],[f1659]) ).
fof(f1661,plain,
( sQ15_spl
| ~ relation(relation_dom(relation_dom(relation_dom(relation_dom(relation_dom(empty_set)))))) ),
inference(forward_demodulation,[status(thm)],[f932,f442]) ).
fof(f1662,plain,
( sQ15_spl
| ~ relation(relation_dom(relation_dom(relation_dom(relation_dom(empty_set))))) ),
inference(forward_demodulation,[status(thm)],[f932,f1661]) ).
fof(f1663,plain,
( sQ15_spl
| ~ relation(relation_dom(relation_dom(relation_dom(empty_set)))) ),
inference(forward_demodulation,[status(thm)],[f932,f1662]) ).
fof(f1664,plain,
( sQ15_spl
| ~ relation(relation_dom(relation_dom(empty_set))) ),
inference(forward_demodulation,[status(thm)],[f932,f1663]) ).
fof(f1665,plain,
( sQ15_spl
| ~ relation(relation_dom(empty_set)) ),
inference(forward_demodulation,[status(thm)],[f932,f1664]) ).
fof(f1666,plain,
( sQ15_spl
| ~ relation(empty_set) ),
inference(forward_demodulation,[status(thm)],[f932,f1665]) ).
fof(f1667,plain,
( sQ15_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1666,f357]) ).
fof(f1668,plain,
sQ15_spl,
inference(contradiction_clause,[status(thm)],[f1667]) ).
fof(f1669,plain,
( sQ13_spl
| ~ relation(relation_dom(relation_dom(relation_dom(relation_dom(empty_set))))) ),
inference(forward_demodulation,[status(thm)],[f932,f430]) ).
fof(f1670,plain,
( sQ13_spl
| ~ relation(relation_dom(relation_dom(relation_dom(empty_set)))) ),
inference(forward_demodulation,[status(thm)],[f932,f1669]) ).
fof(f1671,plain,
( sQ13_spl
| ~ relation(relation_dom(relation_dom(empty_set))) ),
inference(forward_demodulation,[status(thm)],[f932,f1670]) ).
fof(f1672,plain,
( sQ13_spl
| ~ relation(relation_dom(empty_set)) ),
inference(forward_demodulation,[status(thm)],[f932,f1671]) ).
fof(f1673,plain,
( sQ13_spl
| ~ relation(empty_set) ),
inference(forward_demodulation,[status(thm)],[f932,f1672]) ).
fof(f1674,plain,
( sQ13_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1673,f357]) ).
fof(f1675,plain,
sQ13_spl,
inference(contradiction_clause,[status(thm)],[f1674]) ).
fof(f1676,plain,
( sQ11_spl
| ~ relation(relation_dom(relation_dom(relation_dom(empty_set)))) ),
inference(forward_demodulation,[status(thm)],[f932,f418]) ).
fof(f1677,plain,
( sQ11_spl
| ~ relation(relation_dom(relation_dom(empty_set))) ),
inference(forward_demodulation,[status(thm)],[f932,f1676]) ).
fof(f1678,plain,
( sQ11_spl
| ~ relation(relation_dom(empty_set)) ),
inference(forward_demodulation,[status(thm)],[f932,f1677]) ).
fof(f1679,plain,
( sQ11_spl
| ~ relation(empty_set) ),
inference(forward_demodulation,[status(thm)],[f932,f1678]) ).
fof(f1680,plain,
( sQ11_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1679,f357]) ).
fof(f1681,plain,
sQ11_spl,
inference(contradiction_clause,[status(thm)],[f1680]) ).
fof(f1682,plain,
( sQ9_spl
| ~ relation(relation_dom(relation_dom(empty_set))) ),
inference(forward_demodulation,[status(thm)],[f932,f406]) ).
fof(f1683,plain,
( sQ9_spl
| ~ relation(relation_dom(empty_set)) ),
inference(forward_demodulation,[status(thm)],[f932,f1682]) ).
fof(f1684,plain,
( sQ9_spl
| ~ relation(empty_set) ),
inference(forward_demodulation,[status(thm)],[f932,f1683]) ).
fof(f1685,plain,
( sQ9_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1684,f357]) ).
fof(f1686,plain,
sQ9_spl,
inference(contradiction_clause,[status(thm)],[f1685]) ).
fof(f1687,plain,
( sQ7_spl
| ~ relation(relation_dom(empty_set)) ),
inference(forward_demodulation,[status(thm)],[f932,f394]) ).
fof(f1688,plain,
( sQ7_spl
| ~ relation(empty_set) ),
inference(forward_demodulation,[status(thm)],[f932,f1687]) ).
fof(f1689,plain,
( sQ7_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1688,f357]) ).
fof(f1690,plain,
sQ7_spl,
inference(contradiction_clause,[status(thm)],[f1689]) ).
fof(f1691,plain,
( sQ5_spl
| ~ relation(empty_set) ),
inference(forward_demodulation,[status(thm)],[f932,f382]) ).
fof(f1692,plain,
( sQ5_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1691,f357]) ).
fof(f1693,plain,
sQ5_spl,
inference(contradiction_clause,[status(thm)],[f1692]) ).
fof(f1772,plain,
( sQ1_spl
| ~ finite(cartesian_product2(relation_dom(sK29_skl),relation_rng(sK29_skl)))
| ~ relation(sK29_skl) ),
inference(resolution,[status(thm)],[f318,f1258]) ).
fof(f1773,plain,
( subset(empty_set,cartesian_product2(empty_set,relation_rng(empty_set)))
| ~ relation(empty_set) ),
inference(paramodulation,[status(thm)],[f932,f318]) ).
fof(f1774,plain,
( subset(empty_set,cartesian_product2(relation_dom(empty_set),empty_set))
| ~ relation(empty_set) ),
inference(paramodulation,[status(thm)],[f1112,f318]) ).
fof(f1775,definition,
( sQ99_spl
<=> finite(cartesian_product2(relation_dom(sK29_skl),relation_rng(sK29_skl))) ),
introduced(definition,[new_symbols(definition,[sQ99_spl])],[split_symbol_definition]) ).
fof(f1777,plain,
( sQ99_spl
| ~ finite(cartesian_product2(relation_dom(sK29_skl),relation_rng(sK29_skl))) ),
inference(component_clause,[status(thm)],[f1775]) ).
fof(f1778,plain,
( sQ1_spl
| ~ sQ99_spl
| ~ sQ91_spl ),
inference(split_clause,[status(thm)],[f1772,f1499,f1775,f351]) ).
fof(f1779,definition,
( sQ100_spl
<=> subset(empty_set,cartesian_product2(empty_set,relation_rng(empty_set))) ),
introduced(definition,[new_symbols(definition,[sQ100_spl])],[split_symbol_definition]) ).
fof(f1782,plain,
( sQ100_spl
| ~ sQ3_spl ),
inference(split_clause,[status(thm)],[f1773,f368,f1779]) ).
fof(f1783,definition,
( sQ101_spl
<=> subset(empty_set,cartesian_product2(relation_dom(empty_set),empty_set)) ),
introduced(definition,[new_symbols(definition,[sQ101_spl])],[split_symbol_definition]) ).
fof(f1786,plain,
( sQ101_spl
| ~ sQ3_spl ),
inference(split_clause,[status(thm)],[f1774,f368,f1783]) ).
fof(f1810,definition,
( sQ104_spl
<=> function(first_projection_as_func_of(empty_set,empty_set)) ),
introduced(definition,[new_symbols(definition,[sQ104_spl])],[split_symbol_definition]) ).
fof(f1812,plain,
( sQ104_spl
| ~ function(first_projection_as_func_of(empty_set,empty_set)) ),
inference(component_clause,[status(thm)],[f1810]) ).
fof(f1813,definition,
( sQ105_spl
<=> quasi_total(first_projection_as_func_of(empty_set,empty_set),cartesian_product2(empty_set,empty_set),empty_set) ),
introduced(definition,[new_symbols(definition,[sQ105_spl])],[split_symbol_definition]) ).
fof(f1815,plain,
( sQ105_spl
| ~ quasi_total(first_projection_as_func_of(empty_set,empty_set),cartesian_product2(empty_set,empty_set),empty_set) ),
inference(component_clause,[status(thm)],[f1813]) ).
fof(f1823,plain,
( sQ105_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1815,f130]) ).
fof(f1824,plain,
sQ105_spl,
inference(contradiction_clause,[status(thm)],[f1823]) ).
fof(f1825,plain,
( sQ104_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1812,f129]) ).
fof(f1826,plain,
sQ104_spl,
inference(contradiction_clause,[status(thm)],[f1825]) ).
fof(f1827,plain,
( ~ sQ96_spl
| finite(relation_dom(sK29_skl))
| ~ finite(sK29_skl)
| ~ function(first_projection_as_func_of(relation_dom(sK29_skl),relation_rng(sK29_skl)))
| ~ relation(first_projection_as_func_of(relation_dom(sK29_skl),relation_rng(sK29_skl))) ),
inference(paramodulation,[status(thm)],[f1539,f312]) ).
fof(f1828,definition,
( sQ108_spl
<=> relation(first_projection_as_func_of(relation_dom(sK29_skl),relation_rng(sK29_skl))) ),
introduced(definition,[new_symbols(definition,[sQ108_spl])],[split_symbol_definition]) ).
fof(f1830,plain,
( sQ108_spl
| ~ relation(first_projection_as_func_of(relation_dom(sK29_skl),relation_rng(sK29_skl))) ),
inference(component_clause,[status(thm)],[f1828]) ).
fof(f1831,plain,
( ~ sQ96_spl
| sQ0_spl
| ~ sQ1_spl
| ~ sQ93_spl
| ~ sQ108_spl ),
inference(split_clause,[status(thm)],[f1827,f1828,f1529,f351,f348,f1538]) ).
fof(f1832,plain,
( sQ108_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1830,f1254]) ).
fof(f1833,plain,
sQ108_spl,
inference(contradiction_clause,[status(thm)],[f1832]) ).
fof(f1851,plain,
( finite(empty_set)
| ~ finite(relation_dom(empty_set))
| ~ function(empty_set)
| ~ relation(empty_set) ),
inference(paramodulation,[status(thm)],[f1112,f320]) ).
fof(f1852,definition,
( sQ109_spl
<=> finite(relation_dom(empty_set)) ),
introduced(definition,[new_symbols(definition,[sQ109_spl])],[split_symbol_definition]) ).
fof(f1854,plain,
( sQ109_spl
| ~ finite(relation_dom(empty_set)) ),
inference(component_clause,[status(thm)],[f1852]) ).
fof(f1855,plain,
( sQ67_spl
| ~ sQ109_spl
| ~ sQ68_spl
| ~ sQ3_spl ),
inference(split_clause,[status(thm)],[f1851,f368,f1183,f1852,f1171]) ).
fof(f1856,plain,
( sQ109_spl
| ~ finite(empty_set) ),
inference(forward_demodulation,[status(thm)],[f932,f1854]) ).
fof(f1857,plain,
( sQ109_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1856,f359]) ).
fof(f1858,plain,
sQ109_spl,
inference(contradiction_clause,[status(thm)],[f1857]) ).
fof(f1864,plain,
( sQ99_spl
| ~ finite(relation_rng(sK29_skl))
| ~ finite(relation_dom(sK29_skl)) ),
inference(resolution,[status(thm)],[f1777,f314]) ).
fof(f1866,definition,
( sQ110_spl
<=> finite(relation_rng(sK29_skl)) ),
introduced(definition,[new_symbols(definition,[sQ110_spl])],[split_symbol_definition]) ).
fof(f1868,plain,
( sQ110_spl
| ~ finite(relation_rng(sK29_skl)) ),
inference(component_clause,[status(thm)],[f1866]) ).
fof(f1869,plain,
( sQ99_spl
| ~ sQ110_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f1864,f348,f1866,f1775]) ).
fof(f1870,plain,
( sQ110_spl
| ~ finite(relation_dom(sK29_skl))
| ~ function(sK29_skl)
| ~ relation(sK29_skl) ),
inference(resolution,[status(thm)],[f1868,f320]) ).
fof(f1872,definition,
( sQ111_spl
<=> function(sK29_skl) ),
introduced(definition,[new_symbols(definition,[sQ111_spl])],[split_symbol_definition]) ).
fof(f1874,plain,
( sQ111_spl
| ~ function(sK29_skl) ),
inference(component_clause,[status(thm)],[f1872]) ).
fof(f1875,plain,
( sQ110_spl
| ~ sQ0_spl
| ~ sQ111_spl
| ~ sQ91_spl ),
inference(split_clause,[status(thm)],[f1870,f1499,f1872,f348,f1866]) ).
fof(f1876,plain,
( sQ111_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1874,f325]) ).
fof(f1877,plain,
sQ111_spl,
inference(contradiction_clause,[status(thm)],[f1876]) ).
fof(f1896,plain,
( sQ95_spl
| ~ relation_of2_as_subset(first_projection_as_func_of(relation_dom(sK29_skl),relation_rng(sK29_skl)),cartesian_product2(relation_dom(sK29_skl),relation_rng(sK29_skl)),relation_dom(sK29_skl)) ),
inference(resolution,[status(thm)],[f1537,f301]) ).
fof(f1897,plain,
( sQ95_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1896,f131]) ).
fof(f1898,plain,
sQ95_spl,
inference(contradiction_clause,[status(thm)],[f1897]) ).
fof(f1899,plain,
$false,
inference(sat_refutation,[status(thm)],[f354,f355,f383,f395,f407,f419,f431,f443,f455,f475,f487,f499,f511,f532,f544,f556,f568,f584,f596,f608,f620,f633,f645,f657,f669,f700,f733,f750,f752,f760,f762,f1027,f1029,f1055,f1100,f1102,f1179,f1194,f1452,f1459,f1466,f1473,f1480,f1487,f1494,f1498,f1505,f1513,f1515,f1517,f1519,f1521,f1523,f1525,f1527,f1541,f1543,f1545,f1573,f1579,f1585,f1591,f1596,f1601,f1606,f1611,f1616,f1620,f1623,f1627,f1631,f1634,f1637,f1641,f1645,f1648,f1651,f1660,f1668,f1675,f1681,f1686,f1690,f1693,f1778,f1782,f1786,f1824,f1826,f1831,f1833,f1855,f1858,f1869,f1875,f1877,f1898]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU098+1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n007.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Mon Sep 21 05:48:06 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.38 % Drodi V4.1.1
% 0.14/0.41 % Refutation found
% 0.14/0.41 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.14/0.41 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.14/0.43 % Elapsed time: 0.063017 seconds
% 0.14/0.43 % CPU time: 0.313503 seconds
% 0.14/0.43 % Total memory used: 112.302 MB
% 0.14/0.43 % Net memory used: 112.005 MB
%------------------------------------------------------------------------------