Here is a solution of the above problem that I created using the following variables:

- redA/yellowA/greenA: A has a red/yellow/green stamp
- redB/yellowB/greenB: B has a red/yellow/green stamp
- redC/yellowC/greenC: C has a red/yellow/green stamp
- excludeRedA/excludeYellowA: A can exclude the possibility to have a red/yellow stamp
- excludeRedB/excludeYellowB: B can exclude the possibility to have a red/yellow stamp

The important point here is that we have knowledge about what we know like "A has a red stamp" etc. but also what A and B don't know. For this reason, we use variables excludeRedA etc. to express this. Note that it is impossible for anyone to exclude color Green, so we don't use such variables for that color.

However, if one can see two red stamps on the others' heads, it is clear that the own stamp can no longer be a red one since only two red stamps exist. Same with the yellow one. Since A cannot exclude any color, we can conclude that A does neither see two red stamps nor two yellow stamps on B and C's heads. Thus, if redC holds, then excludeRedA must hold.

Now, here is the entire formula:

// each one of A,B,C has a stamp on the head
(redA | yellowA | greenA) &
(redB | yellowB | greenB) &
(redC | yellowC | greenC) &
// and each one has no more than one stamp on the head
(redA -> !greenA & !yellowA) &
(greenA -> !redA & !yellowA) &
(yellowA -> !redA & !greenA) &
(redB -> !greenB & !yellowB) &
(greenB -> !redB & !yellowB) &
(yellowB -> !redB & !greenB) &
(redC -> !greenC & !yellowC) &
(greenC -> !redC & !yellowC) &
(yellowC -> !redC & !greenC) &
// there are only two red stamps
(redA & redB -> !redC) &
(redB & redC -> !redA) &
(redA & redC -> !redB) &
// there are only two yellow stamps
(yellowA & yellowB -> !yellowC) &
(yellowB & yellowC -> !yellowA) &
(yellowA & yellowC -> !yellowB) &
// How to exclude a color is the challenge: A can exclude color red
// if A can see that B and C have red colors (since there are only
// two stamps with red color), but also if C has a red color, and B
// cannot exclude red color. Note that redC & !excludeRedB implies
// redC & !redA & excludeRedA), so that A can exclude color red.
// The same applies to color yellow, but note that there is
// no way to exclude color green.
(redB & redC or redC & !excludeRedB -> excludeRedA) &
(redA & redC or redC & !excludeRedA -> excludeRedB) &
(yellowB & yellowC or yellowC & !excludeYellowB -> excludeYellowA) &
(yellowA & yellowC or yellowC & !excludeYellowA -> excludeYellowB) &
// neither A nor B can exclude a color
!excludeRedA & !excludeYellowA &
!excludeRedB & !excludeYellowB

These are quite many variables so that truth tables are no longer fun. You can of course, reason about the above clauses manually, which will quickly lead to some solution (try it). Instead, I rather computed a ZDD (left hand side) and a BDD (right hand side) for it and got the following results (ZDDs are always good for puzzles):

Since the BDDs show all models of the formula, you can now see that in all models greenC is true, but for A and B, we don't know.

Without BDDs, you can also use the SAT solver to check whether it can prove that one of A, B, C must have one color. Calling the above formula Φ, we check Φ & !greenC for satisfiability (which should not be the case to prove validity of Φ ➞ greenC). And, of course, here is what my SAT solver says (I skipped the listing of the clauses):

computed the following clauses:
redC&redA&redB -> false
redA&__def3 -> false
yellowC&yellowA&yellowB -> false
:
:
--------------------------------------------------
DecisionStack:
--------------------------------------------------
atom redC := False
propagated atoms:
made 0: __def13,excludeRedA,excludeRedB,excludeYellowA,greenC,redC
made 1: __def12,__def15,__def17,__def19,__def23,__def31,__def32,__def33,excludeYellowB,yellowC
DecisionStack:
redC := False
computed assertion clause excludeYellowB -> false by uips ?,__def32,__def33,excludeYellowB,redC,yellowC of 18 :{excludeYellowB -> false}
got assertion clauses
all learnt clauses are already known
--------------------------------------------------
backtracked to the following decisions
DecisionStack:
redC := True (only choice)
computed assertion clause excludeRedB -> false by uips ?,__def24,__def25,excludeRedB,redC of 14 :{excludeRedB -> false}
got assertion clauses
all learnt clauses are already known
--------------------------------------------------
backtracked to the following decisions
DecisionStack:
-------------------------------------------------------
no model
-------------------------------------------------------