----- 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 11933. 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/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,x1,yyy)|rdf(x1,rdf_type,rdf_Property). 0 [] -rdf(xxx,x2,x3)| -'foo:xmlLit'(x3)|rdf(xxx,x2,$f1(xxx,x2,x3)). 0 [] -rdf(xxx,x2,x3)| -'foo:xmlLit'(x3)|rdf($f1(xxx,x2,x3),rdf_type,rdf_XMLLiteral). end_of_list. ------- end included file otter/RDF.otter------- formula_list(usable). rdf('http://example.org/stmt1',rdf_type,rdf_Statement). rdf('http://example.org/stmt1',rdf_subject,'http://example.org/subject'). rdf('http://example.org/stmt1',rdf_predicate,'http://example.org/predicate'). rdf('http://example.org/stmt1',rdf_object,'http://example.org/object'). rdf('http://example.org/stmt2',rdf_type,rdf_Statement). rdf('http://example.org/stmt2',rdf_subject,'http://example.org/subject'). rdf('http://example.org/stmt2',rdf_predicate,'http://example.org/predicate'). rdf('http://example.org/stmt2',rdf_object,'http://example.org/object'). rdf('http://example.org/stmt1','http://example.org/property','http://example.org/foo'). -rdf('http://example.org/stmt2','http://example.org/property','http://example.org/foo'). end_of_list. -------> usable clausifies to: list(usable). 0 [] rdf('http://example.org/stmt1',rdf_type,rdf_Statement). 0 [] rdf('http://example.org/stmt1',rdf_subject,'http://example.org/subject'). 0 [] rdf('http://example.org/stmt1',rdf_predicate,'http://example.org/predicate'). 0 [] rdf('http://example.org/stmt1',rdf_object,'http://example.org/object'). 0 [] rdf('http://example.org/stmt2',rdf_type,rdf_Statement). 0 [] rdf('http://example.org/stmt2',rdf_subject,'http://example.org/subject'). 0 [] rdf('http://example.org/stmt2',rdf_predicate,'http://example.org/predicate'). 0 [] rdf('http://example.org/stmt2',rdf_object,'http://example.org/object'). 0 [] rdf('http://example.org/stmt1','http://example.org/property','http://example.org/foo'). 0 [] -rdf('http://example.org/stmt2','http://example.org/property','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=8): 1 [] -rdf(x,y,z)|rdf(y,rdf_type,rdf_Property). ** KEPT (pick-wt=13): 2 [] -rdf(x,y,z)| -'foo:xmlLit'(z)|rdf(x,y,$f1(x,y,z)). ** KEPT (pick-wt=13): 3 [] -rdf(x,y,z)| -'foo:xmlLit'(z)|rdf($f1(x,y,z),rdf_type,rdf_XMLLiteral). ** KEPT (pick-wt=4): 4 [] -rdf('http://example.org/stmt2','http://example.org/property','http://example.org/foo'). ------------> process sos: ** KEPT (pick-wt=4): 5 [] rdf('http://example.org/stmt1',rdf_type,rdf_Statement). ** KEPT (pick-wt=4): 6 [] rdf('http://example.org/stmt1',rdf_subject,'http://example.org/subject'). ** KEPT (pick-wt=4): 7 [] rdf('http://example.org/stmt1',rdf_predicate,'http://example.org/predicate'). ** KEPT (pick-wt=4): 8 [] rdf('http://example.org/stmt1',rdf_object,'http://example.org/object'). ** KEPT (pick-wt=4): 9 [] rdf('http://example.org/stmt2',rdf_type,rdf_Statement). ** KEPT (pick-wt=4): 10 [] rdf('http://example.org/stmt2',rdf_subject,'http://example.org/subject'). ** KEPT (pick-wt=4): 11 [] rdf('http://example.org/stmt2',rdf_predicate,'http://example.org/predicate'). ** KEPT (pick-wt=4): 12 [] rdf('http://example.org/stmt2',rdf_object,'http://example.org/object'). ** KEPT (pick-wt=4): 13 [] rdf('http://example.org/stmt1','http://example.org/property','http://example.org/foo'). ======= end of input processing ======= =========== start of search =========== given clause #1: (wt=4) 5 [] rdf('http://example.org/stmt1',rdf_type,rdf_Statement). given clause #2: (wt=4) 6 [] rdf('http://example.org/stmt1',rdf_subject,'http://example.org/subject'). given clause #3: (wt=4) 7 [] rdf('http://example.org/stmt1',rdf_predicate,'http://example.org/predicate'). given clause #4: (wt=4) 8 [] rdf('http://example.org/stmt1',rdf_object,'http://example.org/object'). given clause #5: (wt=4) 9 [] rdf('http://example.org/stmt2',rdf_type,rdf_Statement). given clause #6: (wt=4) 10 [] rdf('http://example.org/stmt2',rdf_subject,'http://example.org/subject'). given clause #7: (wt=4) 11 [] rdf('http://example.org/stmt2',rdf_predicate,'http://example.org/predicate'). given clause #8: (wt=4) 12 [] rdf('http://example.org/stmt2',rdf_object,'http://example.org/object'). given clause #9: (wt=4) 13 [] rdf('http://example.org/stmt1','http://example.org/property','http://example.org/foo'). given clause #10: (wt=4) 14 [hyper,5,1] rdf(rdf_type,rdf_type,rdf_Property). given clause #11: (wt=4) 15 [hyper,6,1] rdf(rdf_subject,rdf_type,rdf_Property). given clause #12: (wt=4) 16 [hyper,7,1] rdf(rdf_predicate,rdf_type,rdf_Property). given clause #13: (wt=4) 17 [hyper,8,1] rdf(rdf_object,rdf_type,rdf_Property). given clause #14: (wt=4) 18 [hyper,13,1] rdf('http://example.org/property',rdf_type,rdf_Property). Search stopped because sos empty. Search stopped because sos empty. ============ end of search ============ -------------- statistics ------------- clauses given 14 clauses generated 14 clauses kept 18 clauses forward subsumed 9 clauses back subsumed 0 Kbytes malloced 95 ----------- times (seconds) ----------- user CPU time 0.00 (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.00 for_sub time 0.00 back_sub time 0.00 conflict time 0.00 Process 11933 finished Fri Nov 7 10:22:17 2003