\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{SWW461-1.p} Randomly generated entailment of the form F $\to$ G (n = 17)

A randomly generated entailment with n program variables.
 A random graph with pointers and list segments is generated,
 and then some of the segments are folded. The task is to
 prove whether the unfolded version entails the folded one.
 Parameters are chosen so that about half of the generated
 entailments are valid.
 These entailments stress the role of unfolding axioms.




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

$\mbox{heap}(\mbox{sep}(\mbox{next}(x_7,x_2),\mbox{sep}(\mbox{next}(x_6,x_{11}),\mbox{sep}(\mbox{next}(x_{12},x_4),\mbox{sep}(\mbox{lseg}(x_9,x_{10}),\mbox{sep}(\mbox{next}(x_{10},x_{13}),\mbox{sep}(\mbox{next}(x_8,x_7),\mbox{sep}(\mbox{next}(x_{11},x_{13}),\mbox{sep}(\mbox{next}(x_5,x_9),\mbox{sep}(\mbox{next}(x_{16},x_{14}),\mbox{sep}(\mbox{next}(x_1,x_{10}),\mbox{sep}(\mbox{next}(x_{14},x_6),\mbox{sep}(\mbox{next}(x_{17},x_7),\mbox{sep}(\mbox{lseg}(x_2,x_3),\mbox{sep}(\mbox{next}(x_{13},x_5),\mbox{sep}(\mbox{next}(x_3,x_7),\mbox{sep}(\mbox{next}(x_4,x_{12}),\mbox{sep}(\mbox{lseg}(x_{15},x_2),\mbox{emp}))))))))))))))))))\qquad\mbox{cnf}(\mbox{premise}_1,\mbox{hypothesis})$

$\neg\,\mbox{heap}(\mbox{sep}(\mbox{lseg}(x_{16},x_{14}),\mbox{sep}(\mbox{lseg}(x_1,x_{10}),\mbox{sep}(\mbox{lseg}(x_{15},x_2),\mbox{sep}(\mbox{lseg}(x_3,x_7),\mbox{sep}(\mbox{lseg}(x_{10},x_{13}),\mbox{sep}(\mbox{lseg}(x_{12},x_4),\mbox{sep}(\mbox{lseg}(x_{17},x_7),\mbox{sep}(\mbox{lseg}(x_{14},x_6),\mbox{sep}(\mbox{lseg}(x_4,x_{12}),\mbox{sep}(\mbox{lseg}(x_6,x_{13}),\mbox{sep}(\mbox{lseg}(x_8,x_3),\mbox{sep}(\mbox{lseg}(x_{13},x_{10}),\mbox{emp})))))))))))))\qquad\mbox{cnf}(\mbox{conclusion}_1,\mbox{negated\_conjecture})$

\medskip\textbf{SWW446-1.p} Randomly generated entailment of the form F $\to$ $\bot$ (n = 20)

A randomly generated entailment with n program variables.
 Negated equalities and list segments are added at random, with
 specific paramenters so that about half of the generated
 entailments are valid (or, equivalently, F is unsatisfiable).
 Normalization and well-formedness axioms should be enough to
 decide these entailments.




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

$x_6\ne x_{13}\qquad\mbox{cnf}(\mbox{premise}_1,\mbox{hypothesis})$

$x_{11}\ne x_{14}\qquad\mbox{cnf}(\mbox{premise}_2,\mbox{hypothesis})$

$x_3\ne x_7\qquad\mbox{cnf}(\mbox{premise}_3,\mbox{hypothesis})$

$x_7\ne x_{10}\qquad\mbox{cnf}(\mbox{premise}_4,\mbox{hypothesis})$

$x_7\ne x_{14}\qquad\mbox{cnf}(\mbox{premise}_5,\mbox{hypothesis})$

$x_9\ne x_{11}\qquad\mbox{cnf}(\mbox{premise}_6,\mbox{hypothesis})$

$x_{17}\ne x_{19}\qquad\mbox{cnf}(\mbox{premise}_7,\mbox{hypothesis})$

$x_{12}\ne x_{18}\qquad\mbox{cnf}(\mbox{premise}_8,\mbox{hypothesis})$

$x_{12}\ne x_{17}\qquad\mbox{cnf}(\mbox{premise}_9,\mbox{hypothesis})$

$x_2\ne x_{11}\qquad\mbox{cnf}(\mbox{premise}_{10},\mbox{hypothesis})$

$x_2\ne x_{19}\qquad\mbox{cnf}(\mbox{premise}_{11},\mbox{hypothesis})$

$x_2\ne x_{17}\qquad\mbox{cnf}(\mbox{premise}_{12},\mbox{hypothesis})$

$x_{14}\ne x_{16}\qquad\mbox{cnf}(\mbox{premise}_{13},\mbox{hypothesis})$

$x_1\ne x_3\qquad\mbox{cnf}(\mbox{premise}_{14},\mbox{hypothesis})$

$x_4\ne x_{17}\qquad\mbox{cnf}(\mbox{premise}_{15},\mbox{hypothesis})$

$x_{10}\ne x_{19}\qquad\mbox{cnf}(\mbox{premise}_{16},\mbox{hypothesis})$

$x_{10}\ne x_{17}\qquad\mbox{cnf}(\mbox{premise}_{17},\mbox{hypothesis})$

$x_{10}\ne x_{15}\qquad\mbox{cnf}(\mbox{premise}_{18},\mbox{hypothesis})$

$x_{13}\ne x_{18}\qquad\mbox{cnf}(\mbox{premise}_{19},\mbox{hypothesis})$

$x_{13}\ne x_{17}\qquad\mbox{cnf}(\mbox{premise}_{20},\mbox{hypothesis})$

$x_5\ne x_7\qquad\mbox{cnf}(\mbox{premise}_{21},\mbox{hypothesis})$

$x_5\ne x_{20}\qquad\mbox{cnf}(\mbox{premise}_{22},\mbox{hypothesis})$

$\mbox{heap}(\mbox{sep}(\mbox{lseg}(x_{13},x_{10}),\mbox{sep}(\mbox{lseg}(x_{16},x_{10}),\mbox{sep}(\mbox{lseg}(x_{10},x_{19}),\mbox{sep}(\mbox{lseg}(x_{18},x_{14}),\mbox{sep}(\mbox{lseg}(x_1,x_{20}),\mbox{sep}(\mbox{lseg}(x_{14},x_3),\mbox{sep}(\mbox{lseg}(x_{15},x_{14}),\mbox{sep}(\mbox{lseg}(x_{17},x_{10}),\mbox{sep}(\mbox{lseg}(x_7,x_{10}),\mbox{sep}(\mbox{lseg}(x_3,x_{20}),\mbox{sep}(\mbox{lseg}(x_{11},x_2),\mbox{sep}(\mbox{lseg}(x_{11},x_8),\mbox{sep}(\mbox{lseg}(x_6,x_2),\mbox{emp}))))))))))))))\qquad\mbox{cnf}(\mbox{premise}_{23},\mbox{hypothesis})$

$\mbox{heap}(\mbox{emp}) \ \Rightarrow \ x_1 = x_1\qquad\mbox{cnf}(\mbox{conclusion}_1,\mbox{negated\_conjecture})$

\medskip\textbf{SWW455-1.p} Randomly generated entailment of the form F $\to$ G (n = 14)

A randomly generated entailment with n program variables.
 A random graph with pointers and list segments is generated,
 and then some of the segments are folded. The task is to
 prove whether the unfolded version entails the folded one.
 Parameters are chosen so that about half of the generated
 entailments are valid.
 These entailments stress the role of unfolding axioms.




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

$\mbox{heap}(\mbox{sep}(\mbox{next}(x_3,x_6),\mbox{sep}(\mbox{next}(x_2,x_{12}),\mbox{sep}(\mbox{lseg}(x_1,x_7),\mbox{sep}(\mbox{next}(x_{14},x_{11}),\mbox{sep}(\mbox{next}(x_8,x_{11}),\mbox{sep}(\mbox{next}(x_{12},x_1),\mbox{sep}(\mbox{next}(x_{13},x_4),\mbox{sep}(\mbox{next}(x_{10},x_5),\mbox{sep}(\mbox{next}(x_5,x_2),\mbox{sep}(\mbox{next}(x_4,x_{14}),\mbox{sep}(\mbox{lseg}(x_9,x_4),\mbox{sep}(\mbox{lseg}(x_6,x_8),\mbox{sep}(\mbox{next}(x_{11},x_{13}),\mbox{sep}(\mbox{lseg}(x_7,x_{14}),\mbox{emp})))))))))))))))\qquad\mbox{cnf}(\mbox{premise}_1,\mbox{hypothesis})$

$\neg\,\mbox{heap}(\mbox{sep}(\mbox{lseg}(x_9,x_4),\mbox{sep}(\mbox{lseg}(x_{10},x_5),\mbox{sep}(\mbox{lseg}(x_3,x_{11}),\mbox{sep}(\mbox{lseg}(x_4,x_{14}),\mbox{sep}(\mbox{lseg}(x_5,x_4),\mbox{emp}))))))\qquad\mbox{cnf}(\mbox{conclusion}_1,\mbox{negated\_conjecture})$

\medskip\textbf{SWW462-1.p} Randomly generated entailment of the form F $\to$ G (n = 17)

A randomly generated entailment with n program variables.
 A random graph with pointers and list segments is generated,
 and then some of the segments are folded. The task is to
 prove whether the unfolded version entails the folded one.
 Parameters are chosen so that about half of the generated
 entailments are valid.
 These entailments stress the role of unfolding axioms.




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

$\mbox{heap}(\mbox{sep}(\mbox{next}(x_{15},x_2),\mbox{sep}(\mbox{lseg}(x_{10},x_{17}),\mbox{sep}(\mbox{next}(x_3,x_5),\mbox{sep}(\mbox{lseg}(x_{11},x_{17}),\mbox{sep}(\mbox{next}(x_{12},x_{13}),\mbox{sep}(\mbox{next}(x_6,x_7),\mbox{sep}(\mbox{next}(x_{16},x_{11}),\mbox{sep}(\mbox{next}(x_7,x_{15}),\mbox{sep}(\mbox{lseg}(x_1,x_{11}),\mbox{sep}(\mbox{next}(x_2,x_8),\mbox{sep}(\mbox{next}(x_9,x_1),\mbox{sep}(\mbox{next}(x_{14},x_8),\mbox{sep}(\mbox{lseg}(x_{17},x_{15}),\mbox{sep}(\mbox{lseg}(x_{13},x_{12}),\mbox{sep}(\mbox{next}(x_4,x_{11}),\mbox{sep}(\mbox{next}(x_8,x_6),\mbox{sep}(\mbox{next}(x_5,x_4),\mbox{emp}))))))))))))))))))\qquad\mbox{cnf}(\mbox{premise}_1,\mbox{hypothesis})$

$\neg\,\mbox{heap}(\mbox{sep}(\mbox{lseg}(x_7,x_{15}),\mbox{sep}(\mbox{lseg}(x_{16},x_{11}),\mbox{sep}(\mbox{lseg}(x_9,x_1),\mbox{sep}(\mbox{lseg}(x_{12},x_{13}),\mbox{sep}(\mbox{lseg}(x_{10},x_{17}),\mbox{sep}(\mbox{lseg}(x_3,x_5),\mbox{sep}(\mbox{lseg}(x_{14},x_8),\mbox{sep}(\mbox{lseg}(x_5,x_4),\mbox{sep}(\mbox{lseg}(x_1,x_{11}),\mbox{sep}(\mbox{lseg}(x_{13},x_{12}),\mbox{sep}(\mbox{lseg}(x_4,x_7),\mbox{emp}))))))))))))\qquad\mbox{cnf}(\mbox{conclusion}_1,\mbox{negated\_conjecture})$

\medskip\textbf{SWW448-1.p} Randomly generated entailment of the form F $\to$ G (n = 10)

A randomly generated entailment with n program variables.
 A random graph with pointers and list segments is generated,
 and then some of the segments are folded. The task is to
 prove whether the unfolded version entails the folded one.
 Parameters are chosen so that about half of the generated
 entailments are valid.
 These entailments stress the role of unfolding axioms.




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

$\mbox{heap}(\mbox{sep}(\mbox{next}(x_5,x_{10}),\mbox{sep}(\mbox{lseg}(x_9,x_7),\mbox{sep}(\mbox{next}(x_2,x_7),\mbox{sep}(\mbox{next}(x_4,x_7),\mbox{sep}(\mbox{next}(x_6,x_4),\mbox{sep}(\mbox{next}(x_7,x_3),\mbox{sep}(\mbox{next}(x_1,x_2),\mbox{sep}(\mbox{next}(x_{10},x_1),\mbox{sep}(\mbox{next}(x_8,x_4),\mbox{sep}(\mbox{next}(x_3,x_5),\mbox{emp})))))))))))\qquad\mbox{cnf}(\mbox{premise}_1,\mbox{hypothesis})$

$\neg\,\mbox{heap}(\mbox{sep}(\mbox{lseg}(x_3,x_5),\mbox{sep}(\mbox{lseg}(x_8,x_4),\mbox{sep}(\mbox{lseg}(x_9,x_7),\mbox{sep}(\mbox{lseg}(x_6,x_7),\mbox{sep}(\mbox{lseg}(x_5,x_3),\mbox{emp}))))))\qquad\mbox{cnf}(\mbox{conclusion}_1,\mbox{negated\_conjecture})$

\medskip\textbf{SWW099+1.p} If one is Boolean then exists1(P) = exists2(P).






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

$\forall p{:}\;( ( \mbox{bool}(\mbox{exists}_1(p))\mbox{ or }\mbox{bool}(\mbox{exists}_2(p)) ) \ \Rightarrow \ \mbox{exists}_1(p) = \mbox{exists}_2(p) )\qquad\mbox{fof}(\mbox{exists1\_exists}_2,\mbox{conjecture})$

\medskip\textbf{SWW402-1.p} Verification Condition generated by Smallfoot

This is one of the verification conditions that were gathered
 from the output of Smallfoot when checking assertions on list
 manipulating programs from its own benchmark suite.




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

$\mbox{nil}\ne x_1\qquad\mbox{cnf}(\mbox{premise}_1,\mbox{hypothesis})$

$\mbox{nil}\ne x_2\qquad\mbox{cnf}(\mbox{premise}_2,\mbox{hypothesis})$

$\mbox{nil}\ne x_3\qquad\mbox{cnf}(\mbox{premise}_3,\mbox{hypothesis})$

$\mbox{nil}\ne x_4\qquad\mbox{cnf}(\mbox{premise}_4,\mbox{hypothesis})$

$\mbox{nil}\ne x_5\qquad\mbox{cnf}(\mbox{premise}_5,\mbox{hypothesis})$

$\mbox{nil}\ne x_6\qquad\mbox{cnf}(\mbox{premise}_6,\mbox{hypothesis})$

$x_1\ne x_6\qquad\mbox{cnf}(\mbox{premise}_7,\mbox{hypothesis})$

$x_2\ne x_6\qquad\mbox{cnf}(\mbox{premise}_8,\mbox{hypothesis})$

$x_3\ne x_4\qquad\mbox{cnf}(\mbox{premise}_9,\mbox{hypothesis})$

$x_3\ne x_5\qquad\mbox{cnf}(\mbox{premise}_{10},\mbox{hypothesis})$

$\mbox{heap}(\mbox{sep}(\mbox{next}(x_1,x_6),\mbox{sep}(\mbox{lseg}(x_2,x_1),\mbox{sep}(\mbox{next}(x_6,x_2),\mbox{emp}))))\qquad\mbox{cnf}(\mbox{premise}_{11},\mbox{hypothesis})$

$\mbox{heap}(\mbox{sep}(\mbox{lseg}(x_7,x_6),\mbox{sep}(\mbox{next}(x_6,x_7),\mbox{emp}))) \ \Rightarrow \ x_7 = x_6\qquad\mbox{cnf}(\mbox{conclusion}_1,\mbox{negated\_conjecture})$

\medskip\textbf{SWW097+1.p} Equivalenace of the semantic and syntactic definition of lazy\_and 






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

$\forall p,q{:}\;\mbox{lazy\_and}_1(p,q) = \mbox{lazy\_and}_2(p,q)\qquad\mbox{fof}(\mbox{lazy\_and1\_lazy\_and}_2,\mbox{conjecture})$

\medskip\textbf{SWW431-1.p} Randomly generated entailment of the form F $\to$ $\bot$ (n = 13)

A randomly generated entailment with n program variables.
 Negated equalities and list segments are added at random, with
 specific paramenters so that about half of the generated
 entailments are valid (or, equivalently, F is unsatisfiable).
 Normalization and well-formedness axioms should be enough to
 decide these entailments.




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

$x_8\ne x_{12}\qquad\mbox{cnf}(\mbox{premise}_1,\mbox{hypothesis})$

$x_6\ne x_7\qquad\mbox{cnf}(\mbox{premise}_2,\mbox{hypothesis})$

$x_6\ne x_{13}\qquad\mbox{cnf}(\mbox{premise}_3,\mbox{hypothesis})$

$x_3\ne x_8\qquad\mbox{cnf}(\mbox{premise}_4,\mbox{hypothesis})$

$x_3\ne x_5\qquad\mbox{cnf}(\mbox{premise}_5,\mbox{hypothesis})$

$x_7\ne x_8\qquad\mbox{cnf}(\mbox{premise}_6,\mbox{hypothesis})$

$x_7\ne x_{11}\qquad\mbox{cnf}(\mbox{premise}_7,\mbox{hypothesis})$

$x_{10}\ne x_{11}\qquad\mbox{cnf}(\mbox{premise}_8,\mbox{hypothesis})$

$x_2\ne x_6\qquad\mbox{cnf}(\mbox{premise}_9,\mbox{hypothesis})$

$x_2\ne x_3\qquad\mbox{cnf}(\mbox{premise}_{10},\mbox{hypothesis})$

$x_2\ne x_9\qquad\mbox{cnf}(\mbox{premise}_{11},\mbox{hypothesis})$

$x_5\ne x_7\qquad\mbox{cnf}(\mbox{premise}_{12},\mbox{hypothesis})$

$\mbox{heap}(\mbox{sep}(\mbox{lseg}(x_5,x_3),\mbox{sep}(\mbox{lseg}(x_{10},x_8),\mbox{sep}(\mbox{lseg}(x_{13},x_8),\mbox{sep}(\mbox{lseg}(x_1,x_{11}),\mbox{sep}(\mbox{lseg}(x_4,x_9),\mbox{sep}(\mbox{lseg}(x_2,x_9),\mbox{sep}(\mbox{lseg}(x_{12},x_7),\mbox{sep}(\mbox{lseg}(x_9,x_2),\mbox{sep}(\mbox{lseg}(x_7,x_{10}),\mbox{sep}(\mbox{lseg}(x_{11},x_{12}),\mbox{sep}(\mbox{lseg}(x_{11},x_7),\mbox{sep}(\mbox{lseg}(x_{11},x_1),\mbox{emp})))))))))))))\qquad\mbox{cnf}(\mbox{premise}_{13},\mbox{hypothesis})$

$\mbox{heap}(\mbox{emp}) \ \Rightarrow \ x_1 = x_1\qquad\mbox{cnf}(\mbox{conclusion}_1,\mbox{negated\_conjecture})$

\medskip\textbf{SWW418-1.p} Verification Condition generated by Smallfoot

This is one of the verification conditions that were gathered
 from the output of Smallfoot when checking assertions on list
 manipulating programs from its own benchmark suite.




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

$\mbox{nil}\ne x_1\qquad\mbox{cnf}(\mbox{premise}_1,\mbox{hypothesis})$

$x_2\ne x_1\qquad\mbox{cnf}(\mbox{premise}_2,\mbox{hypothesis})$

$\mbox{heap}(\mbox{sep}(\mbox{lseg}(x_2,\mbox{nil}),\mbox{sep}(\mbox{next}(x_1,x_2),\mbox{emp})))\qquad\mbox{cnf}(\mbox{premise}_3,\mbox{hypothesis})$

$\neg\,\mbox{heap}(\mbox{sep}(\mbox{lseg}(x_2,\mbox{nil}),\mbox{emp}))\qquad\mbox{cnf}(\mbox{conclusion}_1,\mbox{negated\_conjecture})$

\medskip\textbf{SWW674$\wedge$1.p} ICL logic based upon modal logic based upon simple type theory






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

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

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

$\mbox{include}(\mbox{'Axioms/SWV008\string^2.ax'})$

\medskip\textbf{SWW405-1.p} Verification Condition generated by Smallfoot

This is one of the verification conditions that were gathered
 from the output of Smallfoot when checking assertions on list
 manipulating programs from its own benchmark suite.




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

$\mbox{nil}\ne x_1\qquad\mbox{cnf}(\mbox{premise}_1,\mbox{hypothesis})$

$\mbox{nil}\ne x_2\qquad\mbox{cnf}(\mbox{premise}_2,\mbox{hypothesis})$

$\mbox{nil}\ne x_3\qquad\mbox{cnf}(\mbox{premise}_3,\mbox{hypothesis})$

$x_1\ne x_2\qquad\mbox{cnf}(\mbox{premise}_4,\mbox{hypothesis})$

$x_2\ne x_3\qquad\mbox{cnf}(\mbox{premise}_5,\mbox{hypothesis})$

$\mbox{heap}(\mbox{sep}(\mbox{lseg}(x_3,x_1),\mbox{sep}(\mbox{next}(x_1,x_3),\mbox{emp})))\qquad\mbox{cnf}(\mbox{premise}_6,\mbox{hypothesis})$

$\neg\,\mbox{heap}(\mbox{sep}(\mbox{lseg}(x_4,x_1),\mbox{sep}(\mbox{next}(x_1,x_4),\mbox{emp})))\qquad\mbox{cnf}(\mbox{conclusion}_1,\mbox{negated\_conjecture})$

\medskip\textbf{SWW407-1.p} Verification Condition generated by Smallfoot

This is one of the verification conditions that were gathered
 from the output of Smallfoot when checking assertions on list
 manipulating programs from its own benchmark suite.




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

$\mbox{nil}\ne x_1\qquad\mbox{cnf}(\mbox{premise}_1,\mbox{hypothesis})$

$\mbox{nil}\ne x_2\qquad\mbox{cnf}(\mbox{premise}_2,\mbox{hypothesis})$

$\mbox{nil}\ne x_3\qquad\mbox{cnf}(\mbox{premise}_3,\mbox{hypothesis})$

$x_1\ne x_4\qquad\mbox{cnf}(\mbox{premise}_4,\mbox{hypothesis})$

$x_1\ne x_2\qquad\mbox{cnf}(\mbox{premise}_5,\mbox{hypothesis})$

$x_4\ne x_2\qquad\mbox{cnf}(\mbox{premise}_6,\mbox{hypothesis})$

$x_4\ne x_3\qquad\mbox{cnf}(\mbox{premise}_7,\mbox{hypothesis})$

$x_2\ne x_3\qquad\mbox{cnf}(\mbox{premise}_8,\mbox{hypothesis})$

$\mbox{heap}(\mbox{sep}(\mbox{next}(x_1,x_2),\mbox{sep}(\mbox{lseg}(x_3,x_1),\mbox{sep}(\mbox{lseg}(x_4,\mbox{nil}),\mbox{sep}(\mbox{next}(x_2,x_4),\mbox{emp})))))\qquad\mbox{cnf}(\mbox{premise}_9,\mbox{hypothesis})$

