%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SET069-7 : TPTP v9.3.1. Bugfixed v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n016.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:10 PM UTC 2026
% Result : Unsatisfiable 230.69s 30.05s
% Output : CNFRefutation 230.69s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 187
% Syntax : Number of formulae : 728 ( 83 unt; 126 def)
% Number of atoms : 1848 ( 497 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 1878 ( 758 ~; 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/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [X,Y] :
( subclass(X,Y)
| member(not_subclass_element(X,Y),X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [X,Y] :
( subclass(X,Y)
| ~ member(not_subclass_element(X,Y),Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [X] : subclass(X,universal_class),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [X,Y] :
( subclass(Y,X)
| X != Y ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [X,Y] :
( X = Y
| ~ subclass(Y,X)
| ~ subclass(X,Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [U,X,Y] :
( U = Y
| U = X
| ~ member(U,unordered_pair(X,Y)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [X,Y] :
( member(X,unordered_pair(X,Y))
| ~ member(X,universal_class) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f10,axiom,
! [Y,X] :
( member(Y,unordered_pair(X,Y))
| ~ member(Y,universal_class) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f11,axiom,
! [X,Y] : member(unordered_pair(X,Y),universal_class),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [X] : unordered_pair(X,X) = singleton(X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f13,axiom,
! [X,Y] : unordered_pair(singleton(X),unordered_pair(X,singleton(Y))) = ordered_pair(X,Y),
file('/export/starexec/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/benchmark/theBenchmark.p') ).
fof(f18,axiom,
subclass(element_relation,cross_product(universal_class,universal_class)),
file('/export/starexec/sandbox2/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/sandbox2/benchmark/theBenchmark.p') ).
fof(f22,axiom,
! [Z,X,Y] :
( member(Z,Y)
| ~ member(Z,intersection(X,Y)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f23,axiom,
! [Z,X,Y] :
( member(Z,intersection(X,Y))
| ~ member(Z,Y)
| ~ member(Z,X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f24,axiom,
! [Z,X] :
( ~ member(Z,X)
| ~ member(Z,complement(X)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f25,axiom,
! [Z,X] :
( member(Z,X)
| member(Z,complement(X))
| ~ member(Z,universal_class) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f29,axiom,
! [X,Y,Xr] : intersection(cross_product(X,Y),Xr) = restrict(Xr,X,Y),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f30,axiom,
! [X,Z] :
( ~ member(Z,domain_of(X))
| restrict(X,singleton(Z),universal_class) != null_class ),
file('/export/starexec/sandbox2/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/sandbox2/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/sandbox2/benchmark/theBenchmark.p') ).
fof(f42,axiom,
! [Xr,X] : range_of(restrict(Xr,X,universal_class)) = image(Xr,X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f47,axiom,
! [X] :
( member(null_class,X)
| ~ inductive(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f48,axiom,
! [X] :
( subclass(image(successor_relation,X),X)
| ~ inductive(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f49,axiom,
! [X] :
( inductive(X)
| ~ subclass(image(successor_relation,X),X)
| ~ member(null_class,X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f50,axiom,
inductive(omega),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f51,axiom,
! [Y] :
( subclass(omega,Y)
| ~ inductive(Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f53,axiom,
! [X] : domain_of(restrict(element_relation,universal_class,X)) = sum_class(X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f54,axiom,
! [X] :
( member(sum_class(X),universal_class)
| ~ member(X,universal_class) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f55,axiom,
! [X] : complement(image(element_relation,complement(X))) = power_class(X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f56,axiom,
! [U] :
( member(power_class(U),universal_class)
| ~ member(U,universal_class) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f62,axiom,
! [Xf] :
( subclass(Xf,cross_product(universal_class,universal_class))
| ~ function(Xf) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f66,axiom,
! [X] :
( member(regular(X),X)
| X = null_class ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f67,axiom,
! [X] :
( intersection(X,regular(X)) = null_class
| X = null_class ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f68,axiom,
! [Xf,Y] : sum_class(image(Xf,singleton(Y))) = apply(Xf,Y),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f69,axiom,
function(choice),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f70,axiom,
! [Y] :
( member(apply(choice,Y),Y)
| Y = null_class
| ~ member(Y,universal_class) ),
file('/export/starexec/sandbox2/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/sandbox2/benchmark/theBenchmark.p') ).
fof(f75,axiom,
intersection(inverse(subset_relation),subset_relation) = identity_relation,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f80,axiom,
! [Xf] :
( subclass(range_of(Xf),domain_of(domain_of(Xf)))
| ~ operation(Xf) ),
file('/export/starexec/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/benchmark/theBenchmark.p') ).
fof(f97,axiom,
! [X,Y,Z] :
( subclass(X,Z)
| ~ subclass(Y,Z)
| ~ subclass(X,Y) ),
file('/export/starexec/sandbox2/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/sandbox2/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/sandbox2/benchmark/theBenchmark.p') ).
fof(f103,axiom,
! [Z] : ~ member(Z,null_class),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f104,axiom,
! [X] : subclass(null_class,X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f105,axiom,
! [X] :
( X = null_class
| ~ subclass(X,null_class) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f106,axiom,
! [Z] :
( member(not_subclass_element(Z,null_class),Z)
| Z = null_class ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f107,axiom,
member(null_class,universal_class),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f108,axiom,
! [X,Y] : unordered_pair(X,Y) = unordered_pair(Y,X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f109,negated_conjecture,
~ member(y,universal_class),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f110,negated_conjecture,
unordered_pair(x,y) != singleton(x),
file('/export/starexec/sandbox2/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(y,universal_class),
inference(cnf_transformation,[status(thm)],[f109]) ).
fof(f239,plain,
unordered_pair(x,y) != singleton(x),
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,
singleton(x) != unordered_pair(y,x),
inference(forward_demodulation,[status(thm)],[f237,f239]) ).
fof(f244,plain,
! [X0] : subclass(X0,X0),
inference(destructive_equality_resolution,[status(thm)],[f117]) ).
fof(f255,plain,
! [X0,X1] : ordered_pair(X0,X1) = unordered_pair(singleton(X0),unordered_pair(singleton(X1),X0)),
inference(paramodulation,[status(thm)],[f237,f127]) ).
fof(f258,plain,
! [X0] : unordered_pair(singleton(singleton(X0)),singleton(singleton(X0))) = ordered_pair(singleton(X0),X0),
inference(paramodulation,[status(thm)],[f126,f127]) ).
fof(f259,plain,
! [X0,X1] :
( X0 = X1
| X1 = X0
| ~ member(X0,singleton(X1)) ),
inference(paramodulation,[status(thm)],[f126,f120]) ).
fof(f260,plain,
! [X0] : singleton(singleton(singleton(X0))) = ordered_pair(singleton(X0),X0),
inference(forward_demodulation,[status(thm)],[f126,f258]) ).
fof(f261,plain,
! [X0,X1] :
( ~ member(X1,singleton(X0))
| X0 = X1 ),
inference(duplicate_literals_removal,[status(thm)],[f259]) ).
fof(f263,plain,
! [X0,X1,X2] : member(unordered_pair(X0,X1),unordered_pair(X2,unordered_pair(X0,X1))),
inference(resolution,[status(thm)],[f125,f124]) ).
fof(f264,plain,
! [X0,X1] : member(ordered_pair(X0,X1),universal_class),
inference(paramodulation,[status(thm)],[f127,f125]) ).
fof(f265,plain,
! [X0] : member(singleton(X0),universal_class),
inference(paramodulation,[status(thm)],[f126,f125]) ).
fof(f324,plain,
! [X0,X1] :
( ~ member(X0,ordered_pair(singleton(X1),X1))
| X0 = singleton(singleton(X1)) ),
inference(paramodulation,[status(thm)],[f260,f261]) ).
fof(f369,plain,
! [X0,X1,X2,X3] :
( ~ member(X0,restrict(X1,X2,X3))
| member(X0,X1) ),
inference(paramodulation,[status(thm)],[f148,f141]) ).
fof(f462,plain,
! [X0,X1] :
( member(X0,universal_class)
| ~ member(X0,X1) ),
inference(resolution,[status(thm)],[f112,f115]) ).
fof(f466,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(f467,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(f469,plain,
! [X0] :
( ~ subclass(X0,universal_class)
| ~ member(y,X0) ),
inference(resolution,[status(thm)],[f112,f238]) ).
fof(f470,plain,
! [X0,X1,X2,X3] :
( ~ subclass(X1,intersection(X3,X2))
| member(X0,X2)
| ~ member(X0,X1) ),
inference(resolution,[status(thm)],[f112,f141]) ).
fof(f475,plain,
! [X0,X1] :
( ~ subclass(X1,null_class)
| ~ member(X0,X1) ),
inference(resolution,[status(thm)],[f112,f232]) ).
fof(f477,plain,
! [X0,X1,X2] :
( member(X0,unordered_pair(X0,X2))
| ~ subclass(X1,universal_class)
| ~ member(X0,X1) ),
inference(resolution,[status(thm)],[f112,f122]) ).
fof(f478,plain,
! [X0,X1,X2] :
( member(X0,unordered_pair(X2,X0))
| ~ subclass(X1,universal_class)
| ~ member(X0,X1) ),
inference(resolution,[status(thm)],[f112,f124]) ).
fof(f479,plain,
! [X0,X1,X2] :
( member(X0,unordered_pair(X2,X0))
| ~ member(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f478,f115]) ).
fof(f480,plain,
! [X0] : ~ member(y,X0),
inference(forward_subsumption_resolution,[status(thm)],[f469,f115]) ).
fof(f481,plain,
! [X0,X1,X2] :
( member(X0,unordered_pair(X0,X2))
| ~ member(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f477,f115]) ).
fof(f485,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)],[f479,f168]) ).
fof(f491,plain,
! [X0,X1] :
( ~ member(X0,X1)
| member(X0,singleton(X0)) ),
inference(paramodulation,[status(thm)],[f126,f479]) ).
fof(f494,definition,
! [X0] :
( sQ0_spl
<=> ~ member(null_class,X0) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f495,plain,
! [X0] :
( ~ sQ0_spl
| ~ member(null_class,X0) ),
inference(component_clause,[status(thm)],[f494]) ).
fof(f497,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(f498,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)],[f497]) ).
fof(f500,plain,
( sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f485,f494,f497]) ).
fof(f501,plain,
( ~ sQ0_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f236,f495]) ).
fof(f503,plain,
~ sQ0_spl,
inference(contradiction_clause,[status(thm)],[f501]) ).
fof(f515,plain,
! [X0,X1,X2,X3] :
( ~ subclass(universal_class,cross_product(X2,X3))
| member(X0,unordered_pair(X0,X1)) ),
inference(resolution,[status(thm)],[f467,f264]) ).
fof(f523,definition,
! [X0,X1] :
( sQ2_spl
<=> member(X0,unordered_pair(X0,X1)) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f524,plain,
! [X0,X1] :
( ~ sQ2_spl
| member(X0,unordered_pair(X0,X1)) ),
inference(component_clause,[status(thm)],[f523]) ).
fof(f526,definition,
! [X2,X3] :
( sQ3_spl
<=> ~ subclass(universal_class,cross_product(X2,X3)) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f527,plain,
! [X0,X1] :
( ~ sQ3_spl
| ~ subclass(universal_class,cross_product(X0,X1)) ),
inference(component_clause,[status(thm)],[f526]) ).
fof(f529,plain,
( sQ3_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f515,f523,f526]) ).
fof(f541,plain,
( ~ sQ2_spl
| $false ),
inference(resolution,[status(thm)],[f524,f480]) ).
fof(f550,plain,
~ sQ2_spl,
inference(contradiction_clause,[status(thm)],[f541]) ).
fof(f1003,definition,
( sQ5_spl
<=> inductive(null_class) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f1004,plain,
( ~ sQ5_spl
| inductive(null_class) ),
inference(component_clause,[status(thm)],[f1003]) ).
fof(f1006,definition,
( sQ6_spl
<=> null_class = omega ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f1007,plain,
( ~ sQ6_spl
| null_class = omega ),
inference(component_clause,[status(thm)],[f1006]) ).
fof(f1010,definition,
! [X0] :
( sQ7_spl
<=> ~ member(X0,omega) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f1011,plain,
! [X0] :
( ~ sQ7_spl
| ~ member(X0,omega) ),
inference(component_clause,[status(thm)],[f1010]) ).
fof(f1087,plain,
! [X0,X1] :
( ~ member(y,X1)
| ~ member(y,X0) ),
inference(resolution,[status(thm)],[f142,f480]) ).
fof(f1095,definition,
! [X0] :
( sQ11_spl
<=> ~ member(y,X0) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f1098,plain,
sQ11_spl,
inference(split_clause,[status(thm)],[f1087,f1095]) ).
fof(f1126,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,f498]) ).
fof(f1129,definition,
( sQ14_spl
<=> inductive(singleton(null_class)) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f1130,plain,
( ~ sQ14_spl
| inductive(singleton(null_class)) ),
inference(component_clause,[status(thm)],[f1129]) ).
fof(f1132,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(f1134,plain,
( sQ15_spl
| ~ subclass(image(successor_relation,unordered_pair(null_class,null_class)),unordered_pair(null_class,null_class)) ),
inference(component_clause,[status(thm)],[f1132]) ).
fof(f1135,plain,
( ~ sQ1_spl
| ~ sQ15_spl
| sQ14_spl ),
inference(split_clause,[status(thm)],[f1126,f1129,f1132,f497]) ).
fof(f1149,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,f369]) ).
fof(f1156,plain,
! [X0,X1,X2] :
( ~ member(X0,X2)
| member(X0,X1)
| member(X0,complement(X1)) ),
inference(resolution,[status(thm)],[f144,f462]) ).
fof(f1168,definition,
! [X0] :
( sQ16_spl
<=> member(y,X0) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f1169,plain,
! [X0] :
( ~ sQ16_spl
| member(y,X0) ),
inference(component_clause,[status(thm)],[f1168]) ).
fof(f1183,plain,
! [X0,X1] :
( ~ subclass(X1,identity_relation)
| ~ member(X0,X1)
| member(X0,subset_relation) ),
inference(paramodulation,[status(thm)],[f194,f470]) ).
fof(f1187,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(f1224,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,f1187]) ).
fof(f1240,plain,
! [X0] :
( ~ inductive(identity_relation)
| ~ member(X0,omega)
| member(X0,subset_relation) ),
inference(resolution,[status(thm)],[f1183,f170]) ).
fof(f1243,definition,
! [X0] :
( sQ17_spl
<=> ( ~ member(X0,omega)
| member(X0,subset_relation) ) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f1244,plain,
! [X0] :
( ~ sQ17_spl
| ~ member(X0,omega)
| member(X0,subset_relation) ),
inference(component_clause,[status(thm)],[f1243]) ).
fof(f1246,definition,
( sQ18_spl
<=> inductive(identity_relation) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f1249,plain,
( ~ sQ18_spl
| sQ17_spl ),
inference(split_clause,[status(thm)],[f1240,f1243,f1246]) ).
fof(f1273,plain,
! [X0,X1] :
( not_subclass_element(singleton(X0),X1) = X0
| subclass(singleton(X0),X1) ),
inference(resolution,[status(thm)],[f113,f261]) ).
fof(f1279,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(f1293,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)],[f1279,f234]) ).
fof(f1308,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,f1279]) ).
fof(f1362,plain,
! [X0,X1] :
( ~ member(X0,image(element_relation,complement(X1)))
| ~ member(X0,power_class(X1)) ),
inference(paramodulation,[status(thm)],[f174,f143]) ).
fof(f1386,plain,
! [X0,X1,X2,X3] :
( member(X2,X3)
| ~ member(X2,X3)
| ~ member(X0,X1) ),
inference(resolution,[status(thm)],[f132,f129]) ).
fof(f1389,plain,
! [X0,X1,X2,X3] :
( member(X2,universal_class)
| ~ member(X2,X3)
| ~ member(X0,X1) ),
inference(resolution,[status(thm)],[f132,f221]) ).
fof(f1393,definition,
! [X0,X1] :
( sQ20_spl
<=> ~ member(X0,X1) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f1394,plain,
! [X0,X1] :
( ~ sQ20_spl
| ~ member(X0,X1) ),
inference(component_clause,[status(thm)],[f1393]) ).
fof(f1396,definition,
! [X2,X3] :
( sQ21_spl
<=> ( member(X2,X3)
| ~ member(X2,X3) ) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f1399,plain,
( sQ21_spl
| sQ20_spl ),
inference(split_clause,[status(thm)],[f1386,f1393,f1396]) ).
fof(f1400,definition,
! [X2,X3] :
( sQ22_spl
<=> ( member(X2,universal_class)
| ~ member(X2,X3) ) ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f1403,plain,
( sQ22_spl
| sQ20_spl ),
inference(split_clause,[status(thm)],[f1389,f1393,f1400]) ).
fof(f1422,plain,
( ~ sQ20_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f263,f1394]) ).
fof(f1466,plain,
~ sQ20_spl,
inference(contradiction_clause,[status(thm)],[f1422]) ).
fof(f1468,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(f1477,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,f1468]) ).
fof(f1478,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,f1477]) ).
fof(f1479,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,f1478]) ).
fof(f1482,plain,
( ~ sQ14_spl
| subclass(image(successor_relation,singleton(null_class)),singleton(null_class)) ),
inference(resolution,[status(thm)],[f167,f1130]) ).
fof(f1573,plain,
! [X0,X1] :
( subclass(X0,X1)
| ~ subclass(X0,null_class) ),
inference(resolution,[status(thm)],[f226,f233]) ).
fof(f1664,plain,
! [X0] :
( ~ subclass(universal_class,X0)
| universal_class = X0 ),
inference(resolution,[status(thm)],[f118,f115]) ).
fof(f1681,plain,
( ~ function(universal_class)
| cross_product(universal_class,universal_class) = universal_class ),
inference(resolution,[status(thm)],[f1664,f181]) ).
fof(f1685,definition,
( sQ27_spl
<=> cross_product(universal_class,universal_class) = universal_class ),
introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition]) ).
fof(f1686,plain,
( ~ sQ27_spl
| cross_product(universal_class,universal_class) = universal_class ),
inference(component_clause,[status(thm)],[f1685]) ).
fof(f1688,definition,
( sQ28_spl
<=> function(universal_class) ),
introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition]) ).
fof(f1691,plain,
( ~ sQ28_spl
| sQ27_spl ),
inference(split_clause,[status(thm)],[f1681,f1685,f1688]) ).
fof(f1721,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)],[f1686,f137]) ).
fof(f1757,plain,
! [X0,X1] :
( ~ sQ27_spl
| ~ member(X0,X1)
| member(ordered_pair(X0,X1),element_relation) ),
inference(forward_subsumption_resolution,[status(thm)],[f1721,f264]) ).
fof(f1903,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(f1972,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)],[f466,f1757]) ).
fof(f1991,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(f1992,plain,
! [X0,X1] :
( ~ sQ30_spl
| member(X1,unordered_pair(X0,X1))
| ~ member(X0,X1) ),
inference(component_clause,[status(thm)],[f1991]) ).
fof(f1994,definition,
! [X2,X3] :
( sQ31_spl
<=> ~ subclass(element_relation,cross_product(X2,X3)) ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f1995,plain,
! [X0,X1] :
( ~ sQ31_spl
| ~ subclass(element_relation,cross_product(X0,X1)) ),
inference(component_clause,[status(thm)],[f1994]) ).
fof(f1997,plain,
( ~ sQ27_spl
| sQ31_spl
| sQ30_spl ),
inference(split_clause,[status(thm)],[f1972,f1991,f1994,f1685]) ).
fof(f1998,definition,
! [X0,X1] :
( sQ32_spl
<=> member(X0,unordered_pair(X1,X0)) ),
introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition]) ).
fof(f1999,plain,
! [X0,X1] :
( ~ sQ32_spl
| member(X0,unordered_pair(X1,X0)) ),
inference(component_clause,[status(thm)],[f1998]) ).
fof(f2003,plain,
( ~ sQ31_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f135,f1995]) ).
fof(f2004,plain,
~ sQ31_spl,
inference(contradiction_clause,[status(thm)],[f2003]) ).
fof(f2005,plain,
! [X0] :
( ~ sQ30_spl
| ~ member(X0,y) ),
inference(resolution,[status(thm)],[f1992,f480]) ).
fof(f2153,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(f2310,plain,
( ~ sQ30_spl
| y = null_class ),
inference(resolution,[status(thm)],[f235,f2005]) ).
fof(f2316,plain,
! [X0] :
( ~ sQ30_spl
| ~ member(null_class,X0) ),
inference(backward_demodulation,[status(thm)],[f2310,f480]) ).
fof(f2318,plain,
( ~ sQ30_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f2316,f494,f1991]) ).
fof(f2365,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)],[f1293,f498]) ).
fof(f2385,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)],[f1293,f1187]) ).
fof(f2400,definition,
( sQ33_spl
<=> member(null_class,universal_class) ),
introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition]) ).
fof(f2402,plain,
( sQ33_spl
| ~ member(null_class,universal_class) ),
inference(component_clause,[status(thm)],[f2400]) ).
fof(f2403,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(f2435,definition,
( sQ35_spl
<=> singleton(x) = null_class ),
introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition]) ).
fof(f2436,plain,
( ~ sQ35_spl
| singleton(x) = null_class ),
inference(component_clause,[status(thm)],[f2435]) ).
fof(f2437,plain,
( sQ35_spl
| null_class != singleton(x) ),
inference(component_clause,[status(thm)],[f2435]) ).
fof(f2438,definition,
( sQ36_spl
<=> not_subclass_element(unordered_pair(y,x),null_class) = x ),
introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition]) ).
fof(f2439,plain,
( ~ sQ36_spl
| x = not_subclass_element(unordered_pair(y,x),null_class) ),
inference(component_clause,[status(thm)],[f2438]) ).
fof(f2441,definition,
( sQ37_spl
<=> not_subclass_element(unordered_pair(y,x),null_class) = y ),
introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition]) ).
fof(f2442,plain,
( ~ sQ37_spl
| y = not_subclass_element(unordered_pair(y,x),null_class) ),
inference(component_clause,[status(thm)],[f2441]) ).
fof(f2443,plain,
( sQ37_spl
| not_subclass_element(unordered_pair(y,x),null_class) != y ),
inference(component_clause,[status(thm)],[f2441]) ).
fof(f2464,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(f2467,plain,
( ~ sQ1_spl
| sQ38_spl
| sQ5_spl ),
inference(split_clause,[status(thm)],[f2365,f1003,f2464,f497]) ).
fof(f2469,plain,
( ~ sQ6_spl
| inductive(null_class) ),
inference(backward_demodulation,[status(thm)],[f1007,f169]) ).
fof(f2483,plain,
( ~ sQ37_spl
| member(y,unordered_pair(y,x))
| unordered_pair(y,x) = null_class ),
inference(paramodulation,[status(thm)],[f2442,f235]) ).
fof(f2488,definition,
( sQ40_spl
<=> unordered_pair(y,x) = null_class ),
introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition]) ).
fof(f2489,plain,
( ~ sQ40_spl
| unordered_pair(y,x) = null_class ),
inference(component_clause,[status(thm)],[f2488]) ).
fof(f2490,plain,
( sQ40_spl
| unordered_pair(y,x) != null_class ),
inference(component_clause,[status(thm)],[f2488]) ).
fof(f2491,definition,
( sQ41_spl
<=> member(y,unordered_pair(y,x)) ),
introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition]) ).
fof(f2492,plain,
( ~ sQ41_spl
| member(y,unordered_pair(y,x)) ),
inference(component_clause,[status(thm)],[f2491]) ).
fof(f2494,plain,
( ~ sQ37_spl
| sQ41_spl
| sQ40_spl ),
inference(split_clause,[status(thm)],[f2483,f2488,f2491,f2441]) ).
fof(f2495,plain,
( ~ sQ41_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2492,f480]) ).
fof(f2496,plain,
~ sQ41_spl,
inference(contradiction_clause,[status(thm)],[f2495]) ).
fof(f2497,plain,
( ~ sQ40_spl
| null_class != singleton(x) ),
inference(backward_demodulation,[status(thm)],[f2489,f243]) ).
fof(f2507,definition,
( sQ42_spl
<=> null_class = null_class ),
introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition]) ).
fof(f2510,definition,
( sQ43_spl
<=> member(x,null_class) ),
introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition]) ).
fof(f2511,plain,
( ~ sQ43_spl
| member(x,null_class) ),
inference(component_clause,[status(thm)],[f2510]) ).
fof(f2514,plain,
( ~ sQ43_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2511,f232]) ).
fof(f2515,plain,
~ sQ43_spl,
inference(contradiction_clause,[status(thm)],[f2514]) ).
fof(f2535,plain,
! [X0] :
( ~ sQ40_spl
| member(x,null_class)
| ~ member(x,X0) ),
inference(paramodulation,[status(thm)],[f2489,f479]) ).
fof(f2559,definition,
! [X0] :
( sQ44_spl
<=> ~ member(x,X0) ),
introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition]) ).
fof(f2560,plain,
! [X0] :
( ~ sQ44_spl
| ~ member(x,X0) ),
inference(component_clause,[status(thm)],[f2559]) ).
fof(f2562,plain,
( ~ sQ40_spl
| sQ43_spl
| sQ44_spl ),
inference(split_clause,[status(thm)],[f2535,f2559,f2510,f2488]) ).
fof(f2566,definition,
( sQ45_spl
<=> member(y,null_class) ),
introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition]) ).
fof(f2567,plain,
( ~ sQ45_spl
| member(y,null_class) ),
inference(component_clause,[status(thm)],[f2566]) ).
fof(f2670,plain,
( member(apply(choice,null_class),null_class)
| null_class = null_class ),
inference(resolution,[status(thm)],[f189,f236]) ).
fof(f2675,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(f2677,definition,
( sQ47_spl
<=> member(apply(choice,null_class),null_class) ),
introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition]) ).
fof(f2678,plain,
( ~ sQ47_spl
| member(apply(choice,null_class),null_class) ),
inference(component_clause,[status(thm)],[f2677]) ).
fof(f2680,plain,
( sQ47_spl
| sQ42_spl ),
inference(split_clause,[status(thm)],[f2670,f2507,f2677]) ).
fof(f2687,definition,
( sQ50_spl
<=> universal_class = null_class ),
introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition]) ).
fof(f2688,plain,
( ~ sQ50_spl
| null_class = universal_class ),
inference(component_clause,[status(thm)],[f2687]) ).
fof(f2689,plain,
( sQ50_spl
| null_class != universal_class ),
inference(component_clause,[status(thm)],[f2687]) ).
fof(f2691,plain,
( ~ sQ47_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2678,f232]) ).
fof(f2692,plain,
~ sQ47_spl,
inference(contradiction_clause,[status(thm)],[f2691]) ).
fof(f2704,plain,
! [X0] :
( ~ sQ50_spl
| ~ member(X0,universal_class) ),
inference(backward_demodulation,[status(thm)],[f2688,f232]) ).
fof(f2820,plain,
( ~ sQ50_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f265,f2704]) ).
fof(f2829,plain,
~ sQ50_spl,
inference(contradiction_clause,[status(thm)],[f2820]) ).
fof(f2902,definition,
! [X0] :
( sQ51_spl
<=> X0 = null_class ),
introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition]) ).
fof(f2903,plain,
! [X0] :
( ~ sQ51_spl
| null_class = X0 ),
inference(component_clause,[status(thm)],[f2902]) ).
fof(f2909,plain,
( sQ50_spl
| ~ sQ51_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f2689,f2903]) ).
fof(f2910,plain,
( sQ50_spl
| ~ sQ51_spl ),
inference(contradiction_clause,[status(thm)],[f2909]) ).
fof(f2912,plain,
! [X0,X1,X2] :
( ~ member(singleton(singleton(singleton(X0))),cross_product(X2,X1))
| member(X0,X1) ),
inference(paramodulation,[status(thm)],[f260,f131]) ).
fof(f2914,definition,
( sQ52_spl
<=> member(null_class,null_class) ),
introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition]) ).
fof(f2915,plain,
( ~ sQ52_spl
| member(null_class,null_class) ),
inference(component_clause,[status(thm)],[f2914]) ).
fof(f2917,definition,
( sQ53_spl
<=> subclass(universal_class,null_class) ),
introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition]) ).
fof(f2918,plain,
( ~ sQ53_spl
| subclass(universal_class,null_class) ),
inference(component_clause,[status(thm)],[f2917]) ).
fof(f2923,plain,
! [X0] :
( ~ sQ53_spl
| subclass(X0,null_class)
| ~ subclass(X0,universal_class) ),
inference(resolution,[status(thm)],[f2918,f226]) ).
fof(f2928,plain,
! [X0,X1] :
( ~ sQ53_spl
| subclass(X0,X1) ),
inference(backward_subsumption_resolution,[status(thm)],[f1573,f2930]) ).
fof(f2930,plain,
! [X0] :
( ~ sQ53_spl
| subclass(X0,null_class) ),
inference(forward_subsumption_resolution,[status(thm)],[f2923,f115]) ).
fof(f2933,plain,
( ~ sQ3_spl
| ~ sQ53_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f527,f2928]) ).
fof(f3036,plain,
( ~ sQ3_spl
| ~ sQ53_spl ),
inference(contradiction_clause,[status(thm)],[f2933]) ).
fof(f3103,definition,
( sQ54_spl
<=> member(not_subclass_element(null_class,universal_class),null_class) ),
introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition]) ).
fof(f3104,plain,
( ~ sQ54_spl
| member(not_subclass_element(null_class,universal_class),null_class) ),
inference(component_clause,[status(thm)],[f3103]) ).
fof(f3107,plain,
( ~ sQ54_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3104,f232]) ).
fof(f3108,plain,
~ sQ54_spl,
inference(contradiction_clause,[status(thm)],[f3107]) ).
fof(f3109,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)],[f2675,f120]) ).
fof(f3252,definition,
( sQ58_spl
<=> unordered_pair(x,y) = null_class ),
introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition]) ).
fof(f3253,plain,
( ~ sQ58_spl
| unordered_pair(x,y) = null_class ),
inference(component_clause,[status(thm)],[f3252]) ).
fof(f3272,plain,
( ~ sQ58_spl
| unordered_pair(y,x) = null_class ),
inference(forward_demodulation,[status(thm)],[f237,f3253]) ).
fof(f3491,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(f3616,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)],[f3491,f261]) ).
fof(f3816,definition,
( sQ66_spl
<=> x = y ),
introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition]) ).
fof(f3817,plain,
( ~ sQ66_spl
| x = y ),
inference(component_clause,[status(thm)],[f3816]) ).
fof(f3818,plain,
( sQ66_spl
| x != y ),
inference(component_clause,[status(thm)],[f3816]) ).
fof(f3825,plain,
~ inductive(null_class),
inference(resolution,[status(thm)],[f166,f232]) ).
fof(f3837,plain,
( ~ sQ5_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3825,f1004]) ).
fof(f3838,plain,
~ sQ5_spl,
inference(contradiction_clause,[status(thm)],[f3837]) ).
fof(f3839,plain,
( ~ sQ6_spl
| sQ5_spl ),
inference(split_clause,[status(thm)],[f2469,f1003,f1006]) ).
fof(f3862,definition,
( sQ69_spl
<=> x = null_class ),
introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition]) ).
fof(f3863,plain,
( ~ sQ69_spl
| null_class = x ),
inference(component_clause,[status(thm)],[f3862]) ).
fof(f3865,definition,
( sQ70_spl
<=> y = null_class ),
introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition]) ).
fof(f3866,plain,
( ~ sQ70_spl
| y = null_class ),
inference(component_clause,[status(thm)],[f3865]) ).
fof(f3872,plain,
( sQ66_spl
| ~ sQ69_spl
| null_class != y ),
inference(backward_demodulation,[status(thm)],[f3863,f3818]) ).
fof(f3875,plain,
( ~ sQ70_spl
| sQ66_spl
| ~ sQ69_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3866,f3872]) ).
fof(f3876,plain,
( ~ sQ70_spl
| sQ66_spl
| ~ sQ69_spl ),
inference(contradiction_clause,[status(thm)],[f3875]) ).
fof(f3878,plain,
! [X0,X1] :
( ~ member(image(X0,singleton(X1)),universal_class)
| member(apply(X0,X1),universal_class) ),
inference(paramodulation,[status(thm)],[f187,f173]) ).
fof(f3911,plain,
( ~ sQ7_spl
| ~ inductive(omega) ),
inference(resolution,[status(thm)],[f1011,f166]) ).
fof(f3912,plain,
( ~ sQ7_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3911,f169]) ).
fof(f3913,plain,
~ sQ7_spl,
inference(contradiction_clause,[status(thm)],[f3912]) ).
fof(f4053,plain,
! [X0] :
( null_class = singleton(X0)
| regular(singleton(X0)) = X0 ),
inference(resolution,[status(thm)],[f185,f261]) ).
fof(f4055,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(f4112,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)],[f4055,f1187]) ).
fof(f4136,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)],[f4055,f479]) ).
fof(f4140,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)],[f4055,f237]) ).
fof(f4147,definition,
( sQ72_spl
<=> regular(unordered_pair(y,x)) = y ),
introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition]) ).
fof(f4148,plain,
( ~ sQ72_spl
| regular(unordered_pair(y,x)) = y ),
inference(component_clause,[status(thm)],[f4147]) ).
fof(f4150,definition,
( sQ73_spl
<=> regular(unordered_pair(y,x)) = x ),
introduced(definition,[new_symbols(definition,[sQ73_spl])],[split_symbol_definition]) ).
fof(f4151,plain,
( ~ sQ73_spl
| regular(unordered_pair(y,x)) = x ),
inference(component_clause,[status(thm)],[f4150]) ).
fof(f4190,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(f4194,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(f4221,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)],[f4136,f232]) ).
fof(f4235,plain,
( ~ sQ52_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2915,f232]) ).
fof(f4236,plain,
~ sQ52_spl,
inference(contradiction_clause,[status(thm)],[f4235]) ).
fof(f4349,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(f4350,plain,
! [X0] :
( ~ sQ80_spl
| ~ subclass(cross_product(universal_class,universal_class),X0)
| X0 = universal_class ),
inference(component_clause,[status(thm)],[f4349]) ).
fof(f4415,plain,
( ~ sQ80_spl
| cross_product(universal_class,universal_class) = universal_class ),
inference(resolution,[status(thm)],[f4350,f244]) ).
fof(f4416,plain,
( ~ sQ80_spl
| sQ27_spl ),
inference(split_clause,[status(thm)],[f4415,f1685,f4349]) ).
fof(f4746,plain,
! [X0,X1] :
( ~ inductive(X1)
| regular(unordered_pair(X0,null_class)) = null_class
| X0 = regular(unordered_pair(X0,null_class)) ),
inference(resolution,[status(thm)],[f4221,f166]) ).
fof(f4774,definition,
! [X1] :
( sQ86_spl
<=> restrict(X1,singleton(null_class),universal_class) = null_class ),
introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition]) ).
fof(f4775,plain,
! [X0] :
( ~ sQ86_spl
| restrict(X0,singleton(null_class),universal_class) = null_class ),
inference(component_clause,[status(thm)],[f4774]) ).
fof(f4778,definition,
! [X1] :
( sQ87_spl
<=> member(null_class,X1) ),
introduced(definition,[new_symbols(definition,[sQ87_spl])],[split_symbol_definition]) ).
fof(f4779,plain,
! [X0] :
( ~ sQ87_spl
| member(null_class,X0) ),
inference(component_clause,[status(thm)],[f4778]) ).
fof(f4786,definition,
! [X1] :
( sQ89_spl
<=> ~ inductive(X1) ),
introduced(definition,[new_symbols(definition,[sQ89_spl])],[split_symbol_definition]) ).
fof(f4787,plain,
! [X0] :
( ~ sQ89_spl
| ~ inductive(X0) ),
inference(component_clause,[status(thm)],[f4786]) ).
fof(f4789,plain,
( sQ89_spl
| sQ78_spl ),
inference(split_clause,[status(thm)],[f4746,f4194,f4786]) ).
fof(f4791,plain,
( ~ sQ89_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f169,f4787]) ).
fof(f4797,plain,
( sQ15_spl
| ~ subclass(image(successor_relation,singleton(null_class)),unordered_pair(null_class,null_class)) ),
inference(forward_demodulation,[status(thm)],[f126,f1134]) ).
fof(f4798,plain,
( sQ15_spl
| ~ subclass(image(successor_relation,singleton(null_class)),singleton(null_class)) ),
inference(forward_demodulation,[status(thm)],[f126,f4797]) ).
fof(f4836,plain,
! [X0] :
( ~ sQ87_spl
| null_class = singleton(singleton(X0)) ),
inference(resolution,[status(thm)],[f4779,f324]) ).
fof(f4915,plain,
! [X0,X1,X2] :
( ~ sQ87_spl
| ~ member(null_class,cross_product(X2,X1))
| member(X0,X1) ),
inference(backward_demodulation,[status(thm)],[f4836,f2912]) ).
fof(f5007,definition,
! [X0] :
( sQ92_spl
<=> member(X0,unordered_pair(X0,singleton(X0))) ),
introduced(definition,[new_symbols(definition,[sQ92_spl])],[split_symbol_definition]) ).
fof(f5008,plain,
! [X0] :
( ~ sQ92_spl
| member(X0,unordered_pair(X0,singleton(X0))) ),
inference(component_clause,[status(thm)],[f5007]) ).
fof(f5157,plain,
! [X0,X1] :
( ~ sQ87_spl
| ~ member(X0,image(element_relation,complement(X1))) ),
inference(backward_subsumption_resolution,[status(thm)],[f1362,f5209]) ).
fof(f5209,plain,
! [X0,X1] :
( ~ sQ87_spl
| member(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f4915,f4779]) ).
fof(f5222,plain,
( ~ sQ87_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5157,f5209]) ).
fof(f5223,plain,
~ sQ87_spl,
inference(contradiction_clause,[status(thm)],[f5222]) ).
fof(f5258,plain,
( ~ sQ92_spl
| $false ),
inference(resolution,[status(thm)],[f5008,f480]) ).
fof(f5261,plain,
~ sQ92_spl,
inference(contradiction_clause,[status(thm)],[f5258]) ).
fof(f5263,plain,
! [X0] :
( ~ sQ86_spl
| image(X0,singleton(null_class)) = range_of(null_class) ),
inference(paramodulation,[status(thm)],[f4775,f161]) ).
fof(f5970,plain,
( ~ sQ45_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2567,f480]) ).
fof(f5971,plain,
~ sQ45_spl,
inference(contradiction_clause,[status(thm)],[f5970]) ).
fof(f6529,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(f6721,plain,
! [X0,X1,X2] :
( X1 = not_subclass_element(singleton(X1),X2)
| member(X0,X2)
| ~ member(X0,singleton(X1)) ),
inference(resolution,[status(thm)],[f1273,f112]) ).
fof(f6908,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)],[f3109,f1187]) ).
fof(f6937,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(f7031,plain,
! [X0,X1,X2] :
( ~ member(X0,X2)
| member(X0,X1)
| not_subclass_element(singleton(X0),X1) = X0 ),
inference(resolution,[status(thm)],[f6721,f491]) ).
fof(f7048,plain,
! [X0,X1] :
( ~ inductive(X1)
| null_class = not_subclass_element(singleton(null_class),X0)
| member(null_class,X0) ),
inference(resolution,[status(thm)],[f7031,f166]) ).
fof(f7062,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(f7065,plain,
( sQ89_spl
| sQ116_spl ),
inference(split_clause,[status(thm)],[f7048,f7062,f4786]) ).
fof(f7067,plain,
~ sQ89_spl,
inference(contradiction_clause,[status(thm)],[f4791]) ).
fof(f7246,definition,
( sQ117_spl
<=> regular(unordered_pair(x,y)) = x ),
introduced(definition,[new_symbols(definition,[sQ117_spl])],[split_symbol_definition]) ).
fof(f7249,definition,
( sQ118_spl
<=> y = regular(unordered_pair(x,y)) ),
introduced(definition,[new_symbols(definition,[sQ118_spl])],[split_symbol_definition]) ).
fof(f7250,plain,
( ~ sQ118_spl
| y = regular(unordered_pair(x,y)) ),
inference(component_clause,[status(thm)],[f7249]) ).
fof(f7263,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(f7293,plain,
( ~ sQ118_spl
| y = regular(unordered_pair(y,x)) ),
inference(forward_demodulation,[status(thm)],[f237,f7250]) ).
fof(f8063,plain,
! [X0] :
( ~ sQ86_spl
| null_class != null_class
| ~ member(null_class,domain_of(X0)) ),
inference(paramodulation,[status(thm)],[f4775,f149]) ).
fof(f8070,definition,
! [X0] :
( sQ122_spl
<=> ~ member(null_class,domain_of(X0)) ),
introduced(definition,[new_symbols(definition,[sQ122_spl])],[split_symbol_definition]) ).
fof(f8071,plain,
! [X0] :
( ~ sQ122_spl
| ~ member(null_class,domain_of(X0)) ),
inference(component_clause,[status(thm)],[f8070]) ).
fof(f8073,plain,
( ~ sQ86_spl
| ~ sQ42_spl
| sQ122_spl ),
inference(split_clause,[status(thm)],[f8063,f8070,f2507,f4774]) ).
fof(f8076,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)],[f4112,f8071]) ).
fof(f8084,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)],[f2385,f8071]) ).
fof(f8154,plain,
( ~ sQ40_spl
| regular(singleton(x)) = x
| null_class != null_class ),
inference(paramodulation,[status(thm)],[f4053,f2497]) ).
fof(f8171,plain,
! [X0,X1] :
( regular(singleton(X0)) = X0
| ~ member(X0,X1)
| member(X0,null_class) ),
inference(paramodulation,[status(thm)],[f4053,f491]) ).
fof(f8184,definition,
( sQ128_spl
<=> regular(singleton(x)) = x ),
introduced(definition,[new_symbols(definition,[sQ128_spl])],[split_symbol_definition]) ).
fof(f8185,plain,
( ~ sQ128_spl
| x = regular(singleton(x)) ),
inference(component_clause,[status(thm)],[f8184]) ).
fof(f8187,plain,
( ~ sQ40_spl
| sQ128_spl
| ~ sQ42_spl ),
inference(split_clause,[status(thm)],[f8154,f2507,f8184,f2488]) ).
fof(f8188,plain,
! [X0,X1] :
( regular(singleton(X0)) = X0
| ~ member(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f8171,f232]) ).
fof(f8189,definition,
( sQ129_spl
<=> regular(singleton(null_class)) = null_class ),
introduced(definition,[new_symbols(definition,[sQ129_spl])],[split_symbol_definition]) ).
fof(f8193,definition,
! [X0] :
( sQ130_spl
<=> regular(singleton(X0)) = X0 ),
introduced(definition,[new_symbols(definition,[sQ130_spl])],[split_symbol_definition]) ).
fof(f8199,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)],[f6908,f8071]) ).
fof(f8201,plain,
( sQ35_spl
| regular(singleton(x)) = x
| null_class != null_class ),
inference(paramodulation,[status(thm)],[f4053,f2437]) ).
fof(f8202,plain,
( sQ35_spl
| sQ128_spl
| ~ sQ42_spl ),
inference(split_clause,[status(thm)],[f8201,f2507,f8184,f2435]) ).
fof(f8203,plain,
( sQ37_spl
| ~ sQ36_spl
| y != x ),
inference(backward_demodulation,[status(thm)],[f2439,f2443]) ).
fof(f8204,plain,
( sQ40_spl
| y = not_subclass_element(unordered_pair(y,x),null_class)
| not_subclass_element(unordered_pair(y,x),null_class) = x ),
inference(resolution,[status(thm)],[f2490,f1293]) ).
fof(f8205,plain,
( sQ40_spl
| regular(unordered_pair(y,x)) = y
| x = regular(unordered_pair(y,x)) ),
inference(resolution,[status(thm)],[f2490,f4055]) ).
fof(f8206,plain,
( sQ40_spl
| y = regular(unordered_pair(x,y))
| regular(unordered_pair(x,y)) = x ),
inference(resolution,[status(thm)],[f2490,f4140]) ).
fof(f8217,plain,
( sQ40_spl
| sQ72_spl
| sQ73_spl ),
inference(split_clause,[status(thm)],[f8205,f4150,f4147,f2488]) ).
fof(f8219,plain,
( sQ40_spl
| sQ37_spl
| sQ36_spl ),
inference(split_clause,[status(thm)],[f8204,f2438,f2441,f2488]) ).
fof(f8220,plain,
( sQ40_spl
| sQ118_spl
| sQ117_spl ),
inference(split_clause,[status(thm)],[f8206,f7246,f7249,f2488]) ).
fof(f8236,definition,
( sQ131_spl
<=> y = not_subclass_element(unordered_pair(y,x),singleton(x)) ),
introduced(definition,[new_symbols(definition,[sQ131_spl])],[split_symbol_definition]) ).
fof(f8237,plain,
( ~ sQ131_spl
| not_subclass_element(unordered_pair(y,x),singleton(x)) = y ),
inference(component_clause,[status(thm)],[f8236]) ).
fof(f8239,definition,
( sQ132_spl
<=> not_subclass_element(singleton(x),unordered_pair(y,x)) = x ),
introduced(definition,[new_symbols(definition,[sQ132_spl])],[split_symbol_definition]) ).
fof(f8240,plain,
( ~ sQ132_spl
| not_subclass_element(singleton(x),unordered_pair(y,x)) = x ),
inference(component_clause,[status(thm)],[f8239]) ).
fof(f8242,definition,
( sQ133_spl
<=> x = not_subclass_element(unordered_pair(y,x),singleton(x)) ),
introduced(definition,[new_symbols(definition,[sQ133_spl])],[split_symbol_definition]) ).
fof(f8243,plain,
( ~ sQ133_spl
| not_subclass_element(unordered_pair(y,x),singleton(x)) = x ),
inference(component_clause,[status(thm)],[f8242]) ).
fof(f8247,plain,
( ~ sQ58_spl
| sQ40_spl ),
inference(split_clause,[status(thm)],[f3272,f2488,f3252]) ).
fof(f8251,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)],[f3616,f8076]) ).
fof(f8256,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)],[f3616,f8076]) ).
fof(f8259,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)],[f4140,f8076]) ).
fof(f8260,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)],[f1293,f8076]) ).
fof(f8261,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)],[f4055,f8076]) ).
fof(f8262,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,f8076]) ).
fof(f8265,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)],[f8076,f149]) ).
fof(f8266,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)],[f8076,f160]) ).
fof(f8267,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)],[f8076,f161]) ).
fof(f8268,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)],[f8076,f369]) ).
fof(f8269,plain,
( ~ sQ122_spl
| sQ119_spl
| sQ86_spl ),
inference(split_clause,[status(thm)],[f8259,f4774,f7263,f8070]) ).
fof(f8279,definition,
! [X0,X1] :
( sQ136_spl
<=> ( member(X0,X1)
| ~ member(X0,null_class) ) ),
introduced(definition,[new_symbols(definition,[sQ136_spl])],[split_symbol_definition]) ).
fof(f8282,plain,
( ~ sQ122_spl
| sQ77_spl
| sQ136_spl ),
inference(split_clause,[status(thm)],[f8268,f8279,f4190,f8070]) ).
fof(f8283,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(f8286,plain,
( ~ sQ122_spl
| sQ137_spl
| sQ86_spl ),
inference(split_clause,[status(thm)],[f8261,f4774,f8283,f8070]) ).
fof(f8287,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,f8262]) ).
fof(f8288,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,f8287]) ).
fof(f8289,plain,
! [X0,X1] :
( ~ sQ122_spl
| restrict(X1,singleton(singleton(X0)),universal_class) = null_class
| X0 = regular(singleton(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f8288]) ).
fof(f8290,plain,
( ~ sQ122_spl
| sQ104_spl
| sQ86_spl ),
inference(split_clause,[status(thm)],[f8260,f4774,f6529,f8070]) ).
fof(f8291,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(f8294,plain,
( ~ sQ122_spl
| ~ sQ42_spl
| sQ138_spl ),
inference(split_clause,[status(thm)],[f8265,f8291,f2507,f8070]) ).
fof(f8298,plain,
( sQ15_spl
| ~ sQ86_spl
| ~ subclass(range_of(null_class),singleton(null_class)) ),
inference(backward_demodulation,[status(thm)],[f5263,f4798]) ).
fof(f8355,plain,
( ~ sQ128_spl
| singleton(x) = null_class
| member(x,singleton(x)) ),
inference(paramodulation,[status(thm)],[f8185,f185]) ).
fof(f8356,plain,
( ~ sQ128_spl
| null_class = intersection(singleton(x),x)
| null_class = singleton(x) ),
inference(paramodulation,[status(thm)],[f8185,f186]) ).
fof(f8358,definition,
( sQ140_spl
<=> null_class = intersection(singleton(x),x) ),
introduced(definition,[new_symbols(definition,[sQ140_spl])],[split_symbol_definition]) ).
fof(f8359,plain,
( ~ sQ140_spl
| intersection(singleton(x),x) = null_class ),
inference(component_clause,[status(thm)],[f8358]) ).
fof(f8361,plain,
( ~ sQ128_spl
| sQ140_spl
| sQ35_spl ),
inference(split_clause,[status(thm)],[f8356,f2435,f8358,f8184]) ).
fof(f8362,definition,
( sQ141_spl
<=> member(x,singleton(x)) ),
introduced(definition,[new_symbols(definition,[sQ141_spl])],[split_symbol_definition]) ).
fof(f8363,plain,
( ~ sQ141_spl
| member(x,singleton(x)) ),
inference(component_clause,[status(thm)],[f8362]) ).
fof(f8365,plain,
( ~ sQ128_spl
| sQ35_spl
| sQ141_spl ),
inference(split_clause,[status(thm)],[f8355,f8362,f2435,f8184]) ).
fof(f8366,plain,
! [X0] :
( ~ sQ141_spl
| not_subclass_element(singleton(x),X0) = x
| member(x,X0) ),
inference(resolution,[status(thm)],[f8363,f6721]) ).
fof(f8425,plain,
( ~ sQ73_spl
| null_class = intersection(unordered_pair(y,x),x)
| null_class = unordered_pair(y,x) ),
inference(paramodulation,[status(thm)],[f4151,f186]) ).
fof(f8426,definition,
( sQ142_spl
<=> null_class = intersection(unordered_pair(y,x),x) ),
introduced(definition,[new_symbols(definition,[sQ142_spl])],[split_symbol_definition]) ).
fof(f8429,plain,
( ~ sQ73_spl
| sQ142_spl
| sQ40_spl ),
inference(split_clause,[status(thm)],[f8425,f2488,f8426,f4150]) ).
fof(f8431,definition,
( sQ143_spl
<=> member(x,unordered_pair(y,x)) ),
introduced(definition,[new_symbols(definition,[sQ143_spl])],[split_symbol_definition]) ).
fof(f8432,plain,
( ~ sQ143_spl
| member(x,unordered_pair(y,x)) ),
inference(component_clause,[status(thm)],[f8431]) ).
fof(f8436,plain,
! [X0] :
( ~ sQ140_spl
| ~ member(X0,x)
| member(X0,null_class)
| ~ member(X0,singleton(x)) ),
inference(paramodulation,[status(thm)],[f8359,f142]) ).
fof(f8441,plain,
! [X0] :
( ~ sQ140_spl
| ~ member(X0,singleton(x))
| ~ member(X0,x) ),
inference(forward_subsumption_resolution,[status(thm)],[f8436,f232]) ).
fof(f8521,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)],[f255,f8084]) ).
fof(f8522,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,f8084]) ).
fof(f8528,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)],[f1293,f8084]) ).
fof(f8529,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,f8084]) ).
fof(f8532,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)],[f8084,f149]) ).
fof(f8535,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)],[f8084,f369]) ).
fof(f8536,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(f8539,plain,
( ~ sQ122_spl
| sQ86_spl
| sQ144_spl ),
inference(split_clause,[status(thm)],[f8528,f8536,f4774,f8070]) ).
fof(f8540,plain,
( ~ sQ122_spl
| sQ34_spl
| sQ136_spl ),
inference(split_clause,[status(thm)],[f8535,f8279,f2403,f8070]) ).
fof(f8545,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,f8522]) ).
fof(f8546,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,f8545]) ).
fof(f8547,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,f8529]) ).
fof(f8548,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,f8547]) ).
fof(f8549,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)],[f8548]) ).
fof(f8550,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(f8553,plain,
( ~ sQ122_spl
| ~ sQ42_spl
| sQ146_spl ),
inference(split_clause,[status(thm)],[f8532,f8550,f2507,f8070]) ).
fof(f8554,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)],[f255,f8521]) ).
fof(f8555,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)],[f255,f8554]) ).
fof(f8569,plain,
! [X0] :
( null_class = regular(singleton(null_class))
| ~ inductive(X0) ),
inference(resolution,[status(thm)],[f166,f8188]) ).
fof(f8573,plain,
( sQ129_spl
| sQ89_spl ),
inference(split_clause,[status(thm)],[f8569,f4786,f8189]) ).
fof(f8601,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)],[f255,f8199]) ).
fof(f8602,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,f8199]) ).
fof(f8608,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,f8199]) ).
fof(f8611,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)],[f8199,f149]) ).
fof(f8614,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)],[f8199,f369]) ).
fof(f8615,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,f8602]) ).
fof(f8616,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,f8615]) ).
fof(f8617,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(f8620,plain,
( ~ sQ122_spl
| ~ sQ42_spl
| sQ147_spl ),
inference(split_clause,[status(thm)],[f8611,f8617,f2507,f8070]) ).
fof(f8625,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)],[f255,f8601]) ).
fof(f8626,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)],[f255,f8625]) ).
fof(f8627,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,f8608]) ).
fof(f8628,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,f8627]) ).
fof(f8629,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)],[f8628]) ).
fof(f8630,plain,
( ~ sQ122_spl
| sQ107_spl
| sQ136_spl ),
inference(split_clause,[status(thm)],[f8614,f8279,f6937,f8070]) ).
fof(f8643,plain,
! [X0] :
( ~ sQ35_spl
| ~ member(x,X0)
| member(x,null_class) ),
inference(paramodulation,[status(thm)],[f2436,f491]) ).
fof(f8659,plain,
( ~ sQ35_spl
| sQ44_spl
| sQ43_spl ),
inference(split_clause,[status(thm)],[f8643,f2510,f2559,f2435]) ).
fof(f8671,plain,
( ~ sQ143_spl
| ~ sQ44_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f8432,f2560]) ).
fof(f8672,plain,
( ~ sQ143_spl
| ~ sQ44_spl ),
inference(contradiction_clause,[status(thm)],[f8671]) ).
fof(f8732,plain,
( ~ sQ16_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1169,f480]) ).
fof(f8733,plain,
~ sQ16_spl,
inference(contradiction_clause,[status(thm)],[f8732]) ).
fof(f8833,plain,
( ~ sQ118_spl
| sQ72_spl ),
inference(split_clause,[status(thm)],[f7293,f4147,f7249]) ).
fof(f8847,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,f1156]) ).
fof(f8848,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,f481]) ).
fof(f8849,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,f491]) ).
fof(f8851,definition,
( sQ149_spl
<=> subclass(image(successor_relation,universal_class),universal_class) ),
introduced(definition,[new_symbols(definition,[sQ149_spl])],[split_symbol_definition]) ).
fof(f8853,plain,
( sQ149_spl
| ~ subclass(image(successor_relation,universal_class),universal_class) ),
inference(component_clause,[status(thm)],[f8851]) ).
fof(f8854,definition,
( sQ150_spl
<=> inductive(universal_class) ),
introduced(definition,[new_symbols(definition,[sQ150_spl])],[split_symbol_definition]) ).
fof(f8858,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(f8861,plain,
( sQ0_spl
| sQ151_spl ),
inference(split_clause,[status(thm)],[f8848,f8858,f494]) ).
fof(f8862,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(f8865,plain,
( sQ0_spl
| sQ152_spl ),
inference(split_clause,[status(thm)],[f8847,f8862,f494]) ).
fof(f8867,definition,
( sQ153_spl
<=> subclass(image(successor_relation,singleton(null_class)),singleton(null_class)) ),
introduced(definition,[new_symbols(definition,[sQ153_spl])],[split_symbol_definition]) ).
fof(f8869,plain,
( sQ153_spl
| ~ subclass(image(successor_relation,singleton(null_class)),singleton(null_class)) ),
inference(component_clause,[status(thm)],[f8867]) ).
fof(f8870,plain,
( sQ0_spl
| sQ14_spl
| ~ sQ153_spl ),
inference(split_clause,[status(thm)],[f8849,f8867,f1129,f494]) ).
fof(f8871,plain,
( sQ153_spl
| ~ sQ86_spl
| ~ subclass(range_of(null_class),singleton(null_class)) ),
inference(forward_demodulation,[status(thm)],[f5263,f8869]) ).
fof(f8872,plain,
( ~ sQ14_spl
| ~ sQ86_spl
| subclass(range_of(null_class),singleton(null_class)) ),
inference(forward_demodulation,[status(thm)],[f5263,f1482]) ).
fof(f8873,plain,
( ~ sQ14_spl
| ~ sQ86_spl
| sQ15_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f8872,f8298]) ).
fof(f8874,plain,
( ~ sQ14_spl
| ~ sQ86_spl
| sQ15_spl ),
inference(contradiction_clause,[status(thm)],[f8873]) ).
fof(f8875,plain,
( sQ149_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f8853,f115]) ).
fof(f8876,plain,
sQ149_spl,
inference(contradiction_clause,[status(thm)],[f8875]) ).
fof(f8877,plain,
( sQ153_spl
| ~ sQ86_spl
| ~ sQ14_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f8871,f8872]) ).
fof(f8878,plain,
( sQ153_spl
| ~ sQ86_spl
| ~ sQ14_spl ),
inference(contradiction_clause,[status(thm)],[f8877]) ).
fof(f8995,plain,
( ~ sQ36_spl
| member(x,unordered_pair(y,x))
| null_class = unordered_pair(y,x) ),
inference(paramodulation,[status(thm)],[f2439,f235]) ).
fof(f9001,definition,
( sQ154_spl
<=> subclass(unordered_pair(y,x),null_class) ),
introduced(definition,[new_symbols(definition,[sQ154_spl])],[split_symbol_definition]) ).
fof(f9002,plain,
( ~ sQ154_spl
| subclass(unordered_pair(y,x),null_class) ),
inference(component_clause,[status(thm)],[f9001]) ).
fof(f9003,plain,
( sQ154_spl
| ~ subclass(unordered_pair(y,x),null_class) ),
inference(component_clause,[status(thm)],[f9001]) ).
fof(f9005,definition,
( sQ155_spl
<=> member(not_subclass_element(null_class,unordered_pair(y,x)),null_class) ),
introduced(definition,[new_symbols(definition,[sQ155_spl])],[split_symbol_definition]) ).
fof(f9006,plain,
( ~ sQ155_spl
| member(not_subclass_element(null_class,unordered_pair(y,x)),null_class) ),
inference(component_clause,[status(thm)],[f9005]) ).
fof(f9014,plain,
( ~ sQ36_spl
| sQ143_spl
| sQ40_spl ),
inference(split_clause,[status(thm)],[f8995,f2488,f8431,f2438]) ).
fof(f9016,plain,
( ~ sQ155_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f9006,f232]) ).
fof(f9017,plain,
~ sQ155_spl,
inference(contradiction_clause,[status(thm)],[f9016]) ).
fof(f9044,plain,
! [X0,X1] :
( ~ sQ32_spl
| member(X0,unordered_pair(X0,X1)) ),
inference(paramodulation,[status(thm)],[f237,f1999]) ).
fof(f9046,plain,
( ~ sQ32_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f9044,f523,f1998]) ).
fof(f9288,definition,
( sQ159_spl
<=> x = x ),
introduced(definition,[new_symbols(definition,[sQ159_spl])],[split_symbol_definition]) ).
fof(f9431,plain,
! [X0] :
( ~ sQ154_spl
| ~ member(X0,unordered_pair(y,x)) ),
inference(resolution,[status(thm)],[f9002,f475]) ).
fof(f9444,plain,
( ~ sQ143_spl
| ~ sQ154_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f8432,f9431]) ).
fof(f9445,definition,
( sQ161_spl
<=> subclass(null_class,unordered_pair(y,x)) ),
introduced(definition,[new_symbols(definition,[sQ161_spl])],[split_symbol_definition]) ).
fof(f9447,plain,
( sQ161_spl
| ~ subclass(null_class,unordered_pair(y,x)) ),
inference(component_clause,[status(thm)],[f9445]) ).
fof(f9449,plain,
( ~ sQ143_spl
| ~ sQ154_spl ),
inference(contradiction_clause,[status(thm)],[f9444]) ).
fof(f9450,plain,
( sQ161_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f9447,f233]) ).
fof(f9451,plain,
sQ161_spl,
inference(contradiction_clause,[status(thm)],[f9450]) ).
fof(f9514,plain,
( sQ154_spl
| not_subclass_element(unordered_pair(x,y),null_class) = x
| not_subclass_element(unordered_pair(x,y),null_class) = y ),
inference(resolution,[status(thm)],[f9003,f1308]) ).
fof(f9524,definition,
( sQ162_spl
<=> not_subclass_element(unordered_pair(x,y),null_class) = y ),
introduced(definition,[new_symbols(definition,[sQ162_spl])],[split_symbol_definition]) ).
fof(f9525,plain,
( ~ sQ162_spl
| not_subclass_element(unordered_pair(x,y),null_class) = y ),
inference(component_clause,[status(thm)],[f9524]) ).
fof(f9527,definition,
( sQ163_spl
<=> not_subclass_element(unordered_pair(x,y),null_class) = x ),
introduced(definition,[new_symbols(definition,[sQ163_spl])],[split_symbol_definition]) ).
fof(f9530,plain,
( sQ154_spl
| sQ163_spl
| sQ162_spl ),
inference(split_clause,[status(thm)],[f9514,f9524,f9527,f9001]) ).
fof(f9533,plain,
( ~ sQ162_spl
| not_subclass_element(unordered_pair(y,x),null_class) = y ),
inference(forward_demodulation,[status(thm)],[f237,f9525]) ).
fof(f9534,plain,
( ~ sQ162_spl
| ~ sQ36_spl
| x = y ),
inference(forward_demodulation,[status(thm)],[f2439,f9533]) ).
fof(f9535,plain,
( ~ sQ162_spl
| ~ sQ36_spl
| sQ37_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f9534,f8203]) ).
fof(f9536,plain,
( ~ sQ162_spl
| ~ sQ36_spl
| sQ37_spl ),
inference(contradiction_clause,[status(thm)],[f9535]) ).
fof(f9570,plain,
( ~ sQ143_spl
| x = y
| x = x ),
inference(resolution,[status(thm)],[f8432,f120]) ).
fof(f9579,plain,
( ~ sQ143_spl
| sQ66_spl
| sQ159_spl ),
inference(split_clause,[status(thm)],[f9570,f9288,f3816,f8431]) ).
fof(f9581,plain,
( ~ sQ66_spl
| sQ37_spl
| ~ sQ36_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3817,f8203]) ).
fof(f9582,plain,
( ~ sQ66_spl
| sQ37_spl
| ~ sQ36_spl ),
inference(contradiction_clause,[status(thm)],[f9581]) ).
fof(f9729,plain,
( ~ sQ72_spl
| unordered_pair(y,x) = null_class
| member(y,unordered_pair(y,x)) ),
inference(paramodulation,[status(thm)],[f4148,f185]) ).
fof(f9731,plain,
( ~ sQ72_spl
| sQ40_spl
| sQ41_spl ),
inference(split_clause,[status(thm)],[f9729,f2491,f2488,f4147]) ).
fof(f9789,definition,
( sQ167_spl
<=> x = not_subclass_element(unordered_pair(y,x),unordered_pair(x,x)) ),
introduced(definition,[new_symbols(definition,[sQ167_spl])],[split_symbol_definition]) ).
fof(f9790,plain,
( ~ sQ167_spl
| x = not_subclass_element(unordered_pair(y,x),unordered_pair(x,x)) ),
inference(component_clause,[status(thm)],[f9789]) ).
fof(f9791,plain,
( sQ167_spl
| x != not_subclass_element(unordered_pair(y,x),unordered_pair(x,x)) ),
inference(component_clause,[status(thm)],[f9789]) ).
fof(f9804,plain,
( ~ sQ167_spl
| not_subclass_element(unordered_pair(y,x),singleton(x)) = x ),
inference(forward_demodulation,[status(thm)],[f126,f9790]) ).
fof(f9838,plain,
( ~ sQ140_spl
| singleton(x) = null_class
| ~ member(regular(singleton(x)),x) ),
inference(resolution,[status(thm)],[f8441,f185]) ).
fof(f9839,plain,
( ~ sQ140_spl
| null_class = singleton(x)
| ~ member(not_subclass_element(singleton(x),null_class),x) ),
inference(resolution,[status(thm)],[f8441,f235]) ).
fof(f9844,plain,
! [X0] :
( ~ sQ140_spl
| ~ member(x,X0)
| ~ member(x,x) ),
inference(resolution,[status(thm)],[f8441,f491]) ).
fof(f9845,definition,
( sQ170_spl
<=> member(not_subclass_element(singleton(x),null_class),x) ),
introduced(definition,[new_symbols(definition,[sQ170_spl])],[split_symbol_definition]) ).
fof(f9848,plain,
( ~ sQ140_spl
| sQ35_spl
| ~ sQ170_spl ),
inference(split_clause,[status(thm)],[f9839,f9845,f2435,f8358]) ).
fof(f9856,definition,
( sQ173_spl
<=> member(x,x) ),
introduced(definition,[new_symbols(definition,[sQ173_spl])],[split_symbol_definition]) ).
fof(f9859,plain,
( ~ sQ140_spl
| sQ44_spl
| ~ sQ173_spl ),
inference(split_clause,[status(thm)],[f9844,f9856,f2559,f8358]) ).
fof(f9860,definition,
( sQ174_spl
<=> member(regular(singleton(x)),x) ),
introduced(definition,[new_symbols(definition,[sQ174_spl])],[split_symbol_definition]) ).
fof(f9863,plain,
( ~ sQ140_spl
| sQ35_spl
| ~ sQ174_spl ),
inference(split_clause,[status(thm)],[f9838,f9860,f2435,f8358]) ).
fof(f10048,plain,
( ~ sQ132_spl
| ~ member(not_subclass_element(unordered_pair(y,x),singleton(x)),singleton(x))
| ~ member(x,unordered_pair(y,x))
| unordered_pair(y,x) = singleton(x) ),
inference(paramodulation,[status(thm)],[f8240,f230]) ).
fof(f10049,plain,
( ~ sQ132_spl
| subclass(singleton(x),unordered_pair(y,x))
| ~ member(x,unordered_pair(y,x)) ),
inference(paramodulation,[status(thm)],[f8240,f114]) ).
fof(f10051,definition,
( sQ175_spl
<=> subclass(singleton(x),unordered_pair(y,x)) ),
introduced(definition,[new_symbols(definition,[sQ175_spl])],[split_symbol_definition]) ).
fof(f10052,plain,
( ~ sQ175_spl
| subclass(singleton(x),unordered_pair(y,x)) ),
inference(component_clause,[status(thm)],[f10051]) ).
fof(f10053,plain,
( sQ175_spl
| ~ subclass(singleton(x),unordered_pair(y,x)) ),
inference(component_clause,[status(thm)],[f10051]) ).
fof(f10055,plain,
( ~ sQ132_spl
| sQ175_spl
| ~ sQ143_spl ),
inference(split_clause,[status(thm)],[f10049,f8431,f10051,f8239]) ).
fof(f10056,definition,
( sQ176_spl
<=> unordered_pair(y,x) = singleton(x) ),
introduced(definition,[new_symbols(definition,[sQ176_spl])],[split_symbol_definition]) ).
fof(f10057,plain,
( ~ sQ176_spl
| unordered_pair(y,x) = singleton(x) ),
inference(component_clause,[status(thm)],[f10056]) ).
fof(f10059,definition,
( sQ177_spl
<=> member(not_subclass_element(unordered_pair(y,x),singleton(x)),singleton(x)) ),
introduced(definition,[new_symbols(definition,[sQ177_spl])],[split_symbol_definition]) ).
fof(f10061,plain,
( sQ177_spl
| ~ member(not_subclass_element(unordered_pair(y,x),singleton(x)),singleton(x)) ),
inference(component_clause,[status(thm)],[f10059]) ).
fof(f10062,plain,
( ~ sQ132_spl
| ~ sQ177_spl
| ~ sQ143_spl
| sQ176_spl ),
inference(split_clause,[status(thm)],[f10048,f10056,f8431,f10059,f8239]) ).
fof(f10074,plain,
( ~ sQ176_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f10057,f243]) ).
fof(f10075,plain,
~ sQ176_spl,
inference(contradiction_clause,[status(thm)],[f10074]) ).
fof(f10168,plain,
! [X0,X1] :
( ~ sQ141_spl
| x = ordered_pair(first(x),second(x))
| not_subclass_element(singleton(x),cross_product(X0,X1)) = x ),
inference(resolution,[status(thm)],[f8366,f134]) ).
fof(f10191,definition,
! [X1] :
( sQ182_spl
<=> ( x = not_subclass_element(singleton(x),X1)
| member(x,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ182_spl])],[split_symbol_definition]) ).
fof(f10196,definition,
! [X0,X1] :
( sQ183_spl
<=> not_subclass_element(singleton(x),cross_product(X0,X1)) = x ),
introduced(definition,[new_symbols(definition,[sQ183_spl])],[split_symbol_definition]) ).
fof(f10199,definition,
( sQ184_spl
<=> x = ordered_pair(first(x),second(x)) ),
introduced(definition,[new_symbols(definition,[sQ184_spl])],[split_symbol_definition]) ).
fof(f10202,plain,
( ~ sQ141_spl
| sQ184_spl
| sQ183_spl ),
inference(split_clause,[status(thm)],[f10168,f10196,f10199,f8362]) ).
fof(f10225,definition,
! [X0] :
( sQ185_spl
<=> subclass(singleton(x),X0) ),
introduced(definition,[new_symbols(definition,[sQ185_spl])],[split_symbol_definition]) ).
fof(f10226,plain,
! [X0] :
( ~ sQ185_spl
| subclass(singleton(x),X0) ),
inference(component_clause,[status(thm)],[f10225]) ).
fof(f10285,plain,
( sQ177_spl
| ~ sQ167_spl
| ~ member(x,singleton(x)) ),
inference(forward_demodulation,[status(thm)],[f9804,f10061]) ).
fof(f10286,plain,
( sQ177_spl
| ~ sQ167_spl
| ~ sQ141_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f10285,f8363]) ).
fof(f10287,plain,
( sQ177_spl
| ~ sQ167_spl
| ~ sQ141_spl ),
inference(contradiction_clause,[status(thm)],[f10286]) ).
fof(f10288,plain,
( sQ167_spl
| not_subclass_element(unordered_pair(y,x),singleton(x)) != x ),
inference(forward_demodulation,[status(thm)],[f126,f9791]) ).
fof(f10289,plain,
( ~ sQ133_spl
| sQ167_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f8243,f10288]) ).
fof(f10290,plain,
( ~ sQ133_spl
| sQ167_spl ),
inference(contradiction_clause,[status(thm)],[f10289]) ).
fof(f10498,plain,
( ~ sQ175_spl
| singleton(x) = unordered_pair(y,x)
| ~ subclass(unordered_pair(y,x),singleton(x)) ),
inference(resolution,[status(thm)],[f10052,f118]) ).
fof(f10505,definition,
( sQ207_spl
<=> subclass(unordered_pair(y,x),singleton(x)) ),
introduced(definition,[new_symbols(definition,[sQ207_spl])],[split_symbol_definition]) ).
fof(f10507,plain,
( sQ207_spl
| ~ subclass(unordered_pair(y,x),singleton(x)) ),
inference(component_clause,[status(thm)],[f10505]) ).
fof(f10508,plain,
( ~ sQ175_spl
| sQ176_spl
| ~ sQ207_spl ),
inference(split_clause,[status(thm)],[f10498,f10505,f10056,f10051]) ).
fof(f10677,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)],[f8267,f187]) ).
fof(f10690,definition,
! [X0] :
( sQ215_spl
<=> ~ function(X0) ),
introduced(definition,[new_symbols(definition,[sQ215_spl])],[split_symbol_definition]) ).
fof(f10691,plain,
! [X0] :
( ~ sQ215_spl
| ~ function(X0) ),
inference(component_clause,[status(thm)],[f10690]) ).
fof(f10796,plain,
( ~ sQ131_spl
| member(y,unordered_pair(y,x))
| subclass(unordered_pair(y,x),singleton(x)) ),
inference(paramodulation,[status(thm)],[f8237,f113]) ).
fof(f10809,plain,
( ~ sQ131_spl
| sQ41_spl
| sQ207_spl ),
inference(split_clause,[status(thm)],[f10796,f10505,f2491,f8236]) ).
fof(f10983,plain,
! [X0,X1] :
( ~ sQ185_spl
| member(X0,X1)
| ~ member(X0,singleton(x)) ),
inference(resolution,[status(thm)],[f10226,f112]) ).
fof(f10986,plain,
! [X0] :
( ~ sQ140_spl
| ~ sQ185_spl
| ~ member(X0,singleton(x)) ),
inference(backward_subsumption_resolution,[status(thm)],[f8441,f10983]) ).
fof(f10987,plain,
( ~ sQ141_spl
| ~ sQ140_spl
| ~ sQ185_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f8363,f10986]) ).
fof(f10989,plain,
( ~ sQ141_spl
| ~ sQ140_spl
| ~ sQ185_spl ),
inference(contradiction_clause,[status(thm)],[f10987]) ).
fof(f11100,definition,
( sQ239_spl
<=> subclass(null_class,element_relation) ),
introduced(definition,[new_symbols(definition,[sQ239_spl])],[split_symbol_definition]) ).
fof(f11102,plain,
( sQ239_spl
| ~ subclass(null_class,element_relation) ),
inference(component_clause,[status(thm)],[f11100]) ).
fof(f11122,definition,
( sQ244_spl
<=> subclass(null_class,successor_relation) ),
introduced(definition,[new_symbols(definition,[sQ244_spl])],[split_symbol_definition]) ).
fof(f11124,plain,
( sQ244_spl
| ~ subclass(null_class,successor_relation) ),
inference(component_clause,[status(thm)],[f11122]) ).
fof(f11142,plain,
( sQ244_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f11124,f233]) ).
fof(f11143,plain,
sQ244_spl,
inference(contradiction_clause,[status(thm)],[f11142]) ).
fof(f11155,plain,
( sQ239_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f11102,f233]) ).
fof(f11156,plain,
sQ239_spl,
inference(contradiction_clause,[status(thm)],[f11155]) ).
fof(f11165,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(f11166,plain,
! [X0,X1,X2] :
( ~ sQ251_spl
| intersection(X0,null_class) = restrict(X0,X1,X2) ),
inference(component_clause,[status(thm)],[f11165]) ).
fof(f11178,definition,
! [X0,X1] :
( sQ254_spl
<=> cross_product(X0,X1) = null_class ),
introduced(definition,[new_symbols(definition,[sQ254_spl])],[split_symbol_definition]) ).
fof(f11179,plain,
! [X0,X1] :
( ~ sQ254_spl
| cross_product(X0,X1) = null_class ),
inference(component_clause,[status(thm)],[f11178]) ).
fof(f11200,plain,
! [X0] :
( ~ sQ251_spl
| domain_of(intersection(element_relation,null_class)) = sum_class(X0) ),
inference(backward_demodulation,[status(thm)],[f11166,f172]) ).
fof(f11202,plain,
! [X0] :
( ~ sQ86_spl
| ~ sQ251_spl
| null_class = intersection(X0,null_class) ),
inference(backward_demodulation,[status(thm)],[f11166,f4775]) ).
fof(f11206,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)],[f11166,f160]) ).
fof(f11226,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)],[f11166,f1224]) ).
fof(f11230,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)],[f11166,f1149]) ).
fof(f11240,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)],[f11166,f1903]) ).
fof(f11243,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)],[f11166,f1479]) ).
fof(f11244,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)],[f11166,f8251]) ).
fof(f11249,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)],[f11166,f8626]) ).
fof(f11250,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)],[f11166,f8616]) ).
fof(f11251,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)],[f11166,f8555]) ).
fof(f11252,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)],[f11166,f8546]) ).
fof(f11255,plain,
! [X0,X1] :
( ~ sQ122_spl
| ~ sQ251_spl
| intersection(X1,null_class) = null_class
| X0 = regular(singleton(X0)) ),
inference(backward_demodulation,[status(thm)],[f11166,f8289]) ).
fof(f11256,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)],[f11166,f8256]) ).
fof(f11257,plain,
! [X0,X1] :
( ~ sQ122_spl
| ~ sQ251_spl
| null_class = intersection(X1,null_class)
| apply(choice,singleton(X0)) = X0 ),
inference(backward_demodulation,[status(thm)],[f11166,f8629]) ).
fof(f11258,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)],[f11166,f8549]) ).
fof(f11259,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)],[f11166,f8076]) ).
fof(f11267,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)],[f11166,f2153]) ).
fof(f11289,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(f11292,definition,
( sQ259_spl
<=> function(intersection(element_relation,null_class)) ),
introduced(definition,[new_symbols(definition,[sQ259_spl])],[split_symbol_definition]) ).
fof(f11295,plain,
( ~ sQ251_spl
| ~ sQ259_spl
| sQ258_spl ),
inference(split_clause,[status(thm)],[f11243,f11289,f11292,f11165]) ).
fof(f11296,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)],[f11166,f11226]) ).
fof(f11297,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)],[f11166,f11267]) ).
fof(f11298,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)],[f11166,f11297]) ).
fof(f11299,plain,
! [X0,X1] :
( ~ sQ251_spl
| apply(X0,X1) = domain_of(intersection(element_relation,null_class)) ),
inference(backward_demodulation,[status(thm)],[f11200,f187]) ).
fof(f11310,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(f11313,definition,
( sQ261_spl
<=> operation(intersection(element_relation,null_class)) ),
introduced(definition,[new_symbols(definition,[sQ261_spl])],[split_symbol_definition]) ).
fof(f11316,plain,
( ~ sQ251_spl
| ~ sQ261_spl
| sQ260_spl ),
inference(split_clause,[status(thm)],[f11240,f11310,f11313,f11165]) ).
fof(f11338,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)],[f11299,f10677]) ).
fof(f11349,plain,
! [X0,X1] :
( ~ sQ251_spl
| ~ sQ86_spl
| apply(X0,X1) = domain_of(null_class) ),
inference(backward_demodulation,[status(thm)],[f11202,f11299]) ).
fof(f11351,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)],[f11202,f11296]) ).
fof(f11359,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)],[f11202,f11298]) ).
fof(f11411,plain,
! [X0] :
( ~ sQ251_spl
| ~ sQ86_spl
| ~ member(X0,subset_relation)
| member(X0,null_class) ),
inference(forward_demodulation,[status(thm)],[f11202,f11230]) ).
fof(f11416,plain,
! [X0] :
( ~ sQ17_spl
| ~ sQ251_spl
| ~ sQ86_spl
| ~ member(X0,omega) ),
inference(backward_subsumption_resolution,[status(thm)],[f1244,f11419]) ).
fof(f11419,plain,
! [X0] :
( ~ sQ251_spl
| ~ sQ86_spl
| ~ member(X0,subset_relation) ),
inference(forward_subsumption_resolution,[status(thm)],[f11411,f232]) ).
fof(f11424,definition,
! [X0] :
( sQ264_spl
<=> X0 = not_subclass_element(singleton(X0),null_class) ),
introduced(definition,[new_symbols(definition,[sQ264_spl])],[split_symbol_definition]) ).
fof(f11427,definition,
! [X1] :
( sQ265_spl
<=> intersection(X1,null_class) = null_class ),
introduced(definition,[new_symbols(definition,[sQ265_spl])],[split_symbol_definition]) ).
fof(f11430,plain,
( ~ sQ122_spl
| ~ sQ251_spl
| sQ265_spl
| sQ264_spl ),
inference(split_clause,[status(thm)],[f11258,f11424,f11427,f11165,f8070]) ).
fof(f11470,definition,
! [X0] :
( sQ266_spl
<=> apply(choice,singleton(X0)) = X0 ),
introduced(definition,[new_symbols(definition,[sQ266_spl])],[split_symbol_definition]) ).
fof(f11473,plain,
( ~ sQ122_spl
| ~ sQ251_spl
| sQ265_spl
| sQ266_spl ),
inference(split_clause,[status(thm)],[f11257,f11470,f11427,f11165,f8070]) ).
fof(f11509,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(f11512,definition,
( sQ268_spl
<=> function(null_class) ),
introduced(definition,[new_symbols(definition,[sQ268_spl])],[split_symbol_definition]) ).
fof(f11515,plain,
( ~ sQ251_spl
| ~ sQ86_spl
| ~ sQ268_spl
| sQ267_spl ),
inference(split_clause,[status(thm)],[f11359,f11509,f11512,f4774,f11165]) ).
fof(f11556,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(f11559,plain,
( ~ sQ122_spl
| ~ sQ251_spl
| sQ77_spl
| sQ269_spl ),
inference(split_clause,[status(thm)],[f11338,f11556,f4190,f11165,f8070]) ).
fof(f11560,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(f11563,plain,
( ~ sQ122_spl
| ~ sQ251_spl
| sQ265_spl
| sQ270_spl ),
inference(split_clause,[status(thm)],[f11256,f11560,f11427,f11165,f8070]) ).
fof(f11600,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)],[f11179,f132]) ).
fof(f11722,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(f11725,plain,
( ~ sQ122_spl
| ~ sQ251_spl
| sQ265_spl
| sQ273_spl ),
inference(split_clause,[status(thm)],[f11252,f11722,f11427,f11165,f8070]) ).
fof(f11729,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)],[f11349,f3878]) ).
fof(f11742,plain,
( ~ sQ122_spl
| ~ sQ251_spl
| sQ265_spl
| sQ77_spl ),
inference(split_clause,[status(thm)],[f11259,f4190,f11427,f11165,f8070]) ).
fof(f11752,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(f11755,plain,
( ~ sQ122_spl
| ~ sQ251_spl
| sQ265_spl
| sQ275_spl ),
inference(split_clause,[status(thm)],[f11250,f11752,f11427,f11165,f8070]) ).
fof(f11772,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(f11775,definition,
( sQ277_spl
<=> null_class = intersection(null_class,null_class) ),
introduced(definition,[new_symbols(definition,[sQ277_spl])],[split_symbol_definition]) ).
fof(f11778,plain,
( ~ sQ251_spl
| ~ sQ86_spl
| sQ277_spl
| sQ276_spl ),
inference(split_clause,[status(thm)],[f11351,f11772,f11775,f4774,f11165]) ).
fof(f11784,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(f11787,plain,
( ~ sQ122_spl
| ~ sQ251_spl
| sQ265_spl
| sQ279_spl ),
inference(split_clause,[status(thm)],[f11251,f11784,f11427,f11165,f8070]) ).
fof(f11799,plain,
( ~ sQ17_spl
| ~ sQ251_spl
| ~ sQ86_spl
| sQ7_spl ),
inference(split_clause,[status(thm)],[f11416,f1010,f4774,f11165,f1243]) ).
fof(f11810,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(f11813,plain,
( ~ sQ122_spl
| ~ sQ251_spl
| sQ280_spl
| sQ265_spl ),
inference(split_clause,[status(thm)],[f11244,f11427,f11810,f11165,f8070]) ).
fof(f11826,plain,
! [X0] :
( ~ sQ254_spl
| ~ member(X0,universal_class) ),
inference(backward_subsumption_resolution,[status(thm)],[f175,f11871]) ).
fof(f11871,plain,
! [X0,X1,X2,X3] :
( ~ sQ254_spl
| ~ member(X2,X3)
| ~ member(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f11600,f232]) ).
fof(f11917,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)],[f11921,f8266]) ).
fof(f11921,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)],[f11202,f11206]) ).
fof(f11965,plain,
( ~ sQ122_spl
| ~ sQ251_spl
| sQ265_spl
| sQ130_spl ),
inference(split_clause,[status(thm)],[f11255,f8193,f11427,f11165,f8070]) ).
fof(f11966,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(f11969,plain,
( ~ sQ122_spl
| ~ sQ251_spl
| sQ287_spl
| sQ265_spl ),
inference(split_clause,[status(thm)],[f11249,f11427,f11966,f11165,f8070]) ).
fof(f11986,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(f11989,plain,
( ~ sQ122_spl
| ~ sQ251_spl
| ~ sQ86_spl
| sQ289_spl
| sQ77_spl ),
inference(split_clause,[status(thm)],[f11917,f4190,f11986,f4774,f11165,f8070]) ).
fof(f12022,definition,
! [X0,X1] :
( sQ295_spl
<=> ~ member(image(X0,singleton(X1)),universal_class) ),
introduced(definition,[new_symbols(definition,[sQ295_spl])],[split_symbol_definition]) ).
fof(f12025,definition,
( sQ296_spl
<=> member(domain_of(null_class),universal_class) ),
introduced(definition,[new_symbols(definition,[sQ296_spl])],[split_symbol_definition]) ).
fof(f12028,plain,
( ~ sQ251_spl
| ~ sQ86_spl
| sQ296_spl
| sQ295_spl ),
inference(split_clause,[status(thm)],[f11729,f12022,f12025,f4774,f11165]) ).
fof(f12029,plain,
( ~ sQ254_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f236,f11826]) ).
fof(f12044,plain,
~ sQ254_spl,
inference(contradiction_clause,[status(thm)],[f12029]) ).
fof(f12083,plain,
( ~ sQ215_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f188,f10691]) ).
fof(f12094,plain,
~ sQ215_spl,
inference(contradiction_clause,[status(thm)],[f12083]) ).
fof(f12213,definition,
( sQ297_spl
<=> member(not_subclass_element(null_class,singleton(x)),null_class) ),
introduced(definition,[new_symbols(definition,[sQ297_spl])],[split_symbol_definition]) ).
fof(f12214,plain,
( ~ sQ297_spl
| member(not_subclass_element(null_class,singleton(x)),null_class) ),
inference(component_clause,[status(thm)],[f12213]) ).
fof(f12297,plain,
! [X0] :
( inductive(universal_class)
| ~ subclass(image(successor_relation,universal_class),universal_class)
| ~ member(null_class,X0) ),
inference(resolution,[status(thm)],[f462,f168]) ).
fof(f12301,plain,
( sQ150_spl
| ~ sQ149_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f12297,f494,f8851,f8854]) ).
fof(f12326,plain,
( sQ207_spl
| not_subclass_element(unordered_pair(y,x),singleton(x)) = y
| x = not_subclass_element(unordered_pair(y,x),singleton(x)) ),
inference(resolution,[status(thm)],[f10507,f1279]) ).
fof(f12332,plain,
( sQ207_spl
| sQ131_spl
| sQ133_spl ),
inference(split_clause,[status(thm)],[f12326,f8242,f8236,f10505]) ).
fof(f12336,definition,
( sQ302_spl
<=> not_subclass_element(unordered_pair(x,y),singleton(x)) = x ),
introduced(definition,[new_symbols(definition,[sQ302_spl])],[split_symbol_definition]) ).
fof(f12337,plain,
( ~ sQ302_spl
| not_subclass_element(unordered_pair(x,y),singleton(x)) = x ),
inference(component_clause,[status(thm)],[f12336]) ).
fof(f12555,plain,
( sQ175_spl
| x = not_subclass_element(singleton(x),unordered_pair(y,x)) ),
inference(resolution,[status(thm)],[f10053,f1273]) ).
fof(f12561,plain,
( sQ175_spl
| sQ132_spl ),
inference(split_clause,[status(thm)],[f12555,f8239,f10051]) ).
fof(f12562,plain,
( ~ sQ302_spl
| not_subclass_element(unordered_pair(y,x),singleton(x)) = x ),
inference(forward_demodulation,[status(thm)],[f237,f12337]) ).
fof(f12663,plain,
( sQ33_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2402,f236]) ).
fof(f12664,plain,
sQ33_spl,
inference(contradiction_clause,[status(thm)],[f12663]) ).
fof(f12975,plain,
( ~ sQ167_spl
| subclass(unordered_pair(y,x),singleton(x))
| ~ member(x,singleton(x)) ),
inference(paramodulation,[status(thm)],[f9804,f114]) ).
fof(f12979,plain,
( ~ sQ167_spl
| sQ207_spl
| ~ sQ141_spl ),
inference(split_clause,[status(thm)],[f12975,f8362,f10505,f9789]) ).
fof(f12998,plain,
( ~ sQ35_spl
| null_class != unordered_pair(y,x) ),
inference(backward_demodulation,[status(thm)],[f2436,f243]) ).
fof(f13077,plain,
( ~ sQ35_spl
| ~ sQ40_spl ),
inference(split_clause,[status(thm)],[f12998,f2488,f2435]) ).
fof(f13387,plain,
( ~ sQ297_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f12214,f232]) ).
fof(f13388,plain,
~ sQ297_spl,
inference(contradiction_clause,[status(thm)],[f13387]) ).
fof(f13392,plain,
( ~ sQ302_spl
| sQ133_spl ),
inference(split_clause,[status(thm)],[f12562,f8242,f12336]) ).
fof(f13540,plain,
( ~ sQ141_spl
| sQ182_spl ),
inference(split_clause,[status(thm)],[f8366,f10191,f8362]) ).
fof(f13553,plain,
( ~ sQ141_spl
| ~ sQ44_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f8363,f2560]) ).
fof(f13554,plain,
( ~ sQ141_spl
| ~ sQ44_spl ),
inference(contradiction_clause,[status(thm)],[f13553]) ).
fof(f13555,plain,
$false,
inference(sat_refutation,[status(thm)],[f500,f503,f529,f550,f1098,f1135,f1249,f1399,f1403,f1466,f1691,f1997,f2004,f2318,f2467,f2494,f2496,f2515,f2562,f2680,f2692,f2829,f2910,f3036,f3108,f3838,f3839,f3876,f3913,f4236,f4416,f4789,f5223,f5261,f5971,f7065,f7067,f8073,f8187,f8202,f8217,f8219,f8220,f8247,f8269,f8282,f8286,f8290,f8294,f8361,f8365,f8429,f8539,f8540,f8553,f8573,f8620,f8630,f8659,f8672,f8733,f8833,f8861,f8865,f8870,f8874,f8876,f8878,f9014,f9017,f9046,f9449,f9451,f9530,f9536,f9579,f9582,f9731,f9848,f9859,f9863,f10055,f10062,f10075,f10202,f10287,f10290,f10508,f10809,f10989,f11143,f11156,f11295,f11316,f11430,f11473,f11515,f11559,f11563,f11725,f11742,f11755,f11778,f11787,f11799,f11813,f11965,f11969,f11989,f12028,f12044,f12094,f12301,f12332,f12561,f12664,f12979,f13077,f13388,f13392,f13540,f13554]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SET069-7 : TPTP v9.3.1. Bugfixed v2.1.0.
% 0.00/0.07 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.19/0.46 % Computer : n016.cluster.edu
% 0.19/0.46 % Model : x86_64 x86_64
% 0.19/0.46 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.46 % Memory : 8046.5625MB
% 0.19/0.46 % OS : Linux 6.8.0-71-generic
% 0.19/0.46 % CPULimit : 300
% 0.19/0.46 % WCLimit : 300
% 0.19/0.46 % DateTime : Mon Sep 21 04:54:11 UTC 2026
% 0.19/0.47 % CPUTime :
% 0.19/0.51 % Drodi V4.1.1
% 230.69/30.05 % Refutation found
% 230.69/30.05 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 230.69/30.05 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 11.84/30.49 % Elapsed time: 29.991591 seconds
% 11.84/30.49 % CPU time: 234.703306 seconds
% 11.84/30.49 % Total memory used: 715.972 MB
% 11.84/30.49 % Net memory used: 627.013 MB
%------------------------------------------------------------------------------