f is a characteristic function, then charq f = p1 ----> UNIT CONFLICT at 66.78 sec ----> 5520 [binary,5519.1,4556.1] $ans(noteq(isp1 badf,badf)). Length of proof is 8. Level of proof is 6.
1 [reference] k(x) y=x. 4 [reference] pair(x,y) z=pair(x z,y z). 5 [reference] pair(p1 x,p2 x)=x. 6 [reference] abst x y z=x k(z) (y z). 15 [reference] x!=y|eq pair(x,y) =p1. 16 [reference] x=y|eq pair(x,y) =p2. 17 [reference] x=y|x noteq(x,y) !=y noteq(x,y). 19 [reference] x y!=p1|isp1 x y =p1. 20 [reference] x y=p1|isp1 x y =p2. 30 [reference] charq=abst k(eq) pair(pair(p1,p2),isp1). 32 [assumption to refute] p. 33 [assumption to refute] -p|charq badf !=p1. 34 [assumption to refute] badf x=p1|badf x =p2|$ans(x). 35 [ur,33,32,demod,30,6,1,4,4,5] eq pair(badf,isp1 badf)!=p1. 56 [ur,35,15,flip.1] isp1 badf!=badf. 65 [para_into,35.1.1,16.2.1,unit_del,56] p2!=p1. 75 [para_into,65.1.2,20.1.2,flip.1] x y!=p2|isp1 x y =p2. 78 [ur,56,17] isp1 badf noteq(isp1 badf,badf)!=badf noteq(isp1 badf,badf). 4548 [para_into,78.1.1,75.2.1,flip.1] badf noteq(isp1 badf,badf)!=p2. 4556 [para_into,78.1.1,19.2.1,flip.1] badf noteq(isp1 badf,badf)!=p1. 5519 [ur,4548,34] badf noteq(isp1 badf,badf)=p1|$ans(noteq(isp1 badf,badf)). 5520 [binary,5519.1,4556.1] $ans(noteq(isp1 badf,badf)).
up | previous | next | detailed contents | brief contents | OTTER output file