a(a(notp1,x),y) = p1 | a(a(notp1,x),y) = p2. ----> UNIT CONFLICT at 0.07 sec ----> 58 [binary,56.1,27.1] $F. Length of proof is 2. Level of proof is 2.
23 [reference] x y=p1|notp1 x y =p1. 24 [reference] x y!=p1|notp1 x y =p2. 26 [assumption to refute] notp1 bad1 bad2!=p1. 27 [assumption to refute] notp1 bad1 bad2!=p2. 28 [ur,26,23] bad1 bad2=p1. 56 [ur,28,24] notp1 bad1 bad2=p2. 58 [binary,56.1,27.1] $F.
up | previous | next | detailed contents | brief contents | OTTER output file