Functional relations for Kochen-Specker proofs Many proofs of the Kochen-Specker theorem use some form of the following argument (from Mermin's "Simple Unified Form for the major No-Hidden-Variables Theorems" )

[I]f some functional relation
  $$
  f(A,B,C,\ldots)=0
  $$
  holds as an operator identity among the observables of a mutually commuting set, then since the results of the simultaneous measurements of $A,B,C,\ldots$ will be one of the sets $a,b,c,\ldots$ of simultaneous eigenvalues of $A,B,C,\ldots$, the results of those measurements must also satisfy
  $$
  f(a,b,c,\ldots)=0
  $$

Parity-type contradictions (e.g., $1=-1$ or $0=1$) are then seen to arise when $a,b,c\ldots$ are assigned values independently of the context in which they are measured.
The only explicit forms of $f$ that I have seen are either (i) $A+B+C+\ldots$ or (ii) $(A)(B)(C)\ldots$ (see e.g., "Generalized Kochen-Specker Theorem" by Asher Peres, where both forms are used).
My question, then, is: are there examples of parity-type proofs where $f$ is, necessarily, not of the above forms (i) or (ii)? For example one could consider $A+(B)(C)\ldots$ etc. Ideally, I'm looking for explicit examples where $f$ is spelled out, but I would also be interested in arguments where a different kind of $f$ is implicitly used.
 A: First, a trivial example that might anger you:
Let $A_i$ be the observables of the Mermin-Peres square, and $a_i$ their non-contextual values. Then $\prod_i A_i = -\mathbb{1}$, but $\prod_i a_i = 1$, contradiction. In this case $f$ is multiplicative. But the same contradiction can be obtained considering $\prod_i A_i+\prod_i A_i = -2\mathbb{1}$ and $\prod_i a_i+\prod_i a_i = 2$, where $f$ is neither multiplicative nor additive.
Now, a more interesting example, that I've found in a paper by Adán Cabello about inequalities for testing state-independent contextuality:
Let $$A = \begin{pmatrix}
Z \otimes \mathbb{1} & \mathbb{1} \otimes Z & Z \otimes Z \\
\mathbb{1} \otimes X & X \otimes \mathbb{1} & X \otimes X \\
Z \otimes X & X \otimes Z & Y \otimes Y 
\end{pmatrix}$$
be the Mermim-Peres square. If one ascribes non-contextual values $a_{ij} = \pm 1$ to the observables $A_{ij}$, one can then prove that
$$  a_{11} a_{12} a_{13} + a_{21} a_{22} a_{23} +  a_{31} a_{32} a_{33} \\+ a_{11} a_{21} a_{31} + a_{12} a_{22} a_{32} - a_{13} a_{23} a_{33} \le 4, $$
whereas in quantum mechanics
$$ \langle A_{11} A_{12} A_{13}\rangle + \langle A_{21} A_{22} A_{23}\rangle + \langle A_{31} A_{32} A_{33}\rangle \\+ \langle A_{11} A_{21} A_{31}\rangle + \langle A_{12} A_{22} A_{32}\rangle - \langle A_{13} A_{23} A_{33}\rangle = 6.$$
The proof of the inequality may be done simply by enumerating the $2^9$ possibilities, if you're lazy, or by playing around with the triangle inequality. In either case, we have an $f$ that's not additive nor multiplicative. Of course, in this case the contradiction takes the form of an inequality, instead of a definite value for non-contextual values. 
I guess then that they used always a multiplicative or additive $f$ because it's easier to construct these kind of contradictions, based on parity arguments. But I don't think there's anything fundamental to it.
