Proof that setof is one-to-one

weight_list(pick_and_purge).
weight(x,1000).
weight(noteq(bad1,bad2),1).
weight(a(setof,bad1),1).
weight(a(setof,bad2),1).
end_of_list.

-----> EMPTY CLAUSE at  49.38 sec ----> 4119 [para_into,785.1.1,35.2.1,demod,3,2,unit_del,74,8] $F.

Length of proof is 7.  Level of proof is 4.

Proof

2 [reference] p1 pair(x,y)=x.
3 [reference] p2 pair(x,y)=y.
8 [reference] x=x.
15 [reference] x!=y|eq pair(x,y) =p1.
16 [reference] x=y|eq pair(x,y) =p2.
17 [reference] x=y|x noteq(x,y) !=y noteq(x,y).
18 [reference] p1!=p2.
34 [reference] setof xf pair(x,y)=p2|xf x =y.
35 [reference] p2 xy!=xf (p1 xy) |setof xf xy =p1.
38 [assumption to refute] setof bad1=setof bad2.
39 [assumption to refute] bad1!=bad2.
41,40 [ur,38,15] eq pair(setof bad1,setof bad2)=p1.
56 [ur,39,17,flip.1] bad2 noteq(bad1,bad2)!=bad1 noteq(bad1,bad2).
71 [para_into,40.1.1,16.2.1,flip.2] p2=p1|setof bad2 =setof bad1.
74 [para_from,40.1.2,18.1.1,demod,41,flip.1] p2!=p1.
94 [ur,71,74] setof bad2=setof bad1.
97 [ur,56,34] setof bad2 pair(noteq(bad1,bad2),bad1 noteq(bad1,bad2))=p2.
785 [para_into,97.1.1.1,94.1.1] setof bad1 pair(noteq(bad1,bad2),bad1 noteq(bad1,bad2))=p2.
4119 [para_into,785.1.1,35.2.1,demod,3,2,unit_del,74,8] $F.