a(notp1,x) != x. ----> UNIT CONFLICT at 0.06 sec ----> 47 [binary,46.1,8.1] $F. Length of proof is 4. Level of proof is 3.
8 [reference] x=x. 18 [reference] p1!=p2. 23 [reference] x y=p1|notp1 x y =p1. 24 [reference] x y!=p1|notp1 x y =p2. 25 [assumption to refute] notp1 bad=bad. 32 [para_from,25.1.1,24.2.1.1] bad x!=p1|bad x =p2. 34,33 [para_from,25.1.1,23.2.1.1] bad x=p1. 41,40 [back_demod,32,demod,34,34,unit_del,8,flip.1] p2=p1. 46 [back_demod,18,demod,41] p1!=p1. 47 [binary,46.1,8.1] $F.
up | previous | next | detailed contents | brief contents | OTTER output file