Proof of a(a(abst,k(x)),k(y)) = k(a(x,y)).

----> UNIT CONFLICT at   0.17 sec ----> 55 [binary,54.1,8.1] $F.

Length of proof is 1.  Level of proof is 1.

Proof

1 [reference] k(x) y=x.
6 [reference] abst x y z=x k(z) (y z).
8 [reference] x=x.
17 [reference] x=y|x noteq(x,y) !=y noteq(x,y).
50 [assumption to refute] abst k(badx) k(bady)!=k(badx bady).
54 [ur,50,17,demod,6,1,1,1] badx bady!=badx bady.
55 [binary,54.1,8.1] $F.