----- Otter 3.2, August 2001 ----- The process was started by sandro on roke.hawke.org, Thu Sep 4 02:28:22 2003 The command was "otter". The process ID is 2050. 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-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(x1,owl_onProperty,x2)| -rdf(x1,owl_cardinality,x3)| -rdf(x4,rdfs_subClassOf,x1)|rdf($f2(x2,x4,x3),owl_onProperty,x2). 0 [] -rdf(x1,owl_onProperty,x2)| -rdf(x1,owl_cardinality,x3)| -rdf(x4,rdfs_subClassOf,x1)|rdf($f2(x2,x4,x3),owl_maxCardinality,x3). 0 [] -rdf(x1,owl_onProperty,x2)| -rdf(x1,owl_cardinality,x3)| -rdf(x4,rdfs_subClassOf,x1)|rdf($f1(x2,x4,x3),owl_onProperty,x2). 0 [] -rdf(x1,owl_onProperty,x2)| -rdf(x1,owl_cardinality,x3)| -rdf(x4,rdfs_subClassOf,x1)|rdf($f1(x2,x4,x3),owl_minCardinality,x3). 0 [] -rdf(x1,owl_onProperty,x2)| -rdf(x1,owl_cardinality,x3)| -rdf(x4,rdfs_subClassOf,x1)|rdf(x4,rdfs_subClassOf,$f2(x2,x4,x3)). 0 [] -rdf(x1,owl_onProperty,x2)| -rdf(x1,owl_cardinality,x3)| -rdf(x4,rdfs_subClassOf,x1)|rdf(x4,rdfs_subClassOf,$f1(x2,x4,x3)). 0 [] rdf($f3(x2,x4,x3),owl_onProperty,x2)| -rdf(x5,owl_onProperty,x2)| -rdf(x5,owl_maxCardinality,x3)| -rdf(x6,owl_onProperty,x2)| -rdf(x6,owl_minCardinality,x3)| -rdf(x4,rdfs_subClassOf,x5)| -rdf(x4,rdfs_subClassOf,x6). 0 [] rdf($f3(x2,x4,x3),owl_cardinality,x3)| -rdf(x5,owl_onProperty,x2)| -rdf(x5,owl_maxCardinality,x3)| -rdf(x6,owl_onProperty,x2)| -rdf(x6,owl_minCardinality,x3)| -rdf(x4,rdfs_subClassOf,x5)| -rdf(x4,rdfs_subClassOf,x6). 0 [] rdf(x4,rdfs_subClassOf,$f3(x2,x4,x3))| -rdf(x5,owl_onProperty,x2)| -rdf(x5,owl_maxCardinality,x3)| -rdf(x6,owl_onProperty,x2)| -rdf(x6,owl_minCardinality,x3)| -rdf(x4,rdfs_subClassOf,x5)| -rdf(x4,rdfs_subClassOf,x6). 0 [] -rdf(x7,owl_onProperty,x8)|rdf(x7,rdf_type,owl_Restriction). end_of_list. ------- end included file otter/owlAx-cardeq.otter------- formula_list(usable). exists s t (rdf(ns24_c,rdf_type,owl_Class)&rdf(t,rdf_type,owl_Restriction)&rdf(t,owl_onProperty,ns24_p)&rdf(t,owl_maxCardinality,lit1)&rdf('foo:zero','foo:succ',lit1)&rdf(ns24_c,rdfs_subClassOf,t)&rdf(s,rdf_type,owl_Restriction)&rdf(s,owl_onProperty,ns24_p)&rdf(s,owl_minCardinality,lit1)&rdf(ns24_c,rdfs_subClassOf,s)&rdf(ns24_p,rdf_type,owl_ObjectProperty)& -(exists u (rdf(ns24_c,rdf_type,owl_Class)&rdf(u,rdf_type,owl_Restriction)&rdf(u,owl_onProperty,ns24_p)&rdf(u,owl_cardinality,lit1)&rdf('foo:zero','foo:succ',lit1)&rdf(ns24_c,rdfs_subClassOf,u)&rdf(ns24_p,rdf_type,owl_ObjectProperty)))). end_of_list. -------> usable clausifies to: list(usable). 0 [] rdf(ns24_c,rdf_type,owl_Class). 0 [] rdf($c1,rdf_type,owl_Restriction). 0 [] rdf($c1,owl_onProperty,ns24_p). 0 [] rdf($c1,owl_maxCardinality,lit1). 0 [] rdf('foo:zero','foo:succ',lit1). 0 [] rdf(ns24_c,rdfs_subClassOf,$c1). 0 [] rdf($c2,rdf_type,owl_Restriction). 0 [] rdf($c2,owl_onProperty,ns24_p). 0 [] rdf($c2,owl_minCardinality,lit1). 0 [] rdf(ns24_c,rdfs_subClassOf,$c2). 0 [] rdf(ns24_p,rdf_type,owl_ObjectProperty). 0 [] -rdf(ns24_c,rdf_type,owl_Class)| -rdf(u,rdf_type,owl_Restriction)| -rdf(u,owl_onProperty,ns24_p)| -rdf(u,owl_cardinality,lit1)| -rdf('foo:zero','foo:succ',lit1)| -rdf(ns24_c,rdfs_subClassOf,u)| -rdf(ns24_p,rdf_type,owl_ObjectProperty). end_of_list. SCAN INPUT: prop=0, horn=1, equality=0, symmetry=0, max_lits=7. This is a Horn set without equality. The strategy will be hyperresolution, with satellites in sos and nuclei in usable. dependent: set(hyper_res). dependent: clear(order_hyper). ------------> process usable: ** KEPT (pick-wt=19): 1 [] -rdf(x,owl_onProperty,y)| -rdf(x,owl_cardinality,z)| -rdf(u,rdfs_subClassOf,x)|rdf($f2(y,u,z),owl_onProperty,y). ** KEPT (pick-wt=19): 2 [] -rdf(x,owl_onProperty,y)| -rdf(x,owl_cardinality,z)| -rdf(u,rdfs_subClassOf,x)|rdf($f2(y,u,z),owl_maxCardinality,z). ** KEPT (pick-wt=19): 3 [] -rdf(x,owl_onProperty,y)| -rdf(x,owl_cardinality,z)| -rdf(u,rdfs_subClassOf,x)|rdf($f1(y,u,z),owl_onProperty,y). ** KEPT (pick-wt=19): 4 [] -rdf(x,owl_onProperty,y)| -rdf(x,owl_cardinality,z)| -rdf(u,rdfs_subClassOf,x)|rdf($f1(y,u,z),owl_minCardinality,z). ** KEPT (pick-wt=19): 5 [] -rdf(x,owl_onProperty,y)| -rdf(x,owl_cardinality,z)| -rdf(u,rdfs_subClassOf,x)|rdf(u,rdfs_subClassOf,$f2(y,u,z)). ** KEPT (pick-wt=19): 6 [] -rdf(x,owl_onProperty,y)| -rdf(x,owl_cardinality,z)| -rdf(u,rdfs_subClassOf,x)|rdf(u,rdfs_subClassOf,$f1(y,u,z)). ** KEPT (pick-wt=31): 7 [] rdf($f3(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): 8 [] rdf($f3(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): 9 [] rdf(x,rdfs_subClassOf,$f3(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): 10 [] -rdf(x,owl_onProperty,y)|rdf(x,rdf_type,owl_Restriction). ** KEPT (pick-wt=28): 11 [] -rdf(ns24_c,rdf_type,owl_Class)| -rdf(x,rdf_type,owl_Restriction)| -rdf(x,owl_onProperty,ns24_p)| -rdf(x,owl_cardinality,lit1)| -rdf('foo:zero','foo:succ',lit1)| -rdf(ns24_c,rdfs_subClassOf,x)| -rdf(ns24_p,rdf_type,owl_ObjectProperty). ------------> process sos: ** KEPT (pick-wt=4): 12 [] rdf(ns24_c,rdf_type,owl_Class). ** KEPT (pick-wt=4): 13 [] rdf($c1,rdf_type,owl_Restriction). ** KEPT (pick-wt=4): 14 [] rdf($c1,owl_onProperty,ns24_p). ** KEPT (pick-wt=4): 15 [] rdf($c1,owl_maxCardinality,lit1). ** KEPT (pick-wt=4): 16 [] rdf('foo:zero','foo:succ',lit1). ** KEPT (pick-wt=4): 17 [] rdf(ns24_c,rdfs_subClassOf,$c1). ** KEPT (pick-wt=4): 18 [] rdf($c2,rdf_type,owl_Restriction). ** KEPT (pick-wt=4): 19 [] rdf($c2,owl_onProperty,ns24_p). ** KEPT (pick-wt=4): 20 [] rdf($c2,owl_minCardinality,lit1). ** KEPT (pick-wt=4): 21 [] rdf(ns24_c,rdfs_subClassOf,$c2). ** KEPT (pick-wt=4): 22 [] rdf(ns24_p,rdf_type,owl_ObjectProperty). ======= end of input processing ======= =========== start of search =========== given clause #1: (wt=4) 12 [] rdf(ns24_c,rdf_type,owl_Class). given clause #2: (wt=4) 13 [] rdf($c1,rdf_type,owl_Restriction). given clause #3: (wt=4) 14 [] rdf($c1,owl_onProperty,ns24_p). given clause #4: (wt=4) 15 [] rdf($c1,owl_maxCardinality,lit1). given clause #5: (wt=4) 16 [] rdf('foo:zero','foo:succ',lit1). given clause #6: (wt=4) 17 [] rdf(ns24_c,rdfs_subClassOf,$c1). given clause #7: (wt=4) 18 [] rdf($c2,rdf_type,owl_Restriction). given clause #8: (wt=4) 19 [] rdf($c2,owl_onProperty,ns24_p). given clause #9: (wt=4) 20 [] rdf($c2,owl_minCardinality,lit1). given clause #10: (wt=4) 21 [] rdf(ns24_c,rdfs_subClassOf,$c2). given clause #11: (wt=4) 22 [] rdf(ns24_p,rdf_type,owl_ObjectProperty). given clause #12: (wt=7) 23 [hyper,21,9,14,15,19,20,17] rdf(ns24_c,rdfs_subClassOf,$f3(ns24_p,ns24_c,lit1)). given clause #13: (wt=7) 24 [hyper,21,8,14,15,19,20,17] rdf($f3(ns24_p,ns24_c,lit1),owl_cardinality,lit1). given clause #14: (wt=7) 25 [hyper,21,7,14,15,19,20,17] rdf($f3(ns24_p,ns24_c,lit1),owl_onProperty,ns24_p). given clause #15: (wt=7) 26 [hyper,25,10] rdf($f3(ns24_p,ns24_c,lit1),rdf_type,owl_Restriction). -------- PROOF -------- -----> EMPTY CLAUSE at 0.01 sec ----> 33 [hyper,26,11,12,25,24,16,23,22] $F. Length of proof is 4. Level of proof is 2. ---------------- PROOF ---------------- 7 [] rdf($f3(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). 8 [] rdf($f3(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). 9 [] rdf(x,rdfs_subClassOf,$f3(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). 10 [] -rdf(x,owl_onProperty,y)|rdf(x,rdf_type,owl_Restriction). 11 [] -rdf(ns24_c,rdf_type,owl_Class)| -rdf(x,rdf_type,owl_Restriction)| -rdf(x,owl_onProperty,ns24_p)| -rdf(x,owl_cardinality,lit1)| -rdf('foo:zero','foo:succ',lit1)| -rdf(ns24_c,rdfs_subClassOf,x)| -rdf(ns24_p,rdf_type,owl_ObjectProperty). 12 [] rdf(ns24_c,rdf_type,owl_Class). 14 [] rdf($c1,owl_onProperty,ns24_p). 15 [] rdf($c1,owl_maxCardinality,lit1). 16 [] rdf('foo:zero','foo:succ',lit1). 17 [] rdf(ns24_c,rdfs_subClassOf,$c1). 19 [] rdf($c2,owl_onProperty,ns24_p). 20 [] rdf($c2,owl_minCardinality,lit1). 21 [] rdf(ns24_c,rdfs_subClassOf,$c2). 22 [] rdf(ns24_p,rdf_type,owl_ObjectProperty). 23 [hyper,21,9,14,15,19,20,17] rdf(ns24_c,rdfs_subClassOf,$f3(ns24_p,ns24_c,lit1)). 24 [hyper,21,8,14,15,19,20,17] rdf($f3(ns24_p,ns24_c,lit1),owl_cardinality,lit1). 25 [hyper,21,7,14,15,19,20,17] rdf($f3(ns24_p,ns24_c,lit1),owl_onProperty,ns24_p). 26 [hyper,25,10] rdf($f3(ns24_p,ns24_c,lit1),rdf_type,owl_Restriction). 33 [hyper,26,11,12,25,24,16,23,22] $F. ------------ end of proof ------------- Search stopped by max_proofs option. Search stopped by max_proofs option. ============ end of search ============ -------------- statistics ------------- clauses given 15 clauses generated 13 clauses kept 32 clauses forward subsumed 2 clauses back subsumed 0 Kbytes malloced 127 ----------- times (seconds) ----------- user CPU time 0.01 (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.00 for_sub time 0.00 back_sub time 0.00 conflict time 0.00 demod time 0.00 That finishes the proof of the theorem. Process 2050 finished Thu Sep 4 02:28:22 2003