\documentclass{amsart}
    \advance\textheight by 1.75in
    \advance\textwidth by 2in
    \advance\topmargin by -1in
    \advance\oddsidemargin by -1in
    \advance\evensidemargin by -1in
    \usepackage{amssymb}
    \parindent0pt
    \begin{document}
    \textbf{MSC013+1.p} Single-valued relation between 5-tuple and domain element

The existence of a single-valued relation between a 5-tuple of
 Booleans and a domain element




$n_0{=}n_0\mbox{ and }n_1{=}n_1\qquad\mbox{fof}(\mbox{n0\_and\_n1\_reflexive},\mbox{axiom})$

$n_0{=}n_1 \ \Rightarrow \ \mbox{goal}\qquad\mbox{fof}(\mbox{n0\_equal\_n}_1,\mbox{axiom})$

$n_1{=}n_0 \ \Rightarrow \ \mbox{goal}\qquad\mbox{fof}(\mbox{n1\_equal\_n}_0,\mbox{axiom})$

$\forall a,b,c,d,e{:}\;( ( a{=}a\mbox{ and }b{=}b\mbox{ and }c{=}c\mbox{ and }d{=}d\mbox{ and }e{=}e ) \ \Rightarrow \ \exists f{:}\;f(a,b,c,d,e,f) )\qquad\mbox{fof}(\mbox{relation\_exists},\mbox{axiom})$

$\forall a,b,c,d,e,f,g,h,i,j,k{:}\;( ( f(a,b,c,d,e,k)\mbox{ and }f(f,g,h,i,j,k) ) \ \Rightarrow \ ( a{=}f\mbox{ and }b{=}g\mbox{ and }c{=}h\mbox{ and }d{=}i\mbox{ and }e{=}j ) )\qquad\mbox{fof}(\mbox{relation\_injective},\mbox{axiom})$

$\mbox{goal}\qquad\mbox{fof}(\mbox{goal\_to\_be\_proved},\mbox{conjecture})$

\medskip\textbf{MSC008-1.002.p} The (in)constructability of Graeco-Latin Squares

The constructibility of Graeco-Latin squares of order 4t+2.
 This is impossible for t=0,1, but possible for all other
 cases. The size is the size of the squares.




$\neg\,\mbox{eq}(p_1,p_2)\qquad\mbox{cnf}(\mbox{p\_1\_is\_not\_p}_2,\mbox{axiom})$

$\mbox{eq}(x,x)\qquad\mbox{cnf}(\mbox{reflexivity},\mbox{axiom})$

$\mbox{eq}(x,y) \ \Rightarrow \ \mbox{eq}(y,x)\qquad\mbox{cnf}(\mbox{symmetry},\mbox{axiom})$

$( \mbox{latin}(\mbox{row},\mbox{column},\mbox{label}_1)\mbox{ and }\mbox{latin}(\mbox{row},\mbox{column},\mbox{label}_2) ) \ \Rightarrow \ \mbox{eq}(\mbox{label}_1,\mbox{label}_2)\qquad\mbox{cnf}(\mbox{latin\_element\_is\_unique},\mbox{axiom})$

$( \mbox{latin}(\mbox{row},\mbox{column}_1,\mbox{label})\mbox{ and }\mbox{latin}(\mbox{row},\mbox{column}_2,\mbox{label}) ) \ \Rightarrow \ \mbox{eq}(\mbox{column}_1,\mbox{column}_2)\qquad\mbox{cnf}(\mbox{latin\_column\_is\_unique},\mbox{axiom})$

$( \mbox{latin}(\mbox{row}_1,\mbox{column},\mbox{label})\mbox{ and }\mbox{latin}(\mbox{row}_2,\mbox{column},\mbox{label}) ) \ \Rightarrow \ \mbox{eq}(\mbox{row}_1,\mbox{row}_2)\qquad\mbox{cnf}(\mbox{latin\_row\_is\_unique},\mbox{axiom})$

$( \mbox{greek}(\mbox{row},\mbox{column},\mbox{label}_1)\mbox{ and }\mbox{greek}(\mbox{row},\mbox{column},\mbox{label}_2) ) \ \Rightarrow \ \mbox{eq}(\mbox{label}_1,\mbox{label}_2)\qquad\mbox{cnf}(\mbox{greek\_element\_is\_unique},\mbox{axiom})$

$( \mbox{greek}(\mbox{row},\mbox{column}_1,\mbox{label})\mbox{ and }\mbox{greek}(\mbox{row},\mbox{column}_2,\mbox{label}) ) \ \Rightarrow \ \mbox{eq}(\mbox{column}_1,\mbox{column}_2)\qquad\mbox{cnf}(\mbox{greek\_column\_is\_unique},\mbox{axiom})$

$( \mbox{greek}(\mbox{row}_1,\mbox{column},\mbox{label})\mbox{ and }\mbox{greek}(\mbox{row}_2,\mbox{column},\mbox{label}) ) \ \Rightarrow \ \mbox{eq}(\mbox{row}_1,\mbox{row}_2)\qquad\mbox{cnf}(\mbox{greek\_row\_is\_unique},\mbox{axiom})$

$\mbox{latin}(\mbox{row},\mbox{column},p_1)\mbox{ or }\mbox{latin}(\mbox{row},\mbox{column},p_2)\qquad\mbox{cnf}(\mbox{latin\_cell\_element},\mbox{axiom})$

$\mbox{latin}(\mbox{row},p_1,\mbox{label})\mbox{ or }\mbox{latin}(\mbox{row},p_2,\mbox{label})\qquad\mbox{cnf}(\mbox{latin\_column\_required},\mbox{axiom})$

$\mbox{latin}(p_1,\mbox{column},\mbox{label})\mbox{ or }\mbox{latin}(p_2,\mbox{column},\mbox{label})\qquad\mbox{cnf}(\mbox{latin\_row\_required},\mbox{axiom})$

$\mbox{greek}(\mbox{row},\mbox{column},p_1)\mbox{ or }\mbox{greek}(\mbox{row},\mbox{column},p_2)\qquad\mbox{cnf}(\mbox{greek\_cell\_element},\mbox{axiom})$

$\mbox{greek}(\mbox{row},p_1,\mbox{label})\mbox{ or }\mbox{greek}(\mbox{row},p_2,\mbox{label})\qquad\mbox{cnf}(\mbox{greek\_column\_required},\mbox{axiom})$

$\mbox{greek}(p_1,\mbox{column},\mbox{label})\mbox{ or }\mbox{greek}(p_2,\mbox{column},\mbox{label})\qquad\mbox{cnf}(\mbox{greek\_row\_required},\mbox{axiom})$

$( \mbox{greek}(\mbox{row}_1,\mbox{column}_1,\mbox{label}_1)\mbox{ and }\mbox{latin}(\mbox{row}_1,\mbox{column}_1,\mbox{label}_2)\mbox{ and }\mbox{greek}(\mbox{row}_2,\mbox{column}_2,\mbox{label}_1)\mbox{ and }\mbox{latin}(\mbox{row}_2,\mbox{column}_2,\mbox{label}_2) ) \ \Rightarrow \ \mbox{eq}(\mbox{column}_1,\mbox{column}_2)\qquad\mbox{cnf}(\mbox{no\_two\_same}_1,\mbox{negated\_conjecture})$

$( \mbox{greek}(\mbox{row}_1,\mbox{column}_1,\mbox{label}_1)\mbox{ and }\mbox{latin}(\mbox{row}_1,\mbox{column}_1,\mbox{label}_2)\mbox{ and }\mbox{greek}(\mbox{row}_2,\mbox{column}_2,\mbox{label}_1)\mbox{ and }\mbox{latin}(\mbox{row}_2,\mbox{column}_2,\mbox{label}_2) ) \ \Rightarrow \ \mbox{eq}(\mbox{row}_1,\mbox{row}_2)\qquad\mbox{cnf}(\mbox{no\_two\_same}_2,\mbox{negated\_conjecture})$

\medskip\textbf{MSC017+1.p} Diving has no bad outcomes






$\forall d{:}\;( \mbox{dive}(d) \ \Rightarrow \ \mbox{nitrogen}(d) = \mbox{padi}(\mbox{depth}(d),\mbox{time}(d)) )\qquad\mbox{fof}(\mbox{dive\_nitrogen},\mbox{axiom})$

$\forall d{:}\;( \mbox{dive}(d) \ \Rightarrow \ ( ( \mbox{greater}(\mbox{depth}(d),\mbox{depth\_limit})\mbox{ or }\mbox{greater}(\mbox{time}(d),\mbox{time\_limit}) )\iff \mbox{greater}(\mbox{nitrogen}(d),\mbox{nitrogen\_limit}) ) )\qquad\mbox{fof}(\mbox{depth\_and\_time\_and\_nitrogen},\mbox{axiom})$

$\forall d{:}\;( \mbox{dive}(d) \ \Rightarrow \ ( \mbox{greater}(\mbox{nitrogen}(d),\mbox{nitrogen\_limit})\iff \mbox{outcome}(d,\mbox{dci}) ) )\qquad\mbox{fof}(\mbox{too\_much\_nitrogen},\mbox{axiom})$

$\mbox{bad}(\mbox{dci})\qquad\mbox{fof}(\mbox{bad\_dci},\mbox{axiom})$

$\forall d{:}\;( \mbox{dive}(d) \ \Rightarrow \ \forall o{:}\;( ( \mbox{outcome}(d,o)\mbox{ and }\mbox{bad}(o) ) \ \Rightarrow \ o = \mbox{dci} ) )\qquad\mbox{fof}(\mbox{dci\_is\_the\_only\_bad\_outcome},\mbox{axiom})$

$\forall d{:}\;( \mbox{dive}(d) \ \Rightarrow \ ( \neg\,\mbox{greater}(\mbox{depth}(d),\mbox{depth\_limit})\mbox{ and }\neg\,\mbox{greater}(\mbox{time}(d),\mbox{time\_limit}) ) )\qquad\mbox{fof}(\mbox{no\_deep\_long},\mbox{axiom})$

$\forall d{:}\;( \mbox{dive}(d) \ \Rightarrow \ \forall o{:}\;( \mbox{outcome}(d,o) \ \Rightarrow \ \neg\,\mbox{bad}(o) ) )\qquad\mbox{fof}(\mbox{no\_bad},\mbox{conjecture})$

\medskip\textbf{MSC028=1.p} 2 and 3 cents stamps

Suppose we have stamps of two different denominations, 3 cents and
 5 cents. We want to show that it is possible to make up exactly 
 any postage of 8 cents or more using stamps of these two 
 denominations. The formula below asserts this, however "8" 
 replaced by "some lower bound".




