(*  Title:      HOL/TPTP/TPTP_Proof_Reconstruction_Test_Units.thy
    Author:     Nik Sultana, Cambridge University Computer Laboratory

Unit tests for proof reconstruction module.
*)

theory TPTP_Proof_Reconstruction_Test_Units
imports TPTP_Test TPTP_Proof_Reconstruction
begin

declare [[ML_exception_trace, ML_print_depth = 200]]

declare [[tptp_trace_reconstruction = true]]

lemma "! (X1 :: bool) (X2 :: bool) (X3 :: bool) (X4 :: bool) (X5 :: bool). P ==> ! (X1 :: bool) (X3 :: bool) (X5 :: bool). P"
apply (tactic ‹canonicalise_qtfr_order @{context} 1›)
oops

lemma "! (X1 :: bool) (X2 :: bool) (X3 :: bool) (X4 :: bool) (X5 :: bool). P ==> ! (X1 :: bool) (X3 :: bool) (X5 :: bool). P"
apply (tactic ‹canonicalise_qtfr_order @{context} 1›)
apply (rule allI)+
apply (tactic ‹nominal_inst_parametermatch_tac @{context} @{thm allE} 1›)+
oops

(*Could test bind_tac further with NUM667^1 inode43*)

(*
  (* SEU581^2.p_nux *)
     (* (Annotated_step ("inode1", "bind"), *)
lemma "∀(SV5::TPTP_Interpret.ind → bool)
            SV6::TPTP_Interpret.ind.
            (bnd_in (bnd_dsetconstr bnd_sK1_A bnd_sK2_SY15)
              (bnd_powerset bnd_sK1_A) =
             bnd_in (bnd_dsetconstr SV6 SV5)
              (bnd_powerset SV6)) =
            False ==>
         (bnd_in (bnd_dsetconstr bnd_sK1_A bnd_sK2_SY15)
           (bnd_powerset bnd_sK1_A) =
          bnd_in (bnd_dsetconstr bnd_sK1_A bnd_sK2_SY15)
           (bnd_powerset bnd_sK1_A)) =
         False"
ML_prf {*
open TPTP_Syntax;
open TPTP_Proof;


val binds =
[Bind ("SV6", Atom (THF_Atom_term (Term_Func (Uninterpreted "sK1_A", [])))), Bind ("SV5", Quant (Lambda, [("SX0", SOME (Fmla_type (Atom (THF_Atom_term (Term_Func (TypeSymbol Type_Ind, []))))))], Fmla (Interpreted_ExtraLogic Apply, [Atom (THF_Atom_term (Term_Func (Uninterpreted "sK2_SY15", []))), Atom (THF_Atom_term (Term_Var "SX0"))])))]
(* |> TPTP_Reconstruct.permute *)

(*
val binds =
[Bind ("SV5", Quant (Lambda, [("SX0", SOME (Fmla_type (Atom (THF_Atom_term (Term_Func (TypeSymbol Type_Ind, []))))))], Fmla (Interpreted_ExtraLogic Apply, [Atom (THF_Atom_term (Term_Func (Uninterpreted "sK2_SY15", []))), Atom (THF_Atom_term (Term_Var "SX0"))]))),
Bind ("SV6", Atom (THF_Atom_term (Term_Func (Uninterpreted "sK1_A", []))))
]
*)

val tec =
(*
  map (bind_tac @{context} (hd prob_names)) binds
  |> FIRST
*)
  bind_tac @{context} (hd prob_names) binds
*}
apply (tactic {*tec*})
done

     (* (Annotated_step ("inode2", "bind"), *)
lemma "∀(SV7::TPTP_Interpret.ind) SV8::TPTP_Interpret.ind.
            (bnd_subset SV8 SV7 =
             bnd_subset (bnd_dsetconstr bnd_sK1_A bnd_sK2_SY15)
              bnd_sK1_A) =
            False ∨
            bnd_in SV8 (bnd_powerset SV7) = False ==>
         (bnd_subset (bnd_dsetconstr bnd_sK1_A bnd_sK2_SY15)
           bnd_sK1_A =
          bnd_subset (bnd_dsetconstr bnd_sK1_A bnd_sK2_SY15)
           bnd_sK1_A) =
         False ∨
         bnd_in (bnd_dsetconstr bnd_sK1_A bnd_sK2_SY15)
          (bnd_powerset bnd_sK1_A) =
         False"
ML_prf {*
open TPTP_Syntax;
open TPTP_Proof;


val binds =
[Bind ("SV8", Fmla (Interpreted_ExtraLogic Apply, [Fmla (Interpreted_ExtraLogic Apply, [Atom (THF_Atom_term (Term_Func (Uninterpreted "dsetconstr", []))), Atom (THF_Atom_term (Term_Func (Uninterpreted "sK1_A", [])))]), Quant (Lambda, [("SX0", SOME (Fmla_type (Atom (THF_Atom_term (Term_Func (TypeSymbol Type_Ind, []))))))], Fmla (Interpreted_ExtraLogic Apply, [Atom (THF_Atom_term (Term_Func (Uninterpreted "sK2_SY15", []))), Atom (THF_Atom_term (Term_Var "SX0"))]))])), Bind ("SV7", Atom (THF_Atom_term (Term_Func (Uninterpreted "sK1_A", []))))]
(* |> TPTP_Reconstruct.permute *)

val tec =
(*
  map (bind_tac @{context} (hd prob_names)) binds
  |> FIRST
*)
  bind_tac @{context} (hd prob_names) binds
*}
apply (tactic {*tec*})
done
*)

(*
from SEU897^5
lemma "
\<forall>SV9 SV10 SV11 SV12 SV13 SV14.
   (((((bnd_sK5_SY14 SV14 SV13 SV12 = SV11) = False \<or>
       (bnd_sK4_SX0 = SV10 (bnd_sK5_SY14 SV9 SV10 SV11)) =
       False) \<or>
      bnd_cR SV14 = False) \<or>
     (SV12 = SV13 SV14) = False) \<or>
    bnd_cR SV9 = False) \<or>
   (SV11 = SV10 SV9) = False \<Longrightarrow>
\<forall>SV14 SV13 SV12 SV10 SV9.
   (((((bnd_sK5_SY14 SV14 SV13 SV12 =
        bnd_sK5_SY14 SV14 SV13 SV12) =
       False \<or>
       (bnd_sK4_SX0 =
        SV10
         (bnd_sK5_SY14 SV9 SV10
           (bnd_sK5_SY14 SV14 SV13 SV12))) =
       False) \<or>
      bnd_cR SV14 = False) \<or>
     (SV12 = SV13 SV14) = False) \<or>
    bnd_cR SV9 = False) \<or>
   (bnd_sK5_SY14 SV14 SV13 SV12 = SV10 SV9) = False"
ML_prf {*
open TPTP_Syntax;
open TPTP_Proof;

val binds =
[Bind ("SV11", Fmla (Interpreted_ExtraLogic Apply, [Fmla (Interpreted_ExtraLogic Apply, [Fmla (Interpreted_ExtraLogic Apply, [Atom (THF_Atom_term (Term_Func (Uninterpreted "sK5_SY14", []))), Atom (THF_Atom_term (Term_Var "SV14"))]), Atom (THF_Atom_term (Term_Var "SV13"))]), Atom (THF_Atom_term (Term_Var "SV12"))]))]

val tec = bind_tac @{context} (hd prob_names) binds
*}
apply (tactic {*tec*})
done
*)


subsection "Interpreting the inferences"

(*from SET598^5
lemma "(bnd_sK1_X = (\<lambda>SY17. bnd_sK2_Y SY17 \<and> bnd_sK3_Z SY17) \<longrightarrow>
   ((\<forall>SY25. bnd_sK1_X SY25 \<longrightarrow> bnd_sK2_Y SY25) \<and>
    (\<forall>SY26. bnd_sK1_X SY26 \<longrightarrow> bnd_sK3_Z SY26)) \<and>
   (\<forall>SY27.
       (\<forall>SY21. SY27 SY21 \<longrightarrow> bnd_sK2_Y SY21) \<and>
       (\<forall>SY15. SY27 SY15 \<longrightarrow> bnd_sK3_Z SY15) \<longrightarrow>
       (\<forall>SY30. SY27 SY30 \<longrightarrow> bnd_sK1_X SY30))) =
  False \<Longrightarrow>
  (\<not> (bnd_sK1_X = (\<lambda>SY17. bnd_sK2_Y SY17 \<and> bnd_sK3_Z SY17) \<longrightarrow>
      ((\<forall>SY25. bnd_sK1_X SY25 \<longrightarrow> bnd_sK2_Y SY25) \<and>
       (\<forall>SY26. bnd_sK1_X SY26 \<longrightarrow> bnd_sK3_Z SY26)) \<and>
      (\<forall>SY27.
          (\<forall>SY21. SY27 SY21 \<longrightarrow> bnd_sK2_Y SY21) \<and>
          (\<forall>SY15. SY27 SY15 \<longrightarrow> bnd_sK3_Z SY15) \<longrightarrow>
          (\<forall>SY30. SY27 SY30 \<longrightarrow> bnd_sK1_X SY30)))) =
  True"
apply (tactic {*polarity_switch_tac @{context}*})
done
lemma "
  (((\<forall>SY25. bnd_sK1_X SY25 \<longrightarrow> bnd_sK2_Y SY25) \<and>
    (\<forall>SY26. bnd_sK1_X SY26 \<longrightarrow> bnd_sK3_Z SY26)) \<and>
   (\<forall>SY27.
       (\<forall>SY21. SY27 SY21 \<longrightarrow> bnd_sK2_Y SY21) \<and>
       (\<forall>SY15. SY27 SY15 \<longrightarrow> bnd_sK3_Z SY15) \<longrightarrow>
       (\<forall>SY30. SY27 SY30 \<longrightarrow> bnd_sK1_X SY30)) \<longrightarrow>
   bnd_sK1_X = (\<lambda>SY17. bnd_sK2_Y SY17 \<and> bnd_sK3_Z SY17)) =
  False \<Longrightarrow>
  (\<not> (((\<forall>SY25. bnd_sK1_X SY25 \<longrightarrow> bnd_sK2_Y SY25) \<and>
       (\<forall>SY26. bnd_sK1_X SY26 \<longrightarrow> bnd_sK3_Z SY26)) \<and>
      (\<forall>SY27.
          (\<forall>SY21. SY27 SY21 \<longrightarrow> bnd_sK2_Y SY21) \<and>
          (\<forall>SY15. SY27 SY15 \<longrightarrow> bnd_sK3_Z SY15) \<longrightarrow>
          (\<forall>SY30. SY27 SY30 \<longrightarrow> bnd_sK1_X SY30)) \<longrightarrow>
      bnd_sK1_X = (\<lambda>SY17. bnd_sK2_Y SY17 \<and> bnd_sK3_Z SY17))) =
  True"
apply (tactic {*polarity_switch_tac @{context}*})
done
*)

(* beware lack of type annotations
(* lemma "!!x. (A x = B x) = False ==> (B x = A x) = False" *)
(* lemma "!!x. (A x = B x) = True ==> (B x = A x) = True" *)
(* lemma "((A x) = (B x)) = True ==> ((B x) = (A x)) = True" *)
lemma "(A = B) = True ==> (B = A) = True"
*)
lemma "!!x. ((A x :: bool) = B x) = False ==> (B x = A x) = False"
apply (tactic ‹expander_animal @{context} 1›)
oops

lemma "(A & B) ==> ~(~A | ~B)"
by (tactic ‹expander_animal @{context} 1›)

lemma "(A | B) ==> ~(~A & ~B)"
by (tactic ‹expander_animal @{context} 1›)

lemma "(A | B) | C ==> A | (B | C)"
by (tactic ‹expander_animal @{context} 1›)

lemma "(~~A) = B ==> A = B"
by (tactic ‹expander_animal @{context} 1›)

lemma "~ ~ (A = True) ==> A = True"
by (tactic ‹expander_animal @{context} 1›)

(*This might not be a goal which might realistically arise:
lemma "((~~A) = B) & (B = (~~A)) ==> ~(~(A = B) | ~(B = A))" *)
lemma "((~~A) = True) ==> ~(~(A = True) | ~(True = A))"
apply (tactic ‹expander_animal @{context} 1›)+
apply (rule conjI)
apply assumption
apply (rule sym, assumption)
done

lemma "A = B ==> ((~~A) = B) & (B = (~~A)) ==> ~(~(A = B) | ~(B = A))"
by (tactic ‹expander_animal @{context} 1›)+

(*some lemmas assume constants in the signature of PUZ114^5*)
consts
  PUZ114_5_bnd_sK1 :: "TPTP_Interpret.ind"
  PUZ114_5_bnd_sK2 :: "TPTP_Interpret.ind"
  PUZ114_5_bnd_sK3 :: "TPTP_Interpret.ind → TPTP_Interpret.ind → bool"
  PUZ114_5_bnd_sK4 :: "(TPTP_Interpret.ind → TPTP_Interpret.ind → bool) → TPTP_Interpret.ind"
  PUZ114_5_bnd_sK5 :: "(TPTP_Interpret.ind → TPTP_Interpret.ind → bool) → TPTP_Interpret.ind"
  PUZ114_5_bnd_s :: "TPTP_Interpret.ind → TPTP_Interpret.ind"
  PUZ114_5_bnd_c1 :: TPTP_Interpret.ind

(*testing logical expansion*)
lemma "!! SY30. (SY30 PUZ114_5_bnd_c1 PUZ114_5_bnd_c1 ∧
       (∀Xj Xk.
           SY30 Xj Xk ⟶
           SY30 (PUZ114_5_bnd_s (PUZ114_5_bnd_s Xj)) Xk ∧
           SY30 (PUZ114_5_bnd_s Xj) (PUZ114_5_bnd_s Xk)) ⟶
       SY30 PUZ114_5_bnd_sK1 PUZ114_5_bnd_sK2)
==> (
       (~ SY30 PUZ114_5_bnd_c1 PUZ114_5_bnd_c1)
     | (~ (∀Xj Xk.
           SY30 Xj Xk ⟶
           SY30 (PUZ114_5_bnd_s (PUZ114_5_bnd_s Xj)) Xk ∧
           SY30 (PUZ114_5_bnd_s Xj) (PUZ114_5_bnd_s Xk)))
     | SY30 PUZ114_5_bnd_sK1 PUZ114_5_bnd_sK2
)"
by (tactic ‹expander_animal @{context} 1›)+

(*
extcnf_forall_pos:

     (! X. L1) | ... | Ln
 ----------------------------   X' fresh
  ! X'. (L1[X'/X] | ... | Ln)

After elimination rule has been applied we'll have a subgoal which looks like this:
            (! X. L1)
 ----------------------------   X' fresh
  ! X'. (L1[X'/X] | ... | Ln)
and we need to transform it so that, in Isabelle, we go from
 (! X. L1) ==> ! X'. (L1[X'/X] | ... | Ln)