$\neg\,\mbox{heap}(\mbox{sep}(\mbox{lseg}(x_4,\mbox{nil}),\mbox{sep}(\mbox{next}(x_2,x_4),\mbox{sep}(\mbox{lseg}(x_3,x_2),\mbox{emp}))))\qquad\mbox{cnf}(\mbox{conclusion}_1,\mbox{negated\_conjecture})$

\medskip\textbf{SWW421-1.p} Verification Condition generated by Smallfoot

This is one of the verification conditions that were gathered
 from the output of Smallfoot when checking assertions on list
 manipulating programs from its own benchmark suite.




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

$\mbox{nil}\ne x_1\qquad\mbox{cnf}(\mbox{premise}_1,\mbox{hypothesis})$

$x_2\ne x_1\qquad\mbox{cnf}(\mbox{premise}_2,\mbox{hypothesis})$

$x_1\ne x_3\qquad\mbox{cnf}(\mbox{premise}_3,\mbox{hypothesis})$

$\mbox{heap}(\mbox{sep}(\mbox{lseg}(x_2,x_3),\mbox{sep}(\mbox{next}(x_1,x_2),\mbox{emp})))\qquad\mbox{cnf}(\mbox{premise}_4,\mbox{hypothesis})$

$\neg\,\mbox{heap}(\mbox{sep}(\mbox{lseg}(x_1,x_3),\mbox{emp}))\qquad\mbox{cnf}(\mbox{conclusion}_1,\mbox{negated\_conjecture})$

\medskip\textbf{SWW468-1.p} Randomly generated entailment of the form F $\to$ G (n = 20)

A randomly generated entailment with n program variables.
 A random graph with pointers and list segments is generated,
 and then some of the segments are folded. The task is to
 prove whether the unfolded version entails the folded one.
 Parameters are chosen so that about half of the generated
 entailments are valid.
 These entailments stress the role of unfolding axioms.




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

$\mbox{heap}(\mbox{sep}(\mbox{next}(x_{14},x_{13}),\mbox{sep}(\mbox{next}(x_{18},x_1),\mbox{sep}(\mbox{next}(x_{15},x_3),\mbox{sep}(\mbox{next}(x_{20},x_9),\mbox{sep}(\mbox{next}(x_6,x_5),\mbox{sep}(\mbox{next}(x_8,x_{15}),\mbox{sep}(\mbox{lseg}(x_4,x_3),\mbox{sep}(\mbox{next}(x_{10},x_8),\mbox{sep}(\mbox{next}(x_1,x_{19}),\mbox{sep}(\mbox{lseg}(x_2,x_9),\mbox{sep}(\mbox{next}(x_{12},x_7),\mbox{sep}(\mbox{next}(x_{17},x_4),\mbox{sep}(\mbox{next}(x_{16},x_{17}),\mbox{sep}(\mbox{next}(x_9,x_{11}),\mbox{sep}(\mbox{lseg}(x_5,x_{16}),\mbox{sep}(\mbox{next}(x_{13},x_{18}),\mbox{sep}(\mbox{lseg}(x_{11},x_7),\mbox{sep}(\mbox{next}(x_7,x_{18}),\mbox{sep}(\mbox{lseg}(x_{19},x_{14}),\mbox{sep}(\mbox{next}(x_3,x_{17}),\mbox{emp})))))))))))))))))))))\qquad\mbox{cnf}(\mbox{premise}_1,\mbox{hypothesis})$

$\neg\,\mbox{heap}(\mbox{sep}(\mbox{lseg}(x_{13},x_{18}),\mbox{sep}(\mbox{lseg}(x_{20},x_9),\mbox{sep}(\mbox{lseg}(x_{10},x_8),\mbox{sep}(\mbox{lseg}(x_2,x_7),\mbox{sep}(\mbox{lseg}(x_6,x_{17}),\mbox{sep}(\mbox{lseg}(x_4,x_3),\mbox{sep}(\mbox{lseg}(x_{12},x_{13}),\mbox{sep}(\mbox{lseg}(x_8,x_4),\mbox{emp})))))))))\qquad\mbox{cnf}(\mbox{conclusion}_1,\mbox{negated\_conjecture})$

\medskip\textbf{SWW101+1.p} false1 = false2






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

$\mbox{false}_1 = \mbox{false}_2\qquad\mbox{fof}(\mbox{false1\_false}_2,\mbox{conjecture})$

\medskip\textbf{SWW443-1.p} Randomly generated entailment of the form F $\to$ $\bot$ (n = 19)

A randomly generated entailment with n program variables.
 Negated equalities and list segments are added at random, with
 specific paramenters so that about half of the generated
 entailments are valid (or, equivalently, F is unsatisfiable).
 Normalization and well-formedness axioms should be enough to
 decide these entailments.




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

$x_6\ne x_{13}\qquad\mbox{cnf}(\mbox{premise}_1,\mbox{hypothesis})$

$x_{11}\ne x_{16}\qquad\mbox{cnf}(\mbox{premise}_2,\mbox{hypothesis})$

$x_{11}\ne x_{13}\qquad\mbox{cnf}(\mbox{premise}_3,\mbox{hypothesis})$

$x_{11}\ne x_{15}\qquad\mbox{cnf}(\mbox{premise}_4,\mbox{hypothesis})$

$x_3\ne x_4\qquad\mbox{cnf}(\mbox{premise}_5,\mbox{hypothesis})$

$x_3\ne x_5\qquad\mbox{cnf}(\mbox{premise}_6,\mbox{hypothesis})$

$x_{17}\ne x_{18}\qquad\mbox{cnf}(\mbox{premise}_7,\mbox{hypothesis})$

$x_2\ne x_8\qquad\mbox{cnf}(\mbox{premise}_8,\mbox{hypothesis})$

$x_2\ne x_{13}\qquad\mbox{cnf}(\mbox{premise}_9,\mbox{hypothesis})$

$x_2\ne x_{14}\qquad\mbox{cnf}(\mbox{premise}_{10},\mbox{hypothesis})$

$x_{14}\ne x_{18}\qquad\mbox{cnf}(\mbox{premise}_{11},\mbox{hypothesis})$

$x_{14}\ne x_{16}\qquad\mbox{cnf}(\mbox{premise}_{12},\mbox{hypothesis})$

$x_8\ne x_9\qquad\mbox{cnf}(\mbox{premise}_{13},\mbox{hypothesis})$

$x_4\ne x_{18}\qquad\mbox{cnf}(\mbox{premise}_{14},\mbox{hypothesis})$

$x_4\ne x_{19}\qquad\mbox{cnf}(\mbox{premise}_{15},\mbox{hypothesis})$

$x_1\ne x_6\qquad\mbox{cnf}(\mbox{premise}_{16},\mbox{hypothesis})$

$x_1\ne x_{13}\qquad\mbox{cnf}(\mbox{premise}_{17},\mbox{hypothesis})$

$x_1\ne x_{15}\qquad\mbox{cnf}(\mbox{premise}_{18},\mbox{hypothesis})$

$x_1\ne x_{14}\qquad\mbox{cnf}(\mbox{premise}_{19},\mbox{hypothesis})$

$x_{13}\ne x_{19}\qquad\mbox{cnf}(\mbox{premise}_{20},\mbox{hypothesis})$

$x_5\ne x_{16}\qquad\mbox{cnf}(\mbox{premise}_{21},\mbox{hypothesis})$

$x_5\ne x_{15}\qquad\mbox{cnf}(\mbox{premise}_{22},\mbox{hypothesis})$

$\mbox{heap}(\mbox{sep}(\mbox{lseg}(x_{10},x_1),\mbox{sep}(\mbox{lseg}(x_{18},x_{15}),\mbox{sep}(\mbox{lseg}(x_1,x_{14}),\mbox{sep}(\mbox{lseg}(x_1,x_3),\mbox{sep}(\mbox{lseg}(x_{12},x_{13}),\mbox{sep}(\mbox{lseg}(x_2,x_5),\mbox{sep}(\mbox{lseg}(x_2,x_{12}),\mbox{sep}(\mbox{lseg}(x_2,x_{18}),\mbox{sep}(\mbox{lseg}(x_2,x_8),\mbox{sep}(\mbox{lseg}(x_9,x_5),\mbox{sep}(\mbox{lseg}(x_7,x_5),\mbox{sep}(\mbox{lseg}(x_{11},x_9),\mbox{sep}(\mbox{lseg}(x_{11},x_7),\mbox{emp}))))))))))))))\qquad\mbox{cnf}(\mbox{premise}_{23},\mbox{hypothesis})$

$\mbox{heap}(\mbox{emp}) \ \Rightarrow \ x_1 = x_1\qquad\mbox{cnf}(\mbox{conclusion}_1,\mbox{negated\_conjecture})$

\medskip\textbf{SWW429-1.p} Randomly generated entailment of the form F $\to$ $\bot$ (n = 12)

A randomly generated entailment with n program variables.
 Negated equalities and list segments are added at random, with
 specific paramenters so that about half of the generated
 entailments are valid (or, equivalently, F is unsatisfiable).
 Normalization and well-formedness axioms should be enough to
 decide these entailments.




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

$x_4\ne x_7\qquad\mbox{cnf}(\mbox{premise}_1,\mbox{hypothesis})$

$x_4\ne x_{10}\qquad\mbox{cnf}(\mbox{premise}_2,\mbox{hypothesis})$

$x_3\ne x_8\qquad\mbox{cnf}(\mbox{premise}_3,\mbox{hypothesis})$

$x_2\ne x_9\qquad\mbox{cnf}(\mbox{premise}_4,\mbox{hypothesis})$

$x_5\ne x_9\qquad\mbox{cnf}(\mbox{premise}_5,\mbox{hypothesis})$

$\mbox{heap}(\mbox{sep}(\mbox{lseg}(x_5,x_1),\mbox{sep}(\mbox{lseg}(x_7,x_{12}),\mbox{sep}(\mbox{lseg}(x_7,x_8),\mbox{sep}(\mbox{lseg}(x_3,x_5),\mbox{sep}(\mbox{lseg}(x_3,x_{12}),\mbox{sep}(\mbox{lseg}(x_4,x_{12}),\mbox{sep}(\mbox{lseg}(x_4,x_7),\mbox{sep}(\mbox{lseg}(x_1,x_6),\mbox{sep}(\mbox{lseg}(x_6,x_9),\mbox{sep}(\mbox{lseg}(x_6,x_7),\mbox{sep}(\mbox{lseg}(x_8,x_{11}),\mbox{emp}))))))))))))\qquad\mbox{cnf}(\mbox{premise}_6,\mbox{hypothesis})$

$\mbox{heap}(\mbox{emp}) \ \Rightarrow \ x_1 = x_1\qquad\mbox{cnf}(\mbox{conclusion}_1,\mbox{negated\_conjecture})$

\medskip\textbf{SWW416-1.p} Verification Condition generated by Smallfoot

This is one of the verification conditions that were gathered
 from the output of Smallfoot when checking assertions on list
 manipulating programs from its own benchmark suite.




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

$\mbox{nil}\ne x_1\qquad\mbox{cnf}(\mbox{premise}_1,\mbox{hypothesis})$

$x_1\ne x_2\qquad\mbox{cnf}(\mbox{premise}_2,\mbox{hypothesis})$

$x_1\ne x_3\qquad\mbox{cnf}(\mbox{premise}_3,\mbox{hypothesis})$

$\mbox{heap}(\mbox{sep}(\mbox{lseg}(x_3,\mbox{nil}),\mbox{sep}(\mbox{lseg}(x_1,\mbox{nil}),\mbox{emp})))\qquad\mbox{cnf}(\mbox{premise}_4,\mbox{hypothesis})$

$\neg\,\mbox{heap}(\mbox{sep}(\mbox{lseg}(x_1,\mbox{nil}),\mbox{emp}))\qquad\mbox{cnf}(\mbox{conclusion}_1,\mbox{negated\_conjecture})$

\medskip\textbf{SWW430-1.p} Randomly generated entailment of the form F $\to$ $\bot$ (n = 12)

A randomly generated entailment with n program variables.
 Negated equalities and list segments are added at random, with
 specific paramenters so that about half of the generated
 entailments are valid (or, equivalently, F is unsatisfiable).
 Normalization and well-formedness axioms should be enough to
 decide these entailments.




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

$x_3\ne x_{11}\qquad\mbox{cnf}(\mbox{premise}_1,\mbox{hypothesis})$

$x_3\ne x_{12}\qquad\mbox{cnf}(\mbox{premise}_2,\mbox{hypothesis})$

$x_7\ne x_{12}\qquad\mbox{cnf}(\mbox{premise}_3,\mbox{hypothesis})$

$x_2\ne x_{11}\qquad\mbox{cnf}(\mbox{premise}_4,\mbox{hypothesis})$

$x_2\ne x_{10}\qquad\mbox{cnf}(\mbox{premise}_5,\mbox{hypothesis})$

$\mbox{heap}(\mbox{sep}(\mbox{lseg}(x_5,x_2),\mbox{sep}(\mbox{lseg}(x_5,x_7),\mbox{sep}(\mbox{lseg}(x_5,x_4),\mbox{sep}(\mbox{lseg}(x_{12},x_1),\mbox{sep}(\mbox{lseg}(x_{12},x_6),\mbox{sep}(\mbox{lseg}(x_2,x_{12}),\mbox{sep}(\mbox{lseg}(x_9,x_{10}),\mbox{sep}(\mbox{lseg}(x_3,x_{11}),\mbox{sep}(\mbox{lseg}(x_3,x_1),\mbox{sep}(\mbox{lseg}(x_3,x_6),\mbox{sep}(\mbox{lseg}(x_4,x_9),\mbox{sep}(\mbox{lseg}(x_4,x_8),\mbox{sep}(\mbox{lseg}(x_{11},x_8),\mbox{sep}(\mbox{lseg}(x_{11},x_6),\mbox{sep}(\mbox{lseg}(x_1,x_9),\mbox{sep}(\mbox{lseg}(x_1,x_8),\mbox{sep}(\mbox{lseg}(x_6,x_2),\mbox{emp}))))))))))))))))))\qquad\mbox{cnf}(\mbox{premise}_6,\mbox{hypothesis})$

$\mbox{heap}(\mbox{emp}) \ \Rightarrow \ x_1 = x_1\qquad\mbox{cnf}(\mbox{conclusion}_1,\mbox{negated\_conjecture})$

\medskip\textbf{SWW400-1.p} Verification Condition generated by Smallfoot

This is one of the verification conditions that were gathered
 from the output of Smallfoot when checking assertions on list
 manipulating programs from its own benchmark suite.




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

$\mbox{nil}\ne x_1\qquad\mbox{cnf}(\mbox{premise}_1,\mbox{hypothesis})$

$\mbox{nil}\ne x_2\qquad\mbox{cnf}(\mbox{premise}_2,\mbox{hypothesis})$

$\mbox{heap}(\mbox{sep}(\mbox{next}(x_2,\mbox{nil}),\mbox{sep}(\mbox{lseg}(x_1,x_2),\mbox{emp})))\qquad\mbox{cnf}(\mbox{premise}_3,\mbox{hypothesis})$

$\neg\,\mbox{heap}(\mbox{sep}(\mbox{lseg}(x_1,\mbox{nil}),\mbox{emp}))\qquad\mbox{cnf}(\mbox{conclusion}_1,\mbox{negated\_conjecture})$

\medskip\textbf{SWW420-1.p} Verification Condition generated by Smallfoot

This is one of the verification conditions that were gathered
 from the output of Smallfoot when checking assertions on list
 manipulating programs from its own benchmark suite.




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

$\mbox{nil}\ne x_1\qquad\mbox{cnf}(\mbox{premise}_1,\mbox{hypothesis})$

$x_2\ne x_1\qquad\mbox{cnf}(\mbox{premise}_2,\mbox{hypothesis})$

$x_1\ne x_3\qquad\mbox{cnf}(\mbox{premise}_3,\mbox{hypothesis})$

$\mbox{heap}(\mbox{sep}(\mbox{lseg}(x_3,\mbox{nil}),\mbox{sep}(\mbox{lseg}(x_2,\mbox{nil}),\mbox{sep}(\mbox{next}(x_1,x_2),\mbox{emp}))))\qquad\mbox{cnf}(\mbox{premise}_4,\mbox{hypothesis})$

$\neg\,\mbox{heap}(\mbox{sep}(\mbox{lseg}(x_2,\mbox{nil}),\mbox{sep}(\mbox{next}(x_1,x_2),\mbox{sep}(\mbox{lseg}(x_1,x_1),\mbox{emp}))))\qquad\mbox{cnf}(\mbox{conclusion}_1,\mbox{negated\_conjecture})$

\medskip\textbf{SWW439-1.p} Randomly generated entailment of the form F $\to$ $\bot$ (n = 17)

A randomly generated entailment with n program variables.
 Negated equalities and list segments are added at random, with
 specific paramenters so that about half of the generated
 entailments are valid (or, equivalently, F is unsatisfiable).
 Normalization and well-formedness axioms should be enough to
 decide these entailments.




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

$x_6\ne x_{11}\qquad\mbox{cnf}(\mbox{premise}_1,\mbox{hypothesis})$

$x_6\ne x_{14}\qquad\mbox{cnf}(\mbox{premise}_2,\mbox{hypothesis})$

$x_3\ne x_8\qquad\mbox{cnf}(\mbox{premise}_3,\mbox{hypothesis})$

$x_3\ne x_{15}\qquad\mbox{cnf}(\mbox{premise}_4,\mbox{hypothesis})$

$x_7\ne x_8\qquad\mbox{cnf}(\mbox{premise}_5,\mbox{hypothesis})$

$x_{14}\ne x_{16}\qquad\mbox{cnf}(\mbox{premise}_6,\mbox{hypothesis})$

$x_8\ne x_{11}\qquad\mbox{cnf}(\mbox{premise}_7,\mbox{hypothesis})$

$x_8\ne x_{15}\qquad\mbox{cnf}(\mbox{premise}_8,\mbox{hypothesis})$

$x_1\ne x_{14}\qquad\mbox{cnf}(\mbox{premise}_9,\mbox{hypothesis})$

$x_{13}\ne x_{15}\qquad\mbox{cnf}(\mbox{premise}_{10},\mbox{hypothesis})$

$x_{10}\ne x_{11}\qquad\mbox{cnf}(\mbox{premise}_{11},\mbox{hypothesis})$

$x_{10}\ne x_{13}\qquad\mbox{cnf}(\mbox{premise}_{12},\mbox{hypothesis})$

$x_5\ne x_{16}\qquad\mbox{cnf}(\mbox{premise}_{13},\mbox{hypothesis})$

$x_5\ne x_9\qquad\mbox{cnf}(\mbox{premise}_{14},\mbox{hypothesis})$

$\mbox{heap}(\mbox{sep}(\mbox{lseg}(x_{13},x_5),\mbox{sep}(\mbox{lseg}(x_{13},x_2),\mbox{sep}(\mbox{lseg}(x_{10},x_3),\mbox{sep}(\mbox{lseg}(x_1,x_{10}),\mbox{sep}(\mbox{lseg}(x_4,x_{12}),\mbox{sep}(\mbox{lseg}(x_2,x_{15}),\mbox{sep}(\mbox{lseg}(x_2,x_{17}),\mbox{sep}(\mbox{lseg}(x_2,x_{16}),\mbox{sep}(\mbox{lseg}(x_{12},x_{16}),\mbox{sep}(\mbox{lseg}(x_9,x_{14}),\mbox{sep}(\mbox{lseg}(x_7,x_1),\mbox{sep}(\mbox{lseg}(x_3,x_9),\mbox{sep}(\mbox{lseg}(x_6,x_2),\mbox{emp}))))))))))))))\qquad\mbox{cnf}(\mbox{premise}_{15},\mbox{hypothesis})$

$\mbox{heap}(\mbox{emp}) \ \Rightarrow \ x_1 = x_1\qquad\mbox{cnf}(\mbox{conclusion}_1,\mbox{negated\_conjecture})$

\medskip\textbf{SWW438-1.p} Randomly generated entailment of the form F $\to$ $\bot$ (n = 16)

A randomly generated entailment with n program variables.
 Negated equalities and list segments are added at random, with
 specific paramenters so that about half of the generated
 entailments are valid (or, equivalently, F is unsatisfiable).
 Normalization and well-formedness axioms should be enough to
 decide these entailments.




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

$x_6\ne x_{11}\qquad\mbox{cnf}(\mbox{premise}_1,\mbox{hypothesis})$

$x_6\ne x_7\qquad\mbox{cnf}(\mbox{premise}_2,\mbox{hypothesis})$

$x_3\ne x_{10}\qquad\mbox{cnf}(\mbox{premise}_3,\mbox{hypothesis})$

$x_3\ne x_{14}\qquad\mbox{cnf}(\mbox{premise}_4,\mbox{hypothesis})$

$x_7\ne x_{15}\qquad\mbox{cnf}(\mbox{premise}_5,\mbox{hypothesis})$

$x_9\ne x_{15}\qquad\mbox{cnf}(\mbox{premise}_6,\mbox{hypothesis})$

$x_9\ne x_{14}\qquad\mbox{cnf}(\mbox{premise}_7,\mbox{hypothesis})$

$x_2\ne x_{16}\qquad\mbox{cnf}(\mbox{premise}_8,\mbox{hypothesis})$

$x_2\ne x_5\qquad\mbox{cnf}(\mbox{premise}_9,\mbox{hypothesis})$

$x_{14}\ne x_{16}\qquad\mbox{cnf}(\mbox{premise}_{10},\mbox{hypothesis})$

$x_{10}\ne x_{11}\qquad\mbox{cnf}(\mbox{premise}_{11},\mbox{hypothesis})$

$x_{13}\ne x_{15}\qquad\mbox{cnf}(\mbox{premise}_{12},\mbox{hypothesis})$

$x_5\ne x_9\qquad\mbox{cnf}(\mbox{premise}_{13},\mbox{hypothesis})$

$x_5\ne x_{16}\qquad\mbox{cnf}(\mbox{premise}_{14},\mbox{hypothesis})$

$x_5\ne x_{15}\qquad\mbox{cnf}(\mbox{premise}_{15},\mbox{hypothesis})$

$\mbox{heap}(\mbox{sep}(\mbox{lseg}(x_{14},x_{12}),\mbox{sep}(\mbox{lseg}(x_2,x_{13}),\mbox{sep}(\mbox{lseg}(x_{13},x_6),\mbox{sep}(\mbox{lseg}(x_{13},x_8),\mbox{sep}(\mbox{lseg}(x_{10},x_2),\mbox{sep}(\mbox{lseg}(x_{10},x_3),\mbox{sep}(\mbox{lseg}(x_7,x_2),\mbox{sep}(\mbox{lseg}(x_7,x_{16}),\mbox{sep}(\mbox{lseg}(x_3,x_{14}),\mbox{sep}(\mbox{lseg}(x_{11},x_4),\mbox{sep}(\mbox{lseg}(x_6,x_{14}),\mbox{sep}(\mbox{lseg}(x_6,x_{16}),\mbox{emp})))))))))))))\qquad\mbox{cnf}(\mbox{premise}_{16},\mbox{hypothesis})$