$\exists l{:}\;\mbox{\$int}{:}\;\forall k{:}\;\mbox{\$int}{:}\;( \mbox{\$greater}(k,l) \ \Rightarrow \ \exists s_1{:}\;\mbox{\$int},s_2{:}\;\mbox{\$int}{:}\;( \mbox{\$greatereq}(s_1,0)\mbox{ and }\mbox{\$greatereq}(s_2,0)\mbox{ and }k = \mbox{\$sum}(\mbox{\$product}(s_1,3),\mbox{\$product}(s_2,5)) ) )\qquad\mbox{tff}(\mbox{formula},\mbox{conjecture})$

\medskip\textbf{MSC004-1.p} Show that the boy, John, has 10 fingers






$\mbox{has\_parts}(\mbox{big\_part},\mbox{number\_of\_mid\_parts},\mbox{mid\_part}) \ \Rightarrow \ ( \mbox{in}(\mbox{object\_in}(\mbox{big\_part},\mbox{mid\_part},\mbox{small\_part},\mbox{number\_of\_mid\_parts},\mbox{number\_of\_small\_parts}),\mbox{mid\_part})\mbox{ or }\mbox{has\_parts}(\mbox{big\_part},\mbox{times}(\mbox{number\_of\_mid\_parts},\mbox{number\_of\_small\_parts}),\mbox{small\_part}) )\qquad\mbox{cnf}(\mbox{not\_part\_inheritance},\mbox{axiom})$

$( \mbox{has\_parts}(\mbox{big\_part},\mbox{number\_of\_mid\_parts},\mbox{mid\_part})\mbox{ and }\mbox{has\_parts}(\mbox{object\_in}(\mbox{big\_part},\mbox{mid\_part},\mbox{small\_part},\mbox{number\_of\_mid\_parts},\mbox{number\_of\_small\_parts}),\mbox{number\_of\_small\_parts},\mbox{small\_part}) ) \ \Rightarrow \ \mbox{has\_parts}(\mbox{big\_part},\mbox{times}(\mbox{number\_of\_mid\_parts},\mbox{number\_of\_small\_parts}),\mbox{small\_part})\qquad\mbox{cnf}(\mbox{part\_inheritance},\mbox{axiom})$

$\mbox{in}(\mbox{john},\mbox{boy})\qquad\mbox{cnf}(\mbox{john\_is\_a\_boy},\mbox{hypothesis})$

$\mbox{in}(x,\mbox{boy}) \ \Rightarrow \ \mbox{in}(x,\mbox{human})\qquad\mbox{cnf}(\mbox{in\_boy\_in\_human},\mbox{hypothesis})$

$\mbox{in}(x,\mbox{hand}) \ \Rightarrow \ \mbox{has\_parts}(x,n_5,\mbox{fingers})\qquad\mbox{cnf}(\mbox{hands\_have\_5\_fingers},\mbox{hypothesis})$

$\mbox{in}(x,\mbox{human}) \ \Rightarrow \ \mbox{has\_parts}(x,n_2,\mbox{arm})\qquad\mbox{cnf}(\mbox{humans\_have\_two\_arms},\mbox{hypothesis})$

$\mbox{in}(x,\mbox{arm}) \ \Rightarrow \ \mbox{has\_parts}(x,n_1,\mbox{hand})\qquad\mbox{cnf}(\mbox{arms\_have\_one\_hand},\mbox{hypothesis})$

$\neg\,\mbox{has\_parts}(\mbox{john},\mbox{times}(\mbox{times}(n_2,n_1),n_5),\mbox{fingers})\qquad\mbox{cnf}(\mbox{prove\_john\_has\_10\_fingers},\mbox{negated\_conjecture})$

\medskip\textbf{MSC008-2.002.p} The inconstructability of a Graeco-Latin Square

The constructibility of Graeco-Latin squares of order 4t+2.
 This is impossible for t=0,1, but possible for all other
 cases.




$\neg\,\mbox{eq}(p_1,p_2)\qquad\mbox{cnf}(\mbox{p1\_is\_not\_p}_2,\mbox{axiom})$

$\mbox{eq}(a,a)\qquad\mbox{cnf}(\mbox{reflexivity},\mbox{axiom})$

$\mbox{eq}(a,b) \ \Rightarrow \ \mbox{eq}(b,a)\qquad\mbox{cnf}(\mbox{symmetry},\mbox{axiom})$

$( \mbox{latin}(a,b,c)\mbox{ and }\mbox{latin}(a,b,d) ) \ \Rightarrow \ \mbox{eq}(d,c)\qquad\mbox{cnf}(\mbox{latin\_element\_is\_unique},\mbox{axiom})$

$( \mbox{latin}(a,b,c)\mbox{ and }\mbox{latin}(a,d,c) ) \ \Rightarrow \ \mbox{eq}(d,b)\qquad\mbox{cnf}(\mbox{latin\_column\_is\_unique},\mbox{axiom})$

$( \mbox{latin}(a,b,c)\mbox{ and }\mbox{latin}(d,b,c) ) \ \Rightarrow \ \mbox{eq}(d,a)\qquad\mbox{cnf}(\mbox{latin\_row\_is\_unique},\mbox{axiom})$

$( \mbox{greek}(a,b,c)\mbox{ and }\mbox{greek}(a,b,d) ) \ \Rightarrow \ \mbox{eq}(d,c)\qquad\mbox{cnf}(\mbox{greek\_element\_is\_unique},\mbox{axiom})$

$( \mbox{greek}(a,b,c)\mbox{ and }\mbox{greek}(a,d,c) ) \ \Rightarrow \ \mbox{eq}(d,b)\qquad\mbox{cnf}(\mbox{greek\_column\_is\_unique},\mbox{axiom})$

$( \mbox{greek}(a,b,c)\mbox{ and }\mbox{greek}(d,b,c) ) \ \Rightarrow \ \mbox{eq}(d,a)\qquad\mbox{cnf}(\mbox{greek\_row\_is\_unique},\mbox{axiom})$

$\mbox{latin}(e,f,p_1)\mbox{ or }\mbox{latin}(e,f,p_2)\qquad\mbox{cnf}(\mbox{latin\_cell\_element},\mbox{axiom})$

$\mbox{latin}(g,p_1,h)\mbox{ or }\mbox{latin}(g,p_2,h)\qquad\mbox{cnf}(\mbox{latin\_column\_required},\mbox{axiom})$

$\mbox{latin}(p_1,i,j)\mbox{ or }\mbox{latin}(p_2,i,j)\qquad\mbox{cnf}(\mbox{latin\_row\_required},\mbox{axiom})$

$\mbox{greek}(k,l,p_1)\mbox{ or }\mbox{greek}(k,l,p_2)\qquad\mbox{cnf}(\mbox{greek\_cell\_element},\mbox{axiom})$

$\mbox{greek}(m,p_1,n)\mbox{ or }\mbox{greek}(m,p_2,n)\qquad\mbox{cnf}(\mbox{greek\_column\_required},\mbox{axiom})$

$\mbox{greek}(p_1,o,p)\mbox{ or }\mbox{greek}(p_2,o,p)\qquad\mbox{cnf}(\mbox{greek\_row\_required},\mbox{axiom})$

$( \mbox{greek}(a,b,c)\mbox{ and }\mbox{latin}(a,b,d)\mbox{ and }\mbox{greek}(e,f,c)\mbox{ and }\mbox{latin}(e,f,d) ) \ \Rightarrow \ ( \mbox{eq}(f,b)\mbox{ or }\mbox{eq}(e,a) )\qquad\mbox{cnf}(\mbox{no\_two\_same},\mbox{negated\_conjecture})$

\medskip\textbf{MSC001-1.p} A Blind Hand Problem






$\mbox{at}(a,\mbox{there},b) \ \Rightarrow \ \neg\,\mbox{at}(a,\mbox{here},b)\qquad\mbox{cnf}(\mbox{clause}_1,\mbox{axiom})$

$\neg\,\mbox{hold}(\mbox{thing}(a),\mbox{do}(\mbox{let\_go},b))\qquad\mbox{cnf}(\mbox{clause}_2,\mbox{axiom})$

$\neg\,\mbox{red}(\mbox{hand})\qquad\mbox{cnf}(\mbox{clause}_3,\mbox{axiom})$

$\mbox{at}(\mbox{hand},a,\mbox{do}(\mbox{go}(a),b))\qquad\mbox{cnf}(\mbox{clause}_5,\mbox{axiom})$

$\mbox{at}(\mbox{thing}(s),\mbox{here},\mbox{now})\qquad\mbox{cnf}(\mbox{clause}_6,\mbox{axiom})$

$\mbox{at}(\mbox{thing}(a),b,\mbox{do}(\mbox{go}(b),c)) \ \Rightarrow \ ( \mbox{at}(\mbox{thing}(a),b,c)\mbox{ or }\mbox{hold}(\mbox{thing}(a),c) )\qquad\mbox{cnf}(\mbox{clause}_7,\mbox{axiom})$

$( \mbox{at}(\mbox{hand},a,b)\mbox{ and }\mbox{at}(\mbox{thing}(c),a,b) ) \ \Rightarrow \ \mbox{hold}(\mbox{thing}(\mbox{taken}(b)),\mbox{do}(\mbox{pick\_up},b))\qquad\mbox{cnf}(\mbox{clause}_8,\mbox{axiom})$

$( \mbox{hold}(\mbox{thing}(a),b)\mbox{ and }\mbox{at}(\mbox{hand},c,b) ) \ \Rightarrow \ \mbox{at}(\mbox{thing}(a),c,b)\qquad\mbox{cnf}(\mbox{clause}_9,\mbox{axiom})$

$( \mbox{hold}(\mbox{thing}(a),b)\mbox{ and }\mbox{at}(\mbox{thing}(a),c,b) ) \ \Rightarrow \ \mbox{at}(\mbox{hand},c,b)\qquad\mbox{cnf}(\mbox{clause}_{10},\mbox{axiom})$

$( \mbox{red}(a)\mbox{ and }\mbox{at}(a,\mbox{there},b) ) \ \Rightarrow \ \mbox{answer}(b)\qquad\mbox{cnf}(\mbox{clause}_{11},\mbox{axiom})$

$\mbox{at}(\mbox{thing}(a),b,c) \ \Rightarrow \ \mbox{at}(\mbox{thing}(a),b,\mbox{do}(\mbox{go}(b),c))\qquad\mbox{cnf}(\mbox{clause}_{12},\mbox{axiom})$

