我正在寻找一个自动定理证明系统，它可以证明这一点：
鳄鱼带走了男人的孩子。人要求鳄鱼不要吃他的孩子。但鳄鱼说：我会把你的孩子还给你，如果你告诉我，我要拿他怎么办。
他的解析解是这样的：
x - 鳄鱼会吃小孩 y - 男人的答案：鳄鱼会吃小孩
~ 表示平等，！表示不，-> 暗示，+ OR；
((x~y)->!x) and ((x XOR y)->x) =
(x! and y +!x and y+!x)(!x!y+x and y+x) =
(!x+!y)(x+!y) = !y;
所以，答案是男人必须说：“你不会吃掉孩子”；
现在，这里列出了很多系统： http ://en.wikipedia.org/wiki/Automated_theorem_proving
我已经尝试了其中的 5-6 个，但无法真正理解我在这里做什么。如何在其中形式化这个定理，以便我可以进入它的第一部分：
((x~y)->!x) and ((x XOR y)->x)
并得到答案
y作为输出。
任何一次建议，哪个系统至少能够自动执行此操作，并给我更多提示？
问候，康斯坦丁。