From 931351f869d0197c78ac85ba4ba7718525969dc3 Mon Sep 17 00:00:00 2001
From: Mart Lubbers <mart@martlubbers.net>
Date: Tue, 20 Oct 2015 20:21:47 +0200
Subject: [PATCH] update report, added solution to 2 image

---
 ar/assignments/2.tex        |  58 +++++++++++++++++++++++++++---
 ar/assignments/Makefile     |   7 ++--
 ar/assignments/a.tex        |   9 +++++
 ar/assignments/ar.tex       |  10 ++++++
 ar/assignments/preamble.tex |   5 +--
 ar/assignments/s2.png       | Bin 0 -> 14250 bytes
 ar/assignments/src/2.py     |  68 ++++++++++++------------------------
 7 files changed, 101 insertions(+), 56 deletions(-)
 create mode 100644 ar/assignments/s2.png

diff --git a/ar/assignments/2.tex b/ar/assignments/2.tex
index 7bd482d..f4789d8 100644
--- a/ar/assignments/2.tex
+++ b/ar/assignments/2.tex
@@ -38,10 +38,10 @@ specified width and height.
 		\nonumber & \qquad\qquad\qquad \vee c_iy>c_jy+c_jh\\
 		\nonumber & \qquad\qquad\qquad \vee c_iy+c_jh<c_jh\Bigr)\Biggr)\wedge\\
 	\bigwedge_{i\in PC}\bigwedge_{j\in PC}\Biggl( & i=j\\
-		\nonumber & \vee c_ix+\frac{c_iw}{2}-c_jx+\frac{c_jw}{2}>15\\
-		\nonumber & \vee c_jx+\frac{c_jw}{2}-c_ix+\frac{c_iw}{2}>15\\
-		\nonumber & \vee c_iy+\frac{c_ih}{2}-c_jy+\frac{c_jh}{2}>15\\
-		\nonumber & \vee c_jy+\frac{c_jh}{2}-c_iy+\frac{c_ih}{2}>15\Biggr)\wedge\\
+		\nonumber & \vee c_ix+\frac{c_iw}{2}-c_jx+\frac{c_jw}{2}>17\\
+		\nonumber & \vee c_jx+\frac{c_jw}{2}-c_ix+\frac{c_iw}{2}>17\\
+		\nonumber & \vee c_iy+\frac{c_ih}{2}-c_jy+\frac{c_jh}{2}>17\\
+		\nonumber & \vee c_jy+\frac{c_jh}{2}-c_iy+\frac{c_ih}{2}>17\Biggr)\wedge\\
 	\bigwedge_{i\in RC}\bigvee_{j\in PC}\neg\Biggl(
 		& (c_ix-1>c_jx+c_jw\\
 		\nonumber & \vee c_ix+1+c_jw<c_jx\\
@@ -49,4 +49,54 @@ specified width and height.
 		\nonumber & \vee c_iy+1+c_jh<c_jh\Biggr)
 \end{align}
 
+All subformulas describe a constraint from the problem description and can be
+separated in three groups. Subformulas going over all components, only power
+components and only regular components.
+\begin{itemize}
+	\item\textbf{All}
+		\begin{enumerate}
+				\setcounter{enumi}{7}
+			\item Describes that the width and the height of the component can be
+				swapped(in case of rotation).
+			\item Constrains location of the components in regard to the size of
+				the chip.
+			\item Makes sure the components do not overlap by defining for all
+				pairs of components that they either are strictly right, strictly
+				left, strictly above or strictly below the other.
+		\end{enumerate}
+	\item\textbf{Power only}
+		\begin{enumerate}
+				\setcounter{enumi}{10}
+				\item Power components must be at least $17$ block away from
+					other power components. This is defined by saying that the
+					difference between the center of each pair of components is
+					bigger then $17$.
+		\end{enumerate}
+	\item\textbf{Regular only}
+		\begin{enumerate}
+				\setcounter{enumi}{11}
+				\item Regular components must be connected to a power
+						components. This is described using the method from the
+						overalap calculation in a negated way. Every regular
+						component must have overlap with a power component that
+						has been enlarged by $1$.
+		\end{enumerate}
+\end{itemize}
+
 \subsection{SMT format solution}
+The formula is easily convertable via a Python script to SMT format and said
+script is listed in Listing~\ref{listing:2.py}. The Python script optimizes a
+little bit from the original formula by leaving out the overlap checking
+between the same components. When we run the file a solution is found within
+$30$ seconds.
+
+\subsection{Solution}
+Figure~\ref{fig:s2} shows the configuration found by the solver. Light gray
+components are regular components and darker gray components are power
+components.
+
+\begin{figure}[H]
+	\includegraphics[scale=0.75]{s2.png}
+	\label{fig:s2}
+	\caption{Solution visualization for problem 2}
+\end{figure}
diff --git a/ar/assignments/Makefile b/ar/assignments/Makefile
index 2055aa8..4cfb119 100644
--- a/ar/assignments/Makefile
+++ b/ar/assignments/Makefile
@@ -1,4 +1,4 @@
-LATEX:=latex
+LATEX:=pdflatex
 
 DOCUMENT:=ar
 SOURCES:=$(filter-out preamble.tex,$(shell ls *.tex))
@@ -7,10 +7,7 @@ SOURCES:=$(filter-out preamble.tex,$(shell ls *.tex))
 
 all: $(DOCUMENT).pdf
 
-%.pdf: %.dvi
-	dvipdfm $<
-
-%.dvi: %.tex %.fmt $(SOURCES)
+%.pdf: %.tex %.fmt $(SOURCES)
 	$(LATEX) $(basename $@)
 	$(LATEX) $(basename $@)
 
diff --git a/ar/assignments/a.tex b/ar/assignments/a.tex
index 2c35ac5..8ac130a 100644
--- a/ar/assignments/a.tex
+++ b/ar/assignments/a.tex
@@ -1,6 +1,15 @@
 \section{Appendix}
+\begin{lstlisting}[caption={Benchmark system}]
+OS: Linux 3.16.0-4-amd64 #1 SMP Debian 3.16 x86_64 GNU/Linux
+CPU: 3600MHz AMD FX(tm)-4100 Quad-Core Processor
+RAM: 8GB
+\end{lstlisting}
+
 \newpage
 \lstinputlisting[language=lisp,caption={a1.smt},label={listing:a1.smt}]{src/1.smt}
 
+\newpage
+\lstinputlisting[language=python,caption={a2.py},label={listing:2.py}]{src/2.py}
+
 \newpage
 \lstinputlisting[language=python,caption={a4.py},label={listing:4.py}]{src/4.py}
diff --git a/ar/assignments/ar.tex b/ar/assignments/ar.tex
index fc99f80..94e25f9 100644
--- a/ar/assignments/ar.tex
+++ b/ar/assignments/ar.tex
@@ -1,11 +1,21 @@
 %&ar
 \begin{document}
 \maketitle
+\tableofcontents
 
+\newpage
 \input{1.tex}
+
+\newpage
 \input{2.tex}
+
+\newpage
 \input{3.tex}
+
+\newpage
 \input{4.tex}
+
+\newpage
 \input{a.tex}
 
 \end{document}
diff --git a/ar/assignments/preamble.tex b/ar/assignments/preamble.tex
index e9669d1..93b06ec 100644
--- a/ar/assignments/preamble.tex
+++ b/ar/assignments/preamble.tex
@@ -1,16 +1,17 @@
 \documentclass{article}
 
-\usepackage[dvipdfm]{hyperref}
+\usepackage{hyperref}
 \usepackage{a4wide}
 \usepackage{bm}
 \usepackage{float}
+\usepackage{graphicx}
 \usepackage{amsmath}
 \usepackage{listings}
 
 \everymath{\displaystyle}
 
 \lstset{%
-  basicstyle=\footnotesize,
+  basicstyle=\scriptsize,
   breakatwhitespace=true,
   breaklines=true,
   keepspaces=true,
diff --git a/ar/assignments/s2.png b/ar/assignments/s2.png
new file mode 100644
index 0000000000000000000000000000000000000000..2876b39db77a0a854379fb22f74195d07cfed485
GIT binary patch
literal 14250
zcmbWeWk6Kj_clzIQc?mEill(Z44q0zNq33Jzz`x*(qMqJ(hL#;0@B^3AU(8nNq6T^
z?>WPLzyII+e}2!G_lwNTIcM*E*4pb@*Sgj=Nd1`tF%caR1_lPP;!{~o3=FJ$7#Nu0
z1X#c?tg}}xz#nX<CyLqx1OyX*)n+j;m@yP(A8Wrg-JEilj&`|h+NCXcEX!O+CLkcL
zso~61c@&2aTkL;VR*`@YFNc*UOjTIICoB_nZ8Db(3RZR5Tn*O!844B+K6Kn=rp=gr
z%|URp`J6GFa`8ql1iM+hSA6@_A}-loviJDR+q+ScX~{ic*@Ex(&5E3nQ>L6Nt-n{I
z)KpANg*zwZZY)G$s90j#_vJswv(=h(Z0EgPcRu^feZ;^bVD|Hi!V%AqUCxkk(#Ii_
z#=yj>TS6wfnf|nfiZajXM`II{zXR_}z3Y!Se{)%qG~~h>cf>o^R?Jb5QM+ctxz|2&
z-1`+6+Iqa)QBv%+gS<>5ZJ!P>mb52U2JI%2Rze;a6?$J9(cky7|DOxU&oFM<^;Q#D
zaOi^~nPuYv1RVQa#zUGDXGRe#g>W5>?0gRMv5d=niBNg1k;J8~P916;Z|n8K^#UPx
z&aI5Ymf+ls=|6Svwoh`NYLF5K43zoKNT}1rE1ca`^ZH?DjO+M?1`+9_Ioc6?UVjz5
zI;Kgqv(9)pkX%P(DZ#C1Dkkt`E!FDj!q=0*U(7#07&^I$i<H#|_E$PBNVzU>h4J6U
z39P9~e8)hU7gnR8G%P>G!D^fSEIO@RgI&o+$;W;uNV80EO_nwqypA_ke)lUK@K0!@
z3H>jQzpdjBl*-<pkCVxD6cRs<epi0?lV*`1jt0?i0JG9h@aH^YtE>bfr}KTat3s1c
zierie9uJi}2ZACly_6?|ehuO;o$#heUIpI5{cG8w{9^f>e>G|&t?r^!B6jkyBrSUl
zJMKQWQS@_-O9`>{ggdq^bu9yHVz4C_86&Qh)PslYo12Y1BtEO^K92|9^&O|^N9yM=
zbMtxVA;YRmhJMS`$j&&GH@?e`{BT-)BQL@?#VoSXq2h1YkHYipmZI~M8aOFK@Hj$e
zXFZUm0{QmnY)(1x)-&r}f8U--iM4bJ_tov0va_Gd$0=Hrtm4|6Py0#sY-K1}8wF)G
z{x2VD1zWUODg|3K(ny9(=>RLqk8zBZ_cxi-3p)^`zZ?nRQ*yQcj}HsO0a1h9)gP|z
z-}K%5SbR4*F8M9pxkKY6DX-b#PG5NbyJm-k$=unjjS@V!LZ87=n;nW=z23TtdNcKt
zlONthF>*Ssx(jxmr(Hg7rr#G1Or~NFH-0$zY#NOTamk!MWNJ)2%$f*rxp8ylk-OIT
zH}{Lpj)vh4WCZVl&)(tgHzfp*nB(Z={LzY}e`b^9Jlhc;)1^+3`EGAYrm@I+!@4NW
zhja68vh^dLj=1~me?P=#w%Q-xrWN3TW;Zt_77D$ZL3k*lDCG%-hLf#!N#5AX+-9v6
z{Gd_tpC1mz^y>fTdowcvy^n6W&Zar}W%K;~_7X6Se0`w(N!{JGZyV!e760EM-q<#G
zz%%7qLh<iSc$h%{>|Onx+6@@p^}hH{N<)=(>=jKbn4@>&l=;1z^}+`!x45IScv5@g
zL|VqFHnqpmWy%Jfh||@1*!klz_Q)Iy!``L%sA;;1$2Iq<Za=a&364}F!jn;Koz81=
z#b=^laX8r8TmFdOJH8)REO%y>;AuDTORR=#@L-*OO33LVP>L!#SrN5xk++lGKqPRp
zbxq*!D*cN4TD!xwg)G^VNjAoY72fT_Cs_D|b_dLEe9-t6R&J$I^&WURg^qk;^Jw6M
zd`H1QAO5`l)A*0gbjEbw+sX(FfcDdI!1pm@`X|<aXWjpsZPBK>w$Ra?iHp*FVaL_z
zv&by&2C;4<$0BFBfvm&Sv1LYm{_?~$ijw@<L_OWguaCY5N~Ca$zek0ICmgJ~ou0M{
zhK`=imbvkFQ62OdMti=wYE4hCe3>-qZ8hvPsP~;SC`YvDAY?Gas5u$sDP@Mcsl7G#
z$7O9G!HRK<X@S1aQ~qd%T1_W9`P?IdM6Aa8_w?6a2fcCjN?hDrT9JegI(rQ33{l#q
zPEgc|r$J9F(RL5VMs?bhK0Qsmc7-5sGTnFE=5K@o1nD2>Z40@8SX&NLPNPf~;tkjI
zn6465T6LG<<Hfa|pX2zx92Szk&_kc23aNnL)5wMyQ`VdeR=<BBHNxSIE5FT+96L_i
zekVrF%2}<Vom{<IZGz1hzLm|velZ<Fjh$j#xmQeIi;HLa2vywX$!@Qj=R_gXXP)kM
z<BHL@dOd&_bF-k@3YIc&#`Yj6M_m1PhrKezrLdE>=kI-;<chWF-<X9LpWS#Lnk&{?
z4#s5};z-muM~y5NccrXW**vWsX3;ILD|SfjP$sMo{1Kz(?jj%A!?h@R$@Y7yt_(Z)
zGO=7EQBlV>y=RESklrQjju~D_V2%}j!oGYGhum_Qs77!P@H1tS(3&i#r~?4Q&ePcx
ztZvh<w@#(|ZOAuYb{I2x?$3P|a^(#n)bY4{*fn~N>csvin68%im?FzXssZx7C&~J;
zmRz8aPfP>c&Nd>|arbn0K4V*-*lWLPBQP|$lvau@IY-oSf~(Wsv?2IeTV~(oCQr4T
z&Wv9aBkS_&{EvnErq!kHy#diXgnIY{c<Q~GX)Hz*VydC5Gz;`YLa2&o9VtvY(F378
zXT9SHc)7uV(C=s(Q~(Y~HR%Gyc%$m$fghcDuS61}X9UyIB~os#(@NJT8qm}9XT$9Y
zGUb6JA^S({lxCU?L=VaM=lHnGU?$lI6NtME+4tGHyPqNhcq+lH(nJ4_<9)ZgObomg
zQ4UAtu@p0LH<m~3<yzud7_5!AU0p7@RsUXM63o98d8=;4N)w+k^MWg<p*^P2@@?M^
z&#B<Vx3k)In4oeif>6f6=*_J2-`$6%Ch>HVyv7|#q*@X2#mN)XV=-Ui4iAk&G(8kJ
z>pit2sZ+*LH4ipVwXN1}I~wc-RIv=yC!{kus1P#tDR%s5g#I1-R6sE;=9<Z8zw9Yi
zC$F}aWo>M(k$%(6ZaU87bG_87+U59_qRt6uk9)BoucJ=yIN7r>#aHMo5YDGmRebdA
zgIIgA5CECWARK@}?g^Mg5!>M{cvCNsY{&LnPXkAv*5_>d3liJK1x5Bu(d5VH>{lV#
z_75`7tH^1-H!}V)V~7nZ(fKM;w=!%RBeYj9HnU^rRZyNY^G2hQbju5&L1~Gc*#DK?
z^&o22QV%&Aud$DWja6h6Ejw&*ct6=$mvGk^s9vkEOt-^L34aB7Y4OZOGH<oWIQsBl
zYgyjqM>mgT+>Ef^4|(^aHqx6!k?*ijzZ;VDwFl=uR;(qc+in$P1t_POdp&G4pB`DV
zIWgQrW7j_G<l}#`p0Ls@`%mdW))VezD-~P|iZq~~<ESpb8xC-aIo}E(dr-1&NpDiI
zhTgKTvz8-t`z+=#RJve89XRx7%}ni~h{Go^ixvd}@OX!{^4~mTO21s%{Bh`B6rax(
zja$bR5czJwltS{__B7BwvMVu-%iKS|ck?)OwFe8b_s1T`&>%CWcb@>9jqLRe%z;oN
z6_)oPFC5~UE%!X$+V_sS9PRV>5v5*~mifT!2arSSr>UZix4(xt{z-~0`F)xaLn;%@
zpNQ-{wo)4*!okNE<LeqQq!qM_ua~g0AAQhzNsz78R1CQ7>n}No%d-dd;AE4se$aU~
ziVi-Igt`!Yh7E~4JRkxWL4jF25Slum!Gou~<QY}_QPx{mKT*D_Uv=Ylz!cWU6gfpb
z_lI@720X4z5g0gR>WzLI7CJqof4#olHK*zhu5+NSD=JhKOBq*`uhO_+JLrRBVOmrS
zdzrUHULI9B)@F@sdH;mh&ovP+&#GYlPJz+!Lbcz#?D}%$3FNMc5ubsy*Xa=a=Hl{u
z&m~SfAj<Vj9*;VEJlqUvnJ#28{BK|dOChzX>G*FG&9%I3_&b<MfAeFC$w9&Ebm8Ru
znp+%_bt{VpMtV~|)pLtk4;b-6{5%PFwkPYCv~HyTXrC(H*?$$`)vwS2NiXMPMt#D-
zA|~W$upaJv{FW4R5sOMhOqYSyx%bfCz_YV|lme6Z#*Ugvb5vGG!Ngv})vW%u5njc>
z%k5Pt7QrZwG@>{$)K8u;n(>NF;slY*!{F{^noh@d8xzNvB~=(n*&?T;mMvn|F?yR;
z?<@rQ$CtF<WlsoqMrDiZ!a(-Vj0}NL4J^JahYquA^#JRt=kX+^HZru29Oo-{Q#vH+
zW?o6N*b#v^W73Zjc!n4OG}q5!nV2zYEH6sd0xTz9;ZmAG2lL6W6~G;2{h>+D5@{1B
zY}@jPP^TQjaz$H0!kGk9he$Y<fx|Ylv%~pKR)%d}TR4N$8y0~;(i=C@7fklm2Z^wr
zQO!<=YPpLDgH?)jI!=|)Acy2Ta&RlsQ8Oc<8_l)A1q`gPTSY9$ugZoHd+E>4*kf7y
z?IL1t^1^K5o>LJ<XL#?NAh9!yIO{JRI)6#PV7hWnGJ0fv4SsV_3q=Fb-ToAZATf=%
zsHQtJi-XHo>S-7K5G=)1af^$*xbUemuigm!3d!dl+e}>%v2$Q01Wf=R-C4hy-P0i@
z-5li-K9B9FC-Uj!wJmw}nmLZBtm@79{=*r8D(|k;WTCLyIh8%m5an8#d0=~)Vg)nt
zETZ|Djzytx{c?JDkw(2?RosVH3iE$1YvTL=KoWgtyYhHt3U~hG;{rzX&!kcR3bR2}
zP_gqSy)oO1M&|yiOKcFj)9->+;l#Pl<ijShlpps4zFK3DYKb$c-c$g!5OaF{xO<e!
zB(}AeVWao`<dn6@Xz(q)o+?|5wq-%_+ke}-Yx=wSDRGP+K36~#zbuHTcXw>3p8+yv
zIZOAUMFu`U)}nzCWA#~5h10a}W$RHg|Jj}(;ECrcesf;t$Z@Fm@Rw10e22}JKm2E*
zIt`VF3+!qVDRiZ<^?0)1xsMlR(ma8x@gC;y8K_vTFVYv;v5$Y|`P5g0rQSo*?L#5r
zhxI*%Z6(KF_%jPx4<lAbOi*34t1cIF+6^{K!t7rNm|q9^&CQr$r@QLg?^J)2&i%5k
zg;+I5yvlC-3>25oq<6DutFd<_!R>*8<%0VZ;-Wf=u2uV9Vnqws@+*;i0Q^;zi(!eJ
zbb%%M7z00gXoY|BtG%H<+&yI#zk3&W(2yF~X0cWg4J^Qy92#b1womX1Gg$FjVlKj4
zb)$>yG_QsS%&ZVK(@-}(-rt2~;@bxd;NE7#{0-0Kc30f^YR2XrX%b!OThSI-Ynqv7
z08u4Jf~zv527DKqk0({^aoBA;afbUbB4s@5a|z5a*%cKI?xr}uxj^LGK>23``5Q66
zy{zZQyLVP3eUN_?#vg+L)RzZrH!X=@@2c7XmckQQU*l#YBqk%EEZc?-g*!CrUj2DB
zK}{=3-$l+$4@_RSrQK)j+YlB5Ea>NFibI)|P!ftPEEHF_hM>x5p^k>f^I}>(tG_=v
z-UC)hAj}P*!tE~25y{JAp~fyA!K)(pVeilPqGzI$9R6tAdXNKeQRg{X`O0+Jg=M0`
zPU3CD=4B<*s?|UU`MfN+%-8zTr`}%azAe~SA}GIR9&!N1029i9aO!N`{P{X;0d#^x
z@8W|YOqOltR{}en*dYP^CmjPgNuNLo7k~uq;0rS8SvSm1L@_m5kQjQ<R8M=@Lo6W!
zJU1x~qzSyJb~5nNA<<|eEU&Skc6xz|Rxfq>Za)OAVH^^SCcu<##quZ>-TpJ^>v64M
z*Z_G%MXskJu5rU{S?4l`@m3NzBAI%Gp9J7XOXT^1BjmDAQ(`KM9sS;G)auDFJKUMN
zlA6U(PKmcKGi$P<r@>8Qa|^IYCqzi1(zdC&pCLxdPD^z@<01MfUcg$=U=oLOF7J`8
z;l!L8TBeuKoBEN(+dgs52zj(6%I>9}42A;i`<L!%=M2BN^+~K(;%4842_-vc{_8$9
z@Gbl^senlk6$aq}Xj_tEo=HXE$ZvOs4C9leqpfb8hXG`(2T#S(HpIrtNWgpj_6G1u
z(y7H@2;?#E0!#9n0QdW5R#gYyQ-e~r^aW{x6?wq;H3>F&!NAbg>VBROy06fhQ1FX_
zA2dCwIxP!)5D%9!i*`MTN{_a;5v{bmPygP9en}*EsyOm%N3ndjGIzemY$&qs6~`h5
z!ac{D1em@r&2JCtbTlN=c$6<*F8mY)j?6sEg()_m5-zfuU(ArP4)Z4;9R40%mD5%h
zf_}fdKs2>NvS(J}6$^dhQhe>2Kh={y^JFhImTAt&MbBD5u71AKjV@A3Y9i8^JnP(A
z0)u`JJ|umungyo<UtIbDIvamQo;=!({{F_eBKS>WTw$EX1B;9l^ccJpfK|C^ZP{+t
z+jsa6er#)e>tb$mQuSIY&IJ+huXluz@hI`KHS(E}LVJo)m%Ym78ROFt60cR22T>|g
z;9Vm?jux`mA*eZGN@2PRT(42Ow#+z%`Z-+QQzpIbddUEyRQZssV1fo{1)SnE-$6yn
z!_BR79zao{WXbjQwKho*1{RV>+MsladgPVofcuP{pl#*V!K4I^e&9Glp%VeOZCK#}
z21tE~xrJP@ZJ-6e^mPONhT&z2fNyPvb(E2S*1-7Mtq-iF7J?o+<)Plandvty9S-}<
zTR&V^Q01Ujd=?(_<%e2R<mvRntGgO0RHiEkkiWJb*)UAr6<<rKRnyBZ>^*3g1hFsj
z2&h`|8=W~Cnc<ID&eXUSxyuV#k92?d9oiKLcpY8&L^aSc*AK*A24xZaaL$}8GNN*y
z;eKmwmgp*3-sZX$sAuKtc~Kj*8aNVua@2tv$SIn3n4kxQj_>KoRG!q7V4l%)>4=WR
z0TSf8!vJb@)i*|3PGhT@dh^`fm2Can7_L&doyeZ=Lve45v+>+Q=w|8Lh`;G9Pp~GA
zYvJ*aF8856>Gnqn@Nqn<tc1wWdISGW5=p_nnU$%<-W#OJ<pTB!!iZd)3^mB<k6ed!
z9ut9e{)O#rhWVMYT-X!eO;mtdqGSe=Rjsb%tGEpbfvwglW?L4L3NtGrInRSn{NW}M
z$1})q+GNz35F<l9>-xf$SZQ)%16NoHY&_{`T;llV2IS2~{?)mIeCyB3z%9?cZF)7n
z(yd3ObPRHG1{&3IDQ=eE$kW}F3-?ODPbT%RXkSj-13P_X>Q`f%*;dUrW$9Ymt%R}V
zlemsa&f$~E5$Bo8D;Z@P39>O(=G66eeAto7#rcZJ@$K8`eVKlN9W%9cqnhs38NW2O
zw>BL#y<!KJ{H7X5g4z2h#~bTeE3?<mECmyP4z@*=z_yCTxq|sAB9?|I^Ge6XRVnkF
zB7**`an#A6DtJ|poKYwTkr=~1wz_6HGqS$5qJv3?MR=w{w|=kv_C{xW7Ydax$623_
z+WC0@SYJ4{o7gR^-geP^Kf%nE*Bw%SJUY!YY4JStNg`I}tMme)jgynUj$cuMQX$86
z=FUO`p@LR>UWG9uiSS1|tL4R&Q{xgRdRp5ZA(fNUL4|B^uPxgehc%b&xiiv97p>zg
z?#I|!Jo;i=X@wV6ZMSJZisBMUg{+C5CgwDF59)YyuDPs3D#8hOHl=JYKmBkcj(2z^
zcK(ejxB2v0uBerodts>HDv|!5F6+9TQiff5mWUVHJ&Su1?k~S}W%-dj#mbYh=fMW3
zYyN3kB@mu|4LFoDiTyM;(&fNJU`+=k9f2?w1u*kY>H`q@O1xTC99j@0^oS$S>8YQ~
z3Rz;;yDFi1eh)fO)F%53a#U_|F?1Ou%qxv>oD6>of;XlC$PJizHBnuN8-?vvSYz)?
zv4NoV^P2`RHKA$6WWel=ZbPRg4e9DF@7_O`9+ej7Xuv4J>SPksa^kQ(T2i3#kg9g_
z;vh}@^2ZV%4D(~Gqs)Y~i^6URLHIm_$tLkoJrn~Rl^1uTi<(Mg!gP}EXeimIp{C_U
zA9}bWA^@he+-HNMCSuvn9hb6?T;;|lSdY-`{52D%=dA!_ot2Ez$%kC*Nvo4k91ujC
zszEr3EISz*9x+)}8&g^CAyfdLn0(rl47KQxh@Ht%F7mE)nrsjLhJN=^p66;k1h@AM
zdT!SmF@vU&mTtp3@<Q}KqL8_sO9e>W@$?$#RR!Y!iT+bi5@;z2AUmn_mO9Lga<W^d
z(0Ga|0Cv8kXT=ax0_%xftU^B!Ml(CDGEXdm1=>)$9zZ@1_*-mnn$%sa&OsHq%W2==
z2X>rPg8SDhe{ic%4>>qI&ZLR7BZ5;go~gD8b#i>ldU^(<pN>a$MzC(ZYCb{VLdOGe
zpy(uFyDdjg=M-tJ=P8a9p7EqthQlkZB4Bdz12`jq13upAXRv~+ove2Q5XF?b6e`9)
zBfV4hx0%qZO2?&?8tl$pANmdvGM<uJF@68jc~ki;Q&Xz6|Ktv6lh?i=AL<;`ovIa{
zEoa*6S!CsgSK6WWv_sC;`JMo8gW)d^0*;(Q1)D44_Ta;Ip=^f(`=m%IDZ|P3Ou}nR
z0;9lNhaSz9ED$>?WOzapq^9F<iKj+&T)5o6i(U!~n7C&?jpZ^GHSlq?3q5bDi#*en
zoSv!tqDlesPUhK5EcryFu7uL+HgE4$p4X&i^q8G)gOq2DuAc&R&2Y+aE-sLL3<<?W
zwT$-V9Ke+44VI;u52@wR3A+ypQVcqUaFAV96@x7M?VH56*2WYLFVsnvKVz)--4%?(
zb#!R8Jb<DJ05eGB4DPvtULkvJ4D5$029Tv<V3lCG0{d;DT#MyhsC@6|c9GqzA2w{Z
zT_otMct9xqpB)KLMtJKUnj?P(iBhodC3LaV;Mip3F7pDZMSy;#gJPyfW*#p(IBUQn
zitBsmA5Tvdo=39i9{nGPOQQz{xRjTmu^Ok-o5Ohxi-ofIF7_=GBZ)#fZIVB-P2gO|
z_KF^`iFRwmT~8qldc^P%kCvQRp(A3bJMCd^Yde}XP=b!bv*@}kt$-QY#~!FYTKw2>
z7c-eC@wpJ_S<DOYhVO*E^3F*+)5VaFaIu+*zXBebQc@Q=kKUkf`G{pobPS0{O`bg&
zLTc6EFW?`9nCx^Iv0znOXAXq}#26d~h!-=bUX~k&0y8!YJnQQD5SA^Ph#tz?qH797
zj1|0%%>Gt-fQgPnTfk3)<Dva#V6=<@6nl7M0b&2yb`FswTDc~?u5L8gQBP}+q^So{
z@PHL?k~dNa4T%T?Kj>ihEHn^s@rrV40}%WALR<V=FO7fVlGtvAvj<ij^PybB&)dR{
zI}xk4-}nrHNtzyEnj?PjwMktaT#bK>w_z$hX_B(qVm#~*syjG#7{8d^KkF44X1>M(
zk6UEl6PyUI6mMUS->{Iek-Ad~6?j$K)}H<N+hYd2X|H<6v*96436V#-Xd4CM$o|{!
zFx@LFE!k)p^p}`GJ<UHU+a!-qj8`>)1hx=@l9Dqkvl8TqUvNn&bz!VzOmEje>iQcu
zd4k{a;9&lSSiys#*D`d63g>+E*-0X0AQn18QjIWwSN~!!^G$r0p%tUo$;}?MHzDs_
zw{iok2KVJGdS?Pc%`-@5QMN|FL&5DX-u7vx$|)xmXZ=NcI#cuw1kn4y8h~b`eEK76
zV=tfcD(2O!wZ>%lqt{1s^z-b_H)>wYjaW>3-TPJft$B|Tj9v_^7|>%QqO)H<q7V+{
z;ju2+!wKZaAqrN(CZix@XHLb#?3aTG9E3=s(YNZOG)1&Pl%!fUE-qTDBO?Prbt5e%
zKiuRv8s<G(WPTK`fszj#v#Ssaz96?Y1c)RwKdUriX;ef>bYj#_@P~sjK-qB|y#TvN
zj{u!p6E&&#Al`fhsy4?8zBcf)Gmp9%f*hDCnP01NIDxG2U^L(?(3zOz)!>7*-wxg4
zFSI_jfR>e}!TJSd;kIR)<lyJJTC6`yK{*}-q(m^eTeXJ=nn^yzgpyNCfZN%G;L|{8
zQC`C9^v^5CdvS0H*rbc<neOJjS5=w!F13hK36n;_VshoNbTsUPCGrFPIu*Yz(@3*W
z6H6tkxaV-IlOAofSKNT5!|uEaNoJ|d%+s%xI_}=xw3Sqn&@$FNMZ&NB;X(QO31W8*
z`nSAIG>>Tz!tGH%^XUP$R~?t~t39;l*_ZA|F%bH5W#o98n6P?DD^PF7*r#=<AtsB_
zk`@B`$M62^2dI|E!s1<WH}80#Bb8P?rmZ77kp{IJ*=Qti<^opos|5BdY+%w`3<HBk
z7d#8_1gcdimcp2Hxsuvdd()HmYMXwUlz28Rfh;%-9F+vfiAyL&*NtLlanZp;hyv*y
zs@eX8@Xl(so?<7;h#qI8T|XD-d?C>J^|XAZ=y=E?gg!QaWF4w1;Jc>2?A!U<%z&MC
zGs)tWtUx}-dJ$YA$s4*#6pyW{oiYYc7Yq}MKw+<`C@f1=af&-6m~J$mdjtXb%{Eyh
z;NwS);XL<jI4*!2edQR(FlUL2n~We>S75+f$9~;mLSK;fhRdt}-1w(yPybjlNug)#
zi^ZSvL{WS*jUwOO=v*<SI5Qc1Rj<u6FRsoXPRT1&SX>kwQpKmq{(8?QeOfs$Ze`MH
z;6nau%R9^Y(|b`~b&rKG&p3Unt@iewQIW2qjZ3+p@8L|L0Ke)Bl$N`6Q>JFL8ys#k
zXr}s3>xc{aFMVNttHYpqQ4aOkn9npvasBmJDwy@Hp`=~P&%^IT-@l1@K@ff4JJuOF
z7$INbI1UMygUjpx?5>?BE}lO_DVrq~{HxHtWzHO@ei8DZ&DecTis{N&-$U>)q-w?^
zq9Ia5bK*`v6V4FZ?1blw4S}D}x*iR@uHU#*@^7!v&Xj7&-io7E%&2L7FQ{;O|L3Rm
z8p#)Y@dZAxwwA8VBvY&7&+{yPewR41DX=x2q9l<jW}AhyzTYW5492I`0dX}roseno
zmvXr@jn8_YT^+?#*uwG^OS5y|AK(Eo$?=~Oo><)P4|_%>bR$ZR1Ir3BZ4sLk)<ku0
zoK;qeH#wJwMpaROC{_c?7kLJWnZ2U7&VKG0i8+?5d{=H6x+}giil4%+cns5Q82##M
z(5N1z<f&8%gtHV@8k8mPxvT3H;tCP9OnP+u`SOjt$D!92fti5TnCPRAy@uyP>+jkN
z7<idP8y9+nU`MRTY`fqU6095w;ZpCkgM(tsV=ujvDGBV16vSnr)m!Jxb@n6$s~U85
zj3NW}Ix5~u9;k&0RurY3`&HEDt@6;3{fsI#FG0&ahH=ur1g1oa^Z~;q1PqsZC!)wV
z4w)o`^g!0(#F|WWBzl04=JKz<0o&L3liDD7@7ayduu0!=T96#gKJiBls7#f>D$+h!
zMxiQWFGUB34l}E3-*DP4{eq{%LG*e6q8FE~ZfxCs*Pe$_k{!IA6H*fv9VQR8hE*Oo
zT`K@IMAyhw{AZS3w=mh=-m@`vXIJZtQggWbW2roPW*Clagkb@<EsT${#RN*Q-Pca|
zEyjp@Nrrv|7NBsvJJ`*<%7F%zTrjQqH#}AQbCZr{=FMoXXO?Rzq|85kj~acwmgo~N
zLV$1he+hk)7?cj6B1NDLrXow)L^Ct@)IQh&9AZ6Jw$<jQ$sfWB%Am~55B_gDUnk>N
z1`vsH4tTF|Yg%H<NT_hX=8L^i1*7<k>(xZWLHf(sX&TabFbOOG6oSoRVM7A&VChE@
zK!DZ0v9qG0i{|EjwS>Srt0!*LlA@R01-gkJHBJl|j%rYv9iSkJAO*?z8YX=E7)Ix>
z0KER_U4V0l6^&lg7Ye|S{VmXbMbHzuKqkuXxpRR&Lv$C&K0l0x^E`xy%|=Wd_JG4f
zeJv|1_t7(j;C_J1YY*quq_7fpQM2lY@@_$qpr}h=Eq9$dxbU^Vlx{9QJezWlY1EZh
zK<hX-#$euvu|(dR80KNuiY<ZppsHwntykwH2hqBkAK*i{{G_|lPoYAfVQZm8%9y~3
z_u>IKsk8}L=7~EEI@RKd-<c}j%KBQPV0i<)gn^}l6&xks|2NF+`}X*hhn9}M*XMq|
z=ZdWjXXa@2PC6A6EC(|7x~VEU^)6%oK5njDn6L}n+D;Qz6zIdAzV5+UU}_-9V+EWn
zumjLS;4BogfB6egK?)kx^C)dE$&H-xI-qF)v%0eM0UVDRofdEqPXX>G`}qz45r7@<
zOB+DGD3v;-=NXhn4Kf3|uL)4!K4aG%1&BN4lVW;6i`E2w3B$R62mOEx;02AT=)Swa
z(@jY@Pa#{-#85CXs3!sVpZUxH@}I(>i^Vq?^h@VZkO9CBT>R%uQVxF4X!m-6CW*95
zlwu&b%?=5#!{(o(IPN(P1P27@DeFOy0b)fW(c+nhtsOql(Rkic=EBLk#z27<f63It
z{5X&VV#~Bc4$j>fdW~JZQWfSc)A(8SQ3kw|5nvt#{B2A|CLyY|GWcRPYF$^i5dt1$
zQ1FV^7r)rU_*-E2kMZS!213Ghr@uryU<}>qH<c$tXK=F5pyd5uRl)?BeXtJ#%yYfi
zwf(*v1uwJ43f1Q$9Wx}pPK#z@JKrI(*W3TAp9YF0e$6|h@N?3Y0q@$cvw!QXVKBL0
zcPx59?CViqj7JY!KuKl-b+YuerU#AEln<85!K==Bc?k!ndQ|mU6aWKY@GmMVf~^CZ
zH6qL~^KRP~^69>i-6&sz%!qrfNP3lnUSJBb0M-CvIk{k>Fks(G5QxbOV~8|3Vhj*c
zdTWE=Tg)B-pDR;d;DHRQN)sUXT3LAsLmmHHNi5h9w71nwh0b3jG}qwaS8fTwwhD}O
zzrffB6d5XEjY7N`_Cr=5pNUEay7>F?AwP8@Xu07ISN4uO%7J?~BB?(#T(v~DXwo>x
zu?g@#?|5r99Nd*WmgIPT<{Qw0G;xpC$=Ic}pWBLKG$@_>^l_P0@KJ6EDZ9rLCsl*e
zUyZLkE}m@vBO3BB4D%FyG~dfC>)_oILfUGko{!ikmf$y{d`+;th<#1GR|*k#aFSdR
z(sElzBW_0tQ095RLBwnmFBzFP7)lR1MiZ$<w`MJ{FT$oxF6(w?#}HOSRjIwu9|ryd
z-4~6xWf!{%=1K1+4ja8!N#*kHA$z`4h?>R%=i}xrvgFh;rU|PG#4~`ccxJ)VDN*e^
z-`{Uk@@%UCvR=KKI{?7rhZh#uSi^IJB7s8e5yn?e1ME>go{QhyAo_B|uUFT3jQ&mw
z4Of13ouHCL(N&Vj=K?*LdZUx$lP(h>XF_W?qy*&b&J};PKEC+PVmNMw&d^@4lp5`H
zwa!Ftrt0=#SAoScq5?BK)4+d^g6U#C(dRg9mAU3~;h0AMt`g>NEgPcEndwL)?L#E<
z>bIU`$>hmQ3&ODnvlIiB_SMx@X)r4HqTmfG=b4KT3c+oW%fm`@CLQA4#DbpzK85E+
z^IJW^Y8qS0>8D>fFQFD|<d9*f39(xKy^;nWTMeb{Y)PO(Io}XE!%#7|a5xxk*j?{F
zpSi5`kTWa<8k$f~CTsO1pv^w_Oqn$GQ6gm6jOOhW>Sn3CkcfPemZe*vY$MlGOXR!O
z-+ByOl21|H{9ekJ1uIQ}wr@)BIgvm0-dEr-x$Z4Mk2q{$m4cWJ7fdFie|vtsFK9nn
zJsr`zl#q<pX-SiAn!=TZv+;S1Y?t@gkj}8IjAu0n??%^#@JVJ7y~Q!TXb%jE5H2Ss
zDS-R?Ju(_>v-ZGozPyF`n+EwA-Tjen@&OJxT)<?}(7{0sP>mN{R$D9j29QGqk-<<4
zfSHYheW_U5w7djE*gGF+8~~XJ<?)zJpsf;vDhmT*XGH<%p`a3M<-zi-3hYr~IU_)z
zIbZ>E7Lfc<iK-TxdM}OreWGu3f&k+8{vVQYD3qvE_&;Yd->crbZul?(!2g5OR!~s(
zfSK$cIq+08g0R2$o_Pj1z&uu3AW}P400JC5kX7Irzv`T{h!ULc*P-MfdJX_Oa7*(4
z(gi&PEjG|76O1cMgIpsn5U#d||6;NVw{g(Zt`D3i1^@yBvy!HW-F&p$Q!wL$T9s(i
zrp|3<a5QNO!qF(0(!iXSk(t|fDN9HqK}s`dwylRi3jO1Ik3~nYD}ssU{zZQGw(q_F
z)Cp5QlcT$hLl2odX%C|XAUL6?+<|Xo4vqG%8-NU${aFd3V#R350t2%RNI2ou<me;H
zsZW8t6deDxJ_>asT4Y$psunC#)k^^{4DpLa3utwz^hGS)O3gEHQmidu=tNX&rc{71
zen9}7MwW6yJ_Wzf5PXIi`#p;St>S~TrVMcbFp6vM`0_!fmGWw@z(tKheHnY<6RD@6
zlxX1907MM(7=Z`>O*ss&P`rb-?<<fS=nv;@w3s_ZOr)RTAh6Ct6Gxl9PDc2rm>;R5
z&8Yxv(ae%OgO?M^j56~hLNyLcC{kZ84vDCPjx&S58r~Oo?4yLyw@wj!N`|xDsnZ+z
zp=|Z4s>Zjk9`F6?c-)cdcc09@pz8!zjtdkDAD%42bGJ<H?2MDTFYn!oEi)4IcF&Qk
zVxqs!U{%cEX%B`m#3=lQN+a`3YD0gei_+z}^`mg~1|VoB0JV#7@;Fw9Ph$6`5=BtE
zt<kfXNh<t-OZMo+T)$hl(2Jur{Je)ZiS~$Z^A#>M#6%n)%aMXM!oZ}(?AOC+u|$f$
z3+y=+w+QdveTz<8pt6#t2Ejm6Q|3NdK(J+dx4?&<`5vIM2Wca`6D{PLhnW6se1-zq
zhYRpuf+5@c5|~W_A*$aP)E0T+dKEGTkbiPjDihfJvMQhjqh}Ti2-+Kc@LRw#`XWF=
z^2z`rqqsNzgZ#04`t`YPZGpl6iIi(T@8dO97DyszkK{TzY$l(8iJwVCK%I<}K+RrS
z=sKh8p6_RI>h;uY*N|Y|^}P*gsqt3k2h_q+rQ0A=pDh9@NEbq<;(6Zm#Gp{${?M11
z?BvxVQLtI=hu#pvZ~u#&X!q*^Eo3nJHQ|B+?)u*7Vz0BYK!(XWd9LB~s8HX6WefSg
zW(96|Za3yTJgkz7jBMb{tm_lH-=wwFR|ldEFb{Aj0I_2yJ3_e4Af^>xv0u+%n$CW>
zFZ2KU1x*?uht<a)vxm-V@Nr1I__x2PQHK#Mq$Py%IG~B~?dUjx{hQV9{g-ue@z<_O
zH3lf8ygSqr9j?rMsTlCg$Bfh0?dGpQ$k8p2$o8*2RA163P5cxHgufpf8Xe*3|G&_Y
z`59z6a#)3)S%(jTx<340-r0<(o$vUzDG}O`#Bx>45?2C48Qe#Q<!fVr%5!rnvrD4(
zc^uh^)R^MuYrRnCOkB!cluRef-Ban3qF>@JFI8)qynL=i+UQxqEg~)b5OD5)JGB$5
z)D``Ip4v9dp<!tSE75Crzjdp->*{6ZyP9D6KPRf+f8!S0b$;GkA*rb>Y43@%#HPE%
z_^;~6!R(P~pz8OZ8UT+8<bjy&uFa~}X`M=XL}T2d9jBWWUG$<VI+7GYb@e~b?Es~J
z>#VuWqL!%+|De8xYsF;S%zYH|2Xyklz$(XWss0sNEqS!``>w-=F*Su@)F-beXO)~!
zMRnZ2cfaB1Y_ykEposi8*a6ZlU^{qVpzuOU-^Z4H)y4qXMM*8tx$}F;dklB%Y`(%X
zJcuN>PPG|*fB?fk00{r3jZ1+m0rp;|jqSS^i=hW=r<3HXGAbedr8G0QrM?;UQBgE9
z?k`c0HxM(#9;1s$vTRDSsYJriar2n1pT?*?Yl-ty6ZYgrXUNs{)&;sZ05TkIbzjSN
z1f%T0nYG@KdNgcp+_HXG0@KvMtVO(BuE82$D5{|!0~-w1hN&H$h%vi&^diKAPwh$R
z1@r!TuQjX}XlRCuxNhiA?b>)N>+8pl*$tyORvIB-*?Ci^oB`;8+9Z;r-UCBaWdV}F
zq?0Kv72wy@TL6G4vAuhR&R?9sHUtE_0WBE+a9C|OC9U3UGPMm|OujI@S;hj-h4e=4
zo0TD<qa_`^SS>BmRj|TKeF|(v0Q$JPcYCES8eQ*-cdC%v&AXOlG@h;e+E|J4^cAHP
zYCh@NuvGZ5H7Kl+MlRi?bB!^synm$#o6S7U?LKAY*5qWlhVig$B}iR```a7h9Ndv;
zXiHeoqLv^|DZc0DM^E^PQBX@~IL{`uyc6NB(EYaQImaib^y1vN9HyIv)z#jXSDpJ2
zUgwW>3%^W#?|f4SI)WHbCsdGpyu7xVKa1fFT~-xpcV73p`S^P6H8(mh$z&{LMPV|h
zYGMABgLI?;*=eX<?pugdKBsM_7E>Ha?VomErm4n7jlmp+k?)TE-QTqygD2RE{DhGN
zod}UhEPoOL{bydqut7B|d-?6IU+JxGr-#0@tR#0nk^wuq=@2U|1SVjKtYFA98SXwb
z`J+V|8avO_<6E1tJfT%<>AUA+qy84ZVKyu46cBo<qWo3{0U_Anv2n)1M*j7Y>~|R{
zC+oCUyx4^WQC9-F%}b-Xzwm!^SE{=2ZkY~oxnv5p0m8sC;U`Jtr!IutcF7faLeF|-
zEz{V_h?wiHuLVu*nJ_KTo~x<{N1q@?V4`sipm6Za>I^tOm_ELP;(0Ewu|*-H#!+yw
z6zE$XuoDb5LmE5*8vVpbobBp#0Q)8#bssWNSR#3;{x+hw>sL^?u*!a;0*0_Z9p=DI
zWi)|l3c{MZmcLh83LLG`0ls<TU!nV`t(O2DD_{Q+is!<fZPMeTn|pnAek<mXxe{2K
zp%sEj5*zR&Aiov>IcKPh1Ju)3CVAgDUk^w$6bIw#Li`Rj>9>S?<%5FrID?o3dYsoa
zfTPY$hc_lHAAMUsCVS=Vfe#1Al9uke-h*tD*^6HW-OwwC0hQ69ivF-lRWYsTQ=q~G
zNSz@ySS`f~gp8Y)!`(B`N8Y5HaKYf^UBOdD+YtyUc&o&6j0TuIxX5=9LJrfX1y4V!
z-C2pX&>(>>wB9v0H-9A}`eXKkQFzE>0aL&7{<kuROyAfVM}2&eNn*$6y`8?FA|mt}
z_D>~(a>4@e=ngMfUf352memUOEK~9#eq7ODd4Tn)wLWk(>2F8+I+*`ZxR*@o^)ocS
VQTNV)|9pp`DECaZ;K}oM{|_>%Lw5iG

literal 0
HcmV?d00001

diff --git a/ar/assignments/src/2.py b/ar/assignments/src/2.py
index 2b5ed99..e5852e6 100644
--- a/ar/assignments/src/2.py
+++ b/ar/assignments/src/2.py
@@ -1,5 +1,4 @@
 #!/usr/bin/env python3
-
 pc = [(4, 2), (4, 2), (4, 2)]
 rc = [(9, 7), (12, 6), (10, 7), (18, 5), (20, 4), (10, 6), (8, 6), (10, 8)]
 mx = 29
@@ -19,7 +18,6 @@ for i, (w, h) in enumerate(pc+rc, 1):
     print("(c{:02d}h Int)".format(i))
 print(")")
 
-# Preamble2
 print(":formula")
 print("(and")
 
@@ -27,67 +25,47 @@ print("(and")
 for i, (w, h) in enumerate(pc+rc, 1):
     # Print the width and height
     print((
-        '\t(or '
+        '(or '
         '(and (= c{0:02d}w {1}) (= c{0:02d}h {2})) '
-        '(and (= c{0:02d}w {2}) (= c{0:02d}h {1}))'
-        ')').format(i, w-1, h-1))
+        '(and (= c{0:02d}w {2}) (= c{0:02d}h {1})))').format(i, w-1, h-1))
 
-    # Print the bounds of the coordinates
+ # Print the bounds of the coordinates
     print((
-        '\t(> c{0:02d}x 0) (> c{0:02d}y 0)\n'
-        '\t(<= (+ c{0:02d}x c{0:02d}w) {1}) (<= (+ c{0:02d}y c{0:02d}h) {2})\n'
-        ).format(i, mx, my))
+         '(> c{0:02d}x 0) (> c{0:02d}y 0)'
+         '(<= (+ c{0:02d}x c{0:02d}w) {1}) (<= (+ c{0:02d}y c{0:02d}h) {2})'
+         ).format(i, mx, my))
 
-    # Print the non overlap with others
+ # Print the non overlap with others
     for j in range(1, 1+len(pc+rc)):
         if i != j:
             print((
-                '\t(or \n'
-                '\t\t(> c{0:02d}x (+ c{1:02d}x c{1:02d}w)) '
-                '(< (+ c{0:02d}x c{0:02d}w) c{1:02d}x)\n'
-                '\t\t(> c{0:02d}y (+ c{1:02d}y c{1:02d}h)) '
-                '(< (+ c{0:02d}y c{0:02d}h) c{1:02d}y)'
-                ')').format(i, j))
+                 '(or '
+                 '(> c{0:02d}x (+ c{1:02d}x c{1:02d}w)) (< (+ c{0:02d}x c{0:02d}w) c{1:02d}x) '
+                 '(> c{0:02d}y (+ c{1:02d}y c{1:02d}h)) (< (+ c{0:02d}y c{0:02d}h) c{1:02d}y)'
+                 ')').format(i, j))
 
-# Print the PC distance to eachother
+         # Print the PC distance to eachother
 for i, _ in enumerate(pc, 1):
     for j, _ in enumerate(pc, 1):
         if i != j:
             print((
-                '\t(or \n'
-                '\t\t(> \n'
-                '\t\t\t(- \n'
-                '\t\t\t\t(+ \n'
-                '\t\t\t\t\tc{0:02d}x \n'
-                '\t\t\t\t\t(/ c{0:02d}w 2) \n'
-                '\t\t\t\t) \n'
-                '\t\t\t\t(+ \n'
-                '\t\t\t\t\tc{1:02d}x \n'
-                '\t\t\t\t\t(/ c{1:02d}w 2) \n'
-                '\t\t\t\t) \n'
-                '\t\t\t) \n'
-                '\t\t\t{2} \n'
-                '\t\t)\n'
-                '\t\t(> (- (+ c{1:02d}x (/ c{1:02d}w 2)) '
-                '(+ c{0:02d}x (/ c{0:02d}w 2))) {2})\n'
-                '\t\t(> (- (+ c{0:02d}y (/ c{0:02d}h 2)) '
-                '(+ c{1:02d}y (/ c{1:02d}h 2))) {2})\n'
-                '\t\t(> (- (+ c{1:02d}y (/ c{1:02d}h 2)) '
-                '(+ c{0:02d}y (/ c{0:02d}h 2))) {2})'
+                '(or '
+                '(> (- (+ c{0:02d}x (/ c{0:02d}w 2) ) (+ c{1:02d}x (/ c{1:02d}w 2) ) ) {2} ) '
+                '(> (- (+ c{1:02d}x (/ c{1:02d}w 2)) (+ c{0:02d}x (/ c{0:02d}w 2))) {2}) '
+                '(> (- (+ c{0:02d}y (/ c{0:02d}h 2)) (+ c{1:02d}y (/ c{1:02d}h 2))) {2}) '
+                '(> (- (+ c{1:02d}y (/ c{1:02d}h 2)) (+ c{0:02d}y (/ c{0:02d}h 2))) {2})'
                 ')').format(i, j, pd))
 
-# Print the constraint that they have to be connected to a ps
+            # Print the constraint that they have to be connected to a ps
 for i, _ in enumerate(rc, 1+len(pc)):
-    print('\t(or')
+    print('(or')
     for j, _ in enumerate(pc, 1):
         print((
-            '\t(not (or \n'
-            '\t\t(> c{0:02d}x (+ c{1:02d}x 1 c{1:02d}w)) '
-            '(< (+ c{0:02d}x c{0:02d}w) (- c{1:02d}x 1))\n'
-            '\t\t(> c{0:02d}y (+ c{1:02d}y 1 c{1:02d}h)) '
-            '(< (+ c{0:02d}y c{0:02d}h) (- c{1:02d}y 1))'
+            '(not (or '
+            '(> c{0:02d}x (+ c{1:02d}x 1 c{1:02d}w)) (< (+ c{0:02d}x c{0:02d}w) (- c{1:02d}x 1)) '
+            '(> c{0:02d}y (+ c{1:02d}y 1 c{1:02d}h)) (< (+ c{0:02d}y c{0:02d}h) (- c{1:02d}y 1))'
             '))').format(i, j))
-    print('\t)')
+    print(')')
 
 # Close the and,benchmark parenthesis
 print("))")
-- 
2.20.1