$\mbox{hold}(\mbox{thing}(a),b) \ \Rightarrow \ \mbox{hold}(\mbox{thing}(a),\mbox{do}(\mbox{go}(c),b))\qquad\mbox{cnf}(\mbox{clause}_{13},\mbox{axiom})$

$\mbox{at}(\mbox{hand},a,b) \ \Rightarrow \ \mbox{at}(\mbox{thing}(\mbox{taken}(b)),a,b)\qquad\mbox{cnf}(\mbox{clause}_{14},\mbox{axiom})$

$\mbox{at}(a,b,c) \ \Rightarrow \ \mbox{at}(a,b,\mbox{do}(\mbox{pick\_up},c))\qquad\mbox{cnf}(\mbox{clause}_{15},\mbox{axiom})$

$\mbox{at}(a,b,c) \ \Rightarrow \ \mbox{at}(a,b,\mbox{do}(\mbox{let\_go},c))\qquad\mbox{cnf}(\mbox{clause}_{16},\mbox{axiom})$

$\mbox{at}(a,b,\mbox{do}(\mbox{let\_go},c)) \ \Rightarrow \ \mbox{at}(a,b,c)\qquad\mbox{cnf}(\mbox{clause}_{17},\mbox{axiom})$

$\mbox{at}(a,\mbox{here},\mbox{now}) \ \Rightarrow \ \mbox{red}(a)\qquad\mbox{cnf}(\mbox{things\_here\_now\_are\_red},\mbox{hypothesis})$

$\neg\,\mbox{answer}(a)\qquad\mbox{cnf}(\mbox{prove\_there\_is\_a\_red\_thing},\mbox{negated\_conjecture})$

\medskip\textbf{MSC015-1.010.p} Binary counter k=10

Each instance of the problem asserts
 p(0*).                 // p[0]
 p(x*01*) $\to$ p(x*10*).  // p[i] $\to$ p[i + 1]
 not p(1*).             // not p[2$\wedge$n - 1]
 These problems are unsatisfiable and have exponentially large
 propositional resolution refutations, while there is a short
 (quadratic) first order refutation.




$p(s_0,s_0,s_0,s_0,s_0,s_0,s_0,s_0,s_0,s_0)\qquad\mbox{cnf}(\mbox{init},\mbox{axiom})$

$p(x_0,x_1,x_2,x_3,x_4,x_5,x_6,x_7,x_8,s_0) \ \Rightarrow \ p(x_0,x_1,x_2,x_3,x_4,x_5,x_6,x_7,x_8,s_1)\qquad\mbox{cnf}(\mbox{rule}_1,\mbox{axiom})$

$p(x_0,x_1,x_2,x_3,x_4,x_5,x_6,x_7,s_0,s_1) \ \Rightarrow \ p(x_0,x_1,x_2,x_3,x_4,x_5,x_6,x_7,s_1,s_0)\qquad\mbox{cnf}(\mbox{rule}_2,\mbox{axiom})$

$p(x_0,x_1,x_2,x_3,x_4,x_5,x_6,s_0,s_1,s_1) \ \Rightarrow \ p(x_0,x_1,x_2,x_3,x_4,x_5,x_6,s_1,s_0,s_0)\qquad\mbox{cnf}(\mbox{rule}_3,\mbox{axiom})$

$p(x_0,x_1,x_2,x_3,x_4,x_5,s_0,s_1,s_1,s_1) \ \Rightarrow \ p(x_0,x_1,x_2,x_3,x_4,x_5,s_1,s_0,s_0,s_0)\qquad\mbox{cnf}(\mbox{rule}_4,\mbox{axiom})$

$p(x_0,x_1,x_2,x_3,x_4,s_0,s_1,s_1,s_1,s_1) \ \Rightarrow \ p(x_0,x_1,x_2,x_3,x_4,s_1,s_0,s_0,s_0,s_0)\qquad\mbox{cnf}(\mbox{rule}_5,\mbox{axiom})$

$p(x_0,x_1,x_2,x_3,s_0,s_1,s_1,s_1,s_1,s_1) \ \Rightarrow \ p(x_0,x_1,x_2,x_3,s_1,s_0,s_0,s_0,s_0,s_0)\qquad\mbox{cnf}(\mbox{rule}_6,\mbox{axiom})$

$p(x_0,x_1,x_2,s_0,s_1,s_1,s_1,s_1,s_1,s_1) \ \Rightarrow \ p(x_0,x_1,x_2,s_1,s_0,s_0,s_0,s_0,s_0,s_0)\qquad\mbox{cnf}(\mbox{rule}_7,\mbox{axiom})$

$p(x_0,x_1,s_0,s_1,s_1,s_1,s_1,s_1,s_1,s_1) \ \Rightarrow \ p(x_0,x_1,s_1,s_0,s_0,s_0,s_0,s_0,s_0,s_0)\qquad\mbox{cnf}(\mbox{rule}_8,\mbox{axiom})$

$p(x_0,s_0,s_1,s_1,s_1,s_1,s_1,s_1,s_1,s_1) \ \Rightarrow \ p(x_0,s_1,s_0,s_0,s_0,s_0,s_0,s_0,s_0,s_0)\qquad\mbox{cnf}(\mbox{rule}_9,\mbox{axiom})$

$p(s_0,s_1,s_1,s_1,s_1,s_1,s_1,s_1,s_1,s_1) \ \Rightarrow \ p(s_1,s_0,s_0,s_0,s_0,s_0,s_0,s_0,s_0,s_0)\qquad\mbox{cnf}(\mbox{rule}_{10},\mbox{axiom})$

$\neg\,p(s_1,s_1,s_1,s_1,s_1,s_1,s_1,s_1,s_1,s_1)\qquad\mbox{cnf}(\mbox{goal},\mbox{negated\_conjecture})$

\medskip\textbf{MSC005-1.p} The evaluation of XOR expressions






$\mbox{value}(\mbox{truth},\mbox{truth})\qquad\mbox{cnf}(\mbox{true\_is\_true},\mbox{axiom})$

$\mbox{value}(\mbox{falsity},\mbox{falsity})\qquad\mbox{cnf}(\mbox{false\_is\_false},\mbox{axiom})$

$( \mbox{value}(x,\mbox{truth})\mbox{ and }\mbox{value}(y,\mbox{truth}) ) \ \Rightarrow \ \mbox{value}(\mbox{xor}(x,y),\mbox{falsity})\qquad\mbox{cnf}(\mbox{true\_xor\_true},\mbox{axiom})$

$( \mbox{value}(x,\mbox{truth})\mbox{ and }\mbox{value}(y,\mbox{falsity}) ) \ \Rightarrow \ \mbox{value}(\mbox{xor}(x,y),\mbox{truth})\qquad\mbox{cnf}(\mbox{true\_xor\_false},\mbox{axiom})$

$( \mbox{value}(x,\mbox{falsity})\mbox{ and }\mbox{value}(y,\mbox{truth}) ) \ \Rightarrow \ \mbox{value}(\mbox{xor}(x,y),\mbox{truth})\qquad\mbox{cnf}(\mbox{false\_xor\_true},\mbox{axiom})$

$( \mbox{value}(x,\mbox{falsity})\mbox{ and }\mbox{value}(y,\mbox{falsity}) ) \ \Rightarrow \ \mbox{value}(\mbox{xor}(x,y),\mbox{falsity})\qquad\mbox{cnf}(\mbox{false\_xor\_false},\mbox{axiom})$

$\neg\,\mbox{value}(\mbox{xor}(\mbox{xor}(\mbox{xor}(\mbox{xor}(\mbox{truth},\mbox{falsity}),\mbox{falsity}),\mbox{truth}),\mbox{falsity}),\mbox{value})\qquad\mbox{cnf}(\mbox{evaluate\_expression},\mbox{negated\_conjecture})$

\medskip\textbf{MSC021$\wedge$5.p} TPS problem THM300

Relation between HALF and DOUBLE functions.




$\mbox{cS}{:}\;\mbox{\$i}\to \mbox{\$i}\qquad\mbox{thf}(\mbox{cS},\mbox{type})$

$\mbox{cDOUBLE}{:}\;\mbox{\$i}\to \mbox{\$i}\to \mbox{\$o}\qquad\mbox{thf}(\mbox{cDOUBLE},\mbox{type})$

$\mbox{cHALF}{:}\;\mbox{\$i}\to \mbox{\$i}\to \mbox{\$o}\qquad\mbox{thf}(\mbox{cHALF},\mbox{type})$

$c_0{:}\;\mbox{\$i}\qquad\mbox{thf}(c_0,\mbox{type})$

$( \mbox{cDOUBLE}@ c_0@ c_0\mbox{ and }\forall \mbox{xx}{:}\;\mbox{\$i},\mbox{xy}{:}\;\mbox{\$i}{:}\;( ( \mbox{cDOUBLE}@ \mbox{xx}@ \mbox{xy} ) \ \Rightarrow \ ( \mbox{cDOUBLE}@ ( \mbox{cS}@ \mbox{xx} )@ ( \mbox{cS}@ ( \mbox{cS}@ \mbox{xy} ) ) ) )\mbox{ and }\forall q{:}\;\mbox{\$i}\to \mbox{\$i}\to \mbox{\$o},\mbox{xu}{:}\;\mbox{\$i},\mbox{xv}{:}\;\mbox{\$i}{:}\;( ( \mbox{cHALF}@ \mbox{xu}@ \mbox{xv}\mbox{ and }q@ c_0@ c_0\mbox{ and }q@ ( \mbox{cS}@ c_0 )@ c_0\mbox{ and }\forall \mbox{xx}{:}\;\mbox{\$i},\mbox{xy}{:}\;\mbox{\$i}{:}\;( ( q@ \mbox{xx}@ \mbox{xy} ) \ \Rightarrow \ ( q@ ( \mbox{cS}@ ( \mbox{cS}@ \mbox{xx} ) )@ ( \mbox{cS}@ \mbox{xy} ) ) ) ) \ \Rightarrow \ ( q@ \mbox{xu}@ \mbox{xv} ) ) ) \ \Rightarrow \ \forall \mbox{xu}{:}\;\mbox{\$i},\mbox{xv}{:}\;\mbox{\$i}{:}\;( ( \mbox{cHALF}@ \mbox{xu}@ \mbox{xv} ) \ \Rightarrow \ ( \mbox{cDOUBLE}@ \mbox{xv}@ \mbox{xu}\mbox{ or }\mbox{cDOUBLE}@ ( \mbox{cS}@ \mbox{xv} )@ ( \mbox{cS}@ \mbox{xu} ) ) )\qquad\mbox{thf}(\mbox{cTHM}_{300},\mbox{conjecture})$

