%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SET066-7 : TPTP v9.3.1. Bugfixed v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n026.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:09 PM UTC 2026
% Result : Unsatisfiable 222.43s 28.62s
% Output : CNFRefutation 202.20s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 194
% Syntax : Number of formulae : 855 ( 54 unt; 155 def)
% Number of atoms : 2367 ( 589 equ)
% Maximal formula atoms : 9 ( 2 avg)
% Number of connectives : 2414 ( 902 ~;1357 |; 0 &)
% ( 155 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 160 ( 158 usr; 156 prp; 0-2 aty)
% Number of functors : 20 ( 20 usr; 8 con; 0-3 aty)
% Number of variables : 554 ( 554 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X,Y,U] :
( member(U,Y)
| ~ member(U,X)
| ~ subclass(X,Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [X,Y] :
( subclass(X,Y)
| member(not_subclass_element(X,Y),X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [X,Y] :
( subclass(X,Y)
| ~ member(not_subclass_element(X,Y),Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [X] : subclass(X,universal_class),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [X,Y] :
( X = Y
| ~ subclass(Y,X)
| ~ subclass(X,Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [U,X,Y] :
( U = Y
| U = X
| ~ member(U,unordered_pair(X,Y)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [X,Y] :
( member(X,unordered_pair(X,Y))
| ~ member(X,universal_class) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f10,axiom,
! [Y,X] :
( member(Y,unordered_pair(X,Y))
| ~ member(Y,universal_class) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f11,axiom,
! [X,Y] : member(unordered_pair(X,Y),universal_class),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [X] : unordered_pair(X,X) = singleton(X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f13,axiom,
! [X,Y] : unordered_pair(singleton(X),unordered_pair(X,singleton(Y))) = ordered_pair(X,Y),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f15,axiom,
! [U,V,X,Y] :
( member(V,Y)
| ~ member(ordered_pair(U,V),cross_product(X,Y)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f16,axiom,
! [U,X,V,Y] :
( member(ordered_pair(U,V),cross_product(X,Y))
| ~ member(V,Y)
| ~ member(U,X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f18,axiom,
subclass(element_relation,cross_product(universal_class,universal_class)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f20,axiom,
! [X,Y] :
( member(ordered_pair(X,Y),element_relation)
| ~ member(X,Y)
| ~ member(ordered_pair(X,Y),cross_product(universal_class,universal_class)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f23,axiom,
! [Z,X,Y] :
( member(Z,intersection(X,Y))
| ~ member(Z,Y)
| ~ member(Z,X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f25,axiom,
! [Z,X] :
( member(Z,X)
| member(Z,complement(X))
| ~ member(Z,universal_class) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f31,axiom,
! [Z,X] :
( member(Z,domain_of(X))
| restrict(X,singleton(Z),universal_class) = null_class
| ~ member(Z,universal_class) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f47,axiom,
! [X] :
( member(null_class,X)
| ~ inductive(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f49,axiom,
! [X] :
( inductive(X)
| ~ subclass(image(successor_relation,X),X)
| ~ member(null_class,X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f50,axiom,
inductive(omega),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f51,axiom,
! [Y] :
( subclass(omega,Y)
| ~ inductive(Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f52,axiom,
member(omega,universal_class),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f66,axiom,
! [X] :
( member(regular(X),X)
| X = null_class ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f67,axiom,
! [X] :
( intersection(X,regular(X)) = null_class
| X = null_class ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f70,axiom,
! [Y] :
( member(apply(choice,Y),Y)
| Y = null_class
| ~ member(Y,universal_class) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f92,axiom,
! [X,Y,U,V] :
( member(X,unordered_pair(X,Y))
| ~ member(ordered_pair(X,Y),cross_product(U,V)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f93,axiom,
! [X,Y,U,V] :
( member(Y,unordered_pair(X,Y))
| ~ member(ordered_pair(X,Y),cross_product(U,V)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f94,axiom,
! [U,V,X,Y] :
( member(U,universal_class)
| ~ member(ordered_pair(U,V),cross_product(X,Y)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f97,axiom,
! [X,Y,Z] :
( subclass(X,Z)
| ~ subclass(Y,Z)
| ~ subclass(X,Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f98,axiom,
! [X,Y] :
( member(not_subclass_element(Y,X),Y)
| member(not_subclass_element(X,Y),X)
| X = Y ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f99,axiom,
! [X,Y] :
( member(not_subclass_element(Y,X),Y)
| X = Y
| ~ member(not_subclass_element(X,Y),Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f101,axiom,
! [X,Y] :
( X = Y
| ~ member(not_subclass_element(Y,X),X)
| ~ member(not_subclass_element(X,Y),Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f103,axiom,
! [Z] : ~ member(Z,null_class),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f104,axiom,
! [X] : subclass(null_class,X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f105,axiom,
! [X] :
( X = null_class
| ~ subclass(X,null_class) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f106,axiom,
! [Z] :
( member(not_subclass_element(Z,null_class),Z)
| Z = null_class ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f107,axiom,
member(null_class,universal_class),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f108,negated_conjecture,
unordered_pair(x,y) != unordered_pair(y,x),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f109,plain,
! [Y,U] :
( member(U,Y)
| ! [X] :
( ~ member(U,X)
| ~ subclass(X,Y) ) ),
inference(miniscoping,[status(thm)],[f1]) ).
fof(f110,plain,
! [X0,X1,X2] :
( member(X0,X2)
| ~ subclass(X1,X2)
| ~ member(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f109]) ).
fof(f111,plain,
! [X0,X1] :
( subclass(X0,X1)
| member(not_subclass_element(X0,X1),X0) ),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f112,plain,
! [X0,X1] :
( ~ member(not_subclass_element(X0,X1),X1)
| subclass(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f113,plain,
! [X0] : subclass(X0,universal_class),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f116,plain,
! [X0,X1] :
( ~ subclass(X1,X0)
| X0 = X1
| ~ subclass(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f117,plain,
! [U,Y] :
( U = Y
| ! [X] :
( U = X
| ~ member(U,unordered_pair(X,Y)) ) ),
inference(miniscoping,[status(thm)],[f8]) ).
fof(f118,plain,
! [X0,X1,X2] :
( X1 = X2
| ~ member(X1,unordered_pair(X2,X0))
| X0 = X1 ),
inference(cnf_transformation,[status(thm)],[f117]) ).
fof(f119,plain,
! [X] :
( ! [Y] : member(X,unordered_pair(X,Y))
| ~ member(X,universal_class) ),
inference(miniscoping,[status(thm)],[f9]) ).
fof(f120,plain,
! [X0,X1] :
( ~ member(X0,universal_class)
| member(X0,unordered_pair(X0,X1)) ),
inference(cnf_transformation,[status(thm)],[f119]) ).
fof(f121,plain,
! [Y] :
( ! [X] : member(Y,unordered_pair(X,Y))
| ~ member(Y,universal_class) ),
inference(miniscoping,[status(thm)],[f10]) ).
fof(f122,plain,
! [X0,X1] :
( member(X0,unordered_pair(X1,X0))
| ~ member(X0,universal_class) ),
inference(cnf_transformation,[status(thm)],[f121]) ).
fof(f123,plain,
! [X0,X1] : member(unordered_pair(X0,X1),universal_class),
inference(cnf_transformation,[status(thm)],[f11]) ).
fof(f124,plain,
! [X0] : singleton(X0) = unordered_pair(X0,X0),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f125,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,
! [V,Y] :
( member(V,Y)
| ! [U,X] : ~ member(ordered_pair(U,V),cross_product(X,Y)) ),
inference(miniscoping,[status(thm)],[f15]) ).
fof(f129,plain,
! [X0,X1,X2,X3] :
( ~ member(ordered_pair(X2,X0),cross_product(X3,X1))
| member(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f128]) ).
fof(f130,plain,
! [X0,X1,X2,X3] :
( ~ member(X0,X2)
| ~ member(X1,X3)
| member(ordered_pair(X0,X1),cross_product(X2,X3)) ),
inference(cnf_transformation,[status(thm)],[f16]) ).
fof(f133,plain,
subclass(element_relation,cross_product(universal_class,universal_class)),
inference(cnf_transformation,[status(thm)],[f18]) ).
fof(f135,plain,
! [X0,X1] :
( ~ member(X0,X1)
| ~ member(ordered_pair(X0,X1),cross_product(universal_class,universal_class))
| member(ordered_pair(X0,X1),element_relation) ),
inference(cnf_transformation,[status(thm)],[f20]) ).
fof(f140,plain,
! [X0,X1,X2] :
( ~ member(X0,X2)
| ~ member(X0,X1)
| member(X0,intersection(X1,X2)) ),
inference(cnf_transformation,[status(thm)],[f23]) ).
fof(f142,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] :
( ~ member(X1,universal_class)
| member(X1,domain_of(X0))
| restrict(X0,singleton(X1),universal_class) = null_class ),
inference(cnf_transformation,[status(thm)],[f31]) ).
fof(f164,plain,
! [X0] :
( member(null_class,X0)
| ~ inductive(X0) ),
inference(cnf_transformation,[status(thm)],[f47]) ).
fof(f166,plain,
! [X0] :
( ~ member(null_class,X0)
| ~ subclass(image(successor_relation,X0),X0)
| inductive(X0) ),
inference(cnf_transformation,[status(thm)],[f49]) ).
fof(f167,plain,
inductive(omega),
inference(cnf_transformation,[status(thm)],[f50]) ).
fof(f168,plain,
! [X0] :
( ~ inductive(X0)
| subclass(omega,X0) ),
inference(cnf_transformation,[status(thm)],[f51]) ).
fof(f169,plain,
member(omega,universal_class),
inference(cnf_transformation,[status(thm)],[f52]) ).
fof(f183,plain,
! [X0] :
( null_class = X0
| member(regular(X0),X0) ),
inference(cnf_transformation,[status(thm)],[f66]) ).
fof(f184,plain,
! [X0] :
( null_class = X0
| null_class = intersection(X0,regular(X0)) ),
inference(cnf_transformation,[status(thm)],[f67]) ).
fof(f187,plain,
! [X0] :
( member(apply(choice,X0),X0)
| X0 = null_class
| ~ member(X0,universal_class) ),
inference(cnf_transformation,[status(thm)],[f70]) ).
fof(f214,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(f215,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)],[f214]) ).
fof(f216,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(f217,plain,
! [X0,X1,X2,X3] :
( ~ member(ordered_pair(X1,X0),cross_product(X2,X3))
| member(X0,unordered_pair(X1,X0)) ),
inference(cnf_transformation,[status(thm)],[f216]) ).
fof(f218,plain,
! [U] :
( member(U,universal_class)
| ! [V,X,Y] : ~ member(ordered_pair(U,V),cross_product(X,Y)) ),
inference(miniscoping,[status(thm)],[f94]) ).
fof(f219,plain,
! [X0,X1,X2,X3] :
( member(X0,universal_class)
| ~ member(ordered_pair(X0,X1),cross_product(X2,X3)) ),
inference(cnf_transformation,[status(thm)],[f218]) ).
fof(f223,plain,
! [X,Z] :
( subclass(X,Z)
| ! [Y] :
( ~ subclass(Y,Z)
| ~ subclass(X,Y) ) ),
inference(miniscoping,[status(thm)],[f97]) ).
fof(f224,plain,
! [X0,X1,X2] :
( ~ subclass(X0,X2)
| ~ subclass(X2,X1)
| subclass(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f223]) ).
fof(f225,plain,
! [X0,X1] :
( X1 = X0
| member(not_subclass_element(X1,X0),X1)
| member(not_subclass_element(X0,X1),X0) ),
inference(cnf_transformation,[status(thm)],[f98]) ).
fof(f226,plain,
! [X0,X1] :
( X1 = X0
| ~ member(not_subclass_element(X1,X0),X0)
| member(not_subclass_element(X0,X1),X0) ),
inference(cnf_transformation,[status(thm)],[f99]) ).
fof(f228,plain,
! [X0,X1] :
( X0 = X1
| ~ member(not_subclass_element(X1,X0),X0)
| ~ member(not_subclass_element(X0,X1),X1) ),
inference(cnf_transformation,[status(thm)],[f101]) ).
fof(f230,plain,
! [X0] : ~ member(X0,null_class),
inference(cnf_transformation,[status(thm)],[f103]) ).
fof(f231,plain,
! [X0] : subclass(null_class,X0),
inference(cnf_transformation,[status(thm)],[f104]) ).
fof(f232,plain,
! [X0] :
( null_class = X0
| ~ subclass(X0,null_class) ),
inference(cnf_transformation,[status(thm)],[f105]) ).
fof(f233,plain,
! [X0] :
( member(not_subclass_element(X0,null_class),X0)
| X0 = null_class ),
inference(cnf_transformation,[status(thm)],[f106]) ).
fof(f234,plain,
member(null_class,universal_class),
inference(cnf_transformation,[status(thm)],[f107]) ).
fof(f235,plain,
unordered_pair(y,x) != unordered_pair(x,y),
inference(cnf_transformation,[status(thm)],[f108]) ).
fof(f243,plain,
! [X0,X1] : member(ordered_pair(X0,X1),universal_class),
inference(paramodulation,[status(thm)],[f125,f123]) ).
fof(f245,plain,
! [X0] : member(singleton(X0),universal_class),
inference(paramodulation,[status(thm)],[f124,f123]) ).
fof(f248,plain,
! [X0,X1] :
( X1 = X0
| ~ member(X0,singleton(X1))
| X0 = X1 ),
inference(paramodulation,[status(thm)],[f124,f118]) ).
fof(f249,plain,
! [X0,X1] :
( ~ member(X0,singleton(X1))
| X0 = X1 ),
inference(duplicate_literals_removal,[status(thm)],[f248]) ).
fof(f251,plain,
! [X0,X1,X2] :
( X0 = unordered_pair(X1,X2)
| not_subclass_element(unordered_pair(X1,X2),X0) = X2
| not_subclass_element(unordered_pair(X1,X2),X0) = X1
| member(not_subclass_element(X0,unordered_pair(X1,X2)),X0) ),
inference(resolution,[status(thm)],[f225,f118]) ).
fof(f265,plain,
! [X0,X1,X2] : member(ordered_pair(X0,X1),unordered_pair(X2,ordered_pair(X0,X1))),
inference(resolution,[status(thm)],[f122,f243]) ).
fof(f272,plain,
! [X0] :
( member(not_subclass_element(universal_class,null_class),unordered_pair(X0,not_subclass_element(universal_class,null_class)))
| universal_class = null_class ),
inference(resolution,[status(thm)],[f233,f122]) ).
fof(f273,plain,
! [X0] :
( restrict(X0,singleton(not_subclass_element(universal_class,null_class)),universal_class) = null_class
| member(not_subclass_element(universal_class,null_class),domain_of(X0))
| universal_class = null_class ),
inference(resolution,[status(thm)],[f233,f148]) ).
fof(f274,plain,
! [X0] :
( member(not_subclass_element(universal_class,null_class),unordered_pair(not_subclass_element(universal_class,null_class),X0))
| universal_class = null_class ),
inference(resolution,[status(thm)],[f233,f120]) ).
fof(f275,plain,
! [X0] :
( singleton(X0) = null_class
| not_subclass_element(singleton(X0),null_class) = X0 ),
inference(resolution,[status(thm)],[f233,f249]) ).
fof(f276,plain,
! [X0,X1] :
( X1 = not_subclass_element(unordered_pair(X0,X1),null_class)
| null_class = unordered_pair(X0,X1)
| X0 = not_subclass_element(unordered_pair(X0,X1),null_class) ),
inference(resolution,[status(thm)],[f233,f118]) ).
fof(f277,definition,
( sQ0_spl
<=> universal_class = null_class ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f278,plain,
( ~ sQ0_spl
| null_class = universal_class ),
inference(component_clause,[status(thm)],[f277]) ).
fof(f279,plain,
( sQ0_spl
| null_class != universal_class ),
inference(component_clause,[status(thm)],[f277]) ).
fof(f280,definition,
! [X0] :
( sQ1_spl
<=> ( restrict(X0,singleton(not_subclass_element(universal_class,null_class)),universal_class) = null_class
| member(not_subclass_element(universal_class,null_class),domain_of(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f283,plain,
( sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f273,f277,f280]) ).
fof(f284,definition,
! [X0] :
( sQ2_spl
<=> member(not_subclass_element(universal_class,null_class),unordered_pair(X0,not_subclass_element(universal_class,null_class))) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f285,plain,
! [X0] :
( ~ sQ2_spl
| member(not_subclass_element(universal_class,null_class),unordered_pair(X0,not_subclass_element(universal_class,null_class))) ),
inference(component_clause,[status(thm)],[f284]) ).
fof(f287,plain,
( sQ2_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f272,f277,f284]) ).
fof(f288,definition,
( sQ3_spl
<=> null_class = null_class ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f295,definition,
! [X0] :
( sQ5_spl
<=> member(not_subclass_element(universal_class,null_class),unordered_pair(not_subclass_element(universal_class,null_class),X0)) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f296,plain,
! [X0] :
( ~ sQ5_spl
| member(not_subclass_element(universal_class,null_class),unordered_pair(not_subclass_element(universal_class,null_class),X0)) ),
inference(component_clause,[status(thm)],[f295]) ).
fof(f298,plain,
( sQ5_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f274,f277,f295]) ).
fof(f316,plain,
! [X0] :
( ~ sQ0_spl
| ~ member(X0,universal_class) ),
inference(backward_demodulation,[status(thm)],[f278,f230]) ).
fof(f326,plain,
( ~ sQ0_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f243,f316]) ).
fof(f333,plain,
~ sQ0_spl,
inference(contradiction_clause,[status(thm)],[f326]) ).
fof(f339,plain,
! [X0,X1,X2] :
( not_subclass_element(unordered_pair(X1,X2),X0) = X2
| ~ member(not_subclass_element(X0,unordered_pair(X1,X2)),unordered_pair(X1,X2))
| X1 = not_subclass_element(unordered_pair(X1,X2),X0)
| X0 = unordered_pair(X1,X2) ),
inference(resolution,[status(thm)],[f226,f118]) ).
fof(f377,plain,
! [X0,X1,X2] :
( not_subclass_element(unordered_pair(X1,X2),singleton(X0)) = X1
| X0 = not_subclass_element(singleton(X0),unordered_pair(X1,X2))
| X2 = not_subclass_element(unordered_pair(X1,X2),singleton(X0))
| singleton(X0) = unordered_pair(X1,X2) ),
inference(resolution,[status(thm)],[f251,f249]) ).
fof(f378,plain,
! [X0,X1,X2,X3] :
( not_subclass_element(unordered_pair(X0,X1),unordered_pair(X2,X3)) = X1
| X0 = not_subclass_element(unordered_pair(X0,X1),unordered_pair(X2,X3))
| X3 = not_subclass_element(unordered_pair(X2,X3),unordered_pair(X0,X1))
| X2 = not_subclass_element(unordered_pair(X2,X3),unordered_pair(X0,X1))
| unordered_pair(X0,X1) = unordered_pair(X2,X3) ),
inference(resolution,[status(thm)],[f251,f118]) ).
fof(f411,plain,
! [X0] :
( ~ sQ5_spl
| X0 = not_subclass_element(universal_class,null_class)
| not_subclass_element(universal_class,null_class) = not_subclass_element(universal_class,null_class) ),
inference(resolution,[status(thm)],[f296,f118]) ).
fof(f413,definition,
( sQ6_spl
<=> not_subclass_element(universal_class,null_class) = not_subclass_element(universal_class,null_class) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f416,definition,
! [X0] :
( sQ7_spl
<=> X0 = not_subclass_element(universal_class,null_class) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f417,plain,
! [X0] :
( ~ sQ7_spl
| not_subclass_element(universal_class,null_class) = X0 ),
inference(component_clause,[status(thm)],[f416]) ).
fof(f419,plain,
( ~ sQ5_spl
| sQ7_spl
| sQ6_spl ),
inference(split_clause,[status(thm)],[f411,f413,f416,f295]) ).
fof(f441,plain,
! [X0,X1] :
( ordered_pair(X0,X1) = null_class
| unordered_pair(X0,singleton(X1)) = not_subclass_element(unordered_pair(singleton(X0),unordered_pair(X0,singleton(X1))),null_class)
| not_subclass_element(unordered_pair(singleton(X0),unordered_pair(X0,singleton(X1))),null_class) = singleton(X0) ),
inference(paramodulation,[status(thm)],[f125,f276]) ).
fof(f443,plain,
! [X0] :
( ~ sQ5_spl
| X0 = not_subclass_element(unordered_pair(not_subclass_element(universal_class,null_class),X0),null_class)
| not_subclass_element(unordered_pair(not_subclass_element(universal_class,null_class),X0),null_class) = not_subclass_element(universal_class,null_class)
| member(not_subclass_element(universal_class,null_class),null_class) ),
inference(paramodulation,[status(thm)],[f276,f296]) ).
fof(f457,plain,
! [X0,X1] :
( X1 = not_subclass_element(unordered_pair(X0,X1),null_class)
| not_subclass_element(unordered_pair(X0,X1),null_class) = X0
| member(null_class,universal_class) ),
inference(paramodulation,[status(thm)],[f276,f123]) ).
fof(f463,definition,
( sQ8_spl
<=> null_class = unordered_pair(x,y) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f464,plain,
( ~ sQ8_spl
| null_class = unordered_pair(x,y) ),
inference(component_clause,[status(thm)],[f463]) ).
fof(f465,plain,
( sQ8_spl
| unordered_pair(x,y) != null_class ),
inference(component_clause,[status(thm)],[f463]) ).
fof(f466,definition,
( sQ9_spl
<=> not_subclass_element(unordered_pair(y,x),null_class) = y ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f467,plain,
( ~ sQ9_spl
| not_subclass_element(unordered_pair(y,x),null_class) = y ),
inference(component_clause,[status(thm)],[f466]) ).
fof(f469,definition,
( sQ10_spl
<=> x = not_subclass_element(unordered_pair(y,x),null_class) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f470,plain,
( ~ sQ10_spl
| x = not_subclass_element(unordered_pair(y,x),null_class) ),
inference(component_clause,[status(thm)],[f469]) ).
fof(f471,plain,
( sQ10_spl
| not_subclass_element(unordered_pair(y,x),null_class) != x ),
inference(component_clause,[status(thm)],[f469]) ).
fof(f475,definition,
( sQ11_spl
<=> member(null_class,universal_class) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f478,definition,
! [X0,X1] :
( sQ12_spl
<=> ( X1 = not_subclass_element(unordered_pair(X0,X1),null_class)
| not_subclass_element(unordered_pair(X0,X1),null_class) = X0 ) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f481,plain,
( sQ12_spl
| sQ11_spl ),
inference(split_clause,[status(thm)],[f457,f475,f478]) ).
fof(f482,plain,
! [X0,X1] :
( ordered_pair(X0,X1) = null_class
| unordered_pair(X0,singleton(X1)) = not_subclass_element(unordered_pair(singleton(X0),unordered_pair(X0,singleton(X1))),null_class)
| not_subclass_element(ordered_pair(X0,X1),null_class) = singleton(X0) ),
inference(forward_demodulation,[status(thm)],[f125,f441]) ).
fof(f483,plain,
! [X0,X1] :
( null_class = ordered_pair(X0,X1)
| not_subclass_element(ordered_pair(X0,X1),null_class) = unordered_pair(X0,singleton(X1))
| not_subclass_element(ordered_pair(X0,X1),null_class) = singleton(X0) ),
inference(forward_demodulation,[status(thm)],[f125,f482]) ).
fof(f487,definition,
( sQ13_spl
<=> member(not_subclass_element(universal_class,null_class),null_class) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f488,plain,
( ~ sQ13_spl
| member(not_subclass_element(universal_class,null_class),null_class) ),
inference(component_clause,[status(thm)],[f487]) ).
fof(f490,definition,
! [X0] :
( sQ14_spl
<=> ( X0 = not_subclass_element(unordered_pair(not_subclass_element(universal_class,null_class),X0),null_class)
| not_subclass_element(unordered_pair(not_subclass_element(universal_class,null_class),X0),null_class) = not_subclass_element(universal_class,null_class) ) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f493,plain,
( ~ sQ5_spl
| sQ14_spl
| sQ13_spl ),
inference(split_clause,[status(thm)],[f443,f487,f490,f295]) ).
fof(f498,plain,
( ~ sQ13_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f488,f230]) ).
fof(f499,plain,
~ sQ13_spl,
inference(contradiction_clause,[status(thm)],[f498]) ).
fof(f504,definition,
( sQ15_spl
<=> null_class = unordered_pair(y,x) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f505,plain,
( ~ sQ15_spl
| unordered_pair(y,x) = null_class ),
inference(component_clause,[status(thm)],[f504]) ).
fof(f506,plain,
( sQ15_spl
| unordered_pair(y,x) != null_class ),
inference(component_clause,[status(thm)],[f504]) ).
fof(f510,definition,
( sQ17_spl
<=> member(x,null_class) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f511,plain,
( ~ sQ17_spl
| member(x,null_class) ),
inference(component_clause,[status(thm)],[f510]) ).
fof(f514,definition,
( sQ18_spl
<=> member(not_subclass_element(null_class,unordered_pair(y,x)),null_class) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f515,plain,
( ~ sQ18_spl
| member(not_subclass_element(null_class,unordered_pair(y,x)),null_class) ),
inference(component_clause,[status(thm)],[f514]) ).
fof(f517,definition,
( sQ19_spl
<=> member(x,unordered_pair(y,x)) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f518,plain,
( ~ sQ19_spl
| member(x,unordered_pair(y,x)) ),
inference(component_clause,[status(thm)],[f517]) ).
fof(f519,plain,
( sQ19_spl
| ~ member(x,unordered_pair(y,x)) ),
inference(component_clause,[status(thm)],[f517]) ).
fof(f524,plain,
( ~ sQ19_spl
| ~ sQ15_spl
| member(x,null_class) ),
inference(forward_demodulation,[status(thm)],[f505,f518]) ).
fof(f525,plain,
( ~ sQ19_spl
| ~ sQ15_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f524,f230]) ).
fof(f526,plain,
( ~ sQ19_spl
| ~ sQ15_spl ),
inference(contradiction_clause,[status(thm)],[f525]) ).
fof(f527,plain,
( ~ sQ18_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f515,f230]) ).
fof(f528,plain,
~ sQ18_spl,
inference(contradiction_clause,[status(thm)],[f527]) ).
fof(f594,plain,
( sQ8_spl
| y = not_subclass_element(unordered_pair(x,y),null_class)
| x = not_subclass_element(unordered_pair(x,y),null_class) ),
inference(resolution,[status(thm)],[f276,f465]) ).
fof(f595,plain,
( sQ15_spl
| x = not_subclass_element(unordered_pair(y,x),null_class)
| y = not_subclass_element(unordered_pair(y,x),null_class) ),
inference(resolution,[status(thm)],[f276,f506]) ).
fof(f607,plain,
! [X0] :
( ~ sQ2_spl
| not_subclass_element(universal_class,null_class) = not_subclass_element(unordered_pair(X0,not_subclass_element(universal_class,null_class)),null_class)
| X0 = not_subclass_element(unordered_pair(X0,not_subclass_element(universal_class,null_class)),null_class)
| member(not_subclass_element(universal_class,null_class),null_class) ),
inference(paramodulation,[status(thm)],[f276,f285]) ).
fof(f626,definition,
! [X0] :
( sQ24_spl
<=> ( not_subclass_element(universal_class,null_class) = not_subclass_element(unordered_pair(X0,not_subclass_element(universal_class,null_class)),null_class)
| X0 = not_subclass_element(unordered_pair(X0,not_subclass_element(universal_class,null_class)),null_class) ) ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f629,plain,
( ~ sQ2_spl
| sQ24_spl
| sQ13_spl ),
inference(split_clause,[status(thm)],[f607,f487,f626,f284]) ).
fof(f631,plain,
( sQ15_spl
| sQ10_spl
| sQ9_spl ),
inference(split_clause,[status(thm)],[f595,f466,f469,f504]) ).
fof(f636,definition,
( sQ25_spl
<=> x = not_subclass_element(unordered_pair(x,y),null_class) ),
introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition]) ).
fof(f637,plain,
( ~ sQ25_spl
| x = not_subclass_element(unordered_pair(x,y),null_class) ),
inference(component_clause,[status(thm)],[f636]) ).
fof(f638,plain,
( sQ25_spl
| not_subclass_element(unordered_pair(x,y),null_class) != x ),
inference(component_clause,[status(thm)],[f636]) ).
fof(f639,definition,
( sQ26_spl
<=> y = not_subclass_element(unordered_pair(x,y),null_class) ),
introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition]) ).
fof(f640,plain,
( ~ sQ26_spl
| not_subclass_element(unordered_pair(x,y),null_class) = y ),
inference(component_clause,[status(thm)],[f639]) ).
fof(f641,plain,
( sQ26_spl
| y != not_subclass_element(unordered_pair(x,y),null_class) ),
inference(component_clause,[status(thm)],[f639]) ).
fof(f653,plain,
( sQ8_spl
| sQ26_spl
| sQ25_spl ),
inference(split_clause,[status(thm)],[f594,f636,f639,f463]) ).
fof(f655,plain,
( ~ sQ26_spl
| ~ sQ25_spl
| unordered_pair(y,x) != unordered_pair(x,x) ),
inference(backward_demodulation,[status(thm)],[f658,f235]) ).
fof(f658,plain,
( ~ sQ26_spl
| ~ sQ25_spl
| y = x ),
inference(forward_demodulation,[status(thm)],[f637,f640]) ).
fof(f668,plain,
( ~ sQ26_spl
| ~ sQ25_spl
| unordered_pair(x,x) != unordered_pair(x,x) ),
inference(forward_demodulation,[status(thm)],[f658,f655]) ).
fof(f669,plain,
( ~ sQ26_spl
| ~ sQ25_spl
| singleton(x) != unordered_pair(x,x) ),
inference(forward_demodulation,[status(thm)],[f124,f668]) ).
fof(f670,plain,
( ~ sQ26_spl
| ~ sQ25_spl
| singleton(x) != singleton(x) ),
inference(forward_demodulation,[status(thm)],[f124,f669]) ).
fof(f671,plain,
( ~ sQ26_spl
| ~ sQ25_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f670]) ).
fof(f672,plain,
( ~ sQ26_spl
| ~ sQ25_spl ),
inference(contradiction_clause,[status(thm)],[f671]) ).
fof(f678,plain,
( sQ10_spl
| ~ sQ9_spl
| x != y ),
inference(forward_demodulation,[status(thm)],[f467,f471]) ).
fof(f686,definition,
( sQ29_spl
<=> member(y,unordered_pair(x,y)) ),
introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition]) ).
fof(f687,plain,
( ~ sQ29_spl
| member(y,unordered_pair(x,y)) ),
inference(component_clause,[status(thm)],[f686]) ).
fof(f688,plain,
( sQ29_spl
| ~ member(y,unordered_pair(x,y)) ),
inference(component_clause,[status(thm)],[f686]) ).
fof(f690,definition,
( sQ30_spl
<=> member(y,null_class) ),
introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition]) ).
fof(f691,plain,
( ~ sQ30_spl
| member(y,null_class) ),
inference(component_clause,[status(thm)],[f690]) ).
fof(f698,definition,
( sQ32_spl
<=> member(not_subclass_element(null_class,unordered_pair(x,y)),null_class) ),
introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition]) ).
fof(f699,plain,
( ~ sQ32_spl
| member(not_subclass_element(null_class,unordered_pair(x,y)),null_class) ),
inference(component_clause,[status(thm)],[f698]) ).
fof(f703,plain,
( ~ sQ8_spl
| unordered_pair(y,x) != null_class ),
inference(backward_demodulation,[status(thm)],[f464,f235]) ).
fof(f752,definition,
( sQ33_spl
<=> member(y,unordered_pair(y,x)) ),
introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition]) ).
fof(f753,plain,
( ~ sQ33_spl
| member(y,unordered_pair(y,x)) ),
inference(component_clause,[status(thm)],[f752]) ).
fof(f754,plain,
( sQ33_spl
| ~ member(y,unordered_pair(y,x)) ),
inference(component_clause,[status(thm)],[f752]) ).
fof(f758,plain,
( ~ sQ8_spl
| ~ sQ15_spl ),
inference(split_clause,[status(thm)],[f703,f504,f463]) ).
fof(f789,plain,
( ~ sQ33_spl
| x = y
| y = y ),
inference(resolution,[status(thm)],[f753,f118]) ).
fof(f791,definition,
( sQ34_spl
<=> y = y ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f794,definition,
( sQ35_spl
<=> x = y ),
introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition]) ).
fof(f795,plain,
( ~ sQ35_spl
| y = x ),
inference(component_clause,[status(thm)],[f794]) ).
fof(f796,plain,
( sQ35_spl
| x != y ),
inference(component_clause,[status(thm)],[f794]) ).
fof(f797,plain,
( ~ sQ33_spl
| sQ35_spl
| sQ34_spl ),
inference(split_clause,[status(thm)],[f789,f791,f794,f752]) ).
fof(f816,definition,
! [X0] :
( sQ37_spl
<=> X0 = null_class ),
introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition]) ).
fof(f817,plain,
! [X0] :
( ~ sQ37_spl
| null_class = X0 ),
inference(component_clause,[status(thm)],[f816]) ).
fof(f820,definition,
( sQ38_spl
<=> member(null_class,null_class) ),
introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition]) ).
fof(f821,plain,
( ~ sQ38_spl
| member(null_class,null_class) ),
inference(component_clause,[status(thm)],[f820]) ).
fof(f823,definition,
! [X0] :
( sQ39_spl
<=> ( X0 = not_subclass_element(unordered_pair(null_class,X0),null_class)
| null_class = not_subclass_element(unordered_pair(null_class,X0),null_class) ) ),
introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition]) ).
fof(f824,plain,
! [X0] :
( ~ sQ39_spl
| not_subclass_element(unordered_pair(null_class,X0),null_class) = X0
| null_class = not_subclass_element(unordered_pair(null_class,X0),null_class) ),
inference(component_clause,[status(thm)],[f823]) ).
fof(f827,plain,
( sQ0_spl
| ~ sQ37_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f279,f817]) ).
fof(f830,plain,
( ~ sQ38_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f821,f230]) ).
fof(f831,plain,
~ sQ38_spl,
inference(contradiction_clause,[status(thm)],[f830]) ).
fof(f832,plain,
( sQ0_spl
| ~ sQ37_spl ),
inference(contradiction_clause,[status(thm)],[f827]) ).
fof(f843,plain,
! [X0,X1] :
( member(ordered_pair(X0,X1),element_relation)
| ~ member(X0,X1)
| ~ member(X1,universal_class)
| ~ member(X0,universal_class) ),
inference(resolution,[status(thm)],[f130,f135]) ).
fof(f844,plain,
! [X0,X1,X2,X3] :
( member(X2,X3)
| ~ member(X2,X3)
| ~ member(X0,X1) ),
inference(resolution,[status(thm)],[f130,f129]) ).
fof(f847,plain,
! [X0,X1,X2,X3] :
( member(X2,unordered_pair(X0,X2))
| ~ member(X2,X3)
| ~ member(X0,X1) ),
inference(resolution,[status(thm)],[f130,f217]) ).
fof(f849,definition,
! [X0,X1] :
( sQ40_spl
<=> ~ member(X0,X1) ),
introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition]) ).
fof(f850,plain,
! [X0,X1] :
( ~ sQ40_spl
| ~ member(X0,X1) ),
inference(component_clause,[status(thm)],[f849]) ).
fof(f852,definition,
! [X2,X3] :
( sQ41_spl
<=> ( member(X2,X3)
| ~ member(X2,X3) ) ),
introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition]) ).
fof(f855,plain,
( sQ41_spl
| sQ40_spl ),
inference(split_clause,[status(thm)],[f844,f849,f852]) ).
fof(f897,plain,
( ~ sQ40_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f265,f850]) ).
fof(f921,plain,
~ sQ40_spl,
inference(contradiction_clause,[status(thm)],[f897]) ).
fof(f925,plain,
! [X0,X1] :
( ~ subclass(X0,null_class)
| subclass(X0,X1) ),
inference(resolution,[status(thm)],[f224,f231]) ).
fof(f928,plain,
( ~ inductive(omega)
| subclass(omega,omega) ),
inference(resolution,[status(thm)],[f224,f168]) ).
fof(f944,definition,
( sQ42_spl
<=> subclass(omega,omega) ),
introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition]) ).
fof(f947,definition,
( sQ43_spl
<=> inductive(omega) ),
introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition]) ).
fof(f949,plain,
( sQ43_spl
| ~ inductive(omega) ),
inference(component_clause,[status(thm)],[f947]) ).
fof(f950,plain,
( ~ sQ43_spl
| sQ42_spl ),
inference(split_clause,[status(thm)],[f928,f944,f947]) ).
fof(f1000,plain,
( ~ sQ29_spl
| y = x
| y = y ),
inference(resolution,[status(thm)],[f118,f687]) ).
fof(f1004,plain,
( ~ sQ29_spl
| sQ35_spl
| sQ34_spl ),
inference(split_clause,[status(thm)],[f1000,f791,f794,f686]) ).
fof(f1007,plain,
( ~ sQ32_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f699,f230]) ).
fof(f1008,plain,
~ sQ32_spl,
inference(contradiction_clause,[status(thm)],[f1007]) ).
fof(f1009,plain,
( ~ sQ35_spl
| sQ10_spl
| ~ sQ9_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f795,f678]) ).
fof(f1010,plain,
( ~ sQ35_spl
| sQ10_spl
| ~ sQ9_spl ),
inference(contradiction_clause,[status(thm)],[f1009]) ).
fof(f1018,definition,
( sQ46_spl
<=> not_subclass_element(unordered_pair(null_class,null_class),null_class) = null_class ),
introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition]) ).
fof(f1019,plain,
( ~ sQ46_spl
| not_subclass_element(unordered_pair(null_class,null_class),null_class) = null_class ),
inference(component_clause,[status(thm)],[f1018]) ).
fof(f1020,plain,
( sQ46_spl
| not_subclass_element(unordered_pair(null_class,null_class),null_class) != null_class ),
inference(component_clause,[status(thm)],[f1018]) ).
fof(f1021,definition,
( sQ47_spl
<=> null_class = not_subclass_element(singleton(null_class),null_class) ),
introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition]) ).
fof(f1059,plain,
! [X0] : member(omega,unordered_pair(omega,X0)),
inference(resolution,[status(thm)],[f169,f120]) ).
fof(f1060,plain,
! [X0] : member(omega,unordered_pair(X0,omega)),
inference(resolution,[status(thm)],[f169,f122]) ).
fof(f1073,plain,
! [X0] : member(null_class,unordered_pair(null_class,X0)),
inference(resolution,[status(thm)],[f234,f120]) ).
fof(f1074,plain,
! [X0] : member(null_class,unordered_pair(X0,null_class)),
inference(resolution,[status(thm)],[f234,f122]) ).
fof(f1105,plain,
! [X0,X1] :
( ~ sQ7_spl
| X0 = X1 ),
inference(paramodulation,[status(thm)],[f417,f417]) ).
fof(f1110,definition,
( sQ50_spl
<=> member(not_subclass_element(null_class,universal_class),null_class) ),
introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition]) ).
fof(f1111,plain,
( ~ sQ50_spl
| member(not_subclass_element(null_class,universal_class),null_class) ),
inference(component_clause,[status(thm)],[f1110]) ).
fof(f1118,plain,
( sQ0_spl
| ~ sQ7_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f279,f1105]) ).
fof(f1130,plain,
( sQ0_spl
| ~ sQ7_spl ),
inference(contradiction_clause,[status(thm)],[f1118]) ).
fof(f1132,plain,
( ~ sQ50_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1111,f230]) ).
fof(f1133,plain,
~ sQ50_spl,
inference(contradiction_clause,[status(thm)],[f1132]) ).
fof(f1160,definition,
( sQ52_spl
<=> inductive(universal_class) ),
introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition]) ).
fof(f1163,definition,
( sQ53_spl
<=> subclass(image(successor_relation,universal_class),universal_class) ),
introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition]) ).
fof(f1165,plain,
( sQ53_spl
| ~ subclass(image(successor_relation,universal_class),universal_class) ),
inference(component_clause,[status(thm)],[f1163]) ).
fof(f1167,plain,
( sQ53_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1165,f113]) ).
fof(f1168,plain,
sQ53_spl,
inference(contradiction_clause,[status(thm)],[f1167]) ).
fof(f1188,plain,
~ inductive(null_class),
inference(resolution,[status(thm)],[f164,f230]) ).
fof(f1189,plain,
! [X0] :
( member(null_class,unordered_pair(null_class,X0))
| ~ inductive(universal_class) ),
inference(resolution,[status(thm)],[f164,f120]) ).
fof(f1190,plain,
! [X0] :
( member(null_class,unordered_pair(X0,null_class))
| ~ inductive(universal_class) ),
inference(resolution,[status(thm)],[f164,f122]) ).
fof(f1191,definition,
! [X0] :
( sQ54_spl
<=> member(null_class,unordered_pair(X0,null_class)) ),
introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition]) ).
fof(f1194,plain,
( sQ54_spl
| ~ sQ52_spl ),
inference(split_clause,[status(thm)],[f1190,f1160,f1191]) ).
fof(f1195,definition,
! [X0] :
( sQ55_spl
<=> member(null_class,unordered_pair(null_class,X0)) ),
introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition]) ).
fof(f1198,plain,
( sQ55_spl
| ~ sQ52_spl ),
inference(split_clause,[status(thm)],[f1189,f1160,f1195]) ).
fof(f1207,plain,
! [X0,X1,X2] :
( ~ subclass(image(successor_relation,unordered_pair(X0,null_class)),unordered_pair(X0,null_class))
| inductive(unordered_pair(X0,null_class))
| ~ member(null_class,X2)
| ~ member(X0,X1) ),
inference(resolution,[status(thm)],[f847,f166]) ).
fof(f1211,definition,
! [X0,X1] :
( sQ56_spl
<=> ( ~ subclass(image(successor_relation,unordered_pair(X0,null_class)),unordered_pair(X0,null_class))
| inductive(unordered_pair(X0,null_class))
| ~ member(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition]) ).
fof(f1214,definition,
! [X2] :
( sQ57_spl
<=> ~ member(null_class,X2) ),
introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition]) ).
fof(f1215,plain,
! [X0] :
( ~ sQ57_spl
| ~ member(null_class,X0) ),
inference(component_clause,[status(thm)],[f1214]) ).
fof(f1217,plain,
( sQ57_spl
| sQ56_spl ),
inference(split_clause,[status(thm)],[f1207,f1211,f1214]) ).
fof(f1218,plain,
( ~ sQ57_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f234,f1215]) ).
fof(f1226,plain,
~ sQ57_spl,
inference(contradiction_clause,[status(thm)],[f1218]) ).
fof(f1235,definition,
( sQ58_spl
<=> subclass(unordered_pair(null_class,null_class),null_class) ),
introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition]) ).
fof(f1236,plain,
( ~ sQ58_spl
| subclass(unordered_pair(null_class,null_class),null_class) ),
inference(component_clause,[status(thm)],[f1235]) ).
fof(f1239,definition,
( sQ59_spl
<=> subclass(singleton(null_class),null_class) ),
introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition]) ).
fof(f1240,plain,
( ~ sQ59_spl
| subclass(singleton(null_class),null_class) ),
inference(component_clause,[status(thm)],[f1239]) ).
fof(f1241,plain,
( sQ59_spl
| ~ subclass(singleton(null_class),null_class) ),
inference(component_clause,[status(thm)],[f1239]) ).
fof(f1243,definition,
( sQ60_spl
<=> subclass(unordered_pair(x,y),null_class) ),
introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition]) ).
fof(f1244,plain,
( ~ sQ60_spl
| subclass(unordered_pair(x,y),null_class) ),
inference(component_clause,[status(thm)],[f1243]) ).
fof(f1247,definition,
! [X0] :
( sQ61_spl
<=> ( X0 = not_subclass_element(unordered_pair(null_class,X0),null_class)
| subclass(unordered_pair(null_class,X0),null_class) ) ),
introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition]) ).
fof(f1248,plain,
! [X0] :
( ~ sQ61_spl
| subclass(unordered_pair(null_class,X0),null_class)
| not_subclass_element(unordered_pair(null_class,X0),null_class) = X0 ),
inference(component_clause,[status(thm)],[f1247]) ).
fof(f1251,definition,
( sQ62_spl
<=> subclass(unordered_pair(y,x),null_class) ),
introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition]) ).
fof(f1252,plain,
( ~ sQ62_spl
| subclass(unordered_pair(y,x),null_class) ),
inference(component_clause,[status(thm)],[f1251]) ).
fof(f1255,plain,
( ~ sQ58_spl
| subclass(singleton(null_class),null_class) ),
inference(forward_demodulation,[status(thm)],[f124,f1236]) ).
fof(f1258,plain,
! [X0] :
( ~ sQ62_spl
| ~ subclass(null_class,X0)
| subclass(unordered_pair(y,x),X0) ),
inference(resolution,[status(thm)],[f1252,f224]) ).
fof(f1260,plain,
! [X0] :
( ~ sQ62_spl
| subclass(unordered_pair(y,x),X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1258,f231]) ).
fof(f1264,plain,
! [X0,X1] :
( ~ sQ62_spl
| ~ subclass(X0,unordered_pair(y,x))
| subclass(X0,X1) ),
inference(resolution,[status(thm)],[f1260,f224]) ).
fof(f1265,plain,
! [X0] :
( ~ sQ60_spl
| ~ subclass(null_class,X0)
| subclass(unordered_pair(x,y),X0) ),
inference(resolution,[status(thm)],[f1244,f224]) ).
fof(f1267,plain,
! [X0] :
( ~ sQ60_spl
| subclass(unordered_pair(x,y),X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1265,f231]) ).
fof(f1275,plain,
! [X0] :
( ~ sQ62_spl
| ~ inductive(unordered_pair(y,x))
| subclass(omega,X0) ),
inference(resolution,[status(thm)],[f1264,f168]) ).
fof(f1277,definition,
! [X0] :
( sQ63_spl
<=> subclass(omega,X0) ),
introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition]) ).
fof(f1278,plain,
! [X0] :
( ~ sQ63_spl
| subclass(omega,X0) ),
inference(component_clause,[status(thm)],[f1277]) ).
fof(f1280,definition,
( sQ64_spl
<=> inductive(unordered_pair(y,x)) ),
introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition]) ).
fof(f1283,plain,
( ~ sQ62_spl
| ~ sQ64_spl
| sQ63_spl ),
inference(split_clause,[status(thm)],[f1275,f1277,f1280,f1251]) ).
fof(f1284,plain,
! [X0] :
( omega = X0
| omega = omega ),
inference(resolution,[status(thm)],[f1059,f118]) ).
fof(f1286,definition,
( sQ65_spl
<=> omega = omega ),
introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition]) ).
fof(f1289,definition,
! [X0] :
( sQ66_spl
<=> omega = X0 ),
introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition]) ).
fof(f1290,plain,
! [X0] :
( ~ sQ66_spl
| X0 = omega ),
inference(component_clause,[status(thm)],[f1289]) ).
fof(f1292,plain,
( sQ66_spl
| sQ65_spl ),
inference(split_clause,[status(thm)],[f1284,f1286,f1289]) ).
fof(f1295,plain,
( ~ sQ61_spl
| subclass(singleton(null_class),null_class)
| not_subclass_element(unordered_pair(null_class,null_class),null_class) = null_class ),
inference(paramodulation,[status(thm)],[f124,f1248]) ).
fof(f1296,plain,
( ~ sQ61_spl
| sQ59_spl
| sQ46_spl ),
inference(split_clause,[status(thm)],[f1295,f1018,f1239,f1247]) ).
fof(f1304,plain,
! [X0,X1] :
( ~ sQ66_spl
| X0 = X1 ),
inference(paramodulation,[status(thm)],[f1290,f1290]) ).
fof(f1311,plain,
( ~ sQ66_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f235,f1304]) ).
fof(f1322,plain,
~ sQ66_spl,
inference(contradiction_clause,[status(thm)],[f1311]) ).
fof(f1367,plain,
! [X0,X1,X2] :
( member(ordered_pair(X0,X1),complement(X2))
| member(ordered_pair(X0,X1),X2) ),
inference(resolution,[status(thm)],[f142,f243]) ).
fof(f1377,plain,
! [X0,X1,X2] :
( not_subclass_element(unordered_pair(X0,X1),X2) = X1
| subclass(unordered_pair(X0,X1),X2)
| X0 = not_subclass_element(unordered_pair(X0,X1),X2) ),
inference(resolution,[status(thm)],[f111,f118]) ).
fof(f1385,plain,
( ~ sQ26_spl
| subclass(unordered_pair(x,y),null_class)
| member(y,unordered_pair(x,y)) ),
inference(paramodulation,[status(thm)],[f640,f111]) ).
fof(f1388,plain,
( ~ sQ26_spl
| sQ60_spl
| sQ29_spl ),
inference(split_clause,[status(thm)],[f1385,f686,f1243,f639]) ).
fof(f1390,plain,
( sQ26_spl
| ~ sQ25_spl
| y != x ),
inference(backward_demodulation,[status(thm)],[f637,f641]) ).
fof(f1391,plain,
( ~ sQ25_spl
| subclass(unordered_pair(x,y),null_class)
| member(x,unordered_pair(x,y)) ),
inference(paramodulation,[status(thm)],[f637,f111]) ).
fof(f1393,definition,
( sQ67_spl
<=> member(x,unordered_pair(x,y)) ),
introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition]) ).
fof(f1394,plain,
( ~ sQ67_spl
| member(x,unordered_pair(x,y)) ),
inference(component_clause,[status(thm)],[f1393]) ).
fof(f1395,plain,
( sQ67_spl
| ~ member(x,unordered_pair(x,y)) ),
inference(component_clause,[status(thm)],[f1393]) ).
fof(f1396,plain,
( ~ sQ25_spl
| sQ60_spl
| sQ67_spl ),
inference(split_clause,[status(thm)],[f1391,f1393,f1243,f636]) ).
fof(f1398,plain,
( ~ sQ67_spl
| x = x
| y = x ),
inference(resolution,[status(thm)],[f1394,f118]) ).
fof(f1399,definition,
( sQ68_spl
<=> x = x ),
introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition]) ).
fof(f1402,plain,
( ~ sQ67_spl
| sQ68_spl
| sQ35_spl ),
inference(split_clause,[status(thm)],[f1398,f794,f1399,f1393]) ).
fof(f1406,plain,
! [X0,X1,X2,X3] :
( member(X2,universal_class)
| ~ member(X2,X3)
| ~ member(X0,X1) ),
inference(resolution,[status(thm)],[f130,f219]) ).
fof(f1411,definition,
! [X2,X3] :
( sQ69_spl
<=> ( member(X2,universal_class)
| ~ member(X2,X3) ) ),
introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition]) ).
fof(f1412,plain,
! [X0,X1] :
( ~ sQ69_spl
| member(X0,universal_class)
| ~ member(X0,X1) ),
inference(component_clause,[status(thm)],[f1411]) ).
fof(f1414,plain,
( sQ69_spl
| sQ40_spl ),
inference(split_clause,[status(thm)],[f1406,f849,f1411]) ).
fof(f1416,plain,
! [X0,X1] :
( ~ sQ69_spl
| member(ordered_pair(X1,X0),element_relation)
| ~ member(X1,X0)
| ~ member(X0,universal_class) ),
inference(backward_subsumption_resolution,[status(thm)],[f843,f1412]) ).
fof(f1437,plain,
! [X0,X1,X2,X3,X4] :
( ~ member(ordered_pair(X1,X0),X2)
| ~ subclass(X2,cross_product(X3,X4))
| member(X0,unordered_pair(X1,X0)) ),
inference(resolution,[status(thm)],[f110,f217]) ).
fof(f1438,plain,
! [X0,X1,X2,X3,X4] :
( member(X3,unordered_pair(X3,X4))
| ~ member(ordered_pair(X3,X4),X0)
| ~ subclass(X0,cross_product(X1,X2)) ),
inference(resolution,[status(thm)],[f110,f215]) ).
fof(f1445,plain,
! [X0,X1,X2] :
( member(X0,unordered_pair(X0,X2))
| ~ subclass(X1,universal_class)
| ~ member(X0,X1) ),
inference(resolution,[status(thm)],[f110,f120]) ).
fof(f1446,plain,
! [X0,X1,X2] :
( member(X0,unordered_pair(X2,X0))
| ~ subclass(X1,universal_class)
| ~ member(X0,X1) ),
inference(resolution,[status(thm)],[f110,f122]) ).
fof(f1447,plain,
! [X0,X1,X2] :
( member(X0,unordered_pair(X2,X0))
| ~ member(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f1446,f113]) ).
fof(f1448,plain,
! [X0,X1,X2] :
( member(X0,unordered_pair(X0,X2))
| ~ member(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f1445,f113]) ).
fof(f1457,plain,
! [X0] :
( ~ sQ39_spl
| not_subclass_element(unordered_pair(null_class,X0),null_class) = X0
| null_class != X0 ),
inference(equality_factoring,[status(thm)],[f824]) ).
fof(f1459,plain,
( ~ sQ39_spl
| not_subclass_element(unordered_pair(null_class,null_class),null_class) = null_class ),
inference(destructive_equality_resolution,[status(thm)],[f1457]) ).
fof(f1468,plain,
! [X0] :
( null_class = X0
| null_class = null_class ),
inference(resolution,[status(thm)],[f1074,f118]) ).
fof(f1469,plain,
member(null_class,singleton(null_class)),
inference(paramodulation,[status(thm)],[f124,f1074]) ).
fof(f1470,plain,
( sQ37_spl
| sQ3_spl ),
inference(split_clause,[status(thm)],[f1468,f288,f816]) ).
fof(f1502,definition,
( sQ71_spl
<=> subclass(null_class,unordered_pair(x,y)) ),
introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition]) ).
fof(f1504,plain,
( sQ71_spl
| ~ subclass(null_class,unordered_pair(x,y)) ),
inference(component_clause,[status(thm)],[f1502]) ).
fof(f1514,plain,
( ~ sQ39_spl
| subclass(unordered_pair(null_class,null_class),null_class)
| member(null_class,unordered_pair(null_class,null_class)) ),
inference(paramodulation,[status(thm)],[f1459,f111]) ).
fof(f1518,definition,
( sQ72_spl
<=> member(null_class,unordered_pair(null_class,null_class)) ),
introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition]) ).
fof(f1521,plain,
( ~ sQ39_spl
| sQ58_spl
| sQ72_spl ),
inference(split_clause,[status(thm)],[f1514,f1518,f1235,f823]) ).
fof(f1576,plain,
( ~ sQ10_spl
| ~ sQ9_spl
| x = y ),
inference(forward_demodulation,[status(thm)],[f467,f470]) ).
fof(f1588,plain,
( sQ26_spl
| ~ sQ25_spl
| ~ sQ35_spl ),
inference(split_clause,[status(thm)],[f1390,f794,f636,f639]) ).
fof(f1593,plain,
( sQ25_spl
| ~ sQ26_spl
| x != y ),
inference(forward_demodulation,[status(thm)],[f640,f638]) ).
fof(f1661,plain,
( sQ25_spl
| ~ sQ26_spl
| ~ sQ35_spl ),
inference(split_clause,[status(thm)],[f1593,f794,f639,f636]) ).
fof(f1666,plain,
( sQ71_spl
| ~ sQ35_spl
| ~ subclass(null_class,unordered_pair(x,x)) ),
inference(forward_demodulation,[status(thm)],[f795,f1504]) ).
fof(f1667,plain,
( sQ71_spl
| ~ sQ35_spl
| ~ subclass(null_class,singleton(x)) ),
inference(forward_demodulation,[status(thm)],[f124,f1666]) ).
fof(f1668,plain,
( sQ71_spl
| ~ sQ35_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1667,f231]) ).
fof(f1669,plain,
( sQ71_spl
| ~ sQ35_spl ),
inference(contradiction_clause,[status(thm)],[f1668]) ).
fof(f1749,plain,
! [X0] :
( ~ sQ59_spl
| member(X0,null_class)
| ~ member(X0,singleton(null_class)) ),
inference(resolution,[status(thm)],[f1240,f110]) ).
fof(f1752,plain,
( ~ sQ59_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f1469,f1753]) ).
fof(f1753,plain,
! [X0] :
( ~ sQ59_spl
| ~ member(X0,singleton(null_class)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1749,f230]) ).
fof(f1755,plain,
~ sQ59_spl,
inference(contradiction_clause,[status(thm)],[f1752]) ).
fof(f1756,plain,
( ~ sQ58_spl
| sQ59_spl ),
inference(split_clause,[status(thm)],[f1255,f1239,f1235]) ).
fof(f1758,plain,
( ~ sQ46_spl
| not_subclass_element(singleton(null_class),null_class) = null_class ),
inference(forward_demodulation,[status(thm)],[f124,f1019]) ).
fof(f1786,plain,
( ~ sQ46_spl
| subclass(singleton(null_class),null_class)
| member(null_class,singleton(null_class)) ),
inference(paramodulation,[status(thm)],[f1758,f111]) ).
fof(f1788,definition,
( sQ77_spl
<=> member(null_class,singleton(null_class)) ),
introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition]) ).
fof(f1791,plain,
( ~ sQ46_spl
| sQ59_spl
| sQ77_spl ),
inference(split_clause,[status(thm)],[f1786,f1788,f1239,f1018]) ).
fof(f1800,plain,
( ~ sQ63_spl
| null_class = omega ),
inference(resolution,[status(thm)],[f232,f1278]) ).
fof(f1808,plain,
( ~ sQ63_spl
| inductive(null_class) ),
inference(backward_demodulation,[status(thm)],[f1800,f167]) ).
fof(f1817,plain,
( ~ sQ63_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1808,f1188]) ).
fof(f1818,plain,
~ sQ63_spl,
inference(contradiction_clause,[status(thm)],[f1817]) ).
fof(f1832,definition,
( sQ79_spl
<=> singleton(null_class) = null_class ),
introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition]) ).
fof(f1833,plain,
( ~ sQ79_spl
| singleton(null_class) = null_class ),
inference(component_clause,[status(thm)],[f1832]) ).
fof(f1834,plain,
( sQ79_spl
| null_class != singleton(null_class) ),
inference(component_clause,[status(thm)],[f1832]) ).
fof(f1837,plain,
( sQ59_spl
| ~ sQ79_spl
| ~ subclass(null_class,null_class) ),
inference(backward_demodulation,[status(thm)],[f1833,f1241]) ).
fof(f1947,plain,
! [X0] :
( ~ inductive(universal_class)
| member(null_class,domain_of(X0))
| restrict(X0,singleton(null_class),universal_class) = null_class ),
inference(resolution,[status(thm)],[f148,f164]) ).
fof(f1957,definition,
! [X0] :
( sQ82_spl
<=> ( member(null_class,domain_of(X0))
| restrict(X0,singleton(null_class),universal_class) = null_class ) ),
introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition]) ).
fof(f1960,plain,
( ~ sQ52_spl
| sQ82_spl ),
inference(split_clause,[status(thm)],[f1947,f1957,f1160]) ).
fof(f1989,plain,
( ~ sQ9_spl
| member(y,unordered_pair(y,x))
| unordered_pair(y,x) = null_class ),
inference(paramodulation,[status(thm)],[f467,f233]) ).
fof(f1995,plain,
( ~ sQ9_spl
| sQ33_spl
| sQ15_spl ),
inference(split_clause,[status(thm)],[f1989,f504,f752,f466]) ).
fof(f2018,plain,
! [X0,X1,X2] :
( X1 = not_subclass_element(unordered_pair(X0,X1),X2)
| X0 = not_subclass_element(unordered_pair(X0,X1),X2)
| ~ subclass(X2,unordered_pair(X0,X1))
| unordered_pair(X0,X1) = X2 ),
inference(resolution,[status(thm)],[f1377,f116]) ).
fof(f2050,plain,
! [X0,X1,X2,X3] :
( ~ subclass(universal_class,cross_product(X2,X3))
| member(X0,unordered_pair(X1,X0)) ),
inference(resolution,[status(thm)],[f1437,f243]) ).
fof(f2055,definition,
! [X0,X1] :
( sQ84_spl
<=> member(X0,unordered_pair(X1,X0)) ),
introduced(definition,[new_symbols(definition,[sQ84_spl])],[split_symbol_definition]) ).
fof(f2056,plain,
! [X0,X1] :
( ~ sQ84_spl
| member(X0,unordered_pair(X1,X0)) ),
inference(component_clause,[status(thm)],[f2055]) ).
fof(f2058,definition,
! [X2,X3] :
( sQ85_spl
<=> ~ subclass(universal_class,cross_product(X2,X3)) ),
introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition]) ).
fof(f2061,plain,
( sQ85_spl
| sQ84_spl ),
inference(split_clause,[status(thm)],[f2050,f2055,f2058]) ).
fof(f2071,plain,
( member(apply(choice,omega),omega)
| omega = null_class ),
inference(resolution,[status(thm)],[f187,f169]) ).
fof(f2082,plain,
! [X0,X1] :
( member(apply(choice,unordered_pair(X0,X1)),unordered_pair(X0,X1))
| unordered_pair(X0,X1) = null_class ),
inference(resolution,[status(thm)],[f187,f123]) ).
fof(f2084,definition,
( sQ86_spl
<=> member(apply(choice,null_class),null_class) ),
introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition]) ).
fof(f2085,plain,
( ~ sQ86_spl
| member(apply(choice,null_class),null_class) ),
inference(component_clause,[status(thm)],[f2084]) ).
fof(f2097,definition,
( sQ89_spl
<=> omega = null_class ),
introduced(definition,[new_symbols(definition,[sQ89_spl])],[split_symbol_definition]) ).
fof(f2098,plain,
( ~ sQ89_spl
| null_class = omega ),
inference(component_clause,[status(thm)],[f2097]) ).
fof(f2100,definition,
( sQ90_spl
<=> member(apply(choice,omega),omega) ),
introduced(definition,[new_symbols(definition,[sQ90_spl])],[split_symbol_definition]) ).
fof(f2103,plain,
( sQ90_spl
| sQ89_spl ),
inference(split_clause,[status(thm)],[f2071,f2097,f2100]) ).
fof(f2111,plain,
( ~ sQ89_spl
| inductive(null_class) ),
inference(backward_demodulation,[status(thm)],[f2098,f167]) ).
fof(f2121,plain,
( ~ sQ89_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2111,f1188]) ).
fof(f2122,plain,
~ sQ89_spl,
inference(contradiction_clause,[status(thm)],[f2121]) ).
fof(f2131,plain,
( ~ sQ86_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2085,f230]) ).
fof(f2132,plain,
~ sQ86_spl,
inference(contradiction_clause,[status(thm)],[f2131]) ).
fof(f2140,plain,
! [X0,X1,X2,X3] :
( ~ subclass(universal_class,cross_product(X2,X3))
| member(X0,unordered_pair(X0,X1)) ),
inference(resolution,[status(thm)],[f1438,f243]) ).
fof(f2145,definition,
! [X0,X1] :
( sQ91_spl
<=> member(X0,unordered_pair(X0,X1)) ),
introduced(definition,[new_symbols(definition,[sQ91_spl])],[split_symbol_definition]) ).
fof(f2146,plain,
! [X0,X1] :
( ~ sQ91_spl
| member(X0,unordered_pair(X0,X1)) ),
inference(component_clause,[status(thm)],[f2145]) ).
fof(f2148,plain,
( sQ85_spl
| sQ91_spl ),
inference(split_clause,[status(thm)],[f2140,f2145,f2058]) ).
fof(f2157,plain,
! [X0] :
( ~ sQ91_spl
| member(X0,singleton(X0)) ),
inference(paramodulation,[status(thm)],[f124,f2146]) ).
fof(f2202,definition,
( sQ92_spl
<=> inductive(null_class) ),
introduced(definition,[new_symbols(definition,[sQ92_spl])],[split_symbol_definition]) ).
fof(f2234,plain,
( ~ sQ60_spl
| null_class = unordered_pair(x,y) ),
inference(resolution,[status(thm)],[f1267,f232]) ).
fof(f2241,plain,
( ~ sQ60_spl
| sQ8_spl ),
inference(split_clause,[status(thm)],[f2234,f463,f1243]) ).
fof(f2281,plain,
! [X0,X1] :
( apply(choice,unordered_pair(X0,X1)) = X1
| unordered_pair(X0,X1) = null_class
| X0 = apply(choice,unordered_pair(X0,X1)) ),
inference(resolution,[status(thm)],[f2082,f118]) ).
fof(f2346,definition,
( sQ94_spl
<=> member(not_subclass_element(null_class,singleton(null_class)),singleton(null_class)) ),
introduced(definition,[new_symbols(definition,[sQ94_spl])],[split_symbol_definition]) ).
fof(f2348,plain,
( sQ94_spl
| ~ member(not_subclass_element(null_class,singleton(null_class)),singleton(null_class)) ),
inference(component_clause,[status(thm)],[f2346]) ).
fof(f2390,plain,
! [X0] :
( sQ94_spl
| ~ member(not_subclass_element(null_class,singleton(null_class)),X0)
| ~ subclass(X0,singleton(null_class)) ),
inference(resolution,[status(thm)],[f2348,f110]) ).
fof(f2401,plain,
( sQ94_spl
| null_class = singleton(null_class)
| member(not_subclass_element(singleton(null_class),null_class),singleton(null_class))
| ~ subclass(null_class,singleton(null_class)) ),
inference(resolution,[status(thm)],[f2390,f225]) ).
fof(f2408,definition,
( sQ95_spl
<=> subclass(null_class,singleton(null_class)) ),
introduced(definition,[new_symbols(definition,[sQ95_spl])],[split_symbol_definition]) ).
fof(f2410,plain,
( sQ95_spl
| ~ subclass(null_class,singleton(null_class)) ),
inference(component_clause,[status(thm)],[f2408]) ).
fof(f2412,definition,
( sQ96_spl
<=> member(not_subclass_element(singleton(null_class),null_class),singleton(null_class)) ),
introduced(definition,[new_symbols(definition,[sQ96_spl])],[split_symbol_definition]) ).
fof(f2415,plain,
( sQ94_spl
| sQ79_spl
| sQ96_spl
| ~ sQ95_spl ),
inference(split_clause,[status(thm)],[f2401,f2408,f2412,f1832,f2346]) ).
fof(f2416,plain,
( sQ95_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2410,f231]) ).
fof(f2417,plain,
sQ95_spl,
inference(contradiction_clause,[status(thm)],[f2416]) ).
fof(f2431,plain,
( sQ79_spl
| not_subclass_element(singleton(null_class),null_class) = null_class
| null_class != null_class ),
inference(paramodulation,[status(thm)],[f275,f1834]) ).
fof(f2448,plain,
! [X0] :
( ~ sQ91_spl
| not_subclass_element(singleton(X0),null_class) = X0
| member(X0,null_class) ),
inference(paramodulation,[status(thm)],[f275,f2157]) ).
fof(f2459,plain,
! [X0] :
( not_subclass_element(singleton(X0),null_class) = X0
| member(null_class,universal_class) ),
inference(paramodulation,[status(thm)],[f275,f245]) ).
fof(f2460,plain,
( sQ79_spl
| sQ47_spl
| ~ sQ3_spl ),
inference(split_clause,[status(thm)],[f2431,f288,f1021,f1832]) ).
fof(f2485,plain,
! [X0] :
( ~ sQ91_spl
| X0 = not_subclass_element(singleton(X0),null_class) ),
inference(forward_subsumption_resolution,[status(thm)],[f2448,f230]) ).
fof(f2490,definition,
! [X0] :
( sQ99_spl
<=> not_subclass_element(singleton(X0),null_class) = X0 ),
introduced(definition,[new_symbols(definition,[sQ99_spl])],[split_symbol_definition]) ).
fof(f2491,plain,
! [X0] :
( ~ sQ99_spl
| not_subclass_element(singleton(X0),null_class) = X0 ),
inference(component_clause,[status(thm)],[f2490]) ).
fof(f2493,plain,
( sQ99_spl
| sQ11_spl ),
inference(split_clause,[status(thm)],[f2459,f475,f2490]) ).
fof(f2495,plain,
( sQ59_spl
| ~ sQ79_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1837,f231]) ).
fof(f2496,plain,
( sQ59_spl
| ~ sQ79_spl ),
inference(contradiction_clause,[status(thm)],[f2495]) ).
fof(f2497,plain,
( sQ46_spl
| not_subclass_element(singleton(null_class),null_class) != null_class ),
inference(forward_demodulation,[status(thm)],[f124,f1020]) ).
fof(f2498,plain,
( sQ46_spl
| ~ sQ91_spl
| null_class != null_class ),
inference(forward_demodulation,[status(thm)],[f2485,f2497]) ).
fof(f2499,plain,
( sQ46_spl
| ~ sQ91_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f2498]) ).
fof(f2500,plain,
( sQ46_spl
| ~ sQ91_spl ),
inference(contradiction_clause,[status(thm)],[f2499]) ).
fof(f2524,plain,
! [X0,X1] :
( X0 = regular(unordered_pair(X0,X1))
| X1 = regular(unordered_pair(X0,X1))
| null_class = unordered_pair(X0,X1) ),
inference(resolution,[status(thm)],[f183,f118]) ).
fof(f2559,plain,
( sQ15_spl
| y = regular(unordered_pair(y,x))
| regular(unordered_pair(y,x)) = x ),
inference(resolution,[status(thm)],[f2524,f506]) ).
fof(f2560,plain,
( sQ8_spl
| x = regular(unordered_pair(x,y))
| regular(unordered_pair(x,y)) = y ),
inference(resolution,[status(thm)],[f2524,f465]) ).
fof(f2571,plain,
( y = regular(unordered_pair(y,x))
| regular(unordered_pair(y,x)) = x
| null_class != unordered_pair(x,y) ),
inference(paramodulation,[status(thm)],[f2524,f235]) ).
fof(f2590,plain,
! [X0,X1] :
( X0 = regular(unordered_pair(X0,X1))
| regular(unordered_pair(X0,X1)) = X1
| member(null_class,universal_class) ),
inference(paramodulation,[status(thm)],[f2524,f123]) ).
fof(f2593,definition,
( sQ102_spl
<=> regular(unordered_pair(y,x)) = x ),
introduced(definition,[new_symbols(definition,[sQ102_spl])],[split_symbol_definition]) ).
fof(f2594,plain,
( ~ sQ102_spl
| x = regular(unordered_pair(y,x)) ),
inference(component_clause,[status(thm)],[f2593]) ).
fof(f2596,definition,
( sQ103_spl
<=> y = regular(unordered_pair(y,x)) ),
introduced(definition,[new_symbols(definition,[sQ103_spl])],[split_symbol_definition]) ).
fof(f2597,plain,
( ~ sQ103_spl
| y = regular(unordered_pair(y,x)) ),
inference(component_clause,[status(thm)],[f2596]) ).
fof(f2599,plain,
( sQ103_spl
| sQ102_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f2571,f463,f2593,f2596]) ).
fof(f2602,definition,
( sQ104_spl
<=> regular(unordered_pair(x,y)) = y ),
introduced(definition,[new_symbols(definition,[sQ104_spl])],[split_symbol_definition]) ).
fof(f2603,plain,
( ~ sQ104_spl
| regular(unordered_pair(x,y)) = y ),
inference(component_clause,[status(thm)],[f2602]) ).
fof(f2605,definition,
( sQ105_spl
<=> x = regular(unordered_pair(x,y)) ),
introduced(definition,[new_symbols(definition,[sQ105_spl])],[split_symbol_definition]) ).
fof(f2606,plain,
( ~ sQ105_spl
| x = regular(unordered_pair(x,y)) ),
inference(component_clause,[status(thm)],[f2605]) ).
fof(f2608,plain,
( sQ8_spl
| sQ105_spl
| sQ104_spl ),
inference(split_clause,[status(thm)],[f2560,f2602,f2605,f463]) ).
fof(f2613,plain,
( sQ15_spl
| sQ103_spl
| sQ102_spl ),
inference(split_clause,[status(thm)],[f2559,f2593,f2596,f504]) ).
fof(f2618,definition,
! [X0,X1] :
( sQ107_spl
<=> ( X0 = regular(unordered_pair(X0,X1))
| regular(unordered_pair(X0,X1)) = X1 ) ),
introduced(definition,[new_symbols(definition,[sQ107_spl])],[split_symbol_definition]) ).
fof(f2619,plain,
! [X0,X1] :
( ~ sQ107_spl
| X1 = regular(unordered_pair(X1,X0))
| X0 = regular(unordered_pair(X1,X0)) ),
inference(component_clause,[status(thm)],[f2618]) ).
fof(f2621,plain,
( sQ107_spl
| sQ11_spl ),
inference(split_clause,[status(thm)],[f2590,f475,f2618]) ).
fof(f2633,plain,
( sQ19_spl
| ~ sQ84_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f519,f2056]) ).
fof(f2634,plain,
( sQ19_spl
| ~ sQ84_spl ),
inference(contradiction_clause,[status(thm)],[f2633]) ).
fof(f2635,plain,
( ~ sQ103_spl
| ~ sQ102_spl
| y = x ),
inference(forward_demodulation,[status(thm)],[f2594,f2597]) ).
fof(f2636,plain,
( ~ sQ103_spl
| ~ sQ102_spl
| sQ35_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2635,f796]) ).
fof(f2637,plain,
( ~ sQ103_spl
| ~ sQ102_spl
| sQ35_spl ),
inference(contradiction_clause,[status(thm)],[f2636]) ).
fof(f2638,plain,
( sQ43_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f949,f167]) ).
fof(f2639,plain,
sQ43_spl,
inference(contradiction_clause,[status(thm)],[f2638]) ).
fof(f2663,plain,
( ~ sQ105_spl
| ~ sQ104_spl
| x = y ),
inference(forward_demodulation,[status(thm)],[f2603,f2606]) ).
fof(f2664,plain,
( ~ sQ105_spl
| ~ sQ104_spl
| sQ35_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2663,f796]) ).
fof(f2665,plain,
( ~ sQ105_spl
| ~ sQ104_spl
| sQ35_spl ),
inference(contradiction_clause,[status(thm)],[f2664]) ).
fof(f2784,plain,
( ~ sQ105_spl
| null_class = unordered_pair(x,y)
| member(x,unordered_pair(x,y)) ),
inference(paramodulation,[status(thm)],[f2606,f183]) ).
fof(f2785,plain,
( ~ sQ105_spl
| null_class = unordered_pair(x,y)
| null_class = intersection(unordered_pair(x,y),x) ),
inference(paramodulation,[status(thm)],[f2606,f184]) ).
fof(f2786,plain,
( ~ sQ105_spl
| sQ8_spl
| sQ67_spl ),
inference(split_clause,[status(thm)],[f2784,f1393,f463,f2605]) ).
fof(f2787,definition,
( sQ112_spl
<=> null_class = intersection(unordered_pair(x,y),x) ),
introduced(definition,[new_symbols(definition,[sQ112_spl])],[split_symbol_definition]) ).
fof(f2788,plain,
( ~ sQ112_spl
| intersection(unordered_pair(x,y),x) = null_class ),
inference(component_clause,[status(thm)],[f2787]) ).
fof(f2790,plain,
( ~ sQ105_spl
| sQ8_spl
| sQ112_spl ),
inference(split_clause,[status(thm)],[f2785,f2787,f463,f2605]) ).
fof(f2807,plain,
( ~ sQ10_spl
| ~ sQ9_spl
| sQ35_spl ),
inference(split_clause,[status(thm)],[f1576,f794,f466,f469]) ).
fof(f2813,plain,
( ~ sQ17_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f511,f230]) ).
fof(f2814,plain,
~ sQ17_spl,
inference(contradiction_clause,[status(thm)],[f2813]) ).
fof(f2978,plain,
! [X0] :
( ~ sQ112_spl
| ~ member(X0,x)
| ~ member(X0,unordered_pair(x,y))
| member(X0,null_class) ),
inference(paramodulation,[status(thm)],[f2788,f140]) ).
fof(f2980,plain,
! [X0] :
( ~ sQ112_spl
| ~ member(X0,unordered_pair(x,y))
| ~ member(X0,x) ),
inference(forward_subsumption_resolution,[status(thm)],[f2978,f230]) ).
fof(f2986,definition,
( sQ115_spl
<=> subclass(image(element_relation,universal_class),universal_class) ),
introduced(definition,[new_symbols(definition,[sQ115_spl])],[split_symbol_definition]) ).
fof(f2988,plain,
( sQ115_spl
| ~ subclass(image(element_relation,universal_class),universal_class) ),
inference(component_clause,[status(thm)],[f2986]) ).
fof(f2995,plain,
! [X0] :
( ~ sQ15_spl
| member(y,null_class)
| ~ member(y,X0) ),
inference(paramodulation,[status(thm)],[f505,f1448]) ).
fof(f3002,definition,
! [X0] :
( sQ117_spl
<=> ~ member(y,X0) ),
introduced(definition,[new_symbols(definition,[sQ117_spl])],[split_symbol_definition]) ).
fof(f3003,plain,
! [X0] :
( ~ sQ117_spl
| ~ member(y,X0) ),
inference(component_clause,[status(thm)],[f3002]) ).
fof(f3005,plain,
( ~ sQ15_spl
| sQ30_spl
| sQ117_spl ),
inference(split_clause,[status(thm)],[f2995,f3002,f690,f504]) ).
fof(f3006,plain,
( ~ sQ29_spl
| ~ sQ117_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f687,f3003]) ).
fof(f3007,plain,
( ~ sQ29_spl
| ~ sQ117_spl ),
inference(contradiction_clause,[status(thm)],[f3006]) ).
fof(f3029,plain,
( ~ sQ19_spl
| x = y
| x = x ),
inference(resolution,[status(thm)],[f518,f118]) ).
fof(f3030,plain,
( ~ sQ19_spl
| sQ35_spl
| sQ68_spl ),
inference(split_clause,[status(thm)],[f3029,f1399,f794,f517]) ).
fof(f3034,plain,
( ~ sQ103_spl
| null_class = unordered_pair(y,x)
| member(y,unordered_pair(y,x)) ),
inference(paramodulation,[status(thm)],[f2597,f183]) ).
fof(f3035,plain,
( ~ sQ103_spl
| null_class = unordered_pair(y,x)
| null_class = intersection(unordered_pair(y,x),y) ),
inference(paramodulation,[status(thm)],[f2597,f184]) ).
fof(f3036,definition,
( sQ118_spl
<=> null_class = intersection(unordered_pair(y,x),y) ),
introduced(definition,[new_symbols(definition,[sQ118_spl])],[split_symbol_definition]) ).
fof(f3037,plain,
( ~ sQ118_spl
| intersection(unordered_pair(y,x),y) = null_class ),
inference(component_clause,[status(thm)],[f3036]) ).
fof(f3039,plain,
( ~ sQ103_spl
| sQ15_spl
| sQ118_spl ),
inference(split_clause,[status(thm)],[f3035,f3036,f504,f2596]) ).
fof(f3040,plain,
( ~ sQ103_spl
| sQ15_spl
| sQ33_spl ),
inference(split_clause,[status(thm)],[f3034,f752,f504,f2596]) ).
fof(f3121,plain,
! [X0] :
( ~ sQ118_spl
| ~ member(X0,y)
| ~ member(X0,unordered_pair(y,x))
| member(X0,null_class) ),
inference(paramodulation,[status(thm)],[f3037,f140]) ).
fof(f3123,plain,
! [X0] :
( ~ sQ118_spl
| ~ member(X0,unordered_pair(y,x))
| ~ member(X0,y) ),
inference(forward_subsumption_resolution,[status(thm)],[f3121,f230]) ).
fof(f3128,plain,
! [X0,X1] :
( ~ member(null_class,X1)
| ~ subclass(image(successor_relation,unordered_pair(null_class,X0)),unordered_pair(null_class,X0))
| inductive(unordered_pair(null_class,X0)) ),
inference(resolution,[status(thm)],[f166,f1448]) ).
fof(f3131,definition,
! [X0] :
( sQ123_spl
<=> ( ~ subclass(image(successor_relation,unordered_pair(null_class,X0)),unordered_pair(null_class,X0))
| inductive(unordered_pair(null_class,X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ123_spl])],[split_symbol_definition]) ).
fof(f3134,plain,
( sQ57_spl
| sQ123_spl ),
inference(split_clause,[status(thm)],[f3128,f3131,f1214]) ).
fof(f3154,plain,
( ~ sQ112_spl
| null_class = unordered_pair(x,y)
| ~ member(regular(unordered_pair(x,y)),x) ),
inference(resolution,[status(thm)],[f2980,f183]) ).
fof(f3155,plain,
( ~ sQ112_spl
| unordered_pair(x,y) = null_class
| ~ member(apply(choice,unordered_pair(x,y)),x) ),
inference(resolution,[status(thm)],[f2980,f2082]) ).
fof(f3156,plain,
( ~ sQ112_spl
| ~ inductive(unordered_pair(x,y))
| ~ member(null_class,x) ),
inference(resolution,[status(thm)],[f2980,f164]) ).
fof(f3157,plain,
( ~ sQ112_spl
| unordered_pair(x,y) = null_class
| ~ member(not_subclass_element(unordered_pair(x,y),null_class),x) ),
inference(resolution,[status(thm)],[f2980,f233]) ).
fof(f3161,plain,
! [X0] :
( ~ sQ112_spl
| ~ member(x,X0)
| ~ member(x,x) ),
inference(resolution,[status(thm)],[f2980,f1448]) ).
fof(f3163,definition,
( sQ125_spl
<=> member(null_class,x) ),
introduced(definition,[new_symbols(definition,[sQ125_spl])],[split_symbol_definition]) ).
fof(f3166,definition,
( sQ126_spl
<=> inductive(unordered_pair(x,y)) ),
introduced(definition,[new_symbols(definition,[sQ126_spl])],[split_symbol_definition]) ).
fof(f3169,plain,
( ~ sQ112_spl
| ~ sQ126_spl
| ~ sQ125_spl ),
inference(split_clause,[status(thm)],[f3156,f3163,f3166,f2787]) ).
fof(f3170,definition,
( sQ127_spl
<=> member(x,x) ),
introduced(definition,[new_symbols(definition,[sQ127_spl])],[split_symbol_definition]) ).
fof(f3172,plain,
( sQ127_spl
| ~ member(x,x) ),
inference(component_clause,[status(thm)],[f3170]) ).
fof(f3173,definition,
! [X0] :
( sQ128_spl
<=> ~ member(x,X0) ),
introduced(definition,[new_symbols(definition,[sQ128_spl])],[split_symbol_definition]) ).
fof(f3174,plain,
! [X0] :
( ~ sQ128_spl
| ~ member(x,X0) ),
inference(component_clause,[status(thm)],[f3173]) ).
fof(f3176,plain,
( ~ sQ112_spl
| sQ128_spl
| ~ sQ127_spl ),
inference(split_clause,[status(thm)],[f3161,f3170,f3173,f2787]) ).
fof(f3177,definition,
( sQ129_spl
<=> member(not_subclass_element(unordered_pair(x,y),null_class),x) ),
introduced(definition,[new_symbols(definition,[sQ129_spl])],[split_symbol_definition]) ).
fof(f3179,plain,
( sQ129_spl
| ~ member(not_subclass_element(unordered_pair(x,y),null_class),x) ),
inference(component_clause,[status(thm)],[f3177]) ).
fof(f3180,plain,
( ~ sQ112_spl
| sQ8_spl
| ~ sQ129_spl ),
inference(split_clause,[status(thm)],[f3157,f3177,f463,f2787]) ).
fof(f3181,definition,
( sQ130_spl
<=> member(apply(choice,unordered_pair(x,y)),x) ),
introduced(definition,[new_symbols(definition,[sQ130_spl])],[split_symbol_definition]) ).
fof(f3184,plain,
( ~ sQ112_spl
| sQ8_spl
| ~ sQ130_spl ),
inference(split_clause,[status(thm)],[f3155,f3181,f463,f2787]) ).
fof(f3185,definition,
( sQ131_spl
<=> member(regular(unordered_pair(x,y)),x) ),
introduced(definition,[new_symbols(definition,[sQ131_spl])],[split_symbol_definition]) ).
fof(f3187,plain,
( sQ131_spl
| ~ member(regular(unordered_pair(x,y)),x) ),
inference(component_clause,[status(thm)],[f3185]) ).
fof(f3188,plain,
( ~ sQ112_spl
| sQ8_spl
| ~ sQ131_spl ),
inference(split_clause,[status(thm)],[f3154,f3185,f463,f2787]) ).
fof(f3190,plain,
( ~ sQ19_spl
| ~ sQ128_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f518,f3174]) ).
fof(f3192,plain,
( ~ sQ19_spl
| ~ sQ128_spl ),
inference(contradiction_clause,[status(thm)],[f3190]) ).
fof(f3193,plain,
( sQ129_spl
| ~ sQ26_spl
| ~ member(y,x) ),
inference(forward_demodulation,[status(thm)],[f640,f3179]) ).
fof(f3195,plain,
( sQ131_spl
| ~ sQ104_spl
| ~ member(y,x) ),
inference(forward_demodulation,[status(thm)],[f2603,f3187]) ).
fof(f3219,plain,
( ~ sQ104_spl
| null_class = unordered_pair(x,y)
| member(y,unordered_pair(x,y)) ),
inference(paramodulation,[status(thm)],[f2603,f183]) ).
fof(f3220,plain,
( ~ sQ104_spl
| null_class = unordered_pair(x,y)
| null_class = intersection(unordered_pair(x,y),y) ),
inference(paramodulation,[status(thm)],[f2603,f184]) ).
fof(f3221,definition,
( sQ134_spl
<=> null_class = intersection(unordered_pair(x,y),y) ),
introduced(definition,[new_symbols(definition,[sQ134_spl])],[split_symbol_definition]) ).
fof(f3222,plain,
( ~ sQ134_spl
| null_class = intersection(unordered_pair(x,y),y) ),
inference(component_clause,[status(thm)],[f3221]) ).
fof(f3224,plain,
( ~ sQ104_spl
| sQ8_spl
| sQ134_spl ),
inference(split_clause,[status(thm)],[f3220,f3221,f463,f2602]) ).
fof(f3225,plain,
( ~ sQ104_spl
| sQ8_spl
| sQ29_spl ),
inference(split_clause,[status(thm)],[f3219,f686,f463,f2602]) ).
fof(f3281,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)],[f1447,f166]) ).
fof(f3285,definition,
! [X1] :
( sQ135_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,[sQ135_spl])],[split_symbol_definition]) ).
fof(f3288,plain,
( sQ135_spl
| sQ57_spl ),
inference(split_clause,[status(thm)],[f3281,f1214,f3285]) ).
fof(f3291,plain,
! [X0] :
( sQ129_spl
| ~ sQ26_spl
| ~ member(y,X0)
| ~ subclass(X0,x) ),
inference(resolution,[status(thm)],[f3193,f110]) ).
fof(f3328,plain,
! [X0] :
( sQ127_spl
| ~ subclass(X0,x)
| ~ member(x,X0) ),
inference(resolution,[status(thm)],[f3172,f110]) ).
fof(f3343,plain,
( sQ129_spl
| ~ sQ26_spl
| ~ inductive(x)
| ~ member(y,omega) ),
inference(resolution,[status(thm)],[f3291,f168]) ).
fof(f3347,definition,
( sQ136_spl
<=> member(y,omega) ),
introduced(definition,[new_symbols(definition,[sQ136_spl])],[split_symbol_definition]) ).
fof(f3350,definition,
( sQ137_spl
<=> inductive(x) ),
introduced(definition,[new_symbols(definition,[sQ137_spl])],[split_symbol_definition]) ).
fof(f3353,plain,
( sQ129_spl
| ~ sQ26_spl
| ~ sQ137_spl
| ~ sQ136_spl ),
inference(split_clause,[status(thm)],[f3343,f3347,f3350,f639,f3177]) ).
fof(f3354,plain,
( ~ sQ30_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f691,f230]) ).
fof(f3355,plain,
~ sQ30_spl,
inference(contradiction_clause,[status(thm)],[f3354]) ).
fof(f3375,plain,
! [X0] :
( sQ131_spl
| ~ sQ104_spl
| ~ member(y,X0)
| ~ subclass(X0,x) ),
inference(resolution,[status(thm)],[f3195,f110]) ).
fof(f3460,plain,
( sQ127_spl
| ~ inductive(x)
| ~ member(x,omega) ),
inference(resolution,[status(thm)],[f3328,f168]) ).
fof(f3464,definition,
( sQ142_spl
<=> member(x,omega) ),
introduced(definition,[new_symbols(definition,[sQ142_spl])],[split_symbol_definition]) ).
fof(f3467,plain,
( sQ127_spl
| ~ sQ137_spl
| ~ sQ142_spl ),
inference(split_clause,[status(thm)],[f3460,f3464,f3350,f3170]) ).
fof(f3477,plain,
( sQ131_spl
| ~ sQ104_spl
| ~ inductive(x)
| ~ member(y,omega) ),
inference(resolution,[status(thm)],[f3375,f168]) ).
fof(f3481,plain,
( sQ131_spl
| ~ sQ104_spl
| ~ sQ137_spl
| ~ sQ136_spl ),
inference(split_clause,[status(thm)],[f3477,f3347,f3350,f2602,f3185]) ).
fof(f3528,plain,
! [X0] :
( ~ sQ134_spl
| ~ member(X0,y)
| ~ member(X0,unordered_pair(x,y))
| member(X0,null_class) ),
inference(paramodulation,[status(thm)],[f3222,f140]) ).
fof(f3530,plain,
! [X0] :
( ~ sQ134_spl
| ~ member(X0,unordered_pair(x,y))
| ~ member(X0,y) ),
inference(forward_subsumption_resolution,[status(thm)],[f3528,f230]) ).
fof(f3544,plain,
! [X0] :
( not_subclass_element(unordered_pair(omega,X0),null_class) = omega
| not_subclass_element(unordered_pair(omega,X0),null_class) = X0
| member(omega,null_class) ),
inference(paramodulation,[status(thm)],[f276,f1059]) ).
fof(f3547,plain,
! [X0] :
( not_subclass_element(unordered_pair(null_class,X0),null_class) = null_class
| not_subclass_element(unordered_pair(null_class,X0),null_class) = X0
| member(null_class,null_class) ),
inference(paramodulation,[status(thm)],[f276,f1073]) ).
fof(f3560,plain,
! [X0] :
( not_subclass_element(unordered_pair(X0,null_class),null_class) = X0
| not_subclass_element(unordered_pair(X0,null_class),null_class) = null_class
| member(null_class,null_class) ),
inference(paramodulation,[status(thm)],[f276,f1074]) ).
fof(f3566,plain,
! [X0] :
( not_subclass_element(unordered_pair(X0,omega),null_class) = X0
| not_subclass_element(unordered_pair(X0,omega),null_class) = omega
| member(omega,null_class) ),
inference(paramodulation,[status(thm)],[f276,f1060]) ).
fof(f3598,definition,
( sQ144_spl
<=> member(omega,null_class) ),
introduced(definition,[new_symbols(definition,[sQ144_spl])],[split_symbol_definition]) ).
fof(f3599,plain,
( ~ sQ144_spl
| member(omega,null_class) ),
inference(component_clause,[status(thm)],[f3598]) ).
fof(f3601,definition,
! [X0] :
( sQ145_spl
<=> ( not_subclass_element(unordered_pair(omega,X0),null_class) = omega
| not_subclass_element(unordered_pair(omega,X0),null_class) = X0 ) ),
introduced(definition,[new_symbols(definition,[sQ145_spl])],[split_symbol_definition]) ).
fof(f3604,plain,
( sQ145_spl
| sQ144_spl ),
inference(split_clause,[status(thm)],[f3544,f3598,f3601]) ).
fof(f3605,plain,
( sQ39_spl
| sQ38_spl ),
inference(split_clause,[status(thm)],[f3547,f820,f823]) ).
fof(f3611,definition,
! [X0] :
( sQ147_spl
<=> ( not_subclass_element(unordered_pair(X0,omega),null_class) = X0
| not_subclass_element(unordered_pair(X0,omega),null_class) = omega ) ),
introduced(definition,[new_symbols(definition,[sQ147_spl])],[split_symbol_definition]) ).
fof(f3614,plain,
( sQ147_spl
| sQ144_spl ),
inference(split_clause,[status(thm)],[f3566,f3598,f3611]) ).
fof(f3632,definition,
! [X0] :
( sQ149_spl
<=> ( not_subclass_element(unordered_pair(X0,null_class),null_class) = X0
| not_subclass_element(unordered_pair(X0,null_class),null_class) = null_class ) ),
introduced(definition,[new_symbols(definition,[sQ149_spl])],[split_symbol_definition]) ).
fof(f3635,plain,
( sQ149_spl
| sQ38_spl ),
inference(split_clause,[status(thm)],[f3560,f820,f3632]) ).
fof(f3654,plain,
( sQ115_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2988,f113]) ).
fof(f3655,plain,
sQ115_spl,
inference(contradiction_clause,[status(thm)],[f3654]) ).
fof(f3663,plain,
( ~ sQ144_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3599,f230]) ).
fof(f3664,plain,
~ sQ144_spl,
inference(contradiction_clause,[status(thm)],[f3663]) ).
fof(f3812,plain,
! [X0] :
( ~ sQ8_spl
| member(y,null_class)
| ~ member(y,X0) ),
inference(paramodulation,[status(thm)],[f464,f1447]) ).
fof(f3815,plain,
! [X0] :
( ~ sQ8_spl
| member(x,null_class)
| ~ member(x,X0) ),
inference(paramodulation,[status(thm)],[f464,f1448]) ).
fof(f3844,plain,
( ~ sQ8_spl
| sQ17_spl
| sQ128_spl ),
inference(split_clause,[status(thm)],[f3815,f3173,f510,f463]) ).
fof(f3858,plain,
( ~ sQ8_spl
| sQ30_spl
| sQ117_spl ),
inference(split_clause,[status(thm)],[f3812,f3002,f690,f463]) ).
fof(f3860,plain,
( ~ sQ33_spl
| ~ sQ117_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f753,f3003]) ).
fof(f3861,plain,
( ~ sQ33_spl
| ~ sQ117_spl ),
inference(contradiction_clause,[status(thm)],[f3860]) ).
fof(f3948,plain,
( ~ sQ102_spl
| null_class = unordered_pair(y,x)
| member(x,unordered_pair(y,x)) ),
inference(paramodulation,[status(thm)],[f2594,f183]) ).
fof(f3949,plain,
( ~ sQ102_spl
| null_class = unordered_pair(y,x)
| null_class = intersection(unordered_pair(y,x),x) ),
inference(paramodulation,[status(thm)],[f2594,f184]) ).
fof(f3954,plain,
( ~ sQ102_spl
| sQ15_spl
| sQ19_spl ),
inference(split_clause,[status(thm)],[f3948,f517,f504,f2593]) ).
fof(f3955,definition,
( sQ154_spl
<=> null_class = intersection(unordered_pair(y,x),x) ),
introduced(definition,[new_symbols(definition,[sQ154_spl])],[split_symbol_definition]) ).
fof(f3956,plain,
( ~ sQ154_spl
| intersection(unordered_pair(y,x),x) = null_class ),
inference(component_clause,[status(thm)],[f3955]) ).
fof(f3958,plain,
( ~ sQ102_spl
| sQ15_spl
| sQ154_spl ),
inference(split_clause,[status(thm)],[f3949,f3955,f504,f2593]) ).
fof(f4002,plain,
! [X0] :
( regular(unordered_pair(omega,X0)) = X0
| regular(unordered_pair(omega,X0)) = omega
| member(omega,null_class) ),
inference(paramodulation,[status(thm)],[f2524,f1059]) ).
fof(f4016,plain,
! [X0] :
( regular(unordered_pair(X0,omega)) = omega
| regular(unordered_pair(X0,omega)) = X0
| member(omega,null_class) ),
inference(paramodulation,[status(thm)],[f2524,f1060]) ).
fof(f4051,definition,
! [X0] :
( sQ155_spl
<=> ( regular(unordered_pair(X0,omega)) = omega
| regular(unordered_pair(X0,omega)) = X0 ) ),
introduced(definition,[new_symbols(definition,[sQ155_spl])],[split_symbol_definition]) ).
fof(f4054,plain,
( sQ155_spl
| sQ144_spl ),
inference(split_clause,[status(thm)],[f4016,f3598,f4051]) ).
fof(f4076,definition,
! [X0] :
( sQ157_spl
<=> ( regular(unordered_pair(omega,X0)) = X0
| regular(unordered_pair(omega,X0)) = omega ) ),
introduced(definition,[new_symbols(definition,[sQ157_spl])],[split_symbol_definition]) ).
fof(f4079,plain,
( sQ157_spl
| sQ144_spl ),
inference(split_clause,[status(thm)],[f4002,f3598,f4076]) ).
fof(f4083,definition,
! [X0] :
( sQ158_spl
<=> ( regular(unordered_pair(X0,null_class)) = null_class
| regular(unordered_pair(X0,null_class)) = X0 ) ),
introduced(definition,[new_symbols(definition,[sQ158_spl])],[split_symbol_definition]) ).
fof(f4096,plain,
! [X0] :
( ~ sQ5_spl
| regular(unordered_pair(not_subclass_element(universal_class,null_class),X0)) = X0
| regular(unordered_pair(not_subclass_element(universal_class,null_class),X0)) = not_subclass_element(universal_class,null_class)
| member(not_subclass_element(universal_class,null_class),null_class) ),
inference(paramodulation,[status(thm)],[f2524,f296]) ).
fof(f4101,definition,
! [X0] :
( sQ159_spl
<=> ( regular(unordered_pair(not_subclass_element(universal_class,null_class),X0)) = X0
| regular(unordered_pair(not_subclass_element(universal_class,null_class),X0)) = not_subclass_element(universal_class,null_class) ) ),
introduced(definition,[new_symbols(definition,[sQ159_spl])],[split_symbol_definition]) ).
fof(f4104,plain,
( ~ sQ5_spl
| sQ159_spl
| sQ13_spl ),
inference(split_clause,[status(thm)],[f4096,f487,f4101,f295]) ).
fof(f4109,plain,
! [X0] :
( regular(unordered_pair(null_class,X0)) = X0
| regular(unordered_pair(null_class,X0)) = null_class
| member(null_class,null_class) ),
inference(paramodulation,[status(thm)],[f2524,f1073]) ).
fof(f4113,definition,
! [X0] :
( sQ160_spl
<=> ( regular(unordered_pair(null_class,X0)) = X0
| regular(unordered_pair(null_class,X0)) = null_class ) ),
introduced(definition,[new_symbols(definition,[sQ160_spl])],[split_symbol_definition]) ).
fof(f4116,plain,
( sQ160_spl
| sQ38_spl ),
inference(split_clause,[status(thm)],[f4109,f820,f4113]) ).
fof(f4128,plain,
! [X0] :
( regular(unordered_pair(X0,null_class)) = null_class
| regular(unordered_pair(X0,null_class)) = X0
| member(null_class,null_class) ),
inference(paramodulation,[status(thm)],[f2524,f1074]) ).
fof(f4132,plain,
( sQ158_spl
| sQ38_spl ),
inference(split_clause,[status(thm)],[f4128,f820,f4083]) ).
fof(f4183,plain,
! [X0] :
( ~ inductive(null_class)
| subclass(omega,X0) ),
inference(resolution,[status(thm)],[f925,f168]) ).
fof(f4187,plain,
( ~ sQ92_spl
| sQ63_spl ),
inference(split_clause,[status(thm)],[f4183,f1277,f2202]) ).
fof(f4396,plain,
( ~ sQ67_spl
| ~ sQ128_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f1394,f3174]) ).
fof(f4400,plain,
( ~ sQ67_spl
| ~ sQ128_spl ),
inference(contradiction_clause,[status(thm)],[f4396]) ).
fof(f4641,plain,
! [X0,X1] :
( not_subclass_element(ordered_pair(X0,X1),null_class) = unordered_pair(X0,singleton(X1))
| not_subclass_element(ordered_pair(X0,X1),null_class) = singleton(X0)
| member(null_class,universal_class) ),
inference(paramodulation,[status(thm)],[f483,f243]) ).
fof(f4668,definition,
! [X0,X1] :
( sQ170_spl
<=> ( not_subclass_element(ordered_pair(X0,X1),null_class) = unordered_pair(X0,singleton(X1))
| not_subclass_element(ordered_pair(X0,X1),null_class) = singleton(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ170_spl])],[split_symbol_definition]) ).
fof(f4671,plain,
( sQ170_spl
| sQ11_spl ),
inference(split_clause,[status(thm)],[f4641,f475,f4668]) ).
fof(f4784,plain,
( not_subclass_element(unordered_pair(y,x),unordered_pair(x,y)) = x
| y = not_subclass_element(unordered_pair(y,x),unordered_pair(x,y))
| y = not_subclass_element(unordered_pair(x,y),unordered_pair(y,x))
| x = not_subclass_element(unordered_pair(x,y),unordered_pair(y,x)) ),
inference(resolution,[status(thm)],[f378,f235]) ).
fof(f4815,plain,
! [X0,X1] :
( ~ sQ9_spl
| not_subclass_element(unordered_pair(X1,X0),unordered_pair(y,x)) = X1
| x = not_subclass_element(unordered_pair(y,x),unordered_pair(X1,X0))
| y = not_subclass_element(unordered_pair(y,x),unordered_pair(X1,X0))
| not_subclass_element(unordered_pair(X1,X0),null_class) = y
| X0 = not_subclass_element(unordered_pair(X1,X0),unordered_pair(y,x)) ),
inference(paramodulation,[status(thm)],[f378,f467]) ).
fof(f4863,plain,
! [X0,X1] :
( sQ8_spl
| y = not_subclass_element(unordered_pair(x,y),unordered_pair(X0,X1))
| null_class != unordered_pair(X0,X1)
| not_subclass_element(unordered_pair(X0,X1),unordered_pair(x,y)) = X0
| not_subclass_element(unordered_pair(X0,X1),unordered_pair(x,y)) = X1
| x = not_subclass_element(unordered_pair(x,y),unordered_pair(X0,X1)) ),
inference(paramodulation,[status(thm)],[f378,f465]) ).
fof(f4865,plain,
! [X0,X1] :
( ~ sQ102_spl
| not_subclass_element(unordered_pair(X0,X1),unordered_pair(y,x)) = X1
| not_subclass_element(unordered_pair(y,x),unordered_pair(X0,X1)) = x
| not_subclass_element(unordered_pair(X0,X1),unordered_pair(y,x)) = X0
| y = not_subclass_element(unordered_pair(y,x),unordered_pair(X0,X1))
| x = regular(unordered_pair(X0,X1)) ),
inference(paramodulation,[status(thm)],[f378,f2594]) ).
fof(f4936,definition,
( sQ178_spl
<=> x = not_subclass_element(unordered_pair(x,y),unordered_pair(y,x)) ),
introduced(definition,[new_symbols(definition,[sQ178_spl])],[split_symbol_definition]) ).
fof(f4937,plain,
( ~ sQ178_spl
| x = not_subclass_element(unordered_pair(x,y),unordered_pair(y,x)) ),
inference(component_clause,[status(thm)],[f4936]) ).
fof(f4939,definition,
( sQ179_spl
<=> y = not_subclass_element(unordered_pair(x,y),unordered_pair(y,x)) ),
introduced(definition,[new_symbols(definition,[sQ179_spl])],[split_symbol_definition]) ).
fof(f4940,plain,
( ~ sQ179_spl
| y = not_subclass_element(unordered_pair(x,y),unordered_pair(y,x)) ),
inference(component_clause,[status(thm)],[f4939]) ).
fof(f4942,definition,
( sQ180_spl
<=> y = not_subclass_element(unordered_pair(y,x),unordered_pair(x,y)) ),
introduced(definition,[new_symbols(definition,[sQ180_spl])],[split_symbol_definition]) ).
fof(f4943,plain,
( ~ sQ180_spl
| not_subclass_element(unordered_pair(y,x),unordered_pair(x,y)) = y ),
inference(component_clause,[status(thm)],[f4942]) ).
fof(f4945,definition,
( sQ181_spl
<=> not_subclass_element(unordered_pair(y,x),unordered_pair(x,y)) = x ),
introduced(definition,[new_symbols(definition,[sQ181_spl])],[split_symbol_definition]) ).
fof(f4946,plain,
( ~ sQ181_spl
| not_subclass_element(unordered_pair(y,x),unordered_pair(x,y)) = x ),
inference(component_clause,[status(thm)],[f4945]) ).
fof(f4948,plain,
( sQ181_spl
| sQ180_spl
| sQ179_spl
| sQ178_spl ),
inference(split_clause,[status(thm)],[f4784,f4936,f4939,f4942,f4945]) ).
fof(f5014,plain,
! [X0] :
( ~ sQ154_spl
| ~ member(X0,x)
| ~ member(X0,unordered_pair(y,x))
| member(X0,null_class) ),
inference(paramodulation,[status(thm)],[f3956,f140]) ).
fof(f5016,plain,
! [X0] :
( ~ sQ154_spl
| ~ member(X0,unordered_pair(y,x))
| ~ member(X0,x) ),
inference(forward_subsumption_resolution,[status(thm)],[f5014,f230]) ).
fof(f5156,plain,
( ~ sQ67_spl
| ~ sQ134_spl
| ~ member(x,y) ),
inference(resolution,[status(thm)],[f3530,f1394]) ).
fof(f5157,plain,
( ~ sQ29_spl
| ~ sQ134_spl
| ~ member(y,y) ),
inference(resolution,[status(thm)],[f3530,f687]) ).
fof(f5158,plain,
( ~ sQ134_spl
| null_class = unordered_pair(x,y)
| ~ member(regular(unordered_pair(x,y)),y) ),
inference(resolution,[status(thm)],[f3530,f183]) ).
fof(f5159,plain,
( ~ sQ134_spl
| unordered_pair(x,y) = null_class
| ~ member(apply(choice,unordered_pair(x,y)),y) ),
inference(resolution,[status(thm)],[f3530,f2082]) ).
fof(f5160,plain,
( ~ sQ134_spl
| ~ inductive(unordered_pair(x,y))
| ~ member(null_class,y) ),
inference(resolution,[status(thm)],[f3530,f164]) ).
fof(f5164,plain,
( ~ sQ134_spl
| unordered_pair(x,y) = null_class
| ~ member(not_subclass_element(unordered_pair(x,y),null_class),y) ),
inference(resolution,[status(thm)],[f3530,f233]) ).
fof(f5168,plain,
! [X0] :
( ~ sQ134_spl
| ~ member(y,X0)
| ~ member(y,y) ),
inference(resolution,[status(thm)],[f3530,f1447]) ).
fof(f5169,plain,
! [X0] :
( ~ sQ134_spl
| ~ member(x,X0)
| ~ member(x,y) ),
inference(resolution,[status(thm)],[f3530,f1448]) ).
fof(f5180,definition,
( sQ184_spl
<=> member(y,y) ),
introduced(definition,[new_symbols(definition,[sQ184_spl])],[split_symbol_definition]) ).
fof(f5182,plain,
( sQ184_spl
| ~ member(y,y) ),
inference(component_clause,[status(thm)],[f5180]) ).
fof(f5183,plain,
( ~ sQ134_spl
| sQ117_spl
| ~ sQ184_spl ),
inference(split_clause,[status(thm)],[f5168,f5180,f3002,f3221]) ).
fof(f5184,definition,
( sQ185_spl
<=> member(apply(choice,unordered_pair(x,y)),y) ),
introduced(definition,[new_symbols(definition,[sQ185_spl])],[split_symbol_definition]) ).
fof(f5187,plain,
( ~ sQ134_spl
| sQ8_spl
| ~ sQ185_spl ),
inference(split_clause,[status(thm)],[f5159,f5184,f463,f3221]) ).
fof(f5188,definition,
( sQ186_spl
<=> member(regular(unordered_pair(x,y)),y) ),
introduced(definition,[new_symbols(definition,[sQ186_spl])],[split_symbol_definition]) ).
fof(f5190,plain,
( sQ186_spl
| ~ member(regular(unordered_pair(x,y)),y) ),
inference(component_clause,[status(thm)],[f5188]) ).
fof(f5191,plain,
( ~ sQ134_spl
| sQ8_spl
| ~ sQ186_spl ),
inference(split_clause,[status(thm)],[f5158,f5188,f463,f3221]) ).
fof(f5193,definition,
( sQ187_spl
<=> member(not_subclass_element(unordered_pair(x,y),null_class),y) ),
introduced(definition,[new_symbols(definition,[sQ187_spl])],[split_symbol_definition]) ).
fof(f5195,plain,
( sQ187_spl
| ~ member(not_subclass_element(unordered_pair(x,y),null_class),y) ),
inference(component_clause,[status(thm)],[f5193]) ).
fof(f5196,plain,
( ~ sQ134_spl
| sQ8_spl
| ~ sQ187_spl ),
inference(split_clause,[status(thm)],[f5164,f5193,f463,f3221]) ).
fof(f5197,definition,
( sQ188_spl
<=> member(x,y) ),
introduced(definition,[new_symbols(definition,[sQ188_spl])],[split_symbol_definition]) ).
fof(f5199,plain,
( sQ188_spl
| ~ member(x,y) ),
inference(component_clause,[status(thm)],[f5197]) ).
fof(f5200,plain,
( ~ sQ134_spl
| sQ128_spl
| ~ sQ188_spl ),
inference(split_clause,[status(thm)],[f5169,f5197,f3173,f3221]) ).
fof(f5201,definition,
( sQ189_spl
<=> member(null_class,y) ),
introduced(definition,[new_symbols(definition,[sQ189_spl])],[split_symbol_definition]) ).
fof(f5204,plain,
( ~ sQ134_spl
| ~ sQ126_spl
| ~ sQ189_spl ),
inference(split_clause,[status(thm)],[f5160,f5201,f3166,f3221]) ).
fof(f5205,plain,
( sQ187_spl
| ~ sQ25_spl
| ~ member(x,y) ),
inference(forward_demodulation,[status(thm)],[f637,f5195]) ).
fof(f5343,plain,
! [X0,X1] :
( ~ sQ9_spl
| not_subclass_element(unordered_pair(y,x),unordered_pair(X1,X0)) = x
| y != x
| not_subclass_element(unordered_pair(X1,X0),unordered_pair(y,x)) = X1
| not_subclass_element(unordered_pair(X1,X0),null_class) = y
| X0 = not_subclass_element(unordered_pair(X1,X0),unordered_pair(y,x)) ),
inference(equality_factoring,[status(thm)],[f4815]) ).
fof(f5389,definition,
! [X0,X1] :
( sQ197_spl
<=> ( not_subclass_element(unordered_pair(y,x),unordered_pair(X1,X0)) = x
| not_subclass_element(unordered_pair(X1,X0),unordered_pair(y,x)) = X1
| not_subclass_element(unordered_pair(X1,X0),null_class) = y
| X0 = not_subclass_element(unordered_pair(X1,X0),unordered_pair(y,x)) ) ),
introduced(definition,[new_symbols(definition,[sQ197_spl])],[split_symbol_definition]) ).
fof(f5392,plain,
( ~ sQ9_spl
| ~ sQ35_spl
| sQ197_spl ),
inference(split_clause,[status(thm)],[f5343,f5389,f794,f466]) ).
fof(f5402,plain,
! [X0] :
( ~ sQ29_spl
| ~ sQ134_spl
| ~ subclass(X0,y)
| ~ member(y,X0) ),
inference(resolution,[status(thm)],[f5157,f110]) ).
fof(f5414,plain,
! [X0,X1] :
( ~ sQ102_spl
| regular(unordered_pair(X0,X1)) = X1
| regular(unordered_pair(X0,X1)) = X0
| not_subclass_element(unordered_pair(X0,X1),unordered_pair(y,x)) = X1
| X0 = not_subclass_element(unordered_pair(X0,X1),unordered_pair(y,x))
| y = not_subclass_element(unordered_pair(y,x),null_class)
| regular(unordered_pair(X0,X1)) = x
| x = not_subclass_element(unordered_pair(y,x),unordered_pair(X0,X1)) ),
inference(paramodulation,[status(thm)],[f2524,f4865]) ).
fof(f5415,plain,
! [X0,X1] :
( ~ sQ102_spl
| X1 = not_subclass_element(unordered_pair(X0,X1),null_class)
| not_subclass_element(unordered_pair(X0,X1),null_class) = X0
| not_subclass_element(unordered_pair(X0,X1),unordered_pair(y,x)) = X1
| X0 = not_subclass_element(unordered_pair(X0,X1),unordered_pair(y,x))
| y = not_subclass_element(unordered_pair(y,x),null_class)
| regular(unordered_pair(X0,X1)) = x
| x = not_subclass_element(unordered_pair(y,x),unordered_pair(X0,X1)) ),
inference(paramodulation,[status(thm)],[f276,f4865]) ).
fof(f5418,plain,
! [X0,X1] :
( ~ sQ102_spl
| not_subclass_element(unordered_pair(X0,X1),unordered_pair(y,x)) = X1
| X0 = not_subclass_element(unordered_pair(X0,X1),unordered_pair(y,x))
| regular(unordered_pair(X0,X1)) = x
| x = not_subclass_element(unordered_pair(y,x),unordered_pair(X0,X1))
| unordered_pair(y,x) = unordered_pair(X0,X1)
| not_subclass_element(unordered_pair(X0,X1),unordered_pair(y,x)) = X1
| not_subclass_element(unordered_pair(X0,X1),unordered_pair(y,x)) = X0
| member(y,unordered_pair(y,x)) ),
inference(paramodulation,[status(thm)],[f4865,f251]) ).
fof(f5420,plain,
! [X0,X1] :
( ~ sQ102_spl
| not_subclass_element(unordered_pair(X0,X1),unordered_pair(y,x)) = X1
| X0 = not_subclass_element(unordered_pair(X0,X1),unordered_pair(y,x))
| regular(unordered_pair(X0,X1)) = x
| x = not_subclass_element(unordered_pair(y,x),unordered_pair(X0,X1))
| unordered_pair(y,x) = unordered_pair(X0,X1)
| member(y,unordered_pair(y,x))
| member(not_subclass_element(unordered_pair(X0,X1),unordered_pair(y,x)),unordered_pair(X0,X1)) ),
inference(paramodulation,[status(thm)],[f4865,f225]) ).
fof(f5422,plain,
! [X0,X1] :
( ~ sQ102_spl
| not_subclass_element(unordered_pair(X0,X1),unordered_pair(y,x)) = X1
| X0 = not_subclass_element(unordered_pair(X0,X1),unordered_pair(y,x))
| regular(unordered_pair(X0,X1)) = x
| x = not_subclass_element(unordered_pair(y,x),unordered_pair(X0,X1))
| subclass(unordered_pair(y,x),unordered_pair(X0,X1))
| member(y,unordered_pair(y,x)) ),
inference(paramodulation,[status(thm)],[f4865,f111]) ).
fof(f5424,plain,
! [X0,X1] :
( ~ sQ102_spl
| not_subclass_element(unordered_pair(y,x),unordered_pair(X0,X1)) = x
| y != x
| not_subclass_element(unordered_pair(X0,X1),unordered_pair(y,x)) = X1
| X0 = not_subclass_element(unordered_pair(X0,X1),unordered_pair(y,x))
| regular(unordered_pair(X0,X1)) = x ),
inference(equality_factoring,[status(thm)],[f4865]) ).
fof(f5427,definition,
! [X0,X1] :
( sQ199_spl
<=> ( not_subclass_element(unordered_pair(y,x),unordered_pair(X0,X1)) = x
| not_subclass_element(unordered_pair(X0,X1),unordered_pair(y,x)) = X1
| X0 = not_subclass_element(unordered_pair(X0,X1),unordered_pair(y,x))
| regular(unordered_pair(X0,X1)) = x ) ),
introduced(definition,[new_symbols(definition,[sQ199_spl])],[split_symbol_definition]) ).
fof(f5430,plain,
( ~ sQ102_spl
| ~ sQ35_spl
| sQ199_spl ),
inference(split_clause,[status(thm)],[f5424,f5427,f794,f2593]) ).
fof(f5436,definition,
! [X0,X1] :
( sQ201_spl
<=> ( not_subclass_element(unordered_pair(X0,X1),unordered_pair(y,x)) = X1
| X0 = not_subclass_element(unordered_pair(X0,X1),unordered_pair(y,x))
| regular(unordered_pair(X0,X1)) = x
| x = not_subclass_element(unordered_pair(y,x),unordered_pair(X0,X1))
| subclass(unordered_pair(y,x),unordered_pair(X0,X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ201_spl])],[split_symbol_definition]) ).
fof(f5439,plain,
( ~ sQ102_spl
| sQ201_spl
| sQ33_spl ),
inference(split_clause,[status(thm)],[f5422,f752,f5436,f2593]) ).
fof(f5445,definition,
! [X0,X1] :
( sQ202_spl
<=> ( not_subclass_element(unordered_pair(X0,X1),unordered_pair(y,x)) = X1
| X0 = not_subclass_element(unordered_pair(X0,X1),unordered_pair(y,x))
| regular(unordered_pair(X0,X1)) = x
| x = not_subclass_element(unordered_pair(y,x),unordered_pair(X0,X1))
| unordered_pair(y,x) = unordered_pair(X0,X1)
| member(not_subclass_element(unordered_pair(X0,X1),unordered_pair(y,x)),unordered_pair(X0,X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ202_spl])],[split_symbol_definition]) ).
fof(f5448,plain,
( ~ sQ102_spl
| sQ33_spl
| sQ202_spl ),
inference(split_clause,[status(thm)],[f5420,f5445,f752,f2593]) ).
fof(f5449,definition,
! [X0,X1] :
( sQ203_spl
<=> ( regular(unordered_pair(X0,X1)) = X1
| regular(unordered_pair(X0,X1)) = X0
| not_subclass_element(unordered_pair(X0,X1),unordered_pair(y,x)) = X1
| X0 = not_subclass_element(unordered_pair(X0,X1),unordered_pair(y,x))
| regular(unordered_pair(X0,X1)) = x
| x = not_subclass_element(unordered_pair(y,x),unordered_pair(X0,X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ203_spl])],[split_symbol_definition]) ).
fof(f5452,plain,
( ~ sQ102_spl
| sQ9_spl
| sQ203_spl ),
inference(split_clause,[status(thm)],[f5414,f5449,f466,f2593]) ).
fof(f5463,definition,
! [X0,X1] :
( sQ204_spl
<=> ( not_subclass_element(unordered_pair(X0,X1),unordered_pair(y,x)) = X1
| X0 = not_subclass_element(unordered_pair(X0,X1),unordered_pair(y,x))
| regular(unordered_pair(X0,X1)) = x
| x = not_subclass_element(unordered_pair(y,x),unordered_pair(X0,X1))
| unordered_pair(y,x) = unordered_pair(X0,X1)
| not_subclass_element(unordered_pair(X0,X1),unordered_pair(y,x)) = X1
| not_subclass_element(unordered_pair(X0,X1),unordered_pair(y,x)) = X0 ) ),
introduced(definition,[new_symbols(definition,[sQ204_spl])],[split_symbol_definition]) ).
fof(f5466,plain,
( ~ sQ102_spl
| sQ204_spl
| sQ33_spl ),
inference(split_clause,[status(thm)],[f5418,f752,f5463,f2593]) ).
fof(f5467,definition,
! [X0,X1] :
( sQ205_spl
<=> ( X1 = not_subclass_element(unordered_pair(X0,X1),null_class)
| not_subclass_element(unordered_pair(X0,X1),null_class) = X0
| not_subclass_element(unordered_pair(X0,X1),unordered_pair(y,x)) = X1
| X0 = not_subclass_element(unordered_pair(X0,X1),unordered_pair(y,x))
| regular(unordered_pair(X0,X1)) = x
| x = not_subclass_element(unordered_pair(y,x),unordered_pair(X0,X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ205_spl])],[split_symbol_definition]) ).
fof(f5470,plain,
( ~ sQ102_spl
| sQ9_spl
| sQ205_spl ),
inference(split_clause,[status(thm)],[f5415,f5467,f466,f2593]) ).
fof(f5615,plain,
! [X0] :
( ~ sQ67_spl
| ~ sQ134_spl
| ~ subclass(X0,y)
| ~ member(x,X0) ),
inference(resolution,[status(thm)],[f5156,f110]) ).
fof(f5764,plain,
! [X0] :
( ~ sQ103_spl
| not_subclass_element(unordered_pair(y,x),singleton(X0)) = x
| y = regular(singleton(X0))
| not_subclass_element(unordered_pair(y,x),singleton(X0)) = y
| X0 = not_subclass_element(singleton(X0),unordered_pair(y,x)) ),
inference(paramodulation,[status(thm)],[f377,f2597]) ).
fof(f5870,plain,
! [X0,X1,X2,X3,X4] :
( member(ordered_pair(X1,X0),X2)
| ~ subclass(complement(X2),cross_product(X3,X4))
| member(X0,unordered_pair(X1,X0)) ),
inference(resolution,[status(thm)],[f1367,f1437]) ).
fof(f5879,plain,
( ~ sQ29_spl
| ~ sQ134_spl
| ~ inductive(y)
| ~ member(y,omega) ),
inference(resolution,[status(thm)],[f5402,f168]) ).
fof(f5883,definition,
( sQ213_spl
<=> inductive(y) ),
introduced(definition,[new_symbols(definition,[sQ213_spl])],[split_symbol_definition]) ).
fof(f5886,plain,
( ~ sQ29_spl
| ~ sQ134_spl
| ~ sQ213_spl
| ~ sQ136_spl ),
inference(split_clause,[status(thm)],[f5879,f3347,f5883,f3221,f686]) ).
fof(f5893,plain,
( ~ sQ67_spl
| ~ sQ134_spl
| ~ inductive(y)
| ~ member(x,omega) ),
inference(resolution,[status(thm)],[f5615,f168]) ).
fof(f5897,plain,
( ~ sQ67_spl
| ~ sQ134_spl
| ~ sQ213_spl
| ~ sQ142_spl ),
inference(split_clause,[status(thm)],[f5893,f3464,f5883,f3221,f1393]) ).
fof(f6126,plain,
( ~ sQ118_spl
| null_class = unordered_pair(y,x)
| ~ member(regular(unordered_pair(y,x)),y) ),
inference(resolution,[status(thm)],[f3123,f183]) ).
fof(f6127,plain,
( ~ sQ118_spl
| unordered_pair(y,x) = null_class
| ~ member(apply(choice,unordered_pair(y,x)),y) ),
inference(resolution,[status(thm)],[f3123,f2082]) ).
fof(f6128,plain,
( ~ sQ118_spl
| ~ inductive(unordered_pair(y,x))
| ~ member(null_class,y) ),
inference(resolution,[status(thm)],[f3123,f164]) ).
fof(f6134,plain,
( ~ sQ118_spl
| unordered_pair(y,x) = null_class
| ~ member(not_subclass_element(unordered_pair(y,x),null_class),y) ),
inference(resolution,[status(thm)],[f3123,f233]) ).
fof(f6138,plain,
! [X0] :
( ~ sQ118_spl
| ~ member(x,X0)
| ~ member(x,y) ),
inference(resolution,[status(thm)],[f3123,f1447]) ).
fof(f6139,plain,
! [X0] :
( ~ sQ118_spl
| ~ member(y,X0)
| ~ member(y,y) ),
inference(resolution,[status(thm)],[f3123,f1448]) ).
fof(f6147,plain,
( ~ sQ118_spl
| sQ117_spl
| ~ sQ184_spl ),
inference(split_clause,[status(thm)],[f6139,f5180,f3002,f3036]) ).
fof(f6149,definition,
( sQ218_spl
<=> member(apply(choice,unordered_pair(y,x)),y) ),
introduced(definition,[new_symbols(definition,[sQ218_spl])],[split_symbol_definition]) ).
fof(f6152,plain,
( ~ sQ118_spl
| sQ15_spl
| ~ sQ218_spl ),
inference(split_clause,[status(thm)],[f6127,f6149,f504,f3036]) ).
fof(f6153,plain,
( ~ sQ118_spl
| ~ sQ64_spl
| ~ sQ189_spl ),
inference(split_clause,[status(thm)],[f6128,f5201,f1280,f3036]) ).
fof(f6155,plain,
( ~ sQ118_spl
| sQ128_spl
| ~ sQ188_spl ),
inference(split_clause,[status(thm)],[f6138,f5197,f3173,f3036]) ).
fof(f6156,definition,
( sQ219_spl
<=> member(not_subclass_element(unordered_pair(y,x),null_class),y) ),
introduced(definition,[new_symbols(definition,[sQ219_spl])],[split_symbol_definition]) ).
fof(f6158,plain,
( sQ219_spl
| ~ member(not_subclass_element(unordered_pair(y,x),null_class),y) ),
inference(component_clause,[status(thm)],[f6156]) ).
fof(f6159,plain,
( ~ sQ118_spl
| sQ15_spl
| ~ sQ219_spl ),
inference(split_clause,[status(thm)],[f6134,f6156,f504,f3036]) ).
fof(f6160,definition,
( sQ220_spl
<=> member(regular(unordered_pair(y,x)),y) ),
introduced(definition,[new_symbols(definition,[sQ220_spl])],[split_symbol_definition]) ).
fof(f6162,plain,
( sQ220_spl
| ~ member(regular(unordered_pair(y,x)),y) ),
inference(component_clause,[status(thm)],[f6160]) ).
fof(f6163,plain,
( ~ sQ118_spl
| sQ15_spl
| ~ sQ220_spl ),
inference(split_clause,[status(thm)],[f6126,f6160,f504,f3036]) ).
fof(f6209,plain,
! [X0,X1] :
( sQ8_spl
| regular(unordered_pair(X0,X1)) = X1
| regular(unordered_pair(X0,X1)) = X0
| y = not_subclass_element(unordered_pair(x,y),unordered_pair(X0,X1))
| null_class != null_class
| not_subclass_element(unordered_pair(X0,X1),unordered_pair(x,y)) = X0
| not_subclass_element(unordered_pair(X0,X1),unordered_pair(x,y)) = X1
| x = not_subclass_element(unordered_pair(x,y),unordered_pair(X0,X1)) ),
inference(paramodulation,[status(thm)],[f2524,f4863]) ).
fof(f6210,plain,
! [X0,X1] :
( sQ8_spl
| X1 = not_subclass_element(unordered_pair(X0,X1),null_class)
| not_subclass_element(unordered_pair(X0,X1),null_class) = X0
| y = not_subclass_element(unordered_pair(x,y),unordered_pair(X0,X1))
| null_class != null_class
| not_subclass_element(unordered_pair(X0,X1),unordered_pair(x,y)) = X0
| not_subclass_element(unordered_pair(X0,X1),unordered_pair(x,y)) = X1
| x = not_subclass_element(unordered_pair(x,y),unordered_pair(X0,X1)) ),
inference(paramodulation,[status(thm)],[f276,f4863]) ).
fof(f6220,definition,
! [X0,X1] :
( sQ221_spl
<=> ( regular(unordered_pair(X0,X1)) = X1
| regular(unordered_pair(X0,X1)) = X0
| y = not_subclass_element(unordered_pair(x,y),unordered_pair(X0,X1))
| not_subclass_element(unordered_pair(X0,X1),unordered_pair(x,y)) = X0
| not_subclass_element(unordered_pair(X0,X1),unordered_pair(x,y)) = X1
| x = not_subclass_element(unordered_pair(x,y),unordered_pair(X0,X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ221_spl])],[split_symbol_definition]) ).
fof(f6223,plain,
( sQ8_spl
| ~ sQ3_spl
| sQ221_spl ),
inference(split_clause,[status(thm)],[f6209,f6220,f288,f463]) ).
fof(f6224,definition,
! [X0,X1] :
( sQ222_spl
<=> ( X1 = not_subclass_element(unordered_pair(X0,X1),null_class)
| not_subclass_element(unordered_pair(X0,X1),null_class) = X0
| y = not_subclass_element(unordered_pair(x,y),unordered_pair(X0,X1))
| not_subclass_element(unordered_pair(X0,X1),unordered_pair(x,y)) = X0
| not_subclass_element(unordered_pair(X0,X1),unordered_pair(x,y)) = X1
| x = not_subclass_element(unordered_pair(x,y),unordered_pair(X0,X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ222_spl])],[split_symbol_definition]) ).
fof(f6227,plain,
( sQ8_spl
| ~ sQ3_spl
| sQ222_spl ),
inference(split_clause,[status(thm)],[f6210,f6224,f288,f463]) ).
fof(f6353,plain,
! [X0] :
( sQ187_spl
| ~ sQ25_spl
| ~ subclass(X0,y)
| ~ member(x,X0) ),
inference(resolution,[status(thm)],[f5205,f110]) ).
fof(f6374,plain,
! [X0] :
( ~ sQ15_spl
| member(x,null_class)
| ~ member(x,X0) ),
inference(paramodulation,[status(thm)],[f505,f1447]) ).
fof(f6431,plain,
( ~ sQ15_spl
| sQ17_spl
| sQ128_spl ),
inference(split_clause,[status(thm)],[f6374,f3173,f510,f504]) ).
fof(f6463,plain,
( sQ219_spl
| ~ sQ10_spl
| ~ member(x,y) ),
inference(backward_demodulation,[status(thm)],[f470,f6158]) ).
fof(f6465,plain,
( sQ220_spl
| ~ sQ102_spl
| ~ member(x,y) ),
inference(backward_demodulation,[status(thm)],[f2594,f6162]) ).
fof(f6500,plain,
( sQ187_spl
| ~ sQ25_spl
| ~ inductive(y)
| ~ member(x,omega) ),
inference(resolution,[status(thm)],[f6353,f168]) ).
fof(f6504,plain,
( sQ187_spl
| ~ sQ25_spl
| ~ sQ213_spl
| ~ sQ142_spl ),
inference(split_clause,[status(thm)],[f6500,f3464,f5883,f636,f5193]) ).
fof(f6591,plain,
! [X0] :
( ~ sQ10_spl
| not_subclass_element(singleton(X0),unordered_pair(y,x)) = X0
| y = not_subclass_element(unordered_pair(y,x),singleton(X0))
| x = not_subclass_element(unordered_pair(y,x),singleton(X0))
| not_subclass_element(singleton(X0),null_class) = x ),
inference(paramodulation,[status(thm)],[f377,f470]) ).
fof(f6592,plain,
! [X0,X1] :
( ~ sQ10_spl
| not_subclass_element(unordered_pair(y,x),unordered_pair(X1,X0)) = y
| X1 = not_subclass_element(unordered_pair(X1,X0),unordered_pair(y,x))
| not_subclass_element(unordered_pair(y,x),unordered_pair(X1,X0)) = x
| not_subclass_element(unordered_pair(X1,X0),null_class) = x
| X0 = not_subclass_element(unordered_pair(X1,X0),unordered_pair(y,x)) ),
inference(paramodulation,[status(thm)],[f378,f470]) ).
fof(f6597,plain,
( ~ sQ10_spl
| member(x,unordered_pair(y,x))
| unordered_pair(y,x) = null_class ),
inference(paramodulation,[status(thm)],[f470,f233]) ).
fof(f6610,plain,
( ~ sQ10_spl
| sQ19_spl
| sQ15_spl ),
inference(split_clause,[status(thm)],[f6597,f504,f517,f469]) ).
fof(f6642,plain,
! [X0] :
( sQ33_spl
| ~ member(y,X0) ),
inference(resolution,[status(thm)],[f754,f1448]) ).
fof(f6652,plain,
( sQ33_spl
| sQ117_spl ),
inference(split_clause,[status(thm)],[f6642,f3002,f752]) ).
fof(f6655,plain,
( sQ186_spl
| ~ sQ105_spl
| ~ member(x,y) ),
inference(forward_demodulation,[status(thm)],[f2606,f5190]) ).
fof(f6708,plain,
! [X0] :
( sQ219_spl
| ~ sQ10_spl
| ~ subclass(X0,y)
| ~ member(x,X0) ),
inference(resolution,[status(thm)],[f6463,f110]) ).
fof(f6805,plain,
( ~ sQ178_spl
| not_subclass_element(unordered_pair(y,x),unordered_pair(x,y)) = x
| ~ member(x,unordered_pair(y,x))
| y = not_subclass_element(unordered_pair(y,x),unordered_pair(x,y))
| unordered_pair(x,y) = unordered_pair(y,x) ),
inference(paramodulation,[status(thm)],[f4937,f339]) ).
fof(f6806,plain,
( ~ sQ178_spl
| unordered_pair(x,y) = unordered_pair(y,x)
| not_subclass_element(unordered_pair(y,x),unordered_pair(x,y)) = x
| not_subclass_element(unordered_pair(y,x),unordered_pair(x,y)) = y
| member(x,unordered_pair(x,y)) ),
inference(paramodulation,[status(thm)],[f4937,f251]) ).
fof(f6807,plain,
( ~ sQ178_spl
| unordered_pair(y,x) = unordered_pair(x,y)
| ~ member(x,unordered_pair(y,x))
| ~ member(not_subclass_element(unordered_pair(y,x),unordered_pair(x,y)),unordered_pair(x,y)) ),
inference(paramodulation,[status(thm)],[f4937,f228]) ).
fof(f6809,plain,
( ~ sQ178_spl
| unordered_pair(x,y) = unordered_pair(y,x)
| ~ member(x,unordered_pair(y,x))
| member(not_subclass_element(unordered_pair(y,x),unordered_pair(x,y)),unordered_pair(y,x)) ),
inference(paramodulation,[status(thm)],[f4937,f226]) ).
fof(f6810,plain,
( ~ sQ178_spl
| subclass(unordered_pair(x,y),unordered_pair(y,x))
| member(x,unordered_pair(x,y)) ),
inference(paramodulation,[status(thm)],[f4937,f111]) ).
fof(f6811,plain,
( ~ sQ178_spl
| ~ member(x,unordered_pair(y,x))
| subclass(unordered_pair(x,y),unordered_pair(y,x)) ),
inference(paramodulation,[status(thm)],[f4937,f112]) ).
fof(f6812,definition,
( sQ223_spl
<=> unordered_pair(x,y) = unordered_pair(y,x) ),
introduced(definition,[new_symbols(definition,[sQ223_spl])],[split_symbol_definition]) ).
fof(f6813,plain,
( ~ sQ223_spl
| unordered_pair(x,y) = unordered_pair(y,x) ),
inference(component_clause,[status(thm)],[f6812]) ).
fof(f6815,plain,
( ~ sQ178_spl
| sQ181_spl
| ~ sQ19_spl
| sQ180_spl
| sQ223_spl ),
inference(split_clause,[status(thm)],[f6805,f6812,f4942,f517,f4945,f4936]) ).
fof(f6821,definition,
( sQ225_spl
<=> member(not_subclass_element(unordered_pair(y,x),unordered_pair(x,y)),unordered_pair(y,x)) ),
introduced(definition,[new_symbols(definition,[sQ225_spl])],[split_symbol_definition]) ).
fof(f6822,plain,
( ~ sQ225_spl
| member(not_subclass_element(unordered_pair(y,x),unordered_pair(x,y)),unordered_pair(y,x)) ),
inference(component_clause,[status(thm)],[f6821]) ).
fof(f6824,plain,
( ~ sQ178_spl
| sQ223_spl
| ~ sQ19_spl
| sQ225_spl ),
inference(split_clause,[status(thm)],[f6809,f6821,f517,f6812,f4936]) ).
fof(f6825,definition,
( sQ226_spl
<=> subclass(unordered_pair(x,y),unordered_pair(y,x)) ),
introduced(definition,[new_symbols(definition,[sQ226_spl])],[split_symbol_definition]) ).
fof(f6826,plain,
( ~ sQ226_spl
| subclass(unordered_pair(x,y),unordered_pair(y,x)) ),
inference(component_clause,[status(thm)],[f6825]) ).
fof(f6827,plain,
( sQ226_spl
| ~ subclass(unordered_pair(x,y),unordered_pair(y,x)) ),
inference(component_clause,[status(thm)],[f6825]) ).
fof(f6828,plain,
( ~ sQ178_spl
| sQ226_spl
| sQ67_spl ),
inference(split_clause,[status(thm)],[f6810,f1393,f6825,f4936]) ).
fof(f6829,plain,
( ~ sQ178_spl
| sQ223_spl
| sQ181_spl
| sQ180_spl
| sQ67_spl ),
inference(split_clause,[status(thm)],[f6806,f1393,f4942,f4945,f6812,f4936]) ).
fof(f6830,definition,
( sQ227_spl
<=> member(not_subclass_element(unordered_pair(y,x),unordered_pair(x,y)),unordered_pair(x,y)) ),
introduced(definition,[new_symbols(definition,[sQ227_spl])],[split_symbol_definition]) ).
fof(f6832,plain,
( sQ227_spl
| ~ member(not_subclass_element(unordered_pair(y,x),unordered_pair(x,y)),unordered_pair(x,y)) ),
inference(component_clause,[status(thm)],[f6830]) ).
fof(f6833,plain,
( ~ sQ178_spl
| sQ223_spl
| ~ sQ19_spl
| ~ sQ227_spl ),
inference(split_clause,[status(thm)],[f6807,f6830,f517,f6812,f4936]) ).
fof(f6837,plain,
( ~ sQ178_spl
| ~ sQ19_spl
| sQ226_spl ),
inference(split_clause,[status(thm)],[f6811,f6825,f517,f4936]) ).
fof(f6838,plain,
( ~ sQ223_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6813,f235]) ).
fof(f6839,plain,
~ sQ223_spl,
inference(contradiction_clause,[status(thm)],[f6838]) ).
fof(f6841,plain,
( sQ227_spl
| ~ sQ181_spl
| ~ member(x,unordered_pair(x,y)) ),
inference(backward_demodulation,[status(thm)],[f4946,f6832]) ).
fof(f6843,plain,
( sQ227_spl
| ~ sQ181_spl
| ~ sQ67_spl ),
inference(split_clause,[status(thm)],[f6841,f1393,f4945,f6830]) ).
fof(f6934,plain,
( sQ219_spl
| ~ sQ10_spl
| ~ inductive(y)
| ~ member(x,omega) ),
inference(resolution,[status(thm)],[f6708,f168]) ).
fof(f6938,plain,
( sQ219_spl
| ~ sQ10_spl
| ~ sQ213_spl
| ~ sQ142_spl ),
inference(split_clause,[status(thm)],[f6934,f3464,f5883,f469,f6156]) ).
fof(f6991,plain,
! [X0] :
( sQ186_spl
| ~ sQ105_spl
| ~ member(x,X0)
| ~ subclass(X0,y) ),
inference(resolution,[status(thm)],[f6655,f110]) ).
fof(f7053,plain,
( sQ186_spl
| ~ sQ105_spl
| ~ inductive(y)
| ~ member(x,omega) ),
inference(resolution,[status(thm)],[f6991,f168]) ).
fof(f7057,plain,
( sQ186_spl
| ~ sQ105_spl
| ~ sQ213_spl
| ~ sQ142_spl ),
inference(split_clause,[status(thm)],[f7053,f3464,f5883,f2605,f5188]) ).
fof(f7058,plain,
! [X0] :
( sQ188_spl
| ~ member(x,X0)
| ~ subclass(X0,y) ),
inference(resolution,[status(thm)],[f5199,f110]) ).
fof(f7077,plain,
( sQ188_spl
| ~ inductive(y)
| ~ member(x,omega) ),
inference(resolution,[status(thm)],[f7058,f168]) ).
fof(f7081,plain,
( sQ188_spl
| ~ sQ213_spl
| ~ sQ142_spl ),
inference(split_clause,[status(thm)],[f7077,f3464,f5883,f5197]) ).
fof(f7143,plain,
! [X0] :
( sQ220_spl
| ~ sQ102_spl
| ~ member(x,X0)
| ~ subclass(X0,y) ),
inference(resolution,[status(thm)],[f6465,f110]) ).
fof(f7525,plain,
( sQ220_spl
| ~ sQ102_spl
| ~ inductive(y)
| ~ member(x,omega) ),
inference(resolution,[status(thm)],[f7143,f168]) ).
fof(f7530,plain,
( sQ220_spl
| ~ sQ102_spl
| ~ sQ213_spl
| ~ sQ142_spl ),
inference(split_clause,[status(thm)],[f7525,f3464,f5883,f2593,f6160]) ).
fof(f7842,plain,
! [X0,X1] :
( ~ sQ10_spl
| regular(unordered_pair(X1,X0)) = X0
| regular(unordered_pair(X1,X0)) = X1
| not_subclass_element(unordered_pair(y,x),null_class) = y
| X1 = not_subclass_element(unordered_pair(X1,X0),unordered_pair(y,x))
| not_subclass_element(unordered_pair(y,x),unordered_pair(X1,X0)) = x
| not_subclass_element(unordered_pair(X1,X0),null_class) = x
| X0 = not_subclass_element(unordered_pair(X1,X0),unordered_pair(y,x)) ),
inference(paramodulation,[status(thm)],[f2524,f6592]) ).
fof(f7843,plain,
! [X0,X1] :
( ~ sQ10_spl
| X0 = not_subclass_element(unordered_pair(X1,X0),null_class)
| not_subclass_element(unordered_pair(X1,X0),null_class) = X1
| not_subclass_element(unordered_pair(y,x),null_class) = y
| X1 = not_subclass_element(unordered_pair(X1,X0),unordered_pair(y,x))
| not_subclass_element(unordered_pair(y,x),unordered_pair(X1,X0)) = x
| not_subclass_element(unordered_pair(X1,X0),null_class) = x
| X0 = not_subclass_element(unordered_pair(X1,X0),unordered_pair(y,x)) ),
inference(paramodulation,[status(thm)],[f276,f6592]) ).
fof(f7846,plain,
! [X0,X1] :
( ~ sQ10_spl
| X0 = not_subclass_element(unordered_pair(X0,X1),unordered_pair(y,x))
| not_subclass_element(unordered_pair(y,x),unordered_pair(X0,X1)) = x
| not_subclass_element(unordered_pair(X0,X1),null_class) = x
| X1 = not_subclass_element(unordered_pair(X0,X1),unordered_pair(y,x))
| unordered_pair(y,x) = unordered_pair(X0,X1)
| not_subclass_element(unordered_pair(X0,X1),unordered_pair(y,x)) = X1
| not_subclass_element(unordered_pair(X0,X1),unordered_pair(y,x)) = X0
| member(y,unordered_pair(y,x)) ),
inference(paramodulation,[status(thm)],[f6592,f251]) ).
fof(f7848,plain,
! [X0,X1] :
( ~ sQ10_spl
| X0 = not_subclass_element(unordered_pair(X0,X1),unordered_pair(y,x))
| not_subclass_element(unordered_pair(y,x),unordered_pair(X0,X1)) = x
| not_subclass_element(unordered_pair(X0,X1),null_class) = x
| X1 = not_subclass_element(unordered_pair(X0,X1),unordered_pair(y,x))
| unordered_pair(y,x) = unordered_pair(X0,X1)
| member(y,unordered_pair(y,x))
| member(not_subclass_element(unordered_pair(X0,X1),unordered_pair(y,x)),unordered_pair(X0,X1)) ),
inference(paramodulation,[status(thm)],[f6592,f225]) ).
fof(f7850,plain,
! [X0,X1] :
( ~ sQ10_spl
| X0 = not_subclass_element(unordered_pair(X0,X1),unordered_pair(y,x))
| not_subclass_element(unordered_pair(y,x),unordered_pair(X0,X1)) = x
| not_subclass_element(unordered_pair(X0,X1),null_class) = x
| X1 = not_subclass_element(unordered_pair(X0,X1),unordered_pair(y,x))
| subclass(unordered_pair(y,x),unordered_pair(X0,X1))
| member(y,unordered_pair(y,x)) ),
inference(paramodulation,[status(thm)],[f6592,f111]) ).
fof(f7853,plain,
! [X0,X1] :
( ~ sQ10_spl
| not_subclass_element(unordered_pair(y,x),unordered_pair(X1,X0)) = x
| y != x
| X1 = not_subclass_element(unordered_pair(X1,X0),unordered_pair(y,x))
| not_subclass_element(unordered_pair(X1,X0),null_class) = x
| X0 = not_subclass_element(unordered_pair(X1,X0),unordered_pair(y,x)) ),
inference(equality_factoring,[status(thm)],[f6592]) ).
fof(f7856,definition,
! [X0,X1] :
( sQ241_spl
<=> ( X0 = not_subclass_element(unordered_pair(X0,X1),unordered_pair(y,x))
| not_subclass_element(unordered_pair(y,x),unordered_pair(X0,X1)) = x
| not_subclass_element(unordered_pair(X0,X1),null_class) = x
| X1 = not_subclass_element(unordered_pair(X0,X1),unordered_pair(y,x))
| unordered_pair(y,x) = unordered_pair(X0,X1)
| member(not_subclass_element(unordered_pair(X0,X1),unordered_pair(y,x)),unordered_pair(X0,X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ241_spl])],[split_symbol_definition]) ).
fof(f7859,plain,
( ~ sQ10_spl
| sQ33_spl
| sQ241_spl ),
inference(split_clause,[status(thm)],[f7848,f7856,f752,f469]) ).
fof(f7860,definition,
! [X0,X1] :
( sQ242_spl
<=> ( regular(unordered_pair(X1,X0)) = X0
| regular(unordered_pair(X1,X0)) = X1
| X1 = not_subclass_element(unordered_pair(X1,X0),unordered_pair(y,x))
| not_subclass_element(unordered_pair(y,x),unordered_pair(X1,X0)) = x
| not_subclass_element(unordered_pair(X1,X0),null_class) = x
| X0 = not_subclass_element(unordered_pair(X1,X0),unordered_pair(y,x)) ) ),
introduced(definition,[new_symbols(definition,[sQ242_spl])],[split_symbol_definition]) ).
fof(f7863,plain,
( ~ sQ10_spl
| sQ9_spl
| sQ242_spl ),
inference(split_clause,[status(thm)],[f7842,f7860,f466,f469]) ).
fof(f7877,definition,
! [X0,X1] :
( sQ244_spl
<=> ( X0 = not_subclass_element(unordered_pair(X0,X1),unordered_pair(y,x))
| not_subclass_element(unordered_pair(y,x),unordered_pair(X0,X1)) = x
| not_subclass_element(unordered_pair(X0,X1),null_class) = x
| X1 = not_subclass_element(unordered_pair(X0,X1),unordered_pair(y,x))
| unordered_pair(y,x) = unordered_pair(X0,X1)
| not_subclass_element(unordered_pair(X0,X1),unordered_pair(y,x)) = X1
| not_subclass_element(unordered_pair(X0,X1),unordered_pair(y,x)) = X0 ) ),
introduced(definition,[new_symbols(definition,[sQ244_spl])],[split_symbol_definition]) ).
fof(f7880,plain,
( ~ sQ10_spl
| sQ244_spl
| sQ33_spl ),
inference(split_clause,[status(thm)],[f7846,f752,f7877,f469]) ).
fof(f7881,definition,
! [X0,X1] :
( sQ245_spl
<=> ( X0 = not_subclass_element(unordered_pair(X0,X1),unordered_pair(y,x))
| not_subclass_element(unordered_pair(y,x),unordered_pair(X0,X1)) = x
| not_subclass_element(unordered_pair(X0,X1),null_class) = x
| X1 = not_subclass_element(unordered_pair(X0,X1),unordered_pair(y,x))
| subclass(unordered_pair(y,x),unordered_pair(X0,X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ245_spl])],[split_symbol_definition]) ).
fof(f7884,plain,
( ~ sQ10_spl
| sQ245_spl
| sQ33_spl ),
inference(split_clause,[status(thm)],[f7850,f752,f7881,f469]) ).
fof(f7885,definition,
! [X0,X1] :
( sQ246_spl
<=> ( not_subclass_element(unordered_pair(y,x),unordered_pair(X1,X0)) = x
| X1 = not_subclass_element(unordered_pair(X1,X0),unordered_pair(y,x))
| not_subclass_element(unordered_pair(X1,X0),null_class) = x
| X0 = not_subclass_element(unordered_pair(X1,X0),unordered_pair(y,x)) ) ),
introduced(definition,[new_symbols(definition,[sQ246_spl])],[split_symbol_definition]) ).
fof(f7888,plain,
( ~ sQ10_spl
| ~ sQ35_spl
| sQ246_spl ),
inference(split_clause,[status(thm)],[f7853,f7885,f794,f469]) ).
fof(f7889,definition,
! [X0,X1] :
( sQ247_spl
<=> ( X0 = not_subclass_element(unordered_pair(X1,X0),null_class)
| not_subclass_element(unordered_pair(X1,X0),null_class) = X1
| X1 = not_subclass_element(unordered_pair(X1,X0),unordered_pair(y,x))
| not_subclass_element(unordered_pair(y,x),unordered_pair(X1,X0)) = x
| not_subclass_element(unordered_pair(X1,X0),null_class) = x
| X0 = not_subclass_element(unordered_pair(X1,X0),unordered_pair(y,x)) ) ),
introduced(definition,[new_symbols(definition,[sQ247_spl])],[split_symbol_definition]) ).
fof(f7892,plain,
( ~ sQ10_spl
| sQ9_spl
| sQ247_spl ),
inference(split_clause,[status(thm)],[f7843,f7889,f466,f469]) ).
fof(f7907,plain,
( ~ sQ154_spl
| null_class = unordered_pair(y,x)
| ~ member(regular(unordered_pair(y,x)),x) ),
inference(resolution,[status(thm)],[f5016,f183]) ).
fof(f7908,plain,
( ~ sQ154_spl
| unordered_pair(y,x) = null_class
| ~ member(apply(choice,unordered_pair(y,x)),x) ),
inference(resolution,[status(thm)],[f5016,f2082]) ).
fof(f7909,plain,
( ~ sQ154_spl
| ~ inductive(unordered_pair(y,x))
| ~ member(null_class,x) ),
inference(resolution,[status(thm)],[f5016,f164]) ).
fof(f7917,plain,
( ~ sQ154_spl
| unordered_pair(y,x) = null_class
| ~ member(not_subclass_element(unordered_pair(y,x),null_class),x) ),
inference(resolution,[status(thm)],[f5016,f233]) ).
fof(f7921,plain,
! [X0] :
( ~ sQ154_spl
| ~ member(x,X0)
| ~ member(x,x) ),
inference(resolution,[status(thm)],[f5016,f1447]) ).
fof(f7922,plain,
! [X0] :
( ~ sQ154_spl
| ~ member(y,X0)
| ~ member(y,x) ),
inference(resolution,[status(thm)],[f5016,f1448]) ).
fof(f7934,definition,
( sQ249_spl
<=> member(regular(unordered_pair(y,x)),x) ),
introduced(definition,[new_symbols(definition,[sQ249_spl])],[split_symbol_definition]) ).
fof(f7937,plain,
( ~ sQ154_spl
| sQ15_spl
| ~ sQ249_spl ),
inference(split_clause,[status(thm)],[f7907,f7934,f504,f3955]) ).
fof(f7938,definition,
( sQ250_spl
<=> member(y,x) ),
introduced(definition,[new_symbols(definition,[sQ250_spl])],[split_symbol_definition]) ).
fof(f7940,plain,
( sQ250_spl
| ~ member(y,x) ),
inference(component_clause,[status(thm)],[f7938]) ).
fof(f7941,plain,
( ~ sQ154_spl
| sQ117_spl
| ~ sQ250_spl ),
inference(split_clause,[status(thm)],[f7922,f7938,f3002,f3955]) ).
fof(f7942,plain,
( ~ sQ154_spl
| sQ128_spl
| ~ sQ127_spl ),
inference(split_clause,[status(thm)],[f7921,f3170,f3173,f3955]) ).
fof(f7943,definition,
( sQ251_spl
<=> member(apply(choice,unordered_pair(y,x)),x) ),
introduced(definition,[new_symbols(definition,[sQ251_spl])],[split_symbol_definition]) ).
fof(f7946,plain,
( ~ sQ154_spl
| sQ15_spl
| ~ sQ251_spl ),
inference(split_clause,[status(thm)],[f7908,f7943,f504,f3955]) ).
fof(f7948,plain,
( ~ sQ154_spl
| ~ sQ64_spl
| ~ sQ125_spl ),
inference(split_clause,[status(thm)],[f7909,f3163,f1280,f3955]) ).
fof(f7949,definition,
( sQ252_spl
<=> member(not_subclass_element(unordered_pair(y,x),null_class),x) ),
introduced(definition,[new_symbols(definition,[sQ252_spl])],[split_symbol_definition]) ).
fof(f7952,plain,
( ~ sQ154_spl
| sQ15_spl
| ~ sQ252_spl ),
inference(split_clause,[status(thm)],[f7917,f7949,f504,f3955]) ).
fof(f7990,plain,
! [X0] :
( ~ sQ112_spl
| ~ member(y,X0)
| ~ member(y,x) ),
inference(resolution,[status(thm)],[f2980,f1447]) ).
fof(f8004,plain,
( ~ sQ112_spl
| sQ117_spl
| ~ sQ250_spl ),
inference(split_clause,[status(thm)],[f7990,f7938,f3002,f2787]) ).
fof(f8013,plain,
( ~ sQ226_spl
| x = not_subclass_element(unordered_pair(y,x),unordered_pair(x,y))
| y = not_subclass_element(unordered_pair(y,x),unordered_pair(x,y))
| unordered_pair(y,x) = unordered_pair(x,y) ),
inference(resolution,[status(thm)],[f6826,f2018]) ).
fof(f8017,plain,
( ~ sQ226_spl
| unordered_pair(y,x) = unordered_pair(x,y)
| ~ subclass(unordered_pair(y,x),unordered_pair(x,y)) ),
inference(resolution,[status(thm)],[f6826,f116]) ).
fof(f8036,definition,
( sQ253_spl
<=> subclass(unordered_pair(y,x),unordered_pair(x,y)) ),
introduced(definition,[new_symbols(definition,[sQ253_spl])],[split_symbol_definition]) ).
fof(f8038,plain,
( sQ253_spl
| ~ subclass(unordered_pair(y,x),unordered_pair(x,y)) ),
inference(component_clause,[status(thm)],[f8036]) ).
fof(f8039,plain,
( ~ sQ226_spl
| sQ223_spl
| ~ sQ253_spl ),
inference(split_clause,[status(thm)],[f8017,f8036,f6812,f6825]) ).
fof(f8041,plain,
( ~ sQ226_spl
| sQ181_spl
| sQ180_spl
| sQ223_spl ),
inference(split_clause,[status(thm)],[f8013,f6812,f4942,f4945,f6825]) ).
fof(f8062,plain,
( sQ226_spl
| not_subclass_element(unordered_pair(x,y),unordered_pair(y,x)) = y
| x = not_subclass_element(unordered_pair(x,y),unordered_pair(y,x)) ),
inference(resolution,[status(thm)],[f6827,f1377]) ).
fof(f8075,plain,
( sQ226_spl
| sQ179_spl
| sQ178_spl ),
inference(split_clause,[status(thm)],[f8062,f4936,f4939,f6825]) ).
fof(f8093,plain,
! [X0] :
( ~ sQ10_spl
| ~ sQ99_spl
| x = not_subclass_element(unordered_pair(y,x),singleton(X0))
| X0 = x
| y = not_subclass_element(unordered_pair(y,x),singleton(X0))
| X0 = not_subclass_element(singleton(X0),unordered_pair(y,x)) ),
inference(backward_demodulation,[status(thm)],[f2491,f6591]) ).
fof(f8179,plain,
( ~ sQ225_spl
| ~ sQ180_spl
| member(y,unordered_pair(y,x)) ),
inference(backward_demodulation,[status(thm)],[f4943,f6822]) ).
fof(f8198,plain,
( ~ sQ225_spl
| ~ sQ180_spl
| sQ33_spl ),
inference(split_clause,[status(thm)],[f8179,f752,f4942,f6821]) ).
fof(f8214,plain,
( sQ253_spl
| not_subclass_element(unordered_pair(y,x),unordered_pair(x,y)) = x
| y = not_subclass_element(unordered_pair(y,x),unordered_pair(x,y)) ),
inference(resolution,[status(thm)],[f8038,f1377]) ).
fof(f8223,plain,
( sQ253_spl
| sQ181_spl
| sQ180_spl ),
inference(split_clause,[status(thm)],[f8214,f4942,f4945,f8036]) ).
fof(f8234,plain,
( ~ sQ107_spl
| ~ sQ105_spl
| y = regular(unordered_pair(x,y))
| x = x ),
inference(paramodulation,[status(thm)],[f2619,f2606]) ).
fof(f8242,plain,
( ~ sQ107_spl
| ~ sQ105_spl
| sQ104_spl
| sQ68_spl ),
inference(split_clause,[status(thm)],[f8234,f1399,f2602,f2605,f2618]) ).
fof(f8286,plain,
( ~ sQ180_spl
| not_subclass_element(unordered_pair(x,y),unordered_pair(y,x)) = y
| ~ member(y,unordered_pair(x,y))
| x = not_subclass_element(unordered_pair(x,y),unordered_pair(y,x))
| unordered_pair(y,x) = unordered_pair(x,y) ),
inference(paramodulation,[status(thm)],[f4943,f339]) ).
fof(f8289,plain,
( ~ sQ180_spl
| unordered_pair(y,x) = unordered_pair(x,y)
| member(y,unordered_pair(y,x))
| member(not_subclass_element(unordered_pair(x,y),unordered_pair(y,x)),unordered_pair(x,y)) ),
inference(paramodulation,[status(thm)],[f4943,f225]) ).
fof(f8290,plain,
( ~ sQ180_spl
| unordered_pair(y,x) = unordered_pair(x,y)
| ~ member(y,unordered_pair(x,y))
| member(not_subclass_element(unordered_pair(x,y),unordered_pair(y,x)),unordered_pair(x,y)) ),
inference(paramodulation,[status(thm)],[f4943,f226]) ).
fof(f8291,plain,
( ~ sQ180_spl
| subclass(unordered_pair(y,x),unordered_pair(x,y))
| member(y,unordered_pair(y,x)) ),
inference(paramodulation,[status(thm)],[f4943,f111]) ).
fof(f8292,plain,
( ~ sQ180_spl
| ~ member(y,unordered_pair(x,y))
| subclass(unordered_pair(y,x),unordered_pair(x,y)) ),
inference(paramodulation,[status(thm)],[f4943,f112]) ).
fof(f8293,plain,
( ~ sQ180_spl
| sQ253_spl
| sQ33_spl ),
inference(split_clause,[status(thm)],[f8291,f752,f8036,f4942]) ).
fof(f8295,plain,
( ~ sQ180_spl
| ~ sQ29_spl
| sQ253_spl ),
inference(split_clause,[status(thm)],[f8292,f8036,f686,f4942]) ).
fof(f8296,definition,
( sQ254_spl
<=> member(not_subclass_element(unordered_pair(x,y),unordered_pair(y,x)),unordered_pair(x,y)) ),
introduced(definition,[new_symbols(definition,[sQ254_spl])],[split_symbol_definition]) ).
fof(f8297,plain,
( ~ sQ254_spl
| member(not_subclass_element(unordered_pair(x,y),unordered_pair(y,x)),unordered_pair(x,y)) ),
inference(component_clause,[status(thm)],[f8296]) ).
fof(f8299,plain,
( ~ sQ180_spl
| sQ223_spl
| ~ sQ29_spl
| sQ254_spl ),
inference(split_clause,[status(thm)],[f8290,f8296,f686,f6812,f4942]) ).
fof(f8300,plain,
( ~ sQ180_spl
| sQ179_spl
| ~ sQ29_spl
| sQ178_spl
| sQ223_spl ),
inference(split_clause,[status(thm)],[f8286,f6812,f4936,f686,f4939,f4942]) ).
fof(f8301,plain,
( ~ sQ180_spl
| sQ223_spl
| sQ33_spl
| sQ254_spl ),
inference(split_clause,[status(thm)],[f8289,f8296,f752,f6812,f4942]) ).
fof(f8310,plain,
( ~ sQ254_spl
| ~ sQ179_spl
| member(y,unordered_pair(x,y)) ),
inference(backward_demodulation,[status(thm)],[f4940,f8297]) ).
fof(f8311,plain,
( ~ sQ254_spl
| ~ sQ179_spl
| sQ29_spl ),
inference(split_clause,[status(thm)],[f8310,f686,f4939,f8296]) ).
fof(f8335,plain,
! [X0] :
( ~ sQ10_spl
| ~ sQ99_spl
| not_subclass_element(unordered_pair(y,x),singleton(X0)) = x
| y != x
| X0 = x
| X0 = not_subclass_element(singleton(X0),unordered_pair(y,x)) ),
inference(equality_factoring,[status(thm)],[f8093]) ).
fof(f8349,definition,
! [X0] :
( sQ259_spl
<=> ( not_subclass_element(unordered_pair(y,x),singleton(X0)) = x
| X0 = x
| X0 = not_subclass_element(singleton(X0),unordered_pair(y,x)) ) ),
introduced(definition,[new_symbols(definition,[sQ259_spl])],[split_symbol_definition]) ).
fof(f8352,plain,
( ~ sQ10_spl
| ~ sQ99_spl
| ~ sQ35_spl
| sQ259_spl ),
inference(split_clause,[status(thm)],[f8335,f8349,f794,f2490,f469]) ).
fof(f8380,plain,
( ~ sQ181_spl
| not_subclass_element(unordered_pair(x,y),unordered_pair(y,x)) = y
| ~ member(x,unordered_pair(x,y))
| x = not_subclass_element(unordered_pair(x,y),unordered_pair(y,x))
| unordered_pair(y,x) = unordered_pair(x,y) ),
inference(paramodulation,[status(thm)],[f4946,f339]) ).
fof(f8381,plain,
( ~ sQ181_spl
| unordered_pair(y,x) = unordered_pair(x,y)
| not_subclass_element(unordered_pair(x,y),unordered_pair(y,x)) = y
| not_subclass_element(unordered_pair(x,y),unordered_pair(y,x)) = x
| member(x,unordered_pair(y,x)) ),
inference(paramodulation,[status(thm)],[f4946,f251]) ).
fof(f8383,plain,
( ~ sQ181_spl
| unordered_pair(y,x) = unordered_pair(x,y)
| member(x,unordered_pair(y,x))
| member(not_subclass_element(unordered_pair(x,y),unordered_pair(y,x)),unordered_pair(x,y)) ),
inference(paramodulation,[status(thm)],[f4946,f225]) ).
fof(f8384,plain,
( ~ sQ181_spl
| unordered_pair(y,x) = unordered_pair(x,y)
| ~ member(x,unordered_pair(x,y))
| member(not_subclass_element(unordered_pair(x,y),unordered_pair(y,x)),unordered_pair(x,y)) ),
inference(paramodulation,[status(thm)],[f4946,f226]) ).
fof(f8385,plain,
( ~ sQ181_spl
| subclass(unordered_pair(y,x),unordered_pair(x,y))
| member(x,unordered_pair(y,x)) ),
inference(paramodulation,[status(thm)],[f4946,f111]) ).
fof(f8386,plain,
( ~ sQ181_spl
| ~ member(x,unordered_pair(x,y))
| subclass(unordered_pair(y,x),unordered_pair(x,y)) ),
inference(paramodulation,[status(thm)],[f4946,f112]) ).
fof(f8387,plain,
( ~ sQ181_spl
| sQ223_spl
| sQ19_spl
| sQ254_spl ),
inference(split_clause,[status(thm)],[f8383,f8296,f517,f6812,f4945]) ).
fof(f8388,plain,
( ~ sQ181_spl
| ~ sQ67_spl
| sQ253_spl ),
inference(split_clause,[status(thm)],[f8386,f8036,f1393,f4945]) ).
fof(f8389,plain,
( ~ sQ181_spl
| sQ223_spl
| sQ179_spl
| sQ178_spl
| sQ19_spl ),
inference(split_clause,[status(thm)],[f8381,f517,f4936,f4939,f6812,f4945]) ).
fof(f8390,plain,
( ~ sQ181_spl
| sQ223_spl
| ~ sQ67_spl
| sQ254_spl ),
inference(split_clause,[status(thm)],[f8384,f8296,f1393,f6812,f4945]) ).
fof(f8391,plain,
( ~ sQ181_spl
| sQ253_spl
| sQ19_spl ),
inference(split_clause,[status(thm)],[f8385,f517,f8036,f4945]) ).
fof(f8393,plain,
( ~ sQ181_spl
| sQ179_spl
| ~ sQ67_spl
| sQ178_spl
| sQ223_spl ),
inference(split_clause,[status(thm)],[f8380,f6812,f4936,f1393,f4939,f4945]) ).
fof(f8636,plain,
( ~ sQ179_spl
| not_subclass_element(unordered_pair(y,x),unordered_pair(x,y)) = x
| ~ member(y,unordered_pair(y,x))
| y = not_subclass_element(unordered_pair(y,x),unordered_pair(x,y))
| unordered_pair(x,y) = unordered_pair(y,x) ),
inference(paramodulation,[status(thm)],[f4940,f339]) ).
fof(f8637,plain,
( ~ sQ179_spl
| unordered_pair(x,y) = unordered_pair(y,x)
| not_subclass_element(unordered_pair(y,x),unordered_pair(x,y)) = x
| not_subclass_element(unordered_pair(y,x),unordered_pair(x,y)) = y
| member(y,unordered_pair(x,y)) ),
inference(paramodulation,[status(thm)],[f4940,f251]) ).
fof(f8638,plain,
( ~ sQ179_spl
| unordered_pair(y,x) = unordered_pair(x,y)
| ~ member(y,unordered_pair(y,x))
| ~ member(not_subclass_element(unordered_pair(y,x),unordered_pair(x,y)),unordered_pair(x,y)) ),
inference(paramodulation,[status(thm)],[f4940,f228]) ).
fof(f8642,plain,
( ~ sQ179_spl
| ~ member(y,unordered_pair(y,x))
| subclass(unordered_pair(x,y),unordered_pair(y,x)) ),
inference(paramodulation,[status(thm)],[f4940,f112]) ).
fof(f8644,plain,
( ~ sQ179_spl
| ~ sQ33_spl
| sQ226_spl ),
inference(split_clause,[status(thm)],[f8642,f6825,f752,f4939]) ).
fof(f8651,plain,
( ~ sQ179_spl
| sQ223_spl
| sQ181_spl
| sQ180_spl
| sQ29_spl ),
inference(split_clause,[status(thm)],[f8637,f686,f4942,f4945,f6812,f4939]) ).
fof(f8652,plain,
( ~ sQ179_spl
| sQ181_spl
| ~ sQ33_spl
| sQ180_spl
| sQ223_spl ),
inference(split_clause,[status(thm)],[f8636,f6812,f4942,f752,f4945,f4939]) ).
fof(f8654,plain,
( ~ sQ179_spl
| sQ223_spl
| ~ sQ33_spl
| ~ sQ227_spl ),
inference(split_clause,[status(thm)],[f8638,f6830,f752,f6812,f4939]) ).
fof(f8728,plain,
! [X0] :
( sQ250_spl
| ~ subclass(X0,x)
| ~ member(y,X0) ),
inference(resolution,[status(thm)],[f7940,f110]) ).
fof(f8730,plain,
! [X0] :
( ~ sQ69_spl
| ~ subclass(image(successor_relation,universal_class),universal_class)
| inductive(universal_class)
| ~ member(null_class,X0) ),
inference(resolution,[status(thm)],[f1412,f166]) ).
fof(f8735,plain,
! [X0,X1,X2,X3,X4] :
( ~ sQ69_spl
| ~ subclass(universal_class,cross_product(X3,X4))
| member(X1,unordered_pair(X0,X1))
| ~ member(ordered_pair(X0,X1),X2) ),
inference(resolution,[status(thm)],[f1412,f1437]) ).
fof(f8736,plain,
( ~ sQ69_spl
| ~ sQ53_spl
| sQ52_spl
| sQ57_spl ),
inference(split_clause,[status(thm)],[f8730,f1214,f1160,f1163,f1411]) ).
fof(f8737,definition,
! [X0,X1,X2] :
( sQ261_spl
<=> ( member(X1,unordered_pair(X0,X1))
| ~ member(ordered_pair(X0,X1),X2) ) ),
introduced(definition,[new_symbols(definition,[sQ261_spl])],[split_symbol_definition]) ).
fof(f8738,plain,
! [X0,X1,X2] :
( ~ sQ261_spl
| member(X1,unordered_pair(X0,X1))
| ~ member(ordered_pair(X0,X1),X2) ),
inference(component_clause,[status(thm)],[f8737]) ).
fof(f8740,plain,
( ~ sQ69_spl
| sQ85_spl
| sQ261_spl ),
inference(split_clause,[status(thm)],[f8735,f8737,f2058,f1411]) ).
fof(f8741,plain,
! [X0,X1,X2,X3,X4] :
( ~ sQ261_spl
| member(X3,unordered_pair(X4,X3))
| ~ subclass(complement(X0),cross_product(X1,X2)) ),
inference(backward_subsumption_resolution,[status(thm)],[f5870,f8738]) ).
fof(f8742,definition,
! [X0,X1,X2] :
( sQ262_spl
<=> ~ subclass(complement(X0),cross_product(X1,X2)) ),
introduced(definition,[new_symbols(definition,[sQ262_spl])],[split_symbol_definition]) ).
fof(f8745,plain,
( ~ sQ261_spl
| sQ84_spl
| sQ262_spl ),
inference(split_clause,[status(thm)],[f8741,f8742,f2055,f8737]) ).
fof(f8787,plain,
! [X0] :
( sQ184_spl
| ~ member(y,X0)
| ~ subclass(X0,y) ),
inference(resolution,[status(thm)],[f5182,f110]) ).
fof(f8837,plain,
! [X0] :
( sQ29_spl
| ~ member(y,X0) ),
inference(resolution,[status(thm)],[f688,f1447]) ).
fof(f8844,plain,
( sQ29_spl
| sQ117_spl ),
inference(split_clause,[status(thm)],[f8837,f3002,f686]) ).
fof(f8871,plain,
( sQ250_spl
| ~ inductive(x)
| ~ member(y,omega) ),
inference(resolution,[status(thm)],[f8728,f168]) ).
fof(f8876,plain,
( sQ250_spl
| ~ sQ137_spl
| ~ sQ136_spl ),
inference(split_clause,[status(thm)],[f8871,f3347,f3350,f7938]) ).
fof(f9123,plain,
( sQ184_spl
| ~ inductive(y)
| ~ member(y,omega) ),
inference(resolution,[status(thm)],[f8787,f168]) ).
fof(f9128,plain,
( sQ184_spl
| ~ sQ213_spl
| ~ sQ136_spl ),
inference(split_clause,[status(thm)],[f9123,f3347,f5883,f5180]) ).
fof(f9145,plain,
! [X0] :
( sQ19_spl
| ~ member(x,X0) ),
inference(resolution,[status(thm)],[f519,f1447]) ).
fof(f9154,plain,
( sQ19_spl
| sQ128_spl ),
inference(split_clause,[status(thm)],[f9145,f3173,f517]) ).
fof(f9251,plain,
! [X0] :
( apply(choice,unordered_pair(null_class,X0)) = X0
| null_class = apply(choice,unordered_pair(null_class,X0))
| member(null_class,null_class) ),
inference(paramodulation,[status(thm)],[f2281,f1073]) ).
fof(f9265,plain,
! [X0] :
( apply(choice,unordered_pair(omega,X0)) = X0
| omega = apply(choice,unordered_pair(omega,X0))
| member(omega,null_class) ),
inference(paramodulation,[status(thm)],[f2281,f1059]) ).
fof(f9273,plain,
! [X0] :
( apply(choice,unordered_pair(X0,null_class)) = null_class
| X0 = apply(choice,unordered_pair(X0,null_class))
| member(null_class,null_class) ),
inference(paramodulation,[status(thm)],[f2281,f1074]) ).
fof(f9281,plain,
! [X0] :
( apply(choice,unordered_pair(X0,omega)) = omega
| X0 = apply(choice,unordered_pair(X0,omega))
| member(omega,null_class) ),
inference(paramodulation,[status(thm)],[f2281,f1060]) ).
fof(f9299,plain,
! [X0,X1] :
( sQ8_spl
| apply(choice,unordered_pair(X0,X1)) = X1
| X0 = apply(choice,unordered_pair(X0,X1))
| y = not_subclass_element(unordered_pair(x,y),unordered_pair(X0,X1))
| null_class != null_class
| not_subclass_element(unordered_pair(X0,X1),unordered_pair(x,y)) = X0
| not_subclass_element(unordered_pair(X0,X1),unordered_pair(x,y)) = X1
| x = not_subclass_element(unordered_pair(x,y),unordered_pair(X0,X1)) ),
inference(paramodulation,[status(thm)],[f2281,f4863]) ).
fof(f9327,plain,
! [X0,X1] :
( apply(choice,unordered_pair(X0,X1)) = X1
| X0 = apply(choice,unordered_pair(X0,X1))
| member(null_class,universal_class) ),
inference(paramodulation,[status(thm)],[f2281,f123]) ).
fof(f9329,definition,
! [X0,X1] :
( sQ263_spl
<=> ( apply(choice,unordered_pair(X0,X1)) = X1
| X0 = apply(choice,unordered_pair(X0,X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ263_spl])],[split_symbol_definition]) ).
fof(f9332,plain,
( sQ263_spl
| sQ11_spl ),
inference(split_clause,[status(thm)],[f9327,f475,f9329]) ).
fof(f9333,definition,
! [X0] :
( sQ264_spl
<=> ( apply(choice,unordered_pair(X0,null_class)) = null_class
| X0 = apply(choice,unordered_pair(X0,null_class)) ) ),
introduced(definition,[new_symbols(definition,[sQ264_spl])],[split_symbol_definition]) ).
fof(f9336,plain,
( sQ264_spl
| sQ38_spl ),
inference(split_clause,[status(thm)],[f9273,f820,f9333]) ).
fof(f9348,definition,
! [X0] :
( sQ267_spl
<=> ( apply(choice,unordered_pair(null_class,X0)) = X0
| null_class = apply(choice,unordered_pair(null_class,X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ267_spl])],[split_symbol_definition]) ).
fof(f9351,plain,
( sQ267_spl
| sQ38_spl ),
inference(split_clause,[status(thm)],[f9251,f820,f9348]) ).
fof(f9383,definition,
! [X0,X1] :
( sQ271_spl
<=> ( apply(choice,unordered_pair(X0,X1)) = X1
| X0 = apply(choice,unordered_pair(X0,X1))
| y = not_subclass_element(unordered_pair(x,y),unordered_pair(X0,X1))
| not_subclass_element(unordered_pair(X0,X1),unordered_pair(x,y)) = X0
| not_subclass_element(unordered_pair(X0,X1),unordered_pair(x,y)) = X1
| x = not_subclass_element(unordered_pair(x,y),unordered_pair(X0,X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ271_spl])],[split_symbol_definition]) ).
fof(f9386,plain,
( sQ8_spl
| ~ sQ3_spl
| sQ271_spl ),
inference(split_clause,[status(thm)],[f9299,f9383,f288,f463]) ).
fof(f9387,definition,
! [X0] :
( sQ272_spl
<=> ( apply(choice,unordered_pair(X0,omega)) = omega
| X0 = apply(choice,unordered_pair(X0,omega)) ) ),
introduced(definition,[new_symbols(definition,[sQ272_spl])],[split_symbol_definition]) ).
fof(f9390,plain,
( sQ272_spl
| sQ144_spl ),
inference(split_clause,[status(thm)],[f9281,f3598,f9387]) ).
fof(f9397,definition,
! [X0] :
( sQ273_spl
<=> ( apply(choice,unordered_pair(omega,X0)) = X0
| omega = apply(choice,unordered_pair(omega,X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ273_spl])],[split_symbol_definition]) ).
fof(f9400,plain,
( sQ273_spl
| sQ144_spl ),
inference(split_clause,[status(thm)],[f9265,f3598,f9397]) ).
fof(f9480,plain,
! [X0,X1,X2,X3] :
( ~ sQ69_spl
| ~ subclass(element_relation,cross_product(X2,X3))
| member(X0,unordered_pair(X1,X0))
| ~ member(X1,X0)
| ~ member(X0,universal_class) ),
inference(resolution,[status(thm)],[f1416,f1437]) ).
fof(f9484,definition,
! [X0,X1] :
( sQ278_spl
<=> ( member(X0,unordered_pair(X1,X0))
| ~ member(X1,X0)
| ~ member(X0,universal_class) ) ),
introduced(definition,[new_symbols(definition,[sQ278_spl])],[split_symbol_definition]) ).
fof(f9487,definition,
! [X2,X3] :
( sQ279_spl
<=> ~ subclass(element_relation,cross_product(X2,X3)) ),
introduced(definition,[new_symbols(definition,[sQ279_spl])],[split_symbol_definition]) ).
fof(f9488,plain,
! [X0,X1] :
( ~ sQ279_spl
| ~ subclass(element_relation,cross_product(X0,X1)) ),
inference(component_clause,[status(thm)],[f9487]) ).
fof(f9490,plain,
( ~ sQ69_spl
| sQ279_spl
| sQ278_spl ),
inference(split_clause,[status(thm)],[f9480,f9484,f9487,f1411]) ).
fof(f9492,plain,
( ~ sQ279_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f133,f9488]) ).
fof(f9493,plain,
~ sQ279_spl,
inference(contradiction_clause,[status(thm)],[f9492]) ).
fof(f9592,plain,
! [X0] :
( ~ sQ103_spl
| not_subclass_element(unordered_pair(y,x),singleton(X0)) = x
| y != x
| y = regular(singleton(X0))
| X0 = not_subclass_element(singleton(X0),unordered_pair(y,x)) ),
inference(equality_factoring,[status(thm)],[f5764]) ).
fof(f9597,definition,
! [X0] :
( sQ281_spl
<=> ( not_subclass_element(unordered_pair(y,x),singleton(X0)) = x
| y = regular(singleton(X0))
| X0 = not_subclass_element(singleton(X0),unordered_pair(y,x)) ) ),
introduced(definition,[new_symbols(definition,[sQ281_spl])],[split_symbol_definition]) ).
fof(f9600,plain,
( ~ sQ103_spl
| ~ sQ35_spl
| sQ281_spl ),
inference(split_clause,[status(thm)],[f9592,f9597,f794,f2596]) ).
fof(f9704,plain,
! [X0] :
( sQ67_spl
| ~ member(x,X0) ),
inference(resolution,[status(thm)],[f1395,f1448]) ).
fof(f9712,plain,
( sQ67_spl
| sQ128_spl ),
inference(split_clause,[status(thm)],[f9704,f3173,f1393]) ).
fof(f9715,plain,
$false,
inference(sat_refutation,[status(thm)],[f283,f287,f298,f333,f419,f481,f493,f499,f526,f528,f629,f631,f653,f672,f758,f797,f831,f832,f855,f921,f950,f1004,f1008,f1010,f1130,f1133,f1168,f1194,f1198,f1217,f1226,f1283,f1292,f1296,f1322,f1388,f1396,f1402,f1414,f1470,f1521,f1588,f1661,f1669,f1755,f1756,f1791,f1818,f1960,f1995,f2061,f2103,f2122,f2132,f2148,f2241,f2415,f2417,f2460,f2493,f2496,f2500,f2599,f2608,f2613,f2621,f2634,f2637,f2639,f2665,f2786,f2790,f2807,f2814,f3005,f3007,f3030,f3039,f3040,f3134,f3169,f3176,f3180,f3184,f3188,f3192,f3224,f3225,f3288,f3353,f3355,f3467,f3481,f3604,f3605,f3614,f3635,f3655,f3664,f3844,f3858,f3861,f3954,f3958,f4054,f4079,f4104,f4116,f4132,f4187,f4400,f4671,f4948,f5183,f5187,f5191,f5196,f5200,f5204,f5392,f5430,f5439,f5448,f5452,f5466,f5470,f5886,f5897,f6147,f6152,f6153,f6155,f6159,f6163,f6223,f6227,f6431,f6504,f6610,f6652,f6815,f6824,f6828,f6829,f6833,f6837,f6839,f6843,f6938,f7057,f7081,f7530,f7859,f7863,f7880,f7884,f7888,f7892,f7937,f7941,f7942,f7946,f7948,f7952,f8004,f8039,f8041,f8075,f8198,f8223,f8242,f8293,f8295,f8299,f8300,f8301,f8311,f8352,f8387,f8388,f8389,f8390,f8391,f8393,f8644,f8651,f8652,f8654,f8736,f8740,f8745,f8844,f8876,f9128,f9154,f9332,f9336,f9351,f9386,f9390,f9400,f9490,f9493,f9600,f9712]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SET066-7 : TPTP v9.3.1. Bugfixed v2.1.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n026.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Mon Sep 21 04:51:54 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.38 % Drodi V4.1.1
% 222.43/28.62 % Refutation found
% 222.43/28.62 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 222.43/28.62 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 14.36/28.85 % Elapsed time: 28.472908 seconds
% 14.36/28.85 % CPU time: 224.269601 seconds
% 14.36/28.85 % Total memory used: 782.149 MB
% 14.36/28.85 % Net memory used: 680.169 MB
%------------------------------------------------------------------------------