$\mbox{heap}(\mbox{emp}) \ \Rightarrow \ x_1 = x_1\qquad\mbox{cnf}(\mbox{conclusion}_1,\mbox{negated\_conjecture})$

\medskip\textbf{SWW445-1.p} Randomly generated entailment of the form F $\to$ $\bot$ (n = 20)

A randomly generated entailment with n program variables.
 Negated equalities and list segments are added at random, with
 specific paramenters so that about half of the generated
 entailments are valid (or, equivalently, F is unsatisfiable).
 Normalization and well-formedness axioms should be enough to
 decide these entailments.




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

$x_6\ne x_{19}\qquad\mbox{cnf}(\mbox{premise}_1,\mbox{hypothesis})$

$x_3\ne x_7\qquad\mbox{cnf}(\mbox{premise}_2,\mbox{hypothesis})$

$x_3\ne x_{20}\qquad\mbox{cnf}(\mbox{premise}_3,\mbox{hypothesis})$

$x_7\ne x_{20}\qquad\mbox{cnf}(\mbox{premise}_4,\mbox{hypothesis})$

$x_9\ne x_{19}\qquad\mbox{cnf}(\mbox{premise}_5,\mbox{hypothesis})$

$x_2\ne x_{20}\qquad\mbox{cnf}(\mbox{premise}_6,\mbox{hypothesis})$

$x_8\ne x_{19}\qquad\mbox{cnf}(\mbox{premise}_7,\mbox{hypothesis})$

$x_8\ne x_{17}\qquad\mbox{cnf}(\mbox{premise}_8,\mbox{hypothesis})$

$x_4\ne x_{11}\qquad\mbox{cnf}(\mbox{premise}_9,\mbox{hypothesis})$

$x_4\ne x_{13}\qquad\mbox{cnf}(\mbox{premise}_{10},\mbox{hypothesis})$

$x_4\ne x_{19}\qquad\mbox{cnf}(\mbox{premise}_{11},\mbox{hypothesis})$

$x_1\ne x_{16}\qquad\mbox{cnf}(\mbox{premise}_{12},\mbox{hypothesis})$

$x_1\ne x_{20}\qquad\mbox{cnf}(\mbox{premise}_{13},\mbox{hypothesis})$

$x_{13}\ne x_{18}\qquad\mbox{cnf}(\mbox{premise}_{14},\mbox{hypothesis})$

$x_{13}\ne x_{17}\qquad\mbox{cnf}(\mbox{premise}_{15},\mbox{hypothesis})$

$x_{10}\ne x_{19}\qquad\mbox{cnf}(\mbox{premise}_{16},\mbox{hypothesis})$

$x_{10}\ne x_{20}\qquad\mbox{cnf}(\mbox{premise}_{17},\mbox{hypothesis})$

$x_{16}\ne x_{19}\qquad\mbox{cnf}(\mbox{premise}_{18},\mbox{hypothesis})$

$\mbox{heap}(\mbox{sep}(\mbox{lseg}(x_5,x_{17}),\mbox{sep}(\mbox{lseg}(x_{19},x_1),\mbox{sep}(\mbox{lseg}(x_4,x_{12}),\mbox{sep}(\mbox{lseg}(x_{12},x_{20}),\mbox{sep}(\mbox{lseg}(x_{12},x_{15}),\mbox{sep}(\mbox{lseg}(x_{12},x_{11}),\mbox{sep}(\mbox{lseg}(x_2,x_{18}),\mbox{sep}(\mbox{lseg}(x_{17},x_{14}),\mbox{sep}(\mbox{lseg}(x_7,x_{16}),\mbox{sep}(\mbox{lseg}(x_3,x_{20}),\mbox{sep}(\mbox{lseg}(x_3,x_{12}),\mbox{sep}(\mbox{lseg}(x_{11},x_{12}),\mbox{sep}(\mbox{lseg}(x_6,x_{17}),\mbox{sep}(\mbox{lseg}(x_6,x_{19}),\mbox{emp})))))))))))))))\qquad\mbox{cnf}(\mbox{premise}_{19},\mbox{hypothesis})$

$\mbox{heap}(\mbox{emp}) \ \Rightarrow \ x_1 = x_1\qquad\mbox{cnf}(\mbox{conclusion}_1,\mbox{negated\_conjecture})$

\medskip\textbf{SWW413-1.p} Verification Condition generated by Smallfoot

This is one of the verification conditions that were gathered
 from the output of Smallfoot when checking assertions on list
 manipulating programs from its own benchmark suite.




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

$\mbox{nil}\ne x_1\qquad\mbox{cnf}(\mbox{premise}_1,\mbox{hypothesis})$

$\mbox{nil}\ne x_2\qquad\mbox{cnf}(\mbox{premise}_2,\mbox{hypothesis})$

$x_3\ne x_2\qquad\mbox{cnf}(\mbox{premise}_3,\mbox{hypothesis})$

$x_4\ne x_1\qquad\mbox{cnf}(\mbox{premise}_4,\mbox{hypothesis})$

$x_4\ne x_2\qquad\mbox{cnf}(\mbox{premise}_5,\mbox{hypothesis})$

$x_1\ne x_2\qquad\mbox{cnf}(\mbox{premise}_6,\mbox{hypothesis})$

$\mbox{heap}(\mbox{sep}(\mbox{lseg}(x_3,\mbox{nil}),\mbox{sep}(\mbox{next}(x_2,x_3),\mbox{emp})))\qquad\mbox{cnf}(\mbox{premise}_7,\mbox{hypothesis})$

$\neg\,\mbox{heap}(\mbox{sep}(\mbox{lseg}(x_2,\mbox{nil}),\mbox{emp}))\qquad\mbox{cnf}(\mbox{conclusion}_1,\mbox{negated\_conjecture})$

\medskip\textbf{SWW458-1.p} Randomly generated entailment of the form F $\to$ G (n = 15)

A randomly generated entailment with n program variables.
 A random graph with pointers and list segments is generated,
 and then some of the segments are folded. The task is to
 prove whether the unfolded version entails the folded one.
 Parameters are chosen so that about half of the generated
 entailments are valid.
 These entailments stress the role of unfolding axioms.




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

$\mbox{heap}(\mbox{sep}(\mbox{lseg}(x_{11},x_{14}),\mbox{sep}(\mbox{next}(x_4,x_9),\mbox{sep}(\mbox{next}(x_2,x_5),\mbox{sep}(\mbox{next}(x_3,x_{12}),\mbox{sep}(\mbox{lseg}(x_{14},x_{11}),\mbox{sep}(\mbox{lseg}(x_{10},x_{13}),\mbox{sep}(\mbox{next}(x_6,x_2),\mbox{sep}(\mbox{next}(x_{15},x_6),\mbox{sep}(\mbox{next}(x_7,x_5),\mbox{sep}(\mbox{next}(x_1,x_{13}),\mbox{sep}(\mbox{next}(x_5,x_1),\mbox{sep}(\mbox{next}(x_{13},x_{12}),\mbox{sep}(\mbox{next}(x_8,x_{12}),\mbox{sep}(\mbox{lseg}(x_{12},x_5),\mbox{sep}(\mbox{lseg}(x_9,x_8),\mbox{emp}))))))))))))))))\qquad\mbox{cnf}(\mbox{premise}_1,\mbox{hypothesis})$

$\neg\,\mbox{heap}(\mbox{sep}(\mbox{lseg}(x_{15},x_6),\mbox{sep}(\mbox{lseg}(x_{10},x_{13}),\mbox{sep}(\mbox{lseg}(x_6,x_2),\mbox{sep}(\mbox{lseg}(x_3,x_{12}),\mbox{sep}(\mbox{lseg}(x_4,x_9),\mbox{sep}(\mbox{lseg}(x_2,x_5),\mbox{sep}(\mbox{lseg}(x_9,x_8),\mbox{sep}(\mbox{lseg}(x_{13},x_{12}),\mbox{sep}(\mbox{lseg}(x_7,x_5),\mbox{sep}(\mbox{lseg}(x_8,x_{13}),\mbox{sep}(\mbox{lseg}(x_{14},x_{11}),\mbox{sep}(\mbox{lseg}(x_{11},x_{14}),\mbox{emp})))))))))))))\qquad\mbox{cnf}(\mbox{conclusion}_1,\mbox{negated\_conjecture})$

\medskip\textbf{SWW419-1.p} Verification Condition generated by Smallfoot

This is one of the verification conditions that were gathered
 from the output of Smallfoot when checking assertions on list
 manipulating programs from its own benchmark suite.




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

$\mbox{nil}\ne x_1\qquad\mbox{cnf}(\mbox{premise}_1,\mbox{hypothesis})$

$x_2\ne x_1\qquad\mbox{cnf}(\mbox{premise}_2,\mbox{hypothesis})$

$x_1\ne x_3\qquad\mbox{cnf}(\mbox{premise}_3,\mbox{hypothesis})$

$\mbox{heap}(\mbox{sep}(\mbox{next}(x_1,x_3),\mbox{sep}(\mbox{lseg}(x_2,\mbox{nil}),\mbox{emp})))\qquad\mbox{cnf}(\mbox{premise}_4,\mbox{hypothesis})$

$x_2 = x_2 \ \Rightarrow \ \neg\,\mbox{heap}(\mbox{emp})\qquad\mbox{cnf}(\mbox{conclusion}_1,\mbox{negated\_conjecture})$

\medskip\textbf{SWW469\_1.p} Hoare's Logic with Procedures line 112, 100 axioms selected






$\mbox{state}{:}\;\mbox{\$tType}\qquad\mbox{tff}(\mbox{ty\_ty\_tc\_\_Com\_\_Ostate},\mbox{type})$

$\mbox{induct\_false}{:}\;\mbox{\$o}\qquad\mbox{tff}(\mbox{sy\_c\_HOL\_Oinduct\_\_false},\mbox{type})$

$\mbox{induct\_true}{:}\;\mbox{\$o}\qquad\mbox{tff}(\mbox{sy\_c\_HOL\_Oinduct\_\_true},\mbox{type})$

$\mbox{hoare\_1310879719gleton}{:}\;\mbox{\$o}\qquad\mbox{tff}(\mbox{sy\_c\_Hoare\_\_Mirabelle\_\_yiemogtkbg\_Ostate\_\_not\_\_singleton},\mbox{type})$

$\mbox{hoare\_1310879719gleton}\iff \exists s{:}\;\mbox{state},t{:}\;\mbox{state}{:}\;s\ne t\qquad\mbox{tff}(\mbox{fact\_0\_state\_\_not\_\_singleton\_\_def},\mbox{axiom})$

$\neg\,\mbox{induct\_false}\qquad\mbox{tff}(\mbox{fact\_1\_induct\_\_false\_\_def},\mbox{axiom})$

$\mbox{induct\_true}\qquad\mbox{tff}(\mbox{fact\_2\_induct\_\_trueI},\mbox{axiom})$

$\mbox{induct\_true}\qquad\mbox{tff}(\mbox{fact\_3\_induct\_\_true\_\_def},\mbox{axiom})$

$\mbox{hoare\_1310879719gleton}\qquad\mbox{tff}(\mbox{conj}_0,\mbox{hypothesis})$

$\forall t{:}\;\mbox{state}{:}\;\neg\,\forall s{:}\;\mbox{state}{:}\;s = t\qquad\mbox{tff}(\mbox{conj}_1,\mbox{conjecture})$

\medskip\textbf{SWW427-1.p} Randomly generated entailment of the form F $\to$ $\bot$ (n = 11)

A randomly generated entailment with n program variables.
 Negated equalities and list segments are added at random, with
 specific paramenters so that about half of the generated
 entailments are valid (or, equivalently, F is unsatisfiable).
 Normalization and well-formedness axioms should be enough to
 decide these entailments.




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

$x_8\ne x_9\qquad\mbox{cnf}(\mbox{premise}_1,\mbox{hypothesis})$

$x_1\ne x_{11}\qquad\mbox{cnf}(\mbox{premise}_2,\mbox{hypothesis})$

$x_4\ne x_{11}\qquad\mbox{cnf}(\mbox{premise}_3,\mbox{hypothesis})$

$x_4\ne x_7\qquad\mbox{cnf}(\mbox{premise}_4,\mbox{hypothesis})$

$x_3\ne x_8\qquad\mbox{cnf}(\mbox{premise}_5,\mbox{hypothesis})$

$x_3\ne x_4\qquad\mbox{cnf}(\mbox{premise}_6,\mbox{hypothesis})$

$x_7\ne x_8\qquad\mbox{cnf}(\mbox{premise}_7,\mbox{hypothesis})$

$x_7\ne x_9\qquad\mbox{cnf}(\mbox{premise}_8,\mbox{hypothesis})$

$x_2\ne x_{11}\qquad\mbox{cnf}(\mbox{premise}_9,\mbox{hypothesis})$

$\mbox{heap}(\mbox{sep}(\mbox{lseg}(x_{10},x_1),\mbox{sep}(\mbox{lseg}(x_9,x_2),\mbox{sep}(\mbox{lseg}(x_9,x_7),\mbox{sep}(\mbox{lseg}(x_7,x_{10}),\mbox{sep}(\mbox{lseg}(x_{11},x_9),\mbox{sep}(\mbox{lseg}(x_{11},x_7),\mbox{sep}(\mbox{lseg}(x_{11},x_3),\mbox{sep}(\mbox{lseg}(x_{11},x_6),\mbox{sep}(\mbox{lseg}(x_4,x_5),\mbox{emp}))))))))))\qquad\mbox{cnf}(\mbox{premise}_{10},\mbox{hypothesis})$

$\mbox{heap}(\mbox{emp}) \ \Rightarrow \ x_1 = x_1\qquad\mbox{cnf}(\mbox{conclusion}_1,\mbox{negated\_conjecture})$

\medskip\textbf{SWW460-1.p} Randomly generated entailment of the form F $\to$ G (n = 16)

A randomly generated entailment with n program variables.
 A random graph with pointers and list segments is generated,
 and then some of the segments are folded. The task is to
 prove whether the unfolded version entails the folded one.
 Parameters are chosen so that about half of the generated
 entailments are valid.
 These entailments stress the role of unfolding axioms.




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

$\mbox{heap}(\mbox{sep}(\mbox{next}(x_3,x_4),\mbox{sep}(\mbox{next}(x_8,x_{14}),\mbox{sep}(\mbox{next}(x_2,x_{11}),\mbox{sep}(\mbox{lseg}(x_5,x_{15}),\mbox{sep}(\mbox{next}(x_{14},x_1),\mbox{sep}(\mbox{next}(x_{12},x_{11}),\mbox{sep}(\mbox{next}(x_{13},x_1),\mbox{sep}(\mbox{next}(x_9,x_{11}),\mbox{sep}(\mbox{next}(x_{16},x_{14}),\mbox{sep}(\mbox{next}(x_1,x_2),\mbox{sep}(\mbox{lseg}(x_4,x_{15}),\mbox{sep}(\mbox{next}(x_7,x_{11}),\mbox{sep}(\mbox{next}(x_{10},x_6),\mbox{sep}(\mbox{lseg}(x_6,x_5),\mbox{sep}(\mbox{next}(x_{11},x_1),\mbox{sep}(\mbox{next}(x_{15},x_6),\mbox{emp})))))))))))))))))\qquad\mbox{cnf}(\mbox{premise}_1,\mbox{hypothesis})$

$\neg\,\mbox{heap}(\mbox{sep}(\mbox{lseg}(x_{13},x_1),\mbox{sep}(\mbox{lseg}(x_{12},x_{11}),\mbox{sep}(\mbox{lseg}(x_8,x_{14}),\mbox{sep}(\mbox{lseg}(x_{16},x_{14}),\mbox{sep}(\mbox{lseg}(x_3,x_{15}),\mbox{sep}(\mbox{lseg}(x_2,x_{11}),\mbox{sep}(\mbox{lseg}(x_9,x_{11}),\mbox{sep}(\mbox{lseg}(x_{14},x_1),\mbox{sep}(\mbox{lseg}(x_{15},x_6),\mbox{sep}(\mbox{lseg}(x_{10},x_{15}),\mbox{sep}(\mbox{lseg}(x_7,x_2),\mbox{emp}))))))))))))\qquad\mbox{cnf}(\mbox{conclusion}_1,\mbox{negated\_conjecture})$

\medskip\textbf{SWW096+1.p} Equivalenace of the semantic and syntactic definition of and 






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

$\forall p,q{:}\;\mbox{and}_1(p,q) = \mbox{and}_2(p,q)\qquad\mbox{fof}(\mbox{and1\_and}_2,\mbox{conjecture})$

\medskip\textbf{SWW414-1.p} Verification Condition generated by Smallfoot

This is one of the verification conditions that were gathered
 from the output of Smallfoot when checking assertions on list
 manipulating programs from its own benchmark suite.




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

$\mbox{nil}\ne x_1\qquad\mbox{cnf}(\mbox{premise}_1,\mbox{hypothesis})$

$x_1\ne x_2\qquad\mbox{cnf}(\mbox{premise}_2,\mbox{hypothesis})$

$\mbox{heap}(\mbox{sep}(\mbox{lseg}(x_2,\mbox{nil}),\mbox{sep}(\mbox{lseg}(x_1,\mbox{nil}),\mbox{emp})))\qquad\mbox{cnf}(\mbox{premise}_3,\mbox{hypothesis})$

$\neg\,\mbox{heap}(\mbox{sep}(\mbox{lseg}(x_2,\mbox{nil}),\mbox{emp}))\qquad\mbox{cnf}(\mbox{conclusion}_1,\mbox{negated\_conjecture})$

\medskip\textbf{SWW464-1.p} Randomly generated entailment of the form F $\to$ G (n = 18)

A randomly generated entailment with n program variables.
 A random graph with pointers and list segments is generated,
 and then some of the segments are folded. The task is to
 prove whether the unfolded version entails the folded one.
 Parameters are chosen so that about half of the generated
 entailments are valid.
 These entailments stress the role of unfolding axioms.




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

$\mbox{heap}(\mbox{sep}(\mbox{lseg}(x_8,x_6),\mbox{sep}(\mbox{next}(x_6,x_{11}),\mbox{sep}(\mbox{lseg}(x_{15},x_1),\mbox{sep}(\mbox{next}(x_5,x_6),\mbox{sep}(\mbox{next}(x_2,x_7),\mbox{sep}(\mbox{lseg}(x_{11},x_4),\mbox{sep}(\mbox{lseg}(x_9,x_5),\mbox{sep}(\mbox{next}(x_{13},x_{14}),\mbox{sep}(\mbox{lseg}(x_{16},x_{18}),\mbox{sep}(\mbox{next}(x_7,x_{14}),\mbox{sep}(\mbox{next}(x_3,x_{18}),\mbox{sep}(\mbox{next}(x_4,x_{13}),\mbox{sep}(\mbox{lseg}(x_{18},x_{15}),\mbox{sep}(\mbox{next}(x_{12},x_{16}),\mbox{sep}(\mbox{next}(x_{10},x_4),\mbox{sep}(\mbox{next}(x_{14},x_{10}),\mbox{sep}(\mbox{next}(x_{17},x_4),\mbox{sep}(\mbox{next}(x_1,x_{16}),\mbox{emp})))))))))))))))))))\qquad\mbox{cnf}(\mbox{premise}_1,\mbox{hypothesis})$

$\neg\,\mbox{heap}(\mbox{sep}(\mbox{lseg}(x_8,x_6),\mbox{sep}(\mbox{lseg}(x_{10},x_4),\mbox{sep}(\mbox{lseg}(x_9,x_4),\mbox{sep}(\mbox{lseg}(x_{15},x_1),\mbox{sep}(\mbox{lseg}(x_3,x_{18}),\mbox{sep}(\mbox{lseg}(x_2,x_{14}),\mbox{sep}(\mbox{lseg}(x_{12},x_{16}),\mbox{sep}(\mbox{lseg}(x_{17},x_{10}),\mbox{sep}(\mbox{lseg}(x_1,x_{15}),\mbox{emp}))))))))))\qquad\mbox{cnf}(\mbox{conclusion}_1,\mbox{negated\_conjecture})$

\medskip\textbf{SWW410-1.p} Verification Condition generated by Smallfoot

This is one of the verification conditions that were gathered
 from the output of Smallfoot when checking assertions on list
 manipulating programs from its own benchmark suite.




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

$\mbox{nil}\ne x_1\qquad\mbox{cnf}(\mbox{premise}_1,\mbox{hypothesis})$

$\mbox{nil}\ne x_2\qquad\mbox{cnf}(\mbox{premise}_2,\mbox{hypothesis})$

$x_1\ne x_3\qquad\mbox{cnf}(\mbox{premise}_3,\mbox{hypothesis})$

$x_3\ne x_2\qquad\mbox{cnf}(\mbox{premise}_4,\mbox{hypothesis})$

$\mbox{heap}(\mbox{sep}(\mbox{lseg}(x_2,x_1),\mbox{sep}(\mbox{lseg}(x_3,\mbox{nil}),\mbox{sep}(\mbox{next}(x_1,x_3),\mbox{emp}))))\qquad\mbox{cnf}(\mbox{premise}_5,\mbox{hypothesis})$

$\neg\,\mbox{heap}(\mbox{sep}(\mbox{lseg}(x_3,\mbox{nil}),\mbox{sep}(\mbox{lseg}(x_2,x_3),\mbox{emp})))\qquad\mbox{cnf}(\mbox{conclusion}_1,\mbox{negated\_conjecture})$

\medskip\textbf{SWW675-1.p} Lists in Separation Logic






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

\medskip\textbf{SWW409-1.p} Verification Condition generated by Smallfoot

This is one of the verification conditions that were gathered
 from the output of Smallfoot when checking assertions on list
 manipulating programs from its own benchmark suite.




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

$\mbox{nil}\ne x_1\qquad\mbox{cnf}(\mbox{premise}_1,\mbox{hypothesis})$

$\mbox{nil}\ne x_2\qquad\mbox{cnf}(\mbox{premise}_2,\mbox{hypothesis})$

$x_1\ne x_3\qquad\mbox{cnf}(\mbox{premise}_3,\mbox{hypothesis})$

$x_2\ne x_3\qquad\mbox{cnf}(\mbox{premise}_4,\mbox{hypothesis})$

$\mbox{heap}(\mbox{sep}(\mbox{lseg}(x_2,x_1),\mbox{sep}(\mbox{lseg}(x_3,\mbox{nil}),\mbox{sep}(\mbox{next}(x_1,x_3),\mbox{emp}))))\qquad\mbox{cnf}(\mbox{premise}_5,\mbox{hypothesis})$

$\neg\,\mbox{heap}(\mbox{sep}(\mbox{lseg}(x_2,\mbox{nil}),\mbox{emp}))\qquad\mbox{cnf}(\mbox{conclusion}_1,\mbox{negated\_conjecture})$

\medskip\textbf{SWW098+1.p} Equivalence of or1 and or2






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

$\forall p,q{:}\;\mbox{or}_1(p,q) = \mbox{or}_2(p,q)\qquad\mbox{fof}(\mbox{or1\_or}_2,\mbox{conjecture})$

\medskip\textbf{SWW465-1.p} Randomly generated entailment of the form F $\to$ G (n = 19)

