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

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(ns9_Andr_25C3_25A9,ns9_owes,lit).
'foo:plainLit'(lit).
-(rdf(ns9_Andr_C3_A9,ns9_owes,lit)&'foo:plainLit'(lit)).
end_of_list.

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

list(usable).
0 [] rdf(ns9_Andr_25C3_25A9,ns9_owes,lit).
0 [] 'foo:plainLit'(lit).
0 [] -rdf(ns9_Andr_C3_A9,ns9_owes,lit)| -'foo:plainLit'(lit).
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=6): 4 [] -rdf(ns9_Andr_C3_A9,ns9_owes,lit)| -'foo:plainLit'(lit).

------------> process sos:
** KEPT (pick-wt=4): 5 [] rdf(ns9_Andr_25C3_25A9,ns9_owes,lit).
** KEPT (pick-wt=2): 6 [] 'foo:plainLit'(lit).

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

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

given clause #1: (wt=4) 5 [] rdf(ns9_Andr_25C3_25A9,ns9_owes,lit).

given clause #2: (wt=2) 6 [] 'foo:plainLit'(lit).

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

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

Search stopped because sos empty.


Search stopped because sos empty.

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

-------------- statistics -------------
clauses given                  4
clauses generated              3
clauses kept                   8
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 11923 finished Fri Nov  7 10:22:17 2003