subset ----> UNIT CONFLICT at 0.20 sec ----> 101 [binary,99.1,60.1] $F. Length of proof is 1. Level of proof is 1.
5 [reference] pair(p1 x,p2 x)=x. 57 [reference] subset pair(x1,x2)=p2|x1 xc !=p1|x2 xc =p1. 60 [assumption to refute] subset bad!=p2. 61 [assumption to refute] p1 bad badc=p1. 62 [assumption to refute] p2 bad badc!=p1. 99 [ur,62,57,61,demod,5] subset bad=p2. 101 [binary,99.1,60.1] $F.