----- Otter 3.2, August 2001 ----- The process was started by sandro on roke.hawke.org, Thu Sep 4 02:28:41 2003 The command was "otter". The process ID is 2086. 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). exists s t (rdf(ns42_p,rdf_type,owl_ObjectProperty)&rdf(ns42_p,rdfs_domain,ns42_d)&rdf(ns42_q,rdf_type,owl_ObjectProperty)&rdf(ns42_q,rdfs_domain,ns42_d)&rdf(ns42_q,rdf_type,owl_FunctionalProperty)&rdf(ns42_p,rdf_type,owl_FunctionalProperty)&rdf(ns42_v,rdf_type,owl_Thing)&rdf(ns42_d,rdf_type,owl_Class)&rdf(t,rdf_type,owl_Restriction)&rdf(t,owl_onProperty,ns42_p)&rdf(t,owl_hasValue,ns42_v)&rdf(ns42_d,owl_equivalentClass,t)&rdf(s,rdf_type,owl_Restriction)&rdf(s,owl_onProperty,ns42_q)&rdf(s,owl_hasValue,ns42_v)&rdf(ns42_d,owl_equivalentClass,s)& -(rdf(ns42_p,rdf_type,owl_ObjectProperty)&rdf(ns42_q,rdf_type,owl_ObjectProperty)&rdf(ns42_p,owl_equivalentProperty,ns42_q))). end_of_list. -------> usable clausifies to: list(usable). 0 [] rdf(ns42_p,rdf_type,owl_ObjectProperty). 0 [] rdf(ns42_p,rdfs_domain,ns42_d). 0 [] rdf(ns42_q,rdf_type,owl_ObjectProperty). 0 [] rdf(ns42_q,rdfs_domain,ns42_d). 0 [] rdf(ns42_q,rdf_type,owl_FunctionalProperty). 0 [] rdf(ns42_p,rdf_type,owl_FunctionalProperty). 0 [] rdf(ns42_v,rdf_type,owl_Thing). 0 [] rdf(ns42_d,rdf_type,owl_Class). 0 [] rdf($c1,rdf_type,owl_Restriction). 0 [] rdf($c1,owl_onProperty,ns42_p). 0 [] rdf($c1,owl_hasValue,ns42_v). 0 [] rdf(ns42_d,owl_equivalentClass,$c1). 0 [] rdf($c2,rdf_type,owl_Restriction). 0 [] rdf($c2,owl_onProperty,ns42_q). 0 [] rdf($c2,owl_hasValue,ns42_v). 0 [] rdf(ns42_d,owl_equivalentClass,$c2). 0 [] -rdf(ns42_p,rdf_type,owl_ObjectProperty)| -rdf(ns42_q,rdf_type,owl_ObjectProperty)| -rdf(ns42_p,owl_equivalentProperty,ns42_q). end_of_list. SCAN INPUT: prop=0, horn=0, equality=0, symmetry=0, max_lits=3. 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=12): 6 [] -rdf(ns42_p,rdf_type,owl_ObjectProperty)| -rdf(ns42_q,rdf_type,owl_ObjectProperty)| -rdf(ns42_p,owl_equivalentProperty,ns42_q). ------------> 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(ns42_p,rdf_type,owl_ObjectProperty). ** KEPT (pick-wt=4): 14 [] rdf(ns42_p,rdfs_domain,ns42_d). ** KEPT (pick-wt=4): 15 [] rdf(ns42_q,rdf_type,owl_ObjectProperty). ** KEPT (pick-wt=4): 16 [] rdf(ns42_q,rdfs_domain,ns42_d). ** KEPT (pick-wt=4): 17 [] rdf(ns42_q,rdf_type,owl_FunctionalProperty). ** KEPT (pick-wt=4): 18 [] rdf(ns42_p,rdf_type,owl_FunctionalProperty). ** KEPT (pick-wt=4): 19 [] rdf(ns42_v,rdf_type,owl_Thing). ** KEPT (pick-wt=4): 20 [] rdf(ns42_d,rdf_type,owl_Class). ** KEPT (pick-wt=4): 21 [] rdf($c1,rdf_type,owl_Restriction). ** KEPT (pick-wt=4): 22 [] rdf($c1,owl_onProperty,ns42_p). ** KEPT (pick-wt=4): 23 [] rdf($c1,owl_hasValue,ns42_v). ** KEPT (pick-wt=4): 24 [] rdf(ns42_d,owl_equivalentClass,$c1). ** KEPT (pick-wt=4): 25 [] rdf($c2,rdf_type,owl_Restriction). ** KEPT (pick-wt=4): 26 [] rdf($c2,owl_onProperty,ns42_q). ** KEPT (pick-wt=4): 27 [] rdf($c2,owl_hasValue,ns42_v). ** KEPT (pick-wt=4): 28 [] rdf(ns42_d,owl_equivalentClass,$c2). ======= 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(ns42_p,rdf_type,owl_ObjectProperty). given clause #3: (wt=4) 14 [] rdf(ns42_p,rdfs_domain,ns42_d). given clause #4: (wt=4) 15 [] rdf(ns42_q,rdf_type,owl_ObjectProperty). given clause #5: (wt=4) 16 [] rdf(ns42_q,rdfs_domain,ns42_d). given clause #6: (wt=12) 12 [] rdf(x,rdfs_subPropertyOf,y)|rdf($f4(x,y),x,$f3(x,y)). given clause #7: (wt=4) 17 [] rdf(ns42_q,rdf_type,owl_FunctionalProperty). given clause #8: (wt=4) 18 [] rdf(ns42_p,rdf_type,owl_FunctionalProperty). given clause #9: (wt=4) 19 [] rdf(ns42_v,rdf_type,owl_Thing). given clause #10: (wt=4) 20 [] rdf(ns42_d,rdf_type,owl_Class). given clause #11: (wt=4) 21 [] rdf($c1,rdf_type,owl_Restriction). given clause #12: (wt=4) 22 [] rdf($c1,owl_onProperty,ns42_p). given clause #13: (wt=4) 23 [] rdf($c1,owl_hasValue,ns42_v). given clause #14: (wt=4) 24 [] rdf(ns42_d,owl_equivalentClass,$c1). given clause #15: (wt=4) 25 [] rdf($c2,rdf_type,owl_Restriction). given clause #16: (wt=4) 26 [] rdf($c2,owl_onProperty,ns42_q). given clause #17: (wt=4) 27 [] rdf($c2,owl_hasValue,ns42_v). given clause #18: (wt=4) 28 [] rdf(ns42_d,owl_equivalentClass,$c2). given clause #19: (wt=4) 91 [hyper,12,5,factor_simp] rdf(x,rdfs_subPropertyOf,x). given clause #20: (wt=12) 29 [factor,11.2.3] rdf(x,owl_equivalentProperty,x)|rdf($f2(x,x),x,$f1(x,x)). given clause #21: (wt=20) 31 [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 #22: (wt=4) 157 [hyper,29,9,factor_simp] rdf(x,owl_equivalentProperty,x). given clause #23: (wt=12) 75 [hyper,12,10] rdf($f4(rdfs_subPropertyOf,x),rdfs_subPropertyOf,$f3(rdfs_subPropertyOf,x))|rdf(rdfs_subPropertyOf,x,x). given clause #24: (wt=12) 79 [hyper,12,4,16] rdf($f4(rdfs_domain,x),rdfs_domain,$f3(rdfs_domain,x))|rdf(ns42_q,x,ns42_d). given clause #25: (wt=12) 80 [hyper,12,4,15] rdf($f4(rdf_type,x),rdf_type,$f3(rdf_type,x))|rdf(ns42_q,x,owl_ObjectProperty). given clause #26: (wt=20) 32 [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 #27: (wt=12) 81 [hyper,12,4,14] rdf($f4(rdfs_domain,x),rdfs_domain,$f3(rdfs_domain,x))|rdf(ns42_p,x,ns42_d). given clause #28: (wt=12) 82 [hyper,12,4,13] rdf($f4(rdf_type,x),rdf_type,$f3(rdf_type,x))|rdf(ns42_p,x,owl_ObjectProperty). given clause #29: (wt=12) 118 [hyper,17,4,12] rdf(ns42_q,x,owl_FunctionalProperty)|rdf($f4(rdf_type,x),rdf_type,$f3(rdf_type,x)). given clause #30: (wt=12) 121 [hyper,18,4,12] rdf(ns42_p,x,owl_FunctionalProperty)|rdf($f4(rdf_type,x),rdf_type,$f3(rdf_type,x)). given clause #31: (wt=40) 33 [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 #32: (wt=12) 124 [hyper,19,4,12] rdf(ns42_v,x,owl_Thing)|rdf($f4(rdf_type,x),rdf_type,$f3(rdf_type,x)). given clause #33: (wt=12) 127 [hyper,20,4,12] rdf(ns42_d,x,owl_Class)|rdf($f4(rdf_type,x),rdf_type,$f3(rdf_type,x)). given clause #34: (wt=12) 130 [hyper,21,4,12] rdf($c1,x,owl_Restriction)|rdf($f4(rdf_type,x),rdf_type,$f3(rdf_type,x)). given clause #35: (wt=12) 133 [hyper,22,4,12] rdf($c1,x,ns42_p)|rdf($f4(owl_onProperty,x),owl_onProperty,$f3(owl_onProperty,x)). given clause #36: (wt=36) 34 [hyper,11,2,11] rdf($f2(x,y),x,$f1(x,y))|rdf($f2(x,y),y,$f1(x,y))|rdf(x,z,y)|rdf($f2(z,owl_equivalentProperty),z,$f1(z,owl_equivalentProperty))|rdf($f2(z,owl_equivalentProperty),owl_equivalentProperty,$f1(z,owl_equivalentProperty)).