\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{PLA001-1.ax} Blocks world difference axioms for 4 blocks






$\mbox{differ}(y,x) \ \Rightarrow \ \mbox{differ}(x,y)\qquad\mbox{cnf}(\mbox{symmetry\_of\_differ},\mbox{axiom})$

$\mbox{differ}(a,b)\qquad\mbox{cnf}(\mbox{differ\_a\_b},\mbox{axiom})$

$\mbox{differ}(a,c)\qquad\mbox{cnf}(\mbox{differ\_a\_c},\mbox{axiom})$

$\mbox{differ}(a,d)\qquad\mbox{cnf}(\mbox{differ\_a\_d},\mbox{axiom})$

$\mbox{differ}(a,\mbox{table})\qquad\mbox{cnf}(\mbox{differ\_a\_table},\mbox{axiom})$

$\mbox{differ}(b,c)\qquad\mbox{cnf}(\mbox{differ\_b\_c},\mbox{axiom})$

$\mbox{differ}(b,d)\qquad\mbox{cnf}(\mbox{differ\_b\_d},\mbox{axiom})$

$\mbox{differ}(b,\mbox{table})\qquad\mbox{cnf}(\mbox{differ\_b\_table},\mbox{axiom})$

$\mbox{differ}(c,d)\qquad\mbox{cnf}(\mbox{differ\_c\_d},\mbox{axiom})$

$\mbox{differ}(c,\mbox{table})\qquad\mbox{cnf}(\mbox{differ\_c\_table},\mbox{axiom})$

$\mbox{differ}(d,\mbox{table})\qquad\mbox{cnf}(\mbox{differ\_d\_table},\mbox{axiom})$

$\mbox{holds}(\mbox{on}(a,\mbox{table}),s_0)\qquad\mbox{cnf}(\mbox{initial\_state}_1,\mbox{axiom})$

$\mbox{holds}(\mbox{on}(b,\mbox{table}),s_0)\qquad\mbox{cnf}(\mbox{initial\_state}_2,\mbox{axiom})$

$\mbox{holds}(\mbox{on}(c,d),s_0)\qquad\mbox{cnf}(\mbox{initial\_state}_3,\mbox{axiom})$

$\mbox{holds}(\mbox{on}(d,\mbox{table}),s_0)\qquad\mbox{cnf}(\mbox{initial\_state}_4,\mbox{axiom})$

$\mbox{holds}(\mbox{clear}(a),s_0)\qquad\mbox{cnf}(\mbox{initial\_state}_5,\mbox{axiom})$

$\mbox{holds}(\mbox{clear}(b),s_0)\qquad\mbox{cnf}(\mbox{initial\_state}_6,\mbox{axiom})$

$\mbox{holds}(\mbox{clear}(c),s_0)\qquad\mbox{cnf}(\mbox{initial\_state}_7,\mbox{axiom})$

$\mbox{holds}(\mbox{empty},s_0)\qquad\mbox{cnf}(\mbox{initial\_state}_8,\mbox{axiom})$

$\mbox{holds}(\mbox{clear}(\mbox{table}),\mbox{state})\qquad\mbox{cnf}(\mbox{clear\_table},\mbox{axiom})$

\medskip\textbf{PLA001-0.ax} Blocks world axioms






$( \mbox{holds}(x,\mbox{state})\mbox{ and }\mbox{holds}(y,\mbox{state}) ) \ \Rightarrow \ \mbox{holds}(\mbox{and}(x,y),\mbox{state})\qquad\mbox{cnf}(\mbox{and\_definition},\mbox{axiom})$

$( \mbox{holds}(\mbox{empty},\mbox{state})\mbox{ and }\mbox{holds}(\mbox{clear}(x),\mbox{state})\mbox{ and }\mbox{differ}(x,\mbox{table}) ) \ \Rightarrow \ \mbox{holds}(\mbox{holding}(x),\mbox{do}(\mbox{pickup}(x),\mbox{state}))\qquad\mbox{cnf}(\mbox{pickup}_1,\mbox{axiom})$

$( \mbox{holds}(\mbox{on}(x,y),\mbox{state})\mbox{ and }\mbox{holds}(\mbox{clear}(x),\mbox{state})\mbox{ and }\mbox{holds}(\mbox{empty},\mbox{state}) ) \ \Rightarrow \ \mbox{holds}(\mbox{clear}(y),\mbox{do}(\mbox{pickup}(x),\mbox{state}))\qquad\mbox{cnf}(\mbox{pickup}_2,\mbox{axiom})$

$( \mbox{holds}(\mbox{on}(x,y),\mbox{state})\mbox{ and }\mbox{differ}(x,z) ) \ \Rightarrow \ \mbox{holds}(\mbox{on}(x,y),\mbox{do}(\mbox{pickup}(z),\mbox{state}))\qquad\mbox{cnf}(\mbox{pickup}_3,\mbox{axiom})$

$( \mbox{holds}(\mbox{clear}(x),\mbox{state})\mbox{ and }\mbox{differ}(x,z) ) \ \Rightarrow \ \mbox{holds}(\mbox{clear}(x),\mbox{do}(\mbox{pickup}(z),\mbox{state}))\qquad\mbox{cnf}(\mbox{pickup}_4,\mbox{axiom})$

$( \mbox{holds}(\mbox{holding}(x),\mbox{state})\mbox{ and }\mbox{holds}(\mbox{clear}(y),\mbox{state}) ) \ \Rightarrow \ \mbox{holds}(\mbox{empty},\mbox{do}(\mbox{putdown}(x,y),\mbox{state}))\qquad\mbox{cnf}(\mbox{putdown}_1,\mbox{axiom})$

$( \mbox{holds}(\mbox{holding}(x),\mbox{state})\mbox{ and }\mbox{holds}(\mbox{clear}(y),\mbox{state}) ) \ \Rightarrow \ \mbox{holds}(\mbox{on}(x,y),\mbox{do}(\mbox{putdown}(x,y),\mbox{state}))\qquad\mbox{cnf}(\mbox{putdown}_2,\mbox{axiom})$

$( \mbox{holds}(\mbox{holding}(x),\mbox{state})\mbox{ and }\mbox{holds}(\mbox{clear}(y),\mbox{state}) ) \ \Rightarrow \ \mbox{holds}(\mbox{clear}(x),\mbox{do}(\mbox{putdown}(x,y),\mbox{state}))\qquad\mbox{cnf}(\mbox{putdown}_3,\mbox{axiom})$

$\mbox{holds}(\mbox{on}(x,y),\mbox{state}) \ \Rightarrow \ \mbox{holds}(\mbox{on}(x,y),\mbox{do}(\mbox{putdown}(z,w),\mbox{state}))\qquad\mbox{cnf}(\mbox{putdown}_4,\mbox{axiom})$

$( \mbox{holds}(\mbox{clear}(z),\mbox{state})\mbox{ and }\mbox{differ}(z,y) ) \ \Rightarrow \ \mbox{holds}(\mbox{clear}(z),\mbox{do}(\mbox{putdown}(x,y),\mbox{state}))\qquad\mbox{cnf}(\mbox{putdown}_5,\mbox{axiom})$

\medskip\textbf{PLA011-1.p} Block D on C on B






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

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

$\neg\,\mbox{holds}(\mbox{and}(\mbox{on}(d,c),\mbox{on}(c,b)),\mbox{state})\qquad\mbox{cnf}(\mbox{prove\_DCB},\mbox{negated\_conjecture})$

\medskip\textbf{PLA018-1.p} Block A on B and D on C






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

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

$\neg\,\mbox{holds}(\mbox{and}(\mbox{on}(a,b),\mbox{on}(d,c)),\mbox{state})\qquad\mbox{cnf}(\mbox{prove\_AB\_DC},\mbox{negated\_conjecture})$

