diff options
Diffstat (limited to 'test/spass/problem.dfg')
| -rw-r--r-- | test/spass/problem.dfg | 718 |
1 files changed, 718 insertions, 0 deletions
diff --git a/test/spass/problem.dfg b/test/spass/problem.dfg new file mode 100644 index 0000000..4527e6a --- /dev/null +++ b/test/spass/problem.dfg @@ -0,0 +1,718 @@ +%-------------------------------------------------------------------------- +% 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. +%-------------------------------------------------------------------------- |