(benchmark NEQ033_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 ((p12 U))
:extrafuns ((f43 U U U))
:extrafuns ((c6 U))
:extrafuns ((f3 U U U))
:extrafuns ((f20 U U))
:extrafuns ((f11 U U))
:extrafuns ((c15 U))
:extrapreds ((p22 U U))
:extrafuns ((f23 U U))
:extrafuns ((f17 U U))
:extrafuns ((f24 U U))
:extrafuns ((f35 U U U))
:extrafuns ((f21 U U U))
:extrafuns ((f19 U U))
:extrafuns ((f2 U U))
:extrafuns ((c8 U))
:extrafuns ((f4 U U U))
:extrafuns ((c5 U))
:extrafuns ((f18 U U))
:extrafuns ((f13 U U))
:extrafuns ((f7 U U))
:extrafuns ((f16 U U))
:extrafuns ((c49 U))
:extrafuns ((f25 U U U))
:extrafuns ((f40 U U))
:extrafuns ((f37 U U U))
:extrafuns ((f34 U U U))
:extrafuns ((f9 U U))
:extrapreds ((p26 U U))
:extrafuns ((f36 U U U))
:extrafuns ((f31 U U U U))
:extrafuns ((f14 U U))
:extrafuns ((f39 U U U))
:extrafuns ((f28 U U U))
:extrafuns ((f47 U U U))
:extrafuns ((f10 U U))
:extrafuns ((f44 U U U))
:extrafuns ((f45 U U U))
:extrafuns ((c41 U))
:extrafuns ((f33 U U))
:extrafuns ((f30 U U U))
:extrafuns ((c42 U))
:extrafuns ((f1 U U))
:extrafuns ((f46 U U U))
:extrafuns ((f27 U U))
:extrafuns ((f38 U U U))
:extrafuns ((c29 U))
:extrafuns ((f48 U U U))
:extrafuns ((f32 U U))
:extrafuns ((c_0 U))
:extrafuns ((c_1 U))
:extrafuns ((c_2 U))
:formula 
( and 
( distinct c_0 c_1 c_2 )(or (p12 c_0) (not (p12 c_0)) (not (p12 (f43 c_0 c_0))) )(or (p12 c_0) (not (p12 c_1)) (not (p12 (f43 c_0 c_1))) )(or (p12 c_0) (not (p12 c_2)) (not (p12 (f43 c_0 c_2))) )(or (p12 c_1) (not (p12 c_0)) (not (p12 (f43 c_1 c_0))) )(or (p12 c_1) (not (p12 c_1)) (not (p12 (f43 c_1 c_1))) )(or (p12 c_1) (not (p12 c_2)) (not (p12 (f43 c_1 c_2))) )(or (p12 c_2) (not (p12 c_0)) (not (p12 (f43 c_2 c_0))) )(or (p12 c_2) (not (p12 c_1)) (not (p12 (f43 c_2 c_1))) )(or (p12 c_2) (not (p12 c_2)) (not (p12 (f43 c_2 c_2))) )(or (not (p12 (f20 (f3 c_0 c6)))) (p22 (f11 c_0) c15) (not (p12 (f23 c_0))) (p12 (f17 c_0)) (not (p12 (f24 c_0))) )(or (not (p12 (f20 (f3 c_1 c6)))) (p22 (f11 c_1) c15) (not (p12 (f23 c_1))) (p12 (f17 c_1)) (not (p12 (f24 c_1))) )(or (not (p12 (f20 (f3 c_2 c6)))) (p22 (f11 c_2) c15) (not (p12 (f23 c_2))) (p12 (f17 c_2)) (not (p12 (f24 c_2))) )(= (f21 (f35 c_0 c_0) c_0) (f35 (f21 c_0 c_0) (f21 c_0 c_0))) (= (f21 (f35 c_0 c_0) c_1) (f35 (f21 c_0 c_1) (f21 c_0 c_1))) (= (f21 (f35 c_0 c_0) c_2) (f35 (f21 c_0 c_2) (f21 c_0 c_2))) (= (f21 (f35 c_0 c_1) c_0) (f35 (f21 c_0 c_0) (f21 c_1 c_0))) (= (f21 (f35 c_0 c_1) c_1) (f35 (f21 c_0 c_1) (f21 c_1 c_1))) (= (f21 (f35 c_0 c_1) c_2) (f35 (f21 c_0 c_2) (f21 c_1 c_2))) (= (f21 (f35 c_0 c_2) c_0) (f35 (f21 c_0 c_0) (f21 c_2 c_0))) (= (f21 (f35 c_0 c_2) c_1) (f35 (f21 c_0 c_1) (f21 c_2 c_1))) (= (f21 (f35 c_0 c_2) c_2) (f35 (f21 c_0 c_2) (f21 c_2 c_2))) (= (f21 (f35 c_1 c_0) c_0) (f35 (f21 c_1 c_0) (f21 c_0 c_0))) (= (f21 (f35 c_1 c_0) c_1) (f35 (f21 c_1 c_1) (f21 c_0 c_1))) (= (f21 (f35 c_1 c_0) c_2) (f35 (f21 c_1 c_2) (f21 c_0 c_2))) (= (f21 (f35 c_1 c_1) c_0) (f35 (f21 c_1 c_0) (f21 c_1 c_0))) (= (f21 (f35 c_1 c_1) c_1) (f35 (f21 c_1 c_1) (f21 c_1 c_1))) (= (f21 (f35 c_1 c_1) c_2) (f35 (f21 c_1 c_2) (f21 c_1 c_2))) (= (f21 (f35 c_1 c_2) c_0) (f35 (f21 c_1 c_0) (f21 c_2 c_0))) (= (f21 (f35 c_1 c_2) c_1) (f35 (f21 c_1 c_1) (f21 c_2 c_1))) (= (f21 (f35 c_1 c_2) c_2) (f35 (f21 c_1 c_2) (f21 c_2 c_2))) (= (f21 (f35 c_2 c_0) c_0) (f35 (f21 c_2 c_0) (f21 c_0 c_0))) (= (f21 (f35 c_2 c_0) c_1) (f35 (f21 c_2 c_1) (f21 c_0 c_1))) (= (f21 (f35 c_2 c_0) c_2) (f35 (f21 c_2 c_2) (f21 c_0 c_2))) (= (f21 (f35 c_2 c_1) c_0) (f35 (f21 c_2 c_0) (f21 c_1 c_0))) (= (f21 (f35 c_2 c_1) c_1) (f35 (f21 c_2 c_1) (f21 c_1 c_1))) (= (f21 (f35 c_2 c_1) c_2) (f35 (f21 c_2 c_2) (f21 c_1 c_2))) (= (f21 (f35 c_2 c_2) c_0) (f35 (f21 c_2 c_0) (f21 c_2 c_0))) (= (f21 (f35 c_2 c_2) c_1) (f35 (f21 c_2 c_1) (f21 c_2 c_1))) (= (f21 (f35 c_2 c_2) c_2) (f35 (f21 c_2 c_2) (f21 c_2 c_2))) (or (not (p12 (f19 (f3 c_0 c6)))) (not (p12 (f17 c_0))) )(or (not (p12 (f19 (f3 c_1 c6)))) (not (p12 (f17 c_1))) )(or (not (p12 (f19 (f3 c_2 c6)))) (not (p12 (f17 c_2))) )(or (not (p22 c15 c_0)) (= (f21 (f21 (f2 (f3 c_0 c6)) c_0) c_0) (f21 (f21 (f2 c_0) c_0) c_0)) (not (p22 c_0 (f4 c8 c6))) (not (p12 (f24 c_0))) (not (p22 c15 c_0)) (not (p22 c_0 (f4 c5 c6))) (p22 c5 (f11 c_0)) (p12 (f17 c_0)) (= c_0 (f4 (f4 c5 c6) (f18 c_0))) (p12 (f23 c_0)) )(or (not (p22 c15 c_0)) (= (f21 (f21 (f2 (f3 c_0 c6)) c_0) c_1) (f21 (f21 (f2 c_0) c_0) c_1)) (not (p22 c_1 (f4 c8 c6))) (not (p12 (f24 c_0))) (not (p22 c15 c_1)) (not (p22 c_0 (f4 c5 c6))) (p22 c5 (f11 c_0)) (p12 (f17 c_0)) (= c_0 (f4 (f4 c5 c6) (f18 c_0))) (p12 (f23 c_0)) )(or (not (p22 c15 c_0)) (= (f21 (f21 (f2 (f3 c_0 c6)) c_0) c_2) (f21 (f21 (f2 c_0) c_0) c_2)) (not (p22 c_2 (f4 c8 c6))) (not (p12 (f24 c_0))) (not (p22 c15 c_2)) (not (p22 c_0 (f4 c5 c6))) (p22 c5 (f11 c_0)) (p12 (f17 c_0)) (= c_0 (f4 (f4 c5 c6) (f18 c_0))) (p12 (f23 c_0)) )(or (not (p22 c15 c_0)) (= (f21 (f21 (f2 (f3 c_1 c6)) c_0) c_0) (f21 (f21 (f2 c_1) c_0) c_0)) (not (p22 c_0 (f4 c8 c6))) (not (p12 (f24 c_1))) (not (p22 c15 c_0)) (not (p22 c_0 (f4 c5 c6))) (p22 c5 (f11 c_1)) (p12 (f17 c_1)) (= c_0 (f4 (f4 c5 c6) (f18 c_1))) (p12 (f23 c_1)) )(or (not (p22 c15 c_0)) (= (f21 (f21 (f2 (f3 c_1 c6)) c_0) c_1) (f21 (f21 (f2 c_1) c_0) c_1)) (not (p22 c_1 (f4 c8 c6))) (not (p12 (f24 c_1))) (not (p22 c15 c_1)) (not (p22 c_0 (f4 c5 c6))) (p22 c5 (f11 c_1)) (p12 (f17 c_1)) (= c_0 (f4 (f4 c5 c6) (f18 c_1))) (p12 (f23 c_1)) )(or (not (p22 c15 c_0)) (= (f21 (f21 (f2 (f3 c_1 c6)) c_0) c_2) (f21 (f21 (f2 c_1) c_0) c_2)) (not (p22 c_2 (f4 c8 c6))) (not (p12 (f24 c_1))) (not (p22 c15 c_2)) (not (p22 c_0 (f4 c5 c6))) (p22 c5 (f11 c_1)) (p12 (f17 c_1)) (= c_0 (f4 (f4 c5 c6) (f18 c_1))) (p12 (f23 c_1)) )(or (not (p22 c15 c_0)) (= (f21 (f21 (f2 (f3 c_2 c6)) c_0) c_0) (f21 (f21 (f2 c_2) c_0) c_0)) (not (p22 c_0 (f4 c8 c6))) (not (p12 (f24 c_2))) (not (p22 c15 c_0)) (not (p22 c_0 (f4 c5 c6))) (p22 c5 (f11 c_2)) (p12 (f17 c_2)) (= c_0 (f4 (f4 c5 c6) (f18 c_2))) (p12 (f23 c_2)) )(or (not (p22 c15 c_0)) (= (f21 (f21 (f2 (f3 c_2 c6)) c_0) c_1) (f21 (f21 (f2 c_2) c_0) c_1)) (not (p22 c_1 (f4 c8 c6))) (not (p12 (f24 c_2))) (not (p22 c15 c_1)) (not (p22 c_0 (f4 c5 c6))) (p22 c5 (f11 c_2)) (p12 (f17 c_2)) (= c_0 (f4 (f4 c5 c6) (f18 c_2))) (p12 (f23 c_2)) )(or (not (p22 c15 c_0)) (= (f21 (f21 (f2 (f3 c_2 c6)) c_0) c_2) (f21 (f21 (f2 c_2) c_0) c_2)) (not (p22 c_2 (f4 c8 c6))) (not (p12 (f24 c_2))) (not (p22 c15 c_2)) (not (p22 c_0 (f4 c5 c6))) (p22 c5 (f11 c_2)) (p12 (f17 c_2)) (= c_0 (f4 (f4 c5 c6) (f18 c_2))) (p12 (f23 c_2)) )(or (not (p22 c15 c_1)) (= (f21 (f21 (f2 (f3 c_0 c6)) c_1) c_0) (f21 (f21 (f2 c_0) c_1) c_0)) (not (p22 c_0 (f4 c8 c6))) (not (p12 (f24 c_0))) (not (p22 c15 c_0)) (not (p22 c_1 (f4 c5 c6))) (p22 c5 (f11 c_0)) (p12 (f17 c_0)) (= c_1 (f4 (f4 c5 c6) (f18 c_0))) (p12 (f23 c_0)) )(or (not (p22 c15 c_1)) (= (f21 (f21 (f2 (f3 c_0 c6)) c_1) c_1) (f21 (f21 (f2 c_0) c_1) c_1)) (not (p22 c_1 (f4 c8 c6))) (not (p12 (f24 c_0))) (not (p22 c15 c_1)) (not (p22 c_1 (f4 c5 c6))) (p22 c5 (f11 c_0)) (p12 (f17 c_0)) (= c_1 (f4 (f4 c5 c6) (f18 c_0))) (p12 (f23 c_0)) )(or (not (p22 c15 c_1)) (= (f21 (f21 (f2 (f3 c_0 c6)) c_1) c_2) (f21 (f21 (f2 c_0) c_1) c_2)) (not (p22 c_2 (f4 c8 c6))) (not (p12 (f24 c_0))) (not (p22 c15 c_2)) (not (p22 c_1 (f4 c5 c6))) (p22 c5 (f11 c_0)) (p12 (f17 c_0)) (= c_1 (f4 (f4 c5 c6) (f18 c_0))) (p12 (f23 c_0)) )(or (not (p22 c15 c_1)) (= (f21 (f21 (f2 (f3 c_1 c6)) c_1) c_0) (f21 (f21 (f2 c_1) c_1) c_0)) (not (p22 c_0 (f4 c8 c6))) (not (p12 (f24 c_1))) (not (p22 c15 c_0)) (not (p22 c_1 (f4 c5 c6))) (p22 c5 (f11 c_1)) (p12 (f17 c_1)) (= c_1 (f4 (f4 c5 c6) (f18 c_1))) (p12 (f23 c_1)) )(or (not (p22 c15 c_1)) (= (f21 (f21 (f2 (f3 c_1 c6)) c_1) c_1) (f21 (f21 (f2 c_1) c_1) c_1)) (not (p22 c_1 (f4 c8 c6))) (not (p12 (f24 c_1))) (not (p22 c15 c_1)) (not (p22 c_1 (f4 c5 c6))) (p22 c5 (f11 c_1)) (p12 (f17 c_1)) (= c_1 (f4 (f4 c5 c6) (f18 c_1))) (p12 (f23 c_1)) )(or (not (p22 c15 c_1)) (= (f21 (f21 (f2 (f3 c_1 c6)) c_1) c_2) (f21 (f21 (f2 c_1) c_1) c_2)) (not (p22 c_2 (f4 c8 c6))) (not (p12 (f24 c_1))) (not (p22 c15 c_2)) (not (p22 c_1 (f4 c5 c6))) (p22 c5 (f11 c_1)) (p12 (f17 c_1)) (= c_1 (f4 (f4 c5 c6) (f18 c_1))) (p12 (f23 c_1)) )(or (not (p22 c15 c_1)) (= (f21 (f21 (f2 (f3 c_2 c6)) c_1) c_0) (f21 (f21 (f2 c_2) c_1) c_0)) (not (p22 c_0 (f4 c8 c6))) (not (p12 (f24 c_2))) (not (p22 c15 c_0)) (not (p22 c_1 (f4 c5 c6))) (p22 c5 (f11 c_2)) (p12 (f17 c_2)) (= c_1 (f4 (f4 c5 c6) (f18 c_2))) (p12 (f23 c_2)) )(or (not (p22 c15 c_1)) (= (f21 (f21 (f2 (f3 c_2 c6)) c_1) c_1) (f21 (f21 (f2 c_2) c_1) c_1)) (not (p22 c_1 (f4 c8 c6))) (not (p12 (f24 c_2))) (not (p22 c15 c_1)) (not (p22 c_1 (f4 c5 c6))) (p22 c5 (f11 c_2)) (p12 (f17 c_2)) (= c_1 (f4 (f4 c5 c6) (f18 c_2))) (p12 (f23 c_2)) )(or (not (p22 c15 c_1)) (= (f21 (f21 (f2 (f3 c_2 c6)) c_1) c_2) (f21 (f21 (f2 c_2) c_1) c_2)) (not (p22 c_2 (f4 c8 c6))) (not (p12 (f24 c_2))) (not (p22 c15 c_2)) (not (p22 c_1 (f4 c5 c6))) (p22 c5 (f11 c_2)) (p12 (f17 c_2)) (= c_1 (f4 (f4 c5 c6) (f18 c_2))) (p12 (f23 c_2)) )(or (not (p22 c15 c_2)) (= (f21 (f21 (f2 (f3 c_0 c6)) c_2) c_0) (f21 (f21 (f2 c_0) c_2) c_0)) (not (p22 c_0 (f4 c8 c6))) (not (p12 (f24 c_0))) (not (p22 c15 c_0)) (not (p22 c_2 (f4 c5 c6))) (p22 c5 (f11 c_0)) (p12 (f17 c_0)) (= c_2 (f4 (f4 c5 c6) (f18 c_0))) (p12 (f23 c_0)) )(or (not (p22 c15 c_2)) (= (f21 (f21 (f2 (f3 c_0 c6)) c_2) c_1) (f21 (f21 (f2 c_0) c_2) c_1)) (not (p22 c_1 (f4 c8 c6))) (not (p12 (f24 c_0))) (not (p22 c15 c_1)) (not (p22 c_2 (f4 c5 c6))) (p22 c5 (f11 c_0)) (p12 (f17 c_0)) (= c_2 (f4 (f4 c5 c6) (f18 c_0))) (p12 (f23 c_0)) )(or (not (p22 c15 c_2)) (= (f21 (f21 (f2 (f3 c_0 c6)) c_2) c_2) (f21 (f21 (f2 c_0) c_2) c_2)) (not (p22 c_2 (f4 c8 c6))) (not (p12 (f24 c_0))) (not (p22 c15 c_2)) (not (p22 c_2 (f4 c5 c6))) (p22 c5 (f11 c_0)) (p12 (f17 c_0)) (= c_2 (f4 (f4 c5 c6) (f18 c_0))) (p12 (f23 c_0)) )(or (not (p22 c15 c_2)) (= (f21 (f21 (f2 (f3 c_1 c6)) c_2) c_0) (f21 (f21 (f2 c_1) c_2) c_0)) (not (p22 c_0 (f4 c8 c6))) (not (p12 (f24 c_1))) (not (p22 c15 c_0)) (not (p22 c_2 (f4 c5 c6))) (p22 c5 (f11 c_1)) (p12 (f17 c_1)) (= c_2 (f4 (f4 c5 c6) (f18 c_1))) (p12 (f23 c_1)) )(or (not (p22 c15 c_2)) (= (f21 (f21 (f2 (f3 c_1 c6)) c_2) c_1) (f21 (f21 (f2 c_1) c_2) c_1)) (not (p22 c_1 (f4 c8 c6))) (not (p12 (f24 c_1))) (not (p22 c15 c_1)) (not (p22 c_2 (f4 c5 c6))) (p22 c5 (f11 c_1)) (p12 (f17 c_1)) (= c_2 (f4 (f4 c5 c6) (f18 c_1))) (p12 (f23 c_1)) )(or (not (p22 c15 c_2)) (= (f21 (f21 (f2 (f3 c_1 c6)) c_2) c_2) (f21 (f21 (f2 c_1) c_2) c_2)) (not (p22 c_2 (f4 c8 c6))) (not (p12 (f24 c_1))) (not (p22 c15 c_2)) (not (p22 c_2 (f4 c5 c6))) (p22 c5 (f11 c_1)) (p12 (f17 c_1)) (= c_2 (f4 (f4 c5 c6) (f18 c_1))) (p12 (f23 c_1)) )(or (not (p22 c15 c_2)) (= (f21 (f21 (f2 (f3 c_2 c6)) c_2) c_0) (f21 (f21 (f2 c_2) c_2) c_0)) (not (p22 c_0 (f4 c8 c6))) (not (p12 (f24 c_2))) (not (p22 c15 c_0)) (not (p22 c_2 (f4 c5 c6))) (p22 c5 (f11 c_2)) (p12 (f17 c_2)) (= c_2 (f4 (f4 c5 c6) (f18 c_2))) (p12 (f23 c_2)) )(or (not (p22 c15 c_2)) (= (f21 (f21 (f2 (f3 c_2 c6)) c_2) c_1) (f21 (f21 (f2 c_2) c_2) c_1)) (not (p22 c_1 (f4 c8 c6))) (not (p12 (f24 c_2))) (not (p22 c15 c_1)) (not (p22 c_2 (f4 c5 c6))) (p22 c5 (f11 c_2)) (p12 (f17 c_2)) (= c_2 (f4 (f4 c5 c6) (f18 c_2))) (p12 (f23 c_2)) )(or (not (p22 c15 c_2)) (= (f21 (f21 (f2 (f3 c_2 c6)) c_2) c_2) (f21 (f21 (f2 c_2) c_2) c_2)) (not (p22 c_2 (f4 c8 c6))) (not (p12 (f24 c_2))) (not (p22 c15 c_2)) (not (p22 c_2 (f4 c5 c6))) (p22 c5 (f11 c_2)) (p12 (f17 c_2)) (= c_2 (f4 (f4 c5 c6) (f18 c_2))) (p12 (f23 c_2)) )(not (p22 (f3 c_0 c6) c15)) (not (p22 (f3 c_1 c6) c15)) (not (p22 (f3 c_2 c6) c15)) (or (not (= (f11 c_0) c5)) (p12 (f13 c_0)) )(or (not (= (f11 c_1) c5)) (p12 (f13 c_1)) )(or (not (= (f11 c_2) c5)) (p12 (f13 c_2)) )(or (= c_0 c_0) (not (p22 c_0 c_0)) (p22 (f3 c_0 c6) c_0) )(or (= c_0 c_1) (not (p22 c_0 c_1)) (p22 (f3 c_0 c6) c_1) )(or (= c_0 c_2) (not (p22 c_0 c_2)) (p22 (f3 c_0 c6) c_2) )(or (= c_1 c_0) (not (p22 c_1 c_0)) (p22 (f3 c_1 c6) c_0) )(or (= c_1 c_1) (not (p22 c_1 c_1)) (p22 (f3 c_1 c6) c_1) )(or (= c_1 c_2) (not (p22 c_1 c_2)) (p22 (f3 c_1 c6) c_2) )(or (= c_2 c_0) (not (p22 c_2 c_0)) (p22 (f3 c_2 c6) c_0) )(or (= c_2 c_1) (not (p22 c_2 c_1)) (p22 (f3 c_2 c6) c_1) )(or (= c_2 c_2) (not (p22 c_2 c_2)) (p22 (f3 c_2 c6) c_2) )(or (= (f21 (f7 (f3 c_0 c6)) c_0) (f21 (f21 (f2 c_0) (f4 (f4 c5 c6) (f16 c_0))) c_0)) (p12 (f17 c_0)) (p12 (f24 c_0)) (not (p22 c15 c_0)) (p22 (f11 c_0) c15) (not (p22 c_0 (f4 c8 c6))) (not (p12 (f23 c_0))) )(or (= (f21 (f7 (f3 c_0 c6)) c_1) (f21 (f21 (f2 c_0) (f4 (f4 c5 c6) (f16 c_0))) c_1)) (p12 (f17 c_0)) (p12 (f24 c_0)) (not (p22 c15 c_1)) (p22 (f11 c_0) c15) (not (p22 c_1 (f4 c8 c6))) (not (p12 (f23 c_0))) )(or (= (f21 (f7 (f3 c_0 c6)) c_2) (f21 (f21 (f2 c_0) (f4 (f4 c5 c6) (f16 c_0))) c_2)) (p12 (f17 c_0)) (p12 (f24 c_0)) (not (p22 c15 c_2)) (p22 (f11 c_0) c15) (not (p22 c_2 (f4 c8 c6))) (not (p12 (f23 c_0))) )(or (= (f21 (f7 (f3 c_1 c6)) c_0) (f21 (f21 (f2 c_1) (f4 (f4 c5 c6) (f16 c_1))) c_0)) (p12 (f17 c_1)) (p12 (f24 c_1)) (not (p22 c15 c_0)) (p22 (f11 c_1) c15) (not (p22 c_0 (f4 c8 c6))) (not (p12 (f23 c_1))) )(or (= (f21 (f7 (f3 c_1 c6)) c_1) (f21 (f21 (f2 c_1) (f4 (f4 c5 c6) (f16 c_1))) c_1)) (p12 (f17 c_1)) (p12 (f24 c_1)) (not (p22 c15 c_1)) (p22 (f11 c_1) c15) (not (p22 c_1 (f4 c8 c6))) (not (p12 (f23 c_1))) )(or (= (f21 (f7 (f3 c_1 c6)) c_2) (f21 (f21 (f2 c_1) (f4 (f4 c5 c6) (f16 c_1))) c_2)) (p12 (f17 c_1)) (p12 (f24 c_1)) (not (p22 c15 c_2)) (p22 (f11 c_1) c15) (not (p22 c_2 (f4 c8 c6))) (not (p12 (f23 c_1))) )(or (= (f21 (f7 (f3 c_2 c6)) c_0) (f21 (f21 (f2 c_2) (f4 (f4 c5 c6) (f16 c_2))) c_0)) (p12 (f17 c_2)) (p12 (f24 c_2)) (not (p22 c15 c_0)) (p22 (f11 c_2) c15) (not (p22 c_0 (f4 c8 c6))) (not (p12 (f23 c_2))) )(or (= (f21 (f7 (f3 c_2 c6)) c_1) (f21 (f21 (f2 c_2) (f4 (f4 c5 c6) (f16 c_2))) c_1)) (p12 (f17 c_2)) (p12 (f24 c_2)) (not (p22 c15 c_1)) (p22 (f11 c_2) c15) (not (p22 c_1 (f4 c8 c6))) (not (p12 (f23 c_2))) )(or (= (f21 (f7 (f3 c_2 c6)) c_2) (f21 (f21 (f2 c_2) (f4 (f4 c5 c6) (f16 c_2))) c_2)) (p12 (f17 c_2)) (p12 (f24 c_2)) (not (p22 c15 c_2)) (p22 (f11 c_2) c15) (not (p22 c_2 (f4 c8 c6))) (not (p12 (f23 c_2))) )(not (p12 (f23 c49))) (or (not (p12 (f23 c_0))) (p12 (f17 c_0)) (not (p12 (f24 c_0))) (= (f16 (f3 c_0 c6)) (f25 (f3 (f16 c_0) c6) c5)) (p22 (f11 c_0) c15) )(or (not (p12 (f23 c_1))) (p12 (f17 c_1)) (not (p12 (f24 c_1))) (= (f16 (f3 c_1 c6)) (f25 (f3 (f16 c_1) c6) c5)) (p22 (f11 c_1) c15) )(or (not (p12 (f23 c_2))) (p12 (f17 c_2)) (not (p12 (f24 c_2))) (= (f16 (f3 c_2 c6)) (f25 (f3 (f16 c_2) c6) c5)) (p22 (f11 c_2) c15) )(or (p12 (f17 c_0)) (p12 (f19 c_0)) (not (p12 (f19 (f3 c_0 c6)))) (p12 (f24 c_0)) )(or (p12 (f17 c_1)) (p12 (f19 c_1)) (not (p12 (f19 (f3 c_1 c6)))) (p12 (f24 c_1)) )(or (p12 (f17 c_2)) (p12 (f19 c_2)) (not (p12 (f19 (f3 c_2 c6)))) (p12 (f24 c_2)) )(or (not (p12 (f24 c_0))) (not (p12 (f23 c_0))) (= (f11 (f3 c_0 c6)) (f11 c_0)) (p22 (f11 c_0) c15) (p12 (f17 c_0)) )(or (not (p12 (f24 c_1))) (not (p12 (f23 c_1))) (= (f11 (f3 c_1 c6)) (f11 c_1)) (p22 (f11 c_1) c15) (p12 (f17 c_1)) )(or (not (p12 (f24 c_2))) (not (p12 (f23 c_2))) (= (f11 (f3 c_2 c6)) (f11 c_2)) (p22 (f11 c_2) c15) (p12 (f17 c_2)) )(or (p12 c_0) (p12 (f40 c_0)) )(or (p12 c_1) (p12 (f40 c_1)) )(or (p12 c_2) (p12 (f40 c_2)) )(or (not (p12 c_0)) (not (p12 c_0)) (not (p12 (f37 c_0 c_0))) )(or (not (p12 c_0)) (not (p12 c_1)) (not (p12 (f37 c_1 c_0))) )(or (not (p12 c_0)) (not (p12 c_2)) (not (p12 (f37 c_2 c_0))) )(or (not (p12 c_1)) (not (p12 c_0)) (not (p12 (f37 c_0 c_1))) )(or (not (p12 c_1)) (not (p12 c_1)) (not (p12 (f37 c_1 c_1))) )(or (not (p12 c_1)) (not (p12 c_2)) (not (p12 (f37 c_2 c_1))) )(or (not (p12 c_2)) (not (p12 c_0)) (not (p12 (f37 c_0 c_2))) )(or (not (p12 c_2)) (not (p12 c_1)) (not (p12 (f37 c_1 c_2))) )(or (not (p12 c_2)) (not (p12 c_2)) (not (p12 (f37 c_2 c_2))) )(= (f21 (f34 c_0 c_0) c_0) (f34 (f21 c_0 c_0) (f21 c_0 c_0))) (= (f21 (f34 c_0 c_0) c_1) (f34 (f21 c_0 c_1) (f21 c_0 c_1))) (= (f21 (f34 c_0 c_0) c_2) (f34 (f21 c_0 c_2) (f21 c_0 c_2))) (= (f21 (f34 c_0 c_1) c_0) (f34 (f21 c_0 c_0) (f21 c_1 c_0))) (= (f21 (f34 c_0 c_1) c_1) (f34 (f21 c_0 c_1) (f21 c_1 c_1))) (= (f21 (f34 c_0 c_1) c_2) (f34 (f21 c_0 c_2) (f21 c_1 c_2))) (= (f21 (f34 c_0 c_2) c_0) (f34 (f21 c_0 c_0) (f21 c_2 c_0))) (= (f21 (f34 c_0 c_2) c_1) (f34 (f21 c_0 c_1) (f21 c_2 c_1))) (= (f21 (f34 c_0 c_2) c_2) (f34 (f21 c_0 c_2) (f21 c_2 c_2))) (= (f21 (f34 c_1 c_0) c_0) (f34 (f21 c_1 c_0) (f21 c_0 c_0))) (= (f21 (f34 c_1 c_0) c_1) (f34 (f21 c_1 c_1) (f21 c_0 c_1))) (= (f21 (f34 c_1 c_0) c_2) (f34 (f21 c_1 c_2) (f21 c_0 c_2))) (= (f21 (f34 c_1 c_1) c_0) (f34 (f21 c_1 c_0) (f21 c_1 c_0))) (= (f21 (f34 c_1 c_1) c_1) (f34 (f21 c_1 c_1) (f21 c_1 c_1))) (= (f21 (f34 c_1 c_1) c_2) (f34 (f21 c_1 c_2) (f21 c_1 c_2))) (= (f21 (f34 c_1 c_2) c_0) (f34 (f21 c_1 c_0) (f21 c_2 c_0))) (= (f21 (f34 c_1 c_2) c_1) (f34 (f21 c_1 c_1) (f21 c_2 c_1))) (= (f21 (f34 c_1 c_2) c_2) (f34 (f21 c_1 c_2) (f21 c_2 c_2))) (= (f21 (f34 c_2 c_0) c_0) (f34 (f21 c_2 c_0) (f21 c_0 c_0))) (= (f21 (f34 c_2 c_0) c_1) (f34 (f21 c_2 c_1) (f21 c_0 c_1))) (= (f21 (f34 c_2 c_0) c_2) (f34 (f21 c_2 c_2) (f21 c_0 c_2))) (= (f21 (f34 c_2 c_1) c_0) (f34 (f21 c_2 c_0) (f21 c_1 c_0))) (= (f21 (f34 c_2 c_1) c_1) (f34 (f21 c_2 c_1) (f21 c_1 c_1))) (= (f21 (f34 c_2 c_1) c_2) (f34 (f21 c_2 c_2) (f21 c_1 c_2))) (= (f21 (f34 c_2 c_2) c_0) (f34 (f21 c_2 c_0) (f21 c_2 c_0))) (= (f21 (f34 c_2 c_2) c_1) (f34 (f21 c_2 c_1) (f21 c_2 c_1))) (= (f21 (f34 c_2 c_2) c_2) (f34 (f21 c_2 c_2) (f21 c_2 c_2))) (or (not (p22 c15 c_0)) (not (p22 c_0 (f4 c8 c6))) (not (p12 (f23 c_0))) (p12 (f17 c_0)) (= (f21 (f21 (f2 (f3 c_0 c6)) (f4 (f4 c5 c6) (f18 c_0))) c_0) (f21 (f9 c_0) c_0)) (not (p12 (f24 c_0))) )(or (not (p22 c15 c_0)) (not (p22 c_0 (f4 c8 c6))) (not (p12 (f23 c_1))) (p12 (f17 c_1)) (= (f21 (f21 (f2 (f3 c_1 c6)) (f4 (f4 c5 c6) (f18 c_1))) c_0) (f21 (f9 c_1) c_0)) (not (p12 (f24 c_1))) )(or (not (p22 c15 c_0)) (not (p22 c_0 (f4 c8 c6))) (not (p12 (f23 c_2))) (p12 (f17 c_2)) (= (f21 (f21 (f2 (f3 c_2 c6)) (f4 (f4 c5 c6) (f18 c_2))) c_0) (f21 (f9 c_2) c_0)) (not (p12 (f24 c_2))) )(or (not (p22 c15 c_1)) (not (p22 c_1 (f4 c8 c6))) (not (p12 (f23 c_0))) (p12 (f17 c_0)) (= (f21 (f21 (f2 (f3 c_0 c6)) (f4 (f4 c5 c6) (f18 c_0))) c_1) (f21 (f9 c_0) c_1)) (not (p12 (f24 c_0))) )(or (not (p22 c15 c_1)) (not (p22 c_1 (f4 c8 c6))) (not (p12 (f23 c_1))) (p12 (f17 c_1)) (= (f21 (f21 (f2 (f3 c_1 c6)) (f4 (f4 c5 c6) (f18 c_1))) c_1) (f21 (f9 c_1) c_1)) (not (p12 (f24 c_1))) )(or (not (p22 c15 c_1)) (not (p22 c_1 (f4 c8 c6))) (not (p12 (f23 c_2))) (p12 (f17 c_2)) (= (f21 (f21 (f2 (f3 c_2 c6)) (f4 (f4 c5 c6) (f18 c_2))) c_1) (f21 (f9 c_2) c_1)) (not (p12 (f24 c_2))) )(or (not (p22 c15 c_2)) (not (p22 c_2 (f4 c8 c6))) (not (p12 (f23 c_0))) (p12 (f17 c_0)) (= (f21 (f21 (f2 (f3 c_0 c6)) (f4 (f4 c5 c6) (f18 c_0))) c_2) (f21 (f9 c_0) c_2)) (not (p12 (f24 c_0))) )(or (not (p22 c15 c_2)) (not (p22 c_2 (f4 c8 c6))) (not (p12 (f23 c_1))) (p12 (f17 c_1)) (= (f21 (f21 (f2 (f3 c_1 c6)) (f4 (f4 c5 c6) (f18 c_1))) c_2) (f21 (f9 c_1) c_2)) (not (p12 (f24 c_1))) )(or (not (p22 c15 c_2)) (not (p22 c_2 (f4 c8 c6))) (not (p12 (f23 c_2))) (p12 (f17 c_2)) (= (f21 (f21 (f2 (f3 c_2 c6)) (f4 (f4 c5 c6) (f18 c_2))) c_2) (f21 (f9 c_2) c_2)) (not (p12 (f24 c_2))) )(or (not (p26 c_0 c_0)) (not (= c_0 c_0)) )(or (not (p26 c_0 c_1)) (not (= c_1 c_0)) )(or (not (p26 c_0 c_2)) (not (= c_2 c_0)) )(or (not (p26 c_1 c_0)) (not (= c_0 c_1)) )(or (not (p26 c_1 c_1)) (not (= c_1 c_1)) )(or (not (p26 c_1 c_2)) (not (= c_2 c_1)) )(or (not (p26 c_2 c_0)) (not (= c_0 c_2)) )(or (not (p26 c_2 c_1)) (not (= c_1 c_2)) )(or (not (p26 c_2 c_2)) (not (= c_2 c_2)) )(or (p12 (f17 c_0)) (p12 (f24 c_0)) (p12 (f23 c_0)) (= (f11 (f3 c_0 c6)) (f11 c_0)) )(or (p12 (f17 c_1)) (p12 (f24 c_1)) (p12 (f23 c_1)) (= (f11 (f3 c_1 c6)) (f11 c_1)) )(or (p12 (f17 c_2)) (p12 (f24 c_2)) (p12 (f23 c_2)) (= (f11 (f3 c_2 c6)) (f11 c_2)) )(or (not (p22 c15 c_0)) (p12 (f17 c_0)) (not (p22 c_0 (f4 c8 c6))) (= (f21 (f21 (f2 (f3 c_0 c6)) c_0) c_0) (f21 (f21 (f2 c_0) c_0) c_0)) (not (p22 c15 c_0)) (p12 (f24 c_0)) (not (p22 c_0 (f4 c5 c6))) )(or (not (p22 c15 c_0)) (p12 (f17 c_0)) (not (p22 c_1 (f4 c8 c6))) (= (f21 (f21 (f2 (f3 c_0 c6)) c_0) c_1) (f21 (f21 (f2 c_0) c_0) c_1)) (not (p22 c15 c_1)) (p12 (f24 c_0)) (not (p22 c_0 (f4 c5 c6))) )(or (not (p22 c15 c_0)) (p12 (f17 c_0)) (not (p22 c_2 (f4 c8 c6))) (= (f21 (f21 (f2 (f3 c_0 c6)) c_0) c_2) (f21 (f21 (f2 c_0) c_0) c_2)) (not (p22 c15 c_2)) (p12 (f24 c_0)) (not (p22 c_0 (f4 c5 c6))) )(or (not (p22 c15 c_0)) (p12 (f17 c_1)) (not (p22 c_0 (f4 c8 c6))) (= (f21 (f21 (f2 (f3 c_1 c6)) c_0) c_0) (f21 (f21 (f2 c_1) c_0) c_0)) (not (p22 c15 c_0)) (p12 (f24 c_1)) (not (p22 c_0 (f4 c5 c6))) )(or (not (p22 c15 c_0)) (p12 (f17 c_1)) (not (p22 c_1 (f4 c8 c6))) (= (f21 (f21 (f2 (f3 c_1 c6)) c_0) c_1) (f21 (f21 (f2 c_1) c_0) c_1)) (not (p22 c15 c_1)) (p12 (f24 c_1)) (not (p22 c_0 (f4 c5 c6))) )(or (not (p22 c15 c_0)) (p12 (f17 c_1)) (not (p22 c_2 (f4 c8 c6))) (= (f21 (f21 (f2 (f3 c_1 c6)) c_0) c_2) (f21 (f21 (f2 c_1) c_0) c_2)) (not (p22 c15 c_2)) (p12 (f24 c_1)) (not (p22 c_0 (f4 c5 c6))) )(or (not (p22 c15 c_0)) (p12 (f17 c_2)) (not (p22 c_0 (f4 c8 c6))) (= (f21 (f21 (f2 (f3 c_2 c6)) c_0) c_0) (f21 (f21 (f2 c_2) c_0) c_0)) (not (p22 c15 c_0)) (p12 (f24 c_2)) (not (p22 c_0 (f4 c5 c6))) )(or (not (p22 c15 c_0)) (p12 (f17 c_2)) (not (p22 c_1 (f4 c8 c6))) (= (f21 (f21 (f2 (f3 c_2 c6)) c_0) c_1) (f21 (f21 (f2 c_2) c_0) c_1)) (not (p22 c15 c_1)) (p12 (f24 c_2)) (not (p22 c_0 (f4 c5 c6))) )(or (not (p22 c15 c_0)) (p12 (f17 c_2)) (not (p22 c_2 (f4 c8 c6))) (= (f21 (f21 (f2 (f3 c_2 c6)) c_0) c_2) (f21 (f21 (f2 c_2) c_0) c_2)) (not (p22 c15 c_2)) (p12 (f24 c_2)) (not (p22 c_0 (f4 c5 c6))) )(or (not (p22 c15 c_1)) (p12 (f17 c_0)) (not (p22 c_0 (f4 c8 c6))) (= (f21 (f21 (f2 (f3 c_0 c6)) c_1) c_0) (f21 (f21 (f2 c_0) c_1) c_0)) (not (p22 c15 c_0)) (p12 (f24 c_0)) (not (p22 c_1 (f4 c5 c6))) )(or (not (p22 c15 c_1)) (p12 (f17 c_0)) (not (p22 c_1 (f4 c8 c6))) (= (f21 (f21 (f2 (f3 c_0 c6)) c_1) c_1) (f21 (f21 (f2 c_0) c_1) c_1)) (not (p22 c15 c_1)) (p12 (f24 c_0)) (not (p22 c_1 (f4 c5 c6))) )(or (not (p22 c15 c_1)) (p12 (f17 c_0)) (not (p22 c_2 (f4 c8 c6))) (= (f21 (f21 (f2 (f3 c_0 c6)) c_1) c_2) (f21 (f21 (f2 c_0) c_1) c_2)) (not (p22 c15 c_2)) (p12 (f24 c_0)) (not (p22 c_1 (f4 c5 c6))) )(or (not (p22 c15 c_1)) (p12 (f17 c_1)) (not (p22 c_0 (f4 c8 c6))) (= (f21 (f21 (f2 (f3 c_1 c6)) c_1) c_0) (f21 (f21 (f2 c_1) c_1) c_0)) (not (p22 c15 c_0)) (p12 (f24 c_1)) (not (p22 c_1 (f4 c5 c6))) )(or (not (p22 c15 c_1)) (p12 (f17 c_1)) (not (p22 c_1 (f4 c8 c6))) (= (f21 (f21 (f2 (f3 c_1 c6)) c_1) c_1) (f21 (f21 (f2 c_1) c_1) c_1)) (not (p22 c15 c_1)) (p12 (f24 c_1)) (not (p22 c_1 (f4 c5 c6))) )(or (not (p22 c15 c_1)) (p12 (f17 c_1)) (not (p22 c_2 (f4 c8 c6))) (= (f21 (f21 (f2 (f3 c_1 c6)) c_1) c_2) (f21 (f21 (f2 c_1) c_1) c_2)) (not (p22 c15 c_2)) (p12 (f24 c_1)) (not (p22 c_1 (f4 c5 c6))) )(or (not (p22 c15 c_1)) (p12 (f17 c_2)) (not (p22 c_0 (f4 c8 c6))) (= (f21 (f21 (f2 (f3 c_2 c6)) c_1) c_0) (f21 (f21 (f2 c_2) c_1) c_0)) (not (p22 c15 c_0)) (p12 (f24 c_2)) (not (p22 c_1 (f4 c5 c6))) )(or (not (p22 c15 c_1)) (p12 (f17 c_2)) (not (p22 c_1 (f4 c8 c6))) (= (f21 (f21 (f2 (f3 c_2 c6)) c_1) c_1) (f21 (f21 (f2 c_2) c_1) c_1)) (not (p22 c15 c_1)) (p12 (f24 c_2)) (not (p22 c_1 (f4 c5 c6))) )(or (not (p22 c15 c_1)) (p12 (f17 c_2)) (not (p22 c_2 (f4 c8 c6))) (= (f21 (f21 (f2 (f3 c_2 c6)) c_1) c_2) (f21 (f21 (f2 c_2) c_1) c_2)) (not (p22 c15 c_2)) (p12 (f24 c_2)) (not (p22 c_1 (f4 c5 c6))) )(or (not (p22 c15 c_2)) (p12 (f17 c_0)) (not (p22 c_0 (f4 c8 c6))) (= (f21 (f21 (f2 (f3 c_0 c6)) c_2) c_0) (f21 (f21 (f2 c_0) c_2) c_0)) (not (p22 c15 c_0)) (p12 (f24 c_0)) (not (p22 c_2 (f4 c5 c6))) )(or (not (p22 c15 c_2)) (p12 (f17 c_0)) (not (p22 c_1 (f4 c8 c6))) (= (f21 (f21 (f2 (f3 c_0 c6)) c_2) c_1) (f21 (f21 (f2 c_0) c_2) c_1)) (not (p22 c15 c_1)) (p12 (f24 c_0)) (not (p22 c_2 (f4 c5 c6))) )(or (not (p22 c15 c_2)) (p12 (f17 c_0)) (not (p22 c_2 (f4 c8 c6))) (= (f21 (f21 (f2 (f3 c_0 c6)) c_2) c_2) (f21 (f21 (f2 c_0) c_2) c_2)) (not (p22 c15 c_2)) (p12 (f24 c_0)) (not (p22 c_2 (f4 c5 c6))) )(or (not (p22 c15 c_2)) (p12 (f17 c_1)) (not (p22 c_0 (f4 c8 c6))) (= (f21 (f21 (f2 (f3 c_1 c6)) c_2) c_0) (f21 (f21 (f2 c_1) c_2) c_0)) (not (p22 c15 c_0)) (p12 (f24 c_1)) (not (p22 c_2 (f4 c5 c6))) )(or (not (p22 c15 c_2)) (p12 (f17 c_1)) (not (p22 c_1 (f4 c8 c6))) (= (f21 (f21 (f2 (f3 c_1 c6)) c_2) c_1) (f21 (f21 (f2 c_1) c_2) c_1)) (not (p22 c15 c_1)) (p12 (f24 c_1)) (not (p22 c_2 (f4 c5 c6))) )(or (not (p22 c15 c_2)) (p12 (f17 c_1)) (not (p22 c_2 (f4 c8 c6))) (= (f21 (f21 (f2 (f3 c_1 c6)) c_2) c_2) (f21 (f21 (f2 c_1) c_2) c_2)) (not (p22 c15 c_2)) (p12 (f24 c_1)) (not (p22 c_2 (f4 c5 c6))) )(or (not (p22 c15 c_2)) (p12 (f17 c_2)) (not (p22 c_0 (f4 c8 c6))) (= (f21 (f21 (f2 (f3 c_2 c6)) c_2) c_0) (f21 (f21 (f2 c_2) c_2) c_0)) (not (p22 c15 c_0)) (p12 (f24 c_2)) (not (p22 c_2 (f4 c5 c6))) )(or (not (p22 c15 c_2)) (p12 (f17 c_2)) (not (p22 c_1 (f4 c8 c6))) (= (f21 (f21 (f2 (f3 c_2 c6)) c_2) c_1) (f21 (f21 (f2 c_2) c_2) c_1)) (not (p22 c15 c_1)) (p12 (f24 c_2)) (not (p22 c_2 (f4 c5 c6))) )(or (not (p22 c15 c_2)) (p12 (f17 c_2)) (not (p22 c_2 (f4 c8 c6))) (= (f21 (f21 (f2 (f3 c_2 c6)) c_2) c_2) (f21 (f21 (f2 c_2) c_2) c_2)) (not (p22 c15 c_2)) (p12 (f24 c_2)) (not (p22 c_2 (f4 c5 c6))) )(or (p12 (f17 c_0)) (not (p12 (f23 c_0))) (not (p12 (f24 c_0))) (not (p22 (f11 c_0) c15)) (= (f11 (f3 c_0 c6)) (f3 (f11 c_0) c6)) )(or (p12 (f17 c_1)) (not (p12 (f23 c_1))) (not (p12 (f24 c_1))) (not (p22 (f11 c_1) c15)) (= (f11 (f3 c_1 c6)) (f3 (f11 c_1) c6)) )(or (p12 (f17 c_2)) (not (p12 (f23 c_2))) (not (p12 (f24 c_2))) (not (p22 (f11 c_2) c15)) (= (f11 (f3 c_2 c6)) (f3 (f11 c_2) c6)) )(or (not (p12 (f36 c_0 c_0))) (p12 c_0) (p12 c_0) )(or (not (p12 (f36 c_0 c_1))) (p12 c_0) (p12 c_1) )(or (not (p12 (f36 c_0 c_2))) (p12 c_0) (p12 c_2) )(or (not (p12 (f36 c_1 c_0))) (p12 c_1) (p12 c_0) )(or (not (p12 (f36 c_1 c_1))) (p12 c_1) (p12 c_1) )(or (not (p12 (f36 c_1 c_2))) (p12 c_1) (p12 c_2) )(or (not (p12 (f36 c_2 c_0))) (p12 c_2) (p12 c_0) )(or (not (p12 (f36 c_2 c_1))) (p12 c_2) (p12 c_1) )(or (not (p12 (f36 c_2 c_2))) (p12 c_2) (p12 c_2) )(or (= (f18 (f3 c_0 c6)) (f18 c_0)) (not (p22 c5 (f11 c_0))) (p12 (f17 c_0)) (p12 (f23 c_0)) (not (p12 (f24 c_0))) )(or (= (f18 (f3 c_1 c6)) (f18 c_1)) (not (p22 c5 (f11 c_1))) (p12 (f17 c_1)) (p12 (f23 c_1)) (not (p12 (f24 c_1))) )(or (= (f18 (f3 c_2 c6)) (f18 c_2)) (not (p22 c5 (f11 c_2))) (p12 (f17 c_2)) (p12 (f23 c_2)) (not (p12 (f24 c_2))) )(or (= c_0 c_0) (not (p22 c_0 c_0)) (not (p22 c_0 c_0)) )(or (= c_0 c_1) (not (p22 c_1 c_0)) (not (p22 c_0 c_1)) )(or (= c_0 c_2) (not (p22 c_2 c_0)) (not (p22 c_0 c_2)) )(or (= c_1 c_0) (not (p22 c_0 c_1)) (not (p22 c_1 c_0)) )(or (= c_1 c_1) (not (p22 c_1 c_1)) (not (p22 c_1 c_1)) )(or (= c_1 c_2) (not (p22 c_2 c_1)) (not (p22 c_1 c_2)) )(or (= c_2 c_0) (not (p22 c_0 c_2)) (not (p22 c_2 c_0)) )(or (= c_2 c_1) (not (p22 c_1 c_2)) (not (p22 c_2 c_1)) )(or (= c_2 c_2) (not (p22 c_2 c_2)) (not (p22 c_2 c_2)) )(= c6 (f3 c15 c6)) (or (p12 c_0) (not (p12 (f35 c_0 c_0))) (p12 c_0) )(or (p12 c_0) (not (p12 (f35 c_0 c_1))) (p12 c_1) )(or (p12 c_0) (not (p12 (f35 c_0 c_2))) (p12 c_2) )(or (p12 c_1) (not (p12 (f35 c_1 c_0))) (p12 c_0) )(or (p12 c_1) (not (p12 (f35 c_1 c_1))) (p12 c_1) )(or (p12 c_1) (not (p12 (f35 c_1 c_2))) (p12 c_2) )(or (p12 c_2) (not (p12 (f35 c_2 c_0))) (p12 c_0) )(or (p12 c_2) (not (p12 (f35 c_2 c_1))) (p12 c_1) )(or (p12 c_2) (not (p12 (f35 c_2 c_2))) (p12 c_2) )(= (f21 (f31 c_0 c_0 c_0) c_0) (f21 c_0 (f3 c_0 c_0))) (= (f21 (f31 c_0 c_0 c_0) c_1) (f21 c_0 (f3 c_1 c_0))) (= (f21 (f31 c_0 c_0 c_0) c_2) (f21 c_0 (f3 c_2 c_0))) (= (f21 (f31 c_0 c_0 c_1) c_0) (f21 c_0 (f3 c_0 c_0))) (= (f21 (f31 c_0 c_0 c_1) c_1) (f21 c_0 (f3 c_1 c_0))) (= (f21 (f31 c_0 c_0 c_1) c_2) (f21 c_0 (f3 c_2 c_0))) (= (f21 (f31 c_0 c_0 c_2) c_0) (f21 c_0 (f3 c_0 c_0))) (= (f21 (f31 c_0 c_0 c_2) c_1) (f21 c_0 (f3 c_1 c_0))) (= (f21 (f31 c_0 c_0 c_2) c_2) (f21 c_0 (f3 c_2 c_0))) (= (f21 (f31 c_0 c_1 c_0) c_0) (f21 c_0 (f3 c_0 c_1))) (= (f21 (f31 c_0 c_1 c_0) c_1) (f21 c_0 (f3 c_1 c_1))) (= (f21 (f31 c_0 c_1 c_0) c_2) (f21 c_0 (f3 c_2 c_1))) (= (f21 (f31 c_0 c_1 c_1) c_0) (f21 c_0 (f3 c_0 c_1))) (= (f21 (f31 c_0 c_1 c_1) c_1) (f21 c_0 (f3 c_1 c_1))) (= (f21 (f31 c_0 c_1 c_1) c_2) (f21 c_0 (f3 c_2 c_1))) (= (f21 (f31 c_0 c_1 c_2) c_0) (f21 c_0 (f3 c_0 c_1))) (= (f21 (f31 c_0 c_1 c_2) c_1) (f21 c_0 (f3 c_1 c_1))) (= (f21 (f31 c_0 c_1 c_2) c_2) (f21 c_0 (f3 c_2 c_1))) (= (f21 (f31 c_0 c_2 c_0) c_0) (f21 c_0 (f3 c_0 c_2))) (= (f21 (f31 c_0 c_2 c_0) c_1) (f21 c_0 (f3 c_1 c_2))) (= (f21 (f31 c_0 c_2 c_0) c_2) (f21 c_0 (f3 c_2 c_2))) (= (f21 (f31 c_0 c_2 c_1) c_0) (f21 c_0 (f3 c_0 c_2))) (= (f21 (f31 c_0 c_2 c_1) c_1) (f21 c_0 (f3 c_1 c_2))) (= (f21 (f31 c_0 c_2 c_1) c_2) (f21 c_0 (f3 c_2 c_2))) (= (f21 (f31 c_0 c_2 c_2) c_0) (f21 c_0 (f3 c_0 c_2))) (= (f21 (f31 c_0 c_2 c_2) c_1) (f21 c_0 (f3 c_1 c_2))) (= (f21 (f31 c_0 c_2 c_2) c_2) (f21 c_0 (f3 c_2 c_2))) (= (f21 (f31 c_1 c_0 c_0) c_0) (f21 c_1 (f3 c_0 c_0))) (= (f21 (f31 c_1 c_0 c_0) c_1) (f21 c_1 (f3 c_1 c_0))) (= (f21 (f31 c_1 c_0 c_0) c_2) (f21 c_1 (f3 c_2 c_0))) (= (f21 (f31 c_1 c_0 c_1) c_0) (f21 c_1 (f3 c_0 c_0))) (= (f21 (f31 c_1 c_0 c_1) c_1) (f21 c_1 (f3 c_1 c_0))) (= (f21 (f31 c_1 c_0 c_1) c_2) (f21 c_1 (f3 c_2 c_0))) (= (f21 (f31 c_1 c_0 c_2) c_0) (f21 c_1 (f3 c_0 c_0))) (= (f21 (f31 c_1 c_0 c_2) c_1) (f21 c_1 (f3 c_1 c_0))) (= (f21 (f31 c_1 c_0 c_2) c_2) (f21 c_1 (f3 c_2 c_0))) (= (f21 (f31 c_1 c_1 c_0) c_0) (f21 c_1 (f3 c_0 c_1))) (= (f21 (f31 c_1 c_1 c_0) c_1) (f21 c_1 (f3 c_1 c_1))) (= (f21 (f31 c_1 c_1 c_0) c_2) (f21 c_1 (f3 c_2 c_1))) (= (f21 (f31 c_1 c_1 c_1) c_0) (f21 c_1 (f3 c_0 c_1))) (= (f21 (f31 c_1 c_1 c_1) c_1) (f21 c_1 (f3 c_1 c_1))) (= (f21 (f31 c_1 c_1 c_1) c_2) (f21 c_1 (f3 c_2 c_1))) (= (f21 (f31 c_1 c_1 c_2) c_0) (f21 c_1 (f3 c_0 c_1))) (= (f21 (f31 c_1 c_1 c_2) c_1) (f21 c_1 (f3 c_1 c_1))) (= (f21 (f31 c_1 c_1 c_2) c_2) (f21 c_1 (f3 c_2 c_1))) (= (f21 (f31 c_1 c_2 c_0) c_0) (f21 c_1 (f3 c_0 c_2))) (= (f21 (f31 c_1 c_2 c_0) c_1) (f21 c_1 (f3 c_1 c_2))) (= (f21 (f31 c_1 c_2 c_0) c_2) (f21 c_1 (f3 c_2 c_2))) (= (f21 (f31 c_1 c_2 c_1) c_0) (f21 c_1 (f3 c_0 c_2))) (= (f21 (f31 c_1 c_2 c_1) c_1) (f21 c_1 (f3 c_1 c_2))) (= (f21 (f31 c_1 c_2 c_1) c_2) (f21 c_1 (f3 c_2 c_2))) (= (f21 (f31 c_1 c_2 c_2) c_0) (f21 c_1 (f3 c_0 c_2))) (= (f21 (f31 c_1 c_2 c_2) c_1) (f21 c_1 (f3 c_1 c_2))) (= (f21 (f31 c_1 c_2 c_2) c_2) (f21 c_1 (f3 c_2 c_2))) (= (f21 (f31 c_2 c_0 c_0) c_0) (f21 c_2 (f3 c_0 c_0))) (= (f21 (f31 c_2 c_0 c_0) c_1) (f21 c_2 (f3 c_1 c_0))) (= (f21 (f31 c_2 c_0 c_0) c_2) (f21 c_2 (f3 c_2 c_0))) (= (f21 (f31 c_2 c_0 c_1) c_0) (f21 c_2 (f3 c_0 c_0))) (= (f21 (f31 c_2 c_0 c_1) c_1) (f21 c_2 (f3 c_1 c_0))) (= (f21 (f31 c_2 c_0 c_1) c_2) (f21 c_2 (f3 c_2 c_0))) (= (f21 (f31 c_2 c_0 c_2) c_0) (f21 c_2 (f3 c_0 c_0))) (= (f21 (f31 c_2 c_0 c_2) c_1) (f21 c_2 (f3 c_1 c_0))) (= (f21 (f31 c_2 c_0 c_2) c_2) (f21 c_2 (f3 c_2 c_0))) (= (f21 (f31 c_2 c_1 c_0) c_0) (f21 c_2 (f3 c_0 c_1))) (= (f21 (f31 c_2 c_1 c_0) c_1) (f21 c_2 (f3 c_1 c_1))) (= (f21 (f31 c_2 c_1 c_0) c_2) (f21 c_2 (f3 c_2 c_1))) (= (f21 (f31 c_2 c_1 c_1) c_0) (f21 c_2 (f3 c_0 c_1))) (= (f21 (f31 c_2 c_1 c_1) c_1) (f21 c_2 (f3 c_1 c_1))) (= (f21 (f31 c_2 c_1 c_1) c_2) (f21 c_2 (f3 c_2 c_1))) (= (f21 (f31 c_2 c_1 c_2) c_0) (f21 c_2 (f3 c_0 c_1))) (= (f21 (f31 c_2 c_1 c_2) c_1) (f21 c_2 (f3 c_1 c_1))) (= (f21 (f31 c_2 c_1 c_2) c_2) (f21 c_2 (f3 c_2 c_1))) (= (f21 (f31 c_2 c_2 c_0) c_0) (f21 c_2 (f3 c_0 c_2))) (= (f21 (f31 c_2 c_2 c_0) c_1) (f21 c_2 (f3 c_1 c_2))) (= (f21 (f31 c_2 c_2 c_0) c_2) (f21 c_2 (f3 c_2 c_2))) (= (f21 (f31 c_2 c_2 c_1) c_0) (f21 c_2 (f3 c_0 c_2))) (= (f21 (f31 c_2 c_2 c_1) c_1) (f21 c_2 (f3 c_1 c_2))) (= (f21 (f31 c_2 c_2 c_1) c_2) (f21 c_2 (f3 c_2 c_2))) (= (f21 (f31 c_2 c_2 c_2) c_0) (f21 c_2 (f3 c_0 c_2))) (= (f21 (f31 c_2 c_2 c_2) c_1) (f21 c_2 (f3 c_1 c_2))) (= (f21 (f31 c_2 c_2 c_2) c_2) (f21 c_2 (f3 c_2 c_2))) (or (not (= (f11 c_0) c15)) (p12 (f14 c_0)) )(or (not (= (f11 c_1) c15)) (p12 (f14 c_1)) )(or (not (= (f11 c_2) c15)) (p12 (f14 c_2)) )(or (not (p12 c_0)) (p12 c_0) (not (p12 (f39 c_0 c_0))) )(or (not (p12 c_0)) (p12 c_1) (not (p12 (f39 c_1 c_0))) )(or (not (p12 c_0)) (p12 c_2) (not (p12 (f39 c_2 c_0))) )(or (not (p12 c_1)) (p12 c_0) (not (p12 (f39 c_0 c_1))) )(or (not (p12 c_1)) (p12 c_1) (not (p12 (f39 c_1 c_1))) )(or (not (p12 c_1)) (p12 c_2) (not (p12 (f39 c_2 c_1))) )(or (not (p12 c_2)) (p12 c_0) (not (p12 (f39 c_0 c_2))) )(or (not (p12 c_2)) (p12 c_1) (not (p12 (f39 c_1 c_2))) )(or (not (p12 c_2)) (p12 c_2) (not (p12 (f39 c_2 c_2))) )(or (p12 (f43 c_0 c_0)) (not (p12 c_0)) (not (p12 c_0)) )(or (p12 (f43 c_0 c_1)) (not (p12 c_1)) (not (p12 c_0)) )(or (p12 (f43 c_0 c_2)) (not (p12 c_2)) (not (p12 c_0)) )(or (p12 (f43 c_1 c_0)) (not (p12 c_0)) (not (p12 c_1)) )(or (p12 (f43 c_1 c_1)) (not (p12 c_1)) (not (p12 c_1)) )(or (p12 (f43 c_1 c_2)) (not (p12 c_2)) (not (p12 c_1)) )(or (p12 (f43 c_2 c_0)) (not (p12 c_0)) (not (p12 c_2)) )(or (p12 (f43 c_2 c_1)) (not (p12 c_1)) (not (p12 c_2)) )(or (p12 (f43 c_2 c_2)) (not (p12 c_2)) (not (p12 c_2)) )(= (f21 (f37 c_0 c_0) c_0) (f37 (f21 c_0 c_0) (f21 c_0 c_0))) (= (f21 (f37 c_0 c_0) c_1) (f37 (f21 c_0 c_1) (f21 c_0 c_1))) (= (f21 (f37 c_0 c_0) c_2) (f37 (f21 c_0 c_2) (f21 c_0 c_2))) (= (f21 (f37 c_0 c_1) c_0) (f37 (f21 c_0 c_0) (f21 c_1 c_0))) (= (f21 (f37 c_0 c_1) c_1) (f37 (f21 c_0 c_1) (f21 c_1 c_1))) (= (f21 (f37 c_0 c_1) c_2) (f37 (f21 c_0 c_2) (f21 c_1 c_2))) (= (f21 (f37 c_0 c_2) c_0) (f37 (f21 c_0 c_0) (f21 c_2 c_0))) (= (f21 (f37 c_0 c_2) c_1) (f37 (f21 c_0 c_1) (f21 c_2 c_1))) (= (f21 (f37 c_0 c_2) c_2) (f37 (f21 c_0 c_2) (f21 c_2 c_2))) (= (f21 (f37 c_1 c_0) c_0) (f37 (f21 c_1 c_0) (f21 c_0 c_0))) (= (f21 (f37 c_1 c_0) c_1) (f37 (f21 c_1 c_1) (f21 c_0 c_1))) (= (f21 (f37 c_1 c_0) c_2) (f37 (f21 c_1 c_2) (f21 c_0 c_2))) (= (f21 (f37 c_1 c_1) c_0) (f37 (f21 c_1 c_0) (f21 c_1 c_0))) (= (f21 (f37 c_1 c_1) c_1) (f37 (f21 c_1 c_1) (f21 c_1 c_1))) (= (f21 (f37 c_1 c_1) c_2) (f37 (f21 c_1 c_2) (f21 c_1 c_2))) (= (f21 (f37 c_1 c_2) c_0) (f37 (f21 c_1 c_0) (f21 c_2 c_0))) (= (f21 (f37 c_1 c_2) c_1) (f37 (f21 c_1 c_1) (f21 c_2 c_1))) (= (f21 (f37 c_1 c_2) c_2) (f37 (f21 c_1 c_2) (f21 c_2 c_2))) (= (f21 (f37 c_2 c_0) c_0) (f37 (f21 c_2 c_0) (f21 c_0 c_0))) (= (f21 (f37 c_2 c_0) c_1) (f37 (f21 c_2 c_1) (f21 c_0 c_1))) (= (f21 (f37 c_2 c_0) c_2) (f37 (f21 c_2 c_2) (f21 c_0 c_2))) (= (f21 (f37 c_2 c_1) c_0) (f37 (f21 c_2 c_0) (f21 c_1 c_0))) (= (f21 (f37 c_2 c_1) c_1) (f37 (f21 c_2 c_1) (f21 c_1 c_1))) (= (f21 (f37 c_2 c_1) c_2) (f37 (f21 c_2 c_2) (f21 c_1 c_2))) (= (f21 (f37 c_2 c_2) c_0) (f37 (f21 c_2 c_0) (f21 c_2 c_0))) (= (f21 (f37 c_2 c_2) c_1) (f37 (f21 c_2 c_1) (f21 c_2 c_1))) (= (f21 (f37 c_2 c_2) c_2) (f37 (f21 c_2 c_2) (f21 c_2 c_2))) (or (not (p22 c15 c_0)) (p12 (f17 c_0)) (= c_0 (f4 (f4 c5 c6) (f18 c_0))) (not (p22 c15 c_0)) (not (p12 (f24 c_0))) (not (p22 c_0 (f4 c5 c6))) (not (p12 (f23 c_0))) (= (f21 (f21 (f2 (f3 c_0 c6)) c_0) c_0) (f21 (f21 (f2 c_0) c_0) c_0)) (not (p22 c_0 (f4 c8 c6))) )(or (not (p22 c15 c_0)) (p12 (f17 c_0)) (= c_0 (f4 (f4 c5 c6) (f18 c_0))) (not (p22 c15 c_1)) (not (p12 (f24 c_0))) (not (p22 c_0 (f4 c5 c6))) (not (p12 (f23 c_0))) (= (f21 (f21 (f2 (f3 c_0 c6)) c_0) c_1) (f21 (f21 (f2 c_0) c_0) c_1)) (not (p22 c_1 (f4 c8 c6))) )(or (not (p22 c15 c_0)) (p12 (f17 c_0)) (= c_0 (f4 (f4 c5 c6) (f18 c_0))) (not (p22 c15 c_2)) (not (p12 (f24 c_0))) (not (p22 c_0 (f4 c5 c6))) (not (p12 (f23 c_0))) (= (f21 (f21 (f2 (f3 c_0 c6)) c_0) c_2) (f21 (f21 (f2 c_0) c_0) c_2)) (not (p22 c_2 (f4 c8 c6))) )(or (not (p22 c15 c_0)) (p12 (f17 c_1)) (= c_0 (f4 (f4 c5 c6) (f18 c_1))) (not (p22 c15 c_0)) (not (p12 (f24 c_1))) (not (p22 c_0 (f4 c5 c6))) (not (p12 (f23 c_1))) (= (f21 (f21 (f2 (f3 c_1 c6)) c_0) c_0) (f21 (f21 (f2 c_1) c_0) c_0)) (not (p22 c_0 (f4 c8 c6))) )(or (not (p22 c15 c_0)) (p12 (f17 c_1)) (= c_0 (f4 (f4 c5 c6) (f18 c_1))) (not (p22 c15 c_1)) (not (p12 (f24 c_1))) (not (p22 c_0 (f4 c5 c6))) (not (p12 (f23 c_1))) (= (f21 (f21 (f2 (f3 c_1 c6)) c_0) c_1) (f21 (f21 (f2 c_1) c_0) c_1)) (not (p22 c_1 (f4 c8 c6))) )(or (not (p22 c15 c_0)) (p12 (f17 c_1)) (= c_0 (f4 (f4 c5 c6) (f18 c_1))) (not (p22 c15 c_2)) (not (p12 (f24 c_1))) (not (p22 c_0 (f4 c5 c6))) (not (p12 (f23 c_1))) (= (f21 (f21 (f2 (f3 c_1 c6)) c_0) c_2) (f21 (f21 (f2 c_1) c_0) c_2)) (not (p22 c_2 (f4 c8 c6))) )(or (not (p22 c15 c_0)) (p12 (f17 c_2)) (= c_0 (f4 (f4 c5 c6) (f18 c_2))) (not (p22 c15 c_0)) (not (p12 (f24 c_2))) (not (p22 c_0 (f4 c5 c6))) (not (p12 (f23 c_2))) (= (f21 (f21 (f2 (f3 c_2 c6)) c_0) c_0) (f21 (f21 (f2 c_2) c_0) c_0)) (not (p22 c_0 (f4 c8 c6))) )(or (not (p22 c15 c_0)) (p12 (f17 c_2)) (= c_0 (f4 (f4 c5 c6) (f18 c_2))) (not (p22 c15 c_1)) (not (p12 (f24 c_2))) (not (p22 c_0 (f4 c5 c6))) (not (p12 (f23 c_2))) (= (f21 (f21 (f2 (f3 c_2 c6)) c_0) c_1) (f21 (f21 (f2 c_2) c_0) c_1)) (not (p22 c_1 (f4 c8 c6))) )(or (not (p22 c15 c_0)) (p12 (f17 c_2)) (= c_0 (f4 (f4 c5 c6) (f18 c_2))) (not (p22 c15 c_2)) (not (p12 (f24 c_2))) (not (p22 c_0 (f4 c5 c6))) (not (p12 (f23 c_2))) (= (f21 (f21 (f2 (f3 c_2 c6)) c_0) c_2) (f21 (f21 (f2 c_2) c_0) c_2)) (not (p22 c_2 (f4 c8 c6))) )(or (not (p22 c15 c_1)) (p12 (f17 c_0)) (= c_1 (f4 (f4 c5 c6) (f18 c_0))) (not (p22 c15 c_0)) (not (p12 (f24 c_0))) (not (p22 c_1 (f4 c5 c6))) (not (p12 (f23 c_0))) (= (f21 (f21 (f2 (f3 c_0 c6)) c_1) c_0) (f21 (f21 (f2 c_0) c_1) c_0)) (not (p22 c_0 (f4 c8 c6))) )(or (not (p22 c15 c_1)) (p12 (f17 c_0)) (= c_1 (f4 (f4 c5 c6) (f18 c_0))) (not (p22 c15 c_1)) (not (p12 (f24 c_0))) (not (p22 c_1 (f4 c5 c6))) (not (p12 (f23 c_0))) (= (f21 (f21 (f2 (f3 c_0 c6)) c_1) c_1) (f21 (f21 (f2 c_0) c_1) c_1)) (not (p22 c_1 (f4 c8 c6))) )(or (not (p22 c15 c_1)) (p12 (f17 c_0)) (= c_1 (f4 (f4 c5 c6) (f18 c_0))) (not (p22 c15 c_2)) (not (p12 (f24 c_0))) (not (p22 c_1 (f4 c5 c6))) (not (p12 (f23 c_0))) (= (f21 (f21 (f2 (f3 c_0 c6)) c_1) c_2) (f21 (f21 (f2 c_0) c_1) c_2)) (not (p22 c_2 (f4 c8 c6))) )(or (not (p22 c15 c_1)) (p12 (f17 c_1)) (= c_1 (f4 (f4 c5 c6) (f18 c_1))) (not (p22 c15 c_0)) (not (p12 (f24 c_1))) (not (p22 c_1 (f4 c5 c6))) (not (p12 (f23 c_1))) (= (f21 (f21 (f2 (f3 c_1 c6)) c_1) c_0) (f21 (f21 (f2 c_1) c_1) c_0)) (not (p22 c_0 (f4 c8 c6))) )(or (not (p22 c15 c_1)) (p12 (f17 c_1)) (= c_1 (f4 (f4 c5 c6) (f18 c_1))) (not (p22 c15 c_1)) (not (p12 (f24 c_1))) (not (p22 c_1 (f4 c5 c6))) (not (p12 (f23 c_1))) (= (f21 (f21 (f2 (f3 c_1 c6)) c_1) c_1) (f21 (f21 (f2 c_1) c_1) c_1)) (not (p22 c_1 (f4 c8 c6))) )(or (not (p22 c15 c_1)) (p12 (f17 c_1)) (= c_1 (f4 (f4 c5 c6) (f18 c_1))) (not (p22 c15 c_2)) (not (p12 (f24 c_1))) (not (p22 c_1 (f4 c5 c6))) (not (p12 (f23 c_1))) (= (f21 (f21 (f2 (f3 c_1 c6)) c_1) c_2) (f21 (f21 (f2 c_1) c_1) c_2)) (not (p22 c_2 (f4 c8 c6))) )(or (not (p22 c15 c_1)) (p12 (f17 c_2)) (= c_1 (f4 (f4 c5 c6) (f18 c_2))) (not (p22 c15 c_0)) (not (p12 (f24 c_2))) (not (p22 c_1 (f4 c5 c6))) (not (p12 (f23 c_2))) (= (f21 (f21 (f2 (f3 c_2 c6)) c_1) c_0) (f21 (f21 (f2 c_2) c_1) c_0)) (not (p22 c_0 (f4 c8 c6))) )(or (not (p22 c15 c_1)) (p12 (f17 c_2)) (= c_1 (f4 (f4 c5 c6) (f18 c_2))) (not (p22 c15 c_1)) (not (p12 (f24 c_2))) (not (p22 c_1 (f4 c5 c6))) (not (p12 (f23 c_2))) (= (f21 (f21 (f2 (f3 c_2 c6)) c_1) c_1) (f21 (f21 (f2 c_2) c_1) c_1)) (not (p22 c_1 (f4 c8 c6))) )(or (not (p22 c15 c_1)) (p12 (f17 c_2)) (= c_1 (f4 (f4 c5 c6) (f18 c_2))) (not (p22 c15 c_2)) (not (p12 (f24 c_2))) (not (p22 c_1 (f4 c5 c6))) (not (p12 (f23 c_2))) (= (f21 (f21 (f2 (f3 c_2 c6)) c_1) c_2) (f21 (f21 (f2 c_2) c_1) c_2)) (not (p22 c_2 (f4 c8 c6))) )(or (not (p22 c15 c_2)) (p12 (f17 c_0)) (= c_2 (f4 (f4 c5 c6) (f18 c_0))) (not (p22 c15 c_0)) (not (p12 (f24 c_0))) (not (p22 c_2 (f4 c5 c6))) (not (p12 (f23 c_0))) (= (f21 (f21 (f2 (f3 c_0 c6)) c_2) c_0) (f21 (f21 (f2 c_0) c_2) c_0)) (not (p22 c_0 (f4 c8 c6))) )(or (not (p22 c15 c_2)) (p12 (f17 c_0)) (= c_2 (f4 (f4 c5 c6) (f18 c_0))) (not (p22 c15 c_1)) (not (p12 (f24 c_0))) (not (p22 c_2 (f4 c5 c6))) (not (p12 (f23 c_0))) (= (f21 (f21 (f2 (f3 c_0 c6)) c_2) c_1) (f21 (f21 (f2 c_0) c_2) c_1)) (not (p22 c_1 (f4 c8 c6))) )(or (not (p22 c15 c_2)) (p12 (f17 c_0)) (= c_2 (f4 (f4 c5 c6) (f18 c_0))) (not (p22 c15 c_2)) (not (p12 (f24 c_0))) (not (p22 c_2 (f4 c5 c6))) (not (p12 (f23 c_0))) (= (f21 (f21 (f2 (f3 c_0 c6)) c_2) c_2) (f21 (f21 (f2 c_0) c_2) c_2)) (not (p22 c_2 (f4 c8 c6))) )(or (not (p22 c15 c_2)) (p12 (f17 c_1)) (= c_2 (f4 (f4 c5 c6) (f18 c_1))) (not (p22 c15 c_0)) (not (p12 (f24 c_1))) (not (p22 c_2 (f4 c5 c6))) (not (p12 (f23 c_1))) (= (f21 (f21 (f2 (f3 c_1 c6)) c_2) c_0) (f21 (f21 (f2 c_1) c_2) c_0)) (not (p22 c_0 (f4 c8 c6))) )(or (not (p22 c15 c_2)) (p12 (f17 c_1)) (= c_2 (f4 (f4 c5 c6) (f18 c_1))) (not (p22 c15 c_1)) (not (p12 (f24 c_1))) (not (p22 c_2 (f4 c5 c6))) (not (p12 (f23 c_1))) (= (f21 (f21 (f2 (f3 c_1 c6)) c_2) c_1) (f21 (f21 (f2 c_1) c_2) c_1)) (not (p22 c_1 (f4 c8 c6))) )(or (not (p22 c15 c_2)) (p12 (f17 c_1)) (= c_2 (f4 (f4 c5 c6) (f18 c_1))) (not (p22 c15 c_2)) (not (p12 (f24 c_1))) (not (p22 c_2 (f4 c5 c6))) (not (p12 (f23 c_1))) (= (f21 (f21 (f2 (f3 c_1 c6)) c_2) c_2) (f21 (f21 (f2 c_1) c_2) c_2)) (not (p22 c_2 (f4 c8 c6))) )(or (not (p22 c15 c_2)) (p12 (f17 c_2)) (= c_2 (f4 (f4 c5 c6) (f18 c_2))) (not (p22 c15 c_0)) (not (p12 (f24 c_2))) (not (p22 c_2 (f4 c5 c6))) (not (p12 (f23 c_2))) (= (f21 (f21 (f2 (f3 c_2 c6)) c_2) c_0) (f21 (f21 (f2 c_2) c_2) c_0)) (not (p22 c_0 (f4 c8 c6))) )(or (not (p22 c15 c_2)) (p12 (f17 c_2)) (= c_2 (f4 (f4 c5 c6) (f18 c_2))) (not (p22 c15 c_1)) (not (p12 (f24 c_2))) (not (p22 c_2 (f4 c5 c6))) (not (p12 (f23 c_2))) (= (f21 (f21 (f2 (f3 c_2 c6)) c_2) c_1) (f21 (f21 (f2 c_2) c_2) c_1)) (not (p22 c_1 (f4 c8 c6))) )(or (not (p22 c15 c_2)) (p12 (f17 c_2)) (= c_2 (f4 (f4 c5 c6) (f18 c_2))) (not (p22 c15 c_2)) (not (p12 (f24 c_2))) (not (p22 c_2 (f4 c5 c6))) (not (p12 (f23 c_2))) (= (f21 (f21 (f2 (f3 c_2 c6)) c_2) c_2) (f21 (f21 (f2 c_2) c_2) c_2)) (not (p22 c_2 (f4 c8 c6))) )(or (p22 (f11 c_0) c15) (not (p12 (f23 c_0))) (not (p12 (f20 (f3 c_0 c6)))) (p12 (f17 c_0)) (p12 (f24 c_0)) )(or (p22 (f11 c_1) c15) (not (p12 (f23 c_1))) (not (p12 (f20 (f3 c_1 c6)))) (p12 (f17 c_1)) (p12 (f24 c_1)) )(or (p22 (f11 c_2) c15) (not (p12 (f23 c_2))) (not (p12 (f20 (f3 c_2 c6)))) (p12 (f17 c_2)) (p12 (f24 c_2)) )(or (p22 (f11 c_0) c15) (p12 (f17 c_0)) (not (p22 c15 c_0)) (= (f21 (f7 (f3 c_0 c6)) c_0) (f21 (f21 (f2 c_0) (f4 (f4 c5 c6) (f16 c_0))) c_0)) (not (p22 c_0 (f4 c8 c6))) (not (p12 (f24 c_0))) (not (p12 (f23 c_0))) )(or (p22 (f11 c_0) c15) (p12 (f17 c_0)) (not (p22 c15 c_1)) (= (f21 (f7 (f3 c_0 c6)) c_1) (f21 (f21 (f2 c_0) (f4 (f4 c5 c6) (f16 c_0))) c_1)) (not (p22 c_1 (f4 c8 c6))) (not (p12 (f24 c_0))) (not (p12 (f23 c_0))) )(or (p22 (f11 c_0) c15) (p12 (f17 c_0)) (not (p22 c15 c_2)) (= (f21 (f7 (f3 c_0 c6)) c_2) (f21 (f21 (f2 c_0) (f4 (f4 c5 c6) (f16 c_0))) c_2)) (not (p22 c_2 (f4 c8 c6))) (not (p12 (f24 c_0))) (not (p12 (f23 c_0))) )(or (p22 (f11 c_1) c15) (p12 (f17 c_1)) (not (p22 c15 c_0)) (= (f21 (f7 (f3 c_1 c6)) c_0) (f21 (f21 (f2 c_1) (f4 (f4 c5 c6) (f16 c_1))) c_0)) (not (p22 c_0 (f4 c8 c6))) (not (p12 (f24 c_1))) (not (p12 (f23 c_1))) )(or (p22 (f11 c_1) c15) (p12 (f17 c_1)) (not (p22 c15 c_1)) (= (f21 (f7 (f3 c_1 c6)) c_1) (f21 (f21 (f2 c_1) (f4 (f4 c5 c6) (f16 c_1))) c_1)) (not (p22 c_1 (f4 c8 c6))) (not (p12 (f24 c_1))) (not (p12 (f23 c_1))) )(or (p22 (f11 c_1) c15) (p12 (f17 c_1)) (not (p22 c15 c_2)) (= (f21 (f7 (f3 c_1 c6)) c_2) (f21 (f21 (f2 c_1) (f4 (f4 c5 c6) (f16 c_1))) c_2)) (not (p22 c_2 (f4 c8 c6))) (not (p12 (f24 c_1))) (not (p12 (f23 c_1))) )(or (p22 (f11 c_2) c15) (p12 (f17 c_2)) (not (p22 c15 c_0)) (= (f21 (f7 (f3 c_2 c6)) c_0) (f21 (f21 (f2 c_2) (f4 (f4 c5 c6) (f16 c_2))) c_0)) (not (p22 c_0 (f4 c8 c6))) (not (p12 (f24 c_2))) (not (p12 (f23 c_2))) )(or (p22 (f11 c_2) c15) (p12 (f17 c_2)) (not (p22 c15 c_1)) (= (f21 (f7 (f3 c_2 c6)) c_1) (f21 (f21 (f2 c_2) (f4 (f4 c5 c6) (f16 c_2))) c_1)) (not (p22 c_1 (f4 c8 c6))) (not (p12 (f24 c_2))) (not (p12 (f23 c_2))) )(or (p22 (f11 c_2) c15) (p12 (f17 c_2)) (not (p22 c15 c_2)) (= (f21 (f7 (f3 c_2 c6)) c_2) (f21 (f21 (f2 c_2) (f4 (f4 c5 c6) (f16 c_2))) c_2)) (not (p22 c_2 (f4 c8 c6))) (not (p12 (f24 c_2))) (not (p12 (f23 c_2))) )(or (not (p12 (f19 (f3 c_0 c6)))) (p22 c5 (f11 c_0)) (p12 (f23 c_0)) (p12 (f17 c_0)) (not (p12 (f24 c_0))) )(or (not (p12 (f19 (f3 c_1 c6)))) (p22 c5 (f11 c_1)) (p12 (f23 c_1)) (p12 (f17 c_1)) (not (p12 (f24 c_1))) )(or (not (p12 (f19 (f3 c_2 c6)))) (p22 c5 (f11 c_2)) (p12 (f23 c_2)) (p12 (f17 c_2)) (not (p12 (f24 c_2))) )(or (p12 c_0) (p12 (f36 c_0 c_0)) (not (p12 c_0)) )(or (p12 c_0) (p12 (f36 c_0 c_1)) (not (p12 c_1)) )(or (p12 c_0) (p12 (f36 c_0 c_2)) (not (p12 c_2)) )(or (p12 c_1) (p12 (f36 c_1 c_0)) (not (p12 c_0)) )(or (p12 c_1) (p12 (f36 c_1 c_1)) (not (p12 c_1)) )(or (p12 c_1) (p12 (f36 c_1 c_2)) (not (p12 c_2)) )(or (p12 c_2) (p12 (f36 c_2 c_0)) (not (p12 c_0)) )(or (p12 c_2) (p12 (f36 c_2 c_1)) (not (p12 c_1)) )(or (p12 c_2) (p12 (f36 c_2 c_2)) (not (p12 c_2)) )(or (p22 c_0 c15) (= (f21 (f28 c_0 c_0) c_0) (f21 c_0 (f4 c_0 c6))) )(or (p22 c_0 c15) (= (f21 (f28 c_0 c_1) c_0) (f21 c_1 (f4 c_0 c6))) )(or (p22 c_0 c15) (= (f21 (f28 c_0 c_2) c_0) (f21 c_2 (f4 c_0 c6))) )(or (p22 c_0 c15) (= (f21 (f28 c_1 c_0) c_0) (f21 c_0 (f4 c_0 c6))) )(or (p22 c_0 c15) (= (f21 (f28 c_1 c_1) c_0) (f21 c_1 (f4 c_0 c6))) )(or (p22 c_0 c15) (= (f21 (f28 c_1 c_2) c_0) (f21 c_2 (f4 c_0 c6))) )(or (p22 c_0 c15) (= (f21 (f28 c_2 c_0) c_0) (f21 c_0 (f4 c_0 c6))) )(or (p22 c_0 c15) (= (f21 (f28 c_2 c_1) c_0) (f21 c_1 (f4 c_0 c6))) )(or (p22 c_0 c15) (= (f21 (f28 c_2 c_2) c_0) (f21 c_2 (f4 c_0 c6))) )(or (p22 c_1 c15) (= (f21 (f28 c_0 c_0) c_1) (f21 c_0 (f4 c_1 c6))) )(or (p22 c_1 c15) (= (f21 (f28 c_0 c_1) c_1) (f21 c_1 (f4 c_1 c6))) )(or (p22 c_1 c15) (= (f21 (f28 c_0 c_2) c_1) (f21 c_2 (f4 c_1 c6))) )(or (p22 c_1 c15) (= (f21 (f28 c_1 c_0) c_1) (f21 c_0 (f4 c_1 c6))) )(or (p22 c_1 c15) (= (f21 (f28 c_1 c_1) c_1) (f21 c_1 (f4 c_1 c6))) )(or (p22 c_1 c15) (= (f21 (f28 c_1 c_2) c_1) (f21 c_2 (f4 c_1 c6))) )(or (p22 c_1 c15) (= (f21 (f28 c_2 c_0) c_1) (f21 c_0 (f4 c_1 c6))) )(or (p22 c_1 c15) (= (f21 (f28 c_2 c_1) c_1) (f21 c_1 (f4 c_1 c6))) )(or (p22 c_1 c15) (= (f21 (f28 c_2 c_2) c_1) (f21 c_2 (f4 c_1 c6))) )(or (p22 c_2 c15) (= (f21 (f28 c_0 c_0) c_2) (f21 c_0 (f4 c_2 c6))) )(or (p22 c_2 c15) (= (f21 (f28 c_0 c_1) c_2) (f21 c_1 (f4 c_2 c6))) )(or (p22 c_2 c15) (= (f21 (f28 c_0 c_2) c_2) (f21 c_2 (f4 c_2 c6))) )(or (p22 c_2 c15) (= (f21 (f28 c_1 c_0) c_2) (f21 c_0 (f4 c_2 c6))) )(or (p22 c_2 c15) (= (f21 (f28 c_1 c_1) c_2) (f21 c_1 (f4 c_2 c6))) )(or (p22 c_2 c15) (= (f21 (f28 c_1 c_2) c_2) (f21 c_2 (f4 c_2 c6))) )(or (p22 c_2 c15) (= (f21 (f28 c_2 c_0) c_2) (f21 c_0 (f4 c_2 c6))) )(or (p22 c_2 c15) (= (f21 (f28 c_2 c_1) c_2) (f21 c_1 (f4 c_2 c6))) )(or (p22 c_2 c15) (= (f21 (f28 c_2 c_2) c_2) (f21 c_2 (f4 c_2 c6))) )(or (p12 (f36 c_0 c_0)) (not (p12 c_0)) (p12 c_0) )(or (p12 (f36 c_0 c_1)) (not (p12 c_0)) (p12 c_1) )(or (p12 (f36 c_0 c_2)) (not (p12 c_0)) (p12 c_2) )(or (p12 (f36 c_1 c_0)) (not (p12 c_1)) (p12 c_0) )(or (p12 (f36 c_1 c_1)) (not (p12 c_1)) (p12 c_1) )(or (p12 (f36 c_1 c_2)) (not (p12 c_1)) (p12 c_2) )(or (p12 (f36 c_2 c_0)) (not (p12 c_2)) (p12 c_0) )(or (p12 (f36 c_2 c_1)) (not (p12 c_2)) (p12 c_1) )(or (p12 (f36 c_2 c_2)) (not (p12 c_2)) (p12 c_2) )(or (p12 (f17 c_0)) (not (p12 (f23 c_0))) (p12 (f24 c_0)) (not (p22 (f11 c_0) c15)) (not (p22 c_0 (f4 c8 c6))) (not (p22 c15 c_0)) (= (f21 (f7 (f3 c_0 c6)) c_0) (f21 (f7 c_0) c_0)) )(or (p12 (f17 c_0)) (not (p12 (f23 c_0))) (p12 (f24 c_0)) (not (p22 (f11 c_0) c15)) (not (p22 c_1 (f4 c8 c6))) (not (p22 c15 c_1)) (= (f21 (f7 (f3 c_0 c6)) c_1) (f21 (f7 c_0) c_1)) )(or (p12 (f17 c_0)) (not (p12 (f23 c_0))) (p12 (f24 c_0)) (not (p22 (f11 c_0) c15)) (not (p22 c_2 (f4 c8 c6))) (not (p22 c15 c_2)) (= (f21 (f7 (f3 c_0 c6)) c_2) (f21 (f7 c_0) c_2)) )(or (p12 (f17 c_1)) (not (p12 (f23 c_1))) (p12 (f24 c_1)) (not (p22 (f11 c_1) c15)) (not (p22 c_0 (f4 c8 c6))) (not (p22 c15 c_0)) (= (f21 (f7 (f3 c_1 c6)) c_0) (f21 (f7 c_1) c_0)) )(or (p12 (f17 c_1)) (not (p12 (f23 c_1))) (p12 (f24 c_1)) (not (p22 (f11 c_1) c15)) (not (p22 c_1 (f4 c8 c6))) (not (p22 c15 c_1)) (= (f21 (f7 (f3 c_1 c6)) c_1) (f21 (f7 c_1) c_1)) )(or (p12 (f17 c_1)) (not (p12 (f23 c_1))) (p12 (f24 c_1)) (not (p22 (f11 c_1) c15)) (not (p22 c_2 (f4 c8 c6))) (not (p22 c15 c_2)) (= (f21 (f7 (f3 c_1 c6)) c_2) (f21 (f7 c_1) c_2)) )(or (p12 (f17 c_2)) (not (p12 (f23 c_2))) (p12 (f24 c_2)) (not (p22 (f11 c_2) c15)) (not (p22 c_0 (f4 c8 c6))) (not (p22 c15 c_0)) (= (f21 (f7 (f3 c_2 c6)) c_0) (f21 (f7 c_2) c_0)) )(or (p12 (f17 c_2)) (not (p12 (f23 c_2))) (p12 (f24 c_2)) (not (p22 (f11 c_2) c15)) (not (p22 c_1 (f4 c8 c6))) (not (p22 c15 c_1)) (= (f21 (f7 (f3 c_2 c6)) c_1) (f21 (f7 c_2) c_1)) )(or (p12 (f17 c_2)) (not (p12 (f23 c_2))) (p12 (f24 c_2)) (not (p22 (f11 c_2) c15)) (not (p22 c_2 (f4 c8 c6))) (not (p22 c15 c_2)) (= (f21 (f7 (f3 c_2 c6)) c_2) (f21 (f7 c_2) c_2)) )(or (not (p12 (f36 c_0 c_0))) (not (p12 c_0)) (not (p12 c_0)) )(or (not (p12 (f36 c_0 c_1))) (not (p12 c_0)) (not (p12 c_1)) )(or (not (p12 (f36 c_0 c_2))) (not (p12 c_0)) (not (p12 c_2)) )(or (not (p12 (f36 c_1 c_0))) (not (p12 c_1)) (not (p12 c_0)) )(or (not (p12 (f36 c_1 c_1))) (not (p12 c_1)) (not (p12 c_1)) )(or (not (p12 (f36 c_1 c_2))) (not (p12 c_1)) (not (p12 c_2)) )(or (not (p12 (f36 c_2 c_0))) (not (p12 c_2)) (not (p12 c_0)) )(or (not (p12 (f36 c_2 c_1))) (not (p12 c_2)) (not (p12 c_1)) )(or (not (p12 (f36 c_2 c_2))) (not (p12 c_2)) (not (p12 c_2)) )(or (p12 (f47 c_0 c_0)) (p22 c_0 c_0) )(or (p12 (f47 c_0 c_1)) (p22 c_0 c_1) )(or (p12 (f47 c_0 c_2)) (p22 c_0 c_2) )(or (p12 (f47 c_1 c_0)) (p22 c_1 c_0) )(or (p12 (f47 c_1 c_1)) (p22 c_1 c_1) )(or (p12 (f47 c_1 c_2)) (p22 c_1 c_2) )(or (p12 (f47 c_2 c_0)) (p22 c_2 c_0) )(or (p12 (f47 c_2 c_1)) (p22 c_2 c_1) )(or (p12 (f47 c_2 c_2)) (p22 c_2 c_2) )(not (p12 (f13 (f3 c49 c6)))) (= (f10 c_0) (f11 c_0)) (= (f10 c_1) (f11 c_1)) (= (f10 c_2) (f11 c_2)) (or (p12 (f23 c_0)) (p12 (f19 (f3 c_0 c6))) (not (p12 (f24 c_0))) (not (p22 c5 (f11 c_0))) (p12 (f17 c_0)) )(or (p12 (f23 c_1)) (p12 (f19 (f3 c_1 c6))) (not (p12 (f24 c_1))) (not (p22 c5 (f11 c_1))) (p12 (f17 c_1)) )(or (p12 (f23 c_2)) (p12 (f19 (f3 c_2 c6))) (not (p12 (f24 c_2))) (not (p22 c5 (f11 c_2))) (p12 (f17 c_2)) )(or (p12 (f39 c_0 c_0)) (p12 c_0) (p12 c_0) )(or (p12 (f39 c_0 c_1)) (p12 c_0) (p12 c_1) )(or (p12 (f39 c_0 c_2)) (p12 c_0) (p12 c_2) )(or (p12 (f39 c_1 c_0)) (p12 c_1) (p12 c_0) )(or (p12 (f39 c_1 c_1)) (p12 c_1) (p12 c_1) )(or (p12 (f39 c_1 c_2)) (p12 c_1) (p12 c_2) )(or (p12 (f39 c_2 c_0)) (p12 c_2) (p12 c_0) )(or (p12 (f39 c_2 c_1)) (p12 c_2) (p12 c_1) )(or (p12 (f39 c_2 c_2)) (p12 c_2) (p12 c_2) )(or (not (p12 (f44 c_0 c_0))) (= c_0 c_0) )(or (not (p12 (f44 c_0 c_1))) (= c_0 c_1) )(or (not (p12 (f44 c_0 c_2))) (= c_0 c_2) )(or (not (p12 (f44 c_1 c_0))) (= c_1 c_0) )(or (not (p12 (f44 c_1 c_1))) (= c_1 c_1) )(or (not (p12 (f44 c_1 c_2))) (= c_1 c_2) )(or (not (p12 (f44 c_2 c_0))) (= c_2 c_0) )(or (not (p12 (f44 c_2 c_1))) (= c_2 c_1) )(or (not (p12 (f44 c_2 c_2))) (= c_2 c_2) )(or (p22 c_0 c_0) (p12 (f45 c_0 c_0)) )(or (p22 c_0 c_1) (p12 (f45 c_1 c_0)) )(or (p22 c_0 c_2) (p12 (f45 c_2 c_0)) )(or (p22 c_1 c_0) (p12 (f45 c_0 c_1)) )(or (p22 c_1 c_1) (p12 (f45 c_1 c_1)) )(or (p22 c_1 c_2) (p12 (f45 c_2 c_1)) )(or (p22 c_2 c_0) (p12 (f45 c_0 c_2)) )(or (p22 c_2 c_1) (p12 (f45 c_1 c_2)) )(or (p22 c_2 c_2) (p12 (f45 c_2 c_2)) )(or (p12 (f44 c_0 c_0)) (not (= c_0 c_0)) )(or (p12 (f44 c_0 c_1)) (not (= c_0 c_1)) )(or (p12 (f44 c_0 c_2)) (not (= c_0 c_2)) )(or (p12 (f44 c_1 c_0)) (not (= c_1 c_0)) )(or (p12 (f44 c_1 c_1)) (not (= c_1 c_1)) )(or (p12 (f44 c_1 c_2)) (not (= c_1 c_2)) )(or (p12 (f44 c_2 c_0)) (not (= c_2 c_0)) )(or (p12 (f44 c_2 c_1)) (not (= c_2 c_1)) )(or (p12 (f44 c_2 c_2)) (not (= c_2 c_2)) )(p12 c41) (or (not (p22 c15 c_0)) (not (p12 (f21 (f7 (f3 c_0 c6)) c_0))) (not (p12 (f17 c_0))) (not (p22 c_0 (f4 c8 c6))) )(or (not (p22 c15 c_0)) (not (p12 (f21 (f7 (f3 c_1 c6)) c_0))) (not (p12 (f17 c_1))) (not (p22 c_0 (f4 c8 c6))) )(or (not (p22 c15 c_0)) (not (p12 (f21 (f7 (f3 c_2 c6)) c_0))) (not (p12 (f17 c_2))) (not (p22 c_0 (f4 c8 c6))) )(or (not (p22 c15 c_1)) (not (p12 (f21 (f7 (f3 c_0 c6)) c_1))) (not (p12 (f17 c_0))) (not (p22 c_1 (f4 c8 c6))) )(or (not (p22 c15 c_1)) (not (p12 (f21 (f7 (f3 c_1 c6)) c_1))) (not (p12 (f17 c_1))) (not (p22 c_1 (f4 c8 c6))) )(or (not (p22 c15 c_1)) (not (p12 (f21 (f7 (f3 c_2 c6)) c_1))) (not (p12 (f17 c_2))) (not (p22 c_1 (f4 c8 c6))) )(or (not (p22 c15 c_2)) (not (p12 (f21 (f7 (f3 c_0 c6)) c_2))) (not (p12 (f17 c_0))) (not (p22 c_2 (f4 c8 c6))) )(or (not (p22 c15 c_2)) (not (p12 (f21 (f7 (f3 c_1 c6)) c_2))) (not (p12 (f17 c_1))) (not (p22 c_2 (f4 c8 c6))) )(or (not (p22 c15 c_2)) (not (p12 (f21 (f7 (f3 c_2 c6)) c_2))) (not (p12 (f17 c_2))) (not (p22 c_2 (f4 c8 c6))) )(or (not (p22 (f33 c_0) c_0)) (= (f21 (f30 c_0 c_0) c_0) (f21 c_0 (f4 c_0 (f33 c_0)))) )(or (not (p22 (f33 c_0) c_0)) (= (f21 (f30 c_0 c_1) c_0) (f21 c_1 (f4 c_0 (f33 c_0)))) )(or (not (p22 (f33 c_0) c_0)) (= (f21 (f30 c_0 c_2) c_0) (f21 c_2 (f4 c_0 (f33 c_0)))) )(or (not (p22 (f33 c_0) c_1)) (= (f21 (f30 c_0 c_0) c_1) (f21 c_0 (f4 c_1 (f33 c_0)))) )(or (not (p22 (f33 c_0) c_1)) (= (f21 (f30 c_0 c_1) c_1) (f21 c_1 (f4 c_1 (f33 c_0)))) )(or (not (p22 (f33 c_0) c_1)) (= (f21 (f30 c_0 c_2) c_1) (f21 c_2 (f4 c_1 (f33 c_0)))) )(or (not (p22 (f33 c_0) c_2)) (= (f21 (f30 c_0 c_0) c_2) (f21 c_0 (f4 c_2 (f33 c_0)))) )(or (not (p22 (f33 c_0) c_2)) (= (f21 (f30 c_0 c_1) c_2) (f21 c_1 (f4 c_2 (f33 c_0)))) )(or (not (p22 (f33 c_0) c_2)) (= (f21 (f30 c_0 c_2) c_2) (f21 c_2 (f4 c_2 (f33 c_0)))) )(or (not (p22 (f33 c_1) c_0)) (= (f21 (f30 c_1 c_0) c_0) (f21 c_0 (f4 c_0 (f33 c_1)))) )(or (not (p22 (f33 c_1) c_0)) (= (f21 (f30 c_1 c_1) c_0) (f21 c_1 (f4 c_0 (f33 c_1)))) )(or (not (p22 (f33 c_1) c_0)) (= (f21 (f30 c_1 c_2) c_0) (f21 c_2 (f4 c_0 (f33 c_1)))) )(or (not (p22 (f33 c_1) c_1)) (= (f21 (f30 c_1 c_0) c_1) (f21 c_0 (f4 c_1 (f33 c_1)))) )(or (not (p22 (f33 c_1) c_1)) (= (f21 (f30 c_1 c_1) c_1) (f21 c_1 (f4 c_1 (f33 c_1)))) )(or (not (p22 (f33 c_1) c_1)) (= (f21 (f30 c_1 c_2) c_1) (f21 c_2 (f4 c_1 (f33 c_1)))) )(or (not (p22 (f33 c_1) c_2)) (= (f21 (f30 c_1 c_0) c_2) (f21 c_0 (f4 c_2 (f33 c_1)))) )(or (not (p22 (f33 c_1) c_2)) (= (f21 (f30 c_1 c_1) c_2) (f21 c_1 (f4 c_2 (f33 c_1)))) )(or (not (p22 (f33 c_1) c_2)) (= (f21 (f30 c_1 c_2) c_2) (f21 c_2 (f4 c_2 (f33 c_1)))) )(or (not (p22 (f33 c_2) c_0)) (= (f21 (f30 c_2 c_0) c_0) (f21 c_0 (f4 c_0 (f33 c_2)))) )(or (not (p22 (f33 c_2) c_0)) (= (f21 (f30 c_2 c_1) c_0) (f21 c_1 (f4 c_0 (f33 c_2)))) )(or (not (p22 (f33 c_2) c_0)) (= (f21 (f30 c_2 c_2) c_0) (f21 c_2 (f4 c_0 (f33 c_2)))) )(or (not (p22 (f33 c_2) c_1)) (= (f21 (f30 c_2 c_0) c_1) (f21 c_0 (f4 c_1 (f33 c_2)))) )(or (not (p22 (f33 c_2) c_1)) (= (f21 (f30 c_2 c_1) c_1) (f21 c_1 (f4 c_1 (f33 c_2)))) )(or (not (p22 (f33 c_2) c_1)) (= (f21 (f30 c_2 c_2) c_1) (f21 c_2 (f4 c_1 (f33 c_2)))) )(or (not (p22 (f33 c_2) c_2)) (= (f21 (f30 c_2 c_0) c_2) (f21 c_0 (f4 c_2 (f33 c_2)))) )(or (not (p22 (f33 c_2) c_2)) (= (f21 (f30 c_2 c_1) c_2) (f21 c_1 (f4 c_2 (f33 c_2)))) )(or (not (p22 (f33 c_2) c_2)) (= (f21 (f30 c_2 c_2) c_2) (f21 c_2 (f4 c_2 (f33 c_2)))) )(or (not (p12 (f23 c_0))) (p12 (f24 c_0)) (p12 (f17 c_0)) (= (f11 (f3 c_0 c6)) (f4 (f11 c_0) c6)) (p22 (f11 c_0) c15) )(or (not (p12 (f23 c_1))) (p12 (f24 c_1)) (p12 (f17 c_1)) (= (f11 (f3 c_1 c6)) (f4 (f11 c_1) c6)) (p22 (f11 c_1) c15) )(or (not (p12 (f23 c_2))) (p12 (f24 c_2)) (p12 (f17 c_2)) (= (f11 (f3 c_2 c6)) (f4 (f11 c_2) c6)) (p22 (f11 c_2) c15) )(or (not (p22 c15 c_0)) (not (p12 (f24 c_0))) (not (p22 (f11 c_0) c15)) (p12 (f17 c_0)) (not (p12 (f23 c_0))) (= (f21 (f7 (f3 c_0 c6)) c_0) (f21 (f7 c_0) c_0)) (not (p22 c_0 (f4 c8 c6))) )(or (not (p22 c15 c_0)) (not (p12 (f24 c_1))) (not (p22 (f11 c_1) c15)) (p12 (f17 c_1)) (not (p12 (f23 c_1))) (= (f21 (f7 (f3 c_1 c6)) c_0) (f21 (f7 c_1) c_0)) (not (p22 c_0 (f4 c8 c6))) )(or (not (p22 c15 c_0)) (not (p12 (f24 c_2))) (not (p22 (f11 c_2) c15)) (p12 (f17 c_2)) (not (p12 (f23 c_2))) (= (f21 (f7 (f3 c_2 c6)) c_0) (f21 (f7 c_2) c_0)) (not (p22 c_0 (f4 c8 c6))) )(or (not (p22 c15 c_1)) (not (p12 (f24 c_0))) (not (p22 (f11 c_0) c15)) (p12 (f17 c_0)) (not (p12 (f23 c_0))) (= (f21 (f7 (f3 c_0 c6)) c_1) (f21 (f7 c_0) c_1)) (not (p22 c_1 (f4 c8 c6))) )(or (not (p22 c15 c_1)) (not (p12 (f24 c_1))) (not (p22 (f11 c_1) c15)) (p12 (f17 c_1)) (not (p12 (f23 c_1))) (= (f21 (f7 (f3 c_1 c6)) c_1) (f21 (f7 c_1) c_1)) (not (p22 c_1 (f4 c8 c6))) )(or (not (p22 c15 c_1)) (not (p12 (f24 c_2))) (not (p22 (f11 c_2) c15)) (p12 (f17 c_2)) (not (p12 (f23 c_2))) (= (f21 (f7 (f3 c_2 c6)) c_1) (f21 (f7 c_2) c_1)) (not (p22 c_1 (f4 c8 c6))) )(or (not (p22 c15 c_2)) (not (p12 (f24 c_0))) (not (p22 (f11 c_0) c15)) (p12 (f17 c_0)) (not (p12 (f23 c_0))) (= (f21 (f7 (f3 c_0 c6)) c_2) (f21 (f7 c_0) c_2)) (not (p22 c_2 (f4 c8 c6))) )(or (not (p22 c15 c_2)) (not (p12 (f24 c_1))) (not (p22 (f11 c_1) c15)) (p12 (f17 c_1)) (not (p12 (f23 c_1))) (= (f21 (f7 (f3 c_1 c6)) c_2) (f21 (f7 c_1) c_2)) (not (p22 c_2 (f4 c8 c6))) )(or (not (p22 c15 c_2)) (not (p12 (f24 c_2))) (not (p22 (f11 c_2) c15)) (p12 (f17 c_2)) (not (p12 (f23 c_2))) (= (f21 (f7 (f3 c_2 c6)) c_2) (f21 (f7 c_2) c_2)) (not (p22 c_2 (f4 c8 c6))) )(or (not (p12 (f23 c_0))) (p12 (f17 c_0)) (p12 (f24 c_0)) (= (f11 (f3 c_0 c6)) (f11 c_0)) (not (p22 (f11 c_0) c15)) )(or (not (p12 (f23 c_1))) (p12 (f17 c_1)) (p12 (f24 c_1)) (= (f11 (f3 c_1 c6)) (f11 c_1)) (not (p22 (f11 c_1) c15)) )(or (not (p12 (f23 c_2))) (p12 (f17 c_2)) (p12 (f24 c_2)) (= (f11 (f3 c_2 c6)) (f11 c_2)) (not (p22 (f11 c_2) c15)) )(or (not (p12 c_0)) (p12 (f35 c_0 c_0)) )(or (not (p12 c_0)) (p12 (f35 c_0 c_1)) )(or (not (p12 c_0)) (p12 (f35 c_0 c_2)) )(or (not (p12 c_1)) (p12 (f35 c_1 c_0)) )(or (not (p12 c_1)) (p12 (f35 c_1 c_1)) )(or (not (p12 c_1)) (p12 (f35 c_1 c_2)) )(or (not (p12 c_2)) (p12 (f35 c_2 c_0)) )(or (not (p12 c_2)) (p12 (f35 c_2 c_1)) )(or (not (p12 c_2)) (p12 (f35 c_2 c_2)) )(not (= c42 c41)) (or (p12 (f20 (f3 c_0 c6))) (not (p12 (f24 c_0))) (not (p12 (f23 c_0))) (p12 (f17 c_0)) (not (p22 (f11 c_0) c15)) )(or (p12 (f20 (f3 c_1 c6))) (not (p12 (f24 c_1))) (not (p12 (f23 c_1))) (p12 (f17 c_1)) (not (p22 (f11 c_1) c15)) )(or (p12 (f20 (f3 c_2 c6))) (not (p12 (f24 c_2))) (not (p12 (f23 c_2))) (p12 (f17 c_2)) (not (p22 (f11 c_2) c15)) )(or (not (p22 c_0 (f4 c8 c6))) (not (p22 c15 c_0)) (not (p22 c_0 (f4 c5 c6))) (not (p22 c5 (f11 c_0))) (not (p12 (f24 c_0))) (p12 (f23 c_0)) (p12 (f17 c_0)) (= (f21 (f21 (f2 (f3 c_0 c6)) c_0) c_0) (f21 (f21 (f2 c_0) c_0) c_0)) (not (p22 c15 c_0)) )(or (not (p22 c_0 (f4 c8 c6))) (not (p22 c15 c_0)) (not (p22 c_0 (f4 c5 c6))) (not (p22 c5 (f11 c_1))) (not (p12 (f24 c_1))) (p12 (f23 c_1)) (p12 (f17 c_1)) (= (f21 (f21 (f2 (f3 c_1 c6)) c_0) c_0) (f21 (f21 (f2 c_1) c_0) c_0)) (not (p22 c15 c_0)) )(or (not (p22 c_0 (f4 c8 c6))) (not (p22 c15 c_0)) (not (p22 c_0 (f4 c5 c6))) (not (p22 c5 (f11 c_2))) (not (p12 (f24 c_2))) (p12 (f23 c_2)) (p12 (f17 c_2)) (= (f21 (f21 (f2 (f3 c_2 c6)) c_0) c_0) (f21 (f21 (f2 c_2) c_0) c_0)) (not (p22 c15 c_0)) )(or (not (p22 c_0 (f4 c8 c6))) (not (p22 c15 c_1)) (not (p22 c_1 (f4 c5 c6))) (not (p22 c5 (f11 c_0))) (not (p12 (f24 c_0))) (p12 (f23 c_0)) (p12 (f17 c_0)) (= (f21 (f21 (f2 (f3 c_0 c6)) c_1) c_0) (f21 (f21 (f2 c_0) c_1) c_0)) (not (p22 c15 c_0)) )(or (not (p22 c_0 (f4 c8 c6))) (not (p22 c15 c_1)) (not (p22 c_1 (f4 c5 c6))) (not (p22 c5 (f11 c_1))) (not (p12 (f24 c_1))) (p12 (f23 c_1)) (p12 (f17 c_1)) (= (f21 (f21 (f2 (f3 c_1 c6)) c_1) c_0) (f21 (f21 (f2 c_1) c_1) c_0)) (not (p22 c15 c_0)) )(or (not (p22 c_0 (f4 c8 c6))) (not (p22 c15 c_1)) (not (p22 c_1 (f4 c5 c6))) (not (p22 c5 (f11 c_2))) (not (p12 (f24 c_2))) (p12 (f23 c_2)) (p12 (f17 c_2)) (= (f21 (f21 (f2 (f3 c_2 c6)) c_1) c_0) (f21 (f21 (f2 c_2) c_1) c_0)) (not (p22 c15 c_0)) )(or (not (p22 c_0 (f4 c8 c6))) (not (p22 c15 c_2)) (not (p22 c_2 (f4 c5 c6))) (not (p22 c5 (f11 c_0))) (not (p12 (f24 c_0))) (p12 (f23 c_0)) (p12 (f17 c_0)) (= (f21 (f21 (f2 (f3 c_0 c6)) c_2) c_0) (f21 (f21 (f2 c_0) c_2) c_0)) (not (p22 c15 c_0)) )(or (not (p22 c_0 (f4 c8 c6))) (not (p22 c15 c_2)) (not (p22 c_2 (f4 c5 c6))) (not (p22 c5 (f11 c_1))) (not (p12 (f24 c_1))) (p12 (f23 c_1)) (p12 (f17 c_1)) (= (f21 (f21 (f2 (f3 c_1 c6)) c_2) c_0) (f21 (f21 (f2 c_1) c_2) c_0)) (not (p22 c15 c_0)) )(or (not (p22 c_0 (f4 c8 c6))) (not (p22 c15 c_2)) (not (p22 c_2 (f4 c5 c6))) (not (p22 c5 (f11 c_2))) (not (p12 (f24 c_2))) (p12 (f23 c_2)) (p12 (f17 c_2)) (= (f21 (f21 (f2 (f3 c_2 c6)) c_2) c_0) (f21 (f21 (f2 c_2) c_2) c_0)) (not (p22 c15 c_0)) )(or (not (p22 c_1 (f4 c8 c6))) (not (p22 c15 c_0)) (not (p22 c_0 (f4 c5 c6))) (not (p22 c5 (f11 c_0))) (not (p12 (f24 c_0))) (p12 (f23 c_0)) (p12 (f17 c_0)) (= (f21 (f21 (f2 (f3 c_0 c6)) c_0) c_1) (f21 (f21 (f2 c_0) c_0) c_1)) (not (p22 c15 c_1)) )(or (not (p22 c_1 (f4 c8 c6))) (not (p22 c15 c_0)) (not (p22 c_0 (f4 c5 c6))) (not (p22 c5 (f11 c_1))) (not (p12 (f24 c_1))) (p12 (f23 c_1)) (p12 (f17 c_1)) (= (f21 (f21 (f2 (f3 c_1 c6)) c_0) c_1) (f21 (f21 (f2 c_1) c_0) c_1)) (not (p22 c15 c_1)) )(or (not (p22 c_1 (f4 c8 c6))) (not (p22 c15 c_0)) (not (p22 c_0 (f4 c5 c6))) (not (p22 c5 (f11 c_2))) (not (p12 (f24 c_2))) (p12 (f23 c_2)) (p12 (f17 c_2)) (= (f21 (f21 (f2 (f3 c_2 c6)) c_0) c_1) (f21 (f21 (f2 c_2) c_0) c_1)) (not (p22 c15 c_1)) )(or (not (p22 c_1 (f4 c8 c6))) (not (p22 c15 c_1)) (not (p22 c_1 (f4 c5 c6))) (not (p22 c5 (f11 c_0))) (not (p12 (f24 c_0))) (p12 (f23 c_0)) (p12 (f17 c_0)) (= (f21 (f21 (f2 (f3 c_0 c6)) c_1) c_1) (f21 (f21 (f2 c_0) c_1) c_1)) (not (p22 c15 c_1)) )(or (not (p22 c_1 (f4 c8 c6))) (not (p22 c15 c_1)) (not (p22 c_1 (f4 c5 c6))) (not (p22 c5 (f11 c_1))) (not (p12 (f24 c_1))) (p12 (f23 c_1)) (p12 (f17 c_1)) (= (f21 (f21 (f2 (f3 c_1 c6)) c_1) c_1) (f21 (f21 (f2 c_1) c_1) c_1)) (not (p22 c15 c_1)) )(or (not (p22 c_1 (f4 c8 c6))) (not (p22 c15 c_1)) (not (p22 c_1 (f4 c5 c6))) (not (p22 c5 (f11 c_2))) (not (p12 (f24 c_2))) (p12 (f23 c_2)) (p12 (f17 c_2)) (= (f21 (f21 (f2 (f3 c_2 c6)) c_1) c_1) (f21 (f21 (f2 c_2) c_1) c_1)) (not (p22 c15 c_1)) )(or (not (p22 c_1 (f4 c8 c6))) (not (p22 c15 c_2)) (not (p22 c_2 (f4 c5 c6))) (not (p22 c5 (f11 c_0))) (not (p12 (f24 c_0))) (p12 (f23 c_0)) (p12 (f17 c_0)) (= (f21 (f21 (f2 (f3 c_0 c6)) c_2) c_1) (f21 (f21 (f2 c_0) c_2) c_1)) (not (p22 c15 c_1)) )(or (not (p22 c_1 (f4 c8 c6))) (not (p22 c15 c_2)) (not (p22 c_2 (f4 c5 c6))) (not (p22 c5 (f11 c_1))) (not (p12 (f24 c_1))) (p12 (f23 c_1)) (p12 (f17 c_1)) (= (f21 (f21 (f2 (f3 c_1 c6)) c_2) c_1) (f21 (f21 (f2 c_1) c_2) c_1)) (not (p22 c15 c_1)) )(or (not (p22 c_1 (f4 c8 c6))) (not (p22 c15 c_2)) (not (p22 c_2 (f4 c5 c6))) (not (p22 c5 (f11 c_2))) (not (p12 (f24 c_2))) (p12 (f23 c_2)) (p12 (f17 c_2)) (= (f21 (f21 (f2 (f3 c_2 c6)) c_2) c_1) (f21 (f21 (f2 c_2) c_2) c_1)) (not (p22 c15 c_1)) )(or (not (p22 c_2 (f4 c8 c6))) (not (p22 c15 c_0)) (not (p22 c_0 (f4 c5 c6))) (not (p22 c5 (f11 c_0))) (not (p12 (f24 c_0))) (p12 (f23 c_0)) (p12 (f17 c_0)) (= (f21 (f21 (f2 (f3 c_0 c6)) c_0) c_2) (f21 (f21 (f2 c_0) c_0) c_2)) (not (p22 c15 c_2)) )(or (not (p22 c_2 (f4 c8 c6))) (not (p22 c15 c_0)) (not (p22 c_0 (f4 c5 c6))) (not (p22 c5 (f11 c_1))) (not (p12 (f24 c_1))) (p12 (f23 c_1)) (p12 (f17 c_1)) (= (f21 (f21 (f2 (f3 c_1 c6)) c_0) c_2) (f21 (f21 (f2 c_1) c_0) c_2)) (not (p22 c15 c_2)) )(or (not (p22 c_2 (f4 c8 c6))) (not (p22 c15 c_0)) (not (p22 c_0 (f4 c5 c6))) (not (p22 c5 (f11 c_2))) (not (p12 (f24 c_2))) (p12 (f23 c_2)) (p12 (f17 c_2)) (= (f21 (f21 (f2 (f3 c_2 c6)) c_0) c_2) (f21 (f21 (f2 c_2) c_0) c_2)) (not (p22 c15 c_2)) )(or (not (p22 c_2 (f4 c8 c6))) (not (p22 c15 c_1)) (not (p22 c_1 (f4 c5 c6))) (not (p22 c5 (f11 c_0))) (not (p12 (f24 c_0))) (p12 (f23 c_0)) (p12 (f17 c_0)) (= (f21 (f21 (f2 (f3 c_0 c6)) c_1) c_2) (f21 (f21 (f2 c_0) c_1) c_2)) (not (p22 c15 c_2)) )(or (not (p22 c_2 (f4 c8 c6))) (not (p22 c15 c_1)) (not (p22 c_1 (f4 c5 c6))) (not (p22 c5 (f11 c_1))) (not (p12 (f24 c_1))) (p12 (f23 c_1)) (p12 (f17 c_1)) (= (f21 (f21 (f2 (f3 c_1 c6)) c_1) c_2) (f21 (f21 (f2 c_1) c_1) c_2)) (not (p22 c15 c_2)) )(or (not (p22 c_2 (f4 c8 c6))) (not (p22 c15 c_1)) (not (p22 c_1 (f4 c5 c6))) (not (p22 c5 (f11 c_2))) (not (p12 (f24 c_2))) (p12 (f23 c_2)) (p12 (f17 c_2)) (= (f21 (f21 (f2 (f3 c_2 c6)) c_1) c_2) (f21 (f21 (f2 c_2) c_1) c_2)) (not (p22 c15 c_2)) )(or (not (p22 c_2 (f4 c8 c6))) (not (p22 c15 c_2)) (not (p22 c_2 (f4 c5 c6))) (not (p22 c5 (f11 c_0))) (not (p12 (f24 c_0))) (p12 (f23 c_0)) (p12 (f17 c_0)) (= (f21 (f21 (f2 (f3 c_0 c6)) c_2) c_2) (f21 (f21 (f2 c_0) c_2) c_2)) (not (p22 c15 c_2)) )(or (not (p22 c_2 (f4 c8 c6))) (not (p22 c15 c_2)) (not (p22 c_2 (f4 c5 c6))) (not (p22 c5 (f11 c_1))) (not (p12 (f24 c_1))) (p12 (f23 c_1)) (p12 (f17 c_1)) (= (f21 (f21 (f2 (f3 c_1 c6)) c_2) c_2) (f21 (f21 (f2 c_1) c_2) c_2)) (not (p22 c15 c_2)) )(or (not (p22 c_2 (f4 c8 c6))) (not (p22 c15 c_2)) (not (p22 c_2 (f4 c5 c6))) (not (p22 c5 (f11 c_2))) (not (p12 (f24 c_2))) (p12 (f23 c_2)) (p12 (f17 c_2)) (= (f21 (f21 (f2 (f3 c_2 c6)) c_2) c_2) (f21 (f21 (f2 c_2) c_2) c_2)) (not (p22 c15 c_2)) )(or (not (p12 (f24 c_0))) (not (p22 c5 (f11 c_0))) (p12 (f17 c_0)) (p12 (f23 c_0)) (= (f11 (f3 c_0 c6)) (f11 c_0)) )(or (not (p12 (f24 c_1))) (not (p22 c5 (f11 c_1))) (p12 (f17 c_1)) (p12 (f23 c_1)) (= (f11 (f3 c_1 c6)) (f11 c_1)) )(or (not (p12 (f24 c_2))) (not (p22 c5 (f11 c_2))) (p12 (f17 c_2)) (p12 (f23 c_2)) (= (f11 (f3 c_2 c6)) (f11 c_2)) )(or (not (p12 (f17 c_0))) (= (f18 (f3 c_0 c6)) c15) )(or (not (p12 (f17 c_1))) (= (f18 (f3 c_1 c6)) c15) )(or (not (p12 (f17 c_2))) (= (f18 (f3 c_2 c6)) c15) )(or (p12 (f17 c_0)) (p12 (f23 c_0)) (p12 (f24 c_0)) (= (f16 (f3 c_0 c6)) (f16 c_0)) )(or (p12 (f17 c_1)) (p12 (f23 c_1)) (p12 (f24 c_1)) (= (f16 (f3 c_1 c6)) (f16 c_1)) )(or (p12 (f17 c_2)) (p12 (f23 c_2)) (p12 (f24 c_2)) (= (f16 (f3 c_2 c6)) (f16 c_2)) )(= (f1 (f28 c_0 c_0)) (f3 (f1 c_0) c6)) (= (f1 (f28 c_0 c_1)) (f3 (f1 c_1) c6)) (= (f1 (f28 c_0 c_2)) (f3 (f1 c_2) c6)) (= (f1 (f28 c_1 c_0)) (f3 (f1 c_0) c6)) (= (f1 (f28 c_1 c_1)) (f3 (f1 c_1) c6)) (= (f1 (f28 c_1 c_2)) (f3 (f1 c_2) c6)) (= (f1 (f28 c_2 c_0)) (f3 (f1 c_0) c6)) (= (f1 (f28 c_2 c_1)) (f3 (f1 c_1) c6)) (= (f1 (f28 c_2 c_2)) (f3 (f1 c_2) c6)) (or (not (p12 (f20 (f3 c_0 c6)))) (not (p12 (f17 c_0))) )(or (not (p12 (f20 (f3 c_1 c6)))) (not (p12 (f17 c_1))) )(or (not (p12 (f20 (f3 c_2 c6)))) (not (p12 (f17 c_2))) )(or (p22 c_0 c_0) (not (p12 (f46 c_0 c_0))) )(or (p22 c_0 c_1) (not (p12 (f46 c_0 c_1))) )(or (p22 c_0 c_2) (not (p12 (f46 c_0 c_2))) )(or (p22 c_1 c_0) (not (p12 (f46 c_1 c_0))) )(or (p22 c_1 c_1) (not (p12 (f46 c_1 c_1))) )(or (p22 c_1 c_2) (not (p12 (f46 c_1 c_2))) )(or (p22 c_2 c_0) (not (p12 (f46 c_2 c_0))) )(or (p22 c_2 c_1) (not (p12 (f46 c_2 c_1))) )(or (p22 c_2 c_2) (not (p12 (f46 c_2 c_2))) )(or (p22 c5 (f11 c_0)) (p12 (f17 c_0)) (not (p12 (f24 c_0))) (not (p22 c_0 (f4 c8 c6))) (p12 (f23 c_0)) (not (p22 c15 c_0)) (= (f21 (f21 (f2 (f3 c_0 c6)) (f4 (f4 c5 c6) (f18 c_0))) c_0) (f21 (f9 c_0) c_0)) )(or (p22 c5 (f11 c_0)) (p12 (f17 c_0)) (not (p12 (f24 c_0))) (not (p22 c_1 (f4 c8 c6))) (p12 (f23 c_0)) (not (p22 c15 c_1)) (= (f21 (f21 (f2 (f3 c_0 c6)) (f4 (f4 c5 c6) (f18 c_0))) c_1) (f21 (f9 c_0) c_1)) )(or (p22 c5 (f11 c_0)) (p12 (f17 c_0)) (not (p12 (f24 c_0))) (not (p22 c_2 (f4 c8 c6))) (p12 (f23 c_0)) (not (p22 c15 c_2)) (= (f21 (f21 (f2 (f3 c_0 c6)) (f4 (f4 c5 c6) (f18 c_0))) c_2) (f21 (f9 c_0) c_2)) )(or (p22 c5 (f11 c_1)) (p12 (f17 c_1)) (not (p12 (f24 c_1))) (not (p22 c_0 (f4 c8 c6))) (p12 (f23 c_1)) (not (p22 c15 c_0)) (= (f21 (f21 (f2 (f3 c_1 c6)) (f4 (f4 c5 c6) (f18 c_1))) c_0) (f21 (f9 c_1) c_0)) )(or (p22 c5 (f11 c_1)) (p12 (f17 c_1)) (not (p12 (f24 c_1))) (not (p22 c_1 (f4 c8 c6))) (p12 (f23 c_1)) (not (p22 c15 c_1)) (= (f21 (f21 (f2 (f3 c_1 c6)) (f4 (f4 c5 c6) (f18 c_1))) c_1) (f21 (f9 c_1) c_1)) )(or (p22 c5 (f11 c_1)) (p12 (f17 c_1)) (not (p12 (f24 c_1))) (not (p22 c_2 (f4 c8 c6))) (p12 (f23 c_1)) (not (p22 c15 c_2)) (= (f21 (f21 (f2 (f3 c_1 c6)) (f4 (f4 c5 c6) (f18 c_1))) c_2) (f21 (f9 c_1) c_2)) )(or (p22 c5 (f11 c_2)) (p12 (f17 c_2)) (not (p12 (f24 c_2))) (not (p22 c_0 (f4 c8 c6))) (p12 (f23 c_2)) (not (p22 c15 c_0)) (= (f21 (f21 (f2 (f3 c_2 c6)) (f4 (f4 c5 c6) (f18 c_2))) c_0) (f21 (f9 c_2) c_0)) )(or (p22 c5 (f11 c_2)) (p12 (f17 c_2)) (not (p12 (f24 c_2))) (not (p22 c_1 (f4 c8 c6))) (p12 (f23 c_2)) (not (p22 c15 c_1)) (= (f21 (f21 (f2 (f3 c_2 c6)) (f4 (f4 c5 c6) (f18 c_2))) c_1) (f21 (f9 c_2) c_1)) )(or (p22 c5 (f11 c_2)) (p12 (f17 c_2)) (not (p12 (f24 c_2))) (not (p22 c_2 (f4 c8 c6))) (p12 (f23 c_2)) (not (p22 c15 c_2)) (= (f21 (f21 (f2 (f3 c_2 c6)) (f4 (f4 c5 c6) (f18 c_2))) c_2) (f21 (f9 c_2) c_2)) )(= (f1 (f7 c_0)) (f3 (f4 c8 c6) c6)) (= (f1 (f7 c_1)) (f3 (f4 c8 c6) c6)) (= (f1 (f7 c_2)) (f3 (f4 c8 c6) c6)) (or (p12 (f17 c_0)) (not (p12 (f24 c_0))) (= (f21 (f7 (f3 c_0 c6)) c_0) (f21 (f7 c_0) c_0)) (not (p22 c_0 (f4 c8 c6))) (not (p22 c15 c_0)) (p12 (f23 c_0)) )(or (p12 (f17 c_0)) (not (p12 (f24 c_0))) (= (f21 (f7 (f3 c_0 c6)) c_1) (f21 (f7 c_0) c_1)) (not (p22 c_1 (f4 c8 c6))) (not (p22 c15 c_1)) (p12 (f23 c_0)) )(or (p12 (f17 c_0)) (not (p12 (f24 c_0))) (= (f21 (f7 (f3 c_0 c6)) c_2) (f21 (f7 c_0) c_2)) (not (p22 c_2 (f4 c8 c6))) (not (p22 c15 c_2)) (p12 (f23 c_0)) )(or (p12 (f17 c_1)) (not (p12 (f24 c_1))) (= (f21 (f7 (f3 c_1 c6)) c_0) (f21 (f7 c_1) c_0)) (not (p22 c_0 (f4 c8 c6))) (not (p22 c15 c_0)) (p12 (f23 c_1)) )(or (p12 (f17 c_1)) (not (p12 (f24 c_1))) (= (f21 (f7 (f3 c_1 c6)) c_1) (f21 (f7 c_1) c_1)) (not (p22 c_1 (f4 c8 c6))) (not (p22 c15 c_1)) (p12 (f23 c_1)) )(or (p12 (f17 c_1)) (not (p12 (f24 c_1))) (= (f21 (f7 (f3 c_1 c6)) c_2) (f21 (f7 c_1) c_2)) (not (p22 c_2 (f4 c8 c6))) (not (p22 c15 c_2)) (p12 (f23 c_1)) )(or (p12 (f17 c_2)) (not (p12 (f24 c_2))) (= (f21 (f7 (f3 c_2 c6)) c_0) (f21 (f7 c_2) c_0)) (not (p22 c_0 (f4 c8 c6))) (not (p22 c15 c_0)) (p12 (f23 c_2)) )(or (p12 (f17 c_2)) (not (p12 (f24 c_2))) (= (f21 (f7 (f3 c_2 c6)) c_1) (f21 (f7 c_2) c_1)) (not (p22 c_1 (f4 c8 c6))) (not (p22 c15 c_1)) (p12 (f23 c_2)) )(or (p12 (f17 c_2)) (not (p12 (f24 c_2))) (= (f21 (f7 (f3 c_2 c6)) c_2) (f21 (f7 c_2) c_2)) (not (p22 c_2 (f4 c8 c6))) (not (p22 c15 c_2)) (p12 (f23 c_2)) )(or (p12 (f23 c_0)) (p12 (f17 c_0)) (p12 (f20 (f3 c_0 c6))) (p12 (f24 c_0)) (not (p12 (f20 c_0))) )(or (p12 (f23 c_1)) (p12 (f17 c_1)) (p12 (f20 (f3 c_1 c6))) (p12 (f24 c_1)) (not (p12 (f20 c_1))) )(or (p12 (f23 c_2)) (p12 (f17 c_2)) (p12 (f20 (f3 c_2 c6))) (p12 (f24 c_2)) (not (p12 (f20 c_2))) )(or (p22 c5 (f11 c_0)) (p12 (f23 c_0)) (not (p12 (f24 c_0))) (p12 (f17 c_0)) (= (f11 (f3 c_0 c6)) (f3 (f11 c_0) c6)) )(or (p22 c5 (f11 c_1)) (p12 (f23 c_1)) (not (p12 (f24 c_1))) (p12 (f17 c_1)) (= (f11 (f3 c_1 c6)) (f3 (f11 c_1) c6)) )(or (p22 c5 (f11 c_2)) (p12 (f23 c_2)) (not (p12 (f24 c_2))) (p12 (f17 c_2)) (= (f11 (f3 c_2 c6)) (f3 (f11 c_2) c6)) )(or (not (p12 c_0)) (p12 c_0) (not (p12 (f43 c_0 c_0))) )(or (not (p12 c_0)) (p12 c_1) (not (p12 (f43 c_0 c_1))) )(or (not (p12 c_0)) (p12 c_2) (not (p12 (f43 c_0 c_2))) )(or (not (p12 c_1)) (p12 c_0) (not (p12 (f43 c_1 c_0))) )(or (not (p12 c_1)) (p12 c_1) (not (p12 (f43 c_1 c_1))) )(or (not (p12 c_1)) (p12 c_2) (not (p12 (f43 c_1 c_2))) )(or (not (p12 c_2)) (p12 c_0) (not (p12 (f43 c_2 c_0))) )(or (not (p12 c_2)) (p12 c_1) (not (p12 (f43 c_2 c_1))) )(or (not (p12 c_2)) (p12 c_2) (not (p12 (f43 c_2 c_2))) )(or (not (p12 (f23 c_0))) (p12 (f24 c_0)) (p22 (f11 c_0) c15) (p12 (f17 c_0)) (= (f16 (f3 c_0 c6)) (f25 (f3 (f16 c_0) c6) c5)) )(or (not (p12 (f23 c_1))) (p12 (f24 c_1)) (p22 (f11 c_1) c15) (p12 (f17 c_1)) (= (f16 (f3 c_1 c6)) (f25 (f3 (f16 c_1) c6) c5)) )(or (not (p12 (f23 c_2))) (p12 (f24 c_2)) (p22 (f11 c_2) c15) (p12 (f17 c_2)) (= (f16 (f3 c_2 c6)) (f25 (f3 (f16 c_2) c6) c5)) )(or (not (p22 c_0 c_0)) (p22 (f3 c_0 c6) (f3 c_0 c6)) )(or (not (p22 c_0 c_1)) (p22 (f3 c_0 c6) (f3 c_1 c6)) )(or (not (p22 c_0 c_2)) (p22 (f3 c_0 c6) (f3 c_2 c6)) )(or (not (p22 c_1 c_0)) (p22 (f3 c_1 c6) (f3 c_0 c6)) )(or (not (p22 c_1 c_1)) (p22 (f3 c_1 c6) (f3 c_1 c6)) )(or (not (p22 c_1 c_2)) (p22 (f3 c_1 c6) (f3 c_2 c6)) )(or (not (p22 c_2 c_0)) (p22 (f3 c_2 c6) (f3 c_0 c6)) )(or (not (p22 c_2 c_1)) (p22 (f3 c_2 c6) (f3 c_1 c6)) )(or (not (p22 c_2 c_2)) (p22 (f3 c_2 c6) (f3 c_2 c6)) )(= (f21 (f40 c_0) c_0) (f40 (f21 c_0 c_0))) (= (f21 (f40 c_0) c_1) (f40 (f21 c_0 c_1))) (= (f21 (f40 c_0) c_2) (f40 (f21 c_0 c_2))) (= (f21 (f40 c_1) c_0) (f40 (f21 c_1 c_0))) (= (f21 (f40 c_1) c_1) (f40 (f21 c_1 c_1))) (= (f21 (f40 c_1) c_2) (f40 (f21 c_1 c_2))) (= (f21 (f40 c_2) c_0) (f40 (f21 c_2 c_0))) (= (f21 (f40 c_2) c_1) (f40 (f21 c_2 c_1))) (= (f21 (f40 c_2) c_2) (f40 (f21 c_2 c_2))) (or (not (p12 (f21 (f21 (f2 (f3 c_0 c6)) c_0) c_0))) (not (p22 c_0 (f4 c5 c6))) (not (p22 c15 c_0)) (not (p22 c_0 (f4 c8 c6))) (not (p22 c15 c_0)) (not (p12 (f17 c_0))) )(or (not (p12 (f21 (f21 (f2 (f3 c_0 c6)) c_0) c_1))) (not (p22 c_0 (f4 c5 c6))) (not (p22 c15 c_1)) (not (p22 c_1 (f4 c8 c6))) (not (p22 c15 c_0)) (not (p12 (f17 c_0))) )(or (not (p12 (f21 (f21 (f2 (f3 c_0 c6)) c_0) c_2))) (not (p22 c_0 (f4 c5 c6))) (not (p22 c15 c_2)) (not (p22 c_2 (f4 c8 c6))) (not (p22 c15 c_0)) (not (p12 (f17 c_0))) )(or (not (p12 (f21 (f21 (f2 (f3 c_0 c6)) c_1) c_0))) (not (p22 c_1 (f4 c5 c6))) (not (p22 c15 c_0)) (not (p22 c_0 (f4 c8 c6))) (not (p22 c15 c_1)) (not (p12 (f17 c_0))) )(or (not (p12 (f21 (f21 (f2 (f3 c_0 c6)) c_1) c_1))) (not (p22 c_1 (f4 c5 c6))) (not (p22 c15 c_1)) (not (p22 c_1 (f4 c8 c6))) (not (p22 c15 c_1)) (not (p12 (f17 c_0))) )(or (not (p12 (f21 (f21 (f2 (f3 c_0 c6)) c_1) c_2))) (not (p22 c_1 (f4 c5 c6))) (not (p22 c15 c_2)) (not (p22 c_2 (f4 c8 c6))) (not (p22 c15 c_1)) (not (p12 (f17 c_0))) )(or (not (p12 (f21 (f21 (f2 (f3 c_0 c6)) c_2) c_0))) (not (p22 c_2 (f4 c5 c6))) (not (p22 c15 c_0)) (not (p22 c_0 (f4 c8 c6))) (not (p22 c15 c_2)) (not (p12 (f17 c_0))) )(or (not (p12 (f21 (f21 (f2 (f3 c_0 c6)) c_2) c_1))) (not (p22 c_2 (f4 c5 c6))) (not (p22 c15 c_1)) (not (p22 c_1 (f4 c8 c6))) (not (p22 c15 c_2)) (not (p12 (f17 c_0))) )(or (not (p12 (f21 (f21 (f2 (f3 c_0 c6)) c_2) c_2))) (not (p22 c_2 (f4 c5 c6))) (not (p22 c15 c_2)) (not (p22 c_2 (f4 c8 c6))) (not (p22 c15 c_2)) (not (p12 (f17 c_0))) )(or (not (p12 (f21 (f21 (f2 (f3 c_1 c6)) c_0) c_0))) (not (p22 c_0 (f4 c5 c6))) (not (p22 c15 c_0)) (not (p22 c_0 (f4 c8 c6))) (not (p22 c15 c_0)) (not (p12 (f17 c_1))) )(or (not (p12 (f21 (f21 (f2 (f3 c_1 c6)) c_0) c_1))) (not (p22 c_0 (f4 c5 c6))) (not (p22 c15 c_1)) (not (p22 c_1 (f4 c8 c6))) (not (p22 c15 c_0)) (not (p12 (f17 c_1))) )(or (not (p12 (f21 (f21 (f2 (f3 c_1 c6)) c_0) c_2))) (not (p22 c_0 (f4 c5 c6))) (not (p22 c15 c_2)) (not (p22 c_2 (f4 c8 c6))) (not (p22 c15 c_0)) (not (p12 (f17 c_1))) )(or (not (p12 (f21 (f21 (f2 (f3 c_1 c6)) c_1) c_0))) (not (p22 c_1 (f4 c5 c6))) (not (p22 c15 c_0)) (not (p22 c_0 (f4 c8 c6))) (not (p22 c15 c_1)) (not (p12 (f17 c_1))) )(or (not (p12 (f21 (f21 (f2 (f3 c_1 c6)) c_1) c_1))) (not (p22 c_1 (f4 c5 c6))) (not (p22 c15 c_1)) (not (p22 c_1 (f4 c8 c6))) (not (p22 c15 c_1)) (not (p12 (f17 c_1))) )(or (not (p12 (f21 (f21 (f2 (f3 c_1 c6)) c_1) c_2))) (not (p22 c_1 (f4 c5 c6))) (not (p22 c15 c_2)) (not (p22 c_2 (f4 c8 c6))) (not (p22 c15 c_1)) (not (p12 (f17 c_1))) )(or (not (p12 (f21 (f21 (f2 (f3 c_1 c6)) c_2) c_0))) (not (p22 c_2 (f4 c5 c6))) (not (p22 c15 c_0)) (not (p22 c_0 (f4 c8 c6))) (not (p22 c15 c_2)) (not (p12 (f17 c_1))) )(or (not (p12 (f21 (f21 (f2 (f3 c_1 c6)) c_2) c_1))) (not (p22 c_2 (f4 c5 c6))) (not (p22 c15 c_1)) (not (p22 c_1 (f4 c8 c6))) (not (p22 c15 c_2)) (not (p12 (f17 c_1))) )(or (not (p12 (f21 (f21 (f2 (f3 c_1 c6)) c_2) c_2))) (not (p22 c_2 (f4 c5 c6))) (not (p22 c15 c_2)) (not (p22 c_2 (f4 c8 c6))) (not (p22 c15 c_2)) (not (p12 (f17 c_1))) )(or (not (p12 (f21 (f21 (f2 (f3 c_2 c6)) c_0) c_0))) (not (p22 c_0 (f4 c5 c6))) (not (p22 c15 c_0)) (not (p22 c_0 (f4 c8 c6))) (not (p22 c15 c_0)) (not (p12 (f17 c_2))) )(or (not (p12 (f21 (f21 (f2 (f3 c_2 c6)) c_0) c_1))) (not (p22 c_0 (f4 c5 c6))) (not (p22 c15 c_1)) (not (p22 c_1 (f4 c8 c6))) (not (p22 c15 c_0)) (not (p12 (f17 c_2))) )(or (not (p12 (f21 (f21 (f2 (f3 c_2 c6)) c_0) c_2))) (not (p22 c_0 (f4 c5 c6))) (not (p22 c15 c_2)) (not (p22 c_2 (f4 c8 c6))) (not (p22 c15 c_0)) (not (p12 (f17 c_2))) )(or (not (p12 (f21 (f21 (f2 (f3 c_2 c6)) c_1) c_0))) (not (p22 c_1 (f4 c5 c6))) (not (p22 c15 c_0)) (not (p22 c_0 (f4 c8 c6))) (not (p22 c15 c_1)) (not (p12 (f17 c_2))) )(or (not (p12 (f21 (f21 (f2 (f3 c_2 c6)) c_1) c_1))) (not (p22 c_1 (f4 c5 c6))) (not (p22 c15 c_1)) (not (p22 c_1 (f4 c8 c6))) (not (p22 c15 c_1)) (not (p12 (f17 c_2))) )(or (not (p12 (f21 (f21 (f2 (f3 c_2 c6)) c_1) c_2))) (not (p22 c_1 (f4 c5 c6))) (not (p22 c15 c_2)) (not (p22 c_2 (f4 c8 c6))) (not (p22 c15 c_1)) (not (p12 (f17 c_2))) )(or (not (p12 (f21 (f21 (f2 (f3 c_2 c6)) c_2) c_0))) (not (p22 c_2 (f4 c5 c6))) (not (p22 c15 c_0)) (not (p22 c_0 (f4 c8 c6))) (not (p22 c15 c_2)) (not (p12 (f17 c_2))) )(or (not (p12 (f21 (f21 (f2 (f3 c_2 c6)) c_2) c_1))) (not (p22 c_2 (f4 c5 c6))) (not (p22 c15 c_1)) (not (p22 c_1 (f4 c8 c6))) (not (p22 c15 c_2)) (not (p12 (f17 c_2))) )(or (not (p12 (f21 (f21 (f2 (f3 c_2 c6)) c_2) c_2))) (not (p22 c_2 (f4 c5 c6))) (not (p22 c15 c_2)) (not (p22 c_2 (f4 c8 c6))) (not (p22 c15 c_2)) (not (p12 (f17 c_2))) )(or (= (f21 (f30 c_0 c_0) c_0) (f21 c_0 c_0)) (p22 (f33 c_0) c_0) )(or (= (f21 (f30 c_0 c_0) c_1) (f21 c_0 c_1)) (p22 (f33 c_0) c_1) )(or (= (f21 (f30 c_0 c_0) c_2) (f21 c_0 c_2)) (p22 (f33 c_0) c_2) )(or (= (f21 (f30 c_0 c_1) c_0) (f21 c_0 c_0)) (p22 (f33 c_0) c_0) )(or (= (f21 (f30 c_0 c_1) c_1) (f21 c_0 c_1)) (p22 (f33 c_0) c_1) )(or (= (f21 (f30 c_0 c_1) c_2) (f21 c_0 c_2)) (p22 (f33 c_0) c_2) )(or (= (f21 (f30 c_0 c_2) c_0) (f21 c_0 c_0)) (p22 (f33 c_0) c_0) )(or (= (f21 (f30 c_0 c_2) c_1) (f21 c_0 c_1)) (p22 (f33 c_0) c_1) )(or (= (f21 (f30 c_0 c_2) c_2) (f21 c_0 c_2)) (p22 (f33 c_0) c_2) )(or (= (f21 (f30 c_1 c_0) c_0) (f21 c_1 c_0)) (p22 (f33 c_1) c_0) )(or (= (f21 (f30 c_1 c_0) c_1) (f21 c_1 c_1)) (p22 (f33 c_1) c_1) )(or (= (f21 (f30 c_1 c_0) c_2) (f21 c_1 c_2)) (p22 (f33 c_1) c_2) )(or (= (f21 (f30 c_1 c_1) c_0) (f21 c_1 c_0)) (p22 (f33 c_1) c_0) )(or (= (f21 (f30 c_1 c_1) c_1) (f21 c_1 c_1)) (p22 (f33 c_1) c_1) )(or (= (f21 (f30 c_1 c_1) c_2) (f21 c_1 c_2)) (p22 (f33 c_1) c_2) )(or (= (f21 (f30 c_1 c_2) c_0) (f21 c_1 c_0)) (p22 (f33 c_1) c_0) )(or (= (f21 (f30 c_1 c_2) c_1) (f21 c_1 c_1)) (p22 (f33 c_1) c_1) )(or (= (f21 (f30 c_1 c_2) c_2) (f21 c_1 c_2)) (p22 (f33 c_1) c_2) )(or (= (f21 (f30 c_2 c_0) c_0) (f21 c_2 c_0)) (p22 (f33 c_2) c_0) )(or (= (f21 (f30 c_2 c_0) c_1) (f21 c_2 c_1)) (p22 (f33 c_2) c_1) )(or (= (f21 (f30 c_2 c_0) c_2) (f21 c_2 c_2)) (p22 (f33 c_2) c_2) )(or (= (f21 (f30 c_2 c_1) c_0) (f21 c_2 c_0)) (p22 (f33 c_2) c_0) )(or (= (f21 (f30 c_2 c_1) c_1) (f21 c_2 c_1)) (p22 (f33 c_2) c_1) )(or (= (f21 (f30 c_2 c_1) c_2) (f21 c_2 c_2)) (p22 (f33 c_2) c_2) )(or (= (f21 (f30 c_2 c_2) c_0) (f21 c_2 c_0)) (p22 (f33 c_2) c_0) )(or (= (f21 (f30 c_2 c_2) c_1) (f21 c_2 c_1)) (p22 (f33 c_2) c_1) )(or (= (f21 (f30 c_2 c_2) c_2) (f21 c_2 c_2)) (p22 (f33 c_2) c_2) )(or (p12 (f23 c_0)) (= (f18 (f3 c_0 c6)) (f25 (f3 (f18 c_0) c6) c5)) (p22 c5 (f11 c_0)) (not (p12 (f24 c_0))) (p12 (f17 c_0)) )(or (p12 (f23 c_1)) (= (f18 (f3 c_1 c6)) (f25 (f3 (f18 c_1) c6) c5)) (p22 c5 (f11 c_1)) (not (p12 (f24 c_1))) (p12 (f17 c_1)) )(or (p12 (f23 c_2)) (= (f18 (f3 c_2 c6)) (f25 (f3 (f18 c_2) c6) c5)) (p22 c5 (f11 c_2)) (not (p12 (f24 c_2))) (p12 (f17 c_2)) )(or (= c_0 (f3 (f27 c_0) c6)) (= c_0 c15) )(or (= c_1 (f3 (f27 c_1) c6)) (= c_1 c15) )(or (= c_2 (f3 (f27 c_2) c6)) (= c_2 c15) )(or (= (f11 c_0) c15) (not (p12 (f14 c_0))) )(or (= (f11 c_1) c15) (not (p12 (f14 c_1))) )(or (= (f11 c_2) c15) (not (p12 (f14 c_2))) )(= (f1 (f9 c_0)) (f3 (f4 c8 c6) c6)) (= (f1 (f9 c_1)) (f3 (f4 c8 c6) c6)) (= (f1 (f9 c_2)) (f3 (f4 c8 c6) c6)) (or (p12 (f46 c_0 c_0)) (not (p22 c_0 c_0)) )(or (p12 (f46 c_0 c_1)) (not (p22 c_0 c_1)) )(or (p12 (f46 c_0 c_2)) (not (p22 c_0 c_2)) )(or (p12 (f46 c_1 c_0)) (not (p22 c_1 c_0)) )(or (p12 (f46 c_1 c_1)) (not (p22 c_1 c_1)) )(or (p12 (f46 c_1 c_2)) (not (p22 c_1 c_2)) )(or (p12 (f46 c_2 c_0)) (not (p22 c_2 c_0)) )(or (p12 (f46 c_2 c_1)) (not (p22 c_2 c_1)) )(or (p12 (f46 c_2 c_2)) (not (p22 c_2 c_2)) )(or (p22 (f3 c_0 c6) c_0) (= c_0 c_0) (not (p22 c_0 c_0)) )(or (p22 (f3 c_0 c6) c_1) (= c_1 c_0) (not (p22 c_0 c_1)) )(or (p22 (f3 c_0 c6) c_2) (= c_2 c_0) (not (p22 c_0 c_2)) )(or (p22 (f3 c_1 c6) c_0) (= c_0 c_1) (not (p22 c_1 c_0)) )(or (p22 (f3 c_1 c6) c_1) (= c_1 c_1) (not (p22 c_1 c_1)) )(or (p22 (f3 c_1 c6) c_2) (= c_2 c_1) (not (p22 c_1 c_2)) )(or (p22 (f3 c_2 c6) c_0) (= c_0 c_2) (not (p22 c_2 c_0)) )(or (p22 (f3 c_2 c6) c_1) (= c_1 c_2) (not (p22 c_2 c_1)) )(or (p22 (f3 c_2 c6) c_2) (= c_2 c_2) (not (p22 c_2 c_2)) )(or (p12 c_0) (p12 (f38 c_0 c_0)) (p12 c_0) )(or (p12 c_0) (p12 (f38 c_0 c_1)) (p12 c_1) )(or (p12 c_0) (p12 (f38 c_0 c_2)) (p12 c_2) )(or (p12 c_1) (p12 (f38 c_1 c_0)) (p12 c_0) )(or (p12 c_1) (p12 (f38 c_1 c_1)) (p12 c_1) )(or (p12 c_1) (p12 (f38 c_1 c_2)) (p12 c_2) )(or (p12 c_2) (p12 (f38 c_2 c_0)) (p12 c_0) )(or (p12 c_2) (p12 (f38 c_2 c_1)) (p12 c_1) )(or (p12 c_2) (p12 (f38 c_2 c_2)) (p12 c_2) )(or (p12 (f34 c_0 c_0)) (not (p12 c_0)) (not (p12 c_0)) )(or (p12 (f34 c_0 c_1)) (not (p12 c_0)) (not (p12 c_1)) )(or (p12 (f34 c_0 c_2)) (not (p12 c_0)) (not (p12 c_2)) )(or (p12 (f34 c_1 c_0)) (not (p12 c_1)) (not (p12 c_0)) )(or (p12 (f34 c_1 c_1)) (not (p12 c_1)) (not (p12 c_1)) )(or (p12 (f34 c_1 c_2)) (not (p12 c_1)) (not (p12 c_2)) )(or (p12 (f34 c_2 c_0)) (not (p12 c_2)) (not (p12 c_0)) )(or (p12 (f34 c_2 c_1)) (not (p12 c_2)) (not (p12 c_1)) )(or (p12 (f34 c_2 c_2)) (not (p12 c_2)) (not (p12 c_2)) )(= (f1 (f31 c_0 c_0 c_0)) (f4 c_0 (f3 c_0 c6))) (= (f1 (f31 c_0 c_0 c_1)) (f4 c_1 (f3 c_0 c6))) (= (f1 (f31 c_0 c_0 c_2)) (f4 c_2 (f3 c_0 c6))) (= (f1 (f31 c_0 c_1 c_0)) (f4 c_0 (f3 c_1 c6))) (= (f1 (f31 c_0 c_1 c_1)) (f4 c_1 (f3 c_1 c6))) (= (f1 (f31 c_0 c_1 c_2)) (f4 c_2 (f3 c_1 c6))) (= (f1 (f31 c_0 c_2 c_0)) (f4 c_0 (f3 c_2 c6))) (= (f1 (f31 c_0 c_2 c_1)) (f4 c_1 (f3 c_2 c6))) (= (f1 (f31 c_0 c_2 c_2)) (f4 c_2 (f3 c_2 c6))) (= (f1 (f31 c_1 c_0 c_0)) (f4 c_0 (f3 c_0 c6))) (= (f1 (f31 c_1 c_0 c_1)) (f4 c_1 (f3 c_0 c6))) (= (f1 (f31 c_1 c_0 c_2)) (f4 c_2 (f3 c_0 c6))) (= (f1 (f31 c_1 c_1 c_0)) (f4 c_0 (f3 c_1 c6))) (= (f1 (f31 c_1 c_1 c_1)) (f4 c_1 (f3 c_1 c6))) (= (f1 (f31 c_1 c_1 c_2)) (f4 c_2 (f3 c_1 c6))) (= (f1 (f31 c_1 c_2 c_0)) (f4 c_0 (f3 c_2 c6))) (= (f1 (f31 c_1 c_2 c_1)) (f4 c_1 (f3 c_2 c6))) (= (f1 (f31 c_1 c_2 c_2)) (f4 c_2 (f3 c_2 c6))) (= (f1 (f31 c_2 c_0 c_0)) (f4 c_0 (f3 c_0 c6))) (= (f1 (f31 c_2 c_0 c_1)) (f4 c_1 (f3 c_0 c6))) (= (f1 (f31 c_2 c_0 c_2)) (f4 c_2 (f3 c_0 c6))) (= (f1 (f31 c_2 c_1 c_0)) (f4 c_0 (f3 c_1 c6))) (= (f1 (f31 c_2 c_1 c_1)) (f4 c_1 (f3 c_1 c6))) (= (f1 (f31 c_2 c_1 c_2)) (f4 c_2 (f3 c_1 c6))) (= (f1 (f31 c_2 c_2 c_0)) (f4 c_0 (f3 c_2 c6))) (= (f1 (f31 c_2 c_2 c_1)) (f4 c_1 (f3 c_2 c6))) (= (f1 (f31 c_2 c_2 c_2)) (f4 c_2 (f3 c_2 c6))) (or (not (p12 (f17 c_0))) (= (f11 (f3 c_0 c6)) c15) )(or (not (p12 (f17 c_1))) (= (f11 (f3 c_1 c6)) c15) )(or (not (p12 (f17 c_2))) (= (f11 (f3 c_2 c6)) c15) )(or (= (f16 (f3 c_0 c6)) (f16 c_0)) (not (p12 (f24 c_0))) (not (p12 (f23 c_0))) (p12 (f17 c_0)) (not (p22 (f11 c_0) c15)) )(or (= (f16 (f3 c_1 c6)) (f16 c_1)) (not (p12 (f24 c_1))) (not (p12 (f23 c_1))) (p12 (f17 c_1)) (not (p22 (f11 c_1) c15)) )(or (= (f16 (f3 c_2 c6)) (f16 c_2)) (not (p12 (f24 c_2))) (not (p12 (f23 c_2))) (p12 (f17 c_2)) (not (p22 (f11 c_2) c15)) )(or (not (p22 c_0 (f4 c8 c6))) (p12 (f17 c_0)) (not (p22 c15 c_0)) (p12 (f24 c_0)) (= (f21 (f7 (f3 c_0 c6)) c_0) (f21 (f7 c_0) c_0)) (p12 (f23 c_0)) )(or (not (p22 c_0 (f4 c8 c6))) (p12 (f17 c_1)) (not (p22 c15 c_0)) (p12 (f24 c_1)) (= (f21 (f7 (f3 c_1 c6)) c_0) (f21 (f7 c_1) c_0)) (p12 (f23 c_1)) )(or (not (p22 c_0 (f4 c8 c6))) (p12 (f17 c_2)) (not (p22 c15 c_0)) (p12 (f24 c_2)) (= (f21 (f7 (f3 c_2 c6)) c_0) (f21 (f7 c_2) c_0)) (p12 (f23 c_2)) )(or (not (p22 c_1 (f4 c8 c6))) (p12 (f17 c_0)) (not (p22 c15 c_1)) (p12 (f24 c_0)) (= (f21 (f7 (f3 c_0 c6)) c_1) (f21 (f7 c_0) c_1)) (p12 (f23 c_0)) )(or (not (p22 c_1 (f4 c8 c6))) (p12 (f17 c_1)) (not (p22 c15 c_1)) (p12 (f24 c_1)) (= (f21 (f7 (f3 c_1 c6)) c_1) (f21 (f7 c_1) c_1)) (p12 (f23 c_1)) )(or (not (p22 c_1 (f4 c8 c6))) (p12 (f17 c_2)) (not (p22 c15 c_1)) (p12 (f24 c_2)) (= (f21 (f7 (f3 c_2 c6)) c_1) (f21 (f7 c_2) c_1)) (p12 (f23 c_2)) )(or (not (p22 c_2 (f4 c8 c6))) (p12 (f17 c_0)) (not (p22 c15 c_2)) (p12 (f24 c_0)) (= (f21 (f7 (f3 c_0 c6)) c_2) (f21 (f7 c_0) c_2)) (p12 (f23 c_0)) )(or (not (p22 c_2 (f4 c8 c6))) (p12 (f17 c_1)) (not (p22 c15 c_2)) (p12 (f24 c_1)) (= (f21 (f7 (f3 c_1 c6)) c_2) (f21 (f7 c_1) c_2)) (p12 (f23 c_1)) )(or (not (p22 c_2 (f4 c8 c6))) (p12 (f17 c_2)) (not (p22 c15 c_2)) (p12 (f24 c_2)) (= (f21 (f7 (f3 c_2 c6)) c_2) (f21 (f7 c_2) c_2)) (p12 (f23 c_2)) )(= (f3 c15 c_0) c_0) (= (f3 c15 c_1) c_1) (= (f3 c15 c_2) c_2) (or (not (p12 (f23 c_0))) (not (p12 (f24 c_0))) (p12 (f17 c_0)) (= (f18 (f3 c_0 c6)) (f25 (f3 (f18 c_0) c6) c5)) )(or (not (p12 (f23 c_1))) (not (p12 (f24 c_1))) (p12 (f17 c_1)) (= (f18 (f3 c_1 c6)) (f25 (f3 (f18 c_1) c6) c5)) )(or (not (p12 (f23 c_2))) (not (p12 (f24 c_2))) (p12 (f17 c_2)) (= (f18 (f3 c_2 c6)) (f25 (f3 (f18 c_2) c6) c5)) )(p12 (f13 c49)) (or (not (p12 (f38 c_0 c_0))) (not (p12 c_0)) )(or (not (p12 (f38 c_0 c_1))) (not (p12 c_1)) )(or (not (p12 (f38 c_0 c_2))) (not (p12 c_2)) )(or (not (p12 (f38 c_1 c_0))) (not (p12 c_0)) )(or (not (p12 (f38 c_1 c_1))) (not (p12 c_1)) )(or (not (p12 (f38 c_1 c_2))) (not (p12 c_2)) )(or (not (p12 (f38 c_2 c_0))) (not (p12 c_0)) )(or (not (p12 (f38 c_2 c_1))) (not (p12 c_1)) )(or (not (p12 (f38 c_2 c_2))) (not (p12 c_2)) )(= (f21 (f39 c_0 c_0) c_0) (f39 (f21 c_0 c_0) (f21 c_0 c_0))) (= (f21 (f39 c_0 c_0) c_1) (f39 (f21 c_0 c_1) (f21 c_0 c_1))) (= (f21 (f39 c_0 c_0) c_2) (f39 (f21 c_0 c_2) (f21 c_0 c_2))) (= (f21 (f39 c_0 c_1) c_0) (f39 (f21 c_0 c_0) (f21 c_1 c_0))) (= (f21 (f39 c_0 c_1) c_1) (f39 (f21 c_0 c_1) (f21 c_1 c_1))) (= (f21 (f39 c_0 c_1) c_2) (f39 (f21 c_0 c_2) (f21 c_1 c_2))) (= (f21 (f39 c_0 c_2) c_0) (f39 (f21 c_0 c_0) (f21 c_2 c_0))) (= (f21 (f39 c_0 c_2) c_1) (f39 (f21 c_0 c_1) (f21 c_2 c_1))) (= (f21 (f39 c_0 c_2) c_2) (f39 (f21 c_0 c_2) (f21 c_2 c_2))) (= (f21 (f39 c_1 c_0) c_0) (f39 (f21 c_1 c_0) (f21 c_0 c_0))) (= (f21 (f39 c_1 c_0) c_1) (f39 (f21 c_1 c_1) (f21 c_0 c_1))) (= (f21 (f39 c_1 c_0) c_2) (f39 (f21 c_1 c_2) (f21 c_0 c_2))) (= (f21 (f39 c_1 c_1) c_0) (f39 (f21 c_1 c_0) (f21 c_1 c_0))) (= (f21 (f39 c_1 c_1) c_1) (f39 (f21 c_1 c_1) (f21 c_1 c_1))) (= (f21 (f39 c_1 c_1) c_2) (f39 (f21 c_1 c_2) (f21 c_1 c_2))) (= (f21 (f39 c_1 c_2) c_0) (f39 (f21 c_1 c_0) (f21 c_2 c_0))) (= (f21 (f39 c_1 c_2) c_1) (f39 (f21 c_1 c_1) (f21 c_2 c_1))) (= (f21 (f39 c_1 c_2) c_2) (f39 (f21 c_1 c_2) (f21 c_2 c_2))) (= (f21 (f39 c_2 c_0) c_0) (f39 (f21 c_2 c_0) (f21 c_0 c_0))) (= (f21 (f39 c_2 c_0) c_1) (f39 (f21 c_2 c_1) (f21 c_0 c_1))) (= (f21 (f39 c_2 c_0) c_2) (f39 (f21 c_2 c_2) (f21 c_0 c_2))) (= (f21 (f39 c_2 c_1) c_0) (f39 (f21 c_2 c_0) (f21 c_1 c_0))) (= (f21 (f39 c_2 c_1) c_1) (f39 (f21 c_2 c_1) (f21 c_1 c_1))) (= (f21 (f39 c_2 c_1) c_2) (f39 (f21 c_2 c_2) (f21 c_1 c_2))) (= (f21 (f39 c_2 c_2) c_0) (f39 (f21 c_2 c_0) (f21 c_2 c_0))) (= (f21 (f39 c_2 c_2) c_1) (f39 (f21 c_2 c_1) (f21 c_2 c_1))) (= (f21 (f39 c_2 c_2) c_2) (f39 (f21 c_2 c_2) (f21 c_2 c_2))) (not (p12 (f17 c49))) (or (not (p22 c_0 (f4 c_0 c6))) (p22 c_0 c15) )(or (not (p22 c_1 (f4 c_1 c6))) (p22 c_1 c15) )(or (not (p22 c_2 (f4 c_2 c6))) (p22 c_2 c15) )(= (f21 (f36 c_0 c_0) c_0) (f36 (f21 c_0 c_0) (f21 c_0 c_0))) (= (f21 (f36 c_0 c_0) c_1) (f36 (f21 c_0 c_1) (f21 c_0 c_1))) (= (f21 (f36 c_0 c_0) c_2) (f36 (f21 c_0 c_2) (f21 c_0 c_2))) (= (f21 (f36 c_0 c_1) c_0) (f36 (f21 c_0 c_0) (f21 c_1 c_0))) (= (f21 (f36 c_0 c_1) c_1) (f36 (f21 c_0 c_1) (f21 c_1 c_1))) (= (f21 (f36 c_0 c_1) c_2) (f36 (f21 c_0 c_2) (f21 c_1 c_2))) (= (f21 (f36 c_0 c_2) c_0) (f36 (f21 c_0 c_0) (f21 c_2 c_0))) (= (f21 (f36 c_0 c_2) c_1) (f36 (f21 c_0 c_1) (f21 c_2 c_1))) (= (f21 (f36 c_0 c_2) c_2) (f36 (f21 c_0 c_2) (f21 c_2 c_2))) (= (f21 (f36 c_1 c_0) c_0) (f36 (f21 c_1 c_0) (f21 c_0 c_0))) (= (f21 (f36 c_1 c_0) c_1) (f36 (f21 c_1 c_1) (f21 c_0 c_1))) (= (f21 (f36 c_1 c_0) c_2) (f36 (f21 c_1 c_2) (f21 c_0 c_2))) (= (f21 (f36 c_1 c_1) c_0) (f36 (f21 c_1 c_0) (f21 c_1 c_0))) (= (f21 (f36 c_1 c_1) c_1) (f36 (f21 c_1 c_1) (f21 c_1 c_1))) (= (f21 (f36 c_1 c_1) c_2) (f36 (f21 c_1 c_2) (f21 c_1 c_2))) (= (f21 (f36 c_1 c_2) c_0) (f36 (f21 c_1 c_0) (f21 c_2 c_0))) (= (f21 (f36 c_1 c_2) c_1) (f36 (f21 c_1 c_1) (f21 c_2 c_1))) (= (f21 (f36 c_1 c_2) c_2) (f36 (f21 c_1 c_2) (f21 c_2 c_2))) (= (f21 (f36 c_2 c_0) c_0) (f36 (f21 c_2 c_0) (f21 c_0 c_0))) (= (f21 (f36 c_2 c_0) c_1) (f36 (f21 c_2 c_1) (f21 c_0 c_1))) (= (f21 (f36 c_2 c_0) c_2) (f36 (f21 c_2 c_2) (f21 c_0 c_2))) (= (f21 (f36 c_2 c_1) c_0) (f36 (f21 c_2 c_0) (f21 c_1 c_0))) (= (f21 (f36 c_2 c_1) c_1) (f36 (f21 c_2 c_1) (f21 c_1 c_1))) (= (f21 (f36 c_2 c_1) c_2) (f36 (f21 c_2 c_2) (f21 c_1 c_2))) (= (f21 (f36 c_2 c_2) c_0) (f36 (f21 c_2 c_0) (f21 c_2 c_0))) (= (f21 (f36 c_2 c_2) c_1) (f36 (f21 c_2 c_1) (f21 c_2 c_1))) (= (f21 (f36 c_2 c_2) c_2) (f36 (f21 c_2 c_2) (f21 c_2 c_2))) (or (p12 (f20 c_0)) (p12 (f17 c_0)) (not (p12 (f24 c_0))) (not (p12 (f20 (f3 c_0 c6)))) (p12 (f23 c_0)) )(or (p12 (f20 c_1)) (p12 (f17 c_1)) (not (p12 (f24 c_1))) (not (p12 (f20 (f3 c_1 c6)))) (p12 (f23 c_1)) )(or (p12 (f20 c_2)) (p12 (f17 c_2)) (not (p12 (f24 c_2))) (not (p12 (f20 (f3 c_2 c6)))) (p12 (f23 c_2)) )(or (p12 (f24 c_0)) (p12 (f17 c_0)) (= (f16 (f3 c_0 c6)) (f16 c_0)) (not (p22 (f11 c_0) c15)) (not (p12 (f23 c_0))) )(or (p12 (f24 c_1)) (p12 (f17 c_1)) (= (f16 (f3 c_1 c6)) (f16 c_1)) (not (p22 (f11 c_1) c15)) (not (p12 (f23 c_1))) )(or (p12 (f24 c_2)) (p12 (f17 c_2)) (= (f16 (f3 c_2 c6)) (f16 c_2)) (not (p22 (f11 c_2) c15)) (not (p12 (f23 c_2))) )(= (f1 (f2 c_0)) (f3 (f4 c5 c6) c6)) (= (f1 (f2 c_1)) (f3 (f4 c5 c6) c6)) (= (f1 (f2 c_2)) (f3 (f4 c5 c6) c6)) (or (p12 (f17 c_0)) (p12 (f24 c_0)) (not (p12 (f20 (f3 c_0 c6)))) (p12 (f23 c_0)) (p12 (f20 c_0)) )(or (p12 (f17 c_1)) (p12 (f24 c_1)) (not (p12 (f20 (f3 c_1 c6)))) (p12 (f23 c_1)) (p12 (f20 c_1)) )(or (p12 (f17 c_2)) (p12 (f24 c_2)) (not (p12 (f20 (f3 c_2 c6)))) (p12 (f23 c_2)) (p12 (f20 c_2)) )(or (not (p12 (f23 c_0))) (not (p12 (f19 (f3 c_0 c6)))) (not (p12 (f24 c_0))) (p12 (f17 c_0)) )(or (not (p12 (f23 c_1))) (not (p12 (f19 (f3 c_1 c6)))) (not (p12 (f24 c_1))) (p12 (f17 c_1)) )(or (not (p12 (f23 c_2))) (not (p12 (f19 (f3 c_2 c6)))) (not (p12 (f24 c_2))) (p12 (f17 c_2)) )(= (f1 (f30 c_0 c_0)) (f3 (f1 c_0) (f1 c_0))) (= (f1 (f30 c_0 c_1)) (f3 (f1 c_0) (f1 c_1))) (= (f1 (f30 c_0 c_2)) (f3 (f1 c_0) (f1 c_2))) (= (f1 (f30 c_1 c_0)) (f3 (f1 c_1) (f1 c_0))) (= (f1 (f30 c_1 c_1)) (f3 (f1 c_1) (f1 c_1))) (= (f1 (f30 c_1 c_2)) (f3 (f1 c_1) (f1 c_2))) (= (f1 (f30 c_2 c_0)) (f3 (f1 c_2) (f1 c_0))) (= (f1 (f30 c_2 c_1)) (f3 (f1 c_2) (f1 c_1))) (= (f1 (f30 c_2 c_2)) (f3 (f1 c_2) (f1 c_2))) (or (= (f16 (f3 c_0 c6)) c15) (not (p12 (f17 c_0))) )(or (= (f16 (f3 c_1 c6)) c15) (not (p12 (f17 c_1))) )(or (= (f16 (f3 c_2 c6)) c15) (not (p12 (f17 c_2))) )(or (p12 (f19 (f3 c_0 c6))) (not (p12 (f19 c_0))) (p12 (f17 c_0)) (p12 (f24 c_0)) )(or (p12 (f19 (f3 c_1 c6))) (not (p12 (f19 c_1))) (p12 (f17 c_1)) (p12 (f24 c_1)) )(or (p12 (f19 (f3 c_2 c6))) (not (p12 (f19 c_2))) (p12 (f17 c_2)) (p12 (f24 c_2)) )(or (= (f11 c_0) c5) (not (p12 (f13 c_0))) )(or (= (f11 c_1) c5) (not (p12 (f13 c_1))) )(or (= (f11 c_2) c5) (not (p12 (f13 c_2))) )(or (p12 (f24 c_0)) (p12 (f17 c_0)) (= (f18 (f3 c_0 c6)) (f18 c_0)) )(or (p12 (f24 c_1)) (p12 (f17 c_1)) (= (f18 (f3 c_1 c6)) (f18 c_1)) )(or (p12 (f24 c_2)) (p12 (f17 c_2)) (= (f18 (f3 c_2 c6)) (f18 c_2)) )(or (p12 (f43 c_0 c_0)) (p12 c_0) (p12 c_0) )(or (p12 (f43 c_0 c_1)) (p12 c_0) (p12 c_1) )(or (p12 (f43 c_0 c_2)) (p12 c_0) (p12 c_2) )(or (p12 (f43 c_1 c_0)) (p12 c_1) (p12 c_0) )(or (p12 (f43 c_1 c_1)) (p12 c_1) (p12 c_1) )(or (p12 (f43 c_1 c_2)) (p12 c_1) (p12 c_2) )(or (p12 (f43 c_2 c_0)) (p12 c_2) (p12 c_0) )(or (p12 (f43 c_2 c_1)) (p12 c_2) (p12 c_1) )(or (p12 (f43 c_2 c_2)) (p12 c_2) (p12 c_2) )(or (= (f21 (f28 c_0 c_0) c_0) c_0) (not (= c_0 c15)) )(or (= (f21 (f28 c_0 c_0) c_1) c_0) (not (= c_1 c15)) )(or (= (f21 (f28 c_0 c_0) c_2) c_0) (not (= c_2 c15)) )(or (= (f21 (f28 c_0 c_1) c_0) c_0) (not (= c_0 c15)) )(or (= (f21 (f28 c_0 c_1) c_1) c_0) (not (= c_1 c15)) )(or (= (f21 (f28 c_0 c_1) c_2) c_0) (not (= c_2 c15)) )(or (= (f21 (f28 c_0 c_2) c_0) c_0) (not (= c_0 c15)) )(or (= (f21 (f28 c_0 c_2) c_1) c_0) (not (= c_1 c15)) )(or (= (f21 (f28 c_0 c_2) c_2) c_0) (not (= c_2 c15)) )(or (= (f21 (f28 c_1 c_0) c_0) c_1) (not (= c_0 c15)) )(or (= (f21 (f28 c_1 c_0) c_1) c_1) (not (= c_1 c15)) )(or (= (f21 (f28 c_1 c_0) c_2) c_1) (not (= c_2 c15)) )(or (= (f21 (f28 c_1 c_1) c_0) c_1) (not (= c_0 c15)) )(or (= (f21 (f28 c_1 c_1) c_1) c_1) (not (= c_1 c15)) )(or (= (f21 (f28 c_1 c_1) c_2) c_1) (not (= c_2 c15)) )(or (= (f21 (f28 c_1 c_2) c_0) c_1) (not (= c_0 c15)) )(or (= (f21 (f28 c_1 c_2) c_1) c_1) (not (= c_1 c15)) )(or (= (f21 (f28 c_1 c_2) c_2) c_1) (not (= c_2 c15)) )(or (= (f21 (f28 c_2 c_0) c_0) c_2) (not (= c_0 c15)) )(or (= (f21 (f28 c_2 c_0) c_1) c_2) (not (= c_1 c15)) )(or (= (f21 (f28 c_2 c_0) c_2) c_2) (not (= c_2 c15)) )(or (= (f21 (f28 c_2 c_1) c_0) c_2) (not (= c_0 c15)) )(or (= (f21 (f28 c_2 c_1) c_1) c_2) (not (= c_1 c15)) )(or (= (f21 (f28 c_2 c_1) c_2) c_2) (not (= c_2 c15)) )(or (= (f21 (f28 c_2 c_2) c_0) c_2) (not (= c_0 c15)) )(or (= (f21 (f28 c_2 c_2) c_1) c_2) (not (= c_1 c15)) )(or (= (f21 (f28 c_2 c_2) c_2) c_2) (not (= c_2 c15)) )(or (= (f3 c_0 c6) c_0) (not (p22 c_0 (f3 c_0 c6))) (p22 c_0 c_0) )(or (= (f3 c_0 c6) c_1) (not (p22 c_1 (f3 c_0 c6))) (p22 c_1 c_0) )(or (= (f3 c_0 c6) c_2) (not (p22 c_2 (f3 c_0 c6))) (p22 c_2 c_0) )(or (= (f3 c_1 c6) c_0) (not (p22 c_0 (f3 c_1 c6))) (p22 c_0 c_1) )(or (= (f3 c_1 c6) c_1) (not (p22 c_1 (f3 c_1 c6))) (p22 c_1 c_1) )(or (= (f3 c_1 c6) c_2) (not (p22 c_2 (f3 c_1 c6))) (p22 c_2 c_1) )(or (= (f3 c_2 c6) c_0) (not (p22 c_0 (f3 c_2 c6))) (p22 c_0 c_2) )(or (= (f3 c_2 c6) c_1) (not (p22 c_1 (f3 c_2 c6))) (p22 c_1 c_2) )(or (= (f3 c_2 c6) c_2) (not (p22 c_2 (f3 c_2 c6))) (p22 c_2 c_2) )(or (not (p26 c_0 c_0)) (p22 c_0 c_0) )(or (not (p26 c_0 c_1)) (p22 c_1 c_0) )(or (not (p26 c_0 c_2)) (p22 c_2 c_0) )(or (not (p26 c_1 c_0)) (p22 c_0 c_1) )(or (not (p26 c_1 c_1)) (p22 c_1 c_1) )(or (not (p26 c_1 c_2)) (p22 c_2 c_1) )(or (not (p26 c_2 c_0)) (p22 c_0 c_2) )(or (not (p26 c_2 c_1)) (p22 c_1 c_2) )(or (not (p26 c_2 c_2)) (p22 c_2 c_2) )(or (not (p12 c_0)) (p12 (f39 c_0 c_0)) (not (p12 c_0)) )(or (not (p12 c_0)) (p12 (f39 c_1 c_0)) (not (p12 c_1)) )(or (not (p12 c_0)) (p12 (f39 c_2 c_0)) (not (p12 c_2)) )(or (not (p12 c_1)) (p12 (f39 c_0 c_1)) (not (p12 c_0)) )(or (not (p12 c_1)) (p12 (f39 c_1 c_1)) (not (p12 c_1)) )(or (not (p12 c_1)) (p12 (f39 c_2 c_1)) (not (p12 c_2)) )(or (not (p12 c_2)) (p12 (f39 c_0 c_2)) (not (p12 c_0)) )(or (not (p12 c_2)) (p12 (f39 c_1 c_2)) (not (p12 c_1)) )(or (not (p12 c_2)) (p12 (f39 c_2 c_2)) (not (p12 c_2)) )(= (f1 c29) c15) (or (p22 c_0 c_0) (p22 c_0 c_0) (not (p22 c_0 c_0)) )(or (p22 c_0 c_0) (p22 c_0 c_1) (not (p22 c_0 c_1)) )(or (p22 c_0 c_0) (p22 c_0 c_2) (not (p22 c_0 c_2)) )(or (p22 c_0 c_1) (p22 c_1 c_0) (not (p22 c_0 c_0)) )(or (p22 c_0 c_1) (p22 c_1 c_1) (not (p22 c_0 c_1)) )(or (p22 c_0 c_1) (p22 c_1 c_2) (not (p22 c_0 c_2)) )(or (p22 c_0 c_2) (p22 c_2 c_0) (not (p22 c_0 c_0)) )(or (p22 c_0 c_2) (p22 c_2 c_1) (not (p22 c_0 c_1)) )(or (p22 c_0 c_2) (p22 c_2 c_2) (not (p22 c_0 c_2)) )(or (p22 c_1 c_0) (p22 c_0 c_0) (not (p22 c_1 c_0)) )(or (p22 c_1 c_0) (p22 c_0 c_1) (not (p22 c_1 c_1)) )(or (p22 c_1 c_0) (p22 c_0 c_2) (not (p22 c_1 c_2)) )(or (p22 c_1 c_1) (p22 c_1 c_0) (not (p22 c_1 c_0)) )(or (p22 c_1 c_1) (p22 c_1 c_1) (not (p22 c_1 c_1)) )(or (p22 c_1 c_1) (p22 c_1 c_2) (not (p22 c_1 c_2)) )(or (p22 c_1 c_2) (p22 c_2 c_0) (not (p22 c_1 c_0)) )(or (p22 c_1 c_2) (p22 c_2 c_1) (not (p22 c_1 c_1)) )(or (p22 c_1 c_2) (p22 c_2 c_2) (not (p22 c_1 c_2)) )(or (p22 c_2 c_0) (p22 c_0 c_0) (not (p22 c_2 c_0)) )(or (p22 c_2 c_0) (p22 c_0 c_1) (not (p22 c_2 c_1)) )(or (p22 c_2 c_0) (p22 c_0 c_2) (not (p22 c_2 c_2)) )(or (p22 c_2 c_1) (p22 c_1 c_0) (not (p22 c_2 c_0)) )(or (p22 c_2 c_1) (p22 c_1 c_1) (not (p22 c_2 c_1)) )(or (p22 c_2 c_1) (p22 c_1 c_2) (not (p22 c_2 c_2)) )(or (p22 c_2 c_2) (p22 c_2 c_0) (not (p22 c_2 c_0)) )(or (p22 c_2 c_2) (p22 c_2 c_1) (not (p22 c_2 c_1)) )(or (p22 c_2 c_2) (p22 c_2 c_2) (not (p22 c_2 c_2)) )(or (not (p12 c_0)) (p12 (f35 c_0 c_0)) )(or (not (p12 c_0)) (p12 (f35 c_1 c_0)) )(or (not (p12 c_0)) (p12 (f35 c_2 c_0)) )(or (not (p12 c_1)) (p12 (f35 c_0 c_1)) )(or (not (p12 c_1)) (p12 (f35 c_1 c_1)) )(or (not (p12 c_1)) (p12 (f35 c_2 c_1)) )(or (not (p12 c_2)) (p12 (f35 c_0 c_2)) )(or (not (p12 c_2)) (p12 (f35 c_1 c_2)) )(or (not (p12 c_2)) (p12 (f35 c_2 c_2)) )(not (p12 c42)) (not (= (f3 c_0 c6) c15)) (not (= (f3 c_1 c6) c15)) (not (= (f3 c_2 c6) c15)) (or (p12 (f48 c_0 c_0)) (not (p22 c_0 c_0)) )(or (p12 (f48 c_0 c_1)) (not (p22 c_1 c_0)) )(or (p12 (f48 c_0 c_2)) (not (p22 c_2 c_0)) )(or (p12 (f48 c_1 c_0)) (not (p22 c_0 c_1)) )(or (p12 (f48 c_1 c_1)) (not (p22 c_1 c_1)) )(or (p12 (f48 c_1 c_2)) (not (p22 c_2 c_1)) )(or (p12 (f48 c_2 c_0)) (not (p22 c_0 c_2)) )(or (p12 (f48 c_2 c_1)) (not (p22 c_1 c_2)) )(or (p12 (f48 c_2 c_2)) (not (p22 c_2 c_2)) )(or (not (p12 (f39 c_0 c_0))) (p12 c_0) (not (p12 c_0)) )(or (not (p12 (f39 c_0 c_1))) (p12 c_1) (not (p12 c_0)) )(or (not (p12 (f39 c_0 c_2))) (p12 c_2) (not (p12 c_0)) )(or (not (p12 (f39 c_1 c_0))) (p12 c_0) (not (p12 c_1)) )(or (not (p12 (f39 c_1 c_1))) (p12 c_1) (not (p12 c_1)) )(or (not (p12 (f39 c_1 c_2))) (p12 c_2) (not (p12 c_1)) )(or (not (p12 (f39 c_2 c_0))) (p12 c_0) (not (p12 c_2)) )(or (not (p12 (f39 c_2 c_1))) (p12 c_1) (not (p12 c_2)) )(or (not (p12 (f39 c_2 c_2))) (p12 c_2) (not (p12 c_2)) )(or (= (f4 c_0 c_0) c_0) (not (= (f3 c_0 c_0) c_0)) (p26 c_0 c_0) )(or (= (f4 c_0 c_0) c_1) (not (= (f3 c_1 c_0) c_0)) (p26 c_0 c_0) )(or (= (f4 c_0 c_0) c_2) (not (= (f3 c_2 c_0) c_0)) (p26 c_0 c_0) )(or (= (f4 c_0 c_1) c_0) (not (= (f3 c_0 c_1) c_0)) (p26 c_1 c_0) )(or (= (f4 c_0 c_1) c_1) (not (= (f3 c_1 c_1) c_0)) (p26 c_1 c_0) )(or (= (f4 c_0 c_1) c_2) (not (= (f3 c_2 c_1) c_0)) (p26 c_1 c_0) )(or (= (f4 c_0 c_2) c_0) (not (= (f3 c_0 c_2) c_0)) (p26 c_2 c_0) )(or (= (f4 c_0 c_2) c_1) (not (= (f3 c_1 c_2) c_0)) (p26 c_2 c_0) )(or (= (f4 c_0 c_2) c_2) (not (= (f3 c_2 c_2) c_0)) (p26 c_2 c_0) )(or (= (f4 c_1 c_0) c_0) (not (= (f3 c_0 c_0) c_1)) (p26 c_0 c_1) )(or (= (f4 c_1 c_0) c_1) (not (= (f3 c_1 c_0) c_1)) (p26 c_0 c_1) )(or (= (f4 c_1 c_0) c_2) (not (= (f3 c_2 c_0) c_1)) (p26 c_0 c_1) )(or (= (f4 c_1 c_1) c_0) (not (= (f3 c_0 c_1) c_1)) (p26 c_1 c_1) )(or (= (f4 c_1 c_1) c_1) (not (= (f3 c_1 c_1) c_1)) (p26 c_1 c_1) )(or (= (f4 c_1 c_1) c_2) (not (= (f3 c_2 c_1) c_1)) (p26 c_1 c_1) )(or (= (f4 c_1 c_2) c_0) (not (= (f3 c_0 c_2) c_1)) (p26 c_2 c_1) )(or (= (f4 c_1 c_2) c_1) (not (= (f3 c_1 c_2) c_1)) (p26 c_2 c_1) )(or (= (f4 c_1 c_2) c_2) (not (= (f3 c_2 c_2) c_1)) (p26 c_2 c_1) )(or (= (f4 c_2 c_0) c_0) (not (= (f3 c_0 c_0) c_2)) (p26 c_0 c_2) )(or (= (f4 c_2 c_0) c_1) (not (= (f3 c_1 c_0) c_2)) (p26 c_0 c_2) )(or (= (f4 c_2 c_0) c_2) (not (= (f3 c_2 c_0) c_2)) (p26 c_0 c_2) )(or (= (f4 c_2 c_1) c_0) (not (= (f3 c_0 c_1) c_2)) (p26 c_1 c_2) )(or (= (f4 c_2 c_1) c_1) (not (= (f3 c_1 c_1) c_2)) (p26 c_1 c_2) )(or (= (f4 c_2 c_1) c_2) (not (= (f3 c_2 c_1) c_2)) (p26 c_1 c_2) )(or (= (f4 c_2 c_2) c_0) (not (= (f3 c_0 c_2) c_2)) (p26 c_2 c_2) )(or (= (f4 c_2 c_2) c_1) (not (= (f3 c_1 c_2) c_2)) (p26 c_2 c_2) )(or (= (f4 c_2 c_2) c_2) (not (= (f3 c_2 c_2) c_2)) (p26 c_2 c_2) )(or (p12 (f37 c_0 c_0)) (p12 c_0) )(or (p12 (f37 c_0 c_1)) (p12 c_0) )(or (p12 (f37 c_0 c_2)) (p12 c_0) )(or (p12 (f37 c_1 c_0)) (p12 c_1) )(or (p12 (f37 c_1 c_1)) (p12 c_1) )(or (p12 (f37 c_1 c_2)) (p12 c_1) )(or (p12 (f37 c_2 c_0)) (p12 c_2) )(or (p12 (f37 c_2 c_1)) (p12 c_2) )(or (p12 (f37 c_2 c_2)) (p12 c_2) )(p22 c_0 c_0) (p22 c_1 c_1) (p22 c_2 c_2) (or (not (p12 (f45 c_0 c_0))) (not (p22 c_0 c_0)) )(or (not (p12 (f45 c_0 c_1))) (not (p22 c_1 c_0)) )(or (not (p12 (f45 c_0 c_2))) (not (p22 c_2 c_0)) )(or (not (p12 (f45 c_1 c_0))) (not (p22 c_0 c_1)) )(or (not (p12 (f45 c_1 c_1))) (not (p22 c_1 c_1)) )(or (not (p12 (f45 c_1 c_2))) (not (p22 c_2 c_1)) )(or (not (p12 (f45 c_2 c_0))) (not (p22 c_0 c_2)) )(or (not (p12 (f45 c_2 c_1))) (not (p22 c_1 c_2)) )(or (not (p12 (f45 c_2 c_2))) (not (p22 c_2 c_2)) )(or (p12 (f20 (f3 c_0 c6))) (not (p12 (f23 c_0))) (p12 (f17 c_0)) (p12 (f24 c_0)) (not (p22 (f11 c_0) c15)) )(or (p12 (f20 (f3 c_1 c6))) (not (p12 (f23 c_1))) (p12 (f17 c_1)) (p12 (f24 c_1)) (not (p22 (f11 c_1) c15)) )(or (p12 (f20 (f3 c_2 c6))) (not (p12 (f23 c_2))) (p12 (f17 c_2)) (p12 (f24 c_2)) (not (p22 (f11 c_2) c15)) )(or (not (p12 (f20 c_0))) (p12 (f20 (f3 c_0 c6))) (p12 (f23 c_0)) (p12 (f17 c_0)) (not (p12 (f24 c_0))) )(or (not (p12 (f20 c_1))) (p12 (f20 (f3 c_1 c6))) (p12 (f23 c_1)) (p12 (f17 c_1)) (not (p12 (f24 c_1))) )(or (not (p12 (f20 c_2))) (p12 (f20 (f3 c_2 c6))) (p12 (f23 c_2)) (p12 (f17 c_2)) (not (p12 (f24 c_2))) )(or (p26 c_0 c_0) (= (f3 c_0 c_0) c_0) (not (= (f4 c_0 c_0) c_0)) )(or (p26 c_0 c_0) (= (f3 c_1 c_0) c_0) (not (= (f4 c_0 c_0) c_1)) )(or (p26 c_0 c_0) (= (f3 c_2 c_0) c_0) (not (= (f4 c_0 c_0) c_2)) )(or (p26 c_0 c_1) (= (f3 c_0 c_0) c_1) (not (= (f4 c_1 c_0) c_0)) )(or (p26 c_0 c_1) (= (f3 c_1 c_0) c_1) (not (= (f4 c_1 c_0) c_1)) )(or (p26 c_0 c_1) (= (f3 c_2 c_0) c_1) (not (= (f4 c_1 c_0) c_2)) )(or (p26 c_0 c_2) (= (f3 c_0 c_0) c_2) (not (= (f4 c_2 c_0) c_0)) )(or (p26 c_0 c_2) (= (f3 c_1 c_0) c_2) (not (= (f4 c_2 c_0) c_1)) )(or (p26 c_0 c_2) (= (f3 c_2 c_0) c_2) (not (= (f4 c_2 c_0) c_2)) )(or (p26 c_1 c_0) (= (f3 c_0 c_1) c_0) (not (= (f4 c_0 c_1) c_0)) )(or (p26 c_1 c_0) (= (f3 c_1 c_1) c_0) (not (= (f4 c_0 c_1) c_1)) )(or (p26 c_1 c_0) (= (f3 c_2 c_1) c_0) (not (= (f4 c_0 c_1) c_2)) )(or (p26 c_1 c_1) (= (f3 c_0 c_1) c_1) (not (= (f4 c_1 c_1) c_0)) )(or (p26 c_1 c_1) (= (f3 c_1 c_1) c_1) (not (= (f4 c_1 c_1) c_1)) )(or (p26 c_1 c_1) (= (f3 c_2 c_1) c_1) (not (= (f4 c_1 c_1) c_2)) )(or (p26 c_1 c_2) (= (f3 c_0 c_1) c_2) (not (= (f4 c_2 c_1) c_0)) )(or (p26 c_1 c_2) (= (f3 c_1 c_1) c_2) (not (= (f4 c_2 c_1) c_1)) )(or (p26 c_1 c_2) (= (f3 c_2 c_1) c_2) (not (= (f4 c_2 c_1) c_2)) )(or (p26 c_2 c_0) (= (f3 c_0 c_2) c_0) (not (= (f4 c_0 c_2) c_0)) )(or (p26 c_2 c_0) (= (f3 c_1 c_2) c_0) (not (= (f4 c_0 c_2) c_1)) )(or (p26 c_2 c_0) (= (f3 c_2 c_2) c_0) (not (= (f4 c_0 c_2) c_2)) )(or (p26 c_2 c_1) (= (f3 c_0 c_2) c_1) (not (= (f4 c_1 c_2) c_0)) )(or (p26 c_2 c_1) (= (f3 c_1 c_2) c_1) (not (= (f4 c_1 c_2) c_1)) )(or (p26 c_2 c_1) (= (f3 c_2 c_2) c_1) (not (= (f4 c_1 c_2) c_2)) )(or (p26 c_2 c_2) (= (f3 c_0 c_2) c_2) (not (= (f4 c_2 c_2) c_0)) )(or (p26 c_2 c_2) (= (f3 c_1 c_2) c_2) (not (= (f4 c_2 c_2) c_1)) )(or (p26 c_2 c_2) (= (f3 c_2 c_2) c_2) (not (= (f4 c_2 c_2) c_2)) )(or (p12 c_0) (not (p12 (f34 c_0 c_0))) )(or (p12 c_0) (not (p12 (f34 c_1 c_0))) )(or (p12 c_0) (not (p12 (f34 c_2 c_0))) )(or (p12 c_1) (not (p12 (f34 c_0 c_1))) )(or (p12 c_1) (not (p12 (f34 c_1 c_1))) )(or (p12 c_1) (not (p12 (f34 c_2 c_1))) )(or (p12 c_2) (not (p12 (f34 c_0 c_2))) )(or (p12 c_2) (not (p12 (f34 c_1 c_2))) )(or (p12 c_2) (not (p12 (f34 c_2 c_2))) )(or (p12 c_0) (not (p12 (f34 c_0 c_0))) )(or (p12 c_0) (not (p12 (f34 c_0 c_1))) )(or (p12 c_0) (not (p12 (f34 c_0 c_2))) )(or (p12 c_1) (not (p12 (f34 c_1 c_0))) )(or (p12 c_1) (not (p12 (f34 c_1 c_1))) )(or (p12 c_1) (not (p12 (f34 c_1 c_2))) )(or (p12 c_2) (not (p12 (f34 c_2 c_0))) )(or (p12 c_2) (not (p12 (f34 c_2 c_1))) )(or (p12 c_2) (not (p12 (f34 c_2 c_2))) )(or (p22 c_0 c_0) (not (p12 (f48 c_0 c_0))) )(or (p22 c_0 c_1) (not (p12 (f48 c_1 c_0))) )(or (p22 c_0 c_2) (not (p12 (f48 c_2 c_0))) )(or (p22 c_1 c_0) (not (p12 (f48 c_0 c_1))) )(or (p22 c_1 c_1) (not (p12 (f48 c_1 c_1))) )(or (p22 c_1 c_2) (not (p12 (f48 c_2 c_1))) )(or (p22 c_2 c_0) (not (p12 (f48 c_0 c_2))) )(or (p22 c_2 c_1) (not (p12 (f48 c_1 c_2))) )(or (p22 c_2 c_2) (not (p12 (f48 c_2 c_2))) )(or (not (p12 (f47 c_0 c_0))) (not (p22 c_0 c_0)) )(or (not (p12 (f47 c_0 c_1))) (not (p22 c_0 c_1)) )(or (not (p12 (f47 c_0 c_2))) (not (p22 c_0 c_2)) )(or (not (p12 (f47 c_1 c_0))) (not (p22 c_1 c_0)) )(or (not (p12 (f47 c_1 c_1))) (not (p22 c_1 c_1)) )(or (not (p12 (f47 c_1 c_2))) (not (p22 c_1 c_2)) )(or (not (p12 (f47 c_2 c_0))) (not (p22 c_2 c_0)) )(or (not (p12 (f47 c_2 c_1))) (not (p22 c_2 c_1)) )(or (not (p12 (f47 c_2 c_2))) (not (p22 c_2 c_2)) )(or (p12 (f23 c_0)) (not (p12 (f24 c_0))) (p12 (f17 c_0)) (= (f16 (f3 c_0 c6)) (f16 c_0)) )(or (p12 (f23 c_1)) (not (p12 (f24 c_1))) (p12 (f17 c_1)) (= (f16 (f3 c_1 c6)) (f16 c_1)) )(or (p12 (f23 c_2)) (not (p12 (f24 c_2))) (p12 (f17 c_2)) (= (f16 (f3 c_2 c6)) (f16 c_2)) )(or (p22 c_0 c_0) (not (p22 (f3 c_0 c6) (f3 c_0 c6))) )(or (p22 c_0 c_1) (not (p22 (f3 c_0 c6) (f3 c_1 c6))) )(or (p22 c_0 c_2) (not (p22 (f3 c_0 c6) (f3 c_2 c6))) )(or (p22 c_1 c_0) (not (p22 (f3 c_1 c6) (f3 c_0 c6))) )(or (p22 c_1 c_1) (not (p22 (f3 c_1 c6) (f3 c_1 c6))) )(or (p22 c_1 c_2) (not (p22 (f3 c_1 c6) (f3 c_2 c6))) )(or (p22 c_2 c_0) (not (p22 (f3 c_2 c6) (f3 c_0 c6))) )(or (p22 c_2 c_1) (not (p22 (f3 c_2 c6) (f3 c_1 c6))) )(or (p22 c_2 c_2) (not (p22 (f3 c_2 c6) (f3 c_2 c6))) )(or (not (p12 c_0)) (not (p12 (f40 c_0))) )(or (not (p12 c_1)) (not (p12 (f40 c_1))) )(or (not (p12 c_2)) (not (p12 (f40 c_2))) )(or (= c_0 c_0) (not (= (f3 c_0 c6) (f3 c_0 c6))) )(or (= c_0 c_1) (not (= (f3 c_0 c6) (f3 c_1 c6))) )(or (= c_0 c_2) (not (= (f3 c_0 c6) (f3 c_2 c6))) )(or (= c_1 c_0) (not (= (f3 c_1 c6) (f3 c_0 c6))) )(or (= c_1 c_1) (not (= (f3 c_1 c6) (f3 c_1 c6))) )(or (= c_1 c_2) (not (= (f3 c_1 c6) (f3 c_2 c6))) )(or (= c_2 c_0) (not (= (f3 c_2 c6) (f3 c_0 c6))) )(or (= c_2 c_1) (not (= (f3 c_2 c6) (f3 c_1 c6))) )(or (= c_2 c_2) (not (= (f3 c_2 c6) (f3 c_2 c6))) )(= (f21 (f38 c_0 c_0) c_0) (f38 (f21 c_0 c_0) (f21 c_0 c_0))) (= (f21 (f38 c_0 c_0) c_1) (f38 (f21 c_0 c_1) (f21 c_0 c_1))) (= (f21 (f38 c_0 c_0) c_2) (f38 (f21 c_0 c_2) (f21 c_0 c_2))) (= (f21 (f38 c_0 c_1) c_0) (f38 (f21 c_0 c_0) (f21 c_1 c_0))) (= (f21 (f38 c_0 c_1) c_1) (f38 (f21 c_0 c_1) (f21 c_1 c_1))) (= (f21 (f38 c_0 c_1) c_2) (f38 (f21 c_0 c_2) (f21 c_1 c_2))) (= (f21 (f38 c_0 c_2) c_0) (f38 (f21 c_0 c_0) (f21 c_2 c_0))) (= (f21 (f38 c_0 c_2) c_1) (f38 (f21 c_0 c_1) (f21 c_2 c_1))) (= (f21 (f38 c_0 c_2) c_2) (f38 (f21 c_0 c_2) (f21 c_2 c_2))) (= (f21 (f38 c_1 c_0) c_0) (f38 (f21 c_1 c_0) (f21 c_0 c_0))) (= (f21 (f38 c_1 c_0) c_1) (f38 (f21 c_1 c_1) (f21 c_0 c_1))) (= (f21 (f38 c_1 c_0) c_2) (f38 (f21 c_1 c_2) (f21 c_0 c_2))) (= (f21 (f38 c_1 c_1) c_0) (f38 (f21 c_1 c_0) (f21 c_1 c_0))) (= (f21 (f38 c_1 c_1) c_1) (f38 (f21 c_1 c_1) (f21 c_1 c_1))) (= (f21 (f38 c_1 c_1) c_2) (f38 (f21 c_1 c_2) (f21 c_1 c_2))) (= (f21 (f38 c_1 c_2) c_0) (f38 (f21 c_1 c_0) (f21 c_2 c_0))) (= (f21 (f38 c_1 c_2) c_1) (f38 (f21 c_1 c_1) (f21 c_2 c_1))) (= (f21 (f38 c_1 c_2) c_2) (f38 (f21 c_1 c_2) (f21 c_2 c_2))) (= (f21 (f38 c_2 c_0) c_0) (f38 (f21 c_2 c_0) (f21 c_0 c_0))) (= (f21 (f38 c_2 c_0) c_1) (f38 (f21 c_2 c_1) (f21 c_0 c_1))) (= (f21 (f38 c_2 c_0) c_2) (f38 (f21 c_2 c_2) (f21 c_0 c_2))) (= (f21 (f38 c_2 c_1) c_0) (f38 (f21 c_2 c_0) (f21 c_1 c_0))) (= (f21 (f38 c_2 c_1) c_1) (f38 (f21 c_2 c_1) (f21 c_1 c_1))) (= (f21 (f38 c_2 c_1) c_2) (f38 (f21 c_2 c_2) (f21 c_1 c_2))) (= (f21 (f38 c_2 c_2) c_0) (f38 (f21 c_2 c_0) (f21 c_2 c_0))) (= (f21 (f38 c_2 c_2) c_1) (f38 (f21 c_2 c_1) (f21 c_2 c_1))) (= (f21 (f38 c_2 c_2) c_2) (f38 (f21 c_2 c_2) (f21 c_2 c_2))) (or (not (p12 c_0)) (not (p12 (f38 c_0 c_0))) )(or (not (p12 c_0)) (not (p12 (f38 c_0 c_1))) )(or (not (p12 c_0)) (not (p12 (f38 c_0 c_2))) )(or (not (p12 c_1)) (not (p12 (f38 c_1 c_0))) )(or (not (p12 c_1)) (not (p12 (f38 c_1 c_1))) )(or (not (p12 c_1)) (not (p12 (f38 c_1 c_2))) )(or (not (p12 c_2)) (not (p12 (f38 c_2 c_0))) )(or (not (p12 c_2)) (not (p12 (f38 c_2 c_1))) )(or (not (p12 c_2)) (not (p12 (f38 c_2 c_2))) )(or (= c_0 c15) (not (p22 c_0 c15)) )(or (= c_1 c15) (not (p22 c_1 c15)) )(or (= c_2 c15) (not (p22 c_2 c15)) )(p12 (f24 c49)) (or (p12 (f37 c_0 c_0)) (p12 c_0) )(or (p12 (f37 c_0 c_1)) (p12 c_1) )(or (p12 (f37 c_0 c_2)) (p12 c_2) )(or (p12 (f37 c_1 c_0)) (p12 c_0) )(or (p12 (f37 c_1 c_1)) (p12 c_1) )(or (p12 (f37 c_1 c_2)) (p12 c_2) )(or (p12 (f37 c_2 c_0)) (p12 c_0) )(or (p12 (f37 c_2 c_1)) (p12 c_1) )(or (p12 (f37 c_2 c_2)) (p12 c_2) )(= (f21 (f32 c_0) c_0) c_0) (= (f21 (f32 c_0) c_1) c_0) (= (f21 (f32 c_0) c_2) c_0) (= (f21 (f32 c_1) c_0) c_1) (= (f21 (f32 c_1) c_1) c_1) (= (f21 (f32 c_1) c_2) c_1) (= (f21 (f32 c_2) c_0) c_2) (= (f21 (f32 c_2) c_1) c_2) (= (f21 (f32 c_2) c_2) c_2) (or (= (f31 c_0 c_0 c_0) c_0)(= (f31 c_0 c_0 c_0) c_1)(= (f31 c_0 c_0 c_0) c_2))(or (= (f31 c_0 c_0 c_1) c_0)(= (f31 c_0 c_0 c_1) c_1)(= (f31 c_0 c_0 c_1) c_2))(or (= (f31 c_0 c_0 c_2) c_0)(= (f31 c_0 c_0 c_2) c_1)(= (f31 c_0 c_0 c_2) c_2))(or (= (f31 c_0 c_1 c_0) c_0)(= (f31 c_0 c_1 c_0) c_1)(= (f31 c_0 c_1 c_0) c_2))(or (= (f31 c_0 c_1 c_1) c_0)(= (f31 c_0 c_1 c_1) c_1)(= (f31 c_0 c_1 c_1) c_2))(or (= (f31 c_0 c_1 c_2) c_0)(= (f31 c_0 c_1 c_2) c_1)(= (f31 c_0 c_1 c_2) c_2))(or (= (f31 c_0 c_2 c_0) c_0)(= (f31 c_0 c_2 c_0) c_1)(= (f31 c_0 c_2 c_0) c_2))(or (= (f31 c_0 c_2 c_1) c_0)(= (f31 c_0 c_2 c_1) c_1)(= (f31 c_0 c_2 c_1) c_2))(or (= (f31 c_0 c_2 c_2) c_0)(= (f31 c_0 c_2 c_2) c_1)(= (f31 c_0 c_2 c_2) c_2))(or (= (f31 c_1 c_0 c_0) c_0)(= (f31 c_1 c_0 c_0) c_1)(= (f31 c_1 c_0 c_0) c_2))(or (= (f31 c_1 c_0 c_1) c_0)(= (f31 c_1 c_0 c_1) c_1)(= (f31 c_1 c_0 c_1) c_2))(or (= (f31 c_1 c_0 c_2) c_0)(= (f31 c_1 c_0 c_2) c_1)(= (f31 c_1 c_0 c_2) c_2))(or (= (f31 c_1 c_1 c_0) c_0)(= (f31 c_1 c_1 c_0) c_1)(= (f31 c_1 c_1 c_0) c_2))(or (= (f31 c_1 c_1 c_1) c_0)(= (f31 c_1 c_1 c_1) c_1)(= (f31 c_1 c_1 c_1) c_2))(or (= (f31 c_1 c_1 c_2) c_0)(= (f31 c_1 c_1 c_2) c_1)(= (f31 c_1 c_1 c_2) c_2))(or (= (f31 c_1 c_2 c_0) c_0)(= (f31 c_1 c_2 c_0) c_1)(= (f31 c_1 c_2 c_0) c_2))(or (= (f31 c_1 c_2 c_1) c_0)(= (f31 c_1 c_2 c_1) c_1)(= (f31 c_1 c_2 c_1) c_2))(or (= (f31 c_1 c_2 c_2) c_0)(= (f31 c_1 c_2 c_2) c_1)(= (f31 c_1 c_2 c_2) c_2))(or (= (f31 c_2 c_0 c_0) c_0)(= (f31 c_2 c_0 c_0) c_1)(= (f31 c_2 c_0 c_0) c_2))(or (= (f31 c_2 c_0 c_1) c_0)(= (f31 c_2 c_0 c_1) c_1)(= (f31 c_2 c_0 c_1) c_2))(or (= (f31 c_2 c_0 c_2) c_0)(= (f31 c_2 c_0 c_2) c_1)(= (f31 c_2 c_0 c_2) c_2))(or (= (f31 c_2 c_1 c_0) c_0)(= (f31 c_2 c_1 c_0) c_1)(= (f31 c_2 c_1 c_0) c_2))(or (= (f31 c_2 c_1 c_1) c_0)(= (f31 c_2 c_1 c_1) c_1)(= (f31 c_2 c_1 c_1) c_2))(or (= (f31 c_2 c_1 c_2) c_0)(= (f31 c_2 c_1 c_2) c_1)(= (f31 c_2 c_1 c_2) c_2))(or (= (f31 c_2 c_2 c_0) c_0)(= (f31 c_2 c_2 c_0) c_1)(= (f31 c_2 c_2 c_0) c_2))(or (= (f31 c_2 c_2 c_1) c_0)(= (f31 c_2 c_2 c_1) c_1)(= (f31 c_2 c_2 c_1) c_2))(or (= (f31 c_2 c_2 c_2) c_0)(= (f31 c_2 c_2 c_2) c_1)(= (f31 c_2 c_2 c_2) c_2))(or (= (f43 c_0 c_0) c_0)(= (f43 c_0 c_0) c_1)(= (f43 c_0 c_0) c_2))(or (= (f43 c_0 c_1) c_0)(= (f43 c_0 c_1) c_1)(= (f43 c_0 c_1) c_2))(or (= (f43 c_0 c_2) c_0)(= (f43 c_0 c_2) c_1)(= (f43 c_0 c_2) c_2))(or (= (f43 c_1 c_0) c_0)(= (f43 c_1 c_0) c_1)(= (f43 c_1 c_0) c_2))(or (= (f43 c_1 c_1) c_0)(= (f43 c_1 c_1) c_1)(= (f43 c_1 c_1) c_2))(or (= (f43 c_1 c_2) c_0)(= (f43 c_1 c_2) c_1)(= (f43 c_1 c_2) c_2))(or (= (f43 c_2 c_0) c_0)(= (f43 c_2 c_0) c_1)(= (f43 c_2 c_0) c_2))(or (= (f43 c_2 c_1) c_0)(= (f43 c_2 c_1) c_1)(= (f43 c_2 c_1) c_2))(or (= (f43 c_2 c_2) c_0)(= (f43 c_2 c_2) c_1)(= (f43 c_2 c_2) c_2))(or (= (f3 c_0 c_0) c_0)(= (f3 c_0 c_0) c_1)(= (f3 c_0 c_0) c_2))(or (= (f3 c_0 c_1) c_0)(= (f3 c_0 c_1) c_1)(= (f3 c_0 c_1) c_2))(or (= (f3 c_0 c_2) c_0)(= (f3 c_0 c_2) c_1)(= (f3 c_0 c_2) c_2))(or (= (f3 c_1 c_0) c_0)(= (f3 c_1 c_0) c_1)(= (f3 c_1 c_0) c_2))(or (= (f3 c_1 c_1) c_0)(= (f3 c_1 c_1) c_1)(= (f3 c_1 c_1) c_2))(or (= (f3 c_1 c_2) c_0)(= (f3 c_1 c_2) c_1)(= (f3 c_1 c_2) c_2))(or (= (f3 c_2 c_0) c_0)(= (f3 c_2 c_0) c_1)(= (f3 c_2 c_0) c_2))(or (= (f3 c_2 c_1) c_0)(= (f3 c_2 c_1) c_1)(= (f3 c_2 c_1) c_2))(or (= (f3 c_2 c_2) c_0)(= (f3 c_2 c_2) c_1)(= (f3 c_2 c_2) c_2))(or (= (f35 c_0 c_0) c_0)(= (f35 c_0 c_0) c_1)(= (f35 c_0 c_0) c_2))(or (= (f35 c_0 c_1) c_0)(= (f35 c_0 c_1) c_1)(= (f35 c_0 c_1) c_2))(or (= (f35 c_0 c_2) c_0)(= (f35 c_0 c_2) c_1)(= (f35 c_0 c_2) c_2))(or (= (f35 c_1 c_0) c_0)(= (f35 c_1 c_0) c_1)(= (f35 c_1 c_0) c_2))(or (= (f35 c_1 c_1) c_0)(= (f35 c_1 c_1) c_1)(= (f35 c_1 c_1) c_2))(or (= (f35 c_1 c_2) c_0)(= (f35 c_1 c_2) c_1)(= (f35 c_1 c_2) c_2))(or (= (f35 c_2 c_0) c_0)(= (f35 c_2 c_0) c_1)(= (f35 c_2 c_0) c_2))(or (= (f35 c_2 c_1) c_0)(= (f35 c_2 c_1) c_1)(= (f35 c_2 c_1) c_2))(or (= (f35 c_2 c_2) c_0)(= (f35 c_2 c_2) c_1)(= (f35 c_2 c_2) c_2))(or (= (f21 c_0 c_0) c_0)(= (f21 c_0 c_0) c_1)(= (f21 c_0 c_0) c_2))(or (= (f21 c_0 c_1) c_0)(= (f21 c_0 c_1) c_1)(= (f21 c_0 c_1) c_2))(or (= (f21 c_0 c_2) c_0)(= (f21 c_0 c_2) c_1)(= (f21 c_0 c_2) c_2))(or (= (f21 c_1 c_0) c_0)(= (f21 c_1 c_0) c_1)(= (f21 c_1 c_0) c_2))(or (= (f21 c_1 c_1) c_0)(= (f21 c_1 c_1) c_1)(= (f21 c_1 c_1) c_2))(or (= (f21 c_1 c_2) c_0)(= (f21 c_1 c_2) c_1)(= (f21 c_1 c_2) c_2))(or (= (f21 c_2 c_0) c_0)(= (f21 c_2 c_0) c_1)(= (f21 c_2 c_0) c_2))(or (= (f21 c_2 c_1) c_0)(= (f21 c_2 c_1) c_1)(= (f21 c_2 c_1) c_2))(or (= (f21 c_2 c_2) c_0)(= (f21 c_2 c_2) c_1)(= (f21 c_2 c_2) c_2))(or (= (f4 c_0 c_0) c_0)(= (f4 c_0 c_0) c_1)(= (f4 c_0 c_0) c_2))(or (= (f4 c_0 c_1) c_0)(= (f4 c_0 c_1) c_1)(= (f4 c_0 c_1) c_2))(or (= (f4 c_0 c_2) c_0)(= (f4 c_0 c_2) c_1)(= (f4 c_0 c_2) c_2))(or (= (f4 c_1 c_0) c_0)(= (f4 c_1 c_0) c_1)(= (f4 c_1 c_0) c_2))(or (= (f4 c_1 c_1) c_0)(= (f4 c_1 c_1) c_1)(= (f4 c_1 c_1) c_2))(or (= (f4 c_1 c_2) c_0)(= (f4 c_1 c_2) c_1)(= (f4 c_1 c_2) c_2))(or (= (f4 c_2 c_0) c_0)(= (f4 c_2 c_0) c_1)(= (f4 c_2 c_0) c_2))(or (= (f4 c_2 c_1) c_0)(= (f4 c_2 c_1) c_1)(= (f4 c_2 c_1) c_2))(or (= (f4 c_2 c_2) c_0)(= (f4 c_2 c_2) c_1)(= (f4 c_2 c_2) c_2))(or (= (f25 c_0 c_0) c_0)(= (f25 c_0 c_0) c_1)(= (f25 c_0 c_0) c_2))(or (= (f25 c_0 c_1) c_0)(= (f25 c_0 c_1) c_1)(= (f25 c_0 c_1) c_2))(or (= (f25 c_0 c_2) c_0)(= (f25 c_0 c_2) c_1)(= (f25 c_0 c_2) c_2))(or (= (f25 c_1 c_0) c_0)(= (f25 c_1 c_0) c_1)(= (f25 c_1 c_0) c_2))(or (= (f25 c_1 c_1) c_0)(= (f25 c_1 c_1) c_1)(= (f25 c_1 c_1) c_2))(or (= (f25 c_1 c_2) c_0)(= (f25 c_1 c_2) c_1)(= (f25 c_1 c_2) c_2))(or (= (f25 c_2 c_0) c_0)(= (f25 c_2 c_0) c_1)(= (f25 c_2 c_0) c_2))(or (= (f25 c_2 c_1) c_0)(= (f25 c_2 c_1) c_1)(= (f25 c_2 c_1) c_2))(or (= (f25 c_2 c_2) c_0)(= (f25 c_2 c_2) c_1)(= (f25 c_2 c_2) c_2))(or (= (f37 c_0 c_0) c_0)(= (f37 c_0 c_0) c_1)(= (f37 c_0 c_0) c_2))(or (= (f37 c_0 c_1) c_0)(= (f37 c_0 c_1) c_1)(= (f37 c_0 c_1) c_2))(or (= (f37 c_0 c_2) c_0)(= (f37 c_0 c_2) c_1)(= (f37 c_0 c_2) c_2))(or (= (f37 c_1 c_0) c_0)(= (f37 c_1 c_0) c_1)(= (f37 c_1 c_0) c_2))(or (= (f37 c_1 c_1) c_0)(= (f37 c_1 c_1) c_1)(= (f37 c_1 c_1) c_2))(or (= (f37 c_1 c_2) c_0)(= (f37 c_1 c_2) c_1)(= (f37 c_1 c_2) c_2))(or (= (f37 c_2 c_0) c_0)(= (f37 c_2 c_0) c_1)(= (f37 c_2 c_0) c_2))(or (= (f37 c_2 c_1) c_0)(= (f37 c_2 c_1) c_1)(= (f37 c_2 c_1) c_2))(or (= (f37 c_2 c_2) c_0)(= (f37 c_2 c_2) c_1)(= (f37 c_2 c_2) c_2))(or (= (f34 c_0 c_0) c_0)(= (f34 c_0 c_0) c_1)(= (f34 c_0 c_0) c_2))(or (= (f34 c_0 c_1) c_0)(= (f34 c_0 c_1) c_1)(= (f34 c_0 c_1) c_2))(or (= (f34 c_0 c_2) c_0)(= (f34 c_0 c_2) c_1)(= (f34 c_0 c_2) c_2))(or (= (f34 c_1 c_0) c_0)(= (f34 c_1 c_0) c_1)(= (f34 c_1 c_0) c_2))(or (= (f34 c_1 c_1) c_0)(= (f34 c_1 c_1) c_1)(= (f34 c_1 c_1) c_2))(or (= (f34 c_1 c_2) c_0)(= (f34 c_1 c_2) c_1)(= (f34 c_1 c_2) c_2))(or (= (f34 c_2 c_0) c_0)(= (f34 c_2 c_0) c_1)(= (f34 c_2 c_0) c_2))(or (= (f34 c_2 c_1) c_0)(= (f34 c_2 c_1) c_1)(= (f34 c_2 c_1) c_2))(or (= (f34 c_2 c_2) c_0)(= (f34 c_2 c_2) c_1)(= (f34 c_2 c_2) c_2))(or (= (f36 c_0 c_0) c_0)(= (f36 c_0 c_0) c_1)(= (f36 c_0 c_0) c_2))(or (= (f36 c_0 c_1) c_0)(= (f36 c_0 c_1) c_1)(= (f36 c_0 c_1) c_2))(or (= (f36 c_0 c_2) c_0)(= (f36 c_0 c_2) c_1)(= (f36 c_0 c_2) c_2))(or (= (f36 c_1 c_0) c_0)(= (f36 c_1 c_0) c_1)(= (f36 c_1 c_0) c_2))(or (= (f36 c_1 c_1) c_0)(= (f36 c_1 c_1) c_1)(= (f36 c_1 c_1) c_2))(or (= (f36 c_1 c_2) c_0)(= (f36 c_1 c_2) c_1)(= (f36 c_1 c_2) c_2))(or (= (f36 c_2 c_0) c_0)(= (f36 c_2 c_0) c_1)(= (f36 c_2 c_0) c_2))(or (= (f36 c_2 c_1) c_0)(= (f36 c_2 c_1) c_1)(= (f36 c_2 c_1) c_2))(or (= (f36 c_2 c_2) c_0)(= (f36 c_2 c_2) c_1)(= (f36 c_2 c_2) c_2))(or (= (f39 c_0 c_0) c_0)(= (f39 c_0 c_0) c_1)(= (f39 c_0 c_0) c_2))(or (= (f39 c_0 c_1) c_0)(= (f39 c_0 c_1) c_1)(= (f39 c_0 c_1) c_2))(or (= (f39 c_0 c_2) c_0)(= (f39 c_0 c_2) c_1)(= (f39 c_0 c_2) c_2))(or (= (f39 c_1 c_0) c_0)(= (f39 c_1 c_0) c_1)(= (f39 c_1 c_0) c_2))(or (= (f39 c_1 c_1) c_0)(= (f39 c_1 c_1) c_1)(= (f39 c_1 c_1) c_2))(or (= (f39 c_1 c_2) c_0)(= (f39 c_1 c_2) c_1)(= (f39 c_1 c_2) c_2))(or (= (f39 c_2 c_0) c_0)(= (f39 c_2 c_0) c_1)(= (f39 c_2 c_0) c_2))(or (= (f39 c_2 c_1) c_0)(= (f39 c_2 c_1) c_1)(= (f39 c_2 c_1) c_2))(or (= (f39 c_2 c_2) c_0)(= (f39 c_2 c_2) c_1)(= (f39 c_2 c_2) c_2))(or (= (f28 c_0 c_0) c_0)(= (f28 c_0 c_0) c_1)(= (f28 c_0 c_0) c_2))(or (= (f28 c_0 c_1) c_0)(= (f28 c_0 c_1) c_1)(= (f28 c_0 c_1) c_2))(or (= (f28 c_0 c_2) c_0)(= (f28 c_0 c_2) c_1)(= (f28 c_0 c_2) c_2))(or (= (f28 c_1 c_0) c_0)(= (f28 c_1 c_0) c_1)(= (f28 c_1 c_0) c_2))(or (= (f28 c_1 c_1) c_0)(= (f28 c_1 c_1) c_1)(= (f28 c_1 c_1) c_2))(or (= (f28 c_1 c_2) c_0)(= (f28 c_1 c_2) c_1)(= (f28 c_1 c_2) c_2))(or (= (f28 c_2 c_0) c_0)(= (f28 c_2 c_0) c_1)(= (f28 c_2 c_0) c_2))(or (= (f28 c_2 c_1) c_0)(= (f28 c_2 c_1) c_1)(= (f28 c_2 c_1) c_2))(or (= (f28 c_2 c_2) c_0)(= (f28 c_2 c_2) c_1)(= (f28 c_2 c_2) c_2))(or (= (f47 c_0 c_0) c_0)(= (f47 c_0 c_0) c_1)(= (f47 c_0 c_0) c_2))(or (= (f47 c_0 c_1) c_0)(= (f47 c_0 c_1) c_1)(= (f47 c_0 c_1) c_2))(or (= (f47 c_0 c_2) c_0)(= (f47 c_0 c_2) c_1)(= (f47 c_0 c_2) c_2))(or (= (f47 c_1 c_0) c_0)(= (f47 c_1 c_0) c_1)(= (f47 c_1 c_0) c_2))(or (= (f47 c_1 c_1) c_0)(= (f47 c_1 c_1) c_1)(= (f47 c_1 c_1) c_2))(or (= (f47 c_1 c_2) c_0)(= (f47 c_1 c_2) c_1)(= (f47 c_1 c_2) c_2))(or (= (f47 c_2 c_0) c_0)(= (f47 c_2 c_0) c_1)(= (f47 c_2 c_0) c_2))(or (= (f47 c_2 c_1) c_0)(= (f47 c_2 c_1) c_1)(= (f47 c_2 c_1) c_2))(or (= (f47 c_2 c_2) c_0)(= (f47 c_2 c_2) c_1)(= (f47 c_2 c_2) c_2))(or (= (f44 c_0 c_0) c_0)(= (f44 c_0 c_0) c_1)(= (f44 c_0 c_0) c_2))(or (= (f44 c_0 c_1) c_0)(= (f44 c_0 c_1) c_1)(= (f44 c_0 c_1) c_2))(or (= (f44 c_0 c_2) c_0)(= (f44 c_0 c_2) c_1)(= (f44 c_0 c_2) c_2))(or (= (f44 c_1 c_0) c_0)(= (f44 c_1 c_0) c_1)(= (f44 c_1 c_0) c_2))(or (= (f44 c_1 c_1) c_0)(= (f44 c_1 c_1) c_1)(= (f44 c_1 c_1) c_2))(or (= (f44 c_1 c_2) c_0)(= (f44 c_1 c_2) c_1)(= (f44 c_1 c_2) c_2))(or (= (f44 c_2 c_0) c_0)(= (f44 c_2 c_0) c_1)(= (f44 c_2 c_0) c_2))(or (= (f44 c_2 c_1) c_0)(= (f44 c_2 c_1) c_1)(= (f44 c_2 c_1) c_2))(or (= (f44 c_2 c_2) c_0)(= (f44 c_2 c_2) c_1)(= (f44 c_2 c_2) c_2))(or (= (f45 c_0 c_0) c_0)(= (f45 c_0 c_0) c_1)(= (f45 c_0 c_0) c_2))(or (= (f45 c_0 c_1) c_0)(= (f45 c_0 c_1) c_1)(= (f45 c_0 c_1) c_2))(or (= (f45 c_0 c_2) c_0)(= (f45 c_0 c_2) c_1)(= (f45 c_0 c_2) c_2))(or (= (f45 c_1 c_0) c_0)(= (f45 c_1 c_0) c_1)(= (f45 c_1 c_0) c_2))(or (= (f45 c_1 c_1) c_0)(= (f45 c_1 c_1) c_1)(= (f45 c_1 c_1) c_2))(or (= (f45 c_1 c_2) c_0)(= (f45 c_1 c_2) c_1)(= (f45 c_1 c_2) c_2))(or (= (f45 c_2 c_0) c_0)(= (f45 c_2 c_0) c_1)(= (f45 c_2 c_0) c_2))(or (= (f45 c_2 c_1) c_0)(= (f45 c_2 c_1) c_1)(= (f45 c_2 c_1) c_2))(or (= (f45 c_2 c_2) c_0)(= (f45 c_2 c_2) c_1)(= (f45 c_2 c_2) c_2))(or (= (f30 c_0 c_0) c_0)(= (f30 c_0 c_0) c_1)(= (f30 c_0 c_0) c_2))(or (= (f30 c_0 c_1) c_0)(= (f30 c_0 c_1) c_1)(= (f30 c_0 c_1) c_2))(or (= (f30 c_0 c_2) c_0)(= (f30 c_0 c_2) c_1)(= (f30 c_0 c_2) c_2))(or (= (f30 c_1 c_0) c_0)(= (f30 c_1 c_0) c_1)(= (f30 c_1 c_0) c_2))(or (= (f30 c_1 c_1) c_0)(= (f30 c_1 c_1) c_1)(= (f30 c_1 c_1) c_2))(or (= (f30 c_1 c_2) c_0)(= (f30 c_1 c_2) c_1)(= (f30 c_1 c_2) c_2))(or (= (f30 c_2 c_0) c_0)(= (f30 c_2 c_0) c_1)(= (f30 c_2 c_0) c_2))(or (= (f30 c_2 c_1) c_0)(= (f30 c_2 c_1) c_1)(= (f30 c_2 c_1) c_2))(or (= (f30 c_2 c_2) c_0)(= (f30 c_2 c_2) c_1)(= (f30 c_2 c_2) c_2))(or (= (f46 c_0 c_0) c_0)(= (f46 c_0 c_0) c_1)(= (f46 c_0 c_0) c_2))(or (= (f46 c_0 c_1) c_0)(= (f46 c_0 c_1) c_1)(= (f46 c_0 c_1) c_2))(or (= (f46 c_0 c_2) c_0)(= (f46 c_0 c_2) c_1)(= (f46 c_0 c_2) c_2))(or (= (f46 c_1 c_0) c_0)(= (f46 c_1 c_0) c_1)(= (f46 c_1 c_0) c_2))(or (= (f46 c_1 c_1) c_0)(= (f46 c_1 c_1) c_1)(= (f46 c_1 c_1) c_2))(or (= (f46 c_1 c_2) c_0)(= (f46 c_1 c_2) c_1)(= (f46 c_1 c_2) c_2))(or (= (f46 c_2 c_0) c_0)(= (f46 c_2 c_0) c_1)(= (f46 c_2 c_0) c_2))(or (= (f46 c_2 c_1) c_0)(= (f46 c_2 c_1) c_1)(= (f46 c_2 c_1) c_2))(or (= (f46 c_2 c_2) c_0)(= (f46 c_2 c_2) c_1)(= (f46 c_2 c_2) c_2))(or (= (f38 c_0 c_0) c_0)(= (f38 c_0 c_0) c_1)(= (f38 c_0 c_0) c_2))(or (= (f38 c_0 c_1) c_0)(= (f38 c_0 c_1) c_1)(= (f38 c_0 c_1) c_2))(or (= (f38 c_0 c_2) c_0)(= (f38 c_0 c_2) c_1)(= (f38 c_0 c_2) c_2))(or (= (f38 c_1 c_0) c_0)(= (f38 c_1 c_0) c_1)(= (f38 c_1 c_0) c_2))(or (= (f38 c_1 c_1) c_0)(= (f38 c_1 c_1) c_1)(= (f38 c_1 c_1) c_2))(or (= (f38 c_1 c_2) c_0)(= (f38 c_1 c_2) c_1)(= (f38 c_1 c_2) c_2))(or (= (f38 c_2 c_0) c_0)(= (f38 c_2 c_0) c_1)(= (f38 c_2 c_0) c_2))(or (= (f38 c_2 c_1) c_0)(= (f38 c_2 c_1) c_1)(= (f38 c_2 c_1) c_2))(or (= (f38 c_2 c_2) c_0)(= (f38 c_2 c_2) c_1)(= (f38 c_2 c_2) c_2))(or (= (f48 c_0 c_0) c_0)(= (f48 c_0 c_0) c_1)(= (f48 c_0 c_0) c_2))(or (= (f48 c_0 c_1) c_0)(= (f48 c_0 c_1) c_1)(= (f48 c_0 c_1) c_2))(or (= (f48 c_0 c_2) c_0)(= (f48 c_0 c_2) c_1)(= (f48 c_0 c_2) c_2))(or (= (f48 c_1 c_0) c_0)(= (f48 c_1 c_0) c_1)(= (f48 c_1 c_0) c_2))(or (= (f48 c_1 c_1) c_0)(= (f48 c_1 c_1) c_1)(= (f48 c_1 c_1) c_2))(or (= (f48 c_1 c_2) c_0)(= (f48 c_1 c_2) c_1)(= (f48 c_1 c_2) c_2))(or (= (f48 c_2 c_0) c_0)(= (f48 c_2 c_0) c_1)(= (f48 c_2 c_0) c_2))(or (= (f48 c_2 c_1) c_0)(= (f48 c_2 c_1) c_1)(= (f48 c_2 c_1) c_2))(or (= (f48 c_2 c_2) c_0)(= (f48 c_2 c_2) c_1)(= (f48 c_2 c_2) c_2))(or (= (f20 c_0) c_0)(= (f20 c_0) c_1)(= (f20 c_0) c_2))(or (= (f20 c_1) c_0)(= (f20 c_1) c_1)(= (f20 c_1) c_2))(or (= (f20 c_2) c_0)(= (f20 c_2) c_1)(= (f20 c_2) c_2))(or (= (f11 c_0) c_0)(= (f11 c_0) c_1)(= (f11 c_0) c_2))(or (= (f11 c_1) c_0)(= (f11 c_1) c_1)(= (f11 c_1) c_2))(or (= (f11 c_2) c_0)(= (f11 c_2) c_1)(= (f11 c_2) c_2))(or (= (f23 c_0) c_0)(= (f23 c_0) c_1)(= (f23 c_0) c_2))(or (= (f23 c_1) c_0)(= (f23 c_1) c_1)(= (f23 c_1) c_2))(or (= (f23 c_2) c_0)(= (f23 c_2) c_1)(= (f23 c_2) c_2))(or (= (f17 c_0) c_0)(= (f17 c_0) c_1)(= (f17 c_0) c_2))(or (= (f17 c_1) c_0)(= (f17 c_1) c_1)(= (f17 c_1) c_2))(or (= (f17 c_2) c_0)(= (f17 c_2) c_1)(= (f17 c_2) c_2))(or (= (f24 c_0) c_0)(= (f24 c_0) c_1)(= (f24 c_0) c_2))(or (= (f24 c_1) c_0)(= (f24 c_1) c_1)(= (f24 c_1) c_2))(or (= (f24 c_2) c_0)(= (f24 c_2) c_1)(= (f24 c_2) c_2))(or (= (f19 c_0) c_0)(= (f19 c_0) c_1)(= (f19 c_0) c_2))(or (= (f19 c_1) c_0)(= (f19 c_1) c_1)(= (f19 c_1) c_2))(or (= (f19 c_2) c_0)(= (f19 c_2) c_1)(= (f19 c_2) c_2))(or (= (f2 c_0) c_0)(= (f2 c_0) c_1)(= (f2 c_0) c_2))(or (= (f2 c_1) c_0)(= (f2 c_1) c_1)(= (f2 c_1) c_2))(or (= (f2 c_2) c_0)(= (f2 c_2) c_1)(= (f2 c_2) c_2))(or (= (f18 c_0) c_0)(= (f18 c_0) c_1)(= (f18 c_0) c_2))(or (= (f18 c_1) c_0)(= (f18 c_1) c_1)(= (f18 c_1) c_2))(or (= (f18 c_2) c_0)(= (f18 c_2) c_1)(= (f18 c_2) c_2))(or (= (f13 c_0) c_0)(= (f13 c_0) c_1)(= (f13 c_0) c_2))(or (= (f13 c_1) c_0)(= (f13 c_1) c_1)(= (f13 c_1) c_2))(or (= (f13 c_2) c_0)(= (f13 c_2) c_1)(= (f13 c_2) c_2))(or (= (f7 c_0) c_0)(= (f7 c_0) c_1)(= (f7 c_0) c_2))(or (= (f7 c_1) c_0)(= (f7 c_1) c_1)(= (f7 c_1) c_2))(or (= (f7 c_2) c_0)(= (f7 c_2) c_1)(= (f7 c_2) c_2))(or (= (f16 c_0) c_0)(= (f16 c_0) c_1)(= (f16 c_0) c_2))(or (= (f16 c_1) c_0)(= (f16 c_1) c_1)(= (f16 c_1) c_2))(or (= (f16 c_2) c_0)(= (f16 c_2) c_1)(= (f16 c_2) c_2))(or (= (f40 c_0) c_0)(= (f40 c_0) c_1)(= (f40 c_0) c_2))(or (= (f40 c_1) c_0)(= (f40 c_1) c_1)(= (f40 c_1) c_2))(or (= (f40 c_2) c_0)(= (f40 c_2) c_1)(= (f40 c_2) c_2))(or (= (f9 c_0) c_0)(= (f9 c_0) c_1)(= (f9 c_0) c_2))(or (= (f9 c_1) c_0)(= (f9 c_1) c_1)(= (f9 c_1) c_2))(or (= (f9 c_2) c_0)(= (f9 c_2) c_1)(= (f9 c_2) c_2))(or (= (f14 c_0) c_0)(= (f14 c_0) c_1)(= (f14 c_0) c_2))(or (= (f14 c_1) c_0)(= (f14 c_1) c_1)(= (f14 c_1) c_2))(or (= (f14 c_2) c_0)(= (f14 c_2) c_1)(= (f14 c_2) c_2))(or (= (f10 c_0) c_0)(= (f10 c_0) c_1)(= (f10 c_0) c_2))(or (= (f10 c_1) c_0)(= (f10 c_1) c_1)(= (f10 c_1) c_2))(or (= (f10 c_2) c_0)(= (f10 c_2) c_1)(= (f10 c_2) c_2))(or (= (f33 c_0) c_0)(= (f33 c_0) c_1)(= (f33 c_0) c_2))(or (= (f33 c_1) c_0)(= (f33 c_1) c_1)(= (f33 c_1) c_2))(or (= (f33 c_2) c_0)(= (f33 c_2) c_1)(= (f33 c_2) c_2))(or (= (f1 c_0) c_0)(= (f1 c_0) c_1)(= (f1 c_0) c_2))(or (= (f1 c_1) c_0)(= (f1 c_1) c_1)(= (f1 c_1) c_2))(or (= (f1 c_2) c_0)(= (f1 c_2) c_1)(= (f1 c_2) c_2))(or (= (f27 c_0) c_0)(= (f27 c_0) c_1)(= (f27 c_0) c_2))(or (= (f27 c_1) c_0)(= (f27 c_1) c_1)(= (f27 c_1) c_2))(or (= (f27 c_2) c_0)(= (f27 c_2) c_1)(= (f27 c_2) c_2))(or (= (f32 c_0) c_0)(= (f32 c_0) c_1)(= (f32 c_0) c_2))(or (= (f32 c_1) c_0)(= (f32 c_1) c_1)(= (f32 c_1) c_2))(or (= (f32 c_2) c_0)(= (f32 c_2) c_1)(= (f32 c_2) c_2))(or (= c6 c_0)(= c6 c_1)(= c6 c_2))(or (= c15 c_0)(= c15 c_1)(= c15 c_2))(or (= c8 c_0)(= c8 c_1)(= c8 c_2))(or (= c5 c_0)(= c5 c_1)(= c5 c_2))(or (= c49 c_0)(= c49 c_1)(= c49 c_2))(or (= c41 c_0)(= c41 c_1)(= c41 c_2))(or (= c42 c_0)(= c42 c_1)(= c42 c_2))(or (= c29 c_0)(= c29 c_1)(= c29 c_2))))