\medskip\textbf{PLA032$\wedge$7.p} Abductive planning: Bomb-in-the-toilet with detector






$\mbox{include}(\mbox{'Axioms/LCL015\string^0.ax'})$

$\mbox{include}(\mbox{'Axioms/LCL013\string^5.ax'})$

$\mbox{include}(\mbox{'Axioms/LCL015\string^1.ax'})$

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

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

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

$\mbox{mvalid}@ ( \mbox{mbox\_s}_4@ ( \mbox{mexists\_ind}@ \lambda b{:}\;\mbox{mu}{:}\;( \mbox{bomb}@ b ) ) )\qquad\mbox{thf}(\mbox{ax}_1,\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mexists\_ind}@ \lambda a{:}\;\mbox{mu}{:}\;( \mbox{mbox\_s}_4@ ( \mbox{mforall\_ind}@ \lambda x{:}\;\mbox{mu}{:}\;( \mbox{mimplies}@ ( \mbox{mand}@ ( \mbox{bomb}@ x )@ ( h@ a ) )@ ( \mbox{mbox\_s}_4@ ( \mbox{bomb}@ x ) ) ) ) ) )\qquad\mbox{thf}(\mbox{ax}_2,\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mbox\_s}_4@ ( \mbox{mforall\_ind}@ \lambda x{:}\;\mbox{mu}{:}\;( \mbox{mexists\_ind}@ \lambda d{:}\;\mbox{mu}{:}\;( \mbox{mbox\_s}_4@ ( \mbox{mimplies}@ ( \mbox{mand}@ ( \mbox{bomb}@ x )@ ( h@ d ) )@ ( \mbox{defused}@ x ) ) ) ) ) )\qquad\mbox{thf}(\mbox{ax}_3,\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mbox\_s}_4@ ( \mbox{mforall\_ind}@ \lambda x{:}\;\mbox{mu}{:}\;( \mbox{mexists\_ind}@ \lambda d{:}\;\mbox{mu}{:}\;( \mbox{mimplies}@ ( \mbox{mand}@ ( \mbox{bomb}@ x )@ ( h@ d ) )@ ( \mbox{defused}@ x ) ) ) ) )\qquad\mbox{thf}(\mbox{con},\mbox{conjecture})$

\medskip\textbf{PLA005-2.p} Block C on A and D on B






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

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

$\neg\,\mbox{holds}(\mbox{and}(\mbox{on}(d,b),\mbox{on}(c,a)),\mbox{state})\qquad\mbox{cnf}(\mbox{prove\_DB\_AC},\mbox{negated\_conjecture})$

\medskip\textbf{PLA011-2.p} Block D on C on B






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

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

$\neg\,\mbox{holds}(\mbox{and}(\mbox{on}(c,b),\mbox{on}(d,c)),\mbox{state})\qquad\mbox{cnf}(\mbox{prove\_DCB},\mbox{negated\_conjecture})$

\medskip\textbf{PLA012-1.p} Block D on B on C






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

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

$\neg\,\mbox{holds}(\mbox{and}(\mbox{on}(d,b),\mbox{on}(b,c)),\mbox{state})\qquad\mbox{cnf}(\mbox{prove\_DBC},\mbox{negated\_conjecture})$

\medskip\textbf{PLA008-1.p} Block B on D and A on C






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

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

$\neg\,\mbox{holds}(\mbox{and}(\mbox{on}(b,d),\mbox{on}(a,c)),\mbox{state})\qquad\mbox{cnf}(\mbox{prove\_BD\_AC},\mbox{negated\_conjecture})$

\medskip\textbf{PLA002-2.p} Getting from here to there, in all weather






$( \mbox{situation}(\mbox{situation}_1)\mbox{ and }\mbox{situation}(\mbox{situation}_2) ) \ \Rightarrow \ ( \mbox{warm}(\mbox{situation}_1)\mbox{ or }\mbox{cold}(\mbox{situation}_2) )\qquad\mbox{cnf}(\mbox{warm\_or\_cold},\mbox{hypothesis})$

$( \mbox{at}(a,\mbox{situation})\mbox{ and }\mbox{situation}(\mbox{situation}) ) \ \Rightarrow \ \mbox{at}(b,\mbox{walk}(b,\mbox{situation}))\qquad\mbox{cnf}(\mbox{walk\_a\_to\_b},\mbox{hypothesis})$

$( \mbox{at}(a,\mbox{situation})\mbox{ and }\mbox{situation}(\mbox{situation}) ) \ \Rightarrow \ \mbox{at}(b,\mbox{drive}(b,\mbox{situation}))\qquad\mbox{cnf}(\mbox{drive\_a\_to\_b},\mbox{hypothesis})$

$( \mbox{at}(b,\mbox{situation})\mbox{ and }\mbox{situation}(\mbox{situation}) ) \ \Rightarrow \ \mbox{at}(a,\mbox{walk}(a,\mbox{situation}))\qquad\mbox{cnf}(\mbox{walk\_b\_to\_a},\mbox{hypothesis})$

$( \mbox{at}(b,\mbox{situation})\mbox{ and }\mbox{situation}(\mbox{situation}) ) \ \Rightarrow \ \mbox{at}(a,\mbox{drive}(a,\mbox{situation}))\qquad\mbox{cnf}(\mbox{drive\_b\_to\_a},\mbox{hypothesis})$

$( \mbox{cold}(\mbox{situation})\mbox{ and }\mbox{at}(b,\mbox{situation})\mbox{ and }\mbox{situation}(\mbox{situation}) ) \ \Rightarrow \ \mbox{at}(c,\mbox{skate}(c,\mbox{situation}))\qquad\mbox{cnf}(\mbox{cross\_river\_b\_to\_c},\mbox{hypothesis})$

$( \mbox{cold}(\mbox{situation})\mbox{ and }\mbox{at}(c,\mbox{situation})\mbox{ and }\mbox{situation}(\mbox{situation}) ) \ \Rightarrow \ \mbox{at}(b,\mbox{skate}(b,\mbox{situation}))\qquad\mbox{cnf}(\mbox{cross\_river\_c\_to\_b},\mbox{hypothesis})$

$( \mbox{warm}(\mbox{situation})\mbox{ and }\mbox{at}(b,\mbox{situation})\mbox{ and }\mbox{situation}(\mbox{situation}) ) \ \Rightarrow \ \mbox{at}(d,\mbox{climb}(d,\mbox{situation}))\qquad\mbox{cnf}(\mbox{climb\_mountain\_b\_to\_d},\mbox{hypothesis})$

$( \mbox{warm}(\mbox{situation})\mbox{ and }\mbox{at}(d,\mbox{situation})\mbox{ and }\mbox{situation}(\mbox{situation}) ) \ \Rightarrow \ \mbox{at}(b,\mbox{climb}(b,\mbox{situation}))\qquad\mbox{cnf}(\mbox{climb\_mountain\_d\_to\_b},\mbox{hypothesis})$

$( \mbox{at}(c,\mbox{situation})\mbox{ and }\mbox{situation}(\mbox{situation}) ) \ \Rightarrow \ \mbox{at}(d,\mbox{go}(d,\mbox{situation}))\qquad\mbox{cnf}(\mbox{go\_c\_to\_d},\mbox{hypothesis})$

$( \mbox{at}(d,\mbox{situation})\mbox{ and }\mbox{situation}(\mbox{situation}) ) \ \Rightarrow \ \mbox{at}(c,\mbox{go}(c,\mbox{situation}))\qquad\mbox{cnf}(\mbox{go\_d\_to\_c},\mbox{hypothesis})$

$( \mbox{at}(c,\mbox{situation})\mbox{ and }\mbox{situation}(\mbox{situation}) ) \ \Rightarrow \ \mbox{at}(e,\mbox{go}(e,\mbox{situation}))\qquad\mbox{cnf}(\mbox{go\_c\_to\_e},\mbox{hypothesis})$