\medskip\textbf{MSC003-1.p} Show that the boy, John, has 2 hands






$\mbox{has\_parts}(\mbox{big\_part},\mbox{number\_of\_mid\_parts},\mbox{mid\_part}) \ \Rightarrow \ ( \mbox{in}(\mbox{object\_in}(\mbox{big\_part},\mbox{mid\_part},\mbox{small\_part},\mbox{number\_of\_mid\_parts},\mbox{number\_of\_small\_parts}),\mbox{mid\_part})\mbox{ or }\mbox{has\_parts}(\mbox{big\_part},\mbox{times}(\mbox{number\_of\_mid\_parts},\mbox{number\_of\_small\_parts}),\mbox{small\_part}) )\qquad\mbox{cnf}(\mbox{not\_part\_inheritance},\mbox{axiom})$

$( \mbox{has\_parts}(\mbox{big\_part},\mbox{number\_of\_mid\_parts},\mbox{mid\_part})\mbox{ and }\mbox{has\_parts}(\mbox{object\_in}(\mbox{big\_part},\mbox{mid\_part},\mbox{small\_part},\mbox{number\_of\_mid\_parts},\mbox{number\_of\_small\_parts}),\mbox{number\_of\_small\_parts},\mbox{small\_part}) ) \ \Rightarrow \ \mbox{has\_parts}(\mbox{big\_part},\mbox{times}(\mbox{number\_of\_mid\_parts},\mbox{number\_of\_small\_parts}),\mbox{small\_part})\qquad\mbox{cnf}(\mbox{part\_inheritance},\mbox{axiom})$

$\mbox{in}(\mbox{john},\mbox{boy})\qquad\mbox{cnf}(\mbox{john\_is\_a\_boy},\mbox{hypothesis})$

$\mbox{in}(x,\mbox{boy}) \ \Rightarrow \ \mbox{in}(x,\mbox{human})\qquad\mbox{cnf}(\mbox{in\_boy\_in\_human},\mbox{hypothesis})$

$\mbox{in}(x,\mbox{hand}) \ \Rightarrow \ \mbox{has\_parts}(x,n_5,\mbox{fingers})\qquad\mbox{cnf}(\mbox{hands\_have\_5\_fingers},\mbox{hypothesis})$

$\mbox{in}(x,\mbox{human}) \ \Rightarrow \ \mbox{has\_parts}(x,n_2,\mbox{arm})\qquad\mbox{cnf}(\mbox{humans\_have\_two\_arms},\mbox{hypothesis})$

$\mbox{in}(x,\mbox{arm}) \ \Rightarrow \ \mbox{has\_parts}(x,n_1,\mbox{hand})\qquad\mbox{cnf}(\mbox{arms\_have\_one\_hand},\mbox{hypothesis})$

$\neg\,\mbox{has\_parts}(\mbox{john},\mbox{times}(n_2,n_1),\mbox{hand})\qquad\mbox{cnf}(\mbox{prove\_john\_has\_2\_hands},\mbox{negated\_conjecture})$

\medskip\textbf{MSC022=2.p} Celcius 37 to Fahrenheit conversion






$\mbox{celsius\_fahrenheit\_temperature\_conversion}{:}\;( \mbox{\$real}\times \mbox{\$real} )\to \mbox{\$o}\qquad\mbox{tff}(\mbox{celsius\_fahrenheit\_temperature\_conversion\_type},\mbox{type})$

$\forall c{:}\;\mbox{\$real},f{:}\;\mbox{\$real}{:}\;( \mbox{\$sum}(\mbox{\$product}(\mbox{1.}_8,c),\mbox{32.}_0) = f \ \Rightarrow \ \mbox{celsius\_fahrenheit\_temperature\_conversion}(c,f) )\qquad\mbox{tff}(\mbox{celsius\_fahrenheit\_temperature\_conversion},\mbox{axiom})$

$\exists f{:}\;\mbox{\$real}{:}\;\mbox{celsius\_fahrenheit\_temperature\_conversion}(\mbox{37.}_0,f)\qquad\mbox{tff}(\mbox{celsius\_37\_to\_fahrenheit},\mbox{conjecture})$

\medskip\textbf{MSC026-1.p} Sets, numbers, lists, etc, that make up the Isabelle/HOL library






$\mbox{include}(\mbox{'Axioms/MSC001-0.ax'})$

$\mbox{include}(\mbox{'Axioms/MSC001-1.ax'})$

\medskip\textbf{MSC020$\wedge$5.p} TPS problem THM301

Relation between HALF and DOUBLE functions.




$\mbox{cHALF}{:}\;\mbox{\$i}\to \mbox{\$i}\to \mbox{\$o}\qquad\mbox{thf}(\mbox{cHALF},\mbox{type})$

$\mbox{cDOUBLE}{:}\;\mbox{\$i}\to \mbox{\$i}\to \mbox{\$o}\qquad\mbox{thf}(\mbox{cDOUBLE},\mbox{type})$

$\mbox{cS}{:}\;\mbox{\$i}\to \mbox{\$i}\qquad\mbox{thf}(\mbox{cS},\mbox{type})$

$c_0{:}\;\mbox{\$i}\qquad\mbox{thf}(c_0,\mbox{type})$

$( \forall q{:}\;\mbox{\$i}\to \mbox{\$i}\to \mbox{\$o},\mbox{xu}{:}\;\mbox{\$i},\mbox{xv}{:}\;\mbox{\$i}{:}\;( ( \mbox{cDOUBLE}@ \mbox{xu}@ \mbox{xv}\mbox{ and }q@ c_0@ c_0\mbox{ and }\forall \mbox{xx}{:}\;\mbox{\$i},\mbox{xy}{:}\;\mbox{\$i}{:}\;( ( q@ \mbox{xx}@ \mbox{xy} ) \ \Rightarrow \ ( q@ ( \mbox{cS}@ \mbox{xx} )@ ( \mbox{cS}@ ( \mbox{cS}@ \mbox{xy} ) ) ) ) ) \ \Rightarrow \ ( q@ \mbox{xu}@ \mbox{xv} ) )\mbox{ and }\mbox{cHALF}@ c_0@ c_0\mbox{ and }\mbox{cHALF}@ ( \mbox{cS}@ c_0 )@ c_0\mbox{ and }\forall \mbox{xx}{:}\;\mbox{\$i},\mbox{xy}{:}\;\mbox{\$i}{:}\;( ( \mbox{cHALF}@ \mbox{xx}@ \mbox{xy} ) \ \Rightarrow \ ( \mbox{cHALF}@ ( \mbox{cS}@ ( \mbox{cS}@ \mbox{xx} ) )@ ( \mbox{cS}@ \mbox{xy} ) ) ) ) \ \Rightarrow \ \forall \mbox{xu}{:}\;\mbox{\$i},\mbox{xv}{:}\;\mbox{\$i}{:}\;( ( \mbox{cDOUBLE}@ \mbox{xu}@ \mbox{xv} ) \ \Rightarrow \ ( \mbox{cHALF}@ \mbox{xv}@ \mbox{xu} ) )\qquad\mbox{thf}(\mbox{cTHM}_{301},\mbox{conjecture})$

\medskip\textbf{MSC014+1.p} Find a model with a functional relation which is injective, n=4




$n_0{=}n_0\mbox{ and }n_1{=}n_1\qquad\mbox{fof}(\mbox{n0\_and\_n1\_reflexive},\mbox{axiom})$

$\neg\,n_0{=}n_1\mbox{ and }\neg\,n_1{=}n_0\qquad\mbox{fof}(\mbox{n0\_not\_n}_1,\mbox{axiom})$

$\forall x_1,x_2,x_3,x_4{:}\;( ( x_1{=}x_1\mbox{ and }x_2{=}x_2\mbox{ and }x_3{=}x_3\mbox{ and }x_4{=}x_4 ) \ \Rightarrow \ \exists z{:}\;f(x_1,x_2,x_3,x_4,z) )\qquad\mbox{fof}(\mbox{exists\_f},\mbox{axiom})$

$\forall x_1,x_2,x_3,x_4,y_1,y_2,y_3,y_4,z{:}\;( ( f(x_1,x_2,x_3,x_4,z)\mbox{ and }f(y_1,y_2,y_3,y_4,z) ) \ \Rightarrow \ ( x_1{=}y_1\mbox{ and }x_2{=}y_2\mbox{ and }x_3{=}y_3\mbox{ and }x_4{=}y_4 ) )\qquad\mbox{fof}(\mbox{inject\_f},\mbox{axiom})$

\medskip\textbf{MSC002-1.p} A Blind Hand Problem






$\mbox{at}(\mbox{something},\mbox{here},\mbox{now})\qquad\mbox{cnf}(\mbox{something\_is\_here\_now},\mbox{axiom})$

$\mbox{hand\_at}(\mbox{place},\mbox{situation}) \ \Rightarrow \ \mbox{hand\_at}(\mbox{place},\mbox{let\_go}(\mbox{situation}))\qquad\mbox{cnf}(\mbox{hand\_let\_go},\mbox{axiom})$

$\mbox{hand\_at}(\mbox{place},\mbox{situation}) \ \Rightarrow \ \mbox{hand\_at}(\mbox{another\_place},\mbox{go}(\mbox{another\_place},\mbox{situation}))\qquad\mbox{cnf}(\mbox{hand\_go},\mbox{axiom})$

$\neg\,\mbox{held}(\mbox{thing},\mbox{let\_go}(\mbox{situation}))\qquad\mbox{cnf}(\mbox{cant\_hold\_and\_let\_go},\mbox{axiom})$

$\mbox{at}(\mbox{thing},\mbox{here},\mbox{situation}) \ \Rightarrow \ \mbox{red}(\mbox{thing})\qquad\mbox{cnf}(\mbox{everything\_is\_red},\mbox{axiom})$

$\mbox{at}(\mbox{thing},\mbox{place},\mbox{situation}) \ \Rightarrow \ \mbox{at}(\mbox{thing},\mbox{place},\mbox{let\_go}(\mbox{situation}))\qquad\mbox{cnf}(\mbox{situation\_let\_go},\mbox{axiom})$

$\mbox{at}(\mbox{thing},\mbox{place},\mbox{situation}) \ \Rightarrow \ \mbox{at}(\mbox{thing},\mbox{place},\mbox{pick\_up}(\mbox{situation}))\qquad\mbox{cnf}(\mbox{situation\_pick\_up},\mbox{axiom})$

