----- 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 11913. 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). exists s (rdf(s,'http://example.org/prop',lit)&'foo:plainLit'(lit)& -(exists t (rdf(t,'http://example.org/prop',lit)&'foo:plainLit'(lit)))&'foo:plainLit'(lit)). end_of_list. -------> usable clausifies to: list(usable). 0 [] rdf($c1,'http://example.org/prop',lit). 0 [] 'foo:plainLit'(lit). 0 [] -rdf(x4,'http://example.org/prop',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(x,'http://example.org/prop',lit)| -'foo:plainLit'(lit). ------------> process sos: ** KEPT (pick-wt=4): 5 [] rdf($c1,'http://example.org/prop',lit). ** KEPT (pick-wt=2): 6 [] 'foo:plainLit'(lit). ======= end of input processing ======= =========== start of search =========== given clause #1: (wt=4) 5 [] rdf($c1,'http://example.org/prop',lit). given clause #2: (wt=2) 6 [] 'foo:plainLit'(lit). -------- PROOF -------- -----> EMPTY CLAUSE at 0.01 sec ----> 8 [hyper,6,4,5] $F. Length of proof is 0. Level of proof is 0. ---------------- PROOF ---------------- 4 [] -rdf(x,'http://example.org/prop',lit)| -'foo:plainLit'(lit). 5 [] rdf($c1,'http://example.org/prop',lit). 6 [] 'foo:plainLit'(lit). 8 [hyper,6,4,5] $F. ------------ end of proof ------------- Search stopped by max_proofs option. Search stopped by max_proofs option. ============ end of search ============ -------------- statistics ------------- clauses given 2 clauses generated 2 clauses kept 7 clauses forward subsumed 0 clauses back subsumed 0 Kbytes malloced 95 ----------- times (seconds) ----------- user CPU time 0.01 (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 demod time 0.00 That finishes the proof of the theorem. Process 11913 finished Fri Nov 7 10:22:17 2003