----- SUMMARY FOR THEOREM D-1A IN DIRECTORY Q:\D\1 ----- % D-1A.IN Revised 1996 December 28 % Direct Proof of Distributive Law using Binary Resolution % No demodulators except for abbreviations % Quaife, page 161. formula_list(sos). % negation of theorem D-1A -(all x all y all z equal(intersection(x,union(y,z)), union(intersection(x,y),intersection(x,z)))). end_of_list. ----- Otter 3.0.4, August 1995 ----- The job was started by ??? on ???, Sat Jul 12 03:53:27 1997 Length of proof is 55. Level of proof is 23. ---------------- PROOF ---------------- 21 [] -member(z,intersection(x,y)) | member(z,x). 22 [] -member(z,intersection(x,y)) | member(z,y). 23 [] -member(z,x) | -member(z,y) | member(z,intersection(x,y)). 99 [] equal(x,y) | member(notsub(x,y),x) | member(notsub(y,x),y). 100 [] -member(notsub(x,y),y) | equal(x,y) | member(notsub(y,x),y). 101 [] -member(notsub(y,x),x) | equal(x,y) | member(notsub(x,y),x). 102 [] -member(notsub(x,y),y) | -member(notsub(y,x),x) | equal(x,y). 173 [] -member(x,union(y,z)) | member(x,y) | member(x,z). 174 [] -member(x,y) | member(x,union(y,z)). 175 [] -member(x,z) | member(x,union(y,z)). 194 [] -equal(intersection($c3,union($c2,$c1)), union(intersection($c3,$c2),intersection($c3,$c1))). 196 [] equal(notsub(union(intersection(x,y),intersection(x,z)), intersection(x,union(y,z))),n1$(x,y,z)). 197 [] equal(notsub(intersection(x,union(y,z)), union(intersection(x,y),intersection(x,z))),n2$(x,y,z)). 199 [binary,194.1,102.3,demod,197,196] -member(n2$($c3,$c2,$c1),union(intersection($c3,$c2), intersection($c3,$c1))) | -member(n1$($c3,$c2,$c1), intersection($c3,union($c2,$c1))). 200 [binary,194.1,101.2,demod,196,197] -member(n1$($c3,$c2,$c1),intersection($c3,union($c2,$c1))) | member(n2$($c3,$c2,$c1),intersection($c3, union($c2,$c1))). 201 [binary,194.1,100.2,demod,197,196] -member(n2$($c3,$c2,$c1),union(intersection($c3,$c2), intersection($c3,$c1))) | member(n1$($c3,$c2,$c1), union(intersection($c3,$c2),intersection($c3,$c1))). 202 [binary,194.1,99.1,demod,197,196] member(n2$($c3,$c2,$c1),intersection($c3,union($c2,$c1))) | member(n1$($c3,$c2,$c1),union(intersection($c3,$c2), intersection($c3,$c1))). 204 [binary,200.2,22.1] -member(n1$($c3,$c2,$c1),intersection($c3,union($c2,$c1))) | member(n2$($c3,$c2,$c1),union($c2,$c1)). 205 [binary,200.2,21.1] -member(n1$($c3,$c2,$c1),intersection($c3,union($c2,$c1))) | member(n2$($c3,$c2,$c1),$c3). 208 [binary,204.2,173.1] -member(n1$($c3,$c2,$c1),intersection($c3,union($c2,$c1))) | member(n2$($c3,$c2,$c1),$c2) | member(n2$($c3,$c2,$c1),$c1). 211 [binary,199.1,175.2] -member(n1$($c3,$c2,$c1),intersection($c3,union($c2,$c1))) | -member(n2$($c3,$c2,$c1),intersection($c3,$c1)). 212 [binary,199.1,174.2] -member(n1$($c3,$c2,$c1),intersection($c3,union($c2,$c1))) | -member(n2$($c3,$c2,$c1),intersection($c3,$c2)). 214 [binary,211.2,23.3] -member(n1$($c3,$c2,$c1),intersection($c3,union($c2,$c1))) | -member(n2$($c3,$c2,$c1),$c3) | -member(n2$($c3,$c2,$c1),$c1). 216 [binary,212.2,23.3] -member(n1$($c3,$c2,$c1),intersection($c3,union($c2,$c1))) | -member(n2$($c3,$c2,$c1),$c3) | -member(n2$($c3,$c2,$c1),$c2). 217 [binary,202.1,22.1] member(n1$($c3,$c2,$c1),union(intersection($c3,$c2), intersection($c3,$c1))) | member(n2$($c3,$c2,$c1), union($c2,$c1)). 218 [binary,202.1,21.1] member(n1$($c3,$c2,$c1),union(intersection($c3,$c2), intersection($c3,$c1))) | member(n2$($c3,$c2,$c1),$c3). 219 [binary,218.1,173.1] member(n2$($c3,$c2,$c1),$c3) | member(n1$($c3,$c2,$c1), intersection($c3,$c2)) | member(n1$($c3,$c2,$c1), intersection($c3,$c1)). 220 [binary,217.1,173.1] member(n2$($c3,$c2,$c1),union($c2,$c1)) | member(n1$($c3,$c2,$c1),intersection($c3,$c2)) | member(n1$($c3,$c2,$c1),intersection($c3,$c1)). 226 [binary,214.2,205.2,factor_simp] -member(n1$($c3,$c2,$c1),intersection($c3,union($c2,$c1))) | -member(n2$($c3,$c2,$c1),$c1). 229 [binary,226.2,208.3,factor_simp] -member(n1$($c3,$c2,$c1),intersection($c3,union($c2,$c1))) | member(n2$($c3,$c2,$c1),$c2). 237 [binary,216.2,205.2,factor_simp] -member(n1$($c3,$c2,$c1),intersection($c3,union($c2,$c1))) | -member(n2$($c3,$c2,$c1),$c2). 243 [binary,237.2,229.2,factor_simp] -member(n1$($c3,$c2,$c1),intersection($c3,union($c2,$c1))). 244 [binary,243.1,23.3] -member(n1$($c3,$c2,$c1),$c3) | -member(n1$($c3,$c2,$c1),union($c2,$c1)). 245 [binary,244.2,175.2] -member(n1$($c3,$c2,$c1),$c3) | -member(n1$($c3,$c2,$c1),$c1). 246 [binary,244.2,174.2] -member(n1$($c3,$c2,$c1),$c3) | -member(n1$($c3,$c2,$c1),$c2). 247 [binary,219.2,22.1] member(n2$($c3,$c2,$c1),$c3) | member(n1$($c3,$c2,$c1), intersection($c3,$c1)) | member(n1$($c3,$c2,$c1),$c2). 248 [binary,219.2,21.1] member(n2$($c3,$c2,$c1),$c3) | member(n1$($c3,$c2,$c1), intersection($c3,$c1)) | member(n1$($c3,$c2,$c1),$c3). 251 [binary,247.2,22.1] member(n2$($c3,$c2,$c1),$c3) | member(n1$($c3,$c2,$c1),$c2) | member(n1$($c3,$c2,$c1),$c1). 254 [binary,251.2,246.2] member(n2$($c3,$c2,$c1),$c3) | member(n1$($c3,$c2,$c1),$c1) | -member(n1$($c3,$c2,$c1),$c3). 258 [binary,254.2,245.2,factor_simp] member(n2$($c3,$c2,$c1),$c3) | -member(n1$($c3,$c2,$c1), $c3). 261 [binary,248.2,21.1,factor_simp] member(n2$($c3,$c2,$c1),$c3) | member(n1$($c3,$c2,$c1),$c3). 263 [binary,261.2,258.2,factor_simp] member(n2$($c3,$c2,$c1),$c3). 264 [binary,201.1,175.2] member(n1$($c3,$c2,$c1),union(intersection($c3,$c2), intersection($c3,$c1))) | -member(n2$($c3,$c2,$c1), intersection($c3,$c1)). 265 [binary,201.1,174.2] member(n1$($c3,$c2,$c1),union(intersection($c3,$c2), intersection($c3,$c1))) | -member(n2$($c3,$c2,$c1), intersection($c3,$c2)). 267 [binary,264.2,23.3,unit_del,263] member(n1$($c3,$c2,$c1),union(intersection($c3,$c2), intersection($c3,$c1))) | -member(n2$($c3,$c2,$c1),$c1). 268 [binary,267.1,173.1] -member(n2$($c3,$c2,$c1),$c1) | member(n1$($c3,$c2,$c1),intersection($c3,$c2)) | member(n1$($c3,$c2,$c1),intersection($c3,$c1)). 270 [binary,265.2,23.3,unit_del,263] member(n1$($c3,$c2,$c1),union(intersection($c3,$c2), intersection($c3,$c1))) | -member(n2$($c3,$c2,$c1),$c2). 271 [binary,270.1,173.1] -member(n2$($c3,$c2,$c1),$c2) | member(n1$($c3,$c2,$c1),intersection($c3,$c2)) | member(n1$($c3,$c2,$c1),intersection($c3,$c1)). 272 [binary,268.2,22.1] -member(n2$($c3,$c2,$c1),$c1) | member(n1$($c3,$c2,$c1),intersection($c3,$c1)) | member(n1$($c3,$c2,$c1),$c2). 273 [binary,268.2,21.1] -member(n2$($c3,$c2,$c1),$c1) | member(n1$($c3,$c2,$c1),intersection($c3,$c1)) | member(n1$($c3,$c2,$c1),$c3). 276 [binary,272.2,22.1] -member(n2$($c3,$c2,$c1),$c1) | member(n1$($c3,$c2,$c1),$c2) | member(n1$($c3,$c2,$c1),$c1). 279 [binary,276.2,246.2] -member(n2$($c3,$c2,$c1),$c1) | member(n1$($c3,$c2,$c1),$c1) | -member(n1$($c3,$c2,$c1),$c3). 283 [binary,279.2,245.2,factor_simp] -member(n2$($c3,$c2,$c1),$c1) | -member(n1$($c3,$c2,$c1),$c3). 286 [binary,273.2,21.1,factor_simp] -member(n2$($c3,$c2,$c1),$c1) | member(n1$($c3,$c2,$c1),$c3). 288 [binary,286.2,283.2,factor_simp] -member(n2$($c3,$c2,$c1),$c1). 289 [binary,271.2,22.1] -member(n2$($c3,$c2,$c1),$c2) | member(n1$($c3,$c2,$c1),intersection($c3,$c1)) | member(n1$($c3,$c2,$c1),$c2). 290 [binary,271.2,21.1] -member(n2$($c3,$c2,$c1),$c2) | member(n1$($c3,$c2,$c1),intersection($c3,$c1)) | member(n1$($c3,$c2,$c1),$c3). 293 [binary,289.2,22.1] -member(n2$($c3,$c2,$c1),$c2) | member(n1$($c3,$c2,$c1),$c2) | member(n1$($c3,$c2,$c1),$c1). 296 [binary,293.2,246.2] -member(n2$($c3,$c2,$c1),$c2) | member(n1$($c3,$c2,$c1),$c1) | -member(n1$($c3,$c2,$c1),$c3). 300 [binary,296.2,245.2,factor_simp] -member(n2$($c3,$c2,$c1),$c2) | -member(n1$($c3,$c2,$c1),$c3). 303 [binary,290.2,21.1,factor_simp] -member(n2$($c3,$c2,$c1),$c2) | member(n1$($c3,$c2,$c1),$c3). 305 [binary,303.2,300.2,factor_simp] -member(n2$($c3,$c2,$c1),$c2). 306 [binary,220.1,173.1,unit_del,305,288] member(n1$($c3,$c2,$c1),intersection($c3,$c2)) | member(n1$($c3,$c2,$c1),intersection($c3,$c1)). 311 [binary,306.1,22.1] member(n1$($c3,$c2,$c1),intersection($c3,$c1)) | member(n1$($c3,$c2,$c1),$c2). 312 [binary,306.1,21.1] member(n1$($c3,$c2,$c1),intersection($c3,$c1)) | member(n1$($c3,$c2,$c1),$c3). 315 [binary,311.1,22.1] member(n1$($c3,$c2,$c1),$c2) | member(n1$($c3,$c2,$c1),$c1). 318 [binary,315.1,246.2] member(n1$($c3,$c2,$c1),$c1) | -member(n1$($c3,$c2,$c1), $c3). 322 [binary,318.1,245.2,factor_simp] -member(n1$($c3,$c2,$c1),$c3). 325 [binary,312.1,21.1,unit_del,322,322] $F. ------------ end of proof ------------- clauses generated 2313 Kbytes malloced 287 user CPU time 1.27 seconds