- 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