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