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

This benchmark was obtained by trying to find a finite model of a first-order 
formula (Albert Oliveras).
}
:status unknown
:logic QF_UF
:extrafuns ((c2 U))
:extrafuns ((f3 U U U))
:extrafuns ((f1 U U U))
:extrafuns ((f4 U U))
:extrafuns ((f5 U U U U))
:extrafuns ((c6 U))
:extrafuns ((c7 U))
:extrafuns ((c8 U))
:extrafuns ((c_0 U))
:extrafuns ((c_1 U))
:extrafuns ((c_2 U))
:extrafuns ((c_3 U))
:formula 
( and 
( distinct c_0 c_1 c_2 c_3 )(= (f3 c_0 c2) c2) (= (f3 c_1 c2) c2) (= (f3 c_2 c2) c2) (= (f3 c_3 c2) c2) (= (f3 c_0 (f3 c_0 (f3 c_0 c_0))) (f3 (f3 (f3 c_0 c_0) c_0) c_0)) (= (f3 c_0 (f3 c_0 (f3 c_1 c_0))) (f3 (f3 (f3 c_0 c_0) c_1) c_0)) (= (f3 c_0 (f3 c_0 (f3 c_2 c_0))) (f3 (f3 (f3 c_0 c_0) c_2) c_0)) (= (f3 c_0 (f3 c_0 (f3 c_3 c_0))) (f3 (f3 (f3 c_0 c_0) c_3) c_0)) (= (f3 c_0 (f3 c_1 (f3 c_0 c_1))) (f3 (f3 (f3 c_0 c_1) c_0) c_1)) (= (f3 c_0 (f3 c_1 (f3 c_1 c_1))) (f3 (f3 (f3 c_0 c_1) c_1) c_1)) (= (f3 c_0 (f3 c_1 (f3 c_2 c_1))) (f3 (f3 (f3 c_0 c_1) c_2) c_1)) (= (f3 c_0 (f3 c_1 (f3 c_3 c_1))) (f3 (f3 (f3 c_0 c_1) c_3) c_1)) (= (f3 c_0 (f3 c_2 (f3 c_0 c_2))) (f3 (f3 (f3 c_0 c_2) c_0) c_2)) (= (f3 c_0 (f3 c_2 (f3 c_1 c_2))) (f3 (f3 (f3 c_0 c_2) c_1) c_2)) (= (f3 c_0 (f3 c_2 (f3 c_2 c_2))) (f3 (f3 (f3 c_0 c_2) c_2) c_2)) (= (f3 c_0 (f3 c_2 (f3 c_3 c_2))) (f3 (f3 (f3 c_0 c_2) c_3) c_2)) (= (f3 c_0 (f3 c_3 (f3 c_0 c_3))) (f3 (f3 (f3 c_0 c_3) c_0) c_3)) (= (f3 c_0 (f3 c_3 (f3 c_1 c_3))) (f3 (f3 (f3 c_0 c_3) c_1) c_3)) (= (f3 c_0 (f3 c_3 (f3 c_2 c_3))) (f3 (f3 (f3 c_0 c_3) c_2) c_3)) (= (f3 c_0 (f3 c_3 (f3 c_3 c_3))) (f3 (f3 (f3 c_0 c_3) c_3) c_3)) (= (f3 c_1 (f3 c_0 (f3 c_0 c_0))) (f3 (f3 (f3 c_1 c_0) c_0) c_0)) (= (f3 c_1 (f3 c_0 (f3 c_1 c_0))) (f3 (f3 (f3 c_1 c_0) c_1) c_0)) (= (f3 c_1 (f3 c_0 (f3 c_2 c_0))) (f3 (f3 (f3 c_1 c_0) c_2) c_0)) (= (f3 c_1 (f3 c_0 (f3 c_3 c_0))) (f3 (f3 (f3 c_1 c_0) c_3) c_0)) (= (f3 c_1 (f3 c_1 (f3 c_0 c_1))) (f3 (f3 (f3 c_1 c_1) c_0) c_1)) (= (f3 c_1 (f3 c_1 (f3 c_1 c_1))) (f3 (f3 (f3 c_1 c_1) c_1) c_1)) (= (f3 c_1 (f3 c_1 (f3 c_2 c_1))) (f3 (f3 (f3 c_1 c_1) c_2) c_1)) (= (f3 c_1 (f3 c_1 (f3 c_3 c_1))) (f3 (f3 (f3 c_1 c_1) c_3) c_1)) (= (f3 c_1 (f3 c_2 (f3 c_0 c_2))) (f3 (f3 (f3 c_1 c_2) c_0) c_2)) (= (f3 c_1 (f3 c_2 (f3 c_1 c_2))) (f3 (f3 (f3 c_1 c_2) c_1) c_2)) (= (f3 c_1 (f3 c_2 (f3 c_2 c_2))) (f3 (f3 (f3 c_1 c_2) c_2) c_2)) (= (f3 c_1 (f3 c_2 (f3 c_3 c_2))) (f3 (f3 (f3 c_1 c_2) c_3) c_2)) (= (f3 c_1 (f3 c_3 (f3 c_0 c_3))) (f3 (f3 (f3 c_1 c_3) c_0) c_3)) (= (f3 c_1 (f3 c_3 (f3 c_1 c_3))) (f3 (f3 (f3 c_1 c_3) c_1) c_3)) (= (f3 c_1 (f3 c_3 (f3 c_2 c_3))) (f3 (f3 (f3 c_1 c_3) c_2) c_3)) (= (f3 c_1 (f3 c_3 (f3 c_3 c_3))) (f3 (f3 (f3 c_1 c_3) c_3) c_3)) (= (f3 c_2 (f3 c_0 (f3 c_0 c_0))) (f3 (f3 (f3 c_2 c_0) c_0) c_0)) (= (f3 c_2 (f3 c_0 (f3 c_1 c_0))) (f3 (f3 (f3 c_2 c_0) c_1) c_0)) (= (f3 c_2 (f3 c_0 (f3 c_2 c_0))) (f3 (f3 (f3 c_2 c_0) c_2) c_0)) (= (f3 c_2 (f3 c_0 (f3 c_3 c_0))) (f3 (f3 (f3 c_2 c_0) c_3) c_0)) (= (f3 c_2 (f3 c_1 (f3 c_0 c_1))) (f3 (f3 (f3 c_2 c_1) c_0) c_1)) (= (f3 c_2 (f3 c_1 (f3 c_1 c_1))) (f3 (f3 (f3 c_2 c_1) c_1) c_1)) (= (f3 c_2 (f3 c_1 (f3 c_2 c_1))) (f3 (f3 (f3 c_2 c_1) c_2) c_1)) (= (f3 c_2 (f3 c_1 (f3 c_3 c_1))) (f3 (f3 (f3 c_2 c_1) c_3) c_1)) (= (f3 c_2 (f3 c_2 (f3 c_0 c_2))) (f3 (f3 (f3 c_2 c_2) c_0) c_2)) (= (f3 c_2 (f3 c_2 (f3 c_1 c_2))) (f3 (f3 (f3 c_2 c_2) c_1) c_2)) (= (f3 c_2 (f3 c_2 (f3 c_2 c_2))) (f3 (f3 (f3 c_2 c_2) c_2) c_2)) (= (f3 c_2 (f3 c_2 (f3 c_3 c_2))) (f3 (f3 (f3 c_2 c_2) c_3) c_2)) (= (f3 c_2 (f3 c_3 (f3 c_0 c_3))) (f3 (f3 (f3 c_2 c_3) c_0) c_3)) (= (f3 c_2 (f3 c_3 (f3 c_1 c_3))) (f3 (f3 (f3 c_2 c_3) c_1) c_3)) (= (f3 c_2 (f3 c_3 (f3 c_2 c_3))) (f3 (f3 (f3 c_2 c_3) c_2) c_3)) (= (f3 c_2 (f3 c_3 (f3 c_3 c_3))) (f3 (f3 (f3 c_2 c_3) c_3) c_3)) (= (f3 c_3 (f3 c_0 (f3 c_0 c_0))) (f3 (f3 (f3 c_3 c_0) c_0) c_0)) (= (f3 c_3 (f3 c_0 (f3 c_1 c_0))) (f3 (f3 (f3 c_3 c_0) c_1) c_0)) (= (f3 c_3 (f3 c_0 (f3 c_2 c_0))) (f3 (f3 (f3 c_3 c_0) c_2) c_0)) (= (f3 c_3 (f3 c_0 (f3 c_3 c_0))) (f3 (f3 (f3 c_3 c_0) c_3) c_0)) (= (f3 c_3 (f3 c_1 (f3 c_0 c_1))) (f3 (f3 (f3 c_3 c_1) c_0) c_1)) (= (f3 c_3 (f3 c_1 (f3 c_1 c_1))) (f3 (f3 (f3 c_3 c_1) c_1) c_1)) (= (f3 c_3 (f3 c_1 (f3 c_2 c_1))) (f3 (f3 (f3 c_3 c_1) c_2) c_1)) (= (f3 c_3 (f3 c_1 (f3 c_3 c_1))) (f3 (f3 (f3 c_3 c_1) c_3) c_1)) (= (f3 c_3 (f3 c_2 (f3 c_0 c_2))) (f3 (f3 (f3 c_3 c_2) c_0) c_2)) (= (f3 c_3 (f3 c_2 (f3 c_1 c_2))) (f3 (f3 (f3 c_3 c_2) c_1) c_2)) (= (f3 c_3 (f3 c_2 (f3 c_2 c_2))) (f3 (f3 (f3 c_3 c_2) c_2) c_2)) (= (f3 c_3 (f3 c_2 (f3 c_3 c_2))) (f3 (f3 (f3 c_3 c_2) c_3) c_2)) (= (f3 c_3 (f3 c_3 (f3 c_0 c_3))) (f3 (f3 (f3 c_3 c_3) c_0) c_3)) (= (f3 c_3 (f3 c_3 (f3 c_1 c_3))) (f3 (f3 (f3 c_3 c_3) c_1) c_3)) (= (f3 c_3 (f3 c_3 (f3 c_2 c_3))) (f3 (f3 (f3 c_3 c_3) c_2) c_3)) (= (f3 c_3 (f3 c_3 (f3 c_3 c_3))) (f3 (f3 (f3 c_3 c_3) c_3) c_3)) (= (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_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_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_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)) (or (not (= (f1 c_0 c_0) (f1 c_0 c_0))) (= c_0 c_0) )(or (not (= (f1 c_0 c_0) (f1 c_0 c_1))) (= c_0 c_1) )(or (not (= (f1 c_0 c_0) (f1 c_0 c_2))) (= c_0 c_2) )(or (not (= (f1 c_0 c_0) (f1 c_0 c_3))) (= c_0 c_3) )(or (not (= (f1 c_0 c_1) (f1 c_0 c_0))) (= c_1 c_0) )(or (not (= (f1 c_0 c_1) (f1 c_0 c_1))) (= c_1 c_1) )(or (not (= (f1 c_0 c_1) (f1 c_0 c_2))) (= c_1 c_2) )(or (not (= (f1 c_0 c_1) (f1 c_0 c_3))) (= c_1 c_3) )(or (not (= (f1 c_0 c_2) (f1 c_0 c_0))) (= c_2 c_0) )(or (not (= (f1 c_0 c_2) (f1 c_0 c_1))) (= c_2 c_1) )(or (not (= (f1 c_0 c_2) (f1 c_0 c_2))) (= c_2 c_2) )(or (not (= (f1 c_0 c_2) (f1 c_0 c_3))) (= c_2 c_3) )(or (not (= (f1 c_0 c_3) (f1 c_0 c_0))) (= c_3 c_0) )(or (not (= (f1 c_0 c_3) (f1 c_0 c_1))) (= c_3 c_1) )(or (not (= (f1 c_0 c_3) (f1 c_0 c_2))) (= c_3 c_2) )(or (not (= (f1 c_0 c_3) (f1 c_0 c_3))) (= c_3 c_3) )(or (not (= (f1 c_1 c_0) (f1 c_1 c_0))) (= c_0 c_0) )(or (not (= (f1 c_1 c_0) (f1 c_1 c_1))) (= c_0 c_1) )(or (not (= (f1 c_1 c_0) (f1 c_1 c_2))) (= c_0 c_2) )(or (not (= (f1 c_1 c_0) (f1 c_1 c_3))) (= c_0 c_3) )(or (not (= (f1 c_1 c_1) (f1 c_1 c_0))) (= c_1 c_0) )(or (not (= (f1 c_1 c_1) (f1 c_1 c_1))) (= c_1 c_1) )(or (not (= (f1 c_1 c_1) (f1 c_1 c_2))) (= c_1 c_2) )(or (not (= (f1 c_1 c_1) (f1 c_1 c_3))) (= c_1 c_3) )(or (not (= (f1 c_1 c_2) (f1 c_1 c_0))) (= c_2 c_0) )(or (not (= (f1 c_1 c_2) (f1 c_1 c_1))) (= c_2 c_1) )(or (not (= (f1 c_1 c_2) (f1 c_1 c_2))) (= c_2 c_2) )(or (not (= (f1 c_1 c_2) (f1 c_1 c_3))) (= c_2 c_3) )(or (not (= (f1 c_1 c_3) (f1 c_1 c_0))) (= c_3 c_0) )(or (not (= (f1 c_1 c_3) (f1 c_1 c_1))) (= c_3 c_1) )(or (not (= (f1 c_1 c_3) (f1 c_1 c_2))) (= c_3 c_2) )(or (not (= (f1 c_1 c_3) (f1 c_1 c_3))) (= c_3 c_3) )(or (not (= (f1 c_2 c_0) (f1 c_2 c_0))) (= c_0 c_0) )(or (not (= (f1 c_2 c_0) (f1 c_2 c_1))) (= c_0 c_1) )(or (not (= (f1 c_2 c_0) (f1 c_2 c_2))) (= c_0 c_2) )(or (not (= (f1 c_2 c_0) (f1 c_2 c_3))) (= c_0 c_3) )(or (not (= (f1 c_2 c_1) (f1 c_2 c_0))) (= c_1 c_0) )(or (not (= (f1 c_2 c_1) (f1 c_2 c_1))) (= c_1 c_1) )(or (not (= (f1 c_2 c_1) (f1 c_2 c_2))) (= c_1 c_2) )(or (not (= (f1 c_2 c_1) (f1 c_2 c_3))) (= c_1 c_3) )(or (not (= (f1 c_2 c_2) (f1 c_2 c_0))) (= c_2 c_0) )(or (not (= (f1 c_2 c_2) (f1 c_2 c_1))) (= c_2 c_1) )(or (not (= (f1 c_2 c_2) (f1 c_2 c_2))) (= c_2 c_2) )(or (not (= (f1 c_2 c_2) (f1 c_2 c_3))) (= c_2 c_3) )(or (not (= (f1 c_2 c_3) (f1 c_2 c_0))) (= c_3 c_0) )(or (not (= (f1 c_2 c_3) (f1 c_2 c_1))) (= c_3 c_1) )(or (not (= (f1 c_2 c_3) (f1 c_2 c_2))) (= c_3 c_2) )(or (not (= (f1 c_2 c_3) (f1 c_2 c_3))) (= c_3 c_3) )(or (not (= (f1 c_3 c_0) (f1 c_3 c_0))) (= c_0 c_0) )(or (not (= (f1 c_3 c_0) (f1 c_3 c_1))) (= c_0 c_1) )(or (not (= (f1 c_3 c_0) (f1 c_3 c_2))) (= c_0 c_2) )(or (not (= (f1 c_3 c_0) (f1 c_3 c_3))) (= c_0 c_3) )(or (not (= (f1 c_3 c_1) (f1 c_3 c_0))) (= c_1 c_0) )(or (not (= (f1 c_3 c_1) (f1 c_3 c_1))) (= c_1 c_1) )(or (not (= (f1 c_3 c_1) (f1 c_3 c_2))) (= c_1 c_2) )(or (not (= (f1 c_3 c_1) (f1 c_3 c_3))) (= c_1 c_3) )(or (not (= (f1 c_3 c_2) (f1 c_3 c_0))) (= c_2 c_0) )(or (not (= (f1 c_3 c_2) (f1 c_3 c_1))) (= c_2 c_1) )(or (not (= (f1 c_3 c_2) (f1 c_3 c_2))) (= c_2 c_2) )(or (not (= (f1 c_3 c_2) (f1 c_3 c_3))) (= c_2 c_3) )(or (not (= (f1 c_3 c_3) (f1 c_3 c_0))) (= c_3 c_0) )(or (not (= (f1 c_3 c_3) (f1 c_3 c_1))) (= c_3 c_1) )(or (not (= (f1 c_3 c_3) (f1 c_3 c_2))) (= c_3 c_2) )(or (not (= (f1 c_3 c_3) (f1 c_3 c_3))) (= c_3 c_3) )(= (f3 (f1 c_0 c_0) c_0) (f1 (f3 c_0 c_0) (f3 c_0 c_0))) (= (f3 (f1 c_0 c_0) c_1) (f1 (f3 c_0 c_1) (f3 c_0 c_1))) (= (f3 (f1 c_0 c_0) c_2) (f1 (f3 c_0 c_2) (f3 c_0 c_2))) (= (f3 (f1 c_0 c_0) c_3) (f1 (f3 c_0 c_3) (f3 c_0 c_3))) (= (f3 (f1 c_0 c_1) c_0) (f1 (f3 c_0 c_0) (f3 c_1 c_0))) (= (f3 (f1 c_0 c_1) c_1) (f1 (f3 c_0 c_1) (f3 c_1 c_1))) (= (f3 (f1 c_0 c_1) c_2) (f1 (f3 c_0 c_2) (f3 c_1 c_2))) (= (f3 (f1 c_0 c_1) c_3) (f1 (f3 c_0 c_3) (f3 c_1 c_3))) (= (f3 (f1 c_0 c_2) c_0) (f1 (f3 c_0 c_0) (f3 c_2 c_0))) (= (f3 (f1 c_0 c_2) c_1) (f1 (f3 c_0 c_1) (f3 c_2 c_1))) (= (f3 (f1 c_0 c_2) c_2) (f1 (f3 c_0 c_2) (f3 c_2 c_2))) (= (f3 (f1 c_0 c_2) c_3) (f1 (f3 c_0 c_3) (f3 c_2 c_3))) (= (f3 (f1 c_0 c_3) c_0) (f1 (f3 c_0 c_0) (f3 c_3 c_0))) (= (f3 (f1 c_0 c_3) c_1) (f1 (f3 c_0 c_1) (f3 c_3 c_1))) (= (f3 (f1 c_0 c_3) c_2) (f1 (f3 c_0 c_2) (f3 c_3 c_2))) (= (f3 (f1 c_0 c_3) c_3) (f1 (f3 c_0 c_3) (f3 c_3 c_3))) (= (f3 (f1 c_1 c_0) c_0) (f1 (f3 c_1 c_0) (f3 c_0 c_0))) (= (f3 (f1 c_1 c_0) c_1) (f1 (f3 c_1 c_1) (f3 c_0 c_1))) (= (f3 (f1 c_1 c_0) c_2) (f1 (f3 c_1 c_2) (f3 c_0 c_2))) (= (f3 (f1 c_1 c_0) c_3) (f1 (f3 c_1 c_3) (f3 c_0 c_3))) (= (f3 (f1 c_1 c_1) c_0) (f1 (f3 c_1 c_0) (f3 c_1 c_0))) (= (f3 (f1 c_1 c_1) c_1) (f1 (f3 c_1 c_1) (f3 c_1 c_1))) (= (f3 (f1 c_1 c_1) c_2) (f1 (f3 c_1 c_2) (f3 c_1 c_2))) (= (f3 (f1 c_1 c_1) c_3) (f1 (f3 c_1 c_3) (f3 c_1 c_3))) (= (f3 (f1 c_1 c_2) c_0) (f1 (f3 c_1 c_0) (f3 c_2 c_0))) (= (f3 (f1 c_1 c_2) c_1) (f1 (f3 c_1 c_1) (f3 c_2 c_1))) (= (f3 (f1 c_1 c_2) c_2) (f1 (f3 c_1 c_2) (f3 c_2 c_2))) (= (f3 (f1 c_1 c_2) c_3) (f1 (f3 c_1 c_3) (f3 c_2 c_3))) (= (f3 (f1 c_1 c_3) c_0) (f1 (f3 c_1 c_0) (f3 c_3 c_0))) (= (f3 (f1 c_1 c_3) c_1) (f1 (f3 c_1 c_1) (f3 c_3 c_1))) (= (f3 (f1 c_1 c_3) c_2) (f1 (f3 c_1 c_2) (f3 c_3 c_2))) (= (f3 (f1 c_1 c_3) c_3) (f1 (f3 c_1 c_3) (f3 c_3 c_3))) (= (f3 (f1 c_2 c_0) c_0) (f1 (f3 c_2 c_0) (f3 c_0 c_0))) (= (f3 (f1 c_2 c_0) c_1) (f1 (f3 c_2 c_1) (f3 c_0 c_1))) (= (f3 (f1 c_2 c_0) c_2) (f1 (f3 c_2 c_2) (f3 c_0 c_2))) (= (f3 (f1 c_2 c_0) c_3) (f1 (f3 c_2 c_3) (f3 c_0 c_3))) (= (f3 (f1 c_2 c_1) c_0) (f1 (f3 c_2 c_0) (f3 c_1 c_0))) (= (f3 (f1 c_2 c_1) c_1) (f1 (f3 c_2 c_1) (f3 c_1 c_1))) (= (f3 (f1 c_2 c_1) c_2) (f1 (f3 c_2 c_2) (f3 c_1 c_2))) (= (f3 (f1 c_2 c_1) c_3) (f1 (f3 c_2 c_3) (f3 c_1 c_3))) (= (f3 (f1 c_2 c_2) c_0) (f1 (f3 c_2 c_0) (f3 c_2 c_0))) (= (f3 (f1 c_2 c_2) c_1) (f1 (f3 c_2 c_1) (f3 c_2 c_1))) (= (f3 (f1 c_2 c_2) c_2) (f1 (f3 c_2 c_2) (f3 c_2 c_2))) (= (f3 (f1 c_2 c_2) c_3) (f1 (f3 c_2 c_3) (f3 c_2 c_3))) (= (f3 (f1 c_2 c_3) c_0) (f1 (f3 c_2 c_0) (f3 c_3 c_0))) (= (f3 (f1 c_2 c_3) c_1) (f1 (f3 c_2 c_1) (f3 c_3 c_1))) (= (f3 (f1 c_2 c_3) c_2) (f1 (f3 c_2 c_2) (f3 c_3 c_2))) (= (f3 (f1 c_2 c_3) c_3) (f1 (f3 c_2 c_3) (f3 c_3 c_3))) (= (f3 (f1 c_3 c_0) c_0) (f1 (f3 c_3 c_0) (f3 c_0 c_0))) (= (f3 (f1 c_3 c_0) c_1) (f1 (f3 c_3 c_1) (f3 c_0 c_1))) (= (f3 (f1 c_3 c_0) c_2) (f1 (f3 c_3 c_2) (f3 c_0 c_2))) (= (f3 (f1 c_3 c_0) c_3) (f1 (f3 c_3 c_3) (f3 c_0 c_3))) (= (f3 (f1 c_3 c_1) c_0) (f1 (f3 c_3 c_0) (f3 c_1 c_0))) (= (f3 (f1 c_3 c_1) c_1) (f1 (f3 c_3 c_1) (f3 c_1 c_1))) (= (f3 (f1 c_3 c_1) c_2) (f1 (f3 c_3 c_2) (f3 c_1 c_2))) (= (f3 (f1 c_3 c_1) c_3) (f1 (f3 c_3 c_3) (f3 c_1 c_3))) (= (f3 (f1 c_3 c_2) c_0) (f1 (f3 c_3 c_0) (f3 c_2 c_0))) (= (f3 (f1 c_3 c_2) c_1) (f1 (f3 c_3 c_1) (f3 c_2 c_1))) (= (f3 (f1 c_3 c_2) c_2) (f1 (f3 c_3 c_2) (f3 c_2 c_2))) (= (f3 (f1 c_3 c_2) c_3) (f1 (f3 c_3 c_3) (f3 c_2 c_3))) (= (f3 (f1 c_3 c_3) c_0) (f1 (f3 c_3 c_0) (f3 c_3 c_0))) (= (f3 (f1 c_3 c_3) c_1) (f1 (f3 c_3 c_1) (f3 c_3 c_1))) (= (f3 (f1 c_3 c_3) c_2) (f1 (f3 c_3 c_2) (f3 c_3 c_2))) (= (f3 (f1 c_3 c_3) c_3) (f1 (f3 c_3 c_3) (f3 c_3 c_3))) (= (f3 (f3 c_0 c_0) c_0) (f3 c_0 (f3 c_0 c_0))) (= (f3 (f3 c_0 c_1) c_0) (f3 c_0 (f3 c_1 c_0))) (= (f3 (f3 c_0 c_2) c_0) (f3 c_0 (f3 c_2 c_0))) (= (f3 (f3 c_0 c_3) c_0) (f3 c_0 (f3 c_3 c_0))) (= (f3 (f3 c_1 c_0) c_1) (f3 c_1 (f3 c_0 c_1))) (= (f3 (f3 c_1 c_1) c_1) (f3 c_1 (f3 c_1 c_1))) (= (f3 (f3 c_1 c_2) c_1) (f3 c_1 (f3 c_2 c_1))) (= (f3 (f3 c_1 c_3) c_1) (f3 c_1 (f3 c_3 c_1))) (= (f3 (f3 c_2 c_0) c_2) (f3 c_2 (f3 c_0 c_2))) (= (f3 (f3 c_2 c_1) c_2) (f3 c_2 (f3 c_1 c_2))) (= (f3 (f3 c_2 c_2) c_2) (f3 c_2 (f3 c_2 c_2))) (= (f3 (f3 c_2 c_3) c_2) (f3 c_2 (f3 c_3 c_2))) (= (f3 (f3 c_3 c_0) c_3) (f3 c_3 (f3 c_0 c_3))) (= (f3 (f3 c_3 c_1) c_3) (f3 c_3 (f3 c_1 c_3))) (= (f3 (f3 c_3 c_2) c_3) (f3 c_3 (f3 c_2 c_3))) (= (f3 (f3 c_3 c_3) c_3) (f3 c_3 (f3 c_3 c_3))) (= (f4 (f4 c_0)) c_0) (= (f4 (f4 c_1)) c_1) (= (f4 (f4 c_2)) c_2) (= (f4 (f4 c_3)) c_3) (= (f5 c_0 c_0 c_0) (f4 (f5 c_0 c_0 c_0))) (= (f5 c_0 c_0 c_1) (f4 (f5 c_0 c_0 c_1))) (= (f5 c_0 c_0 c_2) (f4 (f5 c_0 c_0 c_2))) (= (f5 c_0 c_0 c_3) (f4 (f5 c_0 c_0 c_3))) (= (f5 c_0 c_1 c_0) (f4 (f5 c_1 c_0 c_0))) (= (f5 c_0 c_1 c_1) (f4 (f5 c_1 c_0 c_1))) (= (f5 c_0 c_1 c_2) (f4 (f5 c_1 c_0 c_2))) (= (f5 c_0 c_1 c_3) (f4 (f5 c_1 c_0 c_3))) (= (f5 c_0 c_2 c_0) (f4 (f5 c_2 c_0 c_0))) (= (f5 c_0 c_2 c_1) (f4 (f5 c_2 c_0 c_1))) (= (f5 c_0 c_2 c_2) (f4 (f5 c_2 c_0 c_2))) (= (f5 c_0 c_2 c_3) (f4 (f5 c_2 c_0 c_3))) (= (f5 c_0 c_3 c_0) (f4 (f5 c_3 c_0 c_0))) (= (f5 c_0 c_3 c_1) (f4 (f5 c_3 c_0 c_1))) (= (f5 c_0 c_3 c_2) (f4 (f5 c_3 c_0 c_2))) (= (f5 c_0 c_3 c_3) (f4 (f5 c_3 c_0 c_3))) (= (f5 c_1 c_0 c_0) (f4 (f5 c_0 c_1 c_0))) (= (f5 c_1 c_0 c_1) (f4 (f5 c_0 c_1 c_1))) (= (f5 c_1 c_0 c_2) (f4 (f5 c_0 c_1 c_2))) (= (f5 c_1 c_0 c_3) (f4 (f5 c_0 c_1 c_3))) (= (f5 c_1 c_1 c_0) (f4 (f5 c_1 c_1 c_0))) (= (f5 c_1 c_1 c_1) (f4 (f5 c_1 c_1 c_1))) (= (f5 c_1 c_1 c_2) (f4 (f5 c_1 c_1 c_2))) (= (f5 c_1 c_1 c_3) (f4 (f5 c_1 c_1 c_3))) (= (f5 c_1 c_2 c_0) (f4 (f5 c_2 c_1 c_0))) (= (f5 c_1 c_2 c_1) (f4 (f5 c_2 c_1 c_1))) (= (f5 c_1 c_2 c_2) (f4 (f5 c_2 c_1 c_2))) (= (f5 c_1 c_2 c_3) (f4 (f5 c_2 c_1 c_3))) (= (f5 c_1 c_3 c_0) (f4 (f5 c_3 c_1 c_0))) (= (f5 c_1 c_3 c_1) (f4 (f5 c_3 c_1 c_1))) (= (f5 c_1 c_3 c_2) (f4 (f5 c_3 c_1 c_2))) (= (f5 c_1 c_3 c_3) (f4 (f5 c_3 c_1 c_3))) (= (f5 c_2 c_0 c_0) (f4 (f5 c_0 c_2 c_0))) (= (f5 c_2 c_0 c_1) (f4 (f5 c_0 c_2 c_1))) (= (f5 c_2 c_0 c_2) (f4 (f5 c_0 c_2 c_2))) (= (f5 c_2 c_0 c_3) (f4 (f5 c_0 c_2 c_3))) (= (f5 c_2 c_1 c_0) (f4 (f5 c_1 c_2 c_0))) (= (f5 c_2 c_1 c_1) (f4 (f5 c_1 c_2 c_1))) (= (f5 c_2 c_1 c_2) (f4 (f5 c_1 c_2 c_2))) (= (f5 c_2 c_1 c_3) (f4 (f5 c_1 c_2 c_3))) (= (f5 c_2 c_2 c_0) (f4 (f5 c_2 c_2 c_0))) (= (f5 c_2 c_2 c_1) (f4 (f5 c_2 c_2 c_1))) (= (f5 c_2 c_2 c_2) (f4 (f5 c_2 c_2 c_2))) (= (f5 c_2 c_2 c_3) (f4 (f5 c_2 c_2 c_3))) (= (f5 c_2 c_3 c_0) (f4 (f5 c_3 c_2 c_0))) (= (f5 c_2 c_3 c_1) (f4 (f5 c_3 c_2 c_1))) (= (f5 c_2 c_3 c_2) (f4 (f5 c_3 c_2 c_2))) (= (f5 c_2 c_3 c_3) (f4 (f5 c_3 c_2 c_3))) (= (f5 c_3 c_0 c_0) (f4 (f5 c_0 c_3 c_0))) (= (f5 c_3 c_0 c_1) (f4 (f5 c_0 c_3 c_1))) (= (f5 c_3 c_0 c_2) (f4 (f5 c_0 c_3 c_2))) (= (f5 c_3 c_0 c_3) (f4 (f5 c_0 c_3 c_3))) (= (f5 c_3 c_1 c_0) (f4 (f5 c_1 c_3 c_0))) (= (f5 c_3 c_1 c_1) (f4 (f5 c_1 c_3 c_1))) (= (f5 c_3 c_1 c_2) (f4 (f5 c_1 c_3 c_2))) (= (f5 c_3 c_1 c_3) (f4 (f5 c_1 c_3 c_3))) (= (f5 c_3 c_2 c_0) (f4 (f5 c_2 c_3 c_0))) (= (f5 c_3 c_2 c_1) (f4 (f5 c_2 c_3 c_1))) (= (f5 c_3 c_2 c_2) (f4 (f5 c_2 c_3 c_2))) (= (f5 c_3 c_2 c_3) (f4 (f5 c_2 c_3 c_3))) (= (f5 c_3 c_3 c_0) (f4 (f5 c_3 c_3 c_0))) (= (f5 c_3 c_3 c_1) (f4 (f5 c_3 c_3 c_1))) (= (f5 c_3 c_3 c_2) (f4 (f5 c_3 c_3 c_2))) (= (f5 c_3 c_3 c_3) (f4 (f5 c_3 c_3 c_3))) (= (f1 c2 c_0) c_0) (= (f1 c2 c_1) c_1) (= (f1 c2 c_2) c_2) (= (f1 c2 c_3) c_3) (= (f3 (f3 c_0 c_0) c_0) (f3 c_0 (f3 c_0 c_0))) (= (f3 (f3 c_0 c_1) c_1) (f3 c_0 (f3 c_1 c_1))) (= (f3 (f3 c_0 c_2) c_2) (f3 c_0 (f3 c_2 c_2))) (= (f3 (f3 c_0 c_3) c_3) (f3 c_0 (f3 c_3 c_3))) (= (f3 (f3 c_1 c_0) c_0) (f3 c_1 (f3 c_0 c_0))) (= (f3 (f3 c_1 c_1) c_1) (f3 c_1 (f3 c_1 c_1))) (= (f3 (f3 c_1 c_2) c_2) (f3 c_1 (f3 c_2 c_2))) (= (f3 (f3 c_1 c_3) c_3) (f3 c_1 (f3 c_3 c_3))) (= (f3 (f3 c_2 c_0) c_0) (f3 c_2 (f3 c_0 c_0))) (= (f3 (f3 c_2 c_1) c_1) (f3 c_2 (f3 c_1 c_1))) (= (f3 (f3 c_2 c_2) c_2) (f3 c_2 (f3 c_2 c_2))) (= (f3 (f3 c_2 c_3) c_3) (f3 c_2 (f3 c_3 c_3))) (= (f3 (f3 c_3 c_0) c_0) (f3 c_3 (f3 c_0 c_0))) (= (f3 (f3 c_3 c_1) c_1) (f3 c_3 (f3 c_1 c_1))) (= (f3 (f3 c_3 c_2) c_2) (f3 c_3 (f3 c_2 c_2))) (= (f3 (f3 c_3 c_3) c_3) (f3 c_3 (f3 c_3 c_3))) (= (f3 c2 c_0) c2) (= (f3 c2 c_1) c2) (= (f3 c2 c_2) c2) (= (f3 c2 c_3) c2) (= (f4 c2) c2) (= (f5 c_0 c_0 c_0) (f1 (f3 (f3 c_0 c_0) c_0) (f4 (f3 c_0 (f3 c_0 c_0))))) (= (f5 c_0 c_0 c_1) (f1 (f3 (f3 c_0 c_0) c_1) (f4 (f3 c_0 (f3 c_0 c_1))))) (= (f5 c_0 c_0 c_2) (f1 (f3 (f3 c_0 c_0) c_2) (f4 (f3 c_0 (f3 c_0 c_2))))) (= (f5 c_0 c_0 c_3) (f1 (f3 (f3 c_0 c_0) c_3) (f4 (f3 c_0 (f3 c_0 c_3))))) (= (f5 c_0 c_1 c_0) (f1 (f3 (f3 c_0 c_1) c_0) (f4 (f3 c_0 (f3 c_1 c_0))))) (= (f5 c_0 c_1 c_1) (f1 (f3 (f3 c_0 c_1) c_1) (f4 (f3 c_0 (f3 c_1 c_1))))) (= (f5 c_0 c_1 c_2) (f1 (f3 (f3 c_0 c_1) c_2) (f4 (f3 c_0 (f3 c_1 c_2))))) (= (f5 c_0 c_1 c_3) (f1 (f3 (f3 c_0 c_1) c_3) (f4 (f3 c_0 (f3 c_1 c_3))))) (= (f5 c_0 c_2 c_0) (f1 (f3 (f3 c_0 c_2) c_0) (f4 (f3 c_0 (f3 c_2 c_0))))) (= (f5 c_0 c_2 c_1) (f1 (f3 (f3 c_0 c_2) c_1) (f4 (f3 c_0 (f3 c_2 c_1))))) (= (f5 c_0 c_2 c_2) (f1 (f3 (f3 c_0 c_2) c_2) (f4 (f3 c_0 (f3 c_2 c_2))))) (= (f5 c_0 c_2 c_3) (f1 (f3 (f3 c_0 c_2) c_3) (f4 (f3 c_0 (f3 c_2 c_3))))) (= (f5 c_0 c_3 c_0) (f1 (f3 (f3 c_0 c_3) c_0) (f4 (f3 c_0 (f3 c_3 c_0))))) (= (f5 c_0 c_3 c_1) (f1 (f3 (f3 c_0 c_3) c_1) (f4 (f3 c_0 (f3 c_3 c_1))))) (= (f5 c_0 c_3 c_2) (f1 (f3 (f3 c_0 c_3) c_2) (f4 (f3 c_0 (f3 c_3 c_2))))) (= (f5 c_0 c_3 c_3) (f1 (f3 (f3 c_0 c_3) c_3) (f4 (f3 c_0 (f3 c_3 c_3))))) (= (f5 c_1 c_0 c_0) (f1 (f3 (f3 c_1 c_0) c_0) (f4 (f3 c_1 (f3 c_0 c_0))))) (= (f5 c_1 c_0 c_1) (f1 (f3 (f3 c_1 c_0) c_1) (f4 (f3 c_1 (f3 c_0 c_1))))) (= (f5 c_1 c_0 c_2) (f1 (f3 (f3 c_1 c_0) c_2) (f4 (f3 c_1 (f3 c_0 c_2))))) (= (f5 c_1 c_0 c_3) (f1 (f3 (f3 c_1 c_0) c_3) (f4 (f3 c_1 (f3 c_0 c_3))))) (= (f5 c_1 c_1 c_0) (f1 (f3 (f3 c_1 c_1) c_0) (f4 (f3 c_1 (f3 c_1 c_0))))) (= (f5 c_1 c_1 c_1) (f1 (f3 (f3 c_1 c_1) c_1) (f4 (f3 c_1 (f3 c_1 c_1))))) (= (f5 c_1 c_1 c_2) (f1 (f3 (f3 c_1 c_1) c_2) (f4 (f3 c_1 (f3 c_1 c_2))))) (= (f5 c_1 c_1 c_3) (f1 (f3 (f3 c_1 c_1) c_3) (f4 (f3 c_1 (f3 c_1 c_3))))) (= (f5 c_1 c_2 c_0) (f1 (f3 (f3 c_1 c_2) c_0) (f4 (f3 c_1 (f3 c_2 c_0))))) (= (f5 c_1 c_2 c_1) (f1 (f3 (f3 c_1 c_2) c_1) (f4 (f3 c_1 (f3 c_2 c_1))))) (= (f5 c_1 c_2 c_2) (f1 (f3 (f3 c_1 c_2) c_2) (f4 (f3 c_1 (f3 c_2 c_2))))) (= (f5 c_1 c_2 c_3) (f1 (f3 (f3 c_1 c_2) c_3) (f4 (f3 c_1 (f3 c_2 c_3))))) (= (f5 c_1 c_3 c_0) (f1 (f3 (f3 c_1 c_3) c_0) (f4 (f3 c_1 (f3 c_3 c_0))))) (= (f5 c_1 c_3 c_1) (f1 (f3 (f3 c_1 c_3) c_1) (f4 (f3 c_1 (f3 c_3 c_1))))) (= (f5 c_1 c_3 c_2) (f1 (f3 (f3 c_1 c_3) c_2) (f4 (f3 c_1 (f3 c_3 c_2))))) (= (f5 c_1 c_3 c_3) (f1 (f3 (f3 c_1 c_3) c_3) (f4 (f3 c_1 (f3 c_3 c_3))))) (= (f5 c_2 c_0 c_0) (f1 (f3 (f3 c_2 c_0) c_0) (f4 (f3 c_2 (f3 c_0 c_0))))) (= (f5 c_2 c_0 c_1) (f1 (f3 (f3 c_2 c_0) c_1) (f4 (f3 c_2 (f3 c_0 c_1))))) (= (f5 c_2 c_0 c_2) (f1 (f3 (f3 c_2 c_0) c_2) (f4 (f3 c_2 (f3 c_0 c_2))))) (= (f5 c_2 c_0 c_3) (f1 (f3 (f3 c_2 c_0) c_3) (f4 (f3 c_2 (f3 c_0 c_3))))) (= (f5 c_2 c_1 c_0) (f1 (f3 (f3 c_2 c_1) c_0) (f4 (f3 c_2 (f3 c_1 c_0))))) (= (f5 c_2 c_1 c_1) (f1 (f3 (f3 c_2 c_1) c_1) (f4 (f3 c_2 (f3 c_1 c_1))))) (= (f5 c_2 c_1 c_2) (f1 (f3 (f3 c_2 c_1) c_2) (f4 (f3 c_2 (f3 c_1 c_2))))) (= (f5 c_2 c_1 c_3) (f1 (f3 (f3 c_2 c_1) c_3) (f4 (f3 c_2 (f3 c_1 c_3))))) (= (f5 c_2 c_2 c_0) (f1 (f3 (f3 c_2 c_2) c_0) (f4 (f3 c_2 (f3 c_2 c_0))))) (= (f5 c_2 c_2 c_1) (f1 (f3 (f3 c_2 c_2) c_1) (f4 (f3 c_2 (f3 c_2 c_1))))) (= (f5 c_2 c_2 c_2) (f1 (f3 (f3 c_2 c_2) c_2) (f4 (f3 c_2 (f3 c_2 c_2))))) (= (f5 c_2 c_2 c_3) (f1 (f3 (f3 c_2 c_2) c_3) (f4 (f3 c_2 (f3 c_2 c_3))))) (= (f5 c_2 c_3 c_0) (f1 (f3 (f3 c_2 c_3) c_0) (f4 (f3 c_2 (f3 c_3 c_0))))) (= (f5 c_2 c_3 c_1) (f1 (f3 (f3 c_2 c_3) c_1) (f4 (f3 c_2 (f3 c_3 c_1))))) (= (f5 c_2 c_3 c_2) (f1 (f3 (f3 c_2 c_3) c_2) (f4 (f3 c_2 (f3 c_3 c_2))))) (= (f5 c_2 c_3 c_3) (f1 (f3 (f3 c_2 c_3) c_3) (f4 (f3 c_2 (f3 c_3 c_3))))) (= (f5 c_3 c_0 c_0) (f1 (f3 (f3 c_3 c_0) c_0) (f4 (f3 c_3 (f3 c_0 c_0))))) (= (f5 c_3 c_0 c_1) (f1 (f3 (f3 c_3 c_0) c_1) (f4 (f3 c_3 (f3 c_0 c_1))))) (= (f5 c_3 c_0 c_2) (f1 (f3 (f3 c_3 c_0) c_2) (f4 (f3 c_3 (f3 c_0 c_2))))) (= (f5 c_3 c_0 c_3) (f1 (f3 (f3 c_3 c_0) c_3) (f4 (f3 c_3 (f3 c_0 c_3))))) (= (f5 c_3 c_1 c_0) (f1 (f3 (f3 c_3 c_1) c_0) (f4 (f3 c_3 (f3 c_1 c_0))))) (= (f5 c_3 c_1 c_1) (f1 (f3 (f3 c_3 c_1) c_1) (f4 (f3 c_3 (f3 c_1 c_1))))) (= (f5 c_3 c_1 c_2) (f1 (f3 (f3 c_3 c_1) c_2) (f4 (f3 c_3 (f3 c_1 c_2))))) (= (f5 c_3 c_1 c_3) (f1 (f3 (f3 c_3 c_1) c_3) (f4 (f3 c_3 (f3 c_1 c_3))))) (= (f5 c_3 c_2 c_0) (f1 (f3 (f3 c_3 c_2) c_0) (f4 (f3 c_3 (f3 c_2 c_0))))) (= (f5 c_3 c_2 c_1) (f1 (f3 (f3 c_3 c_2) c_1) (f4 (f3 c_3 (f3 c_2 c_1))))) (= (f5 c_3 c_2 c_2) (f1 (f3 (f3 c_3 c_2) c_2) (f4 (f3 c_3 (f3 c_2 c_2))))) (= (f5 c_3 c_2 c_3) (f1 (f3 (f3 c_3 c_2) c_3) (f4 (f3 c_3 (f3 c_2 c_3))))) (= (f5 c_3 c_3 c_0) (f1 (f3 (f3 c_3 c_3) c_0) (f4 (f3 c_3 (f3 c_3 c_0))))) (= (f5 c_3 c_3 c_1) (f1 (f3 (f3 c_3 c_3) c_1) (f4 (f3 c_3 (f3 c_3 c_1))))) (= (f5 c_3 c_3 c_2) (f1 (f3 (f3 c_3 c_3) c_2) (f4 (f3 c_3 (f3 c_3 c_2))))) (= (f5 c_3 c_3 c_3) (f1 (f3 (f3 c_3 c_3) c_3) (f4 (f3 c_3 (f3 c_3 c_3))))) (= (f3 c_0 (f4 c_0)) (f4 (f3 c_0 c_0))) (= (f3 c_0 (f4 c_1)) (f4 (f3 c_0 c_1))) (= (f3 c_0 (f4 c_2)) (f4 (f3 c_0 c_2))) (= (f3 c_0 (f4 c_3)) (f4 (f3 c_0 c_3))) (= (f3 c_1 (f4 c_0)) (f4 (f3 c_1 c_0))) (= (f3 c_1 (f4 c_1)) (f4 (f3 c_1 c_1))) (= (f3 c_1 (f4 c_2)) (f4 (f3 c_1 c_2))) (= (f3 c_1 (f4 c_3)) (f4 (f3 c_1 c_3))) (= (f3 c_2 (f4 c_0)) (f4 (f3 c_2 c_0))) (= (f3 c_2 (f4 c_1)) (f4 (f3 c_2 c_1))) (= (f3 c_2 (f4 c_2)) (f4 (f3 c_2 c_2))) (= (f3 c_2 (f4 c_3)) (f4 (f3 c_2 c_3))) (= (f3 c_3 (f4 c_0)) (f4 (f3 c_3 c_0))) (= (f3 c_3 (f4 c_1)) (f4 (f3 c_3 c_1))) (= (f3 c_3 (f4 c_2)) (f4 (f3 c_3 c_2))) (= (f3 c_3 (f4 c_3)) (f4 (f3 c_3 c_3))) (= (f3 (f3 c_0 (f3 c_0 c_0)) c_0) (f3 c_0 (f3 c_0 (f3 c_0 c_0)))) (= (f3 (f3 c_0 (f3 c_0 c_0)) c_1) (f3 c_0 (f3 c_0 (f3 c_0 c_1)))) (= (f3 (f3 c_0 (f3 c_0 c_0)) c_2) (f3 c_0 (f3 c_0 (f3 c_0 c_2)))) (= (f3 (f3 c_0 (f3 c_0 c_0)) c_3) (f3 c_0 (f3 c_0 (f3 c_0 c_3)))) (= (f3 (f3 c_0 (f3 c_1 c_0)) c_0) (f3 c_0 (f3 c_1 (f3 c_0 c_0)))) (= (f3 (f3 c_0 (f3 c_1 c_0)) c_1) (f3 c_0 (f3 c_1 (f3 c_0 c_1)))) (= (f3 (f3 c_0 (f3 c_1 c_0)) c_2) (f3 c_0 (f3 c_1 (f3 c_0 c_2)))) (= (f3 (f3 c_0 (f3 c_1 c_0)) c_3) (f3 c_0 (f3 c_1 (f3 c_0 c_3)))) (= (f3 (f3 c_0 (f3 c_2 c_0)) c_0) (f3 c_0 (f3 c_2 (f3 c_0 c_0)))) (= (f3 (f3 c_0 (f3 c_2 c_0)) c_1) (f3 c_0 (f3 c_2 (f3 c_0 c_1)))) (= (f3 (f3 c_0 (f3 c_2 c_0)) c_2) (f3 c_0 (f3 c_2 (f3 c_0 c_2)))) (= (f3 (f3 c_0 (f3 c_2 c_0)) c_3) (f3 c_0 (f3 c_2 (f3 c_0 c_3)))) (= (f3 (f3 c_0 (f3 c_3 c_0)) c_0) (f3 c_0 (f3 c_3 (f3 c_0 c_0)))) (= (f3 (f3 c_0 (f3 c_3 c_0)) c_1) (f3 c_0 (f3 c_3 (f3 c_0 c_1)))) (= (f3 (f3 c_0 (f3 c_3 c_0)) c_2) (f3 c_0 (f3 c_3 (f3 c_0 c_2)))) (= (f3 (f3 c_0 (f3 c_3 c_0)) c_3) (f3 c_0 (f3 c_3 (f3 c_0 c_3)))) (= (f3 (f3 c_1 (f3 c_0 c_1)) c_0) (f3 c_1 (f3 c_0 (f3 c_1 c_0)))) (= (f3 (f3 c_1 (f3 c_0 c_1)) c_1) (f3 c_1 (f3 c_0 (f3 c_1 c_1)))) (= (f3 (f3 c_1 (f3 c_0 c_1)) c_2) (f3 c_1 (f3 c_0 (f3 c_1 c_2)))) (= (f3 (f3 c_1 (f3 c_0 c_1)) c_3) (f3 c_1 (f3 c_0 (f3 c_1 c_3)))) (= (f3 (f3 c_1 (f3 c_1 c_1)) c_0) (f3 c_1 (f3 c_1 (f3 c_1 c_0)))) (= (f3 (f3 c_1 (f3 c_1 c_1)) c_1) (f3 c_1 (f3 c_1 (f3 c_1 c_1)))) (= (f3 (f3 c_1 (f3 c_1 c_1)) c_2) (f3 c_1 (f3 c_1 (f3 c_1 c_2)))) (= (f3 (f3 c_1 (f3 c_1 c_1)) c_3) (f3 c_1 (f3 c_1 (f3 c_1 c_3)))) (= (f3 (f3 c_1 (f3 c_2 c_1)) c_0) (f3 c_1 (f3 c_2 (f3 c_1 c_0)))) (= (f3 (f3 c_1 (f3 c_2 c_1)) c_1) (f3 c_1 (f3 c_2 (f3 c_1 c_1)))) (= (f3 (f3 c_1 (f3 c_2 c_1)) c_2) (f3 c_1 (f3 c_2 (f3 c_1 c_2)))) (= (f3 (f3 c_1 (f3 c_2 c_1)) c_3) (f3 c_1 (f3 c_2 (f3 c_1 c_3)))) (= (f3 (f3 c_1 (f3 c_3 c_1)) c_0) (f3 c_1 (f3 c_3 (f3 c_1 c_0)))) (= (f3 (f3 c_1 (f3 c_3 c_1)) c_1) (f3 c_1 (f3 c_3 (f3 c_1 c_1)))) (= (f3 (f3 c_1 (f3 c_3 c_1)) c_2) (f3 c_1 (f3 c_3 (f3 c_1 c_2)))) (= (f3 (f3 c_1 (f3 c_3 c_1)) c_3) (f3 c_1 (f3 c_3 (f3 c_1 c_3)))) (= (f3 (f3 c_2 (f3 c_0 c_2)) c_0) (f3 c_2 (f3 c_0 (f3 c_2 c_0)))) (= (f3 (f3 c_2 (f3 c_0 c_2)) c_1) (f3 c_2 (f3 c_0 (f3 c_2 c_1)))) (= (f3 (f3 c_2 (f3 c_0 c_2)) c_2) (f3 c_2 (f3 c_0 (f3 c_2 c_2)))) (= (f3 (f3 c_2 (f3 c_0 c_2)) c_3) (f3 c_2 (f3 c_0 (f3 c_2 c_3)))) (= (f3 (f3 c_2 (f3 c_1 c_2)) c_0) (f3 c_2 (f3 c_1 (f3 c_2 c_0)))) (= (f3 (f3 c_2 (f3 c_1 c_2)) c_1) (f3 c_2 (f3 c_1 (f3 c_2 c_1)))) (= (f3 (f3 c_2 (f3 c_1 c_2)) c_2) (f3 c_2 (f3 c_1 (f3 c_2 c_2)))) (= (f3 (f3 c_2 (f3 c_1 c_2)) c_3) (f3 c_2 (f3 c_1 (f3 c_2 c_3)))) (= (f3 (f3 c_2 (f3 c_2 c_2)) c_0) (f3 c_2 (f3 c_2 (f3 c_2 c_0)))) (= (f3 (f3 c_2 (f3 c_2 c_2)) c_1) (f3 c_2 (f3 c_2 (f3 c_2 c_1)))) (= (f3 (f3 c_2 (f3 c_2 c_2)) c_2) (f3 c_2 (f3 c_2 (f3 c_2 c_2)))) (= (f3 (f3 c_2 (f3 c_2 c_2)) c_3) (f3 c_2 (f3 c_2 (f3 c_2 c_3)))) (= (f3 (f3 c_2 (f3 c_3 c_2)) c_0) (f3 c_2 (f3 c_3 (f3 c_2 c_0)))) (= (f3 (f3 c_2 (f3 c_3 c_2)) c_1) (f3 c_2 (f3 c_3 (f3 c_2 c_1)))) (= (f3 (f3 c_2 (f3 c_3 c_2)) c_2) (f3 c_2 (f3 c_3 (f3 c_2 c_2)))) (= (f3 (f3 c_2 (f3 c_3 c_2)) c_3) (f3 c_2 (f3 c_3 (f3 c_2 c_3)))) (= (f3 (f3 c_3 (f3 c_0 c_3)) c_0) (f3 c_3 (f3 c_0 (f3 c_3 c_0)))) (= (f3 (f3 c_3 (f3 c_0 c_3)) c_1) (f3 c_3 (f3 c_0 (f3 c_3 c_1)))) (= (f3 (f3 c_3 (f3 c_0 c_3)) c_2) (f3 c_3 (f3 c_0 (f3 c_3 c_2)))) (= (f3 (f3 c_3 (f3 c_0 c_3)) c_3) (f3 c_3 (f3 c_0 (f3 c_3 c_3)))) (= (f3 (f3 c_3 (f3 c_1 c_3)) c_0) (f3 c_3 (f3 c_1 (f3 c_3 c_0)))) (= (f3 (f3 c_3 (f3 c_1 c_3)) c_1) (f3 c_3 (f3 c_1 (f3 c_3 c_1)))) (= (f3 (f3 c_3 (f3 c_1 c_3)) c_2) (f3 c_3 (f3 c_1 (f3 c_3 c_2)))) (= (f3 (f3 c_3 (f3 c_1 c_3)) c_3) (f3 c_3 (f3 c_1 (f3 c_3 c_3)))) (= (f3 (f3 c_3 (f3 c_2 c_3)) c_0) (f3 c_3 (f3 c_2 (f3 c_3 c_0)))) (= (f3 (f3 c_3 (f3 c_2 c_3)) c_1) (f3 c_3 (f3 c_2 (f3 c_3 c_1)))) (= (f3 (f3 c_3 (f3 c_2 c_3)) c_2) (f3 c_3 (f3 c_2 (f3 c_3 c_2)))) (= (f3 (f3 c_3 (f3 c_2 c_3)) c_3) (f3 c_3 (f3 c_2 (f3 c_3 c_3)))) (= (f3 (f3 c_3 (f3 c_3 c_3)) c_0) (f3 c_3 (f3 c_3 (f3 c_3 c_0)))) (= (f3 (f3 c_3 (f3 c_3 c_3)) c_1) (f3 c_3 (f3 c_3 (f3 c_3 c_1)))) (= (f3 (f3 c_3 (f3 c_3 c_3)) c_2) (f3 c_3 (f3 c_3 (f3 c_3 c_2)))) (= (f3 (f3 c_3 (f3 c_3 c_3)) c_3) (f3 c_3 (f3 c_3 (f3 c_3 c_3)))) (or (= c_0 c_0) (not (= (f1 c_0 c_0) (f1 c_0 c_0))) )(or (= c_0 c_0) (not (= (f1 c_0 c_1) (f1 c_0 c_1))) )(or (= c_0 c_0) (not (= (f1 c_0 c_2) (f1 c_0 c_2))) )(or (= c_0 c_0) (not (= (f1 c_0 c_3) (f1 c_0 c_3))) )(or (= c_0 c_1) (not (= (f1 c_0 c_0) (f1 c_1 c_0))) )(or (= c_0 c_1) (not (= (f1 c_0 c_1) (f1 c_1 c_1))) )(or (= c_0 c_1) (not (= (f1 c_0 c_2) (f1 c_1 c_2))) )(or (= c_0 c_1) (not (= (f1 c_0 c_3) (f1 c_1 c_3))) )(or (= c_0 c_2) (not (= (f1 c_0 c_0) (f1 c_2 c_0))) )(or (= c_0 c_2) (not (= (f1 c_0 c_1) (f1 c_2 c_1))) )(or (= c_0 c_2) (not (= (f1 c_0 c_2) (f1 c_2 c_2))) )(or (= c_0 c_2) (not (= (f1 c_0 c_3) (f1 c_2 c_3))) )(or (= c_0 c_3) (not (= (f1 c_0 c_0) (f1 c_3 c_0))) )(or (= c_0 c_3) (not (= (f1 c_0 c_1) (f1 c_3 c_1))) )(or (= c_0 c_3) (not (= (f1 c_0 c_2) (f1 c_3 c_2))) )(or (= c_0 c_3) (not (= (f1 c_0 c_3) (f1 c_3 c_3))) )(or (= c_1 c_0) (not (= (f1 c_1 c_0) (f1 c_0 c_0))) )(or (= c_1 c_0) (not (= (f1 c_1 c_1) (f1 c_0 c_1))) )(or (= c_1 c_0) (not (= (f1 c_1 c_2) (f1 c_0 c_2))) )(or (= c_1 c_0) (not (= (f1 c_1 c_3) (f1 c_0 c_3))) )(or (= c_1 c_1) (not (= (f1 c_1 c_0) (f1 c_1 c_0))) )(or (= c_1 c_1) (not (= (f1 c_1 c_1) (f1 c_1 c_1))) )(or (= c_1 c_1) (not (= (f1 c_1 c_2) (f1 c_1 c_2))) )(or (= c_1 c_1) (not (= (f1 c_1 c_3) (f1 c_1 c_3))) )(or (= c_1 c_2) (not (= (f1 c_1 c_0) (f1 c_2 c_0))) )(or (= c_1 c_2) (not (= (f1 c_1 c_1) (f1 c_2 c_1))) )(or (= c_1 c_2) (not (= (f1 c_1 c_2) (f1 c_2 c_2))) )(or (= c_1 c_2) (not (= (f1 c_1 c_3) (f1 c_2 c_3))) )(or (= c_1 c_3) (not (= (f1 c_1 c_0) (f1 c_3 c_0))) )(or (= c_1 c_3) (not (= (f1 c_1 c_1) (f1 c_3 c_1))) )(or (= c_1 c_3) (not (= (f1 c_1 c_2) (f1 c_3 c_2))) )(or (= c_1 c_3) (not (= (f1 c_1 c_3) (f1 c_3 c_3))) )(or (= c_2 c_0) (not (= (f1 c_2 c_0) (f1 c_0 c_0))) )(or (= c_2 c_0) (not (= (f1 c_2 c_1) (f1 c_0 c_1))) )(or (= c_2 c_0) (not (= (f1 c_2 c_2) (f1 c_0 c_2))) )(or (= c_2 c_0) (not (= (f1 c_2 c_3) (f1 c_0 c_3))) )(or (= c_2 c_1) (not (= (f1 c_2 c_0) (f1 c_1 c_0))) )(or (= c_2 c_1) (not (= (f1 c_2 c_1) (f1 c_1 c_1))) )(or (= c_2 c_1) (not (= (f1 c_2 c_2) (f1 c_1 c_2))) )(or (= c_2 c_1) (not (= (f1 c_2 c_3) (f1 c_1 c_3))) )(or (= c_2 c_2) (not (= (f1 c_2 c_0) (f1 c_2 c_0))) )(or (= c_2 c_2) (not (= (f1 c_2 c_1) (f1 c_2 c_1))) )(or (= c_2 c_2) (not (= (f1 c_2 c_2) (f1 c_2 c_2))) )(or (= c_2 c_2) (not (= (f1 c_2 c_3) (f1 c_2 c_3))) )(or (= c_2 c_3) (not (= (f1 c_2 c_0) (f1 c_3 c_0))) )(or (= c_2 c_3) (not (= (f1 c_2 c_1) (f1 c_3 c_1))) )(or (= c_2 c_3) (not (= (f1 c_2 c_2) (f1 c_3 c_2))) )(or (= c_2 c_3) (not (= (f1 c_2 c_3) (f1 c_3 c_3))) )(or (= c_3 c_0) (not (= (f1 c_3 c_0) (f1 c_0 c_0))) )(or (= c_3 c_0) (not (= (f1 c_3 c_1) (f1 c_0 c_1))) )(or (= c_3 c_0) (not (= (f1 c_3 c_2) (f1 c_0 c_2))) )(or (= c_3 c_0) (not (= (f1 c_3 c_3) (f1 c_0 c_3))) )(or (= c_3 c_1) (not (= (f1 c_3 c_0) (f1 c_1 c_0))) )(or (= c_3 c_1) (not (= (f1 c_3 c_1) (f1 c_1 c_1))) )(or (= c_3 c_1) (not (= (f1 c_3 c_2) (f1 c_1 c_2))) )(or (= c_3 c_1) (not (= (f1 c_3 c_3) (f1 c_1 c_3))) )(or (= c_3 c_2) (not (= (f1 c_3 c_0) (f1 c_2 c_0))) )(or (= c_3 c_2) (not (= (f1 c_3 c_1) (f1 c_2 c_1))) )(or (= c_3 c_2) (not (= (f1 c_3 c_2) (f1 c_2 c_2))) )(or (= c_3 c_2) (not (= (f1 c_3 c_3) (f1 c_2 c_3))) )(or (= c_3 c_3) (not (= (f1 c_3 c_0) (f1 c_3 c_0))) )(or (= c_3 c_3) (not (= (f1 c_3 c_1) (f1 c_3 c_1))) )(or (= c_3 c_3) (not (= (f1 c_3 c_2) (f1 c_3 c_2))) )(or (= c_3 c_3) (not (= (f1 c_3 c_3) (f1 c_3 c_3))) )(= (f1 c_0 (f1 c_0 c_0)) (f1 (f1 c_0 c_0) c_0)) (= (f1 c_0 (f1 c_0 c_1)) (f1 (f1 c_0 c_0) c_1)) (= (f1 c_0 (f1 c_0 c_2)) (f1 (f1 c_0 c_0) c_2)) (= (f1 c_0 (f1 c_0 c_3)) (f1 (f1 c_0 c_0) c_3)) (= (f1 c_0 (f1 c_1 c_0)) (f1 (f1 c_0 c_1) c_0)) (= (f1 c_0 (f1 c_1 c_1)) (f1 (f1 c_0 c_1) c_1)) (= (f1 c_0 (f1 c_1 c_2)) (f1 (f1 c_0 c_1) c_2)) (= (f1 c_0 (f1 c_1 c_3)) (f1 (f1 c_0 c_1) c_3)) (= (f1 c_0 (f1 c_2 c_0)) (f1 (f1 c_0 c_2) c_0)) (= (f1 c_0 (f1 c_2 c_1)) (f1 (f1 c_0 c_2) c_1)) (= (f1 c_0 (f1 c_2 c_2)) (f1 (f1 c_0 c_2) c_2)) (= (f1 c_0 (f1 c_2 c_3)) (f1 (f1 c_0 c_2) c_3)) (= (f1 c_0 (f1 c_3 c_0)) (f1 (f1 c_0 c_3) c_0)) (= (f1 c_0 (f1 c_3 c_1)) (f1 (f1 c_0 c_3) c_1)) (= (f1 c_0 (f1 c_3 c_2)) (f1 (f1 c_0 c_3) c_2)) (= (f1 c_0 (f1 c_3 c_3)) (f1 (f1 c_0 c_3) c_3)) (= (f1 c_1 (f1 c_0 c_0)) (f1 (f1 c_1 c_0) c_0)) (= (f1 c_1 (f1 c_0 c_1)) (f1 (f1 c_1 c_0) c_1)) (= (f1 c_1 (f1 c_0 c_2)) (f1 (f1 c_1 c_0) c_2)) (= (f1 c_1 (f1 c_0 c_3)) (f1 (f1 c_1 c_0) c_3)) (= (f1 c_1 (f1 c_1 c_0)) (f1 (f1 c_1 c_1) c_0)) (= (f1 c_1 (f1 c_1 c_1)) (f1 (f1 c_1 c_1) c_1)) (= (f1 c_1 (f1 c_1 c_2)) (f1 (f1 c_1 c_1) c_2)) (= (f1 c_1 (f1 c_1 c_3)) (f1 (f1 c_1 c_1) c_3)) (= (f1 c_1 (f1 c_2 c_0)) (f1 (f1 c_1 c_2) c_0)) (= (f1 c_1 (f1 c_2 c_1)) (f1 (f1 c_1 c_2) c_1)) (= (f1 c_1 (f1 c_2 c_2)) (f1 (f1 c_1 c_2) c_2)) (= (f1 c_1 (f1 c_2 c_3)) (f1 (f1 c_1 c_2) c_3)) (= (f1 c_1 (f1 c_3 c_0)) (f1 (f1 c_1 c_3) c_0)) (= (f1 c_1 (f1 c_3 c_1)) (f1 (f1 c_1 c_3) c_1)) (= (f1 c_1 (f1 c_3 c_2)) (f1 (f1 c_1 c_3) c_2)) (= (f1 c_1 (f1 c_3 c_3)) (f1 (f1 c_1 c_3) c_3)) (= (f1 c_2 (f1 c_0 c_0)) (f1 (f1 c_2 c_0) c_0)) (= (f1 c_2 (f1 c_0 c_1)) (f1 (f1 c_2 c_0) c_1)) (= (f1 c_2 (f1 c_0 c_2)) (f1 (f1 c_2 c_0) c_2)) (= (f1 c_2 (f1 c_0 c_3)) (f1 (f1 c_2 c_0) c_3)) (= (f1 c_2 (f1 c_1 c_0)) (f1 (f1 c_2 c_1) c_0)) (= (f1 c_2 (f1 c_1 c_1)) (f1 (f1 c_2 c_1) c_1)) (= (f1 c_2 (f1 c_1 c_2)) (f1 (f1 c_2 c_1) c_2)) (= (f1 c_2 (f1 c_1 c_3)) (f1 (f1 c_2 c_1) c_3)) (= (f1 c_2 (f1 c_2 c_0)) (f1 (f1 c_2 c_2) c_0)) (= (f1 c_2 (f1 c_2 c_1)) (f1 (f1 c_2 c_2) c_1)) (= (f1 c_2 (f1 c_2 c_2)) (f1 (f1 c_2 c_2) c_2)) (= (f1 c_2 (f1 c_2 c_3)) (f1 (f1 c_2 c_2) c_3)) (= (f1 c_2 (f1 c_3 c_0)) (f1 (f1 c_2 c_3) c_0)) (= (f1 c_2 (f1 c_3 c_1)) (f1 (f1 c_2 c_3) c_1)) (= (f1 c_2 (f1 c_3 c_2)) (f1 (f1 c_2 c_3) c_2)) (= (f1 c_2 (f1 c_3 c_3)) (f1 (f1 c_2 c_3) c_3)) (= (f1 c_3 (f1 c_0 c_0)) (f1 (f1 c_3 c_0) c_0)) (= (f1 c_3 (f1 c_0 c_1)) (f1 (f1 c_3 c_0) c_1)) (= (f1 c_3 (f1 c_0 c_2)) (f1 (f1 c_3 c_0) c_2)) (= (f1 c_3 (f1 c_0 c_3)) (f1 (f1 c_3 c_0) c_3)) (= (f1 c_3 (f1 c_1 c_0)) (f1 (f1 c_3 c_1) c_0)) (= (f1 c_3 (f1 c_1 c_1)) (f1 (f1 c_3 c_1) c_1)) (= (f1 c_3 (f1 c_1 c_2)) (f1 (f1 c_3 c_1) c_2)) (= (f1 c_3 (f1 c_1 c_3)) (f1 (f1 c_3 c_1) c_3)) (= (f1 c_3 (f1 c_2 c_0)) (f1 (f1 c_3 c_2) c_0)) (= (f1 c_3 (f1 c_2 c_1)) (f1 (f1 c_3 c_2) c_1)) (= (f1 c_3 (f1 c_2 c_2)) (f1 (f1 c_3 c_2) c_2)) (= (f1 c_3 (f1 c_2 c_3)) (f1 (f1 c_3 c_2) c_3)) (= (f1 c_3 (f1 c_3 c_0)) (f1 (f1 c_3 c_3) c_0)) (= (f1 c_3 (f1 c_3 c_1)) (f1 (f1 c_3 c_3) c_1)) (= (f1 c_3 (f1 c_3 c_2)) (f1 (f1 c_3 c_3) c_2)) (= (f1 c_3 (f1 c_3 c_3)) (f1 (f1 c_3 c_3) c_3)) (= (f3 c_0 (f1 c_0 c_0)) (f1 (f3 c_0 c_0) (f3 c_0 c_0))) (= (f3 c_0 (f1 c_0 c_1)) (f1 (f3 c_0 c_0) (f3 c_0 c_1))) (= (f3 c_0 (f1 c_0 c_2)) (f1 (f3 c_0 c_0) (f3 c_0 c_2))) (= (f3 c_0 (f1 c_0 c_3)) (f1 (f3 c_0 c_0) (f3 c_0 c_3))) (= (f3 c_0 (f1 c_1 c_0)) (f1 (f3 c_0 c_1) (f3 c_0 c_0))) (= (f3 c_0 (f1 c_1 c_1)) (f1 (f3 c_0 c_1) (f3 c_0 c_1))) (= (f3 c_0 (f1 c_1 c_2)) (f1 (f3 c_0 c_1) (f3 c_0 c_2))) (= (f3 c_0 (f1 c_1 c_3)) (f1 (f3 c_0 c_1) (f3 c_0 c_3))) (= (f3 c_0 (f1 c_2 c_0)) (f1 (f3 c_0 c_2) (f3 c_0 c_0))) (= (f3 c_0 (f1 c_2 c_1)) (f1 (f3 c_0 c_2) (f3 c_0 c_1))) (= (f3 c_0 (f1 c_2 c_2)) (f1 (f3 c_0 c_2) (f3 c_0 c_2))) (= (f3 c_0 (f1 c_2 c_3)) (f1 (f3 c_0 c_2) (f3 c_0 c_3))) (= (f3 c_0 (f1 c_3 c_0)) (f1 (f3 c_0 c_3) (f3 c_0 c_0))) (= (f3 c_0 (f1 c_3 c_1)) (f1 (f3 c_0 c_3) (f3 c_0 c_1))) (= (f3 c_0 (f1 c_3 c_2)) (f1 (f3 c_0 c_3) (f3 c_0 c_2))) (= (f3 c_0 (f1 c_3 c_3)) (f1 (f3 c_0 c_3) (f3 c_0 c_3))) (= (f3 c_1 (f1 c_0 c_0)) (f1 (f3 c_1 c_0) (f3 c_1 c_0))) (= (f3 c_1 (f1 c_0 c_1)) (f1 (f3 c_1 c_0) (f3 c_1 c_1))) (= (f3 c_1 (f1 c_0 c_2)) (f1 (f3 c_1 c_0) (f3 c_1 c_2))) (= (f3 c_1 (f1 c_0 c_3)) (f1 (f3 c_1 c_0) (f3 c_1 c_3))) (= (f3 c_1 (f1 c_1 c_0)) (f1 (f3 c_1 c_1) (f3 c_1 c_0))) (= (f3 c_1 (f1 c_1 c_1)) (f1 (f3 c_1 c_1) (f3 c_1 c_1))) (= (f3 c_1 (f1 c_1 c_2)) (f1 (f3 c_1 c_1) (f3 c_1 c_2))) (= (f3 c_1 (f1 c_1 c_3)) (f1 (f3 c_1 c_1) (f3 c_1 c_3))) (= (f3 c_1 (f1 c_2 c_0)) (f1 (f3 c_1 c_2) (f3 c_1 c_0))) (= (f3 c_1 (f1 c_2 c_1)) (f1 (f3 c_1 c_2) (f3 c_1 c_1))) (= (f3 c_1 (f1 c_2 c_2)) (f1 (f3 c_1 c_2) (f3 c_1 c_2))) (= (f3 c_1 (f1 c_2 c_3)) (f1 (f3 c_1 c_2) (f3 c_1 c_3))) (= (f3 c_1 (f1 c_3 c_0)) (f1 (f3 c_1 c_3) (f3 c_1 c_0))) (= (f3 c_1 (f1 c_3 c_1)) (f1 (f3 c_1 c_3) (f3 c_1 c_1))) (= (f3 c_1 (f1 c_3 c_2)) (f1 (f3 c_1 c_3) (f3 c_1 c_2))) (= (f3 c_1 (f1 c_3 c_3)) (f1 (f3 c_1 c_3) (f3 c_1 c_3))) (= (f3 c_2 (f1 c_0 c_0)) (f1 (f3 c_2 c_0) (f3 c_2 c_0))) (= (f3 c_2 (f1 c_0 c_1)) (f1 (f3 c_2 c_0) (f3 c_2 c_1))) (= (f3 c_2 (f1 c_0 c_2)) (f1 (f3 c_2 c_0) (f3 c_2 c_2))) (= (f3 c_2 (f1 c_0 c_3)) (f1 (f3 c_2 c_0) (f3 c_2 c_3))) (= (f3 c_2 (f1 c_1 c_0)) (f1 (f3 c_2 c_1) (f3 c_2 c_0))) (= (f3 c_2 (f1 c_1 c_1)) (f1 (f3 c_2 c_1) (f3 c_2 c_1))) (= (f3 c_2 (f1 c_1 c_2)) (f1 (f3 c_2 c_1) (f3 c_2 c_2))) (= (f3 c_2 (f1 c_1 c_3)) (f1 (f3 c_2 c_1) (f3 c_2 c_3))) (= (f3 c_2 (f1 c_2 c_0)) (f1 (f3 c_2 c_2) (f3 c_2 c_0))) (= (f3 c_2 (f1 c_2 c_1)) (f1 (f3 c_2 c_2) (f3 c_2 c_1))) (= (f3 c_2 (f1 c_2 c_2)) (f1 (f3 c_2 c_2) (f3 c_2 c_2))) (= (f3 c_2 (f1 c_2 c_3)) (f1 (f3 c_2 c_2) (f3 c_2 c_3))) (= (f3 c_2 (f1 c_3 c_0)) (f1 (f3 c_2 c_3) (f3 c_2 c_0))) (= (f3 c_2 (f1 c_3 c_1)) (f1 (f3 c_2 c_3) (f3 c_2 c_1))) (= (f3 c_2 (f1 c_3 c_2)) (f1 (f3 c_2 c_3) (f3 c_2 c_2))) (= (f3 c_2 (f1 c_3 c_3)) (f1 (f3 c_2 c_3) (f3 c_2 c_3))) (= (f3 c_3 (f1 c_0 c_0)) (f1 (f3 c_3 c_0) (f3 c_3 c_0))) (= (f3 c_3 (f1 c_0 c_1)) (f1 (f3 c_3 c_0) (f3 c_3 c_1))) (= (f3 c_3 (f1 c_0 c_2)) (f1 (f3 c_3 c_0) (f3 c_3 c_2))) (= (f3 c_3 (f1 c_0 c_3)) (f1 (f3 c_3 c_0) (f3 c_3 c_3))) (= (f3 c_3 (f1 c_1 c_0)) (f1 (f3 c_3 c_1) (f3 c_3 c_0))) (= (f3 c_3 (f1 c_1 c_1)) (f1 (f3 c_3 c_1) (f3 c_3 c_1))) (= (f3 c_3 (f1 c_1 c_2)) (f1 (f3 c_3 c_1) (f3 c_3 c_2))) (= (f3 c_3 (f1 c_1 c_3)) (f1 (f3 c_3 c_1) (f3 c_3 c_3))) (= (f3 c_3 (f1 c_2 c_0)) (f1 (f3 c_3 c_2) (f3 c_3 c_0))) (= (f3 c_3 (f1 c_2 c_1)) (f1 (f3 c_3 c_2) (f3 c_3 c_1))) (= (f3 c_3 (f1 c_2 c_2)) (f1 (f3 c_3 c_2) (f3 c_3 c_2))) (= (f3 c_3 (f1 c_2 c_3)) (f1 (f3 c_3 c_2) (f3 c_3 c_3))) (= (f3 c_3 (f1 c_3 c_0)) (f1 (f3 c_3 c_3) (f3 c_3 c_0))) (= (f3 c_3 (f1 c_3 c_1)) (f1 (f3 c_3 c_3) (f3 c_3 c_1))) (= (f3 c_3 (f1 c_3 c_2)) (f1 (f3 c_3 c_3) (f3 c_3 c_2))) (= (f3 c_3 (f1 c_3 c_3)) (f1 (f3 c_3 c_3) (f3 c_3 c_3))) (= (f3 (f4 c_0) c_0) (f4 (f3 c_0 c_0))) (= (f3 (f4 c_0) c_1) (f4 (f3 c_0 c_1))) (= (f3 (f4 c_0) c_2) (f4 (f3 c_0 c_2))) (= (f3 (f4 c_0) c_3) (f4 (f3 c_0 c_3))) (= (f3 (f4 c_1) c_0) (f4 (f3 c_1 c_0))) (= (f3 (f4 c_1) c_1) (f4 (f3 c_1 c_1))) (= (f3 (f4 c_1) c_2) (f4 (f3 c_1 c_2))) (= (f3 (f4 c_1) c_3) (f4 (f3 c_1 c_3))) (= (f3 (f4 c_2) c_0) (f4 (f3 c_2 c_0))) (= (f3 (f4 c_2) c_1) (f4 (f3 c_2 c_1))) (= (f3 (f4 c_2) c_2) (f4 (f3 c_2 c_2))) (= (f3 (f4 c_2) c_3) (f4 (f3 c_2 c_3))) (= (f3 (f4 c_3) c_0) (f4 (f3 c_3 c_0))) (= (f3 (f4 c_3) c_1) (f4 (f3 c_3 c_1))) (= (f3 (f4 c_3) c_2) (f4 (f3 c_3 c_2))) (= (f3 (f4 c_3) c_3) (f4 (f3 c_3 c_3))) (= (f5 c_0 c_0 c_0) (f4 (f5 c_0 c_0 c_0))) (= (f5 c_0 c_0 c_1) (f4 (f5 c_1 c_0 c_0))) (= (f5 c_0 c_0 c_2) (f4 (f5 c_2 c_0 c_0))) (= (f5 c_0 c_0 c_3) (f4 (f5 c_3 c_0 c_0))) (= (f5 c_0 c_1 c_0) (f4 (f5 c_0 c_1 c_0))) (= (f5 c_0 c_1 c_1) (f4 (f5 c_1 c_1 c_0))) (= (f5 c_0 c_1 c_2) (f4 (f5 c_2 c_1 c_0))) (= (f5 c_0 c_1 c_3) (f4 (f5 c_3 c_1 c_0))) (= (f5 c_0 c_2 c_0) (f4 (f5 c_0 c_2 c_0))) (= (f5 c_0 c_2 c_1) (f4 (f5 c_1 c_2 c_0))) (= (f5 c_0 c_2 c_2) (f4 (f5 c_2 c_2 c_0))) (= (f5 c_0 c_2 c_3) (f4 (f5 c_3 c_2 c_0))) (= (f5 c_0 c_3 c_0) (f4 (f5 c_0 c_3 c_0))) (= (f5 c_0 c_3 c_1) (f4 (f5 c_1 c_3 c_0))) (= (f5 c_0 c_3 c_2) (f4 (f5 c_2 c_3 c_0))) (= (f5 c_0 c_3 c_3) (f4 (f5 c_3 c_3 c_0))) (= (f5 c_1 c_0 c_0) (f4 (f5 c_0 c_0 c_1))) (= (f5 c_1 c_0 c_1) (f4 (f5 c_1 c_0 c_1))) (= (f5 c_1 c_0 c_2) (f4 (f5 c_2 c_0 c_1))) (= (f5 c_1 c_0 c_3) (f4 (f5 c_3 c_0 c_1))) (= (f5 c_1 c_1 c_0) (f4 (f5 c_0 c_1 c_1))) (= (f5 c_1 c_1 c_1) (f4 (f5 c_1 c_1 c_1))) (= (f5 c_1 c_1 c_2) (f4 (f5 c_2 c_1 c_1))) (= (f5 c_1 c_1 c_3) (f4 (f5 c_3 c_1 c_1))) (= (f5 c_1 c_2 c_0) (f4 (f5 c_0 c_2 c_1))) (= (f5 c_1 c_2 c_1) (f4 (f5 c_1 c_2 c_1))) (= (f5 c_1 c_2 c_2) (f4 (f5 c_2 c_2 c_1))) (= (f5 c_1 c_2 c_3) (f4 (f5 c_3 c_2 c_1))) (= (f5 c_1 c_3 c_0) (f4 (f5 c_0 c_3 c_1))) (= (f5 c_1 c_3 c_1) (f4 (f5 c_1 c_3 c_1))) (= (f5 c_1 c_3 c_2) (f4 (f5 c_2 c_3 c_1))) (= (f5 c_1 c_3 c_3) (f4 (f5 c_3 c_3 c_1))) (= (f5 c_2 c_0 c_0) (f4 (f5 c_0 c_0 c_2))) (= (f5 c_2 c_0 c_1) (f4 (f5 c_1 c_0 c_2))) (= (f5 c_2 c_0 c_2) (f4 (f5 c_2 c_0 c_2))) (= (f5 c_2 c_0 c_3) (f4 (f5 c_3 c_0 c_2))) (= (f5 c_2 c_1 c_0) (f4 (f5 c_0 c_1 c_2))) (= (f5 c_2 c_1 c_1) (f4 (f5 c_1 c_1 c_2))) (= (f5 c_2 c_1 c_2) (f4 (f5 c_2 c_1 c_2))) (= (f5 c_2 c_1 c_3) (f4 (f5 c_3 c_1 c_2))) (= (f5 c_2 c_2 c_0) (f4 (f5 c_0 c_2 c_2))) (= (f5 c_2 c_2 c_1) (f4 (f5 c_1 c_2 c_2))) (= (f5 c_2 c_2 c_2) (f4 (f5 c_2 c_2 c_2))) (= (f5 c_2 c_2 c_3) (f4 (f5 c_3 c_2 c_2))) (= (f5 c_2 c_3 c_0) (f4 (f5 c_0 c_3 c_2))) (= (f5 c_2 c_3 c_1) (f4 (f5 c_1 c_3 c_2))) (= (f5 c_2 c_3 c_2) (f4 (f5 c_2 c_3 c_2))) (= (f5 c_2 c_3 c_3) (f4 (f5 c_3 c_3 c_2))) (= (f5 c_3 c_0 c_0) (f4 (f5 c_0 c_0 c_3))) (= (f5 c_3 c_0 c_1) (f4 (f5 c_1 c_0 c_3))) (= (f5 c_3 c_0 c_2) (f4 (f5 c_2 c_0 c_3))) (= (f5 c_3 c_0 c_3) (f4 (f5 c_3 c_0 c_3))) (= (f5 c_3 c_1 c_0) (f4 (f5 c_0 c_1 c_3))) (= (f5 c_3 c_1 c_1) (f4 (f5 c_1 c_1 c_3))) (= (f5 c_3 c_1 c_2) (f4 (f5 c_2 c_1 c_3))) (= (f5 c_3 c_1 c_3) (f4 (f5 c_3 c_1 c_3))) (= (f5 c_3 c_2 c_0) (f4 (f5 c_0 c_2 c_3))) (= (f5 c_3 c_2 c_1) (f4 (f5 c_1 c_2 c_3))) (= (f5 c_3 c_2 c_2) (f4 (f5 c_2 c_2 c_3))) (= (f5 c_3 c_2 c_3) (f4 (f5 c_3 c_2 c_3))) (= (f5 c_3 c_3 c_0) (f4 (f5 c_0 c_3 c_3))) (= (f5 c_3 c_3 c_1) (f4 (f5 c_1 c_3 c_3))) (= (f5 c_3 c_3 c_2) (f4 (f5 c_2 c_3 c_3))) (= (f5 c_3 c_3 c_3) (f4 (f5 c_3 c_3 c_3))) (= (f1 (f4 c_0) c_0) c2) (= (f1 (f4 c_1) c_1) c2) (= (f1 (f4 c_2) c_2) c2) (= (f1 (f4 c_3) c_3) c2) (= (f4 (f1 c_0 c_0)) (f1 (f4 c_0) (f4 c_0))) (= (f4 (f1 c_0 c_1)) (f1 (f4 c_0) (f4 c_1))) (= (f4 (f1 c_0 c_2)) (f1 (f4 c_0) (f4 c_2))) (= (f4 (f1 c_0 c_3)) (f1 (f4 c_0) (f4 c_3))) (= (f4 (f1 c_1 c_0)) (f1 (f4 c_1) (f4 c_0))) (= (f4 (f1 c_1 c_1)) (f1 (f4 c_1) (f4 c_1))) (= (f4 (f1 c_1 c_2)) (f1 (f4 c_1) (f4 c_2))) (= (f4 (f1 c_1 c_3)) (f1 (f4 c_1) (f4 c_3))) (= (f4 (f1 c_2 c_0)) (f1 (f4 c_2) (f4 c_0))) (= (f4 (f1 c_2 c_1)) (f1 (f4 c_2) (f4 c_1))) (= (f4 (f1 c_2 c_2)) (f1 (f4 c_2) (f4 c_2))) (= (f4 (f1 c_2 c_3)) (f1 (f4 c_2) (f4 c_3))) (= (f4 (f1 c_3 c_0)) (f1 (f4 c_3) (f4 c_0))) (= (f4 (f1 c_3 c_1)) (f1 (f4 c_3) (f4 c_1))) (= (f4 (f1 c_3 c_2)) (f1 (f4 c_3) (f4 c_2))) (= (f4 (f1 c_3 c_3)) (f1 (f4 c_3) (f4 c_3))) (= (f3 (f3 c_0 c_0) c_0) (f3 c_0 (f3 c_0 c_0))) (= (f3 (f3 c_0 c_0) c_1) (f3 c_0 (f3 c_0 c_1))) (= (f3 (f3 c_0 c_0) c_2) (f3 c_0 (f3 c_0 c_2))) (= (f3 (f3 c_0 c_0) c_3) (f3 c_0 (f3 c_0 c_3))) (= (f3 (f3 c_1 c_1) c_0) (f3 c_1 (f3 c_1 c_0))) (= (f3 (f3 c_1 c_1) c_1) (f3 c_1 (f3 c_1 c_1))) (= (f3 (f3 c_1 c_1) c_2) (f3 c_1 (f3 c_1 c_2))) (= (f3 (f3 c_1 c_1) c_3) (f3 c_1 (f3 c_1 c_3))) (= (f3 (f3 c_2 c_2) c_0) (f3 c_2 (f3 c_2 c_0))) (= (f3 (f3 c_2 c_2) c_1) (f3 c_2 (f3 c_2 c_1))) (= (f3 (f3 c_2 c_2) c_2) (f3 c_2 (f3 c_2 c_2))) (= (f3 (f3 c_2 c_2) c_3) (f3 c_2 (f3 c_2 c_3))) (= (f3 (f3 c_3 c_3) c_0) (f3 c_3 (f3 c_3 c_0))) (= (f3 (f3 c_3 c_3) c_1) (f3 c_3 (f3 c_3 c_1))) (= (f3 (f3 c_3 c_3) c_2) (f3 c_3 (f3 c_3 c_2))) (= (f3 (f3 c_3 c_3) c_3) (f3 c_3 (f3 c_3 c_3))) (not (= (f3 (f3 c6 c7) (f3 c8 c6)) (f3 c6 (f3 (f3 c7 c8) c6)))) (or (= (f5 c_0 c_0 c_0) c_0)(= (f5 c_0 c_0 c_0) c_1)(= (f5 c_0 c_0 c_0) c_2)(= (f5 c_0 c_0 c_0) c_3))(or (= (f5 c_0 c_0 c_1) c_0)(= (f5 c_0 c_0 c_1) c_1)(= (f5 c_0 c_0 c_1) c_2)(= (f5 c_0 c_0 c_1) c_3))(or (= (f5 c_0 c_0 c_2) c_0)(= (f5 c_0 c_0 c_2) c_1)(= (f5 c_0 c_0 c_2) c_2)(= (f5 c_0 c_0 c_2) c_3))(or (= (f5 c_0 c_0 c_3) c_0)(= (f5 c_0 c_0 c_3) c_1)(= (f5 c_0 c_0 c_3) c_2)(= (f5 c_0 c_0 c_3) c_3))(or (= (f5 c_0 c_1 c_0) c_0)(= (f5 c_0 c_1 c_0) c_1)(= (f5 c_0 c_1 c_0) c_2)(= (f5 c_0 c_1 c_0) c_3))(or (= (f5 c_0 c_1 c_1) c_0)(= (f5 c_0 c_1 c_1) c_1)(= (f5 c_0 c_1 c_1) c_2)(= (f5 c_0 c_1 c_1) c_3))(or (= (f5 c_0 c_1 c_2) c_0)(= (f5 c_0 c_1 c_2) c_1)(= (f5 c_0 c_1 c_2) c_2)(= (f5 c_0 c_1 c_2) c_3))(or (= (f5 c_0 c_1 c_3) c_0)(= (f5 c_0 c_1 c_3) c_1)(= (f5 c_0 c_1 c_3) c_2)(= (f5 c_0 c_1 c_3) c_3))(or (= (f5 c_0 c_2 c_0) c_0)(= (f5 c_0 c_2 c_0) c_1)(= (f5 c_0 c_2 c_0) c_2)(= (f5 c_0 c_2 c_0) c_3))(or (= (f5 c_0 c_2 c_1) c_0)(= (f5 c_0 c_2 c_1) c_1)(= (f5 c_0 c_2 c_1) c_2)(= (f5 c_0 c_2 c_1) c_3))(or (= (f5 c_0 c_2 c_2) c_0)(= (f5 c_0 c_2 c_2) c_1)(= (f5 c_0 c_2 c_2) c_2)(= (f5 c_0 c_2 c_2) c_3))(or (= (f5 c_0 c_2 c_3) c_0)(= (f5 c_0 c_2 c_3) c_1)(= (f5 c_0 c_2 c_3) c_2)(= (f5 c_0 c_2 c_3) c_3))(or (= (f5 c_0 c_3 c_0) c_0)(= (f5 c_0 c_3 c_0) c_1)(= (f5 c_0 c_3 c_0) c_2)(= (f5 c_0 c_3 c_0) c_3))(or (= (f5 c_0 c_3 c_1) c_0)(= (f5 c_0 c_3 c_1) c_1)(= (f5 c_0 c_3 c_1) c_2)(= (f5 c_0 c_3 c_1) c_3))(or (= (f5 c_0 c_3 c_2) c_0)(= (f5 c_0 c_3 c_2) c_1)(= (f5 c_0 c_3 c_2) c_2)(= (f5 c_0 c_3 c_2) c_3))(or (= (f5 c_0 c_3 c_3) c_0)(= (f5 c_0 c_3 c_3) c_1)(= (f5 c_0 c_3 c_3) c_2)(= (f5 c_0 c_3 c_3) c_3))(or (= (f5 c_1 c_0 c_0) c_0)(= (f5 c_1 c_0 c_0) c_1)(= (f5 c_1 c_0 c_0) c_2)(= (f5 c_1 c_0 c_0) c_3))(or (= (f5 c_1 c_0 c_1) c_0)(= (f5 c_1 c_0 c_1) c_1)(= (f5 c_1 c_0 c_1) c_2)(= (f5 c_1 c_0 c_1) c_3))(or (= (f5 c_1 c_0 c_2) c_0)(= (f5 c_1 c_0 c_2) c_1)(= (f5 c_1 c_0 c_2) c_2)(= (f5 c_1 c_0 c_2) c_3))(or (= (f5 c_1 c_0 c_3) c_0)(= (f5 c_1 c_0 c_3) c_1)(= (f5 c_1 c_0 c_3) c_2)(= (f5 c_1 c_0 c_3) c_3))(or (= (f5 c_1 c_1 c_0) c_0)(= (f5 c_1 c_1 c_0) c_1)(= (f5 c_1 c_1 c_0) c_2)(= (f5 c_1 c_1 c_0) c_3))(or (= (f5 c_1 c_1 c_1) c_0)(= (f5 c_1 c_1 c_1) c_1)(= (f5 c_1 c_1 c_1) c_2)(= (f5 c_1 c_1 c_1) c_3))(or (= (f5 c_1 c_1 c_2) c_0)(= (f5 c_1 c_1 c_2) c_1)(= (f5 c_1 c_1 c_2) c_2)(= (f5 c_1 c_1 c_2) c_3))(or (= (f5 c_1 c_1 c_3) c_0)(= (f5 c_1 c_1 c_3) c_1)(= (f5 c_1 c_1 c_3) c_2)(= (f5 c_1 c_1 c_3) c_3))(or (= (f5 c_1 c_2 c_0) c_0)(= (f5 c_1 c_2 c_0) c_1)(= (f5 c_1 c_2 c_0) c_2)(= (f5 c_1 c_2 c_0) c_3))(or (= (f5 c_1 c_2 c_1) c_0)(= (f5 c_1 c_2 c_1) c_1)(= (f5 c_1 c_2 c_1) c_2)(= (f5 c_1 c_2 c_1) c_3))(or (= (f5 c_1 c_2 c_2) c_0)(= (f5 c_1 c_2 c_2) c_1)(= (f5 c_1 c_2 c_2) c_2)(= (f5 c_1 c_2 c_2) c_3))(or (= (f5 c_1 c_2 c_3) c_0)(= (f5 c_1 c_2 c_3) c_1)(= (f5 c_1 c_2 c_3) c_2)(= (f5 c_1 c_2 c_3) c_3))(or (= (f5 c_1 c_3 c_0) c_0)(= (f5 c_1 c_3 c_0) c_1)(= (f5 c_1 c_3 c_0) c_2)(= (f5 c_1 c_3 c_0) c_3))(or (= (f5 c_1 c_3 c_1) c_0)(= (f5 c_1 c_3 c_1) c_1)(= (f5 c_1 c_3 c_1) c_2)(= (f5 c_1 c_3 c_1) c_3))(or (= (f5 c_1 c_3 c_2) c_0)(= (f5 c_1 c_3 c_2) c_1)(= (f5 c_1 c_3 c_2) c_2)(= (f5 c_1 c_3 c_2) c_3))(or (= (f5 c_1 c_3 c_3) c_0)(= (f5 c_1 c_3 c_3) c_1)(= (f5 c_1 c_3 c_3) c_2)(= (f5 c_1 c_3 c_3) c_3))(or (= (f5 c_2 c_0 c_0) c_0)(= (f5 c_2 c_0 c_0) c_1)(= (f5 c_2 c_0 c_0) c_2)(= (f5 c_2 c_0 c_0) c_3))(or (= (f5 c_2 c_0 c_1) c_0)(= (f5 c_2 c_0 c_1) c_1)(= (f5 c_2 c_0 c_1) c_2)(= (f5 c_2 c_0 c_1) c_3))(or (= (f5 c_2 c_0 c_2) c_0)(= (f5 c_2 c_0 c_2) c_1)(= (f5 c_2 c_0 c_2) c_2)(= (f5 c_2 c_0 c_2) c_3))(or (= (f5 c_2 c_0 c_3) c_0)(= (f5 c_2 c_0 c_3) c_1)(= (f5 c_2 c_0 c_3) c_2)(= (f5 c_2 c_0 c_3) c_3))(or (= (f5 c_2 c_1 c_0) c_0)(= (f5 c_2 c_1 c_0) c_1)(= (f5 c_2 c_1 c_0) c_2)(= (f5 c_2 c_1 c_0) c_3))(or (= (f5 c_2 c_1 c_1) c_0)(= (f5 c_2 c_1 c_1) c_1)(= (f5 c_2 c_1 c_1) c_2)(= (f5 c_2 c_1 c_1) c_3))(or (= (f5 c_2 c_1 c_2) c_0)(= (f5 c_2 c_1 c_2) c_1)(= (f5 c_2 c_1 c_2) c_2)(= (f5 c_2 c_1 c_2) c_3))(or (= (f5 c_2 c_1 c_3) c_0)(= (f5 c_2 c_1 c_3) c_1)(= (f5 c_2 c_1 c_3) c_2)(= (f5 c_2 c_1 c_3) c_3))(or (= (f5 c_2 c_2 c_0) c_0)(= (f5 c_2 c_2 c_0) c_1)(= (f5 c_2 c_2 c_0) c_2)(= (f5 c_2 c_2 c_0) c_3))(or (= (f5 c_2 c_2 c_1) c_0)(= (f5 c_2 c_2 c_1) c_1)(= (f5 c_2 c_2 c_1) c_2)(= (f5 c_2 c_2 c_1) c_3))(or (= (f5 c_2 c_2 c_2) c_0)(= (f5 c_2 c_2 c_2) c_1)(= (f5 c_2 c_2 c_2) c_2)(= (f5 c_2 c_2 c_2) c_3))(or (= (f5 c_2 c_2 c_3) c_0)(= (f5 c_2 c_2 c_3) c_1)(= (f5 c_2 c_2 c_3) c_2)(= (f5 c_2 c_2 c_3) c_3))(or (= (f5 c_2 c_3 c_0) c_0)(= (f5 c_2 c_3 c_0) c_1)(= (f5 c_2 c_3 c_0) c_2)(= (f5 c_2 c_3 c_0) c_3))(or (= (f5 c_2 c_3 c_1) c_0)(= (f5 c_2 c_3 c_1) c_1)(= (f5 c_2 c_3 c_1) c_2)(= (f5 c_2 c_3 c_1) c_3))(or (= (f5 c_2 c_3 c_2) c_0)(= (f5 c_2 c_3 c_2) c_1)(= (f5 c_2 c_3 c_2) c_2)(= (f5 c_2 c_3 c_2) c_3))(or (= (f5 c_2 c_3 c_3) c_0)(= (f5 c_2 c_3 c_3) c_1)(= (f5 c_2 c_3 c_3) c_2)(= (f5 c_2 c_3 c_3) c_3))(or (= (f5 c_3 c_0 c_0) c_0)(= (f5 c_3 c_0 c_0) c_1)(= (f5 c_3 c_0 c_0) c_2)(= (f5 c_3 c_0 c_0) c_3))(or (= (f5 c_3 c_0 c_1) c_0)(= (f5 c_3 c_0 c_1) c_1)(= (f5 c_3 c_0 c_1) c_2)(= (f5 c_3 c_0 c_1) c_3))(or (= (f5 c_3 c_0 c_2) c_0)(= (f5 c_3 c_0 c_2) c_1)(= (f5 c_3 c_0 c_2) c_2)(= (f5 c_3 c_0 c_2) c_3))(or (= (f5 c_3 c_0 c_3) c_0)(= (f5 c_3 c_0 c_3) c_1)(= (f5 c_3 c_0 c_3) c_2)(= (f5 c_3 c_0 c_3) c_3))(or (= (f5 c_3 c_1 c_0) c_0)(= (f5 c_3 c_1 c_0) c_1)(= (f5 c_3 c_1 c_0) c_2)(= (f5 c_3 c_1 c_0) c_3))(or (= (f5 c_3 c_1 c_1) c_0)(= (f5 c_3 c_1 c_1) c_1)(= (f5 c_3 c_1 c_1) c_2)(= (f5 c_3 c_1 c_1) c_3))(or (= (f5 c_3 c_1 c_2) c_0)(= (f5 c_3 c_1 c_2) c_1)(= (f5 c_3 c_1 c_2) c_2)(= (f5 c_3 c_1 c_2) c_3))(or (= (f5 c_3 c_1 c_3) c_0)(= (f5 c_3 c_1 c_3) c_1)(= (f5 c_3 c_1 c_3) c_2)(= (f5 c_3 c_1 c_3) c_3))(or (= (f5 c_3 c_2 c_0) c_0)(= (f5 c_3 c_2 c_0) c_1)(= (f5 c_3 c_2 c_0) c_2)(= (f5 c_3 c_2 c_0) c_3))(or (= (f5 c_3 c_2 c_1) c_0)(= (f5 c_3 c_2 c_1) c_1)(= (f5 c_3 c_2 c_1) c_2)(= (f5 c_3 c_2 c_1) c_3))(or (= (f5 c_3 c_2 c_2) c_0)(= (f5 c_3 c_2 c_2) c_1)(= (f5 c_3 c_2 c_2) c_2)(= (f5 c_3 c_2 c_2) c_3))(or (= (f5 c_3 c_2 c_3) c_0)(= (f5 c_3 c_2 c_3) c_1)(= (f5 c_3 c_2 c_3) c_2)(= (f5 c_3 c_2 c_3) c_3))(or (= (f5 c_3 c_3 c_0) c_0)(= (f5 c_3 c_3 c_0) c_1)(= (f5 c_3 c_3 c_0) c_2)(= (f5 c_3 c_3 c_0) c_3))(or (= (f5 c_3 c_3 c_1) c_0)(= (f5 c_3 c_3 c_1) c_1)(= (f5 c_3 c_3 c_1) c_2)(= (f5 c_3 c_3 c_1) c_3))(or (= (f5 c_3 c_3 c_2) c_0)(= (f5 c_3 c_3 c_2) c_1)(= (f5 c_3 c_3 c_2) c_2)(= (f5 c_3 c_3 c_2) c_3))(or (= (f5 c_3 c_3 c_3) c_0)(= (f5 c_3 c_3 c_3) c_1)(= (f5 c_3 c_3 c_3) c_2)(= (f5 c_3 c_3 c_3) c_3))(or (= (f3 c_0 c_0) c_0)(= (f3 c_0 c_0) c_1)(= (f3 c_0 c_0) c_2)(= (f3 c_0 c_0) c_3))(or (= (f3 c_0 c_1) c_0)(= (f3 c_0 c_1) c_1)(= (f3 c_0 c_1) c_2)(= (f3 c_0 c_1) c_3))(or (= (f3 c_0 c_2) c_0)(= (f3 c_0 c_2) c_1)(= (f3 c_0 c_2) c_2)(= (f3 c_0 c_2) c_3))(or (= (f3 c_0 c_3) c_0)(= (f3 c_0 c_3) c_1)(= (f3 c_0 c_3) c_2)(= (f3 c_0 c_3) c_3))(or (= (f3 c_1 c_0) c_0)(= (f3 c_1 c_0) c_1)(= (f3 c_1 c_0) c_2)(= (f3 c_1 c_0) c_3))(or (= (f3 c_1 c_1) c_0)(= (f3 c_1 c_1) c_1)(= (f3 c_1 c_1) c_2)(= (f3 c_1 c_1) c_3))(or (= (f3 c_1 c_2) c_0)(= (f3 c_1 c_2) c_1)(= (f3 c_1 c_2) c_2)(= (f3 c_1 c_2) c_3))(or (= (f3 c_1 c_3) c_0)(= (f3 c_1 c_3) c_1)(= (f3 c_1 c_3) c_2)(= (f3 c_1 c_3) c_3))(or (= (f3 c_2 c_0) c_0)(= (f3 c_2 c_0) c_1)(= (f3 c_2 c_0) c_2)(= (f3 c_2 c_0) c_3))(or (= (f3 c_2 c_1) c_0)(= (f3 c_2 c_1) c_1)(= (f3 c_2 c_1) c_2)(= (f3 c_2 c_1) c_3))(or (= (f3 c_2 c_2) c_0)(= (f3 c_2 c_2) c_1)(= (f3 c_2 c_2) c_2)(= (f3 c_2 c_2) c_3))(or (= (f3 c_2 c_3) c_0)(= (f3 c_2 c_3) c_1)(= (f3 c_2 c_3) c_2)(= (f3 c_2 c_3) c_3))(or (= (f3 c_3 c_0) c_0)(= (f3 c_3 c_0) c_1)(= (f3 c_3 c_0) c_2)(= (f3 c_3 c_0) c_3))(or (= (f3 c_3 c_1) c_0)(= (f3 c_3 c_1) c_1)(= (f3 c_3 c_1) c_2)(= (f3 c_3 c_1) c_3))(or (= (f3 c_3 c_2) c_0)(= (f3 c_3 c_2) c_1)(= (f3 c_3 c_2) c_2)(= (f3 c_3 c_2) c_3))(or (= (f3 c_3 c_3) c_0)(= (f3 c_3 c_3) c_1)(= (f3 c_3 c_3) c_2)(= (f3 c_3 c_3) c_3))(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))(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))(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))(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))(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))(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))(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))(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))(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))(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))(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))(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))(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))(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))(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))(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))(or (= (f4 c_0) c_0)(= (f4 c_0) c_1)(= (f4 c_0) c_2)(= (f4 c_0) c_3))(or (= (f4 c_1) c_0)(= (f4 c_1) c_1)(= (f4 c_1) c_2)(= (f4 c_1) c_3))(or (= (f4 c_2) c_0)(= (f4 c_2) c_1)(= (f4 c_2) c_2)(= (f4 c_2) c_3))(or (= (f4 c_3) c_0)(= (f4 c_3) c_1)(= (f4 c_3) c_2)(= (f4 c_3) c_3))(or (= c2 c_0)(= c2 c_1)(= c2 c_2)(= c2 c_3))(or (= c6 c_0)(= c6 c_1)(= c6 c_2)(= c6 c_3))(or (= c7 c_0)(= c7 c_1)(= c7 c_2)(= c7 c_3))(or (= c8 c_0)(= c8 c_1)(= c8 c_2)(= c8 c_3))))