%--------------------------------------------------------------------------
% File     : SET505-6 : TPTP v2.2.1. Bugfixed v2.1.0.
% Domain   : Set Theory
% Problem  : Corollary 2 to universal class not set
% Version  : [Qua92] axioms.
% English  : 

% Refs     : [BL+86] Boyer et al. (1986), Set Theory in First-Order Logic: 
%          : [Qua92] Quaife (1992), Automated Deduction in von Neumann-Bern
% Source   : [Quaife]
% Names    : SP6 cor.2 [Qua92]

% Status   : unsatisfiable
% Rating   : 0.83 v2.2.0, 0.67 v2.1.0
% Syntax   : Number of clauses    :  113 (   8 non-Horn;  38 unit;  80 RR)
%            Number of literals   :  219 (  49 equality)
%            Maximal clause size  :    5 (   1 average)
%            Number of predicates :   11 (   0 propositional; 1-3 arity)
%            Number of functors   :   47 (  13 constant; 0-3 arity)
%            Number of variables  :  214 (  32 singleton)
%            Maximal term depth   :    6 (   1 average)

% Comments : Quaife proves all these problems by augmenting the axioms with 
%            all previously proved theorems. With a few exceptions (the
%            problems that correspond to [BL+86] problems), the TPTP has
%            retained the order in which Quaife presents the problems. The
%            user may create an augmented version of this problem by adding
%            all previously proved theorems (the ones that correspond to
%            [BL+86] are easily identified and positioned using Quaife's
%            naming scheme).
%          : tptp2X -f dfg -t rm_equality:rstfp SET505-6.p 
% Bugfixes : v1.0.1 - Bugfix in SET004-1.ax.
%          : v2.1.0 - Bugfix in SET004-0.ax.
%--------------------------------------------------------------------------

begin_problem(TPTP_Problem).

list_of_descriptions.
name({*[ File     : SET505-6 : TPTP v2.2.1. Bugfixed v2.1.0.],[ Names    : SP6 cor.2 [Qua92]]*}).
author({*[ Source   : [Quaife]]*}).
status(unsatisfiable).
description({*[ Refs     : [BL+86] Boyer et al. (1986), Set Theory in First-Order Logic: ,          : [Qua92] Quaife (1992), Automated Deduction in von Neumann-Bern]*}).
end_of_list.

list_of_symbols.
functions[(application_function,0), (apply,2), (cantor,1), (choice,0), (complement,1), (compose,2), (compose_class,1), (composition_function,0), (cross_product,2), (diagonalise,1), (domain,3), (domain_of,1), (domain_relation,0), (element_relation,0), (first,1), (flip,1), (identity_relation,0), (image,2), (intersection,2), (inverse,1), (not_homomorphism1,3), (not_homomorphism2,3), (not_subclass_element,2), (null_class,0), (omega,0), (ordered_pair,2), (power_class,1), (range,3), (range_of,1), (regular,1), (restrict,3), (rotate,1), (second,1), (single_valued1,1), (single_valued2,1), (single_valued3,1), (singleton,1), (singleton_relation,0), (subset_relation,0), (successor,1), (successor_relation,0), (sum_class,1), (symmetric_difference,2), (union,2), (universal_class,0), (unordered_pair,2), (y,0)].
predicates[(compatible,3), (function,1), (homomorphism,3), (inductive,1), (maps,3), (member,2), (one_to_one,1), (operation,1), (single_valued_class,1), (subclass,2)].
end_of_list.

list_of_clauses(axioms,cnf).

clause(
forall([U,X,Y],
or( not(subclass(X,Y)),
    not(member(U,X)),
    member(U,Y))),
subclass_members ).

clause(
forall([X,Y],
or( member(not_subclass_element(X,Y),X),
    subclass(X,Y))),
not_subclass_members1 ).

clause(
forall([X,Y],
or( not(member(not_subclass_element(X,Y),Y)),
    subclass(X,Y))),
not_subclass_members2 ).

