Proof that s is a subset of closure pair(s, f)

----> UNIT CONFLICT at   4.22 sec ----> 629 [binary,627.1,19.1] $F.

Length of proof is 12.  Level of proof is 6.

Proof

1 [reference] k(x) y=x.
2 [reference] p1 pair(x,y)=x.
3 [reference] p2 pair(x,y)=y.
4 [reference] pair(x,y) z=pair(x z,y z).
5 [reference] pair(p1 x,p2 x)=x.
6 [reference] abst x y z=x k(z) (y z).
16 [reference] x=y|eq pair(x,y) =p2.
19 [reference] p2!=p1.
48 [reference] charq eq=p1.
51 [reference] abst k(x) k(y)=k(x y).
52 [reference] pair(x1,y1)!=pair(x2,y2)|x1=x2.
60 [reference] subset pair(x1,x2)=p2|x1 xc !=p1|x2 xc =p1.
64 [reference] subset x=p1|p1 x notsub(p1 x,p2 x) =p1.
65 [reference] subset x=p1|p2 x notsub(p1 x,p2 x) !=p1.
70 [reference] subset pair(z,kintersection x y)=p1|x notinint(x,notsub(z,kintersection x y)) =p1.
71 [reference] subset pair(z,kintersection x y)=p1|subset pair(z,notinint(x,notsub(z,kintersection x y))) =p2.
72 [reference] closure=abst (abst k(kintersection) (abst k(abst k(eq)) pair(k(k(pair(p1,p1))),pair(abst k(abst k(subset)) pair(abst k(p1),k(pair(p1,p2))),abst k(abst k(closedunder)) pair(k(pair(p1,p2)),abst k(p2)))))) pair(p1,p2).
73 [assumption to refute] p.
74 [assumption to refute] -p|subset pair(bads,closure pair(bads,badf)) !=p1.
75 [ur,74,73,demod,72,6,6,1,6,1,4,1,4,6,1,4,51,2,1,6,1,4,1,51,3,4,2,3] subset pair(bads,kintersection (abst k(eq) pair(k(pair(p1,p1)),pair(abst k(subset) pair(k(bads),pair(p1,p2)),abst k(closedunder) pair(pair(p1,p2),k(badf))))) pair(bads,badf))!=p1.
77,76 [ur,75,71] subset pair(bads,notinint(abst k(eq) pair(k(pair(p1,p1)),pair(abst k(subset) pair(k(bads),pair(p1,p2)),abst k(closedunder) pair(pair(p1,p2),k(badf)))),notsub(bads,kintersection (abst k(eq) pair(k(pair(p1,p1)),pair(abst k(subset) pair(k(bads),pair(p1,p2)),abst k(closedunder) pair(pair(p1,p2),k(badf))))) pair(bads,badf))))=p2.
78 [ur,75,70,demod,6,1,4,1,4,6,1,4,1,4,5,77,6,1,4,4,5,1] eq pair(pair(p1,p1),pair(p2,closedunder pair(notinint(abst k(eq) pair(k(pair(p1,p1)),pair(abst k(subset) pair(k(bads),pair(p1,p2)),abst k(closedunder) pair(pair(p1,p2),k(badf)))),notsub(bads,kintersection (abst k(eq) pair(k(pair(p1,p1)),pair(abst k(subset) pair(k(bads),pair(p1,p2)),abst k(closedunder) pair(pair(p1,p2),k(badf))))) pair(bads,badf))),badf)))=p1.
80 [ur,75,65,demod,3,2,3] kintersection (abst k(eq) pair(k(pair(p1,p1)),pair(abst k(subset) pair(k(bads),pair(p1,p2)),abst k(closedunder) pair(pair(p1,p2),k(badf))))) pair(bads,badf) notsub(bads,kintersection (abst k(eq) pair(k(pair(p1,p1)),pair(abst k(subset) pair(k(bads),pair(p1,p2)),abst k(closedunder) pair(pair(p1,p2),k(badf))))) pair(bads,badf))!=p1.
81 [ur,75,64,demod,2,2,3] bads notsub(bads,kintersection (abst k(eq) pair(k(pair(p1,p1)),pair(abst k(subset) pair(k(bads),pair(p1,p2)),abst k(closedunder) pair(pair(p1,p2),k(badf))))) pair(bads,badf))=p1.
113 [para_into,75.1.2,48.1.2] subset pair(bads,kintersection (abst k(eq) pair(k(pair(p1,p1)),pair(abst k(subset) pair(k(bads),pair(p1,p2)),abst k(closedunder) pair(pair(p1,p2),k(badf))))) pair(bads,badf))!=charq eq.
213 [ur,113,52] pair(subset pair(bads,kintersection (abst k(eq) pair(k(pair(p1,p1)),pair(abst k(subset) pair(k(bads),pair(p1,p2)),abst k(closedunder) pair(pair(p1,p2),k(badf))))) pair(bads,badf)),x)!=pair(charq eq,y).
240 [para_into,78.1.1.2.1.1,48.1.2] eq pair(pair(charq eq,p1),pair(p2,closedunder pair(notinint(abst k(eq) pair(k(pair(p1,p1)),pair(abst k(subset) pair(k(bads),pair(p1,p2)),abst k(closedunder) pair(pair(p1,p2),k(badf)))),notsub(bads,kintersection (abst k(eq) pair(k(pair(p1,p1)),pair(abst k(subset) pair(k(bads),pair(p1,p2)),abst k(closedunder) pair(pair(p1,p2),k(badf))))) pair(bads,badf))),badf)))=p1.
355,354 [ur,80,60,81] subset pair(bads,kintersection (abst k(eq) pair(k(pair(p1,p1)),pair(abst k(subset) pair(k(bads),pair(p1,p2)),abst k(closedunder) pair(pair(p1,p2),k(badf))))) pair(bads,badf))=p2.
395 [back_demod,213,demod,355,flip.1] pair(charq eq,x)!=pair(p2,y).
626,625 [ur,395,16] eq pair(pair(charq eq,x),pair(p2,y))=p2.
627 [back_demod,240,demod,626] p2=p1.
629 [binary,627.1,19.1] $F.