%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : PUZ031+1 : TPTP v8.1.0. Released v2.0.0. % Transfm : none % Format : tptp:raw % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % Computer : n024.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 600s % DateTime : Mon Jul 18 18:27:48 EDT 2022 % Result : Theorem 0.40s 0.62s % Output : Proof 0.47s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : PUZ031+1 : TPTP v8.1.0. Released v2.0.0. % 0.03/0.13 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.14/0.34 % Computer : n024.cluster.edu % 0.14/0.34 % Model : x86_64 x86_64 % 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.34 % Memory : 8042.1875MB % 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.34 % CPULimit : 300 % 0.14/0.34 % WCLimit : 600 % 0.14/0.34 % DateTime : Sat May 28 23:14:22 EDT 2022 % 0.14/0.34 % CPUTime : % 0.40/0.62 % SZS status Theorem % 0.40/0.62 (* PROOF-FOUND *) % 0.40/0.62 (* BEGIN-PROOF *) % 0.40/0.62 % SZS output start Proof % 0.40/0.62 1. (caterpillar T_0) (-. (caterpillar T_0)) ### Axiom % 0.40/0.62 2. (-. ((caterpillar T_0) \/ (snail T_0))) (caterpillar T_0) ### NotOr 1 % 0.40/0.62 3. (fox T_1) (-. (fox T_1)) ### Axiom % 0.40/0.62 4. (wolf T_2) (-. (wolf T_2)) ### Axiom % 0.40/0.62 5. (bird T_3) (-. (bird T_3)) ### Axiom % 0.40/0.62 6. (fox T_1) (-. (fox T_1)) ### Axiom % 0.40/0.62 7. (wolf T_2) (-. (wolf T_2)) ### Axiom % 0.40/0.62 8. (-. (animal T_2)) (animal T_2) ### Axiom % 0.40/0.62 9. ((wolf T_2) => (animal T_2)) (-. (animal T_2)) (wolf T_2) ### Imply 7 8 % 0.40/0.62 10. (All X, ((wolf X) => (animal X))) (wolf T_2) (-. (animal T_2)) ### All 9 % 0.40/0.62 11. (grain T_4) (-. (grain T_4)) ### Axiom % 0.40/0.62 12. (plant T_4) (-. (plant T_4)) ### Axiom % 0.40/0.62 13. (wolf T_2) (-. (wolf T_2)) ### Axiom % 0.40/0.62 14. (grain T_4) (-. (grain T_4)) ### Axiom % 0.40/0.62 15. (-. ((fox T_4) \/ (grain T_4))) (grain T_4) ### NotOr 14 % 0.40/0.62 16. (eats T_2 T_4) (-. (eats T_2 T_4)) ### Axiom % 0.40/0.62 17. (((wolf T_2) /\ ((fox T_4) \/ (grain T_4))) => (-. (eats T_2 T_4))) (eats T_2 T_4) (grain T_4) (wolf T_2) ### DisjTree 13 15 16 % 0.40/0.62 18. (All Y, (((wolf T_2) /\ ((fox Y) \/ (grain Y))) => (-. (eats T_2 Y)))) (wolf T_2) (grain T_4) (eats T_2 T_4) ### All 17 % 0.40/0.62 19. ((plant T_4) => (eats T_2 T_4)) (grain T_4) (wolf T_2) (All Y, (((wolf T_2) /\ ((fox Y) \/ (grain Y))) => (-. (eats T_2 Y)))) (plant T_4) ### Imply 12 18 % 0.40/0.62 20. (All Y, ((plant Y) => (eats T_2 Y))) (plant T_4) (All Y, (((wolf T_2) /\ ((fox Y) \/ (grain Y))) => (-. (eats T_2 Y)))) (wolf T_2) (grain T_4) ### All 19 % 0.40/0.62 21. ((grain T_4) => (plant T_4)) (wolf T_2) (All Y, (((wolf T_2) /\ ((fox Y) \/ (grain Y))) => (-. (eats T_2 Y)))) (All Y, ((plant Y) => (eats T_2 Y))) (grain T_4) ### Imply 11 20 % 0.40/0.62 22. (All X1, ((grain X1) => (plant X1))) (grain T_4) (All Y, ((plant Y) => (eats T_2 Y))) (All Y, (((wolf T_2) /\ ((fox Y) \/ (grain Y))) => (-. (eats T_2 Y)))) (wolf T_2) ### All 21 % 0.40/0.62 23. (All X, (All Y, (((wolf X) /\ ((fox Y) \/ (grain Y))) => (-. (eats X Y))))) (wolf T_2) (All Y, ((plant Y) => (eats T_2 Y))) (grain T_4) (All X1, ((grain X1) => (plant X1))) ### All 22 % 0.40/0.62 24. (bird T_3) (-. (bird T_3)) ### Axiom % 0.40/0.62 25. (snail T_5) (-. (snail T_5)) ### Axiom % 0.40/0.62 26. (-. ((snail T_5) \/ (caterpillar T_5))) (snail T_5) ### NotOr 25 % 0.40/0.62 27. (fox T_1) (-. (fox T_1)) ### Axiom % 0.40/0.62 28. (-. (animal T_1)) (animal T_1) ### Axiom % 0.40/0.62 29. ((fox T_1) => (animal T_1)) (-. (animal T_1)) (fox T_1) ### Imply 27 28 % 0.40/0.62 30. (All X, ((fox X) => (animal X))) (fox T_1) (-. (animal T_1)) ### All 29 % 0.40/0.62 31. (plant T_6) (-. (plant T_6)) ### Axiom % 0.40/0.62 32. (much_smaller T_1 T_2) (-. (much_smaller T_1 T_2)) ### Axiom % 0.40/0.62 33. (plant T_6) (-. (plant T_6)) ### Axiom % 0.40/0.62 34. (eats T_1 T_6) (-. (eats T_1 T_6)) ### Axiom % 0.40/0.62 35. (-. ((plant T_6) /\ (eats T_1 T_6))) (eats T_1 T_6) (plant T_6) ### NotAnd 33 34 % 0.40/0.62 36. (-. (Ex Y, ((plant Y) /\ (eats T_1 Y)))) (plant T_6) (eats T_1 T_6) ### NotExists 35 % 0.40/0.62 37. (wolf T_2) (-. (wolf T_2)) ### Axiom % 0.40/0.62 38. (fox T_1) (-. (fox T_1)) ### Axiom % 0.40/0.62 39. (-. ((fox T_1) \/ (grain T_1))) (fox T_1) ### NotOr 38 % 0.40/0.62 40. (eats T_2 T_1) (-. (eats T_2 T_1)) ### Axiom % 0.40/0.62 41. (((wolf T_2) /\ ((fox T_1) \/ (grain T_1))) => (-. (eats T_2 T_1))) (eats T_2 T_1) (fox T_1) (wolf T_2) ### DisjTree 37 39 40 % 0.40/0.62 42. (All Y, (((wolf T_2) /\ ((fox Y) \/ (grain Y))) => (-. (eats T_2 Y)))) (wolf T_2) (fox T_1) (eats T_2 T_1) ### All 41 % 0.40/0.62 43. (All X, (All Y, (((wolf X) /\ ((fox Y) \/ (grain Y))) => (-. (eats X Y))))) (eats T_2 T_1) (fox T_1) (wolf T_2) ### All 42 % 0.40/0.62 44. (((animal T_1) /\ ((much_smaller T_1 T_2) /\ (Ex Y, ((plant Y) /\ (eats T_1 Y))))) => (eats T_2 T_1)) (wolf T_2) (All X, (All Y, (((wolf X) /\ ((fox Y) \/ (grain Y))) => (-. (eats X Y))))) (eats T_1 T_6) (plant T_6) (much_smaller T_1 T_2) (fox T_1) (All X, ((fox X) => (animal X))) ### DisjTree 30 32 36 43 % 0.40/0.62 45. (All Y1, (((animal Y1) /\ ((much_smaller Y1 T_2) /\ (Ex Z, ((plant Z) /\ (eats Y1 Z))))) => (eats T_2 Y1))) (All X, ((fox X) => (animal X))) (fox T_1) (much_smaller T_1 T_2) (plant T_6) (eats T_1 T_6) (All X, (All Y, (((wolf X) /\ ((fox Y) \/ (grain Y))) => (-. (eats X Y))))) (wolf T_2) ### All 44 % 0.40/0.62 46. ((plant T_6) => (eats T_1 T_6)) (wolf T_2) (All X, (All Y, (((wolf X) /\ ((fox Y) \/ (grain Y))) => (-. (eats X Y))))) (much_smaller T_1 T_2) (fox T_1) (All X, ((fox X) => (animal X))) (All Y1, (((animal Y1) /\ ((much_smaller Y1 T_2) /\ (Ex Z, ((plant Z) /\ (eats Y1 Z))))) => (eats T_2 Y1))) (plant T_6) ### Imply 31 45 % 0.40/0.62 47. (All Y, ((plant Y) => (eats T_1 Y))) (plant T_6) (All Y1, (((animal Y1) /\ ((much_smaller Y1 T_2) /\ (Ex Z, ((plant Z) /\ (eats Y1 Z))))) => (eats T_2 Y1))) (All X, ((fox X) => (animal X))) (fox T_1) (much_smaller T_1 T_2) (All X, (All Y, (((wolf X) /\ ((fox Y) \/ (grain Y))) => (-. (eats X Y))))) (wolf T_2) ### All 46 % 0.40/0.62 48. (bird T_3) (-. (bird T_3)) ### Axiom % 0.40/0.62 49. (-. (animal T_3)) (animal T_3) ### Axiom % 0.40/0.62 50. ((bird T_3) => (animal T_3)) (-. (animal T_3)) (bird T_3) ### Imply 48 49 % 0.40/0.62 51. (All X, ((bird X) => (animal X))) (bird T_3) (-. (animal T_3)) ### All 50 % 0.40/0.62 52. (plant T_6) (-. (plant T_6)) ### Axiom % 0.40/0.62 53. (much_smaller T_3 T_1) (-. (much_smaller T_3 T_1)) ### Axiom % 0.40/0.62 54. (plant T_6) (-. (plant T_6)) ### Axiom % 0.40/0.62 55. (eats T_3 T_6) (-. (eats T_3 T_6)) ### Axiom % 0.40/0.62 56. (-. ((plant T_6) /\ (eats T_3 T_6))) (eats T_3 T_6) (plant T_6) ### NotAnd 54 55 % 0.40/0.62 57. (-. (Ex Y, ((plant Y) /\ (eats T_3 Y)))) (plant T_6) (eats T_3 T_6) ### NotExists 56 % 0.40/0.62 58. (grain T_4) (-. (grain T_4)) ### Axiom % 0.40/0.62 59. (grain T_4) (-. (grain T_4)) ### Axiom % 0.40/0.62 60. (-. (plant T_4)) (plant T_4) ### Axiom % 0.40/0.62 61. ((grain T_4) => (plant T_4)) (-. (plant T_4)) (grain T_4) ### Imply 59 60 % 0.40/0.62 62. (All X1, ((grain X1) => (plant X1))) (grain T_4) (-. (plant T_4)) ### All 61 % 0.40/0.62 63. (-. (eats T_3 T_4)) (eats T_3 T_4) ### Axiom % 0.40/0.62 64. ((plant T_4) => (eats T_3 T_4)) (-. (eats T_3 T_4)) (grain T_4) (All X1, ((grain X1) => (plant X1))) ### Imply 62 63 % 0.40/0.62 65. (All Y, ((plant Y) => (eats T_3 Y))) (All X1, ((grain X1) => (plant X1))) (grain T_4) (-. (eats T_3 T_4)) ### All 64 % 0.40/0.62 66. (eats T_1 T_3) (-. (eats T_1 T_3)) ### Axiom % 0.40/0.62 67. (-. ((grain T_4) /\ ((eats T_3 T_4) /\ (eats T_1 T_3)))) (eats T_1 T_3) (All X1, ((grain X1) => (plant X1))) (All Y, ((plant Y) => (eats T_3 Y))) (grain T_4) ### DisjTree 58 65 66 % 0.40/0.62 68. (-. (Ex Z, ((grain Z) /\ ((eats T_3 Z) /\ (eats T_1 T_3))))) (grain T_4) (All Y, ((plant Y) => (eats T_3 Y))) (All X1, ((grain X1) => (plant X1))) (eats T_1 T_3) ### NotExists 67 % 0.40/0.62 69. (-. ((animal T_1) /\ ((animal T_3) /\ (Ex Z, ((grain Z) /\ ((eats T_3 Z) /\ (eats T_1 T_3))))))) (eats T_1 T_3) (All X1, ((grain X1) => (plant X1))) (All Y, ((plant Y) => (eats T_3 Y))) (grain T_4) (bird T_3) (All X, ((bird X) => (animal X))) (fox T_1) (All X, ((fox X) => (animal X))) ### DisjTree 30 51 68 % 0.40/0.62 70. (-. (Ex Y, ((animal T_1) /\ ((animal Y) /\ (Ex Z, ((grain Z) /\ ((eats Y Z) /\ (eats T_1 Y)))))))) (All X, ((fox X) => (animal X))) (fox T_1) (All X, ((bird X) => (animal X))) (bird T_3) (grain T_4) (All Y, ((plant Y) => (eats T_3 Y))) (All X1, ((grain X1) => (plant X1))) (eats T_1 T_3) ### NotExists 69 % 0.40/0.62 71. (-. (Ex X, (Ex Y, ((animal X) /\ ((animal Y) /\ (Ex Z, ((grain Z) /\ ((eats Y Z) /\ (eats X Y))))))))) (eats T_1 T_3) (All X1, ((grain X1) => (plant X1))) (All Y, ((plant Y) => (eats T_3 Y))) (grain T_4) (bird T_3) (All X, ((bird X) => (animal X))) (fox T_1) (All X, ((fox X) => (animal X))) ### NotExists 70 % 0.40/0.62 72. (((animal T_3) /\ ((much_smaller T_3 T_1) /\ (Ex Y, ((plant Y) /\ (eats T_3 Y))))) => (eats T_1 T_3)) (All X, ((fox X) => (animal X))) (fox T_1) (grain T_4) (All Y, ((plant Y) => (eats T_3 Y))) (All X1, ((grain X1) => (plant X1))) (-. (Ex X, (Ex Y, ((animal X) /\ ((animal Y) /\ (Ex Z, ((grain Z) /\ ((eats Y Z) /\ (eats X Y))))))))) (eats T_3 T_6) (plant T_6) (much_smaller T_3 T_1) (bird T_3) (All X, ((bird X) => (animal X))) ### DisjTree 51 53 57 71 % 0.40/0.62 73. (All Y1, (((animal Y1) /\ ((much_smaller Y1 T_1) /\ (Ex Z, ((plant Z) /\ (eats Y1 Z))))) => (eats T_1 Y1))) (All X, ((bird X) => (animal X))) (bird T_3) (much_smaller T_3 T_1) (plant T_6) (eats T_3 T_6) (-. (Ex X, (Ex Y, ((animal X) /\ ((animal Y) /\ (Ex Z, ((grain Z) /\ ((eats Y Z) /\ (eats X Y))))))))) (All X1, ((grain X1) => (plant X1))) (All Y, ((plant Y) => (eats T_3 Y))) (grain T_4) (fox T_1) (All X, ((fox X) => (animal X))) ### All 72 % 0.47/0.63 74. ((plant T_6) => (eats T_3 T_6)) (All X, ((fox X) => (animal X))) (fox T_1) (grain T_4) (All Y, ((plant Y) => (eats T_3 Y))) (All X1, ((grain X1) => (plant X1))) (-. (Ex X, (Ex Y, ((animal X) /\ ((animal Y) /\ (Ex Z, ((grain Z) /\ ((eats Y Z) /\ (eats X Y))))))))) (much_smaller T_3 T_1) (bird T_3) (All X, ((bird X) => (animal X))) (All Y1, (((animal Y1) /\ ((much_smaller Y1 T_1) /\ (Ex Z, ((plant Z) /\ (eats Y1 Z))))) => (eats T_1 Y1))) (plant T_6) ### Imply 52 73 % 0.47/0.63 75. (plant T_6) (All Y1, (((animal Y1) /\ ((much_smaller Y1 T_1) /\ (Ex Z, ((plant Z) /\ (eats Y1 Z))))) => (eats T_1 Y1))) (All X, ((bird X) => (animal X))) (bird T_3) (much_smaller T_3 T_1) (-. (Ex X, (Ex Y, ((animal X) /\ ((animal Y) /\ (Ex Z, ((grain Z) /\ ((eats Y Z) /\ (eats X Y))))))))) (All X1, ((grain X1) => (plant X1))) (All Y, ((plant Y) => (eats T_3 Y))) (grain T_4) (fox T_1) (All X, ((fox X) => (animal X))) ### All 74 % 0.47/0.63 76. (snail T_5) (-. (snail T_5)) ### Axiom % 0.47/0.63 77. (animal T_5) (-. (animal T_5)) ### Axiom % 0.47/0.63 78. (much_smaller T_5 T_3) (-. (much_smaller T_5 T_3)) ### Axiom % 0.47/0.63 79. (snail T_5) (-. (snail T_5)) ### Axiom % 0.47/0.63 80. (-. ((caterpillar T_5) \/ (snail T_5))) (snail T_5) ### NotOr 79 % 0.47/0.63 81. (-. (Ex Z, ((plant Z) /\ (eats T_5 Z)))) (Ex Z, ((plant Z) /\ (eats T_5 Z))) ### Axiom % 0.47/0.63 82. (((caterpillar T_5) \/ (snail T_5)) => (Ex Z, ((plant Z) /\ (eats T_5 Z)))) (-. (Ex Z, ((plant Z) /\ (eats T_5 Z)))) (snail T_5) ### Imply 80 81 % 0.47/0.63 83. (All X, (((caterpillar X) \/ (snail X)) => (Ex Y, ((plant Y) /\ (eats X Y))))) (snail T_5) (-. (Ex Z, ((plant Z) /\ (eats T_5 Z)))) ### All 82 % 0.47/0.63 84. (bird T_3) (-. (bird T_3)) ### Axiom % 0.47/0.63 85. (snail T_5) (-. (snail T_5)) ### Axiom % 0.47/0.63 86. (eats T_3 T_5) (-. (eats T_3 T_5)) ### Axiom % 0.47/0.63 87. (((bird T_3) /\ (snail T_5)) => (-. (eats T_3 T_5))) (eats T_3 T_5) (snail T_5) (bird T_3) ### DisjTree 84 85 86 % 0.47/0.63 88. (All Y, (((bird T_3) /\ (snail Y)) => (-. (eats T_3 Y)))) (bird T_3) (snail T_5) (eats T_3 T_5) ### All 87 % 0.47/0.63 89. (((animal T_5) /\ ((much_smaller T_5 T_3) /\ (Ex Z, ((plant Z) /\ (eats T_5 Z))))) => (eats T_3 T_5)) (bird T_3) (All Y, (((bird T_3) /\ (snail Y)) => (-. (eats T_3 Y)))) (snail T_5) (All X, (((caterpillar X) \/ (snail X)) => (Ex Y, ((plant Y) /\ (eats X Y))))) (much_smaller T_5 T_3) (animal T_5) ### DisjTree 77 78 83 88 % 0.47/0.63 90. (All Y1, (((animal Y1) /\ ((much_smaller Y1 T_3) /\ (Ex Z, ((plant Z) /\ (eats Y1 Z))))) => (eats T_3 Y1))) (animal T_5) (much_smaller T_5 T_3) (All X, (((caterpillar X) \/ (snail X)) => (Ex Y, ((plant Y) /\ (eats X Y))))) (snail T_5) (All Y, (((bird T_3) /\ (snail Y)) => (-. (eats T_3 Y)))) (bird T_3) ### All 89 % 0.47/0.63 91. ((snail T_5) => (animal T_5)) (bird T_3) (All Y, (((bird T_3) /\ (snail Y)) => (-. (eats T_3 Y)))) (All X, (((caterpillar X) \/ (snail X)) => (Ex Y, ((plant Y) /\ (eats X Y))))) (much_smaller T_5 T_3) (All Y1, (((animal Y1) /\ ((much_smaller Y1 T_3) /\ (Ex Z, ((plant Z) /\ (eats Y1 Z))))) => (eats T_3 Y1))) (snail T_5) ### Imply 76 90 % 0.47/0.63 92. (All X, ((snail X) => (animal X))) (snail T_5) (All Y1, (((animal Y1) /\ ((much_smaller Y1 T_3) /\ (Ex Z, ((plant Z) /\ (eats Y1 Z))))) => (eats T_3 Y1))) (much_smaller T_5 T_3) (All X, (((caterpillar X) \/ (snail X)) => (Ex Y, ((plant Y) /\ (eats X Y))))) (All Y, (((bird T_3) /\ (snail Y)) => (-. (eats T_3 Y)))) (bird T_3) ### All 91 % 0.47/0.63 93. (All X, (All Y, (((bird X) /\ (snail Y)) => (-. (eats X Y))))) (bird T_3) (All X, (((caterpillar X) \/ (snail X)) => (Ex Y, ((plant Y) /\ (eats X Y))))) (much_smaller T_5 T_3) (All Y1, (((animal Y1) /\ ((much_smaller Y1 T_3) /\ (Ex Z, ((plant Z) /\ (eats Y1 Z))))) => (eats T_3 Y1))) (snail T_5) (All X, ((snail X) => (animal X))) ### All 92 % 0.47/0.63 94. ((animal T_3) => ((All Y, ((plant Y) => (eats T_3 Y))) \/ (All Y1, (((animal Y1) /\ ((much_smaller Y1 T_3) /\ (Ex Z, ((plant Z) /\ (eats Y1 Z))))) => (eats T_3 Y1))))) (All X, ((snail X) => (animal X))) (snail T_5) (much_smaller T_5 T_3) (All X, (((caterpillar X) \/ (snail X)) => (Ex Y, ((plant Y) /\ (eats X Y))))) (All X, (All Y, (((bird X) /\ (snail Y)) => (-. (eats X Y))))) (All X, ((fox X) => (animal X))) (fox T_1) (grain T_4) (All X1, ((grain X1) => (plant X1))) (-. (Ex X, (Ex Y, ((animal X) /\ ((animal Y) /\ (Ex Z, ((grain Z) /\ ((eats Y Z) /\ (eats X Y))))))))) (much_smaller T_3 T_1) (All Y1, (((animal Y1) /\ ((much_smaller Y1 T_1) /\ (Ex Z, ((plant Z) /\ (eats Y1 Z))))) => (eats T_1 Y1))) (plant T_6) (bird T_3) (All X, ((bird X) => (animal X))) ### DisjTree 51 75 93 % 0.47/0.63 95. (All X, ((animal X) => ((All Y, ((plant Y) => (eats X Y))) \/ (All Y1, (((animal Y1) /\ ((much_smaller Y1 X) /\ (Ex Z, ((plant Z) /\ (eats Y1 Z))))) => (eats X Y1)))))) (All X, ((bird X) => (animal X))) (bird T_3) (plant T_6) (All Y1, (((animal Y1) /\ ((much_smaller Y1 T_1) /\ (Ex Z, ((plant Z) /\ (eats Y1 Z))))) => (eats T_1 Y1))) (much_smaller T_3 T_1) (-. (Ex X, (Ex Y, ((animal X) /\ ((animal Y) /\ (Ex Z, ((grain Z) /\ ((eats Y Z) /\ (eats X Y))))))))) (All X1, ((grain X1) => (plant X1))) (grain T_4) (fox T_1) (All X, ((fox X) => (animal X))) (All X, (All Y, (((bird X) /\ (snail Y)) => (-. (eats X Y))))) (All X, (((caterpillar X) \/ (snail X)) => (Ex Y, ((plant Y) /\ (eats X Y))))) (much_smaller T_5 T_3) (snail T_5) (All X, ((snail X) => (animal X))) ### All 94 % 0.47/0.63 96. ((animal T_1) => ((All Y, ((plant Y) => (eats T_1 Y))) \/ (All Y1, (((animal Y1) /\ ((much_smaller Y1 T_1) /\ (Ex Z, ((plant Z) /\ (eats Y1 Z))))) => (eats T_1 Y1))))) (All X, ((snail X) => (animal X))) (snail T_5) (much_smaller T_5 T_3) (All X, (((caterpillar X) \/ (snail X)) => (Ex Y, ((plant Y) /\ (eats X Y))))) (All X, (All Y, (((bird X) /\ (snail Y)) => (-. (eats X Y))))) (grain T_4) (All X1, ((grain X1) => (plant X1))) (-. (Ex X, (Ex Y, ((animal X) /\ ((animal Y) /\ (Ex Z, ((grain Z) /\ ((eats Y Z) /\ (eats X Y))))))))) (much_smaller T_3 T_1) (bird T_3) (All X, ((bird X) => (animal X))) (All X, ((animal X) => ((All Y, ((plant Y) => (eats X Y))) \/ (All Y1, (((animal Y1) /\ ((much_smaller Y1 X) /\ (Ex Z, ((plant Z) /\ (eats Y1 Z))))) => (eats X Y1)))))) (wolf T_2) (All X, (All Y, (((wolf X) /\ ((fox Y) \/ (grain Y))) => (-. (eats X Y))))) (much_smaller T_1 T_2) (All Y1, (((animal Y1) /\ ((much_smaller Y1 T_2) /\ (Ex Z, ((plant Z) /\ (eats Y1 Z))))) => (eats T_2 Y1))) (plant T_6) (fox T_1) (All X, ((fox X) => (animal X))) ### DisjTree 30 47 95 % 0.47/0.63 97. (All X, ((fox X) => (animal X))) (fox T_1) (plant T_6) (All Y1, (((animal Y1) /\ ((much_smaller Y1 T_2) /\ (Ex Z, ((plant Z) /\ (eats Y1 Z))))) => (eats T_2 Y1))) (much_smaller T_1 T_2) (All X, (All Y, (((wolf X) /\ ((fox Y) \/ (grain Y))) => (-. (eats X Y))))) (wolf T_2) (All X, ((animal X) => ((All Y, ((plant Y) => (eats X Y))) \/ (All Y1, (((animal Y1) /\ ((much_smaller Y1 X) /\ (Ex Z, ((plant Z) /\ (eats Y1 Z))))) => (eats X Y1)))))) (All X, ((bird X) => (animal X))) (bird T_3) (much_smaller T_3 T_1) (-. (Ex X, (Ex Y, ((animal X) /\ ((animal Y) /\ (Ex Z, ((grain Z) /\ ((eats Y Z) /\ (eats X Y))))))))) (All X1, ((grain X1) => (plant X1))) (grain T_4) (All X, (All Y, (((bird X) /\ (snail Y)) => (-. (eats X Y))))) (All X, (((caterpillar X) \/ (snail X)) => (Ex Y, ((plant Y) /\ (eats X Y))))) (much_smaller T_5 T_3) (snail T_5) (All X, ((snail X) => (animal X))) ### All 96 % 0.47/0.63 98. (((bird T_3) /\ ((snail T_5) \/ (caterpillar T_5))) => (much_smaller T_5 T_3)) (All X, ((snail X) => (animal X))) (All X, (((caterpillar X) \/ (snail X)) => (Ex Y, ((plant Y) /\ (eats X Y))))) (All X, (All Y, (((bird X) /\ (snail Y)) => (-. (eats X Y))))) (grain T_4) (All X1, ((grain X1) => (plant X1))) (-. (Ex X, (Ex Y, ((animal X) /\ ((animal Y) /\ (Ex Z, ((grain Z) /\ ((eats Y Z) /\ (eats X Y))))))))) (much_smaller T_3 T_1) (All X, ((bird X) => (animal X))) (All X, ((animal X) => ((All Y, ((plant Y) => (eats X Y))) \/ (All Y1, (((animal Y1) /\ ((much_smaller Y1 X) /\ (Ex Z, ((plant Z) /\ (eats Y1 Z))))) => (eats X Y1)))))) (wolf T_2) (All X, (All Y, (((wolf X) /\ ((fox Y) \/ (grain Y))) => (-. (eats X Y))))) (much_smaller T_1 T_2) (All Y1, (((animal Y1) /\ ((much_smaller Y1 T_2) /\ (Ex Z, ((plant Z) /\ (eats Y1 Z))))) => (eats T_2 Y1))) (plant T_6) (fox T_1) (All X, ((fox X) => (animal X))) (snail T_5) (bird T_3) ### DisjTree 24 26 97 % 0.47/0.63 99. (All Y, (((bird Y) /\ ((snail T_5) \/ (caterpillar T_5))) => (much_smaller T_5 Y))) (bird T_3) (snail T_5) (All X, ((fox X) => (animal X))) (fox T_1) (plant T_6) (All Y1, (((animal Y1) /\ ((much_smaller Y1 T_2) /\ (Ex Z, ((plant Z) /\ (eats Y1 Z))))) => (eats T_2 Y1))) (much_smaller T_1 T_2) (All X, (All Y, (((wolf X) /\ ((fox Y) \/ (grain Y))) => (-. (eats X Y))))) (wolf T_2) (All X, ((animal X) => ((All Y, ((plant Y) => (eats X Y))) \/ (All Y1, (((animal Y1) /\ ((much_smaller Y1 X) /\ (Ex Z, ((plant Z) /\ (eats Y1 Z))))) => (eats X Y1)))))) (All X, ((bird X) => (animal X))) (much_smaller T_3 T_1) (-. (Ex X, (Ex Y, ((animal X) /\ ((animal Y) /\ (Ex Z, ((grain Z) /\ ((eats Y Z) /\ (eats X Y))))))))) (All X1, ((grain X1) => (plant X1))) (grain T_4) (All X, (All Y, (((bird X) /\ (snail Y)) => (-. (eats X Y))))) (All X, (((caterpillar X) \/ (snail X)) => (Ex Y, ((plant Y) /\ (eats X Y))))) (All X, ((snail X) => (animal X))) ### All 98 % 0.47/0.63 100. ((animal T_2) => ((All Y, ((plant Y) => (eats T_2 Y))) \/ (All Y1, (((animal Y1) /\ ((much_smaller Y1 T_2) /\ (Ex Z, ((plant Z) /\ (eats Y1 Z))))) => (eats T_2 Y1))))) (All X, ((snail X) => (animal X))) (All X, (((caterpillar X) \/ (snail X)) => (Ex Y, ((plant Y) /\ (eats X Y))))) (All X, (All Y, (((bird X) /\ (snail Y)) => (-. (eats X Y))))) (-. (Ex X, (Ex Y, ((animal X) /\ ((animal Y) /\ (Ex Z, ((grain Z) /\ ((eats Y Z) /\ (eats X Y))))))))) (much_smaller T_3 T_1) (All X, ((bird X) => (animal X))) (All X, ((animal X) => ((All Y, ((plant Y) => (eats X Y))) \/ (All Y1, (((animal Y1) /\ ((much_smaller Y1 X) /\ (Ex Z, ((plant Z) /\ (eats Y1 Z))))) => (eats X Y1)))))) (much_smaller T_1 T_2) (plant T_6) (fox T_1) (All X, ((fox X) => (animal X))) (snail T_5) (bird T_3) (All Y, (((bird Y) /\ ((snail T_5) \/ (caterpillar T_5))) => (much_smaller T_5 Y))) (All X1, ((grain X1) => (plant X1))) (grain T_4) (All X, (All Y, (((wolf X) /\ ((fox Y) \/ (grain Y))) => (-. (eats X Y))))) (wolf T_2) (All X, ((wolf X) => (animal X))) ### DisjTree 10 23 99 % 0.47/0.63 101. (All X, ((wolf X) => (animal X))) (wolf T_2) (All X, (All Y, (((wolf X) /\ ((fox Y) \/ (grain Y))) => (-. (eats X Y))))) (grain T_4) (All X1, ((grain X1) => (plant X1))) (All Y, (((bird Y) /\ ((snail T_5) \/ (caterpillar T_5))) => (much_smaller T_5 Y))) (bird T_3) (snail T_5) (All X, ((fox X) => (animal X))) (fox T_1) (plant T_6) (much_smaller T_1 T_2) (All X, ((animal X) => ((All Y, ((plant Y) => (eats X Y))) \/ (All Y1, (((animal Y1) /\ ((much_smaller Y1 X) /\ (Ex Z, ((plant Z) /\ (eats Y1 Z))))) => (eats X Y1)))))) (All X, ((bird X) => (animal X))) (much_smaller T_3 T_1) (-. (Ex X, (Ex Y, ((animal X) /\ ((animal Y) /\ (Ex Z, ((grain Z) /\ ((eats Y Z) /\ (eats X Y))))))))) (All X, (All Y, (((bird X) /\ (snail Y)) => (-. (eats X Y))))) (All X, (((caterpillar X) \/ (snail X)) => (Ex Y, ((plant Y) /\ (eats X Y))))) (All X, ((snail X) => (animal X))) ### All 100 % 0.47/0.63 102. (((bird T_3) /\ (fox T_1)) => (much_smaller T_3 T_1)) (All X, ((snail X) => (animal X))) (All X, (((caterpillar X) \/ (snail X)) => (Ex Y, ((plant Y) /\ (eats X Y))))) (All X, (All Y, (((bird X) /\ (snail Y)) => (-. (eats X Y))))) (-. (Ex X, (Ex Y, ((animal X) /\ ((animal Y) /\ (Ex Z, ((grain Z) /\ ((eats Y Z) /\ (eats X Y))))))))) (All X, ((bird X) => (animal X))) (All X, ((animal X) => ((All Y, ((plant Y) => (eats X Y))) \/ (All Y1, (((animal Y1) /\ ((much_smaller Y1 X) /\ (Ex Z, ((plant Z) /\ (eats Y1 Z))))) => (eats X Y1)))))) (much_smaller T_1 T_2) (plant T_6) (All X, ((fox X) => (animal X))) (snail T_5) (All Y, (((bird Y) /\ ((snail T_5) \/ (caterpillar T_5))) => (much_smaller T_5 Y))) (All X1, ((grain X1) => (plant X1))) (grain T_4) (All X, (All Y, (((wolf X) /\ ((fox Y) \/ (grain Y))) => (-. (eats X Y))))) (wolf T_2) (All X, ((wolf X) => (animal X))) (fox T_1) (bird T_3) ### DisjTree 5 6 101 % 0.47/0.63 103. (All Y, (((bird T_3) /\ (fox Y)) => (much_smaller T_3 Y))) (bird T_3) (fox T_1) (All X, ((wolf X) => (animal X))) (wolf T_2) (All X, (All Y, (((wolf X) /\ ((fox Y) \/ (grain Y))) => (-. (eats X Y))))) (grain T_4) (All X1, ((grain X1) => (plant X1))) (All Y, (((bird Y) /\ ((snail T_5) \/ (caterpillar T_5))) => (much_smaller T_5 Y))) (snail T_5) (All X, ((fox X) => (animal X))) (plant T_6) (much_smaller T_1 T_2) (All X, ((animal X) => ((All Y, ((plant Y) => (eats X Y))) \/ (All Y1, (((animal Y1) /\ ((much_smaller Y1 X) /\ (Ex Z, ((plant Z) /\ (eats Y1 Z))))) => (eats X Y1)))))) (All X, ((bird X) => (animal X))) (-. (Ex X, (Ex Y, ((animal X) /\ ((animal Y) /\ (Ex Z, ((grain Z) /\ ((eats Y Z) /\ (eats X Y))))))))) (All X, (All Y, (((bird X) /\ (snail Y)) => (-. (eats X Y))))) (All X, (((caterpillar X) \/ (snail X)) => (Ex Y, ((plant Y) /\ (eats X Y))))) (All X, ((snail X) => (animal X))) ### All 102 % 0.47/0.63 104. (((fox T_1) /\ (wolf T_2)) => (much_smaller T_1 T_2)) (All X, ((snail X) => (animal X))) (All X, (((caterpillar X) \/ (snail X)) => (Ex Y, ((plant Y) /\ (eats X Y))))) (All X, (All Y, (((bird X) /\ (snail Y)) => (-. (eats X Y))))) (-. (Ex X, (Ex Y, ((animal X) /\ ((animal Y) /\ (Ex Z, ((grain Z) /\ ((eats Y Z) /\ (eats X Y))))))))) (All X, ((bird X) => (animal X))) (All X, ((animal X) => ((All Y, ((plant Y) => (eats X Y))) \/ (All Y1, (((animal Y1) /\ ((much_smaller Y1 X) /\ (Ex Z, ((plant Z) /\ (eats Y1 Z))))) => (eats X Y1)))))) (plant T_6) (All X, ((fox X) => (animal X))) (snail T_5) (All Y, (((bird Y) /\ ((snail T_5) \/ (caterpillar T_5))) => (much_smaller T_5 Y))) (All X1, ((grain X1) => (plant X1))) (grain T_4) (All X, (All Y, (((wolf X) /\ ((fox Y) \/ (grain Y))) => (-. (eats X Y))))) (All X, ((wolf X) => (animal X))) (bird T_3) (All Y, (((bird T_3) /\ (fox Y)) => (much_smaller T_3 Y))) (wolf T_2) (fox T_1) ### DisjTree 3 4 103 % 0.47/0.63 105. (All Y, (((fox T_1) /\ (wolf Y)) => (much_smaller T_1 Y))) (fox T_1) (wolf T_2) (All Y, (((bird T_3) /\ (fox Y)) => (much_smaller T_3 Y))) (bird T_3) (All X, ((wolf X) => (animal X))) (All X, (All Y, (((wolf X) /\ ((fox Y) \/ (grain Y))) => (-. (eats X Y))))) (grain T_4) (All X1, ((grain X1) => (plant X1))) (All Y, (((bird Y) /\ ((snail T_5) \/ (caterpillar T_5))) => (much_smaller T_5 Y))) (snail T_5) (All X, ((fox X) => (animal X))) (plant T_6) (All X, ((animal X) => ((All Y, ((plant Y) => (eats X Y))) \/ (All Y1, (((animal Y1) /\ ((much_smaller Y1 X) /\ (Ex Z, ((plant Z) /\ (eats Y1 Z))))) => (eats X Y1)))))) (All X, ((bird X) => (animal X))) (-. (Ex X, (Ex Y, ((animal X) /\ ((animal Y) /\ (Ex Z, ((grain Z) /\ ((eats Y Z) /\ (eats X Y))))))))) (All X, (All Y, (((bird X) /\ (snail Y)) => (-. (eats X Y))))) (All X, (((caterpillar X) \/ (snail X)) => (Ex Y, ((plant Y) /\ (eats X Y))))) (All X, ((snail X) => (animal X))) ### All 104 % 0.47/0.63 106. ((plant T_6) /\ (eats T_0 T_6)) (All X, ((snail X) => (animal X))) (All X, (((caterpillar X) \/ (snail X)) => (Ex Y, ((plant Y) /\ (eats X Y))))) (All X, (All Y, (((bird X) /\ (snail Y)) => (-. (eats X Y))))) (-. (Ex X, (Ex Y, ((animal X) /\ ((animal Y) /\ (Ex Z, ((grain Z) /\ ((eats Y Z) /\ (eats X Y))))))))) (All X, ((bird X) => (animal X))) (All X, ((animal X) => ((All Y, ((plant Y) => (eats X Y))) \/ (All Y1, (((animal Y1) /\ ((much_smaller Y1 X) /\ (Ex Z, ((plant Z) /\ (eats Y1 Z))))) => (eats X Y1)))))) (All X, ((fox X) => (animal X))) (snail T_5) (All Y, (((bird Y) /\ ((snail T_5) \/ (caterpillar T_5))) => (much_smaller T_5 Y))) (All X1, ((grain X1) => (plant X1))) (grain T_4) (All X, (All Y, (((wolf X) /\ ((fox Y) \/ (grain Y))) => (-. (eats X Y))))) (All X, ((wolf X) => (animal X))) (bird T_3) (All Y, (((bird T_3) /\ (fox Y)) => (much_smaller T_3 Y))) (wolf T_2) (fox T_1) (All Y, (((fox T_1) /\ (wolf Y)) => (much_smaller T_1 Y))) ### And 105 % 0.47/0.63 107. (Ex Z, ((plant Z) /\ (eats T_0 Z))) (All Y, (((fox T_1) /\ (wolf Y)) => (much_smaller T_1 Y))) (fox T_1) (wolf T_2) (All Y, (((bird T_3) /\ (fox Y)) => (much_smaller T_3 Y))) (bird T_3) (All X, ((wolf X) => (animal X))) (All X, (All Y, (((wolf X) /\ ((fox Y) \/ (grain Y))) => (-. (eats X Y))))) (grain T_4) (All X1, ((grain X1) => (plant X1))) (All Y, (((bird Y) /\ ((snail T_5) \/ (caterpillar T_5))) => (much_smaller T_5 Y))) (snail T_5) (All X, ((fox X) => (animal X))) (All X, ((animal X) => ((All Y, ((plant Y) => (eats X Y))) \/ (All Y1, (((animal Y1) /\ ((much_smaller Y1 X) /\ (Ex Z, ((plant Z) /\ (eats Y1 Z))))) => (eats X Y1)))))) (All X, ((bird X) => (animal X))) (-. (Ex X, (Ex Y, ((animal X) /\ ((animal Y) /\ (Ex Z, ((grain Z) /\ ((eats Y Z) /\ (eats X Y))))))))) (All X, (All Y, (((bird X) /\ (snail Y)) => (-. (eats X Y))))) (All X, (((caterpillar X) \/ (snail X)) => (Ex Y, ((plant Y) /\ (eats X Y))))) (All X, ((snail X) => (animal X))) ### Exists 106 % 0.47/0.63 108. (((caterpillar T_0) \/ (snail T_0)) => (Ex Z, ((plant Z) /\ (eats T_0 Z)))) (All X, ((snail X) => (animal X))) (All X, (((caterpillar X) \/ (snail X)) => (Ex Y, ((plant Y) /\ (eats X Y))))) (All X, (All Y, (((bird X) /\ (snail Y)) => (-. (eats X Y))))) (-. (Ex X, (Ex Y, ((animal X) /\ ((animal Y) /\ (Ex Z, ((grain Z) /\ ((eats Y Z) /\ (eats X Y))))))))) (All X, ((bird X) => (animal X))) (All X, ((animal X) => ((All Y, ((plant Y) => (eats X Y))) \/ (All Y1, (((animal Y1) /\ ((much_smaller Y1 X) /\ (Ex Z, ((plant Z) /\ (eats Y1 Z))))) => (eats X Y1)))))) (All X, ((fox X) => (animal X))) (snail T_5) (All Y, (((bird Y) /\ ((snail T_5) \/ (caterpillar T_5))) => (much_smaller T_5 Y))) (All X1, ((grain X1) => (plant X1))) (grain T_4) (All X, (All Y, (((wolf X) /\ ((fox Y) \/ (grain Y))) => (-. (eats X Y))))) (All X, ((wolf X) => (animal X))) (bird T_3) (All Y, (((bird T_3) /\ (fox Y)) => (much_smaller T_3 Y))) (wolf T_2) (fox T_1) (All Y, (((fox T_1) /\ (wolf Y)) => (much_smaller T_1 Y))) (caterpillar T_0) ### Imply 2 107 % 0.47/0.63 109. (caterpillar T_0) (All Y, (((fox T_1) /\ (wolf Y)) => (much_smaller T_1 Y))) (fox T_1) (wolf T_2) (All Y, (((bird T_3) /\ (fox Y)) => (much_smaller T_3 Y))) (bird T_3) (All X, ((wolf X) => (animal X))) (All X, (All Y, (((wolf X) /\ ((fox Y) \/ (grain Y))) => (-. (eats X Y))))) (grain T_4) (All X1, ((grain X1) => (plant X1))) (All Y, (((bird Y) /\ ((snail T_5) \/ (caterpillar T_5))) => (much_smaller T_5 Y))) (snail T_5) (All X, ((fox X) => (animal X))) (All X, ((animal X) => ((All Y, ((plant Y) => (eats X Y))) \/ (All Y1, (((animal Y1) /\ ((much_smaller Y1 X) /\ (Ex Z, ((plant Z) /\ (eats Y1 Z))))) => (eats X Y1)))))) (All X, ((bird X) => (animal X))) (-. (Ex X, (Ex Y, ((animal X) /\ ((animal Y) /\ (Ex Z, ((grain Z) /\ ((eats Y Z) /\ (eats X Y))))))))) (All X, (All Y, (((bird X) /\ (snail Y)) => (-. (eats X Y))))) (All X, (((caterpillar X) \/ (snail X)) => (Ex Y, ((plant Y) /\ (eats X Y))))) (All X, ((snail X) => (animal X))) ### All 108 % 0.47/0.63 110. (All X, (All Y, (((bird Y) /\ ((snail X) \/ (caterpillar X))) => (much_smaller X Y)))) (All X, ((snail X) => (animal X))) (All X, (((caterpillar X) \/ (snail X)) => (Ex Y, ((plant Y) /\ (eats X Y))))) (All X, (All Y, (((bird X) /\ (snail Y)) => (-. (eats X Y))))) (-. (Ex X, (Ex Y, ((animal X) /\ ((animal Y) /\ (Ex Z, ((grain Z) /\ ((eats Y Z) /\ (eats X Y))))))))) (All X, ((bird X) => (animal X))) (All X, ((animal X) => ((All Y, ((plant Y) => (eats X Y))) \/ (All Y1, (((animal Y1) /\ ((much_smaller Y1 X) /\ (Ex Z, ((plant Z) /\ (eats Y1 Z))))) => (eats X Y1)))))) (All X, ((fox X) => (animal X))) (snail T_5) (All X1, ((grain X1) => (plant X1))) (grain T_4) (All X, (All Y, (((wolf X) /\ ((fox Y) \/ (grain Y))) => (-. (eats X Y))))) (All X, ((wolf X) => (animal X))) (bird T_3) (All Y, (((bird T_3) /\ (fox Y)) => (much_smaller T_3 Y))) (wolf T_2) (fox T_1) (All Y, (((fox T_1) /\ (wolf Y)) => (much_smaller T_1 Y))) (caterpillar T_0) ### All 109 % 0.47/0.63 111. (All X, (All Y, (((bird X) /\ (fox Y)) => (much_smaller X Y)))) (caterpillar T_0) (All Y, (((fox T_1) /\ (wolf Y)) => (much_smaller T_1 Y))) (fox T_1) (wolf T_2) (bird T_3) (All X, ((wolf X) => (animal X))) (All X, (All Y, (((wolf X) /\ ((fox Y) \/ (grain Y))) => (-. (eats X Y))))) (grain T_4) (All X1, ((grain X1) => (plant X1))) (snail T_5) (All X, ((fox X) => (animal X))) (All X, ((animal X) => ((All Y, ((plant Y) => (eats X Y))) \/ (All Y1, (((animal Y1) /\ ((much_smaller Y1 X) /\ (Ex Z, ((plant Z) /\ (eats Y1 Z))))) => (eats X Y1)))))) (All X, ((bird X) => (animal X))) (-. (Ex X, (Ex Y, ((animal X) /\ ((animal Y) /\ (Ex Z, ((grain Z) /\ ((eats Y Z) /\ (eats X Y))))))))) (All X, (All Y, (((bird X) /\ (snail Y)) => (-. (eats X Y))))) (All X, (((caterpillar X) \/ (snail X)) => (Ex Y, ((plant Y) /\ (eats X Y))))) (All X, ((snail X) => (animal X))) (All X, (All Y, (((bird Y) /\ ((snail X) \/ (caterpillar X))) => (much_smaller X Y)))) ### All 110 % 0.47/0.63 112. (All X, (All Y, (((fox X) /\ (wolf Y)) => (much_smaller X Y)))) (All X, (All Y, (((bird Y) /\ ((snail X) \/ (caterpillar X))) => (much_smaller X Y)))) (All X, ((snail X) => (animal X))) (All X, (((caterpillar X) \/ (snail X)) => (Ex Y, ((plant Y) /\ (eats X Y))))) (All X, (All Y, (((bird X) /\ (snail Y)) => (-. (eats X Y))))) (-. (Ex X, (Ex Y, ((animal X) /\ ((animal Y) /\ (Ex Z, ((grain Z) /\ ((eats Y Z) /\ (eats X Y))))))))) (All X, ((bird X) => (animal X))) (All X, ((animal X) => ((All Y, ((plant Y) => (eats X Y))) \/ (All Y1, (((animal Y1) /\ ((much_smaller Y1 X) /\ (Ex Z, ((plant Z) /\ (eats Y1 Z))))) => (eats X Y1)))))) (All X, ((fox X) => (animal X))) (snail T_5) (All X1, ((grain X1) => (plant X1))) (grain T_4) (All X, (All Y, (((wolf X) /\ ((fox Y) \/ (grain Y))) => (-. (eats X Y))))) (All X, ((wolf X) => (animal X))) (bird T_3) (wolf T_2) (fox T_1) (caterpillar T_0) (All X, (All Y, (((bird X) /\ (fox Y)) => (much_smaller X Y)))) ### All 111 % 0.47/0.63 113. (Ex X1, (wolf X1)) (All X, (All Y, (((bird X) /\ (fox Y)) => (much_smaller X Y)))) (caterpillar T_0) (fox T_1) (bird T_3) (All X, ((wolf X) => (animal X))) (All X, (All Y, (((wolf X) /\ ((fox Y) \/ (grain Y))) => (-. (eats X Y))))) (grain T_4) (All X1, ((grain X1) => (plant X1))) (snail T_5) (All X, ((fox X) => (animal X))) (All X, ((animal X) => ((All Y, ((plant Y) => (eats X Y))) \/ (All Y1, (((animal Y1) /\ ((much_smaller Y1 X) /\ (Ex Z, ((plant Z) /\ (eats Y1 Z))))) => (eats X Y1)))))) (All X, ((bird X) => (animal X))) (-. (Ex X, (Ex Y, ((animal X) /\ ((animal Y) /\ (Ex Z, ((grain Z) /\ ((eats Y Z) /\ (eats X Y))))))))) (All X, (All Y, (((bird X) /\ (snail Y)) => (-. (eats X Y))))) (All X, (((caterpillar X) \/ (snail X)) => (Ex Y, ((plant Y) /\ (eats X Y))))) (All X, ((snail X) => (animal X))) (All X, (All Y, (((bird Y) /\ ((snail X) \/ (caterpillar X))) => (much_smaller X Y)))) (All X, (All Y, (((fox X) /\ (wolf Y)) => (much_smaller X Y)))) ### Exists 112 % 0.47/0.63 114. (Ex X1, (fox X1)) (All X, (All Y, (((fox X) /\ (wolf Y)) => (much_smaller X Y)))) (All X, (All Y, (((bird Y) /\ ((snail X) \/ (caterpillar X))) => (much_smaller X Y)))) (All X, ((snail X) => (animal X))) (All X, (((caterpillar X) \/ (snail X)) => (Ex Y, ((plant Y) /\ (eats X Y))))) (All X, (All Y, (((bird X) /\ (snail Y)) => (-. (eats X Y))))) (-. (Ex X, (Ex Y, ((animal X) /\ ((animal Y) /\ (Ex Z, ((grain Z) /\ ((eats Y Z) /\ (eats X Y))))))))) (All X, ((bird X) => (animal X))) (All X, ((animal X) => ((All Y, ((plant Y) => (eats X Y))) \/ (All Y1, (((animal Y1) /\ ((much_smaller Y1 X) /\ (Ex Z, ((plant Z) /\ (eats Y1 Z))))) => (eats X Y1)))))) (All X, ((fox X) => (animal X))) (snail T_5) (All X1, ((grain X1) => (plant X1))) (grain T_4) (All X, (All Y, (((wolf X) /\ ((fox Y) \/ (grain Y))) => (-. (eats X Y))))) (All X, ((wolf X) => (animal X))) (bird T_3) (caterpillar T_0) (All X, (All Y, (((bird X) /\ (fox Y)) => (much_smaller X Y)))) (Ex X1, (wolf X1)) ### Exists 113 % 0.47/0.63 115. (Ex X1, (bird X1)) (Ex X1, (wolf X1)) (All X, (All Y, (((bird X) /\ (fox Y)) => (much_smaller X Y)))) (caterpillar T_0) (All X, ((wolf X) => (animal X))) (All X, (All Y, (((wolf X) /\ ((fox Y) \/ (grain Y))) => (-. (eats X Y))))) (grain T_4) (All X1, ((grain X1) => (plant X1))) (snail T_5) (All X, ((fox X) => (animal X))) (All X, ((animal X) => ((All Y, ((plant Y) => (eats X Y))) \/ (All Y1, (((animal Y1) /\ ((much_smaller Y1 X) /\ (Ex Z, ((plant Z) /\ (eats Y1 Z))))) => (eats X Y1)))))) (All X, ((bird X) => (animal X))) (-. (Ex X, (Ex Y, ((animal X) /\ ((animal Y) /\ (Ex Z, ((grain Z) /\ ((eats Y Z) /\ (eats X Y))))))))) (All X, (All Y, (((bird X) /\ (snail Y)) => (-. (eats X Y))))) (All X, (((caterpillar X) \/ (snail X)) => (Ex Y, ((plant Y) /\ (eats X Y))))) (All X, ((snail X) => (animal X))) (All X, (All Y, (((bird Y) /\ ((snail X) \/ (caterpillar X))) => (much_smaller X Y)))) (All X, (All Y, (((fox X) /\ (wolf Y)) => (much_smaller X Y)))) (Ex X1, (fox X1)) ### Exists 114 % 0.47/0.64 116. (Ex X1, (caterpillar X1)) (Ex X1, (fox X1)) (All X, (All Y, (((fox X) /\ (wolf Y)) => (much_smaller X Y)))) (All X, (All Y, (((bird Y) /\ ((snail X) \/ (caterpillar X))) => (much_smaller X Y)))) (All X, ((snail X) => (animal X))) (All X, (((caterpillar X) \/ (snail X)) => (Ex Y, ((plant Y) /\ (eats X Y))))) (All X, (All Y, (((bird X) /\ (snail Y)) => (-. (eats X Y))))) (-. (Ex X, (Ex Y, ((animal X) /\ ((animal Y) /\ (Ex Z, ((grain Z) /\ ((eats Y Z) /\ (eats X Y))))))))) (All X, ((bird X) => (animal X))) (All X, ((animal X) => ((All Y, ((plant Y) => (eats X Y))) \/ (All Y1, (((animal Y1) /\ ((much_smaller Y1 X) /\ (Ex Z, ((plant Z) /\ (eats Y1 Z))))) => (eats X Y1)))))) (All X, ((fox X) => (animal X))) (snail T_5) (All X1, ((grain X1) => (plant X1))) (grain T_4) (All X, (All Y, (((wolf X) /\ ((fox Y) \/ (grain Y))) => (-. (eats X Y))))) (All X, ((wolf X) => (animal X))) (All X, (All Y, (((bird X) /\ (fox Y)) => (much_smaller X Y)))) (Ex X1, (wolf X1)) (Ex X1, (bird X1)) ### Exists 115 % 0.47/0.64 117. (Ex X1, (snail X1)) (Ex X1, (bird X1)) (Ex X1, (wolf X1)) (All X, (All Y, (((bird X) /\ (fox Y)) => (much_smaller X Y)))) (All X, ((wolf X) => (animal X))) (All X, (All Y, (((wolf X) /\ ((fox Y) \/ (grain Y))) => (-. (eats X Y))))) (grain T_4) (All X1, ((grain X1) => (plant X1))) (All X, ((fox X) => (animal X))) (All X, ((animal X) => ((All Y, ((plant Y) => (eats X Y))) \/ (All Y1, (((animal Y1) /\ ((much_smaller Y1 X) /\ (Ex Z, ((plant Z) /\ (eats Y1 Z))))) => (eats X Y1)))))) (All X, ((bird X) => (animal X))) (-. (Ex X, (Ex Y, ((animal X) /\ ((animal Y) /\ (Ex Z, ((grain Z) /\ ((eats Y Z) /\ (eats X Y))))))))) (All X, (All Y, (((bird X) /\ (snail Y)) => (-. (eats X Y))))) (All X, (((caterpillar X) \/ (snail X)) => (Ex Y, ((plant Y) /\ (eats X Y))))) (All X, ((snail X) => (animal X))) (All X, (All Y, (((bird Y) /\ ((snail X) \/ (caterpillar X))) => (much_smaller X Y)))) (All X, (All Y, (((fox X) /\ (wolf Y)) => (much_smaller X Y)))) (Ex X1, (fox X1)) (Ex X1, (caterpillar X1)) ### Exists 116 % 0.47/0.64 118. (Ex X, (grain X)) (Ex X1, (caterpillar X1)) (Ex X1, (fox X1)) (All X, (All Y, (((fox X) /\ (wolf Y)) => (much_smaller X Y)))) (All X, (All Y, (((bird Y) /\ ((snail X) \/ (caterpillar X))) => (much_smaller X Y)))) (All X, ((snail X) => (animal X))) (All X, (((caterpillar X) \/ (snail X)) => (Ex Y, ((plant Y) /\ (eats X Y))))) (All X, (All Y, (((bird X) /\ (snail Y)) => (-. (eats X Y))))) (-. (Ex X, (Ex Y, ((animal X) /\ ((animal Y) /\ (Ex Z, ((grain Z) /\ ((eats Y Z) /\ (eats X Y))))))))) (All X, ((bird X) => (animal X))) (All X, ((animal X) => ((All Y, ((plant Y) => (eats X Y))) \/ (All Y1, (((animal Y1) /\ ((much_smaller Y1 X) /\ (Ex Z, ((plant Z) /\ (eats Y1 Z))))) => (eats X Y1)))))) (All X, ((fox X) => (animal X))) (All X1, ((grain X1) => (plant X1))) (All X, (All Y, (((wolf X) /\ ((fox Y) \/ (grain Y))) => (-. (eats X Y))))) (All X, ((wolf X) => (animal X))) (All X, (All Y, (((bird X) /\ (fox Y)) => (much_smaller X Y)))) (Ex X1, (wolf X1)) (Ex X1, (bird X1)) (Ex X1, (snail X1)) ### Exists 117 % 0.47/0.64 % SZS output end Proof % 0.47/0.64 (* END-PROOF *) %------------------------------------------------------------------------------