clause(
forall([X],
or( subclass(X,universal_class))),
class_elements_are_sets ).

clause(
forall([X,Y],
or( not(equal(X,Y)),
    subclass(X,Y))),
equal_implies_subclass1 ).

clause(
forall([X,Y],
or( not(equal(X,Y)),
    subclass(Y,X))),
equal_implies_subclass2 ).

clause(
forall([X,Y],
or( not(subclass(X,Y)),
    not(subclass(Y,X)),
    equal(X,Y))),
subclass_implies_equal ).

clause(
forall([U,X,Y],
or( not(member(U,unordered_pair(X,Y))),
    equal(U,X),
    equal(U,Y))),
unordered_pair_member ).

clause(
forall([X,Y],
or( not(member(X,universal_class)),
    member(X,unordered_pair(X,Y)))),
unordered_pair2 ).

clause(
forall([X,Y],
or( not(member(Y,universal_class)),
    member(Y,unordered_pair(X,Y)))),
unordered_pair3 ).

clause(
forall([X,Y],
or( member(unordered_pair(X,Y),universal_class))),
unordered_pairs_in_universal ).

clause(
forall([X],
or( equal(unordered_pair(X,X),singleton(X)))),
singleton_set ).

clause(
forall([X,Y],
or( equal(unordered_pair(singleton(X),unordered_pair(X,singleton(Y))),ordered_pair(X,Y)))),
ordered_pair ).

clause(
forall([U,V,X,Y],
or( not(member(ordered_pair(U,V),cross_product(X,Y))),
    member(U,X))),
cartesian_product1 ).

clause(
forall([U,V,X,Y],
or( not(member(ordered_pair(U,V),cross_product(X,Y))),
    member(V,Y))),
cartesian_product2 ).

clause(
forall([U,V,X,Y],
or( not(member(U,X)),
    not(member(V,Y)),
    member(ordered_pair(U,V),cross_product(X,Y)))),
cartesian_product3 ).

clause(
forall([X,Y,Z],
or( not(member(Z,cross_product(X,Y))),
    equal(ordered_pair(first(Z),second(Z)),Z))),
cartesian_product4 ).

clause(
or( subclass(element_relation,cross_product(universal_class,universal_class))),
element_relation1 ).

clause(
forall([X,Y],
or( not(member(ordered_pair(X,Y),element_relation)),
    member(X,Y))),
element_relation2 ).

clause(
forall([X,Y],
or( not(member(ordered_pair(X,Y),cross_product(universal_class,universal_class))),
    not(member(X,Y)),
    member(ordered_pair(X,Y),element_relation))),
element_relation3 ).

clause(
forall([X,Y,Z],
or( not(member(Z,intersection(X,Y))),
    member(Z,X))),
intersection1 ).

clause(
forall([X,Y,Z],
or( not(member(Z,intersection(X,Y))),
    member(Z,Y))),
intersection2 ).

clause(
forall([X,Y,Z],
or( not(member(Z,X)),
    not(member(Z,Y)),
    member(Z,intersection(X,Y)))),
intersection3 ).

clause(
forall([X,Z],
or( not(member(Z,complement(X))),
    not(member(Z,X)))),
complement1 ).

clause(
forall([X,Z],
or( not(member(Z,universal_class)),
    member(Z,complement(X)),
    member(Z,X))),
complement2 ).

clause(
forall([X,Y],
or( equal(complement(intersection(complement(X),complement(Y))),union(X,Y)))),
union ).

clause(
forall([X,Y],
or( equal(intersection(complement(intersection(X,Y)),complement(intersection(complement(X),complement(Y)))),symmetric_difference(X,Y)))),
symmetric_difference ).

clause(
forall([X,Xr,Y],
or( equal(intersection(Xr,cross_product(X,Y)),restrict(Xr,X,Y)))),
restriction1 ).