to
 \<And> X'. L1[X'/X] ==> (L1[X'/X] | ... | Ln)
(where X' is fresh, or renamings are done suitably).*)

lemma "A | B ==> A | B | C"
apply (tactic ‹flip_conclusion_tac @{context} 1›)+
apply (tactic ‹break_hypotheses 1›)+
oops

consts
  CSR122_1_bnd_lBill_THFTYPE_i :: TPTP_Interpret.ind
  CSR122_1_bnd_lMary_THFTYPE_i :: TPTP_Interpret.ind
  CSR122_1_bnd_lSue_THFTYPE_i :: TPTP_Interpret.ind
  CSR122_1_bnd_n2009_THFTYPE_i :: TPTP_Interpret.ind
  CSR122_1_bnd_lYearFn_THFTYPE_IiiI :: "TPTP_Interpret.ind → TPTP_Interpret.ind"
  CSR122_1_bnd_holdsDuring_THFTYPE_IiooI ::
    "TPTP_Interpret.ind → bool → bool"
  CSR122_1_bnd_likes_THFTYPE_IiioI ::
    "TPTP_Interpret.ind → TPTP_Interpret.ind → bool"

lemma "∀SV2. (CSR122_1_bnd_holdsDuring_THFTYPE_IiooI
                 (CSR122_1_bnd_lYearFn_THFTYPE_IiiI CSR122_1_bnd_n2009_THFTYPE_i)
                 (¬ (¬ CSR122_1_bnd_likes_THFTYPE_IiioI
                        CSR122_1_bnd_lMary_THFTYPE_i
                        CSR122_1_bnd_lBill_THFTYPE_i ∨
                     ¬ CSR122_1_bnd_likes_THFTYPE_IiioI
                        CSR122_1_bnd_lSue_THFTYPE_i
                        CSR122_1_bnd_lBill_THFTYPE_i)) =
                CSR122_1_bnd_holdsDuring_THFTYPE_IiooI SV2 True) =
               False ==>
         ∀SV2. (CSR122_1_bnd_lYearFn_THFTYPE_IiiI CSR122_1_bnd_n2009_THFTYPE_i =
                SV2) =
               False ∨
               ((¬ (¬ CSR122_1_bnd_likes_THFTYPE_IiioI
                       CSR122_1_bnd_lMary_THFTYPE_i CSR122_1_bnd_lBill_THFTYPE_i ∨
                    ¬ CSR122_1_bnd_likes_THFTYPE_IiioI CSR122_1_bnd_lSue_THFTYPE_i
                       CSR122_1_bnd_lBill_THFTYPE_i)) =
                True) =
               False"
apply (rule allI, erule_tac x = "SV2" in allE)
apply (tactic ‹extuni_dec_tac @{context} 1›)
done

(*SEU882^5*)
(*
lemma
 "\<forall>(SV2::TPTP_Interpret.ind)
        SV1::TPTP_Interpret.ind \<Rightarrow> TPTP_Interpret.ind.
        (SV1 SV2 = bnd_sK1_Xy) =
        False
   \<Longrightarrow>
   \<forall>SV2::TPTP_Interpret.ind.
            (bnd_sK1_Xy = bnd_sK1_Xy) =
            False"
ML_prf {*
open TPTP_Syntax;
open TPTP_Proof;

val binds =
[Bind ("SV1", Quant (Lambda, [("SX0", SOME (Fmla_type (Atom (THF_Atom_term (Term_Func (TypeSymbol Type_Ind, []))))))], Atom (THF_Atom_term (Term_Func (Uninterpreted "sK1_Xy", [])))))]

val tec = bind_tac @{context} (hd prob_names) binds
*}
(*
apply (tactic {*strip_qtfrs
                (* THEN tec *)*})
*)
apply (tactic {*tec*})
done
*)

lemma "A | B ==> C1 | A | C2 | B | C3"
apply (erule disjE)
apply (tactic ‹clause_breaker 1›)
apply (tactic ‹clause_breaker 1›)
done

lemma "A ==> A"
apply (tactic ‹clause_breaker 1›)
done

typedecl NUM667_1_bnd_nat
consts
  NUM667_1_bnd_less :: "NUM667_1_bnd_nat → NUM667_1_bnd_nat → bool"
  NUM667_1_bnd_x :: NUM667_1_bnd_nat
  NUM667_1_bnd_y :: NUM667_1_bnd_nat

(*NUM667^1 node 302 -- dec*)
lemma "∀SV12 SV13 SV14 SV9 SV10 SV11.
       ((((NUM667_1_bnd_less SV12 SV13 = NUM667_1_bnd_less SV11 SV10) = False ∨
          (SV14 = SV13) = False) ∨
         NUM667_1_bnd_less SV12 SV14 = False) ∨
        NUM667_1_bnd_less SV9 SV10 = True) ∨
       (SV9 = SV11) =
       False ==>
       ∀SV9 SV14 SV10 SV13 SV11 SV12.
       (((((SV12 = SV11) = False ∨ (SV13 = SV10) = False) ∨
          (SV14 = SV13) = False) ∨
         NUM667_1_bnd_less SV12 SV14 = False) ∨
        NUM667_1_bnd_less SV9 SV10 = True) ∨
       (SV9 = SV11) =
       False"
apply (tactic ‹strip_qtfrs_tac @{context}›)
apply (tactic ‹break_hypotheses 1›)
apply (tactic ‹ALLGOALS (TRY o clause_breaker)›)
apply (tactic ‹extuni_dec_tac @{context} 1›)
done

ML ‹
  @{context} 2;
 ›

(*NUM667^1, node 202*)
lemma "∀SV9 SV10 SV11.
       ((((SV9 = SV11) = (NUM667_1_bnd_x = NUM667_1_bnd_y)) = False ∨
         NUM667_1_bnd_less SV11 SV10 = False) ∨
        NUM667_1_bnd_less SV9 SV10 = True) ∨
       NUM667_1_bnd_less NUM667_1_bnd_x NUM667_1_bnd_y =
       True ==>
       ∀SV10 SV9 SV11.
       ((((SV11 = NUM667_1_bnd_x) = False ∨ (SV9 = NUM667_1_bnd_y) = False) ∨
         NUM667_1_bnd_less SV11 SV10 = False) ∨
        NUM667_1_bnd_less SV9 SV10 = True) ∨
       NUM667_1_bnd_less NUM667_1_bnd_x NUM667_1_bnd_y =
       True"
apply (tactic ‹strip_qtfrs_tac @{context}›)
apply (tactic ‹break_hypotheses 1›)
apply (tactic ‹ALLGOALS (TRY o clause_breaker)›)
apply (tactic ‹extuni_dec_tac @{context} 1›)
done

(*NUM667^1 node 141*)
(*
lemma "((bnd_x = bnd_x) = False \<or> (bnd_y = bnd_z) = False) \<or>
         bnd_less bnd_x bnd_y = True \<Longrightarrow>
         (bnd_y = bnd_z) = False \<or> bnd_less bnd_x bnd_y = True"
apply (tactic {*strip_qtfrs*})
apply (tactic {*break_hypotheses 1*})
apply (tactic {*ALLGOALS (TRY o clause_breaker)*})
apply (erule extuni_triv)
done
*)

ML ‹
  full_extcnf_combined_tac ctxt =
 extcnf_combined_tac ctxt NONE
 [ConstsDiff,
 StripQuantifiers,
 Flip_Conclusion,
 Loop [
 Close_Branch,
 ConjI,
 King_Cong,
 Break_Hypotheses,
 Existential_Free,
 Existential_Var,
 Universal,
 RemoveRedundantQuantifications],
 CleanUp [RemoveHypothesesFromSkolemDefs, RemoveDuplicates],
 AbsorbSkolemDefs]
 []
 ›

ML ‹
  nonfull_extcnf_combined_tac ctxt feats =
 extcnf_combined_tac ctxt NONE
 [ConstsDiff,
 StripQuantifiers,
 InnerLoopOnce (Break_Hypotheses :: feats),
 AbsorbSkolemDefs]
 []
 ›

consts SEU882_5_bnd_sK1_Xy :: TPTP_Interpret.ind
lemma
  "∀SV2. (SEU882_5_bnd_sK1_Xy = SEU882_5_bnd_sK1_Xy) = False ==>
   (SEU882_5_bnd_sK1_Xy = SEU882_5_bnd_sK1_Xy) = False"
(* apply (erule_tac x = "(@X. False)" in allE) *)
(* apply (tactic {*remove_redundant_quantification 1*}) *)
(* apply assumption *)
by (tactic ‹nonfull_extcnf_combined_tac @{context} [RemoveRedundantQuantifications, Extuni_FlexRigid]›)

(*NUM667^1*)
(*
     (* (Annotated_step ("153", "extuni_triv"), *)
lemma "((bnd_y = bnd_x) = False ∨ (bnd_z = bnd_z) = False) ∨
         (bnd_y = bnd_z) = True ==>
         (bnd_y = bnd_x) = False ∨ (bnd_y = bnd_z) = True"
apply (tactic {*nonfull_extcnf_combined_tac [Extuni_Triv]*})
done
     (* (Annotated_step ("162", "extuni_triv"), *)
lemma "((bnd_y = bnd_x) = False ∨ (bnd_z = bnd_z) = False) ∨
         bnd_less bnd_y bnd_z = True ==>
         (bnd_y = bnd_x) = False ∨ bnd_less bnd_y bnd_z = True"
apply (tactic {*nonfull_extcnf_combined_tac [Extuni_Triv]*})
done
*)

(* SEU602^2 *)
consts
  SEU602_2_bnd_sK7_E :: "(TPTP_Interpret.ind → bool) → TPTP_Interpret.ind"
  SEU602_2_bnd_sK2_SY17 :: TPTP_Interpret.ind
  SEU602_2_bnd_in :: "TPTP_Interpret.ind → TPTP_Interpret.ind → bool"

     (* (Annotated_step ("113", "extuni_func"), *)
lemma "∀SV49::TPTP_Interpret.ind → bool.
            (SV49 =
             (λSY23::TPTP_Interpret.ind.
                 ¬ SEU602_2_bnd_in SY23 SEU602_2_bnd_sK2_SY17)) =
            False ==>
         ∀SV49::TPTP_Interpret.ind → bool.
            (SV49 (SEU602_2_bnd_sK7_E SV49) =
             (¬ SEU602_2_bnd_in (SEU602_2_bnd_sK7_E SV49) SEU602_2_bnd_sK2_SY17)) =
            False"
(*FIXME this (and similar) tests are getting the "Bad background theory of goal state" error since upgrading to Isabelle2013-2.*)
by (tactic ‹nonfull_extcnf_combined_tac @{context} [Extuni_Func, Existential_Var]›)

consts
  SEV405_5_bnd_sK1_SY2 :: "(TPTP_Interpret.ind → bool) → TPTP_Interpret.ind"
  SEV405_5_bnd_cA :: bool

lemma "∀SV1::TPTP_Interpret.ind → bool.
            (∀SY2::TPTP_Interpret.ind.
                ¬ (¬ (¬ SV1 SY2 ∨ SEV405_5_bnd_cA) ∨
                   ¬ (¬ SEV405_5_bnd_cA ∨ SV1 SY2))) =
            False ==>
         ∀SV1::TPTP_Interpret.ind → bool.
            (¬ (¬ (¬ SV1 (SEV405_5_bnd_sK1_SY2 SV1) ∨ SEV405_5_bnd_cA) ∨
                ¬ (¬ SEV405_5_bnd_cA ∨ SV1 (SEV405_5_bnd_sK1_SY2 SV1)))) =
            False"
by (tactic ‹nonfull_extcnf_combined_tac @{context} [Existential_Var]›)
(*
strip quantifiers -- creating a space of permutations; from shallowest to deepest (iterative deepening)
flip the conclusion -- giving us branch
apply some collection of rules, in some order, until the space has been explored completely. advantage of not having extcnf_combined: search space is shallow -- particularly if the collection of rules is small.
*)

consts
  SEU581_2_bnd_sK1 :: "TPTP_Interpret.ind"
  SEU581_2_bnd_sK2 :: "TPTP_Interpret.ind → bool"
  SEU581_2_bnd_subset :: "TPTP_Interpret.ind → TPTP_Interpret.ind → HOL.bool"
  SEU581_2_bnd_dsetconstr ::  "TPTP_Interpret.ind → (TPTP_Interpret.ind → HOL.bool) → TPTP_Interpret.ind"

(*testing parameters*)
lemma "! X :: TPTP_Interpret.ind . (∀A B. SEU581_2_bnd_in B (SEU581_2_bnd_powerset A) ⟶ SEU581_2_bnd_subset B A) = True
\<Longrightarrow> ! X :: TPTP_Interpret.ind . (∀A B. ¬ SEU581_2_bnd_in B (SEU581_2_bnd_powerset A) ∨ SEU581_2_bnd_subset B A) = True"
by (tactic ‹full_extcnf_combined_tac @{context}›)

lemma "(A & B) = True ==> (A | B) = True"
by (tactic ‹full_extcnf_combined_tac @{context}›)

lemma "(¬ bnd_subset (bnd_dsetconstr bnd_sK1 bnd_sK2) bnd_sK1) = True ==> (bnd_subset (bnd_dsetconstr bnd_sK1 bnd_sK2) bnd_sK1) = False"
by (tactic ‹full_extcnf_combined_tac @{context}›)

(*testing goals with parameters*)
lemma "(¬ bnd_subset (bnd_dsetconstr bnd_sK1 bnd_sK2) bnd_sK1) = True ==> ! X. (bnd_subset (bnd_dsetconstr bnd_sK1 bnd_sK2) bnd_sK1) = False"
by (tactic ‹full_extcnf_combined_tac @{context}›)

lemma "(A & B) = True ==> (B & A) = True"
by (tactic ‹full_extcnf_combined_tac @{context}›)

(*appreciating differences between THEN, REPEAT, and APPEND*)
lemma "A & B ==> B & A"
apply (tactic ‹
 TRY (etac @{thm conjE} 1)
 THEN TRY (rtac @{thm conjI} 1)›)
by assumption+

lemma "A & B ==> B & A"
by (tactic ‹
 etac @{thm conjE} 1
 THEN rtac @{thm conjI} 1
 THEN REPEAT (atac 1)›)

lemma "A & B ==> B & A"
apply (tactic ‹
 rtac @{thm conjI} 1
 APPEND etac @{thm conjE} 1›)+
back
by assumption+

consts
  SEU581_2_bnd_sK3 :: "TPTP_Interpret.ind"
  SEU581_2_bnd_sK4 :: "TPTP_Interpret.ind"
  SEU581_2_bnd_sK5 :: "(TPTP_Interpret.ind → bool) → TPTP_Interpret.ind"
  SEU581_2_bnd_powerset :: "TPTP_Interpret.ind → TPTP_Interpret.ind"
  SEU581_2_bnd_in :: "TPTP_Interpret.ind → TPTP_Interpret.ind → bool"

consts
  bnd_c1 :: TPTP_Interpret.ind
  bnd_s :: "TPTP_Interpret.ind → TPTP_Interpret.ind"

lemma "(∀SX0. (¬ (¬ SX0 (PUZ114_5_bnd_sK4 SX0) (PUZ114_5_bnd_sK5 SX0) ∨
              ¬ (¬ SX0 (bnd_s (bnd_s (PUZ114_5_bnd_sK4 SX0)))
                    (PUZ114_5_bnd_sK5 SX0) ∨
                 ¬ SX0 (bnd_s (PUZ114_5_bnd_sK4 SX0))
                    (bnd_s (PUZ114_5_bnd_sK5 SX0)))) ∨
           ¬ SX0 bnd_c1 bnd_c1) ∨
          SX0 PUZ114_5_bnd_sK1 PUZ114_5_bnd_sK2) =
   True ==> ∀SV1. ((¬ (¬ SV1 (PUZ114_5_bnd_sK4 SV1) (PUZ114_5_bnd_sK5 SV1) ∨
              ¬ (¬ SV1 (bnd_s (bnd_s (PUZ114_5_bnd_sK4 SV1)))
                    (PUZ114_5_bnd_sK5 SV1) ∨
                 ¬ SV1 (bnd_s (PUZ114_5_bnd_sK4 SV1))
                    (bnd_s (PUZ114_5_bnd_sK5 SV1)))) ∨
           ¬ SV1 bnd_c1 bnd_c1) ∨
          SV1 PUZ114_5_bnd_sK1 PUZ114_5_bnd_sK2) =
         True"
by (tactic ‹full_extcnf_combined_tac @{context}›)

lemma "(¬ SEU581_2_bnd_subset (SEU581_2_bnd_dsetconstr SEU581_2_bnd_sK1 SEU581_2_bnd_sK2) SEU581_2_bnd_sK1) = True ==> (SEU581_2_bnd_subset (SEU581_2_bnd_dsetconstr SEU581_2_bnd_sK1 SEU581_2_bnd_sK2) SEU581_2_bnd_sK1) = False"
by (tactic ‹full_extcnf_combined_tac @{context}›)

(*testing repeated application of simulator*)
lemma "(¬ ¬ False) = True ==>
    SEU581_2_bnd_subset (SEU581_2_bnd_dsetconstr SEU581_2_bnd_sK1 SEU581_2_bnd_sK2) SEU581_2_bnd_sK1 = True ∨
    False = True ∨ False = True ∨ False = True"
by (tactic ‹full_extcnf_combined_tac @{context}›)

(*Testing non-normal conclusion. Ideally we should be able to apply
  the tactic to arbitrary chains of extcnf steps -- where it's not
  generally the case that the conclusions are normal.*)
lemma "(¬ ¬ False) = True ==>
    SEU581_2_bnd_subset (SEU581_2_bnd_dsetconstr SEU581_2_bnd_sK1 SEU581_2_bnd_sK2) SEU581_2_bnd_sK1 = True ∨
    (¬ False) = False"
by (tactic ‹full_extcnf_combined_tac @{context}›)

(*testing repeated application of simulator, involving different extcnf rules*)
lemma "(¬ ¬ (False | False)) = True ==>
    SEU581_2_bnd_subset (SEU581_2_bnd_dsetconstr SEU581_2_bnd_sK1 SEU581_2_bnd_sK2) SEU581_2_bnd_sK1 = True ∨
    False = True ∨ False = True ∨ False = True"
by (tactic ‹full_extcnf_combined_tac @{context}›)

(*testing logical expansion*)
lemma "(∀A B. SEU581_2_bnd_in B (SEU581_2_bnd_powerset A) ⟶ SEU581_2_bnd_subset B A) = True
\<Longrightarrow> (∀A B. ¬ SEU581_2_bnd_in B (SEU581_2_bnd_powerset A) ∨ SEU581_2_bnd_subset B A) = True"
by (tactic ‹full_extcnf_combined_tac @{context}›)

(*testing extcnf_forall_pos*)
lemma "(∀A Xphi. SEU581_2_bnd_in (SEU581_2_bnd_dsetconstr A Xphi) (SEU581_2_bnd_powerset A)) = True ==> ∀SV1. (∀SY14.
             SEU581_2_bnd_in (SEU581_2_bnd_dsetconstr SV1 SY14)
              (SEU581_2_bnd_powerset SV1)) = True"
by (tactic ‹full_extcnf_combined_tac @{context}›)

lemma "((∀A Xphi. SEU581_2_bnd_in (SEU581_2_bnd_dsetconstr A Xphi) (SEU581_2_bnd_powerset A)) = True) | ((~ False) = False) ==>
\<forall>SV1. ((∀SY14. SEU581_2_bnd_in (SEU581_2_bnd_dsetconstr SV1 SY14) (SEU581_2_bnd_powerset SV1)) = True) | ((~ False) = False)"
by (tactic ‹full_extcnf_combined_tac @{context}›)

(*testing parameters*)
lemma "(∀A B. SEU581_2_bnd_in B (SEU581_2_bnd_powerset A) ⟶ SEU581_2_bnd_subset B A) = True
\<Longrightarrow> ! X. (∀A B. ¬ SEU581_2_bnd_in B (SEU581_2_bnd_powerset A) ∨ SEU581_2_bnd_subset B A) = True"
by (tactic ‹full_extcnf_combined_tac @{context}›)

lemma "((? A .P1 A) = False) | P2 = True ==> !X. ((P1 X) = False | P2 = True)"
by (tactic ‹full_extcnf_combined_tac @{context}›)

lemma "((!A . (P1a A | P1b A)) = True) | (P2 = True) ==> !X. (P1a X = True | P1b X = True | P2 = True)"
by (tactic ‹full_extcnf_combined_tac @{context}›)

lemma "! Y. (((!A .(P1a A | P1b A)) = True) | P2 = True) ==> ! Y. (!X. (P1a X = True | P1b X = True | P2 = True))"
by (tactic ‹full_extcnf_combined_tac @{context}›)

lemma "! Y. (((!A .(P1a A | P1b A)) = True) | P2 = True) ==> ! Y. (!X. (P1a X = True | P1b X = True | P2 = True))"
by (tactic ‹full_extcnf_combined_tac @{context}›)

lemma "! Y. (((!A .(P1a A | P1b A)) = True) | P2 = True) ==> ! Y. (!X. (P1a X = True | P1b X = True | P2 = True))"
by (tactic ‹full_extcnf_combined_tac @{context}›)

consts dud_bnd_s :: "TPTP_Interpret.ind → TPTP_Interpret.ind"

(*this lemma kills blast*)
lemma "(¬ (∀SX0 SX1.
          ¬ PUZ114_5_bnd_sK3 SX0 SX1 ∨ PUZ114_5_bnd_sK3 (dud_bnd_s (dud_bnd_s SX0)) SX1) ∨
    ¬ (∀SX0 SX1.
          ¬ PUZ114_5_bnd_sK3 SX0 SX1 ∨
          PUZ114_5_bnd_sK3 (dud_bnd_s SX0) (dud_bnd_s SX1))) =
   False ==> (¬ (∀SX0 SX1.
          ¬ PUZ114_5_bnd_sK3 SX0 SX1 ∨
          PUZ114_5_bnd_sK3 (dud_bnd_s SX0) (dud_bnd_s SX1))) =
   False"