$( \mbox{at}(e,\mbox{situation})\mbox{ and }\mbox{situation}(\mbox{situation}) ) \ \Rightarrow \ \mbox{at}(c,\mbox{go}(c,\mbox{situation}))\qquad\mbox{cnf}(\mbox{go\_e\_to\_c},\mbox{hypothesis})$

$( \mbox{at}(d,\mbox{situation})\mbox{ and }\mbox{situation}(\mbox{situation}) ) \ \Rightarrow \ \mbox{at}(f,\mbox{go}(f,\mbox{situation}))\qquad\mbox{cnf}(\mbox{go\_d\_to\_f},\mbox{hypothesis})$

$( \mbox{at}(f,\mbox{situation})\mbox{ and }\mbox{situation}(\mbox{situation}) ) \ \Rightarrow \ \mbox{at}(d,\mbox{go}(d,\mbox{situation}))\qquad\mbox{cnf}(\mbox{go\_f\_to\_d},\mbox{hypothesis})$

$\mbox{situation}(s_0)\qquad\mbox{cnf}(\mbox{initial\_situation},\mbox{hypothesis})$

$\mbox{situation}(\mbox{situation}) \ \Rightarrow \ \mbox{situation}(\mbox{walk}(\mbox{somewhere},\mbox{situation}))\qquad\mbox{cnf}(\mbox{walk\_situation},\mbox{hypothesis})$

$\mbox{situation}(\mbox{situation}) \ \Rightarrow \ \mbox{situation}(\mbox{drive}(\mbox{somewhere},\mbox{situation}))\qquad\mbox{cnf}(\mbox{drive\_situation},\mbox{hypothesis})$

$\mbox{situation}(\mbox{situation}) \ \Rightarrow \ \mbox{situation}(\mbox{climb}(\mbox{somewhere},\mbox{situation}))\qquad\mbox{cnf}(\mbox{climb\_situation},\mbox{hypothesis})$

$\mbox{situation}(\mbox{situation}) \ \Rightarrow \ \mbox{situation}(\mbox{skate}(\mbox{somewhere},\mbox{situation}))\qquad\mbox{cnf}(\mbox{skate\_situation},\mbox{hypothesis})$

$\mbox{situation}(\mbox{situation}) \ \Rightarrow \ \mbox{situation}(\mbox{go}(\mbox{somewhere},\mbox{situation}))\qquad\mbox{cnf}(\mbox{go\_situation},\mbox{hypothesis})$

$\mbox{at}(f,s_0)\qquad\mbox{cnf}(\mbox{initial},\mbox{hypothesis})$

$\mbox{at}(a,s) \ \Rightarrow \ \neg\,\mbox{situation}(s)\qquad\mbox{cnf}(\mbox{prove\_you\_can\_get\_to\_a\_in\_a\_situation},\mbox{negated\_conjecture})$

\medskip\textbf{PLA030-1.p} Blocks world difference axioms for 4 blocks






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

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

\medskip\textbf{PLA033$\wedge$7.p} Abductive planning: Safe problem






$\mbox{include}(\mbox{'Axioms/LCL015\string^0.ax'})$

$\mbox{include}(\mbox{'Axioms/LCL013\string^5.ax'})$

$\mbox{include}(\mbox{'Axioms/LCL015\string^1.ax'})$

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

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

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

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

$o{:}\;\mbox{mu}\qquad\mbox{thf}(\mbox{o\_type},\mbox{type})$

$\forall v{:}\;\mbox{\$i}{:}\;( \mbox{exists\_in\_world}@ o@ v )\qquad\mbox{thf}(\mbox{existence\_of\_o\_ax},\mbox{axiom})$

$n{:}\;\mbox{mu}\qquad\mbox{thf}(\mbox{n\_type},\mbox{type})$

$\forall v{:}\;\mbox{\$i}{:}\;( \mbox{exists\_in\_world}@ n@ v )\qquad\mbox{thf}(\mbox{existence\_of\_n\_ax},\mbox{axiom})$

$d{:}\;\mbox{mu}\qquad\mbox{thf}(\mbox{d\_type},\mbox{type})$

$\forall v{:}\;\mbox{\$i}{:}\;( \mbox{exists\_in\_world}@ d@ v )\qquad\mbox{thf}(\mbox{existence\_of\_d\_ax},\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mbox\_s}_4@ ( \mbox{mforall\_ind}@ \lambda s{:}\;\mbox{mu}{:}\;( \mbox{mforall\_ind}@ \lambda v{:}\;\mbox{mu}{:}\;( \mbox{mexists\_ind}@ \lambda o{:}\;\mbox{mu}{:}\;( \mbox{mand}@ ( \mbox{mbox\_s}_4@ ( \mbox{mimplies}@ ( \mbox{mand}@ ( \mbox{closed}@ s )@ ( \mbox{mand}@ ( \mbox{combo}@ s@ v )@ ( h@ o ) ) )@ ( \mbox{mbox\_s}_4@ ( \mbox{open}@ s ) ) ) )@ ( \mbox{mbox\_s}_4@ ( \mbox{mimplies}@ ( \mbox{mand}@ ( \mbox{closed}@ s )@ ( \mbox{mand}@ ( \mbox{mnot}@ ( \mbox{combo}@ s@ v ) )@ ( h@ o ) ) )@ ( \mbox{mbox\_s}_4@ ( \mbox{closed}@ s ) ) ) ) ) ) ) ) )\qquad\mbox{thf}(\mbox{ax}_1,\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mbox\_s}_4@ ( \mbox{closed}@ d ) )\qquad\mbox{thf}(\mbox{ax}_2,\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mbox\_s}_4@ ( \mbox{mor}@ ( \mbox{combo}@ d@ n )@ ( \mbox{mnot}@ ( \mbox{combo}@ d@ n ) ) ) )\qquad\mbox{thf}(\mbox{ax}_3,\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mbox\_s}_4@ ( \mbox{mforall\_ind}@ \lambda s{:}\;\mbox{mu}{:}\;( \mbox{mnot}@ ( \mbox{mand}@ ( \mbox{open}@ s )@ ( \mbox{closed}@ s ) ) ) ) )\qquad\mbox{thf}(\mbox{ax}_4,\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mexists\_ind}@ \lambda v{:}\;\mbox{mu}{:}\;( \mbox{mbox\_s}_4@ ( \mbox{combo}@ d@ v ) ) )\qquad\mbox{thf}(\mbox{ax}_5,\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mbox\_s}_4@ ( \mbox{mexists\_ind}@ \lambda v{:}\;\mbox{mu}{:}\;( \mbox{mexists\_ind}@ \lambda o{:}\;\mbox{mu}{:}\;( \mbox{mimplies}@ ( \mbox{mbox\_s}_4@ ( \mbox{mand}@ ( \mbox{combo}@ d@ v )@ ( h@ o ) ) )@ ( \mbox{mbox\_s}_4@ ( \mbox{open}@ d ) ) ) ) ) )\qquad\mbox{thf}(\mbox{con},\mbox{conjecture})$

\medskip\textbf{PLA019-1.p} Block D on C






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

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

$\neg\,\mbox{holds}(\mbox{on}(d,c),\mbox{state})\qquad\mbox{cnf}(\mbox{prove\_DC},\mbox{negated\_conjecture})$

\medskip\textbf{PLA007-1.p} Block A on D






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

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

$\neg\,\mbox{holds}(\mbox{on}(a,d),\mbox{state})\qquad\mbox{cnf}(\mbox{prove\_AD},\mbox{negated\_conjecture})$

\medskip\textbf{PLA005-1.p} Block C on A and D on B






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

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

