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

This benchmark was obtained by trying to find a finite model of a first-order 
formula (Albert Oliveras).
}
:status unsat
:logic QF_UF
:extrafuns ((f1 U U U))
:extrapreds ((p2 U U U))
:extrafuns ((c3 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))
:formula 
( and 
( distinct c_0 c_1 c_2 c_3 c_4 )(not (= c_0 (f1 c_0 c_0))) (not (= c_0 (f1 c_1 c_0))) (not (= c_0 (f1 c_2 c_0))) (not (= c_0 (f1 c_3 c_0))) (not (= c_0 (f1 c_4 c_0))) (not (= c_1 (f1 c_0 c_1))) (not (= c_1 (f1 c_1 c_1))) (not (= c_1 (f1 c_2 c_1))) (not (= c_1 (f1 c_3 c_1))) (not (= c_1 (f1 c_4 c_1))) (not (= c_2 (f1 c_0 c_2))) (not (= c_2 (f1 c_1 c_2))) (not (= c_2 (f1 c_2 c_2))) (not (= c_2 (f1 c_3 c_2))) (not (= c_2 (f1 c_4 c_2))) (not (= c_3 (f1 c_0 c_3))) (not (= c_3 (f1 c_1 c_3))) (not (= c_3 (f1 c_2 c_3))) (not (= c_3 (f1 c_3 c_3))) (not (= c_3 (f1 c_4 c_3))) (not (= c_4 (f1 c_0 c_4))) (not (= c_4 (f1 c_1 c_4))) (not (= c_4 (f1 c_2 c_4))) (not (= c_4 (f1 c_3 c_4))) (not (= c_4 (f1 c_4 c_4))) (or (p2 c_0 c_0 c_0) (= c_0 c_0) (not (p2 c_0 c_0 c_0)) (= c_0 c_0) (= c_0 c_0) (not (p2 c_0 c_0 c_0)) )(or (p2 c_0 c_0 c_0) (= c_1 c_0) (not (p2 c_0 c_1 c_0)) (= c_0 c_1) (= c_0 c_1) (not (p2 c_0 c_0 c_1)) )(or (p2 c_0 c_0 c_0) (= c_2 c_0) (not (p2 c_0 c_2 c_0)) (= c_0 c_2) (= c_0 c_2) (not (p2 c_0 c_0 c_2)) )(or (p2 c_0 c_0 c_0) (= c_3 c_0) (not (p2 c_0 c_3 c_0)) (= c_0 c_3) (= c_0 c_3) (not (p2 c_0 c_0 c_3)) )(or (p2 c_0 c_0 c_0) (= c_4 c_0) (not (p2 c_0 c_4 c_0)) (= c_0 c_4) (= c_0 c_4) (not (p2 c_0 c_0 c_4)) )(or (p2 c_0 c_0 c_1) (= c_0 c_1) (not (p2 c_0 c_0 c_1)) (= c_0 c_0) (= c_0 c_0) (not (p2 c_0 c_0 c_0)) )(or (p2 c_0 c_0 c_1) (= c_1 c_1) (not (p2 c_0 c_1 c_1)) (= c_0 c_1) (= c_0 c_1) (not (p2 c_0 c_0 c_1)) )(or (p2 c_0 c_0 c_1) (= c_2 c_1) (not (p2 c_0 c_2 c_1)) (= c_0 c_2) (= c_0 c_2) (not (p2 c_0 c_0 c_2)) )(or (p2 c_0 c_0 c_1) (= c_3 c_1) (not (p2 c_0 c_3 c_1)) (= c_0 c_3) (= c_0 c_3) (not (p2 c_0 c_0 c_3)) )(or (p2 c_0 c_0 c_1) (= c_4 c_1) (not (p2 c_0 c_4 c_1)) (= c_0 c_4) (= c_0 c_4) (not (p2 c_0 c_0 c_4)) )(or (p2 c_0 c_0 c_2) (= c_0 c_2) (not (p2 c_0 c_0 c_2)) (= c_0 c_0) (= c_0 c_0) (not (p2 c_0 c_0 c_0)) )(or (p2 c_0 c_0 c_2) (= c_1 c_2) (not (p2 c_0 c_1 c_2)) (= c_0 c_1) (= c_0 c_1) (not (p2 c_0 c_0 c_1)) )(or (p2 c_0 c_0 c_2) (= c_2 c_2) (not (p2 c_0 c_2 c_2)) (= c_0 c_2) (= c_0 c_2) (not (p2 c_0 c_0 c_2)) )(or (p2 c_0 c_0 c_2) (= c_3 c_2) (not (p2 c_0 c_3 c_2)) (= c_0 c_3) (= c_0 c_3) (not (p2 c_0 c_0 c_3)) )(or (p2 c_0 c_0 c_2) (= c_4 c_2) (not (p2 c_0 c_4 c_2)) (= c_0 c_4) (= c_0 c_4) (not (p2 c_0 c_0 c_4)) )(or (p2 c_0 c_0 c_3) (= c_0 c_3) (not (p2 c_0 c_0 c_3)) (= c_0 c_0) (= c_0 c_0) (not (p2 c_0 c_0 c_0)) )(or (p2 c_0 c_0 c_3) (= c_1 c_3) (not (p2 c_0 c_1 c_3)) (= c_0 c_1) (= c_0 c_1) (not (p2 c_0 c_0 c_1)) )(or (p2 c_0 c_0 c_3) (= c_2 c_3) (not (p2 c_0 c_2 c_3)) (= c_0 c_2) (= c_0 c_2) (not (p2 c_0 c_0 c_2)) )(or (p2 c_0 c_0 c_3) (= c_3 c_3) (not (p2 c_0 c_3 c_3)) (= c_0 c_3) (= c_0 c_3) (not (p2 c_0 c_0 c_3)) )(or (p2 c_0 c_0 c_3) (= c_4 c_3) (not (p2 c_0 c_4 c_3)) (= c_0 c_4) (= c_0 c_4) (not (p2 c_0 c_0 c_4)) )(or (p2 c_0 c_0 c_4) (= c_0 c_4) (not (p2 c_0 c_0 c_4)) (= c_0 c_0) (= c_0 c_0) (not (p2 c_0 c_0 c_0)) )(or (p2 c_0 c_0 c_4) (= c_1 c_4) (not (p2 c_0 c_1 c_4)) (= c_0 c_1) (= c_0 c_1) (not (p2 c_0 c_0 c_1)) )(or (p2 c_0 c_0 c_4) (= c_2 c_4) (not (p2 c_0 c_2 c_4)) (= c_0 c_2) (= c_0 c_2) (not (p2 c_0 c_0 c_2)) )(or (p2 c_0 c_0 c_4) (= c_3 c_4) (not (p2 c_0 c_3 c_4)) (= c_0 c_3) (= c_0 c_3) (not (p2 c_0 c_0 c_3)) )(or (p2 c_0 c_0 c_4) (= c_4 c_4) (not (p2 c_0 c_4 c_4)) (= c_0 c_4) (= c_0 c_4) (not (p2 c_0 c_0 c_4)) )(or (p2 c_0 c_1 c_0) (= c_0 c_0) (not (p2 c_1 c_0 c_0)) (= c_1 c_0) (= c_0 c_0) (not (p2 c_0 c_1 c_0)) )(or (p2 c_0 c_1 c_0) (= c_1 c_0) (not (p2 c_1 c_1 c_0)) (= c_1 c_1) (= c_0 c_1) (not (p2 c_0 c_1 c_1)) )(or (p2 c_0 c_1 c_0) (= c_2 c_0) (not (p2 c_1 c_2 c_0)) (= c_1 c_2) (= c_0 c_2) (not (p2 c_0 c_1 c_2)) )(or (p2 c_0 c_1 c_0) (= c_3 c_0) (not (p2 c_1 c_3 c_0)) (= c_1 c_3) (= c_0 c_3) (not (p2 c_0 c_1 c_3)) )(or (p2 c_0 c_1 c_0) (= c_4 c_0) (not (p2 c_1 c_4 c_0)) (= c_1 c_4) (= c_0 c_4) (not (p2 c_0 c_1 c_4)) )(or (p2 c_0 c_1 c_1) (= c_0 c_1) (not (p2 c_1 c_0 c_1)) (= c_1 c_0) (= c_0 c_0) (not (p2 c_0 c_1 c_0)) )(or (p2 c_0 c_1 c_1) (= c_1 c_1) (not (p2 c_1 c_1 c_1)) (= c_1 c_1) (= c_0 c_1) (not (p2 c_0 c_1 c_1)) )(or (p2 c_0 c_1 c_1) (= c_2 c_1) (not (p2 c_1 c_2 c_1)) (= c_1 c_2) (= c_0 c_2) (not (p2 c_0 c_1 c_2)) )(or (p2 c_0 c_1 c_1) (= c_3 c_1) (not (p2 c_1 c_3 c_1)) (= c_1 c_3) (= c_0 c_3) (not (p2 c_0 c_1 c_3)) )(or (p2 c_0 c_1 c_1) (= c_4 c_1) (not (p2 c_1 c_4 c_1)) (= c_1 c_4) (= c_0 c_4) (not (p2 c_0 c_1 c_4)) )(or (p2 c_0 c_1 c_2) (= c_0 c_2) (not (p2 c_1 c_0 c_2)) (= c_1 c_0) (= c_0 c_0) (not (p2 c_0 c_1 c_0)) )(or (p2 c_0 c_1 c_2) (= c_1 c_2) (not (p2 c_1 c_1 c_2)) (= c_1 c_1) (= c_0 c_1) (not (p2 c_0 c_1 c_1)) )(or (p2 c_0 c_1 c_2) (= c_2 c_2) (not (p2 c_1 c_2 c_2)) (= c_1 c_2) (= c_0 c_2) (not (p2 c_0 c_1 c_2)) )(or (p2 c_0 c_1 c_2) (= c_3 c_2) (not (p2 c_1 c_3 c_2)) (= c_1 c_3) (= c_0 c_3) (not (p2 c_0 c_1 c_3)) )(or (p2 c_0 c_1 c_2) (= c_4 c_2) (not (p2 c_1 c_4 c_2)) (= c_1 c_4) (= c_0 c_4) (not (p2 c_0 c_1 c_4)) )(or (p2 c_0 c_1 c_3) (= c_0 c_3) (not (p2 c_1 c_0 c_3)) (= c_1 c_0) (= c_0 c_0) (not (p2 c_0 c_1 c_0)) )(or (p2 c_0 c_1 c_3) (= c_1 c_3) (not (p2 c_1 c_1 c_3)) (= c_1 c_1) (= c_0 c_1) (not (p2 c_0 c_1 c_1)) )(or (p2 c_0 c_1 c_3) (= c_2 c_3) (not (p2 c_1 c_2 c_3)) (= c_1 c_2) (= c_0 c_2) (not (p2 c_0 c_1 c_2)) )(or (p2 c_0 c_1 c_3) (= c_3 c_3) (not (p2 c_1 c_3 c_3)) (= c_1 c_3) (= c_0 c_3) (not (p2 c_0 c_1 c_3)) )(or (p2 c_0 c_1 c_3) (= c_4 c_3) (not (p2 c_1 c_4 c_3)) (= c_1 c_4) (= c_0 c_4) (not (p2 c_0 c_1 c_4)) )(or (p2 c_0 c_1 c_4) (= c_0 c_4) (not (p2 c_1 c_0 c_4)) (= c_1 c_0) (= c_0 c_0) (not (p2 c_0 c_1 c_0)) )(or (p2 c_0 c_1 c_4) (= c_1 c_4) (not (p2 c_1 c_1 c_4)) (= c_1 c_1) (= c_0 c_1) (not (p2 c_0 c_1 c_1)) )(or (p2 c_0 c_1 c_4) (= c_2 c_4) (not (p2 c_1 c_2 c_4)) (= c_1 c_2) (= c_0 c_2) (not (p2 c_0 c_1 c_2)) )(or (p2 c_0 c_1 c_4) (= c_3 c_4) (not (p2 c_1 c_3 c_4)) (= c_1 c_3) (= c_0 c_3) (not (p2 c_0 c_1 c_3)) )(or (p2 c_0 c_1 c_4) (= c_4 c_4) (not (p2 c_1 c_4 c_4)) (= c_1 c_4) (= c_0 c_4) (not (p2 c_0 c_1 c_4)) )(or (p2 c_0 c_2 c_0) (= c_0 c_0) (not (p2 c_2 c_0 c_0)) (= c_2 c_0) (= c_0 c_0) (not (p2 c_0 c_2 c_0)) )(or (p2 c_0 c_2 c_0) (= c_1 c_0) (not (p2 c_2 c_1 c_0)) (= c_2 c_1) (= c_0 c_1) (not (p2 c_0 c_2 c_1)) )(or (p2 c_0 c_2 c_0) (= c_2 c_0) (not (p2 c_2 c_2 c_0)) (= c_2 c_2) (= c_0 c_2) (not (p2 c_0 c_2 c_2)) )(or (p2 c_0 c_2 c_0) (= c_3 c_0) (not (p2 c_2 c_3 c_0)) (= c_2 c_3) (= c_0 c_3) (not (p2 c_0 c_2 c_3)) )(or (p2 c_0 c_2 c_0) (= c_4 c_0) (not (p2 c_2 c_4 c_0)) (= c_2 c_4) (= c_0 c_4) (not (p2 c_0 c_2 c_4)) )(or (p2 c_0 c_2 c_1) (= c_0 c_1) (not (p2 c_2 c_0 c_1)) (= c_2 c_0) (= c_0 c_0) (not (p2 c_0 c_2 c_0)) )(or (p2 c_0 c_2 c_1) (= c_1 c_1) (not (p2 c_2 c_1 c_1)) (= c_2 c_1) (= c_0 c_1) (not (p2 c_0 c_2 c_1)) )(or (p2 c_0 c_2 c_1) (= c_2 c_1) (not (p2 c_2 c_2 c_1)) (= c_2 c_2) (= c_0 c_2) (not (p2 c_0 c_2 c_2)) )(or (p2 c_0 c_2 c_1) (= c_3 c_1) (not (p2 c_2 c_3 c_1)) (= c_2 c_3) (= c_0 c_3) (not (p2 c_0 c_2 c_3)) )(or (p2 c_0 c_2 c_1) (= c_4 c_1) (not (p2 c_2 c_4 c_1)) (= c_2 c_4) (= c_0 c_4) (not (p2 c_0 c_2 c_4)) )(or (p2 c_0 c_2 c_2) (= c_0 c_2) (not (p2 c_2 c_0 c_2)) (= c_2 c_0) (= c_0 c_0) (not (p2 c_0 c_2 c_0)) )(or (p2 c_0 c_2 c_2) (= c_1 c_2) (not (p2 c_2 c_1 c_2)) (= c_2 c_1) (= c_0 c_1) (not (p2 c_0 c_2 c_1)) )(or (p2 c_0 c_2 c_2) (= c_2 c_2) (not (p2 c_2 c_2 c_2)) (= c_2 c_2) (= c_0 c_2) (not (p2 c_0 c_2 c_2)) )(or (p2 c_0 c_2 c_2) (= c_3 c_2) (not (p2 c_2 c_3 c_2)) (= c_2 c_3) (= c_0 c_3) (not (p2 c_0 c_2 c_3)) )(or (p2 c_0 c_2 c_2) (= c_4 c_2) (not (p2 c_2 c_4 c_2)) (= c_2 c_4) (= c_0 c_4) (not (p2 c_0 c_2 c_4)) )(or (p2 c_0 c_2 c_3) (= c_0 c_3) (not (p2 c_2 c_0 c_3)) (= c_2 c_0) (= c_0 c_0) (not (p2 c_0 c_2 c_0)) )(or (p2 c_0 c_2 c_3) (= c_1 c_3) (not (p2 c_2 c_1 c_3)) (= c_2 c_1) (= c_0 c_1) (not (p2 c_0 c_2 c_1)) )(or (p2 c_0 c_2 c_3) (= c_2 c_3) (not (p2 c_2 c_2 c_3)) (= c_2 c_2) (= c_0 c_2) (not (p2 c_0 c_2 c_2)) )(or (p2 c_0 c_2 c_3) (= c_3 c_3) (not (p2 c_2 c_3 c_3)) (= c_2 c_3) (= c_0 c_3) (not (p2 c_0 c_2 c_3)) )(or (p2 c_0 c_2 c_3) (= c_4 c_3) (not (p2 c_2 c_4 c_3)) (= c_2 c_4) (= c_0 c_4) (not (p2 c_0 c_2 c_4)) )(or (p2 c_0 c_2 c_4) (= c_0 c_4) (not (p2 c_2 c_0 c_4)) (= c_2 c_0) (= c_0 c_0) (not (p2 c_0 c_2 c_0)) )(or (p2 c_0 c_2 c_4) (= c_1 c_4) (not (p2 c_2 c_1 c_4)) (= c_2 c_1) (= c_0 c_1) (not (p2 c_0 c_2 c_1)) )(or (p2 c_0 c_2 c_4) (= c_2 c_4) (not (p2 c_2 c_2 c_4)) (= c_2 c_2) (= c_0 c_2) (not (p2 c_0 c_2 c_2)) )(or (p2 c_0 c_2 c_4) (= c_3 c_4) (not (p2 c_2 c_3 c_4)) (= c_2 c_3) (= c_0 c_3) (not (p2 c_0 c_2 c_3)) )(or (p2 c_0 c_2 c_4) (= c_4 c_4) (not (p2 c_2 c_4 c_4)) (= c_2 c_4) (= c_0 c_4) (not (p2 c_0 c_2 c_4)) )(or (p2 c_0 c_3 c_0) (= c_0 c_0) (not (p2 c_3 c_0 c_0)) (= c_3 c_0) (= c_0 c_0) (not (p2 c_0 c_3 c_0)) )(or (p2 c_0 c_3 c_0) (= c_1 c_0) (not (p2 c_3 c_1 c_0)) (= c_3 c_1) (= c_0 c_1) (not (p2 c_0 c_3 c_1)) )(or (p2 c_0 c_3 c_0) (= c_2 c_0) (not (p2 c_3 c_2 c_0)) (= c_3 c_2) (= c_0 c_2) (not (p2 c_0 c_3 c_2)) )(or (p2 c_0 c_3 c_0) (= c_3 c_0) (not (p2 c_3 c_3 c_0)) (= c_3 c_3) (= c_0 c_3) (not (p2 c_0 c_3 c_3)) )(or (p2 c_0 c_3 c_0) (= c_4 c_0) (not (p2 c_3 c_4 c_0)) (= c_3 c_4) (= c_0 c_4) (not (p2 c_0 c_3 c_4)) )(or (p2 c_0 c_3 c_1) (= c_0 c_1) (not (p2 c_3 c_0 c_1)) (= c_3 c_0) (= c_0 c_0) (not (p2 c_0 c_3 c_0)) )(or (p2 c_0 c_3 c_1) (= c_1 c_1) (not (p2 c_3 c_1 c_1)) (= c_3 c_1) (= c_0 c_1) (not (p2 c_0 c_3 c_1)) )(or (p2 c_0 c_3 c_1) (= c_2 c_1) (not (p2 c_3 c_2 c_1)) (= c_3 c_2) (= c_0 c_2) (not (p2 c_0 c_3 c_2)) )(or (p2 c_0 c_3 c_1) (= c_3 c_1) (not (p2 c_3 c_3 c_1)) (= c_3 c_3) (= c_0 c_3) (not (p2 c_0 c_3 c_3)) )(or (p2 c_0 c_3 c_1) (= c_4 c_1) (not (p2 c_3 c_4 c_1)) (= c_3 c_4) (= c_0 c_4) (not (p2 c_0 c_3 c_4)) )(or (p2 c_0 c_3 c_2) (= c_0 c_2) (not (p2 c_3 c_0 c_2)) (= c_3 c_0) (= c_0 c_0) (not (p2 c_0 c_3 c_0)) )(or (p2 c_0 c_3 c_2) (= c_1 c_2) (not (p2 c_3 c_1 c_2)) (= c_3 c_1) (= c_0 c_1) (not (p2 c_0 c_3 c_1)) )(or (p2 c_0 c_3 c_2) (= c_2 c_2) (not (p2 c_3 c_2 c_2)) (= c_3 c_2) (= c_0 c_2) (not (p2 c_0 c_3 c_2)) )(or (p2 c_0 c_3 c_2) (= c_3 c_2) (not (p2 c_3 c_3 c_2)) (= c_3 c_3) (= c_0 c_3) (not (p2 c_0 c_3 c_3)) )(or (p2 c_0 c_3 c_2) (= c_4 c_2) (not (p2 c_3 c_4 c_2)) (= c_3 c_4) (= c_0 c_4) (not (p2 c_0 c_3 c_4)) )(or (p2 c_0 c_3 c_3) (= c_0 c_3) (not (p2 c_3 c_0 c_3)) (= c_3 c_0) (= c_0 c_0) (not (p2 c_0 c_3 c_0)) )(or (p2 c_0 c_3 c_3) (= c_1 c_3) (not (p2 c_3 c_1 c_3)) (= c_3 c_1) (= c_0 c_1) (not (p2 c_0 c_3 c_1)) )(or (p2 c_0 c_3 c_3) (= c_2 c_3) (not (p2 c_3 c_2 c_3)) (= c_3 c_2) (= c_0 c_2) (not (p2 c_0 c_3 c_2)) )(or (p2 c_0 c_3 c_3) (= c_3 c_3) (not (p2 c_3 c_3 c_3)) (= c_3 c_3) (= c_0 c_3) (not (p2 c_0 c_3 c_3)) )(or (p2 c_0 c_3 c_3) (= c_4 c_3) (not (p2 c_3 c_4 c_3)) (= c_3 c_4) (= c_0 c_4) (not (p2 c_0 c_3 c_4)) )(or (p2 c_0 c_3 c_4) (= c_0 c_4) (not (p2 c_3 c_0 c_4)) (= c_3 c_0) (= c_0 c_0) (not (p2 c_0 c_3 c_0)) )(or (p2 c_0 c_3 c_4) (= c_1 c_4) (not (p2 c_3 c_1 c_4)) (= c_3 c_1) (= c_0 c_1) (not (p2 c_0 c_3 c_1)) )(or (p2 c_0 c_3 c_4) (= c_2 c_4) (not (p2 c_3 c_2 c_4)) (= c_3 c_2) (= c_0 c_2) (not (p2 c_0 c_3 c_2)) )(or (p2 c_0 c_3 c_4) (= c_3 c_4) (not (p2 c_3 c_3 c_4)) (= c_3 c_3) (= c_0 c_3) (not (p2 c_0 c_3 c_3)) )(or (p2 c_0 c_3 c_4) (= c_4 c_4) (not (p2 c_3 c_4 c_4)) (= c_3 c_4) (= c_0 c_4) (not (p2 c_0 c_3 c_4)) )(or (p2 c_0 c_4 c_0) (= c_0 c_0) (not (p2 c_4 c_0 c_0)) (= c_4 c_0) (= c_0 c_0) (not (p2 c_0 c_4 c_0)) )(or (p2 c_0 c_4 c_0) (= c_1 c_0) (not (p2 c_4 c_1 c_0)) (= c_4 c_1) (= c_0 c_1) (not (p2 c_0 c_4 c_1)) )(or (p2 c_0 c_4 c_0) (= c_2 c_0) (not (p2 c_4 c_2 c_0)) (= c_4 c_2) (= c_0 c_2) (not (p2 c_0 c_4 c_2)) )(or (p2 c_0 c_4 c_0) (= c_3 c_0) (not (p2 c_4 c_3 c_0)) (= c_4 c_3) (= c_0 c_3) (not (p2 c_0 c_4 c_3)) )(or (p2 c_0 c_4 c_0) (= c_4 c_0) (not (p2 c_4 c_4 c_0)) (= c_4 c_4) (= c_0 c_4) (not (p2 c_0 c_4 c_4)) )(or (p2 c_0 c_4 c_1) (= c_0 c_1) (not (p2 c_4 c_0 c_1)) (= c_4 c_0) (= c_0 c_0) (not (p2 c_0 c_4 c_0)) )(or (p2 c_0 c_4 c_1) (= c_1 c_1) (not (p2 c_4 c_1 c_1)) (= c_4 c_1) (= c_0 c_1) (not (p2 c_0 c_4 c_1)) )(or (p2 c_0 c_4 c_1) (= c_2 c_1) (not (p2 c_4 c_2 c_1)) (= c_4 c_2) (= c_0 c_2) (not (p2 c_0 c_4 c_2)) )(or (p2 c_0 c_4 c_1) (= c_3 c_1) (not (p2 c_4 c_3 c_1)) (= c_4 c_3) (= c_0 c_3) (not (p2 c_0 c_4 c_3)) )(or (p2 c_0 c_4 c_1) (= c_4 c_1) (not (p2 c_4 c_4 c_1)) (= c_4 c_4) (= c_0 c_4) (not (p2 c_0 c_4 c_4)) )(or (p2 c_0 c_4 c_2) (= c_0 c_2) (not (p2 c_4 c_0 c_2)) (= c_4 c_0) (= c_0 c_0) (not (p2 c_0 c_4 c_0)) )(or (p2 c_0 c_4 c_2) (= c_1 c_2) (not (p2 c_4 c_1 c_2)) (= c_4 c_1) (= c_0 c_1) (not (p2 c_0 c_4 c_1)) )(or (p2 c_0 c_4 c_2) (= c_2 c_2) (not (p2 c_4 c_2 c_2)) (= c_4 c_2) (= c_0 c_2) (not (p2 c_0 c_4 c_2)) )(or (p2 c_0 c_4 c_2) (= c_3 c_2) (not (p2 c_4 c_3 c_2)) (= c_4 c_3) (= c_0 c_3) (not (p2 c_0 c_4 c_3)) )(or (p2 c_0 c_4 c_2) (= c_4 c_2) (not (p2 c_4 c_4 c_2)) (= c_4 c_4) (= c_0 c_4) (not (p2 c_0 c_4 c_4)) )(or (p2 c_0 c_4 c_3) (= c_0 c_3) (not (p2 c_4 c_0 c_3)) (= c_4 c_0) (= c_0 c_0) (not (p2 c_0 c_4 c_0)) )(or (p2 c_0 c_4 c_3) (= c_1 c_3) (not (p2 c_4 c_1 c_3)) (= c_4 c_1) (= c_0 c_1) (not (p2 c_0 c_4 c_1)) )(or (p2 c_0 c_4 c_3) (= c_2 c_3) (not (p2 c_4 c_2 c_3)) (= c_4 c_2) (= c_0 c_2) (not (p2 c_0 c_4 c_2)) )(or (p2 c_0 c_4 c_3) (= c_3 c_3) (not (p2 c_4 c_3 c_3)) (= c_4 c_3) (= c_0 c_3) (not (p2 c_0 c_4 c_3)) )(or (p2 c_0 c_4 c_3) (= c_4 c_3) (not (p2 c_4 c_4 c_3)) (= c_4 c_4) (= c_0 c_4) (not (p2 c_0 c_4 c_4)) )(or (p2 c_0 c_4 c_4) (= c_0 c_4) (not (p2 c_4 c_0 c_4)) (= c_4 c_0) (= c_0 c_0) (not (p2 c_0 c_4 c_0)) )(or (p2 c_0 c_4 c_4) (= c_1 c_4) (not (p2 c_4 c_1 c_4)) (= c_4 c_1) (= c_0 c_1) (not (p2 c_0 c_4 c_1)) )(or (p2 c_0 c_4 c_4) (= c_2 c_4) (not (p2 c_4 c_2 c_4)) (= c_4 c_2) (= c_0 c_2) (not (p2 c_0 c_4 c_2)) )(or (p2 c_0 c_4 c_4) (= c_3 c_4) (not (p2 c_4 c_3 c_4)) (= c_4 c_3) (= c_0 c_3) (not (p2 c_0 c_4 c_3)) )(or (p2 c_0 c_4 c_4) (= c_4 c_4) (not (p2 c_4 c_4 c_4)) (= c_4 c_4) (= c_0 c_4) (not (p2 c_0 c_4 c_4)) )(or (p2 c_1 c_0 c_0) (= c_0 c_0) (not (p2 c_0 c_0 c_0)) (= c_0 c_0) (= c_1 c_0) (not (p2 c_1 c_0 c_0)) )(or (p2 c_1 c_0 c_0) (= c_1 c_0) (not (p2 c_0 c_1 c_0)) (= c_0 c_1) (= c_1 c_1) (not (p2 c_1 c_0 c_1)) )(or (p2 c_1 c_0 c_0) (= c_2 c_0) (not (p2 c_0 c_2 c_0)) (= c_0 c_2) (= c_1 c_2) (not (p2 c_1 c_0 c_2)) )(or (p2 c_1 c_0 c_0) (= c_3 c_0) (not (p2 c_0 c_3 c_0)) (= c_0 c_3) (= c_1 c_3) (not (p2 c_1 c_0 c_3)) )(or (p2 c_1 c_0 c_0) (= c_4 c_0) (not (p2 c_0 c_4 c_0)) (= c_0 c_4) (= c_1 c_4) (not (p2 c_1 c_0 c_4)) )(or (p2 c_1 c_0 c_1) (= c_0 c_1) (not (p2 c_0 c_0 c_1)) (= c_0 c_0) (= c_1 c_0) (not (p2 c_1 c_0 c_0)) )(or (p2 c_1 c_0 c_1) (= c_1 c_1) (not (p2 c_0 c_1 c_1)) (= c_0 c_1) (= c_1 c_1) (not (p2 c_1 c_0 c_1)) )(or (p2 c_1 c_0 c_1) (= c_2 c_1) (not (p2 c_0 c_2 c_1)) (= c_0 c_2) (= c_1 c_2) (not (p2 c_1 c_0 c_2)) )(or (p2 c_1 c_0 c_1) (= c_3 c_1) (not (p2 c_0 c_3 c_1)) (= c_0 c_3) (= c_1 c_3) (not (p2 c_1 c_0 c_3)) )(or (p2 c_1 c_0 c_1) (= c_4 c_1) (not (p2 c_0 c_4 c_1)) (= c_0 c_4) (= c_1 c_4) (not (p2 c_1 c_0 c_4)) )(or (p2 c_1 c_0 c_2) (= c_0 c_2) (not (p2 c_0 c_0 c_2)) (= c_0 c_0) (= c_1 c_0) (not (p2 c_1 c_0 c_0)) )(or (p2 c_1 c_0 c_2) (= c_1 c_2) (not (p2 c_0 c_1 c_2)) (= c_0 c_1) (= c_1 c_1) (not (p2 c_1 c_0 c_1)) )(or (p2 c_1 c_0 c_2) (= c_2 c_2) (not (p2 c_0 c_2 c_2)) (= c_0 c_2) (= c_1 c_2) (not (p2 c_1 c_0 c_2)) )(or (p2 c_1 c_0 c_2) (= c_3 c_2) (not (p2 c_0 c_3 c_2)) (= c_0 c_3) (= c_1 c_3) (not (p2 c_1 c_0 c_3)) )(or (p2 c_1 c_0 c_2) (= c_4 c_2) (not (p2 c_0 c_4 c_2)) (= c_0 c_4) (= c_1 c_4) (not (p2 c_1 c_0 c_4)) )(or (p2 c_1 c_0 c_3) (= c_0 c_3) (not (p2 c_0 c_0 c_3)) (= c_0 c_0) (= c_1 c_0) (not (p2 c_1 c_0 c_0)) )(or (p2 c_1 c_0 c_3) (= c_1 c_3) (not (p2 c_0 c_1 c_3)) (= c_0 c_1) (= c_1 c_1) (not (p2 c_1 c_0 c_1)) )(or (p2 c_1 c_0 c_3) (= c_2 c_3) (not (p2 c_0 c_2 c_3)) (= c_0 c_2) (= c_1 c_2) (not (p2 c_1 c_0 c_2)) )(or (p2 c_1 c_0 c_3) (= c_3 c_3) (not (p2 c_0 c_3 c_3)) (= c_0 c_3) (= c_1 c_3) (not (p2 c_1 c_0 c_3)) )(or (p2 c_1 c_0 c_3) (= c_4 c_3) (not (p2 c_0 c_4 c_3)) (= c_0 c_4) (= c_1 c_4) (not (p2 c_1 c_0 c_4)) )(or (p2 c_1 c_0 c_4) (= c_0 c_4) (not (p2 c_0 c_0 c_4)) (= c_0 c_0) (= c_1 c_0) (not (p2 c_1 c_0 c_0)) )(or (p2 c_1 c_0 c_4) (= c_1 c_4) (not (p2 c_0 c_1 c_4)) (= c_0 c_1) (= c_1 c_1) (not (p2 c_1 c_0 c_1)) )(or (p2 c_1 c_0 c_4) (= c_2 c_4) (not (p2 c_0 c_2 c_4)) (= c_0 c_2) (= c_1 c_2) (not (p2 c_1 c_0 c_2)) )(or (p2 c_1 c_0 c_4) (= c_3 c_4) (not (p2 c_0 c_3 c_4)) (= c_0 c_3) (= c_1 c_3) (not (p2 c_1 c_0 c_3)) )(or (p2 c_1 c_0 c_4) (= c_4 c_4) (not (p2 c_0 c_4 c_4)) (= c_0 c_4) (= c_1 c_4) (not (p2 c_1 c_0 c_4)) )(or (p2 c_1 c_1 c_0) (= c_0 c_0) (not (p2 c_1 c_0 c_0)) (= c_1 c_0) (= c_1 c_0) (not (p2 c_1 c_1 c_0)) )(or (p2 c_1 c_1 c_0) (= c_1 c_0) (not (p2 c_1 c_1 c_0)) (= c_1 c_1) (= c_1 c_1) (not (p2 c_1 c_1 c_1)) )(or (p2 c_1 c_1 c_0) (= c_2 c_0) (not (p2 c_1 c_2 c_0)) (= c_1 c_2) (= c_1 c_2) (not (p2 c_1 c_1 c_2)) )(or (p2 c_1 c_1 c_0) (= c_3 c_0) (not (p2 c_1 c_3 c_0)) (= c_1 c_3) (= c_1 c_3) (not (p2 c_1 c_1 c_3)) )(or (p2 c_1 c_1 c_0) (= c_4 c_0) (not (p2 c_1 c_4 c_0)) (= c_1 c_4) (= c_1 c_4) (not (p2 c_1 c_1 c_4)) )(or (p2 c_1 c_1 c_1) (= c_0 c_1) (not (p2 c_1 c_0 c_1)) (= c_1 c_0) (= c_1 c_0) (not (p2 c_1 c_1 c_0)) )(or (p2 c_1 c_1 c_1) (= c_1 c_1) (not (p2 c_1 c_1 c_1)) (= c_1 c_1) (= c_1 c_1) (not (p2 c_1 c_1 c_1)) )(or (p2 c_1 c_1 c_1) (= c_2 c_1) (not (p2 c_1 c_2 c_1)) (= c_1 c_2) (= c_1 c_2) (not (p2 c_1 c_1 c_2)) )(or (p2 c_1 c_1 c_1) (= c_3 c_1) (not (p2 c_1 c_3 c_1)) (= c_1 c_3) (= c_1 c_3) (not (p2 c_1 c_1 c_3)) )(or (p2 c_1 c_1 c_1) (= c_4 c_1) (not (p2 c_1 c_4 c_1)) (= c_1 c_4) (= c_1 c_4) (not (p2 c_1 c_1 c_4)) )(or (p2 c_1 c_1 c_2) (= c_0 c_2) (not (p2 c_1 c_0 c_2)) (= c_1 c_0) (= c_1 c_0) (not (p2 c_1 c_1 c_0)) )(or (p2 c_1 c_1 c_2) (= c_1 c_2) (not (p2 c_1 c_1 c_2)) (= c_1 c_1) (= c_1 c_1) (not (p2 c_1 c_1 c_1)) )(or (p2 c_1 c_1 c_2) (= c_2 c_2) (not (p2 c_1 c_2 c_2)) (= c_1 c_2) (= c_1 c_2) (not (p2 c_1 c_1 c_2)) )(or (p2 c_1 c_1 c_2) (= c_3 c_2) (not (p2 c_1 c_3 c_2)) (= c_1 c_3) (= c_1 c_3) (not (p2 c_1 c_1 c_3)) )(or (p2 c_1 c_1 c_2) (= c_4 c_2) (not (p2 c_1 c_4 c_2)) (= c_1 c_4) (= c_1 c_4) (not (p2 c_1 c_1 c_4)) )(or (p2 c_1 c_1 c_3) (= c_0 c_3) (not (p2 c_1 c_0 c_3)) (= c_1 c_0) (= c_1 c_0) (not (p2 c_1 c_1 c_0)) )(or (p2 c_1 c_1 c_3) (= c_1 c_3) (not (p2 c_1 c_1 c_3)) (= c_1 c_1) (= c_1 c_1) (not (p2 c_1 c_1 c_1)) )(or (p2 c_1 c_1 c_3) (= c_2 c_3) (not (p2 c_1 c_2 c_3)) (= c_1 c_2) (= c_1 c_2) (not (p2 c_1 c_1 c_2)) )(or (p2 c_1 c_1 c_3) (= c_3 c_3) (not (p2 c_1 c_3 c_3)) (= c_1 c_3) (= c_1 c_3) (not (p2 c_1 c_1 c_3)) )(or (p2 c_1 c_1 c_3) (= c_4 c_3) (not (p2 c_1 c_4 c_3)) (= c_1 c_4) (= c_1 c_4) (not (p2 c_1 c_1 c_4)) )(or (p2 c_1 c_1 c_4) (= c_0 c_4) (not (p2 c_1 c_0 c_4)) (= c_1 c_0) (= c_1 c_0) (not (p2 c_1 c_1 c_0)) )(or (p2 c_1 c_1 c_4) (= c_1 c_4) (not (p2 c_1 c_1 c_4)) (= c_1 c_1) (= c_1 c_1) (not (p2 c_1 c_1 c_1)) )(or (p2 c_1 c_1 c_4) (= c_2 c_4) (not (p2 c_1 c_2 c_4)) (= c_1 c_2) (= c_1 c_2) (not (p2 c_1 c_1 c_2)) )(or (p2 c_1 c_1 c_4) (= c_3 c_4) (not (p2 c_1 c_3 c_4)) (= c_1 c_3) (= c_1 c_3) (not (p2 c_1 c_1 c_3)) )(or (p2 c_1 c_1 c_4) (= c_4 c_4) (not (p2 c_1 c_4 c_4)) (= c_1 c_4) (= c_1 c_4) (not (p2 c_1 c_1 c_4)) )(or (p2 c_1 c_2 c_0) (= c_0 c_0) (not (p2 c_2 c_0 c_0)) (= c_2 c_0) (= c_1 c_0) (not (p2 c_1 c_2 c_0)) )(or (p2 c_1 c_2 c_0) (= c_1 c_0) (not (p2 c_2 c_1 c_0)) (= c_2 c_1) (= c_1 c_1) (not (p2 c_1 c_2 c_1)) )(or (p2 c_1 c_2 c_0) (= c_2 c_0) (not (p2 c_2 c_2 c_0)) (= c_2 c_2) (= c_1 c_2) (not (p2 c_1 c_2 c_2)) )(or (p2 c_1 c_2 c_0) (= c_3 c_0) (not (p2 c_2 c_3 c_0)) (= c_2 c_3) (= c_1 c_3) (not (p2 c_1 c_2 c_3)) )(or (p2 c_1 c_2 c_0) (= c_4 c_0) (not (p2 c_2 c_4 c_0)) (= c_2 c_4) (= c_1 c_4) (not (p2 c_1 c_2 c_4)) )(or (p2 c_1 c_2 c_1) (= c_0 c_1) (not (p2 c_2 c_0 c_1)) (= c_2 c_0) (= c_1 c_0) (not (p2 c_1 c_2 c_0)) )(or (p2 c_1 c_2 c_1) (= c_1 c_1) (not (p2 c_2 c_1 c_1)) (= c_2 c_1) (= c_1 c_1) (not (p2 c_1 c_2 c_1)) )(or (p2 c_1 c_2 c_1) (= c_2 c_1) (not (p2 c_2 c_2 c_1)) (= c_2 c_2) (= c_1 c_2) (not (p2 c_1 c_2 c_2)) )(or (p2 c_1 c_2 c_1) (= c_3 c_1) (not (p2 c_2 c_3 c_1)) (= c_2 c_3) (= c_1 c_3) (not (p2 c_1 c_2 c_3)) )(or (p2 c_1 c_2 c_1) (= c_4 c_1) (not (p2 c_2 c_4 c_1)) (= c_2 c_4) (= c_1 c_4) (not (p2 c_1 c_2 c_4)) )(or (p2 c_1 c_2 c_2) (= c_0 c_2) (not (p2 c_2 c_0 c_2)) (= c_2 c_0) (= c_1 c_0) (not (p2 c_1 c_2 c_0)) )(or (p2 c_1 c_2 c_2) (= c_1 c_2) (not (p2 c_2 c_1 c_2)) (= c_2 c_1) (= c_1 c_1) (not (p2 c_1 c_2 c_1)) )(or (p2 c_1 c_2 c_2) (= c_2 c_2) (not (p2 c_2 c_2 c_2)) (= c_2 c_2) (= c_1 c_2) (not (p2 c_1 c_2 c_2)) )(or (p2 c_1 c_2 c_2) (= c_3 c_2) (not (p2 c_2 c_3 c_2)) (= c_2 c_3) (= c_1 c_3) (not (p2 c_1 c_2 c_3)) )(or (p2 c_1 c_2 c_2) (= c_4 c_2) (not (p2 c_2 c_4 c_2)) (= c_2 c_4) (= c_1 c_4) (not (p2 c_1 c_2 c_4)) )(or (p2 c_1 c_2 c_3) (= c_0 c_3) (not (p2 c_2 c_0 c_3)) (= c_2 c_0) (= c_1 c_0) (not (p2 c_1 c_2 c_0)) )(or (p2 c_1 c_2 c_3) (= c_1 c_3) (not (p2 c_2 c_1 c_3)) (= c_2 c_1) (= c_1 c_1) (not (p2 c_1 c_2 c_1)) )(or (p2 c_1 c_2 c_3) (= c_2 c_3) (not (p2 c_2 c_2 c_3)) (= c_2 c_2) (= c_1 c_2) (not (p2 c_1 c_2 c_2)) )(or (p2 c_1 c_2 c_3) (= c_3 c_3) (not (p2 c_2 c_3 c_3)) (= c_2 c_3) (= c_1 c_3) (not (p2 c_1 c_2 c_3)) )(or (p2 c_1 c_2 c_3) (= c_4 c_3) (not (p2 c_2 c_4 c_3)) (= c_2 c_4) (= c_1 c_4) (not (p2 c_1 c_2 c_4)) )(or (p2 c_1 c_2 c_4) (= c_0 c_4) (not (p2 c_2 c_0 c_4)) (= c_2 c_0) (= c_1 c_0) (not (p2 c_1 c_2 c_0)) )(or (p2 c_1 c_2 c_4) (= c_1 c_4) (not (p2 c_2 c_1 c_4)) (= c_2 c_1) (= c_1 c_1) (not (p2 c_1 c_2 c_1)) )(or (p2 c_1 c_2 c_4) (= c_2 c_4) (not (p2 c_2 c_2 c_4)) (= c_2 c_2) (= c_1 c_2) (not (p2 c_1 c_2 c_2)) )(or (p2 c_1 c_2 c_4) (= c_3 c_4) (not (p2 c_2 c_3 c_4)) (= c_2 c_3) (= c_1 c_3) (not (p2 c_1 c_2 c_3)) )(or (p2 c_1 c_2 c_4) (= c_4 c_4) (not (p2 c_2 c_4 c_4)) (= c_2 c_4) (= c_1 c_4) (not (p2 c_1 c_2 c_4)) )(or (p2 c_1 c_3 c_0) (= c_0 c_0) (not (p2 c_3 c_0 c_0)) (= c_3 c_0) (= c_1 c_0) (not (p2 c_1 c_3 c_0)) )(or (p2 c_1 c_3 c_0) (= c_1 c_0) (not (p2 c_3 c_1 c_0)) (= c_3 c_1) (= c_1 c_1) (not (p2 c_1 c_3 c_1)) )(or (p2 c_1 c_3 c_0) (= c_2 c_0) (not (p2 c_3 c_2 c_0)) (= c_3 c_2) (= c_1 c_2) (not (p2 c_1 c_3 c_2)) )(or (p2 c_1 c_3 c_0) (= c_3 c_0) (not (p2 c_3 c_3 c_0)) (= c_3 c_3) (= c_1 c_3) (not (p2 c_1 c_3 c_3)) )(or (p2 c_1 c_3 c_0) (= c_4 c_0) (not (p2 c_3 c_4 c_0)) (= c_3 c_4) (= c_1 c_4) (not (p2 c_1 c_3 c_4)) )(or (p2 c_1 c_3 c_1) (= c_0 c_1) (not (p2 c_3 c_0 c_1)) (= c_3 c_0) (= c_1 c_0) (not (p2 c_1 c_3 c_0)) )(or (p2 c_1 c_3 c_1) (= c_1 c_1) (not (p2 c_3 c_1 c_1)) (= c_3 c_1) (= c_1 c_1) (not (p2 c_1 c_3 c_1)) )(or (p2 c_1 c_3 c_1) (= c_2 c_1) (not (p2 c_3 c_2 c_1)) (= c_3 c_2) (= c_1 c_2) (not (p2 c_1 c_3 c_2)) )(or (p2 c_1 c_3 c_1) (= c_3 c_1) (not (p2 c_3 c_3 c_1)) (= c_3 c_3) (= c_1 c_3) (not (p2 c_1 c_3 c_3)) )(or (p2 c_1 c_3 c_1) (= c_4 c_1) (not (p2 c_3 c_4 c_1)) (= c_3 c_4) (= c_1 c_4) (not (p2 c_1 c_3 c_4)) )(or (p2 c_1 c_3 c_2) (= c_0 c_2) (not (p2 c_3 c_0 c_2)) (= c_3 c_0) (= c_1 c_0) (not (p2 c_1 c_3 c_0)) )(or (p2 c_1 c_3 c_2) (= c_1 c_2) (not (p2 c_3 c_1 c_2)) (= c_3 c_1) (= c_1 c_1) (not (p2 c_1 c_3 c_1)) )(or (p2 c_1 c_3 c_2) (= c_2 c_2) (not (p2 c_3 c_2 c_2)) (= c_3 c_2) (= c_1 c_2) (not (p2 c_1 c_3 c_2)) )(or (p2 c_1 c_3 c_2) (= c_3 c_2) (not (p2 c_3 c_3 c_2)) (= c_3 c_3) (= c_1 c_3) (not (p2 c_1 c_3 c_3)) )(or (p2 c_1 c_3 c_2) (= c_4 c_2) (not (p2 c_3 c_4 c_2)) (= c_3 c_4) (= c_1 c_4) (not (p2 c_1 c_3 c_4)) )(or (p2 c_1 c_3 c_3) (= c_0 c_3) (not (p2 c_3 c_0 c_3)) (= c_3 c_0) (= c_1 c_0) (not (p2 c_1 c_3 c_0)) )(or (p2 c_1 c_3 c_3) (= c_1 c_3) (not (p2 c_3 c_1 c_3)) (= c_3 c_1) (= c_1 c_1) (not (p2 c_1 c_3 c_1)) )(or (p2 c_1 c_3 c_3) (= c_2 c_3) (not (p2 c_3 c_2 c_3)) (= c_3 c_2) (= c_1 c_2) (not (p2 c_1 c_3 c_2)) )(or (p2 c_1 c_3 c_3) (= c_3 c_3) (not (p2 c_3 c_3 c_3)) (= c_3 c_3) (= c_1 c_3) (not (p2 c_1 c_3 c_3)) )(or (p2 c_1 c_3 c_3) (= c_4 c_3) (not (p2 c_3 c_4 c_3)) (= c_3 c_4) (= c_1 c_4) (not (p2 c_1 c_3 c_4)) )(or (p2 c_1 c_3 c_4) (= c_0 c_4) (not (p2 c_3 c_0 c_4)) (= c_3 c_0) (= c_1 c_0) (not (p2 c_1 c_3 c_0)) )(or (p2 c_1 c_3 c_4) (= c_1 c_4) (not (p2 c_3 c_1 c_4)) (= c_3 c_1) (= c_1 c_1) (not (p2 c_1 c_3 c_1)) )(or (p2 c_1 c_3 c_4) (= c_2 c_4) (not (p2 c_3 c_2 c_4)) (= c_3 c_2) (= c_1 c_2) (not (p2 c_1 c_3 c_2)) )(or (p2 c_1 c_3 c_4) (= c_3 c_4) (not (p2 c_3 c_3 c_4)) (= c_3 c_3) (= c_1 c_3) (not (p2 c_1 c_3 c_3)) )(or (p2 c_1 c_3 c_4) (= c_4 c_4) (not (p2 c_3 c_4 c_4)) (= c_3 c_4) (= c_1 c_4) (not (p2 c_1 c_3 c_4)) )(or (p2 c_1 c_4 c_0) (= c_0 c_0) (not (p2 c_4 c_0 c_0)) (= c_4 c_0) (= c_1 c_0) (not (p2 c_1 c_4 c_0)) )(or (p2 c_1 c_4 c_0) (= c_1 c_0) (not (p2 c_4 c_1 c_0)) (= c_4 c_1) (= c_1 c_1) (not (p2 c_1 c_4 c_1)) )(or (p2 c_1 c_4 c_0) (= c_2 c_0) (not (p2 c_4 c_2 c_0)) (= c_4 c_2) (= c_1 c_2) (not (p2 c_1 c_4 c_2)) )(or (p2 c_1 c_4 c_0) (= c_3 c_0) (not (p2 c_4 c_3 c_0)) (= c_4 c_3) (= c_1 c_3) (not (p2 c_1 c_4 c_3)) )(or (p2 c_1 c_4 c_0) (= c_4 c_0) (not (p2 c_4 c_4 c_0)) (= c_4 c_4) (= c_1 c_4) (not (p2 c_1 c_4 c_4)) )(or (p2 c_1 c_4 c_1) (= c_0 c_1) (not (p2 c_4 c_0 c_1)) (= c_4 c_0) (= c_1 c_0) (not (p2 c_1 c_4 c_0)) )(or (p2 c_1 c_4 c_1) (= c_1 c_1) (not (p2 c_4 c_1 c_1)) (= c_4 c_1) (= c_1 c_1) (not (p2 c_1 c_4 c_1)) )(or (p2 c_1 c_4 c_1) (= c_2 c_1) (not (p2 c_4 c_2 c_1)) (= c_4 c_2) (= c_1 c_2) (not (p2 c_1 c_4 c_2)) )(or (p2 c_1 c_4 c_1) (= c_3 c_1) (not (p2 c_4 c_3 c_1)) (= c_4 c_3) (= c_1 c_3) (not (p2 c_1 c_4 c_3)) )(or (p2 c_1 c_4 c_1) (= c_4 c_1) (not (p2 c_4 c_4 c_1)) (= c_4 c_4) (= c_1 c_4) (not (p2 c_1 c_4 c_4)) )(or (p2 c_1 c_4 c_2) (= c_0 c_2) (not (p2 c_4 c_0 c_2)) (= c_4 c_0) (= c_1 c_0) (not (p2 c_1 c_4 c_0)) )(or (p2 c_1 c_4 c_2) (= c_1 c_2) (not (p2 c_4 c_1 c_2)) (= c_4 c_1) (= c_1 c_1) (not (p2 c_1 c_4 c_1)) )(or (p2 c_1 c_4 c_2) (= c_2 c_2) (not (p2 c_4 c_2 c_2)) (= c_4 c_2) (= c_1 c_2) (not (p2 c_1 c_4 c_2)) )(or (p2 c_1 c_4 c_2) (= c_3 c_2) (not (p2 c_4 c_3 c_2)) (= c_4 c_3) (= c_1 c_3) (not (p2 c_1 c_4 c_3)) )(or (p2 c_1 c_4 c_2) (= c_4 c_2) (not (p2 c_4 c_4 c_2)) (= c_4 c_4) (= c_1 c_4) (not (p2 c_1 c_4 c_4)) )(or (p2 c_1 c_4 c_3) (= c_0 c_3) (not (p2 c_4 c_0 c_3)) (= c_4 c_0) (= c_1 c_0) (not (p2 c_1 c_4 c_0)) )(or (p2 c_1 c_4 c_3) (= c_1 c_3) (not (p2 c_4 c_1 c_3)) (= c_4 c_1) (= c_1 c_1) (not (p2 c_1 c_4 c_1)) )(or (p2 c_1 c_4 c_3) (= c_2 c_3) (not (p2 c_4 c_2 c_3)) (= c_4 c_2) (= c_1 c_2) (not (p2 c_1 c_4 c_2)) )(or (p2 c_1 c_4 c_3) (= c_3 c_3) (not (p2 c_4 c_3 c_3)) (= c_4 c_3) (= c_1 c_3) (not (p2 c_1 c_4 c_3)) )(or (p2 c_1 c_4 c_3) (= c_4 c_3) (not (p2 c_4 c_4 c_3)) (= c_4 c_4) (= c_1 c_4) (not (p2 c_1 c_4 c_4)) )(or (p2 c_1 c_4 c_4) (= c_0 c_4) (not (p2 c_4 c_0 c_4)) (= c_4 c_0) (= c_1 c_0) (not (p2 c_1 c_4 c_0)) )(or (p2 c_1 c_4 c_4) (= c_1 c_4) (not (p2 c_4 c_1 c_4)) (= c_4 c_1) (= c_1 c_1) (not (p2 c_1 c_4 c_1)) )(or (p2 c_1 c_4 c_4) (= c_2 c_4) (not (p2 c_4 c_2 c_4)) (= c_4 c_2) (= c_1 c_2) (not (p2 c_1 c_4 c_2)) )(or (p2 c_1 c_4 c_4) (= c_3 c_4) (not (p2 c_4 c_3 c_4)) (= c_4 c_3) (= c_1 c_3) (not (p2 c_1 c_4 c_3)) )(or (p2 c_1 c_4 c_4) (= c_4 c_4) (not (p2 c_4 c_4 c_4)) (= c_4 c_4) (= c_1 c_4) (not (p2 c_1 c_4 c_4)) )(or (p2 c_2 c_0 c_0) (= c_0 c_0) (not (p2 c_0 c_0 c_0)) (= c_0 c_0) (= c_2 c_0) (not (p2 c_2 c_0 c_0)) )(or (p2 c_2 c_0 c_0) (= c_1 c_0) (not (p2 c_0 c_1 c_0)) (= c_0 c_1) (= c_2 c_1) (not (p2 c_2 c_0 c_1)) )(or (p2 c_2 c_0 c_0) (= c_2 c_0) (not (p2 c_0 c_2 c_0)) (= c_0 c_2) (= c_2 c_2) (not (p2 c_2 c_0 c_2)) )(or (p2 c_2 c_0 c_0) (= c_3 c_0) (not (p2 c_0 c_3 c_0)) (= c_0 c_3) (= c_2 c_3) (not (p2 c_2 c_0 c_3)) )(or (p2 c_2 c_0 c_0) (= c_4 c_0) (not (p2 c_0 c_4 c_0)) (= c_0 c_4) (= c_2 c_4) (not (p2 c_2 c_0 c_4)) )(or (p2 c_2 c_0 c_1) (= c_0 c_1) (not (p2 c_0 c_0 c_1)) (= c_0 c_0) (= c_2 c_0) (not (p2 c_2 c_0 c_0)) )(or (p2 c_2 c_0 c_1) (= c_1 c_1) (not (p2 c_0 c_1 c_1)) (= c_0 c_1) (= c_2 c_1) (not (p2 c_2 c_0 c_1)) )(or (p2 c_2 c_0 c_1) (= c_2 c_1) (not (p2 c_0 c_2 c_1)) (= c_0 c_2) (= c_2 c_2) (not (p2 c_2 c_0 c_2)) )(or (p2 c_2 c_0 c_1) (= c_3 c_1) (not (p2 c_0 c_3 c_1)) (= c_0 c_3) (= c_2 c_3) (not (p2 c_2 c_0 c_3)) )(or (p2 c_2 c_0 c_1) (= c_4 c_1) (not (p2 c_0 c_4 c_1)) (= c_0 c_4) (= c_2 c_4) (not (p2 c_2 c_0 c_4)) )(or (p2 c_2 c_0 c_2) (= c_0 c_2) (not (p2 c_0 c_0 c_2)) (= c_0 c_0) (= c_2 c_0) (not (p2 c_2 c_0 c_0)) )(or (p2 c_2 c_0 c_2) (= c_1 c_2) (not (p2 c_0 c_1 c_2)) (= c_0 c_1) (= c_2 c_1) (not (p2 c_2 c_0 c_1)) )(or (p2 c_2 c_0 c_2) (= c_2 c_2) (not (p2 c_0 c_2 c_2)) (= c_0 c_2) (= c_2 c_2) (not (p2 c_2 c_0 c_2)) )(or (p2 c_2 c_0 c_2) (= c_3 c_2) (not (p2 c_0 c_3 c_2)) (= c_0 c_3) (= c_2 c_3) (not (p2 c_2 c_0 c_3)) )(or (p2 c_2 c_0 c_2) (= c_4 c_2) (not (p2 c_0 c_4 c_2)) (= c_0 c_4) (= c_2 c_4) (not (p2 c_2 c_0 c_4)) )(or (p2 c_2 c_0 c_3) (= c_0 c_3) (not (p2 c_0 c_0 c_3)) (= c_0 c_0) (= c_2 c_0) (not (p2 c_2 c_0 c_0)) )(or (p2 c_2 c_0 c_3) (= c_1 c_3) (not (p2 c_0 c_1 c_3)) (= c_0 c_1) (= c_2 c_1) (not (p2 c_2 c_0 c_1)) )(or (p2 c_2 c_0 c_3) (= c_2 c_3) (not (p2 c_0 c_2 c_3)) (= c_0 c_2) (= c_2 c_2) (not (p2 c_2 c_0 c_2)) )(or (p2 c_2 c_0 c_3) (= c_3 c_3) (not (p2 c_0 c_3 c_3)) (= c_0 c_3) (= c_2 c_3) (not (p2 c_2 c_0 c_3)) )(or (p2 c_2 c_0 c_3) (= c_4 c_3) (not (p2 c_0 c_4 c_3)) (= c_0 c_4) (= c_2 c_4) (not (p2 c_2 c_0 c_4)) )(or (p2 c_2 c_0 c_4) (= c_0 c_4) (not (p2 c_0 c_0 c_4)) (= c_0 c_0) (= c_2 c_0) (not (p2 c_2 c_0 c_0)) )(or (p2 c_2 c_0 c_4) (= c_1 c_4) (not (p2 c_0 c_1 c_4)) (= c_0 c_1) (= c_2 c_1) (not (p2 c_2 c_0 c_1)) )(or (p2 c_2 c_0 c_4) (= c_2 c_4) (not (p2 c_0 c_2 c_4)) (= c_0 c_2) (= c_2 c_2) (not (p2 c_2 c_0 c_2)) )(or (p2 c_2 c_0 c_4) (= c_3 c_4) (not (p2 c_0 c_3 c_4)) (= c_0 c_3) (= c_2 c_3) (not (p2 c_2 c_0 c_3)) )(or (p2 c_2 c_0 c_4) (= c_4 c_4) (not (p2 c_0 c_4 c_4)) (= c_0 c_4) (= c_2 c_4) (not (p2 c_2 c_0 c_4)) )(or (p2 c_2 c_1 c_0) (= c_0 c_0) (not (p2 c_1 c_0 c_0)) (= c_1 c_0) (= c_2 c_0) (not (p2 c_2 c_1 c_0)) )(or (p2 c_2 c_1 c_0) (= c_1 c_0) (not (p2 c_1 c_1 c_0)) (= c_1 c_1) (= c_2 c_1) (not (p2 c_2 c_1 c_1)) )(or (p2 c_2 c_1 c_0) (= c_2 c_0) (not (p2 c_1 c_2 c_0)) (= c_1 c_2) (= c_2 c_2) (not (p2 c_2 c_1 c_2)) )(or (p2 c_2 c_1 c_0) (= c_3 c_0) (not (p2 c_1 c_3 c_0)) (= c_1 c_3) (= c_2 c_3) (not (p2 c_2 c_1 c_3)) )(or (p2 c_2 c_1 c_0) (= c_4 c_0) (not (p2 c_1 c_4 c_0)) (= c_1 c_4) (= c_2 c_4) (not (p2 c_2 c_1 c_4)) )(or (p2 c_2 c_1 c_1) (= c_0 c_1) (not (p2 c_1 c_0 c_1)) (= c_1 c_0) (= c_2 c_0) (not (p2 c_2 c_1 c_0)) )(or (p2 c_2 c_1 c_1) (= c_1 c_1) (not (p2 c_1 c_1 c_1)) (= c_1 c_1) (= c_2 c_1) (not (p2 c_2 c_1 c_1)) )(or (p2 c_2 c_1 c_1) (= c_2 c_1) (not (p2 c_1 c_2 c_1)) (= c_1 c_2) (= c_2 c_2) (not (p2 c_2 c_1 c_2)) )(or (p2 c_2 c_1 c_1) (= c_3 c_1) (not (p2 c_1 c_3 c_1)) (= c_1 c_3) (= c_2 c_3) (not (p2 c_2 c_1 c_3)) )(or (p2 c_2 c_1 c_1) (= c_4 c_1) (not (p2 c_1 c_4 c_1)) (= c_1 c_4) (= c_2 c_4) (not (p2 c_2 c_1 c_4)) )(or (p2 c_2 c_1 c_2) (= c_0 c_2) (not (p2 c_1 c_0 c_2)) (= c_1 c_0) (= c_2 c_0) (not (p2 c_2 c_1 c_0)) )(or (p2 c_2 c_1 c_2) (= c_1 c_2) (not (p2 c_1 c_1 c_2)) (= c_1 c_1) (= c_2 c_1) (not (p2 c_2 c_1 c_1)) )(or (p2 c_2 c_1 c_2) (= c_2 c_2) (not (p2 c_1 c_2 c_2)) (= c_1 c_2) (= c_2 c_2) (not (p2 c_2 c_1 c_2)) )(or (p2 c_2 c_1 c_2) (= c_3 c_2) (not (p2 c_1 c_3 c_2)) (= c_1 c_3) (= c_2 c_3) (not (p2 c_2 c_1 c_3)) )(or (p2 c_2 c_1 c_2) (= c_4 c_2) (not (p2 c_1 c_4 c_2)) (= c_1 c_4) (= c_2 c_4) (not (p2 c_2 c_1 c_4)) )(or (p2 c_2 c_1 c_3) (= c_0 c_3) (not (p2 c_1 c_0 c_3)) (= c_1 c_0) (= c_2 c_0) (not (p2 c_2 c_1 c_0)) )(or (p2 c_2 c_1 c_3) (= c_1 c_3) (not (p2 c_1 c_1 c_3)) (= c_1 c_1) (= c_2 c_1) (not (p2 c_2 c_1 c_1)) )(or (p2 c_2 c_1 c_3) (= c_2 c_3) (not (p2 c_1 c_2 c_3)) (= c_1 c_2) (= c_2 c_2) (not (p2 c_2 c_1 c_2)) )(or (p2 c_2 c_1 c_3) (= c_3 c_3) (not (p2 c_1 c_3 c_3)) (= c_1 c_3) (= c_2 c_3) (not (p2 c_2 c_1 c_3)) )(or (p2 c_2 c_1 c_3) (= c_4 c_3) (not (p2 c_1 c_4 c_3)) (= c_1 c_4) (= c_2 c_4) (not (p2 c_2 c_1 c_4)) )(or (p2 c_2 c_1 c_4) (= c_0 c_4) (not (p2 c_1 c_0 c_4)) (= c_1 c_0) (= c_2 c_0) (not (p2 c_2 c_1 c_0)) )(or (p2 c_2 c_1 c_4) (= c_1 c_4) (not (p2 c_1 c_1 c_4)) (= c_1 c_1) (= c_2 c_1) (not (p2 c_2 c_1 c_1)) )(or (p2 c_2 c_1 c_4) (= c_2 c_4) (not (p2 c_1 c_2 c_4)) (= c_1 c_2) (= c_2 c_2) (not (p2 c_2 c_1 c_2)) )(or (p2 c_2 c_1 c_4) (= c_3 c_4) (not (p2 c_1 c_3 c_4)) (= c_1 c_3) (= c_2 c_3) (not (p2 c_2 c_1 c_3)) )(or (p2 c_2 c_1 c_4) (= c_4 c_4) (not (p2 c_1 c_4 c_4)) (= c_1 c_4) (= c_2 c_4) (not (p2 c_2 c_1 c_4)) )(or (p2 c_2 c_2 c_0) (= c_0 c_0) (not (p2 c_2 c_0 c_0)) (= c_2 c_0) (= c_2 c_0) (not (p2 c_2 c_2 c_0)) )(or (p2 c_2 c_2 c_0) (= c_1 c_0) (not (p2 c_2 c_1 c_0)) (= c_2 c_1) (= c_2 c_1) (not (p2 c_2 c_2 c_1)) )(or (p2 c_2 c_2 c_0) (= c_2 c_0) (not (p2 c_2 c_2 c_0)) (= c_2 c_2) (= c_2 c_2) (not (p2 c_2 c_2 c_2)) )(or (p2 c_2 c_2 c_0) (= c_3 c_0) (not (p2 c_2 c_3 c_0)) (= c_2 c_3) (= c_2 c_3) (not (p2 c_2 c_2 c_3)) )(or (p2 c_2 c_2 c_0) (= c_4 c_0) (not (p2 c_2 c_4 c_0)) (= c_2 c_4) (= c_2 c_4) (not (p2 c_2 c_2 c_4)) )(or (p2 c_2 c_2 c_1) (= c_0 c_1) (not (p2 c_2 c_0 c_1)) (= c_2 c_0) (= c_2 c_0) (not (p2 c_2 c_2 c_0)) )(or (p2 c_2 c_2 c_1) (= c_1 c_1) (not (p2 c_2 c_1 c_1)) (= c_2 c_1) (= c_2 c_1) (not (p2 c_2 c_2 c_1)) )(or (p2 c_2 c_2 c_1) (= c_2 c_1) (not (p2 c_2 c_2 c_1)) (= c_2 c_2) (= c_2 c_2) (not (p2 c_2 c_2 c_2)) )(or (p2 c_2 c_2 c_1) (= c_3 c_1) (not (p2 c_2 c_3 c_1)) (= c_2 c_3) (= c_2 c_3) (not (p2 c_2 c_2 c_3)) )(or (p2 c_2 c_2 c_1) (= c_4 c_1) (not (p2 c_2 c_4 c_1)) (= c_2 c_4) (= c_2 c_4) (not (p2 c_2 c_2 c_4)) )(or (p2 c_2 c_2 c_2) (= c_0 c_2) (not (p2 c_2 c_0 c_2)) (= c_2 c_0) (= c_2 c_0) (not (p2 c_2 c_2 c_0)) )(or (p2 c_2 c_2 c_2) (= c_1 c_2) (not (p2 c_2 c_1 c_2)) (= c_2 c_1) (= c_2 c_1) (not (p2 c_2 c_2 c_1)) )(or (p2 c_2 c_2 c_2) (= c_2 c_2) (not (p2 c_2 c_2 c_2)) (= c_2 c_2) (= c_2 c_2) (not (p2 c_2 c_2 c_2)) )(or (p2 c_2 c_2 c_2) (= c_3 c_2) (not (p2 c_2 c_3 c_2)) (= c_2 c_3) (= c_2 c_3) (not (p2 c_2 c_2 c_3)) )(or (p2 c_2 c_2 c_2) (= c_4 c_2) (not (p2 c_2 c_4 c_2)) (= c_2 c_4) (= c_2 c_4) (not (p2 c_2 c_2 c_4)) )(or (p2 c_2 c_2 c_3) (= c_0 c_3) (not (p2 c_2 c_0 c_3)) (= c_2 c_0) (= c_2 c_0) (not (p2 c_2 c_2 c_0)) )(or (p2 c_2 c_2 c_3) (= c_1 c_3) (not (p2 c_2 c_1 c_3)) (= c_2 c_1) (= c_2 c_1) (not (p2 c_2 c_2 c_1)) )(or (p2 c_2 c_2 c_3) (= c_2 c_3) (not (p2 c_2 c_2 c_3)) (= c_2 c_2) (= c_2 c_2) (not (p2 c_2 c_2 c_2)) )(or (p2 c_2 c_2 c_3) (= c_3 c_3) (not (p2 c_2 c_3 c_3)) (= c_2 c_3) (= c_2 c_3) (not (p2 c_2 c_2 c_3)) )(or (p2 c_2 c_2 c_3) (= c_4 c_3) (not (p2 c_2 c_4 c_3)) (= c_2 c_4) (= c_2 c_4) (not (p2 c_2 c_2 c_4)) )(or (p2 c_2 c_2 c_4) (= c_0 c_4) (not (p2 c_2 c_0 c_4)) (= c_2 c_0) (= c_2 c_0) (not (p2 c_2 c_2 c_0)) )(or (p2 c_2 c_2 c_4) (= c_1 c_4) (not (p2 c_2 c_1 c_4)) (= c_2 c_1) (= c_2 c_1) (not (p2 c_2 c_2 c_1)) )(or (p2 c_2 c_2 c_4) (= c_2 c_4) (not (p2 c_2 c_2 c_4)) (= c_2 c_2) (= c_2 c_2) (not (p2 c_2 c_2 c_2)) )(or (p2 c_2 c_2 c_4) (= c_3 c_4) (not (p2 c_2 c_3 c_4)) (= c_2 c_3) (= c_2 c_3) (not (p2 c_2 c_2 c_3)) )(or (p2 c_2 c_2 c_4) (= c_4 c_4) (not (p2 c_2 c_4 c_4)) (= c_2 c_4) (= c_2 c_4) (not (p2 c_2 c_2 c_4)) )(or (p2 c_2 c_3 c_0) (= c_0 c_0) (not (p2 c_3 c_0 c_0)) (= c_3 c_0) (= c_2 c_0) (not (p2 c_2 c_3 c_0)) )(or (p2 c_2 c_3 c_0) (= c_1 c_0) (not (p2 c_3 c_1 c_0)) (= c_3 c_1) (= c_2 c_1) (not (p2 c_2 c_3 c_1)) )(or (p2 c_2 c_3 c_0) (= c_2 c_0) (not (p2 c_3 c_2 c_0)) (= c_3 c_2) (= c_2 c_2) (not (p2 c_2 c_3 c_2)) )(or (p2 c_2 c_3 c_0) (= c_3 c_0) (not (p2 c_3 c_3 c_0)) (= c_3 c_3) (= c_2 c_3) (not (p2 c_2 c_3 c_3)) )(or (p2 c_2 c_3 c_0) (= c_4 c_0) (not (p2 c_3 c_4 c_0)) (= c_3 c_4) (= c_2 c_4) (not (p2 c_2 c_3 c_4)) )(or (p2 c_2 c_3 c_1) (= c_0 c_1) (not (p2 c_3 c_0 c_1)) (= c_3 c_0) (= c_2 c_0) (not (p2 c_2 c_3 c_0)) )(or (p2 c_2 c_3 c_1) (= c_1 c_1) (not (p2 c_3 c_1 c_1)) (= c_3 c_1) (= c_2 c_1) (not (p2 c_2 c_3 c_1)) )(or (p2 c_2 c_3 c_1) (= c_2 c_1) (not (p2 c_3 c_2 c_1)) (= c_3 c_2) (= c_2 c_2) (not (p2 c_2 c_3 c_2)) )(or (p2 c_2 c_3 c_1) (= c_3 c_1) (not (p2 c_3 c_3 c_1)) (= c_3 c_3) (= c_2 c_3) (not (p2 c_2 c_3 c_3)) )(or (p2 c_2 c_3 c_1) (= c_4 c_1) (not (p2 c_3 c_4 c_1)) (= c_3 c_4) (= c_2 c_4) (not (p2 c_2 c_3 c_4)) )(or (p2 c_2 c_3 c_2) (= c_0 c_2) (not (p2 c_3 c_0 c_2)) (= c_3 c_0) (= c_2 c_0) (not (p2 c_2 c_3 c_0)) )(or (p2 c_2 c_3 c_2) (= c_1 c_2) (not (p2 c_3 c_1 c_2)) (= c_3 c_1) (= c_2 c_1) (not (p2 c_2 c_3 c_1)) )(or (p2 c_2 c_3 c_2) (= c_2 c_2) (not (p2 c_3 c_2 c_2)) (= c_3 c_2) (= c_2 c_2) (not (p2 c_2 c_3 c_2)) )(or (p2 c_2 c_3 c_2) (= c_3 c_2) (not (p2 c_3 c_3 c_2)) (= c_3 c_3) (= c_2 c_3) (not (p2 c_2 c_3 c_3)) )(or (p2 c_2 c_3 c_2) (= c_4 c_2) (not (p2 c_3 c_4 c_2)) (= c_3 c_4) (= c_2 c_4) (not (p2 c_2 c_3 c_4)) )(or (p2 c_2 c_3 c_3) (= c_0 c_3) (not (p2 c_3 c_0 c_3)) (= c_3 c_0) (= c_2 c_0) (not (p2 c_2 c_3 c_0)) )(or (p2 c_2 c_3 c_3) (= c_1 c_3) (not (p2 c_3 c_1 c_3)) (= c_3 c_1) (= c_2 c_1) (not (p2 c_2 c_3 c_1)) )(or (p2 c_2 c_3 c_3) (= c_2 c_3) (not (p2 c_3 c_2 c_3)) (= c_3 c_2) (= c_2 c_2) (not (p2 c_2 c_3 c_2)) )(or (p2 c_2 c_3 c_3) (= c_3 c_3) (not (p2 c_3 c_3 c_3)) (= c_3 c_3) (= c_2 c_3) (not (p2 c_2 c_3 c_3)) )(or (p2 c_2 c_3 c_3) (= c_4 c_3) (not (p2 c_3 c_4 c_3)) (= c_3 c_4) (= c_2 c_4) (not (p2 c_2 c_3 c_4)) )(or (p2 c_2 c_3 c_4) (= c_0 c_4) (not (p2 c_3 c_0 c_4)) (= c_3 c_0) (= c_2 c_0) (not (p2 c_2 c_3 c_0)) )(or (p2 c_2 c_3 c_4) (= c_1 c_4) (not (p2 c_3 c_1 c_4)) (= c_3 c_1) (= c_2 c_1) (not (p2 c_2 c_3 c_1)) )(or (p2 c_2 c_3 c_4) (= c_2 c_4) (not (p2 c_3 c_2 c_4)) (= c_3 c_2) (= c_2 c_2) (not (p2 c_2 c_3 c_2)) )(or (p2 c_2 c_3 c_4) (= c_3 c_4) (not (p2 c_3 c_3 c_4)) (= c_3 c_3) (= c_2 c_3) (not (p2 c_2 c_3 c_3)) )(or (p2 c_2 c_3 c_4) (= c_4 c_4) (not (p2 c_3 c_4 c_4)) (= c_3 c_4) (= c_2 c_4) (not (p2 c_2 c_3 c_4)) )(or (p2 c_2 c_4 c_0) (= c_0 c_0) (not (p2 c_4 c_0 c_0)) (= c_4 c_0) (= c_2 c_0) (not (p2 c_2 c_4 c_0)) )(or (p2 c_2 c_4 c_0) (= c_1 c_0) (not (p2 c_4 c_1 c_0)) (= c_4 c_1) (= c_2 c_1) (not (p2 c_2 c_4 c_1)) )(or (p2 c_2 c_4 c_0) (= c_2 c_0) (not (p2 c_4 c_2 c_0)) (= c_4 c_2) (= c_2 c_2) (not (p2 c_2 c_4 c_2)) )(or (p2 c_2 c_4 c_0) (= c_3 c_0) (not (p2 c_4 c_3 c_0)) (= c_4 c_3) (= c_2 c_3) (not (p2 c_2 c_4 c_3)) )(or (p2 c_2 c_4 c_0) (= c_4 c_0) (not (p2 c_4 c_4 c_0)) (= c_4 c_4) (= c_2 c_4) (not (p2 c_2 c_4 c_4)) )(or (p2 c_2 c_4 c_1) (= c_0 c_1) (not (p2 c_4 c_0 c_1)) (= c_4 c_0) (= c_2 c_0) (not (p2 c_2 c_4 c_0)) )(or (p2 c_2 c_4 c_1) (= c_1 c_1) (not (p2 c_4 c_1 c_1)) (= c_4 c_1) (= c_2 c_1) (not (p2 c_2 c_4 c_1)) )(or (p2 c_2 c_4 c_1) (= c_2 c_1) (not (p2 c_4 c_2 c_1)) (= c_4 c_2) (= c_2 c_2) (not (p2 c_2 c_4 c_2)) )(or (p2 c_2 c_4 c_1) (= c_3 c_1) (not (p2 c_4 c_3 c_1)) (= c_4 c_3) (= c_2 c_3) (not (p2 c_2 c_4 c_3)) )(or (p2 c_2 c_4 c_1) (= c_4 c_1) (not (p2 c_4 c_4 c_1)) (= c_4 c_4) (= c_2 c_4) (not (p2 c_2 c_4 c_4)) )(or (p2 c_2 c_4 c_2) (= c_0 c_2) (not (p2 c_4 c_0 c_2)) (= c_4 c_0) (= c_2 c_0) (not (p2 c_2 c_4 c_0)) )(or (p2 c_2 c_4 c_2) (= c_1 c_2) (not (p2 c_4 c_1 c_2)) (= c_4 c_1) (= c_2 c_1) (not (p2 c_2 c_4 c_1)) )(or (p2 c_2 c_4 c_2) (= c_2 c_2) (not (p2 c_4 c_2 c_2)) (= c_4 c_2) (= c_2 c_2) (not (p2 c_2 c_4 c_2)) )(or (p2 c_2 c_4 c_2) (= c_3 c_2) (not (p2 c_4 c_3 c_2)) (= c_4 c_3) (= c_2 c_3) (not (p2 c_2 c_4 c_3)) )(or (p2 c_2 c_4 c_2) (= c_4 c_2) (not (p2 c_4 c_4 c_2)) (= c_4 c_4) (= c_2 c_4) (not (p2 c_2 c_4 c_4)) )(or (p2 c_2 c_4 c_3) (= c_0 c_3) (not (p2 c_4 c_0 c_3)) (= c_4 c_0) (= c_2 c_0) (not (p2 c_2 c_4 c_0)) )(or (p2 c_2 c_4 c_3) (= c_1 c_3) (not (p2 c_4 c_1 c_3)) (= c_4 c_1) (= c_2 c_1) (not (p2 c_2 c_4 c_1)) )(or (p2 c_2 c_4 c_3) (= c_2 c_3) (not (p2 c_4 c_2 c_3)) (= c_4 c_2) (= c_2 c_2) (not (p2 c_2 c_4 c_2)) )(or (p2 c_2 c_4 c_3) (= c_3 c_3) (not (p2 c_4 c_3 c_3)) (= c_4 c_3) (= c_2 c_3) (not (p2 c_2 c_4 c_3)) )(or (p2 c_2 c_4 c_3) (= c_4 c_3) (not (p2 c_4 c_4 c_3)) (= c_4 c_4) (= c_2 c_4) (not (p2 c_2 c_4 c_4)) )(or (p2 c_2 c_4 c_4) (= c_0 c_4) (not (p2 c_4 c_0 c_4)) (= c_4 c_0) (= c_2 c_0) (not (p2 c_2 c_4 c_0)) )(or (p2 c_2 c_4 c_4) (= c_1 c_4) (not (p2 c_4 c_1 c_4)) (= c_4 c_1) (= c_2 c_1) (not (p2 c_2 c_4 c_1)) )(or (p2 c_2 c_4 c_4) (= c_2 c_4) (not (p2 c_4 c_2 c_4)) (= c_4 c_2) (= c_2 c_2) (not (p2 c_2 c_4 c_2)) )(or (p2 c_2 c_4 c_4) (= c_3 c_4) (not (p2 c_4 c_3 c_4)) (= c_4 c_3) (= c_2 c_3) (not (p2 c_2 c_4 c_3)) )(or (p2 c_2 c_4 c_4) (= c_4 c_4) (not (p2 c_4 c_4 c_4)) (= c_4 c_4) (= c_2 c_4) (not (p2 c_2 c_4 c_4)) )(or (p2 c_3 c_0 c_0) (= c_0 c_0) (not (p2 c_0 c_0 c_0)) (= c_0 c_0) (= c_3 c_0) (not (p2 c_3 c_0 c_0)) )(or (p2 c_3 c_0 c_0) (= c_1 c_0) (not (p2 c_0 c_1 c_0)) (= c_0 c_1) (= c_3 c_1) (not (p2 c_3 c_0 c_1)) )(or (p2 c_3 c_0 c_0) (= c_2 c_0) (not (p2 c_0 c_2 c_0)) (= c_0 c_2) (= c_3 c_2) (not (p2 c_3 c_0 c_2)) )(or (p2 c_3 c_0 c_0) (= c_3 c_0) (not (p2 c_0 c_3 c_0)) (= c_0 c_3) (= c_3 c_3) (not (p2 c_3 c_0 c_3)) )(or (p2 c_3 c_0 c_0) (= c_4 c_0) (not (p2 c_0 c_4 c_0)) (= c_0 c_4) (= c_3 c_4) (not (p2 c_3 c_0 c_4)) )(or (p2 c_3 c_0 c_1) (= c_0 c_1) (not (p2 c_0 c_0 c_1)) (= c_0 c_0) (= c_3 c_0) (not (p2 c_3 c_0 c_0)) )(or (p2 c_3 c_0 c_1) (= c_1 c_1) (not (p2 c_0 c_1 c_1)) (= c_0 c_1) (= c_3 c_1) (not (p2 c_3 c_0 c_1)) )(or (p2 c_3 c_0 c_1) (= c_2 c_1) (not (p2 c_0 c_2 c_1)) (= c_0 c_2) (= c_3 c_2) (not (p2 c_3 c_0 c_2)) )(or (p2 c_3 c_0 c_1) (= c_3 c_1) (not (p2 c_0 c_3 c_1)) (= c_0 c_3) (= c_3 c_3) (not (p2 c_3 c_0 c_3)) )(or (p2 c_3 c_0 c_1) (= c_4 c_1) (not (p2 c_0 c_4 c_1)) (= c_0 c_4) (= c_3 c_4) (not (p2 c_3 c_0 c_4)) )(or (p2 c_3 c_0 c_2) (= c_0 c_2) (not (p2 c_0 c_0 c_2)) (= c_0 c_0) (= c_3 c_0) (not (p2 c_3 c_0 c_0)) )(or (p2 c_3 c_0 c_2) (= c_1 c_2) (not (p2 c_0 c_1 c_2)) (= c_0 c_1) (= c_3 c_1) (not (p2 c_3 c_0 c_1)) )(or (p2 c_3 c_0 c_2) (= c_2 c_2) (not (p2 c_0 c_2 c_2)) (= c_0 c_2) (= c_3 c_2) (not (p2 c_3 c_0 c_2)) )(or (p2 c_3 c_0 c_2) (= c_3 c_2) (not (p2 c_0 c_3 c_2)) (= c_0 c_3) (= c_3 c_3) (not (p2 c_3 c_0 c_3)) )(or (p2 c_3 c_0 c_2) (= c_4 c_2) (not (p2 c_0 c_4 c_2)) (= c_0 c_4) (= c_3 c_4) (not (p2 c_3 c_0 c_4)) )(or (p2 c_3 c_0 c_3) (= c_0 c_3) (not (p2 c_0 c_0 c_3)) (= c_0 c_0) (= c_3 c_0) (not (p2 c_3 c_0 c_0)) )(or (p2 c_3 c_0 c_3) (= c_1 c_3) (not (p2 c_0 c_1 c_3)) (= c_0 c_1) (= c_3 c_1) (not (p2 c_3 c_0 c_1)) )(or (p2 c_3 c_0 c_3) (= c_2 c_3) (not (p2 c_0 c_2 c_3)) (= c_0 c_2) (= c_3 c_2) (not (p2 c_3 c_0 c_2)) )(or (p2 c_3 c_0 c_3) (= c_3 c_3) (not (p2 c_0 c_3 c_3)) (= c_0 c_3) (= c_3 c_3) (not (p2 c_3 c_0 c_3)) )(or (p2 c_3 c_0 c_3) (= c_4 c_3) (not (p2 c_0 c_4 c_3)) (= c_0 c_4) (= c_3 c_4) (not (p2 c_3 c_0 c_4)) )(or (p2 c_3 c_0 c_4) (= c_0 c_4) (not (p2 c_0 c_0 c_4)) (= c_0 c_0) (= c_3 c_0) (not (p2 c_3 c_0 c_0)) )(or (p2 c_3 c_0 c_4) (= c_1 c_4) (not (p2 c_0 c_1 c_4)) (= c_0 c_1) (= c_3 c_1) (not (p2 c_3 c_0 c_1)) )(or (p2 c_3 c_0 c_4) (= c_2 c_4) (not (p2 c_0 c_2 c_4)) (= c_0 c_2) (= c_3 c_2) (not (p2 c_3 c_0 c_2)) )(or (p2 c_3 c_0 c_4) (= c_3 c_4) (not (p2 c_0 c_3 c_4)) (= c_0 c_3) (= c_3 c_3) (not (p2 c_3 c_0 c_3)) )(or (p2 c_3 c_0 c_4) (= c_4 c_4) (not (p2 c_0 c_4 c_4)) (= c_0 c_4) (= c_3 c_4) (not (p2 c_3 c_0 c_4)) )(or (p2 c_3 c_1 c_0) (= c_0 c_0) (not (p2 c_1 c_0 c_0)) (= c_1 c_0) (= c_3 c_0) (not (p2 c_3 c_1 c_0)) )(or (p2 c_3 c_1 c_0) (= c_1 c_0) (not (p2 c_1 c_1 c_0)) (= c_1 c_1) (= c_3 c_1) (not (p2 c_3 c_1 c_1)) )(or (p2 c_3 c_1 c_0) (= c_2 c_0) (not (p2 c_1 c_2 c_0)) (= c_1 c_2) (= c_3 c_2) (not (p2 c_3 c_1 c_2)) )(or (p2 c_3 c_1 c_0) (= c_3 c_0) (not (p2 c_1 c_3 c_0)) (= c_1 c_3) (= c_3 c_3) (not (p2 c_3 c_1 c_3)) )(or (p2 c_3 c_1 c_0) (= c_4 c_0) (not (p2 c_1 c_4 c_0)) (= c_1 c_4) (= c_3 c_4) (not (p2 c_3 c_1 c_4)) )(or (p2 c_3 c_1 c_1) (= c_0 c_1) (not (p2 c_1 c_0 c_1)) (= c_1 c_0) (= c_3 c_0) (not (p2 c_3 c_1 c_0)) )(or (p2 c_3 c_1 c_1) (= c_1 c_1) (not (p2 c_1 c_1 c_1)) (= c_1 c_1) (= c_3 c_1) (not (p2 c_3 c_1 c_1)) )(or (p2 c_3 c_1 c_1) (= c_2 c_1) (not (p2 c_1 c_2 c_1)) (= c_1 c_2) (= c_3 c_2) (not (p2 c_3 c_1 c_2)) )(or (p2 c_3 c_1 c_1) (= c_3 c_1) (not (p2 c_1 c_3 c_1)) (= c_1 c_3) (= c_3 c_3) (not (p2 c_3 c_1 c_3)) )(or (p2 c_3 c_1 c_1) (= c_4 c_1) (not (p2 c_1 c_4 c_1)) (= c_1 c_4) (= c_3 c_4) (not (p2 c_3 c_1 c_4)) )(or (p2 c_3 c_1 c_2) (= c_0 c_2) (not (p2 c_1 c_0 c_2)) (= c_1 c_0) (= c_3 c_0) (not (p2 c_3 c_1 c_0)) )(or (p2 c_3 c_1 c_2) (= c_1 c_2) (not (p2 c_1 c_1 c_2)) (= c_1 c_1) (= c_3 c_1) (not (p2 c_3 c_1 c_1)) )(or (p2 c_3 c_1 c_2) (= c_2 c_2) (not (p2 c_1 c_2 c_2)) (= c_1 c_2) (= c_3 c_2) (not (p2 c_3 c_1 c_2)) )(or (p2 c_3 c_1 c_2) (= c_3 c_2) (not (p2 c_1 c_3 c_2)) (= c_1 c_3) (= c_3 c_3) (not (p2 c_3 c_1 c_3)) )(or (p2 c_3 c_1 c_2) (= c_4 c_2) (not (p2 c_1 c_4 c_2)) (= c_1 c_4) (= c_3 c_4) (not (p2 c_3 c_1 c_4)) )(or (p2 c_3 c_1 c_3) (= c_0 c_3) (not (p2 c_1 c_0 c_3)) (= c_1 c_0) (= c_3 c_0) (not (p2 c_3 c_1 c_0)) )(or (p2 c_3 c_1 c_3) (= c_1 c_3) (not (p2 c_1 c_1 c_3)) (= c_1 c_1) (= c_3 c_1) (not (p2 c_3 c_1 c_1)) )(or (p2 c_3 c_1 c_3) (= c_2 c_3) (not (p2 c_1 c_2 c_3)) (= c_1 c_2) (= c_3 c_2) (not (p2 c_3 c_1 c_2)) )(or (p2 c_3 c_1 c_3) (= c_3 c_3) (not (p2 c_1 c_3 c_3)) (= c_1 c_3) (= c_3 c_3) (not (p2 c_3 c_1 c_3)) )(or (p2 c_3 c_1 c_3) (= c_4 c_3) (not (p2 c_1 c_4 c_3)) (= c_1 c_4) (= c_3 c_4) (not (p2 c_3 c_1 c_4)) )(or (p2 c_3 c_1 c_4) (= c_0 c_4) (not (p2 c_1 c_0 c_4)) (= c_1 c_0) (= c_3 c_0) (not (p2 c_3 c_1 c_0)) )(or (p2 c_3 c_1 c_4) (= c_1 c_4) (not (p2 c_1 c_1 c_4)) (= c_1 c_1) (= c_3 c_1) (not (p2 c_3 c_1 c_1)) )(or (p2 c_3 c_1 c_4) (= c_2 c_4) (not (p2 c_1 c_2 c_4)) (= c_1 c_2) (= c_3 c_2) (not (p2 c_3 c_1 c_2)) )(or (p2 c_3 c_1 c_4) (= c_3 c_4) (not (p2 c_1 c_3 c_4)) (= c_1 c_3) (= c_3 c_3) (not (p2 c_3 c_1 c_3)) )(or (p2 c_3 c_1 c_4) (= c_4 c_4) (not (p2 c_1 c_4 c_4)) (= c_1 c_4) (= c_3 c_4) (not (p2 c_3 c_1 c_4)) )(or (p2 c_3 c_2 c_0) (= c_0 c_0) (not (p2 c_2 c_0 c_0)) (= c_2 c_0) (= c_3 c_0) (not (p2 c_3 c_2 c_0)) )(or (p2 c_3 c_2 c_0) (= c_1 c_0) (not (p2 c_2 c_1 c_0)) (= c_2 c_1) (= c_3 c_1) (not (p2 c_3 c_2 c_1)) )(or (p2 c_3 c_2 c_0) (= c_2 c_0) (not (p2 c_2 c_2 c_0)) (= c_2 c_2) (= c_3 c_2) (not (p2 c_3 c_2 c_2)) )(or (p2 c_3 c_2 c_0) (= c_3 c_0) (not (p2 c_2 c_3 c_0)) (= c_2 c_3) (= c_3 c_3) (not (p2 c_3 c_2 c_3)) )(or (p2 c_3 c_2 c_0) (= c_4 c_0) (not (p2 c_2 c_4 c_0)) (= c_2 c_4) (= c_3 c_4) (not (p2 c_3 c_2 c_4)) )(or (p2 c_3 c_2 c_1) (= c_0 c_1) (not (p2 c_2 c_0 c_1)) (= c_2 c_0) (= c_3 c_0) (not (p2 c_3 c_2 c_0)) )(or (p2 c_3 c_2 c_1) (= c_1 c_1) (not (p2 c_2 c_1 c_1)) (= c_2 c_1) (= c_3 c_1) (not (p2 c_3 c_2 c_1)) )(or (p2 c_3 c_2 c_1) (= c_2 c_1) (not (p2 c_2 c_2 c_1)) (= c_2 c_2) (= c_3 c_2) (not (p2 c_3 c_2 c_2)) )(or (p2 c_3 c_2 c_1) (= c_3 c_1) (not (p2 c_2 c_3 c_1)) (= c_2 c_3) (= c_3 c_3) (not (p2 c_3 c_2 c_3)) )(or (p2 c_3 c_2 c_1) (= c_4 c_1) (not (p2 c_2 c_4 c_1)) (= c_2 c_4) (= c_3 c_4) (not (p2 c_3 c_2 c_4)) )(or (p2 c_3 c_2 c_2) (= c_0 c_2) (not (p2 c_2 c_0 c_2)) (= c_2 c_0) (= c_3 c_0) (not (p2 c_3 c_2 c_0)) )(or (p2 c_3 c_2 c_2) (= c_1 c_2) (not (p2 c_2 c_1 c_2)) (= c_2 c_1) (= c_3 c_1) (not (p2 c_3 c_2 c_1)) )(or (p2 c_3 c_2 c_2) (= c_2 c_2) (not (p2 c_2 c_2 c_2)) (= c_2 c_2) (= c_3 c_2) (not (p2 c_3 c_2 c_2)) )(or (p2 c_3 c_2 c_2) (= c_3 c_2) (not (p2 c_2 c_3 c_2)) (= c_2 c_3) (= c_3 c_3) (not (p2 c_3 c_2 c_3)) )(or (p2 c_3 c_2 c_2) (= c_4 c_2) (not (p2 c_2 c_4 c_2)) (= c_2 c_4) (= c_3 c_4) (not (p2 c_3 c_2 c_4)) )(or (p2 c_3 c_2 c_3) (= c_0 c_3) (not (p2 c_2 c_0 c_3)) (= c_2 c_0) (= c_3 c_0) (not (p2 c_3 c_2 c_0)) )(or (p2 c_3 c_2 c_3) (= c_1 c_3) (not (p2 c_2 c_1 c_3)) (= c_2 c_1) (= c_3 c_1) (not (p2 c_3 c_2 c_1)) )(or (p2 c_3 c_2 c_3) (= c_2 c_3) (not (p2 c_2 c_2 c_3)) (= c_2 c_2) (= c_3 c_2) (not (p2 c_3 c_2 c_2)) )(or (p2 c_3 c_2 c_3) (= c_3 c_3) (not (p2 c_2 c_3 c_3)) (= c_2 c_3) (= c_3 c_3) (not (p2 c_3 c_2 c_3)) )(or (p2 c_3 c_2 c_3) (= c_4 c_3) (not (p2 c_2 c_4 c_3)) (= c_2 c_4) (= c_3 c_4) (not (p2 c_3 c_2 c_4)) )(or (p2 c_3 c_2 c_4) (= c_0 c_4) (not (p2 c_2 c_0 c_4)) (= c_2 c_0) (= c_3 c_0) (not (p2 c_3 c_2 c_0)) )(or (p2 c_3 c_2 c_4) (= c_1 c_4) (not (p2 c_2 c_1 c_4)) (= c_2 c_1) (= c_3 c_1) (not (p2 c_3 c_2 c_1)) )(or (p2 c_3 c_2 c_4) (= c_2 c_4) (not (p2 c_2 c_2 c_4)) (= c_2 c_2) (= c_3 c_2) (not (p2 c_3 c_2 c_2)) )(or (p2 c_3 c_2 c_4) (= c_3 c_4) (not (p2 c_2 c_3 c_4)) (= c_2 c_3) (= c_3 c_3) (not (p2 c_3 c_2 c_3)) )(or (p2 c_3 c_2 c_4) (= c_4 c_4) (not (p2 c_2 c_4 c_4)) (= c_2 c_4) (= c_3 c_4) (not (p2 c_3 c_2 c_4)) )(or (p2 c_3 c_3 c_0) (= c_0 c_0) (not (p2 c_3 c_0 c_0)) (= c_3 c_0) (= c_3 c_0) (not (p2 c_3 c_3 c_0)) )(or (p2 c_3 c_3 c_0) (= c_1 c_0) (not (p2 c_3 c_1 c_0)) (= c_3 c_1) (= c_3 c_1) (not (p2 c_3 c_3 c_1)) )(or (p2 c_3 c_3 c_0) (= c_2 c_0) (not (p2 c_3 c_2 c_0)) (= c_3 c_2) (= c_3 c_2) (not (p2 c_3 c_3 c_2)) )(or (p2 c_3 c_3 c_0) (= c_3 c_0) (not (p2 c_3 c_3 c_0)) (= c_3 c_3) (= c_3 c_3) (not (p2 c_3 c_3 c_3)) )(or (p2 c_3 c_3 c_0) (= c_4 c_0) (not (p2 c_3 c_4 c_0)) (= c_3 c_4) (= c_3 c_4) (not (p2 c_3 c_3 c_4)) )(or (p2 c_3 c_3 c_1) (= c_0 c_1) (not (p2 c_3 c_0 c_1)) (= c_3 c_0) (= c_3 c_0) (not (p2 c_3 c_3 c_0)) )(or (p2 c_3 c_3 c_1) (= c_1 c_1) (not (p2 c_3 c_1 c_1)) (= c_3 c_1) (= c_3 c_1) (not (p2 c_3 c_3 c_1)) )(or (p2 c_3 c_3 c_1) (= c_2 c_1) (not (p2 c_3 c_2 c_1)) (= c_3 c_2) (= c_3 c_2) (not (p2 c_3 c_3 c_2)) )(or (p2 c_3 c_3 c_1) (= c_3 c_1) (not (p2 c_3 c_3 c_1)) (= c_3 c_3) (= c_3 c_3) (not (p2 c_3 c_3 c_3)) )(or (p2 c_3 c_3 c_1) (= c_4 c_1) (not (p2 c_3 c_4 c_1)) (= c_3 c_4) (= c_3 c_4) (not (p2 c_3 c_3 c_4)) )(or (p2 c_3 c_3 c_2) (= c_0 c_2) (not (p2 c_3 c_0 c_2)) (= c_3 c_0) (= c_3 c_0) (not (p2 c_3 c_3 c_0)) )(or (p2 c_3 c_3 c_2) (= c_1 c_2) (not (p2 c_3 c_1 c_2)) (= c_3 c_1) (= c_3 c_1) (not (p2 c_3 c_3 c_1)) )(or (p2 c_3 c_3 c_2) (= c_2 c_2) (not (p2 c_3 c_2 c_2)) (= c_3 c_2) (= c_3 c_2) (not (p2 c_3 c_3 c_2)) )(or (p2 c_3 c_3 c_2) (= c_3 c_2) (not (p2 c_3 c_3 c_2)) (= c_3 c_3) (= c_3 c_3) (not (p2 c_3 c_3 c_3)) )(or (p2 c_3 c_3 c_2) (= c_4 c_2) (not (p2 c_3 c_4 c_2)) (= c_3 c_4) (= c_3 c_4) (not (p2 c_3 c_3 c_4)) )(or (p2 c_3 c_3 c_3) (= c_0 c_3) (not (p2 c_3 c_0 c_3)) (= c_3 c_0) (= c_3 c_0) (not (p2 c_3 c_3 c_0)) )(or (p2 c_3 c_3 c_3) (= c_1 c_3) (not (p2 c_3 c_1 c_3)) (= c_3 c_1) (= c_3 c_1) (not (p2 c_3 c_3 c_1)) )(or (p2 c_3 c_3 c_3) (= c_2 c_3) (not (p2 c_3 c_2 c_3)) (= c_3 c_2) (= c_3 c_2) (not (p2 c_3 c_3 c_2)) )(or (p2 c_3 c_3 c_3) (= c_3 c_3) (not (p2 c_3 c_3 c_3)) (= c_3 c_3) (= c_3 c_3) (not (p2 c_3 c_3 c_3)) )(or (p2 c_3 c_3 c_3) (= c_4 c_3) (not (p2 c_3 c_4 c_3)) (= c_3 c_4) (= c_3 c_4) (not (p2 c_3 c_3 c_4)) )(or (p2 c_3 c_3 c_4) (= c_0 c_4) (not (p2 c_3 c_0 c_4)) (= c_3 c_0) (= c_3 c_0) (not (p2 c_3 c_3 c_0)) )(or (p2 c_3 c_3 c_4) (= c_1 c_4) (not (p2 c_3 c_1 c_4)) (= c_3 c_1) (= c_3 c_1) (not (p2 c_3 c_3 c_1)) )(or (p2 c_3 c_3 c_4) (= c_2 c_4) (not (p2 c_3 c_2 c_4)) (= c_3 c_2) (= c_3 c_2) (not (p2 c_3 c_3 c_2)) )(or (p2 c_3 c_3 c_4) (= c_3 c_4) (not (p2 c_3 c_3 c_4)) (= c_3 c_3) (= c_3 c_3) (not (p2 c_3 c_3 c_3)) )(or (p2 c_3 c_3 c_4) (= c_4 c_4) (not (p2 c_3 c_4 c_4)) (= c_3 c_4) (= c_3 c_4) (not (p2 c_3 c_3 c_4)) )(or (p2 c_3 c_4 c_0) (= c_0 c_0) (not (p2 c_4 c_0 c_0)) (= c_4 c_0) (= c_3 c_0) (not (p2 c_3 c_4 c_0)) )(or (p2 c_3 c_4 c_0) (= c_1 c_0) (not (p2 c_4 c_1 c_0)) (= c_4 c_1) (= c_3 c_1) (not (p2 c_3 c_4 c_1)) )(or (p2 c_3 c_4 c_0) (= c_2 c_0) (not (p2 c_4 c_2 c_0)) (= c_4 c_2) (= c_3 c_2) (not (p2 c_3 c_4 c_2)) )(or (p2 c_3 c_4 c_0) (= c_3 c_0) (not (p2 c_4 c_3 c_0)) (= c_4 c_3) (= c_3 c_3) (not (p2 c_3 c_4 c_3)) )(or (p2 c_3 c_4 c_0) (= c_4 c_0) (not (p2 c_4 c_4 c_0)) (= c_4 c_4) (= c_3 c_4) (not (p2 c_3 c_4 c_4)) )(or (p2 c_3 c_4 c_1) (= c_0 c_1) (not (p2 c_4 c_0 c_1)) (= c_4 c_0) (= c_3 c_0) (not (p2 c_3 c_4 c_0)) )(or (p2 c_3 c_4 c_1) (= c_1 c_1) (not (p2 c_4 c_1 c_1)) (= c_4 c_1) (= c_3 c_1) (not (p2 c_3 c_4 c_1)) )(or (p2 c_3 c_4 c_1) (= c_2 c_1) (not (p2 c_4 c_2 c_1)) (= c_4 c_2) (= c_3 c_2) (not (p2 c_3 c_4 c_2)) )(or (p2 c_3 c_4 c_1) (= c_3 c_1) (not (p2 c_4 c_3 c_1)) (= c_4 c_3) (= c_3 c_3) (not (p2 c_3 c_4 c_3)) )(or (p2 c_3 c_4 c_1) (= c_4 c_1) (not (p2 c_4 c_4 c_1)) (= c_4 c_4) (= c_3 c_4) (not (p2 c_3 c_4 c_4)) )(or (p2 c_3 c_4 c_2) (= c_0 c_2) (not (p2 c_4 c_0 c_2)) (= c_4 c_0) (= c_3 c_0) (not (p2 c_3 c_4 c_0)) )(or (p2 c_3 c_4 c_2) (= c_1 c_2) (not (p2 c_4 c_1 c_2)) (= c_4 c_1) (= c_3 c_1) (not (p2 c_3 c_4 c_1)) )(or (p2 c_3 c_4 c_2) (= c_2 c_2) (not (p2 c_4 c_2 c_2)) (= c_4 c_2) (= c_3 c_2) (not (p2 c_3 c_4 c_2)) )(or (p2 c_3 c_4 c_2) (= c_3 c_2) (not (p2 c_4 c_3 c_2)) (= c_4 c_3) (= c_3 c_3) (not (p2 c_3 c_4 c_3)) )(or (p2 c_3 c_4 c_2) (= c_4 c_2) (not (p2 c_4 c_4 c_2)) (= c_4 c_4) (= c_3 c_4) (not (p2 c_3 c_4 c_4)) )(or (p2 c_3 c_4 c_3) (= c_0 c_3) (not (p2 c_4 c_0 c_3)) (= c_4 c_0) (= c_3 c_0) (not (p2 c_3 c_4 c_0)) )(or (p2 c_3 c_4 c_3) (= c_1 c_3) (not (p2 c_4 c_1 c_3)) (= c_4 c_1) (= c_3 c_1) (not (p2 c_3 c_4 c_1)) )(or (p2 c_3 c_4 c_3) (= c_2 c_3) (not (p2 c_4 c_2 c_3)) (= c_4 c_2) (= c_3 c_2) (not (p2 c_3 c_4 c_2)) )(or (p2 c_3 c_4 c_3) (= c_3 c_3) (not (p2 c_4 c_3 c_3)) (= c_4 c_3) (= c_3 c_3) (not (p2 c_3 c_4 c_3)) )(or (p2 c_3 c_4 c_3) (= c_4 c_3) (not (p2 c_4 c_4 c_3)) (= c_4 c_4) (= c_3 c_4) (not (p2 c_3 c_4 c_4)) )(or (p2 c_3 c_4 c_4) (= c_0 c_4) (not (p2 c_4 c_0 c_4)) (= c_4 c_0) (= c_3 c_0) (not (p2 c_3 c_4 c_0)) )(or (p2 c_3 c_4 c_4) (= c_1 c_4) (not (p2 c_4 c_1 c_4)) (= c_4 c_1) (= c_3 c_1) (not (p2 c_3 c_4 c_1)) )(or (p2 c_3 c_4 c_4) (= c_2 c_4) (not (p2 c_4 c_2 c_4)) (= c_4 c_2) (= c_3 c_2) (not (p2 c_3 c_4 c_2)) )(or (p2 c_3 c_4 c_4) (= c_3 c_4) (not (p2 c_4 c_3 c_4)) (= c_4 c_3) (= c_3 c_3) (not (p2 c_3 c_4 c_3)) )(or (p2 c_3 c_4 c_4) (= c_4 c_4) (not (p2 c_4 c_4 c_4)) (= c_4 c_4) (= c_3 c_4) (not (p2 c_3 c_4 c_4)) )(or (p2 c_4 c_0 c_0) (= c_0 c_0) (not (p2 c_0 c_0 c_0)) (= c_0 c_0) (= c_4 c_0) (not (p2 c_4 c_0 c_0)) )(or (p2 c_4 c_0 c_0) (= c_1 c_0) (not (p2 c_0 c_1 c_0)) (= c_0 c_1) (= c_4 c_1) (not (p2 c_4 c_0 c_1)) )(or (p2 c_4 c_0 c_0) (= c_2 c_0) (not (p2 c_0 c_2 c_0)) (= c_0 c_2) (= c_4 c_2) (not (p2 c_4 c_0 c_2)) )(or (p2 c_4 c_0 c_0) (= c_3 c_0) (not (p2 c_0 c_3 c_0)) (= c_0 c_3) (= c_4 c_3) (not (p2 c_4 c_0 c_3)) )(or (p2 c_4 c_0 c_0) (= c_4 c_0) (not (p2 c_0 c_4 c_0)) (= c_0 c_4) (= c_4 c_4) (not (p2 c_4 c_0 c_4)) )(or (p2 c_4 c_0 c_1) (= c_0 c_1) (not (p2 c_0 c_0 c_1)) (= c_0 c_0) (= c_4 c_0) (not (p2 c_4 c_0 c_0)) )(or (p2 c_4 c_0 c_1) (= c_1 c_1) (not (p2 c_0 c_1 c_1)) (= c_0 c_1) (= c_4 c_1) (not (p2 c_4 c_0 c_1)) )(or (p2 c_4 c_0 c_1) (= c_2 c_1) (not (p2 c_0 c_2 c_1)) (= c_0 c_2) (= c_4 c_2) (not (p2 c_4 c_0 c_2)) )(or (p2 c_4 c_0 c_1) (= c_3 c_1) (not (p2 c_0 c_3 c_1)) (= c_0 c_3) (= c_4 c_3) (not (p2 c_4 c_0 c_3)) )(or (p2 c_4 c_0 c_1) (= c_4 c_1) (not (p2 c_0 c_4 c_1)) (= c_0 c_4) (= c_4 c_4) (not (p2 c_4 c_0 c_4)) )(or (p2 c_4 c_0 c_2) (= c_0 c_2) (not (p2 c_0 c_0 c_2)) (= c_0 c_0) (= c_4 c_0) (not (p2 c_4 c_0 c_0)) )(or (p2 c_4 c_0 c_2) (= c_1 c_2) (not (p2 c_0 c_1 c_2)) (= c_0 c_1) (= c_4 c_1) (not (p2 c_4 c_0 c_1)) )(or (p2 c_4 c_0 c_2) (= c_2 c_2) (not (p2 c_0 c_2 c_2)) (= c_0 c_2) (= c_4 c_2) (not (p2 c_4 c_0 c_2)) )(or (p2 c_4 c_0 c_2) (= c_3 c_2) (not (p2 c_0 c_3 c_2)) (= c_0 c_3) (= c_4 c_3) (not (p2 c_4 c_0 c_3)) )(or (p2 c_4 c_0 c_2) (= c_4 c_2) (not (p2 c_0 c_4 c_2)) (= c_0 c_4) (= c_4 c_4) (not (p2 c_4 c_0 c_4)) )(or (p2 c_4 c_0 c_3) (= c_0 c_3) (not (p2 c_0 c_0 c_3)) (= c_0 c_0) (= c_4 c_0) (not (p2 c_4 c_0 c_0)) )(or (p2 c_4 c_0 c_3) (= c_1 c_3) (not (p2 c_0 c_1 c_3)) (= c_0 c_1) (= c_4 c_1) (not (p2 c_4 c_0 c_1)) )(or (p2 c_4 c_0 c_3) (= c_2 c_3) (not (p2 c_0 c_2 c_3)) (= c_0 c_2) (= c_4 c_2) (not (p2 c_4 c_0 c_2)) )(or (p2 c_4 c_0 c_3) (= c_3 c_3) (not (p2 c_0 c_3 c_3)) (= c_0 c_3) (= c_4 c_3) (not (p2 c_4 c_0 c_3)) )(or (p2 c_4 c_0 c_3) (= c_4 c_3) (not (p2 c_0 c_4 c_3)) (= c_0 c_4) (= c_4 c_4) (not (p2 c_4 c_0 c_4)) )(or (p2 c_4 c_0 c_4) (= c_0 c_4) (not (p2 c_0 c_0 c_4)) (= c_0 c_0) (= c_4 c_0) (not (p2 c_4 c_0 c_0)) )(or (p2 c_4 c_0 c_4) (= c_1 c_4) (not (p2 c_0 c_1 c_4)) (= c_0 c_1) (= c_4 c_1) (not (p2 c_4 c_0 c_1)) )(or (p2 c_4 c_0 c_4) (= c_2 c_4) (not (p2 c_0 c_2 c_4)) (= c_0 c_2) (= c_4 c_2) (not (p2 c_4 c_0 c_2)) )(or (p2 c_4 c_0 c_4) (= c_3 c_4) (not (p2 c_0 c_3 c_4)) (= c_0 c_3) (= c_4 c_3) (not (p2 c_4 c_0 c_3)) )(or (p2 c_4 c_0 c_4) (= c_4 c_4) (not (p2 c_0 c_4 c_4)) (= c_0 c_4) (= c_4 c_4) (not (p2 c_4 c_0 c_4)) )(or (p2 c_4 c_1 c_0) (= c_0 c_0) (not (p2 c_1 c_0 c_0)) (= c_1 c_0) (= c_4 c_0) (not (p2 c_4 c_1 c_0)) )(or (p2 c_4 c_1 c_0) (= c_1 c_0) (not (p2 c_1 c_1 c_0)) (= c_1 c_1) (= c_4 c_1) (not (p2 c_4 c_1 c_1)) )(or (p2 c_4 c_1 c_0) (= c_2 c_0) (not (p2 c_1 c_2 c_0)) (= c_1 c_2) (= c_4 c_2) (not (p2 c_4 c_1 c_2)) )(or (p2 c_4 c_1 c_0) (= c_3 c_0) (not (p2 c_1 c_3 c_0)) (= c_1 c_3) (= c_4 c_3) (not (p2 c_4 c_1 c_3)) )(or (p2 c_4 c_1 c_0) (= c_4 c_0) (not (p2 c_1 c_4 c_0)) (= c_1 c_4) (= c_4 c_4) (not (p2 c_4 c_1 c_4)) )(or (p2 c_4 c_1 c_1) (= c_0 c_1) (not (p2 c_1 c_0 c_1)) (= c_1 c_0) (= c_4 c_0) (not (p2 c_4 c_1 c_0)) )(or (p2 c_4 c_1 c_1) (= c_1 c_1) (not (p2 c_1 c_1 c_1)) (= c_1 c_1) (= c_4 c_1) (not (p2 c_4 c_1 c_1)) )(or (p2 c_4 c_1 c_1) (= c_2 c_1) (not (p2 c_1 c_2 c_1)) (= c_1 c_2) (= c_4 c_2) (not (p2 c_4 c_1 c_2)) )(or (p2 c_4 c_1 c_1) (= c_3 c_1) (not (p2 c_1 c_3 c_1)) (= c_1 c_3) (= c_4 c_3) (not (p2 c_4 c_1 c_3)) )(or (p2 c_4 c_1 c_1) (= c_4 c_1) (not (p2 c_1 c_4 c_1)) (= c_1 c_4) (= c_4 c_4) (not (p2 c_4 c_1 c_4)) )(or (p2 c_4 c_1 c_2) (= c_0 c_2) (not (p2 c_1 c_0 c_2)) (= c_1 c_0) (= c_4 c_0) (not (p2 c_4 c_1 c_0)) )(or (p2 c_4 c_1 c_2) (= c_1 c_2) (not (p2 c_1 c_1 c_2)) (= c_1 c_1) (= c_4 c_1) (not (p2 c_4 c_1 c_1)) )(or (p2 c_4 c_1 c_2) (= c_2 c_2) (not (p2 c_1 c_2 c_2)) (= c_1 c_2) (= c_4 c_2) (not (p2 c_4 c_1 c_2)) )(or (p2 c_4 c_1 c_2) (= c_3 c_2) (not (p2 c_1 c_3 c_2)) (= c_1 c_3) (= c_4 c_3) (not (p2 c_4 c_1 c_3)) )(or (p2 c_4 c_1 c_2) (= c_4 c_2) (not (p2 c_1 c_4 c_2)) (= c_1 c_4) (= c_4 c_4) (not (p2 c_4 c_1 c_4)) )(or (p2 c_4 c_1 c_3) (= c_0 c_3) (not (p2 c_1 c_0 c_3)) (= c_1 c_0) (= c_4 c_0) (not (p2 c_4 c_1 c_0)) )(or (p2 c_4 c_1 c_3) (= c_1 c_3) (not (p2 c_1 c_1 c_3)) (= c_1 c_1) (= c_4 c_1) (not (p2 c_4 c_1 c_1)) )(or (p2 c_4 c_1 c_3) (= c_2 c_3) (not (p2 c_1 c_2 c_3)) (= c_1 c_2) (= c_4 c_2) (not (p2 c_4 c_1 c_2)) )(or (p2 c_4 c_1 c_3) (= c_3 c_3) (not (p2 c_1 c_3 c_3)) (= c_1 c_3) (= c_4 c_3) (not (p2 c_4 c_1 c_3)) )(or (p2 c_4 c_1 c_3) (= c_4 c_3) (not (p2 c_1 c_4 c_3)) (= c_1 c_4) (= c_4 c_4) (not (p2 c_4 c_1 c_4)) )(or (p2 c_4 c_1 c_4) (= c_0 c_4) (not (p2 c_1 c_0 c_4)) (= c_1 c_0) (= c_4 c_0) (not (p2 c_4 c_1 c_0)) )(or (p2 c_4 c_1 c_4) (= c_1 c_4) (not (p2 c_1 c_1 c_4)) (= c_1 c_1) (= c_4 c_1) (not (p2 c_4 c_1 c_1)) )(or (p2 c_4 c_1 c_4) (= c_2 c_4) (not (p2 c_1 c_2 c_4)) (= c_1 c_2) (= c_4 c_2) (not (p2 c_4 c_1 c_2)) )(or (p2 c_4 c_1 c_4) (= c_3 c_4) (not (p2 c_1 c_3 c_4)) (= c_1 c_3) (= c_4 c_3) (not (p2 c_4 c_1 c_3)) )(or (p2 c_4 c_1 c_4) (= c_4 c_4) (not (p2 c_1 c_4 c_4)) (= c_1 c_4) (= c_4 c_4) (not (p2 c_4 c_1 c_4)) )(or (p2 c_4 c_2 c_0) (= c_0 c_0) (not (p2 c_2 c_0 c_0)) (= c_2 c_0) (= c_4 c_0) (not (p2 c_4 c_2 c_0)) )(or (p2 c_4 c_2 c_0) (= c_1 c_0) (not (p2 c_2 c_1 c_0)) (= c_2 c_1) (= c_4 c_1) (not (p2 c_4 c_2 c_1)) )(or (p2 c_4 c_2 c_0) (= c_2 c_0) (not (p2 c_2 c_2 c_0)) (= c_2 c_2) (= c_4 c_2) (not (p2 c_4 c_2 c_2)) )(or (p2 c_4 c_2 c_0) (= c_3 c_0) (not (p2 c_2 c_3 c_0)) (= c_2 c_3) (= c_4 c_3) (not (p2 c_4 c_2 c_3)) )(or (p2 c_4 c_2 c_0) (= c_4 c_0) (not (p2 c_2 c_4 c_0)) (= c_2 c_4) (= c_4 c_4) (not (p2 c_4 c_2 c_4)) )(or (p2 c_4 c_2 c_1) (= c_0 c_1) (not (p2 c_2 c_0 c_1)) (= c_2 c_0) (= c_4 c_0) (not (p2 c_4 c_2 c_0)) )(or (p2 c_4 c_2 c_1) (= c_1 c_1) (not (p2 c_2 c_1 c_1)) (= c_2 c_1) (= c_4 c_1) (not (p2 c_4 c_2 c_1)) )(or (p2 c_4 c_2 c_1) (= c_2 c_1) (not (p2 c_2 c_2 c_1)) (= c_2 c_2) (= c_4 c_2) (not (p2 c_4 c_2 c_2)) )(or (p2 c_4 c_2 c_1) (= c_3 c_1) (not (p2 c_2 c_3 c_1)) (= c_2 c_3) (= c_4 c_3) (not (p2 c_4 c_2 c_3)) )(or (p2 c_4 c_2 c_1) (= c_4 c_1) (not (p2 c_2 c_4 c_1)) (= c_2 c_4) (= c_4 c_4) (not (p2 c_4 c_2 c_4)) )(or (p2 c_4 c_2 c_2) (= c_0 c_2) (not (p2 c_2 c_0 c_2)) (= c_2 c_0) (= c_4 c_0) (not (p2 c_4 c_2 c_0)) )(or (p2 c_4 c_2 c_2) (= c_1 c_2) (not (p2 c_2 c_1 c_2)) (= c_2 c_1) (= c_4 c_1) (not (p2 c_4 c_2 c_1)) )(or (p2 c_4 c_2 c_2) (= c_2 c_2) (not (p2 c_2 c_2 c_2)) (= c_2 c_2) (= c_4 c_2) (not (p2 c_4 c_2 c_2)) )(or (p2 c_4 c_2 c_2) (= c_3 c_2) (not (p2 c_2 c_3 c_2)) (= c_2 c_3) (= c_4 c_3) (not (p2 c_4 c_2 c_3)) )(or (p2 c_4 c_2 c_2) (= c_4 c_2) (not (p2 c_2 c_4 c_2)) (= c_2 c_4) (= c_4 c_4) (not (p2 c_4 c_2 c_4)) )(or (p2 c_4 c_2 c_3) (= c_0 c_3) (not (p2 c_2 c_0 c_3)) (= c_2 c_0) (= c_4 c_0) (not (p2 c_4 c_2 c_0)) )(or (p2 c_4 c_2 c_3) (= c_1 c_3) (not (p2 c_2 c_1 c_3)) (= c_2 c_1) (= c_4 c_1) (not (p2 c_4 c_2 c_1)) )(or (p2 c_4 c_2 c_3) (= c_2 c_3) (not (p2 c_2 c_2 c_3)) (= c_2 c_2) (= c_4 c_2) (not (p2 c_4 c_2 c_2)) )(or (p2 c_4 c_2 c_3) (= c_3 c_3) (not (p2 c_2 c_3 c_3)) (= c_2 c_3) (= c_4 c_3) (not (p2 c_4 c_2 c_3)) )(or (p2 c_4 c_2 c_3) (= c_4 c_3) (not (p2 c_2 c_4 c_3)) (= c_2 c_4) (= c_4 c_4) (not (p2 c_4 c_2 c_4)) )(or (p2 c_4 c_2 c_4) (= c_0 c_4) (not (p2 c_2 c_0 c_4)) (= c_2 c_0) (= c_4 c_0) (not (p2 c_4 c_2 c_0)) )(or (p2 c_4 c_2 c_4) (= c_1 c_4) (not (p2 c_2 c_1 c_4)) (= c_2 c_1) (= c_4 c_1) (not (p2 c_4 c_2 c_1)) )(or (p2 c_4 c_2 c_4) (= c_2 c_4) (not (p2 c_2 c_2 c_4)) (= c_2 c_2) (= c_4 c_2) (not (p2 c_4 c_2 c_2)) )(or (p2 c_4 c_2 c_4) (= c_3 c_4) (not (p2 c_2 c_3 c_4)) (= c_2 c_3) (= c_4 c_3) (not (p2 c_4 c_2 c_3)) )(or (p2 c_4 c_2 c_4) (= c_4 c_4) (not (p2 c_2 c_4 c_4)) (= c_2 c_4) (= c_4 c_4) (not (p2 c_4 c_2 c_4)) )(or (p2 c_4 c_3 c_0) (= c_0 c_0) (not (p2 c_3 c_0 c_0)) (= c_3 c_0) (= c_4 c_0) (not (p2 c_4 c_3 c_0)) )(or (p2 c_4 c_3 c_0) (= c_1 c_0) (not (p2 c_3 c_1 c_0)) (= c_3 c_1) (= c_4 c_1) (not (p2 c_4 c_3 c_1)) )(or (p2 c_4 c_3 c_0) (= c_2 c_0) (not (p2 c_3 c_2 c_0)) (= c_3 c_2) (= c_4 c_2) (not (p2 c_4 c_3 c_2)) )(or (p2 c_4 c_3 c_0) (= c_3 c_0) (not (p2 c_3 c_3 c_0)) (= c_3 c_3) (= c_4 c_3) (not (p2 c_4 c_3 c_3)) )(or (p2 c_4 c_3 c_0) (= c_4 c_0) (not (p2 c_3 c_4 c_0)) (= c_3 c_4) (= c_4 c_4) (not (p2 c_4 c_3 c_4)) )(or (p2 c_4 c_3 c_1) (= c_0 c_1) (not (p2 c_3 c_0 c_1)) (= c_3 c_0) (= c_4 c_0) (not (p2 c_4 c_3 c_0)) )(or (p2 c_4 c_3 c_1) (= c_1 c_1) (not (p2 c_3 c_1 c_1)) (= c_3 c_1) (= c_4 c_1) (not (p2 c_4 c_3 c_1)) )(or (p2 c_4 c_3 c_1) (= c_2 c_1) (not (p2 c_3 c_2 c_1)) (= c_3 c_2) (= c_4 c_2) (not (p2 c_4 c_3 c_2)) )(or (p2 c_4 c_3 c_1) (= c_3 c_1) (not (p2 c_3 c_3 c_1)) (= c_3 c_3) (= c_4 c_3) (not (p2 c_4 c_3 c_3)) )(or (p2 c_4 c_3 c_1) (= c_4 c_1) (not (p2 c_3 c_4 c_1)) (= c_3 c_4) (= c_4 c_4) (not (p2 c_4 c_3 c_4)) )(or (p2 c_4 c_3 c_2) (= c_0 c_2) (not (p2 c_3 c_0 c_2)) (= c_3 c_0) (= c_4 c_0) (not (p2 c_4 c_3 c_0)) )(or (p2 c_4 c_3 c_2) (= c_1 c_2) (not (p2 c_3 c_1 c_2)) (= c_3 c_1) (= c_4 c_1) (not (p2 c_4 c_3 c_1)) )(or (p2 c_4 c_3 c_2) (= c_2 c_2) (not (p2 c_3 c_2 c_2)) (= c_3 c_2) (= c_4 c_2) (not (p2 c_4 c_3 c_2)) )(or (p2 c_4 c_3 c_2) (= c_3 c_2) (not (p2 c_3 c_3 c_2)) (= c_3 c_3) (= c_4 c_3) (not (p2 c_4 c_3 c_3)) )(or (p2 c_4 c_3 c_2) (= c_4 c_2) (not (p2 c_3 c_4 c_2)) (= c_3 c_4) (= c_4 c_4) (not (p2 c_4 c_3 c_4)) )(or (p2 c_4 c_3 c_3) (= c_0 c_3) (not (p2 c_3 c_0 c_3)) (= c_3 c_0) (= c_4 c_0) (not (p2 c_4 c_3 c_0)) )(or (p2 c_4 c_3 c_3) (= c_1 c_3) (not (p2 c_3 c_1 c_3)) (= c_3 c_1) (= c_4 c_1) (not (p2 c_4 c_3 c_1)) )(or (p2 c_4 c_3 c_3) (= c_2 c_3) (not (p2 c_3 c_2 c_3)) (= c_3 c_2) (= c_4 c_2) (not (p2 c_4 c_3 c_2)) )(or (p2 c_4 c_3 c_3) (= c_3 c_3) (not (p2 c_3 c_3 c_3)) (= c_3 c_3) (= c_4 c_3) (not (p2 c_4 c_3 c_3)) )(or (p2 c_4 c_3 c_3) (= c_4 c_3) (not (p2 c_3 c_4 c_3)) (= c_3 c_4) (= c_4 c_4) (not (p2 c_4 c_3 c_4)) )(or (p2 c_4 c_3 c_4) (= c_0 c_4) (not (p2 c_3 c_0 c_4)) (= c_3 c_0) (= c_4 c_0) (not (p2 c_4 c_3 c_0)) )(or (p2 c_4 c_3 c_4) (= c_1 c_4) (not (p2 c_3 c_1 c_4)) (= c_3 c_1) (= c_4 c_1) (not (p2 c_4 c_3 c_1)) )(or (p2 c_4 c_3 c_4) (= c_2 c_4) (not (p2 c_3 c_2 c_4)) (= c_3 c_2) (= c_4 c_2) (not (p2 c_4 c_3 c_2)) )(or (p2 c_4 c_3 c_4) (= c_3 c_4) (not (p2 c_3 c_3 c_4)) (= c_3 c_3) (= c_4 c_3) (not (p2 c_4 c_3 c_3)) )(or (p2 c_4 c_3 c_4) (= c_4 c_4) (not (p2 c_3 c_4 c_4)) (= c_3 c_4) (= c_4 c_4) (not (p2 c_4 c_3 c_4)) )(or (p2 c_4 c_4 c_0) (= c_0 c_0) (not (p2 c_4 c_0 c_0)) (= c_4 c_0) (= c_4 c_0) (not (p2 c_4 c_4 c_0)) )(or (p2 c_4 c_4 c_0) (= c_1 c_0) (not (p2 c_4 c_1 c_0)) (= c_4 c_1) (= c_4 c_1) (not (p2 c_4 c_4 c_1)) )(or (p2 c_4 c_4 c_0) (= c_2 c_0) (not (p2 c_4 c_2 c_0)) (= c_4 c_2) (= c_4 c_2) (not (p2 c_4 c_4 c_2)) )(or (p2 c_4 c_4 c_0) (= c_3 c_0) (not (p2 c_4 c_3 c_0)) (= c_4 c_3) (= c_4 c_3) (not (p2 c_4 c_4 c_3)) )(or (p2 c_4 c_4 c_0) (= c_4 c_0) (not (p2 c_4 c_4 c_0)) (= c_4 c_4) (= c_4 c_4) (not (p2 c_4 c_4 c_4)) )(or (p2 c_4 c_4 c_1) (= c_0 c_1) (not (p2 c_4 c_0 c_1)) (= c_4 c_0) (= c_4 c_0) (not (p2 c_4 c_4 c_0)) )(or (p2 c_4 c_4 c_1) (= c_1 c_1) (not (p2 c_4 c_1 c_1)) (= c_4 c_1) (= c_4 c_1) (not (p2 c_4 c_4 c_1)) )(or (p2 c_4 c_4 c_1) (= c_2 c_1) (not (p2 c_4 c_2 c_1)) (= c_4 c_2) (= c_4 c_2) (not (p2 c_4 c_4 c_2)) )(or (p2 c_4 c_4 c_1) (= c_3 c_1) (not (p2 c_4 c_3 c_1)) (= c_4 c_3) (= c_4 c_3) (not (p2 c_4 c_4 c_3)) )(or (p2 c_4 c_4 c_1) (= c_4 c_1) (not (p2 c_4 c_4 c_1)) (= c_4 c_4) (= c_4 c_4) (not (p2 c_4 c_4 c_4)) )(or (p2 c_4 c_4 c_2) (= c_0 c_2) (not (p2 c_4 c_0 c_2)) (= c_4 c_0) (= c_4 c_0) (not (p2 c_4 c_4 c_0)) )(or (p2 c_4 c_4 c_2) (= c_1 c_2) (not (p2 c_4 c_1 c_2)) (= c_4 c_1) (= c_4 c_1) (not (p2 c_4 c_4 c_1)) )(or (p2 c_4 c_4 c_2) (= c_2 c_2) (not (p2 c_4 c_2 c_2)) (= c_4 c_2) (= c_4 c_2) (not (p2 c_4 c_4 c_2)) )(or (p2 c_4 c_4 c_2) (= c_3 c_2) (not (p2 c_4 c_3 c_2)) (= c_4 c_3) (= c_4 c_3) (not (p2 c_4 c_4 c_3)) )(or (p2 c_4 c_4 c_2) (= c_4 c_2) (not (p2 c_4 c_4 c_2)) (= c_4 c_4) (= c_4 c_4) (not (p2 c_4 c_4 c_4)) )(or (p2 c_4 c_4 c_3) (= c_0 c_3) (not (p2 c_4 c_0 c_3)) (= c_4 c_0) (= c_4 c_0) (not (p2 c_4 c_4 c_0)) )(or (p2 c_4 c_4 c_3) (= c_1 c_3) (not (p2 c_4 c_1 c_3)) (= c_4 c_1) (= c_4 c_1) (not (p2 c_4 c_4 c_1)) )(or (p2 c_4 c_4 c_3) (= c_2 c_3) (not (p2 c_4 c_2 c_3)) (= c_4 c_2) (= c_4 c_2) (not (p2 c_4 c_4 c_2)) )(or (p2 c_4 c_4 c_3) (= c_3 c_3) (not (p2 c_4 c_3 c_3)) (= c_4 c_3) (= c_4 c_3) (not (p2 c_4 c_4 c_3)) )(or (p2 c_4 c_4 c_3) (= c_4 c_3) (not (p2 c_4 c_4 c_3)) (= c_4 c_4) (= c_4 c_4) (not (p2 c_4 c_4 c_4)) )(or (p2 c_4 c_4 c_4) (= c_0 c_4) (not (p2 c_4 c_0 c_4)) (= c_4 c_0) (= c_4 c_0) (not (p2 c_4 c_4 c_0)) )(or (p2 c_4 c_4 c_4) (= c_1 c_4) (not (p2 c_4 c_1 c_4)) (= c_4 c_1) (= c_4 c_1) (not (p2 c_4 c_4 c_1)) )(or (p2 c_4 c_4 c_4) (= c_2 c_4) (not (p2 c_4 c_2 c_4)) (= c_4 c_2) (= c_4 c_2) (not (p2 c_4 c_4 c_2)) )(or (p2 c_4 c_4 c_4) (= c_3 c_4) (not (p2 c_4 c_3 c_4)) (= c_4 c_3) (= c_4 c_3) (not (p2 c_4 c_4 c_3)) )(or (p2 c_4 c_4 c_4) (= c_4 c_4) (not (p2 c_4 c_4 c_4)) (= c_4 c_4) (= c_4 c_4) (not (p2 c_4 c_4 c_4)) )(p2 c_0 c_0 (f1 c_0 c_0)) (p2 c_0 c_1 (f1 c_0 c_1)) (p2 c_0 c_2 (f1 c_0 c_2)) (p2 c_0 c_3 (f1 c_0 c_3)) (p2 c_0 c_4 (f1 c_0 c_4)) (p2 c_1 c_0 (f1 c_1 c_0)) (p2 c_1 c_1 (f1 c_1 c_1)) (p2 c_1 c_2 (f1 c_1 c_2)) (p2 c_1 c_3 (f1 c_1 c_3)) (p2 c_1 c_4 (f1 c_1 c_4)) (p2 c_2 c_0 (f1 c_2 c_0)) (p2 c_2 c_1 (f1 c_2 c_1)) (p2 c_2 c_2 (f1 c_2 c_2)) (p2 c_2 c_3 (f1 c_2 c_3)) (p2 c_2 c_4 (f1 c_2 c_4)) (p2 c_3 c_0 (f1 c_3 c_0)) (p2 c_3 c_1 (f1 c_3 c_1)) (p2 c_3 c_2 (f1 c_3 c_2)) (p2 c_3 c_3 (f1 c_3 c_3)) (p2 c_3 c_4 (f1 c_3 c_4)) (p2 c_4 c_0 (f1 c_4 c_0)) (p2 c_4 c_1 (f1 c_4 c_1)) (p2 c_4 c_2 (f1 c_4 c_2)) (p2 c_4 c_3 (f1 c_4 c_3)) (p2 c_4 c_4 (f1 c_4 c_4)) (or (p2 c_0 c_0 c_0) (not (p2 c_0 c_0 c_0)) )(or (p2 c_0 c_0 c_1) (not (p2 c_0 c_0 c_1)) )(or (p2 c_0 c_0 c_2) (not (p2 c_0 c_0 c_2)) )(or (p2 c_0 c_0 c_3) (not (p2 c_0 c_0 c_3)) )(or (p2 c_0 c_0 c_4) (not (p2 c_0 c_0 c_4)) )(or (p2 c_0 c_1 c_0) (not (p2 c_1 c_0 c_0)) )(or (p2 c_0 c_1 c_1) (not (p2 c_1 c_0 c_1)) )(or (p2 c_0 c_1 c_2) (not (p2 c_1 c_0 c_2)) )(or (p2 c_0 c_1 c_3) (not (p2 c_1 c_0 c_3)) )(or (p2 c_0 c_1 c_4) (not (p2 c_1 c_0 c_4)) )(or (p2 c_0 c_2 c_0) (not (p2 c_2 c_0 c_0)) )(or (p2 c_0 c_2 c_1) (not (p2 c_2 c_0 c_1)) )(or (p2 c_0 c_2 c_2) (not (p2 c_2 c_0 c_2)) )(or (p2 c_0 c_2 c_3) (not (p2 c_2 c_0 c_3)) )(or (p2 c_0 c_2 c_4) (not (p2 c_2 c_0 c_4)) )(or (p2 c_0 c_3 c_0) (not (p2 c_3 c_0 c_0)) )(or (p2 c_0 c_3 c_1) (not (p2 c_3 c_0 c_1)) )(or (p2 c_0 c_3 c_2) (not (p2 c_3 c_0 c_2)) )(or (p2 c_0 c_3 c_3) (not (p2 c_3 c_0 c_3)) )(or (p2 c_0 c_3 c_4) (not (p2 c_3 c_0 c_4)) )(or (p2 c_0 c_4 c_0) (not (p2 c_4 c_0 c_0)) )(or (p2 c_0 c_4 c_1) (not (p2 c_4 c_0 c_1)) )(or (p2 c_0 c_4 c_2) (not (p2 c_4 c_0 c_2)) )(or (p2 c_0 c_4 c_3) (not (p2 c_4 c_0 c_3)) )(or (p2 c_0 c_4 c_4) (not (p2 c_4 c_0 c_4)) )(or (p2 c_1 c_0 c_0) (not (p2 c_0 c_1 c_0)) )(or (p2 c_1 c_0 c_1) (not (p2 c_0 c_1 c_1)) )(or (p2 c_1 c_0 c_2) (not (p2 c_0 c_1 c_2)) )(or (p2 c_1 c_0 c_3) (not (p2 c_0 c_1 c_3)) )(or (p2 c_1 c_0 c_4) (not (p2 c_0 c_1 c_4)) )(or (p2 c_1 c_1 c_0) (not (p2 c_1 c_1 c_0)) )(or (p2 c_1 c_1 c_1) (not (p2 c_1 c_1 c_1)) )(or (p2 c_1 c_1 c_2) (not (p2 c_1 c_1 c_2)) )(or (p2 c_1 c_1 c_3) (not (p2 c_1 c_1 c_3)) )(or (p2 c_1 c_1 c_4) (not (p2 c_1 c_1 c_4)) )(or (p2 c_1 c_2 c_0) (not (p2 c_2 c_1 c_0)) )(or (p2 c_1 c_2 c_1) (not (p2 c_2 c_1 c_1)) )(or (p2 c_1 c_2 c_2) (not (p2 c_2 c_1 c_2)) )(or (p2 c_1 c_2 c_3) (not (p2 c_2 c_1 c_3)) )(or (p2 c_1 c_2 c_4) (not (p2 c_2 c_1 c_4)) )(or (p2 c_1 c_3 c_0) (not (p2 c_3 c_1 c_0)) )(or (p2 c_1 c_3 c_1) (not (p2 c_3 c_1 c_1)) )(or (p2 c_1 c_3 c_2) (not (p2 c_3 c_1 c_2)) )(or (p2 c_1 c_3 c_3) (not (p2 c_3 c_1 c_3)) )(or (p2 c_1 c_3 c_4) (not (p2 c_3 c_1 c_4)) )(or (p2 c_1 c_4 c_0) (not (p2 c_4 c_1 c_0)) )(or (p2 c_1 c_4 c_1) (not (p2 c_4 c_1 c_1)) )(or (p2 c_1 c_4 c_2) (not (p2 c_4 c_1 c_2)) )(or (p2 c_1 c_4 c_3) (not (p2 c_4 c_1 c_3)) )(or (p2 c_1 c_4 c_4) (not (p2 c_4 c_1 c_4)) )(or (p2 c_2 c_0 c_0) (not (p2 c_0 c_2 c_0)) )(or (p2 c_2 c_0 c_1) (not (p2 c_0 c_2 c_1)) )(or (p2 c_2 c_0 c_2) (not (p2 c_0 c_2 c_2)) )(or (p2 c_2 c_0 c_3) (not (p2 c_0 c_2 c_3)) )(or (p2 c_2 c_0 c_4) (not (p2 c_0 c_2 c_4)) )(or (p2 c_2 c_1 c_0) (not (p2 c_1 c_2 c_0)) )(or (p2 c_2 c_1 c_1) (not (p2 c_1 c_2 c_1)) )(or (p2 c_2 c_1 c_2) (not (p2 c_1 c_2 c_2)) )(or (p2 c_2 c_1 c_3) (not (p2 c_1 c_2 c_3)) )(or (p2 c_2 c_1 c_4) (not (p2 c_1 c_2 c_4)) )(or (p2 c_2 c_2 c_0) (not (p2 c_2 c_2 c_0)) )(or (p2 c_2 c_2 c_1) (not (p2 c_2 c_2 c_1)) )(or (p2 c_2 c_2 c_2) (not (p2 c_2 c_2 c_2)) )(or (p2 c_2 c_2 c_3) (not (p2 c_2 c_2 c_3)) )(or (p2 c_2 c_2 c_4) (not (p2 c_2 c_2 c_4)) )(or (p2 c_2 c_3 c_0) (not (p2 c_3 c_2 c_0)) )(or (p2 c_2 c_3 c_1) (not (p2 c_3 c_2 c_1)) )(or (p2 c_2 c_3 c_2) (not (p2 c_3 c_2 c_2)) )(or (p2 c_2 c_3 c_3) (not (p2 c_3 c_2 c_3)) )(or (p2 c_2 c_3 c_4) (not (p2 c_3 c_2 c_4)) )(or (p2 c_2 c_4 c_0) (not (p2 c_4 c_2 c_0)) )(or (p2 c_2 c_4 c_1) (not (p2 c_4 c_2 c_1)) )(or (p2 c_2 c_4 c_2) (not (p2 c_4 c_2 c_2)) )(or (p2 c_2 c_4 c_3) (not (p2 c_4 c_2 c_3)) )(or (p2 c_2 c_4 c_4) (not (p2 c_4 c_2 c_4)) )(or (p2 c_3 c_0 c_0) (not (p2 c_0 c_3 c_0)) )(or (p2 c_3 c_0 c_1) (not (p2 c_0 c_3 c_1)) )(or (p2 c_3 c_0 c_2) (not (p2 c_0 c_3 c_2)) )(or (p2 c_3 c_0 c_3) (not (p2 c_0 c_3 c_3)) )(or (p2 c_3 c_0 c_4) (not (p2 c_0 c_3 c_4)) )(or (p2 c_3 c_1 c_0) (not (p2 c_1 c_3 c_0)) )(or (p2 c_3 c_1 c_1) (not (p2 c_1 c_3 c_1)) )(or (p2 c_3 c_1 c_2) (not (p2 c_1 c_3 c_2)) )(or (p2 c_3 c_1 c_3) (not (p2 c_1 c_3 c_3)) )(or (p2 c_3 c_1 c_4) (not (p2 c_1 c_3 c_4)) )(or (p2 c_3 c_2 c_0) (not (p2 c_2 c_3 c_0)) )(or (p2 c_3 c_2 c_1) (not (p2 c_2 c_3 c_1)) )(or (p2 c_3 c_2 c_2) (not (p2 c_2 c_3 c_2)) )(or (p2 c_3 c_2 c_3) (not (p2 c_2 c_3 c_3)) )(or (p2 c_3 c_2 c_4) (not (p2 c_2 c_3 c_4)) )(or (p2 c_3 c_3 c_0) (not (p2 c_3 c_3 c_0)) )(or (p2 c_3 c_3 c_1) (not (p2 c_3 c_3 c_1)) )(or (p2 c_3 c_3 c_2) (not (p2 c_3 c_3 c_2)) )(or (p2 c_3 c_3 c_3) (not (p2 c_3 c_3 c_3)) )(or (p2 c_3 c_3 c_4) (not (p2 c_3 c_3 c_4)) )(or (p2 c_3 c_4 c_0) (not (p2 c_4 c_3 c_0)) )(or (p2 c_3 c_4 c_1) (not (p2 c_4 c_3 c_1)) )(or (p2 c_3 c_4 c_2) (not (p2 c_4 c_3 c_2)) )(or (p2 c_3 c_4 c_3) (not (p2 c_4 c_3 c_3)) )(or (p2 c_3 c_4 c_4) (not (p2 c_4 c_3 c_4)) )(or (p2 c_4 c_0 c_0) (not (p2 c_0 c_4 c_0)) )(or (p2 c_4 c_0 c_1) (not (p2 c_0 c_4 c_1)) )(or (p2 c_4 c_0 c_2) (not (p2 c_0 c_4 c_2)) )(or (p2 c_4 c_0 c_3) (not (p2 c_0 c_4 c_3)) )(or (p2 c_4 c_0 c_4) (not (p2 c_0 c_4 c_4)) )(or (p2 c_4 c_1 c_0) (not (p2 c_1 c_4 c_0)) )(or (p2 c_4 c_1 c_1) (not (p2 c_1 c_4 c_1)) )(or (p2 c_4 c_1 c_2) (not (p2 c_1 c_4 c_2)) )(or (p2 c_4 c_1 c_3) (not (p2 c_1 c_4 c_3)) )(or (p2 c_4 c_1 c_4) (not (p2 c_1 c_4 c_4)) )(or (p2 c_4 c_2 c_0) (not (p2 c_2 c_4 c_0)) )(or (p2 c_4 c_2 c_1) (not (p2 c_2 c_4 c_1)) )(or (p2 c_4 c_2 c_2) (not (p2 c_2 c_4 c_2)) )(or (p2 c_4 c_2 c_3) (not (p2 c_2 c_4 c_3)) )(or (p2 c_4 c_2 c_4) (not (p2 c_2 c_4 c_4)) )(or (p2 c_4 c_3 c_0) (not (p2 c_3 c_4 c_0)) )(or (p2 c_4 c_3 c_1) (not (p2 c_3 c_4 c_1)) )(or (p2 c_4 c_3 c_2) (not (p2 c_3 c_4 c_2)) )(or (p2 c_4 c_3 c_3) (not (p2 c_3 c_4 c_3)) )(or (p2 c_4 c_3 c_4) (not (p2 c_3 c_4 c_4)) )(or (p2 c_4 c_4 c_0) (not (p2 c_4 c_4 c_0)) )(or (p2 c_4 c_4 c_1) (not (p2 c_4 c_4 c_1)) )(or (p2 c_4 c_4 c_2) (not (p2 c_4 c_4 c_2)) )(or (p2 c_4 c_4 c_3) (not (p2 c_4 c_4 c_3)) )(or (p2 c_4 c_4 c_4) (not (p2 c_4 c_4 c_4)) )(p2 c_0 c_0 c_0) (p2 c_0 c_0 c_1) (p2 c_0 c_0 c_2) (p2 c_0 c_0 c_3) (p2 c_0 c_0 c_4) (p2 c_1 c_1 c_0) (p2 c_1 c_1 c_1) (p2 c_1 c_1 c_2) (p2 c_1 c_1 c_3) (p2 c_1 c_1 c_4) (p2 c_2 c_2 c_0) (p2 c_2 c_2 c_1) (p2 c_2 c_2 c_2) (p2 c_2 c_2 c_3) (p2 c_2 c_2 c_4) (p2 c_3 c_3 c_0) (p2 c_3 c_3 c_1) (p2 c_3 c_3 c_2) (p2 c_3 c_3 c_3) (p2 c_3 c_3 c_4) (p2 c_4 c_4 c_0) (p2 c_4 c_4 c_1) (p2 c_4 c_4 c_2) (p2 c_4 c_4 c_3) (p2 c_4 c_4 c_4) (not (p2 c3 c4 c5)) (or (not (p2 c_0 c_0 c_0)) (p2 c_0 c_0 c_0) )(or (not (p2 c_0 c_0 c_1)) (p2 c_1 c_0 c_0) )(or (not (p2 c_0 c_0 c_2)) (p2 c_2 c_0 c_0) )(or (not (p2 c_0 c_0 c_3)) (p2 c_3 c_0 c_0) )(or (not (p2 c_0 c_0 c_4)) (p2 c_4 c_0 c_0) )(or (not (p2 c_0 c_1 c_0)) (p2 c_0 c_0 c_1) )(or (not (p2 c_0 c_1 c_1)) (p2 c_1 c_0 c_1) )(or (not (p2 c_0 c_1 c_2)) (p2 c_2 c_0 c_1) )(or (not (p2 c_0 c_1 c_3)) (p2 c_3 c_0 c_1) )(or (not (p2 c_0 c_1 c_4)) (p2 c_4 c_0 c_1) )(or (not (p2 c_0 c_2 c_0)) (p2 c_0 c_0 c_2) )(or (not (p2 c_0 c_2 c_1)) (p2 c_1 c_0 c_2) )(or (not (p2 c_0 c_2 c_2)) (p2 c_2 c_0 c_2) )(or (not (p2 c_0 c_2 c_3)) (p2 c_3 c_0 c_2) )(or (not (p2 c_0 c_2 c_4)) (p2 c_4 c_0 c_2) )(or (not (p2 c_0 c_3 c_0)) (p2 c_0 c_0 c_3) )(or (not (p2 c_0 c_3 c_1)) (p2 c_1 c_0 c_3) )(or (not (p2 c_0 c_3 c_2)) (p2 c_2 c_0 c_3) )(or (not (p2 c_0 c_3 c_3)) (p2 c_3 c_0 c_3) )(or (not (p2 c_0 c_3 c_4)) (p2 c_4 c_0 c_3) )(or (not (p2 c_0 c_4 c_0)) (p2 c_0 c_0 c_4) )(or (not (p2 c_0 c_4 c_1)) (p2 c_1 c_0 c_4) )(or (not (p2 c_0 c_4 c_2)) (p2 c_2 c_0 c_4) )(or (not (p2 c_0 c_4 c_3)) (p2 c_3 c_0 c_4) )(or (not (p2 c_0 c_4 c_4)) (p2 c_4 c_0 c_4) )(or (not (p2 c_1 c_0 c_0)) (p2 c_0 c_1 c_0) )(or (not (p2 c_1 c_0 c_1)) (p2 c_1 c_1 c_0) )(or (not (p2 c_1 c_0 c_2)) (p2 c_2 c_1 c_0) )(or (not (p2 c_1 c_0 c_3)) (p2 c_3 c_1 c_0) )(or (not (p2 c_1 c_0 c_4)) (p2 c_4 c_1 c_0) )(or (not (p2 c_1 c_1 c_0)) (p2 c_0 c_1 c_1) )(or (not (p2 c_1 c_1 c_1)) (p2 c_1 c_1 c_1) )(or (not (p2 c_1 c_1 c_2)) (p2 c_2 c_1 c_1) )(or (not (p2 c_1 c_1 c_3)) (p2 c_3 c_1 c_1) )(or (not (p2 c_1 c_1 c_4)) (p2 c_4 c_1 c_1) )(or (not (p2 c_1 c_2 c_0)) (p2 c_0 c_1 c_2) )(or (not (p2 c_1 c_2 c_1)) (p2 c_1 c_1 c_2) )(or (not (p2 c_1 c_2 c_2)) (p2 c_2 c_1 c_2) )(or (not (p2 c_1 c_2 c_3)) (p2 c_3 c_1 c_2) )(or (not (p2 c_1 c_2 c_4)) (p2 c_4 c_1 c_2) )(or (not (p2 c_1 c_3 c_0)) (p2 c_0 c_1 c_3) )(or (not (p2 c_1 c_3 c_1)) (p2 c_1 c_1 c_3) )(or (not (p2 c_1 c_3 c_2)) (p2 c_2 c_1 c_3) )(or (not (p2 c_1 c_3 c_3)) (p2 c_3 c_1 c_3) )(or (not (p2 c_1 c_3 c_4)) (p2 c_4 c_1 c_3) )(or (not (p2 c_1 c_4 c_0)) (p2 c_0 c_1 c_4) )(or (not (p2 c_1 c_4 c_1)) (p2 c_1 c_1 c_4) )(or (not (p2 c_1 c_4 c_2)) (p2 c_2 c_1 c_4) )(or (not (p2 c_1 c_4 c_3)) (p2 c_3 c_1 c_4) )(or (not (p2 c_1 c_4 c_4)) (p2 c_4 c_1 c_4) )(or (not (p2 c_2 c_0 c_0)) (p2 c_0 c_2 c_0) )(or (not (p2 c_2 c_0 c_1)) (p2 c_1 c_2 c_0) )(or (not (p2 c_2 c_0 c_2)) (p2 c_2 c_2 c_0) )(or (not (p2 c_2 c_0 c_3)) (p2 c_3 c_2 c_0) )(or (not (p2 c_2 c_0 c_4)) (p2 c_4 c_2 c_0) )(or (not (p2 c_2 c_1 c_0)) (p2 c_0 c_2 c_1) )(or (not (p2 c_2 c_1 c_1)) (p2 c_1 c_2 c_1) )(or (not (p2 c_2 c_1 c_2)) (p2 c_2 c_2 c_1) )(or (not (p2 c_2 c_1 c_3)) (p2 c_3 c_2 c_1) )(or (not (p2 c_2 c_1 c_4)) (p2 c_4 c_2 c_1) )(or (not (p2 c_2 c_2 c_0)) (p2 c_0 c_2 c_2) )(or (not (p2 c_2 c_2 c_1)) (p2 c_1 c_2 c_2) )(or (not (p2 c_2 c_2 c_2)) (p2 c_2 c_2 c_2) )(or (not (p2 c_2 c_2 c_3)) (p2 c_3 c_2 c_2) )(or (not (p2 c_2 c_2 c_4)) (p2 c_4 c_2 c_2) )(or (not (p2 c_2 c_3 c_0)) (p2 c_0 c_2 c_3) )(or (not (p2 c_2 c_3 c_1)) (p2 c_1 c_2 c_3) )(or (not (p2 c_2 c_3 c_2)) (p2 c_2 c_2 c_3) )(or (not (p2 c_2 c_3 c_3)) (p2 c_3 c_2 c_3) )(or (not (p2 c_2 c_3 c_4)) (p2 c_4 c_2 c_3) )(or (not (p2 c_2 c_4 c_0)) (p2 c_0 c_2 c_4) )(or (not (p2 c_2 c_4 c_1)) (p2 c_1 c_2 c_4) )(or (not (p2 c_2 c_4 c_2)) (p2 c_2 c_2 c_4) )(or (not (p2 c_2 c_4 c_3)) (p2 c_3 c_2 c_4) )(or (not (p2 c_2 c_4 c_4)) (p2 c_4 c_2 c_4) )(or (not (p2 c_3 c_0 c_0)) (p2 c_0 c_3 c_0) )(or (not (p2 c_3 c_0 c_1)) (p2 c_1 c_3 c_0) )(or (not (p2 c_3 c_0 c_2)) (p2 c_2 c_3 c_0) )(or (not (p2 c_3 c_0 c_3)) (p2 c_3 c_3 c_0) )(or (not (p2 c_3 c_0 c_4)) (p2 c_4 c_3 c_0) )(or (not (p2 c_3 c_1 c_0)) (p2 c_0 c_3 c_1) )(or (not (p2 c_3 c_1 c_1)) (p2 c_1 c_3 c_1) )(or (not (p2 c_3 c_1 c_2)) (p2 c_2 c_3 c_1) )(or (not (p2 c_3 c_1 c_3)) (p2 c_3 c_3 c_1) )(or (not (p2 c_3 c_1 c_4)) (p2 c_4 c_3 c_1) )(or (not (p2 c_3 c_2 c_0)) (p2 c_0 c_3 c_2) )(or (not (p2 c_3 c_2 c_1)) (p2 c_1 c_3 c_2) )(or (not (p2 c_3 c_2 c_2)) (p2 c_2 c_3 c_2) )(or (not (p2 c_3 c_2 c_3)) (p2 c_3 c_3 c_2) )(or (not (p2 c_3 c_2 c_4)) (p2 c_4 c_3 c_2) )(or (not (p2 c_3 c_3 c_0)) (p2 c_0 c_3 c_3) )(or (not (p2 c_3 c_3 c_1)) (p2 c_1 c_3 c_3) )(or (not (p2 c_3 c_3 c_2)) (p2 c_2 c_3 c_3) )(or (not (p2 c_3 c_3 c_3)) (p2 c_3 c_3 c_3) )(or (not (p2 c_3 c_3 c_4)) (p2 c_4 c_3 c_3) )(or (not (p2 c_3 c_4 c_0)) (p2 c_0 c_3 c_4) )(or (not (p2 c_3 c_4 c_1)) (p2 c_1 c_3 c_4) )(or (not (p2 c_3 c_4 c_2)) (p2 c_2 c_3 c_4) )(or (not (p2 c_3 c_4 c_3)) (p2 c_3 c_3 c_4) )(or (not (p2 c_3 c_4 c_4)) (p2 c_4 c_3 c_4) )(or (not (p2 c_4 c_0 c_0)) (p2 c_0 c_4 c_0) )(or (not (p2 c_4 c_0 c_1)) (p2 c_1 c_4 c_0) )(or (not (p2 c_4 c_0 c_2)) (p2 c_2 c_4 c_0) )(or (not (p2 c_4 c_0 c_3)) (p2 c_3 c_4 c_0) )(or (not (p2 c_4 c_0 c_4)) (p2 c_4 c_4 c_0) )(or (not (p2 c_4 c_1 c_0)) (p2 c_0 c_4 c_1) )(or (not (p2 c_4 c_1 c_1)) (p2 c_1 c_4 c_1) )(or (not (p2 c_4 c_1 c_2)) (p2 c_2 c_4 c_1) )(or (not (p2 c_4 c_1 c_3)) (p2 c_3 c_4 c_1) )(or (not (p2 c_4 c_1 c_4)) (p2 c_4 c_4 c_1) )(or (not (p2 c_4 c_2 c_0)) (p2 c_0 c_4 c_2) )(or (not (p2 c_4 c_2 c_1)) (p2 c_1 c_4 c_2) )(or (not (p2 c_4 c_2 c_2)) (p2 c_2 c_4 c_2) )(or (not (p2 c_4 c_2 c_3)) (p2 c_3 c_4 c_2) )(or (not (p2 c_4 c_2 c_4)) (p2 c_4 c_4 c_2) )(or (not (p2 c_4 c_3 c_0)) (p2 c_0 c_4 c_3) )(or (not (p2 c_4 c_3 c_1)) (p2 c_1 c_4 c_3) )(or (not (p2 c_4 c_3 c_2)) (p2 c_2 c_4 c_3) )(or (not (p2 c_4 c_3 c_3)) (p2 c_3 c_4 c_3) )(or (not (p2 c_4 c_3 c_4)) (p2 c_4 c_4 c_3) )(or (not (p2 c_4 c_4 c_0)) (p2 c_0 c_4 c_4) )(or (not (p2 c_4 c_4 c_1)) (p2 c_1 c_4 c_4) )(or (not (p2 c_4 c_4 c_2)) (p2 c_2 c_4 c_4) )(or (not (p2 c_4 c_4 c_3)) (p2 c_3 c_4 c_4) )(or (not (p2 c_4 c_4 c_4)) (p2 c_4 c_4 c_4) )(not (= c_0 (f1 c_0 c_0))) (not (= c_0 (f1 c_0 c_1))) (not (= c_0 (f1 c_0 c_2))) (not (= c_0 (f1 c_0 c_3))) (not (= c_0 (f1 c_0 c_4))) (not (= c_1 (f1 c_1 c_0))) (not (= c_1 (f1 c_1 c_1))) (not (= c_1 (f1 c_1 c_2))) (not (= c_1 (f1 c_1 c_3))) (not (= c_1 (f1 c_1 c_4))) (not (= c_2 (f1 c_2 c_0))) (not (= c_2 (f1 c_2 c_1))) (not (= c_2 (f1 c_2 c_2))) (not (= c_2 (f1 c_2 c_3))) (not (= c_2 (f1 c_2 c_4))) (not (= c_3 (f1 c_3 c_0))) (not (= c_3 (f1 c_3 c_1))) (not (= c_3 (f1 c_3 c_2))) (not (= c_3 (f1 c_3 c_3))) (not (= c_3 (f1 c_3 c_4))) (not (= c_4 (f1 c_4 c_0))) (not (= c_4 (f1 c_4 c_1))) (not (= c_4 (f1 c_4 c_2))) (not (= c_4 (f1 c_4 c_3))) (not (= c_4 (f1 c_4 c_4))) (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))(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))(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))(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))(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))(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))(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))(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))(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))(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))(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))(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))(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))(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))(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))(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))(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))(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))(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))(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))(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))(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))(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))(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))(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))(or (= c3 c_0)(= c3 c_1)(= c3 c_2)(= c3 c_3)(= c3 c_4))(or (= c4 c_0)(= c4 c_1)(= c4 c_2)(= c4 c_3)(= c4 c_4))(or (= c5 c_0)(= c5 c_1)(= c5 c_2)(= c5 c_3)(= c5 c_4))))