clause(
forall([X,Xr,Y],
or( equal(intersection(cross_product(X,Y),Xr),restrict(Xr,X,Y)))),
restriction2 ).

clause(
forall([X,Z],
or( not(equal(restrict(X,singleton(Z),universal_class),null_class)),
    not(member(Z,domain_of(X))))),
domain1 ).

clause(
forall([X,Z],
or( not(member(Z,universal_class)),
    equal(restrict(X,singleton(Z),universal_class),null_class),
    member(Z,domain_of(X)))),
domain2 ).

clause(
forall([X],
or( subclass(rotate(X),cross_product(cross_product(universal_class,universal_class),universal_class)))),
rotate1 ).

clause(
forall([U,V,W,X],
or( not(member(ordered_pair(ordered_pair(U,V),W),rotate(X))),
    member(ordered_pair(ordered_pair(V,W),U),X))),
rotate2 ).

clause(
forall([U,V,W,X],
or( not(member(ordered_pair(ordered_pair(V,W),U),X)),
    not(member(ordered_pair(ordered_pair(U,V),W),cross_product(cross_product(universal_class,universal_class),universal_class))),
    member(ordered_pair(ordered_pair(U,V),W),rotate(X)))),
rotate3 ).

clause(
forall([X],
or( subclass(flip(X),cross_product(cross_product(universal_class,universal_class),universal_class)))),
flip1 ).

clause(
forall([U,V,W,X],
or( not(member(ordered_pair(ordered_pair(U,V),W),flip(X))),
    member(ordered_pair(ordered_pair(V,U),W),X))),
flip2 ).

clause(
forall([U,V,W,X],
or( not(member(ordered_pair(ordered_pair(V,U),W),X)),
    not(member(ordered_pair(ordered_pair(U,V),W),cross_product(cross_product(universal_class,universal_class),universal_class))),
    member(ordered_pair(ordered_pair(U,V),W),flip(X)))),
flip3 ).

clause(
forall([Y],
or( equal(domain_of(flip(cross_product(Y,universal_class))),inverse(Y)))),
inverse ).

clause(
forall([Z],
or( equal(domain_of(inverse(Z)),range_of(Z)))),
range_of ).

clause(
forall([X,Y,Z],
or( equal(first(not_subclass_element(restrict(Z,X,singleton(Y)),null_class)),domain(Z,X,Y)))),
domain ).

clause(
forall([X,Y,Z],
or( equal(second(not_subclass_element(restrict(Z,singleton(X),Y),null_class)),range(Z,X,Y)))),
range ).

clause(
forall([X,Xr],
or( equal(range_of(restrict(Xr,X,universal_class)),image(Xr,X)))),
image ).

clause(
forall([X],
or( equal(union(X,singleton(X)),successor(X)))),
successor ).

clause(
or( subclass(successor_relation,cross_product(universal_class,universal_class))),
successor_relation1 ).

clause(
forall([X,Y],
or( not(member(ordered_pair(X,Y),successor_relation)),
    equal(successor(X),Y))),
successor_relation2 ).

clause(
forall([X,Y],
or( not(equal(successor(X),Y)),
    not(member(ordered_pair(X,Y),cross_product(universal_class,universal_class))),
    member(ordered_pair(X,Y),successor_relation))),
successor_relation3 ).

clause(
forall([X],
or( not(inductive(X)),
    member(null_class,X))),
inductive1 ).

clause(
forall([X],
or( not(inductive(X)),
    subclass(image(successor_relation,X),X))),
inductive2 ).

clause(
forall([X],
or( not(member(null_class,X)),
    not(subclass(image(successor_relation,X),X)),
    inductive(X))),
inductive3 ).

clause(
or( inductive(omega)),
omega_is_inductive1 ).

clause(
forall([Y],
or( not(inductive(Y)),
    subclass(omega,Y))),
omega_is_inductive2 ).

clause(
or( member(omega,universal_class)),
omega_in_universal ).