$\neg\,\mbox{holds}(\mbox{and}(\mbox{on}(c,a),\mbox{on}(d,b)),\mbox{state})\qquad\mbox{cnf}(\mbox{prove\_CA\_DB},\mbox{negated\_conjecture})$

\medskip\textbf{PLA029+2.p} Blocks world axioms






$\mbox{include}(\mbox{'Axioms/PLA002+0.ax'})$

\medskip\textbf{PLA016-1.p} Block D on A






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

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

$\neg\,\mbox{holds}(\mbox{on}(d,a),\mbox{state})\qquad\mbox{cnf}(\mbox{prove\_DA},\mbox{negated\_conjecture})$

\medskip\textbf{PLA001-1.p} Cheyenne to DesMoines, buying a loaf of bread on the way

The problem is to drive from Cheyenne, Wyoming to Des Moines,
 Iowa and end up there with a loaf of bread. A portion of the
 road map is expressed in clause form. The allowable actions
 are to drive from a city to a neighboring city, to buy a loaf
 of bread at a city, and to wait\_at at a city for one unit
 of time. Buying a loaf of bread takes one unit of time and
 driving to a neighboring city takes two units of time.




$( \mbox{at}(\mbox{fromCity},\mbox{loaves},\mbox{time},\mbox{situation})\mbox{ and }\mbox{next\_to}(\mbox{fromCity},\mbox{toCity}) ) \ \Rightarrow \ \mbox{at}(\mbox{toCity},\mbox{loaves},s(s(\mbox{time})),\mbox{drive}(\mbox{toCity},\mbox{situation}))\qquad\mbox{cnf}(\mbox{drive}_1,\mbox{axiom})$

$( \mbox{at}(\mbox{fromCity},\mbox{loaves},\mbox{time},\mbox{situation})\mbox{ and }\mbox{next\_to}(\mbox{toCity},\mbox{fromCity}) ) \ \Rightarrow \ \mbox{at}(\mbox{toCity},\mbox{loaves},s(s(\mbox{time})),\mbox{drive}(\mbox{toCity},\mbox{situation}))\qquad\mbox{cnf}(\mbox{drive}_2,\mbox{axiom})$

$\mbox{at}(\mbox{city},\mbox{loaves},\mbox{time},\mbox{situation}) \ \Rightarrow \ \mbox{at}(\mbox{city},\mbox{loaves},s(\mbox{time}),\mbox{wait\_at}(\mbox{situation}))\qquad\mbox{cnf}(\mbox{wait\_in\_city},\mbox{axiom})$

$\mbox{at}(\mbox{city},\mbox{loaves},\mbox{time},\mbox{situation}) \ \Rightarrow \ \mbox{at}(\mbox{city},s(\mbox{loaves}),s(\mbox{time}),\mbox{buy}(\mbox{situation}))\qquad\mbox{cnf}(\mbox{buy\_in\_city},\mbox{axiom})$

$\mbox{next\_to}(\mbox{winnemucca},\mbox{elko})\qquad\mbox{cnf}(\mbox{map}_1,\mbox{hypothesis})$

$\mbox{next\_to}(\mbox{elko},\mbox{saltLakeCity})\qquad\mbox{cnf}(\mbox{map}_2,\mbox{hypothesis})$

$\mbox{next\_to}(\mbox{saltLakeCity},\mbox{rockSprings})\qquad\mbox{cnf}(\mbox{map}_3,\mbox{hypothesis})$

$\mbox{next\_to}(\mbox{rockSprings},\mbox{laramie})\qquad\mbox{cnf}(\mbox{map}_4,\mbox{hypothesis})$

$\mbox{next\_to}(\mbox{laramie},\mbox{cheyenne})\qquad\mbox{cnf}(\mbox{map}_5,\mbox{hypothesis})$

$\mbox{next\_to}(\mbox{cheyenne},\mbox{northPlatte})\qquad\mbox{cnf}(\mbox{map}_6,\mbox{hypothesis})$

$\mbox{next\_to}(\mbox{northPlatte},\mbox{grandIsland})\qquad\mbox{cnf}(\mbox{map}_7,\mbox{hypothesis})$

$\mbox{next\_to}(\mbox{grandIsland},\mbox{lincoln})\qquad\mbox{cnf}(\mbox{map}_8,\mbox{hypothesis})$

$\mbox{next\_to}(\mbox{lincoln},\mbox{omaha})\qquad\mbox{cnf}(\mbox{map}_9,\mbox{hypothesis})$

$\mbox{next\_to}(\mbox{omaha},\mbox{desMoines})\qquad\mbox{cnf}(\mbox{map}_{10},\mbox{hypothesis})$

$\mbox{at}(\mbox{cheyenne},\mbox{none},\mbox{start},\mbox{initial\_situation})\qquad\mbox{cnf}(\mbox{initial},\mbox{hypothesis})$

$\neg\,\mbox{at}(\mbox{desMoines},s(\mbox{none}),\mbox{time},\mbox{situation})\qquad\mbox{cnf}(\mbox{prove\_you\_gat\_get\_there\_with\_bread},\mbox{negated\_conjecture})$

\medskip\textbf{PLA009-1.p} Block A on B and D clear






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

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

$\neg\,\mbox{holds}(\mbox{and}(\mbox{on}(a,b),\mbox{clear}(d)),\mbox{state})\qquad\mbox{cnf}(\mbox{prove\_AB\_D},\mbox{negated\_conjecture})$

\medskip\textbf{PLA020-1.p} Block D clear






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

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

$\neg\,\mbox{holds}(\mbox{clear}(d),\mbox{state})\qquad\mbox{cnf}(\mbox{prove\_D},\mbox{negated\_conjecture})$

\medskip\textbf{PLA014-2.p} Block A on B on C






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

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

$\neg\,\mbox{holds}(\mbox{and}(\mbox{on}(b,c),\mbox{on}(a,b)),\mbox{state})\qquad\mbox{cnf}(\mbox{prove\_ABC},\mbox{negated\_conjecture})$

\medskip\textbf{PLA021-1.p} Block B on D and C on A






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

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

$\neg\,\mbox{holds}(\mbox{and}(\mbox{on}(b,d),\mbox{on}(c,a)),\mbox{state})\qquad\mbox{cnf}(\mbox{prove\_BD\_CA},\mbox{negated\_conjecture})$

\medskip\textbf{PLA022-2.p} Block A on C on D






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

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

$\neg\,\mbox{holds}(\mbox{and}(\mbox{on}(a,c),\mbox{on}(c,d)),\mbox{state})\qquad\mbox{cnf}(\mbox{prove\_ACD},\mbox{negated\_conjecture})$

\medskip\textbf{PLA027+1.p} Blocks A/B/C/D =$>$ D/C/B/A






$\mbox{include}(\mbox{'Axioms/PLA002+0.ax'})$

$\forall y,x{:}\;( ( \mbox{different}(x,y)\mbox{ or }\mbox{different}(y,x) ) \ \Rightarrow \ \mbox{neq}(x,y) )\qquad\mbox{fof}(\mbox{different\_not\_equal},\mbox{hypothesis})$

$\mbox{different}(\mbox{block}_1,\mbox{block}_2)\qquad\mbox{fof}(\mbox{block\_1\_not\_block}_2,\mbox{hypothesis})$

$\mbox{different}(\mbox{block}_1,\mbox{block}_3)\qquad\mbox{fof}(\mbox{block\_1\_not\_block}_3,\mbox{hypothesis})$

$\mbox{different}(\mbox{block}_1,\mbox{block}_4)\qquad\mbox{fof}(\mbox{block\_1\_not\_block}_4,\mbox{hypothesis})$

$\mbox{different}(\mbox{block}_2,\mbox{block}_3)\qquad\mbox{fof}(\mbox{block\_2\_not\_block}_3,\mbox{hypothesis})$

