(benchmark SEQ011_size2.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 unsat
:logic QF_UF
:extrapreds ((p10 U U))
:extrapreds ((p9 U))
:extrafuns ((f16 U U U U))
:extrapreds ((p3 U))
:extrafuns ((f2 U U U))
:extrapreds ((p4 U))
:extrafuns ((f7 U U))
:extrapreds ((p1 U U))
:extrafuns ((f12 U U))
:extrafuns ((c18 U))
:extrapreds ((p14 U U U))
:extrafuns ((f17 U U U U))
:extrafuns ((f13 U U U U))
:extrafuns ((f6 U U))
:extrafuns ((f5 U U))
:extrafuns ((f11 U U))
:extrapreds ((p15 U U))
:extrafuns ((c8 U))
:extrafuns ((c_0 U))
:extrafuns ((c_1 U))
:formula 
( and 
( distinct c_0 c_1 )(or (not (p10 c_0 c_0)) (not (p9 c_0)) (not (= c_0 (f16 c_0 c_0 c_0))) (= c_0 c_0) (not (p3 c_0)) (not (p10 c_0 c_0)) (not (p9 c_0)) )(or (not (p10 c_0 c_0)) (not (p9 c_0)) (not (= c_0 (f16 c_1 c_0 c_0))) (= c_1 c_0) (not (p3 c_0)) (not (p10 c_0 c_1)) (not (p9 c_1)) )(or (not (p10 c_0 c_1)) (not (p9 c_1)) (not (= c_0 (f16 c_0 c_1 c_0))) (= c_0 c_1) (not (p3 c_0)) (not (p10 c_0 c_0)) (not (p9 c_0)) )(or (not (p10 c_0 c_1)) (not (p9 c_1)) (not (= c_0 (f16 c_1 c_1 c_0))) (= c_1 c_1) (not (p3 c_0)) (not (p10 c_0 c_1)) (not (p9 c_1)) )(or (not (p10 c_1 c_0)) (not (p9 c_0)) (not (= c_1 (f16 c_0 c_0 c_1))) (= c_0 c_0) (not (p3 c_1)) (not (p10 c_1 c_0)) (not (p9 c_0)) )(or (not (p10 c_1 c_0)) (not (p9 c_0)) (not (= c_1 (f16 c_1 c_0 c_1))) (= c_1 c_0) (not (p3 c_1)) (not (p10 c_1 c_1)) (not (p9 c_1)) )(or (not (p10 c_1 c_1)) (not (p9 c_1)) (not (= c_1 (f16 c_0 c_1 c_1))) (= c_0 c_1) (not (p3 c_1)) (not (p10 c_1 c_0)) (not (p9 c_0)) )(or (not (p10 c_1 c_1)) (not (p9 c_1)) (not (= c_1 (f16 c_1 c_1 c_1))) (= c_1 c_1) (not (p3 c_1)) (not (p10 c_1 c_1)) (not (p9 c_1)) )(or (not (p3 c_0)) (not (p3 c_0)) (p4 (f2 c_0 c_0)) (= c_0 c_0) )(or (not (p3 c_0)) (not (p3 c_1)) (p4 (f2 c_1 c_0)) (= c_1 c_0) )(or (not (p3 c_1)) (not (p3 c_0)) (p4 (f2 c_0 c_1)) (= c_0 c_1) )(or (not (p3 c_1)) (not (p3 c_1)) (p4 (f2 c_1 c_1)) (= c_1 c_1) )(or (p3 (f7 c_0)) (not (p4 c_0)) )(or (p3 (f7 c_1)) (not (p4 c_1)) )(or (not (p3 c_0)) (= c_0 c_0) (not (p3 c_0)) (p1 c_0 (f2 c_0 c_0)) )(or (not (p3 c_0)) (= c_0 c_1) (not (p3 c_1)) (p1 c_0 (f2 c_0 c_1)) )(or (not (p3 c_1)) (= c_1 c_0) (not (p3 c_0)) (p1 c_1 (f2 c_1 c_0)) )(or (not (p3 c_1)) (= c_1 c_1) (not (p3 c_1)) (p1 c_1 (f2 c_1 c_1)) )(or (p3 (f12 c_0)) (not (p9 c_0)) )(or (p3 (f12 c_1)) (not (p9 c_1)) )(or (not (p1 (f7 c_0) c_0)) (not (p4 c_0)) )(or (not (p1 (f7 c_1) c_1)) (not (p4 c_1)) )(or (p10 (f16 c_0 c_0 c_0) c_0) (= c_0 c_0) (not (p9 c_0)) (not (p9 c_0)) (not (p10 c_0 c_0)) (not (p10 c_0 c_0)) (not (p3 c_0)) )(or (p10 (f16 c_0 c_0 c_1) c_0) (= c_0 c_0) (not (p9 c_0)) (not (p9 c_0)) (not (p10 c_1 c_0)) (not (p10 c_1 c_0)) (not (p3 c_1)) )(or (p10 (f16 c_0 c_1 c_0) c_0) (= c_0 c_1) (not (p9 c_0)) (not (p9 c_1)) (not (p10 c_0 c_1)) (not (p10 c_0 c_0)) (not (p3 c_0)) )(or (p10 (f16 c_0 c_1 c_1) c_0) (= c_0 c_1) (not (p9 c_0)) (not (p9 c_1)) (not (p10 c_1 c_1)) (not (p10 c_1 c_0)) (not (p3 c_1)) )(or (p10 (f16 c_1 c_0 c_0) c_1) (= c_1 c_0) (not (p9 c_1)) (not (p9 c_0)) (not (p10 c_0 c_0)) (not (p10 c_0 c_1)) (not (p3 c_0)) )(or (p10 (f16 c_1 c_0 c_1) c_1) (= c_1 c_0) (not (p9 c_1)) (not (p9 c_0)) (not (p10 c_1 c_0)) (not (p10 c_1 c_1)) (not (p3 c_1)) )(or (p10 (f16 c_1 c_1 c_0) c_1) (= c_1 c_1) (not (p9 c_1)) (not (p9 c_1)) (not (p10 c_0 c_1)) (not (p10 c_0 c_1)) (not (p3 c_0)) )(or (p10 (f16 c_1 c_1 c_1) c_1) (= c_1 c_1) (not (p9 c_1)) (not (p9 c_1)) (not (p10 c_1 c_1)) (not (p10 c_1 c_1)) (not (p3 c_1)) )(p9 c18) (or (not (p10 (f12 c_0) c_0)) (not (p9 c_0)) )(or (not (p10 (f12 c_1) c_1)) (not (p9 c_1)) )(or (not (p10 c_0 c_0)) (not (p9 c_0)) (not (p10 c_0 c_0)) (= c_0 c_0) (not (p9 c_0)) (not (p3 c_0)) (p3 (f16 c_0 c_0 c_0)) )(or (not (p10 c_0 c_0)) (not (p9 c_1)) (not (p10 c_0 c_1)) (= c_0 c_1) (not (p9 c_0)) (not (p3 c_0)) (p3 (f16 c_0 c_1 c_0)) )(or (not (p10 c_0 c_1)) (not (p9 c_0)) (not (p10 c_0 c_0)) (= c_1 c_0) (not (p9 c_1)) (not (p3 c_0)) (p3 (f16 c_1 c_0 c_0)) )(or (not (p10 c_0 c_1)) (not (p9 c_1)) (not (p10 c_0 c_1)) (= c_1 c_1) (not (p9 c_1)) (not (p3 c_0)) (p3 (f16 c_1 c_1 c_0)) )(or (not (p10 c_1 c_0)) (not (p9 c_0)) (not (p10 c_1 c_0)) (= c_0 c_0) (not (p9 c_0)) (not (p3 c_1)) (p3 (f16 c_0 c_0 c_1)) )(or (not (p10 c_1 c_0)) (not (p9 c_1)) (not (p10 c_1 c_1)) (= c_0 c_1) (not (p9 c_0)) (not (p3 c_1)) (p3 (f16 c_0 c_1 c_1)) )(or (not (p10 c_1 c_1)) (not (p9 c_0)) (not (p10 c_1 c_0)) (= c_1 c_0) (not (p9 c_1)) (not (p3 c_1)) (p3 (f16 c_1 c_0 c_1)) )(or (not (p10 c_1 c_1)) (not (p9 c_1)) (not (p10 c_1 c_1)) (= c_1 c_1) (not (p9 c_1)) (not (p3 c_1)) (p3 (f16 c_1 c_1 c_1)) )(or (= c_0 c_0) (not (p14 c_0 c_0 c_0)) (= c_0 c_0) (not (p3 c_0)) (= c_0 c_0) (not (p3 c_0)) (p4 (f17 c_0 c_0 c_0)) (not (p3 c_0)) )(or (= c_0 c_0) (not (p14 c_0 c_0 c_1)) (= c_0 c_1) (not (p3 c_0)) (= c_0 c_1) (not (p3 c_1)) (p4 (f17 c_0 c_0 c_1)) (not (p3 c_0)) )(or (= c_0 c_1) (not (p14 c_0 c_1 c_0)) (= c_0 c_0) (not (p3 c_1)) (= c_1 c_0) (not (p3 c_0)) (p4 (f17 c_0 c_1 c_0)) (not (p3 c_0)) )(or (= c_0 c_1) (not (p14 c_0 c_1 c_1)) (= c_0 c_1) (not (p3 c_1)) (= c_1 c_1) (not (p3 c_1)) (p4 (f17 c_0 c_1 c_1)) (not (p3 c_0)) )(or (= c_1 c_0) (not (p14 c_1 c_0 c_0)) (= c_1 c_0) (not (p3 c_0)) (= c_0 c_0) (not (p3 c_0)) (p4 (f17 c_1 c_0 c_0)) (not (p3 c_1)) )(or (= c_1 c_0) (not (p14 c_1 c_0 c_1)) (= c_1 c_1) (not (p3 c_0)) (= c_0 c_1) (not (p3 c_1)) (p4 (f17 c_1 c_0 c_1)) (not (p3 c_1)) )(or (= c_1 c_1) (not (p14 c_1 c_1 c_0)) (= c_1 c_0) (not (p3 c_1)) (= c_1 c_0) (not (p3 c_0)) (p4 (f17 c_1 c_1 c_0)) (not (p3 c_1)) )(or (= c_1 c_1) (not (p14 c_1 c_1 c_1)) (= c_1 c_1) (not (p3 c_1)) (= c_1 c_1) (not (p3 c_1)) (p4 (f17 c_1 c_1 c_1)) (not (p3 c_1)) )(or (= 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)) (not (p3 c_0)) (= c_0 c_0) )(or (= c_0 c_0) (p10 c_0 (f13 c_0 c_0 c_1)) (not (p3 c_0)) (p14 c_0 c_0 c_1) (= c_0 c_1) (not (p3 c_0)) (not (p3 c_1)) (= c_0 c_1) )(or (= c_0 c_1) (p10 c_1 (f13 c_0 c_1 c_0)) (not (p3 c_1)) (p14 c_0 c_1 c_0) (= c_1 c_0) (not (p3 c_0)) (not (p3 c_0)) (= c_0 c_0) )(or (= c_0 c_1) (p10 c_1 (f13 c_0 c_1 c_1)) (not (p3 c_1)) (p14 c_0 c_1 c_1) (= c_1 c_1) (not (p3 c_0)) (not (p3 c_1)) (= c_0 c_1) )(or (= c_1 c_0) (p10 c_0 (f13 c_1 c_0 c_0)) (not (p3 c_0)) (p14 c_1 c_0 c_0) (= c_0 c_0) (not (p3 c_1)) (not (p3 c_0)) (= c_1 c_0) )(or (= c_1 c_0) (p10 c_0 (f13 c_1 c_0 c_1)) (not (p3 c_0)) (p14 c_1 c_0 c_1) (= c_0 c_1) (not (p3 c_1)) (not (p3 c_1)) (= c_1 c_1) )(or (= c_1 c_1) (p10 c_1 (f13 c_1 c_1 c_0)) (not (p3 c_1)) (p14 c_1 c_1 c_0) (= c_1 c_0) (not (p3 c_1)) (not (p3 c_0)) (= c_1 c_0) )(or (= 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)) (not (p3 c_1)) (= c_1 c_1) )(or (not (p4 c_0)) (p1 (f6 c_0) c_0) )(or (not (p4 c_1)) (p1 (f6 c_1) c_1) )(or (p1 (f5 c_0) c_0) (not (p4 c_0)) )(or (p1 (f5 c_1) c_1) (not (p4 c_1)) )(or (p3 (f6 c_0)) (not (p4 c_0)) )(or (p3 (f6 c_1)) (not (p4 c_1)) )(or (p3 (f5 c_0)) (not (p4 c_0)) )(or (p3 (f5 c_1)) (not (p4 c_1)) )(or (not (p3 c_0)) (p1 c_0 (f17 c_0 c_0 c_0)) (not (p3 c_0)) (= c_0 c_0) (= c_0 c_0) (= c_0 c_0) (not (p14 c_0 c_0 c_0)) (not (p3 c_0)) )(or (not (p3 c_0)) (p1 c_0 (f17 c_0 c_0 c_1)) (not (p3 c_0)) (= c_0 c_0) (= c_0 c_1) (= c_0 c_1) (not (p14 c_0 c_0 c_1)) (not (p3 c_1)) )(or (not (p3 c_0)) (p1 c_0 (f17 c_1 c_0 c_0)) (not (p3 c_1)) (= c_1 c_0) (= c_0 c_0) (= c_1 c_0) (not (p14 c_1 c_0 c_0)) (not (p3 c_0)) )(or (not (p3 c_0)) (p1 c_0 (f17 c_1 c_0 c_1)) (not (p3 c_1)) (= c_1 c_0) (= c_0 c_1) (= c_1 c_1) (not (p14 c_1 c_0 c_1)) (not (p3 c_1)) )(or (not (p3 c_1)) (p1 c_1 (f17 c_0 c_1 c_0)) (not (p3 c_0)) (= c_0 c_1) (= c_1 c_0) (= c_0 c_0) (not (p14 c_0 c_1 c_0)) (not (p3 c_0)) )(or (not (p3 c_1)) (p1 c_1 (f17 c_0 c_1 c_1)) (not (p3 c_0)) (= c_0 c_1) (= c_1 c_1) (= c_0 c_1) (not (p14 c_0 c_1 c_1)) (not (p3 c_1)) )(or (not (p3 c_1)) (p1 c_1 (f17 c_1 c_1 c_0)) (not (p3 c_1)) (= c_1 c_1) (= c_1 c_0) (= c_1 c_0) (not (p14 c_1 c_1 c_0)) (not (p3 c_0)) )(or (not (p3 c_1)) (p1 c_1 (f17 c_1 c_1 c_1)) (not (p3 c_1)) (= c_1 c_1) (= c_1 c_1) (= c_1 c_1) (not (p14 c_1 c_1 c_1)) (not (p3 c_1)) )(or (p3 (f11 c_0)) (not (p9 c_0)) )(or (p3 (f11 c_1)) (not (p9 c_1)) )(or (not (p9 c_0)) (p10 (f11 c_0) c_0) )(or (not (p9 c_1)) (p10 (f11 c_1) c_1) )(or (p15 c_0 c_0) (not (p3 c_0)) (not (p10 c_0 c_0)) (not (p1 c_0 c_0)) (not (p1 c_0 c_0)) (not (p9 c_0)) (= c_0 c_0) (not (p3 c_0)) (not (p10 c_0 c_0)) (not (p4 c_0)) )(or (p15 c_0 c_0) (not (p3 c_0)) (not (p10 c_0 c_0)) (not (p1 c_0 c_0)) (not (p1 c_1 c_0)) (not (p9 c_0)) (= c_0 c_1) (not (p3 c_1)) (not (p10 c_1 c_0)) (not (p4 c_0)) )(or (p15 c_0 c_0) (not (p3 c_1)) (not (p10 c_1 c_0)) (not (p1 c_1 c_0)) (not (p1 c_0 c_0)) (not (p9 c_0)) (= c_1 c_0) (not (p3 c_0)) (not (p10 c_0 c_0)) (not (p4 c_0)) )(or (p15 c_0 c_0) (not (p3 c_1)) (not (p10 c_1 c_0)) (not (p1 c_1 c_0)) (not (p1 c_1 c_0)) (not (p9 c_0)) (= c_1 c_1) (not (p3 c_1)) (not (p10 c_1 c_0)) (not (p4 c_0)) )(or (p15 c_0 c_1) (not (p3 c_0)) (not (p10 c_0 c_1)) (not (p1 c_0 c_0)) (not (p1 c_0 c_0)) (not (p9 c_1)) (= c_0 c_0) (not (p3 c_0)) (not (p10 c_0 c_1)) (not (p4 c_0)) )(or (p15 c_0 c_1) (not (p3 c_0)) (not (p10 c_0 c_1)) (not (p1 c_0 c_0)) (not (p1 c_1 c_0)) (not (p9 c_1)) (= c_0 c_1) (not (p3 c_1)) (not (p10 c_1 c_1)) (not (p4 c_0)) )(or (p15 c_0 c_1) (not (p3 c_1)) (not (p10 c_1 c_1)) (not (p1 c_1 c_0)) (not (p1 c_0 c_0)) (not (p9 c_1)) (= c_1 c_0) (not (p3 c_0)) (not (p10 c_0 c_1)) (not (p4 c_0)) )(or (p15 c_0 c_1) (not (p3 c_1)) (not (p10 c_1 c_1)) (not (p1 c_1 c_0)) (not (p1 c_1 c_0)) (not (p9 c_1)) (= c_1 c_1) (not (p3 c_1)) (not (p10 c_1 c_1)) (not (p4 c_0)) )(or (p15 c_1 c_0) (not (p3 c_0)) (not (p10 c_0 c_0)) (not (p1 c_0 c_1)) (not (p1 c_0 c_1)) (not (p9 c_0)) (= c_0 c_0) (not (p3 c_0)) (not (p10 c_0 c_0)) (not (p4 c_1)) )(or (p15 c_1 c_0) (not (p3 c_0)) (not (p10 c_0 c_0)) (not (p1 c_0 c_1)) (not (p1 c_1 c_1)) (not (p9 c_0)) (= c_0 c_1) (not (p3 c_1)) (not (p10 c_1 c_0)) (not (p4 c_1)) )(or (p15 c_1 c_0) (not (p3 c_1)) (not (p10 c_1 c_0)) (not (p1 c_1 c_1)) (not (p1 c_0 c_1)) (not (p9 c_0)) (= c_1 c_0) (not (p3 c_0)) (not (p10 c_0 c_0)) (not (p4 c_1)) )(or (p15 c_1 c_0) (not (p3 c_1)) (not (p10 c_1 c_0)) (not (p1 c_1 c_1)) (not (p1 c_1 c_1)) (not (p9 c_0)) (= c_1 c_1) (not (p3 c_1)) (not (p10 c_1 c_0)) (not (p4 c_1)) )(or (p15 c_1 c_1) (not (p3 c_0)) (not (p10 c_0 c_1)) (not (p1 c_0 c_1)) (not (p1 c_0 c_1)) (not (p9 c_1)) (= c_0 c_0) (not (p3 c_0)) (not (p10 c_0 c_1)) (not (p4 c_1)) )(or (p15 c_1 c_1) (not (p3 c_0)) (not (p10 c_0 c_1)) (not (p1 c_0 c_1)) (not (p1 c_1 c_1)) (not (p9 c_1)) (= c_0 c_1) (not (p3 c_1)) (not (p10 c_1 c_1)) (not (p4 c_1)) )(or (p15 c_1 c_1) (not (p3 c_1)) (not (p10 c_1 c_1)) (not (p1 c_1 c_1)) (not (p1 c_0 c_1)) (not (p9 c_1)) (= c_1 c_0) (not (p3 c_0)) (not (p10 c_0 c_1)) (not (p4 c_1)) )(or (p15 c_1 c_1) (not (p3 c_1)) (not (p10 c_1 c_1)) (not (p1 c_1 c_1)) (not (p1 c_1 c_1)) (not (p9 c_1)) (= c_1 c_1) (not (p3 c_1)) (not (p10 c_1 c_1)) (not (p4 c_1)) )(or (p10 (f16 c_0 c_0 c_0) c_0) (not (p3 c_0)) (not (p10 c_0 c_0)) (not (p9 c_0)) (not (p9 c_0)) (= c_0 c_0) (not (p10 c_0 c_0)) )(or (p10 (f16 c_0 c_0 c_1) c_0) (not (p3 c_1)) (not (p10 c_1 c_0)) (not (p9 c_0)) (not (p9 c_0)) (= c_0 c_0) (not (p10 c_1 c_0)) )(or (p10 (f16 c_0 c_1 c_0) c_1) (not (p3 c_0)) (not (p10 c_0 c_1)) (not (p9 c_1)) (not (p9 c_0)) (= c_0 c_1) (not (p10 c_0 c_0)) )(or (p10 (f16 c_0 c_1 c_1) c_1) (not (p3 c_1)) (not (p10 c_1 c_1)) (not (p9 c_1)) (not (p9 c_0)) (= c_0 c_1) (not (p10 c_1 c_0)) )(or (p10 (f16 c_1 c_0 c_0) c_0) (not (p3 c_0)) (not (p10 c_0 c_0)) (not (p9 c_0)) (not (p9 c_1)) (= c_1 c_0) (not (p10 c_0 c_1)) )(or (p10 (f16 c_1 c_0 c_1) c_0) (not (p3 c_1)) (not (p10 c_1 c_0)) (not (p9 c_0)) (not (p9 c_1)) (= c_1 c_0) (not (p10 c_1 c_1)) )(or (p10 (f16 c_1 c_1 c_0) c_1) (not (p3 c_0)) (not (p10 c_0 c_1)) (not (p9 c_1)) (not (p9 c_1)) (= c_1 c_1) (not (p10 c_0 c_1)) )(or (p10 (f16 c_1 c_1 c_1) c_1) (not (p3 c_1)) (not (p10 c_1 c_1)) (not (p9 c_1)) (not (p9 c_1)) (= c_1 c_1) (not (p10 c_1 c_1)) )(or (not (p1 c_0 c_0)) (= c_0 c_0) (not (p3 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)) (= c_0 c_0) (not (p4 c_0)) (= c_0 c_0) )(or (not (p1 c_0 c_0)) (= c_0 c_0) (not (p3 c_1)) (p14 c_0 c_1 c_0) (not (p3 c_0)) (not (p1 c_0 c_0)) (not (p1 c_1 c_0)) (not (p3 c_0)) (= c_0 c_1) (not (p4 c_0)) (= c_1 c_0) )(or (not (p1 c_0 c_0)) (= c_0 c_1) (not (p3 c_0)) (p14 c_0 c_0 c_1) (not (p3 c_0)) (not (p1 c_1 c_0)) (not (p1 c_0 c_0)) (not (p3 c_1)) (= c_0 c_0) (not (p4 c_0)) (= c_0 c_1) )(or (not (p1 c_0 c_0)) (= c_0 c_1) (not (p3 c_1)) (p14 c_0 c_1 c_1) (not (p3 c_0)) (not (p1 c_1 c_0)) (not (p1 c_1 c_0)) (not (p3 c_1)) (= c_0 c_1) (not (p4 c_0)) (= c_1 c_1) )(or (not (p1 c_0 c_1)) (= c_0 c_0) (not (p3 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)) (= c_0 c_0) (not (p4 c_1)) (= c_0 c_0) )(or (not (p1 c_0 c_1)) (= c_0 c_0) (not (p3 c_1)) (p14 c_0 c_1 c_0) (not (p3 c_0)) (not (p1 c_0 c_1)) (not (p1 c_1 c_1)) (not (p3 c_0)) (= c_0 c_1) (not (p4 c_1)) (= c_1 c_0) )(or (not (p1 c_0 c_1)) (= c_0 c_1) (not (p3 c_0)) (p14 c_0 c_0 c_1) (not (p3 c_0)) (not (p1 c_1 c_1)) (not (p1 c_0 c_1)) (not (p3 c_1)) (= c_0 c_0) (not (p4 c_1)) (= c_0 c_1) )(or (not (p1 c_0 c_1)) (= c_0 c_1) (not (p3 c_1)) (p14 c_0 c_1 c_1) (not (p3 c_0)) (not (p1 c_1 c_1)) (not (p1 c_1 c_1)) (not (p3 c_1)) (= c_0 c_1) (not (p4 c_1)) (= c_1 c_1) )(or (not (p1 c_1 c_0)) (= c_1 c_0) (not (p3 c_0)) (p14 c_1 c_0 c_0) (not (p3 c_1)) (not (p1 c_0 c_0)) (not (p1 c_0 c_0)) (not (p3 c_0)) (= c_1 c_0) (not (p4 c_0)) (= c_0 c_0) )(or (not (p1 c_1 c_0)) (= c_1 c_0) (not (p3 c_1)) (p14 c_1 c_1 c_0) (not (p3 c_1)) (not (p1 c_0 c_0)) (not (p1 c_1 c_0)) (not (p3 c_0)) (= c_1 c_1) (not (p4 c_0)) (= c_1 c_0) )(or (not (p1 c_1 c_0)) (= c_1 c_1) (not (p3 c_0)) (p14 c_1 c_0 c_1) (not (p3 c_1)) (not (p1 c_1 c_0)) (not (p1 c_0 c_0)) (not (p3 c_1)) (= c_1 c_0) (not (p4 c_0)) (= c_0 c_1) )(or (not (p1 c_1 c_0)) (= c_1 c_1) (not (p3 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)) (= c_1 c_1) (not (p4 c_0)) (= c_1 c_1) )(or (not (p1 c_1 c_1)) (= c_1 c_0) (not (p3 c_0)) (p14 c_1 c_0 c_0) (not (p3 c_1)) (not (p1 c_0 c_1)) (not (p1 c_0 c_1)) (not (p3 c_0)) (= c_1 c_0) (not (p4 c_1)) (= c_0 c_0) )(or (not (p1 c_1 c_1)) (= c_1 c_0) (not (p3 c_1)) (p14 c_1 c_1 c_0) (not (p3 c_1)) (not (p1 c_0 c_1)) (not (p1 c_1 c_1)) (not (p3 c_0)) (= c_1 c_1) (not (p4 c_1)) (= c_1 c_0) )(or (not (p1 c_1 c_1)) (= c_1 c_1) (not (p3 c_0)) (p14 c_1 c_0 c_1) (not (p3 c_1)) (not (p1 c_1 c_1)) (not (p1 c_0 c_1)) (not (p3 c_1)) (= c_1 c_0) (not (p4 c_1)) (= c_0 c_1) )(or (not (p1 c_1 c_1)) (= c_1 c_1) (not (p3 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)) (= c_1 c_1) (not (p4 c_1)) (= c_1 c_1) )(or (not (p3 c_0)) (not (p4 c_0)) (not (p3 c_0)) (not (p1 c_0 c_0)) (= c_0 c_0) (not (p1 c_0 c_0)) (= c_0 c_0) (not (p1 c_0 c_0)) (not (p4 c_0)) (not (p1 c_0 c_0)) )(or (not (p3 c_0)) (not (p4 c_0)) (not (p3 c_0)) (not (p1 c_0 c_0)) (= c_0 c_1) (not (p1 c_0 c_0)) (= c_0 c_0) (not (p1 c_0 c_1)) (not (p4 c_1)) (not (p1 c_0 c_1)) )(or (not (p3 c_0)) (not (p4 c_0)) (not (p3 c_1)) (not (p1 c_1 c_0)) (= c_0 c_0) (not (p1 c_0 c_0)) (= c_1 c_0) (not (p1 c_1 c_0)) (not (p4 c_0)) (not (p1 c_0 c_0)) )(or (not (p3 c_0)) (not (p4 c_0)) (not (p3 c_1)) (not (p1 c_1 c_0)) (= c_0 c_1) (not (p1 c_0 c_0)) (= c_1 c_0) (not (p1 c_1 c_1)) (not (p4 c_1)) (not (p1 c_0 c_1)) )(or (not (p3 c_0)) (not (p4 c_1)) (not (p3 c_0)) (not (p1 c_0 c_1)) (= c_1 c_0) (not (p1 c_0 c_1)) (= c_0 c_0) (not (p1 c_0 c_0)) (not (p4 c_0)) (not (p1 c_0 c_0)) )(or (not (p3 c_0)) (not (p4 c_1)) (not (p3 c_0)) (not (p1 c_0 c_1)) (= c_1 c_1) (not (p1 c_0 c_1)) (= c_0 c_0) (not (p1 c_0 c_1)) (not (p4 c_1)) (not (p1 c_0 c_1)) )(or (not (p3 c_0)) (not (p4 c_1)) (not (p3 c_1)) (not (p1 c_1 c_1)) (= c_1 c_0) (not (p1 c_0 c_1)) (= c_1 c_0) (not (p1 c_1 c_0)) (not (p4 c_0)) (not (p1 c_0 c_0)) )(or (not (p3 c_0)) (not (p4 c_1)) (not (p3 c_1)) (not (p1 c_1 c_1)) (= c_1 c_1) (not (p1 c_0 c_1)) (= c_1 c_0) (not (p1 c_1 c_1)) (not (p4 c_1)) (not (p1 c_0 c_1)) )(or (not (p3 c_1)) (not (p4 c_0)) (not (p3 c_0)) (not (p1 c_0 c_0)) (= c_0 c_0) (not (p1 c_1 c_0)) (= c_0 c_1) (not (p1 c_0 c_0)) (not (p4 c_0)) (not (p1 c_1 c_0)) )(or (not (p3 c_1)) (not (p4 c_0)) (not (p3 c_0)) (not (p1 c_0 c_0)) (= c_0 c_1) (not (p1 c_1 c_0)) (= c_0 c_1) (not (p1 c_0 c_1)) (not (p4 c_1)) (not (p1 c_1 c_1)) )(or (not (p3 c_1)) (not (p4 c_0)) (not (p3 c_1)) (not (p1 c_1 c_0)) (= c_0 c_0) (not (p1 c_1 c_0)) (= c_1 c_1) (not (p1 c_1 c_0)) (not (p4 c_0)) (not (p1 c_1 c_0)) )(or (not (p3 c_1)) (not (p4 c_0)) (not (p3 c_1)) (not (p1 c_1 c_0)) (= c_0 c_1) (not (p1 c_1 c_0)) (= c_1 c_1) (not (p1 c_1 c_1)) (not (p4 c_1)) (not (p1 c_1 c_1)) )(or (not (p3 c_1)) (not (p4 c_1)) (not (p3 c_0)) (not (p1 c_0 c_1)) (= c_1 c_0) (not (p1 c_1 c_1)) (= c_0 c_1) (not (p1 c_0 c_0)) (not (p4 c_0)) (not (p1 c_1 c_0)) )(or (not (p3 c_1)) (not (p4 c_1)) (not (p3 c_0)) (not (p1 c_0 c_1)) (= c_1 c_1) (not (p1 c_1 c_1)) (= c_0 c_1) (not (p1 c_0 c_1)) (not (p4 c_1)) (not (p1 c_1 c_1)) )(or (not (p3 c_1)) (not (p4 c_1)) (not (p3 c_1)) (not (p1 c_1 c_1)) (= c_1 c_0) (not (p1 c_1 c_1)) (= c_1 c_1) (not (p1 c_1 c_0)) (not (p4 c_0)) (not (p1 c_1 c_0)) )(or (not (p3 c_1)) (not (p4 c_1)) (not (p3 c_1)) (not (p1 c_1 c_1)) (= c_1 c_1) (not (p1 c_1 c_1)) (= c_1 c_1) (not (p1 c_1 c_1)) (not (p4 c_1)) (not (p1 c_1 c_1)) )(or (not (p14 c_0 c_0 c_0)) (= c_0 c_0) (p1 c_0 (f17 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) )(or (not (p14 c_0 c_0 c_1)) (= c_0 c_0) (p1 c_1 (f17 c_0 c_0 c_1)) (not (p3 c_0)) (= c_0 c_1) (not (p3 c_1)) (not (p3 c_0)) (= c_0 c_1) )(or (not (p14 c_0 c_1 c_0)) (= c_0 c_1) (p1 c_0 (f17 c_0 c_1 c_0)) (not (p3 c_1)) (= c_1 c_0) (not (p3 c_0)) (not (p3 c_0)) (= c_0 c_0) )(or (not (p14 c_0 c_1 c_1)) (= c_0 c_1) (p1 c_1 (f17 c_0 c_1 c_1)) (not (p3 c_1)) (= c_1 c_1) (not (p3 c_1)) (not (p3 c_0)) (= c_0 c_1) )(or (not (p14 c_1 c_0 c_0)) (= c_1 c_0) (p1 c_0 (f17 c_1 c_0 c_0)) (not (p3 c_0)) (= c_0 c_0) (not (p3 c_0)) (not (p3 c_1)) (= c_1 c_0) )(or (not (p14 c_1 c_0 c_1)) (= c_1 c_0) (p1 c_1 (f17 c_1 c_0 c_1)) (not (p3 c_0)) (= c_0 c_1) (not (p3 c_1)) (not (p3 c_1)) (= c_1 c_1) )(or (not (p14 c_1 c_1 c_0)) (= c_1 c_1) (p1 c_0 (f17 c_1 c_1 c_0)) (not (p3 c_1)) (= c_1 c_0) (not (p3 c_0)) (not (p3 c_1)) (= c_1 c_0) )(or (not (p14 c_1 c_1 c_1)) (= c_1 c_1) (p1 c_1 (f17 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) )(p4 c8) (or (not (p3 c_0)) (= c_0 c_0) (not (p3 c_0)) (p1 c_0 (f2 c_0 c_0)) )(or (not (p3 c_0)) (= c_0 c_1) (not (p3 c_1)) (p1 c_1 (f2 c_0 c_1)) )(or (not (p3 c_1)) (= c_1 c_0) (not (p3 c_0)) (p1 c_0 (f2 c_1 c_0)) )(or (not (p3 c_1)) (= c_1 c_1) (not (p3 c_1)) (p1 c_1 (f2 c_1 c_1)) )(or (= c_0 c_0) (= c_0 c_0) (not (p10 c_0 c18)) (not (p3 c_0)) (not (p3 c_0)) (= c_0 c_0) (not (p10 c_0 c18)) (p14 c_0 c_0 c_0) (not (p3 c_0)) (not (p10 c_0 c18)) )(or (= c_0 c_0) (= c_1 c_0) (not (p10 c_0 c18)) (not (p3 c_0)) (not (p3 c_1)) (= c_1 c_0) (not (p10 c_0 c18)) (p14 c_1 c_0 c_0) (not (p3 c_0)) (not (p10 c_1 c18)) )(or (= c_0 c_1) (= c_0 c_1) (not (p10 c_0 c18)) (not (p3 c_0)) (not (p3 c_0)) (= c_0 c_0) (not (p10 c_1 c18)) (p14 c_0 c_0 c_1) (not (p3 c_1)) (not (p10 c_0 c18)) )(or (= c_0 c_1) (= c_1 c_1) (not (p10 c_0 c18)) (not (p3 c_0)) (not (p3 c_1)) (= c_1 c_0) (not (p10 c_1 c18)) (p14 c_1 c_0 c_1) (not (p3 c_1)) (not (p10 c_1 c18)) )(or (= c_1 c_0) (= c_0 c_0) (not (p10 c_1 c18)) (not (p3 c_1)) (not (p3 c_0)) (= c_0 c_1) (not (p10 c_0 c18)) (p14 c_0 c_1 c_0) (not (p3 c_0)) (not (p10 c_0 c18)) )(or (= c_1 c_0) (= c_1 c_0) (not (p10 c_1 c18)) (not (p3 c_1)) (not (p3 c_1)) (= c_1 c_1) (not (p10 c_0 c18)) (p14 c_1 c_1 c_0) (not (p3 c_0)) (not (p10 c_1 c18)) )(or (= c_1 c_1) (= c_0 c_1) (not (p10 c_1 c18)) (not (p3 c_1)) (not (p3 c_0)) (= c_0 c_1) (not (p10 c_1 c18)) (p14 c_0 c_1 c_1) (not (p3 c_1)) (not (p10 c_0 c18)) )(or (= c_1 c_1) (= c_1 c_1) (not (p10 c_1 c18)) (not (p3 c_1)) (not (p3 c_1)) (= c_1 c_1) (not (p10 c_1 c18)) (p14 c_1 c_1 c_1) (not (p3 c_1)) (not (p10 c_1 c18)) )(or (= c_0 c_0) (not (p3 c_0)) (p10 c_0 (f13 c_0 c_0 c_0)) (= c_0 c_0) (p14 c_0 c_0 c_0) (= c_0 c_0) (not (p3 c_0)) (not (p3 c_0)) )(or (= c_0 c_0) (not (p3 c_1)) (p10 c_0 (f13 c_0 c_0 c_1)) (= c_0 c_1) (p14 c_0 c_0 c_1) (= c_0 c_1) (not (p3 c_0)) (not (p3 c_0)) )(or (= c_0 c_1) (not (p3 c_0)) (p10 c_0 (f13 c_0 c_1 c_0)) (= c_0 c_0) (p14 c_0 c_1 c_0) (= c_1 c_0) (not (p3 c_1)) (not (p3 c_0)) )(or (= c_0 c_1) (not (p3 c_1)) (p10 c_0 (f13 c_0 c_1 c_1)) (= c_0 c_1) (p14 c_0 c_1 c_1) (= c_1 c_1) (not (p3 c_1)) (not (p3 c_0)) )(or (= c_1 c_0) (not (p3 c_0)) (p10 c_1 (f13 c_1 c_0 c_0)) (= c_1 c_0) (p14 c_1 c_0 c_0) (= c_0 c_0) (not (p3 c_0)) (not (p3 c_1)) )(or (= c_1 c_0) (not (p3 c_1)) (p10 c_1 (f13 c_1 c_0 c_1)) (= c_1 c_1) (p14 c_1 c_0 c_1) (= c_0 c_1) (not (p3 c_0)) (not (p3 c_1)) )(or (= c_1 c_1) (not (p3 c_0)) (p10 c_1 (f13 c_1 c_1 c_0)) (= c_1 c_0) (p14 c_1 c_1 c_0) (= c_1 c_0) (not (p3 c_1)) (not (p3 c_1)) )(or (= c_1 c_1) (not (p3 c_1)) (p10 c_1 (f13 c_1 c_1 c_1)) (= c_1 c_1) (p14 c_1 c_1 c_1) (= c_1 c_1) (not (p3 c_1)) (not (p3 c_1)) )(or (p14 c_0 c_0 c_0) (= c_0 c_0) (= c_0 c_0) (not (p3 c_0)) (not (p3 c_0)) (p10 c_0 (f13 c_0 c_0 c_0)) (not (p3 c_0)) (= c_0 c_0) )(or (p14 c_0 c_0 c_1) (= c_0 c_0) (= c_0 c_1) (not (p3 c_0)) (not (p3 c_0)) (p10 c_1 (f13 c_0 c_0 c_1)) (not (p3 c_1)) (= c_0 c_1) )(or (p14 c_0 c_1 c_0) (= c_0 c_1) (= c_1 c_0) (not (p3 c_0)) (not (p3 c_1)) (p10 c_0 (f13 c_0 c_1 c_0)) (not (p3 c_0)) (= c_0 c_0) )(or (p14 c_0 c_1 c_1) (= c_0 c_1) (= c_1 c_1) (not (p3 c_0)) (not (p3 c_1)) (p10 c_1 (f13 c_0 c_1 c_1)) (not (p3 c_1)) (= c_0 c_1) )(or (p14 c_1 c_0 c_0) (= c_1 c_0) (= c_0 c_0) (not (p3 c_1)) (not (p3 c_0)) (p10 c_0 (f13 c_1 c_0 c_0)) (not (p3 c_0)) (= c_1 c_0) )(or (p14 c_1 c_0 c_1) (= c_1 c_0) (= c_0 c_1) (not (p3 c_1)) (not (p3 c_0)) (p10 c_1 (f13 c_1 c_0 c_1)) (not (p3 c_1)) (= c_1 c_1) )(or (p14 c_1 c_1 c_0) (= c_1 c_1) (= c_1 c_0) (not (p3 c_1)) (not (p3 c_1)) (p10 c_0 (f13 c_1 c_1 c_0)) (not (p3 c_0)) (= c_1 c_0) )(or (p14 c_1 c_1 c_1) (= c_1 c_1) (= c_1 c_1) (not (p3 c_1)) (not (p3 c_1)) (p10 c_1 (f13 c_1 c_1 c_1)) (not (p3 c_1)) (= c_1 c_1) )(or (= c_0 c_0) (not (p9 c_0)) (not (p10 c_0 c_0)) (not (p10 c_0 c_0)) (not (p3 c_0)) (not (p10 c_0 c_0)) (not (p3 c_0)) (not (p10 c_0 c_0)) (p14 c_0 c_0 c_0) (not (p9 c_0)) (not (p10 c_0 c_0)) (not (p10 c_0 c_0)) (= c_0 c_0) (= c_0 c_0) (= c_0 c_0) (not (p3 c_0)) )(or (= c_0 c_0) (not (p9 c_0)) (not (p10 c_0 c_0)) (not (p10 c_0 c_0)) (not (p3 c_0)) (not (p10 c_1 c_0)) (not (p3 c_1)) (not (p10 c_1 c_0)) (p14 c_0 c_1 c_0) (not (p9 c_0)) (not (p10 c_0 c_0)) (not (p10 c_0 c_0)) (= c_0 c_0) (= c_1 c_0) (= c_0 c_1) (not (p3 c_0)) )(or (= c_0 c_0) (not (p9 c_0)) (not (p10 c_0 c_0)) (not (p10 c_1 c_0)) (not (p3 c_1)) (not (p10 c_0 c_0)) (not (p3 c_0)) (not (p10 c_0 c_0)) (p14 c_0 c_0 c_1) (not (p9 c_0)) (not (p10 c_1 c_0)) (not (p10 c_0 c_0)) (= c_0 c_1) (= c_0 c_1) (= c_0 c_0) (not (p3 c_0)) )(or (= c_0 c_0) (not (p9 c_0)) (not (p10 c_0 c_0)) (not (p10 c_1 c_0)) (not (p3 c_1)) (not (p10 c_1 c_0)) (not (p3 c_1)) (not (p10 c_1 c_0)) (p14 c_0 c_1 c_1) (not (p9 c_0)) (not (p10 c_1 c_0)) (not (p10 c_0 c_0)) (= c_0 c_1) (= c_1 c_1) (= c_0 c_1) (not (p3 c_0)) )(or (= c_0 c_0) (not (p9 c_0)) (not (p10 c_1 c_0)) (not (p10 c_0 c_0)) (not (p3 c_0)) (not (p10 c_0 c_0)) (not (p3 c_0)) (not (p10 c_0 c_0)) (p14 c_1 c_0 c_0) (not (p9 c_0)) (not (p10 c_0 c_0)) (not (p10 c_1 c_0)) (= c_1 c_0) (= c_0 c_0) (= c_1 c_0) (not (p3 c_1)) )(or (= c_0 c_0) (not (p9 c_0)) (not (p10 c_1 c_0)) (not (p10 c_0 c_0)) (not (p3 c_0)) (not (p10 c_1 c_0)) (not (p3 c_1)) (not (p10 c_1 c_0)) (p14 c_1 c_1 c_0) (not (p9 c_0)) (not (p10 c_0 c_0)) (not (p10 c_1 c_0)) (= c_1 c_0) (= c_1 c_0) (= c_1 c_1) (not (p3 c_1)) )(or (= c_0 c_0) (not (p9 c_0)) (not (p10 c_1 c_0)) (not (p10 c_1 c_0)) (not (p3 c_1)) (not (p10 c_0 c_0)) (not (p3 c_0)) (not (p10 c_0 c_0)) (p14 c_1 c_0 c_1) (not (p9 c_0)) (not (p10 c_1 c_0)) (not (p10 c_1 c_0)) (= c_1 c_1) (= c_0 c_1) (= c_1 c_0) (not (p3 c_1)) )(or (= c_0 c_0) (not (p9 c_0)) (not (p10 c_1 c_0)) (not (p10 c_1 c_0)) (not (p3 c_1)) (not (p10 c_1 c_0)) (not (p3 c_1)) (not (p10 c_1 c_0)) (p14 c_1 c_1 c_1) (not (p9 c_0)) (not (p10 c_1 c_0)) (not (p10 c_1 c_0)) (= c_1 c_1) (= c_1 c_1) (= c_1 c_1) (not (p3 c_1)) )(or (= c_0 c_1) (not (p9 c_1)) (not (p10 c_0 c_1)) (not (p10 c_0 c_0)) (not (p3 c_0)) (not (p10 c_0 c_1)) (not (p3 c_0)) (not (p10 c_0 c_0)) (p14 c_0 c_0 c_0) (not (p9 c_0)) (not (p10 c_0 c_1)) (not (p10 c_0 c_0)) (= c_0 c_0) (= c_0 c_0) (= c_0 c_0) (not (p3 c_0)) )(or (= c_0 c_1) (not (p9 c_1)) (not (p10 c_0 c_1)) (not (p10 c_0 c_0)) (not (p3 c_0)) (not (p10 c_1 c_1)) (not (p3 c_1)) (not (p10 c_1 c_0)) (p14 c_0 c_1 c_0) (not (p9 c_0)) (not (p10 c_0 c_1)) (not (p10 c_0 c_0)) (= c_0 c_0) (= c_1 c_0) (= c_0 c_1) (not (p3 c_0)) )(or (= c_0 c_1) (not (p9 c_1)) (not (p10 c_0 c_1)) (not (p10 c_1 c_0)) (not (p3 c_1)) (not (p10 c_0 c_1)) (not (p3 c_0)) (not (p10 c_0 c_0)) (p14 c_0 c_0 c_1) (not (p9 c_0)) (not (p10 c_1 c_1)) (not (p10 c_0 c_0)) (= c_0 c_1) (= c_0 c_1) (= c_0 c_0) (not (p3 c_0)) )(or (= c_0 c_1) (not (p9 c_1)) (not (p10 c_0 c_1)) (not (p10 c_1 c_0)) (not (p3 c_1)) (not (p10 c_1 c_1)) (not (p3 c_1)) (not (p10 c_1 c_0)) (p14 c_0 c_1 c_1) (not (p9 c_0)) (not (p10 c_1 c_1)) (not (p10 c_0 c_0)) (= c_0 c_1) (= c_1 c_1) (= c_0 c_1) (not (p3 c_0)) )(or (= c_0 c_1) (not (p9 c_1)) (not (p10 c_1 c_1)) (not (p10 c_0 c_0)) (not (p3 c_0)) (not (p10 c_0 c_1)) (not (p3 c_0)) (not (p10 c_0 c_0)) (p14 c_1 c_0 c_0) (not (p9 c_0)) (not (p10 c_0 c_1)) (not (p10 c_1 c_0)) (= c_1 c_0) (= c_0 c_0) (= c_1 c_0) (not (p3 c_1)) )(or (= c_0 c_1) (not (p9 c_1)) (not (p10 c_1 c_1)) (not (p10 c_0 c_0)) (not (p3 c_0)) (not (p10 c_1 c_1)) (not (p3 c_1)) (not (p10 c_1 c_0)) (p14 c_1 c_1 c_0) (not (p9 c_0)) (not (p10 c_0 c_1)) (not (p10 c_1 c_0)) (= c_1 c_0) (= c_1 c_0) (= c_1 c_1) (not (p3 c_1)) )(or (= c_0 c_1) (not (p9 c_1)) (not (p10 c_1 c_1)) (not (p10 c_1 c_0)) (not (p3 c_1)) (not (p10 c_0 c_1)) (not (p3 c_0)) (not (p10 c_0 c_0)) (p14 c_1 c_0 c_1) (not (p9 c_0)) (not (p10 c_1 c_1)) (not (p10 c_1 c_0)) (= c_1 c_1) (= c_0 c_1) (= c_1 c_0) (not (p3 c_1)) )(or (= c_0 c_1) (not (p9 c_1)) (not (p10 c_1 c_1)) (not (p10 c_1 c_0)) (not (p3 c_1)) (not (p10 c_1 c_1)) (not (p3 c_1)) (not (p10 c_1 c_0)) (p14 c_1 c_1 c_1) (not (p9 c_0)) (not (p10 c_1 c_1)) (not (p10 c_1 c_0)) (= c_1 c_1) (= c_1 c_1) (= c_1 c_1) (not (p3 c_1)) )(or (= c_1 c_0) (not (p9 c_0)) (not (p10 c_0 c_0)) (not (p10 c_0 c_1)) (not (p3 c_0)) (not (p10 c_0 c_0)) (not (p3 c_0)) (not (p10 c_0 c_1)) (p14 c_0 c_0 c_0) (not (p9 c_1)) (not (p10 c_0 c_0)) (not (p10 c_0 c_1)) (= c_0 c_0) (= c_0 c_0) (= c_0 c_0) (not (p3 c_0)) )(or (= c_1 c_0) (not (p9 c_0)) (not (p10 c_0 c_0)) (not (p10 c_0 c_1)) (not (p3 c_0)) (not (p10 c_1 c_0)) (not (p3 c_1)) (not (p10 c_1 c_1)) (p14 c_0 c_1 c_0) (not (p9 c_1)) (not (p10 c_0 c_0)) (not (p10 c_0 c_1)) (= c_0 c_0) (= c_1 c_0) (= c_0 c_1) (not (p3 c_0)) )(or (= c_1 c_0) (not (p9 c_0)) (not (p10 c_0 c_0)) (not (p10 c_1 c_1)) (not (p3 c_1)) (not (p10 c_0 c_0)) (not (p3 c_0)) (not (p10 c_0 c_1)) (p14 c_0 c_0 c_1) (not (p9 c_1)) (not (p10 c_1 c_0)) (not (p10 c_0 c_1)) (= c_0 c_1) (= c_0 c_1) (= c_0 c_0) (not (p3 c_0)) )(or (= c_1 c_0) (not (p9 c_0)) (not (p10 c_0 c_0)) (not (p10 c_1 c_1)) (not (p3 c_1)) (not (p10 c_1 c_0)) (not (p3 c_1)) (not (p10 c_1 c_1)) (p14 c_0 c_1 c_1) (not (p9 c_1)) (not (p10 c_1 c_0)) (not (p10 c_0 c_1)) (= c_0 c_1) (= c_1 c_1) (= c_0 c_1) (not (p3 c_0)) )(or (= c_1 c_0) (not (p9 c_0)) (not (p10 c_1 c_0)) (not (p10 c_0 c_1)) (not (p3 c_0)) (not (p10 c_0 c_0)) (not (p3 c_0)) (not (p10 c_0 c_1)) (p14 c_1 c_0 c_0) (not (p9 c_1)) (not (p10 c_0 c_0)) (not (p10 c_1 c_1)) (= c_1 c_0) (= c_0 c_0) (= c_1 c_0) (not (p3 c_1)) )(or (= c_1 c_0) (not (p9 c_0)) (not (p10 c_1 c_0)) (not (p10 c_0 c_1)) (not (p3 c_0)) (not (p10 c_1 c_0)) (not (p3 c_1)) (not (p10 c_1 c_1)) (p14 c_1 c_1 c_0) (not (p9 c_1)) (not (p10 c_0 c_0)) (not (p10 c_1 c_1)) (= c_1 c_0) (= c_1 c_0) (= c_1 c_1) (not (p3 c_1)) )(or (= c_1 c_0) (not (p9 c_0)) (not (p10 c_1 c_0)) (not (p10 c_1 c_1)) (not (p3 c_1)) (not (p10 c_0 c_0)) (not (p3 c_0)) (not (p10 c_0 c_1)) (p14 c_1 c_0 c_1) (not (p9 c_1)) (not (p10 c_1 c_0)) (not (p10 c_1 c_1)) (= c_1 c_1) (= c_0 c_1) (= c_1 c_0) (not (p3 c_1)) )(or (= c_1 c_0) (not (p9 c_0)) (not (p10 c_1 c_0)) (not (p10 c_1 c_1)) (not (p3 c_1)) (not (p10 c_1 c_0)) (not (p3 c_1)) (not (p10 c_1 c_1)) (p14 c_1 c_1 c_1) (not (p9 c_1)) (not (p10 c_1 c_0)) (not (p10 c_1 c_1)) (= c_1 c_1) (= c_1 c_1) (= c_1 c_1) (not (p3 c_1)) )(or (= c_1 c_1) (not (p9 c_1)) (not (p10 c_0 c_1)) (not (p10 c_0 c_1)) (not (p3 c_0)) (not (p10 c_0 c_1)) (not (p3 c_0)) (not (p10 c_0 c_1)) (p14 c_0 c_0 c_0) (not (p9 c_1)) (not (p10 c_0 c_1)) (not (p10 c_0 c_1)) (= c_0 c_0) (= c_0 c_0) (= c_0 c_0) (not (p3 c_0)) )(or (= c_1 c_1) (not (p9 c_1)) (not (p10 c_0 c_1)) (not (p10 c_0 c_1)) (not (p3 c_0)) (not (p10 c_1 c_1)) (not (p3 c_1)) (not (p10 c_1 c_1)) (p14 c_0 c_1 c_0) (not (p9 c_1)) (not (p10 c_0 c_1)) (not (p10 c_0 c_1)) (= c_0 c_0) (= c_1 c_0) (= c_0 c_1) (not (p3 c_0)) )(or (= c_1 c_1) (not (p9 c_1)) (not (p10 c_0 c_1)) (not (p10 c_1 c_1)) (not (p3 c_1)) (not (p10 c_0 c_1)) (not (p3 c_0)) (not (p10 c_0 c_1)) (p14 c_0 c_0 c_1) (not (p9 c_1)) (not (p10 c_1 c_1)) (not (p10 c_0 c_1)) (= c_0 c_1) (= c_0 c_1) (= c_0 c_0) (not (p3 c_0)) )(or (= c_1 c_1) (not (p9 c_1)) (not (p10 c_0 c_1)) (not (p10 c_1 c_1)) (not (p3 c_1)) (not (p10 c_1 c_1)) (not (p3 c_1)) (not (p10 c_1 c_1)) (p14 c_0 c_1 c_1) (not (p9 c_1)) (not (p10 c_1 c_1)) (not (p10 c_0 c_1)) (= c_0 c_1) (= c_1 c_1) (= c_0 c_1) (not (p3 c_0)) )(or (= c_1 c_1) (not (p9 c_1)) (not (p10 c_1 c_1)) (not (p10 c_0 c_1)) (not (p3 c_0)) (not (p10 c_0 c_1)) (not (p3 c_0)) (not (p10 c_0 c_1)) (p14 c_1 c_0 c_0) (not (p9 c_1)) (not (p10 c_0 c_1)) (not (p10 c_1 c_1)) (= c_1 c_0) (= c_0 c_0) (= c_1 c_0) (not (p3 c_1)) )(or (= c_1 c_1) (not (p9 c_1)) (not (p10 c_1 c_1)) (not (p10 c_0 c_1)) (not (p3 c_0)) (not (p10 c_1 c_1)) (not (p3 c_1)) (not (p10 c_1 c_1)) (p14 c_1 c_1 c_0) (not (p9 c_1)) (not (p10 c_0 c_1)) (not (p10 c_1 c_1)) (= c_1 c_0) (= c_1 c_0) (= c_1 c_1) (not (p3 c_1)) )(or (= c_1 c_1) (not (p9 c_1)) (not (p10 c_1 c_1)) (not (p10 c_1 c_1)) (not (p3 c_1)) (not (p10 c_0 c_1)) (not (p3 c_0)) (not (p10 c_0 c_1)) (p14 c_1 c_0 c_1) (not (p9 c_1)) (not (p10 c_1 c_1)) (not (p10 c_1 c_1)) (= c_1 c_1) (= c_0 c_1) (= c_1 c_0) (not (p3 c_1)) )(or (= c_1 c_1) (not (p9 c_1)) (not (p10 c_1 c_1)) (not (p10 c_1 c_1)) (not (p3 c_1)) (not (p10 c_1 c_1)) (not (p3 c_1)) (not (p10 c_1 c_1)) (p14 c_1 c_1 c_1) (not (p9 c_1)) (not (p10 c_1 c_1)) (not (p10 c_1 c_1)) (= c_1 c_1) (= c_1 c_1) (= c_1 c_1) (not (p3 c_1)) )(or (= 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) (not (p3 c_0)) (p1 c_0 (f17 c_0 c_0 c_0)) )(or (= c_0 c_0) (not (p3 c_0)) (not (p14 c_0 c_1 c_0)) (= c_1 c_0) (not (p3 c_0)) (= c_0 c_1) (not (p3 c_1)) (p1 c_0 (f17 c_0 c_1 c_0)) )(or (= c_0 c_1) (not (p3 c_0)) (not (p14 c_0 c_0 c_1)) (= c_0 c_1) (not (p3 c_1)) (= c_0 c_0) (not (p3 c_0)) (p1 c_0 (f17 c_0 c_0 c_1)) )(or (= c_0 c_1) (not (p3 c_0)) (not (p14 c_0 c_1 c_1)) (= c_1 c_1) (not (p3 c_1)) (= c_0 c_1) (not (p3 c_1)) (p1 c_0 (f17 c_0 c_1 c_1)) )(or (= c_1 c_0) (not (p3 c_1)) (not (p14 c_1 c_0 c_0)) (= c_0 c_0) (not (p3 c_0)) (= c_1 c_0) (not (p3 c_0)) (p1 c_1 (f17 c_1 c_0 c_0)) )(or (= c_1 c_0) (not (p3 c_1)) (not (p14 c_1 c_1 c_0)) (= c_1 c_0) (not (p3 c_0)) (= c_1 c_1) (not (p3 c_1)) (p1 c_1 (f17 c_1 c_1 c_0)) )(or (= c_1 c_1) (not (p3 c_1)) (not (p14 c_1 c_0 c_1)) (= c_0 c_1) (not (p3 c_1)) (= c_1 c_0) (not (p3 c_0)) (p1 c_1 (f17 c_1 c_0 c_1)) )(or (= 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) (not (p3 c_1)) (p1 c_1 (f17 c_1 c_1 c_1)) )(or (p14 c_0 c_0 c_0) (not (p3 c_0)) (= c_0 c_0) (= c_0 c_0) (not (p3 c_0)) (p9 (f13 c_0 c_0 c_0)) (not (p3 c_0)) (= c_0 c_0) )(or (p14 c_0 c_0 c_1) (not (p3 c_1)) (= c_0 c_1) (= c_0 c_1) (not (p3 c_0)) (p9 (f13 c_0 c_0 c_1)) (not (p3 c_0)) (= c_0 c_0) )(or (p14 c_0 c_1 c_0) (not (p3 c_0)) (= c_1 c_0) (= c_0 c_0) (not (p3 c_1)) (p9 (f13 c_0 c_1 c_0)) (not (p3 c_0)) (= c_0 c_1) )(or (p14 c_0 c_1 c_1) (not (p3 c_1)) (= c_1 c_1) (= c_0 c_1) (not (p3 c_1)) (p9 (f13 c_0 c_1 c_1)) (not (p3 c_0)) (= c_0 c_1) )(or (p14 c_1 c_0 c_0) (not (p3 c_0)) (= c_0 c_0) (= c_1 c_0) (not (p3 c_0)) (p9 (f13 c_1 c_0 c_0)) (not (p3 c_1)) (= c_1 c_0) )(or (p14 c_1 c_0 c_1) (not (p3 c_1)) (= c_0 c_1) (= c_1 c_1) (not (p3 c_0)) (p9 (f13 c_1 c_0 c_1)) (not (p3 c_1)) (= c_1 c_0) )(or (p14 c_1 c_1 c_0) (not (p3 c_0)) (= c_1 c_0) (= c_1 c_0) (not (p3 c_1)) (p9 (f13 c_1 c_1 c_0)) (not (p3 c_1)) (= c_1 c_1) )(or (p14 c_1 c_1 c_1) (not (p3 c_1)) (= c_1 c_1) (= c_1 c_1) (not (p3 c_1)) (p9 (f13 c_1 c_1 c_1)) (not (p3 c_1)) (= c_1 c_1) )(or (not (= (f5 c_0) (f6 c_0))) (not (p4 c_0)) )(or (not (= (f5 c_1) (f6 c_1))) (not (p4 c_1)) )(or (= (f16 c_0 c_0 c_0) c_0)(= (f16 c_0 c_0 c_0) c_1))(or (= (f16 c_0 c_0 c_1) c_0)(= (f16 c_0 c_0 c_1) c_1))(or (= (f16 c_0 c_1 c_0) c_0)(= (f16 c_0 c_1 c_0) c_1))(or (= (f16 c_0 c_1 c_1) c_0)(= (f16 c_0 c_1 c_1) c_1))(or (= (f16 c_1 c_0 c_0) c_0)(= (f16 c_1 c_0 c_0) c_1))(or (= (f16 c_1 c_0 c_1) c_0)(= (f16 c_1 c_0 c_1) c_1))(or (= (f16 c_1 c_1 c_0) c_0)(= (f16 c_1 c_1 c_0) c_1))(or (= (f16 c_1 c_1 c_1) c_0)(= (f16 c_1 c_1 c_1) c_1))(or (= (f17 c_0 c_0 c_0) c_0)(= (f17 c_0 c_0 c_0) c_1))(or (= (f17 c_0 c_0 c_1) c_0)(= (f17 c_0 c_0 c_1) c_1))(or (= (f17 c_0 c_1 c_0) c_0)(= (f17 c_0 c_1 c_0) c_1))(or (= (f17 c_0 c_1 c_1) c_0)(= (f17 c_0 c_1 c_1) c_1))(or (= (f17 c_1 c_0 c_0) c_0)(= (f17 c_1 c_0 c_0) c_1))(or (= (f17 c_1 c_0 c_1) c_0)(= (f17 c_1 c_0 c_1) c_1))(or (= (f17 c_1 c_1 c_0) c_0)(= (f17 c_1 c_1 c_0) c_1))(or (= (f17 c_1 c_1 c_1) c_0)(= (f17 c_1 c_1 c_1) c_1))(or (= (f13 c_0 c_0 c_0) c_0)(= (f13 c_0 c_0 c_0) c_1))(or (= (f13 c_0 c_0 c_1) c_0)(= (f13 c_0 c_0 c_1) c_1))(or (= (f13 c_0 c_1 c_0) c_0)(= (f13 c_0 c_1 c_0) c_1))(or (= (f13 c_0 c_1 c_1) c_0)(= (f13 c_0 c_1 c_1) c_1))(or (= (f13 c_1 c_0 c_0) c_0)(= (f13 c_1 c_0 c_0) c_1))(or (= (f13 c_1 c_0 c_1) c_0)(= (f13 c_1 c_0 c_1) c_1))(or (= (f13 c_1 c_1 c_0) c_0)(= (f13 c_1 c_1 c_0) c_1))(or (= (f13 c_1 c_1 c_1) c_0)(= (f13 c_1 c_1 c_1) c_1))(or (= (f2 c_0 c_0) c_0)(= (f2 c_0 c_0) c_1))(or (= (f2 c_0 c_1) c_0)(= (f2 c_0 c_1) c_1))(or (= (f2 c_1 c_0) c_0)(= (f2 c_1 c_0) c_1))(or (= (f2 c_1 c_1) c_0)(= (f2 c_1 c_1) c_1))(or (= (f7 c_0) c_0)(= (f7 c_0) c_1))(or (= (f7 c_1) c_0)(= (f7 c_1) c_1))(or (= (f12 c_0) c_0)(= (f12 c_0) c_1))(or (= (f12 c_1) c_0)(= (f12 c_1) c_1))(or (= (f6 c_0) c_0)(= (f6 c_0) c_1))(or (= (f6 c_1) c_0)(= (f6 c_1) c_1))(or (= (f5 c_0) c_0)(= (f5 c_0) c_1))(or (= (f5 c_1) c_0)(= (f5 c_1) c_1))(or (= (f11 c_0) c_0)(= (f11 c_0) c_1))(or (= (f11 c_1) c_0)(= (f11 c_1) c_1))(or (= c18 c_0)(= c18 c_1))(or (= c8 c_0)(= c8 c_1))))