$\mbox{at}(\mbox{thing},\mbox{place},\mbox{situation}) \ \Rightarrow \ \mbox{grabbed}(\mbox{thing},\mbox{pick\_up}(\mbox{go}(\mbox{place},\mbox{let\_go}(\mbox{situation}))))\qquad\mbox{cnf}(\mbox{can\_grab\_if\_previously\_let\_go},\mbox{axiom})$

$( \mbox{red}(\mbox{thing})\mbox{ and }\mbox{put}(\mbox{thing},\mbox{there},\mbox{situation}) ) \ \Rightarrow \ \mbox{answer}(\mbox{situation})\qquad\mbox{cnf}(\mbox{answer\_if\_red\_and\_put\_there},\mbox{axiom})$

$( \mbox{at}(\mbox{thing},\mbox{place},\mbox{situation})\mbox{ and }\mbox{grabbed}(\mbox{thing},\mbox{situation}) ) \ \Rightarrow \ \mbox{put}(\mbox{thing},\mbox{another\_place},\mbox{go}(\mbox{another\_place},\mbox{situation}))\qquad\mbox{cnf}(\mbox{can\_put\_somewhere\_if\_grab\_and\_go\_there},\mbox{axiom})$

$\mbox{at}(\mbox{thing},\mbox{place},\mbox{situation}) \ \Rightarrow \ ( \mbox{held}(\mbox{thing},\mbox{situation})\mbox{ or }\mbox{at}(\mbox{thing},\mbox{place},\mbox{go}(\mbox{another\_place},\mbox{situation})) )\qquad\mbox{cnf}(\mbox{thing\_either\_held\_or\_went\_there},\mbox{axiom})$

$( \mbox{hand\_at}(\mbox{one\_place},\mbox{situation})\mbox{ and }\mbox{held}(\mbox{thing},\mbox{situation}) ) \ \Rightarrow \ \mbox{at}(\mbox{thing},\mbox{place},\mbox{go}(\mbox{place},\mbox{situation}))\qquad\mbox{cnf}(\mbox{thing\_goes\_in\_hand},\mbox{axiom})$

$( \mbox{hand\_at}(\mbox{place},\mbox{situation})\mbox{ and }\mbox{at}(\mbox{thing},\mbox{place},\mbox{situation}) ) \ \Rightarrow \ \mbox{held}(\mbox{thing},\mbox{pick\_up}(\mbox{situation}))\qquad\mbox{cnf}(\mbox{thing\_picked\_up\_by\_hand},\mbox{axiom})$

$\neg\,\mbox{answer}(\mbox{situation})\qquad\mbox{cnf}(\mbox{prove\_there\_is\_an\_answer\_situation},\mbox{negated\_conjecture})$

\medskip\textbf{MSC025$\wedge$2.p} Nik's Challenge

Force the \$i type to only have two elements, then conjecture the
 existence of a bijection between \$o and \$i.




$1{:}\;\mbox{\$i}\qquad\mbox{thf}(\mbox{one},\mbox{type})$

$\mbox{two}{:}\;\mbox{\$i}\qquad\mbox{thf}(\mbox{two},\mbox{type})$

$\forall x{:}\;\mbox{\$i}{:}\;( x = 1\mbox{ or }x = \mbox{two} )\qquad\mbox{thf}(\mbox{binarity\_exhaust},\mbox{axiom})$

$1\ne \mbox{two}\qquad\mbox{thf}(\mbox{binarity\_distinc},\mbox{axiom})$

$b_1{:}\;\mbox{\$o}\to \mbox{\$i}\qquad\mbox{thf}(\mbox{b1\_ty},\mbox{type})$

$\forall x{:}\;\mbox{\$o}{:}\;( ( x \ \Rightarrow \ ( b_1@ x ) = 1 )\mbox{ and }( \neg\,x \ \Rightarrow \ ( b_1@ x ) = \mbox{two} ) )\qquad\mbox{thf}(b_1,\mbox{axiom})$

$b_2{:}\;\mbox{\$o}\to \mbox{\$i}\qquad\mbox{thf}(\mbox{b2\_ty},\mbox{type})$

$\forall x{:}\;\mbox{\$o}{:}\;( ( x \ \Rightarrow \ ( b_2@ x ) = \mbox{two} )\mbox{ and }( \neg\,x \ \Rightarrow \ ( b_2@ x ) = 1 ) )\qquad\mbox{thf}(b_2,\mbox{axiom})$

$\forall f{:}\;\mbox{\$o}\to \mbox{\$i}{:}\;( \forall x{:}\;\mbox{\$o}{:}\;( f@ x )\ne ( f@ \neg\,x ) \ \Rightarrow \ ( f = b_1\mbox{ or }f = b_2 ) )\qquad\mbox{thf}(\mbox{goal},\mbox{conjecture})$

\medskip\textbf{MSC009-1.p} Definitions of a family structure






$\mbox{female}(x) \ \Rightarrow \ \neg\,\mbox{male}(x)\qquad\mbox{cnf}(\mbox{female}_1,\mbox{negated\_conjecture})$

$\mbox{male}(x)\mbox{ or }\mbox{female}(x)\qquad\mbox{cnf}(\mbox{female}_2,\mbox{negated\_conjecture})$

$\mbox{person}(x) \ \Rightarrow \ \mbox{sex}(x,\mbox{sex\_of}_1(x))\qquad\mbox{cnf}(\mbox{person}_1,\mbox{negated\_conjecture})$

$\mbox{person}(x) \ \Rightarrow \ ( \mbox{male}(\mbox{sex\_of}_1(x))\mbox{ or }\mbox{female}(\mbox{sex\_of}_1(x)) )\qquad\mbox{cnf}(\mbox{person}_2,\mbox{negated\_conjecture})$

$( \mbox{sex}(x,y)\mbox{ and }\mbox{male}(y) ) \ \Rightarrow \ \mbox{person}(x)\qquad\mbox{cnf}(\mbox{person}_3,\mbox{negated\_conjecture})$

$( \mbox{sex}(x,y)\mbox{ and }\mbox{female}(y) ) \ \Rightarrow \ \mbox{person}(x)\qquad\mbox{cnf}(\mbox{person}_4,\mbox{negated\_conjecture})$

$\mbox{parent}(x) \ \Rightarrow \ \mbox{person}(x)\qquad\mbox{cnf}(\mbox{parent}_1,\mbox{negated\_conjecture})$

$\mbox{parent}(x) \ \Rightarrow \ \mbox{child}(x,\mbox{child\_of}_1(x))\qquad\mbox{cnf}(\mbox{parent}_2,\mbox{negated\_conjecture})$

$\mbox{parent}(x) \ \Rightarrow \ \mbox{person}(\mbox{child\_of}_1(x))\qquad\mbox{cnf}(\mbox{parent}_3,\mbox{negated\_conjecture})$

$( \mbox{person}(x)\mbox{ and }\mbox{child}(x,y)\mbox{ and }\mbox{person}(y) ) \ \Rightarrow \ \mbox{parent}(x)\qquad\mbox{cnf}(\mbox{parent}_4,\mbox{negated\_conjecture})$

$\mbox{mother}(x) \ \Rightarrow \ \mbox{parent}(x)\qquad\mbox{cnf}(\mbox{mother}_1,\mbox{negated\_conjecture})$

$\mbox{mother}(x) \ \Rightarrow \ \mbox{sex}(x,\mbox{sex\_of}_2(x))\qquad\mbox{cnf}(\mbox{mother}_2,\mbox{negated\_conjecture})$

$\mbox{mother}(x) \ \Rightarrow \ \mbox{female}(\mbox{sex\_of}_2(x))\qquad\mbox{cnf}(\mbox{mother}_3,\mbox{negated\_conjecture})$

$( \mbox{parent}(x)\mbox{ and }\mbox{sex}(x,y)\mbox{ and }\mbox{female}(y) ) \ \Rightarrow \ \mbox{mother}(x)\qquad\mbox{cnf}(\mbox{mother}_4,\mbox{negated\_conjecture})$

$\mbox{father}(x) \ \Rightarrow \ \mbox{parent}(x)\qquad\mbox{cnf}(\mbox{father}_1,\mbox{negated\_conjecture})$

$\mbox{father}(x) \ \Rightarrow \ \neg\,\mbox{mother}(x)\qquad\mbox{cnf}(\mbox{father}_2,\mbox{negated\_conjecture})$

$\mbox{parent}(x) \ \Rightarrow \ ( \mbox{mother}(x)\mbox{ or }\mbox{father}(x) )\qquad\mbox{cnf}(\mbox{father}_3,\mbox{negated\_conjecture})$

$\mbox{grandparent}(x) \ \Rightarrow \ \mbox{parent}(x)\qquad\mbox{cnf}(\mbox{grandparent}_1,\mbox{negated\_conjecture})$

$\mbox{grandparent}(x) \ \Rightarrow \ \mbox{child}(x,\mbox{child\_of}_2(x))\qquad\mbox{cnf}(\mbox{grandparent}_2,\mbox{negated\_conjecture})$

$\mbox{grandparent}(x) \ \Rightarrow \ \mbox{parent}(\mbox{child\_of}_2(x))\qquad\mbox{cnf}(\mbox{grandparent}_3,\mbox{negated\_conjecture})$

$( \mbox{parent}(x)\mbox{ and }\mbox{child}(x,y)\mbox{ and }\mbox{parent}(y) ) \ \Rightarrow \ \mbox{grandparent}(x)\qquad\mbox{cnf}(\mbox{grandparent}_4,\mbox{negated\_conjecture})$

$\mbox{parent\_with\_sons\_only}(x) \ \Rightarrow \ \mbox{parent}(x)\qquad\mbox{cnf}(\mbox{parent\_with\_sons\_only}_1,\mbox{negated\_conjecture})$

$( \mbox{parent\_with\_sons\_only}(x)\mbox{ and }\mbox{child}(x,y) ) \ \Rightarrow \ \mbox{child\_with\_parent}(y)\qquad\mbox{cnf}(\mbox{parent\_with\_sons\_only}_2,\mbox{negated\_conjecture})$

$\mbox{parent}(x) \ \Rightarrow \ ( \mbox{child}(x,\mbox{female\_child\_of}(x))\mbox{ or }\mbox{parent\_with\_sons\_only}(x) )\qquad\mbox{cnf}(\mbox{parent\_with\_sons\_only}_3,\mbox{negated\_conjecture})$