$\mbox{different}(\mbox{block}_2,\mbox{block}_4)\qquad\mbox{fof}(\mbox{block\_2\_not\_block}_4,\mbox{hypothesis})$

$\mbox{different}(\mbox{block}_3,\mbox{block}_4)\qquad\mbox{fof}(\mbox{block\_3\_not\_block}_4,\mbox{hypothesis})$

$\mbox{different}(\mbox{block}_1,\mbox{table})\qquad\mbox{fof}(\mbox{block\_1\_not\_table},\mbox{hypothesis})$

$\mbox{different}(\mbox{block}_2,\mbox{table})\qquad\mbox{fof}(\mbox{block\_2\_not\_table},\mbox{hypothesis})$

$\mbox{different}(\mbox{block}_3,\mbox{table})\qquad\mbox{fof}(\mbox{block\_3\_not\_table},\mbox{hypothesis})$

$\mbox{different}(\mbox{block}_4,\mbox{table})\qquad\mbox{fof}(\mbox{block\_4\_not\_table},\mbox{hypothesis})$

$\mbox{a\_block}(\mbox{block}_1)\qquad\mbox{fof}(\mbox{block}_1,\mbox{hypothesis})$

$\mbox{a\_block}(\mbox{block}_2)\qquad\mbox{fof}(\mbox{block}_2,\mbox{hypothesis})$

$\mbox{a\_block}(\mbox{block}_3)\qquad\mbox{fof}(\mbox{block}_3,\mbox{hypothesis})$

$\mbox{a\_block}(\mbox{block}_4)\qquad\mbox{fof}(\mbox{block}_4,\mbox{hypothesis})$

$\mbox{a\_block}(\mbox{table})\qquad\mbox{fof}(\mbox{table},\mbox{hypothesis})$

$\mbox{fixed}(\mbox{table})\qquad\mbox{fof}(\mbox{fixed\_table},\mbox{hypothesis})$

$\mbox{nonfixed}(\mbox{block}_1)\qquad\mbox{fof}(\mbox{nonfixed\_block}_1,\mbox{hypothesis})$

$\mbox{nonfixed}(\mbox{block}_2)\qquad\mbox{fof}(\mbox{nonfixed\_block}_2,\mbox{hypothesis})$

$\mbox{nonfixed}(\mbox{block}_3)\qquad\mbox{fof}(\mbox{nonfixed\_block}_3,\mbox{hypothesis})$

$\mbox{nonfixed}(\mbox{block}_4)\qquad\mbox{fof}(\mbox{nonfixed\_block}_4,\mbox{hypothesis})$

$\mbox{time}(\mbox{time}_0)\qquad\mbox{fof}(\mbox{time}_0,\mbox{hypothesis})$

$\mbox{time}(s(\mbox{time}_0))\qquad\mbox{fof}(\mbox{time}_1,\mbox{hypothesis})$

$\mbox{time}(s(s(\mbox{time}_0)))\qquad\mbox{fof}(\mbox{time}_2,\mbox{hypothesis})$

$\mbox{time}(s(s(s(\mbox{time}_0))))\qquad\mbox{fof}(\mbox{time}_3,\mbox{hypothesis})$

$\mbox{time}(s(s(s(s(\mbox{time}_0)))))\qquad\mbox{fof}(\mbox{time}_4,\mbox{hypothesis})$

$\forall i{:}\;( \mbox{time}(i) \ \Rightarrow \ ( \mbox{source}(\mbox{block}_1,i)\mbox{ or }\mbox{source}(\mbox{block}_2,i)\mbox{ or }\mbox{source}(\mbox{block}_3,i)\mbox{ or }\mbox{source}(\mbox{block}_4,i)\mbox{ or }\mbox{source}(\mbox{table},i) ) )\qquad\mbox{fof}(\mbox{some\_source},\mbox{hypothesis})$

$\forall i{:}\;( \mbox{time}(i) \ \Rightarrow \ ( \mbox{destination}(\mbox{block}_1,i)\mbox{ or }\mbox{destination}(\mbox{block}_2,i)\mbox{ or }\mbox{destination}(\mbox{block}_3,i)\mbox{ or }\mbox{destination}(\mbox{block}_4,i)\mbox{ or }\mbox{destination}(\mbox{table},i) ) )\qquad\mbox{fof}(\mbox{some\_destination},\mbox{hypothesis})$

$\forall i{:}\;( \mbox{time}(i) \ \Rightarrow \ ( \mbox{object}(\mbox{block}_1,i)\mbox{ or }\mbox{object}(\mbox{block}_2,i)\mbox{ or }\mbox{object}(\mbox{block}_3,i)\mbox{ or }\mbox{object}(\mbox{block}_4,i) ) )\qquad\mbox{fof}(\mbox{some\_object},\mbox{hypothesis})$

$\mbox{on}(\mbox{block}_1,\mbox{block}_2,\mbox{time}_0)\qquad\mbox{fof}(\mbox{initial\_1\_on}_2,\mbox{hypothesis})$

$\mbox{clear}(\mbox{block}_1,\mbox{time}_0)\qquad\mbox{fof}(\mbox{initial\_clear}_1,\mbox{hypothesis})$

$\mbox{on}(\mbox{block}_2,\mbox{block}_3,\mbox{time}_0)\qquad\mbox{fof}(\mbox{initial\_2\_on}_3,\mbox{hypothesis})$

$\mbox{on}(\mbox{block}_3,\mbox{block}_4,\mbox{time}_0)\qquad\mbox{fof}(\mbox{initial\_3\_on}_4,\mbox{hypothesis})$

$\mbox{on}(\mbox{block}_4,\mbox{table},\mbox{time}_0)\qquad\mbox{fof}(\mbox{initial\_4\_on\_table},\mbox{hypothesis})$

$\mbox{goal\_time}(s(s(s(s(\mbox{time}_0)))))\qquad\mbox{fof}(\mbox{goal\_time}_4,\mbox{hypothesis})$

$\forall s{:}\;( \mbox{goal\_time}(s) \ \Rightarrow \ ( \mbox{on}(\mbox{block}_4,\mbox{block}_3,s)\mbox{ and }\mbox{clear}(\mbox{block}_4,s)\mbox{ and }\mbox{on}(\mbox{block}_3,\mbox{block}_2,s)\mbox{ and }\mbox{on}(\mbox{block}_2,\mbox{block}_1,s)\mbox{ and }\mbox{on}(\mbox{block}_1,\mbox{table},s) ) )\qquad\mbox{fof}(\mbox{goal\_state},\mbox{conjecture})$

\medskip\textbf{PLA004-1.p} Block C on B on A






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

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

$\neg\,\mbox{holds}(\mbox{and}(\mbox{on}(c,b),\mbox{on}(b,a)),\mbox{state})\qquad\mbox{cnf}(\mbox{prove\_CBA},\mbox{negated\_conjecture})$

\medskip\textbf{PLA003-1.p} Monkey and Bananas Problem






$\mbox{can}(\mbox{monkey}(\mbox{location}_1,\mbox{floor},\mbox{nothing}),\mbox{ladder}(\mbox{location}_1,\mbox{floor}),\mbox{bananas}) \ \Rightarrow \ \mbox{can}(\mbox{monkey}(\mbox{location}_1,\mbox{ceiling},\mbox{nothing}),\mbox{ladder}(\mbox{location}_1,\mbox{floor}),\mbox{bananas})\qquad\mbox{cnf}(\mbox{climb\_up},\mbox{axiom})$

