subsection‹Tests with the (minimal) shallow embedding: axiom schemata› theory PMLinHOL_shallow_minimal_further_tests_1 imports PMLinHOL_shallow_minimal ―‹C.B., 2025› begin ―‹What is the weakest modal logic in which the following test formulas F1-F10 are provable?› ―‹Test with schematic axioms› abbreviation(input) "AxT ≡ ∀φ. ⊨⇧m (□⇧mφ) ⊃⇧m φ" abbreviation(input) "AxB ≡ ∀φ. ⊨⇧m φ ⊃⇧m □⇧m(◇⇧mφ)" abbreviation(input) "Ax4 ≡ ∀φ. ⊨⇧m (□⇧mφ) ⊃⇧m □⇧m(□⇧mφ)" consts φ::σ ψ::σ abbreviation(input) "F1 ≡ (◇⇧m(◇⇧mφ)) ⊃⇧m ◇⇧mφ" ―‹holds in K4› abbreviation(input) "F2 ≡ (◇⇧m(□⇧mφ)) ⊃⇧m □⇧m(◇⇧mφ)" ―‹holds in KB› abbreviation(input) "F3 ≡ (◇⇧m(□⇧mφ)) ⊃⇧m □⇧mφ" ―‹holds in KB4› abbreviation(input) "F4 ≡ (□⇧m(◇⇧m(□⇧m(◇⇧mφ)))) ⊃⇧m □⇧m(◇⇧mφ)" ―‹holds in KB/K4› abbreviation(input) "F5 ≡ (◇⇧m(φ ∧⇧m (◇⇧mψ))) ⊃⇧m ((◇⇧mφ) ∧⇧m (◇⇧mψ))" ―‹holds in K4› abbreviation(input) "F6 ≡ ((□⇧m(φ ⊃⇧m ψ)) ∧⇧m (◇⇧m(□⇧m(¬⇧mψ)))) ⊃⇧m ¬⇧m(◇⇧mψ)" ―‹holds in KB4› abbreviation(input) "F7 ≡ (◇⇧mφ) ⊃⇧m (□⇧m(φ ∨⇧m ◇⇧mφ))" ―‹holds in KB4› abbreviation(input) "F8 ≡ (◇⇧m(□⇧mφ)) ⊃⇧m (φ ∨⇧m ◇⇧mφ)" ―‹holds in KT/KB› abbreviation(input) "F9 ≡ ((□⇧m(◇⇧mφ)) ∧⇧m (□⇧m(◇⇧m(¬⇧m φ)))) ⊃⇧m ◇⇧m(◇⇧mφ)" ―‹holds in KT› abbreviation(input) "F10 ≡ ((□⇧m(φ ⊃⇧m □⇧mψ)) ∧⇧m (□⇧m(◇⇧m(¬⇧mψ)))) ⊃⇧m ¬⇧m(□⇧mψ)" ―‹holds in KT› declare imp_cong[cong del] nitpick_params experiment begin lemma S5: "AxT ∧ AxB ∧ Ax4 ⟶ ⊨⇧m F1" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› apply simp ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› by metis lemma S4: "AxT ∧ Ax4 ⟶ ⊨⇧m F1" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› apply simp ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› by metis lemma KB4: "AxB ∧ Ax4 ⟶ ⊨⇧m F1" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› apply simp ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› by metis lemma KTB: "AxT ∧ AxB ⟶ ⊨⇧m F1" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops lemma KT: "AxT ⟶ ⊨⇧m F1" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops lemma KB: "AxB ⟶ ⊨⇧m F1" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops lemma K4: "Ax4 ⟶ ⊨⇧m F1" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› apply simp ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› by metis lemma K: "⊨⇧m F1" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops end experiment begin lemma S5: "AxT ∧ AxB ∧ Ax4 ⟶ ⊨⇧m F2" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› apply simp ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› by (metis NegM_def) lemma S4: "AxT ∧ Ax4 ⟶ ⊨⇧m F2" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops lemma KB4: "AxB ∧ Ax4 ⟶ ⊨⇧m F2" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› apply simp ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› by (metis NegM_def) lemma KTB: "AxT ∧ AxB ⟶ ⊨⇧m F2" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› apply simp ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› by (metis NegM_def) lemma KT: "AxT ⟶ ⊨⇧m F2" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops lemma KB: "AxB ⟶ ⊨⇧m F2" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› apply simp ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› by (metis NegM_def) lemma K4: "Ax4 ⟶ ⊨⇧m F2" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops lemma K: "⊨⇧m F2" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops end experiment begin lemma S5: "AxT ∧ AxB ∧ Ax4 ⟶ ⊨⇧m F3" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› apply simp ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› by (metis NegM_def) lemma S4: "AxT ∧ Ax4 ⟶ ⊨⇧m F3" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops lemma KB4: "AxB ∧ Ax4 ⟶ ⊨⇧m F3" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› apply simp ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› by (metis NegM_def) lemma KTB: "AxT ∧ AxB ⟶ ⊨⇧m F3" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops lemma KT: "AxT ⟶ ⊨⇧m F3" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops lemma KB: "AxB ⟶ ⊨⇧m F3" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops lemma K4: "Ax4 ⟶ ⊨⇧m F3" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops lemma K: "⊨⇧m F3" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops end experiment begin lemma S5: "AxT ∧ AxB ∧ Ax4 ⟶ ⊨⇧m F4" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› apply simp ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› by (metis NegM_def) lemma S4: "AxT ∧ Ax4 ⟶ ⊨⇧m F4" ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof› by smt lemma KB4: "AxB ∧ Ax4 ⟶ ⊨⇧m F4" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› apply simp ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› by (metis NegM_def) lemma KTB: "AxT ∧ AxB ⟶ ⊨⇧m F4" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› apply simp ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› by (metis NegM_def) lemma KT: "AxT ⟶ ⊨⇧m F4" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops lemma KB: "AxB ⟶ ⊨⇧m F4" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› apply simp ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› by (metis NegM_def) lemma K4: "Ax4 ⟶ ⊨⇧m F4" ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof› by smt lemma K: "⊨⇧m F4" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops end experiment begin lemma S5: "AxT ∧ AxB ∧ Ax4 ⟶ ⊨⇧m F5" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› apply simp ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› by metis lemma S4: "AxT ∧ Ax4 ⟶ ⊨⇧m F5" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› apply simp ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› by metis lemma KB4: "AxB ∧ Ax4 ⟶ ⊨⇧m F5" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› apply simp ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› by metis lemma KTB: "AxT ∧ AxB ⟶ ⊨⇧m F5" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops lemma KT: "AxT ⟶ ⊨⇧m F5" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops lemma KB: "AxB ⟶ ⊨⇧m F5" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops lemma K4: "Ax4 ⟶ ⊨⇧m F5" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› apply simp ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› by metis lemma K: "⊨⇧m F5" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops end experiment begin lemma S5: "AxT ∧ AxB ∧ Ax4 ⟶ ⊨⇧m F6" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› apply simp ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› by (metis NegM_def) lemma S4: "AxT ∧ Ax4 ⟶ ⊨⇧m F6" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops lemma KB4: "AxB ∧ Ax4 ⟶ ⊨⇧m F6" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› apply simp ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› by (metis NegM_def) lemma KTB: "AxT ∧ AxB ⟶ ⊨⇧m F6" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops lemma KT: "AxT ⟶ ⊨⇧m F6" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops lemma KB: "AxB ⟶ ⊨⇧m F6" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops lemma K4: "Ax4 ⟶ ⊨⇧m F6" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops lemma K: "⊨⇧m F6" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops end experiment begin lemma S5: "AxT ∧ AxB ∧ Ax4 ⟶ ⊨⇧m F7" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› apply simp ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› by (metis NegM_def) lemma S4: "AxT ∧ Ax4 ⟶ ⊨⇧m F7" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops lemma KB4: "AxB ∧ Ax4 ⟶ ⊨⇧m F7" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› apply simp ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› by (metis NegM_def) lemma KTB: "AxT ∧ AxB ⟶ ⊨⇧m F7" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops lemma KT: "AxT ⟶ ⊨⇧m F7" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops lemma KB: "AxB ⟶ ⊨⇧m F7" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops lemma K4: "Ax4 ⟶ ⊨⇧m F7" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops lemma K: "⊨⇧m F7" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops end experiment begin lemma S5: "AxT ∧ AxB ∧ Ax4 ⟶ ⊨⇧m F8" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› apply simp ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› by metis lemma S4: "AxT ∧ Ax4 ⟶ ⊨⇧m F8" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› apply simp ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› by metis lemma KB4: "AxB ∧ Ax4 ⟶ ⊨⇧m F8" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› apply simp ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› by (metis NegM_def) lemma KTB: "AxT ∧ AxB ⟶ ⊨⇧m F8" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› apply simp ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› by metis lemma KT: "AxT ⟶ ⊨⇧m F8" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› apply simp ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› by metis lemma KB: "AxB ⟶ ⊨⇧m F8" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› apply simp ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› by (metis NegM_def) lemma K4: "Ax4 ⟶ ⊨⇧m F8" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops lemma K: "⊨⇧m F8" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops end experiment begin lemma S5: "AxT ∧ AxB ∧ Ax4 ⟶ ⊨⇧m F9" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› apply simp ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› by metis lemma S4: "AxT ∧ Ax4 ⟶ ⊨⇧m F9" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› apply simp ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› by metis lemma KB4: "AxB ∧ Ax4 ⟶ ⊨⇧m F9" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops lemma KTB: "AxT ∧ AxB ⟶ ⊨⇧m F9" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› apply simp ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› by metis lemma KT: "AxT ⟶ ⊨⇧m F9" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› apply simp ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› by metis lemma KB: "AxB ⟶ ⊨⇧m F9" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops lemma K4: "Ax4 ⟶ ⊨⇧m F9" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops lemma K: "⊨⇧m F9" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops end experiment begin lemma S5: "AxT ∧ AxB ∧ Ax4 ⟶ ⊨⇧m F10" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹no prf› apply simp ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› by metis lemma S4: "AxT ∧ Ax4 ⟶ ⊨⇧m F10" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹no prf› apply simp ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› by metis lemma KB4: "AxB ∧ Ax4 ⟶ ⊨⇧m F10" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops lemma KTB: "AxT ∧ AxB ⟶ ⊨⇧m F10" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹no prf› apply simp ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› by metis lemma KT: "AxT ⟶ ⊨⇧m F10" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› apply simp ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› by metis lemma KB: "AxB ⟶ ⊨⇧m F10" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops lemma K4: "Ax4 ⟶ ⊨⇧m F10" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops lemma K: "⊨⇧m F10" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops end ―‹Summary of experiments: Nitpick: ctex=84 (with simp 42, without simp 42), none=72 (with simp 36, without simp 36), unknwn=4 (with simp 2, without simp 2) Sledgehammer: proof=73 (with simp 38, without simp 35), no prf=87(with simp 42, without simp 45)› ―‹No conflicts› end