matita/tests/TPTP/Veloci/COL058-2.p.ma

   1
   2 include "logic/equality.ma".
   3 (* Inclusion of: COL058-2.p *)
   4 (* -------------------------------------------------------------------------- *)
   5 (*  File     : COL058-2 : TPTP v3.1.1. Released v1.0.0. *)
   6 (*  Domain   : Combinatory Logic *)
   7 (*  Problem  : If there's a lark, then there's an egocentric bird. *)
   8 (*  Version  : Especial. *)
   9 (*             Theorem formulation : The egocentric bird is provided and  *)
  10 (*             checked. *)
  11 (*  English  : Suppose we are given a forest that contains a lark, and  *)
  12 (*             we are not given any other information. Prove that at least  *)
  13 (*             one bird in the forest must be egocentric. *)
  14 (*  Refs     : [Smu85] Smullyan (1978), To Mock a Mocking Bird and Other Logi *)
  15 (*           : [GO86]  Glickfield & Overbeek (1986), A Foray into Combinatory *)
  16 (*  Source   : [GO86] *)
  17 (*  Names    : - [GO86] *)
  18 (*  Status   : Unsatisfiable *)
  19 (*  Rating   : 0.00 v2.2.1, 0.11 v2.2.0, 0.14 v2.1.0, 0.00 v2.0.0 *)
  20 (*  Syntax   : Number of clauses     :    2 (   0 non-Horn;   2 unit;   1 RR) *)
  21 (*             Number of atoms       :    2 (   2 equality) *)
  22 (*             Maximal clause size   :    1 (   1 average) *)
  23 (*             Number of predicates  :    1 (   0 propositional; 2-2 arity) *)
  24 (*             Number of functors    :    2 (   1 constant; 0-2 arity) *)
  25 (*             Number of variables   :    2 (   0 singleton) *)
  26 (*             Maximal term depth    :    7 (   5 average) *)
  27 (*  Comments :  *)
  28 (* -------------------------------------------------------------------------- *)
  29 (* ---- There exists a lark  *)
  30 (* ---- Hypothesis: This bird is egocentric  *)
  31 theorem prove_the_bird_exists:
  32  \forall Univ:Set.
  33 \forall lark:Univ.
  34 \forall response:\forall _:Univ.\forall _:Univ.Univ.
  35 \forall H0:\forall X1:Univ.\forall X2:Univ.eq Univ (response (response lark X1) X2) (response X1 (response X2 X2)).eq Univ (response (response (response lark (response (response lark (response lark lark)) (response lark (response lark lark)))) (response lark (response lark lark))) (response (response lark (response (response lark (response lark lark)) (response lark (response lark lark)))) (response lark (response lark lark)))) (response (response lark (response (response lark (response lark lark)) (response lark (response lark lark)))) (response lark (response lark lark)))
  36 .
  37 intros.
  38 autobatch paramodulation timeout=100;
  39 try assumption.
  40 print proofterm.
  41 qed.
  42 (* -------------------------------------------------------------------------- *)