$\mbox{can}(\mbox{monkey}(\mbox{location}_1,\mbox{ceiling},\mbox{nothing}),\mbox{ladder}(\mbox{location}_1,\mbox{floor}),\mbox{bananas}) \ \Rightarrow \ \mbox{can}(\mbox{monkey}(\mbox{location}_1,\mbox{floor},\mbox{nothing}),\mbox{ladder}(\mbox{location}_1,\mbox{floor}),\mbox{bananas})\qquad\mbox{cnf}(\mbox{climb\_down},\mbox{axiom})$

$\mbox{can}(\mbox{monkey}(\mbox{location}_1,\mbox{floor},\mbox{the\_ladder}),\mbox{ladder}(\mbox{location}_1,\mbox{floor}),\mbox{bananas}) \ \Rightarrow \ \mbox{can}(\mbox{monkey}(\mbox{location}_2,\mbox{floor},\mbox{the\_ladder}),\mbox{ladder}(\mbox{location}_2,\mbox{floor}),\mbox{bananas})\qquad\mbox{cnf}(\mbox{go\_holding\_ladder},\mbox{axiom})$

$\mbox{can}(\mbox{monkey}(\mbox{location}_1,\mbox{floor},\mbox{the\_bananas}),\mbox{ladder},\mbox{bananas}(\mbox{location}_1,\mbox{floor})) \ \Rightarrow \ \mbox{can}(\mbox{monkey}(\mbox{location}_2,\mbox{floor},\mbox{the\_bananas}),\mbox{ladder},\mbox{bananas}(\mbox{location}_2,\mbox{floor}))\qquad\mbox{cnf}(\mbox{go\_holding\_bananas},\mbox{axiom})$

$\mbox{can}(\mbox{monkey}(\mbox{location}_1,\mbox{floor},\mbox{nothing}),\mbox{ladder},\mbox{bananas}) \ \Rightarrow \ \mbox{can}(\mbox{monkey}(\mbox{location}_2,\mbox{floor},\mbox{nothing}),\mbox{ladder},\mbox{bananas})\qquad\mbox{cnf}(\mbox{go\_holding\_nothing},\mbox{axiom})$

$\mbox{can}(\mbox{monkey}(\mbox{location},\mbox{height},\mbox{the\_ladder}),\mbox{ladder}(\mbox{location},\mbox{any\_height}),\mbox{bananas}) \ \Rightarrow \ \mbox{can}(\mbox{monkey}(\mbox{location},\mbox{height},\mbox{nothing}),\mbox{ladder}(\mbox{location},\mbox{floor}),\mbox{bananas})\qquad\mbox{cnf}(\mbox{drop\_ladder},\mbox{axiom})$

$\mbox{can}(\mbox{monkey}(\mbox{location},\mbox{height},\mbox{the\_bananas}),\mbox{ladder},\mbox{bananas}(\mbox{location},\mbox{height})) \ \Rightarrow \ \mbox{can}(\mbox{monkey}(\mbox{location},\mbox{height},\mbox{nothing}),\mbox{ladder},\mbox{bananas}(\mbox{location},\mbox{floor}))\qquad\mbox{cnf}(\mbox{drop\_bananas},\mbox{axiom})$

$\mbox{can}(\mbox{monkey}(\mbox{location},\mbox{height},\mbox{nothing}),\mbox{ladder},\mbox{bananas}(\mbox{location},\mbox{height})) \ \Rightarrow \ \mbox{can}(\mbox{monkey}(\mbox{location},\mbox{height},\mbox{the\_bananas}),\mbox{ladder},\mbox{bananas}(\mbox{location},\mbox{height}))\qquad\mbox{cnf}(\mbox{grab\_bananas},\mbox{axiom})$

$\mbox{can}(\mbox{monkey}(\mbox{location},\mbox{height},\mbox{nothing}),\mbox{ladder}(\mbox{location},\mbox{height}),\mbox{bananas}) \ \Rightarrow \ \mbox{can}(\mbox{monkey}(\mbox{location},\mbox{height},\mbox{the\_ladder}),\mbox{ladder}(\mbox{location},\mbox{height}),\mbox{bananas})\qquad\mbox{cnf}(\mbox{grab\_ladder},\mbox{axiom})$

$\mbox{can}(\mbox{monkey}(l_0,\mbox{floor},\mbox{nothing}),\mbox{ladder}(l_1,\mbox{floor}),\mbox{bananas}(l_2,\mbox{ceiling}))\qquad\mbox{cnf}(\mbox{initial\_situation},\mbox{hypothesis})$

$\neg\,\mbox{can}(\mbox{monkey}(\mbox{somewhere},\mbox{some\_height},\mbox{the\_bananas}),\mbox{ladder},\mbox{what})\qquad\mbox{cnf}(\mbox{prove\_the\_monkey\_can\_get\_the\_bananas},\mbox{negated\_conjecture})$

\medskip\textbf{PLA013-1.p} Block A on C on B






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

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

$\neg\,\mbox{holds}(\mbox{and}(\mbox{on}(a,c),\mbox{on}(c,b)),\mbox{state})\qquad\mbox{cnf}(\mbox{prove\_ACB},\mbox{negated\_conjecture})$

\medskip\textbf{PLA024+1.p} Blocks A/B, C =$>$ B/C/A






$\mbox{include}(\mbox{'Axioms/PLA002+0.ax'})$

$\forall y,x{:}\;( ( \mbox{different}(x,y)\mbox{ or }\mbox{different}(y,x) ) \ \Rightarrow \ \mbox{neq}(x,y) )\qquad\mbox{fof}(\mbox{different\_not\_equal},\mbox{hypothesis})$

$\mbox{different}(\mbox{block}_1,\mbox{block}_2)\qquad\mbox{fof}(\mbox{block\_1\_not\_block}_2,\mbox{hypothesis})$

$\mbox{different}(\mbox{block}_1,\mbox{block}_3)\qquad\mbox{fof}(\mbox{block\_1\_not\_block}_3,\mbox{hypothesis})$

$\mbox{different}(\mbox{block}_2,\mbox{block}_3)\qquad\mbox{fof}(\mbox{block\_2\_not\_block}_3,\mbox{hypothesis})$

$\mbox{different}(\mbox{block}_1,\mbox{table})\qquad\mbox{fof}(\mbox{block\_1\_not\_table},\mbox{hypothesis})$

$\mbox{different}(\mbox{block}_2,\mbox{table})\qquad\mbox{fof}(\mbox{block\_2\_not\_table},\mbox{hypothesis})$

$\mbox{different}(\mbox{block}_3,\mbox{table})\qquad\mbox{fof}(\mbox{block\_3\_not\_table},\mbox{hypothesis})$

$\mbox{a\_block}(\mbox{block}_1)\qquad\mbox{fof}(\mbox{block}_1,\mbox{hypothesis})$

$\mbox{a\_block}(\mbox{block}_2)\qquad\mbox{fof}(\mbox{block}_2,\mbox{hypothesis})$

$\mbox{a\_block}(\mbox{block}_3)\qquad\mbox{fof}(\mbox{block}_3,\mbox{hypothesis})$

$\mbox{a\_block}(\mbox{table})\qquad\mbox{fof}(\mbox{table},\mbox{hypothesis})$

$\mbox{fixed}(\mbox{table})\qquad\mbox{fof}(\mbox{fixed\_table},\mbox{hypothesis})$

$\mbox{nonfixed}(\mbox{block}_1)\qquad\mbox{fof}(\mbox{nonfixed\_block}_1,\mbox{hypothesis})$

$\mbox{nonfixed}(\mbox{block}_2)\qquad\mbox{fof}(\mbox{nonfixed\_block}_2,\mbox{hypothesis})$

$\mbox{nonfixed}(\mbox{block}_3)\qquad\mbox{fof}(\mbox{nonfixed\_block}_3,\mbox{hypothesis})$

$\mbox{time}(\mbox{time}_0)\qquad\mbox{fof}(\mbox{time}_0,\mbox{hypothesis})$