by (tactic ‹full_extcnf_combined_tac @{context}›)

(*testing logical expansion -- this should be done by blast*)
lemma "(∀A B. bnd_in B (bnd_powerset A) ⟶ SEU581_2_bnd_subset B A) = True
\<Longrightarrow> (∀A B. ¬ bnd_in B (bnd_powerset A) ∨ SEU581_2_bnd_subset B A) = True"
by (tactic ‹full_extcnf_combined_tac @{context}›)

(*testing related to PUZ114^5.p.out*)
lemma "∀SV1. ((¬ (¬ SV1 (PUZ114_5_bnd_sK4 SV1) (PUZ114_5_bnd_sK5 SV1) ∨
                    ¬ (¬ SV1 (bnd_s (bnd_s (PUZ114_5_bnd_sK4 SV1)))
                          (PUZ114_5_bnd_sK5 SV1) ∨
                       ¬ SV1 (bnd_s (PUZ114_5_bnd_sK4 SV1))
                          (bnd_s (PUZ114_5_bnd_sK5 SV1))))) =
                True ∨
                (¬ SV1 bnd_c1 bnd_c1) = True) ∨
               SV1 PUZ114_5_bnd_sK1 PUZ114_5_bnd_sK2 = True ==>
         ∀SV1. (SV1 bnd_c1 bnd_c1 = False ∨
                (¬ (¬ SV1 (PUZ114_5_bnd_sK4 SV1) (PUZ114_5_bnd_sK5 SV1) ∨
                    ¬ (¬ SV1 (bnd_s (bnd_s (PUZ114_5_bnd_sK4 SV1)))
                          (PUZ114_5_bnd_sK5 SV1) ∨
                       ¬ SV1 (bnd_s (PUZ114_5_bnd_sK4 SV1))
                          (bnd_s (PUZ114_5_bnd_sK5 SV1))))) =
                True) ∨
               SV1 PUZ114_5_bnd_sK1 PUZ114_5_bnd_sK2 = True"
by (tactic ‹full_extcnf_combined_tac @{context}›)

lemma "∀SV2. (∀SY41.
                   ¬ PUZ114_5_bnd_sK3 SV2 SY41 ∨
                   PUZ114_5_bnd_sK3 (dud_bnd_s (dud_bnd_s SV2)) SY41) =
               True ==>
         ∀SV4 SV2.
            (¬ PUZ114_5_bnd_sK3 SV2 SV4 ∨
             PUZ114_5_bnd_sK3 (dud_bnd_s (dud_bnd_s SV2)) SV4) =
            True"
by (tactic ‹full_extcnf_combined_tac @{context}›)

lemma "∀SV3. (∀SY42.
                   ¬ PUZ114_5_bnd_sK3 SV3 SY42 ∨
                   PUZ114_5_bnd_sK3 (dud_bnd_s SV3) (dud_bnd_s SY42)) =
               True ==>
         ∀SV5 SV3.
            (¬ PUZ114_5_bnd_sK3 SV3 SV5 ∨
             PUZ114_5_bnd_sK3 (dud_bnd_s SV3) (dud_bnd_s SV5)) =
            True"
by (tactic ‹full_extcnf_combined_tac @{context}›)


