;;; Schubert's STEAMROLLER Problem ;;; ;;; Problem: ;;; Wolves, foxes, birds, caterpillars, and snails are animals, ;;; and there are some of each. ;;; Also there are some grains, and grains are plants. ;;; Every animal either likes to eat all plants, or all animals much ;;; smaller than itself that like to eat some plants ;;; Caterpillers and snails are much smaller than birds, ;;; which are much smaller than foxes, ;;; which in turn are much smaller than wolves. ;;; Wolves do not like to eat foxes or grains, ;;; while birds like to eat caterpillars but not snails. ;;; Caterpillars and snails like to eat some plants ;;; Therefore there is an animal that likes to eat a grain-eating animal ;;; ;;; EPILOG attempts at this problem in three ways (identical rules/facts/ ;;; questions for each): ;;; 1. with full forward inference ;;; 2. with no forward inference (all goal-directed reasoning) ;;; 3. with partial forward inference (i.e. allowing only full instantiations) ;;; ;;; ANSWER: ;;; THE FOX LIKES TO EAT THE BIRD WHICH LIKES TO EAT THE GRAIN. ;;; The bird is a plant eating animal because it does not like to eat snails, ;;; which like to eat some plant, so it does not like to eat ALL such animals. ;;; Therefore it must like to eat all plants. ;;; The fox is not a plant eating animal, because the wolf does not like to ;;; eat all plants (specifically grain), and therefore must like eating all ;;; animals which like to eat some plant. ;;; But it does not like to eat foxes. ;;; Therefore foxes cannot be animals which like to eat some plant. ;;;=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= ;;; INPUT FILE ;;;=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= (unless (find-package "EPILOG") (load "/home/diamond/u5/epilog/EPILOG4.3/epi/epi")) (in-package #+lucid 'epilog #-lucid epilog) ; "Easy" version -> some => E x ; Harder version could involve quantifier "some" or collections with at least ; one member (tweak '*filter-threshold* 100) (add-lex 'grain 'NOUN :props '(mass)) (trace 'qa-after) (checkpoint 'start) ; Attempt 1 - full forward inferencing (setq time (get-internal-run-time)) ; Wolves, foxes, birds, caterpillars, and snails are animals, ; wolf, fox, bird, caterpillar, snail all exist on the hierarchy under animal ; and there are some of each. (story '(E x (x wolf)) '(E x (x fox)) '(E x (x bird)) '(E x (x caterpillar)) '(E x (x snail)) ) ; Also there are some grains, (story '(E x (x grain))) ; and grains are plants ; also on hierarchy ; Every animal either likes to eat all plants, or all animals much smaller than ; itself that like to eat some plants ; this is where all has been changed to some for consistency ; to use all, the E y and E z would become A y and A z ; If we use A z ... then we get an inconsistency adding that birds like to ; eat caterpillars but not snails (further down). (kn '(A x (x animal) ((A y (y plant) (x like-to-eat y)) or (A z ((z animal) and (z smaller-than x) (E q (q plant) (z like-to-eat q))) (x like-to-eat z)) ))) ; Caterpillers and snails are much smaller than birds, (kn '(A x ((x caterpillar) or (x snail)) (A y (y bird) (x smaller-than y)))) ; which are much smaller than foxes, (kn '(A x (x bird) (A y (y fox) (x smaller-than y)))) ; which in turn are much smaller than wolves. (kn '(A x (x fox) (A y (y wolf) (x smaller-than y)))) ; Wolves do not like to eat foxes or grains, (kn '(A x (x wolf) (A y ((y fox) or (y grain)) (not x like-to-eat y)))) ; while birds like to eat caterpillars (kn '(A x (x bird) (A y (y caterpillar) (x like-to-eat y)))) ; but not snails (kn '(A x (x bird) (A z (z snail) (not x like-to-eat z)))) ; Caterpillars and snails like to eat some plants (kn '(A x ((x snail) or (x caterpillar)) (E y (y plant) (x like-to-eat y)))) ; Therefore there is an animal that likes to eat a grain-eating animal (q '(E x (x animal) (E y ((y animal) and (E z (z grain) (y like-to-eat z))) (x like-to-eat y)))) (print-line "Used " (/ (float (- (get-internal-run-time) time)) internal-time-units-per-second) " seconds CPU time") (retract 'start) ; Attempt 2 - no forward inferencing (setq time (get-internal-run-time)) (tweak '*rule-forward* nil) (tweak '*story-forward* nil) ; Wolves, foxes, birds, caterpillars, and snails are animals, ; wolf, fox, bird, caterpillar, snail all exist on the hierarchy under animal ; and there are some of each. (story '(E x (x wolf)) '(E x (x fox)) '(E x (x bird)) '(E x (x caterpillar)) '(E x (x snail)) ) ; Also there are some grains, (story '(E x (x grain))) ; and grains are plants ; also on hierarchy ; Every animal either likes to eat all plants, or all animals much smaller than ; itself that like to eat some plants ; this is where all has been changed to some for consistency ; to use all, the E y and E z would become A y and A z ; If we use A z ... then we get an inconsistency adding that birds like to ; eat caterpillars but not snails (further down). (kn '(A x (x animal) ((A y (y plant) (x like-to-eat y)) or (A z ((z animal) and (z smaller-than x) (E q (q plant) (z like-to-eat q))) (x like-to-eat z)) ))) ; Caterpillers and snails are much smaller than birds, (kn '(A x ((x caterpillar) or (x snail)) (A y (y bird) (x smaller-than y)))) ; which are much smaller than foxes, (kn '(A x (x bird) (A y (y fox) (x smaller-than y)))) ; which in turn are much smaller than wolves. (kn '(A x (x fox) (A y (y wolf) (x smaller-than y)))) ; Wolves do not like to eat foxes or grains, (kn '(A x (x wolf) (A y ((y fox) or (y grain)) (not x like-to-eat y)))) ; while birds like to eat caterpillars (kn '(A x (x bird) (A y (y caterpillar) (x like-to-eat y)))) ; but not snails (kn '(A x (x bird) (A z (z snail) (not x like-to-eat z)))) ; Caterpillars and snails like to eat some plants (kn '(A x ((x snail) or (x caterpillar)) (E y (y plant) (x like-to-eat y)))) (tweak '*qa-iterations* 400) (tweak '*qa-depth* 16) (trace 'subgoal) ; Therefore there is an animal that likes to eat a grain-eating animal (proof-q '(E x (x animal) (E y ((y animal) and (E z (z grain) (y like-to-eat z))) (x like-to-eat y)))) (print-line "Used " (/ (float (- (get-internal-run-time) time)) internal-time-units-per-second) " seconds CPU time") (q '(c2 like-to-eat c3)) (retract 'start) ; Attempt 3 - full instantiations only in forward inferencing (setq time (get-internal-run-time)) (tweak '*rule-forward* t) (tweak '*story-forward* t) (tweak '*forward-full* t) (tweak '*key-threshold* 0) ; Wolves, foxes, birds, caterpillars, and snails are animals, ; wolf, fox, bird, caterpillar, snail all exist on the hierarchy under animal ; and there are some of each. (story '(E x (x wolf)) '(E x (x fox)) '(E x (x bird)) '(E x (x caterpillar)) '(E x (x snail)) ) ; Also there are some grains, (story '(E x (x grain))) ; and grains are plants ; also on hierarchy ; Every animal either likes to eat all plants, or all animals much smaller than ; itself that like to eat some plants ; this is where all has been changed to some for consistency ; to use all, the E y and E z would become A y and A z ; If we use A z ... then we get an inconsistency adding that birds like to ; eat caterpillars but not snails (further down). (kn '(A x (x animal) ((A y (y plant) (x like-to-eat y)) or (A z ((z animal) and (z smaller-than x) (E q (q plant) (z like-to-eat q))) (x like-to-eat z)) ))) ; Caterpillers and snails are much smaller than birds, (kn '(A x ((x caterpillar) or (x snail)) (A y (y bird) (x smaller-than y)))) ; which are much smaller than foxes, (kn '(A x (x bird) (A y (y fox) (x smaller-than y)))) ; which in turn are much smaller than wolves. (kn '(A x (x fox) (A y (y wolf) (x smaller-than y)))) ; Wolves do not like to eat foxes or grains, (kn '(A x (x wolf) (A y ((y fox) or (y grain)) (not x like-to-eat y)))) ; while birds like to eat caterpillars (kn '(A x (x bird) (A y (y caterpillar) (x like-to-eat y)))) ; but not snails (kn '(A x (x bird) (A z (z snail) (not x like-to-eat z)))) ; Caterpillars and snails like to eat some plants (kn '(A x ((x snail) or (x caterpillar)) (E y (y plant) (x like-to-eat y)))) ; Therefore there is an animal that likes to eat a grain-eating animal (proof-q '(E x (x animal) (E y ((y animal) and (E z (z grain) (y like-to-eat z))) (x like-to-eat y)))) (print-line "Used " (/ (float (- (get-internal-run-time) time)) internal-time-units-per-second) " seconds CPU time") (q '(c2 like-to-eat c3)) ;;;=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= ;;; OUTPUT ;;;=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= ; Loading /usr/staff/lib/cl/siteinit.cl ; Loading sitewide siteinit.cl file. ;;; defined (reset-default-opt) to change optimization settings back to defaults: (declaim (optimize (space 1) (speed 2) (safety 1) (debug 2))) ;; Optimization settings: safety 1, space 1, speed 2, debug 2. ;; For a complete description of all compiler switches given the current ;; optimization settings evaluate (EXPLAIN-COMPILER-SETTINGS). --> Running Cold Initializations --> Running Warm Initializations Initing *random-state* CL-LIB Version: 4.11 Time-stamp: <96/04/17 20:09:03 miller> USER(1): ; Fast loading /home/diamond/u5/epilog/EPILOG4.3/epi/epi.fasl43 ; Fast loading /home/diamond/u5/epilog/EPILOG4.3/epi/EPILOG.fasl43 ****************************************************************** * Welcome to EPILOG: the computational system for Episodic Logic * * * * Last update: August 1993 * ****************************************************************** This version of EPILOG is copyrighted by the University of Alberta. It may be used for academic and instructional purposes, but not for commercial purposes (except by Boeing Company); publication of the source requires written permission from Boeing, for five years following acceptance of this version of EPILOG by Boeing. MEMORY MANAGEMENT ..... LOADING EPILOG ..... ; Fast loading /home/diamond/u5/epilog/EPILOG4.3/epi/epiuser/epiuser.fasl43 ; Fast loading /home/diamond/u5/epilog/EPILOG4.3/epi/story/story.fasl43 ; Fast loading /home/diamond/u5/epilog/EPILOG4.3/epi/lib/lib.fasl43 ; Fast loading ; /home/diamond/u5/epilog/EPILOG4.3/epi/lib/general.fasl43 ; Fast loading /home/diamond/u5/epilog/EPILOG4.3/epi/lib/io.fasl43 ; Fast loading ; /home/diamond/u5/epilog/EPILOG4.3/epi/lib/display.fasl43 ; Fast loading /home/diamond/u5/epilog/EPILOG4.3/epi/lib/help.fasl43 ; Fast loading ; /home/diamond/u5/epilog/EPILOG4.3/epi/lib/rewind.fasl43 ; Fast loading /home/diamond/u5/epilog/EPILOG4.3/epi/lib/hash.fasl43 ; Fast loading /home/diamond/u5/epilog/EPILOG4.3/epi/lib/trace.fasl43 ; Fast loading /home/diamond/u5/epilog/EPILOG4.3/epi/lib/tweak.fasl43 ; Fast loading ; /home/diamond/u5/epilog/EPILOG4.3/epi/epilib/epilib.fasl43 ; Fast loading ; /home/diamond/u5/epilog/EPILOG4.3/epi/epilib/info.fasl43 ; Fast loading ; /home/diamond/u5/epilog/EPILOG4.3/epi/epilib/spec.fasl43 ; Fast loading ; /home/diamond/u5/epilog/EPILOG4.3/epi/epilib/prob.fasl43 ; Fast loading ; /home/diamond/u5/epilog/EPILOG4.3/epi/epilib/pred.fasl43 ; Fast loading ; /home/diamond/u5/epilog/EPILOG4.3/epi/epilib/hier.fasl43 ; Fast loading ; /home/diamond/u5/epilog/EPILOG4.3/epi/epilib/create.fasl43 ; Fast loading ; /home/diamond/u5/epilog/EPILOG4.3/epi/epilib/objects.fasl43 ; Fast loading ; /home/diamond/u5/epilog/EPILOG4.3/epi/epilib/mem.fasl43 ; Fast loading ; /home/diamond/u5/epilog/EPILOG4.3/epi/epilib/subst.fasl43 ; Fast loading ; /home/diamond/u5/epilog/EPILOG4.3/epi/epilib/interest.fasl43 ; Fast loading ; /home/diamond/u5/epilog/EPILOG4.3/epi/epilib/complex.fasl43 ; Fast loading ; /home/diamond/u5/epilog/EPILOG4.3/epi/epilib/class.fasl43 ; Fast loading ; /home/diamond/u5/epilog/EPILOG4.3/epi/epilib/norm.fasl43 ; Fast loading ; /home/diamond/u5/epilog/EPILOG4.3/epi/epilib/ret.fasl43 ; Fast loading ; /home/diamond/u5/epilog/EPILOG4.3/epi/epilib/unify.fasl43 ; Fast loading ; /home/diamond/u5/epilog/EPILOG4.3/epi/epilib/compare.fasl43 ; Fast loading /home/diamond/u5/epilog/EPILOG4.3/epi/spec/spec.fasl43 ; Fast loading ; /home/diamond/u5/epilog/EPILOG4.3/epi/spec/interface.fasl43 ; Fast loading ; /home/diamond/u5/epilog/EPILOG4.3/epi/response/response.fasl43 ; Fast loading ; /home/diamond/u5/epilog/EPILOG4.3/epi/response/defs.fasl43 ; Fast loading ; /home/diamond/u5/epilog/EPILOG4.3/epi/response/lex.fasl43 ; Fast loading ; /home/diamond/u5/epilog/EPILOG4.3/epi/response/filter.fasl43 ; Fast loading ; /home/diamond/u5/epilog/EPILOG4.3/epi/response/organize.fasl43 ; Fast loading ; /home/diamond/u5/epilog/EPILOG4.3/epi/response/general.fasl43 ; Fast loading ; /home/diamond/u5/epilog/EPILOG4.3/epi/response/combine.fasl43 ; Fast loading ; /home/diamond/u5/epilog/EPILOG4.3/epi/response/fragment.fasl43 ; Fast loading ; /home/diamond/u5/epilog/EPILOG4.3/epi/response/build.fasl43 ; Fast loading ; /home/diamond/u5/epilog/EPILOG4.3/epi/response/fill.fasl43 ; Fast loading ; /home/diamond/u5/epilog/EPILOG4.3/epi/response/print.fasl43 ; Fast loading ; /home/diamond/u5/epilog/EPILOG4.3/epi/response/trans.fasl43 ; Fast loading ; /home/diamond/u5/epilog/EPILOG4.3/epi/response/verbalize.fasl43 ; Fast loading ; /home/diamond/u5/epilog/EPILOG4.3/epi/eshell/eshell.fasl43 ; Fast loading ; /home/diamond/u5/epilog/EPILOG4.3/epi/eshell/interp.fasl43 ; Fast loading ; /home/diamond/u5/epilog/EPILOG4.3/epi/eshell/io.fasl43 ; Fast loading ; /home/diamond/u5/epilog/EPILOG4.3/epi/eshell/read.fasl43 ; Fast loading ; /home/diamond/u5/epilog/EPILOG4.3/epi/eshell/cmdhash.fasl43 ; Fast loading ; /home/diamond/u5/epilog/EPILOG4.3/epi/eshell/cmds.fasl43 ; Fast loading /home/diamond/u5/epilog/EPILOG4.3/epi/story/eval.fasl43 ; Fast loading ; /home/diamond/u5/epilog/EPILOG4.3/epi/story/forward.fasl43 ; Fast loading /home/diamond/u5/epilog/EPILOG4.3/epi/story/qa.fasl43 ; Fast loading /home/diamond/u5/epilog/EPILOG4.3/epi/story/enter.fasl43 ; Fast loading ; /home/diamond/u5/epilog/EPILOG4.3/epi/story/subgoal.fasl43 ; Fast loading ; /home/diamond/u5/epilog/EPILOG4.3/epi/story/access.fasl43 ; Fast loading /home/diamond/u5/epilog/EPILOG4.3/epi/story/user.fasl43 ; Fast loading /home/diamond/u5/epilog/EPILOG4.3/epi/epiuser/call.fasl43 ; Fast loading ; /home/diamond/u5/epilog/EPILOG4.3/epi/epiuser/eshell.fasl43 DONE require epiuser DONE require epilog ; Loading /home/diamond/u5/epilog/EPILOG4.3/epi/specialists DONE load specialists ; Fast loading /home/diamond/u5/epilog/EPILOG4.3/epi/type/definition.fasl43 ; Fast loading /home/diamond/u5/epilog/EPILOG4.3/epi/type/type.fasl43 ; Fast loading /home/diamond/u5/epilog/EPILOG4.3/epi/spec/spec.fasl43 ; Fast loading ; /home/diamond/u5/epilog/EPILOG4.3/epi/spec/interface.fasl43 Specialist TYPE-SPECIALIST is now active ; Fast loading ; /home/diamond/u5/epilog/EPILOG4.3/epi/episode/definition.fasl43 ; Fast loading ; /home/diamond/u5/epilog/EPILOG4.3/epi/episode/episode.fasl43 ; Fast loading /home/diamond/u5/epilog/EPILOG4.3/epi/spec/spec.fasl43 ; Fast loading ; /home/diamond/u5/epilog/EPILOG4.3/epi/spec/interface.fasl43 Specialist EPISODE-SPECIALIST is now active ; Fast loading /home/diamond/u5/epilog/EPILOG4.3/epi/hier/definition.fasl43 ; Fast loading /home/diamond/u5/epilog/EPILOG4.3/epi/hier/hier.fasl43 ; Fast loading /home/diamond/u5/epilog/EPILOG4.3/epi/spec/spec.fasl43 ; Fast loading ; /home/diamond/u5/epilog/EPILOG4.3/epi/spec/interface.fasl43 Specialist HIER-SPECIALIST is now active ; Fast loading /home/diamond/u5/epilog/EPILOG4.3/epi/part/definition.fasl43 ; Fast loading /home/diamond/u5/epilog/EPILOG4.3/epi/part/part.fasl43 ; Fast loading /home/diamond/u5/epilog/EPILOG4.3/epi/spec/spec.fasl43 ; Fast loading ; /home/diamond/u5/epilog/EPILOG4.3/epi/spec/interface.fasl43 ; Fast loading /home/diamond/u5/epilog/EPILOG4.3/epi/part/defs.fasl43 ; Fast loading ; /home/diamond/u5/epilog/EPILOG4.3/epi/part/general.fasl43 ; Fast loading /home/diamond/u5/epilog/EPILOG4.3/epi/part/eval.fasl43 ; Fast loading /home/diamond/u5/epilog/EPILOG4.3/epi/part/enter.fasl43 ; Fast loading /home/diamond/u5/epilog/EPILOG4.3/epi/part/print.fasl43 ; Fast loading ; /home/diamond/u5/epilog/EPILOG4.3/epi/part/compare.fasl43 Specialist PART-SPECIALIST is now active ; Fast loading /home/diamond/u5/epilog/EPILOG4.3/epi/meta/definition.fasl43 ; Fast loading /home/diamond/u5/epilog/EPILOG4.3/epi/meta/meta.fasl43 ; Fast loading /home/diamond/u5/epilog/EPILOG4.3/epi/spec/spec.fasl43 ; Fast loading ; /home/diamond/u5/epilog/EPILOG4.3/epi/spec/interface.fasl43 ; Fast loading ; /home/diamond/u5/epilog/EPILOG4.3/epi/meta/functions.fasl43 ; Fast loading /home/diamond/u5/epilog/EPILOG4.3/epi/meta/eval.fasl43 ; Fast loading /home/diamond/u5/epilog/EPILOG4.3/epi/meta/enter.fasl43 Specialist META-SPECIALIST is now active ; Fast loading ; /home/diamond/u5/epilog/EPILOG4.3/epi/other/definition.fasl43 ; Fast loading /home/diamond/u5/epilog/EPILOG4.3/epi/other/other.fasl43 ; Fast loading /home/diamond/u5/epilog/EPILOG4.3/epi/spec/spec.fasl43 ; Fast loading ; /home/diamond/u5/epilog/EPILOG4.3/epi/spec/interface.fasl43 ; Fast loading /home/diamond/u5/epilog/EPILOG4.3/epi/other/eval.fasl43 ; Fast loading /home/diamond/u5/epilog/EPILOG4.3/epi/other/enter.fasl43 Specialist OTHER-SPECIALIST is now active ; Fast loading ; /home/diamond/u5/epilog/EPILOG4.3/epi/equal/definition.fasl43 ; Fast loading /home/diamond/u5/epilog/EPILOG4.3/epi/equal/equal.fasl43 ; Fast loading /home/diamond/u5/epilog/EPILOG4.3/epi/spec/spec.fasl43 ; Fast loading ; /home/diamond/u5/epilog/EPILOG4.3/epi/spec/interface.fasl43 ; Fast loading ; /home/diamond/u5/epilog/EPILOG4.3/epi/set-equal/set-equal.fasl43 ; Fast loading /home/diamond/u5/epilog/EPILOG4.3/epi/spec/spec.fasl43 ; Fast loading ; /home/diamond/u5/epilog/EPILOG4.3/epi/spec/interface.fasl43 ; Fast loading ; /home/diamond/u5/epilog/EPILOG4.3/epi/set-equal/defs.fasl43 ; Fast loading ; /home/diamond/u5/epilog/EPILOG4.3/epi/set-equal/general.fasl43 ; Fast loading ; /home/diamond/u5/epilog/EPILOG4.3/epi/set-equal/enter.fasl43 ; Fast loading ; /home/diamond/u5/epilog/EPILOG4.3/epi/equal/functions.fasl43 ; Fast loading /home/diamond/u5/epilog/EPILOG4.3/epi/equal/eval.fasl43 ; Fast loading /home/diamond/u5/epilog/EPILOG4.3/epi/equal/enter.fasl43 ; Fast loading /home/diamond/u5/epilog/EPILOG4.3/epi/equal/print.fasl43 ; Fast loading ; /home/diamond/u5/epilog/EPILOG4.3/epi/equal/compare.fasl43 Specialist EQUALITY-SPECIALIST is now activeDONE use-spec specialists ; Loading /home/diamond/u5/epilog/EPILOG4.3/epi/epi-hier DONE load epi-hier ; Loading /home/diamond/u5/epilog/EPILOG4.3/epi/epi-indicate DONE load epi-indicate ; Loading /home/diamond/u5/epilog/EPILOG4.3/epi/epi-init.lisp DONE load epi/epi-init.lisp ; Loading ./epi-init.lisp ; Loading ./eg.hier ; Loading ./eg.indicate ; Loading ./eg.parts ; Loading ./eg.trans ; Loading ./eg.lex DONE load epi-init.lisp DONE number-hier DONE loading EPILOG T USER(2): # EPI(3): EPI(3): EPI(3): EPI(3): EPI(3): EPI(3): EPI(3): 100.0 EPI(4): (MASS) EPI(5): NIL EPI(6): EPI(6): NIL EPI(7): EPI(7): EPI(7): 8820 EPI(8): EPI(8): EPI(8): Loading story sentence ... WFF1: (C1 WOLF) Stored in Input Array [0] Probability: 1 There is a wolf. Loading story sentence ... WFF2: (C2 FOX) Stored in Input Array [1] Probability: 1 There is a fox. Loading story sentence ... WFF3: (C3 BIRD) Stored in Input Array [2] Probability: 1 There is a bird. Loading story sentence ... WFF4: (C4 CATERPILLAR) Stored in Input Array [3] Probability: 1 There is a caterpillar. Loading story sentence ... WFF5: (C5 SNAIL) Stored in Input Array [4] Probability: 1 There is a snail. (WFF1 WFF2 WFF3 WFF4 WFF5) EPI(9): EPI(9): Loading story sentence ... WFF6: (C6 GRAIN) Stored in Input Array [5] Probability: 1 There is some grain. (WFF6) EPI(10): EPI(10): EPI(10): Loading knowledge ... WFF20: (A X (X ANIMAL) ((A Y (Y PLANT) (X LIKE-TO-EAT Y)) OR (A Z ((Z ANIMAL) AND (Z SMALLER-THAN X) (E X1 (X1 PLANT) (Z LIKE-TO-EAT X1))) (X LIKE-TO-EAT Z)))) Probability: 1 Animals like to eat plants, or they like to eat other animals smaller than the animals that like to eat other plants. (WFF20) EPI(11): EPI(11): Loading knowledge ... WFF27: (A X ((X SNAIL) OR (X CATERPILLAR)) (A Y (Y BIRD) (X SMALLER-THAN Y))) Probability: 1 ** INFERRED FORMULA ** WFF28: (C4 SMALLER-THAN C3) Rank: 1 Parents: (WFF27 WFF3 WFF4) Probability: 1 ** INFERRED FORMULA ** WFF31: (A X (X BIRD) (C4 SMALLER-THAN X)) Rank: 1 Parents: (WFF27 WFF4) Probability: 1 ** INFERRED FORMULA ** WFF32: (C5 SMALLER-THAN C3) Rank: 1 Parents: (WFF27 WFF3 WFF5) Probability: 1 ** INFERRED FORMULA ** WFF34: (A X (X BIRD) (C5 SMALLER-THAN X)) Rank: 1 Parents: (WFF27 WFF5) Probability: 1 ** INFERRED FORMULA ** WFF37: (A X ((X SNAIL) OR (X CATERPILLAR)) (X SMALLER-THAN C3)) Rank: 1 Parents: (WFF27 WFF3) Probability: 1 Snails or caterpillars are smaller than birds. A caterpillar is smaller than a bird. The caterpillar is smaller than birds. A snail is smaller than the bird. The snail is smaller than birds. Snails or caterpillars are smaller than the bird. (WFF27 WFF28 WFF31 WFF32 WFF34 WFF37) EPI(12): EPI(12): Loading knowledge ... WFF40: (A X (X BIRD) (A Y (Y FOX) (X SMALLER-THAN Y))) Probability: 1 ** INFERRED FORMULA ** WFF41: (C3 SMALLER-THAN C2) Rank: 1 Parents: (WFF40 WFF2 WFF3) Probability: 1 ** INFERRED FORMULA ** WFF44: (A X (X FOX) (C3 SMALLER-THAN X)) Rank: 1 Parents: (WFF40 WFF3) Probability: 1 ** INFERRED FORMULA ** WFF46: (A X (X BIRD) (X SMALLER-THAN C2)) Rank: 1 Parents: (WFF40 WFF2) Probability: 1 Birds are smaller than foxes. A bird is smaller than a fox. The bird is smaller than foxes. Birds are smaller than the fox. (WFF40 WFF41 WFF44 WFF46) EPI(13): EPI(13): Loading knowledge ... WFF49: (A X (X FOX) (A Y (Y WOLF) (X SMALLER-THAN Y))) Probability: 1 ** INFERRED FORMULA ** WFF50: (C2 SMALLER-THAN C1) Rank: 1 Parents: (WFF49 WFF1 WFF2) Probability: 1 ** INFERRED FORMULA ** WFF53: (A X (X WOLF) (C2 SMALLER-THAN X)) Rank: 1 Parents: (WFF49 WFF2) Probability: 1 ** INFERRED FORMULA ** WFF55: (A X (X FOX) (X SMALLER-THAN C1)) Rank: 1 Parents: (WFF49 WFF1) Probability: 1 Foxes are smaller than wolves. A fox is smaller than a wolf. The fox is smaller than wolves. Foxes are smaller than the wolf. (WFF49 WFF50 WFF53 WFF55) EPI(14): EPI(14): Loading knowledge ... WFF60: (A X (X WOLF) (A Y ((Y GRAIN) OR (Y FOX)) (NOT X LIKE-TO-EAT Y))) Probability: 1 ** INFERRED FORMULA ** WFF61: (NOT C1 LIKE-TO-EAT C6) Rank: 1 Parents: (WFF60 WFF6 WFF1) Probability: 1 ** INFERRED FORMULA ** WFF79: (NOT C1 LIKE-TO-EAT C2) Rank: 1 Parents: (WFF60 WFF2 WFF1) Probability: 1 ** INFERRED FORMULA ** WFF87: ((A X (X PLANT) (C1 LIKE-TO-EAT X)) OR (A Y1 (Y1 PLANT) (NOT C2 LIKE-TO-EAT Y1))) Rank: 2 Parents: (WFF20 WFF2 WFF1 WFF50 WFF79) Probability: 1 ** INFERRED FORMULA ** WFF91: (A X (X PLANT) (NOT C2 LIKE-TO-EAT X)) Rank: 3 Parents: (WFF6 WFF61 WFF87) Probability: 1 ** INFERRED FORMULA ** WFF96: (NOT C2 LIKE-TO-EAT C6) Rank: 1 Parents: (WFF91 WFF6) Probability: 1 ** INFERRED FORMULA ** WFF103: (A X ((X GRAIN) OR (X FOX)) (NOT C1 LIKE-TO-EAT X)) Rank: 1 Parents: (WFF60 WFF1) Probability: 1 ** INFERRED FORMULA ** WFF105: (A X (X WOLF) (NOT X LIKE-TO-EAT C2)) Rank: 1 Parents: (WFF60 WFF2) Probability: 1 ** INFERRED FORMULA ** WFF107: (A X (X WOLF) (NOT X LIKE-TO-EAT C6)) Rank: 1 Parents: (WFF60 WFF6) Probability: 1 No wolf likes to eat grain or any foxes. A wolf doesn't like to eat some grain. The wolf doesn't like to eat a fox. The wolf likes to eat plants, or the fox doesn't like to eat a plant. The fox doesn't like to eat a plant. The fox doesn't like to eat the grain. The wolf doesn't like to eat grain or any foxes. No wolf likes to eat the fox. No wolf likes to eat the grain. (WFF60 WFF61 WFF79 WFF87 WFF91 WFF96 WFF103 WFF105 WFF107) EPI(15): EPI(15): Loading knowledge ... WFF110: (A X (X BIRD) (A Y (Y CATERPILLAR) (X LIKE-TO-EAT Y))) Probability: 1 ** INFERRED FORMULA ** WFF111: (C3 LIKE-TO-EAT C4) Rank: 1 Parents: (WFF110 WFF4 WFF3) Probability: 1 ** INFERRED FORMULA ** WFF116: (A X (X CATERPILLAR) (C3 LIKE-TO-EAT X)) Rank: 1 Parents: (WFF110 WFF3) Probability: 1 ** INFERRED FORMULA ** WFF118: (A X (X BIRD) (X LIKE-TO-EAT C4)) Rank: 1 Parents: (WFF110 WFF4) Probability: 1 Birds like to eat caterpillars. A bird likes to eat a caterpillar. The bird likes to eat caterpillars. Birds like to eat the caterpillar. (WFF110 WFF111 WFF116 WFF118) EPI(16): EPI(16): Loading knowledge ... WFF121: (A X (X BIRD) (A Y (Y SNAIL) (NOT X LIKE-TO-EAT Y))) Probability: 1 ** INFERRED FORMULA ** WFF122: (NOT C3 LIKE-TO-EAT C5) Rank: 1 Parents: (WFF121 WFF5 WFF3) Probability: 1 ** INFERRED FORMULA ** WFF132: ((A X (X PLANT) (C3 LIKE-TO-EAT X)) OR (A Y1 (Y1 PLANT) (NOT C5 LIKE-TO-EAT Y1))) Rank: 2 Parents: (WFF20 WFF5 WFF3 WFF32 WFF122) Probability: 1 ** INFERRED FORMULA ** WFF147: (A X (X SNAIL) (NOT C3 LIKE-TO-EAT X)) Rank: 1 Parents: (WFF121 WFF3) Probability: 1 ** INFERRED FORMULA ** WFF149: (A X (X BIRD) (NOT X LIKE-TO-EAT C5)) Rank: 1 Parents: (WFF121 WFF5) Probability: 1 No bird likes to eat a snail. A bird doesn't like to eat a snail. The bird likes to eat plants, or the snail doesn't like to eat a plant. The bird doesn't like to eat a snail. No bird likes to eat the snail. (WFF121 WFF122 WFF132 WFF147 WFF149) EPI(17): EPI(17): Loading knowledge ... WFF153: (A X ((X SNAIL) OR (X CATERPILLAR)) (E U (U PLANT) (X LIKE-TO-EAT U))) Probability: 1 ** INFERRED FORMULA ** WFF156: (C7 PLANT) Rank: 1 Parents: (WFF153 WFF5) Probability: 1 ** INFERRED FORMULA ** WFF157: (NOT C2 LIKE-TO-EAT C7) Rank: 2 Parents: (WFF91 WFF156) Probability: 1 ** INFERRED FORMULA ** WFF170: ((C3 LIKE-TO-EAT C7) OR (NOT C5 LIKE-TO-EAT C7)) Rank: 2 Parents: (WFF132 WFF156) Probability: 1 ** INFERRED FORMULA ** WFF172: ((NOT C5 LIKE-TO-EAT C7) OR (A X (X PLANT) (C3 LIKE-TO-EAT X))) Rank: 2 Parents: (WFF132 WFF156) Probability: 1 ** INFERRED FORMULA ** WFF173: ((C3 LIKE-TO-EAT C7) OR (A X (X PLANT) (NOT C5 LIKE-TO-EAT X))) Rank: 2 Parents: (WFF132 WFF156) Probability: 1 ** INFERRED FORMULA ** WFF175: ((C1 LIKE-TO-EAT C7) OR (A X (X PLANT) (NOT C2 LIKE-TO-EAT X))) Rank: 2 Parents: (WFF87 WFF156) Probability: 1 ** INFERRED FORMULA ** WFF176: (C5 LIKE-TO-EAT C7) Rank: 1 Parents: (WFF153 WFF5) Probability: 1 ** INFERRED FORMULA ** WFF168: (C3 LIKE-TO-EAT C7) Rank: 2 Parents: (WFF170 WFF176) Probability: 1 ** INFERRED FORMULA ** WFF177: ((C2 LIKE-TO-EAT C3) OR (A X (X PLANT) (C2 LIKE-TO-EAT X))) Rank: 3 Parents: (WFF20 WFF156 WFF3 WFF2 WFF41 WFF168) Probability: 1 ** INFERRED FORMULA ** WFF112: (C2 LIKE-TO-EAT C3) Rank: 4 Parents: (WFF156 WFF157 WFF177) Probability: 1 %% Inferred formula WFF180: ((NOT C6 PLANT) OR (C2 LIKE-TO-EAT C3)) already true NOT LOADed! ** INFERRED FORMULA ** WFF183: (A X (X ANIMAL) ((A Y (Y PLANT) (X LIKE-TO-EAT Y)) OR ((C3 SMALLER-THAN X) IMPLIES (X LIKE-TO-EAT C3)))) Rank: 3 Parents: (WFF20 WFF156 WFF3 WFF168) Probability: 1 ** INFERRED FORMULA ** WFF127: (A X (X PLANT) (C3 LIKE-TO-EAT X)) Rank: 2 Parents: (WFF32 WFF20 WFF156 WFF5 WFF3 WFF122 WFF176) Probability: 1 ** INFERRED FORMULA ** WFF191: (C3 LIKE-TO-EAT C6) Rank: 1 Parents: (WFF127 WFF6) Probability: 1 ** INFERRED FORMULA ** WFF195: (A X (X ANIMAL) ((A Y (Y PLANT) (X LIKE-TO-EAT Y)) OR ((C5 SMALLER-THAN X) IMPLIES (X LIKE-TO-EAT C5)))) Rank: 2 Parents: (WFF20 WFF156 WFF5 WFF176) Probability: 1 ** INFERRED FORMULA ** WFF204: (C8 PLANT) Rank: 1 Parents: (WFF153 WFF4) Probability: 1 ** INFERRED FORMULA ** WFF205: (C3 LIKE-TO-EAT C8) Rank: 2 Parents: (WFF127 WFF204) Probability: 1 ** INFERRED FORMULA ** WFF206: (NOT C2 LIKE-TO-EAT C8) Rank: 2 Parents: (WFF91 WFF204) Probability: 1 ** INFERRED FORMULA ** WFF214: ((NOT C5 LIKE-TO-EAT C8) OR (A X (X PLANT) (C3 LIKE-TO-EAT X))) Rank: 2 Parents: (WFF132 WFF204) Probability: 1 ** INFERRED FORMULA ** WFF219: ((C1 LIKE-TO-EAT C8) OR (A X (X PLANT) (NOT C2 LIKE-TO-EAT X))) Rank: 2 Parents: (WFF87 WFF204) Probability: 1 ** INFERRED FORMULA ** WFF220: (C4 LIKE-TO-EAT C8) Rank: 1 Parents: (WFF153 WFF4) Probability: 1 ** INFERRED FORMULA ** WFF223: (A X (X ANIMAL) ((A Y (Y PLANT) (X LIKE-TO-EAT Y)) OR ((C4 SMALLER-THAN X) IMPLIES (X LIKE-TO-EAT C4)))) Rank: 2 Parents: (WFF20 WFF204 WFF4 WFF220) Probability: 1 Snails or caterpillars like to eat plants. A snail likes to eat a plant. A fox doesn't like to eat the plant. A bird likes to eat the plant, or the snail doesn't like to eat the plant. The snail doesn't like to eat the plant, or the bird likes to eat a plant. The bird likes to eat the plant, or the snail doesn't like to eat a plant. A wolf likes to eat the plant, or the fox doesn't like to eat a plant. The bird likes to eat the plant. The fox likes to eat the bird, or it likes to eat plants. The fox likes to eat the bird. Animals like to eat plants, or they like to eat the bird. The bird likes to eat plants. The bird likes to eat some grain. Animals like to eat plants, or they like to eat the snail. A caterpillar likes to eat a plant. The bird likes to eat the plant. The fox doesn't like to eat the plant. The snail doesn't like to eat the plant, or the bird likes to eat a plant. The wolf likes to eat the plant, or the fox doesn't like to eat a plant. Animals like to eat plants, or they like to eat the caterpillar. (WFF153 WFF156 WFF157 WFF170 WFF172 WFF173 WFF175 WFF176 WFF168 WFF177 WFF112 WFF183 WFF127 WFF191 WFF195 WFF204 WFF205 WFF206 WFF214 WFF219 WFF220 WFF223) EPI(18): EPI(18): Questioning (E U (U ANIMAL) (E V ((V ANIMAL) AND (E W (W GRAIN) (V LIKE-TO-EAT W))) (U LIKE-TO-EAT V))) Answer: YES with probability 1 Yes, a fox likes to eat a bird that likes to eat some grain. Used 0.14 seconds CPU time 0.143 seconds real time Used 8 iterations Searched to depth 2 ------------------------------ PROOF subgoal to prove: (E X (X ANIMAL) (E Y ((Y ANIMAL) AND (E Z (Z GRAIN) (Y LIKE-TO-EAT Z))) (X LIKE-TO-EAT Y))) Depth: 0 solved and helpful Interest: 10.0 Inherited Interest: 0.0 Probability: 1 1 Subgoals - need to solve 1 subgoals ------------------------------ PROOF subgoal to prove: (E X (X GRAIN) (C3 LIKE-TO-EAT X)) Depth: 1 solved and helpful Interest: 4465.95 Inherited Interest: 0.0 Probability: 1 (1 WFF1 WFF60 WFF49 WFF6 WFF2 WFF40 PROB1 WFF156 WFF20 WFF27 WFF121 WFF5 WFF3) Wff(s) used: WFF112: (C2 LIKE-TO-EAT C3) WFF3: (C3 BIRD) WFF2: (C2 FOX) Subgoals - need to solve 2 subgoals - combine with OR ------------------------------ PROOF subgoal terminated with YES Depth: 2 solved and helpful Interest: 0 Inherited Interest: 4455.95 Probability: 1 (1 WFF6 WFF27 WFF20 PROB1 WFF121 WFF5 WFF3) Wff(s) used: WFF6: (C6 GRAIN) WFF191: (C3 LIKE-TO-EAT C6) ((YES (WFF2 WFF3 WFF112 WFF6 WFF191) (1 WFF3 WFF5 WFF121 WFF27 WFF20 WFF156 PROB1 WFF40 WFF2 WFF6 WFF49 WFF60 WFF1))) EPI(19): Used 5.39 seconds CPU time NIL EPI(20): Retracting past the named checkpoint QUESTION NIL EPI(21): EPI(21): EPI(21): 14500 EPI(22): EPI(22): NIL EPI(23): NIL EPI(24): EPI(24): EPI(24): Loading story sentence ... WFF1: (C1 WOLF) Stored in Input Array [0] Probability: 1 There is a wolf. Loading story sentence ... WFF2: (C2 FOX) Stored in Input Array [1] Probability: 1 There is a fox. Loading story sentence ... WFF3: (C3 BIRD) Stored in Input Array [2] Probability: 1 There is a bird. Loading story sentence ... WFF4: (C4 CATERPILLAR) Stored in Input Array [3] Probability: 1 There is a caterpillar. Loading story sentence ... WFF5: (C5 SNAIL) Stored in Input Array [4] Probability: 1 There is a snail. (WFF1 WFF2 WFF3 WFF4 WFF5) EPI(25): EPI(25): Loading story sentence ... WFF6: (C6 GRAIN) Stored in Input Array [5] Probability: 1 There is some grain. (WFF6) EPI(26): EPI(26): EPI(26): Loading knowledge ... WFF20: (A X (X ANIMAL) ((A Y (Y PLANT) (X LIKE-TO-EAT Y)) OR (A Z ((Z ANIMAL) AND (Z SMALLER-THAN X) (E X1 (X1 PLANT) (Z LIKE-TO-EAT X1))) (X LIKE-TO-EAT Z)))) Probability: 1 Animals like to eat plants, or they like to eat other animals smaller than the animals that like to eat other plants. (WFF20) EPI(27): EPI(27): Loading knowledge ... WFF27: (A X ((X SNAIL) OR (X CATERPILLAR)) (A Y (Y BIRD) (X SMALLER-THAN Y))) Probability: 1 Snails or caterpillars are smaller than birds. (WFF27) EPI(28): EPI(28): Loading knowledge ... WFF31: (A X (X BIRD) (A Y (Y FOX) (X SMALLER-THAN Y))) Probability: 1 Birds are smaller than foxes. (WFF31) EPI(29): EPI(29): Loading knowledge ... WFF35: (A X (X FOX) (A Y (Y WOLF) (X SMALLER-THAN Y))) Probability: 1 Foxes are smaller than wolves. (WFF35) EPI(30): EPI(30): Loading knowledge ... WFF41: (A X (X WOLF) (A Y ((Y GRAIN) OR (Y FOX)) (NOT X LIKE-TO-EAT Y))) Probability: 1 No wolf likes to eat grain or any foxes. (WFF41) EPI(31): EPI(31): Loading knowledge ... WFF44: (A X (X BIRD) (A Y (Y CATERPILLAR) (X LIKE-TO-EAT Y))) Probability: 1 Birds like to eat caterpillars. (WFF44) EPI(32): EPI(32): Loading knowledge ... WFF47: (A X (X BIRD) (A Y (Y SNAIL) (NOT X LIKE-TO-EAT Y))) Probability: 1 No bird likes to eat a snail. (WFF47) EPI(33): EPI(33): Loading knowledge ... WFF51: (A X ((X SNAIL) OR (X CATERPILLAR)) (E U (U PLANT) (X LIKE-TO-EAT U))) Probability: 1 Snails or caterpillars like to eat plants. (WFF51) EPI(34): EPI(34): 400 EPI(35): 16 EPI(36): NIL EPI(37): EPI(37): Questioning (E U (U ANIMAL) (E V ((V ANIMAL) AND (E W (W GRAIN) (V LIKE-TO-EAT W))) (U LIKE-TO-EAT V))) Adding PROOF subgoal to prove: (E X (X ANIMAL) (E Y ((Y ANIMAL) AND (E Z (Z GRAIN) (Y LIKE-TO-EAT Z))) (X LIKE-TO-EAT Y))) Adding PROOF subgoal to prove: (E X (X ANIMAL) (E Y ((Y ANIMAL) AND (E Z (Z GRAIN) (Y LIKE-TO-EAT Z))) ((X BIRD) AND (Y CATERPILLAR)))) Adding PROOF subgoal to prove: (E X ((X ANIMAL) AND (E Z (Z GRAIN) (X LIKE-TO-EAT Z))) (X CATERPILLAR)) Looking for inferences with (A X ((X SNAIL) OR (X CATERPILLAR)) (E U (U PLANT) (X LIKE-TO-EAT U))) Adding PROOF subgoal to prove: (E X ((X ANIMAL) AND (E Y (Y GRAIN) (X LIKE-TO-EAT Y))) (X CATERPILLAR)) Adding PROOF subgoal to prove: (C8 GRAIN) Adding PROOF subgoal to prove: (E X ((X ANIMAL) AND (E Y (Y GRAIN) ((Y PLANT) AND (X ANIMAL) (E Z ((Z ANIMAL) AND (Z SMALLER-THAN X) (E X1 (X1 PLANT) (Z LIKE-TO-EAT X1))) (NOT X LIKE-TO-EAT Z))))) (X CATERPILLAR)) Adding PROOF subgoal to prove: (E X ((X ANIMAL) AND (E Y (Y GRAIN) ((Y PLANT) AND (X ANIMAL) (C4 SMALLER-THAN X) (NOT X LIKE-TO-EAT C4)))) (X CATERPILLAR)) Adding PROOF subgoal to prove: (E X ((X ANIMAL) AND (C4 SMALLER-THAN X) (NOT X LIKE-TO-EAT C4)) (X CATERPILLAR)) Adding PROOF subgoal to prove: (E X ((C8 GRAIN) AND (X ANIMAL) (C4 SMALLER-THAN X) (NOT X LIKE-TO-EAT C4)) (X CATERPILLAR)) Adding PROOF subgoal to prove: (E X ((C7 GRAIN) AND (X ANIMAL) (C4 SMALLER-THAN X) (NOT X LIKE-TO-EAT C4)) (X CATERPILLAR)) Adding PROOF subgoal to prove: (E X ((X ANIMAL) AND (E Y ((Y ANIMAL) AND (Y SMALLER-THAN X) (E X1 (X1 PLANT) (Y LIKE-TO-EAT X1))) (NOT X LIKE-TO-EAT Y))) (X CATERPILLAR)) Adding PROOF subgoal to prove: (E X ((X ANIMAL) AND (C5 SMALLER-THAN X) (NOT X LIKE-TO-EAT C5)) (X CATERPILLAR)) Adding PROOF subgoal to prove: (E X ((X ANIMAL) AND (E Y (Y GRAIN) ((Y PLANT) AND (X ANIMAL) (C5 SMALLER-THAN X) (NOT X LIKE-TO-EAT C5)))) (X CATERPILLAR)) Adding PROOF subgoal to prove: (E X ((C8 GRAIN) AND (X ANIMAL) (C5 SMALLER-THAN X) (NOT X LIKE-TO-EAT C5)) (X CATERPILLAR)) Adding PROOF subgoal to prove: (E X ((C7 GRAIN) AND (X ANIMAL) (C5 SMALLER-THAN X) (NOT X LIKE-TO-EAT C5)) (X CATERPILLAR)) Adding PROOF subgoal to prove: (E X ((C8 GRAIN) AND (X ANIMAL) (E Y ((Y ANIMAL) AND (Y SMALLER-THAN X) (E X1 (X1 PLANT) (Y LIKE-TO-EAT X1))) (NOT X LIKE-TO-EAT Y))) (X CATERPILLAR)) Adding PROOF subgoal to prove: (E X ((C7 GRAIN) AND (X ANIMAL) (E Y ((Y ANIMAL) AND (Y SMALLER-THAN X) (E X1 (X1 PLANT) (Y LIKE-TO-EAT X1))) (NOT X LIKE-TO-EAT Y))) (X CATERPILLAR)) Adding PROOF subgoal to prove: (E X ((X ANIMAL) AND (X BIRD) (C5 SMALLER-THAN X)) (X CATERPILLAR)) Adding PROOF subgoal to prove: (E X ((X ANIMAL) AND (X BIRD)) (X CATERPILLAR)) Adding PROOF subgoal to prove: (E X ((C8 GRAIN) AND (X ANIMAL) (X BIRD) (C5 SMALLER-THAN X)) (X CATERPILLAR)) Adding PROOF subgoal to prove: (E X ((C8 GRAIN) AND (X ANIMAL) (X BIRD)) (X CATERPILLAR)) Adding PROOF subgoal to prove: (E X ((C7 GRAIN) AND (X ANIMAL) (X BIRD) (C5 SMALLER-THAN X)) (X CATERPILLAR)) Adding PROOF subgoal to prove: (E X ((C7 GRAIN) AND (X ANIMAL) (X BIRD)) (X CATERPILLAR)) Adding PROOF subgoal to prove: (E X ((X ANIMAL) AND (E Y ((Y ANIMAL) AND (Y SMALLER-THAN X) (E Z (Z PLANT) (Y LIKE-TO-EAT Z))) ((Y SNAIL) AND (X BIRD)))) (X CATERPILLAR)) Looking for inferences with (A X ((X SNAIL) OR (X CATERPILLAR)) (E U (U PLANT) (X LIKE-TO-EAT U))) Adding PROOF subgoal to prove: (E X ((X ANIMAL) AND (E Y ((Y ANIMAL) AND (Y SMALLER-THAN X) (E Z (Z PLANT) (Y LIKE-TO-EAT Z))) ((Y SNAIL) AND (X BIRD)))) (X CATERPILLAR)) Adding PROOF subgoal to prove: (E X ((X ANIMAL) AND (E Y ((Y ANIMAL) AND (Y SMALLER-THAN X) (E Z (Z PLANT) ((Z PLANT) AND (Y ANIMAL) (E X1 ((X1 ANIMAL) AND (X1 SMALLER-THAN Y) (E Y1 (Y1 PLANT) (X1 LIKE-TO-EAT Y1))) (NOT Y LIKE-TO-EAT X1))))) ((Y SNAIL) AND (X BIRD)))) (X CATERPILLAR)) Adding PROOF subgoal to prove: (E X ((X ANIMAL) AND (E Y ((Y ANIMAL) AND (Y SMALLER-THAN X) (E Z (Z PLANT) ((Z PLANT) AND (Y ANIMAL) (C5 SMALLER-THAN Y) (NOT Y LIKE-TO-EAT C5)))) ((Y SNAIL) AND (X BIRD)))) (X CATERPILLAR)) Adding PROOF subgoal to prove: (E X ((X ANIMAL) AND (E Y ((Y ANIMAL) AND (Y SMALLER-THAN X) (E Z ((Z ANIMAL) AND (Z SMALLER-THAN Y) (E Y1 (Y1 PLANT) (Z LIKE-TO-EAT Y1))) (NOT Y LIKE-TO-EAT Z))) ((Y SNAIL) AND (X BIRD)))) (X CATERPILLAR)) Adding PROOF subgoal to prove: (E X ((X ANIMAL) AND (E Y ((Y ANIMAL) AND (Y SMALLER-THAN X) (E Z (Z PLANT) ((Z PLANT) AND (Y ANIMAL) (C4 SMALLER-THAN Y) (NOT Y LIKE-TO-EAT C4)))) ((Y SNAIL) AND (X BIRD)))) (X CATERPILLAR)) Adding PROOF subgoal to prove: (E X ((X ANIMAL) AND (E Y ((Y ANIMAL) AND (Y SMALLER-THAN X) (C5 SMALLER-THAN Y) (NOT Y LIKE-TO-EAT C5)) ((Y SNAIL) AND (X BIRD)))) (X CATERPILLAR)) Adding PROOF subgoal to prove: (E X ((X ANIMAL) AND (E Y ((Y ANIMAL) AND (Y SMALLER-THAN X) (C4 SMALLER-THAN Y) (NOT Y LIKE-TO-EAT C4)) ((Y SNAIL) AND (X BIRD)))) (X CATERPILLAR)) Adding PROOF subgoal to prove: (E X ((X ANIMAL) AND (E Y ((Y ANIMAL) AND (Y SMALLER-THAN X) (E Z (Z PLANT) ((Z PLANT) AND (Y ANIMAL) (E X1 ((X1 ANIMAL) AND (X1 SMALLER-THAN Y) (E Y1 (Y1 PLANT) (X1 LIKE-TO-EAT Y1))) ((Y WOLF) AND ((X1 GRAIN) OR (X1 FOX))))))) ((Y SNAIL) AND (X BIRD)))) (X CATERPILLAR)) Adding PROOF subgoal to prove: (E X ((X ANIMAL) AND (E Y ((Y ANIMAL) AND (Y SMALLER-THAN X) (E Z ((Z ANIMAL) AND (Z SMALLER-THAN Y) (E Y1 (Y1 PLANT) (Z LIKE-TO-EAT Y1))) ((Y WOLF) AND ((Z GRAIN) OR (Z FOX))))) ((Y SNAIL) AND (X BIRD)))) (X CATERPILLAR)) Maximum number of iterations (400) reached. Use (q) to continue. Answer: UNKNOWN Used 3.83 seconds CPU time 3.836 seconds real time Used 400 iterations NIL EPI(38): Used 4.81 seconds CPU time NIL EPI(39): EPI(39): Questioning (C2 LIKE-TO-EAT C3) Adding PROOF subgoal to prove: (C2 LIKE-TO-EAT C3) Adding DISPROOF subgoal to prove: (NOT C2 LIKE-TO-EAT C3) Adding PROOF subgoal to prove: ((C3 SMALLER-THAN C2) AND (E X (X PLANT) (NOT C2 LIKE-TO-EAT X)) (E Z (Z PLANT) (C3 LIKE-TO-EAT Z))) Splitting subgoal ((C3 SMALLER-THAN C2) AND (E X (X PLANT) (NOT C2 LIKE-TO-EAT X)) (E Z (Z PLANT) (C3 LIKE-TO-EAT Z))) into ANDed subgoals Adding PROOF subgoal to prove: (C3 SMALLER-THAN C2) Adding PROOF subgoal to prove: (E X (X PLANT) (NOT C2 LIKE-TO-EAT X)) Adding PROOF subgoal to prove: (E X (X PLANT) (C3 LIKE-TO-EAT X)) Answer YES for (C3 SMALLER-THAN C2) Instantiating (A X ((X SNAIL) OR (X CATERPILLAR)) (E U (U PLANT) (X LIKE-TO-EAT U))) with substitutions ((X by C3 1)) Adding PROOF subgoal to prove: (E X (X PLANT) ((X PLANT) AND (E Y ((Y ANIMAL) AND (Y SMALLER-THAN C3) (E Z (Z PLANT) (Y LIKE-TO-EAT Z))) (NOT C3 LIKE-TO-EAT Y)))) Adding PROOF subgoal to prove: (E X ((X ANIMAL) AND (X SMALLER-THAN C3) (E Z (Z PLANT) (X LIKE-TO-EAT Z))) (NOT C3 LIKE-TO-EAT X)) Looking for inferences with (A X ((X SNAIL) OR (X CATERPILLAR)) (E U (U PLANT) (X LIKE-TO-EAT U))) Adding PROOF subgoal to prove: (E X ((X ANIMAL) AND (X SMALLER-THAN C3) (E Y (Y PLANT) (X LIKE-TO-EAT Y))) (NOT C3 LIKE-TO-EAT X)) Adding PROOF subgoal to prove: ((C4 SMALLER-THAN C3) AND (NOT C3 LIKE-TO-EAT C4)) Splitting subgoal ((C4 SMALLER-THAN C3) AND (NOT C3 LIKE-TO-EAT C4)) into ANDed subgoals Adding PROOF subgoal to prove: (C4 SMALLER-THAN C3) Adding PROOF subgoal to prove: (NOT C3 LIKE-TO-EAT C4) Answer YES for (C4 SMALLER-THAN C3) Adding PROOF subgoal to prove: ((C5 SMALLER-THAN C3) AND (NOT C3 LIKE-TO-EAT C5)) Splitting subgoal ((C5 SMALLER-THAN C3) AND (NOT C3 LIKE-TO-EAT C5)) into ANDed subgoals Adding PROOF subgoal to prove: (C5 SMALLER-THAN C3) Adding PROOF subgoal to prove: (NOT C3 LIKE-TO-EAT C5) Answer YES for (C5 SMALLER-THAN C3) Answer YES for (NOT C3 LIKE-TO-EAT C5) Answer YES for ((C5 SMALLER-THAN C3) AND (NOT C3 LIKE-TO-EAT C5)) Answer YES for (E X ((X ANIMAL) AND (X SMALLER-THAN C3) (E Y (Y PLANT) (X LIKE-TO-EAT Y))) (NOT C3 LIKE-TO-EAT X)) Answer YES for (E X ((X ANIMAL) AND (X SMALLER-THAN C3) (E Z (Z PLANT) (X LIKE-TO-EAT Z))) (NOT C3 LIKE-TO-EAT X)) Answer YES for (E X (X PLANT) ((X PLANT) AND (E Y ((Y ANIMAL) AND (Y SMALLER-THAN C3) (E Z (Z PLANT) (Y LIKE-TO-EAT Z))) (NOT C3 LIKE-TO-EAT Y)))) Answer YES for (E X (X PLANT) (C3 LIKE-TO-EAT X)) Adding PROOF subgoal to prove: (E X (X PLANT) (E Y (Y ANIMAL) ((X PLANT) AND (E Z (Z PLANT) (NOT Y LIKE-TO-EAT Z)) (C2 SMALLER-THAN Y) (NOT Y LIKE-TO-EAT C2)))) Adding PROOF subgoal to prove: (E X (X ANIMAL) ((E Z (Z PLANT) (NOT X LIKE-TO-EAT Z)) AND (C2 SMALLER-THAN X) (NOT X LIKE-TO-EAT C2))) Adding PROOF subgoal to prove: (E X (X ANIMAL) ((E Y (Y PLANT) ((X WOLF) AND ((Y GRAIN) OR (Y FOX)))) AND (C2 SMALLER-THAN X) (NOT X LIKE-TO-EAT C2))) Adding PROOF subgoal to prove: (E X (X ANIMAL) ((X WOLF) AND (C2 SMALLER-THAN X) (NOT X LIKE-TO-EAT C2))) Adding PROOF subgoal to prove: (E X (X ANIMAL) ((X WOLF) AND (C2 SMALLER-THAN X))) Adding PROOF subgoal to prove: (E X (X ANIMAL) (X WOLF)) Answer YES for (E X (X ANIMAL) (X WOLF)) Answer YES for (E X (X ANIMAL) ((X WOLF) AND (C2 SMALLER-THAN X))) Answer YES for (E X (X ANIMAL) ((X WOLF) AND (C2 SMALLER-THAN X) (NOT X LIKE-TO-EAT C2))) Answer YES for (E X (X ANIMAL) ((E Y (Y PLANT) ((X WOLF) AND ((Y GRAIN) OR (Y FOX)))) AND (C2 SMALLER-THAN X) (NOT X LIKE-TO-EAT C2))) Answer YES for (E X (X ANIMAL) ((E Z (Z PLANT) (NOT X LIKE-TO-EAT Z)) AND (C2 SMALLER-THAN X) (NOT X LIKE-TO-EAT C2))) Answer YES for (E X (X PLANT) (E Y (Y ANIMAL) ((X PLANT) AND (E Z (Z PLANT) (NOT Y LIKE-TO-EAT Z)) (C2 SMALLER-THAN Y) (NOT Y LIKE-TO-EAT C2)))) Answer YES for (E X (X PLANT) (NOT C2 LIKE-TO-EAT X)) Answer YES for ((C3 SMALLER-THAN C2) AND (E X (X PLANT) (NOT C2 LIKE-TO-EAT X)) (E Z (Z PLANT) (C3 LIKE-TO-EAT Z))) Answer YES for (C2 LIKE-TO-EAT C3) Answer: YES with probability 1 Yes, there is a fox. There is a wolf. There is some grain. There is a bird. There is a snail. Foxes are smaller than wolves. No wolf likes to eat grain or any foxes. Birds are smaller than foxes. Animals like to eat plants, or they like to eat other animals smaller than the animals that like to eat other plants. Snails or caterpillars like to eat plants. Snails or caterpillars are smaller than birds. No bird likes to eat a snail. Used 1.03 seconds CPU time 1.043 seconds real time Used 106 iterations Searched to depth 9 ------------------------------ PROOF subgoal to prove: (C2 LIKE-TO-EAT C3) Depth: 0 solved and helpful Interest: 10.0 Inherited Interest: 0.0 Probability: 1 1 Subgoals - need to solve 1 subgoals ------------------------------ PROOF subgoal to prove: ((C3 SMALLER-THAN C2) AND (E X (X PLANT) (NOT C2 LIKE-TO-EAT X)) (E Z (Z PLANT) (C3 LIKE-TO-EAT Z))) Depth: 1 solved and helpful Interest: 10.0 Inherited Interest: 0.0 Probability: 1 (1 WFF20 WFF3 WFF2) Wff(s) used: WFF20: (A X (X ANIMAL) ((A Y (Y PLANT) (X LIKE-TO-EAT Y)) OR (A Z ((Z ANIMAL) AND (Z SMALLER-THAN X) (E X1 (X1 PLANT) (Z LIKE-TO-EAT X1))) (X LIKE-TO-EAT Z)))) WFF3: (C3 BIRD) WFF2: (C2 FOX) Subgoals - need to solve 3 subgoals - combine with AND ------------------------------ PROOF subgoal to prove: (C3 SMALLER-THAN C2) Depth: 2 solved and helpful Interest: 1.0 Inherited Interest: 0.0 Probability: 1 (1 WFF20 WFF3 WFF2) Subgoals - need to solve 1 subgoals ------------------------------ PROOF subgoal terminated with YES Depth: 3 solved and helpful Interest: 0 Inherited Interest: 0 Probability: 1 (1 WFF31 WFF3 WFF2) Wff(s) used: WFF31: (A X (X BIRD) (A Y (Y FOX) (X SMALLER-THAN Y))) WFF3: (C3 BIRD) WFF2: (C2 FOX) ------------------------------ PROOF subgoal to prove: (E X (X PLANT) (NOT C2 LIKE-TO-EAT X)) Depth: 2 solved and helpful Interest: 10.0 Inherited Interest: 0.0 Probability: 1 (1 WFF20 WFF3 WFF2) Subgoals - need to solve 1 subgoals ------------------------------ PROOF subgoal to prove: (E X (X PLANT) (E Y (Y ANIMAL) ((X PLANT) AND (E Z (Z PLANT) (NOT Y LIKE-TO-EAT Z)) (C2 SMALLER-THAN Y) (NOT Y LIKE-TO-EAT C2)))) Depth: 3 solved and helpful Interest: 10.0 Inherited Interest: 0.0 Probability: 1 (1 WFF2 WFF20) Wff(s) used: WFF2: (C2 FOX) WFF20: (A X (X ANIMAL) ((A Y (Y PLANT) (X LIKE-TO-EAT Y)) OR (A Z ((Z ANIMAL) AND (Z SMALLER-THAN X) (E X1 (X1 PLANT) (Z LIKE-TO-EAT X1))) (X LIKE-TO-EAT Z)))) Subgoals - need to solve 1 subgoals ------------------------------ PROOF subgoal to prove: (E X (X ANIMAL) ((E Z (Z PLANT) (NOT X LIKE-TO-EAT Z)) AND (C2 SMALLER-THAN X) (NOT X LIKE-TO-EAT C2))) Depth: 4 solved and helpful Interest: 10.0 Inherited Interest: 0.0 Probability: 1 (1 WFF6) Wff(s) used: WFF6: (C6 GRAIN) Subgoals - need to solve 1 subgoals ------------------------------ PROOF subgoal to prove: (E X (X ANIMAL) ((E Y (Y PLANT) ((X WOLF) AND ((Y GRAIN) OR (Y FOX)))) AND (C2 SMALLER-THAN X) (NOT X LIKE-TO-EAT C2))) Depth: 5 solved and helpful Interest: 10.0 Inherited Interest: 0.0 Probability: 1 (1 WFF41) Wff(s) used: WFF41: (A X (X WOLF) (A Y ((Y GRAIN) OR (Y FOX)) (NOT X LIKE-TO-EAT Y))) Subgoals - need to solve 1 subgoals ------------------------------ PROOF subgoal to prove: (E X (X ANIMAL) ((X WOLF) AND (C2 SMALLER-THAN X) (NOT X LIKE-TO-EAT C2))) Depth: 6 solved and helpful Interest: 10.0 Inherited Interest: 0.0 Probability: 1 (1 WFF6) Wff(s) used: WFF6: (C6 GRAIN) Subgoals - need to solve 1 subgoals ------------------------------ PROOF subgoal to prove: (E X (X ANIMAL) ((X WOLF) AND (C2 SMALLER-THAN X))) Depth: 7 solved and helpful Interest: 3.0 Inherited Interest: 0.0 Probability: 1 (1 WFF2 WFF41) Wff(s) used: WFF2: (C2 FOX) WFF41: (A X (X WOLF) (A Y ((Y GRAIN) OR (Y FOX)) (NOT X LIKE-TO-EAT Y))) Subgoals - need to solve 1 subgoals ------------------------------ PROOF subgoal to prove: (E X (X ANIMAL) (X WOLF)) Depth: 8 solved and helpful Interest: 3.0 Inherited Interest: 0 Probability: 1 (1 WFF2 WFF35) Wff(s) used: WFF2: (C2 FOX) WFF35: (A X (X FOX) (A Y (Y WOLF) (X SMALLER-THAN Y))) Subgoals - need to solve 1 subgoals ------------------------------ PROOF subgoal terminated with YES Depth: 9 solved and helpful Interest: 0 Inherited Interest: 0 Probability: 1 (1 WFF1) Wff(s) used: WFF1: (C1 WOLF) ------------------------------ PROOF subgoal to prove: (E X (X PLANT) (C3 LIKE-TO-EAT X)) Depth: 2 solved and helpful Interest: 10.0 Inherited Interest: 0.0 Probability: 1 (1 WFF20 WFF3 WFF2) Subgoals - need to solve 1 subgoals ------------------------------ PROOF subgoal to prove: (E X (X PLANT) ((X PLANT) AND (E Y ((Y ANIMAL) AND (Y SMALLER-THAN C3) (E Z (Z PLANT) (Y LIKE-TO-EAT Z))) (NOT C3 LIKE-TO-EAT Y)))) Depth: 3 solved and helpful Interest: 10.0 Inherited Interest: 0.0 Probability: 1 (1 WFF3 WFF20) Wff(s) used: WFF3: (C3 BIRD) WFF20: (A X (X ANIMAL) ((A Y (Y PLANT) (X LIKE-TO-EAT Y)) OR (A Z ((Z ANIMAL) AND (Z SMALLER-THAN X) (E X1 (X1 PLANT) (Z LIKE-TO-EAT X1))) (X LIKE-TO-EAT Z)))) Subgoals - need to solve 1 subgoals ------------------------------ PROOF subgoal to prove: (E X ((X ANIMAL) AND (X SMALLER-THAN C3) (E Z (Z PLANT) (X LIKE-TO-EAT Z))) (NOT C3 LIKE-TO-EAT X)) Depth: 4 solved and helpful Interest: 10.0 Inherited Interest: 0.0 Probability: 1 (1 WFF6) Wff(s) used: WFF6: (C6 GRAIN) Subgoals - need to solve 1 subgoals ------------------------------ PROOF subgoal to prove: (E X ((X ANIMAL) AND (X SMALLER-THAN C3) (E Y (Y PLANT) (X LIKE-TO-EAT Y))) (NOT C3 LIKE-TO-EAT X)) Depth: 5 solved and helpful Interest: 10.0 Inherited Interest: 0.0 Probability: 1 (1 WFF6) Assumptions: WFF60: (C7 PLANT) WFF61: (C5 LIKE-TO-EAT C7) WFF64: (C8 PLANT) WFF65: (C4 LIKE-TO-EAT C8) Wff(s) used: WFF51: (A X ((X SNAIL) OR (X CATERPILLAR)) (E U (U PLANT) (X LIKE-TO-EAT U))) Subgoals - need to solve 2 subgoals - combine with OR ------------------------------ PROOF subgoal to prove: ((C5 SMALLER-THAN C3) AND (NOT C3 LIKE-TO-EAT C5)) Depth: 6 solved and helpful Interest: 15.0 Inherited Interest: 0.0 Probability: 1 (1 PROB1 WFF60 WFF5) Wff(s) used: WFF61: (C5 LIKE-TO-EAT C7) (assumption) WFF60: (C7 PLANT) (assumption) WFF5: (C5 SNAIL) Subgoals - need to solve 2 subgoals - combine with AND ------------------------------ PROOF subgoal to prove: (C5 SMALLER-THAN C3) Depth: 7 solved and helpful Interest: 1.5 Inherited Interest: 5.0 Probability: 1 (1 PROB1 WFF60 WFF5) Subgoals - need to solve 1 subgoals ------------------------------ PROOF subgoal terminated with YES Depth: 8 solved and helpful Interest: 0 Inherited Interest: 0 Probability: 1 (1 WFF27 WFF5 WFF3) Wff(s) used: WFF27: (A X ((X SNAIL) OR (X CATERPILLAR)) (A Y (Y BIRD) (X SMALLER-THAN Y))) WFF5: (C5 SNAIL) WFF3: (C3 BIRD) ------------------------------ PROOF subgoal to prove: (NOT C3 LIKE-TO-EAT C5) Depth: 7 solved and helpful Interest: 15.0 Inherited Interest: 5.0 Probability: 1 (1 PROB1 WFF60 WFF5) Subgoals - need to solve 1 subgoals ------------------------------ PROOF subgoal terminated with YES Depth: 8 solved and helpful Interest: 0 Inherited Interest: 5.0 Probability: 1 (1 WFF47 WFF3 WFF5) Wff(s) used: WFF47: (A X (X BIRD) (A Y (Y SNAIL) (NOT X LIKE-TO-EAT Y))) WFF3: (C3 BIRD) WFF5: (C5 SNAIL) ((YES (WFF5 WFF3 WFF47 WFF27 WFF51 WFF6 WFF20 WFF31 WFF41 WFF1 WFF2 WFF35) (1 WFF5 WFF51 WFF27 WFF3 WFF47 WFF6 WFF20 WFF2 WFF31 WFF41 WFF1 WFF35))) EPI(40): EPI(40): Retracting past the named checkpoint QUESTION NIL EPI(41): EPI(41): EPI(41): 21050 EPI(42): EPI(42): T EPI(43): T EPI(44): T EPI(45): 0.0 EPI(46): EPI(46): EPI(46): Loading story sentence ... WFF1: (C1 WOLF) Stored in Input Array [0] Probability: 1 There is a wolf. Loading story sentence ... WFF2: (C2 FOX) Stored in Input Array [1] Probability: 1 There is a fox. Loading story sentence ... WFF3: (C3 BIRD) Stored in Input Array [2] Probability: 1 There is a bird. Loading story sentence ... WFF4: (C4 CATERPILLAR) Stored in Input Array [3] Probability: 1 There is a caterpillar. Loading story sentence ... WFF5: (C5 SNAIL) Stored in Input Array [4] Probability: 1 There is a snail. (WFF1 WFF2 WFF3 WFF4 WFF5) EPI(47): EPI(47): Loading story sentence ... WFF6: (C6 GRAIN) Stored in Input Array [5] Probability: 1 There is some grain. (WFF6) EPI(48): EPI(48): EPI(48): Loading knowledge ... WFF20: (A X (X ANIMAL) ((A Y (Y PLANT) (X LIKE-TO-EAT Y)) OR (A Z ((Z ANIMAL) AND (Z SMALLER-THAN X) (E X1 (X1 PLANT) (Z LIKE-TO-EAT X1))) (X LIKE-TO-EAT Z)))) Probability: 1 Animals like to eat plants, or they like to eat other animals smaller than the animals that like to eat other plants. (WFF20) EPI(49): EPI(49): Loading knowledge ... WFF27: (A X ((X SNAIL) OR (X CATERPILLAR)) (A Y (Y BIRD) (X SMALLER-THAN Y))) Probability: 1 ** INFERRED FORMULA ** WFF28: (C4 SMALLER-THAN C3) Rank: 1 Parents: (WFF27 WFF3 WFF4) Probability: 1 ** INFERRED FORMULA ** WFF29: (C5 SMALLER-THAN C3) Rank: 1 Parents: (WFF27 WFF3 WFF5) Probability: 1 Snails or caterpillars are smaller than birds. A caterpillar is smaller than a bird. A snail is smaller than the bird. (WFF27 WFF28 WFF29) EPI(50): EPI(50): Loading knowledge ... WFF34: (A X (X BIRD) (A Y (Y FOX) (X SMALLER-THAN Y))) Probability: 1 ** INFERRED FORMULA ** WFF35: (C3 SMALLER-THAN C2) Rank: 1 Parents: (WFF34 WFF2 WFF3) Probability: 1 Birds are smaller than foxes. A bird is smaller than a fox. (WFF34 WFF35) EPI(51): EPI(51): Loading knowledge ... WFF39: (A X (X FOX) (A Y (Y WOLF) (X SMALLER-THAN Y))) Probability: 1 ** INFERRED FORMULA ** WFF40: (C2 SMALLER-THAN C1) Rank: 1 Parents: (WFF39 WFF1 WFF2) Probability: 1 Foxes are smaller than wolves. A fox is smaller than a wolf. (WFF39 WFF40) EPI(52): EPI(52): Loading knowledge ... WFF46: (A X (X WOLF) (A Y ((Y GRAIN) OR (Y FOX)) (NOT X LIKE-TO-EAT Y))) Probability: 1 ** INFERRED FORMULA ** WFF47: (NOT C1 LIKE-TO-EAT C6) Rank: 1 Parents: (WFF46 WFF6 WFF1) Probability: 1 ** INFERRED FORMULA ** WFF49: (NOT C1 LIKE-TO-EAT C2) Rank: 1 Parents: (WFF46 WFF2 WFF1) Probability: 1 No wolf likes to eat grain or any foxes. A wolf doesn't like to eat some grain. The wolf doesn't like to eat a fox. (WFF46 WFF47 WFF49) EPI(53): EPI(53): Loading knowledge ... WFF52: (A X (X BIRD) (A Y (Y CATERPILLAR) (X LIKE-TO-EAT Y))) Probability: 1 ** INFERRED FORMULA ** WFF53: (C3 LIKE-TO-EAT C4) Rank: 1 Parents: (WFF52 WFF4 WFF3) Probability: 1 Birds like to eat caterpillars. A bird likes to eat a caterpillar. (WFF52 WFF53) EPI(54): EPI(54): Loading knowledge ... WFF56: (A X (X BIRD) (A Y (Y SNAIL) (NOT X LIKE-TO-EAT Y))) Probability: 1 ** INFERRED FORMULA ** WFF57: (NOT C3 LIKE-TO-EAT C5) Rank: 1 Parents: (WFF56 WFF5 WFF3) Probability: 1 No bird likes to eat a snail. A bird doesn't like to eat a snail. (WFF56 WFF57) EPI(55): EPI(55): Loading knowledge ... WFF62: (A X ((X SNAIL) OR (X CATERPILLAR)) (E U (U PLANT) (X LIKE-TO-EAT U))) Probability: 1 Adding PROOF subgoal to prove: (E X (X PLANT) (C5 LIKE-TO-EAT X)) ** INFERRED FORMULA ** WFF65: (C7 PLANT) Rank: 1 Parents: (WFF62 WFF5) Probability: 1 ** INFERRED FORMULA ** WFF66: (C5 LIKE-TO-EAT C7) Rank: 1 Parents: (WFF62 WFF5) Probability: 1 Adding PROOF subgoal to prove: (E X (X PLANT) (C4 LIKE-TO-EAT X)) ** INFERRED FORMULA ** WFF70: (C8 PLANT) Rank: 1 Parents: (WFF62 WFF4) Probability: 1 ** INFERRED FORMULA ** WFF71: (C4 LIKE-TO-EAT C8) Rank: 1 Parents: (WFF62 WFF4) Probability: 1 Snails or caterpillars like to eat plants. A snail likes to eat a plant. A caterpillar likes to eat a plant. (WFF62 WFF65 WFF66 WFF70 WFF71) EPI(56): EPI(56): Questioning (E U (U ANIMAL) (E V ((V ANIMAL) AND (E W (W GRAIN) (V LIKE-TO-EAT W))) (U LIKE-TO-EAT V))) Adding PROOF subgoal to prove: (E X (X ANIMAL) (E Y ((Y ANIMAL) AND (E Z (Z GRAIN) (Y LIKE-TO-EAT Z))) (X LIKE-TO-EAT Y))) Adding PROOF subgoal to prove: (E X (X GRAIN) (C4 LIKE-TO-EAT X)) Adding PROOF subgoal to prove: (C8 GRAIN) Adding PROOF subgoal to prove: (E X (X ANIMAL) ((C7 GRAIN) AND (X LIKE-TO-EAT C5))) Adding PROOF subgoal to prove: (E X (X ANIMAL) ((C8 GRAIN) AND (X LIKE-TO-EAT C4))) Instantiating (A X ((X SNAIL) OR (X CATERPILLAR)) (E U (U PLANT) (X LIKE-TO-EAT U))) with substitutions ((X by C4 1)) Adding PROOF subgoal to prove: (E X (X GRAIN) (C4 LIKE-TO-EAT X)) Adding PROOF subgoal to prove: (C9 GRAIN) Adding PROOF subgoal to prove: (E X (X GRAIN) ((X PLANT) AND (E Y ((Y ANIMAL) AND (Y SMALLER-THAN C4) (E Z (Z PLANT) (Y LIKE-TO-EAT Z))) (NOT C4 LIKE-TO-EAT Y)))) Adding PROOF subgoal to prove: (E X (X GRAIN) ((X PLANT) AND (C4 SMALLER-THAN C4) (NOT C4 LIKE-TO-EAT C4))) Adding PROOF subgoal to prove: ((C9 GRAIN) AND (C4 SMALLER-THAN C4) (NOT C4 LIKE-TO-EAT C4)) Splitting subgoal ((C9 GRAIN) AND (C4 SMALLER-THAN C4) (NOT C4 LIKE-TO-EAT C4)) into ANDed subgoals Adding PROOF subgoal to prove: (C4 SMALLER-THAN C4) Adding PROOF subgoal to prove: (NOT C4 LIKE-TO-EAT C4) Adding PROOF subgoal to prove: ((C4 SMALLER-THAN C4) AND (NOT C4 LIKE-TO-EAT C4)) Splitting subgoal ((C4 SMALLER-THAN C4) AND (NOT C4 LIKE-TO-EAT C4)) into ANDed subgoals Adding PROOF subgoal to prove: ((C7 GRAIN) AND (C4 SMALLER-THAN C4) (NOT C4 LIKE-TO-EAT C4)) Splitting subgoal ((C7 GRAIN) AND (C4 SMALLER-THAN C4) (NOT C4 LIKE-TO-EAT C4)) into ANDed subgoals Adding PROOF subgoal to prove: (C7 GRAIN) Adding PROOF subgoal to prove: ((C8 GRAIN) AND (C4 SMALLER-THAN C4) (NOT C4 LIKE-TO-EAT C4)) Splitting subgoal ((C8 GRAIN) AND (C4 SMALLER-THAN C4) (NOT C4 LIKE-TO-EAT C4)) into ANDed subgoals Adding PROOF subgoal to prove: (E X ((X ANIMAL) AND (X SMALLER-THAN C4) (E Z (Z PLANT) (X LIKE-TO-EAT Z))) (NOT C4 LIKE-TO-EAT X)) Adding PROOF subgoal to prove: ((C5 SMALLER-THAN C4) AND (NOT C4 LIKE-TO-EAT C5)) Splitting subgoal ((C5 SMALLER-THAN C4) AND (NOT C4 LIKE-TO-EAT C5)) into ANDed subgoals Adding PROOF subgoal to prove: (C5 SMALLER-THAN C4) Adding PROOF subgoal to prove: (NOT C4 LIKE-TO-EAT C5) Adding PROOF subgoal to prove: ((C9 GRAIN) AND (E X ((X ANIMAL) AND (X SMALLER-THAN C4) (E Z (Z PLANT) (X LIKE-TO-EAT Z))) (NOT C4 LIKE-TO-EAT X))) Splitting subgoal ((C9 GRAIN) AND (E X ((X ANIMAL) AND (X SMALLER-THAN C4) (E Z (Z PLANT) (X LIKE-TO-EAT Z))) (NOT C4 LIKE-TO-EAT X))) into ANDed subgoals Adding PROOF subgoal to prove: (E X ((X ANIMAL) AND (X SMALLER-THAN C4) (E Y (Y PLANT) (X LIKE-TO-EAT Y))) (NOT C4 LIKE-TO-EAT X)) Adding PROOF subgoal to prove: ((C7 GRAIN) AND (E X ((X ANIMAL) AND (X SMALLER-THAN C4) (E Z (Z PLANT) (X LIKE-TO-EAT Z))) (NOT C4 LIKE-TO-EAT X))) Splitting subgoal ((C7 GRAIN) AND (E X ((X ANIMAL) AND (X SMALLER-THAN C4) (E Z (Z PLANT) (X LIKE-TO-EAT Z))) (NOT C4 LIKE-TO-EAT X))) into ANDed subgoals Adding PROOF subgoal to prove: (E X (X GRAIN) ((X PLANT) AND (C5 SMALLER-THAN C4) (NOT C4 LIKE-TO-EAT C5))) Adding PROOF subgoal to prove: ((C9 GRAIN) AND (C5 SMALLER-THAN C4) (NOT C4 LIKE-TO-EAT C5)) Splitting subgoal ((C9 GRAIN) AND (C5 SMALLER-THAN C4) (NOT C4 LIKE-TO-EAT C5)) into ANDed subgoals Adding PROOF subgoal to prove: ((C7 GRAIN) AND (C5 SMALLER-THAN C4) (NOT C4 LIKE-TO-EAT C5)) Splitting subgoal ((C7 GRAIN) AND (C5 SMALLER-THAN C4) (NOT C4 LIKE-TO-EAT C5)) into ANDed subgoals Adding PROOF subgoal to prove: ((C8 GRAIN) AND (C5 SMALLER-THAN C4) (NOT C4 LIKE-TO-EAT C5)) Splitting subgoal ((C8 GRAIN) AND (C5 SMALLER-THAN C4) (NOT C4 LIKE-TO-EAT C5)) into ANDed subgoals Adding PROOF subgoal to prove: ((C8 GRAIN) AND (E X ((X ANIMAL) AND (X SMALLER-THAN C4) (E Z (Z PLANT) (X LIKE-TO-EAT Z))) (NOT C4 LIKE-TO-EAT X))) Splitting subgoal ((C8 GRAIN) AND (E X ((X ANIMAL) AND (X SMALLER-THAN C4) (E Z (Z PLANT) (X LIKE-TO-EAT Z))) (NOT C4 LIKE-TO-EAT X))) into ANDed subgoals Looking for inferences with (A X ((X SNAIL) OR (X CATERPILLAR)) (E U (U PLANT) (X LIKE-TO-EAT U))) Adding PROOF subgoal to prove: (E X ((X ANIMAL) AND (X SMALLER-THAN C4) (E Y (Y PLANT) (X LIKE-TO-EAT Y))) (NOT C4 LIKE-TO-EAT X)) Adding PROOF subgoal to prove: (E X ((X ANIMAL) AND (X SMALLER-THAN C4) (E Y (Y PLANT) ((Y PLANT) AND (X ANIMAL) (E Z ((Z ANIMAL) AND (Z SMALLER-THAN X) (E X1 (X1 PLANT) (Z LIKE-TO-EAT X1))) (NOT X LIKE-TO-EAT Z))))) (NOT C4 LIKE-TO-EAT X)) Adding PROOF subgoal to prove: ((C3 SMALLER-THAN C4) AND (NOT C4 LIKE-TO-EAT C3) (E X (X PLANT) ((X PLANT) AND (E Z (Z PLANT) (C5 LIKE-TO-EAT Z))))) Splitting subgoal ((C3 SMALLER-THAN C4) AND (NOT C4 LIKE-TO-EAT C3) (E X (X PLANT) ((X PLANT) AND (E Z (Z PLANT) (C5 LIKE-TO-EAT Z))))) into ANDed subgoals Adding PROOF subgoal to prove: (C3 SMALLER-THAN C4) Adding PROOF subgoal to prove: (NOT C4 LIKE-TO-EAT C3) Adding PROOF subgoal to prove: (E X (X PLANT) ((X PLANT) AND (E Y (Y PLANT) (C5 LIKE-TO-EAT Y)))) Adding PROOF subgoal to prove: (E X ((X ANIMAL) AND (X SMALLER-THAN C4) (E Y (Y PLANT) ((Y PLANT) AND (X ANIMAL) (C4 SMALLER-THAN X) (NOT X LIKE-TO-EAT C4)))) (NOT C4 LIKE-TO-EAT X)) Adding PROOF subgoal to prove: (E X ((X ANIMAL) AND (X SMALLER-THAN C4) (C4 SMALLER-THAN X) (NOT X LIKE-TO-EAT C4)) (NOT C4 LIKE-TO-EAT X)) Adding PROOF subgoal to prove: (E X ((X ANIMAL) AND (X SMALLER-THAN C4) (E Y ((Y ANIMAL) AND (Y SMALLER-THAN X) (E X1 (X1 PLANT) (Y LIKE-TO-EAT X1))) (NOT X LIKE-TO-EAT Y))) (NOT C4 LIKE-TO-EAT X)) Adding PROOF subgoal to prove: ((C3 SMALLER-THAN C4) AND (NOT C4 LIKE-TO-EAT C3) (E X (X PLANT) (C5 LIKE-TO-EAT X))) Splitting subgoal ((C3 SMALLER-THAN C4) AND (NOT C4 LIKE-TO-EAT C3) (E X (X PLANT) (C5 LIKE-TO-EAT X))) into ANDed subgoals Adding PROOF subgoal to prove: (E X (X PLANT) (C5 LIKE-TO-EAT X)) Adding PROOF subgoal to prove: ((C1 SMALLER-THAN C4) AND (NOT C4 LIKE-TO-EAT C1) (E X (X PLANT) (C2 LIKE-TO-EAT X))) Splitting subgoal ((C1 SMALLER-THAN C4) AND (NOT C4 LIKE-TO-EAT C1) (E X (X PLANT) (C2 LIKE-TO-EAT X))) into ANDed subgoals Adding PROOF subgoal to prove: (C1 SMALLER-THAN C4) Adding PROOF subgoal to prove: (NOT C4 LIKE-TO-EAT C1) Adding PROOF subgoal to prove: (E X (X PLANT) (C2 LIKE-TO-EAT X)) Adding PROOF subgoal to prove: (E X ((X ANIMAL) AND (X SMALLER-THAN C4) (C5 SMALLER-THAN X) (NOT X LIKE-TO-EAT C5)) (NOT C4 LIKE-TO-EAT X)) Adding PROOF subgoal to prove: ((C3 SMALLER-THAN C4) AND (NOT C4 LIKE-TO-EAT C3)) Splitting subgoal ((C3 SMALLER-THAN C4) AND (NOT C4 LIKE-TO-EAT C3)) into ANDed subgoals Adding PROOF subgoal to prove: ((C2 SMALLER-THAN C4) AND (NOT C2 LIKE-TO-EAT C3) (NOT C4 LIKE-TO-EAT C2) (E X (X PLANT) (C3 LIKE-TO-EAT X))) Splitting subgoal ((C2 SMALLER-THAN C4) AND (NOT C2 LIKE-TO-EAT C3) (NOT C4 LIKE-TO-EAT C2) (E X (X PLANT) (C3 LIKE-TO-EAT X))) into ANDed subgoals Adding PROOF subgoal to prove: (C2 SMALLER-THAN C4) Adding PROOF subgoal to prove: (NOT C2 LIKE-TO-EAT C3) Adding PROOF subgoal to prove: (NOT C4 LIKE-TO-EAT C2) Adding PROOF subgoal to prove: (E X (X PLANT) (C3 LIKE-TO-EAT X)) Adding PROOF subgoal to prove: ((C1 SMALLER-THAN C4) AND (NOT C4 LIKE-TO-EAT C1) (E X (X PLANT) ((X PLANT) AND (E Z (Z PLANT) (C2 LIKE-TO-EAT Z))))) Splitting subgoal ((C1 SMALLER-THAN C4) AND (NOT C4 LIKE-TO-EAT C1) (E X (X PLANT) ((X PLANT) AND (E Z (Z PLANT) (C2 LIKE-TO-EAT Z))))) into ANDed subgoals Adding PROOF subgoal to prove: (E X (X PLANT) ((X PLANT) AND (E Y (Y PLANT) (C2 LIKE-TO-EAT Y)))) Adding PROOF subgoal to prove: (E X ((X ANIMAL) AND (X SMALLER-THAN C4) (E Y (Y PLANT) ((Y PLANT) AND (X ANIMAL) (C5 SMALLER-THAN X) (NOT X LIKE-TO-EAT C5)))) (NOT C4 LIKE-TO-EAT X)) Adding PROOF subgoal to prove: ((C3 SMALLER-THAN C4) AND (NOT C4 LIKE-TO-EAT C3) (E X (X PLANT) (X PLANT))) Splitting subgoal ((C3 SMALLER-THAN C4) AND (NOT C4 LIKE-TO-EAT C3) (E X (X PLANT) (X PLANT))) into ANDed subgoals Adding PROOF subgoal to prove: (E X (X PLANT) (X PLANT)) Adding PROOF subgoal to prove: ((C2 SMALLER-THAN C4) AND (NOT C4 LIKE-TO-EAT C2) (E X (X PLANT) ((X PLANT) AND (NOT C2 LIKE-TO-EAT C3) (E Z (Z PLANT) (C3 LIKE-TO-EAT Z))))) Splitting subgoal ((C2 SMALLER-THAN C4) AND (NOT C4 LIKE-TO-EAT C2) (E X (X PLANT) ((X PLANT) AND (NOT C2 LIKE-TO-EAT C3) (E Z (Z PLANT) (C3 LIKE-TO-EAT Z))))) into ANDed subgoals Adding PROOF subgoal to prove: (E X (X PLANT) ((X PLANT) AND (NOT C2 LIKE-TO-EAT C3) (E Y (Y PLANT) (C3 LIKE-TO-EAT Y)))) Maximum number of iterations (400) reached. Use (q) to continue. Answer: UNKNOWN Used 3.19 seconds CPU time 3.212 seconds real time Used 400 iterations NIL EPI(57): Used 4.78 seconds CPU time NIL EPI(58): Questioning (C2 LIKE-TO-EAT C3) Adding PROOF subgoal to prove: (C2 LIKE-TO-EAT C3) Adding DISPROOF subgoal to prove: (NOT C2 LIKE-TO-EAT C3) Adding PROOF subgoal to prove: ((E X (X PLANT) (NOT C2 LIKE-TO-EAT X)) AND (E Z (Z PLANT) (C3 LIKE-TO-EAT Z))) Splitting subgoal ((E X (X PLANT) (NOT C2 LIKE-TO-EAT X)) AND (E Z (Z PLANT) (C3 LIKE-TO-EAT Z))) into ANDed subgoals Adding PROOF subgoal to prove: (E X (X PLANT) (NOT C2 LIKE-TO-EAT X)) Adding PROOF subgoal to prove: (E X (X PLANT) (C3 LIKE-TO-EAT X)) Instantiating (A X ((X SNAIL) OR (X CATERPILLAR)) (E U (U PLANT) (X LIKE-TO-EAT U))) with substitutions ((X by C3 1)) Adding PROOF subgoal to prove: (E X (X PLANT) ((X PLANT) AND (E Y ((Y ANIMAL) AND (Y SMALLER-THAN C3) (E Z (Z PLANT) (Y LIKE-TO-EAT Z))) (NOT C3 LIKE-TO-EAT Y)))) Adding PROOF subgoal to prove: (E X (X PLANT) ((X PLANT) AND (E Y (Y PLANT) (C5 LIKE-TO-EAT Y)))) Adding PROOF subgoal to prove: (E X (X PLANT) (X PLANT)) Answer YES for (E X (X PLANT) (X PLANT)) Answer YES for (E X (X PLANT) ((X PLANT) AND (E Y (Y PLANT) (C5 LIKE-TO-EAT Y)))) Answer YES for (E X (X PLANT) ((X PLANT) AND (E Y ((Y ANIMAL) AND (Y SMALLER-THAN C3) (E Z (Z PLANT) (Y LIKE-TO-EAT Z))) (NOT C3 LIKE-TO-EAT Y)))) Answer YES for (E X (X PLANT) (C3 LIKE-TO-EAT X)) Adding PROOF subgoal to prove: (E X (X PLANT) (E Y (Y ANIMAL) ((X PLANT) AND (E Z (Z PLANT) (NOT Y LIKE-TO-EAT Z)) (C2 SMALLER-THAN Y) (NOT Y LIKE-TO-EAT C2)))) Adding PROOF subgoal to prove: (E X (X PLANT) ((X PLANT) AND (E Y (Y PLANT) (NOT C1 LIKE-TO-EAT Y)))) Adding PROOF subgoal to prove: (E X (X PLANT) (NOT C1 LIKE-TO-EAT X)) Adding PROOF subgoal to prove: (E X (X ANIMAL) ((E Z (Z PLANT) (NOT X LIKE-TO-EAT Z)) AND (C2 SMALLER-THAN X) (NOT X LIKE-TO-EAT C2))) Answer YES for (E X (X PLANT) (NOT C1 LIKE-TO-EAT X)) Answer YES for (E X (X PLANT) ((X PLANT) AND (E Y (Y PLANT) (NOT C1 LIKE-TO-EAT Y)))) Answer YES for (E X (X PLANT) (E Y (Y ANIMAL) ((X PLANT) AND (E Z (Z PLANT) (NOT Y LIKE-TO-EAT Z)) (C2 SMALLER-THAN Y) (NOT Y LIKE-TO-EAT C2)))) Answer YES for (E X (X PLANT) (NOT C2 LIKE-TO-EAT X)) Answer YES for ((E X (X PLANT) (NOT C2 LIKE-TO-EAT X)) AND (E Z (Z PLANT) (C3 LIKE-TO-EAT Z))) Answer YES for (C2 LIKE-TO-EAT C3) Answer: YES with probability 1 Yes, a bird smaller than a fox smaller than a wolf that doesn't like to eat some grain and a fox smaller than the wolf doesn't like to eat a snail smaller than the bird that likes to eat a plant. Animals like to eat plants, or they like to eat other animals smaller than the animals that like to eat other plants. Used 0.67 seconds CPU time 0.674 seconds real time Used 71 iterations Searched to depth 6 ------------------------------ PROOF subgoal to prove: (C2 LIKE-TO-EAT C3) Depth: 0 solved and helpful Interest: 36.197952 Inherited Interest: 0.0 Probability: 1 1 Subgoals - need to solve 1 subgoals ------------------------------ PROOF subgoal to prove: ((E X (X PLANT) (NOT C2 LIKE-TO-EAT X)) AND (E Z (Z PLANT) (C3 LIKE-TO-EAT Z))) Depth: 1 solved and helpful Interest: 26.684063 Inherited Interest: 26.197952 Probability: 1 (1 WFF20 WFF34 WFF2 WFF3) Wff(s) used: WFF20: (A X (X ANIMAL) ((A Y (Y PLANT) (X LIKE-TO-EAT Y)) OR (A Z ((Z ANIMAL) AND (Z SMALLER-THAN X) (E X1 (X1 PLANT) (Z LIKE-TO-EAT X1))) (X LIKE-TO-EAT Z)))) WFF35: (C3 SMALLER-THAN C2) WFF3: (C3 BIRD) WFF2: (C2 FOX) Subgoals - need to solve 2 subgoals - combine with AND ------------------------------ PROOF subgoal to prove: (E X (X PLANT) (NOT C2 LIKE-TO-EAT X)) Depth: 2 solved and helpful Interest: 19.513891 Inherited Interest: 16.684063 Probability: 1 (1 WFF20 WFF34 WFF2 WFF3) Subgoals - need to solve 1 subgoals ------------------------------ PROOF subgoal to prove: (E X (X PLANT) (E Y (Y ANIMAL) ((X PLANT) AND (E Z (Z PLANT) (NOT Y LIKE-TO-EAT Z)) (C2 SMALLER-THAN Y) (NOT Y LIKE-TO-EAT C2)))) Depth: 3 solved and helpful Interest: 19.513891 Inherited Interest: 9.513891 Probability: 1 (1 WFF2 WFF20) Wff(s) used: WFF2: (C2 FOX) WFF20: (A X (X ANIMAL) ((A Y (Y PLANT) (X LIKE-TO-EAT Y)) OR (A Z ((Z ANIMAL) AND (Z SMALLER-THAN X) (E X1 (X1 PLANT) (Z LIKE-TO-EAT X1))) (X LIKE-TO-EAT Z)))) Subgoals - need to solve 2 subgoals - combine with OR ------------------------------ PROOF subgoal to prove: (E X (X PLANT) ((X PLANT) AND (E Y (Y PLANT) (NOT C1 LIKE-TO-EAT Y)))) Depth: 4 solved and helpful Interest: 24.226421 Inherited Interest: 9.513891 Probability: 1 (1 WFF46 WFF39 WFF1 WFF2) Wff(s) used: WFF40: (C2 SMALLER-THAN C1) WFF49: (NOT C1 LIKE-TO-EAT C2) WFF1: (C1 WOLF) Subgoals - need to solve 1 subgoals ------------------------------ PROOF subgoal to prove: (E X (X PLANT) (NOT C1 LIKE-TO-EAT X)) Depth: 5 solved and helpful Interest: 24.226421 Inherited Interest: 14.226421 Probability: 1 (1 WFF65) Wff(s) used: WFF65: (C7 PLANT) Subgoals - need to solve 1 subgoals ------------------------------ PROOF subgoal terminated with YES Depth: 6 solved and helpful Interest: 0 Inherited Interest: 14.226421 Probability: 1 (1 WFF46 WFF6 WFF1) Wff(s) used: WFF6: (C6 GRAIN) WFF47: (NOT C1 LIKE-TO-EAT C6) ------------------------------ PROOF subgoal to prove: (E X (X PLANT) (C3 LIKE-TO-EAT X)) Depth: 2 solved and helpful Interest: 26.684063 Inherited Interest: 16.684063 Probability: 1 (1 WFF20 WFF34 WFF2 WFF3) Subgoals - need to solve 1 subgoals ------------------------------ PROOF subgoal to prove: (E X (X PLANT) ((X PLANT) AND (E Y ((Y ANIMAL) AND (Y SMALLER-THAN C3) (E Z (Z PLANT) (Y LIKE-TO-EAT Z))) (NOT C3 LIKE-TO-EAT Y)))) Depth: 3 solved and helpful Interest: 26.684063 Inherited Interest: 16.684063 Probability: 1 (1 WFF3 WFF20) Wff(s) used: WFF3: (C3 BIRD) WFF20: (A X (X ANIMAL) ((A Y (Y PLANT) (X LIKE-TO-EAT Y)) OR (A Z ((Z ANIMAL) AND (Z SMALLER-THAN X) (E X1 (X1 PLANT) (Z LIKE-TO-EAT X1))) (X LIKE-TO-EAT Z)))) Subgoals - need to solve 1 subgoals ------------------------------ PROOF subgoal to prove: (E X (X PLANT) ((X PLANT) AND (E Y (Y PLANT) (C5 LIKE-TO-EAT Y)))) Depth: 4 solved and helpful Interest: 29.392033 Inherited Interest: 16.684063 Probability: 1 (1 WFF56 WFF27 WFF3 WFF5) Wff(s) used: WFF29: (C5 SMALLER-THAN C3) WFF57: (NOT C3 LIKE-TO-EAT C5) WFF5: (C5 SNAIL) Subgoals - need to solve 1 subgoals ------------------------------ PROOF subgoal to prove: (E X (X PLANT) (X PLANT)) Depth: 5 solved and helpful Interest: 2.0 Inherited Interest: 19.392033 Probability: 1 (1 WFF65 PROB1) Wff(s) used: WFF65: (C7 PLANT) WFF66: (C5 LIKE-TO-EAT C7) Subgoals - need to solve 1 subgoals ------------------------------ PROOF subgoal terminated with YES Depth: 6 solved and helpful Interest: 0 Inherited Interest: 9.392033 Probability: 1 (1 WFF65) Wff(s) used: WFF65: (C7 PLANT) ((YES (WFF1 WFF49 WFF40 WFF65 WFF6 WFF47 WFF2 WFF20 WFF3 WFF66 WFF29 WFF57 WFF5 WFF35) (1 WFF2 WFF1 WFF39 WFF46 WFF65 WFF6 WFF20 WFF34 WFF3 PROB1 WFF56 WFF27 WFF5))) EPI(59): EOF Really exit lisp [n]? ; Exiting Lisp