$( \mbox{parent}(x)\mbox{ and }\mbox{child\_with\_parent}(\mbox{female\_child\_of}(x)) ) \ \Rightarrow \ \mbox{parent\_with\_sons\_only}(x)\qquad\mbox{cnf}(\mbox{parent\_with\_sons\_only}_4,\mbox{negated\_conjecture})$

$\mbox{child\_with\_parent}(y) \ \Rightarrow \ \mbox{sex}(y,\mbox{sex\_of}_3(y))\qquad\mbox{cnf}(\mbox{parent\_with\_sons\_only}_5,\mbox{negated\_conjecture})$

$\mbox{child\_with\_parent}(y) \ \Rightarrow \ \mbox{male}(\mbox{sex\_of}_3(y))\qquad\mbox{cnf}(\mbox{parent\_with\_sons\_only}_6,\mbox{negated\_conjecture})$

$( \mbox{sex}(y,z)\mbox{ and }\mbox{male}(z) ) \ \Rightarrow \ \mbox{child\_with\_parent}(y)\qquad\mbox{cnf}(\mbox{parent\_with\_sons\_only}_7,\mbox{negated\_conjecture})$

\medskip\textbf{MSC011+1.p} Drinker paradox






$\forall a{:}\;( ( \mbox{drunk}(a)\mbox{ and }\mbox{not\_drunk}(a) ) \ \Rightarrow \ \mbox{goal} )\qquad\mbox{fof}(\mbox{d\_cons},\mbox{axiom})$

$\forall a{:}\;( \mbox{drunk}(a)\mbox{ and }\mbox{neg\_psi} )\qquad\mbox{fof}(\mbox{neg\_phi},\mbox{axiom})$

$\mbox{neg\_psi} \ \Rightarrow \ \exists a{:}\;\mbox{not\_drunk}(a)\qquad\mbox{fof}(\mbox{neg\_psi\_ax},\mbox{axiom})$

$\mbox{goal}\qquad\mbox{fof}(\mbox{goal\_to\_be\_proved},\mbox{conjecture})$

\medskip\textbf{MSC027-1.p} Sets, numbers, lists, etc, that make up the Isabelle/HOL library






$\mbox{include}(\mbox{'Axioms/MSC001-0.ax'})$

$\mbox{include}(\mbox{'Axioms/MSC001-2.ax'})$

\medskip\textbf{MSC015-1.015.p} Binary counter k=15

Each instance of the problem asserts
 p(0*).                 // p[0]
 p(x*01*) $\to$ p(x*10*).  // p[i] $\to$ p[i + 1]
 not p(1*).             // not p[2$\wedge$n - 1]
 These problems are unsatisfiable and have exponentially large
 propositional resolution refutations, while there is a short
 (quadratic) first order refutation.




$p(s_0,s_0,s_0,s_0,s_0,s_0,s_0,s_0,s_0,s_0,s_0,s_0,s_0,s_0,s_0)\qquad\mbox{cnf}(\mbox{init},\mbox{axiom})$

$p(x_0,x_1,x_2,x_3,x_4,x_5,x_6,x_7,x_8,x_9,x_{10},x_{11},x_{12},x_{13},s_0) \ \Rightarrow \ p(x_0,x_1,x_2,x_3,x_4,x_5,x_6,x_7,x_8,x_9,x_{10},x_{11},x_{12},x_{13},s_1)\qquad\mbox{cnf}(\mbox{rule}_1,\mbox{axiom})$

$p(x_0,x_1,x_2,x_3,x_4,x_5,x_6,x_7,x_8,x_9,x_{10},x_{11},x_{12},s_0,s_1) \ \Rightarrow \ p(x_0,x_1,x_2,x_3,x_4,x_5,x_6,x_7,x_8,x_9,x_{10},x_{11},x_{12},s_1,s_0)\qquad\mbox{cnf}(\mbox{rule}_2,\mbox{axiom})$

$p(x_0,x_1,x_2,x_3,x_4,x_5,x_6,x_7,x_8,x_9,x_{10},x_{11},s_0,s_1,s_1) \ \Rightarrow \ p(x_0,x_1,x_2,x_3,x_4,x_5,x_6,x_7,x_8,x_9,x_{10},x_{11},s_1,s_0,s_0)\qquad\mbox{cnf}(\mbox{rule}_3,\mbox{axiom})$

$p(x_0,x_1,x_2,x_3,x_4,x_5,x_6,x_7,x_8,x_9,x_{10},s_0,s_1,s_1,s_1) \ \Rightarrow \ p(x_0,x_1,x_2,x_3,x_4,x_5,x_6,x_7,x_8,x_9,x_{10},s_1,s_0,s_0,s_0)\qquad\mbox{cnf}(\mbox{rule}_4,\mbox{axiom})$

$p(x_0,x_1,x_2,x_3,x_4,x_5,x_6,x_7,x_8,x_9,s_0,s_1,s_1,s_1,s_1) \ \Rightarrow \ p(x_0,x_1,x_2,x_3,x_4,x_5,x_6,x_7,x_8,x_9,s_1,s_0,s_0,s_0,s_0)\qquad\mbox{cnf}(\mbox{rule}_5,\mbox{axiom})$

$p(x_0,x_1,x_2,x_3,x_4,x_5,x_6,x_7,x_8,s_0,s_1,s_1,s_1,s_1,s_1) \ \Rightarrow \ p(x_0,x_1,x_2,x_3,x_4,x_5,x_6,x_7,x_8,s_1,s_0,s_0,s_0,s_0,s_0)\qquad\mbox{cnf}(\mbox{rule}_6,\mbox{axiom})$

$p(x_0,x_1,x_2,x_3,x_4,x_5,x_6,x_7,s_0,s_1,s_1,s_1,s_1,s_1,s_1) \ \Rightarrow \ p(x_0,x_1,x_2,x_3,x_4,x_5,x_6,x_7,s_1,s_0,s_0,s_0,s_0,s_0,s_0)\qquad\mbox{cnf}(\mbox{rule}_7,\mbox{axiom})$

$p(x_0,x_1,x_2,x_3,x_4,x_5,x_6,s_0,s_1,s_1,s_1,s_1,s_1,s_1,s_1) \ \Rightarrow \ p(x_0,x_1,x_2,x_3,x_4,x_5,x_6,s_1,s_0,s_0,s_0,s_0,s_0,s_0,s_0)\qquad\mbox{cnf}(\mbox{rule}_8,\mbox{axiom})$

$p(x_0,x_1,x_2,x_3,x_4,x_5,s_0,s_1,s_1,s_1,s_1,s_1,s_1,s_1,s_1) \ \Rightarrow \ p(x_0,x_1,x_2,x_3,x_4,x_5,s_1,s_0,s_0,s_0,s_0,s_0,s_0,s_0,s_0)\qquad\mbox{cnf}(\mbox{rule}_9,\mbox{axiom})$

$p(x_0,x_1,x_2,x_3,x_4,s_0,s_1,s_1,s_1,s_1,s_1,s_1,s_1,s_1,s_1) \ \Rightarrow \ p(x_0,x_1,x_2,x_3,x_4,s_1,s_0,s_0,s_0,s_0,s_0,s_0,s_0,s_0,s_0)\qquad\mbox{cnf}(\mbox{rule}_{10},\mbox{axiom})$

$p(x_0,x_1,x_2,x_3,s_0,s_1,s_1,s_1,s_1,s_1,s_1,s_1,s_1,s_1,s_1) \ \Rightarrow \ p(x_0,x_1,x_2,x_3,s_1,s_0,s_0,s_0,s_0,s_0,s_0,s_0,s_0,s_0,s_0)\qquad\mbox{cnf}(\mbox{rule}_{11},\mbox{axiom})$

$p(x_0,x_1,x_2,s_0,s_1,s_1,s_1,s_1,s_1,s_1,s_1,s_1,s_1,s_1,s_1) \ \Rightarrow \ p(x_0,x_1,x_2,s_1,s_0,s_0,s_0,s_0,s_0,s_0,s_0,s_0,s_0,s_0,s_0)\qquad\mbox{cnf}(\mbox{rule}_{12},\mbox{axiom})$

$p(x_0,x_1,s_0,s_1,s_1,s_1,s_1,s_1,s_1,s_1,s_1,s_1,s_1,s_1,s_1) \ \Rightarrow \ p(x_0,x_1,s_1,s_0,s_0,s_0,s_0,s_0,s_0,s_0,s_0,s_0,s_0,s_0,s_0)\qquad\mbox{cnf}(\mbox{rule}_{13},\mbox{axiom})$

$p(x_0,s_0,s_1,s_1,s_1,s_1,s_1,s_1,s_1,s_1,s_1,s_1,s_1,s_1,s_1) \ \Rightarrow \ p(x_0,s_1,s_0,s_0,s_0,s_0,s_0,s_0,s_0,s_0,s_0,s_0,s_0,s_0,s_0)\qquad\mbox{cnf}(\mbox{rule}_{14},\mbox{axiom})$

$p(s_0,s_1,s_1,s_1,s_1,s_1,s_1,s_1,s_1,s_1,s_1,s_1,s_1,s_1,s_1) \ \Rightarrow \ p(s_1,s_0,s_0,s_0,s_0,s_0,s_0,s_0,s_0,s_0,s_0,s_0,s_0,s_0,s_0)\qquad\mbox{cnf}(\mbox{rule}_{15},\mbox{axiom})$

$\neg\,p(s_1,s_1,s_1,s_1,s_1,s_1,s_1,s_1,s_1,s_1,s_1,s_1,s_1,s_1,s_1)\qquad\mbox{cnf}(\mbox{goal},\mbox{negated\_conjecture})$

\medskip\textbf{MSC015-1.005.p} Binary counter k=05

Each instance of the problem asserts
 p(0*).                 // p[0]
 p(x*01*) $\to$ p(x*10*).  // p[i] $\to$ p[i + 1]
 not p(1*).             // not p[2$\wedge$n - 1]
 These problems are unsatisfiable and have exponentially large
 propositional resolution refutations, while there is a short
 (quadratic) first order refutation.




$p(s_0,s_0,s_0,s_0,s_0)\qquad\mbox{cnf}(\mbox{init},\mbox{axiom})$

$p(x_0,x_1,x_2,x_3,s_0) \ \Rightarrow \ p(x_0,x_1,x_2,x_3,s_1)\qquad\mbox{cnf}(\mbox{rule}_1,\mbox{axiom})$

$p(x_0,x_1,x_2,s_0,s_1) \ \Rightarrow \ p(x_0,x_1,x_2,s_1,s_0)\qquad\mbox{cnf}(\mbox{rule}_2,\mbox{axiom})$

