#!/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,time,random
n=112;ys={};cs=[[1]];F={s:[] for s in range(2,2*n+1)}
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=n+len(ys)+1;ys[u,v]=z;F[s].append(z);cs.extend(([-z,u],[-z,v]))
C={s:[] for s in range(2,113)}
for a in range(1,n+1):
 for b in range(a,n+1):
  s=a+b
  if s<113:C[s].append([-a,-b]+([s] if s<=n else [])+F[s])
CS=[[-a,-(113-a)] for a in range(1,57)];c=list(C)
def unsat(R):return pc.solve(cs+CS+[v for s in R for v in C[s]])=='UNSAT'
print('start',unsat(c),flush=True)
t=time.time()
for s in c[:]:
 if unsat([x for x in c if x!=s]):c.remove(s)
print('core',len(c),c,'secs',round(time.time()-t,2),flush=True)
PY