a(x,y) = p1 | a(a(notp1,x),y) = p1. ----> UNIT CONFLICT at 0.07 sec ----> 40 [binary,39.1,8.1] $F. Length of proof is 2. Level of proof is 2.
1 [reference] k(x) y=x. 4 [reference] pair(x,y) z=pair(x z,y z). 6 [reference] abst x y z=x k(z) (y z). 7 [reference] eq pair(x,x)=p1. 8 [reference] x=x. 20 [reference] x y=p1|isp1 x y =p2. 23 [reference] notp1=abst k(abst k(eq)) pair(k(k(p2)),isp1). 24 [assumption to refute] bad1 bad2!=p1. 25 [assumption to refute] notp1 bad1 bad2!=p1. 27,26 [ur,24,20] isp1 bad1 bad2=p2. 39 [para_into,25.1.1.1.1,23.1.1,demod,6,1,4,1,6,1,4,1,27,7] p1!=p1. 40 [binary,39.1,8.1] $F.
up | previous | next | detailed contents | brief contents | OTTER output file