clause(
forall([X],
or( equal(domain_of(restrict(element_relation,universal_class,X)),sum_class(X)))),
sum_class_definition ).

clause(
forall([X],
or( not(member(X,universal_class)),
    member(sum_class(X),universal_class))),
sum_class2 ).

clause(
forall([X],
or( equal(complement(image(element_relation,complement(X))),power_class(X)))),
power_class_definition ).

clause(
forall([U],
or( not(member(U,universal_class)),
    member(power_class(U),universal_class))),
power_class2 ).

clause(
forall([Xr,Yr],
or( subclass(compose(Yr,Xr),cross_product(universal_class,universal_class)))),
compose1 ).

clause(
forall([Xr,Y,Yr,Z],
or( not(member(ordered_pair(Y,Z),compose(Yr,Xr))),
    member(Z,image(Yr,image(Xr,singleton(Y)))))),
compose2 ).

clause(
forall([Xr,Y,Yr,Z],
or( not(member(Z,image(Yr,image(Xr,singleton(Y))))),
    not(member(ordered_pair(Y,Z),cross_product(universal_class,universal_class))),
    member(ordered_pair(Y,Z),compose(Yr,Xr)))),
compose3 ).

clause(
forall([X],
or( not(single_valued_class(X)),
    subclass(compose(X,inverse(X)),identity_relation))),
single_valued_class1 ).

clause(
forall([X],
or( not(subclass(compose(X,inverse(X)),identity_relation)),
    single_valued_class(X))),
single_valued_class2 ).

clause(
forall([Xf],
or( not(function(Xf)),
    subclass(Xf,cross_product(universal_class,universal_class)))),
function1 ).

clause(
forall([Xf],
or( not(function(Xf)),
    subclass(compose(Xf,inverse(Xf)),identity_relation))),
function2 ).

clause(
forall([Xf],
or( not(subclass(Xf,cross_product(universal_class,universal_class))),
    not(subclass(compose(Xf,inverse(Xf)),identity_relation)),
    function(Xf))),
function3 ).

clause(
forall([X,Xf],
or( not(function(Xf)),
    not(member(X,universal_class)),
    member(image(Xf,X),universal_class))),
replacement ).

clause(
forall([X],
or( equal(X,null_class),
    member(regular(X),X))),
regularity1 ).

clause(
forall([X],
or( equal(X,null_class),
    equal(intersection(X,regular(X)),null_class))),
regularity2 ).

clause(
forall([Xf,Y],
or( equal(sum_class(image(Xf,singleton(Y))),apply(Xf,Y)))),
apply ).

clause(
or( function(choice)),
choice1 ).

clause(
forall([Y],
or( not(member(Y,universal_class)),
    equal(Y,null_class),
    member(apply(choice,Y),Y))),
choice2 ).

clause(
forall([Xf],
or( not(one_to_one(Xf)),
    function(Xf))),
one_to_one1 ).

clause(
forall([Xf],
or( not(one_to_one(Xf)),
    function(inverse(Xf)))),
one_to_one2 ).

clause(
forall([Xf],
or( not(function(inverse(Xf))),
    not(function(Xf)),
    one_to_one(Xf))),
one_to_one3 ).

clause(
or( equal(intersection(cross_product(universal_class,universal_class),intersection(cross_product(universal_class,universal_class),complement(compose(complement(element_relation),inverse(element_relation))))),subset_relation)),
subset_relation ).

clause(
or( equal(intersection(inverse(subset_relation),subset_relation),identity_relation)),
identity_relation ).

clause(
forall([Xr],
or( equal(complement(domain_of(intersection(Xr,identity_relation))),diagonalise(Xr)))),
diagonalisation ).

clause(
forall([X],
or( equal(intersection(domain_of(X),diagonalise(compose(inverse(element_relation),X))),cantor(X)))),
cantor_class ).

clause(
forall([Xf],
or( not(operation(Xf)),
    function(Xf))),
operation1 ).