A randomly generated entailment with n program variables.
 A random graph with pointers and list segments is generated,
 and then some of the segments are folded. The task is to
 prove whether the unfolded version entails the folded one.
 Parameters are chosen so that about half of the generated
 entailments are valid.
 These entailments stress the role of unfolding axioms.




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

$\mbox{heap}(\mbox{sep}(\mbox{lseg}(x_6,x_{15}),\mbox{sep}(\mbox{lseg}(x_4,x_2),\mbox{sep}(\mbox{next}(x_{19},x_{13}),\mbox{sep}(\mbox{next}(x_8,x_9),\mbox{sep}(\mbox{next}(x_5,x_2),\mbox{sep}(\mbox{next}(x_{15},x_{13}),\mbox{sep}(\mbox{next}(x_3,x_4),\mbox{sep}(\mbox{next}(x_{11},x_{15}),\mbox{sep}(\mbox{next}(x_{16},x_5),\mbox{sep}(\mbox{next}(x_{18},x_4),\mbox{sep}(\mbox{next}(x_9,x_1),\mbox{sep}(\mbox{next}(x_2,x_8),\mbox{sep}(\mbox{next}(x_{17},x_2),\mbox{sep}(\mbox{lseg}(x_1,x_3),\mbox{sep}(\mbox{lseg}(x_{14},x_7),\mbox{sep}(\mbox{next}(x_{10},x_1),\mbox{sep}(\mbox{next}(x_7,x_{18}),\mbox{sep}(\mbox{next}(x_{12},x_{13}),\mbox{sep}(\mbox{lseg}(x_{13},x_9),\mbox{emp}))))))))))))))))))))\qquad\mbox{cnf}(\mbox{premise}_1,\mbox{hypothesis})$

$\neg\,\mbox{heap}(\mbox{sep}(\mbox{lseg}(x_{10},x_1),\mbox{sep}(\mbox{lseg}(x_{11},x_{15}),\mbox{sep}(\mbox{lseg}(x_{14},x_{18}),\mbox{sep}(\mbox{lseg}(x_{18},x_4),\mbox{sep}(\mbox{lseg}(x_4,x_2),\mbox{sep}(\mbox{lseg}(x_6,x_{13}),\mbox{sep}(\mbox{lseg}(x_{19},x_{13}),\mbox{sep}(\mbox{lseg}(x_{17},x_2),\mbox{sep}(\mbox{lseg}(x_{12},x_9),\mbox{sep}(\mbox{lseg}(x_{16},x_4),\mbox{emp})))))))))))\qquad\mbox{cnf}(\mbox{conclusion}_1,\mbox{negated\_conjecture})$

\medskip\textbf{SWW469+1.p} Hoare's Logic with Procedures line 112, 100 axioms selected






$\mbox{is\_state}(\mbox{undefined\_state}(\mbox{state}))\qquad\mbox{fof}(\mbox{gsy\_c\_HOL\_Oundefined\_000tc\_\_Com\_\_Ostate},\mbox{axiom})$

$\mbox{hoare\_165779456gleton}\iff \exists s,t{:}\;( \mbox{is\_state}(s)\mbox{ and }\mbox{is\_state}(t)\mbox{ and }s\ne t )\qquad\mbox{fof}(\mbox{fact\_0\_state\_\_not\_\_singleton\_\_def},\mbox{axiom})$

$\neg\,\mbox{induct\_false}\qquad\mbox{fof}(\mbox{fact\_1\_induct\_\_false\_\_def},\mbox{axiom})$

$\mbox{induct\_true}\qquad\mbox{fof}(\mbox{fact\_2\_induct\_\_trueI},\mbox{axiom})$

$\mbox{induct\_true}\qquad\mbox{fof}(\mbox{fact\_3\_induct\_\_true\_\_def},\mbox{axiom})$

$\mbox{hoare\_165779456gleton}\qquad\mbox{fof}(\mbox{conj}_0,\mbox{hypothesis})$

$\forall t{:}\;( \mbox{is\_state}(t) \ \Rightarrow \ \neg\,\forall s{:}\;( \mbox{is\_state}(s) \ \Rightarrow \ s = t ) )\qquad\mbox{fof}(\mbox{conj}_1,\mbox{conjecture})$

\medskip\textbf{SWW417-1.p} Verification Condition generated by Smallfoot

This is one of the verification conditions that were gathered
 from the output of Smallfoot when checking assertions on list
 manipulating programs from its own benchmark suite.




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

$\mbox{nil}\ne x_1\qquad\mbox{cnf}(\mbox{premise}_1,\mbox{hypothesis})$

$x_2\ne x_1\qquad\mbox{cnf}(\mbox{premise}_2,\mbox{hypothesis})$

$\mbox{heap}(\mbox{sep}(\mbox{lseg}(x_2,\mbox{nil}),\mbox{sep}(\mbox{next}(x_1,x_2),\mbox{emp})))\qquad\mbox{cnf}(\mbox{premise}_3,\mbox{hypothesis})$

$\neg\,\mbox{heap}(\mbox{sep}(\mbox{lseg}(x_1,\mbox{nil}),\mbox{emp}))\qquad\mbox{cnf}(\mbox{conclusion}_1,\mbox{negated\_conjecture})$

\medskip\textbf{SWW435-1.p} Randomly generated entailment of the form F $\to$ $\bot$ (n = 15)

A randomly generated entailment with n program variables.
 Negated equalities and list segments are added at random, with
 specific paramenters so that about half of the generated
 entailments are valid (or, equivalently, F is unsatisfiable).
 Normalization and well-formedness axioms should be enough to
 decide these entailments.




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

$x_6\ne x_{11}\qquad\mbox{cnf}(\mbox{premise}_1,\mbox{hypothesis})$

$x_{11}\ne x_{14}\qquad\mbox{cnf}(\mbox{premise}_2,\mbox{hypothesis})$

$x_3\ne x_8\qquad\mbox{cnf}(\mbox{premise}_3,\mbox{hypothesis})$

$x_3\ne x_7\qquad\mbox{cnf}(\mbox{premise}_4,\mbox{hypothesis})$

$x_2\ne x_8\qquad\mbox{cnf}(\mbox{premise}_5,\mbox{hypothesis})$

$x_1\ne x_{11}\qquad\mbox{cnf}(\mbox{premise}_6,\mbox{hypothesis})$

$x_4\ne x_{13}\qquad\mbox{cnf}(\mbox{premise}_7,\mbox{hypothesis})$

$x_{10}\ne x_{11}\qquad\mbox{cnf}(\mbox{premise}_8,\mbox{hypothesis})$

$x_5\ne x_{12}\qquad\mbox{cnf}(\mbox{premise}_9,\mbox{hypothesis})$

$x_5\ne x_{15}\qquad\mbox{cnf}(\mbox{premise}_{10},\mbox{hypothesis})$

$\mbox{heap}(\mbox{sep}(\mbox{lseg}(x_5,x_7),\mbox{sep}(\mbox{lseg}(x_2,x_5),\mbox{sep}(\mbox{lseg}(x_{12},x_3),\mbox{sep}(\mbox{lseg}(x_9,x_{11}),\mbox{sep}(\mbox{lseg}(x_{13},x_{15}),\mbox{sep}(\mbox{lseg}(x_7,x_9),\mbox{sep}(\mbox{lseg}(x_7,x_1),\mbox{sep}(\mbox{lseg}(x_7,x_{11}),\mbox{sep}(\mbox{lseg}(x_3,x_{12}),\mbox{sep}(\mbox{lseg}(x_4,x_{12}),\mbox{sep}(\mbox{lseg}(x_6,x_{12}),\mbox{sep}(\mbox{lseg}(x_6,x_4),\mbox{emp})))))))))))))\qquad\mbox{cnf}(\mbox{premise}_{11},\mbox{hypothesis})$

$\mbox{heap}(\mbox{emp}) \ \Rightarrow \ x_1 = x_1\qquad\mbox{cnf}(\mbox{conclusion}_1,\mbox{negated\_conjecture})$

\medskip\textbf{SWW411-1.p} Verification Condition generated by Smallfoot

This is one of the verification conditions that were gathered
 from the output of Smallfoot when checking assertions on list
 manipulating programs from its own benchmark suite.




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

$\mbox{nil}\ne x_1\qquad\mbox{cnf}(\mbox{premise}_1,\mbox{hypothesis})$

$\mbox{nil}\ne x_2\qquad\mbox{cnf}(\mbox{premise}_2,\mbox{hypothesis})$

$x_3\ne x_1\qquad\mbox{cnf}(\mbox{premise}_3,\mbox{hypothesis})$

$x_3\ne x_2\qquad\mbox{cnf}(\mbox{premise}_4,\mbox{hypothesis})$

$x_1\ne x_2\qquad\mbox{cnf}(\mbox{premise}_5,\mbox{hypothesis})$

$\mbox{heap}(\mbox{sep}(\mbox{lseg}(x_1,\mbox{nil}),\mbox{sep}(\mbox{lseg}(x_3,\mbox{nil}),\mbox{sep}(\mbox{next}(x_2,x_3),\mbox{emp}))))\qquad\mbox{cnf}(\mbox{premise}_6,\mbox{hypothesis})$

$\neg\,\mbox{heap}(\mbox{sep}(\mbox{lseg}(x_1,\mbox{nil}),\mbox{sep}(\mbox{lseg}(x_3,\mbox{nil}),\mbox{emp})))\qquad\mbox{cnf}(\mbox{conclusion}_1,\mbox{negated\_conjecture})$

\medskip\textbf{SWW588=2.p} Division-T-WP parameter division






$\mbox{uni}{:}\;\mbox{\$tType}\qquad\mbox{tff}(\mbox{uni},\mbox{type})$

$\mbox{ty}{:}\;\mbox{\$tType}\qquad\mbox{tff}(\mbox{ty},\mbox{type})$

$\mbox{sort}_1{:}\;( \mbox{ty}\times \mbox{uni} )\to \mbox{\$o}\qquad\mbox{tff}(\mbox{sort},\mbox{type})$

$\mbox{witness}_1{:}\;\mbox{ty}\to \mbox{uni}\qquad\mbox{tff}(\mbox{witness},\mbox{type})$

$\forall a{:}\;\mbox{ty}{:}\;\mbox{sort}_1(a,\mbox{witness}_1(a))\qquad\mbox{tff}(\mbox{witness\_sort}_1,\mbox{axiom})$

$\mbox{int}{:}\;\mbox{ty}\qquad\mbox{tff}(\mbox{int},\mbox{type})$

$\mbox{real}{:}\;\mbox{ty}\qquad\mbox{tff}(\mbox{real},\mbox{type})$

$\mbox{bool}_1{:}\;\mbox{\$tType}\qquad\mbox{tff}(\mbox{bool},\mbox{type})$

$\mbox{bool}{:}\;\mbox{ty}\qquad\mbox{tff}(\mbox{bool}_1,\mbox{type})$

$\mbox{true}_1{:}\;\mbox{bool}_1\qquad\mbox{tff}(\mbox{true},\mbox{type})$

$\mbox{false}_1{:}\;\mbox{bool}_1\qquad\mbox{tff}(\mbox{false},\mbox{type})$

$\mbox{match\_bool}_1{:}\;( \mbox{ty}\times \mbox{bool}_1\times \mbox{uni}\times \mbox{uni} )\to \mbox{uni}\qquad\mbox{tff}(\mbox{match\_bool},\mbox{type})$

$\forall a{:}\;\mbox{ty},x{:}\;\mbox{bool}_1,x_1{:}\;\mbox{uni},x_2{:}\;\mbox{uni}{:}\;\mbox{sort}_1(a,\mbox{match\_bool}_1(a,x,x_1,x_2))\qquad\mbox{tff}(\mbox{match\_bool\_sort}_1,\mbox{axiom})$

$\forall a{:}\;\mbox{ty},z{:}\;\mbox{uni},z_1{:}\;\mbox{uni}{:}\;( \mbox{sort}_1(a,z) \ \Rightarrow \ \mbox{match\_bool}_1(a,\mbox{true}_1,z,z_1) = z )\qquad\mbox{tff}(\mbox{match\_bool\_True},\mbox{axiom})$

$\forall a{:}\;\mbox{ty},z{:}\;\mbox{uni},z_1{:}\;\mbox{uni}{:}\;( \mbox{sort}_1(a,z_1) \ \Rightarrow \ \mbox{match\_bool}_1(a,\mbox{false}_1,z,z_1) = z_1 )\qquad\mbox{tff}(\mbox{match\_bool\_False},\mbox{axiom})$

$\mbox{true}_1\ne \mbox{false}_1\qquad\mbox{tff}(\mbox{true\_False},\mbox{axiom})$

$\forall u{:}\;\mbox{bool}_1{:}\;( u = \mbox{true}_1\mbox{ or }u = \mbox{false}_1 )\qquad\mbox{tff}(\mbox{bool\_inversion},\mbox{axiom})$

$\mbox{tuple}_{02}{:}\;\mbox{\$tType}\qquad\mbox{tff}(\mbox{tuple}_0,\mbox{type})$

$\mbox{tuple}_0{:}\;\mbox{ty}\qquad\mbox{tff}(\mbox{tuple}_{01},\mbox{type})$

$\mbox{tuple}_{03}{:}\;\mbox{tuple}_{02}\qquad\mbox{tff}(\mbox{tuple}_{02},\mbox{type})$

$\forall u{:}\;\mbox{tuple}_{02}{:}\;u = \mbox{tuple}_{03}\qquad\mbox{tff}(\mbox{tuple0\_inversion},\mbox{axiom})$

$\mbox{qtmark}{:}\;\mbox{ty}\qquad\mbox{tff}(\mbox{qtmark},\mbox{type})$

$\forall x{:}\;\mbox{\$int},y{:}\;\mbox{\$int},z{:}\;\mbox{\$int}{:}\;( \mbox{\$lesseq}(x,y) \ \Rightarrow \ ( \mbox{\$lesseq}(0,z) \ \Rightarrow \ \mbox{\$lesseq}(\mbox{\$product}(x,z),\mbox{\$product}(y,z)) ) )\qquad\mbox{tff}(\mbox{compatOrderMult},\mbox{axiom})$

$\mbox{ref}{:}\;\mbox{ty}\to \mbox{ty}\qquad\mbox{tff}(\mbox{ref},\mbox{type})$

$\mbox{mk\_ref}{:}\;( \mbox{ty}\times \mbox{uni} )\to \mbox{uni}\qquad\mbox{tff}(\mbox{mk\_ref},\mbox{type})$

$\forall a{:}\;\mbox{ty},x{:}\;\mbox{uni}{:}\;\mbox{sort}_1(\mbox{ref}(a),\mbox{mk\_ref}(a,x))\qquad\mbox{tff}(\mbox{mk\_ref\_sort}_1,\mbox{axiom})$

$\mbox{contents}{:}\;( \mbox{ty}\times \mbox{uni} )\to \mbox{uni}\qquad\mbox{tff}(\mbox{contents},\mbox{type})$

$\forall a{:}\;\mbox{ty},x{:}\;\mbox{uni}{:}\;\mbox{sort}_1(a,\mbox{contents}(a,x))\qquad\mbox{tff}(\mbox{contents\_sort}_1,\mbox{axiom})$

$\forall a{:}\;\mbox{ty},u{:}\;\mbox{uni}{:}\;( \mbox{sort}_1(a,u) \ \Rightarrow \ \mbox{contents}(a,\mbox{mk\_ref}(a,u)) = u )\qquad\mbox{tff}(\mbox{contents\_def}_1,\mbox{axiom})$

$\forall a{:}\;\mbox{ty},u{:}\;\mbox{uni}{:}\;( \mbox{sort}_1(\mbox{ref}(a),u) \ \Rightarrow \ u = \mbox{mk\_ref}(a,\mbox{contents}(a,u)) )\qquad\mbox{tff}(\mbox{ref\_inversion}_1,\mbox{axiom})$

$\forall a{:}\;\mbox{\$int},b{:}\;\mbox{\$int}{:}\;( ( \mbox{\$lesseq}(0,a)\mbox{ and }\mbox{\$less}(0,b) ) \ \Rightarrow \ ( \mbox{\$sum}(\mbox{\$product}(0,b),a) = a\mbox{ and }\mbox{\$lesseq}(0,a)\mbox{ and }\forall r{:}\;\mbox{\$int},q{:}\;\mbox{\$int}{:}\;( ( \mbox{\$sum}(\mbox{\$product}(q,b),r) = a\mbox{ and }\mbox{\$lesseq}(0,r) ) \ \Rightarrow \ ( ( \mbox{\$lesseq}(b,r) \ \Rightarrow \ \forall q_1{:}\;\mbox{\$int}{:}\;( q_1 = \mbox{\$sum}(q,1) \ \Rightarrow \ \forall r_1{:}\;\mbox{\$int}{:}\;( r_1 = \mbox{\$difference}(r,b) \ \Rightarrow \ ( \mbox{\$sum}(\mbox{\$product}(q_1,b),r_1) = a\mbox{ and }\mbox{\$lesseq}(0,r_1)\mbox{ and }\mbox{\$lesseq}(0,r)\mbox{ and }\mbox{\$less}(r_1,r) ) ) ) )\mbox{ and }( \neg\,\mbox{\$lesseq}(b,r) \ \Rightarrow \ \exists r_1{:}\;\mbox{\$int}{:}\;( \mbox{\$sum}(\mbox{\$product}(q,b),r_1) = a\mbox{ and }\mbox{\$lesseq}(0,r_1)\mbox{ and }\mbox{\$less}(r_1,b) ) ) ) ) ) )\qquad\mbox{tff}(\mbox{wP\_parameter\_division},\mbox{conjecture})$

\medskip\textbf{SWW673+1.p} Priority queue checker






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

$\mbox{include}(\mbox{'Axioms/SWV007+1.ax'})$

$\mbox{include}(\mbox{'Axioms/SWV007+2.ax'})$

$\mbox{include}(\mbox{'Axioms/SWV007+3.ax'})$

$\mbox{include}(\mbox{'Axioms/SWV007+4.ax'})$

\medskip\textbf{SWW454-1.p} Randomly generated entailment of the form F $\to$ G (n = 13)

A randomly generated entailment with n program variables.
 A random graph with pointers and list segments is generated,
 and then some of the segments are folded. The task is to
 prove whether the unfolded version entails the folded one.
 Parameters are chosen so that about half of the generated
 entailments are valid.
 These entailments stress the role of unfolding axioms.




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

$\mbox{heap}(\mbox{sep}(\mbox{next}(x_1,x_3),\mbox{sep}(\mbox{next}(x_{13},x_7),\mbox{sep}(\mbox{next}(x_8,x_9),\mbox{sep}(\mbox{next}(x_{12},x_5),\mbox{sep}(\mbox{lseg}(x_7,x_5),\mbox{sep}(\mbox{next}(x_{10},x_{13}),\mbox{sep}(\mbox{lseg}(x_9,x_2),\mbox{sep}(\mbox{next}(x_2,x_5),\mbox{sep}(\mbox{next}(x_6,x_{13}),\mbox{sep}(\mbox{next}(x_3,x_9),\mbox{sep}(\mbox{next}(x_{11},x_3),\mbox{sep}(\mbox{next}(x_4,x_{13}),\mbox{sep}(\mbox{lseg}(x_5,x_{13}),\mbox{emp}))))))))))))))\qquad\mbox{cnf}(\mbox{premise}_1,\mbox{hypothesis})$

$\neg\,\mbox{heap}(\mbox{sep}(\mbox{lseg}(x_{11},x_3),\mbox{sep}(\mbox{lseg}(x_4,x_{13}),\mbox{sep}(\mbox{lseg}(x_{12},x_5),\mbox{sep}(\mbox{lseg}(x_1,x_9),\mbox{sep}(\mbox{lseg}(x_6,x_{13}),\mbox{sep}(\mbox{lseg}(x_{10},x_7),\mbox{sep}(\mbox{lseg}(x_8,x_5),\mbox{sep}(\mbox{lseg}(x_7,x_{13}),\mbox{emp})))))))))\qquad\mbox{cnf}(\mbox{conclusion}_1,\mbox{negated\_conjecture})$

\medskip\textbf{SWW426-1.p} Randomly generated entailment of the form F $\to$ $\bot$ (n = 10)

A randomly generated entailment with n program variables.
 Negated equalities and list segments are added at random, with
 specific paramenters so that about half of the generated
 entailments are valid (or, equivalently, F is unsatisfiable).
 Normalization and well-formedness axioms should be enough to
 decide these entailments.




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

$x_6\ne x_{10}\qquad\mbox{cnf}(\mbox{premise}_1,\mbox{hypothesis})$

$x_6\ne x_9\qquad\mbox{cnf}(\mbox{premise}_2,\mbox{hypothesis})$

$x_8\ne x_9\qquad\mbox{cnf}(\mbox{premise}_3,\mbox{hypothesis})$

$x_4\ne x_{10}\qquad\mbox{cnf}(\mbox{premise}_4,\mbox{hypothesis})$

$x_1\ne x_6\qquad\mbox{cnf}(\mbox{premise}_5,\mbox{hypothesis})$

$x_1\ne x_2\qquad\mbox{cnf}(\mbox{premise}_6,\mbox{hypothesis})$

$x_3\ne x_7\qquad\mbox{cnf}(\mbox{premise}_7,\mbox{hypothesis})$

$x_3\ne x_{10}\qquad\mbox{cnf}(\mbox{premise}_8,\mbox{hypothesis})$

$x_3\ne x_5\qquad\mbox{cnf}(\mbox{premise}_9,\mbox{hypothesis})$

$x_9\ne x_{10}\qquad\mbox{cnf}(\mbox{premise}_{10},\mbox{hypothesis})$

$x_2\ne x_7\qquad\mbox{cnf}(\mbox{premise}_{11},\mbox{hypothesis})$

$\mbox{heap}(\mbox{sep}(\mbox{lseg}(x_2,x_4),\mbox{sep}(\mbox{lseg}(x_{10},x_3),\mbox{sep}(\mbox{lseg}(x_3,x_9),\mbox{sep}(\mbox{lseg}(x_3,x_1),\mbox{sep}(\mbox{lseg}(x_4,x_9),\mbox{sep}(\mbox{lseg}(x_4,x_8),\mbox{sep}(\mbox{lseg}(x_6,x_{10}),\mbox{emp}))))))))\qquad\mbox{cnf}(\mbox{premise}_{12},\mbox{hypothesis})$

$\mbox{heap}(\mbox{emp}) \ \Rightarrow \ x_1 = x_1\qquad\mbox{cnf}(\mbox{conclusion}_1,\mbox{negated\_conjecture})$

\medskip\textbf{SWW424-1.p} Verification Condition generated by Smallfoot

This is one of the verification conditions that were gathered
 from the output of Smallfoot when checking assertions on list
 manipulating programs from its own benchmark suite.




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

$\mbox{nil}\ne x_1\qquad\mbox{cnf}(\mbox{premise}_1,\mbox{hypothesis})$

$x_2\ne x_1\qquad\mbox{cnf}(\mbox{premise}_2,\mbox{hypothesis})$

$x_2\ne x_3\qquad\mbox{cnf}(\mbox{premise}_3,\mbox{hypothesis})$

$x_1\ne x_3\qquad\mbox{cnf}(\mbox{premise}_4,\mbox{hypothesis})$

