[] = """Euler-1.4.18 30 Oct 2005 14:42:55 GMT ----- Prover9 July-2005C, 7 July 2005 ----- Process 2588 was started by amdus on vam1627, Sun Oct 30 15:42:54 2005 The command was "prover9 -f C:\DOCUME~1\amdus.BE\LOCALS~1\Temp\prover9.in". % Reading from file C:\DOCUME~1\amdus.BE\LOCALS~1\Temp\prover9.in set(auto). % set(auto) -> set(auto1). % set(auto1) -> set(auto_inference). % set(auto1) -> set(fof_reduction). % set(auto1) -> set(predicate_elimination). % set(auto1) -> set(unfold_eq). % set(unfold_eq) -> assign(unfold_eq_limit, 2147483647). % set(unfold_eq) -> clear(fold_eq). % set(auto1) -> set(inverse_order). % set(auto1) -> assign(new_constants, 1). % assign(new_constants, 1) -> clear(x_proofs). % assign(new_constants, 1) -> clear(rx_proofs). % set(auto1) -> assign(lex_dep_demod_lim, 11). % set(auto1) -> set(lex_dep_demod_sane). % set(auto1) -> assign(max_weight, 100). % set(auto1) -> assign(age_part, 1). % set(auto1) -> assign(weight_part, 2). % set(auto1) -> assign(weight_neg_part, 2). % set(auto1) -> assign(sos_limit, 10000). % set(auto1) -> clear(x_proofs). % set(auto1) -> assign(stats, lots). % set(auto1) -> assign(max_megs, 200). % set(auto1) -> clear(clocks). assign(sos_limit,100000). assign(max_megs,800). set(quiet). clear(print_initial_clauses). clear(print_given). clauses(sos). qname("p0:") = iri("http://eulersharp.sourceforge.net/2003/03swap/rpo-rules#"). qname("q:") = iri("http://www.w3.org/2004/ql#"). qname("list:") = iri("http://www.w3.org/2000/10/swap/list#"). qname("e:") = iri("http://eulersharp.sourceforge.net/2003/03swap/log-rules#"). qname("xsd:") = iri("http://www.w3.org/2001/XMLSchema#"). qname("gc:") = iri("http://www.daml.org/2001/01/gedcom/gedcom#"). qname(":") = iri("http://www.agfa.com/w3c/euler/gedcom-facts#"). qname("log:") = iri("http://www.w3.org/2000/10/swap/log#"). qname("rdfs:") = iri("http://www.w3.org/2000/01/rdf-schema#"). qname("math:") = iri("http://www.w3.org/2000/10/swap/math#"). qname("owl:") = iri("http://www.w3.org/2002/07/owl#"). qname("rdf:") = iri("http://www.w3.org/1999/02/22-rdf-syntax-ns#"). triple(qname(":Frans"),qname("gc:spouseIn"),qname(":dp")). triple(qname(":Frans"),qname("gc:sex"),qname("gc:Male")). triple(qname(":Maria"),qname("gc:spouseIn"),qname(":dp")). triple(qname(":Maria"),qname("gc:sex"),qname("gc:Female")). triple(qname(":Jos"),qname("gc:childIn"),qname(":dp")). triple(qname(":Jos"),qname("gc:sex"),qname("gc:Male")). triple(qname(":Rita"),qname("gc:childIn"),qname(":dp")). triple(qname(":Rita"),qname("gc:sex"),qname("gc:Female")). triple(qname(":Geert"),qname("gc:childIn"),qname(":dp")). triple(qname(":Geert"),qname("gc:sex"),qname("gc:Male")). triple(qname(":Caroline"),qname("gc:childIn"),qname(":dp")). triple(qname(":Caroline"),qname("gc:sex"),qname("gc:Female")). triple(qname(":Dirk"),qname("gc:childIn"),qname(":dp")). triple(qname(":Dirk"),qname("gc:sex"),qname("gc:Male")). triple(qname(":Greta"),qname("gc:childIn"),qname(":dp")). triple(qname(":Greta"),qname("gc:sex"),qname("gc:Female")). triple(qname(":Frans"),qname("owl:differentFrom"),qname(":Maria")). triple(qname(":dp"),qname("owl:distinctMembers"),skf_e69_0_). triple(skf_e69_0_,qname("rdf:first"),qname(":Jos")). triple(skf_e69_0_,qname("rdf:rest"),skf_e89_0_). triple(skf_e89_0_,qname("rdf:first"),qname(":Rita")). triple(skf_e89_0_,qname("rdf:rest"),skf_e106_0_). triple(skf_e106_0_,qname("rdf:first"),qname(":Geert")). triple(skf_e106_0_,qname("rdf:rest"),skf_e120_0_). triple(skf_e120_0_,qname("rdf:first"),qname(":Caroline")). triple(skf_e120_0_,qname("rdf:rest"),skf_e131_0_). triple(skf_e131_0_,qname("rdf:first"),qname(":Dirk")). triple(skf_e131_0_,qname("rdf:rest"),skf_e139_0_). triple(skf_e139_0_,qname("rdf:first"),qname(":Greta")). triple(skf_e139_0_,qname("rdf:rest"),qname("rdf:nil")). triple(qname(":Jos"),qname("gc:spouseIn"),qname(":dt")). triple(qname(":Jos"),qname("gc:sex"),qname("gc:Male")). triple(qname(":Maaike"),qname("gc:spouseIn"),qname(":dt")). triple(qname(":Maaike"),qname("gc:sex"),qname("gc:Female")). triple(qname(":Goedele"),qname("gc:childIn"),qname(":dt")). triple(qname(":Goedele"),qname("gc:sex"),qname("gc:Female")). triple(qname(":Veerle"),qname("gc:childIn"),qname(":dt")). triple(qname(":Veerle"),qname("gc:sex"),qname("gc:Female")). triple(qname(":Nele"),qname("gc:childIn"),qname(":dt")). triple(qname(":Nele"),qname("gc:sex"),qname("gc:Female")). triple(qname(":Karel"),qname("gc:childIn"),qname(":dt")). triple(qname(":Karel"),qname("gc:sex"),qname("gc:Male")). triple(qname(":Jos"),qname("owl:differentFrom"),qname(":Maaike")). triple(qname(":dt"),qname("owl:distinctMembers"),skf_e192_0_). triple(skf_e192_0_,qname("rdf:first"),qname(":Goedele")). triple(skf_e192_0_,qname("rdf:rest"),skf_e206_0_). triple(skf_e206_0_,qname("rdf:first"),qname(":Veerle")). triple(skf_e206_0_,qname("rdf:rest"),skf_e217_0_). triple(skf_e217_0_,qname("rdf:first"),qname(":Nele")). triple(skf_e217_0_,qname("rdf:rest"),skf_e225_0_). triple(skf_e225_0_,qname("rdf:first"),qname(":Karel")). triple(skf_e225_0_,qname("rdf:rest"),qname("rdf:nil")). triple(qname(":Paul"),qname("gc:spouseIn"),qname(":gd")). triple(qname(":Paul"),qname("gc:sex"),qname("gc:Male")). triple(qname(":Rita"),qname("gc:spouseIn"),qname(":gd")). triple(qname(":Rita"),qname("gc:sex"),qname("gc:Female")). triple(qname(":Ann"),qname("gc:childIn"),qname(":gd")). triple(qname(":Ann"),qname("gc:sex"),qname("gc:Female")). triple(qname(":Bart"),qname("gc:childIn"),qname(":gd")). triple(qname(":Bart"),qname("gc:sex"),qname("gc:Male")). triple(qname(":Paul"),qname("owl:differentFrom"),qname(":Rita")). triple(qname(":gd"),qname("owl:distinctMembers"),skf_e262_0_). triple(skf_e262_0_,qname("rdf:first"),qname(":Ann")). triple(skf_e262_0_,qname("rdf:rest"),skf_e270_0_). triple(skf_e270_0_,qname("rdf:first"),qname(":Bart")). triple(skf_e270_0_,qname("rdf:rest"),qname("rdf:nil")). triple(qname(":Geert"),qname("gc:spouseIn"),qname(":dv")). triple(qname(":Geert"),qname("gc:sex"),qname("gc:Male")). triple(qname(":Christine"),qname("gc:spouseIn"),qname(":dv")). triple(qname(":Christine"),qname("gc:sex"),qname("gc:Female")). triple(qname(":Ann_Sophie"),qname("gc:childIn"),qname(":dv")). triple(qname(":Ann_Sophie"),qname("gc:sex"),qname("gc:Female")). triple(qname(":Valerie"),qname("gc:childIn"),qname(":dv")). triple(qname(":Valerie"),qname("gc:sex"),qname("gc:Female")). triple(qname(":Stephanie"),qname("gc:childIn"),qname(":dv")). triple(qname(":Stephanie"),qname("gc:sex"),qname("gc:Female")). triple(qname(":Louise"),qname("gc:childIn"),qname(":dv")). triple(qname(":Louise"),qname("gc:sex"),qname("gc:Female")). triple(qname(":Geert"),qname("owl:differentFrom"),qname(":Christine")). triple(qname(":dv"),qname("owl:distinctMembers"),skf_e323_0_). triple(skf_e323_0_,qname("rdf:first"),qname(":Ann_Sophie")). triple(skf_e323_0_,qname("rdf:rest"),skf_e337_0_). triple(skf_e337_0_,qname("rdf:first"),qname(":Valerie")). triple(skf_e337_0_,qname("rdf:rest"),skf_e348_0_). triple(skf_e348_0_,qname("rdf:first"),qname(":Stephanie")). triple(skf_e348_0_,qname("rdf:rest"),skf_e356_0_). triple(skf_e356_0_,qname("rdf:first"),qname(":Louise")). triple(skf_e356_0_,qname("rdf:rest"),qname("rdf:nil")). triple(qname(":Hendrik"),qname("gc:spouseIn"),qname(":cd")). triple(qname(":Hendrik"),qname("gc:sex"),qname("gc:Male")). triple(qname(":Caroline"),qname("gc:spouseIn"),qname(":cd")). triple(qname(":Caroline"),qname("gc:sex"),qname("gc:Female")). triple(qname(":Bieke"),qname("gc:childIn"),qname(":cd")). triple(qname(":Bieke"),qname("gc:sex"),qname("gc:Female")). triple(qname(":Tineke"),qname("gc:childIn"),qname(":cd")). triple(qname(":Tineke"),qname("gc:sex"),qname("gc:Female")). triple(qname(":Hendrik"),qname("owl:differentFrom"),qname(":Caroline")). triple(qname(":cd"),qname("owl:distinctMembers"),skf_e393_0_). triple(skf_e393_0_,qname("rdf:first"),qname(":Bieke")). triple(skf_e393_0_,qname("rdf:rest"),skf_e401_0_). triple(skf_e401_0_,qname("rdf:first"),qname(":Tineke")). triple(skf_e401_0_,qname("rdf:rest"),qname("rdf:nil")). triple(qname(":Dirk"),qname("gc:spouseIn"),qname(":dc")). triple(qname(":Dirk"),qname("gc:sex"),qname("gc:Male")). triple(qname(":Karolien"),qname("gc:spouseIn"),qname(":dc")). triple(qname(":Karolien"),qname("gc:sex"),qname("gc:Female")). triple(qname(":Frederik"),qname("gc:childIn"),qname(":dc")). triple(qname(":Frederik"),qname("gc:sex"),qname("gc:Male")). triple(qname(":Stefanie"),qname("gc:childIn"),qname(":dc")). triple(qname(":Stefanie"),qname("gc:sex"),qname("gc:Female")). triple(qname(":Stijn"),qname("gc:childIn"),qname(":dc")). triple(qname(":Stijn"),qname("gc:sex"),qname("gc:Male")). triple(qname(":Dirk"),qname("owl:differentFrom"),qname(":Karolien")). triple(qname(":dc"),qname("owl:distinctMembers"),skf_e446_0_). triple(skf_e446_0_,qname("rdf:first"),qname(":Frederik")). triple(skf_e446_0_,qname("rdf:rest"),skf_e457_0_). triple(skf_e457_0_,qname("rdf:first"),qname(":Stefanie")). triple(skf_e457_0_,qname("rdf:rest"),skf_e465_0_). triple(skf_e465_0_,qname("rdf:first"),qname(":Stijn")). triple(skf_e465_0_,qname("rdf:rest"),qname("rdf:nil")). triple(qname(":Marc"),qname("gc:spouseIn"),qname(":sd")). triple(qname(":Marc"),qname("gc:sex"),qname("gc:Male")). triple(qname(":Greta"),qname("gc:spouseIn"),qname(":sd")). triple(qname(":Greta"),qname("gc:sex"),qname("gc:Female")). triple(qname(":Lien"),qname("gc:childIn"),qname(":sd")). triple(qname(":Lien"),qname("gc:sex"),qname("gc:Female")). triple(qname(":Tom"),qname("gc:childIn"),qname(":sd")). triple(qname(":Tom"),qname("gc:sex"),qname("gc:Male")). triple(qname(":Marc"),qname("owl:differentFrom"),qname(":Greta")). triple(qname(":sd"),qname("owl:distinctMembers"),skf_e502_0_). triple(skf_e502_0_,qname("rdf:first"),qname(":Lien")). triple(skf_e502_0_,qname("rdf:rest"),skf_e510_0_). triple(skf_e510_0_,qname("rdf:first"),qname(":Tom")). triple(skf_e510_0_,qname("rdf:rest"),qname("rdf:nil")). triple(qname("gc:parent"),qname("owl:inverseOf"),qname("gc:child")). triple(qname("gc:grandparent"),qname("owl:inverseOf"),qname("gc:grandchild")). triple(qname("gc:ancestor"),qname("owl:inverseOf"),qname("gc:descendent")). triple(qname("gc:sibling"),qname("rdf:type"),qname("owl:SymmetricProperty")). triple(qname("gc:spouse"),qname("rdf:type"),qname("owl:SymmetricProperty")). triple(qname("gc:ancestor"),qname("rdf:type"),qname("owl:TransitiveProperty")). triple(qname("gc:parent"),qname("rdfs:subPropertyOf"),qname("gc:ancestor")). - triple(x,qname("gc:childIn"),y) | - triple(z,qname("gc:spouseIn"),y) | triple(x,qname("gc:parent"),z). - triple(x,qname("gc:parent"),y) | - triple(y,qname("gc:sex"),qname("gc:Male")) | triple(x,qname("gc:father"),y). - triple(x,qname("gc:parent"),y) | - triple(y,qname("gc:sex"),qname("gc:Female")) | triple(x,qname("gc:mother"),y). - triple(x,qname("gc:parent"),y) | - triple(x,qname("gc:sex"),qname("gc:Male")) | triple(y,qname("gc:son"),x). - triple(x,qname("gc:parent"),y) | - triple(x,qname("gc:sex"),qname("gc:Female")) | triple(y,qname("gc:daughter"),x). - triple(x,qname("gc:parent"),y) | - triple(y,qname("gc:parent"),z) | triple(x,qname("gc:grandparent"),z). - triple(x,qname("gc:grandparent"),y) | - triple(y,qname("gc:sex"),qname("gc:Male")) | triple(x,qname("gc:grandfather"),y). - triple(x,qname("gc:grandparent"),y) | - triple(y,qname("gc:sex"),qname("gc:Female")) | triple(x,qname("gc:grandmother"),y). - triple(x,qname("gc:grandparent"),y) | - triple(x,qname("gc:sex"),qname("gc:Male")) | triple(y,qname("gc:grandson"),x). - triple(x,qname("gc:grandparent"),y) | - triple(x,qname("gc:sex"),qname("gc:Female")) | triple(y,qname("gc:granddaughter"),x). - triple(x,qname("gc:childIn"),y) | - triple(z,qname("gc:childIn"),y) | - triple(x,qname("owl:differentFrom"),z) | triple(x,qname("gc:sibling"),z). - triple(x,qname("gc:sibling"),y) | - triple(y,qname("gc:sex"),qname("gc:Male")) | triple(x,qname("gc:brother"),y). - triple(x,qname("gc:sibling"),y) | - triple(y,qname("gc:sex"),qname("gc:Female")) | triple(x,qname("gc:sister"),y). - triple(x,qname("gc:spouseIn"),y) | - triple(z,qname("gc:spouseIn"),y) | - triple(x,qname("owl:differentFrom"),z) | triple(x,qname("gc:spouse"),z). - triple(x,qname("gc:spouse"),y) | - triple(y,qname("gc:sex"),qname("gc:Male")) | triple(x,qname("gc:husband"),y). - triple(x,qname("gc:spouse"),y) | - triple(y,qname("gc:sex"),qname("gc:Female")) | triple(x,qname("gc:wife"),y). - triple(x,qname("gc:parent"),y) | - triple(y,qname("gc:brother"),z) | triple(x,qname("gc:uncle"),z). - triple(x,qname("gc:parent"),y) | - triple(y,qname("gc:sister"),z) | - triple(z,qname("gc:spouse"),u) | triple(x,qname("gc:uncle"),u). - triple(x,qname("gc:parent"),y) | - triple(y,qname("gc:sister"),z) | triple(x,qname("gc:aunt"),z). - triple(x,qname("gc:parent"),y) | - triple(y,qname("gc:brother"),z) | - triple(z,qname("gc:spouse"),u) | triple(x,qname("gc:aunt"),u). - triple(x,qname("gc:daughter"),y) | - triple(x,qname("gc:sibling"),z) | triple(z,qname("gc:niece"),y). - triple(x,qname("gc:son"),y) | - triple(x,qname("gc:sibling"),z) | triple(z,qname("gc:nephew"),y). - triple(x,qname("gc:parent"),y) | - triple(z,qname("gc:parent"),u) | - triple(y,qname("gc:sibling"),u) | triple(x,qname("gc:firstcousin"),z). - triple(x,qname("gc:sibling"),y) | - triple(x,qname("gc:descendent"),z) | - triple(y,qname("gc:descendent"),u) | triple(z,qname("gc:cousin"),u). triple(iri("file:/euler/rpo-rules.n3"),iri("file:/euler/rpo-rules.n3#rcsid"),"%24Id%3A+rpo-rules.n3%2Cv+1.9+2005%2F10%2F11+21%3A23%3A50+amdus+Exp+%24"). triple(qname("rdfs:subClassOf"),qname("rdfs:domain"),qname("rdfs:Class")). triple(qname("rdfs:subClassOf"),qname("rdfs:range"),qname("rdfs:Class")). triple(qname("rdfs:subClassOf"),qname("rdf:type"),qname("owl:TransitiveProperty")). triple(qname("rdfs:subPropertyOf"),qname("rdfs:domain"),qname("rdf:Property")). triple(qname("rdfs:subPropertyOf"),qname("rdfs:range"),qname("rdf:Property")). triple(qname("rdfs:subPropertyOf"),qname("rdf:type"),qname("owl:TransitiveProperty")). triple(qname("owl:inverseOf"),qname("rdfs:domain"),qname("owl:ObjectProperty")). triple(qname("owl:inverseOf"),qname("rdfs:range"),qname("owl:ObjectProperty")). triple(qname("owl:inverseOf"),qname("rdf:type"),qname("owl:SymmetricProperty")). triple(qname("owl:differentFrom"),qname("rdfs:domain"),qname("owl:Thing")). triple(qname("owl:differentFrom"),qname("rdfs:range"),qname("owl:Thing")). triple(qname("owl:differentFrom"),qname("rdf:type"),qname("owl:SymmetricProperty")). triple(qname("owl:distinctMembers"),qname("rdfs:domain"),qname("owl:AllDifferent")). triple(qname("owl:distinctMembers"),qname("rdfs:range"),qname("rdf:List")). triple(qname("rdf:first"),qname("rdfs:domain"),qname("rdf:List")). triple(qname("rdf:first"),qname("rdfs:range"),qname("rdfs:Resource")). triple(qname("rdf:first"),qname("rdf:type"),qname("owl:FunctionalProperty")). triple(qname("rdf:rest"),qname("rdfs:domain"),qname("rdf:List")). triple(qname("rdf:rest"),qname("rdfs:range"),qname("rdf:List")). triple(qname("rdf:rest"),qname("rdf:type"),qname("owl:FunctionalProperty")). - triple(x,qname("rdfs:domain"),y) | - triple(z,x,u) | triple(z,qname("rdf:type"),y). - triple(x,qname("rdfs:range"),y) | - triple(z,x,u) | triple(u,qname("rdf:type"),y). - triple(x,qname("rdfs:subClassOf"),y) | - triple(z,qname("rdf:type"),x) | triple(z,qname("rdf:type"),y). - triple(x,qname("rdfs:subPropertyOf"),y) | - triple(z,x,u) | triple(z,y,u). - triple(x,qname("owl:inverseOf"),y) | - triple(z,x,u) | triple(u,y,z). - triple(x,qname("rdf:type"),qname("owl:SymmetricProperty")) | - triple(y,x,z) | triple(z,x,y). - triple(x,qname("rdf:type"),qname("owl:TransitiveProperty")) | - triple(y,x,z) | - triple(u,x,y) | triple(u,x,z). - triple(x,qname("rdf:type"),qname("owl:FunctionalProperty")) | - triple(y,x,z) | - triple(y,x,u) | z = u. - triple(x,qname("rdf:type"),qname("owl:InverseFunctionalProperty")) | - triple(y,x,z) | - triple(u,x,z) | y = u. - triple(x,qname("owl:distinctMembers"),y) | - triple(y,qname("rdf:rest"),z) | triple(x,qname("owl:distinctMembers"),z). - triple(x,qname("owl:distinctMembers"),y) | - triple(z,qname("p0:subListOf"),y) | - triple(z,qname("rdf:first"),u) | - triple(z,qname("rdf:rest"),v) | - triple(w,qname("list:in"),v) | triple(u,qname("owl:differentFrom"),w). - triple(x,qname("owl:oneOf"),y) | - triple(z,qname("list:in"),y) | triple(z,qname("rdf:type"),x). - triple(x,qname("rdf:first"),y) | - triple(x,qname("rdf:type"),qname("rdf:List")) | triple(y,qname("list:in"),x). - triple(x,qname("rdf:rest"),y) | - triple(x,qname("rdf:type"),qname("rdf:List")) | - triple(z,qname("list:in"),y) | triple(z,qname("list:in"),x). - triple(x,qname("rdf:type"),qname("rdf:List")) | triple(x,qname("p0:subListOf"),x). - triple(x,qname("rdf:rest"),y) | - triple(x,qname("rdf:type"),qname("rdf:List")) | - triple(z,qname("p0:subListOf"),y) | triple(z,qname("p0:subListOf"),x). - triple(x,qname("owl:intersectionOf"),[y,z]) | - triple([u,y],qname("p0:mu"),v) | - triple([u,z],qname("p0:mu"),w) | - triple(v,qname("math:lessThan"),w) | triple([u,x],qname("p0:mu"),v). - triple(x,qname("owl:intersectionOf"),[y,z]) | - triple([u,y],qname("p0:mu"),v) | - triple([u,z],qname("p0:mu"),w) | - triple(v,qname("math:notLessThan"),w) | triple([u,x],qname("p0:mu"),w). - triple(x,qname("owl:unionOf"),[y,z]) | - triple([u,y],qname("p0:mu"),v) | - triple([u,z],qname("p0:mu"),w) | - triple(v,qname("math:lessThan"),w) | triple([u,x],qname("p0:mu"),w). - triple(x,qname("owl:unionOf"),[y,z]) | - triple([u,y],qname("p0:mu"),v) | - triple([u,z],qname("p0:mu"),w) | - triple(v,qname("math:notLessThan"),w) | triple([u,x],qname("p0:mu"),v). - triple(x,qname("owl:complementOf"),y) | - triple([z,y],qname("p0:mu"),u) | - triple(["1.0",u],qname("math:difference"),v) | triple([z,x],qname("p0:mu"),v). - triple(x,qname("gc:uncle"),y) | - triple(y,qname("gc:mother"),z) | - triple(z,qname("gc:daughter"),u) | - triple(u,qname("gc:son"),x). triple(skf_e1877_3_,qname("e:hint"),"assign%28sos_limit%2C100000%29.assign%28max_megs%2C800%29.set%28quiet%29.clear%28print_initial_clauses%29.clear%28print_given%29."). end_of_list. % Finished reading the input. % Entering prover search function. % Assigned IDs to 221 clauses. % Starting search at 0.07 seconds. % Back_subsumption disabled, ratio of kept to back_subsumed is 2147483647 (0.00 of 0.90 sec). -------- Proof 1 -------- (1.06 + 0.02 seconds) -------- PROOF -------- Length of proof is 58. Maximum clause weight is 30. 236 triple(qname(":Maria"),qname("gc:spouseIn"),qname(":dp")). [input] 237 triple(qname(":Maria"),qname("gc:sex"),qname("gc:Female")). [input] 246 triple(qname(":Dirk"),qname("gc:childIn"),qname(":dp")). [input] 247 triple(qname(":Dirk"),qname("gc:sex"),qname("gc:Male")). [input] 248 triple(qname(":Greta"),qname("gc:childIn"),qname(":dp")). [input] 249 triple(qname(":Greta"),qname("gc:sex"),qname("gc:Female")). [input] 251 triple(qname(":dp"),qname("owl:distinctMembers"),skf_e69_0_). [input] 253 triple(skf_e69_0_,qname("rdf:rest"),skf_e89_0_). [input] 255 triple(skf_e89_0_,qname("rdf:rest"),skf_e106_0_). [input] 257 triple(skf_e106_0_,qname("rdf:rest"),skf_e120_0_). [input] 259 triple(skf_e120_0_,qname("rdf:rest"),skf_e131_0_). [input] 260 triple(skf_e131_0_,qname("rdf:first"),qname(":Dirk")). [input] 261 triple(skf_e131_0_,qname("rdf:rest"),skf_e139_0_). [input] 262 triple(skf_e139_0_,qname("rdf:first"),qname(":Greta")). [input] 263 triple(skf_e139_0_,qname("rdf:rest"),qname("rdf:nil")). [input] 351 triple(qname(":Greta"),qname("gc:spouseIn"),qname(":sd")). [input] 354 triple(qname(":Tom"),qname("gc:childIn"),qname(":sd")). [input] 355 triple(qname(":Tom"),qname("gc:sex"),qname("gc:Male")). [input] 365 triple(qname("gc:sibling"),qname("rdf:type"),qname("owl:SymmetricProperty")). [input] 369 - triple(x,qname("gc:childIn"),y) | - triple(z,qname("gc:spouseIn"),y) | triple(x,qname("gc:parent"),z). [input] 371 - triple(x,qname("gc:parent"),y) | - triple(y,qname("gc:sex"),qname("gc:Female")) | triple(x,qname("gc:mother"),y). [input] 372 - triple(x,qname("gc:parent"),y) | - triple(x,qname("gc:sex"),qname("gc:Male")) | triple(y,qname("gc:son"),x). [input] 373 - triple(x,qname("gc:parent"),y) | - triple(x,qname("gc:sex"),qname("gc:Female")) | triple(y,qname("gc:daughter"),x). [input] 379 - triple(x,qname("gc:childIn"),y) | - triple(z,qname("gc:childIn"),y) | - triple(x,qname("owl:differentFrom"),z) | triple(x,qname("gc:sibling"),z). [input] 380 - triple(x,qname("gc:sibling"),y) | - triple(y,qname("gc:sex"),qname("gc:Male")) | triple(x,qname("gc:brother"),y). [input] 385 - triple(x,qname("gc:parent"),y) | - triple(y,qname("gc:brother"),z) | triple(x,qname("gc:uncle"),z). [input] 411 triple(qname("rdf:rest"),qname("rdfs:domain"),qname("rdf:List")). [input] 414 - triple(x,qname("rdfs:domain"),y) | - triple(z,x,u) | triple(z,qname("rdf:type"),y). [input] 419 - triple(x,qname("rdf:type"),qname("owl:SymmetricProperty")) | - triple(y,x,z) | triple(z,x,y). [input] 423 - triple(x,qname("owl:distinctMembers"),y) | - triple(y,qname("rdf:rest"),z) | triple(x,qname("owl:distinctMembers"),z). [input] 424 - triple(x,qname("owl:distinctMembers"),y) | - triple(z,qname("p0:subListOf"),y) | - triple(z,qname("rdf:first"),u) | - triple(z,qname("rdf:rest"),v) | - triple(w,qname("list:in"),v) | triple(u,qname("owl:differentFrom"),w). [input] 426 - triple(x,qname("rdf:first"),y) | - triple(x,qname("rdf:type"),qname("rdf:List")) | triple(y,qname("list:in"),x). [input] 428 - triple(x,qname("rdf:type"),qname("rdf:List")) | triple(x,qname("p0:subListOf"),x). [input] 429 - triple(x,qname("rdf:rest"),y) | - triple(x,qname("rdf:type"),qname("rdf:List")) | - triple(z,qname("p0:subListOf"),y) | triple(z,qname("p0:subListOf"),x). [input] 435 - triple(x,qname("gc:uncle"),y) | - triple(y,qname("gc:mother"),z) | - triple(z,qname("gc:daughter"),u) | - triple(u,qname("gc:son"),x). [input] 437 triple(qname(":Tom"),qname("gc:parent"),qname(":Greta")). [hyper (369 a 354 a b 351 a)] 471 triple(qname(":Greta"),qname("gc:parent"),qname(":Maria")). [hyper (369 a 248 a b 236 a)] 473 triple(qname(":Dirk"),qname("gc:parent"),qname(":Maria")). [hyper (369 a 246 a b 236 a)] 507 triple(skf_e139_0_,qname("rdf:type"),qname("rdf:List")). [hyper (414 a 411 a b 263 a)] 508 triple(skf_e131_0_,qname("rdf:type"),qname("rdf:List")). [hyper (414 a 411 a b 261 a)] 509 triple(skf_e120_0_,qname("rdf:type"),qname("rdf:List")). [hyper (414 a 411 a b 259 a)] 510 triple(skf_e106_0_,qname("rdf:type"),qname("rdf:List")). [hyper (414 a 411 a b 257 a)] 511 triple(skf_e89_0_,qname("rdf:type"),qname("rdf:List")). [hyper (414 a 411 a b 255 a)] 582 triple(qname(":dp"),qname("owl:distinctMembers"),skf_e89_0_). [hyper (423 a 251 a b 253 a)] 585 triple(qname(":Greta"),qname("gc:son"),qname(":Tom")). [hyper (372 a 437 a b 355 a)] 692 triple(qname(":Greta"),qname("list:in"),skf_e139_0_). [hyper (426 a 262 a b 507 a)] 694 triple(skf_e131_0_,qname("p0:subListOf"),skf_e131_0_). [hyper (428 a 508 a)] 700 triple(skf_e131_0_,qname("p0:subListOf"),skf_e120_0_). [hyper (429 a 259 a b 509 a c 694 a)] 710 triple(skf_e131_0_,qname("p0:subListOf"),skf_e106_0_). [hyper (429 a 257 a b 510 a c 700 a)] 718 triple(skf_e131_0_,qname("p0:subListOf"),skf_e89_0_). [hyper (429 a 255 a b 511 a c 710 a)] 796 triple(qname(":Dirk"),qname("owl:differentFrom"),qname(":Greta")). [hyper (424 a 582 a b 718 a c 260 a d 261 a e 692 a)] 870 triple(qname(":Maria"),qname("gc:daughter"),qname(":Greta")). [hyper (373 a 471 a b 249 a)] 891 triple(qname(":Dirk"),qname("gc:mother"),qname(":Maria")). [hyper (371 a 473 a b 237 a)] 1043 triple(qname(":Dirk"),qname("gc:sibling"),qname(":Greta")). [hyper (379 a 246 a b 248 a c 796 a)] 1137 - triple(qname(":Tom"),qname("gc:uncle"),qname(":Dirk")). [ur (435 b 891 a c 870 a d 585 a)] 1161 - triple(qname(":Greta"),qname("gc:brother"),qname(":Dirk")). [ur (385 a 437 a c 1137 a)] 1179 - triple(qname(":Greta"),qname("gc:sibling"),qname(":Dirk")). [ur (380 b 247 a c 1161 a)] 1188 $F. [ur (419 a 365 a c 1179 a) unit_del (a 1043)] -------- end of proof ------- Given=723. Generated=1291. Kept=966. Proofs=1. Usable=723. Sos=243. Demods=12. Goals=0. Limbo=0, Disabled=221. Hints=0. Weight_deleted=0. Literals_deleted=0. Forward_subsumed=324. Back_subsumed=0. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=12 (0 lex), Back_demodulated=0. Back_unit_deleted=0. Demod_attempts=8744. Demod_rewrites=0. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=1. Nonunit_bsub_feature_tests=47. Megabytes=0.76. User_CPU=1.07, System_CPU=0.02, Wall_clock=1. THEOREM PROVED Exiting with 1 proof. Process 2588 exit (max_proofs) Sun Oct 30 15:42:55 2005 """.