----- 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 11911. 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/bar',rdf_type,rdf_Property). rdf('http://example.org/bas',rdfs_subPropertyOf,'http://example.org/bar'). rdf('http://example.org/bar',rdfs_domain,'http://example.org/Domain1'). rdf('http://example.org/bas',rdfs_domain,'http://example.org/Domain2'). rdf('http://example.org/bar',rdfs_range,'http://example.org/Range1'). rdf('http://example.org/bas',rdfs_range,'http://example.org/Range2'). rdf('http://example.org/baz1','http://example.org/bas','http://example.org/baz2'). -(rdf('http://example.org/baz1',rdf_type,'http://example.org/Domain1')&rdf('http://example.org/baz1',rdf_type,'http://example.org/Domain2')&rdf('http://example.org/baz2',rdf_type,'http://example.org/Range1')&rdf('http://example.org/baz2',rdf_type,'http://example.org/Range2')). end_of_list. -------> usable clausifies to: list(usable). 0 [] rdf('http://example.org/bar',rdf_type,rdf_Property). 0 [] rdf('http://example.org/bas',rdfs_subPropertyOf,'http://example.org/bar'). 0 [] rdf('http://example.org/bar',rdfs_domain,'http://example.org/Domain1'). 0 [] rdf('http://example.org/bas',rdfs_domain,'http://example.org/Domain2'). 0 [] rdf('http://example.org/bar',rdfs_range,'http://example.org/Range1'). 0 [] rdf('http://example.org/bas',rdfs_range,'http://example.org/Range2'). 0 [] rdf('http://example.org/baz1','http://example.org/bas','http://example.org/baz2'). 0 [] -rdf('http://example.org/baz1',rdf_type,'http://example.org/Domain1')| -rdf('http://example.org/baz1',rdf_type,'http://example.org/Domain2')| -rdf('http://example.org/baz2',rdf_type,'http://example.org/Range1')| -rdf('http://example.org/baz2',rdf_type,'http://example.org/Range2'). end_of_list. SCAN INPUT: prop=0, horn=1, equality=0, symmetry=0, max_lits=4. 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). ** KEPT (pick-wt=16): 19 [] -rdf('http://example.org/baz1',rdf_type,'http://example.org/Domain1')| -rdf('http://example.org/baz1',rdf_type,'http://example.org/Domain2')| -rdf('http://example.org/baz2',rdf_type,'http://example.org/Range1')| -rdf('http://example.org/baz2',rdf_type,'http://example.org/Range2'). ------------> process sos: ** KEPT (pick-wt=4): 20 [] rdf('http://example.org/bar',rdf_type,rdf_Property). ** KEPT (pick-wt=4): 21 [] rdf('http://example.org/bas',rdfs_subPropertyOf,'http://example.org/bar'). ** KEPT (pick-wt=4): 22 [] rdf('http://example.org/bar',rdfs_domain,'http://example.org/Domain1'). ** KEPT (pick-wt=4): 23 [] rdf('http://example.org/bas',rdfs_domain,'http://example.org/Domain2'). ** KEPT (pick-wt=4): 24 [] rdf('http://example.org/bar',rdfs_range,'http://example.org/Range1'). ** KEPT (pick-wt=4): 25 [] rdf('http://example.org/bas',rdfs_range,'http://example.org/Range2'). ** KEPT (pick-wt=4): 26 [] rdf('http://example.org/baz1','http://example.org/bas','http://example.org/baz2'). ======= end of input processing ======= =========== start of search =========== given clause #1: (wt=4) 20 [] rdf('http://example.org/bar',rdf_type,rdf_Property). given clause #2: (wt=4) 21 [] rdf('http://example.org/bas',rdfs_subPropertyOf,'http://example.org/bar'). given clause #3: (wt=4) 22 [] rdf('http://example.org/bar',rdfs_domain,'http://example.org/Domain1'). given clause #4: (wt=4) 23 [] rdf('http://example.org/bas',rdfs_domain,'http://example.org/Domain2'). given clause #5: (wt=4) 24 [] rdf('http://example.org/bar',rdfs_range,'http://example.org/Range1'). given clause #6: (wt=4) 25 [] rdf('http://example.org/bas',rdfs_range,'http://example.org/Range2'). given clause #7: (wt=4) 26 [] rdf('http://example.org/baz1','http://example.org/bas','http://example.org/baz2'). given clause #8: (wt=4) 27 [hyper,20,16] rdf(rdf_type,rdf_type,rdf_Property). given clause #9: (wt=4) 28 [hyper,20,8] rdf('http://example.org/bar',rdfs_subPropertyOf,'http://example.org/bar'). given clause #10: (wt=4) 29 [hyper,20,6] rdf(rdf_Property,rdf_type,rdfs_Resource). given clause #11: (wt=4) 30 [hyper,20,5] rdf('http://example.org/bar',rdf_type,rdfs_Resource). given clause #12: (wt=4) 31 [hyper,21,16] rdf(rdfs_subPropertyOf,rdf_type,rdf_Property). given clause #13: (wt=4) 32 [hyper,21,5] rdf('http://example.org/bas',rdf_type,rdfs_Resource). given clause #14: (wt=4) 33 [hyper,22,16] rdf(rdfs_domain,rdf_type,rdf_Property). given clause #15: (wt=4) 34 [hyper,22,6] rdf('http://example.org/Domain1',rdf_type,rdfs_Resource). given clause #16: (wt=4) 35 [hyper,23,6] rdf('http://example.org/Domain2',rdf_type,rdfs_Resource). given clause #17: (wt=4) 36 [hyper,24,16] rdf(rdfs_range,rdf_type,rdf_Property). given clause #18: (wt=4) 37 [hyper,24,6] rdf('http://example.org/Range1',rdf_type,rdfs_Resource). given clause #19: (wt=4) 38 [hyper,25,6] rdf('http://example.org/Range2',rdf_type,rdfs_Resource). given clause #20: (wt=4) 39 [hyper,26,16] rdf('http://example.org/bas',rdf_type,rdf_Property). given clause #21: (wt=4) 40 [hyper,26,9,21] rdf('http://example.org/baz1','http://example.org/bar','http://example.org/baz2'). given clause #22: (wt=4) 41 [hyper,26,6] rdf('http://example.org/baz2',rdf_type,rdfs_Resource). given clause #23: (wt=4) 42 [hyper,26,5] rdf('http://example.org/baz1',rdf_type,rdfs_Resource). given clause #24: (wt=4) 43 [hyper,26,4,25] rdf('http://example.org/baz2',rdf_type,'http://example.org/Range2'). given clause #25: (wt=4) 44 [hyper,26,3,23] rdf('http://example.org/baz1',rdf_type,'http://example.org/Domain2'). given clause #26: (wt=4) 45 [hyper,27,8] rdf(rdf_type,rdfs_subPropertyOf,rdf_type). given clause #27: (wt=4) 46 [hyper,27,5] rdf(rdf_type,rdf_type,rdfs_Resource). given clause #28: (wt=4) 47 [hyper,29,6] rdf(rdfs_Resource,rdf_type,rdfs_Resource). given clause #29: (wt=4) 48 [hyper,31,8] rdf(rdfs_subPropertyOf,rdfs_subPropertyOf,rdfs_subPropertyOf). given clause #30: (wt=4) 49 [hyper,31,5] rdf(rdfs_subPropertyOf,rdf_type,rdfs_Resource). given clause #31: (wt=4) 50 [hyper,33,8] rdf(rdfs_domain,rdfs_subPropertyOf,rdfs_domain). given clause #32: (wt=4) 51 [hyper,33,5] rdf(rdfs_domain,rdf_type,rdfs_Resource). given clause #33: (wt=4) 52 [hyper,36,8] rdf(rdfs_range,rdfs_subPropertyOf,rdfs_range). given clause #34: (wt=4) 53 [hyper,36,5] rdf(rdfs_range,rdf_type,rdfs_Resource). given clause #35: (wt=4) 54 [hyper,39,8] rdf('http://example.org/bas',rdfs_subPropertyOf,'http://example.org/bas'). given clause #36: (wt=4) 55 [hyper,40,4,24] rdf('http://example.org/baz2',rdf_type,'http://example.org/Range1'). given clause #37: (wt=4) 56 [hyper,40,3,22] rdf('http://example.org/baz1',rdf_type,'http://example.org/Domain1'). -------- PROOF -------- -----> EMPTY CLAUSE at 0.00 sec ----> 57 [hyper,56,19,44,55,43] $F. Length of proof is 5. Level of proof is 2. ---------------- PROOF ---------------- 3 [] -rdf(x,rdfs_domain,y)| -rdf(z,x,u)|rdf(z,rdf_type,y). 4 [] -rdf(x,rdfs_range,y)| -rdf(z,x,u)|rdf(u,rdf_type,y). 9 [] -rdf(x,rdfs_subPropertyOf,y)| -rdf(z,x,u)|rdf(z,y,u). 19 [] -rdf('http://example.org/baz1',rdf_type,'http://example.org/Domain1')| -rdf('http://example.org/baz1',rdf_type,'http://example.org/Domain2')| -rdf('http://example.org/baz2',rdf_type,'http://example.org/Range1')| -rdf('http://example.org/baz2',rdf_type,'http://example.org/Range2'). 21 [] rdf('http://example.org/bas',rdfs_subPropertyOf,'http://example.org/bar'). 22 [] rdf('http://example.org/bar',rdfs_domain,'http://example.org/Domain1'). 23 [] rdf('http://example.org/bas',rdfs_domain,'http://example.org/Domain2'). 24 [] rdf('http://example.org/bar',rdfs_range,'http://example.org/Range1'). 25 [] rdf('http://example.org/bas',rdfs_range,'http://example.org/Range2'). 26 [] rdf('http://example.org/baz1','http://example.org/bas','http://example.org/baz2'). 40 [hyper,26,9,21] rdf('http://example.org/baz1','http://example.org/bar','http://example.org/baz2'). 43 [hyper,26,4,25] rdf('http://example.org/baz2',rdf_type,'http://example.org/Range2'). 44 [hyper,26,3,23] rdf('http://example.org/baz1',rdf_type,'http://example.org/Domain2'). 55 [hyper,40,4,24] rdf('http://example.org/baz2',rdf_type,'http://example.org/Range1'). 56 [hyper,40,3,22] rdf('http://example.org/baz1',rdf_type,'http://example.org/Domain1'). 57 [hyper,56,19,44,55,43] $F. ------------ end of proof ------------- Search stopped by max_proofs option. Search stopped by max_proofs option. ============ end of search ============ -------------- statistics ------------- clauses given 37 clauses generated 171 clauses kept 56 clauses forward subsumed 140 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 demod time 0.00 That finishes the proof of the theorem. Process 11911 finished Fri Nov 7 10:22:17 2003