$\mbox{heap}(\mbox{sep}(\mbox{next}(x_1,x_3),\mbox{sep}(\mbox{lseg}(x_2,\mbox{nil}),\mbox{emp})))\qquad\mbox{cnf}(\mbox{premise}_5,\mbox{hypothesis})$

$\neg\,\mbox{heap}(\mbox{sep}(\mbox{lseg}(x_2,\mbox{nil}),\mbox{emp}))\qquad\mbox{cnf}(\mbox{conclusion}_1,\mbox{negated\_conjecture})$

\medskip\textbf{SWW408-1.p} Verification Condition generated by Smallfoot

This is one of the verification conditions that were gathered
 from the output of Smallfoot when checking assertions on list
 manipulating programs from its own benchmark suite.




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

$\mbox{nil}\ne x_1\qquad\mbox{cnf}(\mbox{premise}_1,\mbox{hypothesis})$

$\mbox{nil}\ne x_2\qquad\mbox{cnf}(\mbox{premise}_2,\mbox{hypothesis})$

$x_1\ne x_2\qquad\mbox{cnf}(\mbox{premise}_3,\mbox{hypothesis})$

$x_1\ne x_3\qquad\mbox{cnf}(\mbox{premise}_4,\mbox{hypothesis})$

$x_2\ne x_3\qquad\mbox{cnf}(\mbox{premise}_5,\mbox{hypothesis})$

$\mbox{heap}(\mbox{sep}(\mbox{next}(x_1,x_2),\mbox{sep}(\mbox{lseg}(x_3,\mbox{nil}),\mbox{sep}(\mbox{next}(x_2,x_3),\mbox{emp}))))\qquad\mbox{cnf}(\mbox{premise}_6,\mbox{hypothesis})$

$\neg\,\mbox{heap}(\mbox{sep}(\mbox{lseg}(x_3,\mbox{nil}),\mbox{emp}))\qquad\mbox{cnf}(\mbox{conclusion}_1,\mbox{negated\_conjecture})$

\medskip\textbf{SWW452-1.p} Randomly generated entailment of the form F $\to$ G (n = 12)

A randomly generated entailment with n program variables.
 A random graph with pointers and list segments is generated,
 and then some of the segments are folded. The task is to
 prove whether the unfolded version entails the folded one.
 Parameters are chosen so that about half of the generated
 entailments are valid.
 These entailments stress the role of unfolding axioms.




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

$\mbox{heap}(\mbox{sep}(\mbox{next}(x_5,x_6),\mbox{sep}(\mbox{next}(x_{12},x_4),\mbox{sep}(\mbox{next}(x_8,x_6),\mbox{sep}(\mbox{lseg}(x_1,x_8),\mbox{sep}(\mbox{next}(x_{11},x_5),\mbox{sep}(\mbox{lseg}(x_4,x_3),\mbox{sep}(\mbox{next}(x_2,x_4),\mbox{sep}(\mbox{next}(x_9,x_6),\mbox{sep}(\mbox{next}(x_3,x_7),\mbox{sep}(\mbox{lseg}(x_6,x_8),\mbox{sep}(\mbox{next}(x_7,x_{10}),\mbox{sep}(\mbox{lseg}(x_{10},x_3),\mbox{emp})))))))))))))\qquad\mbox{cnf}(\mbox{premise}_1,\mbox{hypothesis})$

$\neg\,\mbox{heap}(\mbox{sep}(\mbox{lseg}(x_9,x_6),\mbox{sep}(\mbox{lseg}(x_2,x_4),\mbox{sep}(\mbox{lseg}(x_{12},x_7),\mbox{sep}(\mbox{lseg}(x_{11},x_8),\mbox{sep}(\mbox{lseg}(x_1,x_6),\mbox{sep}(\mbox{lseg}(x_7,x_3),\mbox{emp})))))))\qquad\mbox{cnf}(\mbox{conclusion}_1,\mbox{negated\_conjecture})$

\medskip\textbf{SWW457-1.p} Randomly generated entailment of the form F $\to$ G (n = 15)

A randomly generated entailment with n program variables.
 A random graph with pointers and list segments is generated,
 and then some of the segments are folded. The task is to
 prove whether the unfolded version entails the folded one.
 Parameters are chosen so that about half of the generated
 entailments are valid.
 These entailments stress the role of unfolding axioms.




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

$\mbox{heap}(\mbox{sep}(\mbox{next}(x_{13},x_3),\mbox{sep}(\mbox{lseg}(x_{14},x_2),\mbox{sep}(\mbox{lseg}(x_{11},x_{12}),\mbox{sep}(\mbox{next}(x_4,x_{12}),\mbox{sep}(\mbox{next}(x_{10},x_{15}),\mbox{sep}(\mbox{next}(x_2,x_1),\mbox{sep}(\mbox{next}(x_8,x_2),\mbox{sep}(\mbox{next}(x_6,x_8),\mbox{sep}(\mbox{next}(x_{12},x_6),\mbox{sep}(\mbox{next}(x_3,x_4),\mbox{sep}(\mbox{lseg}(x_7,x_{11}),\mbox{sep}(\mbox{lseg}(x_{15},x_2),\mbox{sep}(\mbox{next}(x_5,x_7),\mbox{sep}(\mbox{next}(x_1,x_6),\mbox{sep}(\mbox{next}(x_9,x_{11}),\mbox{emp}))))))))))))))))\qquad\mbox{cnf}(\mbox{premise}_1,\mbox{hypothesis})$

$\neg\,\mbox{heap}(\mbox{sep}(\mbox{lseg}(x_{14},x_2),\mbox{sep}(\mbox{lseg}(x_{13},x_3),\mbox{sep}(\mbox{lseg}(x_9,x_{11}),\mbox{sep}(\mbox{lseg}(x_{10},x_1),\mbox{sep}(\mbox{lseg}(x_5,x_{12}),\mbox{sep}(\mbox{lseg}(x_3,x_6),\mbox{sep}(\mbox{lseg}(x_1,x_2),\mbox{emp}))))))))\qquad\mbox{cnf}(\mbox{conclusion}_1,\mbox{negated\_conjecture})$

\medskip\textbf{SWW403-1.p} Verification Condition generated by Smallfoot

This is one of the verification conditions that were gathered
 from the output of Smallfoot when checking assertions on list
 manipulating programs from its own benchmark suite.




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

$\mbox{nil}\ne x_1\qquad\mbox{cnf}(\mbox{premise}_1,\mbox{hypothesis})$

$\mbox{nil}\ne x_2\qquad\mbox{cnf}(\mbox{premise}_2,\mbox{hypothesis})$

$\mbox{nil}\ne x_3\qquad\mbox{cnf}(\mbox{premise}_3,\mbox{hypothesis})$

$\mbox{nil}\ne x_4\qquad\mbox{cnf}(\mbox{premise}_4,\mbox{hypothesis})$

$x_2\ne x_3\qquad\mbox{cnf}(\mbox{premise}_5,\mbox{hypothesis})$

$x_2\ne x_4\qquad\mbox{cnf}(\mbox{premise}_6,\mbox{hypothesis})$

$\mbox{heap}(\mbox{sep}(\mbox{lseg}(x_1,x_4),\mbox{sep}(\mbox{next}(x_4,x_1),\mbox{emp})))\qquad\mbox{cnf}(\mbox{premise}_7,\mbox{hypothesis})$

$\neg\,\mbox{heap}(\mbox{sep}(\mbox{lseg}(x_5,x_4),\mbox{sep}(\mbox{next}(x_4,x_5),\mbox{emp})))\qquad\mbox{cnf}(\mbox{conclusion}_1,\mbox{negated\_conjecture})$

\medskip\textbf{SWW442-1.p} Randomly generated entailment of the form F $\to$ $\bot$ (n = 18)

A randomly generated entailment with n program variables.
 Negated equalities and list segments are added at random, with
 specific paramenters so that about half of the generated
 entailments are valid (or, equivalently, F is unsatisfiable).
 Normalization and well-formedness axioms should be enough to
 decide these entailments.




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

$x_6\ne x_{13}\qquad\mbox{cnf}(\mbox{premise}_1,\mbox{hypothesis})$

$x_6\ne x_{16}\qquad\mbox{cnf}(\mbox{premise}_2,\mbox{hypothesis})$

$x_{11}\ne x_{18}\qquad\mbox{cnf}(\mbox{premise}_3,\mbox{hypothesis})$

$x_{11}\ne x_{17}\qquad\mbox{cnf}(\mbox{premise}_4,\mbox{hypothesis})$

$x_3\ne x_{16}\qquad\mbox{cnf}(\mbox{premise}_5,\mbox{hypothesis})$

$x_3\ne x_{12}\qquad\mbox{cnf}(\mbox{premise}_6,\mbox{hypothesis})$

$x_3\ne x_{17}\qquad\mbox{cnf}(\mbox{premise}_7,\mbox{hypothesis})$

$x_7\ne x_{13}\qquad\mbox{cnf}(\mbox{premise}_8,\mbox{hypothesis})$

$x_7\ne x_{14}\qquad\mbox{cnf}(\mbox{premise}_9,\mbox{hypothesis})$

$x_7\ne x_{15}\qquad\mbox{cnf}(\mbox{premise}_{10},\mbox{hypothesis})$

$x_9\ne x_{13}\qquad\mbox{cnf}(\mbox{premise}_{11},\mbox{hypothesis})$

$x_9\ne x_{17}\qquad\mbox{cnf}(\mbox{premise}_{12},\mbox{hypothesis})$

$x_2\ne x_8\qquad\mbox{cnf}(\mbox{premise}_{13},\mbox{hypothesis})$

$x_2\ne x_6\qquad\mbox{cnf}(\mbox{premise}_{14},\mbox{hypothesis})$

$x_2\ne x_{11}\qquad\mbox{cnf}(\mbox{premise}_{15},\mbox{hypothesis})$

$x_2\ne x_{17}\qquad\mbox{cnf}(\mbox{premise}_{16},\mbox{hypothesis})$

$x_{12}\ne x_{14}\qquad\mbox{cnf}(\mbox{premise}_{17},\mbox{hypothesis})$

$x_8\ne x_{14}\qquad\mbox{cnf}(\mbox{premise}_{18},\mbox{hypothesis})$

$x_1\ne x_{10}\qquad\mbox{cnf}(\mbox{premise}_{19},\mbox{hypothesis})$

$x_1\ne x_{15}\qquad\mbox{cnf}(\mbox{premise}_{20},\mbox{hypothesis})$

$x_4\ne x_{11}\qquad\mbox{cnf}(\mbox{premise}_{21},\mbox{hypothesis})$

$x_4\ne x_9\qquad\mbox{cnf}(\mbox{premise}_{22},\mbox{hypothesis})$

$x_4\ne x_{13}\qquad\mbox{cnf}(\mbox{premise}_{23},\mbox{hypothesis})$

$x_{13}\ne x_{18}\qquad\mbox{cnf}(\mbox{premise}_{24},\mbox{hypothesis})$

$x_{10}\ne x_{11}\qquad\mbox{cnf}(\mbox{premise}_{25},\mbox{hypothesis})$

$x_{10}\ne x_{12}\qquad\mbox{cnf}(\mbox{premise}_{26},\mbox{hypothesis})$

$x_5\ne x_6\qquad\mbox{cnf}(\mbox{premise}_{27},\mbox{hypothesis})$

$x_5\ne x_{16}\qquad\mbox{cnf}(\mbox{premise}_{28},\mbox{hypothesis})$

$\mbox{heap}(\mbox{sep}(\mbox{lseg}(x_5,x_{14}),\mbox{sep}(\mbox{lseg}(x_{13},x_{15}),\mbox{sep}(\mbox{lseg}(x_{13},x_{12}),\mbox{sep}(\mbox{lseg}(x_{13},x_2),\mbox{sep}(\mbox{lseg}(x_{10},x_{11}),\mbox{sep}(\mbox{lseg}(x_{18},x_{10}),\mbox{sep}(\mbox{lseg}(x_{18},x_{11}),\mbox{sep}(\mbox{lseg}(x_1,x_5),\mbox{sep}(\mbox{lseg}(x_4,x_{15}),\mbox{sep}(\mbox{lseg}(x_4,x_{11}),\mbox{sep}(\mbox{lseg}(x_{15},x_{16}),\mbox{sep}(\mbox{lseg}(x_{17},x_{10}),\mbox{sep}(\mbox{lseg}(x_2,x_{16}),\mbox{sep}(\mbox{lseg}(x_2,x_6),\mbox{sep}(\mbox{lseg}(x_9,x_{15}),\mbox{sep}(\mbox{lseg}(x_7,x_{12}),\mbox{sep}(\mbox{lseg}(x_7,x_{13}),\mbox{sep}(\mbox{lseg}(x_{11},x_9),\mbox{emp})))))))))))))))))))\qquad\mbox{cnf}(\mbox{premise}_{29},\mbox{hypothesis})$

$\mbox{heap}(\mbox{emp}) \ \Rightarrow \ x_1 = x_1\qquad\mbox{cnf}(\mbox{conclusion}_1,\mbox{negated\_conjecture})$

\medskip\textbf{SWW441-1.p} Randomly generated entailment of the form F $\to$ $\bot$ (n = 18)

A randomly generated entailment with n program variables.
 Negated equalities and list segments are added at random, with
 specific paramenters so that about half of the generated
 entailments are valid (or, equivalently, F is unsatisfiable).
 Normalization and well-formedness axioms should be enough to
 decide these entailments.




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

$x_6\ne x_8\qquad\mbox{cnf}(\mbox{premise}_1,\mbox{hypothesis})$

$x_6\ne x_9\qquad\mbox{cnf}(\mbox{premise}_2,\mbox{hypothesis})$

$x_6\ne x_{13}\qquad\mbox{cnf}(\mbox{premise}_3,\mbox{hypothesis})$

$x_6\ne x_{17}\qquad\mbox{cnf}(\mbox{premise}_4,\mbox{hypothesis})$

$x_6\ne x_{12}\qquad\mbox{cnf}(\mbox{premise}_5,\mbox{hypothesis})$

$x_3\ne x_6\qquad\mbox{cnf}(\mbox{premise}_6,\mbox{hypothesis})$

$x_3\ne x_4\qquad\mbox{cnf}(\mbox{premise}_7,\mbox{hypothesis})$

$x_3\ne x_{18}\qquad\mbox{cnf}(\mbox{premise}_8,\mbox{hypothesis})$

$x_3\ne x_{13}\qquad\mbox{cnf}(\mbox{premise}_9,\mbox{hypothesis})$

$x_3\ne x_{17}\qquad\mbox{cnf}(\mbox{premise}_{10},\mbox{hypothesis})$

$x_3\ne x_5\qquad\mbox{cnf}(\mbox{premise}_{11},\mbox{hypothesis})$

$x_3\ne x_{15}\qquad\mbox{cnf}(\mbox{premise}_{12},\mbox{hypothesis})$

$x_7\ne x_{11}\qquad\mbox{cnf}(\mbox{premise}_{13},\mbox{hypothesis})$

$x_7\ne x_{16}\qquad\mbox{cnf}(\mbox{premise}_{14},\mbox{hypothesis})$

$x_7\ne x_{15}\qquad\mbox{cnf}(\mbox{premise}_{15},\mbox{hypothesis})$

$x_9\ne x_{16}\qquad\mbox{cnf}(\mbox{premise}_{16},\mbox{hypothesis})$

$x_{17}\ne x_{18}\qquad\mbox{cnf}(\mbox{premise}_{17},\mbox{hypothesis})$

$x_2\ne x_8\qquad\mbox{cnf}(\mbox{premise}_{18},\mbox{hypothesis})$

$x_2\ne x_{11}\qquad\mbox{cnf}(\mbox{premise}_{19},\mbox{hypothesis})$

$x_2\ne x_{18}\qquad\mbox{cnf}(\mbox{premise}_{20},\mbox{hypothesis})$

$x_2\ne x_3\qquad\mbox{cnf}(\mbox{premise}_{21},\mbox{hypothesis})$

$x_2\ne x_{10}\qquad\mbox{cnf}(\mbox{premise}_{22},\mbox{hypothesis})$

$x_2\ne x_{16}\qquad\mbox{cnf}(\mbox{premise}_{23},\mbox{hypothesis})$

$x_2\ne x_5\qquad\mbox{cnf}(\mbox{premise}_{24},\mbox{hypothesis})$

$x_{12}\ne x_{13}\qquad\mbox{cnf}(\mbox{premise}_{25},\mbox{hypothesis})$

$x_{15}\ne x_{16}\qquad\mbox{cnf}(\mbox{premise}_{26},\mbox{hypothesis})$

$x_8\ne x_{11}\qquad\mbox{cnf}(\mbox{premise}_{27},\mbox{hypothesis})$

$x_8\ne x_{10}\qquad\mbox{cnf}(\mbox{premise}_{28},\mbox{hypothesis})$

$x_8\ne x_{15}\qquad\mbox{cnf}(\mbox{premise}_{29},\mbox{hypothesis})$

$x_4\ne x_{18}\qquad\mbox{cnf}(\mbox{premise}_{30},\mbox{hypothesis})$

$x_4\ne x_9\qquad\mbox{cnf}(\mbox{premise}_{31},\mbox{hypothesis})$

$x_4\ne x_{14}\qquad\mbox{cnf}(\mbox{premise}_{32},\mbox{hypothesis})$

$x_4\ne x_{15}\qquad\mbox{cnf}(\mbox{premise}_{33},\mbox{hypothesis})$

$x_1\ne x_8\qquad\mbox{cnf}(\mbox{premise}_{34},\mbox{hypothesis})$

$x_1\ne x_{11}\qquad\mbox{cnf}(\mbox{premise}_{35},\mbox{hypothesis})$

$x_1\ne x_{18}\qquad\mbox{cnf}(\mbox{premise}_{36},\mbox{hypothesis})$

$x_1\ne x_{15}\qquad\mbox{cnf}(\mbox{premise}_{37},\mbox{hypothesis})$

$x_1\ne x_5\qquad\mbox{cnf}(\mbox{premise}_{38},\mbox{hypothesis})$

$x_{10}\ne x_{18}\qquad\mbox{cnf}(\mbox{premise}_{39},\mbox{hypothesis})$

$x_{10}\ne x_{15}\qquad\mbox{cnf}(\mbox{premise}_{40},\mbox{hypothesis})$

$x_{16}\ne x_{17}\qquad\mbox{cnf}(\mbox{premise}_{41},\mbox{hypothesis})$

$x_5\ne x_6\qquad\mbox{cnf}(\mbox{premise}_{42},\mbox{hypothesis})$

$x_5\ne x_{16}\qquad\mbox{cnf}(\mbox{premise}_{43},\mbox{hypothesis})$

$\mbox{heap}(\mbox{sep}(\mbox{lseg}(x_5,x_1),\mbox{sep}(\mbox{lseg}(x_{10},x_{13}),\mbox{sep}(\mbox{lseg}(x_{10},x_{18}),\mbox{sep}(\mbox{lseg}(x_{18},x_1),\mbox{sep}(\mbox{lseg}(x_{15},x_{11}),\mbox{sep}(\mbox{lseg}(x_{14},x_{17}),\mbox{sep}(\mbox{lseg}(x_{12},x_{18}),\mbox{sep}(\mbox{lseg}(x_9,x_{12}),\mbox{sep}(\mbox{lseg}(x_7,x_{14}),\mbox{sep}(\mbox{lseg}(x_7,x_{12}),\mbox{sep}(\mbox{lseg}(x_6,x_9),\mbox{emp}))))))))))))\qquad\mbox{cnf}(\mbox{premise}_{44},\mbox{hypothesis})$

$\mbox{heap}(\mbox{emp}) \ \Rightarrow \ x_1 = x_1\qquad\mbox{cnf}(\mbox{conclusion}_1,\mbox{negated\_conjecture})$

\medskip\textbf{SWW401-1.p} Verification Condition generated by Smallfoot

This is one of the verification conditions that were gathered
 from the output of Smallfoot when checking assertions on list
 manipulating programs from its own benchmark suite.




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

$\mbox{nil}\ne x_1\qquad\mbox{cnf}(\mbox{premise}_1,\mbox{hypothesis})$

$\mbox{nil}\ne x_2\qquad\mbox{cnf}(\mbox{premise}_2,\mbox{hypothesis})$

$\mbox{heap}(\mbox{sep}(\mbox{lseg}(x_1,x_2),\mbox{sep}(\mbox{next}(x_2,x_1),\mbox{emp})))\qquad\mbox{cnf}(\mbox{premise}_3,\mbox{hypothesis})$

$\neg\,\mbox{heap}(\mbox{sep}(\mbox{lseg}(x_3,x_2),\mbox{sep}(\mbox{next}(x_2,x_3),\mbox{emp})))\qquad\mbox{cnf}(\mbox{conclusion}_1,\mbox{negated\_conjecture})$

\medskip\textbf{SWW447-1.p} Randomly generated entailment of the form F $\to$ G (n = 10)

A randomly generated entailment with n program variables.
 A random graph with pointers and list segments is generated,
 and then some of the segments are folded. The task is to
 prove whether the unfolded version entails the folded one.
 Parameters are chosen so that about half of the generated
 entailments are valid.
 These entailments stress the role of unfolding axioms.




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

$\mbox{heap}(\mbox{sep}(\mbox{lseg}(x_2,x_7),\mbox{sep}(\mbox{next}(x_6,x_1),\mbox{sep}(\mbox{next}(x_4,x_9),\mbox{sep}(\mbox{next}(x_3,x_2),\mbox{sep}(\mbox{next}(x_8,x_4),\mbox{sep}(\mbox{lseg}(x_{10},x_2),\mbox{sep}(\mbox{next}(x_5,x_7),\mbox{sep}(\mbox{next}(x_1,x_6),\mbox{sep}(\mbox{next}(x_9,x_1),\mbox{sep}(\mbox{lseg}(x_7,x_2),\mbox{emp})))))))))))\qquad\mbox{cnf}(\mbox{premise}_1,\mbox{hypothesis})$

$\neg\,\mbox{heap}(\mbox{sep}(\mbox{lseg}(x_6,x_1),\mbox{sep}(\mbox{lseg}(x_{10},x_2),\mbox{sep}(\mbox{lseg}(x_8,x_4),\mbox{sep}(\mbox{lseg}(x_3,x_2),\mbox{sep}(\mbox{lseg}(x_5,x_7),\mbox{sep}(\mbox{lseg}(x_4,x_6),\mbox{sep}(\mbox{lseg}(x_2,x_7),\mbox{sep}(\mbox{lseg}(x_7,x_2),\mbox{emp})))))))))\qquad\mbox{cnf}(\mbox{conclusion}_1,\mbox{negated\_conjecture})$

\medskip\textbf{SWW581=2.p} Checking a large routine-T-WP parameter routine






$\mbox{uni}{:}\;\mbox{\$tType}\qquad\mbox{tff}(\mbox{uni},\mbox{type})$

$\mbox{ty}{:}\;\mbox{\$tType}\qquad\mbox{tff}(\mbox{ty},\mbox{type})$

$\mbox{sort}{:}\;( \mbox{ty}\times \mbox{uni} )\to \mbox{\$o}\qquad\mbox{tff}(\mbox{sort},\mbox{type})$

$\mbox{witness}{:}\;\mbox{ty}\to \mbox{uni}\qquad\mbox{tff}(\mbox{witness},\mbox{type})$

