and whatever information stored with them. Attribute sequences (ATS) (An informal definition of) a clause in theorem proving is a statement that can result in a true or false answer depending on the evaluation of its literals. A clause is represented as a disjunction (i.e., OR), conjunction (i.e., AND), set, or multi-set (similar to a set but can contain identical elements) of literals. An example of a clause as a disjunction of literals is: where the symbols and are, respectively, logical or and logical not. The above example states that if Y is wealthy AND smart AND beautiful then X loves Y. It does not say who X and Y are though. Note that the above representation comes from the logical statement: For all Y, X belonging to the domain of human beings: By using some transformation rules of formal logic we produce the disjunction of literals of the example given above. X and Y are variables. wealthy, smart, beautiful, loves are literals. Suppose we substitute the variable X for the constant John and the variable Y for the constant Jane then the above clause will become: A clause attribute is a characteristic of a clause. Some examples of clause attributes are: the number of literals in a clause (i.e., clause length) the number of term symbols in a clause the number of constants in a clause the number of variables in a clause the number of functions in a clause the number of negative literals in a clause the number of positive literals in a clause the number of distinct variables in a clause the maximum depth of any term in all the literals in a clause Example the clause has: a length of 2 because it contains two literals one negative literal which is one positive literal which is Q(a,b,f(x)) two constants which are a and b two variables (x occurs twice) one distinct variable which is x one function which is f maximum term depth of 2 five term symbols which are x, a, b, f, x An attribute sequence is a sequence of k n-tuples of clause attributes that represent a projection of a set of derivations of length k. k and n are strictly positive integers. The set of derivations form the domain and the attribute sequences form the codomain of the mapping between derivations and attribute sequences. Example <(2,2),(2,1),(1,1)> is an attribute sequence where