(benchmark SEQ020_size3.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 unknown
: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))
:formula 
( and 
( distinct c_0 c_1 c_2 )(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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_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 (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 (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 (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_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_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 (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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_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 (= 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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_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 (not (p9 c_0)) (not (p10 c_0 c_0)) (not (p3 c_0)) (p3 (f16 c_0 c_0 c_0)) (= c_0 c_0) (not (p9 c_0)) (not (p10 c_0 c_0)) )(or (not (p9 c_0)) (not (p10 c_0 c_1)) (not (p3 c_0)) (p3 (f16 c_0 c_1 c_0)) (= c_0 c_1) (not (p9 c_1)) (not (p10 c_0 c_0)) )(or (not (p9 c_0)) (not (p10 c_0 c_2)) (not (p3 c_0)) (p3 (f16 c_0 c_2 c_0)) (= c_0 c_2) (not (p9 c_2)) (not (p10 c_0 c_0)) )(or (not (p9 c_0)) (not (p10 c_1 c_0)) (not (p3 c_1)) (p3 (f16 c_0 c_0 c_1)) (= c_0 c_0) (not (p9 c_0)) (not (p10 c_1 c_0)) )(or (not (p9 c_0)) (not (p10 c_1 c_1)) (not (p3 c_1)) (p3 (f16 c_0 c_1 c_1)) (= c_0 c_1) (not (p9 c_1)) (not (p10 c_1 c_0)) )(or (not (p9 c_0)) (not (p10 c_1 c_2)) (not (p3 c_1)) (p3 (f16 c_0 c_2 c_1)) (= c_0 c_2) (not (p9 c_2)) (not (p10 c_1 c_0)) )(or (not (p9 c_0)) (not (p10 c_2 c_0)) (not (p3 c_2)) (p3 (f16 c_0 c_0 c_2)) (= c_0 c_0) (not (p9 c_0)) (not (p10 c_2 c_0)) )(or (not (p9 c_0)) (not (p10 c_2 c_1)) (not (p3 c_2)) (p3 (f16 c_0 c_1 c_2)) (= c_0 c_1) (not (p9 c_1)) (not (p10 c_2 c_0)) )(or (not (p9 c_0)) (not (p10 c_2 c_2)) (not (p3 c_2)) (p3 (f16 c_0 c_2 c_2)) (= c_0 c_2) (not (p9 c_2)) (not (p10 c_2 c_0)) )(or (not (p9 c_1)) (not (p10 c_0 c_0)) (not (p3 c_0)) (p3 (f16 c_1 c_0 c_0)) (= c_1 c_0) (not (p9 c_0)) (not (p10 c_0 c_1)) )(or (not (p9 c_1)) (not (p10 c_0 c_1)) (not (p3 c_0)) (p3 (f16 c_1 c_1 c_0)) (= c_1 c_1) (not (p9 c_1)) (not (p10 c_0 c_1)) )(or (not (p9 c_1)) (not (p10 c_0 c_2)) (not (p3 c_0)) (p3 (f16 c_1 c_2 c_0)) (= c_1 c_2) (not (p9 c_2)) (not (p10 c_0 c_1)) )(or (not (p9 c_1)) (not (p10 c_1 c_0)) (not (p3 c_1)) (p3 (f16 c_1 c_0 c_1)) (= c_1 c_0) (not (p9 c_0)) (not (p10 c_1 c_1)) )(or (not (p9 c_1)) (not (p10 c_1 c_1)) (not (p3 c_1)) (p3 (f16 c_1 c_1 c_1)) (= c_1 c_1) (not (p9 c_1)) (not (p10 c_1 c_1)) )(or (not (p9 c_1)) (not (p10 c_1 c_2)) (not (p3 c_1)) (p3 (f16 c_1 c_2 c_1)) (= c_1 c_2) (not (p9 c_2)) (not (p10 c_1 c_1)) )(or (not (p9 c_1)) (not (p10 c_2 c_0)) (not (p3 c_2)) (p3 (f16 c_1 c_0 c_2)) (= c_1 c_0) (not (p9 c_0)) (not (p10 c_2 c_1)) )(or (not (p9 c_1)) (not (p10 c_2 c_1)) (not (p3 c_2)) (p3 (f16 c_1 c_1 c_2)) (= c_1 c_1) (not (p9 c_1)) (not (p10 c_2 c_1)) )(or (not (p9 c_1)) (not (p10 c_2 c_2)) (not (p3 c_2)) (p3 (f16 c_1 c_2 c_2)) (= c_1 c_2) (not (p9 c_2)) (not (p10 c_2 c_1)) )(or (not (p9 c_2)) (not (p10 c_0 c_0)) (not (p3 c_0)) (p3 (f16 c_2 c_0 c_0)) (= c_2 c_0) (not (p9 c_0)) (not (p10 c_0 c_2)) )(or (not (p9 c_2)) (not (p10 c_0 c_1)) (not (p3 c_0)) (p3 (f16 c_2 c_1 c_0)) (= c_2 c_1) (not (p9 c_1)) (not (p10 c_0 c_2)) )(or (not (p9 c_2)) (not (p10 c_0 c_2)) (not (p3 c_0)) (p3 (f16 c_2 c_2 c_0)) (= c_2 c_2) (not (p9 c_2)) (not (p10 c_0 c_2)) )(or (not (p9 c_2)) (not (p10 c_1 c_0)) (not (p3 c_1)) (p3 (f16 c_2 c_0 c_1)) (= c_2 c_0) (not (p9 c_0)) (not (p10 c_1 c_2)) )(or (not (p9 c_2)) (not (p10 c_1 c_1)) (not (p3 c_1)) (p3 (f16 c_2 c_1 c_1)) (= c_2 c_1) (not (p9 c_1)) (not (p10 c_1 c_2)) )(or (not (p9 c_2)) (not (p10 c_1 c_2)) (not (p3 c_1)) (p3 (f16 c_2 c_2 c_1)) (= c_2 c_2) (not (p9 c_2)) (not (p10 c_1 c_2)) )(or (not (p9 c_2)) (not (p10 c_2 c_0)) (not (p3 c_2)) (p3 (f16 c_2 c_0 c_2)) (= c_2 c_0) (not (p9 c_0)) (not (p10 c_2 c_2)) )(or (not (p9 c_2)) (not (p10 c_2 c_1)) (not (p3 c_2)) (p3 (f16 c_2 c_1 c_2)) (= c_2 c_1) (not (p9 c_1)) (not (p10 c_2 c_2)) )(or (not (p9 c_2)) (not (p10 c_2 c_2)) (not (p3 c_2)) (p3 (f16 c_2 c_2 c_2)) (= c_2 c_2) (not (p9 c_2)) (not (p10 c_2 c_2)) )(or (not (p4 c_0)) (not (p1 (f7 c_0) c_0)) )(or (not (p4 c_1)) (not (p1 (f7 c_1) c_1)) )(or (not (p4 c_2)) (not (p1 (f7 c_2) c_2)) )(or (not (p3 c_0)) (= c_0 c_0) (p10 c_0 (f13 c_0 c_0 c_0)) (not (p3 c_0)) (p14 c_0 c_0 c_0) (= c_0 c_0) (not (p3 c_0)) (= c_0 c_0) )(or (not (p3 c_0)) (= c_0 c_0) (p10 c_1 (f13 c_1 c_0 c_0)) (not (p3 c_1)) (p14 c_1 c_0 c_0) (= c_1 c_0) (not (p3 c_0)) (= c_1 c_0) )(or (not (p3 c_0)) (= c_0 c_0) (p10 c_2 (f13 c_2 c_0 c_0)) (not (p3 c_2)) (p14 c_2 c_0 c_0) (= c_2 c_0) (not (p3 c_0)) (= c_2 c_0) )(or (not (p3 c_0)) (= c_1 c_0) (p10 c_0 (f13 c_0 c_1 c_0)) (not (p3 c_0)) (p14 c_0 c_1 c_0) (= c_0 c_1) (not (p3 c_1)) (= c_0 c_0) )(or (not (p3 c_0)) (= c_1 c_0) (p10 c_1 (f13 c_1 c_1 c_0)) (not (p3 c_1)) (p14 c_1 c_1 c_0) (= c_1 c_1) (not (p3 c_1)) (= c_1 c_0) )(or (not (p3 c_0)) (= c_1 c_0) (p10 c_2 (f13 c_2 c_1 c_0)) (not (p3 c_2)) (p14 c_2 c_1 c_0) (= c_2 c_1) (not (p3 c_1)) (= c_2 c_0) )(or (not (p3 c_0)) (= c_2 c_0) (p10 c_0 (f13 c_0 c_2 c_0)) (not (p3 c_0)) (p14 c_0 c_2 c_0) (= c_0 c_2) (not (p3 c_2)) (= c_0 c_0) )(or (not (p3 c_0)) (= c_2 c_0) (p10 c_1 (f13 c_1 c_2 c_0)) (not (p3 c_1)) (p14 c_1 c_2 c_0) (= c_1 c_2) (not (p3 c_2)) (= c_1 c_0) )(or (not (p3 c_0)) (= c_2 c_0) (p10 c_2 (f13 c_2 c_2 c_0)) (not (p3 c_2)) (p14 c_2 c_2 c_0) (= c_2 c_2) (not (p3 c_2)) (= c_2 c_0) )(or (not (p3 c_1)) (= c_0 c_1) (p10 c_0 (f13 c_0 c_0 c_1)) (not (p3 c_0)) (p14 c_0 c_0 c_1) (= c_0 c_0) (not (p3 c_0)) (= c_0 c_1) )(or (not (p3 c_1)) (= c_0 c_1) (p10 c_1 (f13 c_1 c_0 c_1)) (not (p3 c_1)) (p14 c_1 c_0 c_1) (= c_1 c_0) (not (p3 c_0)) (= c_1 c_1) )(or (not (p3 c_1)) (= c_0 c_1) (p10 c_2 (f13 c_2 c_0 c_1)) (not (p3 c_2)) (p14 c_2 c_0 c_1) (= c_2 c_0) (not (p3 c_0)) (= c_2 c_1) )(or (not (p3 c_1)) (= c_1 c_1) (p10 c_0 (f13 c_0 c_1 c_1)) (not (p3 c_0)) (p14 c_0 c_1 c_1) (= c_0 c_1) (not (p3 c_1)) (= c_0 c_1) )(or (not (p3 c_1)) (= c_1 c_1) (p10 c_1 (f13 c_1 c_1 c_1)) (not (p3 c_1)) (p14 c_1 c_1 c_1) (= c_1 c_1) (not (p3 c_1)) (= c_1 c_1) )(or (not (p3 c_1)) (= c_1 c_1) (p10 c_2 (f13 c_2 c_1 c_1)) (not (p3 c_2)) (p14 c_2 c_1 c_1) (= c_2 c_1) (not (p3 c_1)) (= c_2 c_1) )(or (not (p3 c_1)) (= c_2 c_1) (p10 c_0 (f13 c_0 c_2 c_1)) (not (p3 c_0)) (p14 c_0 c_2 c_1) (= c_0 c_2) (not (p3 c_2)) (= c_0 c_1) )(or (not (p3 c_1)) (= c_2 c_1) (p10 c_1 (f13 c_1 c_2 c_1)) (not (p3 c_1)) (p14 c_1 c_2 c_1) (= c_1 c_2) (not (p3 c_2)) (= c_1 c_1) )(or (not (p3 c_1)) (= c_2 c_1) (p10 c_2 (f13 c_2 c_2 c_1)) (not (p3 c_2)) (p14 c_2 c_2 c_1) (= c_2 c_2) (not (p3 c_2)) (= c_2 c_1) )(or (not (p3 c_2)) (= c_0 c_2) (p10 c_0 (f13 c_0 c_0 c_2)) (not (p3 c_0)) (p14 c_0 c_0 c_2) (= c_0 c_0) (not (p3 c_0)) (= c_0 c_2) )(or (not (p3 c_2)) (= c_0 c_2) (p10 c_1 (f13 c_1 c_0 c_2)) (not (p3 c_1)) (p14 c_1 c_0 c_2) (= c_1 c_0) (not (p3 c_0)) (= c_1 c_2) )(or (not (p3 c_2)) (= c_0 c_2) (p10 c_2 (f13 c_2 c_0 c_2)) (not (p3 c_2)) (p14 c_2 c_0 c_2) (= c_2 c_0) (not (p3 c_0)) (= c_2 c_2) )(or (not (p3 c_2)) (= c_1 c_2) (p10 c_0 (f13 c_0 c_1 c_2)) (not (p3 c_0)) (p14 c_0 c_1 c_2) (= c_0 c_1) (not (p3 c_1)) (= c_0 c_2) )(or (not (p3 c_2)) (= c_1 c_2) (p10 c_1 (f13 c_1 c_1 c_2)) (not (p3 c_1)) (p14 c_1 c_1 c_2) (= c_1 c_1) (not (p3 c_1)) (= c_1 c_2) )(or (not (p3 c_2)) (= c_1 c_2) (p10 c_2 (f13 c_2 c_1 c_2)) (not (p3 c_2)) (p14 c_2 c_1 c_2) (= c_2 c_1) (not (p3 c_1)) (= c_2 c_2) )(or (not (p3 c_2)) (= c_2 c_2) (p10 c_0 (f13 c_0 c_2 c_2)) (not (p3 c_0)) (p14 c_0 c_2 c_2) (= c_0 c_2) (not (p3 c_2)) (= c_0 c_2) )(or (not (p3 c_2)) (= c_2 c_2) (p10 c_1 (f13 c_1 c_2 c_2)) (not (p3 c_1)) (p14 c_1 c_2 c_2) (= c_1 c_2) (not (p3 c_2)) (= c_1 c_2) )(or (not (p3 c_2)) (= c_2 c_2) (p10 c_2 (f13 c_2 c_2 c_2)) (not (p3 c_2)) (p14 c_2 c_2 c_2) (= c_2 c_2) (not (p3 c_2)) (= c_2 c_2) )(p9 c18) (or (= c_0 c_0) (not (p3 c_0)) (= c_0 c_0) (= c_0 c_0) (p14 c_0 c_0 c_0) (not (p3 c_0)) (p10 c_0 (f13 c_0 c_0 c_0)) (not (p3 c_0)) )(or (= c_0 c_0) (not (p3 c_1)) (= c_1 c_0) (= c_1 c_0) (p14 c_1 c_0 c_0) (not (p3 c_0)) (p10 c_0 (f13 c_1 c_0 c_0)) (not (p3 c_0)) )(or (= c_0 c_0) (not (p3 c_2)) (= c_2 c_0) (= c_2 c_0) (p14 c_2 c_0 c_0) (not (p3 c_0)) (p10 c_0 (f13 c_2 c_0 c_0)) (not (p3 c_0)) )(or (= c_0 c_1) (not (p3 c_0)) (= c_0 c_0) (= c_0 c_1) (p14 c_0 c_0 c_1) (not (p3 c_0)) (p10 c_1 (f13 c_0 c_0 c_1)) (not (p3 c_1)) )(or (= c_0 c_1) (not (p3 c_1)) (= c_1 c_0) (= c_1 c_1) (p14 c_1 c_0 c_1) (not (p3 c_0)) (p10 c_1 (f13 c_1 c_0 c_1)) (not (p3 c_1)) )(or (= c_0 c_1) (not (p3 c_2)) (= c_2 c_0) (= c_2 c_1) (p14 c_2 c_0 c_1) (not (p3 c_0)) (p10 c_1 (f13 c_2 c_0 c_1)) (not (p3 c_1)) )(or (= c_0 c_2) (not (p3 c_0)) (= c_0 c_0) (= c_0 c_2) (p14 c_0 c_0 c_2) (not (p3 c_0)) (p10 c_2 (f13 c_0 c_0 c_2)) (not (p3 c_2)) )(or (= c_0 c_2) (not (p3 c_1)) (= c_1 c_0) (= c_1 c_2) (p14 c_1 c_0 c_2) (not (p3 c_0)) (p10 c_2 (f13 c_1 c_0 c_2)) (not (p3 c_2)) )(or (= c_0 c_2) (not (p3 c_2)) (= c_2 c_0) (= c_2 c_2) (p14 c_2 c_0 c_2) (not (p3 c_0)) (p10 c_2 (f13 c_2 c_0 c_2)) (not (p3 c_2)) )(or (= c_1 c_0) (not (p3 c_0)) (= c_0 c_1) (= c_0 c_0) (p14 c_0 c_1 c_0) (not (p3 c_1)) (p10 c_0 (f13 c_0 c_1 c_0)) (not (p3 c_0)) )(or (= c_1 c_0) (not (p3 c_1)) (= c_1 c_1) (= c_1 c_0) (p14 c_1 c_1 c_0) (not (p3 c_1)) (p10 c_0 (f13 c_1 c_1 c_0)) (not (p3 c_0)) )(or (= c_1 c_0) (not (p3 c_2)) (= c_2 c_1) (= c_2 c_0) (p14 c_2 c_1 c_0) (not (p3 c_1)) (p10 c_0 (f13 c_2 c_1 c_0)) (not (p3 c_0)) )(or (= c_1 c_1) (not (p3 c_0)) (= c_0 c_1) (= c_0 c_1) (p14 c_0 c_1 c_1) (not (p3 c_1)) (p10 c_1 (f13 c_0 c_1 c_1)) (not (p3 c_1)) )(or (= c_1 c_1) (not (p3 c_1)) (= c_1 c_1) (= c_1 c_1) (p14 c_1 c_1 c_1) (not (p3 c_1)) (p10 c_1 (f13 c_1 c_1 c_1)) (not (p3 c_1)) )(or (= c_1 c_1) (not (p3 c_2)) (= c_2 c_1) (= c_2 c_1) (p14 c_2 c_1 c_1) (not (p3 c_1)) (p10 c_1 (f13 c_2 c_1 c_1)) (not (p3 c_1)) )(or (= c_1 c_2) (not (p3 c_0)) (= c_0 c_1) (= c_0 c_2) (p14 c_0 c_1 c_2) (not (p3 c_1)) (p10 c_2 (f13 c_0 c_1 c_2)) (not (p3 c_2)) )(or (= c_1 c_2) (not (p3 c_1)) (= c_1 c_1) (= c_1 c_2) (p14 c_1 c_1 c_2) (not (p3 c_1)) (p10 c_2 (f13 c_1 c_1 c_2)) (not (p3 c_2)) )(or (= c_1 c_2) (not (p3 c_2)) (= c_2 c_1) (= c_2 c_2) (p14 c_2 c_1 c_2) (not (p3 c_1)) (p10 c_2 (f13 c_2 c_1 c_2)) (not (p3 c_2)) )(or (= c_2 c_0) (not (p3 c_0)) (= c_0 c_2) (= c_0 c_0) (p14 c_0 c_2 c_0) (not (p3 c_2)) (p10 c_0 (f13 c_0 c_2 c_0)) (not (p3 c_0)) )(or (= c_2 c_0) (not (p3 c_1)) (= c_1 c_2) (= c_1 c_0) (p14 c_1 c_2 c_0) (not (p3 c_2)) (p10 c_0 (f13 c_1 c_2 c_0)) (not (p3 c_0)) )(or (= c_2 c_0) (not (p3 c_2)) (= c_2 c_2) (= c_2 c_0) (p14 c_2 c_2 c_0) (not (p3 c_2)) (p10 c_0 (f13 c_2 c_2 c_0)) (not (p3 c_0)) )(or (= c_2 c_1) (not (p3 c_0)) (= c_0 c_2) (= c_0 c_1) (p14 c_0 c_2 c_1) (not (p3 c_2)) (p10 c_1 (f13 c_0 c_2 c_1)) (not (p3 c_1)) )(or (= c_2 c_1) (not (p3 c_1)) (= c_1 c_2) (= c_1 c_1) (p14 c_1 c_2 c_1) (not (p3 c_2)) (p10 c_1 (f13 c_1 c_2 c_1)) (not (p3 c_1)) )(or (= c_2 c_1) (not (p3 c_2)) (= c_2 c_2) (= c_2 c_1) (p14 c_2 c_2 c_1) (not (p3 c_2)) (p10 c_1 (f13 c_2 c_2 c_1)) (not (p3 c_1)) )(or (= c_2 c_2) (not (p3 c_0)) (= c_0 c_2) (= c_0 c_2) (p14 c_0 c_2 c_2) (not (p3 c_2)) (p10 c_2 (f13 c_0 c_2 c_2)) (not (p3 c_2)) )(or (= c_2 c_2) (not (p3 c_1)) (= c_1 c_2) (= c_1 c_2) (p14 c_1 c_2 c_2) (not (p3 c_2)) (p10 c_2 (f13 c_1 c_2 c_2)) (not (p3 c_2)) )(or (= c_2 c_2) (not (p3 c_2)) (= c_2 c_2) (= c_2 c_2) (p14 c_2 c_2 c_2) (not (p3 c_2)) (p10 c_2 (f13 c_2 c_2 c_2)) (not (p3 c_2)) )(or (not (p3 c_0)) (= c_0 c_0) (not (p3 c_0)) (not (p10 c_0 c18)) (p14 c_0 c_0 c_0) (not (p3 c_0)) (not (p10 c_0 c18)) (not (p10 c_0 c18)) (= c_0 c_0) (= c_0 c_0) )(or (not (p3 c_0)) (= c_0 c_0) (not (p3 c_1)) (not (p10 c_1 c18)) (p14 c_0 c_0 c_1) (not (p3 c_0)) (not (p10 c_0 c18)) (not (p10 c_0 c18)) (= c_0 c_1) (= c_0 c_1) )(or (not (p3 c_0)) (= c_0 c_0) (not (p3 c_2)) (not (p10 c_2 c18)) (p14 c_0 c_0 c_2) (not (p3 c_0)) (not (p10 c_0 c18)) (not (p10 c_0 c18)) (= c_0 c_2) (= c_0 c_2) )(or (not (p3 c_0)) (= c_1 c_0) (not (p3 c_0)) (not (p10 c_0 c18)) (p14 c_1 c_0 c_0) (not (p3 c_1)) (not (p10 c_0 c18)) (not (p10 c_1 c18)) (= c_1 c_0) (= c_0 c_0) )(or (not (p3 c_0)) (= c_1 c_0) (not (p3 c_1)) (not (p10 c_1 c18)) (p14 c_1 c_0 c_1) (not (p3 c_1)) (not (p10 c_0 c18)) (not (p10 c_1 c18)) (= c_1 c_1) (= c_0 c_1) )(or (not (p3 c_0)) (= c_1 c_0) (not (p3 c_2)) (not (p10 c_2 c18)) (p14 c_1 c_0 c_2) (not (p3 c_1)) (not (p10 c_0 c18)) (not (p10 c_1 c18)) (= c_1 c_2) (= c_0 c_2) )(or (not (p3 c_0)) (= c_2 c_0) (not (p3 c_0)) (not (p10 c_0 c18)) (p14 c_2 c_0 c_0) (not (p3 c_2)) (not (p10 c_0 c18)) (not (p10 c_2 c18)) (= c_2 c_0) (= c_0 c_0) )(or (not (p3 c_0)) (= c_2 c_0) (not (p3 c_1)) (not (p10 c_1 c18)) (p14 c_2 c_0 c_1) (not (p3 c_2)) (not (p10 c_0 c18)) (not (p10 c_2 c18)) (= c_2 c_1) (= c_0 c_1) )(or (not (p3 c_0)) (= c_2 c_0) (not (p3 c_2)) (not (p10 c_2 c18)) (p14 c_2 c_0 c_2) (not (p3 c_2)) (not (p10 c_0 c18)) (not (p10 c_2 c18)) (= c_2 c_2) (= c_0 c_2) )(or (not (p3 c_1)) (= c_0 c_1) (not (p3 c_0)) (not (p10 c_0 c18)) (p14 c_0 c_1 c_0) (not (p3 c_0)) (not (p10 c_1 c18)) (not (p10 c_0 c18)) (= c_0 c_0) (= c_1 c_0) )(or (not (p3 c_1)) (= c_0 c_1) (not (p3 c_1)) (not (p10 c_1 c18)) (p14 c_0 c_1 c_1) (not (p3 c_0)) (not (p10 c_1 c18)) (not (p10 c_0 c18)) (= c_0 c_1) (= c_1 c_1) )(or (not (p3 c_1)) (= c_0 c_1) (not (p3 c_2)) (not (p10 c_2 c18)) (p14 c_0 c_1 c_2) (not (p3 c_0)) (not (p10 c_1 c18)) (not (p10 c_0 c18)) (= c_0 c_2) (= c_1 c_2) )(or (not (p3 c_1)) (= c_1 c_1) (not (p3 c_0)) (not (p10 c_0 c18)) (p14 c_1 c_1 c_0) (not (p3 c_1)) (not (p10 c_1 c18)) (not (p10 c_1 c18)) (= c_1 c_0) (= c_1 c_0) )(or (not (p3 c_1)) (= c_1 c_1) (not (p3 c_1)) (not (p10 c_1 c18)) (p14 c_1 c_1 c_1) (not (p3 c_1)) (not (p10 c_1 c18)) (not (p10 c_1 c18)) (= c_1 c_1) (= c_1 c_1) )(or (not (p3 c_1)) (= c_1 c_1) (not (p3 c_2)) (not (p10 c_2 c18)) (p14 c_1 c_1 c_2) (not (p3 c_1)) (not (p10 c_1 c18)) (not (p10 c_1 c18)) (= c_1 c_2) (= c_1 c_2) )(or (not (p3 c_1)) (= c_2 c_1) (not (p3 c_0)) (not (p10 c_0 c18)) (p14 c_2 c_1 c_0) (not (p3 c_2)) (not (p10 c_1 c18)) (not (p10 c_2 c18)) (= c_2 c_0) (= c_1 c_0) )(or (not (p3 c_1)) (= c_2 c_1) (not (p3 c_1)) (not (p10 c_1 c18)) (p14 c_2 c_1 c_1) (not (p3 c_2)) (not (p10 c_1 c18)) (not (p10 c_2 c18)) (= c_2 c_1) (= c_1 c_1) )(or (not (p3 c_1)) (= c_2 c_1) (not (p3 c_2)) (not (p10 c_2 c18)) (p14 c_2 c_1 c_2) (not (p3 c_2)) (not (p10 c_1 c18)) (not (p10 c_2 c18)) (= c_2 c_2) (= c_1 c_2) )(or (not (p3 c_2)) (= c_0 c_2) (not (p3 c_0)) (not (p10 c_0 c18)) (p14 c_0 c_2 c_0) (not (p3 c_0)) (not (p10 c_2 c18)) (not (p10 c_0 c18)) (= c_0 c_0) (= c_2 c_0) )(or (not (p3 c_2)) (= c_0 c_2) (not (p3 c_1)) (not (p10 c_1 c18)) (p14 c_0 c_2 c_1) (not (p3 c_0)) (not (p10 c_2 c18)) (not (p10 c_0 c18)) (= c_0 c_1) (= c_2 c_1) )(or (not (p3 c_2)) (= c_0 c_2) (not (p3 c_2)) (not (p10 c_2 c18)) (p14 c_0 c_2 c_2) (not (p3 c_0)) (not (p10 c_2 c18)) (not (p10 c_0 c18)) (= c_0 c_2) (= c_2 c_2) )(or (not (p3 c_2)) (= c_1 c_2) (not (p3 c_0)) (not (p10 c_0 c18)) (p14 c_1 c_2 c_0) (not (p3 c_1)) (not (p10 c_2 c18)) (not (p10 c_1 c18)) (= c_1 c_0) (= c_2 c_0) )(or (not (p3 c_2)) (= c_1 c_2) (not (p3 c_1)) (not (p10 c_1 c18)) (p14 c_1 c_2 c_1) (not (p3 c_1)) (not (p10 c_2 c18)) (not (p10 c_1 c18)) (= c_1 c_1) (= c_2 c_1) )(or (not (p3 c_2)) (= c_1 c_2) (not (p3 c_2)) (not (p10 c_2 c18)) (p14 c_1 c_2 c_2) (not (p3 c_1)) (not (p10 c_2 c18)) (not (p10 c_1 c18)) (= c_1 c_2) (= c_2 c_2) )(or (not (p3 c_2)) (= c_2 c_2) (not (p3 c_0)) (not (p10 c_0 c18)) (p14 c_2 c_2 c_0) (not (p3 c_2)) (not (p10 c_2 c18)) (not (p10 c_2 c18)) (= c_2 c_0) (= c_2 c_0) )(or (not (p3 c_2)) (= c_2 c_2) (not (p3 c_1)) (not (p10 c_1 c18)) (p14 c_2 c_2 c_1) (not (p3 c_2)) (not (p10 c_2 c18)) (not (p10 c_2 c18)) (= c_2 c_1) (= c_2 c_1) )(or (not (p3 c_2)) (= c_2 c_2) (not (p3 c_2)) (not (p10 c_2 c18)) (p14 c_2 c_2 c_2) (not (p3 c_2)) (not (p10 c_2 c18)) (not (p10 c_2 c18)) (= c_2 c_2) (= c_2 c_2) )(or (not (p9 c_0)) (p10 (f11 c_0) c_0) )(or (not (p9 c_1)) (p10 (f11 c_1) c_1) )(or (not (p9 c_2)) (p10 (f11 c_2) c_2) )(or (not (p4 c_0)) (p1 (f5 c_0) c_0) )(or (not (p4 c_1)) (p1 (f5 c_1) c_1) )(or (not (p4 c_2)) (p1 (f5 c_2) c_2) )(or (not (p10 c_0 c_0)) (not (p3 c_0)) (p10 (f16 c_0 c_0 c_0) c_0) (= c_0 c_0) (not (p10 c_0 c_0)) (not (p9 c_0)) (not (p9 c_0)) )(or (not (p10 c_0 c_0)) (not (p3 c_0)) (p10 (f16 c_1 c_0 c_0) c_1) (= c_1 c_0) (not (p10 c_0 c_1)) (not (p9 c_1)) (not (p9 c_0)) )(or (not (p10 c_0 c_0)) (not (p3 c_0)) (p10 (f16 c_2 c_0 c_0) c_2) (= c_2 c_0) (not (p10 c_0 c_2)) (not (p9 c_2)) (not (p9 c_0)) )(or (not (p10 c_0 c_1)) (not (p3 c_0)) (p10 (f16 c_0 c_1 c_0) c_0) (= c_0 c_1) (not (p10 c_0 c_0)) (not (p9 c_0)) (not (p9 c_1)) )(or (not (p10 c_0 c_1)) (not (p3 c_0)) (p10 (f16 c_1 c_1 c_0) c_1) (= c_1 c_1) (not (p10 c_0 c_1)) (not (p9 c_1)) (not (p9 c_1)) )(or (not (p10 c_0 c_1)) (not (p3 c_0)) (p10 (f16 c_2 c_1 c_0) c_2) (= c_2 c_1) (not (p10 c_0 c_2)) (not (p9 c_2)) (not (p9 c_1)) )(or (not (p10 c_0 c_2)) (not (p3 c_0)) (p10 (f16 c_0 c_2 c_0) c_0) (= c_0 c_2) (not (p10 c_0 c_0)) (not (p9 c_0)) (not (p9 c_2)) )(or (not (p10 c_0 c_2)) (not (p3 c_0)) (p10 (f16 c_1 c_2 c_0) c_1) (= c_1 c_2) (not (p10 c_0 c_1)) (not (p9 c_1)) (not (p9 c_2)) )(or (not (p10 c_0 c_2)) (not (p3 c_0)) (p10 (f16 c_2 c_2 c_0) c_2) (= c_2 c_2) (not (p10 c_0 c_2)) (not (p9 c_2)) (not (p9 c_2)) )(or (not (p10 c_1 c_0)) (not (p3 c_1)) (p10 (f16 c_0 c_0 c_1) c_0) (= c_0 c_0) (not (p10 c_1 c_0)) (not (p9 c_0)) (not (p9 c_0)) )(or (not (p10 c_1 c_0)) (not (p3 c_1)) (p10 (f16 c_1 c_0 c_1) c_1) (= c_1 c_0) (not (p10 c_1 c_1)) (not (p9 c_1)) (not (p9 c_0)) )(or (not (p10 c_1 c_0)) (not (p3 c_1)) (p10 (f16 c_2 c_0 c_1) c_2) (= c_2 c_0) (not (p10 c_1 c_2)) (not (p9 c_2)) (not (p9 c_0)) )(or (not (p10 c_1 c_1)) (not (p3 c_1)) (p10 (f16 c_0 c_1 c_1) c_0) (= c_0 c_1) (not (p10 c_1 c_0)) (not (p9 c_0)) (not (p9 c_1)) )(or (not (p10 c_1 c_1)) (not (p3 c_1)) (p10 (f16 c_1 c_1 c_1) c_1) (= c_1 c_1) (not (p10 c_1 c_1)) (not (p9 c_1)) (not (p9 c_1)) )(or (not (p10 c_1 c_1)) (not (p3 c_1)) (p10 (f16 c_2 c_1 c_1) c_2) (= c_2 c_1) (not (p10 c_1 c_2)) (not (p9 c_2)) (not (p9 c_1)) )(or (not (p10 c_1 c_2)) (not (p3 c_1)) (p10 (f16 c_0 c_2 c_1) c_0) (= c_0 c_2) (not (p10 c_1 c_0)) (not (p9 c_0)) (not (p9 c_2)) )(or (not (p10 c_1 c_2)) (not (p3 c_1)) (p10 (f16 c_1 c_2 c_1) c_1) (= c_1 c_2) (not (p10 c_1 c_1)) (not (p9 c_1)) (not (p9 c_2)) )(or (not (p10 c_1 c_2)) (not (p3 c_1)) (p10 (f16 c_2 c_2 c_1) c_2) (= c_2 c_2) (not (p10 c_1 c_2)) (not (p9 c_2)) (not (p9 c_2)) )(or (not (p10 c_2 c_0)) (not (p3 c_2)) (p10 (f16 c_0 c_0 c_2) c_0) (= c_0 c_0) (not (p10 c_2 c_0)) (not (p9 c_0)) (not (p9 c_0)) )(or (not (p10 c_2 c_0)) (not (p3 c_2)) (p10 (f16 c_1 c_0 c_2) c_1) (= c_1 c_0) (not (p10 c_2 c_1)) (not (p9 c_1)) (not (p9 c_0)) )(or (not (p10 c_2 c_0)) (not (p3 c_2)) (p10 (f16 c_2 c_0 c_2) c_2) (= c_2 c_0) (not (p10 c_2 c_2)) (not (p9 c_2)) (not (p9 c_0)) )(or (not (p10 c_2 c_1)) (not (p3 c_2)) (p10 (f16 c_0 c_1 c_2) c_0) (= c_0 c_1) (not (p10 c_2 c_0)) (not (p9 c_0)) (not (p9 c_1)) )(or (not (p10 c_2 c_1)) (not (p3 c_2)) (p10 (f16 c_1 c_1 c_2) c_1) (= c_1 c_1) (not (p10 c_2 c_1)) (not (p9 c_1)) (not (p9 c_1)) )(or (not (p10 c_2 c_1)) (not (p3 c_2)) (p10 (f16 c_2 c_1 c_2) c_2) (= c_2 c_1) (not (p10 c_2 c_2)) (not (p9 c_2)) (not (p9 c_1)) )(or (not (p10 c_2 c_2)) (not (p3 c_2)) (p10 (f16 c_0 c_2 c_2) c_0) (= c_0 c_2) (not (p10 c_2 c_0)) (not (p9 c_0)) (not (p9 c_2)) )(or (not (p10 c_2 c_2)) (not (p3 c_2)) (p10 (f16 c_1 c_2 c_2) c_1) (= c_1 c_2) (not (p10 c_2 c_1)) (not (p9 c_1)) (not (p9 c_2)) )(or (not (p10 c_2 c_2)) (not (p3 c_2)) (p10 (f16 c_2 c_2 c_2) c_2) (= c_2 c_2) (not (p10 c_2 c_2)) (not (p9 c_2)) (not (p9 c_2)) )(or (not (p4 c_0)) (not (= (f5 c_0) (f6 c_0))) )(or (not (p4 c_1)) (not (= (f5 c_1) (f6 c_1))) )(or (not (p4 c_2)) (not (= (f5 c_2) (f6 c_2))) )(or (not (p4 c_0)) (p3 (f5 c_0)) )(or (not (p4 c_1)) (p3 (f5 c_1)) )(or (not (p4 c_2)) (p3 (f5 c_2)) )(or (= c_0 c_0) (not (p3 c_0)) (p1 c_0 (f17 c_0 c_0 c_0)) (not (p3 c_0)) (not (p14 c_0 c_0 c_0)) (= c_0 c_0) (not (p3 c_0)) (= c_0 c_0) )(or (= c_0 c_0) (not (p3 c_0)) (p1 c_0 (f17 c_1 c_0 c_0)) (not (p3 c_0)) (not (p14 c_1 c_0 c_0)) (= c_1 c_0) (not (p3 c_1)) (= c_1 c_0) )(or (= c_0 c_0) (not (p3 c_0)) (p1 c_0 (f17 c_2 c_0 c_0)) (not (p3 c_0)) (not (p14 c_2 c_0 c_0)) (= c_2 c_0) (not (p3 c_2)) (= c_2 c_0) )(or (= c_0 c_1) (not (p3 c_0)) (p1 c_0 (f17 c_0 c_0 c_1)) (not (p3 c_1)) (not (p14 c_0 c_0 c_1)) (= c_0 c_0) (not (p3 c_0)) (= c_0 c_1) )(or (= c_0 c_1) (not (p3 c_0)) (p1 c_0 (f17 c_1 c_0 c_1)) (not (p3 c_1)) (not (p14 c_1 c_0 c_1)) (= c_1 c_0) (not (p3 c_1)) (= c_1 c_1) )(or (= c_0 c_1) (not (p3 c_0)) (p1 c_0 (f17 c_2 c_0 c_1)) (not (p3 c_1)) (not (p14 c_2 c_0 c_1)) (= c_2 c_0) (not (p3 c_2)) (= c_2 c_1) )(or (= c_0 c_2) (not (p3 c_0)) (p1 c_0 (f17 c_0 c_0 c_2)) (not (p3 c_2)) (not (p14 c_0 c_0 c_2)) (= c_0 c_0) (not (p3 c_0)) (= c_0 c_2) )(or (= c_0 c_2) (not (p3 c_0)) (p1 c_0 (f17 c_1 c_0 c_2)) (not (p3 c_2)) (not (p14 c_1 c_0 c_2)) (= c_1 c_0) (not (p3 c_1)) (= c_1 c_2) )(or (= c_0 c_2) (not (p3 c_0)) (p1 c_0 (f17 c_2 c_0 c_2)) (not (p3 c_2)) (not (p14 c_2 c_0 c_2)) (= c_2 c_0) (not (p3 c_2)) (= c_2 c_2) )(or (= c_1 c_0) (not (p3 c_1)) (p1 c_1 (f17 c_0 c_1 c_0)) (not (p3 c_0)) (not (p14 c_0 c_1 c_0)) (= c_0 c_1) (not (p3 c_0)) (= c_0 c_0) )(or (= c_1 c_0) (not (p3 c_1)) (p1 c_1 (f17 c_1 c_1 c_0)) (not (p3 c_0)) (not (p14 c_1 c_1 c_0)) (= c_1 c_1) (not (p3 c_1)) (= c_1 c_0) )(or (= c_1 c_0) (not (p3 c_1)) (p1 c_1 (f17 c_2 c_1 c_0)) (not (p3 c_0)) (not (p14 c_2 c_1 c_0)) (= c_2 c_1) (not (p3 c_2)) (= c_2 c_0) )(or (= c_1 c_1) (not (p3 c_1)) (p1 c_1 (f17 c_0 c_1 c_1)) (not (p3 c_1)) (not (p14 c_0 c_1 c_1)) (= c_0 c_1) (not (p3 c_0)) (= c_0 c_1) )(or (= c_1 c_1) (not (p3 c_1)) (p1 c_1 (f17 c_1 c_1 c_1)) (not (p3 c_1)) (not (p14 c_1 c_1 c_1)) (= c_1 c_1) (not (p3 c_1)) (= c_1 c_1) )(or (= c_1 c_1) (not (p3 c_1)) (p1 c_1 (f17 c_2 c_1 c_1)) (not (p3 c_1)) (not (p14 c_2 c_1 c_1)) (= c_2 c_1) (not (p3 c_2)) (= c_2 c_1) )(or (= c_1 c_2) (not (p3 c_1)) (p1 c_1 (f17 c_0 c_1 c_2)) (not (p3 c_2)) (not (p14 c_0 c_1 c_2)) (= c_0 c_1) (not (p3 c_0)) (= c_0 c_2) )(or (= c_1 c_2) (not (p3 c_1)) (p1 c_1 (f17 c_1 c_1 c_2)) (not (p3 c_2)) (not (p14 c_1 c_1 c_2)) (= c_1 c_1) (not (p3 c_1)) (= c_1 c_2) )(or (= c_1 c_2) (not (p3 c_1)) (p1 c_1 (f17 c_2 c_1 c_2)) (not (p3 c_2)) (not (p14 c_2 c_1 c_2)) (= c_2 c_1) (not (p3 c_2)) (= c_2 c_2) )(or (= c_2 c_0) (not (p3 c_2)) (p1 c_2 (f17 c_0 c_2 c_0)) (not (p3 c_0)) (not (p14 c_0 c_2 c_0)) (= c_0 c_2) (not (p3 c_0)) (= c_0 c_0) )(or (= c_2 c_0) (not (p3 c_2)) (p1 c_2 (f17 c_1 c_2 c_0)) (not (p3 c_0)) (not (p14 c_1 c_2 c_0)) (= c_1 c_2) (not (p3 c_1)) (= c_1 c_0) )(or (= c_2 c_0) (not (p3 c_2)) (p1 c_2 (f17 c_2 c_2 c_0)) (not (p3 c_0)) (not (p14 c_2 c_2 c_0)) (= c_2 c_2) (not (p3 c_2)) (= c_2 c_0) )(or (= c_2 c_1) (not (p3 c_2)) (p1 c_2 (f17 c_0 c_2 c_1)) (not (p3 c_1)) (not (p14 c_0 c_2 c_1)) (= c_0 c_2) (not (p3 c_0)) (= c_0 c_1) )(or (= c_2 c_1) (not (p3 c_2)) (p1 c_2 (f17 c_1 c_2 c_1)) (not (p3 c_1)) (not (p14 c_1 c_2 c_1)) (= c_1 c_2) (not (p3 c_1)) (= c_1 c_1) )(or (= c_2 c_1) (not (p3 c_2)) (p1 c_2 (f17 c_2 c_2 c_1)) (not (p3 c_1)) (not (p14 c_2 c_2 c_1)) (= c_2 c_2) (not (p3 c_2)) (= c_2 c_1) )(or (= c_2 c_2) (not (p3 c_2)) (p1 c_2 (f17 c_0 c_2 c_2)) (not (p3 c_2)) (not (p14 c_0 c_2 c_2)) (= c_0 c_2) (not (p3 c_0)) (= c_0 c_2) )(or (= c_2 c_2) (not (p3 c_2)) (p1 c_2 (f17 c_1 c_2 c_2)) (not (p3 c_2)) (not (p14 c_1 c_2 c_2)) (= c_1 c_2) (not (p3 c_1)) (= c_1 c_2) )(or (= c_2 c_2) (not (p3 c_2)) (p1 c_2 (f17 c_2 c_2 c_2)) (not (p3 c_2)) (not (p14 c_2 c_2 c_2)) (= c_2 c_2) (not (p3 c_2)) (= c_2 c_2) )(or (not (p3 c_0)) (not (p3 c_0)) (= c_0 c_0) (= c_0 c_0) (p9 (f13 c_0 c_0 c_0)) (= c_0 c_0) (not (p3 c_0)) (p14 c_0 c_0 c_0) )(or (not (p3 c_0)) (not (p3 c_0)) (= c_1 c_0) (= c_0 c_0) (p9 (f13 c_0 c_1 c_0)) (= c_0 c_1) (not (p3 c_1)) (p14 c_0 c_1 c_0) )(or (not (p3 c_0)) (not (p3 c_0)) (= c_2 c_0) (= c_0 c_0) (p9 (f13 c_0 c_2 c_0)) (= c_0 c_2) (not (p3 c_2)) (p14 c_0 c_2 c_0) )(or (not (p3 c_0)) (not (p3 c_1)) (= c_0 c_1) (= c_0 c_1) (p9 (f13 c_0 c_0 c_1)) (= c_0 c_0) (not (p3 c_0)) (p14 c_0 c_0 c_1) )(or (not (p3 c_0)) (not (p3 c_1)) (= c_1 c_1) (= c_0 c_1) (p9 (f13 c_0 c_1 c_1)) (= c_0 c_1) (not (p3 c_1)) (p14 c_0 c_1 c_1) )(or (not (p3 c_0)) (not (p3 c_1)) (= c_2 c_1) (= c_0 c_1) (p9 (f13 c_0 c_2 c_1)) (= c_0 c_2) (not (p3 c_2)) (p14 c_0 c_2 c_1) )(or (not (p3 c_0)) (not (p3 c_2)) (= c_0 c_2) (= c_0 c_2) (p9 (f13 c_0 c_0 c_2)) (= c_0 c_0) (not (p3 c_0)) (p14 c_0 c_0 c_2) )(or (not (p3 c_0)) (not (p3 c_2)) (= c_1 c_2) (= c_0 c_2) (p9 (f13 c_0 c_1 c_2)) (= c_0 c_1) (not (p3 c_1)) (p14 c_0 c_1 c_2) )(or (not (p3 c_0)) (not (p3 c_2)) (= c_2 c_2) (= c_0 c_2) (p9 (f13 c_0 c_2 c_2)) (= c_0 c_2) (not (p3 c_2)) (p14 c_0 c_2 c_2) )(or (not (p3 c_1)) (not (p3 c_0)) (= c_0 c_0) (= c_1 c_0) (p9 (f13 c_1 c_0 c_0)) (= c_1 c_0) (not (p3 c_0)) (p14 c_1 c_0 c_0) )(or (not (p3 c_1)) (not (p3 c_0)) (= c_1 c_0) (= c_1 c_0) (p9 (f13 c_1 c_1 c_0)) (= c_1 c_1) (not (p3 c_1)) (p14 c_1 c_1 c_0) )(or (not (p3 c_1)) (not (p3 c_0)) (= c_2 c_0) (= c_1 c_0) (p9 (f13 c_1 c_2 c_0)) (= c_1 c_2) (not (p3 c_2)) (p14 c_1 c_2 c_0) )(or (not (p3 c_1)) (not (p3 c_1)) (= c_0 c_1) (= c_1 c_1) (p9 (f13 c_1 c_0 c_1)) (= c_1 c_0) (not (p3 c_0)) (p14 c_1 c_0 c_1) )(or (not (p3 c_1)) (not (p3 c_1)) (= c_1 c_1) (= c_1 c_1) (p9 (f13 c_1 c_1 c_1)) (= c_1 c_1) (not (p3 c_1)) (p14 c_1 c_1 c_1) )(or (not (p3 c_1)) (not (p3 c_1)) (= c_2 c_1) (= c_1 c_1) (p9 (f13 c_1 c_2 c_1)) (= c_1 c_2) (not (p3 c_2)) (p14 c_1 c_2 c_1) )(or (not (p3 c_1)) (not (p3 c_2)) (= c_0 c_2) (= c_1 c_2) (p9 (f13 c_1 c_0 c_2)) (= c_1 c_0) (not (p3 c_0)) (p14 c_1 c_0 c_2) )(or (not (p3 c_1)) (not (p3 c_2)) (= c_1 c_2) (= c_1 c_2) (p9 (f13 c_1 c_1 c_2)) (= c_1 c_1) (not (p3 c_1)) (p14 c_1 c_1 c_2) )(or (not (p3 c_1)) (not (p3 c_2)) (= c_2 c_2) (= c_1 c_2) (p9 (f13 c_1 c_2 c_2)) (= c_1 c_2) (not (p3 c_2)) (p14 c_1 c_2 c_2) )(or (not (p3 c_2)) (not (p3 c_0)) (= c_0 c_0) (= c_2 c_0) (p9 (f13 c_2 c_0 c_0)) (= c_2 c_0) (not (p3 c_0)) (p14 c_2 c_0 c_0) )(or (not (p3 c_2)) (not (p3 c_0)) (= c_1 c_0) (= c_2 c_0) (p9 (f13 c_2 c_1 c_0)) (= c_2 c_1) (not (p3 c_1)) (p14 c_2 c_1 c_0) )(or (not (p3 c_2)) (not (p3 c_0)) (= c_2 c_0) (= c_2 c_0) (p9 (f13 c_2 c_2 c_0)) (= c_2 c_2) (not (p3 c_2)) (p14 c_2 c_2 c_0) )(or (not (p3 c_2)) (not (p3 c_1)) (= c_0 c_1) (= c_2 c_1) (p9 (f13 c_2 c_0 c_1)) (= c_2 c_0) (not (p3 c_0)) (p14 c_2 c_0 c_1) )(or (not (p3 c_2)) (not (p3 c_1)) (= c_1 c_1) (= c_2 c_1) (p9 (f13 c_2 c_1 c_1)) (= c_2 c_1) (not (p3 c_1)) (p14 c_2 c_1 c_1) )(or (not (p3 c_2)) (not (p3 c_1)) (= c_2 c_1) (= c_2 c_1) (p9 (f13 c_2 c_2 c_1)) (= c_2 c_2) (not (p3 c_2)) (p14 c_2 c_2 c_1) )(or (not (p3 c_2)) (not (p3 c_2)) (= c_0 c_2) (= c_2 c_2) (p9 (f13 c_2 c_0 c_2)) (= c_2 c_0) (not (p3 c_0)) (p14 c_2 c_0 c_2) )(or (not (p3 c_2)) (not (p3 c_2)) (= c_1 c_2) (= c_2 c_2) (p9 (f13 c_2 c_1 c_2)) (= c_2 c_1) (not (p3 c_1)) (p14 c_2 c_1 c_2) )(or (not (p3 c_2)) (not (p3 c_2)) (= c_2 c_2) (= c_2 c_2) (p9 (f13 c_2 c_2 c_2)) (= c_2 c_2) (not (p3 c_2)) (p14 c_2 c_2 c_2) )(or (p1 c_0 (f17 c_0 c_0 c_0)) (not (p14 c_0 c_0 c_0)) (not (p3 c_0)) (= c_0 c_0) (not (p3 c_0)) (not (p3 c_0)) (= c_0 c_0) (= c_0 c_0) )(or (p1 c_0 (f17 c_0 c_1 c_0)) (not (p14 c_0 c_1 c_0)) (not (p3 c_0)) (= c_0 c_1) (not (p3 c_1)) (not (p3 c_0)) (= c_1 c_0) (= c_0 c_0) )(or (p1 c_0 (f17 c_0 c_2 c_0)) (not (p14 c_0 c_2 c_0)) (not (p3 c_0)) (= c_0 c_2) (not (p3 c_2)) (not (p3 c_0)) (= c_2 c_0) (= c_0 c_0) )(or (p1 c_0 (f17 c_1 c_0 c_0)) (not (p14 c_1 c_0 c_0)) (not (p3 c_1)) (= c_1 c_0) (not (p3 c_0)) (not (p3 c_0)) (= c_0 c_0) (= c_1 c_0) )(or (p1 c_0 (f17 c_1 c_1 c_0)) (not (p14 c_1 c_1 c_0)) (not (p3 c_1)) (= c_1 c_1) (not (p3 c_1)) (not (p3 c_0)) (= c_1 c_0) (= c_1 c_0) )(or (p1 c_0 (f17 c_1 c_2 c_0)) (not (p14 c_1 c_2 c_0)) (not (p3 c_1)) (= c_1 c_2) (not (p3 c_2)) (not (p3 c_0)) (= c_2 c_0) (= c_1 c_0) )(or (p1 c_0 (f17 c_2 c_0 c_0)) (not (p14 c_2 c_0 c_0)) (not (p3 c_2)) (= c_2 c_0) (not (p3 c_0)) (not (p3 c_0)) (= c_0 c_0) (= c_2 c_0) )(or (p1 c_0 (f17 c_2 c_1 c_0)) (not (p14 c_2 c_1 c_0)) (not (p3 c_2)) (= c_2 c_1) (not (p3 c_1)) (not (p3 c_0)) (= c_1 c_0) (= c_2 c_0) )(or (p1 c_0 (f17 c_2 c_2 c_0)) (not (p14 c_2 c_2 c_0)) (not (p3 c_2)) (= c_2 c_2) (not (p3 c_2)) (not (p3 c_0)) (= c_2 c_0) (= c_2 c_0) )(or (p1 c_1 (f17 c_0 c_0 c_1)) (not (p14 c_0 c_0 c_1)) (not (p3 c_0)) (= c_0 c_0) (not (p3 c_0)) (not (p3 c_1)) (= c_0 c_1) (= c_0 c_1) )(or (p1 c_1 (f17 c_0 c_1 c_1)) (not (p14 c_0 c_1 c_1)) (not (p3 c_0)) (= c_0 c_1) (not (p3 c_1)) (not (p3 c_1)) (= c_1 c_1) (= c_0 c_1) )(or (p1 c_1 (f17 c_0 c_2 c_1)) (not (p14 c_0 c_2 c_1)) (not (p3 c_0)) (= c_0 c_2) (not (p3 c_2)) (not (p3 c_1)) (= c_2 c_1) (= c_0 c_1) )(or (p1 c_1 (f17 c_1 c_0 c_1)) (not (p14 c_1 c_0 c_1)) (not (p3 c_1)) (= c_1 c_0) (not (p3 c_0)) (not (p3 c_1)) (= c_0 c_1) (= c_1 c_1) )(or (p1 c_1 (f17 c_1 c_1 c_1)) (not (p14 c_1 c_1 c_1)) (not (p3 c_1)) (= c_1 c_1) (not (p3 c_1)) (not (p3 c_1)) (= c_1 c_1) (= c_1 c_1) )(or (p1 c_1 (f17 c_1 c_2 c_1)) (not (p14 c_1 c_2 c_1)) (not (p3 c_1)) (= c_1 c_2) (not (p3 c_2)) (not (p3 c_1)) (= c_2 c_1) (= c_1 c_1) )(or (p1 c_1 (f17 c_2 c_0 c_1)) (not (p14 c_2 c_0 c_1)) (not (p3 c_2)) (= c_2 c_0) (not (p3 c_0)) (not (p3 c_1)) (= c_0 c_1) (= c_2 c_1) )(or (p1 c_1 (f17 c_2 c_1 c_1)) (not (p14 c_2 c_1 c_1)) (not (p3 c_2)) (= c_2 c_1) (not (p3 c_1)) (not (p3 c_1)) (= c_1 c_1) (= c_2 c_1) )(or (p1 c_1 (f17 c_2 c_2 c_1)) (not (p14 c_2 c_2 c_1)) (not (p3 c_2)) (= c_2 c_2) (not (p3 c_2)) (not (p3 c_1)) (= c_2 c_1) (= c_2 c_1) )(or (p1 c_2 (f17 c_0 c_0 c_2)) (not (p14 c_0 c_0 c_2)) (not (p3 c_0)) (= c_0 c_0) (not (p3 c_0)) (not (p3 c_2)) (= c_0 c_2) (= c_0 c_2) )(or (p1 c_2 (f17 c_0 c_1 c_2)) (not (p14 c_0 c_1 c_2)) (not (p3 c_0)) (= c_0 c_1) (not (p3 c_1)) (not (p3 c_2)) (= c_1 c_2) (= c_0 c_2) )(or (p1 c_2 (f17 c_0 c_2 c_2)) (not (p14 c_0 c_2 c_2)) (not (p3 c_0)) (= c_0 c_2) (not (p3 c_2)) (not (p3 c_2)) (= c_2 c_2) (= c_0 c_2) )(or (p1 c_2 (f17 c_1 c_0 c_2)) (not (p14 c_1 c_0 c_2)) (not (p3 c_1)) (= c_1 c_0) (not (p3 c_0)) (not (p3 c_2)) (= c_0 c_2) (= c_1 c_2) )(or (p1 c_2 (f17 c_1 c_1 c_2)) (not (p14 c_1 c_1 c_2)) (not (p3 c_1)) (= c_1 c_1) (not (p3 c_1)) (not (p3 c_2)) (= c_1 c_2) (= c_1 c_2) )(or (p1 c_2 (f17 c_1 c_2 c_2)) (not (p14 c_1 c_2 c_2)) (not (p3 c_1)) (= c_1 c_2) (not (p3 c_2)) (not (p3 c_2)) (= c_2 c_2) (= c_1 c_2) )(or (p1 c_2 (f17 c_2 c_0 c_2)) (not (p14 c_2 c_0 c_2)) (not (p3 c_2)) (= c_2 c_0) (not (p3 c_0)) (not (p3 c_2)) (= c_0 c_2) (= c_2 c_2) )(or (p1 c_2 (f17 c_2 c_1 c_2)) (not (p14 c_2 c_1 c_2)) (not (p3 c_2)) (= c_2 c_1) (not (p3 c_1)) (not (p3 c_2)) (= c_1 c_2) (= c_2 c_2) )(or (p1 c_2 (f17 c_2 c_2 c_2)) (not (p14 c_2 c_2 c_2)) (not (p3 c_2)) (= c_2 c_2) (not (p3 c_2)) (not (p3 c_2)) (= c_2 c_2) (= c_2 c_2) )(or (not (p10 c_0 c_0)) (= c_0 c_0) (not (p9 c_0)) (not (p9 c_0)) (p10 (f16 c_0 c_0 c_0) c_0) (not (p10 c_0 c_0)) (not (p3 c_0)) )(or (not (p10 c_0 c_0)) (= c_1 c_0) (not (p9 c_0)) (not (p9 c_1)) (p10 (f16 c_1 c_0 c_0) c_0) (not (p10 c_0 c_1)) (not (p3 c_0)) )(or (not (p10 c_0 c_0)) (= c_2 c_0) (not (p9 c_0)) (not (p9 c_2)) (p10 (f16 c_2 c_0 c_0) c_0) (not (p10 c_0 c_2)) (not (p3 c_0)) )(or (not (p10 c_0 c_1)) (= c_0 c_1) (not (p9 c_1)) (not (p9 c_0)) (p10 (f16 c_0 c_1 c_0) c_1) (not (p10 c_0 c_0)) (not (p3 c_0)) )(or (not (p10 c_0 c_1)) (= c_1 c_1) (not (p9 c_1)) (not (p9 c_1)) (p10 (f16 c_1 c_1 c_0) c_1) (not (p10 c_0 c_1)) (not (p3 c_0)) )(or (not (p10 c_0 c_1)) (= c_2 c_1) (not (p9 c_1)) (not (p9 c_2)) (p10 (f16 c_2 c_1 c_0) c_1) (not (p10 c_0 c_2)) (not (p3 c_0)) )(or (not (p10 c_0 c_2)) (= c_0 c_2) (not (p9 c_2)) (not (p9 c_0)) (p10 (f16 c_0 c_2 c_0) c_2) (not (p10 c_0 c_0)) (not (p3 c_0)) )(or (not (p10 c_0 c_2)) (= c_1 c_2) (not (p9 c_2)) (not (p9 c_1)) (p10 (f16 c_1 c_2 c_0) c_2) (not (p10 c_0 c_1)) (not (p3 c_0)) )(or (not (p10 c_0 c_2)) (= c_2 c_2) (not (p9 c_2)) (not (p9 c_2)) (p10 (f16 c_2 c_2 c_0) c_2) (not (p10 c_0 c_2)) (not (p3 c_0)) )(or (not (p10 c_1 c_0)) (= c_0 c_0) (not (p9 c_0)) (not (p9 c_0)) (p10 (f16 c_0 c_0 c_1) c_0) (not (p10 c_1 c_0)) (not (p3 c_1)) )(or (not (p10 c_1 c_0)) (= c_1 c_0) (not (p9 c_0)) (not (p9 c_1)) (p10 (f16 c_1 c_0 c_1) c_0) (not (p10 c_1 c_1)) (not (p3 c_1)) )(or (not (p10 c_1 c_0)) (= c_2 c_0) (not (p9 c_0)) (not (p9 c_2)) (p10 (f16 c_2 c_0 c_1) c_0) (not (p10 c_1 c_2)) (not (p3 c_1)) )(or (not (p10 c_1 c_1)) (= c_0 c_1) (not (p9 c_1)) (not (p9 c_0)) (p10 (f16 c_0 c_1 c_1) c_1) (not (p10 c_1 c_0)) (not (p3 c_1)) )(or (not (p10 c_1 c_1)) (= c_1 c_1) (not (p9 c_1)) (not (p9 c_1)) (p10 (f16 c_1 c_1 c_1) c_1) (not (p10 c_1 c_1)) (not (p3 c_1)) )(or (not (p10 c_1 c_1)) (= c_2 c_1) (not (p9 c_1)) (not (p9 c_2)) (p10 (f16 c_2 c_1 c_1) c_1) (not (p10 c_1 c_2)) (not (p3 c_1)) )(or (not (p10 c_1 c_2)) (= c_0 c_2) (not (p9 c_2)) (not (p9 c_0)) (p10 (f16 c_0 c_2 c_1) c_2) (not (p10 c_1 c_0)) (not (p3 c_1)) )(or (not (p10 c_1 c_2)) (= c_1 c_2) (not (p9 c_2)) (not (p9 c_1)) (p10 (f16 c_1 c_2 c_1) c_2) (not (p10 c_1 c_1)) (not (p3 c_1)) )(or (not (p10 c_1 c_2)) (= c_2 c_2) (not (p9 c_2)) (not (p9 c_2)) (p10 (f16 c_2 c_2 c_1) c_2) (not (p10 c_1 c_2)) (not (p3 c_1)) )(or (not (p10 c_2 c_0)) (= c_0 c_0) (not (p9 c_0)) (not (p9 c_0)) (p10 (f16 c_0 c_0 c_2) c_0) (not (p10 c_2 c_0)) (not (p3 c_2)) )(or (not (p10 c_2 c_0)) (= c_1 c_0) (not (p9 c_0)) (not (p9 c_1)) (p10 (f16 c_1 c_0 c_2) c_0) (not (p10 c_2 c_1)) (not (p3 c_2)) )(or (not (p10 c_2 c_0)) (= c_2 c_0) (not (p9 c_0)) (not (p9 c_2)) (p10 (f16 c_2 c_0 c_2) c_0) (not (p10 c_2 c_2)) (not (p3 c_2)) )(or (not (p10 c_2 c_1)) (= c_0 c_1) (not (p9 c_1)) (not (p9 c_0)) (p10 (f16 c_0 c_1 c_2) c_1) (not (p10 c_2 c_0)) (not (p3 c_2)) )(or (not (p10 c_2 c_1)) (= c_1 c_1) (not (p9 c_1)) (not (p9 c_1)) (p10 (f16 c_1 c_1 c_2) c_1) (not (p10 c_2 c_1)) (not (p3 c_2)) )(or (not (p10 c_2 c_1)) (= c_2 c_1) (not (p9 c_1)) (not (p9 c_2)) (p10 (f16 c_2 c_1 c_2) c_1) (not (p10 c_2 c_2)) (not (p3 c_2)) )(or (not (p10 c_2 c_2)) (= c_0 c_2) (not (p9 c_2)) (not (p9 c_0)) (p10 (f16 c_0 c_2 c_2) c_2) (not (p10 c_2 c_0)) (not (p3 c_2)) )(or (not (p10 c_2 c_2)) (= c_1 c_2) (not (p9 c_2)) (not (p9 c_1)) (p10 (f16 c_1 c_2 c_2) c_2) (not (p10 c_2 c_1)) (not (p3 c_2)) )(or (not (p10 c_2 c_2)) (= c_2 c_2) (not (p9 c_2)) (not (p9 c_2)) (p10 (f16 c_2 c_2 c_2) c_2) (not (p10 c_2 c_2)) (not (p3 c_2)) )(p4 c8) (or (not (p3 c_0)) (= c_0 c_0) (p1 c_0 (f2 c_0 c_0)) (not (p3 c_0)) )(or (not (p3 c_0)) (= c_1 c_0) (p1 c_1 (f2 c_1 c_0)) (not (p3 c_1)) )(or (not (p3 c_0)) (= c_2 c_0) (p1 c_2 (f2 c_2 c_0)) (not (p3 c_2)) )(or (not (p3 c_1)) (= c_0 c_1) (p1 c_0 (f2 c_0 c_1)) (not (p3 c_0)) )(or (not (p3 c_1)) (= c_1 c_1) (p1 c_1 (f2 c_1 c_1)) (not (p3 c_1)) )(or (not (p3 c_1)) (= c_2 c_1) (p1 c_2 (f2 c_2 c_1)) (not (p3 c_2)) )(or (not (p3 c_2)) (= c_0 c_2) (p1 c_0 (f2 c_0 c_2)) (not (p3 c_0)) )(or (not (p3 c_2)) (= c_1 c_2) (p1 c_1 (f2 c_1 c_2)) (not (p3 c_1)) )(or (not (p3 c_2)) (= c_2 c_2) (p1 c_2 (f2 c_2 c_2)) (not (p3 c_2)) )(or (= c_0 c_0) (= c_0 c_0) (not (p3 c_0)) (p1 c_0 (f17 c_0 c_0 c_0)) (not (p14 c_0 c_0 c_0)) (= c_0 c_0) (not (p3 c_0)) (not (p3 c_0)) )(or (= c_0 c_0) (= c_1 c_0) (not (p3 c_0)) (p1 c_1 (f17 c_1 c_0 c_0)) (not (p14 c_1 c_0 c_0)) (= c_1 c_0) (not (p3 c_0)) (not (p3 c_1)) )(or (= c_0 c_0) (= c_2 c_0) (not (p3 c_0)) (p1 c_2 (f17 c_2 c_0 c_0)) (not (p14 c_2 c_0 c_0)) (= c_2 c_0) (not (p3 c_0)) (not (p3 c_2)) )(or (= c_0 c_1) (= c_0 c_1) (not (p3 c_0)) (p1 c_0 (f17 c_0 c_0 c_1)) (not (p14 c_0 c_0 c_1)) (= c_0 c_0) (not (p3 c_1)) (not (p3 c_0)) )(or (= c_0 c_1) (= c_1 c_1) (not (p3 c_0)) (p1 c_1 (f17 c_1 c_0 c_1)) (not (p14 c_1 c_0 c_1)) (= c_1 c_0) (not (p3 c_1)) (not (p3 c_1)) )(or (= c_0 c_1) (= c_2 c_1) (not (p3 c_0)) (p1 c_2 (f17 c_2 c_0 c_1)) (not (p14 c_2 c_0 c_1)) (= c_2 c_0) (not (p3 c_1)) (not (p3 c_2)) )(or (= c_0 c_2) (= c_0 c_2) (not (p3 c_0)) (p1 c_0 (f17 c_0 c_0 c_2)) (not (p14 c_0 c_0 c_2)) (= c_0 c_0) (not (p3 c_2)) (not (p3 c_0)) )(or (= c_0 c_2) (= c_1 c_2) (not (p3 c_0)) (p1 c_1 (f17 c_1 c_0 c_2)) (not (p14 c_1 c_0 c_2)) (= c_1 c_0) (not (p3 c_2)) (not (p3 c_1)) )(or (= c_0 c_2) (= c_2 c_2) (not (p3 c_0)) (p1 c_2 (f17 c_2 c_0 c_2)) (not (p14 c_2 c_0 c_2)) (= c_2 c_0) (not (p3 c_2)) (not (p3 c_2)) )(or (= c_1 c_0) (= c_0 c_0) (not (p3 c_1)) (p1 c_0 (f17 c_0 c_1 c_0)) (not (p14 c_0 c_1 c_0)) (= c_0 c_1) (not (p3 c_0)) (not (p3 c_0)) )(or (= c_1 c_0) (= c_1 c_0) (not (p3 c_1)) (p1 c_1 (f17 c_1 c_1 c_0)) (not (p14 c_1 c_1 c_0)) (= c_1 c_1) (not (p3 c_0)) (not (p3 c_1)) )(or (= c_1 c_0) (= c_2 c_0) (not (p3 c_1)) (p1 c_2 (f17 c_2 c_1 c_0)) (not (p14 c_2 c_1 c_0)) (= c_2 c_1) (not (p3 c_0)) (not (p3 c_2)) )(or (= c_1 c_1) (= c_0 c_1) (not (p3 c_1)) (p1 c_0 (f17 c_0 c_1 c_1)) (not (p14 c_0 c_1 c_1)) (= c_0 c_1) (not (p3 c_1)) (not (p3 c_0)) )(or (= c_1 c_1) (= c_1 c_1) (not (p3 c_1)) (p1 c_1 (f17 c_1 c_1 c_1)) (not (p14 c_1 c_1 c_1)) (= c_1 c_1) (not (p3 c_1)) (not (p3 c_1)) )(or (= c_1 c_1) (= c_2 c_1) (not (p3 c_1)) (p1 c_2 (f17 c_2 c_1 c_1)) (not (p14 c_2 c_1 c_1)) (= c_2 c_1) (not (p3 c_1)) (not (p3 c_2)) )(or (= c_1 c_2) (= c_0 c_2) (not (p3 c_1)) (p1 c_0 (f17 c_0 c_1 c_2)) (not (p14 c_0 c_1 c_2)) (= c_0 c_1) (not (p3 c_2)) (not (p3 c_0)) )(or (= c_1 c_2) (= c_1 c_2) (not (p3 c_1)) (p1 c_1 (f17 c_1 c_1 c_2)) (not (p14 c_1 c_1 c_2)) (= c_1 c_1) (not (p3 c_2)) (not (p3 c_1)) )(or (= c_1 c_2) (= c_2 c_2) (not (p3 c_1)) (p1 c_2 (f17 c_2 c_1 c_2)) (not (p14 c_2 c_1 c_2)) (= c_2 c_1) (not (p3 c_2)) (not (p3 c_2)) )(or (= c_2 c_0) (= c_0 c_0) (not (p3 c_2)) (p1 c_0 (f17 c_0 c_2 c_0)) (not (p14 c_0 c_2 c_0)) (= c_0 c_2) (not (p3 c_0)) (not (p3 c_0)) )(or (= c_2 c_0) (= c_1 c_0) (not (p3 c_2)) (p1 c_1 (f17 c_1 c_2 c_0)) (not (p14 c_1 c_2 c_0)) (= c_1 c_2) (not (p3 c_0)) (not (p3 c_1)) )(or (= c_2 c_0) (= c_2 c_0) (not (p3 c_2)) (p1 c_2 (f17 c_2 c_2 c_0)) (not (p14 c_2 c_2 c_0)) (= c_2 c_2) (not (p3 c_0)) (not (p3 c_2)) )(or (= c_2 c_1) (= c_0 c_1) (not (p3 c_2)) (p1 c_0 (f17 c_0 c_2 c_1)) (not (p14 c_0 c_2 c_1)) (= c_0 c_2) (not (p3 c_1)) (not (p3 c_0)) )(or (= c_2 c_1) (= c_1 c_1) (not (p3 c_2)) (p1 c_1 (f17 c_1 c_2 c_1)) (not (p14 c_1 c_2 c_1)) (= c_1 c_2) (not (p3 c_1)) (not (p3 c_1)) )(or (= c_2 c_1) (= c_2 c_1) (not (p3 c_2)) (p1 c_2 (f17 c_2 c_2 c_1)) (not (p14 c_2 c_2 c_1)) (= c_2 c_2) (not (p3 c_1)) (not (p3 c_2)) )(or (= c_2 c_2) (= c_0 c_2) (not (p3 c_2)) (p1 c_0 (f17 c_0 c_2 c_2)) (not (p14 c_0 c_2 c_2)) (= c_0 c_2) (not (p3 c_2)) (not (p3 c_0)) )(or (= c_2 c_2) (= c_1 c_2) (not (p3 c_2)) (p1 c_1 (f17 c_1 c_2 c_2)) (not (p14 c_1 c_2 c_2)) (= c_1 c_2) (not (p3 c_2)) (not (p3 c_1)) )(or (= c_2 c_2) (= c_2 c_2) (not (p3 c_2)) (p1 c_2 (f17 c_2 c_2 c_2)) (not (p14 c_2 c_2 c_2)) (= c_2 c_2) (not (p3 c_2)) (not (p3 c_2)) )(or (p14 c_0 c_0 c_0) (not (p3 c_0)) (not (p10 c_0 c_0)) (not (p10 c_0 c_0)) (not (p9 c_0)) (not (p10 c_0 c_0)) (not (p10 c_0 c_0)) (= c_0 c_0) (not (p3 c_0)) (not (p9 c_0)) (not (p10 c_0 c_0)) (= c_0 c_0) (not (p3 c_0)) (= c_0 c_0) (= c_0 c_0) (not (p10 c_0 c_0)) )(or (p14 c_0 c_0 c_0) (not (p3 c_0)) (not (p10 c_0 c_0)) (not (p10 c_0 c_1)) (not (p9 c_0)) (not (p10 c_0 c_0)) (not (p10 c_0 c_1)) (= c_0 c_1) (not (p3 c_0)) (not (p9 c_1)) (not (p10 c_0 c_1)) (= c_0 c_0) (not (p3 c_0)) (= c_0 c_0) (= c_0 c_0) (not (p10 c_0 c_0)) )(or (p14 c_0 c_0 c_0) (not (p3 c_0)) (not (p10 c_0 c_0)) (not (p10 c_0 c_2)) (not (p9 c_0)) (not (p10 c_0 c_0)) (not (p10 c_0 c_2)) (= c_0 c_2) (not (p3 c_0)) (not (p9 c_2)) (not (p10 c_0 c_2)) (= c_0 c_0) (not (p3 c_0)) (= c_0 c_0) (= c_0 c_0) (not (p10 c_0 c_0)) )(or (p14 c_0 c_0 c_0) (not (p3 c_0)) (not (p10 c_0 c_1)) (not (p10 c_0 c_0)) (not (p9 c_1)) (not (p10 c_0 c_1)) (not (p10 c_0 c_0)) (= c_1 c_0) (not (p3 c_0)) (not (p9 c_0)) (not (p10 c_0 c_0)) (= c_0 c_0) (not (p3 c_0)) (= c_0 c_0) (= c_0 c_0) (not (p10 c_0 c_1)) )(or (p14 c_0 c_0 c_0) (not (p3 c_0)) (not (p10 c_0 c_1)) (not (p10 c_0 c_1)) (not (p9 c_1)) (not (p10 c_0 c_1)) (not (p10 c_0 c_1)) (= c_1 c_1) (not (p3 c_0)) (not (p9 c_1)) (not (p10 c_0 c_1)) (= c_0 c_0) (not (p3 c_0)) (= c_0 c_0) (= c_0 c_0) (not (p10 c_0 c_1)) )(or (p14 c_0 c_0 c_0) (not (p3 c_0)) (not (p10 c_0 c_1)) (not (p10 c_0 c_2)) (not (p9 c_1)) (not (p10 c_0 c_1)) (not (p10 c_0 c_2)) (= c_1 c_2) (not (p3 c_0)) (not (p9 c_2)) (not (p10 c_0 c_2)) (= c_0 c_0) (not (p3 c_0)) (= c_0 c_0) (= c_0 c_0) (not (p10 c_0 c_1)) )(or (p14 c_0 c_0 c_0) (not (p3 c_0)) (not (p10 c_0 c_2)) (not (p10 c_0 c_0)) (not (p9 c_2)) (not (p10 c_0 c_2)) (not (p10 c_0 c_0)) (= c_2 c_0) (not (p3 c_0)) (not (p9 c_0)) (not (p10 c_0 c_0)) (= c_0 c_0) (not (p3 c_0)) (= c_0 c_0) (= c_0 c_0) (not (p10 c_0 c_2)) )(or (p14 c_0 c_0 c_0) (not (p3 c_0)) (not (p10 c_0 c_2)) (not (p10 c_0 c_1)) (not (p9 c_2)) (not (p10 c_0 c_2)) (not (p10 c_0 c_1)) (= c_2 c_1) (not (p3 c_0)) (not (p9 c_1)) (not (p10 c_0 c_1)) (= c_0 c_0) (not (p3 c_0)) (= c_0 c_0) (= c_0 c_0) (not (p10 c_0 c_2)) )(or (p14 c_0 c_0 c_0) (not (p3 c_0)) (not (p10 c_0 c_2)) (not (p10 c_0 c_2)) (not (p9 c_2)) (not (p10 c_0 c_2)) (not (p10 c_0 c_2)) (= c_2 c_2) (not (p3 c_0)) (not (p9 c_2)) (not (p10 c_0 c_2)) (= c_0 c_0) (not (p3 c_0)) (= c_0 c_0) (= c_0 c_0) (not (p10 c_0 c_2)) )(or (p14 c_0 c_0 c_1) (not (p3 c_0)) (not (p10 c_1 c_0)) (not (p10 c_0 c_0)) (not (p9 c_0)) (not (p10 c_0 c_0)) (not (p10 c_1 c_0)) (= c_0 c_0) (not (p3 c_1)) (not (p9 c_0)) (not (p10 c_0 c_0)) (= c_0 c_1) (not (p3 c_0)) (= c_0 c_1) (= c_0 c_0) (not (p10 c_0 c_0)) )(or (p14 c_0 c_0 c_1) (not (p3 c_0)) (not (p10 c_1 c_0)) (not (p10 c_0 c_1)) (not (p9 c_0)) (not (p10 c_0 c_0)) (not (p10 c_1 c_1)) (= c_0 c_1) (not (p3 c_1)) (not (p9 c_1)) (not (p10 c_0 c_1)) (= c_0 c_1) (not (p3 c_0)) (= c_0 c_1) (= c_0 c_0) (not (p10 c_0 c_0)) )(or (p14 c_0 c_0 c_1) (not (p3 c_0)) (not (p10 c_1 c_0)) (not (p10 c_0 c_2)) (not (p9 c_0)) (not (p10 c_0 c_0)) (not (p10 c_1 c_2)) (= c_0 c_2) (not (p3 c_1)) (not (p9 c_2)) (not (p10 c_0 c_2)) (= c_0 c_1) (not (p3 c_0)) (= c_0 c_1) (= c_0 c_0) (not (p10 c_0 c_0)) )(or (p14 c_0 c_0 c_1) (not (p3 c_0)) (not (p10 c_1 c_1)) (not (p10 c_0 c_0)) (not (p9 c_1)) (not (p10 c_0 c_1)) (not (p10 c_1 c_0)) (= c_1 c_0) (not (p3 c_1)) (not (p9 c_0)) (not (p10 c_0 c_0)) (= c_0 c_1) (not (p3 c_0)) (= c_0 c_1) (= c_0 c_0) (not (p10 c_0 c_1)) )(or (p14 c_0 c_0 c_1) (not (p3 c_0)) (not (p10 c_1 c_1)) (not (p10 c_0 c_1)) (not (p9 c_1)) (not (p10 c_0 c_1)) (not (p10 c_1 c_1)) (= c_1 c_1) (not (p3 c_1)) (not (p9 c_1)) (not (p10 c_0 c_1)) (= c_0 c_1) (not (p3 c_0)) (= c_0 c_1) (= c_0 c_0) (not (p10 c_0 c_1)) )(or (p14 c_0 c_0 c_1) (not (p3 c_0)) (not (p10 c_1 c_1)) (not (p10 c_0 c_2)) (not (p9 c_1)) (not (p10 c_0 c_1)) (not (p10 c_1 c_2)) (= c_1 c_2) (not (p3 c_1)) (not (p9 c_2)) (not (p10 c_0 c_2)) (= c_0 c_1) (not (p3 c_0)) (= c_0 c_1) (= c_0 c_0) (not (p10 c_0 c_1)) )(or (p14 c_0 c_0 c_1) (not (p3 c_0)) (not (p10 c_1 c_2)) (not (p10 c_0 c_0)) (not (p9 c_2)) (not (p10 c_0 c_2)) (not (p10 c_1 c_0)) (= c_2 c_0) (not (p3 c_1)) (not (p9 c_0)) (not (p10 c_0 c_0)) (= c_0 c_1) (not (p3 c_0)) (= c_0 c_1) (= c_0 c_0) (not (p10 c_0 c_2)) )(or (p14 c_0 c_0 c_1) (not (p3 c_0)) (not (p10 c_1 c_2)) (not (p10 c_0 c_1)) (not (p9 c_2)) (not (p10 c_0 c_2)) (not (p10 c_1 c_1)) (= c_2 c_1) (not (p3 c_1)) (not (p9 c_1)) (not (p10 c_0 c_1)) (= c_0 c_1) (not (p3 c_0)) (= c_0 c_1) (= c_0 c_0) (not (p10 c_0 c_2)) )(or (p14 c_0 c_0 c_1) (not (p3 c_0)) (not (p10 c_1 c_2)) (not (p10 c_0 c_2)) (not (p9 c_2)) (not (p10 c_0 c_2)) (not (p10 c_1 c_2)) (= c_2 c_2) (not (p3 c_1)) (not (p9 c_2)) (not (p10 c_0 c_2)) (= c_0 c_1) (not (p3 c_0)) (= c_0 c_1) (= c_0 c_0) (not (p10 c_0 c_2)) )(or (p14 c_0 c_0 c_2) (not (p3 c_0)) (not (p10 c_2 c_0)) (not (p10 c_0 c_0)) (not (p9 c_0)) (not (p10 c_0 c_0)) (not (p10 c_2 c_0)) (= c_0 c_0) (not (p3 c_2)) (not (p9 c_0)) (not (p10 c_0 c_0)) (= c_0 c_2) (not (p3 c_0)) (= c_0 c_2) (= c_0 c_0) (not (p10 c_0 c_0)) )(or (p14 c_0 c_0 c_2) (not (p3 c_0)) (not (p10 c_2 c_0)) (not (p10 c_0 c_1)) (not (p9 c_0)) (not (p10 c_0 c_0)) (not (p10 c_2 c_1)) (= c_0 c_1) (not (p3 c_2)) (not (p9 c_1)) (not (p10 c_0 c_1)) (= c_0 c_2) (not (p3 c_0)) (= c_0 c_2) (= c_0 c_0) (not (p10 c_0 c_0)) )(or (p14 c_0 c_0 c_2) (not (p3 c_0)) (not (p10 c_2 c_0)) (not (p10 c_0 c_2)) (not (p9 c_0)) (not (p10 c_0 c_0)) (not (p10 c_2 c_2)) (= c_0 c_2) (not (p3 c_2)) (not (p9 c_2)) (not (p10 c_0 c_2)) (= c_0 c_2) (not (p3 c_0)) (= c_0 c_2) (= c_0 c_0) (not (p10 c_0 c_0)) )(or (p14 c_0 c_0 c_2) (not (p3 c_0)) (not (p10 c_2 c_1)) (not (p10 c_0 c_0)) (not (p9 c_1)) (not (p10 c_0 c_1)) (not (p10 c_2 c_0)) (= c_1 c_0) (not (p3 c_2)) (not (p9 c_0)) (not (p10 c_0 c_0)) (= c_0 c_2) (not (p3 c_0)) (= c_0 c_2) (= c_0 c_0) (not (p10 c_0 c_1)) )(or (p14 c_0 c_0 c_2) (not (p3 c_0)) (not (p10 c_2 c_1)) (not (p10 c_0 c_1)) (not (p9 c_1)) (not (p10 c_0 c_1)) (not (p10 c_2 c_1)) (= c_1 c_1) (not (p3 c_2)) (not (p9 c_1)) (not (p10 c_0 c_1)) (= c_0 c_2) (not (p3 c_0)) (= c_0 c_2) (= c_0 c_0) (not (p10 c_0 c_1)) )(or (p14 c_0 c_0 c_2) (not (p3 c_0)) (not (p10 c_2 c_1)) (not (p10 c_0 c_2)) (not (p9 c_1)) (not (p10 c_0 c_1)) (not (p10 c_2 c_2)) (= c_1 c_2) (not (p3 c_2)) (not (p9 c_2)) (not (p10 c_0 c_2)) (= c_0 c_2) (not (p3 c_0)) (= c_0 c_2) (= c_0 c_0) (not (p10 c_0 c_1)) )(or (p14 c_0 c_0 c_2) (not (p3 c_0)) (not (p10 c_2 c_2)) (not (p10 c_0 c_0)) (not (p9 c_2)) (not (p10 c_0 c_2)) (not (p10 c_2 c_0)) (= c_2 c_0) (not (p3 c_2)) (not (p9 c_0)) (not (p10 c_0 c_0)) (= c_0 c_2) (not (p3 c_0)) (= c_0 c_2) (= c_0 c_0) (not (p10 c_0 c_2)) )(or (p14 c_0 c_0 c_2) (not (p3 c_0)) (not (p10 c_2 c_2)) (not (p10 c_0 c_1)) (not (p9 c_2)) (not (p10 c_0 c_2)) (not (p10 c_2 c_1)) (= c_2 c_1) (not (p3 c_2)) (not (p9 c_1)) (not (p10 c_0 c_1)) (= c_0 c_2) (not (p3 c_0)) (= c_0 c_2) (= c_0 c_0) (not (p10 c_0 c_2)) )(or (p14 c_0 c_0 c_2) (not (p3 c_0)) (not (p10 c_2 c_2)) (not (p10 c_0 c_2)) (not (p9 c_2)) (not (p10 c_0 c_2)) (not (p10 c_2 c_2)) (= c_2 c_2) (not (p3 c_2)) (not (p9 c_2)) (not (p10 c_0 c_2)) (= c_0 c_2) (not (p3 c_0)) (= c_0 c_2) (= c_0 c_0) (not (p10 c_0 c_2)) )(or (p14 c_0 c_1 c_0) (not (p3 c_1)) (not (p10 c_0 c_0)) (not (p10 c_0 c_0)) (not (p9 c_0)) (not (p10 c_0 c_0)) (not (p10 c_0 c_0)) (= c_0 c_0) (not (p3 c_0)) (not (p9 c_0)) (not (p10 c_1 c_0)) (= c_1 c_0) (not (p3 c_0)) (= c_0 c_0) (= c_0 c_1) (not (p10 c_1 c_0)) )(or (p14 c_0 c_1 c_0) (not (p3 c_1)) (not (p10 c_0 c_0)) (not (p10 c_0 c_1)) (not (p9 c_0)) (not (p10 c_0 c_0)) (not (p10 c_0 c_1)) (= c_0 c_1) (not (p3 c_0)) (not (p9 c_1)) (not (p10 c_1 c_1)) (= c_1 c_0) (not (p3 c_0)) (= c_0 c_0) (= c_0 c_1) (not (p10 c_1 c_0)) )(or (p14 c_0 c_1 c_0) (not (p3 c_1)) (not (p10 c_0 c_0)) (not (p10 c_0 c_2)) (not (p9 c_0)) (not (p10 c_0 c_0)) (not (p10 c_0 c_2)) (= c_0 c_2) (not (p3 c_0)) (not (p9 c_2)) (not (p10 c_1 c_2)) (= c_1 c_0) (not (p3 c_0)) (= c_0 c_0) (= c_0 c_1) (not (p10 c_1 c_0)) )(or (p14 c_0 c_1 c_0) (not (p3 c_1)) (not (p10 c_0 c_1)) (not (p10 c_0 c_0)) (not (p9 c_1)) (not (p10 c_0 c_1)) (not (p10 c_0 c_0)) (= c_1 c_0) (not (p3 c_0)) (not (p9 c_0)) (not (p10 c_1 c_0)) (= c_1 c_0) (not (p3 c_0)) (= c_0 c_0) (= c_0 c_1) (not (p10 c_1 c_1)) )(or (p14 c_0 c_1 c_0) (not (p3 c_1)) (not (p10 c_0 c_1)) (not (p10 c_0 c_1)) (not (p9 c_1)) (not (p10 c_0 c_1)) (not (p10 c_0 c_1)) (= c_1 c_1) (not (p3 c_0)) (not (p9 c_1)) (not (p10 c_1 c_1)) (= c_1 c_0) (not (p3 c_0)) (= c_0 c_0) (= c_0 c_1) (not (p10 c_1 c_1)) )(or (p14 c_0 c_1 c_0) (not (p3 c_1)) (not (p10 c_0 c_1)) (not (p10 c_0 c_2)) (not (p9 c_1)) (not (p10 c_0 c_1)) (not (p10 c_0 c_2)) (= c_1 c_2) (not (p3 c_0)) (not (p9 c_2)) (not (p10 c_1 c_2)) (= c_1 c_0) (not (p3 c_0)) (= c_0 c_0) (= c_0 c_1) (not (p10 c_1 c_1)) )(or (p14 c_0 c_1 c_0) (not (p3 c_1)) (not (p10 c_0 c_2)) (not (p10 c_0 c_0)) (not (p9 c_2)) (not (p10 c_0 c_2)) (not (p10 c_0 c_0)) (= c_2 c_0) (not (p3 c_0)) (not (p9 c_0)) (not (p10 c_1 c_0)) (= c_1 c_0) (not (p3 c_0)) (= c_0 c_0) (= c_0 c_1) (not (p10 c_1 c_2)) )(or (p14 c_0 c_1 c_0) (not (p3 c_1)) (not (p10 c_0 c_2)) (not (p10 c_0 c_1)) (not (p9 c_2)) (not (p10 c_0 c_2)) (not (p10 c_0 c_1)) (= c_2 c_1) (not (p3 c_0)) (not (p9 c_1)) (not (p10 c_1 c_1)) (= c_1 c_0) (not (p3 c_0)) (= c_0 c_0) (= c_0 c_1) (not (p10 c_1 c_2)) )(or (p14 c_0 c_1 c_0) (not (p3 c_1)) (not (p10 c_0 c_2)) (not (p10 c_0 c_2)) (not (p9 c_2)) (not (p10 c_0 c_2)) (not (p10 c_0 c_2)) (= c_2 c_2) (not (p3 c_0)) (not (p9 c_2)) (not (p10 c_1 c_2)) (= c_1 c_0) (not (p3 c_0)) (= c_0 c_0) (= c_0 c_1) (not (p10 c_1 c_2)) )(or (p14 c_0 c_1 c_1) (not (p3 c_1)) (not (p10 c_1 c_0)) (not (p10 c_0 c_0)) (not (p9 c_0)) (not (p10 c_0 c_0)) (not (p10 c_1 c_0)) (= c_0 c_0) (not (p3 c_1)) (not (p9 c_0)) (not (p10 c_1 c_0)) (= c_1 c_1) (not (p3 c_0)) (= c_0 c_1) (= c_0 c_1) (not (p10 c_1 c_0)) )(or (p14 c_0 c_1 c_1) (not (p3 c_1)) (not (p10 c_1 c_0)) (not (p10 c_0 c_1)) (not (p9 c_0)) (not (p10 c_0 c_0)) (not (p10 c_1 c_1)) (= c_0 c_1) (not (p3 c_1)) (not (p9 c_1)) (not (p10 c_1 c_1)) (= c_1 c_1) (not (p3 c_0)) (= c_0 c_1) (= c_0 c_1) (not (p10 c_1 c_0)) )(or (p14 c_0 c_1 c_1) (not (p3 c_1)) (not (p10 c_1 c_0)) (not (p10 c_0 c_2)) (not (p9 c_0)) (not (p10 c_0 c_0)) (not (p10 c_1 c_2)) (= c_0 c_2) (not (p3 c_1)) (not (p9 c_2)) (not (p10 c_1 c_2)) (= c_1 c_1) (not (p3 c_0)) (= c_0 c_1) (= c_0 c_1) (not (p10 c_1 c_0)) )(or (p14 c_0 c_1 c_1) (not (p3 c_1)) (not (p10 c_1 c_1)) (not (p10 c_0 c_0)) (not (p9 c_1)) (not (p10 c_0 c_1)) (not (p10 c_1 c_0)) (= c_1 c_0) (not (p3 c_1)) (not (p9 c_0)) (not (p10 c_1 c_0)) (= c_1 c_1) (not (p3 c_0)) (= c_0 c_1) (= c_0 c_1) (not (p10 c_1 c_1)) )(or (p14 c_0 c_1 c_1) (not (p3 c_1)) (not (p10 c_1 c_1)) (not (p10 c_0 c_1)) (not (p9 c_1)) (not (p10 c_0 c_1)) (not (p10 c_1 c_1)) (= c_1 c_1) (not (p3 c_1)) (not (p9 c_1)) (not (p10 c_1 c_1)) (= c_1 c_1) (not (p3 c_0)) (= c_0 c_1) (= c_0 c_1) (not (p10 c_1 c_1)) )(or (p14 c_0 c_1 c_1) (not (p3 c_1)) (not (p10 c_1 c_1)) (not (p10 c_0 c_2)) (not (p9 c_1)) (not (p10 c_0 c_1)) (not (p10 c_1 c_2)) (= c_1 c_2) (not (p3 c_1)) (not (p9 c_2)) (not (p10 c_1 c_2)) (= c_1 c_1) (not (p3 c_0)) (= c_0 c_1) (= c_0 c_1) (not (p10 c_1 c_1)) )(or (p14 c_0 c_1 c_1) (not (p3 c_1)) (not (p10 c_1 c_2)) (not (p10 c_0 c_0)) (not (p9 c_2)) (not (p10 c_0 c_2)) (not (p10 c_1 c_0)) (= c_2 c_0) (not (p3 c_1)) (not (p9 c_0)) (not (p10 c_1 c_0)) (= c_1 c_1) (not (p3 c_0)) (= c_0 c_1) (= c_0 c_1) (not (p10 c_1 c_2)) )(or (p14 c_0 c_1 c_1) (not (p3 c_1)) (not (p10 c_1 c_2)) (not (p10 c_0 c_1)) (not (p9 c_2)) (not (p10 c_0 c_2)) (not (p10 c_1 c_1)) (= c_2 c_1) (not (p3 c_1)) (not (p9 c_1)) (not (p10 c_1 c_1)) (= c_1 c_1) (not (p3 c_0)) (= c_0 c_1) (= c_0 c_1) (not (p10 c_1 c_2)) )(or (p14 c_0 c_1 c_1) (not (p3 c_1)) (not (p10 c_1 c_2)) (not (p10 c_0 c_2)) (not (p9 c_2)) (not (p10 c_0 c_2)) (not (p10 c_1 c_2)) (= c_2 c_2) (not (p3 c_1)) (not (p9 c_2)) (not (p10 c_1 c_2)) (= c_1 c_1) (not (p3 c_0)) (= c_0 c_1) (= c_0 c_1) (not (p10 c_1 c_2)) )(or (p14 c_0 c_1 c_2) (not (p3 c_1)) (not (p10 c_2 c_0)) (not (p10 c_0 c_0)) (not (p9 c_0)) (not (p10 c_0 c_0)) (not (p10 c_2 c_0)) (= c_0 c_0) (not (p3 c_2)) (not (p9 c_0)) (not (p10 c_1 c_0)) (= c_1 c_2) (not (p3 c_0)) (= c_0 c_2) (= c_0 c_1) (not (p10 c_1 c_0)) )(or (p14 c_0 c_1 c_2) (not (p3 c_1)) (not (p10 c_2 c_0)) (not (p10 c_0 c_1)) (not (p9 c_0)) (not (p10 c_0 c_0)) (not (p10 c_2 c_1)) (= c_0 c_1) (not (p3 c_2)) (not (p9 c_1)) (not (p10 c_1 c_1)) (= c_1 c_2) (not (p3 c_0)) (= c_0 c_2) (= c_0 c_1) (not (p10 c_1 c_0)) )(or (p14 c_0 c_1 c_2) (not (p3 c_1)) (not (p10 c_2 c_0)) (not (p10 c_0 c_2)) (not (p9 c_0)) (not (p10 c_0 c_0)) (not (p10 c_2 c_2)) (= c_0 c_2) (not (p3 c_2)) (not (p9 c_2)) (not (p10 c_1 c_2)) (= c_1 c_2) (not (p3 c_0)) (= c_0 c_2) (= c_0 c_1) (not (p10 c_1 c_0)) )(or (p14 c_0 c_1 c_2) (not (p3 c_1)) (not (p10 c_2 c_1)) (not (p10 c_0 c_0)) (not (p9 c_1)) (not (p10 c_0 c_1)) (not (p10 c_2 c_0)) (= c_1 c_0) (not (p3 c_2)) (not (p9 c_0)) (not (p10 c_1 c_0)) (= c_1 c_2) (not (p3 c_0)) (= c_0 c_2) (= c_0 c_1) (not (p10 c_1 c_1)) )(or (p14 c_0 c_1 c_2) (not (p3 c_1)) (not (p10 c_2 c_1)) (not (p10 c_0 c_1)) (not (p9 c_1)) (not (p10 c_0 c_1)) (not (p10 c_2 c_1)) (= c_1 c_1) (not (p3 c_2)) (not (p9 c_1)) (not (p10 c_1 c_1)) (= c_1 c_2) (not (p3 c_0)) (= c_0 c_2) (= c_0 c_1) (not (p10 c_1 c_1)) )(or (p14 c_0 c_1 c_2) (not (p3 c_1)) (not (p10 c_2 c_1)) (not (p10 c_0 c_2)) (not (p9 c_1)) (not (p10 c_0 c_1)) (not (p10 c_2 c_2)) (= c_1 c_2) (not (p3 c_2)) (not (p9 c_2)) (not (p10 c_1 c_2)) (= c_1 c_2) (not (p3 c_0)) (= c_0 c_2) (= c_0 c_1) (not (p10 c_1 c_1)) )(or (p14 c_0 c_1 c_2) (not (p3 c_1)) (not (p10 c_2 c_2)) (not (p10 c_0 c_0)) (not (p9 c_2)) (not (p10 c_0 c_2)) (not (p10 c_2 c_0)) (= c_2 c_0) (not (p3 c_2)) (not (p9 c_0)) (not (p10 c_1 c_0)) (= c_1 c_2) (not (p3 c_0)) (= c_0 c_2) (= c_0 c_1) (not (p10 c_1 c_2)) )(or (p14 c_0 c_1 c_2) (not (p3 c_1)) (not (p10 c_2 c_2)) (not (p10 c_0 c_1)) (not (p9 c_2)) (not (p10 c_0 c_2)) (not (p10 c_2 c_1)) (= c_2 c_1) (not (p3 c_2)) (not (p9 c_1)) (not (p10 c_1 c_1)) (= c_1 c_2) (not (p3 c_0)) (= c_0 c_2) (= c_0 c_1) (not (p10 c_1 c_2)) )(or (p14 c_0 c_1 c_2) (not (p3 c_1)) (not (p10 c_2 c_2)) (not (p10 c_0 c_2)) (not (p9 c_2)) (not (p10 c_0 c_2)) (not (p10 c_2 c_2)) (= c_2 c_2) (not (p3 c_2)) (not (p9 c_2)) (not (p10 c_1 c_2)) (= c_1 c_2) (not (p3 c_0)) (= c_0 c_2) (= c_0 c_1) (not (p10 c_1 c_2)) )(or (p14 c_0 c_2 c_0) (not (p3 c_2)) (not (p10 c_0 c_0)) (not (p10 c_0 c_0)) (not (p9 c_0)) (not (p10 c_0 c_0)) (not (p10 c_0 c_0)) (= c_0 c_0) (not (p3 c_0)) (not (p9 c_0)) (not (p10 c_2 c_0)) (= c_2 c_0) (not (p3 c_0)) (= c_0 c_0) (= c_0 c_2) (not (p10 c_2 c_0)) )(or (p14 c_0 c_2 c_0) (not (p3 c_2)) (not (p10 c_0 c_0)) (not (p10 c_0 c_1)) (not (p9 c_0)) (not (p10 c_0 c_0)) (not (p10 c_0 c_1)) (= c_0 c_1) (not (p3 c_0)) (not (p9 c_1)) (not (p10 c_2 c_1)) (= c_2 c_0) (not (p3 c_0)) (= c_0 c_0) (= c_0 c_2) (not (p10 c_2 c_0)) )(or (p14 c_0 c_2 c_0) (not (p3 c_2)) (not (p10 c_0 c_0)) (not (p10 c_0 c_2)) (not (p9 c_0)) (not (p10 c_0 c_0)) (not (p10 c_0 c_2)) (= c_0 c_2) (not (p3 c_0)) (not (p9 c_2)) (not (p10 c_2 c_2)) (= c_2 c_0) (not (p3 c_0)) (= c_0 c_0) (= c_0 c_2) (not (p10 c_2 c_0)) )(or (p14 c_0 c_2 c_0) (not (p3 c_2)) (not (p10 c_0 c_1)) (not (p10 c_0 c_0)) (not (p9 c_1)) (not (p10 c_0 c_1)) (not (p10 c_0 c_0)) (= c_1 c_0) (not (p3 c_0)) (not (p9 c_0)) (not (p10 c_2 c_0)) (= c_2 c_0) (not (p3 c_0)) (= c_0 c_0) (= c_0 c_2) (not (p10 c_2 c_1)) )(or (p14 c_0 c_2 c_0) (not (p3 c_2)) (not (p10 c_0 c_1)) (not (p10 c_0 c_1)) (not (p9 c_1)) (not (p10 c_0 c_1)) (not (p10 c_0 c_1)) (= c_1 c_1) (not (p3 c_0)) (not (p9 c_1)) (not (p10 c_2 c_1)) (= c_2 c_0) (not (p3 c_0)) (= c_0 c_0) (= c_0 c_2) (not (p10 c_2 c_1)) )(or (p14 c_0 c_2 c_0) (not (p3 c_2)) (not (p10 c_0 c_1)) (not (p10 c_0 c_2)) (not (p9 c_1)) (not (p10 c_0 c_1)) (not (p10 c_0 c_2)) (= c_1 c_2) (not (p3 c_0)) (not (p9 c_2)) (not (p10 c_2 c_2)) (= c_2 c_0) (not (p3 c_0)) (= c_0 c_0) (= c_0 c_2) (not (p10 c_2 c_1)) )(or (p14 c_0 c_2 c_0) (not (p3 c_2)) (not (p10 c_0 c_2)) (not (p10 c_0 c_0)) (not (p9 c_2)) (not (p10 c_0 c_2)) (not (p10 c_0 c_0)) (= c_2 c_0) (not (p3 c_0)) (not (p9 c_0)) (not (p10 c_2 c_0)) (= c_2 c_0) (not (p3 c_0)) (= c_0 c_0) (= c_0 c_2) (not (p10 c_2 c_2)) )(or (p14 c_0 c_2 c_0) (not (p3 c_2)) (not (p10 c_0 c_2)) (not (p10 c_0 c_1)) (not (p9 c_2)) (not (p10 c_0 c_2)) (not (p10 c_0 c_1)) (= c_2 c_1) (not (p3 c_0)) (not (p9 c_1)) (not (p10 c_2 c_1)) (= c_2 c_0) (not (p3 c_0)) (= c_0 c_0) (= c_0 c_2) (not (p10 c_2 c_2)) )(or (p14 c_0 c_2 c_0) (not (p3 c_2)) (not (p10 c_0 c_2)) (not (p10 c_0 c_2)) (not (p9 c_2)) (not (p10 c_0 c_2)) (not (p10 c_0 c_2)) (= c_2 c_2) (not (p3 c_0)) (not (p9 c_2)) (not (p10 c_2 c_2)) (= c_2 c_0) (not (p3 c_0)) (= c_0 c_0) (= c_0 c_2) (not (p10 c_2 c_2)) )(or (p14 c_0 c_2 c_1) (not (p3 c_2)) (not (p10 c_1 c_0)) (not (p10 c_0 c_0)) (not (p9 c_0)) (not (p10 c_0 c_0)) (not (p10 c_1 c_0)) (= c_0 c_0) (not (p3 c_1)) (not (p9 c_0)) (not (p10 c_2 c_0)) (= c_2 c_1) (not (p3 c_0)) (= c_0 c_1) (= c_0 c_2) (not (p10 c_2 c_0)) )(or (p14 c_0 c_2 c_1) (not (p3 c_2)) (not (p10 c_1 c_0)) (not (p10 c_0 c_1)) (not (p9 c_0)) (not (p10 c_0 c_0)) (not (p10 c_1 c_1)) (= c_0 c_1) (not (p3 c_1)) (not (p9 c_1)) (not (p10 c_2 c_1)) (= c_2 c_1) (not (p3 c_0)) (= c_0 c_1) (= c_0 c_2) (not (p10 c_2 c_0)) )(or (p14 c_0 c_2 c_1) (not (p3 c_2)) (not (p10 c_1 c_0)) (not (p10 c_0 c_2)) (not (p9 c_0)) (not (p10 c_0 c_0)) (not (p10 c_1 c_2)) (= c_0 c_2) (not (p3 c_1)) (not (p9 c_2)) (not (p10 c_2 c_2)) (= c_2 c_1) (not (p3 c_0)) (= c_0 c_1) (= c_0 c_2) (not (p10 c_2 c_0)) )(or (p14 c_0 c_2 c_1) (not (p3 c_2)) (not (p10 c_1 c_1)) (not (p10 c_0 c_0)) (not (p9 c_1)) (not (p10 c_0 c_1)) (not (p10 c_1 c_0)) (= c_1 c_0) (not (p3 c_1)) (not (p9 c_0)) (not (p10 c_2 c_0)) (= c_2 c_1) (not (p3 c_0)) (= c_0 c_1) (= c_0 c_2) (not (p10 c_2 c_1)) )(or (p14 c_0 c_2 c_1) (not (p3 c_2)) (not (p10 c_1 c_1)) (not (p10 c_0 c_1)) (not (p9 c_1)) (not (p10 c_0 c_1)) (not (p10 c_1 c_1)) (= c_1 c_1) (not (p3 c_1)) (not (p9 c_1)) (not (p10 c_2 c_1)) (= c_2 c_1) (not (p3 c_0)) (= c_0 c_1) (= c_0 c_2) (not (p10 c_2 c_1)) )(or (p14 c_0 c_2 c_1) (not (p3 c_2)) (not (p10 c_1 c_1)) (not (p10 c_0 c_2)) (not (p9 c_1)) (not (p10 c_0 c_1)) (not (p10 c_1 c_2)) (= c_1 c_2) (not (p3 c_1)) (not (p9 c_2)) (not (p10 c_2 c_2)) (= c_2 c_1) (not (p3 c_0)) (= c_0 c_1) (= c_0 c_2) (not (p10 c_2 c_1)) )(or (p14 c_0 c_2 c_1) (not (p3 c_2)) (not (p10 c_1 c_2)) (not (p10 c_0 c_0)) (not (p9 c_2)) (not (p10 c_0 c_2)) (not (p10 c_1 c_0)) (= c_2 c_0) (not (p3 c_1)) (not (p9 c_0)) (not (p10 c_2 c_0)) (= c_2 c_1) (not (p3 c_0)) (= c_0 c_1) (= c_0 c_2) (not (p10 c_2 c_2)) )(or (p14 c_0 c_2 c_1) (not (p3 c_2)) (not (p10 c_1 c_2)) (not (p10 c_0 c_1)) (not (p9 c_2)) (not (p10 c_0 c_2)) (not (p10 c_1 c_1)) (= c_2 c_1) (not (p3 c_1)) (not (p9 c_1)) (not (p10 c_2 c_1)) (= c_2 c_1) (not (p3 c_0)) (= c_0 c_1) (= c_0 c_2) (not (p10 c_2 c_2)) )(or (p14 c_0 c_2 c_1) (not (p3 c_2)) (not (p10 c_1 c_2)) (not (p10 c_0 c_2)) (not (p9 c_2)) (not (p10 c_0 c_2)) (not (p10 c_1 c_2)) (= c_2 c_2) (not (p3 c_1)) (not (p9 c_2)) (not (p10 c_2 c_2)) (= c_2 c_1) (not (p3 c_0)) (= c_0 c_1) (= c_0 c_2) (not (p10 c_2 c_2)) )(or (p14 c_0 c_2 c_2) (not (p3 c_2)) (not (p10 c_2 c_0)) (not (p10 c_0 c_0)) (not (p9 c_0)) (not (p10 c_0 c_0)) (not (p10 c_2 c_0)) (= c_0 c_0) (not (p3 c_2)) (not (p9 c_0)) (not (p10 c_2 c_0)) (= c_2 c_2) (not (p3 c_0)) (= c_0 c_2) (= c_0 c_2) (not (p10 c_2 c_0)) )(or (p14 c_0 c_2 c_2) (not (p3 c_2)) (not (p10 c_2 c_0)) (not (p10 c_0 c_1)) (not (p9 c_0)) (not (p10 c_0 c_0)) (not (p10 c_2 c_1)) (= c_0 c_1) (not (p3 c_2)) (not (p9 c_1)) (not (p10 c_2 c_1)) (= c_2 c_2) (not (p3 c_0)) (= c_0 c_2) (= c_0 c_2) (not (p10 c_2 c_0)) )(or (p14 c_0 c_2 c_2) (not (p3 c_2)) (not (p10 c_2 c_0)) (not (p10 c_0 c_2)) (not (p9 c_0)) (not (p10 c_0 c_0)) (not (p10 c_2 c_2)) (= c_0 c_2) (not (p3 c_2)) (not (p9 c_2)) (not (p10 c_2 c_2)) (= c_2 c_2) (not (p3 c_0)) (= c_0 c_2) (= c_0 c_2) (not (p10 c_2 c_0)) )(or (p14 c_0 c_2 c_2) (not (p3 c_2)) (not (p10 c_2 c_1)) (not (p10 c_0 c_0)) (not (p9 c_1)) (not (p10 c_0 c_1)) (not (p10 c_2 c_0)) (= c_1 c_0) (not (p3 c_2)) (not (p9 c_0)) (not (p10 c_2 c_0)) (= c_2 c_2) (not (p3 c_0)) (= c_0 c_2) (= c_0 c_2) (not (p10 c_2 c_1)) )(or (p14 c_0 c_2 c_2) (not (p3 c_2)) (not (p10 c_2 c_1)) (not (p10 c_0 c_1)) (not (p9 c_1)) (not (p10 c_0 c_1)) (not (p10 c_2 c_1)) (= c_1 c_1) (not (p3 c_2)) (not (p9 c_1)) (not (p10 c_2 c_1)) (= c_2 c_2) (not (p3 c_0)) (= c_0 c_2) (= c_0 c_2) (not (p10 c_2 c_1)) )(or (p14 c_0 c_2 c_2) (not (p3 c_2)) (not (p10 c_2 c_1)) (not (p10 c_0 c_2)) (not (p9 c_1)) (not (p10 c_0 c_1)) (not (p10 c_2 c_2)) (= c_1 c_2) (not (p3 c_2)) (not (p9 c_2)) (not (p10 c_2 c_2)) (= c_2 c_2) (not (p3 c_0)) (= c_0 c_2) (= c_0 c_2) (not (p10 c_2 c_1)) )(or (p14 c_0 c_2 c_2) (not (p3 c_2)) (not (p10 c_2 c_2)) (not (p10 c_0 c_0)) (not (p9 c_2)) (not (p10 c_0 c_2)) (not (p10 c_2 c_0)) (= c_2 c_0) (not (p3 c_2)) (not (p9 c_0)) (not (p10 c_2 c_0)) (= c_2 c_2) (not (p3 c_0)) (= c_0 c_2) (= c_0 c_2) (not (p10 c_2 c_2)) )(or (p14 c_0 c_2 c_2) (not (p3 c_2)) (not (p10 c_2 c_2)) (not (p10 c_0 c_1)) (not (p9 c_2)) (not (p10 c_0 c_2)) (not (p10 c_2 c_1)) (= c_2 c_1) (not (p3 c_2)) (not (p9 c_1)) (not (p10 c_2 c_1)) (= c_2 c_2) (not (p3 c_0)) (= c_0 c_2) (= c_0 c_2) (not (p10 c_2 c_2)) )(or (p14 c_0 c_2 c_2) (not (p3 c_2)) (not (p10 c_2 c_2)) (not (p10 c_0 c_2)) (not (p9 c_2)) (not (p10 c_0 c_2)) (not (p10 c_2 c_2)) (= c_2 c_2) (not (p3 c_2)) (not (p9 c_2)) (not (p10 c_2 c_2)) (= c_2 c_2) (not (p3 c_0)) (= c_0 c_2) (= c_0 c_2) (not (p10 c_2 c_2)) )(or (p14 c_1 c_0 c_0) (not (p3 c_0)) (not (p10 c_0 c_0)) (not (p10 c_1 c_0)) (not (p9 c_0)) (not (p10 c_1 c_0)) (not (p10 c_0 c_0)) (= c_0 c_0) (not (p3 c_0)) (not (p9 c_0)) (not (p10 c_0 c_0)) (= c_0 c_0) (not (p3 c_1)) (= c_1 c_0) (= c_1 c_0) (not (p10 c_0 c_0)) )(or (p14 c_1 c_0 c_0) (not (p3 c_0)) (not (p10 c_0 c_0)) (not (p10 c_1 c_1)) (not (p9 c_0)) (not (p10 c_1 c_0)) (not (p10 c_0 c_1)) (= c_0 c_1) (not (p3 c_0)) (not (p9 c_1)) (not (p10 c_0 c_1)) (= c_0 c_0) (not (p3 c_1)) (= c_1 c_0) (= c_1 c_0) (not (p10 c_0 c_0)) )(or (p14 c_1 c_0 c_0) (not (p3 c_0)) (not (p10 c_0 c_0)) (not (p10 c_1 c_2)) (not (p9 c_0)) (not (p10 c_1 c_0)) (not (p10 c_0 c_2)) (= c_0 c_2) (not (p3 c_0)) (not (p9 c_2)) (not (p10 c_0 c_2)) (= c_0 c_0) (not (p3 c_1)) (= c_1 c_0) (= c_1 c_0) (not (p10 c_0 c_0)) )(or (p14 c_1 c_0 c_0) (not (p3 c_0)) (not (p10 c_0 c_1)) (not (p10 c_1 c_0)) (not (p9 c_1)) (not (p10 c_1 c_1)) (not (p10 c_0 c_0)) (= c_1 c_0) (not (p3 c_0)) (not (p9 c_0)) (not (p10 c_0 c_0)) (= c_0 c_0) (not (p3 c_1)) (= c_1 c_0) (= c_1 c_0) (not (p10 c_0 c_1)) )(or (p14 c_1 c_0 c_0) (not (p3 c_0)) (not (p10 c_0 c_1)) (not (p10 c_1 c_1)) (not (p9 c_1)) (not (p10 c_1 c_1)) (not (p10 c_0 c_1)) (= c_1 c_1) (not (p3 c_0)) (not (p9 c_1)) (not (p10 c_0 c_1)) (= c_0 c_0) (not (p3 c_1)) (= c_1 c_0) (= c_1 c_0) (not (p10 c_0 c_1)) )(or (p14 c_1 c_0 c_0) (not (p3 c_0)) (not (p10 c_0 c_1)) (not (p10 c_1 c_2)) (not (p9 c_1)) (not (p10 c_1 c_1)) (not (p10 c_0 c_2)) (= c_1 c_2) (not (p3 c_0)) (not (p9 c_2)) (not (p10 c_0 c_2)) (= c_0 c_0) (not (p3 c_1)) (= c_1 c_0) (= c_1 c_0) (not (p10 c_0 c_1)) )(or (p14 c_1 c_0 c_0) (not (p3 c_0)) (not (p10 c_0 c_2)) (not (p10 c_1 c_0)) (not (p9 c_2)) (not (p10 c_1 c_2)) (not (p10 c_0 c_0)) (= c_2 c_0) (not (p3 c_0)) (not (p9 c_0)) (not (p10 c_0 c_0)) (= c_0 c_0) (not (p3 c_1)) (= c_1 c_0) (= c_1 c_0) (not (p10 c_0 c_2)) )(or (p14 c_1 c_0 c_0) (not (p3 c_0)) (not (p10 c_0 c_2)) (not (p10 c_1 c_1)) (not (p9 c_2)) (not (p10 c_1 c_2)) (not (p10 c_0 c_1)) (= c_2 c_1) (not (p3 c_0)) (not (p9 c_1)) (not (p10 c_0 c_1)) (= c_0 c_0) (not (p3 c_1)) (= c_1 c_0) (= c_1 c_0) (not (p10 c_0 c_2)) )(or (p14 c_1 c_0 c_0) (not (p3 c_0)) (not (p10 c_0 c_2)) (not (p10 c_1 c_2)) (not (p9 c_2)) (not (p10 c_1 c_2)) (not (p10 c_0 c_2)) (= c_2 c_2) (not (p3 c_0)) (not (p9 c_2)) (not (p10 c_0 c_2)) (= c_0 c_0) (not (p3 c_1)) (= c_1 c_0) (= c_1 c_0) (not (p10 c_0 c_2)) )(or (p14 c_1 c_0 c_1) (not (p3 c_0)) (not (p10 c_1 c_0)) (not (p10 c_1 c_0)) (not (p9 c_0)) (not (p10 c_1 c_0)) (not (p10 c_1 c_0)) (= c_0 c_0) (not (p3 c_1)) (not (p9 c_0)) (not (p10 c_0 c_0)) (= c_0 c_1) (not (p3 c_1)) (= c_1 c_1) (= c_1 c_0) (not (p10 c_0 c_0)) )(or (p14 c_1 c_0 c_1) (not (p3 c_0)) (not (p10 c_1 c_0)) (not (p10 c_1 c_1)) (not (p9 c_0)) (not (p10 c_1 c_0)) (not (p10 c_1 c_1)) (= c_0 c_1) (not (p3 c_1)) (not (p9 c_1)) (not (p10 c_0 c_1)) (= c_0 c_1) (not (p3 c_1)) (= c_1 c_1) (= c_1 c_0) (not (p10 c_0 c_0)) )(or (p14 c_1 c_0 c_1) (not (p3 c_0)) (not (p10 c_1 c_0)) (not (p10 c_1 c_2)) (not (p9 c_0)) (not (p10 c_1 c_0)) (not (p10 c_1 c_2)) (= c_0 c_2) (not (p3 c_1)) (not (p9 c_2)) (not (p10 c_0 c_2)) (= c_0 c_1) (not (p3 c_1)) (= c_1 c_1) (= c_1 c_0) (not (p10 c_0 c_0)) )(or (p14 c_1 c_0 c_1) (not (p3 c_0)) (not (p10 c_1 c_1)) (not (p10 c_1 c_0)) (not (p9 c_1)) (not (p10 c_1 c_1)) (not (p10 c_1 c_0)) (= c_1 c_0) (not (p3 c_1)) (not (p9 c_0)) (not (p10 c_0 c_0)) (= c_0 c_1) (not (p3 c_1)) (= c_1 c_1) (= c_1 c_0) (not (p10 c_0 c_1)) )(or (p14 c_1 c_0 c_1) (not (p3 c_0)) (not (p10 c_1 c_1)) (not (p10 c_1 c_1)) (not (p9 c_1)) (not (p10 c_1 c_1)) (not (p10 c_1 c_1)) (= c_1 c_1) (not (p3 c_1)) (not (p9 c_1)) (not (p10 c_0 c_1)) (= c_0 c_1) (not (p3 c_1)) (= c_1 c_1) (= c_1 c_0) (not (p10 c_0 c_1)) )(or (p14 c_1 c_0 c_1) (not (p3 c_0)) (not (p10 c_1 c_1)) (not (p10 c_1 c_2)) (not (p9 c_1)) (not (p10 c_1 c_1)) (not (p10 c_1 c_2)) (= c_1 c_2) (not (p3 c_1)) (not (p9 c_2)) (not (p10 c_0 c_2)) (= c_0 c_1) (not (p3 c_1)) (= c_1 c_1) (= c_1 c_0) (not (p10 c_0 c_1)) )(or (p14 c_1 c_0 c_1) (not (p3 c_0)) (not (p10 c_1 c_2)) (not (p10 c_1 c_0)) (not (p9 c_2)) (not (p10 c_1 c_2)) (not (p10 c_1 c_0)) (= c_2 c_0) (not (p3 c_1)) (not (p9 c_0)) (not (p10 c_0 c_0)) (= c_0 c_1) (not (p3 c_1)) (= c_1 c_1) (= c_1 c_0) (not (p10 c_0 c_2)) )(or (p14 c_1 c_0 c_1) (not (p3 c_0)) (not (p10 c_1 c_2)) (not (p10 c_1 c_1)) (not (p9 c_2)) (not (p10 c_1 c_2)) (not (p10 c_1 c_1)) (= c_2 c_1) (not (p3 c_1)) (not (p9 c_1)) (not (p10 c_0 c_1)) (= c_0 c_1) (not (p3 c_1)) (= c_1 c_1) (= c_1 c_0) (not (p10 c_0 c_2)) )(or (p14 c_1 c_0 c_1) (not (p3 c_0)) (not (p10 c_1 c_2)) (not (p10 c_1 c_2)) (not (p9 c_2)) (not (p10 c_1 c_2)) (not (p10 c_1 c_2)) (= c_2 c_2) (not (p3 c_1)) (not (p9 c_2)) (not (p10 c_0 c_2)) (= c_0 c_1) (not (p3 c_1)) (= c_1 c_1) (= c_1 c_0) (not (p10 c_0 c_2)) )(or (p14 c_1 c_0 c_2) (not (p3 c_0)) (not (p10 c_2 c_0)) (not (p10 c_1 c_0)) (not (p9 c_0)) (not (p10 c_1 c_0)) (not (p10 c_2 c_0)) (= c_0 c_0) (not (p3 c_2)) (not (p9 c_0)) (not (p10 c_0 c_0)) (= c_0 c_2) (not (p3 c_1)) (= c_1 c_2) (= c_1 c_0) (not (p10 c_0 c_0)) )(or (p14 c_1 c_0 c_2) (not (p3 c_0)) (not (p10 c_2 c_0)) (not (p10 c_1 c_1)) (not (p9 c_0)) (not (p10 c_1 c_0)) (not (p10 c_2 c_1)) (= c_0 c_1) (not (p3 c_2)) (not (p9 c_1)) (not (p10 c_0 c_1)) (= c_0 c_2) (not (p3 c_1)) (= c_1 c_2) (= c_1 c_0) (not (p10 c_0 c_0)) )(or (p14 c_1 c_0 c_2) (not (p3 c_0)) (not (p10 c_2 c_0)) (not (p10 c_1 c_2)) (not (p9 c_0)) (not (p10 c_1 c_0)) (not (p10 c_2 c_2)) (= c_0 c_2) (not (p3 c_2)) (not (p9 c_2)) (not (p10 c_0 c_2)) (= c_0 c_2) (not (p3 c_1)) (= c_1 c_2) (= c_1 c_0) (not (p10 c_0 c_0)) )(or (p14 c_1 c_0 c_2) (not (p3 c_0)) (not (p10 c_2 c_1)) (not (p10 c_1 c_0)) (not (p9 c_1)) (not (p10 c_1 c_1)) (not (p10 c_2 c_0)) (= c_1 c_0) (not (p3 c_2)) (not (p9 c_0)) (not (p10 c_0 c_0)) (= c_0 c_2) (not (p3 c_1)) (= c_1 c_2) (= c_1 c_0) (not (p10 c_0 c_1)) )(or (p14 c_1 c_0 c_2) (not (p3 c_0)) (not (p10 c_2 c_1)) (not (p10 c_1 c_1)) (not (p9 c_1)) (not (p10 c_1 c_1)) (not (p10 c_2 c_1)) (= c_1 c_1) (not (p3 c_2)) (not (p9 c_1)) (not (p10 c_0 c_1)) (= c_0 c_2) (not (p3 c_1)) (= c_1 c_2) (= c_1 c_0) (not (p10 c_0 c_1)) )(or (p14 c_1 c_0 c_2) (not (p3 c_0)) (not (p10 c_2 c_1)) (not (p10 c_1 c_2)) (not (p9 c_1)) (not (p10 c_1 c_1)) (not (p10 c_2 c_2)) (= c_1 c_2) (not (p3 c_2)) (not (p9 c_2)) (not (p10 c_0 c_2)) (= c_0 c_2) (not (p3 c_1)) (= c_1 c_2) (= c_1 c_0) (not (p10 c_0 c_1)) )(or (p14 c_1 c_0 c_2) (not (p3 c_0)) (not (p10 c_2 c_2)) (not (p10 c_1 c_0)) (not (p9 c_2)) (not (p10 c_1 c_2)) (not (p10 c_2 c_0)) (= c_2 c_0) (not (p3 c_2)) (not (p9 c_0)) (not (p10 c_0 c_0)) (= c_0 c_2) (not (p3 c_1)) (= c_1 c_2) (= c_1 c_0) (not (p10 c_0 c_2)) )(or (p14 c_1 c_0 c_2) (not (p3 c_0)) (not (p10 c_2 c_2)) (not (p10 c_1 c_1)) (not (p9 c_2)) (not (p10 c_1 c_2)) (not (p10 c_2 c_1)) (= c_2 c_1) (not (p3 c_2)) (not (p9 c_1)) (not (p10 c_0 c_1)) (= c_0 c_2) (not (p3 c_1)) (= c_1 c_2) (= c_1 c_0) (not (p10 c_0 c_2)) )(or (p14 c_1 c_0 c_2) (not (p3 c_0)) (not (p10 c_2 c_2)) (not (p10 c_1 c_2)) (not (p9 c_2)) (not (p10 c_1 c_2)) (not (p10 c_2 c_2)) (= c_2 c_2) (not (p3 c_2)) (not (p9 c_2)) (not (p10 c_0 c_2)) (= c_0 c_2) (not (p3 c_1)) (= c_1 c_2) (= c_1 c_0) (not (p10 c_0 c_2)) )(or (p14 c_1 c_1 c_0) (not (p3 c_1)) (not (p10 c_0 c_0)) (not (p10 c_1 c_0)) (not (p9 c_0)) (not (p10 c_1 c_0)) (not (p10 c_0 c_0)) (= c_0 c_0) (not (p3 c_0)) (not (p9 c_0)) (not (p10 c_1 c_0)) (= c_1 c_0) (not (p3 c_1)) (= c_1 c_0) (= c_1 c_1) (not (p10 c_1 c_0)) )(or (p14 c_1 c_1 c_0) (not (p3 c_1)) (not (p10 c_0 c_0)) (not (p10 c_1 c_1)) (not (p9 c_0)) (not (p10 c_1 c_0)) (not (p10 c_0 c_1)) (= c_0 c_1) (not (p3 c_0)) (not (p9 c_1)) (not (p10 c_1 c_1)) (= c_1 c_0) (not (p3 c_1)) (= c_1 c_0) (= c_1 c_1) (not (p10 c_1 c_0)) )(or (p14 c_1 c_1 c_0) (not (p3 c_1)) (not (p10 c_0 c_0)) (not (p10 c_1 c_2)) (not (p9 c_0)) (not (p10 c_1 c_0)) (not (p10 c_0 c_2)) (= c_0 c_2) (not (p3 c_0)) (not (p9 c_2)) (not (p10 c_1 c_2)) (= c_1 c_0) (not (p3 c_1)) (= c_1 c_0) (= c_1 c_1) (not (p10 c_1 c_0)) )(or (p14 c_1 c_1 c_0) (not (p3 c_1)) (not (p10 c_0 c_1)) (not (p10 c_1 c_0)) (not (p9 c_1)) (not (p10 c_1 c_1)) (not (p10 c_0 c_0)) (= c_1 c_0) (not (p3 c_0)) (not (p9 c_0)) (not (p10 c_1 c_0)) (= c_1 c_0) (not (p3 c_1)) (= c_1 c_0) (= c_1 c_1) (not (p10 c_1 c_1)) )(or (p14 c_1 c_1 c_0) (not (p3 c_1)) (not (p10 c_0 c_1)) (not (p10 c_1 c_1)) (not (p9 c_1)) (not (p10 c_1 c_1)) (not (p10 c_0 c_1)) (= c_1 c_1) (not (p3 c_0)) (not (p9 c_1)) (not (p10 c_1 c_1)) (= c_1 c_0) (not (p3 c_1)) (= c_1 c_0) (= c_1 c_1) (not (p10 c_1 c_1)) )(or (p14 c_1 c_1 c_0) (not (p3 c_1)) (not (p10 c_0 c_1)) (not (p10 c_1 c_2)) (not (p9 c_1)) (not (p10 c_1 c_1)) (not (p10 c_0 c_2)) (= c_1 c_2) (not (p3 c_0)) (not (p9 c_2)) (not (p10 c_1 c_2)) (= c_1 c_0) (not (p3 c_1)) (= c_1 c_0) (= c_1 c_1) (not (p10 c_1 c_1)) )(or (p14 c_1 c_1 c_0) (not (p3 c_1)) (not (p10 c_0 c_2)) (not (p10 c_1 c_0)) (not (p9 c_2)) (not (p10 c_1 c_2)) (not (p10 c_0 c_0)) (= c_2 c_0) (not (p3 c_0)) (not (p9 c_0)) (not (p10 c_1 c_0)) (= c_1 c_0) (not (p3 c_1)) (= c_1 c_0) (= c_1 c_1) (not (p10 c_1 c_2)) )(or (p14 c_1 c_1 c_0) (not (p3 c_1)) (not (p10 c_0 c_2)) (not (p10 c_1 c_1)) (not (p9 c_2)) (not (p10 c_1 c_2)) (not (p10 c_0 c_1)) (= c_2 c_1) (not (p3 c_0)) (not (p9 c_1)) (not (p10 c_1 c_1)) (= c_1 c_0) (not (p3 c_1)) (= c_1 c_0) (= c_1 c_1) (not (p10 c_1 c_2)) )(or (p14 c_1 c_1 c_0) (not (p3 c_1)) (not (p10 c_0 c_2)) (not (p10 c_1 c_2)) (not (p9 c_2)) (not (p10 c_1 c_2)) (not (p10 c_0 c_2)) (= c_2 c_2) (not (p3 c_0)) (not (p9 c_2)) (not (p10 c_1 c_2)) (= c_1 c_0) (not (p3 c_1)) (= c_1 c_0) (= c_1 c_1) (not (p10 c_1 c_2)) )(or (p14 c_1 c_1 c_1) (not (p3 c_1)) (not (p10 c_1 c_0)) (not (p10 c_1 c_0)) (not (p9 c_0)) (not (p10 c_1 c_0)) (not (p10 c_1 c_0)) (= c_0 c_0) (not (p3 c_1)) (not (p9 c_0)) (not (p10 c_1 c_0)) (= c_1 c_1) (not (p3 c_1)) (= c_1 c_1) (= c_1 c_1) (not (p10 c_1 c_0)) )(or (p14 c_1 c_1 c_1) (not (p3 c_1)) (not (p10 c_1 c_0)) (not (p10 c_1 c_1)) (not (p9 c_0)) (not (p10 c_1 c_0)) (not (p10 c_1 c_1)) (= c_0 c_1) (not (p3 c_1)) (not (p9 c_1)) (not (p10 c_1 c_1)) (= c_1 c_1) (not (p3 c_1)) (= c_1 c_1) (= c_1 c_1) (not (p10 c_1 c_0)) )(or (p14 c_1 c_1 c_1) (not (p3 c_1)) (not (p10 c_1 c_0)) (not (p10 c_1 c_2)) (not (p9 c_0)) (not (p10 c_1 c_0)) (not (p10 c_1 c_2)) (= c_0 c_2) (not (p3 c_1)) (not (p9 c_2)) (not (p10 c_1 c_2)) (= c_1 c_1) (not (p3 c_1)) (= c_1 c_1) (= c_1 c_1) (not (p10 c_1 c_0)) )(or (p14 c_1 c_1 c_1) (not (p3 c_1)) (not (p10 c_1 c_1)) (not (p10 c_1 c_0)) (not (p9 c_1)) (not (p10 c_1 c_1)) (not (p10 c_1 c_0)) (= c_1 c_0) (not (p3 c_1)) (not (p9 c_0)) (not (p10 c_1 c_0)) (= c_1 c_1) (not (p3 c_1)) (= c_1 c_1) (= c_1 c_1) (not (p10 c_1 c_1)) )(or (p14 c_1 c_1 c_1) (not (p3 c_1)) (not (p10 c_1 c_1)) (not (p10 c_1 c_1)) (not (p9 c_1)) (not (p10 c_1 c_1)) (not (p10 c_1 c_1)) (= c_1 c_1) (not (p3 c_1)) (not (p9 c_1)) (not (p10 c_1 c_1)) (= c_1 c_1) (not (p3 c_1)) (= c_1 c_1) (= c_1 c_1) (not (p10 c_1 c_1)) )(or (p14 c_1 c_1 c_1) (not (p3 c_1)) (not (p10 c_1 c_1)) (not (p10 c_1 c_2)) (not (p9 c_1)) (not (p10 c_1 c_1)) (not (p10 c_1 c_2)) (= c_1 c_2) (not (p3 c_1)) (not (p9 c_2)) (not (p10 c_1 c_2)) (= c_1 c_1) (not (p3 c_1)) (= c_1 c_1) (= c_1 c_1) (not (p10 c_1 c_1)) )(or (p14 c_1 c_1 c_1) (not (p3 c_1)) (not (p10 c_1 c_2)) (not (p10 c_1 c_0)) (not (p9 c_2)) (not (p10 c_1 c_2)) (not (p10 c_1 c_0)) (= c_2 c_0) (not (p3 c_1)) (not (p9 c_0)) (not (p10 c_1 c_0)) (= c_1 c_1) (not (p3 c_1)) (= c_1 c_1) (= c_1 c_1) (not (p10 c_1 c_2)) )(or (p14 c_1 c_1 c_1) (not (p3 c_1)) (not (p10 c_1 c_2)) (not (p10 c_1 c_1)) (not (p9 c_2)) (not (p10 c_1 c_2)) (not (p10 c_1 c_1)) (= c_2 c_1) (not (p3 c_1)) (not (p9 c_1)) (not (p10 c_1 c_1)) (= c_1 c_1) (not (p3 c_1)) (= c_1 c_1) (= c_1 c_1) (not (p10 c_1 c_2)) )(or (p14 c_1 c_1 c_1) (not (p3 c_1)) (not (p10 c_1 c_2)) (not (p10 c_1 c_2)) (not (p9 c_2)) (not (p10 c_1 c_2)) (not (p10 c_1 c_2)) (= c_2 c_2) (not (p3 c_1)) (not (p9 c_2)) (not (p10 c_1 c_2)) (= c_1 c_1) (not (p3 c_1)) (= c_1 c_1) (= c_1 c_1) (not (p10 c_1 c_2)) )(or (p14 c_1 c_1 c_2) (not (p3 c_1)) (not (p10 c_2 c_0)) (not (p10 c_1 c_0)) (not (p9 c_0)) (not (p10 c_1 c_0)) (not (p10 c_2 c_0)) (= c_0 c_0) (not (p3 c_2)) (not (p9 c_0)) (not (p10 c_1 c_0)) (= c_1 c_2) (not (p3 c_1)) (= c_1 c_2) (= c_1 c_1) (not (p10 c_1 c_0)) )(or (p14 c_1 c_1 c_2) (not (p3 c_1)) (not (p10 c_2 c_0)) (not (p10 c_1 c_1)) (not (p9 c_0)) (not (p10 c_1 c_0)) (not (p10 c_2 c_1)) (= c_0 c_1) (not (p3 c_2)) (not (p9 c_1)) (not (p10 c_1 c_1)) (= c_1 c_2) (not (p3 c_1)) (= c_1 c_2) (= c_1 c_1) (not (p10 c_1 c_0)) )(or (p14 c_1 c_1 c_2) (not (p3 c_1)) (not (p10 c_2 c_0)) (not (p10 c_1 c_2)) (not (p9 c_0)) (not (p10 c_1 c_0)) (not (p10 c_2 c_2)) (= c_0 c_2) (not (p3 c_2)) (not (p9 c_2)) (not (p10 c_1 c_2)) (= c_1 c_2) (not (p3 c_1)) (= c_1 c_2) (= c_1 c_1) (not (p10 c_1 c_0)) )(or (p14 c_1 c_1 c_2) (not (p3 c_1)) (not (p10 c_2 c_1)) (not (p10 c_1 c_0)) (not (p9 c_1)) (not (p10 c_1 c_1)) (not (p10 c_2 c_0)) (= c_1 c_0) (not (p3 c_2)) (not (p9 c_0)) (not (p10 c_1 c_0)) (= c_1 c_2) (not (p3 c_1)) (= c_1 c_2) (= c_1 c_1) (not (p10 c_1 c_1)) )(or (p14 c_1 c_1 c_2) (not (p3 c_1)) (not (p10 c_2 c_1)) (not (p10 c_1 c_1)) (not (p9 c_1)) (not (p10 c_1 c_1)) (not (p10 c_2 c_1)) (= c_1 c_1) (not (p3 c_2)) (not (p9 c_1)) (not (p10 c_1 c_1)) (= c_1 c_2) (not (p3 c_1)) (= c_1 c_2) (= c_1 c_1) (not (p10 c_1 c_1)) )(or (p14 c_1 c_1 c_2) (not (p3 c_1)) (not (p10 c_2 c_1)) (not (p10 c_1 c_2)) (not (p9 c_1)) (not (p10 c_1 c_1)) (not (p10 c_2 c_2)) (= c_1 c_2) (not (p3 c_2)) (not (p9 c_2)) (not (p10 c_1 c_2)) (= c_1 c_2) (not (p3 c_1)) (= c_1 c_2) (= c_1 c_1) (not (p10 c_1 c_1)) )(or (p14 c_1 c_1 c_2) (not (p3 c_1)) (not (p10 c_2 c_2)) (not (p10 c_1 c_0)) (not (p9 c_2)) (not (p10 c_1 c_2)) (not (p10 c_2 c_0)) (= c_2 c_0) (not (p3 c_2)) (not (p9 c_0)) (not (p10 c_1 c_0)) (= c_1 c_2) (not (p3 c_1)) (= c_1 c_2) (= c_1 c_1) (not (p10 c_1 c_2)) )(or (p14 c_1 c_1 c_2) (not (p3 c_1)) (not (p10 c_2 c_2)) (not (p10 c_1 c_1)) (not (p9 c_2)) (not (p10 c_1 c_2)) (not (p10 c_2 c_1)) (= c_2 c_1) (not (p3 c_2)) (not (p9 c_1)) (not (p10 c_1 c_1)) (= c_1 c_2) (not (p3 c_1)) (= c_1 c_2) (= c_1 c_1) (not (p10 c_1 c_2)) )(or (p14 c_1 c_1 c_2) (not (p3 c_1)) (not (p10 c_2 c_2)) (not (p10 c_1 c_2)) (not (p9 c_2)) (not (p10 c_1 c_2)) (not (p10 c_2 c_2)) (= c_2 c_2) (not (p3 c_2)) (not (p9 c_2)) (not (p10 c_1 c_2)) (= c_1 c_2) (not (p3 c_1)) (= c_1 c_2) (= c_1 c_1) (not (p10 c_1 c_2)) )(or (p14 c_1 c_2 c_0) (not (p3 c_2)) (not (p10 c_0 c_0)) (not (p10 c_1 c_0)) (not (p9 c_0)) (not (p10 c_1 c_0)) (not (p10 c_0 c_0)) (= c_0 c_0) (not (p3 c_0)) (not (p9 c_0)) (not (p10 c_2 c_0)) (= c_2 c_0) (not (p3 c_1)) (= c_1 c_0) (= c_1 c_2) (not (p10 c_2 c_0)) )(or (p14 c_1 c_2 c_0) (not (p3 c_2)) (not (p10 c_0 c_0)) (not (p10 c_1 c_1)) (not (p9 c_0)) (not (p10 c_1 c_0)) (not (p10 c_0 c_1)) (= c_0 c_1) (not (p3 c_0)) (not (p9 c_1)) (not (p10 c_2 c_1)) (= c_2 c_0) (not (p3 c_1)) (= c_1 c_0) (= c_1 c_2) (not (p10 c_2 c_0)) )(or (p14 c_1 c_2 c_0) (not (p3 c_2)) (not (p10 c_0 c_0)) (not (p10 c_1 c_2)) (not (p9 c_0)) (not (p10 c_1 c_0)) (not (p10 c_0 c_2)) (= c_0 c_2) (not (p3 c_0)) (not (p9 c_2)) (not (p10 c_2 c_2)) (= c_2 c_0) (not (p3 c_1)) (= c_1 c_0) (= c_1 c_2) (not (p10 c_2 c_0)) )(or (p14 c_1 c_2 c_0) (not (p3 c_2)) (not (p10 c_0 c_1)) (not (p10 c_1 c_0)) (not (p9 c_1)) (not (p10 c_1 c_1)) (not (p10 c_0 c_0)) (= c_1 c_0) (not (p3 c_0)) (not (p9 c_0)) (not (p10 c_2 c_0)) (= c_2 c_0) (not (p3 c_1)) (= c_1 c_0) (= c_1 c_2) (not (p10 c_2 c_1)) )(or (p14 c_1 c_2 c_0) (not (p3 c_2)) (not (p10 c_0 c_1)) (not (p10 c_1 c_1)) (not (p9 c_1)) (not (p10 c_1 c_1)) (not (p10 c_0 c_1)) (= c_1 c_1) (not (p3 c_0)) (not (p9 c_1)) (not (p10 c_2 c_1)) (= c_2 c_0) (not (p3 c_1)) (= c_1 c_0) (= c_1 c_2) (not (p10 c_2 c_1)) )(or (p14 c_1 c_2 c_0) (not (p3 c_2)) (not (p10 c_0 c_1)) (not (p10 c_1 c_2)) (not (p9 c_1)) (not (p10 c_1 c_1)) (not (p10 c_0 c_2)) (= c_1 c_2) (not (p3 c_0)) (not (p9 c_2)) (not (p10 c_2 c_2)) (= c_2 c_0) (not (p3 c_1)) (= c_1 c_0) (= c_1 c_2) (not (p10 c_2 c_1)) )(or (p14 c_1 c_2 c_0) (not (p3 c_2)) (not (p10 c_0 c_2)) (not (p10 c_1 c_0)) (not (p9 c_2)) (not (p10 c_1 c_2)) (not (p10 c_0 c_0)) (= c_2 c_0) (not (p3 c_0)) (not (p9 c_0)) (not (p10 c_2 c_0)) (= c_2 c_0) (not (p3 c_1)) (= c_1 c_0) (= c_1 c_2) (not (p10 c_2 c_2)) )(or (p14 c_1 c_2 c_0) (not (p3 c_2)) (not (p10 c_0 c_2)) (not (p10 c_1 c_1)) (not (p9 c_2)) (not (p10 c_1 c_2)) (not (p10 c_0 c_1)) (= c_2 c_1) (not (p3 c_0)) (not (p9 c_1)) (not (p10 c_2 c_1)) (= c_2 c_0) (not (p3 c_1)) (= c_1 c_0) (= c_1 c_2) (not (p10 c_2 c_2)) )(or (p14 c_1 c_2 c_0) (not (p3 c_2)) (not (p10 c_0 c_2)) (not (p10 c_1 c_2)) (not (p9 c_2)) (not (p10 c_1 c_2)) (not (p10 c_0 c_2)) (= c_2 c_2) (not (p3 c_0)) (not (p9 c_2)) (not (p10 c_2 c_2)) (= c_2 c_0) (not (p3 c_1)) (= c_1 c_0) (= c_1 c_2) (not (p10 c_2 c_2)) )(or (p14 c_1 c_2 c_1) (not (p3 c_2)) (not (p10 c_1 c_0)) (not (p10 c_1 c_0)) (not (p9 c_0)) (not (p10 c_1 c_0)) (not (p10 c_1 c_0)) (= c_0 c_0) (not (p3 c_1)) (not (p9 c_0)) (not (p10 c_2 c_0)) (= c_2 c_1) (not (p3 c_1)) (= c_1 c_1) (= c_1 c_2) (not (p10 c_2 c_0)) )(or (p14 c_1 c_2 c_1) (not (p3 c_2)) (not (p10 c_1 c_0)) (not (p10 c_1 c_1)) (not (p9 c_0)) (not (p10 c_1 c_0)) (not (p10 c_1 c_1)) (= c_0 c_1) (not (p3 c_1)) (not (p9 c_1)) (not (p10 c_2 c_1)) (= c_2 c_1) (not (p3 c_1)) (= c_1 c_1) (= c_1 c_2) (not (p10 c_2 c_0)) )(or (p14 c_1 c_2 c_1) (not (p3 c_2)) (not (p10 c_1 c_0)) (not (p10 c_1 c_2)) (not (p9 c_0)) (not (p10 c_1 c_0)) (not (p10 c_1 c_2)) (= c_0 c_2) (not (p3 c_1)) (not (p9 c_2)) (not (p10 c_2 c_2)) (= c_2 c_1) (not (p3 c_1)) (= c_1 c_1) (= c_1 c_2) (not (p10 c_2 c_0)) )(or (p14 c_1 c_2 c_1) (not (p3 c_2)) (not (p10 c_1 c_1)) (not (p10 c_1 c_0)) (not (p9 c_1)) (not (p10 c_1 c_1)) (not (p10 c_1 c_0)) (= c_1 c_0) (not (p3 c_1)) (not (p9 c_0)) (not (p10 c_2 c_0)) (= c_2 c_1) (not (p3 c_1)) (= c_1 c_1) (= c_1 c_2) (not (p10 c_2 c_1)) )(or (p14 c_1 c_2 c_1) (not (p3 c_2)) (not (p10 c_1 c_1)) (not (p10 c_1 c_1)) (not (p9 c_1)) (not (p10 c_1 c_1)) (not (p10 c_1 c_1)) (= c_1 c_1) (not (p3 c_1)) (not (p9 c_1)) (not (p10 c_2 c_1)) (= c_2 c_1) (not (p3 c_1)) (= c_1 c_1) (= c_1 c_2) (not (p10 c_2 c_1)) )(or (p14 c_1 c_2 c_1) (not (p3 c_2)) (not (p10 c_1 c_1)) (not (p10 c_1 c_2)) (not (p9 c_1)) (not (p10 c_1 c_1)) (not (p10 c_1 c_2)) (= c_1 c_2) (not (p3 c_1)) (not (p9 c_2)) (not (p10 c_2 c_2)) (= c_2 c_1) (not (p3 c_1)) (= c_1 c_1) (= c_1 c_2) (not (p10 c_2 c_1)) )(or (p14 c_1 c_2 c_1) (not (p3 c_2)) (not (p10 c_1 c_2)) (not (p10 c_1 c_0)) (not (p9 c_2)) (not (p10 c_1 c_2)) (not (p10 c_1 c_0)) (= c_2 c_0) (not (p3 c_1)) (not (p9 c_0)) (not (p10 c_2 c_0)) (= c_2 c_1) (not (p3 c_1)) (= c_1 c_1) (= c_1 c_2) (not (p10 c_2 c_2)) )(or (p14 c_1 c_2 c_1) (not (p3 c_2)) (not (p10 c_1 c_2)) (not (p10 c_1 c_1)) (not (p9 c_2)) (not (p10 c_1 c_2)) (not (p10 c_1 c_1)) (= c_2 c_1) (not (p3 c_1)) (not (p9 c_1)) (not (p10 c_2 c_1)) (= c_2 c_1) (not (p3 c_1)) (= c_1 c_1) (= c_1 c_2) (not (p10 c_2 c_2)) )(or (p14 c_1 c_2 c_1) (not (p3 c_2)) (not (p10 c_1 c_2)) (not (p10 c_1 c_2)) (not (p9 c_2)) (not (p10 c_1 c_2)) (not (p10 c_1 c_2)) (= c_2 c_2) (not (p3 c_1)) (not (p9 c_2)) (not (p10 c_2 c_2)) (= c_2 c_1) (not (p3 c_1)) (= c_1 c_1) (= c_1 c_2) (not (p10 c_2 c_2)) )(or (p14 c_1 c_2 c_2) (not (p3 c_2)) (not (p10 c_2 c_0)) (not (p10 c_1 c_0)) (not (p9 c_0)) (not (p10 c_1 c_0)) (not (p10 c_2 c_0)) (= c_0 c_0) (not (p3 c_2)) (not (p9 c_0)) (not (p10 c_2 c_0)) (= c_2 c_2) (not (p3 c_1)) (= c_1 c_2) (= c_1 c_2) (not (p10 c_2 c_0)) )(or (p14 c_1 c_2 c_2) (not (p3 c_2)) (not (p10 c_2 c_0)) (not (p10 c_1 c_1)) (not (p9 c_0)) (not (p10 c_1 c_0)) (not (p10 c_2 c_1)) (= c_0 c_1) (not (p3 c_2)) (not (p9 c_1)) (not (p10 c_2 c_1)) (= c_2 c_2) (not (p3 c_1)) (= c_1 c_2) (= c_1 c_2) (not (p10 c_2 c_0)) )(or (p14 c_1 c_2 c_2) (not (p3 c_2)) (not (p10 c_2 c_0)) (not (p10 c_1 c_2)) (not (p9 c_0)) (not (p10 c_1 c_0)) (not (p10 c_2 c_2)) (= c_0 c_2) (not (p3 c_2)) (not (p9 c_2)) (not (p10 c_2 c_2)) (= c_2 c_2) (not (p3 c_1)) (= c_1 c_2) (= c_1 c_2) (not (p10 c_2 c_0)) )(or (p14 c_1 c_2 c_2) (not (p3 c_2)) (not (p10 c_2 c_1)) (not (p10 c_1 c_0)) (not (p9 c_1)) (not (p10 c_1 c_1)) (not (p10 c_2 c_0)) (= c_1 c_0) (not (p3 c_2)) (not (p9 c_0)) (not (p10 c_2 c_0)) (= c_2 c_2) (not (p3 c_1)) (= c_1 c_2) (= c_1 c_2) (not (p10 c_2 c_1)) )(or (p14 c_1 c_2 c_2) (not (p3 c_2)) (not (p10 c_2 c_1)) (not (p10 c_1 c_1)) (not (p9 c_1)) (not (p10 c_1 c_1)) (not (p10 c_2 c_1)) (= c_1 c_1) (not (p3 c_2)) (not (p9 c_1)) (not (p10 c_2 c_1)) (= c_2 c_2) (not (p3 c_1)) (= c_1 c_2) (= c_1 c_2) (not (p10 c_2 c_1)) )(or (p14 c_1 c_2 c_2) (not (p3 c_2)) (not (p10 c_2 c_1)) (not (p10 c_1 c_2)) (not (p9 c_1)) (not (p10 c_1 c_1)) (not (p10 c_2 c_2)) (= c_1 c_2) (not (p3 c_2)) (not (p9 c_2)) (not (p10 c_2 c_2)) (= c_2 c_2) (not (p3 c_1)) (= c_1 c_2) (= c_1 c_2) (not (p10 c_2 c_1)) )(or (p14 c_1 c_2 c_2) (not (p3 c_2)) (not (p10 c_2 c_2)) (not (p10 c_1 c_0)) (not (p9 c_2)) (not (p10 c_1 c_2)) (not (p10 c_2 c_0)) (= c_2 c_0) (not (p3 c_2)) (not (p9 c_0)) (not (p10 c_2 c_0)) (= c_2 c_2) (not (p3 c_1)) (= c_1 c_2) (= c_1 c_2) (not (p10 c_2 c_2)) )(or (p14 c_1 c_2 c_2) (not (p3 c_2)) (not (p10 c_2 c_2)) (not (p10 c_1 c_1)) (not (p9 c_2)) (not (p10 c_1 c_2)) (not (p10 c_2 c_1)) (= c_2 c_1) (not (p3 c_2)) (not (p9 c_1)) (not (p10 c_2 c_1)) (= c_2 c_2) (not (p3 c_1)) (= c_1 c_2) (= c_1 c_2) (not (p10 c_2 c_2)) )(or (p14 c_1 c_2 c_2) (not (p3 c_2)) (not (p10 c_2 c_2)) (not (p10 c_1 c_2)) (not (p9 c_2)) (not (p10 c_1 c_2)) (not (p10 c_2 c_2)) (= c_2 c_2) (not (p3 c_2)) (not (p9 c_2)) (not (p10 c_2 c_2)) (= c_2 c_2) (not (p3 c_1)) (= c_1 c_2) (= c_1 c_2) (not (p10 c_2 c_2)) )(or (p14 c_2 c_0 c_0) (not (p3 c_0)) (not (p10 c_0 c_0)) (not (p10 c_2 c_0)) (not (p9 c_0)) (not (p10 c_2 c_0)) (not (p10 c_0 c_0)) (= c_0 c_0) (not (p3 c_0)) (not (p9 c_0)) (not (p10 c_0 c_0)) (= c_0 c_0) (not (p3 c_2)) (= c_2 c_0) (= c_2 c_0) (not (p10 c_0 c_0)) )(or (p14 c_2 c_0 c_0) (not (p3 c_0)) (not (p10 c_0 c_0)) (not (p10 c_2 c_1)) (not (p9 c_0)) (not (p10 c_2 c_0)) (not (p10 c_0 c_1)) (= c_0 c_1) (not (p3 c_0)) (not (p9 c_1)) (not (p10 c_0 c_1)) (= c_0 c_0) (not (p3 c_2)) (= c_2 c_0) (= c_2 c_0) (not (p10 c_0 c_0)) )(or (p14 c_2 c_0 c_0) (not (p3 c_0)) (not (p10 c_0 c_0)) (not (p10 c_2 c_2)) (not (p9 c_0)) (not (p10 c_2 c_0)) (not (p10 c_0 c_2)) (= c_0 c_2) (not (p3 c_0)) (not (p9 c_2)) (not (p10 c_0 c_2)) (= c_0 c_0) (not (p3 c_2)) (= c_2 c_0) (= c_2 c_0) (not (p10 c_0 c_0)) )(or (p14 c_2 c_0 c_0) (not (p3 c_0)) (not (p10 c_0 c_1)) (not (p10 c_2 c_0)) (not (p9 c_1)) (not (p10 c_2 c_1)) (not (p10 c_0 c_0)) (= c_1 c_0) (not (p3 c_0)) (not (p9 c_0)) (not (p10 c_0 c_0)) (= c_0 c_0) (not (p3 c_2)) (= c_2 c_0) (= c_2 c_0) (not (p10 c_0 c_1)) )(or (p14 c_2 c_0 c_0) (not (p3 c_0)) (not (p10 c_0 c_1)) (not (p10 c_2 c_1)) (not (p9 c_1)) (not (p10 c_2 c_1)) (not (p10 c_0 c_1)) (= c_1 c_1) (not (p3 c_0)) (not (p9 c_1)) (not (p10 c_0 c_1)) (= c_0 c_0) (not (p3 c_2)) (= c_2 c_0) (= c_2 c_0) (not (p10 c_0 c_1)) )(or (p14 c_2 c_0 c_0) (not (p3 c_0)) (not (p10 c_0 c_1)) (not (p10 c_2 c_2)) (not (p9 c_1)) (not (p10 c_2 c_1)) (not (p10 c_0 c_2)) (= c_1 c_2) (not (p3 c_0)) (not (p9 c_2)) (not (p10 c_0 c_2)) (= c_0 c_0) (not (p3 c_2)) (= c_2 c_0) (= c_2 c_0) (not (p10 c_0 c_1)) )(or (p14 c_2 c_0 c_0) (not (p3 c_0)) (not (p10 c_0 c_2)) (not (p10 c_2 c_0)) (not (p9 c_2)) (not (p10 c_2 c_2)) (not (p10 c_0 c_0)) (= c_2 c_0) (not (p3 c_0)) (not (p9 c_0)) (not (p10 c_0 c_0)) (= c_0 c_0) (not (p3 c_2)) (= c_2 c_0) (= c_2 c_0) (not (p10 c_0 c_2)) )(or (p14 c_2 c_0 c_0) (not (p3 c_0)) (not (p10 c_0 c_2)) (not (p10 c_2 c_1)) (not (p9 c_2)) (not (p10 c_2 c_2)) (not (p10 c_0 c_1)) (= c_2 c_1) (not (p3 c_0)) (not (p9 c_1)) (not (p10 c_0 c_1)) (= c_0 c_0) (not (p3 c_2)) (= c_2 c_0) (= c_2 c_0) (not (p10 c_0 c_2)) )(or (p14 c_2 c_0 c_0) (not (p3 c_0)) (not (p10 c_0 c_2)) (not (p10 c_2 c_2)) (not (p9 c_2)) (not (p10 c_2 c_2)) (not (p10 c_0 c_2)) (= c_2 c_2) (not (p3 c_0)) (not (p9 c_2)) (not (p10 c_0 c_2)) (= c_0 c_0) (not (p3 c_2)) (= c_2 c_0) (= c_2 c_0) (not (p10 c_0 c_2)) )(or (p14 c_2 c_0 c_1) (not (p3 c_0)) (not (p10 c_1 c_0)) (not (p10 c_2 c_0)) (not (p9 c_0)) (not (p10 c_2 c_0)) (not (p10 c_1 c_0)) (= c_0 c_0) (not (p3 c_1)) (not (p9 c_0)) (n