| %-------------------------------------------------------------------------- |
| % 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. |
| %-------------------------------------------------------------------------- |