(benchmark SEQ020_size4.smt
:source {
CADE ATP System competition. See http://www.cs.miami.edu/~tptp/CASC
 for more information. 

This benchmark was obtained by trying to find a finite model of a first-order 
formula (Albert Oliveras).
}
:status sat
:logic QF_UF
:extrapreds ((p3 U))
:extrapreds ((p1 U U))
:extrapreds ((p4 U))
:extrapreds ((p14 U U U))
:extrapreds ((p9 U))
:extrafuns ((f12 U U))
:extrafuns ((f6 U U))
:extrafuns ((f2 U U U))
:extrafuns ((f17 U U U U))
:extrapreds ((p10 U U))
:extrafuns ((f16 U U U U))
:extrafuns ((f7 U U))
:extrafuns ((f13 U U U U))
:extrafuns ((c18 U))
:extrafuns ((f11 U U))
:extrafuns ((f5 U U))
:extrafuns ((c8 U))
:extrapreds ((p15 U U))
:extrafuns ((c_0 U))
:extrafuns ((c_1 U))
:extrafuns ((c_2 U))
:extrafuns ((c_3 U))
:formula 
( and 
( distinct c_0 c_1 c_2 c_3 )(or (not (p3 c_0)) (not (p1 c_0 c_0)) (= c_0 c_0) (p1 c_0 c_0) (not (p3 c_0)) (not (p3 c_0)) (= c_0 c_0) (not (p1 c_0 c_0)) (not (p4 c_0)) (= c_0 c_0) (not (p14 c_0 c_0 c_0)) )(or (not (p3 c_0)) (not (p1 c_0 c_0)) (= c_0 c_1) (p1 c_1 c_0) (not (p3 c_0)) (not (p3 c_1)) (= c_0 c_1) (not (p1 c_0 c_0)) (not (p4 c_0)) (= c_0 c_0) (not (p14 c_0 c_0 c_1)) )(or (not (p3 c_0)) (not (p1 c_0 c_0)) (= c_0 c_2) (p1 c_2 c_0) (not (p3 c_0)) (not (p3 c_2)) (= c_0 c_2) (not (p1 c_0 c_0)) (not (p4 c_0)) (= c_0 c_0) (not (p14 c_0 c_0 c_2)) )(or (not (p3 c_0)) (not (p1 c_0 c_0)) (= c_0 c_3) (p1 c_3 c_0) (not (p3 c_0)) (not (p3 c_3)) (= c_0 c_3) (not (p1 c_0 c_0)) (not (p4 c_0)) (= c_0 c_0) (not (p14 c_0 c_0 c_3)) )(or (not (p3 c_0)) (not (p1 c_0 c_1)) (= c_0 c_0) (p1 c_0 c_1) (not (p3 c_0)) (not (p3 c_0)) (= c_0 c_0) (not (p1 c_0 c_1)) (not (p4 c_1)) (= c_0 c_0) (not (p14 c_0 c_0 c_0)) )(or (not (p3 c_0)) (not (p1 c_0 c_1)) (= c_0 c_1) (p1 c_1 c_1) (not (p3 c_0)) (not (p3 c_1)) (= c_0 c_1) (not (p1 c_0 c_1)) (not (p4 c_1)) (= c_0 c_0) (not (p14 c_0 c_0 c_1)) )(or (not (p3 c_0)) (not (p1 c_0 c_1)) (= c_0 c_2) (p1 c_2 c_1) (not (p3 c_0)) (not (p3 c_2)) (= c_0 c_2) (not (p1 c_0 c_1)) (not (p4 c_1)) (= c_0 c_0) (not (p14 c_0 c_0 c_2)) )(or (not (p3 c_0)) (not (p1 c_0 c_1)) (= c_0 c_3) (p1 c_3 c_1) (not (p3 c_0)) (not (p3 c_3)) (= c_0 c_3) (not (p1 c_0 c_1)) (not (p4 c_1)) (= c_0 c_0) (not (p14 c_0 c_0 c_3)) )(or (not (p3 c_0)) (not (p1 c_0 c_2)) (= c_0 c_0) (p1 c_0 c_2) (not (p3 c_0)) (not (p3 c_0)) (= c_0 c_0) (not (p1 c_0 c_2)) (not (p4 c_2)) (= c_0 c_0) (not (p14 c_0 c_0 c_0)) )(or (not (p3 c_0)) (not (p1 c_0 c_2)) (= c_0 c_1) (p1 c_1 c_2) (not (p3 c_0)) (not (p3 c_1)) (= c_0 c_1) (not (p1 c_0 c_2)) (not (p4 c_2)) (= c_0 c_0) (not (p14 c_0 c_0 c_1)) )(or (not (p3 c_0)) (not (p1 c_0 c_2)) (= c_0 c_2) (p1 c_2 c_2) (not (p3 c_0)) (not (p3 c_2)) (= c_0 c_2) (not (p1 c_0 c_2)) (not (p4 c_2)) (= c_0 c_0) (not (p14 c_0 c_0 c_2)) )(or (not (p3 c_0)) (not (p1 c_0 c_2)) (= c_0 c_3) (p1 c_3 c_2) (not (p3 c_0)) (not (p3 c_3)) (= c_0 c_3) (not (p1 c_0 c_2)) (not (p4 c_2)) (= c_0 c_0) (not (p14 c_0 c_0 c_3)) )(or (not (p3 c_0)) (not (p1 c_0 c_3)) (= c_0 c_0) (p1 c_0 c_3) (not (p3 c_0)) (not (p3 c_0)) (= c_0 c_0) (not (p1 c_0 c_3)) (not (p4 c_3)) (= c_0 c_0) (not (p14 c_0 c_0 c_0)) )(or (not (p3 c_0)) (not (p1 c_0 c_3)) (= c_0 c_1) (p1 c_1 c_3) (not (p3 c_0)) (not (p3 c_1)) (= c_0 c_1) (not (p1 c_0 c_3)) (not (p4 c_3)) (= c_0 c_0) (not (p14 c_0 c_0 c_1)) )(or (not (p3 c_0)) (not (p1 c_0 c_3)) (= c_0 c_2) (p1 c_2 c_3) (not (p3 c_0)) (not (p3 c_2)) (= c_0 c_2) (not (p1 c_0 c_3)) (not (p4 c_3)) (= c_0 c_0) (not (p14 c_0 c_0 c_2)) )(or (not (p3 c_0)) (not (p1 c_0 c_3)) (= c_0 c_3) (p1 c_3 c_3) (not (p3 c_0)) (not (p3 c_3)) (= c_0 c_3) (not (p1 c_0 c_3)) (not (p4 c_3)) (= c_0 c_0) (not (p14 c_0 c_0 c_3)) )(or (not (p3 c_0)) (not (p1 c_1 c_0)) (= c_1 c_0) (p1 c_0 c_0) (not (p3 c_1)) (not (p3 c_0)) (= c_0 c_0) (not (p1 c_0 c_0)) (not (p4 c_0)) (= c_1 c_0) (not (p14 c_1 c_0 c_0)) )(or (not (p3 c_0)) (not (p1 c_1 c_0)) (= c_1 c_1) (p1 c_1 c_0) (not (p3 c_1)) (not (p3 c_1)) (= c_0 c_1) (not (p1 c_0 c_0)) (not (p4 c_0)) (= c_1 c_0) (not (p14 c_1 c_0 c_1)) )(or (not (p3 c_0)) (not (p1 c_1 c_0)) (= c_1 c_2) (p1 c_2 c_0) (not (p3 c_1)) (not (p3 c_2)) (= c_0 c_2) (not (p1 c_0 c_0)) (not (p4 c_0)) (= c_1 c_0) (not (p14 c_1 c_0 c_2)) )(or (not (p3 c_0)) (not (p1 c_1 c_0)) (= c_1 c_3) (p1 c_3 c_0) (not (p3 c_1)) (not (p3 c_3)) (= c_0 c_3) (not (p1 c_0 c_0)) (not (p4 c_0)) (= c_1 c_0) (not (p14 c_1 c_0 c_3)) )(or (not (p3 c_0)) (not (p1 c_1 c_1)) (= c_1 c_0) (p1 c_0 c_1) (not (p3 c_1)) (not (p3 c_0)) (= c_0 c_0) (not (p1 c_0 c_1)) (not (p4 c_1)) (= c_1 c_0) (not (p14 c_1 c_0 c_0)) )(or (not (p3 c_0)) (not (p1 c_1 c_1)) (= c_1 c_1) (p1 c_1 c_1) (not (p3 c_1)) (not (p3 c_1)) (= c_0 c_1) (not (p1 c_0 c_1)) (not (p4 c_1)) (= c_1 c_0) (not (p14 c_1 c_0 c_1)) )(or (not (p3 c_0)) (not (p1 c_1 c_1)) (= c_1 c_2) (p1 c_2 c_1) (not (p3 c_1)) (not (p3 c_2)) (= c_0 c_2) (not (p1 c_0 c_1)) (not (p4 c_1)) (= c_1 c_0) (not (p14 c_1 c_0 c_2)) )(or (not (p3 c_0)) (not (p1 c_1 c_1)) (= c_1 c_3) (p1 c_3 c_1) (not (p3 c_1)) (not (p3 c_3)) (= c_0 c_3) (not (p1 c_0 c_1)) (not (p4 c_1)) (= c_1 c_0) (not (p14 c_1 c_0 c_3)) )(or (not (p3 c_0)) (not (p1 c_1 c_2)) (= c_1 c_0) (p1 c_0 c_2) (not (p3 c_1)) (not (p3 c_0)) (= c_0 c_0) (not (p1 c_0 c_2)) (not (p4 c_2)) (= c_1 c_0) (not (p14 c_1 c_0 c_0)) )(or (not (p3 c_0)) (not (p1 c_1 c_2)) (= c_1 c_1) (p1 c_1 c_2) (not (p3 c_1)) (not (p3 c_1)) (= c_0 c_1) (not (p1 c_0 c_2)) (not (p4 c_2)) (= c_1 c_0) (not (p14 c_1 c_0 c_1)) )(or (not (p3 c_0)) (not (p1 c_1 c_2)) (= c_1 c_2) (p1 c_2 c_2) (not (p3 c_1)) (not (p3 c_2)) (= c_0 c_2) (not (p1 c_0 c_2)) (not (p4 c_2)) (= c_1 c_0) (not (p14 c_1 c_0 c_2)) )(or (not (p3 c_0)) (not (p1 c_1 c_2)) (= c_1 c_3) (p1 c_3 c_2) (not (p3 c_1)) (not (p3 c_3)) (= c_0 c_3) (not (p1 c_0 c_2)) (not (p4 c_2)) (= c_1 c_0) (not (p14 c_1 c_0 c_3)) )(or (not (p3 c_0)) (not (p1 c_1 c_3)) (= c_1 c_0) (p1 c_0 c_3) (not (p3 c_1)) (not (p3 c_0)) (= c_0 c_0) (not (p1 c_0 c_3)) (not (p4 c_3)) (= c_1 c_0) (not (p14 c_1 c_0 c_0)) )(or (not (p3 c_0)) (not (p1 c_1 c_3)) (= c_1 c_1) (p1 c_1 c_3) (not (p3 c_1)) (not (p3 c_1)) (= c_0 c_1) (not (p1 c_0 c_3)) (not (p4 c_3)) (= c_1 c_0) (not (p14 c_1 c_0 c_1)) )(or (not (p3 c_0)) (not (p1 c_1 c_3)) (= c_1 c_2) (p1 c_2 c_3) (not (p3 c_1)) (not (p3 c_2)) (= c_0 c_2) (not (p1 c_0 c_3)) (not (p4 c_3)) (= c_1 c_0) (not (p14 c_1 c_0 c_2)) )(or (not (p3 c_0)) (not (p1 c_1 c_3)) (= c_1 c_3) (p1 c_3 c_3) (not (p3 c_1)) (not (p3 c_3)) (= c_0 c_3) (not (p1 c_0 c_3)) (not (p4 c_3)) (= c_1 c_0) (not (p14 c_1 c_0 c_3)) )(or (not (p3 c_0)) (not (p1 c_2 c_0)) (= c_2 c_0) (p1 c_0 c_0) (not (p3 c_2)) (not (p3 c_0)) (= c_0 c_0) (not (p1 c_0 c_0)) (not (p4 c_0)) (= c_2 c_0) (not (p14 c_2 c_0 c_0)) )(or (not (p3 c_0)) (not (p1 c_2 c_0)) (= c_2 c_1) (p1 c_1 c_0) (not (p3 c_2)) (not (p3 c_1)) (= c_0 c_1) (not (p1 c_0 c_0)) (not (p4 c_0)) (= c_2 c_0) (not (p14 c_2 c_0 c_1)) )(or (not (p3 c_0)) (not (p1 c_2 c_0)) (= c_2 c_2) (p1 c_2 c_0) (not (p3 c_2)) (not (p3 c_2)) (= c_0 c_2) (not (p1 c_0 c_0)) (not (p4 c_0)) (= c_2 c_0) (not (p14 c_2 c_0 c_2)) )(or (not (p3 c_0)) (not (p1 c_2 c_0)) (= c_2 c_3) (p1 c_3 c_0) (not (p3 c_2)) (not (p3 c_3)) (= c_0 c_3) (not (p1 c_0 c_0)) (not (p4 c_0)) (= c_2 c_0) (not (p14 c_2 c_0 c_3)) )(or (not (p3 c_0)) (not (p1 c_2 c_1)) (= c_2 c_0) (p1 c_0 c_1) (not (p3 c_2)) (not (p3 c_0)) (= c_0 c_0) (not (p1 c_0 c_1)) (not (p4 c_1)) (= c_2 c_0) (not (p14 c_2 c_0 c_0)) )(or (not (p3 c_0)) (not (p1 c_2 c_1)) (= c_2 c_1) (p1 c_1 c_1) (not (p3 c_2)) (not (p3 c_1)) (= c_0 c_1) (not (p1 c_0 c_1)) (not (p4 c_1)) (= c_2 c_0) (not (p14 c_2 c_0 c_1)) )(or (not (p3 c_0)) (not (p1 c_2 c_1)) (= c_2 c_2) (p1 c_2 c_1) (not (p3 c_2)) (not (p3 c_2)) (= c_0 c_2) (not (p1 c_0 c_1)) (not (p4 c_1)) (= c_2 c_0) (not (p14 c_2 c_0 c_2)) )(or (not (p3 c_0)) (not (p1 c_2 c_1)) (= c_2 c_3) (p1 c_3 c_1) (not (p3 c_2)) (not (p3 c_3)) (= c_0 c_3) (not (p1 c_0 c_1)) (not (p4 c_1)) (= c_2 c_0) (not (p14 c_2 c_0 c_3)) )(or (not (p3 c_0)) (not (p1 c_2 c_2)) (= c_2 c_0) (p1 c_0 c_2) (not (p3 c_2)) (not (p3 c_0)) (= c_0 c_0) (not (p1 c_0 c_2)) (not (p4 c_2)) (= c_2 c_0) (not (p14 c_2 c_0 c_0)) )(or (not (p3 c_0)) (not (p1 c_2 c_2)) (= c_2 c_1) (p1 c_1 c_2) (not (p3 c_2)) (not (p3 c_1)) (= c_0 c_1) (not (p1 c_0 c_2)) (not (p4 c_2)) (= c_2 c_0) (not (p14 c_2 c_0 c_1)) )(or (not (p3 c_0)) (not (p1 c_2 c_2)) (= c_2 c_2) (p1 c_2 c_2) (not (p3 c_2)) (not (p3 c_2)) (= c_0 c_2) (not (p1 c_0 c_2)) (not (p4 c_2)) (= c_2 c_0) (not (p14 c_2 c_0 c_2)) )(or (not (p3 c_0)) (not (p1 c_2 c_2)) (= c_2 c_3) (p1 c_3 c_2) (not (p3 c_2)) (not (p3 c_3)) (= c_0 c_3) (not (p1 c_0 c_2)) (not (p4 c_2)) (= c_2 c_0) (not (p14 c_2 c_0 c_3)) )(or (not (p3 c_0)) (not (p1 c_2 c_3)) (= c_2 c_0) (p1 c_0 c_3) (not (p3 c_2)) (not (p3 c_0)) (= c_0 c_0) (not (p1 c_0 c_3)) (not (p4 c_3)) (= c_2 c_0) (not (p14 c_2 c_0 c_0)) )(or (not (p3 c_0)) (not (p1 c_2 c_3)) (= c_2 c_1) (p1 c_1 c_3) (not (p3 c_2)) (not (p3 c_1)) (= c_0 c_1) (not (p1 c_0 c_3)) (not (p4 c_3)) (= c_2 c_0) (not (p14 c_2 c_0 c_1)) )(or (not (p3 c_0)) (not (p1 c_2 c_3)) (= c_2 c_2) (p1 c_2 c_3) (not (p3 c_2)) (not (p3 c_2)) (= c_0 c_2) (not (p1 c_0 c_3)) (not (p4 c_3)) (= c_2 c_0) (not (p14 c_2 c_0 c_2)) )(or (not (p3 c_0)) (not (p1 c_2 c_3)) (= c_2 c_3) (p1 c_3 c_3) (not (p3 c_2)) (not (p3 c_3)) (= c_0 c_3) (not (p1 c_0 c_3)) (not (p4 c_3)) (= c_2 c_0) (not (p14 c_2 c_0 c_3)) )(or (not (p3 c_0)) (not (p1 c_3 c_0)) (= c_3 c_0) (p1 c_0 c_0) (not (p3 c_3)) (not (p3 c_0)) (= c_0 c_0) (not (p1 c_0 c_0)) (not (p4 c_0)) (= c_3 c_0) (not (p14 c_3 c_0 c_0)) )(or (not (p3 c_0)) (not (p1 c_3 c_0)) (= c_3 c_1) (p1 c_1 c_0) (not (p3 c_3)) (not (p3 c_1)) (= c_0 c_1) (not (p1 c_0 c_0)) (not (p4 c_0)) (= c_3 c_0) (not (p14 c_3 c_0 c_1)) )(or (not (p3 c_0)) (not (p1 c_3 c_0)) (= c_3 c_2) (p1 c_2 c_0) (not (p3 c_3)) (not (p3 c_2)) (= c_0 c_2) (not (p1 c_0 c_0)) (not (p4 c_0)) (= c_3 c_0) (not (p14 c_3 c_0 c_2)) )(or (not (p3 c_0)) (not (p1 c_3 c_0)) (= c_3 c_3) (p1 c_3 c_0) (not (p3 c_3)) (not (p3 c_3)) (= c_0 c_3) (not (p1 c_0 c_0)) (not (p4 c_0)) (= c_3 c_0) (not (p14 c_3 c_0 c_3)) )(or (not (p3 c_0)) (not (p1 c_3 c_1)) (= c_3 c_0) (p1 c_0 c_1) (not (p3 c_3)) (not (p3 c_0)) (= c_0 c_0) (not (p1 c_0 c_1)) (not (p4 c_1)) (= c_3 c_0) (not (p14 c_3 c_0 c_0)) )(or (not (p3 c_0)) (not (p1 c_3 c_1)) (= c_3 c_1) (p1 c_1 c_1) (not (p3 c_3)) (not (p3 c_1)) (= c_0 c_1) (not (p1 c_0 c_1)) (not (p4 c_1)) (= c_3 c_0) (not (p14 c_3 c_0 c_1)) )(or (not (p3 c_0)) (not (p1 c_3 c_1)) (= c_3 c_2) (p1 c_2 c_1) (not (p3 c_3)) (not (p3 c_2)) (= c_0 c_2) (not (p1 c_0 c_1)) (not (p4 c_1)) (= c_3 c_0) (not (p14 c_3 c_0 c_2)) )(or (not (p3 c_0)) (not (p1 c_3 c_1)) (= c_3 c_3) (p1 c_3 c_1) (not (p3 c_3)) (not (p3 c_3)) (= c_0 c_3) (not (p1 c_0 c_1)) (not (p4 c_1)) (= c_3 c_0) (not (p14 c_3 c_0 c_3)) )(or (not (p3 c_0)) (not (p1 c_3 c_2)) (= c_3 c_0) (p1 c_0 c_2) (not (p3 c_3)) (not (p3 c_0)) (= c_0 c_0) (not (p1 c_0 c_2)) (not (p4 c_2)) (= c_3 c_0) (not (p14 c_3 c_0 c_0)) )(or (not (p3 c_0)) (not (p1 c_3 c_2)) (= c_3 c_1) (p1 c_1 c_2) (not (p3 c_3)) (not (p3 c_1)) (= c_0 c_1) (not (p1 c_0 c_2)) (not (p4 c_2)) (= c_3 c_0) (not (p14 c_3 c_0 c_1)) )(or (not (p3 c_0)) (not (p1 c_3 c_2)) (= c_3 c_2) (p1 c_2 c_2) (not (p3 c_3)) (not (p3 c_2)) (= c_0 c_2) (not (p1 c_0 c_2)) (not (p4 c_2)) (= c_3 c_0) (not (p14 c_3 c_0 c_2)) )(or (not (p3 c_0)) (not (p1 c_3 c_2)) (= c_3 c_3) (p1 c_3 c_2) (not (p3 c_3)) (not (p3 c_3)) (= c_0 c_3) (not (p1 c_0 c_2)) (not (p4 c_2)) (= c_3 c_0) (not (p14 c_3 c_0 c_3)) )(or (not (p3 c_0)) (not (p1 c_3 c_3)) (= c_3 c_0) (p1 c_0 c_3) (not (p3 c_3)) (not (p3 c_0)) (= c_0 c_0) (not (p1 c_0 c_3)) (not (p4 c_3)) (= c_3 c_0) (not (p14 c_3 c_0 c_0)) )(or (not (p3 c_0)) (not (p1 c_3 c_3)) (= c_3 c_1) (p1 c_1 c_3) (not (p3 c_3)) (not (p3 c_1)) (= c_0 c_1) (not (p1 c_0 c_3)) (not (p4 c_3)) (= c_3 c_0) (not (p14 c_3 c_0 c_1)) )(or (not (p3 c_0)) (not (p1 c_3 c_3)) (= c_3 c_2) (p1 c_2 c_3) (not (p3 c_3)) (not (p3 c_2)) (= c_0 c_2) (not (p1 c_0 c_3)) (not (p4 c_3)) (= c_3 c_0) (not (p14 c_3 c_0 c_2)) )(or (not (p3 c_0)) (not (p1 c_3 c_3)) (= c_3 c_3) (p1 c_3 c_3) (not (p3 c_3)) (not (p3 c_3)) (= c_0 c_3) (not (p1 c_0 c_3)) (not (p4 c_3)) (= c_3 c_0) (not (p14 c_3 c_0 c_3)) )(or (not (p3 c_1)) (not (p1 c_0 c_0)) (= c_0 c_0) (p1 c_0 c_0) (not (p3 c_0)) (not (p3 c_0)) (= c_1 c_0) (not (p1 c_1 c_0)) (not (p4 c_0)) (= c_0 c_1) (not (p14 c_0 c_1 c_0)) )(or (not (p3 c_1)) (not (p1 c_0 c_0)) (= c_0 c_1) (p1 c_1 c_0) (not (p3 c_0)) (not (p3 c_1)) (= c_1 c_1) (not (p1 c_1 c_0)) (not (p4 c_0)) (= c_0 c_1) (not (p14 c_0 c_1 c_1)) )(or (not (p3 c_1)) (not (p1 c_0 c_0)) (= c_0 c_2) (p1 c_2 c_0) (not (p3 c_0)) (not (p3 c_2)) (= c_1 c_2) (not (p1 c_1 c_0)) (not (p4 c_0)) (= c_0 c_1) (not (p14 c_0 c_1 c_2)) )(or (not (p3 c_1)) (not (p1 c_0 c_0)) (= c_0 c_3) (p1 c_3 c_0) (not (p3 c_0)) (not (p3 c_3)) (= c_1 c_3) (not (p1 c_1 c_0)) (not (p4 c_0)) (= c_0 c_1) (not (p14 c_0 c_1 c_3)) )(or (not (p3 c_1)) (not (p1 c_0 c_1)) (= c_0 c_0) (p1 c_0 c_1) (not (p3 c_0)) (not (p3 c_0)) (= c_1 c_0) (not (p1 c_1 c_1)) (not (p4 c_1)) (= c_0 c_1) (not (p14 c_0 c_1 c_0)) )(or (not (p3 c_1)) (not (p1 c_0 c_1)) (= c_0 c_1) (p1 c_1 c_1) (not (p3 c_0)) (not (p3 c_1)) (= c_1 c_1) (not (p1 c_1 c_1)) (not (p4 c_1)) (= c_0 c_1) (not (p14 c_0 c_1 c_1)) )(or (not (p3 c_1)) (not (p1 c_0 c_1)) (= c_0 c_2) (p1 c_2 c_1) (not (p3 c_0)) (not (p3 c_2)) (= c_1 c_2) (not (p1 c_1 c_1)) (not (p4 c_1)) (= c_0 c_1) (not (p14 c_0 c_1 c_2)) )(or (not (p3 c_1)) (not (p1 c_0 c_1)) (= c_0 c_3) (p1 c_3 c_1) (not (p3 c_0)) (not (p3 c_3)) (= c_1 c_3) (not (p1 c_1 c_1)) (not (p4 c_1)) (= c_0 c_1) (not (p14 c_0 c_1 c_3)) )(or (not (p3 c_1)) (not (p1 c_0 c_2)) (= c_0 c_0) (p1 c_0 c_2) (not (p3 c_0)) (not (p3 c_0)) (= c_1 c_0) (not (p1 c_1 c_2)) (not (p4 c_2)) (= c_0 c_1) (not (p14 c_0 c_1 c_0)) )(or (not (p3 c_1)) (not (p1 c_0 c_2)) (= c_0 c_1) (p1 c_1 c_2) (not (p3 c_0)) (not (p3 c_1)) (= c_1 c_1) (not (p1 c_1 c_2)) (not (p4 c_2)) (= c_0 c_1) (not (p14 c_0 c_1 c_1)) )(or (not (p3 c_1)) (not (p1 c_0 c_2)) (= c_0 c_2) (p1 c_2 c_2) (not (p3 c_0)) (not (p3 c_2)) (= c_1 c_2) (not (p1 c_1 c_2)) (not (p4 c_2)) (= c_0 c_1) (not (p14 c_0 c_1 c_2)) )(or (not (p3 c_1)) (not (p1 c_0 c_2)) (= c_0 c_3) (p1 c_3 c_2) (not (p3 c_0)) (not (p3 c_3)) (= c_1 c_3) (not (p1 c_1 c_2)) (not (p4 c_2)) (= c_0 c_1) (not (p14 c_0 c_1 c_3)) )(or (not (p3 c_1)) (not (p1 c_0 c_3)) (= c_0 c_0) (p1 c_0 c_3) (not (p3 c_0)) (not (p3 c_0)) (= c_1 c_0) (not (p1 c_1 c_3)) (not (p4 c_3)) (= c_0 c_1) (not (p14 c_0 c_1 c_0)) )(or (not (p3 c_1)) (not (p1 c_0 c_3)) (= c_0 c_1) (p1 c_1 c_3) (not (p3 c_0)) (not (p3 c_1)) (= c_1 c_1) (not (p1 c_1 c_3)) (not (p4 c_3)) (= c_0 c_1) (not (p14 c_0 c_1 c_1)) )(or (not (p3 c_1)) (not (p1 c_0 c_3)) (= c_0 c_2) (p1 c_2 c_3) (not (p3 c_0)) (not (p3 c_2)) (= c_1 c_2) (not (p1 c_1 c_3)) (not (p4 c_3)) (= c_0 c_1) (not (p14 c_0 c_1 c_2)) )(or (not (p3 c_1)) (not (p1 c_0 c_3)) (= c_0 c_3) (p1 c_3 c_3) (not (p3 c_0)) (not (p3 c_3)) (= c_1 c_3) (not (p1 c_1 c_3)) (not (p4 c_3)) (= c_0 c_1) (not (p14 c_0 c_1 c_3)) )(or (not (p3 c_1)) (not (p1 c_1 c_0)) (= c_1 c_0) (p1 c_0 c_0) (not (p3 c_1)) (not (p3 c_0)) (= c_1 c_0) (not (p1 c_1 c_0)) (not (p4 c_0)) (= c_1 c_1) (not (p14 c_1 c_1 c_0)) )(or (not (p3 c_1)) (not (p1 c_1 c_0)) (= c_1 c_1) (p1 c_1 c_0) (not (p3 c_1)) (not (p3 c_1)) (= c_1 c_1) (not (p1 c_1 c_0)) (not (p4 c_0)) (= c_1 c_1) (not (p14 c_1 c_1 c_1)) )(or (not (p3 c_1)) (not (p1 c_1 c_0)) (= c_1 c_2) (p1 c_2 c_0) (not (p3 c_1)) (not (p3 c_2)) (= c_1 c_2) (not (p1 c_1 c_0)) (not (p4 c_0)) (= c_1 c_1) (not (p14 c_1 c_1 c_2)) )(or (not (p3 c_1)) (not (p1 c_1 c_0)) (= c_1 c_3) (p1 c_3 c_0) (not (p3 c_1)) (not (p3 c_3)) (= c_1 c_3) (not (p1 c_1 c_0)) (not (p4 c_0)) (= c_1 c_1) (not (p14 c_1 c_1 c_3)) )(or (not (p3 c_1)) (not (p1 c_1 c_1)) (= c_1 c_0) (p1 c_0 c_1) (not (p3 c_1)) (not (p3 c_0)) (= c_1 c_0) (not (p1 c_1 c_1)) (not (p4 c_1)) (= c_1 c_1) (not (p14 c_1 c_1 c_0)) )(or (not (p3 c_1)) (not (p1 c_1 c_1)) (= c_1 c_1) (p1 c_1 c_1) (not (p3 c_1)) (not (p3 c_1)) (= c_1 c_1) (not (p1 c_1 c_1)) (not (p4 c_1)) (= c_1 c_1) (not (p14 c_1 c_1 c_1)) )(or (not (p3 c_1)) (not (p1 c_1 c_1)) (= c_1 c_2) (p1 c_2 c_1) (not (p3 c_1)) (not (p3 c_2)) (= c_1 c_2) (not (p1 c_1 c_1)) (not (p4 c_1)) (= c_1 c_1) (not (p14 c_1 c_1 c_2)) )(or (not (p3 c_1)) (not (p1 c_1 c_1)) (= c_1 c_3) (p1 c_3 c_1) (not (p3 c_1)) (not (p3 c_3)) (= c_1 c_3) (not (p1 c_1 c_1)) (not (p4 c_1)) (= c_1 c_1) (not (p14 c_1 c_1 c_3)) )(or (not (p3 c_1)) (not (p1 c_1 c_2)) (= c_1 c_0) (p1 c_0 c_2) (not (p3 c_1)) (not (p3 c_0)) (= c_1 c_0) (not (p1 c_1 c_2)) (not (p4 c_2)) (= c_1 c_1) (not (p14 c_1 c_1 c_0)) )(or (not (p3 c_1)) (not (p1 c_1 c_2)) (= c_1 c_1) (p1 c_1 c_2) (not (p3 c_1)) (not (p3 c_1)) (= c_1 c_1) (not (p1 c_1 c_2)) (not (p4 c_2)) (= c_1 c_1) (not (p14 c_1 c_1 c_1)) )(or (not (p3 c_1)) (not (p1 c_1 c_2)) (= c_1 c_2) (p1 c_2 c_2) (not (p3 c_1)) (not (p3 c_2)) (= c_1 c_2) (not (p1 c_1 c_2)) (not (p4 c_2)) (= c_1 c_1) (not (p14 c_1 c_1 c_2)) )(or (not (p3 c_1)) (not (p1 c_1 c_2)) (= c_1 c_3) (p1 c_3 c_2) (not (p3 c_1)) (not (p3 c_3)) (= c_1 c_3) (not (p1 c_1 c_2)) (not (p4 c_2)) (= c_1 c_1) (not (p14 c_1 c_1 c_3)) )(or (not (p3 c_1)) (not (p1 c_1 c_3)) (= c_1 c_0) (p1 c_0 c_3) (not (p3 c_1)) (not (p3 c_0)) (= c_1 c_0) (not (p1 c_1 c_3)) (not (p4 c_3)) (= c_1 c_1) (not (p14 c_1 c_1 c_0)) )(or (not (p3 c_1)) (not (p1 c_1 c_3)) (= c_1 c_1) (p1 c_1 c_3) (not (p3 c_1)) (not (p3 c_1)) (= c_1 c_1) (not (p1 c_1 c_3)) (not (p4 c_3)) (= c_1 c_1) (not (p14 c_1 c_1 c_1)) )(or (not (p3 c_1)) (not (p1 c_1 c_3)) (= c_1 c_2) (p1 c_2 c_3) (not (p3 c_1)) (not (p3 c_2)) (= c_1 c_2) (not (p1 c_1 c_3)) (not (p4 c_3)) (= c_1 c_1) (not (p14 c_1 c_1 c_2)) )(or (not (p3 c_1)) (not (p1 c_1 c_3)) (= c_1 c_3) (p1 c_3 c_3) (not (p3 c_1)) (not (p3 c_3)) (= c_1 c_3) (not (p1 c_1 c_3)) (not (p4 c_3)) (= c_1 c_1) (not (p14 c_1 c_1 c_3)) )(or (not (p3 c_1)) (not (p1 c_2 c_0)) (= c_2 c_0) (p1 c_0 c_0) (not (p3 c_2)) (not (p3 c_0)) (= c_1 c_0) (not (p1 c_1 c_0)) (not (p4 c_0)) (= c_2 c_1) (not (p14 c_2 c_1 c_0)) )(or (not (p3 c_1)) (not (p1 c_2 c_0)) (= c_2 c_1) (p1 c_1 c_0) (not (p3 c_2)) (not (p3 c_1)) (= c_1 c_1) (not (p1 c_1 c_0)) (not (p4 c_0)) (= c_2 c_1) (not (p14 c_2 c_1 c_1)) )(or (not (p3 c_1)) (not (p1 c_2 c_0)) (= c_2 c_2) (p1 c_2 c_0) (not (p3 c_2)) (not (p3 c_2)) (= c_1 c_2) (not (p1 c_1 c_0)) (not (p4 c_0)) (= c_2 c_1) (not (p14 c_2 c_1 c_2)) )(or (not (p3 c_1)) (not (p1 c_2 c_0)) (= c_2 c_3) (p1 c_3 c_0) (not (p3 c_2)) (not (p3 c_3)) (= c_1 c_3) (not (p1 c_1 c_0)) (not (p4 c_0)) (= c_2 c_1) (not (p14 c_2 c_1 c_3)) )(or (not (p3 c_1)) (not (p1 c_2 c_1)) (= c_2 c_0) (p1 c_0 c_1) (not (p3 c_2)) (not (p3 c_0)) (= c_1 c_0) (not (p1 c_1 c_1)) (not (p4 c_1)) (= c_2 c_1) (not (p14 c_2 c_1 c_0)) )(or (not (p3 c_1)) (not (p1 c_2 c_1)) (= c_2 c_1) (p1 c_1 c_1) (not (p3 c_2)) (not (p3 c_1)) (= c_1 c_1) (not (p1 c_1 c_1)) (not (p4 c_1)) (= c_2 c_1) (not (p14 c_2 c_1 c_1)) )(or (not (p3 c_1)) (not (p1 c_2 c_1)) (= c_2 c_2) (p1 c_2 c_1) (not (p3 c_2)) (not (p3 c_2)) (= c_1 c_2) (not (p1 c_1 c_1)) (not (p4 c_1)) (= c_2 c_1) (not (p14 c_2 c_1 c_2)) )(or (not (p3 c_1)) (not (p1 c_2 c_1)) (= c_2 c_3) (p1 c_3 c_1) (not (p3 c_2)) (not (p3 c_3)) (= c_1 c_3) (not (p1 c_1 c_1)) (not (p4 c_1)) (= c_2 c_1) (not (p14 c_2 c_1 c_3)) )(or (not (p3 c_1)) (not (p1 c_2 c_2)) (= c_2 c_0) (p1 c_0 c_2) (not (p3 c_2)) (not (p3 c_0)) (= c_1 c_0) (not (p1 c_1 c_2)) (not (p4 c_2)) (= c_2 c_1) (not (p14 c_2 c_1 c_0)) )(or (not (p3 c_1)) (not (p1 c_2 c_2)) (= c_2 c_1) (p1 c_1 c_2) (not (p3 c_2)) (not (p3 c_1)) (= c_1 c_1) (not (p1 c_1 c_2)) (not (p4 c_2)) (= c_2 c_1) (not (p14 c_2 c_1 c_1)) )(or (not (p3 c_1)) (not (p1 c_2 c_2)) (= c_2 c_2) (p1 c_2 c_2) (not (p3 c_2)) (not (p3 c_2)) (= c_1 c_2) (not (p1 c_1 c_2)) (not (p4 c_2)) (= c_2 c_1) (not (p14 c_2 c_1 c_2)) )(or (not (p3 c_1)) (not (p1 c_2 c_2)) (= c_2 c_3) (p1 c_3 c_2) (not (p3 c_2)) (not (p3 c_3)) (= c_1 c_3) (not (p1 c_1 c_2)) (not (p4 c_2)) (= c_2 c_1) (not (p14 c_2 c_1 c_3)) )(or (not (p3 c_1)) (not (p1 c_2 c_3)) (= c_2 c_0) (p1 c_0 c_3) (not (p3 c_2)) (not (p3 c_0)) (= c_1 c_0) (not (p1 c_1 c_3)) (not (p4 c_3)) (= c_2 c_1) (not (p14 c_2 c_1 c_0)) )(or (not (p3 c_1)) (not (p1 c_2 c_3)) (= c_2 c_1) (p1 c_1 c_3) (not (p3 c_2)) (not (p3 c_1)) (= c_1 c_1) (not (p1 c_1 c_3)) (not (p4 c_3)) (= c_2 c_1) (not (p14 c_2 c_1 c_1)) )(or (not (p3 c_1)) (not (p1 c_2 c_3)) (= c_2 c_2) (p1 c_2 c_3) (not (p3 c_2)) (not (p3 c_2)) (= c_1 c_2) (not (p1 c_1 c_3)) (not (p4 c_3)) (= c_2 c_1) (not (p14 c_2 c_1 c_2)) )(or (not (p3 c_1)) (not (p1 c_2 c_3)) (= c_2 c_3) (p1 c_3 c_3) (not (p3 c_2)) (not (p3 c_3)) (= c_1 c_3) (not (p1 c_1 c_3)) (not (p4 c_3)) (= c_2 c_1) (not (p14 c_2 c_1 c_3)) )(or (not (p3 c_1)) (not (p1 c_3 c_0)) (= c_3 c_0) (p1 c_0 c_0) (not (p3 c_3)) (not (p3 c_0)) (= c_1 c_0) (not (p1 c_1 c_0)) (not (p4 c_0)) (= c_3 c_1) (not (p14 c_3 c_1 c_0)) )(or (not (p3 c_1)) (not (p1 c_3 c_0)) (= c_3 c_1) (p1 c_1 c_0) (not (p3 c_3)) (not (p3 c_1)) (= c_1 c_1) (not (p1 c_1 c_0)) (not (p4 c_0)) (= c_3 c_1) (not (p14 c_3 c_1 c_1)) )(or (not (p3 c_1)) (not (p1 c_3 c_0)) (= c_3 c_2) (p1 c_2 c_0) (not (p3 c_3)) (not (p3 c_2)) (= c_1 c_2) (not (p1 c_1 c_0)) (not (p4 c_0)) (= c_3 c_1) (not (p14 c_3 c_1 c_2)) )(or (not (p3 c_1)) (not (p1 c_3 c_0)) (= c_3 c_3) (p1 c_3 c_0) (not (p3 c_3)) (not (p3 c_3)) (= c_1 c_3) (not (p1 c_1 c_0)) (not (p4 c_0)) (= c_3 c_1) (not (p14 c_3 c_1 c_3)) )(or (not (p3 c_1)) (not (p1 c_3 c_1)) (= c_3 c_0) (p1 c_0 c_1) (not (p3 c_3)) (not (p3 c_0)) (= c_1 c_0) (not (p1 c_1 c_1)) (not (p4 c_1)) (= c_3 c_1) (not (p14 c_3 c_1 c_0)) )(or (not (p3 c_1)) (not (p1 c_3 c_1)) (= c_3 c_1) (p1 c_1 c_1) (not (p3 c_3)) (not (p3 c_1)) (= c_1 c_1) (not (p1 c_1 c_1)) (not (p4 c_1)) (= c_3 c_1) (not (p14 c_3 c_1 c_1)) )(or (not (p3 c_1)) (not (p1 c_3 c_1)) (= c_3 c_2) (p1 c_2 c_1) (not (p3 c_3)) (not (p3 c_2)) (= c_1 c_2) (not (p1 c_1 c_1)) (not (p4 c_1)) (= c_3 c_1) (not (p14 c_3 c_1 c_2)) )(or (not (p3 c_1)) (not (p1 c_3 c_1)) (= c_3 c_3) (p1 c_3 c_1) (not (p3 c_3)) (not (p3 c_3)) (= c_1 c_3) (not (p1 c_1 c_1)) (not (p4 c_1)) (= c_3 c_1) (not (p14 c_3 c_1 c_3)) )(or (not (p3 c_1)) (not (p1 c_3 c_2)) (= c_3 c_0) (p1 c_0 c_2) (not (p3 c_3)) (not (p3 c_0)) (= c_1 c_0) (not (p1 c_1 c_2)) (not (p4 c_2)) (= c_3 c_1) (not (p14 c_3 c_1 c_0)) )(or (not (p3 c_1)) (not (p1 c_3 c_2)) (= c_3 c_1) (p1 c_1 c_2) (not (p3 c_3)) (not (p3 c_1)) (= c_1 c_1) (not (p1 c_1 c_2)) (not (p4 c_2)) (= c_3 c_1) (not (p14 c_3 c_1 c_1)) )(or (not (p3 c_1)) (not (p1 c_3 c_2)) (= c_3 c_2) (p1 c_2 c_2) (not (p3 c_3)) (not (p3 c_2)) (= c_1 c_2) (not (p1 c_1 c_2)) (not (p4 c_2)) (= c_3 c_1) (not (p14 c_3 c_1 c_2)) )(or (not (p3 c_1)) (not (p1 c_3 c_2)) (= c_3 c_3) (p1 c_3 c_2) (not (p3 c_3)) (not (p3 c_3)) (= c_1 c_3) (not (p1 c_1 c_2)) (not (p4 c_2)) (= c_3 c_1) (not (p14 c_3 c_1 c_3)) )(or (not (p3 c_1)) (not (p1 c_3 c_3)) (= c_3 c_0) (p1 c_0 c_3) (not (p3 c_3)) (not (p3 c_0)) (= c_1 c_0) (not (p1 c_1 c_3)) (not (p4 c_3)) (= c_3 c_1) (not (p14 c_3 c_1 c_0)) )(or (not (p3 c_1)) (not (p1 c_3 c_3)) (= c_3 c_1) (p1 c_1 c_3) (not (p3 c_3)) (not (p3 c_1)) (= c_1 c_1) (not (p1 c_1 c_3)) (not (p4 c_3)) (= c_3 c_1) (not (p14 c_3 c_1 c_1)) )(or (not (p3 c_1)) (not (p1 c_3 c_3)) (= c_3 c_2) (p1 c_2 c_3) (not (p3 c_3)) (not (p3 c_2)) (= c_1 c_2) (not (p1 c_1 c_3)) (not (p4 c_3)) (= c_3 c_1) (not (p14 c_3 c_1 c_2)) )(or (not (p3 c_1)) (not (p1 c_3 c_3)) (= c_3 c_3) (p1 c_3 c_3) (not (p3 c_3)) (not (p3 c_3)) (= c_1 c_3) (not (p1 c_1 c_3)) (not (p4 c_3)) (= c_3 c_1) (not (p14 c_3 c_1 c_3)) )(or (not (p3 c_2)) (not (p1 c_0 c_0)) (= c_0 c_0) (p1 c_0 c_0) (not (p3 c_0)) (not (p3 c_0)) (= c_2 c_0) (not (p1 c_2 c_0)) (not (p4 c_0)) (= c_0 c_2) (not (p14 c_0 c_2 c_0)) )(or (not (p3 c_2)) (not (p1 c_0 c_0)) (= c_0 c_1) (p1 c_1 c_0) (not (p3 c_0)) (not (p3 c_1)) (= c_2 c_1) (not (p1 c_2 c_0)) (not (p4 c_0)) (= c_0 c_2) (not (p14 c_0 c_2 c_1)) )(or (not (p3 c_2)) (not (p1 c_0 c_0)) (= c_0 c_2) (p1 c_2 c_0) (not (p3 c_0)) (not (p3 c_2)) (= c_2 c_2) (not (p1 c_2 c_0)) (not (p4 c_0)) (= c_0 c_2) (not (p14 c_0 c_2 c_2)) )(or (not (p3 c_2)) (not (p1 c_0 c_0)) (= c_0 c_3) (p1 c_3 c_0) (not (p3 c_0)) (not (p3 c_3)) (= c_2 c_3) (not (p1 c_2 c_0)) (not (p4 c_0)) (= c_0 c_2) (not (p14 c_0 c_2 c_3)) )(or (not (p3 c_2)) (not (p1 c_0 c_1)) (= c_0 c_0) (p1 c_0 c_1) (not (p3 c_0)) (not (p3 c_0)) (= c_2 c_0) (not (p1 c_2 c_1)) (not (p4 c_1)) (= c_0 c_2) (not (p14 c_0 c_2 c_0)) )(or (not (p3 c_2)) (not (p1 c_0 c_1)) (= c_0 c_1) (p1 c_1 c_1) (not (p3 c_0)) (not (p3 c_1)) (= c_2 c_1) (not (p1 c_2 c_1)) (not (p4 c_1)) (= c_0 c_2) (not (p14 c_0 c_2 c_1)) )(or (not (p3 c_2)) (not (p1 c_0 c_1)) (= c_0 c_2) (p1 c_2 c_1) (not (p3 c_0)) (not (p3 c_2)) (= c_2 c_2) (not (p1 c_2 c_1)) (not (p4 c_1)) (= c_0 c_2) (not (p14 c_0 c_2 c_2)) )(or (not (p3 c_2)) (not (p1 c_0 c_1)) (= c_0 c_3) (p1 c_3 c_1) (not (p3 c_0)) (not (p3 c_3)) (= c_2 c_3) (not (p1 c_2 c_1)) (not (p4 c_1)) (= c_0 c_2) (not (p14 c_0 c_2 c_3)) )(or (not (p3 c_2)) (not (p1 c_0 c_2)) (= c_0 c_0) (p1 c_0 c_2) (not (p3 c_0)) (not (p3 c_0)) (= c_2 c_0) (not (p1 c_2 c_2)) (not (p4 c_2)) (= c_0 c_2) (not (p14 c_0 c_2 c_0)) )(or (not (p3 c_2)) (not (p1 c_0 c_2)) (= c_0 c_1) (p1 c_1 c_2) (not (p3 c_0)) (not (p3 c_1)) (= c_2 c_1) (not (p1 c_2 c_2)) (not (p4 c_2)) (= c_0 c_2) (not (p14 c_0 c_2 c_1)) )(or (not (p3 c_2)) (not (p1 c_0 c_2)) (= c_0 c_2) (p1 c_2 c_2) (not (p3 c_0)) (not (p3 c_2)) (= c_2 c_2) (not (p1 c_2 c_2)) (not (p4 c_2)) (= c_0 c_2) (not (p14 c_0 c_2 c_2)) )(or (not (p3 c_2)) (not (p1 c_0 c_2)) (= c_0 c_3) (p1 c_3 c_2) (not (p3 c_0)) (not (p3 c_3)) (= c_2 c_3) (not (p1 c_2 c_2)) (not (p4 c_2)) (= c_0 c_2) (not (p14 c_0 c_2 c_3)) )(or (not (p3 c_2)) (not (p1 c_0 c_3)) (= c_0 c_0) (p1 c_0 c_3) (not (p3 c_0)) (not (p3 c_0)) (= c_2 c_0) (not (p1 c_2 c_3)) (not (p4 c_3)) (= c_0 c_2) (not (p14 c_0 c_2 c_0)) )(or (not (p3 c_2)) (not (p1 c_0 c_3)) (= c_0 c_1) (p1 c_1 c_3) (not (p3 c_0)) (not (p3 c_1)) (= c_2 c_1) (not (p1 c_2 c_3)) (not (p4 c_3)) (= c_0 c_2) (not (p14 c_0 c_2 c_1)) )(or (not (p3 c_2)) (not (p1 c_0 c_3)) (= c_0 c_2) (p1 c_2 c_3) (not (p3 c_0)) (not (p3 c_2)) (= c_2 c_2) (not (p1 c_2 c_3)) (not (p4 c_3)) (= c_0 c_2) (not (p14 c_0 c_2 c_2)) )(or (not (p3 c_2)) (not (p1 c_0 c_3)) (= c_0 c_3) (p1 c_3 c_3) (not (p3 c_0)) (not (p3 c_3)) (= c_2 c_3) (not (p1 c_2 c_3)) (not (p4 c_3)) (= c_0 c_2) (not (p14 c_0 c_2 c_3)) )(or (not (p3 c_2)) (not (p1 c_1 c_0)) (= c_1 c_0) (p1 c_0 c_0) (not (p3 c_1)) (not (p3 c_0)) (= c_2 c_0) (not (p1 c_2 c_0)) (not (p4 c_0)) (= c_1 c_2) (not (p14 c_1 c_2 c_0)) )(or (not (p3 c_2)) (not (p1 c_1 c_0)) (= c_1 c_1) (p1 c_1 c_0) (not (p3 c_1)) (not (p3 c_1)) (= c_2 c_1) (not (p1 c_2 c_0)) (not (p4 c_0)) (= c_1 c_2) (not (p14 c_1 c_2 c_1)) )(or (not (p3 c_2)) (not (p1 c_1 c_0)) (= c_1 c_2) (p1 c_2 c_0) (not (p3 c_1)) (not (p3 c_2)) (= c_2 c_2) (not (p1 c_2 c_0)) (not (p4 c_0)) (= c_1 c_2) (not (p14 c_1 c_2 c_2)) )(or (not (p3 c_2)) (not (p1 c_1 c_0)) (= c_1 c_3) (p1 c_3 c_0) (not (p3 c_1)) (not (p3 c_3)) (= c_2 c_3) (not (p1 c_2 c_0)) (not (p4 c_0)) (= c_1 c_2) (not (p14 c_1 c_2 c_3)) )(or (not (p3 c_2)) (not (p1 c_1 c_1)) (= c_1 c_0) (p1 c_0 c_1) (not (p3 c_1)) (not (p3 c_0)) (= c_2 c_0) (not (p1 c_2 c_1)) (not (p4 c_1)) (= c_1 c_2) (not (p14 c_1 c_2 c_0)) )(or (not (p3 c_2)) (not (p1 c_1 c_1)) (= c_1 c_1) (p1 c_1 c_1) (not (p3 c_1)) (not (p3 c_1)) (= c_2 c_1) (not (p1 c_2 c_1)) (not (p4 c_1)) (= c_1 c_2) (not (p14 c_1 c_2 c_1)) )(or (not (p3 c_2)) (not (p1 c_1 c_1)) (= c_1 c_2) (p1 c_2 c_1) (not (p3 c_1)) (not (p3 c_2)) (= c_2 c_2) (not (p1 c_2 c_1)) (not (p4 c_1)) (= c_1 c_2) (not (p14 c_1 c_2 c_2)) )(or (not (p3 c_2)) (not (p1 c_1 c_1)) (= c_1 c_3) (p1 c_3 c_1) (not (p3 c_1)) (not (p3 c_3)) (= c_2 c_3) (not (p1 c_2 c_1)) (not (p4 c_1)) (= c_1 c_2) (not (p14 c_1 c_2 c_3)) )(or (not (p3 c_2)) (not (p1 c_1 c_2)) (= c_1 c_0) (p1 c_0 c_2) (not (p3 c_1)) (not (p3 c_0)) (= c_2 c_0) (not (p1 c_2 c_2)) (not (p4 c_2)) (= c_1 c_2) (not (p14 c_1 c_2 c_0)) )(or (not (p3 c_2)) (not (p1 c_1 c_2)) (= c_1 c_1) (p1 c_1 c_2) (not (p3 c_1)) (not (p3 c_1)) (= c_2 c_1) (not (p1 c_2 c_2)) (not (p4 c_2)) (= c_1 c_2) (not (p14 c_1 c_2 c_1)) )(or (not (p3 c_2)) (not (p1 c_1 c_2)) (= c_1 c_2) (p1 c_2 c_2) (not (p3 c_1)) (not (p3 c_2)) (= c_2 c_2) (not (p1 c_2 c_2)) (not (p4 c_2)) (= c_1 c_2) (not (p14 c_1 c_2 c_2)) )(or (not (p3 c_2)) (not (p1 c_1 c_2)) (= c_1 c_3) (p1 c_3 c_2) (not (p3 c_1)) (not (p3 c_3)) (= c_2 c_3) (not (p1 c_2 c_2)) (not (p4 c_2)) (= c_1 c_2) (not (p14 c_1 c_2 c_3)) )(or (not (p3 c_2)) (not (p1 c_1 c_3)) (= c_1 c_0) (p1 c_0 c_3) (not (p3 c_1)) (not (p3 c_0)) (= c_2 c_0) (not (p1 c_2 c_3)) (not (p4 c_3)) (= c_1 c_2) (not (p14 c_1 c_2 c_0)) )(or (not (p3 c_2)) (not (p1 c_1 c_3)) (= c_1 c_1) (p1 c_1 c_3) (not (p3 c_1)) (not (p3 c_1)) (= c_2 c_1) (not (p1 c_2 c_3)) (not (p4 c_3)) (= c_1 c_2) (not (p14 c_1 c_2 c_1)) )(or (not (p3 c_2)) (not (p1 c_1 c_3)) (= c_1 c_2) (p1 c_2 c_3) (not (p3 c_1)) (not (p3 c_2)) (= c_2 c_2) (not (p1 c_2 c_3)) (not (p4 c_3)) (= c_1 c_2) (not (p14 c_1 c_2 c_2)) )(or (not (p3 c_2)) (not (p1 c_1 c_3)) (= c_1 c_3) (p1 c_3 c_3) (not (p3 c_1)) (not (p3 c_3)) (= c_2 c_3) (not (p1 c_2 c_3)) (not (p4 c_3)) (= c_1 c_2) (not (p14 c_1 c_2 c_3)) )(or (not (p3 c_2)) (not (p1 c_2 c_0)) (= c_2 c_0) (p1 c_0 c_0) (not (p3 c_2)) (not (p3 c_0)) (= c_2 c_0) (not (p1 c_2 c_0)) (not (p4 c_0)) (= c_2 c_2) (not (p14 c_2 c_2 c_0)) )(or (not (p3 c_2)) (not (p1 c_2 c_0)) (= c_2 c_1) (p1 c_1 c_0) (not (p3 c_2)) (not (p3 c_1)) (= c_2 c_1) (not (p1 c_2 c_0)) (not (p4 c_0)) (= c_2 c_2) (not (p14 c_2 c_2 c_1)) )(or (not (p3 c_2)) (not (p1 c_2 c_0)) (= c_2 c_2) (p1 c_2 c_0) (not (p3 c_2)) (not (p3 c_2)) (= c_2 c_2) (not (p1 c_2 c_0)) (not (p4 c_0)) (= c_2 c_2) (not (p14 c_2 c_2 c_2)) )(or (not (p3 c_2)) (not (p1 c_2 c_0)) (= c_2 c_3) (p1 c_3 c_0) (not (p3 c_2)) (not (p3 c_3)) (= c_2 c_3) (not (p1 c_2 c_0)) (not (p4 c_0)) (= c_2 c_2) (not (p14 c_2 c_2 c_3)) )(or (not (p3 c_2)) (not (p1 c_2 c_1)) (= c_2 c_0) (p1 c_0 c_1) (not (p3 c_2)) (not (p3 c_0)) (= c_2 c_0) (not (p1 c_2 c_1)) (not (p4 c_1)) (= c_2 c_2) (not (p14 c_2 c_2 c_0)) )(or (not (p3 c_2)) (not (p1 c_2 c_1)) (= c_2 c_1) (p1 c_1 c_1) (not (p3 c_2)) (not (p3 c_1)) (= c_2 c_1) (not (p1 c_2 c_1)) (not (p4 c_1)) (= c_2 c_2) (not (p14 c_2 c_2 c_1)) )(or (not (p3 c_2)) (not (p1 c_2 c_1)) (= c_2 c_2) (p1 c_2 c_1) (not (p3 c_2)) (not (p3 c_2)) (= c_2 c_2) (not (p1 c_2 c_1)) (not (p4 c_1)) (= c_2 c_2) (not (p14 c_2 c_2 c_2)) )(or (not (p3 c_2)) (not (p1 c_2 c_1)) (= c_2 c_3) (p1 c_3 c_1) (not (p3 c_2)) (not (p3 c_3)) (= c_2 c_3) (not (p1 c_2 c_1)) (not (p4 c_1)) (= c_2 c_2) (not (p14 c_2 c_2 c_3)) )(or (not (p3 c_2)) (not (p1 c_2 c_2)) (= c_2 c_0) (p1 c_0 c_2) (not (p3 c_2)) (not (p3 c_0)) (= c_2 c_0) (not (p1 c_2 c_2)) (not (p4 c_2)) (= c_2 c_2) (not (p14 c_2 c_2 c_0)) )(or (not (p3 c_2)) (not (p1 c_2 c_2)) (= c_2 c_1) (p1 c_1 c_2) (not (p3 c_2)) (not (p3 c_1)) (= c_2 c_1) (not (p1 c_2 c_2)) (not (p4 c_2)) (= c_2 c_2) (not (p14 c_2 c_2 c_1)) )(or (not (p3 c_2)) (not (p1 c_2 c_2)) (= c_2 c_2) (p1 c_2 c_2) (not (p3 c_2)) (not (p3 c_2)) (= c_2 c_2) (not (p1 c_2 c_2)) (not (p4 c_2)) (= c_2 c_2) (not (p14 c_2 c_2 c_2)) )(or (not (p3 c_2)) (not (p1 c_2 c_2)) (= c_2 c_3) (p1 c_3 c_2) (not (p3 c_2)) (not (p3 c_3)) (= c_2 c_3) (not (p1 c_2 c_2)) (not (p4 c_2)) (= c_2 c_2) (not (p14 c_2 c_2 c_3)) )(or (not (p3 c_2)) (not (p1 c_2 c_3)) (= c_2 c_0) (p1 c_0 c_3) (not (p3 c_2)) (not (p3 c_0)) (= c_2 c_0) (not (p1 c_2 c_3)) (not (p4 c_3)) (= c_2 c_2) (not (p14 c_2 c_2 c_0)) )(or (not (p3 c_2)) (not (p1 c_2 c_3)) (= c_2 c_1) (p1 c_1 c_3) (not (p3 c_2)) (not (p3 c_1)) (= c_2 c_1) (not (p1 c_2 c_3)) (not (p4 c_3)) (= c_2 c_2) (not (p14 c_2 c_2 c_1)) )(or (not (p3 c_2)) (not (p1 c_2 c_3)) (= c_2 c_2) (p1 c_2 c_3) (not (p3 c_2)) (not (p3 c_2)) (= c_2 c_2) (not (p1 c_2 c_3)) (not (p4 c_3)) (= c_2 c_2) (not (p14 c_2 c_2 c_2)) )(or (not (p3 c_2)) (not (p1 c_2 c_3)) (= c_2 c_3) (p1 c_3 c_3) (not (p3 c_2)) (not (p3 c_3)) (= c_2 c_3) (not (p1 c_2 c_3)) (not (p4 c_3)) (= c_2 c_2) (not (p14 c_2 c_2 c_3)) )(or (not (p3 c_2)) (not (p1 c_3 c_0)) (= c_3 c_0) (p1 c_0 c_0) (not (p3 c_3)) (not (p3 c_0)) (= c_2 c_0) (not (p1 c_2 c_0)) (not (p4 c_0)) (= c_3 c_2) (not (p14 c_3 c_2 c_0)) )(or (not (p3 c_2)) (not (p1 c_3 c_0)) (= c_3 c_1) (p1 c_1 c_0) (not (p3 c_3)) (not (p3 c_1)) (= c_2 c_1) (not (p1 c_2 c_0)) (not (p4 c_0)) (= c_3 c_2) (not (p14 c_3 c_2 c_1)) )(or (not (p3 c_2)) (not (p1 c_3 c_0)) (= c_3 c_2) (p1 c_2 c_0) (not (p3 c_3)) (not (p3 c_2)) (= c_2 c_2) (not (p1 c_2 c_0)) (not (p4 c_0)) (= c_3 c_2) (not (p14 c_3 c_2 c_2)) )(or (not (p3 c_2)) (not (p1 c_3 c_0)) (= c_3 c_3) (p1 c_3 c_0) (not (p3 c_3)) (not (p3 c_3)) (= c_2 c_3) (not (p1 c_2 c_0)) (not (p4 c_0)) (= c_3 c_2) (not (p14 c_3 c_2 c_3)) )(or (not (p3 c_2)) (not (p1 c_3 c_1)) (= c_3 c_0) (p1 c_0 c_1) (not (p3 c_3)) (not (p3 c_0)) (= c_2 c_0) (not (p1 c_2 c_1)) (not (p4 c_1)) (= c_3 c_2) (not (p14 c_3 c_2 c_0)) )(or (not (p3 c_2)) (not (p1 c_3 c_1)) (= c_3 c_1) (p1 c_1 c_1) (not (p3 c_3)) (not (p3 c_1)) (= c_2 c_1) (not (p1 c_2 c_1)) (not (p4 c_1)) (= c_3 c_2) (not (p14 c_3 c_2 c_1)) )(or (not (p3 c_2)) (not (p1 c_3 c_1)) (= c_3 c_2) (p1 c_2 c_1) (not (p3 c_3)) (not (p3 c_2)) (= c_2 c_2) (not (p1 c_2 c_1)) (not (p4 c_1)) (= c_3 c_2) (not (p14 c_3 c_2 c_2)) )(or (not (p3 c_2)) (not (p1 c_3 c_1)) (= c_3 c_3) (p1 c_3 c_1) (not (p3 c_3)) (not (p3 c_3)) (= c_2 c_3) (not (p1 c_2 c_1)) (not (p4 c_1)) (= c_3 c_2) (not (p14 c_3 c_2 c_3)) )(or (not (p3 c_2)) (not (p1 c_3 c_2)) (= c_3 c_0) (p1 c_0 c_2) (not (p3 c_3)) (not (p3 c_0)) (= c_2 c_0) (not (p1 c_2 c_2)) (not (p4 c_2)) (= c_3 c_2) (not (p14 c_3 c_2 c_0)) )(or (not (p3 c_2)) (not (p1 c_3 c_2)) (= c_3 c_1) (p1 c_1 c_2) (not (p3 c_3)) (not (p3 c_1)) (= c_2 c_1) (not (p1 c_2 c_2)) (not (p4 c_2)) (= c_3 c_2) (not (p14 c_3 c_2 c_1)) )(or (not (p3 c_2)) (not (p1 c_3 c_2)) (= c_3 c_2) (p1 c_2 c_2) (not (p3 c_3)) (not (p3 c_2)) (= c_2 c_2) (not (p1 c_2 c_2)) (not (p4 c_2)) (= c_3 c_2) (not (p14 c_3 c_2 c_2)) )(or (not (p3 c_2)) (not (p1 c_3 c_2)) (= c_3 c_3) (p1 c_3 c_2) (not (p3 c_3)) (not (p3 c_3)) (= c_2 c_3) (not (p1 c_2 c_2)) (not (p4 c_2)) (= c_3 c_2) (not (p14 c_3 c_2 c_3)) )(or (not (p3 c_2)) (not (p1 c_3 c_3)) (= c_3 c_0) (p1 c_0 c_3) (not (p3 c_3)) (not (p3 c_0)) (= c_2 c_0) (not (p1 c_2 c_3)) (not (p4 c_3)) (= c_3 c_2) (not (p14 c_3 c_2 c_0)) )(or (not (p3 c_2)) (not (p1 c_3 c_3)) (= c_3 c_1) (p1 c_1 c_3) (not (p3 c_3)) (not (p3 c_1)) (= c_2 c_1) (not (p1 c_2 c_3)) (not (p4 c_3)) (= c_3 c_2) (not (p14 c_3 c_2 c_1)) )(or (not (p3 c_2)) (not (p1 c_3 c_3)) (= c_3 c_2) (p1 c_2 c_3) (not (p3 c_3)) (not (p3 c_2)) (= c_2 c_2) (not (p1 c_2 c_3)) (not (p4 c_3)) (= c_3 c_2) (not (p14 c_3 c_2 c_2)) )(or (not (p3 c_2)) (not (p1 c_3 c_3)) (= c_3 c_3) (p1 c_3 c_3) (not (p3 c_3)) (not (p3 c_3)) (= c_2 c_3) (not (p1 c_2 c_3)) (not (p4 c_3)) (= c_3 c_2) (not (p14 c_3 c_2 c_3)) )(or (not (p3 c_3)) (not (p1 c_0 c_0)) (= c_0 c_0) (p1 c_0 c_0) (not (p3 c_0)) (not (p3 c_0)) (= c_3 c_0) (not (p1 c_3 c_0)) (not (p4 c_0)) (= c_0 c_3) (not (p14 c_0 c_3 c_0)) )(or (not (p3 c_3)) (not (p1 c_0 c_0)) (= c_0 c_1) (p1 c_1 c_0) (not (p3 c_0)) (not (p3 c_1)) (= c_3 c_1) (not (p1 c_3 c_0)) (not (p4 c_0)) (= c_0 c_3) (not (p14 c_0 c_3 c_1)) )(or (not (p3 c_3)) (not (p1 c_0 c_0)) (= c_0 c_2) (p1 c_2 c_0) (not (p3 c_0)) (not (p3 c_2)) (= c_3 c_2) (not (p1 c_3 c_0)) (not (p4 c_0)) (= c_0 c_3) (not (p14 c_0 c_3 c_2)) )(or (not (p3 c_3)) (not (p1 c_0 c_0)) (= c_0 c_3) (p1 c_3 c_0) (not (p3 c_0)) (not (p3 c_3)) (= c_3 c_3) (not (p1 c_3 c_0)) (not (p4 c_0)) (= c_0 c_3) (not (p14 c_0 c_3 c_3)) )(or (not (p3 c_3)) (not (p1 c_0 c_1)) (= c_0 c_0) (p1 c_0 c_1) (not (p3 c_0)) (not (p3 c_0)) (= c_3 c_0) (not (p1 c_3 c_1)) (not (p4 c_1)) (= c_0 c_3) (not (p14 c_0 c_3 c_0)) )(or (not (p3 c_3)) (not (p1 c_0 c_1)) (= c_0 c_1) (p1 c_1 c_1) (not (p3 c_0)) (not (p3 c_1)) (= c_3 c_1) (not (p1 c_3 c_1)) (not (p4 c_1)) (= c_0 c_3) (not (p14 c_0 c_3 c_1)) )(or (not (p3 c_3)) (not (p1 c_0 c_1)) (= c_0 c_2) (p1 c_2 c_1) (not (p3 c_0)) (not (p3 c_2)) (= c_3 c_2) (not (p1 c_3 c_1)) (not (p4 c_1)) (= c_0 c_3) (not (p14 c_0 c_3 c_2)) )(or (not (p3 c_3)) (not (p1 c_0 c_1)) (= c_0 c_3) (p1 c_3 c_1) (not (p3 c_0)) (not (p3 c_3)) (= c_3 c_3) (not (p1 c_3 c_1)) (not (p4 c_1)) (= c_0 c_3) (not (p14 c_0 c_3 c_3)) )(or (not (p3 c_3)) (not (p1 c_0 c_2)) (= c_0 c_0) (p1 c_0 c_2) (not (p3 c_0)) (not (p3 c_0)) (= c_3 c_0) (not (p1 c_3 c_2)) (not (p4 c_2)) (= c_0 c_3) (not (p14 c_0 c_3 c_0)) )(or (not (p3 c_3)) (not (p1 c_0 c_2)) (= c_0 c_1) (p1 c_1 c_2) (not (p3 c_0)) (not (p3 c_1)) (= c_3 c_1) (not (p1 c_3 c_2)) (not (p4 c_2)) (= c_0 c_3) (not (p14 c_0 c_3 c_1)) )(or (not (p3 c_3)) (not (p1 c_0 c_2)) (= c_0 c_2) (p1 c_2 c_2) (not (p3 c_0)) (not (p3 c_2)) (= c_3 c_2) (not (p1 c_3 c_2)) (not (p4 c_2)) (= c_0 c_3) (not (p14 c_0 c_3 c_2)) )(or (not (p3 c_3)) (not (p1 c_0 c_2)) (= c_0 c_3) (p1 c_3 c_2) (not (p3 c_0)) (not (p3 c_3)) (= c_3 c_3) (not (p1 c_3 c_2)) (not (p4 c_2)) (= c_0 c_3) (not (p14 c_0 c_3 c_3)) )(or (not (p3 c_3)) (not (p1 c_0 c_3)) (= c_0 c_0) (p1 c_0 c_3) (not (p3 c_0)) (not (p3 c_0)) (= c_3 c_0) (not (p1 c_3 c_3)) (not (p4 c_3)) (= c_0 c_3) (not (p14 c_0 c_3 c_0)) )(or (not (p3 c_3)) (not (p1 c_0 c_3)) (= c_0 c_1) (p1 c_1 c_3) (not (p3 c_0)) (not (p3 c_1)) (= c_3 c_1) (not (p1 c_3 c_3)) (not (p4 c_3)) (= c_0 c_3) (not (p14 c_0 c_3 c_1)) )(or (not (p3 c_3)) (not (p1 c_0 c_3)) (= c_0 c_2) (p1 c_2 c_3) (not (p3 c_0)) (not (p3 c_2)) (= c_3 c_2) (not (p1 c_3 c_3)) (not (p4 c_3)) (= c_0 c_3) (not (p14 c_0 c_3 c_2)) )(or (not (p3 c_3)) (not (p1 c_0 c_3)) (= c_0 c_3) (p1 c_3 c_3) (not (p3 c_0)) (not (p3 c_3)) (= c_3 c_3) (not (p1 c_3 c_3)) (not (p4 c_3)) (= c_0 c_3) (not (p14 c_0 c_3 c_3)) )(or (not (p3 c_3)) (not (p1 c_1 c_0)) (= c_1 c_0) (p1 c_0 c_0) (not (p3 c_1)) (not (p3 c_0)) (= c_3 c_0) (not (p1 c_3 c_0)) (not (p4 c_0)) (= c_1 c_3) (not (p14 c_1 c_3 c_0)) )(or (not (p3 c_3)) (not (p1 c_1 c_0)) (= c_1 c_1) (p1 c_1 c_0) (not (p3 c_1)) (not (p3 c_1)) (= c_3 c_1) (not (p1 c_3 c_0)) (not (p4 c_0)) (= c_1 c_3) (not (p14 c_1 c_3 c_1)) )(or (not (p3 c_3)) (not (p1 c_1 c_0)) (= c_1 c_2) (p1 c_2 c_0) (not (p3 c_1)) (not (p3 c_2)) (= c_3 c_2) (not (p1 c_3 c_0)) (not (p4 c_0)) (= c_1 c_3) (not (p14 c_1 c_3 c_2)) )(or (not (p3 c_3)) (not (p1 c_1 c_0)) (= c_1 c_3) (p1 c_3 c_0) (not (p3 c_1)) (not (p3 c_3)) (= c_3 c_3) (not (p1 c_3 c_0)) (not (p4 c_0)) (= c_1 c_3) (not (p14 c_1 c_3 c_3)) )(or (not (p3 c_3)) (not (p1 c_1 c_1)) (= c_1 c_0) (p1 c_0 c_1) (not (p3 c_1)) (not (p3 c_0)) (= c_3 c_0) (not (p1 c_3 c_1)) (not (p4 c_1)) (= c_1 c_3) (not (p14 c_1 c_3 c_0)) )(or (not (p3 c_3)) (not (p1 c_1 c_1)) (= c_1 c_1) (p1 c_1 c_1) (not (p3 c_1)) (not (p3 c_1)) (= c_3 c_1) (not (p1 c_3 c_1)) (not (p4 c_1)) (= c_1 c_3) (not (p14 c_1 c_3 c_1)) )(or (not (p3 c_3)) (not (p1 c_1 c_1)) (= c_1 c_2) (p1 c_2 c_1) (not (p3 c_1)) (not (p3 c_2)) (= c_3 c_2) (not (p1 c_3 c_1)) (not (p4 c_1)) (= c_1 c_3) (not (p14 c_1 c_3 c_2)) )(or (not (p3 c_3)) (not (p1 c_1 c_1)) (= c_1 c_3) (p1 c_3 c_1) (not (p3 c_1)) (not (p3 c_3)) (= c_3 c_3) (not (p1 c_3 c_1)) (not (p4 c_1)) (= c_1 c_3) (not (p14 c_1 c_3 c_3)) )(or (not (p3 c_3)) (not (p1 c_1 c_2)) (= c_1 c_0) (p1 c_0 c_2) (not (p3 c_1)) (not (p3 c_0)) (= c_3 c_0) (not (p1 c_3 c_2)) (not (p4 c_2)) (= c_1 c_3) (not (p14 c_1 c_3 c_0)) )(or (not (p3 c_3)) (not (p1 c_1 c_2)) (= c_1 c_1) (p1 c_1 c_2) (not (p3 c_1)) (not (p3 c_1)) (= c_3 c_1) (not (p1 c_3 c_2)) (not (p4 c_2)) (= c_1 c_3) (not (p14 c_1 c_3 c_1)) )(or (not (p3 c_3)) (not (p1 c_1 c_2)) (= c_1 c_2) (p1 c_2 c_2) (not (p3 c_1)) (not (p3 c_2)) (= c_3 c_2) (not (p1 c_3 c_2)) (not (p4 c_2)) (= c_1 c_3) (not (p14 c_1 c_3 c_2)) )(or (not (p3 c_3)) (not (p1 c_1 c_2)) (= c_1 c_3) (p1 c_3 c_2) (not (p3 c_1)) (not (p3 c_3)) (= c_3 c_3) (not (p1 c_3 c_2)) (not (p4 c_2)) (= c_1 c_3) (not (p14 c_1 c_3 c_3)) )(or (not (p3 c_3)) (not (p1 c_1 c_3)) (= c_1 c_0) (p1 c_0 c_3) (not (p3 c_1)) (not (p3 c_0)) (= c_3 c_0) (not (p1 c_3 c_3)) (not (p4 c_3)) (= c_1 c_3) (not (p14 c_1 c_3 c_0)) )(or (not (p3 c_3)) (not (p1 c_1 c_3)) (= c_1 c_1) (p1 c_1 c_3) (not (p3 c_1)) (not (p3 c_1)) (= c_3 c_1) (not (p1 c_3 c_3)) (not (p4 c_3)) (= c_1 c_3) (not (p14 c_1 c_3 c_1)) )(or (not (p3 c_3)) (not (p1 c_1 c_3)) (= c_1 c_2) (p1 c_2 c_3) (not (p3 c_1)) (not (p3 c_2)) (= c_3 c_2) (not (p1 c_3 c_3)) (not (p4 c_3)) (= c_1 c_3) (not (p14 c_1 c_3 c_2)) )(or (not (p3 c_3)) (not (p1 c_1 c_3)) (= c_1 c_3) (p1 c_3 c_3) (not (p3 c_1)) (not (p3 c_3)) (= c_3 c_3) (not (p1 c_3 c_3)) (not (p4 c_3)) (= c_1 c_3) (not (p14 c_1 c_3 c_3)) )(or (not (p3 c_3)) (not (p1 c_2 c_0)) (= c_2 c_0) (p1 c_0 c_0) (not (p3 c_2)) (not (p3 c_0)) (= c_3 c_0) (not (p1 c_3 c_0)) (not (p4 c_0)) (= c_2 c_3) (not (p14 c_2 c_3 c_0)) )(or (not (p3 c_3)) (not (p1 c_2 c_0)) (= c_2 c_1) (p1 c_1 c_0) (not (p3 c_2)) (not (p3 c_1)) (= c_3 c_1) (not (p1 c_3 c_0)) (not (p4 c_0)) (= c_2 c_3) (not (p14 c_2 c_3 c_1)) )(or (not (p3 c_3)) (not (p1 c_2 c_0)) (= c_2 c_2) (p1 c_2 c_0) (not (p3 c_2)) (not (p3 c_2)) (= c_3 c_2) (not (p1 c_3 c_0)) (not (p4 c_0)) (= c_2 c_3) (not (p14 c_2 c_3 c_2)) )(or (not (p3 c_3)) (not (p1 c_2 c_0)) (= c_2 c_3) (p1 c_3 c_0) (not (p3 c_2)) (not (p3 c_3)) (= c_3 c_3) (not (p1 c_3 c_0)) (not (p4 c_0)) (= c_2 c_3) (not (p14 c_2 c_3 c_3)) )(or (not (p3 c_3)) (not (p1 c_2 c_1)) (= c_2 c_0) (p1 c_0 c_1) (not (p3 c_2)) (not (p3 c_0)) (= c_3 c_0) (not (p1 c_3 c_1)) (not (p4 c_1)) (= c_2 c_3) (not (p14 c_2 c_3 c_0)) )(or (not (p3 c_3)) (not (p1 c_2 c_1)) (= c_2 c_1) (p1 c_1 c_1) (not (p3 c_2)) (not (p3 c_1)) (= c_3 c_1) (not (p1 c_3 c_1)) (not (p4 c_1)) (= c_2 c_3) (not (p14 c_2 c_3 c_1)) )(or (not (p3 c_3)) (not (p1 c_2 c_1)) (= c_2 c_2) (p1 c_2 c_1) (not (p3 c_2)) (not (p3 c_2)) (= c_3 c_2) (not (p1 c_3 c_1)) (not (p4 c_1)) (= c_2 c_3) (not (p14 c_2 c_3 c_2)) )(or (not (p3 c_3)) (not (p1 c_2 c_1)) (= c_2 c_3) (p1 c_3 c_1) (not (p3 c_2)) (not (p3 c_3)) (= c_3 c_3) (not (p1 c_3 c_1)) (not (p4 c_1)) (= c_2 c_3) (not (p14 c_2 c_3 c_3)) )(or (not (p3 c_3)) (not (p1 c_2 c_2)) (= c_2 c_0) (p1 c_0 c_2) (not (p3 c_2)) (not (p3 c_0)) (= c_3 c_0) (not (p1 c_3 c_2)) (not (p4 c_2)) (= c_2 c_3) (not (p14 c_2 c_3 c_0)) )(or (not (p3 c_3)) (not (p1 c_2 c_2)) (= c_2 c_1) (p1 c_1 c_2) (not (p3 c_2)) (not (p3 c_1)) (= c_3 c_1) (not (p1 c_3 c_2)) (not (p4 c_2)) (= c_2 c_3) (not (p14 c_2 c_3 c_1)) )(or (not (p3 c_3)) (not (p1 c_2 c_2)) (= c_2 c_2) (p1 c_2 c_2) (not (p3 c_2)) (not (p3 c_2)) (= c_3 c_2) (not (p1 c_3 c_2)) (not (p4 c_2)) (= c_2 c_3) (not (p14 c_2 c_3 c_2)) )(or (not (p3 c_3)) (not (p1 c_2 c_2)) (= c_2 c_3) (p1 c_3 c_2) (not (p3 c_2)) (not (p3 c_3)) (= c_3 c_3) (not (p1 c_3 c_2)) (not (p4 c_2)) (= c_2 c_3) (not (p14 c_2 c_3 c_3)) )(or (not (p3 c_3)) (not (p1 c_2 c_3)) (= c_2 c_0) (p1 c_0 c_3) (not (p3 c_2)) (not (p3 c_0)) (= c_3 c_0) (not (p1 c_3 c_3)) (not (p4 c_3)) (= c_2 c_3) (not (p14 c_2 c_3 c_0)) )(or (not (p3 c_3)) (not (p1 c_2 c_3)) (= c_2 c_1) (p1 c_1 c_3) (not (p3 c_2)) (not (p3 c_1)) (= c_3 c_1) (not (p1 c_3 c_3)) (not (p4 c_3)) (= c_2 c_3) (not (p14 c_2 c_3 c_1)) )(or (not (p3 c_3)) (not (p1 c_2 c_3)) (= c_2 c_2) (p1 c_2 c_3) (not (p3 c_2)) (not (p3 c_2)) (= c_3 c_2) (not (p1 c_3 c_3)) (not (p4 c_3)) (= c_2 c_3) (not (p14 c_2 c_3 c_2)) )(or (not (p3 c_3)) (not (p1 c_2 c_3)) (= c_2 c_3) (p1 c_3 c_3) (not (p3 c_2)) (not (p3 c_3)) (= c_3 c_3) (not (p1 c_3 c_3)) (not (p4 c_3)) (= c_2 c_3) (not (p14 c_2 c_3 c_3)) )(or (not (p3 c_3)) (not (p1 c_3 c_0)) (= c_3 c_0) (p1 c_0 c_0) (not (p3 c_3)) (not (p3 c_0)) (= c_3 c_0) (not (p1 c_3 c_0)) (not (p4 c_0)) (= c_3 c_3) (not (p14 c_3 c_3 c_0)) )(or (not (p3 c_3)) (not (p1 c_3 c_0)) (= c_3 c_1) (p1 c_1 c_0) (not (p3 c_3)) (not (p3 c_1)) (= c_3 c_1) (not (p1 c_3 c_0)) (not (p4 c_0)) (= c_3 c_3) (not (p14 c_3 c_3 c_1)) )(or (not (p3 c_3)) (not (p1 c_3 c_0)) (= c_3 c_2) (p1 c_2 c_0) (not (p3 c_3)) (not (p3 c_2)) (= c_3 c_2) (not (p1 c_3 c_0)) (not (p4 c_0)) (= c_3 c_3) (not (p14 c_3 c_3 c_2)) )(or (not (p3 c_3)) (not (p1 c_3 c_0)) (= c_3 c_3) (p1 c_3 c_0) (not (p3 c_3)) (not (p3 c_3)) (= c_3 c_3) (not (p1 c_3 c_0)) (not (p4 c_0)) (= c_3 c_3) (not (p14 c_3 c_3 c_3)) )(or (not (p3 c_3)) (not (p1 c_3 c_1)) (= c_3 c_0) (p1 c_0 c_1) (not (p3 c_3)) (not (p3 c_0)) (= c_3 c_0) (not (p1 c_3 c_1)) (not (p4 c_1)) (= c_3 c_3) (not (p14 c_3 c_3 c_0)) )(or (not (p3 c_3)) (not (p1 c_3 c_1)) (= c_3 c_1) (p1 c_1 c_1) (not (p3 c_3)) (not (p3 c_1)) (= c_3 c_1) (not (p1 c_3 c_1)) (not (p4 c_1)) (= c_3 c_3) (not (p14 c_3 c_3 c_1)) )(or (not (p3 c_3)) (not (p1 c_3 c_1)) (= c_3 c_2) (p1 c_2 c_1) (not (p3 c_3)) (not (p3 c_2)) (= c_3 c_2) (not (p1 c_3 c_1)) (not (p4 c_1)) (= c_3 c_3) (not (p14 c_3 c_3 c_2)) )(or (not (p3 c_3)) (not (p1 c_3 c_1)) (= c_3 c_3) (p1 c_3 c_1) (not (p3 c_3)) (not (p3 c_3)) (= c_3 c_3) (not (p1 c_3 c_1)) (not (p4 c_1)) (= c_3 c_3) (not (p14 c_3 c_3 c_3)) )(or (not (p3 c_3)) (not (p1 c_3 c_2)) (= c_3 c_0) (p1 c_0 c_2) (not (p3 c_3)) (not (p3 c_0)) (= c_3 c_0) (not (p1 c_3 c_2)) (not (p4 c_2)) (= c_3 c_3) (not (p14 c_3 c_3 c_0)) )(or (not (p3 c_3)) (not (p1 c_3 c_2)) (= c_3 c_1) (p1 c_1 c_2) (not (p3 c_3)) (not (p3 c_1)) (= c_3 c_1) (not (p1 c_3 c_2)) (not (p4 c_2)) (= c_3 c_3) (not (p14 c_3 c_3 c_1)) )(or (not (p3 c_3)) (not (p1 c_3 c_2)) (= c_3 c_2) (p1 c_2 c_2) (not (p3 c_3)) (not (p3 c_2)) (= c_3 c_2) (not (p1 c_3 c_2)) (not (p4 c_2)) (= c_3 c_3) (not (p14 c_3 c_3 c_2)) )(or (not (p3 c_3)) (not (p1 c_3 c_2)) (= c_3 c_3) (p1 c_3 c_2) (not (p3 c_3)) (not (p3 c_3)) (= c_3 c_3) (not (p1 c_3 c_2)) (not (p4 c_2)) (= c_3 c_3) (not (p14 c_3 c_3 c_3)) )(or (not (p3 c_3)) (not (p1 c_3 c_3)) (= c_3 c_0) (p1 c_0 c_3) (not (p3 c_3)) (not (p3 c_0)) (= c_3 c_0) (not (p1 c_3 c_3)) (not (p4 c_3)) (= c_3 c_3) (not (p14 c_3 c_3 c_0)) )(or (not (p3 c_3)) (not (p1 c_3 c_3)) (= c_3 c_1) (p1 c_1 c_3) (not (p3 c_3)) (not (p3 c_1)) (= c_3 c_1) (not (p1 c_3 c_3)) (not (p4 c_3)) (= c_3 c_3) (not (p14 c_3 c_3 c_1)) )(or (not (p3 c_3)) (not (p1 c_3 c_3)) (= c_3 c_2) (p1 c_2 c_3) (not (p3 c_3)) (not (p3 c_2)) (= c_3 c_2) (not (p1 c_3 c_3)) (not (p4 c_3)) (= c_3 c_3) (not (p14 c_3 c_3 c_2)) )(or (not (p3 c_3)) (not (p1 c_3 c_3)) (= c_3 c_3) (p1 c_3 c_3) (not (p3 c_3)) (not (p3 c_3)) (= c_3 c_3) (not (p1 c_3 c_3)) (not (p4 c_3)) (= c_3 c_3) (not (p14 c_3 c_3 c_3)) )(or (not (p9 c_0)) (p3 (f12 c_0)) )(or (not (p9 c_1)) (p3 (f12 c_1)) )(or (not (p9 c_2)) (p3 (f12 c_2)) )(or (not (p9 c_3)) (p3 (f12 c_3)) )(or (not (p4 c_0)) (p1 (f6 c_0) c_0) )(or (not (p4 c_1)) (p1 (f6 c_1) c_1) )(or (not (p4 c_2)) (p1 (f6 c_2) c_2) )(or (not (p4 c_3)) (p1 (f6 c_3) c_3) )(or (not (p3 c_0)) (p4 (f2 c_0 c_0)) (= c_0 c_0) (not (p3 c_0)) )(or (not (p3 c_0)) (p4 (f2 c_0 c_1)) (= c_0 c_1) (not (p3 c_1)) )(or (not (p3 c_0)) (p4 (f2 c_0 c_2)) (= c_0 c_2) (not (p3 c_2)) )(or (not (p3 c_0)) (p4 (f2 c_0 c_3)) (= c_0 c_3) (not (p3 c_3)) )(or (not (p3 c_1)) (p4 (f2 c_1 c_0)) (= c_1 c_0) (not (p3 c_0)) )(or (not (p3 c_1)) (p4 (f2 c_1 c_1)) (= c_1 c_1) (not (p3 c_1)) )(or (not (p3 c_1)) (p4 (f2 c_1 c_2)) (= c_1 c_2) (not (p3 c_2)) )(or (not (p3 c_1)) (p4 (f2 c_1 c_3)) (= c_1 c_3) (not (p3 c_3)) )(or (not (p3 c_2)) (p4 (f2 c_2 c_0)) (= c_2 c_0) (not (p3 c_0)) )(or (not (p3 c_2)) (p4 (f2 c_2 c_1)) (= c_2 c_1) (not (p3 c_1)) )(or (not (p3 c_2)) (p4 (f2 c_2 c_2)) (= c_2 c_2) (not (p3 c_2)) )(or (not (p3 c_2)) (p4 (f2 c_2 c_3)) (= c_2 c_3) (not (p3 c_3)) )(or (not (p3 c_3)) (p4 (f2 c_3 c_0)) (= c_3 c_0) (not (p3 c_0)) )(or (not (p3 c_3)) (p4 (f2 c_3 c_1)) (= c_3 c_1) (not (p3 c_1)) )(or (not (p3 c_3)) (p4 (f2 c_3 c_2)) (= c_3 c_2) (not (p3 c_2)) )(or (not (p3 c_3)) (p4 (f2 c_3 c_3)) (= c_3 c_3) (not (p3 c_3)) )(or (not (p4 c_0)) (not (p3 c_0)) (= c_0 c_0) (not (p3 c_0)) (= c_0 c_0) (not (p1 c_0 c_0)) (not (p1 c_0 c_0)) (not (p1 c_0 c_0)) (not (p4 c_0)) (not (p1 c_0 c_0)) )(or (not (p4 c_0)) (not (p3 c_0)) (= c_0 c_0) (not (p3 c_1)) (= c_0 c_1) (not (p1 c_1 c_0)) (not (p1 c_0 c_0)) (not (p1 c_1 c_0)) (not (p4 c_0)) (not (p1 c_0 c_0)) )(or (not (p4 c_0)) (not (p3 c_0)) (= c_0 c_0) (not (p3 c_2)) (= c_0 c_2) (not (p1 c_2 c_0)) (not (p1 c_0 c_0)) (not (p1 c_2 c_0)) (not (p4 c_0)) (not (p1 c_0 c_0)) )(or (not (p4 c_0)) (not (p3 c_0)) (= c_0 c_0) (not (p3 c_3)) (= c_0 c_3) (not (p1 c_3 c_0)) (not (p1 c_0 c_0)) (not (p1 c_3 c_0)) (not (p4 c_0)) (not (p1 c_0 c_0)) )(or (not (p4 c_0)) (not (p3 c_0)) (= c_1 c_0) (not (p3 c_0)) (= c_0 c_0) (not (p1 c_0 c_0)) (not (p1 c_0 c_1)) (not (p1 c_0 c_1)) (not (p4 c_1)) (not (p1 c_0 c_0)) )(or (not (p4 c_0)) (not (p3 c_0)) (= c_1 c_0) (not (p3 c_1)) (= c_0 c_1) (not (p1 c_1 c_0)) (not (p1 c_0 c_1)) (not (p1 c_1 c_1)) (not (p4 c_1)) (not (p1 c_0 c_0)) )(or (not (p4 c_0)) (not (p3 c_0)) (= c_1 c_0) (not (p3 c_2)) (= c_0 c_2) (not (p1 c_2 c_0)) (not (p1 c_0 c_1)) (not (p1 c_2 c_1)) (not (p4 c_1)) (not (p1 c_0 c_0)) )(or (not (p4 c_0)) (not (p3 c_0)) (= c_1 c_0) (not (p3 c_3)) (= c_0 c_3) (not (p1 c_3 c_0)) (not (p1 c_0 c_1)) (not (p1 c_3 c_1)) (not (p4 c_1)) (not (p1 c_0 c_0)) )(or (not (p4 c_0)) (not (p3 c_0)) (= c_2 c_0) (not (p3 c_0)) (= c_0 c_0) (not (p1 c_0 c_0)) (not (p1 c_0 c_2)) (not (p1 c_0 c_2)) (not (p4 c_2)) (not (p1 c_0 c_0)) )(or (not (p4 c_0)) (not (p3 c_0)) (= c_2 c_0) (not (p3 c_1)) (= c_0 c_1) (not (p1 c_1 c_0)) (not (p1 c_0 c_2)) (not (p1 c_1 c_2)) (not (p4 c_2)) (not (p1 c_0 c_0)) )(or (not (p4 c_0)) (not (p3 c_0)) (= c_2 c_0) (not (p3 c_2)) (= c_0 c_2) (not (p1 c_2 c_0)) (not (p1 c_0 c_2)) (not (p1 c_2 c_2)) (not (p4 c_2)) (not (p1 c_0 c_0)) )(or (not (p4 c_0)) (not (p3 c_0)) (= c_2 c_0) (not (p3 c_3)) (= c_0 c_3) (not (p1 c_3 c_0)) (not (p1 c_0 c_2)) (not (p1 c_3 c_2)) (not (p4 c_2)) (not (p1 c_0 c_0)) )(or (not (p4 c_0)) (not (p3 c_0)) (= c_3 c_0) (not (p3 c_0)) (= c_0 c_0) (not (p1 c_0 c_0)) (not (p1 c_0 c_3)) (not (p1 c_0 c_3)) (not (p4 c_3)) (not (p1 c_0 c_0)) )(or (not (p4 c_0)) (not (p3 c_0)) (= c_3 c_0) (not (p3 c_1)) (= c_0 c_1) (not (p1 c_1 c_0)) (not (p1 c_0 c_3)) (not (p1 c_1 c_3)) (not (p4 c_3)) (not (p1 c_0 c_0)) )(or (not (p4 c_0)) (not (p3 c_0)) (= c_3 c_0) (not (p3 c_2)) (= c_0 c_2) (not (p1 c_2 c_0)) (not (p1 c_0 c_3)) (not (p1 c_2 c_3)) (not (p4 c_3)) (not (p1 c_0 c_0)) )(or (not (p4 c_0)) (not (p3 c_0)) (= c_3 c_0) (not (p3 c_3)) (= c_0 c_3) (not (p1 c_3 c_0)) (not (p1 c_0 c_3)) (not (p1 c_3 c_3)) (not (p4 c_3)) (not (p1 c_0 c_0)) )(or (not (p4 c_0)) (not (p3 c_1)) (= c_0 c_0) (not (p3 c_0)) (= c_1 c_0) (not (p1 c_0 c_0)) (not (p1 c_1 c_0)) (not (p1 c_0 c_0)) (not (p4 c_0)) (not (p1 c_1 c_0)) )(or (not (p4 c_0)) (not (p3 c_1)) (= c_0 c_0) (not (p3 c_1)) (= c_1 c_1) (not (p1 c_1 c_0)) (not (p1 c_1 c_0)) (not (p1 c_1 c_0)) (not (p4 c_0)) (not (p1 c_1 c_0)) )(or (not (p4 c_0)) (not (p3 c_1)) (= c_0 c_0) (not (p3 c_2)) (= c_1 c_2) (not (p1 c_2 c_0)) (not (p1 c_1 c_0)) (not (p1 c_2 c_0)) (not (p4 c_0)) (not (p1 c_1 c_0)) )(or (not (p4 c_0)) (not (p3 c_1)) (= c_0 c_0) (not (p3 c_3)) (= c_1 c_3) (not (p1 c_3 c_0)) (not (p1 c_1 c_0)) (not (p1 c_3 c_0)) (not (p4 c_0)) (not (p1 c_1 c_0)) )(or (not (p4 c_0)) (not (p3 c_1)) (= c_1 c_0) (not (p3 c_0)) (= c_1 c_0) (not (p1 c_0 c_0)) (not (p1 c_1 c_1)) (not (p1 c_0 c_1)) (not (p4 c_1)) (not (p1 c_1 c_0)) )(or (not (p4 c_0)) (not (p3 c_1)) (= c_1 c_0) (not (p3 c_1)) (= c_1 c_1) (not (p1 c_1 c_0)) (not (p1 c_1 c_1)) (not (p1 c_1 c_1)) (not (p4 c_1)) (not (p1 c_1 c_0)) )(or (not (p4 c_0)) (not (p3 c_1)) (= c_1 c_0) (not (p3 c_2)) (= c_1 c_2) (not (p1 c_2 c_0)) (not (p1 c_1 c_1)) (not (p1 c_2 c_1)) (not (p4 c_1)) (not (p1 c_1 c_0)) )(or (not (p4 c_0)) (not (p3 c_1)) (= c_1 c_0) (not (p3 c_3)) (= c_1 c_3) (not (p1 c_3 c_0)) (not (p1 c_1 c_1)) (not (p1 c_3 c_1)) (not (p4 c_1)) (not (p1 c_1 c_0)) )(or (not (p4 c_0)) (not (p3 c_1)) (= c_2 c_0) (not (p3 c_0)) (= c_1 c_0) (not (p1 c_0 c_0)) (not (p1 c_1 c_2)) (not (p1 c_0 c_2)) (not (p4 c_2)) (not (p1 c_1 c_0)) )(or (not (p4 c_0)) (not (p3 c_1)) (= c_2 c_0) (not (p3 c_1)) (= c_1 c_1) (not (p1 c_1 c_0)) (not (p1 c_1 c_2)) (not (p1 c_1 c_2)) (not (p4 c_2)) (not (p1 c_1 c_0)) )(or (not (p4 c_0)) (not (p3 c_1)) (= c_2 c_0) (not (p3 c_2)) (= c_1 c_2) (not (p1 c_2 c_0)) (not (p1 c_1 c_2)) (not (p1 c_2 c_2)) (not (p4 c_2)) (not (p1 c_1 c_0)) )(or (not (p4 c_0)) (not (p3 c_1)) (= c_2 c_0) (not (p3 c_3)) (= c_1 c_3) (not (p1 c_3 c_0)) (not (p1 c_1 c_2)) (not (p1 c_3 c_2)) (not (p4 c_2)) (not (p1 c_1 c_0)) )(or (not (p4 c_0)) (not (p3 c_1)) (= c_3 c_0) (not (p3 c_0)) (= c_1 c_0) (not (p1 c_0 c_0)) (not (p1 c_1 c_3)) (not (p1 c_0 c_3)) (not (p4 c_3)) (not (p1 c_1 c_0)) )(or (not (p4 c_0)) (not (p3 c_1)) (= c_3 c_0) (not (p3 c_1)) (= c_1 c_1) (not (p1 c_1 c_0)) (not (p1 c_1 c_3)) (not (p1 c_1 c_3)) (not (p4 c_3)) (not (p1 c_1 c_0)) )(or (not (p4 c_0)) (not (p3 c_1)) (= c_3 c_0) (not (p3 c_2)) (= c_1 c_2) (not (p1 c_2 c_0)) (not (p1 c_1 c_3)) (not (p1 c_2 c_3)) (not (p4 c_3)) (not (p1 c_1 c_0)) )(or (not (p4 c_0)) (not (p3 c_1)) (= c_3 c_0) (not (p3 c_3)) (= c_1 c_3) (not (p1 c_3 c_0)) (not (p1 c_1 c_3)) (not (p1 c_3 c_3)) (not (p4 c_3)) (not (p1 c_1 c_0)) )(or (not (p4 c_0)) (not (p3 c_2)) (= c_0 c_0) (not (p3 c_0)) (= c_2 c_0) (not (p1 c_0 c_0)) (not (p1 c_2 c_0)) (not (p1 c_0 c_0)) (not (p4 c_0)) (not (p1 c_2 c_0)) )(or (not (p4 c_0)) (not (p3 c_2)) (= c_0 c_0) (not (p3 c_1)) (= c_2 c_1) (not (p1 c_1 c_0)) (not (p1 c_2 c_0)) (not (p1 c_1 c_0)) (not (p4 c_0)) (not (p1 c_2 c_0)) )(or (not (p4 c_0)) (not (p3 c_2)) (= c_0 c_0) (not (p3 c_2)) (= c_2 c_2) (not (p1 c_2 c_0)) (not (p1 c_2 c_0)) (not (p1 c_2 c_0)) (not (p4 c_0)) (not (p1 c_2 c_0)) )(or (not (p4 c_0)) (not (p3 c_2)) (= c_0 c_0) (not (p3 c_3)) (= c_2 c_3) (not (p1 c_3 c_0)) (not (p1 c_2 c_0)) (not (p1 c_3 c_0)) (not (p4 c_0)) (not (p1 c_2 c_0)) )(or (not (p4 c_0)) (not (p3 c_2)) (= c_1 c_0) (not (p3 c_0)) (= c_2 c_0) (not (p1 c_0 c_0)) (not (p1 c_2 c_1)) (not (p1 c_0 c_1)) (not (p4 c_1)) (not (p1 c_2 c_0)) )(or (not (p4 c_0)) (not (p3 c_2)) (= c_1 c_0) (not (p3 c_1)) (= c_2 c_1) (not (p1 c_1 c_0)) (not (p1 c_2 c_1)) (not (p1 c_1 c_1)) (not (p4 c_1)) (not (p1 c_2 c_0)) )(or (not (p4 c_0)) (not (p3 c_2)) (= c_1 c_0) (not (p3 c_2)) (= c_2 c_2) (not (p1 c_2 c_0)) (not (p1 c_2 c_1)) (not (p1 c_2 c_1)) (not (p4 c_1)) (not (p1 c_2 c_0)) )(or (not (p4 c_0)) (not (p3 c_2)) (= c_1 c_0) (not (p3 c_3)) (= c_2 c_3) (not (p1 c_3 c_0)) (not (p1 c_2 c_1)) (not (p1 c_3 c_1)) (not (p4 c_1)) (not (p1 c_2 c_0)) )(or (not (p4 c_0)) (not (p3 c_2)) (= c_2 c_0) (not (p3 c_0)) (= c_2 c_0) (not (p1 c_0 c_0)) (not (p1 c_2 c_2)) (not (p1 c_0 c_2)) (not (p4 c_2)) (not (p1 c_2 c_0)) )(or (not (p4 c_0)) (not (p3 c_2)) (= c_2 c_0) (not (p3 c_1)) (= c_2 c_1) (not (p1 c_1 c_0)) (not (p1 c_2 c_2)) (not (p1 c_1 c_2)) (not (p4 c_2)) (not (p1 c_2 c_0)) )(or (not (p4 c_0)) (not (p3 c_2)) (= c_2 c_0) (not (p3 c_2)) (= c_2 c_2) (not (p1 c_2 c_0)) (not (p1 c_2 c_2)) (not (p1 c_2 c_2)) (not (p4 c_2)) (not (p1 c_2 c_0)) )(or (not (p4 c_0)) (not (p3 c_2)) (= c_2 c_0) (not (p3 c_3)) (= c_2 c_3) (not (p1 c_3 c_0)) (not (p1 c_2 c_2)) (not (p1 c_3 c_2)) (not (p4 c_2)) (not (p1 c_2 c_0)) )(or (not (p4 c_0)) (not (p3 c_2)) (= c_3 c_0) (not (p3 c_0)) (= c_2 c_0) (not (p1 c_0 c_0)) (not (p1 c_2 c_3)) (not (p1 c_0 c_3)) (not (p4 c_3)) (not (p1 c_2 c_0)) )(or (not (p4 c_0)) (not (p3 c_2)) (= c_3 c_0) (not (p3 c_1)) (= c_2 c_1) (not (p1 c_1 c_0)) (not (p1 c_2 c_3)) (not (p1 c_1 c_3)) (not (p4 c_3)) (not (p1 c_2 c_0)) )(or (not (p4 c_0)) (not (p3 c_2)) (= c_3 c_0) (not (p3 c_2)) (= c_2 c_2) (not (p1 c_2 c_0)) (not (p1 c_2 c_3)) (not (p1 c_2 c_3)) (not (p4 c_3)) (not (p1 c_2 c_0)) )(or (not (p4 c_0)) (not (p3 c_2)) (= c_3 c_0) (not (p3 c_3)) (= c_2 c_3) (not (p1 c_3 c_0)) (not (p1 c_2 c_3)) (not (p1 c_3 c_3)) (not (p4 c_3)) (not (p1 c_2 c_0)) )(or (not (p4 c_0)) (not (p3 c_3)) (= c_0 c_0) (not (p3 c_0)) (= c_3 c_0) (not (p1 c_0 c_0)) (not (p1 c_3 c_0)) (not (p1 c_0 c_0)) (not (p4 c_0)) (not (p1 c_3 c_0)) )(or (not (p4 c_0)) (not (p3 c_3)) (= c_0 c_0) (not (p3 c_1)) (= c_3 c_1) (not (p1 c_1 c_0)) (not (p1 c_3 c_0)) (not (p1 c_1 c_0)) (not (p4 c_0)) (not (p1 c_3 c_0)) )(or (not (p4 c_0)) (not (p3 c_3)) (= c_0 c_0) (not (p3 c_2)) (= c_3 c_2) (not (p1 c_2 c_0)) (not (p1 c_3 c_0)) (not (p1 c_2 c_0)) (not (p4 c_0)) (not (p1 c_3 c_0)) )(or (not (p4 c_0)) (not (p3 c_3)) (= c_0 c_0) (not (p3 c_3)) (= c_3 c_3) (not (p1 c_3 c_0)) (not (p1 c_3 c_0)) (not (p1 c_3 c_0)) (not (p4 c_0)) (not (p1 c_3 c_0)) )(or (not (p4 c_0)) (not (p3 c_3)) (= c_1 c_0) (not (p3 c_0)) (= c_3 c_0) (not (p1 c_0 c_0)) (not (p1 c_3 c_1)) (not (p1 c_0 c_1)) (not (p4 c_1)) (not (p1 c_3 c_0)) )(or (not (p4 c_0)) (not (p3 c_3)) (= c_1 c_0) (not (p3 c_1)) (= c_3 c_1) (not (p1 c_1 c_0)) (not (p1 c_3 c_1)) (not (p1 c_1 c_1)) (not (p4 c_1)) (not (p1 c_3 c_0)) )(or (not (p4 c_0)) (not (p3 c_3)) (= c_1 c_0) (not (p3 c_2)) (= c_3 c_2) (not (p1 c_2 c_0)) (not (p1 c_3 c_1)) (not (p1 c_2 c_1)) (not (p4 c_1)) (not (p1 c_3 c_0)) )(or (not (p4 c_0)) (not (p3 c_3)) (= c_1 c_0) (not (p3 c_3)) (= c_3 c_3) (not (p1 c_3 c_0)) (not (p1 c_3 c_1)) (not (p1 c_3 c_1)) (not (p4 c_1)) (not (p1 c_3 c_0)) )(or (not (p4 c_0)) (not (p3 c_3)) (= c_2 c_0) (not (p3 c_0)) (= c_3 c_0) (not (p1 c_0 c_0)) (not (p1 c_3 c_2)) (not (p1 c_0 c_2)) (not (p4 c_2)) (not (p1 c_3 c_0)) )(or (not (p4 c_0)) (not (p3 c_3)) (= c_2 c_0) (not (p3 c_1)) (= c_3 c_1) (not (p1 c_1 c_0)) (not (p1 c_3 c_2)) (not (p1 c_1 c_2)) (not (p4 c_2)) (not (p1 c_3 c_0)) )(or (not (p4 c_0)) (not (p3 c_3)) (= c_2 c_0) (not (p3 c_2)) (= c_3 c_2) (not (p1 c_2 c_0)) (not (p1 c_3 c_2)) (not (p1 c_2 c_2)) (not (p4 c_2)) (not (p1 c_3 c_0)) )(or (not (p4 c_0)) (not (p3 c_3)) (= c_2 c_0) (not (p3 c_3)) (= c_3 c_3) (not (p1 c_3 c_0)) (not (p1 c_3 c_2)) (not (p1 c_3 c_2)) (not (p4 c_2)) (not (p1 c_3 c_0)) )(or (not (p4 c_0)) (not (p3 c_3)) (= c_3 c_0) (not (p3 c_0)) (= c_3 c_0) (not (p1 c_0 c_0)) (not (p1 c_3 c_3)) (not (p1 c_0 c_3)) (not (p4 c_3)) (not (p1 c_3 c_0)) )(or (not (p4 c_0)) (not (p3 c_3)) (= c_3 c_0) (not (p3 c_1)) (= c_3 c_1) (not (p1 c_1 c_0)) (not (p1 c_3 c_3)) (not (p1 c_1 c_3)) (not (p4 c_3)) (not (p1 c_3 c_0)) )(or (not (p4 c_0)) (not (p3 c_3)) (= c_3 c_0) (not (p3 c_2)) (= c_3 c_2) (not (p1 c_2 c_0)) (not (p1 c_3 c_3)) (not (p1 c_2 c_3)) (not (p4 c_3)) (not (p1 c_3 c_0)) )(or (not (p4 c_0)) (not (p3 c_3)) (= c_3 c_0) (not (p3 c_3)) (= c_3 c_3) (not (p1 c_3 c_0)) (not (p1 c_3 c_3)) (not (p1 c_3 c_3)) (not (p4 c_3)) (not (p1 c_3 c_0)) )(or (not (p4 c_1)) (not (p3 c_0)) (= c_0 c_1) (not (p3 c_0)) (= c_0 c_0) (not (p1 c_0 c_1)) (not (p1 c_0 c_0)) (not (p1 c_0 c_0)) (not (p4 c_0)) (not (p1 c_0 c_1)) )(or (not (p4 c_1)) (not (p3 c_0)) (= c_0 c_1) (not (p3 c_1)) (= c_0 c_1) (not (p1 c_1 c_1)) (not (p1 c_0 c_0)) (not (p1 c_1 c_0)) (not (p4 c_0)) (not (p1 c_0 c_1)) )(or (not (p4 c_1)) (not (p3 c_0)) (= c_0 c_1) (not (p3 c_2)) (= c_0 c_2) (not (p1 c_2 c_1)) (not (p1 c_0 c_0)) (not (p1 c_2 c_0)) (not (p4 c_0)) (not (p1 c_0 c_1)) )(or (not (p4 c_1)) (not (p3 c_0)) (= c_0 c_1) (not (p3 c_3)) (= c_0 c_3) (not (p1 c_3 c_1)) (not (p1 c_0 c_0)) (not (p1 c_3 c_0)) (not (p4 c_0)) (not (p1 c_0 c_1)) )(or (not (p4 c_1)) (not (p3 c_0)) (= c_1 c_1) (not (p3 c_0)) (= c_0 c_0) (not (p1 c_0 c_1)) (not (p1 c_0 c_1)) (not (p1 c_0 c_1)) (not (p4 c_1)) (not (p1 c_0 c_1)) )(or (not (p4 c_1)) (not (p3 c_0)) (= c_1 c_1) (not (p3 c_1)) (= c_0 c_1) (not (p1 c_1 c_1)) (not (p1 c_0 c_1)) (not (p1 c_1 c_1)) (not (p4 c_1)) (not (p1 c_0 c_1)) )(or (not (p4 c_1)) (not (p3 c_0)) (= c_1 c_1) (not (p3 c_2)) (= c_0 c_2) (not (p1 c_2 c_1)) (not (p1 c_0 c_1)) (not (p1 c_2 c_1)) (not (p4 c_1)) (not (p1 c_0 c_1)) )(or (not (p4 c_1)) (not (p3 c_0)) (= c_1 c_1) (not (p3 c_3)) (= c_0 c_3) (not (p1 c_3 c_1)) (not (p1 c_0 c_1)) (not (p1 c_3 c_1)) (not (p4 c_1)) (not (p1 c_0 c_1)) )(or (not (p4 c_1)) (not (p3 c_0)) (= c_2 c_1) (not (p3 c_0)) (= c_0 c_0) (not (p1 c_0 c_1)) (not (p1 c_0 c_2)) (not (p1 c_0 c_2)) (not (p4 c_2)) (not (p1 c_0 c_1)) )(or (not (p4 c_1)) (not (p3 c_0)) (= c_2 c_1) (not (p3 c_1)) (= c_0 c_1) (not (p1 c_1 c_1)) (not (p1 c_0 c_2)) (not (p1 c_1 c_2)) (not (p4 c_2)) (not (p1 c_0 c_1)) )(or (not (p4 c_1)) (not (p3 c_0)) (= c_2 c_1) (not (p3 c_2)) (= c_0 c_2) (not (p1 c_2 c_1)) (not (p1 c_0 c_2)) (not (p1 c_2 c_2)) (not (p4 c_2)) (not (p1 c_0 c_1)) )(or (not (p4 c_1)) (not (p3 c_0)) (= c_2 c_1) (not (p3 c_3)) (= c_0 c_3) (not (p1 c_3 c_1)) (not (p1 c_0 c_2)) (not (p1 c_3 c_2)) (not (p4 c_2)) (not (p1 c_0 c_1)) )(or (not (p4 c_1)) (not (p3 c_0)) (= c_3 c_1) (not (p3 c_0)) (= c_0 c_0) (not (p1 c_0 c_1)) (not (p1 c_0 c_3)) (not (p1 c_0 c_3)) (not (p4 c_3)) (not (p1 c_0 c_1)) )(or (not (p4 c_1)) (not (p3 c_0)) (= c_3 c_1) (not (p3 c_1)) (= c_0 c_1) (not (p1 c_1 c_1)) (not (p1 c_0 c_3)) (not (p1 c_1 c_3)) (not (p4 c_3)) (not (p1 c_0 c_1)) )(or (not (p4 c_1)) (not (p3 c_0)) (= c_3 c_1) (not (p3 c_2)) (= c_0 c_2) (not (p1 c_2 c_1)) (not (p1 c_0 c_3)) (not (p1 c_2 c_3)) (not (p4 c_3)) (not (p1 c_0 c_1)) )(or (not (p4 c_1)) (not (p3 c_0)) (= c_3 c_1) (not (p3 c_3)) (= c_0 c_3) (not (p1 c_3 c_1)) (not (p1 c_0 c_3)) (not (p1 c_3 c_3)) (not (p4 c_3)) (not (p1 c_0 c_1)) )(or (not (p4 c_1)) (not (p3 c_1)) (= c_0 c_1) (not (p3 c_0)) (= c_1 c_0) (not (p1 c_0 c_1)) (not (p1 c_1 c_0)) (not (p1 c_0 c_0)) (not (p4 c_0)) (not (p1 c_1 c_1)) )(or (not (p4 c_1)) (not (p3 c_1)) (= c_0 c_1) (not (p3 c_1)) (= c_1 c_1) (not (p1 c_1 c_1)) (not (p1 c_1 c_0)) (not (p1 c_1 c_0)) (not (p4 c_0)) (not (p1 c_1 c_1)) )(or (not (p4 c_1)) (not (p3 c_1)) (= c_0 c_1) (not (p3 c_2)) (= c_1 c_2) (not (p1 c_2 c_1)) (not (p1 c_1 c_0)) (not (p1 c_2 c_0)) (not (p4 c_0)) (not (p1 c_1 c_1)) )(or (not (p4 c_1)) (not (p3 c_1)) (= c_0 c_1) (not (p3 c_3)) (= c_1 c_3) (not (p1 c_3 c_1)) (not (p1 c_1 c_0)) (not (p1 c_3 c_0)) (not (p4 c_0)) (not (p1 c_1 c_1)) )(or (not (p4 c_1)) (not (p3 c_1)) (= c_1 c_1) (not (p3 c_0)) (= c_1 c_0) (not (p1 c_0 c_1)) (not (p1 c_1 c_1)) (not (p1 c_0 c_1)) (not (p4 c_1)) (not (p1 c_1 c_1)) )(or (not (p4 c_1)) (not (p3 c_1)) (= c_1 c_1) (not (p3 c_1)) (= c_1 c_1) (not (p1 c_1 c_1)) (not (p1 c_1 c_1)) (not (p1 c_1 c_1)) (not (p4 c_1)) (not (p1 c_1 c_1)) )(or (not (p4 c_1)) (not (p3 c_1)) (= c_1 c_1) (not (p3 c_2)) (= c_1 c_2) (not (p1 c_2 c_1)) (not (p1 c_1 c_1)) (not (p1 c_2 c_1)) (not (p4 c_1)) (not (p1 c_1 c_1)) )(or (not (p4 c_1)) (not (p3 c_1)) (= c_1 c_1) (not (p3 c_3)) (= c_1 c_3) (not (p1 c_3 c_1)) (not (p1 c_1 c_1)) (not (p1 c_3 c_1)) (not (p4 c_1)) (not (p1 c_1 c_1)) )(or (not (p4 c_1)) (not (p3 c_1)) (= c_2 c_1) (not (p3 c_0)) (= c_1 c_0) (not (p1 c_0 c_1)) (not (p1 c_1 c_2)) (not (p1 c_0 c_2)) (not (p4 c_2)) (not (p1 c_1 c_1)) )(or (not (p4 c_1)) (not (p3 c_1)) (= c_2 c_1) (not (p3 c_1)) (= c_1 c_1) (not (p1 c_1 c_1)) (not (p1 c_1 c_2)) (not (p1 c_1 c_2)) (not (p4 c_2)) (not (p1 c_1 c_1)) )(or (not (p4 c_1)) (not (p3 c_1)) (= c_2 c_1) (not (p3 c_2)) (= c_1 c_2) (not (p1 c_2 c_1)) (not (p1 c_1 c_2)) (not (p1 c_2 c_2)) (not (p4 c_2)) (not (p1 c_1 c_1)) )(or (not (p4 c_1)) (not (p3 c_1)) (= c_2 c_1) (not (p3 c_3)) (= c_1 c_3) (not (p1 c_3 c_1)) (not (p1 c_1 c_2)) (not (p1 c_3 c_2)) (not (p4 c_2)) (not (p1 c_1 c_1)) )(or (not (p4 c_1)) (not (p3 c_1)) (= c_3 c_1) (not (p3 c_0)) (= c_1 c_0) (not (p1 c_0 c_1)) (not (p1 c_1 c_3)) (not (p1 c_0 c_3)) (not (p4 c_3)) (not (p1 c_1 c_1)) )(or (not (p4 c_1)) (not (p3 c_1)) (= c_3 c_1) (not (p3 c_1)) (= c_1 c_1) (not (p1 c_1 c_1)) (not (p1 c_1 c_3)) (not (p1 c_1 c_3)) (not (p4 c_3)) (not (p1 c_1 c_1)) )(or (not (p4 c_1)) (not (p3 c_1)) (= c_3 c_1) (not (p3 c_2)) (= c_1 c_2) (not (p1 c_2 c_1)) (not (p1 c_1 c_3)) (not (p1 c_2 c_3)) (not (p4 c_3)) (not (p1 c_1 c_1)) )(or (not (p4 c_1)) (not (p3 c_1)) (= c_3 c_1) (not (p3 c_3)) (= c_1 c_3) (not (p1 c_3 c_1)) (not (p1 c_1 c_3)) (not (p1 c_3 c_3)) (not (p4 c_3)) (not (p1 c_1 c_1)) )(or (not (p4 c_1)) (not (p3 c_2)) (= c_0 c_1) (not (p3 c_0)) (= c_2 c_0) (not (p1 c_0 c_1)) (not (p1 c_2 c_0)) (not (p1 c_0 c_0)) (not (p4 c_0)) (not (p1 c_2 c_1)) )(or (not (p4 c_1)) (not (p3 c_2)) (= c_0 c_1) (not (p3 c_1)) (= c_2 c_1) (not (p1 c_1 c_1)) (not (p1 c_2 c_0)) (not (p1 c_1 c_0)) (not (p4 c_0)) (not (p1 c_2 c_1)) )(or (not (p4 c_1)) (not (p3 c_2)) (= c_0 c_1) (not (p3 c_2)) (= c_2 c_2) (not (p1 c_2 c_1)) (not (p1 c_2 c_0)) (not (p1 c_2 c_0)) (not (p4 c_0)) (not (p1 c_2 c_1)) )(or (not (p4 c_1)) (not (p3 c_2)) (= c_0 c_1) (not (p3 c_3)) (= c_2 c_3) (not (p1 c_3 c_1)) (not (p1 c_2 c_0)) (not (p1 c_3 c_0)) (not (p4 c_0)) (not (p1 c_2 c_1)) )(or (not (p4 c_1)) (not (p3 c_2)) (= c_1 c_1) (not (p3 c_0)) (= c_2 c_0) (not (p1 c_0 c_1)) (not (p1 c_2 c_1)) (not (p1 c_0 c_1)) (not (p4 c_1)) (not (p1 c_2 c_1)) )(or (not (p4 c_1)) (not (p3 c_2)) (= c_1 c_1) (not (p3 c_1)) (= c_2 c_1) (not (p1 c_1 c_1)) (not (p1 c_2 c_1)) (not (p1 c_1 c_1)) (not (p4 c_1)) (not (p1 c_2 c_1)) )(or (not (p4 c_1)) (not (p3 c_2)) (= c_1 c_1) (not (p3 c_2)) (= c_2 c_2) (not (p1 c_2 c_1)) (not (p1 c_2 c_1)) (not (p1 c_2 c_1)) (not (p4 c_1)) (not (p1 c_2 c_1)) )(or (not (p4 c_1)) (not (p3 c_2)) (= c_1 c_1) (not (p3 c_3)) (= c_2 c_3) (not (p1 c_3 c_1)) (not (p1 c_2 c_1)) (not (p1 c_3 c_1)) (not (p4 c_1)) (not (p1 c_2 c_1)) )(or (not (p4 c_1)) (not (p3 c_2)) (= c_2 c_1) (not (p3 c_0)) (= c_2 c_0) (not (p1 c_0 c_1)) (not (p1 c_2 c_2)) (not (p1 c_0 c_2)) (not (p4 c_2)) (not (p1 c_2 c_1)) )(or (not (p4 c_1)) (not (p3 c_2)) (= c_2 c_1) (not (p3 c_1)) (= c_2 c_1) (not (p1 c_1 c_1)) (not (p1 c_2 c_2)) (not (p1 c_1 c_2)) (not (p4 c_2)) (not (p1 c_2 c_1)) )(or (not (p4 c_1)) (not (p3 c_2)) (= c_2 c_1) (not (p3 c_2)) (= c_2 c_2) (not (p1 c_2 c_1)) (not (p1 c_2 c_2)) (not (p1 c_2 c_2)) (not (p4 c_2)) (not (p1 c_2 c_1)) )(or (not (p4 c_1)) (not (p3 c_2)) (= c_2 c_1) (not (p3 c_3)) (= c_2 c_3) (not (p1 c_3 c_1)) (not (p1 c_2 c_2)) (not (p1 c_3 c_2)) (not (p4 c_2)) (not (p1 c_2 c_1)) )(or (not (p4 c_1)) (not (p3 c_2)) (= c_3 c_1) (not (p3 c_0)) (= c_2 c_0) (not (p1 c_0 c_1)) (not (p1 c_2 c_3)) (not (p1 c_0 c_3)) (not (p4 c_3)) (not (p1 c_2 c_1)) )(or (not (p4 c_1)) (not (p3 c_2)) (= c_3 c_1) (not (p3 c_1)) (= c_2 c_1) (not (p1 c_1 c_1)) (not (p1 c_2 c_3)) (not (p1 c_1 c_3)) (not (p4 c_3)) (not (p1 c_2 c_1)) )(or (not (p4 c_1)) (not (p3 c_2)) (= c_3 c_1) (not (p3 c_2)) (= c_2 c_2) (not (p1 c_2 c_1)) (not (p1 c_2 c_3)) (not (p1 c_2 c_3)) (not (p4 c_3)) (not (p1 c_2 c_1)) )(or (not (p4 c_1)) (not (p3 c_2)) (= c_3 c_1) (not (p3 c_3)) (= c_2 c_3) (not (p1 c_3 c_1)) (not (p1 c_2 c_3)) (not (p1 c_3 c_3)) (not (p4 c_3)) (not (p1 c_2 c_1)) )(or (not (p4 c_1)) (not (p3 c_3)) (= c_0 c_1) (not (p3 c_0)) (= c_3 c_0) (not (p1 c_0 c_1)) (not (p1 c_3 c_0)) (not (p1 c_0 c_0)) (not (p4 c_0)) (not (p1 c_3 c_1)) )(or (not (p4 c_1)) (not (p3 c_3)) (= c_0 c_1) (not (p3 c_1)) (= c_3 c_1) (not (p1 c_1 c_1)) (not (p1 c_3 c_0)) (not (p1 c_1 c_0)) (not (p4 c_0)) (not (p1 c_3 c_1)) )(or (not (p4 c_1)) (not (p3 c_3)) (= c_0 c_1) (not (p3 c_2)) (= c_3 c_2) (not (p1 c_2 c_1)) (not (p1 c_3 c_0)) (not (p1 c_2 c_0)) (not (p4 c_0)) (not (p1 c_3 c_1)) )(or (not (p4 c_1)) (not (p3 c_3)) (= c_0 c_1) (not (p3 c_3)) (= c_3 c_3) (not (p1 c_3 c_1)) (not (p1 c_3 c_0)) (not (p1 c_3 c_0)) (not (p4 c_0)) (not (p1 c_3 c_1)) )(or (not (p4 c_1)) (not (p3 c_3)) (= c_1 c_1) (not (p3 c_0)) (= c_3 c_0) (not (p1 c_0 c_1)) (not (p1 c_3 c_1)) (not (p1 c_0 c_1)) (not (p4 c_1)) (not (p1 c_3 c_1)) )(or (not (p4 c_1)) (not (p3 c_3)) (= c_1 c_1) (not (p3 c_1)) (= c_3 c_1) (not (p1 c_1 c_1)) (not (p1 c_3 c_1)) (not (p1 c_1 c_1)) (not (p4 c_1)) (not (p1 c_3 c_1)) )(or (not (p4 c_1)) (not (p3 c_3)) (= c_1 c_1) (not (p3 c_2)) (= c_3 c_2) (not (p1 c_2 c_1)) (not (p1 c_3 c_1)) (not (p1 c_2 c_1)) (not (p4 c_1)) (not (p1 c_3 c_1)) )(or (not (p4 c_1)) (not (p3 c_3)) (= c_1 c_1) (not (p3 c_3)) (= c_3 c_3) (not (p1 c_3 c_1)) (not (p1 c_3 c_1)) (not (p1 c_3 c_1)) (not (p4 c_1)) (not (p1 c_3 c_1)) )(or (not (p4 c_1)) (not (p3 c_3)) (= c_2 c_1) (not (p3 c_0)) (= c_3 c_0) (not (p1 c_0 c_1)) (not (p1 c_3 c_2)) (not (p1 c_0 c_2)) (not (p4 c_2)) (not (p1 c_3 c_1)) )(or (not (p4 c_1)) (not (p3 c_3)) (= c_2 c_1) (not (p3 c_1)) (= c_3 c_1) (not (p1 c_1 c_1)) (not (p1 c_3 c_2)) (not (p1 c_1 c_2)) (not (p4 c_2)) (not (p1 c_3 c_1)) )(or (not (p4 c_1)) (not (p3 c_3)) (= c_2 c_1) (not (p3 c_2)) (= c_3 c_2) (not (p1 c_2 c_1)) (not (p1 c_3 c_2)) (not (p1 c_2 c_2)) (not (p4 c_2)) (not (p1 c_3 c_1)) )(or (not (p4 c_1)) (not (p3 c_3)) (= c_2 c_1) (not (p3 c_3)) (= c_3 c_3) (not (p1 c_3 c_1)) (not (p1 c_3 c_2)) (not (p1 c_3 c_2)) (not (p4 c_2)) (not (p1 c_3 c_1)) )(or (not (p4 c_1)) (not (p3 c_3)) (= c_3 c_1) (not (p3 c_0)) (= c_3 c_0) (not (p1 c_0 c_1)) (not (p1 c_3 c_3)) (not (p1 c_0 c_3)) (not (p4 c_3)) (not (p1 c_3 c_1)) )(or (not (p4 c_1)) (not (p3 c_3)) (= c_3 c_1) (not (p3 c_1)) (= c_3 c_1) (not (p1 c_1 c_1)) (not (p1 c_3 c_3)) (not (p1 c_1 c_3)) (not (p4 c_3)) (not (p1 c_3 c_1)) )(or (not (p4 c_1)) (not (p3 c_3)) (= c_3 c_1) (not (p3 c_2)) (= c_3 c_2) (not (p1 c_2 c_1)) (not (p1 c_3 c_3)) (not (p1 c_2 c_3)) (not (p4 c_3)) (not (p1 c_3 c_1)) )(or (not (p4 c_1)) (not (p3 c_3)) (= c_3 c_1) (not (p3 c_3)) (= c_3 c_3) (not (p1 c_3 c_1)) (not (p1 c_3 c_3)) (not (p1 c_3 c_3)) (not (p4 c_3)) (not (p1 c_3 c_1)) )(or (not (p4 c_2)) (not (p3 c_0)) (= c_0 c_2) (not (p3 c_0)) (= c_0 c_0) (not (p1 c_0 c_2)) (not (p1 c_0 c_0)) (not (p1 c_0 c_0)) (not (p4 c_0)) (not (p1 c_0 c_2)) )(or (not (p4 c_2)) (not (p3 c_0)) (= c_0 c_2) (not (p3 c_1)) (= c_0 c_1) (not (p1 c_1 c_2)) (not (p1 c_0 c_0)) (not (p1 c_1 c_0)) (not (p4 c_0)) (not (p1 c_0 c_2)) )(or (not (p4 c_2)) (not (p3 c_0)) (= c_0 c_2) (not (p3 c_2)) (= c_0 c_2) (not (p1 c_2 c_2)) (not (p1 c_0 c_0)) (not (p1 c_2 c_0)) (not (p4 c_0)) (not (p1 c_0 c_2)) )(or (not (p4 c_2)) (not (p3 c_0)) (= c_0 c_2) (not (p3 c_3)) (= c_0 c_3) (not (p1 c_3 c_2)) (not (p1 c_0 c_0)) (not (p1 c_3 c_0)) (not (p4 c_0)) (not (p1 c_0 c_2)) )(or (not (p4 c_2)) (not (p3 c_0)) (= c_1 c_2) (not (p3 c_0)) (= c_0 c_0) (not (p1 c_0 c_2)) (not (p1 c_0 c_1)) (not (p1 c_0 c_1)) (not (p4 c_1)) (not (p1 c_0 c_2)) )(or (not (p4 c_2)) (not (p3 c_0)) (= c_1 c_2) (not (p3 c_1)) (= c_0 c_1) (not (p1 c_1 c_2)) (not (p1 c_0 c_1)) (not (p1 c_1 c_1)) (not (p4 c_1)) (not (p1 c_0 c_2)) )(or (not (p4 c_2)) (not (p3 c_0)) (= c_1 c_2) (not (p3 c_2)) (= c_0 c_2) (not (p1 c_2 c_2)) (not (p1 c_0 c_1)) (not (p1 c_2 c_1)) (not (p4 c_1)) (not (p1 c_0 c_2)) )(or (not (p4 c_2)) (not (p3 c_0)) (= c_1 c_2) (not (p3 c_3)) (= c_0 c_3) (not (p1 c_3 c_2)) (not (p1 c_0 c_1)) (not (p1 c_3 c_1)) (not (p4 c_1)) (not (p1 c_0 c_2)) )(or (not (p4 c_2)) (not (p3 c_0)) (= c_2 c_2) (not (p3 c_0)) (= c_0 c_0) (not (p1 c_0 c_2)) (not (p1 c_0 c_2)) (not (p1 c_0 c_2)) (not (p4 c_2)) (not (p1 c_0 c_2)) )(or (not (p4 c_2)) (not (p3 c_0)) (= c_2 c_2) (not (p3 c_1)) (= c_0 c_1) (not (p1 c_1 c_2)) (not (p1 c_0 c_2)) (not (p1 c_1 c_2)) (not (p4 c_2)) (not (p1 c_0 c_2)) )(or (not (p4 c_2)) (not (p3 c_0)) (= c_2 c_2) (not (p3 c_2)) (= c_0 c_2) (not (p1 c_2 c_2)) (not (p1 c_0 c_2)) (not (p1 c_2 c_2)) (not (p4 c_2)) (not (p1 c_0 c_2)) )(or (not (p4 c_2)) (not (p3 c_0)) (= c_2 c_2) (not (p3 c_3)) (= c_0 c_3) (not (p1 c_3 c_2)) (not (p1 c_0 c_2)) (not (p1 c_3 c_2)) (not (p4 c_2)) (not (p1 c_0 c_2)) )(or (not (p4 c_2)) (not (p3 c_0)) (= c_3 c_2) (not (p3 c_0)) (= c_0 c_0) (not (p1 c_0 c_2)) (not (p1 c_0 c_3)) (not (p1 c_0 c_3)) (not (p4 c_3)) (not (p1 c_0 c_2)) )(or (not (p4 c_2)) (not (p3 c_0)) (= c_3 c_2) (not (p3 c_1)) (= c_0 c_1) (not (p1 c_1 c_2)) (not (p1 c_0 c_3)) (not (p1 c_1 c_3)) (not (p4 c_3)) (not (p1 c_0 c_2)) )(or (not (p4 c_2)) (not (p3 c_0)) (= c_3 c_2) (not (p3 c_2)) (= c_0 c_2) (not (p1 c_2 c_2)) (not (p1 c_0 c_3)) (not (p1 c_2 c_3)) (not (p4 c_3)) (not (p1 c_0 c_2)) )(or (not (p4 c_2)) (not (p3 c_0)) (= c_3 c_2) (not (p3 c_3)) (= c_0 c_3) (not (p1 c_3 c_2)) (not (p1 c_0 c_3)) (not (p1 c_3 c_3)) (not (p4 c_3)) (not (p1 c_0 c_2)) )(or (not (p4 c_2)) (not (p3 c_1)) (= c_0 c_2) (not (p3 c_0)) (= c_1 c_0) (not (p1 c_0 c_2)) (not (p1 c_1 c_0)) (not (p1 c_0 c_0)) (not (p4 c_0)) (not (p1 c_1 c_2)) )(or (not (p4 c_2)) (not (p3 c_1)) (= c_0 c_2) (not (p3 c_1)) (= c_1 c_1) (not (p1 c_1 c_2)) (not (p1 c_1 c_0)) (not (p1 c_1 c_0)) (not (p4 c_0)) (not (p1 c_1 c_2)) )(or (not (p4 c_2)) (not (p3 c_1)) (= c_0 c_2) (not (p3 c_2)) (= c_1 c_2) (not (p1 c_2 c_2)) (not (p1 c_1 c_0)) (not (p1 c_2 c_0)) (not (p4 c_0)) (not (p1 c_1 c_2)) )(or (not (p4 c_2)) (not (p3 c_1)) (= c_0 c_2) (not (p3 c_3)) (= c_1 c_3) (not (p1 c_3 c_2)) (not (p1 c_1 c_0)) (not (p1 c_3 c_0)) (not (p4 c_0)) (not (p1 c_1 c_2)) )(or (not (p4 c_2)) (not (p3 c_1)) (= c_1 c_2) (not (p3 c_0)) (= c_1 c_0) (not (p1 c_0 c_2)) (not (p1 c_1 c_1)) (not (p1 c_0 c_1)) (not (p4 c_1)) (not (p1 c_1 c_2)) )(or (not (p4 c_2)) (not (p3 c_1)) (= c_1 c_2) (not (p3 c_1)) (= c_1 c_1) (not (p1 c_1 c_2)) (not (p1 c_1 c_1)) (not (p1 c_1 c_1)) (not (p4 c_1)) (not (p1 c_1 c_2)) )(or (not (p4 c_2)) (not (p3 c_1)) (= c_1 c_2) (not (p3 c_2)) (= c_1 c_2) (not (p1 c_2 c_2)) (not (p1 c_1 c_1)) (not (p1 c_2 c_1)) (not (p4 c_1)) (not (p1 c_1 c_2)) )(or (not (p4 c_2)) (not (p3 c_1)) (= c_1 c_2) (not (p3 c_3)) (= c_1 c_3) (not (p1 c_3 c_2)) (not (p1 c_1 c_1)) (not (p1 c_3 c_1)) (not (p4 c_1)) (not (p1 c_1 c_2)) )(or (not (p4 c_2)) (not (p3 c_1)) (= c_2 c_2) (not (p3 c_0)) (= c_1 c_0) (not (p1 c_0 c_2)) (not (p1 c_1 c_2)) (not (p1 c_0 c_2)) (not (p4 c_2)) (not (p1 c_1 c_2)) )(or (not (p4 c_2)) (not (p3 c_1)) (= c_2 c_2) (not (p3 c_1)) (= c_1 c_1) (not (p1 c_1 c_2)) (not (p1 c_1 c_2)) (not (p1 c_1 c_2)) (not (p4 c_2)) (not (p1 c_1 c_2)) )(or (not (p4 c_2)) (not (p3 c_1)) (= c_2 c_2) (not (p3 c_2)) (= c_1 c_2) (not (p1 c_2 c_2)) (not (p1 c_1 c_2)) (not (p1 c_2 c_2)) (not (p4 c_2)) (not (p1 c_1 c_2)) )(or (not (p4 c_2)) (not (p3 c_1)) (= c_2 c_2) (not (p3 c_3)) (= c_1 c_3) (not (p1 c_3 c_2)) (not (p1 c_1 c_2)) (not (p1 c_3 c_2)) (not (p4 c_2)) (not (p1 c_1 c_2)) )(or (not (p4 c_2)) (not (p3 c_1)) (= c_3 c_2) (not (p3 c_0)) (= c_1 c_0) (not (p1 c_0 c_2)) (not (p1 c_1 c_3)) (not (p1 c_0 c_3)) (not (p4 c_3)) (not (p1 c_1 c_2)) )(or (not (p4 c_2)) (not (p3 c_1)) (= c_3 c_2) (not (p3 c_1)) (= c_1 c_1) (not (p1 c_1 c_2)) (not (p1 c_1 c_3)) (not (p1 c_1 c_3)) (not (p4 c_3)) (not (p1 c_1 c_2)) )(or (not (p4 c_2)) (not (p3 c_1)) (= c_3 c_2) (not (p3 c_2)) (= c_1 c_2) (not (p1 c_2 c_2)) (not (p1 c_1 c_3)) (not (p1 c_2 c_3)) (not (p4 c_3)) (not (p1 c_1 c_2)) )(or (not (p4 c_2)) (not (p3 c_1)) (= c_3 c_2) (not (p3 c_3)) (= c_1 c_3) (not (p1 c_3 c_2)) (not (p1 c_1 c_3)) (not (p1 c_3 c_3)) (not (p4 c_3)) (not (p1 c_1 c_2)) )(or (not (p4 c_2)) (not (p3 c_2)) (= c_0 c_2) (not (p3 c_0)) (= c_2 c_0) (not (p1 c_0 c_2)) (not (p1 c_2 c_0)) (not (p1 c_0 c_0)) (not (p4 c_0)) (not (p1 c_2 c_2)) )(or (not (p4 c_2)) (not (p3 c_2)) (= c_0 c_2) (not (p3 c_1)) (= c_2 c_1) (not (p1 c_1 c_2)) (not (p1 c_2 c_0)) (not (p1 c_1 c_0)) (not (p4 c_0)) (not (p1 c_2 c_2)) )(or (not (p4 c_2)) (not (p3 c_2)) (= c_0 c_2) (not (p3 c_2)) (= c_2 c_2) (not (p1 c_2 c_2)) (not (p1 c_2 c_0)) (not (p1 c_2 c_0)) (not (p4 c_0)) (not (p1 c_2 c_2)) )(or (not (p4 c_2)) (not (p3 c_2)) (= c_0 c_2) (not (p3 c_3)) (= c_2 c_3) (not (p1 c_3 c_2)) (not (p1 c_2 c_0)) (not (p1 c_3 c_0)) (not (p4 c_0)) (not (p1 c_2 c_2)) )(or (not (p4 c_2)) (not (p3 c_2)) (= c_1 c_2) (not (p3 c_0)) (= c_2 c_0) (not (p1 c_0 c_2)) (not (p1 c_2 c_1)) (not (p1 c_0 c_1)) (not (p4 c_1)) (not (p1 c_2 c_2)) )(or (not (p4 c_2)) (not (p3 c_2)) (= c_1 c_2) (not (p3 c_1)) (= c_2 c_1) (not (p1 c_1 c_2)) (not (p1 c_2 c_1)) (not (p1 c_1 c_1)) (not (p4 c_1)) (not (p1 c_2 c_2)) )(or (not (p4 c_2)) (not (p3 c_2)) (= c_1 c_2) (not (p3 c_2)) (= c_2 c_2) (not (p1 c_2 c_2)) (not (p1 c_2 c_1)) (not (p1 c_2 c_1)) (not (p4 c_1)) (not (p1 c_2 c_2)) )(or (not (p4 c_2)) (not (p3 c_2)) (= c_1 c_2) (not (p3 c_3)) (= c_2 c_3) (not (p1 c_3 c_2)) (not (p1 c_2 c_1)) (not (p1 c_3 c_1)) (not (p4 c_1)) (not (p1 c_2 c_2)) )(or (not (p4 c_2)) (not (p3 c_2)) (= c_2 c_2) (not (p3 c_0)) (= c_2 c_0) (not (p1 c_0 c_2)) (not (p1 c_2 c_2)) (not (p1 c_0 c_2)) (not (p4 c_2)) (not (p1 c_2 c_2)) )(or (not (p4 c_2)) (not (p3 c_2)) (= c_2 c_2) (not (p3 c_1)) (= c_2 c_1) (not (p1 c_1 c_2)) (not (p1 c_2 c_2)) (not (p1 c_1 c_2)) (not (p4 c_2)) (not (p1 c_2 c_2)) )(or (not (p4 c_2)) (not (p3 c_2)) (= c_2 c_2) (not (p3 c_2)) (= c_2 c_2) (not (p1 c_2 c_2)) (not (p1 c_2 c_2)) (not (p1 c_2 c_2)) (not (p4 c_2)) (not (p1 c_2 c_2)) )(or (not (p4 c_2)) (not (p3 c_2)) (= c_2 c_2) (not (p3 c_3)) (= c_2 c_3) (not (p1 c_3 c_2)) (not (p1 c_2 c_2)) (not (p1 c_3 c_2)) (not (p4 c_2)) (not (p1 c_2 c_2)) )(or (not (p4 c_2)) (not (p3 c_2)) (= c_3 c_2) (not (p3 c_0)) (= c_2 c_0) (not (p1 c_0 c_2)) (not (p1 c_2 c_3)) (not (p1 c_0 c_3)) (not (p4 c_3)) (not (p1 c_2 c_2)) )(or (not (p4 c_2)) (not (p3 c_2)) (= c_3 c_2) (not (p3 c_1)) (= c_2 c_1) (not (p1 c_1 c_2)) (not (p1 c_2 c_3)) (not (p1 c_1 c_3)) (not (p4 c_3)) (not (p1 c_2 c_2)) )(or (not (p4 c_2)) (not (p3 c_2)) (= c_3 c_2) (not (p3 c_2)) (= c_2 c_2) (not (p1 c_2 c_2)) (not (p1 c_2 c_3)) (not (p1 c_2 c_3)) (not (p4 c_3)) (not (p1 c_2 c_2)) )(or (not (p4 c_2)) (not (p3 c_2)) (= c_3 c_2) (not (p3 c_3)) (= c_2 c_3) (not (p1 c_3 c_2)) (not (p1 c_2 c_3)) (not (p1 c_3 c_3)) (not (p4 c_3)) (not (p1 c_2 c_2)) )(or (not (p4 c_2)) (not (p3 c_3)) (= c_0 c_2) (not (p3 c_0)) (= c_3 c_0) (not (p1 c_0 c_2)) (not (p1 c_3 c_0)) (not (p1 c_0 c_0)) (not (p4 c_0)) (not (p1 c_3 c_2)) )(or (not (p4 c_2)) (not (p3 c_3)) (= c_0 c_2) (not (p3 c_1)) (= c_3 c_1) (not (p1 c_1 c_2)) (not (p1 c_3 c_0)) (not (p1 c_1 c_0)) (not (p4 c_0)) (not (p1 c_3 c_2)) )(or (not (p4 c_2)) (not (p3 c_3)) (= c_0 c_2) (not (p3 c_2)) (= c_3 c_2) (not (p1 c_2 c_2)) (not (p1 c_3 c_0)) (not (p1 c_2 c_0)) (not (p4 c_0)) (not (p1 c_3 c_2)) )(or (not (p4 c_2)) (not (p3 c_3)) (= c_0 c_2) (not (p3 c_3)) (= c_3 c_3) (not (p1 c_3 c_2)) (not (p1 c_3 c_0)) (not (p1 c_3 c_0)) (not (p4 c_0)) (not (p1 c_3 c_2)) )(or (not (p4 c_2)) (not (p3 c_3)) (= c_1 c_2) (not (p3 c_0)) (= c_3 c_0) (not (p1 c_0 c_2)) (not (p1 c_3 c_1)) (not (p1 c_0 c_1)) (not (p4 c_1)) (not (p1 c_3 c_2)) )(or (not (p4 c_2)) (not (p3 c_3)) (= c_1 c_2) (not (p3 c_1)) (= c_3 c_1) (not (p1 c_1 c_2)) (not (p1 c_3 c_1)) (not (p1 c_1 c_1)) (not (p4 c_1)) (not (p1 c_3 c_2)) )(or (not (p4 c_2)) (not (p3 c_3)) (= c_1 c_2) (not (p3 c_2)) (= c_3 c_2) (not (p1 c_2 c_2)) (not (p1 c_3 c_1)) (not (p1 c_2 c_1)) (not (p4 c_1)) (not (p1 c_3 c_2)) )(or (not (p4 c_2)) (not (p3 c_3)) (= c_1 c_2) (not (p3 c_3)) (= c_3 c_3) (not (p1 c_3 c_2)) (not (p1 c_3 c_1)) (not (p1 c_3 c_1)) (not (p4 c_1)) (not (p1 c_3 c_2)) )(or (not (p4 c_2)) (not (p3 c_3)) (= c_2 c_2) (not (p3 c_0)) (= c_3 c_0) (not (p1 c_0 c_2)) (not (p1 c_3 c_2)) (not (p1 c_0 c_2)) (not (p4 c_2)) (not (p1 c_3 c_2)) )(or (not (p4 c_2)) (not (p3 c_3)) (= c_2 c_2) (not (p3 c_1)) (= c_3 c_1) (not (p1 c_1 c_2)) (not (p1 c_3 c_2)) (not (p1 c_1 c_2)) (not (p4 c_2)) (not (p1 c_3 c_2)) )(or (not (p4 c_2)) (not (p3 c_3)) (= c_2 c_2) (not (p3 c_2)) (= c_3 c_2) (not (p1 c_2 c_2)) (not (p1 c_3 c_2)) (not (p1 c_2 c_2)) (not (p4 c_2)) (not (p1 c_3 c_2)) )(or (not (p4 c_2)) (not (p3 c_3)) (= c_2 c_2) (not (p3 c_3)) (= c_3 c_3) (not (p1 c_3 c_2)) (not (p1 c_3 c_2)) (not (p1 c_3 c_2)) (not (p4 c_2)) (not (p1 c_3 c_2)) )(or (not (p4 c_2)) (not (p3 c_3)) (= c_3 c_2) (not (p3 c_0)) (= c_3 c_0) (not (p1 c_0 c_2)) (not (p1 c_3 c_3)) (not (p1 c_0 c_3)) (not (p4 c_3)) (not (p1 c_3 c_2)) )(or (not (p4 c_2)) (not (p3 c_3)) (= c_3 c_2) (not (p3 c_1)) (= c_3 c_1) (not (p1 c_1 c_2)) (not (p1 c_3 c_3)) (not (p1 c_1 c_3)) (not (p4 c_3)) (not (p1 c_3 c_2)) )(or (not (p4 c_2)) (not (p3 c_3)) (= c_3 c_2) (not (p3 c_2)) (= c_3 c_2) (not (p1 c_2 c_2)) (not (p1 c_3 c_3)) (not (p1 c_2 c_3)) (not (p4 c_3)) (not (p1 c_3 c_2)) )(or (not (p4 c_2)) (not (p3 c_3)) (= c_3 c_2) (not (p3 c_3)) (= c_3 c_3) (not (p1 c_3 c_2)) (not (p1 c_3 c_3)) (not (p1 c_3 c_3)) (not (p4 c_3)) (not (p1 c_3 c_2)) )(or (not (p4 c_3)) (not (p3 c_0)) (= c_0 c_3) (not (p3 c_0)) (= c_0 c_0) (not (p1 c_0 c_3)) (not (p1 c_0 c_0)) (not (p1 c_0 c_0)) (not (p4 c_0)) (not (p1 c_0 c_3)) )(or (not (p4 c_3)) (not (p3 c_0)) (= c_0 c_3) (not (p3 c_1)) (= c_0 c_1) (not (p1 c_1 c_3)) (not (p1 c_0 c_0)) (not (p1 c_1 c_0)) (not (p4 c_0)) (not (p1 c_0 c_3)) )(or (not (p4 c_3)) (not (p3 c_0)) (= c_0 c_3) (not (p3 c_2)) (= c_0 c_2) (not (p1 c_2 c_3)) (not (p1 c_0 c_0)) (not (p1 c_2 c_0)) (not (p4 c_0)) (not (p1 c_0 c_3)) )(or (not (p4 c_3)) (not (p3 c_0)) (= c_0 c_3) (not (p3 c_3)) (= c_0 c_3) (not (p1 c_3 c_3)) (not (p1 c_0 c_0)) (not (p1 c_3 c_0)) (not (p4 c_0)) (not (p1 c_0 c_3)) )(or (not (p4 c_3)) (not (p3 c_0)) (= c_1 c_3) (not (p3 c_0)) (= c_0 c_0) (not (p1 c_0 c_3)) (not (p1 c_0 c_1)) (not (p1 c_0 c_1)) (not (p4 c_1)) (not (p1 c_0 c_3)) )(or (not (p4 c_3)) (not (p3 c_0)) (= c_1 c_3) (not (p3 c_1)) (= c_0 c_1) (not (p1 c_1 c_3)) (not (p1 c_0 c_1)) (not (p1 c_1 c_1)) (not (p4 c_1)) (not (p1 c_0 c_3)) )(or (not (p4 c_3)) (not (p3 c_0)) (= c_1 c_3) (not (p3 c_2)) (= c_0 c_2) (not (p1 c_2 c_3)) (not (p1 c_0 c_1)) (not (p1 c_2 c_1)) (not (p4 c_1)) (not (p1 c_0 c_3)) )(or (not (p4 c_3)) (not (p3 c_0)) (= c_1 c_3) (not (p3 c_3)) (= c_0 c_3) (not (p1 c_3 c_3)) (not (p1 c_0 c_1)) (not (p1 c_3 c_1)) (not (p4 c_1)) (not (p1 c_0 c_3)) )(or (not (p4 c_3)) (not (p3 c_0)) (= c_2 c_3) (not (p3 c_0)) (= c_0 c_0) (not (p1 c_0 c_3)) (not (p1 c_0 c_2)) (not (p1 c_0 c_2)) (not (p4 c_2)) (not (p1 c_0 c_3)) )(or (not (p4 c_3)) (not (p3 c_0)) (= c_2 c_3) (not (p3 c_1)) (= c_0 c_1) (not (p1 c_1 c_3)) (not (p1 c_0 c_2)) (not (p1 c_1 c_2)) (not (p4 c_2)) (not (p1 c_0 c_3)) )(or (not (p4 c_3)) (not (p3 c_0)) (= c_2 c_3) (not (p3 c_2)) (= c_0 c_2) (not (p1 c_2 c_3)) (not (p1 c_0 c_2)) (not (p1 c_2 c_2)) (not (p4 c_2)) (not (p1 c_0 c_3)) )(or (not (p4 c_3)) (not (p3 c_0)) (= c_2 c_3) (not (p3 c_3)) (= c_0 c_3) (not (p1 c_3 c_3)) (not (p1 c_0 c_2)) (not (p1 c_3 c_2)) (not (p4 c_2)) (not (p1 c_0 c_3)) )(or (not (p4 c_3)) (not (p3 c_0)) (= c_3 c_3) (not (p3 c_0)) (= c_0 c_0) (not (p1 c_0 c_3)) (not (p1 c_0 c_3)) (not (p1 c_0 c_3)) (not (p4 c_3)) (not (p1 c_0 c_3)) )(or (not (p4 c_3)) (not (p3 c_0)) (= c_3 c_3) (not (p3 c_1)) (= c_0 c_1) (not (p1 c_1 c_3)) (not (p1 c_0 c_3)) (not (p1 c_1 c_3)) (not (p4 c_3)) (not (p1 c_0 c_3)) )(or (not (p4 c_3)) (not (p3 c_0)) (= c_3 c_3) (not (p3 c_2)) (= c_0 c_2) (not (p1 c_2 c_3)) (not (p1 c_0 c_3)) (not (p1 c_2 c_3)) (not (p4 c_3)) (not (p1 c_0 c_3)) )(or (not (p4 c_3)) (not (p3 c_0)) (= c_3 c_3) (not (p3 c_3)) (= c_0 c_3) (not (p1 c_3 c_3)) (not (p1 c_0 c_3)) (not (p1 c_3 c_3)) (not (p4 c_3)) (not (p1 c_0 c_3)) )(or (not (p4 c_3)) (not (p3 c_1)) (= c_0 c_3) (not (p3 c_0)) (= c_1 c_0) (not (p1 c_0 c_3)) (not (p1 c_1 c_0)) (not (p1 c_0 c_0)) (not (p4 c_0)) (not (p1 c_1 c_3)) )(or (not (p4 c_3)) (not (p3 c_1)) (= c_0 c_3) (not (p3 c_1)) (= c_1 c_1) (not (p1 c_1 c_3)) (not (p1 c_1 c_0)) (not (p1 c_1 c_0)) (not (p4 c_0)) (not (p1 c_1 c_3)) )(or (not (p4 c_3)) (not (p3 c_1)) (= c_0 c_3) (not (p3 c_2)) (= c_1 c_2) (not (p1 c_2 c_3)) (not (p1 c_1 c_0)) (not (p1 c_2 c_0)) (not (p4 c_0)) (not (p1 c_1 c_3)) )(or (not (p4 c_3)) (not (p3 c_1)) (= c_0 c_3) (not (p3 c_3)) (= c_1 c_3) (not (p1 c_3 c_3)) (not (p1 c_1 c_0)) (not (p1 c_3 c_0)) (not (p4 c_0)) (not (p1 c_1 c_3)) )(or (not (p4 c_3)) (not (p3 c_1)) (= c_1 c_3) (not (p3 c_0)) (= c_1 c_0) (not (p1 c_0 c_3)) (not (p1 c_1 c_1)) (not (p1 c_0 c_1)) (not (p4 c_1)) (not (p1 c_1 c_3)) )(or (not (p4 c_3)) (not (p3 c_1)) (= c_1 c_3) (not (p3 c_1)) (= c_1 c_1) (not (p1 c_1 c_3)) (not (p1 c_1 c_1)) (not (p1 c_1 c_1)) (not (p4 c_1)) (not (p1 c_1 c_3)) )(or (not (p4 c_3)) (not (p3 c_1)) (= c_1 c_3) (not (p3 c_2)) (= c_1 c_2) (not (p1 c_2 c_3)) (not (p1 c_1 c_1)) (not (p1 c_2 c_1)) (not (p4 c_1)) (not (p1 c_1 c_3)) )(or (not (p4 c_3)) (not (p3 c_1)) (= c_1 c_3) (not (p3 c_3)) (= c_1 c_3) (not (p1 c_3 c_3)) (not (p1 c_1 c_1)) (not (p1 c_3 c_1)) (not (p4 c_1)) (not (p1 c_1 c_3)) )(or (not (p4 c_3)) (not (p3 c_1)) (= c_2 c_3) (not (p3 c_0)) (= c_1 c_0) (not (p1 c_0 c_3)) (not (p1 c_1 c_2)) (not (p1 c_0 c_2)) (not (p4 c_2)) (not (p1 c_1 c_3)) )(or (not (p4 c_3)) (not (p3 c_1)) (= c_2 c_3) (not (p3 c_1)) (= c_1 c_1) (not (p1 c_1 c_3)) (not (p1 c_1 c_2)) (not (p1 c_1 c_2)) (not (p4 c_2)) (not (p1 c_1 c_3)) )(or (not (p4 c_3)) (not (p3 c_1)) (= c_2 c_3) (not (p3 c_2)) (= c_1 c_2) (not (p1 c_2 c_3)) (not (p1 c_1 c_2)) (not (p1 c_2 c_2)) (not (p4 c_2)) (not (p1 c_1 c_3)) )(or (not (p4 c_3)) (not (p3 c_1)) (= c_2 c_3) (not (p3 c_3)) (= c_1 c_3) (not (p1 c_3 c_3)) (not (p1 c_1 c_2)) (not (p1 c_3 c_2)) (not (p4 c_2)) (not (p1 c_1 c_3)) )(or (not (p4 c_3)) (not (p3 c_1)) (= c_3 c_3) (not (p3 c_0)) (= c_1 c_0) (not (p1 c_0 c_3)) (not (p1 c_1 c_3)) (not (p1 c_0 c_3)) (not (p4 c_3)) (not (p1 c_1 c_3)) )(or (not (p4 c_3)) (not (p3 c_1)) (= c_3 c_3) (not (p3 c_1)) (= c_1 c_1) (not (p1 c_1 c_3)) (not (p1 c_1 c_3)) (not (p1 c_1 c_3)) (not (p4 c_3)) (not (p1 c_1 c_3)) )(or (not (p4 c_3)) (not (p3 c_1)) (= c_3 c_3) (not (p3 c_2)) (= c_1 c_2) (not (p1 c_2 c_3)) (not (p1 c_1 c_3)) (not (p1 c_2 c_3)) (not (p4 c_3)) (not (p1 c_1 c_3)) )(or (not (p4 c_3)) (not (p3 c_1)) (= c_3 c_3) (not (p3 c_3)) (= c_1 c_3) (not (p1 c_3 c_3)) (not (p1 c_1 c_3)) (not (p1 c_3 c_3)) (not (p4 c_3)) (not (p1 c_1 c_3)) )(or (not (p4 c_3)) (not (p3 c_2)) (= c_0 c_3) (not (p3 c_0)) (= c_2 c_0) (not (p1 c_0 c_3)) (not (p1 c_2 c_0)) (not (p1 c_0 c_0)) (not (p4 c_0)) (not (p1 c_2 c_3)) )(or (not (p4 c_3)) (not (p3 c_2)) (= c_0 c_3) (not (p3 c_1)) (= c_2 c_1) (not (p1 c_1 c_3)) (not (p1 c_2 c_0)) (not (p1 c_1 c_0)) (not (p4 c_0)) (not (p1 c_2 c_3)) )(or (not (p4 c_3)) (not (p3 c_2)) (= c_0 c_3) (not (p3 c_2)) (= c_2 c_2) (not (p1 c_2 c_3)) (not (p1 c_2 c_0)) (not (p1 c_2 c_0)) (not (p4 c_0)) (not (p1 c_2 c_3)) )(or (not (p4 c_3)) (not (p3 c_2)) (= c_0 c_3) (not (p3 c_3)) (= c_2 c_3) (not (p1 c_3 c_3)) (not (p1 c_2 c_0)) (not (p1 c_3 c_0)) (not (p4 c_0)) (not (p1 c_2 c_3)) )(or (not (p4 c_3)) (not (p3 c_2)) (= c_1 c_3) (not (p3 c_0)) (= c_2 c_0) (not (p1 c_0 c_3)) (not (p1 c_2 c_1)) (not (p1 c_0 c_1)) (not (p4 c_1)) (not (p1 c_2 c_3)) )(or (not (p4 c_3)) (not (p3 c_2)) (= c_1 c_3) (not (p3 c_1)) (= c_2 c_1) (not (p1 c_1 c_3)) (not (p1 c_2 c_1)) (not (p1 c_1 c_1)) (not (p4 c_1)) (not (p1 c_2 c_3)) )(or (not (p4 c_3)) (not (p3 c_2)) (= c_1 c_3) (not (p3 c_2)) (= c_2 c_2) (not (p1 c_2 c_3)) (not (p1 c_2 c_1)) (not (p1 c_2 c_1)) (not (p4 c_1)) (not (p1 c_2 c_3)) )(or (not (p4 c_3)) (not (p3 c_2)) (= c_1 c_3) (not (p3 c_3)) (= c_2 c_3) (not (p1 c_3 c_3)) (not (p1 c_2 c_1)) (not (p1 c_3 c_1)) (not (p4 c_1)) (not (p1 c_2 c_3)) )(or (not (p4 c_3)) (not (p3 c_2)) (= c_2 c_3) (not (p3 c_0)) (= c_2 c_0) (not (p1 c_0 c_3)) (not (p1 c_2 c_2)) (not (p1 c_0 c_2)) (not (p4 c_2)) (not (p1 c_2 c_3)) )(or (not (p4 c_3)) (not (p3 c_2)) (= c_2 c_3) (not (p3 c_1)) (= c_2 c_1) (not (p1 c_1 c_3)) (not (p1 c_2 c_2)) (not (p1 c_1 c_2)) (not (p4 c_2)) (not (p1 c_2 c_3)) )(or (not (p4 c_3)) (not (p3 c_2)) (= c_2 c_3) (not (p3 c_2)) (= c_2 c_2) (not (p1 c_2 c_3)) (not (p1 c_2 c_2)) (not (p1 c_2 c_2)) (not (p4 c_2)) (not (p1 c_2 c_3)) )(or (not (p4 c_3)) (not (p3 c_2)) (= c_2 c_3) (not (p3 c_3)) (= c_2 c_3) (not (p1 c_3 c_3)) (not (p1 c_2 c_2)) (not (p1 c_3 c_2)) (not (p4 c_2)) (not (p1 c_2 c_3)) )(or (not (p4 c_3)) (not (p3 c_2)) (= c_3 c_3) (not (p3 c_0)) (= c_2 c_0) (not (p1 c_0 c_3)) (not (p1 c_2 c_3)) (not (p1 c_0 c_3)) (not (p4 c_3)) (not (p1 c_2 c_3)) )(or (not (p4 c_3)) (not (p3 c_2)) (= c_3 c_3) (not (p3 c_1)) (= c_2 c_1) (not (p1 c_1 c_3)) (not (p1 c_2 c_3)) (not (p1 c_1 c_3)) (not (p4 c_3)) (not (p1 c_2 c_3)) )(or (not (p4 c_3)) (not (p3 c_2)) (= c_3 c_3) (not (p3 c_2)) (= c_2 c_2) (not (p1 c_2 c_3)) (not (p1 c_2 c_3)) (not (p1 c_2 c_3)) (not (p4 c_3)) (not (p1 c_2 c_3)) )(or (not (p4 c_3)) (not (p3 c_2)) (= c_3 c_3) (not (p3 c_3)) (= c_2 c_3) (not (p1 c_3 c_3)) (not (p1 c_2 c_3)) (not (p1 c_3 c_3)) (not (p4 c_3)) (not (p1 c_2 c_3)) )(or (not (p4 c_3)) (not (p3 c_3)) (= c_0 c_3) (not (p3 c_0)) (= c_3 c_0) (not (p1 c_0 c_3)) (not (p1 c_3 c_0)) (not (p1 c_0 c_0)) (not (p4 c_0)) (not (p1 c_3 c_3)) )(or (not (p4 c_3)) (not (p3 c_3)) (= c_0 c_3) (not (p3 c_1)) (= c_3 c_1) (not (p1 c_1 c_3)) (not (p1 c_3 c_0)) (not (p1 c_1 c_0)) (not (p4 c_0)) (not (p1 c_3 c_3)) )(or (not (p4 c_3)) (not (p3 c_3)) (= c_0 c_3) (not (p3 c_2)) (= c_3 c_2) (not (p1 c_2 c_3)) (not (p1 c_3 c_0)) (not (p1 c_2 c_0)) (not (p4 c_0)) (not (p1 c_3 c_3)) )(or (not (p4 c_3)) (not (p3 c_3)) (= c_0 c_3) (not (p3 c_3)) (= c_3 c_3) (not (p1 c_3 c_3)) (not (p1 c_3 c_0)) (not (p1 c_3 c_0)) (not (p4 c_0)) (not (p1 c_3 c_3)) )(or (not (p4 c_3)) (not (p3 c_3)) (= c_1 c_3) (not (p3 c_0)) (= c_3 c_0) (not (p1 c_0 c_3)) (not (p1 c_3 c_1)) (not (p1 c_0 c_1)) (not (p4 c_1)) (not (p1 c_3 c_3)) )(or (not (p4 c_3)) (not (p3 c_3)) (= c_1 c_3) (not (p3 c_1)) (= c_3 c_1) (not (p1 c_1 c_3)) (not (p1 c_3 c_1)) (not (p1 c_1 c_1)) (not (p4 c_1)) (not (p1 c_3 c_3)) )(or (not (p4 c_3)) (not (p3 c_3)) (= c_1 c_3) (not (p3 c_2)) (= c_3 c_2) (not (p1 c_2 c_3)) (not (p1 c_3 c_1)) (not (p1 c_2 c_1)) (not (p4 c_1)) (not (p1 c_3 c_3)) )(or (not (p4 c_3)) (not (p3 c_3)) (= c_1 c_3) (not (p3 c_3)) (= c_3 c_3) (not (p1 c_3 c_3)) (not (p1 c_3 c_1)) (not (p1 c_3 c_1)) (not (p4 c_1)) (not (p1 c_3 c_3)) )(or (not (p4 c_3)) (not (p3 c_3)) (= c_2 c_3) (not (p3 c_0)) (= c_3 c_0) (not (p1 c_0 c_3)) (not (p1 c_3 c_2)) (not (p1 c_0 c_2)) (not (p4 c_2)) (not (p1 c_3 c_3)) )(or (not (p4 c_3)) (not (p3 c_3)) (= c_2 c_3) (not (p3 c_1)) (= c_3 c_1) (not (p1 c_1 c_3)) (not (p1 c_3 c_2)) (not (p1 c_1 c_2)) (not (p4 c_2)) (not (p1 c_3 c_3)) )(or (not (p4 c_3)) (not (p3 c_3)) (= c_2 c_3) (not (p3 c_2)) (= c_3 c_2) (not (p1 c_2 c_3)) (not (p1 c_3 c_2)) (not (p1 c_2 c_2)) (not (p4 c_2)) (not (p1 c_3 c_3)) )(or (not (p4 c_3)) (not (p3 c_3)) (= c_2 c_3) (not (p3 c_3)) (= c_3 c_3) (not (p1 c_3 c_3)) (not (p1 c_3 c_2)) (not (p1 c_3 c_2)) (not (p4 c_2)) (not (p1 c_3 c_3)) )(or (not (p4 c_3)) (not (p3 c_3)) (= c_3 c_3) (not (p3 c_0)) (= c_3 c_0) (not (p1 c_0 c_3)) (not (p1 c_3 c_3)) (not (p1 c_0 c_3)) (not (p4 c_3)) (not (p1 c_3 c_3)) )(or (not (p4 c_3)) (not (p3 c_3)) (= c_3 c_3) (not (p3 c_1)) (= c_3 c_1) (not (p1 c_1 c_3)) (not (p1 c_3 c_3)) (not (p1 c_1 c_3)) (not (p4 c_3)) (not (p1 c_3 c_3)) )(or (not (p4 c_3)) (not (p3 c_3)) (= c_3 c_3) (not (p3 c_2)) (= c_3 c_2) (not (p1 c_2 c_3)) (not (p1 c_3 c_3)) (not (p1 c_2 c_3)) (not (p4 c_3)) (not (p1 c_3 c_3)) )(or (not (p4 c_3)) (not (p3 c_3)) (= c_3 c_3) (not (p3 c_3)) (= c_3 c_3) (not (p1 c_3 c_3)) (not (p1 c_3 c_3)) (not (p1 c_3 c_3)) (not (p4 c_3)) (not (p1 c_3 c_3)) )(or (= c_0 c_0) (not (p3 c_0)) (p1 c_0 (f2 c_0 c_0)) (not (p3 c_0)) )(or (= c_0 c_1) (not (p3 c_1)) (p1 c_1 (f2 c_0 c_1)) (not (p3 c_0)) )(or (= c_0 c_2) (not (p3 c_2)) (p1 c_2 (f2 c_0 c_2)) (not (p3 c_0)) )(or (= c_0 c_3) (not (p3 c_3)) (p1 c_3 (f2 c_0 c_3)) (not (p3 c_0)) )(or (= c_1 c_0) (not (p3 c_0)) (p1 c_0 (f2 c_1 c_0)) (not (p3 c_1)) )(or (= c_1 c_1) (not (p3 c_1)) (p1 c_1 (f2 c_1 c_1)) (not (p3 c_1)) )(or (= c_1 c_2) (not (p3 c_2)) (p1 c_2 (f2 c_1 c_2)) (not (p3 c_1)) )(or (= c_1 c_3) (not (p3 c_3)) (p1 c_3 (f2 c_1 c_3)) (not (p3 c_1)) )(or (= c_2 c_0) (not (p3 c_0)) (p1 c_0 (f2 c_2 c_0)) (not (p3 c_2)) )(or (= c_2 c_1) (not (p3 c_1)) (p1 c_1 (f2 c_2 c_1)) (not (p3 c_2)) )(or (= c_2 c_2) (not (p3 c_2)) (p1 c_2 (f2 c_2 c_2)) (not (p3 c_2)) )(or (= c_2 c_3) (not (p3 c_3)) (p1 c_3 (f2 c_2 c_3)) (not (p3 c_2)) )(or (= c_3 c_0) (not (p3 c_0)) (p1 c_0 (f2 c_3 c_0)) (not (p3 c_3)) )(or (= c_3 c_1) (not (p3 c_1)) (p1 c_1 (f2 c_3 c_1)) (not (p3 c_3)) )(or (= c_3 c_2) (not (p3 c_2)) (p1 c_2 (f2 c_3 c_2)) (not (p3 c_3)) )(or (= c_3 c_3) (not (p3 c_3)) (p1 c_3 (f2 c_3 c_3)) (not (p3 c_3)) )(or (= c_0 c_0) (not (p3 c_0)) (p4 (f17 c_0 c_0 c_0)) (= c_0 c_0) (not (p3 c_0)) (not (p14 c_0 c_0 c_0)) (not (p3 c_0)) (= c_0 c_0) )(or (= c_0 c_0) (not (p3 c_0)) (p4 (f17 c_0 c_1 c_0)) (= c_0 c_1) (not (p3 c_1)) (not (p14 c_0 c_1 c_0)) (not (p3 c_0)) (= c_1 c_0) )(or (= c_0 c_0) (not (p3 c_0)) (p4 (f17 c_0 c_2 c_0)) (= c_0 c_2) (not (p3 c_2)) (not (p14 c_0 c_2 c_0)) (not (p3 c_0)) (= c_2 c_0) )(or (= c_0 c_0) (not (p3 c_0)) (p4 (f17 c_0 c_3 c_0)) (= c_0 c_3) (not (p3 c_3)) (not (p14 c_0 c_3 c_0)) (not (p3 c_0)) (= c_3 c_0) )(or (= c_0 c_1) (not (p3 c_1)) (p4 (f17 c_0 c_0 c_1)) (= c_0 c_0) (not (p3 c_0)) (not (p14 c_0 c_0 c_1)) (not (p3 c_0)) (= c_0 c_1) )(or (= c_0 c_1) (not (p3 c_1)) (p4 (f17 c_0 c_1 c_1)) (= c_0 c_1) (not (p3 c_1)) (not (p14 c_0 c_1 c_1)) (not (p3 c_0)) (= c_1 c_1) )(or (= c_0 c_1) (not (p3 c_1)) (p4 (f17 c_0 c_2 c_1)) (= c_0 c_2) (not (p3 c_2)) (not (p14 c_0 c_2 c_1)) (not (p3 c_0)) (= c_2 c_1) )(or (= c_0 c_1) (not (p3 c_1)) (p4 (f17 c_0 c_3 c_1)) (= c_0 c_3) (not (p3 c_3)) (not (p14 c_0 c_3 c_1)) (not (p3 c_0)) (= c_3 c_1) )(or (= c_0 c_2) (not (p3 c_2)) (p4 (f17 c_0 c_0 c_2)) (= c_0 c_0) (not (p3 c_0)) (not (p14 c_0 c_0 c_2)) (not (p3 c_0)) (= c_0 c_2) )(or (= c_0 c_2) (not (p3 c_2)) (p4 (f17 c_0 c_1 c_2)) (= c_0 c_1) (not (p3 c_1)) (not (p14 c_0 c_1 c_2)) (not (p3 c_0)) (= c_1 c_2) )(or (= c_0 c_2) (not (p3 c_2)) (p4 (f17 c_0 c_2 c_2)) (= c_0 c_2) (not (p3 c_2)) (not (p14 c_0 c_2 c_2)) (not (p3 c_0)) (= c_2 c_2) )(or (= c_0 c_2) (not (p3 c_2)) (p4 (f17 c_0 c_3 c_2)) (= c_0 c_3) (not (p3 c_3)) (not (p14 c_0 c_3 c_2)) (not (p3 c_0)) (= c_3 c_2) )(or (= c_0 c_3) (not (p3 c_3)) (p4 (f17 c_0 c_0 c_3)) (= c_0 c_0) (not (p3 c_0)) (not (p14 c_0 c_0 c_3)) (not (p3 c_0)) (= c_0 c_3) )(or (= c_0 c_3) (not (p3 c_3)) (p4 (f17 c_0 c_1 c_3)) (= c_0 c_1) (not (p3 c_1)) (not (p14 c_0 c_1 c_3)) (not (p3 c_0)) (= c_1 c_3) )(or (= c_0 c_3) (not (p3 c_3)) (p4 (f17 c_0 c_2 c_3)) (= c_0 c_2) (not (p3 c_2)) (not (p14 c_0 c_2 c_3)) (not (p3 c_0)) (= c_2 c_3) )(or (= c_0 c_3) (not (p3 c_3)) (p4 (f17 c_0 c_3 c_3)) (= c_0 c_3) (not (p3 c_3)) (not (p14 c_0 c_3 c_3)) (not (p3 c_0)) (= c_3 c_3) )(or (= c_1 c_0) (not (p3 c_0)) (p4 (f17 c_1 c_0 c_0)) (= c_1 c_0) (not (p3 c_0)) (not (p14 c_1 c_0 c_0)) (not (p3 c_1)) (= c_0 c_0) )(or (= c_1 c_0) (not (p3 c_0)) (p4 (f17 c_1 c_1 c_0)) (= c_1 c_1) (not (p3 c_1)) (not (p14 c_1 c_1 c_0)) (not (p3 c_1)) (= c_1 c_0) )(or (= c_1 c_0) (not (p3 c_0)) (p4 (f17 c_1 c_2 c_0)) (= c_1 c_2) (not (p3 c_2)) (not (p14 c_1 c_2 c_0)) (not (p3 c_1)) (= c_2 c_0) )(or (= c_1 c_0) (not (p3 c_0)) (p4 (f17 c_1 c_3 c_0)) (= c_1 c_3) (not (p3 c_3)) (not (p14 c_1 c_3 c_0)) (not (p3 c_1)) (= c_3 c_0) )(or (= c_1 c_1) (not (p3 c_1)) (p4 (f17 c_1 c_0 c_1)) (= c_1 c_0) (not (p3 c_0)) (not (p14 c_1 c_0 c_1)) (not (p3 c_1)) (= c_0 c_1) )(or (= c_1 c_1) (not (p3 c_1)) (p4 (f17 c_1 c_1 c_1)) (= c_1 c_1) (not (p3 c_1)) (not (p14 c_1 c_1 c_1)) (not (p3 c_1)) (= c_1 c_1) )(or (= c_1 c_1) (not (p3 c_1)) (p4 (f17 c_1 c_2 c_1)) (= c_1 c_2) (not (p3 c_2)) (not (p14 c_1 c_2 c_1)) (not (p3 c_1)) (= c_2 c_1) )(or (= c_1 c_1) (not (p3 c_1)) (p4 (f17 c_1 c_3 c_1)) (= c_1 c_3) (not (p3 c_3)) (not (p14 c_1 c_3 c_1)) (not (p3 c_1)) (= c_3 c_1) )(or (= c_1 c_2) (not (p3 c_2)) (p4 (f17 c_1 c_0 c_2)) (= c_1 c_0) (not (p3 c_0)) (not (p14 c_1 c_0 c_2)) (not (p3 c_1)) (= c_0 c_2) )(or (= c_1 c_2) (not (p3 c_2)) (p4 (f17 c_1 c_1 c_2)) (= c_1 c_1) (not (p3 c_1)) (not (p14 c_1 c_1 c_2)) (not (p3 c_1)) (= c_1 c_2) )(or (= c_1 c_2) (not (p3 c_2)) (p4 (f17 c_1 c_2 c_2)) (= c_1 c_2) (not (p3 c_2)) (not (p14 c_1 c_2 c_2)) (not (p3 c_1)) (= c_2 c_2) )(or (= c_1 c_2) (not (p3 c_2)) (p4 (f17 c_1 c_3 c_2)) (= c_1 c_3) (not (p3 c_3)) (not (p14 c_1 c_3 c_2)) (not (p3 c_1)) (= c_3 c_2) )(or (= c_1 c_3) (not (p3 c_3)) (p4 (f17 c_1 c_0 c_3)) (= c_1 c_0) (not (p3 c_0)) (not (p14 c_1 c_0 c_3)) (not (p3 c_1)) (= c_0 c_3) )(or (= c_1 c_3) (not (p3 c_3)) (p4 (f17 c_1 c_1 c_3)) (= c_1 c_1) (not (p3 c_1)) (not (p14 c_1 c_1 c_3)) (not (p3 c_1)) (= c_1 c_3) )(or (= c_1 c_3) (not (p3 c_3)) (p4 (f17 c_1 c_2 c_3)) (= c_1 c_2) (not (p3 c_2)) (not (p14 c_1 c_2 c_3)) (not (p3 c_1)) (= c_2 c_3) )(or (= c_1 c_3) (not (p3 c_3)) (p4 (f17 c_1 c_3 c_3)) (= c_1 c_3) (not (p3 c_3)) (not (p14 c_1 c_3 c_3)) (not (p3 c_1)) (= c_3 c_3) )(or (= c_2 c_0) (not (p3 c_0)) (p4 (f17 c_2 c_0 c_0)) (= c_2 c_0) (not (p3 c_0)) (not (p14 c_2 c_0 c_0)) (not (p3 c_2)) (= c_0 c_0) )(or (= c_2 c_0) (not (p3 c_0)) (p4 (f17 c_2 c_1 c_0)) (= c_2 c_1) (not (p3 c_1)) (not (p14 c_2 c_1 c_0)) (not (p3 c_2)) (= c_1 c_0) )(or (= c_2 c_0) (not (p3 c_0)) (p4 (f17 c_2 c_2 c_0)) (= c_2 c_2) (not (p3 c_2)) (not (p14 c_2 c_2 c_0)) (not (p3 c_2)) (= c_2 c_0) )(or (= c_2 c_0) (not (p3 c_0)) (p4 (f17 c_2 c_3 c_0)) (= c_2 c_3) (not (p3 c_3)) (not (p14 c_2 c_3 c_0)) (not (p3 c_2)) (= c_3 c_0) )(or (= c_2 c_1) (not (p3 c_1)) (p4 (f17 c_2 c_0 c_1)) (= c_2 c_0) (not (p3 c_0)) (not (p14 c_2 c_0 c_1)) (not (p3 c_2)) (= c_0 c_1) )(or (= c_2 c_1) (not (p3 c_1)) (p4 (f17 c_2 c_1 c_1)) (= c_2 c_1) (not (p3 c_1)) (not (p14 c_2 c_1 c_1)) (not (p3 c_2)) (= c_1 c_1) )(or (= c_2 c_1) (not (p3 c_1)) (p4 (f17 c_2 c_2 c_1)) (= c_2 c_2) (not (p3 c_2)) (not (p14 c_2 c_2 c_1)) (not (p3 c_2)) (= c_2 c_1) )(or (= c_2 c_1) (not (p3 c_1)) (p4 (f17 c_2 c_3 c_1)) (= c_2 c_3) (not (p3 c_3)) (not (p14 c_2 c_3 c_1)) (not (p3 c_2)) (= c_3 c_1) )(or (= c_2 c_2) (not (p3 c_2)) (p4 (f17 c_2 c_0 c_2)) (= c_2 c_0) (not (p3 c_0)) (not (p14 c_2 c_0 c_2)) (not (p3 c_2)) (= c_0 c_2) )(or (= c_2 c_2) (not (p3 c_2)) (p4 (f17 c_2 c_1 c_2)) (= c_2 c_1) (not (p3 c_1)) (not (p14 c_2 c_1 c_2)) (not (p3 c_2)) (= c_1 c_2) )(or (= c_2 c_2) (not (p3 c_2)) (p4 (f17 c_2 c_2 c_2)) (= c_2 c_2) (not (p3 c_2)) (not (p14 c_2 c_2 c_2)) (not (p3 c_2)) (= c_2 c_2) )(or (= c_2 c_2) (not (p3 c_2)) (p4 (f17 c_2 c_3 c_2)) (= c_2 c_3) (not (p3 c_3)) (not (p14 c_2 c_3 c_2)) (not (p3 c_2)) (= c_3 c_2) )(or (= c_2 c_3) (not (p3 c_3)) (p4 (f17 c_2 c_0 c_3)) (= c_2 c_0) (not (p3 c_0)) (not (p14 c_2 c_0 c_3)) (not (p3 c_2)) (= c_0 c_3) )(or (= c_2 c_3) (not (p3 c_3)) (p4 (f17 c_2 c_1 c_3)) (= c_2 c_1) (not (p3 c_1)) (not (p14 c_2 c_1 c_3)) (not (p3 c_2)) (= c_1 c_3) )(or (= c_2 c_3) (not (p3 c_3)) (p4 (f17 c_2 c_2 c_3)) (= c_2 c_2) (not (p3 c_2)) (not (p14 c_2 c_2 c_3)) (not (p3 c_2)) (= c_2 c_3) )(or (= c_2 c_3) (not (p3 c_3)) (p4 (f17 c_2 c_3 c_3)) (= c_2 c_3) (not (p3 c_3)) (not (p14 c_2 c_3 c_3)) (not (p3 c_2)) (= c_3 c_3) )(or (= c_3 c_0) (not (p3 c_0)) (p4 (f17 c_3 c_0 c_0)) (= c_3 c_0) (not (p3 c_0)) (not (p14 c_3 c_0 c_0)) (not (p3 c_3)) (= c_0 c_0) )(or (= c_3 c_0) (not (p3 c_0)) (p4 (f17 c_3 c_1 c_0)) (= c_3 c_1) (not (p3 c_1)) (not (p14 c_3 c_1 c_0)) (not (p3 c_3)) (= c_1 c_0) )(or (= c_3 c_0) (not (p3 c_0)) (p4 (f17 c_3 c_2 c_0)) (= c_3 c_2) (not (p3 c_2)) (not (p14 c_3 c_2 c_0)) (not (p3 c_3)) (= c_2 c_0) )(or (= c_3 c_0) (not (p3 c_0)) (p4 (f17 c_3 c_3 c_0)) (= c_3 c_3) (not (p3 c_3)) (not (p14 c_3 c_3 c_0)) (not (p3 c_3)) (= c_3 c_0) )(or (= c_3 c_1) (not (p3 c_1)) (p4 (f17 c_3 c_0 c_1)) (= c_3 c_0) (not (p3 c_0)) (not (p14 c_3 c_0 c_1)) (not (p3 c_3)) (= c_0 c_1) )(or (= c_3 c_1) (not (p3 c_1)) (p4 (f17 c_3 c_1 c_1)) (= c_3 c_1) (not (p3 c_1)) (not (p14 c_3 c_1 c_1)) (not (p3 c_3)) (= c_1 c_1) )(or (= c_3 c_1) (not (p3 c_1)) (p4 (f17 c_3 c_2 c_1)) (= c_3 c_2) (not (p3 c_2)) (not (p14 c_3 c_2 c_1)) (not (p3 c_3)) (= c_2 c_1) )(or (= c_3 c_1) (not (p3 c_1)) (p4 (f17 c_3 c_3 c_1)) (= c_3 c_3) (not (p3 c_3)) (not (p14 c_3 c_3 c_1)) (not (p3 c_3)) (= c_3 c_1) )(or (= c_3 c_2) (not (p3 c_2)) (p4 (f17 c_3 c_0 c_2)) (= c_3 c_0) (not (p3 c_0)) (not (p14 c_3 c_0 c_2)) (not (p3 c_3)) (= c_0 c_2) )(or (= c_3 c_2) (not (p3 c_2)) (p4 (f17 c_3 c_1 c_2)) (= c_3 c_1) (not (p3 c_1)) (not (p14 c_3 c_1 c_2)) (not (p3 c_3)) (= c_1 c_2) )(or (= c_3 c_2) (not (p3 c_2)) (p4 (f17 c_3 c_2 c_2)) (= c_3 c_2) (not (p3 c_2)) (not (p14 c_3 c_2 c_2)) (not (p3 c_3)) (= c_2 c_2) )(or (= c_3 c_2) (not (p3 c_2)) (p4 (f17 c_3 c_3 c_2)) (= c_3 c_3) (not (p3 c_3)) (not (p14 c_3 c_3 c_2)) (not (p3 c_3)) (= c_3 c_2) )(or (= c_3 c_3) (not (p3 c_3)) (p4 (f17 c_3 c_0 c_3)) (= c_3 c_0) (not (p3 c_0)) (not (p14 c_3 c_0 c_3)) (not (p3 c_3)) (= c_0 c_3) )(or (= c_3 c_3) (not (p3 c_3)) (p4 (f17 c_3 c_1 c_3)) (= c_3 c_1) (not (p3 c_1)) (not (p14 c_3 c_1 c_3)) (not (p3 c_3)) (= c_1 c_3) )(or (= c_3 c_3) (not (p3 c_3)) (p4 (f17 c_3 c_2 c_3)) (= c_3 c_2) (not (p3 c_2)) (not (p14 c_3 c_2 c_3)) (not (p3 c_3)) (= c_2 c_3) )(or (= c_3 c_3) (not (p3 c_3)) (p4 (f17 c_3 c_3 c_3)) (= c_3 c_3) (not (p3 c_3)) (not (p14 c_3 c_3 c_3)) (not (p3 c_3)) (= c_3 c_3) )(or (= c_0 c_0) (= c_0 c_0) (= c_0 c_0) (p14 c_0 c_0 c_0) (not (p3 c_0)) (not (p1 c_0 c_0)) (not (p1 c_0 c_0)) (not (p3 c_0)) (not (p4 c_0)) (not (p3 c_0)) (not (p1 c_0 c_0)) )(or (= c_0 c_0) (= c_0 c_0) (= c_0 c_0) (p14 c_0 c_0 c_0) (not (p3 c_0)) (not (p1 c_0 c_1)) (not (p1 c_0 c_1)) (not (p3 c_0)) (not (p4 c_1)) (not (p3 c_0)) (not (p1 c_0 c_1)) )(or (= c_0 c_0) (= c_0 c_0) (= c_0 c_0) (p14 c_0 c_0 c_0) (not (p3 c_0)) (not (p1 c_0 c_2)) (not (p1 c_0 c_2)) (not (p3 c_0)) (not (p4 c_2)) (not (p3 c_0)) (not (p1 c_0 c_2)) )(or (= c_0 c_0) (= c_0 c_0) (= c_0 c_0) (p14 c_0 c_0 c_0) (not (p3 c_0)) (not (p1 c_0 c_3)) (not (p1 c_0 c_3)) (not (p3 c_0)) (not (p4 c_3)) (not (p3 c_0)) (not (p1 c_0 c_3)) )(or (= c_0 c_0) (= c_1 c_0) (= c_0 c_1) (p14 c_0 c_1 c_0) (not (p3 c_0)) (not (p1 c_1 c_0)) (not (p1 c_0 c_0)) (not (p3 c_0)) (not (p4 c_0)) (not (p3 c_1)) (not (p1 c_0 c_0)) )(or (= c_0 c_0) (= c_1 c_0) (= c_0 c_1) (p14 c_0 c_1 c_0) (not (p3 c_0)) (not (p1 c_1 c_1)) (not (p1 c_0 c_1)) (not (p3 c_0)) (not (p4 c_1)) (not (p3 c_1)) (not (p1 c_0 c_1)) )(or (= c_0 c_0) (= c_1 c_0) (= c_0 c_1) (p14 c_0 c_1 c_0) (not (p3 c_0)) (not (p1 c_1 c_2)) (not (p1 c_0 c_2)) (not (p3 c_0)) (not (p4 c_2)) (not (p3 c_1)) (not (p1 c_0 c_2)) )(or (= c_0 c_0) (= c_1 c_0) (= c_0 c_1) (p14 c_0 c_1 c_0) (not (p3 c_0)) (not (p1 c_1 c_3)) (not (p1 c_0 c_3)) (not (p3 c_0)) (not (p4 c_3)) (not (p3 c_1)) (not (p1 c_0 c_3)) )(or (= c_0 c_0) (= c_2 c_0) (= c_0 c_2) (p14 c_0 c_2 c_0) (not (p3 c_0)) (not (p1 c_2 c_0)) (not (p1 c_0 c_0)) (not (p3 c_0)) (not (p4 c_0)) (not (p3 c_2)) (not (p1 c_0 c_0)) )(or (= c_0 c_0) (= c_2 c_0) (= c_0 c_2) (p14 c_0 c_2 c_0) (not (p3 c_0)) (not (p1 c_2 c_1)) (not (p1 c_0 c_1)) (not (p3 c_0)) (not (p4 c_1)) (not (p3 c_2)) (not (p1 c_0 c_1)) )(or (= c_0 c_0) (= c_2 c_0) (= c_0 c_2) (p14 c_0 c_2 c_0) (not (p3 c_0)) (not (p1 c_2 c_2)) (not (p1 c_0 c_2)) (not (p3 c_0)) (not (p4 c_2)) (not (p3 c_2)) (not (p1 c_0 c_2)) )(or (= c_0 c_0) (= c_2 c_0) (= c_0 c_2) (p14 c_0 c_2 c_0) (not (p3 c_0)) (not (p1 c_2 c_3)) (not (p1 c_0 c_3)) (not (p3 c_0)) (not (p4 c_3)) (not (p3 c_2)) (not (p1 c_0 c_3)) )(or (= c_0 c_0) (= c_3 c_0) (= c_0 c_3) (p14 c_0 c_3 c_0) (not (p3 c_0)) (not (p1 c_3 c_0)) (not (p1 c_0 c_0)) (not (p3 c_0)) (not (p4 c_0)) (not (p3 c_3)) (not (p1 c_0 c_0)) )(or (= c_0 c_0) (= c_3 c_0) (= c_0 c_3) (p14 c_0 c_3 c_0) (not (p3 c_0)) (not (p1 c_3 c_1)) (not (p1 c_0 c_1)) (not (p3 c_0)) (not (p4 c_1)) (not (p3 c_3)) (not (p1 c_0 c_1)) )(or (= c_0 c_0) (= c_3 c_0) (= c_0 c_3) (p14 c_0 c_3 c_0) (not (p3 c_0)) (not (p1 c_3 c_2)) (not (p1 c_0 c_2)) (not (p3 c_0)) (not (p4 c_2)) (not (p3 c_3)) (not (p1 c_0 c_2)) )(or (= c_0 c_0) (= c_3 c_0) (= c_0 c_3) (p14 c_0 c_3 c_0) (not (p3 c_0)) (not (p1 c_3 c_3)) (not (p1 c_0 c_3)) (not (p3 c_0)) (not (p4 c_3)) (not (p3 c_3)) (not (p1 c_0 c_3)) )(or (= c_0 c_1) (= c_0 c_1) (= c_0 c_0) (p14 c_0 c_0 c_1) (not (p3 c_0)) (not (p1 c_0 c_0)) (not (p1 c_0 c_0)) (not (p3 c_1)) (not (p4 c_0)) (not (p3 c_0)) (not (p1 c_1 c_0)) )(or (= c_0 c_1) (= c_0 c_1) (= c_0 c_0) (p14 c_0 c_0 c_1) (not (p3 c_0)) (not (p1 c_0 c_1)) (not (p1 c_0 c_1)) (not (p3 c_1)) (not (p4 c_1)) (not (p3 c_0)) (not (p1 c_1 c_1)) )(or (= c_0 c_1) (= c_0 c_1) (= c_0 c_0) (p14 c_0 c_0 c_1) (not (p3 c_0)) (not (p1 c_0 c_2)) (not (p1 c_0 c_2)) (not (p3 c_1)) (not (p4 c_2)) (not (p3 c_0)) (not (p1 c_1 c_2)) )(or (= c_0 c_1) (= c_0 c_1) (= c_0 c_0) (p14 c_0 c_0 c_1) (not (p3 c_0)) (not (p1 c_0 c_3)) (not (p1 c_0 c_3)) (not (p3 c_1)) (not (p4 c_3)) (not (p3 c_0)) (not (p1 c_1 c_3)) )(or (= c_0 c_1) (= c_1 c_1) (= c_0 c_1) (p14 c_0 c_1 c_1) (not (p3 c_0)) (not (p1 c_1 c_0)) (not (p1 c_0 c_0)) (not (p3 c_1)) (not (p4 c_0)) (not (p3 c_1)) (not (p1 c_1 c_0)) )(or (= c_0 c_1) (= c_1 c_1) (= c_0 c_1) (p14 c_0 c_1 c_1) (not (p3 c_0)) (not (p1 c_1 c_1)) (not (p1 c_0 c_1)) (not (p3 c_1)) (not (p4 c_1)) (not (p3 c_1)) (not (p1 c_1 c_1)) )(or (= c_0 c_1) (= c_1 c_1) (= c_0 c_1) (p14 c_0 c_1 c_1) (not (p3 c_0)) (not (p1 c_1 c_2)) (not (p1 c_0 c_2)) (not (p3 c_1)) (not (p4 c_2)) (not (p3 c_1)) (not (p1 c_1 c_2)) )(or (= c_0 c_1) (= c_1 c_1) (= c_0 c_1) (p14 c_0 c_1 c_1) (not (p3 c_0)) (not (p1 c_1 c_3)) (not (p1 c_0 c_3)) (not (p3 c_1)) (not (p4 c_3)) (not (p3 c_1)) (not (p1 c_1 c_3)) )(or (= c_0 c_1) (= c_2 c_1) (= c_0 c_2) (p14 c_0 c_2 c_1) (not (p3 c_0)) (not (p1 c_2 c_0)) (not (p1 c_0 c_0)) (not (p3 c_1)) (not (p4 c_0)) (not (p3 c_2)) (not (p1 c_1 c_0)) )(or (= c_0 c_1) (= c_2 c_1) (= c_0 c_2) (p14 c_0 c_2 c_1) (not (p3 c_0)) (not (p1 c_2 c_1)) (not (p1 c_0 c_1)) (not (p3 c_1)) (not (p4 c_1)) (not (p3 c_2)) (not (p1 c_1 c_1)) )(or (= c_0 c_1) (= c_2 c_1) (= c_0 c_2) (p14 c_0 c_2 c_1) (not (p3 c_0)) (not (p1 c_2 c_2)) (not (p1 c_0 c_2)) (not (p3 c_1)) (not (p4 c_2)) (not (p3 c_2)) (not (p1 c_1 c_2)) )(or (= c_0 c_1) (= c_2 c_1) (= c_0 c_2) (p14 c_0 c_2 c_1) (not (p3 c_0)) (not (p1 c_2 c_3)) (not (p1 c_0 c_3)) (not (p3 c_1)) (not (p4 c_3)) (not (p3 c_2)) (not (p1 c_1 c_3)) )(or (= c_0 c_1) (= c_3 c_1) (= c_0 c_3) (p14 c_0 c_3 c_1) (not (p3 c_0)) (not (p1 c_3 c_0)) (not (p1 c_0 c_0)) (not (p3 c_1)) (not (p4 c_0)) (not (p3 c_3)) (not (p1 c_1 c_0)) )(or (= c_0 c_1) (= c_3 c_1) (= c_0 c_3) (p14 c_0 c_3 c_1) (not (p3 c_0)) (not (p1 c_3 c_1)) (not (p1 c_0 c_1)) (not (p3 c_1)) (not (p4 c_1)) (not (p3 c_3)) (not (p1 c_1 c_1)) )(or (= c_0 c_1) (= c_3 c_1) (= c_0 c_3) (p14 c_0 c_3 c_1) (not (p3 c_0)) (not (p1 c_3 c_2)) (not (p1 c_0 c_2)) (not (p3 c_1)) (not (p4 c_2)) (not (p3 c_3)) (not (p1 c_1 c_2)) )(or (= c_0 c_1) (= c_3 c_1) (= c_0 c_3) (p14 c_0 c_3 c_1) (not (p3 c_0)) (not (p1 c_3 c_3)) (not (p1 c_0 c_3)) (not (p3 c_1)) (not (p4 c_3)) (not (p3 c_3)) (not (p1 c_1 c_3)) )(or (= c_0 c_2) (= c_0 c_2) (= c_0 c_0) (p14 c_0 c_0 c_2) (not (p3 c_0)) (not (p1 c_0 c_0)) (not (p1 c_0 c_0)) (not (p3 c_2)) (not (p4 c_0)) (not (p3 c_0)) (not (p1 c_2 c_0)) )(or (= c_0 c_2) (= c_0 c_2) (= c_0 c_0) (p14 c_0 c_0 c_2) (not (p3 c_0)) (not (p1 c_0 c_1)) (not (p1 c_0 c_1)) (not (p3 c_2)) (not (p4 c_1)) (not (p3 c_0)) (not (p1 c_2 c_1)) )(or (= c_0 c_2) (= c_0 c_2) (= c_0 c_0) (p14 c_0 c_0 c_2) (not (p3 c_0)) (not (p1 c_0 c_2)) (not (p1 c_0 c_2)) (not (p3 c_2)) (not (p4 c_2)) (not (p3 c_0)) (not (p1 c_2 c_2)) )(or (= c_0 c_2) (= c_0 c_2) (= c_0 c_0) (p14 c_0 c_0 c_2) (not (p3 c_0)) (not (p1 c_0 c_3)) (not (p1 c_0 c_3)) (not (p3 c_2)) (not (p4 c_3)) (not (p3 c_0)) (not (p1 c_2 c_3)) )(or (= c_0 c_2) (= c_1 c_2) (= c_0 c_1) (p14 c_0 c_1 c_2) (not (p3 c_0)) (not (p1 c_1 c_0)) (not (p1 c_0 c_0)) (not (p3 c_2)) (not (p4 c_0)) (not (p3 c_1)) (not (p1 c_2 c_0)) )(or (= c_0 c_2) (= c_1 c_2) (= c_0 c_1) (p14 c_0 c_1 c_2) (not (p3 c_0)) (not (p1 c_1 c_1)) (not (p1 c_0 c_1)) (not (p3 c_2)) (not (p4 c_1)) (not (p3 c_1)) (not (p1 c_2 c_1)) )(or (= c_0 c_2) (= c_1 c_2) (= c_0 c_1) (p14 c_0 c_1 c_2) (not (p3 c_0)) (not (p1 c_1 c_2)) (not (p1 c_0 c_2)) (not (p3 c_2)) (not (p4 c_2)) (not (p3 c_1)) (not (p1 c_2 c_2)) )(or (= c_0 c_2) (= c_1 c_2) (= c_0 c_1) (p14 c_0 c_1 c_2) (not (p3 c_0)) (not (p1 c_1 c_3)) (not (p1 c_0 c_3)) (not (p3 c_2)) (not (p4 c_3)) (not (p3 c_1)) (not (p1 c_2 c_3)) )(or (= c_0 c_2) (= c_2 c_2) (= c_0 c_2) (p14 c_0 c_2 c_2) (not (p3 c_0)) (not (p1 c_2 c_0)) (not (p1 c_0 c_0)) (not (p3 c_2)) (not (p4 c_0)) (not (p3 c_2)) (not (p1 c_2 c_0)) )(or (= c_0 c_2) (= c_2 c_2) (= c_0 c_2) (p14 c_0 c_2 c_2) (not (p3 c_0)) (not (p1 c_2 c_1)) (not (p1 c_0 c_1)) (not (p3 c_2)) (not (p4 c_1)) (not (p3 c_2)) (not (p1 c_2 c_1)) )(or (= c_0 c_2) (= c_2 c_2) (= c_0 c_2) (p14 c_0 c_2 c_2) (not (p3 c_0)) (not (p1 c_2 c_2)) (not (p1 c_0 c_2)) (not (p3 c_2)) (not (p4 c_2)) (not (p3 c_2)) (not (p1 c_2 c_2)) )(or (= c_0 c_2) (= c_2 c_2) (= c_0 c_2) (p14 c_0 c_2 c_2) (not (p3 c_0)) (not (p1 c_2 c_3)) (not (p1 c_0 c_3)) (not (p3 c_2)) (not (p4 c_3)) (not (p3 c_2)) (not (p1 c_2 c_3)) )(or (= c_0 c_2) (= c_3 c_2) (= c_0 c_3) (p14 c_0 c_3 c_2) (not (p3 c_0)) (not (p1 c_3 c_0)) (not (p1 c_0 c_0)) (not (p3 c_2)) (not (p4 c_0)) (not (p3 c_3)) (not (p1 c_2 c_0)) )(or (= c_0 c_2) (= c_3 c_2) (= c_0 c_3) (p14 c_0 c_3 c_2) (not (p3 c_0)) (not (p1 c_3 c_1)) (not (p1 c_0 c_1)) (not (p3 c_2)) (not (p4 c_1)) (not (p3 c_3)) (not (p1 c_2 c_1)) )(or (= c_0 c_2) (= c_3 c_2) (= c_0 c_3) (p14 c_0 c_3 c_2) (not (p3 c_0)) (not (p1 c_3 c_2)) (not (p1 c_0 c_2)) (not (p3 c_2)) (not (p4 c_2)) (not (p3 c_3)) (not (p1 c_2 c_2)) )(or (= c_0 c_2) (= c_3 c_2) (= c_0 c_3) (p14 c_0 c_3 c_2) (not (p3 c_0)) (not (p1 c_3 c_3)) (not (p1 c_0 c_3)) (not (p3 c_2)) (not (p4 c_3)) (not (p3 c_3)) (not (p1 c_2 c_3)) )(or (= c_0 c_3) (= c_0 c_3) (= c_0 c_0) (p14 c_0 c_0 c_3) (not (p3 c_0)) (not (p1 c_0 c_0)) (not (p1 c_0 c_0)) (not (p3 c_3)) (not (p4 c_0)) (not (p3 c_0)) (not (p1 c_3 c_0)) )(or (= c_0 c_3) (= c_0 c_3) (= c_0 c_0) (p14 c_0 c_0 c_3) (not (p3 c_0)) (not (p1 c_0 c_1)) (not (p1 c_0 c_1)) (not (p3 c_3)) (not (p4 c_1)) (not (p3 c_0)) (not (p1 c_3 c_1)) )(or (= c_0 c_3) (= c_0 c_3) (= c_0 c_0) (p14 c_0 c_0 c_3) (not (p3 c_0)) (not (p1 c_0 c_2)) (not (p1 c_0 c_2)) (not (p3 c_3)) (not (p4 c_2)) (not (p3 c_0)) (not (p1 c_3 c_2)) )(or (= c_0 c_3) (= c_0 c_3) (= c_0 c_0) (p14 c_0 c_0 c_3) (not (p3 c_0)) (not (p1 c_0 c_3)) (not (p1 c_0 c_3)) (not (p3 c_3)) (not (p4 c_3)) (not (p3 c_0)) (not (p1 c_3 c_3)) )(or (= c_0 c_3) (= c_1 c_3) (= c_0 c_1) (p14 c_0 c_1 c_3) (not (p3 c_0)) (not (p1 c_1 c_0)) (not (p1 c_0 c_0)) (not (p3 c_3)) (not (p4 c_0)) (not (p3 c_1)) (not (p1 c_3 c_0)) )(or (= c_0 c_3) (= c_1 c_3) (= c_0 c_1) (p14 c_0 c_1 c_3) (not (p3 c_0)) (not (p1 c_1 c_1)) (not (p1 c_0 c_1)) (not (p3 c_3)) (not (p4 c_1)) (not (p3 c_1)) (not (p1 c_3 c_1)) )(or (= c_0 c_3) (= c_1 c_3) (= c_0 c_1) (p14 c_0 c_1 c_3) (not (p3 c_0)) (not (p1 c_1 c_2)) (not (p1 c_0 c_2)) (not (p3 c_3)) (not (p4 c_2)) (not (p3 c_1)) (not (p1 c_3 c_2)) )(or (= c_0 c_3) (= c_1 c_3) (= c_0 c_1) (p14 c_0 c_1 c_3) (not (p3 c_0)) (not (p1 c_1 c_3)) (not (p1 c_0 c_3)) (not (p3 c_3)) (not (p4 c_3)) (not (p3 c_1)) (not (p1 c_3 c_3)) )(or (= c_0 c_3) (= c_2 c_3) (= c_0 c_2) (p14 c_0 c_2 c_3) (not (p3 c_0)) (not (p1 c_2 c_0)) (not (p1 c_0 c_0)) (not (p3 c_3)) (not (p4 c_0)) (not (p3 c_2)) (not (p1 c_3 c_0)) )(or (= c_0 c_3) (= c_2 c_3) (= c_0 c_2) (p14 c_0 c_2 c_3) (not (p3 c_0)) (not (p1 c_2 c_1)) (not (p1 c_0 c_1)) (not (p3 c_3)) (not (p4 c_1)) (not (p3 c_2)) (not (p1 c_3 c_1)) )(or (= c_0 c_3) (= c_2 c_3) (= c_0 c_2) (p14 c_0 c_2 c_3) (not (p3 c_0)) (not (p1 c_2 c_2)) (not (p1 c_0 c_2)) (not (p3 c_3)) (not (p4 c_2)) (not (p3 c_2)) (not (p1 c_3 c_2)) )(or (= c_0 c_3) (= c_2 c_3) (= c_0 c_2) (p14 c_0 c_2 c_3) (not (p3 c_0)) (not (p1 c_2 c_3)) (not (p1 c_0 c_3)) (not (p3 c_3)) (not (p4 c_3)) (not (p3 c_2)) (not (p1 c_3 c_3)) )(or (= c_0 c_3) (= c_3 c_3) (= c_0 c_3) (p14 c_0 c_3 c_3) (not (p3 c_0)) (not (p1 c_3 c_0)) (not (p1 c_0 c_0)) (not (p3 c_3)) (not (p4 c_0)) (not (p3 c_3)) (not (p1 c_3 c_0)) )(or (= c_0 c_3) (= c_3 c_3) (= c_0 c_3) (p14 c_0 c_3 c_3) (not (p3 c_0)) (not (p1 c_3 c_1)) (not (p1 c_0 c_1)) (not (p3 c_3)) (not (p4 c_1)) (not (p3 c_3)) (not (p1 c_3 c_1)) )(or (= c_0 c_3) (= c_3 c_3) (= c_0 c_3) (p14 c_0 c_3 c_3) (not (p3 c_0)) (not (p1 c_3 c_2)) (not (p1 c_0 c_2)) (not (p3 c_3)) (not (p4 c_2)) (not (p3 c_3)) (not (p1 c_3 c_2)) )(or (= c_0 c_3) (= c_3 c_3) (= c_0 c_3) (p14 c_0 c_3 c_3) (not (p3 c_0)) (not (p1 c_3 c_3)) (not (p1 c_0 c_3)) (not (p3 c_3)) (not (p4 c_3)) (not (p3 c_3)) (not (p1 c_3 c_3)) )(or (= c_1 c_0) (= c_0 c_0) (= c_1 c_0) (p14 c_1 c_0 c_0) (not (p3 c_1)) (not (p1 c_0 c_0)) (not (p1 c_1 c_0)) (not (p3 c_0)) (not (p4 c_0)) (not (p3 c_0)) (not (p1 c_0 c_0)) )(or (= c_1 c_0) (= c_0 c_0) (= c_1 c_0) (p14 c_1 c_0 c_0) (not (p3 c_1)) (not (p1 c_0 c_1)) (not (p1 c_1 c_1)) (not (p3 c_0)) (not (p4 c_1)) (not (p3 c_0)) (not (p1 c_0 c_1)) )(or (= c_1 c_0) (= c_0 c_0) (= c_1 c_0) (p14 c_1 c_0 c_0) (not (p3 c_1)) (not (p1 c_0 c_2)) (not (p1 c_1 c_2)) (not (p3 c_0)) (not (p4 c_2)) (not (p3 c_0)) (not (p1 c_0 c_2)) )(or (= c_1 c_0) (= c_0 c_0) (= c_1 c_0) (p14 c_1 c_0 c_0) (not (p3 c_1)) (not (p1 c_0 c_3)) (not (p1 c_1 c_3)) (not (p3 c_0)) (not (p4 c_3)) (not (p3 c_0)) (not (p1 c_0 c_3)) )(or (= c_1 c_0) (= c_1 c_0) (= c_1 c_1) (p14 c_1 c_1 c_0) (not (p3 c_1)) (not (p1 c_1 c_0)) (not (p1 c_1 c_0)) (not (p3 c_0)) (not (p4 c_0)) (not (p3 c_1)) (not (p1 c_0 c_0)) )(or (= c_1 c_0) (= c_1 c_0) (= c_1 c_1) (p14 c_1 c_1 c_0) (not (p3 c_1)) (not (p1 c_1 c_1)) (not (p1 c_1 c_1)) (not (p3 c_0)) (not (p4 c_1)) (not (p3 c_1)) (not (p1 c_0 c_1)) )(or (= c_1 c_0) (= c_1 c_0) (= c_1 c_1) (p14 c_1 c_1 c_0) (not (p3 c_1)) (not (p1 c_1 c_2)) (not (p1 c_1 c_2)) (not (p3 c_0)) (not (p4 c_2)) (not (p3 c_1)) (not (p1 c_0 c_2)) )(or (= c_1 c_0) (= c_1 c_0) (= c_1 c_1) (p14 c_1 c_1 c_0) (not (p3 c_1)) (not (p1 c_1 c_3)) (not (p1 c_1 c_3)) (not (p3 c_0)) (not (p4 c_3)) (not (p3 c_1)) (not (p1 c_0 c_3)) )(or (= c_1 c_0) (= c_2 c_0) (= c_1 c_2) (p14 c_1 c_2 c_0) (not (p3 c_1)) (not (p1 c_2 c_0)) (not (p1 c_1 c_0)) (not (p3 c_0)) (not (p4 c_0)) (not (p3 c_2)) (not (p1 c_0 c_0)) )(or (= c_1 c_0) (= c_2 c_0) (= c_1 c_2) (p14 c_1 c_2 c_0) (not (p3 c_1)) (not (p1 c_2 c_1)) (not (p1 c_1 c_1)) (not (p3 c_0)) (not (p4 c_1)) (not (p3 c_2)) (not (p1 c_0 c_1)) )(or (= c_1 c_0) (= c_2 c_0) (= c_1 c_2) (p14 c_1 c_2 c_0) (not (p3 c_1)) (not (p1 c_2 c_2)) (not (p1 c_1 c_2)) (not (p3 c_0)) (not (p4 c_2)) (not (p3 c_2)) (not (p1 c_0 c_2)) )(or (= c_1 c_0) (= c_2 c_0) (= c_1 c_2) (p14 c_1 c_2 c_0) (not (p3 c_1)) (not (p1 c_2 c_3)) (not (p1 c_1 c_3)) (not (p3 c_0)) (not (p4 c_3)) (not (p3 c_2)) (not (p1 c_0 c_3)) )(or (= c_1 c_0) (= c_3 c_0) (= c_1 c_3) (p14 c_1 c_3 c_0) (not (p3 c_1)) (not (p1 c_3 c_0)) (not (p1 c_1 c_0)) (not (p3 c_0)) (not (p4 c_0)) (not (p3 c_3)) (not (p1 c_0 c_0)) )(or (= c_1 c_0) (= c_3 c_0) (= c_1 c_3) (p14 c_1 c_3 c_0) (not (p3 c_1)) (not (p1 c_3 c_1)) (not (p1 c_1 c_1)) (not (p3 c_0)) (not (p4 c_1)) (not (p3 c_3)) (not (p1 c_0 c_1)) )(or (= c_1 c_0) (= c_3 c_0) (= c_1 c_3) (p14 c_1 c_3 c_0) (not (p3 c_1)) (not (p1 c_3 c_2)) (not (p1 c_1 c_2)) (not (p3 c_0)) (not (p4 c_2)) (not (p3 c_3)) (not (p1 c_0 c_2)) )(or (= c_1 c_0) (= c_3 c_0) (= c_1 c_3) (p14 c_1 c_3 c_0) (not (p3 c_1)) (not (p1 c_3 c_3)) (not (p1 c_1 c_3)) (not (p3 c_0)) (not (p4 c_3)) (not (p3 c_3)) (not (p1 c_0 c_3)) )(or (= c_1 c_1) (= c_0 c_1) (= c_1 c_0) (p14 c_1 c_0 c_1) (not (p3 c_1)) (not (p1 c_0 c_0)) (not (p1 c_1 c_0)) (not (p3 c_1)) (not (p4 c_0)) (not (p3 c_0)) (not (p1 c_1 c_0)) )(or (= c_1 c_1) (= c_0 c_1) (= c_1 c_0) (p14 c_1 c_0 c_1) (not (p3 c_1)) (not (p1 c_0 c_1)) (not (p1 c_1 c_1)) (not (p3 c_1)) (not (p4 c_1)) (not (p3 c_0)) (not (p1 c_1 c_1)) )(or (= c_1 c_1) (= c_0 c_1) (= c_1 c_0) (p14 c_1 c_0 c_1) (not (p3 c_1)) (not (p1 c_0 c_2)) (not (p1 c_1 c_2)) (not (p3 c_1)) (not (p4 c_2)) (not (p3 c_0)) (not (p1 c_1 c_2)) )(or (= c_1 c_1) (= c_0 c_1) (= c_1 c_0) (p14 c_1 c_0 c_1) (not (p3 c_1)) (not (p1 c_0 c_3)) (not (p1 c_1 c_3)) (not (p3 c_1)) (not (p4 c_3)) (not (p3 c_0)) (not (p1 c_1 c_3)) )(or (= c_1 c_1) (= c_1 c_1) (= c_1 c_1) (p14 c_1 c_1 c_1) (not (p3 c_1)) (not (p1 c_1 c_0)) (not (p1 c_1 c_0)) (not (p3 c_1)) (not (p4 c_0)) (not (p3 c_1)) (not (p1 c_1 c_0)) )(or (= c_1 c_1) (= c_1 c_1) (= c_1 c_1) (p14 c_1 c_1 c_1) (not (p3 c_1)) (not (p1 c_1 c_1)) (not (p1 c_1 c_1)) (not (p3 c_1)) (not (p4 c_1)) (not (p3 c_1)) (not (p1 c_1 c_1)) )(or (= c_1 c_1) (= c_1 c_1) (= c_1 c_1) (p14 c_1 c_1 c_1) (not (p3 c_1)) (not (p1 c_1 c_2)) (not (p1 c_1 c_2)) (not (p3 c_1)) (not (p4 c_2)) (not (p3 c_1)) (not (p1 c_1 c_2)) )(or (= c_1 c_1) (= c_1 c_1) (= c_1 c_1) (p14 c_1 c_1 c_1) (not (p3 c_1)) (not (p1 c_1 c_3)) (not (p1 c_1 c_3)) (not (p3 c_1)) (not (p4 c_3)) (not (p3 c_1)) (not (p1 c_1 c_3)) )(or (= c_1 c_1) (= c_2 c_1) (= c_1 c_2) (p14 c_1 c_2 c_1) (not (p3 c_1)) (not (p1 c_2 c_0)) (not (p1 c_1 c_0)) (not (p3 c_1)) (not (p4 c_0)) (not (p3 c_2)) (not (p1 c_1 c_0)) )(or (= c_1 c_1) (= c_2 c_1) (= c_1 c_2) (p14 c_1 c_2 c_1) (not (p3 c_1)) (not (p1 c_2 c_1)) (not (p1 c_1 c_1)) (not (p3 c_1)) (not (p4 c_1)) (not (p3 c_2)) (not (p1 c_1 c_1)) )(or (= c_1 c_1) (= c_2 c_1) (= c_1 c_2) (p14 c_1 c_2 c_1) (not (p3 c_1)) (not (p1 c_2 c_2)) (not (p1 c_1 c_2)) (not (p3 c_1)) (not (p4 c_2)) (not (p3 c_2)) (not (p1 c_1 c_2)) )(or (= c_1 c_1) (= c_2 c_1) (= c_1 c_2) (p14 c_1 c_2 c_1) (not (p3 c_1)) (not (p1 c_2 c_3)) (not (p1 c_1 c_3)) (not (p3 c_1)) (not (p4 c_3)) (not (p3 c_2)) (not (p1 c_1 c_3)) )(or (= c_1 c_1) (= c_3 c_1) (= c_1 c_3) (p14 c_1 c_3 c_1) (not (p3 c_1)) (not (p1 c_3 c_0)) (not (p1 c_1 c_0)) (not (p3 c_1)) (not (p4 c_0)) (not (p3 c_3)) (not (p1 c_1 c_0)) )(or (= c_1 c_1) (= c_3 c_1) (= c_1 c_3) (p14 c_1 c_3 c_1) (not (p3 c_1)) (not (p1 c_3 c_1)) (not (p1 c_1 c_1)) (not (p3 c_1)) (not (p4 c_1)) (not (p3 c_3)) (not (p1 c_1 c_1)) )(or (= c_1 c_1) (= c_3 c_1) (= c_1 c_3) (p14 c_1 c_3 c_1) (not (p3 c_1)) (not (p1 c_3 c_2)) (not (p1 c_1 c_2)) (not (p3 c_1)) (not (p4 c_2)) (not (p3 c_3)) (not (p1 c_1 c_2)) )(or (= c_1 c_1) (= c_3 c_1) (= c_1 c_3) (p14 c_1 c_3 c_1) (not (p3 c_1)) (not (p1 c_3 c_3)) (not (p1 c_1 c_3)) (not (p3 c_1)) (not (p4 c_3)) (not (p3 c_3)) (not (p1 c_1 c_3)) )(or (= c_1 c_2) (= c_0 c_2) (= c_1 c_0) (p14 c_1 c_0 c_2) (not (p3 c_1)) (not (p1 c_0 c_0)) (not (p1 c_1 c_0)) (not (p3 c_2)) (not (p4 c_0)) (not (p3 c_0)) (not (p1 c_2 c_0)) )(or (= c_1 c_2) (= c_0 c_2) (= c_1 c_0) (p14 c_1 c_0 c_2) (not (p3 c_1)) (not (p1 c_0 c_1)) (not (p1 c_1 c_1)) (not (p3 c_2)) (not (p4 c_1)) (not (p3 c_0)) (not (p1 c_2 c_1)) )(or (= c_1 c_2) (= c_0 c_2) (= c_1 c_0) (p14 c_1 c_0 c_2) (not (p3 c_1)) (not (p1 c_0 c_2)) (not (p1 c_1 c_2)) (not (p3 c_2)) (not (p4 c_2)) (not (p3 c_0)) (not (p1 c_2 c_2)) )(or (= c_1 c_2) (= c_0 c_2) (= c_1 c_0) (p14 c_1 c_0 c_2) (not (p3 c_1)) (not (p1 c_0 c_3)) (not (p1 c_1 c_3)) (not (p3 c_2)) (not (p4 c_3)) (not (p3 c_0)) (not (p1 c_2 c_3)) )(or (= c_1 c_2) (= c_1 c_2) (= c_1 c_1) (p14 c_1 c_1 c_2) (not (p3 c_1)) (not (p1 c_1 c_0)) (not (p1 c_1 c_0)) (not (p3 c_2)) (not (p4 c_0)) (not (p3 c_1)) (not (p1 c_2 c_0)) )(or (= c_1 c_2) (= c_1 c_2) (= c_1 c_1) (p14 c_1 c_1 c_2) (not (p3 c_1)) (not (p1 c_1 c_1)) (not (p1 c_1 c_1)) (not (p3 c_2)) (not (p4 c_1)) (not (p3 c_1)) (not (p1 c_2 c_1)) )(or (= c_1 c_2) (= c_1 c_2) (= c_1 c_1) (p14 c_1 c_1 c_2) (not (p3 c_1)) (not (p1 c_1 c_2)) (not (p1 c_1 c_2)) (not (p3 c_2)) (not (p4 c_2)) (not (p3 c_1)) (not (p1 c_2 c_2)) )(or (= c_1 c_2) (= c_1 c_2) (= c_1 c_1) (p14 c_1 c_1 c_2) (not (p3 c_1)) (not (p1 c_1 c_3)) (not (p1 c_1 c_3)) (not (p3 c_2)) (not (p4 c_3)) (not (p3 c_1)) (not (p1 c_2 c_3)) )(or (= c_1 c_2) (= c_2 c_2) (= c_1 c_2) (p14 c_1 c_2 c_2) (not (p3 c_1)) (not (p1 c_2 c_0)) (not (p1 c_1 c_0)) (not (p3 c_2)) (not (p4 c_0)) (not (p3 c_2)) (not (p1 c_2 c_0)) )(or (= c_1 c_2) (= c_2 c_2) (= c_1 c_2) (p14 c_1 c_2 c_2) (not (p3 c_1)) (not (p1 c_2 c_1)) (not (p1 c_1 c_1)) (not (p3 c_2)) (not (p4 c_1)) (not (p3 c_2)) (not (p1 c_2 c_1)) )(or (= c_1 c_2) (= c_2 c_2) (= c_1 c_2) (p14 c_1 c_2 c_2) (not (p3 c_1)) (not (p1 c_2 c_2)) (not (p1 c_1 c_2)) (not (p3 c_2)) (not (p4 c_2)) (not (p3 c_2)) (not (p1 c_2 c_2)) )(or (= c_1 c_2) (= c_2 c_2) (= c_1 c_2) (p14 c_1 c_2 c_2) (not (p3 c_1)) (not (p1 c_2 c_3)) (not (p1 c_1 c_3)) (not (p3 c_2)) (not (p4 c_3)) (not (p3 c_2)) (not (p1 c_2 c_3)) )(or (= c_1 c_2) (= c_3 c_2) (= c_1 c_3) (p14 c_1 c_3 c_2) (not (p3 c_1)) (not (p1 c_3 c_0)) (not (p1 c_1 c_0)) (not (p3 c_2)) (not (p4 c_0)) (not (p3 c_3)) (not (p1 c_2 c_0)) )(or (= c_1 c_2) (= c_3 c_2) (= c_1 c_3) (p14 c_1 c_3 c_2) (not (p3 c_1)) (not (p1 c_3 c_1)) (not (p1 c_1 c_1)) (not (p3 c_2)) (not (p4 c_1)) (not (p3 c_3)) (not (p1 c_2 c_1)) )(or (= c_1 c_2) (= c_3 c_2) (= c_1 c_3) (p14 c_1 c_3 c_2) (not (p3 c_1)) (not (p1 c_3 c_2)) (not (p1 c_1 c_2)) (not (p3 c_2)) (not (p4 c_2)) (not (p3 c_3)) (not (p1 c_2 c_2)) )(or (= c_1 c_2) (= c_3 c_2) (= c_1 c_3) (p14 c_1 c_3 c_2) (not (p3 c_1)) (not (p1 c_3 c_3)) (not (p1 c_1 c_3)) (not (p3 c_2)) (not (p4 c_3)) (not (p3 c_3)) (not (p1 c_2 c_3)) )(or (= c_1 c_3) (= c_0 c_3) (= c_1 c_0) (p14 c_1 c_0 c_3) (not (p3 c_1)) (not (p1 c_0 c_0)) (not (p1 c_1 c_0)) (not (p3 c_3)) (not (p4 c_0)) (not (p3 c_0)) (not (p1 c_3 c_0)) )(or (= c_1 c_3) (= c_0 c_3) (= c_1 c_0) (p14 c_1 c_0 c_3) (not (p3 c_1)) (not (p1 c_0 c_1)) (not (p1 c_1 c_1)) (not (p3 c_3)) (not (p4 c_1)) (not (p3 c_0)) (not (p1 c_3 c_1)) )(or (= c_1 c_3) (= c_0 c_3) (= c_1 c_0) (p14 c_1 c_0 c_3) (not (p3 c_1)) (not (p1 c_0 c_2)) (not (p1 c_1 c_2)) (not (p3 c_3)) (not (p4 c_2)) (not (p3 c_0)) (not (p1 c_3 c_2)) )(or (= c_1 c_3) (= c_0 c_3) (= c_1 c_0) (p14 c_1 c_0 c_3) (not (p3 c_1)) (not (p1 c_0 c_3)) (not (p1 c_1 c_3)) (not (p3 c_3)) (not (p4 c_3)) (not (p3 c_0)) (not (p1 c_3 c_3)) )(or (= c_1 c_3) (= c_1 c_3) (= c_1 c_1) (p14 c_1 c_1 c_3) (not (p3 c_1)) (not (p1 c_1 c_0)) (not (p1 c_1 c_0)) (not (p3 c_3)) (not (p4 c_0)) (not (p3 c_1)) (not (p1 c_3 c_0)) )(or (= c_1 c_3) (= c_1 c_3) (= c_1 c_1) (p14 c_1 c_1 c_3) (not (p3 c_1)) (not (p1 c_1 c_1)) (not (p1 c_1 c_1)) (not (p3 c_3)) (not (p4 c_1)) (not (p3 c_1)) (not (p1 c_3 c_1)) )(or (= c_1 c_3) (= c_1 c_3) (= c_1 c_1) (p14 c_1 c_1 c_3) (not (p3 c_1)) (not (p1 c_1 c_2)) (not (p1 c_1 c_2)) (not (p3 c_3)) (not (p4 c_2)) (not (p3 c_1)) (not (p1 c_3 c_2)) )(or (= c_1 c_3) (= c_1 c_3) (= c_1 c_1) (p14 c_1 c_1 c_3) (not (p3 c_1)) (not (p1 c_1 c_3)) (not (p1 c_1 c_3)) (not (p3 c_3)) (not (p4 c_3)) (not (p3 c_1)) (not (p1 c_3 c_3)) )(or (= c_1 c_3) (= c_2 c_3) (= c_1 c_2) (p14 c_1 c_2 c_3) (not (p3 c_1)) (not (p1 c_2 c_0)) (not (p1 c_1 c_0)) (not (p3 c_3)) (not (p4 c_0)) (not (p3 c_2)) (not (p1 c_3 c_0)) )(or (= c_1 c_3) (= c_2 c_3) (= c_1 c_2) (p14 c_1 c_2 c_3) (not (p3 c_1)) (not (p1 c_2 c_1)) (not (p1 c_1 c_1)) (not (p3 c_3)) (not (p4 c_1)) (not (p3 c_2)) (not (p1 c_3 c_1)) )(or (= c_1 c_3) (= c_2 c_3) (= c_1 c_2) (p14 c_1 c_2 c_3) (not (p3 c_1)) (not (p1 c_2 c_2)) (not (p1 c_1 c_2)) (not (p3 c_3)) (not (p4 c_2)) (not (p3 c_2)) (not (p1 c_3 c_2)) )(or (= c_1 c_3) (= c_2 c_3) (= c_1 c_2) (p14 c_1 c_2 c_3) (not (p3 c_1)) (not (p1 c_2 c_3)) (not (p1 c_1 c_3)) (not (p3 c_3)) (not (p4 c_3)) (not (p3 c_2)) (not (p1 c_3 c_3)) )(or (= c_1 c_3) (= c_3 c_3) (= c_1 c_3) (p14 c_1 c_3 c_3) (not (p3 c_1)) (not (p1 c_3 c_0)) (not (p1 c_1 c_0)) (not (p3 c_3)) (not (p4 c_0)) (not (p3 c_3)) (not (p1 c_3 c_0)) )(or (= c_1 c_3) (= c_3 c_3) (= c_1 c_3) (p14 c_1 c_3 c_3) (not (p3 c_1)) (not (p1 c_3 c_1)) (not (p1 c_1 c_1)) (not (p3 c_3)) (not (p4 c_1)) (not (p3 c_3)) (not (p1 c_3 c_1)) )(or (= c_1 c_3) (= c_3 c_3) (= c_1 c_3) (p14 c_1 c_3 c_3) (not (p3 c_1)) (not (p1 c_3 c_2)) (not (p1 c_1 c_2)) (not (p3 c_3)) (not (p4 c_2)) (not (p3 c_3)) (not (p1 c_3 c_2)) )(or (= c_1 c_3) (= c_3 c_3) (= c_1 c_3) (p14 c_1 c_3 c_3) (not (p3 c_1)) (not (p1 c_3 c_3)) (not (p1 c_1 c_3)) (not (p3 c_3)) (not (p4 c_3)) (not (p3 c_3)) (not (p1 c_3 c_3)) )(or (= c_2 c_0) (= c_0 c_0) (= c_2 c_0) (p14 c_2 c_0 c_0) (not (p3 c_2)) (not (p1 c_0 c_0)) (not (p1 c_2 c_0)) (not (p3 c_0)) (not (p4 c_0)) (not (p3 c_0)) (not (p1 c_0 c_0)) )(or (= c_2 c_0) (= c_0 c_0) (= c_2 c_0) (p14 c_2 c_0 c_0) (not (p3 c_2)) (not (p1 c_0 c_1)) (not (p1 c_2 c_1)) (not (p3 c_0)) (not (p4 c_1)) (not (p3 c_0)) (not (p1 c_0 c_1)) )(or (= c_2 c_0) (= c_0 c_0) (= c_2 c_0) (p14 c_2 c_0 c_0) (not (p3 c_2)) (not (p1 c_0 c_2)) (not (p1 c_2 c_2)) (not (p3 c_0)) (not (p4 c_2)) (not (p3 c_0)) (not (p1 c_0 c_2)) )(or (= c_2 c_0) (= c_0 c_0) (= c_2 c_0) (p14 c_2 c_0 c_0) (not (p3 c_2)) (not (p1 c_0 c_3)) (not (p1 c_2 c_3)) (not (p3 c_0)) (not (p4 c_3)) (not (p3 c_0)) (not (p1 c_0 c_3)) )(or (= c_2 c_0) (= c_1 c_0) (= c_2 c_1) (p14 c_2 c_1 c_0) (not (p3 c_2)) (not (p1 c_1 c_0)) (not (p1 c_2 c_0)) (not (p3 c_0)) (not (p4 c_0)) (not (p3 c_1)) (not (p1 c_0 c_0)) )(or (= c_2 c_0) (= c_1 c_0) (= c_2 c_1) (p14 c_2 c_1 c_0) (not (p3 c_2)) (not (p1 c_1 c_1)) (not (p1 c_2 c_1)) (not (p3 c_0)) (not (p4 c_1)) (not (p3 c_1)) (not (p1 c_0 c_1)) )(or (= c_2 c_0) (= c_1 c_0) (= c_2 c_1) (p14 c_2 c_1 c_0) (not (p3 c_2)) (not (p1 c_1 c_2)) (not (p1 c_2 c_2)) (not (p3 c_0)) (not (p4 c_2)) (not (p3 c_1)) (not (p1 c_0 c_2)) )(or (= c_2 c_0) (= c_1 c_0) (= c_2 c_1) (p14 c_2 c_1 c_0) (not (p3 c_2)) (not (p1 c_1 c_3)) (not (p1 c_2 c_3)) (not (p3 c_0)) (not (p4 c_3)) (not (p3 c_1)) (not (p1 c_0 c_3)) )(or (= c_2 c_0) (= c_2 c_0) (= c_2 c_2) (p14 c_2 c_2 c_0) (not (p3 c_2)) (not (p1 c_2 c_0)) (not (p1 c_2 c_0)) (not (p3 c_0)) (not (p4 c_0)) (not (p3 c_2)) (not (p1 c_0 c_0)) )(or (= c_2 c_0) (= c_2 c_0) (= c_2 c_2) (p14 c_2 c_2 c_0) (not (p3 c_2)) (not (p1 c_2 c_1)) (not (p1 c_2 c_1)) (not (p3 c_0)) (not (p4 c_1)) (not (p3 c_2)) (not (p1 c_0 c_1)) )(or (= c_2 c_0) (= c_2 c_0) (= c_2 c_2) (p14 c_2 c_2 c_0) (not (p3 c_2)) (not (p1 c_2 c_2)) (not (p1 c_2 c_2)) (not (p3 c_0)) (not (p4 c_2)) (not (p3 c_2)) (not (p1 c_0 c_2)) )(or (= c_2 c_0) (= c_2 c_0) (= c_2 c_2) (p14 c_2 c_2 c_0) (not (p3 c_2)) (not (p1 c_2 c_3)) (not (p1 c_2 c_3)) (not (p3 c_0)) (not (p4 c_3)) (not (p3 c_2)) (not (p1 c_0 c_3)) )(or (= c_2 c_0) (= c_3 c_0) (= c_2 c_3) (p14 c_2 c_3 c_0) (not (p3 c_2)) (not (p1 c_3 c_0)) (not (p1 c_2 c_0)) (not (p3 c_0)) (not (p4 c_0)) (not (p3 c_3)) (not (p1 c_0 c_0)) )(or (= c_2 c_0) (= c_3 c_0) (= c_2 c_3) (p14 c_2 c_3 c_0) (not (p3 c_2)) (not (p1 c_3 c_1)) (not (p1 c_2 c_1)) (not (p3 c_0)) (not (p4 c_1)) (not (p3 c_3)) (not (p1 c_0 c_1)) )(or (= c_2 c_0) (= c_3 c_0) (= c_2 c_3) (p14 c_2 c_3 c_0) (not (p3 c_2)) (not (p1 c_3 c_2)) (not (p1 c_2 c_2)) (not (p3 c_0)) (not (p4 c_2)) (not (p3 c_3)) (not (p1 c_0 c_2)) )(or (= c_2 c_0) (= c_3 c_0) (= c_2 c_3) (p14 c_2 c_3 c_0) (not (p3 c_2)) (not (p1 c_3 c_3)) (not (p1 c_2 c_3)) (not (p3 c_0)) (not (p4 c_3)) (not (p3 c_3)) (not (p1 c_0 c_3)) )(or (= c_2 c_1) (= c_0 c_1) (= c_2 c_0) (p14 c_2 c_0 c_1) (not (p3 c_2)) (not (p1 c_0 c_0)) (not (p1 c_2 c_0)) (not (p3 c_1)) (not (p4 c_0)) (not (p3 c_0)) (not (p1 c_1 c_0)) )(or (= c_2 c_1) (= c_0 c_1) (= c_2 c_0) (p14 c_2 c_0 c_1) (not (p3 c_2)) (not (p1 c_0 c_1)) (not (p1 c_2 c_1)) (not (p3 c_1)) (not (p4 c_1)) (not (p3 c_0)) (not (p1 c_1 c_1)) )(or (= c_2 c_1) (= c_0 c_1) (= c_2 c_0) (p14 c_2 c_0 c_1) (not (p3 c_2)) (not (p1 c_0 c_2)) (not (p1 c_2 c_2)) (not (p3 c_1)) (not (p4 c_2)) (not (p3 c_0)) (not (p1 c_1 c_2)) )(or (= c_2 c_1) (= c_0 c_1) (= c_2 c_0) (p14 c_2 c_0 c_1) (not (p3 c_2)) (not (p1 c_0 c_3)) (not (p1 c_2 c_3)) (not (p3 c_1)) (not (p4 c_3)) (not (p3 c_0)) (not (p1 c_1 c_3)) )(or (= c_2 c_1) (= c_1 c_1) (= c_2 c_1) (p14 c_2 c_1 c_1) (not (p3 c_2)) (not (p1 c_1 c_0)) (not (p1 c_2 c_0)) (not (p3 c_1)) (not (p4 c_0)) (not (p3 c_1)) (not (p1 c_1 c_0)) )(or (= c_2 c_1) (= c_1 c_1) (= c_2 c_1) (p14 c_2 c_1 c_1) (not (p3 c_2)) (not (p1 c_1 c_1)) (not (p1 c_2 c_1)) (not (p3 c_1)) (not (p4 c_1)) (not (p3 c_1)) (not (p1 c_1 c_1)) )(or (= c_2 c_1) (= c_1 c_1) (= c_2 c_1) (p14 c_2 c_1 c_1) (not (p3 c_2)) (not (p1 c_1 c_2)) (not (p1 c_2 c_2)) (not (p3 c_1)) (not (p4 c_2)) (not (p3 c_1)) (not (p1 c_1 c_2)) )(or (= c_2 c_1) (= c_1 c_1) (= c_2 c_1) (p14 c_2 c_1 c_1) (not (p3 c_2)) (not (p1 c_1 c_3)) (not (p1 c_2 c_3)) (not (p3 c_1)) (not (p4 c_3)) (not (p3 c_1)) (not (p1 c_1 c_3)) )(or (= c_2 c_1) (= c_2 c_1) (= c_2 c_2) (p14 c_2 c_2 c_1) (not (p3 c_2)) (not (p1 c_2 c_0)) (not (p1 c_2 c_0)) (not (p3 c_1)) (not (p4 c_0)) (not (p3 c_2)) (not (p1 c_1 c_0)) )(or (= c_2 c_1) (= c_2 c_1) (= c_2 c_2) (p14 c_2 c_2 c_1) (not (p3 c_2)) (not (p1 c_2 c_1)) (not (p1 c_2 c_1)) (not (p3 c_1)) (not (p4 c_1)) (not (p3 c_2)) (not (p1 c_1 c_1)) )(or (= c_2 c_1) (= c_2 c_1) (= c_2 c_2) (p14 c_2 c_2 c_1) (not (p3 c_2)) (not (p1 c_2 c_2)) (not (p1 c_2 c_2)) (not (p3 c_1)) (not (p4 c_2)) (not (p3 c_2)) (not (p1 c_1 c_2)) )(or (= c_2 c_1) (= c_2 c_1) (= c_2 c_2) (p14 c_2 c_2 c_1) (not (p3 c_2)) (not (p1 c_2 c_3)) (not (p1 c_2 c_3)) (not (p3 c_1)) (not (p4 c_3)) (not (p3 c_2)) (not (p1 c_1 c_3)) )(or (= c_2 c_1) (= c_3 c_1) (= c_2 c_3) (p14 c_2 c_3 c_1) (not (p3 c_2)) (not (p1 c_3 c_0)) (not (p1 c_2 c_0)) (not (p3 c_1)) (not (p4 c_0)) (not (p3 c_3)) (not (p1 c_1 c_0)) )(or (= c_2 c_1) (= c_3 c_1) (= c_2 c_3) (p14 c_2 c_3 c_1) (not (p3 c_2)) (not (p1 c_3 c_1)) (not (p1 c_2 c_1)) (not (p3 c_1)) (not (p4 c_1)) (not (p3 c_3)) (not (p1 c_1 c_1)) )(or (= c_2 c_1) (= c_3 c_1) (= c_2 c_3) (p14 c_2 c_3 c_1) (not (p3 c_2)) (not (p1 c_3 c_2)) (not (p1 c_2 c_2)) (not (p3 c_1)) (not (p4 c_2)) (not (p3 c_3)) (not (p1 c_1 c_2)) )(or (= c_2 c_1) (= c_3 c_1) (= c_2 c_3) (p14 c_2 c_3 c_1) (not (p3 c_2)) (not (p1 c_3 c_3)) (not (p1 c_2 c_3)) (not (p3 c_1)) (not (p4 c_3)) (not (p3 c_3)) (not (p1 c_1 c_3)) )(or (= c_2 c_2) (= c_0 c_2) (= c_2 c_0) (p14 c_2 c_0 c_2) (not (p3 c_2)) (not (p1 c_0 c_0)) (not (p1 c_2 c_0)) (not (p3 c_2)) (not (p4 c_0)) (not (p3 c_0)) (not (p1 c_2 c_0)) )(or (= c_2 c_2) (= c_0 c_2) (= c_2 c_0) (p14 c_2 c_0 c_2) (not (p3 c_2)) (not (p1 c_0 c_1)) (not (p1 c_2 c_1)) (not (p3 c_2)) (not (p4 c_1)) (not (p3 c_0)) (not (p1 c_2 c_1)) )(or (= c_2 c_2) (= c_0 c_2) (= c_2 c_0) (p14 c_2 c_0 c_2) (not (p3 c_2)) (not (p1 c_0 c_2)) (not (p1 c_2 c_2)) (not (p3 c_2)) (not (p4 c_2)) (not (p3 c_0)) (not (p1 c_2 c_2)) )(or (= c_2 c_2) (= c_0 c_2) (= c_2 c_0) (p14 c_2 c_0 c_2) (not (p3 c_2)) (not (p1 c_0 c_3)) (not (p1 c_2 c_3)) (not (p3 c_2)) (not (p4 c_3)) (not (p3 c_0)) (not (p1 c_2 c_3)) )(or (= c_2 c_2) (= c_1 c_2) (= c_2 c_1) (p14 c_2 c_1 c_2) (not (p3 c_2)) (not (p1 c_1 c_0)) (not (p1 c_2 c_0)) (not (p3 c_2)) (not (p4 c_0)) (not (p3 c_1)) (not (p1 c_2 c_0)) )(or (= c_2 c_2) (= c_1 c_2) (= c_2 c_1) (p14 c_2 c_1 c_2) (not (p3 c_2)) (not (p1 c_1 c_1)) (not (p1 c_2 c_1)) (not (p3 c_2)) (not (p4 c_1)) (not (p3 c_1)) (not (p1 c_2 c_1)) )(or (= c_2 c_2) (= c_1 c_2) (= c_2 c_1) (p14 c_2 c_1 c_2) (not (p3 c_2)) (not (p1 c_1 c_2)) (not (p1 c_2 c_2)) (not (p3 c_2)) (not (p4 c_2)) (not (p3 c_1)) (not (p1 c_2 c_2)) )(or (= c_2 c_2) (= c_1 c_2) (= c_2 c_1) (p14 c_2 c_1 c_2) (not (p3 c_2)) (not (p1 c_1 c_3)) (not (p1 c_2 c_3)) (not (p3 c_2)) (not (p4 c_3)) (not (p3 c_1)) (not (p1 c_2 c_3)) )(or (= c_2 c_2) (= c_2 c_2) (= c_2 c_2) (p14 c_2 c_2 c_2) (not (p3 c_2)) (not (p1 c_2 c_0)) (not (p1 c_2 c_0)) (not (p3 c_2)) (not (p4 c_0)) (not (p3 c_2)) (not (p1 c_2 c_0)) )(or (= c_2 c_2) (= c_2 c_2) (= c_2 c_2) (p14 c_2 c_2 c_2) (not (p3 c_2)) (not (p1 c_2 c_1)) (not (p1 c_2 c_1)) (not (p3 c_2)) (not (p4 c_1)) (not (p3 c_2)) (not (p1 c_2 c_1)) )(or (= c_2 c_2) (= c_2 c_2) (= c_2 c_2) (p14 c_2 c_2 c_2) (not (p3 c_2)) (not (p1 c_2 c_2)) (not (p1 c_2 c_2)) (not (p3 c_2)) (not (p4 c_2)) (not (p3 c_2)) (not (p1 c_2 c_2)) )(or (= c_2 c_2) (= c_2 c_2) (= c_2 c_2) (p14 c_2 c_2 c_2) (not (p3 c_2)) (not (p1 c_2 c_3)) (not (p1 c_2 c_3)) (not (p3 c_2)) (not (p4 c_3)) (not (p3 c_2)) (not (p1 c_2 c_3)) )(or (= c_2 c_2) (= c_3 c_2) (= c_2 c_3) (p14 c_2 c_3 c_2) (not (p3 c_2)) (not (p1 c_3 c_0)) (not (p1 c_2 c_0)) (not (p3 c_2)) (not (p4 c_0)) (not (p3 c_3)) (not (p1 c_2 c_0)) )(or (= c_2 c_2) (= c_3 c_2) (= c_2 c_3) (p14 c_2 c_3 c_2) (not (p3 c_2)) (not (p1 c_3 c_1)) (not (p1 c_2 c_1)) (not (p3 c_2)) (not (p4 c_1)) (not (p3 c_3)) (not (p1 c_2 c_1)) )(or (= c_2 c_2) (= c_3 c_2) (= c_2 c_3) (p14 c_2 c_3 c_2) (not (p3 c_2)) (not (p1 c_3 c_2)) (not (p1 c_2 c_2)) (not (p3 c_2)) (not (p4 c_2)) (not (p3 c_3)) (not (p1 c_2 c_2)) )(or (= c_2 c_2) (= c_3 c_2) (= c_2 c_3) (p14 c_2 c_3 c_2) (not (p3 c_2)) (not (p1 c_3 c_3)) (not (p1 c_2 c_3)) (not (p3 c_2)) (not (p4 c_3)) (not (p3 c_3)) (not (p1 c_2 c_3)) )(or (= c_2 c_3) (= c_0 c_3) (= c_2 c_0) (p14 c_2 c_0 c_3) (not (p3 c_2)) (not (p1 c_0 c_0)) (not (p1 c_2 c_0)) (not (p3 c_3)) (not (p4 c_0)) (not (p3 c_0)) (not (p1 c_3 c_0)) )(or (= c_2 c_3) (= c_0 c_3) (= c_2 c_0) (p14 c_2 c_0 c_3) (not (p3 c_2)) (not (p1 c_0 c_1)) (not (p1 c_2 c_1)) (not (p3 c_3)) (not (p4 c_1)) (not (p3 c_0)) (not (p1 c_3 c_1)) )(or (= c_2 c_3) (= c_0 c_3) (= c_2 c_0) (p14 c_2 c_0 c_3) (not (p3 c_2)) (not (p1 c_0 c_2)) (not (p1 c_2 c_2)) (not (p3 c_3)) (not (p4 c_2)) (not (p3 c_0)) (not (p1 c_3 c_2)) )(or (= c_2 c_3) (= c_0 c_3) (= c_2 c_0) (p14 c_2 c_0 c_3) (not (p3 c_2)) (not (p1 c_0 c_3)) (not (p1 c_2 c_3)) (not (p3 c_3)) (not (p4 c_3)) (not (p3 c_0)) (not (p1 c_3 c_3)) )(or (= c_2 c_3) (= c_1 c_3) (= c_2 c_1) (p14 c_2 c_1 c_3) (not (p3 c_2)) (not (p1 c_1 c_0)) (not (p1 c_2 c_0)) (not (p3 c_3)) (not (p4 c_0)) (not (p3 c_1)) (not (p1 c_3 c_0)) )(or (= c_2 c_3) (= c_1 c_3) (= c_2 c_1) (p14 c_2 c_1 c_3) (not (p3 c_2)) (not (p1 c_1 c_1)) (not (p1 c_2 c_1)) (not (p3 c_3)) (not (p4 c_1)) (not (p3 c_1)) (not