main = Taut.Start
Taut.Start = if (Taut.isTaut Taut.testProp) 1 0
Taut.testProp = Taut.Implies (Taut.foldr1 Taut.And (Taut.map Taut.imp Taut.names)) (Taut.Implies (Taut.Var (Flite.char 'q')) (Taut.foldr1 Taut.And (Taut.map Taut.Var Taut.names)))
Taut.names = Flite.str "abcdefghijklmnop"
Flite.str !_x_0 = select _x_0 ("" -> Flite.Nil) (_ -> Flite.Cons (Flite.char (string_select _x_0 0)) (Flite.str (<{StdString.%_10}> _x_0 (_Tuple2 1 (string_size _x_0)))))
<{StdString.%_10}> !str_0 !_x_1 = select _x_1 (_Tuple2 a b -> string_slice str_0 a b)
Flite.char !c_0 = toInt_char c_0
:: Flite.List = Flite.Nil | Flite.Cons a1 a2
:: Taut.Prop = Taut.Const a1 | Taut.Var a1 | Taut.Not a1 | Taut.And a1 a2 | Taut.Implies a1 a2
Taut.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) (Taut.map f_0 xs_1_1)) 
Taut.foldr1 f_0 !_x_1 = select _x_1 (Flite.Cons x_1_0 xs_1_1 -> if (Taut.null xs_1_1) x_1_0 (f_0 x_1_0 (Taut.foldr1 f_0 xs_1_1))) 
Taut.null !_x_0 = select _x_0 (Flite.Nil -> True) (Flite.Cons x_1_0 xs_1_1 -> False) 
Taut.imp v_0 = Taut.Implies (Taut.Var (Flite.char 'q')) (Taut.Var v_0)
Taut.isTaut !p_0 = Taut.and (Taut.map (Taut.flip Taut.eval p_0) (Taut.substs p_0))
Taut.substs !p_0 = let vs_1_0 = Taut.rmdups_26 (Taut.vars p_0) in Taut.map (Taut.zip vs_1_0) (Taut.bools (Taut.len vs_1_0))
Taut.len !_x_0 = select _x_0 (Flite.Nil -> 0) (Flite.Cons x_1_0 xs_1_1 -> add 1 (Taut.len xs_1_1)) 
Taut.bools !n_0 = if (eq n_0 0) (Flite.Cons Flite.Nil Flite.Nil) (let m_1_0 = sub n_0 1 in Taut.append (Taut.map (Flite.Cons False) (Taut.bools m_1_0)) (Taut.map (Flite.Cons True) (Taut.bools m_1_0)))
Taut.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 (Taut.append xs_1_1 ys_1)) 
Taut.zip !_x_0 ys_1 = select _x_0 (Flite.Nil -> Flite.Nil) (Flite.Cons x_1_0 xs_1_1 -> select ys_1 (Flite.Nil -> Flite.Nil) (Flite.Cons y_2_0 ys_2_1 -> Flite.Cons (Flite.Pair x_1_0 y_2_0) (Taut.zip xs_1_1 ys_2_1)) ) 
:: Flite.Pair = Flite.Pair a1 a2
Taut.vars !_x_0 = select _x_0 (Taut.Const b_1_0 -> Flite.Nil) (Taut.Var x_1_0 -> Flite.Cons x_1_0 Flite.Nil) (Taut.Not p_1_0 -> Taut.vars p_1_0) (Taut.And p_1_0 q_1_1 -> Taut.append (Taut.vars p_1_0) (Taut.vars q_1_1)) (Taut.Implies p_1_0 q_1_1 -> Taut.append (Taut.vars p_1_0) (Taut.vars q_1_1)) 
Taut.rmdups_26 !_x_0 = select _x_0 (Flite.Nil -> Flite.Nil) (Flite.Cons x_1_0 xs_1_1 -> Flite.Cons x_1_0 (Taut.rmdups_26 (Taut.filter (Taut.neq_27 x_1_0) xs_1_1))) 
Taut.neq_27 !x_0 !y_1 = <{Taut./=_28}> x_0 y_1
<{Taut./=_28}> !a_0 !b_1 = <{Taut.<>_29}> a_0 b_1
<{Taut.<>_29}> !x_0 !y_1 = not (eq x_0 y_1)
Taut.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 (Taut.filter p_0 xs_1_1)) (Taut.filter p_0 xs_1_1)) 
Taut.eval s_0 !_x_1 = select _x_1 (Taut.Const b_1_0 -> b_1_0) (Taut.Var x_1_0 -> Taut.find_25 x_1_0 s_0) (Taut.Not p_1_0 -> if (Taut.eval s_0 p_1_0) False True) (Taut.And p_1_0 q_1_1 -> if (Taut.eval s_0 p_1_0) (Taut.eval s_0 q_1_1) False) (Taut.Implies p_1_0 q_1_1 -> if (Taut.eval s_0 p_1_0) (Taut.eval s_0 q_1_1) True) 
Taut.find_25 !key_0 !_x_1 = select _x_1 (Flite.Cons _x_1_0 t_1_1 -> select _x_1_0 (Flite.Pair k_2_0 v_2_1 -> if (eq key_0 k_2_0) v_2_1 (Taut.find_25 key_0 t_1_1)) ) 
Taut.flip !f_0 y_1 x_2 = f_0 x_2 y_1
Taut.and !_x_0 = select _x_0 (Flite.Nil -> True) (Flite.Cons b_1_0 bs_1_1 -> if b_1_0 (Taut.and bs_1_1) False)