----- Otter 3.2, August 2001 ----- The process was started by sandro on roke.hawke.org, Wed Sep 3 15:24:40 2003 The command was "otter". The process ID is 29581. 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-equivProp.otter'). ------- start included file otter/owlAx-equivProp.otter------- formula_list(usable). all PRED1 PRED2 (rdf(PRED1,owl_equivalentProperty,PRED2)<-> (all SUBJ OBJ (rdf(SUBJ,PRED1,OBJ)<->rdf(SUBJ,PRED2,OBJ)))). all PRED1 PRED2 (rdf(PRED1,rdfs_subPropertyOf,PRED2)<-> (all SUBJ OBJ (rdf(SUBJ,PRED1,OBJ)->rdf(SUBJ,PRED2,OBJ)))). end_of_list. -------> usable clausifies to: list(usable). 0 [] -rdf(x1,owl_equivalentProperty,x2)| -rdf(x3,x1,x4)|rdf(x3,x2,x4). 0 [] -rdf(x1,owl_equivalentProperty,x2)|rdf(x3,x1,x4)| -rdf(x3,x2,x4). 0 [] rdf(x1,owl_equivalentProperty,x2)|rdf($f2(x1,x2),x1,$f1(x1,x2))|rdf($f2(x1,x2),x2,$f1(x1,x2)). 0 [] rdf(x1,owl_equivalentProperty,x2)| -rdf($f2(x1,x2),x1,$f1(x1,x2))| -rdf($f2(x1,x2),x2,$f1(x1,x2)). 0 [] -rdf(x5,rdfs_subPropertyOf,x6)| -rdf(x7,x5,x8)|rdf(x7,x6,x8). 0 [] rdf(x5,rdfs_subPropertyOf,x6)|rdf($f4(x5,x6),x5,$f3(x5,x6)). 0 [] rdf(x5,rdfs_subPropertyOf,x6)| -rdf($f4(x5,x6),x6,$f3(x5,x6)). end_of_list. ------- end included file otter/owlAx-equivProp.otter------- formula_list(usable). rdf(ns40_hasHead,rdf_type,owl_ObjectProperty). rdf(ns40_hasLeader,rdf_type,owl_ObjectProperty). rdf(ns40_hasHead,owl_equivalentProperty,ns40_hasLeader). -(rdf(ns40_hasHead,rdf_type,owl_ObjectProperty)&rdf(ns40_hasHead,rdfs_subPropertyOf,ns40_hasLeader)&rdf(ns40_hasLeader,rdf_type,owl_ObjectProperty)&rdf(ns40_hasLeader,rdfs_subPropertyOf,ns40_hasHead)). end_of_list. -------> usable clausifies to: list(usable). 0 [] rdf(ns40_hasHead,rdf_type,owl_ObjectProperty). 0 [] rdf(ns40_hasLeader,rdf_type,owl_ObjectProperty). 0 [] rdf(ns40_hasHead,owl_equivalentProperty,ns40_hasLeader). 0 [] -rdf(ns40_hasHead,rdf_type,owl_ObjectProperty)| -rdf(ns40_hasHead,rdfs_subPropertyOf,ns40_hasLeader)| -rdf(ns40_hasLeader,rdf_type,owl_ObjectProperty)| -rdf(ns40_hasLeader,rdfs_subPropertyOf,ns40_hasHead). end_of_list. SCAN INPUT: prop=0, horn=0, equality=0, symmetry=0, max_lits=4. 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(x,owl_equivalentProperty,y)| -rdf(z,x,u)|rdf(z,y,u). ** KEPT (pick-wt=12): 2 [] -rdf(x,owl_equivalentProperty,y)|rdf(z,x,u)| -rdf(z,y,u). ** KEPT (pick-wt=20): 3 [] rdf(x,owl_equivalentProperty,y)| -rdf($f2(x,y),x,$f1(x,y))| -rdf($f2(x,y),y,$f1(x,y)). ** KEPT (pick-wt=12): 4 [] -rdf(x,rdfs_subPropertyOf,y)| -rdf(z,x,u)|rdf(z,y,u). ** KEPT (pick-wt=12): 5 [] rdf(x,rdfs_subPropertyOf,y)| -rdf($f4(x,y),y,$f3(x,y)). ** KEPT (pick-wt=16): 6 [] -rdf(ns40_hasHead,rdf_type,owl_ObjectProperty)| -rdf(ns40_hasHead,rdfs_subPropertyOf,ns40_hasLeader)| -rdf(ns40_hasLeader,rdf_type,owl_ObjectProperty)| -rdf(ns40_hasLeader,rdfs_subPropertyOf,ns40_hasHead). ------------> process sos: ** KEPT (pick-wt=20): 11 [] rdf(x,owl_equivalentProperty,y)|rdf($f2(x,y),x,$f1(x,y))|rdf($f2(x,y),y,$f1(x,y)). ** KEPT (pick-wt=12): 12 [] rdf(x,rdfs_subPropertyOf,y)|rdf($f4(x,y),x,$f3(x,y)). ** KEPT (pick-wt=4): 13 [] rdf(ns40_hasHead,rdf_type,owl_ObjectProperty). ** KEPT (pick-wt=4): 14 [] rdf(ns40_hasLeader,rdf_type,owl_ObjectProperty). ** KEPT (pick-wt=4): 15 [] rdf(ns40_hasHead,owl_equivalentProperty,ns40_hasLeader). ======= end of input processing ======= =========== start of search =========== given clause #1: (wt=20) 11 [] rdf(x,owl_equivalentProperty,y)|rdf($f2(x,y),x,$f1(x,y))|rdf($f2(x,y),y,$f1(x,y)). given clause #2: (wt=4) 13 [] rdf(ns40_hasHead,rdf_type,owl_ObjectProperty). given clause #3: (wt=4) 14 [] rdf(ns40_hasLeader,rdf_type,owl_ObjectProperty). given clause #4: (wt=4) 15 [] rdf(ns40_hasHead,owl_equivalentProperty,ns40_hasLeader). given clause #5: (wt=12) 12 [] rdf(x,rdfs_subPropertyOf,y)|rdf($f4(x,y),x,$f3(x,y)). given clause #6: (wt=12) 16 [factor,11.2.3] rdf(x,owl_equivalentProperty,x)|rdf($f2(x,x),x,$f1(x,x)). given clause #7: (wt=4) 81 [hyper,12,5,factor_simp] rdf(x,rdfs_subPropertyOf,x). given clause #8: (wt=4) 110 [hyper,16,9,factor_simp] rdf(x,owl_equivalentProperty,x). given clause #9: (wt=12) 63 [factor,59.1.3] rdf($f2(ns40_hasLeader,ns40_hasHead),ns40_hasHead,$f1(ns40_hasLeader,ns40_hasHead))|rdf(ns40_hasLeader,owl_equivalentProperty,ns40_hasHead). given clause #10: (wt=12) 64 [factor,61.1.3] rdf($f2(ns40_hasLeader,ns40_hasHead),ns40_hasLeader,$f1(ns40_hasLeader,ns40_hasHead))|rdf(ns40_hasLeader,owl_equivalentProperty,ns40_hasHead). given clause #11: (wt=20) 18 [hyper,11,8] rdf($f2(x,owl_equivalentProperty),x,$f1(x,owl_equivalentProperty))|rdf($f2(x,owl_equivalentProperty),owl_equivalentProperty,$f1(x,owl_equivalentProperty))|rdf(x,x,owl_equivalentProperty). given clause #12: (wt=4) 124 [hyper,64,3,63,factor_simp,factor_simp] rdf(ns40_hasLeader,owl_equivalentProperty,ns40_hasHead). given clause #13: (wt=12) 65 [hyper,12,10] rdf($f4(rdfs_subPropertyOf,x),rdfs_subPropertyOf,$f3(rdfs_subPropertyOf,x))|rdf(rdfs_subPropertyOf,x,x). given clause #14: (wt=12) 70 [hyper,12,4,15] rdf($f4(owl_equivalentProperty,x),owl_equivalentProperty,$f3(owl_equivalentProperty,x))|rdf(ns40_hasHead,x,ns40_hasLeader). given clause #15: (wt=12) 71 [hyper,12,4,14] rdf($f4(rdf_type,x),rdf_type,$f3(rdf_type,x))|rdf(ns40_hasLeader,x,owl_ObjectProperty). given clause #16: (wt=20) 19 [hyper,11,7] rdf($f2(owl_equivalentProperty,x),owl_equivalentProperty,$f1(owl_equivalentProperty,x))|rdf($f2(owl_equivalentProperty,x),x,$f1(owl_equivalentProperty,x))|rdf(owl_equivalentProperty,x,x). given clause #17: (wt=12) 72 [hyper,12,4,13] rdf($f4(rdf_type,x),rdf_type,$f3(rdf_type,x))|rdf(ns40_hasHead,x,owl_ObjectProperty). given clause #18: (wt=12) 87 [hyper,12,2,15] rdf(ns40_hasLeader,rdfs_subPropertyOf,x)|rdf($f4(ns40_hasLeader,x),ns40_hasHead,$f3(ns40_hasLeader,x)). given clause #19: (wt=4) 507 [hyper,87,5,factor_simp] rdf(ns40_hasLeader,rdfs_subPropertyOf,ns40_hasHead). given clause #20: (wt=8) 517 [hyper,507,6,13,70,14] rdf($f4(owl_equivalentProperty,rdfs_subPropertyOf),owl_equivalentProperty,$f3(owl_equivalentProperty,rdfs_subPropertyOf)). given clause #21: (wt=40) 20 [hyper,11,5] rdf($f2($f4(x,owl_equivalentProperty),$f3(x,owl_equivalentProperty)),$f4(x,owl_equivalentProperty),$f1($f4(x,owl_equivalentProperty),$f3(x,owl_equivalentProperty)))|rdf($f2($f4(x,owl_equivalentProperty),$f3(x,owl_equivalentProperty)),$f3(x,owl_equivalentProperty),$f1($f4(x,owl_equivalentProperty),$f3(x,owl_equivalentProperty)))|rdf(x,rdfs_subPropertyOf,owl_equivalentProperty). given clause #22: (wt=8) 518 [hyper,507,6,13,12,14] rdf($f4(ns40_hasHead,ns40_hasLeader),ns40_hasHead,$f3(ns40_hasHead,ns40_hasLeader)). given clause #23: (wt=8) 592 [hyper,518,2,124] rdf($f4(ns40_hasHead,ns40_hasLeader),ns40_hasLeader,$f3(ns40_hasHead,ns40_hasLeader)). given clause #24: (wt=4) 596 [hyper,592,5] rdf(ns40_hasHead,rdfs_subPropertyOf,ns40_hasLeader). -------- PROOF -------- -----> EMPTY CLAUSE at 0.10 sec ----> 603 [hyper,596,6,13,14,507] $F. Length of proof is 10. Level of proof is 5. ---------------- PROOF ---------------- 1 [] -rdf(x,owl_equivalentProperty,y)| -rdf(z,x,u)|rdf(z,y,u). 2 [] -rdf(x,owl_equivalentProperty,y)|rdf(z,x,u)| -rdf(z,y,u). 3 [] rdf(x,owl_equivalentProperty,y)| -rdf($f2(x,y),x,$f1(x,y))| -rdf($f2(x,y),y,$f1(x,y)). 5 [] rdf(x,rdfs_subPropertyOf,y)| -rdf($f4(x,y),y,$f3(x,y)). 6 [] -rdf(ns40_hasHead,rdf_type,owl_ObjectProperty)| -rdf(ns40_hasHead,rdfs_subPropertyOf,ns40_hasLeader)| -rdf(ns40_hasLeader,rdf_type,owl_ObjectProperty)| -rdf(ns40_hasLeader,rdfs_subPropertyOf,ns40_hasHead). 11 [] rdf(x,owl_equivalentProperty,y)|rdf($f2(x,y),x,$f1(x,y))|rdf($f2(x,y),y,$f1(x,y)). 12 [] rdf(x,rdfs_subPropertyOf,y)|rdf($f4(x,y),x,$f3(x,y)). 13 [] rdf(ns40_hasHead,rdf_type,owl_ObjectProperty). 14 [] rdf(ns40_hasLeader,rdf_type,owl_ObjectProperty). 15 [] rdf(ns40_hasHead,owl_equivalentProperty,ns40_hasLeader). 59 [hyper,15,2,11] rdf($f2(ns40_hasLeader,x),ns40_hasHead,$f1(ns40_hasLeader,x))|rdf(ns40_hasLeader,owl_equivalentProperty,x)|rdf($f2(ns40_hasLeader,x),x,$f1(ns40_hasLeader,x)). 61 [hyper,15,1,11] rdf($f2(x,ns40_hasHead),ns40_hasLeader,$f1(x,ns40_hasHead))|rdf(x,owl_equivalentProperty,ns40_hasHead)|rdf($f2(x,ns40_hasHead),x,$f1(x,ns40_hasHead)). 63 [factor,59.1.3] rdf($f2(ns40_hasLeader,ns40_hasHead),ns40_hasHead,$f1(ns40_hasLeader,ns40_hasHead))|rdf(ns40_hasLeader,owl_equivalentProperty,ns40_hasHead). 64 [factor,61.1.3] rdf($f2(ns40_hasLeader,ns40_hasHead),ns40_hasLeader,$f1(ns40_hasLeader,ns40_hasHead))|rdf(ns40_hasLeader,owl_equivalentProperty,ns40_hasHead). 87 [hyper,12,2,15] rdf(ns40_hasLeader,rdfs_subPropertyOf,x)|rdf($f4(ns40_hasLeader,x),ns40_hasHead,$f3(ns40_hasLeader,x)). 124 [hyper,64,3,63,factor_simp,factor_simp] rdf(ns40_hasLeader,owl_equivalentProperty,ns40_hasHead). 507 [hyper,87,5,factor_simp] rdf(ns40_hasLeader,rdfs_subPropertyOf,ns40_hasHead). 518 [hyper,507,6,13,12,14] rdf($f4(ns40_hasHead,ns40_hasLeader),ns40_hasHead,$f3(ns40_hasHead,ns40_hasLeader)). 592 [hyper,518,2,124] rdf($f4(ns40_hasHead,ns40_hasLeader),ns40_hasLeader,$f3(ns40_hasHead,ns40_hasLeader)). 596 [hyper,592,5] rdf(ns40_hasHead,rdfs_subPropertyOf,ns40_hasLeader). 603 [hyper,596,6,13,14,507] $F. ------------ end of proof ------------- Search stopped by max_proofs option. Search stopped by max_proofs option. ============ end of search ============ -------------- statistics ------------- clauses given 24 clauses generated 1527 clauses kept 602 clauses forward subsumed 935 clauses back subsumed 50 Kbytes malloced 574 ----------- times (seconds) ----------- user CPU time 0.10 (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.02 for_sub time 0.02 back_sub time 0.02 conflict time 0.00 demod time 0.00 That finishes the proof of the theorem. Process 29581 finished Wed Sep 3 15:24:40 2003