subsection "unfold_def"
     (* (Annotated_step ("9", "unfold_def"), *)
lemma "bnd_kpairiskpair =
             (ALL Xx Xy.
                 bnd_iskpair
                  (bnd_setadjoin (bnd_setadjoin Xx bnd_emptyset)
                    (bnd_setadjoin (bnd_setadjoin Xx (bnd_setadjoin Xy bnd_emptyset))
                      bnd_emptyset))) &
             bnd_kpair =
             (%Xx Xy.
                 bnd_setadjoin (bnd_setadjoin Xx bnd_emptyset)
                  (bnd_setadjoin (bnd_setadjoin Xx (bnd_setadjoin Xy bnd_emptyset))
                    bnd_emptyset)) &
             bnd_iskpair =
             (%A. EX Xx. bnd_in Xx (bnd_setunion A) &
                         (EX Xy. bnd_in Xy (bnd_setunion A) &
                                 A = bnd_setadjoin (bnd_setadjoin Xx bnd_emptyset)
                                      (bnd_setadjoin
                                        (bnd_setadjoin Xx
(bnd_setadjoin Xy bnd_emptyset))
                                        bnd_emptyset))) &
             (~ (ALL SY0 SY1.
                    EX SY3.
                       bnd_in SY3
                        (bnd_setunion
                          (bnd_setadjoin (bnd_setadjoin SY0 bnd_emptyset)
                            (bnd_setadjoin
                              (bnd_setadjoin SY0 (bnd_setadjoin SY1 bnd_emptyset))
                              bnd_emptyset))) &
                       (EX SY4.
                           bnd_in SY4
                            (bnd_setunion
                              (bnd_setadjoin (bnd_setadjoin SY0 bnd_emptyset)
                                (bnd_setadjoin
                                  (bnd_setadjoin SY0
                                    (bnd_setadjoin SY1 bnd_emptyset))
                                  bnd_emptyset))) &
                           bnd_setadjoin (bnd_setadjoin SY0 bnd_emptyset)
                            (bnd_setadjoin
                              (bnd_setadjoin SY0 (bnd_setadjoin SY1 bnd_emptyset))
                              bnd_emptyset) =
                           bnd_setadjoin (bnd_setadjoin SY3 bnd_emptyset)
                            (bnd_setadjoin
                              (bnd_setadjoin SY3 (bnd_setadjoin SY4 bnd_emptyset))
                              bnd_emptyset)))) =
             True
             ==> (~ (ALL SX0 SX1.
                        ~ (ALL SX2.
                              ~ ~ (~ bnd_in SX2
                                      (bnd_setunion
                                        (bnd_setadjoin
(bnd_setadjoin SX0 bnd_emptyset)
(bnd_setadjoin (bnd_setadjoin SX0 (bnd_setadjoin SX1 bnd_emptyset)) bnd_emptyset))) |
                                   ~ ~ (ALL SX3.
 ~ ~ (~ bnd_in SX3
         (bnd_setunion
           (bnd_setadjoin (bnd_setadjoin SX0 bnd_emptyset)
             (bnd_setadjoin (bnd_setadjoin SX0 (bnd_setadjoin SX1 bnd_emptyset))
               bnd_emptyset))) |
      bnd_setadjoin (bnd_setadjoin SX0 bnd_emptyset)
       (bnd_setadjoin (bnd_setadjoin SX0 (bnd_setadjoin SX1 bnd_emptyset))
         bnd_emptyset) ~=
      bnd_setadjoin (bnd_setadjoin SX2 bnd_emptyset)
       (bnd_setadjoin (bnd_setadjoin SX2 (bnd_setadjoin SX3 bnd_emptyset))
         bnd_emptyset))))))) =
                 True"
by (tactic ‹unfold_def_tac @{context} []›)

     (* (Annotated_step ("10", "unfold_def"), *)
lemma "bnd_kpairiskpair =
             (ALL Xx Xy.
                 bnd_iskpair
                  (bnd_setadjoin (bnd_setadjoin Xx bnd_emptyset)
                    (bnd_setadjoin (bnd_setadjoin Xx (bnd_setadjoin Xy bnd_emptyset))
                      bnd_emptyset))) &
             bnd_kpair =
             (%Xx Xy.
                 bnd_setadjoin (bnd_setadjoin Xx bnd_emptyset)
                  (bnd_setadjoin (bnd_setadjoin Xx (bnd_setadjoin Xy bnd_emptyset))
                    bnd_emptyset)) &
             bnd_iskpair =
             (%A. EX Xx. bnd_in Xx (bnd_setunion A) &
                         (EX Xy. bnd_in Xy (bnd_setunion A) &
                                 A = bnd_setadjoin (bnd_setadjoin Xx bnd_emptyset)
                                      (bnd_setadjoin
                                        (bnd_setadjoin Xx
(bnd_setadjoin Xy bnd_emptyset))
                                        bnd_emptyset))) &
             (ALL SY5 SY6.
                 EX SY7.
                    bnd_in SY7
                     (bnd_setunion
                       (bnd_setadjoin (bnd_setadjoin SY5 bnd_emptyset)
                         (bnd_setadjoin
                           (bnd_setadjoin SY5 (bnd_setadjoin SY6 bnd_emptyset))
                           bnd_emptyset))) &
                    (EX SY8.
                        bnd_in SY8
                         (bnd_setunion
                           (bnd_setadjoin (bnd_setadjoin SY5 bnd_emptyset)
                             (bnd_setadjoin
                               (bnd_setadjoin SY5 (bnd_setadjoin SY6 bnd_emptyset))
                               bnd_emptyset))) &
                        bnd_setadjoin (bnd_setadjoin SY5 bnd_emptyset)
                         (bnd_setadjoin
                           (bnd_setadjoin SY5 (bnd_setadjoin SY6 bnd_emptyset))
                           bnd_emptyset) =
                        bnd_setadjoin (bnd_setadjoin SY7 bnd_emptyset)
                         (bnd_setadjoin
                           (bnd_setadjoin SY7 (bnd_setadjoin SY8 bnd_emptyset))
                           bnd_emptyset))) =
             True
             ==> (ALL SX0 SX1.
                     ~ (ALL SX2.
                           ~ ~ (~ bnd_in SX2
                                   (bnd_setunion
                                     (bnd_setadjoin (bnd_setadjoin SX0 bnd_emptyset)
                                       (bnd_setadjoin
                                         (bnd_setadjoin SX0
 (bnd_setadjoin SX1 bnd_emptyset))
                                         bnd_emptyset))) |
                                ~ ~ (ALL SX3.
                                        ~ ~ (~ bnd_in SX3
      (bnd_setunion
        (bnd_setadjoin (bnd_setadjoin SX0 bnd_emptyset)
          (bnd_setadjoin (bnd_setadjoin SX0 (bnd_setadjoin SX1 bnd_emptyset))
            bnd_emptyset))) |
   bnd_setadjoin (bnd_setadjoin SX0 bnd_emptyset)
    (bnd_setadjoin (bnd_setadjoin SX0 (bnd_setadjoin SX1 bnd_emptyset))
      bnd_emptyset) ~=
   bnd_setadjoin (bnd_setadjoin SX2 bnd_emptyset)
    (bnd_setadjoin (bnd_setadjoin SX2 (bnd_setadjoin SX3 bnd_emptyset))
      bnd_emptyset)))))) =
                 True"
by (tactic ‹unfold_def_tac @{context} []›)

     (* (Annotated_step ("12", "unfold_def"), *)
lemma "bnd_cCKB6_BLACK =
         (λXu Xv.
             ∀Xw. Xw bnd_c1 bnd_c1 ∧
                  (∀Xj Xk.
                      Xw Xj Xk ⟶
                      Xw (bnd_s (bnd_s Xj)) Xk ∧
                      Xw (bnd_s Xj) (bnd_s Xk)) ⟶
                  Xw Xu Xv) ∧
         ((((∀SY36 SY37.
                ¬ PUZ114_5_bnd_sK3 SY36 SY37 ∨
                PUZ114_5_bnd_sK3 (bnd_s (bnd_s SY36)) SY37) ∧
            (∀SY38 SY39.
                ¬ PUZ114_5_bnd_sK3 SY38 SY39 ∨
                PUZ114_5_bnd_sK3 (bnd_s SY38) (bnd_s SY39))) ∧
           PUZ114_5_bnd_sK3 bnd_c1 bnd_c1) ∧
          ¬ PUZ114_5_bnd_sK3 (bnd_s (bnd_s (bnd_s PUZ114_5_bnd_sK1)))
             (bnd_s PUZ114_5_bnd_sK2)) =
         True ==>
         (¬ (¬ ¬ (¬ ¬ (¬ (∀SX0 SX1.
                             ¬ PUZ114_5_bnd_sK3 SX0 SX1 ∨
                             PUZ114_5_bnd_sK3 (bnd_s (bnd_s SX0)) SX1) ∨
                       ¬ (∀SX0 SX1.
                             ¬ PUZ114_5_bnd_sK3 SX0 SX1 ∨
                             PUZ114_5_bnd_sK3 (bnd_s SX0) (bnd_s SX1))) ∨
                  ¬ PUZ114_5_bnd_sK3 bnd_c1 bnd_c1) ∨
             ¬ ¬ PUZ114_5_bnd_sK3 (bnd_s (bnd_s (bnd_s PUZ114_5_bnd_sK1)))
                  (bnd_s PUZ114_5_bnd_sK2))) =
         True"
(*
apply (erule conjE)+
apply (erule subst)+
apply (tactic {*log_expander 1*})+
apply (rule refl)
*)
by (tactic ‹unfold_def_tac @{context} []›)

     (* (Annotated_step ("13", "unfold_def"), *)
lemma "bnd_cCKB6_BLACK =
         (λXu Xv.
             ∀Xw. Xw bnd_c1 bnd_c1 ∧
                  (∀Xj Xk.
                      Xw Xj Xk ⟶
                      Xw (bnd_s (bnd_s Xj)) Xk ∧
                      Xw (bnd_s Xj) (bnd_s Xk)) ⟶
                  Xw Xu Xv) ∧
         (∀SY30.
             (SY30 (PUZ114_5_bnd_sK4 SY30) (PUZ114_5_bnd_sK5 SY30) ∧
              (¬ SY30 (bnd_s (bnd_s (PUZ114_5_bnd_sK4 SY30)))
                  (PUZ114_5_bnd_sK5 SY30) ∨
               ¬ SY30 (bnd_s (PUZ114_5_bnd_sK4 SY30))
                  (bnd_s (PUZ114_5_bnd_sK5 SY30))) ∨
              ¬ SY30 bnd_c1 bnd_c1) ∨
             SY30 PUZ114_5_bnd_sK1 PUZ114_5_bnd_sK2) =
         True ==>
         (∀SX0. (¬ (¬ SX0 (PUZ114_5_bnd_sK4 SX0) (PUZ114_5_bnd_sK5 SX0) ∨
                    ¬ (¬ SX0 (bnd_s (bnd_s (PUZ114_5_bnd_sK4 SX0)))
                          (PUZ114_5_bnd_sK5 SX0) ∨
                       ¬ SX0 (bnd_s (PUZ114_5_bnd_sK4 SX0))
                          (bnd_s (PUZ114_5_bnd_sK5 SX0)))) ∨
                 ¬ SX0 bnd_c1 bnd_c1) ∨
                SX0 PUZ114_5_bnd_sK1 PUZ114_5_bnd_sK2) =
         True"
(*
apply (erule conjE)+
apply (tactic {*expander_animal 1*})+
apply assumption
*)
by (tactic ‹unfold_def_tac @{context} []›)

(*FIXME move this heuristic elsewhere*)
ML ‹
 
 expects a parameter indicating the smallest integer.
  (Using Int.minInt isn't always viable).*)
fun max_int_floored min l =
  if null l then raise List.Empty
  else fold (curry Int.max) l min;

val _ = @{assert} (max_int_floored ~101002 [1]  = 1)
val _ = @{assert} (max_int_floored 0 [1, 3, 5] = 5)

fun max_index_floored min l =
  let
    val max = max_int_floored min l
  in find_index (pair max #> (=)) l end
›

ML ‹
max_index_floored 0 [1, 3, 5]
\<close>

ML \<open>
(*
Given argument ([h_1, ..., h_n], conc),
obtained from term of form
  h_1 ==> ... ==> h_n ==> conclusion,
this function indicates which h_i is biggest,
or NONE if h_n = 0.
*)
fun biggest_hypothesis (hypos, _) =
  if null hypos then NONE
  else
    map size_of_term hypos
    |> max_index_floored 0
    |> SOME
›

ML ‹
fun biggest_hyp_first_tac i = fn st =>
  let
    val results = TERMFUN biggest_hypothesis (SOME i) st
  in
    if null results then no_tac st
    else
      let
        val result = the_single results
      in
        case result of
            NONE => no_tac st
          | SOME n =>
              if n > 0 then rotate_tac n i st else no_tac st
      end
  end
\<close>

     (* (Annotated_step ("6", "unfold_def"), *)
lemma  "(¬ (∃U :: TPTP_Interpret.ind → bool. ∀V. U V = SEV405_5_bnd_cA)) = True ==>
         (¬ ¬ (∀SX0 :: TPTP_Interpret.ind → bool. ¬ (∀SX1. ¬ (¬ (¬ SX0 SX1 ∨ SEV405_5_bnd_cA) ∨
 ¬ (¬ SEV405_5_bnd_cA ∨ SX0 SX1))))) =
         True"
(* by (tactic {*unfold_def_tac []*}) *)
oops

subsection "Using leo2_tac"
(*these require PUZ114^5's proof to be loaded

ML {*leo2_tac @{context} (hd prob_names) "50"*}

ML {*leo2_tac @{context} (hd prob_names) "4"*}

ML {*leo2_tac @{context} (hd prob_names) "9"*}

     (* (Annotated_step ("9", "extcnf_combined"), *)
lemma "(∀SY30.
             SY30 bnd_c1 bnd_c1 ∧
             (∀Xj Xk.
                 SY30 Xj Xk ⟶
                 SY30 (bnd_s (bnd_s Xj)) Xk ∧
                 SY30 (bnd_s Xj) (bnd_s Xk)) ⟶
             SY30 bnd_sK1 bnd_sK2) =
         True ==>
         (∀SY30.
             (SY30 (bnd_sK4 SY30) (bnd_sK5 SY30) ∧
              (¬ SY30 (bnd_s (bnd_s (bnd_sK4 SY30)))
                  (bnd_sK5 SY30) ∨
               ¬ SY30 (bnd_s (bnd_sK4 SY30))
                  (bnd_s (bnd_sK5 SY30))) ∨
              ¬ SY30 bnd_c1 bnd_c1) ∨
             SY30 bnd_sK1 bnd_sK2) =
         True"
by (tactic {*rtac (leo2_tac @{context} (hd prob_names) "9") 1*})
*)



typedecl GEG007_1_bnd_reg
consts
  GEG007_1_bnd_sK7_SX2 :: "TPTP_Interpret.ind → TPTP_Interpret.ind → GEG007_1_bnd_reg"
  GEG007_1_bnd_sK6_SX2 :: "TPTP_Interpret.ind → TPTP_Interpret.ind → GEG007_1_bnd_reg"
  GEG007_1_bnd_a :: "TPTP_Interpret.ind → TPTP_Interpret.ind → bool"
  GEG007_1_bnd_catalunya  :: "GEG007_1_bnd_reg"
  GEG007_1_bnd_spain :: "GEG007_1_bnd_reg"
  GEG007_1_bnd_c :: "GEG007_1_bnd_reg → GEG007_1_bnd_reg → bool"

     (* (Annotated_step ("147", "extcnf_forall_neg"), *)
lemma "∀SV13 SV6.
            (∀SX2. ¬ GEG007_1_bnd_c SX2 GEG007_1_bnd_spain ∨
                   GEG007_1_bnd_c SX2 GEG007_1_bnd_catalunya) =
            False ∨
            GEG007_1_bnd_a SV6 SV13 = False ==>
         ∀SV6 SV13.
            (¬ GEG007_1_bnd_c (GEG007_1_bnd_sK7_SX2 SV13 SV6) GEG007_1_bnd_spain ∨
             GEG007_1_bnd_c (GEG007_1_bnd_sK7_SX2 SV13 SV6) GEG007_1_bnd_catalunya) =
            False ∨
            GEG007_1_bnd_a SV6 SV13 = False"
by (tactic ‹nonfull_extcnf_combined_tac @{context} [Existential_Var]›)

     (* (Annotated_step ("116", "extcnf_forall_neg"), *)
lemma "∀SV13 SV6.
            (∀SX2. ¬ ¬ (¬ ¬ (¬ GEG007_1_bnd_c SX2 GEG007_1_bnd_catalunya ∨
                             ¬ ¬ ¬ (∀SX3.
       ¬ ¬ (¬ (∀SX4. ¬ GEG007_1_bnd_c SX4 SX3 ∨ GEG007_1_bnd_c SX4 SX2) ∨
            ¬ (∀SX4. ¬ GEG007_1_bnd_c SX4 SX3 ∨
                     GEG007_1_bnd_c SX4 GEG007_1_bnd_catalunya)))) ∨
                        ¬ ¬ (¬ GEG007_1_bnd_c SX2 GEG007_1_bnd_spain ∨
                             ¬ ¬ ¬ (∀SX3.
       ¬ ¬ (¬ (∀SX4. ¬ GEG007_1_bnd_c SX4 SX3 ∨ GEG007_1_bnd_c SX4 SX2) ∨
            ¬ (∀SX4. ¬ GEG007_1_bnd_c SX4 SX3 ∨
                     GEG007_1_bnd_c SX4 GEG007_1_bnd_spain)))))) =
            False ∨
            GEG007_1_bnd_a SV6 SV13 = False ==>
         ∀SV6 SV13.
            (¬ ¬ (¬ ¬ (¬ GEG007_1_bnd_c (GEG007_1_bnd_sK6_SX2 SV13 SV6)
                          GEG007_1_bnd_catalunya ∨
                       ¬ ¬ ¬ (∀SY68.
 ¬ ¬ (¬ (∀SY69.
            ¬ GEG007_1_bnd_c SY69 SY68 ∨
            GEG007_1_bnd_c SY69 (GEG007_1_bnd_sK6_SX2 SV13 SV6)) ∨
      ¬ (∀SX4. ¬ GEG007_1_bnd_c SX4 SY68 ∨ GEG007_1_bnd_c SX4 GEG007_1_bnd_catalunya)))) ∨
                  ¬ ¬ (¬ GEG007_1_bnd_c (GEG007_1_bnd_sK6_SX2 SV13 SV6)
                          GEG007_1_bnd_spain ∨
                       ¬ ¬ ¬ (∀SY71.
 ¬ ¬ (¬ (∀SY72.
            ¬ GEG007_1_bnd_c SY72 SY71 ∨
            GEG007_1_bnd_c SY72 (GEG007_1_bnd_sK6_SX2 SV13 SV6)) ∨
      ¬ (∀SX4. ¬ GEG007_1_bnd_c SX4 SY71 ∨ GEG007_1_bnd_c SX4 GEG007_1_bnd_spain)))))) =
            False ∨
            GEG007_1_bnd_a SV6 SV13 = False"
by (tactic ‹nonfull_extcnf_combined_tac @{context} [Existential_Var]›)

consts PUZ107_5_bnd_sK1_SX0 ::
  "TPTP_Interpret.ind
      → TPTP_Interpret.ind
        → TPTP_Interpret.ind → TPTP_Interpret.ind → bool"

lemma "∀(SV4::TPTP_Interpret.ind) (SV8::TPTP_Interpret.ind)
   (SV6::TPTP_Interpret.ind) (SV2::TPTP_Interpret.ind)
   (SV3::TPTP_Interpret.ind) SV1::TPTP_Interpret.ind.
   ((SV1 ≠ SV3) = False ∨ PUZ107_5_bnd_sK1_SX0 SV1 SV2 SV6 SV8 = False) ∨
   PUZ107_5_bnd_sK1_SX0 SV3 SV4 SV6 SV8 = False ==>
\<forall>(SV4::TPTP_Interpret.ind) (SV8::TPTP_Interpret.ind)
   (SV6::TPTP_Interpret.ind) (SV2::TPTP_Interpret.ind)
   (SV3::TPTP_Interpret.ind) SV1::TPTP_Interpret.ind.
   ((SV1 = SV3) = True ∨ PUZ107_5_bnd_sK1_SX0 SV1 SV2 SV6 SV8 = False) ∨
   PUZ107_5_bnd_sK1_SX0 SV3 SV4 SV6 SV8 = False"
by (tactic ‹nonfull_extcnf_combined_tac @{context} [Not_neg]›)

lemma "
\<forall>(SV8::TPTP_Interpret.ind) (SV6::TPTP_Interpret.ind)
   (SV4::TPTP_Interpret.ind) (SV2::TPTP_Interpret.ind)
   (SV3::TPTP_Interpret.ind) SV1::TPTP_Interpret.ind.
   ((SV1 ≠ SV3 ∨ SV2 ≠ SV4) = False ∨
    PUZ107_5_bnd_sK1_SX0 SV1 SV2 SV6 SV8 = False) ∨
   PUZ107_5_bnd_sK1_SX0 SV3 SV4 SV6 SV8 = False ==>
\<forall>(SV4::TPTP_Interpret.ind) (SV8::TPTP_Interpret.ind)
   (SV6::TPTP_Interpret.ind) (SV2::TPTP_Interpret.ind)
   (SV3::TPTP_Interpret.ind) SV1::TPTP_Interpret.ind.
   ((SV1 ≠ SV3) = False ∨ PUZ107_5_bnd_sK1_SX0 SV1 SV2 SV6 SV8 = False) ∨
   PUZ107_5_bnd_sK1_SX0 SV3 SV4 SV6 SV8 = False"
by (tactic ‹nonfull_extcnf_combined_tac @{context} [Or_neg]›)

consts
  NUM016_5_bnd_a :: TPTP_Interpret.ind
  NUM016_5_bnd_prime :: "TPTP_Interpret.ind → bool"
  NUM016_5_bnd_factorial_plus_one :: "TPTP_Interpret.ind → TPTP_Interpret.ind"
  NUM016_5_bnd_prime_divisor :: "TPTP_Interpret.ind → TPTP_Interpret.ind"
  NUM016_5_bnd_divides :: "TPTP_Interpret.ind → TPTP_Interpret.ind → bool"
  NUM016_5_bnd_less :: "TPTP_Interpret.ind → TPTP_Interpret.ind → bool"

     (* (Annotated_step ("6", "unfold_def"), *)
lemma "((((((((((((∀X::TPTP_Interpret.ind. ¬ NUM016_5_bnd_less X X) ∧
                    (∀(X::TPTP_Interpret.ind)
                        Y::TPTP_Interpret.ind.
                        ¬ NUM016_5_bnd_less X Y ∨ ¬ NUM016_5_bnd_less Y X)) ∧
                   (∀X::TPTP_Interpret.ind. NUM016_5_bnd_divides X X)) ∧
                  (∀(X::TPTP_Interpret.ind)
                      (Y::TPTP_Interpret.ind)
                      Z::TPTP_Interpret.ind.
                      (¬ NUM016_5_bnd_divides X Y ∨ ¬ NUM016_5_bnd_divides Y Z) ∨
                      NUM016_5_bnd_divides X Z)) ∧
                 (∀(X::TPTP_Interpret.ind) Y::TPTP_Interpret.ind.
                     ¬ NUM016_5_bnd_divides X Y ∨ ¬ NUM016_5_bnd_less Y X)) ∧
                (∀X::TPTP_Interpret.ind.
                    NUM016_5_bnd_less X (NUM016_5_bnd_factorial_plus_one X))) ∧
               (∀(X::TPTP_Interpret.ind) Y::TPTP_Interpret.ind.
                   ¬ NUM016_5_bnd_divides X (NUM016_5_bnd_factorial_plus_one Y) ∨
                   NUM016_5_bnd_less Y X)) ∧
              (∀X::TPTP_Interpret.ind.
                  NUM016_5_bnd_prime X ∨
                  NUM016_5_bnd_divides (NUM016_5_bnd_prime_divisor X) X)) ∧
             (∀X::TPTP_Interpret.ind.
                 NUM016_5_bnd_prime X ∨
                 NUM016_5_bnd_prime (NUM016_5_bnd_prime_divisor X))) ∧
            (∀X::TPTP_Interpret.ind.
                NUM016_5_bnd_prime X ∨
                NUM016_5_bnd_less (NUM016_5_bnd_prime_divisor X) X)) ∧
           NUM016_5_bnd_prime NUM016_5_bnd_a) ∧
          (∀X::TPTP_Interpret.ind.
              (¬ NUM016_5_bnd_prime X ∨ ¬ NUM016_5_bnd_less NUM016_5_bnd_a X) ∨
              NUM016_5_bnd_less (NUM016_5_bnd_factorial_plus_one NUM016_5_bnd_a) X)) =
         True ==>
         (¬ (¬ ¬ (¬ ¬ (¬ ¬ (¬ ¬ (¬ ¬ (¬ ¬ (¬ ¬ (¬ ¬ (¬ ¬ (¬ ¬ (¬ (∀SX0::TPTP_Interpret.ind.
     ¬ NUM016_5_bnd_less SX0 SX0) ∨
                               ¬ (∀(SX0::TPTP_Interpret.ind)
     SX1::TPTP_Interpret.ind.
     ¬ NUM016_5_bnd_less SX0 SX1 ∨ ¬ NUM016_5_bnd_less SX1 SX0)) ∨
                          ¬ (∀SX0::TPTP_Interpret.ind.
NUM016_5_bnd_divides SX0 SX0)) ∨
                     ¬ (∀(SX0::TPTP_Interpret.ind)
                           (SX1::TPTP_Interpret.ind)
                           SX2::TPTP_Interpret.ind.
                           (¬ NUM016_5_bnd_divides SX0 SX1 ∨
                            ¬ NUM016_5_bnd_divides SX1 SX2) ∨
                           NUM016_5_bnd_divides SX0 SX2)) ∨
                ¬ (∀(SX0::TPTP_Interpret.ind)
                      SX1::TPTP_Interpret.ind.
                      ¬ NUM016_5_bnd_divides SX0 SX1 ∨
                      ¬ NUM016_5_bnd_less SX1 SX0)) ∨
           ¬ (∀SX0::TPTP_Interpret.ind.
                 NUM016_5_bnd_less SX0 (NUM016_5_bnd_factorial_plus_one SX0))) ∨
      ¬ (∀(SX0::TPTP_Interpret.ind) SX1::TPTP_Interpret.ind.
            ¬ NUM016_5_bnd_divides SX0 (NUM016_5_bnd_factorial_plus_one SX1) ∨
            NUM016_5_bnd_less SX1 SX0)) ∨
 ¬ (∀SX0::TPTP_Interpret.ind.
       NUM016_5_bnd_prime SX0 ∨
       NUM016_5_bnd_divides (NUM016_5_bnd_prime_divisor SX0) SX0)) ∨
                            ¬ (∀SX0::TPTP_Interpret.ind.
  NUM016_5_bnd_prime SX0 ∨ NUM016_5_bnd_prime (NUM016_5_bnd_prime_divisor SX0))) ∨
                       ¬ (∀SX0::TPTP_Interpret.ind.
                             NUM016_5_bnd_prime SX0 ∨
                             NUM016_5_bnd_less (NUM016_5_bnd_prime_divisor SX0)
                              SX0)) ∨
                  ¬ NUM016_5_bnd_prime NUM016_5_bnd_a) ∨
             ¬ (∀SX0::TPTP_Interpret.ind.
                   (¬ NUM016_5_bnd_prime SX0 ∨ ¬ NUM016_5_bnd_less NUM016_5_bnd_a SX0) ∨
                   NUM016_5_bnd_less (NUM016_5_bnd_factorial_plus_one NUM016_5_bnd_a)
                    SX0))) =
         True"
