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

This benchmark was obtained by trying to find a finite model of a first-order 
formula (Albert Oliveras).
}
:status sat
:logic QF_UF
:extrafuns ((f1 U U U))
:extrafuns ((f2 U U U))
:extrafuns ((f3 U U))
:extrafuns ((c6 U))
:extrafuns ((c7 U))
:extrafuns ((c4 U))
:extrafuns ((c5 U))
:extrafuns ((c_0 U))
:extrafuns ((c_1 U))
:extrafuns ((c_2 U))
:extrafuns ((c_3 U))
:extrafuns ((c_4 U))
:extrafuns ((c_5 U))
:extrafuns ((c_6 U))
:extrafuns ((c_7 U))
:formula 
( and 
( distinct c_0 c_1 c_2 c_3 c_4 c_5 c_6 c_7 )(= (f2 c_0 (f1 c_0 c_0)) c_0) (= (f2 c_0 (f1 c_0 c_1)) c_0) (= (f2 c_0 (f1 c_0 c_2)) c_0) (= (f2 c_0 (f1 c_0 c_3)) c_0) (= (f2 c_0 (f1 c_0 c_4)) c_0) (= (f2 c_0 (f1 c_0 c_5)) c_0) (= (f2 c_0 (f1 c_0 c_6)) c_0) (= (f2 c_0 (f1 c_0 c_7)) c_0) (= (f2 c_1 (f1 c_1 c_0)) c_1) (= (f2 c_1 (f1 c_1 c_1)) c_1) (= (f2 c_1 (f1 c_1 c_2)) c_1) (= (f2 c_1 (f1 c_1 c_3)) c_1) (= (f2 c_1 (f1 c_1 c_4)) c_1) (= (f2 c_1 (f1 c_1 c_5)) c_1) (= (f2 c_1 (f1 c_1 c_6)) c_1) (= (f2 c_1 (f1 c_1 c_7)) c_1) (= (f2 c_2 (f1 c_2 c_0)) c_2) (= (f2 c_2 (f1 c_2 c_1)) c_2) (= (f2 c_2 (f1 c_2 c_2)) c_2) (= (f2 c_2 (f1 c_2 c_3)) c_2) (= (f2 c_2 (f1 c_2 c_4)) c_2) (= (f2 c_2 (f1 c_2 c_5)) c_2) (= (f2 c_2 (f1 c_2 c_6)) c_2) (= (f2 c_2 (f1 c_2 c_7)) c_2) (= (f2 c_3 (f1 c_3 c_0)) c_3) (= (f2 c_3 (f1 c_3 c_1)) c_3) (= (f2 c_3 (f1 c_3 c_2)) c_3) (= (f2 c_3 (f1 c_3 c_3)) c_3) (= (f2 c_3 (f1 c_3 c_4)) c_3) (= (f2 c_3 (f1 c_3 c_5)) c_3) (= (f2 c_3 (f1 c_3 c_6)) c_3) (= (f2 c_3 (f1 c_3 c_7)) c_3) (= (f2 c_4 (f1 c_4 c_0)) c_4) (= (f2 c_4 (f1 c_4 c_1)) c_4) (= (f2 c_4 (f1 c_4 c_2)) c_4) (= (f2 c_4 (f1 c_4 c_3)) c_4) (= (f2 c_4 (f1 c_4 c_4)) c_4) (= (f2 c_4 (f1 c_4 c_5)) c_4) (= (f2 c_4 (f1 c_4 c_6)) c_4) (= (f2 c_4 (f1 c_4 c_7)) c_4) (= (f2 c_5 (f1 c_5 c_0)) c_5) (= (f2 c_5 (f1 c_5 c_1)) c_5) (= (f2 c_5 (f1 c_5 c_2)) c_5) (= (f2 c_5 (f1 c_5 c_3)) c_5) (= (f2 c_5 (f1 c_5 c_4)) c_5) (= (f2 c_5 (f1 c_5 c_5)) c_5) (= (f2 c_5 (f1 c_5 c_6)) c_5) (= (f2 c_5 (f1 c_5 c_7)) c_5) (= (f2 c_6 (f1 c_6 c_0)) c_6) (= (f2 c_6 (f1 c_6 c_1)) c_6) (= (f2 c_6 (f1 c_6 c_2)) c_6) (= (f2 c_6 (f1 c_6 c_3)) c_6) (= (f2 c_6 (f1 c_6 c_4)) c_6) (= (f2 c_6 (f1 c_6 c_5)) c_6) (= (f2 c_6 (f1 c_6 c_6)) c_6) (= (f2 c_6 (f1 c_6 c_7)) c_6) (= (f2 c_7 (f1 c_7 c_0)) c_7) (= (f2 c_7 (f1 c_7 c_1)) c_7) (= (f2 c_7 (f1 c_7 c_2)) c_7) (= (f2 c_7 (f1 c_7 c_3)) c_7) (= (f2 c_7 (f1 c_7 c_4)) c_7) (= (f2 c_7 (f1 c_7 c_5)) c_7) (= (f2 c_7 (f1 c_7 c_6)) c_7) (= (f2 c_7 (f1 c_7 c_7)) c_7) (= (f1 c_0 c_0) c_0) (= (f1 c_1 c_1) c_1) (= (f1 c_2 c_2) c_2) (= (f1 c_3 c_3) c_3) (= (f1 c_4 c_4) c_4) (= (f1 c_5 c_5) c_5) (= (f1 c_6 c_6) c_6) (= (f1 c_7 c_7) c_7) (= (f3 (f2 c_0 c_0)) (f1 (f3 c_0) (f3 c_0))) (= (f3 (f2 c_0 c_1)) (f1 (f3 c_0) (f3 c_1))) (= (f3 (f2 c_0 c_2)) (f1 (f3 c_0) (f3 c_2))) (= (f3 (f2 c_0 c_3)) (f1 (f3 c_0) (f3 c_3))) (= (f3 (f2 c_0 c_4)) (f1 (f3 c_0) (f3 c_4))) (= (f3 (f2 c_0 c_5)) (f1 (f3 c_0) (f3 c_5))) (= (f3 (f2 c_0 c_6)) (f1 (f3 c_0) (f3 c_6))) (= (f3 (f2 c_0 c_7)) (f1 (f3 c_0) (f3 c_7))) (= (f3 (f2 c_1 c_0)) (f1 (f3 c_1) (f3 c_0))) (= (f3 (f2 c_1 c_1)) (f1 (f3 c_1) (f3 c_1))) (= (f3 (f2 c_1 c_2)) (f1 (f3 c_1) (f3 c_2))) (= (f3 (f2 c_1 c_3)) (f1 (f3 c_1) (f3 c_3))) (= (f3 (f2 c_1 c_4)) (f1 (f3 c_1) (f3 c_4))) (= (f3 (f2 c_1 c_5)) (f1 (f3 c_1) (f3 c_5))) (= (f3 (f2 c_1 c_6)) (f1 (f3 c_1) (f3 c_6))) (= (f3 (f2 c_1 c_7)) (f1 (f3 c_1) (f3 c_7))) (= (f3 (f2 c_2 c_0)) (f1 (f3 c_2) (f3 c_0))) (= (f3 (f2 c_2 c_1)) (f1 (f3 c_2) (f3 c_1))) (= (f3 (f2 c_2 c_2)) (f1 (f3 c_2) (f3 c_2))) (= (f3 (f2 c_2 c_3)) (f1 (f3 c_2) (f3 c_3))) (= (f3 (f2 c_2 c_4)) (f1 (f3 c_2) (f3 c_4))) (= (f3 (f2 c_2 c_5)) (f1 (f3 c_2) (f3 c_5))) (= (f3 (f2 c_2 c_6)) (f1 (f3 c_2) (f3 c_6))) (= (f3 (f2 c_2 c_7)) (f1 (f3 c_2) (f3 c_7))) (= (f3 (f2 c_3 c_0)) (f1 (f3 c_3) (f3 c_0))) (= (f3 (f2 c_3 c_1)) (f1 (f3 c_3) (f3 c_1))) (= (f3 (f2 c_3 c_2)) (f1 (f3 c_3) (f3 c_2))) (= (f3 (f2 c_3 c_3)) (f1 (f3 c_3) (f3 c_3))) (= (f3 (f2 c_3 c_4)) (f1 (f3 c_3) (f3 c_4))) (= (f3 (f2 c_3 c_5)) (f1 (f3 c_3) (f3 c_5))) (= (f3 (f2 c_3 c_6)) (f1 (f3 c_3) (f3 c_6))) (= (f3 (f2 c_3 c_7)) (f1 (f3 c_3) (f3 c_7))) (= (f3 (f2 c_4 c_0)) (f1 (f3 c_4) (f3 c_0))) (= (f3 (f2 c_4 c_1)) (f1 (f3 c_4) (f3 c_1))) (= (f3 (f2 c_4 c_2)) (f1 (f3 c_4) (f3 c_2))) (= (f3 (f2 c_4 c_3)) (f1 (f3 c_4) (f3 c_3))) (= (f3 (f2 c_4 c_4)) (f1 (f3 c_4) (f3 c_4))) (= (f3 (f2 c_4 c_5)) (f1 (f3 c_4) (f3 c_5))) (= (f3 (f2 c_4 c_6)) (f1 (f3 c_4) (f3 c_6))) (= (f3 (f2 c_4 c_7)) (f1 (f3 c_4) (f3 c_7))) (= (f3 (f2 c_5 c_0)) (f1 (f3 c_5) (f3 c_0))) (= (f3 (f2 c_5 c_1)) (f1 (f3 c_5) (f3 c_1))) (= (f3 (f2 c_5 c_2)) (f1 (f3 c_5) (f3 c_2))) (= (f3 (f2 c_5 c_3)) (f1 (f3 c_5) (f3 c_3))) (= (f3 (f2 c_5 c_4)) (f1 (f3 c_5) (f3 c_4))) (= (f3 (f2 c_5 c_5)) (f1 (f3 c_5) (f3 c_5))) (= (f3 (f2 c_5 c_6)) (f1 (f3 c_5) (f3 c_6))) (= (f3 (f2 c_5 c_7)) (f1 (f3 c_5) (f3 c_7))) (= (f3 (f2 c_6 c_0)) (f1 (f3 c_6) (f3 c_0))) (= (f3 (f2 c_6 c_1)) (f1 (f3 c_6) (f3 c_1))) (= (f3 (f2 c_6 c_2)) (f1 (f3 c_6) (f3 c_2))) (= (f3 (f2 c_6 c_3)) (f1 (f3 c_6) (f3 c_3))) (= (f3 (f2 c_6 c_4)) (f1 (f3 c_6) (f3 c_4))) (= (f3 (f2 c_6 c_5)) (f1 (f3 c_6) (f3 c_5))) (= (f3 (f2 c_6 c_6)) (f1 (f3 c_6) (f3 c_6))) (= (f3 (f2 c_6 c_7)) (f1 (f3 c_6) (f3 c_7))) (= (f3 (f2 c_7 c_0)) (f1 (f3 c_7) (f3 c_0))) (= (f3 (f2 c_7 c_1)) (f1 (f3 c_7) (f3 c_1))) (= (f3 (f2 c_7 c_2)) (f1 (f3 c_7) (f3 c_2))) (= (f3 (f2 c_7 c_3)) (f1 (f3 c_7) (f3 c_3))) (= (f3 (f2 c_7 c_4)) (f1 (f3 c_7) (f3 c_4))) (= (f3 (f2 c_7 c_5)) (f1 (f3 c_7) (f3 c_5))) (= (f3 (f2 c_7 c_6)) (f1 (f3 c_7) (f3 c_6))) (= (f3 (f2 c_7 c_7)) (f1 (f3 c_7) (f3 c_7))) (not (= (f2 (f1 (f3 c6) (f2 c6 c7)) (f2 (f3 c7) (f1 c6 c7))) c4)) (= (f2 (f2 c_0 c_0) c_0) (f2 c_0 (f2 c_0 c_0))) (= (f2 (f2 c_0 c_0) c_1) (f2 c_0 (f2 c_0 c_1))) (= (f2 (f2 c_0 c_0) c_2) (f2 c_0 (f2 c_0 c_2))) (= (f2 (f2 c_0 c_0) c_3) (f2 c_0 (f2 c_0 c_3))) (= (f2 (f2 c_0 c_0) c_4) (f2 c_0 (f2 c_0 c_4))) (= (f2 (f2 c_0 c_0) c_5) (f2 c_0 (f2 c_0 c_5))) (= (f2 (f2 c_0 c_0) c_6) (f2 c_0 (f2 c_0 c_6))) (= (f2 (f2 c_0 c_0) c_7) (f2 c_0 (f2 c_0 c_7))) (= (f2 (f2 c_0 c_1) c_0) (f2 c_0 (f2 c_1 c_0))) (= (f2 (f2 c_0 c_1) c_1) (f2 c_0 (f2 c_1 c_1))) (= (f2 (f2 c_0 c_1) c_2) (f2 c_0 (f2 c_1 c_2))) (= (f2 (f2 c_0 c_1) c_3) (f2 c_0 (f2 c_1 c_3))) (= (f2 (f2 c_0 c_1) c_4) (f2 c_0 (f2 c_1 c_4))) (= (f2 (f2 c_0 c_1) c_5) (f2 c_0 (f2 c_1 c_5))) (= (f2 (f2 c_0 c_1) c_6) (f2 c_0 (f2 c_1 c_6))) (= (f2 (f2 c_0 c_1) c_7) (f2 c_0 (f2 c_1 c_7))) (= (f2 (f2 c_0 c_2) c_0) (f2 c_0 (f2 c_2 c_0))) (= (f2 (f2 c_0 c_2) c_1) (f2 c_0 (f2 c_2 c_1))) (= (f2 (f2 c_0 c_2) c_2) (f2 c_0 (f2 c_2 c_2))) (= (f2 (f2 c_0 c_2) c_3) (f2 c_0 (f2 c_2 c_3))) (= (f2 (f2 c_0 c_2) c_4) (f2 c_0 (f2 c_2 c_4))) (= (f2 (f2 c_0 c_2) c_5) (f2 c_0 (f2 c_2 c_5))) (= (f2 (f2 c_0 c_2) c_6) (f2 c_0 (f2 c_2 c_6))) (= (f2 (f2 c_0 c_2) c_7) (f2 c_0 (f2 c_2 c_7))) (= (f2 (f2 c_0 c_3) c_0) (f2 c_0 (f2 c_3 c_0))) (= (f2 (f2 c_0 c_3) c_1) (f2 c_0 (f2 c_3 c_1))) (= (f2 (f2 c_0 c_3) c_2) (f2 c_0 (f2 c_3 c_2))) (= (f2 (f2 c_0 c_3) c_3) (f2 c_0 (f2 c_3 c_3))) (= (f2 (f2 c_0 c_3) c_4) (f2 c_0 (f2 c_3 c_4))) (= (f2 (f2 c_0 c_3) c_5) (f2 c_0 (f2 c_3 c_5))) (= (f2 (f2 c_0 c_3) c_6) (f2 c_0 (f2 c_3 c_6))) (= (f2 (f2 c_0 c_3) c_7) (f2 c_0 (f2 c_3 c_7))) (= (f2 (f2 c_0 c_4) c_0) (f2 c_0 (f2 c_4 c_0))) (= (f2 (f2 c_0 c_4) c_1) (f2 c_0 (f2 c_4 c_1))) (= (f2 (f2 c_0 c_4) c_2) (f2 c_0 (f2 c_4 c_2))) (= (f2 (f2 c_0 c_4) c_3) (f2 c_0 (f2 c_4 c_3))) (= (f2 (f2 c_0 c_4) c_4) (f2 c_0 (f2 c_4 c_4))) (= (f2 (f2 c_0 c_4) c_5) (f2 c_0 (f2 c_4 c_5))) (= (f2 (f2 c_0 c_4) c_6) (f2 c_0 (f2 c_4 c_6))) (= (f2 (f2 c_0 c_4) c_7) (f2 c_0 (f2 c_4 c_7))) (= (f2 (f2 c_0 c_5) c_0) (f2 c_0 (f2 c_5 c_0))) (= (f2 (f2 c_0 c_5) c_1) (f2 c_0 (f2 c_5 c_1))) (= (f2 (f2 c_0 c_5) c_2) (f2 c_0 (f2 c_5 c_2))) (= (f2 (f2 c_0 c_5) c_3) (f2 c_0 (f2 c_5 c_3))) (= (f2 (f2 c_0 c_5) c_4) (f2 c_0 (f2 c_5 c_4))) (= (f2 (f2 c_0 c_5) c_5) (f2 c_0 (f2 c_5 c_5))) (= (f2 (f2 c_0 c_5) c_6) (f2 c_0 (f2 c_5 c_6))) (= (f2 (f2 c_0 c_5) c_7) (f2 c_0 (f2 c_5 c_7))) (= (f2 (f2 c_0 c_6) c_0) (f2 c_0 (f2 c_6 c_0))) (= (f2 (f2 c_0 c_6) c_1) (f2 c_0 (f2 c_6 c_1))) (= (f2 (f2 c_0 c_6) c_2) (f2 c_0 (f2 c_6 c_2))) (= (f2 (f2 c_0 c_6) c_3) (f2 c_0 (f2 c_6 c_3))) (= (f2 (f2 c_0 c_6) c_4) (f2 c_0 (f2 c_6 c_4))) (= (f2 (f2 c_0 c_6) c_5) (f2 c_0 (f2 c_6 c_5))) (= (f2 (f2 c_0 c_6) c_6) (f2 c_0 (f2 c_6 c_6))) (= (f2 (f2 c_0 c_6) c_7) (f2 c_0 (f2 c_6 c_7))) (= (f2 (f2 c_0 c_7) c_0) (f2 c_0 (f2 c_7 c_0))) (= (f2 (f2 c_0 c_7) c_1) (f2 c_0 (f2 c_7 c_1))) (= (f2 (f2 c_0 c_7) c_2) (f2 c_0 (f2 c_7 c_2))) (= (f2 (f2 c_0 c_7) c_3) (f2 c_0 (f2 c_7 c_3))) (= (f2 (f2 c_0 c_7) c_4) (f2 c_0 (f2 c_7 c_4))) (= (f2 (f2 c_0 c_7) c_5) (f2 c_0 (f2 c_7 c_5))) (= (f2 (f2 c_0 c_7) c_6) (f2 c_0 (f2 c_7 c_6))) (= (f2 (f2 c_0 c_7) c_7) (f2 c_0 (f2 c_7 c_7))) (= (f2 (f2 c_1 c_0) c_0) (f2 c_1 (f2 c_0 c_0))) (= (f2 (f2 c_1 c_0) c_1) (f2 c_1 (f2 c_0 c_1))) (= (f2 (f2 c_1 c_0) c_2) (f2 c_1 (f2 c_0 c_2))) (= (f2 (f2 c_1 c_0) c_3) (f2 c_1 (f2 c_0 c_3))) (= (f2 (f2 c_1 c_0) c_4) (f2 c_1 (f2 c_0 c_4))) (= (f2 (f2 c_1 c_0) c_5) (f2 c_1 (f2 c_0 c_5))) (= (f2 (f2 c_1 c_0) c_6) (f2 c_1 (f2 c_0 c_6))) (= (f2 (f2 c_1 c_0) c_7) (f2 c_1 (f2 c_0 c_7))) (= (f2 (f2 c_1 c_1) c_0) (f2 c_1 (f2 c_1 c_0))) (= (f2 (f2 c_1 c_1) c_1) (f2 c_1 (f2 c_1 c_1))) (= (f2 (f2 c_1 c_1) c_2) (f2 c_1 (f2 c_1 c_2))) (= (f2 (f2 c_1 c_1) c_3) (f2 c_1 (f2 c_1 c_3))) (= (f2 (f2 c_1 c_1) c_4) (f2 c_1 (f2 c_1 c_4))) (= (f2 (f2 c_1 c_1) c_5) (f2 c_1 (f2 c_1 c_5))) (= (f2 (f2 c_1 c_1) c_6) (f2 c_1 (f2 c_1 c_6))) (= (f2 (f2 c_1 c_1) c_7) (f2 c_1 (f2 c_1 c_7))) (= (f2 (f2 c_1 c_2) c_0) (f2 c_1 (f2 c_2 c_0))) (= (f2 (f2 c_1 c_2) c_1) (f2 c_1 (f2 c_2 c_1))) (= (f2 (f2 c_1 c_2) c_2) (f2 c_1 (f2 c_2 c_2))) (= (f2 (f2 c_1 c_2) c_3) (f2 c_1 (f2 c_2 c_3))) (= (f2 (f2 c_1 c_2) c_4) (f2 c_1 (f2 c_2 c_4))) (= (f2 (f2 c_1 c_2) c_5) (f2 c_1 (f2 c_2 c_5))) (= (f2 (f2 c_1 c_2) c_6) (f2 c_1 (f2 c_2 c_6))) (= (f2 (f2 c_1 c_2) c_7) (f2 c_1 (f2 c_2 c_7))) (= (f2 (f2 c_1 c_3) c_0) (f2 c_1 (f2 c_3 c_0))) (= (f2 (f2 c_1 c_3) c_1) (f2 c_1 (f2 c_3 c_1))) (= (f2 (f2 c_1 c_3) c_2) (f2 c_1 (f2 c_3 c_2))) (= (f2 (f2 c_1 c_3) c_3) (f2 c_1 (f2 c_3 c_3))) (= (f2 (f2 c_1 c_3) c_4) (f2 c_1 (f2 c_3 c_4))) (= (f2 (f2 c_1 c_3) c_5) (f2 c_1 (f2 c_3 c_5))) (= (f2 (f2 c_1 c_3) c_6) (f2 c_1 (f2 c_3 c_6))) (= (f2 (f2 c_1 c_3) c_7) (f2 c_1 (f2 c_3 c_7))) (= (f2 (f2 c_1 c_4) c_0) (f2 c_1 (f2 c_4 c_0))) (= (f2 (f2 c_1 c_4) c_1) (f2 c_1 (f2 c_4 c_1))) (= (f2 (f2 c_1 c_4) c_2) (f2 c_1 (f2 c_4 c_2))) (= (f2 (f2 c_1 c_4) c_3) (f2 c_1 (f2 c_4 c_3))) (= (f2 (f2 c_1 c_4) c_4) (f2 c_1 (f2 c_4 c_4))) (= (f2 (f2 c_1 c_4) c_5) (f2 c_1 (f2 c_4 c_5))) (= (f2 (f2 c_1 c_4) c_6) (f2 c_1 (f2 c_4 c_6))) (= (f2 (f2 c_1 c_4) c_7) (f2 c_1 (f2 c_4 c_7))) (= (f2 (f2 c_1 c_5) c_0) (f2 c_1 (f2 c_5 c_0))) (= (f2 (f2 c_1 c_5) c_1) (f2 c_1 (f2 c_5 c_1))) (= (f2 (f2 c_1 c_5) c_2) (f2 c_1 (f2 c_5 c_2))) (= (f2 (f2 c_1 c_5) c_3) (f2 c_1 (f2 c_5 c_3))) (= (f2 (f2 c_1 c_5) c_4) (f2 c_1 (f2 c_5 c_4))) (= (f2 (f2 c_1 c_5) c_5) (f2 c_1 (f2 c_5 c_5))) (= (f2 (f2 c_1 c_5) c_6) (f2 c_1 (f2 c_5 c_6))) (= (f2 (f2 c_1 c_5) c_7) (f2 c_1 (f2 c_5 c_7))) (= (f2 (f2 c_1 c_6) c_0) (f2 c_1 (f2 c_6 c_0))) (= (f2 (f2 c_1 c_6) c_1) (f2 c_1 (f2 c_6 c_1))) (= (f2 (f2 c_1 c_6) c_2) (f2 c_1 (f2 c_6 c_2))) (= (f2 (f2 c_1 c_6) c_3) (f2 c_1 (f2 c_6 c_3))) (= (f2 (f2 c_1 c_6) c_4) (f2 c_1 (f2 c_6 c_4))) (= (f2 (f2 c_1 c_6) c_5) (f2 c_1 (f2 c_6 c_5))) (= (f2 (f2 c_1 c_6) c_6) (f2 c_1 (f2 c_6 c_6))) (= (f2 (f2 c_1 c_6) c_7) (f2 c_1 (f2 c_6 c_7))) (= (f2 (f2 c_1 c_7) c_0) (f2 c_1 (f2 c_7 c_0))) (= (f2 (f2 c_1 c_7) c_1) (f2 c_1 (f2 c_7 c_1))) (= (f2 (f2 c_1 c_7) c_2) (f2 c_1 (f2 c_7 c_2))) (= (f2 (f2 c_1 c_7) c_3) (f2 c_1 (f2 c_7 c_3))) (= (f2 (f2 c_1 c_7) c_4) (f2 c_1 (f2 c_7 c_4))) (= (f2 (f2 c_1 c_7) c_5) (f2 c_1 (f2 c_7 c_5))) (= (f2 (f2 c_1 c_7) c_6) (f2 c_1 (f2 c_7 c_6))) (= (f2 (f2 c_1 c_7) c_7) (f2 c_1 (f2 c_7 c_7))) (= (f2 (f2 c_2 c_0) c_0) (f2 c_2 (f2 c_0 c_0))) (= (f2 (f2 c_2 c_0) c_1) (f2 c_2 (f2 c_0 c_1))) (= (f2 (f2 c_2 c_0) c_2) (f2 c_2 (f2 c_0 c_2))) (= (f2 (f2 c_2 c_0) c_3) (f2 c_2 (f2 c_0 c_3))) (= (f2 (f2 c_2 c_0) c_4) (f2 c_2 (f2 c_0 c_4))) (= (f2 (f2 c_2 c_0) c_5) (f2 c_2 (f2 c_0 c_5))) (= (f2 (f2 c_2 c_0) c_6) (f2 c_2 (f2 c_0 c_6))) (= (f2 (f2 c_2 c_0) c_7) (f2 c_2 (f2 c_0 c_7))) (= (f2 (f2 c_2 c_1) c_0) (f2 c_2 (f2 c_1 c_0))) (= (f2 (f2 c_2 c_1) c_1) (f2 c_2 (f2 c_1 c_1))) (= (f2 (f2 c_2 c_1) c_2) (f2 c_2 (f2 c_1 c_2))) (= (f2 (f2 c_2 c_1) c_3) (f2 c_2 (f2 c_1 c_3))) (= (f2 (f2 c_2 c_1) c_4) (f2 c_2 (f2 c_1 c_4))) (= (f2 (f2 c_2 c_1) c_5) (f2 c_2 (f2 c_1 c_5))) (= (f2 (f2 c_2 c_1) c_6) (f2 c_2 (f2 c_1 c_6))) (= (f2 (f2 c_2 c_1) c_7) (f2 c_2 (f2 c_1 c_7))) (= (f2 (f2 c_2 c_2) c_0) (f2 c_2 (f2 c_2 c_0))) (= (f2 (f2 c_2 c_2) c_1) (f2 c_2 (f2 c_2 c_1))) (= (f2 (f2 c_2 c_2) c_2) (f2 c_2 (f2 c_2 c_2))) (= (f2 (f2 c_2 c_2) c_3) (f2 c_2 (f2 c_2 c_3))) (= (f2 (f2 c_2 c_2) c_4) (f2 c_2 (f2 c_2 c_4))) (= (f2 (f2 c_2 c_2) c_5) (f2 c_2 (f2 c_2 c_5))) (= (f2 (f2 c_2 c_2) c_6) (f2 c_2 (f2 c_2 c_6))) (= (f2 (f2 c_2 c_2) c_7) (f2 c_2 (f2 c_2 c_7))) (= (f2 (f2 c_2 c_3) c_0) (f2 c_2 (f2 c_3 c_0))) (= (f2 (f2 c_2 c_3) c_1) (f2 c_2 (f2 c_3 c_1))) (= (f2 (f2 c_2 c_3) c_2) (f2 c_2 (f2 c_3 c_2))) (= (f2 (f2 c_2 c_3) c_3) (f2 c_2 (f2 c_3 c_3))) (= (f2 (f2 c_2 c_3) c_4) (f2 c_2 (f2 c_3 c_4))) (= (f2 (f2 c_2 c_3) c_5) (f2 c_2 (f2 c_3 c_5))) (= (f2 (f2 c_2 c_3) c_6) (f2 c_2 (f2 c_3 c_6))) (= (f2 (f2 c_2 c_3) c_7) (f2 c_2 (f2 c_3 c_7))) (= (f2 (f2 c_2 c_4) c_0) (f2 c_2 (f2 c_4 c_0))) (= (f2 (f2 c_2 c_4) c_1) (f2 c_2 (f2 c_4 c_1))) (= (f2 (f2 c_2 c_4) c_2) (f2 c_2 (f2 c_4 c_2))) (= (f2 (f2 c_2 c_4) c_3) (f2 c_2 (f2 c_4 c_3))) (= (f2 (f2 c_2 c_4) c_4) (f2 c_2 (f2 c_4 c_4))) (= (f2 (f2 c_2 c_4) c_5) (f2 c_2 (f2 c_4 c_5))) (= (f2 (f2 c_2 c_4) c_6) (f2 c_2 (f2 c_4 c_6))) (= (f2 (f2 c_2 c_4) c_7) (f2 c_2 (f2 c_4 c_7))) (= (f2 (f2 c_2 c_5) c_0) (f2 c_2 (f2 c_5 c_0))) (= (f2 (f2 c_2 c_5) c_1) (f2 c_2 (f2 c_5 c_1))) (= (f2 (f2 c_2 c_5) c_2) (f2 c_2 (f2 c_5 c_2))) (= (f2 (f2 c_2 c_5) c_3) (f2 c_2 (f2 c_5 c_3))) (= (f2 (f2 c_2 c_5) c_4) (f2 c_2 (f2 c_5 c_4))) (= (f2 (f2 c_2 c_5) c_5) (f2 c_2 (f2 c_5 c_5))) (= (f2 (f2 c_2 c_5) c_6) (f2 c_2 (f2 c_5 c_6))) (= (f2 (f2 c_2 c_5) c_7) (f2 c_2 (f2 c_5 c_7))) (= (f2 (f2 c_2 c_6) c_0) (f2 c_2 (f2 c_6 c_0))) (= (f2 (f2 c_2 c_6) c_1) (f2 c_2 (f2 c_6 c_1))) (= (f2 (f2 c_2 c_6) c_2) (f2 c_2 (f2 c_6 c_2))) (= (f2 (f2 c_2 c_6) c_3) (f2 c_2 (f2 c_6 c_3))) (= (f2 (f2 c_2 c_6) c_4) (f2 c_2 (f2 c_6 c_4))) (= (f2 (f2 c_2 c_6) c_5) (f2 c_2 (f2 c_6 c_5))) (= (f2 (f2 c_2 c_6) c_6) (f2 c_2 (f2 c_6 c_6))) (= (f2 (f2 c_2 c_6) c_7) (f2 c_2 (f2 c_6 c_7))) (= (f2 (f2 c_2 c_7) c_0) (f2 c_2 (f2 c_7 c_0))) (= (f2 (f2 c_2 c_7) c_1) (f2 c_2 (f2 c_7 c_1))) (= (f2 (f2 c_2 c_7) c_2) (f2 c_2 (f2 c_7 c_2))) (= (f2 (f2 c_2 c_7) c_3) (f2 c_2 (f2 c_7 c_3))) (= (f2 (f2 c_2 c_7) c_4) (f2 c_2 (f2 c_7 c_4))) (= (f2 (f2 c_2 c_7) c_5) (f2 c_2 (f2 c_7 c_5))) (= (f2 (f2 c_2 c_7) c_6) (f2 c_2 (f2 c_7 c_6))) (= (f2 (f2 c_2 c_7) c_7) (f2 c_2 (f2 c_7 c_7))) (= (f2 (f2 c_3 c_0) c_0) (f2 c_3 (f2 c_0 c_0))) (= (f2 (f2 c_3 c_0) c_1) (f2 c_3 (f2 c_0 c_1))) (= (f2 (f2 c_3 c_0) c_2) (f2 c_3 (f2 c_0 c_2))) (= (f2 (f2 c_3 c_0) c_3) (f2 c_3 (f2 c_0 c_3))) (= (f2 (f2 c_3 c_0) c_4) (f2 c_3 (f2 c_0 c_4))) (= (f2 (f2 c_3 c_0) c_5) (f2 c_3 (f2 c_0 c_5))) (= (f2 (f2 c_3 c_0) c_6) (f2 c_3 (f2 c_0 c_6))) (= (f2 (f2 c_3 c_0) c_7) (f2 c_3 (f2 c_0 c_7))) (= (f2 (f2 c_3 c_1) c_0) (f2 c_3 (f2 c_1 c_0))) (= (f2 (f2 c_3 c_1) c_1) (f2 c_3 (f2 c_1 c_1))) (= (f2 (f2 c_3 c_1) c_2) (f2 c_3 (f2 c_1 c_2))) (= (f2 (f2 c_3 c_1) c_3) (f2 c_3 (f2 c_1 c_3))) (= (f2 (f2 c_3 c_1) c_4) (f2 c_3 (f2 c_1 c_4))) (= (f2 (f2 c_3 c_1) c_5) (f2 c_3 (f2 c_1 c_5))) (= (f2 (f2 c_3 c_1) c_6) (f2 c_3 (f2 c_1 c_6))) (= (f2 (f2 c_3 c_1) c_7) (f2 c_3 (f2 c_1 c_7))) (= (f2 (f2 c_3 c_2) c_0) (f2 c_3 (f2 c_2 c_0))) (= (f2 (f2 c_3 c_2) c_1) (f2 c_3 (f2 c_2 c_1))) (= (f2 (f2 c_3 c_2) c_2) (f2 c_3 (f2 c_2 c_2))) (= (f2 (f2 c_3 c_2) c_3) (f2 c_3 (f2 c_2 c_3))) (= (f2 (f2 c_3 c_2) c_4) (f2 c_3 (f2 c_2 c_4))) (= (f2 (f2 c_3 c_2) c_5) (f2 c_3 (f2 c_2 c_5))) (= (f2 (f2 c_3 c_2) c_6) (f2 c_3 (f2 c_2 c_6))) (= (f2 (f2 c_3 c_2) c_7) (f2 c_3 (f2 c_2 c_7))) (= (f2 (f2 c_3 c_3) c_0) (f2 c_3 (f2 c_3 c_0))) (= (f2 (f2 c_3 c_3) c_1) (f2 c_3 (f2 c_3 c_1))) (= (f2 (f2 c_3 c_3) c_2) (f2 c_3 (f2 c_3 c_2))) (= (f2 (f2 c_3 c_3) c_3) (f2 c_3 (f2 c_3 c_3))) (= (f2 (f2 c_3 c_3) c_4) (f2 c_3 (f2 c_3 c_4))) (= (f2 (f2 c_3 c_3) c_5) (f2 c_3 (f2 c_3 c_5))) (= (f2 (f2 c_3 c_3) c_6) (f2 c_3 (f2 c_3 c_6))) (= (f2 (f2 c_3 c_3) c_7) (f2 c_3 (f2 c_3 c_7))) (= (f2 (f2 c_3 c_4) c_0) (f2 c_3 (f2 c_4 c_0))) (= (f2 (f2 c_3 c_4) c_1) (f2 c_3 (f2 c_4 c_1))) (= (f2 (f2 c_3 c_4) c_2) (f2 c_3 (f2 c_4 c_2))) (= (f2 (f2 c_3 c_4) c_3) (f2 c_3 (f2 c_4 c_3))) (= (f2 (f2 c_3 c_4) c_4) (f2 c_3 (f2 c_4 c_4))) (= (f2 (f2 c_3 c_4) c_5) (f2 c_3 (f2 c_4 c_5))) (= (f2 (f2 c_3 c_4) c_6) (f2 c_3 (f2 c_4 c_6))) (= (f2 (f2 c_3 c_4) c_7) (f2 c_3 (f2 c_4 c_7))) (= (f2 (f2 c_3 c_5) c_0) (f2 c_3 (f2 c_5 c_0))) (= (f2 (f2 c_3 c_5) c_1) (f2 c_3 (f2 c_5 c_1))) (= (f2 (f2 c_3 c_5) c_2) (f2 c_3 (f2 c_5 c_2))) (= (f2 (f2 c_3 c_5) c_3) (f2 c_3 (f2 c_5 c_3))) (= (f2 (f2 c_3 c_5) c_4) (f2 c_3 (f2 c_5 c_4))) (= (f2 (f2 c_3 c_5) c_5) (f2 c_3 (f2 c_5 c_5))) (= (f2 (f2 c_3 c_5) c_6) (f2 c_3 (f2 c_5 c_6))) (= (f2 (f2 c_3 c_5) c_7) (f2 c_3 (f2 c_5 c_7))) (= (f2 (f2 c_3 c_6) c_0) (f2 c_3 (f2 c_6 c_0))) (= (f2 (f2 c_3 c_6) c_1) (f2 c_3 (f2 c_6 c_1))) (= (f2 (f2 c_3 c_6) c_2) (f2 c_3 (f2 c_6 c_2))) (= (f2 (f2 c_3 c_6) c_3) (f2 c_3 (f2 c_6 c_3))) (= (f2 (f2 c_3 c_6) c_4) (f2 c_3 (f2 c_6 c_4))) (= (f2 (f2 c_3 c_6) c_5) (f2 c_3 (f2 c_6 c_5))) (= (f2 (f2 c_3 c_6) c_6) (f2 c_3 (f2 c_6 c_6))) (= (f2 (f2 c_3 c_6) c_7) (f2 c_3 (f2 c_6 c_7))) (= (f2 (f2 c_3 c_7) c_0) (f2 c_3 (f2 c_7 c_0))) (= (f2 (f2 c_3 c_7) c_1) (f2 c_3 (f2 c_7 c_1))) (= (f2 (f2 c_3 c_7) c_2) (f2 c_3 (f2 c_7 c_2))) (= (f2 (f2 c_3 c_7) c_3) (f2 c_3 (f2 c_7 c_3))) (= (f2 (f2 c_3 c_7) c_4) (f2 c_3 (f2 c_7 c_4))) (= (f2 (f2 c_3 c_7) c_5) (f2 c_3 (f2 c_7 c_5))) (= (f2 (f2 c_3 c_7) c_6) (f2 c_3 (f2 c_7 c_6))) (= (f2 (f2 c_3 c_7) c_7) (f2 c_3 (f2 c_7 c_7))) (= (f2 (f2 c_4 c_0) c_0) (f2 c_4 (f2 c_0 c_0))) (= (f2 (f2 c_4 c_0) c_1) (f2 c_4 (f2 c_0 c_1))) (= (f2 (f2 c_4 c_0) c_2) (f2 c_4 (f2 c_0 c_2))) (= (f2 (f2 c_4 c_0) c_3) (f2 c_4 (f2 c_0 c_3))) (= (f2 (f2 c_4 c_0) c_4) (f2 c_4 (f2 c_0 c_4))) (= (f2 (f2 c_4 c_0) c_5) (f2 c_4 (f2 c_0 c_5))) (= (f2 (f2 c_4 c_0) c_6) (f2 c_4 (f2 c_0 c_6))) (= (f2 (f2 c_4 c_0) c_7) (f2 c_4 (f2 c_0 c_7))) (= (f2 (f2 c_4 c_1) c_0) (f2 c_4 (f2 c_1 c_0))) (= (f2 (f2 c_4 c_1) c_1) (f2 c_4 (f2 c_1 c_1))) (= (f2 (f2 c_4 c_1) c_2) (f2 c_4 (f2 c_1 c_2))) (= (f2 (f2 c_4 c_1) c_3) (f2 c_4 (f2 c_1 c_3))) (= (f2 (f2 c_4 c_1) c_4) (f2 c_4 (f2 c_1 c_4))) (= (f2 (f2 c_4 c_1) c_5) (f2 c_4 (f2 c_1 c_5))) (= (f2 (f2 c_4 c_1) c_6) (f2 c_4 (f2 c_1 c_6))) (= (f2 (f2 c_4 c_1) c_7) (f2 c_4 (f2 c_1 c_7))) (= (f2 (f2 c_4 c_2) c_0) (f2 c_4 (f2 c_2 c_0))) (= (f2 (f2 c_4 c_2) c_1) (f2 c_4 (f2 c_2 c_1))) (= (f2 (f2 c_4 c_2) c_2) (f2 c_4 (f2 c_2 c_2))) (= (f2 (f2 c_4 c_2) c_3) (f2 c_4 (f2 c_2 c_3))) (= (f2 (f2 c_4 c_2) c_4) (f2 c_4 (f2 c_2 c_4))) (= (f2 (f2 c_4 c_2) c_5) (f2 c_4 (f2 c_2 c_5))) (= (f2 (f2 c_4 c_2) c_6) (f2 c_4 (f2 c_2 c_6))) (= (f2 (f2 c_4 c_2) c_7) (f2 c_4 (f2 c_2 c_7))) (= (f2 (f2 c_4 c_3) c_0) (f2 c_4 (f2 c_3 c_0))) (= (f2 (f2 c_4 c_3) c_1) (f2 c_4 (f2 c_3 c_1))) (= (f2 (f2 c_4 c_3) c_2) (f2 c_4 (f2 c_3 c_2))) (= (f2 (f2 c_4 c_3) c_3) (f2 c_4 (f2 c_3 c_3))) (= (f2 (f2 c_4 c_3) c_4) (f2 c_4 (f2 c_3 c_4))) (= (f2 (f2 c_4 c_3) c_5) (f2 c_4 (f2 c_3 c_5))) (= (f2 (f2 c_4 c_3) c_6) (f2 c_4 (f2 c_3 c_6))) (= (f2 (f2 c_4 c_3) c_7) (f2 c_4 (f2 c_3 c_7))) (= (f2 (f2 c_4 c_4) c_0) (f2 c_4 (f2 c_4 c_0))) (= (f2 (f2 c_4 c_4) c_1) (f2 c_4 (f2 c_4 c_1))) (= (f2 (f2 c_4 c_4) c_2) (f2 c_4 (f2 c_4 c_2))) (= (f2 (f2 c_4 c_4) c_3) (f2 c_4 (f2 c_4 c_3))) (= (f2 (f2 c_4 c_4) c_4) (f2 c_4 (f2 c_4 c_4))) (= (f2 (f2 c_4 c_4) c_5) (f2 c_4 (f2 c_4 c_5))) (= (f2 (f2 c_4 c_4) c_6) (f2 c_4 (f2 c_4 c_6))) (= (f2 (f2 c_4 c_4) c_7) (f2 c_4 (f2 c_4 c_7))) (= (f2 (f2 c_4 c_5) c_0) (f2 c_4 (f2 c_5 c_0))) (= (f2 (f2 c_4 c_5) c_1) (f2 c_4 (f2 c_5 c_1))) (= (f2 (f2 c_4 c_5) c_2) (f2 c_4 (f2 c_5 c_2))) (= (f2 (f2 c_4 c_5) c_3) (f2 c_4 (f2 c_5 c_3))) (= (f2 (f2 c_4 c_5) c_4) (f2 c_4 (f2 c_5 c_4))) (= (f2 (f2 c_4 c_5) c_5) (f2 c_4 (f2 c_5 c_5))) (= (f2 (f2 c_4 c_5) c_6) (f2 c_4 (f2 c_5 c_6))) (= (f2 (f2 c_4 c_5) c_7) (f2 c_4 (f2 c_5 c_7))) (= (f2 (f2 c_4 c_6) c_0) (f2 c_4 (f2 c_6 c_0))) (= (f2 (f2 c_4 c_6) c_1) (f2 c_4 (f2 c_6 c_1))) (= (f2 (f2 c_4 c_6) c_2) (f2 c_4 (f2 c_6 c_2))) (= (f2 (f2 c_4 c_6) c_3) (f2 c_4 (f2 c_6 c_3))) (= (f2 (f2 c_4 c_6) c_4) (f2 c_4 (f2 c_6 c_4))) (= (f2 (f2 c_4 c_6) c_5) (f2 c_4 (f2 c_6 c_5))) (= (f2 (f2 c_4 c_6) c_6) (f2 c_4 (f2 c_6 c_6))) (= (f2 (f2 c_4 c_6) c_7) (f2 c_4 (f2 c_6 c_7))) (= (f2 (f2 c_4 c_7) c_0) (f2 c_4 (f2 c_7 c_0))) (= (f2 (f2 c_4 c_7) c_1) (f2 c_4 (f2 c_7 c_1))) (= (f2 (f2 c_4 c_7) c_2) (f2 c_4 (f2 c_7 c_2))) (= (f2 (f2 c_4 c_7) c_3) (f2 c_4 (f2 c_7 c_3))) (= (f2 (f2 c_4 c_7) c_4) (f2 c_4 (f2 c_7 c_4))) (= (f2 (f2 c_4 c_7) c_5) (f2 c_4 (f2 c_7 c_5))) (= (f2 (f2 c_4 c_7) c_6) (f2 c_4 (f2 c_7 c_6))) (= (f2 (f2 c_4 c_7) c_7) (f2 c_4 (f2 c_7 c_7))) (= (f2 (f2 c_5 c_0) c_0) (f2 c_5 (f2 c_0 c_0))) (= (f2 (f2 c_5 c_0) c_1) (f2 c_5 (f2 c_0 c_1))) (= (f2 (f2 c_5 c_0) c_2) (f2 c_5 (f2 c_0 c_2))) (= (f2 (f2 c_5 c_0) c_3) (f2 c_5 (f2 c_0 c_3))) (= (f2 (f2 c_5 c_0) c_4) (f2 c_5 (f2 c_0 c_4))) (= (f2 (f2 c_5 c_0) c_5) (f2 c_5 (f2 c_0 c_5))) (= (f2 (f2 c_5 c_0) c_6) (f2 c_5 (f2 c_0 c_6))) (= (f2 (f2 c_5 c_0) c_7) (f2 c_5 (f2 c_0 c_7))) (= (f2 (f2 c_5 c_1) c_0) (f2 c_5 (f2 c_1 c_0))) (= (f2 (f2 c_5 c_1) c_1) (f2 c_5 (f2 c_1 c_1))) (= (f2 (f2 c_5 c_1) c_2) (f2 c_5 (f2 c_1 c_2))) (= (f2 (f2 c_5 c_1) c_3) (f2 c_5 (f2 c_1 c_3))) (= (f2 (f2 c_5 c_1) c_4) (f2 c_5 (f2 c_1 c_4))) (= (f2 (f2 c_5 c_1) c_5) (f2 c_5 (f2 c_1 c_5))) (= (f2 (f2 c_5 c_1) c_6) (f2 c_5 (f2 c_1 c_6))) (= (f2 (f2 c_5 c_1) c_7) (f2 c_5 (f2 c_1 c_7))) (= (f2 (f2 c_5 c_2) c_0) (f2 c_5 (f2 c_2 c_0))) (= (f2 (f2 c_5 c_2) c_1) (f2 c_5 (f2 c_2 c_1))) (= (f2 (f2 c_5 c_2) c_2) (f2 c_5 (f2 c_2 c_2))) (= (f2 (f2 c_5 c_2) c_3) (f2 c_5 (f2 c_2 c_3))) (= (f2 (f2 c_5 c_2) c_4) (f2 c_5 (f2 c_2 c_4))) (= (f2 (f2 c_5 c_2) c_5) (f2 c_5 (f2 c_2 c_5))) (= (f2 (f2 c_5 c_2) c_6) (f2 c_5 (f2 c_2 c_6))) (= (f2 (f2 c_5 c_2) c_7) (f2 c_5 (f2 c_2 c_7))) (= (f2 (f2 c_5 c_3) c_0) (f2 c_5 (f2 c_3 c_0))) (= (f2 (f2 c_5 c_3) c_1) (f2 c_5 (f2 c_3 c_1))) (= (f2 (f2 c_5 c_3) c_2) (f2 c_5 (f2 c_3 c_2))) (= (f2 (f2 c_5 c_3) c_3) (f2 c_5 (f2 c_3 c_3))) (= (f2 (f2 c_5 c_3) c_4) (f2 c_5 (f2 c_3 c_4))) (= (f2 (f2 c_5 c_3) c_5) (f2 c_5 (f2 c_3 c_5))) (= (f2 (f2 c_5 c_3) c_6) (f2 c_5 (f2 c_3 c_6))) (= (f2 (f2 c_5 c_3) c_7) (f2 c_5 (f2 c_3 c_7))) (= (f2 (f2 c_5 c_4) c_0) (f2 c_5 (f2 c_4 c_0))) (= (f2 (f2 c_5 c_4) c_1) (f2 c_5 (f2 c_4 c_1))) (= (f2 (f2 c_5 c_4) c_2) (f2 c_5 (f2 c_4 c_2))) (= (f2 (f2 c_5 c_4) c_3) (f2 c_5 (f2 c_4 c_3))) (= (f2 (f2 c_5 c_4) c_4) (f2 c_5 (f2 c_4 c_4))) (= (f2 (f2 c_5 c_4) c_5) (f2 c_5 (f2 c_4 c_5))) (= (f2 (f2 c_5 c_4) c_6) (f2 c_5 (f2 c_4 c_6))) (= (f2 (f2 c_5 c_4) c_7) (f2 c_5 (f2 c_4 c_7))) (= (f2 (f2 c_5 c_5) c_0) (f2 c_5 (f2 c_5 c_0))) (= (f2 (f2 c_5 c_5) c_1) (f2 c_5 (f2 c_5 c_1))) (= (f2 (f2 c_5 c_5) c_2) (f2 c_5 (f2 c_5 c_2))) (= (f2 (f2 c_5 c_5) c_3) (f2 c_5 (f2 c_5 c_3))) (= (f2 (f2 c_5 c_5) c_4) (f2 c_5 (f2 c_5 c_4))) (= (f2 (f2 c_5 c_5) c_5) (f2 c_5 (f2 c_5 c_5))) (= (f2 (f2 c_5 c_5) c_6) (f2 c_5 (f2 c_5 c_6))) (= (f2 (f2 c_5 c_5) c_7) (f2 c_5 (f2 c_5 c_7))) (= (f2 (f2 c_5 c_6) c_0) (f2 c_5 (f2 c_6 c_0))) (= (f2 (f2 c_5 c_6) c_1) (f2 c_5 (f2 c_6 c_1))) (= (f2 (f2 c_5 c_6) c_2) (f2 c_5 (f2 c_6 c_2))) (= (f2 (f2 c_5 c_6) c_3) (f2 c_5 (f2 c_6 c_3))) (= (f2 (f2 c_5 c_6) c_4) (f2 c_5 (f2 c_6 c_4))) (= (f2 (f2 c_5 c_6) c_5) (f2 c_5 (f2 c_6 c_5))) (= (f2 (f2 c_5 c_6) c_6) (f2 c_5 (f2 c_6 c_6))) (= (f2 (f2 c_5 c_6) c_7) (f2 c_5 (f2 c_6 c_7))) (= (f2 (f2 c_5 c_7) c_0) (f2 c_5 (f2 c_7 c_0))) (= (f2 (f2 c_5 c_7) c_1) (f2 c_5 (f2 c_7 c_1))) (= (f2 (f2 c_5 c_7) c_2) (f2 c_5 (f2 c_7 c_2))) (= (f2 (f2 c_5 c_7) c_3) (f2 c_5 (f2 c_7 c_3))) (= (f2 (f2 c_5 c_7) c_4) (f2 c_5 (f2 c_7 c_4))) (= (f2 (f2 c_5 c_7) c_5) (f2 c_5 (f2 c_7 c_5))) (= (f2 (f2 c_5 c_7) c_6) (f2 c_5 (f2 c_7 c_6))) (= (f2 (f2 c_5 c_7) c_7) (f2 c_5 (f2 c_7 c_7))) (= (f2 (f2 c_6 c_0) c_0) (f2 c_6 (f2 c_0 c_0))) (= (f2 (f2 c_6 c_0) c_1) (f2 c_6 (f2 c_0 c_1))) (= (f2 (f2 c_6 c_0) c_2) (f2 c_6 (f2 c_0 c_2))) (= (f2 (f2 c_6 c_0) c_3) (f2 c_6 (f2 c_0 c_3))) (= (f2 (f2 c_6 c_0) c_4) (f2 c_6 (f2 c_0 c_4))) (= (f2 (f2 c_6 c_0) c_5) (f2 c_6 (f2 c_0 c_5))) (= (f2 (f2 c_6 c_0) c_6) (f2 c_6 (f2 c_0 c_6))) (= (f2 (f2 c_6 c_0) c_7) (f2 c_6 (f2 c_0 c_7))) (= (f2 (f2 c_6 c_1) c_0) (f2 c_6 (f2 c_1 c_0))) (= (f2 (f2 c_6 c_1) c_1) (f2 c_6 (f2 c_1 c_1))) (= (f2 (f2 c_6 c_1) c_2) (f2 c_6 (f2 c_1 c_2))) (= (f2 (f2 c_6 c_1) c_3) (f2 c_6 (f2 c_1 c_3))) (= (f2 (f2 c_6 c_1) c_4) (f2 c_6 (f2 c_1 c_4))) (= (f2 (f2 c_6 c_1) c_5) (f2 c_6 (f2 c_1 c_5))) (= (f2 (f2 c_6 c_1) c_6) (f2 c_6 (f2 c_1 c_6))) (= (f2 (f2 c_6 c_1) c_7) (f2 c_6 (f2 c_1 c_7))) (= (f2 (f2 c_6 c_2) c_0) (f2 c_6 (f2 c_2 c_0))) (= (f2 (f2 c_6 c_2) c_1) (f2 c_6 (f2 c_2 c_1))) (= (f2 (f2 c_6 c_2) c_2) (f2 c_6 (f2 c_2 c_2))) (= (f2 (f2 c_6 c_2) c_3) (f2 c_6 (f2 c_2 c_3))) (= (f2 (f2 c_6 c_2) c_4) (f2 c_6 (f2 c_2 c_4))) (= (f2 (f2 c_6 c_2) c_5) (f2 c_6 (f2 c_2 c_5))) (= (f2 (f2 c_6 c_2) c_6) (f2 c_6 (f2 c_2 c_6))) (= (f2 (f2 c_6 c_2) c_7) (f2 c_6 (f2 c_2 c_7))) (= (f2 (f2 c_6 c_3) c_0) (f2 c_6 (f2 c_3 c_0))) (= (f2 (f2 c_6 c_3) c_1) (f2 c_6 (f2 c_3 c_1))) (= (f2 (f2 c_6 c_3) c_2) (f2 c_6 (f2 c_3 c_2))) (= (f2 (f2 c_6 c_3) c_3) (f2 c_6 (f2 c_3 c_3))) (= (f2 (f2 c_6 c_3) c_4) (f2 c_6 (f2 c_3 c_4))) (= (f2 (f2 c_6 c_3) c_5) (f2 c_6 (f2 c_3 c_5))) (= (f2 (f2 c_6 c_3) c_6) (f2 c_6 (f2 c_3 c_6))) (= (f2 (f2 c_6 c_3) c_7) (f2 c_6 (f2 c_3 c_7))) (= (f2 (f2 c_6 c_4) c_0) (f2 c_6 (f2 c_4 c_0))) (= (f2 (f2 c_6 c_4) c_1) (f2 c_6 (f2 c_4 c_1))) (= (f2 (f2 c_6 c_4) c_2) (f2 c_6 (f2 c_4 c_2))) (= (f2 (f2 c_6 c_4) c_3) (f2 c_6 (f2 c_4 c_3))) (= (f2 (f2 c_6 c_4) c_4) (f2 c_6 (f2 c_4 c_4))) (= (f2 (f2 c_6 c_4) c_5) (f2 c_6 (f2 c_4 c_5))) (= (f2 (f2 c_6 c_4) c_6) (f2 c_6 (f2 c_4 c_6))) (= (f2 (f2 c_6 c_4) c_7) (f2 c_6 (f2 c_4 c_7))) (= (f2 (f2 c_6 c_5) c_0) (f2 c_6 (f2 c_5 c_0))) (= (f2 (f2 c_6 c_5) c_1) (f2 c_6 (f2 c_5 c_1))) (= (f2 (f2 c_6 c_5) c_2) (f2 c_6 (f2 c_5 c_2))) (= (f2 (f2 c_6 c_5) c_3) (f2 c_6 (f2 c_5 c_3))) (= (f2 (f2 c_6 c_5) c_4) (f2 c_6 (f2 c_5 c_4))) (= (f2 (f2 c_6 c_5) c_5) (f2 c_6 (f2 c_5 c_5))) (= (f2 (f2 c_6 c_5) c_6) (f2 c_6 (f2 c_5 c_6))) (= (f2 (f2 c_6 c_5) c_7) (f2 c_6 (f2 c_5 c_7))) (= (f2 (f2 c_6 c_6) c_0) (f2 c_6 (f2 c_6 c_0))) (= (f2 (f2 c_6 c_6) c_1) (f2 c_6 (f2 c_6 c_1))) (= (f2 (f2 c_6 c_6) c_2) (f2 c_6 (f2 c_6 c_2))) (= (f2 (f2 c_6 c_6) c_3) (f2 c_6 (f2 c_6 c_3))) (= (f2 (f2 c_6 c_6) c_4) (f2 c_6 (f2 c_6 c_4))) (= (f2 (f2 c_6 c_6) c_5) (f2 c_6 (f2 c_6 c_5))) (= (f2 (f2 c_6 c_6) c_6) (f2 c_6 (f2 c_6 c_6))) (= (f2 (f2 c_6 c_6) c_7) (f2 c_6 (f2 c_6 c_7))) (= (f2 (f2 c_6 c_7) c_0) (f2 c_6 (f2 c_7 c_0))) (= (f2 (f2 c_6 c_7) c_1) (f2 c_6 (f2 c_7 c_1))) (= (f2 (f2 c_6 c_7) c_2) (f2 c_6 (f2 c_7 c_2))) (= (f2 (f2 c_6 c_7) c_3) (f2 c_6 (f2 c_7 c_3))) (= (f2 (f2 c_6 c_7) c_4) (f2 c_6 (f2 c_7 c_4))) (= (f2 (f2 c_6 c_7) c_5) (f2 c_6 (f2 c_7 c_5))) (= (f2 (f2 c_6 c_7) c_6) (f2 c_6 (f2 c_7 c_6))) (= (f2 (f2 c_6 c_7) c_7) (f2 c_6 (f2 c_7 c_7))) (= (f2 (f2 c_7 c_0) c_0) (f2 c_7 (f2 c_0 c_0))) (= (f2 (f2 c_7 c_0) c_1) (f2 c_7 (f2 c_0 c_1))) (= (f2 (f2 c_7 c_0) c_2) (f2 c_7 (f2 c_0 c_2))) (= (f2 (f2 c_7 c_0) c_3) (f2 c_7 (f2 c_0 c_3))) (= (f2 (f2 c_7 c_0) c_4) (f2 c_7 (f2 c_0 c_4))) (= (f2 (f2 c_7 c_0) c_5) (f2 c_7 (f2 c_0 c_5))) (= (f2 (f2 c_7 c_0) c_6) (f2 c_7 (f2 c_0 c_6))) (= (f2 (f2 c_7 c_0) c_7) (f2 c_7 (f2 c_0 c_7))) (= (f2 (f2 c_7 c_1) c_0) (f2 c_7 (f2 c_1 c_0))) (= (f2 (f2 c_7 c_1) c_1) (f2 c_7 (f2 c_1 c_1))) (= (f2 (f2 c_7 c_1) c_2) (f2 c_7 (f2 c_1 c_2))) (= (f2 (f2 c_7 c_1) c_3) (f2 c_7 (f2 c_1 c_3))) (= (f2 (f2 c_7 c_1) c_4) (f2 c_7 (f2 c_1 c_4))) (= (f2 (f2 c_7 c_1) c_5) (f2 c_7 (f2 c_1 c_5))) (= (f2 (f2 c_7 c_1) c_6) (f2 c_7 (f2 c_1 c_6))) (= (f2 (f2 c_7 c_1) c_7) (f2 c_7 (f2 c_1 c_7))) (= (f2 (f2 c_7 c_2) c_0) (f2 c_7 (f2 c_2 c_0))) (= (f2 (f2 c_7 c_2) c_1) (f2 c_7 (f2 c_2 c_1))) (= (f2 (f2 c_7 c_2) c_2) (f2 c_7 (f2 c_2 c_2))) (= (f2 (f2 c_7 c_2) c_3) (f2 c_7 (f2 c_2 c_3))) (= (f2 (f2 c_7 c_2) c_4) (f2 c_7 (f2 c_2 c_4))) (= (f2 (f2 c_7 c_2) c_5) (f2 c_7 (f2 c_2 c_5))) (= (f2 (f2 c_7 c_2) c_6) (f2 c_7 (f2 c_2 c_6))) (= (f2 (f2 c_7 c_2) c_7) (f2 c_7 (f2 c_2 c_7))) (= (f2 (f2 c_7 c_3) c_0) (f2 c_7 (f2 c_3 c_0))) (= (f2 (f2 c_7 c_3) c_1) (f2 c_7 (f2 c_3 c_1))) (= (f2 (f2 c_7 c_3) c_2) (f2 c_7 (f2 c_3 c_2))) (= (f2 (f2 c_7 c_3) c_3) (f2 c_7 (f2 c_3 c_3))) (= (f2 (f2 c_7 c_3) c_4) (f2 c_7 (f2 c_3 c_4))) (= (f2 (f2 c_7 c_3) c_5) (f2 c_7 (f2 c_3 c_5))) (= (f2 (f2 c_7 c_3) c_6) (f2 c_7 (f2 c_3 c_6))) (= (f2 (f2 c_7 c_3) c_7) (f2 c_7 (f2 c_3 c_7))) (= (f2 (f2 c_7 c_4) c_0) (f2 c_7 (f2 c_4 c_0))) (= (f2 (f2 c_7 c_4) c_1) (f2 c_7 (f2 c_4 c_1))) (= (f2 (f2 c_7 c_4) c_2) (f2 c_7 (f2 c_4 c_2))) (= (f2 (f2 c_7 c_4) c_3) (f2 c_7 (f2 c_4 c_3))) (= (f2 (f2 c_7 c_4) c_4) (f2 c_7 (f2 c_4 c_4))) (= (f2 (f2 c_7 c_4) c_5) (f2 c_7 (f2 c_4 c_5))) (= (f2 (f2 c_7 c_4) c_6) (f2 c_7 (f2 c_4 c_6))) (= (f2 (f2 c_7 c_4) c_7) (f2 c_7 (f2 c_4 c_7))) (= (f2 (f2 c_7 c_5) c_0) (f2 c_7 (f2 c_5 c_0))) (= (f2 (f2 c_7 c_5) c_1) (f2 c_7 (f2 c_5 c_1))) (= (f2 (f2 c_7 c_5) c_2) (f2 c_7 (f2 c_5 c_2))) (= (f2 (f2 c_7 c_5) c_3) (f2 c_7 (f2 c_5 c_3))) (= (f2 (f2 c_7 c_5) c_4) (f2 c_7 (f2 c_5 c_4))) (= (f2 (f2 c_7 c_5) c_5) (f2 c_7 (f2 c_5 c_5))) (= (f2 (f2 c_7 c_5) c_6) (f2 c_7 (f2 c_5 c_6))) (= (f2 (f2 c_7 c_5) c_7) (f2 c_7 (f2 c_5 c_7))) (= (f2 (f2 c_7 c_6) c_0) (f2 c_7 (f2 c_6 c_0))) (= (f2 (f2 c_7 c_6) c_1) (f2 c_7 (f2 c_6 c_1))) (= (f2 (f2 c_7 c_6) c_2) (f2 c_7 (f2 c_6 c_2))) (= (f2 (f2 c_7 c_6) c_3) (f2 c_7 (f2 c_6 c_3))) (= (f2 (f2 c_7 c_6) c_4) (f2 c_7 (f2 c_6 c_4))) (= (f2 (f2 c_7 c_6) c_5) (f2 c_7 (f2 c_6 c_5))) (= (f2 (f2 c_7 c_6) c_6) (f2 c_7 (f2 c_6 c_6))) (= (f2 (f2 c_7 c_6) c_7) (f2 c_7 (f2 c_6 c_7))) (= (f2 (f2 c_7 c_7) c_0) (f2 c_7 (f2 c_7 c_0))) (= (f2 (f2 c_7 c_7) c_1) (f2 c_7 (f2 c_7 c_1))) (= (f2 (f2 c_7 c_7) c_2) (f2 c_7 (f2 c_7 c_2))) (= (f2 (f2 c_7 c_7) c_3) (f2 c_7 (f2 c_7 c_3))) (= (f2 (f2 c_7 c_7) c_4) (f2 c_7 (f2 c_7 c_4))) (= (f2 (f2 c_7 c_7) c_5) (f2 c_7 (f2 c_7 c_5))) (= (f2 (f2 c_7 c_7) c_6) (f2 c_7 (f2 c_7 c_6))) (= (f2 (f2 c_7 c_7) c_7) (f2 c_7 (f2 c_7 c_7))) (= (f1 c_0 c_0) (f1 c_0 c_0)) (= (f1 c_0 c_1) (f1 c_1 c_0)) (= (f1 c_0 c_2) (f1 c_2 c_0)) (= (f1 c_0 c_3) (f1 c_3 c_0)) (= (f1 c_0 c_4) (f1 c_4 c_0)) (= (f1 c_0 c_5) (f1 c_5 c_0)) (= (f1 c_0 c_6) (f1 c_6 c_0)) (= (f1 c_0 c_7) (f1 c_7 c_0)) (= (f1 c_1 c_0) (f1 c_0 c_1)) (= (f1 c_1 c_1) (f1 c_1 c_1)) (= (f1 c_1 c_2) (f1 c_2 c_1)) (= (f1 c_1 c_3) (f1 c_3 c_1)) (= (f1 c_1 c_4) (f1 c_4 c_1)) (= (f1 c_1 c_5) (f1 c_5 c_1)) (= (f1 c_1 c_6) (f1 c_6 c_1)) (= (f1 c_1 c_7) (f1 c_7 c_1)) (= (f1 c_2 c_0) (f1 c_0 c_2)) (= (f1 c_2 c_1) (f1 c_1 c_2)) (= (f1 c_2 c_2) (f1 c_2 c_2)) (= (f1 c_2 c_3) (f1 c_3 c_2)) (= (f1 c_2 c_4) (f1 c_4 c_2)) (= (f1 c_2 c_5) (f1 c_5 c_2)) (= (f1 c_2 c_6) (f1 c_6 c_2)) (= (f1 c_2 c_7) (f1 c_7 c_2)) (= (f1 c_3 c_0) (f1 c_0 c_3)) (= (f1 c_3 c_1) (f1 c_1 c_3)) (= (f1 c_3 c_2) (f1 c_2 c_3)) (= (f1 c_3 c_3) (f1 c_3 c_3)) (= (f1 c_3 c_4) (f1 c_4 c_3)) (= (f1 c_3 c_5) (f1 c_5 c_3)) (= (f1 c_3 c_6) (f1 c_6 c_3)) (= (f1 c_3 c_7) (f1 c_7 c_3)) (= (f1 c_4 c_0) (f1 c_0 c_4)) (= (f1 c_4 c_1) (f1 c_1 c_4)) (= (f1 c_4 c_2) (f1 c_2 c_4)) (= (f1 c_4 c_3) (f1 c_3 c_4)) (= (f1 c_4 c_4) (f1 c_4 c_4)) (= (f1 c_4 c_5) (f1 c_5 c_4)) (= (f1 c_4 c_6) (f1 c_6 c_4)) (= (f1 c_4 c_7) (f1 c_7 c_4)) (= (f1 c_5 c_0) (f1 c_0 c_5)) (= (f1 c_5 c_1) (f1 c_1 c_5)) (= (f1 c_5 c_2) (f1 c_2 c_5)) (= (f1 c_5 c_3) (f1 c_3 c_5)) (= (f1 c_5 c_4) (f1 c_4 c_5)) (= (f1 c_5 c_5) (f1 c_5 c_5)) (= (f1 c_5 c_6) (f1 c_6 c_5)) (= (f1 c_5 c_7) (f1 c_7 c_5)) (= (f1 c_6 c_0) (f1 c_0 c_6)) (= (f1 c_6 c_1) (f1 c_1 c_6)) (= (f1 c_6 c_2) (f1 c_2 c_6)) (= (f1 c_6 c_3) (f1 c_3 c_6)) (= (f1 c_6 c_4) (f1 c_4 c_6)) (= (f1 c_6 c_5) (f1 c_5 c_6)) (= (f1 c_6 c_6) (f1 c_6 c_6)) (= (f1 c_6 c_7) (f1 c_7 c_6)) (= (f1 c_7 c_0) (f1 c_0 c_7)) (= (f1 c_7 c_1) (f1 c_1 c_7)) (= (f1 c_7 c_2) (f1 c_2 c_7)) (= (f1 c_7 c_3) (f1 c_3 c_7)) (= (f1 c_7 c_4) (f1 c_4 c_7)) (= (f1 c_7 c_5) (f1 c_5 c_7)) (= (f1 c_7 c_6) (f1 c_6 c_7)) (= (f1 c_7 c_7) (f1 c_7 c_7)) (= (f2 c_0 c_0) (f2 c_0 c_0)) (= (f2 c_0 c_1) (f2 c_1 c_0)) (= (f2 c_0 c_2) (f2 c_2 c_0)) (= (f2 c_0 c_3) (f2 c_3 c_0)) (= (f2 c_0 c_4) (f2 c_4 c_0)) (= (f2 c_0 c_5) (f2 c_5 c_0)) (= (f2 c_0 c_6) (f2 c_6 c_0)) (= (f2 c_0 c_7) (f2 c_7 c_0)) (= (f2 c_1 c_0) (f2 c_0 c_1)) (= (f2 c_1 c_1) (f2 c_1 c_1)) (= (f2 c_1 c_2) (f2 c_2 c_1)) (= (f2 c_1 c_3) (f2 c_3 c_1)) (= (f2 c_1 c_4) (f2 c_4 c_1)) (= (f2 c_1 c_5) (f2 c_5 c_1)) (= (f2 c_1 c_6) (f2 c_6 c_1)) (= (f2 c_1 c_7) (f2 c_7 c_1)) (= (f2 c_2 c_0) (f2 c_0 c_2)) (= (f2 c_2 c_1) (f2 c_1 c_2)) (= (f2 c_2 c_2) (f2 c_2 c_2)) (= (f2 c_2 c_3) (f2 c_3 c_2)) (= (f2 c_2 c_4) (f2 c_4 c_2)) (= (f2 c_2 c_5) (f2 c_5 c_2)) (= (f2 c_2 c_6) (f2 c_6 c_2)) (= (f2 c_2 c_7) (f2 c_7 c_2)) (= (f2 c_3 c_0) (f2 c_0 c_3)) (= (f2 c_3 c_1) (f2 c_1 c_3)) (= (f2 c_3 c_2) (f2 c_2 c_3)) (= (f2 c_3 c_3) (f2 c_3 c_3)) (= (f2 c_3 c_4) (f2 c_4 c_3)) (= (f2 c_3 c_5) (f2 c_5 c_3)) (= (f2 c_3 c_6) (f2 c_6 c_3)) (= (f2 c_3 c_7) (f2 c_7 c_3)) (= (f2 c_4 c_0) (f2 c_0 c_4)) (= (f2 c_4 c_1) (f2 c_1 c_4)) (= (f2 c_4 c_2) (f2 c_2 c_4)) (= (f2 c_4 c_3) (f2 c_3 c_4)) (= (f2 c_4 c_4) (f2 c_4 c_4)) (= (f2 c_4 c_5) (f2 c_5 c_4)) (= (f2 c_4 c_6) (f2 c_6 c_4)) (= (f2 c_4 c_7) (f2 c_7 c_4)) (= (f2 c_5 c_0) (f2 c_0 c_5)) (= (f2 c_5 c_1) (f2 c_1 c_5)) (= (f2 c_5 c_2) (f2 c_2 c_5)) (= (f2 c_5 c_3) (f2 c_3 c_5)) (= (f2 c_5 c_4) (f2 c_4 c_5)) (= (f2 c_5 c_5) (f2 c_5 c_5)) (= (f2 c_5 c_6) (f2 c_6 c_5)) (= (f2 c_5 c_7) (f2 c_7 c_5)) (= (f2 c_6 c_0) (f2 c_0 c_6)) (= (f2 c_6 c_1) (f2 c_1 c_6)) (= (f2 c_6 c_2) (f2 c_2 c_6)) (= (f2 c_6 c_3) (f2 c_3 c_6)) (= (f2 c_6 c_4) (f2 c_4 c_6)) (= (f2 c_6 c_5) (f2 c_5 c_6)) (= (f2 c_6 c_6) (f2 c_6 c_6)) (= (f2 c_6 c_7) (f2 c_7 c_6)) (= (f2 c_7 c_0) (f2 c_0 c_7)) (= (f2 c_7 c_1) (f2 c_1 c_7)) (= (f2 c_7 c_2) (f2 c_2 c_7)) (= (f2 c_7 c_3) (f2 c_3 c_7)) (= (f2 c_7 c_4) (f2 c_4 c_7)) (= (f2 c_7 c_5) (f2 c_5 c_7)) (= (f2 c_7 c_6) (f2 c_6 c_7)) (= (f2 c_7 c_7) (f2 c_7 c_7)) (= (f3 (f1 c_0 c_0)) (f2 (f3 c_0) (f3 c_0))) (= (f3 (f1 c_0 c_1)) (f2 (f3 c_0) (f3 c_1))) (= (f3 (f1 c_0 c_2)) (f2 (f3 c_0) (f3 c_2))) (= (f3 (f1 c_0 c_3)) (f2 (f3 c_0) (f3 c_3))) (= (f3 (f1 c_0 c_4)) (f2 (f3 c_0) (f3 c_4))) (= (f3 (f1 c_0 c_5)) (f2 (f3 c_0) (f3 c_5))) (= (f3 (f1 c_0 c_6)) (f2 (f3 c_0) (f3 c_6))) (= (f3 (f1 c_0 c_7)) (f2 (f3 c_0) (f3 c_7))) (= (f3 (f1 c_1 c_0)) (f2 (f3 c_1) (f3 c_0))) (= (f3 (f1 c_1 c_1)) (f2 (f3 c_1) (f3 c_1))) (= (f3 (f1 c_1 c_2)) (f2 (f3 c_1) (f3 c_2))) (= (f3 (f1 c_1 c_3)) (f2 (f3 c_1) (f3 c_3))) (= (f3 (f1 c_1 c_4)) (f2 (f3 c_1) (f3 c_4))) (= (f3 (f1 c_1 c_5)) (f2 (f3 c_1) (f3 c_5))) (= (f3 (f1 c_1 c_6)) (f2 (f3 c_1) (f3 c_6))) (= (f3 (f1 c_1 c_7)) (f2 (f3 c_1) (f3 c_7))) (= (f3 (f1 c_2 c_0)) (f2 (f3 c_2) (f3 c_0))) (= (f3 (f1 c_2 c_1)) (f2 (f3 c_2) (f3 c_1))) (= (f3 (f1 c_2 c_2)) (f2 (f3 c_2) (f3 c_2))) (= (f3 (f1 c_2 c_3)) (f2 (f3 c_2) (f3 c_3))) (= (f3 (f1 c_2 c_4)) (f2 (f3 c_2) (f3 c_4))) (= (f3 (f1 c_2 c_5)) (f2 (f3 c_2) (f3 c_5))) (= (f3 (f1 c_2 c_6)) (f2 (f3 c_2) (f3 c_6))) (= (f3 (f1 c_2 c_7)) (f2 (f3 c_2) (f3 c_7))) (= (f3 (f1 c_3 c_0)) (f2 (f3 c_3) (f3 c_0))) (= (f3 (f1 c_3 c_1)) (f2 (f3 c_3) (f3 c_1))) (= (f3 (f1 c_3 c_2)) (f2 (f3 c_3) (f3 c_2))) (= (f3 (f1 c_3 c_3)) (f2 (f3 c_3) (f3 c_3))) (= (f3 (f1 c_3 c_4)) (f2 (f3 c_3) (f3 c_4))) (= (f3 (f1 c_3 c_5)) (f2 (f3 c_3) (f3 c_5))) (= (f3 (f1 c_3 c_6)) (f2 (f3 c_3) (f3 c_6))) (= (f3 (f1 c_3 c_7)) (f2 (f3 c_3) (f3 c_7))) (= (f3 (f1 c_4 c_0)) (f2 (f3 c_4) (f3 c_0))) (= (f3 (f1 c_4 c_1)) (f2 (f3 c_4) (f3 c_1))) (= (f3 (f1 c_4 c_2)) (f2 (f3 c_4) (f3 c_2))) (= (f3 (f1 c_4 c_3)) (f2 (f3 c_4) (f3 c_3))) (= (f3 (f1 c_4 c_4)) (f2 (f3 c_4) (f3 c_4))) (= (f3 (f1 c_4 c_5)) (f2 (f3 c_4) (f3 c_5))) (= (f3 (f1 c_4 c_6)) (f2 (f3 c_4) (f3 c_6))) (= (f3 (f1 c_4 c_7)) (f2 (f3 c_4) (f3 c_7))) (= (f3 (f1 c_5 c_0)) (f2 (f3 c_5) (f3 c_0))) (= (f3 (f1 c_5 c_1)) (f2 (f3 c_5) (f3 c_1))) (= (f3 (f1 c_5 c_2)) (f2 (f3 c_5) (f3 c_2))) (= (f3 (f1 c_5 c_3)) (f2 (f3 c_5) (f3 c_3))) (= (f3 (f1 c_5 c_4)) (f2 (f3 c_5) (f3 c_4))) (= (f3 (f1 c_5 c_5)) (f2 (f3 c_5) (f3 c_5))) (= (f3 (f1 c_5 c_6)) (f2 (f3 c_5) (f3 c_6))) (= (f3 (f1 c_5 c_7)) (f2 (f3 c_5) (f3 c_7))) (= (f3 (f1 c_6 c_0)) (f2 (f3 c_6) (f3 c_0))) (= (f3 (f1 c_6 c_1)) (f2 (f3 c_6) (f3 c_1))) (= (f3 (f1 c_6 c_2)) (f2 (f3 c_6) (f3 c_2))) (= (f3 (f1 c_6 c_3)) (f2 (f3 c_6) (f3 c_3))) (= (f3 (f1 c_6 c_4)) (f2 (f3 c_6) (f3 c_4))) (= (f3 (f1 c_6 c_5)) (f2 (f3 c_6) (f3 c_5))) (= (f3 (f1 c_6 c_6)) (f2 (f3 c_6) (f3 c_6))) (= (f3 (f1 c_6 c_7)) (f2 (f3 c_6) (f3 c_7))) (= (f3 (f1 c_7 c_0)) (f2 (f3 c_7) (f3 c_0))) (= (f3 (f1 c_7 c_1)) (f2 (f3 c_7) (f3 c_1))) (= (f3 (f1 c_7 c_2)) (f2 (f3 c_7) (f3 c_2))) (= (f3 (f1 c_7 c_3)) (f2 (f3 c_7) (f3 c_3))) (= (f3 (f1 c_7 c_4)) (f2 (f3 c_7) (f3 c_4))) (= (f3 (f1 c_7 c_5)) (f2 (f3 c_7) (f3 c_5))) (= (f3 (f1 c_7 c_6)) (f2 (f3 c_7) (f3 c_6))) (= (f3 (f1 c_7 c_7)) (f2 (f3 c_7) (f3 c_7))) (= (f2 (f3 c_0) c_0) c4) (= (f2 (f3 c_1) c_1) c4) (= (f2 (f3 c_2) c_2) c4) (= (f2 (f3 c_3) c_3) c4) (= (f2 (f3 c_4) c_4) c4) (= (f2 (f3 c_5) c_5) c4) (= (f2 (f3 c_6) c_6) c4) (= (f2 (f3 c_7) c_7) c4) (= (f1 (f1 c_0 c_0) c_0) (f1 c_0 (f1 c_0 c_0))) (= (f1 (f1 c_0 c_0) c_1) (f1 c_0 (f1 c_0 c_1))) (= (f1 (f1 c_0 c_0) c_2) (f1 c_0 (f1 c_0 c_2))) (= (f1 (f1 c_0 c_0) c_3) (f1 c_0 (f1 c_0 c_3))) (= (f1 (f1 c_0 c_0) c_4) (f1 c_0 (f1 c_0 c_4))) (= (f1 (f1 c_0 c_0) c_5) (f1 c_0 (f1 c_0 c_5))) (= (f1 (f1 c_0 c_0) c_6) (f1 c_0 (f1 c_0 c_6))) (= (f1 (f1 c_0 c_0) c_7) (f1 c_0 (f1 c_0 c_7))) (= (f1 (f1 c_0 c_1) c_0) (f1 c_0 (f1 c_1 c_0))) (= (f1 (f1 c_0 c_1) c_1) (f1 c_0 (f1 c_1 c_1))) (= (f1 (f1 c_0 c_1) c_2) (f1 c_0 (f1 c_1 c_2))) (= (f1 (f1 c_0 c_1) c_3) (f1 c_0 (f1 c_1 c_3))) (= (f1 (f1 c_0 c_1) c_4) (f1 c_0 (f1 c_1 c_4))) (= (f1 (f1 c_0 c_1) c_5) (f1 c_0 (f1 c_1 c_5))) (= (f1 (f1 c_0 c_1) c_6) (f1 c_0 (f1 c_1 c_6))) (= (f1 (f1 c_0 c_1) c_7) (f1 c_0 (f1 c_1 c_7))) (= (f1 (f1 c_0 c_2) c_0) (f1 c_0 (f1 c_2 c_0))) (= (f1 (f1 c_0 c_2) c_1) (f1 c_0 (f1 c_2 c_1))) (= (f1 (f1 c_0 c_2) c_2) (f1 c_0 (f1 c_2 c_2))) (= (f1 (f1 c_0 c_2) c_3) (f1 c_0 (f1 c_2 c_3))) (= (f1 (f1 c_0 c_2) c_4) (f1 c_0 (f1 c_2 c_4))) (= (f1 (f1 c_0 c_2) c_5) (f1 c_0 (f1 c_2 c_5))) (= (f1 (f1 c_0 c_2) c_6) (f1 c_0 (f1 c_2 c_6))) (= (f1 (f1 c_0 c_2) c_7) (f1 c_0 (f1 c_2 c_7))) (= (f1 (f1 c_0 c_3) c_0) (f1 c_0 (f1 c_3 c_0))) (= (f1 (f1 c_0 c_3) c_1) (f1 c_0 (f1 c_3 c_1))) (= (f1 (f1 c_0 c_3) c_2) (f1 c_0 (f1 c_3 c_2))) (= (f1 (f1 c_0 c_3) c_3) (f1 c_0 (f1 c_3 c_3))) (= (f1 (f1 c_0 c_3) c_4) (f1 c_0 (f1 c_3 c_4))) (= (f1 (f1 c_0 c_3) c_5) (f1 c_0 (f1 c_3 c_5))) (= (f1 (f1 c_0 c_3) c_6) (f1 c_0 (f1 c_3 c_6))) (= (f1 (f1 c_0 c_3) c_7) (f1 c_0 (f1 c_3 c_7))) (= (f1 (f1 c_0 c_4) c_0) (f1 c_0 (f1 c_4 c_0))) (= (f1 (f1 c_0 c_4) c_1) (f1 c_0 (f1 c_4 c_1))) (= (f1 (f1 c_0 c_4) c_2) (f1 c_0 (f1 c_4 c_2))) (= (f1 (f1 c_0 c_4) c_3) (f1 c_0 (f1 c_4 c_3))) (= (f1 (f1 c_0 c_4) c_4) (f1 c_0 (f1 c_4 c_4))) (= (f1 (f1 c_0 c_4) c_5) (f1 c_0 (f1 c_4 c_5))) (= (f1 (f1 c_0 c_4) c_6) (f1 c_0 (f1 c_4 c_6))) (= (f1 (f1 c_0 c_4) c_7) (f1 c_0 (f1 c_4 c_7))) (= (f1 (f1 c_0 c_5) c_0) (f1 c_0 (f1 c_5 c_0))) (= (f1 (f1 c_0 c_5) c_1) (f1 c_0 (f1 c_5 c_1))) (= (f1 (f1 c_0 c_5) c_2) (f1 c_0 (f1 c_5 c_2))) (= (f1 (f1 c_0 c_5) c_3) (f1 c_0 (f1 c_5 c_3))) (= (f1 (f1 c_0 c_5) c_4) (f1 c_0 (f1 c_5 c_4))) (= (f1 (f1 c_0 c_5) c_5) (f1 c_0 (f1 c_5 c_5))) (= (f1 (f1 c_0 c_5) c_6) (f1 c_0 (f1 c_5 c_6))) (= (f1 (f1 c_0 c_5) c_7) (f1 c_0 (f1 c_5 c_7))) (= (f1 (f1 c_0 c_6) c_0) (f1 c_0 (f1 c_6 c_0))) (= (f1 (f1 c_0 c_6) c_1) (f1 c_0 (f1 c_6 c_1))) (= (f1 (f1 c_0 c_6) c_2) (f1 c_0 (f1 c_6 c_2))) (= (f1 (f1 c_0 c_6) c_3) (f1 c_0 (f1 c_6 c_3))) (= (f1 (f1 c_0 c_6) c_4) (f1 c_0 (f1 c_6 c_4))) (= (f1 (f1 c_0 c_6) c_5) (f1 c_0 (f1 c_6 c_5))) (= (f1 (f1 c_0 c_6) c_6) (f1 c_0 (f1 c_6 c_6))) (= (f1 (f1 c_0 c_6) c_7) (f1 c_0 (f1 c_6 c_7))) (= (f1 (f1 c_0 c_7) c_0) (f1 c_0 (f1 c_7 c_0))) (= (f1 (f1 c_0 c_7) c_1) (f1 c_0 (f1 c_7 c_1))) (= (f1 (f1 c_0 c_7) c_2) (f1 c_0 (f1 c_7 c_2))) (= (f1 (f1 c_0 c_7) c_3) (f1 c_0 (f1 c_7 c_3))) (= (f1 (f1 c_0 c_7) c_4) (f1 c_0 (f1 c_7 c_4))) (= (f1 (f1 c_0 c_7) c_5) (f1 c_0 (f1 c_7 c_5))) (= (f1 (f1 c_0 c_7) c_6) (f1 c_0 (f1 c_7 c_6))) (= (f1 (f1 c_0 c_7) c_7) (f1 c_0 (f1 c_7 c_7))) (= (f1 (f1 c_1 c_0) c_0) (f1 c_1 (f1 c_0 c_0))) (= (f1 (f1 c_1 c_0) c_1) (f1 c_1 (f1 c_0 c_1))) (= (f1 (f1 c_1 c_0) c_2) (f1 c_1 (f1 c_0 c_2))) (= (f1 (f1 c_1 c_0) c_3) (f1 c_1 (f1 c_0 c_3))) (= (f1 (f1 c_1 c_0) c_4) (f1 c_1 (f1 c_0 c_4))) (= (f1 (f1 c_1 c_0) c_5) (f1 c_1 (f1 c_0 c_5))) (= (f1 (f1 c_1 c_0) c_6) (f1 c_1 (f1 c_0 c_6))) (= (f1 (f1 c_1 c_0) c_7) (f1 c_1 (f1 c_0 c_7))) (= (f1 (f1 c_1 c_1) c_0) (f1 c_1 (f1 c_1 c_0))) (= (f1 (f1 c_1 c_1) c_1) (f1 c_1 (f1 c_1 c_1))) (= (f1 (f1 c_1 c_1) c_2) (f1 c_1 (f1 c_1 c_2))) (= (f1 (f1 c_1 c_1) c_3) (f1 c_1 (f1 c_1 c_3))) (= (f1 (f1 c_1 c_1) c_4) (f1 c_1 (f1 c_1 c_4))) (= (f1 (f1 c_1 c_1) c_5) (f1 c_1 (f1 c_1 c_5))) (= (f1 (f1 c_1 c_1) c_6) (f1 c_1 (f1 c_1 c_6))) (= (f1 (f1 c_1 c_1) c_7) (f1 c_1 (f1 c_1 c_7))) (= (f1 (f1 c_1 c_2) c_0) (f1 c_1 (f1 c_2 c_0))) (= (f1 (f1 c_1 c_2) c_1) (f1 c_1 (f1 c_2 c_1))) (= (f1 (f1 c_1 c_2) c_2) (f1 c_1 (f1 c_2 c_2))) (= (f1 (f1 c_1 c_2) c_3) (f1 c_1 (f1 c_2 c_3))) (= (f1 (f1 c_1 c_2) c_4) (f1 c_1 (f1 c_2 c_4))) (= (f1 (f1 c_1 c_2) c_5) (f1 c_1 (f1 c_2 c_5))) (= (f1 (f1 c_1 c_2) c_6) (f1 c_1 (f1 c_2 c_6))) (= (f1 (f1 c_1 c_2) c_7) (f1 c_1 (f1 c_2 c_7))) (= (f1 (f1 c_1 c_3) c_0) (f1 c_1 (f1 c_3 c_0))) (= (f1 (f1 c_1 c_3) c_1) (f1 c_1 (f1 c_3 c_1))) (= (f1 (f1 c_1 c_3) c_2) (f1 c_1 (f1 c_3 c_2))) (= (f1 (f1 c_1 c_3) c_3) (f1 c_1 (f1 c_3 c_3))) (= (f1 (f1 c_1 c_3) c_4) (f1 c_1 (f1 c_3 c_4))) (= (f1 (f1 c_1 c_3) c_5) (f1 c_1 (f1 c_3 c_5))) (= (f1 (f1 c_1 c_3) c_6) (f1 c_1 (f1 c_3 c_6))) (= (f1 (f1 c_1 c_3) c_7) (f1 c_1 (f1 c_3 c_7))) (= (f1 (f1 c_1 c_4) c_0) (f1 c_1 (f1 c_4 c_0))) (= (f1 (f1 c_1 c_4) c_1) (f1 c_1 (f1 c_4 c_1))) (= (f1 (f1 c_1 c_4) c_2) (f1 c_1 (f1 c_4 c_2))) (= (f1 (f1 c_1 c_4) c_3) (f1 c_1 (f1 c_4 c_3))) (= (f1 (f1 c_1 c_4) c_4) (f1 c_1 (f1 c_4 c_4))) (= (f1 (f1 c_1 c_4) c_5) (f1 c_1 (f1 c_4 c_5))) (= (f1 (f1 c_1 c_4) c_6) (f1 c_1 (f1 c_4 c_6))) (= (f1 (f1 c_1 c_4) c_7) (f1 c_1 (f1 c_4 c_7))) (= (f1 (f1 c_1 c_5) c_0) (f1 c_1 (f1 c_5 c_0))) (= (f1 (f1 c_1 c_5) c_1) (f1 c_1 (f1 c_5 c_1))) (= (f1 (f1 c_1 c_5) c_2) (f1 c_1 (f1 c_5 c_2))) (= (f1 (f1 c_1 c_5) c_3) (f1 c_1 (f1 c_5 c_3))) (= (f1 (f1 c_1 c_5) c_4) (f1 c_1 (f1 c_5 c_4))) (= (f1 (f1 c_1 c_5) c_5) (f1 c_1 (f1 c_5 c_5))) (= (f1 (f1 c_1 c_5) c_6) (f1 c_1 (f1 c_5 c_6))) (= (f1 (f1 c_1 c_5) c_7) (f1 c_1 (f1 c_5 c_7))) (= (f1 (f1 c_1 c_6) c_0) (f1 c_1 (f1 c_6 c_0))) (= (f1 (f1 c_1 c_6) c_1) (f1 c_1 (f1 c_6 c_1))) (= (f1 (f1 c_1 c_6) c_2) (f1 c_1 (f1 c_6 c_2))) (= (f1 (f1 c_1 c_6) c_3) (f1 c_1 (f1 c_6 c_3))) (= (f1 (f1 c_1 c_6) c_4) (f1 c_1 (f1 c_6 c_4))) (= (f1 (f1 c_1 c_6) c_5) (f1 c_1 (f1 c_6 c_5))) (= (f1 (f1 c_1 c_6) c_6) (f1 c_1 (f1 c_6 c_6))) (= (f1 (f1 c_1 c_6) c_7) (f1 c_1 (f1 c_6 c_7))) (= (f1 (f1 c_1 c_7) c_0) (f1 c_1 (f1 c_7 c_0))) (= (f1 (f1 c_1 c_7) c_1) (f1 c_1 (f1 c_7 c_1))) (= (f1 (f1 c_1 c_7) c_2) (f1 c_1 (f1 c_7 c_2))) (= (f1 (f1 c_1 c_7) c_3) (f1 c_1 (f1 c_7 c_3))) (= (f1 (f1 c_1 c_7) c_4) (f1 c_1 (f1 c_7 c_4))) (= (f1 (f1 c_1 c_7) c_5) (f1 c_1 (f1 c_7 c_5))) (= (f1 (f1 c_1 c_7) c_6) (f1 c_1 (f1 c_7 c_6))) (= (f1 (f1 c_1 c_7) c_7) (f1 c_1 (f1 c_7 c_7))) (= (f1 (f1 c_2 c_0) c_0) (f1 c_2 (f1 c_0 c_0))) (= (f1 (f1 c_2 c_0) c_1) (f1 c_2 (f1 c_0 c_1))) (= (f1 (f1 c_2 c_0) c_2) (f1 c_2 (f1 c_0 c_2))) (= (f1 (f1 c_2 c_0) c_3) (f1 c_2 (f1 c_0 c_3))) (= (f1 (f1 c_2 c_0) c_4) (f1 c_2 (f1 c_0 c_4))) (= (f1 (f1 c_2 c_0) c_5) (f1 c_2 (f1 c_0 c_5))) (= (f1 (f1 c_2 c_0) c_6) (f1 c_2 (f1 c_0 c_6))) (= (f1 (f1 c_2 c_0) c_7) (f1 c_2 (f1 c_0 c_7))) (= (f1 (f1 c_2 c_1) c_0) (f1 c_2 (f1 c_1 c_0))) (= (f1 (f1 c_2 c_1) c_1) (f1 c_2 (f1 c_1 c_1))) (= (f1 (f1 c_2 c_1) c_2) (f1 c_2 (f1 c_1 c_2))) (= (f1 (f1 c_2 c_1) c_3) (f1 c_2 (f1 c_1 c_3))) (= (f1 (f1 c_2 c_1) c_4) (f1 c_2 (f1 c_1 c_4))) (= (f1 (f1 c_2 c_1) c_5) (f1 c_2 (f1 c_1 c_5))) (= (f1 (f1 c_2 c_1) c_6) (f1 c_2 (f1 c_1 c_6))) (= (f1 (f1 c_2 c_1) c_7) (f1 c_2 (f1 c_1 c_7))) (= (f1 (f1 c_2 c_2) c_0) (f1 c_2 (f1 c_2 c_0))) (= (f1 (f1 c_2 c_2) c_1) (f1 c_2 (f1 c_2 c_1))) (= (f1 (f1 c_2 c_2) c_2) (f1 c_2 (f1 c_2 c_2))) (= (f1 (f1 c_2 c_2) c_3) (f1 c_2 (f1 c_2 c_3))) (= (f1 (f1 c_2 c_2) c_4) (f1 c_2 (f1 c_2 c_4))) (= (f1 (f1 c_2 c_2) c_5) (f1 c_2 (f1 c_2 c_5))) (= (f1 (f1 c_2 c_2) c_6) (f1 c_2 (f1 c_2 c_6))) (= (f1 (f1 c_2 c_2) c_7) (f1 c_2 (f1 c_2 c_7))) (= (f1 (f1 c_2 c_3) c_0) (f1 c_2 (f1 c_3 c_0))) (= (f1 (f1 c_2 c_3) c_1) (f1 c_2 (f1 c_3 c_1))) (= (f1 (f1 c_2 c_3) c_2) (f1 c_2 (f1 c_3 c_2))) (= (f1 (f1 c_2 c_3) c_3) (f1 c_2 (f1 c_3 c_3))) (= (f1 (f1 c_2 c_3) c_4) (f1 c_2 (f1 c_3 c_4))) (= (f1 (f1 c_2 c_3) c_5) (f1 c_2 (f1 c_3 c_5))) (= (f1 (f1 c_2 c_3) c_6) (f1 c_2 (f1 c_3 c_6))) (= (f1 (f1 c_2 c_3) c_7) (f1 c_2 (f1 c_3 c_7))) (= (f1 (f1 c_2 c_4) c_0) (f1 c_2 (f1 c_4 c_0))) (= (f1 (f1 c_2 c_4) c_1) (f1 c_2 (f1 c_4 c_1))) (= (f1 (f1 c_2 c_4) c_2) (f1 c_2 (f1 c_4 c_2))) (= (f1 (f1 c_2 c_4) c_3) (f1 c_2 (f1 c_4 c_3))) (= (f1 (f1 c_2 c_4) c_4) (f1 c_2 (f1 c_4 c_4))) (= (f1 (f1 c_2 c_4) c_5) (f1 c_2 (f1 c_4 c_5))) (= (f1 (f1 c_2 c_4) c_6) (f1 c_2 (f1 c_4 c_6))) (= (f1 (f1 c_2 c_4) c_7) (f1 c_2 (f1 c_4 c_7))) (= (f1 (f1 c_2 c_5) c_0) (f1 c_2 (f1 c_5 c_0))) (= (f1 (f1 c_2 c_5) c_1) (f1 c_2 (f1 c_5 c_1))) (= (f1 (f1 c_2 c_5) c_2) (f1 c_2 (f1 c_5 c_2))) (= (f1 (f1 c_2 c_5) c_3) (f1 c_2 (f1 c_5 c_3))) (= (f1 (f1 c_2 c_5) c_4) (f1 c_2 (f1 c_5 c_4))) (= (f1 (f1 c_2 c_5) c_5) (f1 c_2 (f1 c_5 c_5))) (= (f1 (f1 c_2 c_5) c_6) (f1 c_2 (f1 c_5 c_6))) (= (f1 (f1 c_2 c_5) c_7) (f1 c_2 (f1 c_5 c_7))) (= (f1 (f1 c_2 c_6) c_0) (f1 c_2 (f1 c_6 c_0))) (= (f1 (f1 c_2 c_6) c_1) (f1 c_2 (f1 c_6 c_1))) (= (f1 (f1 c_2 c_6) c_2) (f1 c_2 (f1 c_6 c_2))) (= (f1 (f1 c_2 c_6) c_3) (f1 c_2 (f1 c_6 c_3))) (= (f1 (f1 c_2 c_6) c_4) (f1 c_2 (f1 c_6 c_4))) (= (f1 (f1 c_2 c_6) c_5) (f1 c_2 (f1 c_6 c_5))) (= (f1 (f1 c_2 c_6) c_6) (f1 c_2 (f1 c_6 c_6))) (= (f1 (f1 c_2 c_6) c_7) (f1 c_2 (f1 c_6 c_7))) (= (f1 (f1 c_2 c_7) c_0) (f1 c_2 (f1 c_7 c_0))) (= (f1 (f1 c_2 c_7) c_1) (f1 c_2 (f1 c_7 c_1))) (= (f1 (f1 c_2 c_7) c_2) (f1 c_2 (f1 c_7 c_2))) (= (f1 (f1 c_2 c_7) c_3) (f1 c_2 (f1 c_7 c_3))) (= (f1 (f1 c_2 c_7) c_4) (f1 c_2 (f1 c_7 c_4))) (= (f1 (f1 c_2 c_7) c_5) (f1 c_2 (f1 c_7 c_5))) (= (f1 (f1 c_2 c_7) c_6) (f1 c_2 (f1 c_7 c_6))) (= (f1 (f1 c_2 c_7) c_7) (f1 c_2 (f1 c_7 c_7))) (= (f1 (f1 c_3 c_0) c_0) (f1 c_3 (f1 c_0 c_0))) (= (f1 (f1 c_3 c_0) c_1) (f1 c_3 (f1 c_0 c_1))) (= (f1 (f1 c_3 c_0) c_2) (f1 c_3 (f1 c_0 c_2))) (= (f1 (f1 c_3 c_0) c_3) (f1 c_3 (f1 c_0 c_3))) (= (f1 (f1 c_3 c_0) c_4) (f1 c_3 (f1 c_0 c_4))) (= (f1 (f1 c_3 c_0) c_5) (f1 c_3 (f1 c_0 c_5))) (= (f1 (f1 c_3 c_0) c_6) (f1 c_3 (f1 c_0 c_6))) (= (f1 (f1 c_3 c_0) c_7) (f1 c_3 (f1 c_0 c_7))) (= (f1 (f1 c_3 c_1) c_0) (f1 c_3 (f1 c_1 c_0))) (= (f1 (f1 c_3 c_1) c_1) (f1 c_3 (f1 c_1 c_1))) (= (f1 (f1 c_3 c_1) c_2) (f1 c_3 (f1 c_1 c_2))) (= (f1 (f1 c_3 c_1) c_3) (f1 c_3 (f1 c_1 c_3))) (= (f1 (f1 c_3 c_1) c_4) (f1 c_3 (f1 c_1 c_4))) (= (f1 (f1 c_3 c_1) c_5) (f1 c_3 (f1 c_1 c_5))) (= (f1 (f1 c_3 c_1) c_6) (f1 c_3 (f1 c_1 c_6))) (= (f1 (f1 c_3 c_1) c_7) (f1 c_3 (f1 c_1 c_7))) (= (f1 (f1 c_3 c_2) c_0) (f1 c_3 (f1 c_2 c_0))) (= (f1 (f1 c_3 c_2) c_1) (f1 c_3 (f1 c_2 c_1))) (= (f1 (f1 c_3 c_2) c_2) (f1 c_3 (f1 c_2 c_2))) (= (f1 (f1 c_3 c_2) c_3) (f1 c_3 (f1 c_2 c_3))) (= (f1 (f1 c_3 c_2) c_4) (f1 c_3 (f1 c_2 c_4))) (= (f1 (f1 c_3 c_2) c_5) (f1 c_3 (f1 c_2 c_5))) (= (f1 (f1 c_3 c_2) c_6) (f1 c_3 (f1 c_2 c_6))) (= (f1 (f1 c_3 c_2) c_7) (f1 c_3 (f1 c_2 c_7))) (= (f1 (f1 c_3 c_3) c_0) (f1 c_3 (f1 c_3 c_0))) (= (f1 (f1 c_3 c_3) c_1) (f1 c_3 (f1 c_3 c_1))) (= (f1 (f1 c_3 c_3) c_2) (f1 c_3 (f1 c_3 c_2))) (= (f1 (f1 c_3 c_3) c_3) (f1 c_3 (f1 c_3 c_3))) (= (f1 (f1 c_3 c_3) c_4) (f1 c_3 (f1 c_3 c_4))) (= (f1 (f1 c_3 c_3) c_5) (f1 c_3 (f1 c_3 c_5))) (= (f1 (f1 c_3 c_3) c_6) (f1 c_3 (f1 c_3 c_6))) (= (f1 (f1 c_3 c_3) c_7) (f1 c_3 (f1 c_3 c_7))) (= (f1 (f1 c_3 c_4) c_0) (f1 c_3 (f1 c_4 c_0))) (= (f1 (f1 c_3 c_4) c_1) (f1 c_3 (f1 c_4 c_1))) (= (f1 (f1 c_3 c_4) c_2) (f1 c_3 (f1 c_4 c_2))) (= (f1 (f1 c_3 c_4) c_3) (f1 c_3 (f1 c_4 c_3))) (= (f1 (f1 c_3 c_4) c_4) (f1 c_3 (f1 c_4 c_4))) (= (f1 (f1 c_3 c_4) c_5) (f1 c_3 (f1 c_4 c_5))) (= (f1 (f1 c_3 c_4) c_6) (f1 c_3 (f1 c_4 c_6))) (= (f1 (f1 c_3 c_4) c_7) (f1 c_3 (f1 c_4 c_7))) (= (f1 (f1 c_3 c_5) c_0) (f1 c_3 (f1 c_5 c_0))) (= (f1 (f1 c_3 c_5) c_1) (f1 c_3 (f1 c_5 c_1))) (= (f1 (f1 c_3 c_5) c_2) (f1 c_3 (f1 c_5 c_2))) (= (f1 (f1 c_3 c_5) c_3) (f1 c_3 (f1 c_5 c_3))) (= (f1 (f1 c_3 c_5) c_4) (f1 c_3 (f1 c_5 c_4))) (= (f1 (f1 c_3 c_5) c_5) (f1 c_3 (f1 c_5 c_5))) (= (f1 (f1 c_3 c_5) c_6) (f1 c_3 (f1 c_5 c_6))) (= (f1 (f1 c_3 c_5) c_7) (f1 c_3 (f1 c_5 c_7))) (= (f1 (f1 c_3 c_6) c_0) (f1 c_3 (f1 c_6 c_0))) (= (f1 (f1 c_3 c_6) c_1) (f1 c_3 (f1 c_6 c_1))) (= (f1 (f1 c_3 c_6) c_2) (f1 c_3 (f1 c_6 c_2))) (= (f1 (f1 c_3 c_6) c_3) (f1 c_3 (f1 c_6 c_3))) (= (f1 (f1 c_3 c_6) c_4) (f1 c_3 (f1 c_6 c_4))) (= (f1 (f1 c_3 c_6) c_5) (f1 c_3 (f1 c_6 c_5))) (= (f1 (f1 c_3 c_6) c_6) (f1 c_3 (f1 c_6 c_6))) (= (f1 (f1 c_3 c_6) c_7) (f1 c_3 (f1 c_6 c_7))) (= (f1 (f1 c_3 c_7) c_0) (f1 c_3 (f1 c_7 c_0))) (= (f1 (f1 c_3 c_7) c_1) (f1 c_3 (f1 c_7 c_1))) (= (f1 (f1 c_3 c_7) c_2) (f1 c_3 (f1 c_7 c_2))) (= (f1 (f1 c_3 c_7) c_3) (f1 c_3 (f1 c_7 c_3))) (= (f1 (f1 c_3 c_7) c_4) (f1 c_3 (f1 c_7 c_4))) (= (f1 (f1 c_3 c_7) c_5) (f1 c_3 (f1 c_7 c_5))) (= (f1 (f1 c_3 c_7) c_6) (f1 c_3 (f1 c_7 c_6))) (= (f1 (f1 c_3 c_7) c_7) (f1 c_3 (f1 c_7 c_7))) (= (f1 (f1 c_4 c_0) c_0) (f1 c_4 (f1 c_0 c_0))) (= (f1 (f1 c_4 c_0) c_1) (f1 c_4 (f1 c_0 c_1))) (= (f1 (f1 c_4 c_0) c_2) (f1 c_4 (f1 c_0 c_2))) (= (f1 (f1 c_4 c_0) c_3) (f1 c_4 (f1 c_0 c_3))) (= (f1 (f1 c_4 c_0) c_4) (f1 c_4 (f1 c_0 c_4))) (= (f1 (f1 c_4 c_0) c_5) (f1 c_4 (f1 c_0 c_5))) (= (f1 (f1 c_4 c_0) c_6) (f1 c_4 (f1 c_0 c_6))) (= (f1 (f1 c_4 c_0) c_7) (f1 c_4 (f1 c_0 c_7))) (= (f1 (f1 c_4 c_1) c_0) (f1 c_4 (f1 c_1 c_0))) (= (f1 (f1 c_4 c_1) c_1) (f1 c_4 (f1 c_1 c_1))) (= (f1 (f1 c_4 c_1) c_2) (f1 c_4 (f1 c_1 c_2))) (= (f1 (f1 c_4 c_1) c_3) (f1 c_4 (f1 c_1 c_3))) (= (f1 (f1 c_4 c_1) c_4) (f1 c_4 (f1 c_1 c_4))) (= (f1 (f1 c_4 c_1) c_5) (f1 c_4 (f1 c_1 c_5))) (= (f1 (f1 c_4 c_1) c_6) (f1 c_4 (f1 c_1 c_6))) (= (f1 (f1 c_4 c_1) c_7) (f1 c_4 (f1 c_1 c_7))) (= (f1 (f1 c_4 c_2) c_0) (f1 c_4 (f1 c_2 c_0))) (= (f1 (f1 c_4 c_2) c_1) (f1 c_4 (f1 c_2 c_1))) (= (f1 (f1 c_4 c_2) c_2) (f1 c_4 (f1 c_2 c_2))) (= (f1 (f1 c_4 c_2) c_3) (f1 c_4 (f1 c_2 c_3))) (= (f1 (f1 c_4 c_2) c_4) (f1 c_4 (f1 c_2 c_4))) (= (f1 (f1 c_4 c_2) c_5) (f1 c_4 (f1 c_2 c_5))) (= (f1 (f1 c_4 c_2) c_6) (f1 c_4 (f1 c_2 c_6))) (= (f1 (f1 c_4 c_2) c_7) (f1 c_4 (f1 c_2 c_7))) (= (f1 (f1 c_4 c_3) c_0) (f1 c_4 (f1 c_3 c_0))) (= (f1 (f1 c_4 c_3) c_1) (f1 c_4 (f1 c_3 c_1))) (= (f1 (f1 c_4 c_3) c_2) (f1 c_4 (f1 c_3 c_2))) (= (f1 (f1 c_4 c_3) c_3) (f1 c_4 (f1 c_3 c_3))) (= (f1 (f1 c_4 c_3) c_4) (f1 c_4 (f1 c_3 c_4))) (= (f1 (f1 c_4 c_3) c_5) (f1 c_4 (f1 c_3 c_5))) (= (f1 (f1 c_4 c_3) c_6) (f1 c_4 (f1 c_3 c_6))) (= (f1 (f1 c_4 c_3) c_7) (f1 c_4 (f1 c_3 c_7))) (= (f1 (f1 c_4 c_4) c_0) (f1 c_4 (f1 c_4 c_0))) (= (f1 (f1 c_4 c_4) c_1) (f1 c_4 (f1 c_4 c_1))) (= (f1 (f1 c_4 c_4) c_2) (f1 c_4 (f1 c_4 c_2))) (= (f1 (f1 c_4 c_4) c_3) (f1 c_4 (f1 c_4 c_3))) (= (f1 (f1 c_4 c_4) c_4) (f1 c_4 (f1 c_4 c_4))) (= (f1 (f1 c_4 c_4) c_5) (f1 c_4 (f1 c_4 c_5))) (= (f1 (f1 c_4 c_4) c_6) (f1 c_4 (f1 c_4 c_6))) (= (f1 (f1 c_4 c_4) c_7) (f1 c_4 (f1 c_4 c_7))) (= (f1 (f1 c_4 c_5) c_0) (f1 c_4 (f1 c_5 c_0))) (= (f1 (f1 c_4 c_5) c_1) (f1 c_4 (f1 c_5 c_1))) (= (f1 (f1 c_4 c_5) c_2) (f1 c_4 (f1 c_5 c_2))) (= (f1 (f1 c_4 c_5) c_3) (f1 c_4 (f1 c_5 c_3))) (= (f1 (f1 c_4 c_5) c_4) (f1 c_4 (f1 c_5 c_4))) (= (f1 (f1 c_4 c_5) c_5) (f1 c_4 (f1 c_5 c_5))) (= (f1 (f1 c_4 c_5) c_6) (f1 c_4 (f1 c_5 c_6))) (= (f1 (f1 c_4 c_5) c_7) (f1 c_4 (f1 c_5 c_7))) (= (f1 (f1 c_4 c_6) c_0) (f1 c_4 (f1 c_6 c_0))) (= (f1 (f1 c_4 c_6) c_1) (f1 c_4 (f1 c_6 c_1))) (= (f1 (f1 c_4 c_6) c_2) (f1 c_4 (f1 c_6 c_2))) (= (f1 (f1 c_4 c_6) c_3) (f1 c_4 (f1 c_6 c_3))) (= (f1 (f1 c_4 c_6) c_4) (f1 c_4 (f1 c_6 c_4))) (= (f1 (f1 c_4 c_6) c_5) (f1 c_4 (f1 c_6 c_5))) (= (f1 (f1 c_4 c_6) c_6) (f1 c_4 (f1 c_6 c_6))) (= (f1 (f1 c_4 c_6) c_7) (f1 c_4 (f1 c_6 c_7))) (= (f1 (f1 c_4 c_7) c_0) (f1 c_4 (f1 c_7 c_0))) (= (f1 (f1 c_4 c_7) c_1) (f1 c_4 (f1 c_7 c_1))) (= (f1 (f1 c_4 c_7) c_2) (f1 c_4 (f1 c_7 c_2))) (= (f1 (f1 c_4 c_7) c_3) (f1 c_4 (f1 c_7 c_3))) (= (f1 (f1 c_4 c_7) c_4) (f1 c_4 (f1 c_7 c_4))) (= (f1 (f1 c_4 c_7) c_5) (f1 c_4 (f1 c_7 c_5))) (= (f1 (f1 c_4 c_7) c_6) (f1 c_4 (f1 c_7 c_6))) (= (f1 (f1 c_4 c_7) c_7) (f1 c_4 (f1 c_7 c_7))) (= (f1 (f1 c_5 c_0) c_0) (f1 c_5 (f1 c_0 c_0))) (= (f1 (f1 c_5 c_0) c_1) (f1 c_5 (f1 c_0 c_1))) (= (f1 (f1 c_5 c_0) c_2) (f1 c_5 (f1 c_0 c_2))) (= (f1 (f1 c_5 c_0) c_3) (f1 c_5 (f1 c_0 c_3))) (= (f1 (f1 c_5 c_0) c_4) (f1 c_5 (f1 c_0 c_4))) (= (f1 (f1 c_5 c_0) c_5) (f1 c_5 (f1 c_0 c_5))) (= (f1 (f1 c_5 c_0) c_6) (f1 c_5 (f1 c_0 c_6))) (= (f1 (f1 c_5 c_0) c_7) (f1 c_5 (f1 c_0 c_7))) (= (f1 (f1 c_5 c_1) c_0) (f1 c_5 (f1 c_1 c_0))) (= (f1 (f1 c_5 c_1) c_1) (f1 c_5 (f1 c_1 c_1))) (= (f1 (f1 c_5 c_1) c_2) (f1 c_5 (f1 c_1 c_2))) (= (f1 (f1 c_5 c_1) c_3) (f1 c_5 (f1 c_1 c_3))) (= (f1 (f1 c_5 c_1) c_4) (f1 c_5 (f1 c_1 c_4))) (= (f1 (f1 c_5 c_1) c_5) (f1 c_5 (f1 c_1 c_5))) (= (f1 (f1 c_5 c_1) c_6) (f1 c_5 (f1 c_1 c_6))) (= (f1 (f1 c_5 c_1) c_7) (f1 c_5 (f1 c_1 c_7))) (= (f1 (f1 c_5 c_2) c_0) (f1 c_5 (f1 c_2 c_0))) (= (f1 (f1 c_5 c_2) c_1) (f1 c_5 (f1 c_2 c_1))) (= (f1 (f1 c_5 c_2) c_2) (f1 c_5 (f1 c_2 c_2))) (= (f1 (f1 c_5 c_2) c_3) (f1 c_5 (f1 c_2 c_3))) (= (f1 (f1 c_5 c_2) c_4) (f1 c_5 (f1 c_2 c_4))) (= (f1 (f1 c_5 c_2) c_5) (f1 c_5 (f1 c_2 c_5))) (= (f1 (f1 c_5 c_2) c_6) (f1 c_5 (f1 c_2 c_6))) (= (f1 (f1 c_5 c_2) c_7) (f1 c_5 (f1 c_2 c_7))) (= (f1 (f1 c_5 c_3) c_0) (f1 c_5 (f1 c_3 c_0))) (= (f1 (f1 c_5 c_3) c_1) (f1 c_5 (f1 c_3 c_1))) (= (f1 (f1 c_5 c_3) c_2) (f1 c_5 (f1 c_3 c_2))) (= (f1 (f1 c_5 c_3) c_3) (f1 c_5 (f1 c_3 c_3))) (= (f1 (f1 c_5 c_3) c_4) (f1 c_5 (f1 c_3 c_4))) (= (f1 (f1 c_5 c_3) c_5) (f1 c_5 (f1 c_3 c_5))) (= (f1 (f1 c_5 c_3) c_6) (f1 c_5 (f1 c_3 c_6))) (= (f1 (f1 c_5 c_3) c_7) (f1 c_5 (f1 c_3 c_7))) (= (f1 (f1 c_5 c_4) c_0) (f1 c_5 (f1 c_4 c_0))) (= (f1 (f1 c_5 c_4) c_1) (f1 c_5 (f1 c_4 c_1))) (= (f1 (f1 c_5 c_4) c_2) (f1 c_5 (f1 c_4 c_2))) (= (f1 (f1 c_5 c_4) c_3) (f1 c_5 (f1 c_4 c_3))) (= (f1 (f1 c_5 c_4) c_4) (f1 c_5 (f1 c_4 c_4))) (= (f1 (f1 c_5 c_4) c_5) (f1 c_5 (f1 c_4 c_5))) (= (f1 (f1 c_5 c_4) c_6) (f1 c_5 (f1 c_4 c_6))) (= (f1 (f1 c_5 c_4) c_7) (f1 c_5 (f1 c_4 c_7))) (= (f1 (f1 c_5 c_5) c_0) (f1 c_5 (f1 c_5 c_0))) (= (f1 (f1 c_5 c_5) c_1) (f1 c_5 (f1 c_5 c_1))) (= (f1 (f1 c_5 c_5) c_2) (f1 c_5 (f1 c_5 c_2))) (= (f1 (f1 c_5 c_5) c_3) (f1 c_5 (f1 c_5 c_3))) (= (f1 (f1 c_5 c_5) c_4) (f1 c_5 (f1 c_5 c_4))) (= (f1 (f1 c_5 c_5) c_5) (f1 c_5 (f1 c_5 c_5))) (= (f1 (f1 c_5 c_5) c_6) (f1 c_5 (f1 c_5 c_6))) (= (f1 (f1 c_5 c_5) c_7) (f1 c_5 (f1 c_5 c_7))) (= (f1 (f1 c_5 c_6) c_0) (f1 c_5 (f1 c_6 c_0))) (= (f1 (f1 c_5 c_6) c_1) (f1 c_5 (f1 c_6 c_1))) (= (f1 (f1 c_5 c_6) c_2) (f1 c_5 (f1 c_6 c_2))) (= (f1 (f1 c_5 c_6) c_3) (f1 c_5 (f1 c_6 c_3))) (= (f1 (f1 c_5 c_6) c_4) (f1 c_5 (f1 c_6 c_4))) (= (f1 (f1 c_5 c_6) c_5) (f1 c_5 (f1 c_6 c_5))) (= (f1 (f1 c_5 c_6) c_6) (f1 c_5 (f1 c_6 c_6))) (= (f1 (f1 c_5 c_6) c_7) (f1 c_5 (f1 c_6 c_7))) (= (f1 (f1 c_5 c_7) c_0) (f1 c_5 (f1 c_7 c_0))) (= (f1 (f1 c_5 c_7) c_1) (f1 c_5 (f1 c_7 c_1))) (= (f1 (f1 c_5 c_7) c_2) (f1 c_5 (f1 c_7 c_2))) (= (f1 (f1 c_5 c_7) c_3) (f1 c_5 (f1 c_7 c_3))) (= (f1 (f1 c_5 c_7) c_4) (f1 c_5 (f1 c_7 c_4))) (= (f1 (f1 c_5 c_7) c_5) (f1 c_5 (f1 c_7 c_5))) (= (f1 (f1 c_5 c_7) c_6) (f1 c_5 (f1 c_7 c_6))) (= (f1 (f1 c_5 c_7) c_7) (f1 c_5 (f1 c_7 c_7))) (= (f1 (f1 c_6 c_0) c_0) (f1 c_6 (f1 c_0 c_0))) (= (f1 (f1 c_6 c_0) c_1) (f1 c_6 (f1 c_0 c_1))) (= (f1 (f1 c_6 c_0) c_2) (f1 c_6 (f1 c_0 c_2))) (= (f1 (f1 c_6 c_0) c_3) (f1 c_6 (f1 c_0 c_3))) (= (f1 (f1 c_6 c_0) c_4) (f1 c_6 (f1 c_0 c_4))) (= (f1 (f1 c_6 c_0) c_5) (f1 c_6 (f1 c_0 c_5))) (= (f1 (f1 c_6 c_0) c_6) (f1 c_6 (f1 c_0 c_6))) (= (f1 (f1 c_6 c_0) c_7) (f1 c_6 (f1 c_0 c_7))) (= (f1 (f1 c_6 c_1) c_0) (f1 c_6 (f1 c_1 c_0))) (= (f1 (f1 c_6 c_1) c_1) (f1 c_6 (f1 c_1 c_1))) (= (f1 (f1 c_6 c_1) c_2) (f1 c_6 (f1 c_1 c_2))) (= (f1 (f1 c_6 c_1) c_3) (f1 c_6 (f1 c_1 c_3))) (= (f1 (f1 c_6 c_1) c_4) (f1 c_6 (f1 c_1 c_4))) (= (f1 (f1 c_6 c_1) c_5) (f1 c_6 (f1 c_1 c_5))) (= (f1 (f1 c_6 c_1) c_6) (f1 c_6 (f1 c_1 c_6))) (= (f1 (f1 c_6 c_1) c_7) (f1 c_6 (f1 c_1 c_7))) (= (f1 (f1 c_6 c_2) c_0) (f1 c_6 (f1 c_2 c_0))) (= (f1 (f1 c_6 c_2) c_1) (f1 c_6 (f1 c_2 c_1))) (= (f1 (f1 c_6 c_2) c_2) (f1 c_6 (f1 c_2 c_2))) (= (f1 (f1 c_6 c_2) c_3) (f1 c_6 (f1 c_2 c_3))) (= (f1 (f1 c_6 c_2) c_4) (f1 c_6 (f1 c_2 c_4))) (= (f1 (f1 c_6 c_2) c_5) (f1 c_6 (f1 c_2 c_5))) (= (f1 (f1 c_6 c_2) c_6) (f1 c_6 (f1 c_2 c_6))) (= (f1 (f1 c_6 c_2) c_7) (f1 c_6 (f1 c_2 c_7))) (= (f1 (f1 c_6 c_3) c_0) (f1 c_6 (f1 c_3 c_0))) (= (f1 (f1 c_6 c_3) c_1) (f1 c_6 (f1 c_3 c_1))) (= (f1 (f1 c_6 c_3) c_2) (f1 c_6 (f1 c_3 c_2))) (= (f1 (f1 c_6 c_3) c_3) (f1 c_6 (f1 c_3 c_3))) (= (f1 (f1 c_6 c_3) c_4) (f1 c_6 (f1 c_3 c_4))) (= (f1 (f1 c_6 c_3) c_5) (f1 c_6 (f1 c_3 c_5))) (= (f1 (f1 c_6 c_3) c_6) (f1 c_6 (f1 c_3 c_6))) (= (f1 (f1 c_6 c_3) c_7) (f1 c_6 (f1 c_3 c_7))) (= (f1 (f1 c_6 c_4) c_0) (f1 c_6 (f1 c_4 c_0))) (= (f1 (f1 c_6 c_4) c_1) (f1 c_6 (f1 c_4 c_1))) (= (f1 (f1 c_6 c_4) c_2) (f1 c_6 (f1 c_4 c_2))) (= (f1 (f1 c_6 c_4) c_3) (f1 c_6 (f1 c_4 c_3))) (= (f1 (f1 c_6 c_4) c_4) (f1 c_6 (f1 c_4 c_4))) (= (f1 (f1 c_6 c_4) c_5) (f1 c_6 (f1 c_4 c_5))) (= (f1 (f1 c_6 c_4) c_6) (f1 c_6 (f1 c_4 c_6))) (= (f1 (f1 c_6 c_4) c_7) (f1 c_6 (f1 c_4 c_7))) (= (f1 (f1 c_6 c_5) c_0) (f1 c_6 (f1 c_5 c_0))) (= (f1 (f1 c_6 c_5) c_1) (f1 c_6 (f1 c_5 c_1))) (= (f1 (f1 c_6 c_5) c_2) (f1 c_6 (f1 c_5 c_2))) (= (f1 (f1 c_6 c_5) c_3) (f1 c_6 (f1 c_5 c_3))) (= (f1 (f1 c_6 c_5) c_4) (f1 c_6 (f1 c_5 c_4))) (= (f1 (f1 c_6 c_5) c_5) (f1 c_6 (f1 c_5 c_5))) (= (f1 (f1 c_6 c_5) c_6) (f1 c_6 (f1 c_5 c_6))) (= (f1 (f1 c_6 c_5) c_7) (f1 c_6 (f1 c_5 c_7))) (= (f1 (f1 c_6 c_6) c_0) (f1 c_6 (f1 c_6 c_0))) (= (f1 (f1 c_6 c_6) c_1) (f1 c_6 (f1 c_6 c_1))) (= (f1 (f1 c_6 c_6) c_2) (f1 c_6 (f1 c_6 c_2))) (= (f1 (f1 c_6 c_6) c_3) (f1 c_6 (f1 c_6 c_3))) (= (f1 (f1 c_6 c_6) c_4) (f1 c_6 (f1 c_6 c_4))) (= (f1 (f1 c_6 c_6) c_5) (f1 c_6 (f1 c_6 c_5))) (= (f1 (f1 c_6 c_6) c_6) (f1 c_6 (f1 c_6 c_6))) (= (f1 (f1 c_6 c_6) c_7) (f1 c_6 (f1 c_6 c_7))) (= (f1 (f1 c_6 c_7) c_0) (f1 c_6 (f1 c_7 c_0))) (= (f1 (f1 c_6 c_7) c_1) (f1 c_6 (f1 c_7 c_1))) (= (f1 (f1 c_6 c_7) c_2) (f1 c_6 (f1 c_7 c_2))) (= (f1 (f1 c_6 c_7) c_3) (f1 c_6 (f1 c_7 c_3))) (= (f1 (f1 c_6 c_7) c_4) (f1 c_6 (f1 c_7 c_4))) (= (f1 (f1 c_6 c_7) c_5) (f1 c_6 (f1 c_7 c_5))) (= (f1 (f1 c_6 c_7) c_6) (f1 c_6 (f1 c_7 c_6))) (= (f1 (f1 c_6 c_7) c_7) (f1 c_6 (f1 c_7 c_7))) (= (f1 (f1 c_7 c_0) c_0) (f1 c_7 (f1 c_0 c_0))) (= (f1 (f1 c_7 c_0) c_1) (f1 c_7 (f1 c_0 c_1))) (= (f1 (f1 c_7 c_0) c_2) (f1 c_7 (f1 c_0 c_2))) (= (f1 (f1 c_7 c_0) c_3) (f1 c_7 (f1 c_0 c_3))) (= (f1 (f1 c_7 c_0) c_4) (f1 c_7 (f1 c_0 c_4))) (= (f1 (f1 c_7 c_0) c_5) (f1 c_7 (f1 c_0 c_5))) (= (f1 (f1 c_7 c_0) c_6) (f1 c_7 (f1 c_0 c_6))) (= (f1 (f1 c_7 c_0) c_7) (f1 c_7 (f1 c_0 c_7))) (= (f1 (f1 c_7 c_1) c_0) (f1 c_7 (f1 c_1 c_0))) (= (f1 (f1 c_7 c_1) c_1) (f1 c_7 (f1 c_1 c_1))) (= (f1 (f1 c_7 c_1) c_2) (f1 c_7 (f1 c_1 c_2))) (= (f1 (f1 c_7 c_1) c_3) (f1 c_7 (f1 c_1 c_3))) (= (f1 (f1 c_7 c_1) c_4) (f1 c_7 (f1 c_1 c_4))) (= (f1 (f1 c_7 c_1) c_5) (f1 c_7 (f1 c_1 c_5))) (= (f1 (f1 c_7 c_1) c_6) (f1 c_7 (f1 c_1 c_6))) (= (f1 (f1 c_7 c_1) c_7) (f1 c_7 (f1 c_1 c_7))) (= (f1 (f1 c_7 c_2) c_0) (f1 c_7 (f1 c_2 c_0))) (= (f1 (f1 c_7 c_2) c_1) (f1 c_7 (f1 c_2 c_1))) (= (f1 (f1 c_7 c_2) c_2) (f1 c_7 (f1 c_2 c_2))) (= (f1 (f1 c_7 c_2) c_3) (f1 c_7 (f1 c_2 c_3))) (= (f1 (f1 c_7 c_2) c_4) (f1 c_7 (f1 c_2 c_4))) (= (f1 (f1 c_7 c_2) c_5) (f1 c_7 (f1 c_2 c_5))) (= (f1 (f1 c_7 c_2) c_6) (f1 c_7 (f1 c_2 c_6))) (= (f1 (f1 c_7 c_2) c_7) (f1 c_7 (f1 c_2 c_7))) (= (f1 (f1 c_7 c_3) c_0) (f1 c_7 (f1 c_3 c_0))) (= (f1 (f1 c_7 c_3) c_1) (f1 c_7 (f1 c_3 c_1))) (= (f1 (f1 c_7 c_3) c_2) (f1 c_7 (f1 c_3 c_2))) (= (f1 (f1 c_7 c_3) c_3) (f1 c_7 (f1 c_3 c_3))) (= (f1 (f1 c_7 c_3) c_4) (f1 c_7 (f1 c_3 c_4))) (= (f1 (f1 c_7 c_3) c_5) (f1 c_7 (f1 c_3 c_5))) (= (f1 (f1 c_7 c_3) c_6) (f1 c_7 (f1 c_3 c_6))) (= (f1 (f1 c_7 c_3) c_7) (f1 c_7 (f1 c_3 c_7))) (= (f1 (f1 c_7 c_4) c_0) (f1 c_7 (f1 c_4 c_0))) (= (f1 (f1 c_7 c_4) c_1) (f1 c_7 (f1 c_4 c_1))) (= (f1 (f1 c_7 c_4) c_2) (f1 c_7 (f1 c_4 c_2))) (= (f1 (f1 c_7 c_4) c_3) (f1 c_7 (f1 c_4 c_3))) (= (f1 (f1 c_7 c_4) c_4) (f1 c_7 (f1 c_4 c_4))) (= (f1 (f1 c_7 c_4) c_5) (f1 c_7 (f1 c_4 c_5))) (= (f1 (f1 c_7 c_4) c_6) (f1 c_7 (f1 c_4 c_6))) (= (f1 (f1 c_7 c_4) c_7) (f1 c_7 (f1 c_4 c_7))) (= (f1 (f1 c_7 c_5) c_0) (f1 c_7 (f1 c_5 c_0))) (= (f1 (f1 c_7 c_5) c_1) (f1 c_7 (f1 c_5 c_1))) (= (f1 (f1 c_7 c_5) c_2) (f1 c_7 (f1 c_5 c_2))) (= (f1 (f1 c_7 c_5) c_3) (f1 c_7 (f1 c_5 c_3))) (= (f1 (f1 c_7 c_5) c_4) (f1 c_7 (f1 c_5 c_4))) (= (f1 (f1 c_7 c_5) c_5) (f1 c_7 (f1 c_5 c_5))) (= (f1 (f1 c_7 c_5) c_6) (f1 c_7 (f1 c_5 c_6))) (= (f1 (f1 c_7 c_5) c_7) (f1 c_7 (f1 c_5 c_7))) (= (f1 (f1 c_7 c_6) c_0) (f1 c_7 (f1 c_6 c_0))) (= (f1 (f1 c_7 c_6) c_1) (f1 c_7 (f1 c_6 c_1))) (= (f1 (f1 c_7 c_6) c_2) (f1 c_7 (f1 c_6 c_2))) (= (f1 (f1 c_7 c_6) c_3) (f1 c_7 (f1 c_6 c_3))) (= (f1 (f1 c_7 c_6) c_4) (f1 c_7 (f1 c_6 c_4))) (= (f1 (f1 c_7 c_6) c_5) (f1 c_7 (f1 c_6 c_5))) (= (f1 (f1 c_7 c_6) c_6) (f1 c_7 (f1 c_6 c_6))) (= (f1 (f1 c_7 c_6) c_7) (f1 c_7 (f1 c_6 c_7))) (= (f1 (f1 c_7 c_7) c_0) (f1 c_7 (f1 c_7 c_0))) (= (f1 (f1 c_7 c_7) c_1) (f1 c_7 (f1 c_7 c_1))) (= (f1 (f1 c_7 c_7) c_2) (f1 c_7 (f1 c_7 c_2))) (= (f1 (f1 c_7 c_7) c_3) (f1 c_7 (f1 c_7 c_3))) (= (f1 (f1 c_7 c_7) c_4) (f1 c_7 (f1 c_7 c_4))) (= (f1 (f1 c_7 c_7) c_5) (f1 c_7 (f1 c_7 c_5))) (= (f1 (f1 c_7 c_7) c_6) (f1 c_7 (f1 c_7 c_6))) (= (f1 (f1 c_7 c_7) c_7) (f1 c_7 (f1 c_7 c_7))) (= (f2 c_0 c_0) c_0) (= (f2 c_1 c_1) c_1) (= (f2 c_2 c_2) c_2) (= (f2 c_3 c_3) c_3) (= (f2 c_4 c_4) c_4) (= (f2 c_5 c_5) c_5) (= (f2 c_6 c_6) c_6) (= (f2 c_7 c_7) c_7) (= (f1 (f3 c_0) c_0) c5) (= (f1 (f3 c_1) c_1) c5) (= (f1 (f3 c_2) c_2) c5) (= (f1 (f3 c_3) c_3) c5) (= (f1 (f3 c_4) c_4) c5) (= (f1 (f3 c_5) c_5) c5) (= (f1 (f3 c_6) c_6) c5) (= (f1 (f3 c_7) c_7) c5) (= (f1 c_0 (f2 c_0 c_0)) c_0) (= (f1 c_0 (f2 c_0 c_1)) c_0) (= (f1 c_0 (f2 c_0 c_2)) c_0) (= (f1 c_0 (f2 c_0 c_3)) c_0) (= (f1 c_0 (f2 c_0 c_4)) c_0) (= (f1 c_0 (f2 c_0 c_5)) c_0) (= (f1 c_0 (f2 c_0 c_6)) c_0) (= (f1 c_0 (f2 c_0 c_7)) c_0) (= (f1 c_1 (f2 c_1 c_0)) c_1) (= (f1 c_1 (f2 c_1 c_1)) c_1) (= (f1 c_1 (f2 c_1 c_2)) c_1) (= (f1 c_1 (f2 c_1 c_3)) c_1) (= (f1 c_1 (f2 c_1 c_4)) c_1) (= (f1 c_1 (f2 c_1 c_5)) c_1) (= (f1 c_1 (f2 c_1 c_6)) c_1) (= (f1 c_1 (f2 c_1 c_7)) c_1) (= (f1 c_2 (f2 c_2 c_0)) c_2) (= (f1 c_2 (f2 c_2 c_1)) c_2) (= (f1 c_2 (f2 c_2 c_2)) c_2) (= (f1 c_2 (f2 c_2 c_3)) c_2) (= (f1 c_2 (f2 c_2 c_4)) c_2) (= (f1 c_2 (f2 c_2 c_5)) c_2) (= (f1 c_2 (f2 c_2 c_6)) c_2) (= (f1 c_2 (f2 c_2 c_7)) c_2) (= (f1 c_3 (f2 c_3 c_0)) c_3) (= (f1 c_3 (f2 c_3 c_1)) c_3) (= (f1 c_3 (f2 c_3 c_2)) c_3) (= (f1 c_3 (f2 c_3 c_3)) c_3) (= (f1 c_3 (f2 c_3 c_4)) c_3) (= (f1 c_3 (f2 c_3 c_5)) c_3) (= (f1 c_3 (f2 c_3 c_6)) c_3) (= (f1 c_3 (f2 c_3 c_7)) c_3) (= (f1 c_4 (f2 c_4 c_0)) c_4) (= (f1 c_4 (f2 c_4 c_1)) c_4) (= (f1 c_4 (f2 c_4 c_2)) c_4) (= (f1 c_4 (f2 c_4 c_3)) c_4) (= (f1 c_4 (f2 c_4 c_4)) c_4) (= (f1 c_4 (f2 c_4 c_5)) c_4) (= (f1 c_4 (f2 c_4 c_6)) c_4) (= (f1 c_4 (f2 c_4 c_7)) c_4) (= (f1 c_5 (f2 c_5 c_0)) c_5) (= (f1 c_5 (f2 c_5 c_1)) c_5) (= (f1 c_5 (f2 c_5 c_2)) c_5) (= (f1 c_5 (f2 c_5 c_3)) c_5) (= (f1 c_5 (f2 c_5 c_4)) c_5) (= (f1 c_5 (f2 c_5 c_5)) c_5) (= (f1 c_5 (f2 c_5 c_6)) c_5) (= (f1 c_5 (f2 c_5 c_7)) c_5) (= (f1 c_6 (f2 c_6 c_0)) c_6) (= (f1 c_6 (f2 c_6 c_1)) c_6) (= (f1 c_6 (f2 c_6 c_2)) c_6) (= (f1 c_6 (f2 c_6 c_3)) c_6) (= (f1 c_6 (f2 c_6 c_4)) c_6) (= (f1 c_6 (f2 c_6 c_5)) c_6) (= (f1 c_6 (f2 c_6 c_6)) c_6) (= (f1 c_6 (f2 c_6 c_7)) c_6) (= (f1 c_7 (f2 c_7 c_0)) c_7) (= (f1 c_7 (f2 c_7 c_1)) c_7) (= (f1 c_7 (f2 c_7 c_2)) c_7) (= (f1 c_7 (f2 c_7 c_3)) c_7) (= (f1 c_7 (f2 c_7 c_4)) c_7) (= (f1 c_7 (f2 c_7 c_5)) c_7) (= (f1 c_7 (f2 c_7 c_6)) c_7) (= (f1 c_7 (f2 c_7 c_7)) c_7) (= (f3 (f3 c_0)) c_0) (= (f3 (f3 c_1)) c_1) (= (f3 (f3 c_2)) c_2) (= (f3 (f3 c_3)) c_3) (= (f3 (f3 c_4)) c_4) (= (f3 (f3 c_5)) c_5) (= (f3 (f3 c_6)) c_6) (= (f3 (f3 c_7)) c_7) (or (= (f1 c_0 c_0) c_0)(= (f1 c_0 c_0) c_1)(= (f1 c_0 c_0) c_2)(= (f1 c_0 c_0) c_3)(= (f1 c_0 c_0) c_4)(= (f1 c_0 c_0) c_5)(= (f1 c_0 c_0) c_6)(= (f1 c_0 c_0) c_7))(or (= (f1 c_0 c_1) c_0)(= (f1 c_0 c_1) c_1)(= (f1 c_0 c_1) c_2)(= (f1 c_0 c_1) c_3)(= (f1 c_0 c_1) c_4)(= (f1 c_0 c_1) c_5)(= (f1 c_0 c_1) c_6)(= (f1 c_0 c_1) c_7))(or (= (f1 c_0 c_2) c_0)(= (f1 c_0 c_2) c_1)(= (f1 c_0 c_2) c_2)(= (f1 c_0 c_2) c_3)(= (f1 c_0 c_2) c_4)(= (f1 c_0 c_2) c_5)(= (f1 c_0 c_2) c_6)(= (f1 c_0 c_2) c_7))(or (= (f1 c_0 c_3) c_0)(= (f1 c_0 c_3) c_1)(= (f1 c_0 c_3) c_2)(= (f1 c_0 c_3) c_3)(= (f1 c_0 c_3) c_4)(= (f1 c_0 c_3) c_5)(= (f1 c_0 c_3) c_6)(= (f1 c_0 c_3) c_7))(or (= (f1 c_0 c_4) c_0)(= (f1 c_0 c_4) c_1)(= (f1 c_0 c_4) c_2)(= (f1 c_0 c_4) c_3)(= (f1 c_0 c_4) c_4)(= (f1 c_0 c_4) c_5)(= (f1 c_0 c_4) c_6)(= (f1 c_0 c_4) c_7))(or (= (f1 c_0 c_5) c_0)(= (f1 c_0 c_5) c_1)(= (f1 c_0 c_5) c_2)(= (f1 c_0 c_5) c_3)(= (f1 c_0 c_5) c_4)(= (f1 c_0 c_5) c_5)(= (f1 c_0 c_5) c_6)(= (f1 c_0 c_5) c_7))(or (= (f1 c_0 c_6) c_0)(= (f1 c_0 c_6) c_1)(= (f1 c_0 c_6) c_2)(= (f1 c_0 c_6) c_3)(= (f1 c_0 c_6) c_4)(= (f1 c_0 c_6) c_5)(= (f1 c_0 c_6) c_6)(= (f1 c_0 c_6) c_7))(or (= (f1 c_0 c_7) c_0)(= (f1 c_0 c_7) c_1)(= (f1 c_0 c_7) c_2)(= (f1 c_0 c_7) c_3)(= (f1 c_0 c_7) c_4)(= (f1 c_0 c_7) c_5)(= (f1 c_0 c_7) c_6)(= (f1 c_0 c_7) c_7))(or (= (f1 c_1 c_0) c_0)(= (f1 c_1 c_0) c_1)(= (f1 c_1 c_0) c_2)(= (f1 c_1 c_0) c_3)(= (f1 c_1 c_0) c_4)(= (f1 c_1 c_0) c_5)(= (f1 c_1 c_0) c_6)(= (f1 c_1 c_0) c_7))(or (= (f1 c_1 c_1) c_0)(= (f1 c_1 c_1) c_1)(= (f1 c_1 c_1) c_2)(= (f1 c_1 c_1) c_3)(= (f1 c_1 c_1) c_4)(= (f1 c_1 c_1) c_5)(= (f1 c_1 c_1) c_6)(= (f1 c_1 c_1) c_7))(or (= (f1 c_1 c_2) c_0)(= (f1 c_1 c_2) c_1)(= (f1 c_1 c_2) c_2)(= (f1 c_1 c_2) c_3)(= (f1 c_1 c_2) c_4)(= (f1 c_1 c_2) c_5)(= (f1 c_1 c_2) c_6)(= (f1 c_1 c_2) c_7))(or (= (f1 c_1 c_3) c_0)(= (f1 c_1 c_3) c_1)(= (f1 c_1 c_3) c_2)(= (f1 c_1 c_3) c_3)(= (f1 c_1 c_3) c_4)(= (f1 c_1 c_3) c_5)(= (f1 c_1 c_3) c_6)(= (f1 c_1 c_3) c_7))(or (= (f1 c_1 c_4) c_0)(= (f1 c_1 c_4) c_1)(= (f1 c_1 c_4) c_2)(= (f1 c_1 c_4) c_3)(= (f1 c_1 c_4) c_4)(= (f1 c_1 c_4) c_5)(= (f1 c_1 c_4) c_6)(= (f1 c_1 c_4) c_7))(or (= (f1 c_1 c_5) c_0)(= (f1 c_1 c_5) c_1)(= (f1 c_1 c_5) c_2)(= (f1 c_1 c_5) c_3)(= (f1 c_1 c_5) c_4)(= (f1 c_1 c_5) c_5)(= (f1 c_1 c_5) c_6)(= (f1 c_1 c_5) c_7))(or (= (f1 c_1 c_6) c_0)(= (f1 c_1 c_6) c_1)(= (f1 c_1 c_6) c_2)(= (f1 c_1 c_6) c_3)(= (f1 c_1 c_6) c_4)(= (f1 c_1 c_6) c_5)(= (f1 c_1 c_6) c_6)(= (f1 c_1 c_6) c_7))(or (= (f1 c_1 c_7) c_0)(= (f1 c_1 c_7) c_1)(= (f1 c_1 c_7) c_2)(= (f1 c_1 c_7) c_3)(= (f1 c_1 c_7) c_4)(= (f1 c_1 c_7) c_5)(= (f1 c_1 c_7) c_6)(= (f1 c_1 c_7) c_7))(or (= (f1 c_2 c_0) c_0)(= (f1 c_2 c_0) c_1)(= (f1 c_2 c_0) c_2)(= (f1 c_2 c_0) c_3)(= (f1 c_2 c_0) c_4)(= (f1 c_2 c_0) c_5)(= (f1 c_2 c_0) c_6)(= (f1 c_2 c_0) c_7))(or (= (f1 c_2 c_1) c_0)(= (f1 c_2 c_1) c_1)(= (f1 c_2 c_1) c_2)(= (f1 c_2 c_1) c_3)(= (f1 c_2 c_1) c_4)(= (f1 c_2 c_1) c_5)(= (f1 c_2 c_1) c_6)(= (f1 c_2 c_1) c_7))(or (= (f1 c_2 c_2) c_0)(= (f1 c_2 c_2) c_1)(= (f1 c_2 c_2) c_2)(= (f1 c_2 c_2) c_3)(= (f1 c_2 c_2) c_4)(= (f1 c_2 c_2) c_5)(= (f1 c_2 c_2) c_6)(= (f1 c_2 c_2) c_7))(or (= (f1 c_2 c_3) c_0)(= (f1 c_2 c_3) c_1)(= (f1 c_2 c_3) c_2)(= (f1 c_2 c_3) c_3)(= (f1 c_2 c_3) c_4)(= (f1 c_2 c_3) c_5)(= (f1 c_2 c_3) c_6)(= (f1 c_2 c_3) c_7))(or (= (f1 c_2 c_4) c_0)(= (f1 c_2 c_4) c_1)(= (f1 c_2 c_4) c_2)(= (f1 c_2 c_4) c_3)(= (f1 c_2 c_4) c_4)(= (f1 c_2 c_4) c_5)(= (f1 c_2 c_4) c_6)(= (f1 c_2 c_4) c_7))(or (= (f1 c_2 c_5) c_0)(= (f1 c_2 c_5) c_1)(= (f1 c_2 c_5) c_2)(= (f1 c_2 c_5) c_3)(= (f1 c_2 c_5) c_4)(= (f1 c_2 c_5) c_5)(= (f1 c_2 c_5) c_6)(= (f1 c_2 c_5) c_7))(or (= (f1 c_2 c_6) c_0)(= (f1 c_2 c_6) c_1)(= (f1 c_2 c_6) c_2)(= (f1 c_2 c_6) c_3)(= (f1 c_2 c_6) c_4)(= (f1 c_2 c_6) c_5)(= (f1 c_2 c_6) c_6)(= (f1 c_2 c_6) c_7))(or (= (f1 c_2 c_7) c_0)(= (f1 c_2 c_7) c_1)(= (f1 c_2 c_7) c_2)(= (f1 c_2 c_7) c_3)(= (f1 c_2 c_7) c_4)(= (f1 c_2 c_7) c_5)(= (f1 c_2 c_7) c_6)(= (f1 c_2 c_7) c_7))(or (= (f1 c_3 c_0) c_0)(= (f1 c_3 c_0) c_1)(= (f1 c_3 c_0) c_2)(= (f1 c_3 c_0) c_3)(= (f1 c_3 c_0) c_4)(= (f1 c_3 c_0) c_5)(= (f1 c_3 c_0) c_6)(= (f1 c_3 c_0) c_7))(or (= (f1 c_3 c_1) c_0)(= (f1 c_3 c_1) c_1)(= (f1 c_3 c_1) c_2)(= (f1 c_3 c_1) c_3)(= (f1 c_3 c_1) c_4)(= (f1 c_3 c_1) c_5)(= (f1 c_3 c_1) c_6)(= (f1 c_3 c_1) c_7))(or (= (f1 c_3 c_2) c_0)(= (f1 c_3 c_2) c_1)(= (f1 c_3 c_2) c_2)(= (f1 c_3 c_2) c_3)(= (f1 c_3 c_2) c_4)(= (f1 c_3 c_2) c_5)(= (f1 c_3 c_2) c_6)(= (f1 c_3 c_2) c_7))(or (= (f1 c_3 c_3) c_0)(= (f1 c_3 c_3) c_1)(= (f1 c_3 c_3) c_2)(= (f1 c_3 c_3) c_3)(= (f1 c_3 c_3) c_4)(= (f1 c_3 c_3) c_5)(= (f1 c_3 c_3) c_6)(= (f1 c_3 c_3) c_7))(or (= (f1 c_3 c_4) c_0)(= (f1 c_3 c_4) c_1)(= (f1 c_3 c_4) c_2)(= (f1 c_3 c_4) c_3)(= (f1 c_3 c_4) c_4)(= (f1 c_3 c_4) c_5)(= (f1 c_3 c_4) c_6)(= (f1 c_3 c_4) c_7))(or (= (f1 c_3 c_5) c_0)(= (f1 c_3 c_5) c_1)(= (f1 c_3 c_5) c_2)(= (f1 c_3 c_5) c_3)(= (f1 c_3 c_5) c_4)(= (f1 c_3 c_5) c_5)(= (f1 c_3 c_5) c_6)(= (f1 c_3 c_5) c_7))(or (= (f1 c_3 c_6) c_0)(= (f1 c_3 c_6) c_1)(= (f1 c_3 c_6) c_2)(= (f1 c_3 c_6) c_3)(= (f1 c_3 c_6) c_4)(= (f1 c_3 c_6) c_5)(= (f1 c_3 c_6) c_6)(= (f1 c_3 c_6) c_7))(or (= (f1 c_3 c_7) c_0)(= (f1 c_3 c_7) c_1)(= (f1 c_3 c_7) c_2)(= (f1 c_3 c_7) c_3)(= (f1 c_3 c_7) c_4)(= (f1 c_3 c_7) c_5)(= (f1 c_3 c_7) c_6)(= (f1 c_3 c_7) c_7))(or (= (f1 c_4 c_0) c_0)(= (f1 c_4 c_0) c_1)(= (f1 c_4 c_0) c_2)(= (f1 c_4 c_0) c_3)(= (f1 c_4 c_0) c_4)(= (f1 c_4 c_0) c_5)(= (f1 c_4 c_0) c_6)(= (f1 c_4 c_0) c_7))(or (= (f1 c_4 c_1) c_0)(= (f1 c_4 c_1) c_1)(= (f1 c_4 c_1) c_2)(= (f1 c_4 c_1) c_3)(= (f1 c_4 c_1) c_4)(= (f1 c_4 c_1) c_5)(= (f1 c_4 c_1) c_6)(= (f1 c_4 c_1) c_7))(or (= (f1 c_4 c_2) c_0)(= (f1 c_4 c_2) c_1)(= (f1 c_4 c_2) c_2)(= (f1 c_4 c_2) c_3)(= (f1 c_4 c_2) c_4)(= (f1 c_4 c_2) c_5)(= (f1 c_4 c_2) c_6)(= (f1 c_4 c_2) c_7))(or (= (f1 c_4 c_3) c_0)(= (f1 c_4 c_3) c_1)(= (f1 c_4 c_3) c_2)(= (f1 c_4 c_3) c_3)(= (f1 c_4 c_3) c_4)(= (f1 c_4 c_3) c_5)(= (f1 c_4 c_3) c_6)(= (f1 c_4 c_3) c_7))(or (= (f1 c_4 c_4) c_0)(= (f1 c_4 c_4) c_1)(= (f1 c_4 c_4) c_2)(= (f1 c_4 c_4) c_3)(= (f1 c_4 c_4) c_4)(= (f1 c_4 c_4) c_5)(= (f1 c_4 c_4) c_6)(= (f1 c_4 c_4) c_7))(or (= (f1 c_4 c_5) c_0)(= (f1 c_4 c_5) c_1)(= (f1 c_4 c_5) c_2)(= (f1 c_4 c_5) c_3)(= (f1 c_4 c_5) c_4)(= (f1 c_4 c_5) c_5)(= (f1 c_4 c_5) c_6)(= (f1 c_4 c_5) c_7))(or (= (f1 c_4 c_6) c_0)(= (f1 c_4 c_6) c_1)(= (f1 c_4 c_6) c_2)(= (f1 c_4 c_6) c_3)(= (f1 c_4 c_6) c_4)(= (f1 c_4 c_6) c_5)(= (f1 c_4 c_6) c_6)(= (f1 c_4 c_6) c_7))(or (= (f1 c_4 c_7) c_0)(= (f1 c_4 c_7) c_1)(= (f1 c_4 c_7) c_2)(= (f1 c_4 c_7) c_3)(= (f1 c_4 c_7) c_4)(= (f1 c_4 c_7) c_5)(= (f1 c_4 c_7) c_6)(= (f1 c_4 c_7) c_7))(or (= (f1 c_5 c_0) c_0)(= (f1 c_5 c_0) c_1)(= (f1 c_5 c_0) c_2)(= (f1 c_5 c_0) c_3)(= (f1 c_5 c_0) c_4)(= (f1 c_5 c_0) c_5)(= (f1 c_5 c_0) c_6)(= (f1 c_5 c_0) c_7))(or (= (f1 c_5 c_1) c_0)(= (f1 c_5 c_1) c_1)(= (f1 c_5 c_1) c_2)(= (f1 c_5 c_1) c_3)(= (f1 c_5 c_1) c_4)(= (f1 c_5 c_1) c_5)(= (f1 c_5 c_1) c_6)(= (f1 c_5 c_1) c_7))(or (= (f1 c_5 c_2) c_0)(= (f1 c_5 c_2) c_1)(= (f1 c_5 c_2) c_2)(= (f1 c_5 c_2) c_3)(= (f1 c_5 c_2) c_4)(= (f1 c_5 c_2) c_5)(= (f1 c_5 c_2) c_6)(= (f1 c_5 c_2) c_7))(or (= (f1 c_5 c_3) c_0)(= (f1 c_5 c_3) c_1)(= (f1 c_5 c_3) c_2)(= (f1 c_5 c_3) c_3)(= (f1 c_5 c_3) c_4)(= (f1 c_5 c_3) c_5)(= (f1 c_5 c_3) c_6)(= (f1 c_5 c_3) c_7))(or (= (f1 c_5 c_4) c_0)(= (f1 c_5 c_4) c_1)(= (f1 c_5 c_4) c_2)(= (f1 c_5 c_4) c_3)(= (f1 c_5 c_4) c_4)(= (f1 c_5 c_4) c_5)(= (f1 c_5 c_4) c_6)(= (f1 c_5 c_4) c_7))(or (= (f1 c_5 c_5) c_0)(= (f1 c_5 c_5) c_1)(= (f1 c_5 c_5) c_2)(= (f1 c_5 c_5) c_3)(= (f1 c_5 c_5) c_4)(= (f1 c_5 c_5) c_5)(= (f1 c_5 c_5) c_6)(= (f1 c_5 c_5) c_7))(or (= (f1 c_5 c_6) c_0)(= (f1 c_5 c_6) c_1)(= (f1 c_5 c_6) c_2)(= (f1 c_5 c_6) c_3)(= (f1 c_5 c_6) c_4)(= (f1 c_5 c_6) c_5)(= (f1 c_5 c_6) c_6)(= (f1 c_5 c_6) c_7))(or (= (f1 c_5 c_7) c_0)(= (f1 c_5 c_7) c_1)(= (f1 c_5 c_7) c_2)(= (f1 c_5 c_7) c_3)(= (f1 c_5 c_7) c_4)(= (f1 c_5 c_7) c_5)(= (f1 c_5 c_7) c_6)(= (f1 c_5 c_7) c_7))(or (= (f1 c_6 c_0) c_0)(= (f1 c_6 c_0) c_1)(= (f1 c_6 c_0) c_2)(= (f1 c_6 c_0) c_3)(= (f1 c_6 c_0) c_4)(= (f1 c_6 c_0) c_5)(= (f1 c_6 c_0) c_6)(= (f1 c_6 c_0) c_7))(or (= (f1 c_6 c_1) c_0)(= (f1 c_6 c_1) c_1)(= (f1 c_6 c_1) c_2)(= (f1 c_6 c_1) c_3)(= (f1 c_6 c_1) c_4)(= (f1 c_6 c_1) c_5)(= (f1 c_6 c_1) c_6)(= (f1 c_6 c_1) c_7))(or (= (f1 c_6 c_2) c_0)(= (f1 c_6 c_2) c_1)(= (f1 c_6 c_2) c_2)(= (f1 c_6 c_2) c_3)(= (f1 c_6 c_2) c_4)(= (f1 c_6 c_2) c_5)(= (f1 c_6 c_2) c_6)(= (f1 c_6 c_2) c_7))(or (= (f1 c_6 c_3) c_0)(= (f1 c_6 c_3) c_1)(= (f1 c_6 c_3) c_2)(= (f1 c_6 c_3) c_3)(= (f1 c_6 c_3) c_4)(= (f1 c_6 c_3) c_5)(= (f1 c_6 c_3) c_6)(= (f1 c_6 c_3) c_7))(or (= (f1 c_6 c_4) c_0)(= (f1 c_6 c_4) c_1)(= (f1 c_6 c_4) c_2)(= (f1 c_6 c_4) c_3)(= (f1 c_6 c_4) c_4)(= (f1 c_6 c_4) c_5)(= (f1 c_6 c_4) c_6)(= (f1 c_6 c_4) c_7))(or (= (f1 c_6 c_5) c_0)(= (f1 c_6 c_5) c_1)(= (f1 c_6 c_5) c_2)(= (f1 c_6 c_5) c_3)(= (f1 c_6 c_5) c_4)(= (f1 c_6 c_5) c_5)(= (f1 c_6 c_5) c_6)(= (f1 c_6 c_5) c_7))(or (= (f1 c_6 c_6) c_0)(= (f1 c_6 c_6) c_1)(= (f1 c_6 c_6) c_2)(= (f1 c_6 c_6) c_3)(= (f1 c_6 c_6) c_4)(= (f1 c_6 c_6) c_5)(= (f1 c_6 c_6) c_6)(= (f1 c_6 c_6) c_7))(or (= (f1 c_6 c_7) c_0)(= (f1 c_6 c_7) c_1)(= (f1 c_6 c_7) c_2)(= (f1 c_6 c_7) c_3)(= (f1 c_6 c_7) c_4)(= (f1 c_6 c_7) c_5)(= (f1 c_6 c_7) c_6)(= (f1 c_6 c_7) c_7))(or (= (f1 c_7 c_0) c_0)(= (f1 c_7 c_0) c_1)(= (f1 c_7 c_0) c_2)(= (f1 c_7 c_0) c_3)(= (f1 c_7 c_0) c_4)(= (f1 c_7 c_0) c_5)(= (f1 c_7 c_0) c_6)(= (f1 c_7 c_0) c_7))(or (= (f1 c_7 c_1) c_0)(= (f1 c_7 c_1) c_1)(= (f1 c_7 c_1) c_2)(= (f1 c_7 c_1) c_3)(= (f1 c_7 c_1) c_4)(= (f1 c_7 c_1) c_5)(= (f1 c_7 c_1) c_6)(= (f1 c_7 c_1) c_7))(or (= (f1 c_7 c_2) c_0)(= (f1 c_7 c_2) c_1)(= (f1 c_7 c_2) c_2)(= (f1 c_7 c_2) c_3)(= (f1 c_7 c_2) c_4)(= (f1 c_7 c_2) c_5)(= (f1 c_7 c_2) c_6)(= (f1 c_7 c_2) c_7))(or (= (f1 c_7 c_3) c_0)(= (f1 c_7 c_3) c_1)(= (f1 c_7 c_3) c_2)(= (f1 c_7 c_3) c_3)(= (f1 c_7 c_3) c_4)(= (f1 c_7 c_3) c_5)(= (f1 c_7 c_3) c_6)(= (f1 c_7 c_3) c_7))(or (= (f1 c_7 c_4) c_0)(= (f1 c_7 c_4) c_1)(= (f1 c_7 c_4) c_2)(= (f1 c_7 c_4) c_3)(= (f1 c_7 c_4) c_4)(= (f1 c_7 c_4) c_5)(= (f1 c_7 c_4) c_6)(= (f1 c_7 c_4) c_7))(or (= (f1 c_7 c_5) c_0)(= (f1 c_7 c_5) c_1)(= (f1 c_7 c_5) c_2)(= (f1 c_7 c_5) c_3)(= (f1 c_7 c_5) c_4)(= (f1 c_7 c_5) c_5)(= (f1 c_7 c_5) c_6)(= (f1 c_7 c_5) c_7))(or (= (f1 c_7 c_6) c_0)(= (f1 c_7 c_6) c_1)(= (f1 c_7 c_6) c_2)(= (f1 c_7 c_6) c_3)(= (f1 c_7 c_6) c_4)(= (f1 c_7 c_6) c_5)(= (f1 c_7 c_6) c_6)(= (f1 c_7 c_6) c_7))(or (= (f1 c_7 c_7) c_0)(= (f1 c_7 c_7) c_1)(= (f1 c_7 c_7) c_2)(= (f1 c_7 c_7) c_3)(= (f1 c_7 c_7) c_4)(= (f1 c_7 c_7) c_5)(= (f1 c_7 c_7) c_6)(= (f1 c_7 c_7) c_7))(or (= (f2 c_0 c_0) c_0)(= (f2 c_0 c_0) c_1)(= (f2 c_0 c_0) c_2)(= (f2 c_0 c_0) c_3)(= (f2 c_0 c_0) c_4)(= (f2 c_0 c_0) c_5)(= (f2 c_0 c_0) c_6)(= (f2 c_0 c_0) c_7))(or (= (f2 c_0 c_1) c_0)(= (f2 c_0 c_1) c_1)(= (f2 c_0 c_1) c_2)(= (f2 c_0 c_1) c_3)(= (f2 c_0 c_1) c_4)(= (f2 c_0 c_1) c_5)(= (f2 c_0 c_1) c_6)(= (f2 c_0 c_1) c_7))(or (= (f2 c_0 c_2) c_0)(= (f2 c_0 c_2) c_1)(= (f2 c_0 c_2) c_2)(= (f2 c_0 c_2) c_3)(= (f2 c_0 c_2) c_4)(= (f2 c_0 c_2) c_5)(= (f2 c_0 c_2) c_6)(= (f2 c_0 c_2) c_7))(or (= (f2 c_0 c_3) c_0)(= (f2 c_0 c_3) c_1)(= (f2 c_0 c_3) c_2)(= (f2 c_0 c_3) c_3)(= (f2 c_0 c_3) c_4)(= (f2 c_0 c_3) c_5)(= (f2 c_0 c_3) c_6)(= (f2 c_0 c_3) c_7))(or (= (f2 c_0 c_4) c_0)(= (f2 c_0 c_4) c_1)(= (f2 c_0 c_4) c_2)(= (f2 c_0 c_4) c_3)(= (f2 c_0 c_4) c_4)(= (f2 c_0 c_4) c_5)(= (f2 c_0 c_4) c_6)(= (f2 c_0 c_4) c_7))(or (= (f2 c_0 c_5) c_0)(= (f2 c_0 c_5) c_1)(= (f2 c_0 c_5) c_2)(= (f2 c_0 c_5) c_3)(= (f2 c_0 c_5) c_4)(= (f2 c_0 c_5) c_5)(= (f2 c_0 c_5) c_6)(= (f2 c_0 c_5) c_7))(or (= (f2 c_0 c_6) c_0)(= (f2 c_0 c_6) c_1)(= (f2 c_0 c_6) c_2)(= (f2 c_0 c_6) c_3)(= (f2 c_0 c_6) c_4)(= (f2 c_0 c_6) c_5)(= (f2 c_0 c_6) c_6)(= (f2 c_0 c_6) c_7))(or (= (f2 c_0 c_7) c_0)(= (f2 c_0 c_7) c_1)(= (f2 c_0 c_7) c_2)(= (f2 c_0 c_7) c_3)(= (f2 c_0 c_7) c_4)(= (f2 c_0 c_7) c_5)(= (f2 c_0 c_7) c_6)(= (f2 c_0 c_7) c_7))(or (= (f2 c_1 c_0) c_0)(= (f2 c_1 c_0) c_1)(= (f2 c_1 c_0) c_2)(= (f2 c_1 c_0) c_3)(= (f2 c_1 c_0) c_4)(= (f2 c_1 c_0) c_5)(= (f2 c_1 c_0) c_6)(= (f2 c_1 c_0) c_7))(or (= (f2 c_1 c_1) c_0)(= (f2 c_1 c_1) c_1)(= (f2 c_1 c_1) c_2)(= (f2 c_1 c_1) c_3)(= (f2 c_1 c_1) c_4)(= (f2 c_1 c_1) c_5)(= (f2 c_1 c_1) c_6)(= (f2 c_1 c_1) c_7))(or (= (f2 c_1 c_2) c_0)(= (f2 c_1 c_2) c_1)(= (f2 c_1 c_2) c_2)(= (f2 c_1 c_2) c_3)(= (f2 c_1 c_2) c_4)(= (f2 c_1 c_2) c_5)(= (f2 c_1 c_2) c_6)(= (f2 c_1 c_2) c_7))(or (= (f2 c_1 c_3) c_0)(= (f2 c_1 c_3) c_1)(= (f2 c_1 c_3) c_2)(= (f2 c_1 c_3) c_3)(= (f2 c_1 c_3) c_4)(= (f2 c_1 c_3) c_5)(= (f2 c_1 c_3) c_6)(= (f2 c_1 c_3) c_7))(or (= (f2 c_1 c_4) c_0)(= (f2 c_1 c_4) c_1)(= (f2 c_1 c_4) c_2)(= (f2 c_1 c_4) c_3)(= (f2 c_1 c_4) c_4)(= (f2 c_1 c_4) c_5)(= (f2 c_1 c_4) c_6)(= (f2 c_1 c_4) c_7))(or (= (f2 c_1 c_5) c_0)(= (f2 c_1 c_5) c_1)(= (f2 c_1 c_5) c_2)(= (f2 c_1 c_5) c_3)(= (f2 c_1 c_5) c_4)(= (f2 c_1 c_5) c_5)(= (f2 c_1 c_5) c_6)(= (f2 c_1 c_5) c_7))(or (= (f2 c_1 c_6) c_0)(= (f2 c_1 c_6) c_1)(= (f2 c_1 c_6) c_2)(= (f2 c_1 c_6) c_3)(= (f2 c_1 c_6) c_4)(= (f2 c_1 c_6) c_5)(= (f2 c_1 c_6) c_6)(= (f2 c_1 c_6) c_7))(or (= (f2 c_1 c_7) c_0)(= (f2 c_1 c_7) c_1)(= (f2 c_1 c_7) c_2)(= (f2 c_1 c_7) c_3)(= (f2 c_1 c_7) c_4)(= (f2 c_1 c_7) c_5)(= (f2 c_1 c_7) c_6)(= (f2 c_1 c_7) c_7))(or (= (f2 c_2 c_0) c_0)(= (f2 c_2 c_0) c_1)(= (f2 c_2 c_0) c_2)(= (f2 c_2 c_0) c_3)(= (f2 c_2 c_0) c_4)(= (f2 c_2 c_0) c_5)(= (f2 c_2 c_0) c_6)(= (f2 c_2 c_0) c_7))(or (= (f2 c_2 c_1) c_0)(= (f2 c_2 c_1) c_1)(= (f2 c_2 c_1) c_2)(= (f2 c_2 c_1) c_3)(= (f2 c_2 c_1) c_4)(= (f2 c_2 c_1) c_5)(= (f2 c_2 c_1) c_6)(= (f2 c_2 c_1) c_7))(or (= (f2 c_2 c_2) c_0)(= (f2 c_2 c_2) c_1)(= (f2 c_2 c_2) c_2)(= (f2 c_2 c_2) c_3)(= (f2 c_2 c_2) c_4)(= (f2 c_2 c_2) c_5)(= (f2 c_2 c_2) c_6)(= (f2 c_2 c_2) c_7))(or (= (f2 c_2 c_3) c_0)(= (f2 c_2 c_3) c_1)(= (f2 c_2 c_3) c_2)(= (f2 c_2 c_3) c_3)(= (f2 c_2 c_3) c_4)(= (f2 c_2 c_3) c_5)(= (f2 c_2 c_3) c_6)(= (f2 c_2 c_3) c_7))(or (= (f2 c_2 c_4) c_0)(= (f2 c_2 c_4) c_1)(= (f2 c_2 c_4) c_2)(= (f2 c_2 c_4) c_3)(= (f2 c_2 c_4) c_4)(= (f2 c_2 c_4) c_5)(= (f2 c_2 c_4) c_6)(= (f2 c_2 c_4) c_7))(or (= (f2 c_2 c_5) c_0)(= (f2 c_2 c_5) c_1)(= (f2 c_2 c_5) c_2)(= (f2 c_2 c_5) c_3)(= (f2 c_2 c_5) c_4)(= (f2 c_2 c_5) c_5)(= (f2 c_2 c_5) c_6)(= (f2 c_2 c_5) c_7))(or (= (f2 c_2 c_6) c_0)(= (f2 c_2 c_6) c_1)(= (f2 c_2 c_6) c_2)(= (f2 c_2 c_6) c_3)(= (f2 c_2 c_6) c_4)(= (f2 c_2 c_6) c_5)(= (f2 c_2 c_6) c_6)(= (f2 c_2 c_6) c_7))(or (= (f2 c_2 c_7) c_0)(= (f2 c_2 c_7) c_1)(= (f2 c_2 c_7) c_2)(= (f2 c_2 c_7) c_3)(= (f2 c_2 c_7) c_4)(= (f2 c_2 c_7) c_5)(= (f2 c_2 c_7) c_6)(= (f2 c_2 c_7) c_7))(or (= (f2 c_3 c_0) c_0)(= (f2 c_3 c_0) c_1)(= (f2 c_3 c_0) c_2)(= (f2 c_3 c_0) c_3)(= (f2 c_3 c_0) c_4)(= (f2 c_3 c_0) c_5)(= (f2 c_3 c_0) c_6)(= (f2 c_3 c_0) c_7))(or (= (f2 c_3 c_1) c_0)(= (f2 c_3 c_1) c_1)(= (f2 c_3 c_1) c_2)(= (f2 c_3 c_1) c_3)(= (f2 c_3 c_1) c_4)(= (f2 c_3 c_1) c_5)(= (f2 c_3 c_1) c_6)(= (f2 c_3 c_1) c_7))(or (= (f2 c_3 c_2) c_0)(= (f2 c_3 c_2) c_1)(= (f2 c_3 c_2) c_2)(= (f2 c_3 c_2) c_3)(= (f2 c_3 c_2) c_4)(= (f2 c_3 c_2) c_5)(= (f2 c_3 c_2) c_6)(= (f2 c_3 c_2) c_7))(or (= (f2 c_3 c_3) c_0)(= (f2 c_3 c_3) c_1)(= (f2 c_3 c_3) c_2)(= (f2 c_3 c_3) c_3)(= (f2 c_3 c_3) c_4)(= (f2 c_3 c_3) c_5)(= (f2 c_3 c_3) c_6)(= (f2 c_3 c_3) c_7))(or (= (f2 c_3 c_4) c_0)(= (f2 c_3 c_4) c_1)(= (f2 c_3 c_4) c_2)(= (f2 c_3 c_4) c_3)(= (f2 c_3 c_4) c_4)(= (f2 c_3 c_4) c_5)(= (f2 c_3 c_4) c_6)(= (f2 c_3 c_4) c_7))(or (= (f2 c_3 c_5) c_0)(= (f2 c_3 c_5) c_1)(= (f2 c_3 c_5) c_2)(= (f2 c_3 c_5) c_3)(= (f2 c_3 c_5) c_4)(= (f2 c_3 c_5) c_5)(= (f2 c_3 c_5) c_6)(= (f2 c_3 c_5) c_7))(or (= (f2 c_3 c_6) c_0)(= (f2 c_3 c_6) c_1)(= (f2 c_3 c_6) c_2)(= (f2 c_3 c_6) c_3)(= (f2 c_3 c_6) c_4)(= (f2 c_3 c_6) c_5)(= (f2 c_3 c_6) c_6)(= (f2 c_3 c_6) c_7))(or (= (f2 c_3 c_7) c_0)(= (f2 c_3 c_7) c_1)(= (f2 c_3 c_7) c_2)(= (f2 c_3 c_7) c_3)(= (f2 c_3 c_7) c_4)(= (f2 c_3 c_7) c_5)(= (f2 c_3 c_7) c_6)(= (f2 c_3 c_7) c_7))(or (= (f2 c_4 c_0) c_0)(= (f2 c_4 c_0) c_1)(= (f2 c_4 c_0) c_2)(= (f2 c_4 c_0) c_3)(= (f2 c_4 c_0) c_4)(= (f2 c_4 c_0) c_5)(= (f2 c_4 c_0) c_6)(= (f2 c_4 c_0) c_7))(or (= (f2 c_4 c_1) c_0)(= (f2 c_4 c_1) c_1)(= (f2 c_4 c_1) c_2)(= (f2 c_4 c_1) c_3)(= (f2 c_4 c_1) c_4)(= (f2 c_4 c_1) c_5)(= (f2 c_4 c_1) c_6)(= (f2 c_4 c_1) c_7))(or (= (f2 c_4 c_2) c_0)(= (f2 c_4 c_2) c_1)(= (f2 c_4 c_2) c_2)(= (f2 c_4 c_2) c_3)(= (f2 c_4 c_2) c_4)(= (f2 c_4 c_2) c_5)(= (f2 c_4 c_2) c_6)(= (f2 c_4 c_2) c_7))(or (= (f2 c_4 c_3) c_0)(= (f2 c_4 c_3) c_1)(= (f2 c_4 c_3) c_2)(= (f2 c_4 c_3) c_3)(= (f2 c_4 c_3) c_4)(= (f2 c_4 c_3) c_5)(= (f2 c_4 c_3) c_6)(= (f2 c_4 c_3) c_7))(or (= (f2 c_4 c_4) c_0)(= (f2 c_4 c_4) c_1)(= (f2 c_4 c_4) c_2)(= (f2 c_4 c_4) c_3)(= (f2 c_4 c_4) c_4)(= (f2 c_4 c_4) c_5)(= (f2 c_4 c_4) c_6)(= (f2 c_4 c_4) c_7))(or (= (f2 c_4 c_5) c_0)(= (f2 c_4 c_5) c_1)(= (f2 c_4 c_5) c_2)(= (f2 c_4 c_5) c_3)(= (f2 c_4 c_5) c_4)(= (f2 c_4 c_5) c_5)(= (f2 c_4 c_5) c_6)(= (f2 c_4 c_5) c_7))(or (= (f2 c_4 c_6) c_0)(= (f2 c_4 c_6) c_1)(= (f2 c_4 c_6) c_2)(= (f2 c_4 c_6) c_3)(= (f2 c_4 c_6) c_4)(= (f2 c_4 c_6) c_5)(= (f2 c_4 c_6) c_6)(= (f2 c_4 c_6) c_7))(or (= (f2 c_4 c_7) c_0)(= (f2 c_4 c_7) c_1)(= (f2 c_4 c_7) c_2)(= (f2 c_4 c_7) c_3)(= (f2 c_4 c_7) c_4)(= (f2 c_4 c_7) c_5)(= (f2 c_4 c_7) c_6)(= (f2 c_4 c_7) c_7))(or (= (f2 c_5 c_0) c_0)(= (f2 c_5 c_0) c_1)(= (f2 c_5 c_0) c_2)(= (f2 c_5 c_0) c_3)(= (f2 c_5 c_0) c_4)(= (f2 c_5 c_0) c_5)(= (f2 c_5 c_0) c_6)(= (f2 c_5 c_0) c_7))(or (= (f2 c_5 c_1) c_0)(= (f2 c_5 c_1) c_1)(= (f2 c_5 c_1) c_2)(= (f2 c_5 c_1) c_3)(= (f2 c_5 c_1) c_4)(= (f2 c_5 c_1) c_5)(= (f2 c_5 c_1) c_6)(= (f2 c_5 c_1) c_7))(or (= (f2 c_5 c_2) c_0)(= (f2 c_5 c_2) c_1)(= (f2 c_5 c_2) c_2)(= (f2 c_5 c_2) c_3)(= (f2 c_5 c_2) c_4)(= (f2 c_5 c_2) c_5)(= (f2 c_5 c_2) c_6)(= (f2 c_5 c_2) c_7))(or (= (f2 c_5 c_3) c_0)(= (f2 c_5 c_3) c_1)(= (f2 c_5 c_3) c_2)(= (f2 c_5 c_3) c_3)(= (f2 c_5 c_3) c_4)(= (f2 c_5 c_3) c_5)(= (f2 c_5 c_3) c_6)(= (f2 c_5 c_3) c_7))(or (= (f2 c_5 c_4) c_0)(= (f2 c_5 c_4) c_1)(= (f2 c_5 c_4) c_2)(= (f2 c_5 c_4) c_3)(= (f2 c_5 c_4) c_4)(= (f2 c_5 c_4) c_5)(= (f2 c_5 c_4) c_6)(= (f2 c_5 c_4) c_7))(or (= (f2 c_5 c_5) c_0)(= (f2 c_5 c_5) c_1)(= (f2 c_5 c_5) c_2)(= (f2 c_5 c_5) c_3)(= (f2 c_5 c_5) c_4)(= (f2 c_5 c_5) c_5)(= (f2 c_5 c_5) c_6)(= (f2 c_5 c_5) c_7))(or (= (f2 c_5 c_6) c_0)(= (f2 c_5 c_6) c_1)(= (f2 c_5 c_6) c_2)(= (f2 c_5 c_6) c_3)(= (f2 c_5 c_6) c_4)(= (f2 c_5 c_6) c_5)(= (f2 c_5 c_6) c_6)(= (f2 c_5 c_6) c_7))(or (= (f2 c_5 c_7) c_0)(= (f2 c_5 c_7) c_1)(= (f2 c_5 c_7) c_2)(= (f2 c_5 c_7) c_3)(= (f2 c_5 c_7) c_4)(= (f2 c_5 c_7) c_5)(= (f2 c_5 c_7) c_6)(= (f2 c_5 c_7) c_7))(or (= (f2 c_6 c_0) c_0)(= (f2 c_6 c_0) c_1)(= (f2 c_6 c_0) c_2)(= (f2 c_6 c_0) c_3)(= (f2 c_6 c_0) c_4)(= (f2 c_6 c_0) c_5)(= (f2 c_6 c_0) c_6)(= (f2 c_6 c_0) c_7))(or (= (f2 c_6 c_1) c_0)(= (f2 c_6 c_1) c_1)(= (f2 c_6 c_1) c_2)(= (f2 c_6 c_1) c_3)(= (f2 c_6 c_1) c_4)(= (f2 c_6 c_1) c_5)(= (f2 c_6 c_1) c_6)(= (f2 c_6 c_1) c_7))(or (= (f2 c_6 c_2) c_0)(= (f2 c_6 c_2) c_1)(= (f2 c_6 c_2) c_2)(= (f2 c_6 c_2) c_3)(= (f2 c_6 c_2) c_4)(= (f2 c_6 c_2) c_5)(= (f2 c_6 c_2) c_6)(= (f2 c_6 c_2) c_7))(or (= (f2 c_6 c_3) c_0)(= (f2 c_6 c_3) c_1)(= (f2 c_6 c_3) c_2)(= (f2 c_6 c_3) c_3)(= (f2 c_6 c_3) c_4)(= (f2 c_6 c_3) c_5)(= (f2 c_6 c_3) c_6)(= (f2 c_6 c_3) c_7))(or (= (f2 c_6 c_4) c_0)(= (f2 c_6 c_4) c_1)(= (f2 c_6 c_4) c_2)(= (f2 c_6 c_4) c_3)(= (f2 c_6 c_4) c_4)(= (f2 c_6 c_4) c_5)(= (f2 c_6 c_4) c_6)(= (f2 c_6 c_4) c_7))(or (= (f2 c_6 c_5) c_0)(= (f2 c_6 c_5) c_1)(= (f2 c_6 c_5) c_2)(= (f2 c_6 c_5) c_3)(= (f2 c_6 c_5) c_4)(= (f2 c_6 c_5) c_5)(= (f2 c_6 c_5) c_6)(= (f2 c_6 c_5) c_7))(or (= (f2 c_6 c_6) c_0)(= (f2 c_6 c_6) c_1)(= (f2 c_6 c_6) c_2)(= (f2 c_6 c_6) c_3)(= (f2 c_6 c_6) c_4)(= (f2 c_6 c_6) c_5)(= (f2 c_6 c_6) c_6)(= (f2 c_6 c_6) c_7))(or (= (f2 c_6 c_7) c_0)(= (f2 c_6 c_7) c_1)(= (f2 c_6 c_7) c_2)(= (f2 c_6 c_7) c_3)(= (f2 c_6 c_7) c_4)(= (f2 c_6 c_7) c_5)(= (f2 c_6 c_7) c_6)(= (f2 c_6 c_7) c_7))(or (= (f2 c_7 c_0) c_0)(= (f2 c_7 c_0) c_1)(= (f2 c_7 c_0) c_2)(= (f2 c_7 c_0) c_3)(= (f2 c_7 c_0) c_4)(= (f2 c_7 c_0) c_5)(= (f2 c_7 c_0) c_6)(= (f2 c_7 c_0) c_7))(or (= (f2 c_7 c_1) c_0)(= (f2 c_7 c_1) c_1)(= (f2 c_7 c_1) c_2)(= (f2 c_7 c_1) c_3)(= (f2 c_7 c_1) c_4)(= (f2 c_7 c_1) c_5)(= (f2 c_7 c_1) c_6)(= (f2 c_7 c_1) c_7))(or (= (f2 c_7 c_2) c_0)(= (f2 c_7 c_2) c_1)(= (f2 c_7 c_2) c_2)(= (f2 c_7 c_2) c_3)(= (f2 c_7 c_2) c_4)(= (f2 c_7 c_2) c_5)(= (f2 c_7 c_2) c_6)(= (f2 c_7 c_2) c_7))(or (= (f2 c_7 c_3) c_0)(= (f2 c_7 c_3) c_1)(= (f2 c_7 c_3) c_2)(= (f2 c_7 c_3) c_3)(= (f2 c_7 c_3) c_4)(= (f2 c_7 c_3) c_5)(= (f2 c_7 c_3) c_6)(= (f2 c_7 c_3) c_7))(or (= (f2 c_7 c_4) c_0)(= (f2 c_7 c_4) c_1)(= (f2 c_7 c_4) c_2)(= (f2 c_7 c_4) c_3)(= (f2 c_7 c_4) c_4)(= (f2 c_7 c_4) c_5)(= (f2 c_7 c_4) c_6)(= (f2 c_7 c_4) c_7))(or (= (f2 c_7 c_5) c_0)(= (f2 c_7 c_5) c_1)(= (f2 c_7 c_5) c_2)(= (f2 c_7 c_5) c_3)(= (f2 c_7 c_5) c_4)(= (f2 c_7 c_5) c_5)(= (f2 c_7 c_5) c_6)(= (f2 c_7 c_5) c_7))(or (= (f2 c_7 c_6) c_0)(= (f2 c_7 c_6) c_1)(= (f2 c_7 c_6) c_2)(= (f2 c_7 c_6) c_3)(= (f2 c_7 c_6) c_4)(= (f2 c_7 c_6) c_5)(= (f2 c_7 c_6) c_6)(= (f2 c_7 c_6) c_7))(or (= (f2 c_7 c_7) c_0)(= (f2 c_7 c_7) c_1)(= (f2 c_7 c_7) c_2)(= (f2 c_7 c_7) c_3)(= (f2 c_7 c_7) c_4)(= (f2 c_7 c_7) c_5)(= (f2 c_7 c_7) c_6)(= (f2 c_7 c_7) c_7))(or (= (f3 c_0) c_0)(= (f3 c_0) c_1)(= (f3 c_0) c_2)(= (f3 c_0) c_3)(= (f3 c_0) c_4)(= (f3 c_0) c_5)(= (f3 c_0) c_6)(= (f3 c_0) c_7))(or (= (f3 c_1) c_0)(= (f3 c_1) c_1)(= (f3 c_1) c_2)(= (f3 c_1) c_3)(= (f3 c_1) c_4)(= (f3 c_1) c_5)(= (f3 c_1) c_6)(= (f3 c_1) c_7))(or (= (f3 c_2) c_0)(= (f3 c_2) c_1)(= (f3 c_2) c_2)(= (f3 c_2) c_3)(= (f3 c_2) c_4)(= (f3 c_2) c_5)(= (f3 c_2) c_6)(= (f3 c_2) c_7))(or (= (f3 c_3) c_0)(= (f3 c_3) c_1)(= (f3 c_3) c_2)(= (f3 c_3) c_3)(= (f3 c_3) c_4)(= (f3 c_3) c_5)(= (f3 c_3) c_6)(= (f3 c_3) c_7))(or (= (f3 c_4) c_0)(= (f3 c_4) c_1)(= (f3 c_4) c_2)(= (f3 c_4) c_3)(= (f3 c_4) c_4)(= (f3 c_4) c_5)(= (f3 c_4) c_6)(= (f3 c_4) c_7))(or (= (f3 c_5) c_0)(= (f3 c_5) c_1)(= (f3 c_5) c_2)(= (f3 c_5) c_3)(= (f3 c_5) c_4)(= (f3 c_5) c_5)(= (f3 c_5) c_6)(= (f3 c_5) c_7))(or (= (f3 c_6) c_0)(= (f3 c_6) c_1)(= (f3 c_6) c_2)(= (f3 c_6) c_3)(= (f3 c_6) c_4)(= (f3 c_6) c_5)(= (f3 c_6) c_6)(= (f3 c_6) c_7))(or (= (f3 c_7) c_0)(= (f3 c_7) c_1)(= (f3 c_7) c_2)(= (f3 c_7) c_3)(= (f3 c_7) c_4)(= (f3 c_7) c_5)(= (f3 c_7) c_6)(= (f3 c_7) c_7))(or (= c6 c_0)(= c6 c_1)(= c6 c_2)(= c6 c_3)(= c6 c_4)(= c6 c_5)(= c6 c_6)(= c6 c_7))(or (= c7 c_0)(= c7 c_1)(= c7 c_2)(= c7 c_3)(= c7 c_4)(= c7 c_5)(= c7 c_6)(= c7 c_7))(or (= c4 c_0)(= c4 c_1)(= c4 c_2)(= c4 c_3)(= c4 c_4)(= c4 c_5)(= c4 c_6)(= c4 c_7))(or (= c5 c_0)(= c5 c_1)(= c5 c_2)(= c5 c_3)(= c5 c_4)(= c5 c_5)(= c5 c_6)(= c5 c_7))))