----- Otter 3.2, August 2001 ----- The process was started by sandro on roke.hawke.org, Wed Sep 3 15:24:41 2003 The command was "otter". The process ID is 29583. 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(ns41_hasHead,rdf_type,owl_ObjectProperty). rdf(ns41_hasHead,rdfs_subPropertyOf,ns41_hasLeader). rdf(ns41_hasLeader,rdf_type,owl_ObjectProperty). rdf(ns41_hasLeader,rdfs_subPropertyOf,ns41_hasHead). -(rdf(ns41_hasHead,rdf_type,owl_ObjectProperty)&rdf(ns41_hasLeader,rdf_type,owl_ObjectProperty)&rdf(ns41_hasHead,owl_equivalentProperty,ns41_hasLeader)). end_of_list. -------> usable clausifies to: list(usable). 0 [] rdf(ns41_hasHead,rdf_type,owl_ObjectProperty). 0 [] rdf(ns41_hasHead,rdfs_subPropertyOf,ns41_hasLeader). 0 [] rdf(ns41_hasLeader,rdf_type,owl_ObjectProperty). 0 [] rdf(ns41_hasLeader,rdfs_subPropertyOf,ns41_hasHead). 0 [] -rdf(ns41_hasHead,rdf_type,owl_ObjectProperty)| -rdf(ns41_hasLeader,rdf_type,owl_ObjectProperty)| -rdf(ns41_hasHead,owl_equivalentProperty,ns41_hasLeader). 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(ns41_hasHead,rdf_type,owl_ObjectProperty)| -rdf(ns41_hasLeader,rdf_type,owl_ObjectProperty)| -rdf(ns41_hasHead,owl_equivalentProperty,ns41_hasLeader). ------------> 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(ns41_hasHead,rdf_type,owl_ObjectProperty). ** KEPT (pick-wt=4): 14 [] rdf(ns41_hasHead,rdfs_subPropertyOf,ns41_hasLeader). ** KEPT (pick-wt=4): 15 [] rdf(ns41_hasLeader,rdf_type,owl_ObjectProperty). ** KEPT (pick-wt=4): 16 [] rdf(ns41_hasLeader,rdfs_subPropertyOf,ns41_hasHead). ======= 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(ns41_hasHead,rdf_type,owl_ObjectProperty). given clause #3: (wt=4) 14 [] rdf(ns41_hasHead,rdfs_subPropertyOf,ns41_hasLeader). given clause #4: (wt=4) 15 [] rdf(ns41_hasLeader,rdf_type,owl_ObjectProperty). given clause #5: (wt=4) 16 [] rdf(ns41_hasLeader,rdfs_subPropertyOf,ns41_hasHead). given clause #6: (wt=12) 12 [] rdf(x,rdfs_subPropertyOf,y)|rdf($f4(x,y),x,$f3(x,y)). given clause #7: (wt=4) 87 [hyper,12,5,factor_simp] rdf(x,rdfs_subPropertyOf,x). given clause #8: (wt=12) 17 [factor,11.2.3] rdf(x,owl_equivalentProperty,x)|rdf($f2(x,x),x,$f1(x,x)). given clause #9: (wt=4) 119 [hyper,17,9,factor_simp] rdf(x,owl_equivalentProperty,x). given clause #10: (wt=12) 60 [factor,56.1.3] rdf($f2(ns41_hasLeader,ns41_hasHead),ns41_hasLeader,$f1(ns41_hasLeader,ns41_hasHead))|rdf(ns41_hasLeader,owl_equivalentProperty,ns41_hasHead). given clause #11: (wt=20) 19 [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=12) 61 [factor,57.1.3] rdf($f2(ns41_hasHead,ns41_hasLeader),ns41_hasLeader,$f1(ns41_hasHead,ns41_hasLeader))|rdf(ns41_hasHead,owl_equivalentProperty,ns41_hasLeader). given clause #13: (wt=8) 187 [hyper,61,6,13,15] rdf($f2(ns41_hasHead,ns41_hasLeader),ns41_hasLeader,$f1(ns41_hasHead,ns41_hasLeader)). given clause #14: (wt=8) 188 [hyper,187,4,16] rdf($f2(ns41_hasHead,ns41_hasLeader),ns41_hasHead,$f1(ns41_hasHead,ns41_hasLeader)). given clause #15: (wt=4) 193 [hyper,188,3,187] rdf(ns41_hasHead,owl_equivalentProperty,ns41_hasLeader). -------- PROOF -------- -----> EMPTY CLAUSE at 0.04 sec ----> 196 [hyper,193,6,13,15] $F. Length of proof is 5. Level of proof is 5. ---------------- PROOF ---------------- 3 [] rdf(x,owl_equivalentProperty,y)| -rdf($f2(x,y),x,$f1(x,y))| -rdf($f2(x,y),y,$f1(x,y)). 4 [] -rdf(x,rdfs_subPropertyOf,y)| -rdf(z,x,u)|rdf(z,y,u). 6 [] -rdf(ns41_hasHead,rdf_type,owl_ObjectProperty)| -rdf(ns41_hasLeader,rdf_type,owl_ObjectProperty)| -rdf(ns41_hasHead,owl_equivalentProperty,ns41_hasLeader). 11 [] rdf(x,owl_equivalentProperty,y)|rdf($f2(x,y),x,$f1(x,y))|rdf($f2(x,y),y,$f1(x,y)). 13 [] rdf(ns41_hasHead,rdf_type,owl_ObjectProperty). 14 [] rdf(ns41_hasHead,rdfs_subPropertyOf,ns41_hasLeader). 15 [] rdf(ns41_hasLeader,rdf_type,owl_ObjectProperty). 16 [] rdf(ns41_hasLeader,rdfs_subPropertyOf,ns41_hasHead). 57 [hyper,14,4,11] rdf($f2(ns41_hasHead,x),ns41_hasLeader,$f1(ns41_hasHead,x))|rdf(ns41_hasHead,owl_equivalentProperty,x)|rdf($f2(ns41_hasHead,x),x,$f1(ns41_hasHead,x)). 61 [factor,57.1.3] rdf($f2(ns41_hasHead,ns41_hasLeader),ns41_hasLeader,$f1(ns41_hasHead,ns41_hasLeader))|rdf(ns41_hasHead,owl_equivalentProperty,ns41_hasLeader). 187 [hyper,61,6,13,15] rdf($f2(ns41_hasHead,ns41_hasLeader),ns41_hasLeader,$f1(ns41_hasHead,ns41_hasLeader)). 188 [hyper,187,4,16] rdf($f2(ns41_hasHead,ns41_hasLeader),ns41_hasHead,$f1(ns41_hasHead,ns41_hasLeader)). 193 [hyper,188,3,187] rdf(ns41_hasHead,owl_equivalentProperty,ns41_hasLeader). 196 [hyper,193,6,13,15] $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 640 clauses kept 195 clauses forward subsumed 456 clauses back subsumed 13 Kbytes malloced 255 ----------- times (seconds) ----------- user CPU time 0.04 (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 29583 finished Wed Sep 3 15:24:41 2003