$\mbox{time}(s(\mbox{time}_0))\qquad\mbox{fof}(\mbox{time}_1,\mbox{hypothesis})$

$\mbox{time}(s(s(\mbox{time}_0)))\qquad\mbox{fof}(\mbox{time}_2,\mbox{hypothesis})$

$\mbox{time}(s(s(s(\mbox{time}_0))))\qquad\mbox{fof}(\mbox{time}_3,\mbox{hypothesis})$

$\forall i{:}\;( \mbox{time}(i) \ \Rightarrow \ ( \mbox{source}(\mbox{block}_1,i)\mbox{ or }\mbox{source}(\mbox{block}_2,i)\mbox{ or }\mbox{source}(\mbox{block}_3,i)\mbox{ or }\mbox{source}(\mbox{table},i) ) )\qquad\mbox{fof}(\mbox{some\_source},\mbox{hypothesis})$

$\forall i{:}\;( \mbox{time}(i) \ \Rightarrow \ ( \mbox{destination}(\mbox{block}_1,i)\mbox{ or }\mbox{destination}(\mbox{block}_2,i)\mbox{ or }\mbox{destination}(\mbox{block}_3,i)\mbox{ or }\mbox{destination}(\mbox{table},i) ) )\qquad\mbox{fof}(\mbox{some\_destination},\mbox{hypothesis})$

$\forall i{:}\;( \mbox{time}(i) \ \Rightarrow \ ( \mbox{object}(\mbox{block}_1,i)\mbox{ or }\mbox{object}(\mbox{block}_2,i)\mbox{ or }\mbox{object}(\mbox{block}_3,i) ) )\qquad\mbox{fof}(\mbox{some\_object},\mbox{hypothesis})$

$\mbox{on}(\mbox{block}_1,\mbox{block}_2,\mbox{time}_0)\qquad\mbox{fof}(\mbox{initial\_1\_on}_2,\mbox{hypothesis})$

$\mbox{clear}(\mbox{block}_1,\mbox{time}_0)\qquad\mbox{fof}(\mbox{initial\_clear}_1,\mbox{hypothesis})$

$\mbox{on}(\mbox{block}_2,\mbox{table},\mbox{time}_0)\qquad\mbox{fof}(\mbox{initial\_2\_on\_table},\mbox{hypothesis})$

$\mbox{on}(\mbox{block}_3,\mbox{table},\mbox{time}_0)\qquad\mbox{fof}(\mbox{initial\_3\_on\_table},\mbox{hypothesis})$

$\mbox{clear}(\mbox{block}_3,\mbox{time}_0)\qquad\mbox{fof}(\mbox{initial\_clear}_3,\mbox{hypothesis})$

$\mbox{goal\_time}(s(s(s(\mbox{time}_0))))\qquad\mbox{fof}(\mbox{goal\_time}_3,\mbox{hypothesis})$

$\forall s{:}\;( \mbox{goal\_time}(s) \ \Rightarrow \ ( \mbox{on}(\mbox{block}_2,\mbox{block}_3,s)\mbox{ and }\mbox{clear}(\mbox{block}_2,s)\mbox{ and }\mbox{on}(\mbox{block}_3,\mbox{block}_1,s)\mbox{ and }\mbox{on}(\mbox{block}_1,\mbox{table},s) ) )\qquad\mbox{fof}(\mbox{goal\_state},\mbox{conjecture})$

\medskip\textbf{PLA022-1.p} Block A on C on D






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

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

$\neg\,\mbox{holds}(\mbox{and}(\mbox{on}(c,d),\mbox{on}(a,c)),\mbox{state})\qquad\mbox{cnf}(\mbox{prove\_ACD},\mbox{negated\_conjecture})$

\medskip\textbf{PLA009-2.p} Block A on B and D clear






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

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

$\neg\,\mbox{holds}(\mbox{and}(\mbox{clear}(d),\mbox{on}(a,b)),\mbox{state})\qquad\mbox{cnf}(\mbox{prove\_D\_AB},\mbox{negated\_conjecture})$

\medskip\textbf{PLA028+1.p} Blocks A, B =$>$ A/B






$\mbox{include}(\mbox{'Axioms/PLA002+0.ax'})$

$\forall y,x{:}\;( ( \mbox{different}(x,y)\mbox{ or }\mbox{different}(y,x) ) \ \Rightarrow \ \mbox{neq}(x,y) )\qquad\mbox{fof}(\mbox{different\_not\_equal},\mbox{hypothesis})$

$\mbox{different}(\mbox{block}_1,\mbox{block}_2)\qquad\mbox{fof}(\mbox{block\_1\_not\_block}_2,\mbox{hypothesis})$

$\mbox{different}(\mbox{block}_1,\mbox{table})\qquad\mbox{fof}(\mbox{block\_1\_not\_table},\mbox{hypothesis})$

$\mbox{different}(\mbox{block}_2,\mbox{table})\qquad\mbox{fof}(\mbox{block\_2\_not\_table},\mbox{hypothesis})$

$\mbox{a\_block}(\mbox{block}_1)\qquad\mbox{fof}(\mbox{block}_1,\mbox{hypothesis})$

$\mbox{a\_block}(\mbox{block}_2)\qquad\mbox{fof}(\mbox{block}_2,\mbox{hypothesis})$

$\mbox{a\_block}(\mbox{table})\qquad\mbox{fof}(\mbox{table},\mbox{hypothesis})$

$\mbox{fixed}(\mbox{table})\qquad\mbox{fof}(\mbox{fixed\_table},\mbox{hypothesis})$

$\mbox{nonfixed}(\mbox{block}_1)\qquad\mbox{fof}(\mbox{nonfixed\_block}_1,\mbox{hypothesis})$

$\mbox{nonfixed}(\mbox{block}_2)\qquad\mbox{fof}(\mbox{nonfixed\_block}_2,\mbox{hypothesis})$

$\mbox{time}(\mbox{time}_0)\qquad\mbox{fof}(\mbox{time}_0,\mbox{hypothesis})$

$\mbox{time}(s(\mbox{time}_0))\qquad\mbox{fof}(\mbox{time}_1,\mbox{hypothesis})$

$\forall i{:}\;( \mbox{time}(i) \ \Rightarrow \ ( \mbox{source}(\mbox{block}_1,i)\mbox{ or }\mbox{source}(\mbox{block}_2,i)\mbox{ or }\mbox{source}(\mbox{table},i) ) )\qquad\mbox{fof}(\mbox{some\_source},\mbox{hypothesis})$

$\forall i{:}\;( \mbox{time}(i) \ \Rightarrow \ ( \mbox{destination}(\mbox{block}_1,i)\mbox{ or }\mbox{destination}(\mbox{block}_2,i)\mbox{ or }\mbox{destination}(\mbox{table},i) ) )\qquad\mbox{fof}(\mbox{some\_destination},\mbox{hypothesis})$

$\forall i{:}\;( \mbox{time}(i) \ \Rightarrow \ ( \mbox{object}(\mbox{block}_1,i)\mbox{ or }\mbox{object}(\mbox{block}_2,i) ) )\qquad\mbox{fof}(\mbox{some\_object},\mbox{hypothesis})$

$\mbox{on}(\mbox{block}_1,\mbox{table},\mbox{time}_0)\qquad\mbox{fof}(\mbox{initial\_1\_on\_table},\mbox{hypothesis})$

$\mbox{clear}(\mbox{block}_1,\mbox{time}_0)\qquad\mbox{fof}(\mbox{initial\_clear}_1,\mbox{hypothesis})$

$\mbox{on}(\mbox{block}_2,\mbox{table},\mbox{time}_0)\qquad\mbox{fof}(\mbox{initial\_2\_on\_table},\mbox{hypothesis})$