$p(x_0,x_1,s_0,s_1,s_1) \ \Rightarrow \ p(x_0,x_1,s_1,s_0,s_0)\qquad\mbox{cnf}(\mbox{rule}_3,\mbox{axiom})$

$p(x_0,s_0,s_1,s_1,s_1) \ \Rightarrow \ p(x_0,s_1,s_0,s_0,s_0)\qquad\mbox{cnf}(\mbox{rule}_4,\mbox{axiom})$

$p(s_0,s_1,s_1,s_1,s_1) \ \Rightarrow \ p(s_1,s_0,s_0,s_0,s_0)\qquad\mbox{cnf}(\mbox{rule}_5,\mbox{axiom})$

$\neg\,p(s_1,s_1,s_1,s_1,s_1)\qquad\mbox{cnf}(\mbox{goal},\mbox{negated\_conjecture})$

\medskip\textbf{MSC023=2.p} Fahrenheit 451 to Celcius conversion






$\mbox{celsius\_fahrenheit\_temperature\_conversion}{:}\;( \mbox{\$real}\times \mbox{\$real} )\to \mbox{\$o}\qquad\mbox{tff}(\mbox{celsius\_fahrenheit\_temperature\_conversion\_type},\mbox{type})$

$\forall c{:}\;\mbox{\$real},f{:}\;\mbox{\$real}{:}\;( \mbox{\$sum}(\mbox{\$product}(\mbox{1.}_8,c),\mbox{32.}_0) = f \ \Rightarrow \ \mbox{celsius\_fahrenheit\_temperature\_conversion}(c,f) )\qquad\mbox{tff}(\mbox{celsius\_fahrenheit\_temperature\_conversion},\mbox{axiom})$

$\exists c{:}\;\mbox{\$real}{:}\;\mbox{celsius\_fahrenheit\_temperature\_conversion}(c,\mbox{451.}_0)\qquad\mbox{tff}(\mbox{fahrenheit\_451\_to\_celsius},\mbox{conjecture})$

\medskip\textbf{MSC007$\wedge$1.003.004.p} Cook pigeon-hole problem, 4 pigeons and 3 holes

Suppose there are N holes and more pigeons to put in the
 holes. Every pigeon is in a hole and no hole contains more
 than one pigeon. Prove that some pigoen has no hole.




$\mbox{hole}{:}\;\mbox{\$tType}\qquad\mbox{thf}(\mbox{hole},\mbox{type})$

$\mbox{pigeon}{:}\;\mbox{\$tType}\qquad\mbox{thf}(\mbox{pigeon},\mbox{type})$

$\mbox{hole}_1{:}\;\mbox{hole}\qquad\mbox{thf}(\mbox{hole}_1,\mbox{type})$

$\mbox{hole}_2{:}\;\mbox{hole}\qquad\mbox{thf}(\mbox{hole}_2,\mbox{type})$

$\mbox{hole}_3{:}\;\mbox{hole}\qquad\mbox{thf}(\mbox{hole}_3,\mbox{type})$

$\mbox{pigeon}_1{:}\;\mbox{pigeon}\qquad\mbox{thf}(\mbox{pigeon}_1,\mbox{type})$

$\mbox{pigeon}_2{:}\;\mbox{pigeon}\qquad\mbox{thf}(\mbox{pigeon}_2,\mbox{type})$

$\mbox{pigeon}_3{:}\;\mbox{pigeon}\qquad\mbox{thf}(\mbox{pigeon}_3,\mbox{type})$

$\mbox{pigeon}_4{:}\;\mbox{pigeon}\qquad\mbox{thf}(\mbox{pigeon}_4,\mbox{type})$

$\mbox{pigeon\_hole}{:}\;\mbox{pigeon}\to \mbox{hole}\qquad\mbox{thf}(\mbox{pigeon\_hole\_t},\mbox{type})$

$\forall p{:}\;\mbox{hole}\to \mbox{\$o}{:}\;( ( p@ \mbox{hole}_1\mbox{ and }p@ \mbox{hole}_2\mbox{ and }p@ \mbox{hole}_3 ) \ \Rightarrow \ \forall x{:}\;\mbox{hole}{:}\;( p@ x ) )\qquad\mbox{thf}(\mbox{holecover},\mbox{axiom})$

$\mbox{pigeon}_1\ne \mbox{pigeon}_2\qquad\mbox{thf}(\mbox{pigeon1pigeon}_2,\mbox{axiom})$

$\mbox{pigeon}_1\ne \mbox{pigeon}_3\qquad\mbox{thf}(\mbox{pigeon1pigeon}_3,\mbox{axiom})$

$\mbox{pigeon}_2\ne \mbox{pigeon}_3\qquad\mbox{thf}(\mbox{pigeon2pigeon}_3,\mbox{axiom})$

$\mbox{pigeon}_1\ne \mbox{pigeon}_4\qquad\mbox{thf}(\mbox{pigeon1pigeon}_4,\mbox{axiom})$

$\mbox{pigeon}_2\ne \mbox{pigeon}_4\qquad\mbox{thf}(\mbox{pigeon2pigeon}_4,\mbox{axiom})$

$\mbox{pigeon}_3\ne \mbox{pigeon}_4\qquad\mbox{thf}(\mbox{pigeon3pigeon}_4,\mbox{axiom})$

$\exists x{:}\;\mbox{pigeon},y{:}\;\mbox{pigeon}{:}\;( ( \mbox{pigeon\_hole}@ x ) = ( \mbox{pigeon\_hole}@ y )\mbox{ and }x\ne y )\qquad\mbox{thf}(\mbox{sharing\_a\_hole},\mbox{conjecture})$

\medskip\textbf{MSC009+1.p} Definitions of a family structure






$\forall x{:}\;( \mbox{female}(x)\iff \neg\,\mbox{male}(x) )\qquad\mbox{fof}(\mbox{female},\mbox{axiom})$

$\forall x{:}\;( \mbox{person}(x)\iff \exists y{:}\;( \mbox{sex}(x,y)\mbox{ and }( \mbox{male}(y)\mbox{ or }\mbox{female}(y) ) ) )\qquad\mbox{fof}(\mbox{person},\mbox{axiom})$

$\forall x{:}\;( \mbox{parent}(x)\iff ( \mbox{person}(x)\mbox{ and }\exists y{:}\;( \mbox{child}(x,y)\mbox{ and }\mbox{person}(y) ) ) )\qquad\mbox{fof}(\mbox{parent},\mbox{axiom})$

$\forall x{:}\;( \mbox{mother}(x)\iff ( \mbox{parent}(x)\mbox{ and }\exists y{:}\;( \mbox{sex}(x,y)\mbox{ and }\mbox{female}(y) ) ) )\qquad\mbox{fof}(\mbox{mother},\mbox{axiom})$

$\forall x{:}\;( \mbox{father}(x)\iff ( \mbox{parent}(x)\mbox{ and }\neg\,\mbox{mother}(x) ) )\qquad\mbox{fof}(\mbox{father},\mbox{axiom})$

$\forall x{:}\;( \mbox{grandparent}(x)\iff ( \mbox{parent}(x)\mbox{ and }\exists y{:}\;( \mbox{child}(x,y)\mbox{ and }\mbox{parent}(y) ) ) )\qquad\mbox{fof}(\mbox{grandparent},\mbox{axiom})$

$\forall x{:}\;( \mbox{parent\_with\_sons\_only}(x)\iff ( \mbox{parent}(x)\mbox{ and }\forall y{:}\;( \mbox{child}(x,y) \ \Rightarrow \ \exists z{:}\;( \mbox{sex}(y,z)\mbox{ and }\mbox{male}(z) ) ) ) )\qquad\mbox{fof}(\mbox{parent\_with\_sons\_only},\mbox{axiom})$

\medskip\textbf{MSC006-1.p} A "non-obvious" problem

Suppose there are two relations, P and Q. P is transitive, and
 Q is both transitive and symmetric. Suppose further the
 "squareness" of P and Q: any two things are related either in
 the P manner or the Q manner. Prove that either P is total or
 Q is total.




$( p(x,y)\mbox{ and }p(y,z) ) \ \Rightarrow \ p(x,z)\qquad\mbox{cnf}(\mbox{p\_transitivity},\mbox{hypothesis})$

$( q(x,y)\mbox{ and }q(y,z) ) \ \Rightarrow \ q(x,z)\qquad\mbox{cnf}(\mbox{q\_transitivity},\mbox{hypothesis})$

$q(x,y) \ \Rightarrow \ q(y,x)\qquad\mbox{cnf}(\mbox{q\_symmetry},\mbox{hypothesis})$

$p(x,y)\mbox{ or }q(x,y)\qquad\mbox{cnf}(\mbox{all\_related},\mbox{hypothesis})$

$\neg\,p(a,b)\qquad\mbox{cnf}(\mbox{p\_is\_not\_total},\mbox{hypothesis})$

$\neg\,q(c,d)\qquad\mbox{cnf}(\mbox{prove\_q\_is\_total},\mbox{negated\_conjecture})$

\medskip\textbf{MSC012+1.p} A serial and transitive relation inconsistent for non-empty domain






$\forall a,b{:}\;( ( p(a)\mbox{ and }\mbox{less}(a,b)\mbox{ and }p(b) ) \ \Rightarrow \ \mbox{goal} )\qquad\mbox{fof}(\mbox{left\_to\_right},\mbox{axiom})$

$\forall a{:}\;( p(a)\mbox{ or }\exists b{:}\;( \mbox{less}(a,b)\mbox{ and }p(b) ) )\qquad\mbox{fof}(\mbox{right\_to\_left},\mbox{axiom})$

$\forall a,b,c{:}\;( ( \mbox{less}(a,b)\mbox{ and }\mbox{less}(b,c) ) \ \Rightarrow \ \mbox{less}(a,c) )\qquad\mbox{fof}(\mbox{transitive\_less},\mbox{axiom})$

$\forall a{:}\;\exists b{:}\;\mbox{less}(a,b)\qquad\mbox{fof}(\mbox{serial\_less},\mbox{axiom})$

$\mbox{goal}\qquad\mbox{fof}(\mbox{goal\_to\_be\_proved},\mbox{conjecture})$

\medskip\textbf{MSC025$\wedge$1.p} Nik's Challenge

Force the \$i type to only have two elements, then conjecture the
 existence of a bijection between \$o and \$i.




$1{:}\;\mbox{\$i}\qquad\mbox{thf}(\mbox{one},\mbox{type})$

