Hello Professor, With the current Knowledge Base of a-f, it seems we are unable to generate BinaryTrees predicates without a MakeTree inside of it and encompassing all other terms. That is, we can only generate Trees such as BinaryTree(MakeTree(0, 0)) or BinaryTree(MakeTree(LeftTree(0), RightTree(0)) and not, say, BinaryTrees(LeftTree(MakeTree(0,0)) because in order to do so, we have to prove that Maketree(0,0) is equal to 0, which is not allowed because of d). That is, f) is what generates BinaryTree with LeftTree or RightTree encompassing all other terms inside the BinaryTree predicate, but we would first need to derive a BinaryTree and a variable equal to 0.