%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SET018-6 : TPTP v9.3.1. Bugfixed v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 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 : Thu Sep 24 02:08:54 PM UTC 2026
% Result : Unsatisfiable 60.76s 8.14s
% Output : CNFRefutation 4.60s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 256
% Syntax : Number of formulae : 1075 ( 80 unt; 212 def)
% Number of atoms : 2676 ( 405 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 2845 (1244 ~;1389 |; 0 &)
% ( 212 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of predicates : 218 ( 216 usr; 213 prp; 0-2 aty)
% Number of functors : 32 ( 32 usr; 12 con; 0-3 aty)
% Number of variables : 541 ( 541 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X,Y,U] :
( member(U,Y)
| ~ member(U,X)
| ~ subclass(X,Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [X,Y] :
( subclass(X,Y)
| member(not_subclass_element(X,Y),X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [X,Y] :
( subclass(X,Y)
| ~ member(not_subclass_element(X,Y),Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [X] : subclass(X,universal_class),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [X,Y] :
( X = Y
| ~ subclass(Y,X)
| ~ subclass(X,Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [U,X,Y] :
( U = Y
| U = X
| ~ member(U,unordered_pair(X,Y)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [X,Y] :
( member(X,unordered_pair(X,Y))
| ~ member(X,universal_class) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f10,axiom,
! [Y,X] :
( member(Y,unordered_pair(X,Y))
| ~ member(Y,universal_class) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f11,axiom,
! [X,Y] : member(unordered_pair(X,Y),universal_class),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [X] : unordered_pair(X,X) = singleton(X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f13,axiom,
! [X,Y] : unordered_pair(singleton(X),unordered_pair(X,singleton(Y))) = ordered_pair(X,Y),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f14,axiom,
! [U,V,X,Y] :
( member(U,X)
| ~ member(ordered_pair(U,V),cross_product(X,Y)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f15,axiom,
! [U,V,X,Y] :
( member(V,Y)
| ~ member(ordered_pair(U,V),cross_product(X,Y)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f16,axiom,
! [U,X,V,Y] :
( member(ordered_pair(U,V),cross_product(X,Y))
| ~ member(V,Y)
| ~ member(U,X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f18,axiom,
subclass(element_relation,cross_product(universal_class,universal_class)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f19,axiom,
! [X,Y] :
( member(X,Y)
| ~ member(ordered_pair(X,Y),element_relation) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f21,axiom,
! [Z,X,Y] :
( member(Z,X)
| ~ member(Z,intersection(X,Y)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f22,axiom,
! [Z,X,Y] :
( member(Z,Y)
| ~ member(Z,intersection(X,Y)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f23,axiom,
! [Z,X,Y] :
( member(Z,intersection(X,Y))
| ~ member(Z,Y)
| ~ member(Z,X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f24,axiom,
! [Z,X] :
( ~ member(Z,X)
| ~ member(Z,complement(X)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f25,axiom,
! [Z,X] :
( member(Z,X)
| member(Z,complement(X))
| ~ member(Z,universal_class) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f26,axiom,
! [X,Y] : complement(intersection(complement(X),complement(Y))) = union(X,Y),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f27,axiom,
! [X,Y] : intersection(complement(intersection(X,Y)),complement(intersection(complement(X),complement(Y)))) = symmetric_difference(X,Y),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f28,axiom,
! [Xr,X,Y] : intersection(Xr,cross_product(X,Y)) = restrict(Xr,X,Y),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f29,axiom,
! [X,Y,Xr] : intersection(cross_product(X,Y),Xr) = restrict(Xr,X,Y),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f30,axiom,
! [X,Z] :
( ~ member(Z,domain_of(X))
| restrict(X,singleton(Z),universal_class) != null_class ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f31,axiom,
! [Z,X] :
( member(Z,domain_of(X))
| restrict(X,singleton(Z),universal_class) = null_class
| ~ member(Z,universal_class) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f47,axiom,
! [X] :
( member(null_class,X)
| ~ inductive(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f49,axiom,
! [X] :
( inductive(X)
| ~ subclass(image(successor_relation,X),X)
| ~ member(null_class,X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f50,axiom,
inductive(omega),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f51,axiom,
! [Y] :
( subclass(omega,Y)
| ~ inductive(Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f52,axiom,
member(omega,universal_class),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f55,axiom,
! [X] : complement(image(element_relation,complement(X))) = power_class(X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f59,axiom,
! [Z,Yr,Xr,Y] :
( member(ordered_pair(Y,Z),compose(Yr,Xr))
| ~ member(ordered_pair(Y,Z),cross_product(universal_class,universal_class))
| ~ member(Z,image(Yr,image(Xr,singleton(Y)))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f66,axiom,
! [X] :
( member(regular(X),X)
| X = null_class ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f67,axiom,
! [X] :
( intersection(X,regular(X)) = null_class
| X = null_class ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f69,axiom,
function(choice),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f70,axiom,
! [Y] :
( member(apply(choice,Y),Y)
| Y = null_class
| ~ member(Y,universal_class) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f74,axiom,
intersection(cross_product(universal_class,universal_class),intersection(cross_product(universal_class,universal_class),complement(compose(complement(element_relation),inverse(element_relation))))) = subset_relation,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f76,axiom,
! [Xr] : complement(domain_of(intersection(Xr,identity_relation))) = diagonalise(Xr),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f77,axiom,
! [X] : intersection(domain_of(X),diagonalise(compose(inverse(element_relation),X))) = cantor(X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f92,negated_conjecture,
ordered_pair(w,x) = ordered_pair(y,z),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f93,negated_conjecture,
member(x,universal_class),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f94,negated_conjecture,
x != z,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f95,plain,
! [Y,U] :
( member(U,Y)
| ! [X] :
( ~ member(U,X)
| ~ subclass(X,Y) ) ),
inference(miniscoping,[status(thm)],[f1]) ).
fof(f96,plain,
! [X0,X1,X2] :
( member(X2,X1)
| ~ member(X2,X0)
| ~ subclass(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f95]) ).
fof(f97,plain,
! [X0,X1] :
( subclass(X0,X1)
| member(not_subclass_element(X0,X1),X0) ),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f98,plain,
! [X0,X1] :
( subclass(X0,X1)
| ~ member(not_subclass_element(X0,X1),X1) ),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f99,plain,
! [X0] : subclass(X0,universal_class),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f102,plain,
! [X0,X1] :
( X0 = X1
| ~ subclass(X1,X0)
| ~ subclass(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f103,plain,
! [U,Y] :
( U = Y
| ! [X] :
( U = X
| ~ member(U,unordered_pair(X,Y)) ) ),
inference(miniscoping,[status(thm)],[f8]) ).
fof(f104,plain,
! [X0,X1,X2] :
( X0 = X2
| X0 = X1
| ~ member(X0,unordered_pair(X1,X2)) ),
inference(cnf_transformation,[status(thm)],[f103]) ).
fof(f105,plain,
! [X] :
( ! [Y] : member(X,unordered_pair(X,Y))
| ~ member(X,universal_class) ),
inference(miniscoping,[status(thm)],[f9]) ).
fof(f106,plain,
! [X0,X1] :
( member(X0,unordered_pair(X0,X1))
| ~ member(X0,universal_class) ),
inference(cnf_transformation,[status(thm)],[f105]) ).
fof(f107,plain,
! [Y] :
( ! [X] : member(Y,unordered_pair(X,Y))
| ~ member(Y,universal_class) ),
inference(miniscoping,[status(thm)],[f10]) ).
fof(f108,plain,
! [X0,X1] :
( member(X0,unordered_pair(X1,X0))
| ~ member(X0,universal_class) ),
inference(cnf_transformation,[status(thm)],[f107]) ).
fof(f109,plain,
! [X0,X1] : member(unordered_pair(X0,X1),universal_class),
inference(cnf_transformation,[status(thm)],[f11]) ).
fof(f110,plain,
! [X0] : unordered_pair(X0,X0) = singleton(X0),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f111,plain,
! [X0,X1] : unordered_pair(singleton(X0),unordered_pair(X0,singleton(X1))) = ordered_pair(X0,X1),
inference(cnf_transformation,[status(thm)],[f13]) ).
fof(f112,plain,
! [U,X] :
( member(U,X)
| ! [V,Y] : ~ member(ordered_pair(U,V),cross_product(X,Y)) ),
inference(miniscoping,[status(thm)],[f14]) ).
fof(f113,plain,
! [X0,X1,X2,X3] :
( member(X0,X2)
| ~ member(ordered_pair(X0,X1),cross_product(X2,X3)) ),
inference(cnf_transformation,[status(thm)],[f112]) ).
fof(f114,plain,
! [V,Y] :
( member(V,Y)
| ! [U,X] : ~ member(ordered_pair(U,V),cross_product(X,Y)) ),
inference(miniscoping,[status(thm)],[f15]) ).
fof(f115,plain,
! [X0,X1,X2,X3] :
( member(X1,X3)
| ~ member(ordered_pair(X0,X1),cross_product(X2,X3)) ),
inference(cnf_transformation,[status(thm)],[f114]) ).
fof(f116,plain,
! [X0,X1,X2,X3] :
( member(ordered_pair(X0,X2),cross_product(X1,X3))
| ~ member(X2,X3)
| ~ member(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f16]) ).
fof(f119,plain,
subclass(element_relation,cross_product(universal_class,universal_class)),
inference(cnf_transformation,[status(thm)],[f18]) ).
fof(f120,plain,
! [X0,X1] :
( member(X0,X1)
| ~ member(ordered_pair(X0,X1),element_relation) ),
inference(cnf_transformation,[status(thm)],[f19]) ).
fof(f122,plain,
! [Z,X] :
( member(Z,X)
| ! [Y] : ~ member(Z,intersection(X,Y)) ),
inference(miniscoping,[status(thm)],[f21]) ).
fof(f123,plain,
! [X0,X1,X2] :
( member(X0,X1)
| ~ member(X0,intersection(X1,X2)) ),
inference(cnf_transformation,[status(thm)],[f122]) ).
fof(f124,plain,
! [Z,Y] :
( member(Z,Y)
| ! [X] : ~ member(Z,intersection(X,Y)) ),
inference(miniscoping,[status(thm)],[f22]) ).
fof(f125,plain,
! [X0,X1,X2] :
( member(X0,X2)
| ~ member(X0,intersection(X1,X2)) ),
inference(cnf_transformation,[status(thm)],[f124]) ).
fof(f126,plain,
! [X0,X1,X2] :
( member(X0,intersection(X1,X2))
| ~ member(X0,X2)
| ~ member(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f23]) ).
fof(f127,plain,
! [X0,X1] :
( ~ member(X0,X1)
| ~ member(X0,complement(X1)) ),
inference(cnf_transformation,[status(thm)],[f24]) ).
fof(f128,plain,
! [X0,X1] :
( member(X0,X1)
| member(X0,complement(X1))
| ~ member(X0,universal_class) ),
inference(cnf_transformation,[status(thm)],[f25]) ).
fof(f129,plain,
! [X0,X1] : complement(intersection(complement(X0),complement(X1))) = union(X0,X1),
inference(cnf_transformation,[status(thm)],[f26]) ).
fof(f130,plain,
! [X0,X1] : intersection(complement(intersection(X0,X1)),complement(intersection(complement(X0),complement(X1)))) = symmetric_difference(X0,X1),
inference(cnf_transformation,[status(thm)],[f27]) ).
fof(f131,plain,
! [X0,X1,X2] : intersection(X0,cross_product(X1,X2)) = restrict(X0,X1,X2),
inference(cnf_transformation,[status(thm)],[f28]) ).
fof(f132,plain,
! [X0,X1,X2] : intersection(cross_product(X0,X1),X2) = restrict(X2,X0,X1),
inference(cnf_transformation,[status(thm)],[f29]) ).
fof(f133,plain,
! [X0,X1] :
( ~ member(X1,domain_of(X0))
| restrict(X0,singleton(X1),universal_class) != null_class ),
inference(cnf_transformation,[status(thm)],[f30]) ).
fof(f134,plain,
! [X0,X1] :
( member(X0,domain_of(X1))
| restrict(X1,singleton(X0),universal_class) = null_class
| ~ member(X0,universal_class) ),
inference(cnf_transformation,[status(thm)],[f31]) ).
fof(f150,plain,
! [X0] :
( member(null_class,X0)
| ~ inductive(X0) ),
inference(cnf_transformation,[status(thm)],[f47]) ).
fof(f152,plain,
! [X0] :
( inductive(X0)
| ~ subclass(image(successor_relation,X0),X0)
| ~ member(null_class,X0) ),
inference(cnf_transformation,[status(thm)],[f49]) ).
fof(f153,plain,
inductive(omega),
inference(cnf_transformation,[status(thm)],[f50]) ).
fof(f154,plain,
! [X0] :
( subclass(omega,X0)
| ~ inductive(X0) ),
inference(cnf_transformation,[status(thm)],[f51]) ).
fof(f155,plain,
member(omega,universal_class),
inference(cnf_transformation,[status(thm)],[f52]) ).
fof(f158,plain,
! [X0] : complement(image(element_relation,complement(X0))) = power_class(X0),
inference(cnf_transformation,[status(thm)],[f55]) ).
fof(f162,plain,
! [X0,X1,X2,X3] :
( member(ordered_pair(X3,X0),compose(X1,X2))
| ~ member(ordered_pair(X3,X0),cross_product(universal_class,universal_class))
| ~ member(X0,image(X1,image(X2,singleton(X3)))) ),
inference(cnf_transformation,[status(thm)],[f59]) ).
fof(f169,plain,
! [X0] :
( member(regular(X0),X0)
| X0 = null_class ),
inference(cnf_transformation,[status(thm)],[f66]) ).
fof(f170,plain,
! [X0] :
( intersection(X0,regular(X0)) = null_class
| X0 = null_class ),
inference(cnf_transformation,[status(thm)],[f67]) ).
fof(f172,plain,
function(choice),
inference(cnf_transformation,[status(thm)],[f69]) ).
fof(f173,plain,
! [X0] :
( member(apply(choice,X0),X0)
| X0 = null_class
| ~ member(X0,universal_class) ),
inference(cnf_transformation,[status(thm)],[f70]) ).
fof(f177,plain,
intersection(cross_product(universal_class,universal_class),intersection(cross_product(universal_class,universal_class),complement(compose(complement(element_relation),inverse(element_relation))))) = subset_relation,
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f179,plain,
! [X0] : complement(domain_of(intersection(X0,identity_relation))) = diagonalise(X0),
inference(cnf_transformation,[status(thm)],[f76]) ).
fof(f180,plain,
! [X0] : intersection(domain_of(X0),diagonalise(compose(inverse(element_relation),X0))) = cantor(X0),
inference(cnf_transformation,[status(thm)],[f77]) ).
fof(f200,plain,
ordered_pair(w,x) = ordered_pair(y,z),
inference(cnf_transformation,[status(thm)],[f92]) ).
fof(f201,plain,
member(x,universal_class),
inference(cnf_transformation,[status(thm)],[f93]) ).
fof(f202,plain,
x != z,
inference(cnf_transformation,[status(thm)],[f94]) ).
fof(f207,plain,
! [X0,X1] :
( member(X0,universal_class)
| ~ member(X0,X1) ),
inference(resolution,[status(thm)],[f99,f96]) ).
fof(f208,plain,
! [X0] : member(singleton(X0),universal_class),
inference(paramodulation,[status(thm)],[f110,f109]) ).
fof(f211,plain,
! [X0,X1] :
( member(X1,X0)
| ~ member(X1,omega)
| ~ inductive(X0) ),
inference(resolution,[status(thm)],[f154,f96]) ).
fof(f212,plain,
! [X0] :
( X0 = null_class
| member(regular(X0),universal_class) ),
inference(resolution,[status(thm)],[f207,f169]) ).
fof(f213,plain,
! [X0] :
( ~ inductive(X0)
| member(null_class,universal_class) ),
inference(resolution,[status(thm)],[f207,f150]) ).
fof(f219,definition,
( sQ0_spl
<=> member(null_class,universal_class) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f222,definition,
! [X0] :
( sQ1_spl
<=> ~ inductive(X0) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f223,plain,
! [X0] :
( ~ sQ1_spl
| ~ inductive(X0) ),
inference(component_clause,[status(thm)],[f222]) ).
fof(f225,plain,
( sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f213,f219,f222]) ).
fof(f227,plain,
! [X0] :
( ~ inductive(X0)
| X0 = omega
| ~ subclass(X0,omega) ),
inference(resolution,[status(thm)],[f102,f154]) ).
fof(f233,plain,
! [X0] :
( member(X0,cross_product(universal_class,universal_class))
| ~ member(X0,element_relation) ),
inference(resolution,[status(thm)],[f119,f96]) ).
fof(f241,plain,
! [X0] :
( complement(X0) = null_class
| ~ member(regular(complement(X0)),X0) ),
inference(resolution,[status(thm)],[f127,f169]) ).
fof(f242,plain,
! [X0] :
( ~ inductive(complement(X0))
| ~ member(null_class,X0) ),
inference(resolution,[status(thm)],[f127,f150]) ).
fof(f256,plain,
! [X0,X1] :
( X0 = X1
| X0 = X1
| ~ member(X0,singleton(X1)) ),
inference(paramodulation,[status(thm)],[f110,f104]) ).
fof(f257,plain,
! [X0,X1] :
( X0 = X1
| ~ member(X0,singleton(X1)) ),
inference(duplicate_literals_removal,[status(thm)],[f256]) ).
fof(f260,plain,
! [X0] :
( member(X0,singleton(X0))
| ~ member(X0,universal_class) ),
inference(paramodulation,[status(thm)],[f110,f106]) ).
fof(f263,plain,
! [X0] :
( member(X0,singleton(X0))
| ~ member(X0,universal_class) ),
inference(paramodulation,[status(thm)],[f110,f108]) ).
fof(f264,plain,
! [X0] :
( singleton(X0) = null_class
| regular(singleton(X0)) = X0 ),
inference(resolution,[status(thm)],[f257,f169]) ).
fof(f265,plain,
! [X0] :
( ~ inductive(singleton(X0))
| null_class = X0 ),
inference(resolution,[status(thm)],[f257,f150]) ).
fof(f268,plain,
! [X0] : unordered_pair(singleton(singleton(X0)),singleton(singleton(X0))) = ordered_pair(singleton(X0),X0),
inference(paramodulation,[status(thm)],[f110,f111]) ).
fof(f269,plain,
! [X0,X1] :
( member(unordered_pair(X0,singleton(X1)),ordered_pair(X0,X1))
| ~ member(unordered_pair(X0,singleton(X1)),universal_class) ),
inference(paramodulation,[status(thm)],[f111,f108]) ).
fof(f270,plain,
! [X0,X1] :
( member(singleton(X0),ordered_pair(X0,X1))
| ~ member(singleton(X0),universal_class) ),
inference(paramodulation,[status(thm)],[f111,f106]) ).
fof(f271,plain,
! [X0,X1,X2] :
( X0 = unordered_pair(X1,singleton(X2))
| X0 = singleton(X1)
| ~ member(X0,ordered_pair(X1,X2)) ),
inference(paramodulation,[status(thm)],[f111,f104]) ).
fof(f272,plain,
! [X0,X1] : member(ordered_pair(X0,X1),universal_class),
inference(paramodulation,[status(thm)],[f111,f109]) ).
fof(f273,plain,
! [X0] : singleton(singleton(singleton(X0))) = ordered_pair(singleton(X0),X0),
inference(forward_demodulation,[status(thm)],[f110,f268]) ).
fof(f274,plain,
! [X0,X1] : member(unordered_pair(X0,singleton(X1)),ordered_pair(X0,X1)),
inference(forward_subsumption_resolution,[status(thm)],[f269,f109]) ).
fof(f275,plain,
! [X0,X1] : member(singleton(X0),ordered_pair(X0,X1)),
inference(forward_subsumption_resolution,[status(thm)],[f270,f208]) ).
fof(f279,plain,
member(singleton(w),ordered_pair(y,z)),
inference(paramodulation,[status(thm)],[f200,f275]) ).
fof(f282,plain,
! [X0] :
( ~ inductive(X0)
| ~ inductive(complement(X0)) ),
inference(resolution,[status(thm)],[f242,f150]) ).
fof(f283,plain,
! [X0] :
( ~ member(null_class,universal_class)
| ~ inductive(complement(unordered_pair(X0,null_class))) ),
inference(resolution,[status(thm)],[f242,f108]) ).
fof(f284,plain,
! [X0] :
( ~ member(null_class,universal_class)
| ~ inductive(complement(unordered_pair(null_class,X0))) ),
inference(resolution,[status(thm)],[f242,f106]) ).
fof(f285,definition,
! [X0] :
( sQ6_spl
<=> ~ inductive(complement(unordered_pair(X0,null_class))) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f288,plain,
( ~ sQ0_spl
| sQ6_spl ),
inference(split_clause,[status(thm)],[f283,f285,f219]) ).
fof(f289,definition,
! [X0] :
( sQ7_spl
<=> ~ inductive(complement(unordered_pair(null_class,X0))) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f292,plain,
( ~ sQ0_spl
| sQ7_spl ),
inference(split_clause,[status(thm)],[f284,f289,f219]) ).
fof(f295,plain,
! [X0,X1] :
( member(w,X0)
| ~ member(ordered_pair(y,z),cross_product(X0,X1)) ),
inference(paramodulation,[status(thm)],[f200,f113]) ).
fof(f296,plain,
! [X0,X1] :
( intersection(X0,X1) = null_class
| member(regular(intersection(X0,X1)),X0) ),
inference(resolution,[status(thm)],[f123,f169]) ).
fof(f297,plain,
! [X0,X1] :
( ~ inductive(intersection(X0,X1))
| member(null_class,X0) ),
inference(resolution,[status(thm)],[f123,f150]) ).
fof(f298,plain,
! [X0,X1,X2] :
( subclass(intersection(X0,X1),X2)
| member(not_subclass_element(intersection(X0,X1),X2),X0) ),
inference(resolution,[status(thm)],[f123,f97]) ).
fof(f300,plain,
! [X0,X1] :
( intersection(X0,X1) = null_class
| member(regular(intersection(X0,X1)),X1) ),
inference(resolution,[status(thm)],[f125,f169]) ).
fof(f302,plain,
! [X0,X1,X2] :
( subclass(intersection(X0,X1),X2)
| member(not_subclass_element(intersection(X0,X1),X2),X1) ),
inference(resolution,[status(thm)],[f125,f97]) ).
fof(f331,plain,
( ~ inductive(omega)
| ~ inductive(omega)
| omega = omega ),
inference(resolution,[status(thm)],[f227,f154]) ).
fof(f339,definition,
( sQ14_spl
<=> inductive(omega) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f341,plain,
( sQ14_spl
| ~ inductive(omega) ),
inference(component_clause,[status(thm)],[f339]) ).
fof(f343,definition,
( sQ15_spl
<=> omega = omega ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f346,plain,
( ~ sQ14_spl
| sQ15_spl ),
inference(split_clause,[status(thm)],[f331,f343,f339]) ).
fof(f348,plain,
( sQ14_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f341,f153]) ).
fof(f349,plain,
sQ14_spl,
inference(contradiction_clause,[status(thm)],[f348]) ).
fof(f355,plain,
( ~ inductive(complement(singleton(null_class)))
| ~ member(null_class,universal_class) ),
inference(resolution,[status(thm)],[f260,f242]) ).
fof(f358,definition,
( sQ17_spl
<=> inductive(complement(singleton(null_class))) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f361,plain,
( ~ sQ17_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f355,f219,f358]) ).
fof(f363,plain,
! [X0,X1] :
( member(x,X1)
| ~ member(ordered_pair(y,z),cross_product(X0,X1)) ),
inference(paramodulation,[status(thm)],[f200,f115]) ).
fof(f364,plain,
! [X0,X1] :
( member(w,X0)
| ~ member(z,X1)
| ~ member(y,X0) ),
inference(resolution,[status(thm)],[f116,f295]) ).
fof(f365,plain,
! [X0,X1,X2,X3] :
( member(X2,X3)
| ~ member(X2,X3)
| ~ member(X0,X1) ),
inference(resolution,[status(thm)],[f116,f115]) ).
fof(f368,plain,
! [X0,X1] :
( member(ordered_pair(y,z),cross_product(X0,X1))
| ~ member(x,X1)
| ~ member(w,X0) ),
inference(paramodulation,[status(thm)],[f200,f116]) ).
fof(f369,definition,
! [X0] :
( sQ18_spl
<=> ( member(w,X0)
| ~ member(y,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f370,plain,
! [X0] :
( ~ sQ18_spl
| member(w,X0)
| ~ member(y,X0) ),
inference(component_clause,[status(thm)],[f369]) ).
fof(f372,definition,
! [X1] :
( sQ19_spl
<=> ~ member(z,X1) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f373,plain,
! [X0] :
( ~ sQ19_spl
| ~ member(z,X0) ),
inference(component_clause,[status(thm)],[f372]) ).
fof(f375,plain,
( sQ19_spl
| sQ18_spl ),
inference(split_clause,[status(thm)],[f364,f369,f372]) ).
fof(f376,definition,
! [X0,X1] :
( sQ20_spl
<=> ~ member(X0,X1) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f377,plain,
! [X0,X1] :
( ~ sQ20_spl
| ~ member(X0,X1) ),
inference(component_clause,[status(thm)],[f376]) ).
fof(f379,definition,
! [X2,X3] :
( sQ21_spl
<=> ( member(X2,X3)
| ~ member(X2,X3) ) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f382,plain,
( sQ21_spl
| sQ20_spl ),
inference(split_clause,[status(thm)],[f365,f376,f379]) ).
fof(f384,plain,
( ~ sQ18_spl
| ~ member(y,universal_class)
| member(w,singleton(y)) ),
inference(resolution,[status(thm)],[f370,f260]) ).
fof(f387,definition,
( sQ22_spl
<=> member(w,singleton(y)) ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f388,plain,
( ~ sQ22_spl
| member(w,singleton(y)) ),
inference(component_clause,[status(thm)],[f387]) ).
fof(f390,definition,
( sQ23_spl
<=> member(y,universal_class) ),
introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition]) ).
fof(f391,plain,
( ~ sQ23_spl
| member(y,universal_class) ),
inference(component_clause,[status(thm)],[f390]) ).
fof(f393,plain,
( ~ sQ18_spl
| ~ sQ23_spl
| sQ22_spl ),
inference(split_clause,[status(thm)],[f384,f387,f390,f369]) ).
fof(f394,definition,
! [X0] :
( sQ24_spl
<=> member(w,unordered_pair(X0,y)) ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f395,plain,
! [X0] :
( ~ sQ24_spl
| member(w,unordered_pair(X0,y)) ),
inference(component_clause,[status(thm)],[f394]) ).
fof(f398,definition,
! [X0] :
( sQ25_spl
<=> member(w,unordered_pair(y,X0)) ),
introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition]) ).
fof(f399,plain,
! [X0] :
( ~ sQ25_spl
| member(w,unordered_pair(y,X0)) ),
inference(component_clause,[status(thm)],[f398]) ).
fof(f402,plain,
! [X0,X1] :
( ~ member(z,X0)
| ~ member(y,X1)
| member(x,X0) ),
inference(resolution,[status(thm)],[f363,f116]) ).
fof(f403,definition,
! [X0] :
( sQ26_spl
<=> ( ~ member(z,X0)
| member(x,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition]) ).
fof(f404,plain,
! [X0] :
( ~ sQ26_spl
| ~ member(z,X0)
| member(x,X0) ),
inference(component_clause,[status(thm)],[f403]) ).
fof(f406,definition,
! [X1] :
( sQ27_spl
<=> ~ member(y,X1) ),
introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition]) ).
fof(f407,plain,
! [X0] :
( ~ sQ27_spl
| ~ member(y,X0) ),
inference(component_clause,[status(thm)],[f406]) ).
fof(f409,plain,
( sQ27_spl
| sQ26_spl ),
inference(split_clause,[status(thm)],[f402,f403,f406]) ).
fof(f411,plain,
! [X0] :
( ~ sQ26_spl
| ~ member(z,universal_class)
| member(x,unordered_pair(X0,z)) ),
inference(resolution,[status(thm)],[f404,f108]) ).
fof(f413,definition,
( sQ28_spl
<=> member(x,singleton(z)) ),
introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition]) ).
fof(f414,plain,
( ~ sQ28_spl
| member(x,singleton(z)) ),
inference(component_clause,[status(thm)],[f413]) ).
fof(f416,definition,
( sQ29_spl
<=> member(z,universal_class) ),
introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition]) ).
fof(f420,definition,
! [X0] :
( sQ30_spl
<=> member(x,unordered_pair(X0,z)) ),
introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition]) ).
fof(f421,plain,
! [X0] :
( ~ sQ30_spl
| member(x,unordered_pair(X0,z)) ),
inference(component_clause,[status(thm)],[f420]) ).
fof(f423,plain,
( ~ sQ26_spl
| ~ sQ29_spl
| sQ30_spl ),
inference(split_clause,[status(thm)],[f411,f420,f416,f403]) ).
fof(f424,definition,
! [X0] :
( sQ31_spl
<=> member(x,unordered_pair(z,X0)) ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f425,plain,
! [X0] :
( ~ sQ31_spl
| member(x,unordered_pair(z,X0)) ),
inference(component_clause,[status(thm)],[f424]) ).
fof(f429,plain,
! [X0,X1] :
( member(w,X0)
| ~ member(x,X1)
| ~ member(w,X0) ),
inference(resolution,[status(thm)],[f368,f295]) ).
fof(f430,plain,
! [X0,X1] :
( member(z,X1)
| ~ member(x,X1)
| ~ member(w,X0) ),
inference(resolution,[status(thm)],[f368,f115]) ).
fof(f431,plain,
! [X0,X1] :
( member(y,X0)
| ~ member(x,X1)
| ~ member(w,X0) ),
inference(resolution,[status(thm)],[f368,f113]) ).
fof(f433,definition,
! [X0] :
( sQ32_spl
<=> ~ member(w,X0) ),
introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition]) ).
fof(f434,plain,
! [X0] :
( ~ sQ32_spl
| ~ member(w,X0) ),
inference(component_clause,[status(thm)],[f433]) ).
fof(f440,definition,
! [X0] :
( sQ34_spl
<=> ( member(w,X0)
| ~ member(w,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f443,definition,
! [X1] :
( sQ35_spl
<=> ~ member(x,X1) ),
introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition]) ).
fof(f444,plain,
! [X0] :
( ~ sQ35_spl
| ~ member(x,X0) ),
inference(component_clause,[status(thm)],[f443]) ).
fof(f446,plain,
( sQ35_spl
| sQ34_spl ),
inference(split_clause,[status(thm)],[f429,f440,f443]) ).
fof(f447,definition,
! [X1] :
( sQ36_spl
<=> ( member(z,X1)
| ~ member(x,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition]) ).
fof(f448,plain,
! [X0] :
( ~ sQ36_spl
| member(z,X0)
| ~ member(x,X0) ),
inference(component_clause,[status(thm)],[f447]) ).
fof(f450,plain,
( sQ36_spl
| sQ32_spl ),
inference(split_clause,[status(thm)],[f430,f433,f447]) ).
fof(f451,definition,
! [X0] :
( sQ37_spl
<=> ( member(y,X0)
| ~ member(w,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition]) ).
fof(f454,plain,
( sQ35_spl
| sQ37_spl ),
inference(split_clause,[status(thm)],[f431,f451,f443]) ).
fof(f455,definition,
( sQ38_spl
<=> member(ordered_pair(y,z),universal_class) ),
introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition]) ).
fof(f457,plain,
( sQ38_spl
| ~ member(ordered_pair(y,z),universal_class) ),
inference(component_clause,[status(thm)],[f455]) ).
fof(f461,plain,
( ~ sQ35_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f201,f444]) ).
fof(f465,plain,
~ sQ35_spl,
inference(contradiction_clause,[status(thm)],[f461]) ).
fof(f483,plain,
( member(w,x)
| ~ member(ordered_pair(y,z),element_relation) ),
inference(paramodulation,[status(thm)],[f200,f120]) ).
fof(f484,definition,
( sQ39_spl
<=> member(ordered_pair(y,z),element_relation) ),
introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition]) ).
fof(f486,plain,
( sQ39_spl
| ~ member(ordered_pair(y,z),element_relation) ),
inference(component_clause,[status(thm)],[f484]) ).
fof(f487,definition,
( sQ40_spl
<=> member(w,x) ),
introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition]) ).
fof(f488,plain,
( ~ sQ40_spl
| member(w,x) ),
inference(component_clause,[status(thm)],[f487]) ).
fof(f490,plain,
( sQ40_spl
| ~ sQ39_spl ),
inference(split_clause,[status(thm)],[f483,f484,f487]) ).
fof(f491,plain,
( ~ sQ20_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f201,f377]) ).
fof(f504,plain,
~ sQ20_spl,
inference(contradiction_clause,[status(thm)],[f491]) ).
fof(f510,definition,
( sQ42_spl
<=> member(ordered_pair(w,x),element_relation) ),
introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition]) ).
fof(f511,plain,
( ~ sQ42_spl
| member(ordered_pair(w,x),element_relation) ),
inference(component_clause,[status(thm)],[f510]) ).
fof(f514,plain,
( ~ sQ42_spl
| member(ordered_pair(y,z),element_relation) ),
inference(forward_demodulation,[status(thm)],[f200,f511]) ).
fof(f518,plain,
! [X0,X1] :
( X1 = null_class
| member(X0,null_class)
| ~ member(X0,regular(X1))
| ~ member(X0,X1) ),
inference(paramodulation,[status(thm)],[f170,f126]) ).
fof(f522,plain,
! [X0] :
( ~ sQ32_spl
| member(w,X0)
| ~ member(w,universal_class) ),
inference(resolution,[status(thm)],[f128,f434]) ).
fof(f527,definition,
( sQ44_spl
<=> member(w,universal_class) ),
introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition]) ).
fof(f529,plain,
( sQ44_spl
| ~ member(w,universal_class) ),
inference(component_clause,[status(thm)],[f527]) ).
fof(f530,definition,
! [X0] :
( sQ45_spl
<=> member(w,X0) ),
introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition]) ).
fof(f531,plain,
! [X0] :
( ~ sQ45_spl
| member(w,X0) ),
inference(component_clause,[status(thm)],[f530]) ).
fof(f533,plain,
( ~ sQ32_spl
| sQ45_spl
| ~ sQ44_spl ),
inference(split_clause,[status(thm)],[f522,f527,f530,f433]) ).
fof(f534,plain,
( ~ sQ45_spl
| ~ sQ32_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f531,f434]) ).
fof(f535,plain,
( ~ sQ45_spl
| ~ sQ32_spl ),
inference(contradiction_clause,[status(thm)],[f534]) ).
fof(f538,plain,
! [X0] :
( ~ sQ19_spl
| member(z,X0)
| ~ member(z,universal_class) ),
inference(resolution,[status(thm)],[f373,f128]) ).
fof(f540,definition,
! [X0] :
( sQ46_spl
<=> member(z,X0) ),
introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition]) ).
fof(f541,plain,
! [X0] :
( ~ sQ46_spl
| member(z,X0) ),
inference(component_clause,[status(thm)],[f540]) ).
fof(f543,plain,
( ~ sQ19_spl
| sQ46_spl
| ~ sQ29_spl ),
inference(split_clause,[status(thm)],[f538,f416,f540,f372]) ).
fof(f551,plain,
( ~ sQ42_spl
| sQ39_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f514,f486]) ).
fof(f552,plain,
( ~ sQ42_spl
| sQ39_spl ),
inference(contradiction_clause,[status(thm)],[f551]) ).
fof(f553,plain,
( ~ sQ40_spl
| ~ sQ32_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f488,f434]) ).
fof(f554,plain,
( ~ sQ40_spl
| ~ sQ32_spl ),
inference(contradiction_clause,[status(thm)],[f553]) ).
fof(f574,plain,
! [X0] :
( regular(singleton(X0)) = X0
| singleton(X0) = null_class ),
inference(resolution,[status(thm)],[f169,f257]) ).
fof(f578,plain,
! [X0,X1,X2] :
( member(X0,intersection(complement(X1),complement(X2)))
| member(X0,union(X1,X2))
| ~ member(X0,universal_class) ),
inference(paramodulation,[status(thm)],[f129,f128]) ).
fof(f580,plain,
! [X0,X1] : intersection(complement(intersection(X0,X1)),union(X0,X1)) = symmetric_difference(X0,X1),
inference(forward_demodulation,[status(thm)],[f129,f130]) ).
fof(f584,plain,
! [X0] :
( X0 = null_class
| intersection(complement(null_class),union(X0,regular(X0))) = symmetric_difference(X0,regular(X0)) ),
inference(paramodulation,[status(thm)],[f170,f580]) ).
fof(f589,plain,
! [X0] :
( complement(X0) = null_class
| ~ member(regular(complement(X0)),X0) ),
inference(resolution,[status(thm)],[f127,f169]) ).
fof(f595,plain,
! [X0] :
( member(null_class,X0)
| ~ member(null_class,universal_class)
| ~ inductive(complement(complement(X0))) ),
inference(resolution,[status(thm)],[f242,f128]) ).
fof(f597,definition,
! [X0] :
( sQ47_spl
<=> ( member(null_class,X0)
| ~ inductive(complement(complement(X0))) ) ),
introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition]) ).
fof(f600,plain,
( ~ sQ0_spl
| sQ47_spl ),
inference(split_clause,[status(thm)],[f595,f597,f219]) ).
fof(f601,plain,
( ~ sQ1_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f153,f223]) ).
fof(f602,plain,
~ sQ1_spl,
inference(contradiction_clause,[status(thm)],[f601]) ).
fof(f613,plain,
! [X0,X1] :
( cross_product(X0,X1) = null_class
| null_class = restrict(regular(cross_product(X0,X1)),X0,X1) ),
inference(paramodulation,[status(thm)],[f170,f132]) ).
fof(f638,plain,
! [X0] :
( singleton(X0) = null_class
| singleton(X0) = null_class
| member(X0,universal_class) ),
inference(paramodulation,[status(thm)],[f264,f212]) ).
fof(f639,plain,
! [X0] :
( singleton(X0) = null_class
| member(X0,singleton(X0))
| singleton(X0) = null_class ),
inference(paramodulation,[status(thm)],[f264,f169]) ).
fof(f641,plain,
! [X0] :
( singleton(X0) = null_class
| member(X0,universal_class) ),
inference(duplicate_literals_removal,[status(thm)],[f638]) ).
fof(f642,plain,
! [X0] :
( member(X0,singleton(X0))
| singleton(X0) = null_class ),
inference(duplicate_literals_removal,[status(thm)],[f639]) ).
fof(f645,plain,
( member(w,universal_class)
| member(null_class,ordered_pair(y,z)) ),
inference(paramodulation,[status(thm)],[f641,f279]) ).
fof(f661,definition,
( sQ49_spl
<=> member(null_class,ordered_pair(y,z)) ),
introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition]) ).
fof(f662,plain,
( ~ sQ49_spl
| member(null_class,ordered_pair(y,z)) ),
inference(component_clause,[status(thm)],[f661]) ).
fof(f664,plain,
( sQ44_spl
| sQ49_spl ),
inference(split_clause,[status(thm)],[f645,f661,f527]) ).
fof(f668,definition,
( sQ51_spl
<=> inductive(null_class) ),
introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition]) ).
fof(f670,plain,
( sQ51_spl
| ~ inductive(null_class) ),
inference(component_clause,[status(thm)],[f668]) ).
fof(f672,definition,
! [X0] :
( sQ52_spl
<=> member(X0,universal_class) ),
introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition]) ).
fof(f673,plain,
! [X0] :
( ~ sQ52_spl
| member(X0,universal_class) ),
inference(component_clause,[status(thm)],[f672]) ).
fof(f684,definition,
( sQ53_spl
<=> null_class = null_class ),
introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition]) ).
fof(f687,definition,
( sQ54_spl
<=> inductive(complement(universal_class)) ),
introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition]) ).
fof(f710,definition,
! [X0] :
( sQ57_spl
<=> X0 = null_class ),
introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition]) ).
fof(f711,plain,
! [X0] :
( ~ sQ57_spl
| X0 = null_class ),
inference(component_clause,[status(thm)],[f710]) ).
fof(f716,plain,
! [X0] :
( ~ sQ57_spl
| sQ51_spl
| ~ inductive(X0) ),
inference(paramodulation,[status(thm)],[f711,f670]) ).
fof(f724,plain,
( ~ sQ57_spl
| sQ51_spl
| sQ1_spl ),
inference(split_clause,[status(thm)],[f716,f222,f668,f710]) ).
fof(f777,plain,
( ~ sQ49_spl
| member(null_class,universal_class) ),
inference(resolution,[status(thm)],[f662,f207]) ).
fof(f834,plain,
! [X0,X1] :
( member(not_subclass_element(X0,complement(X1)),X1)
| ~ member(not_subclass_element(X0,complement(X1)),universal_class)
| subclass(X0,complement(X1)) ),
inference(resolution,[status(thm)],[f98,f128]) ).
fof(f850,plain,
! [X0,X1] :
( unordered_pair(X0,X1) = null_class
| regular(unordered_pair(X0,X1)) = X1
| regular(unordered_pair(X0,X1)) = X0 ),
inference(resolution,[status(thm)],[f104,f169]) ).
fof(f885,plain,
( ~ sQ32_spl
| singleton(w) = null_class ),
inference(resolution,[status(thm)],[f642,f434]) ).
fof(f886,plain,
( ~ sQ27_spl
| singleton(y) = null_class ),
inference(resolution,[status(thm)],[f642,f407]) ).
fof(f887,plain,
( ~ sQ19_spl
| singleton(z) = null_class ),
inference(resolution,[status(thm)],[f642,f373]) ).
fof(f891,definition,
( sQ60_spl
<=> singleton(null_class) = null_class ),
introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition]) ).
fof(f892,plain,
( ~ sQ60_spl
| singleton(null_class) = null_class ),
inference(component_clause,[status(thm)],[f891]) ).
fof(f893,plain,
( sQ60_spl
| singleton(null_class) != null_class ),
inference(component_clause,[status(thm)],[f891]) ).
fof(f897,plain,
( ~ sQ32_spl
| member(w,null_class)
| singleton(w) = null_class ),
inference(paramodulation,[status(thm)],[f885,f642]) ).
fof(f904,plain,
! [X0] :
( ~ sQ32_spl
| member(null_class,ordered_pair(w,X0)) ),
inference(paramodulation,[status(thm)],[f885,f275]) ).
fof(f905,plain,
! [X0] :
( ~ sQ32_spl
| X0 = w
| ~ member(X0,null_class) ),
inference(paramodulation,[status(thm)],[f885,f257]) ).
fof(f907,plain,
! [X0] :
( ~ sQ32_spl
| unordered_pair(singleton(X0),unordered_pair(X0,null_class)) = ordered_pair(X0,w) ),
inference(paramodulation,[status(thm)],[f885,f111]) ).
fof(f911,definition,
( sQ61_spl
<=> singleton(w) = null_class ),
introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition]) ).
fof(f914,definition,
( sQ62_spl
<=> member(w,null_class) ),
introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition]) ).
fof(f915,plain,
( ~ sQ62_spl
| member(w,null_class) ),
inference(component_clause,[status(thm)],[f914]) ).
fof(f917,plain,
( ~ sQ32_spl
| sQ62_spl
| sQ61_spl ),
inference(split_clause,[status(thm)],[f897,f911,f914,f433]) ).
fof(f923,definition,
( sQ64_spl
<=> null_class = w ),
introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition]) ).
fof(f924,plain,
( ~ sQ64_spl
| null_class = w ),
inference(component_clause,[status(thm)],[f923]) ).
fof(f935,plain,
( ~ sQ27_spl
| member(y,null_class)
| ~ member(y,universal_class) ),
inference(paramodulation,[status(thm)],[f886,f263]) ).
fof(f937,plain,
! [X0] :
( ~ sQ27_spl
| X0 = y
| ~ member(X0,null_class) ),
inference(paramodulation,[status(thm)],[f886,f257]) ).
fof(f943,definition,
( sQ65_spl
<=> singleton(y) = null_class ),
introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition]) ).
fof(f944,plain,
( ~ sQ65_spl
| singleton(y) = null_class ),
inference(component_clause,[status(thm)],[f943]) ).
fof(f946,definition,
( sQ66_spl
<=> member(y,null_class) ),
introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition]) ).
fof(f947,plain,
( ~ sQ66_spl
| member(y,null_class) ),
inference(component_clause,[status(thm)],[f946]) ).
fof(f959,plain,
( ~ sQ27_spl
| sQ66_spl
| ~ sQ23_spl ),
inference(split_clause,[status(thm)],[f935,f390,f946,f406]) ).
fof(f969,plain,
! [X0] :
( ~ sQ19_spl
| X0 = z
| ~ member(X0,null_class) ),
inference(paramodulation,[status(thm)],[f887,f257]) ).
fof(f975,definition,
( sQ69_spl
<=> singleton(z) = null_class ),
introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition]) ).
fof(f976,plain,
( ~ sQ69_spl
| singleton(z) = null_class ),
inference(component_clause,[status(thm)],[f975]) ).
fof(f978,definition,
( sQ70_spl
<=> member(z,null_class) ),
introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition]) ).
fof(f979,plain,
( ~ sQ70_spl
| member(z,null_class) ),
inference(component_clause,[status(thm)],[f978]) ).
fof(f992,plain,
! [X0] :
( ~ sQ32_spl
| subclass(null_class,X0)
| not_subclass_element(null_class,X0) = w ),
inference(resolution,[status(thm)],[f905,f97]) ).
fof(f1017,plain,
( inductive(universal_class)
| ~ member(null_class,universal_class) ),
inference(resolution,[status(thm)],[f152,f99]) ).
fof(f1018,definition,
( sQ73_spl
<=> inductive(universal_class) ),
introduced(definition,[new_symbols(definition,[sQ73_spl])],[split_symbol_definition]) ).
fof(f1021,plain,
( sQ73_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f1017,f219,f1018]) ).
fof(f1024,plain,
! [X0] :
( ~ sQ32_spl
| subclass(null_class,X0)
| subclass(null_class,X0)
| member(w,null_class) ),
inference(paramodulation,[status(thm)],[f992,f97]) ).
fof(f1026,definition,
! [X0] :
( sQ74_spl
<=> ( subclass(null_class,X0)
| subclass(null_class,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ74_spl])],[split_symbol_definition]) ).
fof(f1027,plain,
! [X0] :
( ~ sQ74_spl
| subclass(null_class,X0)
| subclass(null_class,X0) ),
inference(component_clause,[status(thm)],[f1026]) ).
fof(f1029,plain,
( ~ sQ32_spl
| sQ74_spl
| sQ62_spl ),
inference(split_clause,[status(thm)],[f1024,f914,f1026,f433]) ).
fof(f1031,plain,
( ~ sQ62_spl
| ~ sQ32_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f915,f434]) ).
fof(f1032,plain,
( ~ sQ62_spl
| ~ sQ32_spl ),
inference(contradiction_clause,[status(thm)],[f1031]) ).
fof(f1033,plain,
! [X0] :
( ~ sQ74_spl
| subclass(null_class,X0) ),
inference(duplicate_literals_removal,[status(thm)],[f1027]) ).
fof(f1036,definition,
( sQ75_spl
<=> null_class = omega ),
introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition]) ).
fof(f1037,plain,
( ~ sQ75_spl
| null_class = omega ),
inference(component_clause,[status(thm)],[f1036]) ).
fof(f1053,plain,
( ~ sQ32_spl
| unordered_pair(singleton(null_class),singleton(null_class)) = ordered_pair(null_class,w) ),
inference(paramodulation,[status(thm)],[f110,f907]) ).
fof(f1056,plain,
( ~ sQ32_spl
| singleton(singleton(null_class)) = ordered_pair(null_class,w) ),
inference(forward_demodulation,[status(thm)],[f110,f1053]) ).
fof(f1057,plain,
( ~ sQ32_spl
| member(singleton(null_class),universal_class)
| null_class = ordered_pair(null_class,w) ),
inference(paramodulation,[status(thm)],[f641,f1056]) ).
fof(f1061,plain,
( ~ sQ32_spl
| regular(ordered_pair(null_class,w)) = singleton(null_class)
| singleton(singleton(null_class)) = null_class ),
inference(paramodulation,[status(thm)],[f1056,f574]) ).
fof(f1065,plain,
( ~ sQ32_spl
| ~ inductive(ordered_pair(null_class,w))
| null_class = singleton(null_class) ),
inference(paramodulation,[status(thm)],[f1056,f265]) ).
fof(f1066,plain,
( ~ sQ32_spl
| member(singleton(null_class),ordered_pair(null_class,w))
| ~ member(singleton(null_class),universal_class) ),
inference(paramodulation,[status(thm)],[f1056,f263]) ).
fof(f1068,plain,
! [X0] :
( ~ sQ32_spl
| X0 = singleton(null_class)
| ~ member(X0,ordered_pair(null_class,w)) ),
inference(paramodulation,[status(thm)],[f1056,f257]) ).
fof(f1073,definition,
( sQ77_spl
<=> null_class = ordered_pair(null_class,w) ),
introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition]) ).
fof(f1074,plain,
( ~ sQ77_spl
| null_class = ordered_pair(null_class,w) ),
inference(component_clause,[status(thm)],[f1073]) ).
fof(f1075,plain,
( sQ77_spl
| null_class != ordered_pair(null_class,w) ),
inference(component_clause,[status(thm)],[f1073]) ).
fof(f1076,definition,
( sQ78_spl
<=> member(singleton(null_class),universal_class) ),
introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition]) ).
fof(f1079,plain,
( ~ sQ32_spl
| sQ78_spl
| sQ77_spl ),
inference(split_clause,[status(thm)],[f1057,f1073,f1076,f433]) ).
fof(f1080,definition,
( sQ79_spl
<=> singleton(null_class) = ordered_pair(null_class,w) ),
introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition]) ).
fof(f1081,plain,
( ~ sQ79_spl
| singleton(null_class) = ordered_pair(null_class,w) ),
inference(component_clause,[status(thm)],[f1080]) ).
fof(f1082,plain,
( sQ79_spl
| singleton(null_class) != ordered_pair(null_class,w) ),
inference(component_clause,[status(thm)],[f1080]) ).
fof(f1084,definition,
( sQ80_spl
<=> singleton(singleton(null_class)) = null_class ),
introduced(definition,[new_symbols(definition,[sQ80_spl])],[split_symbol_definition]) ).
fof(f1085,plain,
( ~ sQ80_spl
| singleton(singleton(null_class)) = null_class ),
inference(component_clause,[status(thm)],[f1084]) ).
fof(f1087,definition,
( sQ81_spl
<=> member(singleton(null_class),ordered_pair(null_class,w)) ),
introduced(definition,[new_symbols(definition,[sQ81_spl])],[split_symbol_definition]) ).
fof(f1091,definition,
( sQ82_spl
<=> regular(ordered_pair(null_class,w)) = singleton(null_class) ),
introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition]) ).
fof(f1092,plain,
( ~ sQ82_spl
| regular(ordered_pair(null_class,w)) = singleton(null_class) ),
inference(component_clause,[status(thm)],[f1091]) ).
fof(f1094,plain,
( ~ sQ32_spl
| sQ82_spl
| sQ80_spl ),
inference(split_clause,[status(thm)],[f1061,f1084,f1091,f433]) ).
fof(f1096,definition,
( sQ83_spl
<=> inductive(ordered_pair(null_class,w)) ),
introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition]) ).
fof(f1099,plain,
( ~ sQ32_spl
| ~ sQ83_spl
| sQ60_spl ),
inference(split_clause,[status(thm)],[f1065,f891,f1096,f433]) ).
fof(f1100,plain,
( ~ sQ32_spl
| sQ81_spl
| ~ sQ78_spl ),
inference(split_clause,[status(thm)],[f1066,f1076,f1087,f433]) ).
fof(f1101,plain,
( ~ sQ80_spl
| ~ sQ32_spl
| ordered_pair(null_class,w) = null_class ),
inference(forward_demodulation,[status(thm)],[f1056,f1085]) ).
fof(f1123,definition,
( sQ87_spl
<=> member(null_class,w) ),
introduced(definition,[new_symbols(definition,[sQ87_spl])],[split_symbol_definition]) ).
fof(f1124,plain,
( ~ sQ87_spl
| member(null_class,w) ),
inference(component_clause,[status(thm)],[f1123]) ).
fof(f1125,plain,
( sQ87_spl
| ~ member(null_class,w) ),
inference(component_clause,[status(thm)],[f1123]) ).
fof(f1126,definition,
( sQ88_spl
<=> member(ordered_pair(null_class,w),element_relation) ),
introduced(definition,[new_symbols(definition,[sQ88_spl])],[split_symbol_definition]) ).
fof(f1127,plain,
( ~ sQ88_spl
| member(ordered_pair(null_class,w),element_relation) ),
inference(component_clause,[status(thm)],[f1126]) ).
fof(f1130,plain,
( ~ sQ70_spl
| ~ sQ19_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f979,f373]) ).
fof(f1131,plain,
( ~ sQ70_spl
| ~ sQ19_spl ),
inference(contradiction_clause,[status(thm)],[f1130]) ).
fof(f1132,plain,
( ~ sQ66_spl
| ~ sQ27_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f947,f407]) ).
fof(f1133,plain,
( ~ sQ66_spl
| ~ sQ27_spl ),
inference(contradiction_clause,[status(thm)],[f1132]) ).
fof(f1146,plain,
( sQ87_spl
| ~ inductive(w) ),
inference(resolution,[status(thm)],[f1125,f150]) ).
fof(f1164,plain,
( ~ sQ60_spl
| member(null_class,null_class)
| ~ member(null_class,universal_class) ),
inference(paramodulation,[status(thm)],[f892,f263]) ).
fof(f1176,definition,
( sQ89_spl
<=> member(null_class,null_class) ),
introduced(definition,[new_symbols(definition,[sQ89_spl])],[split_symbol_definition]) ).
fof(f1177,plain,
( ~ sQ89_spl
| member(null_class,null_class) ),
inference(component_clause,[status(thm)],[f1176]) ).
fof(f1178,plain,
( sQ89_spl
| ~ member(null_class,null_class) ),
inference(component_clause,[status(thm)],[f1176]) ).
fof(f1188,plain,
( ~ sQ60_spl
| sQ89_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f1164,f219,f1176,f891]) ).
fof(f1201,plain,
( ~ sQ32_spl
| ~ sQ89_spl
| null_class = w ),
inference(resolution,[status(thm)],[f1177,f905]) ).
fof(f1255,definition,
( sQ93_spl
<=> member(w,omega) ),
introduced(definition,[new_symbols(definition,[sQ93_spl])],[split_symbol_definition]) ).
fof(f1256,plain,
( ~ sQ93_spl
| member(w,omega) ),
inference(component_clause,[status(thm)],[f1255]) ).
fof(f1261,plain,
( ~ sQ69_spl
| member(z,null_class)
| ~ member(z,universal_class) ),
inference(paramodulation,[status(thm)],[f976,f263]) ).
fof(f1268,plain,
( ~ sQ69_spl
| sQ70_spl
| ~ sQ29_spl ),
inference(split_clause,[status(thm)],[f1261,f416,f978,f975]) ).
fof(f1276,plain,
! [X0,X1] :
( member(X0,image(element_relation,complement(X1)))
| member(X0,power_class(X1))
| ~ member(X0,universal_class) ),
inference(paramodulation,[status(thm)],[f158,f128]) ).
fof(f1278,plain,
( ~ sQ65_spl
| member(y,null_class)
| ~ member(y,universal_class) ),
inference(paramodulation,[status(thm)],[f944,f263]) ).
fof(f1285,plain,
( ~ sQ65_spl
| sQ66_spl
| ~ sQ23_spl ),
inference(split_clause,[status(thm)],[f1278,f390,f946,f943]) ).
fof(f1286,plain,
( ~ sQ93_spl
| member(w,universal_class) ),
inference(resolution,[status(thm)],[f1256,f207]) ).
fof(f1294,plain,
( ~ sQ77_spl
| member(singleton(null_class),null_class) ),
inference(paramodulation,[status(thm)],[f1074,f275]) ).
fof(f1302,definition,
( sQ94_spl
<=> subclass(null_class,null_class) ),
introduced(definition,[new_symbols(definition,[sQ94_spl])],[split_symbol_definition]) ).
fof(f1304,plain,
( sQ94_spl
| ~ subclass(null_class,null_class) ),
inference(component_clause,[status(thm)],[f1302]) ).
fof(f1307,plain,
( ~ sQ36_spl
| ~ member(x,universal_class)
| member(z,singleton(x)) ),
inference(resolution,[status(thm)],[f448,f263]) ).
fof(f1312,definition,
( sQ95_spl
<=> member(z,singleton(x)) ),
introduced(definition,[new_symbols(definition,[sQ95_spl])],[split_symbol_definition]) ).
fof(f1313,plain,
( ~ sQ95_spl
| member(z,singleton(x)) ),
inference(component_clause,[status(thm)],[f1312]) ).
fof(f1314,plain,
( sQ95_spl
| ~ member(z,singleton(x)) ),
inference(component_clause,[status(thm)],[f1312]) ).
fof(f1315,definition,
( sQ96_spl
<=> member(x,universal_class) ),
introduced(definition,[new_symbols(definition,[sQ96_spl])],[split_symbol_definition]) ).
fof(f1317,plain,
( sQ96_spl
| ~ member(x,universal_class) ),
inference(component_clause,[status(thm)],[f1315]) ).
fof(f1318,plain,
( ~ sQ36_spl
| ~ sQ96_spl
| sQ95_spl ),
inference(split_clause,[status(thm)],[f1307,f1312,f1315,f447]) ).
fof(f1323,plain,
( sQ96_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1317,f201]) ).
fof(f1324,plain,
sQ96_spl,
inference(contradiction_clause,[status(thm)],[f1323]) ).
fof(f1348,plain,
( ~ sQ93_spl
| sQ44_spl ),
inference(split_clause,[status(thm)],[f1286,f527,f1255]) ).
fof(f1359,plain,
! [X0] :
( null_class = X0
| ~ inductive(singleton(X0)) ),
inference(resolution,[status(thm)],[f150,f257]) ).
fof(f1369,plain,
! [X0,X1,X2] :
( ~ inductive(image(X1,image(X2,singleton(X0))))
| member(ordered_pair(X0,null_class),compose(X1,X2))
| ~ member(ordered_pair(X0,null_class),cross_product(universal_class,universal_class)) ),
inference(resolution,[status(thm)],[f162,f150]) ).
fof(f1373,plain,
( ~ sQ70_spl
| ~ sQ27_spl
| z = y ),
inference(resolution,[status(thm)],[f937,f979]) ).
fof(f1381,plain,
! [X0] :
( ~ sQ27_spl
| ~ sQ70_spl
| ~ member(z,X0) ),
inference(backward_demodulation,[status(thm)],[f1373,f407]) ).
fof(f1388,plain,
( ~ sQ27_spl
| ~ sQ70_spl
| sQ19_spl ),
inference(split_clause,[status(thm)],[f1381,f372,f978,f406]) ).
fof(f1452,plain,
( ~ sQ95_spl
| z = x ),
inference(resolution,[status(thm)],[f1313,f257]) ).
fof(f1454,plain,
( ~ sQ95_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1452,f202]) ).
fof(f1455,plain,
~ sQ95_spl,
inference(contradiction_clause,[status(thm)],[f1454]) ).
fof(f1472,plain,
( sQ44_spl
| ~ sQ52_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f529,f673]) ).
fof(f1474,plain,
( sQ44_spl
| ~ sQ52_spl ),
inference(contradiction_clause,[status(thm)],[f1472]) ).
fof(f1496,definition,
( sQ101_spl
<=> w = omega ),
introduced(definition,[new_symbols(definition,[sQ101_spl])],[split_symbol_definition]) ).
fof(f1497,plain,
( ~ sQ101_spl
| w = omega ),
inference(component_clause,[status(thm)],[f1496]) ).
fof(f1506,plain,
( ~ sQ101_spl
| inductive(w) ),
inference(backward_demodulation,[status(thm)],[f1497,f153]) ).
fof(f1508,plain,
( ~ sQ101_spl
| sQ87_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1506,f1146]) ).
fof(f1509,plain,
( ~ sQ101_spl
| sQ87_spl ),
inference(contradiction_clause,[status(thm)],[f1508]) ).
fof(f1554,plain,
( ~ sQ28_spl
| ~ sQ19_spl
| member(x,null_class) ),
inference(forward_demodulation,[status(thm)],[f887,f414]) ).
fof(f1555,plain,
( ~ sQ22_spl
| ~ sQ32_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f388,f434]) ).
fof(f1556,plain,
( ~ sQ22_spl
| ~ sQ32_spl ),
inference(contradiction_clause,[status(thm)],[f1555]) ).
fof(f1645,plain,
! [X0,X1] :
( member(apply(choice,intersection(X0,X1)),X0)
| intersection(X0,X1) = null_class
| ~ member(intersection(X0,X1),universal_class) ),
inference(resolution,[status(thm)],[f173,f123]) ).
fof(f1646,plain,
! [X0,X1] :
( member(apply(choice,intersection(X0,X1)),X1)
| intersection(X0,X1) = null_class
| ~ member(intersection(X0,X1),universal_class) ),
inference(resolution,[status(thm)],[f173,f125]) ).
fof(f1667,plain,
restrict(intersection(cross_product(universal_class,universal_class),complement(compose(complement(element_relation),inverse(element_relation)))),universal_class,universal_class) = subset_relation,
inference(forward_demodulation,[status(thm)],[f132,f177]) ).
fof(f1668,plain,
restrict(restrict(complement(compose(complement(element_relation),inverse(element_relation))),universal_class,universal_class),universal_class,universal_class) = subset_relation,
inference(forward_demodulation,[status(thm)],[f132,f1667]) ).
fof(f1681,plain,
! [X0,X1] :
( regular(unordered_pair(X0,X1)) = X1
| regular(unordered_pair(X0,X1)) = X0
| unordered_pair(X0,X1) = null_class ),
inference(resolution,[status(thm)],[f169,f104]) ).
fof(f1824,plain,
( ~ sQ82_spl
| intersection(ordered_pair(null_class,w),singleton(null_class)) = null_class
| ordered_pair(null_class,w) = null_class ),
inference(paramodulation,[status(thm)],[f1092,f170]) ).
fof(f1828,plain,
! [X0] :
( X0 = null_class
| intersection(complement(null_class),union(X0,regular(X0))) = symmetric_difference(X0,regular(X0)) ),
inference(paramodulation,[status(thm)],[f170,f580]) ).
fof(f1829,plain,
! [X0,X1] :
( X1 = null_class
| member(X0,null_class)
| ~ member(X0,regular(X1))
| ~ member(X0,X1) ),
inference(paramodulation,[status(thm)],[f170,f126]) ).
fof(f1831,definition,
( sQ110_spl
<=> intersection(ordered_pair(null_class,w),singleton(null_class)) = null_class ),
introduced(definition,[new_symbols(definition,[sQ110_spl])],[split_symbol_definition]) ).
fof(f1834,plain,
( ~ sQ82_spl
| sQ110_spl
| sQ77_spl ),
inference(split_clause,[status(thm)],[f1824,f1073,f1831,f1091]) ).
fof(f1835,plain,
( ~ sQ80_spl
| ~ sQ32_spl
| sQ77_spl ),
inference(split_clause,[status(thm)],[f1101,f1073,f433,f1084]) ).
fof(f1841,plain,
! [X0] :
( ~ inductive(cantor(X0))
| member(null_class,domain_of(X0)) ),
inference(paramodulation,[status(thm)],[f180,f297]) ).
fof(f1941,plain,
( ~ sQ32_spl
| ordered_pair(null_class,w) = null_class
| ~ member(ordered_pair(null_class,w),universal_class)
| apply(choice,ordered_pair(null_class,w)) = singleton(null_class) ),
inference(resolution,[status(thm)],[f1068,f173]) ).
fof(f1946,definition,
( sQ112_spl
<=> apply(choice,ordered_pair(null_class,w)) = singleton(null_class) ),
introduced(definition,[new_symbols(definition,[sQ112_spl])],[split_symbol_definition]) ).
fof(f1949,definition,
( sQ113_spl
<=> member(ordered_pair(null_class,w),universal_class) ),
introduced(definition,[new_symbols(definition,[sQ113_spl])],[split_symbol_definition]) ).
fof(f1951,plain,
( sQ113_spl
| ~ member(ordered_pair(null_class,w),universal_class) ),
inference(component_clause,[status(thm)],[f1949]) ).
fof(f1952,plain,
( ~ sQ32_spl
| sQ77_spl
| ~ sQ113_spl
| sQ112_spl ),
inference(split_clause,[status(thm)],[f1941,f1946,f1949,f1073,f433]) ).
fof(f1955,plain,
( sQ113_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1951,f272]) ).
fof(f1956,plain,
sQ113_spl,
inference(contradiction_clause,[status(thm)],[f1955]) ).
fof(f1963,definition,
( sQ114_spl
<=> intersection(ordered_pair(null_class,w),null_class) = null_class ),
introduced(definition,[new_symbols(definition,[sQ114_spl])],[split_symbol_definition]) ).
fof(f1965,plain,
( sQ114_spl
| intersection(ordered_pair(null_class,w),null_class) != null_class ),
inference(component_clause,[status(thm)],[f1963]) ).
fof(f1967,definition,
( sQ115_spl
<=> member(null_class,ordered_pair(null_class,w)) ),
introduced(definition,[new_symbols(definition,[sQ115_spl])],[split_symbol_definition]) ).
fof(f1968,plain,
( ~ sQ115_spl
| member(null_class,ordered_pair(null_class,w)) ),
inference(component_clause,[status(thm)],[f1967]) ).
fof(f1969,plain,
( sQ115_spl
| ~ member(null_class,ordered_pair(null_class,w)) ),
inference(component_clause,[status(thm)],[f1967]) ).
fof(f1972,plain,
( ~ sQ32_spl
| ~ sQ115_spl
| null_class = singleton(null_class) ),
inference(resolution,[status(thm)],[f1968,f1068]) ).
fof(f1974,plain,
( ~ sQ32_spl
| ~ sQ115_spl
| sQ60_spl ),
inference(split_clause,[status(thm)],[f1972,f891,f1967,f433]) ).
fof(f1983,definition,
( sQ116_spl
<=> member(null_class,singleton(null_class)) ),
introduced(definition,[new_symbols(definition,[sQ116_spl])],[split_symbol_definition]) ).
fof(f1984,plain,
( ~ sQ116_spl
| member(null_class,singleton(null_class)) ),
inference(component_clause,[status(thm)],[f1983]) ).
fof(f1985,plain,
( sQ116_spl
| ~ member(null_class,singleton(null_class)) ),
inference(component_clause,[status(thm)],[f1983]) ).
fof(f2158,definition,
( sQ126_spl
<=> intersection(regular(null_class),null_class) = null_class ),
introduced(definition,[new_symbols(definition,[sQ126_spl])],[split_symbol_definition]) ).
fof(f2160,plain,
( sQ126_spl
| intersection(regular(null_class),null_class) != null_class ),
inference(component_clause,[status(thm)],[f2158]) ).
fof(f2185,definition,
( sQ127_spl
<=> member(singleton(null_class),null_class) ),
introduced(definition,[new_symbols(definition,[sQ127_spl])],[split_symbol_definition]) ).
fof(f2186,plain,
( ~ sQ127_spl
| member(singleton(null_class),null_class) ),
inference(component_clause,[status(thm)],[f2185]) ).
fof(f2187,plain,
( sQ127_spl
| ~ member(singleton(null_class),null_class) ),
inference(component_clause,[status(thm)],[f2185]) ).
fof(f2213,plain,
( ~ sQ25_spl
| ~ sQ32_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f399,f434]) ).
fof(f2214,plain,
( ~ sQ25_spl
| ~ sQ32_spl ),
inference(contradiction_clause,[status(thm)],[f2213]) ).
fof(f2215,plain,
( ~ sQ24_spl
| ~ sQ32_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f395,f434]) ).
fof(f2216,plain,
( ~ sQ24_spl
| ~ sQ32_spl ),
inference(contradiction_clause,[status(thm)],[f2215]) ).
fof(f2219,plain,
( ~ sQ19_spl
| ~ sQ28_spl
| x = z ),
inference(resolution,[status(thm)],[f1554,f969]) ).
fof(f2222,plain,
( ~ sQ19_spl
| ~ sQ28_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2219,f202]) ).
fof(f2223,plain,
( ~ sQ19_spl
| ~ sQ28_spl ),
inference(contradiction_clause,[status(thm)],[f2222]) ).
fof(f2320,definition,
! [X0] :
( sQ129_spl
<=> member(ordered_pair(null_class,w),ordered_pair(null_class,X0)) ),
introduced(definition,[new_symbols(definition,[sQ129_spl])],[split_symbol_definition]) ).
fof(f2321,plain,
! [X0] :
( ~ sQ129_spl
| member(ordered_pair(null_class,w),ordered_pair(null_class,X0)) ),
inference(component_clause,[status(thm)],[f2320]) ).
fof(f2324,plain,
( ~ sQ32_spl
| ~ sQ129_spl
| ordered_pair(null_class,w) = singleton(null_class) ),
inference(resolution,[status(thm)],[f2321,f1068]) ).
fof(f2335,plain,
( sQ115_spl
| ~ sQ32_spl
| ~ sQ129_spl
| ~ member(null_class,singleton(null_class)) ),
inference(backward_demodulation,[status(thm)],[f2324,f1969]) ).
fof(f2346,plain,
( sQ115_spl
| ~ sQ32_spl
| ~ sQ129_spl
| ~ sQ116_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2335,f1984]) ).
fof(f2347,plain,
( sQ115_spl
| ~ sQ32_spl
| ~ sQ129_spl
| ~ sQ116_spl ),
inference(contradiction_clause,[status(thm)],[f2346]) ).
fof(f2361,plain,
( sQ116_spl
| ~ member(null_class,universal_class) ),
inference(resolution,[status(thm)],[f1985,f263]) ).
fof(f2364,plain,
( sQ116_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f2361,f219,f1983]) ).
fof(f2374,plain,
! [X0] :
( omega = null_class
| ~ member(omega,universal_class)
| member(apply(choice,omega),X0)
| ~ inductive(X0) ),
inference(resolution,[status(thm)],[f211,f173]) ).
fof(f2375,plain,
! [X0] :
( ~ inductive(omega)
| member(null_class,X0)
| ~ inductive(X0) ),
inference(resolution,[status(thm)],[f211,f150]) ).
fof(f2377,plain,
! [X0] :
( omega = null_class
| member(regular(omega),X0)
| ~ inductive(X0) ),
inference(resolution,[status(thm)],[f211,f169]) ).
fof(f2378,definition,
! [X0] :
( sQ130_spl
<=> ( member(apply(choice,omega),X0)
| ~ inductive(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ130_spl])],[split_symbol_definition]) ).
fof(f2379,plain,
! [X0] :
( ~ sQ130_spl
| member(apply(choice,omega),X0)
| ~ inductive(X0) ),
inference(component_clause,[status(thm)],[f2378]) ).
fof(f2381,definition,
( sQ131_spl
<=> member(omega,universal_class) ),
introduced(definition,[new_symbols(definition,[sQ131_spl])],[split_symbol_definition]) ).
fof(f2383,plain,
( sQ131_spl
| ~ member(omega,universal_class) ),
inference(component_clause,[status(thm)],[f2381]) ).
fof(f2384,plain,
( sQ75_spl
| ~ sQ131_spl
| sQ130_spl ),
inference(split_clause,[status(thm)],[f2374,f2378,f2381,f1036]) ).
fof(f2385,definition,
! [X0] :
( sQ132_spl
<=> ( member(null_class,X0)
| ~ inductive(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ132_spl])],[split_symbol_definition]) ).
fof(f2388,plain,
( ~ sQ14_spl
| sQ132_spl ),
inference(split_clause,[status(thm)],[f2375,f2385,f339]) ).
fof(f2389,definition,
! [X0] :
( sQ133_spl
<=> ( member(regular(omega),X0)
| ~ inductive(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ133_spl])],[split_symbol_definition]) ).
fof(f2390,plain,
! [X0] :
( ~ sQ133_spl
| member(regular(omega),X0)
| ~ inductive(X0) ),
inference(component_clause,[status(thm)],[f2389]) ).
fof(f2392,plain,
( sQ75_spl
| sQ133_spl ),
inference(split_clause,[status(thm)],[f2377,f2389,f1036]) ).
fof(f2393,plain,
( sQ131_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2383,f155]) ).
fof(f2394,plain,
sQ131_spl,
inference(contradiction_clause,[status(thm)],[f2393]) ).
fof(f2448,plain,
( sQ51_spl
| ~ sQ75_spl
| ~ inductive(omega) ),
inference(backward_demodulation,[status(thm)],[f1037,f670]) ).
fof(f2471,plain,
( sQ51_spl
| ~ sQ75_spl
| ~ sQ14_spl ),
inference(split_clause,[status(thm)],[f2448,f339,f1036,f668]) ).
fof(f2479,plain,
! [X0,X1] :
( member(unordered_pair(X0,singleton(X1)),ordered_pair(X0,X1))
| ~ member(unordered_pair(X0,singleton(X1)),universal_class) ),
inference(paramodulation,[status(thm)],[f111,f108]) ).
fof(f2481,plain,
! [X0,X1] : member(unordered_pair(X0,singleton(X1)),ordered_pair(X0,X1)),
inference(forward_subsumption_resolution,[status(thm)],[f2479,f109]) ).
fof(f2610,definition,
! [X0] :
( sQ136_spl
<=> member(null_class,X0) ),
introduced(definition,[new_symbols(definition,[sQ136_spl])],[split_symbol_definition]) ).
fof(f2611,plain,
! [X0] :
( ~ sQ136_spl
| member(null_class,X0) ),
inference(component_clause,[status(thm)],[f2610]) ).
fof(f2614,plain,
( sQ89_spl
| ~ sQ136_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f1178,f2611]) ).
fof(f2628,plain,
( sQ89_spl
| ~ sQ136_spl ),
inference(contradiction_clause,[status(thm)],[f2614]) ).
fof(f2678,definition,
! [X0] :
( sQ137_spl
<=> member(regular(null_class),X0) ),
introduced(definition,[new_symbols(definition,[sQ137_spl])],[split_symbol_definition]) ).
fof(f2679,plain,
! [X0] :
( ~ sQ137_spl
| member(regular(null_class),X0) ),
inference(component_clause,[status(thm)],[f2678]) ).
fof(f2696,plain,
! [X0] :
( ~ sQ137_spl
| ~ member(regular(null_class),X0) ),
inference(resolution,[status(thm)],[f2679,f127]) ).
fof(f2704,plain,
( ~ sQ137_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2696,f2679]) ).
fof(f2705,plain,
~ sQ137_spl,
inference(contradiction_clause,[status(thm)],[f2704]) ).
fof(f2726,plain,
! [X0] :
( ~ sQ133_spl
| ~ member(regular(omega),X0)
| ~ inductive(complement(X0)) ),
inference(resolution,[status(thm)],[f2390,f127]) ).
fof(f2728,plain,
! [X0] :
( ~ sQ133_spl
| member(regular(omega),universal_class)
| ~ inductive(X0) ),
inference(resolution,[status(thm)],[f2390,f207]) ).
fof(f2729,definition,
! [X0] :
( sQ139_spl
<=> member(regular(omega),X0) ),
introduced(definition,[new_symbols(definition,[sQ139_spl])],[split_symbol_definition]) ).
fof(f2730,plain,
! [X0] :
( ~ sQ139_spl
| member(regular(omega),X0) ),
inference(component_clause,[status(thm)],[f2729]) ).
fof(f2733,definition,
( sQ140_spl
<=> regular(omega) = w ),
introduced(definition,[new_symbols(definition,[sQ140_spl])],[split_symbol_definition]) ).
fof(f2734,plain,
( ~ sQ140_spl
| regular(omega) = w ),
inference(component_clause,[status(thm)],[f2733]) ).
fof(f2735,plain,
( sQ140_spl
| regular(omega) != w ),
inference(component_clause,[status(thm)],[f2733]) ).
fof(f2750,definition,
( sQ144_spl
<=> member(regular(omega),universal_class) ),
introduced(definition,[new_symbols(definition,[sQ144_spl])],[split_symbol_definition]) ).
fof(f2753,plain,
( ~ sQ133_spl
| sQ144_spl
| sQ1_spl ),
inference(split_clause,[status(thm)],[f2728,f222,f2750,f2389]) ).
fof(f2756,definition,
( sQ145_spl
<=> member(null_class,omega) ),
introduced(definition,[new_symbols(definition,[sQ145_spl])],[split_symbol_definition]) ).
fof(f2758,plain,
( sQ145_spl
| ~ member(null_class,omega) ),
inference(component_clause,[status(thm)],[f2756]) ).
fof(f2785,plain,
( ~ sQ77_spl
| sQ127_spl ),
inference(split_clause,[status(thm)],[f1294,f2185,f1073]) ).
fof(f2795,plain,
( ~ sQ140_spl
| member(w,omega)
| omega = null_class ),
inference(paramodulation,[status(thm)],[f2734,f169]) ).
fof(f2796,plain,
( ~ sQ140_spl
| sQ93_spl
| sQ75_spl ),
inference(split_clause,[status(thm)],[f2795,f1036,f1255,f2733]) ).
fof(f2822,plain,
! [X0] :
( ~ sQ31_spl
| x = X0
| x = z ),
inference(resolution,[status(thm)],[f425,f104]) ).
fof(f2825,definition,
( sQ150_spl
<=> x = z ),
introduced(definition,[new_symbols(definition,[sQ150_spl])],[split_symbol_definition]) ).
fof(f2826,plain,
( ~ sQ150_spl
| x = z ),
inference(component_clause,[status(thm)],[f2825]) ).
fof(f2828,definition,
! [X0] :
( sQ151_spl
<=> x = X0 ),
introduced(definition,[new_symbols(definition,[sQ151_spl])],[split_symbol_definition]) ).
fof(f2829,plain,
! [X0] :
( ~ sQ151_spl
| x = X0 ),
inference(component_clause,[status(thm)],[f2828]) ).
fof(f2831,plain,
( ~ sQ31_spl
| sQ151_spl
| sQ150_spl ),
inference(split_clause,[status(thm)],[f2822,f2825,f2828,f424]) ).
fof(f2832,plain,
( ~ sQ150_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2826,f202]) ).
fof(f2833,plain,
~ sQ150_spl,
inference(contradiction_clause,[status(thm)],[f2832]) ).
fof(f2834,plain,
! [X0] :
( ~ sQ30_spl
| x = z
| x = X0 ),
inference(resolution,[status(thm)],[f421,f104]) ).
fof(f2837,plain,
( ~ sQ30_spl
| sQ150_spl
| sQ151_spl ),
inference(split_clause,[status(thm)],[f2834,f2828,f2825,f420]) ).
fof(f2838,plain,
( ~ sQ151_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f202,f2829]) ).
fof(f2846,plain,
~ sQ151_spl,
inference(contradiction_clause,[status(thm)],[f2838]) ).
fof(f2855,plain,
! [X0] :
( ~ sQ139_spl
| ~ member(regular(omega),X0) ),
inference(resolution,[status(thm)],[f2730,f127]) ).
fof(f2859,definition,
! [X0] :
( sQ152_spl
<=> regular(omega) = X0 ),
introduced(definition,[new_symbols(definition,[sQ152_spl])],[split_symbol_definition]) ).
fof(f2860,plain,
! [X0] :
( ~ sQ152_spl
| regular(omega) = X0 ),
inference(component_clause,[status(thm)],[f2859]) ).
fof(f2863,plain,
( ~ sQ139_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2855,f2730]) ).
fof(f2864,plain,
~ sQ139_spl,
inference(contradiction_clause,[status(thm)],[f2863]) ).
fof(f2865,plain,
( sQ140_spl
| ~ sQ152_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f2735,f2860]) ).
fof(f2868,plain,
( sQ140_spl
| ~ sQ152_spl ),
inference(contradiction_clause,[status(thm)],[f2865]) ).
fof(f2977,plain,
member(singleton(w),ordered_pair(y,z)),
inference(paramodulation,[status(thm)],[f200,f275]) ).
fof(f2995,plain,
( sQ95_spl
| ~ sQ46_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f1314,f541]) ).
fof(f3007,plain,
( sQ95_spl
| ~ sQ46_spl ),
inference(contradiction_clause,[status(thm)],[f2995]) ).
fof(f3139,definition,
! [X0] :
( sQ158_spl
<=> ~ function(X0) ),
introduced(definition,[new_symbols(definition,[sQ158_spl])],[split_symbol_definition]) ).
fof(f3140,plain,
! [X0] :
( ~ sQ158_spl
| ~ function(X0) ),
inference(component_clause,[status(thm)],[f3139]) ).
fof(f3150,plain,
( ~ sQ158_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f172,f3140]) ).
fof(f3151,plain,
~ sQ158_spl,
inference(contradiction_clause,[status(thm)],[f3150]) ).
fof(f3424,plain,
! [X0] :
( member(regular(X0),universal_class)
| X0 = null_class ),
inference(resolution,[status(thm)],[f169,f207]) ).
fof(f3527,definition,
! [X0] :
( sQ167_spl
<=> member(apply(choice,null_class),X0) ),
introduced(definition,[new_symbols(definition,[sQ167_spl])],[split_symbol_definition]) ).
fof(f3528,plain,
! [X0] :
( ~ sQ167_spl
| member(apply(choice,null_class),X0) ),
inference(component_clause,[status(thm)],[f3527]) ).
fof(f3553,plain,
! [X0] :
( ~ sQ167_spl
| ~ member(apply(choice,null_class),X0) ),
inference(resolution,[status(thm)],[f3528,f127]) ).
fof(f3560,plain,
( ~ sQ167_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3553,f3528]) ).
fof(f3561,plain,
~ sQ167_spl,
inference(contradiction_clause,[status(thm)],[f3560]) ).
fof(f3566,definition,
! [X0] :
( sQ170_spl
<=> member(X0,null_class) ),
introduced(definition,[new_symbols(definition,[sQ170_spl])],[split_symbol_definition]) ).
fof(f3567,plain,
! [X0] :
( ~ sQ170_spl
| member(X0,null_class) ),
inference(component_clause,[status(thm)],[f3566]) ).
fof(f3570,plain,
( sQ127_spl
| ~ sQ170_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f2187,f3567]) ).
fof(f3582,plain,
( sQ127_spl
| ~ sQ170_spl ),
inference(contradiction_clause,[status(thm)],[f3570]) ).
fof(f3672,definition,
! [X0] :
( sQ176_spl
<=> ( member(X0,universal_class)
| regular(omega) = X0 ) ),
introduced(definition,[new_symbols(definition,[sQ176_spl])],[split_symbol_definition]) ).
fof(f3673,plain,
! [X0] :
( ~ sQ176_spl
| member(X0,universal_class)
| regular(omega) = X0 ),
inference(component_clause,[status(thm)],[f3672]) ).
fof(f3897,plain,
( ~ sQ66_spl
| ~ sQ19_spl
| y = z ),
inference(resolution,[status(thm)],[f969,f947]) ).
fof(f3905,plain,
( ~ sQ23_spl
| ~ sQ66_spl
| ~ sQ19_spl
| member(z,universal_class) ),
inference(backward_demodulation,[status(thm)],[f3897,f391]) ).
fof(f3907,plain,
( ~ sQ66_spl
| ~ sQ19_spl
| member(z,null_class) ),
inference(backward_demodulation,[status(thm)],[f3897,f947]) ).
fof(f3919,plain,
( ~ sQ23_spl
| ~ sQ66_spl
| ~ sQ19_spl
| sQ29_spl ),
inference(split_clause,[status(thm)],[f3905,f416,f372,f946,f390]) ).
fof(f3921,plain,
( ~ sQ66_spl
| ~ sQ19_spl
| sQ70_spl ),
inference(split_clause,[status(thm)],[f3907,f978,f372,f946]) ).
fof(f4003,plain,
! [X0,X1] :
( null_class = X1
| null_class = X0
| ~ inductive(unordered_pair(X0,X1)) ),
inference(resolution,[status(thm)],[f150,f104]) ).
fof(f4113,plain,
! [X0] :
( ~ sQ133_spl
| ~ member(regular(omega),X0)
| ~ inductive(complement(X0)) ),
inference(resolution,[status(thm)],[f2390,f127]) ).
fof(f4133,definition,
( sQ182_spl
<=> regular(omega) = singleton(null_class) ),
introduced(definition,[new_symbols(definition,[sQ182_spl])],[split_symbol_definition]) ).
fof(f4134,plain,
( ~ sQ182_spl
| regular(omega) = singleton(null_class) ),
inference(component_clause,[status(thm)],[f4133]) ).
fof(f4152,plain,
( ~ sQ182_spl
| member(null_class,regular(omega))
| ~ member(null_class,universal_class) ),
inference(paramodulation,[status(thm)],[f4134,f263]) ).
fof(f4170,definition,
( sQ185_spl
<=> member(null_class,regular(omega)) ),
introduced(definition,[new_symbols(definition,[sQ185_spl])],[split_symbol_definition]) ).
fof(f4171,plain,
( ~ sQ185_spl
| member(null_class,regular(omega)) ),
inference(component_clause,[status(thm)],[f4170]) ).
fof(f4173,plain,
( ~ sQ182_spl
| sQ185_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f4152,f219,f4170,f4133]) ).
fof(f4429,plain,
( sQ140_spl
| ~ sQ176_spl
| member(w,universal_class) ),
inference(resolution,[status(thm)],[f3673,f2735]) ).
fof(f4443,plain,
( sQ140_spl
| ~ sQ176_spl
| sQ44_spl ),
inference(split_clause,[status(thm)],[f4429,f527,f3672,f2733]) ).
fof(f4610,plain,
( complement(universal_class) = null_class
| complement(universal_class) = null_class ),
inference(resolution,[status(thm)],[f241,f3424]) ).
fof(f4618,definition,
( sQ189_spl
<=> complement(universal_class) = null_class ),
introduced(definition,[new_symbols(definition,[sQ189_spl])],[split_symbol_definition]) ).
fof(f4619,plain,
( ~ sQ189_spl
| complement(universal_class) = null_class ),
inference(component_clause,[status(thm)],[f4618]) ).
fof(f4621,plain,
sQ189_spl,
inference(split_clause,[status(thm)],[f4610,f4618]) ).
fof(f4667,plain,
( ~ sQ32_spl
| member(null_class,ordered_pair(y,z)) ),
inference(forward_demodulation,[status(thm)],[f885,f2977]) ).
fof(f4762,plain,
! [X0] :
( ~ sQ32_spl
| ~ sQ64_spl
| member(w,ordered_pair(w,X0)) ),
inference(backward_demodulation,[status(thm)],[f924,f904]) ).
fof(f4807,plain,
( ~ sQ32_spl
| ~ sQ64_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4762,f434]) ).
fof(f4808,plain,
( ~ sQ32_spl
| ~ sQ64_spl ),
inference(contradiction_clause,[status(thm)],[f4807]) ).
fof(f4824,plain,
( ~ sQ189_spl
| ~ inductive(universal_class)
| ~ inductive(null_class) ),
inference(paramodulation,[status(thm)],[f4619,f282]) ).
fof(f4827,plain,
! [X0] :
( ~ sQ189_spl
| ~ member(X0,universal_class)
| ~ member(X0,null_class) ),
inference(paramodulation,[status(thm)],[f4619,f127]) ).
fof(f4831,plain,
( ~ sQ189_spl
| ~ sQ73_spl
| ~ sQ51_spl ),
inference(split_clause,[status(thm)],[f4824,f668,f1018,f4618]) ).
fof(f4832,plain,
! [X0] :
( ~ sQ189_spl
| ~ member(X0,null_class) ),
inference(forward_subsumption_resolution,[status(thm)],[f4827,f207]) ).
fof(f5146,plain,
! [X0] :
( ~ sQ32_spl
| member(singleton(null_class),domain_of(X0))
| restrict(X0,ordered_pair(null_class,w),universal_class) = null_class
| ~ member(singleton(null_class),universal_class) ),
inference(paramodulation,[status(thm)],[f1056,f134]) ).
fof(f5165,definition,
! [X0] :
( sQ202_spl
<=> ( member(singleton(null_class),domain_of(X0))
| restrict(X0,ordered_pair(null_class,w),universal_class) = null_class ) ),
introduced(definition,[new_symbols(definition,[sQ202_spl])],[split_symbol_definition]) ).
fof(f5168,plain,
( ~ sQ32_spl
| sQ202_spl
| ~ sQ78_spl ),
inference(split_clause,[status(thm)],[f5146,f1076,f5165,f433]) ).
fof(f5273,plain,
member(unordered_pair(w,singleton(x)),ordered_pair(y,z)),
inference(paramodulation,[status(thm)],[f200,f274]) ).
fof(f5277,plain,
( ~ sQ32_spl
| null_class = unordered_pair(y,singleton(z))
| null_class = singleton(y) ),
inference(resolution,[status(thm)],[f271,f4667]) ).
fof(f5286,plain,
! [X0] :
( X0 = unordered_pair(w,singleton(x))
| X0 = singleton(w)
| ~ member(X0,ordered_pair(y,z)) ),
inference(paramodulation,[status(thm)],[f200,f271]) ).
fof(f5291,definition,
! [X0] :
( sQ204_spl
<=> null_class = unordered_pair(z,singleton(X0)) ),
introduced(definition,[new_symbols(definition,[sQ204_spl])],[split_symbol_definition]) ).
fof(f5292,plain,
! [X0] :
( ~ sQ204_spl
| null_class = unordered_pair(z,singleton(X0)) ),
inference(component_clause,[status(thm)],[f5291]) ).
fof(f5295,definition,
( sQ205_spl
<=> null_class = unordered_pair(y,singleton(z)) ),
introduced(definition,[new_symbols(definition,[sQ205_spl])],[split_symbol_definition]) ).
fof(f5296,plain,
( ~ sQ205_spl
| null_class = unordered_pair(y,singleton(z)) ),
inference(component_clause,[status(thm)],[f5295]) ).
fof(f5297,plain,
( sQ205_spl
| null_class != unordered_pair(y,singleton(z)) ),
inference(component_clause,[status(thm)],[f5295]) ).
fof(f5298,plain,
( ~ sQ32_spl
| sQ205_spl
| sQ65_spl ),
inference(split_clause,[status(thm)],[f5277,f943,f5295,f433]) ).
fof(f5302,plain,
! [X0] :
( ~ sQ32_spl
| X0 = unordered_pair(w,singleton(x))
| X0 = null_class
| ~ member(X0,ordered_pair(y,z)) ),
inference(forward_demodulation,[status(thm)],[f885,f5286]) ).
fof(f5306,plain,
( ~ sQ65_spl
| singleton(singleton(null_class)) = ordered_pair(singleton(y),y) ),
inference(paramodulation,[status(thm)],[f944,f273]) ).
fof(f5326,plain,
( ~ sQ65_spl
| ~ sQ32_spl
| ordered_pair(null_class,w) = ordered_pair(singleton(y),y) ),
inference(forward_demodulation,[status(thm)],[f1056,f5306]) ).
fof(f5327,plain,
( ~ sQ65_spl
| ~ sQ32_spl
| ordered_pair(null_class,w) = ordered_pair(null_class,y) ),
inference(forward_demodulation,[status(thm)],[f944,f5326]) ).
fof(f5348,definition,
( sQ207_spl
<=> unordered_pair(y,null_class) = null_class ),
introduced(definition,[new_symbols(definition,[sQ207_spl])],[split_symbol_definition]) ).
fof(f5349,plain,
( ~ sQ207_spl
| unordered_pair(y,null_class) = null_class ),
inference(component_clause,[status(thm)],[f5348]) ).
fof(f5370,plain,
( ~ sQ207_spl
| member(null_class,null_class)
| ~ member(null_class,universal_class) ),
inference(paramodulation,[status(thm)],[f5349,f108]) ).
fof(f5378,plain,
( ~ sQ207_spl
| sQ89_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f5370,f219,f1176,f5348]) ).
fof(f5379,plain,
( unordered_pair(w,singleton(x)) = unordered_pair(y,singleton(z))
| unordered_pair(w,singleton(x)) = singleton(y) ),
inference(resolution,[status(thm)],[f5273,f271]) ).
fof(f5382,definition,
( sQ208_spl
<=> unordered_pair(w,singleton(x)) = singleton(y) ),
introduced(definition,[new_symbols(definition,[sQ208_spl])],[split_symbol_definition]) ).
fof(f5383,plain,
( ~ sQ208_spl
| unordered_pair(w,singleton(x)) = singleton(y) ),
inference(component_clause,[status(thm)],[f5382]) ).
fof(f5385,definition,
( sQ209_spl
<=> unordered_pair(w,singleton(x)) = unordered_pair(y,singleton(z)) ),
introduced(definition,[new_symbols(definition,[sQ209_spl])],[split_symbol_definition]) ).
fof(f5386,plain,
( ~ sQ209_spl
| unordered_pair(w,singleton(x)) = unordered_pair(y,singleton(z)) ),
inference(component_clause,[status(thm)],[f5385]) ).
fof(f5388,plain,
( sQ209_spl
| sQ208_spl ),
inference(split_clause,[status(thm)],[f5379,f5382,f5385]) ).
fof(f5389,definition,
( sQ210_spl
<=> member(unordered_pair(w,null_class),ordered_pair(y,z)) ),
introduced(definition,[new_symbols(definition,[sQ210_spl])],[split_symbol_definition]) ).
fof(f5390,plain,
( ~ sQ210_spl
| member(unordered_pair(w,null_class),ordered_pair(y,z)) ),
inference(component_clause,[status(thm)],[f5389]) ).
fof(f5393,plain,
( ~ sQ208_spl
| ~ sQ65_spl
| unordered_pair(w,singleton(x)) = null_class ),
inference(forward_demodulation,[status(thm)],[f944,f5383]) ).
fof(f5400,plain,
! [X0] :
( ~ sQ204_spl
| member(X0,universal_class)
| null_class = unordered_pair(z,null_class) ),
inference(paramodulation,[status(thm)],[f641,f5292]) ).
fof(f5411,definition,
( sQ211_spl
<=> null_class = unordered_pair(z,null_class) ),
introduced(definition,[new_symbols(definition,[sQ211_spl])],[split_symbol_definition]) ).
fof(f5412,plain,
( ~ sQ211_spl
| null_class = unordered_pair(z,null_class) ),
inference(component_clause,[status(thm)],[f5411]) ).
fof(f5414,plain,
( ~ sQ204_spl
| sQ52_spl
| sQ211_spl ),
inference(split_clause,[status(thm)],[f5400,f5411,f672,f5291]) ).
fof(f5419,definition,
! [X0] :
( sQ212_spl
<=> null_class = singleton(X0) ),
introduced(definition,[new_symbols(definition,[sQ212_spl])],[split_symbol_definition]) ).
fof(f5420,plain,
! [X0] :
( ~ sQ212_spl
| null_class = singleton(X0) ),
inference(component_clause,[status(thm)],[f5419]) ).
fof(f5435,plain,
( sQ60_spl
| ~ sQ212_spl
| null_class != null_class ),
inference(backward_demodulation,[status(thm)],[f5420,f893]) ).
fof(f5461,plain,
( sQ60_spl
| ~ sQ212_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f5435]) ).
fof(f5462,plain,
( sQ60_spl
| ~ sQ212_spl ),
inference(contradiction_clause,[status(thm)],[f5461]) ).
fof(f5469,plain,
( ~ sQ211_spl
| member(null_class,null_class)
| ~ member(null_class,universal_class) ),
inference(paramodulation,[status(thm)],[f5412,f108]) ).
fof(f5480,plain,
( ~ sQ211_spl
| sQ89_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f5469,f219,f1176,f5411]) ).
fof(f5685,plain,
( ~ sQ208_spl
| ~ sQ65_spl
| member(singleton(x),null_class)
| ~ member(singleton(x),universal_class) ),
inference(paramodulation,[status(thm)],[f5393,f108]) ).
fof(f5690,definition,
( sQ219_spl
<=> null_class = singleton(x) ),
introduced(definition,[new_symbols(definition,[sQ219_spl])],[split_symbol_definition]) ).
fof(f5691,plain,
( ~ sQ219_spl
| null_class = singleton(x) ),
inference(component_clause,[status(thm)],[f5690]) ).
fof(f5694,definition,
( sQ220_spl
<=> regular(unordered_pair(w,singleton(x))) = w ),
introduced(definition,[new_symbols(definition,[sQ220_spl])],[split_symbol_definition]) ).
fof(f5695,plain,
( ~ sQ220_spl
| regular(unordered_pair(w,singleton(x))) = w ),
inference(component_clause,[status(thm)],[f5694]) ).
fof(f5696,plain,
( sQ220_spl
| regular(unordered_pair(w,singleton(x))) != w ),
inference(component_clause,[status(thm)],[f5694]) ).
fof(f5700,definition,
( sQ222_spl
<=> unordered_pair(w,singleton(x)) = null_class ),
introduced(definition,[new_symbols(definition,[sQ222_spl])],[split_symbol_definition]) ).
fof(f5701,plain,
( ~ sQ222_spl
| unordered_pair(w,singleton(x)) = null_class ),
inference(component_clause,[status(thm)],[f5700]) ).
fof(f5705,definition,
( sQ223_spl
<=> member(singleton(x),universal_class) ),
introduced(definition,[new_symbols(definition,[sQ223_spl])],[split_symbol_definition]) ).
fof(f5707,plain,
( sQ223_spl
| ~ member(singleton(x),universal_class) ),
inference(component_clause,[status(thm)],[f5705]) ).
fof(f5708,definition,
( sQ224_spl
<=> member(singleton(x),null_class) ),
introduced(definition,[new_symbols(definition,[sQ224_spl])],[split_symbol_definition]) ).
fof(f5709,plain,
( ~ sQ224_spl
| member(singleton(x),null_class) ),
inference(component_clause,[status(thm)],[f5708]) ).
fof(f5711,plain,
( ~ sQ208_spl
| ~ sQ65_spl
| sQ224_spl
| ~ sQ223_spl ),
inference(split_clause,[status(thm)],[f5685,f5705,f5708,f943,f5382]) ).
fof(f5712,plain,
( sQ223_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5707,f208]) ).
fof(f5713,plain,
sQ223_spl,
inference(contradiction_clause,[status(thm)],[f5712]) ).
fof(f5714,plain,
( ~ sQ224_spl
| ~ sQ189_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5709,f4832]) ).
fof(f5715,plain,
( ~ sQ224_spl
| ~ sQ189_spl ),
inference(contradiction_clause,[status(thm)],[f5714]) ).
fof(f5982,plain,
! [X0] :
( ~ member(null_class,X0)
| ~ inductive(complement(X0)) ),
inference(resolution,[status(thm)],[f150,f127]) ).
fof(f6003,plain,
! [X0] :
( member(regular(X0),universal_class)
| X0 = null_class ),
inference(resolution,[status(thm)],[f169,f207]) ).
fof(f6040,plain,
( ~ sQ222_spl
| member(singleton(x),null_class)
| ~ member(singleton(x),universal_class) ),
inference(paramodulation,[status(thm)],[f5701,f108]) ).
fof(f6049,plain,
( ~ sQ222_spl
| sQ224_spl
| ~ sQ223_spl ),
inference(split_clause,[status(thm)],[f6040,f5705,f5708,f5700]) ).
fof(f6080,definition,
( sQ229_spl
<=> unordered_pair(w,null_class) = null_class ),
introduced(definition,[new_symbols(definition,[sQ229_spl])],[split_symbol_definition]) ).
fof(f6081,plain,
( ~ sQ229_spl
| unordered_pair(w,null_class) = null_class ),
inference(component_clause,[status(thm)],[f6080]) ).
fof(f6082,plain,
( sQ229_spl
| unordered_pair(w,null_class) != null_class ),
inference(component_clause,[status(thm)],[f6080]) ).
fof(f6145,plain,
! [X0] :
( ~ sQ189_spl
| intersection(null_class,X0) = null_class ),
inference(resolution,[status(thm)],[f296,f4832]) ).
fof(f6175,plain,
! [X0,X1] :
( subclass(intersection(X0,X1),X0)
| subclass(intersection(X0,X1),X0) ),
inference(resolution,[status(thm)],[f298,f98]) ).
fof(f6191,plain,
! [X0,X1] : subclass(intersection(X0,X1),X0),
inference(duplicate_literals_removal,[status(thm)],[f6175]) ).
fof(f6234,plain,
! [X0,X1] :
( ~ sQ189_spl
| restrict(null_class,X0,X1) = null_class ),
inference(paramodulation,[status(thm)],[f131,f6145]) ).
fof(f6247,definition,
( sQ234_spl
<=> member(regular(null_class),null_class) ),
introduced(definition,[new_symbols(definition,[sQ234_spl])],[split_symbol_definition]) ).
fof(f6248,plain,
( ~ sQ234_spl
| member(regular(null_class),null_class) ),
inference(component_clause,[status(thm)],[f6247]) ).
fof(f6250,definition,
! [X0] :
( sQ235_spl
<=> intersection(null_class,X0) = null_class ),
introduced(definition,[new_symbols(definition,[sQ235_spl])],[split_symbol_definition]) ).
fof(f6254,plain,
( ~ sQ234_spl
| ~ sQ189_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6248,f4832]) ).
fof(f6255,plain,
( ~ sQ234_spl
| ~ sQ189_spl ),
inference(contradiction_clause,[status(thm)],[f6254]) ).
fof(f6258,plain,
! [X0,X1] :
( X0 = intersection(X0,X1)
| ~ subclass(X0,intersection(X0,X1)) ),
inference(resolution,[status(thm)],[f6191,f102]) ).
fof(f6262,plain,
! [X0,X1,X2] : subclass(restrict(X0,X1,X2),cross_product(X1,X2)),
inference(paramodulation,[status(thm)],[f132,f6191]) ).
fof(f6267,plain,
! [X0] :
( ~ sQ189_spl
| ~ member(X0,domain_of(null_class)) ),
inference(resolution,[status(thm)],[f6234,f133]) ).
fof(f6268,plain,
! [X0] :
( ~ sQ189_spl
| member(X0,domain_of(null_class))
| null_class = null_class
| ~ member(X0,universal_class) ),
inference(paramodulation,[status(thm)],[f6234,f134]) ).
fof(f6269,plain,
! [X0] :
( ~ sQ189_spl
| ~ member(X0,domain_of(null_class))
| null_class != null_class ),
inference(paramodulation,[status(thm)],[f6234,f133]) ).
fof(f6273,definition,
! [X0] :
( sQ236_spl
<=> ( member(X0,domain_of(null_class))
| ~ member(X0,universal_class) ) ),
introduced(definition,[new_symbols(definition,[sQ236_spl])],[split_symbol_definition]) ).
fof(f6274,plain,
! [X0] :
( ~ sQ236_spl
| member(X0,domain_of(null_class))
| ~ member(X0,universal_class) ),
inference(component_clause,[status(thm)],[f6273]) ).
fof(f6276,plain,
( ~ sQ189_spl
| sQ53_spl
| sQ236_spl ),
inference(split_clause,[status(thm)],[f6268,f6273,f684,f4618]) ).
fof(f6277,definition,
! [X0] :
( sQ237_spl
<=> ~ member(X0,domain_of(null_class)) ),
introduced(definition,[new_symbols(definition,[sQ237_spl])],[split_symbol_definition]) ).
fof(f6280,plain,
( ~ sQ189_spl
| sQ237_spl
| ~ sQ53_spl ),
inference(split_clause,[status(thm)],[f6269,f684,f6277,f4618]) ).
fof(f6282,plain,
( ~ sQ189_spl
| domain_of(null_class) = null_class
| ~ member(domain_of(null_class),universal_class) ),
inference(resolution,[status(thm)],[f6267,f173]) ).
fof(f6287,plain,
( ~ sQ189_spl
| domain_of(null_class) = null_class ),
inference(resolution,[status(thm)],[f6267,f169]) ).
fof(f6288,definition,
( sQ238_spl
<=> member(domain_of(null_class),universal_class) ),
introduced(definition,[new_symbols(definition,[sQ238_spl])],[split_symbol_definition]) ).
fof(f6290,plain,
( sQ238_spl
| ~ member(domain_of(null_class),universal_class) ),
inference(component_clause,[status(thm)],[f6288]) ).
fof(f6291,definition,
( sQ239_spl
<=> domain_of(null_class) = null_class ),
introduced(definition,[new_symbols(definition,[sQ239_spl])],[split_symbol_definition]) ).
fof(f6294,plain,
( ~ sQ189_spl
| sQ239_spl
| ~ sQ238_spl ),
inference(split_clause,[status(thm)],[f6282,f6288,f6291,f4618]) ).
fof(f6346,plain,
! [X0] :
( ~ sQ189_spl
| intersection(X0,null_class) = null_class ),
inference(resolution,[status(thm)],[f300,f4832]) ).
fof(f6367,plain,
! [X0,X1] :
( subclass(intersection(X0,X1),X1)
| subclass(intersection(X0,X1),X1) ),
inference(resolution,[status(thm)],[f302,f98]) ).
fof(f6384,plain,
! [X0,X1] : subclass(intersection(X0,X1),X1),
inference(duplicate_literals_removal,[status(thm)],[f6367]) ).
fof(f6445,plain,
! [X0,X1] :
( ~ sQ32_spl
| subclass(intersection(X0,ordered_pair(y,z)),X1)
| not_subclass_element(intersection(X0,ordered_pair(y,z)),X1) = unordered_pair(w,singleton(x))
| not_subclass_element(intersection(X0,ordered_pair(y,z)),X1) = null_class ),
inference(resolution,[status(thm)],[f5302,f302]) ).
fof(f6446,plain,
! [X0,X1] :
( ~ sQ32_spl
| subclass(intersection(ordered_pair(y,z),X0),X1)
| not_subclass_element(intersection(ordered_pair(y,z),X0),X1) = unordered_pair(w,singleton(x))
| not_subclass_element(intersection(ordered_pair(y,z),X0),X1) = null_class ),
inference(resolution,[status(thm)],[f5302,f298]) ).
fof(f6447,plain,
! [X0] :
( ~ sQ32_spl
| subclass(ordered_pair(y,z),X0)
| not_subclass_element(ordered_pair(y,z),X0) = unordered_pair(w,singleton(x))
| not_subclass_element(ordered_pair(y,z),X0) = null_class ),
inference(resolution,[status(thm)],[f5302,f97]) ).
fof(f6463,definition,
( sQ254_spl
<=> ordered_pair(y,z) = null_class ),
introduced(definition,[new_symbols(definition,[sQ254_spl])],[split_symbol_definition]) ).
fof(f6464,plain,
( ~ sQ254_spl
| ordered_pair(y,z) = null_class ),
inference(component_clause,[status(thm)],[f6463]) ).
fof(f6490,definition,
! [X0] :
( sQ257_spl
<=> intersection(X0,null_class) = null_class ),
introduced(definition,[new_symbols(definition,[sQ257_spl])],[split_symbol_definition]) ).
fof(f6497,plain,
! [X0,X1] :
( X0 = intersection(X1,X0)
| ~ subclass(X0,intersection(X1,X0)) ),
inference(resolution,[status(thm)],[f6384,f102]) ).
fof(f6534,plain,
( sQ38_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f457,f272]) ).
fof(f6535,plain,
sQ38_spl,
inference(contradiction_clause,[status(thm)],[f6534]) ).
fof(f6537,plain,
( sQ126_spl
| ~ sQ189_spl
| null_class != null_class ),
inference(forward_demodulation,[status(thm)],[f6346,f2160]) ).
fof(f6538,plain,
( sQ126_spl
| ~ sQ189_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f6537]) ).
fof(f6539,plain,
( sQ126_spl
| ~ sQ189_spl ),
inference(contradiction_clause,[status(thm)],[f6538]) ).
fof(f6540,plain,
( sQ114_spl
| ~ sQ189_spl
| null_class != null_class ),
inference(forward_demodulation,[status(thm)],[f6346,f1965]) ).
fof(f6541,plain,
( sQ114_spl
| ~ sQ189_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f6540]) ).
fof(f6542,plain,
( sQ114_spl
| ~ sQ189_spl ),
inference(contradiction_clause,[status(thm)],[f6541]) ).
fof(f6573,plain,
( ~ sQ189_spl
| complement(domain_of(null_class)) = diagonalise(null_class) ),
inference(paramodulation,[status(thm)],[f6145,f179]) ).
fof(f6583,plain,
( ~ sQ189_spl
| complement(null_class) = diagonalise(null_class) ),
inference(forward_demodulation,[status(thm)],[f6287,f6573]) ).
fof(f6682,definition,
( sQ265_spl
<=> subclass(subset_relation,cross_product(universal_class,universal_class)) ),
introduced(definition,[new_symbols(definition,[sQ265_spl])],[split_symbol_definition]) ).
fof(f6684,plain,
( sQ265_spl
| ~ subclass(subset_relation,cross_product(universal_class,universal_class)) ),
inference(component_clause,[status(thm)],[f6682]) ).
fof(f6711,plain,
( sQ238_spl
| ~ sQ189_spl
| ~ member(null_class,universal_class) ),
inference(forward_demodulation,[status(thm)],[f6287,f6290]) ).
fof(f6712,plain,
( sQ238_spl
| ~ sQ189_spl
| ~ sQ49_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6711,f777]) ).
fof(f6713,plain,
( sQ238_spl
| ~ sQ189_spl
| ~ sQ49_spl ),
inference(contradiction_clause,[status(thm)],[f6712]) ).
fof(f6757,plain,
( ~ sQ254_spl
| member(unordered_pair(w,singleton(x)),null_class) ),
inference(backward_demodulation,[status(thm)],[f6464,f5273]) ).
fof(f6783,plain,
( ~ sQ254_spl
| ~ sQ189_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6757,f4832]) ).
fof(f6784,plain,
( ~ sQ254_spl
| ~ sQ189_spl ),
inference(contradiction_clause,[status(thm)],[f6783]) ).
fof(f6791,definition,
( sQ274_spl
<=> subclass(null_class,range_of(null_class)) ),
introduced(definition,[new_symbols(definition,[sQ274_spl])],[split_symbol_definition]) ).
fof(f6793,plain,
( sQ274_spl
| ~ subclass(null_class,range_of(null_class)) ),
inference(component_clause,[status(thm)],[f6791]) ).
fof(f6798,plain,
( sQ274_spl
| ~ sQ74_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6793,f1033]) ).
fof(f6799,plain,
( sQ274_spl
| ~ sQ74_spl ),
inference(contradiction_clause,[status(thm)],[f6798]) ).
fof(f6876,plain,
! [X0] :
( ~ sQ189_spl
| member(X0,null_class)
| member(X0,diagonalise(null_class))
| ~ member(X0,universal_class) ),
inference(paramodulation,[status(thm)],[f6583,f128]) ).
fof(f6886,plain,
! [X0] :
( ~ sQ189_spl
| member(X0,diagonalise(null_class))
| ~ member(X0,universal_class) ),
inference(forward_subsumption_resolution,[status(thm)],[f6876,f4832]) ).
fof(f7185,plain,
! [X0,X1] :
( member(null_class,X0)
| ~ inductive(intersection(X0,X1)) ),
inference(resolution,[status(thm)],[f150,f123]) ).
fof(f7319,definition,
! [X0] :
( sQ288_spl
<=> ~ member(X0,universal_class) ),
introduced(definition,[new_symbols(definition,[sQ288_spl])],[split_symbol_definition]) ).
fof(f7320,plain,
! [X0] :
( ~ sQ288_spl
| ~ member(X0,universal_class) ),
inference(component_clause,[status(thm)],[f7319]) ).
fof(f7342,plain,
! [X0,X1] :
( ~ sQ288_spl
| ~ member(X0,X1) ),
inference(backward_subsumption_resolution,[status(thm)],[f207,f7320]) ).
fof(f7357,plain,
( ~ sQ288_spl
| sQ20_spl ),
inference(split_clause,[status(thm)],[f7342,f376,f7319]) ).
fof(f7605,plain,
! [X0] :
( ~ sQ133_spl
| ~ member(regular(omega),X0)
| ~ inductive(complement(X0)) ),
inference(resolution,[status(thm)],[f2390,f127]) ).
fof(f7841,plain,
! [X0,X1] :
( ~ sQ189_spl
| X1 = null_class
| ~ member(X0,regular(X1))
| ~ member(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f518,f4832]) ).
fof(f7843,plain,
( ~ sQ185_spl
| ~ sQ189_spl
| omega = null_class
| ~ member(null_class,omega) ),
inference(resolution,[status(thm)],[f7841,f4171]) ).
fof(f7853,plain,
( ~ sQ185_spl
| ~ sQ189_spl
| sQ75_spl
| ~ sQ145_spl ),
inference(split_clause,[status(thm)],[f7843,f2756,f1036,f4618,f4170]) ).
fof(f7859,plain,
( sQ145_spl
| ~ inductive(omega) ),
inference(resolution,[status(thm)],[f2758,f150]) ).
fof(f7860,plain,
( sQ145_spl
| ~ sQ14_spl ),
inference(split_clause,[status(thm)],[f7859,f339,f2756]) ).
fof(f7870,definition,
( sQ301_spl
<=> subclass(null_class,cantor(inverse(null_class))) ),
introduced(definition,[new_symbols(definition,[sQ301_spl])],[split_symbol_definition]) ).
fof(f7872,plain,
( sQ301_spl
| ~ subclass(null_class,cantor(inverse(null_class))) ),
inference(component_clause,[status(thm)],[f7870]) ).
fof(f7877,plain,
( sQ301_spl
| ~ sQ74_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7872,f1033]) ).
fof(f7878,plain,
( sQ301_spl
| ~ sQ74_spl ),
inference(contradiction_clause,[status(thm)],[f7877]) ).
fof(f7897,plain,
! [X0,X1] :
( ~ sQ65_spl
| ~ sQ32_spl
| member(w,X1)
| ~ member(ordered_pair(null_class,y),cross_product(X0,X1)) ),
inference(paramodulation,[status(thm)],[f5327,f115]) ).
fof(f7898,plain,
( ~ sQ65_spl
| ~ sQ32_spl
| member(null_class,w)
| ~ member(ordered_pair(null_class,y),element_relation) ),
inference(paramodulation,[status(thm)],[f5327,f120]) ).
fof(f7911,plain,
! [X0,X1] :
( ~ sQ65_spl
| ~ sQ32_spl
| ~ member(ordered_pair(null_class,y),cross_product(X0,X1)) ),
inference(forward_subsumption_resolution,[status(thm)],[f7897,f434]) ).
fof(f7912,definition,
( sQ304_spl
<=> member(ordered_pair(null_class,y),element_relation) ),
introduced(definition,[new_symbols(definition,[sQ304_spl])],[split_symbol_definition]) ).
fof(f7915,plain,
( ~ sQ65_spl
| ~ sQ32_spl
| sQ87_spl
| ~ sQ304_spl ),
inference(split_clause,[status(thm)],[f7898,f7912,f1123,f433,f943]) ).
fof(f8081,definition,
( sQ312_spl
<=> ordered_pair(z,x) = null_class ),
introduced(definition,[new_symbols(definition,[sQ312_spl])],[split_symbol_definition]) ).
fof(f8082,plain,
( ~ sQ312_spl
| ordered_pair(z,x) = null_class ),
inference(component_clause,[status(thm)],[f8081]) ).
fof(f8236,plain,
! [X0,X1] :
( ~ inductive(complement(intersection(complement(X0),complement(X1))))
| member(null_class,union(X0,X1))
| ~ member(null_class,universal_class) ),
inference(resolution,[status(thm)],[f578,f5982]) ).
fof(f8260,definition,
! [X0,X1] :
( sQ321_spl
<=> member(w,union(X0,X1)) ),
introduced(definition,[new_symbols(definition,[sQ321_spl])],[split_symbol_definition]) ).
fof(f8261,plain,
! [X0,X1] :
( ~ sQ321_spl
| member(w,union(X0,X1)) ),
inference(component_clause,[status(thm)],[f8260]) ).
fof(f8264,definition,
! [X0,X1] :
( sQ322_spl
<=> ( ~ inductive(complement(intersection(complement(X0),complement(X1))))
| member(null_class,union(X0,X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ322_spl])],[split_symbol_definition]) ).
fof(f8267,plain,
( sQ322_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f8236,f219,f8264]) ).
fof(f8292,plain,
( ~ sQ321_spl
| ~ sQ32_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f8261,f434]) ).
fof(f8293,plain,
( ~ sQ321_spl
| ~ sQ32_spl ),
inference(contradiction_clause,[status(thm)],[f8292]) ).
fof(f8343,plain,
( ~ sQ312_spl
| member(singleton(z),null_class) ),
inference(paramodulation,[status(thm)],[f8082,f275]) ).
fof(f8528,plain,
! [X0] :
( ~ sQ82_spl
| ~ sQ189_spl
| ordered_pair(null_class,w) = null_class
| ~ member(X0,singleton(null_class))
| ~ member(X0,ordered_pair(null_class,w)) ),
inference(paramodulation,[status(thm)],[f1092,f7841]) ).
fof(f8532,definition,
! [X0] :
( sQ325_spl
<=> ( ~ member(X0,singleton(null_class))
| ~ member(X0,ordered_pair(null_class,w)) ) ),
introduced(definition,[new_symbols(definition,[sQ325_spl])],[split_symbol_definition]) ).
fof(f8535,plain,
( ~ sQ82_spl
| ~ sQ189_spl
| sQ77_spl
| sQ325_spl ),
inference(split_clause,[status(thm)],[f8528,f8532,f1073,f4618,f1091]) ).
fof(f8606,plain,
! [X0] :
( ~ sQ189_spl
| X0 = null_class
| intersection(diagonalise(null_class),union(X0,regular(X0))) = symmetric_difference(X0,regular(X0)) ),
inference(forward_demodulation,[status(thm)],[f6583,f584]) ).
fof(f8607,plain,
( ~ sQ82_spl
| ~ sQ189_spl
| ordered_pair(null_class,w) = null_class
| intersection(diagonalise(null_class),union(ordered_pair(null_class,w),singleton(null_class))) = symmetric_difference(ordered_pair(null_class,w),regular(ordered_pair(null_class,w))) ),
inference(paramodulation,[status(thm)],[f1092,f8606]) ).
fof(f8618,definition,
( sQ326_spl
<=> intersection(diagonalise(null_class),union(ordered_pair(null_class,w),singleton(null_class))) = symmetric_difference(ordered_pair(null_class,w),regular(ordered_pair(null_class,w))) ),
introduced(definition,[new_symbols(definition,[sQ326_spl])],[split_symbol_definition]) ).
fof(f8621,plain,
( ~ sQ82_spl
| ~ sQ189_spl
| sQ77_spl
| sQ326_spl ),
inference(split_clause,[status(thm)],[f8607,f8618,f1073,f4618,f1091]) ).
fof(f8683,plain,
( ~ sQ220_spl
| member(w,universal_class)
| unordered_pair(w,singleton(x)) = null_class ),
inference(paramodulation,[status(thm)],[f5695,f6003]) ).
fof(f8686,definition,
( sQ328_spl
<=> regular(unordered_pair(w,null_class)) = w ),
introduced(definition,[new_symbols(definition,[sQ328_spl])],[split_symbol_definition]) ).
fof(f8687,plain,
( ~ sQ328_spl
| regular(unordered_pair(w,null_class)) = w ),
inference(component_clause,[status(thm)],[f8686]) ).
fof(f8698,plain,
( ~ sQ220_spl
| sQ44_spl
| sQ222_spl ),
inference(split_clause,[status(thm)],[f8683,f5700,f527,f5694]) ).
fof(f8699,definition,
( sQ331_spl
<=> member(w,unordered_pair(w,singleton(x))) ),
introduced(definition,[new_symbols(definition,[sQ331_spl])],[split_symbol_definition]) ).
fof(f8700,plain,
( ~ sQ331_spl
| member(w,unordered_pair(w,singleton(x))) ),
inference(component_clause,[status(thm)],[f8699]) ).
fof(f8707,plain,
( ~ sQ331_spl
| ~ sQ32_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f8700,f434]) ).
fof(f8708,plain,
( ~ sQ331_spl
| ~ sQ32_spl ),
inference(contradiction_clause,[status(thm)],[f8707]) ).
fof(f8711,plain,
( ~ sQ328_spl
| member(w,universal_class)
| unordered_pair(w,null_class) = null_class ),
inference(paramodulation,[status(thm)],[f8687,f6003]) ).
fof(f8722,plain,
( ~ sQ328_spl
| sQ44_spl
| sQ229_spl ),
inference(split_clause,[status(thm)],[f8711,f6080,f527,f8686]) ).
fof(f8723,definition,
( sQ335_spl
<=> member(w,unordered_pair(w,null_class)) ),
introduced(definition,[new_symbols(definition,[sQ335_spl])],[split_symbol_definition]) ).
fof(f8724,plain,
( ~ sQ335_spl
| member(w,unordered_pair(w,null_class)) ),
inference(component_clause,[status(thm)],[f8723]) ).
fof(f8731,plain,
( ~ sQ335_spl
| ~ sQ32_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f8724,f434]) ).
fof(f8732,plain,
( ~ sQ335_spl
| ~ sQ32_spl ),
inference(contradiction_clause,[status(thm)],[f8731]) ).
fof(f8736,plain,
( ~ sQ229_spl
| member(null_class,null_class)
| ~ member(null_class,universal_class) ),
inference(paramodulation,[status(thm)],[f6081,f108]) ).
fof(f8742,plain,
( ~ sQ229_spl
| sQ89_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f8736,f219,f1176,f6080]) ).
fof(f8761,definition,
! [X0] :
( sQ338_spl
<=> ~ member(null_class,X0) ),
introduced(definition,[new_symbols(definition,[sQ338_spl])],[split_symbol_definition]) ).
fof(f8762,plain,
! [X0] :
( ~ sQ338_spl
| ~ member(null_class,X0) ),
inference(component_clause,[status(thm)],[f8761]) ).
fof(f8846,plain,
( ~ sQ189_spl
| complement(null_class) = null_class
| ~ member(regular(diagonalise(null_class)),null_class) ),
inference(paramodulation,[status(thm)],[f6583,f589]) ).
fof(f8864,definition,
( sQ340_spl
<=> member(regular(diagonalise(null_class)),null_class) ),
introduced(definition,[new_symbols(definition,[sQ340_spl])],[split_symbol_definition]) ).
fof(f8867,definition,
( sQ341_spl
<=> complement(null_class) = null_class ),
introduced(definition,[new_symbols(definition,[sQ341_spl])],[split_symbol_definition]) ).
fof(f8868,plain,
( ~ sQ341_spl
| complement(null_class) = null_class ),
inference(component_clause,[status(thm)],[f8867]) ).
fof(f8870,plain,
( ~ sQ189_spl
| sQ341_spl
| ~ sQ340_spl ),
inference(split_clause,[status(thm)],[f8846,f8864,f8867,f4618]) ).
fof(f8880,plain,
( ~ sQ341_spl
| ~ sQ189_spl
| diagonalise(null_class) = null_class ),
inference(forward_demodulation,[status(thm)],[f6583,f8868]) ).
fof(f8967,plain,
( ~ sQ189_spl
| ~ sQ341_spl
| complement(null_class) = null_class ),
inference(backward_demodulation,[status(thm)],[f8880,f6583]) ).
fof(f8978,plain,
! [X0] :
( ~ sQ189_spl
| ~ sQ341_spl
| member(X0,null_class)
| member(X0,null_class)
| ~ member(X0,universal_class) ),
inference(paramodulation,[status(thm)],[f8967,f128]) ).
fof(f8997,plain,
! [X0] :
( ~ sQ189_spl
| ~ sQ341_spl
| member(X0,null_class)
| ~ member(X0,universal_class) ),
inference(duplicate_literals_removal,[status(thm)],[f8978]) ).
fof(f8998,plain,
! [X0] :
( ~ sQ189_spl
| ~ sQ341_spl
| ~ member(X0,universal_class) ),
inference(forward_subsumption_resolution,[status(thm)],[f8997,f4832]) ).
fof(f9038,plain,
! [X0] :
( singleton(X0) = null_class
| member(X0,singleton(X0))
| singleton(X0) = null_class ),
inference(paramodulation,[status(thm)],[f264,f169]) ).
fof(f9045,plain,
! [X0] :
( member(X0,singleton(X0))
| singleton(X0) = null_class ),
inference(duplicate_literals_removal,[status(thm)],[f9038]) ).
fof(f9170,plain,
! [X0,X1] :
( ~ sQ65_spl
| ~ sQ32_spl
| ~ member(y,X1)
| ~ member(null_class,X0) ),
inference(resolution,[status(thm)],[f7911,f116]) ).
fof(f9172,plain,
( ~ sQ65_spl
| ~ sQ32_spl
| ~ member(ordered_pair(null_class,y),element_relation) ),
inference(resolution,[status(thm)],[f7911,f233]) ).
fof(f9173,plain,
( ~ sQ65_spl
| ~ sQ32_spl
| sQ27_spl
| sQ338_spl ),
inference(split_clause,[status(thm)],[f9170,f8761,f406,f433,f943]) ).
fof(f9176,plain,
( ~ sQ87_spl
| ~ sQ338_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f1124,f8762]) ).
fof(f9199,plain,
( ~ sQ87_spl
| ~ sQ338_spl ),
inference(contradiction_clause,[status(thm)],[f9176]) ).
fof(f9314,plain,
! [X0] :
( cross_product(singleton(X0),universal_class) = null_class
| ~ member(X0,domain_of(regular(cross_product(singleton(X0),universal_class))))
| null_class != null_class ),
inference(paramodulation,[status(thm)],[f613,f133]) ).
fof(f9325,definition,
! [X0] :
( sQ354_spl
<=> ( cross_product(singleton(X0),universal_class) = null_class
| ~ member(X0,domain_of(regular(cross_product(singleton(X0),universal_class)))) ) ),
introduced(definition,[new_symbols(definition,[sQ354_spl])],[split_symbol_definition]) ).
fof(f9328,plain,
( sQ354_spl
| ~ sQ53_spl ),
inference(split_clause,[status(thm)],[f9314,f684,f9325]) ).
fof(f9395,plain,
! [X0,X1] :
( ~ sQ32_spl
| subclass(intersection(ordered_pair(y,z),X0),X1)
| not_subclass_element(intersection(ordered_pair(y,z),X0),X1) = unordered_pair(w,singleton(x))
| not_subclass_element(intersection(ordered_pair(y,z),X0),X1) = null_class ),
inference(resolution,[status(thm)],[f5302,f298]) ).
fof(f9416,plain,
( ~ sQ32_spl
| ~ sQ89_spl
| sQ64_spl ),
inference(split_clause,[status(thm)],[f1201,f923,f1176,f433]) ).
fof(f9615,plain,
( ~ sQ32_spl
| unordered_pair(w,singleton(x)) = unordered_pair(w,singleton(x))
| unordered_pair(w,singleton(x)) = null_class ),
inference(resolution,[status(thm)],[f5273,f5302]) ).
fof(f9618,definition,
( sQ361_spl
<=> unordered_pair(w,singleton(x)) = unordered_pair(w,singleton(x)) ),
introduced(definition,[new_symbols(definition,[sQ361_spl])],[split_symbol_definition]) ).
fof(f9621,plain,
( ~ sQ32_spl
| sQ361_spl
| sQ222_spl ),
inference(split_clause,[status(thm)],[f9615,f5700,f9618,f433]) ).
fof(f9902,definition,
( sQ367_spl
<=> regular(omega) = unordered_pair(w,null_class) ),
introduced(definition,[new_symbols(definition,[sQ367_spl])],[split_symbol_definition]) ).
fof(f9903,plain,
( ~ sQ367_spl
| regular(omega) = unordered_pair(w,null_class) ),
inference(component_clause,[status(thm)],[f9902]) ).
fof(f9912,definition,
( sQ369_spl
<=> member(w,regular(omega)) ),
introduced(definition,[new_symbols(definition,[sQ369_spl])],[split_symbol_definition]) ).
fof(f9913,plain,
( ~ sQ369_spl
| member(w,regular(omega)) ),
inference(component_clause,[status(thm)],[f9912]) ).
fof(f9918,plain,
( ~ sQ369_spl
| ~ sQ32_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f9913,f434]) ).
fof(f9919,plain,
( ~ sQ369_spl
| ~ sQ32_spl ),
inference(contradiction_clause,[status(thm)],[f9918]) ).
fof(f9935,plain,
( ~ sQ367_spl
| member(null_class,regular(omega))
| ~ member(null_class,universal_class) ),
inference(paramodulation,[status(thm)],[f9903,f108]) ).
fof(f9940,plain,
( ~ sQ367_spl
| sQ185_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f9935,f219,f4170,f9902]) ).
fof(f9984,plain,
subclass(subset_relation,cross_product(universal_class,universal_class)),
inference(paramodulation,[status(thm)],[f1668,f6262]) ).
fof(f9985,plain,
( sQ265_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f9984,f6684]) ).
fof(f9986,plain,
sQ265_spl,
inference(contradiction_clause,[status(thm)],[f9985]) ).
fof(f10039,definition,
( sQ374_spl
<=> cross_product(universal_class,universal_class) = null_class ),
introduced(definition,[new_symbols(definition,[sQ374_spl])],[split_symbol_definition]) ).
fof(f10040,plain,
( ~ sQ374_spl
| cross_product(universal_class,universal_class) = null_class ),
inference(component_clause,[status(thm)],[f10039]) ).
fof(f10054,plain,
! [X0,X1] :
( ~ sQ374_spl
| member(ordered_pair(X0,X1),null_class)
| ~ member(X1,universal_class)
| ~ member(X0,universal_class) ),
inference(paramodulation,[status(thm)],[f10040,f116]) ).
fof(f10065,plain,
! [X0,X1] :
( ~ sQ374_spl
| ~ sQ189_spl
| ~ member(X1,universal_class)
| ~ member(X0,universal_class) ),
inference(forward_subsumption_resolution,[status(thm)],[f10054,f4832]) ).
fof(f10368,plain,
! [X0,X1] :
( ~ sQ32_spl
| subclass(intersection(X0,ordered_pair(y,z)),complement(X1))
| not_subclass_element(intersection(X0,ordered_pair(y,z)),complement(X1)) = null_class
| member(not_subclass_element(intersection(X0,ordered_pair(y,z)),complement(X1)),X1)
| ~ member(unordered_pair(w,singleton(x)),universal_class)
| subclass(intersection(X0,ordered_pair(y,z)),complement(X1)) ),
inference(paramodulation,[status(thm)],[f6445,f834]) ).
fof(f10383,definition,
! [X0,X1] :
( sQ378_spl
<=> ( subclass(intersection(X0,ordered_pair(y,z)),complement(X1))
| not_subclass_element(intersection(X0,ordered_pair(y,z)),complement(X1)) = null_class
| member(not_subclass_element(intersection(X0,ordered_pair(y,z)),complement(X1)),X1)
| subclass(intersection(X0,ordered_pair(y,z)),complement(X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ378_spl])],[split_symbol_definition]) ).
fof(f10386,definition,
( sQ379_spl
<=> member(unordered_pair(w,singleton(x)),universal_class) ),
introduced(definition,[new_symbols(definition,[sQ379_spl])],[split_symbol_definition]) ).
fof(f10388,plain,
( sQ379_spl
| ~ member(unordered_pair(w,singleton(x)),universal_class) ),
inference(component_clause,[status(thm)],[f10386]) ).
fof(f10389,plain,
( ~ sQ32_spl
| ~ sQ379_spl
| sQ378_spl ),
inference(split_clause,[status(thm)],[f10368,f10383,f10386,f433]) ).
fof(f10397,plain,
( sQ379_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f10388,f109]) ).
fof(f10398,plain,
sQ379_spl,
inference(contradiction_clause,[status(thm)],[f10397]) ).
fof(f10406,plain,
! [X0,X1] :
( ~ sQ32_spl
| subclass(intersection(ordered_pair(y,z),X0),complement(X1))
| not_subclass_element(intersection(ordered_pair(y,z),X0),complement(X1)) = null_class
| member(not_subclass_element(intersection(ordered_pair(y,z),X0),complement(X1)),X1)
| ~ member(unordered_pair(w,singleton(x)),universal_class)
| subclass(intersection(ordered_pair(y,z),X0),complement(X1)) ),
inference(paramodulation,[status(thm)],[f6446,f834]) ).
fof(f10423,definition,
! [X0,X1] :
( sQ383_spl
<=> ( subclass(intersection(ordered_pair(y,z),X0),complement(X1))
| not_subclass_element(intersection(ordered_pair(y,z),X0),complement(X1)) = null_class
| member(not_subclass_element(intersection(ordered_pair(y,z),X0),complement(X1)),X1)
| subclass(intersection(ordered_pair(y,z),X0),complement(X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ383_spl])],[split_symbol_definition]) ).
fof(f10426,plain,
( ~ sQ32_spl
| ~ sQ379_spl
| sQ383_spl ),
inference(split_clause,[status(thm)],[f10406,f10423,f10386,f433]) ).
fof(f10566,plain,
! [X0] :
( ~ sQ32_spl
| subclass(ordered_pair(y,z),complement(X0))
| not_subclass_element(ordered_pair(y,z),complement(X0)) = null_class
| member(not_subclass_element(ordered_pair(y,z),complement(X0)),X0)
| ~ member(unordered_pair(w,singleton(x)),universal_class)
| subclass(ordered_pair(y,z),complement(X0)) ),
inference(paramodulation,[status(thm)],[f6447,f834]) ).
fof(f10571,definition,
! [X0] :
( sQ385_spl
<=> ( subclass(ordered_pair(y,z),complement(X0))
| not_subclass_element(ordered_pair(y,z),complement(X0)) = null_class
| member(not_subclass_element(ordered_pair(y,z),complement(X0)),X0)
| subclass(ordered_pair(y,z),complement(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ385_spl])],[split_symbol_definition]) ).
fof(f10574,plain,
( ~ sQ32_spl
| ~ sQ379_spl
| sQ385_spl ),
inference(split_clause,[status(thm)],[f10566,f10571,f10386,f433]) ).
fof(f10718,definition,
( sQ397_spl
<=> member(w,regular(ordered_pair(y,z))) ),
introduced(definition,[new_symbols(definition,[sQ397_spl])],[split_symbol_definition]) ).
fof(f10719,plain,
( ~ sQ397_spl
| member(w,regular(ordered_pair(y,z))) ),
inference(component_clause,[status(thm)],[f10718]) ).
fof(f10724,plain,
( ~ sQ397_spl
| ~ sQ32_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f10719,f434]) ).
fof(f10725,plain,
( ~ sQ397_spl
| ~ sQ32_spl ),
inference(contradiction_clause,[status(thm)],[f10724]) ).
fof(f11099,plain,
( sQ79_spl
| ~ sQ65_spl
| ~ sQ32_spl
| singleton(null_class) != ordered_pair(null_class,y) ),
inference(backward_demodulation,[status(thm)],[f5327,f1082]) ).
fof(f11101,plain,
( sQ115_spl
| ~ sQ65_spl
| ~ sQ32_spl
| ~ member(null_class,ordered_pair(null_class,y)) ),
inference(backward_demodulation,[status(thm)],[f5327,f1969]) ).
fof(f11103,plain,
( sQ77_spl
| ~ sQ65_spl
| ~ sQ32_spl
| null_class != ordered_pair(null_class,y) ),
inference(backward_demodulation,[status(thm)],[f5327,f1075]) ).
fof(f11265,plain,
! [X0] :
( ~ sQ32_spl
| ordered_pair(y,z) = null_class
| subclass(intersection(ordered_pair(y,z),regular(ordered_pair(y,z))),X0)
| not_subclass_element(null_class,X0) = unordered_pair(w,singleton(x))
| not_subclass_element(intersection(ordered_pair(y,z),regular(ordered_pair(y,z))),X0) = null_class ),
inference(paramodulation,[status(thm)],[f170,f9395]) ).
fof(f11284,definition,
! [X0] :
( sQ402_spl
<=> ( subclass(intersection(ordered_pair(y,z),regular(ordered_pair(y,z))),X0)
| not_subclass_element(null_class,X0) = unordered_pair(w,singleton(x))
| not_subclass_element(intersection(ordered_pair(y,z),regular(ordered_pair(y,z))),X0) = null_class ) ),
introduced(definition,[new_symbols(definition,[sQ402_spl])],[split_symbol_definition]) ).
fof(f11287,plain,
( ~ sQ32_spl
| sQ254_spl
| sQ402_spl ),
inference(split_clause,[status(thm)],[f11265,f11284,f6463,f433]) ).
fof(f11327,plain,
( ~ sQ82_spl
| ~ sQ65_spl
| ~ sQ32_spl
| regular(ordered_pair(null_class,y)) = singleton(null_class) ),
inference(forward_demodulation,[status(thm)],[f5327,f1092]) ).
fof(f11328,plain,
( ~ sQ82_spl
| ~ sQ65_spl
| ~ sQ32_spl
| intersection(ordered_pair(null_class,y),singleton(null_class)) = null_class
| ordered_pair(null_class,y) = null_class ),
inference(paramodulation,[status(thm)],[f11327,f170]) ).
fof(f11330,plain,
( ~ sQ82_spl
| ~ sQ65_spl
| ~ sQ32_spl
| member(singleton(null_class),ordered_pair(null_class,y))
| ordered_pair(null_class,y) = null_class ),
inference(paramodulation,[status(thm)],[f11327,f169]) ).
fof(f11331,definition,
( sQ403_spl
<=> ordered_pair(null_class,y) = null_class ),
introduced(definition,[new_symbols(definition,[sQ403_spl])],[split_symbol_definition]) ).
fof(f11332,plain,
( ~ sQ403_spl
| ordered_pair(null_class,y) = null_class ),
inference(component_clause,[status(thm)],[f11331]) ).
fof(f11334,definition,
( sQ404_spl
<=> intersection(ordered_pair(null_class,y),singleton(null_class)) = null_class ),
introduced(definition,[new_symbols(definition,[sQ404_spl])],[split_symbol_definition]) ).
fof(f11335,plain,
( ~ sQ404_spl
| intersection(ordered_pair(null_class,y),singleton(null_class)) = null_class ),
inference(component_clause,[status(thm)],[f11334]) ).
fof(f11337,plain,
( ~ sQ82_spl
| ~ sQ65_spl
| ~ sQ32_spl
| sQ404_spl
| sQ403_spl ),
inference(split_clause,[status(thm)],[f11328,f11331,f11334,f433,f943,f1091]) ).
fof(f11339,definition,
( sQ405_spl
<=> member(singleton(null_class),ordered_pair(null_class,y)) ),
introduced(definition,[new_symbols(definition,[sQ405_spl])],[split_symbol_definition]) ).
fof(f11342,plain,
( ~ sQ82_spl
| ~ sQ65_spl
| ~ sQ32_spl
| sQ405_spl
| sQ403_spl ),
inference(split_clause,[status(thm)],[f11330,f11331,f11339,f433,f943,f1091]) ).
fof(f11343,plain,
( ~ sQ403_spl
| sQ77_spl
| ~ sQ65_spl
| ~ sQ32_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f11332,f11103]) ).
fof(f11344,plain,
( ~ sQ403_spl
| sQ77_spl
| ~ sQ65_spl
| ~ sQ32_spl ),
inference(contradiction_clause,[status(thm)],[f11343]) ).
fof(f11345,plain,
( ~ sQ32_spl
| ~ sQ65_spl
| singleton(singleton(null_class)) = ordered_pair(null_class,y) ),
inference(forward_demodulation,[status(thm)],[f5327,f1056]) ).
fof(f11355,plain,
! [X0] :
( ~ sQ32_spl
| ~ sQ65_spl
| member(singleton(null_class),domain_of(X0))
| restrict(X0,ordered_pair(null_class,y),universal_class) = null_class
| ~ member(singleton(null_class),universal_class) ),
inference(paramodulation,[status(thm)],[f11345,f134]) ).
fof(f11356,plain,
( ~ sQ32_spl
| ~ sQ65_spl
| null_class = singleton(null_class)
| ~ inductive(ordered_pair(null_class,y)) ),
inference(paramodulation,[status(thm)],[f11345,f1359]) ).
fof(f11370,definition,
( sQ406_spl
<=> singleton(null_class) = ordered_pair(null_class,y) ),
introduced(definition,[new_symbols(definition,[sQ406_spl])],[split_symbol_definition]) ).
fof(f11371,plain,
( ~ sQ406_spl
| singleton(null_class) = ordered_pair(null_class,y) ),
inference(component_clause,[status(thm)],[f11370]) ).
fof(f11375,definition,
( sQ407_spl
<=> regular(ordered_pair(null_class,y)) = singleton(null_class) ),
introduced(definition,[new_symbols(definition,[sQ407_spl])],[split_symbol_definition]) ).
fof(f11376,plain,
( ~ sQ407_spl
| regular(ordered_pair(null_class,y)) = singleton(null_class) ),
inference(component_clause,[status(thm)],[f11375]) ).
fof(f11380,definition,
! [X0] :
( sQ408_spl
<=> ( member(singleton(null_class),domain_of(X0))
| restrict(X0,ordered_pair(null_class,y),universal_class) = null_class ) ),
introduced(definition,[new_symbols(definition,[sQ408_spl])],[split_symbol_definition]) ).
fof(f11383,plain,
( ~ sQ32_spl
| ~ sQ65_spl
| sQ408_spl
| ~ sQ78_spl ),
inference(split_clause,[status(thm)],[f11355,f1076,f11380,f943,f433]) ).
fof(f11384,definition,
( sQ409_spl
<=> inductive(ordered_pair(null_class,y)) ),
introduced(definition,[new_symbols(definition,[sQ409_spl])],[split_symbol_definition]) ).
fof(f11387,plain,
( ~ sQ32_spl
| ~ sQ65_spl
| sQ60_spl
| ~ sQ409_spl ),
inference(split_clause,[status(thm)],[f11356,f11384,f891,f943,f433]) ).
fof(f11391,plain,
( ~ sQ406_spl
| sQ79_spl
| ~ sQ65_spl
| ~ sQ32_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f11371,f11099]) ).
fof(f11392,plain,
( ~ sQ406_spl
| sQ79_spl
| ~ sQ65_spl
| ~ sQ32_spl ),
inference(contradiction_clause,[status(thm)],[f11391]) ).
fof(f11400,plain,
( ~ sQ209_spl
| ~ sQ19_spl
| unordered_pair(w,singleton(x)) = unordered_pair(y,null_class) ),
inference(forward_demodulation,[status(thm)],[f887,f5386]) ).
fof(f11403,plain,
( ~ sQ209_spl
| ~ sQ19_spl
| member(singleton(x),unordered_pair(y,null_class))
| ~ member(singleton(x),universal_class) ),
inference(paramodulation,[status(thm)],[f11400,f108]) ).
fof(f11414,definition,
( sQ411_spl
<=> member(singleton(x),unordered_pair(y,null_class)) ),
introduced(definition,[new_symbols(definition,[sQ411_spl])],[split_symbol_definition]) ).
fof(f11415,plain,
( ~ sQ411_spl
| member(singleton(x),unordered_pair(y,null_class)) ),
inference(component_clause,[status(thm)],[f11414]) ).
fof(f11417,plain,
( ~ sQ209_spl
| ~ sQ19_spl
| sQ411_spl
| ~ sQ223_spl ),
inference(split_clause,[status(thm)],[f11403,f5705,f11414,f372,f5385]) ).
fof(f11418,definition,
( sQ412_spl
<=> member(w,unordered_pair(y,null_class)) ),
introduced(definition,[new_symbols(definition,[sQ412_spl])],[split_symbol_definition]) ).
fof(f11419,plain,
( ~ sQ412_spl
| member(w,unordered_pair(y,null_class)) ),
inference(component_clause,[status(thm)],[f11418]) ).
fof(f11424,plain,
( ~ sQ412_spl
| ~ sQ32_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f11419,f434]) ).
fof(f11425,plain,
( ~ sQ412_spl
| ~ sQ32_spl ),
inference(contradiction_clause,[status(thm)],[f11424]) ).
fof(f11432,plain,
( ~ sQ88_spl
| ~ sQ65_spl
| ~ sQ32_spl
| member(ordered_pair(null_class,y),element_relation) ),
inference(forward_demodulation,[status(thm)],[f5327,f1127]) ).
fof(f11433,plain,
( ~ sQ88_spl
| ~ sQ65_spl
| ~ sQ32_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f11432,f9172]) ).
fof(f11434,plain,
( ~ sQ88_spl
| ~ sQ65_spl
| ~ sQ32_spl ),
inference(contradiction_clause,[status(thm)],[f11433]) ).
fof(f11435,plain,
( ~ sQ127_spl
| ~ sQ189_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2186,f4832]) ).
fof(f11436,plain,
( ~ sQ127_spl
| ~ sQ189_spl ),
inference(contradiction_clause,[status(thm)],[f11435]) ).
fof(f11565,plain,
! [X0,X1] :
( ~ sQ32_spl
| subclass(intersection(ordered_pair(y,z),X0),X1)
| not_subclass_element(intersection(ordered_pair(y,z),X0),X1) = unordered_pair(w,singleton(x))
| not_subclass_element(intersection(ordered_pair(y,z),X0),X1) = null_class ),
inference(resolution,[status(thm)],[f5302,f298]) ).
fof(f11607,definition,
( sQ415_spl
<=> inductive(complement(diagonalise(null_class))) ),
introduced(definition,[new_symbols(definition,[sQ415_spl])],[split_symbol_definition]) ).
fof(f11701,plain,
( ~ sQ189_spl
| ~ inductive(cantor(null_class))
| member(null_class,null_class) ),
inference(paramodulation,[status(thm)],[f6287,f1841]) ).
fof(f11709,definition,
( sQ420_spl
<=> inductive(cantor(null_class)) ),
introduced(definition,[new_symbols(definition,[sQ420_spl])],[split_symbol_definition]) ).
fof(f11712,plain,
( ~ sQ189_spl
| ~ sQ420_spl
| sQ89_spl ),
inference(split_clause,[status(thm)],[f11701,f1176,f11709,f4618]) ).
fof(f11748,definition,
( sQ421_spl
<=> null_class = unordered_pair(z,singleton(x)) ),
introduced(definition,[new_symbols(definition,[sQ421_spl])],[split_symbol_definition]) ).
fof(f11749,plain,
( ~ sQ421_spl
| null_class = unordered_pair(z,singleton(x)) ),
inference(component_clause,[status(thm)],[f11748]) ).
fof(f11767,plain,
( ~ sQ421_spl
| member(singleton(x),null_class)
| ~ member(singleton(x),universal_class) ),
inference(paramodulation,[status(thm)],[f11749,f108]) ).
fof(f11778,plain,
( ~ sQ421_spl
| sQ224_spl
| ~ sQ223_spl ),
inference(split_clause,[status(thm)],[f11767,f5705,f5708,f11748]) ).
fof(f11793,plain,
( sQ220_spl
| unordered_pair(w,singleton(x)) = null_class
| regular(unordered_pair(w,singleton(x))) = w
| singleton(x) != w ),
inference(paramodulation,[status(thm)],[f850,f5696]) ).
fof(f11795,definition,
( sQ424_spl
<=> singleton(x) = w ),
introduced(definition,[new_symbols(definition,[sQ424_spl])],[split_symbol_definition]) ).
fof(f11798,plain,
( sQ222_spl
| sQ220_spl
| ~ sQ424_spl ),
inference(split_clause,[status(thm)],[f11793,f11795,f5694,f5700]) ).
fof(f11879,plain,
! [X0] :
( ~ sQ130_spl
| member(apply(choice,omega),universal_class)
| ~ inductive(X0) ),
inference(resolution,[status(thm)],[f2379,f207]) ).
fof(f11895,definition,
( sQ429_spl
<=> member(apply(choice,omega),universal_class) ),
introduced(definition,[new_symbols(definition,[sQ429_spl])],[split_symbol_definition]) ).
fof(f11898,plain,
( ~ sQ130_spl
| sQ429_spl
| sQ1_spl ),
inference(split_clause,[status(thm)],[f11879,f222,f11895,f2378]) ).
fof(f11927,plain,
( ~ sQ133_spl
| omega = null_class
| ~ inductive(complement(universal_class)) ),
inference(resolution,[status(thm)],[f2726,f6003]) ).
fof(f11928,plain,
( ~ sQ133_spl
| omega = null_class
| ~ inductive(complement(omega)) ),
inference(resolution,[status(thm)],[f2726,f169]) ).
fof(f11932,plain,
( ~ sQ133_spl
| ~ member(regular(omega),universal_class)
| ~ inductive(complement(singleton(regular(omega)))) ),
inference(resolution,[status(thm)],[f2726,f263]) ).
fof(f11933,plain,
! [X0] :
( ~ sQ133_spl
| ~ member(regular(omega),universal_class)
| ~ inductive(complement(unordered_pair(X0,regular(omega)))) ),
inference(resolution,[status(thm)],[f2726,f108]) ).
fof(f11934,plain,
! [X0] :
( ~ sQ133_spl
| ~ member(regular(omega),universal_class)
| ~ inductive(complement(unordered_pair(regular(omega),X0))) ),
inference(resolution,[status(thm)],[f2726,f106]) ).
fof(f11936,plain,
! [X0] :
( ~ sQ133_spl
| member(regular(omega),X0)
| ~ member(regular(omega),universal_class)
| ~ inductive(complement(complement(X0))) ),
inference(resolution,[status(thm)],[f2726,f128]) ).
fof(f11938,plain,
! [X0,X1] :
( ~ sQ133_spl
| member(regular(omega),union(X0,X1))
| ~ member(regular(omega),universal_class)
| ~ inductive(complement(intersection(complement(X0),complement(X1)))) ),
inference(resolution,[status(thm)],[f2726,f578]) ).
fof(f11941,plain,
( ~ sQ133_spl
| sQ75_spl
| ~ sQ54_spl ),
inference(split_clause,[status(thm)],[f11927,f687,f1036,f2389]) ).
fof(f11942,definition,
( sQ430_spl
<=> inductive(complement(omega)) ),
introduced(definition,[new_symbols(definition,[sQ430_spl])],[split_symbol_definition]) ).
fof(f11945,plain,
( ~ sQ133_spl
| sQ75_spl
| ~ sQ430_spl ),
inference(split_clause,[status(thm)],[f11928,f11942,f1036,f2389]) ).
fof(f11947,definition,
( sQ431_spl
<=> inductive(complement(singleton(regular(omega)))) ),
introduced(definition,[new_symbols(definition,[sQ431_spl])],[split_symbol_definition]) ).
fof(f11950,definition,
( sQ432_spl
<=> singleton(regular(omega)) = null_class ),
introduced(definition,[new_symbols(definition,[sQ432_spl])],[split_symbol_definition]) ).
fof(f11951,plain,
( ~ sQ432_spl
| singleton(regular(omega)) = null_class ),
inference(component_clause,[status(thm)],[f11950]) ).
fof(f11954,plain,
( ~ sQ133_spl
| ~ sQ144_spl
| ~ sQ431_spl ),
inference(split_clause,[status(thm)],[f11932,f11947,f2750,f2389]) ).
fof(f11955,definition,
! [X0] :
( sQ433_spl
<=> ~ inductive(complement(unordered_pair(X0,regular(omega)))) ),
introduced(definition,[new_symbols(definition,[sQ433_spl])],[split_symbol_definition]) ).
fof(f11958,plain,
( ~ sQ133_spl
| ~ sQ144_spl
| sQ433_spl ),
inference(split_clause,[status(thm)],[f11933,f11955,f2750,f2389]) ).
fof(f11959,definition,
! [X0] :
( sQ434_spl
<=> ~ inductive(complement(unordered_pair(regular(omega),X0))) ),
introduced(definition,[new_symbols(definition,[sQ434_spl])],[split_symbol_definition]) ).
fof(f11962,plain,
( ~ sQ133_spl
| ~ sQ144_spl
| sQ434_spl ),
inference(split_clause,[status(thm)],[f11934,f11959,f2750,f2389]) ).
fof(f11963,definition,
! [X0] :
( sQ435_spl
<=> ( member(regular(omega),X0)
| ~ inductive(complement(complement(X0))) ) ),
introduced(definition,[new_symbols(definition,[sQ435_spl])],[split_symbol_definition]) ).
fof(f11966,plain,
( ~ sQ133_spl
| ~ sQ144_spl
| sQ435_spl ),
inference(split_clause,[status(thm)],[f11936,f11963,f2750,f2389]) ).
fof(f11967,definition,
! [X0,X1] :
( sQ436_spl
<=> ( member(regular(omega),union(X0,X1))
| ~ inductive(complement(intersection(complement(X0),complement(X1)))) ) ),
introduced(definition,[new_symbols(definition,[sQ436_spl])],[split_symbol_definition]) ).
fof(f11970,plain,
( ~ sQ133_spl
| ~ sQ144_spl
| sQ436_spl ),
inference(split_clause,[status(thm)],[f11938,f11967,f2750,f2389]) ).
fof(f11984,plain,
( ~ sQ432_spl
| member(regular(omega),null_class)
| ~ member(regular(omega),universal_class) ),
inference(paramodulation,[status(thm)],[f11951,f263]) ).
fof(f11996,definition,
( sQ437_spl
<=> member(regular(omega),null_class) ),
introduced(definition,[new_symbols(definition,[sQ437_spl])],[split_symbol_definition]) ).
fof(f11997,plain,
( ~ sQ437_spl
| member(regular(omega),null_class) ),
inference(component_clause,[status(thm)],[f11996]) ).
fof(f12010,plain,
( ~ sQ432_spl
| sQ437_spl
| ~ sQ144_spl ),
inference(split_clause,[status(thm)],[f11984,f2750,f11996,f11950]) ).
fof(f12019,plain,
( ~ sQ437_spl
| ~ sQ189_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f11997,f4832]) ).
fof(f12020,plain,
( ~ sQ437_spl
| ~ sQ189_spl ),
inference(contradiction_clause,[status(thm)],[f12019]) ).
fof(f12055,definition,
( sQ444_spl
<=> member(w,regular(null_class)) ),
introduced(definition,[new_symbols(definition,[sQ444_spl])],[split_symbol_definition]) ).
fof(f12056,plain,
( ~ sQ444_spl
| member(w,regular(null_class)) ),
inference(component_clause,[status(thm)],[f12055]) ).
fof(f12061,plain,
( ~ sQ444_spl
| ~ sQ32_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f12056,f434]) ).
fof(f12062,plain,
( ~ sQ444_spl
| ~ sQ32_spl ),
inference(contradiction_clause,[status(thm)],[f12061]) ).
fof(f12239,definition,
( sQ452_spl
<=> x = w ),
introduced(definition,[new_symbols(definition,[sQ452_spl])],[split_symbol_definition]) ).
fof(f12240,plain,
( ~ sQ452_spl
| x = w ),
inference(component_clause,[status(thm)],[f12239]) ).
fof(f12243,definition,
! [X0] :
( sQ453_spl
<=> ( member(X0,universal_class)
| x = X0 ) ),
introduced(definition,[new_symbols(definition,[sQ453_spl])],[split_symbol_definition]) ).
fof(f12244,plain,
! [X0] :
( ~ sQ453_spl
| member(X0,universal_class)
| x = X0 ),
inference(component_clause,[status(thm)],[f12243]) ).
fof(f12281,plain,
! [X0] :
( ~ sQ32_spl
| ~ sQ452_spl
| ~ member(x,X0) ),
inference(backward_demodulation,[status(thm)],[f12240,f434]) ).
fof(f12290,plain,
( ~ sQ32_spl
| ~ sQ452_spl
| sQ35_spl ),
inference(split_clause,[status(thm)],[f12281,f443,f12239,f433]) ).
fof(f12895,plain,
( ~ sQ32_spl
| ~ sQ453_spl
| x = w ),
inference(resolution,[status(thm)],[f12244,f434]) ).
fof(f12902,plain,
( ~ sQ32_spl
| ~ sQ453_spl
| sQ452_spl ),
inference(split_clause,[status(thm)],[f12895,f12239,f12243,f433]) ).
fof(f13377,plain,
( ~ sQ411_spl
| singleton(x) = null_class
| singleton(x) = y ),
inference(resolution,[status(thm)],[f11415,f104]) ).
fof(f13380,definition,
( sQ463_spl
<=> singleton(x) = y ),
introduced(definition,[new_symbols(definition,[sQ463_spl])],[split_symbol_definition]) ).
fof(f13381,plain,
( ~ sQ463_spl
| singleton(x) = y ),
inference(component_clause,[status(thm)],[f13380]) ).
fof(f13383,plain,
( ~ sQ411_spl
| sQ219_spl
| sQ463_spl ),
inference(split_clause,[status(thm)],[f13377,f13380,f5690,f11414]) ).
fof(f13405,plain,
( ~ sQ463_spl
| member(y,universal_class) ),
inference(paramodulation,[status(thm)],[f13381,f208]) ).
fof(f13459,plain,
( ~ sQ219_spl
| member(x,null_class)
| ~ member(x,universal_class) ),
inference(paramodulation,[status(thm)],[f5691,f263]) ).
fof(f13473,definition,
( sQ465_spl
<=> member(x,null_class) ),
introduced(definition,[new_symbols(definition,[sQ465_spl])],[split_symbol_definition]) ).
fof(f13474,plain,
( ~ sQ465_spl
| member(x,null_class) ),
inference(component_clause,[status(thm)],[f13473]) ).
fof(f13476,plain,
( ~ sQ219_spl
| sQ465_spl
| ~ sQ96_spl ),
inference(split_clause,[status(thm)],[f13459,f1315,f13473,f5690]) ).
fof(f13480,plain,
( ~ sQ465_spl
| ~ sQ189_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f13474,f4832]) ).
fof(f13481,plain,
( ~ sQ465_spl
| ~ sQ189_spl ),
inference(contradiction_clause,[status(thm)],[f13480]) ).
fof(f13562,plain,
! [X0] :
( ~ inductive(complement(image(element_relation,complement(X0))))
| member(null_class,power_class(X0))
| ~ member(null_class,universal_class) ),
inference(resolution,[status(thm)],[f1276,f5982]) ).
fof(f13581,definition,
! [X0] :
( sQ466_spl
<=> ( ~ inductive(complement(image(element_relation,complement(X0))))
| member(null_class,power_class(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ466_spl])],[split_symbol_definition]) ).
fof(f13584,plain,
( sQ466_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f13562,f219,f13581]) ).
fof(f13585,definition,
! [X0] :
( sQ467_spl
<=> member(w,power_class(X0)) ),
introduced(definition,[new_symbols(definition,[sQ467_spl])],[split_symbol_definition]) ).
fof(f13586,plain,
! [X0] :
( ~ sQ467_spl
| member(w,power_class(X0)) ),
inference(component_clause,[status(thm)],[f13585]) ).
fof(f13601,plain,
( ~ sQ467_spl
| ~ sQ32_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f13586,f434]) ).
fof(f13602,plain,
( ~ sQ467_spl
| ~ sQ32_spl ),
inference(contradiction_clause,[status(thm)],[f13601]) ).
fof(f13623,plain,
( ~ sQ463_spl
| sQ23_spl ),
inference(split_clause,[status(thm)],[f13405,f390,f13380]) ).
fof(f13630,plain,
( ~ sQ312_spl
| ~ sQ189_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f8343,f4832]) ).
fof(f13631,plain,
( ~ sQ312_spl
| ~ sQ189_spl ),
inference(contradiction_clause,[status(thm)],[f13630]) ).
fof(f13705,plain,
! [X0,X1,X2] :
( ~ member(null_class,universal_class)
| ~ member(X0,universal_class)
| ~ inductive(image(X1,image(X2,singleton(X0))))
| member(ordered_pair(X0,null_class),compose(X1,X2)) ),
inference(resolution,[status(thm)],[f1369,f116]) ).
fof(f13706,definition,
! [X0,X1,X2] :
( sQ474_spl
<=> ( ~ member(X0,universal_class)
| ~ inductive(image(X1,image(X2,singleton(X0))))
| member(ordered_pair(X0,null_class),compose(X1,X2)) ) ),
introduced(definition,[new_symbols(definition,[sQ474_spl])],[split_symbol_definition]) ).
fof(f13709,plain,
( ~ sQ0_spl
| sQ474_spl ),
inference(split_clause,[status(thm)],[f13705,f13706,f219]) ).
fof(f14097,plain,
! [X0] :
( ~ sQ189_spl
| member(apply(choice,null_class),null_class)
| intersection(null_class,X0) = null_class
| ~ member(intersection(null_class,X0),universal_class) ),
inference(paramodulation,[status(thm)],[f6145,f1645]) ).
fof(f14117,definition,
! [X0] :
( sQ489_spl
<=> ( intersection(null_class,X0) = null_class
| ~ member(intersection(null_class,X0),universal_class) ) ),
introduced(definition,[new_symbols(definition,[sQ489_spl])],[split_symbol_definition]) ).
fof(f14120,definition,
( sQ490_spl
<=> member(apply(choice,null_class),null_class) ),
introduced(definition,[new_symbols(definition,[sQ490_spl])],[split_symbol_definition]) ).
fof(f14121,plain,
( ~ sQ490_spl
| member(apply(choice,null_class),null_class) ),
inference(component_clause,[status(thm)],[f14120]) ).
fof(f14123,plain,
( ~ sQ189_spl
| sQ490_spl
| sQ489_spl ),
inference(split_clause,[status(thm)],[f14097,f14117,f14120,f4618]) ).
fof(f14145,plain,
( ~ sQ490_spl
| ~ sQ189_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f14121,f4832]) ).
fof(f14146,plain,
( ~ sQ490_spl
| ~ sQ189_spl ),
inference(contradiction_clause,[status(thm)],[f14145]) ).
fof(f14177,plain,
! [X0] :
( ~ sQ189_spl
| member(apply(choice,null_class),null_class)
| intersection(X0,null_class) = null_class
| ~ member(intersection(X0,null_class),universal_class) ),
inference(paramodulation,[status(thm)],[f6346,f1646]) ).
fof(f14199,definition,
! [X0] :
( sQ491_spl
<=> ( intersection(X0,null_class) = null_class
| ~ member(intersection(X0,null_class),universal_class) ) ),
introduced(definition,[new_symbols(definition,[sQ491_spl])],[split_symbol_definition]) ).
fof(f14202,plain,
( ~ sQ189_spl
| sQ490_spl
| sQ491_spl ),
inference(split_clause,[status(thm)],[f14177,f14199,f14120,f4618]) ).
fof(f14387,plain,
( ~ sQ189_spl
| ~ sQ341_spl
| sQ288_spl ),
inference(split_clause,[status(thm)],[f8998,f7319,f8867,f4618]) ).
fof(f14755,definition,
( sQ507_spl
<=> member(singleton(z),universal_class) ),
introduced(definition,[new_symbols(definition,[sQ507_spl])],[split_symbol_definition]) ).
fof(f14757,plain,
( sQ507_spl
| ~ member(singleton(z),universal_class) ),
inference(component_clause,[status(thm)],[f14755]) ).
fof(f14758,definition,
( sQ508_spl
<=> member(singleton(z),null_class) ),
introduced(definition,[new_symbols(definition,[sQ508_spl])],[split_symbol_definition]) ).
fof(f14759,plain,
( ~ sQ508_spl
| member(singleton(z),null_class) ),
inference(component_clause,[status(thm)],[f14758]) ).
fof(f14765,plain,
( ~ sQ508_spl
| ~ sQ189_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f14759,f4832]) ).
fof(f14766,plain,
( ~ sQ508_spl
| ~ sQ189_spl ),
inference(contradiction_clause,[status(thm)],[f14765]) ).
fof(f14767,plain,
( sQ507_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f14757,f208]) ).
fof(f14768,plain,
sQ507_spl,
inference(contradiction_clause,[status(thm)],[f14767]) ).
fof(f15146,plain,
( ~ sQ205_spl
| member(singleton(z),null_class)
| ~ member(singleton(z),universal_class) ),
inference(paramodulation,[status(thm)],[f5296,f108]) ).
fof(f15156,plain,
( ~ sQ205_spl
| sQ508_spl
| ~ sQ507_spl ),
inference(split_clause,[status(thm)],[f15146,f14755,f14758,f5295]) ).
fof(f15725,plain,
! [X0] :
( ~ sQ133_spl
| member(regular(omega),power_class(X0))
| ~ member(regular(omega),universal_class)
| ~ inductive(complement(image(element_relation,complement(X0)))) ),
inference(resolution,[status(thm)],[f4113,f1276]) ).
fof(f15737,definition,
! [X0] :
( sQ536_spl
<=> ( member(regular(omega),power_class(X0))
| ~ inductive(complement(image(element_relation,complement(X0)))) ) ),
introduced(definition,[new_symbols(definition,[sQ536_spl])],[split_symbol_definition]) ).
fof(f15740,plain,
( ~ sQ133_spl
| ~ sQ144_spl
| sQ536_spl ),
inference(split_clause,[status(thm)],[f15725,f15737,f2750,f2389]) ).
fof(f15906,plain,
! [X0] :
( ~ sQ189_spl
| X0 = null_class
| intersection(diagonalise(null_class),union(X0,regular(X0))) = symmetric_difference(X0,regular(X0)) ),
inference(forward_demodulation,[status(thm)],[f6583,f1828]) ).
fof(f15911,plain,
( ~ sQ407_spl
| ~ sQ189_spl
| ordered_pair(null_class,y) = null_class
| intersection(diagonalise(null_class),union(ordered_pair(null_class,y),singleton(null_class))) = symmetric_difference(ordered_pair(null_class,y),regular(ordered_pair(null_class,y))) ),
inference(paramodulation,[status(thm)],[f11376,f15906]) ).
fof(f15916,plain,
! [X0] :
( ~ sQ189_spl
| X0 = null_class
| member(null_class,diagonalise(null_class))
| ~ inductive(symmetric_difference(X0,regular(X0))) ),
inference(paramodulation,[status(thm)],[f15906,f7185]) ).
fof(f15934,definition,
( sQ546_spl
<=> intersection(diagonalise(null_class),union(ordered_pair(null_class,y),singleton(null_class))) = symmetric_difference(ordered_pair(null_class,y),regular(ordered_pair(null_class,y))) ),
introduced(definition,[new_symbols(definition,[sQ546_spl])],[split_symbol_definition]) ).
fof(f15937,plain,
( ~ sQ407_spl
| ~ sQ189_spl
| sQ403_spl
| sQ546_spl ),
inference(split_clause,[status(thm)],[f15911,f15934,f11331,f4618,f11375]) ).
fof(f15938,definition,
! [X0] :
( sQ547_spl
<=> ( X0 = null_class
| ~ inductive(symmetric_difference(X0,regular(X0))) ) ),
introduced(definition,[new_symbols(definition,[sQ547_spl])],[split_symbol_definition]) ).
fof(f15939,plain,
! [X0] :
( ~ sQ547_spl
| X0 = null_class
| ~ inductive(symmetric_difference(X0,regular(X0))) ),
inference(component_clause,[status(thm)],[f15938]) ).
fof(f15941,definition,
( sQ548_spl
<=> member(null_class,diagonalise(null_class)) ),
introduced(definition,[new_symbols(definition,[sQ548_spl])],[split_symbol_definition]) ).
fof(f15944,plain,
( ~ sQ189_spl
| sQ548_spl
| sQ547_spl ),
inference(split_clause,[status(thm)],[f15916,f15938,f15941,f4618]) ).
fof(f15953,plain,
! [X0] :
( ~ sQ32_spl
| ~ sQ65_spl
| X0 = singleton(null_class)
| ~ member(X0,ordered_pair(null_class,y)) ),
inference(forward_demodulation,[status(thm)],[f5327,f1068]) ).
fof(f15960,plain,
( ~ sQ32_spl
| ~ sQ65_spl
| ordered_pair(null_class,y) = null_class
| ~ member(ordered_pair(null_class,y),universal_class)
| apply(choice,ordered_pair(null_class,y)) = singleton(null_class) ),
inference(resolution,[status(thm)],[f15953,f173]) ).
fof(f15966,plain,
( ~ sQ32_spl
| ~ sQ65_spl
| ordered_pair(null_class,y) = null_class
| regular(ordered_pair(null_class,y)) = singleton(null_class) ),
inference(resolution,[status(thm)],[f15953,f169]) ).
fof(f15969,definition,
( sQ549_spl
<=> apply(choice,ordered_pair(null_class,y)) = singleton(null_class) ),
introduced(definition,[new_symbols(definition,[sQ549_spl])],[split_symbol_definition]) ).
fof(f15972,definition,
( sQ550_spl
<=> member(ordered_pair(null_class,y),universal_class) ),
introduced(definition,[new_symbols(definition,[sQ550_spl])],[split_symbol_definition]) ).
fof(f15974,plain,
( sQ550_spl
| ~ member(ordered_pair(null_class,y),universal_class) ),
inference(component_clause,[status(thm)],[f15972]) ).
fof(f15975,plain,
( ~ sQ32_spl
| ~ sQ65_spl
| sQ403_spl
| ~ sQ550_spl
| sQ549_spl ),
inference(split_clause,[status(thm)],[f15960,f15969,f15972,f11331,f943,f433]) ).
fof(f15976,plain,
( ~ sQ32_spl
| ~ sQ65_spl
| sQ403_spl
| sQ407_spl ),
inference(split_clause,[status(thm)],[f15966,f11375,f11331,f943,f433]) ).
fof(f15977,plain,
( sQ550_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f15974,f272]) ).
fof(f15978,plain,
sQ550_spl,
inference(contradiction_clause,[status(thm)],[f15977]) ).
fof(f16033,plain,
( ~ sQ407_spl
| ~ sQ547_spl
| ordered_pair(null_class,y) = null_class
| ~ inductive(symmetric_difference(ordered_pair(null_class,y),singleton(null_class))) ),
inference(paramodulation,[status(thm)],[f11376,f15939]) ).
fof(f16038,definition,
( sQ551_spl
<=> inductive(symmetric_difference(ordered_pair(null_class,y),singleton(null_class))) ),
introduced(definition,[new_symbols(definition,[sQ551_spl])],[split_symbol_definition]) ).
fof(f16041,plain,
( ~ sQ407_spl
| ~ sQ547_spl
| sQ403_spl
| ~ sQ551_spl ),
inference(split_clause,[status(thm)],[f16033,f16038,f11331,f15938,f11375]) ).
fof(f16042,plain,
! [X0,X1] :
( ~ sQ189_spl
| X1 = null_class
| ~ member(X0,regular(X1))
| ~ member(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f1829,f4832]) ).
fof(f16060,plain,
! [X0] :
( ~ sQ407_spl
| ~ sQ189_spl
| ordered_pair(null_class,y) = null_class
| ~ member(X0,singleton(null_class))
| ~ member(X0,ordered_pair(null_class,y)) ),
inference(paramodulation,[status(thm)],[f11376,f16042]) ).
fof(f16068,definition,
! [X0] :
( sQ552_spl
<=> ( ~ member(X0,singleton(null_class))
| ~ member(X0,ordered_pair(null_class,y)) ) ),
introduced(definition,[new_symbols(definition,[sQ552_spl])],[split_symbol_definition]) ).
fof(f16071,plain,
( ~ sQ407_spl
| ~ sQ189_spl
| sQ403_spl
| sQ552_spl ),
inference(split_clause,[status(thm)],[f16060,f16068,f11331,f4618,f11375]) ).
fof(f16077,definition,
( sQ553_spl
<=> subclass(domain_of(null_class),range_of(null_class)) ),
introduced(definition,[new_symbols(definition,[sQ553_spl])],[split_symbol_definition]) ).
fof(f16079,plain,
( sQ553_spl
| ~ subclass(domain_of(null_class),range_of(null_class)) ),
inference(component_clause,[status(thm)],[f16077]) ).
fof(f16094,plain,
( sQ553_spl
| ~ sQ189_spl
| ~ subclass(null_class,range_of(null_class)) ),
inference(forward_demodulation,[status(thm)],[f6287,f16079]) ).
fof(f16095,plain,
( sQ553_spl
| ~ sQ189_spl
| ~ sQ74_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f16094,f1033]) ).
fof(f16096,plain,
( sQ553_spl
| ~ sQ189_spl
| ~ sQ74_spl ),
inference(contradiction_clause,[status(thm)],[f16095]) ).
fof(f16194,plain,
( ~ sQ79_spl
| ~ sQ65_spl
| ~ sQ32_spl
| singleton(null_class) = ordered_pair(null_class,y) ),
inference(forward_demodulation,[status(thm)],[f5327,f1081]) ).
fof(f16214,plain,
! [X0] :
( ~ sQ32_spl
| ~ sQ209_spl
| X0 = unordered_pair(y,singleton(z))
| X0 = null_class
| ~ member(X0,ordered_pair(y,z)) ),
inference(backward_demodulation,[status(thm)],[f5386,f5302]) ).
fof(f16220,plain,
( ~ sQ209_spl
| null_class = singleton(x)
| null_class = w
| ~ inductive(unordered_pair(y,singleton(z))) ),
inference(paramodulation,[status(thm)],[f5386,f4003]) ).
fof(f16221,plain,
( ~ sQ209_spl
| regular(unordered_pair(y,singleton(z))) = singleton(x)
| regular(unordered_pair(w,singleton(x))) = w
| unordered_pair(w,singleton(x)) = null_class ),
inference(paramodulation,[status(thm)],[f5386,f1681]) ).
fof(f16228,definition,
( sQ565_spl
<=> unordered_pair(w,null_class) = unordered_pair(y,singleton(z)) ),
introduced(definition,[new_symbols(definition,[sQ565_spl])],[split_symbol_definition]) ).
fof(f16235,definition,
( sQ566_spl
<=> inductive(unordered_pair(y,singleton(z))) ),
introduced(definition,[new_symbols(definition,[sQ566_spl])],[split_symbol_definition]) ).
fof(f16238,plain,
( ~ sQ209_spl
| sQ219_spl
| sQ64_spl
| ~ sQ566_spl ),
inference(split_clause,[status(thm)],[f16220,f16235,f923,f5690,f5385]) ).
fof(f16239,definition,
( sQ567_spl
<=> regular(unordered_pair(y,singleton(z))) = singleton(x) ),
introduced(definition,[new_symbols(definition,[sQ567_spl])],[split_symbol_definition]) ).
fof(f16240,plain,
( ~ sQ567_spl
| regular(unordered_pair(y,singleton(z))) = singleton(x) ),
inference(component_clause,[status(thm)],[f16239]) ).
fof(f16242,plain,
( ~ sQ209_spl
| sQ567_spl
| sQ220_spl
| sQ222_spl ),
inference(split_clause,[status(thm)],[f16221,f5700,f5694,f16239,f5385]) ).
fof(f16250,definition,
( sQ570_spl
<=> member(singleton(x),unordered_pair(y,singleton(z))) ),
introduced(definition,[new_symbols(definition,[sQ570_spl])],[split_symbol_definition]) ).
fof(f16251,plain,
( ~ sQ570_spl
| member(singleton(x),unordered_pair(y,singleton(z))) ),
inference(component_clause,[status(thm)],[f16250]) ).
fof(f16254,definition,
( sQ571_spl
<=> member(w,unordered_pair(y,singleton(z))) ),
introduced(definition,[new_symbols(definition,[sQ571_spl])],[split_symbol_definition]) ).
fof(f16255,plain,
( ~ sQ571_spl
| member(w,unordered_pair(y,singleton(z))) ),
inference(component_clause,[status(thm)],[f16254]) ).
fof(f16261,plain,
( ~ sQ571_spl
| ~ sQ32_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f16255,f434]) ).
fof(f16262,plain,
( ~ sQ571_spl
| ~ sQ32_spl ),
inference(contradiction_clause,[status(thm)],[f16261]) ).
fof(f16273,plain,
( sQ115_spl
| ~ sQ65_spl
| ~ sQ32_spl
| ~ sQ79_spl
| ~ member(null_class,singleton(null_class)) ),
inference(backward_demodulation,[status(thm)],[f16194,f11101]) ).
fof(f16293,plain,
( sQ115_spl
| ~ sQ65_spl
| ~ sQ32_spl
| ~ sQ79_spl
| ~ sQ116_spl ),
inference(split_clause,[status(thm)],[f16273,f1983,f1080,f433,f943,f1967]) ).
fof(f16314,plain,
( ~ sQ32_spl
| ~ sQ209_spl
| unordered_pair(y,singleton(z)) = unordered_pair(y,singleton(z))
| unordered_pair(y,singleton(z)) = null_class ),
inference(resolution,[status(thm)],[f16214,f2481]) ).
fof(f16329,definition,
( sQ573_spl
<=> unordered_pair(y,singleton(z)) = unordered_pair(y,singleton(z)) ),
introduced(definition,[new_symbols(definition,[sQ573_spl])],[split_symbol_definition]) ).
fof(f16332,plain,
( ~ sQ32_spl
| ~ sQ209_spl
| sQ573_spl
| sQ205_spl ),
inference(split_clause,[status(thm)],[f16314,f5295,f16329,f5385,f433]) ).
fof(f16333,definition,
( sQ574_spl
<=> singleton(y) = unordered_pair(y,singleton(z)) ),
introduced(definition,[new_symbols(definition,[sQ574_spl])],[split_symbol_definition]) ).
fof(f16334,plain,
( ~ sQ574_spl
| singleton(y) = unordered_pair(y,singleton(z)) ),
inference(component_clause,[status(thm)],[f16333]) ).
fof(f16347,plain,
( ~ sQ574_spl
| ~ sQ65_spl
| null_class = unordered_pair(y,singleton(z)) ),
inference(forward_demodulation,[status(thm)],[f944,f16334]) ).
fof(f16348,plain,
( ~ sQ574_spl
| ~ sQ65_spl
| sQ205_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f16347,f5297]) ).
fof(f16349,plain,
( ~ sQ574_spl
| ~ sQ65_spl
| sQ205_spl ),
inference(contradiction_clause,[status(thm)],[f16348]) ).
fof(f16374,definition,
( sQ577_spl
<=> member(unordered_pair(y,singleton(z)),universal_class) ),
introduced(definition,[new_symbols(definition,[sQ577_spl])],[split_symbol_definition]) ).
fof(f16376,plain,
( sQ577_spl
| ~ member(unordered_pair(y,singleton(z)),universal_class) ),
inference(component_clause,[status(thm)],[f16374]) ).
fof(f16422,plain,
! [X0] :
( ~ sQ189_spl
| null_class = intersection(null_class,X0)
| ~ subclass(null_class,null_class) ),
inference(paramodulation,[status(thm)],[f6145,f6258]) ).
fof(f16442,plain,
( ~ sQ189_spl
| sQ235_spl
| ~ sQ94_spl ),
inference(split_clause,[status(thm)],[f16422,f1302,f6250,f4618]) ).
fof(f16495,plain,
! [X0] :
( ~ sQ236_spl
| ~ sQ189_spl
| member(X0,null_class)
| ~ member(X0,universal_class) ),
inference(forward_demodulation,[status(thm)],[f6287,f6274]) ).
fof(f16497,plain,
! [X0,X1] :
( ~ sQ236_spl
| ~ sQ189_spl
| ~ member(X0,X1) ),
inference(backward_subsumption_resolution,[status(thm)],[f207,f16518]) ).
fof(f16518,plain,
! [X0] :
( ~ sQ236_spl
| ~ sQ189_spl
| ~ member(X0,universal_class) ),
inference(forward_subsumption_resolution,[status(thm)],[f16495,f4832]) ).
fof(f16528,plain,
( ~ sQ236_spl
| ~ sQ189_spl
| sQ20_spl ),
inference(split_clause,[status(thm)],[f16497,f376,f4618,f6273]) ).
fof(f16670,plain,
! [X0,X1] :
( ~ sQ32_spl
| ~ sQ209_spl
| subclass(intersection(ordered_pair(y,z),X0),X1)
| not_subclass_element(intersection(ordered_pair(y,z),X0),X1) = unordered_pair(y,singleton(z))
| not_subclass_element(intersection(ordered_pair(y,z),X0),X1) = null_class ),
inference(forward_demodulation,[status(thm)],[f5386,f11565]) ).
fof(f16673,plain,
! [X0] :
( ~ sQ32_spl
| ~ sQ209_spl
| ordered_pair(y,z) = null_class
| subclass(intersection(ordered_pair(y,z),regular(ordered_pair(y,z))),X0)
| not_subclass_element(null_class,X0) = unordered_pair(y,singleton(z))
| not_subclass_element(intersection(ordered_pair(y,z),regular(ordered_pair(y,z))),X0) = null_class ),
inference(paramodulation,[status(thm)],[f170,f16670]) ).
fof(f16686,definition,
! [X0] :
( sQ580_spl
<=> ( subclass(intersection(ordered_pair(y,z),regular(ordered_pair(y,z))),X0)
| not_subclass_element(null_class,X0) = unordered_pair(y,singleton(z))
| not_subclass_element(intersection(ordered_pair(y,z),regular(ordered_pair(y,z))),X0) = null_class ) ),
introduced(definition,[new_symbols(definition,[sQ580_spl])],[split_symbol_definition]) ).
fof(f16689,plain,
( ~ sQ32_spl
| ~ sQ209_spl
| sQ254_spl
| sQ580_spl ),
inference(split_clause,[status(thm)],[f16673,f16686,f6463,f5385,f433]) ).
fof(f16939,definition,
( sQ585_spl
<=> member(unordered_pair(w,null_class),universal_class) ),
introduced(definition,[new_symbols(definition,[sQ585_spl])],[split_symbol_definition]) ).
fof(f16941,plain,
( sQ585_spl
| ~ member(unordered_pair(w,null_class),universal_class) ),
inference(component_clause,[status(thm)],[f16939]) ).
fof(f16956,plain,
( sQ585_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f16941,f109]) ).
fof(f16957,plain,
sQ585_spl,
inference(contradiction_clause,[status(thm)],[f16956]) ).
fof(f17096,plain,
! [X0] :
( ~ sQ189_spl
| null_class = intersection(X0,null_class)
| ~ subclass(null_class,null_class) ),
inference(paramodulation,[status(thm)],[f6346,f6497]) ).
fof(f17116,plain,
( ~ sQ189_spl
| sQ257_spl
| ~ sQ94_spl ),
inference(split_clause,[status(thm)],[f17096,f1302,f6490,f4618]) ).
fof(f17454,plain,
! [X0] :
( ~ sQ74_spl
| null_class = intersection(X0,null_class) ),
inference(resolution,[status(thm)],[f1033,f6497]) ).
fof(f17455,plain,
! [X0] :
( ~ sQ74_spl
| null_class = intersection(null_class,X0) ),
inference(resolution,[status(thm)],[f1033,f6258]) ).
fof(f17485,definition,
( sQ599_spl
<=> member(w,apply(choice,omega)) ),
introduced(definition,[new_symbols(definition,[sQ599_spl])],[split_symbol_definition]) ).
fof(f17486,plain,
( ~ sQ599_spl
| member(w,apply(choice,omega)) ),
inference(component_clause,[status(thm)],[f17485]) ).
fof(f17495,plain,
( ~ sQ599_spl
| ~ sQ32_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f17486,f434]) ).
fof(f17496,plain,
( ~ sQ599_spl
| ~ sQ32_spl ),
inference(contradiction_clause,[status(thm)],[f17495]) ).
fof(f17622,plain,
( sQ94_spl
| ~ sQ74_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1304,f1033]) ).
fof(f17623,plain,
( sQ94_spl
| ~ sQ74_spl ),
inference(contradiction_clause,[status(thm)],[f17622]) ).
fof(f18363,definition,
( sQ608_spl
<=> member(intersection(ordered_pair(y,z),null_class),universal_class) ),
introduced(definition,[new_symbols(definition,[sQ608_spl])],[split_symbol_definition]) ).
fof(f18365,plain,
( sQ608_spl
| ~ member(intersection(ordered_pair(y,z),null_class),universal_class) ),
inference(component_clause,[status(thm)],[f18363]) ).
fof(f18381,plain,
( sQ608_spl
| ~ sQ74_spl
| ~ member(null_class,universal_class) ),
inference(forward_demodulation,[status(thm)],[f17454,f18365]) ).
fof(f18382,plain,
( sQ608_spl
| ~ sQ74_spl
| ~ sQ49_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f18381,f777]) ).
fof(f18383,plain,
( sQ608_spl
| ~ sQ74_spl
| ~ sQ49_spl ),
inference(contradiction_clause,[status(thm)],[f18382]) ).
fof(f18388,definition,
( sQ612_spl
<=> member(intersection(null_class,ordered_pair(y,z)),universal_class) ),
introduced(definition,[new_symbols(definition,[sQ612_spl])],[split_symbol_definition]) ).
fof(f18390,plain,
( sQ612_spl
| ~ member(intersection(null_class,ordered_pair(y,z)),universal_class) ),
inference(component_clause,[status(thm)],[f18388]) ).
fof(f18403,plain,
( sQ612_spl
| ~ sQ74_spl
| ~ member(null_class,universal_class) ),
inference(forward_demodulation,[status(thm)],[f17455,f18390]) ).
fof(f18404,plain,
( sQ612_spl
| ~ sQ74_spl
| ~ sQ49_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f18403,f777]) ).
fof(f18405,plain,
( sQ612_spl
| ~ sQ74_spl
| ~ sQ49_spl ),
inference(contradiction_clause,[status(thm)],[f18404]) ).
fof(f19082,plain,
( ~ sQ189_spl
| ~ sQ133_spl
| ~ member(regular(omega),universal_class)
| ~ inductive(complement(diagonalise(null_class))) ),
inference(resolution,[status(thm)],[f7605,f6886]) ).
fof(f19097,plain,
( ~ sQ189_spl
| ~ sQ133_spl
| ~ sQ144_spl
| ~ sQ415_spl ),
inference(split_clause,[status(thm)],[f19082,f11607,f2750,f2389,f4618]) ).
fof(f19494,plain,
( ~ sQ404_spl
| singleton(null_class) = intersection(ordered_pair(null_class,y),singleton(null_class))
| ~ subclass(singleton(null_class),null_class) ),
inference(paramodulation,[status(thm)],[f11335,f6497]) ).
fof(f19496,plain,
( ~ sQ404_spl
| ordered_pair(null_class,y) = intersection(ordered_pair(null_class,y),singleton(null_class))
| ~ subclass(ordered_pair(null_class,y),null_class) ),
inference(paramodulation,[status(thm)],[f11335,f6258]) ).
fof(f19514,definition,
( sQ654_spl
<=> member(null_class,ordered_pair(null_class,y)) ),
introduced(definition,[new_symbols(definition,[sQ654_spl])],[split_symbol_definition]) ).
fof(f19515,plain,
( ~ sQ654_spl
| member(null_class,ordered_pair(null_class,y)) ),
inference(component_clause,[status(thm)],[f19514]) ).
fof(f19518,definition,
( sQ655_spl
<=> subclass(singleton(null_class),null_class) ),
introduced(definition,[new_symbols(definition,[sQ655_spl])],[split_symbol_definition]) ).
fof(f19521,definition,
( sQ656_spl
<=> singleton(null_class) = intersection(ordered_pair(null_class,y),singleton(null_class)) ),
introduced(definition,[new_symbols(definition,[sQ656_spl])],[split_symbol_definition]) ).
fof(f19522,plain,
( ~ sQ656_spl
| singleton(null_class) = intersection(ordered_pair(null_class,y),singleton(null_class)) ),
inference(component_clause,[status(thm)],[f19521]) ).
fof(f19524,plain,
( ~ sQ404_spl
| sQ656_spl
| ~ sQ655_spl ),
inference(split_clause,[status(thm)],[f19494,f19518,f19521,f11334]) ).
fof(f19526,definition,
( sQ657_spl
<=> subclass(ordered_pair(null_class,y),null_class) ),
introduced(definition,[new_symbols(definition,[sQ657_spl])],[split_symbol_definition]) ).
fof(f19529,definition,
( sQ658_spl
<=> ordered_pair(null_class,y) = intersection(ordered_pair(null_class,y),singleton(null_class)) ),
introduced(definition,[new_symbols(definition,[sQ658_spl])],[split_symbol_definition]) ).
fof(f19530,plain,
( ~ sQ658_spl
| ordered_pair(null_class,y) = intersection(ordered_pair(null_class,y),singleton(null_class)) ),
inference(component_clause,[status(thm)],[f19529]) ).
fof(f19532,plain,
( ~ sQ404_spl
| sQ658_spl
| ~ sQ657_spl ),
inference(split_clause,[status(thm)],[f19496,f19526,f19529,f11334]) ).
fof(f19544,plain,
( ~ sQ658_spl
| ~ sQ404_spl
| ordered_pair(null_class,y) = null_class ),
inference(forward_demodulation,[status(thm)],[f11335,f19530]) ).
fof(f19545,plain,
( ~ sQ658_spl
| ~ sQ404_spl
| sQ77_spl
| ~ sQ65_spl
| ~ sQ32_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19544,f11103]) ).
fof(f19546,plain,
( ~ sQ658_spl
| ~ sQ404_spl
| sQ77_spl
| ~ sQ65_spl
| ~ sQ32_spl ),
inference(contradiction_clause,[status(thm)],[f19545]) ).
fof(f19547,plain,
( ~ sQ656_spl
| ~ sQ404_spl
| singleton(null_class) = null_class ),
inference(forward_demodulation,[status(thm)],[f11335,f19522]) ).
fof(f19548,plain,
( ~ sQ656_spl
| ~ sQ404_spl
| sQ60_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19547,f893]) ).
fof(f19549,plain,
( ~ sQ656_spl
| ~ sQ404_spl
| sQ60_spl ),
inference(contradiction_clause,[status(thm)],[f19548]) ).
fof(f19550,plain,
( ~ sQ654_spl
| sQ115_spl
| ~ sQ65_spl
| ~ sQ32_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19515,f11101]) ).
fof(f19551,plain,
( ~ sQ654_spl
| sQ115_spl
| ~ sQ65_spl
| ~ sQ32_spl ),
inference(contradiction_clause,[status(thm)],[f19550]) ).
fof(f19611,plain,
( sQ577_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f16376,f109]) ).
fof(f19612,plain,
sQ577_spl,
inference(contradiction_clause,[status(thm)],[f19611]) ).
fof(f19616,definition,
( sQ660_spl
<=> member(unordered_pair(y,null_class),universal_class) ),
introduced(definition,[new_symbols(definition,[sQ660_spl])],[split_symbol_definition]) ).
fof(f19618,plain,
( sQ660_spl
| ~ member(unordered_pair(y,null_class),universal_class) ),
inference(component_clause,[status(thm)],[f19616]) ).
fof(f19620,plain,
( sQ660_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19618,f109]) ).
fof(f19621,plain,
sQ660_spl,
inference(contradiction_clause,[status(thm)],[f19620]) ).
fof(f19815,plain,
( ~ sQ32_spl
| ~ sQ209_spl
| ~ sQ210_spl
| unordered_pair(w,null_class) = unordered_pair(y,singleton(z))
| unordered_pair(w,null_class) = null_class ),
inference(resolution,[status(thm)],[f5390,f16214]) ).
fof(f19818,plain,
( ~ sQ32_spl
| ~ sQ209_spl
| ~ sQ210_spl
| sQ565_spl
| sQ229_spl ),
inference(split_clause,[status(thm)],[f19815,f6080,f16228,f5389,f5385,f433]) ).
fof(f19819,definition,
( sQ672_spl
<=> unordered_pair(w,null_class) = singleton(y) ),
introduced(definition,[new_symbols(definition,[sQ672_spl])],[split_symbol_definition]) ).
fof(f19820,plain,
( ~ sQ672_spl
| unordered_pair(w,null_class) = singleton(y) ),
inference(component_clause,[status(thm)],[f19819]) ).
fof(f19823,plain,
( ~ sQ672_spl
| ~ sQ65_spl
| unordered_pair(w,null_class) = null_class ),
inference(forward_demodulation,[status(thm)],[f944,f19820]) ).
fof(f19824,plain,
( ~ sQ672_spl
| ~ sQ65_spl
| sQ229_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19823,f6082]) ).
fof(f19825,plain,
( ~ sQ672_spl
| ~ sQ65_spl
| sQ229_spl ),
inference(contradiction_clause,[status(thm)],[f19824]) ).
fof(f20179,plain,
( ~ sQ374_spl
| ~ sQ189_spl
| sQ288_spl ),
inference(split_clause,[status(thm)],[f10065,f7319,f4618,f10039]) ).
fof(f20301,plain,
( ~ sQ567_spl
| member(z,universal_class)
| regular(unordered_pair(y,null_class)) = singleton(x) ),
inference(paramodulation,[status(thm)],[f641,f16240]) ).
fof(f20302,plain,
( ~ sQ567_spl
| intersection(unordered_pair(y,singleton(z)),singleton(x)) = null_class
| unordered_pair(y,singleton(z)) = null_class ),
inference(paramodulation,[status(thm)],[f16240,f170]) ).
fof(f20304,plain,
( ~ sQ567_spl
| member(singleton(x),unordered_pair(y,singleton(z)))
| unordered_pair(y,singleton(z)) = null_class ),
inference(paramodulation,[status(thm)],[f16240,f169]) ).
fof(f20305,definition,
( sQ690_spl
<=> regular(unordered_pair(y,null_class)) = singleton(x) ),
introduced(definition,[new_symbols(definition,[sQ690_spl])],[split_symbol_definition]) ).
fof(f20306,plain,
( ~ sQ690_spl
| regular(unordered_pair(y,null_class)) = singleton(x) ),
inference(component_clause,[status(thm)],[f20305]) ).
fof(f20308,plain,
( ~ sQ567_spl
| sQ29_spl
| sQ690_spl ),
inference(split_clause,[status(thm)],[f20301,f20305,f416,f16239]) ).
fof(f20309,definition,
( sQ691_spl
<=> intersection(unordered_pair(y,singleton(z)),singleton(x)) = null_class ),
introduced(definition,[new_symbols(definition,[sQ691_spl])],[split_symbol_definition]) ).
fof(f20312,plain,
( ~ sQ567_spl
| sQ691_spl
| sQ205_spl ),
inference(split_clause,[status(thm)],[f20302,f5295,f20309,f16239]) ).
fof(f20314,plain,
( ~ sQ567_spl
| sQ570_spl
| sQ205_spl ),
inference(split_clause,[status(thm)],[f20304,f5295,f16250,f16239]) ).
fof(f20319,plain,
( ~ sQ690_spl
| member(singleton(x),unordered_pair(y,null_class))
| unordered_pair(y,null_class) = null_class ),
inference(paramodulation,[status(thm)],[f20306,f169]) ).
fof(f20325,plain,
( ~ sQ690_spl
| sQ411_spl
| sQ207_spl ),
inference(split_clause,[status(thm)],[f20319,f5348,f11414,f20305]) ).
fof(f20326,plain,
( ~ sQ570_spl
| singleton(x) = singleton(z)
| singleton(x) = y ),
inference(resolution,[status(thm)],[f16251,f104]) ).
fof(f20330,definition,
( sQ693_spl
<=> singleton(x) = singleton(z) ),
introduced(definition,[new_symbols(definition,[sQ693_spl])],[split_symbol_definition]) ).
fof(f20331,plain,
( ~ sQ693_spl
| singleton(x) = singleton(z) ),
inference(component_clause,[status(thm)],[f20330]) ).
fof(f20333,plain,
( ~ sQ570_spl
| sQ693_spl
| sQ463_spl ),
inference(split_clause,[status(thm)],[f20326,f13380,f20330,f16250]) ).
fof(f20344,plain,
( sQ95_spl
| ~ sQ693_spl
| ~ member(z,singleton(z)) ),
inference(backward_demodulation,[status(thm)],[f20331,f1314]) ).
fof(f20348,plain,
( ~ sQ693_spl
| member(x,singleton(z))
| singleton(x) = null_class ),
inference(paramodulation,[status(thm)],[f20331,f9045]) ).
fof(f20372,plain,
( ~ sQ693_spl
| sQ28_spl
| sQ219_spl ),
inference(split_clause,[status(thm)],[f20348,f5690,f413,f20330]) ).
fof(f20417,plain,
( sQ95_spl
| ~ sQ693_spl
| singleton(z) = null_class ),
inference(resolution,[status(thm)],[f20344,f9045]) ).
fof(f20418,plain,
( sQ95_spl
| ~ sQ693_spl
| ~ member(z,universal_class) ),
inference(resolution,[status(thm)],[f20344,f263]) ).
fof(f20420,plain,
( sQ95_spl
| ~ sQ693_spl
| sQ69_spl ),
inference(split_clause,[status(thm)],[f20417,f975,f20330,f1312]) ).
fof(f20421,plain,
( sQ95_spl
| ~ sQ693_spl
| ~ sQ29_spl ),
inference(split_clause,[status(thm)],[f20418,f416,f20330,f1312]) ).
fof(f20423,plain,
$false,
inference(sat_refutation,[status(thm)],[f225,f288,f292,f346,f349,f361,f375,f382,f393,f409,f423,f446,f450,f454,f465,f490,f504,f533,f535,f543,f552,f554,f600,f602,f664,f724,f917,f959,f1021,f1029,f1032,f1079,f1094,f1099,f1100,f1131,f1133,f1188,f1268,f1285,f1318,f1324,f1348,f1388,f1455,f1474,f1509,f1556,f1834,f1835,f1952,f1956,f1974,f2214,f2216,f2223,f2347,f2364,f2384,f2388,f2392,f2394,f2471,f2628,f2705,f2753,f2785,f2796,f2831,f2833,f2837,f2846,f2864,f2868,f3007,f3151,f3561,f3582,f3919,f3921,f4173,f4443,f4621,f4808,f4831,f5168,f5298,f5378,f5388,f5414,f5462,f5480,f5711,f5713,f5715,f6049,f6255,f6276,f6280,f6294,f6535,f6539,f6542,f6713,f6784,f6799,f7357,f7853,f7860,f7878,f7915,f8267,f8293,f8535,f8621,f8698,f8708,f8722,f8732,f8742,f8870,f9173,f9199,f9328,f9416,f9621,f9919,f9940,f9986,f10389,f10398,f10426,f10574,f10725,f11287,f11337,f11342,f11344,f11383,f11387,f11392,f11417,f11425,f11434,f11436,f11712,f11778,f11798,f11898,f11941,f11945,f11954,f11958,f11962,f11966,f11970,f12010,f12020,f12062,f12290,f12902,f13383,f13476,f13481,f13584,f13602,f13623,f13631,f13709,f14123,f14146,f14202,f14387,f14766,f14768,f15156,f15740,f15937,f15944,f15975,f15976,f15978,f16041,f16071,f16096,f16238,f16242,f16262,f16293,f16332,f16349,f16442,f16528,f16689,f16957,f17116,f17496,f17623,f18383,f18405,f19097,f19524,f19532,f19546,f19549,f19551,f19612,f19621,f19818,f19825,f20179,f20308,f20312,f20314,f20325,f20333,f20372,f20420,f20421]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SET018-6 : TPTP v9.3.1. Bugfixed v2.1.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 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 : Mon Sep 21 04:42:47 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.13/0.38 % Drodi V4.1.1
% 60.76/8.14 % Refutation found
% 60.76/8.14 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 60.76/8.14 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 4.60/8.23 % Elapsed time: 7.851834 seconds
% 4.60/8.23 % CPU time: 61.393145 seconds
% 4.60/8.23 % Total memory used: 436.572 MB
% 4.60/8.23 % Net memory used: 385.870 MB
%------------------------------------------------------------------------------