Proof of converse defining property for kintersecton

-----> EMPTY CLAUSE at  77.87 sec ----> 5815 [para_into,5716.1.1,22.2.1,unit_del,19,5750] $ans(noteq(abst k(eq) pair(k(pair(p1,k(p2))),pair(badf,abst (abst k(abst) (abst k(isp1))) k(k(badx)))),k(p2))).

Length of proof is 8.  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).
8 [reference] x=x.
9 [reference] k(x) y=x.
17 [reference] x=y|x noteq(x,y) !=y noteq(x,y).
19 [reference] p2!=p1.
20 [reference] p1 x!=p2 x |eq x =p1.
21 [reference] p1 x=p2 x |eq x =p2.
22 [reference] x y!=p1|isp1 x y =p1.
51 [reference] abst k(x) k(y)=k(x y).
52 [reference] pair(x1,y1)!=pair(x2,y2)|x1=x2.
53 [reference] pair(x1,y1)!=pair(x2,y2)|y1=y2.
54 [reference] kintersection=abst (abst k(abst) (abst k(abst k(abst)) (abst (abst k(abst) (abst k(abst k(abst)) (abst k(abst k(abst k(eq))) pair(k(k(k(k(p2)))),abst k(abst k(abst k(abst k(eq)))) pair(k(k(k(k(pair(p1,k(p2)))))),pair(pair(p1,p2),k(k(abst (abst k(abst) (abst k(isp1))))))))))) k(k(k(pair(p1,p2))))))) k(k(k(pair(p1,p2)))).
56 [assumption to refute] p.
57 [assumption to refute] badf z!=p1|z badx =p1|$ans(z).
58 [assumption to refute] -p|kintersection badf bady badx !=p1.
59 [ur,58,56,demod,54,6,6,1,6,1,6,6,1,6,1,6,1,4,1,6,1,4,1,4,4,5,1,1,1,6,6,1,6,6,1,6,1,4,1,6,1,4,1,4,1,1,1,1,6,6,6,1,4,1,6,1,4,1,4,1,1,1] eq pair(k(p2),abst k(eq) pair(k(pair(p1,k(p2))),pair(badf,abst (abst k(abst) (abst k(isp1))) k(k(badx))))) pair(p1,p2) pair(p1,p2)!=p1.
78 [para_into,59.1.1.1.1,20.2.1,demod,2,2,2,3,unit_del,8,flip.1] abst k(eq) pair(k(pair(p1,k(p2))),pair(badf,abst (abst k(abst) (abst k(isp1))) k(k(badx))))!=k(p2).
109 [ur,78,17,demod,6,1,4,1,4,6,6,1,51,1,51,1] eq pair(pair(p1,k(p2)),pair(badf noteq(abst k(eq) pair(k(pair(p1,k(p2))),pair(badf,abst (abst k(abst) (abst k(isp1))) k(k(badx)))),k(p2)),k(isp1 noteq(abst k(eq) pair(k(pair(p1,k(p2))),pair(badf,abst (abst k(abst) (abst k(isp1))) k(k(badx)))),k(p2)) badx)))!=p2.
376 [ur,109,21,demod,2,3,flip.1] pair(badf noteq(abst k(eq) pair(k(pair(p1,k(p2))),pair(badf,abst (abst k(abst) (abst k(isp1))) k(k(badx)))),k(p2)),k(isp1 noteq(abst k(eq) pair(k(pair(p1,k(p2))),pair(badf,abst (abst k(abst) (abst k(isp1))) k(k(badx)))),k(p2)) badx))=pair(p1,k(p2)).
5612 [ur,376,53] k(isp1 noteq(abst k(eq) pair(k(pair(p1,k(p2))),pair(badf,abst (abst k(abst) (abst k(isp1))) k(k(badx)))),k(p2)) badx)=k(p2).
5613 [ur,376,52] badf noteq(abst k(eq) pair(k(pair(p1,k(p2))),pair(badf,abst (abst k(abst) (abst k(isp1))) k(k(badx)))),k(p2))=p1.
5716 [para_from,5612.1.1,9.1.1.1,demod,1,flip.1] isp1 noteq(abst k(eq) pair(k(pair(p1,k(p2))),pair(badf,abst (abst k(abst) (abst k(isp1))) k(k(badx)))),k(p2)) badx=p2.
5750 [ur,5613,57] noteq(abst k(eq) pair(k(pair(p1,k(p2))),pair(badf,abst (abst k(abst) (abst k(isp1))) k(k(badx)))),k(p2)) badx=p1|$ans(noteq(abst k(eq) pair(k(pair(p1,k(p2))),pair(badf,abst (abst k(abst) (abst k(isp1))) k(k(badx)))),k(p2))).
5815 [para_into,5716.1.1,22.2.1,unit_del,19,5750] $ans(noteq(abst k(eq) pair(k(pair(p1,k(p2))),pair(badf,abst (abst k(abst) (abst k(isp1))) k(k(badx)))),k(p2))).