$\forall a{:}\;\mbox{ty}{:}\;\mbox{sort}(a,\mbox{witness}(a))\qquad\mbox{tff}(\mbox{witness\_sort},\mbox{axiom})$

$\mbox{int}{:}\;\mbox{ty}\qquad\mbox{tff}(\mbox{int},\mbox{type})$

$\mbox{real}{:}\;\mbox{ty}\qquad\mbox{tff}(\mbox{real},\mbox{type})$

$\mbox{bool}{:}\;\mbox{\$tType}\qquad\mbox{tff}(\mbox{bool},\mbox{type})$

$\mbox{bool}_1{:}\;\mbox{ty}\qquad\mbox{tff}(\mbox{bool}_1,\mbox{type})$

$\mbox{true}{:}\;\mbox{bool}\qquad\mbox{tff}(\mbox{true},\mbox{type})$

$\mbox{false}{:}\;\mbox{bool}\qquad\mbox{tff}(\mbox{false},\mbox{type})$

$\mbox{match\_bool}{:}\;( \mbox{ty}\times \mbox{bool}\times \mbox{uni}\times \mbox{uni} )\to \mbox{uni}\qquad\mbox{tff}(\mbox{match\_bool},\mbox{type})$

$\forall a{:}\;\mbox{ty},x{:}\;\mbox{bool},x_1{:}\;\mbox{uni},x_2{:}\;\mbox{uni}{:}\;\mbox{sort}(a,\mbox{match\_bool}(a,x,x_1,x_2))\qquad\mbox{tff}(\mbox{match\_bool\_sort},\mbox{axiom})$

$\forall a{:}\;\mbox{ty},z{:}\;\mbox{uni},z_1{:}\;\mbox{uni}{:}\;( \mbox{sort}(a,z) \ \Rightarrow \ \mbox{match\_bool}(a,\mbox{true},z,z_1) = z )\qquad\mbox{tff}(\mbox{match\_bool\_True},\mbox{axiom})$

$\forall a{:}\;\mbox{ty},z{:}\;\mbox{uni},z_1{:}\;\mbox{uni}{:}\;( \mbox{sort}(a,z_1) \ \Rightarrow \ \mbox{match\_bool}(a,\mbox{false},z,z_1) = z_1 )\qquad\mbox{tff}(\mbox{match\_bool\_False},\mbox{axiom})$

$\mbox{true}\ne \mbox{false}\qquad\mbox{tff}(\mbox{true\_False},\mbox{axiom})$

$\forall u{:}\;\mbox{bool}{:}\;( u = \mbox{true}\mbox{ or }u = \mbox{false} )\qquad\mbox{tff}(\mbox{bool\_inversion},\mbox{axiom})$

$\mbox{tuple}_0{:}\;\mbox{\$tType}\qquad\mbox{tff}(\mbox{tuple}_0,\mbox{type})$

$\mbox{tuple}_{01}{:}\;\mbox{ty}\qquad\mbox{tff}(\mbox{tuple}_{01},\mbox{type})$

$\mbox{tuple}_{02}{:}\;\mbox{tuple}_0\qquad\mbox{tff}(\mbox{tuple}_{02},\mbox{type})$

$\forall u{:}\;\mbox{tuple}_0{:}\;u = \mbox{tuple}_{02}\qquad\mbox{tff}(\mbox{tuple0\_inversion},\mbox{axiom})$

$\mbox{qtmark}{:}\;\mbox{ty}\qquad\mbox{tff}(\mbox{qtmark},\mbox{type})$

$\forall x{:}\;\mbox{\$int},y{:}\;\mbox{\$int},z{:}\;\mbox{\$int}{:}\;( \mbox{\$lesseq}(x,y) \ \Rightarrow \ ( \mbox{\$lesseq}(0,z) \ \Rightarrow \ \mbox{\$lesseq}(\mbox{\$product}(x,z),\mbox{\$product}(y,z)) ) )\qquad\mbox{tff}(\mbox{compatOrderMult},\mbox{axiom})$

$\mbox{fact}{:}\;\mbox{\$int}\to \mbox{\$int}\qquad\mbox{tff}(\mbox{fact},\mbox{type})$

$\mbox{fact}(0) = 1\qquad\mbox{tff}(\mbox{fact}_0,\mbox{axiom})$

$\forall n{:}\;\mbox{\$int}{:}\;( \mbox{\$lesseq}(1,n) \ \Rightarrow \ \mbox{fact}(n) = \mbox{\$product}(n,\mbox{fact}(\mbox{\$difference}(n,1))) )\qquad\mbox{tff}(\mbox{factn},\mbox{axiom})$

$\mbox{ref}{:}\;\mbox{ty}\to \mbox{ty}\qquad\mbox{tff}(\mbox{ref},\mbox{type})$

$\mbox{mk\_ref}{:}\;( \mbox{ty}\times \mbox{uni} )\to \mbox{uni}\qquad\mbox{tff}(\mbox{mk\_ref},\mbox{type})$

$\forall a{:}\;\mbox{ty},x{:}\;\mbox{uni}{:}\;\mbox{sort}(\mbox{ref}(a),\mbox{mk\_ref}(a,x))\qquad\mbox{tff}(\mbox{mk\_ref\_sort},\mbox{axiom})$

$\mbox{contents}{:}\;( \mbox{ty}\times \mbox{uni} )\to \mbox{uni}\qquad\mbox{tff}(\mbox{contents},\mbox{type})$

$\forall a{:}\;\mbox{ty},x{:}\;\mbox{uni}{:}\;\mbox{sort}(a,\mbox{contents}(a,x))\qquad\mbox{tff}(\mbox{contents\_sort},\mbox{axiom})$

$\forall a{:}\;\mbox{ty},u{:}\;\mbox{uni}{:}\;( \mbox{sort}(a,u) \ \Rightarrow \ \mbox{contents}(a,\mbox{mk\_ref}(a,u)) = u )\qquad\mbox{tff}(\mbox{contents\_def},\mbox{axiom})$

$\forall a{:}\;\mbox{ty},u{:}\;\mbox{uni}{:}\;( \mbox{sort}(\mbox{ref}(a),u) \ \Rightarrow \ u = \mbox{mk\_ref}(a,\mbox{contents}(a,u)) )\qquad\mbox{tff}(\mbox{ref\_inversion},\mbox{axiom})$

$\forall n{:}\;\mbox{\$int}{:}\;( \mbox{\$lesseq}(0,n) \ \Rightarrow \ \forall u{:}\;\mbox{\$int},r{:}\;\mbox{\$int}{:}\;( ( \mbox{\$lesseq}(0,r)\mbox{ and }\mbox{\$lesseq}(r,n)\mbox{ and }u = \mbox{fact}(r) ) \ \Rightarrow \ ( \mbox{\$less}(r,n) \ \Rightarrow \ \forall s{:}\;\mbox{\$int},u_1{:}\;\mbox{\$int}{:}\;( ( \mbox{\$lesseq}(1,s)\mbox{ and }\mbox{\$lesseq}(s,\mbox{\$sum}(r,1))\mbox{ and }u_1 = \mbox{\$product}(s,\mbox{fact}(r)) ) \ \Rightarrow \ ( \neg\,\mbox{\$lesseq}(s,r) \ \Rightarrow \ \forall r_1{:}\;\mbox{\$int}{:}\;( r_1 = \mbox{\$sum}(r,1) \ \Rightarrow \ ( \mbox{\$lesseq}(0,r_1)\mbox{ and }\mbox{\$lesseq}(r_1,n)\mbox{ and }u_1 = \mbox{fact}(r_1) ) ) ) ) ) ) )\qquad\mbox{tff}(\mbox{wP\_parameter\_routine},\mbox{conjecture})$

\medskip\textbf{SWW398-1.p} Verification Condition generated by Smallfoot

This is one of the verification conditions that were gathered
 from the output of Smallfoot when checking assertions on list
 manipulating programs from its own benchmark suite.




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

$\mbox{nil}\ne x_1\qquad\mbox{cnf}(\mbox{premise}_1,\mbox{hypothesis})$

$\mbox{heap}(\mbox{sep}(\mbox{next}(x_1,\mbox{nil}),\mbox{emp}))\qquad\mbox{cnf}(\mbox{premise}_2,\mbox{hypothesis})$

$\neg\,\mbox{heap}(\mbox{sep}(\mbox{lseg}(\mbox{nil},\mbox{nil}),\mbox{emp}))\qquad\mbox{cnf}(\mbox{conclusion}_1,\mbox{negated\_conjecture})$

\medskip\textbf{SWW437-1.p} Randomly generated entailment of the form F $\to$ $\bot$ (n = 16)

A randomly generated entailment with n program variables.
 Negated equalities and list segments are added at random, with
 specific paramenters so that about half of the generated
 entailments are valid (or, equivalently, F is unsatisfiable).
 Normalization and well-formedness axioms should be enough to
 decide these entailments.




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

$x_6\ne x_7\qquad\mbox{cnf}(\mbox{premise}_1,\mbox{hypothesis})$

$x_6\ne x_9\qquad\mbox{cnf}(\mbox{premise}_2,\mbox{hypothesis})$

$x_{11}\ne x_{16}\qquad\mbox{cnf}(\mbox{premise}_3,\mbox{hypothesis})$

$x_{11}\ne x_{12}\qquad\mbox{cnf}(\mbox{premise}_4,\mbox{hypothesis})$

$x_3\ne x_6\qquad\mbox{cnf}(\mbox{premise}_5,\mbox{hypothesis})$

$x_3\ne x_8\qquad\mbox{cnf}(\mbox{premise}_6,\mbox{hypothesis})$

$x_3\ne x_{11}\qquad\mbox{cnf}(\mbox{premise}_7,\mbox{hypothesis})$

$x_3\ne x_4\qquad\mbox{cnf}(\mbox{premise}_8,\mbox{hypothesis})$

$x_7\ne x_8\qquad\mbox{cnf}(\mbox{premise}_9,\mbox{hypothesis})$

$x_7\ne x_{16}\qquad\mbox{cnf}(\mbox{premise}_{10},\mbox{hypothesis})$

$x_7\ne x_{15}\qquad\mbox{cnf}(\mbox{premise}_{11},\mbox{hypothesis})$

$x_2\ne x_7\qquad\mbox{cnf}(\mbox{premise}_{12},\mbox{hypothesis})$

$x_8\ne x_9\qquad\mbox{cnf}(\mbox{premise}_{13},\mbox{hypothesis})$

$x_1\ne x_{11}\qquad\mbox{cnf}(\mbox{premise}_{14},\mbox{hypothesis})$

$x_1\ne x_{13}\qquad\mbox{cnf}(\mbox{premise}_{15},\mbox{hypothesis})$

$x_1\ne x_{12}\qquad\mbox{cnf}(\mbox{premise}_{16},\mbox{hypothesis})$

$x_1\ne x_2\qquad\mbox{cnf}(\mbox{premise}_{17},\mbox{hypothesis})$

$x_4\ne x_7\qquad\mbox{cnf}(\mbox{premise}_{18},\mbox{hypothesis})$

$x_4\ne x_9\qquad\mbox{cnf}(\mbox{premise}_{19},\mbox{hypothesis})$

$x_4\ne x_{14}\qquad\mbox{cnf}(\mbox{premise}_{20},\mbox{hypothesis})$

$x_{10}\ne x_{16}\qquad\mbox{cnf}(\mbox{premise}_{21},\mbox{hypothesis})$

$x_{10}\ne x_{12}\qquad\mbox{cnf}(\mbox{premise}_{22},\mbox{hypothesis})$

$x_{10}\ne x_{14}\qquad\mbox{cnf}(\mbox{premise}_{23},\mbox{hypothesis})$

$x_{13}\ne x_{16}\qquad\mbox{cnf}(\mbox{premise}_{24},\mbox{hypothesis})$

$x_{13}\ne x_{14}\qquad\mbox{cnf}(\mbox{premise}_{25},\mbox{hypothesis})$

$x_5\ne x_{16}\qquad\mbox{cnf}(\mbox{premise}_{26},\mbox{hypothesis})$

$\mbox{heap}(\mbox{sep}(\mbox{lseg}(x_5,x_1),\mbox{sep}(\mbox{lseg}(x_{12},x_8),\mbox{sep}(\mbox{lseg}(x_2,x_6),\mbox{sep}(\mbox{lseg}(x_{16},x_7),\mbox{sep}(\mbox{lseg}(x_{16},x_3),\mbox{sep}(\mbox{lseg}(x_{10},x_{15}),\mbox{sep}(\mbox{lseg}(x_{10},x_5),\mbox{sep}(\mbox{lseg}(x_7,x_1),\mbox{sep}(\mbox{lseg}(x_3,x_{12}),\mbox{sep}(\mbox{lseg}(x_3,x_{16}),\mbox{sep}(\mbox{lseg}(x_{11},x_8),\mbox{emp}))))))))))))\qquad\mbox{cnf}(\mbox{premise}_{27},\mbox{hypothesis})$

$\mbox{heap}(\mbox{emp}) \ \Rightarrow \ x_1 = x_1\qquad\mbox{cnf}(\mbox{conclusion}_1,\mbox{negated\_conjecture})$

\medskip\textbf{SWW449-1.p} Randomly generated entailment of the form F $\to$ G (n = 11)

A randomly generated entailment with n program variables.
 A random graph with pointers and list segments is generated,
 and then some of the segments are folded. The task is to
 prove whether the unfolded version entails the folded one.
 Parameters are chosen so that about half of the generated
 entailments are valid.
 These entailments stress the role of unfolding axioms.




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

$\mbox{heap}(\mbox{sep}(\mbox{next}(x_1,x_{11}),\mbox{sep}(\mbox{next}(x_3,x_1),\mbox{sep}(\mbox{next}(x_6,x_2),\mbox{sep}(\mbox{next}(x_9,x_6),\mbox{sep}(\mbox{next}(x_4,x_1),\mbox{sep}(\mbox{next}(x_8,x_3),\mbox{sep}(\mbox{next}(x_5,x_{11}),\mbox{sep}(\mbox{lseg}(x_7,x_9),\mbox{sep}(\mbox{next}(x_{11},x_3),\mbox{sep}(\mbox{next}(x_2,x_{11}),\mbox{sep}(\mbox{lseg}(x_{10},x_{11}),\mbox{emp}))))))))))))\qquad\mbox{cnf}(\mbox{premise}_1,\mbox{hypothesis})$

$\neg\,\mbox{heap}(\mbox{sep}(\mbox{lseg}(x_8,x_3),\mbox{sep}(\mbox{lseg}(x_7,x_9),\mbox{sep}(\mbox{lseg}(x_3,x_1),\mbox{sep}(\mbox{lseg}(x_4,x_1),\mbox{sep}(\mbox{lseg}(x_9,x_{11}),\mbox{sep}(\mbox{lseg}(x_{10},x_{11}),\mbox{sep}(\mbox{lseg}(x_5,x_{11}),\mbox{sep}(\mbox{lseg}(x_1,x_3),\mbox{emp})))))))))\qquad\mbox{cnf}(\mbox{conclusion}_1,\mbox{negated\_conjecture})$

\medskip\textbf{SWW103+1.p} Syntactic definitions of the logical operators






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

\medskip\textbf{SWW467-1.p} Randomly generated entailment of the form F $\to$ G (n = 20)

A randomly generated entailment with n program variables.
 A random graph with pointers and list segments is generated,
 and then some of the segments are folded. The task is to
 prove whether the unfolded version entails the folded one.
 Parameters are chosen so that about half of the generated
 entailments are valid.
 These entailments stress the role of unfolding axioms.




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

$\mbox{heap}(\mbox{sep}(\mbox{next}(x_6,x_{12}),\mbox{sep}(\mbox{lseg}(x_{15},x_7),\mbox{sep}(\mbox{lseg}(x_{10},x_1),\mbox{sep}(\mbox{next}(x_{14},x_7),\mbox{sep}(\mbox{next}(x_2,x_1),\mbox{sep}(\mbox{lseg}(x_{12},x_7),\mbox{sep}(\mbox{next}(x_9,x_{19}),\mbox{sep}(\mbox{next}(x_{13},x_{11}),\mbox{sep}(\mbox{next}(x_8,x_{17}),\mbox{sep}(\mbox{next}(x_{16},x_1),\mbox{sep}(\mbox{next}(x_1,x_{18}),\mbox{sep}(\mbox{next}(x_4,x_{19}),\mbox{sep}(\mbox{next}(x_{17},x_{11}),\mbox{sep}(\mbox{next}(x_3,x_{12}),\mbox{sep}(\mbox{next}(x_{18},x_4),\mbox{sep}(\mbox{lseg}(x_{20},x_{12}),\mbox{sep}(\mbox{next}(x_5,x_{17}),\mbox{sep}(\mbox{next}(x_{11},x_6),\mbox{sep}(\mbox{next}(x_{19},x_1),\mbox{sep}(\mbox{lseg}(x_7,x_{12}),\mbox{emp})))))))))))))))))))))\qquad\mbox{cnf}(\mbox{premise}_1,\mbox{hypothesis})$

$\neg\,\mbox{heap}(\mbox{sep}(\mbox{lseg}(x_{15},x_7),\mbox{sep}(\mbox{lseg}(x_3,x_{12}),\mbox{sep}(\mbox{lseg}(x_8,x_{17}),\mbox{sep}(\mbox{lseg}(x_{14},x_7),\mbox{sep}(\mbox{lseg}(x_5,x_{17}),\mbox{sep}(\mbox{lseg}(x_7,x_{12}),\mbox{sep}(\mbox{lseg}(x_{10},x_1),\mbox{sep}(\mbox{lseg}(x_{16},x_1),\mbox{sep}(\mbox{lseg}(x_{20},x_{12}),\mbox{sep}(\mbox{lseg}(x_{13},x_{11}),\mbox{sep}(\mbox{lseg}(x_{17},x_{11}),\mbox{sep}(\mbox{lseg}(x_9,x_1),\mbox{sep}(\mbox{lseg}(x_{11},x_7),\mbox{sep}(\mbox{lseg}(x_2,x_{19}),\mbox{emp})))))))))))))))\qquad\mbox{cnf}(\mbox{conclusion}_1,\mbox{negated\_conjecture})$

\medskip\textbf{SWW428-1.p} Randomly generated entailment of the form F $\to$ $\bot$ (n = 11)

A randomly generated entailment with n program variables.
 Negated equalities and list segments are added at random, with
 specific paramenters so that about half of the generated
 entailments are valid (or, equivalently, F is unsatisfiable).
 Normalization and well-formedness axioms should be enough to
 decide these entailments.




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

$x_8\ne x_9\qquad\mbox{cnf}(\mbox{premise}_1,\mbox{hypothesis})$

$x_6\ne x_8\qquad\mbox{cnf}(\mbox{premise}_2,\mbox{hypothesis})$

$x_6\ne x_{11}\qquad\mbox{cnf}(\mbox{premise}_3,\mbox{hypothesis})$

$x_6\ne x_{10}\qquad\mbox{cnf}(\mbox{premise}_4,\mbox{hypothesis})$

$x_4\ne x_5\qquad\mbox{cnf}(\mbox{premise}_5,\mbox{hypothesis})$

$x_1\ne x_3\qquad\mbox{cnf}(\mbox{premise}_6,\mbox{hypothesis})$

$x_3\ne x_4\qquad\mbox{cnf}(\mbox{premise}_7,\mbox{hypothesis})$

$x_9\ne x_{11}\qquad\mbox{cnf}(\mbox{premise}_8,\mbox{hypothesis})$

$x_2\ne x_4\qquad\mbox{cnf}(\mbox{premise}_9,\mbox{hypothesis})$

$\mbox{heap}(\mbox{sep}(\mbox{lseg}(x_5,x_4),\mbox{sep}(\mbox{lseg}(x_2,x_8),\mbox{sep}(\mbox{lseg}(x_9,x_7),\mbox{sep}(\mbox{lseg}(x_7,x_6),\mbox{sep}(\mbox{lseg}(x_6,x_5),\mbox{emp}))))))\qquad\mbox{cnf}(\mbox{premise}_{10},\mbox{hypothesis})$

$\mbox{heap}(\mbox{emp}) \ \Rightarrow \ x_1 = x_1\qquad\mbox{cnf}(\mbox{conclusion}_1,\mbox{negated\_conjecture})$

\medskip\textbf{SWW440-1.p} Randomly generated entailment of the form F $\to$ $\bot$ (n = 17)

A randomly generated entailment with n program variables.
 Negated equalities and list segments are added at random, with
 specific paramenters so that about half of the generated
 entailments are valid (or, equivalently, F is unsatisfiable).
 Normalization and well-formedness axioms should be enough to
 decide these entailments.




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

$x_6\ne x_{11}\qquad\mbox{cnf}(\mbox{premise}_1,\mbox{hypothesis})$

$x_6\ne x_{13}\qquad\mbox{cnf}(\mbox{premise}_2,\mbox{hypothesis})$

$x_{11}\ne x_{17}\qquad\mbox{cnf}(\mbox{premise}_3,\mbox{hypothesis})$

$x_{11}\ne x_{12}\qquad\mbox{cnf}(\mbox{premise}_4,\mbox{hypothesis})$

$x_3\ne x_{11}\qquad\mbox{cnf}(\mbox{premise}_5,\mbox{hypothesis})$

$x_3\ne x_{14}\qquad\mbox{cnf}(\mbox{premise}_6,\mbox{hypothesis})$

$x_9\ne x_{11}\qquad\mbox{cnf}(\mbox{premise}_7,\mbox{hypothesis})$

$x_2\ne x_{11}\qquad\mbox{cnf}(\mbox{premise}_8,\mbox{hypothesis})$

$x_2\ne x_7\qquad\mbox{cnf}(\mbox{premise}_9,\mbox{hypothesis})$

$x_2\ne x_{16}\qquad\mbox{cnf}(\mbox{premise}_{10},\mbox{hypothesis})$

$x_2\ne x_{13}\qquad\mbox{cnf}(\mbox{premise}_{11},\mbox{hypothesis})$

$x_2\ne x_{12}\qquad\mbox{cnf}(\mbox{premise}_{12},\mbox{hypothesis})$

$x_{14}\ne x_{16}\qquad\mbox{cnf}(\mbox{premise}_{13},\mbox{hypothesis})$

$x_1\ne x_6\qquad\mbox{cnf}(\mbox{premise}_{14},\mbox{hypothesis})$

$x_1\ne x_{16}\qquad\mbox{cnf}(\mbox{premise}_{15},\mbox{hypothesis})$

$x_4\ne x_6\qquad\mbox{cnf}(\mbox{premise}_{16},\mbox{hypothesis})$

$x_4\ne x_{15}\qquad\mbox{cnf}(\mbox{premise}_{17},\mbox{hypothesis})$

$x_5\ne x_{14}\qquad\mbox{cnf}(\mbox{premise}_{18},\mbox{hypothesis})$