by (tactic ‹unfold_def_tac @{context} []›)

     (* (Annotated_step ("3", "unfold_def"), *)
lemma "(~ ((((((((((((ALL X. ~ bnd_less X X) &
                           (ALL X Y. ~ bnd_less X Y | ~ bnd_less Y X)) &
                          (ALL X. bnd_divides X X)) &
                         (ALL X Y Z.
                             (~ bnd_divides X Y | ~ bnd_divides Y Z) |
                             bnd_divides X Z)) &
                        (ALL X Y. ~ bnd_divides X Y | ~ bnd_less Y X)) &
                       (ALL X. bnd_less X (bnd_factorial_plus_one X))) &
                      (ALL X Y.
                          ~ bnd_divides X (bnd_factorial_plus_one Y) |
                          bnd_less Y X)) &
                     (ALL X. bnd_prime X | bnd_divides (bnd_prime_divisor X) X)) &
                    (ALL X. bnd_prime X | bnd_prime (bnd_prime_divisor X))) &
                   (ALL X. bnd_prime X | bnd_less (bnd_prime_divisor X) X)) &
                  bnd_prime bnd_a) &
                 (ALL X. (~ bnd_prime X | ~ bnd_less bnd_a X) |
                         bnd_less (bnd_factorial_plus_one bnd_a) X))) =
             False
             ==> (~ ((((((((((((ALL X. ~ bnd_less X X) &
                               (ALL X Y. ~ bnd_less X Y | ~ bnd_less Y X)) &
                              (ALL X. bnd_divides X X)) &
                             (ALL X Y Z.
                                 (~ bnd_divides X Y | ~ bnd_divides Y Z) |
                                 bnd_divides X Z)) &
                            (ALL X Y. ~ bnd_divides X Y | ~ bnd_less Y X)) &
                           (ALL X. bnd_less X (bnd_factorial_plus_one X))) &
                          (ALL X Y.
                              ~ bnd_divides X (bnd_factorial_plus_one Y) |
                              bnd_less Y X)) &
                         (ALL X. bnd_prime X |
                                 bnd_divides (bnd_prime_divisor X) X)) &
                        (ALL X. bnd_prime X | bnd_prime (bnd_prime_divisor X))) &
                       (ALL X. bnd_prime X | bnd_less (bnd_prime_divisor X) X)) &
                      bnd_prime bnd_a) &
                     (ALL X. (~ bnd_prime X | ~ bnd_less bnd_a X) |
                             bnd_less (bnd_factorial_plus_one bnd_a) X))) =
                 False"
by (tactic ‹unfold_def_tac @{context} []›)

