%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : PUZ074+1 : TPTP v8.1.0. Released v3.5.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n019.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 600s % DateTime : Mon Jul 18 18:33:42 EDT 2022 % Result : Theorem 2.92s 3.12s % Output : Proof 3.01s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.10 % Problem : PUZ074+1 : TPTP v8.1.0. Released v3.5.0. % 0.00/0.10 % Command : run_zenon %s %d % 0.09/0.30 % Computer : n019.cluster.edu % 0.09/0.30 % Model : x86_64 x86_64 % 0.09/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.30 % Memory : 8042.1875MB % 0.09/0.30 % OS : Linux 3.10.0-693.el7.x86_64 % 0.09/0.31 % CPULimit : 300 % 0.09/0.31 % WCLimit : 600 % 0.09/0.31 % DateTime : Sun May 29 00:25:10 EDT 2022 % 0.09/0.31 % CPUTime : % 2.92/3.12 (* PROOF-FOUND *) % 2.92/3.12 % SZS status Theorem % 2.92/3.12 (* BEGIN-PROOF *) % 2.92/3.12 % SZS output start Proof % 2.92/3.12 Theorem tlhfof29942 : (~(adj (cell1) (cell100))). % 2.92/3.12 Proof. % 2.92/3.12 apply NNPP. intro zenon_G. % 2.92/3.12 apply zenon_G. zenon_intro zenon_H1359. % 2.92/3.12 generalize (tlhfof24991 (cell100)). zenon_intro zenon_H135a. % 2.92/3.12 generalize (zenon_H135a (cell1)). zenon_intro zenon_H135b. % 2.92/3.12 apply (zenon_equiv_s _ _ zenon_H135b); [ zenon_intro zenon_H135e; zenon_intro zenon_H135d | zenon_intro zenon_H1359; zenon_intro zenon_H135c ]. % 2.92/3.12 exact (zenon_H135e zenon_H1359). % 2.92/3.12 apply (zenon_or_s _ _ zenon_H135c); [ zenon_intro zenon_H1360 | zenon_intro zenon_H135f ]. % 2.92/3.12 generalize (tlhfof24990 (cell100)). zenon_intro zenon_H1361. % 2.92/3.12 generalize (zenon_H1361 (cell1)). zenon_intro zenon_H1362. % 2.92/3.12 apply (zenon_equiv_s _ _ zenon_H1362); [ zenon_intro zenon_H1365; zenon_intro zenon_H1364 | zenon_intro zenon_H1360; zenon_intro zenon_H1363 ]. % 2.92/3.12 exact (zenon_H1365 zenon_H1360). % 2.92/3.12 apply (zenon_or_s _ _ zenon_H1363); [ zenon_intro zenon_H1367 | zenon_intro zenon_H1366 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H1367). zenon_intro zenon_H1369. zenon_intro zenon_H1368. % 2.92/3.12 apply tlhfof29940. apply sym_equal. exact zenon_H1368. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H1366); [ zenon_intro zenon_H136b | zenon_intro zenon_H136a ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H136b). zenon_intro zenon_H136d. zenon_intro zenon_H136c. % 2.92/3.12 apply tlhfof29939. apply sym_equal. exact zenon_H136d. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H136a); [ zenon_intro zenon_H136f | zenon_intro zenon_H136e ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H136f). zenon_intro zenon_H1371. zenon_intro zenon_H1370. % 2.92/3.12 apply tlhfof29937. apply sym_equal. exact zenon_H1371. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H136e); [ zenon_intro zenon_H1373 | zenon_intro zenon_H1372 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H1373). zenon_intro zenon_H1375. zenon_intro zenon_H1374. % 2.92/3.12 apply tlhfof29934. apply sym_equal. exact zenon_H1375. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H1372); [ zenon_intro zenon_H1377 | zenon_intro zenon_H1376 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H1377). zenon_intro zenon_H1379. zenon_intro zenon_H1378. % 2.92/3.12 apply tlhfof29930. apply sym_equal. exact zenon_H1379. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H1376); [ zenon_intro zenon_H137b | zenon_intro zenon_H137a ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H137b). zenon_intro zenon_H137d. zenon_intro zenon_H137c. % 2.92/3.12 apply tlhfof29925. apply sym_equal. exact zenon_H137d. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H137a); [ zenon_intro zenon_H137f | zenon_intro zenon_H137e ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H137f). zenon_intro zenon_H1381. zenon_intro zenon_H1380. % 2.92/3.12 apply tlhfof29919. apply sym_equal. exact zenon_H1381. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H137e); [ zenon_intro zenon_H1383 | zenon_intro zenon_H1382 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H1383). zenon_intro zenon_H1385. zenon_intro zenon_H1384. % 2.92/3.12 apply tlhfof29912. apply sym_equal. exact zenon_H1385. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H1382); [ zenon_intro zenon_H1387 | zenon_intro zenon_H1386 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H1387). zenon_intro zenon_H1389. zenon_intro zenon_H1388. % 2.92/3.12 apply tlhfof29904. apply sym_equal. exact zenon_H1389. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H1386); [ zenon_intro zenon_H138b | zenon_intro zenon_H138a ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H138b). zenon_intro zenon_H138d. zenon_intro zenon_H138c. % 2.92/3.12 apply tlhfof29874. apply sym_equal. exact zenon_H138d. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H138a); [ zenon_intro zenon_H138f | zenon_intro zenon_H138e ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H138f). zenon_intro zenon_H1391. zenon_intro zenon_H1390. % 2.92/3.12 apply tlhfof29885. apply sym_equal. exact zenon_H1391. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H138e); [ zenon_intro zenon_H1393 | zenon_intro zenon_H1392 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H1393). zenon_intro zenon_H1395. zenon_intro zenon_H1394. % 2.92/3.12 apply tlhfof29862. apply sym_equal. exact zenon_H1395. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H1392); [ zenon_intro zenon_H1397 | zenon_intro zenon_H1396 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H1397). zenon_intro zenon_H1399. zenon_intro zenon_H1398. % 2.92/3.12 apply tlhfof29849. apply sym_equal. exact zenon_H1399. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H1396); [ zenon_intro zenon_H139b | zenon_intro zenon_H139a ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H139b). zenon_intro zenon_H139d. zenon_intro zenon_H139c. % 2.92/3.12 apply tlhfof29835. apply sym_equal. exact zenon_H139d. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H139a); [ zenon_intro zenon_H139f | zenon_intro zenon_H139e ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H139f). zenon_intro zenon_H13a1. zenon_intro zenon_H13a0. % 2.92/3.12 apply tlhfof29820. apply sym_equal. exact zenon_H13a1. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H139e); [ zenon_intro zenon_H13a3 | zenon_intro zenon_H13a2 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H13a3). zenon_intro zenon_H13a5. zenon_intro zenon_H13a4. % 2.92/3.12 apply tlhfof29804. apply sym_equal. exact zenon_H13a5. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H13a2); [ zenon_intro zenon_H13a7 | zenon_intro zenon_H13a6 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H13a7). zenon_intro zenon_H13a9. zenon_intro zenon_H13a8. % 2.92/3.12 apply tlhfof29787. apply sym_equal. exact zenon_H13a9. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H13a6); [ zenon_intro zenon_H13ab | zenon_intro zenon_H13aa ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H13ab). zenon_intro zenon_H13ad. zenon_intro zenon_H13ac. % 2.92/3.12 apply tlhfof29769. apply sym_equal. exact zenon_H13ad. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H13aa); [ zenon_intro zenon_H13af | zenon_intro zenon_H13ae ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H13af). zenon_intro zenon_H13b1. zenon_intro zenon_H13b0. % 2.92/3.12 apply tlhfof29709. apply sym_equal. exact zenon_H13b1. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H13ae); [ zenon_intro zenon_H13b3 | zenon_intro zenon_H13b2 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H13b3). zenon_intro zenon_H13b5. zenon_intro zenon_H13b4. % 2.92/3.12 apply tlhfof29730. apply sym_equal. exact zenon_H13b5. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H13b2); [ zenon_intro zenon_H13b7 | zenon_intro zenon_H13b6 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H13b7). zenon_intro zenon_H13b9. zenon_intro zenon_H13b8. % 2.92/3.12 apply tlhfof29687. apply sym_equal. exact zenon_H13b9. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H13b6); [ zenon_intro zenon_H13bb | zenon_intro zenon_H13ba ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H13bb). zenon_intro zenon_H13bd. zenon_intro zenon_H13bc. % 2.92/3.12 apply tlhfof29664. apply sym_equal. exact zenon_H13bd. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H13ba); [ zenon_intro zenon_H13bf | zenon_intro zenon_H13be ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H13bf). zenon_intro zenon_H13c1. zenon_intro zenon_H13c0. % 2.92/3.12 apply tlhfof29640. apply sym_equal. exact zenon_H13c1. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H13be); [ zenon_intro zenon_H13c3 | zenon_intro zenon_H13c2 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H13c3). zenon_intro zenon_H13c5. zenon_intro zenon_H13c4. % 2.92/3.12 apply tlhfof29615. apply sym_equal. exact zenon_H13c5. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H13c2); [ zenon_intro zenon_H13c7 | zenon_intro zenon_H13c6 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H13c7). zenon_intro zenon_H13c9. zenon_intro zenon_H13c8. % 2.92/3.12 apply tlhfof29589. apply sym_equal. exact zenon_H13c9. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H13c6); [ zenon_intro zenon_H13cb | zenon_intro zenon_H13ca ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H13cb). zenon_intro zenon_H13cd. zenon_intro zenon_H13cc. % 2.92/3.12 apply tlhfof29562. apply sym_equal. exact zenon_H13cd. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H13ca); [ zenon_intro zenon_H13cf | zenon_intro zenon_H13ce ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H13cf). zenon_intro zenon_H13d1. zenon_intro zenon_H13d0. % 2.92/3.12 apply tlhfof29534. apply sym_equal. exact zenon_H13d1. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H13ce); [ zenon_intro zenon_H13d3 | zenon_intro zenon_H13d2 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H13d3). zenon_intro zenon_H13d5. zenon_intro zenon_H13d4. % 2.92/3.12 apply tlhfof29444. apply sym_equal. exact zenon_H13d5. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H13d2); [ zenon_intro zenon_H13d7 | zenon_intro zenon_H13d6 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H13d7). zenon_intro zenon_H13d9. zenon_intro zenon_H13d8. % 2.92/3.12 apply tlhfof29475. apply sym_equal. exact zenon_H13d9. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H13d6); [ zenon_intro zenon_H13db | zenon_intro zenon_H13da ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H13db). zenon_intro zenon_H13dd. zenon_intro zenon_H13dc. % 2.92/3.12 apply tlhfof29412. apply sym_equal. exact zenon_H13dd. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H13da); [ zenon_intro zenon_H13df | zenon_intro zenon_H13de ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H13df). zenon_intro zenon_H13e1. zenon_intro zenon_H13e0. % 2.92/3.12 apply tlhfof29379. apply sym_equal. exact zenon_H13e1. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H13de); [ zenon_intro zenon_H13e3 | zenon_intro zenon_H13e2 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H13e3). zenon_intro zenon_H13e5. zenon_intro zenon_H13e4. % 2.92/3.12 apply tlhfof29345. apply sym_equal. exact zenon_H13e5. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H13e2); [ zenon_intro zenon_H13e7 | zenon_intro zenon_H13e6 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H13e7). zenon_intro zenon_H13e9. zenon_intro zenon_H13e8. % 2.92/3.12 apply tlhfof29310. apply sym_equal. exact zenon_H13e9. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H13e6); [ zenon_intro zenon_H13eb | zenon_intro zenon_H13ea ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H13eb). zenon_intro zenon_H13ed. zenon_intro zenon_H13ec. % 2.92/3.12 apply tlhfof29274. apply sym_equal. exact zenon_H13ed. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H13ea); [ zenon_intro zenon_H13ef | zenon_intro zenon_H13ee ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H13ef). zenon_intro zenon_H13f1. zenon_intro zenon_H13f0. % 2.92/3.12 apply tlhfof29237. apply sym_equal. exact zenon_H13f1. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H13ee); [ zenon_intro zenon_H13f3 | zenon_intro zenon_H13f2 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H13f3). zenon_intro zenon_H13f5. zenon_intro zenon_H13f4. % 2.92/3.12 apply tlhfof29199. apply sym_equal. exact zenon_H13f5. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H13f2); [ zenon_intro zenon_H13f7 | zenon_intro zenon_H13f6 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H13f7). zenon_intro zenon_H13f9. zenon_intro zenon_H13f8. % 2.92/3.12 apply tlhfof29079. apply sym_equal. exact zenon_H13f9. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H13f6); [ zenon_intro zenon_H13fb | zenon_intro zenon_H13fa ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H13fb). zenon_intro zenon_H13fd. zenon_intro zenon_H13fc. % 2.92/3.12 apply tlhfof29120. apply sym_equal. exact zenon_H13fd. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H13fa); [ zenon_intro zenon_H13ff | zenon_intro zenon_H13fe ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H13ff). zenon_intro zenon_H1401. zenon_intro zenon_H1400. % 2.92/3.12 apply tlhfof29037. apply sym_equal. exact zenon_H1401. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H13fe); [ zenon_intro zenon_H1403 | zenon_intro zenon_H1402 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H1403). zenon_intro zenon_H1405. zenon_intro zenon_H1404. % 2.92/3.12 apply tlhfof28994. apply sym_equal. exact zenon_H1405. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H1402); [ zenon_intro zenon_H1407 | zenon_intro zenon_H1406 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H1407). zenon_intro zenon_H1409. zenon_intro zenon_H1408. % 2.92/3.12 apply tlhfof28950. apply sym_equal. exact zenon_H1409. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H1406); [ zenon_intro zenon_H140b | zenon_intro zenon_H140a ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H140b). zenon_intro zenon_H140d. zenon_intro zenon_H140c. % 2.92/3.12 apply tlhfof28905. apply sym_equal. exact zenon_H140d. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H140a); [ zenon_intro zenon_H140f | zenon_intro zenon_H140e ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H140f). zenon_intro zenon_H1411. zenon_intro zenon_H1410. % 2.92/3.12 apply tlhfof28859. apply sym_equal. exact zenon_H1411. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H140e); [ zenon_intro zenon_H1413 | zenon_intro zenon_H1412 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H1413). zenon_intro zenon_H1415. zenon_intro zenon_H1414. % 2.92/3.12 apply tlhfof28812. apply sym_equal. exact zenon_H1415. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H1412); [ zenon_intro zenon_H1417 | zenon_intro zenon_H1416 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H1417). zenon_intro zenon_H1419. zenon_intro zenon_H1418. % 2.92/3.12 apply tlhfof28764. apply sym_equal. exact zenon_H1419. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H1416); [ zenon_intro zenon_H141b | zenon_intro zenon_H141a ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H141b). zenon_intro zenon_H141d. zenon_intro zenon_H141c. % 2.92/3.12 apply tlhfof28614. apply sym_equal. exact zenon_H141d. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H141a); [ zenon_intro zenon_H141f | zenon_intro zenon_H141e ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H141f). zenon_intro zenon_H1421. zenon_intro zenon_H1420. % 2.92/3.12 apply tlhfof28665. apply sym_equal. exact zenon_H1421. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H141e); [ zenon_intro zenon_H1423 | zenon_intro zenon_H1422 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H1423). zenon_intro zenon_H1425. zenon_intro zenon_H1424. % 2.92/3.12 apply tlhfof28562. apply sym_equal. exact zenon_H1425. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H1422); [ zenon_intro zenon_H1427 | zenon_intro zenon_H1426 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H1427). zenon_intro zenon_H1429. zenon_intro zenon_H1428. % 2.92/3.12 apply tlhfof28509. apply sym_equal. exact zenon_H1429. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H1426); [ zenon_intro zenon_H142b | zenon_intro zenon_H142a ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H142b). zenon_intro zenon_H142d. zenon_intro zenon_H142c. % 2.92/3.12 apply tlhfof28455. apply sym_equal. exact zenon_H142d. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H142a); [ zenon_intro zenon_H142f | zenon_intro zenon_H142e ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H142f). zenon_intro zenon_H1431. zenon_intro zenon_H1430. % 2.92/3.12 apply tlhfof28400. apply sym_equal. exact zenon_H1431. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H142e); [ zenon_intro zenon_H1433 | zenon_intro zenon_H1432 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H1433). zenon_intro zenon_H1435. zenon_intro zenon_H1434. % 2.92/3.12 apply tlhfof28344. apply sym_equal. exact zenon_H1435. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H1432); [ zenon_intro zenon_H1437 | zenon_intro zenon_H1436 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H1437). zenon_intro zenon_H1439. zenon_intro zenon_H1438. % 2.92/3.12 apply tlhfof28287. apply sym_equal. exact zenon_H1439. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H1436); [ zenon_intro zenon_H143b | zenon_intro zenon_H143a ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H143b). zenon_intro zenon_H143d. zenon_intro zenon_H143c. % 2.92/3.12 apply tlhfof28229. apply sym_equal. exact zenon_H143d. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H143a); [ zenon_intro zenon_H143f | zenon_intro zenon_H143e ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H143f). zenon_intro zenon_H1441. zenon_intro zenon_H1440. % 2.92/3.12 apply tlhfof28049. apply sym_equal. exact zenon_H1441. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H143e); [ zenon_intro zenon_H1443 | zenon_intro zenon_H1442 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H1443). zenon_intro zenon_H1445. zenon_intro zenon_H1444. % 2.92/3.12 apply tlhfof28110. apply sym_equal. exact zenon_H1445. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H1442); [ zenon_intro zenon_H1447 | zenon_intro zenon_H1446 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H1447). zenon_intro zenon_H1449. zenon_intro zenon_H1448. % 2.92/3.12 apply tlhfof27987. apply sym_equal. exact zenon_H1449. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H1446); [ zenon_intro zenon_H144b | zenon_intro zenon_H144a ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H144b). zenon_intro zenon_H144d. zenon_intro zenon_H144c. % 2.92/3.12 apply tlhfof27924. apply sym_equal. exact zenon_H144d. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H144a); [ zenon_intro zenon_H144f | zenon_intro zenon_H144e ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H144f). zenon_intro zenon_H1451. zenon_intro zenon_H1450. % 2.92/3.12 apply tlhfof27860. apply sym_equal. exact zenon_H1451. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H144e); [ zenon_intro zenon_H1453 | zenon_intro zenon_H1452 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H1453). zenon_intro zenon_H1455. zenon_intro zenon_H1454. % 2.92/3.12 apply tlhfof27795. apply sym_equal. exact zenon_H1455. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H1452); [ zenon_intro zenon_H1457 | zenon_intro zenon_H1456 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H1457). zenon_intro zenon_H1459. zenon_intro zenon_H1458. % 2.92/3.12 apply tlhfof27729. apply sym_equal. exact zenon_H1459. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H1456); [ zenon_intro zenon_H145b | zenon_intro zenon_H145a ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H145b). zenon_intro zenon_H145d. zenon_intro zenon_H145c. % 2.92/3.12 apply tlhfof27662. apply sym_equal. exact zenon_H145d. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H145a); [ zenon_intro zenon_H145f | zenon_intro zenon_H145e ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H145f). zenon_intro zenon_H1461. zenon_intro zenon_H1460. % 2.92/3.12 apply tlhfof27594. apply sym_equal. exact zenon_H1461. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H145e); [ zenon_intro zenon_H1463 | zenon_intro zenon_H1462 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H1463). zenon_intro zenon_H1465. zenon_intro zenon_H1464. % 2.92/3.12 apply tlhfof27384. apply sym_equal. exact zenon_H1465. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H1462); [ zenon_intro zenon_H1467 | zenon_intro zenon_H1466 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H1467). zenon_intro zenon_H1469. zenon_intro zenon_H1468. % 2.92/3.12 apply tlhfof27455. apply sym_equal. exact zenon_H1469. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H1466); [ zenon_intro zenon_H146b | zenon_intro zenon_H146a ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H146b). zenon_intro zenon_H146d. zenon_intro zenon_H146c. % 2.92/3.12 apply tlhfof27312. apply sym_equal. exact zenon_H146d. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H146a); [ zenon_intro zenon_H146f | zenon_intro zenon_H146e ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H146f). zenon_intro zenon_H1471. zenon_intro zenon_H1470. % 2.92/3.12 apply tlhfof27239. apply sym_equal. exact zenon_H1471. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H146e); [ zenon_intro zenon_H1473 | zenon_intro zenon_H1472 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H1473). zenon_intro zenon_H1475. zenon_intro zenon_H1474. % 2.92/3.12 apply tlhfof27165. apply sym_equal. exact zenon_H1475. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H1472); [ zenon_intro zenon_H1477 | zenon_intro zenon_H1476 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H1477). zenon_intro zenon_H1479. zenon_intro zenon_H1478. % 2.92/3.12 apply tlhfof27090. apply sym_equal. exact zenon_H1479. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H1476); [ zenon_intro zenon_H147b | zenon_intro zenon_H147a ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H147b). zenon_intro zenon_H147d. zenon_intro zenon_H147c. % 2.92/3.12 apply tlhfof27014. apply sym_equal. exact zenon_H147d. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H147a); [ zenon_intro zenon_H147f | zenon_intro zenon_H147e ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H147f). zenon_intro zenon_H1481. zenon_intro zenon_H1480. % 2.92/3.12 apply tlhfof26937. apply sym_equal. exact zenon_H1481. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H147e); [ zenon_intro zenon_H1483 | zenon_intro zenon_H1482 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H1483). zenon_intro zenon_H1485. zenon_intro zenon_H1484. % 2.92/3.12 apply tlhfof26859. apply sym_equal. exact zenon_H1485. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H1482); [ zenon_intro zenon_H1487 | zenon_intro zenon_H1486 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H1487). zenon_intro zenon_H1489. zenon_intro zenon_H1488. % 2.92/3.12 apply tlhfof26619. apply sym_equal. exact zenon_H1489. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H1486); [ zenon_intro zenon_H148b | zenon_intro zenon_H148a ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H148b). zenon_intro zenon_H148d. zenon_intro zenon_H148c. % 2.92/3.12 apply tlhfof26700. apply sym_equal. exact zenon_H148d. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H148a); [ zenon_intro zenon_H148f | zenon_intro zenon_H148e ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H148f). zenon_intro zenon_H1491. zenon_intro zenon_H1490. % 2.92/3.12 apply tlhfof26537. apply sym_equal. exact zenon_H1491. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H148e); [ zenon_intro zenon_H1493 | zenon_intro zenon_H1492 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H1493). zenon_intro zenon_H1495. zenon_intro zenon_H1494. % 2.92/3.12 apply tlhfof26454. apply sym_equal. exact zenon_H1495. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H1492); [ zenon_intro zenon_H1497 | zenon_intro zenon_H1496 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H1497). zenon_intro zenon_H1499. zenon_intro zenon_H1498. % 2.92/3.12 apply tlhfof26370. apply sym_equal. exact zenon_H1499. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H1496); [ zenon_intro zenon_H149b | zenon_intro zenon_H149a ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H149b). zenon_intro zenon_H149d. zenon_intro zenon_H149c. % 2.92/3.12 apply tlhfof26285. apply sym_equal. exact zenon_H149d. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H149a); [ zenon_intro zenon_H149f | zenon_intro zenon_H149e ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H149f). zenon_intro zenon_H14a1. zenon_intro zenon_H14a0. % 2.92/3.12 apply tlhfof26199. apply sym_equal. exact zenon_H14a1. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H149e); [ zenon_intro zenon_H14a3 | zenon_intro zenon_H14a2 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H14a3). zenon_intro zenon_H14a5. zenon_intro zenon_H14a4. % 2.92/3.12 apply tlhfof26112. apply sym_equal. exact zenon_H14a5. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H14a2); [ zenon_intro zenon_H14a7 | zenon_intro zenon_H14a6 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H14a7). zenon_intro zenon_H14a9. zenon_intro zenon_H14a8. % 2.92/3.12 apply tlhfof26024. apply sym_equal. exact zenon_H14a9. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H14a6); [ zenon_intro zenon_H14ab | zenon_intro zenon_H14aa ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H14ab). zenon_intro zenon_H14ad. zenon_intro zenon_H14ac. % 2.92/3.12 apply tlhfof25754. apply sym_equal. exact zenon_H14ad. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H14aa); [ zenon_intro zenon_H14af | zenon_intro zenon_H14ae ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H14af). zenon_intro zenon_H14b1. zenon_intro zenon_H14b0. % 2.92/3.12 apply tlhfof25845. apply sym_equal. exact zenon_H14b1. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H14ae); [ zenon_intro zenon_H14b3 | zenon_intro zenon_H14b2 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H14b3). zenon_intro zenon_H14b5. zenon_intro zenon_H14b4. % 2.92/3.12 apply tlhfof25662. apply sym_equal. exact zenon_H14b5. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H14b2); [ zenon_intro zenon_H14b7 | zenon_intro zenon_H14b6 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H14b7). zenon_intro zenon_H14b9. zenon_intro zenon_H14b8. % 2.92/3.12 apply tlhfof25569. apply sym_equal. exact zenon_H14b9. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H14b6); [ zenon_intro zenon_H14bb | zenon_intro zenon_H14ba ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H14bb). zenon_intro zenon_H14bd. zenon_intro zenon_H14bc. % 2.92/3.12 apply tlhfof25475. apply sym_equal. exact zenon_H14bd. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H14ba); [ zenon_intro zenon_H14bf | zenon_intro zenon_H14be ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H14bf). zenon_intro zenon_H14c1. zenon_intro zenon_H14c0. % 2.92/3.12 apply tlhfof25380. apply sym_equal. exact zenon_H14c1. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H14be); [ zenon_intro zenon_H14c3 | zenon_intro zenon_H14c2 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H14c3). zenon_intro zenon_H14c5. zenon_intro zenon_H14c4. % 2.92/3.12 apply tlhfof25284. apply sym_equal. exact zenon_H14c5. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H14c2); [ zenon_intro zenon_H14c7 | zenon_intro zenon_H14c6 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H14c7). zenon_intro zenon_H14c9. zenon_intro zenon_H14c8. % 2.92/3.12 apply tlhfof25187. apply sym_equal. exact zenon_H14c9. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H14c6); [ zenon_intro zenon_H14cb | zenon_intro zenon_H14ca ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H14cb). zenon_intro zenon_H14cd. zenon_intro zenon_H14cc. % 2.92/3.12 apply tlhfof25089. apply sym_equal. exact zenon_H14cd. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H14ca); [ zenon_intro zenon_H14cf | zenon_intro zenon_H14ce ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H14cf). zenon_intro zenon_H1369. zenon_intro zenon_H14d0. % 2.92/3.12 apply tlhfof29875. apply sym_equal. exact zenon_H14d0. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H14ce); [ zenon_intro zenon_H14d2 | zenon_intro zenon_H14d1 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H14d2). zenon_intro zenon_H136d. zenon_intro zenon_H138c. % 2.92/3.12 apply tlhfof29939. apply sym_equal. exact zenon_H136d. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H14d1); [ zenon_intro zenon_H14d4 | zenon_intro zenon_H14d3 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H14d4). zenon_intro zenon_H1371. zenon_intro zenon_H1390. % 2.92/3.12 apply tlhfof29937. apply sym_equal. exact zenon_H1371. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H14d3); [ zenon_intro zenon_H14d6 | zenon_intro zenon_H14d5 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H14d6). zenon_intro zenon_H1375. zenon_intro zenon_H1394. % 2.92/3.12 apply tlhfof29934. apply sym_equal. exact zenon_H1375. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H14d5); [ zenon_intro zenon_H14d8 | zenon_intro zenon_H14d7 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H14d8). zenon_intro zenon_H1379. zenon_intro zenon_H1398. % 2.92/3.12 apply tlhfof29930. apply sym_equal. exact zenon_H1379. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H14d7); [ zenon_intro zenon_H14da | zenon_intro zenon_H14d9 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H14da). zenon_intro zenon_H137d. zenon_intro zenon_H139c. % 2.92/3.12 apply tlhfof29925. apply sym_equal. exact zenon_H137d. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H14d9); [ zenon_intro zenon_H14dc | zenon_intro zenon_H14db ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H14dc). zenon_intro zenon_H1381. zenon_intro zenon_H13a0. % 2.92/3.12 apply tlhfof29919. apply sym_equal. exact zenon_H1381. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H14db); [ zenon_intro zenon_H14de | zenon_intro zenon_H14dd ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H14de). zenon_intro zenon_H1385. zenon_intro zenon_H13a4. % 2.92/3.12 apply tlhfof29912. apply sym_equal. exact zenon_H1385. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H14dd); [ zenon_intro zenon_H14e0 | zenon_intro zenon_H14df ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H14e0). zenon_intro zenon_H1389. zenon_intro zenon_H13a8. % 2.92/3.12 apply tlhfof29904. apply sym_equal. exact zenon_H1389. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H14df); [ zenon_intro zenon_H14e2 | zenon_intro zenon_H14e1 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H14e2). zenon_intro zenon_H14e3. zenon_intro zenon_H13ac. % 2.92/3.12 apply tlhfof29895. apply sym_equal. exact zenon_H14e3. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H14e1); [ zenon_intro zenon_H14e5 | zenon_intro zenon_H14e4 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H14e5). zenon_intro zenon_H138d. zenon_intro zenon_H14e6. % 2.92/3.12 apply tlhfof29874. apply sym_equal. exact zenon_H138d. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H14e4); [ zenon_intro zenon_H14e8 | zenon_intro zenon_H14e7 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H14e8). zenon_intro zenon_H1391. zenon_intro zenon_H13b0. % 2.92/3.12 apply tlhfof29885. apply sym_equal. exact zenon_H1391. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H14e7); [ zenon_intro zenon_H14ea | zenon_intro zenon_H14e9 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H14ea). zenon_intro zenon_H1395. zenon_intro zenon_H13b4. % 2.92/3.12 apply tlhfof29862. apply sym_equal. exact zenon_H1395. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H14e9); [ zenon_intro zenon_H14ec | zenon_intro zenon_H14eb ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H14ec). zenon_intro zenon_H1399. zenon_intro zenon_H13b8. % 2.92/3.12 apply tlhfof29849. apply sym_equal. exact zenon_H1399. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H14eb); [ zenon_intro zenon_H14ee | zenon_intro zenon_H14ed ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H14ee). zenon_intro zenon_H139d. zenon_intro zenon_H13bc. % 2.92/3.12 apply tlhfof29835. apply sym_equal. exact zenon_H139d. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H14ed); [ zenon_intro zenon_H14f0 | zenon_intro zenon_H14ef ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H14f0). zenon_intro zenon_H13a1. zenon_intro zenon_H13c0. % 2.92/3.12 apply tlhfof29820. apply sym_equal. exact zenon_H13a1. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H14ef); [ zenon_intro zenon_H14f2 | zenon_intro zenon_H14f1 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H14f2). zenon_intro zenon_H13a5. zenon_intro zenon_H13c4. % 2.92/3.12 apply tlhfof29804. apply sym_equal. exact zenon_H13a5. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H14f1); [ zenon_intro zenon_H14f4 | zenon_intro zenon_H14f3 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H14f4). zenon_intro zenon_H13a9. zenon_intro zenon_H13c8. % 2.92/3.12 apply tlhfof29787. apply sym_equal. exact zenon_H13a9. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H14f3); [ zenon_intro zenon_H14f6 | zenon_intro zenon_H14f5 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H14f6). zenon_intro zenon_H13ad. zenon_intro zenon_H13cc. % 2.92/3.12 apply tlhfof29769. apply sym_equal. exact zenon_H13ad. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H14f5); [ zenon_intro zenon_H14f8 | zenon_intro zenon_H14f7 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H14f8). zenon_intro zenon_H14f9. zenon_intro zenon_H13d0. % 2.92/3.12 apply tlhfof29750. apply sym_equal. exact zenon_H14f9. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H14f7); [ zenon_intro zenon_H14fb | zenon_intro zenon_H14fa ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H14fb). zenon_intro zenon_H13b1. zenon_intro zenon_H14fc. % 2.92/3.12 apply tlhfof29709. apply sym_equal. exact zenon_H13b1. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H14fa); [ zenon_intro zenon_H14fe | zenon_intro zenon_H14fd ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H14fe). zenon_intro zenon_H13b5. zenon_intro zenon_H13d4. % 2.92/3.12 apply tlhfof29730. apply sym_equal. exact zenon_H13b5. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H14fd); [ zenon_intro zenon_H1500 | zenon_intro zenon_H14ff ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H1500). zenon_intro zenon_H13b9. zenon_intro zenon_H13d8. % 2.92/3.12 apply tlhfof29687. apply sym_equal. exact zenon_H13b9. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H14ff); [ zenon_intro zenon_H1502 | zenon_intro zenon_H1501 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H1502). zenon_intro zenon_H13bd. zenon_intro zenon_H13dc. % 2.92/3.12 apply tlhfof29664. apply sym_equal. exact zenon_H13bd. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H1501); [ zenon_intro zenon_H1504 | zenon_intro zenon_H1503 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H1504). zenon_intro zenon_H13c1. zenon_intro zenon_H13e0. % 2.92/3.12 apply tlhfof29640. apply sym_equal. exact zenon_H13c1. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H1503); [ zenon_intro zenon_H1506 | zenon_intro zenon_H1505 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H1506). zenon_intro zenon_H13c5. zenon_intro zenon_H13e4. % 2.92/3.12 apply tlhfof29615. apply sym_equal. exact zenon_H13c5. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H1505); [ zenon_intro zenon_H1508 | zenon_intro zenon_H1507 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H1508). zenon_intro zenon_H13c9. zenon_intro zenon_H13e8. % 2.92/3.12 apply tlhfof29589. apply sym_equal. exact zenon_H13c9. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H1507); [ zenon_intro zenon_H150a | zenon_intro zenon_H1509 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H150a). zenon_intro zenon_H13cd. zenon_intro zenon_H13ec. % 2.92/3.12 apply tlhfof29562. apply sym_equal. exact zenon_H13cd. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H1509); [ zenon_intro zenon_H150c | zenon_intro zenon_H150b ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H150c). zenon_intro zenon_H13d1. zenon_intro zenon_H13f0. % 2.92/3.12 apply tlhfof29534. apply sym_equal. exact zenon_H13d1. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H150b); [ zenon_intro zenon_H150e | zenon_intro zenon_H150d ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H150e). zenon_intro zenon_H150f. zenon_intro zenon_H13f4. % 2.92/3.12 apply tlhfof29505. apply sym_equal. exact zenon_H150f. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H150d); [ zenon_intro zenon_H1511 | zenon_intro zenon_H1510 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H1511). zenon_intro zenon_H13d5. zenon_intro zenon_H1512. % 2.92/3.12 apply tlhfof29444. apply sym_equal. exact zenon_H13d5. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H1510); [ zenon_intro zenon_H1514 | zenon_intro zenon_H1513 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H1514). zenon_intro zenon_H13d9. zenon_intro zenon_H13f8. % 2.92/3.12 apply tlhfof29475. apply sym_equal. exact zenon_H13d9. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H1513); [ zenon_intro zenon_H1516 | zenon_intro zenon_H1515 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H1516). zenon_intro zenon_H13dd. zenon_intro zenon_H13fc. % 2.92/3.12 apply tlhfof29412. apply sym_equal. exact zenon_H13dd. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H1515); [ zenon_intro zenon_H1518 | zenon_intro zenon_H1517 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H1518). zenon_intro zenon_H13e1. zenon_intro zenon_H1400. % 2.92/3.12 apply tlhfof29379. apply sym_equal. exact zenon_H13e1. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H1517); [ zenon_intro zenon_H151a | zenon_intro zenon_H1519 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H151a). zenon_intro zenon_H13e5. zenon_intro zenon_H1404. % 2.92/3.12 apply tlhfof29345. apply sym_equal. exact zenon_H13e5. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H1519); [ zenon_intro zenon_H151c | zenon_intro zenon_H151b ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H151c). zenon_intro zenon_H13e9. zenon_intro zenon_H1408. % 2.92/3.12 apply tlhfof29310. apply sym_equal. exact zenon_H13e9. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H151b); [ zenon_intro zenon_H151e | zenon_intro zenon_H151d ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H151e). zenon_intro zenon_H13ed. zenon_intro zenon_H140c. % 2.92/3.12 apply tlhfof29274. apply sym_equal. exact zenon_H13ed. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H151d); [ zenon_intro zenon_H1520 | zenon_intro zenon_H151f ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H1520). zenon_intro zenon_H13f1. zenon_intro zenon_H1410. % 2.92/3.12 apply tlhfof29237. apply sym_equal. exact zenon_H13f1. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H151f); [ zenon_intro zenon_H1522 | zenon_intro zenon_H1521 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H1522). zenon_intro zenon_H13f5. zenon_intro zenon_H1414. % 2.92/3.12 apply tlhfof29199. apply sym_equal. exact zenon_H13f5. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H1521); [ zenon_intro zenon_H1524 | zenon_intro zenon_H1523 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H1524). zenon_intro zenon_H1525. zenon_intro zenon_H1418. % 2.92/3.12 apply tlhfof29160. apply sym_equal. exact zenon_H1525. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H1523); [ zenon_intro zenon_H1527 | zenon_intro zenon_H1526 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H1527). zenon_intro zenon_H13f9. zenon_intro zenon_H1528. % 2.92/3.12 apply tlhfof29079. apply sym_equal. exact zenon_H13f9. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H1526); [ zenon_intro zenon_H152a | zenon_intro zenon_H1529 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H152a). zenon_intro zenon_H13fd. zenon_intro zenon_H141c. % 2.92/3.12 apply tlhfof29120. apply sym_equal. exact zenon_H13fd. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H1529); [ zenon_intro zenon_H152c | zenon_intro zenon_H152b ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H152c). zenon_intro zenon_H1401. zenon_intro zenon_H1420. % 2.92/3.12 apply tlhfof29037. apply sym_equal. exact zenon_H1401. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H152b); [ zenon_intro zenon_H152e | zenon_intro zenon_H152d ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H152e). zenon_intro zenon_H1405. zenon_intro zenon_H1424. % 2.92/3.12 apply tlhfof28994. apply sym_equal. exact zenon_H1405. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H152d); [ zenon_intro zenon_H1530 | zenon_intro zenon_H152f ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H1530). zenon_intro zenon_H1409. zenon_intro zenon_H1428. % 2.92/3.12 apply tlhfof28950. apply sym_equal. exact zenon_H1409. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H152f); [ zenon_intro zenon_H1532 | zenon_intro zenon_H1531 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H1532). zenon_intro zenon_H140d. zenon_intro zenon_H142c. % 2.92/3.12 apply tlhfof28905. apply sym_equal. exact zenon_H140d. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H1531); [ zenon_intro zenon_H1534 | zenon_intro zenon_H1533 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H1534). zenon_intro zenon_H1411. zenon_intro zenon_H1430. % 2.92/3.12 apply tlhfof28859. apply sym_equal. exact zenon_H1411. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H1533); [ zenon_intro zenon_H1536 | zenon_intro zenon_H1535 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H1536). zenon_intro zenon_H1415. zenon_intro zenon_H1434. % 2.92/3.12 apply tlhfof28812. apply sym_equal. exact zenon_H1415. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H1535); [ zenon_intro zenon_H1538 | zenon_intro zenon_H1537 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H1538). zenon_intro zenon_H1419. zenon_intro zenon_H1438. % 2.92/3.12 apply tlhfof28764. apply sym_equal. exact zenon_H1419. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H1537); [ zenon_intro zenon_H153a | zenon_intro zenon_H1539 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H153a). zenon_intro zenon_H153b. zenon_intro zenon_H143c. % 2.92/3.12 apply tlhfof28715. apply sym_equal. exact zenon_H153b. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H1539); [ zenon_intro zenon_H153d | zenon_intro zenon_H153c ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H153d). zenon_intro zenon_H141d. zenon_intro zenon_H153e. % 2.92/3.12 apply tlhfof28614. apply sym_equal. exact zenon_H141d. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H153c); [ zenon_intro zenon_H1540 | zenon_intro zenon_H153f ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H1540). zenon_intro zenon_H1421. zenon_intro zenon_H1440. % 2.92/3.12 apply tlhfof28665. apply sym_equal. exact zenon_H1421. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H153f); [ zenon_intro zenon_H1542 | zenon_intro zenon_H1541 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H1542). zenon_intro zenon_H1425. zenon_intro zenon_H1444. % 2.92/3.12 apply tlhfof28562. apply sym_equal. exact zenon_H1425. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H1541); [ zenon_intro zenon_H1544 | zenon_intro zenon_H1543 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H1544). zenon_intro zenon_H1429. zenon_intro zenon_H1448. % 2.92/3.12 apply tlhfof28509. apply sym_equal. exact zenon_H1429. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H1543); [ zenon_intro zenon_H1546 | zenon_intro zenon_H1545 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H1546). zenon_intro zenon_H142d. zenon_intro zenon_H144c. % 2.92/3.12 apply tlhfof28455. apply sym_equal. exact zenon_H142d. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H1545); [ zenon_intro zenon_H1548 | zenon_intro zenon_H1547 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H1548). zenon_intro zenon_H1431. zenon_intro zenon_H1450. % 2.92/3.12 apply tlhfof28400. apply sym_equal. exact zenon_H1431. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H1547); [ zenon_intro zenon_H154a | zenon_intro zenon_H1549 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H154a). zenon_intro zenon_H1435. zenon_intro zenon_H1454. % 2.92/3.12 apply tlhfof28344. apply sym_equal. exact zenon_H1435. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H1549); [ zenon_intro zenon_H154c | zenon_intro zenon_H154b ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H154c). zenon_intro zenon_H1439. zenon_intro zenon_H1458. % 2.92/3.12 apply tlhfof28287. apply sym_equal. exact zenon_H1439. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H154b); [ zenon_intro zenon_H154e | zenon_intro zenon_H154d ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H154e). zenon_intro zenon_H143d. zenon_intro zenon_H145c. % 2.92/3.12 apply tlhfof28229. apply sym_equal. exact zenon_H143d. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H154d); [ zenon_intro zenon_H1550 | zenon_intro zenon_H154f ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H1550). zenon_intro zenon_H1551. zenon_intro zenon_H1460. % 2.92/3.12 apply tlhfof28170. apply sym_equal. exact zenon_H1551. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H154f); [ zenon_intro zenon_H1553 | zenon_intro zenon_H1552 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H1553). zenon_intro zenon_H1441. zenon_intro zenon_H1554. % 2.92/3.12 apply tlhfof28049. apply sym_equal. exact zenon_H1441. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H1552); [ zenon_intro zenon_H1556 | zenon_intro zenon_H1555 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H1556). zenon_intro zenon_H1445. zenon_intro zenon_H1464. % 2.92/3.12 apply tlhfof28110. apply sym_equal. exact zenon_H1445. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H1555); [ zenon_intro zenon_H1558 | zenon_intro zenon_H1557 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H1558). zenon_intro zenon_H1449. zenon_intro zenon_H1468. % 2.92/3.12 apply tlhfof27987. apply sym_equal. exact zenon_H1449. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H1557); [ zenon_intro zenon_H155a | zenon_intro zenon_H1559 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H155a). zenon_intro zenon_H144d. zenon_intro zenon_H146c. % 2.92/3.12 apply tlhfof27924. apply sym_equal. exact zenon_H144d. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H1559); [ zenon_intro zenon_H155c | zenon_intro zenon_H155b ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H155c). zenon_intro zenon_H1451. zenon_intro zenon_H1470. % 2.92/3.12 apply tlhfof27860. apply sym_equal. exact zenon_H1451. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H155b); [ zenon_intro zenon_H155e | zenon_intro zenon_H155d ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H155e). zenon_intro zenon_H1455. zenon_intro zenon_H1474. % 2.92/3.12 apply tlhfof27795. apply sym_equal. exact zenon_H1455. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H155d); [ zenon_intro zenon_H1560 | zenon_intro zenon_H155f ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H1560). zenon_intro zenon_H1459. zenon_intro zenon_H1478. % 2.92/3.12 apply tlhfof27729. apply sym_equal. exact zenon_H1459. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H155f); [ zenon_intro zenon_H1562 | zenon_intro zenon_H1561 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H1562). zenon_intro zenon_H145d. zenon_intro zenon_H147c. % 2.92/3.12 apply tlhfof27662. apply sym_equal. exact zenon_H145d. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H1561); [ zenon_intro zenon_H1564 | zenon_intro zenon_H1563 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H1564). zenon_intro zenon_H1461. zenon_intro zenon_H1480. % 2.92/3.12 apply tlhfof27594. apply sym_equal. exact zenon_H1461. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H1563); [ zenon_intro zenon_H1566 | zenon_intro zenon_H1565 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H1566). zenon_intro zenon_H1567. zenon_intro zenon_H1484. % 2.92/3.12 apply tlhfof27525. apply sym_equal. exact zenon_H1567. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H1565); [ zenon_intro zenon_H1569 | zenon_intro zenon_H1568 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H1569). zenon_intro zenon_H1465. zenon_intro zenon_H156a. % 2.92/3.12 apply tlhfof27384. apply sym_equal. exact zenon_H1465. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H1568); [ zenon_intro zenon_H156c | zenon_intro zenon_H156b ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H156c). zenon_intro zenon_H1469. zenon_intro zenon_H1488. % 2.92/3.12 apply tlhfof27455. apply sym_equal. exact zenon_H1469. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H156b); [ zenon_intro zenon_H156e | zenon_intro zenon_H156d ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H156e). zenon_intro zenon_H146d. zenon_intro zenon_H148c. % 2.92/3.12 apply tlhfof27312. apply sym_equal. exact zenon_H146d. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H156d); [ zenon_intro zenon_H1570 | zenon_intro zenon_H156f ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H1570). zenon_intro zenon_H1471. zenon_intro zenon_H1490. % 2.92/3.12 apply tlhfof27239. apply sym_equal. exact zenon_H1471. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H156f); [ zenon_intro zenon_H1572 | zenon_intro zenon_H1571 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H1572). zenon_intro zenon_H1475. zenon_intro zenon_H1494. % 2.92/3.12 apply tlhfof27165. apply sym_equal. exact zenon_H1475. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H1571); [ zenon_intro zenon_H1574 | zenon_intro zenon_H1573 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H1574). zenon_intro zenon_H1479. zenon_intro zenon_H1498. % 2.92/3.12 apply tlhfof27090. apply sym_equal. exact zenon_H1479. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H1573); [ zenon_intro zenon_H1576 | zenon_intro zenon_H1575 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H1576). zenon_intro zenon_H147d. zenon_intro zenon_H149c. % 2.92/3.12 apply tlhfof27014. apply sym_equal. exact zenon_H147d. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H1575); [ zenon_intro zenon_H1578 | zenon_intro zenon_H1577 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H1578). zenon_intro zenon_H1481. zenon_intro zenon_H14a0. % 2.92/3.12 apply tlhfof26937. apply sym_equal. exact zenon_H1481. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H1577); [ zenon_intro zenon_H157a | zenon_intro zenon_H1579 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H157a). zenon_intro zenon_H1485. zenon_intro zenon_H14a4. % 2.92/3.12 apply tlhfof26859. apply sym_equal. exact zenon_H1485. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H1579); [ zenon_intro zenon_H157c | zenon_intro zenon_H157b ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H157c). zenon_intro zenon_H157d. zenon_intro zenon_H14a8. % 2.92/3.12 apply tlhfof26780. apply sym_equal. exact zenon_H157d. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H157b); [ zenon_intro zenon_H157f | zenon_intro zenon_H157e ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H157f). zenon_intro zenon_H1489. zenon_intro zenon_H1580. % 2.92/3.12 apply tlhfof26619. apply sym_equal. exact zenon_H1489. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H157e); [ zenon_intro zenon_H1582 | zenon_intro zenon_H1581 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H1582). zenon_intro zenon_H148d. zenon_intro zenon_H14ac. % 2.92/3.12 apply tlhfof26700. apply sym_equal. exact zenon_H148d. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H1581); [ zenon_intro zenon_H1584 | zenon_intro zenon_H1583 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H1584). zenon_intro zenon_H1491. zenon_intro zenon_H14b0. % 2.92/3.12 apply tlhfof26537. apply sym_equal. exact zenon_H1491. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H1583); [ zenon_intro zenon_H1586 | zenon_intro zenon_H1585 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H1586). zenon_intro zenon_H1495. zenon_intro zenon_H14b4. % 2.92/3.12 apply tlhfof26454. apply sym_equal. exact zenon_H1495. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H1585); [ zenon_intro zenon_H1588 | zenon_intro zenon_H1587 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H1588). zenon_intro zenon_H1499. zenon_intro zenon_H14b8. % 2.92/3.12 apply tlhfof26370. apply sym_equal. exact zenon_H1499. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H1587); [ zenon_intro zenon_H158a | zenon_intro zenon_H1589 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H158a). zenon_intro zenon_H149d. zenon_intro zenon_H14bc. % 2.92/3.12 apply tlhfof26285. apply sym_equal. exact zenon_H149d. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H1589); [ zenon_intro zenon_H158c | zenon_intro zenon_H158b ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H158c). zenon_intro zenon_H14a1. zenon_intro zenon_H14c0. % 2.92/3.12 apply tlhfof26199. apply sym_equal. exact zenon_H14a1. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H158b); [ zenon_intro zenon_H158e | zenon_intro zenon_H158d ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H158e). zenon_intro zenon_H14a5. zenon_intro zenon_H14c4. % 2.92/3.12 apply tlhfof26112. apply sym_equal. exact zenon_H14a5. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H158d); [ zenon_intro zenon_H1590 | zenon_intro zenon_H158f ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H1590). zenon_intro zenon_H14a9. zenon_intro zenon_H14c8. % 2.92/3.12 apply tlhfof26024. apply sym_equal. exact zenon_H14a9. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H158f). zenon_intro zenon_H1591. zenon_intro zenon_H14cc. % 2.92/3.12 apply tlhfof25935. apply sym_equal. exact zenon_H1591. % 2.92/3.12 generalize (tlhfof24990 (cell1)). zenon_intro zenon_H1592. % 2.92/3.12 generalize (zenon_H1592 (cell100)). zenon_intro zenon_H1593. % 2.92/3.12 apply (zenon_equiv_s _ _ zenon_H1593); [ zenon_intro zenon_H1596; zenon_intro zenon_H1595 | zenon_intro zenon_H135f; zenon_intro zenon_H1594 ]. % 2.92/3.12 exact (zenon_H1596 zenon_H135f). % 2.92/3.12 apply (zenon_or_s _ _ zenon_H1594); [ zenon_intro zenon_H1598 | zenon_intro zenon_H1597 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H1598). zenon_intro zenon_H1599. zenon_intro zenon_H136d. % 2.92/3.12 apply tlhfof29941. apply sym_equal. exact zenon_H1599. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H1597); [ zenon_intro zenon_H159b | zenon_intro zenon_H159a ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H159b). zenon_intro zenon_H1368. zenon_intro zenon_H1371. % 2.92/3.12 apply tlhfof29940. apply sym_equal. exact zenon_H1368. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H159a); [ zenon_intro zenon_H159d | zenon_intro zenon_H159c ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H159d). zenon_intro zenon_H136c. zenon_intro zenon_H1375. % 2.92/3.12 apply tlhfof29938. apply sym_equal. exact zenon_H136c. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H159c); [ zenon_intro zenon_H159f | zenon_intro zenon_H159e ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H159f). zenon_intro zenon_H1370. zenon_intro zenon_H1379. % 2.92/3.12 apply tlhfof29935. apply sym_equal. exact zenon_H1370. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H159e); [ zenon_intro zenon_H15a1 | zenon_intro zenon_H15a0 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H15a1). zenon_intro zenon_H1374. zenon_intro zenon_H137d. % 2.92/3.12 apply tlhfof29931. apply sym_equal. exact zenon_H1374. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H15a0); [ zenon_intro zenon_H15a3 | zenon_intro zenon_H15a2 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H15a3). zenon_intro zenon_H1378. zenon_intro zenon_H1381. % 2.92/3.12 apply tlhfof29926. apply sym_equal. exact zenon_H1378. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H15a2); [ zenon_intro zenon_H15a5 | zenon_intro zenon_H15a4 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H15a5). zenon_intro zenon_H137c. zenon_intro zenon_H1385. % 2.92/3.12 apply tlhfof29920. apply sym_equal. exact zenon_H137c. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H15a4); [ zenon_intro zenon_H15a7 | zenon_intro zenon_H15a6 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H15a7). zenon_intro zenon_H1380. zenon_intro zenon_H1389. % 2.92/3.12 apply tlhfof29913. apply sym_equal. exact zenon_H1380. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H15a6); [ zenon_intro zenon_H15a9 | zenon_intro zenon_H15a8 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H15a9). zenon_intro zenon_H1384. zenon_intro zenon_H14e3. % 2.92/3.12 apply tlhfof29905. apply sym_equal. exact zenon_H1384. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H15a8); [ zenon_intro zenon_H15ab | zenon_intro zenon_H15aa ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H15ab). zenon_intro zenon_H14d0. zenon_intro zenon_H1391. % 2.92/3.12 apply tlhfof29875. apply sym_equal. exact zenon_H14d0. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H15aa); [ zenon_intro zenon_H15ad | zenon_intro zenon_H15ac ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H15ad). zenon_intro zenon_H138c. zenon_intro zenon_H1395. % 2.92/3.12 apply tlhfof29886. apply sym_equal. exact zenon_H138c. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H15ac); [ zenon_intro zenon_H15af | zenon_intro zenon_H15ae ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H15af). zenon_intro zenon_H1390. zenon_intro zenon_H1399. % 2.92/3.12 apply tlhfof29863. apply sym_equal. exact zenon_H1390. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H15ae); [ zenon_intro zenon_H15b1 | zenon_intro zenon_H15b0 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H15b1). zenon_intro zenon_H1394. zenon_intro zenon_H139d. % 2.92/3.12 apply tlhfof29850. apply sym_equal. exact zenon_H1394. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H15b0); [ zenon_intro zenon_H15b3 | zenon_intro zenon_H15b2 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H15b3). zenon_intro zenon_H1398. zenon_intro zenon_H13a1. % 2.92/3.12 apply tlhfof29836. apply sym_equal. exact zenon_H1398. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H15b2); [ zenon_intro zenon_H15b5 | zenon_intro zenon_H15b4 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H15b5). zenon_intro zenon_H139c. zenon_intro zenon_H13a5. % 2.92/3.12 apply tlhfof29821. apply sym_equal. exact zenon_H139c. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H15b4); [ zenon_intro zenon_H15b7 | zenon_intro zenon_H15b6 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H15b7). zenon_intro zenon_H13a0. zenon_intro zenon_H13a9. % 2.92/3.12 apply tlhfof29805. apply sym_equal. exact zenon_H13a0. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H15b6); [ zenon_intro zenon_H15b9 | zenon_intro zenon_H15b8 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H15b9). zenon_intro zenon_H13a4. zenon_intro zenon_H13ad. % 2.92/3.12 apply tlhfof29788. apply sym_equal. exact zenon_H13a4. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H15b8); [ zenon_intro zenon_H15bb | zenon_intro zenon_H15ba ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H15bb). zenon_intro zenon_H13a8. zenon_intro zenon_H14f9. % 2.92/3.12 apply tlhfof29770. apply sym_equal. exact zenon_H13a8. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H15ba); [ zenon_intro zenon_H15bd | zenon_intro zenon_H15bc ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H15bd). zenon_intro zenon_H14e6. zenon_intro zenon_H13b5. % 2.92/3.12 apply tlhfof29710. apply sym_equal. exact zenon_H14e6. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H15bc); [ zenon_intro zenon_H15bf | zenon_intro zenon_H15be ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H15bf). zenon_intro zenon_H13b0. zenon_intro zenon_H13b9. % 2.92/3.12 apply tlhfof29731. apply sym_equal. exact zenon_H13b0. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H15be); [ zenon_intro zenon_H15c1 | zenon_intro zenon_H15c0 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H15c1). zenon_intro zenon_H13b4. zenon_intro zenon_H13bd. % 2.92/3.12 apply tlhfof29688. apply sym_equal. exact zenon_H13b4. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H15c0); [ zenon_intro zenon_H15c3 | zenon_intro zenon_H15c2 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H15c3). zenon_intro zenon_H13b8. zenon_intro zenon_H13c1. % 2.92/3.12 apply tlhfof29665. apply sym_equal. exact zenon_H13b8. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H15c2); [ zenon_intro zenon_H15c5 | zenon_intro zenon_H15c4 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H15c5). zenon_intro zenon_H13bc. zenon_intro zenon_H13c5. % 2.92/3.12 apply tlhfof29641. apply sym_equal. exact zenon_H13bc. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H15c4); [ zenon_intro zenon_H15c7 | zenon_intro zenon_H15c6 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H15c7). zenon_intro zenon_H13c0. zenon_intro zenon_H13c9. % 2.92/3.12 apply tlhfof29616. apply sym_equal. exact zenon_H13c0. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H15c6); [ zenon_intro zenon_H15c9 | zenon_intro zenon_H15c8 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H15c9). zenon_intro zenon_H13c4. zenon_intro zenon_H13cd. % 2.92/3.12 apply tlhfof29590. apply sym_equal. exact zenon_H13c4. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H15c8); [ zenon_intro zenon_H15cb | zenon_intro zenon_H15ca ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H15cb). zenon_intro zenon_H13c8. zenon_intro zenon_H13d1. % 2.92/3.12 apply tlhfof29563. apply sym_equal. exact zenon_H13c8. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H15ca); [ zenon_intro zenon_H15cd | zenon_intro zenon_H15cc ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H15cd). zenon_intro zenon_H13cc. zenon_intro zenon_H150f. % 2.92/3.12 apply tlhfof29535. apply sym_equal. exact zenon_H13cc. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H15cc); [ zenon_intro zenon_H15cf | zenon_intro zenon_H15ce ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H15cf). zenon_intro zenon_H14fc. zenon_intro zenon_H13d9. % 2.92/3.12 apply tlhfof29445. apply sym_equal. exact zenon_H14fc. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H15ce); [ zenon_intro zenon_H15d1 | zenon_intro zenon_H15d0 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H15d1). zenon_intro zenon_H13d4. zenon_intro zenon_H13dd. % 2.92/3.12 apply tlhfof29476. apply sym_equal. exact zenon_H13d4. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H15d0); [ zenon_intro zenon_H15d3 | zenon_intro zenon_H15d2 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H15d3). zenon_intro zenon_H13d8. zenon_intro zenon_H13e1. % 2.92/3.12 apply tlhfof29413. apply sym_equal. exact zenon_H13d8. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H15d2); [ zenon_intro zenon_H15d5 | zenon_intro zenon_H15d4 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H15d5). zenon_intro zenon_H13dc. zenon_intro zenon_H13e5. % 2.92/3.12 apply tlhfof29380. apply sym_equal. exact zenon_H13dc. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H15d4); [ zenon_intro zenon_H15d7 | zenon_intro zenon_H15d6 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H15d7). zenon_intro zenon_H13e0. zenon_intro zenon_H13e9. % 2.92/3.12 apply tlhfof29346. apply sym_equal. exact zenon_H13e0. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H15d6); [ zenon_intro zenon_H15d9 | zenon_intro zenon_H15d8 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H15d9). zenon_intro zenon_H13e4. zenon_intro zenon_H13ed. % 2.92/3.12 apply tlhfof29311. apply sym_equal. exact zenon_H13e4. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H15d8); [ zenon_intro zenon_H15db | zenon_intro zenon_H15da ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H15db). zenon_intro zenon_H13e8. zenon_intro zenon_H13f1. % 2.92/3.12 apply tlhfof29275. apply sym_equal. exact zenon_H13e8. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H15da); [ zenon_intro zenon_H15dd | zenon_intro zenon_H15dc ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H15dd). zenon_intro zenon_H13ec. zenon_intro zenon_H13f5. % 2.92/3.12 apply tlhfof29238. apply sym_equal. exact zenon_H13ec. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H15dc); [ zenon_intro zenon_H15df | zenon_intro zenon_H15de ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H15df). zenon_intro zenon_H13f0. zenon_intro zenon_H1525. % 2.92/3.12 apply tlhfof29200. apply sym_equal. exact zenon_H13f0. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H15de); [ zenon_intro zenon_H15e1 | zenon_intro zenon_H15e0 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H15e1). zenon_intro zenon_H1512. zenon_intro zenon_H13fd. % 2.92/3.12 apply tlhfof29080. apply sym_equal. exact zenon_H1512. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H15e0); [ zenon_intro zenon_H15e3 | zenon_intro zenon_H15e2 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H15e3). zenon_intro zenon_H13f8. zenon_intro zenon_H1401. % 2.92/3.12 apply tlhfof29121. apply sym_equal. exact zenon_H13f8. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H15e2); [ zenon_intro zenon_H15e5 | zenon_intro zenon_H15e4 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H15e5). zenon_intro zenon_H13fc. zenon_intro zenon_H1405. % 2.92/3.12 apply tlhfof29038. apply sym_equal. exact zenon_H13fc. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H15e4); [ zenon_intro zenon_H15e7 | zenon_intro zenon_H15e6 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H15e7). zenon_intro zenon_H1400. zenon_intro zenon_H1409. % 2.92/3.12 apply tlhfof28995. apply sym_equal. exact zenon_H1400. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H15e6); [ zenon_intro zenon_H15e9 | zenon_intro zenon_H15e8 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H15e9). zenon_intro zenon_H1404. zenon_intro zenon_H140d. % 2.92/3.12 apply tlhfof28951. apply sym_equal. exact zenon_H1404. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H15e8); [ zenon_intro zenon_H15eb | zenon_intro zenon_H15ea ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H15eb). zenon_intro zenon_H1408. zenon_intro zenon_H1411. % 2.92/3.12 apply tlhfof28906. apply sym_equal. exact zenon_H1408. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H15ea); [ zenon_intro zenon_H15ed | zenon_intro zenon_H15ec ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H15ed). zenon_intro zenon_H140c. zenon_intro zenon_H1415. % 2.92/3.12 apply tlhfof28860. apply sym_equal. exact zenon_H140c. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H15ec); [ zenon_intro zenon_H15ef | zenon_intro zenon_H15ee ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H15ef). zenon_intro zenon_H1410. zenon_intro zenon_H1419. % 2.92/3.12 apply tlhfof28813. apply sym_equal. exact zenon_H1410. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H15ee); [ zenon_intro zenon_H15f1 | zenon_intro zenon_H15f0 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H15f1). zenon_intro zenon_H1414. zenon_intro zenon_H153b. % 2.92/3.12 apply tlhfof28765. apply sym_equal. exact zenon_H1414. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H15f0); [ zenon_intro zenon_H15f3 | zenon_intro zenon_H15f2 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H15f3). zenon_intro zenon_H1528. zenon_intro zenon_H1421. % 2.92/3.12 apply tlhfof28615. apply sym_equal. exact zenon_H1528. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H15f2); [ zenon_intro zenon_H15f5 | zenon_intro zenon_H15f4 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H15f5). zenon_intro zenon_H141c. zenon_intro zenon_H1425. % 2.92/3.12 apply tlhfof28666. apply sym_equal. exact zenon_H141c. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H15f4); [ zenon_intro zenon_H15f7 | zenon_intro zenon_H15f6 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H15f7). zenon_intro zenon_H1420. zenon_intro zenon_H1429. % 2.92/3.12 apply tlhfof28563. apply sym_equal. exact zenon_H1420. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H15f6); [ zenon_intro zenon_H15f9 | zenon_intro zenon_H15f8 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H15f9). zenon_intro zenon_H1424. zenon_intro zenon_H142d. % 2.92/3.12 apply tlhfof28510. apply sym_equal. exact zenon_H1424. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H15f8); [ zenon_intro zenon_H15fb | zenon_intro zenon_H15fa ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H15fb). zenon_intro zenon_H1428. zenon_intro zenon_H1431. % 2.92/3.12 apply tlhfof28456. apply sym_equal. exact zenon_H1428. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H15fa); [ zenon_intro zenon_H15fd | zenon_intro zenon_H15fc ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H15fd). zenon_intro zenon_H142c. zenon_intro zenon_H1435. % 2.92/3.12 apply tlhfof28401. apply sym_equal. exact zenon_H142c. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H15fc); [ zenon_intro zenon_H15ff | zenon_intro zenon_H15fe ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H15ff). zenon_intro zenon_H1430. zenon_intro zenon_H1439. % 2.92/3.12 apply tlhfof28345. apply sym_equal. exact zenon_H1430. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H15fe); [ zenon_intro zenon_H1601 | zenon_intro zenon_H1600 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H1601). zenon_intro zenon_H1434. zenon_intro zenon_H143d. % 2.92/3.12 apply tlhfof28288. apply sym_equal. exact zenon_H1434. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H1600); [ zenon_intro zenon_H1603 | zenon_intro zenon_H1602 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H1603). zenon_intro zenon_H1438. zenon_intro zenon_H1551. % 2.92/3.12 apply tlhfof28230. apply sym_equal. exact zenon_H1438. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H1602); [ zenon_intro zenon_H1605 | zenon_intro zenon_H1604 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H1605). zenon_intro zenon_H153e. zenon_intro zenon_H1445. % 2.92/3.12 apply tlhfof28050. apply sym_equal. exact zenon_H153e. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H1604); [ zenon_intro zenon_H1607 | zenon_intro zenon_H1606 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H1607). zenon_intro zenon_H1440. zenon_intro zenon_H1449. % 2.92/3.12 apply tlhfof28111. apply sym_equal. exact zenon_H1440. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H1606); [ zenon_intro zenon_H1609 | zenon_intro zenon_H1608 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H1609). zenon_intro zenon_H1444. zenon_intro zenon_H144d. % 2.92/3.12 apply tlhfof27988. apply sym_equal. exact zenon_H1444. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H1608); [ zenon_intro zenon_H160b | zenon_intro zenon_H160a ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H160b). zenon_intro zenon_H1448. zenon_intro zenon_H1451. % 2.92/3.12 apply tlhfof27925. apply sym_equal. exact zenon_H1448. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H160a); [ zenon_intro zenon_H160d | zenon_intro zenon_H160c ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H160d). zenon_intro zenon_H144c. zenon_intro zenon_H1455. % 2.92/3.12 apply tlhfof27861. apply sym_equal. exact zenon_H144c. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H160c); [ zenon_intro zenon_H160f | zenon_intro zenon_H160e ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H160f). zenon_intro zenon_H1450. zenon_intro zenon_H1459. % 2.92/3.12 apply tlhfof27796. apply sym_equal. exact zenon_H1450. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H160e); [ zenon_intro zenon_H1611 | zenon_intro zenon_H1610 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H1611). zenon_intro zenon_H1454. zenon_intro zenon_H145d. % 2.92/3.12 apply tlhfof27730. apply sym_equal. exact zenon_H1454. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H1610); [ zenon_intro zenon_H1613 | zenon_intro zenon_H1612 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H1613). zenon_intro zenon_H1458. zenon_intro zenon_H1461. % 2.92/3.12 apply tlhfof27663. apply sym_equal. exact zenon_H1458. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H1612); [ zenon_intro zenon_H1615 | zenon_intro zenon_H1614 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H1615). zenon_intro zenon_H145c. zenon_intro zenon_H1567. % 2.92/3.12 apply tlhfof27595. apply sym_equal. exact zenon_H145c. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H1614); [ zenon_intro zenon_H1617 | zenon_intro zenon_H1616 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H1617). zenon_intro zenon_H1554. zenon_intro zenon_H1469. % 2.92/3.12 apply tlhfof27385. apply sym_equal. exact zenon_H1554. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H1616); [ zenon_intro zenon_H1619 | zenon_intro zenon_H1618 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H1619). zenon_intro zenon_H1464. zenon_intro zenon_H146d. % 2.92/3.12 apply tlhfof27456. apply sym_equal. exact zenon_H1464. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H1618); [ zenon_intro zenon_H161b | zenon_intro zenon_H161a ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H161b). zenon_intro zenon_H1468. zenon_intro zenon_H1471. % 2.92/3.12 apply tlhfof27313. apply sym_equal. exact zenon_H1468. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H161a); [ zenon_intro zenon_H161d | zenon_intro zenon_H161c ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H161d). zenon_intro zenon_H146c. zenon_intro zenon_H1475. % 2.92/3.12 apply tlhfof27240. apply sym_equal. exact zenon_H146c. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H161c); [ zenon_intro zenon_H161f | zenon_intro zenon_H161e ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H161f). zenon_intro zenon_H1470. zenon_intro zenon_H1479. % 2.92/3.12 apply tlhfof27166. apply sym_equal. exact zenon_H1470. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H161e); [ zenon_intro zenon_H1621 | zenon_intro zenon_H1620 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H1621). zenon_intro zenon_H1474. zenon_intro zenon_H147d. % 2.92/3.12 apply tlhfof27091. apply sym_equal. exact zenon_H1474. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H1620); [ zenon_intro zenon_H1623 | zenon_intro zenon_H1622 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H1623). zenon_intro zenon_H1478. zenon_intro zenon_H1481. % 2.92/3.12 apply tlhfof27015. apply sym_equal. exact zenon_H1478. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H1622); [ zenon_intro zenon_H1625 | zenon_intro zenon_H1624 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H1625). zenon_intro zenon_H147c. zenon_intro zenon_H1485. % 2.92/3.12 apply tlhfof26938. apply sym_equal. exact zenon_H147c. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H1624); [ zenon_intro zenon_H1627 | zenon_intro zenon_H1626 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H1627). zenon_intro zenon_H1480. zenon_intro zenon_H157d. % 2.92/3.12 apply tlhfof26860. apply sym_equal. exact zenon_H1480. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H1626); [ zenon_intro zenon_H1629 | zenon_intro zenon_H1628 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H1629). zenon_intro zenon_H156a. zenon_intro zenon_H148d. % 2.92/3.12 apply tlhfof26620. apply sym_equal. exact zenon_H156a. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H1628); [ zenon_intro zenon_H162b | zenon_intro zenon_H162a ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H162b). zenon_intro zenon_H1488. zenon_intro zenon_H1491. % 2.92/3.12 apply tlhfof26701. apply sym_equal. exact zenon_H1488. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H162a); [ zenon_intro zenon_H162d | zenon_intro zenon_H162c ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H162d). zenon_intro zenon_H148c. zenon_intro zenon_H1495. % 2.92/3.12 apply tlhfof26538. apply sym_equal. exact zenon_H148c. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H162c); [ zenon_intro zenon_H162f | zenon_intro zenon_H162e ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H162f). zenon_intro zenon_H1490. zenon_intro zenon_H1499. % 2.92/3.12 apply tlhfof26455. apply sym_equal. exact zenon_H1490. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H162e); [ zenon_intro zenon_H1631 | zenon_intro zenon_H1630 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H1631). zenon_intro zenon_H1494. zenon_intro zenon_H149d. % 2.92/3.12 apply tlhfof26371. apply sym_equal. exact zenon_H1494. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H1630); [ zenon_intro zenon_H1633 | zenon_intro zenon_H1632 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H1633). zenon_intro zenon_H1498. zenon_intro zenon_H14a1. % 2.92/3.12 apply tlhfof26286. apply sym_equal. exact zenon_H1498. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H1632); [ zenon_intro zenon_H1635 | zenon_intro zenon_H1634 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H1635). zenon_intro zenon_H149c. zenon_intro zenon_H14a5. % 2.92/3.12 apply tlhfof26200. apply sym_equal. exact zenon_H149c. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H1634); [ zenon_intro zenon_H1637 | zenon_intro zenon_H1636 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H1637). zenon_intro zenon_H14a0. zenon_intro zenon_H14a9. % 2.92/3.12 apply tlhfof26113. apply sym_equal. exact zenon_H14a0. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H1636); [ zenon_intro zenon_H1639 | zenon_intro zenon_H1638 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H1639). zenon_intro zenon_H14a4. zenon_intro zenon_H1591. % 2.92/3.12 apply tlhfof26025. apply sym_equal. exact zenon_H14a4. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H1638); [ zenon_intro zenon_H163b | zenon_intro zenon_H163a ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H163b). zenon_intro zenon_H1580. zenon_intro zenon_H14b1. % 2.92/3.12 apply tlhfof25755. apply sym_equal. exact zenon_H1580. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H163a); [ zenon_intro zenon_H163d | zenon_intro zenon_H163c ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H163d). zenon_intro zenon_H14ac. zenon_intro zenon_H14b5. % 2.92/3.12 apply tlhfof25846. apply sym_equal. exact zenon_H14ac. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H163c); [ zenon_intro zenon_H163f | zenon_intro zenon_H163e ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H163f). zenon_intro zenon_H14b0. zenon_intro zenon_H14b9. % 2.92/3.12 apply tlhfof25663. apply sym_equal. exact zenon_H14b0. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H163e); [ zenon_intro zenon_H1641 | zenon_intro zenon_H1640 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H1641). zenon_intro zenon_H14b4. zenon_intro zenon_H14bd. % 2.92/3.12 apply tlhfof25570. apply sym_equal. exact zenon_H14b4. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H1640); [ zenon_intro zenon_H1643 | zenon_intro zenon_H1642 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H1643). zenon_intro zenon_H14b8. zenon_intro zenon_H14c1. % 2.92/3.12 apply tlhfof25476. apply sym_equal. exact zenon_H14b8. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H1642); [ zenon_intro zenon_H1645 | zenon_intro zenon_H1644 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H1645). zenon_intro zenon_H14bc. zenon_intro zenon_H14c5. % 2.92/3.12 apply tlhfof25381. apply sym_equal. exact zenon_H14bc. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H1644); [ zenon_intro zenon_H1647 | zenon_intro zenon_H1646 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H1647). zenon_intro zenon_H14c0. zenon_intro zenon_H14c9. % 2.92/3.12 apply tlhfof25285. apply sym_equal. exact zenon_H14c0. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H1646); [ zenon_intro zenon_H1649 | zenon_intro zenon_H1648 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H1649). zenon_intro zenon_H14c4. zenon_intro zenon_H14cd. % 2.92/3.12 apply tlhfof25188. apply sym_equal. exact zenon_H14c4. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H1648); [ zenon_intro zenon_H164b | zenon_intro zenon_H164a ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H164b). zenon_intro zenon_H14c8. zenon_intro zenon_H164c. % 2.92/3.12 apply tlhfof25090. apply sym_equal. exact zenon_H14c8. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H164a); [ zenon_intro zenon_H164e | zenon_intro zenon_H164d ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H164e). zenon_intro zenon_H1599. zenon_intro zenon_H138d. % 2.92/3.12 apply tlhfof29941. apply sym_equal. exact zenon_H1599. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H164d); [ zenon_intro zenon_H1650 | zenon_intro zenon_H164f ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H1650). zenon_intro zenon_H1368. zenon_intro zenon_H1391. % 2.92/3.12 apply tlhfof29940. apply sym_equal. exact zenon_H1368. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H164f); [ zenon_intro zenon_H1652 | zenon_intro zenon_H1651 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H1652). zenon_intro zenon_H136c. zenon_intro zenon_H1395. % 2.92/3.12 apply tlhfof29938. apply sym_equal. exact zenon_H136c. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H1651); [ zenon_intro zenon_H1654 | zenon_intro zenon_H1653 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H1654). zenon_intro zenon_H1370. zenon_intro zenon_H1399. % 2.92/3.12 apply tlhfof29935. apply sym_equal. exact zenon_H1370. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H1653); [ zenon_intro zenon_H1656 | zenon_intro zenon_H1655 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H1656). zenon_intro zenon_H1374. zenon_intro zenon_H139d. % 2.92/3.12 apply tlhfof29931. apply sym_equal. exact zenon_H1374. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H1655); [ zenon_intro zenon_H1658 | zenon_intro zenon_H1657 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H1658). zenon_intro zenon_H1378. zenon_intro zenon_H13a1. % 2.92/3.12 apply tlhfof29926. apply sym_equal. exact zenon_H1378. % 2.92/3.12 apply (zenon_or_s _ _ zenon_H1657); [ zenon_intro zenon_H165a | zenon_intro zenon_H1659 ]. % 2.92/3.12 apply (zenon_and_s _ _ zenon_H165a). zenon_intro zenon_H137c. zenon_intro zenon_H13a5. % 3.01/3.28 apply tlhfof29920. apply sym_equal. exact zenon_H137c. % 3.01/3.28 apply (zenon_or_s _ _ zenon_H1659); [ zenon_intro zenon_H165c | zenon_intro zenon_H165b ]. % 3.01/3.28 apply (zenon_and_s _ _ zenon_H165c). zenon_intro zenon_H1380. zenon_intro zenon_H13a9. % 3.01/3.28 apply tlhfof29913. apply sym_equal. exact zenon_H1380. % 3.01/3.28 apply (zenon_or_s _ _ zenon_H165b); [ zenon_intro zenon_H165e | zenon_intro zenon_H165d ]. % 3.01/3.28 apply (zenon_and_s _ _ zenon_H165e). zenon_intro zenon_H1384. zenon_intro zenon_H13ad. % 3.01/3.28 apply tlhfof29905. apply sym_equal. exact zenon_H1384. % 3.01/3.28 apply (zenon_or_s _ _ zenon_H165d); [ zenon_intro zenon_H1660 | zenon_intro zenon_H165f ]. % 3.01/3.28 apply (zenon_and_s _ _ zenon_H1660). zenon_intro zenon_H1388. zenon_intro zenon_H14f9. % 3.01/3.28 apply tlhfof29896. apply sym_equal. exact zenon_H1388. % 3.01/3.28 apply (zenon_or_s _ _ zenon_H165f); [ zenon_intro zenon_H1662 | zenon_intro zenon_H1661 ]. % 3.01/3.28 apply (zenon_and_s _ _ zenon_H1662). zenon_intro zenon_H14d0. zenon_intro zenon_H13b1. % 3.01/3.28 apply tlhfof29875. apply sym_equal. exact zenon_H14d0. % 3.01/3.28 apply (zenon_or_s _ _ zenon_H1661); [ zenon_intro zenon_H1664 | zenon_intro zenon_H1663 ]. % 3.01/3.28 apply (zenon_and_s _ _ zenon_H1664). zenon_intro zenon_H138c. zenon_intro zenon_H13b5. % 3.01/3.28 apply tlhfof29886. apply sym_equal. exact zenon_H138c. % 3.01/3.28 apply (zenon_or_s _ _ zenon_H1663); [ zenon_intro zenon_H1666 | zenon_intro zenon_H1665 ]. % 3.01/3.28 apply (zenon_and_s _ _ zenon_H1666). zenon_intro zenon_H1390. zenon_intro zenon_H13b9. % 3.01/3.28 apply tlhfof29863. apply sym_equal. exact zenon_H1390. % 3.01/3.28 apply (zenon_or_s _ _ zenon_H1665); [ zenon_intro zenon_H1668 | zenon_intro zenon_H1667 ]. % 3.01/3.28 apply (zenon_and_s _ _ zenon_H1668). zenon_intro zenon_H1394. zenon_intro zenon_H13bd. % 3.01/3.28 apply tlhfof29850. apply sym_equal. exact zenon_H1394. % 3.01/3.28 apply (zenon_or_s _ _ zenon_H1667); [ zenon_intro zenon_H166a | zenon_intro zenon_H1669 ]. % 3.01/3.28 apply (zenon_and_s _ _ zenon_H166a). zenon_intro zenon_H1398. zenon_intro zenon_H13c1. % 3.01/3.28 apply tlhfof29836. apply sym_equal. exact zenon_H1398. % 3.01/3.28 apply (zenon_or_s _ _ zenon_H1669); [ zenon_intro zenon_H166c | zenon_intro zenon_H166b ]. % 3.01/3.28 apply (zenon_and_s _ _ zenon_H166c). zenon_intro zenon_H139c. zenon_intro zenon_H13c5. % 3.01/3.28 apply tlhfof29821. apply sym_equal. exact zenon_H139c. % 3.01/3.28 apply (zenon_or_s _ _ zenon_H166b); [ zenon_intro zenon_H166e | zenon_intro zenon_H166d ]. % 3.01/3.28 apply (zenon_and_s _ _ zenon_H166e). zenon_intro zenon_H13a0. zenon_intro zenon_H13c9. % 3.01/3.28 apply tlhfof29805. apply sym_equal. exact zenon_H13a0. % 3.01/3.28 apply (zenon_or_s _ _ zenon_H166d); [ zenon_intro zenon_H1670 | zenon_intro zenon_H166f ]. % 3.01/3.28 apply (zenon_and_s _ _ zenon_H1670). zenon_intro zenon_H13a4. zenon_intro zenon_H13cd. % 3.01/3.28 apply tlhfof29788. apply sym_equal. exact zenon_H13a4. % 3.01/3.28 apply (zenon_or_s _ _ zenon_H166f); [ zenon_intro zenon_H1672 | zenon_intro zenon_H1671 ]. % 3.01/3.28 apply (zenon_and_s _ _ zenon_H1672). zenon_intro zenon_H13a8. zenon_intro zenon_H13d1. % 3.01/3.28 apply tlhfof29770. apply sym_equal. exact zenon_H13a8. % 3.01/3.28 apply (zenon_or_s _ _ zenon_H1671); [ zenon_intro zenon_H1674 | zenon_intro zenon_H1673 ]. % 3.01/3.28 apply (zenon_and_s _ _ zenon_H1674). zenon_intro zenon_H13ac. zenon_intro zenon_H150f. % 3.01/3.28 apply tlhfof29751. apply sym_equal. exact zenon_H13ac. % 3.01/3.28 apply (zenon_or_s _ _ zenon_H1673); [ zenon_intro zenon_H1676 | zenon_intro zenon_H1675 ]. % 3.01/3.28 apply (zenon_and_s _ _ zenon_H1676). zenon_intro zenon_H14e6. zenon_intro zenon_H13d5. % 3.01/3.28 apply tlhfof29710. apply sym_equal. exact zenon_H14e6. % 3.01/3.28 apply (zenon_or_s _ _ zenon_H1675); [ zenon_intro zenon_H1678 | zenon_intro zenon_H1677 ]. % 3.01/3.28 apply (zenon_and_s _ _ zenon_H1678). zenon_intro zenon_H13b0. zenon_intro zenon_H13d9. % 3.01/3.28 apply tlhfof29731. apply sym_equal. exact zenon_H13b0. % 3.01/3.28 apply (zenon_or_s _ _ zenon_H1677); [ zenon_intro zenon_H167a | zenon_intro zenon_H1679 ]. % 3.01/3.28 apply (zenon_and_s _ _ zenon_H167a). zenon_intro zenon_H13b4. zenon_intro zenon_H13dd. % 3.01/3.28 apply tlhfof29688. apply sym_equal. exact zenon_H13b4. % 3.01/3.28 apply (zenon_or_s _ _ zenon_H1679); [ zenon_intro zenon_H167c | zenon_intro zenon_H167b ]. % 3.01/3.28 apply (zenon_and_s _ _ zenon_H167c). zenon_intro zenon_H13b8. zenon_intro zenon_H13e1. % 3.01/3.28 apply tlhfof29665. apply sym_equal. exact zenon_H13b8. % 3.01/3.28 apply (zenon_or_s _ _ zenon_H167b); [ zenon_intro zenon_H167e | zenon_intro zenon_H167d ]. % 3.01/3.28 apply (zenon_and_s _ _ zenon_H167e). zenon_intro zenon_H13bc. zenon_intro zenon_H13e5. % 3.01/3.28 apply tlhfof29641. apply sym_equal. exact zenon_H13bc. % 3.01/3.28 apply (zenon_or_s _ _ zenon_H167d); [ zenon_intro zenon_H1680 | zenon_intro zenon_H167f ]. % 3.01/3.28 apply (zenon_and_s _ _ zenon_H1680). zenon_intro zenon_H13c0. zenon_intro zenon_H13e9. % 3.01/3.28 apply tlhfof29616. apply sym_equal. exact zenon_H13c0. % 3.01/3.28 apply (zenon_or_s _ _ zenon_H167f); [ zenon_intro zenon_H1682 | zenon_intro zenon_H1681 ]. % 3.01/3.28 apply (zenon_and_s _ _ zenon_H1682). zenon_intro zenon_H13c4. zenon_intro zenon_H13ed. % 3.01/3.28 apply tlhfof29590. apply sym_equal. exact zenon_H13c4. % 3.01/3.28 apply (zenon_or_s _ _ zenon_H1681); [ zenon_intro zenon_H1684 | zenon_intro zenon_H1683 ]. % 3.01/3.28 apply (zenon_and_s _ _ zenon_H1684). zenon_intro zenon_H13c8. zenon_intro zenon_H13f1. % 3.01/3.28 apply tlhfof29563. apply sym_equal. exact zenon_H13c8. % 3.01/3.28 apply (zenon_or_s _ _ zenon_H1683); [ zenon_intro zenon_H1686 | zenon_intro zenon_H1685 ]. % 3.01/3.28 apply (zenon_and_s _ _ zenon_H1686). zenon_intro zenon_H13cc. zenon_intro zenon_H13f5. % 3.01/3.28 apply tlhfof29535. apply sym_equal. exact zenon_H13cc. % 3.01/3.28 apply (zenon_or_s _ _ zenon_H1685); [ zenon_intro zenon_H1688 | zenon_intro zenon_H1687 ]. % 3.01/3.28 apply (zenon_and_s _ _ zenon_H1688). zenon_intro zenon_H13d0. zenon_intro zenon_H1525. % 3.01/3.28 apply tlhfof29506. apply sym_equal. exact zenon_H13d0. % 3.01/3.28 apply (zenon_or_s _ _ zenon_H1687); [ zenon_intro zenon_H168a | zenon_intro zenon_H1689 ]. % 3.01/3.28 apply (zenon_and_s _ _ zenon_H168a). zenon_intro zenon_H14fc. zenon_intro zenon_H13f9. % 3.01/3.28 apply tlhfof29445. apply sym_equal. exact zenon_H14fc. % 3.01/3.28 apply (zenon_or_s _ _ zenon_H1689); [ zenon_intro zenon_H168c | zenon_intro zenon_H168b ]. % 3.01/3.28 apply (zenon_and_s _ _ zenon_H168c). zenon_intro zenon_H13d4. zenon_intro zenon_H13fd. % 3.01/3.28 apply tlhfof29476. apply sym_equal. exact zenon_H13d4. % 3.01/3.28 apply (zenon_or_s _ _ zenon_H168b); [ zenon_intro zenon_H168e | zenon_intro zenon_H168d ]. % 3.01/3.28 apply (zenon_and_s _ _ zenon_H168e). zenon_intro zenon_H13d8. zenon_intro zenon_H1401. % 3.01/3.28 apply tlhfof29413. apply sym_equal. exact zenon_H13d8. % 3.01/3.28 apply (zenon_or_s _ _ zenon_H168d); [ zenon_intro zenon_H1690 | zenon_intro zenon_H168f ]. % 3.01/3.28 apply (zenon_and_s _ _ zenon_H1690). zenon_intro zenon_H13dc. zenon_intro zenon_H1405. % 3.01/3.28 apply tlhfof29380. apply sym_equal. exact zenon_H13dc. % 3.01/3.28 apply (zenon_or_s _ _ zenon_H168f); [ zenon_intro zenon_H1692 | zenon_intro zenon_H1691 ]. % 3.01/3.28 apply (zenon_and_s _ _ zenon_H1692). zenon_intro zenon_H13e0. zenon_intro zenon_H1409. % 3.01/3.28 apply tlhfof29346. apply sym_equal. exact zenon_H13e0. % 3.01/3.28 apply (zenon_or_s _ _ zenon_H1691); [ zenon_intro zenon_H1694 | zenon_intro zenon_H1693 ]. % 3.01/3.28 apply (zenon_and_s _ _ zenon_H1694). zenon_intro zenon_H13e4. zenon_intro zenon_H140d. % 3.01/3.28 apply tlhfof29311. apply sym_equal. exact zenon_H13e4. % 3.01/3.28 apply (zenon_or_s _ _ zenon_H1693); [ zenon_intro zenon_H1696 | zenon_intro zenon_H1695 ]. % 3.01/3.28 apply (zenon_and_s _ _ zenon_H1696). zenon_intro zenon_H13e8. zenon_intro zenon_H1411. % 3.01/3.28 apply tlhfof29275. apply sym_equal. exact zenon_H13e8. % 3.01/3.28 apply (zenon_or_s _ _ zenon_H1695); [ zenon_intro zenon_H1698 | zenon_intro zenon_H1697 ]. % 3.01/3.28 apply (zenon_and_s _ _ zenon_H1698). zenon_intro zenon_H13ec. zenon_intro zenon_H1415. % 3.01/3.28 apply tlhfof29238. apply sym_equal. exact zenon_H13ec. % 3.01/3.28 apply (zenon_or_s _ _ zenon_H1697); [ zenon_intro zenon_H169a | zenon_intro zenon_H1699 ]. % 3.01/3.28 apply (zenon_and_s _ _ zenon_H169a). zenon_intro zenon_H13f0. zenon_intro zenon_H1419. % 3.01/3.28 apply tlhfof29200. apply sym_equal. exact zenon_H13f0. % 3.01/3.28 apply (zenon_or_s _ _ zenon_H1699); [ zenon_intro zenon_H169c | zenon_intro zenon_H169b ]. % 3.01/3.28 apply (zenon_and_s _ _ zenon_H169c). zenon_intro zenon_H13f4. zenon_intro zenon_H153b. % 3.01/3.28 apply tlhfof29161. apply sym_equal. exact zenon_H13f4. % 3.01/3.28 apply (zenon_or_s _ _ zenon_H169b); [ zenon_intro zenon_H169e | zenon_intro zenon_H169d ]. % 3.01/3.28 apply (zenon_and_s _ _ zenon_H169e). zenon_intro zenon_H1512. zenon_intro zenon_H141d. % 3.01/3.28 apply tlhfof29080. apply sym_equal. exact zenon_H1512. % 3.01/3.28 apply (zenon_or_s _ _ zenon_H169d); [ zenon_intro zenon_H16a0 | zenon_intro zenon_H169f ]. % 3.01/3.28 apply (zenon_and_s _ _ zenon_H16a0). zenon_intro zenon_H13f8. zenon_intro zenon_H1421. % 3.01/3.28 apply tlhfof29121. apply sym_equal. exact zenon_H13f8. % 3.01/3.28 apply (zenon_or_s _ _ zenon_H169f); [ zenon_intro zenon_H16a2 | zenon_intro zenon_H16a1 ]. % 3.01/3.28 apply (zenon_and_s _ _ zenon_H16a2). zenon_intro zenon_H13fc. zenon_intro zenon_H1425. % 3.01/3.28 apply tlhfof29038. apply sym_equal. exact zenon_H13fc. % 3.01/3.28 apply (zenon_or_s _ _ zenon_H16a1); [ zenon_intro zenon_H16a4 | zenon_intro zenon_H16a3 ]. % 3.01/3.28 apply (zenon_and_s _ _ zenon_H16a4). zenon_intro zenon_H1400. zenon_intro zenon_H1429. % 3.01/3.28 apply tlhfof28995. apply sym_equal. exact zenon_H1400. % 3.01/3.28 apply (zenon_or_s _ _ zenon_H16a3); [ zenon_intro zenon_H16a6 | zenon_intro zenon_H16a5 ]. % 3.01/3.28 apply (zenon_and_s _ _ zenon_H16a6). zenon_intro zenon_H1404. zenon_intro zenon_H142d. % 3.01/3.28 apply tlhfof28951. apply sym_equal. exact zenon_H1404. % 3.01/3.28 apply (zenon_or_s _ _ zenon_H16a5); [ zenon_intro zenon_H16a8 | zenon_intro zenon_H16a7 ]. % 3.01/3.28 apply (zenon_and_s _ _ zenon_H16a8). zenon_intro zenon_H1408. zenon_intro zenon_H1431. % 3.01/3.28 apply tlhfof28906. apply sym_equal. exact zenon_H1408. % 3.01/3.28 apply (zenon_or_s _ _ zenon_H16a7); [ zenon_intro zenon_H16aa | zenon_intro zenon_H16a9 ]. % 3.01/3.28 apply (zenon_and_s _ _ zenon_H16aa). zenon_intro zenon_H140c. zenon_intro zenon_H1435. % 3.01/3.28 apply tlhfof28860. apply sym_equal. exact zenon_H140c. % 3.01/3.28 apply (zenon_or_s _ _ zenon_H16a9); [ zenon_intro zenon_H16ac | zenon_intro zenon_H16ab ]. % 3.01/3.28 apply (zenon_and_s _ _ zenon_H16ac). zenon_intro zenon_H1410. zenon_intro zenon_H1439. % 3.01/3.28 apply tlhfof28813. apply sym_equal. exact zenon_H1410. % 3.01/3.28 apply (zenon_or_s _ _ zenon_H16ab); [ zenon_intro zenon_H16ae | zenon_intro zenon_H16ad ]. % 3.01/3.28 apply (zenon_and_s _ _ zenon_H16ae). zenon_intro zenon_H1414. zenon_intro zenon_H143d. % 3.01/3.28 apply tlhfof28765. apply sym_equal. exact zenon_H1414. % 3.01/3.28 apply (zenon_or_s _ _ zenon_H16ad); [ zenon_intro zenon_H16b0 | zenon_intro zenon_H16af ]. % 3.01/3.28 apply (zenon_and_s _ _ zenon_H16b0). zenon_intro zenon_H1418. zenon_intro zenon_H1551. % 3.01/3.28 apply tlhfof28716. apply sym_equal. exact zenon_H1418. % 3.01/3.28 apply (zenon_or_s _ _ zenon_H16af); [ zenon_intro zenon_H16b2 | zenon_intro zenon_H16b1 ]. % 3.01/3.28 apply (zenon_and_s _ _ zenon_H16b2). zenon_intro zenon_H1528. zenon_intro zenon_H1441. % 3.01/3.28 apply tlhfof28615. apply sym_equal. exact zenon_H1528. % 3.01/3.28 apply (zenon_or_s _ _ zenon_H16b1); [ zenon_intro zenon_H16b4 | zenon_intro zenon_H16b3 ]. % 3.01/3.28 apply (zenon_and_s _ _ zenon_H16b4). zenon_intro zenon_H141c. zenon_intro zenon_H1445. % 3.01/3.28 apply tlhfof28666. apply sym_equal. exact zenon_H141c. % 3.01/3.28 apply (zenon_or_s _ _ zenon_H16b3); [ zenon_intro zenon_H16b6 | zenon_intro zenon_H16b5 ]. % 3.01/3.28 apply (zenon_and_s _ _ zenon_H16b6). zenon_intro zenon_H1420. zenon_intro zenon_H1449. % 3.01/3.28 apply tlhfof28563. apply sym_equal. exact zenon_H1420. % 3.01/3.28 apply (zenon_or_s _ _ zenon_H16b5); [ zenon_intro zenon_H16b8 | zenon_intro zenon_H16b7 ]. % 3.01/3.28 apply (zenon_and_s _ _ zenon_H16b8). zenon_intro zenon_H1424. zenon_intro zenon_H144d. % 3.01/3.28 apply tlhfof28510. apply sym_equal. exact zenon_H1424. % 3.01/3.28 apply (zenon_or_s _ _ zenon_H16b7); [ zenon_intro zenon_H16ba | zenon_intro zenon_H16b9 ]. % 3.01/3.28 apply (zenon_and_s _ _ zenon_H16ba). zenon_intro zenon_H1428. zenon_intro zenon_H1451. % 3.01/3.28 apply tlhfof28456. apply sym_equal. exact zenon_H1428. % 3.01/3.28 apply (zenon_or_s _ _ zenon_H16b9); [ zenon_intro zenon_H16bc | zenon_intro zenon_H16bb ]. % 3.01/3.28 apply (zenon_and_s _ _ zenon_H16bc). zenon_intro zenon_H142c. zenon_intro zenon_H1455. % 3.01/3.28 apply tlhfof28401. apply sym_equal. exact zenon_H142c. % 3.01/3.28 apply (zenon_or_s _ _ zenon_H16bb); [ zenon_intro zenon_H16be | zenon_intro zenon_H16bd ]. % 3.01/3.28 apply (zenon_and_s _ _ zenon_H16be). zenon_intro zenon_H1430. zenon_intro zenon_H1459. % 3.01/3.28 apply tlhfof28345. apply sym_equal. exact zenon_H1430. % 3.01/3.28 apply (zenon_or_s _ _ zenon_H16bd); [ zenon_intro zenon_H16c0 | zenon_intro zenon_H16bf ]. % 3.01/3.28 apply (zenon_and_s _ _ zenon_H16c0). zenon_intro zenon_H1434. zenon_intro zenon_H145d. % 3.01/3.28 apply tlhfof28288. apply sym_equal. exact zenon_H1434. % 3.01/3.28 apply (zenon_or_s _ _ zenon_H16bf); [ zenon_intro zenon_H16c2 | zenon_intro zenon_H16c1 ]. % 3.01/3.28 apply (zenon_and_s _ _ zenon_H16c2). zenon_intro zenon_H1438. zenon_intro zenon_H1461. % 3.01/3.28 apply tlhfof28230. apply sym_equal. exact zenon_H1438. % 3.01/3.28 apply (zenon_or_s _ _ zenon_H16c1); [ zenon_intro zenon_H16c4 | zenon_intro zenon_H16c3 ]. % 3.01/3.28 apply (zenon_and_s _ _ zenon_H16c4). zenon_intro zenon_H143c. zenon_intro zenon_H1567. % 3.01/3.28 apply tlhfof28171. apply sym_equal. exact zenon_H143c. % 3.01/3.28 apply (zenon_or_s _ _ zenon_H16c3); [ zenon_intro zenon_H16c6 | zenon_intro zenon_H16c5 ]. % 3.01/3.28 apply (zenon_and_s _ _ zenon_H16c6). zenon_intro zenon_H153e. zenon_intro zenon_H1465. % 3.01/3.28 apply tlhfof28050. apply sym_equal. exact zenon_H153e. % 3.01/3.28 apply (zenon_or_s _ _ zenon_H16c5); [ zenon_intro zenon_H16c8 | zenon_intro zenon_H16c7 ]. % 3.01/3.28 apply (zenon_and_s _ _ zenon_H16c8). zenon_intro zenon_H1440. zenon_intro zenon_H1469. % 3.01/3.28 apply tlhfof28111. apply sym_equal. exact zenon_H1440. % 3.01/3.28 apply (zenon_or_s _ _ zenon_H16c7); [ zenon_intro zenon_H16ca | zenon_intro zenon_H16c9 ]. % 3.01/3.28 apply (zenon_and_s _ _ zenon_H16ca). zenon_intro zenon_H1444. zenon_intro zenon_H146d. % 3.01/3.28 apply tlhfof27988. apply sym_equal. exact zenon_H1444. % 3.01/3.28 apply (zenon_or_s _ _ zenon_H16c9); [ zenon_intro zenon_H16cc | zenon_intro zenon_H16cb ]. % 3.01/3.28 apply (zenon_and_s _ _ zenon_H16cc). zenon_intro zenon_H1448. zenon_intro zenon_H1471. % 3.01/3.28 apply tlhfof27925. apply sym_equal. exact zenon_H1448. % 3.01/3.28 apply (zenon_or_s _ _ zenon_H16cb); [ zenon_intro zenon_H16ce | zenon_intro zenon_H16cd ]. % 3.01/3.28 apply (zenon_and_s _ _ zenon_H16ce). zenon_intro zenon_H144c. zenon_intro zenon_H1475. % 3.01/3.28 apply tlhfof27861. apply sym_equal. exact zenon_H144c. % 3.01/3.28 apply (zenon_or_s _ _ zenon_H16cd); [ zenon_intro zenon_H16d0 | zenon_intro zenon_H16cf ]. % 3.01/3.28 apply (zenon_and_s _ _ zenon_H16d0). zenon_intro zenon_H1450. zenon_intro zenon_H1479. % 3.01/3.28 apply tlhfof27796. apply sym_equal. exact zenon_H1450. % 3.01/3.28 apply (zenon_or_s _ _ zenon_H16cf); [ zenon_intro zenon_H16d2 | zenon_intro zenon_H16d1 ]. % 3.01/3.28 apply (zenon_and_s _ _ zenon_H16d2). zenon_intro zenon_H1454. zenon_intro zenon_H147d. % 3.01/3.28 apply tlhfof27730. apply sym_equal. exact zenon_H1454. % 3.01/3.28 apply (zenon_or_s _ _ zenon_H16d1); [ zenon_intro zenon_H16d4 | zenon_intro zenon_H16d3 ]. % 3.01/3.28 apply (zenon_and_s _ _ zenon_H16d4). zenon_intro zenon_H1458. zenon_intro zenon_H1481. % 3.01/3.28 apply tlhfof27663. apply sym_equal. exact zenon_H1458. % 3.01/3.28 apply (zenon_or_s _ _ zenon_H16d3); [ zenon_intro zenon_H16d6 | zenon_intro zenon_H16d5 ]. % 3.01/3.28 apply (zenon_and_s _ _ zenon_H16d6). zenon_intro zenon_H145c. zenon_intro zenon_H1485. % 3.01/3.28 apply tlhfof27595. apply sym_equal. exact zenon_H145c. % 3.01/3.28 apply (zenon_or_s _ _ zenon_H16d5); [ zenon_intro zenon_H16d8 | zenon_intro zenon_H16d7 ]. % 3.01/3.28 apply (zenon_and_s _ _ zenon_H16d8). zenon_intro zenon_H1460. zenon_intro zenon_H157d. % 3.01/3.28 apply tlhfof27526. apply sym_equal. exact zenon_H1460. % 3.01/3.28 apply (zenon_or_s _ _ zenon_H16d7); [ zenon_intro zenon_H16da | zenon_intro zenon_H16d9 ]. % 3.01/3.28 apply (zenon_and_s _ _ zenon_H16da). zenon_intro zenon_H1554. zenon_intro zenon_H1489. % 3.01/3.28 apply tlhfof27385. apply sym_equal. exact zenon_H1554. % 3.01/3.28 apply (zenon_or_s _ _ zenon_H16d9); [ zenon_intro zenon_H16dc | zenon_intro zenon_H16db ]. % 3.01/3.28 apply (zenon_and_s _ _ zenon_H16dc). zenon_intro zenon_H1464. zenon_intro zenon_H148d. % 3.01/3.28 apply tlhfof27456. apply sym_equal. exact zenon_H1464. % 3.01/3.28 apply (zenon_or_s _ _ zenon_H16db); [ zenon_intro zenon_H16de | zenon_intro zenon_H16dd ]. % 3.01/3.28 apply (zenon_and_s _ _ zenon_H16de). zenon_intro zenon_H1468. zenon_intro zenon_H1491. % 3.01/3.28 apply tlhfof27313. apply sym_equal. exact zenon_H1468. % 3.01/3.28 apply (zenon_or_s _ _ zenon_H16dd); [ zenon_intro zenon_H16e0 | zenon_intro zenon_H16df ]. % 3.01/3.28 apply (zenon_and_s _ _ zenon_H16e0). zenon_intro zenon_H146c. zenon_intro zenon_H1495. % 3.01/3.28 apply tlhfof27240. apply sym_equal. exact zenon_H146c. % 3.01/3.28 apply (zenon_or_s _ _ zenon_H16df); [ zenon_intro zenon_H16e2 | zenon_intro zenon_H16e1 ]. % 3.01/3.28 apply (zenon_and_s _ _ zenon_H16e2). zenon_intro zenon_H1470. zenon_intro zenon_H1499. % 3.01/3.28 apply tlhfof27166. apply sym_equal. exact zenon_H1470. % 3.01/3.28 apply (zenon_or_s _ _ zenon_H16e1); [ zenon_intro zenon_H16e4 | zenon_intro zenon_H16e3 ]. % 3.01/3.28 apply (zenon_and_s _ _ zenon_H16e4). zenon_intro zenon_H1474. zenon_intro zenon_H149d. % 3.01/3.28 apply tlhfof27091. apply sym_equal. exact zenon_H1474. % 3.01/3.28 apply (zenon_or_s _ _ zenon_H16e3); [ zenon_intro zenon_H16e6 | zenon_intro zenon_H16e5 ]. % 3.01/3.28 apply (zenon_and_s _ _ zenon_H16e6). zenon_intro zenon_H1478. zenon_intro zenon_H14a1. % 3.01/3.28 apply tlhfof27015. apply sym_equal. exact zenon_H1478. % 3.01/3.28 apply (zenon_or_s _ _ zenon_H16e5); [ zenon_intro zenon_H16e8 | zenon_intro zenon_H16e7 ]. % 3.01/3.28 apply (zenon_and_s _ _ zenon_H16e8). zenon_intro zenon_H147c. zenon_intro zenon_H14a5. % 3.01/3.28 apply tlhfof26938. apply sym_equal. exact zenon_H147c. % 3.01/3.28 apply (zenon_or_s _ _ zenon_H16e7); [ zenon_intro zenon_H16ea | zenon_intro zenon_H16e9 ]. % 3.01/3.28 apply (zenon_and_s _ _ zenon_H16ea). zenon_intro zenon_H1480. zenon_intro zenon_H14a9. % 3.01/3.28 apply tlhfof26860. apply sym_equal. exact zenon_H1480. % 3.01/3.28 apply (zenon_or_s _ _ zenon_H16e9); [ zenon_intro zenon_H16ec | zenon_intro zenon_H16eb ]. % 3.01/3.28 apply (zenon_and_s _ _ zenon_H16ec). zenon_intro zenon_H1484. zenon_intro zenon_H1591. % 3.01/3.28 apply tlhfof26781. apply sym_equal. exact zenon_H1484. % 3.01/3.28 apply (zenon_or_s _ _ zenon_H16eb); [ zenon_intro zenon_H16ee | zenon_intro zenon_H16ed ]. % 3.01/3.28 apply (zenon_and_s _ _ zenon_H16ee). zenon_intro zenon_H156a. zenon_intro zenon_H14ad. % 3.01/3.28 apply tlhfof26620. apply sym_equal. exact zenon_H156a. % 3.01/3.28 apply (zenon_or_s _ _ zenon_H16ed); [ zenon_intro zenon_H16f0 | zenon_intro zenon_H16ef ]. % 3.01/3.28 apply (zenon_and_s _ _ zenon_H16f0). zenon_intro zenon_H1488. zenon_intro zenon_H14b1. % 3.01/3.28 apply tlhfof26701. apply sym_equal. exact zenon_H1488. % 3.01/3.28 apply (zenon_or_s _ _ zenon_H16ef); [ zenon_intro zenon_H16f2 | zenon_intro zenon_H16f1 ]. % 3.01/3.28 apply (zenon_and_s _ _ zenon_H16f2). zenon_intro zenon_H148c. zenon_intro zenon_H14b5. % 3.01/3.28 apply tlhfof26538. apply sym_equal. exact zenon_H148c. % 3.01/3.28 apply (zenon_or_s _ _ zenon_H16f1); [ zenon_intro zenon_H16f4 | zenon_intro zenon_H16f3 ]. % 3.01/3.28 apply (zenon_and_s _ _ zenon_H16f4). zenon_intro zenon_H1490. zenon_intro zenon_H14b9. % 3.01/3.28 apply tlhfof26455. apply sym_equal. exact zenon_H1490. % 3.01/3.28 apply (zenon_or_s _ _ zenon_H16f3); [ zenon_intro zenon_H16f6 | zenon_intro zenon_H16f5 ]. % 3.01/3.28 apply (zenon_and_s _ _ zenon_H16f6). zenon_intro zenon_H1494. zenon_intro zenon_H14bd. % 3.01/3.28 apply tlhfof26371. apply sym_equal. exact zenon_H1494. % 3.01/3.28 apply (zenon_or_s _ _ zenon_H16f5); [ zenon_intro zenon_H16f8 | zenon_intro zenon_H16f7 ]. % 3.01/3.28 apply (zenon_and_s _ _ zenon_H16f8). zenon_intro zenon_H1498. zenon_intro zenon_H14c1. % 3.01/3.28 apply tlhfof26286. apply sym_equal. exact zenon_H1498. % 3.01/3.28 apply (zenon_or_s _ _ zenon_H16f7); [ zenon_intro zenon_H16fa | zenon_intro zenon_H16f9 ]. % 3.01/3.28 apply (zenon_and_s _ _ zenon_H16fa). zenon_intro zenon_H149c. zenon_intro zenon_H14c5. % 3.01/3.28 apply tlhfof26200. apply sym_equal. exact zenon_H149c. % 3.01/3.28 apply (zenon_or_s _ _ zenon_H16f9); [ zenon_intro zenon_H16fc | zenon_intro zenon_H16fb ]. % 3.01/3.28 apply (zenon_and_s _ _ zenon_H16fc). zenon_intro zenon_H14a0. zenon_intro zenon_H14c9. % 3.01/3.28 apply tlhfof26113. apply sym_equal. exact zenon_H14a0. % 3.01/3.28 apply (zenon_or_s _ _ zenon_H16fb); [ zenon_intro zenon_H16fe | zenon_intro zenon_H16fd ]. % 3.01/3.28 apply (zenon_and_s _ _ zenon_H16fe). zenon_intro zenon_H14a4. zenon_intro zenon_H14cd. % 3.01/3.28 apply tlhfof26025. apply sym_equal. exact zenon_H14a4. % 3.01/3.28 apply (zenon_and_s _ _ zenon_H16fd). zenon_intro zenon_H14a8. zenon_intro zenon_H164c. % 3.01/3.28 apply tlhfof25936. apply sym_equal. exact zenon_H14a8. % 3.01/3.28 Qed. % 3.01/3.28 % SZS output end Proof % 3.01/3.28 (* END-PROOF *) % 3.01/3.28 nodes searched: 727 % 3.01/3.28 max branch formulas: 4958 % 3.01/3.28 proof nodes created: 727 % 3.01/3.28 formulas created: 70013 % 3.01/3.28 %------------------------------------------------------------------------------