----- Otter 3.2, August 2001 ----- The process was started by sandro on roke.hawke.org, Wed Sep 3 15:24:48 2003 The command was "otter". The process ID is 29599. 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(sigint_interact). include('otter/owlAx-oneOf.otter'). ------- start included file otter/owlAx-oneOf.otter------- formula_list(usable). all CLASS LIST (rdf(CLASS,owl_oneOf,LIST)-> (all INST (rdf(INST,rdf_type,CLASS)<->inList(INST,LIST)))). all MEMBER LIST HEAD TAIL (rdf(LIST,rdf_first,HEAD)&rdf(LIST,rdf_rest,TAIL)-> (inList(MEMBER,LIST)<->rdf(MEMBER,owl_sameAs,HEAD)|inList(MEMBER,TAIL))). all MEMBER (-inList(MEMBER,rdf_nil)). end_of_list. -------> usable clausifies to: list(usable). 0 [] -rdf(x1,owl_oneOf,x2)| -rdf(x3,rdf_type,x1)|inList(x3,x2). 0 [] -rdf(x1,owl_oneOf,x2)|rdf(x3,rdf_type,x1)| -inList(x3,x2). 0 [] -rdf(x4,rdf_first,x5)| -rdf(x4,rdf_rest,x6)| -inList(x7,x4)|rdf(x7,owl_sameAs,x5)|inList(x7,x6). 0 [] -rdf(x4,rdf_first,x5)| -rdf(x4,rdf_rest,x6)|inList(x7,x4)| -rdf(x7,owl_sameAs,x5). 0 [] -rdf(x4,rdf_first,x5)| -rdf(x4,rdf_rest,x6)|inList(x7,x4)| -inList(x7,x6). 0 [] -inList(x8,rdf_nil). end_of_list. ------- end included file otter/owlAx-oneOf.otter------- formula_list(usable). exists s t u s0 s1 s2 (rdf(s2,rdf_type,rdf_List)&rdf(s2,rdf_first,ns50_small)&rdf(s1,rdf_type,rdf_List)&rdf(s2,rdf_rest,s1)&rdf(s1,rdf_first,ns50_medium)&rdf(s0,rdf_type,rdf_List)&rdf(s1,rdf_rest,s0)&rdf(s0,rdf_first,ns50_large)&rdf(s0,rdf_rest,rdf_nil)&rdf(ns50_T1,owl_oneOf,s2)&rdf(u,rdf_type,rdf_List)&rdf(u,rdf_first,ns50_large)&rdf(t,rdf_type,rdf_List)&rdf(u,rdf_rest,t)&rdf(t,rdf_first,ns50_medium)&rdf(s,rdf_type,rdf_List)&rdf(t,rdf_rest,s)&rdf(s,rdf_first,ns50_small)&rdf(s,rdf_rest,rdf_nil)&rdf(ns50_T2,owl_oneOf,u)&rdf(ns50_myT,rdf_type,ns50_T1)& -rdf(ns50_myT,rdf_type,ns50_T2)). end_of_list. -------> usable clausifies to: list(usable). 0 [] rdf($c1,rdf_type,rdf_List). 0 [] rdf($c1,rdf_first,ns50_small). 0 [] rdf($c2,rdf_type,rdf_List). 0 [] rdf($c1,rdf_rest,$c2). 0 [] rdf($c2,rdf_first,ns50_medium). 0 [] rdf($c3,rdf_type,rdf_List). 0 [] rdf($c2,rdf_rest,$c3). 0 [] rdf($c3,rdf_first,ns50_large). 0 [] rdf($c3,rdf_rest,rdf_nil). 0 [] rdf(ns50_T1,owl_oneOf,$c1). 0 [] rdf($c4,rdf_type,rdf_List). 0 [] rdf($c4,rdf_first,ns50_large). 0 [] rdf($c5,rdf_type,rdf_List). 0 [] rdf($c4,rdf_rest,$c5). 0 [] rdf($c5,rdf_first,ns50_medium). 0 [] rdf($c6,rdf_type,rdf_List). 0 [] rdf($c5,rdf_rest,$c6). 0 [] rdf($c6,rdf_first,ns50_small). 0 [] rdf($c6,rdf_rest,rdf_nil). 0 [] rdf(ns50_T2,owl_oneOf,$c4). 0 [] rdf(ns50_myT,rdf_type,ns50_T1). 0 [] -rdf(ns50_myT,rdf_type,ns50_T2). end_of_list. SCAN INPUT: prop=0, horn=0, equality=0, symmetry=0, max_lits=5. This is a non-Horn set without equality. The strategy will be ordered hyper_res, unit deletion, and factoring, with satellites in sos and with nuclei in usable. dependent: set(hyper_res). dependent: set(factor). dependent: set(unit_deletion). ------------> process usable: ** KEPT (pick-wt=11): 1 [] -rdf(x,owl_oneOf,y)| -rdf(z,rdf_type,x)|inList(z,y). ** KEPT (pick-wt=11): 2 [] -rdf(x,owl_oneOf,y)|rdf(z,rdf_type,x)| -inList(z,y). ** KEPT (pick-wt=18): 3 [] -rdf(x,rdf_first,y)| -rdf(x,rdf_rest,z)| -inList(u,x)|rdf(u,owl_sameAs,y)|inList(u,z). ** KEPT (pick-wt=15): 4 [] -rdf(x,rdf_first,y)| -rdf(x,rdf_rest,z)|inList(u,x)| -rdf(u,owl_sameAs,y). ** KEPT (pick-wt=14): 5 [] -rdf(x,rdf_first,y)| -rdf(x,rdf_rest,z)|inList(u,x)| -inList(u,z). ** KEPT (pick-wt=3): 6 [] -inList(x,rdf_nil). ** KEPT (pick-wt=4): 7 [] -rdf(ns50_myT,rdf_type,ns50_T2). ------------> process sos: ** KEPT (pick-wt=4): 8 [] rdf($c1,rdf_type,rdf_List). ** KEPT (pick-wt=4): 9 [] rdf($c1,rdf_first,ns50_small). ** KEPT (pick-wt=4): 10 [] rdf($c2,rdf_type,rdf_List). ** KEPT (pick-wt=4): 11 [] rdf($c1,rdf_rest,$c2). ** KEPT (pick-wt=4): 12 [] rdf($c2,rdf_first,ns50_medium). ** KEPT (pick-wt=4): 13 [] rdf($c3,rdf_type,rdf_List). ** KEPT (pick-wt=4): 14 [] rdf($c2,rdf_rest,$c3). ** KEPT (pick-wt=4): 15 [] rdf($c3,rdf_first,ns50_large). ** KEPT (pick-wt=4): 16 [] rdf($c3,rdf_rest,rdf_nil). ** KEPT (pick-wt=4): 17 [] rdf(ns50_T1,owl_oneOf,$c1). ** KEPT (pick-wt=4): 18 [] rdf($c4,rdf_type,rdf_List). ** KEPT (pick-wt=4): 19 [] rdf($c4,rdf_first,ns50_large). ** KEPT (pick-wt=4): 20 [] rdf($c5,rdf_type,rdf_List). ** KEPT (pick-wt=4): 21 [] rdf($c4,rdf_rest,$c5). ** KEPT (pick-wt=4): 22 [] rdf($c5,rdf_first,ns50_medium). ** KEPT (pick-wt=4): 23 [] rdf($c6,rdf_type,rdf_List). ** KEPT (pick-wt=4): 24 [] rdf($c5,rdf_rest,$c6). ** KEPT (pick-wt=4): 25 [] rdf($c6,rdf_first,ns50_small). ** KEPT (pick-wt=4): 26 [] rdf($c6,rdf_rest,rdf_nil). ** KEPT (pick-wt=4): 27 [] rdf(ns50_T2,owl_oneOf,$c4). ** KEPT (pick-wt=4): 28 [] rdf(ns50_myT,rdf_type,ns50_T1). ======= end of input processing ======= =========== start of search =========== given clause #1: (wt=4) 8 [] rdf($c1,rdf_type,rdf_List). given clause #2: (wt=4) 9 [] rdf($c1,rdf_first,ns50_small). given clause #3: (wt=4) 10 [] rdf($c2,rdf_type,rdf_List). given clause #4: (wt=4) 11 [] rdf($c1,rdf_rest,$c2). given clause #5: (wt=4) 12 [] rdf($c2,rdf_first,ns50_medium). given clause #6: (wt=4) 13 [] rdf($c3,rdf_type,rdf_List). given clause #7: (wt=4) 14 [] rdf($c2,rdf_rest,$c3). given clause #8: (wt=4) 15 [] rdf($c3,rdf_first,ns50_large). given clause #9: (wt=4) 16 [] rdf($c3,rdf_rest,rdf_nil). given clause #10: (wt=4) 17 [] rdf(ns50_T1,owl_oneOf,$c1). given clause #11: (wt=4) 18 [] rdf($c4,rdf_type,rdf_List). given clause #12: (wt=4) 19 [] rdf($c4,rdf_first,ns50_large). given clause #13: (wt=4) 20 [] rdf($c5,rdf_type,rdf_List). given clause #14: (wt=4) 21 [] rdf($c4,rdf_rest,$c5). given clause #15: (wt=4) 22 [] rdf($c5,rdf_first,ns50_medium). given clause #16: (wt=4) 23 [] rdf($c6,rdf_type,rdf_List). given clause #17: (wt=4) 24 [] rdf($c5,rdf_rest,$c6). given clause #18: (wt=4) 25 [] rdf($c6,rdf_first,ns50_small). given clause #19: (wt=4) 26 [] rdf($c6,rdf_rest,rdf_nil). given clause #20: (wt=4) 27 [] rdf(ns50_T2,owl_oneOf,$c4). given clause #21: (wt=4) 28 [] rdf(ns50_myT,rdf_type,ns50_T1). given clause #22: (wt=3) 29 [hyper,28,1,17] inList(ns50_myT,$c1). given clause #23: (wt=7) 30 [hyper,29,3,9,11] rdf(ns50_myT,owl_sameAs,ns50_small)|inList(ns50_myT,$c2). given clause #24: (wt=11) 31 [hyper,30,3,12,14] rdf(ns50_myT,owl_sameAs,ns50_small)|rdf(ns50_myT,owl_sameAs,ns50_medium)|inList(ns50_myT,$c3). given clause #25: (wt=12) 32 [hyper,31,3,15,16,unit_del,6] rdf(ns50_myT,owl_sameAs,ns50_small)|rdf(ns50_myT,owl_sameAs,ns50_medium)|rdf(ns50_myT,owl_sameAs,ns50_large). given clause #26: (wt=11) 33 [hyper,32,4,25,26] rdf(ns50_myT,owl_sameAs,ns50_medium)|rdf(ns50_myT,owl_sameAs,ns50_large)|inList(ns50_myT,$c6). given clause #27: (wt=11) 34 [hyper,32,4,22,24] rdf(ns50_myT,owl_sameAs,ns50_small)|rdf(ns50_myT,owl_sameAs,ns50_large)|inList(ns50_myT,$c5). given clause #28: (wt=11) 35 [hyper,32,4,19,21] rdf(ns50_myT,owl_sameAs,ns50_small)|rdf(ns50_myT,owl_sameAs,ns50_medium)|inList(ns50_myT,$c4). given clause #29: (wt=8) 38 [hyper,35,2,27,unit_del,7] rdf(ns50_myT,owl_sameAs,ns50_small)|rdf(ns50_myT,owl_sameAs,ns50_medium). given clause #30: (wt=7) 39 [hyper,38,4,25,26] rdf(ns50_myT,owl_sameAs,ns50_medium)|inList(ns50_myT,$c6). given clause #31: (wt=11) 37 [hyper,34,5,19,21] rdf(ns50_myT,owl_sameAs,ns50_small)|rdf(ns50_myT,owl_sameAs,ns50_large)|inList(ns50_myT,$c4). given clause #32: (wt=7) 40 [hyper,38,4,22,24] rdf(ns50_myT,owl_sameAs,ns50_small)|inList(ns50_myT,$c5). given clause #33: (wt=7) 41 [hyper,39,5,22,24] rdf(ns50_myT,owl_sameAs,ns50_medium)|inList(ns50_myT,$c5). given clause #34: (wt=7) 43 [hyper,40,5,19,21] rdf(ns50_myT,owl_sameAs,ns50_small)|inList(ns50_myT,$c4). given clause #35: (wt=4) 45 [hyper,43,2,27,unit_del,7] rdf(ns50_myT,owl_sameAs,ns50_small). given clause #36: (wt=7) 44 [hyper,41,5,19,21] rdf(ns50_myT,owl_sameAs,ns50_medium)|inList(ns50_myT,$c4). given clause #37: (wt=3) 46 [hyper,45,4,25,26] inList(ns50_myT,$c6). given clause #38: (wt=3) 48 [hyper,46,5,22,24] inList(ns50_myT,$c5). given clause #39: (wt=3) 49 [hyper,48,5,19,21] inList(ns50_myT,$c4). -------- PROOF -------- ----> UNIT CONFLICT at 0.01 sec ----> 51 [binary,50.1,7.1] $F. Length of proof is 13. Level of proof is 13. ---------------- PROOF ---------------- 1 [] -rdf(x,owl_oneOf,y)| -rdf(z,rdf_type,x)|inList(z,y). 2 [] -rdf(x,owl_oneOf,y)|rdf(z,rdf_type,x)| -inList(z,y). 3 [] -rdf(x,rdf_first,y)| -rdf(x,rdf_rest,z)| -inList(u,x)|rdf(u,owl_sameAs,y)|inList(u,z). 4 [] -rdf(x,rdf_first,y)| -rdf(x,rdf_rest,z)|inList(u,x)| -rdf(u,owl_sameAs,y). 5 [] -rdf(x,rdf_first,y)| -rdf(x,rdf_rest,z)|inList(u,x)| -inList(u,z). 6 [] -inList(x,rdf_nil). 7 [] -rdf(ns50_myT,rdf_type,ns50_T2). 9 [] rdf($c1,rdf_first,ns50_small). 11 [] rdf($c1,rdf_rest,$c2). 12 [] rdf($c2,rdf_first,ns50_medium). 14 [] rdf($c2,rdf_rest,$c3). 15 [] rdf($c3,rdf_first,ns50_large). 16 [] rdf($c3,rdf_rest,rdf_nil). 17 [] rdf(ns50_T1,owl_oneOf,$c1). 19 [] rdf($c4,rdf_first,ns50_large). 21 [] rdf($c4,rdf_rest,$c5). 22 [] rdf($c5,rdf_first,ns50_medium). 24 [] rdf($c5,rdf_rest,$c6). 25 [] rdf($c6,rdf_first,ns50_small). 26 [] rdf($c6,rdf_rest,rdf_nil). 27 [] rdf(ns50_T2,owl_oneOf,$c4). 28 [] rdf(ns50_myT,rdf_type,ns50_T1). 29 [hyper,28,1,17] inList(ns50_myT,$c1). 30 [hyper,29,3,9,11] rdf(ns50_myT,owl_sameAs,ns50_small)|inList(ns50_myT,$c2). 31 [hyper,30,3,12,14] rdf(ns50_myT,owl_sameAs,ns50_small)|rdf(ns50_myT,owl_sameAs,ns50_medium)|inList(ns50_myT,$c3). 32 [hyper,31,3,15,16,unit_del,6] rdf(ns50_myT,owl_sameAs,ns50_small)|rdf(ns50_myT,owl_sameAs,ns50_medium)|rdf(ns50_myT,owl_sameAs,ns50_large). 35 [hyper,32,4,19,21] rdf(ns50_myT,owl_sameAs,ns50_small)|rdf(ns50_myT,owl_sameAs,ns50_medium)|inList(ns50_myT,$c4). 38 [hyper,35,2,27,unit_del,7] rdf(ns50_myT,owl_sameAs,ns50_small)|rdf(ns50_myT,owl_sameAs,ns50_medium). 40 [hyper,38,4,22,24] rdf(ns50_myT,owl_sameAs,ns50_small)|inList(ns50_myT,$c5). 43 [hyper,40,5,19,21] rdf(ns50_myT,owl_sameAs,ns50_small)|inList(ns50_myT,$c4). 45 [hyper,43,2,27,unit_del,7] rdf(ns50_myT,owl_sameAs,ns50_small). 46 [hyper,45,4,25,26] inList(ns50_myT,$c6). 48 [hyper,46,5,22,24] inList(ns50_myT,$c5). 49 [hyper,48,5,19,21] inList(ns50_myT,$c4). 50 [hyper,49,2,27] rdf(ns50_myT,rdf_type,ns50_T2). 51 [binary,50.1,7.1] $F. ------------ end of proof ------------- Search stopped by max_proofs option. Search stopped by max_proofs option. ============ end of search ============ -------------- statistics ------------- clauses given 39 clauses generated 43 clauses kept 50 clauses forward subsumed 21 clauses back subsumed 15 Kbytes malloced 127 ----------- 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 29599 finished Wed Sep 3 15:24:48 2003