----- Otter 3.3, August 2003 ----- The process was started by mccune on gyro.thornwood, Wed Aug 6 14:25:55 2003 The command was "../../bin/otter". The process ID is 5756. 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). formula_list(usable). all x (Wolf(x)->animal(x)). all x (Fox(x)->animal(x)). all x (Bird(x)->animal(x)). all x (Caterpillar(x)->animal(x)). all x (Snail(x)->animal(x)). all x (Grain(x)->plant(x)). exists x Wolf(x). exists x Fox(x). exists x Bird(x). exists x Caterpillar(x). exists x Snail(x). exists x Grain(x). all x (animal(x)-> (all y (plant(y)->eats(x,y)))| (all z (animal(z)&Smaller(z,x)& (exists u (plant(u)&eats(z,u)))->eats(x,z)))). all x y (Caterpillar(x)&Bird(y)->Smaller(x,y)). all x y (Snail(x)&Bird(y)->Smaller(x,y)). all x y (Bird(x)&Fox(y)->Smaller(x,y)). all x y (Fox(x)&Wolf(y)->Smaller(x,y)). all x y (Bird(x)&Caterpillar(y)->eats(x,y)). all x (Caterpillar(x)-> (exists y (plant(y)&eats(x,y)))). all x (Snail(x)-> (exists y (plant(y)&eats(x,y)))). all x y (Wolf(x)&Fox(y)-> -eats(x,y)). all x y (Wolf(x)&Grain(y)-> -eats(x,y)). all x y (Bird(x)&Snail(y)-> -eats(x,y)). -(exists x y (-$answer(eats(x,y))&animal(x)&animal(y)&eats(x,y)& (all z (Grain(z)->eats(y,z))))). end_of_list. -------> usable clausifies to: list(usable). 0 [] -Wolf(x)|animal(x). 0 [] -Fox(x)|animal(x). 0 [] -Bird(x)|animal(x). 0 [] -Caterpillar(x)|animal(x). 0 [] -Snail(x)|animal(x). 0 [] -Grain(x)|plant(x). 0 [] Wolf($c1). 0 [] Fox($c2). 0 [] Bird($c3). 0 [] Caterpillar($c4). 0 [] Snail($c5). 0 [] Grain($c6). 0 [] -animal(x)| -plant(y)|eats(x,y)| -animal(z)| -Smaller(z,x)| -plant(u)| -eats(z,u)|eats(x,z). 0 [] -Caterpillar(x)| -Bird(y)|Smaller(x,y). 0 [] -Snail(x)| -Bird(y)|Smaller(x,y). 0 [] -Bird(x)| -Fox(y)|Smaller(x,y). 0 [] -Fox(x)| -Wolf(y)|Smaller(x,y). 0 [] -Bird(x)| -Caterpillar(y)|eats(x,y). 0 [] -Caterpillar(x)|plant($f1(x)). 0 [] -Caterpillar(x)|eats(x,$f1(x)). 0 [] -Snail(x)|plant($f2(x)). 0 [] -Snail(x)|eats(x,$f2(x)). 0 [] -Wolf(x)| -Fox(y)| -eats(x,y). 0 [] -Wolf(x)| -Grain(y)| -eats(x,y). 0 [] -Bird(x)| -Snail(y)| -eats(x,y). 0 [] $answer(eats(x,y))| -animal(x)| -animal(y)| -eats(x,y)|Grain($f3(x,y)). 0 [] $answer(eats(x,y))| -animal(x)| -animal(y)| -eats(x,y)| -eats(y,$f3(x,y)). end_of_list. SCAN INPUT: prop=0, horn=0, equality=0, symmetry=0, max_lits=8. 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=4): 1 [] -Wolf(x)|animal(x). ** KEPT (pick-wt=4): 2 [] -Fox(x)|animal(x). ** KEPT (pick-wt=4): 3 [] -Bird(x)|animal(x). ** KEPT (pick-wt=4): 4 [] -Caterpillar(x)|animal(x). ** KEPT (pick-wt=4): 5 [] -Snail(x)|animal(x). ** KEPT (pick-wt=4): 6 [] -Grain(x)|plant(x). ** KEPT (pick-wt=20): 7 [] -animal(x)| -plant(y)|eats(x,y)| -animal(z)| -Smaller(z,x)| -plant(u)| -eats(z,u)|eats(x,z). ** KEPT (pick-wt=7): 8 [] -Caterpillar(x)| -Bird(y)|Smaller(x,y). ** KEPT (pick-wt=7): 9 [] -Snail(x)| -Bird(y)|Smaller(x,y). ** KEPT (pick-wt=7): 10 [] -Bird(x)| -Fox(y)|Smaller(x,y). ** KEPT (pick-wt=7): 11 [] -Fox(x)| -Wolf(y)|Smaller(x,y). ** KEPT (pick-wt=7): 12 [] -Bird(x)| -Caterpillar(y)|eats(x,y). ** KEPT (pick-wt=5): 13 [] -Caterpillar(x)|plant($f1(x)). ** KEPT (pick-wt=6): 14 [] -Caterpillar(x)|eats(x,$f1(x)). ** KEPT (pick-wt=5): 15 [] -Snail(x)|plant($f2(x)). ** KEPT (pick-wt=6): 16 [] -Snail(x)|eats(x,$f2(x)). ** KEPT (pick-wt=7): 17 [] -Wolf(x)| -Fox(y)| -eats(x,y). ** KEPT (pick-wt=7): 18 [] -Wolf(x)| -Grain(y)| -eats(x,y). ** KEPT (pick-wt=7): 19 [] -Bird(x)| -Snail(y)| -eats(x,y). ** KEPT (pick-wt=11): 20 [] $answer(eats(x,y))| -animal(x)| -animal(y)| -eats(x,y)|Grain($f3(x,y)). ** KEPT (pick-wt=12): 21 [] $answer(eats(x,y))| -animal(x)| -animal(y)| -eats(x,y)| -eats(y,$f3(x,y)). ------------> process sos: ** KEPT (pick-wt=2): 29 [] Wolf($c1). ** KEPT (pick-wt=2): 30 [] Fox($c2). ** KEPT (pick-wt=2): 31 [] Bird($c3). ** KEPT (pick-wt=2): 32 [] Caterpillar($c4). ** KEPT (pick-wt=2): 33 [] Snail($c5). ** KEPT (pick-wt=2): 34 [] Grain($c6). ======= end of input processing ======= =========== start of search =========== given clause #1: (wt=2) 29 [] Wolf($c1). given clause #2: (wt=2) 30 [] Fox($c2). given clause #3: (wt=2) 31 [] Bird($c3). given clause #4: (wt=2) 32 [] Caterpillar($c4). given clause #5: (wt=2) 33 [] Snail($c5). given clause #6: (wt=2) 34 [] Grain($c6). given clause #7: (wt=2) 35 [hyper,29,1] animal($c1). given clause #8: (wt=2) 37 [hyper,30,2] animal($c2). given clause #9: (wt=2) 39 [hyper,31,3] animal($c3). given clause #10: (wt=2) 44 [hyper,32,4] animal($c4). given clause #11: (wt=3) 36 [hyper,30,11,29] Smaller($c2,$c1). given clause #12: (wt=2) 48 [hyper,33,5] animal($c5). given clause #13: (wt=2) 49 [hyper,34,6] plant($c6). given clause #14: (wt=3) 38 [hyper,31,10,30] Smaller($c3,$c2). given clause #15: (wt=3) 41 [hyper,32,13] plant($f1($c4)). given clause #16: (wt=4) 40 [hyper,32,14] eats($c4,$f1($c4)). given clause #17: (wt=3) 42 [hyper,32,12,31] eats($c3,$c4). given clause #18: (wt=3) 43 [hyper,32,8,31] Smaller($c4,$c3). given clause #19: (wt=3) 46 [hyper,33,15] plant($f2($c5)). given clause #20: (wt=3) 47 [hyper,33,9,31] Smaller($c5,$c3). given clause #21: (wt=4) 45 [hyper,33,16] eats($c5,$f2($c5)). given clause #22: (wt=4) 50 [hyper,42,20,39,44] $answer(eats($c3,$c4))|Grain($f3($c3,$c4)). given clause #23: (wt=4) 54 [hyper,50,6] $answer(eats($c3,$c4))|plant($f3($c3,$c4)). given clause #24: (wt=6) 52 [hyper,45,7,39,49,48,47,46] eats($c3,$c6)|eats($c3,$c5). given clause #25: (wt=3) 61 [hyper,52,19,31,33] eats($c3,$c6). given clause #26: (wt=7) 51 [hyper,45,23,39,46,48,47] eats($c3,$f2($c5))|eats($c3,$c5). given clause #27: (wt=4) 67 [hyper,51,19,31,33] eats($c3,$f2($c5)). given clause #28: (wt=6) 62 [hyper,61,23,37,49,39,38] eats($c2,$c6)|eats($c2,$c3). given clause #29: (wt=7) 53 [hyper,45,7,39,41,48,47,46] eats($c3,$f1($c4))|eats($c3,$c5). given clause #30: (wt=4) 74 [hyper,53,19,31,33] eats($c3,$f1($c4)). given clause #31: (wt=8) 55 [hyper,54,7,39,48,47,46,45] $answer(eats($c3,$c4))|eats($c3,$f3($c3,$c4))|eats($c3,$c5). given clause #32: (wt=5) 76 [hyper,55,19,31,33] $answer(eats($c3,$c4))|eats($c3,$f3($c3,$c4)). given clause #33: (wt=7) 64 [hyper,61,7,37,46,39,38,49] eats($c2,$f2($c5))|eats($c2,$c3). given clause #34: (wt=7) 65 [hyper,61,7,37,41,39,38,49] eats($c2,$f1($c4))|eats($c2,$c3). given clause #35: (wt=7) 72 [hyper,62,20,37,39] eats($c2,$c6)|$answer(eats($c2,$c3))|Grain($f3($c2,$c3)). given clause #36: (wt=8) 63 [hyper,61,7,37,54,39,38,49] eats($c2,$f3($c3,$c4))|eats($c2,$c3)|$answer(eats($c3,$c4)). given clause #37: (wt=7) 79 [hyper,72,6] eats($c2,$c6)|$answer(eats($c2,$c3))|plant($f3($c2,$c3)). given clause #38: (wt=8) 77 [hyper,64,20,37,39] eats($c2,$f2($c5))|$answer(eats($c2,$c3))|Grain($f3($c2,$c3)). given clause #39: (wt=8) 78 [hyper,65,20,37,39] eats($c2,$f1($c4))|$answer(eats($c2,$c3))|Grain($f3($c2,$c3)). given clause #40: (wt=8) 82 [hyper,77,6] eats($c2,$f2($c5))|$answer(eats($c2,$c3))|plant($f3($c2,$c3)). given clause #41: (wt=9) 68 [hyper,62,23,35,49,37,36] eats($c2,$c3)|eats($c1,$c6)|eats($c1,$c2). given clause #42: (wt=6) 86 [hyper,68,18,29,34] eats($c2,$c3)|eats($c1,$c2). given clause #43: (wt=3) 91 [hyper,86,17,29,30] eats($c2,$c3). given clause #44: (wt=4) 92 [hyper,91,20,37,39] $answer(eats($c2,$c3))|Grain($f3($c2,$c3)). given clause #45: (wt=4) 93 [hyper,92,6] $answer(eats($c2,$c3))|plant($f3($c2,$c3)). given clause #46: (wt=8) 94 [hyper,93,7,39,48,47,46,45] $answer(eats($c2,$c3))|eats($c3,$f3($c2,$c3))|eats($c3,$c5). given clause #47: (wt=3) 95 [hyper,94,21,37,39,91,factor_simp] $answer(eats($c2,$c3))|eats($c3,$c5). -------- PROOF -------- 99 [hyper,95,19,31,33] $answer(eats($c2,$c3)). -----> EMPTY CLAUSE at 0.01 sec ----> 99 [hyper,95,19,31,33] $answer(eats($c2,$c3)). Length of proof is 21. Level of proof is 11. ---------------- PROOF ---------------- 1 [] -Wolf(x)|animal(x). 2 [] -Fox(x)|animal(x). 3 [] -Bird(x)|animal(x). 5 [] -Snail(x)|animal(x). 6 [] -Grain(x)|plant(x). 7 [] -animal(x)| -plant(y)|eats(x,y)| -animal(z)| -Smaller(z,x)| -plant(u)| -eats(z,u)|eats(x,z). 9 [] -Snail(x)| -Bird(y)|Smaller(x,y). 10 [] -Bird(x)| -Fox(y)|Smaller(x,y). 11 [] -Fox(x)| -Wolf(y)|Smaller(x,y). 15 [] -Snail(x)|plant($f2(x)). 16 [] -Snail(x)|eats(x,$f2(x)). 17 [] -Wolf(x)| -Fox(y)| -eats(x,y). 18 [] -Wolf(x)| -Grain(y)| -eats(x,y). 19 [] -Bird(x)| -Snail(y)| -eats(x,y). 20 [] $answer(eats(x,y))| -animal(x)| -animal(y)| -eats(x,y)|Grain($f3(x,y)). 21 [] $answer(eats(x,y))| -animal(x)| -animal(y)| -eats(x,y)| -eats(y,$f3(x,y)). 23 [factor,7.2.6] -animal(x)| -plant(y)|eats(x,y)| -animal(z)| -Smaller(z,x)| -eats(z,y)|eats(x,z). 29 [] Wolf($c1). 30 [] Fox($c2). 31 [] Bird($c3). 33 [] Snail($c5). 34 [] Grain($c6). 35 [hyper,29,1] animal($c1). 36 [hyper,30,11,29] Smaller($c2,$c1). 37 [hyper,30,2] animal($c2). 38 [hyper,31,10,30] Smaller($c3,$c2). 39 [hyper,31,3] animal($c3). 45 [hyper,33,16] eats($c5,$f2($c5)). 46 [hyper,33,15] plant($f2($c5)). 47 [hyper,33,9,31] Smaller($c5,$c3). 48 [hyper,33,5] animal($c5). 49 [hyper,34,6] plant($c6). 52 [hyper,45,7,39,49,48,47,46] eats($c3,$c6)|eats($c3,$c5). 61 [hyper,52,19,31,33] eats($c3,$c6). 62 [hyper,61,23,37,49,39,38] eats($c2,$c6)|eats($c2,$c3). 68 [hyper,62,23,35,49,37,36] eats($c2,$c3)|eats($c1,$c6)|eats($c1,$c2). 86 [hyper,68,18,29,34] eats($c2,$c3)|eats($c1,$c2). 91 [hyper,86,17,29,30] eats($c2,$c3). 92 [hyper,91,20,37,39] $answer(eats($c2,$c3))|Grain($f3($c2,$c3)). 93 [hyper,92,6] $answer(eats($c2,$c3))|plant($f3($c2,$c3)). 94 [hyper,93,7,39,48,47,46,45] $answer(eats($c2,$c3))|eats($c3,$f3($c2,$c3))|eats($c3,$c5). 95 [hyper,94,21,37,39,91,factor_simp] $answer(eats($c2,$c3))|eats($c3,$c5). 99 [hyper,95,19,31,33] $answer(eats($c2,$c3)). ------------ end of proof ------------- Search stopped by max_proofs option. Search stopped by max_proofs option. ============ end of search ============ -------------- statistics ------------- clauses given 47 clauses generated 161 clauses kept 98 clauses forward subsumed 85 clauses back subsumed 37 Kbytes malloced 223 ----------- times (seconds) ----------- user CPU time 0.01 (0 hr, 0 min, 0 sec) system CPU time 0.01 (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.01 conflict time 0.00 That finishes the proof of the theorem. Process 5756 finished Wed Aug 6 14:25:55 2003