- From: Sandro Hawke <sandro@w3.org>
- Date: Thu, 09 Jan 2003 10:44:45 -0500
- To: connolly@w3.org
- Cc: www-archive@w3.org
[The version of cwm I'm using here is not checked in, because Tim's made some changes I haven't integrated yet.] 1. Negate the conclusion a. Convert to N3 cwm -rdf d24.prem.rdf -n3 d24.nconc.n3 b. Wrap in { } a log:Falsehood. cat d24.nconc.n3 @prefix : <http://example.org/vocab#> . @prefix rdf: <http://www.w3.org/1999/02/22-rdf-syntax-ns#> . @prefix log: <http://www.w3.org/2000/10/swap/log#> . { [ :population "2688418"; :stateBird :WesternMeadowlark; rdf:nodeID "A0" ]. } a log:Falsehood. 2. Run cwm --check on premise, negated-conclusions, and axioms python cwm.py -rdf d24.prem.rdf -n3 d24.nconc.n3 /tmp/ontAx.n3 --check [ I think "--check" should be "--engine=otter --think". ] output includes: # autoprefix ns5 http://example.org/vocab # autoprefix ns6 http://www.w3.org/2002/07/owl leaving ,lx.engine.otter.fromOtter Contradiction found. for details try: cat ,lx.engine.otter.fromOtter First look at ,lx.engine.otter.toOtter, so we what happened to the n3: (the first 4 lines are boilerplate, then 7 lines of premise, then 1 line of negated conclusion, then the axioms....) ================================================================ set(auto). set(prolog_style_variables). clear(control_memory). formula_list(usable). rdf(s, rdf_nodeID, '<md5:d88c146dfafdea37a837778a92415bc2>'). rdf(s, ns5_stateCode, '<md5:a32356331cf2a7f56e45306fc6d328d9>'). rdf(s, ns5_population, '<md5:749b0f41b1f91012db8edab830aacdba>'). rdf(ns5_stateCode, rdf_type, ns6_InverseFunctionalProperty). rdf(s, rdf_nodeID, '<md5:27f237e6b7f96587b6202ff3607ad88a>'). rdf(s, ns5_stateCode, '<md5:a32356331cf2a7f56e45306fc6d328d9>'). rdf(s, ns5_stateBird, ns5_WesternMeadowlark). -(exists s ((rdf(s, ns5_population, '<md5:749b0f41b1f91012db8edab830aacdba>') & rdf(s, ns5_stateBird, ns5_WesternMeadowlark)) & rdf(s, rdf_nodeID, '<md5:d88c146dfafdea37a837778a92415bc2>'))). rdf('<file:/tmp/ontAx.n3>', '<http://purl.org/dc/elements/1.1/description>', '<md5:821f59c4d08564bb37d62c58b49f0d03>'). rdf('<file:/tmp/ontAx.n3>', '<http://purl.org/dc/elements/1.1/description>', '<md5:1f0efb73e107e9313dcc5f6dfbe9892a>'). rdf('<file:/tmp/ontAx.n3>', '<http://purl.org/dc/elements/1.1/source>', '<http://www.w3.org/TR/2002/WD-owl-features-20020729/>'). rdf('<file:/tmp/ontAx.n3>', '<http://purl.org/dc/elements/1.1/source>', '<http://www.agfa.com/w3c/euler/owl-rules>'). rdf('<file:/tmp/ontAx.n3>', rdfs_seeAlso, '<http://www.w3.org/2000/10/swap/util/rdfs-rules.n3>'). rdf(daml_Class, rdfs_label, '<md5:9bd81329febf6efe22788e03ddeaf0af>'). rdf(daml_Class, rdfs_subClassOf, rdfs_Class). rdf(daml_sameClassAs, rdf_type, daml_TransitiveProperty). rdf(daml_sameClassAs, rdf_type, daml_SymmetricProperty). all A B ( rdf(A, daml_sameClassAs, B) <-> rdf(B, rdfs_subClassOf, A) & rdf(A, rdfs_subClassOf, B) ). rdf(daml_samePropertyAs, rdf_type, daml_TransitiveProperty). rdf(daml_samePropertyAs, rdf_type, daml_SymmetricProperty). all A B ( rdf(A, daml_samePropertyAs, B) <-> rdf(B, rdfs_subPropertyOf, A) & rdf(A, rdfs_subPropertyOf, B) ). rdf(daml_sameIndividualAs, rdf_type, daml_TransitiveProperty). rdf(daml_sameIndividualAs, rdf_type, daml_SymmetricProperty). all A B C D ( rdf(A, daml_sameIndividualAs, B) & rdf(A, C, D) -> rdf(B, C, D) ). all A B C D ( rdf(A, daml_sameIndividualAs, B) & rdf(C, D, A) -> rdf(C, D, B) ). rdf(daml_differentIndividualFrom, rdf_type, daml_SymmetricProperty). rdf(daml_differentIndividualFrom, ontAx__converse, daml_sameIndividualAs). rdf(ontAx__converse, rdf_type, daml_SymmetricProperty). all A B C ( -(exists s (rdf(s, ontAx__converse, A) & rdf(B, s, C))) -> rdf(B, A, C) ). all A B C ( (exists s (rdf(s, ontAx__converse, A) & rdf(B, s, C))) -> -rdf(B, A, C) ). rdf(daml_inverseOf, rdf_type, daml_SymmetricProperty). all A B C ( (exists s (rdf(s, daml_inverseOf, A) & rdf(B, s, C))) -> rdf(C, A, B) ). all A B C D ( rdf(A, rdf_type, daml_FunctionalProperty) -> (rdf(B, A, C) & rdf(B, A, D) -> rdf(C, daml_equivalentTo, D)) ). all A B C D ( rdf(A, rdf_type, daml_InverseFunctionalProperty) -> (rdf(B, A, C) & rdf(D, A, C) -> rdf(B, daml_equivalentTo, D)) ). all A B C D ( (exists s (((rdf(s, daml_allValuesFrom, A) & rdf(s, daml_onProperty, B)) & rdf(C, rdf_type, s)) & rdf(C, B, D))) -> rdf(D, rdf_type, A) ). all A B C ( (exists s ((rdf(s, daml_onProperty, A) & rdf(s, daml_someValuesFrom, B)) & rdf(C, rdf_type, s))) -> (exists t (rdf(t, rdf_type, B) & rdf(C, A, t))) ). rdf('<file:/tmp/ontAx.n3>', ontAx_note, '<md5:298e17a6fc6db286af85fedc40e8d132>'). rdf('<file:/tmp/ontAx.n3>', ontAx_note, '<md5:bfbe1f1d0c2a32c63467e34db15b3e38>'). all A B ( (exists s (rdf(s, daml_item, A) & rdf(B, daml_oneOf, s))) -> rdf(A, rdf_type, B) ). all A B C D ( (rdf(A, daml_oneOf, B) & rdf(C, daml_oneOf, D)) & rdf(B, daml_rest, D) -> rdf(C, rdfs_subClassOf, A) ). rdf('<file:/tmp/ontAx.n3>', ontAx_note, '<md5:8425c7c4e78a0b61ca0177cba0fc28fd>'). rdf(daml_first, rdf_type, daml_FunctionalProperty). rdf(daml_rest, rdf_type, daml_FunctionalProperty). all A B ( rdf(A, daml_first, B) -> rdf(A, ontAx__item, B) ). rdf('<file:/tmp/ontAx.n3>', ontAx_note, '<md5:6f05a3e924c4636761b0bddc7ee46f69>'). rdf('<file:/tmp/ontAx.n3>', ontAx_note, '<md5:bcc79261d87a60c1f21ef1b0b91d2692>'). all A B ( rdf(A, daml_equivalentTo, B) -> rdf(B, daml_equivalentTo, A) ). all A B C D ( ((rdf(A, log_notEqualTo, log_forAll) & rdf(A, log_notEqualTo, log_forSome)) & rdf(B, daml_equivalentTo, C)) & rdf(B, A, D) -> rdf(C, A, D) ). all A B C D ( ((rdf(A, daml_equivalentTo, B) & rdf(A, log_notEqualTo, log_forAll)) & rdf(A, log_notEqualTo, log_forSome)) & rdf(C, A, D) -> rdf(C, B, D) ). all A B C D ( ((rdf(A, log_notEqualTo, log_forAll) & rdf(A, log_notEqualTo, log_forSome)) & rdf(B, A, C)) & rdf(C, daml_equivalentTo, D) -> rdf(B, A, D) ). all A B ( rdf(A, daml_sameIndividualAs, B) -> rdf(B, daml_sameIndividualAs, A) ). all A B C ( (exists s (rdf(s, daml_sameIndividualAs, A) & rdf(s, B, C))) -> rdf(A, B, C) ). all A B ( rdf(A, daml_samePropertyAs, B) -> rdf(B, daml_samePropertyAs, A) ). all A B C D ( rdf(A, rdf_type, daml_UnambiguousProperty) -> (rdf(B, A, C) & rdf(D, A, C) -> rdf(B, daml_equivalentTo, D)) ). all A ( rdf(A, rdf_type, daml_Nothing) -> rdf(A, rdf_type, ontAx_SymptomOfInconsistency) ). all A B C D ( (rdf(A, daml_hasValue, B) & rdf(A, daml_onProperty, C)) & rdf(D, C, B) -> rdf(D, rdf_type, A) ). all A B C ( (exists s (exists t (exists u (((((rdf(u, daml_intersectionOf, t) & rdf(t, daml_first, A)) & rdf(t, daml_rest, s)) & rdf(s, daml_first, B)) & rdf(s, daml_rest, daml_nil)) & rdf(C, rdf_type, u))))) -> rdf(C, rdf_type, A) & rdf(C, rdf_type, B) ). all A B ( rdf(A, daml_differentIndividualFrom, B) -> rdf(A, rdf_type, daml_Thing) ). rdf(daml_Nothing, daml_oneOf, daml_nil). rdf(daml_Thing, daml_complementOf, daml_Nothing). all A B C ( (exists s ((rdf(s, A, B) & rdf(A, rdf_type, daml_TransitiveProperty)) & rdf(C, A, s))) -> rdf(C, A, B) ). all A B C ( rdf(A, rdf_type, daml_SymmetricProperty) & rdf(B, A, C) -> rdf(C, A, B) ). all A B C D E ( (((rdf(A, daml_hasAtMostOne, B) & rdf(C, log_notEqualTo, D)) & rdf(E, rdf_type, A)) & rdf(E, B, C)) & rdf(E, B, D) -> rdf(C, daml_equivalentTo, D) ). all A B ( (exists s (rdf(s, ontAx__item, A) & rdf(B, daml_rest, s))) -> rdf(B, ontAx__item, A) ). all A B ( rdf(A, daml_equivalentTo, B) -> rdf(A, daml_equivalentTo, B) ). all A B C ( (exists s (rdf(s, daml_sameIndividualAs, A) & rdf(B, C, s))) -> rdf(B, C, A) ). all A B C ( (exists s (rdf(s, daml_samePropertyAs, A) & rdf(B, s, C))) -> rdf(B, A, C) ). all A B C D ( (exists s (exists t (((((((rdf(t, daml_first, A) & rdf(t, daml_rest, s)) & rdf(s, daml_first, B)) & rdf(s, daml_rest, daml_nil)) & rdf(C, daml_intersectionOf, t)) & rdf(A, log_notEqualTo, B)) & rdf(D, rdf_type, A)) & rdf(D, rdf_type, B)))) -> rdf(D, rdf_type, C) ). all A B C D ( (exists s (exists t (exists u (exists s0 (((((((rdf(t, daml_oneOf, s) & rdf(s, daml_first, A)) & rdf(s, daml_rest, B)) & rdf(s0, daml_complementOf, u)) & rdf(u, daml_oneOf, B)) & rdf(C, daml_complementOf, t)) & rdf(D, rdf_type, s0)) & rdf(D, daml_differentIndividualFrom, A)))))) -> rdf(D, rdf_type, C) ). end_list. ================================================================ Then look at ,lx.engine.otter.fromOtter: ----- Otter 3.2, August 2001 ----- The process was started by sandro on wadimousa.hawke.org, Thu Jan 9 10:39:04 2003 The command was "otter". The process ID is 18453. 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). set(prolog_style_variables). clear(control_memory). formula_list(usable). rdf(s,rdf_nodeID,'<md5:d88c146dfafdea37a837778a92415bc2>'). rdf(s,ns5_stateCode,'<md5:a32356331cf2a7f56e45306fc6d328d9>'). rdf(s,ns5_population,'<md5:749b0f41b1f91012db8edab830aacdba>'). rdf(ns5_stateCode,rdf_type,ns6_InverseFunctionalProperty). rdf(s,rdf_nodeID,'<md5:27f237e6b7f96587b6202ff3607ad88a>'). rdf(s,ns5_stateCode,'<md5:a32356331cf2a7f56e45306fc6d328d9>'). rdf(s,ns5_stateBird,ns5_WesternMeadowlark). -(exists s (rdf(s,ns5_population,'<md5:749b0f41b1f91012db8edab830aacdba>')&rdf(s,ns5_stateBird,ns5_WesternMeadowlark)&rdf(s,rdf_nodeID,'<md5:d88c146dfafdea37a837778a92415bc2>'))). rdf('<file:/tmp/ontAx.n3>','<http://purl.org/dc/elements/1.1/description>','<md5:821f59c4d08564bb37d62c58b49f0d03>'). rdf('<file:/tmp/ontAx.n3>','<http://purl.org/dc/elements/1.1/description>','<md5:1f0efb73e107e9313dcc5f6dfbe9892a>'). rdf('<file:/tmp/ontAx.n3>','<http://purl.org/dc/elements/1.1/source>','<http://www.w3.org/TR/2002/WD-owl-features-20020729/>'). rdf('<file:/tmp/ontAx.n3>','<http://purl.org/dc/elements/1.1/source>','<http://www.agfa.com/w3c/euler/owl-rules>'). rdf('<file:/tmp/ontAx.n3>',rdfs_seeAlso,'<http://www.w3.org/2000/10/swap/util/rdfs-rules.n3>'). rdf(daml_Class,rdfs_label,'<md5:9bd81329febf6efe22788e03ddeaf0af>'). rdf(daml_Class,rdfs_subClassOf,rdfs_Class). rdf(daml_sameClassAs,rdf_type,daml_TransitiveProperty). rdf(daml_sameClassAs,rdf_type,daml_SymmetricProperty). all A B (rdf(A,daml_sameClassAs,B)<->rdf(B,rdfs_subClassOf,A)&rdf(A,rdfs_subClassOf,B)). rdf(daml_samePropertyAs,rdf_type,daml_TransitiveProperty). rdf(daml_samePropertyAs,rdf_type,daml_SymmetricProperty). all A B (rdf(A,daml_samePropertyAs,B)<->rdf(B,rdfs_subPropertyOf,A)&rdf(A,rdfs_subPropertyOf,B)). rdf(daml_sameIndividualAs,rdf_type,daml_TransitiveProperty). rdf(daml_sameIndividualAs,rdf_type,daml_SymmetricProperty). all A B C D (rdf(A,daml_sameIndividualAs,B)&rdf(A,C,D)->rdf(B,C,D)). all A B C D (rdf(A,daml_sameIndividualAs,B)&rdf(C,D,A)->rdf(C,D,B)). rdf(daml_differentIndividualFrom,rdf_type,daml_SymmetricProperty). rdf(daml_differentIndividualFrom,ontAx__converse,daml_sameIndividualAs). rdf(ontAx__converse,rdf_type,daml_SymmetricProperty). all A B C (-(exists s (rdf(s,ontAx__converse,A)&rdf(B,s,C)))->rdf(B,A,C)). all A B C ((exists s (rdf(s,ontAx__converse,A)&rdf(B,s,C)))-> -rdf(B,A,C)). rdf(daml_inverseOf,rdf_type,daml_SymmetricProperty). all A B C ((exists s (rdf(s,daml_inverseOf,A)&rdf(B,s,C)))->rdf(C,A,B)). all A B C D (rdf(A,rdf_type,daml_FunctionalProperty)-> (rdf(B,A,C)&rdf(B,A,D)->rdf(C,daml_equivalentTo,D))). all A B C D (rdf(A,rdf_type,daml_InverseFunctionalProperty)-> (rdf(B,A,C)&rdf(D,A,C)->rdf(B,daml_equivalentTo,D))). all A B C D ((exists s (rdf(s,daml_allValuesFrom,A)&rdf(s,daml_onProperty,B)&rdf(C,rdf_type,s)&rdf(C,B,D)))->rdf(D,rdf_type,A)). all A B C ((exists s (rdf(s,daml_onProperty,A)&rdf(s,daml_someValuesFrom,B)&rdf(C,rdf_type,s)))-> (exists t (rdf(t,rdf_type,B)&rdf(C,A,t)))). rdf('<file:/tmp/ontAx.n3>',ontAx_note,'<md5:298e17a6fc6db286af85fedc40e8d132>'). rdf('<file:/tmp/ontAx.n3>',ontAx_note,'<md5:bfbe1f1d0c2a32c63467e34db15b3e38>'). all A B ((exists s (rdf(s,daml_item,A)&rdf(B,daml_oneOf,s)))->rdf(A,rdf_type,B)). all A B C D (rdf(A,daml_oneOf,B)&rdf(C,daml_oneOf,D)&rdf(B,daml_rest,D)->rdf(C,rdfs_subClassOf,A)). rdf('<file:/tmp/ontAx.n3>',ontAx_note,'<md5:8425c7c4e78a0b61ca0177cba0fc28fd>'). rdf(daml_first,rdf_type,daml_FunctionalProperty). rdf(daml_rest,rdf_type,daml_FunctionalProperty). all A B (rdf(A,daml_first,B)->rdf(A,ontAx__item,B)). rdf('<file:/tmp/ontAx.n3>',ontAx_note,'<md5:6f05a3e924c4636761b0bddc7ee46f69>'). rdf('<file:/tmp/ontAx.n3>',ontAx_note,'<md5:bcc79261d87a60c1f21ef1b0b91d2692>'). all A B (rdf(A,daml_equivalentTo,B)->rdf(B,daml_equivalentTo,A)). all A B C D (rdf(A,log_notEqualTo,log_forAll)&rdf(A,log_notEqualTo,log_forSome)&rdf(B,daml_equivalentTo,C)&rdf(B,A,D)->rdf(C,A,D)). all A B C D (rdf(A,daml_equivalentTo,B)&rdf(A,log_notEqualTo,log_forAll)&rdf(A,log_notEqualTo,log_forSome)&rdf(C,A,D)->rdf(C,B,D)). all A B C D (rdf(A,log_notEqualTo,log_forAll)&rdf(A,log_notEqualTo,log_forSome)&rdf(B,A,C)&rdf(C,daml_equivalentTo,D)->rdf(B,A,D)). all A B (rdf(A,daml_sameIndividualAs,B)->rdf(B,daml_sameIndividualAs,A)). all A B C ((exists s (rdf(s,daml_sameIndividualAs,A)&rdf(s,B,C)))->rdf(A,B,C)). all A B (rdf(A,daml_samePropertyAs,B)->rdf(B,daml_samePropertyAs,A)). all A B C D (rdf(A,rdf_type,daml_UnambiguousProperty)-> (rdf(B,A,C)&rdf(D,A,C)->rdf(B,daml_equivalentTo,D))). all A (rdf(A,rdf_type,daml_Nothing)->rdf(A,rdf_type,ontAx_SymptomOfInconsistency)). all A B C D (rdf(A,daml_hasValue,B)&rdf(A,daml_onProperty,C)&rdf(D,C,B)->rdf(D,rdf_type,A)). all A B C ((exists s t u (rdf(u,daml_intersectionOf,t)&rdf(t,daml_first,A)&rdf(t,daml_rest,s)&rdf(s,daml_first,B)&rdf(s,daml_rest,daml_nil)&rdf(C,rdf_type,u)))->rdf(C,rdf_type,A)&rdf(C,rdf_type,B)). all A B (rdf(A,daml_differentIndividualFrom,B)->rdf(A,rdf_type,daml_Thing)). rdf(daml_Nothing,daml_oneOf,daml_nil). rdf(daml_Thing,daml_complementOf,daml_Nothing). all A B C ((exists s (rdf(s,A,B)&rdf(A,rdf_type,daml_TransitiveProperty)&rdf(C,A,s)))->rdf(C,A,B)). all A B C (rdf(A,rdf_type,daml_SymmetricProperty)&rdf(B,A,C)->rdf(C,A,B)). all A B C D E (rdf(A,daml_hasAtMostOne,B)&rdf(C,log_notEqualTo,D)&rdf(E,rdf_type,A)&rdf(E,B,C)&rdf(E,B,D)->rdf(C,daml_equivalentTo,D)). all A B ((exists s (rdf(s,ontAx__item,A)&rdf(B,daml_rest,s)))->rdf(B,ontAx__item,A)). all A B (rdf(A,daml_equivalentTo,B)->rdf(A,daml_equivalentTo,B)). all A B C ((exists s (rdf(s,daml_sameIndividualAs,A)&rdf(B,C,s)))->rdf(B,C,A)). all A B C ((exists s (rdf(s,daml_samePropertyAs,A)&rdf(B,s,C)))->rdf(B,A,C)). all A B C D ((exists s t (rdf(t,daml_first,A)&rdf(t,daml_rest,s)&rdf(s,daml_first,B)&rdf(s,daml_rest,daml_nil)&rdf(C,daml_intersectionOf,t)&rdf(A,log_notEqualTo,B)&rdf(D,rdf_type,A)&rdf(D,rdf_type,B)))->rdf(D,rdf_type,C)). all A B C D ((exists s t u s0 (rdf(t,daml_oneOf,s)&rdf(s,daml_first,A)&rdf(s,daml_rest,B)&rdf(s0,daml_complementOf,u)&rdf(u,daml_oneOf,B)&rdf(C,daml_complementOf,t)&rdf(D,rdf_type,s0)&rdf(D,daml_differentIndividualFrom,A)))->rdf(D,rdf_type,C)). end_list. end_of_list. -------> usable clausifies to: list(usable). 0 [] rdf(s,rdf_nodeID,'<md5:d88c146dfafdea37a837778a92415bc2>'). 0 [] rdf(s,ns5_stateCode,'<md5:a32356331cf2a7f56e45306fc6d328d9>'). 0 [] rdf(s,ns5_population,'<md5:749b0f41b1f91012db8edab830aacdba>'). 0 [] rdf(ns5_stateCode,rdf_type,ns6_InverseFunctionalProperty). 0 [] rdf(s,rdf_nodeID,'<md5:27f237e6b7f96587b6202ff3607ad88a>'). 0 [] rdf(s,ns5_stateCode,'<md5:a32356331cf2a7f56e45306fc6d328d9>'). 0 [] rdf(s,ns5_stateBird,ns5_WesternMeadowlark). 0 [] -rdf(X1,ns5_population,'<md5:749b0f41b1f91012db8edab830aacdba>')| -rdf(X1,ns5_stateBird,ns5_WesternMeadowlark)| -rdf(X1,rdf_nodeID,'<md5:d88c146dfafdea37a837778a92415bc2>'). 0 [] rdf('<file:/tmp/ontAx.n3>','<http://purl.org/dc/elements/1.1/description>','<md5:821f59c4d08564bb37d62c58b49f0d03>'). 0 [] rdf('<file:/tmp/ontAx.n3>','<http://purl.org/dc/elements/1.1/description>','<md5:1f0efb73e107e9313dcc5f6dfbe9892a>'). 0 [] rdf('<file:/tmp/ontAx.n3>','<http://purl.org/dc/elements/1.1/source>','<http://www.w3.org/TR/2002/WD-owl-features-20020729/>'). 0 [] rdf('<file:/tmp/ontAx.n3>','<http://purl.org/dc/elements/1.1/source>','<http://www.agfa.com/w3c/euler/owl-rules>'). 0 [] rdf('<file:/tmp/ontAx.n3>',rdfs_seeAlso,'<http://www.w3.org/2000/10/swap/util/rdfs-rules.n3>'). 0 [] rdf(daml_Class,rdfs_label,'<md5:9bd81329febf6efe22788e03ddeaf0af>'). 0 [] rdf(daml_Class,rdfs_subClassOf,rdfs_Class). 0 [] rdf(daml_sameClassAs,rdf_type,daml_TransitiveProperty). 0 [] rdf(daml_sameClassAs,rdf_type,daml_SymmetricProperty). 0 [] -rdf(A,daml_sameClassAs,B)|rdf(B,rdfs_subClassOf,A). 0 [] -rdf(A,daml_sameClassAs,B)|rdf(A,rdfs_subClassOf,B). 0 [] rdf(A,daml_sameClassAs,B)| -rdf(B,rdfs_subClassOf,A)| -rdf(A,rdfs_subClassOf,B). 0 [] rdf(daml_samePropertyAs,rdf_type,daml_TransitiveProperty). 0 [] rdf(daml_samePropertyAs,rdf_type,daml_SymmetricProperty). 0 [] -rdf(A,daml_samePropertyAs,B)|rdf(B,rdfs_subPropertyOf,A). 0 [] -rdf(A,daml_samePropertyAs,B)|rdf(A,rdfs_subPropertyOf,B). 0 [] rdf(A,daml_samePropertyAs,B)| -rdf(B,rdfs_subPropertyOf,A)| -rdf(A,rdfs_subPropertyOf,B). 0 [] rdf(daml_sameIndividualAs,rdf_type,daml_TransitiveProperty). 0 [] rdf(daml_sameIndividualAs,rdf_type,daml_SymmetricProperty). 0 [] -rdf(A,daml_sameIndividualAs,B)| -rdf(A,C,D)|rdf(B,C,D). 0 [] -rdf(A,daml_sameIndividualAs,B)| -rdf(C,D,A)|rdf(C,D,B). 0 [] rdf(daml_differentIndividualFrom,rdf_type,daml_SymmetricProperty). 0 [] rdf(daml_differentIndividualFrom,ontAx__converse,daml_sameIndividualAs). 0 [] rdf(ontAx__converse,rdf_type,daml_SymmetricProperty). 0 [] rdf($f1(A,B,C),ontAx__converse,A)|rdf(B,A,C). 0 [] rdf(B,$f1(A,B,C),C)|rdf(B,A,C). 0 [] -rdf(X2,ontAx__converse,A)| -rdf(B,X2,C)| -rdf(B,A,C). 0 [] rdf(daml_inverseOf,rdf_type,daml_SymmetricProperty). 0 [] -rdf(X3,daml_inverseOf,A)| -rdf(B,X3,C)|rdf(C,A,B). 0 [] -rdf(A,rdf_type,daml_FunctionalProperty)| -rdf(B,A,C)| -rdf(B,A,D)|rdf(C,daml_equivalentTo,D). 0 [] -rdf(A,rdf_type,daml_InverseFunctionalProperty)| -rdf(B,A,C)| -rdf(D,A,C)|rdf(B,daml_equivalentTo,D). 0 [] -rdf(X4,daml_allValuesFrom,A)| -rdf(X4,daml_onProperty,B)| -rdf(C,rdf_type,X4)| -rdf(C,B,D)|rdf(D,rdf_type,A). 0 [] -rdf(X5,daml_onProperty,A)| -rdf(X5,daml_someValuesFrom,B)| -rdf(C,rdf_type,X5)|rdf($f2(A,B,C),rdf_type,B). 0 [] -rdf(X5,daml_onProperty,A)| -rdf(X5,daml_someValuesFrom,B)| -rdf(C,rdf_type,X5)|rdf(C,A,$f2(A,B,C)). 0 [] rdf('<file:/tmp/ontAx.n3>',ontAx_note,'<md5:298e17a6fc6db286af85fedc40e8d132>'). 0 [] rdf('<file:/tmp/ontAx.n3>',ontAx_note,'<md5:bfbe1f1d0c2a32c63467e34db15b3e38>'). 0 [] -rdf(X6,daml_item,A)| -rdf(B,daml_oneOf,X6)|rdf(A,rdf_type,B). 0 [] -rdf(A,daml_oneOf,B)| -rdf(C,daml_oneOf,D)| -rdf(B,daml_rest,D)|rdf(C,rdfs_subClassOf,A). 0 [] rdf('<file:/tmp/ontAx.n3>',ontAx_note,'<md5:8425c7c4e78a0b61ca0177cba0fc28fd>'). 0 [] rdf(daml_first,rdf_type,daml_FunctionalProperty). 0 [] rdf(daml_rest,rdf_type,daml_FunctionalProperty). 0 [] -rdf(A,daml_first,B)|rdf(A,ontAx__item,B). 0 [] rdf('<file:/tmp/ontAx.n3>',ontAx_note,'<md5:6f05a3e924c4636761b0bddc7ee46f69>'). 0 [] rdf('<file:/tmp/ontAx.n3>',ontAx_note,'<md5:bcc79261d87a60c1f21ef1b0b91d2692>'). 0 [] -rdf(A,daml_equivalentTo,B)|rdf(B,daml_equivalentTo,A). 0 [] -rdf(A,log_notEqualTo,log_forAll)| -rdf(A,log_notEqualTo,log_forSome)| -rdf(B,daml_equivalentTo,C)| -rdf(B,A,D)|rdf(C,A,D). 0 [] -rdf(A,daml_equivalentTo,B)| -rdf(A,log_notEqualTo,log_forAll)| -rdf(A,log_notEqualTo,log_forSome)| -rdf(C,A,D)|rdf(C,B,D). 0 [] -rdf(A,log_notEqualTo,log_forAll)| -rdf(A,log_notEqualTo,log_forSome)| -rdf(B,A,C)| -rdf(C,daml_equivalentTo,D)|rdf(B,A,D). 0 [] -rdf(A,daml_sameIndividualAs,B)|rdf(B,daml_sameIndividualAs,A). 0 [] -rdf(X7,daml_sameIndividualAs,A)| -rdf(X7,B,C)|rdf(A,B,C). 0 [] -rdf(A,daml_samePropertyAs,B)|rdf(B,daml_samePropertyAs,A). 0 [] -rdf(A,rdf_type,daml_UnambiguousProperty)| -rdf(B,A,C)| -rdf(D,A,C)|rdf(B,daml_equivalentTo,D). 0 [] -rdf(A,rdf_type,daml_Nothing)|rdf(A,rdf_type,ontAx_SymptomOfInconsistency). 0 [] -rdf(A,daml_hasValue,B)| -rdf(A,daml_onProperty,C)| -rdf(D,C,B)|rdf(D,rdf_type,A). 0 [] -rdf(X8,daml_intersectionOf,X9)| -rdf(X9,daml_first,A)| -rdf(X9,daml_rest,X10)| -rdf(X10,daml_first,B)| -rdf(X10,daml_rest,daml_nil)| -rdf(C,rdf_type,X8)|rdf(C,rdf_type,A). 0 [] -rdf(X8,daml_intersectionOf,X9)| -rdf(X9,daml_first,A)| -rdf(X9,daml_rest,X10)| -rdf(X10,daml_first,B)| -rdf(X10,daml_rest,daml_nil)| -rdf(C,rdf_type,X8)|rdf(C,rdf_type,B). 0 [] -rdf(A,daml_differentIndividualFrom,B)|rdf(A,rdf_type,daml_Thing). 0 [] rdf(daml_Nothing,daml_oneOf,daml_nil). 0 [] rdf(daml_Thing,daml_complementOf,daml_Nothing). 0 [] -rdf(X11,A,B)| -rdf(A,rdf_type,daml_TransitiveProperty)| -rdf(C,A,X11)|rdf(C,A,B). 0 [] -rdf(A,rdf_type,daml_SymmetricProperty)| -rdf(B,A,C)|rdf(C,A,B). 0 [] -rdf(A,daml_hasAtMostOne,B)| -rdf(C,log_notEqualTo,D)| -rdf(E,rdf_type,A)| -rdf(E,B,C)| -rdf(E,B,D)|rdf(C,daml_equivalentTo,D). 0 [] -rdf(X12,ontAx__item,A)| -rdf(B,daml_rest,X12)|rdf(B,ontAx__item,A). 0 [] -rdf(X13,daml_sameIndividualAs,A)| -rdf(B,C,X13)|rdf(B,C,A). 0 [] -rdf(X14,daml_samePropertyAs,A)| -rdf(B,X14,C)|rdf(B,A,C). 0 [] -rdf(X15,daml_first,A)| -rdf(X15,daml_rest,X16)| -rdf(X16,daml_first,B)| -rdf(X16,daml_rest,daml_nil)| -rdf(C,daml_intersectionOf,X15)| -rdf(A,log_notEqualTo,B)| -rdf(D,rdf_type,A)| -rdf(D,rdf_type,B)|rdf(D,rdf_type,C). 0 [] -rdf(X17,daml_oneOf,X18)| -rdf(X18,daml_first,A)| -rdf(X18,daml_rest,B)| -rdf(X19,daml_complementOf,X20)| -rdf(X20,daml_oneOf,B)| -rdf(C,daml_complementOf,X17)| -rdf(D,rdf_type,X19)| -rdf(D,daml_differentIndividualFrom,A)|rdf(D,rdf_type,C). 0 [] end_list. end_of_list. SCAN INPUT: prop=0, horn=0, equality=0, symmetry=0, max_lits=9. This is a non-Horn set without equality. The strategy will be ordered hyper_res, unit deletion, and factoring, with satellites in sos and with nuclei in usable. dependent: set(hyper_res). dependent: set(factor). dependent: set(unit_deletion). ------------> process usable: ** KEPT (pick-wt=12): 1 [] -rdf(A,ns5_population,'<md5:749b0f41b1f91012db8edab830aacdba>')| -rdf(A,ns5_stateBird,ns5_WesternMeadowlark)| -rdf(A,rdf_nodeID,'<md5:d88c146dfafdea37a837778a92415bc2>'). ** KEPT (pick-wt=8): 2 [] -rdf(A,daml_sameClassAs,B)|rdf(B,rdfs_subClassOf,A). ** KEPT (pick-wt=8): 3 [] -rdf(A,daml_sameClassAs,B)|rdf(A,rdfs_subClassOf,B). ** KEPT (pick-wt=12): 4 [] rdf(A,daml_sameClassAs,B)| -rdf(B,rdfs_subClassOf,A)| -rdf(A,rdfs_subClassOf,B). ** KEPT (pick-wt=8): 5 [] -rdf(A,daml_samePropertyAs,B)|rdf(B,rdfs_subPropertyOf,A). ** KEPT (pick-wt=8): 6 [] -rdf(A,daml_samePropertyAs,B)|rdf(A,rdfs_subPropertyOf,B). ** KEPT (pick-wt=12): 7 [] rdf(A,daml_samePropertyAs,B)| -rdf(B,rdfs_subPropertyOf,A)| -rdf(A,rdfs_subPropertyOf,B). ** KEPT (pick-wt=12): 8 [] -rdf(A,daml_sameIndividualAs,B)| -rdf(A,C,D)|rdf(B,C,D). ** KEPT (pick-wt=12): 9 [] -rdf(A,daml_sameIndividualAs,B)| -rdf(C,D,A)|rdf(C,D,B). ** KEPT (pick-wt=12): 10 [] -rdf(A,ontAx__converse,B)| -rdf(C,A,D)| -rdf(C,B,D). ** KEPT (pick-wt=12): 11 [] -rdf(A,daml_inverseOf,B)| -rdf(C,A,D)|rdf(D,B,C). ** KEPT (pick-wt=16): 12 [] -rdf(A,rdf_type,daml_FunctionalProperty)| -rdf(B,A,C)| -rdf(B,A,D)|rdf(C,daml_equivalentTo,D). ** KEPT (pick-wt=16): 13 [] -rdf(A,rdf_type,daml_InverseFunctionalProperty)| -rdf(B,A,C)| -rdf(D,A,C)|rdf(B,daml_equivalentTo,D). ** KEPT (pick-wt=20): 14 [] -rdf(A,daml_allValuesFrom,B)| -rdf(A,daml_onProperty,C)| -rdf(D,rdf_type,A)| -rdf(D,C,E)|rdf(E,rdf_type,B). ** KEPT (pick-wt=19): 15 [] -rdf(A,daml_onProperty,B)| -rdf(A,daml_someValuesFrom,C)| -rdf(D,rdf_type,A)|rdf($f2(B,C,D),rdf_type,C). ** KEPT (pick-wt=19): 16 [] -rdf(A,daml_onProperty,B)| -rdf(A,daml_someValuesFrom,C)| -rdf(D,rdf_type,A)|rdf(D,B,$f2(B,C,D)). ** KEPT (pick-wt=12): 17 [] -rdf(A,daml_item,B)| -rdf(C,daml_oneOf,A)|rdf(B,rdf_type,C). ** KEPT (pick-wt=16): 18 [] -rdf(A,daml_oneOf,B)| -rdf(C,daml_oneOf,D)| -rdf(B,daml_rest,D)|rdf(C,rdfs_subClassOf,A). ** KEPT (pick-wt=8): 19 [] -rdf(A,daml_first,B)|rdf(A,ontAx__item,B). ** KEPT (pick-wt=8): 20 [] -rdf(A,daml_equivalentTo,B)|rdf(B,daml_equivalentTo,A). ** KEPT (pick-wt=20): 21 [] -rdf(A,log_notEqualTo,log_forAll)| -rdf(A,log_notEqualTo,log_forSome)| -rdf(B,daml_equivalentTo,C)| -rdf(B,A,D)|rdf(C,A,D). ** KEPT (pick-wt=20): 22 [] -rdf(A,daml_equivalentTo,B)| -rdf(A,log_notEqualTo,log_forAll)| -rdf(A,log_notEqualTo,log_forSome)| -rdf(C,A,D)|rdf(C,B,D). ** KEPT (pick-wt=20): 23 [] -rdf(A,log_notEqualTo,log_forAll)| -rdf(A,log_notEqualTo,log_forSome)| -rdf(B,A,C)| -rdf(C,daml_equivalentTo,D)|rdf(B,A,D). ** KEPT (pick-wt=8): 24 [] -rdf(A,daml_sameIndividualAs,B)|rdf(B,daml_sameIndividualAs,A). Following clause subsumed by 8 during input processing: 0 [] -rdf(A,daml_sameIndividualAs,B)| -rdf(A,C,D)|rdf(B,C,D). ** KEPT (pick-wt=8): 25 [] -rdf(A,daml_samePropertyAs,B)|rdf(B,daml_samePropertyAs,A). ** KEPT (pick-wt=16): 26 [] -rdf(A,rdf_type,daml_UnambiguousProperty)| -rdf(B,A,C)| -rdf(D,A,C)|rdf(B,daml_equivalentTo,D). ** KEPT (pick-wt=8): 27 [] -rdf(A,rdf_type,daml_Nothing)|rdf(A,rdf_type,ontAx_SymptomOfInconsistency). ** KEPT (pick-wt=16): 28 [] -rdf(A,daml_hasValue,B)| -rdf(A,daml_onProperty,C)| -rdf(D,C,B)|rdf(D,rdf_type,A). ** KEPT (pick-wt=28): 29 [] -rdf(A,daml_intersectionOf,B)| -rdf(B,daml_first,C)| -rdf(B,daml_rest,D)| -rdf(D,daml_first,E)| -rdf(D,daml_rest,daml_nil)| -rdf(F,rdf_type,A)|rdf(F,rdf_type,C). ** KEPT (pick-wt=28): 30 [] -rdf(A,daml_intersectionOf,B)| -rdf(B,daml_first,C)| -rdf(B,daml_rest,D)| -rdf(D,daml_first,E)| -rdf(D,daml_rest,daml_nil)| -rdf(F,rdf_type,A)|rdf(F,rdf_type,E). ** KEPT (pick-wt=8): 31 [] -rdf(A,daml_differentIndividualFrom,B)|rdf(A,rdf_type,daml_Thing). ** KEPT (pick-wt=16): 32 [] -rdf(A,B,C)| -rdf(B,rdf_type,daml_TransitiveProperty)| -rdf(D,B,A)|rdf(D,B,C). ** KEPT (pick-wt=12): 33 [] -rdf(A,rdf_type,daml_SymmetricProperty)| -rdf(B,A,C)|rdf(C,A,B). ** KEPT (pick-wt=24): 34 [] -rdf(A,daml_hasAtMostOne,B)| -rdf(C,log_notEqualTo,D)| -rdf(E,rdf_type,A)| -rdf(E,B,C)| -rdf(E,B,D)|rdf(C,daml_equivalentTo,D). ** KEPT (pick-wt=12): 35 [] -rdf(A,ontAx__item,B)| -rdf(C,daml_rest,A)|rdf(C,ontAx__item,B). Following clause subsumed by 9 during input processing: 0 [] -rdf(A,daml_sameIndividualAs,B)| -rdf(C,D,A)|rdf(C,D,B). ** KEPT (pick-wt=12): 36 [] -rdf(A,daml_samePropertyAs,B)| -rdf(C,A,D)|rdf(C,B,D). ** KEPT (pick-wt=36): 37 [] -rdf(A,daml_first,B)| -rdf(A,daml_rest,C)| -rdf(C,daml_first,D)| -rdf(C,daml_rest,daml_nil)| -rdf(E,daml_intersectionOf,A)| -rdf(B,log_notEqualTo,D)| -rdf(F,rdf_type,B)| -rdf(F,rdf_type,D)|rdf(F,rdf_type,E). ** KEPT (pick-wt=36): 38 [] -rdf(A,daml_oneOf,B)| -rdf(B,daml_first,C)| -rdf(B,daml_rest,D)| -rdf(E,daml_complementOf,F)| -rdf(F,daml_oneOf,D)| -rdf(G,daml_complementOf,A)| -rdf(H,rdf_type,E)| -rdf(H,daml_differentIndividualFrom,C)|rdf(H,rdf_type,G). ------------> process sos: ** KEPT (pick-wt=4): 93 [] rdf(s,rdf_nodeID,'<md5:d88c146dfafdea37a837778a92415bc2>'). ** KEPT (pick-wt=4): 94 [] rdf(s,ns5_stateCode,'<md5:a32356331cf2a7f56e45306fc6d328d9>'). ** KEPT (pick-wt=4): 95 [] rdf(s,ns5_population,'<md5:749b0f41b1f91012db8edab830aacdba>'). ** KEPT (pick-wt=4): 96 [] rdf(ns5_stateCode,rdf_type,ns6_InverseFunctionalProperty). ** KEPT (pick-wt=4): 97 [] rdf(s,rdf_nodeID,'<md5:27f237e6b7f96587b6202ff3607ad88a>'). Following clause subsumed by 94 during input processing: 0 [] rdf(s,ns5_stateCode,'<md5:a32356331cf2a7f56e45306fc6d328d9>'). ** KEPT (pick-wt=4): 98 [] rdf(s,ns5_stateBird,ns5_WesternMeadowlark). ** KEPT (pick-wt=4): 99 [] rdf('<file:/tmp/ontAx.n3>','<http://purl.org/dc/elements/1.1/description>','<md5:821f59c4d08564bb37d62c58b49f0d03>'). ** KEPT (pick-wt=4): 100 [] rdf('<file:/tmp/ontAx.n3>','<http://purl.org/dc/elements/1.1/description>','<md5:1f0efb73e107e9313dcc5f6dfbe9892a>'). ** KEPT (pick-wt=4): 101 [] rdf('<file:/tmp/ontAx.n3>','<http://purl.org/dc/elements/1.1/source>','<http://www.w3.org/TR/2002/WD-owl-features-20020729/>'). ** KEPT (pick-wt=4): 102 [] rdf('<file:/tmp/ontAx.n3>','<http://purl.org/dc/elements/1.1/source>','<http://www.agfa.com/w3c/euler/owl-rules>'). ** KEPT (pick-wt=4): 103 [] rdf('<file:/tmp/ontAx.n3>',rdfs_seeAlso,'<http://www.w3.org/2000/10/swap/util/rdfs-rules.n3>'). ** KEPT (pick-wt=4): 104 [] rdf(daml_Class,rdfs_label,'<md5:9bd81329febf6efe22788e03ddeaf0af>'). ** KEPT (pick-wt=4): 105 [] rdf(daml_Class,rdfs_subClassOf,rdfs_Class). ** KEPT (pick-wt=4): 106 [] rdf(daml_sameClassAs,rdf_type,daml_TransitiveProperty). ** KEPT (pick-wt=4): 107 [] rdf(daml_sameClassAs,rdf_type,daml_SymmetricProperty). ** KEPT (pick-wt=4): 108 [] rdf(daml_samePropertyAs,rdf_type,daml_TransitiveProperty). ** KEPT (pick-wt=4): 109 [] rdf(daml_samePropertyAs,rdf_type,daml_SymmetricProperty). ** KEPT (pick-wt=4): 110 [] rdf(daml_sameIndividualAs,rdf_type,daml_TransitiveProperty). ** KEPT (pick-wt=4): 111 [] rdf(daml_sameIndividualAs,rdf_type,daml_SymmetricProperty). ** KEPT (pick-wt=4): 112 [] rdf(daml_differentIndividualFrom,rdf_type,daml_SymmetricProperty). ** KEPT (pick-wt=4): 113 [] rdf(daml_differentIndividualFrom,ontAx__converse,daml_sameIndividualAs). ** KEPT (pick-wt=4): 114 [] rdf(ontAx__converse,rdf_type,daml_SymmetricProperty). ** KEPT (pick-wt=11): 115 [] rdf($f1(A,B,C),ontAx__converse,A)|rdf(B,A,C). ** KEPT (pick-wt=11): 116 [] rdf(A,$f1(B,A,C),C)|rdf(A,B,C). ** KEPT (pick-wt=4): 117 [] rdf(daml_inverseOf,rdf_type,daml_SymmetricProperty). ** KEPT (pick-wt=4): 118 [] rdf('<file:/tmp/ontAx.n3>',ontAx_note,'<md5:298e17a6fc6db286af85fedc40e8d132>'). ** KEPT (pick-wt=4): 119 [] rdf('<file:/tmp/ontAx.n3>',ontAx_note,'<md5:bfbe1f1d0c2a32c63467e34db15b3e38>'). ** KEPT (pick-wt=4): 120 [] rdf('<file:/tmp/ontAx.n3>',ontAx_note,'<md5:8425c7c4e78a0b61ca0177cba0fc28fd>'). ** KEPT (pick-wt=4): 121 [] rdf(daml_first,rdf_type,daml_FunctionalProperty). ** KEPT (pick-wt=4): 122 [] rdf(daml_rest,rdf_type,daml_FunctionalProperty). ** KEPT (pick-wt=4): 123 [] rdf('<file:/tmp/ontAx.n3>',ontAx_note,'<md5:6f05a3e924c4636761b0bddc7ee46f69>'). ** KEPT (pick-wt=4): 124 [] rdf('<file:/tmp/ontAx.n3>',ontAx_note,'<md5:bcc79261d87a60c1f21ef1b0b91d2692>'). ** KEPT (pick-wt=4): 125 [] rdf(daml_Nothing,daml_oneOf,daml_nil). ** KEPT (pick-wt=4): 126 [] rdf(daml_Thing,daml_complementOf,daml_Nothing). ** KEPT (pick-wt=1): 127 [] end_list. ======= end of input processing ======= =========== start of search =========== given clause #1: (wt=4) 93 [] rdf(s,rdf_nodeID,'<md5:d88c146dfafdea37a837778a92415bc2>'). given clause #2: (wt=1) 127 [] end_list. given clause #3: (wt=4) 94 [] rdf(s,ns5_stateCode,'<md5:a32356331cf2a7f56e45306fc6d328d9>'). given clause #4: (wt=4) 95 [] rdf(s,ns5_population,'<md5:749b0f41b1f91012db8edab830aacdba>'). given clause #5: (wt=4) 96 [] rdf(ns5_stateCode,rdf_type,ns6_InverseFunctionalProperty). given clause #6: (wt=4) 97 [] rdf(s,rdf_nodeID,'<md5:27f237e6b7f96587b6202ff3607ad88a>'). given clause #7: (wt=4) 98 [] rdf(s,ns5_stateBird,ns5_WesternMeadowlark). -------- PROOF -------- -----> EMPTY CLAUSE at 0.05 sec ----> 128 [hyper,98,1,95,93] $F. Length of proof is 0. Level of proof is 0. ---------------- PROOF ---------------- 1 [] -rdf(A,ns5_population,'<md5:749b0f41b1f91012db8edab830aacdba>')| -rdf(A,ns5_stateBird,ns5_WesternMeadowlark)| -rdf(A,rdf_nodeID,'<md5:d88c146dfafdea37a837778a92415bc2>'). 93 [] rdf(s,rdf_nodeID,'<md5:d88c146dfafdea37a837778a92415bc2>'). 95 [] rdf(s,ns5_population,'<md5:749b0f41b1f91012db8edab830aacdba>'). 98 [] rdf(s,ns5_stateBird,ns5_WesternMeadowlark). 128 [hyper,98,1,95,93] $F. ------------ end of proof ------------- Search stopped by max_proofs option. Search stopped by max_proofs option. ============ end of search ============ -------------- statistics ------------- clauses given 7 clauses generated 81 clauses kept 127 clauses forward subsumed 24 clauses back subsumed 0 Kbytes malloced 223 ----------- times (seconds) ----------- user CPU time 0.05 (0 hr, 0 min, 0 sec) system CPU time 0.00 (0 hr, 0 min, 0 sec) wall-clock time 0 (0 hr, 0 min, 0 sec) hyper_res time 0.01 for_sub time 0.01 back_sub time 0.00 conflict time 0.00 demod time 0.00 That finishes the proof of the theorem. Process 18453 finished Thu Jan 9 10:39:04 2003
Received on Thursday, 9 January 2003 10:50:16 UTC