The finite ordered tree problem was researched by Harvey Friedman. Friedman defines an ordered tree as a triple (V,≤,<') where (V,≤) is a finite poset with a least element (root) in which the set of predecessors under ≤ of each vertex is linearly ordered by ≤, and where for each vertex, <' is a strict linear ordering on its immediate successors. He also defines the following: * Vertex x ≤* y iff x is to the left of y, or if x ≤ y. * d(v) is the position of v in counting from 1. * |T[0]| = 1 * |T[1]| = 2 * |T[2]| = 4 * |T[3]| = 14 * |T[4]| > 243 * |T[5]| > 2↑↑2295