----- Otter 3.2, August 2001 ----- The process was started by sandro on roke.hawke.org, Fri Nov 7 10:22:17 2003 The command was "otter". The process ID is 11931. 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(control_memory). clear(sigint_interact). include('otter/RDFS.otter'). ------- start included file otter/RDFS.otter------- formula_list(usable). all xxx aaa lll (rdf(xxx,aaa,lll)&'foo:plainLit'(lll)-> (exists nnn (rdf(xxx,aaa,nnn)&rdf(nnn,rdf_type,rdfs_Literal)))). all aaa xxx yyy zzz (rdf(aaa,rdfs_domain,zzz)&rdf(xxx,aaa,yyy)->rdf(xxx,rdf_type,zzz)). all aaa xxx uuu zzz (rdf(aaa,rdfs_range,zzz)&rdf(xxx,aaa,uuu)->rdf(uuu,rdf_type,zzz)). all aaa xxx yyy (rdf(xxx,aaa,yyy)->rdf(xxx,rdf_type,rdfs_Resource)). all aaa xxx uuu (rdf(xxx,aaa,uuu)->rdf(uuu,rdf_type,rdfs_Resource)). all aaa bbb ccc uuu xxx yyy zzz (rdf(aaa,rdfs_subPropertyOf,bbb)&rdf(bbb,rdfs_subPropertyOf,ccc)->rdf(aaa,rdfs_subPropertyOf,ccc)). all aaa bbb ccc uuu xxx yyy zzz (rdf(xxx,rdf_type,rdf_Property)->rdf(xxx,rdfs_subPropertyOf,xxx)). all aaa bbb ccc uuu xxx yyy zzz (rdf(aaa,rdfs_subPropertyOf,bbb)&rdf(xxx,aaa,yyy)->rdf(xxx,bbb,yyy)). all aaa bbb ccc uuu xxx yyy zzz (rdf(xxx,rdf_type,rdfs_Class)->rdf(xxx,rdfs_subClassOf,rdfs_Resource)). all aaa bbb ccc uuu xxx yyy zzz (rdf(xxx,rdfs_subClassOf,yyy)&rdf(aaa,rdf_type,xxx)->rdf(aaa,rdf_type,yyy)). all aaa bbb ccc uuu xxx yyy zzz (rdf(xxx,rdf_type,rdfs_Class)->rdf(xxx,rdfs_subClassOf,xxx)). all aaa bbb ccc uuu xxx yyy zzz (rdf(xxx,rdfs_subClassOf,yyy)&rdf(yyy,rdfs_subClassOf,zzz)->rdf(xxx,rdfs_subClassOf,zzz)). all aaa bbb ccc uuu xxx yyy zzz (rdf(xxx,rdf_type,rdfs_ContainerMembershipProperty)->rdf(xxx,rdfs_subPropertyOf,rdfs_member)). all aaa bbb ccc uuu xxx yyy zzz (rdf(xxx,rdf_type,rdfs_Datatype)->rdf(xxx,rdfs_subClassOf,rdfs_Literal)). end_of_list. -------> usable clausifies to: list(usable). 0 [] -rdf(xxx,x1,x2)| -'foo:plainLit'(x2)|rdf(xxx,x1,$f1(xxx,x1,x2)). 0 [] -rdf(xxx,x1,x2)| -'foo:plainLit'(x2)|rdf($f1(xxx,x1,x2),rdf_type,rdfs_Literal). 0 [] -rdf(x3,rdfs_domain,zzz)| -rdf(xxx,x3,yyy)|rdf(xxx,rdf_type,zzz). 0 [] -rdf(x4,rdfs_range,zzz)| -rdf(xxx,x4,uuu)|rdf(uuu,rdf_type,zzz). 0 [] -rdf(xxx,x5,yyy)|rdf(xxx,rdf_type,rdfs_Resource). 0 [] -rdf(xxx,x6,uuu)|rdf(uuu,rdf_type,rdfs_Resource). 0 [] -rdf(x7,rdfs_subPropertyOf,x8)| -rdf(x8,rdfs_subPropertyOf,x9)|rdf(x7,rdfs_subPropertyOf,x9). 0 [] -rdf(xxx,rdf_type,rdf_Property)|rdf(xxx,rdfs_subPropertyOf,xxx). 0 [] -rdf(x10,rdfs_subPropertyOf,x11)| -rdf(xxx,x10,yyy)|rdf(xxx,x11,yyy). 0 [] -rdf(xxx,rdf_type,rdfs_Class)|rdf(xxx,rdfs_subClassOf,rdfs_Resource). 0 [] -rdf(xxx,rdfs_subClassOf,yyy)| -rdf(x12,rdf_type,xxx)|rdf(x12,rdf_type,yyy). 0 [] -rdf(xxx,rdf_type,rdfs_Class)|rdf(xxx,rdfs_subClassOf,xxx). 0 [] -rdf(xxx,rdfs_subClassOf,yyy)| -rdf(yyy,rdfs_subClassOf,zzz)|rdf(xxx,rdfs_subClassOf,zzz). 0 [] -rdf(xxx,rdf_type,rdfs_ContainerMembershipProperty)|rdf(xxx,rdfs_subPropertyOf,rdfs_member). 0 [] -rdf(xxx,rdf_type,rdfs_Datatype)|rdf(xxx,rdfs_subClassOf,rdfs_Literal). end_of_list. ------- end included file otter/RDFS.otter------- include('otter/RDF.otter'). ------- start included file otter/RDF.otter------- formula_list(usable). all xxx aaa yyy (rdf(xxx,aaa,yyy)->rdf(aaa,rdf_type,rdf_Property)). all xxx aaa lll (rdf(xxx,aaa,lll)&'foo:xmlLit'(lll)-> (exists nnn (rdf(xxx,aaa,nnn)&rdf(nnn,rdf_type,rdf_XMLLiteral)))). end_of_list. -------> usable clausifies to: list(usable). 0 [] -rdf(xxx,x13,yyy)|rdf(x13,rdf_type,rdf_Property). 0 [] -rdf(xxx,x14,x15)| -'foo:xmlLit'(x15)|rdf(xxx,x14,$f2(xxx,x14,x15)). 0 [] -rdf(xxx,x14,x15)| -'foo:xmlLit'(x15)|rdf($f2(xxx,x14,x15),rdf_type,rdf_XMLLiteral). end_of_list. ------- end included file otter/RDF.otter------- formula_list(usable). rdf('http://example.org/foo',rdf_type,rdf_Property). rdf('http://example.org/bar',rdfs_subClassOf,'http://example.org/foo'). end_of_list. -------> usable clausifies to: list(usable). 0 [] rdf('http://example.org/foo',rdf_type,rdf_Property). 0 [] rdf('http://example.org/bar',rdfs_subClassOf,'http://example.org/foo'). end_of_list. SCAN INPUT: prop=0, horn=1, equality=0, symmetry=0, max_lits=3. 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=13): 1 [] -rdf(x,y,z)| -'foo:plainLit'(z)|rdf(x,y,$f1(x,y,z)). ** KEPT (pick-wt=13): 2 [] -rdf(x,y,z)| -'foo:plainLit'(z)|rdf($f1(x,y,z),rdf_type,rdfs_Literal). ** KEPT (pick-wt=12): 3 [] -rdf(x,rdfs_domain,y)| -rdf(z,x,u)|rdf(z,rdf_type,y). ** KEPT (pick-wt=12): 4 [] -rdf(x,rdfs_range,y)| -rdf(z,x,u)|rdf(u,rdf_type,y). ** KEPT (pick-wt=8): 5 [] -rdf(x,y,z)|rdf(x,rdf_type,rdfs_Resource). ** KEPT (pick-wt=8): 6 [] -rdf(x,y,z)|rdf(z,rdf_type,rdfs_Resource). ** KEPT (pick-wt=12): 7 [] -rdf(x,rdfs_subPropertyOf,y)| -rdf(y,rdfs_subPropertyOf,z)|rdf(x,rdfs_subPropertyOf,z). ** KEPT (pick-wt=8): 8 [] -rdf(x,rdf_type,rdf_Property)|rdf(x,rdfs_subPropertyOf,x). ** KEPT (pick-wt=12): 9 [] -rdf(x,rdfs_subPropertyOf,y)| -rdf(z,x,u)|rdf(z,y,u). ** KEPT (pick-wt=8): 10 [] -rdf(x,rdf_type,rdfs_Class)|rdf(x,rdfs_subClassOf,rdfs_Resource). ** KEPT (pick-wt=12): 11 [] -rdf(x,rdfs_subClassOf,y)| -rdf(z,rdf_type,x)|rdf(z,rdf_type,y). ** KEPT (pick-wt=8): 12 [] -rdf(x,rdf_type,rdfs_Class)|rdf(x,rdfs_subClassOf,x). ** KEPT (pick-wt=12): 13 [] -rdf(x,rdfs_subClassOf,y)| -rdf(y,rdfs_subClassOf,z)|rdf(x,rdfs_subClassOf,z). ** KEPT (pick-wt=8): 14 [] -rdf(x,rdf_type,rdfs_ContainerMembershipProperty)|rdf(x,rdfs_subPropertyOf,rdfs_member). ** KEPT (pick-wt=8): 15 [] -rdf(x,rdf_type,rdfs_Datatype)|rdf(x,rdfs_subClassOf,rdfs_Literal). ** KEPT (pick-wt=8): 16 [] -rdf(x,y,z)|rdf(y,rdf_type,rdf_Property). ** KEPT (pick-wt=13): 17 [] -rdf(x,y,z)| -'foo:xmlLit'(z)|rdf(x,y,$f2(x,y,z)). ** KEPT (pick-wt=13): 18 [] -rdf(x,y,z)| -'foo:xmlLit'(z)|rdf($f2(x,y,z),rdf_type,rdf_XMLLiteral). ------------> process sos: ** KEPT (pick-wt=4): 19 [] rdf('http://example.org/foo',rdf_type,rdf_Property). ** KEPT (pick-wt=4): 20 [] rdf('http://example.org/bar',rdfs_subClassOf,'http://example.org/foo'). ======= end of input processing ======= =========== start of search =========== given clause #1: (wt=4) 19 [] rdf('http://example.org/foo',rdf_type,rdf_Property). given clause #2: (wt=4) 20 [] rdf('http://example.org/bar',rdfs_subClassOf,'http://example.org/foo'). given clause #3: (wt=4) 21 [hyper,19,16] rdf(rdf_type,rdf_type,rdf_Property). given clause #4: (wt=4) 22 [hyper,19,8] rdf('http://example.org/foo',rdfs_subPropertyOf,'http://example.org/foo'). given clause #5: (wt=4) 23 [hyper,19,6] rdf(rdf_Property,rdf_type,rdfs_Resource). given clause #6: (wt=4) 24 [hyper,19,5] rdf('http://example.org/foo',rdf_type,rdfs_Resource). given clause #7: (wt=4) 25 [hyper,20,16] rdf(rdfs_subClassOf,rdf_type,rdf_Property). given clause #8: (wt=4) 26 [hyper,20,5] rdf('http://example.org/bar',rdf_type,rdfs_Resource). given clause #9: (wt=4) 27 [hyper,21,8] rdf(rdf_type,rdfs_subPropertyOf,rdf_type). given clause #10: (wt=4) 28 [hyper,21,5] rdf(rdf_type,rdf_type,rdfs_Resource). given clause #11: (wt=4) 29 [hyper,22,16] rdf(rdfs_subPropertyOf,rdf_type,rdf_Property). given clause #12: (wt=4) 30 [hyper,23,6] rdf(rdfs_Resource,rdf_type,rdfs_Resource). given clause #13: (wt=4) 31 [hyper,25,8] rdf(rdfs_subClassOf,rdfs_subPropertyOf,rdfs_subClassOf). given clause #14: (wt=4) 32 [hyper,25,5] rdf(rdfs_subClassOf,rdf_type,rdfs_Resource). given clause #15: (wt=4) 33 [hyper,29,8] rdf(rdfs_subPropertyOf,rdfs_subPropertyOf,rdfs_subPropertyOf). given clause #16: (wt=4) 34 [hyper,29,5] rdf(rdfs_subPropertyOf,rdf_type,rdfs_Resource). Search stopped because sos empty. Search stopped because sos empty. ============ end of search ============ -------------- statistics ------------- clauses given 16 clauses generated 77 clauses kept 34 clauses forward subsumed 63 clauses back subsumed 0 Kbytes malloced 127 ----------- times (seconds) ----------- user CPU time 0.00 (0 hr, 0 min, 0 sec) system CPU time 0.01 (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 Process 11931 finished Fri Nov 7 10:22:17 2003