z is a subset of every element of x, then z is a subset of the intersection of x ----> UNIT CONFLICT at 0.63 sec ----> 355 [binary,353.1,313.1] $ans(notinint(bad_collection,notsub(bad_set,kintersection bad_collection bad))). Length of proof is 6. Level of proof is 3.
2 [reference] p1 pair(x,y)=x. 3 [reference] p2 pair(x,y)=y. 56 [reference] kintersection xf y x=p1|xf notinint(xf,x) =p1. 57 [reference] kintersection xf y x=p1|notinint(xf,x) x !=p1. 60 [reference] subset pair(x1,x2)=p2|x1 xc !=p1|x2 xc =p1. 64 [reference] subset x=p1|p1 x notsub(p1 x,p2 x) =p1. 65 [reference] subset x=p1|p2 x notsub(p1 x,p2 x) !=p1. 70 [assumption to refute] bad_collection x!=p1|subset pair(bad_set,x) !=p2|$ans(x). 71 [assumption to refute] subset pair(bad_set,kintersection bad_collection bad)!=p1. 72 [ur,71,65,demod,3,2,3] kintersection bad_collection bad notsub(bad_set,kintersection bad_collection bad)!=p1. 73 [ur,71,64,demod,2,2,3] bad_set notsub(bad_set,kintersection bad_collection bad)=p1. 106 [ur,72,57] notinint(bad_collection,notsub(bad_set,kintersection bad_collection bad)) notsub(bad_set,kintersection bad_collec tion bad)!=p1. 107 [ur,72,56] bad_collection notinint(bad_collection,notsub(bad_set,kintersection bad_collection bad))=p1. 313 [ur,107,70] subset pair(bad_set,notinint(bad_collection,notsub(bad_set,kintersection bad_collection bad)))!=p2|$ans(notinint (bad_collection,notsub(bad_set,kintersection bad_collection bad))). 353 [ur,106,60,73] subset pair(bad_set,notinint(bad_collection,notsub(bad_set,kintersection bad_collection bad)))=p2. 355 [binary,353.1,313.1] $ans(notinint(bad_collection,notsub(bad_set,kintersection bad_collection bad))).
up | previous | next | detailed contents | brief contents | OTTER output file