(* SET062^6.p.out
      [[(Annotated_step ("3", "unfold_def"), *)
lemma "(∀Z3. False ⟶ bnd_cA Z3) = False ==>
         (∀Z3. False ⟶ bnd_cA Z3) = False"
by (tactic ‹unfold_def_tac @{context} []›)

(*
(* SEU559^2.p.out *)
   (* [[(Annotated_step ("3", "unfold_def"), *)
lemma "bnd_subset = (λA B. ∀Xx. bnd_in Xx A ⟶ bnd_in Xx B) ∧
         (∀A B. (∀Xx. bnd_in Xx A ⟶ bnd_in Xx B) ⟶
                bnd_subset A B) =
         False ==>
         (∀SY0 SY1.
             (∀Xx. bnd_in Xx SY0 ⟶ bnd_in Xx SY1) ⟶
             (∀SY5. bnd_in SY5 SY0 ⟶ bnd_in SY5 SY1)) =
         False"
by (tactic {*unfold_def_tac [@{thm bnd_subset_def}]*})

(* SEU559^2.p.out
    [[(Annotated_step ("6", "unfold_def"), *)
lemma "(¬ (∃Xx. ∀Xy. Xx ⟶ Xy)) = True ==>
         (¬ ¬ (∀SX0. ¬ (∀SX1. ¬ SX0 ∨ SX1))) = True"
by (tactic {*unfold_def_tac []*})

(* SEU502^2.p.out
    [[(Annotated_step ("3", "unfold_def"), *)
lemma "bnd_emptysetE =
         (∀Xx. bnd_in Xx bnd_emptyset ⟶ (∀Xphi. Xphi)) ∧
         (bnd_emptysetE ⟶
          (∀Xx. bnd_in Xx bnd_emptyset ⟶ False)) =
         False ==>
         ((∀Xx. bnd_in Xx bnd_emptyset ⟶ (∀Xphi. Xphi)) ⟶
          (∀Xx. bnd_in Xx bnd_emptyset ⟶ False)) =
         False"
by (tactic {*unfold_def_tac [@{thm bnd_emptysetE_def}]*})
*)

typedecl AGT037_2_bnd_mu
consts
  AGT037_2_bnd_sK1_SX0 :: TPTP_Interpret.ind
  AGT037_2_bnd_cola :: AGT037_2_bnd_mu
  AGT037_2_bnd_jan :: AGT037_2_bnd_mu
  AGT037_2_bnd_possibly_likes :: "AGT037_2_bnd_mu → AGT037_2_bnd_mu → TPTP_Interpret.ind → bool"
  AGT037_2_bnd_sK5_SY68 ::
    "TPTP_Interpret.ind
     → AGT037_2_bnd_mu
       → AGT037_2_bnd_mu
         → TPTP_Interpret.ind → TPTP_Interpret.ind"
  AGT037_2_bnd_likes :: "AGT037_2_bnd_mu → AGT037_2_bnd_mu → TPTP_Interpret.ind → bool"
  AGT037_2_bnd_very_much_likes :: "AGT037_2_bnd_mu → AGT037_2_bnd_mu → TPTP_Interpret.ind → bool"
  AGT037_2_bnd_a1 :: "TPTP_Interpret.ind → TPTP_Interpret.ind → bool"
  AGT037_2_bnd_a2 :: "TPTP_Interpret.ind → TPTP_Interpret.ind → bool"
  AGT037_2_bnd_a3 :: "TPTP_Interpret.ind → TPTP_Interpret.ind → bool"

(*test that nullary skolem terms are OK*)
     (* (Annotated_step ("79", "extcnf_forall_neg"), *)
lemma "(∀SX0::TPTP_Interpret.ind.
             AGT037_2_bnd_possibly_likes AGT037_2_bnd_jan AGT037_2_bnd_cola SX0) =
         False ==>
         AGT037_2_bnd_possibly_likes AGT037_2_bnd_jan AGT037_2_bnd_cola AGT037_2_bnd_sK1_SX0 =
         False"
by (tactic ‹nonfull_extcnf_combined_tac @{context} [Existential_Var]›)

     (* (Annotated_step ("202", "extcnf_forall_neg"), *)
lemma "∀(SV13::TPTP_Interpret.ind) (SV39::AGT037_2_bnd_mu) (SV29::AGT037_2_bnd_mu)
            SV45::TPTP_Interpret.ind.
            ((((∀SY68::TPTP_Interpret.ind.
                   ¬ AGT037_2_bnd_a1 SV45 SY68 ∨
                   AGT037_2_bnd_likes SV29 SV39 SY68) =
               False ∨
               (¬ (∀SY69::TPTP_Interpret.ind.
                      ¬ AGT037_2_bnd_a2 SV45 SY69 ∨
                      AGT037_2_bnd_likes SV29 SV39 SY69)) =
               True) ∨
              AGT037_2_bnd_likes SV29 SV39 SV45 = False) ∨
             AGT037_2_bnd_very_much_likes SV29 SV39 SV45 = True) ∨
            AGT037_2_bnd_a3 SV13 SV45 = False ==>
         ∀(SV29::AGT037_2_bnd_mu) (SV39::AGT037_2_bnd_mu) (SV13::TPTP_Interpret.ind)
            SV45::TPTP_Interpret.ind.
            ((((¬ AGT037_2_bnd_a1 SV45
                   (AGT037_2_bnd_sK5_SY68 SV13 SV39 SV29 SV45) ∨
                AGT037_2_bnd_likes SV29 SV39
                 (AGT037_2_bnd_sK5_SY68 SV13 SV39 SV29 SV45)) =
               False ∨
               (¬ (∀SY69::TPTP_Interpret.ind.
                      ¬ AGT037_2_bnd_a2 SV45 SY69 ∨
                      AGT037_2_bnd_likes SV29 SV39 SY69)) =
               True) ∨
              AGT037_2_bnd_likes SV29 SV39 SV45 = False) ∨
             AGT037_2_bnd_very_much_likes SV29 SV39 SV45 = True) ∨
            AGT037_2_bnd_a3 SV13 SV45 = False"
(*
apply (rule allI)+
apply (erule_tac x = "SV13" in allE)
apply (erule_tac x = "SV39" in allE)
apply (erule_tac x = "SV29" in allE)
apply (erule_tac x = "SV45" in allE)
apply (erule disjE)+
defer
apply (tactic {*clause_breaker 1*})+
apply (drule_tac sk = "bnd_sK5_SY68 SV13 SV39 SV29 SV45" in leo2_skolemise)
defer
apply (tactic {*clause_breaker 1*})
apply (tactic {*nonfull_extcnf_combined_tac []*})
*)
by (tactic ‹nonfull_extcnf_combined_tac @{context} [Existential_Var]›)

(*(*NUM667^1*)
lemma "∀SV12 SV13 SV14 SV9 SV10 SV11.
   ((((bnd_less SV12 SV13 = bnd_less SV11 SV10) = False ∨
      (SV14 = SV13) = False) ∨
     bnd_less SV12 SV14 = False) ∨
    bnd_less SV9 SV10 = True) ∨
   (SV9 = SV11) = False ==>
\<forall>SV9 SV14 SV10 SV11 SV13 SV12.
   ((((bnd_less SV12 SV13 = False ∨
       bnd_less SV11 SV10 = False) ∨
      (SV14 = SV13) = False) ∨
     bnd_less SV12 SV14 = False) ∨
    bnd_less SV9 SV10 = True) ∨
   (SV9 = SV11) = False"
(*
apply (tactic {*
  extcnf_combined_tac NONE
   [ConstsDiff,
    StripQuantifiers]
   []*})
*)
(*
apply (rule allI)+
apply (erule_tac x = "SV12" in allE)
apply (erule_tac x = "SV13" in allE)
apply (erule_tac x = "SV14" in allE)
apply (erule_tac x = "SV9" in allE)
apply (erule_tac x = "SV10" in allE)
apply (erule_tac x = "SV11" in allE)
*)
by (tactic {*rtac (leo2_tac @{context} (hd prob_names) "300") 1*})


(*NUM667^1 node 302 -- dec*)
lemma "∀SV12 SV13 SV14 SV9 SV10 SV11.
       ((((bnd_less SV12 SV13 = bnd_less SV11 SV10) = False ∨
          (SV14 = SV13) = False) ∨
         bnd_less SV12 SV14 = False) ∨
        bnd_less SV9 SV10 = True) ∨
       (SV9 = SV11) =
       False ==>
       ∀SV9 SV14 SV10 SV13 SV11 SV12.
       (((((SV12 = SV11) = False ∨ (SV13 = SV10) = False) ∨
          (SV14 = SV13) = False) ∨
         bnd_less SV12 SV14 = False) ∨
        bnd_less SV9 SV10 = True) ∨
       (SV9 = SV11) =
       False"
by (tactic {*rtac (leo2_tac @{context} (hd prob_names) "302") 1*})
*)


(*
(*CSR122^2*)
     (* (Annotated_step ("23", "extuni_bool2"), *)
lemma "(bnd_holdsDuring_THFTYPE_IiooI
           (bnd_lYearFn_THFTYPE_IiiI bnd_n2009_THFTYPE_i)
           (¬ (¬ bnd_likes_THFTYPE_IiioI bnd_lMary_THFTYPE_i
                  bnd_lBill_THFTYPE_i ∨
               ¬ bnd_likes_THFTYPE_IiioI bnd_lSue_THFTYPE_i
                  bnd_lBill_THFTYPE_i)) =
          bnd_likes_THFTYPE_IiioI bnd_lSue_THFTYPE_i
           bnd_lBill_THFTYPE_i) =
         False ==>
         bnd_holdsDuring_THFTYPE_IiooI
          (bnd_lYearFn_THFTYPE_IiiI bnd_n2009_THFTYPE_i)
          (¬ (¬ bnd_likes_THFTYPE_IiioI bnd_lMary_THFTYPE_i
                 bnd_lBill_THFTYPE_i ∨
              ¬ bnd_likes_THFTYPE_IiioI bnd_lSue_THFTYPE_i
                 bnd_lBill_THFTYPE_i)) =
         True ∨
         bnd_likes_THFTYPE_IiioI bnd_lSue_THFTYPE_i
          bnd_lBill_THFTYPE_i =
         True"
(* apply (erule extuni_bool2) *)
(* done *)
by (tactic {*rtac (leo2_tac @{context} (hd prob_names) "23") 1*})

     (* (Annotated_step ("24", "extuni_bool1"), *)
lemma "(bnd_holdsDuring_THFTYPE_IiooI
           (bnd_lYearFn_THFTYPE_IiiI bnd_n2009_THFTYPE_i)
           (¬ (¬ bnd_likes_THFTYPE_IiioI bnd_lMary_THFTYPE_i
                  bnd_lBill_THFTYPE_i ∨
               ¬ bnd_likes_THFTYPE_IiioI bnd_lSue_THFTYPE_i
                  bnd_lBill_THFTYPE_i)) =
          bnd_likes_THFTYPE_IiioI bnd_lMary_THFTYPE_i
           bnd_lBill_THFTYPE_i) =
         False ==>
         bnd_holdsDuring_THFTYPE_IiooI
          (bnd_lYearFn_THFTYPE_IiiI bnd_n2009_THFTYPE_i)
          (¬ (¬ bnd_likes_THFTYPE_IiioI bnd_lMary_THFTYPE_i
                 bnd_lBill_THFTYPE_i ∨
              ¬ bnd_likes_THFTYPE_IiioI bnd_lSue_THFTYPE_i
                 bnd_lBill_THFTYPE_i)) =
         False ∨
         bnd_likes_THFTYPE_IiioI bnd_lMary_THFTYPE_i
          bnd_lBill_THFTYPE_i =
         False"
(* apply (erule extuni_bool1) *)
(* done *)
by (tactic {*rtac (leo2_tac @{context} (hd prob_names) "24") 1*})

     (* (Annotated_step ("25", "extuni_bool2"), *)
lemma "(bnd_holdsDuring_THFTYPE_IiooI
           (bnd_lYearFn_THFTYPE_IiiI bnd_n2009_THFTYPE_i)
           (¬ (¬ bnd_likes_THFTYPE_IiioI bnd_lMary_THFTYPE_i
                  bnd_lBill_THFTYPE_i ∨
               ¬ bnd_likes_THFTYPE_IiioI bnd_lSue_THFTYPE_i
                  bnd_lBill_THFTYPE_i)) =
          bnd_likes_THFTYPE_IiioI bnd_lMary_THFTYPE_i
           bnd_lBill_THFTYPE_i) =
         False ==>
         bnd_holdsDuring_THFTYPE_IiooI
          (bnd_lYearFn_THFTYPE_IiiI bnd_n2009_THFTYPE_i)
          (¬ (¬ bnd_likes_THFTYPE_IiioI bnd_lMary_THFTYPE_i
                 bnd_lBill_THFTYPE_i ∨
              ¬ bnd_likes_THFTYPE_IiioI bnd_lSue_THFTYPE_i
                 bnd_lBill_THFTYPE_i)) =
         True ∨
         bnd_likes_THFTYPE_IiioI bnd_lMary_THFTYPE_i
          bnd_lBill_THFTYPE_i =
         True"
(* apply (erule extuni_bool2) *)
(* done *)
by (tactic {*rtac (leo2_tac @{context} (hd prob_names) "25") 1*})

     (* (Annotated_step ("26", "extuni_bool1"), *)
lemma "∀SV2. (bnd_holdsDuring_THFTYPE_IiooI
                 (bnd_lYearFn_THFTYPE_IiiI bnd_n2009_THFTYPE_i)
                 (¬ (¬ bnd_likes_THFTYPE_IiioI
                        bnd_lMary_THFTYPE_i
                        bnd_lBill_THFTYPE_i ∨
                     ¬ bnd_likes_THFTYPE_IiioI
                        bnd_lSue_THFTYPE_i
                        bnd_lBill_THFTYPE_i)) =
                bnd_holdsDuring_THFTYPE_IiooI SV2 True) =
               False ==>
         ∀SV2. bnd_holdsDuring_THFTYPE_IiooI
                (bnd_lYearFn_THFTYPE_IiiI bnd_n2009_THFTYPE_i)
                (¬ (¬ bnd_likes_THFTYPE_IiioI
                       bnd_lMary_THFTYPE_i bnd_lBill_THFTYPE_i ∨
                    ¬ bnd_likes_THFTYPE_IiioI bnd_lSue_THFTYPE_i
                       bnd_lBill_THFTYPE_i)) =
               False ∨
               bnd_holdsDuring_THFTYPE_IiooI SV2 True = False"
(* apply (rule allI, erule allE) *)
(* apply (erule extuni_bool1) *)
(* done *)
by (tactic {*rtac (leo2_tac @{context} (hd prob_names) "26") 1*})

     (* (Annotated_step ("27", "extuni_bool2"), *)
lemma "∀SV2. (bnd_holdsDuring_THFTYPE_IiooI
                 (bnd_lYearFn_THFTYPE_IiiI bnd_n2009_THFTYPE_i)
                 (¬ (¬ bnd_likes_THFTYPE_IiioI
                        bnd_lMary_THFTYPE_i
                        bnd_lBill_THFTYPE_i ∨
                     ¬ bnd_likes_THFTYPE_IiioI
                        bnd_lSue_THFTYPE_i
                        bnd_lBill_THFTYPE_i)) =
                bnd_holdsDuring_THFTYPE_IiooI SV2 True) =
               False ==>
         ∀SV2. bnd_holdsDuring_THFTYPE_IiooI
                (bnd_lYearFn_THFTYPE_IiiI bnd_n2009_THFTYPE_i)
                (¬ (¬ bnd_likes_THFTYPE_IiioI
                       bnd_lMary_THFTYPE_i bnd_lBill_THFTYPE_i ∨
                    ¬ bnd_likes_THFTYPE_IiioI bnd_lSue_THFTYPE_i
                       bnd_lBill_THFTYPE_i)) =
               True ∨
               bnd_holdsDuring_THFTYPE_IiooI SV2 True = True"
(* apply (rule allI, erule allE) *)
(* apply (erule extuni_bool2) *)
(* done *)
by (tactic {*rtac (leo2_tac @{context} (hd prob_names) "27") 1*})

     (* (Annotated_step ("30", "extuni_bool1"), *)
lemma "((¬ (¬ bnd_likes_THFTYPE_IiioI bnd_lMary_THFTYPE_i
                 bnd_lBill_THFTYPE_i ∨
              ¬ bnd_likes_THFTYPE_IiioI bnd_lSue_THFTYPE_i
                 bnd_lBill_THFTYPE_i)) =
          True) =
         False ==>
         (¬ (¬ bnd_likes_THFTYPE_IiioI bnd_lMary_THFTYPE_i
                bnd_lBill_THFTYPE_i ∨
             ¬ bnd_likes_THFTYPE_IiioI bnd_lSue_THFTYPE_i
                bnd_lBill_THFTYPE_i)) =
         False ∨
         True = False"
(* apply (erule extuni_bool1) *)
(* done *)
by (tactic {*rtac (leo2_tac @{context} (hd prob_names) "30") 1*})

     (* (Annotated_step ("29", "extuni_bind"), *)
lemma "(bnd_lYearFn_THFTYPE_IiiI bnd_n2009_THFTYPE_i =
          bnd_lYearFn_THFTYPE_IiiI bnd_n2009_THFTYPE_i) =
         False ∨
         ((¬ (¬ bnd_likes_THFTYPE_IiioI bnd_lMary_THFTYPE_i
                 bnd_lBill_THFTYPE_i ∨
              ¬ bnd_likes_THFTYPE_IiioI bnd_lSue_THFTYPE_i
                 bnd_lBill_THFTYPE_i)) =
          True) =
         False ==>
         ((¬ (¬ bnd_likes_THFTYPE_IiioI bnd_lMary_THFTYPE_i
                 bnd_lBill_THFTYPE_i ∨
              ¬ bnd_likes_THFTYPE_IiioI bnd_lSue_THFTYPE_i
                 bnd_lBill_THFTYPE_i)) =
          True) =
         False"
(* apply (tactic {*break_hypotheses 1*}) *)
(* apply (erule extuni_bind) *)
(* apply (tactic {*clause_breaker 1*}) *)
(* done *)
by (tactic {*rtac (leo2_tac @{context} (hd prob_names) "29") 1*})

     (* (Annotated_step ("28", "extuni_dec"), *)
lemma "∀SV2. (bnd_holdsDuring_THFTYPE_IiooI
                 (bnd_lYearFn_THFTYPE_IiiI bnd_n2009_THFTYPE_i)
                 (¬ (¬ bnd_likes_THFTYPE_IiioI
                        bnd_lMary_THFTYPE_i
                        bnd_lBill_THFTYPE_i ∨
                     ¬ bnd_likes_THFTYPE_IiioI
                        bnd_lSue_THFTYPE_i
                        bnd_lBill_THFTYPE_i)) =
                bnd_holdsDuring_THFTYPE_IiooI SV2 True) =
               False ==>
         ∀SV2. (bnd_lYearFn_THFTYPE_IiiI bnd_n2009_THFTYPE_i =
                SV2) =
               False ∨
               ((¬ (¬ bnd_likes_THFTYPE_IiioI
                       bnd_lMary_THFTYPE_i bnd_lBill_THFTYPE_i ∨
                    ¬ bnd_likes_THFTYPE_IiioI bnd_lSue_THFTYPE_i
                       bnd_lBill_THFTYPE_i)) =
                True) =
               False"
(* apply (rule allI) *)
(* apply (erule_tac x = "SV2" in allE) *)
(* apply (erule extuni_dec_2) *)
(* done *)
by (tactic {*rtac (leo2_tac @{context} (hd prob_names) "28") 1*})
*)

(* QUA002^1
   (* [[(Annotated_step ("49", "extuni_dec"), *)
lemma "((bnd_sK3_E = bnd_sK1_X1 ∨ bnd_sK3_E = bnd_sK2_X2) =
          (bnd_sK3_E = bnd_sK2_X2 ∨ bnd_sK3_E = bnd_sK1_X1)) =
         False ==>
         ((bnd_sK3_E = bnd_sK2_X2) = (bnd_sK3_E = bnd_sK2_X2)) =
         False ∨
         ((bnd_sK3_E = bnd_sK1_X1) = (bnd_sK3_E = bnd_sK1_X1)) =
         False"
by (tactic {*rtac (leo2_tac @{context} (hd prob_names) "49") 1*})

     (* (Annotated_step ("20", "unfold_def"), *)
lemma "(bnd_addition bnd_sK1_X1 bnd_sK2_X2 ≠
          bnd_addition bnd_sK2_X2 bnd_sK1_X1) =
         True ==>
         (bnd_sup
           (λSX0::TPTP_Interpret.ind.
               SX0 = bnd_sK1_X1 ∨ SX0 = bnd_sK2_X2) ≠
          bnd_sup
           (λSX0::TPTP_Interpret.ind.
               SX0 = bnd_sK2_X2 ∨ SX0 = bnd_sK1_X1)) =
         True"
by (tactic {*rtac (leo2_tac @{context} (hd prob_names) "20") 1*})
*)

(*
(*SEU620^2*)
     (* (Annotated_step ("11", "unfold_def"), *)
lemma "bnd_kpairiskpair =
         (∀Xx Xy.
             bnd_iskpair
              (bnd_setadjoin (bnd_setadjoin Xx bnd_emptyset)
                (bnd_setadjoin
                  (bnd_setadjoin Xx
                    (bnd_setadjoin Xy bnd_emptyset))
                  bnd_emptyset))) ∧
         bnd_kpair =
         (λXx Xy.
             bnd_setadjoin (bnd_setadjoin Xx bnd_emptyset)
              (bnd_setadjoin
                (bnd_setadjoin Xx
                  (bnd_setadjoin Xy bnd_emptyset))
                bnd_emptyset)) ∧
         bnd_iskpair =
         (λA. ∃Xx. bnd_in Xx (bnd_setunion A) ∧
                   (∃Xy. bnd_in Xy (bnd_setunion A) ∧
                         A =
                         bnd_setadjoin
                          (bnd_setadjoin Xx bnd_emptyset)
                          (bnd_setadjoin
                            (bnd_setadjoin Xx
                              (bnd_setadjoin Xy bnd_emptyset))
                            bnd_emptyset))) ∧
         (∀SY5 SY6.
             (bnd_setadjoin (bnd_setadjoin SY5 bnd_emptyset)
               (bnd_setadjoin
                 (bnd_setadjoin SY5
                   (bnd_setadjoin SY6 bnd_emptyset))
                 bnd_emptyset) =
              bnd_setadjoin
               (bnd_setadjoin (bnd_sK3 SY6 SY5) bnd_emptyset)
               (bnd_setadjoin
                 (bnd_setadjoin (bnd_sK3 SY6 SY5)
                   (bnd_setadjoin (bnd_sK4 SY6 SY5)
                     bnd_emptyset))
                 bnd_emptyset) ∧
              bnd_in (bnd_sK4 SY6 SY5)
               (bnd_setunion
                 (bnd_setadjoin (bnd_setadjoin SY5 bnd_emptyset)
                   (bnd_setadjoin
                     (bnd_setadjoin SY5
                       (bnd_setadjoin SY6 bnd_emptyset))
                     bnd_emptyset)))) ∧
             bnd_in (bnd_sK3 SY6 SY5)
              (bnd_setunion
                (bnd_setadjoin (bnd_setadjoin SY5 bnd_emptyset)
                  (bnd_setadjoin
                    (bnd_setadjoin SY5
                      (bnd_setadjoin SY6 bnd_emptyset))
                    bnd_emptyset)))) =
         True ==>
         (∀SX0 SX1.
             ¬ (¬ ¬ (bnd_setadjoin
                      (bnd_setadjoin SX0 bnd_emptyset)
                      (bnd_setadjoin
                        (bnd_setadjoin SX0
                          (bnd_setadjoin SX1 bnd_emptyset))
                        bnd_emptyset) ≠
                     bnd_setadjoin
                      (bnd_setadjoin (bnd_sK3 SX1 SX0)
                        bnd_emptyset)
                      (bnd_setadjoin
                        (bnd_setadjoin (bnd_sK3 SX1 SX0)
                          (bnd_setadjoin (bnd_sK4 SX1 SX0)
                            bnd_emptyset))
                        bnd_emptyset) ∨
                     ¬ bnd_in (bnd_sK4 SX1 SX0)
                        (bnd_setunion
                          (bnd_setadjoin
                            (bnd_setadjoin SX0 bnd_emptyset)
                            (bnd_setadjoin
                              (bnd_setadjoin SX0
(bnd_setadjoin SX1 bnd_emptyset))
                              bnd_emptyset)))) ∨
                ¬ bnd_in (bnd_sK3 SX1 SX0)
                   (bnd_setunion
                     (bnd_setadjoin
                       (bnd_setadjoin SX0 bnd_emptyset)
                       (bnd_setadjoin
                         (bnd_setadjoin SX0
                           (bnd_setadjoin SX1 bnd_emptyset))
                         bnd_emptyset))))) =
         True"
by (tactic {*rtac (leo2_tac @{context} (hd prob_names) "11") 1*})

     (* (Annotated_step ("3", "unfold_def"), *)
lemma "bnd_kpairiskpair =
         (∀Xx Xy.
             bnd_iskpair
              (bnd_setadjoin (bnd_setadjoin Xx bnd_emptyset)
                (bnd_setadjoin
                  (bnd_setadjoin Xx
                    (bnd_setadjoin Xy bnd_emptyset))
                  bnd_emptyset))) ∧
         bnd_kpair =
         (λXx Xy.
             bnd_setadjoin (bnd_setadjoin Xx bnd_emptyset)
              (bnd_setadjoin
                (bnd_setadjoin Xx
                  (bnd_setadjoin Xy bnd_emptyset))
                bnd_emptyset)) ∧
         bnd_iskpair =
         (λA. ∃Xx. bnd_in Xx (bnd_setunion A) ∧
                   (∃Xy. bnd_in Xy (bnd_setunion A) ∧
                         A =
                         bnd_setadjoin
                          (bnd_setadjoin Xx bnd_emptyset)
                          (bnd_setadjoin
                            (bnd_setadjoin Xx
                              (bnd_setadjoin Xy bnd_emptyset))
                            bnd_emptyset))) ∧
         (bnd_kpairiskpair ⟶
          (∀Xx Xy. bnd_iskpair (bnd_kpair Xx Xy))) =
         False ==>
         ((∀SY5 SY6.
              ∃SY7. bnd_in SY7
                     (bnd_setunion
                       (bnd_setadjoin
                         (bnd_setadjoin SY5 bnd_emptyset)
                         (bnd_setadjoin
                           (bnd_setadjoin SY5
                             (bnd_setadjoin SY6 bnd_emptyset))
                           bnd_emptyset))) ∧
                    (∃SY8. bnd_in SY8
                            (bnd_setunion
                              (bnd_setadjoin
(bnd_setadjoin SY5 bnd_emptyset)
(bnd_setadjoin
  (bnd_setadjoin SY5 (bnd_setadjoin SY6 bnd_emptyset))
  bnd_emptyset))) ∧
                           bnd_setadjoin
                            (bnd_setadjoin SY5 bnd_emptyset)
                            (bnd_setadjoin
                              (bnd_setadjoin SY5
(bnd_setadjoin SY6 bnd_emptyset))
                              bnd_emptyset) =
                           bnd_setadjoin
                            (bnd_setadjoin SY7 bnd_emptyset)
                            (bnd_setadjoin
                              (bnd_setadjoin SY7
(bnd_setadjoin SY8 bnd_emptyset))
                              bnd_emptyset))) ⟶
          (∀SY0 SY1.
              ∃SY3. bnd_in SY3
                     (bnd_setunion
                       (bnd_setadjoin
                         (bnd_setadjoin SY0 bnd_emptyset)
                         (bnd_setadjoin
                           (bnd_setadjoin SY0
                             (bnd_setadjoin SY1 bnd_emptyset))
                           bnd_emptyset))) ∧
                    (∃SY4. bnd_in SY4
                            (bnd_setunion
                              (bnd_setadjoin
(bnd_setadjoin SY0 bnd_emptyset)
(bnd_setadjoin
  (bnd_setadjoin SY0 (bnd_setadjoin SY1 bnd_emptyset))
  bnd_emptyset))) ∧
                           bnd_setadjoin
                            (bnd_setadjoin SY0 bnd_emptyset)
                            (bnd_setadjoin
                              (bnd_setadjoin SY0
(bnd_setadjoin SY1 bnd_emptyset))
                              bnd_emptyset) =
                           bnd_setadjoin
                            (bnd_setadjoin SY3 bnd_emptyset)
                            (bnd_setadjoin
                              (bnd_setadjoin SY3
(bnd_setadjoin SY4 bnd_emptyset))
                              bnd_emptyset)))) =
         False"
by (tactic {*rtac (leo2_tac @{context} (hd prob_names) "3") 1*})

     (* (Annotated_step ("8", "extcnf_combined"), *)
lemma "(∀SY5 SY6.
             ∃SY7. bnd_in SY7
                    (bnd_setunion
                      (bnd_setadjoin
                        (bnd_setadjoin SY5 bnd_emptyset)
                        (bnd_setadjoin
                          (bnd_setadjoin SY5
                            (bnd_setadjoin SY6 bnd_emptyset))
                          bnd_emptyset))) ∧
                   (∃SY8. bnd_in SY8
                           (bnd_setunion
                             (bnd_setadjoin
                               (bnd_setadjoin SY5 bnd_emptyset)
                               (bnd_setadjoin
 (bnd_setadjoin SY5 (bnd_setadjoin SY6 bnd_emptyset))
 bnd_emptyset))) ∧
                          bnd_setadjoin
                           (bnd_setadjoin SY5 bnd_emptyset)
                           (bnd_setadjoin
                             (bnd_setadjoin SY5
                               (bnd_setadjoin SY6 bnd_emptyset))
                             bnd_emptyset) =
                          bnd_setadjoin
                           (bnd_setadjoin SY7 bnd_emptyset)
                           (bnd_setadjoin
                             (bnd_setadjoin SY7
                               (bnd_setadjoin SY8 bnd_emptyset))
                             bnd_emptyset))) =
         True ==>
         (∀SY5 SY6.
             (bnd_setadjoin (bnd_setadjoin SY5 bnd_emptyset)
               (bnd_setadjoin
                 (bnd_setadjoin SY5
                   (bnd_setadjoin SY6 bnd_emptyset))
                 bnd_emptyset) =
              bnd_setadjoin
               (bnd_setadjoin (bnd_sK3 SY6 SY5) bnd_emptyset)
               (bnd_setadjoin
                 (bnd_setadjoin (bnd_sK3 SY6 SY5)
                   (bnd_setadjoin (bnd_sK4 SY6 SY5)
                     bnd_emptyset))
                 bnd_emptyset) \<and>
              bnd_in (bnd_sK4 SY6 SY5)
               (bnd_setunion
                 (bnd_setadjoin (bnd_setadjoin SY5 bnd_emptyset)
                   (bnd_setadjoin
                     (bnd_setadjoin SY5
                       (bnd_setadjoin SY6 bnd_emptyset))
                     bnd_emptyset)))) \<and>
             bnd_in (bnd_sK3 SY6 SY5)
              (bnd_setunion
                (bnd_setadjoin (bnd_setadjoin SY5 bnd_emptyset)
                  (bnd_setadjoin
                    (bnd_setadjoin SY5
                      (bnd_setadjoin SY6 bnd_emptyset))
                    bnd_emptyset)))) =
         True"
by (tactic {*
HEADGOAL (extcnf_combined_tac Full false (hd prob_names))
*})

     (* (Annotated_step ("7", "extcnf_combined"), *)
lemma "(\<not> (\<forall>SY0 SY1.
                \<exists>SY3. bnd_in SY3
                       (bnd_setunion
                         (bnd_setadjoin
                           (bnd_setadjoin SY0 bnd_emptyset)
                           (bnd_setadjoin
                             (bnd_setadjoin SY0
                               (bnd_setadjoin SY1 bnd_emptyset))
                             bnd_emptyset))) \<and>
                      (\<exists>SY4. bnd_in SY4
                              (bnd_setunion
(bnd_setadjoin (bnd_setadjoin SY0 bnd_emptyset)
  (bnd_setadjoin
    (bnd_setadjoin SY0 (bnd_setadjoin SY1 bnd_emptyset))
    bnd_emptyset))) \<and>
                             bnd_setadjoin
                              (bnd_setadjoin SY0 bnd_emptyset)
                              (bnd_setadjoin
(bnd_setadjoin SY0 (bnd_setadjoin SY1 bnd_emptyset))
bnd_emptyset) =
                             bnd_setadjoin
                              (bnd_setadjoin SY3 bnd_emptyset)
                              (bnd_setadjoin
(bnd_setadjoin SY3 (bnd_setadjoin SY4 bnd_emptyset))
bnd_emptyset)))) =
         True \<Longrightarrow>
         (\<forall>SY24.
             (\<forall>SY25.
                 bnd_setadjoin
                  (bnd_setadjoin bnd_sK1 bnd_emptyset)
                  (bnd_setadjoin
                    (bnd_setadjoin bnd_sK1
                      (bnd_setadjoin bnd_sK2 bnd_emptyset))
                    bnd_emptyset) \<noteq>
                 bnd_setadjoin (bnd_setadjoin SY24 bnd_emptyset)
                  (bnd_setadjoin
                    (bnd_setadjoin SY24
                      (bnd_setadjoin SY25 bnd_emptyset))
                    bnd_emptyset) \<or>
                 \<not> bnd_in SY25
                    (bnd_setunion
                      (bnd_setadjoin
                        (bnd_setadjoin bnd_sK1 bnd_emptyset)
                        (bnd_setadjoin
                          (bnd_setadjoin bnd_sK1
                            (bnd_setadjoin bnd_sK2
                              bnd_emptyset))
                          bnd_emptyset)))) \<or>
             \<not> bnd_in SY24
                (bnd_setunion
                  (bnd_setadjoin
                    (bnd_setadjoin bnd_sK1 bnd_emptyset)
                    (bnd_setadjoin
                      (bnd_setadjoin bnd_sK1
                        (bnd_setadjoin bnd_sK2 bnd_emptyset))
                      bnd_emptyset)))) =
         True"
by (tactic {*HEADGOAL (extcnf_combined_tac Full false (hd prob_names))*})
*)

(*PUZ081^2*)
(*
     (* (Annotated_step ("9", "unfold_def"), *)
lemma "bnd_says bnd_mel
          (\<not> bnd_knave bnd_zoey \<and> \<not> bnd_knave bnd_mel) \<Longrightarrow>
         bnd_says bnd_mel
          (\<not> bnd_knave bnd_zoey \<and> \<not> bnd_knave bnd_mel) =
         True"
by (tactic {*rtac (leo2_tac @{context} (hd prob_names) "9") 1*})

     (* (Annotated_step ("10", "unfold_def"), *)
lemma "bnd_says bnd_zoey (bnd_knave bnd_mel) \<Longrightarrow>
         bnd_says bnd_zoey (bnd_knave bnd_mel) = True"
by (tactic {*rtac (leo2_tac @{context} (hd prob_names) "10") 1*})

     (* (Annotated_step ("11", "unfold_def"), *)
lemma "\<forall>P S. bnd_knave P \<and> bnd_says P S \<longrightarrow> \<not> S \<Longrightarrow>
         (\<forall>P S. bnd_knave P \<and> bnd_says P S \<longrightarrow> \<not> S) = True"
by (tactic {*rtac (leo2_tac @{context} (hd prob_names) "11") 1*})

     (* (Annotated_step ("12", "unfold_def"), *)
lemma "\<forall>P S. bnd_knight P \<and> bnd_says P S \<longrightarrow> S \<Longrightarrow>
         (\<forall>P S. bnd_knight P \<and> bnd_says P S \<longrightarrow> S) = True"
by (tactic {*rtac (leo2_tac @{context} (hd prob_names) "12") 1*})

     (* (Annotated_step ("13", "unfold_def"), *)
lemma "\<forall>P. bnd_knight P \<noteq> bnd_knave P \<Longrightarrow>
         (\<forall>P. bnd_knight P \<noteq> bnd_knave P) = True"
by (tactic {*rtac (leo2_tac @{context} (hd prob_names) "13") 1*})

     (* (Annotated_step ("15", "extcnf_combined"), *)
lemma "(\<not> (\<exists>TZ TM. TZ bnd_zoey \<and> TM bnd_mel)) = True \<Longrightarrow>
         ((\<forall>TM. \<not> TM bnd_mel) \<or> (\<forall>TZ. \<not> TZ bnd_zoey)) = True"
by (tactic {*extcnf_combined_tac Full false (hd prob_names) 1*})

     (* (Annotated_step ("18", "extcnf_combined"), *)
lemma "(\<forall>P. bnd_knight P \<noteq> bnd_knave P) = True \<Longrightarrow>
         ((\<forall>P. \<not> bnd_knave P \<or> \<not> bnd_knight P) \<and>
          (\<forall>P. bnd_knave P \<or> bnd_knight P)) =
         True"
by (tactic {*extcnf_combined_tac Full false (hd prob_names) 1*})
*)

(*
(*from SEU667^2.p.out*)
     (* (Annotated_step ("10", "unfold_def"), *)
lemma "bnd_dpsetconstrSub =
         (\<forall>A B Xphi.
             bnd_subset (bnd_dpsetconstr A B Xphi)
              (bnd_cartprod A B)) \<and>
         bnd_dpsetconstr =
         (\<lambda>A B Xphi.
             bnd_dsetconstr (bnd_cartprod A B)
              (\<lambda>Xu. \<exists>Xx. bnd_in Xx A \<and>
                         (\<exists>Xy. (bnd_in Xy B \<and> Xphi Xx Xy) \<and>
                               Xu = bnd_kpair Xx Xy))) \<and>
         bnd_breln = (\<lambda>A B C. bnd_subset C (bnd_cartprod A B)) \<and>
         (\<not> bnd_subset
             (bnd_dsetconstr (bnd_cartprod bnd_sK1 bnd_sK2)
               (\<lambda>SY66.
                   \<exists>SY67.
                      bnd_in SY67 bnd_sK1 \<and>
                      (\<exists>SY68.
                          (bnd_in SY68 bnd_sK2 \<and>
                           bnd_sK3 SY67 SY68) \<and>
                          SY66 = bnd_kpair SY67 SY68)))
             (bnd_cartprod bnd_sK1 bnd_sK2)) =
         True \<Longrightarrow>
         (\<not> bnd_subset
             (bnd_dsetconstr (bnd_cartprod bnd_sK1 bnd_sK2)
               (\<lambda>SX0. \<not> (\<forall>SX1. \<not> \<not> (\<not> bnd_in SX1 bnd_sK1 \<or>
    \<not> \<not> (\<forall>SX2. \<not> \<not> (\<not> \<not> (\<not> bnd_in SX2 bnd_sK2 \<or>
                         \<not> bnd_sK3 SX1 SX2) \<or>
                    SX0 \<noteq> bnd_kpair SX1 SX2))))))
             (bnd_cartprod bnd_sK1 bnd_sK2)) =
         True"
by (tactic {*rtac (leo2_tac @{context} (hd prob_names) "10") 1*})


     (* (Annotated_step ("11", "unfold_def"), *)
lemma "bnd_dpsetconstrSub =
         (\<forall>A B Xphi.
             bnd_subset (bnd_dpsetconstr A B Xphi)
              (bnd_cartprod A B)) \<and>
         bnd_dpsetconstr =
         (\<lambda>A B Xphi.
             bnd_dsetconstr (bnd_cartprod A B)
              (\<lambda>Xu. \<exists>Xx. bnd_in Xx A \<and>
                         (\<exists>Xy. (bnd_in Xy B \<and> Xphi Xx Xy) \<and>
                               Xu = bnd_kpair Xx Xy))) \<and>
         bnd_breln = (\<lambda>A B C. bnd_subset C (bnd_cartprod A B)) \<and>
         (\<forall>SY21 SY22 SY23.
             bnd_subset
              (bnd_dsetconstr (bnd_cartprod SY21 SY22)
                (\<lambda>SY35.
                    \<exists>SY36.
                       bnd_in SY36 SY21 \<and>
                       (\<exists>SY37.
                           (bnd_in SY37 SY22 \<and> SY23 SY36 SY37) \<and>
                           SY35 = bnd_kpair SY36 SY37)))
              (bnd_cartprod SY21 SY22)) =
         True \<Longrightarrow>
         (\<forall>SX0 SX1 SX2.
             bnd_subset
              (bnd_dsetconstr (bnd_cartprod SX0 SX1)
                (\<lambda>SX3. \<not> (\<forall>SX4. \<not> \<not> (\<not> bnd_in SX4 SX0 \<or>
     \<not> \<not> (\<forall>SX5. \<not> \<not> (\<not> \<not> (\<not> bnd_in SX5 SX1 \<or> \<not> SX2 SX4 SX5) \<or>
                     SX3 \<noteq> bnd_kpair SX4 SX5))))))
              (bnd_cartprod SX0 SX1)) =
         True"
by (tactic {*rtac (leo2_tac @{context} (hd prob_names) "11") 1*})
*)

(*
(*from ALG001^5*)
      (* (Annotated_step ("4", "extcnf_forall_neg"), *)
lemma "(\<forall>(Xh1 :: bnd_g \<Rightarrow> bnd_b) (Xh2 :: bnd_b \<Rightarrow> bnd_a) (Xf1 :: bnd_g \<Rightarrow> bnd_g \<Rightarrow> bnd_g) (Xf2 :: bnd_b \<Rightarrow> bnd_b \<Rightarrow> bnd_b) (Xf3 :: bnd_a \<Rightarrow> bnd_a \<Rightarrow> bnd_a).
             (\<forall>Xx Xy. Xh1 (Xf1 Xx Xy) = Xf2 (Xh1 Xx) (Xh1 Xy)) \<and>
             (\<forall>Xx Xy.
                 Xh2 (Xf2 Xx Xy) = Xf3 (Xh2 Xx) (Xh2 Xy)) \<longrightarrow>
             (\<forall>Xx Xy.
                 Xh2 (Xh1 (Xf1 Xx Xy)) =
                 Xf3 (Xh2 (Xh1 Xx)) (Xh2 (Xh1 Xy)))) =
         False \<Longrightarrow>
         ((\<forall>SY35 SY36.
              bnd_sK1 (bnd_sK3 SY35 SY36) =
              bnd_sK4 (bnd_sK1 SY35) (bnd_sK1 SY36)) \<and>
          (\<forall>SY31 SY32.
              bnd_sK2 (bnd_sK4 SY31 SY32) =
              bnd_sK5 (bnd_sK2 SY31) (bnd_sK2 SY32)) \<longrightarrow>
          (\<forall>SY39 SY40.
              bnd_sK2 (bnd_sK1 (bnd_sK3 SY39 SY40)) =
              bnd_sK5 (bnd_sK2 (bnd_sK1 SY39))
               (bnd_sK2 (bnd_sK1 SY40)))) =
         False"
by (tactic {*rtac (leo2_tac @{context} (hd prob_names) "4") 1*})
*)

(*SYN044^4*)
(*
declare [[ML_print_depth = 1400]]
(* the_tactics *)
*}

     (* (Annotated_step ("12", "unfold_def"), *)
lemma "bnd_mor =
         (\<lambda>(X::TPTP_Interpret.ind \<Rightarrow> bool)
             (Y::TPTP_Interpret.ind \<Rightarrow> bool) U::TPTP_Interpret.ind.
             X U \<or> Y U) \<and>
         bnd_mnot =
         (\<lambda>(X::TPTP_Interpret.ind \<Rightarrow> bool) U::TPTP_Interpret.ind.
             \<not> X U) \<and>
         bnd_mimplies =
         (\<lambda>U::TPTP_Interpret.ind \<Rightarrow> bool. bnd_mor (bnd_mnot U)) \<and>
         bnd_mbox_s4 =
         (\<lambda>(P::TPTP_Interpret.ind \<Rightarrow> bool) X::TPTP_Interpret.ind.
             \<forall>Y::TPTP_Interpret.ind. bnd_irel X Y \<longrightarrow> P Y) \<and>
         bnd_mand =
         (\<lambda>(X::TPTP_Interpret.ind \<Rightarrow> bool)
             (Y::TPTP_Interpret.ind \<Rightarrow> bool) U::TPTP_Interpret.ind.
             X U \<and> Y U) \<and>
         bnd_ixor =
         (\<lambda>(P::TPTP_Interpret.ind \<Rightarrow> bool)
             Q::TPTP_Interpret.ind \<Rightarrow> bool.
             bnd_inot (bnd_iequiv P Q)) \<and>
         bnd_ivalid = All \<and>
         bnd_itrue = (\<lambda>W::TPTP_Interpret.ind. True) \<and>
         bnd_isatisfiable = Ex \<and>
         bnd_ior =
         (\<lambda>(P::TPTP_Interpret.ind \<Rightarrow> bool)
             Q::TPTP_Interpret.ind \<Rightarrow> bool.
             bnd_mor (bnd_mbox_s4 P) (bnd_mbox_s4 Q)) \<and>
         bnd_inot =
         (\<lambda>P::TPTP_Interpret.ind \<Rightarrow> bool.
             bnd_mnot (bnd_mbox_s4 P)) \<and>
         bnd_iinvalid =
         (\<lambda>Phi::TPTP_Interpret.ind \<Rightarrow> bool.
             \<forall>W::TPTP_Interpret.ind. \<not> Phi W) \<and>
         bnd_iimplies =
         (\<lambda>(P::TPTP_Interpret.ind \<Rightarrow> bool)
             Q::TPTP_Interpret.ind \<Rightarrow> bool.
             bnd_mimplies (bnd_mbox_s4 P) (bnd_mbox_s4 Q)) \<and>
         bnd_iimplied =
         (\<lambda>(P::TPTP_Interpret.ind \<Rightarrow> bool)
             Q::TPTP_Interpret.ind \<Rightarrow> bool. bnd_iimplies Q P) \<and>
         bnd_ifalse = bnd_inot bnd_itrue \<and>
         bnd_iequiv =
         (\<lambda>(P::TPTP_Interpret.ind \<Rightarrow> bool)
             Q::TPTP_Interpret.ind \<Rightarrow> bool.
             bnd_iand (bnd_iimplies P Q) (bnd_iimplies Q P)) \<and>
         bnd_icountersatisfiable =
         (\<lambda>Phi::TPTP_Interpret.ind \<Rightarrow> bool.
             \<exists>W::TPTP_Interpret.ind. \<not> Phi W) \<and>
         bnd_iatom = (\<lambda>P::TPTP_Interpret.ind \<Rightarrow> bool. P) \<and>
         bnd_iand = bnd_mand \<and>
         (\<forall>(X::TPTP_Interpret.ind) (Y::TPTP_Interpret.ind)
             Z::TPTP_Interpret.ind.
             bnd_irel X Y \<and> bnd_irel Y Z \<longrightarrow> bnd_irel X Z) \<Longrightarrow>
         (\<forall>(X::TPTP_Interpret.ind) (Y::TPTP_Interpret.ind)
             Z::TPTP_Interpret.ind.
             bnd_irel X Y \<and> bnd_irel Y Z \<longrightarrow> bnd_irel X Z) =
         True"
(* by (tactic {*tectoc @{context}*}) *)
by (tactic {*rtac (leo2_tac @{context} (hd prob_names) "12") 1*})

     (* (Annotated_step ("11", "unfold_def"), *)
lemma "bnd_mor =
         (\<lambda>(X::TPTP_Interpret.ind \<Rightarrow> bool)
             (Y::TPTP_Interpret.ind \<Rightarrow> bool) U::TPTP_Interpret.ind.
             X U \<or> Y U) \<and>
         bnd_mnot =
         (\<lambda>(X::TPTP_Interpret.ind \<Rightarrow> bool) U::TPTP_Interpret.ind.
             \<not> X U) \<and>
         bnd_mimplies =
         (\<lambda>U::TPTP_Interpret.ind \<Rightarrow> bool. bnd_mor (bnd_mnot U)) \<and>
         bnd_mbox_s4 =
         (\<lambda>(P::TPTP_Interpret.ind \<Rightarrow> bool) X::TPTP_Interpret.ind.
             \<forall>Y::TPTP_Interpret.ind. bnd_irel X Y \<longrightarrow> P Y) \<and>
         bnd_mand =
         (\<lambda>(X::TPTP_Interpret.ind \<Rightarrow> bool)
             (Y::TPTP_Interpret.ind \<Rightarrow> bool) U::TPTP_Interpret.ind.
             X U \<and> Y U) \<and>
         bnd_ixor =
         (\<lambda>(P::TPTP_Interpret.ind \<Rightarrow> bool)
             Q::TPTP_Interpret.ind \<Rightarrow> bool.
             bnd_inot (bnd_iequiv P Q)) \<and>
         bnd_ivalid = All \<and>
         bnd_itrue = (\<lambda>W::TPTP_Interpret.ind. True) \<and>
         bnd_isatisfiable = Ex \<and>
         bnd_ior =
         (\<lambda>(P::TPTP_Interpret.ind \<Rightarrow> bool)
             Q::TPTP_Interpret.ind \<Rightarrow> bool.
             bnd_mor (bnd_mbox_s4 P) (bnd_mbox_s4 Q)) \<and>
         bnd_inot =
         (\<lambda>P::TPTP_Interpret.ind \<Rightarrow> bool.
             bnd_mnot (bnd_mbox_s4 P)) \<and>
         bnd_iinvalid =
         (\<lambda>Phi::TPTP_Interpret.ind \<Rightarrow> bool.
             \<forall>W::TPTP_Interpret.ind. \<not> Phi W) \<and>
         bnd_iimplies =
         (\<lambda>(P::TPTP_Interpret.ind \<Rightarrow> bool)
             Q::TPTP_Interpret.ind \<Rightarrow> bool.
             bnd_mimplies (bnd_mbox_s4 P) (bnd_mbox_s4 Q)) \<and>
         bnd_iimplied =
         (\<lambda>(P::TPTP_Interpret.ind \<Rightarrow> bool)
             Q::TPTP_Interpret.ind \<Rightarrow> bool. bnd_iimplies Q P) \<and>
         bnd_ifalse = bnd_inot bnd_itrue \<and>
         bnd_iequiv =
         (\<lambda>(P::TPTP_Interpret.ind \<Rightarrow> bool)
             Q::TPTP_Interpret.ind \<Rightarrow> bool.
             bnd_iand (bnd_iimplies P Q) (bnd_iimplies Q P)) \<and>
         bnd_icountersatisfiable =
         (\<lambda>Phi::TPTP_Interpret.ind \<Rightarrow> bool.
             \<exists>W::TPTP_Interpret.ind. \<not> Phi W) \<and>
         bnd_iatom = (\<lambda>P::TPTP_Interpret.ind \<Rightarrow> bool. P) \<and>
         bnd_iand = bnd_mand \<and>
         bnd_ivalid
          (bnd_iimplies (bnd_iatom bnd_q) (bnd_iatom bnd_r)) \<Longrightarrow>
         (\<forall>SY161::TPTP_Interpret.ind.
             \<not> (\<forall>SY162::TPTP_Interpret.ind.
                   bnd_irel SY161 SY162 \<longrightarrow> bnd_q SY162) \<or>
             (\<forall>SY163::TPTP_Interpret.ind.
                 bnd_irel SY161 SY163 \<longrightarrow> bnd_r SY163)) =
         True"
(* by (tactic {*tectoc @{context}*}) *)
by (tactic {*rtac (leo2_tac @{context} (hd prob_names) "11") 1*})

lemma "
(\<forall>SY136.
    \<not> (\<forall>SY137. bnd_irel SY136 SY137 \<longrightarrow> bnd_r SY137) \<or>
    (\<forall>SY138.
        bnd_irel SY136 SY138 \<longrightarrow> bnd_p SY138 \<and> bnd_q SY138)) =
True \<Longrightarrow>
(\<forall>SY136.
    bnd_irel SY136 (bnd_sK5 SY136) \<and> \<not> bnd_r (bnd_sK5 SY136) \<or>
    (\<forall>SY138. \<not> bnd_irel SY136 SY138 \<or> bnd_p SY138) \<and>
    (\<forall>SY138. \<not> bnd_irel SY136 SY138 \<or> bnd_q SY138)) =
True"
by (tactic {*HEADGOAL (extcnf_combined_tac Full false (hd prob_names))*})
*)

     (* (Annotated_step ("11", "extcnf_forall_neg"), *)
lemma "\<forall>SV1::TPTP_Interpret.ind \<Rightarrow> bool.
            (\<forall>SY2::TPTP_Interpret.ind.
                \<not> (\<not> (\<not> SV1 SY2 \<or> SEV405_5_bnd_cA) \<or>
                   \<not> (\<not> SEV405_5_bnd_cA \<or> SV1 SY2))) =
            False \<Longrightarrow>
         \<forall>SV1::TPTP_Interpret.ind \<Rightarrow> bool.
            (\<not> (\<not> (\<not> SV1 (SEV405_5_bnd_sK1_SY2 SV1) \<or> SEV405_5_bnd_cA) \<or>
                \<not> (\<not> SEV405_5_bnd_cA \<or> SV1 (SEV405_5_bnd_sK1_SY2 SV1)))) =
            False"
(* apply (tactic {*full_extcnf_combined_tac*}) *)
by (tactic \<open>nonfull_extcnf_combined_tac @{context} [Existential_Var]\<close>)

     (* (Annotated_step ("13", "extcnf_forall_pos"), *)
lemma "(\<forall>SY31 SY32.
             bnd_sK2 (bnd_sK4 SY31 SY32) =
             bnd_sK5 (bnd_sK2 SY31) (bnd_sK2 SY32)) =
         True \<Longrightarrow>
         \<forall>SV1. (\<forall>SY42.
                   bnd_sK2 (bnd_sK4 SV1 SY42) =
                   bnd_sK5 (bnd_sK2 SV1) (bnd_sK2 SY42)) =
               True"
by (tactic \<open>nonfull_extcnf_combined_tac @{context} [Universal]\<close>)

     (* (Annotated_step ("14", "extcnf_forall_pos"), *)
lemma "(\<forall>SY35 SY36.
             bnd_sK1 (bnd_sK3 SY35 SY36) =
             bnd_sK4 (bnd_sK1 SY35) (bnd_sK1 SY36)) =
         True \<Longrightarrow>
         \<forall>SV2. (\<forall>SY43.
                   bnd_sK1 (bnd_sK3 SV2 SY43) =
                   bnd_sK4 (bnd_sK1 SV2) (bnd_sK1 SY43)) =
               True"
by (tactic \<open>nonfull_extcnf_combined_tac @{context} [Universal]\<close>)


(*from SYO198^5.p.out*)
   (* [[(Annotated_step ("11", "extcnf_forall_special_pos"), *)
lemma "(\<forall>SX0::bool \<Rightarrow> bool.
             \<not> \<not> (\<not> SX0 bnd_sK1_Xx \<or> \<not> SX0 bnd_sK2_Xy)) =
         True \<Longrightarrow>
         (\<not> \<not> (\<not> True \<or> \<not> True)) = True"
apply (tactic \<open>extcnf_forall_special_pos_tac 1\<close>)
done

     (* (Annotated_step ("13", "extcnf_forall_special_pos"), *)
lemma "(\<forall>SX0::bool \<Rightarrow> bool.
             \<not> \<not> (\<not> SX0 bnd_sK1_Xx \<or> \<not> SX0 bnd_sK2_Xy)) =
         True \<Longrightarrow>
         (\<not> \<not> (\<not> bnd_sK1_Xx \<or> \<not> bnd_sK2_Xy)) = True"
apply (tactic \<open>extcnf_forall_special_pos_tac 1\<close>)
done

   (* [[(Annotated_step ("8", "polarity_switch"), *)
lemma "(\<forall>(Xx::bool) (Xy::bool) Xz::bool. True \<and> True \<longrightarrow> True) =
         False \<Longrightarrow>
         (\<not> (\<forall>(Xx::bool) (Xy::bool) Xz::bool.
                True \<and> True \<longrightarrow> True)) =
         True"
apply (tactic \<open>nonfull_extcnf_combined_tac @{context} [Polarity_switch]\<close>)
done

lemma "((\<forall>SY22 SY23 SY24.
       bnd_sK1_RRR SY22 SY23 \<and> bnd_sK1_RRR SY23 SY24 \<longrightarrow>
       bnd_sK1_RRR SY22 SY24) \<and>
   (\<forall>SY25.
       (\<forall>SY26. SY25 SY26 \<longrightarrow> bnd_sK1_RRR SY26 (bnd_sK2_U SY25)) \<and>
       (\<forall>SY27.
           (\<forall>SY28. SY25 SY28 \<longrightarrow> bnd_sK1_RRR SY28 SY27) \<longrightarrow>
           bnd_sK1_RRR (bnd_sK2_U SY25) SY27)) \<longrightarrow>
   (\<forall>SY29. \<exists>SY30. \<forall>SY31. SY29 SY31 \<longrightarrow> bnd_sK1_RRR SY31 SY30)) =
  False \<Longrightarrow>
  (\<forall>SY25.
      (\<forall>SY26. SY25 SY26 \<longrightarrow> bnd_sK1_RRR SY26 (bnd_sK2_U SY25)) \<and>
      (\<forall>SY27.
          (\<forall>SY28. SY25 SY28 \<longrightarrow> bnd_sK1_RRR SY28 SY27) \<longrightarrow>
          bnd_sK1_RRR (bnd_sK2_U SY25) SY27)) =
  True"
apply (tactic \<open>standard_cnf_tac @{context} 1\<close>)
done

lemma "((\<forall>Xx. bnd_in Xx bnd_emptyset \<longrightarrow> (\<forall>Xphi. Xphi)) \<longrightarrow>
   (\<forall>Xx Xy. bnd_in Xx (bnd_setadjoin Xx Xy)) \<longrightarrow>
   (\<forall>A B. A = B \<longrightarrow>
          (\<forall>Xx Xy. Xx = Xy \<longrightarrow> bnd_in Xx A = bnd_in Xy B)) \<longrightarrow>
   (\<forall>SY0. bnd_in SY0 bnd_omega \<longrightarrow>
          bnd_setadjoin SY0 SY0 \<noteq> bnd_emptyset)) =
  False \<Longrightarrow>
 (\<forall>Xx. bnd_in Xx bnd_emptyset \<longrightarrow> (\<forall>Xphi. Xphi)) =
  True"
apply (tactic \<open>standard_cnf_tac @{context} 1\<close>)
done

lemma "((\<forall>Xx. bnd_in Xx bnd_emptyset \<longrightarrow> (\<forall>Xphi. Xphi)) \<longrightarrow>
   (\<forall>Xx Xy. bnd_in Xx (bnd_setadjoin Xx Xy)) \<longrightarrow>
   (\<forall>A B. A = B \<longrightarrow>
          (\<forall>Xx Xy. Xx = Xy \<longrightarrow> bnd_in Xx A = bnd_in Xy B)) \<longrightarrow>
   (\<forall>SY0. bnd_in SY0 bnd_omega \<longrightarrow>
          bnd_setadjoin SY0 SY0 \<noteq> bnd_emptyset)) =
  False \<Longrightarrow>
  (\<forall>Xx Xy. bnd_in Xx (bnd_setadjoin Xx Xy)) =
  True"
apply (tactic \<open>standard_cnf_tac @{context} 1\<close>)
done

lemma "((\<forall>Xx. bnd_in Xx bnd_emptyset \<longrightarrow> (\<forall>Xphi. Xphi)) \<longrightarrow>
   (\<forall>Xx Xy. bnd_in Xx (bnd_setadjoin Xx Xy)) \<longrightarrow>
   (\<forall>A B. A = B \<longrightarrow>
          (\<forall>Xx Xy. Xx = Xy \<longrightarrow> bnd_in Xx A = bnd_in Xy B)) \<longrightarrow>
   (\<forall>SY0. bnd_in SY0 bnd_omega \<longrightarrow>
          bnd_setadjoin SY0 SY0 \<noteq> bnd_emptyset)) =
  False \<Longrightarrow>
  (\<forall>A B. A = B \<longrightarrow>
         (\<forall>Xx Xy. Xx = Xy \<longrightarrow> bnd_in Xx A = bnd_in Xy B)) =
  True"
apply (tactic \<open>standard_cnf_tac @{context} 1\<close>)
done

lemma "((\<forall>Xx. bnd_in Xx bnd_emptyset \<longrightarrow> (\<forall>Xphi. Xphi)) \<longrightarrow>
   (\<forall>Xx Xy. bnd_in Xx (bnd_setadjoin Xx Xy)) \<longrightarrow>
   (\<forall>A B. A = B \<longrightarrow>
          (\<forall>Xx Xy. Xx = Xy \<longrightarrow> bnd_in Xx A = bnd_in Xy B)) \<longrightarrow>
   (\<forall>SY0. bnd_in SY0 bnd_omega \<longrightarrow>
          bnd_setadjoin SY0 SY0 \<noteq> bnd_emptyset)) =
  False \<Longrightarrow>
  (\<forall>SY0. bnd_in SY0 bnd_omega \<longrightarrow>
         bnd_setadjoin SY0 SY0 \<noteq> bnd_emptyset) =
  False"
apply (tactic \<open>standard_cnf_tac @{context} 1\<close>)
done

(*nested conjunctions*)
lemma "((((\<forall>Xx. bnd_cP bnd_e Xx = Xx) \<and>
     (\<forall>Xy. bnd_cP Xy bnd_e = Xy)) \<and>
    (\<forall>Xz. bnd_cP Xz Xz = bnd_e)) \<and>
   (\<forall>Xx Xy Xz.
       bnd_cP (bnd_cP Xx Xy) Xz = bnd_cP Xx (bnd_cP Xy Xz)) \<longrightarrow>
   (\<forall>Xa Xb. bnd_cP Xa Xb = bnd_cP Xb Xa)) =
  False \<Longrightarrow>
  (\<forall>Xx. bnd_cP bnd_e Xx = Xx) =
  True"
apply (tactic \<open>standard_cnf_tac @{context} 1\<close>)
done

end