81   auto Y = Ctx.atom();  in TEST()  local
82   auto NotY = Ctx.neg(Y);  in TEST()
88                            Pair(Y, Solver::Result::Assignment::AssignedFalse)));  in TEST()
104   auto Y = Ctx.atom();  in TEST()  local
105   auto XOrY = Ctx.disj(X, Y);  in TEST()
115   auto Y = Ctx.atom();  in TEST()  local
116   auto XAndY = Ctx.conj(X, Y);  in TEST()
164   auto Y = Ctx.atom();  in TEST()  local
166   auto NotXOrY = Ctx.disj(NotX, Y);  in TEST()
167   auto NotY = Ctx.neg(Y);  in TEST()
174                            Pair(Y, _)));  in TEST()
180   auto Y = Ctx.atom();  in TEST()  local
181   auto XOrY = Ctx.disj(X, Y);  in TEST()
183   auto NotXOrY = Ctx.disj(NotX, Y);  in TEST()
184   auto NotY = Ctx.neg(Y);  in TEST()
191                            Pair(Y, Solver::Result::Assignment::AssignedTrue)));  in TEST()
197   auto Y = Ctx.atom();  in TEST()  local
198   auto XOrY = Ctx.disj(X, Y);  in TEST()
200   auto NotXOrY = Ctx.disj(NotX, Y);  in TEST()
201   auto NotY = Ctx.neg(Y);  in TEST()
212   auto Y = Ctx.atom();  in TEST()  local
214   auto NotY = Ctx.neg(Y);  in TEST()
215   auto XIffY = Ctx.iff(X, Y);  in TEST()
216   auto XIffYDNF = Ctx.disj(Ctx.conj(X, Y), Ctx.conj(NotX, NotY));  in TEST()
235   auto Y = Ctx.atom();  in TEST()  local
236   auto XEqY = Ctx.iff(X, Y);  in TEST()
243                 Pair(Y, Solver::Result::Assignment::AssignedTrue)),  in TEST()
246                 Pair(Y, Solver::Result::Assignment::AssignedFalse))));  in TEST()
252   auto Y = Ctx.atom();  in TEST()  local
253   auto XEqY = Ctx.iff(X, Y);  in TEST()
257       solve({XEqY, X, Y}),  in TEST()
259                            Pair(Y, Solver::Result::Assignment::AssignedTrue)));  in TEST()
265   auto Y = Ctx.atom();  in TEST()  local
266   auto XEqY = Ctx.iff(X, Y);  in TEST()
267   auto NotY = Ctx.neg(Y);  in TEST()
276   auto Y = Ctx.atom();  in TEST()  local
278   auto XEqY = Ctx.iff(X, Y);  in TEST()
279   auto YEqZ = Ctx.iff(Y, Z);  in TEST()
289   auto Y = Ctx.atom();  in TEST()  local
294   auto A = Ctx.iff(Ctx.neg(Ctx.disj(X, Y)), Ctx.conj(Ctx.neg(X), Ctx.neg(Y)));  in TEST()
306   auto Y = Ctx.atom();  in TEST()  local
307   auto XEqY = Ctx.iff(X, Y);  in TEST()
308   auto NotY = Ctx.neg(Y);  in TEST()
317   auto Y = Ctx.atom();  in TEST()  local
318   auto XImpliesY = Ctx.impl(X, Y);  in TEST()
319   auto XImpliesYDNF = Ctx.disj(Ctx.neg(X), Y);  in TEST()
329   auto Y = Ctx.atom();  in TEST()  local
330   auto *XImplY = Ctx.impl(X, Y);  in TEST()
331   auto *XAndNotY = Ctx.conj(X, Ctx.neg(Y));  in TEST()