Proof of pair(x1,y1) != pair(x2,y2) | x1 = x2.

----> UNIT CONFLICT at   0.98 sec ----> 63 [binary,62.1,8.1] $F.

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

Proof

2 [reference] p1 pair(x,y)=x.
3 [reference] p2 pair(x,y)=y.
8 [reference] x=x.
10 [reference] p1 pair(x,y)=x.
11 [reference] p2 pair(x,y)=y.
52 [assumption to refute] pair(bad1,bad2)=pair(bad3,bad4).
53 [assumption to refute] bad1!=bad3.
59,58 [para_from,52.1.1,11.1.1.2,demod,3] bad4=bad2.
61,60 [para_from,52.1.1,10.1.1.2,demod,59,2] bad3=bad1.
62 [back_demod,53,demod,61] bad1!=bad1.
63 [binary,62.1,8.1] $F.