clause(
forall([Xf],
or( not(operation(Xf)),
    equal(cross_product(domain_of(domain_of(Xf)),domain_of(domain_of(Xf))),domain_of(Xf)))),
operation2 ).

clause(
forall([Xf],
or( not(operation(Xf)),
    subclass(range_of(Xf),domain_of(domain_of(Xf))))),
operation3 ).

clause(
forall([Xf],
or( not(function(Xf)),
    not(equal(cross_product(domain_of(domain_of(Xf)),domain_of(domain_of(Xf))),domain_of(Xf))),
    not(subclass(range_of(Xf),domain_of(domain_of(Xf)))),
    operation(Xf))),
operation4 ).

clause(
forall([Xf1,Xf2,Xh],
or( not(compatible(Xh,Xf1,Xf2)),
    function(Xh))),
compatible1 ).

clause(
forall([Xf1,Xf2,Xh],
or( not(compatible(Xh,Xf1,Xf2)),
    equal(domain_of(domain_of(Xf1)),domain_of(Xh)))),
compatible2 ).

clause(
forall([Xf1,Xf2,Xh],
or( not(compatible(Xh,Xf1,Xf2)),
    subclass(range_of(Xh),domain_of(domain_of(Xf2))))),
compatible3 ).

clause(
forall([Xf1,Xf2,Xh],
or( not(function(Xh)),
    not(equal(domain_of(domain_of(Xf1)),domain_of(Xh))),
    not(subclass(range_of(Xh),domain_of(domain_of(Xf2)))),
    compatible(Xh,Xf1,Xf2))),
compatible4 ).

clause(
forall([Xf1,Xf2,Xh],
or( not(homomorphism(Xh,Xf1,Xf2)),
    operation(Xf1))),
homomorphism1 ).

clause(
forall([Xf1,Xf2,Xh],
or( not(homomorphism(Xh,Xf1,Xf2)),
    operation(Xf2))),
homomorphism2 ).

clause(
forall([Xf1,Xf2,Xh],
or( not(homomorphism(Xh,Xf1,Xf2)),
    compatible(Xh,Xf1,Xf2))),
homomorphism3 ).

clause(
forall([X,Xf1,Xf2,Xh,Y],
or( not(homomorphism(Xh,Xf1,Xf2)),
    not(member(ordered_pair(X,Y),domain_of(Xf1))),
    equal(apply(Xf2,ordered_pair(apply(Xh,X),apply(Xh,Y))),apply(Xh,apply(Xf1,ordered_pair(X,Y)))))),
homomorphism4 ).

clause(
forall([Xf1,Xf2,Xh],
or( not(operation(Xf1)),
    not(operation(Xf2)),
    not(compatible(Xh,Xf1,Xf2)),
    member(ordered_pair(not_homomorphism1(Xh,Xf1,Xf2),not_homomorphism2(Xh,Xf1,Xf2)),domain_of(Xf1)),
    homomorphism(Xh,Xf1,Xf2))),
homomorphism5 ).

clause(
forall([Xf1,Xf2,Xh],
or( not(operation(Xf1)),
    not(operation(Xf2)),
    not(compatible(Xh,Xf1,Xf2)),
    not(equal(apply(Xf2,ordered_pair(apply(Xh,not_homomorphism1(Xh,Xf1,Xf2)),apply(Xh,not_homomorphism2(Xh,Xf1,Xf2)))),apply(Xh,apply(Xf1,ordered_pair(not_homomorphism1(Xh,Xf1,Xf2),not_homomorphism2(Xh,Xf1,Xf2)))))),
    homomorphism(Xh,Xf1,Xf2))),
homomorphism6 ).

clause(
forall([X],
or( subclass(compose_class(X),cross_product(universal_class,universal_class)))),
compose_class_definition1 ).

clause(
forall([X,Y,Z],
or( not(member(ordered_pair(Y,Z),compose_class(X))),
    equal(compose(X,Y),Z))),
compose_class_definition2 ).

