path: root/etc/isar/AThousandTheorems.thy

theory AThousandTheorems imports Main
begin

ML {* val start = Timing.start () *}
(* ELISP: -- (setq start (current-time)) -- *)

lemma foo: "P --> P" by auto
lemma foo2: "P --> P" by auto
lemma foo3: "P --> P" by auto
lemma foo4: "P --> P" by auto
lemma foo5: "P --> P" by auto
lemma foo6: "P --> P" by auto
lemma foo7: "P --> P" by auto
lemma foo8: "P --> P" by auto
lemma foo9: "P --> P" by auto
lemma foo10: "P --> P" by auto
lemma foo11: "P --> P" by auto
lemma foo12: "P --> P" by auto
lemma foo13: "P --> P" by auto
lemma foo14: "P --> P" by auto
lemma foo15: "P --> P" by auto
lemma foo16: "P --> P" by auto
lemma foo17: "P --> P" by auto
lemma foo18: "P --> P" by auto
lemma foo19: "P --> P" by auto
lemma foo20: "P --> P" by auto
lemma foo21: "P --> P" by auto
lemma foo22: "P --> P" by auto
lemma foo23: "P --> P" by auto
lemma foo24: "P --> P" by auto
lemma foo25: "P --> P" by auto
lemma foo26: "P --> P" by auto
lemma foo27: "P --> P" by auto
lemma foo28: "P --> P" by auto
lemma foo29: "P --> P" by auto
lemma foo30: "P --> P" by auto
lemma foo31: "P --> P" by auto
lemma foo32: "P --> P" by auto
lemma foo33: "P --> P" by auto
lemma foo34: "P --> P" by auto
lemma foo35: "P --> P" by auto
lemma foo36: "P --> P" by auto
lemma foo37: "P --> P" by auto
lemma foo38: "P --> P" by auto
lemma foo39: "P --> P" by auto
lemma foo40: "P --> P" by auto
lemma foo41: "P --> P" by auto
lemma foo42: "P --> P" by auto
lemma foo43: "P --> P" by auto
lemma foo44: "P --> P" by auto
lemma foo45: "P --> P" by auto
lemma foo46: "P --> P" by auto
lemma foo47: "P --> P" by auto
lemma foo48: "P --> P" by auto
lemma foo49: "P --> P" by auto
lemma foo50: "P --> P" by auto
lemma foo51: "P --> P" by auto
lemma foo52: "P --> P" by auto
lemma foo53: "P --> P" by auto
lemma foo54: "P --> P" by auto
lemma foo55: "P --> P" by auto
lemma foo56: "P --> P" by auto
lemma foo57: "P --> P" by auto
lemma foo58: "P --> P" by auto
lemma foo59: "P --> P" by auto
lemma foo60: "P --> P" by auto
lemma foo61: "P --> P" by auto
lemma foo62: "P --> P" by auto
lemma foo63: "P --> P" by auto
lemma foo64: "P --> P" by auto
lemma foo65: "P --> P" by auto
lemma foo66: "P --> P" by auto
lemma foo67: "P --> P" by auto
lemma foo68: "P --> P" by auto
lemma foo69: "P --> P" by auto
lemma foo70: "P --> P" by auto
lemma foo71: "P --> P" by auto
lemma foo72: "P --> P" by auto
lemma foo73: "P --> P" by auto
lemma foo74: "P --> P" by auto
lemma foo75: "P --> P" by auto
lemma foo76: "P --> P" by auto
lemma foo77: "P --> P" by auto
lemma foo78: "P --> P" by auto
lemma foo79: "P --> P" by auto
lemma foo80: "P --> P" by auto
lemma foo81: "P --> P" by auto
lemma foo82: "P --> P" by auto
lemma foo83: "P --> P" by auto
lemma foo84: "P --> P" by auto
lemma foo85: "P --> P" by auto
lemma foo86: "P --> P" by auto
lemma foo87: "P --> P" by auto
lemma foo88: "P --> P" by auto
lemma foo89: "P --> P" by auto
lemma foo90: "P --> P" by auto
lemma foo91: "P --> P" by auto
lemma foo92: "P --> P" by auto
lemma foo93: "P --> P" by auto
lemma foo94: "P --> P" by auto
lemma foo95: "P --> P" by auto
lemma foo96: "P --> P" by auto
lemma foo97: "P --> P" by auto
lemma foo98: "P --> P" by auto
lemma foo99: "P --> P" by auto
lemma foo100: "P --> P" by auto
lemma foo101: "P --> P" by auto
lemma foo102: "P --> P" by auto
lemma foo103: "P --> P" by auto
lemma foo104: "P --> P" by auto
lemma foo105: "P --> P" by auto
lemma foo106: "P --> P" by auto
lemma foo107: "P --> P" by auto
lemma foo108: "P --> P" by auto
lemma foo109: "P --> P" by auto
lemma foo110: "P --> P" by auto
lemma foo111: "P --> P" by auto
lemma foo112: "P --> P" by auto
lemma foo113: "P --> P" by auto
lemma foo114: "P --> P" by auto
lemma foo115: "P --> P" by auto
lemma foo116: "P --> P" by auto
lemma foo117: "P --> P" by auto
lemma foo118: "P --> P" by auto
lemma foo119: "P --> P" by auto
lemma foo120: "P --> P" by auto
lemma foo121: "P --> P" by auto
lemma foo122: "P --> P" by auto
lemma foo123: "P --> P" by auto
lemma foo124: "P --> P" by auto
lemma foo125: "P --> P" by auto
lemma foo126: "P --> P" by auto
lemma foo127: "P --> P" by auto
lemma foo128: "P --> P" by auto
lemma foo129: "P --> P" by auto
lemma foo130: "P --> P" by auto
lemma foo131: "P --> P" by auto
lemma foo132: "P --> P" by auto
lemma foo133: "P --> P" by auto
lemma foo134: "P --> P" by auto
lemma foo135: "P --> P" by auto
lemma foo136: "P --> P" by auto
lemma foo137: "P --> P" by auto
lemma foo138: "P --> P" by auto
lemma foo139: "P --> P" by auto
lemma foo140: "P --> P" by auto
lemma foo141: "P --> P" by auto
lemma foo142: "P --> P" by auto
lemma foo143: "P --> P" by auto
lemma foo144: "P --> P" by auto
lemma foo145: "P --> P" by auto
lemma foo146: "P --> P" by auto
lemma foo147: "P --> P" by auto
lemma foo148: "P --> P" by auto
lemma foo149: "P --> P" by auto
lemma foo150: "P --> P" by auto
lemma foo151: "P --> P" by auto
lemma foo152: "P --> P" by auto
lemma foo153: "P --> P" by auto
lemma foo154: "P --> P" by auto
lemma foo155: "P --> P" by auto
lemma foo156: "P --> P" by auto
lemma foo157: "P --> P" by auto
lemma foo158: "P --> P" by auto
lemma foo159: "P --> P" by auto
lemma foo160: "P --> P" by auto
lemma foo161: "P --> P" by auto
lemma foo162: "P --> P" by auto
lemma foo163: "P --> P" by auto
lemma foo164: "P --> P" by auto
lemma foo165: "P --> P" by auto
lemma foo166: "P --> P" by auto
lemma foo167: "P --> P" by auto
lemma foo168: "P --> P" by auto
lemma foo169: "P --> P" by auto
lemma foo170: "P --> P" by auto
lemma foo171: "P --> P" by auto
lemma foo172: "P --> P" by auto
lemma foo173: "P --> P" by auto
lemma foo174: "P --> P" by auto
lemma foo175: "P --> P" by auto
lemma foo176: "P --> P" by auto
lemma foo177: "P --> P" by auto
lemma foo178: "P --> P" by auto
lemma foo179: "P --> P" by auto
lemma foo180: "P --> P" by auto
lemma foo181: "P --> P" by auto
lemma foo182: "P --> P" by auto
lemma foo183: "P --> P" by auto
lemma foo184: "P --> P" by auto
lemma foo185: "P --> P" by auto
lemma foo186: "P --> P" by auto
lemma foo187: "P --> P" by auto
lemma foo188: "P --> P" by auto
lemma foo189: "P --> P" by auto
lemma foo190: "P --> P" by auto
lemma foo191: "P --> P" by auto
lemma foo192: "P --> P" by auto
lemma foo193: "P --> P" by auto
lemma foo194: "P --> P" by auto
lemma foo195: "P --> P" by auto
lemma foo196: "P --> P" by auto
lemma foo197: "P --> P" by auto
lemma foo198: "P --> P" by auto
lemma foo199: "P --> P" by auto
lemma foo200: "P --> P" by auto
lemma foo201: "P --> P" by auto
lemma foo202: "P --> P" by auto
lemma foo203: "P --> P" by auto
lemma foo204: "P --> P" by auto
lemma foo205: "P --> P" by auto
lemma foo206: "P --> P" by auto
lemma foo207: "P --> P" by auto
lemma foo208: "P --> P" by auto
lemma foo209: "P --> P" by auto
lemma foo210: "P --> P" by auto
lemma foo211: "P --> P" by auto
lemma foo212: "P --> P" by auto
lemma foo213: "P --> P" by auto
lemma foo214: "P --> P" by auto
lemma foo215: "P --> P" by auto
lemma foo216: "P --> P" by auto
lemma foo217: "P --> P" by auto
lemma foo218: "P --> P" by auto
lemma foo219: "P --> P" by auto
lemma foo220: "P --> P" by auto
lemma foo221: "P --> P" by auto
lemma foo222: "P --> P" by auto
lemma foo223: "P --> P" by auto
lemma foo224: "P --> P" by auto
lemma foo225: "P --> P" by auto
lemma foo226: "P --> P" by auto
lemma foo227: "P --> P" by auto
lemma foo228: "P --> P" by auto
lemma foo229: "P --> P" by auto
lemma foo230: "P --> P" by auto
lemma foo231: "P --> P" by auto
lemma foo232: "P --> P" by auto
lemma foo233: "P --> P" by auto
lemma foo234: "P --> P" by auto
lemma foo235: "P --> P" by auto
lemma foo236: "P --> P" by auto
lemma foo237: "P --> P" by auto
lemma foo238: "P --> P" by auto
lemma foo239: "P --> P" by auto
lemma foo240: "P --> P" by auto
lemma foo241: "P --> P" by auto
lemma foo242: "P --> P" by auto
lemma foo243: "P --> P" by auto
lemma foo244: "P --> P" by auto
lemma foo245: "P --> P" by auto
lemma foo246: "P --> P" by auto
lemma foo247: "P --> P" by auto
lemma foo248: "P --> P" by auto
lemma foo249: "P --> P" by auto
lemma foo250: "P --> P" by auto
lemma foo251: "P --> P" by auto
lemma foo252: "P --> P" by auto
lemma foo253: "P --> P" by auto
lemma foo254: "P --> P" by auto
lemma foo255: "P --> P" by auto
lemma foo256: "P --> P" by auto
lemma foo257: "P --> P" by auto
lemma foo258: "P --> P" by auto
lemma foo259: "P --> P" by auto
lemma foo260: "P --> P" by auto
lemma foo261: "P --> P" by auto
lemma foo262: "P --> P" by auto
lemma foo263: "P --> P" by auto
lemma foo264: "P --> P" by auto
lemma foo265: "P --> P" by auto
lemma foo266: "P --> P" by auto
lemma foo267: "P --> P" by auto
lemma foo268: "P --> P" by auto
lemma foo269: "P --> P" by auto
lemma foo270: "P --> P" by auto
lemma foo271: "P --> P" by auto
lemma foo272: "P --> P" by auto
lemma foo273: "P --> P" by auto
lemma foo274: "P --> P" by auto
lemma foo275: "P --> P" by auto
lemma foo276: "P --> P" by auto
lemma foo277: "P --> P" by auto
lemma foo278: "P --> P" by auto
lemma foo279: "P --> P" by auto
lemma foo280: "P --> P" by auto
lemma foo281: "P --> P" by auto
lemma foo282: "P --> P" by auto
lemma foo283: "P --> P" by auto
lemma foo284: "P --> P" by auto
lemma foo285: "P --> P" by auto
lemma foo286: "P --> P" by auto
lemma foo287: "P --> P" by auto
lemma foo288: "P --> P" by auto
lemma foo289: "P --> P" by auto
lemma foo290: "P --> P" by auto
lemma foo291: "P --> P" by auto
lemma foo292: "P --> P" by auto
lemma foo293: "P --> P" by auto
lemma foo294: "P --> P" by auto
lemma foo295: "P --> P" by auto
lemma foo296: "P --> P" by auto
lemma foo297: "P --> P" by auto
lemma foo298: "P --> P" by auto
lemma foo299: "P --> P" by auto
lemma foo300: "P --> P" by auto
lemma foo301: "P --> P" by auto
lemma foo302: "P --> P" by auto
lemma foo303: "P --> P" by auto
lemma foo304: "P --> P" by auto
lemma foo305: "P --> P" by auto
lemma foo306: "P --> P" by auto
lemma foo307: "P --> P" by auto
lemma foo308: "P --> P" by auto
lemma foo309: "P --> P" by auto
lemma foo310: "P --> P" by auto
lemma foo311: "P --> P" by auto
lemma foo312: "P --> P" by auto
lemma foo313: "P --> P" by auto
lemma foo314: "P --> P" by auto
lemma foo315: "P --> P" by auto
lemma foo316: "P --> P" by auto
lemma foo317: "P --> P" by auto
lemma foo318: "P --> P" by auto
lemma foo319: "P --> P" by auto
lemma foo320: "P --> P" by auto
lemma foo321: "P --> P" by auto
lemma foo322: "P --> P" by auto
lemma foo323: "P --> P" by auto
lemma foo324: "P --> P" by auto
lemma foo325: "P --> P" by auto
lemma foo326: "P --> P" by auto
lemma foo327: "P --> P" by auto
lemma foo328: "P --> P" by auto
lemma foo329: "P --> P" by auto
lemma foo330: "P --> P" by auto
lemma foo331: "P --> P" by auto
lemma foo332: "P --> P" by auto
lemma foo333: "P --> P" by auto
lemma foo334: "P --> P" by auto
lemma foo335: "P --> P" by auto
lemma foo336: "P --> P" by auto
lemma foo337: "P --> P" by auto
lemma foo338: "P --> P" by auto
lemma foo339: "P --> P" by auto
lemma foo340: "P --> P" by auto
lemma foo341: "P --> P" by auto
lemma foo342: "P --> P" by auto
lemma foo343: "P --> P" by auto
lemma foo344: "P --> P" by auto
lemma foo345: "P --> P" by auto
lemma foo346: "P --> P" by auto
lemma foo347: "P --> P" by auto
lemma foo348: "P --> P" by auto
lemma foo349: "P --> P" by auto
lemma foo350: "P --> P" by auto
lemma foo351: "P --> P" by auto
lemma foo352: "P --> P" by auto
lemma foo353: "P --> P" by auto
lemma foo354: "P --> P" by auto
lemma foo355: "P --> P" by auto
lemma foo356: "P --> P" by auto
lemma foo357: "P --> P" by auto
lemma foo358: "P --> P" by auto
lemma foo359: "P --> P" by auto
lemma foo360: "P --> P" by auto
lemma foo361: "P --> P" by auto
lemma foo362: "P --> P" by auto
lemma foo363: "P --> P" by auto
lemma foo364: "P --> P" by auto
lemma foo365: "P --> P" by auto
lemma foo366: "P --> P" by auto
lemma foo367: "P --> P" by auto
lemma foo368: "P --> P" by auto
lemma foo369: "P --> P" by auto
lemma foo370: "P --> P" by auto
lemma foo371: "P --> P" by auto
lemma foo372: "P --> P" by auto
lemma foo373: "P --> P" by auto
lemma foo374: "P --> P" by auto
lemma foo375: "P --> P" by auto
lemma foo376: "P --> P" by auto
lemma foo377: "P --> P" by auto
lemma foo378: "P --> P" by auto
lemma foo379: "P --> P" by auto
lemma foo380: "P --> P" by auto
lemma foo381: "P --> P" by auto
lemma foo382: "P --> P" by auto
lemma foo383: "P --> P" by auto
lemma foo384: "P --> P" by auto
lemma foo385: "P --> P" by auto
lemma foo386: "P --> P" by auto
lemma foo387: "P --> P" by auto
lemma foo388: "P --> P" by auto
lemma foo389: "P --> P" by auto
lemma foo390: "P --> P" by auto
lemma foo391: "P --> P" by auto
lemma foo392: "P --> P" by auto
lemma foo393: "P --> P" by auto
lemma foo394: "P --> P" by auto
lemma foo395: "P --> P" by auto
lemma foo396: "P --> P" by auto
lemma foo397: "P --> P" by auto
lemma foo398: "P --> P" by auto
lemma foo399: "P --> P" by auto
lemma foo400: "P --> P" by auto
lemma foo401: "P --> P" by auto
lemma foo402: "P --> P" by auto
lemma foo403: "P --> P" by auto
lemma foo404: "P --> P" by auto
lemma foo405: "P --> P" by auto
lemma foo406: "P --> P" by auto
lemma foo407: "P --> P" by auto
lemma foo408: "P --> P" by auto
lemma foo409: "P --> P" by auto
lemma foo410: "P --> P" by auto
lemma foo411: "P --> P" by auto
lemma foo412: "P --> P" by auto
lemma foo413: "P --> P" by auto
lemma foo414: "P --> P" by auto
lemma foo415: "P --> P" by auto
lemma foo416: "P --> P" by auto
lemma foo417: "P --> P" by auto
lemma foo418: "P --> P" by auto
lemma foo419: "P --> P" by auto
lemma foo420: "P --> P" by auto
lemma foo421: "P --> P" by auto
lemma foo422: "P --> P" by auto
lemma foo423: "P --> P" by auto
lemma foo424: "P --> P" by auto
lemma foo425: "P --> P" by auto
lemma foo426: "P --> P" by auto
lemma foo427: "P --> P" by auto
lemma foo428: "P --> P" by auto
lemma foo429: "P --> P" by auto
lemma foo430: "P --> P" by auto
lemma foo431: "P --> P" by auto
lemma foo432: "P --> P" by auto
lemma foo433: "P --> P" by auto
lemma foo434: "P --> P" by auto
lemma foo435: "P --> P" by auto
lemma foo436: "P --> P" by auto
lemma foo437: "P --> P" by auto
lemma foo438: "P --> P" by auto
lemma foo439: "P --> P" by auto
lemma foo440: "P --> P" by auto
lemma foo441: "P --> P" by auto
lemma foo442: "P --> P" by auto
lemma foo443: "P --> P" by auto
lemma foo444: "P --> P" by auto
lemma foo445: "P --> P" by auto
lemma foo446: "P --> P" by auto
lemma foo447: "P --> P" by auto
lemma foo448: "P --> P" by auto
lemma foo449: "P --> P" by auto
lemma foo450: "P --> P" by auto
lemma foo451: "P --> P" by auto
lemma foo452: "P --> P" by auto
lemma foo453: "P --> P" by auto
lemma foo454: "P --> P" by auto
lemma foo455: "P --> P" by auto
lemma foo456: "P --> P" by auto
lemma foo457: "P --> P" by auto
lemma foo458: "P --> P" by auto
lemma foo459: "P --> P" by auto
lemma foo460: "P --> P" by auto
lemma foo461: "P --> P" by auto
lemma foo462: "P --> P" by auto
lemma foo463: "P --> P" by auto
lemma foo464: "P --> P" by auto
lemma foo465: "P --> P" by auto
lemma foo466: "P --> P" by auto
lemma foo467: "P --> P" by auto
lemma foo468: "P --> P" by auto
lemma foo469: "P --> P" by auto
lemma foo470: "P --> P" by auto
lemma foo471: "P --> P" by auto
lemma foo472: "P --> P" by auto
lemma foo473: "P --> P" by auto
lemma foo474: "P --> P" by auto
lemma foo475: "P --> P" by auto
lemma foo476: "P --> P" by auto
lemma foo477: "P --> P" by auto
lemma foo478: "P --> P" by auto
lemma foo479: "P --> P" by auto
lemma foo480: "P --> P" by auto
lemma foo481: "P --> P" by auto
lemma foo482: "P --> P" by auto
lemma foo483: "P --> P" by auto
lemma foo484: "P --> P" by auto
lemma foo485: "P --> P" by auto
lemma foo486: "P --> P" by auto
lemma foo487: "P --> P" by auto
lemma foo488: "P --> P" by auto
lemma foo489: "P --> P" by auto
lemma foo490: "P --> P" by auto
lemma foo491: "P --> P" by auto
lemma foo492: "P --> P" by auto
lemma foo493: "P --> P" by auto
lemma foo494: "P --> P" by auto
lemma foo495: "P --> P" by auto
lemma foo496: "P --> P" by auto
lemma foo497: "P --> P" by auto
lemma foo498: "P --> P" by auto
lemma foo499: "P --> P" by auto
lemma foo500: "P --> P" by auto
(*lemma foo500: "P --> P" by auto *)
lemma foo501: "P --> P" by auto
lemma foo502: "P --> P" by auto
lemma foo503: "P --> P" by auto
lemma foo504: "P --> P" by auto
lemma foo505: "P --> P" by auto
lemma foo506: "P --> P" by auto
lemma foo507: "P --> P" by auto
lemma foo508: "P --> P" by auto
lemma foo509: "P --> P" by auto
lemma foo510: "P --> P" by auto
lemma foo511: "P --> P" by auto
lemma foo512: "P --> P" by auto
lemma foo513: "P --> P" by auto
lemma foo514: "P --> P" by auto
lemma foo515: "P --> P" by auto
lemma foo516: "P --> P" by auto
lemma foo517: "P --> P" by auto
lemma foo518: "P --> P" by auto
lemma foo519: "P --> P" by auto
lemma foo520: "P --> P" by auto
lemma foo521: "P --> P" by auto
lemma foo522: "P --> P" by auto
lemma foo523: "P --> P" by auto
lemma foo524: "P --> P" by auto
lemma foo525: "P --> P" by auto
lemma foo526: "P --> P" by auto
lemma foo527: "P --> P" by auto
lemma foo528: "P --> P" by auto
lemma foo529: "P --> P" by auto
lemma foo530: "P --> P" by auto
lemma foo531: "P --> P" by auto
lemma foo532: "P --> P" by auto
lemma foo533: "P --> P" by auto
lemma foo534: "P --> P" by auto
lemma foo535: "P --> P" by auto
lemma foo536: "P --> P" by auto
lemma foo537: "P --> P" by auto
lemma foo538: "P --> P" by auto
lemma foo539: "P --> P" by auto
lemma foo540: "P --> P" by auto
lemma foo541: "P --> P" by auto
lemma foo542: "P --> P" by auto
lemma foo543: "P --> P" by auto
lemma foo544: "P --> P" by auto
lemma foo545: "P --> P" by auto
lemma foo546: "P --> P" by auto
lemma foo547: "P --> P" by auto
lemma foo548: "P --> P" by auto
lemma foo549: "P --> P" by auto
lemma foo550: "P --> P" by auto
lemma foo551: "P --> P" by auto
lemma foo552: "P --> P" by auto
lemma foo553: "P --> P" by auto
lemma foo554: "P --> P" by auto
lemma foo555: "P --> P" by auto
lemma foo556: "P --> P" by auto
lemma foo557: "P --> P" by auto
lemma foo558: "P --> P" by auto
lemma foo559: "P --> P" by auto
lemma foo560: "P --> P" by auto
lemma foo561: "P --> P" by auto
lemma foo562: "P --> P" by auto
lemma foo563: "P --> P" by auto
lemma foo564: "P --> P" by auto
lemma foo565: "P --> P" by auto
lemma foo566: "P --> P" by auto
lemma foo567: "P --> P" by auto
lemma foo568: "P --> P" by auto
lemma foo569: "P --> P" by auto
lemma foo570: "P --> P" by auto
lemma foo571: "P --> P" by auto
lemma foo572: "P --> P" by auto
lemma foo573: "P --> P" by auto
lemma foo574: "P --> P" by auto
lemma foo575: "P --> P" by auto
lemma foo576: "P --> P" by auto
lemma foo577: "P --> P" by auto
lemma foo578: "P --> P" by auto
lemma foo579: "P --> P" by auto
lemma foo580: "P --> P" by auto
lemma foo581: "P --> P" by auto
lemma foo582: "P --> P" by auto
lemma foo583: "P --> P" by auto
lemma foo584: "P --> P" by auto
lemma foo585: "P --> P" by auto
lemma foo586: "P --> P" by auto
lemma foo587: "P --> P" by auto
lemma foo588: "P --> P" by auto
lemma foo589: "P --> P" by auto
lemma foo590: "P --> P" by auto
lemma foo591: "P --> P" by auto
lemma foo592: "P --> P" by auto
lemma foo593: "P --> P" by auto
lemma foo594: "P --> P" by auto
lemma foo595: "P --> P" by auto
lemma foo596: "P --> P" by auto
lemma foo597: "P --> P" by auto
lemma foo598: "P --> P" by auto
lemma foo599: "P --> P" by auto
lemma foo600: "P --> P" by auto
lemma foo601: "P --> P" by auto
lemma foo602: "P --> P" by auto
lemma foo603: "P --> P" by auto
lemma foo604: "P --> P" by auto
lemma foo605: "P --> P" by auto
lemma foo606: "P --> P" by auto
lemma foo607: "P --> P" by auto
lemma foo608: "P --> P" by auto
lemma foo609: "P --> P" by auto
lemma foo610: "P --> P" by auto
lemma foo611: "P --> P" by auto
lemma foo612: "P --> P" by auto
lemma foo613: "P --> P" by auto
lemma foo614: "P --> P" by auto
lemma foo615: "P --> P" by auto
lemma foo616: "P --> P" by auto
lemma foo617: "P --> P" by auto
lemma foo618: "P --> P" by auto
lemma foo619: "P --> P" by auto
lemma foo620: "P --> P" by auto
lemma foo621: "P --> P" by auto
lemma foo622: "P --> P" by auto
lemma foo623: "P --> P" by auto
lemma foo624: "P --> P" by auto
lemma foo625: "P --> P" by auto
lemma foo626: "P --> P" by auto
lemma foo627: "P --> P" by auto
lemma foo628: "P --> P" by auto
lemma foo629: "P --> P" by auto
lemma foo630: "P --> P" by auto
lemma foo631: "P --> P" by auto
lemma foo632: "P --> P" by auto
lemma foo633: "P --> P" by auto
lemma foo634: "P --> P" by auto
lemma foo635: "P --> P" by auto
lemma foo636: "P --> P" by auto
lemma foo637: "P --> P" by auto
lemma foo638: "P --> P" by auto
lemma foo639: "P --> P" by auto
lemma foo640: "P --> P" by auto
lemma foo641: "P --> P" by auto
lemma foo642: "P --> P" by auto
lemma foo643: "P --> P" by auto
lemma foo644: "P --> P" by auto
lemma foo645: "P --> P" by auto
lemma foo646: "P --> P" by auto
lemma foo647: "P --> P" by auto
lemma foo648: "P --> P" by auto
lemma foo649: "P --> P" by auto
lemma foo650: "P --> P" by auto
lemma foo651: "P --> P" by auto
lemma foo652: "P --> P" by auto
lemma foo653: "P --> P" by auto
lemma foo654: "P --> P" by auto
lemma foo655: "P --> P" by auto
lemma foo656: "P --> P" by auto
lemma foo657: "P --> P" by auto
lemma foo658: "P --> P" by auto
lemma foo659: "P --> P" by auto
lemma foo660: "P --> P" by auto
lemma foo661: "P --> P" by auto
lemma foo662: "P --> P" by auto
lemma foo663: "P --> P" by auto
lemma foo664: "P --> P" by auto
lemma foo665: "P --> P" by auto
lemma foo666: "P --> P" by auto
lemma foo667: "P --> P" by auto
lemma foo668: "P --> P" by auto
lemma foo669: "P --> P" by auto
lemma foo670: "P --> P" by auto
lemma foo671: "P --> P" by auto
lemma foo672: "P --> P" by auto
lemma foo673: "P --> P" by auto
lemma foo674: "P --> P" by auto
lemma foo675: "P --> P" by auto
lemma foo676: "P --> P" by auto
lemma foo677: "P --> P" by auto
lemma foo678: "P --> P" by auto
lemma foo679: "P --> P" by auto
lemma foo680: "P --> P" by auto
lemma foo681: "P --> P" by auto
lemma foo682: "P --> P" by auto
lemma foo683: "P --> P" by auto
lemma foo684: "P --> P" by auto
lemma foo685: "P --> P" by auto
lemma foo686: "P --> P" by auto
lemma foo687: "P --> P" by auto
lemma foo688: "P --> P" by auto
lemma foo689: "P --> P" by auto
lemma foo690: "P --> P" by auto
lemma foo691: "P --> P" by auto
lemma foo692: "P --> P" by auto
lemma foo693: "P --> P" by auto
lemma foo694: "P --> P" by auto
lemma foo695: "P --> P" by auto
lemma foo696: "P --> P" by auto
lemma foo697: "P --> P" by auto
lemma foo698: "P --> P" by auto
lemma foo699: "P --> P" by auto
lemma foo700: "P --> P" by auto
lemma foo701: "P --> P" by auto
lemma foo702: "P --> P" by auto
lemma foo703: "P --> P" by auto
lemma foo704: "P --> P" by auto
lemma foo705: "P --> P" by auto
lemma foo706: "P --> P" by auto
lemma foo707: "P --> P" by auto
lemma foo708: "P --> P" by auto
lemma foo709: "P --> P" by auto
lemma foo710: "P --> P" by auto
lemma foo711: "P --> P" by auto
lemma foo712: "P --> P" by auto
lemma foo713: "P --> P" by auto
lemma foo714: "P --> P" by auto
lemma foo715: "P --> P" by auto
lemma foo716: "P --> P" by auto
lemma foo717: "P --> P" by auto
lemma foo718: "P --> P" by auto
lemma foo719: "P --> P" by auto
lemma foo720: "P --> P" by auto
lemma foo721: "P --> P" by auto
lemma foo722: "P --> P" by auto
lemma foo723: "P --> P" by auto
lemma foo724: "P --> P" by auto
lemma foo725: "P --> P" by auto
lemma foo726: "P --> P" by auto
lemma foo727: "P --> P" by auto
lemma foo728: "P --> P" by auto
lemma foo729: "P --> P" by auto
lemma foo730: "P --> P" by auto
lemma foo731: "P --> P" by auto
lemma foo732: "P --> P" by auto
lemma foo733: "P --> P" by auto
lemma foo734: "P --> P" by auto
lemma foo735: "P --> P" by auto
lemma foo736: "P --> P" by auto
lemma foo737: "P --> P" by auto
lemma foo738: "P --> P" by auto
lemma foo739: "P --> P" by auto
lemma foo740: "P --> P" by auto
lemma foo741: "P --> P" by auto
lemma foo742: "P --> P" by auto
lemma foo743: "P --> P" by auto
lemma foo744: "P --> P" by auto
lemma foo745: "P --> P" by auto
lemma foo746: "P --> P" by auto
lemma foo747: "P --> P" by auto
lemma foo748: "P --> P" by auto
lemma foo749: "P --> P" by auto
lemma foo750: "P --> P" by auto
lemma foo751: "P --> P" by auto
lemma foo752: "P --> P" by auto
lemma foo753: "P --> P" by auto
lemma foo754: "P --> P" by auto
lemma foo755: "P --> P" by auto
lemma foo756: "P --> P" by auto
lemma foo757: "P --> P" by auto
lemma foo758: "P --> P" by auto
lemma foo759: "P --> P" by auto
lemma foo760: "P --> P" by auto
lemma foo761: "P --> P" by auto
lemma foo762: "P --> P" by auto
lemma foo763: "P --> P" by auto
lemma foo764: "P --> P" by auto
lemma foo765: "P --> P" by auto
lemma foo766: "P --> P" by auto
lemma foo767: "P --> P" by auto
lemma foo768: "P --> P" by auto
lemma foo769: "P --> P" by auto
lemma foo770: "P --> P" by auto
lemma foo771: "P --> P" by auto
lemma foo772: "P --> P" by auto
lemma foo773: "P --> P" by auto
lemma foo774: "P --> P" by auto
lemma foo775: "P --> P" by auto
lemma foo776: "P --> P" by auto
lemma foo777: "P --> P" by auto
lemma foo778: "P --> P" by auto
lemma foo779: "P --> P" by auto
lemma foo780: "P --> P" by auto
lemma foo781: "P --> P" by auto
lemma foo782: "P --> P" by auto
lemma foo783: "P --> P" by auto
lemma foo784: "P --> P" by auto
lemma foo785: "P --> P" by auto
lemma foo786: "P --> P" by auto
lemma foo787: "P --> P" by auto
lemma foo788: "P --> P" by auto
lemma foo789: "P --> P" by auto
lemma foo790: "P --> P" by auto
lemma foo791: "P --> P" by auto
lemma foo792: "P --> P" by auto
lemma foo793: "P --> P" by auto
lemma foo794: "P --> P" by auto
lemma foo795: "P --> P" by auto
lemma foo796: "P --> P" by auto
lemma foo797: "P --> P" by auto
lemma foo798: "P --> P" by auto
lemma foo799: "P --> P" by auto
lemma foo800: "P --> P" by auto
lemma foo801: "P --> P" by auto
lemma foo802: "P --> P" by auto
lemma foo803: "P --> P" by auto
lemma foo804: "P --> P" by auto
lemma foo805: "P --> P" by auto
lemma foo806: "P --> P" by auto
lemma foo807: "P --> P" by auto
lemma foo808: "P --> P" by auto
lemma foo809: "P --> P" by auto
lemma foo810: "P --> P" by auto
lemma foo811: "P --> P" by auto
lemma foo812: "P --> P" by auto
lemma foo813: "P --> P" by auto
lemma foo814: "P --> P" by auto
lemma foo815: "P --> P" by auto
lemma foo816: "P --> P" by auto
lemma foo817: "P --> P" by auto
lemma foo818: "P --> P" by auto
lemma foo819: "P --> P" by auto
lemma foo820: "P --> P" by auto
lemma foo821: "P --> P" by auto
lemma foo822: "P --> P" by auto
lemma foo823: "P --> P" by auto
lemma foo824: "P --> P" by auto
lemma foo825: "P --> P" by auto
lemma foo826: "P --> P" by auto
lemma foo827: "P --> P" by auto
lemma foo828: "P --> P" by auto
lemma foo829: "P --> P" by auto
lemma foo830: "P --> P" by auto
lemma foo831: "P --> P" by auto
lemma foo832: "P --> P" by auto
lemma foo833: "P --> P" by auto
lemma foo834: "P --> P" by auto
lemma foo835: "P --> P" by auto
lemma foo836: "P --> P" by auto
lemma foo837: "P --> P" by auto
lemma foo838: "P --> P" by auto
lemma foo839: "P --> P" by auto
lemma foo840: "P --> P" by auto
lemma foo841: "P --> P" by auto
lemma foo842: "P --> P" by auto
lemma foo843: "P --> P" by auto
lemma foo844: "P --> P" by auto
lemma foo845: "P --> P" by auto
lemma foo846: "P --> P" by auto
lemma foo847: "P --> P" by auto
lemma foo848: "P --> P" by auto
lemma foo849: "P --> P" by auto
lemma foo850: "P --> P" by auto
lemma foo851: "P --> P" by auto
lemma foo852: "P --> P" by auto
lemma foo853: "P --> P" by auto
lemma foo854: "P --> P" by auto
lemma foo855: "P --> P" by auto
lemma foo856: "P --> P" by auto
lemma foo857: "P --> P" by auto
lemma foo858: "P --> P" by auto
lemma foo859: "P --> P" by auto
lemma foo860: "P --> P" by auto
lemma foo861: "P --> P" by auto
lemma foo862: "P --> P" by auto
lemma foo863: "P --> P" by auto
lemma foo864: "P --> P" by auto
lemma foo865: "P --> P" by auto
lemma foo866: "P --> P" by auto
lemma foo867: "P --> P" by auto
lemma foo868: "P --> P" by auto
lemma foo869: "P --> P" by auto
lemma foo870: "P --> P" by auto
lemma foo871: "P --> P" by auto
lemma foo872: "P --> P" by auto
lemma foo873: "P --> P" by auto
lemma foo874: "P --> P" by auto
lemma foo875: "P --> P" by auto
lemma foo876: "P --> P" by auto
lemma foo877: "P --> P" by auto
lemma foo878: "P --> P" by auto
lemma foo879: "P --> P" by auto
lemma foo880: "P --> P" by auto
lemma foo881: "P --> P" by auto
lemma foo882: "P --> P" by auto
lemma foo883: "P --> P" by auto
lemma foo884: "P --> P" by auto
lemma foo885: "P --> P" by auto
lemma foo886: "P --> P" by auto
lemma foo887: "P --> P" by auto
lemma foo888: "P --> P" by auto
lemma foo889: "P --> P" by auto
lemma foo890: "P --> P" by auto
lemma foo891: "P --> P" by auto
lemma foo892: "P --> P" by auto
lemma foo893: "P --> P" by auto
lemma foo894: "P --> P" by auto
lemma foo895: "P --> P" by auto
lemma foo896: "P --> P" by auto
lemma foo897: "P --> P" by auto
lemma foo898: "P --> P" by auto
lemma foo899: "P --> P" by auto
lemma foo900: "P --> P" by auto
lemma foo901: "P --> P" by auto
lemma foo902: "P --> P" by auto
lemma foo903: "P --> P" by auto
lemma foo904: "P --> P" by auto
lemma foo905: "P --> P" by auto
lemma foo906: "P --> P" by auto
lemma foo907: "P --> P" by auto
lemma foo908: "P --> P" by auto
lemma foo909: "P --> P" by auto
lemma foo910: "P --> P" by auto
lemma foo911: "P --> P" by auto
lemma foo912: "P --> P" by auto
lemma foo913: "P --> P" by auto
lemma foo914: "P --> P" by auto
lemma foo915: "P --> P" by auto
lemma foo916: "P --> P" by auto
lemma foo917: "P --> P" by auto
lemma foo918: "P --> P" by auto
lemma foo919: "P --> P" by auto
lemma foo920: "P --> P" by auto
lemma foo921: "P --> P" by auto
lemma foo922: "P --> P" by auto
lemma foo923: "P --> P" by auto
lemma foo924: "P --> P" by auto
lemma foo925: "P --> P" by auto
lemma foo926: "P --> P" by auto
lemma foo927: "P --> P" by auto
lemma foo928: "P --> P" by auto
lemma foo929: "P --> P" by auto
lemma foo930: "P --> P" by auto
lemma foo931: "P --> P" by auto
lemma foo932: "P --> P" by auto
lemma foo933: "P --> P" by auto
lemma foo934: "P --> P" by auto
lemma foo935: "P --> P" by auto
lemma foo936: "P --> P" by auto
lemma foo937: "P --> P" by auto
lemma foo938: "P --> P" by auto
lemma foo939: "P --> P" by auto
lemma foo940: "P --> P" by auto
lemma foo941: "P --> P" by auto
lemma foo942: "P --> P" by auto
lemma foo943: "P --> P" by auto
lemma foo944: "P --> P" by auto
lemma foo945: "P --> P" by auto
lemma foo946: "P --> P" by auto
lemma foo947: "P --> P" by auto
lemma foo948: "P --> P" by auto
lemma foo949: "P --> P" by auto
lemma foo950: "P --> P" by auto
lemma foo951: "P --> P" by auto
lemma foo952: "P --> P" by auto
lemma foo953: "P --> P" by auto
lemma foo954: "P --> P" by auto
lemma foo955: "P --> P" by auto
lemma foo956: "P --> P" by auto
lemma foo957: "P --> P" by auto
lemma foo958: "P --> P" by auto
lemma foo959: "P --> P" by auto
lemma foo960: "P --> P" by auto
lemma foo961: "P --> P" by auto
lemma foo962: "P --> P" by auto
lemma foo963: "P --> P" by auto
lemma foo964: "P --> P" by auto
lemma foo965: "P --> P" by auto
lemma foo966: "P --> P" by auto
lemma foo967: "P --> P" by auto
lemma foo968: "P --> P" by auto
lemma foo969: "P --> P" by auto
lemma foo970: "P --> P" by auto
lemma foo971: "P --> P" by auto
lemma foo972: "P --> P" by auto
lemma foo973: "P --> P" by auto
lemma foo974: "P --> P" by auto
lemma foo975: "P --> P" by auto
lemma foo976: "P --> P" by auto
lemma foo977: "P --> P" by auto
lemma foo978: "P --> P" by auto
lemma foo979: "P --> P" by auto
lemma foo980: "P --> P" by auto
lemma foo981: "P --> P" by auto
lemma foo982: "P --> P" by auto
lemma foo983: "P --> P" by auto
lemma foo984: "P --> P" by auto
lemma foo985: "P --> P" by auto
lemma foo986: "P --> P" by auto
lemma foo987: "P --> P" by auto
lemma foo988: "P --> P" by auto
lemma foo989: "P --> P" by auto
lemma foo990: "P --> P" by auto
lemma foo991: "P --> P" by auto
lemma foo992: "P --> P" by auto
lemma foo993: "P --> P" by auto
lemma foo994: "P --> P" by auto
lemma foo995: "P --> P" by auto
lemma foo996: "P --> P" by auto
lemma foo997: "P --> P" by auto
lemma foo998: "P --> P" by auto
lemma foo999: "P --> P" by auto
lemma foo1000: "P --> P" by auto

ML {* warning (Timing.message (Timing.result start)) *}
(* ELISP: -- (message "Time taken: %f seconds" (time-to-seconds (time-since start))) -- *)

end