#!/bin/sh
fetch -q -o /tmp/p.tgz https://files.pythonhosted.org/packages/source/p/pycosat/pycosat-0.6.6.tar.gz;tar -xzf /tmp/p.tgz -C /tmp;cd /tmp/pycosat-0.6.6;python3 setup.py build -q >/dev/null 2>/dev/null;PYTHONPATH=$(echo build/lib.*) python3 - <<'PY'
import pycosat as pc,math
n=112;C=[[1]];F=[[] for i in range(2*n+1)];z=n
for u in range(2,n+1):
 for v in range(u,n+1):
  s=u*v
  if s>2*n:break
  if u==v:F[s].append(u)
  else:
   z+=1;F[s].append(z);C.extend(([-z,u],[-z,v]))
C.extend([-a,-(113-a)] for a in range(1,57))
for s in range(2,225):
 for a in range(1,min(n,s//2)+1):
  b=s-a
  if b<=n:C.append([-a,-b]+([s] if s<=n else [])+F[s])
 if s in [12,20,30,40,50,60,70,80,90,100,108,109,110,112,114]:
  R=pc.solve(C+[[-i] for i in [109]]); T=pc.solve(C+[[-i] for i in [103]]); P=pc.solve(C+[[i] for i in [4]])
  print(s,'overall',pc.solve(C)=='UNSAT','forced109',R=='UNSAT','forced103',T=='UNSAT','exclude4',P=='UNSAT',flush=True)
PY