clause(
forall([X,Y,Z],
or( not(member(ordered_pair(Y,Z),cross_product(universal_class,universal_class))),
    not(equal(compose(X,Y),Z)),
    member(ordered_pair(Y,Z),compose_class(X)))),
compose_class_definition3 ).

clause(
or( subclass(composition_function,cross_product(universal_class,cross_product(universal_class,universal_class)))),
definition_of_composition_function1 ).

clause(
forall([X,Y,Z],
or( not(member(ordered_pair(X,ordered_pair(Y,Z)),composition_function)),
    equal(compose(X,Y),Z))),
definition_of_composition_function2 ).

clause(
forall([X,Y],
or( not(member(ordered_pair(X,Y),cross_product(universal_class,universal_class))),
    member(ordered_pair(X,ordered_pair(Y,compose(X,Y))),composition_function))),
definition_of_composition_function3 ).

clause(
or( subclass(domain_relation,cross_product(universal_class,universal_class))),
definition_of_domain_relation1 ).

clause(
forall([X,Y],
or( not(member(ordered_pair(X,Y),domain_relation)),
    equal(domain_of(X),Y))),
definition_of_domain_relation2 ).

clause(
forall([X],
or( not(member(X,universal_class)),
    member(ordered_pair(X,domain_of(X)),domain_relation))),
definition_of_domain_relation3 ).

clause(
forall([X],
or( equal(first(not_subclass_element(compose(X,inverse(X)),identity_relation)),single_valued1(X)))),
single_valued_term_defn1 ).

clause(
forall([X],
or( equal(second(not_subclass_element(compose(X,inverse(X)),identity_relation)),single_valued2(X)))),
single_valued_term_defn2 ).

clause(
forall([X],
or( equal(domain(X,image(inverse(X),singleton(single_valued1(X))),single_valued2(X)),single_valued3(X)))),
single_valued_term_defn3 ).

clause(
or( equal(intersection(complement(compose(element_relation,complement(identity_relation))),element_relation),singleton_relation)),
compose_can_define_singleton ).

clause(
or( subclass(application_function,cross_product(universal_class,cross_product(universal_class,universal_class)))),
application_function_defn1 ).

clause(
forall([X,Y,Z],
or( not(member(ordered_pair(X,ordered_pair(Y,Z)),application_function)),
    member(Y,domain_of(X)))),
application_function_defn2 ).

clause(
forall([X,Y,Z],
or( not(member(ordered_pair(X,ordered_pair(Y,Z)),application_function)),
    equal(apply(X,Y),Z))),
application_function_defn3 ).

clause(
forall([X,Y,Z],
or( not(member(ordered_pair(X,ordered_pair(Y,Z)),cross_product(universal_class,cross_product(universal_class,universal_class)))),
    not(member(Y,domain_of(X))),
    member(ordered_pair(X,ordered_pair(Y,apply(X,Y))),application_function))),
application_function_defn4 ).

clause(
forall([X,Xf,Y],
or( not(maps(Xf,X,Y)),
    function(Xf))),
maps1 ).

clause(
forall([X,Xf,Y],
or( not(maps(Xf,X,Y)),
    equal(domain_of(Xf),X))),
maps2 ).

clause(
forall([X,Xf,Y],
or( not(maps(Xf,X,Y)),
    subclass(range_of(Xf),Y))),
maps3 ).

clause(
forall([Xf,Y],
or( not(function(Xf)),
    not(subclass(range_of(Xf),Y)),
    maps(Xf,domain_of(Xf),Y))),
maps4 ).

end_of_list.

list_of_clauses(conjectures,cnf).

clause(  %(conjecture)
or( member(ordered_pair(universal_class,y),cross_product(universal_class,universal_class))),
prove_corollary_2_to_universal_class_not_set_1 ).

end_of_list.

end_problem.
%--------------------------------------------------------------------------