(benchmark NEQ004_size6.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
:extrafuns ((c14 U))
:extrafuns ((c12 U))
:extrapreds ((p4 U U))
:extrafuns ((c13 U))
:extrapreds ((p3 U U))
:extrafuns ((c15 U))
:extrafuns ((c17 U))
:extrapreds ((p6 U U))
:extrapreds ((p2 U U))
:extrapreds ((p1 U U))
:extrafuns ((c11 U))
:extrafuns ((f5 U U U))
:extrafuns ((c10 U))
:extrapreds ((p8 U))
:extrafuns ((c16 U))
:extrapreds ((p9 U U))
:extrapreds ((p7 U U))
:extrafuns ((c_0 U))
:extrafuns ((c_1 U))
:extrafuns ((c_2 U))
:extrafuns ((c_3 U))
:extrafuns ((c_4 U))
:extrafuns ((c_5 U))
:formula 
( and 
( distinct c_0 c_1 c_2 c_3 c_4 c_5 )(p4 c14 c12) (p4 c14 c13) (or (not (= c_0 c_0)) (p3 c_0 c_0) )(or (not (= c_0 c_1)) (p3 c_0 c_1) )(or (not (= c_0 c_2)) (p3 c_0 c_2) )(or (not (= c_0 c_3)) (p3 c_0 c_3) )(or (not (= c_0 c_4)) (p3 c_0 c_4) )(or (not (= c_0 c_5)) (p3 c_0 c_5) )(or (not (= c_1 c_0)) (p3 c_1 c_0) )(or (not (= c_1 c_1)) (p3 c_1 c_1) )(or (not (= c_1 c_2)) (p3 c_1 c_2) )(or (not (= c_1 c_3)) (p3 c_1 c_3) )(or (not (= c_1 c_4)) (p3 c_1 c_4) )(or (not (= c_1 c_5)) (p3 c_1 c_5) )(or (not (= c_2 c_0)) (p3 c_2 c_0) )(or (not (= c_2 c_1)) (p3 c_2 c_1) )(or (not (= c_2 c_2)) (p3 c_2 c_2) )(or (not (= c_2 c_3)) (p3 c_2 c_3) )(or (not (= c_2 c_4)) (p3 c_2 c_4) )(or (not (= c_2 c_5)) (p3 c_2 c_5) )(or (not (= c_3 c_0)) (p3 c_3 c_0) )(or (not (= c_3 c_1)) (p3 c_3 c_1) )(or (not (= c_3 c_2)) (p3 c_3 c_2) )(or (not (= c_3 c_3)) (p3 c_3 c_3) )(or (not (= c_3 c_4)) (p3 c_3 c_4) )(or (not (= c_3 c_5)) (p3 c_3 c_5) )(or (not (= c_4 c_0)) (p3 c_4 c_0) )(or (not (= c_4 c_1)) (p3 c_4 c_1) )(or (not (= c_4 c_2)) (p3 c_4 c_2) )(or (not (= c_4 c_3)) (p3 c_4 c_3) )(or (not (= c_4 c_4)) (p3 c_4 c_4) )(or (not (= c_4 c_5)) (p3 c_4 c_5) )(or (not (= c_5 c_0)) (p3 c_5 c_0) )(or (not (= c_5 c_1)) (p3 c_5 c_1) )(or (not (= c_5 c_2)) (p3 c_5 c_2) )(or (not (= c_5 c_3)) (p3 c_5 c_3) )(or (not (= c_5 c_4)) (p3 c_5 c_4) )(or (not (= c_5 c_5)) (p3 c_5 c_5) )(or (not (p4 c_0 c_0)) (not (p4 c_0 c_0)) )(or (not (p4 c_0 c_1)) (not (p4 c_1 c_0)) )(or (not (p4 c_0 c_2)) (not (p4 c_2 c_0)) )(or (not (p4 c_0 c_3)) (not (p4 c_3 c_0)) )(or (not (p4 c_0 c_4)) (not (p4 c_4 c_0)) )(or (not (p4 c_0 c_5)) (not (p4 c_5 c_0)) )(or (not (p4 c_1 c_0)) (not (p4 c_0 c_1)) )(or (not (p4 c_1 c_1)) (not (p4 c_1 c_1)) )(or (not (p4 c_1 c_2)) (not (p4 c_2 c_1)) )(or (not (p4 c_1 c_3)) (not (p4 c_3 c_1)) )(or (not (p4 c_1 c_4)) (not (p4 c_4 c_1)) )(or (not (p4 c_1 c_5)) (not (p4 c_5 c_1)) )(or (not (p4 c_2 c_0)) (not (p4 c_0 c_2)) )(or (not (p4 c_2 c_1)) (not (p4 c_1 c_2)) )(or (not (p4 c_2 c_2)) (not (p4 c_2 c_2)) )(or (not (p4 c_2 c_3)) (not (p4 c_3 c_2)) )(or (not (p4 c_2 c_4)) (not (p4 c_4 c_2)) )(or (not (p4 c_2 c_5)) (not (p4 c_5 c_2)) )(or (not (p4 c_3 c_0)) (not (p4 c_0 c_3)) )(or (not (p4 c_3 c_1)) (not (p4 c_1 c_3)) )(or (not (p4 c_3 c_2)) (not (p4 c_2 c_3)) )(or (not (p4 c_3 c_3)) (not (p4 c_3 c_3)) )(or (not (p4 c_3 c_4)) (not (p4 c_4 c_3)) )(or (not (p4 c_3 c_5)) (not (p4 c_5 c_3)) )(or (not (p4 c_4 c_0)) (not (p4 c_0 c_4)) )(or (not (p4 c_4 c_1)) (not (p4 c_1 c_4)) )(or (not (p4 c_4 c_2)) (not (p4 c_2 c_4)) )(or (not (p4 c_4 c_3)) (not (p4 c_3 c_4)) )(or (not (p4 c_4 c_4)) (not (p4 c_4 c_4)) )(or (not (p4 c_4 c_5)) (not (p4 c_5 c_4)) )(or (not (p4 c_5 c_0)) (not (p4 c_0 c_5)) )(or (not (p4 c_5 c_1)) (not (p4 c_1 c_5)) )(or (not (p4 c_5 c_2)) (not (p4 c_2 c_5)) )(or (not (p4 c_5 c_3)) (not (p4 c_3 c_5)) )(or (not (p4 c_5 c_4)) (not (p4 c_4 c_5)) )(or (not (p4 c_5 c_5)) (not (p4 c_5 c_5)) )(not (p6 c15 c17)) (or (not (p4 c_0 c_0)) (p2 c_0 c_0) )(or (not (p4 c_0 c_1)) (p2 c_1 c_0) )(or (not (p4 c_0 c_2)) (p2 c_2 c_0) )(or (not (p4 c_0 c_3)) (p2 c_3 c_0) )(or (not (p4 c_0 c_4)) (p2 c_4 c_0) )(or (not (p4 c_0 c_5)) (p2 c_5 c_0) )(or (not (p4 c_1 c_0)) (p2 c_0 c_1) )(or (not (p4 c_1 c_1)) (p2 c_1 c_1) )(or (not (p4 c_1 c_2)) (p2 c_2 c_1) )(or (not (p4 c_1 c_3)) (p2 c_3 c_1) )(or (not (p4 c_1 c_4)) (p2 c_4 c_1) )(or (not (p4 c_1 c_5)) (p2 c_5 c_1) )(or (not (p4 c_2 c_0)) (p2 c_0 c_2) )(or (not (p4 c_2 c_1)) (p2 c_1 c_2) )(or (not (p4 c_2 c_2)) (p2 c_2 c_2) )(or (not (p4 c_2 c_3)) (p2 c_3 c_2) )(or (not (p4 c_2 c_4)) (p2 c_4 c_2) )(or (not (p4 c_2 c_5)) (p2 c_5 c_2) )(or (not (p4 c_3 c_0)) (p2 c_0 c_3) )(or (not (p4 c_3 c_1)) (p2 c_1 c_3) )(or (not (p4 c_3 c_2)) (p2 c_2 c_3) )(or (not (p4 c_3 c_3)) (p2 c_3 c_3) )(or (not (p4 c_3 c_4)) (p2 c_4 c_3) )(or (not (p4 c_3 c_5)) (p2 c_5 c_3) )(or (not (p4 c_4 c_0)) (p2 c_0 c_4) )(or (not (p4 c_4 c_1)) (p2 c_1 c_4) )(or (not (p4 c_4 c_2)) (p2 c_2 c_4) )(or (not (p4 c_4 c_3)) (p2 c_3 c_4) )(or (not (p4 c_4 c_4)) (p2 c_4 c_4) )(or (not (p4 c_4 c_5)) (p2 c_5 c_4) )(or (not (p4 c_5 c_0)) (p2 c_0 c_5) )(or (not (p4 c_5 c_1)) (p2 c_1 c_5) )(or (not (p4 c_5 c_2)) (p2 c_2 c_5) )(or (not (p4 c_5 c_3)) (p2 c_3 c_5) )(or (not (p4 c_5 c_4)) (p2 c_4 c_5) )(or (not (p4 c_5 c_5)) (p2 c_5 c_5) )(or (p1 c_0 c_0) (not (= c_0 c_0)) )(or (p1 c_0 c_1) (not (= c_0 c_1)) )(or (p1 c_0 c_2) (not (= c_0 c_2)) )(or (p1 c_0 c_3) (not (= c_0 c_3)) )(or (p1 c_0 c_4) (not (= c_0 c_4)) )(or (p1 c_0 c_5) (not (= c_0 c_5)) )(or (p1 c_1 c_0) (not (= c_1 c_0)) )(or (p1 c_1 c_1) (not (= c_1 c_1)) )(or (p1 c_1 c_2) (not (= c_1 c_2)) )(or (p1 c_1 c_3) (not (= c_1 c_3)) )(or (p1 c_1 c_4) (not (= c_1 c_4)) )(or (p1 c_1 c_5) (not (= c_1 c_5)) )(or (p1 c_2 c_0) (not (= c_2 c_0)) )(or (p1 c_2 c_1) (not (= c_2 c_1)) )(or (p1 c_2 c_2) (not (= c_2 c_2)) )(or (p1 c_2 c_3) (not (= c_2 c_3)) )(or (p1 c_2 c_4) (not (= c_2 c_4)) )(or (p1 c_2 c_5) (not (= c_2 c_5)) )(or (p1 c_3 c_0) (not (= c_3 c_0)) )(or (p1 c_3 c_1) (not (= c_3 c_1)) )(or (p1 c_3 c_2) (not (= c_3 c_2)) )(or (p1 c_3 c_3) (not (= c_3 c_3)) )(or (p1 c_3 c_4) (not (= c_3 c_4)) )(or (p1 c_3 c_5) (not (= c_3 c_5)) )(or (p1 c_4 c_0) (not (= c_4 c_0)) )(or (p1 c_4 c_1) (not (= c_4 c_1)) )(or (p1 c_4 c_2) (not (= c_4 c_2)) )(or (p1 c_4 c_3) (not (= c_4 c_3)) )(or (p1 c_4 c_4) (not (= c_4 c_4)) )(or (p1 c_4 c_5) (not (= c_4 c_5)) )(or (p1 c_5 c_0) (not (= c_5 c_0)) )(or (p1 c_5 c_1) (not (= c_5 c_1)) )(or (p1 c_5 c_2) (not (= c_5 c_2)) )(or (p1 c_5 c_3) (not (= c_5 c_3)) )(or (p1 c_5 c_4) (not (= c_5 c_4)) )(or (p1 c_5 c_5) (not (= c_5 c_5)) )(p4 c13 c11) (or (not (p4 c_0 c_0)) (p3 c_0 c_0) )(or (not (p4 c_0 c_1)) (p3 c_0 c_1) )(or (not (p4 c_0 c_2)) (p3 c_0 c_2) )(or (not (p4 c_0 c_3)) (p3 c_0 c_3) )(or (not (p4 c_0 c_4)) (p3 c_0 c_4) )(or (not (p4 c_0 c_5)) (p3 c_0 c_5) )(or (not (p4 c_1 c_0)) (p3 c_1 c_0) )(or (not (p4 c_1 c_1)) (p3 c_1 c_1) )(or (not (p4 c_1 c_2)) (p3 c_1 c_2) )(or (not (p4 c_1 c_3)) (p3 c_1 c_3) )(or (not (p4 c_1 c_4)) (p3 c_1 c_4) )(or (not (p4 c_1 c_5)) (p3 c_1 c_5) )(or (not (p4 c_2 c_0)) (p3 c_2 c_0) )(or (not (p4 c_2 c_1)) (p3 c_2 c_1) )(or (not (p4 c_2 c_2)) (p3 c_2 c_2) )(or (not (p4 c_2 c_3)) (p3 c_2 c_3) )(or (not (p4 c_2 c_4)) (p3 c_2 c_4) )(or (not (p4 c_2 c_5)) (p3 c_2 c_5) )(or (not (p4 c_3 c_0)) (p3 c_3 c_0) )(or (not (p4 c_3 c_1)) (p3 c_3 c_1) )(or (not (p4 c_3 c_2)) (p3 c_3 c_2) )(or (not (p4 c_3 c_3)) (p3 c_3 c_3) )(or (not (p4 c_3 c_4)) (p3 c_3 c_4) )(or (not (p4 c_3 c_5)) (p3 c_3 c_5) )(or (not (p4 c_4 c_0)) (p3 c_4 c_0) )(or (not (p4 c_4 c_1)) (p3 c_4 c_1) )(or (not (p4 c_4 c_2)) (p3 c_4 c_2) )(or (not (p4 c_4 c_3)) (p3 c_4 c_3) )(or (not (p4 c_4 c_4)) (p3 c_4 c_4) )(or (not (p4 c_4 c_5)) (p3 c_4 c_5) )(or (not (p4 c_5 c_0)) (p3 c_5 c_0) )(or (not (p4 c_5 c_1)) (p3 c_5 c_1) )(or (not (p4 c_5 c_2)) (p3 c_5 c_2) )(or (not (p4 c_5 c_3)) (p3 c_5 c_3) )(or (not (p4 c_5 c_4)) (p3 c_5 c_4) )(or (not (p4 c_5 c_5)) (p3 c_5 c_5) )(or (= (f5 c_0 c_0) c10) (not (p8 c_0)) (not (p6 c_0 c_0)) )(or (= (f5 c_0 c_1) c10) (not (p8 c_0)) (not (p6 c_0 c_1)) )(or (= (f5 c_0 c_2) c10) (not (p8 c_0)) (not (p6 c_0 c_2)) )(or (= (f5 c_0 c_3) c10) (not (p8 c_0)) (not (p6 c_0 c_3)) )(or (= (f5 c_0 c_4) c10) (not (p8 c_0)) (not (p6 c_0 c_4)) )(or (= (f5 c_0 c_5) c10) (not (p8 c_0)) (not (p6 c_0 c_5)) )(or (= (f5 c_1 c_0) c10) (not (p8 c_1)) (not (p6 c_1 c_0)) )(or (= (f5 c_1 c_1) c10) (not (p8 c_1)) (not (p6 c_1 c_1)) )(or (= (f5 c_1 c_2) c10) (not (p8 c_1)) (not (p6 c_1 c_2)) )(or (= (f5 c_1 c_3) c10) (not (p8 c_1)) (not (p6 c_1 c_3)) )(or (= (f5 c_1 c_4) c10) (not (p8 c_1)) (not (p6 c_1 c_4)) )(or (= (f5 c_1 c_5) c10) (not (p8 c_1)) (not (p6 c_1 c_5)) )(or (= (f5 c_2 c_0) c10) (not (p8 c_2)) (not (p6 c_2 c_0)) )(or (= (f5 c_2 c_1) c10) (not (p8 c_2)) (not (p6 c_2 c_1)) )(or (= (f5 c_2 c_2) c10) (not (p8 c_2)) (not (p6 c_2 c_2)) )(or (= (f5 c_2 c_3) c10) (not (p8 c_2)) (not (p6 c_2 c_3)) )(or (= (f5 c_2 c_4) c10) (not (p8 c_2)) (not (p6 c_2 c_4)) )(or (= (f5 c_2 c_5) c10) (not (p8 c_2)) (not (p6 c_2 c_5)) )(or (= (f5 c_3 c_0) c10) (not (p8 c_3)) (not (p6 c_3 c_0)) )(or (= (f5 c_3 c_1) c10) (not (p8 c_3)) (not (p6 c_3 c_1)) )(or (= (f5 c_3 c_2) c10) (not (p8 c_3)) (not (p6 c_3 c_2)) )(or (= (f5 c_3 c_3) c10) (not (p8 c_3)) (not (p6 c_3 c_3)) )(or (= (f5 c_3 c_4) c10) (not (p8 c_3)) (not (p6 c_3 c_4)) )(or (= (f5 c_3 c_5) c10) (not (p8 c_3)) (not (p6 c_3 c_5)) )(or (= (f5 c_4 c_0) c10) (not (p8 c_4)) (not (p6 c_4 c_0)) )(or (= (f5 c_4 c_1) c10) (not (p8 c_4)) (not (p6 c_4 c_1)) )(or (= (f5 c_4 c_2) c10) (not (p8 c_4)) (not (p6 c_4 c_2)) )(or (= (f5 c_4 c_3) c10) (not (p8 c_4)) (not (p6 c_4 c_3)) )(or (= (f5 c_4 c_4) c10) (not (p8 c_4)) (not (p6 c_4 c_4)) )(or (= (f5 c_4 c_5) c10) (not (p8 c_4)) (not (p6 c_4 c_5)) )(or (= (f5 c_5 c_0) c10) (not (p8 c_5)) (not (p6 c_5 c_0)) )(or (= (f5 c_5 c_1) c10) (not (p8 c_5)) (not (p6 c_5 c_1)) )(or (= (f5 c_5 c_2) c10) (not (p8 c_5)) (not (p6 c_5 c_2)) )(or (= (f5 c_5 c_3) c10) (not (p8 c_5)) (not (p6 c_5 c_3)) )(or (= (f5 c_5 c_4) c10) (not (p8 c_5)) (not (p6 c_5 c_4)) )(or (= (f5 c_5 c_5) c10) (not (p8 c_5)) (not (p6 c_5 c_5)) )(p6 c15 c16) (p8 c15) (not (p4 (f5 c15 c17) (f5 c15 c16))) (or (= c_0 c_0) (p4 c_0 c_0) (p2 c_0 c_0) )(or (= c_0 c_1) (p4 c_0 c_1) (p2 c_0 c_1) )(or (= c_0 c_2) (p4 c_0 c_2) (p2 c_0 c_2) )(or (= c_0 c_3) (p4 c_0 c_3) (p2 c_0 c_3) )(or (= c_0 c_4) (p4 c_0 c_4) (p2 c_0 c_4) )(or (= c_0 c_5) (p4 c_0 c_5) (p2 c_0 c_5) )(or (= c_1 c_0) (p4 c_1 c_0) (p2 c_1 c_0) )(or (= c_1 c_1) (p4 c_1 c_1) (p2 c_1 c_1) )(or (= c_1 c_2) (p4 c_1 c_2) (p2 c_1 c_2) )(or (= c_1 c_3) (p4 c_1 c_3) (p2 c_1 c_3) )(or (= c_1 c_4) (p4 c_1 c_4) (p2 c_1 c_4) )(or (= c_1 c_5) (p4 c_1 c_5) (p2 c_1 c_5) )(or (= c_2 c_0) (p4 c_2 c_0) (p2 c_2 c_0) )(or (= c_2 c_1) (p4 c_2 c_1) (p2 c_2 c_1) )(or (= c_2 c_2) (p4 c_2 c_2) (p2 c_2 c_2) )(or (= c_2 c_3) (p4 c_2 c_3) (p2 c_2 c_3) )(or (= c_2 c_4) (p4 c_2 c_4) (p2 c_2 c_4) )(or (= c_2 c_5) (p4 c_2 c_5) (p2 c_2 c_5) )(or (= c_3 c_0) (p4 c_3 c_0) (p2 c_3 c_0) )(or (= c_3 c_1) (p4 c_3 c_1) (p2 c_3 c_1) )(or (= c_3 c_2) (p4 c_3 c_2) (p2 c_3 c_2) )(or (= c_3 c_3) (p4 c_3 c_3) (p2 c_3 c_3) )(or (= c_3 c_4) (p4 c_3 c_4) (p2 c_3 c_4) )(or (= c_3 c_5) (p4 c_3 c_5) (p2 c_3 c_5) )(or (= c_4 c_0) (p4 c_4 c_0) (p2 c_4 c_0) )(or (= c_4 c_1) (p4 c_4 c_1) (p2 c_4 c_1) )(or (= c_4 c_2) (p4 c_4 c_2) (p2 c_4 c_2) )(or (= c_4 c_3) (p4 c_4 c_3) (p2 c_4 c_3) )(or (= c_4 c_4) (p4 c_4 c_4) (p2 c_4 c_4) )(or (= c_4 c_5) (p4 c_4 c_5) (p2 c_4 c_5) )(or (= c_5 c_0) (p4 c_5 c_0) (p2 c_5 c_0) )(or (= c_5 c_1) (p4 c_5 c_1) (p2 c_5 c_1) )(or (= c_5 c_2) (p4 c_5 c_2) (p2 c_5 c_2) )(or (= c_5 c_3) (p4 c_5 c_3) (p2 c_5 c_3) )(or (= c_5 c_4) (p4 c_5 c_4) (p2 c_5 c_4) )(or (= c_5 c_5) (p4 c_5 c_5) (p2 c_5 c_5) )(p4 c12 c11) (or (= c_0 c_0) (not (p1 c_0 c_0)) (p2 c_0 c_0) )(or (= c_0 c_1) (not (p1 c_0 c_1)) (p2 c_0 c_1) )(or (= c_0 c_2) (not (p1 c_0 c_2)) (p2 c_0 c_2) )(or (= c_0 c_3) (not (p1 c_0 c_3)) (p2 c_0 c_3) )(or (= c_0 c_4) (not (p1 c_0 c_4)) (p2 c_0 c_4) )(or (= c_0 c_5) (not (p1 c_0 c_5)) (p2 c_0 c_5) )(or (= c_1 c_0) (not (p1 c_1 c_0)) (p2 c_1 c_0) )(or (= c_1 c_1) (not (p1 c_1 c_1)) (p2 c_1 c_1) )(or (= c_1 c_2) (not (p1 c_1 c_2)) (p2 c_1 c_2) )(or (= c_1 c_3) (not (p1 c_1 c_3)) (p2 c_1 c_3) )(or (= c_1 c_4) (not (p1 c_1 c_4)) (p2 c_1 c_4) )(or (= c_1 c_5) (not (p1 c_1 c_5)) (p2 c_1 c_5) )(or (= c_2 c_0) (not (p1 c_2 c_0)) (p2 c_2 c_0) )(or (= c_2 c_1) (not (p1 c_2 c_1)) (p2 c_2 c_1) )(or (= c_2 c_2) (not (p1 c_2 c_2)) (p2 c_2 c_2) )(or (= c_2 c_3) (not (p1 c_2 c_3)) (p2 c_2 c_3) )(or (= c_2 c_4) (not (p1 c_2 c_4)) (p2 c_2 c_4) )(or (= c_2 c_5) (not (p1 c_2 c_5)) (p2 c_2 c_5) )(or (= c_3 c_0) (not (p1 c_3 c_0)) (p2 c_3 c_0) )(or (= c_3 c_1) (not (p1 c_3 c_1)) (p2 c_3 c_1) )(or (= c_3 c_2) (not (p1 c_3 c_2)) (p2 c_3 c_2) )(or (= c_3 c_3) (not (p1 c_3 c_3)) (p2 c_3 c_3) )(or (= c_3 c_4) (not (p1 c_3 c_4)) (p2 c_3 c_4) )(or (= c_3 c_5) (not (p1 c_3 c_5)) (p2 c_3 c_5) )(or (= c_4 c_0) (not (p1 c_4 c_0)) (p2 c_4 c_0) )(or (= c_4 c_1) (not (p1 c_4 c_1)) (p2 c_4 c_1) )(or (= c_4 c_2) (not (p1 c_4 c_2)) (p2 c_4 c_2) )(or (= c_4 c_3) (not (p1 c_4 c_3)) (p2 c_4 c_3) )(or (= c_4 c_4) (not (p1 c_4 c_4)) (p2 c_4 c_4) )(or (= c_4 c_5) (not (p1 c_4 c_5)) (p2 c_4 c_5) )(or (= c_5 c_0) (not (p1 c_5 c_0)) (p2 c_5 c_0) )(or (= c_5 c_1) (not (p1 c_5 c_1)) (p2 c_5 c_1) )(or (= c_5 c_2) (not (p1 c_5 c_2)) (p2 c_5 c_2) )(or (= c_5 c_3) (not (p1 c_5 c_3)) (p2 c_5 c_3) )(or (= c_5 c_4) (not (p1 c_5 c_4)) (p2 c_5 c_4) )(or (= c_5 c_5) (not (p1 c_5 c_5)) (p2 c_5 c_5) )(or (p4 c_0 c_0) (not (p2 c_0 c_0)) )(or (p4 c_0 c_1) (not (p2 c_1 c_0)) )(or (p4 c_0 c_2) (not (p2 c_2 c_0)) )(or (p4 c_0 c_3) (not (p2 c_3 c_0)) )(or (p4 c_0 c_4) (not (p2 c_4 c_0)) )(or (p4 c_0 c_5) (not (p2 c_5 c_0)) )(or (p4 c_1 c_0) (not (p2 c_0 c_1)) )(or (p4 c_1 c_1) (not (p2 c_1 c_1)) )(or (p4 c_1 c_2) (not (p2 c_2 c_1)) )(or (p4 c_1 c_3) (not (p2 c_3 c_1)) )(or (p4 c_1 c_4) (not (p2 c_4 c_1)) )(or (p4 c_1 c_5) (not (p2 c_5 c_1)) )(or (p4 c_2 c_0) (not (p2 c_0 c_2)) )(or (p4 c_2 c_1) (not (p2 c_1 c_2)) )(or (p4 c_2 c_2) (not (p2 c_2 c_2)) )(or (p4 c_2 c_3) (not (p2 c_3 c_2)) )(or (p4 c_2 c_4) (not (p2 c_4 c_2)) )(or (p4 c_2 c_5) (not (p2 c_5 c_2)) )(or (p4 c_3 c_0) (not (p2 c_0 c_3)) )(or (p4 c_3 c_1) (not (p2 c_1 c_3)) )(or (p4 c_3 c_2) (not (p2 c_2 c_3)) )(or (p4 c_3 c_3) (not (p2 c_3 c_3)) )(or (p4 c_3 c_4) (not (p2 c_4 c_3)) )(or (p4 c_3 c_5) (not (p2 c_5 c_3)) )(or (p4 c_4 c_0) (not (p2 c_0 c_4)) )(or (p4 c_4 c_1) (not (p2 c_1 c_4)) )(or (p4 c_4 c_2) (not (p2 c_2 c_4)) )(or (p4 c_4 c_3) (not (p2 c_3 c_4)) )(or (p4 c_4 c_4) (not (p2 c_4 c_4)) )(or (p4 c_4 c_5) (not (p2 c_5 c_4)) )(or (p4 c_5 c_0) (not (p2 c_0 c_5)) )(or (p4 c_5 c_1) (not (p2 c_1 c_5)) )(or (p4 c_5 c_2) (not (p2 c_2 c_5)) )(or (p4 c_5 c_3) (not (p2 c_3 c_5)) )(or (p4 c_5 c_4) (not (p2 c_4 c_5)) )(or (p4 c_5 c_5) (not (p2 c_5 c_5)) )(or (= c_0 c_0) (p4 c_0 c_0) (not (p3 c_0 c_0)) )(or (= c_0 c_1) (p4 c_0 c_1) (not (p3 c_0 c_1)) )(or (= c_0 c_2) (p4 c_0 c_2) (not (p3 c_0 c_2)) )(or (= c_0 c_3) (p4 c_0 c_3) (not (p3 c_0 c_3)) )(or (= c_0 c_4) (p4 c_0 c_4) (not (p3 c_0 c_4)) )(or (= c_0 c_5) (p4 c_0 c_5) (not (p3 c_0 c_5)) )(or (= c_1 c_0) (p4 c_1 c_0) (not (p3 c_1 c_0)) )(or (= c_1 c_1) (p4 c_1 c_1) (not (p3 c_1 c_1)) )(or (= c_1 c_2) (p4 c_1 c_2) (not (p3 c_1 c_2)) )(or (= c_1 c_3) (p4 c_1 c_3) (not (p3 c_1 c_3)) )(or (= c_1 c_4) (p4 c_1 c_4) (not (p3 c_1 c_4)) )(or (= c_1 c_5) (p4 c_1 c_5) (not (p3 c_1 c_5)) )(or (= c_2 c_0) (p4 c_2 c_0) (not (p3 c_2 c_0)) )(or (= c_2 c_1) (p4 c_2 c_1) (not (p3 c_2 c_1)) )(or (= c_2 c_2) (p4 c_2 c_2) (not (p3 c_2 c_2)) )(or (= c_2 c_3) (p4 c_2 c_3) (not (p3 c_2 c_3)) )(or (= c_2 c_4) (p4 c_2 c_4) (not (p3 c_2 c_4)) )(or (= c_2 c_5) (p4 c_2 c_5) (not (p3 c_2 c_5)) )(or (= c_3 c_0) (p4 c_3 c_0) (not (p3 c_3 c_0)) )(or (= c_3 c_1) (p4 c_3 c_1) (not (p3 c_3 c_1)) )(or (= c_3 c_2) (p4 c_3 c_2) (not (p3 c_3 c_2)) )(or (= c_3 c_3) (p4 c_3 c_3) (not (p3 c_3 c_3)) )(or (= c_3 c_4) (p4 c_3 c_4) (not (p3 c_3 c_4)) )(or (= c_3 c_5) (p4 c_3 c_5) (not (p3 c_3 c_5)) )(or (= c_4 c_0) (p4 c_4 c_0) (not (p3 c_4 c_0)) )(or (= c_4 c_1) (p4 c_4 c_1) (not (p3 c_4 c_1)) )(or (= c_4 c_2) (p4 c_4 c_2) (not (p3 c_4 c_2)) )(or (= c_4 c_3) (p4 c_4 c_3) (not (p3 c_4 c_3)) )(or (= c_4 c_4) (p4 c_4 c_4) (not (p3 c_4 c_4)) )(or (= c_4 c_5) (p4 c_4 c_5) (not (p3 c_4 c_5)) )(or (= c_5 c_0) (p4 c_5 c_0) (not (p3 c_5 c_0)) )(or (= c_5 c_1) (p4 c_5 c_1) (not (p3 c_5 c_1)) )(or (= c_5 c_2) (p4 c_5 c_2) (not (p3 c_5 c_2)) )(or (= c_5 c_3) (p4 c_5 c_3) (not (p3 c_5 c_3)) )(or (= c_5 c_4) (p4 c_5 c_4) (not (p3 c_5 c_4)) )(or (= c_5 c_5) (p4 c_5 c_5) (not (p3 c_5 c_5)) )(p4 c11 c10) (or (not (p4 c_0 c_0)) (p4 c_0 c_0) (not (p4 c_0 c_0)) )(or (not (p4 c_0 c_0)) (p4 c_0 c_1) (not (p4 c_0 c_1)) )(or (not (p4 c_0 c_0)) (p4 c_0 c_2) (not (p4 c_0 c_2)) )(or (not (p4 c_0 c_0)) (p4 c_0 c_3) (not (p4 c_0 c_3)) )(or (not (p4 c_0 c_0)) (p4 c_0 c_4) (not (p4 c_0 c_4)) )(or (not (p4 c_0 c_0)) (p4 c_0 c_5) (not (p4 c_0 c_5)) )(or (not (p4 c_0 c_1)) (p4 c_0 c_0) (not (p4 c_1 c_0)) )(or (not (p4 c_0 c_1)) (p4 c_0 c_1) (not (p4 c_1 c_1)) )(or (not (p4 c_0 c_1)) (p4 c_0 c_2) (not (p4 c_1 c_2)) )(or (not (p4 c_0 c_1)) (p4 c_0 c_3) (not (p4 c_1 c_3)) )(or (not (p4 c_0 c_1)) (p4 c_0 c_4) (not (p4 c_1 c_4)) )(or (not (p4 c_0 c_1)) (p4 c_0 c_5) (not (p4 c_1 c_5)) )(or (not (p4 c_0 c_2)) (p4 c_0 c_0) (not (p4 c_2 c_0)) )(or (not (p4 c_0 c_2)) (p4 c_0 c_1) (not (p4 c_2 c_1)) )(or (not (p4 c_0 c_2)) (p4 c_0 c_2) (not (p4 c_2 c_2)) )(or (not (p4 c_0 c_2)) (p4 c_0 c_3) (not (p4 c_2 c_3)) )(or (not (p4 c_0 c_2)) (p4 c_0 c_4) (not (p4 c_2 c_4)) )(or (not (p4 c_0 c_2)) (p4 c_0 c_5) (not (p4 c_2 c_5)) )(or (not (p4 c_0 c_3)) (p4 c_0 c_0) (not (p4 c_3 c_0)) )(or (not (p4 c_0 c_3)) (p4 c_0 c_1) (not (p4 c_3 c_1)) )(or (not (p4 c_0 c_3)) (p4 c_0 c_2) (not (p4 c_3 c_2)) )(or (not (p4 c_0 c_3)) (p4 c_0 c_3) (not (p4 c_3 c_3)) )(or (not (p4 c_0 c_3)) (p4 c_0 c_4) (not (p4 c_3 c_4)) )(or (not (p4 c_0 c_3)) (p4 c_0 c_5) (not (p4 c_3 c_5)) )(or (not (p4 c_0 c_4)) (p4 c_0 c_0) (not (p4 c_4 c_0)) )(or (not (p4 c_0 c_4)) (p4 c_0 c_1) (not (p4 c_4 c_1)) )(or (not (p4 c_0 c_4)) (p4 c_0 c_2) (not (p4 c_4 c_2)) )(or (not (p4 c_0 c_4)) (p4 c_0 c_3) (not (p4 c_4 c_3)) )(or (not (p4 c_0 c_4)) (p4 c_0 c_4) (not (p4 c_4 c_4)) )(or (not (p4 c_0 c_4)) (p4 c_0 c_5) (not (p4 c_4 c_5)) )(or (not (p4 c_0 c_5)) (p4 c_0 c_0) (not (p4 c_5 c_0)) )(or (not (p4 c_0 c_5)) (p4 c_0 c_1) (not (p4 c_5 c_1)) )(or (not (p4 c_0 c_5)) (p4 c_0 c_2) (not (p4 c_5 c_2)) )(or (not (p4 c_0 c_5)) (p4 c_0 c_3) (not (p4 c_5 c_3)) )(or (not (p4 c_0 c_5)) (p4 c_0 c_4) (not (p4 c_5 c_4)) )(or (not (p4 c_0 c_5)) (p4 c_0 c_5) (not (p4 c_5 c_5)) )(or (not (p4 c_1 c_0)) (p4 c_1 c_0) (not (p4 c_0 c_0)) )(or (not (p4 c_1 c_0)) (p4 c_1 c_1) (not (p4 c_0 c_1)) )(or (not (p4 c_1 c_0)) (p4 c_1 c_2) (not (p4 c_0 c_2)) )(or (not (p4 c_1 c_0)) (p4 c_1 c_3) (not (p4 c_0 c_3)) )(or (not (p4 c_1 c_0)) (p4 c_1 c_4) (not (p4 c_0 c_4)) )(or (not (p4 c_1 c_0)) (p4 c_1 c_5) (not (p4 c_0 c_5)) )(or (not (p4 c_1 c_1)) (p4 c_1 c_0) (not (p4 c_1 c_0)) )(or (not (p4 c_1 c_1)) (p4 c_1 c_1) (not (p4 c_1 c_1)) )(or (not (p4 c_1 c_1)) (p4 c_1 c_2) (not (p4 c_1 c_2)) )(or (not (p4 c_1 c_1)) (p4 c_1 c_3) (not (p4 c_1 c_3)) )(or (not (p4 c_1 c_1)) (p4 c_1 c_4) (not (p4 c_1 c_4)) )(or (not (p4 c_1 c_1)) (p4 c_1 c_5) (not (p4 c_1 c_5)) )(or (not (p4 c_1 c_2)) (p4 c_1 c_0) (not (p4 c_2 c_0)) )(or (not (p4 c_1 c_2)) (p4 c_1 c_1) (not (p4 c_2 c_1)) )(or (not (p4 c_1 c_2)) (p4 c_1 c_2) (not (p4 c_2 c_2)) )(or (not (p4 c_1 c_2)) (p4 c_1 c_3) (not (p4 c_2 c_3)) )(or (not (p4 c_1 c_2)) (p4 c_1 c_4) (not (p4 c_2 c_4)) )(or (not (p4 c_1 c_2)) (p4 c_1 c_5) (not (p4 c_2 c_5)) )(or (not (p4 c_1 c_3)) (p4 c_1 c_0) (not (p4 c_3 c_0)) )(or (not (p4 c_1 c_3)) (p4 c_1 c_1) (not (p4 c_3 c_1)) )(or (not (p4 c_1 c_3)) (p4 c_1 c_2) (not (p4 c_3 c_2)) )(or (not (p4 c_1 c_3)) (p4 c_1 c_3) (not (p4 c_3 c_3)) )(or (not (p4 c_1 c_3)) (p4 c_1 c_4) (not (p4 c_3 c_4)) )(or (not (p4 c_1 c_3)) (p4 c_1 c_5) (not (p4 c_3 c_5)) )(or (not (p4 c_1 c_4)) (p4 c_1 c_0) (not (p4 c_4 c_0)) )(or (not (p4 c_1 c_4)) (p4 c_1 c_1) (not (p4 c_4 c_1)) )(or (not (p4 c_1 c_4)) (p4 c_1 c_2) (not (p4 c_4 c_2)) )(or (not (p4 c_1 c_4)) (p4 c_1 c_3) (not (p4 c_4 c_3)) )(or (not (p4 c_1 c_4)) (p4 c_1 c_4) (not (p4 c_4 c_4)) )(or (not (p4 c_1 c_4)) (p4 c_1 c_5) (not (p4 c_4 c_5)) )(or (not (p4 c_1 c_5)) (p4 c_1 c_0) (not (p4 c_5 c_0)) )(or (not (p4 c_1 c_5)) (p4 c_1 c_1) (not (p4 c_5 c_1)) )(or (not (p4 c_1 c_5)) (p4 c_1 c_2) (not (p4 c_5 c_2)) )(or (not (p4 c_1 c_5)) (p4 c_1 c_3) (not (p4 c_5 c_3)) )(or (not (p4 c_1 c_5)) (p4 c_1 c_4) (not (p4 c_5 c_4)) )(or (not (p4 c_1 c_5)) (p4 c_1 c_5) (not (p4 c_5 c_5)) )(or (not (p4 c_2 c_0)) (p4 c_2 c_0) (not (p4 c_0 c_0)) )(or (not (p4 c_2 c_0)) (p4 c_2 c_1) (not (p4 c_0 c_1)) )(or (not (p4 c_2 c_0)) (p4 c_2 c_2) (not (p4 c_0 c_2)) )(or (not (p4 c_2 c_0)) (p4 c_2 c_3) (not (p4 c_0 c_3)) )(or (not (p4 c_2 c_0)) (p4 c_2 c_4) (not (p4 c_0 c_4)) )(or (not (p4 c_2 c_0)) (p4 c_2 c_5) (not (p4 c_0 c_5)) )(or (not (p4 c_2 c_1)) (p4 c_2 c_0) (not (p4 c_1 c_0)) )(or (not (p4 c_2 c_1)) (p4 c_2 c_1) (not (p4 c_1 c_1)) )(or (not (p4 c_2 c_1)) (p4 c_2 c_2) (not (p4 c_1 c_2)) )(or (not (p4 c_2 c_1)) (p4 c_2 c_3) (not (p4 c_1 c_3)) )(or (not (p4 c_2 c_1)) (p4 c_2 c_4) (not (p4 c_1 c_4)) )(or (not (p4 c_2 c_1)) (p4 c_2 c_5) (not (p4 c_1 c_5)) )(or (not (p4 c_2 c_2)) (p4 c_2 c_0) (not (p4 c_2 c_0)) )(or (not (p4 c_2 c_2)) (p4 c_2 c_1) (not (p4 c_2 c_1)) )(or (not (p4 c_2 c_2)) (p4 c_2 c_2) (not (p4 c_2 c_2)) )(or (not (p4 c_2 c_2)) (p4 c_2 c_3) (not (p4 c_2 c_3)) )(or (not (p4 c_2 c_2)) (p4 c_2 c_4) (not (p4 c_2 c_4)) )(or (not (p4 c_2 c_2)) (p4 c_2 c_5) (not (p4 c_2 c_5)) )(or (not (p4 c_2 c_3)) (p4 c_2 c_0) (not (p4 c_3 c_0)) )(or (not (p4 c_2 c_3)) (p4 c_2 c_1) (not (p4 c_3 c_1)) )(or (not (p4 c_2 c_3)) (p4 c_2 c_2) (not (p4 c_3 c_2)) )(or (not (p4 c_2 c_3)) (p4 c_2 c_3) (not (p4 c_3 c_3)) )(or (not (p4 c_2 c_3)) (p4 c_2 c_4) (not (p4 c_3 c_4)) )(or (not (p4 c_2 c_3)) (p4 c_2 c_5) (not (p4 c_3 c_5)) )(or (not (p4 c_2 c_4)) (p4 c_2 c_0) (not (p4 c_4 c_0)) )(or (not (p4 c_2 c_4)) (p4 c_2 c_1) (not (p4 c_4 c_1)) )(or (not (p4 c_2 c_4)) (p4 c_2 c_2) (not (p4 c_4 c_2)) )(or (not (p4 c_2 c_4)) (p4 c_2 c_3) (not (p4 c_4 c_3)) )(or (not (p4 c_2 c_4)) (p4 c_2 c_4) (not (p4 c_4 c_4)) )(or (not (p4 c_2 c_4)) (p4 c_2 c_5) (not (p4 c_4 c_5)) )(or (not (p4 c_2 c_5)) (p4 c_2 c_0) (not (p4 c_5 c_0)) )(or (not (p4 c_2 c_5)) (p4 c_2 c_1) (not (p4 c_5 c_1)) )(or (not (p4 c_2 c_5)) (p4 c_2 c_2) (not (p4 c_5 c_2)) )(or (not (p4 c_2 c_5)) (p4 c_2 c_3) (not (p4 c_5 c_3)) )(or (not (p4 c_2 c_5)) (p4 c_2 c_4) (not (p4 c_5 c_4)) )(or (not (p4 c_2 c_5)) (p4 c_2 c_5) (not (p4 c_5 c_5)) )(or (not (p4 c_3 c_0)) (p4 c_3 c_0) (not (p4 c_0 c_0)) )(or (not (p4 c_3 c_0)) (p4 c_3 c_1) (not (p4 c_0 c_1)) )(or (not (p4 c_3 c_0)) (p4 c_3 c_2) (not (p4 c_0 c_2)) )(or (not (p4 c_3 c_0)) (p4 c_3 c_3) (not (p4 c_0 c_3)) )(or (not (p4 c_3 c_0)) (p4 c_3 c_4) (not (p4 c_0 c_4)) )(or (not (p4 c_3 c_0)) (p4 c_3 c_5) (not (p4 c_0 c_5)) )(or (not (p4 c_3 c_1)) (p4 c_3 c_0) (not (p4 c_1 c_0)) )(or (not (p4 c_3 c_1)) (p4 c_3 c_1) (not (p4 c_1 c_1)) )(or (not (p4 c_3 c_1)) (p4 c_3 c_2) (not (p4 c_1 c_2)) )(or (not (p4 c_3 c_1)) (p4 c_3 c_3) (not (p4 c_1 c_3)) )(or (not (p4 c_3 c_1)) (p4 c_3 c_4) (not (p4 c_1 c_4)) )(or (not (p4 c_3 c_1)) (p4 c_3 c_5) (not (p4 c_1 c_5)) )(or (not (p4 c_3 c_2)) (p4 c_3 c_0) (not (p4 c_2 c_0)) )(or (not (p4 c_3 c_2)) (p4 c_3 c_1) (not (p4 c_2 c_1)) )(or (not (p4 c_3 c_2)) (p4 c_3 c_2) (not (p4 c_2 c_2)) )(or (not (p4 c_3 c_2)) (p4 c_3 c_3) (not (p4 c_2 c_3)) )(or (not (p4 c_3 c_2)) (p4 c_3 c_4) (not (p4 c_2 c_4)) )(or (not (p4 c_3 c_2)) (p4 c_3 c_5) (not (p4 c_2 c_5)) )(or (not (p4 c_3 c_3)) (p4 c_3 c_0) (not (p4 c_3 c_0)) )(or (not (p4 c_3 c_3)) (p4 c_3 c_1) (not (p4 c_3 c_1)) )(or (not (p4 c_3 c_3)) (p4 c_3 c_2) (not (p4 c_3 c_2)) )(or (not (p4 c_3 c_3)) (p4 c_3 c_3) (not (p4 c_3 c_3)) )(or (not (p4 c_3 c_3)) (p4 c_3 c_4) (not (p4 c_3 c_4)) )(or (not (p4 c_3 c_3)) (p4 c_3 c_5) (not (p4 c_3 c_5)) )(or (not (p4 c_3 c_4)) (p4 c_3 c_0) (not (p4 c_4 c_0)) )(or (not (p4 c_3 c_4)) (p4 c_3 c_1) (not (p4 c_4 c_1)) )(or (not (p4 c_3 c_4)) (p4 c_3 c_2) (not (p4 c_4 c_2)) )(or (not (p4 c_3 c_4)) (p4 c_3 c_3) (not (p4 c_4 c_3)) )(or (not (p4 c_3 c_4)) (p4 c_3 c_4) (not (p4 c_4 c_4)) )(or (not (p4 c_3 c_4)) (p4 c_3 c_5) (not (p4 c_4 c_5)) )(or (not (p4 c_3 c_5)) (p4 c_3 c_0) (not (p4 c_5 c_0)) )(or (not (p4 c_3 c_5)) (p4 c_3 c_1) (not (p4 c_5 c_1)) )(or (not (p4 c_3 c_5)) (p4 c_3 c_2) (not (p4 c_5 c_2)) )(or (not (p4 c_3 c_5)) (p4 c_3 c_3) (not (p4 c_5 c_3)) )(or (not (p4 c_3 c_5)) (p4 c_3 c_4) (not (p4 c_5 c_4)) )(or (not (p4 c_3 c_5)) (p4 c_3 c_5) (not (p4 c_5 c_5)) )(or (not (p4 c_4 c_0)) (p4 c_4 c_0) (not (p4 c_0 c_0)) )(or (not (p4 c_4 c_0)) (p4 c_4 c_1) (not (p4 c_0 c_1)) )(or (not (p4 c_4 c_0)) (p4 c_4 c_2) (not (p4 c_0 c_2)) )(or (not (p4 c_4 c_0)) (p4 c_4 c_3) (not (p4 c_0 c_3)) )(or (not (p4 c_4 c_0)) (p4 c_4 c_4) (not (p4 c_0 c_4)) )(or (not (p4 c_4 c_0)) (p4 c_4 c_5) (not (p4 c_0 c_5)) )(or (not (p4 c_4 c_1)) (p4 c_4 c_0) (not (p4 c_1 c_0)) )(or (not (p4 c_4 c_1)) (p4 c_4 c_1) (not (p4 c_1 c_1)) )(or (not (p4 c_4 c_1)) (p4 c_4 c_2) (not (p4 c_1 c_2)) )(or (not (p4 c_4 c_1)) (p4 c_4 c_3) (not (p4 c_1 c_3)) )(or (not (p4 c_4 c_1)) (p4 c_4 c_4) (not (p4 c_1 c_4)) )(or (not (p4 c_4 c_1)) (p4 c_4 c_5) (not (p4 c_1 c_5)) )(or (not (p4 c_4 c_2)) (p4 c_4 c_0) (not (p4 c_2 c_0)) )(or (not (p4 c_4 c_2)) (p4 c_4 c_1) (not (p4 c_2 c_1)) )(or (not (p4 c_4 c_2)) (p4 c_4 c_2) (not (p4 c_2 c_2)) )(or (not (p4 c_4 c_2)) (p4 c_4 c_3) (not (p4 c_2 c_3)) )(or (not (p4 c_4 c_2)) (p4 c_4 c_4) (not (p4 c_2 c_4)) )(or (not (p4 c_4 c_2)) (p4 c_4 c_5) (not (p4 c_2 c_5)) )(or (not (p4 c_4 c_3)) (p4 c_4 c_0) (not (p4 c_3 c_0)) )(or (not (p4 c_4 c_3)) (p4 c_4 c_1) (not (p4 c_3 c_1)) )(or (not (p4 c_4 c_3)) (p4 c_4 c_2) (not (p4 c_3 c_2)) )(or (not (p4 c_4 c_3)) (p4 c_4 c_3) (not (p4 c_3 c_3)) )(or (not (p4 c_4 c_3)) (p4 c_4 c_4) (not (p4 c_3 c_4)) )(or (not (p4 c_4 c_3)) (p4 c_4 c_5) (not (p4 c_3 c_5)) )(or (not (p4 c_4 c_4)) (p4 c_4 c_0) (not (p4 c_4 c_0)) )(or (not (p4 c_4 c_4)) (p4 c_4 c_1) (not (p4 c_4 c_1)) )(or (not (p4 c_4 c_4)) (p4 c_4 c_2) (not (p4 c_4 c_2)) )(or (not (p4 c_4 c_4)) (p4 c_4 c_3) (not (p4 c_4 c_3)) )(or (not (p4 c_4 c_4)) (p4 c_4 c_4) (not (p4 c_4 c_4)) )(or (not (p4 c_4 c_4)) (p4 c_4 c_5) (not (p4 c_4 c_5)) )(or (not (p4 c_4 c_5)) (p4 c_4 c_0) (not (p4 c_5 c_0)) )(or (not (p4 c_4 c_5)) (p4 c_4 c_1) (not (p4 c_5 c_1)) )(or (not (p4 c_4 c_5)) (p4 c_4 c_2) (not (p4 c_5 c_2)) )(or (not (p4 c_4 c_5)) (p4 c_4 c_3) (not (p4 c_5 c_3)) )(or (not (p4 c_4 c_5)) (p4 c_4 c_4) (not (p4 c_5 c_4)) )(or (not (p4 c_4 c_5)) (p4 c_4 c_5) (not (p4 c_5 c_5)) )(or (not (p4 c_5 c_0)) (p4 c_5 c_0) (not (p4 c_0 c_0)) )(or (not (p4 c_5 c_0)) (p4 c_5 c_1) (not (p4 c_0 c_1)) )(or (not (p4 c_5 c_0)) (p4 c_5 c_2) (not (p4 c_0 c_2)) )(or (not (p4 c_5 c_0)) (p4 c_5 c_3) (not (p4 c_0 c_3)) )(or (not (p4 c_5 c_0)) (p4 c_5 c_4) (not (p4 c_0 c_4)) )(or (not (p4 c_5 c_0)) (p4 c_5 c_5) (not (p4 c_0 c_5)) )(or (not (p4 c_5 c_1)) (p4 c_5 c_0) (not (p4 c_1 c_0)) )(or (not (p4 c_5 c_1)) (p4 c_5 c_1) (not (p4 c_1 c_1)) )(or (not (p4 c_5 c_1)) (p4 c_5 c_2) (not (p4 c_1 c_2)) )(or (not (p4 c_5 c_1)) (p4 c_5 c_3) (not (p4 c_1 c_3)) )(or (not (p4 c_5 c_1)) (p4 c_5 c_4) (not (p4 c_1 c_4)) )(or (not (p4 c_5 c_1)) (p4 c_5 c_5) (not (p4 c_1 c_5)) )(or (not (p4 c_5 c_2)) (p4 c_5 c_0) (not (p4 c_2 c_0)) )(or (not (p4 c_5 c_2)) (p4 c_5 c_1) (not (p4 c_2 c_1)) )(or (not (p4 c_5 c_2)) (p4 c_5 c_2) (not (p4 c_2 c_2)) )(or (not (p4 c_5 c_2)) (p4 c_5 c_3) (not (p4 c_2 c_3)) )(or (not (p4 c_5 c_2)) (p4 c_5 c_4) (not (p4 c_2 c_4)) )(or (not (p4 c_5 c_2)) (p4 c_5 c_5) (not (p4 c_2 c_5)) )(or (not (p4 c_5 c_3)) (p4 c_5 c_0) (not (p4 c_3 c_0)) )(or (not (p4 c_5 c_3)) (p4 c_5 c_1) (not (p4 c_3 c_1)) )(or (not (p4 c_5 c_3)) (p4 c_5 c_2) (not (p4 c_3 c_2)) )(or (not (p4 c_5 c_3)) (p4 c_5 c_3) (not (p4 c_3 c_3)) )(or (not (p4 c_5 c_3)) (p4 c_5 c_4) (not (p4 c_3 c_4)) )(or (not (p4 c_5 c_3)) (p4 c_5 c_5) (not (p4 c_3 c_5)) )(or (not (p4 c_5 c_4)) (p4 c_5 c_0) (not (p4 c_4 c_0)) )(or (not (p4 c_5 c_4)) (p4 c_5 c_1) (not (p4 c_4 c_1)) )(or (not (p4 c_5 c_4)) (p4 c_5 c_2) (not (p4 c_4 c_2)) )(or (not (p4 c_5 c_4)) (p4 c_5 c_3) (not (p4 c_4 c_3)) )(or (not (p4 c_5 c_4)) (p4 c_5 c_4) (not (p4 c_4 c_4)) )(or (not (p4 c_5 c_4)) (p4 c_5 c_5) (not (p4 c_4 c_5)) )(or (not (p4 c_5 c_5)) (p4 c_5 c_0) (not (p4 c_5 c_0)) )(or (not (p4 c_5 c_5)) (p4 c_5 c_1) (not (p4 c_5 c_1)) )(or (not (p4 c_5 c_5)) (p4 c_5 c_2) (not (p4 c_5 c_2)) )(or (not (p4 c_5 c_5)) (p4 c_5 c_3) (not (p4 c_5 c_3)) )(or (not (p4 c_5 c_5)) (p4 c_5 c_4) (not (p4 c_5 c_4)) )(or (not (p4 c_5 c_5)) (p4 c_5 c_5) (not (p4 c_5 c_5)) )(or (not (p9 c_0 c_0)) (p6 c_0 c_0) (not (p8 c_0)) (not (p7 c_0 c_0)) (= (f5 c_0 c_0) c11) )(or (not (p9 c_0 c_1)) (p6 c_0 c_1) (not (p8 c_0)) (not (p7 c_0 c_1)) (= (f5 c_0 c_1) c11) )(or (not (p9 c_0 c_2)) (p6 c_0 c_2) (not (p8 c_0)) (not (p7 c_0 c_2)) (= (f5 c_0 c_2) c11) )(or (not (p9 c_0 c_3)) (p6 c_0 c_3) (not (p8 c_0)) (not (p7 c_0 c_3)) (= (f5 c_0 c_3) c11) )(or (not (p9 c_0 c_4)) (p6 c_0 c_4) (not (p8 c_0)) (not (p7 c_0 c_4)) (= (f5 c_0 c_4) c11) )(or (not (p9 c_0 c_5)) (p6 c_0 c_5) (not (p8 c_0)) (not (p7 c_0 c_5)) (= (f5 c_0 c_5) c11) )(or (not (p9 c_1 c_0)) (p6 c_1 c_0) (not (p8 c_1)) (not (p7 c_1 c_0)) (= (f5 c_1 c_0) c11) )(or (not (p9 c_1 c_1)) (p6 c_1 c_1) (not (p8 c_1)) (not (p7 c_1 c_1)) (= (f5 c_1 c_1) c11) )(or (not (p9 c_1 c_2)) (p6 c_1 c_2) (not (p8 c_1)) (not (p7 c_1 c_2)) (= (f5 c_1 c_2) c11) )(or (not (p9 c_1 c_3)) (p6 c_1 c_3) (not (p8 c_1)) (not (p7 c_1 c_3)) (= (f5 c_1 c_3) c11) )(or (not (p9 c_1 c_4)) (p6 c_1 c_4) (not (p8 c_1)) (not (p7 c_1 c_4)) (= (f5 c_1 c_4) c11) )(or (not (p9 c_1 c_5)) (p6 c_1 c_5) (not (p8 c_1)) (not (p7 c_1 c_5)) (= (f5 c_1 c_5) c11) )(or (not (p9 c_2 c_0)) (p6 c_2 c_0) (not (p8 c_2)) (not (p7 c_2 c_0)) (= (f5 c_2 c_0) c11) )(or (not (p9 c_2 c_1)) (p6 c_2 c_1) (not (p8 c_2)) (not (p7 c_2 c_1)) (= (f5 c_2 c_1) c11) )(or (not (p9 c_2 c_2)) (p6 c_2 c_2) (not (p8 c_2)) (not (p7 c_2 c_2)) (= (f5 c_2 c_2) c11) )(or (not (p9 c_2 c_3)) (p6 c_2 c_3) (not (p8 c_2)) (not (p7 c_2 c_3)) (= (f5 c_2 c_3) c11) )(or (not (p9 c_2 c_4)) (p6 c_2 c_4) (not (p8 c_2)) (not (p7 c_2 c_4)) (= (f5 c_2 c_4) c11) )(or (not (p9 c_2 c_5)) (p6 c_2 c_5) (not (p8 c_2)) (not (p7 c_2 c_5)) (= (f5 c_2 c_5) c11) )(or (not (p9 c_3 c_0)) (p6 c_3 c_0) (not (p8 c_3)) (not (p7 c_3 c_0)) (= (f5 c_3 c_0) c11) )(or (not (p9 c_3 c_1)) (p6 c_3 c_1) (not (p8 c_3)) (not (p7 c_3 c_1)) (= (f5 c_3 c_1) c11) )(or (not (p9 c_3 c_2)) (p6 c_3 c_2) (not (p8 c_3)) (not (p7 c_3 c_2)) (= (f5 c_3 c_2) c11) )(or (not (p9 c_3 c_3)) (p6 c_3 c_3) (not (p8 c_3)) (not (p7 c_3 c_3)) (= (f5 c_3 c_3) c11) )(or (not (p9 c_3 c_4)) (p6 c_3 c_4) (not (p8 c_3)) (not (p7 c_3 c_4)) (= (f5 c_3 c_4) c11) )(or (not (p9 c_3 c_5)) (p6 c_3 c_5) (not (p8 c_3)) (not (p7 c_3 c_5)) (= (f5 c_3 c_5) c11) )(or (not (p9 c_4 c_0)) (p6 c_4 c_0) (not (p8 c_4)) (not (p7 c_4 c_0)) (= (f5 c_4 c_0) c11) )(or (not (p9 c_4 c_1)) (p6 c_4 c_1) (not (p8 c_4)) (not (p7 c_4 c_1)) (= (f5 c_4 c_1) c11) )(or (not (p9 c_4 c_2)) (p6 c_4 c_2) (not (p8 c_4)) (not (p7 c_4 c_2)) (= (f5 c_4 c_2) c11) )(or (not (p9 c_4 c_3)) (p6 c_4 c_3) (not (p8 c_4)) (not (p7 c_4 c_3)) (= (f5 c_4 c_3) c11) )(or (not (p9 c_4 c_4)) (p6 c_4 c_4) (not (p8 c_4)) (not (p7 c_4 c_4)) (= (f5 c_4 c_4) c11) )(or (not (p9 c_4 c_5)) (p6 c_4 c_5) (not (p8 c_4)) (not (p7 c_4 c_5)) (= (f5 c_4 c_5) c11) )(or (not (p9 c_5 c_0)) (p6 c_5 c_0) (not (p8 c_5)) (not (p7 c_5 c_0)) (= (f5 c_5 c_0) c11) )(or (not (p9 c_5 c_1)) (p6 c_5 c_1) (not (p8 c_5)) (not (p7 c_5 c_1)) (= (f5 c_5 c_1) c11) )(or (not (p9 c_5 c_2)) (p6 c_5 c_2) (not (p8 c_5)) (not (p7 c_5 c_2)) (= (f5 c_5 c_2) c11) )(or (not (p9 c_5 c_3)) (p6 c_5 c_3) (not (p8 c_5)) (not (p7 c_5 c_3)) (= (f5 c_5 c_3) c11) )(or (not (p9 c_5 c_4)) (p6 c_5 c_4) (not (p8 c_5)) (not (p7 c_5 c_4)) (= (f5 c_5 c_4) c11) )(or (not (p9 c_5 c_5)) (p6 c_5 c_5) (not (p8 c_5)) (not (p7 c_5 c_5)) (= (f5 c_5 c_5) c11) )(or (not (p2 c_0 c_0)) (p1 c_0 c_0) )(or (not (p2 c_0 c_1)) (p1 c_0 c_1) )(or (not (p2 c_0 c_2)) (p1 c_0 c_2) )(or (not (p2 c_0 c_3)) (p1 c_0 c_3) )(or (not (p2 c_0 c_4)) (p1 c_0 c_4) )(or (not (p2 c_0 c_5)) (p1 c_0 c_5) )(or (not (p2 c_1 c_0)) (p1 c_1 c_0) )(or (not (p2 c_1 c_1)) (p1 c_1 c_1) )(or (not (p2 c_1 c_2)) (p1 c_1 c_2) )(or (not (p2 c_1 c_3)) (p1 c_1 c_3) )(or (not (p2 c_1 c_4)) (p1 c_1 c_4) )(or (not (p2 c_1 c_5)) (p1 c_1 c_5) )(or (not (p2 c_2 c_0)) (p1 c_2 c_0) )(or (not (p2 c_2 c_1)) (p1 c_2 c_1) )(or (not (p2 c_2 c_2)) (p1 c_2 c_2) )(or (not (p2 c_2 c_3)) (p1 c_2 c_3) )(or (not (p2 c_2 c_4)) (p1 c_2 c_4) )(or (not (p2 c_2 c_5)) (p1 c_2 c_5) )(or (not (p2 c_3 c_0)) (p1 c_3 c_0) )(or (not (p2 c_3 c_1)) (p1 c_3 c_1) )(or (not (p2 c_3 c_2)) (p1 c_3 c_2) )(or (not (p2 c_3 c_3)) (p1 c_3 c_3) )(or (not (p2 c_3 c_4)) (p1 c_3 c_4) )(or (not (p2 c_3 c_5)) (p1 c_3 c_5) )(or (not (p2 c_4 c_0)) (p1 c_4 c_0) )(or (not (p2 c_4 c_1)) (p1 c_4 c_1) )(or (not (p2 c_4 c_2)) (p1 c_4 c_2) )(or (not (p2 c_4 c_3)) (p1 c_4 c_3) )(or (not (p2 c_4 c_4)) (p1 c_4 c_4) )(or (not (p2 c_4 c_5)) (p1 c_4 c_5) )(or (not (p2 c_5 c_0)) (p1 c_5 c_0) )(or (not (p2 c_5 c_1)) (p1 c_5 c_1) )(or (not (p2 c_5 c_2)) (p1 c_5 c_2) )(or (not (p2 c_5 c_3)) (p1 c_5 c_3) )(or (not (p2 c_5 c_4)) (p1 c_5 c_4) )(or (not (p2 c_5 c_5)) (p1 c_5 c_5) )(or (p6 c_0 c_0) (= (f5 c_0 c_0) c13) (p9 c_0 c_0) (not (p8 c_0)) (not (p7 c_0 c_0)) )(or (p6 c_0 c_1) (= (f5 c_0 c_1) c13) (p9 c_0 c_1) (not (p8 c_0)) (not (p7 c_0 c_1)) )(or (p6 c_0 c_2) (= (f5 c_0 c_2) c13) (p9 c_0 c_2) (not (p8 c_0)) (not (p7 c_0 c_2)) )(or (p6 c_0 c_3) (= (f5 c_0 c_3) c13) (p9 c_0 c_3) (not (p8 c_0)) (not (p7 c_0 c_3)) )(or (p6 c_0 c_4) (= (f5 c_0 c_4) c13) (p9 c_0 c_4) (not (p8 c_0)) (not (p7 c_0 c_4)) )(or (p6 c_0 c_5) (= (f5 c_0 c_5) c13) (p9 c_0 c_5) (not (p8 c_0)) (not (p7 c_0 c_5)) )(or (p6 c_1 c_0) (= (f5 c_1 c_0) c13) (p9 c_1 c_0) (not (p8 c_1)) (not (p7 c_1 c_0)) )(or (p6 c_1 c_1) (= (f5 c_1 c_1) c13) (p9 c_1 c_1) (not (p8 c_1)) (not (p7 c_1 c_1)) )(or (p6 c_1 c_2) (= (f5 c_1 c_2) c13) (p9 c_1 c_2) (not (p8 c_1)) (not (p7 c_1 c_2)) )(or (p6 c_1 c_3) (= (f5 c_1 c_3) c13) (p9 c_1 c_3) (not (p8 c_1)) (not (p7 c_1 c_3)) )(or (p6 c_1 c_4) (= (f5 c_1 c_4) c13) (p9 c_1 c_4) (not (p8 c_1)) (not (p7 c_1 c_4)) )(or (p6 c_1 c_5) (= (f5 c_1 c_5) c13) (p9 c_1 c_5) (not (p8 c_1)) (not (p7 c_1 c_5)) )(or (p6 c_2 c_0) (= (f5 c_2 c_0) c13) (p9 c_2 c_0) (not (p8 c_2)) (not (p7 c_2 c_0)) )(or (p6 c_2 c_1) (= (f5 c_2 c_1) c13) (p9 c_2 c_1) (not (p8 c_2)) (not (p7 c_2 c_1)) )(or (p6 c_2 c_2) (= (f5 c_2 c_2) c13) (p9 c_2 c_2) (not (p8 c_2)) (not (p7 c_2 c_2)) )(or (p6 c_2 c_3) (= (f5 c_2 c_3) c13) (p9 c_2 c_3) (not (p8 c_2)) (not (p7 c_2 c_3)) )(or (p6 c_2 c_4) (= (f5 c_2 c_4) c13) (p9 c_2 c_4) (not (p8 c_2)) (not (p7 c_2 c_4)) )(or (p6 c_2 c_5) (= (f5 c_2 c_5) c13) (p9 c_2 c_5) (not (p8 c_2)) (not (p7 c_2 c_5)) )(or (p6 c_3 c_0) (= (f5 c_3 c_0) c13) (p9 c_3 c_0) (not (p8 c_3)) (not (p7 c_3 c_0)) )(or (p6 c_3 c_1) (= (f5 c_3 c_1) c13) (p9 c_3 c_1) (not (p8 c_3)) (not (p7 c_3 c_1)) )(or (p6 c_3 c_2) (= (f5 c_3 c_2) c13) (p9 c_3 c_2) (not (p8 c_3)) (not (p7 c_3 c_2)) )(or (p6 c_3 c_3) (= (f5 c_3 c_3) c13) (p9 c_3 c_3) (not (p8 c_3)) (not (p7 c_3 c_3)) )(or (p6 c_3 c_4) (= (f5 c_3 c_4) c13) (p9 c_3 c_4) (not (p8 c_3)) (not (p7 c_3 c_4)) )(or (p6 c_3 c_5) (= (f5 c_3 c_5) c13) (p9 c_3 c_5) (not (p8 c_3)) (not (p7 c_3 c_5)) )(or (p6 c_4 c_0) (= (f5 c_4 c_0) c13) (p9 c_4 c_0) (not (p8 c_4)) (not (p7 c_4 c_0)) )(or (p6 c_4 c_1) (= (f5 c_4 c_1) c13) (p9 c_4 c_1) (not (p8 c_4)) (not (p7 c_4 c_1)) )(or (p6 c_4 c_2) (= (f5 c_4 c_2) c13) (p9 c_4 c_2) (not (p8 c_4)) (not (p7 c_4 c_2)) )(or (p6 c_4 c_3) (= (f5 c_4 c_3) c13) (p9 c_4 c_3) (not (p8 c_4)) (not (p7 c_4 c_3)) )(or (p6 c_4 c_4) (= (f5 c_4 c_4) c13) (p9 c_4 c_4) (not (p8 c_4)) (not (p7 c_4 c_4)) )(or (p6 c_4 c_5) (= (f5 c_4 c_5) c13) (p9 c_4 c_5) (not (p8 c_4)) (not (p7 c_4 c_5)) )(or (p6 c_5 c_0) (= (f5 c_5 c_0) c13) (p9 c_5 c_0) (not (p8 c_5)) (not (p7 c_5 c_0)) )(or (p6 c_5 c_1) (= (f5 c_5 c_1) c13) (p9 c_5 c_1) (not (p8 c_5)) (not (p7 c_5 c_1)) )(or (p6 c_5 c_2) (= (f5 c_5 c_2) c13) (p9 c_5 c_2) (not (p8 c_5)) (not (p7 c_5 c_2)) )(or (p6 c_5 c_3) (= (f5 c_5 c_3) c13) (p9 c_5 c_3) (not (p8 c_5)) (not (p7 c_5 c_3)) )(or (p6 c_5 c_4) (= (f5 c_5 c_4) c13) (p9 c_5 c_4) (not (p8 c_5)) (not (p7 c_5 c_4)) )(or (p6 c_5 c_5) (= (f5 c_5 c_5) c13) (p9 c_5 c_5) (not (p8 c_5)) (not (p7 c_5 c_5)) )(or (= (f5 c_0 c_0) c14) (p7 c_0 c_0) (p6 c_0 c_0) (not (p8 c_0)) (p9 c_0 c_0) )(or (= (f5 c_0 c_1) c14) (p7 c_0 c_1) (p6 c_0 c_1) (not (p8 c_0)) (p9 c_0 c_1) )(or (= (f5 c_0 c_2) c14) (p7 c_0 c_2) (p6 c_0 c_2) (not (p8 c_0)) (p9 c_0 c_2) )(or (= (f5 c_0 c_3) c14) (p7 c_0 c_3) (p6 c_0 c_3) (not (p8 c_0)) (p9 c_0 c_3) )(or (= (f5 c_0 c_4) c14) (p7 c_0 c_4) (p6 c_0 c_4) (not (p8 c_0)) (p9 c_0 c_4) )(or (= (f5 c_0 c_5) c14) (p7 c_0 c_5) (p6 c_0 c_5) (not (p8 c_0)) (p9 c_0 c_5) )(or (= (f5 c_1 c_0) c14) (p7 c_1 c_0) (p6 c_1 c_0) (not (p8 c_1)) (p9 c_1 c_0) )(or (= (f5 c_1 c_1) c14) (p7 c_1 c_1) (p6 c_1 c_1) (not (p8 c_1)) (p9 c_1 c_1) )(or (= (f5 c_1 c_2) c14) (p7 c_1 c_2) (p6 c_1 c_2) (not (p8 c_1)) (p9 c_1 c_2) )(or (= (f5 c_1 c_3) c14) (p7 c_1 c_3) (p6 c_1 c_3) (not (p8 c_1)) (p9 c_1 c_3) )(or (= (f5 c_1 c_4) c14) (p7 c_1 c_4) (p6 c_1 c_4) (not (p8 c_1)) (p9 c_1 c_4) )(or (= (f5 c_1 c_5) c14) (p7 c_1 c_5) (p6 c_1 c_5) (not (p8 c_1)) (p9 c_1 c_5) )(or (= (f5 c_2 c_0) c14) (p7 c_2 c_0) (p6 c_2 c_0) (not (p8 c_2)) (p9 c_2 c_0) )(or (= (f5 c_2 c_1) c14) (p7 c_2 c_1) (p6 c_2 c_1) (not (p8 c_2)) (p9 c_2 c_1) )(or (= (f5 c_2 c_2) c14) (p7 c_2 c_2) (p6 c_2 c_2) (not (p8 c_2)) (p9 c_2 c_2) )(or (= (f5 c_2 c_3) c14) (p7 c_2 c_3) (p6 c_2 c_3) (not (p8 c_2)) (p9 c_2 c_3) )(or (= (f5 c_2 c_4) c14) (p7 c_2 c_4) (p6 c_2 c_4) (not (p8 c_2)) (p9 c_2 c_4) )(or (= (f5 c_2 c_5) c14) (p7 c_2 c_5) (p6 c_2 c_5) (not (p8 c_2)) (p9 c_2 c_5) )(or (= (f5 c_3 c_0) c14) (p7 c_3 c_0) (p6 c_3 c_0) (not (p8 c_3)) (p9 c_3 c_0) )(or (= (f5 c_3 c_1) c14) (p7 c_3 c_1) (p6 c_3 c_1) (not (p8 c_3)) (p9 c_3 c_1) )(or (= (f5 c_3 c_2) c14) (p7 c_3 c_2) (p6 c_3 c_2) (not (p8 c_3)) (p9 c_3 c_2) )(or (= (f5 c_3 c_3) c14) (p7 c_3 c_3) (p6 c_3 c_3) (not (p8 c_3)) (p9 c_3 c_3) )(or (= (f5 c_3 c_4) c14) (p7 c_3 c_4) (p6 c_3 c_4) (not (p8 c_3)) (p9 c_3 c_4) )(or (= (f5 c_3 c_5) c14) (p7 c_3 c_5) (p6 c_3 c_5) (not (p8 c_3)) (p9 c_3 c_5) )(or (= (f5 c_4 c_0) c14) (p7 c_4 c_0) (p6 c_4 c_0) (not (p8 c_4)) (p9 c_4 c_0) )(or (= (f5 c_4 c_1) c14) (p7 c_4 c_1) (p6 c_4 c_1) (not (p8 c_4)) (p9 c_4 c_1) )(or (= (f5 c_4 c_2) c14) (p7 c_4 c_2) (p6 c_4 c_2) (not (p8 c_4)) (p9 c_4 c_2) )(or (= (f5 c_4 c_3) c14) (p7 c_4 c_3) (p6 c_4 c_3) (not (p8 c_4)) (p9 c_4 c_3) )(or (= (f5 c_4 c_4) c14) (p7 c_4 c_4) (p6 c_4 c_4) (not (p8 c_4)) (p9 c_4 c_4) )(or (= (f5 c_4 c_5) c14) (p7 c_4 c_5) (p6 c_4 c_5) (not (p8 c_4)) (p9 c_4 c_5) )(or (= (f5 c_5 c_0) c14) (p7 c_5 c_0) (p6 c_5 c_0) (not (p8 c_5)) (p9 c_5 c_0) )(or (= (f5 c_5 c_1) c14) (p7 c_5 c_1) (p6 c_5 c_1) (not (p8 c_5)) (p9 c_5 c_1) )(or (= (f5 c_5 c_2) c14) (p7 c_5 c_2) (p6 c_5 c_2) (not (p8 c_5)) (p9 c_5 c_2) )(or (= (f5 c_5 c_3) c14) (p7 c_5 c_3) (p6 c_5 c_3) (not (p8 c_5)) (p9 c_5 c_3) )(or (= (f5 c_5 c_4) c14) (p7 c_5 c_4) (p6 c_5 c_4) (not (p8 c_5)) (p9 c_5 c_4) )(or (= (f5 c_5 c_5) c14) (p7 c_5 c_5) (p6 c_5 c_5) (not (p8 c_5)) (p9 c_5 c_5) )(or (p6 c_0 c_0) (not (p9 c_0 c_0)) (p7 c_0 c_0) (= (f5 c_0 c_0) c12) (not (p8 c_0)) )(or (p6 c_0 c_1) (not (p9 c_0 c_1)) (p7 c_0 c_1) (= (f5 c_0 c_1) c12) (not (p8 c_0)) )(or (p6 c_0 c_2) (not (p9 c_0 c_2)) (p7 c_0 c_2) (= (f5 c_0 c_2) c12) (not (p8 c_0)) )(or (p6 c_0 c_3) (not (p9 c_0 c_3)) (p7 c_0 c_3) (= (f5 c_0 c_3) c12) (not (p8 c_0)) )(or (p6 c_0 c_4) (not (p9 c_0 c_4)) (p7 c_0 c_4) (= (f5 c_0 c_4) c12) (not (p8 c_0)) )(or (p6 c_0 c_5) (not (p9 c_0 c_5)) (p7 c_0 c_5) (= (f5 c_0 c_5) c12) (not (p8 c_0)) )(or (p6 c_1 c_0) (not (p9 c_1 c_0)) (p7 c_1 c_0) (= (f5 c_1 c_0) c12) (not (p8 c_1)) )(or (p6 c_1 c_1) (not (p9 c_1 c_1)) (p7 c_1 c_1) (= (f5 c_1 c_1) c12) (not (p8 c_1)) )(or (p6 c_1 c_2) (not (p9 c_1 c_2)) (p7 c_1 c_2) (= (f5 c_1 c_2) c12) (not (p8 c_1)) )(or (p6 c_1 c_3) (not (p9 c_1 c_3)) (p7 c_1 c_3) (= (f5 c_1 c_3) c12) (not (p8 c_1)) )(or (p6 c_1 c_4) (not (p9 c_1 c_4)) (p7 c_1 c_4) (= (f5 c_1 c_4) c12) (not (p8 c_1)) )(or (p6 c_1 c_5) (not (p9 c_1 c_5)) (p7 c_1 c_5) (= (f5 c_1 c_5) c12) (not (p8 c_1)) )(or (p6 c_2 c_0) (not (p9 c_2 c_0)) (p7 c_2 c_0) (= (f5 c_2 c_0) c12) (not (p8 c_2)) )(or (p6 c_2 c_1) (not (p9 c_2 c_1)) (p7 c_2 c_1) (= (f5 c_2 c_1) c12) (not (p8 c_2)) )(or (p6 c_2 c_2) (not (p9 c_2 c_2)) (p7 c_2 c_2) (= (f5 c_2 c_2) c12) (not (p8 c_2)) )(or (p6 c_2 c_3) (not (p9 c_2 c_3)) (p7 c_2 c_3) (= (f5 c_2 c_3) c12) (not (p8 c_2)) )(or (p6 c_2 c_4) (not (p9 c_2 c_4)) (p7 c_2 c_4) (= (f5 c_2 c_4) c12) (not (p8 c_2)) )(or (p6 c_2 c_5) (not (p9 c_2 c_5)) (p7 c_2 c_5) (= (f5 c_2 c_5) c12) (not (p8 c_2)) )(or (p6 c_3 c_0) (not (p9 c_3 c_0)) (p7 c_3 c_0) (= (f5 c_3 c_0) c12) (not (p8 c_3)) )(or (p6 c_3 c_1) (not (p9 c_3 c_1)) (p7 c_3 c_1) (= (f5 c_3 c_1) c12) (not (p8 c_3)) )(or (p6 c_3 c_2) (not (p9 c_3 c_2)) (p7 c_3 c_2) (= (f5 c_3 c_2) c12) (not (p8 c_3)) )(or (p6 c_3 c_3) (not (p9 c_3 c_3)) (p7 c_3 c_3) (= (f5 c_3 c_3) c12) (not (p8 c_3)) )(or (p6 c_3 c_4) (not (p9 c_3 c_4)) (p7 c_3 c_4) (= (f5 c_3 c_4) c12) (not (p8 c_3)) )(or (p6 c_3 c_5) (not (p9 c_3 c_5)) (p7 c_3 c_5) (= (f5 c_3 c_5) c12) (not (p8 c_3)) )(or (p6 c_4 c_0) (not (p9 c_4 c_0)) (p7 c_4 c_0) (= (f5 c_4 c_0) c12) (not (p8 c_4)) )(or (p6 c_4 c_1) (not (p9 c_4 c_1)) (p7 c_4 c_1) (= (f5 c_4 c_1) c12) (not (p8 c_4)) )(or (p6 c_4 c_2) (not (p9 c_4 c_2)) (p7 c_4 c_2) (= (f5 c_4 c_2) c12) (not (p8 c_4)) )(or (p6 c_4 c_3) (not (p9 c_4 c_3)) (p7 c_4 c_3) (= (f5 c_4 c_3) c12) (not (p8 c_4)) )(or (p6 c_4 c_4) (not (p9 c_4 c_4)) (p7 c_4 c_4) (= (f5 c_4 c_4) c12) (not (p8 c_4)) )(or (p6 c_4 c_5) (not (p9 c_4 c_5)) (p7 c_4 c_5) (= (f5 c_4 c_5) c12) (not (p8 c_4)) )(or (p6 c_5 c_0) (not (p9 c_5 c_0)) (p7 c_5 c_0) (= (f5 c_5 c_0) c12) (not (p8 c_5)) )(or (p6 c_5 c_1) (not (p9 c_5 c_1)) (p7 c_5 c_1) (= (f5 c_5 c_1) c12) (not (p8 c_5)) )(or (p6 c_5 c_2) (not (p9 c_5 c_2)) (p7 c_5 c_2) (= (f5 c_5 c_2) c12) (not (p8 c_5)) )(or (p6 c_5 c_3) (not (p9 c_5 c_3)) (p7 c_5 c_3) (= (f5 c_5 c_3) c12) (not (p8 c_5)) )(or (p6 c_5 c_4) (not (p9 c_5 c_4)) (p7 c_5 c_4) (= (f5 c_5 c_4) c12) (not (p8 c_5)) )(or (p6 c_5 c_5) (not (p9 c_5 c_5)) (p7 c_5 c_5) (= (f5 c_5 c_5) c12) (not (p8 c_5)) )(or (= (f5 c_0 c_0) c_0)(= (f5 c_0 c_0) c_1)(= (f5 c_0 c_0) c_2)(= (f5 c_0 c_0) c_3)(= (f5 c_0 c_0) c_4)(= (f5 c_0 c_0) c_5))(or (= (f5 c_0 c_1) c_0)(= (f5 c_0 c_1) c_1)(= (f5 c_0 c_1) c_2)(= (f5 c_0 c_1) c_3)(= (f5 c_0 c_1) c_4)(= (f5 c_0 c_1) c_5))(or (= (f5 c_0 c_2) c_0)(= (f5 c_0 c_2) c_1)(= (f5 c_0 c_2) c_2)(= (f5 c_0 c_2) c_3)(= (f5 c_0 c_2) c_4)(= (f5 c_0 c_2) c_5))(or (= (f5 c_0 c_3) c_0)(= (f5 c_0 c_3) c_1)(= (f5 c_0 c_3) c_2)(= (f5 c_0 c_3) c_3)(= (f5 c_0 c_3) c_4)(= (f5 c_0 c_3) c_5))(or (= (f5 c_0 c_4) c_0)(= (f5 c_0 c_4) c_1)(= (f5 c_0 c_4) c_2)(= (f5 c_0 c_4) c_3)(= (f5 c_0 c_4) c_4)(= (f5 c_0 c_4) c_5))(or (= (f5 c_0 c_5) c_0)(= (f5 c_0 c_5) c_1)(= (f5 c_0 c_5) c_2)(= (f5 c_0 c_5) c_3)(= (f5 c_0 c_5) c_4)(= (f5 c_0 c_5) c_5))(or (= (f5 c_1 c_0) c_0)(= (f5 c_1 c_0) c_1)(= (f5 c_1 c_0) c_2)(= (f5 c_1 c_0) c_3)(= (f5 c_1 c_0) c_4)(= (f5 c_1 c_0) c_5))(or (= (f5 c_1 c_1) c_0)(= (f5 c_1 c_1) c_1)(= (f5 c_1 c_1) c_2)(= (f5 c_1 c_1) c_3)(= (f5 c_1 c_1) c_4)(= (f5 c_1 c_1) c_5))(or (= (f5 c_1 c_2) c_0)(= (f5 c_1 c_2) c_1)(= (f5 c_1 c_2) c_2)(= (f5 c_1 c_2) c_3)(= (f5 c_1 c_2) c_4)(= (f5 c_1 c_2) c_5))(or (= (f5 c_1 c_3) c_0)(= (f5 c_1 c_3) c_1)(= (f5 c_1 c_3) c_2)(= (f5 c_1 c_3) c_3)(= (f5 c_1 c_3) c_4)(= (f5 c_1 c_3) c_5))(or (= (f5 c_1 c_4) c_0)(= (f5 c_1 c_4) c_1)(= (f5 c_1 c_4) c_2)(= (f5 c_1 c_4) c_3)(= (f5 c_1 c_4) c_4)(= (f5 c_1 c_4) c_5))(or (= (f5 c_1 c_5) c_0)(= (f5 c_1 c_5) c_1)(= (f5 c_1 c_5) c_2)(= (f5 c_1 c_5) c_3)(= (f5 c_1 c_5) c_4)(= (f5 c_1 c_5) c_5))(or (= (f5 c_2 c_0) c_0)(= (f5 c_2 c_0) c_1)(= (f5 c_2 c_0) c_2)(= (f5 c_2 c_0) c_3)(= (f5 c_2 c_0) c_4)(= (f5 c_2 c_0) c_5))(or (= (f5 c_2 c_1) c_0)(= (f5 c_2 c_1) c_1)(= (f5 c_2 c_1) c_2)(= (f5 c_2 c_1) c_3)(= (f5 c_2 c_1) c_4)(= (f5 c_2 c_1) c_5))(or (= (f5 c_2 c_2) c_0)(= (f5 c_2 c_2) c_1)(= (f5 c_2 c_2) c_2)(= (f5 c_2 c_2) c_3)(= (f5 c_2 c_2) c_4)(= (f5 c_2 c_2) c_5))(or (= (f5 c_2 c_3) c_0)(= (f5 c_2 c_3) c_1)(= (f5 c_2 c_3) c_2)(= (f5 c_2 c_3) c_3)(= (f5 c_2 c_3) c_4)(= (f5 c_2 c_3) c_5))(or (= (f5 c_2 c_4) c_0)(= (f5 c_2 c_4) c_1)(= (f5 c_2 c_4) c_2)(= (f5 c_2 c_4) c_3)(= (f5 c_2 c_4) c_4)(= (f5 c_2 c_4) c_5))(or (= (f5 c_2 c_5) c_0)(= (f5 c_2 c_5) c_1)(= (f5 c_2 c_5) c_2)(= (f5 c_2 c_5) c_3)(= (f5 c_2 c_5) c_4)(= (f5 c_2 c_5) c_5))(or (= (f5 c_3 c_0) c_0)(= (f5 c_3 c_0) c_1)(= (f5 c_3 c_0) c_2)(= (f5 c_3 c_0) c_3)(= (f5 c_3 c_0) c_4)(= (f5 c_3 c_0) c_5))(or (= (f5 c_3 c_1) c_0)(= (f5 c_3 c_1) c_1)(= (f5 c_3 c_1) c_2)(= (f5 c_3 c_1) c_3)(= (f5 c_3 c_1) c_4)(= (f5 c_3 c_1) c_5))(or (= (f5 c_3 c_2) c_0)(= (f5 c_3 c_2) c_1)(= (f5 c_3 c_2) c_2)(= (f5 c_3 c_2) c_3)(= (f5 c_3 c_2) c_4)(= (f5 c_3 c_2) c_5))(or (= (f5 c_3 c_3) c_0)(= (f5 c_3 c_3) c_1)(= (f5 c_3 c_3) c_2)(= (f5 c_3 c_3) c_3)(= (f5 c_3 c_3) c_4)(= (f5 c_3 c_3) c_5))(or (= (f5 c_3 c_4) c_0)(= (f5 c_3 c_4) c_1)(= (f5 c_3 c_4) c_2)(= (f5 c_3 c_4) c_3)(= (f5 c_3 c_4) c_4)(= (f5 c_3 c_4) c_5))(or (= (f5 c_3 c_5) c_0)(= (f5 c_3 c_5) c_1)(= (f5 c_3 c_5) c_2)(= (f5 c_3 c_5) c_3)(= (f5 c_3 c_5) c_4)(= (f5 c_3 c_5) c_5))(or (= (f5 c_4 c_0) c_0)(= (f5 c_4 c_0) c_1)(= (f5 c_4 c_0) c_2)(= (f5 c_4 c_0) c_3)(= (f5 c_4 c_0) c_4)(= (f5 c_4 c_0) c_5))(or (= (f5 c_4 c_1) c_0)(= (f5 c_4 c_1) c_1)(= (f5 c_4 c_1) c_2)(= (f5 c_4 c_1) c_3)(= (f5 c_4 c_1) c_4)(= (f5 c_4 c_1) c_5))(or (= (f5 c_4 c_2) c_0)(= (f5 c_4 c_2) c_1)(= (f5 c_4 c_2) c_2)(= (f5 c_4 c_2) c_3)(= (f5 c_4 c_2) c_4)(= (f5 c_4 c_2) c_5))(or (= (f5 c_4 c_3) c_0)(= (f5 c_4 c_3) c_1)(= (f5 c_4 c_3) c_2)(= (f5 c_4 c_3) c_3)(= (f5 c_4 c_3) c_4)(= (f5 c_4 c_3) c_5))(or (= (f5 c_4 c_4) c_0)(= (f5 c_4 c_4) c_1)(= (f5 c_4 c_4) c_2)(= (f5 c_4 c_4) c_3)(= (f5 c_4 c_4) c_4)(= (f5 c_4 c_4) c_5))(or (= (f5 c_4 c_5) c_0)(= (f5 c_4 c_5) c_1)(= (f5 c_4 c_5) c_2)(= (f5 c_4 c_5) c_3)(= (f5 c_4 c_5) c_4)(= (f5 c_4 c_5) c_5))(or (= (f5 c_5 c_0) c_0)(= (f5 c_5 c_0) c_1)(= (f5 c_5 c_0) c_2)(= (f5 c_5 c_0) c_3)(= (f5 c_5 c_0) c_4)(= (f5 c_5 c_0) c_5))(or (= (f5 c_5 c_1) c_0)(= (f5 c_5 c_1) c_1)(= (f5 c_5 c_1) c_2)(= (f5 c_5 c_1) c_3)(= (f5 c_5 c_1) c_4)(= (f5 c_5 c_1) c_5))(or (= (f5 c_5 c_2) c_0)(= (f5 c_5 c_2) c_1)(= (f5 c_5 c_2) c_2)(= (f5 c_5 c_2) c_3)(= (f5 c_5 c_2) c_4)(= (f5 c_5 c_2) c_5))(or (= (f5 c_5 c_3) c_0)(= (f5 c_5 c_3) c_1)(= (f5 c_5 c_3) c_2)(= (f5 c_5 c_3) c_3)(= (f5 c_5 c_3) c_4)(= (f5 c_5 c_3) c_5))(or (= (f5 c_5 c_4) c_0)(= (f5 c_5 c_4) c_1)(= (f5 c_5 c_4) c_2)(= (f5 c_5 c_4) c_3)(= (f5 c_5 c_4) c_4)(= (f5 c_5 c_4) c_5))(or (= (f5 c_5 c_5) c_0)(= (f5 c_5 c_5) c_1)(= (f5 c_5 c_5) c_2)(= (f5 c_5 c_5) c_3)(= (f5 c_5 c_5) c_4)(= (f5 c_5 c_5) c_5))(or (= c14 c_0)(= c14 c_1)(= c14 c_2)(= c14 c_3)(= c14 c_4)(= c14 c_5))(or (= c12 c_0)(= c12 c_1)(= c12 c_2)(= c12 c_3)(= c12 c_4)(= c12 c_5))(or (= c13 c_0)(= c13 c_1)(= c13 c_2)(= c13 c_3)(= c13 c_4)(= c13 c_5))(or (= c15 c_0)(= c15 c_1)(= c15 c_2)(= c15 c_3)(= c15 c_4)(= c15 c_5))(or (= c17 c_0)(= c17 c_1)(= c17 c_2)(= c17 c_3)(= c17 c_4)(= c17 c_5))(or (= c11 c_0)(= c11 c_1)(= c11 c_2)(= c11 c_3)(= c11 c_4)(= c11 c_5))(or (= c10 c_0)(= c10 c_1)(= c10 c_2)(= c10 c_3)(= c10 c_4)(= c10 c_5))(or (= c16 c_0)(= c16 c_1)(= c16 c_2)(= c16 c_3)(= c16 c_4)(= c16 c_5))))