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