%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SET070-7 : TPTP v9.3.1. Bugfixed v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n002.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:09:11 PM UTC 2026
% Result : Unsatisfiable 131.50s 17.52s
% Output : CNFRefutation 131.50s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 187
% Syntax : Number of formulae : 727 ( 82 unt; 126 def)
% Number of atoms : 1847 ( 496 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 1877 ( 757 ~; 994 |; 0 &)
% ( 126 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 4 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of predicates : 134 ( 132 usr; 127 prp; 0-3 aty)
% Number of functors : 30 ( 30 usr; 10 con; 0-3 aty)
% Number of variables : 797 ( 797 !; 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(f6,axiom,
! [X,Y] :
( subclass(Y,X)
| X != Y ),
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(f17,axiom,
! [Z,X,Y] :
( ordered_pair(first(Z),second(Z)) = Z
| ~ member(Z,cross_product(X,Y)) ),
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(f20,axiom,
! [X,Y] :
( member(ordered_pair(X,Y),element_relation)
| ~ member(X,Y)
| ~ member(ordered_pair(X,Y),cross_product(universal_class,universal_class)) ),
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(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(f41,axiom,
! [Z,X,Y] : second(not_subclass_element(restrict(Z,singleton(X),Y),null_class)) = range(Z,X,Y),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f42,axiom,
! [Xr,X] : range_of(restrict(Xr,X,universal_class)) = image(Xr,X),
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(f48,axiom,
! [X] :
( subclass(image(successor_relation,X),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(f53,axiom,
! [X] : domain_of(restrict(element_relation,universal_class,X)) = sum_class(X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f54,axiom,
! [X] :
( member(sum_class(X),universal_class)
| ~ member(X,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(f56,axiom,
! [U] :
( member(power_class(U),universal_class)
| ~ member(U,universal_class) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f62,axiom,
! [Xf] :
( subclass(Xf,cross_product(universal_class,universal_class))
| ~ function(Xf) ),
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(f68,axiom,
! [Xf,Y] : sum_class(image(Xf,singleton(Y))) = apply(Xf,Y),
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(f75,axiom,
intersection(inverse(subset_relation),subset_relation) = identity_relation,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f80,axiom,
! [Xf] :
( subclass(range_of(Xf),domain_of(domain_of(Xf)))
| ~ operation(Xf) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f81,axiom,
! [Xf] :
( operation(Xf)
| ~ subclass(range_of(Xf),domain_of(domain_of(Xf)))
| cross_product(domain_of(domain_of(Xf)),domain_of(domain_of(Xf))) != domain_of(Xf)
| ~ function(Xf) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f85,axiom,
! [Xh,Xf1,Xf2] :
( compatible(Xh,Xf1,Xf2)
| ~ subclass(range_of(Xh),domain_of(domain_of(Xf2)))
| domain_of(domain_of(Xf1)) != domain_of(Xh)
| ~ function(Xh) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f92,axiom,
! [X,Y,U,V] :
( member(X,unordered_pair(X,Y))
| ~ member(ordered_pair(X,Y),cross_product(U,V)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f93,axiom,
! [X,Y,U,V] :
( member(Y,unordered_pair(X,Y))
| ~ member(ordered_pair(X,Y),cross_product(U,V)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f94,axiom,
! [U,V,X,Y] :
( member(U,universal_class)
| ~ member(ordered_pair(U,V),cross_product(X,Y)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f97,axiom,
! [X,Y,Z] :
( subclass(X,Z)
| ~ subclass(Y,Z)
| ~ subclass(X,Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f98,axiom,
! [X,Y] :
( member(not_subclass_element(Y,X),Y)
| member(not_subclass_element(X,Y),X)
| X = Y ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f101,axiom,
! [X,Y] :
( X = Y
| ~ member(not_subclass_element(Y,X),X)
| ~ member(not_subclass_element(X,Y),Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f103,axiom,
! [Z] : ~ member(Z,null_class),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f104,axiom,
! [X] : subclass(null_class,X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f105,axiom,
! [X] :
( X = null_class
| ~ subclass(X,null_class) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f106,axiom,
! [Z] :
( member(not_subclass_element(Z,null_class),Z)
| Z = null_class ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f107,axiom,
member(null_class,universal_class),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f108,axiom,
! [X,Y] : unordered_pair(X,Y) = unordered_pair(Y,X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f109,negated_conjecture,
~ member(x,universal_class),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f110,negated_conjecture,
unordered_pair(x,y) != singleton(y),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f111,plain,
! [Y,U] :
( member(U,Y)
| ! [X] :
( ~ member(U,X)
| ~ subclass(X,Y) ) ),
inference(miniscoping,[status(thm)],[f1]) ).
fof(f112,plain,
! [X0,X1,X2] :
( ~ subclass(X2,X1)
| ~ member(X0,X2)
| member(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f111]) ).
fof(f113,plain,
! [X0,X1] :
( member(not_subclass_element(X0,X1),X0)
| subclass(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f114,plain,
! [X0,X1] :
( subclass(X0,X1)
| ~ member(not_subclass_element(X0,X1),X1) ),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f115,plain,
! [X0] : subclass(X0,universal_class),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f117,plain,
! [X0,X1] :
( subclass(X1,X0)
| X0 != X1 ),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f118,plain,
! [X0,X1] :
( ~ subclass(X1,X0)
| X1 = X0
| ~ subclass(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f119,plain,
! [U,Y] :
( U = Y
| ! [X] :
( U = X
| ~ member(U,unordered_pair(X,Y)) ) ),
inference(miniscoping,[status(thm)],[f8]) ).
fof(f120,plain,
! [X0,X1,X2] :
( X0 = X1
| X0 = X2
| ~ member(X0,unordered_pair(X1,X2)) ),
inference(cnf_transformation,[status(thm)],[f119]) ).
fof(f121,plain,
! [X] :
( ! [Y] : member(X,unordered_pair(X,Y))
| ~ member(X,universal_class) ),
inference(miniscoping,[status(thm)],[f9]) ).
fof(f122,plain,
! [X0,X1] :
( ~ member(X0,universal_class)
| member(X0,unordered_pair(X0,X1)) ),
inference(cnf_transformation,[status(thm)],[f121]) ).
fof(f123,plain,
! [Y] :
( ! [X] : member(Y,unordered_pair(X,Y))
| ~ member(Y,universal_class) ),
inference(miniscoping,[status(thm)],[f10]) ).
fof(f124,plain,
! [X0,X1] :
( member(X0,unordered_pair(X1,X0))
| ~ member(X0,universal_class) ),
inference(cnf_transformation,[status(thm)],[f123]) ).
fof(f125,plain,
! [X0,X1] : member(unordered_pair(X0,X1),universal_class),
inference(cnf_transformation,[status(thm)],[f11]) ).
fof(f126,plain,
! [X0] : singleton(X0) = unordered_pair(X0,X0),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f127,plain,
! [X0,X1] : unordered_pair(singleton(X0),unordered_pair(X0,singleton(X1))) = ordered_pair(X0,X1),
inference(cnf_transformation,[status(thm)],[f13]) ).
fof(f128,plain,
! [U,X] :
( member(U,X)
| ! [V,Y] : ~ member(ordered_pair(U,V),cross_product(X,Y)) ),
inference(miniscoping,[status(thm)],[f14]) ).
fof(f129,plain,
! [X0,X1,X2,X3] :
( ~ member(ordered_pair(X0,X2),cross_product(X1,X3))
| member(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f128]) ).
fof(f130,plain,
! [V,Y] :
( member(V,Y)
| ! [U,X] : ~ member(ordered_pair(U,V),cross_product(X,Y)) ),
inference(miniscoping,[status(thm)],[f15]) ).
fof(f131,plain,
! [X0,X1,X2,X3] :
( member(X1,X3)
| ~ member(ordered_pair(X0,X1),cross_product(X2,X3)) ),
inference(cnf_transformation,[status(thm)],[f130]) ).
fof(f132,plain,
! [X0,X1,X2,X3] :
( ~ member(X2,X3)
| member(ordered_pair(X0,X2),cross_product(X1,X3))
| ~ member(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f16]) ).
fof(f133,plain,
! [Z] :
( ordered_pair(first(Z),second(Z)) = Z
| ! [X,Y] : ~ member(Z,cross_product(X,Y)) ),
inference(miniscoping,[status(thm)],[f17]) ).
fof(f134,plain,
! [X0,X1,X2] :
( ~ member(X0,cross_product(X1,X2))
| X0 = ordered_pair(first(X0),second(X0)) ),
inference(cnf_transformation,[status(thm)],[f133]) ).
fof(f135,plain,
subclass(element_relation,cross_product(universal_class,universal_class)),
inference(cnf_transformation,[status(thm)],[f18]) ).
fof(f137,plain,
! [X0,X1] :
( ~ member(X0,X1)
| member(ordered_pair(X0,X1),element_relation)
| ~ member(ordered_pair(X0,X1),cross_product(universal_class,universal_class)) ),
inference(cnf_transformation,[status(thm)],[f20]) ).
fof(f140,plain,
! [Z,Y] :
( member(Z,Y)
| ! [X] : ~ member(Z,intersection(X,Y)) ),
inference(miniscoping,[status(thm)],[f22]) ).
fof(f141,plain,
! [X0,X1,X2] :
( member(X0,X2)
| ~ member(X0,intersection(X1,X2)) ),
inference(cnf_transformation,[status(thm)],[f140]) ).
fof(f142,plain,
! [X0,X1,X2] :
( ~ member(X0,X2)
| ~ member(X0,X1)
| member(X0,intersection(X1,X2)) ),
inference(cnf_transformation,[status(thm)],[f23]) ).
fof(f143,plain,
! [X0,X1] :
( ~ member(X0,complement(X1))
| ~ member(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f24]) ).
fof(f144,plain,
! [X0,X1] :
( ~ member(X0,universal_class)
| member(X0,X1)
| member(X0,complement(X1)) ),
inference(cnf_transformation,[status(thm)],[f25]) ).
fof(f148,plain,
! [X0,X1,X2] : restrict(X0,X1,X2) = intersection(cross_product(X1,X2),X0),
inference(cnf_transformation,[status(thm)],[f29]) ).
fof(f149,plain,
! [X0,X1] :
( null_class != restrict(X1,singleton(X0),universal_class)
| ~ member(X0,domain_of(X1)) ),
inference(cnf_transformation,[status(thm)],[f30]) ).
fof(f150,plain,
! [X0,X1] :
( ~ member(X1,universal_class)
| member(X1,domain_of(X0))
| restrict(X0,singleton(X1),universal_class) = null_class ),
inference(cnf_transformation,[status(thm)],[f31]) ).
fof(f160,plain,
! [X0,X1,X2] : second(not_subclass_element(restrict(X0,singleton(X1),X2),null_class)) = range(X0,X1,X2),
inference(cnf_transformation,[status(thm)],[f41]) ).
fof(f161,plain,
! [X0,X1] : image(X0,X1) = range_of(restrict(X0,X1,universal_class)),
inference(cnf_transformation,[status(thm)],[f42]) ).
fof(f166,plain,
! [X0] :
( member(null_class,X0)
| ~ inductive(X0) ),
inference(cnf_transformation,[status(thm)],[f47]) ).
fof(f167,plain,
! [X0] :
( ~ inductive(X0)
| subclass(image(successor_relation,X0),X0) ),
inference(cnf_transformation,[status(thm)],[f48]) ).
fof(f168,plain,
! [X0] :
( inductive(X0)
| ~ subclass(image(successor_relation,X0),X0)
| ~ member(null_class,X0) ),
inference(cnf_transformation,[status(thm)],[f49]) ).
fof(f169,plain,
inductive(omega),
inference(cnf_transformation,[status(thm)],[f50]) ).
fof(f170,plain,
! [X0] :
( subclass(omega,X0)
| ~ inductive(X0) ),
inference(cnf_transformation,[status(thm)],[f51]) ).
fof(f172,plain,
! [X0] : domain_of(restrict(element_relation,universal_class,X0)) = sum_class(X0),
inference(cnf_transformation,[status(thm)],[f53]) ).
fof(f173,plain,
! [X0] :
( member(sum_class(X0),universal_class)
| ~ member(X0,universal_class) ),
inference(cnf_transformation,[status(thm)],[f54]) ).
fof(f174,plain,
! [X0] : power_class(X0) = complement(image(element_relation,complement(X0))),
inference(cnf_transformation,[status(thm)],[f55]) ).
fof(f175,plain,
! [X0] :
( member(power_class(X0),universal_class)
| ~ member(X0,universal_class) ),
inference(cnf_transformation,[status(thm)],[f56]) ).
fof(f181,plain,
! [X0] :
( ~ function(X0)
| subclass(X0,cross_product(universal_class,universal_class)) ),
inference(cnf_transformation,[status(thm)],[f62]) ).
fof(f185,plain,
! [X0] :
( X0 = null_class
| member(regular(X0),X0) ),
inference(cnf_transformation,[status(thm)],[f66]) ).
fof(f186,plain,
! [X0] :
( null_class = intersection(X0,regular(X0))
| null_class = X0 ),
inference(cnf_transformation,[status(thm)],[f67]) ).
fof(f187,plain,
! [X0,X1] : sum_class(image(X0,singleton(X1))) = apply(X0,X1),
inference(cnf_transformation,[status(thm)],[f68]) ).
fof(f188,plain,
function(choice),
inference(cnf_transformation,[status(thm)],[f69]) ).
fof(f189,plain,
! [X0] :
( ~ member(X0,universal_class)
| member(apply(choice,X0),X0)
| X0 = null_class ),
inference(cnf_transformation,[status(thm)],[f70]) ).
fof(f193,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(f194,plain,
identity_relation = intersection(inverse(subset_relation),subset_relation),
inference(cnf_transformation,[status(thm)],[f75]) ).
fof(f199,plain,
! [X0] :
( subclass(range_of(X0),domain_of(domain_of(X0)))
| ~ operation(X0) ),
inference(cnf_transformation,[status(thm)],[f80]) ).
fof(f200,plain,
! [X0] :
( ~ subclass(range_of(X0),domain_of(domain_of(X0)))
| operation(X0)
| ~ function(X0)
| cross_product(domain_of(domain_of(X0)),domain_of(domain_of(X0))) != domain_of(X0) ),
inference(cnf_transformation,[status(thm)],[f81]) ).
fof(f207,plain,
! [X0,X1,X2] :
( compatible(X0,X2,X1)
| domain_of(domain_of(X2)) != domain_of(X0)
| ~ subclass(range_of(X0),domain_of(domain_of(X1)))
| ~ function(X0) ),
inference(cnf_transformation,[status(thm)],[f85]) ).
fof(f216,plain,
! [X,Y] :
( member(X,unordered_pair(X,Y))
| ! [U,V] : ~ member(ordered_pair(X,Y),cross_product(U,V)) ),
inference(miniscoping,[status(thm)],[f92]) ).
fof(f217,plain,
! [X0,X1,X2,X3] :
( member(X0,unordered_pair(X0,X1))
| ~ member(ordered_pair(X0,X1),cross_product(X2,X3)) ),
inference(cnf_transformation,[status(thm)],[f216]) ).
fof(f218,plain,
! [X,Y] :
( member(Y,unordered_pair(X,Y))
| ! [U,V] : ~ member(ordered_pair(X,Y),cross_product(U,V)) ),
inference(miniscoping,[status(thm)],[f93]) ).
fof(f219,plain,
! [X0,X1,X2,X3] :
( member(X1,unordered_pair(X0,X1))
| ~ member(ordered_pair(X0,X1),cross_product(X2,X3)) ),
inference(cnf_transformation,[status(thm)],[f218]) ).
fof(f220,plain,
! [U] :
( member(U,universal_class)
| ! [V,X,Y] : ~ member(ordered_pair(U,V),cross_product(X,Y)) ),
inference(miniscoping,[status(thm)],[f94]) ).
fof(f221,plain,
! [X0,X1,X2,X3] :
( ~ member(ordered_pair(X0,X1),cross_product(X2,X3))
| member(X0,universal_class) ),
inference(cnf_transformation,[status(thm)],[f220]) ).
fof(f225,plain,
! [X,Z] :
( subclass(X,Z)
| ! [Y] :
( ~ subclass(Y,Z)
| ~ subclass(X,Y) ) ),
inference(miniscoping,[status(thm)],[f97]) ).
fof(f226,plain,
! [X0,X1,X2] :
( subclass(X0,X2)
| ~ subclass(X1,X2)
| ~ subclass(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f225]) ).
fof(f227,plain,
! [X0,X1] :
( member(not_subclass_element(X1,X0),X1)
| member(not_subclass_element(X0,X1),X0)
| X0 = X1 ),
inference(cnf_transformation,[status(thm)],[f98]) ).
fof(f230,plain,
! [X0,X1] :
( ~ member(not_subclass_element(X1,X0),X0)
| ~ member(not_subclass_element(X0,X1),X1)
| X0 = X1 ),
inference(cnf_transformation,[status(thm)],[f101]) ).
fof(f232,plain,
! [X0] : ~ member(X0,null_class),
inference(cnf_transformation,[status(thm)],[f103]) ).
fof(f233,plain,
! [X0] : subclass(null_class,X0),
inference(cnf_transformation,[status(thm)],[f104]) ).
fof(f234,plain,
! [X0] :
( null_class = X0
| ~ subclass(X0,null_class) ),
inference(cnf_transformation,[status(thm)],[f105]) ).
fof(f235,plain,
! [X0] :
( member(not_subclass_element(X0,null_class),X0)
| null_class = X0 ),
inference(cnf_transformation,[status(thm)],[f106]) ).
fof(f236,plain,
member(null_class,universal_class),
inference(cnf_transformation,[status(thm)],[f107]) ).
fof(f237,plain,
! [X0,X1] : unordered_pair(X0,X1) = unordered_pair(X1,X0),
inference(cnf_transformation,[status(thm)],[f108]) ).
fof(f238,plain,
~ member(x,universal_class),
inference(cnf_transformation,[status(thm)],[f109]) ).
fof(f239,plain,
singleton(y) != unordered_pair(x,y),
inference(cnf_transformation,[status(thm)],[f110]) ).
fof(f241,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)],[f148,f193]) ).
fof(f242,plain,
subset_relation = restrict(restrict(complement(compose(complement(element_relation),inverse(element_relation))),universal_class,universal_class),universal_class,universal_class),
inference(forward_demodulation,[status(thm)],[f148,f241]) ).
fof(f243,plain,
! [X0] : subclass(X0,X0),
inference(destructive_equality_resolution,[status(thm)],[f117]) ).
fof(f254,plain,
! [X0,X1] : ordered_pair(X0,X1) = unordered_pair(singleton(X0),unordered_pair(singleton(X1),X0)),
inference(paramodulation,[status(thm)],[f237,f127]) ).
fof(f257,plain,
! [X0] : unordered_pair(singleton(singleton(X0)),singleton(singleton(X0))) = ordered_pair(singleton(X0),X0),
inference(paramodulation,[status(thm)],[f126,f127]) ).
fof(f258,plain,
! [X0,X1] :
( X0 = X1
| X1 = X0
| ~ member(X0,singleton(X1)) ),
inference(paramodulation,[status(thm)],[f126,f120]) ).
fof(f259,plain,
! [X0] : singleton(singleton(singleton(X0))) = ordered_pair(singleton(X0),X0),
inference(forward_demodulation,[status(thm)],[f126,f257]) ).
fof(f260,plain,
! [X0,X1] :
( ~ member(X1,singleton(X0))
| X0 = X1 ),
inference(duplicate_literals_removal,[status(thm)],[f258]) ).
fof(f262,plain,
! [X0,X1,X2] : member(unordered_pair(X0,X1),unordered_pair(X2,unordered_pair(X0,X1))),
inference(resolution,[status(thm)],[f125,f124]) ).
fof(f263,plain,
! [X0,X1] : member(ordered_pair(X0,X1),universal_class),
inference(paramodulation,[status(thm)],[f127,f125]) ).
fof(f264,plain,
! [X0] : member(singleton(X0),universal_class),
inference(paramodulation,[status(thm)],[f126,f125]) ).
fof(f323,plain,
! [X0,X1] :
( ~ member(X0,ordered_pair(singleton(X1),X1))
| X0 = singleton(singleton(X1)) ),
inference(paramodulation,[status(thm)],[f259,f260]) ).
fof(f368,plain,
! [X0,X1,X2,X3] :
( ~ member(X0,restrict(X1,X2,X3))
| member(X0,X1) ),
inference(paramodulation,[status(thm)],[f148,f141]) ).
fof(f461,plain,
! [X0,X1] :
( member(X0,universal_class)
| ~ member(X0,X1) ),
inference(resolution,[status(thm)],[f112,f115]) ).
fof(f465,plain,
! [X0,X1,X2,X3,X4] :
( member(X1,unordered_pair(X0,X1))
| ~ subclass(X2,cross_product(X3,X4))
| ~ member(ordered_pair(X0,X1),X2) ),
inference(resolution,[status(thm)],[f112,f219]) ).
fof(f466,plain,
! [X0,X1,X2,X3,X4] :
( ~ subclass(X2,cross_product(X3,X4))
| member(X0,unordered_pair(X0,X1))
| ~ member(ordered_pair(X0,X1),X2) ),
inference(resolution,[status(thm)],[f112,f217]) ).
fof(f468,plain,
! [X0] :
( ~ subclass(X0,universal_class)
| ~ member(x,X0) ),
inference(resolution,[status(thm)],[f112,f238]) ).
fof(f469,plain,
! [X0,X1,X2,X3] :
( ~ subclass(X1,intersection(X3,X2))
| member(X0,X2)
| ~ member(X0,X1) ),
inference(resolution,[status(thm)],[f112,f141]) ).
fof(f474,plain,
! [X0,X1] :
( ~ subclass(X1,null_class)
| ~ member(X0,X1) ),
inference(resolution,[status(thm)],[f112,f232]) ).
fof(f476,plain,
! [X0,X1,X2] :
( member(X0,unordered_pair(X0,X2))
| ~ subclass(X1,universal_class)
| ~ member(X0,X1) ),
inference(resolution,[status(thm)],[f112,f122]) ).
fof(f477,plain,
! [X0,X1,X2] :
( member(X0,unordered_pair(X2,X0))
| ~ subclass(X1,universal_class)
| ~ member(X0,X1) ),
inference(resolution,[status(thm)],[f112,f124]) ).
fof(f478,plain,
! [X0,X1,X2] :
( member(X0,unordered_pair(X2,X0))
| ~ member(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f477,f115]) ).
fof(f479,plain,
! [X0] : ~ member(x,X0),
inference(forward_subsumption_resolution,[status(thm)],[f468,f115]) ).
fof(f480,plain,
! [X0,X1,X2] :
( member(X0,unordered_pair(X0,X2))
| ~ member(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f476,f115]) ).
fof(f484,plain,
! [X0,X1] :
( ~ subclass(image(successor_relation,unordered_pair(X1,null_class)),unordered_pair(X1,null_class))
| inductive(unordered_pair(X1,null_class))
| ~ member(null_class,X0) ),
inference(resolution,[status(thm)],[f478,f168]) ).
fof(f490,plain,
! [X0,X1] :
( ~ member(X0,X1)
| member(X0,singleton(X0)) ),
inference(paramodulation,[status(thm)],[f126,f478]) ).
fof(f493,definition,
! [X0] :
( sQ0_spl
<=> ~ member(null_class,X0) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f494,plain,
! [X0] :
( ~ sQ0_spl
| ~ member(null_class,X0) ),
inference(component_clause,[status(thm)],[f493]) ).
fof(f496,definition,
! [X1] :
( sQ1_spl
<=> ( ~ subclass(image(successor_relation,unordered_pair(X1,null_class)),unordered_pair(X1,null_class))
| inductive(unordered_pair(X1,null_class)) ) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f497,plain,
! [X0] :
( ~ sQ1_spl
| inductive(unordered_pair(X0,null_class))
| ~ subclass(image(successor_relation,unordered_pair(X0,null_class)),unordered_pair(X0,null_class)) ),
inference(component_clause,[status(thm)],[f496]) ).
fof(f499,plain,
( sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f484,f493,f496]) ).
fof(f500,plain,
( ~ sQ0_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f236,f494]) ).
fof(f502,plain,
~ sQ0_spl,
inference(contradiction_clause,[status(thm)],[f500]) ).
fof(f514,plain,
! [X0,X1,X2,X3] :
( ~ subclass(universal_class,cross_product(X2,X3))
| member(X0,unordered_pair(X0,X1)) ),
inference(resolution,[status(thm)],[f466,f263]) ).
fof(f522,definition,
! [X0,X1] :
( sQ2_spl
<=> member(X0,unordered_pair(X0,X1)) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f523,plain,
! [X0,X1] :
( ~ sQ2_spl
| member(X0,unordered_pair(X0,X1)) ),
inference(component_clause,[status(thm)],[f522]) ).
fof(f525,definition,
! [X2,X3] :
( sQ3_spl
<=> ~ subclass(universal_class,cross_product(X2,X3)) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f526,plain,
! [X0,X1] :
( ~ sQ3_spl
| ~ subclass(universal_class,cross_product(X0,X1)) ),
inference(component_clause,[status(thm)],[f525]) ).
fof(f528,plain,
( sQ3_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f514,f522,f525]) ).
fof(f540,plain,
( ~ sQ2_spl
| $false ),
inference(resolution,[status(thm)],[f523,f479]) ).
fof(f549,plain,
~ sQ2_spl,
inference(contradiction_clause,[status(thm)],[f540]) ).
fof(f1002,definition,
( sQ5_spl
<=> inductive(null_class) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f1003,plain,
( ~ sQ5_spl
| inductive(null_class) ),
inference(component_clause,[status(thm)],[f1002]) ).
fof(f1005,definition,
( sQ6_spl
<=> null_class = omega ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f1006,plain,
( ~ sQ6_spl
| null_class = omega ),
inference(component_clause,[status(thm)],[f1005]) ).
fof(f1009,definition,
! [X0] :
( sQ7_spl
<=> ~ member(X0,omega) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f1010,plain,
! [X0] :
( ~ sQ7_spl
| ~ member(X0,omega) ),
inference(component_clause,[status(thm)],[f1009]) ).
fof(f1086,plain,
! [X0,X1] :
( ~ member(x,X1)
| ~ member(x,X0) ),
inference(resolution,[status(thm)],[f142,f479]) ).
fof(f1094,definition,
! [X0] :
( sQ11_spl
<=> ~ member(x,X0) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f1097,plain,
sQ11_spl,
inference(split_clause,[status(thm)],[f1086,f1094]) ).
fof(f1125,plain,
( ~ sQ1_spl
| ~ subclass(image(successor_relation,unordered_pair(null_class,null_class)),unordered_pair(null_class,null_class))
| inductive(singleton(null_class)) ),
inference(paramodulation,[status(thm)],[f126,f497]) ).
fof(f1128,definition,
( sQ14_spl
<=> inductive(singleton(null_class)) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f1129,plain,
( ~ sQ14_spl
| inductive(singleton(null_class)) ),
inference(component_clause,[status(thm)],[f1128]) ).
fof(f1131,definition,
( sQ15_spl
<=> subclass(image(successor_relation,unordered_pair(null_class,null_class)),unordered_pair(null_class,null_class)) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f1133,plain,
( sQ15_spl
| ~ subclass(image(successor_relation,unordered_pair(null_class,null_class)),unordered_pair(null_class,null_class)) ),
inference(component_clause,[status(thm)],[f1131]) ).
fof(f1134,plain,
( ~ sQ1_spl
| ~ sQ15_spl
| sQ14_spl ),
inference(split_clause,[status(thm)],[f1125,f1128,f1131,f496]) ).
fof(f1148,plain,
! [X0] :
( ~ member(X0,subset_relation)
| member(X0,restrict(complement(compose(complement(element_relation),inverse(element_relation))),universal_class,universal_class)) ),
inference(paramodulation,[status(thm)],[f242,f368]) ).
fof(f1155,plain,
! [X0,X1,X2] :
( ~ member(X0,X2)
| member(X0,X1)
| member(X0,complement(X1)) ),
inference(resolution,[status(thm)],[f144,f461]) ).
fof(f1167,definition,
! [X0] :
( sQ16_spl
<=> member(x,X0) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f1168,plain,
! [X0] :
( ~ sQ16_spl
| member(x,X0) ),
inference(component_clause,[status(thm)],[f1167]) ).
fof(f1182,plain,
! [X0,X1] :
( ~ subclass(X1,identity_relation)
| ~ member(X0,X1)
| member(X0,subset_relation) ),
inference(paramodulation,[status(thm)],[f194,f469]) ).
fof(f1186,plain,
! [X0,X1,X2] :
( member(unordered_pair(X1,X2),domain_of(X0))
| null_class = restrict(X0,singleton(unordered_pair(X1,X2)),universal_class) ),
inference(resolution,[status(thm)],[f150,f125]) ).
fof(f1223,plain,
! [X0,X1,X2] :
( restrict(restrict(element_relation,universal_class,X2),singleton(unordered_pair(X0,X1)),universal_class) = null_class
| member(unordered_pair(X0,X1),sum_class(X2)) ),
inference(paramodulation,[status(thm)],[f172,f1186]) ).
fof(f1239,plain,
! [X0] :
( ~ inductive(identity_relation)
| ~ member(X0,omega)
| member(X0,subset_relation) ),
inference(resolution,[status(thm)],[f1182,f170]) ).
fof(f1242,definition,
! [X0] :
( sQ17_spl
<=> ( ~ member(X0,omega)
| member(X0,subset_relation) ) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f1243,plain,
! [X0] :
( ~ sQ17_spl
| ~ member(X0,omega)
| member(X0,subset_relation) ),
inference(component_clause,[status(thm)],[f1242]) ).
fof(f1245,definition,
( sQ18_spl
<=> inductive(identity_relation) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f1248,plain,
( ~ sQ18_spl
| sQ17_spl ),
inference(split_clause,[status(thm)],[f1239,f1242,f1245]) ).
fof(f1272,plain,
! [X0,X1] :
( not_subclass_element(singleton(X0),X1) = X0
| subclass(singleton(X0),X1) ),
inference(resolution,[status(thm)],[f113,f260]) ).
fof(f1278,plain,
! [X0,X1,X2] :
( not_subclass_element(unordered_pair(X0,X1),X2) = X0
| X1 = not_subclass_element(unordered_pair(X0,X1),X2)
| subclass(unordered_pair(X0,X1),X2) ),
inference(resolution,[status(thm)],[f113,f120]) ).
fof(f1292,plain,
! [X0,X1] :
( X1 = not_subclass_element(unordered_pair(X0,X1),null_class)
| unordered_pair(X0,X1) = null_class
| not_subclass_element(unordered_pair(X0,X1),null_class) = X0 ),
inference(resolution,[status(thm)],[f1278,f234]) ).
fof(f1307,plain,
! [X0,X1,X2] :
( not_subclass_element(unordered_pair(X0,X1),X2) = X0
| subclass(unordered_pair(X1,X0),X2)
| not_subclass_element(unordered_pair(X0,X1),X2) = X1 ),
inference(paramodulation,[status(thm)],[f237,f1278]) ).
fof(f1361,plain,
! [X0,X1] :
( ~ member(X0,image(element_relation,complement(X1)))
| ~ member(X0,power_class(X1)) ),
inference(paramodulation,[status(thm)],[f174,f143]) ).
fof(f1385,plain,
! [X0,X1,X2,X3] :
( member(X2,X3)
| ~ member(X2,X3)
| ~ member(X0,X1) ),
inference(resolution,[status(thm)],[f132,f129]) ).
fof(f1388,plain,
! [X0,X1,X2,X3] :
( member(X2,universal_class)
| ~ member(X2,X3)
| ~ member(X0,X1) ),
inference(resolution,[status(thm)],[f132,f221]) ).
fof(f1392,definition,
! [X0,X1] :
( sQ20_spl
<=> ~ member(X0,X1) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f1393,plain,
! [X0,X1] :
( ~ sQ20_spl
| ~ member(X0,X1) ),
inference(component_clause,[status(thm)],[f1392]) ).
fof(f1395,definition,
! [X2,X3] :
( sQ21_spl
<=> ( member(X2,X3)
| ~ member(X2,X3) ) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f1398,plain,
( sQ21_spl
| sQ20_spl ),
inference(split_clause,[status(thm)],[f1385,f1392,f1395]) ).
fof(f1399,definition,
! [X2,X3] :
( sQ22_spl
<=> ( member(X2,universal_class)
| ~ member(X2,X3) ) ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f1402,plain,
( sQ22_spl
| sQ20_spl ),
inference(split_clause,[status(thm)],[f1388,f1392,f1399]) ).
fof(f1421,plain,
( ~ sQ20_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f262,f1393]) ).
fof(f1465,plain,
~ sQ20_spl,
inference(contradiction_clause,[status(thm)],[f1421]) ).
fof(f1467,plain,
! [X0] :
( ~ subclass(range_of(restrict(element_relation,universal_class,X0)),domain_of(sum_class(X0)))
| domain_of(restrict(element_relation,universal_class,X0)) != cross_product(domain_of(domain_of(restrict(element_relation,universal_class,X0))),domain_of(domain_of(restrict(element_relation,universal_class,X0))))
| operation(restrict(element_relation,universal_class,X0))
| ~ function(restrict(element_relation,universal_class,X0)) ),
inference(paramodulation,[status(thm)],[f172,f200]) ).
fof(f1476,plain,
! [X0] :
( ~ subclass(range_of(restrict(element_relation,universal_class,X0)),domain_of(sum_class(X0)))
| sum_class(X0) != cross_product(domain_of(domain_of(restrict(element_relation,universal_class,X0))),domain_of(domain_of(restrict(element_relation,universal_class,X0))))
| operation(restrict(element_relation,universal_class,X0))
| ~ function(restrict(element_relation,universal_class,X0)) ),
inference(forward_demodulation,[status(thm)],[f172,f1467]) ).
fof(f1477,plain,
! [X0] :
( ~ subclass(range_of(restrict(element_relation,universal_class,X0)),domain_of(sum_class(X0)))
| sum_class(X0) != cross_product(domain_of(sum_class(X0)),domain_of(domain_of(restrict(element_relation,universal_class,X0))))
| operation(restrict(element_relation,universal_class,X0))
| ~ function(restrict(element_relation,universal_class,X0)) ),
inference(forward_demodulation,[status(thm)],[f172,f1476]) ).
fof(f1478,plain,
! [X0] :
( operation(restrict(element_relation,universal_class,X0))
| ~ function(restrict(element_relation,universal_class,X0))
| ~ subclass(range_of(restrict(element_relation,universal_class,X0)),domain_of(sum_class(X0)))
| cross_product(domain_of(sum_class(X0)),domain_of(sum_class(X0))) != sum_class(X0) ),
inference(forward_demodulation,[status(thm)],[f172,f1477]) ).
fof(f1481,plain,
( ~ sQ14_spl
| subclass(image(successor_relation,singleton(null_class)),singleton(null_class)) ),
inference(resolution,[status(thm)],[f167,f1129]) ).
fof(f1572,plain,
! [X0,X1] :
( subclass(X0,X1)
| ~ subclass(X0,null_class) ),
inference(resolution,[status(thm)],[f226,f233]) ).
fof(f1663,plain,
! [X0] :
( ~ subclass(universal_class,X0)
| universal_class = X0 ),
inference(resolution,[status(thm)],[f118,f115]) ).
fof(f1680,plain,
( ~ function(universal_class)
| cross_product(universal_class,universal_class) = universal_class ),
inference(resolution,[status(thm)],[f1663,f181]) ).
fof(f1684,definition,
( sQ27_spl
<=> cross_product(universal_class,universal_class) = universal_class ),
introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition]) ).
fof(f1685,plain,
( ~ sQ27_spl
| cross_product(universal_class,universal_class) = universal_class ),
inference(component_clause,[status(thm)],[f1684]) ).
fof(f1687,definition,
( sQ28_spl
<=> function(universal_class) ),
introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition]) ).
fof(f1690,plain,
( ~ sQ28_spl
| sQ27_spl ),
inference(split_clause,[status(thm)],[f1680,f1684,f1687]) ).
fof(f1720,plain,
! [X0,X1] :
( ~ sQ27_spl
| ~ member(ordered_pair(X0,X1),universal_class)
| ~ member(X0,X1)
| member(ordered_pair(X0,X1),element_relation) ),
inference(backward_demodulation,[status(thm)],[f1685,f137]) ).
fof(f1756,plain,
! [X0,X1] :
( ~ sQ27_spl
| ~ member(X0,X1)
| member(ordered_pair(X0,X1),element_relation) ),
inference(forward_subsumption_resolution,[status(thm)],[f1720,f263]) ).
fof(f1902,plain,
! [X0] :
( ~ operation(restrict(element_relation,universal_class,X0))
| subclass(range_of(restrict(element_relation,universal_class,X0)),domain_of(sum_class(X0))) ),
inference(paramodulation,[status(thm)],[f172,f199]) ).
fof(f1971,plain,
! [X0,X1,X2,X3] :
( ~ sQ27_spl
| ~ member(X1,X0)
| ~ subclass(element_relation,cross_product(X2,X3))
| member(X0,unordered_pair(X1,X0)) ),
inference(resolution,[status(thm)],[f465,f1756]) ).
fof(f1990,definition,
! [X0,X1] :
( sQ30_spl
<=> ( ~ member(X1,X0)
| member(X0,unordered_pair(X1,X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition]) ).
fof(f1991,plain,
! [X0,X1] :
( ~ sQ30_spl
| member(X1,unordered_pair(X0,X1))
| ~ member(X0,X1) ),
inference(component_clause,[status(thm)],[f1990]) ).
fof(f1993,definition,
! [X2,X3] :
( sQ31_spl
<=> ~ subclass(element_relation,cross_product(X2,X3)) ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f1994,plain,
! [X0,X1] :
( ~ sQ31_spl
| ~ subclass(element_relation,cross_product(X0,X1)) ),
inference(component_clause,[status(thm)],[f1993]) ).
fof(f1996,plain,
( ~ sQ27_spl
| sQ31_spl
| sQ30_spl ),
inference(split_clause,[status(thm)],[f1971,f1990,f1993,f1684]) ).
fof(f1997,definition,
! [X0,X1] :
( sQ32_spl
<=> member(X0,unordered_pair(X1,X0)) ),
introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition]) ).
fof(f1998,plain,
! [X0,X1] :
( ~ sQ32_spl
| member(X0,unordered_pair(X1,X0)) ),
inference(component_clause,[status(thm)],[f1997]) ).
fof(f2002,plain,
( ~ sQ31_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f135,f1994]) ).
fof(f2003,plain,
~ sQ31_spl,
inference(contradiction_clause,[status(thm)],[f2002]) ).
fof(f2004,plain,
! [X0] :
( ~ sQ30_spl
| ~ member(X0,x) ),
inference(resolution,[status(thm)],[f1991,f479]) ).
fof(f2152,plain,
! [X0,X1,X2,X3] :
( compatible(restrict(X0,X1,universal_class),X2,X3)
| ~ subclass(image(X0,X1),domain_of(domain_of(X3)))
| domain_of(restrict(X0,X1,universal_class)) != domain_of(domain_of(X2))
| ~ function(restrict(X0,X1,universal_class)) ),
inference(paramodulation,[status(thm)],[f161,f207]) ).
fof(f2309,plain,
( ~ sQ30_spl
| x = null_class ),
inference(resolution,[status(thm)],[f235,f2004]) ).
fof(f2315,plain,
! [X0] :
( ~ sQ30_spl
| ~ member(null_class,X0) ),
inference(backward_demodulation,[status(thm)],[f2309,f479]) ).
fof(f2317,plain,
( ~ sQ30_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f2315,f493,f1990]) ).
fof(f2364,plain,
! [X0] :
( ~ sQ1_spl
| not_subclass_element(unordered_pair(X0,null_class),null_class) = X0
| not_subclass_element(unordered_pair(X0,null_class),null_class) = null_class
| ~ subclass(image(successor_relation,unordered_pair(X0,null_class)),unordered_pair(X0,null_class))
| inductive(null_class) ),
inference(paramodulation,[status(thm)],[f1292,f497]) ).
fof(f2384,plain,
! [X0,X1,X2] :
( member(null_class,domain_of(X2))
| null_class = restrict(X2,singleton(unordered_pair(X1,X0)),universal_class)
| X1 = not_subclass_element(unordered_pair(X1,X0),null_class)
| X0 = not_subclass_element(unordered_pair(X1,X0),null_class) ),
inference(paramodulation,[status(thm)],[f1292,f1186]) ).
fof(f2399,definition,
( sQ33_spl
<=> member(null_class,universal_class) ),
introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition]) ).
fof(f2401,plain,
( sQ33_spl
| ~ member(null_class,universal_class) ),
inference(component_clause,[status(thm)],[f2399]) ).
fof(f2402,definition,
! [X0,X1] :
( sQ34_spl
<=> ( not_subclass_element(unordered_pair(X0,X1),null_class) = X0
| not_subclass_element(unordered_pair(X0,X1),null_class) = X1 ) ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f2434,definition,
( sQ35_spl
<=> singleton(y) = null_class ),
introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition]) ).
fof(f2435,plain,
( ~ sQ35_spl
| singleton(y) = null_class ),
inference(component_clause,[status(thm)],[f2434]) ).
fof(f2436,plain,
( sQ35_spl
| null_class != singleton(y) ),
inference(component_clause,[status(thm)],[f2434]) ).
fof(f2437,definition,
( sQ36_spl
<=> not_subclass_element(unordered_pair(x,y),null_class) = y ),
introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition]) ).
fof(f2438,plain,
( ~ sQ36_spl
| y = not_subclass_element(unordered_pair(x,y),null_class) ),
inference(component_clause,[status(thm)],[f2437]) ).
fof(f2440,definition,
( sQ37_spl
<=> not_subclass_element(unordered_pair(x,y),null_class) = x ),
introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition]) ).
fof(f2441,plain,
( ~ sQ37_spl
| x = not_subclass_element(unordered_pair(x,y),null_class) ),
inference(component_clause,[status(thm)],[f2440]) ).
fof(f2442,plain,
( sQ37_spl
| not_subclass_element(unordered_pair(x,y),null_class) != x ),
inference(component_clause,[status(thm)],[f2440]) ).
fof(f2463,definition,
! [X0] :
( sQ38_spl
<=> ( not_subclass_element(unordered_pair(X0,null_class),null_class) = X0
| not_subclass_element(unordered_pair(X0,null_class),null_class) = null_class
| ~ subclass(image(successor_relation,unordered_pair(X0,null_class)),unordered_pair(X0,null_class)) ) ),
introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition]) ).
fof(f2466,plain,
( ~ sQ1_spl
| sQ38_spl
| sQ5_spl ),
inference(split_clause,[status(thm)],[f2364,f1002,f2463,f496]) ).
fof(f2468,plain,
( ~ sQ6_spl
| inductive(null_class) ),
inference(backward_demodulation,[status(thm)],[f1006,f169]) ).
fof(f2482,plain,
( ~ sQ37_spl
| member(x,unordered_pair(x,y))
| unordered_pair(x,y) = null_class ),
inference(paramodulation,[status(thm)],[f2441,f235]) ).
fof(f2487,definition,
( sQ40_spl
<=> unordered_pair(x,y) = null_class ),
introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition]) ).
fof(f2488,plain,
( ~ sQ40_spl
| unordered_pair(x,y) = null_class ),
inference(component_clause,[status(thm)],[f2487]) ).
fof(f2489,plain,
( sQ40_spl
| unordered_pair(x,y) != null_class ),
inference(component_clause,[status(thm)],[f2487]) ).
fof(f2490,definition,
( sQ41_spl
<=> member(x,unordered_pair(x,y)) ),
introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition]) ).
fof(f2491,plain,
( ~ sQ41_spl
| member(x,unordered_pair(x,y)) ),
inference(component_clause,[status(thm)],[f2490]) ).
fof(f2493,plain,
( ~ sQ37_spl
| sQ41_spl
| sQ40_spl ),
inference(split_clause,[status(thm)],[f2482,f2487,f2490,f2440]) ).
fof(f2494,plain,
( ~ sQ41_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2491,f479]) ).
fof(f2495,plain,
~ sQ41_spl,
inference(contradiction_clause,[status(thm)],[f2494]) ).
fof(f2496,plain,
( ~ sQ40_spl
| null_class != singleton(y) ),
inference(backward_demodulation,[status(thm)],[f2488,f239]) ).
fof(f2506,definition,
( sQ42_spl
<=> null_class = null_class ),
introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition]) ).
fof(f2509,definition,
( sQ43_spl
<=> member(y,null_class) ),
introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition]) ).
fof(f2510,plain,
( ~ sQ43_spl
| member(y,null_class) ),
inference(component_clause,[status(thm)],[f2509]) ).
fof(f2513,plain,
( ~ sQ43_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2510,f232]) ).
fof(f2514,plain,
~ sQ43_spl,
inference(contradiction_clause,[status(thm)],[f2513]) ).
fof(f2534,plain,
! [X0] :
( ~ sQ40_spl
| member(y,null_class)
| ~ member(y,X0) ),
inference(paramodulation,[status(thm)],[f2488,f478]) ).
fof(f2558,definition,
! [X0] :
( sQ44_spl
<=> ~ member(y,X0) ),
introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition]) ).
fof(f2559,plain,
! [X0] :
( ~ sQ44_spl
| ~ member(y,X0) ),
inference(component_clause,[status(thm)],[f2558]) ).
fof(f2561,plain,
( ~ sQ40_spl
| sQ43_spl
| sQ44_spl ),
inference(split_clause,[status(thm)],[f2534,f2558,f2509,f2487]) ).
fof(f2565,definition,
( sQ45_spl
<=> member(x,null_class) ),
introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition]) ).
fof(f2566,plain,
( ~ sQ45_spl
| member(x,null_class) ),
inference(component_clause,[status(thm)],[f2565]) ).
fof(f2669,plain,
( member(apply(choice,null_class),null_class)
| null_class = null_class ),
inference(resolution,[status(thm)],[f189,f236]) ).
fof(f2674,plain,
! [X0,X1] :
( member(apply(choice,unordered_pair(X0,X1)),unordered_pair(X0,X1))
| null_class = unordered_pair(X0,X1) ),
inference(resolution,[status(thm)],[f189,f125]) ).
fof(f2676,definition,
( sQ47_spl
<=> member(apply(choice,null_class),null_class) ),
introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition]) ).
fof(f2677,plain,
( ~ sQ47_spl
| member(apply(choice,null_class),null_class) ),
inference(component_clause,[status(thm)],[f2676]) ).
fof(f2679,plain,
( sQ47_spl
| sQ42_spl ),
inference(split_clause,[status(thm)],[f2669,f2506,f2676]) ).
fof(f2686,definition,
( sQ50_spl
<=> universal_class = null_class ),
introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition]) ).
fof(f2687,plain,
( ~ sQ50_spl
| null_class = universal_class ),
inference(component_clause,[status(thm)],[f2686]) ).
fof(f2688,plain,
( sQ50_spl
| null_class != universal_class ),
inference(component_clause,[status(thm)],[f2686]) ).
fof(f2690,plain,
( ~ sQ47_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2677,f232]) ).
fof(f2691,plain,
~ sQ47_spl,
inference(contradiction_clause,[status(thm)],[f2690]) ).
fof(f2703,plain,
! [X0] :
( ~ sQ50_spl
| ~ member(X0,universal_class) ),
inference(backward_demodulation,[status(thm)],[f2687,f232]) ).
fof(f2819,plain,
( ~ sQ50_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f264,f2703]) ).
fof(f2828,plain,
~ sQ50_spl,
inference(contradiction_clause,[status(thm)],[f2819]) ).
fof(f2901,definition,
! [X0] :
( sQ51_spl
<=> X0 = null_class ),
introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition]) ).
fof(f2902,plain,
! [X0] :
( ~ sQ51_spl
| null_class = X0 ),
inference(component_clause,[status(thm)],[f2901]) ).
fof(f2908,plain,
( sQ50_spl
| ~ sQ51_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f2688,f2902]) ).
fof(f2909,plain,
( sQ50_spl
| ~ sQ51_spl ),
inference(contradiction_clause,[status(thm)],[f2908]) ).
fof(f2911,plain,
! [X0,X1,X2] :
( ~ member(singleton(singleton(singleton(X0))),cross_product(X2,X1))
| member(X0,X1) ),
inference(paramodulation,[status(thm)],[f259,f131]) ).
fof(f2913,definition,
( sQ52_spl
<=> member(null_class,null_class) ),
introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition]) ).
fof(f2914,plain,
( ~ sQ52_spl
| member(null_class,null_class) ),
inference(component_clause,[status(thm)],[f2913]) ).
fof(f2916,definition,
( sQ53_spl
<=> subclass(universal_class,null_class) ),
introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition]) ).
fof(f2917,plain,
( ~ sQ53_spl
| subclass(universal_class,null_class) ),
inference(component_clause,[status(thm)],[f2916]) ).
fof(f2922,plain,
! [X0] :
( ~ sQ53_spl
| subclass(X0,null_class)
| ~ subclass(X0,universal_class) ),
inference(resolution,[status(thm)],[f2917,f226]) ).
fof(f2927,plain,
! [X0,X1] :
( ~ sQ53_spl
| subclass(X0,X1) ),
inference(backward_subsumption_resolution,[status(thm)],[f1572,f2929]) ).
fof(f2929,plain,
! [X0] :
( ~ sQ53_spl
| subclass(X0,null_class) ),
inference(forward_subsumption_resolution,[status(thm)],[f2922,f115]) ).
fof(f2932,plain,
( ~ sQ3_spl
| ~ sQ53_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f526,f2927]) ).
fof(f3035,plain,
( ~ sQ3_spl
| ~ sQ53_spl ),
inference(contradiction_clause,[status(thm)],[f2932]) ).
fof(f3102,definition,
( sQ54_spl
<=> member(not_subclass_element(null_class,universal_class),null_class) ),
introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition]) ).
fof(f3103,plain,
( ~ sQ54_spl
| member(not_subclass_element(null_class,universal_class),null_class) ),
inference(component_clause,[status(thm)],[f3102]) ).
fof(f3106,plain,
( ~ sQ54_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3103,f232]) ).
fof(f3107,plain,
~ sQ54_spl,
inference(contradiction_clause,[status(thm)],[f3106]) ).
fof(f3108,plain,
! [X0,X1] :
( unordered_pair(X1,X0) = null_class
| apply(choice,unordered_pair(X1,X0)) = X1
| X0 = apply(choice,unordered_pair(X1,X0)) ),
inference(resolution,[status(thm)],[f2674,f120]) ).
fof(f3251,definition,
( sQ58_spl
<=> unordered_pair(y,x) = null_class ),
introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition]) ).
fof(f3252,plain,
( ~ sQ58_spl
| unordered_pair(y,x) = null_class ),
inference(component_clause,[status(thm)],[f3251]) ).
fof(f3271,plain,
( ~ sQ58_spl
| unordered_pair(x,y) = null_class ),
inference(forward_demodulation,[status(thm)],[f237,f3252]) ).
fof(f3490,plain,
! [X0,X1,X2] :
( not_subclass_element(unordered_pair(X0,X1),X2) = X1
| X0 = not_subclass_element(unordered_pair(X0,X1),X2)
| member(not_subclass_element(X2,unordered_pair(X0,X1)),X2)
| unordered_pair(X0,X1) = X2 ),
inference(resolution,[status(thm)],[f227,f120]) ).
fof(f3615,plain,
! [X0,X1,X2] :
( X1 = not_subclass_element(unordered_pair(X0,X1),singleton(X2))
| unordered_pair(X0,X1) = singleton(X2)
| not_subclass_element(singleton(X2),unordered_pair(X0,X1)) = X2
| X0 = not_subclass_element(unordered_pair(X0,X1),singleton(X2)) ),
inference(resolution,[status(thm)],[f3490,f260]) ).
fof(f3815,definition,
( sQ66_spl
<=> y = x ),
introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition]) ).
fof(f3816,plain,
( ~ sQ66_spl
| y = x ),
inference(component_clause,[status(thm)],[f3815]) ).
fof(f3817,plain,
( sQ66_spl
| y != x ),
inference(component_clause,[status(thm)],[f3815]) ).
fof(f3824,plain,
~ inductive(null_class),
inference(resolution,[status(thm)],[f166,f232]) ).
fof(f3836,plain,
( ~ sQ5_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3824,f1003]) ).
fof(f3837,plain,
~ sQ5_spl,
inference(contradiction_clause,[status(thm)],[f3836]) ).
fof(f3838,plain,
( ~ sQ6_spl
| sQ5_spl ),
inference(split_clause,[status(thm)],[f2468,f1002,f1005]) ).
fof(f3861,definition,
( sQ69_spl
<=> y = null_class ),
introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition]) ).
fof(f3862,plain,
( ~ sQ69_spl
| null_class = y ),
inference(component_clause,[status(thm)],[f3861]) ).
fof(f3864,definition,
( sQ70_spl
<=> x = null_class ),
introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition]) ).
fof(f3865,plain,
( ~ sQ70_spl
| x = null_class ),
inference(component_clause,[status(thm)],[f3864]) ).
fof(f3871,plain,
( sQ66_spl
| ~ sQ69_spl
| null_class != x ),
inference(backward_demodulation,[status(thm)],[f3862,f3817]) ).
fof(f3874,plain,
( ~ sQ70_spl
| sQ66_spl
| ~ sQ69_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3865,f3871]) ).
fof(f3875,plain,
( ~ sQ70_spl
| sQ66_spl
| ~ sQ69_spl ),
inference(contradiction_clause,[status(thm)],[f3874]) ).
fof(f3877,plain,
! [X0,X1] :
( ~ member(image(X0,singleton(X1)),universal_class)
| member(apply(X0,X1),universal_class) ),
inference(paramodulation,[status(thm)],[f187,f173]) ).
fof(f3910,plain,
( ~ sQ7_spl
| ~ inductive(omega) ),
inference(resolution,[status(thm)],[f1010,f166]) ).
fof(f3911,plain,
( ~ sQ7_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3910,f169]) ).
fof(f3912,plain,
~ sQ7_spl,
inference(contradiction_clause,[status(thm)],[f3911]) ).
fof(f4052,plain,
! [X0] :
( null_class = singleton(X0)
| regular(singleton(X0)) = X0 ),
inference(resolution,[status(thm)],[f185,f260]) ).
fof(f4054,plain,
! [X0,X1] :
( X1 = regular(unordered_pair(X0,X1))
| unordered_pair(X0,X1) = null_class
| regular(unordered_pair(X0,X1)) = X0 ),
inference(resolution,[status(thm)],[f185,f120]) ).
fof(f4111,plain,
! [X0,X1,X2] :
( null_class = restrict(X0,singleton(unordered_pair(X1,X2)),universal_class)
| X1 = regular(unordered_pair(X1,X2))
| regular(unordered_pair(X1,X2)) = X2
| member(null_class,domain_of(X0)) ),
inference(paramodulation,[status(thm)],[f4054,f1186]) ).
fof(f4135,plain,
! [X0,X1,X2] :
( regular(unordered_pair(X2,X0)) = X0
| regular(unordered_pair(X2,X0)) = X2
| member(X0,null_class)
| ~ member(X0,X1) ),
inference(paramodulation,[status(thm)],[f4054,f478]) ).
fof(f4139,plain,
! [X0,X1] :
( X0 = regular(unordered_pair(X1,X0))
| regular(unordered_pair(X1,X0)) = X1
| unordered_pair(X0,X1) = null_class ),
inference(paramodulation,[status(thm)],[f4054,f237]) ).
fof(f4146,definition,
( sQ72_spl
<=> regular(unordered_pair(x,y)) = x ),
introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition]) ).
fof(f4147,plain,
( ~ sQ72_spl
| regular(unordered_pair(x,y)) = x ),
inference(component_clause,[status(thm)],[f4146]) ).
fof(f4149,definition,
( sQ73_spl
<=> regular(unordered_pair(x,y)) = y ),
introduced(definition,[new_symbols(definition,[sQ73_spl])],[split_symbol_definition]) ).
fof(f4150,plain,
( ~ sQ73_spl
| regular(unordered_pair(x,y)) = y ),
inference(component_clause,[status(thm)],[f4149]) ).
fof(f4189,definition,
! [X0,X1] :
( sQ77_spl
<=> ( regular(unordered_pair(X0,X1)) = X1
| regular(unordered_pair(X0,X1)) = X0 ) ),
introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition]) ).
fof(f4193,definition,
! [X0] :
( sQ78_spl
<=> ( regular(unordered_pair(X0,null_class)) = null_class
| regular(unordered_pair(X0,null_class)) = X0 ) ),
introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition]) ).
fof(f4220,plain,
! [X0,X1,X2] :
( regular(unordered_pair(X0,X1)) = X1
| ~ member(X1,X2)
| regular(unordered_pair(X0,X1)) = X0 ),
inference(forward_subsumption_resolution,[status(thm)],[f4135,f232]) ).
fof(f4234,plain,
( ~ sQ52_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2914,f232]) ).
fof(f4235,plain,
~ sQ52_spl,
inference(contradiction_clause,[status(thm)],[f4234]) ).
fof(f4348,definition,
! [X0] :
( sQ80_spl
<=> ( ~ subclass(cross_product(universal_class,universal_class),X0)
| universal_class = X0 ) ),
introduced(definition,[new_symbols(definition,[sQ80_spl])],[split_symbol_definition]) ).
fof(f4349,plain,
! [X0] :
( ~ sQ80_spl
| ~ subclass(cross_product(universal_class,universal_class),X0)
| X0 = universal_class ),
inference(component_clause,[status(thm)],[f4348]) ).
fof(f4414,plain,
( ~ sQ80_spl
| cross_product(universal_class,universal_class) = universal_class ),
inference(resolution,[status(thm)],[f4349,f243]) ).
fof(f4415,plain,
( ~ sQ80_spl
| sQ27_spl ),
inference(split_clause,[status(thm)],[f4414,f1684,f4348]) ).
fof(f4745,plain,
! [X0,X1] :
( ~ inductive(X1)
| regular(unordered_pair(X0,null_class)) = null_class
| X0 = regular(unordered_pair(X0,null_class)) ),
inference(resolution,[status(thm)],[f4220,f166]) ).
fof(f4773,definition,
! [X1] :
( sQ86_spl
<=> restrict(X1,singleton(null_class),universal_class) = null_class ),
introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition]) ).
fof(f4774,plain,
! [X0] :
( ~ sQ86_spl
| restrict(X0,singleton(null_class),universal_class) = null_class ),
inference(component_clause,[status(thm)],[f4773]) ).
fof(f4777,definition,
! [X1] :
( sQ87_spl
<=> member(null_class,X1) ),
introduced(definition,[new_symbols(definition,[sQ87_spl])],[split_symbol_definition]) ).
fof(f4778,plain,
! [X0] :
( ~ sQ87_spl
| member(null_class,X0) ),
inference(component_clause,[status(thm)],[f4777]) ).
fof(f4785,definition,
! [X1] :
( sQ89_spl
<=> ~ inductive(X1) ),
introduced(definition,[new_symbols(definition,[sQ89_spl])],[split_symbol_definition]) ).
fof(f4786,plain,
! [X0] :
( ~ sQ89_spl
| ~ inductive(X0) ),
inference(component_clause,[status(thm)],[f4785]) ).
fof(f4788,plain,
( sQ89_spl
| sQ78_spl ),
inference(split_clause,[status(thm)],[f4745,f4193,f4785]) ).
fof(f4790,plain,
( ~ sQ89_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f169,f4786]) ).
fof(f4796,plain,
( sQ15_spl
| ~ subclass(image(successor_relation,singleton(null_class)),unordered_pair(null_class,null_class)) ),
inference(forward_demodulation,[status(thm)],[f126,f1133]) ).
fof(f4797,plain,
( sQ15_spl
| ~ subclass(image(successor_relation,singleton(null_class)),singleton(null_class)) ),
inference(forward_demodulation,[status(thm)],[f126,f4796]) ).
fof(f4835,plain,
! [X0] :
( ~ sQ87_spl
| null_class = singleton(singleton(X0)) ),
inference(resolution,[status(thm)],[f4778,f323]) ).
fof(f4914,plain,
! [X0,X1,X2] :
( ~ sQ87_spl
| ~ member(null_class,cross_product(X2,X1))
| member(X0,X1) ),
inference(backward_demodulation,[status(thm)],[f4835,f2911]) ).
fof(f5006,definition,
! [X0] :
( sQ92_spl
<=> member(X0,unordered_pair(X0,singleton(X0))) ),
introduced(definition,[new_symbols(definition,[sQ92_spl])],[split_symbol_definition]) ).
fof(f5007,plain,
! [X0] :
( ~ sQ92_spl
| member(X0,unordered_pair(X0,singleton(X0))) ),
inference(component_clause,[status(thm)],[f5006]) ).
fof(f5156,plain,
! [X0,X1] :
( ~ sQ87_spl
| ~ member(X0,image(element_relation,complement(X1))) ),
inference(backward_subsumption_resolution,[status(thm)],[f1361,f5208]) ).
fof(f5208,plain,
! [X0,X1] :
( ~ sQ87_spl
| member(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f4914,f4778]) ).
fof(f5221,plain,
( ~ sQ87_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5156,f5208]) ).
fof(f5222,plain,
~ sQ87_spl,
inference(contradiction_clause,[status(thm)],[f5221]) ).
fof(f5257,plain,
( ~ sQ92_spl
| $false ),
inference(resolution,[status(thm)],[f5007,f479]) ).
fof(f5260,plain,
~ sQ92_spl,
inference(contradiction_clause,[status(thm)],[f5257]) ).
fof(f5262,plain,
! [X0] :
( ~ sQ86_spl
| image(X0,singleton(null_class)) = range_of(null_class) ),
inference(paramodulation,[status(thm)],[f4774,f161]) ).
fof(f5969,plain,
( ~ sQ45_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2566,f479]) ).
fof(f5970,plain,
~ sQ45_spl,
inference(contradiction_clause,[status(thm)],[f5969]) ).
fof(f6528,definition,
! [X0,X1] :
( sQ104_spl
<=> ( X1 = not_subclass_element(unordered_pair(X1,X0),null_class)
| not_subclass_element(unordered_pair(X1,X0),null_class) = X0
| regular(unordered_pair(X1,X0)) = X1
| X0 = regular(unordered_pair(X1,X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ104_spl])],[split_symbol_definition]) ).
fof(f6720,plain,
! [X0,X1,X2] :
( X1 = not_subclass_element(singleton(X1),X2)
| member(X0,X2)
| ~ member(X0,singleton(X1)) ),
inference(resolution,[status(thm)],[f1272,f112]) ).
fof(f6907,plain,
! [X0,X1,X2] :
( apply(choice,unordered_pair(X1,X2)) = X1
| member(null_class,domain_of(X0))
| X2 = apply(choice,unordered_pair(X1,X2))
| restrict(X0,singleton(unordered_pair(X1,X2)),universal_class) = null_class ),
inference(paramodulation,[status(thm)],[f3108,f1186]) ).
fof(f6936,definition,
! [X0,X1] :
( sQ107_spl
<=> ( apply(choice,unordered_pair(X1,X0)) = X1
| X0 = apply(choice,unordered_pair(X1,X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ107_spl])],[split_symbol_definition]) ).
fof(f7030,plain,
! [X0,X1,X2] :
( ~ member(X0,X2)
| member(X0,X1)
| not_subclass_element(singleton(X0),X1) = X0 ),
inference(resolution,[status(thm)],[f6720,f490]) ).
fof(f7047,plain,
! [X0,X1] :
( ~ inductive(X1)
| null_class = not_subclass_element(singleton(null_class),X0)
| member(null_class,X0) ),
inference(resolution,[status(thm)],[f7030,f166]) ).
fof(f7061,definition,
! [X0] :
( sQ116_spl
<=> ( null_class = not_subclass_element(singleton(null_class),X0)
| member(null_class,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ116_spl])],[split_symbol_definition]) ).
fof(f7064,plain,
( sQ89_spl
| sQ116_spl ),
inference(split_clause,[status(thm)],[f7047,f7061,f4785]) ).
fof(f7066,plain,
~ sQ89_spl,
inference(contradiction_clause,[status(thm)],[f4790]) ).
fof(f7245,definition,
( sQ117_spl
<=> regular(unordered_pair(y,x)) = y ),
introduced(definition,[new_symbols(definition,[sQ117_spl])],[split_symbol_definition]) ).
fof(f7248,definition,
( sQ118_spl
<=> x = regular(unordered_pair(y,x)) ),
introduced(definition,[new_symbols(definition,[sQ118_spl])],[split_symbol_definition]) ).
fof(f7249,plain,
( ~ sQ118_spl
| x = regular(unordered_pair(y,x)) ),
inference(component_clause,[status(thm)],[f7248]) ).
fof(f7262,definition,
! [X0,X1] :
( sQ119_spl
<=> ( X1 = regular(unordered_pair(X0,X1))
| regular(unordered_pair(X0,X1)) = X0
| regular(unordered_pair(X1,X0)) = X1
| X0 = regular(unordered_pair(X1,X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ119_spl])],[split_symbol_definition]) ).
fof(f7292,plain,
( ~ sQ118_spl
| x = regular(unordered_pair(x,y)) ),
inference(forward_demodulation,[status(thm)],[f237,f7249]) ).
fof(f8062,plain,
! [X0] :
( ~ sQ86_spl
| null_class != null_class
| ~ member(null_class,domain_of(X0)) ),
inference(paramodulation,[status(thm)],[f4774,f149]) ).
fof(f8069,definition,
! [X0] :
( sQ122_spl
<=> ~ member(null_class,domain_of(X0)) ),
introduced(definition,[new_symbols(definition,[sQ122_spl])],[split_symbol_definition]) ).
fof(f8070,plain,
! [X0] :
( ~ sQ122_spl
| ~ member(null_class,domain_of(X0)) ),
inference(component_clause,[status(thm)],[f8069]) ).
fof(f8072,plain,
( ~ sQ86_spl
| ~ sQ42_spl
| sQ122_spl ),
inference(split_clause,[status(thm)],[f8062,f8069,f2506,f4773]) ).
fof(f8075,plain,
! [X0,X1,X2] :
( ~ sQ122_spl
| regular(unordered_pair(X0,X1)) = X1
| null_class = restrict(X2,singleton(unordered_pair(X0,X1)),universal_class)
| regular(unordered_pair(X0,X1)) = X0 ),
inference(backward_subsumption_resolution,[status(thm)],[f4111,f8070]) ).
fof(f8083,plain,
! [X0,X1,X2] :
( ~ sQ122_spl
| not_subclass_element(unordered_pair(X0,X1),null_class) = X1
| null_class = restrict(X2,singleton(unordered_pair(X0,X1)),universal_class)
| X0 = not_subclass_element(unordered_pair(X0,X1),null_class) ),
inference(forward_subsumption_resolution,[status(thm)],[f2384,f8070]) ).
fof(f8153,plain,
( ~ sQ40_spl
| regular(singleton(y)) = y
| null_class != null_class ),
inference(paramodulation,[status(thm)],[f4052,f2496]) ).
fof(f8170,plain,
! [X0,X1] :
( regular(singleton(X0)) = X0
| ~ member(X0,X1)
| member(X0,null_class) ),
inference(paramodulation,[status(thm)],[f4052,f490]) ).
fof(f8183,definition,
( sQ128_spl
<=> regular(singleton(y)) = y ),
introduced(definition,[new_symbols(definition,[sQ128_spl])],[split_symbol_definition]) ).
fof(f8184,plain,
( ~ sQ128_spl
| y = regular(singleton(y)) ),
inference(component_clause,[status(thm)],[f8183]) ).
fof(f8186,plain,
( ~ sQ40_spl
| sQ128_spl
| ~ sQ42_spl ),
inference(split_clause,[status(thm)],[f8153,f2506,f8183,f2487]) ).
fof(f8187,plain,
! [X0,X1] :
( regular(singleton(X0)) = X0
| ~ member(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f8170,f232]) ).
fof(f8188,definition,
( sQ129_spl
<=> regular(singleton(null_class)) = null_class ),
introduced(definition,[new_symbols(definition,[sQ129_spl])],[split_symbol_definition]) ).
fof(f8192,definition,
! [X0] :
( sQ130_spl
<=> regular(singleton(X0)) = X0 ),
introduced(definition,[new_symbols(definition,[sQ130_spl])],[split_symbol_definition]) ).
fof(f8198,plain,
! [X0,X1,X2] :
( ~ sQ122_spl
| apply(choice,unordered_pair(X1,X2)) = X2
| X1 = apply(choice,unordered_pair(X1,X2))
| null_class = restrict(X0,singleton(unordered_pair(X1,X2)),universal_class) ),
inference(forward_subsumption_resolution,[status(thm)],[f6907,f8070]) ).
fof(f8200,plain,
( sQ35_spl
| regular(singleton(y)) = y
| null_class != null_class ),
inference(paramodulation,[status(thm)],[f4052,f2436]) ).
fof(f8201,plain,
( sQ35_spl
| sQ128_spl
| ~ sQ42_spl ),
inference(split_clause,[status(thm)],[f8200,f2506,f8183,f2434]) ).
fof(f8202,plain,
( sQ37_spl
| ~ sQ36_spl
| x != y ),
inference(backward_demodulation,[status(thm)],[f2438,f2442]) ).
fof(f8203,plain,
( sQ40_spl
| x = not_subclass_element(unordered_pair(x,y),null_class)
| not_subclass_element(unordered_pair(x,y),null_class) = y ),
inference(resolution,[status(thm)],[f2489,f1292]) ).
fof(f8204,plain,
( sQ40_spl
| regular(unordered_pair(x,y)) = x
| y = regular(unordered_pair(x,y)) ),
inference(resolution,[status(thm)],[f2489,f4054]) ).
fof(f8205,plain,
( sQ40_spl
| x = regular(unordered_pair(y,x))
| regular(unordered_pair(y,x)) = y ),
inference(resolution,[status(thm)],[f2489,f4139]) ).
fof(f8216,plain,
( sQ40_spl
| sQ72_spl
| sQ73_spl ),
inference(split_clause,[status(thm)],[f8204,f4149,f4146,f2487]) ).
fof(f8218,plain,
( sQ40_spl
| sQ37_spl
| sQ36_spl ),
inference(split_clause,[status(thm)],[f8203,f2437,f2440,f2487]) ).
fof(f8219,plain,
( sQ40_spl
| sQ118_spl
| sQ117_spl ),
inference(split_clause,[status(thm)],[f8205,f7245,f7248,f2487]) ).
fof(f8235,definition,
( sQ131_spl
<=> x = not_subclass_element(unordered_pair(x,y),singleton(y)) ),
introduced(definition,[new_symbols(definition,[sQ131_spl])],[split_symbol_definition]) ).
fof(f8236,plain,
( ~ sQ131_spl
| not_subclass_element(unordered_pair(x,y),singleton(y)) = x ),
inference(component_clause,[status(thm)],[f8235]) ).
fof(f8238,definition,
( sQ132_spl
<=> not_subclass_element(singleton(y),unordered_pair(x,y)) = y ),
introduced(definition,[new_symbols(definition,[sQ132_spl])],[split_symbol_definition]) ).
fof(f8239,plain,
( ~ sQ132_spl
| not_subclass_element(singleton(y),unordered_pair(x,y)) = y ),
inference(component_clause,[status(thm)],[f8238]) ).
fof(f8241,definition,
( sQ133_spl
<=> y = not_subclass_element(unordered_pair(x,y),singleton(y)) ),
introduced(definition,[new_symbols(definition,[sQ133_spl])],[split_symbol_definition]) ).
fof(f8242,plain,
( ~ sQ133_spl
| not_subclass_element(unordered_pair(x,y),singleton(y)) = y ),
inference(component_clause,[status(thm)],[f8241]) ).
fof(f8246,plain,
( ~ sQ58_spl
| sQ40_spl ),
inference(split_clause,[status(thm)],[f3271,f2487,f3251]) ).
fof(f8250,plain,
! [X0,X1,X2,X3,X4] :
( ~ sQ122_spl
| X3 = regular(unordered_pair(X3,X4))
| regular(unordered_pair(X3,X4)) = X4
| not_subclass_element(unordered_pair(X1,X2),singleton(unordered_pair(X3,X4))) = X1
| not_subclass_element(singleton(unordered_pair(X3,X4)),unordered_pair(X1,X2)) = unordered_pair(X3,X4)
| not_subclass_element(unordered_pair(X1,X2),singleton(unordered_pair(X3,X4))) = X2
| restrict(X0,unordered_pair(X1,X2),universal_class) = null_class ),
inference(paramodulation,[status(thm)],[f3615,f8075]) ).
fof(f8255,plain,
! [X0,X1,X2,X3] :
( ~ sQ122_spl
| regular(unordered_pair(X0,X1)) = X1
| not_subclass_element(unordered_pair(X0,X1),singleton(X3)) = X0
| X3 = not_subclass_element(singleton(X3),unordered_pair(X0,X1))
| X1 = not_subclass_element(unordered_pair(X0,X1),singleton(X3))
| restrict(X2,singleton(singleton(X3)),universal_class) = null_class
| X0 = regular(unordered_pair(X0,X1)) ),
inference(paramodulation,[status(thm)],[f3615,f8075]) ).
fof(f8258,plain,
! [X0,X1,X2] :
( ~ sQ122_spl
| X1 = regular(unordered_pair(X2,X1))
| regular(unordered_pair(X2,X1)) = X2
| regular(unordered_pair(X1,X2)) = X2
| X1 = regular(unordered_pair(X1,X2))
| restrict(X0,singleton(null_class),universal_class) = null_class ),
inference(paramodulation,[status(thm)],[f4139,f8075]) ).
fof(f8259,plain,
! [X0,X1,X2] :
( ~ sQ122_spl
| X1 = not_subclass_element(unordered_pair(X1,X2),null_class)
| not_subclass_element(unordered_pair(X1,X2),null_class) = X2
| regular(unordered_pair(X1,X2)) = X2
| X1 = regular(unordered_pair(X1,X2))
| restrict(X0,singleton(null_class),universal_class) = null_class ),
inference(paramodulation,[status(thm)],[f1292,f8075]) ).
fof(f8260,plain,
! [X0,X1,X2] :
( ~ sQ122_spl
| regular(unordered_pair(X1,X2)) = X1
| X2 = regular(unordered_pair(X1,X2))
| regular(unordered_pair(X1,X2)) = X2
| X1 = regular(unordered_pair(X1,X2))
| restrict(X0,singleton(null_class),universal_class) = null_class ),
inference(paramodulation,[status(thm)],[f4054,f8075]) ).
fof(f8261,plain,
! [X0,X1] :
( ~ sQ122_spl
| regular(unordered_pair(X1,X1)) = X1
| X1 = regular(unordered_pair(X1,X1))
| restrict(X0,singleton(singleton(X1)),universal_class) = null_class ),
inference(paramodulation,[status(thm)],[f126,f8075]) ).
fof(f8264,plain,
! [X0,X1,X2] :
( ~ sQ122_spl
| regular(unordered_pair(X0,X1)) = X1
| X0 = regular(unordered_pair(X0,X1))
| null_class != null_class
| ~ member(unordered_pair(X0,X1),domain_of(X2)) ),
inference(paramodulation,[status(thm)],[f8075,f149]) ).
fof(f8265,plain,
! [X0,X1,X2] :
( ~ sQ122_spl
| second(not_subclass_element(null_class,null_class)) = range(X2,unordered_pair(X0,X1),universal_class)
| regular(unordered_pair(X0,X1)) = X1
| regular(unordered_pair(X0,X1)) = X0 ),
inference(paramodulation,[status(thm)],[f8075,f160]) ).
fof(f8266,plain,
! [X0,X1,X2] :
( ~ sQ122_spl
| image(X2,singleton(unordered_pair(X1,X0))) = range_of(null_class)
| X1 = regular(unordered_pair(X1,X0))
| X0 = regular(unordered_pair(X1,X0)) ),
inference(paramodulation,[status(thm)],[f8075,f161]) ).
fof(f8267,plain,
! [X0,X1,X2,X3] :
( ~ sQ122_spl
| regular(unordered_pair(X2,X3)) = X3
| X2 = regular(unordered_pair(X2,X3))
| member(X0,X1)
| ~ member(X0,null_class) ),
inference(paramodulation,[status(thm)],[f8075,f368]) ).
fof(f8268,plain,
( ~ sQ122_spl
| sQ119_spl
| sQ86_spl ),
inference(split_clause,[status(thm)],[f8258,f4773,f7262,f8069]) ).
fof(f8278,definition,
! [X0,X1] :
( sQ136_spl
<=> ( member(X0,X1)
| ~ member(X0,null_class) ) ),
introduced(definition,[new_symbols(definition,[sQ136_spl])],[split_symbol_definition]) ).
fof(f8281,plain,
( ~ sQ122_spl
| sQ77_spl
| sQ136_spl ),
inference(split_clause,[status(thm)],[f8267,f8278,f4189,f8069]) ).
fof(f8282,definition,
! [X1,X2] :
( sQ137_spl
<=> ( regular(unordered_pair(X1,X2)) = X1
| X2 = regular(unordered_pair(X1,X2))
| regular(unordered_pair(X1,X2)) = X2
| X1 = regular(unordered_pair(X1,X2)) ) ),
introduced(definition,[new_symbols(definition,[sQ137_spl])],[split_symbol_definition]) ).
fof(f8285,plain,
( ~ sQ122_spl
| sQ137_spl
| sQ86_spl ),
inference(split_clause,[status(thm)],[f8260,f4773,f8282,f8069]) ).
fof(f8286,plain,
! [X0,X1] :
( ~ sQ122_spl
| regular(unordered_pair(X1,X1)) = X1
| X1 = regular(singleton(X1))
| restrict(X0,singleton(singleton(X1)),universal_class) = null_class ),
inference(forward_demodulation,[status(thm)],[f126,f8261]) ).
fof(f8287,plain,
! [X0,X1] :
( ~ sQ122_spl
| regular(singleton(X1)) = X1
| X1 = regular(singleton(X1))
| restrict(X0,singleton(singleton(X1)),universal_class) = null_class ),
inference(forward_demodulation,[status(thm)],[f126,f8286]) ).
fof(f8288,plain,
! [X0,X1] :
( ~ sQ122_spl
| restrict(X1,singleton(singleton(X0)),universal_class) = null_class
| X0 = regular(singleton(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f8287]) ).
fof(f8289,plain,
( ~ sQ122_spl
| sQ104_spl
| sQ86_spl ),
inference(split_clause,[status(thm)],[f8259,f4773,f6528,f8069]) ).
fof(f8290,definition,
! [X0,X1,X2] :
( sQ138_spl
<=> ( regular(unordered_pair(X0,X1)) = X1
| X0 = regular(unordered_pair(X0,X1))
| ~ member(unordered_pair(X0,X1),domain_of(X2)) ) ),
introduced(definition,[new_symbols(definition,[sQ138_spl])],[split_symbol_definition]) ).
fof(f8293,plain,
( ~ sQ122_spl
| ~ sQ42_spl
| sQ138_spl ),
inference(split_clause,[status(thm)],[f8264,f8290,f2506,f8069]) ).
fof(f8297,plain,
( sQ15_spl
| ~ sQ86_spl
| ~ subclass(range_of(null_class),singleton(null_class)) ),
inference(backward_demodulation,[status(thm)],[f5262,f4797]) ).
fof(f8354,plain,
( ~ sQ128_spl
| singleton(y) = null_class
| member(y,singleton(y)) ),
inference(paramodulation,[status(thm)],[f8184,f185]) ).
fof(f8355,plain,
( ~ sQ128_spl
| null_class = intersection(singleton(y),y)
| null_class = singleton(y) ),
inference(paramodulation,[status(thm)],[f8184,f186]) ).
fof(f8357,definition,
( sQ140_spl
<=> null_class = intersection(singleton(y),y) ),
introduced(definition,[new_symbols(definition,[sQ140_spl])],[split_symbol_definition]) ).
fof(f8358,plain,
( ~ sQ140_spl
| intersection(singleton(y),y) = null_class ),
inference(component_clause,[status(thm)],[f8357]) ).
fof(f8360,plain,
( ~ sQ128_spl
| sQ140_spl
| sQ35_spl ),
inference(split_clause,[status(thm)],[f8355,f2434,f8357,f8183]) ).
fof(f8361,definition,
( sQ141_spl
<=> member(y,singleton(y)) ),
introduced(definition,[new_symbols(definition,[sQ141_spl])],[split_symbol_definition]) ).
fof(f8362,plain,
( ~ sQ141_spl
| member(y,singleton(y)) ),
inference(component_clause,[status(thm)],[f8361]) ).
fof(f8364,plain,
( ~ sQ128_spl
| sQ35_spl
| sQ141_spl ),
inference(split_clause,[status(thm)],[f8354,f8361,f2434,f8183]) ).
fof(f8365,plain,
! [X0] :
( ~ sQ141_spl
| not_subclass_element(singleton(y),X0) = y
| member(y,X0) ),
inference(resolution,[status(thm)],[f8362,f6720]) ).
fof(f8424,plain,
( ~ sQ73_spl
| null_class = intersection(unordered_pair(x,y),y)
| null_class = unordered_pair(x,y) ),
inference(paramodulation,[status(thm)],[f4150,f186]) ).
fof(f8425,definition,
( sQ142_spl
<=> null_class = intersection(unordered_pair(x,y),y) ),
introduced(definition,[new_symbols(definition,[sQ142_spl])],[split_symbol_definition]) ).
fof(f8428,plain,
( ~ sQ73_spl
| sQ142_spl
| sQ40_spl ),
inference(split_clause,[status(thm)],[f8424,f2487,f8425,f4149]) ).
fof(f8430,definition,
( sQ143_spl
<=> member(y,unordered_pair(x,y)) ),
introduced(definition,[new_symbols(definition,[sQ143_spl])],[split_symbol_definition]) ).
fof(f8431,plain,
( ~ sQ143_spl
| member(y,unordered_pair(x,y)) ),
inference(component_clause,[status(thm)],[f8430]) ).
fof(f8435,plain,
! [X0] :
( ~ sQ140_spl
| ~ member(X0,y)
| member(X0,null_class)
| ~ member(X0,singleton(y)) ),
inference(paramodulation,[status(thm)],[f8358,f142]) ).
fof(f8440,plain,
! [X0] :
( ~ sQ140_spl
| ~ member(X0,singleton(y))
| ~ member(X0,y) ),
inference(forward_subsumption_resolution,[status(thm)],[f8435,f232]) ).
fof(f8520,plain,
! [X0,X1,X2] :
( ~ sQ122_spl
| not_subclass_element(unordered_pair(singleton(X0),unordered_pair(singleton(X1),X0)),null_class) = unordered_pair(singleton(X1),X0)
| restrict(X2,singleton(ordered_pair(X0,X1)),universal_class) = null_class
| not_subclass_element(unordered_pair(singleton(X0),unordered_pair(singleton(X1),X0)),null_class) = singleton(X0) ),
inference(paramodulation,[status(thm)],[f254,f8083]) ).
fof(f8521,plain,
! [X0,X1,X2] :
( ~ sQ122_spl
| not_subclass_element(unordered_pair(singleton(X0),unordered_pair(X0,singleton(X1))),null_class) = unordered_pair(X0,singleton(X1))
| restrict(X2,singleton(ordered_pair(X0,X1)),universal_class) = null_class
| not_subclass_element(unordered_pair(singleton(X0),unordered_pair(X0,singleton(X1))),null_class) = singleton(X0) ),
inference(paramodulation,[status(thm)],[f127,f8083]) ).
fof(f8527,plain,
! [X0,X1,X2] :
( ~ sQ122_spl
| X0 = not_subclass_element(unordered_pair(X0,X1),null_class)
| not_subclass_element(unordered_pair(X0,X1),null_class) = X1
| not_subclass_element(unordered_pair(X0,X1),null_class) = X1
| restrict(X2,singleton(null_class),universal_class) = null_class
| not_subclass_element(unordered_pair(X0,X1),null_class) = X0 ),
inference(paramodulation,[status(thm)],[f1292,f8083]) ).
fof(f8528,plain,
! [X0,X1] :
( ~ sQ122_spl
| not_subclass_element(unordered_pair(X0,X0),null_class) = X0
| restrict(X1,singleton(singleton(X0)),universal_class) = null_class
| not_subclass_element(unordered_pair(X0,X0),null_class) = X0 ),
inference(paramodulation,[status(thm)],[f126,f8083]) ).
fof(f8531,plain,
! [X0,X1,X2] :
( ~ sQ122_spl
| not_subclass_element(unordered_pair(X0,X1),null_class) = X1
| not_subclass_element(unordered_pair(X0,X1),null_class) = X0
| null_class != null_class
| ~ member(unordered_pair(X0,X1),domain_of(X2)) ),
inference(paramodulation,[status(thm)],[f8083,f149]) ).
fof(f8534,plain,
! [X0,X1,X2,X3] :
( ~ sQ122_spl
| not_subclass_element(unordered_pair(X2,X3),null_class) = X3
| not_subclass_element(unordered_pair(X2,X3),null_class) = X2
| member(X0,X1)
| ~ member(X0,null_class) ),
inference(paramodulation,[status(thm)],[f8083,f368]) ).
fof(f8535,definition,
! [X0,X1] :
( sQ144_spl
<=> ( X0 = not_subclass_element(unordered_pair(X0,X1),null_class)
| not_subclass_element(unordered_pair(X0,X1),null_class) = X1
| not_subclass_element(unordered_pair(X0,X1),null_class) = X1
| not_subclass_element(unordered_pair(X0,X1),null_class) = X0 ) ),
introduced(definition,[new_symbols(definition,[sQ144_spl])],[split_symbol_definition]) ).
fof(f8538,plain,
( ~ sQ122_spl
| sQ86_spl
| sQ144_spl ),
inference(split_clause,[status(thm)],[f8527,f8535,f4773,f8069]) ).
fof(f8539,plain,
( ~ sQ122_spl
| sQ34_spl
| sQ136_spl ),
inference(split_clause,[status(thm)],[f8534,f8278,f2402,f8069]) ).
fof(f8544,plain,
! [X0,X1,X2] :
( ~ sQ122_spl
| not_subclass_element(unordered_pair(singleton(X0),unordered_pair(X0,singleton(X1))),null_class) = unordered_pair(X0,singleton(X1))
| restrict(X2,singleton(ordered_pair(X0,X1)),universal_class) = null_class
| not_subclass_element(ordered_pair(X0,X1),null_class) = singleton(X0) ),
inference(forward_demodulation,[status(thm)],[f127,f8521]) ).
fof(f8545,plain,
! [X0,X1,X2] :
( ~ sQ122_spl
| not_subclass_element(ordered_pair(X0,X1),null_class) = singleton(X0)
| restrict(X2,singleton(ordered_pair(X0,X1)),universal_class) = null_class
| unordered_pair(X0,singleton(X1)) = not_subclass_element(ordered_pair(X0,X1),null_class) ),
inference(forward_demodulation,[status(thm)],[f127,f8544]) ).
fof(f8546,plain,
! [X0,X1] :
( ~ sQ122_spl
| not_subclass_element(unordered_pair(X0,X0),null_class) = X0
| restrict(X1,singleton(singleton(X0)),universal_class) = null_class
| not_subclass_element(singleton(X0),null_class) = X0 ),
inference(forward_demodulation,[status(thm)],[f126,f8528]) ).
fof(f8547,plain,
! [X0,X1] :
( ~ sQ122_spl
| not_subclass_element(singleton(X0),null_class) = X0
| restrict(X1,singleton(singleton(X0)),universal_class) = null_class
| not_subclass_element(singleton(X0),null_class) = X0 ),
inference(forward_demodulation,[status(thm)],[f126,f8546]) ).
fof(f8548,plain,
! [X0,X1] :
( ~ sQ122_spl
| not_subclass_element(singleton(X1),null_class) = X1
| null_class = restrict(X0,singleton(singleton(X1)),universal_class) ),
inference(duplicate_literals_removal,[status(thm)],[f8547]) ).
fof(f8549,definition,
! [X0,X1,X2] :
( sQ146_spl
<=> ( not_subclass_element(unordered_pair(X0,X1),null_class) = X1
| not_subclass_element(unordered_pair(X0,X1),null_class) = X0
| ~ member(unordered_pair(X0,X1),domain_of(X2)) ) ),
introduced(definition,[new_symbols(definition,[sQ146_spl])],[split_symbol_definition]) ).
fof(f8552,plain,
( ~ sQ122_spl
| ~ sQ42_spl
| sQ146_spl ),
inference(split_clause,[status(thm)],[f8531,f8549,f2506,f8069]) ).
fof(f8553,plain,
! [X0,X1,X2] :
( ~ sQ122_spl
| not_subclass_element(unordered_pair(singleton(X0),unordered_pair(singleton(X1),X0)),null_class) = unordered_pair(singleton(X1),X0)
| restrict(X2,singleton(ordered_pair(X0,X1)),universal_class) = null_class
| not_subclass_element(ordered_pair(X0,X1),null_class) = singleton(X0) ),
inference(forward_demodulation,[status(thm)],[f254,f8520]) ).
fof(f8554,plain,
! [X0,X1,X2] :
( ~ sQ122_spl
| singleton(X1) = not_subclass_element(ordered_pair(X1,X2),null_class)
| not_subclass_element(ordered_pair(X1,X2),null_class) = unordered_pair(singleton(X2),X1)
| null_class = restrict(X0,singleton(ordered_pair(X1,X2)),universal_class) ),
inference(forward_demodulation,[status(thm)],[f254,f8553]) ).
fof(f8568,plain,
! [X0] :
( null_class = regular(singleton(null_class))
| ~ inductive(X0) ),
inference(resolution,[status(thm)],[f166,f8187]) ).
fof(f8572,plain,
( sQ129_spl
| sQ89_spl ),
inference(split_clause,[status(thm)],[f8568,f4785,f8188]) ).
fof(f8600,plain,
! [X0,X1,X2] :
( ~ sQ122_spl
| unordered_pair(singleton(X1),X0) = apply(choice,unordered_pair(singleton(X0),unordered_pair(singleton(X1),X0)))
| null_class = restrict(X2,singleton(ordered_pair(X0,X1)),universal_class)
| singleton(X0) = apply(choice,unordered_pair(singleton(X0),unordered_pair(singleton(X1),X0))) ),
inference(paramodulation,[status(thm)],[f254,f8198]) ).
fof(f8601,plain,
! [X0,X1,X2] :
( ~ sQ122_spl
| unordered_pair(X0,singleton(X1)) = apply(choice,unordered_pair(singleton(X0),unordered_pair(X0,singleton(X1))))
| null_class = restrict(X2,singleton(ordered_pair(X0,X1)),universal_class)
| singleton(X0) = apply(choice,unordered_pair(singleton(X0),unordered_pair(X0,singleton(X1)))) ),
inference(paramodulation,[status(thm)],[f127,f8198]) ).
fof(f8607,plain,
! [X0,X1] :
( ~ sQ122_spl
| X0 = apply(choice,unordered_pair(X0,X0))
| null_class = restrict(X1,singleton(singleton(X0)),universal_class)
| X0 = apply(choice,unordered_pair(X0,X0)) ),
inference(paramodulation,[status(thm)],[f126,f8198]) ).
fof(f8610,plain,
! [X0,X1,X2] :
( ~ sQ122_spl
| X1 = apply(choice,unordered_pair(X0,X1))
| X0 = apply(choice,unordered_pair(X0,X1))
| null_class != null_class
| ~ member(unordered_pair(X0,X1),domain_of(X2)) ),
inference(paramodulation,[status(thm)],[f8198,f149]) ).
fof(f8613,plain,
! [X0,X1,X2,X3] :
( ~ sQ122_spl
| X3 = apply(choice,unordered_pair(X2,X3))
| X2 = apply(choice,unordered_pair(X2,X3))
| member(X0,X1)
| ~ member(X0,null_class) ),
inference(paramodulation,[status(thm)],[f8198,f368]) ).
fof(f8614,plain,
! [X0,X1,X2] :
( ~ sQ122_spl
| unordered_pair(X0,singleton(X1)) = apply(choice,unordered_pair(singleton(X0),unordered_pair(X0,singleton(X1))))
| null_class = restrict(X2,singleton(ordered_pair(X0,X1)),universal_class)
| singleton(X0) = apply(choice,ordered_pair(X0,X1)) ),
inference(forward_demodulation,[status(thm)],[f127,f8601]) ).
fof(f8615,plain,
! [X0,X1,X2] :
( ~ sQ122_spl
| singleton(X0) = apply(choice,ordered_pair(X0,X1))
| restrict(X2,singleton(ordered_pair(X0,X1)),universal_class) = null_class
| unordered_pair(X0,singleton(X1)) = apply(choice,ordered_pair(X0,X1)) ),
inference(forward_demodulation,[status(thm)],[f127,f8614]) ).
fof(f8616,definition,
! [X0,X1,X2] :
( sQ147_spl
<=> ( X1 = apply(choice,unordered_pair(X0,X1))
| X0 = apply(choice,unordered_pair(X0,X1))
| ~ member(unordered_pair(X0,X1),domain_of(X2)) ) ),
introduced(definition,[new_symbols(definition,[sQ147_spl])],[split_symbol_definition]) ).
fof(f8619,plain,
( ~ sQ122_spl
| ~ sQ42_spl
| sQ147_spl ),
inference(split_clause,[status(thm)],[f8610,f8616,f2506,f8069]) ).
fof(f8624,plain,
! [X0,X1,X2] :
( ~ sQ122_spl
| unordered_pair(singleton(X1),X0) = apply(choice,unordered_pair(singleton(X0),unordered_pair(singleton(X1),X0)))
| null_class = restrict(X2,singleton(ordered_pair(X0,X1)),universal_class)
| singleton(X0) = apply(choice,ordered_pair(X0,X1)) ),
inference(forward_demodulation,[status(thm)],[f254,f8600]) ).
fof(f8625,plain,
! [X0,X1,X2] :
( ~ sQ122_spl
| apply(choice,ordered_pair(X1,X2)) = singleton(X1)
| unordered_pair(singleton(X2),X1) = apply(choice,ordered_pair(X1,X2))
| null_class = restrict(X0,singleton(ordered_pair(X1,X2)),universal_class) ),
inference(forward_demodulation,[status(thm)],[f254,f8624]) ).
fof(f8626,plain,
! [X0,X1] :
( ~ sQ122_spl
| X0 = apply(choice,unordered_pair(X0,X0))
| null_class = restrict(X1,singleton(singleton(X0)),universal_class)
| X0 = apply(choice,singleton(X0)) ),
inference(forward_demodulation,[status(thm)],[f126,f8607]) ).
fof(f8627,plain,
! [X0,X1] :
( ~ sQ122_spl
| X0 = apply(choice,singleton(X0))
| null_class = restrict(X1,singleton(singleton(X0)),universal_class)
| X0 = apply(choice,singleton(X0)) ),
inference(forward_demodulation,[status(thm)],[f126,f8626]) ).
fof(f8628,plain,
! [X0,X1] :
( ~ sQ122_spl
| X1 = apply(choice,singleton(X1))
| null_class = restrict(X0,singleton(singleton(X1)),universal_class) ),
inference(duplicate_literals_removal,[status(thm)],[f8627]) ).
fof(f8629,plain,
( ~ sQ122_spl
| sQ107_spl
| sQ136_spl ),
inference(split_clause,[status(thm)],[f8613,f8278,f6936,f8069]) ).
fof(f8642,plain,
! [X0] :
( ~ sQ35_spl
| ~ member(y,X0)
| member(y,null_class) ),
inference(paramodulation,[status(thm)],[f2435,f490]) ).
fof(f8658,plain,
( ~ sQ35_spl
| sQ44_spl
| sQ43_spl ),
inference(split_clause,[status(thm)],[f8642,f2509,f2558,f2434]) ).
fof(f8670,plain,
( ~ sQ143_spl
| ~ sQ44_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f8431,f2559]) ).
fof(f8671,plain,
( ~ sQ143_spl
| ~ sQ44_spl ),
inference(contradiction_clause,[status(thm)],[f8670]) ).
fof(f8731,plain,
( ~ sQ16_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1168,f479]) ).
fof(f8732,plain,
~ sQ16_spl,
inference(contradiction_clause,[status(thm)],[f8731]) ).
fof(f8832,plain,
( ~ sQ118_spl
| sQ72_spl ),
inference(split_clause,[status(thm)],[f7292,f4146,f7248]) ).
fof(f8846,plain,
! [X0,X1] :
( member(null_class,X0)
| ~ member(null_class,X1)
| inductive(complement(X0))
| ~ subclass(image(successor_relation,complement(X0)),complement(X0)) ),
inference(resolution,[status(thm)],[f168,f1155]) ).
fof(f8847,plain,
! [X0,X1] :
( ~ member(null_class,X1)
| inductive(unordered_pair(null_class,X0))
| ~ subclass(image(successor_relation,unordered_pair(null_class,X0)),unordered_pair(null_class,X0)) ),
inference(resolution,[status(thm)],[f168,f480]) ).
fof(f8848,plain,
! [X0] :
( ~ member(null_class,X0)
| inductive(singleton(null_class))
| ~ subclass(image(successor_relation,singleton(null_class)),singleton(null_class)) ),
inference(resolution,[status(thm)],[f168,f490]) ).
fof(f8850,definition,
( sQ149_spl
<=> subclass(image(successor_relation,universal_class),universal_class) ),
introduced(definition,[new_symbols(definition,[sQ149_spl])],[split_symbol_definition]) ).
fof(f8852,plain,
( sQ149_spl
| ~ subclass(image(successor_relation,universal_class),universal_class) ),
inference(component_clause,[status(thm)],[f8850]) ).
fof(f8853,definition,
( sQ150_spl
<=> inductive(universal_class) ),
introduced(definition,[new_symbols(definition,[sQ150_spl])],[split_symbol_definition]) ).
fof(f8857,definition,
! [X0] :
( sQ151_spl
<=> ( inductive(unordered_pair(null_class,X0))
| ~ subclass(image(successor_relation,unordered_pair(null_class,X0)),unordered_pair(null_class,X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ151_spl])],[split_symbol_definition]) ).
fof(f8860,plain,
( sQ0_spl
| sQ151_spl ),
inference(split_clause,[status(thm)],[f8847,f8857,f493]) ).
fof(f8861,definition,
! [X0] :
( sQ152_spl
<=> ( member(null_class,X0)
| inductive(complement(X0))
| ~ subclass(image(successor_relation,complement(X0)),complement(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ152_spl])],[split_symbol_definition]) ).
fof(f8864,plain,
( sQ0_spl
| sQ152_spl ),
inference(split_clause,[status(thm)],[f8846,f8861,f493]) ).
fof(f8866,definition,
( sQ153_spl
<=> subclass(image(successor_relation,singleton(null_class)),singleton(null_class)) ),
introduced(definition,[new_symbols(definition,[sQ153_spl])],[split_symbol_definition]) ).
fof(f8868,plain,
( sQ153_spl
| ~ subclass(image(successor_relation,singleton(null_class)),singleton(null_class)) ),
inference(component_clause,[status(thm)],[f8866]) ).
fof(f8869,plain,
( sQ0_spl
| sQ14_spl
| ~ sQ153_spl ),
inference(split_clause,[status(thm)],[f8848,f8866,f1128,f493]) ).
fof(f8870,plain,
( sQ153_spl
| ~ sQ86_spl
| ~ subclass(range_of(null_class),singleton(null_class)) ),
inference(forward_demodulation,[status(thm)],[f5262,f8868]) ).
fof(f8871,plain,
( ~ sQ14_spl
| ~ sQ86_spl
| subclass(range_of(null_class),singleton(null_class)) ),
inference(forward_demodulation,[status(thm)],[f5262,f1481]) ).
fof(f8872,plain,
( ~ sQ14_spl
| ~ sQ86_spl
| sQ15_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f8871,f8297]) ).
fof(f8873,plain,
( ~ sQ14_spl
| ~ sQ86_spl
| sQ15_spl ),
inference(contradiction_clause,[status(thm)],[f8872]) ).
fof(f8874,plain,
( sQ149_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f8852,f115]) ).
fof(f8875,plain,
sQ149_spl,
inference(contradiction_clause,[status(thm)],[f8874]) ).
fof(f8876,plain,
( sQ153_spl
| ~ sQ86_spl
| ~ sQ14_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f8870,f8871]) ).
fof(f8877,plain,
( sQ153_spl
| ~ sQ86_spl
| ~ sQ14_spl ),
inference(contradiction_clause,[status(thm)],[f8876]) ).
fof(f8994,plain,
( ~ sQ36_spl
| member(y,unordered_pair(x,y))
| null_class = unordered_pair(x,y) ),
inference(paramodulation,[status(thm)],[f2438,f235]) ).
fof(f9000,definition,
( sQ154_spl
<=> subclass(unordered_pair(x,y),null_class) ),
introduced(definition,[new_symbols(definition,[sQ154_spl])],[split_symbol_definition]) ).
fof(f9001,plain,
( ~ sQ154_spl
| subclass(unordered_pair(x,y),null_class) ),
inference(component_clause,[status(thm)],[f9000]) ).
fof(f9002,plain,
( sQ154_spl
| ~ subclass(unordered_pair(x,y),null_class) ),
inference(component_clause,[status(thm)],[f9000]) ).
fof(f9004,definition,
( sQ155_spl
<=> member(not_subclass_element(null_class,unordered_pair(x,y)),null_class) ),
introduced(definition,[new_symbols(definition,[sQ155_spl])],[split_symbol_definition]) ).
fof(f9005,plain,
( ~ sQ155_spl
| member(not_subclass_element(null_class,unordered_pair(x,y)),null_class) ),
inference(component_clause,[status(thm)],[f9004]) ).
fof(f9013,plain,
( ~ sQ36_spl
| sQ143_spl
| sQ40_spl ),
inference(split_clause,[status(thm)],[f8994,f2487,f8430,f2437]) ).
fof(f9015,plain,
( ~ sQ155_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f9005,f232]) ).
fof(f9016,plain,
~ sQ155_spl,
inference(contradiction_clause,[status(thm)],[f9015]) ).
fof(f9043,plain,
! [X0,X1] :
( ~ sQ32_spl
| member(X0,unordered_pair(X0,X1)) ),
inference(paramodulation,[status(thm)],[f237,f1998]) ).
fof(f9045,plain,
( ~ sQ32_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f9043,f522,f1997]) ).
fof(f9287,definition,
( sQ159_spl
<=> y = y ),
introduced(definition,[new_symbols(definition,[sQ159_spl])],[split_symbol_definition]) ).
fof(f9430,plain,
! [X0] :
( ~ sQ154_spl
| ~ member(X0,unordered_pair(x,y)) ),
inference(resolution,[status(thm)],[f9001,f474]) ).
fof(f9443,plain,
( ~ sQ143_spl
| ~ sQ154_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f8431,f9430]) ).
fof(f9444,definition,
( sQ161_spl
<=> subclass(null_class,unordered_pair(x,y)) ),
introduced(definition,[new_symbols(definition,[sQ161_spl])],[split_symbol_definition]) ).
fof(f9446,plain,
( sQ161_spl
| ~ subclass(null_class,unordered_pair(x,y)) ),
inference(component_clause,[status(thm)],[f9444]) ).
fof(f9448,plain,
( ~ sQ143_spl
| ~ sQ154_spl ),
inference(contradiction_clause,[status(thm)],[f9443]) ).
fof(f9449,plain,
( sQ161_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f9446,f233]) ).
fof(f9450,plain,
sQ161_spl,
inference(contradiction_clause,[status(thm)],[f9449]) ).
fof(f9513,plain,
( sQ154_spl
| not_subclass_element(unordered_pair(y,x),null_class) = y
| not_subclass_element(unordered_pair(y,x),null_class) = x ),
inference(resolution,[status(thm)],[f9002,f1307]) ).
fof(f9523,definition,
( sQ162_spl
<=> not_subclass_element(unordered_pair(y,x),null_class) = x ),
introduced(definition,[new_symbols(definition,[sQ162_spl])],[split_symbol_definition]) ).
fof(f9524,plain,
( ~ sQ162_spl
| not_subclass_element(unordered_pair(y,x),null_class) = x ),
inference(component_clause,[status(thm)],[f9523]) ).
fof(f9526,definition,
( sQ163_spl
<=> not_subclass_element(unordered_pair(y,x),null_class) = y ),
introduced(definition,[new_symbols(definition,[sQ163_spl])],[split_symbol_definition]) ).
fof(f9529,plain,
( sQ154_spl
| sQ163_spl
| sQ162_spl ),
inference(split_clause,[status(thm)],[f9513,f9523,f9526,f9000]) ).
fof(f9532,plain,
( ~ sQ162_spl
| not_subclass_element(unordered_pair(x,y),null_class) = x ),
inference(forward_demodulation,[status(thm)],[f237,f9524]) ).
fof(f9533,plain,
( ~ sQ162_spl
| ~ sQ36_spl
| y = x ),
inference(forward_demodulation,[status(thm)],[f2438,f9532]) ).
fof(f9534,plain,
( ~ sQ162_spl
| ~ sQ36_spl
| sQ37_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f9533,f8202]) ).
fof(f9535,plain,
( ~ sQ162_spl
| ~ sQ36_spl
| sQ37_spl ),
inference(contradiction_clause,[status(thm)],[f9534]) ).
fof(f9569,plain,
( ~ sQ143_spl
| y = x
| y = y ),
inference(resolution,[status(thm)],[f8431,f120]) ).
fof(f9578,plain,
( ~ sQ143_spl
| sQ66_spl
| sQ159_spl ),
inference(split_clause,[status(thm)],[f9569,f9287,f3815,f8430]) ).
fof(f9580,plain,
( ~ sQ66_spl
| sQ37_spl
| ~ sQ36_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3816,f8202]) ).
fof(f9581,plain,
( ~ sQ66_spl
| sQ37_spl
| ~ sQ36_spl ),
inference(contradiction_clause,[status(thm)],[f9580]) ).
fof(f9728,plain,
( ~ sQ72_spl
| unordered_pair(x,y) = null_class
| member(x,unordered_pair(x,y)) ),
inference(paramodulation,[status(thm)],[f4147,f185]) ).
fof(f9730,plain,
( ~ sQ72_spl
| sQ40_spl
| sQ41_spl ),
inference(split_clause,[status(thm)],[f9728,f2490,f2487,f4146]) ).
fof(f9788,definition,
( sQ167_spl
<=> y = not_subclass_element(unordered_pair(x,y),unordered_pair(y,y)) ),
introduced(definition,[new_symbols(definition,[sQ167_spl])],[split_symbol_definition]) ).
fof(f9789,plain,
( ~ sQ167_spl
| y = not_subclass_element(unordered_pair(x,y),unordered_pair(y,y)) ),
inference(component_clause,[status(thm)],[f9788]) ).
fof(f9790,plain,
( sQ167_spl
| y != not_subclass_element(unordered_pair(x,y),unordered_pair(y,y)) ),
inference(component_clause,[status(thm)],[f9788]) ).
fof(f9803,plain,
( ~ sQ167_spl
| not_subclass_element(unordered_pair(x,y),singleton(y)) = y ),
inference(forward_demodulation,[status(thm)],[f126,f9789]) ).
fof(f9837,plain,
( ~ sQ140_spl
| singleton(y) = null_class
| ~ member(regular(singleton(y)),y) ),
inference(resolution,[status(thm)],[f8440,f185]) ).
fof(f9838,plain,
( ~ sQ140_spl
| null_class = singleton(y)
| ~ member(not_subclass_element(singleton(y),null_class),y) ),
inference(resolution,[status(thm)],[f8440,f235]) ).
fof(f9843,plain,
! [X0] :
( ~ sQ140_spl
| ~ member(y,X0)
| ~ member(y,y) ),
inference(resolution,[status(thm)],[f8440,f490]) ).
fof(f9844,definition,
( sQ170_spl
<=> member(not_subclass_element(singleton(y),null_class),y) ),
introduced(definition,[new_symbols(definition,[sQ170_spl])],[split_symbol_definition]) ).
fof(f9847,plain,
( ~ sQ140_spl
| sQ35_spl
| ~ sQ170_spl ),
inference(split_clause,[status(thm)],[f9838,f9844,f2434,f8357]) ).
fof(f9855,definition,
( sQ173_spl
<=> member(y,y) ),
introduced(definition,[new_symbols(definition,[sQ173_spl])],[split_symbol_definition]) ).
fof(f9858,plain,
( ~ sQ140_spl
| sQ44_spl
| ~ sQ173_spl ),
inference(split_clause,[status(thm)],[f9843,f9855,f2558,f8357]) ).
fof(f9859,definition,
( sQ174_spl
<=> member(regular(singleton(y)),y) ),
introduced(definition,[new_symbols(definition,[sQ174_spl])],[split_symbol_definition]) ).
fof(f9862,plain,
( ~ sQ140_spl
| sQ35_spl
| ~ sQ174_spl ),
inference(split_clause,[status(thm)],[f9837,f9859,f2434,f8357]) ).
fof(f10047,plain,
( ~ sQ132_spl
| ~ member(not_subclass_element(unordered_pair(x,y),singleton(y)),singleton(y))
| ~ member(y,unordered_pair(x,y))
| unordered_pair(x,y) = singleton(y) ),
inference(paramodulation,[status(thm)],[f8239,f230]) ).
fof(f10048,plain,
( ~ sQ132_spl
| subclass(singleton(y),unordered_pair(x,y))
| ~ member(y,unordered_pair(x,y)) ),
inference(paramodulation,[status(thm)],[f8239,f114]) ).
fof(f10050,definition,
( sQ175_spl
<=> subclass(singleton(y),unordered_pair(x,y)) ),
introduced(definition,[new_symbols(definition,[sQ175_spl])],[split_symbol_definition]) ).
fof(f10051,plain,
( ~ sQ175_spl
| subclass(singleton(y),unordered_pair(x,y)) ),
inference(component_clause,[status(thm)],[f10050]) ).
fof(f10052,plain,
( sQ175_spl
| ~ subclass(singleton(y),unordered_pair(x,y)) ),
inference(component_clause,[status(thm)],[f10050]) ).
fof(f10054,plain,
( ~ sQ132_spl
| sQ175_spl
| ~ sQ143_spl ),
inference(split_clause,[status(thm)],[f10048,f8430,f10050,f8238]) ).
fof(f10055,definition,
( sQ176_spl
<=> unordered_pair(x,y) = singleton(y) ),
introduced(definition,[new_symbols(definition,[sQ176_spl])],[split_symbol_definition]) ).
fof(f10056,plain,
( ~ sQ176_spl
| unordered_pair(x,y) = singleton(y) ),
inference(component_clause,[status(thm)],[f10055]) ).
fof(f10058,definition,
( sQ177_spl
<=> member(not_subclass_element(unordered_pair(x,y),singleton(y)),singleton(y)) ),
introduced(definition,[new_symbols(definition,[sQ177_spl])],[split_symbol_definition]) ).
fof(f10060,plain,
( sQ177_spl
| ~ member(not_subclass_element(unordered_pair(x,y),singleton(y)),singleton(y)) ),
inference(component_clause,[status(thm)],[f10058]) ).
fof(f10061,plain,
( ~ sQ132_spl
| ~ sQ177_spl
| ~ sQ143_spl
| sQ176_spl ),
inference(split_clause,[status(thm)],[f10047,f10055,f8430,f10058,f8238]) ).
fof(f10073,plain,
( ~ sQ176_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f10056,f239]) ).
fof(f10074,plain,
~ sQ176_spl,
inference(contradiction_clause,[status(thm)],[f10073]) ).
fof(f10167,plain,
! [X0,X1] :
( ~ sQ141_spl
| y = ordered_pair(first(y),second(y))
| not_subclass_element(singleton(y),cross_product(X0,X1)) = y ),
inference(resolution,[status(thm)],[f8365,f134]) ).
fof(f10190,definition,
! [X1] :
( sQ182_spl
<=> ( y = not_subclass_element(singleton(y),X1)
| member(y,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ182_spl])],[split_symbol_definition]) ).
fof(f10195,definition,
! [X0,X1] :
( sQ183_spl
<=> not_subclass_element(singleton(y),cross_product(X0,X1)) = y ),
introduced(definition,[new_symbols(definition,[sQ183_spl])],[split_symbol_definition]) ).
fof(f10198,definition,
( sQ184_spl
<=> y = ordered_pair(first(y),second(y)) ),
introduced(definition,[new_symbols(definition,[sQ184_spl])],[split_symbol_definition]) ).
fof(f10201,plain,
( ~ sQ141_spl
| sQ184_spl
| sQ183_spl ),
inference(split_clause,[status(thm)],[f10167,f10195,f10198,f8361]) ).
fof(f10224,definition,
! [X0] :
( sQ185_spl
<=> subclass(singleton(y),X0) ),
introduced(definition,[new_symbols(definition,[sQ185_spl])],[split_symbol_definition]) ).
fof(f10225,plain,
! [X0] :
( ~ sQ185_spl
| subclass(singleton(y),X0) ),
inference(component_clause,[status(thm)],[f10224]) ).
fof(f10284,plain,
( sQ177_spl
| ~ sQ167_spl
| ~ member(y,singleton(y)) ),
inference(forward_demodulation,[status(thm)],[f9803,f10060]) ).
fof(f10285,plain,
( sQ177_spl
| ~ sQ167_spl
| ~ sQ141_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f10284,f8362]) ).
fof(f10286,plain,
( sQ177_spl
| ~ sQ167_spl
| ~ sQ141_spl ),
inference(contradiction_clause,[status(thm)],[f10285]) ).
fof(f10287,plain,
( sQ167_spl
| not_subclass_element(unordered_pair(x,y),singleton(y)) != y ),
inference(forward_demodulation,[status(thm)],[f126,f9790]) ).
fof(f10288,plain,
( ~ sQ133_spl
| sQ167_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f8242,f10287]) ).
fof(f10289,plain,
( ~ sQ133_spl
| sQ167_spl ),
inference(contradiction_clause,[status(thm)],[f10288]) ).
fof(f10497,plain,
( ~ sQ175_spl
| singleton(y) = unordered_pair(x,y)
| ~ subclass(unordered_pair(x,y),singleton(y)) ),
inference(resolution,[status(thm)],[f10051,f118]) ).
fof(f10504,definition,
( sQ207_spl
<=> subclass(unordered_pair(x,y),singleton(y)) ),
introduced(definition,[new_symbols(definition,[sQ207_spl])],[split_symbol_definition]) ).
fof(f10506,plain,
( sQ207_spl
| ~ subclass(unordered_pair(x,y),singleton(y)) ),
inference(component_clause,[status(thm)],[f10504]) ).
fof(f10507,plain,
( ~ sQ175_spl
| sQ176_spl
| ~ sQ207_spl ),
inference(split_clause,[status(thm)],[f10497,f10504,f10055,f10050]) ).
fof(f10676,plain,
! [X0,X1,X2] :
( ~ sQ122_spl
| regular(unordered_pair(X1,X2)) = X2
| regular(unordered_pair(X1,X2)) = X1
| sum_class(range_of(null_class)) = apply(X0,unordered_pair(X1,X2)) ),
inference(paramodulation,[status(thm)],[f8266,f187]) ).
fof(f10689,definition,
! [X0] :
( sQ215_spl
<=> ~ function(X0) ),
introduced(definition,[new_symbols(definition,[sQ215_spl])],[split_symbol_definition]) ).
fof(f10690,plain,
! [X0] :
( ~ sQ215_spl
| ~ function(X0) ),
inference(component_clause,[status(thm)],[f10689]) ).
fof(f10795,plain,
( ~ sQ131_spl
| member(x,unordered_pair(x,y))
| subclass(unordered_pair(x,y),singleton(y)) ),
inference(paramodulation,[status(thm)],[f8236,f113]) ).
fof(f10808,plain,
( ~ sQ131_spl
| sQ41_spl
| sQ207_spl ),
inference(split_clause,[status(thm)],[f10795,f10504,f2490,f8235]) ).
fof(f10982,plain,
! [X0,X1] :
( ~ sQ185_spl
| member(X0,X1)
| ~ member(X0,singleton(y)) ),
inference(resolution,[status(thm)],[f10225,f112]) ).
fof(f10985,plain,
! [X0] :
( ~ sQ140_spl
| ~ sQ185_spl
| ~ member(X0,singleton(y)) ),
inference(backward_subsumption_resolution,[status(thm)],[f8440,f10982]) ).
fof(f10986,plain,
( ~ sQ141_spl
| ~ sQ140_spl
| ~ sQ185_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f8362,f10985]) ).
fof(f10988,plain,
( ~ sQ141_spl
| ~ sQ140_spl
| ~ sQ185_spl ),
inference(contradiction_clause,[status(thm)],[f10986]) ).
fof(f11099,definition,
( sQ239_spl
<=> subclass(null_class,element_relation) ),
introduced(definition,[new_symbols(definition,[sQ239_spl])],[split_symbol_definition]) ).
fof(f11101,plain,
( sQ239_spl
| ~ subclass(null_class,element_relation) ),
inference(component_clause,[status(thm)],[f11099]) ).
fof(f11121,definition,
( sQ244_spl
<=> subclass(null_class,successor_relation) ),
introduced(definition,[new_symbols(definition,[sQ244_spl])],[split_symbol_definition]) ).
fof(f11123,plain,
( sQ244_spl
| ~ subclass(null_class,successor_relation) ),
inference(component_clause,[status(thm)],[f11121]) ).
fof(f11141,plain,
( sQ244_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f11123,f233]) ).
fof(f11142,plain,
sQ244_spl,
inference(contradiction_clause,[status(thm)],[f11141]) ).
fof(f11154,plain,
( sQ239_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f11101,f233]) ).
fof(f11155,plain,
sQ239_spl,
inference(contradiction_clause,[status(thm)],[f11154]) ).
fof(f11164,definition,
! [X0,X1,X2] :
( sQ251_spl
<=> restrict(X0,X1,X2) = intersection(X0,null_class) ),
introduced(definition,[new_symbols(definition,[sQ251_spl])],[split_symbol_definition]) ).
fof(f11165,plain,
! [X0,X1,X2] :
( ~ sQ251_spl
| intersection(X0,null_class) = restrict(X0,X1,X2) ),
inference(component_clause,[status(thm)],[f11164]) ).
fof(f11177,definition,
! [X0,X1] :
( sQ254_spl
<=> cross_product(X0,X1) = null_class ),
introduced(definition,[new_symbols(definition,[sQ254_spl])],[split_symbol_definition]) ).
fof(f11178,plain,
! [X0,X1] :
( ~ sQ254_spl
| cross_product(X0,X1) = null_class ),
inference(component_clause,[status(thm)],[f11177]) ).
fof(f11199,plain,
! [X0] :
( ~ sQ251_spl
| domain_of(intersection(element_relation,null_class)) = sum_class(X0) ),
inference(backward_demodulation,[status(thm)],[f11165,f172]) ).
fof(f11201,plain,
! [X0] :
( ~ sQ86_spl
| ~ sQ251_spl
| null_class = intersection(X0,null_class) ),
inference(backward_demodulation,[status(thm)],[f11165,f4774]) ).
fof(f11205,plain,
! [X0,X1,X2] :
( ~ sQ251_spl
| range(X0,X1,X2) = second(not_subclass_element(intersection(X0,null_class),null_class)) ),
inference(backward_demodulation,[status(thm)],[f11165,f160]) ).
fof(f11225,plain,
! [X0,X1,X2] :
( ~ sQ251_spl
| member(unordered_pair(X1,X2),sum_class(X0))
| intersection(restrict(element_relation,universal_class,X0),null_class) = null_class ),
inference(backward_demodulation,[status(thm)],[f11165,f1223]) ).
fof(f11229,plain,
! [X0] :
( ~ sQ251_spl
| ~ member(X0,subset_relation)
| member(X0,intersection(complement(compose(complement(element_relation),inverse(element_relation))),null_class)) ),
inference(backward_demodulation,[status(thm)],[f11165,f1148]) ).
fof(f11239,plain,
! [X0] :
( ~ sQ251_spl
| ~ operation(intersection(element_relation,null_class))
| subclass(range_of(restrict(element_relation,universal_class,X0)),domain_of(sum_class(X0))) ),
inference(backward_demodulation,[status(thm)],[f11165,f1902]) ).
fof(f11242,plain,
! [X0] :
( ~ sQ251_spl
| ~ function(intersection(element_relation,null_class))
| operation(restrict(element_relation,universal_class,X0))
| cross_product(domain_of(sum_class(X0)),domain_of(sum_class(X0))) != sum_class(X0)
| ~ subclass(range_of(restrict(element_relation,universal_class,X0)),domain_of(sum_class(X0))) ),
inference(backward_demodulation,[status(thm)],[f11165,f1478]) ).
fof(f11243,plain,
! [X0,X1,X2,X3,X4] :
( ~ sQ122_spl
| ~ sQ251_spl
| X3 = regular(unordered_pair(X3,X4))
| regular(unordered_pair(X3,X4)) = X4
| not_subclass_element(unordered_pair(X1,X2),singleton(unordered_pair(X3,X4))) = X1
| not_subclass_element(singleton(unordered_pair(X3,X4)),unordered_pair(X1,X2)) = unordered_pair(X3,X4)
| not_subclass_element(unordered_pair(X1,X2),singleton(unordered_pair(X3,X4))) = X2
| intersection(X0,null_class) = null_class ),
inference(backward_demodulation,[status(thm)],[f11165,f8250]) ).
fof(f11248,plain,
! [X0,X1,X2] :
( ~ sQ122_spl
| ~ sQ251_spl
| unordered_pair(singleton(X2),X1) = apply(choice,ordered_pair(X1,X2))
| singleton(X1) = apply(choice,ordered_pair(X1,X2))
| intersection(X0,null_class) = null_class ),
inference(backward_demodulation,[status(thm)],[f11165,f8625]) ).
fof(f11249,plain,
! [X0,X1,X2] :
( ~ sQ122_spl
| ~ sQ251_spl
| intersection(X2,null_class) = null_class
| apply(choice,ordered_pair(X0,X1)) = singleton(X0)
| unordered_pair(X0,singleton(X1)) = apply(choice,ordered_pair(X0,X1)) ),
inference(backward_demodulation,[status(thm)],[f11165,f8615]) ).
fof(f11250,plain,
! [X0,X1,X2] :
( ~ sQ122_spl
| ~ sQ251_spl
| unordered_pair(singleton(X1),X0) = not_subclass_element(ordered_pair(X0,X1),null_class)
| intersection(X2,null_class) = null_class
| singleton(X0) = not_subclass_element(ordered_pair(X0,X1),null_class) ),
inference(backward_demodulation,[status(thm)],[f11165,f8554]) ).
fof(f11251,plain,
! [X0,X1,X2] :
( ~ sQ122_spl
| ~ sQ251_spl
| intersection(X2,null_class) = null_class
| singleton(X0) = not_subclass_element(ordered_pair(X0,X1),null_class)
| not_subclass_element(ordered_pair(X0,X1),null_class) = unordered_pair(X0,singleton(X1)) ),
inference(backward_demodulation,[status(thm)],[f11165,f8545]) ).
fof(f11254,plain,
! [X0,X1] :
( ~ sQ122_spl
| ~ sQ251_spl
| intersection(X1,null_class) = null_class
| X0 = regular(singleton(X0)) ),
inference(backward_demodulation,[status(thm)],[f11165,f8288]) ).
fof(f11255,plain,
! [X0,X1,X2,X3] :
( ~ sQ122_spl
| ~ sQ251_spl
| regular(unordered_pair(X0,X1)) = X1
| not_subclass_element(unordered_pair(X0,X1),singleton(X3)) = X0
| X3 = not_subclass_element(singleton(X3),unordered_pair(X0,X1))
| X1 = not_subclass_element(unordered_pair(X0,X1),singleton(X3))
| intersection(X2,null_class) = null_class
| X0 = regular(unordered_pair(X0,X1)) ),
inference(backward_demodulation,[status(thm)],[f11165,f8255]) ).
fof(f11256,plain,
! [X0,X1] :
( ~ sQ122_spl
| ~ sQ251_spl
| null_class = intersection(X1,null_class)
| apply(choice,singleton(X0)) = X0 ),
inference(backward_demodulation,[status(thm)],[f11165,f8628]) ).
fof(f11257,plain,
! [X0,X1] :
( ~ sQ122_spl
| ~ sQ251_spl
| intersection(X1,null_class) = null_class
| X0 = not_subclass_element(singleton(X0),null_class) ),
inference(backward_demodulation,[status(thm)],[f11165,f8548]) ).
fof(f11258,plain,
! [X0,X1,X2] :
( ~ sQ122_spl
| ~ sQ251_spl
| regular(unordered_pair(X0,X1)) = X1
| null_class = intersection(X2,null_class)
| regular(unordered_pair(X0,X1)) = X0 ),
inference(backward_demodulation,[status(thm)],[f11165,f8075]) ).
fof(f11266,plain,
! [X0,X1,X2,X3] :
( ~ sQ251_spl
| domain_of(domain_of(X3)) != domain_of(intersection(X0,null_class))
| compatible(restrict(X0,X1,universal_class),X3,X2)
| ~ function(restrict(X0,X1,universal_class))
| ~ subclass(image(X0,X1),domain_of(domain_of(X2))) ),
inference(backward_demodulation,[status(thm)],[f11165,f2152]) ).
fof(f11288,definition,
! [X0] :
( sQ258_spl
<=> ( operation(restrict(element_relation,universal_class,X0))
| cross_product(domain_of(sum_class(X0)),domain_of(sum_class(X0))) != sum_class(X0)
| ~ subclass(range_of(restrict(element_relation,universal_class,X0)),domain_of(sum_class(X0))) ) ),
introduced(definition,[new_symbols(definition,[sQ258_spl])],[split_symbol_definition]) ).
fof(f11291,definition,
( sQ259_spl
<=> function(intersection(element_relation,null_class)) ),
introduced(definition,[new_symbols(definition,[sQ259_spl])],[split_symbol_definition]) ).
fof(f11294,plain,
( ~ sQ251_spl
| ~ sQ259_spl
| sQ258_spl ),
inference(split_clause,[status(thm)],[f11242,f11288,f11291,f11164]) ).
fof(f11295,plain,
! [X0,X1,X2] :
( ~ sQ251_spl
| null_class = intersection(intersection(element_relation,null_class),null_class)
| member(unordered_pair(X0,X1),sum_class(X2)) ),
inference(forward_demodulation,[status(thm)],[f11165,f11225]) ).
fof(f11296,plain,
! [X0,X1,X2,X3] :
( ~ sQ251_spl
| domain_of(domain_of(X3)) != domain_of(intersection(X0,null_class))
| compatible(restrict(X0,X1,universal_class),X3,X2)
| ~ function(intersection(X0,null_class))
| ~ subclass(image(X0,X1),domain_of(domain_of(X2))) ),
inference(forward_demodulation,[status(thm)],[f11165,f11266]) ).
fof(f11297,plain,
! [X0,X1,X2,X3] :
( ~ sQ251_spl
| ~ function(intersection(X0,null_class))
| ~ subclass(image(X0,X3),domain_of(domain_of(X2)))
| domain_of(domain_of(X1)) != domain_of(intersection(X0,null_class))
| compatible(intersection(X0,null_class),X1,X2) ),
inference(forward_demodulation,[status(thm)],[f11165,f11296]) ).
fof(f11298,plain,
! [X0,X1] :
( ~ sQ251_spl
| apply(X0,X1) = domain_of(intersection(element_relation,null_class)) ),
inference(backward_demodulation,[status(thm)],[f11199,f187]) ).
fof(f11309,definition,
! [X0] :
( sQ260_spl
<=> subclass(range_of(restrict(element_relation,universal_class,X0)),domain_of(sum_class(X0))) ),
introduced(definition,[new_symbols(definition,[sQ260_spl])],[split_symbol_definition]) ).
fof(f11312,definition,
( sQ261_spl
<=> operation(intersection(element_relation,null_class)) ),
introduced(definition,[new_symbols(definition,[sQ261_spl])],[split_symbol_definition]) ).
fof(f11315,plain,
( ~ sQ251_spl
| ~ sQ261_spl
| sQ260_spl ),
inference(split_clause,[status(thm)],[f11239,f11309,f11312,f11164]) ).
fof(f11337,plain,
! [X0,X1] :
( ~ sQ122_spl
| ~ sQ251_spl
| regular(unordered_pair(X0,X1)) = X1
| regular(unordered_pair(X0,X1)) = X0
| sum_class(range_of(null_class)) = domain_of(intersection(element_relation,null_class)) ),
inference(backward_demodulation,[status(thm)],[f11298,f10676]) ).
fof(f11348,plain,
! [X0,X1] :
( ~ sQ251_spl
| ~ sQ86_spl
| apply(X0,X1) = domain_of(null_class) ),
inference(backward_demodulation,[status(thm)],[f11201,f11298]) ).
fof(f11350,plain,
! [X0,X1,X2] :
( ~ sQ251_spl
| ~ sQ86_spl
| null_class = intersection(null_class,null_class)
| member(unordered_pair(X0,X1),sum_class(X2)) ),
inference(backward_demodulation,[status(thm)],[f11201,f11295]) ).
fof(f11358,plain,
! [X0,X1,X2,X3] :
( ~ sQ251_spl
| ~ sQ86_spl
| ~ function(null_class)
| ~ subclass(image(X0,X3),domain_of(domain_of(X2)))
| domain_of(domain_of(X1)) != domain_of(intersection(X0,null_class))
| compatible(intersection(X0,null_class),X1,X2) ),
inference(backward_demodulation,[status(thm)],[f11201,f11297]) ).
fof(f11410,plain,
! [X0] :
( ~ sQ251_spl
| ~ sQ86_spl
| ~ member(X0,subset_relation)
| member(X0,null_class) ),
inference(forward_demodulation,[status(thm)],[f11201,f11229]) ).
fof(f11415,plain,
! [X0] :
( ~ sQ17_spl
| ~ sQ251_spl
| ~ sQ86_spl
| ~ member(X0,omega) ),
inference(backward_subsumption_resolution,[status(thm)],[f1243,f11418]) ).
fof(f11418,plain,
! [X0] :
( ~ sQ251_spl
| ~ sQ86_spl
| ~ member(X0,subset_relation) ),
inference(forward_subsumption_resolution,[status(thm)],[f11410,f232]) ).
fof(f11423,definition,
! [X0] :
( sQ264_spl
<=> X0 = not_subclass_element(singleton(X0),null_class) ),
introduced(definition,[new_symbols(definition,[sQ264_spl])],[split_symbol_definition]) ).
fof(f11426,definition,
! [X1] :
( sQ265_spl
<=> intersection(X1,null_class) = null_class ),
introduced(definition,[new_symbols(definition,[sQ265_spl])],[split_symbol_definition]) ).
fof(f11429,plain,
( ~ sQ122_spl
| ~ sQ251_spl
| sQ265_spl
| sQ264_spl ),
inference(split_clause,[status(thm)],[f11257,f11423,f11426,f11164,f8069]) ).
fof(f11469,definition,
! [X0] :
( sQ266_spl
<=> apply(choice,singleton(X0)) = X0 ),
introduced(definition,[new_symbols(definition,[sQ266_spl])],[split_symbol_definition]) ).
fof(f11472,plain,
( ~ sQ122_spl
| ~ sQ251_spl
| sQ265_spl
| sQ266_spl ),
inference(split_clause,[status(thm)],[f11256,f11469,f11426,f11164,f8069]) ).
fof(f11508,definition,
! [X0,X1,X2,X3] :
( sQ267_spl
<=> ( ~ subclass(image(X0,X3),domain_of(domain_of(X2)))
| domain_of(domain_of(X1)) != domain_of(intersection(X0,null_class))
| compatible(intersection(X0,null_class),X1,X2) ) ),
introduced(definition,[new_symbols(definition,[sQ267_spl])],[split_symbol_definition]) ).
fof(f11511,definition,
( sQ268_spl
<=> function(null_class) ),
introduced(definition,[new_symbols(definition,[sQ268_spl])],[split_symbol_definition]) ).
fof(f11514,plain,
( ~ sQ251_spl
| ~ sQ86_spl
| ~ sQ268_spl
| sQ267_spl ),
inference(split_clause,[status(thm)],[f11358,f11508,f11511,f4773,f11164]) ).
fof(f11555,definition,
( sQ269_spl
<=> sum_class(range_of(null_class)) = domain_of(intersection(element_relation,null_class)) ),
introduced(definition,[new_symbols(definition,[sQ269_spl])],[split_symbol_definition]) ).
fof(f11558,plain,
( ~ sQ122_spl
| ~ sQ251_spl
| sQ77_spl
| sQ269_spl ),
inference(split_clause,[status(thm)],[f11337,f11555,f4189,f11164,f8069]) ).
fof(f11559,definition,
! [X0,X1,X3] :
( sQ270_spl
<=> ( regular(unordered_pair(X0,X1)) = X1
| not_subclass_element(unordered_pair(X0,X1),singleton(X3)) = X0
| X3 = not_subclass_element(singleton(X3),unordered_pair(X0,X1))
| X1 = not_subclass_element(unordered_pair(X0,X1),singleton(X3))
| X0 = regular(unordered_pair(X0,X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ270_spl])],[split_symbol_definition]) ).
fof(f11562,plain,
( ~ sQ122_spl
| ~ sQ251_spl
| sQ265_spl
| sQ270_spl ),
inference(split_clause,[status(thm)],[f11255,f11559,f11426,f11164,f8069]) ).
fof(f11599,plain,
! [X0,X1,X2,X3] :
( ~ sQ254_spl
| member(ordered_pair(X0,X2),null_class)
| ~ member(X2,X3)
| ~ member(X0,X1) ),
inference(backward_demodulation,[status(thm)],[f11178,f132]) ).
fof(f11721,definition,
! [X0,X1] :
( sQ273_spl
<=> ( singleton(X0) = not_subclass_element(ordered_pair(X0,X1),null_class)
| not_subclass_element(ordered_pair(X0,X1),null_class) = unordered_pair(X0,singleton(X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ273_spl])],[split_symbol_definition]) ).
fof(f11724,plain,
( ~ sQ122_spl
| ~ sQ251_spl
| sQ265_spl
| sQ273_spl ),
inference(split_clause,[status(thm)],[f11251,f11721,f11426,f11164,f8069]) ).
fof(f11728,plain,
! [X0,X1] :
( ~ sQ251_spl
| ~ sQ86_spl
| member(domain_of(null_class),universal_class)
| ~ member(image(X0,singleton(X1)),universal_class) ),
inference(backward_demodulation,[status(thm)],[f11348,f3877]) ).
fof(f11741,plain,
( ~ sQ122_spl
| ~ sQ251_spl
| sQ265_spl
| sQ77_spl ),
inference(split_clause,[status(thm)],[f11258,f4189,f11426,f11164,f8069]) ).
fof(f11751,definition,
! [X0,X1] :
( sQ275_spl
<=> ( apply(choice,ordered_pair(X0,X1)) = singleton(X0)
| unordered_pair(X0,singleton(X1)) = apply(choice,ordered_pair(X0,X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ275_spl])],[split_symbol_definition]) ).
fof(f11754,plain,
( ~ sQ122_spl
| ~ sQ251_spl
| sQ265_spl
| sQ275_spl ),
inference(split_clause,[status(thm)],[f11249,f11751,f11426,f11164,f8069]) ).
fof(f11771,definition,
! [X0,X1,X2] :
( sQ276_spl
<=> member(unordered_pair(X0,X1),sum_class(X2)) ),
introduced(definition,[new_symbols(definition,[sQ276_spl])],[split_symbol_definition]) ).
fof(f11774,definition,
( sQ277_spl
<=> null_class = intersection(null_class,null_class) ),
introduced(definition,[new_symbols(definition,[sQ277_spl])],[split_symbol_definition]) ).
fof(f11777,plain,
( ~ sQ251_spl
| ~ sQ86_spl
| sQ277_spl
| sQ276_spl ),
inference(split_clause,[status(thm)],[f11350,f11771,f11774,f4773,f11164]) ).
fof(f11783,definition,
! [X0,X1] :
( sQ279_spl
<=> ( unordered_pair(singleton(X1),X0) = not_subclass_element(ordered_pair(X0,X1),null_class)
| singleton(X0) = not_subclass_element(ordered_pair(X0,X1),null_class) ) ),
introduced(definition,[new_symbols(definition,[sQ279_spl])],[split_symbol_definition]) ).
fof(f11786,plain,
( ~ sQ122_spl
| ~ sQ251_spl
| sQ265_spl
| sQ279_spl ),
inference(split_clause,[status(thm)],[f11250,f11783,f11426,f11164,f8069]) ).
fof(f11798,plain,
( ~ sQ17_spl
| ~ sQ251_spl
| ~ sQ86_spl
| sQ7_spl ),
inference(split_clause,[status(thm)],[f11415,f1009,f4773,f11164,f1242]) ).
fof(f11809,definition,
! [X1,X2,X3,X4] :
( sQ280_spl
<=> ( X3 = regular(unordered_pair(X3,X4))
| regular(unordered_pair(X3,X4)) = X4
| not_subclass_element(unordered_pair(X1,X2),singleton(unordered_pair(X3,X4))) = X1
| not_subclass_element(singleton(unordered_pair(X3,X4)),unordered_pair(X1,X2)) = unordered_pair(X3,X4)
| not_subclass_element(unordered_pair(X1,X2),singleton(unordered_pair(X3,X4))) = X2 ) ),
introduced(definition,[new_symbols(definition,[sQ280_spl])],[split_symbol_definition]) ).
fof(f11812,plain,
( ~ sQ122_spl
| ~ sQ251_spl
| sQ280_spl
| sQ265_spl ),
inference(split_clause,[status(thm)],[f11243,f11426,f11809,f11164,f8069]) ).
fof(f11825,plain,
! [X0] :
( ~ sQ254_spl
| ~ member(X0,universal_class) ),
inference(backward_subsumption_resolution,[status(thm)],[f175,f11870]) ).
fof(f11870,plain,
! [X0,X1,X2,X3] :
( ~ sQ254_spl
| ~ member(X2,X3)
| ~ member(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f11599,f232]) ).
fof(f11916,plain,
! [X0,X1] :
( ~ sQ122_spl
| ~ sQ251_spl
| ~ sQ86_spl
| second(not_subclass_element(null_class,null_class)) = second(not_subclass_element(null_class,null_class))
| regular(unordered_pair(X0,X1)) = X1
| regular(unordered_pair(X0,X1)) = X0 ),
inference(backward_demodulation,[status(thm)],[f11920,f8265]) ).
fof(f11920,plain,
! [X0,X1,X2] :
( ~ sQ251_spl
| ~ sQ86_spl
| second(not_subclass_element(null_class,null_class)) = range(X0,X1,X2) ),
inference(forward_demodulation,[status(thm)],[f11201,f11205]) ).
fof(f11964,plain,
( ~ sQ122_spl
| ~ sQ251_spl
| sQ265_spl
| sQ130_spl ),
inference(split_clause,[status(thm)],[f11254,f8192,f11426,f11164,f8069]) ).
fof(f11965,definition,
! [X1,X2] :
( sQ287_spl
<=> ( unordered_pair(singleton(X2),X1) = apply(choice,ordered_pair(X1,X2))
| singleton(X1) = apply(choice,ordered_pair(X1,X2)) ) ),
introduced(definition,[new_symbols(definition,[sQ287_spl])],[split_symbol_definition]) ).
fof(f11968,plain,
( ~ sQ122_spl
| ~ sQ251_spl
| sQ287_spl
| sQ265_spl ),
inference(split_clause,[status(thm)],[f11248,f11426,f11965,f11164,f8069]) ).
fof(f11985,definition,
( sQ289_spl
<=> second(not_subclass_element(null_class,null_class)) = second(not_subclass_element(null_class,null_class)) ),
introduced(definition,[new_symbols(definition,[sQ289_spl])],[split_symbol_definition]) ).
fof(f11988,plain,
( ~ sQ122_spl
| ~ sQ251_spl
| ~ sQ86_spl
| sQ289_spl
| sQ77_spl ),
inference(split_clause,[status(thm)],[f11916,f4189,f11985,f4773,f11164,f8069]) ).
fof(f12021,definition,
! [X0,X1] :
( sQ295_spl
<=> ~ member(image(X0,singleton(X1)),universal_class) ),
introduced(definition,[new_symbols(definition,[sQ295_spl])],[split_symbol_definition]) ).
fof(f12024,definition,
( sQ296_spl
<=> member(domain_of(null_class),universal_class) ),
introduced(definition,[new_symbols(definition,[sQ296_spl])],[split_symbol_definition]) ).
fof(f12027,plain,
( ~ sQ251_spl
| ~ sQ86_spl
| sQ296_spl
| sQ295_spl ),
inference(split_clause,[status(thm)],[f11728,f12021,f12024,f4773,f11164]) ).
fof(f12028,plain,
( ~ sQ254_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f236,f11825]) ).
fof(f12043,plain,
~ sQ254_spl,
inference(contradiction_clause,[status(thm)],[f12028]) ).
fof(f12082,plain,
( ~ sQ215_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f188,f10690]) ).
fof(f12093,plain,
~ sQ215_spl,
inference(contradiction_clause,[status(thm)],[f12082]) ).
fof(f12212,definition,
( sQ297_spl
<=> member(not_subclass_element(null_class,singleton(y)),null_class) ),
introduced(definition,[new_symbols(definition,[sQ297_spl])],[split_symbol_definition]) ).
fof(f12213,plain,
( ~ sQ297_spl
| member(not_subclass_element(null_class,singleton(y)),null_class) ),
inference(component_clause,[status(thm)],[f12212]) ).
fof(f12296,plain,
! [X0] :
( inductive(universal_class)
| ~ subclass(image(successor_relation,universal_class),universal_class)
| ~ member(null_class,X0) ),
inference(resolution,[status(thm)],[f461,f168]) ).
fof(f12300,plain,
( sQ150_spl
| ~ sQ149_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f12296,f493,f8850,f8853]) ).
fof(f12325,plain,
( sQ207_spl
| not_subclass_element(unordered_pair(x,y),singleton(y)) = x
| y = not_subclass_element(unordered_pair(x,y),singleton(y)) ),
inference(resolution,[status(thm)],[f10506,f1278]) ).
fof(f12331,plain,
( sQ207_spl
| sQ131_spl
| sQ133_spl ),
inference(split_clause,[status(thm)],[f12325,f8241,f8235,f10504]) ).
fof(f12335,definition,
( sQ302_spl
<=> not_subclass_element(unordered_pair(y,x),singleton(y)) = y ),
introduced(definition,[new_symbols(definition,[sQ302_spl])],[split_symbol_definition]) ).
fof(f12336,plain,
( ~ sQ302_spl
| not_subclass_element(unordered_pair(y,x),singleton(y)) = y ),
inference(component_clause,[status(thm)],[f12335]) ).
fof(f12554,plain,
( sQ175_spl
| y = not_subclass_element(singleton(y),unordered_pair(x,y)) ),
inference(resolution,[status(thm)],[f10052,f1272]) ).
fof(f12560,plain,
( sQ175_spl
| sQ132_spl ),
inference(split_clause,[status(thm)],[f12554,f8238,f10050]) ).
fof(f12561,plain,
( ~ sQ302_spl
| not_subclass_element(unordered_pair(x,y),singleton(y)) = y ),
inference(forward_demodulation,[status(thm)],[f237,f12336]) ).
fof(f12662,plain,
( sQ33_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2401,f236]) ).
fof(f12663,plain,
sQ33_spl,
inference(contradiction_clause,[status(thm)],[f12662]) ).
fof(f12974,plain,
( ~ sQ167_spl
| subclass(unordered_pair(x,y),singleton(y))
| ~ member(y,singleton(y)) ),
inference(paramodulation,[status(thm)],[f9803,f114]) ).
fof(f12978,plain,
( ~ sQ167_spl
| sQ207_spl
| ~ sQ141_spl ),
inference(split_clause,[status(thm)],[f12974,f8361,f10504,f9788]) ).
fof(f12997,plain,
( ~ sQ35_spl
| null_class != unordered_pair(x,y) ),
inference(backward_demodulation,[status(thm)],[f2435,f239]) ).
fof(f13076,plain,
( ~ sQ35_spl
| ~ sQ40_spl ),
inference(split_clause,[status(thm)],[f12997,f2487,f2434]) ).
fof(f13386,plain,
( ~ sQ297_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f12213,f232]) ).
fof(f13387,plain,
~ sQ297_spl,
inference(contradiction_clause,[status(thm)],[f13386]) ).
fof(f13391,plain,
( ~ sQ302_spl
| sQ133_spl ),
inference(split_clause,[status(thm)],[f12561,f8241,f12335]) ).
fof(f13539,plain,
( ~ sQ141_spl
| sQ182_spl ),
inference(split_clause,[status(thm)],[f8365,f10190,f8361]) ).
fof(f13552,plain,
( ~ sQ141_spl
| ~ sQ44_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f8362,f2559]) ).
fof(f13553,plain,
( ~ sQ141_spl
| ~ sQ44_spl ),
inference(contradiction_clause,[status(thm)],[f13552]) ).
fof(f13554,plain,
$false,
inference(sat_refutation,[status(thm)],[f499,f502,f528,f549,f1097,f1134,f1248,f1398,f1402,f1465,f1690,f1996,f2003,f2317,f2466,f2493,f2495,f2514,f2561,f2679,f2691,f2828,f2909,f3035,f3107,f3837,f3838,f3875,f3912,f4235,f4415,f4788,f5222,f5260,f5970,f7064,f7066,f8072,f8186,f8201,f8216,f8218,f8219,f8246,f8268,f8281,f8285,f8289,f8293,f8360,f8364,f8428,f8538,f8539,f8552,f8572,f8619,f8629,f8658,f8671,f8732,f8832,f8860,f8864,f8869,f8873,f8875,f8877,f9013,f9016,f9045,f9448,f9450,f9529,f9535,f9578,f9581,f9730,f9847,f9858,f9862,f10054,f10061,f10074,f10201,f10286,f10289,f10507,f10808,f10988,f11142,f11155,f11294,f11315,f11429,f11472,f11514,f11558,f11562,f11724,f11741,f11754,f11777,f11786,f11798,f11812,f11964,f11968,f11988,f12027,f12043,f12093,f12300,f12331,f12560,f12663,f12978,f13076,f13387,f13391,f13539,f13553]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SET070-7 : TPTP v9.3.1. Bugfixed v2.1.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n002.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:52:04 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.38 % Drodi V4.1.1
% 131.50/17.52 % Refutation found
% 131.50/17.52 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 131.50/17.52 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 8.79/17.82 % Elapsed time: 17.442291 seconds
% 8.79/17.82 % CPU time: 136.643266 seconds
% 8.79/17.82 % Total memory used: 791.339 MB
% 8.79/17.82 % Net memory used: 694.900 MB
%------------------------------------------------------------------------------