a(isp1,a(notp1,x)) = a(notp1,x). ----> UNIT CONFLICT at 0.10 sec ----> 57 [binary,56.1,25.1] $F. Length of proof is 2. Level of proof is 2.
24 [reference] notp1 (notp1 x)=isp1 x. 25 [reference] notp1 (isp1 x)=notp1 x. 26 [assumption to refute] isp1 (notp1 bad)!=notp1 bad. 31 [para_into,26.1.1,24.1.2] notp1 (notp1 (notp1 bad))!=notp1 bad. 56 [para_into,31.1.1.2,24.1.1] notp1 (isp1 bad)!=notp1 bad. 57 [binary,56.1,25.1] $F.
up | previous | next | detailed contents | brief contents | OTTER output file