k = 3 and n = 2. It corresponds to some derivation, say, <(B1,B2),(R1,B3),(R2,B4)> where B1, B2, R1, B3, R2, and B4 are clauses. The attribute here is assumed to be the length of a clause. The first pair (2,2) corresponds to the pair (B1,B2) from the derivation. It indicates that the length of B1 is 2 and the length of B2 is also 2. The second pair (2,1) corresponds to the pair (R1,B3) and it indicates that the length of R1 is 2 and the length of B3 is 1. The last pair (1,1) corresponds to the pair (R2,B4) and it indicates that the length of R2 is 1 and the length of B4 is 1. Note: An n-tuple of clause attributes is similar (but not the same) to the feature vector named by Stephan Schulz, PhD (see E equational theorem prover). References External links CARINE's web site ACM publication E home page Theorem proving software systems