Proof of pushset Lemma 3

-----> EMPTY CLAUSE at 558.66 sec ----> 10196 [back_demod,398,demod,10187,10187,unit_del,12,23] $F.

Length of proof is 4.  Level of proof is 3.

Proof

12 [reference] x=x.
21 [reference] x=y|x noteq(x,y) !=y noteq(x,y).
23 [reference] p2!=p1.
79 [reference] closure x y=p1|closure x y =p2.
101 [reference] closure pair(notp1 charq,push) x=p2|closure pair(notp1 charq,setof) x =p1.
102 [reference] closure pair(notp1 charq,push) x=p1|closure pair(notp1 charq,setof) x =p2.
103 [assumption to refute] closure pair(notp1 charq,push)!=closure pair(notp1 charq,setof).
110 [ur,103,21,flip.1] closure pair(notp1 charq,setof) noteq(closure pair(notp1 charq,push),closure pair(notp1 charq,setof))!=closure pair(notp1 charq,push) noteq(closure pair(notp1 charq,push),closure pair(notp1 charq,setof)).
397 [para_into,110.1.1,102.2.1,flip.1] closure pair(notp1 charq,push) noteq(closure pair(notp1 charq,push),closure pair(notp1 charq,setof))!=p2|closure pair(notp1 charq,push) noteq(closure pair(notp1 charq,push),closure pair(notp1 charq,setof)) =p1.
398 [para_into,110.1.1,101.2.1,flip.1] closure pair(notp1 charq,push) noteq(closure pair(notp1 charq,push),closure pair(notp1 charq,setof))!=p1|closure pair(notp1 charq,push) noteq(closure pair(notp1 charq,push),closure pair(notp1 charq,setof)) =p2.
10187,10186 [para_into,397.1.1,79.2.1,unit_del,12] closure pair(notp1 charq,push) noteq(closure pair(notp1 charq,push),closure pair(notp1 charq,setof))=p1.
10196 [back_demod,398,demod,10187,10187,unit_del,12,23] $F.