$\mbox{heap}(\mbox{sep}(\mbox{lseg}(x_{10},x_5),\mbox{sep}(\mbox{lseg}(x_{10},x_9),\mbox{sep}(\mbox{lseg}(x_{13},x_{10}),\mbox{sep}(\mbox{lseg}(x_4,x_{17}),\mbox{sep}(\mbox{lseg}(x_8,x_{12}),\mbox{sep}(\mbox{lseg}(x_{15},x_{12}),\mbox{sep}(\mbox{lseg}(x_{15},x_{17}),\mbox{sep}(\mbox{lseg}(x_{15},x_{13}),\mbox{sep}(\mbox{lseg}(x_{14},x_9),\mbox{sep}(\mbox{lseg}(x_{12},x_7),\mbox{sep}(\mbox{lseg}(x_{12},x_4),\mbox{sep}(\mbox{lseg}(x_2,x_4),\mbox{sep}(\mbox{lseg}(x_7,x_{15}),\mbox{sep}(\mbox{lseg}(x_3,x_{14}),\mbox{sep}(\mbox{lseg}(x_3,x_1),\mbox{sep}(\mbox{lseg}(x_{11},x_3),\mbox{sep}(\mbox{lseg}(x_6,x_{17}),\mbox{emp}))))))))))))))))))\qquad\mbox{cnf}(\mbox{premise}_{19},\mbox{hypothesis})$

$\mbox{heap}(\mbox{emp}) \ \Rightarrow \ x_1 = x_1\qquad\mbox{cnf}(\mbox{conclusion}_1,\mbox{negated\_conjecture})$

\medskip\textbf{SWW433-1.p} Randomly generated entailment of the form F $\to$ $\bot$ (n = 14)

A randomly generated entailment with n program variables.
 Negated equalities and list segments are added at random, with
 specific paramenters so that about half of the generated
 entailments are valid (or, equivalently, F is unsatisfiable).
 Normalization and well-formedness axioms should be enough to
 decide these entailments.




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

$x_6\ne x_7\qquad\mbox{cnf}(\mbox{premise}_1,\mbox{hypothesis})$

$x_1\ne x_8\qquad\mbox{cnf}(\mbox{premise}_2,\mbox{hypothesis})$

$x_1\ne x_{12}\qquad\mbox{cnf}(\mbox{premise}_3,\mbox{hypothesis})$

$x_4\ne x_{10}\qquad\mbox{cnf}(\mbox{premise}_4,\mbox{hypothesis})$

$x_3\ne x_4\qquad\mbox{cnf}(\mbox{premise}_5,\mbox{hypothesis})$

$x_7\ne x_{13}\qquad\mbox{cnf}(\mbox{premise}_6,\mbox{hypothesis})$

$x_{10}\ne x_{11}\qquad\mbox{cnf}(\mbox{premise}_7,\mbox{hypothesis})$

$\mbox{heap}(\mbox{sep}(\mbox{lseg}(x_{14},x_5),\mbox{sep}(\mbox{lseg}(x_{14},x_7),\mbox{sep}(\mbox{lseg}(x_5,x_2),\mbox{sep}(\mbox{lseg}(x_5,x_{12}),\mbox{sep}(\mbox{lseg}(x_5,x_6),\mbox{sep}(\mbox{lseg}(x_9,x_4),\mbox{sep}(\mbox{lseg}(x_9,x_6),\mbox{sep}(\mbox{lseg}(x_{11},x_{13}),\mbox{sep}(\mbox{lseg}(x_1,x_{10}),\mbox{sep}(\mbox{lseg}(x_8,x_7),\mbox{sep}(\mbox{lseg}(x_8,x_3),\mbox{sep}(\mbox{lseg}(x_8,x_4),\mbox{emp})))))))))))))\qquad\mbox{cnf}(\mbox{premise}_8,\mbox{hypothesis})$

$\mbox{heap}(\mbox{emp}) \ \Rightarrow \ x_1 = x_1\qquad\mbox{cnf}(\mbox{conclusion}_1,\mbox{negated\_conjecture})$

\medskip\textbf{SWW397-1.p} Verification Condition generated by Smallfoot

This is one of the verification conditions that were gathered
 from the output of Smallfoot when checking assertions on list
 manipulating programs from its own benchmark suite.




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

$\mbox{nil}\ne x_1\qquad\mbox{cnf}(\mbox{premise}_1,\mbox{hypothesis})$

$\mbox{heap}(\mbox{sep}(\mbox{lseg}(x_2,\mbox{nil}),\mbox{emp}))\qquad\mbox{cnf}(\mbox{premise}_2,\mbox{hypothesis})$

$x_2 = x_2 \ \Rightarrow \ \neg\,\mbox{heap}(\mbox{emp})\qquad\mbox{cnf}(\mbox{conclusion}_1,\mbox{negated\_conjecture})$

\medskip\textbf{SWW463-1.p} Randomly generated entailment of the form F $\to$ G (n = 18)

A randomly generated entailment with n program variables.
 A random graph with pointers and list segments is generated,
 and then some of the segments are folded. The task is to
 prove whether the unfolded version entails the folded one.
 Parameters are chosen so that about half of the generated
 entailments are valid.
 These entailments stress the role of unfolding axioms.




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

$\mbox{heap}(\mbox{sep}(\mbox{lseg}(x_{14},x_{17}),\mbox{sep}(\mbox{next}(x_{17},x_{13}),\mbox{sep}(\mbox{next}(x_1,x_7),\mbox{sep}(\mbox{next}(x_4,x_6),\mbox{sep}(\mbox{next}(x_{10},x_8),\mbox{sep}(\mbox{next}(x_8,x_2),\mbox{sep}(\mbox{lseg}(x_3,x_{17}),\mbox{sep}(\mbox{next}(x_2,x_5),\mbox{sep}(\mbox{next}(x_6,x_{13}),\mbox{sep}(\mbox{next}(x_{16},x_7),\mbox{sep}(\mbox{next}(x_9,x_{12}),\mbox{sep}(\mbox{next}(x_{18},x_{10}),\mbox{sep}(\mbox{lseg}(x_7,x_{14}),\mbox{sep}(\mbox{lseg}(x_{12},x_{14}),\mbox{sep}(\mbox{next}(x_5,x_1),\mbox{sep}(\mbox{next}(x_{13},x_{18}),\mbox{sep}(\mbox{next}(x_{15},x_{11}),\mbox{sep}(\mbox{lseg}(x_{11},x_8),\mbox{emp})))))))))))))))))))\qquad\mbox{cnf}(\mbox{premise}_1,\mbox{hypothesis})$

$\neg\,\mbox{heap}(\mbox{sep}(\mbox{lseg}(x_9,x_{12}),\mbox{sep}(\mbox{lseg}(x_{18},x_{10}),\mbox{sep}(\mbox{lseg}(x_{15},x_8),\mbox{sep}(\mbox{lseg}(x_{16},x_7),\mbox{sep}(\mbox{lseg}(x_4,x_6),\mbox{sep}(\mbox{lseg}(x_{12},x_{14}),\mbox{sep}(\mbox{lseg}(x_3,x_{17}),\mbox{sep}(\mbox{lseg}(x_6,x_{13}),\mbox{sep}(\mbox{lseg}(x_{10},x_{18}),\mbox{emp}))))))))))\qquad\mbox{cnf}(\mbox{conclusion}_1,\mbox{negated\_conjecture})$

\medskip\textbf{SWW422-1.p} Verification Condition generated by Smallfoot

This is one of the verification conditions that were gathered
 from the output of Smallfoot when checking assertions on list
 manipulating programs from its own benchmark suite.




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

$\mbox{nil}\ne x_1\qquad\mbox{cnf}(\mbox{premise}_1,\mbox{hypothesis})$

$x_2\ne x_1\qquad\mbox{cnf}(\mbox{premise}_2,\mbox{hypothesis})$

$x_1\ne x_3\qquad\mbox{cnf}(\mbox{premise}_3,\mbox{hypothesis})$

$\mbox{heap}(\mbox{sep}(\mbox{lseg}(x_2,x_3),\mbox{sep}(\mbox{next}(x_1,x_2),\mbox{emp})))\qquad\mbox{cnf}(\mbox{premise}_4,\mbox{hypothesis})$

$x_3 = x_3 \ \Rightarrow \ \neg\,\mbox{heap}(\mbox{sep}(\mbox{lseg}(x_2,x_3),\mbox{emp}))\qquad\mbox{cnf}(\mbox{conclusion}_1,\mbox{negated\_conjecture})$

\medskip\textbf{SWW432-1.p} Randomly generated entailment of the form F $\to$ $\bot$ (n = 13)

A randomly generated entailment with n program variables.
 Negated equalities and list segments are added at random, with
 specific paramenters so that about half of the generated
 entailments are valid (or, equivalently, F is unsatisfiable).
 Normalization and well-formedness axioms should be enough to
 decide these entailments.




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

$x_1\ne x_4\qquad\mbox{cnf}(\mbox{premise}_1,\mbox{hypothesis})$

$x_4\ne x_6\qquad\mbox{cnf}(\mbox{premise}_2,\mbox{hypothesis})$

$x_7\ne x_{12}\qquad\mbox{cnf}(\mbox{premise}_3,\mbox{hypothesis})$

$x_2\ne x_9\qquad\mbox{cnf}(\mbox{premise}_4,\mbox{hypothesis})$

$x_5\ne x_{13}\qquad\mbox{cnf}(\mbox{premise}_5,\mbox{hypothesis})$

$x_5\ne x_9\qquad\mbox{cnf}(\mbox{premise}_6,\mbox{hypothesis})$

$\mbox{heap}(\mbox{sep}(\mbox{lseg}(x_5,x_9),\mbox{sep}(\mbox{lseg}(x_5,x_1),\mbox{sep}(\mbox{lseg}(x_{13},x_9),\mbox{sep}(\mbox{lseg}(x_8,x_3),\mbox{sep}(\mbox{lseg}(x_3,x_{11}),\mbox{sep}(\mbox{lseg}(x_{11},x_{10}),\mbox{sep}(\mbox{lseg}(x_6,x_3),\mbox{emp}))))))))\qquad\mbox{cnf}(\mbox{premise}_7,\mbox{hypothesis})$

$\mbox{heap}(\mbox{emp}) \ \Rightarrow \ x_1 = x_1\qquad\mbox{cnf}(\mbox{conclusion}_1,\mbox{negated\_conjecture})$

\medskip\textbf{SWW425-1.p} Randomly generated entailment of the form F $\to$ $\bot$ (n = 10)

A randomly generated entailment with n program variables.
 Negated equalities and list segments are added at random, with
 specific paramenters so that about half of the generated
 entailments are valid (or, equivalently, F is unsatisfiable).
 Normalization and well-formedness axioms should be enough to
 decide these entailments.




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

$x_1\ne x_6\qquad\mbox{cnf}(\mbox{premise}_1,\mbox{hypothesis})$

$x_1\ne x_7\qquad\mbox{cnf}(\mbox{premise}_2,\mbox{hypothesis})$

$x_1\ne x_{10}\qquad\mbox{cnf}(\mbox{premise}_3,\mbox{hypothesis})$

$x_4\ne x_8\qquad\mbox{cnf}(\mbox{premise}_4,\mbox{hypothesis})$

$x_4\ne x_7\qquad\mbox{cnf}(\mbox{premise}_5,\mbox{hypothesis})$

$x_4\ne x_9\qquad\mbox{cnf}(\mbox{premise}_6,\mbox{hypothesis})$

$x_3\ne x_8\qquad\mbox{cnf}(\mbox{premise}_7,\mbox{hypothesis})$

$x_7\ne x_{10}\qquad\mbox{cnf}(\mbox{premise}_8,\mbox{hypothesis})$

$x_2\ne x_6\qquad\mbox{cnf}(\mbox{premise}_9,\mbox{hypothesis})$

$x_2\ne x_3\qquad\mbox{cnf}(\mbox{premise}_{10},\mbox{hypothesis})$

$x_2\ne x_7\qquad\mbox{cnf}(\mbox{premise}_{11},\mbox{hypothesis})$

$\mbox{heap}(\mbox{sep}(\mbox{lseg}(x_5,x_7),\mbox{sep}(\mbox{lseg}(x_2,x_5),\mbox{sep}(\mbox{lseg}(x_2,x_{10}),\mbox{sep}(\mbox{lseg}(x_2,x_1),\mbox{sep}(\mbox{lseg}(x_9,x_1),\mbox{sep}(\mbox{lseg}(x_7,x_6),\mbox{sep}(\mbox{lseg}(x_3,x_{10}),\mbox{sep}(\mbox{lseg}(x_6,x_9),\mbox{emp})))))))))\qquad\mbox{cnf}(\mbox{premise}_{12},\mbox{hypothesis})$

$\mbox{heap}(\mbox{emp}) \ \Rightarrow \ x_1 = x_1\qquad\mbox{cnf}(\mbox{conclusion}_1,\mbox{negated\_conjecture})$

\medskip\textbf{SWW451-1.p} Randomly generated entailment of the form F $\to$ G (n = 12)

A randomly generated entailment with n program variables.
 A random graph with pointers and list segments is generated,
 and then some of the segments are folded. The task is to
 prove whether the unfolded version entails the folded one.
 Parameters are chosen so that about half of the generated
 entailments are valid.
 These entailments stress the role of unfolding axioms.




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

$\mbox{heap}(\mbox{sep}(\mbox{next}(x_{10},x_6),\mbox{sep}(\mbox{next}(x_2,x_1),\mbox{sep}(\mbox{next}(x_8,x_5),\mbox{sep}(\mbox{next}(x_4,x_7),\mbox{sep}(\mbox{next}(x_1,x_6),\mbox{sep}(\mbox{next}(x_9,x_3),\mbox{sep}(\mbox{next}(x_6,x_4),\mbox{sep}(\mbox{lseg}(x_{12},x_8),\mbox{sep}(\mbox{next}(x_5,x_1),\mbox{sep}(\mbox{next}(x_7,x_6),\mbox{sep}(\mbox{next}(x_3,x_5),\mbox{sep}(\mbox{lseg}(x_{11},x_8),\mbox{emp})))))))))))))\qquad\mbox{cnf}(\mbox{premise}_1,\mbox{hypothesis})$

$\neg\,\mbox{heap}(\mbox{sep}(\mbox{lseg}(x_{10},x_6),\mbox{sep}(\mbox{lseg}(x_{12},x_8),\mbox{sep}(\mbox{lseg}(x_{11},x_5),\mbox{sep}(\mbox{lseg}(x_9,x_5),\mbox{sep}(\mbox{lseg}(x_5,x_1),\mbox{sep}(\mbox{lseg}(x_2,x_4),\mbox{sep}(\mbox{lseg}(x_4,x_6),\mbox{emp}))))))))\qquad\mbox{cnf}(\mbox{conclusion}_1,\mbox{negated\_conjecture})$

\medskip\textbf{SWW444-1.p} Randomly generated entailment of the form F $\to$ $\bot$ (n = 19)

A randomly generated entailment with n program variables.
 Negated equalities and list segments are added at random, with
 specific paramenters so that about half of the generated
 entailments are valid (or, equivalently, F is unsatisfiable).
 Normalization and well-formedness axioms should be enough to
 decide these entailments.




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

$x_6\ne x_{10}\qquad\mbox{cnf}(\mbox{premise}_1,\mbox{hypothesis})$

$x_6\ne x_{15}\qquad\mbox{cnf}(\mbox{premise}_2,\mbox{hypothesis})$

$x_{11}\ne x_{17}\qquad\mbox{cnf}(\mbox{premise}_3,\mbox{hypothesis})$

$x_3\ne x_{11}\qquad\mbox{cnf}(\mbox{premise}_4,\mbox{hypothesis})$

$x_3\ne x_4\qquad\mbox{cnf}(\mbox{premise}_5,\mbox{hypothesis})$

$x_3\ne x_{18}\qquad\mbox{cnf}(\mbox{premise}_6,\mbox{hypothesis})$

$x_7\ne x_{16}\qquad\mbox{cnf}(\mbox{premise}_7,\mbox{hypothesis})$

$x_{12}\ne x_{19}\qquad\mbox{cnf}(\mbox{premise}_8,\mbox{hypothesis})$

$x_{17}\ne x_{18}\qquad\mbox{cnf}(\mbox{premise}_9,\mbox{hypothesis})$

$x_2\ne x_6\qquad\mbox{cnf}(\mbox{premise}_{10},\mbox{hypothesis})$

$x_2\ne x_4\qquad\mbox{cnf}(\mbox{premise}_{11},\mbox{hypothesis})$

$x_2\ne x_{10}\qquad\mbox{cnf}(\mbox{premise}_{12},\mbox{hypothesis})$

$x_2\ne x_{17}\qquad\mbox{cnf}(\mbox{premise}_{13},\mbox{hypothesis})$

$x_{15}\ne x_{19}\qquad\mbox{cnf}(\mbox{premise}_{14},\mbox{hypothesis})$

$x_8\ne x_{11}\qquad\mbox{cnf}(\mbox{premise}_{15},\mbox{hypothesis})$

$x_8\ne x_9\qquad\mbox{cnf}(\mbox{premise}_{16},\mbox{hypothesis})$

$x_8\ne x_{12}\qquad\mbox{cnf}(\mbox{premise}_{17},\mbox{hypothesis})$

$x_8\ne x_{14}\qquad\mbox{cnf}(\mbox{premise}_{18},\mbox{hypothesis})$

$x_1\ne x_8\qquad\mbox{cnf}(\mbox{premise}_{19},\mbox{hypothesis})$

$x_1\ne x_{13}\qquad\mbox{cnf}(\mbox{premise}_{20},\mbox{hypothesis})$

$x_{13}\ne x_{17}\qquad\mbox{cnf}(\mbox{premise}_{21},\mbox{hypothesis})$

$x_{16}\ne x_{19}\qquad\mbox{cnf}(\mbox{premise}_{22},\mbox{hypothesis})$

$x_5\ne x_{11}\qquad\mbox{cnf}(\mbox{premise}_{23},\mbox{hypothesis})$

$x_5\ne x_{14}\qquad\mbox{cnf}(\mbox{premise}_{24},\mbox{hypothesis})$

$\mbox{heap}(\mbox{sep}(\mbox{lseg}(x_5,x_2),\mbox{sep}(\mbox{lseg}(x_5,x_8),\mbox{sep}(\mbox{lseg}(x_{19},x_{14}),\mbox{sep}(\mbox{lseg}(x_{19},x_9),\mbox{sep}(\mbox{lseg}(x_{10},x_9),\mbox{sep}(\mbox{lseg}(x_{10},x_{18}),\mbox{sep}(\mbox{lseg}(x_{18},x_{10}),\mbox{sep}(\mbox{lseg}(x_{18},x_7),\mbox{sep}(\mbox{lseg}(x_{15},x_{17}),\mbox{sep}(\mbox{lseg}(x_{15},x_9),\mbox{sep}(\mbox{lseg}(x_{15},x_1),\mbox{sep}(\mbox{lseg}(x_{12},x_1),\mbox{sep}(\mbox{lseg}(x_{12},x_6),\mbox{sep}(\mbox{lseg}(x_{17},x_6),\mbox{sep}(\mbox{lseg}(x_2,x_3),\mbox{sep}(\mbox{lseg}(x_9,x_{16}),\mbox{sep}(\mbox{lseg}(x_3,x_{15}),\mbox{emp}))))))))))))))))))\qquad\mbox{cnf}(\mbox{premise}_{25},\mbox{hypothesis})$

$\mbox{heap}(\mbox{emp}) \ \Rightarrow \ x_1 = x_1\qquad\mbox{cnf}(\mbox{conclusion}_1,\mbox{negated\_conjecture})$

\medskip\textbf{SWW453-1.p} Randomly generated entailment of the form F $\to$ G (n = 13)

A randomly generated entailment with n program variables.
 A random graph with pointers and list segments is generated,
 and then some of the segments are folded. The task is to
 prove whether the unfolded version entails the folded one.
 Parameters are chosen so that about half of the generated
 entailments are valid.
 These entailments stress the role of unfolding axioms.




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

$\mbox{heap}(\mbox{sep}(\mbox{next}(x_2,x_6),\mbox{sep}(\mbox{next}(x_4,x_1),\mbox{sep}(\mbox{next}(x_{11},x_8),\mbox{sep}(\mbox{lseg}(x_1,x_3),\mbox{sep}(\mbox{next}(x_{13},x_6),\mbox{sep}(\mbox{next}(x_8,x_6),\mbox{sep}(\mbox{next}(x_3,x_7),\mbox{sep}(\mbox{next}(x_7,x_3),\mbox{sep}(\mbox{next}(x_6,x_2),\mbox{sep}(\mbox{lseg}(x_{12},x_7),\mbox{sep}(\mbox{lseg}(x_{10},x_{11}),\mbox{sep}(\mbox{next}(x_9,x_2),\mbox{sep}(\mbox{lseg}(x_5,x_{11}),\mbox{emp}))))))))))))))\qquad\mbox{cnf}(\mbox{premise}_1,\mbox{hypothesis})$

$\neg\,\mbox{heap}(\mbox{sep}(\mbox{lseg}(x_4,x_1),\mbox{sep}(\mbox{lseg}(x_9,x_6),\mbox{sep}(\mbox{lseg}(x_5,x_{11}),\mbox{sep}(\mbox{lseg}(x_{12},x_3),\mbox{sep}(\mbox{lseg}(x_{13},x_6),\mbox{sep}(\mbox{lseg}(x_{10},x_{11}),\mbox{sep}(\mbox{lseg}(x_1,x_7),\mbox{sep}(\mbox{lseg}(x_{11},x_2),\mbox{emp})))))))))\qquad\mbox{cnf}(\mbox{conclusion}_1,\mbox{negated\_conjecture})$

\medskip\textbf{SWW434-1.p} Randomly generated entailment of the form F $\to$ $\bot$ (n = 14)

A randomly generated entailment with n program variables.
 Negated equalities and list segments are added at random, with
 specific paramenters so that about half of the generated
 entailments are valid (or, equivalently, F is unsatisfiable).
 Normalization and well-formedness axioms should be enough to
 decide these entailments.




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

$x_6\ne x_{14}\qquad\mbox{cnf}(\mbox{premise}_1,\mbox{hypothesis})$

$x_8\ne x_{10}\qquad\mbox{cnf}(\mbox{premise}_2,\mbox{hypothesis})$

$x_4\ne x_8\qquad\mbox{cnf}(\mbox{premise}_3,\mbox{hypothesis})$

$x_4\ne x_7\qquad\mbox{cnf}(\mbox{premise}_4,\mbox{hypothesis})$

$x_3\ne x_5\qquad\mbox{cnf}(\mbox{premise}_5,\mbox{hypothesis})$

$x_9\ne x_{14}\qquad\mbox{cnf}(\mbox{premise}_6,\mbox{hypothesis})$

$x_{13}\ne x_{14}\qquad\mbox{cnf}(\mbox{premise}_7,\mbox{hypothesis})$

$\mbox{heap}(\mbox{sep}(\mbox{lseg}(x_5,x_{10}),\mbox{sep}(\mbox{lseg}(x_{13},x_{12}),\mbox{sep}(\mbox{lseg}(x_1,x_7),\mbox{sep}(\mbox{lseg}(x_8,x_{14}),\mbox{sep}(\mbox{lseg}(x_{12},x_8),\mbox{sep}(\mbox{lseg}(x_2,x_{12}),\mbox{sep}(\mbox{lseg}(x_2,x_{11}),\mbox{sep}(\mbox{lseg}(x_9,x_{14}),\mbox{sep}(\mbox{lseg}(x_9,x_1),\mbox{sep}(\mbox{lseg}(x_3,x_9),\mbox{sep}(\mbox{lseg}(x_{11},x_{13}),\mbox{sep}(\mbox{lseg}(x_{11},x_3),\mbox{emp})))))))))))))\qquad\mbox{cnf}(\mbox{premise}_8,\mbox{hypothesis})$

