----- 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 11935.

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/subj','http://example.org/prop','http://example.org/obj').
-(exists s (rdf(s,rdf_type,rdf_Statement)&rdf(s,rdf_subject,'http://example.org/subj')&rdf(s,rdf_predicate,'http://example.org/prop')&rdf(s,rdf_object,'http://example.org/obj'))).
end_of_list.

-------> usable clausifies to:

list(usable).
0 [] rdf('http://example.org/subj','http://example.org/prop','http://example.org/obj').
0 [] -rdf(x4,rdf_type,rdf_Statement)| -rdf(x4,rdf_subject,'http://example.org/subj')| -rdf(x4,rdf_predicate,'http://example.org/prop')| -rdf(x4,rdf_object,'http://example.org/obj').
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=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=16): 4 [] -rdf(x,rdf_type,rdf_Statement)| -rdf(x,rdf_subject,'http://example.org/subj')| -rdf(x,rdf_predicate,'http://example.org/prop')| -rdf(x,rdf_object,'http://example.org/obj').

------------> process sos:
** KEPT (pick-wt=4): 5 [] rdf('http://example.org/subj','http://example.org/prop','http://example.org/obj').

======= end of input processing =======

=========== start of search ===========

given clause #1: (wt=4) 5 [] rdf('http://example.org/subj','http://example.org/prop','http://example.org/obj').

given clause #2: (wt=4) 6 [hyper,5,1] rdf('http://example.org/prop',rdf_type,rdf_Property).

given clause #3: (wt=4) 7 [hyper,6,1] rdf(rdf_type,rdf_type,rdf_Property).

Search stopped because sos empty.


Search stopped because sos empty.

============ end of search ============

-------------- statistics -------------
clauses given                  3
clauses generated              3
clauses kept                   7
clauses forward subsumed       1
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 11935 finished Fri Nov  7 10:22:17 2003