main = Clausify.Start
Clausify.Start = let a_1_0 = Clausify.Sym 0 in Clausify.display (Clausify.clausify (Clausify.foldr Clausify.Con a_1_0 (Clausify.replicate 80 (Clausify.eqv (Clausify.eqv a_1_0 (Clausify.eqv a_1_0 a_1_0)) (Clausify.eqv (Clausify.eqv a_1_0 (Clausify.eqv a_1_0 a_1_0)) (Clausify.eqv a_1_0 (Clausify.eqv a_1_0 a_1_0)))))))
Clausify.eqv a_0 b_1 = Clausify.Con (Clausify.Dis (Clausify.Neg a_0) b_1) (Clausify.Dis (Clausify.Neg b_1) a_0)
:: Clausify.P = Clausify.Sym a1 | Clausify.Neg a1 | Clausify.Con a1 a2 | Clausify.Dis a1 a2
Clausify.replicate !n_0 a_1 = if (eq n_0 0) Flite.Nil (Flite.Cons a_1 (Clausify.replicate (sub n_0 1) a_1))
:: Flite.List = Flite.Nil | Flite.Cons a1 a2
Clausify.foldr f_0 z_1 !_x_2 = select _x_2 (Flite.Nil -> z_1) (Flite.Cons x_1_0 xs_1_1 -> f_0 x_1_0 (Clausify.foldr f_0 z_1 xs_1_1)) 
Clausify.clausify !p_0 = Clausify.uniq_43 (Clausify.nonTaut_39 (Clausify.clauses (Clausify.split (Clausify.disin (Clausify.negin p_0)))))
Clausify.negin !_x_0 = select _x_0 (Clausify.Neg _x_1_0 -> select _x_1_0 (Clausify.Con p_2_0 q_2_1 -> Clausify.Dis (Clausify.negin (Clausify.Neg p_2_0)) (Clausify.negin (Clausify.Neg q_2_1))) (Clausify.Dis p_2_0 q_2_1 -> Clausify.Con (Clausify.negin (Clausify.Neg p_2_0)) (Clausify.negin (Clausify.Neg q_2_1))) (Clausify.Neg p_2_0 -> Clausify.negin p_2_0) (Clausify.Sym s_2_0 -> Clausify.Neg (Clausify.Sym s_2_0)) ) (Clausify.Dis p_1_0 q_1_1 -> Clausify.Dis (Clausify.negin p_1_0) (Clausify.negin q_1_1)) (Clausify.Con p_1_0 q_1_1 -> Clausify.Con (Clausify.negin p_1_0) (Clausify.negin q_1_1)) (Clausify.Sym s_1_0 -> Clausify.Sym s_1_0) 
Clausify.disin !_x_0 = select _x_0 (Clausify.Sym s_1_0 -> Clausify.Sym s_1_0) (Clausify.Neg p_1_0 -> Clausify.Neg p_1_0) (Clausify.Con p_1_0 q_1_1 -> Clausify.Con (Clausify.disin p_1_0) (Clausify.disin q_1_1)) (Clausify.Dis p_1_0 q_1_1 -> Clausify.din (Clausify.disin p_1_0) (Clausify.disin q_1_1)) 
Clausify.din !_x_0 r_1 = select _x_0 (Clausify.Con p_1_0 q_1_1 -> Clausify.Con (Clausify.din p_1_0 r_1) (Clausify.din q_1_1 r_1)) (Clausify.Dis p_1_0 q_1_1 -> Clausify.din2 (Clausify.Dis p_1_0 q_1_1) r_1) (Clausify.Neg p_1_0 -> Clausify.din2 (Clausify.Neg p_1_0) r_1) (Clausify.Sym s_1_0 -> Clausify.din2 (Clausify.Sym s_1_0) r_1) 
Clausify.din2 p_0 !_x_1 = select _x_1 (Clausify.Con q_1_0 r_1_1 -> Clausify.Con (Clausify.din p_0 q_1_0) (Clausify.din p_0 r_1_1)) (Clausify.Dis q_1_0 r_1_1 -> Clausify.Dis p_0 (Clausify.Dis q_1_0 r_1_1)) (Clausify.Neg q_1_0 -> Clausify.Dis p_0 (Clausify.Neg q_1_0)) (Clausify.Sym s_1_0 -> Clausify.Dis p_0 (Clausify.Sym s_1_0)) 
Clausify.split !p_0 = Clausify.spl Flite.Nil p_0
Clausify.spl a_0 !_x_1 = select _x_1 (Clausify.Con p_1_0 q_1_1 -> Clausify.spl (Clausify.spl a_0 p_1_0) q_1_1) (Clausify.Dis p_1_0 q_1_1 -> Flite.Cons (Clausify.Dis p_1_0 q_1_1) a_0) (Clausify.Neg p_1_0 -> Flite.Cons (Clausify.Neg p_1_0) a_0) (Clausify.Sym s_1_0 -> Flite.Cons (Clausify.Sym s_1_0) a_0) 
Clausify.clauses !ps_0 = Clausify.map (Clausify.clause (Flite.Pair Flite.Nil Flite.Nil)) ps_0
:: Flite.Pair = Flite.Pair a1 a2
Clausify.clause !_x_0 !_x_1 = select _x_0 (Flite.Pair c_1_0 a_1_1 -> select _x_1 (Clausify.Dis p_2_0 q_2_1 -> Clausify.clause (Clausify.clause (Flite.Pair c_1_0 a_1_1) p_2_0) q_2_1) (Clausify.Sym s_2_0 -> Flite.Pair (Clausify.ins_38 s_2_0 c_1_0) a_1_1) (Clausify.Neg _x_2_0 -> select _x_2_0 (Clausify.Sym s_3_0 -> Flite.Pair c_1_0 (Clausify.ins_38 s_3_0 a_1_1)) ) ) 
Clausify.ins_38 x_0 !_x_1 = select _x_1 (Flite.Nil -> Flite.Cons x_0 Flite.Nil) (Flite.Cons y_1_0 ys_1_1 -> if (eq x_0 y_1_0) (Flite.Cons y_1_0 ys_1_1) (if (<{Clausify.<=_37}> x_0 y_1_0) (Flite.Cons x_0 (Flite.Cons y_1_0 ys_1_1)) (Flite.Cons y_1_0 (Clausify.ins_38 x_0 ys_1_1)))) 
<{Clausify.<=_37}> !x_0 !y_1 = not (lt y_1 x_0)
Clausify.map f_0 !_x_1 = select _x_1 (Flite.Nil -> Flite.Nil) (Flite.Cons x_1_0 xs_1_1 -> Flite.Cons (f_0 x_1_0) (Clausify.map f_0 xs_1_1)) 
Clausify.nonTaut_39 !cs_0 = Clausify.filter Clausify.invTaut_40 cs_0
Clausify.invTaut_40 !_x_0 = select _x_0 (Flite.Pair c_1_0 a_1_1 -> Clausify.null (Clausify.inter eq c_1_0 a_1_1)) 
Clausify.inter eq_0 xs_1 !ys_2 = Clausify.filter (Clausify.contains eq_0 xs_1) ys_2
Clausify.contains eq_0 !_x_1 y_2 = select _x_1 (Flite.Nil -> False) (Flite.Cons x_1_0 xs_1_1 -> Clausify.or (eq_0 x_1_0 y_2) (Clausify.contains eq_0 xs_1_1 y_2)) 
Clausify.or !_x_0 x_1 = if _x_0 True x_1
Clausify.filter p_0 !_x_1 = select _x_1 (Flite.Nil -> Flite.Nil) (Flite.Cons x_1_0 xs_1_1 -> if (p_0 x_1_0) (Flite.Cons x_1_0 (Clausify.filter p_0 xs_1_1)) (Clausify.filter p_0 xs_1_1)) 
Clausify.null !_x_0 = select _x_0 (Flite.Nil -> True) (Flite.Cons x_1_0 xs_1_1 -> False) 
Clausify.uniq_43 !xs_0 = Clausify.foldr (Clausify.comp (Clausify.union Clausify.eqClause_44) Clausify.singleton) Flite.Nil xs_0
Clausify.singleton x_0 = Flite.Cons x_0 Flite.Nil
Clausify.eqClause_44 !_x_0 !_x_1 = select _x_0 (Flite.Pair a_1_0 b_1_1 -> select _x_1 (Flite.Pair c_2_0 d_2_1 -> Clausify.and (Clausify.eqList eq a_1_0 c_2_0) (Clausify.eqList eq b_1_1 d_2_1)) ) 
Clausify.eqList f_0 !_x_1 !_x_2 = select _x_1 (Flite.Nil -> select _x_2 (Flite.Nil -> True) (Flite.Cons y_2_0 ys_2_1 -> False) ) (Flite.Cons x_1_0 xs_1_1 -> select _x_2 (Flite.Nil -> False) (Flite.Cons y_2_0 ys_2_1 -> Clausify.and (f_0 x_1_0 y_2_0) (Clausify.eqList f_0 xs_1_1 ys_2_1)) ) 
Clausify.and !_x_0 x_1 = if _x_0 x_1 False
Clausify.union eq_0 !xs_1 ys_2 = Clausify.append xs_1 (Clausify.filter (Clausify.comp Clausify.inv (Clausify.contains eq_0 xs_1)) ys_2)
Clausify.inv !_x_0 = if _x_0 False True
Clausify.comp !f_0 g_1 x_2 = f_0 (g_1 x_2)
Clausify.append !_x_0 ys_1 = select _x_0 (Flite.Nil -> ys_1) (Flite.Cons x_1_0 xs_1_1 -> Flite.Cons x_1_0 (Clausify.append xs_1_1 ys_1)) 
Clausify.display !_x_0 = select _x_0 (Flite.Nil -> 0) (Flite.Cons c_1_0 cs_1_1 -> add (Clausify.emitClause c_1_0) (Clausify.display cs_1_1)) 
Clausify.emitClause !_x_0 = select _x_0 (Flite.Pair c_1_0 a_1_1 -> add (Clausify.sum c_1_0) (Clausify.sum a_1_1)) 
Clausify.sum !_x_0 = select _x_0 (Flite.Nil -> 0) (Flite.Cons x_1_0 xs_1_1 -> add x_1_0 (Clausify.sum xs_1_1))