$\mbox{two}{:}\;\mbox{\$i}\qquad\mbox{thf}(\mbox{two},\mbox{type})$

$\forall x{:}\;\mbox{\$i}{:}\;( x = 1\mbox{ or }x = \mbox{two} )\qquad\mbox{thf}(\mbox{binary\_exhaust},\mbox{axiom})$

$1\ne \mbox{two}\qquad\mbox{thf}(\mbox{binary\_distinc},\mbox{axiom})$

$\exists f{:}\;\mbox{\$o}\to \mbox{\$i}{:}\;\forall x{:}\;\mbox{\$o}{:}\;( f@ x )\ne ( f@ \neg\,x )\qquad\mbox{thf}(\mbox{goal},\mbox{conjecture})$

\medskip\textbf{MSC002-2.p} A Blind Hand Problem






$\mbox{at}(\mbox{something},\mbox{here},\mbox{now})\qquad\mbox{cnf}(\mbox{something\_is\_here\_now},\mbox{axiom})$

$\neg\,\mbox{held}(\mbox{thing},\mbox{let\_go}(\mbox{situation}))\qquad\mbox{cnf}(\mbox{cant\_hold\_and\_let\_go},\mbox{axiom})$

$\mbox{at}(\mbox{thing},\mbox{here},\mbox{situation}) \ \Rightarrow \ \mbox{red}(\mbox{thing})\qquad\mbox{cnf}(\mbox{everything\_is\_red},\mbox{axiom})$

$\mbox{at}(\mbox{thing},\mbox{place},\mbox{situation}) \ \Rightarrow \ \mbox{at}(\mbox{thing},\mbox{place},\mbox{let\_go}(\mbox{situation}))\qquad\mbox{cnf}(\mbox{situation\_let\_go},\mbox{axiom})$

$\mbox{at}(\mbox{thing},\mbox{place},\mbox{situation}) \ \Rightarrow \ \mbox{at}(\mbox{thing},\mbox{place},\mbox{pick\_up}(\mbox{situation}))\qquad\mbox{cnf}(\mbox{situation\_pick\_up},\mbox{axiom})$

$\mbox{at}(\mbox{thing},\mbox{place},\mbox{situation}) \ \Rightarrow \ \mbox{grabbed}(\mbox{thing},\mbox{pick\_up}(\mbox{go}(\mbox{place},\mbox{let\_go}(\mbox{situation}))))\qquad\mbox{cnf}(\mbox{can\_grab\_if\_previously\_let\_go},\mbox{axiom})$

$( \mbox{red}(\mbox{thing})\mbox{ and }\mbox{put}(\mbox{thing},\mbox{there},\mbox{situation}) ) \ \Rightarrow \ \mbox{answer}(\mbox{situation})\qquad\mbox{cnf}(\mbox{answer\_if\_red\_and\_put\_there},\mbox{axiom})$

$( \mbox{at}(\mbox{thing},\mbox{place},\mbox{situation})\mbox{ and }\mbox{grabbed}(\mbox{thing},\mbox{situation}) ) \ \Rightarrow \ \mbox{put}(\mbox{thing},\mbox{another\_place},\mbox{go}(\mbox{another\_place},\mbox{situation}))\qquad\mbox{cnf}(\mbox{can\_put\_somewhere\_if\_grab\_and\_go\_there},\mbox{axiom})$

$\mbox{at}(\mbox{thing},\mbox{place},\mbox{situation}) \ \Rightarrow \ ( \mbox{held}(\mbox{thing},\mbox{situation})\mbox{ or }\mbox{at}(\mbox{thing},\mbox{place},\mbox{go}(\mbox{another\_place},\mbox{situation})) )\qquad\mbox{cnf}(\mbox{thing\_either\_held\_or\_went\_there},\mbox{axiom})$

$\neg\,\mbox{answer}(\mbox{situation})\qquad\mbox{cnf}(\mbox{prove\_there\_is\_an\_answer\_situation},\mbox{negated\_conjecture})$

\medskip\textbf{MSC007-2.005.p} Cook pigeon-hole problem

Suppose there are N holes and N+1 pigeons to put in the
 holes. Every pigeon is in a hole and no hole contains more
 than one pigeon. Prove that this is impossible. The size is
 the number of pigeons.




$x = x\qquad\mbox{cnf}(\mbox{reflexivity},\mbox{axiom})$

$x = y \ \Rightarrow \ y = x\qquad\mbox{cnf}(\mbox{symmetry},\mbox{axiom})$

$( x = y\mbox{ and }y = z ) \ \Rightarrow \ x = z\qquad\mbox{cnf}(\mbox{transitivity},\mbox{axiom})$

$\mbox{pigeon}(\mbox{pigeon}_1)\qquad\mbox{cnf}(\mbox{pigeon}_1,\mbox{axiom})$

$\mbox{pigeon}(\mbox{pigeon}_2)\qquad\mbox{cnf}(\mbox{pigeon}_2,\mbox{axiom})$

$\mbox{pigeon}(\mbox{pigeon}_3)\qquad\mbox{cnf}(\mbox{pigeon}_3,\mbox{axiom})$

$\mbox{pigeon}(\mbox{pigeon}_4)\qquad\mbox{cnf}(\mbox{pigeon}_4,\mbox{axiom})$

$\mbox{pigeon}(\mbox{pigeon}_5)\qquad\mbox{cnf}(\mbox{pigeon}_5,\mbox{axiom})$

$\mbox{pigeon}_1\ne \mbox{pigeon}_2\qquad\mbox{cnf}(\mbox{pigeon\_1\_is\_not\_pigeon}_2,\mbox{axiom})$

$\mbox{pigeon}_1\ne \mbox{pigeon}_3\qquad\mbox{cnf}(\mbox{pigeon\_1\_is\_not\_pigeon}_3,\mbox{axiom})$

$\mbox{pigeon}_1\ne \mbox{pigeon}_4\qquad\mbox{cnf}(\mbox{pigeon\_1\_is\_not\_pigeon}_4,\mbox{axiom})$

$\mbox{pigeon}_1\ne \mbox{pigeon}_5\qquad\mbox{cnf}(\mbox{pigeon\_1\_is\_not\_pigeon}_5,\mbox{axiom})$

$\mbox{pigeon}_2\ne \mbox{pigeon}_3\qquad\mbox{cnf}(\mbox{pigeon\_2\_is\_not\_pigeon}_3,\mbox{axiom})$

$\mbox{pigeon}_2\ne \mbox{pigeon}_4\qquad\mbox{cnf}(\mbox{pigeon\_2\_is\_not\_pigeon}_4,\mbox{axiom})$

$\mbox{pigeon}_2\ne \mbox{pigeon}_5\qquad\mbox{cnf}(\mbox{pigeon\_2\_is\_not\_pigeon}_5,\mbox{axiom})$

$\mbox{pigeon}_3\ne \mbox{pigeon}_4\qquad\mbox{cnf}(\mbox{pigeon\_3\_is\_not\_pigeon}_4,\mbox{axiom})$

$\mbox{pigeon}_3\ne \mbox{pigeon}_5\qquad\mbox{cnf}(\mbox{pigeon\_3\_is\_not\_pigeon}_5,\mbox{axiom})$

$\mbox{pigeon}_4\ne \mbox{pigeon}_5\qquad\mbox{cnf}(\mbox{pigeon\_4\_is\_not\_pigeon}_5,\mbox{axiom})$

$\mbox{hole}(\mbox{hole}_1)\qquad\mbox{cnf}(\mbox{hole}_1,\mbox{axiom})$

$\mbox{hole}(\mbox{hole}_2)\qquad\mbox{cnf}(\mbox{hole}_2,\mbox{axiom})$

$\mbox{hole}(\mbox{hole}_3)\qquad\mbox{cnf}(\mbox{hole}_3,\mbox{axiom})$

$\mbox{hole}(\mbox{hole}_4)\qquad\mbox{cnf}(\mbox{hole}_4,\mbox{axiom})$

$\mbox{hole}_1\ne \mbox{hole}_2\qquad\mbox{cnf}(\mbox{hole\_1\_is\_not\_hole}_2,\mbox{axiom})$

$\mbox{hole}_1\ne \mbox{hole}_3\qquad\mbox{cnf}(\mbox{hole\_1\_is\_not\_hole}_3,\mbox{axiom})$

$\mbox{hole}_1\ne \mbox{hole}_4\qquad\mbox{cnf}(\mbox{hole\_1\_is\_not\_hole}_4,\mbox{axiom})$

$\mbox{hole}_2\ne \mbox{hole}_3\qquad\mbox{cnf}(\mbox{hole\_2\_is\_not\_hole}_3,\mbox{axiom})$

$\mbox{hole}_2\ne \mbox{hole}_4\qquad\mbox{cnf}(\mbox{hole\_2\_is\_not\_hole}_4,\mbox{axiom})$

$\mbox{hole}_3\ne \mbox{hole}_4\qquad\mbox{cnf}(\mbox{hole\_3\_is\_not\_hole}_4,\mbox{axiom})$

$\mbox{hole}(\mbox{hole}) \ \Rightarrow \ ( \mbox{hole} = \mbox{hole}_1\mbox{ or }\mbox{hole} = \mbox{hole}_2\mbox{ or }\mbox{hole} = \mbox{hole}_3\mbox{ or }\mbox{hole} = \mbox{hole}_4 )\qquad\mbox{cnf}(\mbox{all\_holes},\mbox{axiom})$

$\mbox{pigeon}(x) \ \Rightarrow \ \mbox{hole}(\mbox{hole\_of}(x))\qquad\mbox{cnf}(\mbox{each\_pigeons\_hole}_1,\mbox{axiom})$

$\mbox{pigeon}(x) \ \Rightarrow \ \mbox{in}(x,\mbox{hole\_of}(x))\qquad\mbox{cnf}(\mbox{each\_pigeons\_hole}_2,\mbox{axiom})$

$( \mbox{hole}(\mbox{hole})\mbox{ and }\mbox{pigeon}(\mbox{pigeon}_1)\mbox{ and }\mbox{pigeon}(\mbox{pigeon}_2)\mbox{ and }\mbox{in}(\mbox{pigeon}_1,\mbox{hole})\mbox{ and }\mbox{in}(\mbox{pigeon}_2,\mbox{hole}) ) \ \Rightarrow \ \mbox{pigeon}_1 = \mbox{pigeon}_2\qquad\mbox{cnf}(\mbox{only\_one\_per\_hole},\mbox{negated\_conjecture})$

\medskip
\end{document}