A machine generated proof for the Math Prof puzzle using a so-called sequent calculus, see https://en.wikipedia.org/wiki/Sequent_calculus.

The gaps in the numbering a due to the fact that the system explored other possible branches of reasoning that turned out to be dead-ends.
Sequent #179 is an axiom since 'b' occurs on both sides.

Make sure to look at this in a UTF-8 enabled viewer, otherwise the logical symbols look bizarre. 


{1, {a ∧ b ∧ c → d, ¬ a ∧ e → f, g ∧ h → ¬ d, i ∧ e → c, ¬ b ∧ g → j, ¬ d ∧ b ∧ h → i, e ∧ ¬ k → l, ¬ j ∧ e → m, m ∧ l ∧ ¬ f → h, j ∧ g → f, e ∧ f → ¬ g, m ∧ k ∧ a → h} ⊃ {¬ (e ∧ g)}, "-", "goal"}
{2, {e ∧ g, e ∧ f → ¬ g, e ∧ ¬ k → l, g ∧ h → ¬ d, i ∧ e → c, j ∧ g → f, a ∧ b ∧ c → d, m ∧ k ∧ a → h, m ∧ l ∧ ¬ f → h, ¬ d ∧ b ∧ h → i, ¬ a ∧ e → f, ¬ b ∧ g → j, ¬ j ∧ e → m} ⊃ {}, 1, "notR"}
{3, {e, g, e ∧ f → ¬ g, e ∧ ¬ k → l, g ∧ h → ¬ d, i ∧ e → c, j ∧ g → f, a ∧ b ∧ c → d, m ∧ k ∧ a → h, m ∧ l ∧ ¬ f → h, ¬ d ∧ b ∧ h → i, ¬ a ∧ e → f, ¬ b ∧ g → j, ¬ j ∧ e → m} ⊃ {}, 2, "andL"}
{4, {e, g, e ∧ ¬ k → l, g ∧ h → ¬ d, i ∧ e → c, j ∧ g → f, a ∧ b ∧ c → d, m ∧ k ∧ a → h, m ∧ l ∧ ¬ f → h, ¬ d ∧ b ∧ h → i, ¬ a ∧ e → f, ¬ b ∧ g → j, ¬ j ∧ e → m} ⊃ {e ∧ f}, 3, "impL1"}
{7, {e, g, e ∧ ¬ k → l, g ∧ h → ¬ d, i ∧ e → c, j ∧ g → f, a ∧ b ∧ c → d, m ∧ k ∧ a → h, m ∧ l ∧ ¬ f → h, ¬ d ∧ b ∧ h → i, ¬ a ∧ e → f, ¬ b ∧ g → j, ¬ j ∧ e → m} ⊃ {f}, 4, "andR2"}
{8, {e, g, g ∧ h → ¬ d, i ∧ e → c, j ∧ g → f, a ∧ b ∧ c → d, m ∧ k ∧ a → h, m ∧ l ∧ ¬ f → h, ¬ d ∧ b ∧ h → i, ¬ a ∧ e → f, ¬ b ∧ g → j, ¬ j ∧ e → m} ⊃ {f, e ∧ ¬ k}, 7, "impL1"}
{11, {e, g, g ∧ h → ¬ d, i ∧ e → c, j ∧ g → f, a ∧ b ∧ c → d, m ∧ k ∧ a → h, m ∧ l ∧ ¬ f → h, ¬ d ∧ b ∧ h → i, ¬ a ∧ e → f, ¬ b ∧ g → j, ¬ j ∧ e → m} ⊃ {f, ¬ k}, 8, "andR2"}
{12, {e, g, k, g ∧ h → ¬ d, i ∧ e → c, j ∧ g → f, a ∧ b ∧ c → d, m ∧ k ∧ a → h, m ∧ l ∧ ¬ f → h, ¬ d ∧ b ∧ h → i, ¬ a ∧ e → f, ¬ b ∧ g → j, ¬ j ∧ e → m} ⊃ {f}, 11, "notR"}
{13, {e, g, k, i ∧ e → c, j ∧ g → f, a ∧ b ∧ c → d, m ∧ k ∧ a → h, m ∧ l ∧ ¬ f → h, ¬ d ∧ b ∧ h → i, ¬ a ∧ e → f, ¬ b ∧ g → j, ¬ j ∧ e → m} ⊃ {f, g ∧ h}, 12, "impL1"}
{16, {e, g, k, i ∧ e → c, j ∧ g → f, a ∧ b ∧ c → d, m ∧ k ∧ a → h, m ∧ l ∧ ¬ f → h, ¬ d ∧ b ∧ h → i, ¬ a ∧ e → f, ¬ b ∧ g → j, ¬ j ∧ e → m} ⊃ {f, h}, 13, "andR2"}
{17, {e, g, k, j ∧ g → f, a ∧ b ∧ c → d, m ∧ k ∧ a → h, m ∧ l ∧ ¬ f → h, ¬ d ∧ b ∧ h → i, ¬ a ∧ e → f, ¬ b ∧ g → j, ¬ j ∧ e → m} ⊃ {f, h, i ∧ e}, 16, "impL1"}
{19, {e, g, k, j ∧ g → f, a ∧ b ∧ c → d, m ∧ k ∧ a → h, m ∧ l ∧ ¬ f → h, ¬ d ∧ b ∧ h → i, ¬ a ∧ e → f, ¬ b ∧ g → j, ¬ j ∧ e → m} ⊃ {f, h, i}, 17, "andR1"}
{21, {e, g, k, a ∧ b ∧ c → d, m ∧ k ∧ a → h, m ∧ l ∧ ¬ f → h, ¬ d ∧ b ∧ h → i, ¬ a ∧ e → f, ¬ b ∧ g → j, ¬ j ∧ e → m} ⊃ {f, h, i, j ∧ g}, 19, "impL1"}
{23, {e, g, k, a ∧ b ∧ c → d, m ∧ k ∧ a → h, m ∧ l ∧ ¬ f → h, ¬ d ∧ b ∧ h → i, ¬ a ∧ e → f, ¬ b ∧ g → j, ¬ j ∧ e → m} ⊃ {f, h, i, j}, 21, "andR1"}
{25, {e, g, k, m ∧ k ∧ a → h, m ∧ l ∧ ¬ f → h, ¬ d ∧ b ∧ h → i, ¬ a ∧ e → f, ¬ b ∧ g → j, ¬ j ∧ e → m} ⊃ {f, h, i, j, a ∧ b ∧ c}, 23, "impL1"}
{27, {e, g, k, m ∧ k ∧ a → h, m ∧ l ∧ ¬ f → h, ¬ d ∧ b ∧ h → i, ¬ a ∧ e → f, ¬ b ∧ g → j, ¬ j ∧ e → m} ⊃ {f, h, i, j, a ∧ b}, 25, "andR1"}
{30, {e, g, k, m ∧ k ∧ a → h, m ∧ l ∧ ¬ f → h, ¬ d ∧ b ∧ h → i, ¬ a ∧ e → f, ¬ b ∧ g → j, ¬ j ∧ e → m} ⊃ {b, f, h, i, j}, 27, "andR2"}
{116, {e, g, k, m ∧ l ∧ ¬ f → h, ¬ d ∧ b ∧ h → i, ¬ a ∧ e → f, ¬ b ∧ g → j, ¬ j ∧ e → m} ⊃ {b, f, h, i, j, m ∧ k ∧ a}, 30, "impL1"}
{118, {e, g, k, m ∧ l ∧ ¬ f → h, ¬ d ∧ b ∧ h → i, ¬ a ∧ e → f, ¬ b ∧ g → j, ¬ j ∧ e → m} ⊃ {b, f, h, i, j, m ∧ k}, 116, "andR1"}
{120, {e, g, k, m ∧ l ∧ ¬ f → h, ¬ d ∧ b ∧ h → i, ¬ a ∧ e → f, ¬ b ∧ g → j, ¬ j ∧ e → m} ⊃ {b, f, h, i, j, m}, 118, "andR1"}
{122, {e, g, k, ¬ d ∧ b ∧ h → i, ¬ a ∧ e → f, ¬ b ∧ g → j, ¬ j ∧ e → m} ⊃ {b, f, h, i, j, m, m ∧ l ∧ ¬ f}, 120, "impL1"}
{124, {e, g, k, ¬ d ∧ b ∧ h → i, ¬ a ∧ e → f, ¬ b ∧ g → j, ¬ j ∧ e → m} ⊃ {b, f, h, i, j, m, m ∧ l}, 122, "andR1"}
{127, {e, g, k, ¬ d ∧ b ∧ h → i, ¬ a ∧ e → f, ¬ b ∧ g → j, ¬ j ∧ e → m} ⊃ {b, f, h, i, j, l, m}, 124, "andR2"}
{154, {e, g, k, ¬ a ∧ e → f, ¬ b ∧ g → j, ¬ j ∧ e → m} ⊃ {b, f, h, i, j, l, m, ¬ d ∧ b ∧ h}, 127, "impL1"}
{157, {e, g, k, ¬ a ∧ e → f, ¬ b ∧ g → j, ¬ j ∧ e → m} ⊃ {b, f, h, i, j, l, m}, 154, "andR2"}
{170, {e, g, k, ¬ b ∧ g → j, ¬ j ∧ e → m} ⊃ {b, f, h, i, j, l, m, ¬ a ∧ e}, 157, "impL1"}
{172, {e, g, k, ¬ b ∧ g → j, ¬ j ∧ e → m} ⊃ {b, f, h, i, j, l, m, ¬ a}, 170, "andR1"}
{174, {a, e, g, k, ¬ b ∧ g → j, ¬ j ∧ e → m} ⊃ {b, f, h, i, j, l, m}, 172, "notR"}
{175, {a, e, g, k, ¬ j ∧ e → m} ⊃ {b, f, h, i, j, l, m, ¬ b ∧ g}, 174, "impL1"}
{177, {a, e, g, k, ¬ j ∧ e → m} ⊃ {b, f, h, i, j, l, m, ¬ b}, 175, "andR1"}
{179, {a, b, e, g, k, ¬ j ∧ e → m} ⊃ {b, f, h, i, j, l, m}, 177, "notR"}