$\mbox{clear}(\mbox{block}_2,\mbox{time}_0)\qquad\mbox{fof}(\mbox{initial\_clear}_2,\mbox{hypothesis})$

$\mbox{goal\_time}(s(\mbox{time}_0))\qquad\mbox{fof}(\mbox{goal\_time}_1,\mbox{hypothesis})$

$\forall s{:}\;( \mbox{goal\_time}(s) \ \Rightarrow \ ( \mbox{clear}(\mbox{block}_1,s)\mbox{ and }\mbox{on}(\mbox{block}_1,\mbox{block}_2,s)\mbox{ and }\mbox{on}(\mbox{block}_2,\mbox{table},s) ) )\qquad\mbox{fof}(\mbox{goal\_state},\mbox{conjecture})$

\medskip\textbf{PLA004-2.p} Block C on B on A






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

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

$\neg\,\mbox{holds}(\mbox{and}(\mbox{on}(b,a),\mbox{on}(c,b)),\mbox{state})\qquad\mbox{cnf}(\mbox{prove\_CBA},\mbox{negated\_conjecture})$

\medskip\textbf{PLA006-1.p} Block C on Table






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

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

$\neg\,\mbox{holds}(\mbox{on}(c,\mbox{table}),\mbox{state})\qquad\mbox{cnf}(\mbox{prove\_CTable},\mbox{negated\_conjecture})$

\medskip\textbf{PLA015-1.p} Block A on B on D






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

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

$\neg\,\mbox{holds}(\mbox{and}(\mbox{on}(a,b),\mbox{on}(b,d)),\mbox{state})\qquad\mbox{cnf}(\mbox{prove\_ABD},\mbox{negated\_conjecture})$

\medskip\textbf{PLA002-1.p} Getting from here to there, in all weather

The problem is to travel from one place to another.
 Certain paths are passable at different times of the year, so
 a conditional plan must be generated. Either all situations
 are cold or all situations are warm. There is a river which
 may be crossed only in winter when it is covered with ice,
 and a mountain range may be crossed only in summer. The
 problem is to get from city F to city A.




$\mbox{warm}(\mbox{situation}_1)\mbox{ or }\mbox{cold}(\mbox{situation}_2)\qquad\mbox{cnf}(\mbox{warm\_or\_cold},\mbox{hypothesis})$

$\mbox{at}(a,\mbox{situation}) \ \Rightarrow \ \mbox{at}(b,\mbox{walk}(b,\mbox{situation}))\qquad\mbox{cnf}(\mbox{walk\_a\_to\_b},\mbox{hypothesis})$

$\mbox{at}(a,\mbox{situation}) \ \Rightarrow \ \mbox{at}(b,\mbox{drive}(b,\mbox{situation}))\qquad\mbox{cnf}(\mbox{drive\_a\_to\_b},\mbox{hypothesis})$

$\mbox{at}(b,\mbox{situation}) \ \Rightarrow \ \mbox{at}(a,\mbox{walk}(a,\mbox{situation}))\qquad\mbox{cnf}(\mbox{walk\_b\_to\_a},\mbox{hypothesis})$

$\mbox{at}(b,\mbox{situation}) \ \Rightarrow \ \mbox{at}(a,\mbox{drive}(a,\mbox{situation}))\qquad\mbox{cnf}(\mbox{drive\_b\_to\_a},\mbox{hypothesis})$

$( \mbox{cold}(\mbox{situation})\mbox{ and }\mbox{at}(b,\mbox{situation}) ) \ \Rightarrow \ \mbox{at}(c,\mbox{skate}(c,\mbox{situation}))\qquad\mbox{cnf}(\mbox{cross\_river\_b\_to\_c},\mbox{hypothesis})$

$( \mbox{cold}(\mbox{situation})\mbox{ and }\mbox{at}(c,\mbox{situation}) ) \ \Rightarrow \ \mbox{at}(b,\mbox{skate}(b,\mbox{situation}))\qquad\mbox{cnf}(\mbox{cross\_river\_c\_to\_b},\mbox{hypothesis})$

$( \mbox{warm}(\mbox{situation})\mbox{ and }\mbox{at}(b,\mbox{situation}) ) \ \Rightarrow \ \mbox{at}(d,\mbox{climb}(d,\mbox{situation}))\qquad\mbox{cnf}(\mbox{climb\_mountain\_b\_to\_d},\mbox{hypothesis})$

$( \mbox{warm}(\mbox{situation})\mbox{ and }\mbox{at}(d,\mbox{situation}) ) \ \Rightarrow \ \mbox{at}(b,\mbox{climb}(b,\mbox{situation}))\qquad\mbox{cnf}(\mbox{climb\_mountain\_d\_to\_b},\mbox{hypothesis})$

$\mbox{at}(c,\mbox{situation}) \ \Rightarrow \ \mbox{at}(d,\mbox{go}(d,\mbox{situation}))\qquad\mbox{cnf}(\mbox{go\_c\_to\_d},\mbox{hypothesis})$

$\mbox{at}(d,\mbox{situation}) \ \Rightarrow \ \mbox{at}(c,\mbox{go}(c,\mbox{situation}))\qquad\mbox{cnf}(\mbox{go\_d\_to\_c},\mbox{hypothesis})$

$\mbox{at}(c,\mbox{situation}) \ \Rightarrow \ \mbox{at}(e,\mbox{go}(e,\mbox{situation}))\qquad\mbox{cnf}(\mbox{go\_c\_to\_e},\mbox{hypothesis})$

$\mbox{at}(e,\mbox{situation}) \ \Rightarrow \ \mbox{at}(c,\mbox{go}(c,\mbox{situation}))\qquad\mbox{cnf}(\mbox{go\_e\_to\_c},\mbox{hypothesis})$

$\mbox{at}(d,\mbox{situation}) \ \Rightarrow \ \mbox{at}(f,\mbox{go}(f,\mbox{situation}))\qquad\mbox{cnf}(\mbox{go\_d\_to\_f},\mbox{hypothesis})$

$\mbox{at}(f,\mbox{situation}) \ \Rightarrow \ \mbox{at}(d,\mbox{go}(d,\mbox{situation}))\qquad\mbox{cnf}(\mbox{go\_f\_to\_d},\mbox{hypothesis})$

$\mbox{at}(f,s_0)\qquad\mbox{cnf}(\mbox{initial},\mbox{hypothesis})$

$\neg\,\mbox{at}(a,s)\qquad\mbox{cnf}(\mbox{prove\_you\_can\_get\_to\_a},\mbox{negated\_conjecture})$

\medskip\textbf{PLA014-1.p} Block A on B on C






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

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

$\neg\,\mbox{holds}(\mbox{and}(\mbox{on}(a,b),\mbox{on}(b,c)),\mbox{state})\qquad\mbox{cnf}(\mbox{prove\_ABC},\mbox{negated\_conjecture})$

\medskip\textbf{PLA029-1.p} Blocks world axioms






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

\medskip\textbf{PLA017-1.p} Block A on C






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

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

$\neg\,\mbox{holds}(\mbox{on}(a,c),\mbox{state})\qquad\mbox{cnf}(\mbox{prove\_AC},\mbox{negated\_conjecture})$

\medskip\textbf{PLA023-1.p} Block D on A on C






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

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

$\neg\,\mbox{holds}(\mbox{and}(\mbox{on}(d,a),\mbox{on}(a,c)),\mbox{state})\qquad\mbox{cnf}(\mbox{prove\_DAC},\mbox{negated\_conjecture})$

\medskip\textbf{PLA010-1.p} Block A on D on B






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

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

$\neg\,\mbox{holds}(\mbox{and}(\mbox{on}(a,d),\mbox{on}(d,b)),\mbox{state})\qquad\mbox{cnf}(\mbox{prove\_ADB},\mbox{negated\_conjecture})$

\medskip
\end{document}