(set-option :produce-models true)
(set-option :produce-proofs true)
(set-option :produce-unsat-cores true) 

(echo "Solving the graph...")

(declare-const v1r Bool) (declare-const v1g Bool) (declare-const v1b Bool)
(declare-const v2r Bool) (declare-const v2g Bool) (declare-const v2b Bool)
(declare-const v3r Bool) (declare-const v3g Bool) (declare-const v3b Bool)
(declare-const v4r Bool) (declare-const v4g Bool) (declare-const v4b Bool)
(declare-const v5r Bool) (declare-const v5g Bool) (declare-const v5b Bool)
(declare-const v6r Bool) (declare-const v6g Bool) (declare-const v6b Bool)
(declare-const v7r Bool) (declare-const v7g Bool) (declare-const v7b Bool)
(declare-const v8r Bool) (declare-const v8g Bool) (declare-const v8b Bool)
(declare-const v9r Bool) (declare-const v9g Bool) (declare-const v9b Bool)
(declare-const v10r Bool) (declare-const v10g Bool) (declare-const v10b Bool)
(declare-const v11r Bool) (declare-const v11g Bool) (declare-const v11b Bool)
(declare-const v12r Bool) (declare-const v12g Bool) (declare-const v12b Bool)

(assert (xor v1r v1g v1b)) (assert (xor v2r v2g v2b)) (assert (xor v3r v3g v3b))
(assert (xor v4r v4g v4b)) (assert (xor v5r v5g v5b)) (assert (xor v6r v6g v6b))
(assert (xor v7r v7g v7b)) (assert (xor v8r v8g v8b)) (assert (xor v9r v9g v9b))
(assert (xor v10r v10g v10b)) (assert (xor v11r v11g v11b)) (assert (xor v12r v12g v12b))

(assert (!(and 
(or (not v1r) (not v2r))
(or (not v1g) (not v2g))
(or (not v1b) (not v2b))
) :named v1v2))

(assert (!(and 
(or (not v2r) (not v3r))
(or (not v2g) (not v3g))
(or (not v2b) (not v3b))
) :named v2v3))

(assert (!(and 
(or (not v3r) (not v4r))
(or (not v3g) (not v4g))
(or (not v3b) (not v4b))
) :named v3v4))

(assert (!(and 
(or (not v2r) (not v4r))
(or (not v2g) (not v4g))
(or (not v2b) (not v4b))
) :named v2v4))

(assert (!(and 
(or (not v4r) (not v5r))
(or (not v4g) (not v5g))
(or (not v4b) (not v5b))
) :named v4v5))

(assert (!(and 
(or (not v5r) (not v6r))
(or (not v5g) (not v6g))
(or (not v5b) (not v6b))
) :named v5v6))

(assert (!(and 
(or (not v4r) (not v6r))
(or (not v4g) (not v6g))
(or (not v4b) (not v6b))
) :named v4v6))

(assert (!(and 
(or (not v6r) (not v7r))
(or (not v6g) (not v7g))
(or (not v6b) (not v7b))
) :named v6v7))

(assert (!(and 
(or (not v7r) (not v8r))
(or (not v7g) (not v8g))
(or (not v7b) (not v8b))
) :named v7v8))

(assert (!(and 
(or (not v6r) (not v8r))
(or (not v6g) (not v8g))
(or (not v6b) (not v8b))
) :named v6v8))

(assert (!(and 
(or (not v8r) (not v9r))
(or (not v8g) (not v9g))
(or (not v8b) (not v9b))
) :named v8v9))

(assert (!(and 
(or (not v9r) (not v10r))
(or (not v9g) (not v10g))
(or (not v9b) (not v10b))
) :named v9v10))

(assert (!(and 
(or (not v8r) (not v10r))
(or (not v8g) (not v10g))
(or (not v8b) (not v10b))
) :named v8v10))

(assert (!(and 
(or (not v10r) (not v11r))
(or (not v10g) (not v11g))
(or (not v10b) (not v11b))
) :named v10v11))

(assert (!(and 
(or (not v11r) (not v12r))
(or (not v11g) (not v12g))
(or (not v11b) (not v12b))
) :named v11v12))

(assert (!(and 
(or (not v10r) (not v12r))
(or (not v10g) (not v12g))
(or (not v10b) (not v12b))
) :named v10v12))

(assert (!(and 
(or (not v1r) (not v12r))
(or (not v1g) (not v12g))
(or (not v1b) (not v12b))
) :named v1v12))

(assert (!(and 
(or (not v2r) (not v12r))
(or (not v2g) (not v12g))
(or (not v2b) (not v12b))
) :named v2v12))

(assert (!(and 
(or (not v1r) (not v7r))
(or (not v1g) (not v7g))
(or (not v1b) (not v7b))
) :named v1v7))

(assert (!(and 
(or (not v5r) (not v11r))
(or (not v5g) (not v11g))
(or (not v5b) (not v11b))
) :named v5v11))

(assert (!(and 
(or (not v3r) (not v9r))
(or (not v3g) (not v9g))
(or (not v3b) (not v9b))
) :named v3v9))

(check-sat)
(get-unsat-core)
(get-proof)