----- Otter 3.2, August 2001 ----- The process was started by sandro on roke.hawke.org, Wed Sep 3 15:25:47 2003 The command was "otter". The process ID is 29723. set(auto). dependent: set(auto1). dependent: set(process_input). dependent: clear(print_kept). dependent: clear(print_new_demod). dependent: clear(print_back_demod). dependent: clear(print_back_sub). dependent: set(control_memory). dependent: assign(max_mem, 12000). dependent: assign(pick_given_ratio, 4). dependent: assign(stats_level, 1). dependent: assign(max_seconds, 10800). clear(sigint_interact). include('otter/owlAx.otter'). ------- start included file otter/owlAx.otter------- include('otter/owlAx-unionOf.otter'). ------- start included file otter/owlAx-unionOf.otter------- formula_list(usable). all INST CLASS LIST (rdf(CLASS,owl_unionOf,LIST)-> (rdf(INST,rdf_type,CLASS)<->instanceOfAny(INST,LIST))). all INST LIST HEAD TAIL (rdf(LIST,rdf_first,HEAD)&rdf(LIST,rdf_rest,TAIL)-> (instanceOfAny(INST,LIST)<->rdf(INST,rdf_type,HEAD)|instanceOfAny(INST,TAIL))). all INST (-instanceOfAny(INST,rdf_nil)). end_of_list. -------> usable clausifies to: list(usable). 0 [] -rdf(x1,owl_unionOf,x2)| -rdf(x3,rdf_type,x1)|instanceOfAny(x3,x2). 0 [] -rdf(x1,owl_unionOf,x2)|rdf(x3,rdf_type,x1)| -instanceOfAny(x3,x2). 0 [] -rdf(x4,rdf_first,x5)| -rdf(x4,rdf_rest,x6)| -instanceOfAny(x7,x4)|rdf(x7,rdf_type,x5)|instanceOfAny(x7,x6). 0 [] -rdf(x4,rdf_first,x5)| -rdf(x4,rdf_rest,x6)|instanceOfAny(x7,x4)| -rdf(x7,rdf_type,x5). 0 [] -rdf(x4,rdf_first,x5)| -rdf(x4,rdf_rest,x6)|instanceOfAny(x7,x4)| -instanceOfAny(x7,x6). 0 [] -instanceOfAny(x8,rdf_nil). end_of_list. ------- end included file otter/owlAx-unionOf.otter------- include('otter/owlAx-oneOf.otter'). ------- start included file otter/owlAx-oneOf.otter------- formula_list(usable). all CLASS LIST (rdf(CLASS,owl_oneOf,LIST)-> (all INST (rdf(INST,rdf_type,CLASS)<->inList(INST,LIST)))). all MEMBER LIST HEAD TAIL (rdf(LIST,rdf_first,HEAD)&rdf(LIST,rdf_rest,TAIL)-> (inList(MEMBER,LIST)<->rdf(MEMBER,owl_sameAs,HEAD)|inList(MEMBER,TAIL))). all MEMBER (-inList(MEMBER,rdf_nil)). end_of_list. -------> usable clausifies to: list(usable). 0 [] -rdf(x9,owl_oneOf,x10)| -rdf(x11,rdf_type,x9)|inList(x11,x10). 0 [] -rdf(x9,owl_oneOf,x10)|rdf(x11,rdf_type,x9)| -inList(x11,x10). 0 [] -rdf(x12,rdf_first,x13)| -rdf(x12,rdf_rest,x14)| -inList(x15,x12)|rdf(x15,owl_sameAs,x13)|inList(x15,x14). 0 [] -rdf(x12,rdf_first,x13)| -rdf(x12,rdf_rest,x14)|inList(x15,x12)| -rdf(x15,owl_sameAs,x13). 0 [] -rdf(x12,rdf_first,x13)| -rdf(x12,rdf_rest,x14)|inList(x15,x12)| -inList(x15,x14). 0 [] -inList(x16,rdf_nil). end_of_list. ------- end included file otter/owlAx-oneOf.otter------- include('otter/owlAx-equivProp.otter'). ------- start included file otter/owlAx-equivProp.otter------- formula_list(usable). all PRED1 PRED2 (rdf(PRED1,owl_equivalentProperty,PRED2)<-> (all SUBJ OBJ (rdf(SUBJ,PRED1,OBJ)<->rdf(SUBJ,PRED2,OBJ)))). all PRED1 PRED2 (rdf(PRED1,rdfs_subPropertyOf,PRED2)<-> (all SUBJ OBJ (rdf(SUBJ,PRED1,OBJ)->rdf(SUBJ,PRED2,OBJ)))). end_of_list. -------> usable clausifies to: list(usable). 0 [] -rdf(x17,owl_equivalentProperty,x18)| -rdf(x19,x17,x20)|rdf(x19,x18,x20). 0 [] -rdf(x17,owl_equivalentProperty,x18)|rdf(x19,x17,x20)| -rdf(x19,x18,x20). 0 [] rdf(x17,owl_equivalentProperty,x18)|rdf($f2(x17,x18),x17,$f1(x17,x18))|rdf($f2(x17,x18),x18,$f1(x17,x18)). 0 [] rdf(x17,owl_equivalentProperty,x18)| -rdf($f2(x17,x18),x17,$f1(x17,x18))| -rdf($f2(x17,x18),x18,$f1(x17,x18)). 0 [] -rdf(x21,rdfs_subPropertyOf,x22)| -rdf(x23,x21,x24)|rdf(x23,x22,x24). 0 [] rdf(x21,rdfs_subPropertyOf,x22)|rdf($f4(x21,x22),x21,$f3(x21,x22)). 0 [] rdf(x21,rdfs_subPropertyOf,x22)| -rdf($f4(x21,x22),x22,$f3(x21,x22)). end_of_list. ------- end included file otter/owlAx-equivProp.otter------- include('otter/owlAx-card.otter'). ------- start included file otter/owlAx-card.otter------- formula_list(usable). all X (X=X). all X Y (rdf(X,owl_differentFrom,Y)->X!=Y). all X Y (rdf(X,owl_differentFrom,Y)->Y!=X). all X Y Z (rdf(X,'foo:succ',Y)&rdf(X,'foo:succ',Z)->Y=Z). all X Y Z (rdf(X,'foo:succ',Y)&rdf(Z,'foo:succ',Y)->X=Z). 'foo:zero'=i0. rdf('foo:zero','foo:succ',i1). rdf(i1,'foo:succ',i2). rdf(i2,'foo:succ',i3). all S (maxCardinality(S,i0)<-> -(exists A item(A,S))). all S (maxCardinality(S,i1)<-> -(exists A B (A!=B&item(A,S)&item(B,S)))). all S (maxCardinality(S,i2)<-> -(exists A B C (A!=B&A!=C&B!=C&B!=A&C!=A&C!=B&item(A,S)&item(B,S)&item(C,S)))). all S minCardinality(S,i0). all S (minCardinality(S,i1)<-> (exists A item(A,S))). all S (minCardinality(S,i2)<-> (exists A B (A!=B&item(A,S)&item(B,S)))). all S (minCardinality(S,i2)<-> (exists A B (A!=B&item(A,S)&item(B,S)))). all S (minCardinality(S,i3)<-> (exists A B C (A!=B&B!=C&A!=C&item(A,S)&item(B,S)&item(C,S)))). all RESTRICTION PROPERTY CARDINALITY INST (rdf(RESTRICTION,rdf_type,owl_Restriction)&rdf(RESTRICTION,owl_onProperty,PROPERTY)&rdf(RESTRICTION,owl_cardinality,CARDINALITY)&rdf(INST,rdf_type,RESTRICTION)-> (exists SET all VAL ((rdf(INST,PROPERTY,VAL)->item(VAL,SET))&minCardinality(SET,CARDINALITY)&maxCardinality(SET,CARDINALITY)))). all RESTRICTION PROPERTY CARDINALITY INST (rdf(RESTRICTION,rdf_type,owl_Restriction)&rdf(RESTRICTION,owl_onProperty,PROPERTY)&rdf(RESTRICTION,owl_maxCardinality,CARDINALITY)&rdf(INST,rdf_type,RESTRICTION)-> (exists SET all VAL ((rdf(INST,PROPERTY,VAL)->item(VAL,SET))&maxCardinality(SET,CARDINALITY)))). all RESTRICTION PROPERTY CARDINALITY INST (rdf(RESTRICTION,rdf_type,owl_Restriction)&rdf(RESTRICTION,owl_onProperty,PROPERTY)&rdf(RESTRICTION,owl_minCardinality,CARDINALITY)&rdf(INST,rdf_type,RESTRICTION)-> (exists SET all VAL ((rdf(INST,PROPERTY,VAL)->item(VAL,SET))&minCardinality(SET,CARDINALITY)))). end_of_list. -------> usable clausifies to: list(usable). 0 [] x25=x25. 0 [] -rdf(x26,owl_differentFrom,x27)|x26!=x27. 0 [] -rdf(x28,owl_differentFrom,x29)|x29!=x28. 0 [] -rdf(x30,'foo:succ',x31)| -rdf(x30,'foo:succ',x32)|x31=x32. 0 [] -rdf(x33,'foo:succ',x34)| -rdf(x35,'foo:succ',x34)|x33=x35. 0 [] 'foo:zero'=i0. 0 [] rdf('foo:zero','foo:succ',i1). 0 [] rdf(i1,'foo:succ',i2). 0 [] rdf(i2,'foo:succ',i3). 0 [] -maxCardinality(x36,i0)| -item(x37,x36). 0 [] maxCardinality(x36,i0)|item($f5(x36),x36). 0 [] -maxCardinality(x38,i1)|x39=x40| -item(x39,x38)| -item(x40,x38). 0 [] maxCardinality(x38,i1)|$f7(x38)!=$f6(x38). 0 [] maxCardinality(x38,i1)|item($f7(x38),x38). 0 [] maxCardinality(x38,i1)|item($f6(x38),x38). 0 [] -maxCardinality(x41,i2)|x42=x43|x42=x44|x43=x44|x43=x42|x44=x42|x44=x43| -item(x42,x41)| -item(x43,x41)| -item(x44,x41). 0 [] maxCardinality(x41,i2)|$f10(x41)!=$f9(x41). 0 [] maxCardinality(x41,i2)|$f10(x41)!=$f8(x41). 0 [] maxCardinality(x41,i2)|$f9(x41)!=$f8(x41). 0 [] maxCardinality(x41,i2)|$f9(x41)!=$f10(x41). 0 [] maxCardinality(x41,i2)|$f8(x41)!=$f10(x41). 0 [] maxCardinality(x41,i2)|$f8(x41)!=$f9(x41). 0 [] maxCardinality(x41,i2)|item($f10(x41),x41). 0 [] maxCardinality(x41,i2)|item($f9(x41),x41). 0 [] maxCardinality(x41,i2)|item($f8(x41),x41). 0 [] minCardinality(x45,i0). 0 [] -minCardinality(x46,i1)|item($f11(x46),x46). 0 [] minCardinality(x46,i1)| -item(x47,x46). 0 [] -minCardinality(x48,i2)|$f13(x48)!=$f12(x48). 0 [] -minCardinality(x48,i2)|item($f13(x48),x48). 0 [] -minCardinality(x48,i2)|item($f12(x48),x48). 0 [] minCardinality(x48,i2)|x49=x50| -item(x49,x48)| -item(x50,x48). 0 [] -minCardinality(x51,i2)|$f15(x51)!=$f14(x51). 0 [] -minCardinality(x51,i2)|item($f15(x51),x51). 0 [] -minCardinality(x51,i2)|item($f14(x51),x51). 0 [] minCardinality(x51,i2)|x52=x53| -item(x52,x51)| -item(x53,x51). 0 [] -minCardinality(x54,i3)|$f18(x54)!=$f17(x54). 0 [] -minCardinality(x54,i3)|$f17(x54)!=$f16(x54). 0 [] -minCardinality(x54,i3)|$f18(x54)!=$f16(x54). 0 [] -minCardinality(x54,i3)|item($f18(x54),x54). 0 [] -minCardinality(x54,i3)|item($f17(x54),x54). 0 [] -minCardinality(x54,i3)|item($f16(x54),x54). 0 [] minCardinality(x54,i3)|x55=x56|x56=x57|x55=x57| -item(x55,x54)| -item(x56,x54)| -item(x57,x54). 0 [] -rdf(x58,rdf_type,owl_Restriction)| -rdf(x58,owl_onProperty,x59)| -rdf(x58,owl_cardinality,x60)| -rdf(x61,rdf_type,x58)| -rdf(x61,x59,x62)|item(x62,$f19(x58,x59,x60,x61)). 0 [] -rdf(x58,rdf_type,owl_Restriction)| -rdf(x58,owl_onProperty,x59)| -rdf(x58,owl_cardinality,x60)| -rdf(x61,rdf_type,x58)|minCardinality($f19(x58,x59,x60,x61),x60). 0 [] -rdf(x58,rdf_type,owl_Restriction)| -rdf(x58,owl_onProperty,x59)| -rdf(x58,owl_cardinality,x60)| -rdf(x61,rdf_type,x58)|maxCardinality($f19(x58,x59,x60,x61),x60). 0 [] -rdf(x63,rdf_type,owl_Restriction)| -rdf(x63,owl_onProperty,x64)| -rdf(x63,owl_maxCardinality,x65)| -rdf(x66,rdf_type,x63)| -rdf(x66,x64,x67)|item(x67,$f20(x63,x64,x65,x66)). 0 [] -rdf(x63,rdf_type,owl_Restriction)| -rdf(x63,owl_onProperty,x64)| -rdf(x63,owl_maxCardinality,x65)| -rdf(x66,rdf_type,x63)|maxCardinality($f20(x63,x64,x65,x66),x65). 0 [] -rdf(x68,rdf_type,owl_Restriction)| -rdf(x68,owl_onProperty,x69)| -rdf(x68,owl_minCardinality,x70)| -rdf(x71,rdf_type,x68)| -rdf(x71,x69,x72)|item(x72,$f21(x68,x69,x70,x71)). 0 [] -rdf(x68,rdf_type,owl_Restriction)| -rdf(x68,owl_onProperty,x69)| -rdf(x68,owl_minCardinality,x70)| -rdf(x71,rdf_type,x68)|minCardinality($f21(x68,x69,x70,x71),x70). end_of_list. ------- end included file otter/owlAx-card.otter------- include('otter/owlAx-cardeq.otter'). ------- start included file otter/owlAx-cardeq.otter------- formula_list(usable). all PROP CLASS CARD ((exists R (rdf(R,owl_onProperty,PROP)&rdf(R,owl_cardinality,CARD)&rdf(CLASS,rdfs_subClassOf,R)))<-> (exists R1 R2 (rdf(R1,owl_onProperty,PROP)&rdf(R1,owl_maxCardinality,CARD)&rdf(R2,owl_onProperty,PROP)&rdf(R2,owl_minCardinality,CARD)&rdf(CLASS,rdfs_subClassOf,R1)&rdf(CLASS,rdfs_subClassOf,R2)))). all INST PROP (rdf(INST,owl_onProperty,PROP)->rdf(INST,rdf_type,owl_Restriction)). end_of_list. -------> usable clausifies to: list(usable). 0 [] -rdf(x73,owl_onProperty,x74)| -rdf(x73,owl_cardinality,x75)| -rdf(x76,rdfs_subClassOf,x73)|rdf($f23(x74,x76,x75),owl_onProperty,x74). 0 [] -rdf(x73,owl_onProperty,x74)| -rdf(x73,owl_cardinality,x75)| -rdf(x76,rdfs_subClassOf,x73)|rdf($f23(x74,x76,x75),owl_maxCardinality,x75). 0 [] -rdf(x73,owl_onProperty,x74)| -rdf(x73,owl_cardinality,x75)| -rdf(x76,rdfs_subClassOf,x73)|rdf($f22(x74,x76,x75),owl_onProperty,x74). 0 [] -rdf(x73,owl_onProperty,x74)| -rdf(x73,owl_cardinality,x75)| -rdf(x76,rdfs_subClassOf,x73)|rdf($f22(x74,x76,x75),owl_minCardinality,x75). 0 [] -rdf(x73,owl_onProperty,x74)| -rdf(x73,owl_cardinality,x75)| -rdf(x76,rdfs_subClassOf,x73)|rdf(x76,rdfs_subClassOf,$f23(x74,x76,x75)). 0 [] -rdf(x73,owl_onProperty,x74)| -rdf(x73,owl_cardinality,x75)| -rdf(x76,rdfs_subClassOf,x73)|rdf(x76,rdfs_subClassOf,$f22(x74,x76,x75)). 0 [] rdf($f24(x74,x76,x75),owl_onProperty,x74)| -rdf(x77,owl_onProperty,x74)| -rdf(x77,owl_maxCardinality,x75)| -rdf(x78,owl_onProperty,x74)| -rdf(x78,owl_minCardinality,x75)| -rdf(x76,rdfs_subClassOf,x77)| -rdf(x76,rdfs_subClassOf,x78). 0 [] rdf($f24(x74,x76,x75),owl_cardinality,x75)| -rdf(x77,owl_onProperty,x74)| -rdf(x77,owl_maxCardinality,x75)| -rdf(x78,owl_onProperty,x74)| -rdf(x78,owl_minCardinality,x75)| -rdf(x76,rdfs_subClassOf,x77)| -rdf(x76,rdfs_subClassOf,x78). 0 [] rdf(x76,rdfs_subClassOf,$f24(x74,x76,x75))| -rdf(x77,owl_onProperty,x74)| -rdf(x77,owl_maxCardinality,x75)| -rdf(x78,owl_onProperty,x74)| -rdf(x78,owl_minCardinality,x75)| -rdf(x76,rdfs_subClassOf,x77)| -rdf(x76,rdfs_subClassOf,x78). 0 [] -rdf(x79,owl_onProperty,x80)|rdf(x79,rdf_type,owl_Restriction). end_of_list. ------- end included file otter/owlAx-cardeq.otter------- formula_list(usable). -(exists c rdf(rdf_nil,rdf_rest,c)). -(exists c rdf(rdf_nil,rdf_first,c)). -(exists c rdf(c,rdf_type,owl_Nothing)). rdf(owl_Nothing,rdf_type,owl_Class). all X rdf(X,rdf_type,owl_Thing). all X rdf(X,rdf_type,rdf_Resource). all INST CLASS LIST (rdf(CLASS,owl_intersectionOf,LIST)-> (rdf(INST,rdf_type,CLASS)<->instanceOfAll(INST,LIST))). all INST LIST HEAD TAIL (rdf(LIST,rdf_first,HEAD)&rdf(LIST,rdf_rest,TAIL)-> (instanceOfAll(INST,LIST)<->rdf(INST,rdf_type,HEAD)&instanceOfAll(INST,TAIL))). all INST instanceOfAll(INST,rdf_nil). all C1 C2 (rdf(C1,owl_equivalentClass,C2)<-> (all INST (rdf(INST,rdf_type,C1)<->rdf(INST,rdf_type,C2)))). all C1 C2 (rdf(C1,rdfs_subClassOf,C2)<-> (all INST (rdf(INST,rdf_type,C1)->rdf(INST,rdf_type,C2)))). all a b (rdf(a,owl_equivalentClass,b)->rdf(a,rdfs_subClassOf,b)). all a b (rdf(a,rdfs_subClassOf,b)&rdf(b,rdfs_subClassOf,a)->rdf(a,owl_equivalentClass,b)). all C1 C2 (rdf(C1,owl_complementOf,C2)<-> (all INST (rdf(INST,rdf_type,C1)<-> -rdf(INST,rdf_type,C2)))). all C1 C2 (rdf(C1,owl_disjointWith,C2)-> (all INST (-(rdf(INST,rdf_type,C1)&rdf(INST,rdf_type,C2))))). all INST C1 C2 (rdf(C1,rdfs_subClassOf,C2)-> (rdf(INST,rdf_type,C1)->rdf(INST,rdf_type,C2))). all RESTRICTION PROPERTY BASECLASS INST VALUE (rdf(RESTRICTION,rdf_type,owl_Restriction)&rdf(RESTRICTION,owl_onProperty,PROPERTY)&rdf(RESTRICTION,owl_allValuesFrom,BASECLASS)&rdf(INST,rdf_type,RESTRICTION)-> (rdf(INST,PROPERTY,VALUE)<->rdf(VALUE,rdf_type,BASECLASS))). all RESTRICTION PROPERTY BASECLASS INST (rdf(RESTRICTION,rdf_type,owl_Restriction)&rdf(RESTRICTION,owl_onProperty,PROPERTY)&rdf(RESTRICTION,owl_someValuesFrom,BASECLASS)&rdf(INST,rdf_type,RESTRICTION)->rdf(INST,PROPERTY,valueSkFunc(INST,RESTRICTION))&rdf(valueSkFunc(INST,RESTRICTION),rdf_type,BASECLASS)). all RESTRICTION PROPERTY VALUE INST (rdf(RESTRICTION,rdf_type,owl_Restriction)&rdf(RESTRICTION,owl_onProperty,PROPERTY)&rdf(RESTRICTION,owl_hasValue,VALUE)&rdf(INST,rdf_type,RESTRICTION)->rdf(INST,PROPERTY,VALUE)). all PROPERTY (rdf(PROPERTY,rdf_type,owl_FunctionalProperty)<-> (all INST VAL1 VAL2 (rdf(INST,PROPERTY,VAL1)&rdf(INST,PROPERTY,VAL2)->rdf(VAL1,owl_sameAs,VAL2)))). all PROPERTY (rdf(PROPERTY,rdf_type,owl_InverseFunctionalProperty)<-> (all INST1 INST2 VAL (rdf(INST1,PROPERTY,VAL)&rdf(INST2,PROPERTY,VAL)->rdf(INST1,owl_sameAs,INST2)))). all X rdf(X,owl_sameAs,X). all X Y (rdf(X,owl_sameAs,Y)->rdf(Y,owl_sameAs,X)). all X Y Z (rdf(X,owl_sameAs,Y)&rdf(Y,owl_sameAs,Z)->rdf(X,owl_sameAs,Z)). all THING1 THING2 (rdf(THING1,owl_sameAs,THING2)-> (all X Y ((rdf(X,Y,THING1)<->rdf(X,Y,THING2))& (rdf(X,THING1,Y)<->rdf(X,THING2,Y))& (rdf(THING1,X,Y)<->rdf(THING2,X,Y))))). all X Y (rdf(X,owl_differentFrom,Y)->rdf(Y,owl_differentFrom,X)). all X Y (rdf(X,owl_differentFrom,Y)<-> -rdf(X,owl_sameAs,Y)). all PRED CLASS (rdf(PRED,rdfs_range,CLASS)<-> (all SUBJ OBJ (rdf(SUBJ,PRED,OBJ)->rdf(OBJ,rdf_type,CLASS)))). all PRED CLASS (rdf(PRED,rdfs_domain,CLASS)<-> (all SUBJ OBJ (rdf(SUBJ,PRED,OBJ)->rdf(SUBJ,rdf_type,CLASS)))). all PRED1 PRED2 (rdf(PRED1,owl_inverseOf,PRED2)-> (all SUBJ OBJ (rdf(SUBJ,PRED1,OBJ)<->rdf(OBJ,PRED2,SUBJ)))). all P (rdf(P,rdf_type,owl_SymmetricProperty)-> (all X Y (rdf(X,P,Y)<->rdf(Y,P,X)))). all P (rdf(P,rdf_type,owl_TransitiveProperty)-> (all X Y Z (rdf(X,P,Y)&rdf(Y,P,Z)<->rdf(X,P,Z)))). all A (rdf(A,rdf_type,owl_AllDifferent)<-> (exists L rdf(A,owl_distinctMembers,L))). all A L (rdf(A,owl_distinctMembers,L)->allDifferent(L)). allDifferent(rdf_nil). all LIST HEAD TAIL (allDifferent(LIST)&rdf(LIST,rdf_first,HEAD)&rdf(LIST,rdf_rest,TAIL)->differentFromAll(HEAD,TAIL)). all SUBJECT differentFromAll(SUBJECT,rdf_nil). all SUBJECT LIST HEAD TAIL (differentFromAll(SUBJECT,LIST)&rdf(LIST,rdf_first,HEAD)&rdf(LIST,rdf_rest,TAIL)->rdf(SUBJECT,owl_differentFrom,HEAD)&differentFromAll(SUBJECT,TAIL)). all X Y (rdf(X,owl_differentFrom,Y)->rdf(Y,owl_differentFrom,X)). all P1 P2 (rdf(P1,owl_inverseOf,P2)&rdf(P1,rdf_type,owl_FunctionalProperty)->rdf(P2,rdf_type,owl_InverseFunctionalProperty)). all P1 P2 (rdf(P1,owl_inverseOf,P2)&rdf(P1,rdf_type,owl_InverseFunctionalProperty)->rdf(P2,rdf_type,owl_FunctionalProperty)). all INST CLASS LIST FIRST (rdf(INST,rdf_type,CLASS)&rdf(CLASS,owl_unionOf,LIST)&rdf(LIST,rdf_first,FIRST)&rdf(LIST,rdf_rest,rdf_nil)->rdf(INST,rdf_type,FIRST)). all INST CLASS LIST L2 FIRST SECOND (rdf(INST,rdf_type,CLASS)&rdf(CLASS,owl_unionOf,LIST)&rdf(LIST,rdf_first,FIRST)&rdf(LIST,rdf_rest,L2)&rdf(L2,rdf_first,SECOND)&rdf(L2,rdf_rest,rdf_nil)->rdf(INST,rdf_type,FIRST)|rdf(INST,rdf_type,SECOND)). end_of_list. -------> usable clausifies to: list(usable). 0 [] -rdf(rdf_nil,rdf_rest,x81). 0 [] -rdf(rdf_nil,rdf_first,x82). 0 [] -rdf(x83,rdf_type,owl_Nothing). 0 [] rdf(owl_Nothing,rdf_type,owl_Class). 0 [] rdf(x84,rdf_type,owl_Thing). 0 [] rdf(x85,rdf_type,rdf_Resource). 0 [] -rdf(x86,owl_intersectionOf,x87)| -rdf(x88,rdf_type,x86)|instanceOfAll(x88,x87). 0 [] -rdf(x86,owl_intersectionOf,x87)|rdf(x88,rdf_type,x86)| -instanceOfAll(x88,x87). 0 [] -rdf(x89,rdf_first,x90)| -rdf(x89,rdf_rest,x91)| -instanceOfAll(x92,x89)|rdf(x92,rdf_type,x90). 0 [] -rdf(x89,rdf_first,x90)| -rdf(x89,rdf_rest,x91)| -instanceOfAll(x92,x89)|instanceOfAll(x92,x91). 0 [] -rdf(x89,rdf_first,x90)| -rdf(x89,rdf_rest,x91)|instanceOfAll(x92,x89)| -rdf(x92,rdf_type,x90)| -instanceOfAll(x92,x91). 0 [] instanceOfAll(x93,rdf_nil). 0 [] -rdf(x94,owl_equivalentClass,x95)| -rdf(x96,rdf_type,x94)|rdf(x96,rdf_type,x95). 0 [] -rdf(x94,owl_equivalentClass,x95)|rdf(x96,rdf_type,x94)| -rdf(x96,rdf_type,x95). 0 [] rdf(x94,owl_equivalentClass,x95)|rdf($f25(x94,x95),rdf_type,x94)|rdf($f25(x94,x95),rdf_type,x95). 0 [] rdf(x94,owl_equivalentClass,x95)| -rdf($f25(x94,x95),rdf_type,x94)| -rdf($f25(x94,x95),rdf_type,x95). 0 [] -rdf(x97,rdfs_subClassOf,x98)| -rdf(x99,rdf_type,x97)|rdf(x99,rdf_type,x98). 0 [] rdf(x97,rdfs_subClassOf,x98)|rdf($f26(x97,x98),rdf_type,x97). 0 [] rdf(x97,rdfs_subClassOf,x98)| -rdf($f26(x97,x98),rdf_type,x98). 0 [] -rdf(x100,owl_equivalentClass,x101)|rdf(x100,rdfs_subClassOf,x101). 0 [] -rdf(x102,rdfs_subClassOf,x103)| -rdf(x103,rdfs_subClassOf,x102)|rdf(x102,owl_equivalentClass,x103). 0 [] -rdf(x104,owl_complementOf,x105)| -rdf(x106,rdf_type,x104)| -rdf(x106,rdf_type,x105). 0 [] -rdf(x104,owl_complementOf,x105)|rdf(x106,rdf_type,x104)|rdf(x106,rdf_type,x105). 0 [] rdf(x104,owl_complementOf,x105)|rdf($f27(x104,x105),rdf_type,x104)| -rdf($f27(x104,x105),rdf_type,x105). 0 [] rdf(x104,owl_complementOf,x105)| -rdf($f27(x104,x105),rdf_type,x104)|rdf($f27(x104,x105),rdf_type,x105). 0 [] -rdf(x107,owl_disjointWith,x108)| -rdf(x109,rdf_type,x107)| -rdf(x109,rdf_type,x108). 0 [] -rdf(x110,rdfs_subClassOf,x111)| -rdf(x112,rdf_type,x110)|rdf(x112,rdf_type,x111). 0 [] -rdf(x113,rdf_type,owl_Restriction)| -rdf(x113,owl_onProperty,x114)| -rdf(x113,owl_allValuesFrom,x115)| -rdf(x116,rdf_type,x113)| -rdf(x116,x114,x117)|rdf(x117,rdf_type,x115). 0 [] -rdf(x113,rdf_type,owl_Restriction)| -rdf(x113,owl_onProperty,x114)| -rdf(x113,owl_allValuesFrom,x115)| -rdf(x116,rdf_type,x113)|rdf(x116,x114,x117)| -rdf(x117,rdf_type,x115). 0 [] -rdf(x118,rdf_type,owl_Restriction)| -rdf(x118,owl_onProperty,x119)| -rdf(x118,owl_someValuesFrom,x120)| -rdf(x121,rdf_type,x118)|rdf(x121,x119,valueSkFunc(x121,x118)). 0 [] -rdf(x118,rdf_type,owl_Restriction)| -rdf(x118,owl_onProperty,x119)| -rdf(x118,owl_someValuesFrom,x120)| -rdf(x121,rdf_type,x118)|rdf(valueSkFunc(x121,x118),rdf_type,x120). 0 [] -rdf(x122,rdf_type,owl_Restriction)| -rdf(x122,owl_onProperty,x123)| -rdf(x122,owl_hasValue,x124)| -rdf(x125,rdf_type,x122)|rdf(x125,x123,x124). 0 [] -rdf(x126,rdf_type,owl_FunctionalProperty)| -rdf(x127,x126,x128)| -rdf(x127,x126,x129)|rdf(x128,owl_sameAs,x129). 0 [] rdf(x126,rdf_type,owl_FunctionalProperty)|rdf($f30(x126),x126,$f29(x126)). 0 [] rdf(x126,rdf_type,owl_FunctionalProperty)|rdf($f30(x126),x126,$f28(x126)). 0 [] rdf(x126,rdf_type,owl_FunctionalProperty)| -rdf($f29(x126),owl_sameAs,$f28(x126)). 0 [] -rdf(x130,rdf_type,owl_InverseFunctionalProperty)| -rdf(x131,x130,x132)| -rdf(x133,x130,x132)|rdf(x131,owl_sameAs,x133). 0 [] rdf(x130,rdf_type,owl_InverseFunctionalProperty)|rdf($f33(x130),x130,$f31(x130)). 0 [] rdf(x130,rdf_type,owl_InverseFunctionalProperty)|rdf($f32(x130),x130,$f31(x130)). 0 [] rdf(x130,rdf_type,owl_InverseFunctionalProperty)| -rdf($f33(x130),owl_sameAs,$f32(x130)). 0 [] rdf(x134,owl_sameAs,x134). 0 [] -rdf(x135,owl_sameAs,x136)|rdf(x136,owl_sameAs,x135). 0 [] -rdf(x137,owl_sameAs,x138)| -rdf(x138,owl_sameAs,x139)|rdf(x137,owl_sameAs,x139). 0 [] -rdf(x140,owl_sameAs,x141)| -rdf(x142,x143,x140)|rdf(x142,x143,x141). 0 [] -rdf(x140,owl_sameAs,x141)|rdf(x142,x143,x140)| -rdf(x142,x143,x141). 0 [] -rdf(x140,owl_sameAs,x141)| -rdf(x142,x140,x143)|rdf(x142,x141,x143). 0 [] -rdf(x140,owl_sameAs,x141)|rdf(x142,x140,x143)| -rdf(x142,x141,x143). 0 [] -rdf(x140,owl_sameAs,x141)| -rdf(x140,x142,x143)|rdf(x141,x142,x143). 0 [] -rdf(x140,owl_sameAs,x141)|rdf(x140,x142,x143)| -rdf(x141,x142,x143). 0 [] -rdf(x144,owl_differentFrom,x145)|rdf(x145,owl_differentFrom,x144). 0 [] -rdf(x146,owl_differentFrom,x147)| -rdf(x146,owl_sameAs,x147). 0 [] rdf(x146,owl_differentFrom,x147)|rdf(x146,owl_sameAs,x147). 0 [] -rdf(x148,rdfs_range,x149)| -rdf(x150,x148,x151)|rdf(x151,rdf_type,x149). 0 [] rdf(x148,rdfs_range,x149)|rdf($f35(x148,x149),x148,$f34(x148,x149)). 0 [] rdf(x148,rdfs_range,x149)| -rdf($f34(x148,x149),rdf_type,x149). 0 [] -rdf(x152,rdfs_domain,x153)| -rdf(x154,x152,x155)|rdf(x154,rdf_type,x153). 0 [] rdf(x152,rdfs_domain,x153)|rdf($f37(x152,x153),x152,$f36(x152,x153)). 0 [] rdf(x152,rdfs_domain,x153)| -rdf($f37(x152,x153),rdf_type,x153). 0 [] -rdf(x156,owl_inverseOf,x157)| -rdf(x158,x156,x159)|rdf(x159,x157,x158). 0 [] -rdf(x156,owl_inverseOf,x157)|rdf(x158,x156,x159)| -rdf(x159,x157,x158). 0 [] -rdf(x160,rdf_type,owl_SymmetricProperty)| -rdf(x161,x160,x162)|rdf(x162,x160,x161). 0 [] -rdf(x160,rdf_type,owl_SymmetricProperty)|rdf(x161,x160,x162)| -rdf(x162,x160,x161). 0 [] -rdf(x163,rdf_type,owl_TransitiveProperty)| -rdf(x164,x163,x165)| -rdf(x165,x163,x166)|rdf(x164,x163,x166). 0 [] -rdf(x163,rdf_type,owl_TransitiveProperty)|rdf(x164,x163,x165)| -rdf(x164,x163,x166). 0 [] -rdf(x163,rdf_type,owl_TransitiveProperty)|rdf(x165,x163,x166)| -rdf(x164,x163,x166). 0 [] -rdf(x167,rdf_type,owl_AllDifferent)|rdf(x167,owl_distinctMembers,$f38(x167)). 0 [] rdf(x167,rdf_type,owl_AllDifferent)| -rdf(x167,owl_distinctMembers,x168). 0 [] -rdf(x169,owl_distinctMembers,x170)|allDifferent(x170). 0 [] allDifferent(rdf_nil). 0 [] -allDifferent(x171)| -rdf(x171,rdf_first,x172)| -rdf(x171,rdf_rest,x173)|differentFromAll(x172,x173). 0 [] differentFromAll(x174,rdf_nil). 0 [] -differentFromAll(x175,x176)| -rdf(x176,rdf_first,x177)| -rdf(x176,rdf_rest,x178)|rdf(x175,owl_differentFrom,x177). 0 [] -differentFromAll(x175,x176)| -rdf(x176,rdf_first,x177)| -rdf(x176,rdf_rest,x178)|differentFromAll(x175,x178). 0 [] -rdf(x179,owl_differentFrom,x180)|rdf(x180,owl_differentFrom,x179). 0 [] -rdf(x181,owl_inverseOf,x182)| -rdf(x181,rdf_type,owl_FunctionalProperty)|rdf(x182,rdf_type,owl_InverseFunctionalProperty). 0 [] -rdf(x183,owl_inverseOf,x184)| -rdf(x183,rdf_type,owl_InverseFunctionalProperty)|rdf(x184,rdf_type,owl_FunctionalProperty). 0 [] -rdf(x185,rdf_type,x186)| -rdf(x186,owl_unionOf,x187)| -rdf(x187,rdf_first,x188)| -rdf(x187,rdf_rest,rdf_nil)|rdf(x185,rdf_type,x188). 0 [] -rdf(x189,rdf_type,x190)| -rdf(x190,owl_unionOf,x191)| -rdf(x191,rdf_first,x192)| -rdf(x191,rdf_rest,x193)| -rdf(x193,rdf_first,x194)| -rdf(x193,rdf_rest,rdf_nil)|rdf(x189,rdf_type,x192)|rdf(x189,rdf_type,x194). end_of_list. ------- end included file otter/owlAx.otter------- formula_list(usable). exists s t u s0 s1 s2 s3 s4 s5 s6 s7 (rdf('http://www.w3.org/2002/03owlt/description_2Dlogic/inconsistent604',rdf_type,owl_Ontology)&rdf(ns60_c2,rdf_type,owl_Class)&rdf(ns60_c1,rdf_type,owl_Class)&rdf(ns63_C_2E1_2Ecomp,rdf_type,owl_Class)&rdf(s7,rdf_type,owl_Restriction)&rdf(ns63_P_2E1,rdf_type,owl_DatatypeProperty)&rdf(s7,owl_onProperty,ns63_P_2E1)&rdf(s7,owl_maxCardinality,lit0)&rdf(ns63_C_2E1_2Ecomp,owl_equivalentClass,s7)&rdf(s6,rdf_type,owl_Restriction)&rdf(ns60_rx3,rdf_type,owl_ObjectProperty)&rdf(s6,owl_onProperty,ns60_rx3)&rdf(ns63_A_2E2,rdf_type,owl_Class)&rdf(s6,owl_someValuesFrom,ns63_A_2E2)&rdf(ns63_C_2E1_2Ecomp,owl_equivalentClass,s6)&rdf(ns60_Unsatisfiable,rdf_type,owl_Class)&rdf(ns63_C_2E1,rdf_type,owl_Class)&rdf(s5,rdf_type,rdf_List)&rdf(s5,rdf_first,ns63_C_2E1)&rdf(s4,rdf_type,owl_Restriction)&rdf(ns60_rx3,rdf_type,owl_ObjectProperty)&rdf(s4,owl_onProperty,ns60_rx3)&rdf(s4,owl_someValuesFrom,ns60_c1)&rdf(s3,rdf_type,rdf_List)&rdf(s5,rdf_rest,s3)&rdf(s3,rdf_first,s4)&rdf(s2,rdf_type,owl_Restriction)&rdf(ns60_rx4,rdf_type,owl_ObjectProperty)&rdf(s2,owl_onProperty,ns60_rx4)&rdf(s2,owl_someValuesFrom,ns60_c2)&rdf(s1,rdf_type,rdf_List)&rdf(s3,rdf_rest,s1)&rdf(s1,rdf_first,s2)&rdf(s1,rdf_rest,rdf_nil)&rdf(ns60_Unsatisfiable,owl_intersectionOf,s5)&rdf(ns63_C_2E1,rdf_type,owl_Class)&rdf(s0,rdf_type,owl_Restriction)&rdf(s0,owl_onProperty,ns63_P_2E1)&rdf(s0,owl_minCardinality,lit1)&rdf(ns63_C_2E1,owl_equivalentClass,s0)&rdf(ns63_A_2E2,rdf_type,owl_Class)&rdf(ns60_c1,rdf_type,owl_Class)&rdf(u,rdf_type,rdf_List)&rdf(u,rdf_first,ns60_c1)&rdf(ns60_c2,rdf_type,owl_Class)&rdf(t,rdf_type,rdf_List)&rdf(u,rdf_rest,t)&rdf(t,rdf_first,ns60_c2)&rdf(t,rdf_rest,rdf_nil)&rdf(ns63_A_2E2,owl_intersectionOf,u)&rdf(ns60_rx4,rdf_type,owl_ObjectProperty)&rdf(ns60_rx2,rdf_type,owl_ObjectProperty)&rdf(ns60_rx4,rdfs_subPropertyOf,ns60_rx2)&rdf(ns60_rx,rdf_type,owl_ObjectProperty)&rdf(ns60_rx4,rdfs_subPropertyOf,ns60_rx)&rdf(ns60_rx4,rdf_type,owl_FunctionalProperty)&rdf(ns60_rx3,rdf_type,owl_ObjectProperty)&rdf(ns60_rx1,rdf_type,owl_ObjectProperty)&rdf(ns60_rx3,rdfs_subPropertyOf,ns60_rx1)&rdf(ns60_rx,rdf_type,owl_ObjectProperty)&rdf(ns60_rx3,rdfs_subPropertyOf,ns60_rx)&rdf(ns60_rx3,rdf_type,owl_FunctionalProperty)&rdf(ns60_rxa,rdf_type,owl_ObjectProperty)&rdf(ns60_rx,rdf_type,owl_ObjectProperty)&rdf(ns60_rx,rdf_type,owl_FunctionalProperty)&rdf(ns60_rx1a,rdf_type,owl_ObjectProperty)&rdf(ns60_rx2a,rdf_type,owl_ObjectProperty)&rdf(ns60_rx3a,rdf_type,owl_ObjectProperty)&rdf(ns60_rx3a,rdfs_subPropertyOf,ns60_rx1a)&rdf(ns60_rx3a,rdfs_subPropertyOf,ns60_rxa)&rdf(ns60_rx3a,rdf_type,owl_FunctionalProperty)&rdf(ns60_rx4a,rdf_type,owl_ObjectProperty)&rdf(ns60_rx4a,rdfs_subPropertyOf,ns60_rx2a)&rdf(ns60_rx4a,rdfs_subPropertyOf,ns60_rxa)&rdf(ns60_rx4a,rdf_type,owl_FunctionalProperty)&rdf(s,rdf_type,ns60_Unsatisfiable)). end_of_list. -------> usable clausifies to: list(usable). 0 [] rdf('http://www.w3.org/2002/03owlt/description_2Dlogic/inconsistent604',rdf_type,owl_Ontology). 0 [] rdf(ns60_c2,rdf_type,owl_Class). 0 [] rdf(ns60_c1,rdf_type,owl_Class). 0 [] rdf(ns63_C_2E1_2Ecomp,rdf_type,owl_Class). 0 [] rdf($c1,rdf_type,owl_Restriction). 0 [] rdf(ns63_P_2E1,rdf_type,owl_DatatypeProperty). 0 [] rdf($c1,owl_onProperty,ns63_P_2E1). 0 [] rdf($c1,owl_maxCardinality,lit0). 0 [] rdf(ns63_C_2E1_2Ecomp,owl_equivalentClass,$c1). 0 [] rdf($c2,rdf_type,owl_Restriction). 0 [] rdf(ns60_rx3,rdf_type,owl_ObjectProperty). 0 [] rdf($c2,owl_onProperty,ns60_rx3). 0 [] rdf(ns63_A_2E2,rdf_type,owl_Class). 0 [] rdf($c2,owl_someValuesFrom,ns63_A_2E2). 0 [] rdf(ns63_C_2E1_2Ecomp,owl_equivalentClass,$c2). 0 [] rdf(ns60_Unsatisfiable,rdf_type,owl_Class). 0 [] rdf(ns63_C_2E1,rdf_type,owl_Class). 0 [] rdf($c3,rdf_type,rdf_List). 0 [] rdf($c3,rdf_first,ns63_C_2E1). 0 [] rdf($c4,rdf_type,owl_Restriction). 0 [] rdf($c4,owl_onProperty,ns60_rx3). 0 [] rdf($c4,owl_someValuesFrom,ns60_c1). 0 [] rdf($c5,rdf_type,rdf_List). 0 [] rdf($c3,rdf_rest,$c5). 0 [] rdf($c5,rdf_first,$c4). 0 [] rdf($c6,rdf_type,owl_Restriction). 0 [] rdf(ns60_rx4,rdf_type,owl_ObjectProperty). 0 [] rdf($c6,owl_onProperty,ns60_rx4). 0 [] rdf($c6,owl_someValuesFrom,ns60_c2). 0 [] rdf($c7,rdf_type,rdf_List). 0 [] rdf($c5,rdf_rest,$c7). 0 [] rdf($c7,rdf_first,$c6). 0 [] rdf($c7,rdf_rest,rdf_nil). 0 [] rdf(ns60_Unsatisfiable,owl_intersectionOf,$c3). 0 [] rdf($c8,rdf_type,owl_Restriction). 0 [] rdf($c8,owl_onProperty,ns63_P_2E1). 0 [] rdf($c8,owl_minCardinality,lit1). 0 [] rdf(ns63_C_2E1,owl_equivalentClass,$c8). 0 [] rdf($c9,rdf_type,rdf_List). 0 [] rdf($c9,rdf_first,ns60_c1). 0 [] rdf($c10,rdf_type,rdf_List). 0 [] rdf($c9,rdf_rest,$c10). 0 [] rdf($c10,rdf_first,ns60_c2). 0 [] rdf($c10,rdf_rest,rdf_nil). 0 [] rdf(ns63_A_2E2,owl_intersectionOf,$c9). 0 [] rdf(ns60_rx2,rdf_type,owl_ObjectProperty). 0 [] rdf(ns60_rx4,rdfs_subPropertyOf,ns60_rx2). 0 [] rdf(ns60_rx,rdf_type,owl_ObjectProperty). 0 [] rdf(ns60_rx4,rdfs_subPropertyOf,ns60_rx). 0 [] rdf(ns60_rx4,rdf_type,owl_FunctionalProperty). 0 [] rdf(ns60_rx1,rdf_type,owl_ObjectProperty). 0 [] rdf(ns60_rx3,rdfs_subPropertyOf,ns60_rx1). 0 [] rdf(ns60_rx3,rdfs_subPropertyOf,ns60_rx). 0 [] rdf(ns60_rx3,rdf_type,owl_FunctionalProperty). 0 [] rdf(ns60_rxa,rdf_type,owl_ObjectProperty). 0 [] rdf(ns60_rx,rdf_type,owl_FunctionalProperty). 0 [] rdf(ns60_rx1a,rdf_type,owl_ObjectProperty). 0 [] rdf(ns60_rx2a,rdf_type,owl_ObjectProperty). 0 [] rdf(ns60_rx3a,rdf_type,owl_ObjectProperty). 0 [] rdf(ns60_rx3a,rdfs_subPropertyOf,ns60_rx1a). 0 [] rdf(ns60_rx3a,rdfs_subPropertyOf,ns60_rxa). 0 [] rdf(ns60_rx3a,rdf_type,owl_FunctionalProperty). 0 [] rdf(ns60_rx4a,rdf_type,owl_ObjectProperty). 0 [] rdf(ns60_rx4a,rdfs_subPropertyOf,ns60_rx2a). 0 [] rdf(ns60_rx4a,rdfs_subPropertyOf,ns60_rxa). 0 [] rdf(ns60_rx4a,rdf_type,owl_FunctionalProperty). 0 [] rdf($c11,rdf_type,ns60_Unsatisfiable). end_of_list. SCAN INPUT: prop=0, horn=0, equality=1, symmetry=0, max_lits=10. This ia a non-Horn set with equality. The strategy will be Knuth-Bendix, ordered hyper_res, factoring, and unit deletion, with positive clauses in sos and nonpositive clauses in usable. dependent: set(knuth_bendix). dependent: set(para_from). dependent: set(para_into). dependent: clear(para_from_right). dependent: clear(para_into_right). dependent: set(para_from_vars). dependent: set(eq_units_both_ways). dependent: set(dynamic_demod_all). dependent: set(dynamic_demod). dependent: set(order_eq). dependent: set(back_demod). dependent: set(lrpo). dependent: set(hyper_res). dependent: set(unit_deletion). dependent: set(factor). ------------> process usable: ** KEPT (pick-wt=11): 1 [] -rdf(x,owl_unionOf,y)| -rdf(z,rdf_type,x)|instanceOfAny(z,y). ** KEPT (pick-wt=11): 2 [] -rdf(x,owl_unionOf,y)|rdf(z,rdf_type,x)| -instanceOfAny(z,y). ** KEPT (pick-wt=18): 3 [] -rdf(x,rdf_first,y)| -rdf(x,rdf_rest,z)| -instanceOfAny(u,x)|rdf(u,rdf_type,y)|instanceOfAny(u,z). ** KEPT (pick-wt=15): 4 [] -rdf(x,rdf_first,y)| -rdf(x,rdf_rest,z)|instanceOfAny(u,x)| -rdf(u,rdf_type,y). ** KEPT (pick-wt=14): 5 [] -rdf(x,rdf_first,y)| -rdf(x,rdf_rest,z)|instanceOfAny(u,x)| -instanceOfAny(u,z). ** KEPT (pick-wt=3): 6 [] -instanceOfAny(x,rdf_nil). ** KEPT (pick-wt=11): 7 [] -rdf(x,owl_oneOf,y)| -rdf(z,rdf_type,x)|inList(z,y). ** KEPT (pick-wt=11): 8 [] -rdf(x,owl_oneOf,y)|rdf(z,rdf_type,x)| -inList(z,y). ** KEPT (pick-wt=18): 9 [] -rdf(x,rdf_first,y)| -rdf(x,rdf_rest,z)| -inList(u,x)|rdf(u,owl_sameAs,y)|inList(u,z). ** KEPT (pick-wt=15): 10 [] -rdf(x,rdf_first,y)| -rdf(x,rdf_rest,z)|inList(u,x)| -rdf(u,owl_sameAs,y). ** KEPT (pick-wt=14): 11 [] -rdf(x,rdf_first,y)| -rdf(x,rdf_rest,z)|inList(u,x)| -inList(u,z). ** KEPT (pick-wt=3): 12 [] -inList(x,rdf_nil). ** KEPT (pick-wt=12): 13 [] -rdf(x,owl_equivalentProperty,y)| -rdf(z,x,u)|rdf(z,y,u). ** KEPT (pick-wt=12): 14 [] -rdf(x,owl_equivalentProperty,y)|rdf(z,x,u)| -rdf(z,y,u). ** KEPT (pick-wt=20): 15 [] rdf(x,owl_equivalentProperty,y)| -rdf($f2(x,y),x,$f1(x,y))| -rdf($f2(x,y),y,$f1(x,y)). ** KEPT (pick-wt=12): 16 [] -rdf(x,rdfs_subPropertyOf,y)| -rdf(z,x,u)|rdf(z,y,u). ** KEPT (pick-wt=12): 17 [] rdf(x,rdfs_subPropertyOf,y)| -rdf($f4(x,y),y,$f3(x,y)). ** KEPT (pick-wt=7): 18 [] -rdf(x,owl_differentFrom,y)|x!=y. ** KEPT (pick-wt=7): 19 [] -rdf(x,owl_differentFrom,y)|y!=x. ** KEPT (pick-wt=11): 20 [] -rdf(x,'foo:succ',y)| -rdf(x,'foo:succ',z)|y=z. ** KEPT (pick-wt=11): 21 [] -rdf(x,'foo:succ',y)| -rdf(z,'foo:succ',y)|x=z. ** KEPT (pick-wt=6): 22 [] -maxCardinality(x,i0)| -item(y,x). ** KEPT (pick-wt=12): 23 [] -maxCardinality(x,i1)|y=z| -item(y,x)| -item(z,x). ** KEPT (pick-wt=8): 24 [] maxCardinality(x,i1)|$f7(x)!=$f6(x). ** KEPT (pick-wt=30): 25 [] -maxCardinality(x,i2)|y=z|y=u|z=u|z=y|u=y|u=z| -item(y,x)| -item(z,x)| -item(u,x). ** KEPT (pick-wt=8): 27 [copy,26,flip.2] maxCardinality(x,i2)|$f9(x)!=$f10(x). ** KEPT (pick-wt=8): 29 [copy,28,flip.2] maxCardinality(x,i2)|$f8(x)!=$f10(x). ** KEPT (pick-wt=8): 30 [] maxCardinality(x,i2)|$f9(x)!=$f8(x). Following clause subsumed by 27 during input processing: 0 [] maxCardinality(x,i2)|$f9(x)!=$f10(x). Following clause subsumed by 29 during input processing: 0 [] maxCardinality(x,i2)|$f8(x)!=$f10(x). Following clause subsumed by 30 during input processing: 0 [flip.2] maxCardinality(x,i2)|$f9(x)!=$f8(x). ** KEPT (pick-wt=7): 31 [] -minCardinality(x,i1)|item($f11(x),x). ** KEPT (pick-wt=6): 32 [] minCardinality(x,i1)| -item(y,x). ** KEPT (pick-wt=8): 33 [] -minCardinality(x,i2)|$f13(x)!=$f12(x). ** KEPT (pick-wt=7): 34 [] -minCardinality(x,i2)|item($f13(x),x). ** KEPT (pick-wt=7): 35 [] -minCardinality(x,i2)|item($f12(x),x). ** KEPT (pick-wt=12): 36 [] minCardinality(x,i2)|y=z| -item(y,x)| -item(z,x). ** KEPT (pick-wt=8): 37 [] -minCardinality(x,i2)|$f15(x)!=$f14(x). ** KEPT (pick-wt=7): 38 [] -minCardinality(x,i2)|item($f15(x),x). ** KEPT (pick-wt=7): 39 [] -minCardinality(x,i2)|item($f14(x),x). Following clause subsumed by 36 during input processing: 0 [] minCardinality(x,i2)|y=z| -item(y,x)| -item(z,x). ** KEPT (pick-wt=8): 40 [] -minCardinality(x,i3)|$f18(x)!=$f17(x). ** KEPT (pick-wt=8): 41 [] -minCardinality(x,i3)|$f17(x)!=$f16(x). ** KEPT (pick-wt=8): 42 [] -minCardinality(x,i3)|$f18(x)!=$f16(x). ** KEPT (pick-wt=7): 43 [] -minCardinality(x,i3)|item($f18(x),x). ** KEPT (pick-wt=7): 44 [] -minCardinality(x,i3)|item($f17(x),x). ** KEPT (pick-wt=7): 45 [] -minCardinality(x,i3)|item($f16(x),x). ** KEPT (pick-wt=21): 46 [] minCardinality(x,i3)|y=z|z=u|y=u| -item(y,x)| -item(z,x)| -item(u,x). ** KEPT (pick-wt=27): 47 [] -rdf(x,rdf_type,owl_Restriction)| -rdf(x,owl_onProperty,y)| -rdf(x,owl_cardinality,z)| -rdf(u,rdf_type,x)| -rdf(u,y,v)|item(v,$f19(x,y,z,u)). ** KEPT (pick-wt=23): 48 [] -rdf(x,rdf_type,owl_Restriction)| -rdf(x,owl_onProperty,y)| -rdf(x,owl_cardinality,z)| -rdf(u,rdf_type,x)|minCardinality($f19(x,y,z,u),z). ** KEPT (pick-wt=23): 49 [] -rdf(x,rdf_type,owl_Restriction)| -rdf(x,owl_onProperty,y)| -rdf(x,owl_cardinality,z)| -rdf(u,rdf_type,x)|maxCardinality($f19(x,y,z,u),z). ** KEPT (pick-wt=27): 50 [] -rdf(x,rdf_type,owl_Restriction)| -rdf(x,owl_onProperty,y)| -rdf(x,owl_maxCardinality,z)| -rdf(u,rdf_type,x)| -rdf(u,y,v)|item(v,$f20(x,y,z,u)). ** KEPT (pick-wt=23): 51 [] -rdf(x,rdf_type,owl_Restriction)| -rdf(x,owl_onProperty,y)| -rdf(x,owl_maxCardinality,z)| -rdf(u,rdf_type,x)|maxCardinality($f20(x,y,z,u),z). ** KEPT (pick-wt=27): 52 [] -rdf(x,rdf_type,owl_Restriction)| -rdf(x,owl_onProperty,y)| -rdf(x,owl_minCardinality,z)| -rdf(u,rdf_type,x)| -rdf(u,y,v)|item(v,$f21(x,y,z,u)). ** KEPT (pick-wt=23): 53 [] -rdf(x,rdf_type,owl_Restriction)| -rdf(x,owl_onProperty,y)| -rdf(x,owl_minCardinality,z)| -rdf(u,rdf_type,x)|minCardinality($f21(x,y,z,u),z). ** KEPT (pick-wt=19): 54 [] -rdf(x,owl_onProperty,y)| -rdf(x,owl_cardinality,z)| -rdf(u,rdfs_subClassOf,x)|rdf($f23(y,u,z),owl_onProperty,y). ** KEPT (pick-wt=19): 55 [] -rdf(x,owl_onProperty,y)| -rdf(x,owl_cardinality,z)| -rdf(u,rdfs_subClassOf,x)|rdf($f23(y,u,z),owl_maxCardinality,z). ** KEPT (pick-wt=19): 56 [] -rdf(x,owl_onProperty,y)| -rdf(x,owl_cardinality,z)| -rdf(u,rdfs_subClassOf,x)|rdf($f22(y,u,z),owl_onProperty,y). ** KEPT (pick-wt=19): 57 [] -rdf(x,owl_onProperty,y)| -rdf(x,owl_cardinality,z)| -rdf(u,rdfs_subClassOf,x)|rdf($f22(y,u,z),owl_minCardinality,z). ** KEPT (pick-wt=19): 58 [] -rdf(x,owl_onProperty,y)| -rdf(x,owl_cardinality,z)| -rdf(u,rdfs_subClassOf,x)|rdf(u,rdfs_subClassOf,$f23(y,u,z)). ** KEPT (pick-wt=19): 59 [] -rdf(x,owl_onProperty,y)| -rdf(x,owl_cardinality,z)| -rdf(u,rdfs_subClassOf,x)|rdf(u,rdfs_subClassOf,$f22(y,u,z)). ** KEPT (pick-wt=31): 60 [] rdf($f24(x,y,z),owl_onProperty,x)| -rdf(u,owl_onProperty,x)| -rdf(u,owl_maxCardinality,z)| -rdf(v,owl_onProperty,x)| -rdf(v,owl_minCardinality,z)| -rdf(y,rdfs_subClassOf,u)| -rdf(y,rdfs_subClassOf,v). ** KEPT (pick-wt=31): 61 [] rdf($f24(x,y,z),owl_cardinality,z)| -rdf(u,owl_onProperty,x)| -rdf(u,owl_maxCardinality,z)| -rdf(v,owl_onProperty,x)| -rdf(v,owl_minCardinality,z)| -rdf(y,rdfs_subClassOf,u)| -rdf(y,rdfs_subClassOf,v). ** KEPT (pick-wt=31): 62 [] rdf(x,rdfs_subClassOf,$f24(y,x,z))| -rdf(u,owl_onProperty,y)| -rdf(u,owl_maxCardinality,z)| -rdf(v,owl_onProperty,y)| -rdf(v,owl_minCardinality,z)| -rdf(x,rdfs_subClassOf,u)| -rdf(x,rdfs_subClassOf,v). ** KEPT (pick-wt=8): 63 [] -rdf(x,owl_onProperty,y)|rdf(x,rdf_type,owl_Restriction). ** KEPT (pick-wt=4): 64 [] -rdf(rdf_nil,rdf_rest,x). ** KEPT (pick-wt=4): 65 [] -rdf(rdf_nil,rdf_first,x). ** KEPT (pick-wt=4): 66 [] -rdf(x,rdf_type,owl_Nothing). ** KEPT (pick-wt=11): 67 [] -rdf(x,owl_intersectionOf,y)| -rdf(z,rdf_type,x)|instanceOfAll(z,y). ** KEPT (pick-wt=11): 68 [] -rdf(x,owl_intersectionOf,y)|rdf(z,rdf_type,x)| -instanceOfAll(z,y). ** KEPT (pick-wt=15): 69 [] -rdf(x,rdf_first,y)| -rdf(x,rdf_rest,z)| -instanceOfAll(u,x)|rdf(u,rdf_type,y). ** KEPT (pick-wt=14): 70 [] -rdf(x,rdf_first,y)| -rdf(x,rdf_rest,z)| -instanceOfAll(u,x)|instanceOfAll(u,z). ** KEPT (pick-wt=18): 71 [] -rdf(x,rdf_first,y)| -rdf(x,rdf_rest,z)|instanceOfAll(u,x)| -rdf(u,rdf_type,y)| -instanceOfAll(u,z). ** KEPT (pick-wt=12): 72 [] -rdf(x,owl_equivalentClass,y)| -rdf(z,rdf_type,x)|rdf(z,rdf_type,y). ** KEPT (pick-wt=12): 73 [] -rdf(x,owl_equivalentClass,y)|rdf(z,rdf_type,x)| -rdf(z,rdf_type,y). ** KEPT (pick-wt=16): 74 [] rdf(x,owl_equivalentClass,y)| -rdf($f25(x,y),rdf_type,x)| -rdf($f25(x,y),rdf_type,y). ** KEPT (pick-wt=12): 75 [] -rdf(x,rdfs_subClassOf,y)| -rdf(z,rdf_type,x)|rdf(z,rdf_type,y). ** KEPT (pick-wt=10): 76 [] rdf(x,rdfs_subClassOf,y)| -rdf($f26(x,y),rdf_type,y). ** KEPT (pick-wt=8): 77 [] -rdf(x,owl_equivalentClass,y)|rdf(x,rdfs_subClassOf,y). ** KEPT (pick-wt=12): 78 [] -rdf(x,rdfs_subClassOf,y)| -rdf(y,rdfs_subClassOf,x)|rdf(x,owl_equivalentClass,y). ** KEPT (pick-wt=12): 79 [] -rdf(x,owl_complementOf,y)| -rdf(z,rdf_type,x)| -rdf(z,rdf_type,y). ** KEPT (pick-wt=12): 80 [] -rdf(x,owl_complementOf,y)|rdf(z,rdf_type,x)|rdf(z,rdf_type,y). ** KEPT (pick-wt=16): 81 [] rdf(x,owl_complementOf,y)|rdf($f27(x,y),rdf_type,x)| -rdf($f27(x,y),rdf_type,y). ** KEPT (pick-wt=16): 82 [] rdf(x,owl_complementOf,y)| -rdf($f27(x,y),rdf_type,x)|rdf($f27(x,y),rdf_type,y). ** KEPT (pick-wt=12): 83 [] -rdf(x,owl_disjointWith,y)| -rdf(z,rdf_type,x)| -rdf(z,rdf_type,y). Following clause subsumed by 75 during input processing: 0 [] -rdf(x,rdfs_subClassOf,y)| -rdf(z,rdf_type,x)|rdf(z,rdf_type,y). ** KEPT (pick-wt=24): 84 [] -rdf(x,rdf_type,owl_Restriction)| -rdf(x,owl_onProperty,y)| -rdf(x,owl_allValuesFrom,z)| -rdf(u,rdf_type,x)| -rdf(u,y,v)|rdf(v,rdf_type,z). ** KEPT (pick-wt=24): 85 [] -rdf(x,rdf_type,owl_Restriction)| -rdf(x,owl_onProperty,y)| -rdf(x,owl_allValuesFrom,z)| -rdf(u,rdf_type,x)|rdf(u,y,v)| -rdf(v,rdf_type,z). ** KEPT (pick-wt=22): 86 [] -rdf(x,rdf_type,owl_Restriction)| -rdf(x,owl_onProperty,y)| -rdf(x,owl_someValuesFrom,z)| -rdf(u,rdf_type,x)|rdf(u,y,valueSkFunc(u,x)). ** KEPT (pick-wt=22): 87 [] -rdf(x,rdf_type,owl_Restriction)| -rdf(x,owl_onProperty,y)| -rdf(x,owl_someValuesFrom,z)| -rdf(u,rdf_type,x)|rdf(valueSkFunc(u,x),rdf_type,z). ** KEPT (pick-wt=20): 88 [] -rdf(x,rdf_type,owl_Restriction)| -rdf(x,owl_onProperty,y)| -rdf(x,owl_hasValue,z)| -rdf(u,rdf_type,x)|rdf(u,y,z). ** KEPT (pick-wt=16): 89 [] -rdf(x,rdf_type,owl_FunctionalProperty)| -rdf(y,x,z)| -rdf(y,x,u)|rdf(z,owl_sameAs,u). ** KEPT (pick-wt=10): 90 [] rdf(x,rdf_type,owl_FunctionalProperty)| -rdf($f29(x),owl_sameAs,$f28(x)). ** KEPT (pick-wt=16): 91 [] -rdf(x,rdf_type,owl_InverseFunctionalProperty)| -rdf(y,x,z)| -rdf(u,x,z)|rdf(y,owl_sameAs,u). ** KEPT (pick-wt=10): 92 [] rdf(x,rdf_type,owl_InverseFunctionalProperty)| -rdf($f33(x),owl_sameAs,$f32(x)). ** KEPT (pick-wt=8): 93 [] -rdf(x,owl_sameAs,y)|rdf(y,owl_sameAs,x). ** KEPT (pick-wt=12): 94 [] -rdf(x,owl_sameAs,y)| -rdf(y,owl_sameAs,z)|rdf(x,owl_sameAs,z). ** KEPT (pick-wt=12): 95 [] -rdf(x,owl_sameAs,y)| -rdf(z,u,x)|rdf(z,u,y). ** KEPT (pick-wt=12): 96 [] -rdf(x,owl_sameAs,y)|rdf(z,u,x)| -rdf(z,u,y). ** KEPT (pick-wt=12): 97 [] -rdf(x,owl_sameAs,y)| -rdf(z,x,u)|rdf(z,y,u). ** KEPT (pick-wt=12): 98 [] -rdf(x,owl_sameAs,y)|rdf(z,x,u)| -rdf(z,y,u). ** KEPT (pick-wt=12): 99 [] -rdf(x,owl_sameAs,y)| -rdf(x,z,u)|rdf(y,z,u). ** KEPT (pick-wt=12): 100 [] -rdf(x,owl_sameAs,y)|rdf(x,z,u)| -rdf(y,z,u). ** KEPT (pick-wt=8): 101 [] -rdf(x,owl_differentFrom,y)|rdf(y,owl_differentFrom,x). ** KEPT (pick-wt=8): 102 [] -rdf(x,owl_differentFrom,y)| -rdf(x,owl_sameAs,y). ** KEPT (pick-wt=12): 103 [] -rdf(x,rdfs_range,y)| -rdf(z,x,u)|rdf(u,rdf_type,y). ** KEPT (pick-wt=10): 104 [] rdf(x,rdfs_range,y)| -rdf($f34(x,y),rdf_type,y). ** KEPT (pick-wt=12): 105 [] -rdf(x,rdfs_domain,y)| -rdf(z,x,u)|rdf(z,rdf_type,y). ** KEPT (pick-wt=10): 106 [] rdf(x,rdfs_domain,y)| -rdf($f37(x,y),rdf_type,y). ** KEPT (pick-wt=12): 107 [] -rdf(x,owl_inverseOf,y)| -rdf(z,x,u)|rdf(u,y,z). ** KEPT (pick-wt=12): 108 [] -rdf(x,owl_inverseOf,y)|rdf(z,x,u)| -rdf(u,y,z). ** KEPT (pick-wt=12): 109 [] -rdf(x,rdf_type,owl_SymmetricProperty)| -rdf(y,x,z)|rdf(z,x,y). Following clause subsumed by 109 during input processing: 0 [] -rdf(x,rdf_type,owl_SymmetricProperty)|rdf(y,x,z)| -rdf(z,x,y). ** KEPT (pick-wt=16): 110 [] -rdf(x,rdf_type,owl_TransitiveProperty)| -rdf(y,x,z)| -rdf(z,x,u)|rdf(y,x,u). ** KEPT (pick-wt=12): 111 [] -rdf(x,rdf_type,owl_TransitiveProperty)|rdf(y,x,z)| -rdf(y,x,u). ** KEPT (pick-wt=12): 112 [] -rdf(x,rdf_type,owl_TransitiveProperty)|rdf(y,x,z)| -rdf(u,x,z). ** KEPT (pick-wt=9): 113 [] -rdf(x,rdf_type,owl_AllDifferent)|rdf(x,owl_distinctMembers,$f38(x)). ** KEPT (pick-wt=8): 114 [] rdf(x,rdf_type,owl_AllDifferent)| -rdf(x,owl_distinctMembers,y). ** KEPT (pick-wt=6): 115 [] -rdf(x,owl_distinctMembers,y)|allDifferent(y). ** KEPT (pick-wt=13): 116 [] -allDifferent(x)| -rdf(x,rdf_first,y)| -rdf(x,rdf_rest,z)|differentFromAll(y,z). ** KEPT (pick-wt=15): 117 [] -differentFromAll(x,y)| -rdf(y,rdf_first,z)| -rdf(y,rdf_rest,u)|rdf(x,owl_differentFrom,z). ** KEPT (pick-wt=14): 118 [] -differentFromAll(x,y)| -rdf(y,rdf_first,z)| -rdf(y,rdf_rest,u)|differentFromAll(x,u). Following clause subsumed by 101 during input processing: 0 [] -rdf(x,owl_differentFrom,y)|rdf(y,owl_differentFrom,x). ** KEPT (pick-wt=12): 119 [] -rdf(x,owl_inverseOf,y)| -rdf(x,rdf_type,owl_FunctionalProperty)|rdf(y,rdf_type,owl_InverseFunctionalProperty). ** KEPT (pick-wt=12): 120 [] -rdf(x,owl_inverseOf,y)| -rdf(x,rdf_type,owl_InverseFunctionalProperty)|rdf(y,rdf_type,owl_FunctionalProperty). ** KEPT (pick-wt=20): 121 [] -rdf(x,rdf_type,y)| -rdf(y,owl_unionOf,z)| -rdf(z,rdf_first,u)| -rdf(z,rdf_rest,rdf_nil)|rdf(x,rdf_type,u). ** KEPT (pick-wt=32): 122 [] -rdf(x,rdf_type,y)| -rdf(y,owl_unionOf,z)| -rdf(z,rdf_first,u)| -rdf(z,rdf_rest,v)| -rdf(v,rdf_first,w)| -rdf(v,rdf_rest,rdf_nil)|rdf(x,rdf_type,u)|rdf(x,rdf_type,w). 95 back subsumes 94. 111 back subsumes 110. ------------> process sos: ** KEPT (pick-wt=20): 204 [] rdf(x,owl_equivalentProperty,y)|rdf($f2(x,y),x,$f1(x,y))|rdf($f2(x,y),y,$f1(x,y)). ** KEPT (pick-wt=12): 205 [] rdf(x,rdfs_subPropertyOf,y)|rdf($f4(x,y),x,$f3(x,y)). ** KEPT (pick-wt=3): 206 [] x=x. ** KEPT (pick-wt=3): 208 [copy,207,flip.1] i0='foo:zero'. ---> New Demodulator: 209 [new_demod,208] i0='foo:zero'. ** KEPT (pick-wt=4): 210 [] rdf('foo:zero','foo:succ',i1). ** KEPT (pick-wt=4): 211 [] rdf(i1,'foo:succ',i2). ** KEPT (pick-wt=4): 212 [] rdf(i2,'foo:succ',i3). ** KEPT (pick-wt=7): 214 [copy,213,demod,209] maxCardinality(x,'foo:zero')|item($f5(x),x). ** KEPT (pick-wt=7): 215 [] maxCardinality(x,i1)|item($f7(x),x). ** KEPT (pick-wt=7): 216 [] maxCardinality(x,i1)|item($f6(x),x). ** KEPT (pick-wt=7): 217 [] maxCardinality(x,i2)|item($f10(x),x). ** KEPT (pick-wt=7): 218 [] maxCardinality(x,i2)|item($f9(x),x). ** KEPT (pick-wt=7): 219 [] maxCardinality(x,i2)|item($f8(x),x). ** KEPT (pick-wt=3): 221 [copy,220,demod,209] minCardinality(x,'foo:zero'). ** KEPT (pick-wt=4): 222 [] rdf(owl_Nothing,rdf_type,owl_Class). ** KEPT (pick-wt=4): 223 [] rdf(x,rdf_type,owl_Thing). ** KEPT (pick-wt=4): 224 [] rdf(x,rdf_type,rdf_Resource). ** KEPT (pick-wt=3): 225 [] instanceOfAll(x,rdf_nil). ** KEPT (pick-wt=16): 226 [] rdf(x,owl_equivalentClass,y)|rdf($f25(x,y),rdf_type,x)|rdf($f25(x,y),rdf_type,y). ** KEPT (pick-wt=10): 227 [] rdf(x,rdfs_subClassOf,y)|rdf($f26(x,y),rdf_type,x). ** KEPT (pick-wt=10): 228 [] rdf(x,rdf_type,owl_FunctionalProperty)|rdf($f30(x),x,$f29(x)). ** KEPT (pick-wt=10): 229 [] rdf(x,rdf_type,owl_FunctionalProperty)|rdf($f30(x),x,$f28(x)). ** KEPT (pick-wt=10): 230 [] rdf(x,rdf_type,owl_InverseFunctionalProperty)|rdf($f33(x),x,$f31(x)). ** KEPT (pick-wt=10): 231 [] rdf(x,rdf_type,owl_InverseFunctionalProperty)|rdf($f32(x),x,$f31(x)). ** KEPT (pick-wt=4): 232 [] rdf(x,owl_sameAs,x). ** KEPT (pick-wt=8): 233 [] rdf(x,owl_differentFrom,y)|rdf(x,owl_sameAs,y). ** KEPT (pick-wt=12): 234 [] rdf(x,rdfs_range,y)|rdf($f35(x,y),x,$f34(x,y)). ** KEPT (pick-wt=12): 235 [] rdf(x,rdfs_domain,y)|rdf($f37(x,y),x,$f36(x,y)). ** KEPT (pick-wt=2): 236 [] allDifferent(rdf_nil). ** KEPT (pick-wt=3): 237 [] differentFromAll(x,rdf_nil). ** KEPT (pick-wt=4): 238 [] rdf('http://www.w3.org/2002/03owlt/description_2Dlogic/inconsistent604',rdf_type,owl_Ontology). ** KEPT (pick-wt=4): 239 [] rdf(ns60_c2,rdf_type,owl_Class). ** KEPT (pick-wt=4): 240 [] rdf(ns60_c1,rdf_type,owl_Class). ** KEPT (pick-wt=4): 241 [] rdf(ns63_C_2E1_2Ecomp,rdf_type,owl_Class). ** KEPT (pick-wt=4): 242 [] rdf($c1,rdf_type,owl_Restriction). ** KEPT (pick-wt=4): 243 [] rdf(ns63_P_2E1,rdf_type,owl_DatatypeProperty). ** KEPT (pick-wt=4): 244 [] rdf($c1,owl_onProperty,ns63_P_2E1). ** KEPT (pick-wt=4): 245 [] rdf($c1,owl_maxCardinality,lit0). ** KEPT (pick-wt=4): 246 [] rdf(ns63_C_2E1_2Ecomp,owl_equivalentClass,$c1). ** KEPT (pick-wt=4): 247 [] rdf($c2,rdf_type,owl_Restriction). ** KEPT (pick-wt=4): 248 [] rdf(ns60_rx3,rdf_type,owl_ObjectProperty). ** KEPT (pick-wt=4): 249 [] rdf($c2,owl_onProperty,ns60_rx3). ** KEPT (pick-wt=4): 250 [] rdf(ns63_A_2E2,rdf_type,owl_Class). ** KEPT (pick-wt=4): 251 [] rdf($c2,owl_someValuesFrom,ns63_A_2E2). ** KEPT (pick-wt=4): 252 [] rdf(ns63_C_2E1_2Ecomp,owl_equivalentClass,$c2). ** KEPT (pick-wt=4): 253 [] rdf(ns60_Unsatisfiable,rdf_type,owl_Class). ** KEPT (pick-wt=4): 254 [] rdf(ns63_C_2E1,rdf_type,owl_Class). ** KEPT (pick-wt=4): 255 [] rdf($c3,rdf_type,rdf_List). ** KEPT (pick-wt=4): 256 [] rdf($c3,rdf_first,ns63_C_2E1). ** KEPT (pick-wt=4): 257 [] rdf($c4,rdf_type,owl_Restriction). ** KEPT (pick-wt=4): 258 [] rdf($c4,owl_onProperty,ns60_rx3). ** KEPT (pick-wt=4): 259 [] rdf($c4,owl_someValuesFrom,ns60_c1). ** KEPT (pick-wt=4): 260 [] rdf($c5,rdf_type,rdf_List). ** KEPT (pick-wt=4): 261 [] rdf($c3,rdf_rest,$c5). ** KEPT (pick-wt=4): 262 [] rdf($c5,rdf_first,$c4). ** KEPT (pick-wt=4): 263 [] rdf($c6,rdf_type,owl_Restriction). ** KEPT (pick-wt=4): 264 [] rdf(ns60_rx4,rdf_type,owl_ObjectProperty). ** KEPT (pick-wt=4): 265 [] rdf($c6,owl_onProperty,ns60_rx4). ** KEPT (pick-wt=4): 266 [] rdf($c6,owl_someValuesFrom,ns60_c2). ** KEPT (pick-wt=4): 267 [] rdf($c7,rdf_type,rdf_List). ** KEPT (pick-wt=4): 268 [] rdf($c5,rdf_rest,$c7). ** KEPT (pick-wt=4): 269 [] rdf($c7,rdf_first,$c6). ** KEPT (pick-wt=4): 270 [] rdf($c7,rdf_rest,rdf_nil). ** KEPT (pick-wt=4): 271 [] rdf(ns60_Unsatisfiable,owl_intersectionOf,$c3). ** KEPT (pick-wt=4): 272 [] rdf($c8,rdf_type,owl_Restriction). ** KEPT (pick-wt=4): 273 [] rdf($c8,owl_onProperty,ns63_P_2E1). ** KEPT (pick-wt=4): 274 [] rdf($c8,owl_minCardinality,lit1). ** KEPT (pick-wt=4): 275 [] rdf(ns63_C_2E1,owl_equivalentClass,$c8). ** KEPT (pick-wt=4): 276 [] rdf($c9,rdf_type,rdf_List). ** KEPT (pick-wt=4): 277 [] rdf($c9,rdf_first,ns60_c1). ** KEPT (pick-wt=4): 278 [] rdf($c10,rdf_type,rdf_List). ** KEPT (pick-wt=4): 279 [] rdf($c9,rdf_rest,$c10). ** KEPT (pick-wt=4): 280 [] rdf($c10,rdf_first,ns60_c2). ** KEPT (pick-wt=4): 281 [] rdf($c10,rdf_rest,rdf_nil). ** KEPT (pick-wt=4): 282 [] rdf(ns63_A_2E2,owl_intersectionOf,$c9). ** KEPT (pick-wt=4): 283 [] rdf(ns60_rx2,rdf_type,owl_ObjectProperty). ** KEPT (pick-wt=4): 284 [] rdf(ns60_rx4,rdfs_subPropertyOf,ns60_rx2). ** KEPT (pick-wt=4): 285 [] rdf(ns60_rx,rdf_type,owl_ObjectProperty). ** KEPT (pick-wt=4): 286 [] rdf(ns60_rx4,rdfs_subPropertyOf,ns60_rx). ** KEPT (pick-wt=4): 287 [] rdf(ns60_rx4,rdf_type,owl_FunctionalProperty). ** KEPT (pick-wt=4): 288 [] rdf(ns60_rx1,rdf_type,owl_ObjectProperty). ** KEPT (pick-wt=4): 289 [] rdf(ns60_rx3,rdfs_subPropertyOf,ns60_rx1). ** KEPT (pick-wt=4): 290 [] rdf(ns60_rx3,rdfs_subPropertyOf,ns60_rx). ** KEPT (pick-wt=4): 291 [] rdf(ns60_rx3,rdf_type,owl_FunctionalProperty). ** KEPT (pick-wt=4): 292 [] rdf(ns60_rxa,rdf_type,owl_ObjectProperty). ** KEPT (pick-wt=4): 293 [] rdf(ns60_rx,rdf_type,owl_FunctionalProperty). ** KEPT (pick-wt=4): 294 [] rdf(ns60_rx1a,rdf_type,owl_ObjectProperty). ** KEPT (pick-wt=4): 295 [] rdf(ns60_rx2a,rdf_type,owl_ObjectProperty). ** KEPT (pick-wt=4): 296 [] rdf(ns60_rx3a,rdf_type,owl_ObjectProperty). ** KEPT (pick-wt=4): 297 [] rdf(ns60_rx3a,rdfs_subPropertyOf,ns60_rx1a). ** KEPT (pick-wt=4): 298 [] rdf(ns60_rx3a,rdfs_subPropertyOf,ns60_rxa). ** KEPT (pick-wt=4): 299 [] rdf(ns60_rx3a,rdf_type,owl_FunctionalProperty). ** KEPT (pick-wt=4): 300 [] rdf(ns60_rx4a,rdf_type,owl_ObjectProperty). ** KEPT (pick-wt=4): 301 [] rdf(ns60_rx4a,rdfs_subPropertyOf,ns60_rx2a). ** KEPT (pick-wt=4): 302 [] rdf(ns60_rx4a,rdfs_subPropertyOf,ns60_rxa). ** KEPT (pick-wt=4): 303 [] rdf(ns60_rx4a,rdf_type,owl_FunctionalProperty). ** KEPT (pick-wt=4): 304 [] rdf($c11,rdf_type,ns60_Unsatisfiable). Following clause subsumed by 206 during input processing: 0 [copy,206,flip.1] x=x. 206 back subsumes 132. 206 back subsumes 131. 206 back subsumes 130. 206 back subsumes 129. 206 back subsumes 128. 206 back subsumes 127. >>>> Starting back demodulation with 209. >> back demodulating 22 with 209. 232 back subsumes 203. 232 back subsumes 202. 232 back subsumes 180. 232 back subsumes 177. 232 back subsumes 176. 232 back subsumes 173. ======= end of input processing ======= =========== start of search =========== given clause #1: (wt=20) 204 [] rdf(x,owl_equivalentProperty,y)|rdf($f2(x,y),x,$f1(x,y))|rdf($f2(x,y),y,$f1(x,y)). given clause #2: (wt=2) 236 [] allDifferent(rdf_nil). given clause #3: (wt=3) 206 [] x=x. given clause #4: (wt=3) 208 [copy,207,flip.1] i0='foo:zero'. given clause #5: (wt=3) 221 [copy,220,demod,209] minCardinality(x,'foo:zero'). given clause #6: (wt=12) 205 [] rdf(x,rdfs_subPropertyOf,y)|rdf($f4(x,y),x,$f3(x,y)). given clause #7: (wt=3) 225 [] instanceOfAll(x,rdf_nil). given clause #8: (wt=3) 237 [] differentFromAll(x,rdf_nil). given clause #9: (wt=4) 210 [] rdf('foo:zero','foo:succ',i1). given clause #10: (wt=4) 211 [] rdf(i1,'foo:succ',i2). given clause #11: (wt=4) 212 [] rdf(i2,'foo:succ',i3). given clause #12: (wt=4) 222 [] rdf(owl_Nothing,rdf_type,owl_Class). given clause #13: (wt=4) 223 [] rdf(x,rdf_type,owl_Thing). given clause #14: (wt=4) 224 [] rdf(x,rdf_type,rdf_Resource). given clause #15: (wt=4) 232 [] rdf(x,owl_sameAs,x). given clause #16: (wt=7) 214 [copy,213,demod,209] maxCardinality(x,'foo:zero')|item($f5(x),x). given clause #17: (wt=4) 238 [] rdf('http://www.w3.org/2002/03owlt/description_2Dlogic/inconsistent604',rdf_type,owl_Ontology). given clause #18: (wt=4) 239 [] rdf(ns60_c2,rdf_type,owl_Class). given clause #19: (wt=4) 240 [] rdf(ns60_c1,rdf_type,owl_Class). given clause #20: (wt=4) 241 [] rdf(ns63_C_2E1_2Ecomp,rdf_type,owl_Class). given clause #21: (wt=7) 215 [] maxCardinality(x,i1)|item($f7(x),x). given clause #22: (wt=4) 242 [] rdf($c1,rdf_type,owl_Restriction). given clause #23: (wt=4) 243 [] rdf(ns63_P_2E1,rdf_type,owl_DatatypeProperty). given clause #24: (wt=4) 244 [] rdf($c1,owl_onProperty,ns63_P_2E1). given clause #25: (wt=4) 245 [] rdf($c1,owl_maxCardinality,lit0). given clause #26: (wt=7) 216 [] maxCardinality(x,i1)|item($f6(x),x). given clause #27: (wt=4) 246 [] rdf(ns63_C_2E1_2Ecomp,owl_equivalentClass,$c1). given clause #28: (wt=4) 247 [] rdf($c2,rdf_type,owl_Restriction). given clause #29: (wt=4) 248 [] rdf(ns60_rx3,rdf_type,owl_ObjectProperty). given clause #30: (wt=4) 249 [] rdf($c2,owl_onProperty,ns60_rx3). given clause #31: (wt=7) 217 [] maxCardinality(x,i2)|item($f10(x),x). given clause #32: (wt=4) 250 [] rdf(ns63_A_2E2,rdf_type,owl_Class). given clause #33: (wt=4) 251 [] rdf($c2,owl_someValuesFrom,ns63_A_2E2). given clause #34: (wt=4) 252 [] rdf(ns63_C_2E1_2Ecomp,owl_equivalentClass,$c2). given clause #35: (wt=4) 253 [] rdf(ns60_Unsatisfiable,rdf_type,owl_Class).