Footnote
A backward chaining rule to rotate a cube face is fired for a general cube (containing uninstantiated variables). This generates clauses corresponding to each possible rotation which are stored on a database; unification can then be used to rotate specific cubes.