$\mbox{heap}(\mbox{emp}) \ \Rightarrow \ x_1 = x_1\qquad\mbox{cnf}(\mbox{conclusion}_1,\mbox{negated\_conjecture})$

\medskip\textbf{SWW100+1.p} If only one element non-Boolean, then exists1(P) = exists2(P)






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

$\forall p{:}\;( \forall x_1,x_2{:}\;( ( \neg\,\mbox{bool}(\mbox{apply}(p,x_1))\mbox{ and }\neg\,\mbox{bool}(\mbox{apply}(p,x_2)) ) \ \Rightarrow \ \mbox{apply}(p,x_1) = \mbox{apply}(p,x_2) ) \ \Rightarrow \ \mbox{exists}_1(p) = \mbox{exists}_2(p) )\qquad\mbox{fof}(\mbox{exists1\_exists}_2,\mbox{conjecture})$

\medskip\textbf{SWW456-1.p} Randomly generated entailment of the form F $\to$ G (n = 14)

A randomly generated entailment with n program variables.
 A random graph with pointers and list segments is generated,
 and then some of the segments are folded. The task is to
 prove whether the unfolded version entails the folded one.
 Parameters are chosen so that about half of the generated
 entailments are valid.
 These entailments stress the role of unfolding axioms.




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

$\mbox{heap}(\mbox{sep}(\mbox{next}(x_{11},x_8),\mbox{sep}(\mbox{next}(x_5,x_{13}),\mbox{sep}(\mbox{next}(x_{10},x_5),\mbox{sep}(\mbox{next}(x_9,x_7),\mbox{sep}(\mbox{next}(x_7,x_3),\mbox{sep}(\mbox{next}(x_3,x_{10}),\mbox{sep}(\mbox{next}(x_{12},x_3),\mbox{sep}(\mbox{next}(x_{13},x_9),\mbox{sep}(\mbox{next}(x_6,x_4),\mbox{sep}(\mbox{lseg}(x_2,x_5),\mbox{sep}(\mbox{next}(x_{14},x_{12}),\mbox{sep}(\mbox{next}(x_1,x_3),\mbox{sep}(\mbox{next}(x_8,x_{13}),\mbox{sep}(\mbox{lseg}(x_4,x_{12}),\mbox{emp})))))))))))))))\qquad\mbox{cnf}(\mbox{premise}_1,\mbox{hypothesis})$

$\neg\,\mbox{heap}(\mbox{sep}(\mbox{lseg}(x_1,x_3),\mbox{sep}(\mbox{lseg}(x_2,x_5),\mbox{sep}(\mbox{lseg}(x_{14},x_{12}),\mbox{sep}(\mbox{lseg}(x_5,x_{13}),\mbox{sep}(\mbox{lseg}(x_6,x_3),\mbox{sep}(\mbox{lseg}(x_{11},x_8),\mbox{sep}(\mbox{lseg}(x_8,x_5),\mbox{emp}))))))))\qquad\mbox{cnf}(\mbox{conclusion}_1,\mbox{negated\_conjecture})$

\medskip\textbf{SWW415-1.p} Verification Condition generated by Smallfoot

This is one of the verification conditions that were gathered
 from the output of Smallfoot when checking assertions on list
 manipulating programs from its own benchmark suite.




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

$\mbox{nil}\ne x_1\qquad\mbox{cnf}(\mbox{premise}_1,\mbox{hypothesis})$

$x_1\ne x_2\qquad\mbox{cnf}(\mbox{premise}_2,\mbox{hypothesis})$

$\mbox{heap}(\mbox{sep}(\mbox{lseg}(x_3,\mbox{nil}),\mbox{emp}))\qquad\mbox{cnf}(\mbox{premise}_3,\mbox{hypothesis})$

$x_3 = x_3 \ \Rightarrow \ \neg\,\mbox{heap}(\mbox{emp})\qquad\mbox{cnf}(\mbox{conclusion}_1,\mbox{negated\_conjecture})$

\medskip\textbf{SWW399-1.p} Verification Condition generated by Smallfoot

This is one of the verification conditions that were gathered
 from the output of Smallfoot when checking assertions on list
 manipulating programs from its own benchmark suite.




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

$\mbox{nil}\ne x_1\qquad\mbox{cnf}(\mbox{premise}_1,\mbox{hypothesis})$

$\mbox{heap}(\mbox{sep}(\mbox{next}(x_1,\mbox{nil}),\mbox{emp}))\qquad\mbox{cnf}(\mbox{premise}_2,\mbox{hypothesis})$

$\neg\,\mbox{heap}(\mbox{sep}(\mbox{lseg}(x_1,\mbox{nil}),\mbox{emp}))\qquad\mbox{cnf}(\mbox{conclusion}_1,\mbox{negated\_conjecture})$

\medskip\textbf{SWW466-1.p} Randomly generated entailment of the form F $\to$ G (n = 19)

A randomly generated entailment with n program variables.
 A random graph with pointers and list segments is generated,
 and then some of the segments are folded. The task is to
 prove whether the unfolded version entails the folded one.
 Parameters are chosen so that about half of the generated
 entailments are valid.
 These entailments stress the role of unfolding axioms.




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

$\mbox{heap}(\mbox{sep}(\mbox{lseg}(x_6,x_{13}),\mbox{sep}(\mbox{next}(x_8,x_1),\mbox{sep}(\mbox{next}(x_7,x_{16}),\mbox{sep}(\mbox{next}(x_{17},x_1),\mbox{sep}(\mbox{lseg}(x_{11},x_{19}),\mbox{sep}(\mbox{next}(x_{16},x_{11}),\mbox{sep}(\mbox{next}(x_2,x_5),\mbox{sep}(\mbox{next}(x_{15},x_7),\mbox{sep}(\mbox{lseg}(x_5,x_{19}),\mbox{sep}(\mbox{lseg}(x_{19},x_{12}),\mbox{sep}(\mbox{next}(x_9,x_{14}),\mbox{sep}(\mbox{next}(x_{18},x_{11}),\mbox{sep}(\mbox{lseg}(x_4,x_{16}),\mbox{sep}(\mbox{next}(x_{13},x_2),\mbox{sep}(\mbox{next}(x_{14},x_{10}),\mbox{sep}(\mbox{next}(x_3,x_{17}),\mbox{sep}(\mbox{next}(x_{10},x_5),\mbox{sep}(\mbox{next}(x_{12},x_{14}),\mbox{sep}(\mbox{next}(x_1,x_5),\mbox{emp}))))))))))))))))))))\qquad\mbox{cnf}(\mbox{premise}_1,\mbox{hypothesis})$

$\neg\,\mbox{heap}(\mbox{sep}(\mbox{lseg}(x_8,x_1),\mbox{sep}(\mbox{lseg}(x_9,x_{14}),\mbox{sep}(\mbox{lseg}(x_6,x_2),\mbox{sep}(\mbox{lseg}(x_2,x_5),\mbox{sep}(\mbox{lseg}(x_3,x_{17}),\mbox{sep}(\mbox{lseg}(x_{17},x_5),\mbox{sep}(\mbox{lseg}(x_{15},x_{16}),\mbox{sep}(\mbox{lseg}(x_4,x_{16}),\mbox{sep}(\mbox{lseg}(x_{16},x_{11}),\mbox{sep}(\mbox{lseg}(x_{18},x_{19}),\mbox{sep}(\mbox{lseg}(x_{19},x_{12}),\mbox{sep}(\mbox{lseg}(x_{12},x_{19}),\mbox{emp})))))))))))))\qquad\mbox{cnf}(\mbox{conclusion}_1,\mbox{negated\_conjecture})$

\medskip\textbf{SWW450-1.p} Randomly generated entailment of the form F $\to$ G (n = 11)

A randomly generated entailment with n program variables.
 A random graph with pointers and list segments is generated,
 and then some of the segments are folded. The task is to
 prove whether the unfolded version entails the folded one.
 Parameters are chosen so that about half of the generated
 entailments are valid.
 These entailments stress the role of unfolding axioms.




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

$\mbox{heap}(\mbox{sep}(\mbox{next}(x_7,x_1),\mbox{sep}(\mbox{next}(x_{11},x_7),\mbox{sep}(\mbox{next}(x_9,x_8),\mbox{sep}(\mbox{lseg}(x_4,x_9),\mbox{sep}(\mbox{next}(x_8,x_5),\mbox{sep}(\mbox{next}(x_1,x_4),\mbox{sep}(\mbox{lseg}(x_{10},x_2),\mbox{sep}(\mbox{next}(x_5,x_6),\mbox{sep}(\mbox{lseg}(x_3,x_2),\mbox{sep}(\mbox{next}(x_6,x_5),\mbox{sep}(\mbox{next}(x_2,x_6),\mbox{emp}))))))))))))\qquad\mbox{cnf}(\mbox{premise}_1,\mbox{hypothesis})$

$\neg\,\mbox{heap}(\mbox{sep}(\mbox{lseg}(x_{11},x_7),\mbox{sep}(\mbox{lseg}(x_7,x_9),\mbox{sep}(\mbox{lseg}(x_9,x_5),\mbox{sep}(\mbox{lseg}(x_3,x_2),\mbox{sep}(\mbox{lseg}(x_5,x_6),\mbox{sep}(\mbox{lseg}(x_{10},x_5),\mbox{emp})))))))\qquad\mbox{cnf}(\mbox{conclusion}_1,\mbox{negated\_conjecture})$

\medskip\textbf{SWW459-1.p} Randomly generated entailment of the form F $\to$ G (n = 16)

A randomly generated entailment with n program variables.
 A random graph with pointers and list segments is generated,
 and then some of the segments are folded. The task is to
 prove whether the unfolded version entails the folded one.
 Parameters are chosen so that about half of the generated
 entailments are valid.
 These entailments stress the role of unfolding axioms.




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

$\mbox{heap}(\mbox{sep}(\mbox{lseg}(x_2,x_{12}),\mbox{sep}(\mbox{lseg}(x_{10},x_5),\mbox{sep}(\mbox{next}(x_{14},x_3),\mbox{sep}(\mbox{next}(x_1,x_{11}),\mbox{sep}(\mbox{next}(x_9,x_7),\mbox{sep}(\mbox{next}(x_{16},x_{10}),\mbox{sep}(\mbox{next}(x_8,x_9),\mbox{sep}(\mbox{next}(x_{13},x_2),\mbox{sep}(\mbox{next}(x_4,x_3),\mbox{sep}(\mbox{next}(x_{11},x_8),\mbox{sep}(\mbox{next}(x_6,x_{16}),\mbox{sep}(\mbox{lseg}(x_{12},x_{16}),\mbox{sep}(\mbox{next}(x_5,x_1),\mbox{sep}(\mbox{next}(x_3,x_{10}),\mbox{sep}(\mbox{next}(x_7,x_1),\mbox{sep}(\mbox{lseg}(x_{15},x_{12}),\mbox{emp})))))))))))))))))\qquad\mbox{cnf}(\mbox{premise}_1,\mbox{hypothesis})$

$\neg\,\mbox{heap}(\mbox{sep}(\mbox{lseg}(x_9,x_7),\mbox{sep}(\mbox{lseg}(x_6,x_{16}),\mbox{sep}(\mbox{lseg}(x_{14},x_3),\mbox{sep}(\mbox{lseg}(x_4,x_3),\mbox{sep}(\mbox{lseg}(x_{13},x_{12}),\mbox{sep}(\mbox{lseg}(x_{15},x_{12}),\mbox{sep}(\mbox{lseg}(x_{12},x_{16}),\mbox{sep}(\mbox{lseg}(x_3,x_{10}),\mbox{sep}(\mbox{lseg}(x_{16},x_1),\mbox{sep}(\mbox{lseg}(x_7,x_9),\mbox{emp})))))))))))\qquad\mbox{cnf}(\mbox{conclusion}_1,\mbox{negated\_conjecture})$

\medskip\textbf{SWW406-1.p} Verification Condition generated by Smallfoot

This is one of the verification conditions that were gathered
 from the output of Smallfoot when checking assertions on list
 manipulating programs from its own benchmark suite.




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

$\mbox{nil}\ne x_1\qquad\mbox{cnf}(\mbox{premise}_1,\mbox{hypothesis})$

$\mbox{nil}\ne x_2\qquad\mbox{cnf}(\mbox{premise}_2,\mbox{hypothesis})$

$\mbox{nil}\ne x_3\qquad\mbox{cnf}(\mbox{premise}_3,\mbox{hypothesis})$

$x_1\ne x_3\qquad\mbox{cnf}(\mbox{premise}_4,\mbox{hypothesis})$

$x_2\ne x_3\qquad\mbox{cnf}(\mbox{premise}_5,\mbox{hypothesis})$

$\mbox{heap}(\mbox{sep}(\mbox{lseg}(x_2,x_1),\mbox{sep}(\mbox{next}(x_3,x_2),\mbox{sep}(\mbox{next}(x_1,x_3),\mbox{emp}))))\qquad\mbox{cnf}(\mbox{premise}_6,\mbox{hypothesis})$

$\neg\,\mbox{heap}(\mbox{sep}(\mbox{next}(x_4,x_3),\mbox{sep}(\mbox{lseg}(x_2,x_4),\mbox{sep}(\mbox{next}(x_3,x_2),\mbox{emp}))))\qquad\mbox{cnf}(\mbox{conclusion}_1,\mbox{negated\_conjecture})$

\medskip\textbf{SWW423-1.p} Verification Condition generated by Smallfoot

This is one of the verification conditions that were gathered
 from the output of Smallfoot when checking assertions on list
 manipulating programs from its own benchmark suite.




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

$\mbox{nil}\ne x_1\qquad\mbox{cnf}(\mbox{premise}_1,\mbox{hypothesis})$

$x_2\ne x_1\qquad\mbox{cnf}(\mbox{premise}_2,\mbox{hypothesis})$

$x_1\ne x_3\qquad\mbox{cnf}(\mbox{premise}_3,\mbox{hypothesis})$

$\mbox{heap}(\mbox{sep}(\mbox{lseg}(x_2,\mbox{nil}),\mbox{sep}(\mbox{lseg}(x_3,\mbox{nil}),\mbox{sep}(\mbox{next}(x_1,x_2),\mbox{emp}))))\qquad\mbox{cnf}(\mbox{premise}_4,\mbox{hypothesis})$

$\neg\,\mbox{heap}(\mbox{sep}(\mbox{lseg}(x_1,\mbox{nil}),\mbox{sep}(\mbox{lseg}(x_3,\mbox{nil}),\mbox{emp})))\qquad\mbox{cnf}(\mbox{conclusion}_1,\mbox{negated\_conjecture})$

\medskip\textbf{SWW404-1.p} Verification Condition generated by Smallfoot

This is one of the verification conditions that were gathered
 from the output of Smallfoot when checking assertions on list
 manipulating programs from its own benchmark suite.




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

$\mbox{nil}\ne x_1\qquad\mbox{cnf}(\mbox{premise}_1,\mbox{hypothesis})$

$\mbox{nil}\ne x_2\qquad\mbox{cnf}(\mbox{premise}_2,\mbox{hypothesis})$

$\mbox{nil}\ne x_3\qquad\mbox{cnf}(\mbox{premise}_3,\mbox{hypothesis})$

$x_1\ne x_2\qquad\mbox{cnf}(\mbox{premise}_4,\mbox{hypothesis})$

$x_1\ne x_3\qquad\mbox{cnf}(\mbox{premise}_5,\mbox{hypothesis})$

$\mbox{heap}(\mbox{sep}(\mbox{lseg}(x_2,x_3),\mbox{sep}(\mbox{next}(x_1,x_2),\mbox{sep}(\mbox{next}(x_3,x_1),\mbox{emp}))))\qquad\mbox{cnf}(\mbox{premise}_6,\mbox{hypothesis})$

$\mbox{heap}(\mbox{sep}(\mbox{lseg}(x_4,x_3),\mbox{sep}(\mbox{next}(x_3,x_4),\mbox{emp}))) \ \Rightarrow \ x_4 = x_3\qquad\mbox{cnf}(\mbox{conclusion}_1,\mbox{negated\_conjecture})$

\medskip\textbf{SWW469$\wedge$1.p} Hoare's Logic with Procedures line 112, 100 axioms selected






$\mbox{state}{:}\;\mbox{\$tType}\qquad\mbox{thf}(\mbox{ty\_ty\_tc\_\_Com\_\_Ostate},\mbox{type})$

$\mbox{induct\_false}{:}\;\mbox{\$o}\qquad\mbox{thf}(\mbox{sy\_c\_HOL\_Oinduct\_\_false},\mbox{type})$

$\mbox{induct\_true}{:}\;\mbox{\$o}\qquad\mbox{thf}(\mbox{sy\_c\_HOL\_Oinduct\_\_true},\mbox{type})$

$\mbox{hoare\_1821564147gleton}{:}\;\mbox{\$o}\qquad\mbox{thf}(\mbox{sy\_c\_Hoare\_\_Mirabelle\_\_ghhkfsbqqq\_Ostate\_\_not\_\_singleton},\mbox{type})$

$\mbox{hoare\_1821564147gleton}\iff \exists s{:}\;\mbox{state},t{:}\;\mbox{state}{:}\;s\ne t\qquad\mbox{thf}(\mbox{fact\_0\_state\_\_not\_\_singleton\_\_def},\mbox{axiom})$

$\neg\,\mbox{induct\_false}\qquad\mbox{thf}(\mbox{fact\_1\_induct\_\_false\_\_def},\mbox{axiom})$

$\mbox{induct\_true}\qquad\mbox{thf}(\mbox{fact\_2\_induct\_\_trueI},\mbox{axiom})$

$\mbox{induct\_true}\qquad\mbox{thf}(\mbox{fact\_3\_induct\_\_true\_\_def},\mbox{axiom})$

$\mbox{hoare\_1821564147gleton}\qquad\mbox{thf}(\mbox{conj}_0,\mbox{hypothesis})$

$\forall t{:}\;\mbox{state}{:}\;\neg\,\forall s{:}\;\mbox{state}{:}\;s = t\qquad\mbox{thf}(\mbox{conj}_1,\mbox{conjecture})$

\medskip\textbf{SWW436-1.p} Randomly generated entailment of the form F $\to$ $\bot$ (n = 15)

A randomly generated entailment with n program variables.
 Negated equalities and list segments are added at random, with
 specific paramenters so that about half of the generated
 entailments are valid (or, equivalently, F is unsatisfiable).
 Normalization and well-formedness axioms should be enough to
 decide these entailments.




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

$x_6\ne x_{14}\qquad\mbox{cnf}(\mbox{premise}_1,\mbox{hypothesis})$

$x_3\ne x_6\qquad\mbox{cnf}(\mbox{premise}_2,\mbox{hypothesis})$

$x_3\ne x_{13}\qquad\mbox{cnf}(\mbox{premise}_3,\mbox{hypothesis})$

$x_4\ne x_6\qquad\mbox{cnf}(\mbox{premise}_4,\mbox{hypothesis})$

$x_4\ne x_7\qquad\mbox{cnf}(\mbox{premise}_5,\mbox{hypothesis})$

$x_4\ne x_{12}\qquad\mbox{cnf}(\mbox{premise}_6,\mbox{hypothesis})$

$x_1\ne x_3\qquad\mbox{cnf}(\mbox{premise}_7,\mbox{hypothesis})$

$x_{10}\ne x_{15}\qquad\mbox{cnf}(\mbox{premise}_8,\mbox{hypothesis})$

$\mbox{heap}(\mbox{sep}(\mbox{lseg}(x_{13},x_2),\mbox{sep}(\mbox{lseg}(x_4,x_9),\mbox{sep}(\mbox{lseg}(x_4,x_{13}),\mbox{sep}(\mbox{lseg}(x_1,x_5),\mbox{sep}(\mbox{lseg}(x_1,x_6),\mbox{sep}(\mbox{lseg}(x_8,x_{14}),\mbox{sep}(\mbox{lseg}(x_8,x_{15}),\mbox{sep}(\mbox{lseg}(x_8,x_1),\mbox{sep}(\mbox{lseg}(x_{14},x_8),\mbox{sep}(\mbox{lseg}(x_{15},x_4),\mbox{sep}(\mbox{lseg}(x_2,x_{15}),\mbox{sep}(\mbox{lseg}(x_2,x_9),\mbox{sep}(\mbox{lseg}(x_9,x_7),\mbox{sep}(\mbox{lseg}(x_9,x_6),\mbox{sep}(\mbox{lseg}(x_3,x_{10}),\mbox{sep}(\mbox{lseg}(x_6,x_2),\mbox{emp})))))))))))))))))\qquad\mbox{cnf}(\mbox{premise}_9,\mbox{hypothesis})$

$\mbox{heap}(\mbox{emp}) \ \Rightarrow \ x_1 = x_1\qquad\mbox{cnf}(\mbox{conclusion}_1,\mbox{negated\_conjecture})$

\medskip\textbf{SWW102+1.p} Equivalence of not1 and not2






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

$\forall p{:}\;\mbox{not}_1(p) = \mbox{not}_2(p)\qquad\mbox{fof}(\mbox{not1\_not}_2,\mbox{conjecture})$

\medskip\textbf{SWW412-1.p} Verification Condition generated by Smallfoot

This is one of the verification conditions that were gathered
 from the output of Smallfoot when checking assertions on list
 manipulating programs from its own benchmark suite.




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

$\mbox{nil}\ne x_1\qquad\mbox{cnf}(\mbox{premise}_1,\mbox{hypothesis})$

$\mbox{nil}\ne x_2\qquad\mbox{cnf}(\mbox{premise}_2,\mbox{hypothesis})$

$x_3\ne x_1\qquad\mbox{cnf}(\mbox{premise}_3,\mbox{hypothesis})$

$x_3\ne x_2\qquad\mbox{cnf}(\mbox{premise}_4,\mbox{hypothesis})$

$x_1\ne x_2\qquad\mbox{cnf}(\mbox{premise}_5,\mbox{hypothesis})$

$x_1\ne x_4\qquad\mbox{cnf}(\mbox{premise}_6,\mbox{hypothesis})$

$x_2\ne x_4\qquad\mbox{cnf}(\mbox{premise}_7,\mbox{hypothesis})$

$\mbox{heap}(\mbox{sep}(\mbox{lseg}(x_3,\mbox{nil}),\mbox{sep}(\mbox{lseg}(x_4,\mbox{nil}),\mbox{sep}(\mbox{next}(x_1,x_4),\mbox{sep}(\mbox{next}(x_2,x_3),\mbox{emp})))))\qquad\mbox{cnf}(\mbox{premise}_8,\mbox{hypothesis})$

$\neg\,\mbox{heap}(\mbox{sep}(\mbox{lseg}(x_2,\mbox{nil}),\mbox{sep}(\mbox{lseg}(x_1,\mbox{nil}),\mbox{emp})))\qquad\mbox{cnf}(\mbox{conclusion}_1,\mbox{negated\_conjecture})$

\medskip
\end{document}