It’s a good thing that Wo’s tree proof generator doesn’t use exactly the the same rules for trees as I’m using in my intro logic course, or else I wouldn’t be able to in good faith ask the kiddies to build trees for their assignments. (Note that this is because I’m using a strange tree system, not because Wo is.) It is also a good thing that such a generator exists, I might find this useful when I’m trying to quickly decide what’s valid and invalid. Sadly, the tree generator doesn’t seem to have the capacity to recognise loops, so if you’re easily amused you can sit around all day watching it figure out whether everything points to somehing entails everything points to everything.