Satisfaction of some intuitionistic formulas for various Kripke frames

table.pdf

table.tex

\documentclass[10pt,a4paper]{article}  % -*- coding: utf-8 -*-
%% This file is automatically generated.  Do not edit!
\usepackage[a4paper,margin=1.5cm]{geometry}
\usepackage[utf8]{inputenc}
\usepackage[T1]{fontenc}
\usepackage{lmodern}
\usepackage{newtxtext}
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{pifont}
\usepackage{supertabular}
%\usepackage{adjustbox}
\usepackage{graphicx}
\usepackage[usenames,svgnames]{xcolor}
\newcommand{\sideways}[1]{\rotatebox{90}{#1}}%
\newcommand{\cmark}{\ding{51}}%
\newcommand{\xmark}{\ding{55}}%
\begin{document}
\setlength{\parindent}{0pt}
\textbf{Satisfaction of some intuitionistic formulas for various Kripke frames:}
\par
\begin{supertabular}{l|ccccccccccccccc}
&\sideways{\texttt{basic-1}}
&\sideways{\texttt{basic-2}}
&\sideways{\texttt{basic-3}}
&\sideways{\texttt{basic-4}}
&\sideways{\texttt{basic-5}}
&\sideways{\texttt{skvortsov-1}}
&\sideways{\texttt{skvortsov-2}}
&\sideways{\texttt{skvortsov-3}}
&\sideways{\texttt{skvortsov-4}}
&\sideways{\texttt{skvortsov-5}}
&\sideways{\texttt{skvortsov-6}}
&\sideways{\texttt{skvortsov-7}}
&\sideways{\texttt{skvortsov-8}}
&\sideways{\texttt{skvortsov-9}}
&\sideways{\texttt{skvortsov-10}}
\\\hline
\texttt{lem}
&\textcolor{Green}{\cmark}&\textcolor{DarkRed}{\xmark}&\textcolor{DarkRed}{\xmark}&\textcolor{DarkRed}{\xmark}&\textcolor{DarkRed}{\xmark}&\textcolor{DarkRed}{\xmark}&\textcolor{DarkRed}{\xmark}&\textcolor{DarkRed}{\xmark}&\textcolor{DarkRed}{\xmark}&\textcolor{DarkRed}{\xmark}&\textcolor{DarkRed}{\xmark}&\textcolor{DarkRed}{\xmark}&\textcolor{DarkRed}{\xmark}&\textcolor{DarkRed}{\xmark}&\textcolor{DarkRed}{\xmark}
\\
\texttt{smetanich}
&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{DarkRed}{\xmark}&\textcolor{DarkRed}{\xmark}&\textcolor{DarkRed}{\xmark}&\textcolor{DarkRed}{\xmark}&\textcolor{DarkRed}{\xmark}&\textcolor{DarkRed}{\xmark}&\textcolor{DarkRed}{\xmark}&\textcolor{DarkRed}{\xmark}&\textcolor{DarkRed}{\xmark}&\textcolor{DarkRed}{\xmark}&\textcolor{DarkRed}{\xmark}&\textcolor{DarkRed}{\xmark}&\textcolor{DarkRed}{\xmark}
\\
\texttt{bd2}
&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{DarkRed}{\xmark}&\textcolor{Green}{\cmark}&\textcolor{DarkRed}{\xmark}&\textcolor{DarkRed}{\xmark}&\textcolor{DarkRed}{\xmark}&\textcolor{Green}{\cmark}&\textcolor{DarkRed}{\xmark}&\textcolor{DarkRed}{\xmark}&\textcolor{DarkRed}{\xmark}&\textcolor{DarkRed}{\xmark}&\textcolor{DarkRed}{\xmark}&\textcolor{DarkRed}{\xmark}&\textcolor{DarkRed}{\xmark}
\\
\texttt{goedel-dummett}
&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{DarkRed}{\xmark}&\textcolor{DarkRed}{\xmark}&\textcolor{DarkRed}{\xmark}&\textcolor{DarkRed}{\xmark}&\textcolor{DarkRed}{\xmark}&\textcolor{DarkRed}{\xmark}&\textcolor{DarkRed}{\xmark}&\textcolor{DarkRed}{\xmark}&\textcolor{DarkRed}{\xmark}&\textcolor{DarkRed}{\xmark}&\textcolor{DarkRed}{\xmark}&\textcolor{DarkRed}{\xmark}
\\
\texttt{wlem}
&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{DarkRed}{\xmark}&\textcolor{Green}{\cmark}&\textcolor{DarkRed}{\xmark}&\textcolor{DarkRed}{\xmark}&\textcolor{DarkRed}{\xmark}&\textcolor{DarkRed}{\xmark}&\textcolor{DarkRed}{\xmark}&\textcolor{DarkRed}{\xmark}&\textcolor{DarkRed}{\xmark}&\textcolor{DarkRed}{\xmark}&\textcolor{DarkRed}{\xmark}&\textcolor{DarkRed}{\xmark}
\\
\texttt{bc3}
&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{DarkRed}{\xmark}&\textcolor{DarkRed}{\xmark}&\textcolor{DarkRed}{\xmark}&\textcolor{DarkRed}{\xmark}&\textcolor{DarkRed}{\xmark}&\textcolor{DarkRed}{\xmark}&\textcolor{DarkRed}{\xmark}&\textcolor{DarkRed}{\xmark}&\textcolor{DarkRed}{\xmark}&\textcolor{DarkRed}{\xmark}&\textcolor{DarkRed}{\xmark}
\\
\texttt{scott}
&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{DarkRed}{\xmark}&\textcolor{DarkRed}{\xmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{DarkRed}{\xmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}
\\
\texttt{jankov-r}
&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{DarkRed}{\xmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}
\\
\texttt{bw2}
&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{DarkRed}{\xmark}&\textcolor{DarkRed}{\xmark}&\textcolor{DarkRed}{\xmark}&\textcolor{DarkRed}{\xmark}&\textcolor{DarkRed}{\xmark}&\textcolor{DarkRed}{\xmark}&\textcolor{DarkRed}{\xmark}&\textcolor{DarkRed}{\xmark}
\\
\texttt{kreisel-putnam}
&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{DarkRed}{\xmark}&\textcolor{DarkRed}{\xmark}&\textcolor{DarkRed}{\xmark}&\textcolor{DarkRed}{\xmark}&\textcolor{DarkRed}{\xmark}&\textcolor{DarkRed}{\xmark}&\textcolor{Green}{\cmark}&\textcolor{DarkRed}{\xmark}
\\
\texttt{two-of-three}
&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{DarkRed}{\xmark}&\textcolor{DarkRed}{\xmark}&\textcolor{DarkRed}{\xmark}&\textcolor{DarkRed}{\xmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{DarkRed}{\xmark}&\textcolor{DarkRed}{\xmark}
\\
\texttt{skvortsov}
&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{DarkRed}{\xmark}&\textcolor{DarkRed}{\xmark}&\textcolor{DarkRed}{\xmark}&\textcolor{DarkRed}{\xmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{DarkRed}{\xmark}
\\
\texttt{ceitin-star}
&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{DarkRed}{\xmark}&\textcolor{DarkRed}{\xmark}&\textcolor{DarkRed}{\xmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{DarkRed}{\xmark}&\textcolor{Green}{\cmark}&\textcolor{DarkRed}{\xmark}
\\
\texttt{bb2}
&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{DarkRed}{\xmark}&\textcolor{DarkRed}{\xmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{DarkRed}{\xmark}&\textcolor{DarkRed}{\xmark}&\textcolor{DarkRed}{\xmark}&\textcolor{DarkRed}{\xmark}
\\
\texttt{ceitin}
&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{DarkRed}{\xmark}&\textcolor{Green}{\cmark}&\textcolor{DarkRed}{\xmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{DarkRed}{\xmark}&\textcolor{Green}{\cmark}&\textcolor{DarkRed}{\xmark}
\\
\texttt{plisko-p3}
&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{DarkRed}{\xmark}&\textcolor{Green}{\cmark}&\textcolor{DarkRed}{\xmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{DarkRed}{\xmark}
\\
\texttt{jankov-i3}
&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{DarkRed}{\xmark}&\textcolor{Green}{\cmark}&\textcolor{DarkRed}{\xmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}
\\
\texttt{jankov-k3}
&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{DarkRed}{\xmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}
\\
\texttt{anti-scott}
&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{DarkRed}{\xmark}&\textcolor{Green}{\cmark}&\textcolor{DarkRed}{\xmark}&\textcolor{DarkRed}{\xmark}&\textcolor{DarkRed}{\xmark}&\textcolor{DarkRed}{\xmark}&\textcolor{DarkRed}{\xmark}
\\
\texttt{rose}
&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{DarkRed}{\xmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}
\\
\texttt{plisko-p}
&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{DarkRed}{\xmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{DarkRed}{\xmark}
\\
\texttt{plisko-l}
&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{Green}{\cmark}&\textcolor{DarkRed}{\xmark}&\textcolor{Green}{\cmark}
\\
\end{supertabular}

\vskip 15pt plus 1fil\relax
\textbf{Formulas:}
\par\nobreak
\begin{supertabular}{lp{0.8\textwidth}}
\texttt{lem}
&$p \mskip4mu plus 4mu\relax\relax\lor\penalty0\relax\mskip4mu plus 4mu\relax\relax  \neg p$
\\[1.5pt]
\texttt{smetanich}
&$(\neg q\mskip3mu plus 2mu\relax\relax\Rightarrow\penalty300\relax\mskip3mu plus 2mu\relax\relax p) \mskip5mu plus 4mu\relax\relax\Rightarrow\penalty0\relax\mskip5mu plus 4mu\relax\relax  (((p\Rightarrow\penalty900\relax q)\mskip1mu\relax\Rightarrow\penalty600\relax\mskip1mu\relax p)\mskip3mu plus 2mu\relax\relax\Rightarrow\penalty300\relax\mskip3mu plus 2mu\relax\relax p)$
\\[1.5pt]
\texttt{bd2}
&$p_{2} \mskip4mu plus 4mu\relax\relax\lor\penalty0\relax\mskip4mu plus 4mu\relax\relax  (p_{2} \mskip3mu plus 2mu\relax\relax\Rightarrow\penalty300\relax\mskip3mu plus 2mu\relax\relax  p_{1}\mskip2mu plus 2mu\relax\relax\lor\penalty300\relax\mskip2mu plus 2mu\relax\relax \neg p_{1})$
\\[1.5pt]
\texttt{goedel-dummett}
&$(p_{0} \mskip3mu plus 2mu\relax\relax\Rightarrow\penalty300\relax\mskip3mu plus 2mu\relax\relax  p_{1}) \mskip4mu plus 4mu\relax\relax\lor\penalty0\relax\mskip4mu plus 4mu\relax\relax  (p_{1} \mskip3mu plus 2mu\relax\relax\Rightarrow\penalty300\relax\mskip3mu plus 2mu\relax\relax  p_{0})$
\\[1.5pt]
\texttt{wlem}
&$\neg p \mskip4mu plus 4mu\relax\relax\lor\penalty0\relax\mskip4mu plus 4mu\relax\relax  \neg \neg p$
\\[1.5pt]
\texttt{bc3}
&$p_{0} \mskip4mu plus 4mu\relax\relax\lor\penalty0\relax\mskip4mu plus 4mu\relax\relax  (p_{0} \mskip3mu plus 2mu\relax\relax\Rightarrow\penalty300\relax\mskip3mu plus 2mu\relax\relax  p_{1}) \mskip4mu plus 4mu\relax\relax\lor\penalty0\relax\mskip4mu plus 4mu\relax\relax  (p_{0}\mskip1mu plus 2mu\relax\relax\land\penalty300\relax\mskip1mu plus 2mu\relax\relax p_{1} \mskip3mu plus 2mu\relax\relax\Rightarrow\penalty300\relax\mskip3mu plus 2mu\relax\relax  p_{2}) \mskip4mu plus 4mu\relax\relax\lor\penalty0\relax\mskip4mu plus 4mu\relax\relax  \neg (p_{0}\mskip1mu plus 2mu\relax\relax\land\penalty300\relax\mskip1mu plus 2mu\relax\relax p_{1}\mskip1mu plus 2mu\relax\relax\land\penalty300\relax\mskip1mu plus 2mu\relax\relax p_{2})$
\\[1.5pt]
\texttt{scott}
&$((\neg \neg p\mskip1mu\relax\Rightarrow\penalty600\relax\mskip1mu\relax p) \mskip3mu plus 2mu\relax\relax\Rightarrow\penalty300\relax\mskip3mu plus 2mu\relax\relax  (\neg p\mskip0mu\relax\lor\penalty600\relax\mskip0mu\relax \neg \neg p)) \mskip5mu plus 4mu\relax\relax\Rightarrow\penalty0\relax\mskip5mu plus 4mu\relax\relax  (\neg p\mskip2mu plus 2mu\relax\relax\lor\penalty300\relax\mskip2mu plus 2mu\relax\relax \neg \neg p)$
\\[1.5pt]
\texttt{jankov-r}
&$(\neg (p\land\penalty600\relax q) \mskip1mu plus 2mu\relax\relax\land\penalty300\relax\mskip1mu plus 2mu\relax\relax  \neg (\neg p\land\penalty600\relax \neg q) \mskip1mu plus 2mu\relax\relax\land\penalty300\relax\mskip1mu plus 2mu\relax\relax  ((\neg \neg p\Rightarrow\penalty900\relax p)\mskip1mu\relax\Rightarrow\penalty600\relax\mskip1mu\relax (p\lor\penalty900\relax \neg p)) \mskip1mu plus 2mu\relax\relax\land\penalty300\relax\mskip1mu plus 2mu\relax\relax  ((\neg \neg q\Rightarrow\penalty900\relax q)\mskip1mu\relax\Rightarrow\penalty600\relax\mskip1mu\relax (q\lor\penalty900\relax \neg q))) \mskip5mu plus 4mu\relax\relax\Rightarrow\penalty0\relax\mskip5mu plus 4mu\relax\relax  (\neg p\mskip2mu plus 2mu\relax\relax\lor\penalty300\relax\mskip2mu plus 2mu\relax\relax \neg q)$
\\[1.5pt]
\texttt{bw2}
&$(p_{0} \mskip3mu plus 2mu\relax\relax\Rightarrow\penalty300\relax\mskip3mu plus 2mu\relax\relax  p_{1}\mskip2mu plus 2mu\relax\relax\lor\penalty300\relax\mskip2mu plus 2mu\relax\relax p_{2}) \mskip4mu plus 4mu\relax\relax\lor\penalty0\relax\mskip4mu plus 4mu\relax\relax  (p_{1} \mskip3mu plus 2mu\relax\relax\Rightarrow\penalty300\relax\mskip3mu plus 2mu\relax\relax  p_{0}\mskip2mu plus 2mu\relax\relax\lor\penalty300\relax\mskip2mu plus 2mu\relax\relax p_{2}) \mskip4mu plus 4mu\relax\relax\lor\penalty0\relax\mskip4mu plus 4mu\relax\relax  (p_{2} \mskip3mu plus 2mu\relax\relax\Rightarrow\penalty300\relax\mskip3mu plus 2mu\relax\relax  p_{0}\mskip2mu plus 2mu\relax\relax\lor\penalty300\relax\mskip2mu plus 2mu\relax\relax p_{1})$
\\[1.5pt]
\texttt{kreisel-putnam}
&$(\neg p\mskip3mu plus 2mu\relax\relax\Rightarrow\penalty300\relax\mskip3mu plus 2mu\relax\relax q\mskip2mu plus 2mu\relax\relax\lor\penalty300\relax\mskip2mu plus 2mu\relax\relax r) \mskip5mu plus 4mu\relax\relax\Rightarrow\penalty0\relax\mskip5mu plus 4mu\relax\relax  ((\neg p\mskip1mu\relax\Rightarrow\penalty600\relax\mskip1mu\relax q) \mskip2mu plus 2mu\relax\relax\lor\penalty300\relax\mskip2mu plus 2mu\relax\relax  (\neg p\mskip1mu\relax\Rightarrow\penalty600\relax\mskip1mu\relax r))$
\\[1.5pt]
\texttt{two-of-three}
&$\neg (p_{1}\mskip1mu plus 2mu\relax\relax\land\penalty300\relax\mskip1mu plus 2mu\relax\relax p_{2}\mskip1mu plus 2mu\relax\relax\land\penalty300\relax\mskip1mu plus 2mu\relax\relax p_{3}) \mskip5mu plus 4mu\relax\relax\Rightarrow\penalty0\relax\mskip5mu plus 4mu\relax\relax  \neg (p_{2}\mskip1mu plus 2mu\relax\relax\land\penalty300\relax\mskip1mu plus 2mu\relax\relax p_{3}) \mskip4mu plus 4mu\relax\relax\lor\penalty0\relax\mskip4mu plus 4mu\relax\relax  \neg (p_{1}\mskip1mu plus 2mu\relax\relax\land\penalty300\relax\mskip1mu plus 2mu\relax\relax p_{3}) \mskip4mu plus 4mu\relax\relax\lor\penalty0\relax\mskip4mu plus 4mu\relax\relax  \neg (p_{1}\mskip1mu plus 2mu\relax\relax\land\penalty300\relax\mskip1mu plus 2mu\relax\relax p_{2})$
\\[1.5pt]
\texttt{skvortsov}
&$(\neg (p_{1}\land\penalty600\relax p_{2}) \mskip3mu plus 2mu\relax\relax\Rightarrow\penalty300\relax\mskip3mu plus 2mu\relax\relax  \neg (\neg p_{1}\land\penalty600\relax p_{2})\mskip2mu plus 2mu\relax\relax\lor\penalty300\relax\mskip2mu plus 2mu\relax\relax \neg (p_{1}\land\penalty600\relax \neg p_{2})) \mskip5mu plus 4mu\relax\relax\Rightarrow\penalty0\relax\mskip5mu plus 4mu\relax\relax  (\neg (\neg p_{1}\land\penalty600\relax p_{2})\mskip2mu plus 2mu\relax\relax\lor\penalty300\relax\mskip2mu plus 2mu\relax\relax \neg (p_{1}\land\penalty600\relax \neg p_{2}))$
\\[1.5pt]
\texttt{ceitin-star}
&$(\neg (p_{1}\land\penalty600\relax p_{2}) \mskip1mu plus 2mu\relax\relax\land\penalty300\relax\mskip1mu plus 2mu\relax\relax  (\neg p_{1}\mskip1mu\relax\Rightarrow\penalty600\relax\mskip1mu\relax (q_{1}\lor\penalty900\relax r)) \mskip1mu plus 2mu\relax\relax\land\penalty300\relax\mskip1mu plus 2mu\relax\relax  (\neg p_{2}\mskip1mu\relax\Rightarrow\penalty600\relax\mskip1mu\relax (q_{2}\lor\penalty900\relax r))) \mskip5mu plus 4mu\relax\relax\Rightarrow\penalty0\relax\mskip5mu plus 4mu\relax\relax  ((\neg p_{1}\mskip1mu\relax\Rightarrow\penalty600\relax\mskip1mu\relax q_{1}) \mskip2mu plus 2mu\relax\relax\lor\penalty300\relax\mskip2mu plus 2mu\relax\relax  (\neg p_{1}\mskip1mu\relax\Rightarrow\penalty600\relax\mskip1mu\relax r) \mskip2mu plus 2mu\relax\relax\lor\penalty300\relax\mskip2mu plus 2mu\relax\relax  (\neg p_{2}\mskip1mu\relax\Rightarrow\penalty600\relax\mskip1mu\relax q_{2}) \mskip2mu plus 2mu\relax\relax\lor\penalty300\relax\mskip2mu plus 2mu\relax\relax  (\neg p_{2}\mskip1mu\relax\Rightarrow\penalty600\relax\mskip1mu\relax r))$
\\[1.5pt]
\texttt{bb2}
&$((p_{0}\mskip1mu\relax\Rightarrow\penalty600\relax\mskip1mu\relax (p_{1}\lor\penalty900\relax p_{2}))\mskip3mu plus 2mu\relax\relax\Rightarrow\penalty300\relax\mskip3mu plus 2mu\relax\relax (p_{1}\mskip0mu\relax\lor\penalty600\relax\mskip0mu\relax p_{2})) \mskip3mu plus 4mu\relax\relax\land\penalty0\relax\mskip3mu plus 4mu\relax\relax  ((p_{1}\mskip1mu\relax\Rightarrow\penalty600\relax\mskip1mu\relax (p_{0}\lor\penalty900\relax p_{2}))\mskip3mu plus 2mu\relax\relax\Rightarrow\penalty300\relax\mskip3mu plus 2mu\relax\relax (p_{0}\mskip0mu\relax\lor\penalty600\relax\mskip0mu\relax p_{2})) \mskip3mu plus 4mu\relax\relax\land\penalty0\relax\mskip3mu plus 4mu\relax\relax  ((p_{2}\mskip1mu\relax\Rightarrow\penalty600\relax\mskip1mu\relax (p_{0}\lor\penalty900\relax p_{1}))\mskip3mu plus 2mu\relax\relax\Rightarrow\penalty300\relax\mskip3mu plus 2mu\relax\relax (p_{0}\mskip0mu\relax\lor\penalty600\relax\mskip0mu\relax p_{1})) \mskip5mu plus 4mu\relax\relax\Rightarrow\penalty0\relax\mskip5mu plus 4mu\relax\relax  (p_{0}\mskip2mu plus 2mu\relax\relax\lor\penalty300\relax\mskip2mu plus 2mu\relax\relax p_{1}\mskip2mu plus 2mu\relax\relax\lor\penalty300\relax\mskip2mu plus 2mu\relax\relax p_{2})$
\\[1.5pt]
\texttt{ceitin}
&$(\neg (p_{1}\land\penalty600\relax p_{2}) \mskip1mu plus 2mu\relax\relax\land\penalty300\relax\mskip1mu plus 2mu\relax\relax  (\neg p_{1}\mskip1mu\relax\Rightarrow\penalty600\relax\mskip1mu\relax (q_{1}\lor\penalty900\relax q_{2})) \mskip1mu plus 2mu\relax\relax\land\penalty300\relax\mskip1mu plus 2mu\relax\relax  (\neg p_{2}\mskip1mu\relax\Rightarrow\penalty600\relax\mskip1mu\relax (q_{1}\lor\penalty900\relax q_{2}))) \mskip5mu plus 4mu\relax\relax\Rightarrow\penalty0\relax\mskip5mu plus 4mu\relax\relax  ((\neg p_{1}\mskip1mu\relax\Rightarrow\penalty600\relax\mskip1mu\relax q_{1}) \mskip2mu plus 2mu\relax\relax\lor\penalty300\relax\mskip2mu plus 2mu\relax\relax  (\neg p_{1}\mskip1mu\relax\Rightarrow\penalty600\relax\mskip1mu\relax q_{2}) \mskip2mu plus 2mu\relax\relax\lor\penalty300\relax\mskip2mu plus 2mu\relax\relax  (\neg p_{2}\mskip1mu\relax\Rightarrow\penalty600\relax\mskip1mu\relax q_{1}) \mskip2mu plus 2mu\relax\relax\lor\penalty300\relax\mskip2mu plus 2mu\relax\relax  (\neg p_{2}\mskip1mu\relax\Rightarrow\penalty600\relax\mskip1mu\relax q_{2}))$
\\[1.5pt]
\texttt{plisko-p3}
&$(\neg \neg (p_{1}\mskip0mu\relax\lor\penalty600\relax\mskip0mu\relax p_{2}\mskip0mu\relax\lor\penalty600\relax\mskip0mu\relax q) \mskip1mu plus 2mu\relax\relax\land\penalty300\relax\mskip1mu plus 2mu\relax\relax  (\neg \neg (p_{1}\lor\penalty900\relax q)\mskip1mu\relax\Rightarrow\penalty600\relax\mskip1mu\relax p_{1}\mskip0mu\relax\lor\penalty600\relax\mskip0mu\relax q) \mskip1mu plus 2mu\relax\relax\land\penalty300\relax\mskip1mu plus 2mu\relax\relax  (\neg \neg (p_{2}\lor\penalty900\relax q)\mskip1mu\relax\Rightarrow\penalty600\relax\mskip1mu\relax p_{2}\mskip0mu\relax\lor\penalty600\relax\mskip0mu\relax q)) \mskip5mu plus 4mu\relax\relax\Rightarrow\penalty0\relax\mskip5mu plus 4mu\relax\relax  (\neg \neg (p_{1}\mskip0mu\relax\lor\penalty600\relax\mskip0mu\relax p_{2})\mskip2mu plus 2mu\relax\relax\lor\penalty300\relax\mskip2mu plus 2mu\relax\relax q)$
\\[1.5pt]
\texttt{jankov-i3}
&$(\neg (p_{2}\land\penalty600\relax p_{3}) \mskip1mu plus 2mu\relax\relax\land\penalty300\relax\mskip1mu plus 2mu\relax\relax  \neg (p_{1}\land\penalty600\relax p_{3}) \mskip1mu plus 2mu\relax\relax\land\penalty300\relax\mskip1mu plus 2mu\relax\relax  \neg (p_{1}\land\penalty600\relax p_{2}) \mskip1mu plus 2mu\relax\relax\land\penalty300\relax\mskip1mu plus 2mu\relax\relax  (\neg p_{1}\mskip1mu\relax\Rightarrow\penalty600\relax\mskip1mu\relax p_{2}\mskip0mu\relax\lor\penalty600\relax\mskip0mu\relax p_{3}) \mskip1mu plus 2mu\relax\relax\land\penalty300\relax\mskip1mu plus 2mu\relax\relax  (\neg p_{2}\mskip1mu\relax\Rightarrow\penalty600\relax\mskip1mu\relax p_{1}\mskip0mu\relax\lor\penalty600\relax\mskip0mu\relax p_{3})) \mskip5mu plus 4mu\relax\relax\Rightarrow\penalty0\relax\mskip5mu plus 4mu\relax\relax  (p_{3}\mskip2mu plus 2mu\relax\relax\lor\penalty300\relax\mskip2mu plus 2mu\relax\relax \neg p_{3})$
\\[1.5pt]
\texttt{jankov-k3}
&$\neg (p_{2}\mskip1mu plus 2mu\relax\relax\land\penalty300\relax\mskip1mu plus 2mu\relax\relax p_{3}) \mskip3mu plus 4mu\relax\relax\land\penalty0\relax\mskip3mu plus 4mu\relax\relax  \neg (p_{1}\mskip1mu plus 2mu\relax\relax\land\penalty300\relax\mskip1mu plus 2mu\relax\relax p_{3}) \mskip3mu plus 4mu\relax\relax\land\penalty0\relax\mskip3mu plus 4mu\relax\relax  \neg (p_{1}\mskip1mu plus 2mu\relax\relax\land\penalty300\relax\mskip1mu plus 2mu\relax\relax p_{2}) \mskip3mu plus 4mu\relax\relax\land\penalty0\relax\mskip3mu plus 4mu\relax\relax  (\neg p_{1}\mskip3mu plus 2mu\relax\relax\Rightarrow\penalty300\relax\mskip3mu plus 2mu\relax\relax (p_{2}\mskip0mu\relax\lor\penalty600\relax\mskip0mu\relax p_{3})) \mskip3mu plus 4mu\relax\relax\land\penalty0\relax\mskip3mu plus 4mu\relax\relax  (\neg p_{2}\mskip3mu plus 2mu\relax\relax\Rightarrow\penalty300\relax\mskip3mu plus 2mu\relax\relax (p_{1}\mskip0mu\relax\lor\penalty600\relax\mskip0mu\relax p_{3})) \mskip3mu plus 4mu\relax\relax\land\penalty0\relax\mskip3mu plus 4mu\relax\relax  (\neg p_{3}\mskip3mu plus 2mu\relax\relax\Rightarrow\penalty300\relax\mskip3mu plus 2mu\relax\relax (p_{1}\mskip0mu\relax\lor\penalty600\relax\mskip0mu\relax p_{2})) \mskip5mu plus 4mu\relax\relax\Rightarrow\penalty0\relax\mskip5mu plus 4mu\relax\relax  (p_{1} \mskip2mu plus 2mu\relax\relax\lor\penalty300\relax\mskip2mu plus 2mu\relax\relax  p_{2} \mskip2mu plus 2mu\relax\relax\lor\penalty300\relax\mskip2mu plus 2mu\relax\relax  p_{3})$
\\[1.5pt]
\texttt{anti-scott}
&$(((\neg \neg p\Rightarrow\penalty900\relax p) \mskip1mu\relax\Rightarrow\penalty600\relax\mskip1mu\relax  (\neg p\lor\penalty900\relax \neg \neg p)) \mskip3mu plus 2mu\relax\relax\Rightarrow\penalty300\relax\mskip3mu plus 2mu\relax\relax  (\neg p\mskip0mu\relax\lor\penalty600\relax\mskip0mu\relax \neg \neg p)) \mskip5mu plus 4mu\relax\relax\Rightarrow\penalty0\relax\mskip5mu plus 4mu\relax\relax  (\neg \neg p \mskip2mu plus 2mu\relax\relax\lor\penalty300\relax\mskip2mu plus 2mu\relax\relax  (\neg \neg p\mskip1mu\relax\Rightarrow\penalty600\relax\mskip1mu\relax p))$
\\[1.5pt]
\texttt{rose}
&$((\neg \neg (\neg q_{1}\lor\penalty900\relax \neg q_{2})\mskip1mu\relax\Rightarrow\penalty600\relax\mskip1mu\relax (\neg q_{1}\lor\penalty900\relax \neg q_{2})) \mskip3mu plus 2mu\relax\relax\Rightarrow\penalty300\relax\mskip3mu plus 2mu\relax\relax  (\neg (\neg q_{1}\lor\penalty900\relax \neg q_{2})\mskip0mu\relax\lor\penalty600\relax\mskip0mu\relax \neg \neg (\neg q_{1}\lor\penalty900\relax \neg q_{2}))) \mskip5mu plus 4mu\relax\relax\Rightarrow\penalty0\relax\mskip5mu plus 4mu\relax\relax  (\neg (\neg q_{1}\mskip0mu\relax\lor\penalty600\relax\mskip0mu\relax \neg q_{2})\mskip2mu plus 2mu\relax\relax\lor\penalty300\relax\mskip2mu plus 2mu\relax\relax \neg \neg (\neg q_{1}\mskip0mu\relax\lor\penalty600\relax\mskip0mu\relax \neg q_{2}))$
\\[1.5pt]
\texttt{plisko-p}
&$(\neg (p_{1}\land\penalty600\relax p_{2}) \mskip1mu plus 2mu\relax\relax\land\penalty300\relax\mskip1mu plus 2mu\relax\relax  \neg (\neg q_{1}\land\penalty600\relax \neg q_{2}) \mskip1mu plus 2mu\relax\relax\land\penalty300\relax\mskip1mu plus 2mu\relax\relax  (((p_{1}\Rightarrow\penalty1200\relax q_{1}) \lor\penalty900\relax  (p_{1}\Rightarrow\penalty1200\relax q_{2})) \mskip1mu\relax\Rightarrow\penalty600\relax\mskip1mu\relax  ((p_{2}\Rightarrow\penalty1200\relax q_{1}) \lor\penalty900\relax  (p_{2}\Rightarrow\penalty1200\relax q_{2})))) \mskip5mu plus 4mu\relax\relax\Rightarrow\penalty0\relax\mskip5mu plus 4mu\relax\relax  ((p_{2}\mskip1mu\relax\Rightarrow\penalty600\relax\mskip1mu\relax q_{1}) \mskip2mu plus 2mu\relax\relax\lor\penalty300\relax\mskip2mu plus 2mu\relax\relax  (p_{2}\mskip1mu\relax\Rightarrow\penalty600\relax\mskip1mu\relax q_{2}))$
\\[1.5pt]
\texttt{plisko-l}
&$((\neg \neg p_{1}\mskip1mu\relax\Rightarrow\penalty600\relax\mskip1mu\relax (\neg p_{2}\land\penalty900\relax \neg p_{3})) \mskip1mu plus 2mu\relax\relax\land\penalty300\relax\mskip1mu plus 2mu\relax\relax  (\neg \neg p_{2}\mskip1mu\relax\Rightarrow\penalty600\relax\mskip1mu\relax (\neg p_{3}\land\penalty900\relax \neg p_{1})) \mskip1mu plus 2mu\relax\relax\land\penalty300\relax\mskip1mu plus 2mu\relax\relax  (\neg \neg p_{3}\mskip1mu\relax\Rightarrow\penalty600\relax\mskip1mu\relax (\neg p_{1}\land\penalty900\relax \neg p_{2})) \mskip1mu plus 2mu\relax\relax\land\penalty300\relax\mskip1mu plus 2mu\relax\relax  ((\neg p_{2}\land\penalty900\relax \neg p_{3})\mskip1mu\relax\Rightarrow\penalty600\relax\mskip1mu\relax \neg \neg p_{1}) \mskip1mu plus 2mu\relax\relax\land\penalty300\relax\mskip1mu plus 2mu\relax\relax  ((\neg p_{3}\land\penalty900\relax \neg p_{1})\mskip1mu\relax\Rightarrow\penalty600\relax\mskip1mu\relax \neg \neg p_{2}) \mskip1mu plus 2mu\relax\relax\land\penalty300\relax\mskip1mu plus 2mu\relax\relax  ((\neg p_{1}\land\penalty900\relax \neg p_{2})\mskip1mu\relax\Rightarrow\penalty600\relax\mskip1mu\relax \neg \neg p_{3}) \mskip1mu plus 2mu\relax\relax\land\penalty300\relax\mskip1mu plus 2mu\relax\relax  ((\neg p_{1}\Rightarrow\penalty900\relax (\neg p_{2}\lor\penalty1200\relax \neg p_{3})) \mskip1mu\relax\Rightarrow\penalty600\relax\mskip1mu\relax  (\neg p_{2}\lor\penalty900\relax \neg p_{3})) \mskip1mu plus 2mu\relax\relax\land\penalty300\relax\mskip1mu plus 2mu\relax\relax  ((\neg p_{2}\Rightarrow\penalty900\relax (\neg p_{3}\lor\penalty1200\relax \neg p_{1})) \mskip1mu\relax\Rightarrow\penalty600\relax\mskip1mu\relax  (\neg p_{3}\lor\penalty900\relax \neg p_{1})) \mskip1mu plus 2mu\relax\relax\land\penalty300\relax\mskip1mu plus 2mu\relax\relax  ((\neg p_{3}\Rightarrow\penalty900\relax (\neg p_{1}\lor\penalty1200\relax \neg p_{2})) \mskip1mu\relax\Rightarrow\penalty600\relax\mskip1mu\relax  (\neg p_{1}\lor\penalty900\relax \neg p_{2}))) \mskip5mu plus 4mu\relax\relax\Rightarrow\penalty0\relax\mskip5mu plus 4mu\relax\relax  (\neg p_{1} \mskip2mu plus 2mu\relax\relax\lor\penalty300\relax\mskip2mu plus 2mu\relax\relax  \neg p_{2} \mskip2mu plus 2mu\relax\relax\lor\penalty300\relax\mskip2mu plus 2mu\relax\relax  \neg p_{3})$
\\
\end{supertabular}

\vskip 15pt plus 1fil\relax
\textbf{Frames:}
\par\nobreak
{\setlength{\lineskip}{24pt plus 12pt minus 12pt}
\begin{tabular}[t]{ll}
\texttt{basic-1}
\\
\includegraphics[scale=0.5]{testframes/basic-1}
\end{tabular}
\penalty0\hskip 2em plus 1fil\relax
\begin{tabular}[t]{ll}
\texttt{basic-2}
\\
\includegraphics[scale=0.5]{testframes/basic-2}
\end{tabular}
\penalty0\hskip 2em plus 1fil\relax
\begin{tabular}[t]{ll}
\texttt{basic-3}
\\
\includegraphics[scale=0.5]{testframes/basic-3}
\end{tabular}
\penalty0\hskip 2em plus 1fil\relax
\begin{tabular}[t]{ll}
\texttt{basic-4}
\\
\includegraphics[scale=0.5]{testframes/basic-4}
\end{tabular}
\penalty0\hskip 2em plus 1fil\relax
\begin{tabular}[t]{ll}
\texttt{basic-5}
\\
\includegraphics[scale=0.5]{testframes/basic-5}
\end{tabular}
\penalty0\hskip 2em plus 1fil\relax
\begin{tabular}[t]{ll}
\texttt{skvortsov-1}
\\
\includegraphics[scale=0.5]{testframes/skvortsov-1}
\end{tabular}
\penalty0\hskip 2em plus 1fil\relax
\begin{tabular}[t]{ll}
\texttt{skvortsov-2}
\\
\includegraphics[scale=0.5]{testframes/skvortsov-2}
\end{tabular}
\penalty0\hskip 2em plus 1fil\relax
\begin{tabular}[t]{ll}
\texttt{skvortsov-3}
\\
\includegraphics[scale=0.5]{testframes/skvortsov-3}
\end{tabular}
\penalty0\hskip 2em plus 1fil\relax
\begin{tabular}[t]{ll}
\texttt{skvortsov-4}
\\
\includegraphics[scale=0.5]{testframes/skvortsov-4}
\end{tabular}
\penalty0\hskip 2em plus 1fil\relax
\begin{tabular}[t]{ll}
\texttt{skvortsov-5}
\\
\includegraphics[scale=0.5]{testframes/skvortsov-5}
\end{tabular}
\penalty0\hskip 2em plus 1fil\relax
\begin{tabular}[t]{ll}
\texttt{skvortsov-6}
\\
\includegraphics[scale=0.5]{testframes/skvortsov-6}
\end{tabular}
\penalty0\hskip 2em plus 1fil\relax
\begin{tabular}[t]{ll}
\texttt{skvortsov-7}
\\
\includegraphics[scale=0.5]{testframes/skvortsov-7}
\end{tabular}
\penalty0\hskip 2em plus 1fil\relax
\begin{tabular}[t]{ll}
\texttt{skvortsov-8}
\\
\includegraphics[scale=0.5]{testframes/skvortsov-8}
\end{tabular}
\penalty0\hskip 2em plus 1fil\relax
\begin{tabular}[t]{ll}
\texttt{skvortsov-9}
\\
\includegraphics[scale=0.5]{testframes/skvortsov-9}
\end{tabular}
\penalty0\hskip 2em plus 1fil\relax
\begin{tabular}[t]{ll}
\texttt{skvortsov-10}
\\
\includegraphics[scale=0.5]{testframes/skvortsov-10}
\end{tabular}
\par}

\vfill
\end{document}